Theory Denotational_Semantics

theory "Denotational_Semantics" 
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Lib"
  "Ids"
  "Syntax"
begin
subsection ‹Denotational Semantics›
text ‹
  The canonical dynamic semantics of dL are given as a denotational semantics.
  The important definitions for the denotational semantics are states $\nu$,
  interpretations I and the semantic functions $[[\psi]]I$, $[[\theta]]I\nu$,
  $[[\alpha]]I$, which are represented by the Isabelle functions \verb|fml_sem|,
  \verb|dterm_sem| and \verb|prog_sem|, respectively.
  ›
subsection ‹States›
text ‹We formalize a state S as a pair $(S_V, S_V') : R^n \times R^n $, where $S_V$ assigns
  values to the program variables and $S_V$' assigns values to their
  differentials. Function constants are also formalized as having a fixed arity
  m \verb|(Rvec_dim)| which may differ from n. If a function does not need to
  have m arguments, any remaining arguments can be uniformly set to 0,
  which simulates the affect of having functions of less arguments.
  
  Most semantic proofs need to reason about states agreeing on variables.
  We say Vagree A B V if states A and B have the same values on all variables in V,
  similarly with VSagree A B V for simple states A and B and Iagree I J V for interpretations
  I and J.
  ›

― ‹Vector of reals of length ‹'a››
type_synonym 'a Rvec = "real^('a::finite)"
― ‹A state specifies one vector of values for unprimed variables ‹x› and a second vector for ‹x'››
type_synonym 'a state = "'a Rvec × 'a Rvec"
― ‹‹'a simple_state› is half a state - either the ‹x›s or the ‹x'›s›
type_synonym 'a simple_state = "'a Rvec"

