Session FOL_Seq_Calc2

v class="head">

Theory SeCaV

chapter SeCaV

(*
  Author: Jørgen Villadsen, DTU Compute, 2020
  Contributors: Stefan Berghofer, Asta Halkjær From, Alexander Birch Jensen & Anders Schlichtkrull
*)

section ‹Sequent Calculus Verifier (SeCaV)›

theory SeCaV imports Main begin

section ‹Syntax: Terms / Formulas›

datatype tm = Fun nat ‹tm list› | Var nat

datatype fm = Pre nat ‹tm list› | Imp fm fm | Dis fm fm | Con fm fm | Exi fm | Uni fm | Neg fm

section ‹Semantics: Terms / Formulas›

definition ‹shift e v x ≡ λn. if n < v then e n else if n = v then x else e (n - 1)›

primrec semantics_term and semantics_list where
  ‹semantics_term e f (Var n) = e n› |
  ‹semantics_term e f (Fun i l) = f i (semantics_list e f l)› |
  ‹semantics_list e f [] = []› |
  ‹semantics_list e f (t # l) = semantics_term e f t # semantics_list e f l›

primrec semantics where
  ‹semantics e f g (Pre i l) = g i (semantics_list e f l)› |
  ‹semantics e f g (Imp p q) = (semantics e f g p ⟶ semantics e f g q)› |
  ‹semantics e f g (Dis p q) = (semantics e f g p ∨ semantics e f g q)› |
  ‹semantics e f g (Con p q) = (semantics e f g p ∧ semantics e f g q)› |
  ‹semantics e f g (Exi p) = (∃x. semantics (shift e 0 x) f g p)› |
  ‹semantics e f g (Uni p) = (∀x. semantics (shift e 0 x) f g p)› |
  ‹semantics e f g (Neg p) = (¬ semantics e f g p)›

― ‹Test›

corollary ‹semantics e f g (Imp (Pre 0 []) (Pre 0 []))›
  by simp

lemma ‹¬ semantics e f g (Neg (Imp (Pre 0 []) (Pre 0 [])))›
  by simp

section ‹Auxiliary Functions›

primrec new_term and new_list where
  ‹new_term c (Var n) = True› |
  ‹new_term c (Fun i l) = (if i = c then False else new_list c l)› |
  ‹new_list c [] = True› |
  ‹new_list c (t # l) = (if new_term c t then new_list c l else False)›

primrec new where
  ‹new c (Pre i l) = new_list c l› |
  ‹new c (Imp p q) = (if new c p then new c q else False)› |
  ‹new c (Dis p q) = (if new c p then new c q else False)› |
  ‹new c (Con p q) = (if new c p then new c q else False)› |
  ‹new c (Exi p) = new c p› |
  ‹new c (Uni p) = new c p› |
  ‹new c (Neg p) = new c p›

primrec news where
  ‹news c [] = True› |
  ‹news c (p # z) = (if new c p then news c z else False)›

primrec inc_term and inc_list where
  ‹inc_term (Var n) = Var (n + 1)› |
  ‹inc_term (Fun i l) = Fun i (inc_list l)› |
  ‹inc_list [] = []› |
  ‹inc_list (t # l) = inc_term t # inc_list l›

primrec sub_term and sub_list where
  ‹sub_term v s (Var n) = (if n < v then Var n else if n = v then s else Var (n - 1))› |
  ‹sub_term v s (Fun i l) = Fun i (sub_list v s l)› |
  ‹sub_list v s [] = []› |
  ‹sub_list v s (t # l) = sub_term v s t # sub_list v s l›

primrec sub where
  ‹sub v s (Pre i l) = Pre i (sub_list v s l)› |
  ‹sub v s (Imp p q) = Imp (sub v s p) (sub v s q)› |
  ‹sub v s (Dis p q) = Dis (sub v s p) (sub v s q)› |
  ‹sub v s (Con p q) = Con (sub v s p) (sub v s q)› |
  ‹sub v s (Exi p) = Exi (sub (v + 1) (inc_term s) p)› |
  ‹sub v s (Uni p) = Uni (sub (v + 1) (inc_term s) p)› |
  ‹sub v s (Neg p) = Neg (sub v s p)›

primrec member where
  ‹member p [] = False› |
  ‹member p (q # z) = (if p = q then True else member p z)›

primrec ext where
  ‹ext y [] = True› |
  ‹ext y (p # z) = (if member p y then ext y z else False)›

― ‹Simplifications›

lemma member [iff]: ‹member p z ⟷ p ∈ set z›
  by (induct z) simp_all

lemma ext [iff]: ‹ext y z ⟷ set z ⊆ set y›
  by (induct z) simp_all

section ‹Sequent Calculus›

inductive sequent_calculus (‹⊩ _› 0) where
  ‹⊩ p # z› if ‹member (Neg p) z› |
  ‹⊩ Dis p q # z› if ‹⊩ p # q # z› |
  ‹⊩ Imp p q # z› if ‹⊩ Neg p # q # z› |
  ‹⊩ Neg (Con p q) # z› if ‹⊩ Neg p # Neg q # z› |
  ‹⊩ Con p q # z› if ‹⊩ p # z› and ‹⊩ q # z› |
  ‹⊩ Neg (Imp p q) # z› if ‹⊩ p # z› and ‹⊩ Neg q # z› |
  ‹⊩ Neg (Dis p q) # z› if ‹⊩ Neg p # z› and ‹⊩ Neg q # z› |
  ‹⊩ Exi p # z› if ‹⊩ sub 0 t p # z› |
  ‹⊩ Neg (Uni p) # z› if ‹⊩ Neg (sub 0 t p) # z› |
  ‹⊩ Uni p # z› if ‹⊩ sub 0 (Fun i []) p # z› and ‹news i (p # z)› |
  ‹⊩ Neg (Exi p) # z› if ‹⊩ Neg (sub 0 (Fun i []) p) # z› and ‹news i (p # z)› |
  ‹⊩ Neg (Neg p) # z› if ‹⊩ p # z› |
  ‹⊩ y› if ‹⊩ z› and ‹ext y z›

― ‹Test›

corollary ‹⊩ [Imp (Pre 0 []) (Pre 0 [])]›
  using sequent_calculus.intros(1,3,13) ext.simps member.simps(2) by metis

section ‹Shorthands›

lemmas Basic = sequent_calculus.intros(1)

lemmas AlphaDis = sequent_calculus.intros(2)
lemmas AlphaImp = sequent_calculus.intros(3)
lemmas AlphaCon = sequent_calculus.intros(4)

lemmas BetaCon = sequent_calculus.intros(5)
lemmas BetaImp = sequent_calculus.intros(6)
lemmas BetaDis = sequent_calculus.intros(7)

lemmas GammaExi = sequent_calculus.intros(8)
lemmas GammaUni = sequent_calculus.intros(9)

lemmas DeltaUni = sequent_calculus.intros(10)
lemmas DeltaExi = sequent_calculus.intros(11)

lemmas Neg = sequent_calculus.intros(12)

lemmas Ext = sequent_calculus.intros(13)

― ‹Test›

lemma ‹⊩
  [
    Imp (Pre 0 []) (Pre 0 [])
  ]
  ›
proof -
  from AlphaImp have ?thesis if ‹⊩
    [
      Neg (Pre 0 []),
      Pre 0 []
    ]
    ›
    using that by simp
  with Ext have ?thesis if ‹⊩
    [
      Pre 0 [],
      Neg (Pre 0 [])
    ]
    ›
    using that by simp
  with Basic show ?thesis
    by simp
qed

section ‹Appendix: Soundness›

subsection ‹Increment Function›

primrec liftt :: ‹tm ⇒ tm› and liftts :: ‹tm list ⇒ tm list› where
  ‹liftt (Var i) = Var (Suc i)› |
  ‹liftt (Fun a ts) = Fun a (liftts ts)› |
  ‹liftts [] = []› |
  ‹liftts (t # ts) = liftt t # liftts ts›

subsection ‹Parameters: Terms›

primrec paramst :: ‹tm ⇒ nat set› and paramsts :: ‹tm list ⇒ nat set› where
  ‹paramst (Var n) = {}› |
  ‹paramst (Fun a ts) = {a} ∪ paramsts ts› |
  ‹paramsts [] = {}› |
  ‹paramsts (t # ts) = (paramst t ∪ paramsts ts)›

lemma p0 [simp]: ‹paramsts ts = ⋃(set (map paramst ts))›
  by (induct ts) simp_all

primrec paramst' :: ‹tm ⇒ nat set› where
  ‹paramst' (Var n) = {}› |
  ‹paramst' (Fun a ts) = {a} ∪ ⋃(set (map paramst' ts))›

lemma p1 [simp]: ‹paramst' t = paramst t›
  by (induct t) simp_all

subsection ‹Parameters: Formulas›

primrec params :: ‹fm ⇒ nat set› where
  ‹params (Pre b ts) = paramsts ts› |
  ‹params (Imp p q) = params p ∪ params q› |
  ‹params (Dis p q) = params p ∪ params q› |
  ‹params (Con p q) = params p ∪ params q› |
  ‹params (Exi p) = params p› |
  ‹params (Uni p) = params p› |
  ‹params (Neg p) = params p›

primrec params' :: ‹fm ⇒ nat set› where
  ‹params' (Pre b ts) = ⋃(set (map paramst' ts))› |
  ‹params' (Imp p q) = params' p ∪ params' q› |
  ‹params' (Dis p q) = params' p ∪ params' q› |
  ‹params' (Con p q) = params' p ∪ params' q› |
  ‹params' (Exi p) = params' p› |
  ‹params' (Uni p) = params' p› |
  ‹params' (Neg p) = params' p›

lemma p2 [simp]: ‹params' p = params p›
  by (induct p) simp_all

fun paramst'' :: ‹tm ⇒ nat set› where
  ‹paramst'' (Var n) = {}› |
  ‹paramst'' (Fun a ts) = {a} ∪ (⋃t ∈ set ts. paramst'' t)›

lemma p1' [simp]: ‹paramst'' t = paramst t›
  by (induct t) simp_all

fun params'' :: ‹fm ⇒ nat set› where
  ‹params'' (Pre b ts) = (⋃t ∈ set ts. paramst'' t)› |
  ‹params'' (Imp p q) = params'' p ∪ params'' q› |
  ‹params'' (Dis p q) = params'' p ∪ params'' q› |
  ‹params'' (Con p q) = params'' p ∪ params'' q› |
  ‹params'' (Exi p) = params'' p› |
  ‹params'' (Uni p) = params'' p› |
  ‹params'' (Neg p) = params'' p›

lemma p2' [simp]: ‹params'' p = params p›
  by (induct p) simp_all

subsection ‹Update Lemmas›

lemma upd_lemma' [simp]:
  ‹n ∉ paramst t ⟹ semantics_term e (f(n := z)) t = semantics_term e f t›
  ‹n ∉ paramsts ts ⟹ semantics_list e (f(n := z)) ts = semantics_list e f ts›
  by (induct t and ts rule: paramst.induct paramsts.induct) auto

lemma upd_lemma [iff]: ‹n ∉ params p ⟹ semantics e (f(n := z)) g p ⟷ semantics e f g p›
  by (induct p arbitrary: e) simp_all

subsection ‹Substitution›

primrec substt :: ‹tm ⇒ tm ⇒ nat ⇒ tm› and substts :: ‹tm list ⇒ tm ⇒ nat ⇒ tm list› where
  ‹substt (Var i) s k = (if k < i then Var (i - 1) else if i = k then s else Var i)› |
  ‹substt (Fun a ts) s k = Fun a (substts ts s k)› |
  ‹substts [] s k = []› |
  ‹substts (t # ts) s k = substt t s k # substts ts s k›

primrec subst :: ‹fm ⇒ tm ⇒ nat ⇒ fm› where
  ‹subst (Pre b ts) s k = Pre b (substts ts s k)› |
  ‹subst (Imp p q) s k = Imp (subst p s k) (subst q s k)› |
  ‹subst (Dis p q) s k = Dis (subst p s k) (subst q s k)› |
  ‹subst (Con p q) s k = Con (subst p s k) (subst q s k)› |
  ‹subst (Exi p) s k = Exi (subst p (liftt s) (Suc k))› |
  ‹subst (Uni p) s k = Uni (subst p (liftt s) (Suc k))› |
  ‹subst (Neg p) s k = Neg (subst p s k)›

lemma shift_eq [simp]: ‹i = j ⟹ (shift e i T) j = T› for i :: nat
  unfolding shift_def by simp

lemma shift_gt [simp]: ‹j < i ⟹ (shift e i T) j = e j› for i :: nat
  unfolding shift_def by simp

lemma shift_lt [simp]: ‹i < j ⟹ (shift e i T) j = e (j - 1)› for i :: nat
  unfolding shift_def by simp

lemma shift_commute [simp]: ‹shift (shift e i U) 0 T = shift (shift e 0 T) (Suc i) U›
  unfolding shift_def by force

lemma subst_lemma' [simp]:
  ‹semantics_term e f (substt t u i) = semantics_term (shift e i (semantics_term e f u)) f t›
  ‹semantics_list e f (substts ts u i) = semantics_list (shift e i (semantics_term e f u)) f ts›
  by (induct t and ts rule: substt.induct substts.induct) simp_all

lemma lift_lemma [simp]:
  ‹semantics_term (shift e 0 x) f (liftt t) = semantics_term e f t›
  ‹semantics_list (shift e 0 x) f (liftts ts) = semantics_list e f ts›
  by (induct t and ts rule: liftt.induct liftts.induct) simp_all

lemma subst_lemma [iff]:
  ‹semantics e f g (subst a t i) ⟷ semantics (shift e i (semantics_term e f t)) f g a›
  by (induct a arbitrary: e i t) simp_all

subsection ‹Auxiliary Lemmas›

lemma s1 [iff]: ‹new_term c t ⟷ (c ∉ paramst t)› ‹new_list c l ⟷ (c ∉ paramsts l)›
  by (induct t and l rule: new_term.induct new_list.induct) simp_all

lemma s2 [iff]: ‹new c p ⟷ (c ∉ params p)›
  by (induct p) simp_all

lemma s3 [iff]: ‹news c z ⟷ list_all (λp. c ∉ params p) z›
  by (induct z) simp_all

lemma s4 [simp]: ‹inc_term t = liftt t› ‹inc_list l = liftts l›
  by (induct t and l rule: inc_term.induct inc_list.induct) simp_all

lemma s5 [simp]: ‹sub_term v s t = substt t s v› ‹sub_list v s l = substts l s v›
  by (induct t and l rule: inc_term.induct inc_list.induct) simp_all

lemma s6 [simp]: ‹sub v s p = subst p s v›
  by (induct p arbitrary: v s) simp_all

subsection ‹Soundness›

theorem sound: ‹⊩ z ⟹ ∃p ∈ set z. semantics e f g p›
proof (induct arbitrary: f rule: sequent_calculus.induct)
  case (10 i p z)
  then show ?case
  proof (cases ‹∀x. semantics e (f(i := λ_. x)) g (sub 0 (Fun i []) p)›)
    case False
    moreover have ‹list_all (λp. i ∉ params p) z›
      using 10 by simp
    ultimately show ?thesis
      using 10 Ball_set insert_iff list.set(2) upd_lemma by metis
  qed simp
next
  case (11 i p z)
  then show ?case
  proof (cases ‹∀x. semantics e (f(i := λ_. x)) g (Neg (sub 0 (Fun i []) p))›)
    case False
    moreover have ‹list_all (λp. i ∉ params p) z›
      using 11 by simp
    ultimately show ?thesis
      using 11 Ball_set insert_iff list.set(2) upd_lemma by metis
  qed simp
qed force+

corollary ‹⊩ z ⟹ ∃p. member p z ∧ semantics e f g p›
  using sound by force

corollary ‹⊩ [p] ⟹ semantics e f g p›
  using sound by force

corollary ‹¬ (⊩ [])›
  using sound by force

section ‹Reference›

text ‹Mordechai Ben-Ari (Springer 2012): Mathematical Logic for Computer Science (Third Edition)›

end

Theory Sequent1

theory Sequent1 imports "FOL_Seq_Calc1.Sequent"
begin

text ‹This theory exists exclusively as a shim to link the AFP theory imported here
  to the ‹Sequent_Calculus_Verifier› theory.›

end

Theory Sequent_Calculus_Verifier

(*
  Author: Jørgen Villadsen, DTU Compute, 2020
*)

section ‹Appendix: Completeness›

theory Sequent_Calculus_Verifier imports Sequent1 SeCaV begin

primrec from_tm and from_tm_list where
  ‹from_tm (Var n) = FOL_Fitting.Var n› |
  ‹from_tm (Fun a ts) = App a (from_tm_list ts)› |
  ‹from_tm_list [] = []› |
  ‹from_tm_list (t # ts) = from_tm t # from_tm_list ts›

primrec from_fm where
  ‹from_fm (Pre b ts) = Pred b (from_tm_list ts)› |
  ‹from_fm (Con p q) = And (from_fm p) (from_fm q)› |
  ‹from_fm (Dis p q) = Or (from_fm p) (from_fm q)› |
  ‹from_fm (Imp p q) = Impl (from_fm p) (from_fm q)› |
  ‹from_fm (Neg p) = FOL_Fitting.Neg (from_fm p)› |
  ‹from_fm (Uni p) = Forall (from_fm p)› |
  ‹from_fm (Exi p) = Exists (from_fm p)›

primrec to_tm and to_tm_list where
  ‹to_tm (FOL_Fitting.Var n) = Var n› |
  ‹to_tm (App a ts) = Fun a (to_tm_list ts)› |
  ‹to_tm_list [] = []› |
  ‹to_tm_list (t # ts) = to_tm t # to_tm_list ts›

primrec to_fm where
  ‹to_fm ⊥ = Neg (Imp (Pre 0 []) (Pre 0 []))› |
  ‹to_fm ⊤ = Imp (Pre 0 []) (Pre 0 [])› |
  ‹to_fm (Pred b ts) = Pre b (to_tm_list ts)› |
  ‹to_fm (And p q) = Con (to_fm p) (to_fm q)› |
  ‹to_fm (Or p q) = Dis (to_fm p) (to_fm q)› |
  ‹to_fm (Impl p q) = Imp (to_fm p) (to_fm q)› |
  ‹to_fm (FOL_Fitting.Neg p) = Neg (to_fm p)› |
  ‹to_fm (Forall p) = Uni (to_fm p)› |
  ‹to_fm (Exists p) = Exi (to_fm p)›

theorem to_from_tm [simp]: ‹to_tm (from_tm t) = t› ‹to_tm_list (from_tm_list ts) = ts›
  by (induct t and ts rule: from_tm.induct from_tm_list.induct) simp_all

theorem to_from_fm [simp]: ‹to_fm (from_fm p) = p›
  by (induct p) simp_all

lemma Truth [simp]: ‹⊩ Imp (Pre 0 []) (Pre 0 []) # z›
  using AlphaImp Basic Ext ext.simps member.simps(2) by metis

lemma paramst [simp]:
  ‹FOL_Fitting.new_term c t = new_term c (to_tm t)›
  ‹FOL_Fitting.new_list c l = new_list c (to_tm_list l)›
  by (induct t and l rule: FOL_Fitting.paramst.induct FOL_Fitting.paramsts.induct) simp_all

lemma params [iff]: ‹FOL_Fitting.new c p ⟷ new c (to_fm p)›
  by (induct p) simp_all

lemma list_params [iff]: ‹FOL_Fitting.news c z ⟷ news c (map to_fm z)›
  by (induct z) simp_all

lemma liftt [simp]:
  ‹to_tm (FOL_Fitting.liftt t) = inc_term (to_tm t)›
  ‹to_tm_list (FOL_Fitting.liftts l) = inc_list (to_tm_list l)›
  by (induct t and l rule: FOL_Fitting.liftt.induct FOL_Fitting.liftts.induct) simp_all

lemma substt [simp]:
  ‹to_tm (FOL_Fitting.substt t s v) = sub_term v (to_tm s) (to_tm t)›
  ‹to_tm_list (FOL_Fitting.substts l s v) = sub_list v (to_tm s) (to_tm_list l)›
  by (induct t and l rule: FOL_Fitting.substt.induct FOL_Fitting.substts.induct) simp_all

lemma subst [simp]: ‹to_fm (FOL_Fitting.subst A t s) = sub s (to_tm t) (to_fm A)›
  by (induct A arbitrary: t s) simp_all

lemma sim: ‹(⊢ x) ⟹ (⊩ (map to_fm x))›
  by (induct rule: SC.induct) (force intro: sequent_calculus.intros)+

lemma evalt [simp]:
  ‹semantics_term e f t = evalt e f (from_tm t)›
  ‹semantics_list e f ts = evalts e f (from_tm_list ts)›
  by (induct t and ts rule: from_tm.induct from_tm_list.induct) simp_all

lemma shift [simp]: ‹shift e 0 x = e⟨0:x⟩›
  unfolding shift_def FOL_Fitting.shift_def by simp

lemma semantics [iff]: ‹semantics e f g p ⟷ eval e f g (from_fm p)›
  by (induct p arbitrary: e) simp_all

abbreviation valid ("⪢ _" 0) where
  ‹(⪢ p) ≡ ∀(e :: _ ⇒ nat hterm) f g. semantics e f g p›

theorem complete_sound: ‹⪢ p ⟹ ⊩ [p]› ‹⊩ [q] ⟹ semantics e f g q›
  by (metis to_from_fm sim semantics list.map SC_completeness) (use sound in force)

corollary ‹(⪢ p) ⟷ (⊩ [p])›
  using complete_sound by fast

section ‹Reference›

text ‹Asta Halkjær From (2019): Sequent Calculus 🌐‹https://www.isa-afp.org/entries/FOL_Seq_Calc1.html››

end
iv class="head">

Theory Prover

chapter ‹The prover›

section ‹Proof search procedure›

theory Prover
  imports SeCaV
    "HOL-Library.Stream"
    Abstract_Completeness.Abstract_Completeness
    Abstract_Soundness.Finite_Proof_Soundness
    "HOL-Library.Countable"
    "HOL-Library.Code_Lazy"
begin

text ‹This theory defines the actual proof search procedure.›

subsection ‹Datatypes›

text ‹A sequent is a list of formulas›
type_synonym sequent = ‹fm list›

text ‹We introduce a number of rules to prove sequents.
  These rules mirror the proof system of SeCaV, but are higher-level in the sense that they apply to
  all formulas in the sequent at once. This obviates the need for the structural Ext rule.
  There is also no Basic rule, since this is implicit in the prover.›
datatype rule
  = AlphaDis | AlphaImp  | AlphaCon
  | BetaCon | BetaImp | BetaDis
  | DeltaUni | DeltaExi
  | NegNeg
  | GammaExi | GammaUni

subsection ‹Auxiliary functions›

text ‹Before defining what the rules do, we need to define a number of auxiliary functions needed
  for the semantics of the rules.›

text ‹listFunTm is a list of function and constant names in a term›
primrec listFunTm :: ‹tm ⇒ nat list› and listFunTms :: ‹tm list ⇒ nat list›where
  ‹listFunTm (Fun n ts) = n # listFunTms ts›
| ‹listFunTm (Var n) = []›
| ‹listFunTms [] = []›
| ‹listFunTms (t # ts) = listFunTm t @ listFunTms ts›

text ‹generateNew uses the ‹listFunTms› function to obtain a fresh function index›
definition generateNew :: ‹tm list ⇒ nat› where
  ‹generateNew ts ≡ 1 + foldr max (listFunTms ts) 0›

text ‹subtermTm returns a list of all terms occurring within a term›
primrec subtermTm :: ‹tm ⇒ tm list› where
  ‹subtermTm (Fun n ts) = Fun n ts # remdups (concat (map subtermTm ts))›
| ‹subtermTm (Var n) = [Var n]›

text ‹subtermFm returns a list of all terms occurring within a formula›
primrec subtermFm :: ‹fm ⇒ tm list› where
  ‹subtermFm (Pre _ ts) = concat (map subtermTm ts)›
| ‹subtermFm (Imp p q) = subtermFm p @ subtermFm q›
| ‹subtermFm (Dis p q) = subtermFm p @ subtermFm q›
| ‹subtermFm (Con p q) = subtermFm p @ subtermFm q›
| ‹subtermFm (Exi p) = subtermFm p›
| ‹subtermFm (Uni p) = subtermFm p›
| ‹subtermFm (Neg p) = subtermFm p›

text ‹subtermFms returns a list of all terms occurring within a list of formulas›
abbreviation ‹subtermFms z ≡ concat (map subtermFm z)›

text ‹subterms returns a list of all terms occurring within a sequent.
  This is used to determine which terms to instantiate Gamma-formulas with.
  We must always be able to instantiate Gamma-formulas, so if there are no terms in the sequent,
  the function simply returns a list containing the first function.›
definition subterms :: ‹sequent ⇒ tm list› where
  ‹subterms z ≡ case remdups (subtermFms z) of
                [] ⇒ [Fun 0 []]
              | ts ⇒ ts›

text ‹We need to be able to detect if a sequent is an axiom to know whether a branch of the proof
  is done. The disjunct ‹Neg (Neg p) ∈ set z› is not necessary for the prover, but makes the proof
  of the lemma ‹branchDone_contradiction› easier.›
fun branchDone :: ‹sequent ⇒ bool› where
  ‹branchDone [] = False›
| ‹branchDone (Neg p # z) = (p ∈ set z ∨ Neg (Neg p) ∈ set z ∨ branchDone z)›
| ‹branchDone (p # z) = (Neg p ∈ set z ∨ branchDone z)›

subsection ‹Effects of rules›

text ‹This defines the resulting formulas when applying a rule to a single formula.
  This definition mirrors the semantics of SeCaV.
  If the rule and the formula do not match, the resulting formula is simply the original formula.
  Parameter A should be the list of terms on the branch.›
definition parts :: ‹tm list ⇒ rule ⇒ fm ⇒ fm list list› where
  ‹parts A r f = (case (r, f) of
      (NegNeg, Neg (Neg p)) ⇒ [[p]]
    | (AlphaImp, Imp p q) ⇒ [[Neg p, q]]
    | (AlphaDis, Dis p q) ⇒ [[p, q]]
    | (AlphaCon, Neg (Con p q)) ⇒ [[Neg p, Neg q]]
    | (BetaImp, Neg (Imp p q)) ⇒ [[p], [Neg q]]
    | (BetaDis, Neg (Dis p q)) ⇒ [[Neg p], [Neg q]]
    | (BetaCon, Con p q) ⇒ [[p], [q]]
    | (DeltaExi, Neg (Exi p)) ⇒ [[Neg (sub 0 (Fun (generateNew A) []) p)]]
    | (DeltaUni, Uni p) ⇒ [[sub 0 (Fun (generateNew A) []) p]]
    | (GammaExi, Exi p) ⇒ [Exi p # map (λt. sub 0 t p) A]
    | (GammaUni, Neg (Uni p)) ⇒ [Neg (Uni p) # map (λt. Neg (sub 0 t p)) A]
    | _ ⇒ [[f]])›

text ‹This function defines the Cartesian product of two lists.
  This is needed to create the list of branches created when applying a beta rule.›
primrec list_prod :: ‹'a list list ⇒ 'a list list ⇒ 'a list list› where
  ‹list_prod _ [] = []›
| ‹list_prod hs (t # ts) = map (λh. h @ t) hs @ list_prod hs ts›

text ‹This function computes the children of a node in the proof tree.
  For Alpha rules, Delta rules and Gamma rules, there will be only one sequent, which is the result
  of applying the rule to every formula in the current sequent.
  For Beta rules, the proof tree will branch into two branches once for each formula in the sequent
  that matches the rule, which results in ‹2n› branches (created using text‹list_prod›).
  The list of terms in the sequent needs to be updated after applying the rule to each formula since
  Delta rules and Gamma rules may introduce new terms.
  Note that any formulas that don't match the rule are left unchanged in the new sequent.›
primrec children :: ‹tm list ⇒ rule ⇒ sequent ⇒ sequent list› where
  ‹children _ _ [] = [[]]›
| ‹children A r (p # z) =
  (let hs = parts A r p; A' = remdups (A @ subtermFms (concat hs))
   in list_prod hs (children A' r z))›

text ‹The proof state is the combination of a list of terms and a sequent.›
type_synonym state = ‹tm list × sequent›

text ‹This function defines the effect of applying a rule to a proof state.
  If the sequent is an axiom, the effect is to end the branch of the proof tree, so an empty set of
  child branches is returned.
  Otherwise, we compute the children generated by applying the rule to the current proof state,
  then add any new subterms to the proof states of the children.›
primrec effect :: ‹rule ⇒ state ⇒ state fset› where
  ‹effect r (A, z) =
  (if branchDone z then {||} else
    fimage (λz'. (remdups (A @ subterms z @ subterms z'), z'))
    (fset_of_list (children (remdups (A @ subtermFms z)) r z)))›

subsection ‹The rule stream›

text ‹We need to define an infinite stream of rules that the prover should try to apply.
  Since rules simply do nothing if they don't fit the formulas in the sequent, the rule stream is
  just all rules in the order: Alpha, Delta, Beta, Gamma, which guarantees completeness.›
definition ‹rulesList ≡ [
  NegNeg, AlphaImp, AlphaDis, AlphaCon,
  DeltaExi, DeltaUni,
  BetaImp, BetaDis, BetaCon,
  GammaExi, GammaUni
]›

text ‹By cycling the list of all rules we obtain an infinite stream with every rule occurring
  infinitely often.›
definition rules where
  ‹rules = cycle rulesList›

subsection ‹Abstract completeness›

text ‹We write effect as a relation to use it with the abstract completeness framework.›
definition eff where
  ‹eff ≡ λr s ss. effect r s = ss›

text ‹To use the framework, we need to prove enabledness.
  This is trivial because all of our rules are always enabled and simply do nothing if they don't
  match the formulas.›
lemma all_rules_enabled: ‹∀st. ∀r ∈ i.R (cycle rulesList). ∃sl. eff r st sl›
  unfolding eff_def by blast

text ‹The first step of the framework is to prove that our prover fits the framework.›
interpretation RuleSystem eff rules UNIV
  unfolding rules_def RuleSystem_def
  using all_rules_enabled stream.set_sel(1)
  by blast

text ‹Next, we need to prove that our rules are persistent.
  This is also trivial, since all of our rules are always enabled.›
lemma all_rules_persistent: ‹∀r. r ∈ R ⟶ per r›
  by (metis all_rules_enabled enabled_def per_def rules_def)

text ‹We can then prove that our prover fully fits the framework.›
interpretation PersistentRuleSystem eff rules UNIV
  unfolding PersistentRuleSystem_def RuleSystem_def PersistentRuleSystem_axioms_def
  using all_rules_persistent enabled_R
  by blast

text ‹We can then use the framework to define the prover.
  The mkTree function applies the rules to build the proof tree using the effect relation, but the
  prover is not actually executable yet.›
definition ‹secavProver ≡ mkTree rules›

abbreviation ‹rootSequent t ≡ snd (fst (root t))›

end
iv class="head">

Theory Export

section ‹Export›

theory Export
  imports Prover
begin

text ‹In this theory, we make the prover executable using the code interpretation of the abstract
completeness framework and the Isabelle to Haskell code generator.›

text ‹To actually execute the prover, we need to lazily evaluate the stream of rules to apply.
Otherwise, we will never actually get to a result.›
code_lazy_type stream

text ‹We would also like to make the evaluation of streams a bit more efficient.›
declare Stream.smember_code [code del]
lemma [code]: "Stream.smember x (y ## s) = (x = y ∨ Stream.smember x s)"
  unfolding Stream.smember_def by auto

text ‹To export code to Haskell, we need to specify that functions on the option type should be
  exported into the equivalent functions on the Maybe monad.›
code_printing
  constant the ⇀ (Haskell) "MaybeExt.fromJust"
| constant Option.is_none ⇀ (Haskell) "MaybeExt.isNothing"

text ‹To use the Maybe monad, we need to import it, so we add a shim to do so in every module.›
code_printing code_module MaybeExt ⇀ (Haskell)
  ‹module MaybeExt(fromJust, isNothing) where
     import Data.Maybe(fromJust, isNothing);›

text ‹The default export setup will create a cycle of module imports, so we roll most of the
  theories into one module when exporting to Haskell to prevent this.›
code_identifier
  code_module Stream ⇀ (Haskell) Prover
| code_module Prover ⇀ (Haskell) Prover
| code_module Export ⇀ (Haskell) Prover
| code_module Option ⇀ (Haskell) Prover
| code_module MaybeExt ⇀ (Haskell) Prover
| code_module Abstract_Completeness ⇀ (Haskell) Prover

text ‹Finally, we define an executable version of the prover using the code interpretation from the
  framework, and a version where the list of terms is initially empty.›
definition ‹secavTreeCode ≡ i.mkTree (λr s. Some (effect r s)) rules›
definition ‹secavProverCode ≡ λz . secavTreeCode ([], z)›

text ‹We then export this version of the prover into Haskell.›
export_code open secavProverCode in Haskell

end
dy>

Theory ProverLemmas

section ‹Lemmas about the prover›

theory ProverLemmas imports Prover begin

text ‹This theory contains a number of lemmas about the prover.
  We will need these when proving soundness and completeness.›

subsection ‹SeCaV lemmas›
text ‹We need a few lemmas about the SeCaV system.›

text ‹Incrementing variable indices does not change the function names in term or a list of terms.›
lemma paramst_liftt [simp]:
  ‹paramst (liftt t) = paramst t› ‹paramsts (liftts ts) = paramsts ts›
  by (induct t and ts rule: liftt.induct liftts.induct) auto

text ‹Subterms do not contain any functions except those in the original term›
lemma paramst_sub_term:
  ‹paramst (sub_term m s t) ⊆ paramst s ∪ paramst t›
  ‹paramsts (sub_list m s l) ⊆ paramst s ∪ paramsts l›
  by (induct t and l rule: sub_term.induct sub_list.induct) auto

text ‹Substituting a variable for a term does not introduce function names not in that term›
lemma params_sub: ‹params (sub m t p) ⊆ paramst t ∪ params p›
proof (induct p arbitrary: m t)
  case (Pre x1 x2)
  then show ?case
    using paramst_sub_term(2) by simp
qed fastforce+

abbreviation ‹paramss z ≡ ⋃p ∈ set z. params p›

text ‹If a function name is fresh, it is not in the list of function names in the sequent›
lemma news_paramss: ‹news i z ⟷ i ∉ paramss z›
  by (induct z) auto

text ‹If a list of terms is a subset of another, the set of function names in it is too›
lemma paramsts_subset: ‹set A ⊆ set B ⟹ paramsts A ⊆ paramsts B›
  by (induct A) auto

text ‹Substituting a variable by a term does not change the depth of a formula
  (only the term size changes)›
lemma size_sub [simp]: ‹size (sub i t p) = size p›
  by (induct p arbitrary: i t) auto

subsection ‹Fairness›
text ‹While fairness of the rule stream should be pretty trivial (since we are simply repeating a
  static list of rules forever), the proof is a bit involved.›

text ‹This function tells us what rule comes next in the stream.›
primrec next_rule :: ‹rule ⇒ rule› where
  ‹next_rule NegNeg = AlphaImp›
| ‹next_rule AlphaImp = AlphaDis›
| ‹next_rule AlphaDis = AlphaCon›
| ‹next_rule AlphaCon = DeltaExi›
| ‹next_rule DeltaExi = DeltaUni›
| ‹next_rule DeltaUni = BetaImp›
| ‹next_rule BetaImp = BetaDis›
| ‹next_rule BetaDis = BetaCon›
| ‹next_rule BetaCon = GammaExi›
| ‹next_rule GammaExi = GammaUni›
| ‹next_rule GammaUni = NegNeg›

text ‹This function tells us the index of a rule in the list of rules to repeat.›
primrec rule_index :: ‹rule ⇒ nat› where
  ‹rule_index NegNeg = 0›
| ‹rule_index AlphaImp = 1›
| ‹rule_index AlphaDis = 2›
| ‹rule_index AlphaCon = 3›
| ‹rule_index DeltaExi = 4›
| ‹rule_index DeltaUni = 5›
| ‹rule_index BetaImp = 6›
| ‹rule_index BetaDis = 7›
| ‹rule_index BetaCon = 8›
| ‹rule_index GammaExi = 9›
| ‹rule_index GammaUni = 10›

text ‹The list of rules does not have any duplicates.
  This is important because we can then look up rules by their index.›
lemma distinct_rulesList: ‹distinct rulesList›
  unfolding rulesList_def by simp

text ‹If you cycle a list, it repeats every ‹length› elements.›
lemma cycle_nth: ‹xs ≠ [] ⟹ cycle xs !! n = xs ! (n mod length xs)›
  by (metis cycle.sel(1) hd_rotate_conv_nth rotate_conv_mod sdrop_cycle sdrop_simps(1))

text ‹The rule index function can actually be used to look up rules in the list.›
lemma nth_rule_index: ‹rulesList ! (rule_index r) = r›
  unfolding rulesList_def by (cases r) simp_all

lemma rule_index_bnd: ‹rule_index r < length rulesList›
  unfolding rulesList_def by (cases r) simp_all

lemma unique_rule_index:
  assumes ‹n < length rulesList› ‹rulesList ! n = r›
  shows ‹n = rule_index r›
  using assms nth_rule_index distinct_rulesList rule_index_bnd nth_eq_iff_index_eq by metis

text ‹The rule indices repeat in the stream each cycle.›
lemma rule_index_mod:
  assumes ‹rules !! n = r›
  shows ‹n mod length rulesList = rule_index r›
proof -
  have *: ‹rulesList ! (n mod length rulesList) = r›
    using assms cycle_nth unfolding rules_def rulesList_def by (metis list.distinct(1))
  then show ?thesis
    using distinct_rulesList * unique_rule_index
    by (cases r) (metis length_greater_0_conv list.discI rulesList_def
        unique_euclidean_semiring_numeral_class.pos_mod_bound)+
qed

text ‹We need some lemmas about the modulo function to show that the rules repeat at the right rate.›
lemma mod_hit:
  fixes k :: nat
  assumes ‹0 < k›
  shows ‹∀i < k. ∃n > m. n mod k = i›
proof safe
  fix i
  let ?n = ‹(1 + m) * k + i›
  assume ‹i < k›
  then have ‹?n mod k = i›
    by (metis mod_less mod_mult_self3)
  moreover have ‹?n > m›
    using assms
    by (metis One_nat_def Suc_eq_plus1_left Suc_leI add.commute add_lessD1 less_add_one
        mult.right_neutral nat_mult_less_cancel1 order_le_less trans_less_add1 zero_less_one)
  ultimately show ‹∃n > m. n mod k = i›
    by fast
qed

lemma mod_suff:
  assumes ‹∀(n :: nat) > m. P (n mod k)› ‹0 < k›
  shows ‹∀i < k. P i›
  using assms mod_hit by blast

text ‹It is always possible to find an index after some point that results in any given rule.›
lemma rules_repeat: ‹∃n > m. rules !! n = r›
proof (rule ccontr)
  assume ‹¬ (∃n > m. rules !! n = r)›
  then have ‹¬ (∃n > m. n mod length rulesList = rule_index r)›
    using rule_index_mod nth_rule_index by metis
  then have ‹∀n > m. n mod length rulesList ≠ rule_index r›
    by blast
  moreover have ‹length rulesList > 0›
    unfolding rulesList_def by simp
  ultimately have ‹∀k < length rulesList. k ≠ rule_index r›
    using mod_suff[where P=‹λa. a ≠ rule_index r›] by blast
  then show False
    using rule_index_bnd by blast
qed

text ‹It is possible to find such an index no matter where in the stream we start.›
lemma rules_repeat_sdrop: ‹∃n. (sdrop k rules) !! n = r›
  using rules_repeat by (metis less_imp_add_positive sdrop_snth)

text ‹Using the lemma above, we prove that the stream of rules is fair by coinduction.›
lemma fair_rules: ‹fair rules›
proof -
  { fix r assume ‹r ∈ R›
    then obtain m where r: ‹r = rules !! m› unfolding sset_range by blast
    { fix n :: nat and rs let ?rules = ‹λn. sdrop n rules›
      assume ‹n > 0›
      then have ‹alw (ev (holds ((=) r))) (rs @- ?rules n)›
      proof (coinduction arbitrary: n rs)
        case alw
        show ?case
        proof (rule exI[of _ ‹rs @- ?rules n›], safe)
          show ‹∃n' rs'. stl (rs @- ?rules n) = rs' @- ?rules n' ∧ n' > 0›
          proof (cases rs)
            case Nil then show ?thesis unfolding alw
              by (metis sdrop_simps(2) shift.simps(1) zero_less_Suc)
          qed (auto simp: alw intro: exI[of _ n])
        next
          have ‹ev (holds ((=) r)) (sdrop n rules)›
            unfolding ev_holds_sset using rules_repeat_sdrop by (metis snth_sset)
          then show ‹ev (holds ((=) r)) (rs @- sdrop n rules)›
            unfolding ev_holds_sset by simp
        qed
      qed
    }
  }
  then show ‹fair rules› unfolding fair_def
    by (metis (full_types) alw_iff_sdrop ev_holds_sset neq0_conv order_refl sdrop.simps(1)
        stake_sdrop)
qed

subsection ‹Substitution›
text ‹We need some lemmas about substitution of variables for terms for the Delta and Gamma rules.›

text ‹If a term is a subterm of another, so are all of its subterms.›
lemma subtermTm_le: ‹t ∈ set (subtermTm s) ⟹ set (subtermTm t) ⊆ set (subtermTm s)›
  by (induct s) auto

text ‹Trying to substitute a variable that is not in the term does nothing (contrapositively).›
lemma sub_term_const_transfer:
  ‹sub_term m (Fun a []) t ≠ sub_term m s t ⟹
    Fun a [] ∈ set (subtermTm (sub_term m (Fun a []) t))›
  ‹sub_list m (Fun a []) ts ≠ sub_list m s ts ⟹
    Fun a [] ∈ (⋃t ∈ set (sub_list m (Fun a []) ts). set (subtermTm t))›
proof (induct t and ts rule: sub_term.induct sub_list.induct)
  case (Var x)
  then show ?case
    by (metis list.set_intros(1) sub_term.simps(1) subtermTm.simps(1))
qed auto

text ‹If substituting different terms makes a difference, then the substitution has an effect.›
lemma sub_const_transfer:
  assumes ‹sub m (Fun a []) p ≠ sub m t p›
  shows ‹Fun a [] ∈ set (subtermFm (sub m (Fun a []) p))›
  using assms
proof (induct p arbitrary: m t)
  case (Pre i l)
  then show ?case
    using sub_term_const_transfer(2) by simp
qed auto

text ‹If the list of subterms is empty for all formulas in a sequent, constant 0 is used instead.›
lemma set_subterms:
  fixes z
  defines ‹ts ≡ ⋃p ∈ set z. set (subtermFm p)›
  shows ‹set (subterms z) = (if ts = {} then {Fun 0 []} else ts)›
proof -
  have *: ‹set (remdups (concat (map subtermFm z))) = (⋃p ∈ set z. set (subtermFm p))›
    by (induct z) auto
  then show ?thesis
  proof (cases ‹ts = {}›)
    case True
    then show ?thesis
      unfolding subterms_def ts_def using *
      by (metis list.simps(15) list.simps(4) set_empty)
  next
    case False
    then show ?thesis
      unfolding subterms_def ts_def using *
      by (metis empty_set list.exhaust list.simps(5))
  qed
qed

text ‹The parameters and the subterm functions respect each other.›
lemma paramst_subtermTm:
  ‹∀i ∈ paramst t. ∃l. Fun i l ∈ set (subtermTm t)›
  ‹∀i ∈ paramsts ts. ∃l. Fun i l ∈ (⋃t ∈ set ts. set (subtermTm t))›
  by (induct t and ts rule: paramst.induct paramsts.induct) fastforce+

lemma params_subtermFm: ‹∀i ∈ params p. ∃l. Fun i l ∈ set (subtermFm p)›
proof (induct p)
  case (Pre x1 x2)
  then show ?case
    using paramst_subtermTm by simp
qed auto

lemma subtermFm_subset_params: ‹set (subtermFm p) ⊆ set A ⟹ params p ⊆ paramsts A›
  using params_subtermFm by force

subsection ‹Custom cases›
text ‹Some proofs are more efficient with some custom case lemmas.›

lemma Neg_exhaust
  [case_names Pre Imp Dis Con Exi Uni NegPre NegImp NegDis NegCon NegExi NegUni NegNeg]:
  assumes
    ‹⋀i ts. x = Pre i ts ⟹ P›
    ‹⋀p q. x = Imp p q ⟹ P›
    ‹⋀p q. x = Dis p q ⟹ P›
    ‹⋀p q. x = Con p q ⟹ P›
    ‹⋀p. x = Exi p ⟹ P›
    ‹⋀p. x = Uni p ⟹ P›
    ‹⋀i ts. x = Neg (Pre i ts) ⟹ P›
    ‹⋀p q. x = Neg (Imp p q) ⟹ P›
    ‹⋀p q. x = Neg (Dis p q) ⟹ P›
    ‹⋀p q. x = Neg (Con p q) ⟹ P›
    ‹⋀p. x = Neg (Exi p) ⟹ P›
    ‹⋀p. x = Neg (Uni p) ⟹ P›
    ‹⋀p. x = Neg (Neg p) ⟹ P›
  shows P
  using assms
proof (induct x)
  case (Neg p)
  then show ?case
    by (cases p) simp_all
qed simp_all

lemma parts_exhaust
  [case_names AlphaDis AlphaImp AlphaCon BetaDis BetaImp BetaCon
    DeltaUni DeltaExi NegNeg GammaExi GammaUni Other]:
  assumes
    ‹⋀p q. r = AlphaDis ⟹ x = Dis p q ⟹ P›
    ‹⋀p q. r = AlphaImp ⟹ x = Imp p q ⟹ P›
    ‹⋀p q. r = AlphaCon ⟹ x = Neg (Con p q) ⟹ P›
    ‹⋀p q. r = BetaDis ⟹ x = Neg (Dis p q) ⟹ P›
    ‹⋀p q. r = BetaImp ⟹ x = Neg (Imp p q) ⟹ P›
    ‹⋀p q. r = BetaCon ⟹ x = Con p q ⟹ P›
    ‹⋀p. r = DeltaUni ⟹ x = Uni p ⟹ P›
    ‹⋀p. r = DeltaExi ⟹ x = Neg (Exi p) ⟹ P›
    ‹⋀p. r = NegNeg ⟹ x = Neg (Neg p) ⟹ P›
    ‹⋀p. r = GammaExi ⟹ x = Exi p ⟹ P›
    ‹⋀p. r = GammaUni ⟹ x = Neg (Uni p) ⟹ P›
    ‹∀A. parts A r x = [[x]] ⟹ P›
  shows P
  using assms
proof (cases r)
  case BetaCon
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (Con p q)
    then show ?thesis
      using BetaCon assms by blast
  qed (simp_all add: parts_def)
next
  case BetaImp
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegImp p q)
    then show ?thesis
      using BetaImp assms by blast
  qed (simp_all add: parts_def)
next
  case DeltaUni
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (Uni p)
    then show ?thesis
      using DeltaUni assms by fast
  qed (simp_all add: parts_def)
next
  case DeltaExi
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegExi p)
    then show ?thesis
      using DeltaExi assms by fast
  qed (simp_all add: parts_def)
next
  case n: NegNeg
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegNeg p)
    then show ?thesis
      using n assms by fast
  qed (simp_all add: parts_def)
next
  case GammaExi
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (Exi p)
    then show ?thesis
      using GammaExi assms by fast
  qed (simp_all add: parts_def)
next
  case GammaUni
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegUni p)
    then show ?thesis
      using GammaUni assms by fast
  qed (simp_all add: parts_def)
qed (cases x rule: Neg_exhaust, simp_all add: parts_def)+

subsection ‹Unaffected formulas›
text ‹We need some lemmas to show that formulas to which rules do not apply are not lost.›

text ‹This function returns True if the rule applies to the formula, and False otherwise.›
definition affects :: ‹rule ⇒ fm ⇒ bool› where
  ‹affects r p ≡ case (r, p) of
    (AlphaDis, Dis _ _) ⇒ True
  | (AlphaImp, Imp _ _) ⇒ True
  | (AlphaCon, Neg (Con _ _)) ⇒ True
  | (BetaCon, Con _ _) ⇒ True
  | (BetaImp, Neg (Imp _ _)) ⇒ True
  | (BetaDis, Neg (Dis _ _)) ⇒ True
  | (DeltaUni, Uni _) ⇒ True
  | (DeltaExi, Neg (Exi _)) ⇒ True
  | (NegNeg, Neg (Neg _)) ⇒ True
  | (GammaExi, Exi _) ⇒ False
  | (GammaUni, Neg (Uni _)) ⇒ False
  | (_,  _) ⇒ False›

text ‹If a rule does not affect a formula, that formula will be in the sequent obtained after
  applying the rule.›
lemma parts_preserves_unaffected:
  assumes ‹¬ affects r p› ‹z' ∈ set (parts A r p)›
  shows ‹p ∈ set z'›
  using assms unfolding affects_def
  by (cases r p rule: parts_exhaust) (simp_all add: parts_def)

text ‹The ‹list_prod› function computes the Cartesian product.›
lemma list_prod_is_cartesian:
  ‹set (list_prod hs ts) = {h @ t |h t. h ∈ set hs ∧ t ∈ set ts}›
  by (induct ts) auto

text ‹The ‹children› function produces the Cartesian product of the branches from the first formula
and the branches from the rest of the sequent.›
lemma set_children_Cons:
  ‹set (children A r (p # z)) =
    {hs @ ts |hs ts. hs ∈ set (parts A r p) ∧
      ts ∈ set (children (remdups (A @ subtermFms (concat (parts A r p)))) r z)}›
  using list_prod_is_cartesian by (metis children.simps(2))

text ‹The ‹children› function does not change unaffected formulas.›
lemma children_preserves_unaffected:
  assumes ‹p ∈ set z› ‹¬ affects r p› ‹z' ∈ set (children A r z)›
  shows ‹p ∈ set z'›
  using assms parts_preserves_unaffected set_children_Cons
  by (induct z arbitrary: A z') auto

text ‹The ‹effect› function does not change unaffected formulas.›
lemma effect_preserves_unaffected:
  assumes ‹p ∈ set z› and ‹¬ affects r p› and ‹(B, z') |∈| effect r (A, z)›
  shows ‹p ∈ set z'›
  using assms children_preserves_unaffected
  unfolding effect_def
  by (smt (verit, best) Pair_inject femptyE fimageE fset_of_list_elem old.prod.case)

subsection ‹Affected formulas›
text ‹We need some lemmas to show that formulas to which rules do apply are decomposed into their
  constituent parts correctly.›

text ‹If a formula occurs in a sequent on a child branch generated by ‹children›, it was part of
  the current sequent.›
lemma parts_in_children:
  assumes ‹p ∈ set z› ‹z' ∈ set (children A r z)›
  shows ‹∃B xs. set A ⊆ set B ∧ xs ∈ set (parts B r p) ∧ set xs ⊆ set z'›
  using assms
proof (induct z arbitrary: A z')
  case (Cons a _)
  then show ?case
  proof (cases ‹a = p›)
    case True
    then show ?thesis
      using Cons(3) set_children_Cons by fastforce
  next
    case False
    then show ?thesis
      using Cons set_children_Cons
      by (smt (verit, del_insts) le_sup_iff mem_Collect_eq set_ConsD set_append set_remdups subset_trans sup_ge2)
  qed
qed simp

text ‹If ‹effect› contains something, then the input sequent is not an axiom.›
lemma ne_effect_not_branchDone: ‹(B, z') |∈| effect r (A, z) ⟹ ¬ branchDone z›
  by (cases ‹branchDone z›) simp_all

text ‹The ‹effect› function decomposes formulas in the sequent using the ‹parts› function.
  (Unless the sequent is an axiom, in which case no child branches are generated.)›
lemma parts_in_effect:
  assumes ‹p ∈ set z› and ‹(B, z') |∈| effect r (A, z)›
  shows ‹∃C xs. set A ⊆ set C ∧ xs ∈ set (parts C r p) ∧ set xs ⊆ set z'›
  using assms parts_in_children ne_effect_not_branchDone
  by (smt (verit, ccfv_threshold) Pair_inject effect.simps fimageE fset_of_list_elem le_sup_iff
      set_append set_remdups)

text ‹Specifically, this applied to the double negation elimination rule and the GammaUni rule.›
corollary ‹Neg (Neg p) ∈ set z ⟹ (B, z') |∈| effect NegNeg (A, z) ⟹ p ∈ set z'›
  using parts_in_effect unfolding parts_def by fastforce

corollary ‹Neg (Uni p) ∈ set z ⟹ (B, z') |∈| effect GammaUni (A, z) ⟹
    set (map (λt. Neg (sub 0 t p)) A) ⊆ set z'›
  using parts_in_effect unfolding parts_def by fastforce

text ‹If the sequent is not an axiom, and the rule and sequent match, all of the child branches
  generated by ‹children› will be included in the proof tree.›
lemma eff_children:
  assumes ‹¬ branchDone z› ‹eff r (A, z) ss›
  shows ‹∀z' ∈ set (children (remdups (A @ subtermFms z)) r z). ∃B. (B, z') |∈| ss›
  using assms unfolding eff_def using fset_of_list_elem by fastforce

subsection ‹Generating new function names›
text ‹We need to show that the ‹generateNew› function actually generates new function names.
  This requires a few lemmas about the interplay between ‹max› and ‹foldr›.›

lemma foldr_max:
  fixes xs :: ‹nat list›
  shows ‹foldr max xs 0 = (if xs = [] then 0 else Max (set xs))›
  by (induct xs) simp_all

lemma Suc_max_new:
  fixes xs :: ‹nat list›
  shows ‹Suc (foldr max xs 0) ∉ set xs›
proof (cases xs)
  case (Cons x xs)
  then have ‹foldr max (x # xs) 0 = Max (set (x # xs))›
    using foldr_max by simp
  then show ?thesis
    using Cons by (metis List.finite_set Max.insert add_0 empty_iff list.set(2) max_0_1(2)
        n_not_Suc_n nat_add_max_left plus_1_eq_Suc remdups.simps(2) set_remdups)
qed simp

lemma listFunTm_paramst: ‹set (listFunTm t) = paramst t› ‹set (listFunTms ts) = paramsts ts›
  by (induct t and ts rule: paramst.induct paramsts.induct) auto

subsection ‹Finding axioms›

text ‹The ‹branchDone› function correctly determines whether a sequent is an axiom.›
lemma branchDone_contradiction: ‹branchDone z ⟷ (∃p. p ∈ set z ∧ Neg p ∈ set z)›
  by (induct z rule: branchDone.induct) auto

subsection ‹Subterms›
text ‹We need a few lemmas about the behaviour of our subterm functions.›

text ‹Any term is a subterm of itself.›
lemma subtermTm_refl [simp]: ‹t ∈ set (subtermTm t)›
  by (induct t) simp_all

text ‹The arguments of a predicate are subterms of it.›
lemma subterm_Pre_refl: ‹set ts ⊆ set (subtermFm (Pre n ts))›
  by (induct ts) auto

text ‹The arguments of function are subterms of it.›
lemma subterm_Fun_refl: ‹set ts ⊆ set (subtermTm (Fun n ts))›
  by (induct ts) auto

text ‹This function computes the predicates in a formula.
  We will use this function to help prove the final lemma in this section.›
primrec preds :: ‹fm ⇒ fm set› where
  ‹preds (Pre n ts) = {Pre n ts}›
| ‹preds (Imp p q) = preds p ∪ preds q›
| ‹preds (Dis p q) = preds p ∪ preds q›
| ‹preds (Con p q) = preds p ∪ preds q›
| ‹preds (Exi p) = preds p›
| ‹preds (Uni p) = preds p›
| ‹preds (Neg p) = preds p›

text ‹If a term is a subterm of a formula, it is a subterm of some predicate in the formula.›
lemma subtermFm_preds: ‹t ∈ set (subtermFm p) ⟷ (∃pre ∈ preds p. t ∈ set (subtermFm pre))›
  by (induct p) auto

lemma preds_shape: ‹pre ∈ preds p ⟹ ∃n ts. pre = Pre n ts›
  by (induct p) auto

text ‹If a function is a subterm of a formula, so are the arguments of that function.›
lemma fun_arguments_subterm:
  assumes ‹Fun n ts ∈ set (subtermFm p)›
  shows ‹set ts ⊆ set (subtermFm p)›
proof -
  obtain pre where pre: ‹pre ∈ preds p› ‹Fun n ts ∈ set (subtermFm pre)›
    using assms subtermFm_preds by blast
  then obtain n' ts' where ‹pre = Pre n' ts'›
    using preds_shape by blast
  then have ‹set ts ⊆ set (subtermFm pre)›
    using subtermTm_le pre by force
  then have ‹set ts ⊆ set (subtermFm p)›
    using pre subtermFm_preds by blast
  then show ?thesis
    by blast
qed

end

Theory Hintikka

section ‹Hintikka sets for SeCaV›

theory Hintikka
  imports Prover
begin

text ‹In this theory, we define the concept of a Hintikka set for SeCaV formulas.
  The definition mirrors the SeCaV proof system such that Hintikka sets are downwards closed with
  respect to the proof system.›

text ‹This defines the set of all terms in a set of formulas (containing ‹Fun 0 []› if it would
  otherwise be empty).›
definition
  ‹terms H ≡ if (⋃p ∈ H. set (subtermFm p)) = {} then {Fun 0 []}
    else (⋃p ∈ H. set (subtermFm p))›

locale Hintikka =
  fixes H :: ‹fm set›
  assumes
    Basic: ‹Pre n ts ∈ H ⟹ Neg (Pre n ts) ∉ H› and
    AlphaDis: ‹Dis p q ∈ H ⟹ p ∈ H ∧ q ∈ H› and
    AlphaImp: ‹Imp p q ∈ H ⟹ Neg p ∈ H ∧ q ∈ H› and
    AlphaCon: ‹Neg (Con p q) ∈ H ⟹ Neg p ∈ H ∧ Neg q ∈ H› and
    BetaCon: ‹Con p q ∈ H ⟹ p ∈ H ∨ q ∈ H› and
    BetaImp: ‹Neg (Imp p q) ∈ H ⟹ p ∈ H ∨ Neg q ∈ H› and
    BetaDis: ‹Neg (Dis p q) ∈ H ⟹ Neg p ∈ H ∨ Neg q ∈ H› and
    GammaExi: ‹Exi p ∈ H ⟹ ∀t ∈ terms H. sub 0 t p ∈ H› and
    GammaUni: ‹Neg (Uni p) ∈ H ⟹ ∀t ∈ terms H. Neg (sub 0 t p) ∈ H› and
    DeltaUni: ‹Uni p ∈ H ⟹ ∃t ∈ terms H. sub 0 t p ∈ H› and
    DeltaExi: ‹Neg (Exi p) ∈ H ⟹ ∃t ∈ terms H. Neg (sub 0 t p) ∈ H› and
    Neg: ‹Neg (Neg p) ∈ H ⟹ p ∈ H›

end
ody>

Theory EPathHintikka

section ‹Escape path formulas are Hintikka›

theory EPathHintikka imports Hintikka ProverLemmas begin

text ‹In this theory, we show that the formulas in the sequents on a saturated escape path in a
  proof tree form a Hintikka set.
  This is a crucial part of our completeness proof.›

subsection ‹Definitions›
text ‹In this section we define a few concepts that make the following proofs easier to read.›

text ‹‹pseq› is the sequent in a node.›
definition pseq :: ‹state × rule ⇒ sequent› where
  ‹pseq z = snd (fst z)›

text ‹‹ptms› is the list of terms in a node.›
definition ptms :: ‹state × rule ⇒ tm list› where
  ‹ptms z = fst (fst z)›

subsection ‹Facts about streams›

text ‹Escape paths are infinite, so if you drop the first ‹n› nodes, you are still on the path.›
lemma epath_sdrop: ‹epath steps ⟹ epath (sdrop n steps)›
  by (induct n) (auto elim: epath.cases)

text ‹Dropping the first ‹n› elements of a stream can only reduce the set of elements in the stream.›
lemma sset_sdrop: ‹sset (sdrop n s) ⊆ sset s›
proof (induct n arbitrary: s)
  case (Suc n)
  then show ?case
    by (metis in_mono sdrop_simps(2) stl_sset subsetI)
qed simp

subsection  ‹Transformation of states on an escape path›
text ‹We need to prove some lemmas about how the states of an escape path are connected.›

text ‹Since escape paths are well-formed, the eff relation holds between the nodes on the path.›
lemma epath_eff:
  assumes ‹epath steps› ‹eff (snd (shd steps)) (fst (shd steps)) ss›
  shows ‹fst (shd (stl steps)) |∈| ss›
  using assms by (metis (mono_tags, lifting) epath.simps eff_def)

text ‹The list of terms in a state contains the terms of the current sequent and the terms from the
  previous state.›
lemma effect_tms:
  assumes ‹(B, z') |∈| effect r (A, z)›
  shows ‹B = remdups (A @ subterms z @ subterms z')›
  using assms by (smt (verit, best) effect.simps fempty_iff fimageE prod.simps(1))

text ‹The two previous lemmas can be combined into a single lemma.›
lemma epath_effect:
  assumes ‹epath steps› ‹shd steps = ((A, z), r)›
  shows ‹∃B z' r'. (B, z') |∈| effect r (A, z) ∧ shd (stl steps) = ((B, z'), r') ∧
          (B = remdups (A @ subterms z @ subterms z'))›
  using assms epath_eff effect_tms
  by (metis (mono_tags, lifting) eff_def fst_conv prod.collapse snd_conv)

text ‹The list of terms in the next state on an escape path contains the terms in the current state
  plus the terms from the next state.›
lemma epath_stl_ptms:
  assumes ‹epath steps›
  shows ‹ptms (shd (stl steps)) = remdups (ptms (shd steps) @
    subterms (pseq (shd steps)) @ subterms (pseq (shd (stl steps))))›
  using assms epath_effect
  by (metis (mono_tags) eff_def effect_tms epath_eff pseq_def ptms_def surjective_pairing)

text ‹The list of terms never decreases on an escape path.›
lemma epath_sdrop_ptms:
  assumes ‹epath steps›
  shows ‹set (ptms (shd steps)) ⊆ set (ptms (shd (sdrop n steps)))›
  using assms
proof (induct n)
  case (Suc n)
  then have ‹epath (sdrop n steps)›
    using epath_sdrop by blast
  then show ?case
    using Suc epath_stl_ptms by fastforce
qed simp

subsection ‹Preservation of formulas on escape paths›

text ‹If a property will eventually hold on a path, there is some index from which it begins to
  hold, and before which it does not hold.›
lemma ev_prefix_sdrop:
  assumes ‹ev (holds P) xs›
  shows ‹∃n. list_all (not P) (stake n xs) ∧ holds P (sdrop n xs)›
  using assms
proof (induct xs)
  case (base xs)
  then show ?case
    by (metis list.pred_inject(1) sdrop.simps(1) stake.simps(1))
next
  case (step xs)
  then show ?case
    by (metis holds.elims(1) list.pred_inject(2) list_all_simps(2) sdrop.simps(1-2) stake.simps(1-2))
qed

text ‹More specifically, the path will consists of a prefix and a suffix for which the property
  does not hold and does hold, respectively.›
lemma ev_prefix:
  assumes ‹ev (holds P) xs›
  shows ‹∃pre suf. list_all (not P) pre ∧ holds P suf ∧ xs = pre @- suf›
  using assms ev_prefix_sdrop by (metis stake_sdrop)

text ‹All rules are always enabled, so they are also always enabled at specific steps.›
lemma always_enabledAtStep: ‹enabledAtStep r xs›
  by (simp add: RuleSystem_Defs.enabled_def eff_def)

text ‹If a formula is in the sequent in the first state of an escape path and none of the rule
  applications in some prefix of the path affect that formula, the formula will still be in the
  sequent after that prefix.›
lemma epath_preserves_unaffected:
  assumes ‹p ∈ set (pseq (shd steps))› and ‹epath steps› and ‹steps = pre @- suf› and
    ‹list_all (not (λstep. affects (snd step) p)) pre›
  shows ‹p ∈ set (pseq (shd suf))›
  using assms
proof (induct pre arbitrary: steps)
  case Nil
  then show ?case
    by simp
next
  case (Cons q pre)
  from this(3) show ?case
  proof cases
    case (epath sl)
    from this(2-4) show ?thesis
      using Cons(1-2, 4-5) effect_preserves_unaffected unfolding eff_def pseq_def list_all_def
      by (metis (no_types, lifting) list.sel(1) list.set_intros(1-2) prod.exhaust_sel
          shift.simps(2) shift_simps(1) stream.sel(2))
  qed
qed

subsection ‹Formulas on an escape path form a Hintikka set›

text ‹This definition captures the set of formulas on an entire path›
definition ‹tree_fms steps ≡ ⋃ss ∈ sset steps. set (pseq ss)›

text ‹The sequent at the head of a path is in the set of formulas on that path›
lemma pseq_in_tree_fms: ‹⟦x ∈ sset steps; p ∈ set (pseq x)⟧ ⟹ p ∈ tree_fms steps›
  using pseq_def tree_fms_def by blast

text ‹If a formula is in the set of formulas on a path, there is some index on the path where that
  formula can be found in the sequent.›
lemma tree_fms_in_pseq: ‹p ∈ tree_fms steps ⟹ ∃n. p ∈ set (pseq (steps !! n))›
  unfolding pseq_def tree_fms_def using sset_range[of steps] by simp

text ‹If a path is saturated, so is any suffix of that path (since saturation is defined in terms of
  the always operator).›
lemma Saturated_sdrop: ‹Saturated steps ⟹ Saturated (sdrop n steps)›
  by (simp add: RuleSystem_Defs.Saturated_def alw_iff_sdrop saturated_def)

text ‹This is an abbreviation that determines whether a given rule is applied in a given state.›
abbreviation ‹is_rule r step ≡ snd step = r›

text ‹If a path is saturated, it is always possible to find a state in which a given rule is applied.›
lemma Saturated_ev_rule:
  assumes ‹Saturated steps›
  shows ‹ev (holds (is_rule r)) (sdrop n steps)›
proof -
  have ‹Saturated (sdrop n steps)›
    using ‹Saturated steps› Saturated_sdrop by fast
  moreover have ‹r ∈ Prover.R›
    by (metis rules_repeat snth_sset)
  ultimately have ‹saturated r (sdrop n steps)›
    unfolding Saturated_def by fast
  then show ?thesis
    unfolding saturated_def using always_enabledAtStep holds.elims(3) by blast
qed

text ‹On an escape path, the sequent is never an axiom (since that would end the branch, and escape
  paths are infinitely long).›
lemma epath_never_branchDone:
  assumes ‹epath steps›
  shows ‹alw (holds (not (branchDone o pseq))) steps›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then have ‹ev (holds (branchDone o pseq)) steps›
    by (simp add: alw_iff_sdrop ev_iff_sdrop)
  then obtain n where n: ‹holds (branchDone o pseq) (sdrop n steps)›
    using sdrop_wait by blast
  let ?suf = ‹sdrop n steps›
  have ‹∀r A. effect r (A, pseq (shd ?suf)) = {||}›
    unfolding effect_def using n by simp
  moreover have ‹epath ?suf›
    using ‹epath steps› epath_sdrop by blast
  then have ‹∀r A. ∃z' r'. z' |∈| effect r (A, pseq (shd ?suf)) ∧ shd (stl ?suf) = (z', r')›
    using epath_effect by (metis calculation prod.exhaust_sel pseq_def)
  ultimately show False
    by blast
qed

text ‹Finally we arrive at the main result of this theory:
  The set of formulas on a saturated escape path form a Hintikka set.

  The proof basically says that, given a formula, we can find some index into the path where a rule
  is applied to decompose that formula into the parts needed for the Hintikka set.
  The lemmas above are used to guarantee that the formula does not disappear (and that the branch
  does not end) before the rule is applied, and that the correct formulas are generated by the
  effect function when the rule is finally applied.
  For Beta rules, only one of the constituent formulas need to be on the path, since the path runs
  along only one of the two branches.
  For Gamma and Delta rules, the construction of the list of terms in each state guarantees that
  the formulas are instantiated with terms in the Hintikka set.›
lemma escape_path_Hintikka:
  assumes ‹epath steps› and ‹Saturated steps›
  shows ‹Hintikka (tree_fms steps)›
    (is ‹Hintikka ?H›)
proof
  fix n ts
  assume pre: ‹Pre n ts ∈ ?H›
  then obtain m where m: ‹Pre n ts ∈ set (pseq (shd (sdrop m steps)))›
    using tree_fms_in_pseq by auto

  show ‹Neg (Pre n ts) ∉ ?H›
  proof
    assume ‹Neg (Pre n ts) ∈ ?H›
    then obtain k where k: ‹Neg (Pre n ts) ∈ set (pseq (shd (sdrop k steps)))›
      using tree_fms_in_pseq by auto

    let ?pre = ‹stake (m + k) steps›
    let ?suf = ‹sdrop (m + k) steps›

    have
      1: ‹¬ affects r (Pre n ts)› and
      2: ‹¬ affects r (Neg (Pre n ts))› for r
      unfolding affects_def by (cases r, simp_all)+

    have ‹list_all (not (λstep. affects (snd step) (Pre n ts))) ?pre›
      unfolding list_all_def using 1 by (induct ?pre) simp_all
    then have p: ‹Pre n ts ∈ set (pseq (shd ?suf))›
      using ‹epath steps› epath_preserves_unaffected m epath_sdrop
      by (metis (no_types, lifting) list.pred_mono_strong list_all_append
          sdrop_add stake_add stake_sdrop)

    have ‹list_all (not (λstep. affects (snd step) (Neg (Pre n ts)))) ?pre›
      unfolding list_all_def using 2 by (induct ?pre) simp_all
    then have np: ‹Neg (Pre n ts) ∈ set (pseq (shd ?suf))›
      using ‹epath steps› epath_preserves_unaffected k epath_sdrop
      by (smt (verit, best) add.commute list.pred_mono_strong list_all_append sdrop_add
          stake_add stake_sdrop)

    have ‹holds (branchDone o pseq) ?suf›
      using p np branchDone_contradiction by auto
    moreover have ‹¬ holds (branchDone o pseq) ?suf›
      using ‹epath steps› epath_never_branchDone by (simp add: alw_iff_sdrop)
    ultimately show False
      by blast
  qed
next
  fix p q
  assume ‹Dis p q ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = AlphaDis
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately have ‹p ∈ set z'› ‹q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce+

  then show ‹p ∈ ?H ∧ q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Imp p q ∈ tree_fms steps› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = AlphaImp
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately have ‹Neg p ∈ set z'› ‹q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce+

  then show ‹Neg p ∈ ?H ∧ q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Neg (Con p q) ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = AlphaCon
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately have ‹Neg p ∈ set z'› ‹Neg q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce+

  then show ‹Neg p ∈ ?H ∧ Neg q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Con p q ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = BetaCon
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately consider ‹p ∈ set z'› | ‹q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce

  then show ‹p ∈ ?H ∨ q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Neg (Imp p q) ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = BetaImp
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately consider ‹p ∈ set z'› | ‹Neg q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce

  then show ‹p ∈ ?H ∨ Neg q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Neg (Dis p q) ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = BetaDis
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately consider ‹Neg p ∈ set z'› | ‹Neg q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce

  then show ‹Neg p ∈ ?H ∨ Neg q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p
  assume ‹Exi p ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto

  let ?r = GammaExi

  show ‹∀t ∈ terms ?H. sub 0 t p ∈ ?H›
  proof
    fix t
    assume t: ‹t ∈ terms ?H›
    show ‹sub 0 t p ∈ ?H›
    proof -
      have ‹∃m. t ∈ set (subterms (pseq (shd (sdrop m steps))))›
      proof (cases ‹(⋃f ∈ ?H. set (subtermFm f)) = {}›)
        case True
        moreover have ‹∀p ∈ set (pseq (shd steps)). p ∈ ?H›
          unfolding tree_fms_def by (metis pseq_in_tree_fms shd_sset tree_fms_def)
        ultimately have ‹∀p ∈ set (pseq (shd steps)). subtermFm p = []›
          by simp
        then have ‹concat (map subtermFm (pseq (shd steps))) = []›
          by (induct ‹pseq (shd steps)›) simp_all
        then have ‹subterms (pseq (shd steps)) = [Fun 0 []]›
          unfolding subterms_def by (metis list.simps(4) remdups_eq_nil_iff)
        then show ?thesis
          using True t unfolding terms_def
          by (metis empty_iff insert_iff list.set_intros(1) sdrop.simps(1))
      next
        case False
        then obtain pt where pt: ‹t ∈ set (subtermFm pt)› ‹pt ∈ ?H›
          using t unfolding terms_def by (metis