Theory Proof_Checker

theory "Proof_Checker" 
imports
  Ordinary_Differential_Equations.ODE_Analysis
  "Ids"
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Axioms"
  "Differential_Axioms"
  "Frechet_Correctness"
  "Static_Semantics"
  "Coincidence"
  "Bound_Effect"
  "Uniform_Renaming"
  "USubst_Lemma"
  "Pretty_Printer"
  
begin context ids begin
section ‹Proof Checker›
text ‹This proof checker defines a datatype for proof terms in dL and a function for checking proof
 terms, with a soundness proof that any proof accepted by the checker is a proof of a sound rule or
 valid formula.

 A simple concrete hybrid system and a differential invariant rule for conjunctions are provided
 as example proofs.
›
  
lemma sound_weaken_gen:"⋀A B C. sublist A B ⟹ sound (A, C) ⟹ sound (B,C)"
proof (rule soundI_mem)
  fix A B::"('sf,'sc,'sz) sequent list" 
    and C::"('sf,'sc,'sz) sequent" 
    and I::"('sf,'sc,'sz) interp"
  assume sub:"sublist A B"
  assume good:"is_interp I"
  assume "sound (A, C)"
  then have soundC:"(⋀φ. List.member A φ ⟹ seq_sem I φ = UNIV) ⟹ seq_sem I C = UNIV"
    apply simp
    apply(drule soundD_mem)
      by (auto simp add: good)
  assume SG:"(⋀φ. List.member B φ ⟹ seq_sem I φ = UNIV)"
  show "seq_sem I C = UNIV"
    using soundC SG sub unfolding sublist_def by auto
qed
  
lemma sound_weaken:"⋀SG SGS C. sound (SGS, C) ⟹ sound (SG # SGS, C)"
  subgoal for SG SGS C
    apply(induction SGS)
     subgoal unfolding sound_def by auto
    subgoal for SG2 SGS
      unfolding sound_def 
      by (metis fst_conv le0 length_Cons not_less_eq nth_Cons_Suc snd_conv)
    done
  done

lemma member_filter:"⋀P. List.member (filter P L) x ⟹ List.member L x"
  apply(induction L, auto)
  by(metis (full_types) member_rec(1))

lemma nth_member:"n < List.length L ⟹ List.member L (List.nth L n)"
  apply(induction L, auto simp add: member_rec)
  by (metis in_set_member length_Cons nth_mem set_ConsD)

lemma mem_appL:"List.member A x ⟹ List.member (A @ B) x"
  by(induction A, auto simp add: member_rec)

lemma sound_weaken_appR:"⋀SG SGS C. sound (SG, C) ⟹ sound (SG @ SGS, C)"
  subgoal for SG SGS C
    apply(rule sound_weaken_gen)
     apply(auto)
    unfolding sublist_def apply(rule allI)
    subgoal for x
      using mem_appL[of SG x SGS] by auto 
    done
  done

fun start_proof::"('sf,'sc,'sz) sequent ⇒ ('sf,'sc,'sz) rule"
where "start_proof S = ([S], S)"
  
lemma start_proof_sound:"sound (start_proof S)"
  unfolding sound_def by auto
  
section ‹Proof Checker Implementation›

datatype axiom =
  AloopIter | AI | Atest | Abox | Achoice | AK | AV | Aassign | Adassign
| AdConst | AdPlus | AdMult
| ADW | ADE | ADC | ADS | ADIGeq | ADIGr | ADG
  
fun get_axiom:: "axiom ⇒ ('sf,'sc,'sz) formula"
where 
  "get_axiom AloopIter = loop_iterate_axiom"
| "get_axiom AI = Iaxiom"
| "get_axiom Atest = test_axiom"
| "get_axiom Abox = box_axiom"
| "get_axiom Achoice = choice_axiom"
| "get_axiom AK = Kaxiom"
| "get_axiom AV = Vaxiom"
| "get_axiom Aassign = assign_axiom"
| "get_axiom Adassign = diff_assign_axiom" 
| "get_axiom AdConst = diff_const_axiom"
| "get_axiom AdPlus = diff_plus_axiom"
| "get_axiom AdMult = diff_times_axiom"
| "get_axiom ADW = DWaxiom"
| "get_axiom ADE = DEaxiom"
| "get_axiom ADC = DCaxiom"
| "get_axiom ADS = DSaxiom"
| "get_axiom ADIGeq = DIGeqaxiom"
| "get_axiom ADIGr = DIGraxiom"
| "get_axiom ADG = DGaxiom"
  
lemma axiom_safe:"fsafe (get_axiom a)"
  by(cases a, auto simp add: axiom_defs Box_def Or_def Equiv_def Implies_def empty_def Equals_def f1_def p1_def P_def f0_def expand_singleton Forall_def Greater_def id_simps)
  (*apply(cases a)
  prefer 9
  subgoal
    apply(simp only: get_axiom.simps diff_assign_axiom_def Equiv_def Or_def Box_def)
    apply(simp only: fsafe_Not_simps fsafe_Diamond_simps fsafe_And_simps)
    apply(rule conjI)+
    subgoal apply(simp only: hpsafe_DiffAssign_simps dsafe_Fun_simps empty_def dsafe_Const) by auto
    
    *)
   (*auto simp add: loop_iterate_axiom_def Iaxiom_def diff_assign_axiom_def test_axiom_def choice_axiom_def box_axiom_def empty_def Kaxiom_def Vaxiom_def assign_axiom_def diff_const_axiom_def diff_plus_axiom_def diff_times_axiom_def DWaxiom_def Equals_def state_fun_def DEaxiom_def DCaxiom_def DSaxiom_def DIGeqaxiom_def DIGraxiom_def f1_def p1_def P_def expand_singleton f0_def Forall_def DGaxiom_def Equiv_def Implies_def Or_def Box_def Greater_def vne12*)
lemma axiom_valid:"valid (get_axiom a)"
proof (cases a)
  case AloopIter
  then show ?thesis by (simp add: loop_valid) 
next
  case AI
  then show ?thesis by (simp add: I_valid)
next
  case Atest
  then show ?thesis by (simp add: test_valid)
next
  case Abox
  then show ?thesis by (simp add: box_valid)
next
  case Achoice
  then show ?thesis by (simp add: choice_valid)
next
  case AK
  then show ?thesis by (simp add: K_valid)
next
  case AV
  then show ?thesis by (simp add: V_valid)
next
  case Aassign
  then show ?thesis by (simp add: assign_valid)
next
  case Adassign
  then show ?thesis by (simp add: diff_assign_valid)
next
  case AdConst
  then show ?thesis by (simp add: diff_const_axiom_valid)
next
  case AdPlus
  then show ?thesis by (simp add: diff_plus_axiom_valid)
next
  case AdMult
  then show ?thesis by (simp add: diff_times_axiom_valid)
next
  case ADW
  then show ?thesis by (simp add: DW_valid)
next
  case ADE
  then show ?thesis by (simp add: DE_valid)
next
  case ADC
  then show ?thesis by (simp add: DC_valid)
next
  case ADS
  then show ?thesis by (simp add: DS_valid)
next
  case ADIGeq
  then show ?thesis by (simp add: DIGeq_valid)
next
  case ADIGr
  then show ?thesis by (simp add: DIGr_valid)
next
  case ADG
  then show ?thesis by (simp add: DG_valid)
qed

datatype rrule = ImplyR | AndR | CohideR | CohideRR | TrueR | EquivR
datatype lrule = ImplyL | AndL | EquivForwardL | EquivBackwardL
  