definition Vagree :: "'c::finite state ⇒ 'c state ⇒ ('c + 'c) set ⇒ bool"
where "Vagree ν ν' V ≡
   (∀i. Inl i ∈ V ⟶ fst ν $ i = fst ν' $ i)
 ∧ (∀i. Inr i ∈ V ⟶ snd ν $ i = snd ν' $ i)"

definition VSagree :: "'c::finite simple_state ⇒ 'c simple_state ⇒ 'c set ⇒ bool"
where "VSagree ν ν' V ⟷ (∀i ∈ V. (ν $ i) = (ν' $ i))"

― ‹Agreement lemmas›
lemma agree_nil:"Vagree ν ω {}"
  by (auto simp add: Vagree_def)

lemma agree_supset:"A ⊇ B ⟹ Vagree ν ν' A ⟹ Vagree ν ν' B"
  by (auto simp add: Vagree_def)

lemma VSagree_nil:"VSagree ν ω {}"
  by (auto simp add: VSagree_def)

lemma VSagree_supset:"A ⊇ B ⟹ VSagree ν ν' A ⟹ VSagree ν ν' B"
  by (auto simp add: VSagree_def)

lemma VSagree_UNIV_eq:"VSagree A B UNIV ⟹ A = B"
  unfolding VSagree_def by (auto simp add: vec_eq_iff)

lemma agree_comm:"⋀A B V. Vagree A B V ⟹ Vagree B A V" unfolding Vagree_def by auto

lemma agree_sub:"⋀ν ω A B . A ⊆ B ⟹ Vagree ν ω B ⟹ Vagree ν ω A"
  unfolding Vagree_def by auto

lemma agree_UNIV_eq:"⋀ν ω. Vagree ν ω UNIV ⟹ ν = ω"
  unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma agree_UNIV_fst:"⋀ν ω. Vagree ν ω (Inl ` UNIV) ⟹ (fst ν) = (fst ω)"
  unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma agree_UNIV_snd:"⋀ν ω. Vagree ν ω (Inr ` UNIV) ⟹ (snd ν) = (snd ω)"
  unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma Vagree_univ:"⋀a b c d. Vagree (a,b) (c,d) UNIV ⟹ a = c ∧ b = d"
  by (auto simp add: Vagree_def vec_eq_iff)

lemma agree_union:"⋀ν ω A B. Vagree ν ω A ⟹ Vagree ν ω B ⟹ Vagree ν ω (A ∪ B)"
  unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma agree_trans:"Vagree ν μ A ⟹ Vagree μ ω B ⟹ Vagree ν ω (A ∩ B)"
  by (auto simp add: Vagree_def)

lemma agree_refl:"Vagree ν ν A"
  by (auto simp add: Vagree_def)

lemma VSagree_sub:"⋀ν ω A B . A ⊆ B ⟹ VSagree ν ω B ⟹ VSagree ν ω A"
  unfolding VSagree_def by auto

lemma VSagree_refl:"VSagree ν ν A"
  by (auto simp add: VSagree_def)

subsection Interpretations
text‹
    For convenience we pretend interpretations contain an extra field called
  FunctionFrechet specifying the Frechet derivative \verb|(FunctionFrechet f ν)| : $R^m \rightarrow R$ 
  for every function in every state. The proposition \verb|(is_interp I)| says that such a
  derivative actually exists and is continuous (i.e. all functions are C1-continuous)
  without saying what the exact derivative is.
  
  The type parameters 'a, 'b, 'c are finite types whose cardinalities indicate the maximum number 
  of functions, contexts, and <everything else defined by the interpretation>, respectively.
›
record ('a, 'b, 'c) interp =
  Functions       :: "'a ⇒ 'c Rvec ⇒ real"
  Predicates      :: "'c ⇒ 'c Rvec ⇒ bool"
  Contexts        :: "'b ⇒ 'c state set ⇒ 'c state set"
  Programs        :: "'c ⇒ ('c state * 'c state) set"
  ODEs            :: "'c ⇒ 'c simple_state ⇒ 'c simple_state"
  ODEBV           :: "'c ⇒ 'c set"

fun FunctionFrechet :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ 'a ⇒ 'c Rvec ⇒ 'c Rvec ⇒ real"
  where "FunctionFrechet I i = (THE f'. ∀ x. (Functions I i has_derivative f' x) (at x))"

― ‹For an interpretation to be valid, all functions must be differentiable everywhere.›
definition is_interp :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ bool"
  where "is_interp I ≡
   ∀x. ∀i. ((FDERIV (Functions I i) x :> (FunctionFrechet I i x)) ∧ continuous_on UNIV (λx. Blinfun (FunctionFrechet I i x)))"

lemma is_interpD:"is_interp I ⟹ ∀x. ∀i. (FDERIV (Functions I i) x :> (FunctionFrechet I i x))"
  unfolding is_interp_def by auto
  
― ‹Agreement between interpretations.›
definition Iagree :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a + 'b + 'c) set ⇒ bool"
where "Iagree I J V ≡
  (∀i∈V.
    (∀x. i = Inl x ⟶ Functions I x = Functions J x) ∧
    (∀x. i = Inr (Inl x) ⟶ Contexts I x = Contexts J x) ∧
    (∀x. i = Inr (Inr x) ⟶ Predicates I x = Predicates J x) ∧
    (∀x. i = Inr (Inr x) ⟶ Programs I x = Programs J x) ∧
    (∀x. i = Inr (Inr x) ⟶ ODEs I x = ODEs J x) ∧
    (∀x. i = Inr (Inr x) ⟶ ODEBV I x = ODEBV J x))"

lemma Iagree_Func:"Iagree I J V ⟹ Inl f ∈ V ⟹ Functions I f = Functions J f"
  unfolding Iagree_def by auto

lemma Iagree_Contexts:"Iagree I J V ⟹ Inr (Inl C) ∈ V ⟹ Contexts I C = Contexts J C"
  unfolding Iagree_def by auto

lemma Iagree_Pred:"Iagree I J V ⟹ Inr (Inr p) ∈ V ⟹ Predicates I p = Predicates J p"
  unfolding Iagree_def by auto

lemma Iagree_Prog:"Iagree I J V ⟹ Inr (Inr a) ∈ V ⟹ Programs I a = Programs J a"
  unfolding Iagree_def by auto

lemma Iagree_ODE:"Iagree I J V ⟹ Inr (Inr a) ∈ V ⟹ ODEs I a = ODEs J a"
  unfolding Iagree_def by auto  

lemma Iagree_comm:"⋀A B V. Iagree A B V ⟹ Iagree B A V" 
  unfolding Iagree_def by auto

lemma Iagree_sub:"⋀I J A B . A ⊆ B ⟹ Iagree I J B ⟹ Iagree I J A"
  unfolding Iagree_def by auto

lemma Iagree_refl:"Iagree I I A"
  by (auto simp add: Iagree_def)

― ‹Semantics for differential-free terms. Because there are no differentials, depends only on the ‹x› variables›
― ‹and not the ‹x'› variables.›
primrec sterm_sem :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c simple_state ⇒ real"
where
  "sterm_sem I (Var x) v = v $ x"
| "sterm_sem I (Function f args) v = Functions I f (χ i. sterm_sem I (args i) v)"
| "sterm_sem I (Plus t1 t2) v = sterm_sem I t1 v + sterm_sem I t2 v"
| "sterm_sem I (Times t1 t2) v = sterm_sem I t1 v * sterm_sem I t2 v"
| "sterm_sem I (Const r) v = r"
| "sterm_sem I ($' c) v = undefined"
| "sterm_sem I (Differential d) v = undefined"
  
― ‹‹frechet I θ ν› syntactically computes the frechet derivative of the term ‹θ› in the interpretation›
― ‹‹I› at state ‹ν› (containing only the unprimed variables). The frechet derivative is a›
― ‹linear map from the differential state ‹ν› to reals.›
primrec frechet :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c simple_state ⇒ 'c simple_state ⇒ real"
where
  "frechet I (Var x) v = (λv'. v' ∙ axis x 1)"
| "frechet I (Function f args) v =
    (λv'. FunctionFrechet I f (χ i. sterm_sem I (args i) v) (χ i. frechet I (args i) v v'))"
| "frechet I (Plus t1 t2) v = (λv'. frechet I t1 v v' + frechet I t2 v v')"
| "frechet I (Times t1 t2) v =
    (λv'. sterm_sem I t1 v * frechet I t2 v v' + frechet I t1 v v' * sterm_sem I t2 v)"
| "frechet I (Const r) v = (λv'. 0)"
| "frechet I ($' c) v = undefined"
| "frechet I (Differential d) v = undefined"

definition directional_derivative :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c state ⇒ real"
where "directional_derivative I t = (λv. frechet I t (fst v) (snd v))"

― ‹Sem for terms that are allowed to contain differentials.›
― ‹Note there is some duplication with ‹sterm_sem›.›
primrec dterm_sem :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c state ⇒ real"
where
  "dterm_sem I (Var x) = (λv. fst v $ x)"
| "dterm_sem I (DiffVar x) = (λv. snd v $ x)"
| "dterm_sem I (Function f args) = (λv. Functions I f (χ i. dterm_sem I (args i) v))"
| "dterm_sem I (Plus t1 t2) = (λv. (dterm_sem I t1 v) + (dterm_sem I t2 v))"
| "dterm_sem I (Times t1 t2) = (λv. (dterm_sem I t1 v) * (dterm_sem I t2 v))"
| "dterm_sem I (Differential t) = (λv. directional_derivative I t v)"
| "dterm_sem I (Const c) = (λv. c)"

text‹ The semantics of an ODE is the vector field at a given point. ODE's are all time-independent
  so no time variable is necessary. Terms on the RHS of an ODE must be differential-free, so
  depends only on the xs.

  The safety predicate \texttt{osafe} ensures the domains of ODE1 and ODE2 are disjoint, so vector addition
  is equivalent to saying "take things defined from ODE1 from ODE1, take things defined
  by ODE2 from ODE2"›
fun ODE_sem:: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) ODE ⇒ 'c Rvec ⇒ 'c Rvec"
  where
  ODE_sem_OVar:"ODE_sem I (OVar x) = ODEs I x"
| ODE_sem_OSing:"ODE_sem I (OSing x θ) =  (λν. (χ i. if i = x then sterm_sem I θ ν else 0))"
― ‹Note: Could define using ‹SOME› operator in a way that more closely matches above description,›
― ‹but that gets complicated in the ‹OVar› case because not all variables are bound by the ‹OVar››
| ODE_sem_OProd:"ODE_sem I (OProd ODE1 ODE2) = (λν. ODE_sem I ODE1 ν + ODE_sem I ODE2 ν)"

― ‹The bound variables of an ODE›
fun ODE_vars :: "('a,'b,'c) interp ⇒ ('a, 'c) ODE ⇒ 'c set"
  where 
  "ODE_vars I (OVar c) = ODEBV I c"
| "ODE_vars I (OSing x θ) = {x}"
| "ODE_vars I (OProd ODE1 ODE2) = ODE_vars I ODE1 ∪ ODE_vars I ODE2"
  
fun semBV ::"('a, 'b,'c) interp ⇒ ('a, 'c) ODE ⇒ ('c + 'c) set"
  where "semBV I ODE = Inl ` (ODE_vars I ODE) ∪ Inr ` (ODE_vars I ODE)"

lemma ODE_vars_lr:
  fixes x::"'sz" and ODE::"('sf,'sz) ODE" and I::"('sf,'sc,'sz) interp"
  shows "Inl x ∈ semBV I ODE ⟷ Inr x ∈ semBV I ODE"
  by (induction "ODE", auto)

fun mk_xode::"('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'c::finite) ODE ⇒ 'c::finite simple_state ⇒ 'c::finite state"
where "mk_xode I ODE sol = (sol, ODE_sem I ODE sol)"
 
text‹ Given an initial state $\nu$ and solution to an ODE at some point, construct the resulting state $\omega$.
  This is defined using the SOME operator because the concrete definition is unwieldy. ›
definition mk_v::"('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'c::finite) ODE ⇒ 'c::finite state ⇒ 'c::finite simple_state ⇒ 'c::finite state"
where "mk_v I ODE ν sol = (THE ω. 
  Vagree ω ν (- semBV I ODE) 
∧ Vagree ω (mk_xode I ODE sol) (semBV I ODE))"

