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 (no_types, lifting) UN_E) then obtain m where m: ‹pt ∈ set (pseq (shd (sdrop m steps)))› using tree_fms_in_pseq by auto then show ?thesis using pt(1) set_subterms by fastforce qed then obtain m where ‹t ∈ set (subterms (pseq (shd (sdrop m steps))))› by blast then have ‹t ∈ set (ptms (shd (stl (sdrop m steps))))› using epath_stl_ptms epath_sdrop ‹epath steps› by (metis (no_types, opaque_lifting) Un_iff set_append set_remdups) moreover have ‹epath (stl (sdrop m steps))› using epath_sdrop ‹epath steps› by (meson epath.cases) ultimately have ‹∀k ≥ m. t ∈ set (ptms (shd (stl (sdrop k steps))))› using epath_sdrop_ptms by (metis (no_types, lifting) le_Suc_ex sdrop_add sdrop_stl subsetD) then have above: ‹∀k > m. t ∈ set (ptms (shd (sdrop k steps)))› by (metis Nat.lessE less_irrefl_nat less_trans_Suc linorder_not_less sdrop_simps(2)) let ?pre = ‹stake (n + m + 1) steps› let ?suf = ‹sdrop (n + m + 1) steps› have *: ‹¬ affects r ?f› for r unfolding affects_def by (cases r, simp_all)+ have ‹ev (holds (is_rule ?r)) ?suf› using ‹Saturated steps› Saturated_ev_rule by blast then obtain pre suf k where pre: ‹list_all (not (is_rule ?r)) pre› and suf: ‹holds (is_rule ?r) suf› and ori: ‹pre = stake k ?suf› ‹suf = sdrop k ?suf› using ev_prefix_sdrop by blast have k: ‹∃k > m. suf = sdrop k steps› using ori by (meson le_add2 less_add_one order_le_less_trans sdrop_add trans_less_add1) have ‹list_all (not (λstep. affects (snd step) ?f)) ?pre› unfolding list_all_def using * by (induct ?pre) simp_all then have ‹?f ∈ set (pseq (shd ?suf))› using ‹epath steps› epath_preserves_unaffected n epath_sdrop by (metis (no_types, lifting) list.pred_mono_strong list_all_append sdrop_add stake_add stake_sdrop) then have ‹?f ∈ set (pseq (shd suf))› using ‹epath steps› epath_preserves_unaffected n epath_sdrop * ori by (metis (no_types, lifting) list.pred_mono_strong pre stake_sdrop) moreover have ‹epath suf› using ‹epath steps› epath_sdrop ori by blast 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) moreover have ‹t ∈ set (ptms (shd suf))› using above k by (meson le_add2 less_add_one order_le_less_trans) ultimately have ‹sub 0 t p ∈ set z'› using parts_in_effect[where A=‹ptms (shd suf)›] unfolding parts_def by fastforce then show ?thesis using k pseq_in_tree_fms z'(2) by (metis Pair_inject in_mono prod.collapse pseq_def shd_sset sset_sdrop stl_sset) qed qed next fix p assume ‹Neg (Uni 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 = GammaUni show ‹∀t ∈ terms ?H. Neg (sub 0 t p) ∈ ?H› proof fix t assume t: ‹t ∈ terms ?H› show ‹Neg (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 (no_types, lifting) UN_E) then obtain m where m: ‹pt ∈ set (pseq (shd (sdrop m steps)))› using tree_fms_in_pseq by auto then show ?thesis using pt(1) set_subterms by fastforce qed then obtain m where ‹t ∈ set (subterms (pseq (shd (sdrop m steps))))› by blast then have ‹t ∈ set (ptms (shd (stl (sdrop m steps))))› using epath_stl_ptms epath_sdrop ‹epath steps› by (metis (no_types, lifting) Un_iff set_append set_remdups) moreover have ‹epath (stl (sdrop m steps))› using epath_sdrop ‹epath steps› by (meson epath.cases) ultimately have ‹∀k ≥ m. t ∈ set (ptms (shd (stl (sdrop k steps))))› using epath_sdrop_ptms by (metis (no_types, lifting) le_Suc_ex sdrop_add sdrop_stl subsetD) then have above: ‹∀k > m. t ∈ set (ptms (shd (sdrop k steps)))› by (metis Nat.lessE less_irrefl_nat less_trans_Suc linorder_not_less sdrop_simps(2)) let ?pre = ‹stake (n + m + 1) steps› let ?suf = ‹sdrop (n + m + 1) steps› have *: ‹¬ affects r ?f› for r unfolding affects_def by (cases r, simp_all)+ have ‹ev (holds (is_rule ?r)) ?suf› using ‹Saturated steps› Saturated_ev_rule by blast then obtain pre suf k where pre: ‹list_all (not (is_rule ?r)) pre› and suf: ‹holds (is_rule ?r) suf› and ori: ‹pre = stake k ?suf› ‹suf = sdrop k ?suf› using ev_prefix_sdrop by blast have k: ‹∃k > m. suf = sdrop k steps› using ori by (meson le_add2 less_add_one order_le_less_trans sdrop_add trans_less_add1) have ‹list_all (not (λstep. affects (snd step) ?f)) ?pre› unfolding list_all_def using * by (induct ?pre) simp_all then have ‹?f ∈ set (pseq (shd ?suf))› using ‹epath steps› epath_preserves_unaffected n epath_sdrop by (metis (no_types, lifting) list.pred_mono_strong list_all_append sdrop_add stake_add stake_sdrop) then have ‹?f ∈ set (pseq (shd suf))› using ‹epath steps› epath_preserves_unaffected n epath_sdrop * ori by (metis (no_types, lifting) list.pred_mono_strong pre stake_sdrop) moreover have ‹epath suf› using ‹epath steps› epath_sdrop ori by blast 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) moreover have ‹t ∈ set (ptms (shd suf))› using above k by (meson le_add2 less_add_one order_le_less_trans) ultimately have ‹Neg (sub 0 t p) ∈ set z'› using parts_in_effect[where A=‹ptms (shd suf)›] unfolding parts_def by fastforce then show ?thesis using k pseq_in_tree_fms z'(2) by (metis Pair_inject in_mono prod.collapse pseq_def shd_sset sset_sdrop stl_sset) qed qed next fix p assume ‹Uni p ∈ 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 = DeltaUni 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 obtain C where C: ‹set (ptms (shd suf)) ⊆ set C› ‹sub 0 (Fun (generateNew C) []) p ∈ set z'› using parts_in_effect[where B=B and z'=‹z'› and z=‹pseq (shd suf)› and r=‹?r› and p=‹Uni p›] unfolding parts_def by auto then have *: ‹sub 0 (Fun (generateNew C) []) p ∈ ?H› using z'(2) ori pseq_in_tree_fms by (metis (no_types, lifting) Pair_inject Un_iff in_mono prod.collapse pseq_def shd_sset sset_sdrop sset_shift stl_sset) let ?t = ‹Fun (generateNew C) []› show ‹∃t ∈ terms ?H. sub 0 t p ∈ ?H› proof (cases ‹?t ∈ set (subtermFm (sub 0 ?t p))›) case True then have ‹?t ∈ terms ?H› unfolding terms_def using * by (metis UN_I empty_iff) then show ?thesis using * by blast next case False then have ‹sub 0 t p = sub 0 ?t p› for t using sub_const_transfer by metis moreover have ‹terms ?H ≠ {}› unfolding terms_def by simp then have ‹∃t. t ∈ terms ?H› by blast ultimately show ?thesis using * by metis qed next fix p assume ‹Neg (Exi p) ∈ 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 = DeltaExi 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 obtain C where C: ‹set (ptms (shd suf)) ⊆ set C› ‹Neg (sub 0 (Fun (generateNew C) []) p) ∈ set z'› using parts_in_effect[where B=B and z'=z' and z=‹pseq (shd suf)› and r=‹?r› and p=‹Neg (Exi p)›] unfolding parts_def by auto then have *: ‹Neg (sub 0 (Fun (generateNew C) []) p) ∈ ?H› using z'(2) ori pseq_in_tree_fms by (metis (no_types, lifting) Pair_inject Un_iff in_mono prod.collapse pseq_def shd_sset sset_sdrop sset_shift stl_sset) let ?t = ‹Fun (generateNew C) []› show ‹∃t ∈ terms ?H. Neg (sub 0 t p) ∈ ?H› proof (cases ‹?t ∈ set (subtermFm (Neg (sub 0 ?t p)))›) case True then have ‹?t ∈ terms ?H› unfolding terms_def using * by (metis UN_I empty_iff) then show ?thesis using * by blast next case False then have ‹Neg (sub 0 t p) = Neg (sub 0 ?t p)› for t using sub_const_transfer by (metis subtermFm.simps(7)) moreover have ‹terms ?H ≠ {}› unfolding terms_def by simp then have ‹∃t. t ∈ terms ?H› by blast ultimately show ?thesis using * by metis qed next fix p assume ‹Neg (Neg p) ∈ 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 = NegNeg 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'› using parts_in_effect unfolding parts_def by fastforce then show ‹p ∈ ?H› using z'(2) ori pseq_in_tree_fms by (metis (no_types, lifting) Pair_inject Un_iff in_mono prod.collapse pseq_def shd_sset sset_sdrop sset_shift stl_sset) qed end