datatype ('a, 'b, 'c) step =
  Axiom axiom
| MP
| G
| CT
| CQ  "('a, 'c) trm" "('a, 'c) trm" "('a, 'b, 'c) subst"
| CE  "('a, 'b, 'c) formula" "('a, 'b, 'c) formula" "('a, 'b, 'c) subst"
| Skolem
― ‹Apply ‹Usubst› to some other (valid) formula›
| VSubst "('a, 'b, 'c) formula" "('a, 'b, 'c) subst"
| AxSubst axiom "('a, 'b, 'c) subst"
| URename
| BRename
| Rrule rrule nat
| Lrule lrule nat
| CloseId nat nat
| Cut "('a, 'b, 'c) formula"
| DEAxiomSchema "('a,'c) ODE" "('a, 'b, 'c) subst"
  
type_synonym ('a, 'b, 'c) derivation = "(nat * ('a, 'b, 'c) step) list"
type_synonym ('a, 'b, 'c) pf = "('a,'b,'c) sequent * ('a, 'b, 'c) derivation"

fun seq_to_string :: "('sf, 'sc, 'sz) sequent ⇒ char list"
where "seq_to_string (A,S) = join '', '' (map fml_to_string A) @ '' |- '' @ join '', '' (map fml_to_string S)"
  
fun rule_to_string :: "('sf, 'sc, 'sz) rule ⇒ char list"
where "rule_to_string (SG, C) = (join '';;   '' (map seq_to_string SG)) @ ''            '' @  ⌦‹[char_of_nat 10] @› seq_to_string C"

fun close :: "'a list ⇒ 'a ⇒'a list"
where "close L x = filter (λy. y ≠ x) L"

fun closeI ::"'a list ⇒ nat ⇒'a list"
where "closeI L i = close L (nth L i)"

lemma close_sub:"sublist (close Γ φ) Γ"
  apply (auto simp add: sublist_def)
  using member_filter by fastforce

lemma close_app_comm:"close (A @ B) x  = close A x @ close B x"
  by auto

lemma close_provable_sound:"sound (SG, C) ⟹ sound (close SG φ, φ) ⟹ sound (close SG φ, C)"
proof (rule soundI_mem)
  fix I::"('sf,'sc,'sz) interp"
  assume S1:"sound (SG, C)"
  assume S2:"sound (close SG φ, φ)"
  assume good:"is_interp I"
  assume SGCs:"(⋀φ'. List.member (close SG φ) φ' ⟹ seq_sem I φ' = UNIV)"
  have Sφ:"seq_sem I φ = UNIV"
    using S2 apply simp
    apply(drule soundD_mem)
      using good apply auto
    using SGCs UNIV_I by fastforce
  have mem_close:"⋀P. List.member SG P ⟹ P ≠ φ ⟹ List.member (close SG φ) P"
    by(induction SG, auto simp add: member_rec)
  have SGs:"⋀P. List.member SG P ⟹ seq_sem I P = UNIV"
    subgoal for P
      apply(cases "P = φ")
       subgoal using Sφ by auto
      subgoal using mem_close[of P] SGCs by auto
      done
    done
  show "seq_sem I C = UNIV"
    using S1 apply simp
    apply(drule soundD_mem)
      using good apply auto
    using SGs apply auto
    using impl_sem by blast
  qed

fun Lrule_result :: "lrule ⇒ nat ⇒ ('sf, 'sc, 'sz) sequent ⇒ ('sf, 'sc, 'sz) sequent list"
where "Lrule_result AndL j (A,S) = (case (nth A j) of And p q ⇒ [(close ([p, q] @ A) (nth A j), S)])"
| "Lrule_result ImplyL j (A,S) = (case (nth A j) of Not (And (Not q) (Not (Not p))) ⇒ 
   [(close (q # A) (nth A j), S), (close A (nth A j), p # S)])"
| "Lrule_result EquivForwardL j (A,S) = (case (nth A j) of Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) ⇒
   [(close (q # A) (nth A j), S), (close A (nth A j), p # S)])"
| "Lrule_result EquivBackwardL j (A,S) = (case (nth A j) of Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) ⇒
   [(close (p # A) (nth A j), S), (close A (nth A j), q # S)])"

― ‹Note: Some of the pattern-matching here is... interesting. The reason for this is that we can only›
― ‹match on things in the base grammar, when we would quite like to check things in the derived grammar.›
― ‹So all the pattern-matches have the definitions expanded, sometimes in a silly way.›
fun Rrule_result :: "rrule ⇒ nat ⇒ ('sf, 'sc, 'sz) sequent ⇒ ('sf, 'sc, 'sz) sequent list"
where 
  Rstep_Imply:"Rrule_result ImplyR j (A,S) = (case (nth S j) of Not (And (Not q) (Not (Not p))) ⇒ [(p # A, q # (closeI S j))] | _ ⇒ undefined)"
| Rstep_And:"Rrule_result AndR j (A,S) = (case (nth S j) of (And p q) ⇒ [(A, p # (closeI S j )), (A, q # (closeI S j))])"
| Rstep_EquivR:"Rrule_result EquivR j (A,S) =
   (case (nth S j) of Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) ⇒ 
                (if (p = p' ∧ q = q') then [(p # A, q # (closeI S j)), (q # A, p # (closeI S j))]
                else undefined))"
| Rstep_CohideR:"Rrule_result CohideR j (A,S) = [(A, [nth S j])]"
| Rstep_CohideRR:"Rrule_result CohideRR j (A,S) = [([], [nth S j])]"
| Rstep_TrueR:"Rrule_result TrueR j (A,S) = []"

fun step_result :: "('sf, 'sc, 'sz) rule ⇒ (nat * ('sf, 'sc, 'sz) step) ⇒  ('sf, 'sc, 'sz) rule"
where
  Step_axiom:"step_result (SG,C) (i,Axiom a)   = (closeI SG i, C)"
| Step_AxSubst:"step_result (SG,C) (i,AxSubst a σ)   = (closeI SG i, C)"
| Step_Lrule:"step_result (SG,C) (i,Lrule L j) = (close (append SG (Lrule_result L j (nth SG i))) (nth SG i), C)"
| Step_Rrule:"step_result (SG,C) (i,Rrule L j) = (close (append SG (Rrule_result L j (nth SG i))) (nth SG i), C)" 
| Step_Cut:"step_result (SG,C) (i,Cut φ) = (let (A,S) = nth SG i in ((φ # A, S) # ((A, φ # S) # (closeI SG i)), C))"
| Step_Vsubst:"step_result (SG,C) (i,VSubst φ σ) = (closeI SG i, C)"
| Step_CloseId:"step_result (SG,C) (i,CloseId j k) = (closeI SG i, C)"
| Step_G:"step_result (SG,C) (i,G) = (case nth SG i of (_, (Not (Diamond q (Not p))) # Nil) ⇒ (([], [p]) # closeI SG i, C))"
| Step_DEAxiomSchema:"step_result (SG,C) (i,DEAxiomSchema ODE σ) = (closeI SG i, C)"
| Step_CE:"step_result (SG,C) (i, CE φ ψ σ) =  (closeI SG i, C)"
| Step_CQ:"step_result (SG,C) (i, CQ θ1 θ2 σ) =  (closeI SG i, C)"
| Step_default:"step_result R (i,S) = R"
  
fun deriv_result :: "('sf, 'sc, 'sz) rule ⇒ ('sf, 'sc, 'sz) derivation ⇒ ('sf, 'sc, 'sz) rule"
where 
  "deriv_result R [] = R"
| "deriv_result R (s # ss) = deriv_result (step_result R s) (ss)" 
  
fun proof_result :: "('sf, 'sc, 'sz) pf ⇒ ('sf, 'sc, 'sz) rule"
where "proof_result (D,S) = deriv_result (start_proof D) S"
  
inductive lrule_ok ::"('sf,'sc,'sz) sequent list ⇒ ('sf,'sc,'sz) sequent ⇒ nat ⇒ nat ⇒ lrule ⇒ bool"
where
  Lrule_And:"⋀p q. nth (fst (nth SG i)) j = (p && q) ⟹ lrule_ok SG C i j AndL"
| Lrule_Imply:"⋀p q. nth (fst (nth SG i)) j = (p → q) ⟹ lrule_ok SG C i j ImplyL"
| Lrule_EquivForward:"⋀p q. nth (fst (nth SG i)) j = (p ↔ q) ⟹ lrule_ok SG C i j EquivForwardL"
| Lrule_EquivBackward:"⋀p q. nth (fst (nth SG i)) j = (p ↔ q) ⟹ lrule_ok SG C i j EquivBackwardL"

named_theorems prover "Simplification rules for checking validity of proof certificates" 
lemmas [prover] = axiom_defs Box_def Or_def Implies_def filter_append ssafe_def SDom_def FUadmit_def PFUadmit_def id_simps

inductive_simps 
    Lrule_And[prover]: "lrule_ok SG C i j AndL"
and Lrule_Imply[prover]: "lrule_ok SG C i j ImplyL"
and Lrule_Forward[prover]: "lrule_ok SG C i j EquivForwardL"
and Lrule_EquivBackward[prover]: "lrule_ok SG C i j EquivBackwardL"

inductive rrule_ok ::"('sf,'sc,'sz) sequent list ⇒ ('sf,'sc,'sz) sequent ⇒ nat ⇒ nat ⇒ rrule ⇒ bool"
where
  Rrule_And:"⋀p q. nth (snd (nth SG i)) j = (p && q) ⟹ rrule_ok SG C i j AndR"
| Rrule_Imply:"⋀p q. nth (snd (nth SG i)) j = (p → q) ⟹ rrule_ok SG C i j ImplyR"
| Rrule_Equiv:"⋀p q. nth (snd (nth SG i)) j = (p ↔ q) ⟹ rrule_ok SG C i j EquivR"
| Rrule_Cohide:"length (snd (nth SG i)) > j ⟹ (⋀Γ q. (nth SG i) ≠ (Γ, [q])) ⟹ rrule_ok SG C i j CohideR"
| Rrule_CohideRR:"length (snd (nth SG i)) > j  ⟹ (⋀q. (nth SG i) ≠ ([], [q])) ⟹ rrule_ok SG C i j CohideRR"
| Rrule_True:"nth (snd (nth SG i)) j = TT ⟹ rrule_ok SG C i j TrueR"
  
inductive_simps 
    Rrule_And_simps[prover]: "rrule_ok SG C i j AndR"
and Rrule_Imply_simps[prover]: "rrule_ok SG C i j ImplyR"
and Rrule_Equiv_simps[prover]: "rrule_ok SG C i j EquivR"
and Rrule_CohideR_simps[prover]: "rrule_ok SG C i j CohideR"
and Rrule_CohideRR_simps[prover]: "rrule_ok SG C i j CohideRR"
and Rrule_TrueR_simps[prover]: "rrule_ok SG C i j TrueR"

inductive step_ok  :: "('sf, 'sc, 'sz) rule ⇒ nat ⇒ ('sf, 'sc, 'sz) step ⇒ bool"
where
  Step_Axiom:"(nth SG i) = ([], [get_axiom a]) ⟹ step_ok (SG,C) i (Axiom a)"
| Step_AxSubst:"(nth SG i) = ([], [Fsubst (get_axiom a) σ]) ⟹ Fadmit σ (get_axiom a) ⟹ ssafe σ ⟹ step_ok (SG,C) i (AxSubst a σ)"
| Step_Lrule:"lrule_ok SG C i j L ⟹ j < length (fst (nth SG i)) ⟹ step_ok (SG,C) i (Lrule L j)"
| Step_Rrule:"rrule_ok SG C i j L ⟹ j < length (snd (nth SG i)) ⟹ step_ok (SG,C) i (Rrule L j)"
| Step_Cut:"fsafe φ ⟹ i < length SG ⟹ step_ok (SG,C) i (Cut φ)"
| Step_CloseId:"nth (fst (nth SG i)) j = nth (snd (nth SG i)) k ⟹ j < length (fst (nth SG i)) ⟹ k < length (snd (nth SG i)) ⟹ step_ok (SG,C) i (CloseId j k) "
| Step_G:"⋀a p. nth SG i = ([], [([[a]]p)]) ⟹ step_ok (SG,C) i G"
| Step_DEAxiom_schema:
  " nth SG i = 
  ([], [Fsubst ((([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1)) ODE) (p1 vid2 vid1)]] (P pid1)) ↔
          ([[EvolveODE ((OProd  (OSing vid1 (f1 fid1 vid1))) ODE) (p1 vid2 vid1)]]
               [[DiffAssign vid1 (f1 fid1 vid1)]]P pid1))) σ])
    ⟹ ssafe σ
    ⟹ osafe ODE
    ⟹ {Inl vid1, Inr vid1} ∩ BVO ODE = {}
    ⟹ Fadmit σ ((([[EvolveODE (OProd  (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]] (P pid1)) ↔
          ([[EvolveODE ((OProd  (OSing vid1 (f1 fid1 vid1))ODE)) (p1 vid2 vid1)]]
               [[DiffAssign vid1 (f1 fid1 vid1)]]P pid1))) 
    ⟹ step_ok (SG,C) i (DEAxiomSchema ODE σ)"
| Step_CE:"nth SG i = ([], [Fsubst (Equiv (InContext pid1 φ) (InContext pid1 ψ)) σ]) 
    ⟹ valid (Equiv φ ψ) 
    ⟹ fsafe φ
    ⟹ fsafe ψ
    ⟹ ssafe σ
    ⟹ Fadmit σ (Equiv (InContext pid1 φ) (InContext pid1 ψ))
    ⟹ step_ok (SG,C) i (CE φ ψ σ)"
| Step_CQ:"nth SG i = ([], [Fsubst (Equiv (Prop p (singleton θ)) (Prop p (singleton θ'))) σ]) 
    ⟹ valid (Equals θ θ') 
    ⟹ dsafe θ
    ⟹ dsafe θ'
    ⟹ ssafe σ
    ⟹ Fadmit σ (Equiv (Prop p (singleton θ)) (Prop p (singleton θ')))
    ⟹ step_ok (SG,C) i (CQ θ θ' σ)"  
  
inductive_simps 
    Step_G_simps[prover]: "step_ok (SG,C) i G"
and Step_CloseId_simps[prover]: "step_ok (SG,C) i (CloseId j k)"
and Step_Cut_simps[prover]: "step_ok (SG,C) i (Cut φ)"
and Step_Rrule_simps[prover]: "step_ok (SG,C) i (Rrule j L)"
and Step_Lrule_simps[prover]: "step_ok (SG,C) i (Lrule j L)"
and Step_Axiom_simps[prover]: "step_ok (SG,C) i (Axiom a)"
and Step_AxSubst_simps[prover]: "step_ok (SG,C) i (AxSubst a σ)"
and Step_DEAxiom_schema_simps[prover]: "step_ok (SG,C) i (DEAxiomSchema ODE σ)"
and Step_CE_simps[prover]: "step_ok (SG,C) i (CE φ ψ σ)"
and Step_CQ_simps[prover]: "step_ok (SG,C) i (CQ θ θ' σ)"

inductive deriv_ok :: "('sf, 'sc, 'sz) rule ⇒ ('sf, 'sc, 'sz) derivation ⇒ bool"
where 
  Deriv_Nil:"deriv_ok R Nil"
| Deriv_Cons:"step_ok R i S ⟹ i ≥ 0 ⟹ i < length (fst R) ⟹ deriv_ok (step_result R (i,S)) SS ⟹ deriv_ok R ((i,S) # SS)"
  
inductive_simps 
    Deriv_nil_simps[prover]: "deriv_ok R Nil"
and Deriv_cons_simps[prover]: "deriv_ok R ((i,S)#SS)"

inductive proof_ok :: "('sf, 'sc, 'sz) pf ⇒ bool"
where
  Proof_ok:"deriv_ok (start_proof D) S ⟹ proof_ok (D,S)"

inductive_simps Proof_ok_simps[prover]: "proof_ok (D,S)"

subsection ‹Soundness›

named_theorems member_intros "Prove that stuff is in lists"

lemma mem_sing[member_intros]:"⋀x. List.member [x] x"
  by(auto simp add: member_rec)

lemma mem_appR[member_intros]:"⋀A B x. List.member B x ⟹ List.member (A @ B) x"
  subgoal for A by(induction A, auto simp add: member_rec) done

lemma mem_filter[member_intros]:"⋀A P x. P x ⟹ List.member A x ⟹ List.member (filter P A) x"
  subgoal for A
    by(induction A, auto simp add: member_rec)
  done

lemma sound_weaken_appL:"⋀SG SGS C. sound (SGS, C) ⟹ sound (SG @ SGS, C)"
  subgoal for SG SGS C
    apply(rule sound_weaken_gen)
     apply(auto)
    unfolding sublist_def apply(rule allI)
    subgoal for x
      using mem_appR[of SGS x SG] by auto
    done
  done

lemma fml_seq_valid:"valid φ ⟹ seq_valid ([], [φ])"
  unfolding seq_valid_def valid_def by auto

lemma closeI_provable_sound:"⋀i. sound (SG, C) ⟹ sound (closeI SG i, (nth SG i)) ⟹ sound (closeI SG i, C)"
  using close_provable_sound by auto

lemma valid_to_sound:"seq_valid A ⟹ sound (B, A)"
  unfolding seq_valid_def sound_def by auto

lemma closeI_valid_sound:"⋀i. sound (SG, C) ⟹ seq_valid (nth SG i) ⟹ sound (closeI SG i, C)"
  using valid_to_sound closeI_provable_sound by auto
  
lemma close_nonmember_eq:"¬(List.member A a) ⟹ close A a = A"
  by (induction A, auto simp add: member_rec)

lemma close_noneq_nonempty:"List.member A x ⟹ x ≠ a ⟹ close A a ≠ []"
  by(induction A, auto simp add: member_rec)

lemma close_app_neq:"List.member A x ⟹ x ≠ a ⟹ close (A @ B) a ≠ B" 
  using append_self_conv2[of "close A a" "close B a"] append_self_conv2[of "close A a" "B"] close_app_comm[of A B a] close_noneq_nonempty[of A x a]
  apply(cases "close B a = B")
   apply (auto)
  by (metis (no_types, lifting) filter_True filter_append mem_Collect_eq set_filter)
  
lemma member_singD:"⋀x P. P x ⟹ (⋀y. List.member [x] y ⟹ P y)"
  by (metis member_rec(1) member_rec(2))

lemma fst_neq:"A ≠ B ⟹ (A,C) ≠ (B,D)"
  by auto
  
lemma lrule_sound: "lrule_ok SG C i j L ⟹ i < length SG ⟹ j < length (fst (SG ! i)) ⟹ sound (SG,C) ⟹ sound (close (append SG (Lrule_result L j (nth SG i))) (nth SG i), C)"
proof(induction rule: lrule_ok.induct)
  case (Lrule_And SG i j C p q)
  assume eq:"fst (SG ! i) ! j = (p && q)"
  assume sound:"sound (SG, C)"
  obtain AI and SI where SG_dec:"(AI,SI) = (SG ! i)"
    by (metis seq2fml.cases)
  have AIjeq:"AI ! j = (p && q)" using SG_dec eq
    by (metis fst_conv)
  have sub:"sublist [(close ([p, q] @ AI) (p && q),SI)] ([y←SG . y ≠ (AI, SI)] @ [y← [(close (p # q # AI) (p && q), SI)] . y ≠ (AI, SI)])"
    apply (rule sublistI)
    using member_singD [of "λy. List.member ([y←SG . y ≠ (AI, SI)] @ [y← [(close ([p, q] @ AI) (p && q), SI)] . y ≠ (AI, SI)]) y" "(close ([p, q] @ AI) (p && q),SI)"]
    using close_app_neq[of "[p, q]" p "p && q" AI] 
    by(auto intro: member_intros fst_neq simp add: member_rec expr_diseq)
  have cool:"sound ([y←SG . y ≠ (AI, SI)] @ [y← [(close (p # q # AI) (p && q), SI)] . y ≠ (AI, SI)], AI, SI)"
    apply(rule sound_weaken_gen[OF sub] )
    apply(auto simp add: member_rec expr_diseq)
    unfolding seq_valid_def
  proof (rule soundI_mem)
    fix I::"('sf,'sc,'sz) interp"
    assume good:"is_interp I"
    assume sgs:"(⋀φ. List.member [(p # q # [y←AI . y ≠ (p && q)], SI)] φ ⟹ seq_sem I φ = UNIV)"
    have theSg:"seq_sem I (p # q # [y←AI . y ≠ (p && q)], SI) = UNIV"
      apply(rule sgs)
      by(auto intro: member_intros)
    then have sgIn:"⋀ν. ν ∈ seq_sem I ((p && q) # [y←AI . y ≠ (p && q)], SI)"
      by auto
    { fix ν
      assume sem:"ν ∈ seq_sem I ((p && q) # [y←AI . y ≠ (p && q)], SI)"
      have mem_eq:"⋀x. List.member ((p && q) # [y←AI . y ≠ (p && q)]) x = List.member AI x"
        by (metis (mono_tags, lifting) Lrule_And.prems(2) SG_dec eq fst_conv local.member_filter mem_filter member_rec(1) nth_member)
      have myeq:"ν ∈ seq_sem I ((p && q) # [y←AI . y ≠ (p && q)], SI) ⟹  ν ∈ seq_sem I (AI, SI)"
        using and_foldl_sem and_foldl_sem_conv seq_semI Lrule_And.prems(2) SG_dec eq  seq_MP seq_semI' mem_eq
        by (metis (no_types, lifting))
      have "ν ∈ seq_sem I ((p && q) # [y←AI . y ≠ (p && q)], SI)"
        using sem by auto
      then have "ν ∈ seq_sem I ((p && q) # [y←AI . y ≠ (p && q)], SI)"
        by blast
      then have "ν ∈ seq_sem I (AI, SI)"
        using myeq by auto}
      then show "seq_sem I (AI, SI) = UNIV"
        using sgIn by blast
    qed
  have res_sound:"sound ([y←SG . y ≠ (AI,SI)] @ [y←Lrule_result AndL j (AI,SI) . y ≠ (AI,SI)],(AI,SI))"
    apply (simp)
    using cool AIjeq by auto
 show "?case"
  apply(rule close_provable_sound)
   apply(rule sound_weaken_appR)
   apply(rule sound)
  using res_sound SG_dec by auto
next
  case (Lrule_Imply SG i j C p q)
  have implyL_simp:"⋀AI SI SS p q. 
    (nth AI  j) = (Not (And (Not q) (Not (Not p)))) ⟹ 
    (AI,SI) = SS ⟹ 
    Lrule_result ImplyL j SS = [(close (q # AI) (nth AI j), SI), (close AI (nth AI j), p # SI)]"
    subgoal for AI SI SS p q apply(cases SS) by auto done
  assume eq:"fst (SG ! i) ! j = (p → q)"
  assume iL:"i < length SG"
  assume jL:"j < length (fst (SG ! i))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have res_eq:"Lrule_result ImplyL j (SG ! i) = 
    [(close (q # Γ) (nth Γ j), Δ), 
     (close Γ (nth Γ j), p # Δ)]"
    apply(rule implyL_simp)
    using SG_dec eq Implies_def Or_def 
    by (metis fstI)+
  have AIjeq:"Γ ! j = (p → q)" 
    using SG_dec eq unfolding Implies_def Or_def
    by (metis fst_conv)
  have big_sound:"sound ([(close (q # Γ) (p → q), Δ), (close Γ (p → q), p # Δ)], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good:"is_interp I"
    assume sgs:"(⋀i. 0 ≤ i ⟹
             i < length [(close (q # Γ) (p → q), Δ), (close Γ (p → q), p # Δ)] ⟹
             ν ∈ seq_sem I ([(close (q # Γ) (p → q), Δ), (close Γ (p → q), p # Δ)] ! i))"
    have sg1:"ν ∈ seq_sem I (close (q # Γ) (p → q), Δ)" using sgs[of 0] by auto
    have sg2:"ν ∈ seq_sem I (close Γ (p → q), p # Δ)" using sgs[of "Suc 0"] by auto
    assume Γ:"ν ∈ fml_sem I (foldr And Γ TT)"
    have Γ_proj:"⋀φ Γ. List.member Γ φ ⟹ ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I φ"
      apply(induction Γ, auto simp add: member_rec)
      using and_foldl_sem by blast
    have imp:"ν ∈ fml_sem I (p → q)" 
      apply(rule Γ_proj[of Γ])
      using AIjeq  jL SG_dec nth_member
      apply (metis fst_conv)
      by (rule Γ)
    have sub:"sublist (close Γ (p → q)) Γ"
      by (rule close_sub)
    have ΓC:"ν ∈ fml_sem I (foldr And (close Γ (p → q)) TT)"
      by (rule Γ_sub_sem[OF sub Γ])
    have "ν ∈ fml_sem I (foldr (||) (p # Δ) FF)"
      by(rule seq_MP[OF sg2 ΓC])
    then have disj:"ν ∈ fml_sem I p ∨ ν ∈ fml_sem I (foldr (||) Δ FF)"
      by auto 
    { assume p:"ν ∈ fml_sem I p"
      have q:"ν ∈ fml_sem I q" using p imp by simp
      have res: "ν ∈ fml_sem I (foldr (||) Δ FF)" 
        using disj Γ seq_semI
        proof -
          have "ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)"
            using Γ q by auto
          then show ?thesis
            by (meson Γ_sub_sem close_sub seq_MP sg1)
        qed
      have conj:"ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)"
        using q Γ by auto
      have conj:"ν ∈ fml_sem I (foldr (&&) (close (q # Γ) (p → q)) TT)"
        apply(rule Γ_sub_sem)
        defer
        apply(rule conj)
        by(rule close_sub)
      have Δ1:"ν ∈ fml_sem I (foldr (||) Δ FF)"
        by(rule seq_MP[OF sg1 conj])
      }
    then show "ν ∈ fml_sem I (foldr (||) Δ FF)"
      using disj by auto
    qed
    have neq1:"close ([q] @ Γ) (p → q) ≠ Γ"
      apply(rule close_app_neq)
       apply(rule mem_sing)
      by (auto simp add: expr_diseq)
    have neq2:"p # Δ ≠ Δ"
      by(induction p, auto)
    have close_eq:"close [(close (q # Γ) (p → q), Δ), (close Γ (p → q), p # Δ)] (Γ,Δ) = [(close (q # Γ) (p → q), Δ), (close Γ (p → q), p # Δ)]"
      apply(rule close_nonmember_eq)
      apply auto
       using neq1 neq2  
       apply (simp add: member_rec)
    proof -
      assume a1: "q = (p → q)"
      assume "List.member [([y←Γ . y ≠ q], Δ), ([y←Γ . y ≠ q], p # Δ)] (Γ, Δ)"
        then have "[f←Γ . f ≠ q] = Γ"
      by (simp add: member_rec)
      then show False
        using a1 neq1 by fastforce
    qed       
  show ?case 
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    apply(unfold res_eq)
    apply(unfold AIjeq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using close_eq big_sound SG_dec   
    by simp
next
  case (Lrule_EquivBackward SG i j C p q)
  have equivLBackward_simp:"⋀AI SI SS p q. 
    (nth AI  j) = Not (And (Not (And p q)) (Not (And (Not p) (Not q)))) ⟹ 
    (AI,SI) = SS ⟹ 
    Lrule_result EquivBackwardL j SS = [(close (p # AI) (nth AI j), SI), (close AI (nth AI j), q # SI)]"
    subgoal for AI SI SS p q apply(cases SS) by auto done
  assume eq:"fst (SG ! i) ! j = (p ↔ q)"
  assume iL:"i < length SG"
  assume jL:"j < length (fst (SG ! i))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have res_eq:"Lrule_result EquivBackwardL j (SG ! i) = 
    [(close (p # Γ) (nth Γ j), Δ), 
     (close Γ (nth Γ j), q # Δ)]"
    apply(rule equivLBackward_simp)
     using SG_dec eq Equiv_def Or_def 
     by (metis fstI)+
  have AIjeq:"Γ ! j = (p ↔ q)" 
    using SG_dec eq unfolding Implies_def Or_def
    by (metis fst_conv)
  have big_sound:"sound ([(close (p # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), q # Δ)], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good:"is_interp I"
    assume sgs:"(⋀i. 0 ≤ i ⟹
             i < length [(close (p # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), q # Δ)] ⟹
             ν ∈ seq_sem I ([(close (p # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), q # Δ)] ! i))"
    have sg1:"ν ∈ seq_sem I (close (p # Γ) (p ↔ q), Δ)" using sgs[of 0] by auto
    have sg2:"ν ∈ seq_sem I (close Γ (p ↔ q), q # Δ)" using sgs[of "Suc 0"] by auto 
    assume Γ:"ν ∈ fml_sem I (foldr And Γ TT)"
    have Γ_proj:"⋀φ Γ. List.member Γ φ ⟹ ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I φ"
      apply(induction Γ, auto simp add: member_rec)
      using and_foldl_sem by blast
    have imp:"ν ∈ fml_sem I (p ↔ q)" 
      apply(rule Γ_proj[of Γ])
      using AIjeq  jL SG_dec nth_member
      apply (metis fst_conv)
      by (rule Γ)
    have sub:"sublist (close Γ (p → q)) Γ"
      by (rule close_sub)
    have ΓC:"ν ∈ fml_sem I (foldr And (close Γ (p → q)) TT)"
      by (rule Γ_sub_sem[OF sub Γ])
    have "ν ∈ fml_sem I (foldr (||) (p # Δ) FF)"
      by (metis Γ Γ_sub_sem close_sub iff_sem imp member_rec(1) or_foldl_sem or_foldl_sem_conv seq_MP sg2)
    then have disj:"ν ∈ fml_sem I p ∨ ν ∈ fml_sem I (foldr (||) Δ FF)"
      by auto 
    { assume p:"ν ∈ fml_sem I p"
      have q:"ν ∈ fml_sem I q" using p imp by simp
      have res: "ν ∈ fml_sem I (foldr (||) Δ FF)" 
        using disj Γ seq_semI
        proof -
          have "ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)"
            using Γ q by auto
          then show ?thesis
            proof -
              have "∀fs p i. (∃f. List.member fs (f::('sf, 'sc, 'sz) formula) ∧ p ∉ fml_sem i f) ∨ p ∈ fml_sem i (foldr (&&) fs TT)"
                using and_foldl_sem_conv by blast
              then obtain ff :: "('sf, 'sc, 'sz) formula list ⇒ (real, 'sz) vec × (real, 'sz) vec ⇒ ('sf, 'sc, 'sz) interp ⇒ ('sf, 'sc, 'sz) formula" where
                f1: "∀fs p i. List.member fs (ff fs p i) ∧ p ∉ fml_sem i (ff fs p i) ∨ p ∈ fml_sem i (foldr (&&) fs TT)"
                by metis
              have "⋀f. ν ∈ fml_sem I f ∨ ¬ List.member Γ f"
                by (meson ‹ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)› and_foldl_sem member_rec(1))
              then have "ν ∈ fml_sem I (foldr (&&) (close (p # Γ) (p ↔ q)) TT)"
                using f1 by (metis (no_types) close_sub local.sublist_def member_rec(1) p)
              then show ?thesis
                using seq_MP sg1 by blast
            qed
        qed
      have conj:"ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)"
        using q Γ by auto
      have conj:"ν ∈ fml_sem I (foldr (&&) (close (q # Γ) (p → q)) TT)"
        apply(rule Γ_sub_sem)
        defer
        apply(rule conj)
        by(rule close_sub)
      have Δ1:"ν ∈ fml_sem I (foldr (||) Δ FF)"
        using res by blast
      }
    then show "ν ∈ fml_sem I (foldr (||) Δ FF)"
      using disj by auto
  qed
  have neq1:"close ([q] @ Γ) (p ↔ q) ≠ Γ"
    apply(rule close_app_neq)
     apply(rule mem_sing)
    by (auto simp add: expr_diseq)
  have neq2:"p # Δ ≠ Δ"
    by(induction p, auto)                 
  have close_eq:"close [(close (p # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), q # Δ)] (Γ,Δ) = [(close (p # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), q # Δ)]"
    apply(rule close_nonmember_eq)
    apply auto
     using neq1 neq2  
     apply (simp add: member_rec)
     apply (metis append_Cons append_Nil close.simps close_app_neq member_rec(1))
    proof -
       assume a1:"p = (p ↔ q)"
       then show False
         by (simp add: expr_diseq)
    qed
  show ?case 
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    apply(unfold res_eq)
    apply(unfold AIjeq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using close_eq big_sound SG_dec   
    by simp
next
  case (Lrule_EquivForward SG i j C p q)
  have equivLForward_simp:"⋀AI SI SS p q. 
    (nth AI  j) = Not (And (Not (And p q)) (Not (And (Not p) (Not q)))) ⟹ 
    (AI,SI) = SS ⟹ 
    Lrule_result EquivForwardL j SS = [(close (q # AI) (nth AI j), SI), (close AI (nth AI j), p # SI)]"
    subgoal for AI SI SS p q apply(cases SS) by auto done
  assume eq:"fst (SG ! i) ! j = (p ↔ q)"
  assume iL:"i < length SG"
  assume jL:"j < length (fst (SG ! i))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have res_eq:"Lrule_result EquivForwardL j (SG ! i) = 
    [(close (q # Γ) (nth Γ j), Δ), 
     (close Γ (nth Γ j), p # Δ)]"
    apply(rule equivLForward_simp)
    using SG_dec eq Equiv_def Or_def 
    by (metis fstI)+
  have AIjeq:"Γ ! j = (p ↔ q)" 
    using SG_dec eq unfolding Implies_def Or_def
    by (metis fst_conv)
  have big_sound:"sound ([(close (q # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), p # Δ)], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good:"is_interp I"
    assume sgs:"(⋀i. 0 ≤ i ⟹
             i < length [(close (q # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), p # Δ)] ⟹
             ν ∈ seq_sem I ([(close (q # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), p # Δ)] ! i))"
    have sg1:"ν ∈ seq_sem I (close (q # Γ) (p ↔ q), Δ)" using sgs[of 0] by auto
    have sg2:"ν ∈ seq_sem I (close Γ (p ↔ q), p # Δ)" using sgs[of "Suc 0"] by auto 
    assume Γ:"ν ∈ fml_sem I (foldr And Γ TT)"
    have Γ_proj:"⋀φ Γ. List.member Γ φ ⟹ ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I φ"
      apply(induction Γ, auto simp add: member_rec)
      using and_foldl_sem by blast
    have imp:"ν ∈ fml_sem I (p ↔ q)" 
      apply(rule Γ_proj[of Γ])
       using AIjeq  jL SG_dec nth_member
       apply (metis fst_conv)
      by (rule Γ)
    have sub:"sublist (close Γ (p → q)) Γ"
      by (rule close_sub)
    have ΓC:"ν ∈ fml_sem I (foldr And (close Γ (p → q)) TT)"
      by (rule Γ_sub_sem[OF sub Γ])
    have "ν ∈ fml_sem I (foldr (||) (p # Δ) FF)"
      by (metis Γ Γ_sub_sem close_sub iff_sem imp member_rec(1) or_foldl_sem or_foldl_sem_conv seq_MP sg2)
    then have disj:"ν ∈ fml_sem I p ∨ ν ∈ fml_sem I (foldr (||) Δ FF)"
      by auto 
    { assume p:"ν ∈ fml_sem I p"
      have q:"ν ∈ fml_sem I q" using p imp by simp
      have res: "ν ∈ fml_sem I (foldr (||) Δ FF)" 
        using disj Γ seq_semI
        proof -
          have "ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)"
            using Γ q by auto
          then show ?thesis
            by (meson ‹ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)› and_foldl_sem and_foldl_sem_conv close_sub local.sublist_def seq_MP sg1)
        qed
      have conj:"ν ∈ fml_sem I (foldr (&&) (q # Γ) TT)"
        using q Γ by auto
      have conj:"ν ∈ fml_sem I (foldr (&&) (close (q # Γ) (p → q)) TT)"
        apply(rule Γ_sub_sem)
        defer
        apply(rule conj)
        by(rule close_sub)
      have Δ1:"ν ∈ fml_sem I (foldr (||) Δ FF)"
        using res by blast
      }
    then show "ν ∈ fml_sem I (foldr (||) Δ FF)"
      using disj by auto
  qed
  have neq1:"close ([q] @ Γ) (p ↔ q) ≠ Γ"
    apply(rule close_app_neq)
    apply(rule mem_sing)
    by (auto simp add: expr_diseq)
  have neq2:"p # Δ ≠ Δ"
    by(induction p, auto)
  have close_eq:"close [(close (q # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), p # Δ)] (Γ,Δ) = [(close (q # Γ) (p ↔ q), Δ), (close Γ (p ↔ q), p # Δ)]"
    apply(rule close_nonmember_eq)
    apply auto
     using neq1 neq2  
     apply (simp add: member_rec)
  proof -
     assume a1:"q = (p ↔ q)"
     then show False
       by (simp add: expr_diseq)
  qed
  show ?case 
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    apply(unfold res_eq)
    apply(unfold AIjeq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using close_eq big_sound SG_dec   
  by simp
qed

lemma rrule_sound: "rrule_ok SG C i j L ⟹ i < length SG ⟹ j < length (snd (SG ! i)) ⟹ sound (SG,C) ⟹ sound (close (append SG (Rrule_result L j (nth SG i))) (nth SG i), C)"
proof(induction rule: rrule_ok.induct)
  case (Rrule_And SG i j C p q)
  assume eq:"snd (SG ! i) ! j = (p && q)"
  assume "i < length SG"
  assume "j < length (snd (SG ! i))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have andR_simp:"⋀Γ Δ SS p q. 
    (nth Δ j) = And p q ⟹ 
    (Γ,Δ) = SS ⟹ 
    Rrule_result AndR j SS = [(Γ, p # (close Δ (nth Δ j))), (Γ, q # (close Δ (nth Δ j)))]"
    subgoal for AI SI SS p q apply(cases SS) by auto done
  have res_eq:"Rrule_result AndR j (SG ! i) = 
    [(Γ, p # (close Δ (nth Δ j))), (Γ, q # (close Δ (nth Δ j)))]"
    using SG_dec andR_simp apply auto
    using SG_dec eq Implies_def Or_def
    using fstI
    by (metis andR_simp close.simps snd_conv)
  have AIjeq:"Δ ! j = (p && q)" 
    using SG_dec eq snd_conv
    by metis
  have big_sound:"sound ([(Γ, p # (close Δ (nth Δ j))), (Γ, q # (close Δ (nth Δ j)))], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν
    assume good:"is_interp I"
    assume sgs:"(⋀i. 0 ≤ i ⟹
             i < length [(Γ, p # close Δ (nth Δ  j)), (Γ, q # close Δ (nth Δ  j))] ⟹
             ν ∈ seq_sem I (nth [(Γ, p # close Δ (nth Δ  j)), (Γ, q # close Δ (nth Δ j))] i))"
    assume Γ_sem:"ν ∈ fml_sem I (foldr (&&) Γ TT)"
    have sg1:"ν ∈ seq_sem I (Γ, p # close Δ (nth Δ j))" using sgs[of 0] by auto
    have sg2:"ν ∈ seq_sem I (Γ, q # close Δ (nth Δ j))" using sgs[of 1] by auto
    have Δ1:"ν ∈ fml_sem I (foldr (||) (p # close Δ (nth Δ j)) FF)"
      by(rule seq_MP[OF sg1 Γ_sem])
    have Δ2:"ν ∈ fml_sem I (foldr (||) (q # close Δ (nth Δ j)) FF)"
      by(rule seq_MP[OF sg2 Γ_sem])
    have Δ':"ν ∈ fml_sem I (foldr (||) ((p && q) # close Δ (nth Δ j)) FF)"
      using Δ1 Δ2 by auto
    have mem_eq:"⋀x. List.member ((p && q) # close Δ (nth Δ j)) x ⟹ List.member Δ x"
      using Rrule_And.prems SG_dec eq  member_rec(1) nth_member
      by (metis close_sub local.sublist_def snd_conv)
    have myeq:"ν ∈ fml_sem I (foldr (||) ((p && q) # close Δ (nth Δ j)) FF) ⟹  ν ∈ fml_sem I (foldr (||) Δ FF)"
        using  seq_semI Rrule_And.prems SG_dec eq  seq_MP seq_semI' mem_eq
        or_foldl_sem or_foldl_sem_conv
        by metis
    then show "ν ∈ fml_sem I (foldr (||) Δ FF)"
      using Δ' by auto  
  qed
  have list_neqI1:"⋀L1 L2 x. List.member L1 x ⟹ ¬(List.member L2 x) ⟹ L1 ≠ L2"
    by(auto)
  have list_neqI2:"⋀L1 L2 x. ¬(List.member L1 x) ⟹ (List.member L2 x) ⟹ L1 ≠ L2"
    by(auto)
  have notin_cons:"⋀x y ys. x ≠ y ⟹ ¬(List.member ys x) ⟹ ¬(List.member (y # ys) x)"
    subgoal for x y ys
      by(induction ys, auto simp add: member_rec)
    done
  have notin_close:"⋀L x. ¬(List.member (close L x) x)"
    subgoal for L x
      by(induction L, auto simp add: member_rec)
    done
  have neq_lemma:"⋀L x y. List.member L x ⟹ y ≠ x ⟹ (y # (close L x)) ≠ L"
    subgoal for L x y
      apply(cases "List.member L y")
       subgoal
         apply(rule list_neqI2[of "y # close L x" x])
          apply(rule notin_cons)
           defer
           apply(rule notin_close)
          by(auto)
      subgoal
        apply(rule list_neqI2[of "y # close L x" x])
         apply(rule notin_cons)
          defer
          apply(rule notin_close)
         by(auto)
      done
    done
  have neq1:"p # close Δ (p && q) ≠ Δ"
    apply(rule neq_lemma)
     apply (metis Rrule_And.prems(2) SG_dec eq nth_member sndI)
    by(auto simp add: expr_diseq) 
  have neq2:"q # close Δ (p && q) ≠ Δ"
    apply(rule neq_lemma)
     apply (metis Rrule_And.prems(2) SG_dec eq nth_member sndI)
    by(auto simp add: expr_diseq)
  have close_eq:"close [(Γ, p # close Δ (p && q)), (Γ, q # close Δ (p && q))] (Γ,Δ) = [(Γ, p # close Δ (p && q)), (Γ, q # close Δ (p && q))]"
    apply(rule close_nonmember_eq)
    apply auto
    using neq1 neq2  
    by (simp add: member_rec)
  show " sound (close (SG @ Rrule_result AndR j (SG ! i)) (SG ! i), C)" 
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    apply(unfold res_eq)
    apply(unfold AIjeq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using close_eq big_sound SG_dec   
    by (simp add: AIjeq)
next
  case (Rrule_Imply SG i j C p q)
  assume eq:"snd (SG ! i) ! j = (p → q)"
  assume "i < length SG"
  assume "j < length (snd (SG ! i))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have impR_simp:"⋀Γ Δ SS p q. 
    (nth Δ j) = Implies p q ⟹ 
    (Γ,Δ) = SS ⟹ 
    Rrule_result ImplyR j SS = [(p # Γ, q # (close Δ (nth Δ j)))]"
    subgoal for AI SI SS p q apply(cases SS) by (auto simp add: Implies_def Or_def) done
  have res_eq:"Rrule_result ImplyR j (SG ! i) = 
    [(p # Γ, q # (close Δ (nth Δ j)))]"
    using SG_dec impR_simp apply auto
    using SG_dec eq Implies_def Or_def
    using fstI
    by (metis impR_simp close.simps snd_conv)
  have AIjeq:"Δ ! j = (p → q)" 
    using SG_dec eq snd_conv
    by metis
  have close_eq:"close [(p # Γ, q # (close Δ (nth Δ j)))] (Γ,Δ) = [(p # Γ, q # (close Δ (nth Δ j)))]"
    apply(rule close_nonmember_eq)
    by (simp add: member_rec)
  have big_sound:"sound ([(p # Γ, q # close Δ (Δ ! j))], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
  proof -
    fix I ::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume "is_interp I"
    assume sgs:"(⋀i. 0 ≤ i ⟹ i < length [(p # Γ, q # close Δ (Δ ! j))] ⟹ ν ∈ seq_sem I ([(p # Γ, q # close Δ (Δ ! j))] ! i))"
      have sg:"ν ∈ seq_sem I (p # Γ, q # close Δ (Δ ! j))" using sgs[of 0] by auto
    assume Γ_sem:"ν ∈ fml_sem I (foldr (&&) Γ TT)"
    show "ν ∈ fml_sem I (foldr (||) Δ FF)"
      using Γ_sem sg 
        AIjeq Rrule_Imply.prems(2) SG_dec and_foldl_sem_conv close_sub impl_sem local.sublist_def member_rec(1) nth_member or_foldl_sem_conv seq_MP seq_semI snd_conv
        Γ_sub_sem and_foldl_sem or_foldl_sem seq_sem.simps sublistI
    proof -
      have f1: "∀fs p i. ∃f. (p ∈ fml_sem i (foldr (&&) fs (TT::('sf, 'sc, 'sz) formula)) ∨ List.member fs f) ∧ (p ∉ fml_sem i f ∨ p ∈ fml_sem i (foldr (&&) fs TT))"
        using and_foldl_sem_conv by blast
      have "∀p i fs. ∃f. ∀pa ia fa fb pb ib fc fd. p ∈ fml_sem i (f::('sf, 'sc, 'sz) formula) ∧ (pa ∈ fml_sem ia (fa::('sf, 'sc, 'sz) formula) ∨ pa ∈ fml_sem ia (fa → fb)) ∧ (pb ∉ fml_sem ib (fc::('sf, 'sc, 'sz) formula) ∨ pb ∈ fml_sem ib (fd → fc)) ∧ (p ∉ fml_sem i (foldr (||) fs FF) ∨ List.member fs f)"
        by (metis impl_sem or_foldl_sem_conv)
      then obtain ff :: "(real, 'sz) vec × (real, 'sz) vec ⇒ ('sf, 'sc, 'sz) interp ⇒ ('sf, 'sc, 'sz) formula list ⇒ ('sf, 'sc, 'sz) formula" where
        f2: "⋀p i fs pa ia f fa pb ib fb fc. p ∈ fml_sem i (ff p i fs) ∧ (pa ∈ fml_sem ia (f::('sf, 'sc, 'sz) formula) ∨ pa ∈ fml_sem ia (f → fa)) ∧ (pb ∉ fml_sem ib (fb::('sf, 'sc, 'sz) formula) ∨ pb ∈ fml_sem ib (fc → fb)) ∧ (p ∉ fml_sem i (foldr (||) fs FF) ∨ List.member fs (ff p i fs))"
        by metis
      then have "⋀fs. ν ∉ fml_sem I (foldr (&&) (p # Γ) TT) ∨ ¬ local.sublist (close Δ (p → q)) fs ∨ ff ν I (q # close Δ (p → q)) = q ∨ List.member fs (ff ν I (q # close Δ (p → q)))"
        by (metis (no_types) AIjeq local.sublist_def member_rec(1) seq_MP sg)
      then have "∃f. List.member Δ f ∧ ν ∈ fml_sem I f"
        using f2 f1 by (metis (no_types) AIjeq Rrule_Imply.prems(2) SG_dec Γ_sem and_foldl_sem close_sub member_rec(1) nth_member snd_conv)
      then show ?thesis
        using or_foldl_sem by blast
    qed
  qed
  show ?case
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    using res_eq
    apply(unfold res_eq)
    apply(unfold AIjeq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using close_eq big_sound SG_dec AIjeq
    by (simp add: AIjeq)
next
  case (Rrule_Cohide SG i j C)
  assume "i < length SG"
  assume "j < length (snd (SG ! i))"
  assume chg:"(⋀Γ q. (nth SG i) ≠ (Γ, [q]))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have cohideR_simp:"
    (Γ,Δ) = SS ⟹ 
    Rrule_result CohideR j SS = [(Γ, [nth Δ j])]" for Γ Δ SS p q
    by (cases SS, auto)
  have res_eq:"Rrule_result CohideR j (SG ! i) =  [(Γ, [nth Δ j])]"
    using SG_dec by (rule cohideR_simp)
  have close_eq:"close [(Γ, [nth Δ j])] (Γ,Δ) = [(Γ, [nth Δ j])]"
    using chg 
    by (metis SG_dec close_nonmember_eq member_rec(1) member_rec(2))
  have big_sound:"sound ([(Γ, [nth Δ j])], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
    by (metis (no_types, lifting) Rrule_Cohide.prems(2) SG_dec length_greater_0_conv less_or_eq_imp_le list.distinct(1) member_singD nth_Cons_0 nth_member or_foldl_sem or_foldl_sem_conv seq_MP snd_conv)
  show ?case
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    using res_eq
    apply(unfold res_eq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using big_sound SG_dec
    apply(cases "[nth Δ j] = Δ")
     apply(auto)
    using chg by (metis)+
next
  case (Rrule_CohideRR SG i j C)
  assume "i < length SG"
  assume "j < length (snd (SG ! i))"
  assume chg:"(⋀q. (nth SG i) ≠ ([], [q]))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have cohideRR_simp:" 
    (Γ,Δ) = SS ⟹ 
    Rrule_result CohideRR j SS = [([], [nth Δ j])]" for Γ Δ SS p q
    by (cases SS, auto)
  have res_eq:"Rrule_result CohideRR j (SG ! i) =  [([], [nth Δ j])]"
    using SG_dec by (rule cohideRR_simp)
  have close_eq:"close [([], [nth Δ j])] (Γ,Δ) = [([], [nth Δ j])]"
    using chg 
    by (metis SG_dec close_nonmember_eq member_rec(1) member_rec(2))
  have big_sound:"sound ([([], [nth Δ j])], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
    by (metis (no_types, lifting) Rrule_CohideRR.prems(2) SG_dec and_foldl_sem_conv length_greater_0_conv less_or_eq_imp_le list.distinct(1) member_rec(2) member_singD nth_Cons_0 nth_member or_foldl_sem or_foldl_sem_conv seq_MP snd_conv)
  show ?case
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    using res_eq
    apply(unfold res_eq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using big_sound SG_dec
    apply(cases "[nth Δ j] = Δ")
     apply(auto)
     using chg by (metis)+
next
  case (Rrule_True SG i j C)
  assume tt:"snd (SG ! i) ! j = TT"
  assume iL:"i < length SG"
  assume iJ:"j < length (snd (SG ! i))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have "⋀I ν. is_interp I ⟹ ν ∈ fml_sem I (foldr (||) Δ FF)"
    proof -
      fix I::"('sf,'sc,'sz)interp" and ν::"'sz state"
      assume good:"is_interp I"
      have mem2:"List.member Δ (Δ ! j)"
        using iJ nth_member 
        by (metis SG_dec snd_conv)
      then show "ν ∈ fml_sem I (foldr (||) Δ FF)"
        using mem2
        using or_foldl_sem 
        by (metis SG_dec UNIV_I snd_conv tt tt_sem)
    qed
  then have seq_valid:"seq_valid (SG ! i)"
    unfolding seq_valid_def using SG_dec
    by (metis UNIV_eq_I seq_semI')
  show ?case
    using closeI_valid_sound[OF sound seq_valid]
    by (simp add: sound_weaken_appR)
next
  case (Rrule_Equiv SG i j C p q)
  assume eq:"snd (SG ! i) ! j = (p ↔ q)"
  assume iL:"i < length SG"
  assume jL:"j < length (snd (SG ! i))"
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have equivR_simp:"⋀Γ Δ SS p q. 
    (nth Δ j) = Equiv p q ⟹ 
    (Γ,Δ) = SS ⟹ 
    Rrule_result EquivR j SS = [(p # Γ, q # (closeI Δ j)), (q # Γ, p # (closeI Δ j))]"
    subgoal for AI SI SS p q apply(cases SS) by (auto simp add: Equiv_def Implies_def Or_def) done
  have res_eq:"Rrule_result EquivR j (SG ! i) = 
    [(p # Γ, q # (closeI Δ j)), (q # Γ, p # (closeI Δ j))]"
    apply(rule equivR_simp)
    subgoal using eq SG_dec by (metis snd_conv)
    by (rule SG_dec) 
  have AIjeq:"Δ ! j = (p ↔ q)" 
    using SG_dec eq snd_conv
    by metis
  have close_eq:"close [(p # Γ, q # (closeI Δ j)), (q # Γ, p # (closeI Δ j))] (Γ,Δ) = [(p # Γ, q # (closeI Δ j)), (q # Γ, p # (closeI Δ j))]"
    apply(rule close_nonmember_eq)
    by (simp add: member_rec)
  have big_sound:"sound ([(p # Γ, q # (closeI Δ j)), (q # Γ, p # (closeI Δ j))], (Γ,Δ))"
    apply(rule soundI')
    apply(rule seq_semI')
  proof -
    fix I ::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good:"is_interp I"
    assume sgs:"(⋀i. 0 ≤ i ⟹ i < length [(p # Γ, q # (closeI Δ j)), (q # Γ, p # (closeI Δ j))] ⟹ ν ∈ seq_sem I ([(p # Γ, q # (closeI Δ j)), (q # Γ, p # (closeI Δ j))] ! i))"
    have sg1:"ν ∈ seq_sem I (p # Γ, q # close Δ (Δ ! j))" using sgs[of 0] by auto
    have sg2:"ν ∈ seq_sem I (q # Γ, p # (closeI Δ j))" using sgs[of 1] by auto
    assume Γ_sem:"ν ∈ fml_sem I (foldr (&&) Γ TT)"
    have case1:"ν ∈ fml_sem I p ⟹ ν ∈ fml_sem I (foldr (||) Δ FF)"
    proof -
      assume sem:"ν ∈ fml_sem I p"
      have "ν ∈ fml_sem I (foldr (||) (q # (close Δ (nth Δ j))) FF)"
        using sem Γ_sem sg1 by auto
      then show "ν ∈ fml_sem I (foldr (||) Δ FF)"
        using AIjeq SG_dec close_sub[of Δ "nth Δ j"] iff_sem[of "ν" I p q] jL local.sublist_def
        member_rec(1)[of q "close Δ (nth Δ j)"] sem snd_conv
        or_foldl_sem_conv[of ν I "q # close Δ (nth Δ j)"]
        or_foldl_sem[of "Δ", where I=I and ν=ν]
        nth_member[of j "snd (SG ! i)"]
        by metis
    qed
    have case2:"ν ∉ fml_sem I p ⟹ ν ∈ fml_sem I (foldr (||) Δ FF)"
    proof -
      assume sem:"ν ∉ fml_sem I p"
      have "ν ∈ fml_sem I q ⟹  ν ∉ fml_sem I (foldr (||) Δ FF) ⟹ False"
        using  
          and_foldl_sem[OF Γ_sem]
          and_foldl_sem_conv
          closeI.simps
          close_sub
          local.sublist_def
          member_rec(1)[of "p" "closeI Δ j"]
          member_rec(1)[of "q" "Γ"]
          or_foldl_sem[of "Δ"]
          or_foldl_sem_conv[of ν  I "p # closeI Δ j"]
          sem
          sg2
          seq_MP[of ν I "q # Γ" "p # closeI Δ j", OF sg2]
      proof -
        assume a1: "ν ∈ fml_sem I q"
        assume a2: "ν ∉ fml_sem I (foldr (||) Δ FF)"
        obtain ff :: "('sf, 'sc, 'sz) formula" where
          "ν ∈ fml_sem I ff ∧ List.member (p # close Δ (Δ ! j)) ff"
          using a1 by (metis (no_types) ‹⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ› ‹⋀y. List.member (q # Γ) y = (q = y ∨ List.member Γ y)› ‹ν ∈ fml_sem I (foldr (&&) (q # Γ) TT) ⟹ ν ∈ fml_sem I (foldr (||) (p # closeI Δ j) FF)› ‹ν ∈ fml_sem I (foldr (||) (p # closeI Δ j) FF) ⟹ ∃φ. ν ∈ fml_sem I φ ∧ List.member (p # closeI Δ j) φ› and_foldl_sem_conv closeI.simps)
        then show ?thesis
          using a2 by (metis (no_types) ‹⋀φ ν I. ⟦List.member Δ φ; ν ∈ fml_sem I φ⟧ ⟹ ν ∈ fml_sem I (foldr (||) Δ FF)› ‹⋀y. List.member (p # closeI Δ j) y = (p = y ∨ List.member (closeI Δ j) y)› closeI.simps close_sub local.sublist_def sem)
      qed
      show "ν ∈ fml_sem I (foldr (||) Δ FF)"
        by (metis AIjeq SG_dec ‹⟦ν ∈ fml_sem I q; ν ∉ fml_sem I (foldr (||) Δ FF)⟧ ⟹ False› iff_sem jL nth_member or_foldl_sem sem snd_eqD)
    qed
    show "ν ∈ fml_sem I (foldr (||) Δ FF)"
      by(cases "ν ∈ fml_sem I p", (simp add: case1 case2)+)
    qed
  show ?case
    apply(rule close_provable_sound)
     apply(rule sound_weaken_appR)
     apply(rule sound)
    using res_eq
    apply(unfold res_eq)
    unfolding close_app_comm
    apply (rule sound_weaken_appL)
    using close_eq big_sound SG_dec AIjeq
    by (simp add: AIjeq)
qed

lemma step_sound:"step_ok R i S ⟹ i ≥ 0 ⟹ i < length (fst R) ⟹ sound R ⟹ sound (step_result R (i,S))"
proof(induction rule: step_ok.induct)
  case (Step_Axiom SG i a C)
  assume is_axiom:"SG ! i = ([], [get_axiom a])"
  assume sound:"sound (SG, C)"
  assume i0:"0 ≤ i"
  assume "i < length (fst (SG, C))"
  then have iL:"i < length (SG)" 
    by auto
  have "seq_valid ([], [get_axiom a])"
    apply(rule fml_seq_valid)
    by(rule axiom_valid)
  then have seq_valid:"seq_valid (SG ! i)"
    using is_axiom by auto
  ― ‹‹i0 iL››
  then show ?case 
    using closeI_valid_sound[OF sound seq_valid] by simp
next
  case (Step_AxSubst SG i a σ C)
  assume is_axiom:"SG ! i = ([], [Fsubst (get_axiom a) σ])"
  assume sound:"sound (SG, C)"
  assume ssafe:"ssafe σ"
  assume i0:"0 ≤ i"
  assume Fadmit:"Fadmit σ (get_axiom a)"
  assume "i < length (fst (SG, C))"
  then have iL:"i < length (SG)" 
    by auto
  have valid_axiom:"valid (get_axiom a)"
    by(rule axiom_valid)
  have subst_valid:"valid (Fsubst (get_axiom a) σ)"
    apply(rule subst_fml_valid)
       apply(rule Fadmit)
      apply(rule axiom_safe)
     apply(rule ssafe)
    by(rule valid_axiom)
  have "seq_valid ([], [(Fsubst (get_axiom a) σ)])"
    apply(rule fml_seq_valid)
    by(rule subst_valid)
  then have seq_valid:"seq_valid (SG ! i)"
    using is_axiom by auto
  ― ‹‹i0 iL››
  then show ?case 
    using closeI_valid_sound[OF sound seq_valid] by simp
next
  case (Step_Lrule R i j L)
  then show ?case
    using lrule_sound
    using step_result.simps(2) surj_pair
    by simp
next
  case (Step_Rrule R i SG j L)
  then show ?case 
    using rrule_sound
    using step_result.simps(2) surj_pair
    by simp
next
  case (Step_Cut φ i SG C)
  assume safe:"fsafe φ"
  assume "i < length (fst (SG, C))"
  then have iL:"i < length SG" by auto
  assume sound:"sound (SG, C)"
  obtain Γ and Δ where SG_dec:"(Γ,Δ) = (SG ! i)"
    by (metis seq2fml.cases)
  have "sound ((φ # Γ, Δ) # (Γ, φ # Δ) # [y←SG . y ≠ SG ! i], C)"
    apply(rule soundI_memv)
  proof -
    fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
    assume good:"is_interp I"
    assume sgs:"(⋀φ' ν. List.member ((φ # Γ, Δ) # (Γ, φ # Δ) # [y←SG . y ≠ SG ! i]) φ' ⟹ ν ∈ seq_sem I φ')"
    have sg1:"⋀ν. ν ∈ seq_sem I (φ # Γ, Δ)" using sgs by (meson member_rec(1))
    have sg2:"⋀ν. ν ∈ seq_sem I (Γ, φ # Δ)" using sgs by (meson member_rec(1))
    have sgs:"⋀φ ν. (List.member (close SG (nth SG i)) φ) ⟹ ν ∈ seq_sem I φ"
      using sgs  by (simp add: member_rec(1))
    then have sgs:"⋀φ ν. (List.member (close SG (Γ,Δ)) φ) ⟹ ν ∈ seq_sem I φ"
      using SG_dec by auto
    have sgNew:"⋀ν. ν ∈ seq_sem I (Γ, Δ)"
      using sg1 sg2 by auto
    have same_mem:"⋀x. List.member SG x ⟹ List.member ((Γ,Δ) # close SG (Γ,Δ)) x"
      subgoal for s
        by(induction SG, auto simp add: member_rec)
      done
    have SGS:"(⋀φ' ν. List.member SG φ' ⟹ ν ∈ seq_sem I φ')"
      using sgNew sgs same_mem member_rec(1) seq_MP
      by metis
    show "ν ∈ seq_sem I C"
      using sound apply simp
      apply(drule soundD_memv)
        apply(rule good)
       using SGS 
       apply blast
      by auto
  qed
  then show ?case 
    using SG_dec case_prod_conv
  proof -
    have "(⋀f. ((case nth SG i of (x, xa) ⇒ ((f x xa)::('sf, 'sc, 'sz) rule)) = (f Γ Δ)))"
      by (metis (no_types) SG_dec case_prod_conv)
    then show ?thesis
      by (simp add: ‹sound ((φ # Γ, Δ) # (Γ, φ # Δ) # [y←SG . y ≠ SG ! i], C)›)
  qed
next
  case (Step_G SG i C a p)
  assume eq:"SG ! i = ([], [([[a]]p)])"
  assume iL:"i < length (fst (SG, C))"
  assume sound:"sound (SG, C)"
  have "sound (([], [p]) # (close SG ([], [([[ a ]] p)])), C)"
    apply(rule soundI_memv)
  proof -
    fix I::"('sf,'sc,'sz) interp" and  ν::"'sz state"
    assume "is_interp I"
    assume sgs:"(⋀φ ν. List.member (([], [p]) # close SG ([], [([[a]]p)])) φ ⟹ ν ∈ seq_sem I φ)"
    have sg0:"(⋀ν. ν ∈ seq_sem I ([], [p]))"
      using sgs by (meson member_rec(1))
    then have sg0':"(⋀ν. ν ∈ seq_sem I ([], [([[a]]p)]))"
      by auto
    have sgTail:"(⋀φ ν. List.member (close SG ([], [([[a]]p)])) φ ⟹ ν ∈ seq_sem I φ)"
      using sgs by (simp add: member_rec(1))
    have same_mem:"⋀x. List.member SG x ⟹ List.member (([], [([[a]]p)]) # close SG ([], [([[a]]p)])) x"
      subgoal for s
        by(induction SG, auto simp add: member_rec)
      done
    have sgsC:"(⋀φ ν. List.member SG φ ⟹ ν ∈ seq_sem I φ)"
      apply auto
      using sgTail sg0' same_mem member_rec
      by (metis seq_MP)
    then show "ν ∈ seq_sem I C"
      using sound
      by (metis UNIV_eq_I ‹is_interp I› iso_tuple_UNIV_I soundD_mem)
  qed
  then show ?case 
    by(auto simp add: eq Box_def)
next
  case (Step_CloseId SG i j k C)
  assume match:"fst (SG ! i) ! j = snd (SG ! i) ! k"
  assume jL:"j < length (fst (SG ! i))"
  assume kL:"k < length (snd (SG ! i))"
  assume iL:"i < length (fst (SG, C))"
  then have iL:"i < length (SG)" 
    by auto
  assume sound:"sound (SG, C)"
  obtain Γ Δ where SG_dec:"(Γ, Δ) = SG ! i" 
    using prod.collapse by blast
  have jΓ:"j < length Γ"
    using SG_dec jL
    by (metis fst_conv)
  have kΔ:"k < length Δ"
    using SG_dec kL
    by (metis snd_conv)
  have "⋀I ν. is_interp I ⟹ ν ∈ fml_sem I (foldr (&&) Γ TT) ⟹ ν ∈ fml_sem I (foldr (||) Δ FF)"
  proof -
    fix I::"('sf,'sc,'sz)interp" and ν::"'sz state"
    assume good:"is_interp I"
    assume Γ_sem:"ν ∈ fml_sem I (foldr (&&) Γ TT)"
    have mem:"List.member Γ (Γ ! j)"
      using jΓ nth_member by blast
    have mem2:"List.member Δ (Δ ! k)"
      using kΔ nth_member by blast
    have "ν ∈ fml_sem I (Γ ! j)"
      using Γ_sem mem
      using and_foldl_sem by blast
    then have "ν ∈ fml_sem I (Δ ! k)"
      using match SG_dec
      by (metis fst_conv snd_conv)
    then show "ν ∈ fml_sem I (foldr (||) Δ FF)"
      using mem2
      using or_foldl_sem by blast
  qed
  then have seq_valid:"seq_valid (SG ! i)"
    unfolding seq_valid_def using SG_dec
    by (metis UNIV_eq_I seq_semI')
  then show "sound (step_result (SG, C) (i, CloseId j k))" 
    using closeI_valid_sound[OF sound seq_valid] by simp
next
  case (Step_DEAxiom_schema SG i ODE σ C )
  assume isNth:"nth SG i =
  ([], [Fsubst (([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]]P pid1) ↔
                ([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]][[DiffAssign vid1 (f1 fid1 vid1)]]P pid1)) σ])"
  assume FA:"Fadmit σ
   (([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]]P pid1) ↔
    ([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]][[DiffAssign vid1 (f1 fid1 vid1)]]P pid1))"
  assume disj:"{Inl vid1, Inr vid1} ∩ BVO ODE = {}"
  have schem_valid:"valid (([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]] (P pid1)) ↔
    ([[EvolveODE ((OProd (OSing vid1 (f1 fid1 vid1))ODE)) (p1 vid2 vid1)]]
    [[DiffAssign vid1 (f1 fid1 vid1)]]P pid1))"
    using DE_sys_valid[OF disj] by auto
  assume ssafe:"ssafe σ"
  assume osafe:"osafe ODE"
  have subst_valid:"valid (Fsubst (([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]]P pid1) ↔
                ([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]][[DiffAssign vid1 (f1 fid1 vid1)]]P pid1)) σ)"
    apply(rule subst_fml_valid)
       apply(rule FA)
      subgoal using disj by(auto simp add: f1_def Box_def p1_def P_def Equiv_def Or_def expand_singleton osafe, induction ODE, auto)
     subgoal by (rule ssafe)
    by (rule schem_valid)
  assume "0 ≤ i" 
  assume "i < length (fst (SG, C))" 
  assume sound:"sound (SG, C)"
  have "seq_valid ([], [(Fsubst (([[EvolveODE (OProd  (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]]P pid1) ↔
                ([[EvolveODE (OProd  (OSing vid1 (f1 fid1 vid1))ODE) (p1 vid2 vid1)]][[DiffAssign vid1 (f1 fid1 vid1)]]P pid1)) σ)])"
    apply(rule fml_seq_valid)
    by(rule subst_valid)
  then have seq_valid:"seq_valid (SG ! i)"
    using isNth by auto
  ― ‹‹i0 iL››
  then show ?case 
  using closeI_valid_sound[OF sound seq_valid] by simp
next
  case (Step_CE SG i φ ψ σ C)
  assume isNth:"SG ! i = ([], [Fsubst (InContext pid1 φ ↔ InContext pid1 ψ) σ])"
  assume valid:"valid (φ ↔ ψ)"
  assume FA:"Fadmit σ (InContext pid1 φ ↔ InContext pid1 ψ)"
  assume "0 ≤ i"
  assume "i < length (fst (SG, C))"
  assume sound:"sound (SG, C)"
  assume fsafe1:"fsafe φ"
  assume fsafe2:"fsafe ψ"
  assume ssafe:"ssafe σ"
  have schem_valid:"valid (InContext pid1 φ ↔ InContext pid1 ψ)"
    using valid unfolding valid_def 
    by (metis CE_holds_def CE_sound fml_sem.simps(7) iff_sem surj_pair valid_def)+
  have subst_valid:"valid (Fsubst (InContext pid1 φ ↔ InContext pid1 ψ) σ)"
    apply(rule subst_fml_valid)
       apply(rule FA)
      subgoal by(auto simp add: f1_def Box_def p1_def P_def Equiv_def Or_def expand_singleton fsafe1 fsafe2)
     subgoal by (rule ssafe)
    by (rule schem_valid)
  have "seq_valid ([], [Fsubst (InContext pid1 φ ↔ InContext pid1 ψ) σ])"
    apply(rule fml_seq_valid)
    by(rule subst_valid)
  then have seq_valid:"seq_valid (SG ! i)"
    using isNth by auto
  show "sound (step_result (SG, C) (i, CE φ ψ σ))"
    using closeI_valid_sound[OF sound seq_valid] by simp
next
  case (Step_CQ SG i p θ θ' σ C)
  assume isNth:"nth SG  i = ([], [Fsubst (Equiv (Prop p (singleton θ)) (Prop p (singleton θ'))) σ])"
  assume valid:"valid (Equals θ θ')"
  assume FA:"Fadmit σ ($φ p (singleton θ) ↔ $φ p (singleton θ'))"
  assume "0 ≤ i"
  assume "i < length (fst (SG, C))"
  assume sound:"sound (SG, C)"
  assume dsafe1:"dsafe θ"
  assume dsafe2:"dsafe θ'"
  assume ssafe:"ssafe σ"
  have schem_valid:"valid ($φ p (singleton θ) ↔ $φ p (singleton θ'))"
    using valid unfolding valid_def 
    by (metis CQ_holds_def CQ_sound fml_sem.simps(7) iff_sem surj_pair valid_def)+
  have subst_valid:"valid (Fsubst ($φ p (singleton θ) ↔ $φ p (singleton θ')) σ)"
    apply(rule subst_fml_valid)
       apply(rule FA)
      using schem_valid ssafe by (auto simp add: f1_def Box_def p1_def P_def Equiv_def Or_def expand_singleton dsafe1 dsafe2 expand_singleton) 
  have "seq_valid ([], [Fsubst ($φ p (singleton θ) ↔ $φ p (singleton θ')) σ])"
    apply(rule fml_seq_valid)
    by(rule subst_valid)
  then have seq_valid:"seq_valid (SG ! i)"
    using isNth by auto
  show "sound (step_result (SG, C) (i, CQ θ θ' σ))"
    using closeI_valid_sound[OF sound seq_valid] by simp
qed

lemma deriv_sound:"deriv_ok R D ⟹ sound R ⟹ sound (deriv_result R D)"
  apply(induction rule: deriv_ok.induct)
   using step_sound by auto

lemma proof_sound:"proof_ok Pf ⟹ sound (proof_result Pf)"
  apply(induct rule: proof_ok.induct)
  unfolding proof_result.simps  apply(rule deriv_sound)
  apply assumption
  by(rule start_proof_sound)
  
section ‹Example 1: Differential Invariants›

definition DIAndConcl::"('sf,'sc,'sz) sequent"
where "DIAndConcl = ([], [Implies (And (Predicational pid1) (Predicational pid2)) 
       (Implies ([[Pvar vid1]](And (Predicational pid3) (Predicational pid4))) 
                ([[Pvar vid1]](And (Predicational pid1) (Predicational pid2))))])"

definition DIAndSG1::"('sf,'sc,'sz) formula"
where "DIAndSG1 = (Implies (Predicational pid1) (Implies ([[Pvar vid1]](Predicational pid3)) ([[Pvar vid1]](Predicational pid1))))"

definition DIAndSG2::"('sf,'sc,'sz) formula"
where "DIAndSG2 = (Implies (Predicational pid2) (Implies ([[Pvar vid1]](Predicational pid4)) ([[Pvar vid1]](Predicational pid2))))"

definition DIAndCut::"('sf,'sc,'sz) formula"
where "DIAndCut = 
  (([[$α vid1]]((And (Predicational ( pid3)) (Predicational ( pid4)))) → (And (Predicational ( pid1)) (Predicational ( pid2))))
    → ([[$α vid1]](And (Predicational ( pid3)) (Predicational ( pid4)))) → ([[$α vid1]](And (Predicational (pid1)) (Predicational ( pid2)))))"
  
definition DIAndSubst::"('sf,'sc,'sz) subst"
where "DIAndSubst = 
  ⦇ SFunctions = (λ_. None),
    SPredicates = (λ_. None),
    SContexts = (λC. (if C = pid1 then Some(And (Predicational (Inl pid3)) (Predicational (Inl pid4))) 
                else (if C = pid2 then Some(And (Predicational (Inl pid1)) (Predicational (Inl pid2))) else None))),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"
  
― ‹‹[a]R&H->R->[a]R&H->[a]R DIAndSubst34››
definition DIAndSubst341::"('sf,'sc,'sz) subst"
where "DIAndSubst341 = 
  ⦇ SFunctions = (λ_. None),
    SPredicates = (λ_. None),
    SContexts = (λC. (if C = pid1 then Some(And (Predicational (Inl pid3)) (Predicational (Inl pid4))) 
                else (if C = pid2 then Some(Predicational (Inl pid3)) else None))),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"
definition DIAndSubst342::"('sf,'sc,'sz) subst"
where "DIAndSubst342 = 
  ⦇ SFunctions = (λ_. None),
    SPredicates = (λ_. None),
    SContexts = (λC. (if C = pid1 then Some(And (Predicational (Inl pid3)) (Predicational (Inl pid4))) 
                else (if C = pid2 then Some(Predicational (Inl pid4)) else None))),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"
  
― ‹‹[a]P, [a]R&H, P, Q |- [a]Q->P&Q->[a]Q->[a]P&Q, [a]P&Q;;››
definition DIAndSubst12::"('sf,'sc,'sz) subst"
where "DIAndSubst12 = 
  ⦇ SFunctions = (λ_. None),
    SPredicates = (λ_. None),
    SContexts = (λC. (if C = pid1 then Some(Predicational (Inl pid2)) 
                else (if C = pid2 then Some(Predicational (Inl pid1) && Predicational (Inl pid2)) else None))),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"

― ‹‹P ->  Q->P&Q››
definition DIAndCurry12::"('sf,'sc,'sz) subst"
where "DIAndCurry12 = 
  ⦇ SFunctions = (λ_. None),
    SPredicates = (λ_. None),
    SContexts = (λC. (if C = pid1 then Some(Predicational (Inl pid1)) 
                else (if C = pid2 then Some(Predicational (Inl pid2) → (Predicational (Inl pid1) && Predicational (Inl pid2))) else None))),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"
  
definition DIAnd :: "('sf,'sc,'sz) rule" 
where "DIAnd = 
  ([([],[DIAndSG1]),([],[DIAndSG2])], 
  DIAndConcl)"

definition DIAndCutP1 :: "('sf,'sc,'sz) formula"
where "DIAndCutP1 = ([[Pvar vid1]](Predicational pid1))" 

definition DIAndCutP2 :: "('sf,'sc,'sz) formula"
where "DIAndCutP2 = ([[Pvar vid1]](Predicational pid2))" 

definition DIAndCutP12 :: "('sf,'sc,'sz) formula"
where "DIAndCutP12 = (([[Pvar vid1]](Pc pid1) → (Pc pid2 → (And (Pc pid1) (Pc pid2))))
  → (([[Pvar vid1]]Pc pid1) → ([[Pvar vid1]](Pc pid2 → (And (Pc pid1) (Pc pid2))))))" 

definition DIAndCut34Elim1 :: "('sf,'sc,'sz) formula"
where "DIAndCut34Elim1 = (([[Pvar vid1]](Pc pid3 && Pc pid4) → (Pc pid3))
  → (([[Pvar vid1]](Pc pid3 && Pc pid4)) → ([[Pvar vid1]](Pc pid3))))" 

definition DIAndCut34Elim2 :: "('sf,'sc,'sz) formula"
where "DIAndCut34Elim2 = (([[Pvar vid1]](Pc pid3 && Pc pid4) → (Pc pid4))
  → (([[Pvar vid1]](Pc pid3 && Pc pid4)) → ([[Pvar vid1]](Pc pid4))))" 

definition DIAndCut12Intro :: "('sf,'sc,'sz) formula"
where "DIAndCut12Intro = (([[Pvar vid1]](Pc pid2  → (Pc pid1 && Pc pid2)))
  → (([[Pvar vid1]](Pc pid2)) → ([[Pvar vid1]](Pc pid1 && Pc pid2))))" 

definition DIAndProof :: "('sf, 'sc, 'sz) pf"
where "DIAndProof =
  (DIAndConcl, [
   (0, Rrule ImplyR 0)  ― ‹1›
  ,(0, Lrule AndL 0)
  ,(0, Rrule ImplyR 0)
  ,(0, Cut DIAndCutP1)
  ,(1, Cut DIAndSG1)
  ,(0, Rrule CohideR 0)
  ,(Suc (Suc 0), Lrule ImplyL 0)
  ,(Suc (Suc (Suc 0)), CloseId 1 0)
  ,(Suc (Suc 0), Lrule ImplyL 0)
  ,(Suc (Suc 0), CloseId 0 0)
  ,(Suc (Suc 0), Cut DIAndCut34Elim1) ― ‹11›
  ,(0, Lrule ImplyL 0)
  ,(Suc (Suc (Suc 0)), Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(0, Rrule CohideRR 0)
  ,(Suc 0, Rrule CohideRR 0)
  ,(Suc (Suc (Suc (Suc (Suc 0)))), G)  
  ,(0, Rrule ImplyR 0)
  ,(Suc (Suc (Suc (Suc (Suc 0)))), Lrule AndL 0)
  ,(Suc (Suc (Suc (Suc (Suc 0)))), CloseId 0 0)
  ,(Suc (Suc (Suc 0)), AxSubst AK DIAndSubst341) ― ‹21›
  ,(Suc (Suc 0), CloseId 0 0)
  ,(Suc 0, CloseId 0 0)
  ,(0, Cut DIAndCut12Intro)
  ,(Suc 0, Rrule CohideRR 0)
  ,(Suc (Suc 0), AxSubst AK DIAndSubst12)
  ,(0, Lrule ImplyL 0)
  ,(1, Lrule ImplyL 0)
  ,(Suc (Suc 0), CloseId 0 0)
  ,(Suc 0, Cut DIAndCutP12)
  ,(0, Lrule ImplyL 0) ― ‹31›
  ,(0, Rrule CohideRR 0)
  ,(Suc (Suc (Suc (Suc 0))), AxSubst AK DIAndCurry12)
  ,(Suc (Suc (Suc 0)), Rrule CohideRR 0)
  ,(Suc (Suc 0), Lrule ImplyL 0)
  ,(Suc (Suc 0), G)  
  ,(0, Rrule ImplyR 0)  
  ,(Suc (Suc (Suc (Suc 0))), Rrule ImplyR 0)  
  ,(Suc (Suc (Suc (Suc 0))), Rrule AndR 0)  
  ,(Suc (Suc (Suc (Suc (Suc 0)))), CloseId 0 0)
  ,(Suc (Suc (Suc (Suc 0))), CloseId 1 0) ― ‹41›
  ,(Suc (Suc  0), CloseId 0 0)   
  ,(Suc 0, Cut DIAndCut34Elim2)
  ,(0, Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(Suc (Suc (Suc (Suc 0))), AxSubst AK DIAndSubst342) ― ‹46›
  ,(Suc (Suc (Suc 0)), Rrule CohideRR 0)
  ,(Suc (Suc (Suc 0)), G) ― ‹48›
  ,(0, Rrule ImplyR 0)
  ,(Suc (Suc (Suc 0)), Lrule AndL 0) ― ‹50›
  ,(Suc (Suc (Suc 0)), CloseId 1 0)
  ,(Suc (Suc 0), Lrule ImplyL 0)
  ,(Suc 0, CloseId 0 0)
  ,(1, Cut DIAndSG2)
  ,(0, Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(Suc (Suc (Suc 0)), CloseId 4 0)
  ,(Suc (Suc 0), Lrule ImplyL 0)
  ,(Suc (Suc (Suc 0)), CloseId 0 0)
  ,(Suc (Suc (Suc 0)), CloseId 0 0)
  ,(1, CloseId 1 0)
  ])
  "

fun proof_take :: "nat ⇒ ('sf,'sc,'sz) pf ⇒ ('sf,'sc,'sz) pf"
where "proof_take n (C,D) = (C,List.take n D)"

fun last_step::"('sf,'sc,'sz) pf ⇒ nat ⇒ nat * ('sf,'sc,'sz ) step"
where "last_step (C,D) n = List.last (take n D)"

lemma DIAndSound_lemma:"sound (proof_result (proof_take 61 DIAndProof))"
  apply(rule proof_sound)
  unfolding DIAndProof_def DIAndConcl_def  DIAndCutP1_def DIAndSG1_def DIAndCut34Elim1_def  DIAndSubst341_def DIAndCut12Intro_def DIAndSubst12_def
    DIAndCutP12_def DIAndCurry12_def DIAndSubst342_def
    DIAndCut34Elim2_def ― ‹43›
    DIAndSG2_def ― ‹54› (* slow *)
  apply (auto simp add: prover)
  done
  
section ‹Example 2: Concrete Hybrid System›

― ‹‹v ≥ 0 ∧ A() ≥ 0 ⟶ [v' = A, x' = v]v' ≥ 0››
definition SystemConcl::"('sf,'sc,'sz) sequent"
where "SystemConcl = 
  ([],[
  Implies (And (Geq (Var vid1) (Const 0)) (Geq (f0 fid1) (Const 0)))
  ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (TT)]]Geq (Var vid1) (Const 0))
  ])"

definition SystemDICut :: "('sf,'sc,'sz) formula"
where "SystemDICut =
  Implies
  (Implies TT ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]]
     (Geq (Differential (Var vid1)) (Differential (Const 0)))))
  (Implies
     (Implies TT (Geq (Var vid1) (Const 0)))
     ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]](Geq (Var vid1) (Const 0))))"
(*
    (Implies (Geq (Var vid1) (Const 0)) 
      (Implies (And TT ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]]
                  (Geq (Differential (Var vid1)) (Differential (Const 0)))
   )) ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]](Geq (Var vid1) (Const 0)))))"
*)  
definition SystemDCCut::"('sf,'sc,'sz) formula"
where "SystemDCCut =
(([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]](Geq (f0 fid1) (Const 0))) →
   (([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]]((Geq (Differential (Var vid1)) (Differential (Const 0))))) 
   ↔  
   ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]](Geq (Differential (Var vid1)) (Differential (Const 0))))))"
  
definition SystemVCut::"('sf,'sc,'sz) formula"
where "SystemVCut = 
  Implies (Geq (f0 fid1) (Const 0)) ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]](Geq (f0 fid1) (Const 0)))" 

definition SystemVCut2::"('sf,'sc,'sz) formula"
where "SystemVCut2 = 
  Implies (Geq (f0 fid1) (Const 0)) ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]](Geq (f0 fid1) (Const 0)))" 

definition SystemDECut::"('sf,'sc,'sz) formula"
where "SystemDECut = (([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]] ((Geq (Differential (Var vid1)) (Differential (Const 0))))) ↔
 ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]]
    [[DiffAssign vid1 (f0 fid1)]](Geq (Differential (Var vid1)) (Differential (Const 0)))))"

definition SystemKCut::"('sf,'sc,'sz) formula"
where "SystemKCut =
  (Implies ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]]
                (Implies ((And TT (Geq (f0 fid1) (Const 0)))) ([[DiffAssign vid1 (f0 fid1)]](Geq (Differential (Var vid1)) (Differential (Const 0))))))
      (Implies ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]] ((And TT (Geq (f0 fid1) (Const 0)))))
               ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]] ([[DiffAssign vid1 (f0 fid1)]](Geq (Differential (Var vid1)) (Differential (Const 0)))))))"

definition SystemEquivCut::"('sf,'sc,'sz) formula"
where "SystemEquivCut =
  (Equiv (Implies ((And TT (Geq (f0 fid1) (Const 0)))) ([[DiffAssign vid1 (f0 fid1)]](Geq (Differential (Var vid1)) (Differential (Const 0)))))
         (Implies ((And TT (Geq (f0 fid1) (Const 0)))) ([[DiffAssign vid1 (f0 fid1)]](Geq (DiffVar vid1) (Const 0)))))"

definition SystemDiffAssignCut::"('sf,'sc,'sz) formula"
where "SystemDiffAssignCut =
  (([[DiffAssign vid1  ($f fid1 empty)]] (Geq (DiffVar vid1) (Const 0)))
↔ (Geq ($f fid1 empty) (Const 0)))"
  
definition SystemCEFml1::"('sf,'sc,'sz) formula"
where "SystemCEFml1 = Geq (Differential (Var vid1)) (Differential (Const 0))"

definition SystemCEFml2::"('sf,'sc,'sz) formula"
where "SystemCEFml2 = Geq (DiffVar vid1) (Const 0)"


(*
definition diff_const_axiom :: "('sf, 'sc, 'sz) formula"
  where [axiom_defs]:"diff_const_axiom ≡ Equals (Differential ($f fid1 empty)) (Const 0)"

definition diff_var_axiom :: "('sf, 'sc, 'sz) formula"
  where [axiom_defs]:"diff_var_axiom ≡ Equals (Differential (Var vid1)) (DiffVar vid1)"*)

  
definition CQ1Concl::"('sf,'sc,'sz) formula"
where "CQ1Concl = (Geq (Differential (Var vid1)) (Differential (Const 0)) ↔ Geq (DiffVar vid1) (Differential (Const 0)))"

definition CQ2Concl::"('sf,'sc,'sz) formula"
where "CQ2Concl = (Geq (DiffVar vid1) (Differential (Const 0)) ↔ Geq ($' vid1) (Const 0))"

definition CEReq::"('sf,'sc,'sz) formula"
where "CEReq = (Geq (Differential (trm.Var vid1)) (Differential (Const 0)) ↔ Geq ($' vid1) (Const 0))"

definition CQRightSubst::"('sf,'sc,'sz) subst"
where "CQRightSubst = 
  ⦇ SFunctions = (λ_. None),
    SPredicates = (λp. (if p = vid1 then (Some (Geq (DiffVar vid1) (Function  (Inr vid1)  empty))) else None)),
    SContexts = (λ_. None),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"


definition CQLeftSubst::"('sf,'sc,'sz) subst"
where "CQLeftSubst = 
  ⦇ SFunctions = (λ_. None),
    SPredicates = (λp. (if p = vid1 then (Some (Geq  (Function  (Inr vid1)  empty) (Differential (Const 0)))) else None)),
    SContexts = (λ_. None),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"

definition CEProof::"('sf,'sc,'sz) pf"
where "CEProof = (([],[CEReq]), [
  (0, Cut CQ1Concl)
 ,(0, Cut CQ2Concl)
 ,(1, Rrule CohideRR 0)
 ,(Suc (Suc 0), CQ (Differential (Const 0)) (Const 0) CQRightSubst)
 ,(1, Rrule CohideRR 0)
 ,(1, CQ (Differential (Var vid1)) (DiffVar vid1) CQLeftSubst)
 ,(0, Rrule EquivR 0)
 ,(0, Lrule EquivForwardL 1)
 ,(Suc (Suc 0), Lrule EquivForwardL 1)
 ,(Suc (Suc (Suc 0)), CloseId 0 0)
 ,(Suc (Suc 0), CloseId 0 0)
 ,(Suc 0, CloseId 0 0)
 ,(0, Lrule EquivBackwardL (Suc (Suc 0)))
 ,(0, CloseId 0 0)
 ,(0, Lrule EquivBackwardL (Suc 0))
 ,(0, CloseId 0 0)
 ,(0, CloseId 0 0)
 ])"  

lemma CE_result_correct:"proof_result CEProof = ([],([],[CEReq]))"
  unfolding CEProof_def CEReq_def CQ1Concl_def  CQ2Concl_def Implies_def Or_def f0_def TT_def Equiv_def Box_def CQRightSubst_def
  by (auto simp add: id_simps)

definition DiffConstSubst::"('sf,'sc,'sz) subst"
where "DiffConstSubst = ⦇
    SFunctions = (λf. (if f = fid1 then (Some (Const 0)) else None)),
    SPredicates = (λ_. None),
    SContexts = (λ_. None),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"

definition DiffConstProof::"('sf,'sc,'sz) pf"
where "DiffConstProof = (([],[(Equals (Differential (Const 0)) (Const 0))]), [
  (0, AxSubst AdConst DiffConstSubst)])"

lemma diffconst_result_correct:"proof_result DiffConstProof = ([], ([],[Equals (Differential (Const 0)) (Const 0)]))"
  by(auto simp add: prover DiffConstProof_def)

lemma diffconst_sound_lemma:"sound (proof_result DiffConstProof)"
  apply(rule proof_sound)
  unfolding DiffConstProof_def
  by (auto simp add: prover DiffConstProof_def DiffConstSubst_def Equals_def empty_def TUadmit_def)
  
lemma valid_of_sound:"sound ([], ([],[φ])) ⟹ valid φ"
  unfolding valid_def sound_def TT_def FF_def 
  apply (auto simp add: TT_def FF_def Or_def)
  subgoal for I a b
    apply(erule allE[where x=I])
    by(auto)
  done

lemma almost_diff_const_sound:"sound ([], ([], [Equals (Differential (Const 0)) (Const 0)]))"
  using diffconst_result_correct diffconst_sound_lemma by simp

lemma almost_diff_const:"valid (Equals (Differential (Const 0)) (Const 0))"
  using almost_diff_const_sound valid_of_sound by auto

― ‹Note: this is just unpacking the definition: the axiom is defined as literally this formula›
lemma almost_diff_var:"valid (Equals (Differential (trm.Var vid1)) ($' vid1))"
  using diff_var_axiom_valid unfolding diff_var_axiom_def by auto

lemma CESound_lemma:"sound (proof_result CEProof)"
  apply(rule proof_sound)
  unfolding CEProof_def CEReq_def CQ1Concl_def CQ2Concl_def Equiv_def CQRightSubst_def diff_const_axiom_valid diff_var_axiom_valid empty_def Or_def expand_singleton 
  diff_var_axiom_def
  by (auto simp add: prover CEProof_def CEReq_def CQ1Concl_def CQ2Concl_def Equiv_def
    CQRightSubst_def diff_const_axiom_valid diff_var_axiom_valid empty_def Or_def expand_singleton 
    TUadmit_def NTUadmit_def almost_diff_const CQLeftSubst_def almost_diff_var)

lemma sound_to_valid:"sound ([], ([], [φ])) ⟹ valid φ"
  unfolding  valid_def apply auto
  apply(drule soundD_mem)
  by (auto simp add: member_rec(2))
  
lemma CE1pre:"sound ([], ([], [CEReq]))"  
  using CE_result_correct CESound_lemma 
  by simp
                            
lemma CE1pre_valid:"valid CEReq"
  by (rule sound_to_valid[OF CE1pre])
    
lemma CE1pre_valid2:"valid (! (! (Geq (Differential (trm.Var vid1)) (Differential (Const 0)) && Geq ($' vid1) (Const 0)) &&
              ! (! (Geq (Differential (trm.Var vid1)) (Differential (Const 0))) && ! (Geq ($' vid1) (Const 0))))) "
  using CE1pre_valid unfolding CEReq_def Equiv_def Or_def by auto

definition SystemDISubst::"('sf,'sc,'sz) subst"
where "SystemDISubst = 
  ⦇ SFunctions = (λf. 
    (     if f = fid1 then Some(Function (Inr vid1) empty)
     else if f = fid2 then Some(Const 0)
     else None)),
    SPredicates = (λp. if p = vid1 then Some TT else None),
    SContexts = (λ_. None),
    SPrograms = (λ_. None),
    SODEs = (λc. if c = vid1 then Some (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (trm.Var vid1))) else None)
  ⦈"
  
  (*
  Implies 
  (Implies (Prop vid1 empty) ([[EvolveODE (OVar vid1) (Prop vid1 empty)]](Geq (Differential (f1 fid1 vid1)) (Differential (f1 fid2 vid1)))))
  (Implies
     (Implies(Prop vid1 empty) (Geq (f1 fid1 vid1) (f1 fid2 vid1)))
     ([[EvolveODE (OVar vid1) (Prop vid1 empty)]](Geq (f1 fid1 vid1) (f1 fid2 vid1))))"
*)
(*
Implies
  (Implies TT ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]]
     (Geq (Differential (Var vid1)) (Differential (Const 0)))))
  (Implies
     (Implies TT (Geq (Var vid1) (Const 0)))
     ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) TT]](Geq (Var vid1) (Const 0))))
*)

definition SystemDCSubst::"('sf,'sc,'sz) subst"
where "SystemDCSubst = 
  ⦇ SFunctions = (λ
  f.  None),
    SPredicates = (λp.  None),
    SContexts = (λC. 
    if C = pid1 then
      Some TT
    else if C = pid2 then
      Some (Geq (Differential (Var vid1)) (Differential (Const 0)))
    else if C = pid3 then
      Some (Geq (Function fid1 empty) (Const 0)) 
    else 
     None),
    SPrograms = (λ_. None),
    SODEs = (λc. if c = vid1 then Some (OProd (OSing vid1 (Function fid1 empty)) (OSing vid2 (trm.Var vid1))) else None)
  ⦈"

definition SystemVSubst::"('sf,'sc,'sz) subst"
where "SystemVSubst = 
  ⦇ SFunctions = (λf.  None),
    SPredicates = (λp. if p = vid1 then Some (Geq (Function (Inl fid1) empty) (Const 0)) else None),
    SContexts = (λ_. None),
    SPrograms = (λa. if a = vid1 then 
      Some (EvolveODE (OProd 
                         (OSing vid1 (Function fid1 empty)) 
                         (OSing vid2 (Var vid1))) 
                      (And TT (Geq (Function fid1 empty) (Const 0)))) 
                      else None),
    SODEs = (λ_. None)
  ⦈"

definition SystemVSubst2::"('sf,'sc,'sz) subst"
where "SystemVSubst2 = 
  ⦇ SFunctions = (λf.  None),
    SPredicates = (λp. if p = vid1 then Some (Geq (Function (Inl fid1) empty) (Const 0)) else None),
    SContexts = (λ_. None),
    SPrograms = (λa. if a = vid1 then 
      Some (EvolveODE (OProd 
                         (OSing vid1 (Function fid1 empty)) 
                         (OSing vid2 (Var vid1))) 
                      TT) 
                      else None),
    SODEs = (λ_. None)
  ⦈"

definition SystemDESubst::"('sf,'sc,'sz) subst"
where "SystemDESubst = 
  ⦇ SFunctions = (λf. if f = fid1 then Some(Function (Inl fid1) empty) else None),
    SPredicates = (λp. if p = vid2 then Some(And TT (Geq (Function (Inl fid1) empty) (Const 0))) else None),
    SContexts = (λC. if C = pid1 then Some(Geq (Differential (Var vid1)) (Differential (Const 0))) else None),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"

lemma systemdesubst_correct:"∃ ODE.(([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]] ((Geq (Differential (Var vid1)) (Differential (Const 0))))) ↔
 ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (And TT (Geq (f0 fid1) (Const 0)))]]
    [[DiffAssign vid1 (f0 fid1)]](Geq (Differential (Var vid1)) (Differential (Const 0)))))
    = Fsubst ((([[EvolveODE (OProd (OSing vid1 (f1 fid1 vid1)) ODE) (p1 vid2 vid1)]] (P pid1)) ↔
          ([[EvolveODE ((OProd  (OSing vid1 (f1 fid1 vid1))) ODE) (p1 vid2 vid1)]]
               [[DiffAssign vid1 (f1 fid1 vid1)]]P pid1))) SystemDESubst"
  apply(rule exI[where x="OSing vid2 (trm.Var vid1)"])
  by(auto simp add: f0_def f1_def Box_def Or_def Equiv_def empty_def TT_def P_def p1_def SystemDESubst_def empty_def)
  
― ‹‹[{dx=, dy=x&r>=r&>=r}]r>=r&>=r->[D{x}:=]D{x}>=D{r}->››
― ‹‹[{dx=, dy=x&r>=r&>=r}]r>=r&>=r->››
― ‹‹[{dx=, dy=x&r>=r&>=r}][D{x}:=]D{x}>=D{r}››
― ‹‹([[$α vid1]]((Predicational pid1) → (Predicational pid2)))››
― ‹‹→ ([[$α vid1]]Predicational pid1) → ([[$α vid1]]Predicational pid2)››
definition SystemKSubst::"('sf,'sc,'sz) subst"
where "SystemKSubst = ⦇ SFunctions = (λf.  None),
    SPredicates = (λ_. None),
    SContexts = (λC. if C = pid1 then 
        (Some (And (Geq (Const 0) (Const 0)) (Geq (Function fid1 empty) (Const 0)))) 
      else if C = pid2 then 
        (Some ([[DiffAssign vid1 (Function fid1 empty)]](Geq (Differential (Var vid1)) (Differential (Const 0))))) else None),
    SPrograms = (λc. if c = vid1 then Some (EvolveODE (OProd (OSing vid1 (Function fid1 empty)) (OSing vid2 (Var vid1))) (And (Geq (Const 0) (Const 0)) (Geq (Function fid1 empty) (Const 0)))) else None),
    SODEs = (λ_. None)
  ⦈"

lemma subst_imp_simp:"Fsubst (Implies p q) σ = (Implies (Fsubst p σ) (Fsubst q σ))"
  unfolding Implies_def Or_def by auto

lemma subst_equiv_simp:"Fsubst (Equiv p q) σ = (Equiv (Fsubst p σ) (Fsubst q σ))"
  unfolding Implies_def Or_def Equiv_def by auto

lemma subst_box_simp:"Fsubst (Box p q) σ = (Box (Psubst p σ) (Fsubst q σ))"
  unfolding Box_def Or_def by auto

lemma pfsubst_box_simp:"PFsubst (Box p q) σ = (Box (PPsubst p σ) (PFsubst q σ))"
  unfolding Box_def Or_def by auto

lemma pfsubst_imp_simp:"PFsubst (Implies p q) σ = (Implies (PFsubst p σ) (PFsubst q σ))"
  unfolding Box_def Implies_def Or_def by auto

definition SystemDWSubst::"('sf,'sc,'sz) subst"
where "SystemDWSubst = ⦇ SFunctions = (λf.  None),
    SPredicates = (λ_. None),
    SContexts = (λC. if C = pid1 then Some (And (Geq (Const 0) (Const 0)) (Geq (Function fid1 empty) (Const 0))) else None),
    SPrograms = (λ_. None),
    SODEs = (λc. if c = vid1 then Some (OProd (OSing vid1 (Function fid1 empty)) (OSing vid2 (Var vid1))) else None)
  ⦈"

definition SystemCESubst::"('sf,'sc,'sz) subst"
where "SystemCESubst = ⦇ SFunctions = (λf.  None),
    SPredicates = (λ_. None),
    SContexts = (λC. if C = pid1 then Some(Implies(And (Geq (Const 0) (Const 0)) (Geq (Function fid1 empty) (Const 0))) ([[DiffAssign vid1 (Function fid1 empty)]](Predicational (Inr ())))) else None),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"

lemma SystemCESubstOK:
  "step_ok 
  ([([],[Equiv (Implies(And (Geq (Const 0) (Const 0)) (Geq (Function fid1 empty) (Const 0))) ([[DiffAssign vid1 (Function fid1 empty)]]( SystemCEFml1))) 
         (Implies(And (Geq (Const 0) (Const 0)) (Geq (Function fid1 empty) (Const 0))) ([[DiffAssign vid1 (Function fid1 empty)]]( (SystemCEFml2))))
         ])],
         ([],[]))
         
         0 
         (CE SystemCEFml1 SystemCEFml2 SystemCESubst)"
  apply(rule Step_CE)
       subgoal by(auto simp add: subst_equiv_simp subst_imp_simp subst_box_simp SystemCESubst_def SystemCEFml1_def SystemCEFml2_def pfsubst_imp_simp pfsubst_box_simp)
      subgoal using CE1pre_valid 
        by (auto simp add: CEReq_def SystemCEFml1_def SystemCEFml2_def CE1pre_valid)
     subgoal unfolding SystemCEFml1_def by auto
    subgoal unfolding SystemCEFml2_def by auto
   subgoal unfolding SystemCESubst_def ssafe_def Implies_def Box_def Or_def empty_def by auto
  unfolding SystemCESubst_def Equiv_def Or_def SystemCEFml1_def SystemCEFml2_def TUadmit_def apply (auto simp add: TUadmit_def FUadmit_def Box_def Implies_def Or_def)
     unfolding PFUadmit_def by auto
  
― ‹‹[D{x}:=f]Dv{x}>=r<->f>=r››
― ‹‹[[DiffAssign vid1  ($f fid1 empty)]] (Prop vid1 (singleton (DiffVar vid1))))››
― ‹‹↔ Prop vid1 (singleton ($f fid1 empty))››
definition SystemDiffAssignSubst::"('sf,'sc,'sz) subst"
where "SystemDiffAssignSubst = ⦇ SFunctions = (λf.  None),
    SPredicates = (λp. if p = vid1 then Some (Geq (Function (Inr vid1) empty) (Const 0)) else None),
    SContexts = (λ_. None),
    SPrograms = (λ_. None),
    SODEs = (λ_. None)
  ⦈"

lemma SystemDICutCorrect:"SystemDICut = Fsubst DIGeqaxiom SystemDISubst"
  unfolding SystemDICut_def DIGeqaxiom_def SystemDISubst_def 
  by (auto simp add: f1_def p1_def f0_def Implies_def Or_def id_simps TT_def Box_def empty_def)

― ‹‹v≥0 ∧ A()≥0 → [{x'=v, v'=A()}]v≥0››
definition SystemProof :: "('sf, 'sc, 'sz) pf"
where "SystemProof =
  (SystemConcl, [
  (0, Rrule ImplyR 0)
  ,(0, Lrule AndL 0)
  ,(0, Cut SystemDICut)
  ,(0, Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(0, Lrule ImplyL 0)
  ,(Suc (Suc 0), CloseId 0 0)
  ,(Suc 0, AxSubst ADIGeq SystemDISubst) ― ‹8›
  ,(Suc 0, Rrule ImplyR 0)
  ⌦‹,(0, CloseId 0 0)›
  ,(Suc 0, CloseId 1 0)        
  ⌦‹,(0, Rrule AndR 0)›
  ,(0, Rrule ImplyR 0)   
  ,(0, Cut SystemDCCut)
  ,(0, Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(0, Lrule EquivBackwardL 0)
  ,(0, Rrule CohideR 0)
  ,(0, AxSubst ADC SystemDCSubst) ― ‹17›
  ,(0, CloseId 0 0)
  ,(0, Rrule CohideRR 0)
  ,(0, Cut SystemVCut)
  ,(0, Lrule ImplyL 0) 
  ,(0, Rrule CohideRR 0)
  ,(0, Cut SystemDECut)
  ,(0, Lrule EquivBackwardL 0)
  ,(0, Rrule CohideRR 0)
  ,(1, CloseId (Suc 1) 0) ― ‹Last step›
  ,(Suc 1, CloseId 0 0)
  ,(1, AxSubst AV SystemVSubst) ― ‹28›
  ,(0, Cut SystemVCut2)
  
  ,(0, Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(Suc 1, CloseId 0 0)
  ,(Suc 1, CloseId (Suc 2) 0)
  
  ,(Suc 1, AxSubst AV SystemVSubst2) ― ‹34›
  ,(0, Rrule CohideRR 0)
  ,(0, DEAxiomSchema (OSing vid2 (trm.Var vid1)) SystemDESubst) ― ‹36›
  ,(0, Cut SystemKCut)
  ,(0, Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(0, Lrule ImplyL 0)
  ,(0, Rrule CohideRR 0)
  ,(0, AxSubst AK SystemKSubst) ― ‹42›
  ,(0, CloseId 0 0)
  ,(0, Rrule CohideR 0)
  ,(1, AxSubst ADW SystemDWSubst) ― ‹45›
  ,(0, G)
  ,(0, Cut SystemEquivCut)
  ,(0, Lrule EquivBackwardL 0)
  ,(0, Rrule CohideR 0)
  ,(0, CloseId 0 0)
  ,(0, Rrule CohideR 0)
  ,(0, CE SystemCEFml1 SystemCEFml2 SystemCESubst) ― ‹52›
  ,(0, Rrule ImplyR 0)
  ,(0, Lrule AndL 0)
  ,(0, Cut SystemDiffAssignCut) 
  ,(0, Lrule EquivBackwardL 0)
  ,(0, Rrule CohideRR 0)
  ,(0, CloseId 0 0)
  ,(0, CloseId 1 0)
  ,(0, AxSubst Adassign SystemDiffAssignSubst) ― ‹60›
  ])"
  
lemma system_result_correct:"proof_result SystemProof = 
  ([],
  ([],[Implies (And (Geq (Var vid1) (Const 0)) (Geq (f0 fid1) (Const 0)))
        ([[EvolveODE (OProd (OSing vid1 (f0 fid1)) (OSing vid2 (Var vid1))) (TT)]]Geq (Var vid1) (Const 0))]))"
  unfolding SystemProof_def SystemConcl_def Implies_def Or_def f0_def TT_def Equiv_def SystemDICut_def SystemDCCut_def
  proof_result.simps deriv_result.simps start_proof.simps  Box_def SystemDCSubst_def SystemVCut_def SystemDECut_def SystemKCut_def SystemEquivCut_def
  SystemDiffAssignCut_def SystemVCut2_def
    (* slow *)
  apply( simp add:  prover)
  done

lemma SystemSound_lemma:"sound (proof_result SystemProof)"
  apply(rule proof_sound)
  unfolding SystemProof_def SystemConcl_def CQ1Concl_def CQ2Concl_def Equiv_def CQRightSubst_def diff_const_axiom_valid diff_var_axiom_valid empty_def Or_def expand_singleton 
  diff_var_axiom_def SystemDICut_def
  (* slow *)
  apply (auto simp add: prover CEProof_def CEReq_def CQ1Concl_def CQ2Concl_def Equiv_def
    CQRightSubst_def diff_const_axiom_valid diff_var_axiom_valid empty_def Or_def expand_singleton 
    TUadmit_def NTUadmit_def almost_diff_const CQLeftSubst_def almost_diff_var f0_def TT_def SystemDISubst_def f1_def p1_def SystemDCCut_def SystemDCSubst_def
    SystemVCut_def SystemDECut_def SystemVSubst_def
    SystemVCut2_def SystemVSubst2_def  SystemDESubst_def P_def SystemKCut_def  SystemKSubst_def SystemDWSubst_def SystemEquivCut_def
    SystemCESubst_def SystemCEFml1_def SystemCEFml2_def CE1pre_valid2 SystemDiffAssignCut_def SystemDiffAssignSubst_def)
  done

lemma system_sound:"sound ([], SystemConcl)"
  using SystemSound_lemma system_result_correct unfolding SystemConcl_def by auto
  
lemma DIAnd_result_correct:"proof_result (proof_take 61 DIAndProof) = DIAnd"
  unfolding DIAndProof_def DIAndConcl_def Implies_def Or_def 
  proof_result.simps deriv_result.simps start_proof.simps DIAndCutP12_def  DIAndSG1_def DIAndSG2_def DIAndCutP1_def Box_def DIAndCut34Elim1_def DIAndCut12Intro_def DIAndCut34Elim2_def DIAnd_def
  using pne12 pne13 pne14 pne23 pne24 pne34 by (auto)

theorem DIAnd_sound: "sound DIAnd"
  using DIAndSound_lemma DIAnd_result_correct by auto

end end