― ‹‹repv ν x r› replaces the value of (unprimed) variable ‹x› in the state ‹ν› with r›
fun repv :: "'c::finite state ⇒ 'c ⇒ real ⇒ 'c state"
where "repv v x r = ((χ y. if x = y then r else vec_nth (fst v) y), snd v)"

― ‹‹repd ν x' r› replaces the value of (primed) variable ‹x'› in the state ‹ν› with ‹r››
fun repd :: "'c::finite state ⇒ 'c ⇒ real ⇒ 'c state"
where "repd v x r = (fst v, (χ y. if x = y then r else vec_nth (snd v) y))"  
  
― ‹Semantics for formulas, differential formulas, programs.›
fun fml_sem  :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) formula ⇒ 'c::finite state set" and
  prog_sem :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) hp ⇒ ('c::finite state * 'c::finite state) set"
where
  "fml_sem I (Geq t1 t2) = {v. dterm_sem I t1 v ≥ dterm_sem I t2 v}"
| "fml_sem I (Prop P terms) = {ν. Predicates I P (χ i. dterm_sem I (terms i) ν)}"
| "fml_sem I (Not φ) = {v. v ∉ fml_sem I φ}"
| "fml_sem I (And φ ψ) = fml_sem I φ ∩ fml_sem I ψ"
| "fml_sem I (Exists x φ) = {v | v r. (repv v x r) ∈ fml_sem I φ}"
| "fml_sem I (Diamond α φ) = {ν | ν ω. (ν, ω) ∈ prog_sem I α ∧ ω ∈ fml_sem I φ}"
| "fml_sem I (InContext c φ) = Contexts I c (fml_sem I φ)"

