# 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âº |

â â¹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 AlphaImp = sequent_calculus.intros(3)
lemmas AlphaCon = sequent_calculus.intros(4)

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

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âº

[
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

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


# 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
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 â¹2â§nâº 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 â¡ [
DeltaExi, DeltaUni,
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


# 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 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.âº
â¹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 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.âº

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 AlphaCon = DeltaExiâº
| â¹next_rule DeltaExi = DeltaUniâº
| â¹next_rule DeltaUni = BetaImpâº
| â¹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 AlphaCon = 3âº
| â¹rule_index DeltaExi = 4âº
| â¹rule_index DeltaUni = 5âº
| â¹rule_index BetaImp = 6âº
| â¹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
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
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
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
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
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
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
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
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 (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)
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)âº

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âº

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âº
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

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

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âº
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âº
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