| "prog_sem I (Pvar p) = Programs I p"
| "prog_sem I (Assign x t) = {(ν, ω). ω = repv ν x (dterm_sem I t ν)}"
| "prog_sem I (DiffAssign x t) = {(ν, ω). ω = repd ν x (dterm_sem I t ν)}"
| "prog_sem I (Test φ) = {(ν, ν) | ν. ν ∈ fml_sem I φ}"
| "prog_sem I (Choice α β) = prog_sem I α ∪ prog_sem I β"
| "prog_sem I (Sequence α β) = prog_sem I α O prog_sem I β"
| "prog_sem I (Loop α) = (prog_sem I α)⇧*"
| "prog_sem I (EvolveODE ODE φ) =
  ({(ν, mk_v I ODE ν (sol t)) | ν sol t.
      t ≥ 0 ∧
      (sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
      sol 0 = fst ν})"

context ids begin
definition valid :: "('sf, 'sc, 'sz) formula ⇒ bool"
where "valid φ ≡ (∀ I. ∀ ν. is_interp I ⟶ ν ∈ fml_sem I φ)"
end

text‹ Because mk\_v is defined with the SOME operator, need to construct a state that satisfies
    ${\tt Vagree} \omega \nu (- {\tt ODE\_vars\ ODE}) 
     \wedge {\tt Vagree} \omega {\tt (mk\_xode\ I\ ODE\ sol)\ (ODE\_vars\ ODE)})$
    to do anything useful ›
fun concrete_v::"('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'c::finite) ODE ⇒ 'c::finite state ⇒ 'c::finite simple_state ⇒ 'c::finite state"
where "concrete_v I ODE ν sol =
((χ i. (if Inl i ∈ semBV I ODE then sol else (fst ν)) $ i),
 (χ i. (if Inr i ∈ semBV I ODE then ODE_sem I ODE sol else (snd ν)) $ i))"

lemma mk_v_exists:"∃ω. Vagree ω ν (- semBV I ODE) 
∧ Vagree ω (mk_xode I ODE sol) (semBV I ODE)"
  by(rule exI[where x="(concrete_v I ODE ν sol)"], auto simp add: Vagree_def)
    
lemma mk_v_agree:"Vagree (mk_v I ODE ν sol) ν (- semBV I ODE) 
∧ Vagree (mk_v I ODE ν sol) (mk_xode I ODE sol) (semBV I ODE)"
  unfolding mk_v_def 
  apply(rule theI[where a= "((χ i. (if Inl i ∈ semBV I ODE then sol else (fst ν)) $ i),
  (χ i. (if Inr i ∈ semBV I ODE then ODE_sem I ODE sol else (snd ν)) $ i))"])
   using exE[OF mk_v_exists, of ν I ODE sol]
   by (auto simp add: Vagree_def vec_eq_iff)

lemma mk_v_concrete:"mk_v I ODE ν sol = ((χ i. (if Inl i ∈ semBV I ODE then sol else (fst ν)) $ i),
  (χ i. (if Inr i ∈ semBV I ODE then ODE_sem I ODE sol else (snd ν)) $ i))"
  apply(rule agree_UNIV_eq)
  using mk_v_agree[of I ODE ν sol]
  unfolding Vagree_def by auto

subsection ‹Trivial Simplification Lemmas›
text ‹
 We often want to pretend the definitions in the semantics are written slightly
 differently than they are. Since the simplifier has some trouble guessing that
 these are the right simplifications to do, we write them all out explicitly as
 lemmas, even though they prove trivially.
›

lemma svar_case:
  "sterm_sem I (Var x) = (λv. v $ x)"
  by auto

lemma sconst_case:
  "sterm_sem I (Const r) = (λv. r)"
  by auto

lemma sfunction_case:
  "sterm_sem I (Function f args) = (λv. Functions I f (χ i. sterm_sem I (args i) v))"
  by auto

lemma splus_case:
  "sterm_sem I (Plus t1 t2) = (λv. (sterm_sem I t1 v) + (sterm_sem I t2 v))"
  by auto

lemma stimes_case:
  "sterm_sem I (Times t1 t2) = (λv. (sterm_sem I t1 v) * (sterm_sem I t2 v))"
  by auto  

lemma or_sem [simp]:
  "fml_sem I (Or φ ψ) = fml_sem I φ ∪ fml_sem I ψ"
  by (auto simp add: Or_def)

lemma iff_sem [simp]: "(ν ∈ fml_sem I (A ↔ B))
  ⟷ ((ν ∈ fml_sem I A) ⟷ (ν ∈ fml_sem I B))"
  by (auto simp add: Equiv_def)

lemma box_sem [simp]:"fml_sem I (Box α φ) = {ν. ∀ ω. (ν, ω) ∈ prog_sem I α ⟶ ω ∈ fml_sem I φ}"
  unfolding Box_def fml_sem.simps
  using Collect_cong by (auto)
  
lemma forall_sem [simp]:"fml_sem I (Forall x φ) = {v. ∀r. (repv v x r) ∈ fml_sem I φ}"
  unfolding Forall_def fml_sem.simps
  using Collect_cong by (auto)
  
lemma greater_sem[simp]:"fml_sem I (Greater θ θ') = {v. dterm_sem I θ v > dterm_sem I θ' v}"
  unfolding Greater_def by auto

lemma loop_sem:"prog_sem I (Loop α) = (prog_sem I α)⇧*"
  by (auto)

lemma impl_sem [simp]: "(ν ∈ fml_sem I (A → B))
  = ((ν ∈ fml_sem I A) ⟶ (ν ∈ fml_sem I B))"
  by (auto simp add: Implies_def)

lemma equals_sem [simp]: "(ν ∈ fml_sem I (Equals θ θ'))
  = (dterm_sem I θ ν = dterm_sem I θ' ν)"
  by (auto simp add: Equals_def)

lemma diamond_sem [simp]: "fml_sem I (Diamond α φ)
  = {ν. ∃ ω. (ν, ω) ∈ prog_sem I α ∧ ω ∈ fml_sem I φ}"
  by auto

lemma tt_sem [simp]:"fml_sem I TT = UNIV" unfolding TT_def by auto
lemma ff_sem [simp]:"fml_sem I FF = {}" unfolding FF_def by auto

lemma iff_to_impl: "((ν ∈ fml_sem I A) ⟷ (ν ∈ fml_sem I B))
  ⟷ (((ν ∈ fml_sem I A) ⟶ (ν ∈ fml_sem I B))
     ∧ ((ν ∈ fml_sem I B) ⟶ (ν ∈ fml_sem I A)))"
  by (auto) 
    
    fun seq2fml :: "('a,'b,'c) sequent ⇒ ('a,'b,'c) formula"
where
  "seq2fml (ante,succ) = Implies (foldr And ante TT) (foldr Or succ FF)"
  
context ids begin
fun seq_sem ::"('sf, 'sc, 'sz) interp ⇒ ('sf, 'sc, 'sz) sequent ⇒ 'sz state set"
where "seq_sem I S = fml_sem I (seq2fml S)"

lemma and_foldl_sem:"ν ∈ fml_sem I (foldr And Γ TT) ⟹ (⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ)"
  by(induction Γ, auto simp add: member_rec)

lemma and_foldl_sem_conv:"(⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ) ⟹ ν ∈ fml_sem I (foldr And Γ TT)"
  by(induction Γ, auto simp add: member_rec)

lemma or_foldl_sem:"List.member Γ φ ⟹ ν ∈ fml_sem I φ ⟹ ν ∈ fml_sem I (foldr Or Γ FF)"
  by(induction Γ, auto simp add: member_rec)

lemma or_foldl_sem_conv:"ν ∈ fml_sem I (foldr Or Γ FF) ⟹ ∃ φ. ν ∈ fml_sem I φ ∧ List.member Γ φ"
  by(induction Γ, auto simp add: member_rec)

lemma seq_semI':"(ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I (foldr Or Δ FF)) ⟹ ν ∈ seq_sem I (Γ,Δ)"
  by auto 

lemma seq_semD':"⋀P. ν ∈ seq_sem I (Γ,Δ) ⟹ ((ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I (foldr Or Δ FF)) ⟹ P) ⟹ P"
  by simp

definition sublist::"'a list ⇒ 'a list ⇒ bool"
where "sublist A B ≡ (∀x. List.member A x ⟶ List.member B x)"

lemma sublistI:"(⋀x. List.member A x ⟹ List.member B x) ⟹ sublist A B"
  unfolding sublist_def by auto

lemma Γ_sub_sem:"sublist Γ1 Γ2 ⟹ ν ∈ fml_sem I (foldr And Γ2 TT) ⟹ ν ∈ fml_sem I (foldr And Γ1 TT)"
  unfolding sublist_def 
  by (metis and_foldl_sem and_foldl_sem_conv)

lemma seq_semI:"List.member Δ ψ ⟹((⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ) ⟹ ν ∈ fml_sem I ψ) ⟹ ν ∈ seq_sem I (Γ,Δ)"
  apply(rule seq_semI')
  using and_foldl_sem[of ν I Γ] or_foldl_sem by blast

lemma seq_semD:"ν ∈ seq_sem I (Γ,Δ) ⟹ (⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ) ⟹ ∃φ. (List.member Δ φ) ∧ν ∈ fml_sem I φ "
  apply(rule seq_semD')
  using and_foldl_sem_conv or_foldl_sem_conv
  by blast+

lemma seq_MP:"ν ∈ seq_sem I (Γ,Δ) ⟹ ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I (foldr Or Δ FF)"
  by(induction Δ, auto)

definition seq_valid
where "seq_valid S ≡ ∀I. is_interp I ⟶ seq_sem I S = UNIV"  


text‹ Soundness for derived rules is local soundness, i.e. if the premisses are all true in the same interpretation,
  then the conclusion is also true in that same interpretation. ›
definition sound :: "('sf, 'sc, 'sz) rule ⇒ bool"
where "sound R ⟷ (∀I. is_interp I ⟶ (∀i. i ≥ 0 ⟶ i < length (fst R) ⟶ seq_sem I (nth (fst R) i) = UNIV) ⟶ seq_sem I (snd R) = UNIV)"

lemma soundI:"(⋀I. is_interp I ⟹ (⋀i. i ≥ 0 ⟹ i < length SG ⟹ seq_sem I (nth SG i) = UNIV) ⟹ seq_sem I G = UNIV) ⟹ sound (SG,G)"
  unfolding sound_def by auto

lemma soundI':"(⋀I ν. is_interp I ⟹ (⋀i . i ≥ 0 ⟹ i < length SG ⟹ ν ∈ seq_sem I (nth SG i)) ⟹ ν ∈ seq_sem I G) ⟹ sound (SG,G)"
  unfolding sound_def by auto
    
lemma soundI_mem:"(⋀I. is_interp I ⟹ (⋀φ. List.member SG φ ⟹ seq_sem I φ = UNIV) ⟹ seq_sem I C = UNIV) ⟹ sound (SG,C)"
  apply (auto simp add: sound_def)
  by (metis in_set_conv_nth in_set_member iso_tuple_UNIV_I seq2fml.simps)

lemma soundI_memv:"(⋀I. is_interp I ⟹ (⋀φ ν. List.member SG φ ⟹ ν ∈ seq_sem I φ) ⟹ (⋀ν. ν ∈ seq_sem I C)) ⟹ sound (SG,C)"
  apply(rule soundI_mem)
  using impl_sem by blast

lemma soundI_memv':"(⋀I. is_interp I ⟹ (⋀φ ν. List.member SG φ ⟹ ν ∈ seq_sem I φ) ⟹ (⋀ν. ν ∈ seq_sem I C)) ⟹ R = (SG,C) ⟹ sound R"
  using  soundI_mem
  using impl_sem by blast

lemma soundD_mem:"sound (SG,C) ⟹ (⋀I. is_interp I ⟹ (⋀φ. List.member SG φ ⟹ seq_sem I φ = UNIV) ⟹ seq_sem I C = UNIV)"
  apply (auto simp add: sound_def)
  using in_set_conv_nth in_set_member iso_tuple_UNIV_I seq2fml.simps
  by (metis seq2fml.elims)

lemma soundD_memv:"sound (SG,C) ⟹ (⋀I. is_interp I ⟹ (⋀φ ν. List.member SG φ ⟹ ν ∈ seq_sem I φ) ⟹ (⋀ν. ν ∈ seq_sem I C))"
  using soundD_mem
  by (metis UNIV_I UNIV_eq_I)

end
end