diff --git a/thys/Hybrid_Logic/Hybrid_Logic.thy b/thys/Hybrid_Logic/Hybrid_Logic.thy --- a/thys/Hybrid_Logic/Hybrid_Logic.thy +++ b/thys/Hybrid_Logic/Hybrid_Logic.thy @@ -1,5199 +1,4909 @@ theory Hybrid_Logic imports "HOL-Library.Countable" begin section \Syntax\ datatype ('a, 'b) fm = Pro 'a | Nom 'b | Neg \('a, 'b) fm\ (\\<^bold>\ _\ [40] 40) | Dis \('a, 'b) fm\ \('a, 'b) fm\ (infixr \\<^bold>\\ 30) | Dia \('a, 'b) fm\ (\\<^bold>\ _\ 10) | Sat 'b \('a, 'b) fm\ (\\<^bold>@ _ _\ 10) text \We can give other connectives as abbreviations.\ abbreviation Top (\\<^bold>\\) where \\<^bold>\ \ (undefined \<^bold>\ \<^bold>\ undefined)\ abbreviation Con (infixr \\<^bold>\\ 35) where \p \<^bold>\ q \ \<^bold>\ (\<^bold>\ p \<^bold>\ \<^bold>\ q)\ abbreviation Imp (infixr \\<^bold>\\ 25) where \p \<^bold>\ q \ \<^bold>\ (p \<^bold>\ \<^bold>\ q)\ abbreviation Box (\\<^bold>\ _\ 10) where \\<^bold>\ p \ \<^bold>\ (\<^bold>\ \<^bold>\ p)\ primrec nominals :: \('a, 'b) fm \ 'b set\ where \nominals (Pro x) = {}\ | \nominals (Nom i) = {i}\ | \nominals (\<^bold>\ p) = nominals p\ | \nominals (p \<^bold>\ q) = nominals p \ nominals q\ | \nominals (\<^bold>\ p) = nominals p\ | \nominals (\<^bold>@ i p) = {i} \ nominals p\ primrec sub :: \('b \ 'c) \ ('a, 'b) fm \ ('a, 'c) fm\ where \sub _ (Pro x) = Pro x\ | \sub f (Nom i) = Nom (f i)\ | \sub f (\<^bold>\ p) = (\<^bold>\ sub f p)\ | \sub f (p \<^bold>\ q) = (sub f p \<^bold>\ sub f q)\ | \sub f (\<^bold>\ p) = (\<^bold>\ sub f p)\ | \sub f (\<^bold>@ i p) = (\<^bold>@ (f i) (sub f p))\ lemma sub_nominals: \nominals (sub f p) = f ` nominals p\ by (induct p) auto lemma sub_id: \sub id p = p\ by (induct p) simp_all lemma sub_upd_fresh: \i \ nominals p \ sub (f(i := j)) p = sub f p\ by (induct p) auto section \Semantics\ text \ Type variable \'w\ stands for the set of worlds and \'a\ for the set of propositional symbols. The accessibility relation is given by \R\ and the valuation by \V\. The mapping from nominals to worlds is an extra argument \g\ to the semantics.\ datatype ('w, 'a) model = Model (R: \'w \ 'w set\) (V: \'w \ 'a \ bool\) primrec semantics :: \('w, 'a) model \ ('b \ 'w) \ 'w \ ('a, 'b) fm \ bool\ (\_, _, _ \ _\ [50, 50, 50] 50) where \(M, _, w \ Pro x) = V M w x\ | \(_, g, w \ Nom i) = (w = g i)\ | \(M, g, w \ \<^bold>\ p) = (\ M, g, w \ p)\ | \(M, g, w \ (p \<^bold>\ q)) = ((M, g, w \ p) \ (M, g, w \ q))\ | \(M, g, w \ \<^bold>\ p) = (\v \ R M w. M, g, v \ p)\ | \(M, g, _ \ \<^bold>@ i p) = (M, g, g i \ p)\ lemma \M, g, w \ \<^bold>\\ by simp lemma semantics_fresh: \i \ nominals p \ (M, g, w \ p) = (M, g(i := v), w \ p)\ by (induct p arbitrary: w) auto subsection \Examples\ abbreviation is_named :: \('w, 'b) model \ bool\ where \is_named M \ \w. \a. V M a = w\ abbreviation reflexive :: \('w, 'b) model \ bool\ where \reflexive M \ \w. w \ R M w\ abbreviation irreflexive :: \('w, 'b) model \ bool\ where \irreflexive M \ \w. w \ R M w\ abbreviation symmetric :: \('w, 'b) model \ bool\ where \symmetric M \ \v w. w \ R M v \ v \ R M w\ abbreviation asymmetric :: \('w, 'b) model \ bool\ where \asymmetric M \ \v w. \ (w \ R M v \ v \ R M w)\ abbreviation transitive :: \('w, 'b) model \ bool\ where \transitive M \ \v w x. w \ R M v \ x \ R M w \ x \ R M v\ abbreviation universal :: \('w, 'b) model \ bool\ where \universal M \ \v w. v \ R M w\ lemma \irreflexive M \ M, g, w \ \<^bold>@ i \<^bold>\ (\<^bold>\ Nom i)\ proof - assume \irreflexive M\ then have \g i \ R M (g i)\ by simp then have \\ M, g, g i \ \<^bold>\ Nom i\ by simp then have \M, g, g i \ \<^bold>\ (\<^bold>\ Nom i)\ by simp then show \M, g, w \ \<^bold>@ i \<^bold>\ (\<^bold>\ Nom i)\ by simp qed text \We can automatically show some characterizations of frames by pure axioms.\ lemma \irreflexive M = (\g w. M, g, w \ \<^bold>@ i \<^bold>\ (\<^bold>\ Nom i))\ by auto lemma \asymmetric M = (\g w. M, g, w \ \<^bold>@ i (\<^bold>\ \<^bold>\ (\<^bold>\ Nom i)))\ by auto lemma \universal M = (\g w. M, g, w \ \<^bold>\ Nom i)\ by auto section \Tableau\ text \ A block is defined as a list of formulas paired with an opening nominal. The opening nominal is not necessarily in the list. A branch is a list of blocks. \ type_synonym ('a, 'b) block = \('a, 'b) fm list \ 'b\ type_synonym ('a, 'b) branch = \('a, 'b) block list\ abbreviation member_list :: \'a \ 'a list \ bool\ (\_ \. _\ [51, 51] 50) where \x \. xs \ x \ set xs\ text \The predicate \on\ presents the opening nominal as appearing on the block.\ primrec on :: \('a, 'b) fm \ ('a, 'b) block \ bool\ (\_ on _\ [51, 51] 50) where \p on (ps, i) = (p \. ps \ p = Nom i)\ syntax "_Ballon" :: \pttrn \ 'a set \ bool \ bool\ (\(3\(_/on_)./ _)\ [0, 0, 10] 10) "_Bexon" :: \pttrn \ 'a set \ bool \ bool\ (\(3\(_/on_)./ _)\ [0, 0, 10] 10) translations "\p on A. P" \ "\p. p on A \ P" "\p on A. P" \ "\p. p on A \ P" abbreviation list_nominals :: \('a, 'b) fm list \ 'b set\ where \list_nominals ps \ (\p \ set ps. nominals p)\ primrec block_nominals :: \('a, 'b) block \ 'b set\ where \block_nominals (ps, i) = {i} \ list_nominals ps\ definition branch_nominals :: \('a, 'b) branch \ 'b set\ where \branch_nominals branch \ (\block \ set branch. block_nominals block)\ -abbreviation at_in :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ bool\ - (\_ at _ in _\ [51, 51, 51] 50) where - \p at a in branch \ \ps. (ps, a) \. branch \ p on (ps, a)\ +abbreviation at_in_branch :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ bool\ where + \at_in_branch p a branch \ \ps. (ps, a) \. branch \ p on (ps, a)\ + +notation at_in_branch (\_ at _ in _\ [51, 51, 51] 50) definition new :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ bool\ where \new p a branch \ \ p at a in branch\ definition witnessed :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ bool\ where \witnessed p a branch \ \i. (\<^bold>@ i p) at a in branch \ (\<^bold>\ Nom i) at a in branch\ text \ A branch has a closing tableau iff it is contained in the following inductively defined set. In that case I call the branch closeable. The first argument on the left of the turnstile, \A\, is a fixed set of nominals restricting Nom. This set rules out the copying of nominals and accessibility formulas introduced by DiaP. The second argument is "potential", used to restrict the GoTo rule. \ -inductive ST :: \'b set \ nat \ ('a, 'b) branch \ bool\ (\_, _ \ _\ [50, 50, 50] 50) +inductive STA :: \'b set \ nat \ ('a, 'b) branch \ bool\ (\_, _ \ _\ [50, 50, 50] 50) for A :: \'b set\ where Close: \p at i in branch \ (\<^bold>\ p) at i in branch \ - A, n \ branch\ + A, n \ branch\ | Neg: \(\<^bold>\ \<^bold>\ p) at a in (ps, a) # branch \ - new p a ((ps, a) # branch) \ - A, Suc n \ (p # ps, a) # branch \ - A, n \ (ps, a) # branch\ + new p a ((ps, a) # branch) \ + A, Suc n \ (p # ps, a) # branch \ + A, n \ (ps, a) # branch\ | DisP: \(p \<^bold>\ q) at a in (ps, a) # branch \ - new p a ((ps, a) # branch) \ new q a ((ps, a) # branch) \ - A, Suc n \ (p # ps, a) # branch \ A, Suc n \ (q # ps, a) # branch \ - A, n \ (ps, a) # branch\ + new p a ((ps, a) # branch) \ new q a ((ps, a) # branch) \ + A, Suc n \ (p # ps, a) # branch \ A, Suc n \ (q # ps, a) # branch \ + A, n \ (ps, a) # branch\ | DisN: \(\<^bold>\ (p \<^bold>\ q)) at a in (ps, a) # branch \ - new (\<^bold>\ p) a ((ps, a) # branch) \ new (\<^bold>\ q) a ((ps, a) # branch) \ - A, Suc n \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch \ - A, n \ (ps, a) # branch\ + new (\<^bold>\ p) a ((ps, a) # branch) \ new (\<^bold>\ q) a ((ps, a) # branch) \ + A, Suc n \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch \ + A, n \ (ps, a) # branch\ | DiaP: \(\<^bold>\ p) at a in (ps, a) # branch \ - i \ A \ branch_nominals ((ps, a) # branch) \ - \a. p = Nom a \ \ witnessed p a ((ps, a) # branch) \ - A, Suc n \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch \ - A, n \ (ps, a) # branch\ + i \ A \ branch_nominals ((ps, a) # branch) \ + \a. p = Nom a \ \ witnessed p a ((ps, a) # branch) \ + A, Suc n \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch \ + A, n \ (ps, a) # branch\ | DiaN: \(\<^bold>\ (\<^bold>\ p)) at a in (ps, a) # branch \ - (\<^bold>\ Nom i) at a in (ps, a) # branch \ - new (\<^bold>\ (\<^bold>@ i p)) a ((ps, a) # branch) \ - A, Suc n \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch \ - A, n \ (ps, a) # branch\ + (\<^bold>\ Nom i) at a in (ps, a) # branch \ + new (\<^bold>\ (\<^bold>@ i p)) a ((ps, a) # branch) \ + A, Suc n \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch \ + A, n \ (ps, a) # branch\ | SatP: \(\<^bold>@ a p) at b in (ps, a) # branch \ - new p a ((ps, a) # branch) \ - A, Suc n \ (p # ps, a) # branch \ - A, n \ (ps, a) # branch\ + new p a ((ps, a) # branch) \ + A, Suc n \ (p # ps, a) # branch \ + A, n \ (ps, a) # branch\ | SatN: \(\<^bold>\ (\<^bold>@ a p)) at b in (ps, a) # branch \ - new (\<^bold>\ p) a ((ps, a) # branch) \ - A, Suc n \ ((\<^bold>\ p) # ps, a) # branch \ - A, n \ (ps, a) # branch\ + new (\<^bold>\ p) a ((ps, a) # branch) \ + A, Suc n \ ((\<^bold>\ p) # ps, a) # branch \ + A, n \ (ps, a) # branch\ | GoTo: \i \ branch_nominals branch \ - A, n \ ([], i) # branch \ - A, Suc n \ branch\ + A, n \ ([], i) # branch \ + A, Suc n \ branch\ | Nom: \p at b in (ps, a) # branch \ Nom a at b in (ps, a) # branch \ - \i. p = Nom i \ p = (\<^bold>\ Nom i) \ i \ A \ - new p a ((ps, a) # branch) \ - A, Suc n \ (p # ps, a) # branch \ - A, n \ (ps, a) # branch\ - -abbreviation ST_ex_potential :: \'b set \ ('a, 'b) branch \ bool\ (\_ \ _\ [50, 50] 50) where + \i. p = Nom i \ p = (\<^bold>\ Nom i) \ i \ A \ + new p a ((ps, a) # branch) \ + A, Suc n \ (p # ps, a) # branch \ + A, n \ (ps, a) # branch\ + +abbreviation STA_ex_potential :: \'b set \ ('a, 'b) branch \ bool\ (\_ \ _\ [50, 50] 50) where \A \ branch \ \n. A, n \ branch\ -lemma ST_Suc: \A, n \ branch \ A, Suc n \ branch\ - by (induct n branch rule: ST.induct) (simp_all add: ST.intros) +lemma STA_Suc: \A, n \ branch \ A, Suc n \ branch\ + by (induct n branch rule: STA.induct) (simp_all add: STA.intros) text \A verified derivation in the calculus.\ lemma fixes i defines \p \ \<^bold>\ (\<^bold>@ i (Nom i))\ shows \A, Suc n \ [([p], a)]\ proof - have \i \ branch_nominals [([p], a)]\ unfolding p_def branch_nominals_def by simp then have ?thesis if \A, n \ [([], i), ([p], a)]\ using that GoTo by fast moreover have \new (\<^bold>\ Nom i) i [([], i), ([p], a)]\ unfolding p_def new_def by auto moreover have \(\<^bold>\ (\<^bold>@ i (Nom i))) at a in [([], i), ([p], a)]\ unfolding p_def by fastforce ultimately have ?thesis if \A, Suc n \ [([\<^bold>\ Nom i], i), ([p], a)]\ using that SatN by fast then show ?thesis by (meson Close list.set_intros(1) on.simps) qed section \Soundness\ text \ An \i\-block is satisfied by a model \M\ and assignment \g\ if all formulas on the block are true under \M\ at the world \g i\ A branch is satisfied by a model and assignment if all blocks on it are. \ primrec block_sat :: \('w, 'a) model \ ('b \ 'w) \ ('a, 'b) block \ bool\ (\_, _ \\<^sub>B _\ [50, 50] 50) where \(M, g \\<^sub>B (ps, i)) = (\p on (ps, i). M, g, g i \ p)\ abbreviation branch_sat :: \('w, 'a) model \ ('b \ 'w) \ ('a, 'b) branch \ bool\ (\_, _ \\<^sub>\ _\ [50, 50] 50) where \M, g \\<^sub>\ branch \ \(ps, i) \ set branch. M, g \\<^sub>B (ps, i)\ lemma block_nominals: \p on block \ i \ nominals p \ i \ block_nominals block\ by (induct block) auto lemma block_sat_fresh: assumes \M, g \\<^sub>B block\ \i \ block_nominals block\ shows \M, g(i := v) \\<^sub>B block\ using assms proof (induct block) case (Pair ps a) then have \\p on (ps, a). i \ nominals p\ using block_nominals by fast moreover have \i \ a\ using calculation by simp ultimately have \\p on (ps, a). M, g(i := v), (g(i := v)) a \ p\ using Pair semantics_fresh by fastforce then show ?case by (meson block_sat.simps) qed lemma branch_sat_fresh: assumes \M, g \\<^sub>\ branch\ \i \ branch_nominals branch\ shows \M, g(i := v) \\<^sub>\ branch\ using assms using block_sat_fresh unfolding branch_nominals_def by fast text \If a branch has a derivation then it cannot be satisfied.\ lemma soundness': \A, n \ branch \ M, g \\<^sub>\ branch \ False\ -proof (induct n branch arbitrary: g rule: ST.induct) +proof (induct n branch arbitrary: g rule: STA.induct) case (Close p i branch) then have \M, g, g i \ p\ \M, g, g i \ \<^bold>\ p\ by fastforce+ then show ?case by simp next case (Neg p a ps branch) have \M, g, g a \ p\ using Neg(1, 5) by fastforce then have \M, g \\<^sub>\ (p # ps, a) # branch\ using Neg(5) by simp then show ?case using Neg(4) by blast next case (DisP p q a ps branch) consider \M, g, g a \ p\ | \M, g, g a \ q\ using DisP(1, 8) by fastforce then consider \M, g \\<^sub>\ (p # ps, a) # branch\ | \M, g \\<^sub>\ (q # ps, a) # branch\ using DisP(8) by auto then show ?case using DisP(5, 7) by metis next case (DisN p q a ps branch) have \M, g, g a \ \<^bold>\ p\ \M, g, g a \ \<^bold>\ q\ using DisN(1, 5) by fastforce+ then have \M, g \\<^sub>\ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch\ using DisN(5) by simp then show ?case using DisN(4) by blast next case (DiaP p a ps branch i) then have *: \M, g \\<^sub>B (ps, a)\ by simp have \i \ nominals p\ using DiaP(1-2) unfolding branch_nominals_def by fastforce have \M, g, g a \ \<^bold>\ p\ using DiaP(1, 7) by fastforce then obtain v where \v \ R M (g a)\ \M, g, v \ p\ by auto then have \M, g(i := v), v \ p\ using \i \ nominals p\ semantics_fresh by metis then have \M, g(i := v), g a \ \<^bold>@ i p\ by simp moreover have \M, g(i := v), g a \ \<^bold>\ Nom i\ using \v \ R M (g a)\ by simp moreover have \M, g(i := v) \\<^sub>\ (ps, a) # branch\ using DiaP(2, 7) branch_sat_fresh by fast moreover have \i \ block_nominals (ps, a)\ using DiaP(2) unfolding branch_nominals_def by simp then have \\p on (ps, a). M, g(i := v), g a \ p\ using * semantics_fresh by fastforce ultimately have \M, g(i := v) \\<^sub>\ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch\ by auto then show ?case using DiaP by blast next case (DiaN p a ps branch i) have \M, g, g a \ \<^bold>\ (\<^bold>\ p)\ \M, g, g a \ \<^bold>\ Nom i\ using DiaN(1-2, 6) by fastforce+ then have \M, g, g a \ \<^bold>\ (\<^bold>@ i p)\ by simp then have \M, g \\<^sub>\ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch\ using DiaN(6) by simp then show ?thesis using DiaN(5) by blast next case (SatP a p b ps branch) have \M, g, g a \ p\ using SatP(1, 5) by fastforce then have \M, g \\<^sub>\ (p # ps, a) # branch\ using SatP(5) by simp then show ?case using SatP(4) by blast next case (SatN a p b ps branch) have \M, g, g a \ \<^bold>\ p\ using SatN(1, 5) by fastforce then have \M, g \\<^sub>\ ((\<^bold>\ p) # ps, a) # branch\ using SatN(5) by simp then show ?case using SatN(4) by blast next case (GoTo i branch) then show ?case by auto next case (Nom p b ps a branch) have \M, g, g b \ p\ \M, g, g b \ Nom a\ using Nom(1-2, 7) by fastforce+ moreover have \M, g \\<^sub>B (ps, a)\ using Nom(7) by simp ultimately have \M, g \\<^sub>B (p # ps, a)\ by simp then have \M, g \\<^sub>\ (p # ps, a) # branch\ using Nom(7) by simp then show ?case using Nom(6) by blast qed lemma block_sat: \\p on block. M, g, w \ p \ M, g \\<^sub>B block\ by (induct block) auto lemma branch_sat: assumes \\(ps, i) \ set branch. \p on (ps, i). M, g, w \ p\ shows \M, g \\<^sub>\ branch\ using assms block_sat by fast lemma soundness: assumes \A, n \ branch\ shows \\block \ set branch. \p on block. \ M, g, w \ p\ using assms soundness' branch_sat by fast corollary \\ A, n \ []\ using soundness by fastforce theorem soundness_fresh: assumes \A, n \ [([\<^bold>\ p], i)]\ \i \ nominals p\ shows \M, g, w \ p\ proof - from assms(1) have \M, g, g i \ p\ for g using soundness by fastforce then have \M, g(i := w), (g(i := w)) i \ p\ by blast then have \M, g(i := w), w \ p\ by simp then have \M, g(i := g i), w \ p\ using assms(2) semantics_fresh by metis then show ?thesis by simp qed section \No Detours\ text \ We only need to spend initial potential when we apply GoTo twice in a row. Otherwise another rule will have been applied in-between that justifies the GoTo. Therefore, by filtering out detours we can close any closeable branch starting from a single unit of potential. \ primrec nonempty :: \('a, 'b) block \ bool\ where \nonempty (ps, i) = (ps \ [])\ lemma nonempty_Suc: assumes \A, n \ (ps, a) # filter nonempty left @ right\ \q at a in (ps, a) # filter nonempty left @ right\ \q \ Nom a\ shows \A, Suc n \ filter nonempty ((ps, a) # left) @ right\ proof (cases ps) case Nil then have \a \ branch_nominals (filter nonempty left @ right)\ unfolding branch_nominals_def using assms(2-3) by fastforce then show ?thesis using assms(1) Nil GoTo by auto next case Cons then show ?thesis - using assms(1) ST_Suc by auto + using assms(1) STA_Suc by auto qed -lemma ST_nonempty: +lemma STA_nonempty: \A, n \ left @ right \ A, Suc m \ filter nonempty left @ right\ -proof (induct n \left @ right\ arbitrary: left right rule: ST.induct) +proof (induct n \left @ right\ arbitrary: left right rule: STA.induct) case (Close p i n) have \(\<^bold>\ p) at i in filter nonempty left @ right\ using Close(2) by fastforce moreover from this have \p at i in filter nonempty left @ right\ using Close(1) by fastforce ultimately show ?case - using ST.Close by fast + using STA.Close by fast next case (Neg p a ps branch n) then show ?case proof (cases left) case Nil then have \A, Suc m \ (p # ps, a) # branch\ using Neg(4) by fastforce then have \A, m \ (ps, a) # branch\ - using Neg(1-2) ST.Neg by fast + using Neg(1-2) STA.Neg by fast then show ?thesis - using Nil Neg(5) ST_Suc by auto + using Nil Neg(5) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ (p # ps, a) # filter nonempty left' @ right\ using Neg(4)[where left=\_ # left'\] Neg(5) by fastforce moreover have *: \(\<^bold>\ \<^bold>\ p) at a in (ps, a) # filter nonempty left' @ right\ using Cons Neg(1, 5) by fastforce moreover have \new p a ((ps, a) # filter nonempty left' @ right)\ using Cons Neg(2, 5) unfolding new_def by auto ultimately have \A, m \ (ps, a) # filter nonempty left' @ right\ - using ST.Neg by fast + using STA.Neg by fast then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ using * nonempty_Suc by fast then show ?thesis using Cons Neg(5) by auto qed next case (DisP p q a ps branch n) then show ?case proof (cases left) case Nil then have \A, Suc m \ (p # ps, a) # branch\ \A, Suc m \ (q # ps, a) # branch\ using DisP(5, 7) by fastforce+ then have \A, m \ (ps, a) # branch\ - using DisP(1-3) ST.DisP by fast + using DisP(1-3) STA.DisP by fast then show ?thesis - using Nil DisP(8) ST_Suc by auto + using Nil DisP(8) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ (p # ps, a) # filter nonempty left' @ right\ \A, Suc m \ (q # ps, a) # filter nonempty left' @ right\ using DisP(5, 7)[where left=\_ # left'\] DisP(8) by fastforce+ moreover have *: \(p \<^bold>\ q) at a in (ps, a) # filter nonempty left' @ right\ using Cons DisP(1, 8) by fastforce moreover have \new p a ((ps, a) # filter nonempty left' @ right)\ \new q a ((ps, a) # filter nonempty left' @ right)\ using Cons DisP(2-3, 8) unfolding new_def by auto ultimately have \A, m \ (ps, a) # filter nonempty left' @ right\ - using ST.DisP by fast + using STA.DisP by fast then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ using * nonempty_Suc by fast then show ?thesis using Cons DisP(8) by auto qed next case (DisN p q a ps branch n) then show ?case proof (cases left) case Nil then have \A, Suc m \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch\ using DisN(4) by fastforce then have \A, m \ (ps, a) # branch\ - using DisN(1-2) ST.DisN by fast + using DisN(1-2) STA.DisN by fast then show ?thesis - using Nil DisN(5) ST_Suc by auto + using Nil DisN(5) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # filter nonempty left' @ right\ using DisN(4)[where left=\_ # left'\] DisN(5) by fastforce moreover have *: \(\<^bold>\ (p \<^bold>\ q)) at a in (ps, a) # filter nonempty left' @ right\ using Cons DisN(1, 5) by fastforce moreover consider \new (\<^bold>\ p) a ((ps, a) # filter nonempty left' @ right)\ | \new (\<^bold>\ q) a ((ps, a) # filter nonempty left' @ right)\ using Cons DisN(2, 5) unfolding new_def by auto ultimately have \A, m \ (ps, a) # filter nonempty left' @ right\ - using ST.DisN by metis + using STA.DisN by metis then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ using * nonempty_Suc by fast then show ?thesis using Cons DisN(5) by auto qed next case (DiaP p a ps branch i n) then show ?case proof (cases left) case Nil then have \A, Suc m \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch\ using DiaP(6) by fastforce then have \A, m \ (ps, a) # branch\ - using DiaP(1-4) ST.DiaP by fast + using DiaP(1-4) STA.DiaP by fast then show ?thesis - using Nil DiaP(7) ST_Suc by auto + using Nil DiaP(7) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # filter nonempty left' @ right\ using DiaP(6)[where left=\_ # left'\] DiaP(7) by fastforce moreover have *: \(\<^bold>\ p) at a in (ps, a) # filter nonempty left' @ right\ using Cons DiaP(1, 7) by fastforce moreover have \i \ A \ branch_nominals ((ps, a) # filter nonempty left' @ right)\ using Cons DiaP(2, 7) unfolding branch_nominals_def by auto moreover have \\ witnessed p a ((ps, a) # filter nonempty left' @ right)\ using Cons DiaP(4, 7) unfolding witnessed_def by auto ultimately have \A, m \ (ps, a) # filter nonempty left' @ right\ - using DiaP(3) ST.DiaP by fast + using DiaP(3) STA.DiaP by fast then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ using * nonempty_Suc by fast then show ?thesis using Cons DiaP(7) by auto qed next case (DiaN p a ps branch i n) then show ?case proof (cases left) case Nil then have \A, Suc m \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch\ using DiaN(5) by fastforce then have \A, m \ (ps, a) # branch\ - using DiaN(1-3) ST.DiaN by fast + using DiaN(1-3) STA.DiaN by fast then show ?thesis - using Nil DiaN(6) ST_Suc by auto + using Nil DiaN(6) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # filter nonempty left' @ right\ using DiaN(5)[where left=\_ # left'\] DiaN(6) by fastforce moreover have *: \(\<^bold>\ (\<^bold>\ p)) at a in (ps, a) # filter nonempty left' @ right\ using Cons DiaN(1, 6) by fastforce moreover have *: \(\<^bold>\ Nom i) at a in (ps, a) # filter nonempty left' @ right\ using Cons DiaN(2, 6) by fastforce moreover have \new (\<^bold>\ (\<^bold>@ i p)) a ((ps, a) # filter nonempty left' @ right)\ using Cons DiaN(3, 6) unfolding new_def by auto ultimately have \A, m \ (ps, a) # filter nonempty left' @ right\ - using ST.DiaN by fast + using STA.DiaN by fast then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ using * nonempty_Suc by fast then show ?thesis using Cons DiaN(6) by auto qed next case (SatP a p b ps branch n) then show ?case proof (cases left) case Nil then have \A, Suc m \ (p # ps, a) # branch\ using SatP(4) by fastforce then have \A, m \ (ps, a) # branch\ - using SatP(1-2) ST.SatP by fast + using SatP(1-2) STA.SatP by fast then show ?thesis - using Nil SatP(5) ST_Suc by auto + using Nil SatP(5) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ (p # ps, a) # filter nonempty left' @ right\ using SatP(4)[where left=\_ # left'\] SatP(5) by fastforce moreover have \(\<^bold>@ a p) at b in (ps, a) # filter nonempty left' @ right\ using Cons SatP(1, 5) by fastforce moreover have \new p a ((ps, a) # filter nonempty left' @ right)\ using Cons SatP(2, 5) unfolding new_def by auto ultimately have *: \A, m \ (ps, a) # filter nonempty left' @ right\ - using ST.SatP by fast + using STA.SatP by fast then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ proof (cases ps) case Nil then have \a \ branch_nominals (filter nonempty left' @ right)\ unfolding branch_nominals_def using SatP(1, 5) Cons by fastforce then show ?thesis using * Nil GoTo by fastforce next case Cons then show ?thesis - using * ST_Suc by auto + using * STA_Suc by auto qed then show ?thesis using Cons SatP(5) by auto qed next case (SatN a p b ps branch n) then show ?case proof (cases left) case Nil then have \A, Suc m \ ((\<^bold>\ p) # ps, a) # branch\ using SatN(4) by fastforce then have \A, m \ (ps, a) # branch\ - using SatN(1-2) ST.SatN by fast + using SatN(1-2) STA.SatN by fast then show ?thesis - using Nil SatN(5) ST_Suc by auto + using Nil SatN(5) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ ((\<^bold>\ p) # ps, a) # filter nonempty left' @ right\ using SatN(4)[where left=\_ # left'\] SatN(5) by fastforce moreover have \(\<^bold>\ (\<^bold>@ a p)) at b in (ps, a) # filter nonempty left' @ right\ using Cons SatN(1, 5) by fastforce moreover have \new (\<^bold>\ p) a ((ps, a) # filter nonempty left' @ right)\ using Cons SatN(2, 5) unfolding new_def by auto ultimately have *: \A, m \ (ps, a) # filter nonempty left' @ right\ - using ST.SatN by fast + using STA.SatN by fast then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ proof (cases ps) case Nil then have \a \ branch_nominals (filter nonempty left' @ right)\ unfolding branch_nominals_def using SatN(1, 5) Cons by fastforce then show ?thesis using * Nil GoTo by fastforce next case Cons then show ?thesis - using * ST_Suc by auto + using * STA_Suc by auto qed then show ?thesis using Cons SatN(5) by auto qed next case (GoTo i n) show ?case using GoTo(3)[where left=\([], i) # left\] by simp next case (Nom p b ps a branch n) then show ?case proof (cases left) case Nil then have \A, Suc m \ (p # ps, a) # branch\ using Nom(6) by fastforce then have \A, m \ (ps, a) # branch\ - using Nom(1-4) ST.Nom by metis + using Nom(1-4) STA.Nom by metis then show ?thesis - using Nil Nom(7) ST_Suc by auto + using Nil Nom(7) STA_Suc by auto next case (Cons _ left') then have \A, Suc m \ (p # ps, a) # filter nonempty left' @ right\ using Nom(6)[where left=\_ # left'\] Nom(7) by fastforce moreover have \p at b in (ps, a) # filter nonempty left' @ right\ and a: \Nom a at b in (ps, a) # filter nonempty left' @ right\ using Cons Nom(1-2, 7) by simp_all (metis empty_iff empty_set)+ moreover have \new p a ((ps, a) # filter nonempty left' @ right)\ using Cons Nom(4, 7) unfolding new_def by auto ultimately have *: \A, m \ (ps, a) # filter nonempty left' @ right\ - using Nom(3) ST.Nom by metis + using Nom(3) STA.Nom by metis then have \A, Suc m \ filter nonempty ((ps, a) # left') @ right\ proof (cases ps) case Nil moreover have \a \ b\ using Nom(1, 4) unfolding new_def by blast ultimately have \a \ branch_nominals (filter nonempty left' @ right)\ using a unfolding branch_nominals_def by fastforce then show ?thesis using * Nil GoTo by auto next case Cons then show ?thesis - using * ST_Suc by auto + using * STA_Suc by auto qed then show ?thesis using Cons Nom(7) by auto qed qed -theorem ST_potential: \A, n \ branch \ A, Suc m \ branch\ - using ST_nonempty[where left=\[]\] by auto - -corollary ST_one: \A, n \ branch \ A, 1 \ branch\ - using ST_potential by auto +theorem STA_potential: \A, n \ branch \ A, Suc m \ branch\ + using STA_nonempty[where left=\[]\] by auto + +corollary STA_one: \A, n \ branch \ A, 1 \ branch\ + using STA_potential by auto subsection \Free GoTo\ text \The above result allows us to prove a version of GoTo that works "for free."\ lemma GoTo': assumes \A, Suc n \ ([], i) # branch\ \i \ branch_nominals branch\ shows \A, Suc n \ branch\ - using assms GoTo ST_potential by fast + using assms GoTo STA_potential by fast section \Indexed Mapping\ text \This section contains some machinery for showing admissible rules.\ subsection \Indexing\ text \ We use pairs of natural numbers to index into the branch. The first component specifies the block and the second specifies the formula on that block. We index from the back to ensure that indices are stable under the addition of new formulas and blocks. \ primrec rev_nth :: \'a list \ nat \ 'a option\ (infixl \!.\ 100) where \[] !. v = None\ | \(x # xs) !. v = (if length xs = v then Some x else xs !. v)\ lemma rev_nth_last: \xs !. 0 = Some x \ last xs = x\ by (induct xs) auto lemma rev_nth_zero: \(xs @ [x]) !. 0 = Some x\ by (induct xs) auto lemma rev_nth_snoc: \(xs @ [x]) !. Suc v = Some y \ xs !. v = Some y\ by (induct xs) auto lemma rev_nth_Suc: \(xs @ [x]) !. Suc v = xs !. v\ by (induct xs) auto lemma rev_nth_bounded: \v < length xs \ \x. xs !. v = Some x\ by (induct xs) simp_all lemma rev_nth_Cons: \xs !. v = Some y \ (x # xs) !. v = Some y\ proof (induct xs arbitrary: v rule: rev_induct) case (snoc a xs) then show ?case proof (induct v) case (Suc v) then have \xs !. v = Some y\ using rev_nth_snoc by fast then have \(x # xs) !. v = Some y\ using Suc(2) by blast then show ?case using Suc(3) by auto qed simp qed simp lemma rev_nth_append: \xs !. v = Some y \ (ys @ xs) !. v = Some y\ using rev_nth_Cons[where xs=\_ @ xs\] by (induct ys) simp_all lemma rev_nth_mem: \block \. branch \ (\v. branch !. v = Some block)\ proof assume \block \. branch\ then show \\v. branch !. v = Some block\ proof (induct branch) case (Cons block' branch) then show ?case proof (cases \block = block'\) case False then have \\v. branch !. v = Some block\ using Cons by simp then show ?thesis using rev_nth_Cons by fast qed auto qed simp next assume \\v. branch !. v = Some block\ then show \block \. branch\ proof (induct branch) case (Cons block' branch) then show ?case by simp (metis option.sel) qed simp qed lemma rev_nth_on: \p on (ps, i) \ (\v. ps !. v = Some p) \ p = Nom i\ by (simp add: rev_nth_mem) lemma rev_nth_Some: \xs !. v = Some y \ v < length xs\ proof (induct xs arbitrary: v rule: rev_induct) case (snoc x xs) then show ?case by (induct v) (simp_all, metis rev_nth_snoc) qed simp lemma index_Cons: assumes \((ps, a) # branch) !. v = Some (qs, b)\ \qs !. v' = Some q\ shows \\qs'. ((p # ps, a) # branch) !. v = Some (qs', b) \ qs' !. v' = Some q\ proof - have \((p # ps, a) # branch) !. v = Some (qs, b) \ ((p # ps, a) # branch) !. v = Some (p # qs, b)\ using assms(1) by auto moreover have \qs !. v' = Some q\ \(p # qs) !. v' = Some q\ using assms(2) rev_nth_Cons by fast+ ultimately show ?thesis by fastforce qed subsection \Mapping\ primrec mapi :: \(nat \ 'a \ 'b) \ 'a list \ 'b list\ where \mapi f [] = []\ | \mapi f (x # xs) = f (length xs) x # mapi f xs\ primrec mapi_block :: \(nat \ ('a, 'b) fm \ ('a, 'b) fm) \ (('a, 'b) block \ ('a, 'b) block)\ where \mapi_block f (ps, i) = (mapi f ps, i)\ definition mapi_branch :: \(nat \ nat \ ('a, 'b) fm \ ('a, 'b) fm) \ (('a, 'b) branch \ ('a, 'b) branch)\ where \mapi_branch f branch \ mapi (\v. mapi_block (f v)) branch\ abbreviation mapper :: \(('a, 'b) fm \ ('a, 'b) fm) \ (nat \ nat) set \ nat \ nat \ ('a, 'b) fm \ ('a, 'b) fm\ where \mapper f xs v v' p \ (if (v, v') \ xs then f p else p)\ lemma mapi_block_add_oob: assumes \length ps \ v'\ shows \mapi_block (mapper f ({(v, v')} \ xs) v) (ps, i) = mapi_block (mapper f xs v) (ps, i)\ using assms by (induct ps) simp_all lemma mapi_branch_add_oob: assumes \length branch \ v\ shows \mapi_branch (mapper f ({(v, v')} \ xs)) branch = mapi_branch (mapper f xs) branch\ unfolding mapi_branch_def using assms by (induct branch) simp_all lemma mapi_branch_head_add_oob: \mapi_branch (mapper f ({(length branch, length ps)} \ xs)) ((ps, a) # branch) = mapi_branch (mapper f xs) ((ps, a) # branch)\ using mapi_branch_add_oob[where branch=branch] unfolding mapi_branch_def using mapi_block_add_oob[where ps=ps] by simp lemma mapi_branch_mem: assumes \(ps, i) \. branch\ shows \\v. (mapi (f v) ps, i) \. mapi_branch f branch\ unfolding mapi_branch_def using assms by (induct branch) auto lemma rev_nth_mapi_branch: assumes \branch !. v = Some (ps, a)\ shows \(mapi (f v) ps, a) \. mapi_branch f branch\ unfolding mapi_branch_def using assms by (induct branch) (simp_all, metis mapi_block.simps option.inject) lemma rev_nth_mapi_block: assumes \ps !. v' = Some p\ shows \f v' p on (mapi f ps, a)\ using assms by (induct ps) (simp_all, metis option.sel) lemma mapi_append: \mapi f (xs @ ys) = mapi (\v. f (v + length ys)) xs @ mapi f ys\ by (induct xs) simp_all lemma mapi_block_id: \mapi_block (mapper f {} v) (ps, i) = (ps, i)\ by (induct ps) auto lemma mapi_branch_id: \mapi_branch (mapper f {}) branch = branch\ unfolding mapi_branch_def using mapi_block_id by (induct branch) auto lemma length_mapi: \length (mapi f xs) = length xs\ by (induct xs) auto lemma mapi_rev_nth: assumes \xs !. v = Some x\ shows \mapi f xs !. v = Some (f v x)\ using assms proof (induct xs arbitrary: v) case (Cons y xs) have *: \mapi f (y # xs) = f (length xs) y # mapi f xs\ by simp show ?case proof (cases \v = length xs\) case True then have \mapi f (y # xs) !. v = Some (f (length xs) y)\ using length_mapi * by (metis rev_nth.simps(2)) then show ?thesis using Cons.prems True by auto next case False then show ?thesis using * Cons length_mapi by (metis rev_nth.simps(2)) qed qed simp section \Duplicate Formulas\ subsection \Removable indices\ abbreviation \proj \ Equiv_Relations.proj\ definition all_is :: \('a, 'b) fm \ ('a, 'b) fm list \ nat set \ bool\ where \all_is p ps xs \ \v \ xs. ps !. v = Some p\ definition is_at :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ nat \ nat \ bool\ where \is_at p i branch v v' \ \ps. branch !. v = Some (ps, i) \ ps !. v' = Some p\ text \This definition is slightly complicated by the inability to index the opening nominal.\ definition is_elsewhere :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ (nat \ nat) set \ bool\ where \is_elsewhere p i branch xs \ \w w' ps. (w, w') \ xs \ branch !. w = Some (ps, i) \ (p = Nom i \ ps !. w' = Some p)\ definition Dup :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ (nat \ nat) set \ bool\ where \Dup p i branch xs \ \(v, v') \ xs. is_at p i branch v v' \ is_elsewhere p i branch xs\ lemma Dup_all_is: assumes \Dup p i branch xs\ \branch !. v = Some (ps, a)\ shows \all_is p ps (proj xs v)\ using assms unfolding Dup_def is_at_def all_is_def proj_def by auto lemma Dup_branch: \Dup p i branch xs \ Dup p i (extra @ branch) xs\ unfolding Dup_def is_at_def is_elsewhere_def using rev_nth_append by fast lemma Dup_block: assumes \Dup p i ((ps, a) # branch) xs\ shows \Dup p i ((ps' @ ps, a) # branch) xs\ unfolding Dup_def proof safe fix v v' assume \(v, v') \ xs\ then show \is_at p i ((ps' @ ps, a) # branch) v v'\ using assms rev_nth_append unfolding Dup_def is_at_def by fastforce next fix v v' assume \(v, v') \ xs\ then obtain w w' qs where \(w, w') \ xs\ \((ps, a) # branch) !. w = Some (qs, i)\ \p = Nom i \ qs !. w' = Some p\ using assms unfolding Dup_def is_elsewhere_def by blast then have \\qs. ((ps' @ ps, a) # branch) !. w = Some (qs, i) \ (p = Nom i \ qs !. w' = Some p)\ using rev_nth_append by fastforce then show \is_elsewhere p i ((ps' @ ps, a) # branch) xs\ unfolding is_elsewhere_def using \(w, w') \ xs\ by blast qed definition only_touches :: \'b \ ('a, 'b) branch \ (nat \ nat) set \ bool\ where \only_touches i branch xs \ \(v, v') \ xs. \ps a. branch !. v = Some (ps, a) \ i = a\ lemma Dup_touches: \Dup p i branch xs \ only_touches i branch xs\ unfolding Dup_def is_at_def only_touches_def by auto lemma only_touches_opening: assumes \only_touches i branch xs\ \(v, v') \ xs\ \branch !. v = Some (ps, a)\ shows \i = a\ using assms unfolding only_touches_def is_at_def by auto lemma Dup_head: \Dup p i ((ps, a) # branch) xs \ Dup p i ((q # ps, a) # branch) xs\ using Dup_block[where ps'=\[_]\] by simp lemma Dup_head_oob': assumes \Dup p i ((ps, a) # branch) xs\ shows \(length branch, k + length ps) \ xs\ using assms rev_nth_Some unfolding Dup_def is_at_def by fastforce lemma Dup_head_oob: assumes \Dup p i ((ps, a) # branch) xs\ shows \(length branch, length ps) \ xs\ using assms Dup_head_oob'[where k=0] by fastforce subsection \Omitting formulas\ primrec omit :: \nat set \ ('a, 'b) fm list \ ('a, 'b) fm list\ where \omit xs [] = []\ | \omit xs (p # ps) = (if length ps \ xs then omit xs ps else p # omit xs ps)\ primrec omit_block :: \nat set \ ('a, 'b) block \ ('a, 'b) block\ where \omit_block xs (ps, a) = (omit xs ps, a)\ definition omit_branch :: \(nat \ nat) set \ ('a, 'b) branch \ ('a, 'b) branch\ where \omit_branch xs branch \ mapi (\v. omit_block (proj xs v)) branch\ lemma omit_mem: \ps !. v = Some p \ v \ xs \ p \. omit xs ps\ proof (induct ps) case (Cons q ps) then show ?case by (cases \v = length ps\) simp_all qed simp lemma omit_id: \omit {} ps = ps\ by (induct ps) auto lemma omit_block_id: \omit_block {} block = block\ using omit_id by (cases block) simp lemma omit_branch_id: \omit_branch {} branch = branch\ unfolding omit_branch_def proj_def using omit_block_id by (induct branch) fastforce+ lemma omit_branch_mem_diff_opening: assumes \only_touches i branch xs\ \(ps, a) \. branch\ \i \ a\ shows \(ps, a) \. omit_branch xs branch\ proof - obtain v where v: \branch !. v = Some (ps, a)\ using assms(2) rev_nth_mem by fast then have \omit_branch xs branch !. v = Some (omit (proj xs v) ps, a)\ unfolding omit_branch_def by (simp add: mapi_rev_nth) then have *: \(omit (proj xs v) ps, a) \. omit_branch xs branch\ using rev_nth_mem by fast moreover have \proj xs v = {}\ unfolding proj_def using assms(1, 3) v only_touches_opening by fast then have \omit (proj xs v) ps = ps\ using omit_id by auto ultimately show ?thesis by simp qed lemma Dup_omit_branch_mem_same_opening: assumes \Dup p i branch xs\ \p at i in branch\ shows \p at i in omit_branch xs branch\ proof - obtain ps where ps: \(ps, i) \. branch\ \p on (ps, i)\ using assms(2) by blast then obtain v where v: \branch !. v = Some (ps, i)\ using rev_nth_mem by fast then have \omit_branch xs branch !. v = Some (omit (proj xs v) ps, i)\ unfolding omit_branch_def by (simp add: mapi_rev_nth) then have *: \(omit (proj xs v) ps, i) \. omit_branch xs branch\ using rev_nth_mem by fast consider v' where \ps !. v' = Some p\ \(v, v') \ xs\ | v' where \ps !. v' = Some p\ \(v, v') \ xs\ | \p = Nom i\ using ps v rev_nth_mem by fastforce then show ?thesis proof cases case (1 v') then obtain qs w w' where qs: \(w, w') \ xs\ \branch !. w = Some (qs, i)\ \p = Nom i \ qs !. w' = Some p\ using assms(1) unfolding Dup_def is_elsewhere_def by blast then have \omit_branch xs branch !. w = Some (omit (proj xs w) qs, i)\ unfolding omit_branch_def by (simp add: mapi_rev_nth) then have \(omit (proj xs w) qs, i) \. omit_branch xs branch\ using rev_nth_mem by fast moreover have \p on (omit (proj xs w) qs, i)\ unfolding proj_def using qs(1, 3) omit_mem by fastforce ultimately show ?thesis by blast next case (2 v') then show ?thesis using * omit_mem unfolding proj_def by (metis Image_singleton_iff on.simps) next case 3 then show ?thesis using * by auto qed qed lemma omit_del: assumes \p \. ps\ \p \ set (omit xs ps)\ shows \\v. ps !. v = Some p \ v \ xs\ using assms omit_mem rev_nth_mem by metis lemma omit_all_is: assumes \all_is p ps xs\ \q \. ps\ \q \ set (omit xs ps)\ shows \q = p\ using assms omit_del unfolding all_is_def by fastforce definition all_is_branch :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ (nat \ nat) set \ bool\ where \all_is_branch p i branch xs \ \(v, v') \ xs. v < length branch \ is_at p i branch v v'\ lemma all_is_branch: \all_is_branch p i branch xs \ branch !. v = Some (ps, a) \ all_is p ps (proj xs v)\ unfolding all_is_branch_def is_at_def all_is_def proj_def using rev_nth_Some by fastforce lemma Dup_all_is_branch: \Dup p i branch xs \ all_is_branch p i branch xs\ unfolding all_is_branch_def Dup_def by fast lemma omit_branch_mem_diff_formula: assumes \all_is_branch p i branch xs\ \q at i in branch\ \p \ q\ shows \q at i in omit_branch xs branch\ proof - obtain ps where ps: \(ps, i) \. branch\ \q on (ps, i)\ using assms(2) by blast then obtain v where v: \branch !. v = Some (ps, i)\ using rev_nth_mem by fast then have \omit_branch xs branch !. v = Some (omit (proj xs v) ps, i)\ unfolding omit_branch_def by (simp add: mapi_rev_nth) then have *: \(omit (proj xs v) ps, i) \. omit_branch xs branch\ using rev_nth_mem by fast moreover have \all_is p ps (proj xs v)\ using assms(1) v all_is_branch by fast then have \q on (omit (proj xs v) ps, i)\ using ps assms(3) omit_all_is by auto ultimately show ?thesis by blast qed lemma Dup_omit_branch_mem: assumes \Dup p i branch xs\ \q at a in branch\ shows \q at a in omit_branch xs branch\ using assms omit_branch_mem_diff_opening Dup_touches Dup_omit_branch_mem_same_opening omit_branch_mem_diff_formula Dup_all_is_branch by fast lemma omit_set: \set (omit xs ps) \ set ps\ by (induct ps) auto lemma on_omit: \p on (omit xs ps, i) \ p on (ps, i)\ using omit_set by auto lemma all_is_set: assumes \all_is p ps xs\ shows \{p} \ set (omit xs ps) = {p} \ set ps\ using assms omit_all_is omit_set unfolding all_is_def by fast lemma all_is_list_nominals: assumes \all_is p ps xs\ shows \nominals p \ list_nominals (omit xs ps) = nominals p \ list_nominals ps\ using assms all_is_set by fastforce lemma all_is_block_nominals: assumes \all_is p ps xs\ shows \nominals p \ block_nominals (omit xs ps, i) = nominals p \ block_nominals (ps, i)\ using assms by (simp add: all_is_list_nominals) lemma all_is_branch_nominals': assumes \all_is_branch p i branch xs\ shows \nominals p \ branch_nominals (omit_branch xs branch) = nominals p \ branch_nominals branch\ proof - have \\(v, v') \ xs. v < length branch \ is_at p i branch v v'\ using assms unfolding all_is_branch_def is_at_def by auto then show ?thesis proof (induct branch) case Nil then show ?case unfolding omit_branch_def by simp next case (Cons block branch) then show ?case proof (cases block) case (Pair ps a) have \\(v, v') \ xs. v < length branch \ is_at p i branch v v'\ using Cons(2) rev_nth_Cons unfolding is_at_def by auto then have \nominals p \ branch_nominals (omit_branch xs branch) = nominals p \ branch_nominals branch\ using Cons(1) by blast then have \nominals p \ branch_nominals (omit_branch xs ((ps, a) # branch)) = nominals p \ block_nominals (omit (proj xs (length branch)) ps, a) \ branch_nominals branch\ unfolding branch_nominals_def omit_branch_def by auto moreover have \all_is p ps (proj xs (length branch))\ using Cons(2) Pair unfolding proj_def all_is_def is_at_def by auto then have \nominals p \ block_nominals (omit (proj xs (length branch)) ps, a) = nominals p \ block_nominals (ps, a)\ using all_is_block_nominals by fast then have \nominals p \ block_nominals (omit_block (proj xs (length branch)) (ps, a)) = nominals p \ block_nominals (ps, a)\ by simp ultimately have \nominals p \ branch_nominals (omit_branch xs ((ps, a) # branch)) = nominals p \ block_nominals (ps, a) \ branch_nominals branch\ by auto then show ?thesis unfolding branch_nominals_def using Pair by auto qed qed qed lemma Dup_branch_nominals: assumes \Dup p i branch xs\ shows \branch_nominals (omit_branch xs branch) = branch_nominals branch\ proof (cases \xs = {}\) case True then show ?thesis using omit_branch_id by metis next case False with assms obtain ps w w' where \(w, w') \ xs\ \branch !. w = Some (ps, i)\ \p = Nom i \ ps !. w' = Some p\ unfolding Dup_def is_elsewhere_def by fast then have *: \(ps, i) \. branch\ \p on (ps, i)\ using rev_nth_mem rev_nth_on by fast+ then have \nominals p \ branch_nominals branch\ unfolding branch_nominals_def using block_nominals by fast moreover obtain ps' where \(ps', i) \. omit_branch xs branch\ \p on (ps', i)\ using assms * Dup_omit_branch_mem by fast then have \nominals p \ branch_nominals (omit_branch xs branch)\ unfolding branch_nominals_def using block_nominals by fast moreover have \nominals p \ branch_nominals (omit_branch xs branch) = nominals p \ branch_nominals branch\ using assms all_is_branch_nominals' Dup_all_is_branch by fast ultimately show ?thesis by blast qed lemma omit_branch_mem_dual: assumes \p at i in omit_branch xs branch\ shows \p at i in branch\ proof - obtain ps where ps: \(ps, i) \. omit_branch xs branch\ \p on (ps, i)\ using assms(1) by blast then obtain v where v: \omit_branch xs branch !. v = Some (ps, i)\ using rev_nth_mem unfolding omit_branch_def by fast then have \v < length (omit_branch xs branch)\ using rev_nth_Some by fast then have \v < length branch\ unfolding omit_branch_def using length_mapi by metis then obtain ps' i' where ps': \branch !. v = Some (ps', i')\ using rev_nth_bounded by (metis surj_pair) then have \omit_branch xs branch !. v = Some (omit (proj xs v) ps', i')\ unfolding omit_branch_def by (simp add: mapi_rev_nth) then have \ps = omit (proj xs v) ps'\ \i = i'\ using v by simp_all then have \p on (ps', i)\ using ps omit_set by auto moreover have \(ps', i) \. branch\ using ps' \i = i'\ rev_nth_mem by fast ultimately show ?thesis using \ps = omit (proj xs v) ps'\ by blast qed lemma witnessed_omit_branch: assumes \witnessed p a (omit_branch xs branch)\ shows \witnessed p a branch\ proof - obtain ps qs i where ps: \(ps, a) \. omit_branch xs branch\ \(\<^bold>@ i p) on (ps, a)\ and qs: \(qs, a) \. omit_branch xs branch\ \(\<^bold>\ Nom i) on (qs, a)\ using assms unfolding witnessed_def by blast from ps obtain ps' where \(ps', a) \. branch\ \(\<^bold>@ i p) on (ps', a)\ using omit_branch_mem_dual by fast moreover from qs obtain qs' where \(qs', a) \. branch\ \(\<^bold>\ Nom i) on (qs', a)\ using omit_branch_mem_dual by fast ultimately show ?thesis unfolding witnessed_def by blast qed lemma new_omit_branch: assumes \new p a branch\ shows \new p a (omit_branch xs branch)\ using assms omit_branch_mem_dual unfolding new_def by fast lemma omit_oob: assumes \length ps \ v\ shows \omit ({v} \ xs) ps = omit xs ps\ using assms by (induct ps) simp_all lemma omit_branch_oob: assumes \length branch \ v\ shows \omit_branch ({(v, v')} \ xs) branch = omit_branch xs branch\ using assms proof (induct branch) case Nil then show ?case unfolding omit_branch_def by simp next case (Cons block branch) let ?xs = \({(v, v')} \ xs)\ show ?case proof (cases block) case (Pair ps a) then have \omit_branch ?xs ((ps, a) # branch) = (omit (proj ?xs (length branch)) ps, a) # omit_branch xs branch\ using Cons unfolding omit_branch_def by simp moreover have \proj ?xs (length branch) = proj xs (length branch)\ using Cons(2) unfolding proj_def by auto ultimately show ?thesis unfolding omit_branch_def by simp qed qed subsection \Induction\ -lemma ST_Dup: +lemma STA_Dup: assumes \A, n \ branch\ \Dup q i branch xs\ shows \A, n \ omit_branch xs branch\ using assms proof (induct n branch) case (Close p i' branch n) have \p at i' in omit_branch xs branch\ using Close(1, 3) Dup_omit_branch_mem by fast moreover have \(\<^bold>\ p) at i' in omit_branch xs branch\ using Close(2, 3) Dup_omit_branch_mem by fast ultimately show ?case - using ST.Close by fast + using STA.Close by fast next case (Neg p a ps branch n) have \A, Suc n \ omit_branch xs ((p # ps, a) # branch)\ using Neg(4-) Dup_head by fast moreover have \(length branch, length ps) \ xs\ using Neg(5) Dup_head_oob by fast ultimately have \A, Suc n \ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp moreover have \(\<^bold>\ \<^bold>\ p) at a in omit_branch xs ((ps, a) # branch)\ using Neg(1, 5) Dup_omit_branch_mem by fast moreover have \new p a (omit_branch xs ((ps, a) # branch))\ using Neg(2) new_omit_branch by fast ultimately show ?case - by (simp add: omit_branch_def ST.Neg) + by (simp add: omit_branch_def STA.Neg) next case (DisP p q a ps branch n) have \A, Suc n \ omit_branch xs ((p # ps, a) # branch)\ \A, Suc n \ omit_branch xs ((q # ps, a) # branch)\ using DisP(4-) Dup_head by fast+ moreover have \(length branch, length ps) \ xs\ using DisP(8) Dup_head_oob by fast ultimately have \A, Suc n \ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ \A, Suc n \ (q # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp_all moreover have \(p \<^bold>\ q) at a in omit_branch xs ((ps, a) # branch)\ using DisP(1, 8) Dup_omit_branch_mem by fast moreover have \new p a (omit_branch xs ((ps, a) # branch))\ using DisP(2) new_omit_branch by fast moreover have \new q a (omit_branch xs ((ps, a) # branch))\ using DisP(3) new_omit_branch by fast ultimately show ?case - by (simp add: omit_branch_def ST.DisP) + by (simp add: omit_branch_def STA.DisP) next case (DisN p q a ps branch n) have \A, Suc n \ omit_branch xs (((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch)\ using DisN(4-) Dup_block[where ps'=\[_, _]\] by fastforce moreover have \(length branch, length ps) \ xs\ using DisN(5) Dup_head_oob by fast moreover have \(length branch, 1 + length ps) \ xs\ using DisN(5) Dup_head_oob' by fast ultimately have \A, Suc n \ ((\<^bold>\ q) # (\<^bold>\ p) # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp moreover have \(\<^bold>\ (p \<^bold>\ q)) at a in omit_branch xs ((ps, a) # branch)\ using DisN(1, 5) Dup_omit_branch_mem by fast moreover have \new (\<^bold>\ p) a (omit_branch xs ((ps, a) # branch)) \ new (\<^bold>\ q) a (omit_branch xs ((ps, a) # branch))\ using DisN(2) new_omit_branch by fast ultimately show ?case - by (simp add: omit_branch_def ST.DisN) + by (simp add: omit_branch_def STA.DisN) next case (DiaP p a ps branch i n) have \A, Suc n \ omit_branch xs (((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch)\ using DiaP(4-) Dup_block[where ps'=\[_, _]\] by fastforce moreover have \(length branch, length ps) \ xs\ using DiaP(7) Dup_head_oob by fast moreover have \(length branch, 1+ length ps) \ xs\ using DiaP(7) Dup_head_oob' by fast ultimately have \A, Suc n \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp moreover have \(\<^bold>\ p) at a in omit_branch xs ((ps, a) # branch)\ using DiaP(1, 7) Dup_omit_branch_mem by fast moreover have \i \ A \ branch_nominals (omit_branch xs ((ps, a) # branch))\ using DiaP(2, 7) Dup_branch_nominals by fast moreover have \\ witnessed p a (omit_branch xs ((ps, a) # branch))\ using DiaP(4) witnessed_omit_branch by fast ultimately show ?case - using DiaP(3) by (simp add: omit_branch_def ST.DiaP) + using DiaP(3) by (simp add: omit_branch_def STA.DiaP) next case (DiaN p a ps branch i n) have \A, Suc n \ omit_branch xs (((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch)\ using DiaN(4-) Dup_head by fast moreover have \(length branch, length ps) \ xs\ using DiaN(6) Dup_head_oob by fast ultimately have \A, Suc n \ ((\<^bold>\ (\<^bold>@ i p)) # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp moreover have \(\<^bold>\ (\<^bold>\ p)) at a in omit_branch xs ((ps, a) # branch)\ using DiaN(1, 6) Dup_omit_branch_mem by fast moreover have \(\<^bold>\ Nom i) at a in omit_branch xs ((ps, a) # branch)\ using DiaN(2, 6) Dup_omit_branch_mem by fast moreover have \new (\<^bold>\ (\<^bold>@ i p)) a (omit_branch xs ((ps, a) # branch))\ using DiaN(3) new_omit_branch by fast ultimately show ?case - by (simp add: omit_branch_def ST.DiaN) + by (simp add: omit_branch_def STA.DiaN) next case (SatP a p b ps branch n) have \A, Suc n \ omit_branch xs ((p # ps, a) # branch)\ using SatP(4-) Dup_head by fast moreover have \(length branch, length ps) \ xs\ using SatP(5) Dup_head_oob by fast ultimately have \A, Suc n \ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp moreover have \(\<^bold>@ a p) at b in omit_branch xs ((ps, a) # branch)\ using SatP(1, 5) Dup_omit_branch_mem by fast moreover have \new p a (omit_branch xs ((ps, a) # branch))\ using SatP(2) new_omit_branch by fast ultimately show ?case - by (simp add: omit_branch_def ST.SatP) + by (simp add: omit_branch_def STA.SatP) next case (SatN a p b ps branch n) have \A, Suc n \ omit_branch xs (((\<^bold>\ p) # ps, a) # branch)\ using SatN(4-) Dup_head by fast moreover have \(length branch, length ps) \ xs\ using SatN(5) Dup_head_oob by fast ultimately have \A, Suc n \ ((\<^bold>\ p) # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp moreover have \(\<^bold>\ (\<^bold>@ a p)) at b in omit_branch xs ((ps, a) # branch)\ using SatN(1, 5) Dup_omit_branch_mem by fast moreover have \new (\<^bold>\ p) a (omit_branch xs ((ps, a) # branch))\ using SatN(2) new_omit_branch by fast ultimately show ?case - by (simp add: omit_branch_def ST.SatN) + by (simp add: omit_branch_def STA.SatN) next case (GoTo i branch n) then have \A, n \ omit_branch xs (([], i) # branch)\ using Dup_branch[where extra=\[([], i)]\] by fastforce then have \A, n \ ([], i) # omit_branch xs branch\ unfolding omit_branch_def by simp moreover have \i \ branch_nominals (omit_branch xs branch)\ using GoTo(1, 4) Dup_branch_nominals by fast ultimately show ?case - unfolding omit_branch_def by (simp add: ST.GoTo) + unfolding omit_branch_def by (simp add: STA.GoTo) next case (Nom p b ps a branch n) have \A, Suc n \ omit_branch xs ((p # ps, a) # branch)\ using Nom(4-) Dup_head by fast moreover have \(length branch, length ps) \ xs\ using Nom(7) Dup_head_oob by fast ultimately have \A, Suc n \ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ unfolding omit_branch_def proj_def by simp moreover have \p at b in omit_branch xs ((ps, a) # branch)\ using Nom(1, 7) Dup_omit_branch_mem by fast moreover have \Nom a at b in omit_branch xs ((ps, a) # branch)\ using Nom(2, 7) Dup_omit_branch_mem by fast moreover have \new p a (omit_branch xs ((ps, a) # branch))\ using Nom(4) new_omit_branch by fast ultimately show ?case - using Nom(3) by (simp add: omit_branch_def ST.Nom) + using Nom(3) by (simp add: omit_branch_def STA.Nom) qed theorem Dup: assumes \A, n \ (p # ps, a) # branch\ \\ new p a ((ps, a) # branch)\ shows \A, n \ (ps, a) # branch\ proof - obtain qs where qs: \(qs, a) \. (ps, a) # branch\ \p on (qs, a)\ using assms(2) unfolding new_def by blast let ?xs = \{(length branch, length ps)}\ have *: \is_at p a ((p # ps, a) # branch) (length branch) (length ps)\ unfolding is_at_def by simp have \Dup p a ((p # ps, a) # branch) ?xs\ proof (cases \p = Nom a\) case True moreover have \((p # ps, a) # branch) !. length branch = Some (p # ps, a)\ by simp moreover have \p on (p # ps, a)\ by simp ultimately have \is_elsewhere p a ((p # ps, a) # branch) ?xs\ unfolding is_elsewhere_def using assms(2) rev_nth_Some by (metis (mono_tags, lifting) Pair_inject less_le singletonD) then show ?thesis unfolding Dup_def using * by blast next case false: False then show ?thesis proof (cases \ps = qs\) case True then obtain w' where w': \qs !. w' = Some p\ using qs(2) false rev_nth_mem by fastforce then have \(p # ps) !. w' = Some p\ using True rev_nth_Cons by fast moreover have \((p # ps, a) # branch) !. length branch = Some (p # ps, a)\ by simp moreover have \(length branch, w') \ ?xs\ using True w' rev_nth_Some by fast ultimately have \is_elsewhere p a ((p # ps, a) # branch) ?xs\ unfolding is_elsewhere_def by fast then show ?thesis unfolding Dup_def using * by fast next case False then obtain w where w: \branch !. w = Some (qs, a)\ using qs(1) rev_nth_mem by fastforce moreover obtain w' where w': \qs !. w' = Some p\ using qs(2) false rev_nth_mem by fastforce moreover have \(w, w') \ ?xs\ using rev_nth_Some w by fast ultimately have \is_elsewhere p a ((p # ps, a) # branch) ?xs\ unfolding is_elsewhere_def using rev_nth_Cons by fast then show ?thesis unfolding Dup_def using * by fast qed qed then have \A, n \ omit_branch ?xs ((p # ps, a) # branch)\ - using assms(1) ST_Dup by fast + using assms(1) STA_Dup by fast then have \A, n \ (omit (proj ?xs (length branch)) ps, a) # omit_branch ?xs branch\ unfolding omit_branch_def proj_def by simp moreover have \omit_branch ?xs branch = omit_branch {} branch\ using omit_branch_oob by auto then have \omit_branch ?xs branch = branch\ using omit_branch_id by simp moreover have \proj ?xs (length branch) = {length ps}\ unfolding proj_def by blast then have \omit (proj ?xs (length branch)) ps = omit {} ps\ using omit_oob by auto then have \omit (proj ?xs (length branch)) ps = ps\ using omit_id by simp ultimately show ?thesis by simp qed subsection \Unrestricted rules\ -lemma ST_add: \A, n \ branch \ A, m + n \ branch\ - using ST_Suc by (induct m) auto - -lemma ST_le: \A, n \ branch \ n \ m \ A, m \ branch\ - using ST_add by (metis le_add_diff_inverse2) +lemma STA_add: \A, n \ branch \ A, m + n \ branch\ + using STA_Suc by (induct m) auto + +lemma STA_le: \A, n \ branch \ n \ m \ A, m \ branch\ + using STA_add by (metis le_add_diff_inverse2) lemma Neg': assumes \(\<^bold>\ \<^bold>\ p) at a in (ps, a) # branch\ \A, n \ (p # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ - using assms Neg Dup ST_Suc by metis + using assms Neg Dup STA_Suc by metis lemma DisP': assumes \(p \<^bold>\ q) at a in (ps, a) # branch\ \A, n \ (p # ps, a) # branch\ \A, n \ (q # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ proof (cases \new p a ((ps, a) # branch) \ new q a ((ps, a) # branch)\) case True moreover have \A, Suc n \ (p # ps, a) # branch\ \A, Suc n \ (q # ps, a) # branch\ - using assms(2-3) ST_Suc by fast+ + using assms(2-3) STA_Suc by fast+ ultimately show ?thesis using assms(1) DisP by fast next case False then show ?thesis using assms Dup by fast qed lemma DisP'': assumes \(p \<^bold>\ q) at a in (ps, a) # branch\ \A, n \ (p # ps, a) # branch\ \A, m \ (q # ps, a) # branch\ shows \A, max n m \ (ps, a) # branch\ proof (cases \n \ m\) case True then have \A, m \ (p # ps, a) # branch\ - using assms(2) ST_le by blast + using assms(2) STA_le by blast then show ?thesis using assms True by (simp add: DisP' max.absorb2) next case False then have \A, n \ (q # ps, a) # branch\ - using assms(3) ST_le by fastforce + using assms(3) STA_le by fastforce then show ?thesis using assms False by (simp add: DisP' max.absorb1) qed lemma DisN': assumes \(\<^bold>\ (p \<^bold>\ q)) at a in (ps, a) # branch\ \A, n \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ proof (cases \new (\<^bold>\ q) a ((ps, a) # branch) \ new (\<^bold>\ p) a ((ps, a) # branch)\) case True then show ?thesis - using assms DisN ST_Suc by fast + using assms DisN STA_Suc by fast next case False then show ?thesis using assms Dup by (metis (no_types, lifting) list.set_intros(1-2) new_def on.simps set_ConsD) qed lemma DiaP': assumes \(\<^bold>\ p) at a in (ps, a) # branch\ \i \ A \ branch_nominals ((ps, a) # branch)\ \\a. p = Nom a\ \\ witnessed p a ((ps, a) # branch)\ \A, n \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ - using assms DiaP ST_Suc by fast + using assms DiaP STA_Suc by fast lemma DiaN': assumes \(\<^bold>\ (\<^bold>\ p)) at a in (ps, a) # branch\ \(\<^bold>\ Nom i) at a in (ps, a) # branch\ \A, n \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ - using assms DiaN Dup ST_Suc by fast + using assms DiaN Dup STA_Suc by fast lemma SatP': assumes \(\<^bold>@ a p) at b in (ps, a) # branch\ \A, n \ (p # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ - using assms SatP Dup ST_Suc by fast + using assms SatP Dup STA_Suc by fast lemma SatN': assumes \(\<^bold>\ (\<^bold>@ a p)) at b in (ps, a) # branch\ \A, n \ ((\<^bold>\ p) # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ - using assms SatN Dup ST_Suc by fast + using assms SatN Dup STA_Suc by fast lemma Nom': assumes \p at b in (ps, a) # branch\ \Nom a at b in (ps, a) # branch\ \\i. p = Nom i \ p = (\<^bold>\ Nom i) \ i \ A\ \A, n \ (p # ps, a) # branch\ shows \A, n \ (ps, a) # branch\ proof (cases \new p a ((ps, a) # branch)\) case True moreover have \A, Suc n \ (p # ps, a) # branch\ - using assms(4) ST_Suc by blast + using assms(4) STA_Suc by blast ultimately show ?thesis using assms(1-3) Nom by metis next case False then show ?thesis using assms Dup by fast qed section \Substitution\ lemma finite_nominals: \finite (nominals p)\ by (induct p) simp_all lemma finite_block_nominals: \finite (block_nominals block)\ using finite_nominals by (induct block) auto lemma finite_branch_nominals: \finite (branch_nominals branch)\ unfolding branch_nominals_def by (induct branch) (auto simp: finite_block_nominals) abbreviation sub_list :: \('b \ 'c) \ ('a, 'b) fm list \ ('a, 'c) fm list\ where \sub_list f ps \ map (sub f) ps\ primrec sub_block :: \('b \ 'c) \ ('a, 'b) block \ ('a, 'c) block\ where \sub_block f (ps, i) = (sub_list f ps, f i)\ definition sub_branch :: \('b \ 'c) \ ('a, 'b) branch \ ('a, 'c) branch\ where \sub_branch f blocks \ map (sub_block f) blocks\ lemma sub_block_mem: \p on block \ sub f p on sub_block f block\ by (induct block) auto lemma sub_branch_mem: assumes \(ps, i) \. branch\ shows \(sub_list f ps, f i) \. sub_branch f branch\ unfolding sub_branch_def using assms image_iff by fastforce lemma sub_block_nominals: \block_nominals (sub_block f block) = f ` block_nominals block\ by (induct block) (auto simp: sub_nominals) lemma sub_branch_nominals: \branch_nominals (sub_branch f branch) = f ` branch_nominals branch\ unfolding branch_nominals_def sub_branch_def by (induct branch) (auto simp: sub_block_nominals) lemma sub_list_id: \sub_list id ps = ps\ using sub_id by (induct ps) auto lemma sub_block_id: \sub_block id block = block\ using sub_list_id by (induct block) auto lemma sub_branch_id: \sub_branch id branch = branch\ unfolding sub_branch_def using sub_block_id by (induct branch) auto lemma sub_block_upd_fresh: assumes \i \ block_nominals block\ shows \sub_block (f(i := j)) block = sub_block f block\ using assms by (induct block) (auto simp add: sub_upd_fresh) lemma sub_branch_upd_fresh: assumes \i \ branch_nominals branch\ shows \sub_branch (f(i := j)) branch = sub_branch f branch\ using assms unfolding branch_nominals_def sub_branch_def by (induct branch) (auto simp: sub_block_upd_fresh) lemma sub_comp: \sub f (sub g p) = sub (f o g) p\ by (induct p) simp_all lemma sub_list_comp: \sub_list f (sub_list g ps) = sub_list (f o g) ps\ using sub_comp by (induct ps) auto lemma sub_block_comp: \sub_block f (sub_block g block) = sub_block (f o g) block\ using sub_list_comp by (induct block) simp_all lemma sub_branch_comp: \sub_branch f (sub_branch g branch) = sub_branch (f o g) branch\ unfolding sub_branch_def using sub_block_comp by (induct branch) fastforce+ lemma swap_id: \(id(i := j, j := i)) o (id(i := j, j := i)) = id\ by auto lemma at_in_sub_branch: assumes \p at i in (ps, a) # branch\ shows \sub f p at f i in (sub_list f ps, f a) # sub_branch f branch\ using assms sub_branch_mem by fastforce lemma sub_still_allowed: assumes \\i. p = Nom i \ p = (\<^bold>\ Nom i) \ i \ A\ shows \sub f p = Nom i \ sub f p = (\<^bold>\ Nom i) \ i \ f ` A\ proof safe assume \sub f p = Nom i\ then obtain i' where i': \p = Nom i'\ \f i' = i\ by (cases p) simp_all then have \i' \ A\ using assms by fast then show \i \ f ` A\ using i' by fast next assume \sub f p = (\<^bold>\ Nom i)\ then obtain i' where i': \p = (\<^bold>\ Nom i')\ \f i' = i\ proof (induct p) case (Dia q) then show ?case by (cases q) simp_all qed simp_all then have \i' \ A\ using assms by fast then show \i \ f ` A\ using i' by fast qed text \ If a branch has a closing tableau then so does any branch obtained by renaming nominals as long as the substitution leaves some nominals free. This is always the case for substitutions that do not change the type of nominals. Since some formulas on the renamed branch may no longer be new, they do not contribute any potential and so we existentially quantify over the potential needed to close the new branch. We assume that the set of allowed nominals \A\ is finite such that we can obtain a free nominal. \ -lemma ST_sub': +lemma STA_sub': fixes f :: \'b \ 'c\ assumes \\(f :: 'b \ 'c) i A. finite A \ i \ A \ \j. j \ f ` A\ \finite A\ \A, n \ branch\ shows \f ` A \ sub_branch f branch\ using assms(3-) -proof (induct n branch arbitrary: f rule: ST.induct) +proof (induct n branch arbitrary: f rule: STA.induct) case (Close p i branch n) have \sub f p at f i in sub_branch f branch\ using Close(1) sub_branch_mem by fastforce moreover have \(\<^bold>\ sub f p) at f i in sub_branch f branch\ using Close(2) sub_branch_mem by force ultimately show ?case - using ST.Close by fast + using STA.Close by fast next case (Neg p a ps branch n f) then have \f ` A \ (sub f p # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp moreover have \(\<^bold>\ \<^bold>\ sub f p) at f a in (sub_list f ps, f a) # sub_branch f branch\ using Neg(1) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(3)) ultimately have \f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using Neg' by fast then show ?case unfolding sub_branch_def by simp next case (DisP p q a ps branch n) then have \f ` A \ (sub f p # sub_list f ps, f a) # sub_branch f branch\ \f ` A \ (sub f q # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp_all moreover have \(sub f p \<^bold>\ sub f q) at f a in (sub_list f ps, f a) # sub_branch f branch\ using DisP(1) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(4)) ultimately have \f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using DisP'' by fast then show ?case unfolding sub_branch_def by simp next case (DisN p q a ps branch n) then have \f ` A \ ((\<^bold>\ sub f q) # (\<^bold>\ sub f p) # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp moreover have \(\<^bold>\ (sub f p \<^bold>\ sub f q)) at f a in (sub_list f ps, f a) # sub_branch f branch\ using DisN(1) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(3-4)) ultimately have \f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using DisN' by fast then show ?case unfolding sub_branch_def by simp next case (DiaP p a ps branch i n) have \i \ A\ using DiaP(2) by simp show ?case proof (cases \witnessed (sub f p) (f a) (sub_branch f ((ps, a) # branch))\) case True then obtain i' where rs: \(\<^bold>@ i' (sub f p)) at f a in (sub_list f ps, f a) # sub_branch f branch\ and ts: \(\<^bold>\ Nom i') at f a in (sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def witnessed_def by auto from rs have rs': \(\<^bold>@ i' (sub f p)) at f a in ((\<^bold>\ Nom i') # sub_list f ps, f a) # sub_branch f branch\ by fastforce let ?f = \f(i := i')\ let ?branch = \sub_branch ?f branch\ have \sub_branch ?f ((ps, a) # branch) = sub_branch f ((ps, a) # branch)\ using DiaP(2) sub_branch_upd_fresh by fast then have **: \sub_list ?f ps = sub_list f ps\ \?f a = f a\ \?branch = sub_branch f branch\ unfolding sub_branch_def by simp_all have p: \sub ?f p = sub f p\ using DiaP(1-2) sub_upd_fresh unfolding branch_nominals_def by fastforce have \?f ` A \ sub_branch ?f (((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch)\ using DiaP(6) by blast then have \?f ` A \ ((\<^bold>@ (?f i) (sub ?f p)) # (\<^bold>\ Nom (?f i)) # sub_list ?f ps, ?f a) # ?branch\ unfolding sub_branch_def by fastforce then have \?f ` A \ ((\<^bold>@ i' (sub f p)) # (\<^bold>\ Nom i') # sub_list f ps, f a) # sub_branch f branch\ using p ** by simp then have \?f ` A \ ((\<^bold>\ Nom i') # sub_list f ps, f a) # sub_branch f branch\ using rs' by (meson Dup new_def) then have \?f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using ts by (meson Dup new_def) moreover have \?f ` A = f ` A\ using \i \ A\ by auto ultimately show ?thesis unfolding sub_branch_def by auto next case False have \finite (branch_nominals ((ps, a) # branch))\ by (simp add: finite_branch_nominals) then have \finite (A \ branch_nominals ((ps, a) # branch))\ using \finite A\ by simp then obtain j where *: \j \ f ` (A \ branch_nominals ((ps, a) # branch))\ using DiaP(2) assms by metis then have \j \ f ` A\ by blast let ?f = \f(i := j)\ let ?branch = \sub_branch ?f branch\ have **: \sub_branch ?f ((ps, a) # branch) = sub_branch f ((ps, a) # branch)\ using DiaP(2) sub_branch_upd_fresh by fast then have ***: \sub_list ?f ps = sub_list f ps\ \?f a = f a\ \?branch = sub_branch f branch\ unfolding sub_branch_def by simp_all moreover have p: \sub ?f p = sub f p\ using DiaP(1-2) sub_upd_fresh unfolding branch_nominals_def by fastforce ultimately have \\ witnessed (sub ?f p) (?f a) (sub_branch ?f ((ps, a) # branch))\ using False ** by simp then have w: \\ witnessed (sub ?f p) (?f a) ((sub_list ?f ps, ?f a) # ?branch)\ unfolding sub_branch_def by simp have f: \?f ` A = f ` A\ using \i \ A\ by auto have \?f ` A \ sub_branch ?f (((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch)\ using DiaP(6) by blast then have \f ` A \ ((\<^bold>@ (?f i) (sub ?f p)) # (\<^bold>\ Nom (?f i)) # sub_list ?f ps, ?f a) # ?branch\ unfolding sub_branch_def using f by simp moreover have \sub ?f (\<^bold>\ p) at ?f a in (sub_list ?f ps, ?f a) # sub_branch ?f branch\ using DiaP(1) at_in_sub_branch by fast then have \(\<^bold>\ sub ?f p) at ?f a in (sub_list ?f ps, ?f a) # sub_branch ?f branch\ by simp moreover have \\a. sub ?f p = Nom a\ using DiaP(3) by (cases p) simp_all moreover have \j \ f ` (branch_nominals ((ps, a) # branch))\ using * by blast then have \?f i \ branch_nominals ((sub_list ?f ps, ?f a) # ?branch)\ using ** sub_branch_nominals unfolding sub_branch_def by (metis fun_upd_same list.simps(9) sub_block.simps) ultimately have \f ` A \ (sub_list ?f ps, ?f a) # ?branch\ using w DiaP' \j \ f ` A\ by (metis Un_iff fun_upd_same) then show ?thesis using *** unfolding sub_branch_def by simp qed next case (DiaN p a ps branch i n) then have \f ` A \ ((\<^bold>\ (\<^bold>@ (f i) (sub f p))) # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp moreover have \(\<^bold>\ (\<^bold>\ sub f p)) at f a in (sub_list f ps, f a) # sub_branch f branch\ using DiaN(1) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(3, 5)) moreover have \(\<^bold>\ Nom (f i)) at f a in (sub_list f ps, f a) # sub_branch f branch\ using DiaN(2) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(2, 5)) ultimately have \f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using DiaN' by fast then show ?case unfolding sub_branch_def by simp next case (SatP a p b ps branch n) then have \f ` A \ (sub f p # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp moreover have \(\<^bold>@ (f a) (sub f p)) at f b in (sub_list f ps, f a) # sub_branch f branch\ using SatP(1) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(6)) ultimately have \f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using SatP' by fast then show ?case unfolding sub_branch_def by simp next case (SatN a p b ps branch n) then have \f ` A \ ((\<^bold>\ sub f p) # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp moreover have \(\<^bold>\ (\<^bold>@ (f a) (sub f p))) at f b in (sub_list f ps, f a) # sub_branch f branch\ using SatN(1) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(3, 6)) ultimately have \f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using SatN' by fast then show ?case unfolding sub_branch_def by simp next case (GoTo i branch n) then have \f ` A \ ([], f i) # sub_branch f branch\ unfolding sub_branch_def by simp moreover have \f i \ branch_nominals (sub_branch f branch)\ using GoTo(1) sub_branch_nominals by fast ultimately show ?case - using ST.GoTo by fast + using STA.GoTo by fast next case (Nom p b ps a branch n) then have \f ` A \ sub_branch f ((p # ps, a) # branch)\ by blast then have \f ` A \ (sub f p # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp moreover have \sub f p at f b in (sub_list f ps, f a) # sub_branch f branch\ using Nom(1) at_in_sub_branch by fast moreover have \Nom (f a) at f b in (sub_list f ps, f a) # sub_branch f branch\ using Nom(2) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(2)) moreover have \\i. sub f p = Nom i \ sub f p = (\<^bold>\ Nom i) \ i \ f ` A\ using Nom(3) sub_still_allowed by metis ultimately have \f ` A \ (sub_list f ps, f a) # sub_branch f branch\ using Nom' by metis then show ?case unfolding sub_branch_def by simp qed lemma ex_fresh_gt: fixes f :: \'b \ 'c\ assumes \\g :: 'c \ 'b. surj g\ \finite A\ \i \ A\ shows \\j. j \ f ` A\ proof (rule ccontr) assume \\j. j \ f ` A\ moreover obtain g :: \'c \ 'b\ where \surj g\ using assms(1) by blast ultimately show False using assms(2-3) by (metis UNIV_I UNIV_eq_I card_image_le card_seteq finite_imageI image_comp subsetI) qed -corollary ST_sub_gt: +corollary STA_sub_gt: fixes f :: \'b \ 'c\ assumes \\g :: 'c \ 'b. surj g\ \A \ branch\ \finite A\ \\i \ branch_nominals branch. f i \ f ` A \ i \ A\ shows \f ` A \ sub_branch f branch\ - using assms ex_fresh_gt ST_sub' by metis - -corollary ST_sub_inf: + using assms ex_fresh_gt STA_sub' by metis + +corollary STA_sub_inf: fixes f :: \'b \ 'c\ assumes \infinite (UNIV :: 'c set)\ \A \ branch\ \finite A\ \\i \ branch_nominals branch. f i \ f ` A \ i \ A\ shows \f ` A \ sub_branch f branch\ proof - have \finite A \ \j. j \ f ` A\ for A and f :: \'b \ 'c\ using assms(1) ex_new_if_finite by blast then show ?thesis - using assms(2-) ST_sub' by metis + using assms(2-) STA_sub' by metis qed -corollary ST_sub: +corollary STA_sub: fixes f :: \'b \ 'b\ assumes \A \ branch\ \finite A\ shows \f ` A \ sub_branch f branch\ proof - have \finite A \ i \ A \ \j. j \ f ` A\ for i A and f :: \'b \ 'b\ by (metis card_image_le card_seteq finite_imageI subsetI) then show ?thesis - using assms ST_sub' by metis + using assms STA_sub' by metis qed subsection \Unrestricted \(\<^bold>\)\ rule\ lemma DiaP'': assumes \(\<^bold>\ p) at a in (ps, a) # branch\ \i \ A \ branch_nominals ((ps, a) # branch)\ \\a. p = Nom a\ \finite A\ \A \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch\ shows \A \ (ps, a) # branch\ proof (cases \witnessed p a ((ps, a) # branch)\) case True then obtain i' where rs: \(\<^bold>@ i' p) at a in (ps, a) # branch\ and ts: \(\<^bold>\ Nom i') at a in (ps, a) # branch\ unfolding witnessed_def by blast then have rs': \(\<^bold>@ i' p) at a in ((\<^bold>\ Nom i') # ps, a) # branch\ by fastforce let ?f = \id(i := i')\ have \?f ` A \ sub_branch ?f (((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch)\ - using assms(4-5) ST_sub by blast + using assms(4-5) STA_sub by blast then have \?f ` A \ ((\<^bold>@ i' (sub ?f p)) # (\<^bold>\ Nom i') # sub_list ?f ps, ?f a) # sub_branch ?f branch\ unfolding sub_branch_def by simp moreover have \i \ nominals p\ \i \ list_nominals ps\ \i \ a\ \i \ branch_nominals branch\ using assms(1-3) unfolding branch_nominals_def by fastforce+ then have \sub ?f p = p\ by (simp add: sub_id sub_upd_fresh) moreover have \sub_list ?f ps = ps\ using \i \ list_nominals ps\ by (simp add: map_idI sub_id sub_upd_fresh) moreover have \?f a = a\ using \i \ a\ by simp moreover have \sub_branch ?f branch = branch\ using \i \ branch_nominals branch\ by (simp add: sub_branch_id sub_branch_upd_fresh) ultimately have \?f ` A \ ((\<^bold>@ i' p) # (\<^bold>\ Nom i') # ps, a) # branch\ by simp then have \?f ` A \ ((\<^bold>\ Nom i') # ps, a) # branch\ using rs' by (meson Dup new_def) then have \?f ` A \ (ps, a) # branch\ using ts by (meson Dup new_def) moreover have \?f ` A = A\ using assms(2) by auto ultimately show ?thesis by simp next case False then show ?thesis - using assms DiaP' ST_Suc by fast + using assms DiaP' STA_Suc by fast qed section \Structural Properties\ lemma block_nominals_branch: assumes \block \. branch\ shows \block_nominals block \ branch_nominals branch\ unfolding branch_nominals_def using assms by blast lemma sub_block_fresh: assumes \i \ branch_nominals branch\ \block \. branch\ shows \sub_block (f(i := j)) block = sub_block f block\ using assms block_nominals_branch sub_block_upd_fresh by fast lemma list_down_induct [consumes 1, case_names Start Cons]: assumes \\y \ set ys. Q y\ \P (ys @ xs)\ \\y xs. Q y \ P (y # xs) \ P xs\ shows \P xs\ using assms by (induct ys) auto text \ If the last block on a branch has opening nominal \a\ and the last formulas on that block occur on another block alongside nominal \a\, then we can drop those formulas. \ -lemma ST_drop_prefix: +lemma STA_drop_prefix: assumes \set ps \ set qs\ \(qs, a) \. branch\ \A, n \ (ps @ ps', a) # branch\ shows \A, n \ (ps', a) # branch\ proof - have \\p \ set ps. p on (qs, a)\ using assms(1) by auto then show ?thesis proof (induct ps' rule: list_down_induct) case Start then show ?case using assms(3) . next case (Cons p ps) then show ?case using assms(2) by (meson Dup new_def list.set_intros(2)) qed qed text \We can drop a block if it is subsumed by another block.\ -lemma ST_drop_block: +lemma STA_drop_block: assumes \set ps \ set ps'\ \(ps', a) \. branch\ \A, n \ (ps, a) # branch\ shows \A, Suc n \ branch\ using assms proof (induct branch) case Nil then show ?case by simp next case (Cons block branch) then show ?case proof (cases block) case (Pair qs b) then have \A, n \ ([], a) # (qs, b) # branch\ - using Cons(2-4) ST_drop_prefix[where branch=\(qs, b) # branch\] by simp + using Cons(2-4) STA_drop_prefix[where branch=\(qs, b) # branch\] by simp moreover have \a \ branch_nominals ((qs, b) # branch)\ unfolding branch_nominals_def using Cons(3) Pair by fastforce ultimately have \A, Suc n \ (qs, b) # branch\ by (simp add: GoTo) then show ?thesis using Pair Dup by fast qed qed -lemma ST_drop_block': +lemma STA_drop_block': assumes \A, n \ (ps, a) # branch\ \(ps, a) \. branch\ shows \A, Suc n \ branch\ - using assms ST_drop_block by fastforce + using assms STA_drop_block by fastforce lemma sub_branch_image: \set (sub_branch f branch) = sub_block f ` set branch\ unfolding sub_branch_def by simp lemma sub_block_repl: assumes \j \ block_nominals block\ shows \i \ block_nominals (sub_block (id(i := j, j := i)) block)\ using assms by (simp add: image_iff sub_block_nominals) lemma sub_branch_repl: assumes \j \ branch_nominals branch\ shows \i \ branch_nominals (sub_branch (id(i := j, j := i)) branch)\ using assms by (simp add: image_iff sub_branch_nominals) text \If a finite set of blocks has a closing tableau then so does any finite superset.\ -lemma ST_struct: +lemma STA_struct: fixes branch :: \('a, 'b) branch\ assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and \A, n \ branch\ \set branch \ set branch'\ shows \A \ branch'\ using assms(3-) -proof (induct n branch arbitrary: branch' rule: ST.induct) +proof (induct n branch arbitrary: branch' rule: STA.induct) case (Close p i branch n) then show ?case - using ST.Close by fast + using STA.Close by fast next case (Neg p a ps branch n) have \A \ (p # ps, a) # branch'\ using Neg(4-) by (simp add: subset_code(1)) moreover have \(\<^bold>\ \<^bold>\ p) at a in (ps, a) # branch'\ using Neg(1, 5) by auto ultimately have \A \ (ps, a) # branch'\ using Neg' by fast moreover have \(ps, a) \. branch'\ using Neg(5) by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast next case (DisP p q a ps branch n) have \A \ (p # ps, a) # branch'\ \A \ (q # ps, a) # branch'\ using DisP(5, 7-) by (simp_all add: subset_code(1)) moreover have \(p \<^bold>\ q) at a in (ps, a) # branch'\ using DisP(1, 8) by auto ultimately have \A \ (ps, a) # branch'\ using DisP'' by fast moreover have \(ps, a) \. branch'\ using DisP(8) by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast next case (DisN p q a ps branch n) have \A \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a)# branch'\ using DisN(4-) by (simp add: subset_code(1)) moreover have \(\<^bold>\ (p \<^bold>\ q)) at a in (ps, a) # branch'\ using DisN(1, 5) by auto ultimately have \A \ (ps, a) # branch'\ using DisN' by fast moreover have \(ps, a) \. branch'\ using DisN(5) by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast next case (DiaP p a ps branch i n) have \finite (A \ branch_nominals branch')\ using fin by (simp add: finite_branch_nominals) then obtain j where j: \j \ A \ branch_nominals branch'\ using assms ex_new_if_finite by blast then have j': \j \ branch_nominals ((ps, a) # branch)\ using DiaP(7) unfolding branch_nominals_def by blast let ?f = \id(i := j, j := i)\ let ?branch' = \sub_branch ?f branch'\ have branch': \sub_branch ?f ?branch' = branch'\ using sub_branch_comp sub_branch_id swap_id by metis have \i \ branch_nominals ((ps, a) # branch)\ using DiaP(2) by blast then have branch: \sub_branch ?f ((ps, a) # branch) = (ps, a) # branch\ using DiaP(2) j' sub_branch_id sub_branch_upd_fresh by metis moreover have \set (sub_branch ?f ((ps, a) # branch)) \ set ?branch'\ using DiaP(7) sub_branch_image by blast ultimately have *: \set ((ps, a) # branch) \ set ?branch'\ unfolding sub_branch_def by auto have \i \ block_nominals (ps, a)\ using DiaP unfolding branch_nominals_def by simp moreover have \i \ branch_nominals ?branch'\ using j sub_branch_repl by fast ultimately have i: \i \ branch_nominals ((ps, a) # ?branch')\ unfolding branch_nominals_def by simp have \?f ` A = A\ using DiaP(2) j by auto have \A \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # ?branch'\ using DiaP(6) * by (metis (no_types, lifting) subset_code(1) insert_mono list.set(2) set_subset_Cons) moreover have \(\<^bold>\ p) at a in (ps, a) # ?branch'\ using DiaP(1, 7) * by (meson set_subset_Cons subset_code(1)) ultimately have \A \ (ps, a) # ?branch'\ using inf DiaP(2-3) fin i DiaP'' by (metis Un_iff) then have \?f ` A \ sub_branch ?f ((ps, a) # ?branch')\ - using ST_sub fin by blast + using STA_sub fin by blast then have \A \ (ps, a) # branch'\ using \?f ` A = A\ branch' branch unfolding sub_branch_def by simp moreover have \(ps, a) \. branch'\ using \set ((ps, a) # branch) \ set branch'\ by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast next case (DiaN p a ps branch i n) have \A \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch'\ using DiaN(5-) by (simp add: subset_code(1)) moreover have \(\<^bold>\ (\<^bold>\ p)) at a in (ps, a) # branch'\ \(\<^bold>\ Nom i) at a in (ps, a) # branch'\ using DiaN(1-2, 6) by auto ultimately have \A \ (ps, a) # branch'\ using DiaN' by fast moreover have \(ps, a) \. branch'\ using DiaN(6) by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast next case (SatP a p b ps branch n) have \A \ (p # ps, a) # branch'\ using SatP(4-) by (simp add: subset_code(1)) moreover have \(\<^bold>@ a p) at b in (ps, a) # branch'\ using SatP(1, 5) by auto ultimately have \A \ (ps, a) # branch'\ using SatP' by fast moreover have \(ps, a) \. branch'\ using SatP(5) by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast next case (SatN a p b ps branch n) have \A \ ((\<^bold>\ p) # ps, a) # branch'\ using SatN(4-) by (simp add: subset_code(1)) moreover have \(\<^bold>\ (\<^bold>@ a p)) at b in (ps, a) # branch'\ using SatN(1, 5) by auto ultimately have \A \ (ps, a) # branch'\ using SatN' by fast moreover have \(ps, a) \. branch'\ using SatN(5) by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast next case (GoTo i branch n) then have \A \ ([], i) # branch'\ by (simp add: subset_code(1)) moreover have \i \ branch_nominals branch'\ using GoTo(1, 4) unfolding branch_nominals_def by auto ultimately show ?case - using GoTo(2) ST.GoTo by fast + using GoTo(2) STA.GoTo by fast next case (Nom p b ps a branch n) have \A \ (p # ps, a) # branch'\ using Nom(6-) by (simp add: subset_code(1)) moreover have \p at b in (ps, a) # branch'\ using Nom(1, 7) by auto moreover have \Nom a at b in (ps, a) # branch'\ using Nom(2, 7) by auto ultimately have \A \ (ps, a) # branch'\ using Nom(3) Nom' by metis moreover have \(ps, a) \. branch'\ using Nom(7) by simp ultimately show ?case - using ST_drop_block' by fast + using STA_drop_block' by fast qed text \ If a branch has a closing tableau then we can replace the formulas of the last block on that branch with any finite superset and still obtain a closing tableau. \ -lemma ST_struct_block: +lemma STA_struct_block: fixes branch :: \('a, 'b) branch\ assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and \A, n \ (ps, a) # branch\ \set ps \ set ps'\ shows \A \ (ps', a) # branch\ using assms(3-) -proof (induct n \(ps, a) # branch\ arbitrary: ps ps' rule: ST.induct) +proof (induct n \(ps, a) # branch\ arbitrary: ps ps' rule: STA.induct) case (Close p i n ts ts') then have \p at i in (ts', a) # branch\ \(\<^bold>\ p) at i in (ts', a) # branch\ by auto then show ?case - using ST.Close by fast + using STA.Close by fast next case (Neg p ps n) then have \(\<^bold>\ \<^bold>\ p) at a in (ps', a) # branch\ by auto moreover have \A \ (p # ps', a) # branch\ using Neg(4-) by (simp add: subset_code(1)) ultimately show ?case using Neg' by fast next case (DisP p q ps n) then have \(p \<^bold>\ q) at a in (ps', a) # branch\ by auto moreover have \A \ (p # ps', a) # branch\ \A \ (q # ps', a) # branch\ using DisP(5, 7-) by (simp_all add: subset_code(1)) ultimately show ?case using DisP'' by fast next case (DisN p q ps n) then have \(\<^bold>\ (p \<^bold>\ q)) at a in (ps', a) # branch\ by auto moreover have \A \ ((\<^bold>\ q) # (\<^bold>\ p) # ps', a) # branch\ using DisN(4-) by (simp add: subset_code(1)) ultimately show ?case using DisN' by fast next case (DiaP p ps i n) have \finite (A \ branch_nominals ((ps', a) # branch))\ using fin finite_branch_nominals by blast then obtain j where j: \j \ A \ branch_nominals ((ps', a) # branch)\ using assms ex_new_if_finite by blast then have j': \j \ block_nominals (ps, a)\ using DiaP.prems unfolding branch_nominals_def by auto let ?f = \id(i := j, j := i)\ let ?ps' = \sub_list ?f ps'\ have ps': \sub_list ?f ?ps' = ps'\ using sub_list_comp sub_list_id swap_id by metis have \i \ block_nominals (ps, a)\ using DiaP(1-2) unfolding branch_nominals_def by simp then have ps: \sub_block ?f (ps, a) = (ps, a)\ using j' sub_block_id sub_block_upd_fresh by metis moreover have \set (sub_list ?f ps) \ set (sub_list ?f ps')\ using \set ps \ set ps'\ by auto ultimately have *: \set ps \ set ?ps'\ by simp have \i \ branch_nominals branch\ using DiaP unfolding branch_nominals_def by simp moreover have \j \ branch_nominals branch\ using j unfolding branch_nominals_def by simp ultimately have branch: \sub_branch ?f branch = branch\ using sub_branch_id sub_branch_upd_fresh by metis have \i \ a\ \j \ a\ using DiaP j unfolding branch_nominals_def by simp_all then have \?f a = a\ by simp moreover have \j \ block_nominals (ps', a)\ using j unfolding branch_nominals_def by simp ultimately have \i \ block_nominals (?ps', a)\ using sub_block_repl[where block=\(ps', a)\ and i=i and j=j] by simp have \?f ` A = A\ using DiaP(2) j by auto have \(\<^bold>\ p) at a in (?ps', a) # branch\ using DiaP(1) * by fastforce moreover have \A \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ?ps', a) # branch\ using * DiaP(6) fin by (simp add: subset_code(1)) moreover have \i \ A \ branch_nominals ((?ps', a) # branch)\ using DiaP(2) \i \ block_nominals (?ps', a)\ unfolding branch_nominals_def by simp ultimately have \A \ (?ps', a) # branch\ using DiaP(3) fin DiaP'' by metis then have \?f ` A \ sub_branch ?f ((?ps', a) # branch)\ - using ST_sub fin by blast + using STA_sub fin by blast then have \A \ (sub_list ?f ?ps', ?f a) # sub_branch ?f branch\ unfolding sub_branch_def using \?f ` A = A\ by simp then show ?case using \?f a = a\ ps' branch by simp next case (DiaN p ps i n) then have \(\<^bold>\ (\<^bold>\ p)) at a in (ps', a) # branch\ \(\<^bold>\ Nom i) at a in (ps', a) # branch\ by auto moreover have \A \ ((\<^bold>\ (\<^bold>@ i p)) # ps', a) # branch\ using DiaN(5-) by (simp add: subset_code(1)) ultimately show ?case using DiaN' by fast next case (SatP p b ps n) then have \(\<^bold>@ a p) at b in (ps', a) # branch\ by auto moreover have \A \ (p # ps', a) # branch\ using SatP(4-) by (simp add: subset_code(1)) ultimately show ?case using SatP' by fast next case (SatN p b ps n) then have \(\<^bold>\ (\<^bold>@ a p)) at b in (ps', a) # branch\ by auto moreover have \A \ ((\<^bold>\ p) # ps', a) # branch\ using SatN(4-) by (simp add: subset_code(1)) ultimately show ?case using SatN' by fast next case (GoTo i n ps) then have \A, Suc n \ (ps, a) # branch\ - using ST.GoTo by fast + using STA.GoTo by fast then obtain m where \A, m \ (ps, a) # (ps', a) # branch\ - using inf fin ST_struct[where branch'=\(ps, a) # _ # _\] by fastforce + using inf fin STA_struct[where branch'=\(ps, a) # _ # _\] by fastforce then have \A, Suc m \ (ps', a) # branch\ - using GoTo(4) by (simp add: ST_drop_block[where a=a]) + using GoTo(4) by (simp add: STA_drop_block[where a=a]) then show ?case by blast next case (Nom p b ps n) have \p at b in (ps', a) # branch\ using Nom(1, 7) by auto moreover have \Nom a at b in (ps', a) # branch\ using Nom(2, 7) by auto moreover have \A \ (p # ps', a) # branch\ using Nom(6-) by (simp add: subset_code(1)) ultimately show ?case using Nom(3) Nom' by metis qed section \Bridge\ text \ We define a \descendants k i branch\ relation on sets of indices. The sets are built on the index of a \\<^bold>\ Nom k\ on an \i\-block in \branch\ and can be extended by indices of formula occurrences that can be thought of as descending from that \\<^bold>\ Nom k\ by application of either the \(\<^bold>\ \<^bold>\)\ or \Nom\ rule. We show that if we have nominals \j\ and \k\ on the same block in a closeable branch, then the branch obtained by the following transformation is also closeable: For every index \v\, if the formula at \v\ is \\<^bold>\ Nom k\, replace it by \\<^bold>\ Nom j\ and if it is \\<^bold>\ (\<^bold>@ k p)\ replace it by \\<^bold>\ (\<^bold>@ j p)\. There are no other cases. From this transformation we can show admissibility of the Bridge rule under the assumption that \j\ is an allowed nominal. \ subsection \Replacing\ abbreviation bridge' :: \'b \ 'b \ ('a, 'b) fm \ ('a, 'b) fm\ where \bridge' k j p \ case p of (\<^bold>\ Nom k') \ (if k = k' then (\<^bold>\ Nom j) else (\<^bold>\ Nom k')) | (\<^bold>\ (\<^bold>@ k' q)) \ (if k = k' then (\<^bold>\ (\<^bold>@ j q)) else (\<^bold>\ (\<^bold>@ k' q))) | p \ p\ abbreviation bridge :: \'b \ 'b \ (nat \ nat) set \ nat \ nat \ ('a, 'b) fm \ ('a, 'b) fm\ where \bridge k j \ mapper (bridge' k j)\ lemma bridge_on_Nom: \Nom i on (ps, a) \ Nom i on (mapi (bridge k j xs v) ps, a)\ by (induct ps) auto lemma bridge'_nominals: \nominals (bridge' k j p) \ {k, j} = nominals p \ {k, j}\ proof (induct p) case (Neg p) then show ?case by (cases p) auto next case (Dia p) then show ?case by (cases p) auto qed auto lemma bridge_nominals: \nominals (bridge k j xs v v' p) \ {k, j} = nominals p \ {k, j}\ proof (cases \(v, v') \ xs\) case True then have \nominals (bridge k j xs v v' p) = nominals (bridge' k j p)\ by simp then show ?thesis using bridge'_nominals by metis qed simp lemma bridge_block_nominals: \block_nominals (mapi_block (bridge k j xs v) (ps, a)) \ {k, j} = block_nominals (ps, a) \ {k, j}\ proof (induct ps) case Nil then show ?case by simp next case (Cons p ps) have \?case \ (nominals (bridge k j xs v (length ps) p)) \ (block_nominals (mapi_block (bridge k j xs v) (ps, a)) \ {k, j}) = (nominals p) \ (block_nominals (ps, a) \ {k, j})\ by simp also have \\ \ (nominals (bridge k j xs v (length ps) p) \ {k, j}) \ (block_nominals (mapi_block (bridge k j xs v) (ps, a)) \ {k, j}) = (nominals p \ {k, j}) \ (block_nominals (ps, a) \ {k, j})\ by blast moreover have \nominals (bridge k j xs v (length ps) p) \ {k, j} = nominals p \ {k, j}\ using bridge_nominals by metis moreover note Cons ultimately show ?case by argo qed lemma bridge_branch_nominals: \branch_nominals (mapi_branch (bridge k j xs) branch) \ {k, j} = branch_nominals branch \ {k, j}\ proof (induct branch) case Nil then show ?case unfolding branch_nominals_def mapi_branch_def by simp next case (Cons block branch) have \?case \ (block_nominals (mapi_block (bridge k j xs (length branch)) block)) \ (branch_nominals (mapi_branch (bridge k j xs) branch) \ {k, j}) = (block_nominals block) \ (branch_nominals branch \ {k, j})\ unfolding branch_nominals_def mapi_branch_def by simp also have \\ \ (block_nominals (mapi_block (bridge k j xs (length branch)) block) \ {k, j}) \ (branch_nominals (mapi_branch (bridge k j xs) branch) \ {k, j}) = (block_nominals block \ {k, j}) \ (branch_nominals branch \ {k, j})\ by blast moreover have \block_nominals (mapi_block (bridge k j xs (length branch)) block) \ {k, j} = block_nominals block \ {k, j}\ using bridge_block_nominals[where ps=\fst block\ and a=\snd block\] by simp ultimately show ?case using Cons by argo qed lemma at_in_mapi_branch: assumes \p at a in branch\ \p \ Nom a\ shows \\v v'. f v v' p at a in mapi_branch f branch\ using assms by (meson mapi_branch_mem rev_nth_mapi_block rev_nth_on) lemma nom_at_in_bridge: fixes k j xs defines \f \ bridge k j xs\ assumes \Nom i at a in branch\ shows \Nom i at a in mapi_branch f branch\ proof - obtain qs where qs: \(qs, a) \. branch\ \Nom i on (qs, a)\ using assms(2) by blast then obtain l where \(mapi (f l) qs, a) \. mapi_branch f branch\ using mapi_branch_mem by fast moreover have \Nom i on (mapi (f l) qs, a)\ unfolding f_def using qs(2) by (induct qs) auto ultimately show ?thesis by blast qed lemma nominals_mapi_branch_bridge: assumes \Nom k at j in branch\ shows \branch_nominals (mapi_branch (bridge k j xs) branch) = branch_nominals branch\ proof - let ?f = \bridge k j xs\ have \Nom k at j in mapi_branch ?f branch\ using assms nom_at_in_bridge by fast then have \j \ branch_nominals (mapi_branch ?f branch)\ \k \ branch_nominals (mapi_branch ?f branch)\ unfolding branch_nominals_def by fastforce+ moreover have \j \ branch_nominals branch\ \k \ branch_nominals branch\ using assms unfolding branch_nominals_def by fastforce+ moreover have \branch_nominals (mapi_branch ?f branch) \ {k, j} = branch_nominals branch \ {k, j}\ using bridge_branch_nominals by metis ultimately show ?thesis by blast qed lemma bridge_proper_dia: assumes \\a. p = Nom a\ shows \bridge k j xs v v' (\<^bold>\ p) = (\<^bold>\ p)\ using assms by (induct p) simp_all lemma bridge_compl_cases: fixes k j xs v v' w w' p defines \q \ bridge k j xs v v' p\ and \q' \ bridge k j xs w w' (\<^bold>\ p)\ shows \(q = (\<^bold>\ Nom j) \ q' = (\<^bold>\ (\<^bold>\ Nom k))) \ (\r. q = (\<^bold>\ (\<^bold>@ j r)) \ q' = (\<^bold>\ \<^bold>\ (\<^bold>@ k r))) \ (\r. q = (\<^bold>@ k r) \ q' = (\<^bold>\ (\<^bold>@ j r))) \ (q = p \ q' = (\<^bold>\ p))\ proof (cases p) case (Neg p) then show ?thesis by (cases p) (simp_all add: q_def q'_def) next case (Dia p) then show ?thesis by (cases p) (simp_all add: q_def q'_def) qed (simp_all add: q_def q'_def) subsection \Descendants\ inductive descendants :: \'b \ 'b \ ('a, 'b) branch \ (nat \ nat) set \ bool\ where Initial: \branch !. v = Some (qs, i) \ qs !. v' = Some (\<^bold>\ Nom k) \ descendants k i branch {(v, v')}\ | Derived: \branch !. v = Some (qs, a) \ qs !. v' = Some (\<^bold>\ (\<^bold>@ k p)) \ descendants k i branch xs \ (w, w') \ xs \ branch !. w = Some (rs, a) \ rs !. w' = Some (\<^bold>\ Nom k) \ descendants k i branch ({(v, v')} \ xs)\ | Copied: \branch !. v = Some (qs, a) \ qs !. v' = Some p \ descendants k i branch xs \ (w, w') \ xs \ branch !. w = Some (rs, b) \ rs !. w' = Some p \ Nom a at b in branch \ descendants k i branch ({(v, v')} \ xs)\ lemma descendants_initial: assumes \descendants k i branch xs\ shows \\(v, v') \ xs. \ps. branch !. v = Some (ps, i) \ ps !. v' = Some (\<^bold>\ Nom k)\ using assms by (induct k i branch xs rule: descendants.induct) simp_all lemma descendants_bounds_fst: assumes \descendants k i branch xs\ \(v, v') \ xs\ shows \v < length branch\ using assms rev_nth_Some by (induct k i branch xs rule: descendants.induct) fast+ lemma descendants_bounds_snd: assumes \descendants k i branch xs\ \(v, v') \ xs\ \branch !. v = Some (ps, a)\ shows \v' < length ps\ using assms by (induct k i branch xs rule: descendants.induct) (auto simp: rev_nth_Some) lemma descendants_branch: \descendants k i branch xs \ descendants k i (extra @ branch) xs\ proof (induct k i branch xs rule: descendants.induct) case (Initial branch v qs i v' k) then show ?case using rev_nth_append descendants.Initial by fast next case (Derived branch v qs a v' k p i xs w w' rs) then have \(extra @ branch) !. v = Some (qs, a)\ \(extra @ branch) !. w = Some (rs, a)\ using rev_nth_append by fast+ then show ?case using Derived(2, 4-5, 7) descendants.Derived by fast next case (Copied branch v qs a v' p k i xs w w' rs b) then have \(extra @ branch) !. v = Some (qs, a)\ \(extra @ branch) !. w = Some (rs, b)\ using rev_nth_append by fast+ moreover have \Nom a at b in (extra @ branch)\ using Copied(8) by auto ultimately show ?case using Copied(2-4, 5-7) descendants.Copied by fast qed lemma descendants_block: assumes \descendants k i ((ps, a) # branch) xs\ shows \descendants k i ((ps' @ ps, a) # branch) xs\ using assms proof (induct k i \(ps, a) # branch\ xs arbitrary: ps a branch rule: descendants.induct) case (Initial v qs i v' k) have \((ps' @ ps, a) # branch) !. v = Some (qs, i) \ ((ps' @ ps, a) # branch) !. v = Some (ps' @ qs, i)\ using Initial(1) by auto moreover have \qs !. v' = Some (\<^bold>\ Nom k)\ \(ps' @ qs) !. v' = Some (\<^bold>\ Nom k)\ using Initial(2) rev_nth_append by simp_all ultimately show ?case using descendants.Initial by fast next case (Derived v qs a' v' k p i xs w w' rs) have \((ps' @ ps, a) # branch) !. v = Some (qs, a') \ ((ps' @ ps, a) # branch) !. v = Some (ps' @ qs, a')\ using Derived(1) by auto moreover have \qs !. v' = Some (\<^bold>\ (\<^bold>@ k p))\ \(ps' @ qs) !. v' = Some (\<^bold>\ (\<^bold>@ k p))\ using Derived(2) rev_nth_append by simp_all moreover have \((ps' @ ps, a) # branch) !. w = Some (rs, a') \ ((ps' @ ps, a) # branch) !. w = Some (ps' @ rs, a')\ using \((ps, a) # branch) !. w = Some (rs, a')\ by auto moreover have \rs !. w' = Some (\<^bold>\ Nom k)\ \(ps' @ rs) !. w' = Some (\<^bold>\ Nom k)\ using Derived(7) rev_nth_append by simp_all ultimately show ?case using Derived(4-5) descendants.Derived by fast next case (Copied v qs a' v' p k i xs w w' rs b) have \((ps' @ ps, a) # branch) !. v = Some (qs, a') \ ((ps' @ ps, a) # branch) !. v = Some (ps' @ qs, a')\ using Copied(1) by auto moreover have \qs !. v' = Some p\ \(ps' @ qs) !. v' = Some p\ using Copied(2) rev_nth_append by simp_all moreover have \((ps' @ ps, a) # branch) !. w = Some (rs, b) \ ((ps' @ ps, a) # branch) !. w = Some (ps' @ rs, b)\ using Copied(6) by auto moreover have \rs !. w' = Some p\ \(ps' @ rs) !. w' = Some p\ using Copied(7) rev_nth_append by simp_all moreover have \((ps' @ ps, a) # branch) !. w = Some (rs, b) \ ((ps' @ ps, a) # branch) !. w = Some (ps' @ rs, b)\ using Copied(6) by auto moreover have \rs !. w' = Some p\ \(ps' @ rs) !. w' = Some p\ using Copied(7) rev_nth_append by simp_all moreover have \Nom a' at b in (ps' @ ps, a) # branch\ using Copied(8) by fastforce ultimately show ?case using Copied(4-5) descendants.Copied[where branch=\(ps' @ ps, a) # branch\] by blast qed lemma descendants_no_head: assumes \descendants k i ((ps, a) # branch) xs\ shows \descendants k i ((p # ps, a) # branch) xs\ using assms descendants_block[where ps'=\[_]\] by simp lemma descendants_types: assumes \descendants k i branch xs\ \(v, v') \ xs\ \branch !. v = Some (ps, a)\ \ps !. v' = Some p\ shows \p = (\<^bold>\ Nom k) \ (\q. p = (\<^bold>\ (\<^bold>@ k q)))\ using assms by (induct k i branch xs arbitrary: v v' ps a) fastforce+ lemma descendants_oob_head': assumes \descendants k i ((ps, a) # branch) xs\ shows \(length branch, m + length ps) \ xs\ using assms descendants_bounds_snd by fastforce lemma descendants_oob_head: assumes \descendants k i ((ps, a) # branch) xs\ shows \(length branch, length ps) \ xs\ using assms descendants_oob_head'[where m=0] by fastforce subsection \Induction\ text \ We induct over an arbitrary set of indices. That way, we can determine in each case whether the extension gets replaced or not by manipulating the set before applying the induction hypothesis. \ -lemma ST_bridge': +lemma STA_bridge': fixes a :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and \j \ A\ \A, n \ (ps, a) # branch\ \descendants k i ((ps, a) # branch) xs\ \Nom k at j in branch\ shows \A \ mapi_branch (bridge k j xs) ((ps, a) # branch)\ using assms(4-) -proof (induct n \(ps, a) # branch\ arbitrary: ps a branch xs rule: ST.induct) +proof (induct n \(ps, a) # branch\ arbitrary: ps a branch xs rule: STA.induct) case (Close p i' n) let ?f = \bridge k j xs\ let ?branch = \mapi_branch ?f ((ps, a) # branch)\ obtain qs where qs: \(qs, i') \. (ps, a) # branch\ \p on (qs, i')\ using Close(1) by blast obtain rs where rs: \(rs, i') \. (ps, a) # branch\ \(\<^bold>\ p) on (rs, i')\ using Close(2) by blast obtain v where v: \(mapi (?f v) qs, i') \. ?branch\ using qs mapi_branch_mem by fast obtain w where w: \(mapi (?f w) rs, i') \. ?branch\ using rs mapi_branch_mem by fast have k: \Nom k at j in ?branch\ using Close(4) nom_at_in_bridge unfolding mapi_branch_def by fastforce show ?case proof (cases \\a. p = Nom a\) case True then have \p on (mapi (?f v) qs, i')\ using qs bridge_on_Nom by fast moreover have \(\<^bold>\ p) on (mapi (?f w) rs, i')\ using rs(2) True by (induct rs) auto ultimately show ?thesis - using v w ST.Close by fast + using v w STA.Close by fast next case False then obtain v' where \qs !. v' = Some p\ using qs rev_nth_on by fast then have qs': \(?f v v' p) on (mapi (?f v) qs, i')\ using rev_nth_mapi_block by fast then obtain w' where \rs !. w' = Some (\<^bold>\ p)\ using rs rev_nth_on by fast then have rs': \(?f w w' (\<^bold>\ p)) on (mapi (?f w) rs, i')\ using rev_nth_mapi_block by fast obtain q q' where q: \?f v v' p = q\ and q': \?f w w' (\<^bold>\ p) = q'\ by simp_all then consider (dia) \q = (\<^bold>\ Nom j)\ \q' = (\<^bold>\ (\<^bold>\ Nom k))\ | (satn)\\r. q = (\<^bold>\ (\<^bold>@ j r)) \ q' = (\<^bold>\ \<^bold>\ (\<^bold>@ k r))\ | (sat) \\r. q = (\<^bold>@ k r) \ q' = (\<^bold>\ (\<^bold>@ j r))\ | (old) \q = p\ \q' = (\<^bold>\ p)\ using bridge_compl_cases by fast then show ?thesis proof cases case dia then have *: \(\<^bold>\ Nom j) on (mapi (?f v) qs, i')\ \(\<^bold>\ (\<^bold>\ Nom k)) on (mapi (?f w) rs, i')\ using q qs' q' rs' by simp_all have \i' \ branch_nominals ?branch\ unfolding branch_nominals_def using v by fastforce then have ?thesis if \A \ ([], i') # ?branch\ using that GoTo by fast moreover have \(mapi (?f v) qs, i') \. ([], i') # ?branch\ using v by simp moreover have \(mapi (?f w) rs, i') \. ([], i') # ?branch\ using w by simp ultimately have ?thesis if \A \ ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ using that * by (meson DiaN') moreover have \j \ branch_nominals (([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch)\ unfolding branch_nominals_def by simp ultimately have ?thesis if \A \ ([], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ using that GoTo by fast moreover have \(\<^bold>\ (\<^bold>@ j (Nom k))) at i' in ([], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ by fastforce ultimately have ?thesis if \A \ ([\<^bold>\ Nom k], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ using that SatN' by fast moreover have \Nom k at j in ([\<^bold>\ Nom k], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ using k by fastforce moreover have \(\<^bold>\ Nom k) at j in ([\<^bold>\ Nom k], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ by fastforce ultimately show ?thesis - using ST.Close by fast + using STA.Close by fast next case satn then obtain r where *: \(\<^bold>\ (\<^bold>@ j r)) on (mapi (?f v) qs, i')\ \(\<^bold>\ \<^bold>\ (\<^bold>@ k r)) on (mapi (?f w) rs, i')\ using q qs' q' rs' by auto have \i' \ branch_nominals ?branch\ unfolding branch_nominals_def using v by fastforce then have ?thesis if \A \ ([], i') # ?branch\ using that GoTo by fast moreover have \(mapi (?f w) rs, i') \. ([], i') # ?branch\ using w by simp ultimately have ?thesis if \A \ ([\<^bold>@ k r], i') # ?branch\ using that *(2) by (meson Neg') moreover have \j \ branch_nominals (([\<^bold>@ k r], i') # ?branch)\ unfolding branch_nominals_def using k by fastforce ultimately have ?thesis if \A \ ([], j) # ([\<^bold>@ k r], i') # ?branch\ using that GoTo by fast moreover have \(\<^bold>\ (\<^bold>@ j r)) at i' in ([], j) # ([\<^bold>@ k r], i') # ?branch\ using *(1) v by auto ultimately have ?thesis if \A \ ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ using that SatN' by fast moreover have \k \ branch_nominals (([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch)\ unfolding branch_nominals_def using k by fastforce ultimately have ?thesis if \A \ ([], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ using that GoTo by fast moreover have \(\<^bold>@ k r) at i' in ([], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ by fastforce ultimately have ?thesis if \A \ ([r], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ using that SatP' by fast moreover have \Nom k at j in ([r], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ \(\<^bold>\ r) at j in ([r], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ using k by fastforce+ ultimately have ?thesis if \A \ ([\<^bold>\ r, r], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ using that by (meson Nom' fm.distinct(21) fm.simps(18)) moreover have \r at k in ([\<^bold>\ r, r], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ \(\<^bold>\ r) at k in ([\<^bold>\ r, r], k) # ([\<^bold>\ r], j) # ([\<^bold>@ k r], i') # ?branch\ by fastforce+ ultimately show ?thesis - using ST.Close by fast + using STA.Close by fast next case sat then obtain r where *: \(\<^bold>@ k r) on (mapi (?f v) qs, i')\ \(\<^bold>\ (\<^bold>@ j r)) on (mapi (?f w) rs, i')\ using q qs' q' rs' by auto have \j \ branch_nominals ?branch\ unfolding branch_nominals_def using k by fastforce then have ?thesis if \A \ ([], j) # ?branch\ using that GoTo by fast moreover have \(\<^bold>\ (\<^bold>@ j r)) at i' in ([], j) # ?branch\ using *(2) w by auto ultimately have ?thesis if \A \ ([\<^bold>\ r], j) # ?branch\ using that by (meson SatN') moreover have \k \ branch_nominals (([\<^bold>\ r], j) # ?branch)\ unfolding branch_nominals_def using k by fastforce ultimately have ?thesis if \A \ ([], k) # ([\<^bold>\ r], j) # ?branch\ using that GoTo by fast moreover have \(\<^bold>@ k r) at i' in ([], k) # ([\<^bold>\ r], j) # ?branch\ using *(1) v by auto ultimately have ?thesis if \A \ ([r], k) # ([\<^bold>\ r], j) # ?branch\ using that SatP' by fast moreover have \Nom k at j in ([r], k) # ([\<^bold>\ r], j) # ?branch\ \(\<^bold>\ r) at j in ([r], k) # ([\<^bold>\ r], j) # ?branch\ using k by fastforce+ ultimately have ?thesis if \A \ ([\<^bold>\ r, r], k) # ([\<^bold>\ r], j) # ?branch\ using that by (meson Nom' fm.distinct(21) fm.simps(18)) moreover have \r at k in ([\<^bold>\ r, r], k) # ([\<^bold>\ r], j) # ?branch\ \(\<^bold>\ r) at k in ([\<^bold>\ r, r], k) # ([\<^bold>\ r], j) # ?branch\ by fastforce+ ultimately show ?thesis - using ST.Close by fast + using STA.Close by fast next case old then have \p on (mapi (?f v) qs, i')\ \(\<^bold>\ p) on (mapi (?f w) rs, i')\ using q qs' q' rs' by simp_all then show ?thesis - using v w ST.Close[where p=p and i=i'] by fast + using v w STA.Close[where p=p and i=i'] by fast qed qed next case (Neg p a ps branch n) let ?f = \bridge k j xs\ have p: \?f l l' (\<^bold>\ \<^bold>\ p) = (\<^bold>\ \<^bold>\ p)\ for l l' by simp have \descendants k i ((p # ps, a) # branch) xs\ using Neg(5) descendants_no_head by fast then have \A \ mapi_branch ?f ((p # ps, a) # branch)\ using Neg(4-) by blast moreover have \(length branch, length ps) \ xs\ using Neg(5) descendants_oob_head by fast ultimately have \A \ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \\l l'. ?f l l' (\<^bold>\ \<^bold>\ p) at a in mapi_branch ?f ((ps, a) # branch)\ using Neg(1) at_in_mapi_branch by fast then have \(\<^bold>\ \<^bold>\ p) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using p by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using Neg' by fast then show ?case unfolding mapi_branch_def by auto next case (DisP p q a ps branch n) let ?f = \bridge k j xs\ have p: \?f l l' (p \<^bold>\ q) = (p \<^bold>\ q)\ for l l' by simp have \descendants k i ((p # ps, a) # branch) xs\ \descendants k i ((q # ps, a) # branch) xs\ using DisP(8) descendants_no_head by fast+ then have \A \ mapi_branch ?f ((p # ps, a) # branch)\ \A \ mapi_branch ?f ((q # ps, a) # branch)\ using DisP(5-) by blast+ moreover have \(length branch, length ps) \ xs\ using DisP(8) descendants_oob_head by fast ultimately have \A \ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ \A \ (q # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp_all moreover have \\l l'. ?f l l' (p \<^bold>\ q) at a in mapi_branch ?f ((ps, a) # branch)\ using DisP(1) at_in_mapi_branch by fast then have \(p \<^bold>\ q) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using p by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using DisP'' by fast then show ?case unfolding mapi_branch_def by auto next case (DisN p q a ps branch n) let ?f = \bridge k j xs\ have p: \?f l l' (\<^bold>\ (p \<^bold>\ q)) = (\<^bold>\ (p \<^bold>\ q))\ for l l' by simp have \descendants k i (((\<^bold>\ p) # ps, a) # branch) xs\ using DisN(5) descendants_no_head by fast then have \descendants k i (((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch) xs\ using descendants_no_head by fast then have \A \ mapi_branch ?f (((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch)\ using DisN(4-) by blast moreover have \(length branch, length ps) \ xs\ using DisN(5) descendants_oob_head by fast moreover have \(length branch, 1 + length ps) \ xs\ using DisN(5) descendants_oob_head' by fast ultimately have \A \ ((\<^bold>\ q) # (\<^bold>\ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \\l l'. ?f l l' (\<^bold>\ (p \<^bold>\ q)) at a in mapi_branch ?f ((ps, a) # branch)\ using DisN(1) at_in_mapi_branch by fast then have \(\<^bold>\ (p \<^bold>\ q)) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using p by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using DisN' by fast then show ?case unfolding mapi_branch_def by auto next case (DiaP p a ps branch i' n) let ?f = \bridge k j xs\ have p: \?f l l' (\<^bold>\ p) = (\<^bold>\ p)\ for l l' using DiaP(3) bridge_proper_dia by fast have \branch_nominals (mapi_branch ?f ((ps, a) # branch)) = branch_nominals ((ps, a) # branch)\ using DiaP(8-) nominals_mapi_branch_bridge[where j=j and k=k and branch=\(ps, a) # branch\] by auto then have i': \i' \ A \ branch_nominals ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)\ unfolding mapi_branch_def using DiaP(2) by simp have 1: \?f (length branch) (1 + length ps) (\<^bold>@ i' p) = (\<^bold>@ i' p)\ by simp have \i' \ k\ using DiaP(2, 8) unfolding branch_nominals_def by fastforce then have 2: \?f (length branch) (length ps) (\<^bold>\ Nom i') = (\<^bold>\ Nom i')\ by simp have \i' \ j\ using DiaP(2, 8) unfolding branch_nominals_def by fastforce moreover have \descendants k i (((\<^bold>@ i' p) # (\<^bold>\ Nom i') # ps, a) # branch) xs\ using DiaP(7) descendants_block[where ps'=\[_, _]\] by fastforce ultimately have \A \ mapi_branch ?f (((\<^bold>@ i' p) # (\<^bold>\ Nom i') # ps, a) # branch)\ using DiaP(4-) by blast then have \A \ ((\<^bold>@ i' p) # (\<^bold>\ Nom i') # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using 1 by (simp add: 2) moreover have \\l l'. ?f l l' (\<^bold>\ p) at a in mapi_branch ?f ((ps, a) # branch)\ using DiaP(1) at_in_mapi_branch by fast then have \(\<^bold>\ p) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using p by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using i' DiaP(3) fin DiaP'' by fast then show ?case unfolding mapi_branch_def by simp next case (DiaN p a ps branch i' n) have p: \bridge k j xs l l' (\<^bold>\ (\<^bold>\ p)) = (\<^bold>\ (\<^bold>\ p))\ for xs l l' by simp obtain rs where rs: \(rs, a) \. (ps, a) # branch\ \(\<^bold>\ Nom i') on (rs, a)\ using DiaN(2) by fast obtain v where v: \((ps, a) # branch) !. v = Some (rs, a)\ using rs(1) rev_nth_mem by fast obtain v' where v': \rs !. v' = Some (\<^bold>\ Nom i')\ using rs(2) rev_nth_on by fast show ?case proof (cases \(v, v') \ xs\) case True then have \i' = k\ using DiaN(6) v v' descendants_types by fast let ?xs = \{(length branch, length ps)} \ xs\ let ?f = \bridge k j ?xs\ let ?branch = \((\<^bold>\ (\<^bold>@ i' p)) # ps, a) # branch\ obtain rs' where \(((\<^bold>\ (\<^bold>@ k p)) # ps, a) # branch) !. v = Some (rs', a)\ \rs' !. v' = Some (\<^bold>\ Nom i')\ using v v' index_Cons by fast moreover have \descendants k i (((\<^bold>\ (\<^bold>@ k p)) # ps, a) # branch) xs\ using DiaN(6) descendants_block[where ps'=\[_]\] by fastforce moreover have \?branch !. length branch = Some ((\<^bold>\ (\<^bold>@ k p)) # ps, a)\ using \i' = k\ by simp moreover have \((\<^bold>\ (\<^bold>@ k p)) # ps) !. length ps = Some (\<^bold>\ (\<^bold>@ k p))\ by simp ultimately have \descendants k i (((\<^bold>\ (\<^bold>@ k p)) # ps, a) # branch) ?xs\ using True \i' = k\ Derived[where branch=\_ # branch\] by simp then have \A \ mapi_branch ?f (((\<^bold>\ (\<^bold>@ k p)) # ps, a) # branch)\ using \i' = k\ DiaN(5-) by blast then have \A \ ((\<^bold>\ (\<^bold>@ j p)) # mapi (?f (length branch)) ps, a) # mapi_branch (bridge k j ?xs) branch\ unfolding mapi_branch_def using \i' = k\ by simp moreover have \\l l'. ?f l l' (\<^bold>\ (\<^bold>\ p)) at a in mapi_branch ?f ((ps, a) # branch)\ using DiaN(1) at_in_mapi_branch by fast then have \(\<^bold>\ (\<^bold>\ p)) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using p[where xs=\?xs\] by simp moreover have \(mapi (?f v) rs, a) \. mapi_branch ?f ((ps, a) # branch)\ using v rev_nth_mapi_branch by fast then have \(mapi (?f v) rs, a) \ set ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)\ unfolding mapi_branch_def by simp moreover have \?f v v' (\<^bold>\ Nom i') on (mapi (?f v) rs, a)\ using v' rev_nth_mapi_block by fast then have \(\<^bold>\ Nom j) on (mapi (?f v) rs, a)\ using True \i' = k\ by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ by (meson DiaN') then have \A \ (mapi (bridge k j xs (length branch)) ps, a) # mapi_branch (bridge k j xs) branch\ using mapi_branch_head_add_oob[where branch=branch and ps=ps] unfolding mapi_branch_def by simp then show ?thesis unfolding mapi_branch_def by simp next case False let ?f = \bridge k j xs\ have \descendants k i (((\<^bold>\ (\<^bold>@ i' p)) # ps, a) # branch) xs\ using DiaN(6) descendants_no_head by fast then have \A \ mapi_branch ?f (((\<^bold>\ (\<^bold>@ i' p)) # ps, a) # branch)\ using DiaN(5-) by blast moreover have \(length branch, length ps) \ xs\ using DiaN(6) descendants_oob_head by fast ultimately have \A \ ((\<^bold>\ (\<^bold>@ i' p)) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \\l l'. ?f l l' (\<^bold>\ (\<^bold>\ p)) at a in mapi_branch ?f ((ps, a) # branch)\ using DiaN(1) at_in_mapi_branch by fast then have \(\<^bold>\ (\<^bold>\ p)) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using p[where xs=\xs\] by simp moreover have \(mapi (?f v) rs, a) \. mapi_branch ?f ((ps, a) # branch)\ using v rev_nth_mapi_branch by fast then have \(mapi (?f v) rs, a) \ set ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)\ unfolding mapi_branch_def by simp moreover have \?f v v' (\<^bold>\ Nom i') on (mapi (?f v) rs, a)\ using v' rev_nth_mapi_block by fast then have \(\<^bold>\ Nom i') on (mapi (?f v) rs, a)\ using False by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ by (meson DiaN') then show ?thesis unfolding mapi_branch_def by simp qed next case (SatP a p b ps branch n) let ?f = \bridge k j xs\ have p: \?f l l' (\<^bold>@ a p) = (\<^bold>@ a p)\ for l l' by simp have \descendants k i ((p # ps, a) # branch) xs\ using SatP(5) descendants_no_head by fast then have \A \ mapi_branch ?f ((p # ps, a) # branch)\ using SatP(4-) by blast moreover have \(length branch, length ps) \ xs\ using SatP(5) descendants_oob_head by fast ultimately have \A \ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \\l l'. ?f l l' (\<^bold>@ a p) at b in mapi_branch ?f ((ps, a) # branch)\ using SatP(1) at_in_mapi_branch by fast then have \(\<^bold>@ a p) at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using p by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using SatP' by fast then show ?case unfolding mapi_branch_def by simp next case (SatN a p b ps branch n) obtain qs where qs: \(qs, b) \. (ps, a) # branch\ \(\<^bold>\ (\<^bold>@ a p)) on (qs, b)\ using SatN(1) by fast obtain v where v: \((ps, a) # branch) !. v = Some (qs, b)\ using qs(1) rev_nth_mem by fast obtain v' where v': \qs !. v' = Some (\<^bold>\ (\<^bold>@ a p))\ using qs(2) rev_nth_on by fast show ?case proof (cases \(v, v') \ xs\) case True then have \a = k\ using SatN(5) v v' descendants_types by fast let ?f = \bridge k j xs\ let ?branch = \((\<^bold>\ p) # ps, a) # branch\ have p: \?f v v' (\<^bold>\ (\<^bold>@ k p)) = (\<^bold>\ (\<^bold>@ j p))\ using True by simp obtain rs' where \?branch !. v = Some (rs', b)\ \rs' !. v' = Some (\<^bold>\ (\<^bold>@ k p))\ using v v' \a = k\ index_Cons by fast have \descendants k i ?branch xs\ using SatN(5) descendants_no_head by fast then have \A \ mapi_branch ?f ?branch\ using \a = k\ SatN(4-) by blast moreover have \(length branch, length ps) \ xs\ using SatN(5) descendants_oob_head by fast ultimately have \A \ ((\<^bold>\ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using \a = k\ by simp moreover have \set (((\<^bold>\ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch) \ set (((\<^bold>\ p) # mapi (?f (length branch)) ps, a) # ([\<^bold>\ p], j) # mapi_branch ?f branch)\ by auto ultimately have *: \A \ ((\<^bold>\ p) # mapi (?f (length branch)) ps, a) # ([\<^bold>\ p], j) # mapi_branch ?f branch\ - using inf fin ST_struct by fastforce + using inf fin STA_struct by fastforce have k: \Nom k at j in mapi_branch ?f ((ps, a) # branch)\ using SatN(6) nom_at_in_bridge unfolding mapi_branch_def by fastforce have \(mapi (?f v) qs, b) \. mapi_branch ?f ((ps, a) # branch)\ using v rev_nth_mapi_branch by fast moreover have \?f v v' (\<^bold>\ (\<^bold>@ k p)) on (mapi (?f v) qs, b)\ using v' \a = k\ rev_nth_mapi_block by fast then have \(\<^bold>\ (\<^bold>@ j p)) on (mapi (?f v) qs, b)\ using p by simp ultimately have satn: \(\<^bold>\ (\<^bold>@ j p)) at b in mapi_branch ?f ((ps, a) # branch)\ by blast have \j \ branch_nominals (mapi_branch ?f ((ps, a) # branch))\ unfolding branch_nominals_def using k by fastforce then have ?thesis if \A \ ([], j) # mapi_branch ?f ((ps, a) # branch)\ using that GoTo by fast moreover have \(\<^bold>\ (\<^bold>@ j p)) at b in ([], j) # mapi_branch ?f ((ps, a) # branch)\ using satn by auto ultimately have ?thesis if \A \ ([\<^bold>\ p], j) # mapi_branch ?f ((ps, a) # branch)\ using that SatN' by fast then have ?thesis if \A \ ([\<^bold>\ p], j) # mapi_branch ?f ((ps, a) # branch)\ using that SatN' by fast then have ?thesis if \A \ ([\<^bold>\ p], j) # (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using that unfolding mapi_branch_def by simp moreover have \set ((mapi (?f (length branch)) ps, a) # ([\<^bold>\ p], j) # mapi_branch ?f branch) \ set (([\<^bold>\ p], j) # (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)\ by auto ultimately have ?thesis if \A \ (mapi (?f (length branch)) ps, a) # ([\<^bold>\ p], j) # mapi_branch ?f branch\ - using that inf fin ST_struct by blast + using that inf fin STA_struct by blast moreover have \Nom k at j in (mapi (?f (length branch)) ps, a) # ([\<^bold>\ p], j) # mapi_branch ?f branch\ using k unfolding mapi_branch_def by auto moreover have \(\<^bold>\ p) at j in (mapi (?f (length branch)) ps, a) # ([\<^bold>\ p], j) # mapi_branch ?f branch\ by fastforce ultimately have ?thesis if \A \ ((\<^bold>\ p) # mapi (?f (length branch)) ps, a) # ([\<^bold>\ p], j) # mapi_branch ?f branch\ using that \a = k\ by (meson Nom' fm.distinct(21) fm.simps(18)) then show ?thesis using * by blast next case False let ?f = \bridge k j xs\ have \descendants k i (((\<^bold>\ p) # ps, a) # branch) xs\ using SatN(5) descendants_no_head by fast then have \A \ mapi_branch (bridge k j xs) (((\<^bold>\ p) # ps, a) # branch)\ using SatN(4-) by blast moreover have \(length branch, length ps) \ xs\ using SatN(5) descendants_oob_head by fast ultimately have \A \ ((\<^bold>\ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \(mapi (?f v) qs, b) \. mapi_branch ?f ((ps, a) # branch)\ using v rev_nth_mapi_branch by fast then have \(mapi (?f v) qs, b) \ set ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)\ unfolding mapi_branch_def by simp moreover have \?f v v' (\<^bold>\ (\<^bold>@ a p)) on (mapi (?f v) qs, b)\ using v' rev_nth_mapi_block by fast then have \(\<^bold>\ (\<^bold>@ a p)) on (mapi (?f v) qs, b)\ using False by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ by (meson SatN') then show ?thesis unfolding mapi_branch_def by simp qed next case (GoTo i' n ps a branch) let ?f = \bridge k j xs\ have \descendants k i (([], i') # (ps, a) # branch) xs\ using GoTo(4) descendants_branch[where extra=\[_]\] by simp then have \A \ mapi_branch ?f (([], i') # (ps, a) # branch)\ using GoTo(3, 5-) by auto then have \A \ ([], i') # mapi_branch ?f ((ps, a) # branch)\ unfolding mapi_branch_def by simp moreover have \branch_nominals (mapi_branch ?f ((ps, a) # branch)) = branch_nominals ((ps, a) # branch)\ using GoTo(5-) nominals_mapi_branch_bridge[where j=j and k=k and branch=\(ps, a) # branch\] by auto then have \i' \ branch_nominals (mapi_branch (bridge k j xs) ((ps, a) # branch))\ using GoTo(1) by blast ultimately show ?case - using ST.GoTo by fast + using STA.GoTo by fast next case (Nom p b ps a branch n) show ?case proof (cases \\j. p = Nom j\) case True let ?f = \bridge k j xs\ have \descendants k i ((p # ps, a) # branch) xs\ using Nom(7) descendants_block[where ps'=\[p]\] by simp then have \A \ mapi_branch ?f ((p # ps, a) # branch)\ using Nom(6-) by blast moreover have \?f (length branch) (length ps) p = p\ using True by auto ultimately have \A \ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \p at b in mapi_branch ?f ((ps, a) # branch)\ using Nom(1) True nom_at_in_bridge by fast then have \p at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \Nom a at b in mapi_branch ?f ((ps, a) # branch)\ using Nom(2) True nom_at_in_bridge by fast then have \Nom a at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ by (meson Nom' Nom.hyps(3)) then show ?thesis unfolding mapi_branch_def by simp next case False obtain qs where qs: \(qs, b) \. (ps, a) # branch\ \p on (qs, b)\ using Nom(1) by blast obtain v where v: \((ps, a) # branch) !. v = Some (qs, b)\ using qs(1) rev_nth_mem by fast obtain v' where v': \qs !. v' = Some p\ using qs(2) False rev_nth_on by fast show ?thesis proof (cases \(v, v') \ xs\) case True let ?xs = \{(length branch, length ps)} \ xs\ let ?f = \bridge k j ?xs\ let ?p = \bridge' k j p\ have p: \?f v v' p = ?p\ using True by simp consider (dia) \p = (\<^bold>\ Nom k)\ | (satn) q where \p = (\<^bold>\ (\<^bold>@ k q))\ | (old) \?p = p\ by (meson Nom.prems(1) True descendants_types v v') then have A: \\i. ?p = Nom i \ ?p = (\<^bold>\ Nom i) \ i \ A\ using Nom(3) \j \ A\ by cases simp_all obtain qs' where \((p # ps, a) # branch) !. v = Some (qs', b)\ \qs' !. v' = Some p\ using v v' index_Cons by fast moreover have \Nom a at b in (p # ps, a) # branch\ using Nom(2) by fastforce moreover have \descendants k i ((p # ps, a) # branch) xs\ using Nom(7) descendants_block[where ps'=\[p]\] by simp moreover have \((p # ps, a) # branch) !. length branch = Some (p # ps, a)\ \(p # ps) !. length ps = Some p\ by simp_all ultimately have \descendants k i ((p # ps, a) # branch) ?xs\ using True Copied by fast then have \A \ mapi_branch ?f ((p # ps, a) # branch)\ using Nom(6-) by blast then have \A \ (?p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \(mapi (?f v) qs, b) \. mapi_branch ?f ((ps, a) # branch)\ using v rev_nth_mapi_branch by fast then have \(mapi (?f v) qs, b) \. (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \?f v v' p on (mapi (?f v) qs, b)\ using v v' rev_nth_mapi_block by fast then have \?p on (mapi (?f v) qs, b)\ using p by simp moreover have \Nom a at b in mapi_branch ?f ((ps, a) # branch)\ using Nom(2) nom_at_in_bridge by fast then have \Nom a at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using A by (meson Nom' Nom(3)) then have \A \ (mapi (bridge k j xs (length branch)) ps, a) # mapi_branch (bridge k j xs) branch\ using mapi_branch_head_add_oob[where branch=branch and ps=ps] unfolding mapi_branch_def by simp then show ?thesis unfolding mapi_branch_def by simp next case False let ?f = \bridge k j xs\ have \descendants k i ((p # ps, a) # branch) xs\ using Nom(7) descendants_no_head by fast then have \A \ mapi_branch ?f ((p # ps, a) # branch)\ using Nom(6-) by blast moreover have \(length branch, length ps) \ xs\ using Nom(7) descendants_oob_head by fast ultimately have \A \ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \(mapi (?f v) qs, b) \. mapi_branch ?f ((ps, a) # branch)\ using v rev_nth_mapi_branch by fast then have \(mapi (?f v) qs, b) \. (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \?f v v' p on (mapi (?f v) qs, b)\ using v v' rev_nth_mapi_block by fast then have \p on (mapi (?f v) qs, b)\ using False by simp moreover have \Nom a at b in mapi_branch ?f ((ps, a) # branch)\ using Nom(2) nom_at_in_bridge by fast then have \Nom a at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp ultimately have \A \ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ by (meson Nom' Nom(3)) then show ?thesis unfolding mapi_branch_def by simp qed qed qed -lemma ST_bridge: +lemma STA_bridge: fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \A \ branch\ \descendants k i branch xs\ \Nom k at j in branch\ \finite A\ \j \ A\ shows \A \ mapi_branch (bridge k j xs) branch\ proof - have \A \ ([], j) # branch\ - using assms(2, 5-6) inf ST_struct[where branch'=\([], j) # branch\] by auto + using assms(2, 5-6) inf STA_struct[where branch'=\([], j) # branch\] by auto moreover have \descendants k i (([], j) # branch) xs\ using assms(3) descendants_branch[where extra=\[_]\] by fastforce ultimately have \A \ mapi_branch (bridge k j xs) (([], j) # branch)\ - using ST_bridge' inf assms(3-) by fast + using STA_bridge' inf assms(3-) by fast then have *: \A \ ([], j) # mapi_branch (bridge k j xs) branch\ unfolding mapi_branch_def by simp have \branch_nominals (mapi_branch (bridge k j xs) branch) = branch_nominals branch\ using nominals_mapi_branch_bridge assms(4-) by fast moreover have \j \ branch_nominals branch\ using assms(4) unfolding branch_nominals_def by fastforce ultimately have \j \ branch_nominals (mapi_branch (bridge k j xs) branch)\ by simp then show ?thesis using * GoTo by fast qed subsection \Derivation\ theorem Bridge: fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and \j \ A\ \Nom k at j in (ps, i) # branch\ \(\<^bold>\ Nom j) at i in (ps, i) # branch\ \A \ ((\<^bold>\ Nom k) # ps, i) # branch\ shows \A \ (ps, i) # branch\ proof - let ?xs = \{(length branch, length ps)}\ have \descendants k i (((\<^bold>\ Nom k) # ps, i) # branch) ?xs\ using Initial by force moreover have \Nom k at j in ((\<^bold>\ Nom k) # ps, i) # branch\ using assms(4) by fastforce ultimately have \A \ mapi_branch (bridge k j ?xs) (((\<^bold>\ Nom k) # ps, i) # branch)\ - using ST_bridge inf fin assms(3, 6) by fast + using STA_bridge inf fin assms(3, 6) by fast then have \A \ ((\<^bold>\ Nom j) # mapi (bridge k j ?xs (length branch)) ps, i) # mapi_branch (bridge k j ?xs) branch\ unfolding mapi_branch_def by simp moreover have \mapi_branch (bridge k j {(length branch, length ps)}) branch = mapi_branch (bridge k j {}) branch\ using mapi_branch_add_oob[where xs=\{}\] by fastforce moreover have \mapi (bridge k j ?xs (length branch)) ps = mapi (bridge k j {} (length branch)) ps\ using mapi_block_add_oob[where xs=\{}\ and ps=ps] by simp ultimately have \A \ ((\<^bold>\ Nom j) # ps, i) # branch\ using mapi_block_id[where ps=ps] mapi_branch_id[where branch=branch] by simp then show ?thesis using Dup assms(5) by (metis new_def) qed section \Completeness\ subsection \Hintikka\ -abbreviation at_in' :: \('a, 'b) fm \ 'b \ ('a, 'b) block set \ bool\ - (\_ at _ in'' _\ [51, 51, 51] 50) where - \p at a in' branch \ \ps. (ps, a) \ branch \ p on (ps, a)\ +abbreviation at_in_set :: \('a, 'b) fm \ 'b \ ('a, 'b) block set \ bool\ where + \at_in_set p a S \ \ps. (ps, a) \ S \ p on (ps, a)\ + +notation at_in_set (\_ at _ in'' _\ [51, 51, 51] 50) text \ A set of blocks is Hintikka if it satisfies the following requirements. Intuitively, if it corresponds to an exhausted open branch with respect to the fixed set of allowed nominals \A\. For example, we only require symmetry, "if \j\ occurs at \i\ then \i\ occurs at \j\" if \i \ A\. \ -definition hintikka :: \'b set \ ('a, 'b) block set \ bool\ where - \hintikka A H \ - (\x i j. Nom j at i in' H \ Pro x at j in' H \ - \ (\<^bold>\ Pro x) at i in' H) \ - (\a i. Nom a at i in' H \ - \ (\<^bold>\ Nom a) at i in' H) \ - (\i j. (\<^bold>\ Nom j) at i in' H \ - \ (\<^bold>\ (\<^bold>\ Nom j)) at i in' H) \ - (\p i. i \ nominals p \ (\block \ H. p on block) \ - (\ps. (ps, i) \ H)) \ - (\i. \j. i \ A \ Nom j at i in' H \ - Nom i at j in' H) \ - (\i j k. i \ A \ k \ A \ Nom j at i in' H \ Nom k at j in' H \ - Nom k at i in' H) \ - (\i j k. j \ A \ (\<^bold>\ Nom j) at i in' H \ Nom k at j in' H \ - (\<^bold>\ Nom k) at i in' H) \ - (\i j k. j \ A \ (\<^bold>\ Nom j) at i in' H \ Nom k at i in' H \ - (\<^bold>\ Nom j) at k in' H) \ - (\p q i. (p \<^bold>\ q) at i in' H \ - p at i in' H \ q at i in' H) \ - (\p q i. (\<^bold>\ (p \<^bold>\ q)) at i in' H \ - (\<^bold>\ p) at i in' H \ (\<^bold>\ q) at i in' H) \ - (\p i. (\<^bold>\ \<^bold>\ p) at i in' H \ - p at i in' H) \ - (\p i a. (\<^bold>@ i p) at a in' H \ - p at i in' H) \ - (\p i a. (\<^bold>\ (\<^bold>@ i p)) at a in' H \ - (\<^bold>\ p) at i in' H) \ - (\p i. (\a. p = Nom a) \ (\<^bold>\ p) at i in' H \ - (\j. (\<^bold>\ Nom j) at i in' H \ (\<^bold>@ j p) at i in' H)) \ - (\p i j. (\<^bold>\ (\<^bold>\ p)) at i in' H \ (\<^bold>\ Nom j) at i in' H \ - (\<^bold>\ (\<^bold>@ j p)) at i in' H) \ - (\p i j. (\a. p = Nom a \ p = (\<^bold>\ Nom a) \ a \ A) \ p at i in' H \ Nom j at i in' H \ - p at j in' H)\ +locale Hintikka = + fixes A :: \'b set\ and H :: \('a, 'b) block set\ assumes + ProP: \Nom j at i in' H \ Pro x at j in' H \ \ (\<^bold>\ Pro x) at i in' H\ and + NomP: \Nom a at i in' H \ \ (\<^bold>\ Nom a) at i in' H\ and + NegN: \(\<^bold>\ \<^bold>\ p) at i in' H \ p at i in' H\ and + DisP: \(p \<^bold>\ q) at i in' H \ p at i in' H \ q at i in' H\ and + DisN: \(\<^bold>\ (p \<^bold>\ q)) at i in' H \ (\<^bold>\ p) at i in' H \ (\<^bold>\ q) at i in' H\ and + DiaP: \\a. p = Nom a \ (\<^bold>\ p) at i in' H \ + \j. (\<^bold>\ Nom j) at i in' H \ (\<^bold>@ j p) at i in' H\ and + DiaN: \(\<^bold>\ (\<^bold>\ p)) at i in' H \ (\<^bold>\ Nom j) at i in' H \ (\<^bold>\ (\<^bold>@ j p)) at i in' H\ and + SatP: \(\<^bold>@ i p) at a in' H \ p at i in' H\ and + SatN: \(\<^bold>\ (\<^bold>@ i p)) at a in' H \ (\<^bold>\ p) at i in' H\ and + GoTo: \i \ nominals p \ \a. p at a in' H \ \ps. (ps, i) \ H\ and + Nom: \\a. p = Nom a \ p = (\<^bold>\ Nom a) \ a \ A \ + p at i in' H \ Nom j at i in' H \ p at j in' H\ text \ Two nominals \i\ and \j\ are equivalent in respect to a Hintikka set \H\ if \H\ contains an \i\-block with \j\ on it. This is an equivalence relation on the names in \H\ intersected with the allowed nominals \A\. \ definition hequiv :: \('a, 'b) block set \ 'b \ 'b \ bool\ where \hequiv H i j \ Nom j at i in' H\ abbreviation hequiv_rel :: \'b set \ ('a, 'b) block set \ ('b \ 'b) set\ where \hequiv_rel A H \ {(i, j) |i j. hequiv H i j \ i \ A \ j \ A}\ definition names :: \('a, 'b) block set \ 'b set\ where \names H \ {i |ps i. (ps, i) \ H}\ -lemma hequiv_refl: \hintikka A H \ i \ names H \ hequiv H i i\ - unfolding hintikka_def hequiv_def names_def by simp - -lemma hequiv_refl': \hintikka A H \ (ps, i) \ H \ hequiv H i i\ - using hequiv_refl unfolding names_def by fast - -lemma hequiv_sym': \hintikka A H \ i \ A \ hequiv H i j \ hequiv H j i\ - unfolding hintikka_def hequiv_def by meson - -lemma hequiv_sym: \hintikka A H \ i \ A \ j \ A \ hequiv H i j \ hequiv H j i\ - unfolding hintikka_def hequiv_def by meson +lemma hequiv_refl: \i \ names H \ hequiv H i i\ + unfolding hequiv_def names_def by simp + +lemma hequiv_refl': \(ps, i) \ H \ hequiv H i i\ + using hequiv_refl unfolding names_def by fastforce + +lemma hequiv_sym': + assumes \Hintikka A H\ \i \ A\ \hequiv H i j\ + shows \hequiv H j i\ +proof - + have \i \ A \ Nom i at i in' H \ Nom j at i in' H \ Nom i at j in' H\ for i j + using assms(1) Hintikka.Nom by fast + then show ?thesis + using assms(2-) unfolding hequiv_def by auto +qed + +lemma hequiv_sym: \Hintikka A H \ i \ A \ j \ A \ hequiv H i j \ hequiv H j i\ + by (meson hequiv_sym') lemma hequiv_trans: - \hintikka A H \ i \ A \ k \ A \ hequiv H i j \ hequiv H j k \ hequiv H i k\ - unfolding hintikka_def hequiv_def by simp + assumes \Hintikka A H\ \i \ A\ \k \ A\ \hequiv H i j\ \hequiv H j k\ + shows \hequiv H i k\ +proof - + have \hequiv H j i\ + by (meson assms(1-2, 4) hequiv_sym') + moreover have \k \ A \ Nom k at j in' H \ Nom i at j in' H \ Nom k at i in' H\ for i k j + using assms(1) Hintikka.Nom by fast + ultimately show ?thesis + using assms(3-) unfolding hequiv_def by blast +qed lemma hequiv_names: \hequiv H i j \ i \ names H\ unfolding hequiv_def names_def by blast lemma hequiv_names_rel: - assumes \hintikka A H\ + assumes \Hintikka A H\ shows \hequiv_rel A H \ names H \ names H\ using assms hequiv_names hequiv_sym by fast lemma hequiv_refl_rel: - assumes \hintikka A H\ + assumes \Hintikka A H\ shows \refl_on (names H \ A) (hequiv_rel A H)\ unfolding refl_on_def using assms hequiv_refl hequiv_names_rel by fast -lemma hequiv_sym_rel: \hintikka A H \ sym (hequiv_rel A H)\ +lemma hequiv_sym_rel: \Hintikka A H \ sym (hequiv_rel A H)\ unfolding sym_def using hequiv_sym by fast -lemma hequiv_trans_rel: \hintikka B A \ trans (hequiv_rel B A)\ +lemma hequiv_trans_rel: \Hintikka B A \ trans (hequiv_rel B A)\ unfolding trans_def using hequiv_trans by fast -lemma hequiv_rel: \hintikka A H \ equiv (names H \ A) (hequiv_rel A H)\ +lemma hequiv_rel: \Hintikka A H \ equiv (names H \ A) (hequiv_rel A H)\ using hequiv_refl_rel hequiv_sym_rel hequiv_trans_rel by (rule equivI) lemma nominal_in_names: - assumes \hintikka A H\ \\block \ H. i \ block_nominals block\ + assumes \Hintikka A H\ \\block \ H. i \ block_nominals block\ shows \i \ names H\ -proof - - have \(\p. i \ nominals p \ (\block \ H. p on block) \ (\br. (br, i) \ H))\ - using \hintikka A H\ unfolding hintikka_def by meson - then show ?thesis - unfolding names_def using assms(2) by fastforce -qed + using assms Hintikka.GoTo unfolding names_def by fastforce subsubsection \Named model\ text \ Given a Hintikka set \H\, a formula \p\ on a block in \H\ and a set of allowed nominals \A\ which contains all "root-like" nominals in \p\ we construct a model that satisfies \p\. The worlds of our model are sets of equivalent nominals and nominals are assigned to the equivalence class of an equivalent allowed nominal. This definition resembles the "ur-father" notion. From a world \is\, we can reach a world \js\ iff there is an \i \ is\ and a \j \ js\ s.t. there is an \i\-block in \H\ with \\<^bold>\ Nom j\ on it. A propositional symbol \p\ is true in a world \is\ if there exists an \i \ is\ s.t. \p\ occurs on an \i\-block in \H\. \ definition assign :: \'b set \ ('a, 'b) block set \ 'b \ 'b set\ where \assign A H i \ if \a. a \ A \ Nom a at i in' H then proj (hequiv_rel A H) (SOME a. a \ A \ Nom a at i in' H) else {i}\ definition reach :: \'b set \ ('a, 'b) block set \ 'b set \ 'b set set\ where \reach A H is \ {assign A H j |i j. i \ is \ (\<^bold>\ Nom j) at i in' H}\ definition val :: \('a, 'b) block set \ 'b set \ 'a \ bool\ where \val H is x \ \i \ is. Pro x at i in' H\ +lemma ex_assignment: + assumes \Hintikka A H\ + shows \assign A H i \ {}\ +proof (cases \\b. b \ A \ Nom b at i in' H\) + case True + let ?b = \SOME b. b \ A \ Nom b at i in' H\ + have *: \?b \ A \ Nom ?b at i in' H\ + using someI_ex True . + moreover from this have \hequiv H ?b ?b\ + using assms block_nominals nominal_in_names hequiv_refl + by (metis (no_types, lifting) nominals.simps(2) singletonI) + ultimately show ?thesis + unfolding assign_def proj_def by auto +next + case False + then show ?thesis + unfolding assign_def by auto +qed + lemma ur_closure: - assumes \hintikka A H\ \p at i in' H\ \\a. p = Nom a \ p = (\<^bold>\ Nom a) \ a \ A\ - shows \\a \ assign A H i. p at a in' H\ + assumes \Hintikka A H\ \p at i in' H\ \\a. p = Nom a \ p = (\<^bold>\ Nom a) \ a \ A\ + shows \\a \ assign A H i. p at a in' H\ proof (cases \\b. b \ A \ Nom b at i in' H\) case True let ?b = \SOME b. b \ A \ Nom b at i in' H\ have *: \?b \ A \ Nom ?b at i in' H\ using someI_ex True . then have \p at ?b in' H\ - using assms unfolding hintikka_def by blast + using assms by (meson Hintikka.Nom) + then have \p at a in' H\ if \hequiv H ?b a\ for a + using that assms(1, 3) unfolding hequiv_def by (meson Hintikka.Nom) moreover have \assign A H i = proj (hequiv_rel A H) ?b\ unfolding assign_def using True by simp ultimately show ?thesis - unfolding proj_def using * assms(1) hequiv_refl' by fast + unfolding proj_def by blast next case False then show ?thesis unfolding assign_def using assms by auto qed +lemma ur_closure': + assumes \Hintikka A H\ \p at i in' H\ \\a. p = Nom a \ p = (\<^bold>\ Nom a) \ a \ A\ + shows \\a \ assign A H i. p at a in' H\ +proof - + obtain a where \a \ assign A H i\ + using assms(1) ex_assignment by fast + then show ?thesis + using assms ur_closure[where i=i] by blast +qed + lemma mem_hequiv_rel: \a \ proj (hequiv_rel A H) b \ a \ A\ unfolding proj_def by blast -lemma assign_hequiv: - assumes \hintikka A H\ \a \ assign A H i\ \i \ A\ \i \ names H\ - shows \hequiv H a i\ -proof (cases \\b. b \ A \ Nom b at i in' H\) - case True - let ?b = \SOME b. b \ A \ Nom b at i in' H\ - have *: \?b \ A \ Nom ?b at i in' H\ - using someI_ex True . - then have \hequiv H i ?b\ - unfolding hequiv_def by simp - then have \hequiv H ?b i\ - using hequiv_sym' assms(1, 3) by fast - - moreover have \assign A H i = proj (hequiv_rel A H) ?b\ - unfolding assign_def using True by simp - then have \a \ proj (hequiv_rel A H) ?b\ - using assms(2) by simp - then have \hequiv H ?b a\ - unfolding proj_def by fast - then have \hequiv H a ?b\ - using assms(1) * hequiv_sym' by fast - - moreover have \a \ A\ - using assms(2) \assign A H i = proj (hequiv_rel A H) ?b\ - unfolding proj_def by fast - - ultimately show ?thesis - using assms(1, 3) hequiv_trans by fast -next - case False - then have \assign A H i = {i}\ - unfolding assign_def by auto - then have \a = i\ - using assms(2) by simp - then show ?thesis - using assms(1, 4) hequiv_refl by fast -qed - lemma hequiv_proj: - assumes \hintikka A H\ + assumes \Hintikka A H\ \Nom a at i in' H\ \a \ A\ \Nom b at i in' H\ \b \ A\ shows \proj (hequiv_rel A H) a = proj (hequiv_rel A H) b\ proof - have \equiv (names H \ A) (hequiv_rel A H)\ using assms(1) hequiv_rel by fast moreover have \{a, b} \ names H \ A\ using assms(1-5) nominal_in_names by fastforce moreover have \Nom b at a in' H\ - using assms(1-2, 4-5) unfolding hintikka_def by blast + using assms(1-2, 4-5) Hintikka.Nom by fast then have \hequiv H a b\ unfolding hequiv_def by simp ultimately show ?thesis by (simp add: proj_iff) qed lemma hequiv_proj_opening: - assumes \hintikka A H\ \Nom a at i in' H\ \a \ A\ \i \ A\ + assumes \Hintikka A H\ \Nom a at i in' H\ \a \ A\ \i \ A\ shows \proj (hequiv_rel A H) a = proj (hequiv_rel A H) i\ using hequiv_proj assms by fastforce lemma assign_proj_refl: - assumes \hintikka A H\ \Nom i at i in' H\ \i \ A\ + assumes \Hintikka A H\ \Nom i at i in' H\ \i \ A\ shows \assign A H i = proj (hequiv_rel A H) i\ proof - let ?a = \SOME a. a \ A \ Nom a at i in' H\ have \\a. a \ A \ Nom a at i in' H\ using assms(2-3) by fast with someI_ex have *: \?a \ A \ Nom ?a at i in' H\ . then have \assign A H i = proj (hequiv_rel A H) ?a\ unfolding assign_def by auto then show ?thesis unfolding assign_def using hequiv_proj * assms by fast qed lemma assign_named: - assumes \hintikka A H\ \i \ proj (hequiv_rel A H) a\ + assumes \Hintikka A H\ \i \ proj (hequiv_rel A H) a\ shows \i \ names H\ using assms unfolding proj_def by simp (meson hequiv_names hequiv_sym') lemma assign_unique: - assumes \hintikka A H\ \a \ assign A H i\ + assumes \Hintikka A H\ \a \ assign A H i\ shows \assign A H a = assign A H i\ proof (cases \\b. b \ A \ Nom b at i in' H\) case True let ?b = \SOME b. b \ A \ Nom b at i in' H\ have *: \?b \ A \ Nom ?b at i in' H\ using someI_ex True . have **: \assign A H i = proj (hequiv_rel A H) ?b\ unfolding assign_def using True by simp moreover from this have \Nom a at a in' H\ using assms assign_named unfolding names_def by fastforce ultimately have \assign A H a = proj (hequiv_rel A H) a\ using assms assign_proj_refl mem_hequiv_rel by fast with ** show ?thesis unfolding proj_def using assms by simp (meson hequiv_sym' hequiv_trans) next case False then have \assign A H i = {i}\ unfolding assign_def by auto then have \a = i\ using assms(2) by simp then show ?thesis by simp qed lemma assign_val: assumes - \hintikka A H\ \Pro x at a in' H\ \(\<^bold>\ Pro x) at i in' H\ + \Hintikka A H\ \Pro x at a in' H\ \(\<^bold>\ Pro x) at i in' H\ \a \ assign A H i\ \i \ names H\ shows False -proof (cases \\b. b \ A \ Nom b at i in' H\) - case True - let ?b = \SOME b. b \ A \ Nom b at i in' H\ - have *: \?b \ A \ Nom ?b at i in' H\ - using someI_ex True . - then have \hequiv H i ?b\ - unfolding hequiv_def by simp - then have \\ Pro x at ?b in' H\ - using assms(3, 1) unfolding hintikka_def hequiv_def by meson - - moreover have \assign A H i = proj (hequiv_rel A H) ?b\ - unfolding assign_def using True by simp - then have \a \ proj (hequiv_rel A H) ?b\ - using assms(4) by simp - then have \hequiv H ?b a\ - unfolding proj_def by fast - then have \hequiv H a ?b\ - using assms(1) * hequiv_sym' by fast - then have \Pro x at ?b in' H\ - using assms(1, 2) unfolding hintikka_def hequiv_def by blast - - ultimately show ?thesis - by blast -next - case False - then have \assign A H i = {i}\ - unfolding assign_def by auto - then have \a = i\ - using assms(4) by simp - then have \Pro x at i in' H\ - using assms(2) by fast - moreover have \hequiv H i i\ - using assms(1, 5) hequiv_refl by fast - ultimately have \\ (\<^bold>\ Pro x) at i in' H\ - using assms(1) unfolding hintikka_def hequiv_def by meson - then show ?thesis - using assms(3) by fast -qed - -lemma ur_closure_existing: - assumes \hintikka A H\ \p at i in' H\ \\a. p = Nom a \ p = (\<^bold>\ Nom a) \ a \ A\ - \a \ assign A H i\ - shows \p at a in' H\ -proof (cases \\b. b \ A \ Nom b at i in' H\) - case True - let ?b = \SOME b. b \ A \ Nom b at i in' H\ - have *: \?b \ A \ Nom ?b at i in' H\ - using someI_ex True . - then have \p at ?b in' H\ - using assms(1-3) unfolding hintikka_def by blast - moreover have \assign A H i = proj (hequiv_rel A H) ?b\ - unfolding assign_def using True by simp - then have \a \ proj (hequiv_rel A H) ?b\ - using assms(4) by simp - then have \Nom a at ?b in' H\ - unfolding proj_def hequiv_def by simp - ultimately show ?thesis - using assms(1, 3) unfolding hintikka_def by blast -next - case False - then have \assign A H i = {i}\ - unfolding assign_def by auto - then have \a = i\ - using assms(4) by simp - then show ?thesis - using assms(2) by simp -qed - -text \ - The allowed set \A\ is well-formed with respect to \p\ if all right nominals in \p\ are in \A\ - as well as any that appear in "proper" formulas. -\ - -definition wf_allowed :: \'b set \ ('a, 'b) block set \ ('a, 'b) fm \ bool\ where - \wf_allowed A H p \ \i \ nominals p. - (\a. Nom i at a in' H \ i \ a \ i \ A) \ - (\a p. p at a in' H \ i \ nominals p \ p \ Nom i \ p \ (\<^bold>\ Nom i) \ i \ A)\ - -lemma hintikka_model: - assumes \hintikka A H\ + using assms Hintikka.ProP ur_closure by fastforce + +lemma Hintikka_model: + assumes \Hintikka A H\ shows - \p at i in' H \ wf_allowed A H p \ \a. p = (\<^bold>\ Nom a) \ a \ A \ + \p at i in' H \ nominals p \ A \ Model (reach A H) (val H), assign A H, assign A H i \ p\ - \(\<^bold>\ p) at i in' H \ wf_allowed A H p \ + \(\<^bold>\ p) at i in' H \ nominals p \ A \ \ Model (reach A H) (val H), assign A H, assign A H i \ p\ proof (induct p arbitrary: i) fix i case (Pro x) assume \Pro x at i in' H\ then show \Model (reach A H) (val H), assign A H, assign A H i \ Pro x\ - using assms(1) ur_closure unfolding val_def by fastforce + using assms(1) ur_closure' unfolding val_def by fastforce next fix i case (Pro x) assume \(\<^bold>\ Pro x) at i in' H\ then have \\a. a \ assign A H i \ Pro x at a in' H\ using assms(1) assign_val unfolding names_def by fast then have \\ val H (assign A H i) x\ unfolding proj_def val_def hequiv_def by simp then show \\ Model (reach A H) (val H), assign A H, assign A H i \ Pro x\ by simp next fix i case (Nom a) - assume *: \Nom a at i in' H\ \wf_allowed A H (Nom a)\ + assume *: \Nom a at i in' H\ \nominals (Nom a) \ A\ let ?b = \SOME b. b \ A \ Nom b at i in' H\ let ?c = \SOME b. b \ A \ Nom b at a in' H\ - have \assign A H i = assign A H a\ - proof (cases \a = i\) - case False - then have \a \ A\ - using * unfolding wf_allowed_def by auto - then have \\b. b \ A \ Nom b at i in' H\ - using * by fast - with someI_ex have b: \?b \ A \ Nom ?b at i in' H\ . - then have \assign A H i = proj (hequiv_rel A H) ?b\ - unfolding assign_def by auto - also have \proj (hequiv_rel A H) ?b = proj (hequiv_rel A H) a\ - using hequiv_proj assms(1) b * \a \ A\ by fast - - also have \Nom a at a in' H\ - using * \a \ A\ assms(1) unfolding hintikka_def by blast - then have \\c. c \ A \ Nom c at a in' H\ - using \a \ A\ by blast - with someI_ex have c: \?c \ A \ Nom ?c at a in' H\ . - then have \assign A H a = proj (hequiv_rel A H) ?c\ - unfolding assign_def by auto - then have \proj (hequiv_rel A H) a = assign A H a\ - using hequiv_proj_opening assms(1) \a \ A\ c by fast - - finally show ?thesis . - qed simp + have \a \ A\ + using *(2) by simp + then have \\b. b \ A \ Nom b at i in' H\ + using * by fast + with someI_ex have b: \?b \ A \ Nom ?b at i in' H\ . + then have \assign A H i = proj (hequiv_rel A H) ?b\ + unfolding assign_def by auto + also have \proj (hequiv_rel A H) ?b = proj (hequiv_rel A H) a\ + using hequiv_proj assms(1) b * \a \ A\ by fast + + also have \Nom a at a in' H\ + using * \a \ A\ assms(1) Hintikka.Nom by fast + then have \\c. c \ A \ Nom c at a in' H\ + using \a \ A\ by blast + with someI_ex have c: \?c \ A \ Nom ?c at a in' H\ . + then have \assign A H a = proj (hequiv_rel A H) ?c\ + unfolding assign_def by auto + then have \proj (hequiv_rel A H) a = assign A H a\ + using hequiv_proj_opening assms(1) \a \ A\ c by fast + + finally have \assign A H i = assign A H a\ . then show \Model (reach A H) (val H), assign A H, assign A H i \ Nom a\ by simp next fix i case (Nom a) - assume *: \(\<^bold>\ Nom a) at i in' H\ \wf_allowed A H (Nom a)\ + assume *: \(\<^bold>\ Nom a) at i in' H\ \nominals (Nom a) \ A\ then have \a \ A\ - unfolding wf_allowed_def by fastforce + by simp have \hequiv H a a\ using hequiv_refl * nominal_in_names assms(1) by fastforce obtain j where j: \j \ assign A H i\ \(\<^bold>\ Nom a) at j in' H\ - using ur_closure assms(1) * by fastforce + using ur_closure' assms(1) * by fastforce then have \\ Nom a at j in' H\ - using assms(1) unfolding hintikka_def by meson - - moreover have \Nom a at b in' H\ if \hequiv H a b\ for b - using that assms(1) \a \ A\ unfolding hintikka_def hequiv_def by meson - then have \\b \ assign A H a. Nom a at b in' H\ - using assign_hequiv \a \ A\ assms(1) \hequiv H a a\ assign_hequiv hequiv_names - unfolding hequiv_def by metis + using assms(1) Hintikka.NomP by fast + + moreover have \\b \ assign A H a. Nom a at b in' H\ + using assms \a \ A\ \hequiv H a a\ ur_closure unfolding hequiv_def by fast ultimately have \assign A H a \ assign A H i\ using j by blast then show \\ Model (reach A H) (val H), assign A H, assign A H i \ Nom a\ by simp next fix i case (Neg p) - moreover assume \(\<^bold>\ p) at i in' H\ - moreover assume \wf_allowed A H (\<^bold>\ p)\ - then have \wf_allowed A H p\ - unfolding wf_allowed_def by simp + moreover assume \(\<^bold>\ p) at i in' H\ \nominals (\<^bold>\ p) \ A\ ultimately show \Model (reach A H) (val H), assign A H, assign A H i \ \<^bold>\ p\ by simp next fix i case (Neg p) moreover assume *: \(\<^bold>\ \<^bold>\ p) at i in' H\ then have \p at i in' H\ - using assms(1) unfolding hintikka_def by meson - moreover assume wf: \wf_allowed A H (\<^bold>\ p)\ - then have \wf_allowed A H p\ - unfolding wf_allowed_def by simp - moreover from * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ - using wf unfolding wf_allowed_def by fastforce + using assms(1) Hintikka.NegN by fast + moreover assume \nominals (\<^bold>\ p) \ A\ + moreover from this * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ + by auto ultimately show \\ Model (reach A H) (val H), assign A H, assign A H i \ \<^bold>\ p\ using assms(1) by auto next fix i case (Dis p q) moreover assume *: \(p \<^bold>\ q) at i in' H\ then have \p at i in' H \ q at i in' H\ - using assms(1) unfolding hintikka_def by meson - moreover assume wf: \wf_allowed A H (p \<^bold>\ q)\ - then have \wf_allowed A H p\ \wf_allowed A H q\ - unfolding wf_allowed_def by simp_all - moreover from * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ \\a. q = (\<^bold>\ Nom a) \ a \ A\ - using wf unfolding wf_allowed_def by fastforce+ + using assms(1) Hintikka.DisP by fast + moreover assume \nominals (p \<^bold>\ q) \ A\ + moreover from this * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ \\a. q = (\<^bold>\ Nom a) \ a \ A\ + by auto ultimately show \Model (reach A H) (val H), assign A H, assign A H i \ (p \<^bold>\ q)\ - by (metis semantics.simps(4)) + by simp metis next fix i case (Dis p q) moreover assume *: \(\<^bold>\ (p \<^bold>\ q)) at i in' H\ then have \(\<^bold>\ p) at i in' H\ \(\<^bold>\ q) at i in' H\ - using assms(1) unfolding hintikka_def by meson+ - moreover assume wf: \wf_allowed A H (p \<^bold>\ q)\ - then have \wf_allowed A H p\ \wf_allowed A H q\ - unfolding wf_allowed_def by simp_all - moreover from * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ \\a. q = (\<^bold>\ Nom a) \ a \ A\ - using wf unfolding wf_allowed_def by fastforce+ + using assms(1) Hintikka.DisN by fast+ + moreover assume \nominals (p \<^bold>\ q) \ A\ + moreover from this * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ \\a. q = (\<^bold>\ Nom a) \ a \ A\ + by auto ultimately show \\ Model (reach A H) (val H), assign A H, assign A H i \ (p \<^bold>\ q)\ by auto next fix i case (Dia p) - assume *: \(\<^bold>\ p) at i in' H\ \\a. (\<^bold>\ p) = (\<^bold>\ Nom a) \ a \ A\ - assume wf: \wf_allowed A H (\<^bold>\ p)\ - then have wfp: \wf_allowed A H p\ - unfolding wf_allowed_def by simp - from * have p: \\a. p = (\<^bold>\ Nom a) \ a \ A\ - using wf unfolding wf_allowed_def by fastforce + assume *: \(\<^bold>\ p) at i in' H\ \nominals (\<^bold>\ p) \ A\ + with * have p: \\a. p = (\<^bold>\ Nom a) \ a \ A\ + by auto show \Model (reach A H) (val H), assign A H, assign A H i \ \<^bold>\ p\ proof (cases \\j. p = Nom j\) case True then obtain j where j: \p = Nom j\ \j \ A\ - using * by blast + using *(2) by auto then obtain a where a: \a \ assign A H i\ \(\<^bold>\ Nom j) at a in' H\ - using ur_closure assms(1) \(\<^bold>\ p) at i in' H\ by fast + using ur_closure' assms(1) \(\<^bold>\ p) at i in' H\ by fast from j have \(\<^bold>\ Nom j) at i in' H\ - using assms(1) *(1) unfolding hintikka_def by meson + using *(1) by simp then have \(\<^bold>\ Nom j) at a in' H\ - using ur_closure_existing assms(1) a(2) by fast + using ur_closure assms(1) a(2) by fast then have \assign A H j \ reach A H (assign A H i)\ unfolding reach_def using a(1) by fast then show ?thesis using j(1) by simp next case False then obtain a where a: \a \ assign A H i\ \(\<^bold>\ p) at a in' H\ - using ur_closure assms(1) \(\<^bold>\ p) at i in' H\ by fast + using ur_closure' assms(1) \(\<^bold>\ p) at i in' H\ by fast then have \\j. (\<^bold>\ Nom j) at a in' H \ (\<^bold>@ j p) at a in' H\ - using False assms \(\<^bold>\ p) at i in' H\ unfolding hintikka_def by blast + using False assms \(\<^bold>\ p) at i in' H\ by (meson Hintikka.DiaP) then obtain j where j: \(\<^bold>\ Nom j) at a in' H\ \(\<^bold>@ j p) at a in' H\ by blast from j(2) have \p at j in' H\ - using assms(1) unfolding hintikka_def by blast + using assms(1) Hintikka.SatP by fast then have \Model (reach A H) (val H), assign A H, assign A H j \ p\ - using Dia wfp p by simp + using Dia p *(2) by simp moreover have \assign A H j \ reach A H (assign A H i)\ unfolding reach_def using a(1) j(1) by blast ultimately show ?thesis by auto qed next fix i case (Dia p) - assume *: \(\<^bold>\ (\<^bold>\ p)) at i in' H\ + assume *: \(\<^bold>\ (\<^bold>\ p)) at i in' H\ \nominals (\<^bold>\ p) \ A\ then obtain a where a: \a \ assign A H i\ \(\<^bold>\ (\<^bold>\ p)) at a in' H\ - using ur_closure assms(1) by fast - assume wf: \wf_allowed A H (\<^bold>\ p)\ - then have wfp: \wf_allowed A H p\ - unfolding wf_allowed_def by simp - moreover from * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ - using wf unfolding wf_allowed_def by fastforce + using ur_closure' assms(1) by fast { fix j b - assume *: \(\<^bold>\ Nom j) at b in' H\ \b \ assign A H a\ + assume \(\<^bold>\ Nom j) at b in' H\ \b \ assign A H a\ moreover have \(\<^bold>\ (\<^bold>\ p)) at b in' H\ - using a(2) assms(1) calculation(2) ur_closure_existing by fast + using a(2) assms(1) calculation(2) ur_closure by fast ultimately have \(\<^bold>\ (\<^bold>@ j p)) at b in' H\ - using assms(1) unfolding hintikka_def by blast + using assms(1) Hintikka.DiaN by fast then have \(\<^bold>\ p) at j in' H\ - using assms(1) unfolding hintikka_def by blast + using assms(1) Hintikka.SatN by fast then have \\ Model (reach A H) (val H), assign A H, assign A H j \ p\ - using Dia wfp by fast + using Dia *(2) by simp } then have \\ Model (reach A H) (val H), assign A H, assign A H a \ \<^bold>\ p\ unfolding reach_def by auto moreover have \assign A H a = assign A H i\ using assms(1) a assign_unique by fast ultimately show \\ Model (reach A H) (val H), assign A H, assign A H i \ \<^bold>\ p\ by simp next fix i case (Sat j p) - assume *: \(\<^bold>@ j p) at i in' H\ - moreover assume wf: \wf_allowed A H (\<^bold>@ j p)\ - then have \wf_allowed A H p\ - unfolding wf_allowed_def by simp_all - moreover from * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ - using wf unfolding wf_allowed_def by fastforce + assume \(\<^bold>@ j p) at i in' H\ \nominals (\<^bold>@ j p) \ A\ + moreover from this have \\a. p = (\<^bold>\ Nom a) \ a \ A\ + by auto moreover have \p at j in' H\ if \\a. (\<^bold>@ j p) at a in' H\ - using that assms(1) unfolding hintikka_def by meson + using that assms(1) Hintikka.SatP by fast ultimately show \Model (reach A H) (val H), assign A H, assign A H i \ \<^bold>@ j p\ using Sat by auto next fix i case (Sat j p) - assume *: \(\<^bold>\ (\<^bold>@ j p)) at i in' H\ - moreover assume wf: \wf_allowed A H (\<^bold>@ j p)\ - then have \wf_allowed A H p\ - unfolding wf_allowed_def by simp_all - moreover from * have \\a. p = (\<^bold>\ Nom a) \ a \ A\ - using wf unfolding wf_allowed_def by fastforce + assume \(\<^bold>\ (\<^bold>@ j p)) at i in' H\ \nominals (\<^bold>@ j p) \ A\ + moreover from this have \\a. p = (\<^bold>\ Nom a) \ a \ A\ + by auto moreover have \(\<^bold>\ p) at j in' H\ if \\a. (\<^bold>\ (\<^bold>@ j p)) at a in' H\ - using that assms(1) unfolding hintikka_def by meson + using that assms(1) Hintikka.SatN by fast ultimately show \\ Model (reach A H) (val H), assign A H, assign A H i \ \<^bold>@ j p\ using Sat by fastforce qed subsection \Lindenbaum-Henkin\ text \ A set of blocks is consistent if no finite subset can be derived. Given a consistent set of blocks we are going to extend it to be saturated and maximally consistent and show that is then Hintikka. All definitions are with respect to the set of allowed nominals. \ definition consistent :: \'b set \ ('a, 'b) block set \ bool\ where \consistent A S \ \S'. set S' \ S \ A \ S'\ instance fm :: (countable, countable) countable by countable_datatype definition proper_dia :: \('a, 'b) fm \ ('a, 'b) fm option\ where \proper_dia p \ case p of (\<^bold>\ p) \ (if \a. p = Nom a then Some p else None) | _ \ None\ lemma proper_dia: \proper_dia p = Some q \ p = (\<^bold>\ q) \ (\a. q = Nom a)\ unfolding proper_dia_def by (cases p) (simp_all, metis option.discI option.inject) text \The following function witnesses each \\<^bold>\ p\ in a fresh world.\ primrec witness_list :: \('a, 'b) fm list \ 'b set \ ('a, 'b) fm list\ where \witness_list [] _ = []\ | \witness_list (p # ps) used = (case proper_dia p of None \ witness_list ps used | Some q \ let i = SOME i. i \ used in (\<^bold>@ i q) # (\<^bold>\ Nom i) # witness_list ps ({i} \ used))\ primrec witness :: \('a, 'b) block \ 'b set \ ('a, 'b) block\ where \witness (ps, a) used = (witness_list ps used, a)\ lemma witness_list: \proper_dia p = Some q \ witness_list (p # ps) used = (let i = SOME i. i \ used in (\<^bold>@ i q) # (\<^bold>\ Nom i) # witness_list ps ({i} \ used))\ by simp primrec extend :: \'b set \ ('a, 'b) block set \ (nat \ ('a, 'b) block) \ nat \ ('a, 'b) block set\ where \extend A S f 0 = S\ | \extend A S f (Suc n) = (if \ consistent A ({f n} \ extend A S f n) then extend A S f n else let used = A \ (\block \ {f n} \ extend A S f n. block_nominals block) in {f n, witness (f n) used} \ extend A S f n)\ definition Extend :: \'b set \ ('a, 'b) block set \ (nat \ ('a, 'b) block) \ ('a, 'b) block set\ where \Extend A S f \ (\n. extend A S f n)\ lemma extend_chain: \extend A S f n \ extend A S f (Suc n)\ by auto lemma extend_mem: \S \ extend A S f n\ by (induct n) auto lemma Extend_mem: \S \ Extend A S f\ unfolding Extend_def using extend_mem by fast subsubsection \Consistency\ lemma split_list: \set A \ {x} \ X \ x \. A \ \B. set (x # B) = set A \ x \ set B\ by simp (metis Diff_insert_absorb mk_disjoint_insert set_removeAll) lemma consistent_drop_single: fixes a :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and cons: \consistent A ({(p # ps, a)} \ S)\ shows \consistent A ({(ps, a)} \ S)\ unfolding consistent_def proof assume \\S'. set S' \ {(ps, a)} \ S \ A \ S'\ then obtain S' n where \set S' \ {(ps, a)} \ S\ \(ps, a) \. S'\ \A, n \ S'\ using assms unfolding consistent_def by blast then obtain S'' where \set ((ps, a) # S'') = set S'\ \(ps, a) \ set S''\ using split_list by metis then have \A \ (ps, a) # S''\ - using inf fin ST_struct \A, n \ S'\ by blast + using inf fin STA_struct \A, n \ S'\ by blast then have \A \ (p # ps, a) # S''\ - using inf fin ST_struct_block[where ps'=\p # ps\] by fastforce + using inf fin STA_struct_block[where ps'=\p # ps\] by fastforce moreover have \set ((p # ps, a) # S'') \ {(p # ps, a)} \ S\ using \(ps, a) \ set S''\ \set ((ps, a) # S'') = set S'\ \set S' \ {(ps, a)} \ S\ by auto ultimately show False using cons unfolding consistent_def by blast qed lemma consistent_drop_block: \consistent A ({block} \ S) \ consistent A S\ unfolding consistent_def by blast lemma inconsistent_weaken: \\ consistent A S \ S \ S' \ \ consistent A S'\ unfolding consistent_def by blast lemma finite_nominals_set: \finite S \ finite (\block \ S. block_nominals block)\ by (induct S rule: finite_induct) (simp_all add: finite_block_nominals) lemma witness_list_used: fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \finite used\ \i \ list_nominals ps\ shows \i \ list_nominals (witness_list ps ({i} \ used))\ using assms(2-) proof (induct ps arbitrary: used) case (Cons p ps) then show ?case proof (cases \proper_dia p\) case (Some q) let ?j = \SOME j. j \ {i} \ used\ have \finite ({i} \ used)\ using \finite used\ by simp then have \\j. j \ {i} \ used\ using inf ex_new_if_finite by metis then have j: \?j \ {i} \ used\ using someI_ex by metis have \witness_list (p # ps) ({i} \ used) = (\<^bold>@ ?j q) # (\<^bold>\ Nom ?j) # witness_list ps ({?j} \ ({i} \ used))\ using Some witness_list by metis then have *: \list_nominals (witness_list (p # ps) ({i} \ used)) = {?j} \ nominals q \ list_nominals (witness_list ps ({?j} \ ({i} \ used)))\ by simp have \finite ({?j} \ used)\ using \finite used\ by simp moreover have \i \ list_nominals ps\ using \i \ list_nominals (p # ps)\ by simp ultimately have \i \ list_nominals (witness_list ps ({i} \ ({?j} \ used)))\ using Cons by metis moreover have \{i} \ ({?j} \ used) = {?j} \ ({i} \ used)\ by blast moreover have \i \ ?j\ using j by auto ultimately have \i \ list_nominals (witness_list (p # ps) ({i} \ used)) \ i \ nominals q\ using * by simp moreover have \i \ nominals q\ using Cons(3) Some proper_dia by fastforce ultimately show ?thesis by blast qed simp qed simp lemma witness_used: fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \finite used\ \i \ block_nominals block\ shows \i \ block_nominals (witness block ({i} \ used))\ using assms witness_list_used by (induct block) fastforce lemma consistent_witness_list: fixes a :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \consistent A S\ \(ps, a) \ S\ \finite used\ \A \ \ (block_nominals ` S) \ used\ shows \consistent A ({(witness_list ps used, a)} \ S)\ using assms(2-) proof (induct ps arbitrary: used S) case Nil then have \{(witness_list [] used, a)} \ S = S\ by auto moreover have \finite {}\ \{} \ used = {}\ by simp_all ultimately show ?case using \consistent A S\ by simp next case (Cons p ps) have fin: \finite A\ using assms(4-5) finite_subset by fast have \{(p # ps, a)} \ S = S\ using \(p # ps, a) \ S\ by blast then have \consistent A ({(p # ps, a)} \ S)\ using \consistent A S\ by simp then have \consistent A ({(ps, a)} \ S)\ using inf fin consistent_drop_single by fast moreover have \(ps, a) \ {(ps, a)} \ S\ by simp moreover have \A \ \ (block_nominals ` ({(ps, a)} \ S)) \ extra \ used\ for extra using \(p # ps, a) \ S\ \A \ \ (block_nominals ` S) \ used\ by fastforce moreover have \finite (extra \ used)\ if \finite extra\ for extra using that \finite used\ by blast ultimately have cons: \consistent A ({(witness_list ps (extra \ used), a)} \ ({(ps, a)} \ S))\ if \finite extra\ for extra using that Cons by metis show ?case proof (cases \proper_dia p\) case None then have \witness_list (p # ps) used = witness_list ps used\ by auto moreover have \consistent A ({(witness_list ps used, a)} \ ({(ps, a)} \ S))\ using cons[where extra=\{}\] by simp then have \consistent A ({(witness_list ps used, a)} \ S)\ using consistent_drop_block[where block=\(ps, a)\] by auto ultimately show ?thesis by simp next case (Some q) let ?i = \SOME i. i \ used\ have \\i. i \ used\ using ex_new_if_finite inf \finite used\ . with someI_ex have \?i \ used\ . then have i: \?i \ \ (block_nominals ` S)\ using Cons by auto then have \?i \ block_nominals (p # ps, a)\ using Cons by blast let ?tail = \witness_list ps ({?i} \ used)\ have \consistent A ({(?tail, a)} \ ({(ps, a)} \ S))\ using cons[where extra=\{?i}\] by blast then have *: \consistent A ({(?tail, a)} \ S)\ using consistent_drop_block[where block=\(ps, a)\] by simp have \witness_list (p # ps) used = (\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail\ using Some witness_list by metis moreover have \consistent A ({((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a)} \ S)\ unfolding consistent_def proof assume \\S'. set S' \ {((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a)} \ S \ A \ S'\ then obtain S' n where \A, n \ S'\ and S': \set S' \ {((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a)} \ S\ \((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) \. S'\ using * unfolding consistent_def by blast then obtain S'' where S'': \set (((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) # S'') = set S'\ \((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) \ set S''\ using split_list[where x=\((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a)\] by blast then have \A \ ((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) # S''\ - using inf \finite A\ ST_struct \A, n \ S'\ by blast + using inf \finite A\ STA_struct \A, n \ S'\ by blast moreover have \set (((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) # S'') \ set (((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) # (p # ps, a) # S'')\ by auto ultimately have **: \A \ ((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) # (p # ps, a) # S''\ - using inf \finite A\ ST_struct by blast + using inf \finite A\ STA_struct by blast have \?i \ block_nominals (?tail, a)\ using inf \finite used\ \?i \ block_nominals (p # ps, a)\ witness_used by fastforce moreover have \?i \ branch_nominals S''\ unfolding branch_nominals_def using i S' S'' by auto ultimately have \?i \ branch_nominals ((?tail, a) # (p # ps, a) # S'')\ using \?i \ block_nominals (p # ps, a)\ unfolding branch_nominals_def by simp then have \?i \ A \ branch_nominals ((?tail, a) # (p # ps, a) # S'')\ using \?i \ used\ Cons.prems(4) by blast moreover have \\a. q = Nom a\ using Some proper_dia by blast moreover have \(p # ps, a) \. (?tail, a) # (p # ps, a) # S''\ by simp moreover have \p = (\<^bold>\ q)\ using Some proper_dia by blast then have \(\<^bold>\ q) on (p # ps, a)\ by simp ultimately have \A \ (?tail, a) # (p # ps, a) # S''\ using ** \finite A\ DiaP'' by fast moreover have \set ((p # ps, a) # S'') \ S\ using Cons(3) S' S'' by auto ultimately show False using * unfolding consistent_def by (simp add: subset_Un_eq) qed ultimately show ?thesis by simp qed qed lemma consistent_witness: fixes block :: \('a, 'b) block\ assumes \infinite (UNIV :: 'b set)\ \consistent A S\ \finite (\ (block_nominals ` S))\ \block \ S\ \finite A\ shows \consistent A ({witness block (A \ \ (block_nominals ` S))} \ S)\ using assms consistent_witness_list by (cases block) fastforce lemma consistent_extend: fixes S :: \('a, 'b) block set\ assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and \consistent A (extend A S f n)\ \finite (\ (block_nominals ` extend A S f n))\ shows \consistent A (extend A S f (Suc n))\ proof (cases \consistent A ({f n} \ extend A S f n)\) case True let ?used = \A \ (\block \ {f n} \ extend A S f n. block_nominals block)\ have *: \extend A S f (n + 1) = {f n, witness (f n) ?used} \ extend A S f n\ using True by simp have \consistent A ({f n} \ extend A S f n)\ using True by simp moreover have \finite ((\ (block_nominals ` ({f n} \ extend A S f n))))\ using \finite (\ (block_nominals ` extend A S f n))\ finite_nominals_set by force moreover have \f n \ {f n} \ extend A S f n\ by simp ultimately have \consistent A ({witness (f n) ?used} \ ({f n} \ extend A S f n))\ using inf fin consistent_witness by blast then show ?thesis using * by simp next case False then show ?thesis using assms(3) by simp qed lemma finite_nominals_extend: assumes \finite (\ (block_nominals ` S))\ shows \finite (\ (block_nominals ` extend A S f n))\ using assms by (induct n) (auto simp add: finite_block_nominals) lemma consistent_extend': fixes S :: \('a, 'b) block set\ assumes \infinite (UNIV :: 'b set)\ \finite A\ \consistent A S\ \finite (\ (block_nominals ` S))\ shows \consistent A (extend A S f n)\ using assms proof (induct n) case (Suc n) then show ?case by (metis consistent_extend finite_nominals_extend) qed simp lemma UN_finite_bound: assumes \finite A\ \A \ (\n. f n)\ shows \\m :: nat. A \ (\n \ m. f n)\ using assms proof (induct A rule: finite_induct) case (insert x A) then obtain m where \A \ (\n \ m. f n)\ by fast then have \A \ (\n \ (m + k). f n)\ for k by fastforce moreover obtain m' where \x \ f m'\ using insert(4) by blast ultimately have \{x} \ A \ (\n \ m + m'. f n)\ by auto then show ?case by blast qed simp lemma extend_bound: \(\n \ m. extend A S f n) = extend A S f m\ proof (induct m) case (Suc m) have \\ (extend A S f ` {..Suc m}) = \ (extend A S f ` {..m}) \ extend A S f (Suc m)\ using atMost_Suc by auto also have \\ = extend A S f m \ extend A S f (Suc m)\ using Suc by blast also have \\ = extend A S f (Suc m)\ using extend_chain by blast finally show ?case by simp qed simp lemma consistent_Extend: fixes S :: \('a, 'b) block set\ assumes inf: \infinite (UNIV :: 'b set)\ and \finite A\ \consistent A S\ \finite (\ (block_nominals ` S))\ shows \consistent A (Extend A S f)\ unfolding Extend_def proof (rule ccontr) assume \\ consistent A (\ (range (extend A S f)))\ then obtain S' n where *: \A, n \ S'\ \set S' \ (\n. extend A S f n)\ unfolding consistent_def by blast moreover have \finite (set S')\ by simp ultimately obtain m where \set S' \ (\n \ m. extend A S f n)\ using UN_finite_bound by metis then have \set S' \ extend A S f m\ using extend_bound by blast moreover have \consistent A (extend A S f m)\ using assms consistent_extend' by blast ultimately show False unfolding consistent_def using * by blast qed subsubsection \Maximality\ text \A set of blocks is maximally consistent if any proper extension makes it inconsistent.\ definition maximal :: \'b set \ ('a, 'b) block set \ bool\ where - \maximal A S \ consistent A S \ - (\block. block \ S \ \ consistent A ({block} \ S))\ + \maximal A S \ consistent A S \ (\block. block \ S \ \ consistent A ({block} \ S))\ lemma extend_not_mem: \f n \ extend A S f (Suc n) \ \ consistent A ({f n} \ extend A S f n)\ by (metis Un_insert_left extend.simps(2) insertI1) lemma maximal_Extend: fixes S :: \('a, 'b) block set\ assumes inf: \infinite (UNIV :: 'b set)\ and \finite A\ \consistent A S\ \finite (\ (block_nominals ` S))\ \surj f\ shows \maximal A (Extend A S f)\ proof (rule ccontr) assume \\ maximal A (Extend A S f)\ then obtain block where \block \ Extend A S f\ \consistent A ({block} \ Extend A S f)\ unfolding maximal_def using assms consistent_Extend by metis obtain n where n: \f n = block\ using \surj f\ unfolding surj_def by metis then have \block \ extend A S f (Suc n)\ using \block \ Extend A S f\ extend_chain unfolding Extend_def by blast then have \\ consistent A ({block} \ extend A S f n)\ using n extend_not_mem by blast moreover have \block \ extend A S f n\ using \block \ extend A S f (Suc n)\ extend_chain by blast then have \{block} \ extend A S f n \ {block} \ Extend A S f\ unfolding Extend_def by blast ultimately have \\ consistent A ({block} \ Extend A S f)\ using inconsistent_weaken by blast then show False using \consistent A ({block} \ Extend A S f)\ by simp qed subsubsection \Saturation\ text \A set of blocks is saturated if every \\<^bold>\ p\ is witnessed.\ definition saturated :: \('a, 'b) block set \ bool\ where \saturated S \ \p i. (\<^bold>\ p) at i in' S \ (\a. p = Nom a) \ (\j. (\<^bold>@ j p) at i in' S \ (\<^bold>\ Nom j) at i in' S)\ lemma witness_list_append: \\extra. witness_list (ps @ qs) used = witness_list ps used @ witness_list qs (extra \ used)\ proof (induct ps arbitrary: used) case Nil then show ?case by (metis Un_absorb append_self_conv2 witness_list.simps(1)) next case (Cons p ps) show ?case proof (cases \\q. proper_dia p = Some q\) case True let ?i = \SOME i. i \ used\ from True obtain q where q: \proper_dia p = Some q\ by blast moreover have \(p # ps) @ qs = p # (ps @ qs)\ by simp ultimately have \witness_list ((p # ps) @ qs) used = (\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # witness_list (ps @ qs) ({?i} \ used)\ using witness_list by metis then have \\extra. witness_list ((p # ps) @ qs) used = (\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # witness_list ps ({?i} \ used) @ witness_list qs (extra \ ({?i} \ used))\ using Cons by metis moreover have \(\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # witness_list ps ({?i} \ used) = witness_list (p # ps) used\ using q witness_list by metis ultimately have \\extra. witness_list ((p # ps) @ qs) used = witness_list (p # ps) used @ witness_list qs (extra \ ({?i} \ used))\ by (metis append_Cons) then have \\extra. witness_list ((p # ps) @ qs) used = witness_list (p # ps) used @ witness_list qs (({?i} \ extra) \ used)\ by simp then show ?thesis by blast qed (simp add: Cons) qed lemma ex_witness_list: assumes \p \. ps\ \proper_dia p = Some q\ shows \\i. {\<^bold>@ i q, \<^bold>\ Nom i} \ set (witness_list ps used)\ using \p \. ps\ proof (induct ps arbitrary: used) case (Cons a ps) then show ?case proof (induct \a = p\) case True then have \\i. witness_list (a # ps) used = (\<^bold>@ i q) # (\<^bold>\ Nom i) # witness_list ps ({i} \ used)\ using \proper_dia p = Some q\ witness_list by metis then show ?case by auto next case False then have \\i. {\<^bold>@ i q, \<^bold>\ Nom i} \ set (witness_list ps (extra \ used))\ for extra by simp moreover have \\extra. witness_list (a # ps) used = witness_list [a] used @ witness_list ps (extra \ used)\ using witness_list_append[where ps=\[_]\] by simp ultimately show ?case by fastforce qed qed simp lemma saturated_Extend: fixes S :: \('a, 'b) block set\ assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and \consistent A S\ \finite (\ (block_nominals ` S))\ \surj f\ shows \saturated (Extend A S f)\ unfolding saturated_def proof safe fix ps i p assume \(ps, i) \ Extend A S f\ \(\<^bold>\ p) on (ps, i)\ \\a. p = Nom a\ obtain n where n: \f n = (ps, i)\ using \surj f\ unfolding surj_def by metis let ?used = \A \ (\block \ {f n} \ extend A S f n. block_nominals block)\ have \extend A S f n \ Extend A S f\ unfolding Extend_def by auto moreover have \consistent A (Extend A S f)\ using assms consistent_Extend by blast ultimately have \consistent A ({(ps, i)} \ extend A S f n)\ using \(ps, i) \ Extend A S f\ inconsistent_weaken by blast then have \extend A S f (Suc n) = {f n, witness (f n) ?used} \ extend A S f n\ using n \(\<^bold>\ p) on (ps, i)\ by auto then have \witness (f n) ?used \ Extend A S f\ unfolding Extend_def by blast then have *: \(witness_list ps ?used, i) \ Extend A S f\ using n by simp have \(\<^bold>\ p) \. ps\ using \(\<^bold>\ p) on (ps, i)\ by simp moreover have \proper_dia (\<^bold>\ p) = Some p\ unfolding proper_dia_def using \\a. p = Nom a\ by simp ultimately have \\j. (\<^bold>@ j p) on (witness_list ps ?used, i) \ (\<^bold>\ Nom j) on (witness_list ps ?used, i)\ using ex_witness_list by fastforce then show \\j. (\qs. (qs, i) \ Extend A S f \ (\<^bold>@ j p) on (qs, i)) \ (\rs. (rs, i) \ Extend A S f \ (\<^bold>\ Nom j) on (rs, i))\ using * by blast qed subsection \Smullyan-Fitting\ -lemma Nom_trans: - fixes i :: 'b - assumes - inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and - \Nom j at i in (ps, i) # branch\ \Nom k at j in (ps, i) # branch\ - \i \ A\ \k \ A\ - \A, n \ (Nom k # ps, i) # branch\ - shows \A \ (ps, i) # branch\ -proof - - have \set ((Nom k # ps, i) # branch) \ set ((Nom k # ps, i) # ([Nom i], j) # branch)\ - by auto - then have \A \ (Nom k # ps, i) # ([Nom i], j) # branch\ - using ST_struct inf fin assms(7) by blast - then have \A \ (ps, i) # ([Nom i], j) # branch\ - using assms(4, 6) Nom'[where p=\Nom k\ and b=j and a=i] - by (metis (no_types, lifting) fm.distinct(15) fm.inject(2) list.set_intros on.simps set_ConsD) - then have \A \ ([Nom i], j) # (ps, i) # branch\ - using ST_struct[where branch'=\([Nom i], j) # (ps, i) # branch\] inf fin by fastforce - then have \A \ ([], j) # (ps, i) # branch\ - using assms(3, 5) Nom'[where p=\Nom i\ and a=j and b=i] - by (metis fm.distinct(15) fm.inject(2) insertCI list.set(2) on.simps) - moreover have \j \ branch_nominals ((ps, i) # branch)\ - using assms(4) unfolding branch_nominals_def by fastforce - ultimately show ?thesis - using GoTo by fast -qed - -lemma hintikka_Extend: +lemma Hintikka_Extend: fixes S :: \('a, 'b) block set\ assumes inf: \infinite (UNIV :: 'b set)\ and fin: \finite A\ and \maximal A S\ \consistent A S\ \saturated S\ - shows \hintikka A S\ - unfolding hintikka_def + shows \Hintikka A S\ + unfolding Hintikka_def proof safe fix x i j ps qs rs assume ps: \(ps, i) \ S\ \Nom j on (ps, i)\ and qs: \(qs, j) \ S\ \Pro x on (qs, j)\ and rs: \(rs, i) \ S\ \(\<^bold>\ Pro x) on (rs, i)\ then have \\ A, n \ [(qs, j), (ps, i), (rs, i)]\ for n using \consistent A S\ unfolding consistent_def by simp moreover have \A, n \ [((\<^bold>\ Pro x) # qs, j), (ps, i), (rs, i)]\ for n using qs(2) Close by (metis (no_types, lifting) list.set_intros(1) on.simps set_subset_Cons subsetD) then have \A, n \ [(qs, j), (ps, i), (rs, i)]\ for n using ps(2) rs(2) by (meson Nom' fm.distinct(21) fm.simps(18) list.set_intros(1) set_subset_Cons subsetD) ultimately show False by blast next fix a i ps qs assume ps: \(ps, i) \ S\ \Nom a on (ps, i)\ and qs: \(qs, i) \ S\ \(\<^bold>\ Nom a) on (qs, i)\ then have \\ A , n \ [(ps, i), (qs, i)]\ for n using \consistent A S\ unfolding consistent_def by simp moreover have \A, n \ [(ps, i), (qs, i)]\ for n using ps(2) qs(2) by (meson Close list.set_intros(1) set_subset_Cons subset_code(1)) ultimately show False by blast next - fix i j ps qs - assume - ps: \(ps, i) \ S\ \(\<^bold>\ Nom j) on (ps, i)\ and - qs: \(qs, i) \ S\ \(\<^bold>\ (\<^bold>\ Nom j)) on (qs, i)\ - then have \\ A, n \ [(ps, i), (qs, i)]\ for n - using \consistent A S\ unfolding consistent_def by simp - moreover have \A, n \ [(ps, i), (qs, i)]\ for n - using ps(2) qs(2) Close[where p=\\<^bold>\ Nom j\ and i=i] by force - ultimately show False - by blast -next - fix p i ps a - assume i: \i \ nominals p\ and ps: \(ps, a) \ S\ \p on (ps, a)\ - show \\qs. (qs, i) \ S\ + fix p i ps + assume ps: \(ps, i) \ S\ \(\<^bold>\ \<^bold>\ p) on (ps, i)\ + show \p at i in' S\ proof (rule ccontr) - assume \\qs. (qs, i) \ S\ + assume \\ p at i in' S\ then obtain S' n where - \A, n \ S'\ and S': \set S' \ {([], i)} \ S\ and \([], i) \. S'\ - using \maximal A S\ unfolding maximal_def consistent_def - by (metis insert_is_Un subset_insert) - then obtain S'' where S'': - \set (([], i) # S'') = set S'\ \([], i) \ set S''\ - using split_list[where x=\([], i)\] by blast - then have \A \ ([], i) # (ps, a) # S''\ - using inf fin ST_struct[where branch'=\([], i) # (ps, a) # S''\] \A, n \ S'\ by fastforce - moreover have \i \ branch_nominals ((ps, a) # S'')\ - using i ps unfolding branch_nominals_def by auto - ultimately have \A \ (ps, a) # S''\ - using GoTo by fast - moreover have \set ((ps, a) # S'') \ S\ - using S' S'' ps by auto - ultimately show False - using \consistent A S\ unfolding consistent_def by blast - qed -next - fix i j ps - assume i: \i \ A\ and ps: \(ps, i) \ S\ \Nom j on (ps, i)\ - show \\qs. (qs, j) \ S \ Nom i on (qs, j)\ - proof (rule ccontr) - assume \\qs. (qs, j) \ S \ Nom i on (qs, j)\ - then obtain S' n where - \A, n \ S'\ and S': \set S' \ {([Nom i], j)} \ S\ and \([Nom i], j) \. S'\ - using \maximal A S\ unfolding maximal_def consistent_def - by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) - then obtain S'' where S'': - \set (([Nom i], j) # S'') = set S'\ \([Nom i], j) \ set S''\ - using split_list[where x=\([Nom i], j)\] by blast - then have \A \ ([Nom i], j) # (ps, i) # S''\ - using inf fin ST_struct[where branch'=\([Nom i], j) # (ps, i) # S''\] \A, n \ S'\ by fastforce - then have \A \ ([], j) # (ps, i) # S''\ - using i ps(2) - by (metis Nom' fm.distinct(15) fm.inject(2) list.set_intros(1) list.set_intros(2) on.simps) - moreover have \j \ branch_nominals ((ps, i) # S'')\ - using \Nom j on (ps, i)\ unfolding branch_nominals_def by fastforce - ultimately have \A \ (ps, i) # S''\ - using GoTo by fast - moreover have \set ((ps, i) # S'') \ S\ - using S' S'' ps by auto - ultimately show False - using \consistent A S\ unfolding consistent_def by blast - qed -next - fix i j k ps qs - assume - ps: \(ps, i) \ S\ \Nom j on (ps, i)\ and - qs: \(qs, j) \ S\ \Nom k on (qs, j)\ and - i: \i \ A\ and k: \k \ A\ - show \\rs. (rs, i) \ S \ Nom k on (rs, i)\ - proof (rule ccontr) - assume \\rs. (rs, i) \ S \ Nom k on (rs, i)\ - then obtain S' n where - \A, n \ S'\ and S': \set S' \ {([Nom k], i)} \ S\ and \([Nom k], i) \. S'\ + \A, n \ S'\ and S': \set S' \ {(p # ps, i)} \ S\ and \(p # ps, i) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) then obtain S'' where S'': - \set (([Nom k], i) # S'') = set S'\ \([Nom k], i) \ set S''\ - using split_list[where x=\([Nom k], i)\] by blast - then have \A \ ([Nom k], i) # (Nom k # ps, i) # (qs, j) # S''\ - using inf fin ST_struct[where branch'=\([Nom k], i) # (Nom k # ps, i) # (qs, j) # S''\] - \A, n \ S'\ by fastforce - then have \A \ ([], i) # (Nom k # ps, i) # (qs, j) # S''\ - by (meson Dup list.set_intros(1) new_def on.simps set_subset_Cons subset_code(1)) - moreover have \i \ branch_nominals ((Nom k # ps, i) # (qs, j) # S'')\ - unfolding branch_nominals_def by simp - ultimately have \A \ (Nom k # ps, i) # (qs, j) # S''\ - using GoTo by fast - moreover have \Nom j at i in (ps, i) # (qs, j) # S''\ \Nom k at j in (ps, i) # (qs, j) # S''\ - using ps(2) qs(2) by auto - ultimately have \A \ (ps, i) # (qs, j) # S''\ - using Nom_trans[where i=i and j=j and k=k] inf fin i k by fast - moreover have \set ((ps, i) # (qs, j) # S'') \ S\ - using S' S'' ps qs by auto - ultimately show False - using \consistent A S\ unfolding consistent_def by blast - qed -next - fix i j k ps qs - assume - ps: \(ps, i) \ S\ \(\<^bold>\ Nom j) on (ps, i)\ and - qs: \(qs, j) \ S\ \Nom k on (qs, j)\ and - j: \j \ A\ - show \\rs. (rs, i) \ S \ (\<^bold>\ Nom k) on (rs, i)\ - proof (rule ccontr) - assume \\rs. (rs, i) \ S \ (\<^bold>\ Nom k) on (rs, i)\ - then obtain S' n where - \A, n \ S'\ and S': \set S' \ {([\<^bold>\ Nom k], i)} \ S\ and \([\<^bold>\ Nom k], i) \. S'\ - using \maximal A S\ unfolding maximal_def consistent_def - by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) - then obtain S'' where S'': - \set (([\<^bold>\ Nom k], i) # S'') = set S'\ \([\<^bold>\ Nom k], i) \ set S''\ - using split_list[where x=\([\<^bold>\ Nom k], i)\] by blast - then have \A \ ([\<^bold>\ Nom k], i) # (ps, i) # (qs, j) # S''\ - using inf fin ST_struct[where branch'=\([\<^bold>\ Nom k], i) # (ps, i) # (qs, j) # S''\] \A, n \ S'\ - by fastforce - then have \A \ ([], i) # (ps, i) # (qs, j) # S''\ - using ps(2) qs(2) j inf fin ST_bridge - by (meson Bridge list.set_intros(1) on.simps set_subset_Cons subset_iff) - moreover have \i \ branch_nominals ((ps, i) # (qs, j) # S'')\ - using ps unfolding branch_nominals_def by fastforce - ultimately have \A \ (ps, i) # (qs, j) # S''\ - using GoTo by fast - moreover have \set ((ps, i) # (qs, j) # S'') \ S\ - using S' S'' ps qs by auto - ultimately show False - using \consistent A S\ unfolding consistent_def by blast - qed -next - fix i j k ps qs - assume - ps: \(ps, i) \ S\ \(\<^bold>\ Nom j) on (ps, i)\ and - qs: \(qs, i) \ S\ \Nom k on (qs, i)\ and - j: \j \ A\ - show \\rs. (rs, k) \ S \ (\<^bold>\ Nom j) on (rs, k)\ - proof (rule ccontr) - assume \\rs. (rs, k) \ S \ (\<^bold>\ Nom j) on (rs, k)\ - then obtain S' n where - \A, n \ S'\ and S': \set S' \ {([\<^bold>\ Nom j], k)} \ S\ and \([\<^bold>\ Nom j], k) \. S'\ - using \maximal A S\ unfolding maximal_def consistent_def - by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) - then obtain S'' where S'': - \set (([\<^bold>\ Nom j], k) # S'') = set S'\ \([\<^bold>\ Nom j], k) \ set S''\ - using split_list[where x=\([\<^bold>\ Nom j], k)\] by blast - then have \A \ ([\<^bold>\ Nom j], k) # (Nom k # ps, i) # (qs, i) # S''\ - using inf fin ST_struct[where branch'=\([\<^bold>\ Nom j], k) # (Nom k # ps, i) # (qs, i) # S''\] - \A, n \ S'\ by fastforce - then have \A \ ([], k) # (Nom k # ps, i) # (qs, i) # S''\ - using ps(2) j Nom'[where p=\\<^bold>\ Nom j\ and a=k and b=i and branch=\(Nom k # ps, i) # _\] - by fastforce - moreover have \k \ branch_nominals ((Nom k # ps, i) # (qs, i) # S'')\ - unfolding branch_nominals_def by simp - ultimately have \A \ (Nom k # ps, i) # (qs, i) # S''\ - using GoTo by fast - then have \A \ (ps, i) # (qs, i) # S''\ - using ps(2) qs(2) by (meson Dup list.set_intros(1) new_def set_subset_Cons subsetD) - moreover have \set ((ps, i) # (qs, i) # S'') \ S\ - using S' S'' ps qs by auto + \set ((p # ps, i) # S'') = set S'\ \(p # ps, i) \ set S''\ + using split_list[where x=\(p # ps, i)\] by blast + then have \A \ (p # ps, i) # S''\ + using inf fin STA_struct \A, n \ S'\ by blast + then have \A \ (ps, i) # S''\ + using ps by (meson Neg' list.set_intros(1)) + moreover have \set ((ps, i) # S'') \ S\ + using S' S'' ps by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next fix p q i ps assume ps: \(ps, i) \ S\ \(p \<^bold>\ q) on (ps, i)\ and *: \\ q at i in' S\ show \p at i in' S\ proof (rule ccontr) assume \\ p at i in' S\ then obtain Sp' np where \A, np \ Sp'\ and Sp': \set Sp' \ {(p # ps, i)} \ S\ and \(p # ps, i) \. Sp'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) then obtain Sp'' where Sp'': \set ((p # ps, i) # Sp'') = set Sp'\ \(p # ps, i) \ set Sp''\ using split_list[where x=\(p # ps, i)\] by blast then have \A \ (p # ps, i) # Sp''\ - using \A, np \ Sp'\ inf fin ST_struct by blast + using \A, np \ Sp'\ inf fin STA_struct by blast obtain Sq' nq where \A, nq \ Sq'\ and Sq': \set Sq' \ {(q # ps, i)} \ S\ and \(q # ps, i) \. Sq'\ using * \maximal A S\ unfolding maximal_def consistent_def by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) then obtain Sq'' where Sq'': \set ((q # ps, i) # Sq'') = set Sq'\ \(q # ps, i) \ set Sq''\ using split_list[where x=\(q # ps, i)\] by blast then have \A \ (q # ps, i) # Sq''\ - using \A, nq \ Sq'\ inf fin ST_struct by blast + using \A, nq \ Sq'\ inf fin STA_struct by blast obtain S'' where S'': \set S'' = set Sp'' \ set Sq''\ by (meson set_union) then have \set ((p # ps, i) # Sp'') \ set ((p # ps, i) # S'')\ \set ((q # ps, i) # Sq'') \ set ((q # ps, i) # S'')\ by auto then have \A \ (p # ps, i) # S''\ \A \ (q # ps, i) # S''\ - using \A \ (p # ps, i) # Sp''\ \A \ (q # ps, i) # Sq''\ inf fin ST_struct by blast+ + using \A \ (p # ps, i) # Sp''\ \A \ (q # ps, i) # Sq''\ inf fin STA_struct by blast+ then have \A \ (ps, i) # S''\ using ps by (meson DisP'' list.set_intros(1)) moreover have \set ((ps, i) # S'') \ S\ using ps Sp' Sp'' Sq' Sq'' S'' by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next fix p q i ps assume ps: \(ps, i) \ S\ \(\<^bold>\ (p \<^bold>\ q)) on (ps, i)\ show \(\<^bold>\ p) at i in' S\ proof (rule ccontr) assume \\ (\<^bold>\ p) at i in' S\ then obtain S' where \A \ S'\ and S': \set S' \ {((\<^bold>\ q) # (\<^bold>\ p) # ps, i)} \ S\ and \((\<^bold>\ q) # (\<^bold>\ p) # ps, i) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis (mono_tags, lifting) insert_is_Un insert_subset list.simps(15) on.simps set_subset_Cons subset_insert) then obtain S'' where S'': \set (((\<^bold>\ q) # (\<^bold>\ p) # ps, i) # S'') = set S'\ \((\<^bold>\ q) # (\<^bold>\ p) # ps, i) \ set S''\ using split_list[where x=\((\<^bold>\ q) # (\<^bold>\ p) # ps, i)\] by blast then have \A \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, i) # S''\ - using inf fin ST_struct \A \ S'\ by blast + using inf fin STA_struct \A \ S'\ by blast then have \A \ (ps, i) # S''\ using ps by (meson DisN' list.set_intros(1)) moreover have \set ((ps, i) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next fix p q i ps assume ps: \(ps, i) \ S\ \(\<^bold>\ (p \<^bold>\ q)) on (ps, i)\ show \(\<^bold>\ q) at i in' S\ proof (rule ccontr) assume \\ (\<^bold>\ q) at i in' S\ then obtain S' where \A \ S'\ and S': \set S' \ {((\<^bold>\ q) # (\<^bold>\ p) # ps, i)} \ S\ and \((\<^bold>\ q) # (\<^bold>\ p) # ps, i) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis (mono_tags, lifting) insert_is_Un insert_subset list.simps(15) on.simps set_subset_Cons subset_insert) then obtain S'' where S'': \set (((\<^bold>\ q) # (\<^bold>\ p) # ps, i) # S'') = set S'\ \((\<^bold>\ q) # (\<^bold>\ p) # ps, i) \ set S''\ using split_list[where x=\((\<^bold>\ q) # (\<^bold>\ p) # ps, i)\] by blast then have \A \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, i) # S''\ - using inf fin ST_struct \A \ S'\ by blast + using inf fin STA_struct \A \ S'\ by blast then have \A \ (ps, i) # S''\ using ps by (meson DisN' list.set_intros(1)) moreover have \set ((ps, i) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next fix p i ps - assume ps: \(ps, i) \ S\ \(\<^bold>\ \<^bold>\ p) on (ps, i)\ - show \\qs. (qs, i) \ S \ p on (qs, i)\ + assume \\a. p = Nom a\ \(ps, i) \ S\ \(\<^bold>\ p) on (ps, i)\ + then show \\j. (\<^bold>\ Nom j) at i in' S \ (\<^bold>@ j p) at i in' S\ + using \saturated S\ unfolding saturated_def by blast +next + fix p i j ps qs + assume + ps: \(ps, i) \ S\ \(\<^bold>\ (\<^bold>\ p)) on (ps, i)\ and + qs: \(qs, i) \ S\ \(\<^bold>\ Nom j) on (qs, i)\ + show \(\<^bold>\ (\<^bold>@ j p)) at i in' S\ proof (rule ccontr) - assume \\qs. (qs, i) \ S \ p on (qs, i)\ + assume \\ (\<^bold>\ (\<^bold>@ j p)) at i in' S\ then obtain S' n where - \A, n \ S'\ and S': \set S' \ {(p # ps, i)} \ S\ and \(p # ps, i) \. S'\ + \A, n \ S'\ and S': \set S' \ {([\<^bold>\ (\<^bold>@ j p)], i)} \ S\ and \([\<^bold>\ (\<^bold>@ j p)], i) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) then obtain S'' where S'': - \set ((p # ps, i) # S'') = set S'\ \(p # ps, i) \ set S''\ - using split_list[where x=\(p # ps, i)\] by blast - then have \A \ (p # ps, i) # S''\ - using inf fin ST_struct \A, n \ S'\ by blast - then have \A \ (ps, i) # S''\ - using ps by (meson Neg' list.set_intros(1)) - moreover have \set ((ps, i) # S'') \ S\ - using S' S'' ps by auto + \set (([\<^bold>\ (\<^bold>@ j p)], i) # S'') = set S'\ \([\<^bold>\ (\<^bold>@ j p)], i) \ set S''\ + using split_list[where x=\([\<^bold>\ (\<^bold>@ j p)], i)\] by blast + then have \A \ ([\<^bold>\ (\<^bold>@ j p)], i) # S''\ + using inf fin STA_struct \A, n \ S'\ by blast + then have \A \ ([\<^bold>\ (\<^bold>@ j p)], i) # (ps, i) # (qs, i) # S''\ + using inf fin STA_struct[where branch'=\([_], _) # (ps, i) # (qs, i) # S''\] \A, n \ S'\ + by fastforce + then have \A \ ([], i) # (ps, i) # (qs, i) # S''\ + using ps(2) qs(2) by (meson DiaN' list.set_intros(1) set_subset_Cons subset_iff) + moreover have \i \ branch_nominals ((ps, i) # (qs, i) # S'')\ + unfolding branch_nominals_def by simp + ultimately have \A \ (ps, i) # (qs, i) # S''\ + using GoTo by fast + moreover have \set ((ps, i) # (qs, i) # S'') \ S\ + using S' S'' ps qs by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next fix p i ps a assume ps: \(ps, a) \ S\ \(\<^bold>@ i p) on (ps, a)\ - show \\qs. (qs, i) \ S \ p on (qs, i)\ + show \p at i in' S\ proof (rule ccontr) - assume \\qs. (qs, i) \ S \ p on (qs, i)\ + assume \\ p at i in' S\ then obtain S' n where \A, n \ S'\ and S': \set S' \ {([p], i)} \ S\ and \([p], i) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) then obtain S'' where S'': \set (([p], i) # S'') = set S'\ \([p], i) \ set S''\ using split_list[where x=\([p], i)\] by blast then have \A \ ([p], i) # S''\ - using inf fin ST_struct \A, n \ S'\ by blast + using inf fin STA_struct \A, n \ S'\ by blast moreover have \set (([p], i) # S'') \ set (([p], i) # (ps, a) # S'')\ by auto ultimately have \A \ ([p], i) # (ps, a) # S''\ - using inf fin ST_struct \A, n \ S'\ by blast + using inf fin STA_struct \A, n \ S'\ by blast then have \A \ ([], i) # (ps, a) # S''\ using ps by (metis SatP' insert_iff list.simps(15)) moreover have \i \ branch_nominals ((ps, a) # S'')\ using ps unfolding branch_nominals_def by fastforce ultimately have \A \ (ps, a) # S''\ using GoTo by fast moreover have \set ((ps, a) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next fix p i ps a assume ps: \(ps, a) \ S\ \(\<^bold>\ (\<^bold>@ i p)) on (ps, a)\ - show \\qs. (qs, i) \ S \ (\<^bold>\ p) on (qs, i)\ + show \(\<^bold>\ p) at i in' S\ proof (rule ccontr) - assume \\qs. (qs, i) \ S \ (\<^bold>\ p) on (qs, i)\ + assume \\ (\<^bold>\ p) at i in' S\ then obtain S' n where \A, n \ S'\ and S': \set S' \ {([\<^bold>\ p], i)} \ S\ and \([\<^bold>\ p], i) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) then obtain S'' where S'': \set (([\<^bold>\ p], i) # S'') = set S'\ \([\<^bold>\ p], i) \ set S''\ using split_list[where x=\([\<^bold>\ p], i)\] by blast then have \A \ ([\<^bold>\ p], i) # S''\ - using inf fin ST_struct \A, n \ S'\ by blast + using inf fin STA_struct \A, n \ S'\ by blast then have \A \ ([\<^bold>\ p], i) # (ps, a) # S''\ - using inf fin ST_struct[where branch'=\([\<^bold>\ p], i) # _ # S''\] \A, n \ S'\ + using inf fin STA_struct[where branch'=\([\<^bold>\ p], i) # _ # S''\] \A, n \ S'\ by fastforce then have \A \ ([], i) # (ps, a) # S''\ using ps by (metis SatN' insert_iff list.simps(15)) moreover have \i \ branch_nominals ((ps, a) # S'')\ using ps unfolding branch_nominals_def by fastforce ultimately have \A \ (ps, a) # S''\ using GoTo by fast moreover have \set ((ps, a) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next - fix p i ps - assume - \\a. p = Nom a\ and - ps: \(ps, i) \ S\ \(\<^bold>\ p) on (ps, i)\ - then show \\j. - (\qs. (qs, i) \ S \ (\<^bold>\ Nom j) on (qs, i)) \ - (\rs. (rs, i) \ S \ (\<^bold>@ j p) on (rs, i))\ - using \saturated S\ unfolding saturated_def by blast -next - fix p i j ps qs - assume - ps: \(ps, i) \ S\ \(\<^bold>\ (\<^bold>\ p)) on (ps, i)\ and - qs: \(qs, i) \ S\ \(\<^bold>\ Nom j) on (qs, i)\ - show \\rs. (rs, i) \ S \ (\<^bold>\ (\<^bold>@ j p)) on (rs, i)\ + fix p i ps a + assume i: \i \ nominals p\ and ps: \(ps, a) \ S\ \p on (ps, a)\ + show \\qs. (qs, i) \ S\ proof (rule ccontr) - assume \\qs. (qs, i) \ S \ (\<^bold>\ (\<^bold>@ j p)) on (qs, i)\ + assume \\qs. (qs, i) \ S\ then obtain S' n where - \A, n \ S'\ and S': \set S' \ {([\<^bold>\ (\<^bold>@ j p)], i)} \ S\ and \([\<^bold>\ (\<^bold>@ j p)], i) \. S'\ + \A, n \ S'\ and S': \set S' \ {([], i)} \ S\ and \([], i) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def - by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) + by (metis insert_is_Un subset_insert) then obtain S'' where S'': - \set (([\<^bold>\ (\<^bold>@ j p)], i) # S'') = set S'\ \([\<^bold>\ (\<^bold>@ j p)], i) \ set S''\ - using split_list[where x=\([\<^bold>\ (\<^bold>@ j p)], i)\] by blast - then have \A \ ([\<^bold>\ (\<^bold>@ j p)], i) # S''\ - using inf fin ST_struct \A, n \ S'\ by blast - then have \A \ ([\<^bold>\ (\<^bold>@ j p)], i) # (ps, i) # (qs, i) # S''\ - using inf fin ST_struct[where branch'=\([_], _) # (ps, i) # (qs, i) # S''\] \A, n \ S'\ - by fastforce - then have \A \ ([], i) # (ps, i) # (qs, i) # S''\ - using ps(2) qs(2) by (meson DiaN' list.set_intros(1) set_subset_Cons subset_iff) - moreover have \i \ branch_nominals ((ps, i) # (qs, i) # S'')\ - unfolding branch_nominals_def by simp - ultimately have \A \ (ps, i) # (qs, i) # S''\ + \set (([], i) # S'') = set S'\ \([], i) \ set S''\ + using split_list[where x=\([], i)\] by blast + then have \A \ ([], i) # (ps, a) # S''\ + using inf fin STA_struct[where branch'=\([], i) # (ps, a) # S''\] \A, n \ S'\ by fastforce + moreover have \i \ branch_nominals ((ps, a) # S'')\ + using i ps unfolding branch_nominals_def by auto + ultimately have \A \ (ps, a) # S''\ using GoTo by fast - moreover have \set ((ps, i) # (qs, i) # S'') \ S\ - using S' S'' ps qs by auto + moreover have \set ((ps, a) # S'') \ S\ + using S' S'' ps by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed next fix p i j ps qs assume p: \\a. p = Nom a \ p = (\<^bold>\ Nom a) \ a \ A\ and ps: \(ps, i) \ S\ \p on (ps, i)\ and qs: \(qs, i) \ S\ \Nom j on (qs, i)\ show \p at j in' S\ proof (rule ccontr) assume \\rs. (rs, j) \ S \ p on (rs, j)\ then obtain S' n where \A, n \ S'\ and S': \set S' \ {([p], j)} \ S\ and \([p], j) \. S'\ using \maximal A S\ unfolding maximal_def consistent_def by (metis insert_is_Un list.set_intros(1) on.simps subset_insert) then obtain S'' where S'': \set (([p], j) # S'') = set S'\ \([p], j) \ set S''\ using split_list[where x=\([p], j)\] by blast then have \A \ ([p], j) # S''\ - using inf fin ST_struct \A, n \ S'\ by blast + using inf fin STA_struct \A, n \ S'\ by blast then have \A \ ([p], j) # (ps, i) # (qs, i) # S''\ - using inf fin ST_struct[where branch'=\([_], _) # (ps, i) # (qs, i) # S''\] \A, n \ S'\ + using inf fin STA_struct[where branch'=\([_], _) # (ps, i) # (qs, i) # S''\] \A, n \ S'\ by fastforce then have \A \ ([], j) # (ps, i) # (qs, i) # S''\ using ps(2) qs(2) p by (meson Nom' in_mono list.set_intros(1) set_subset_Cons) moreover have \j \ branch_nominals ((ps, i) # (qs, i) # S'')\ using qs(2) unfolding branch_nominals_def by fastforce ultimately have \A \ (ps, i) # (qs, i) # S''\ using GoTo by fast moreover have \set ((ps, i) # (qs, i) # S'') \ S\ using S' S'' ps qs by auto ultimately show False using \consistent A S\ unfolding consistent_def by blast qed qed subsection \Result\ theorem completeness: fixes p :: \('a :: countable, 'b :: countable) fm\ assumes inf: \infinite (UNIV :: 'b set)\ and valid: \\(M :: ('b set, 'a) model) g w. M, g, w \ p\ shows \nominals p, 1 \ [([\<^bold>\ p], i)]\ proof - let ?A = \nominals p\ have \?A \ [([\<^bold>\ p], i)]\ proof (rule ccontr) assume \\ ?A \ [([\<^bold>\ p], i)]\ moreover have \finite ?A\ using finite_nominals by blast ultimately have *: \consistent ?A {([\<^bold>\ p], i)}\ - unfolding consistent_def using ST_struct inf + unfolding consistent_def using STA_struct inf by (metis empty_set list.simps(15)) let ?S = \Extend ?A {([\<^bold>\ p], i)} from_nat\ have \finite {([\<^bold>\ p], i)}\ by simp then have fin: \finite (\ (block_nominals ` {([\<^bold>\ p], i)}))\ using finite_nominals_set by blast have \consistent ?A ?S\ using consistent_Extend inf * fin \finite ?A\ by blast moreover have \maximal ?A ?S\ using maximal_Extend inf * fin by fastforce moreover have \saturated ?S\ using saturated_Extend inf * fin by fastforce - ultimately have \hintikka ?A ?S\ - using hintikka_Extend inf \finite ?A\ by blast + ultimately have \Hintikka ?A ?S\ + using Hintikka_Extend inf \finite ?A\ by blast moreover have \([\<^bold>\ p], i) \ ?S\ using Extend_mem by blast moreover have \(\<^bold>\ p) on ([\<^bold>\ p], i)\ by simp - moreover have \wf_allowed ?A ?S p\ - unfolding wf_allowed_def by simp ultimately have \\ Model (reach ?A ?S) (val ?S), assign ?A ?S, assign ?A ?S i \ p\ - using hintikka_model(2) by metis + using Hintikka_model(2) by fast then show False using valid by blast qed then show ?thesis - using ST_one by fast + using STA_one by fast qed text \ We arbitrarily fix nominal and propositional symbols to be natural numbers (any countably infinite type suffices) and define validity as truth in all models with sets of natural numbers as worlds. We show below that this implies validity for any type of worlds. \ abbreviation \valid p \ \(M :: (nat set, nat) model) (g :: nat \ _) w. M, g, w \ p\ text \ A formula is valid iff its negation has a closing tableau from a fresh world. We can assume a single unit of potential and take the allowed nominals to be the root nominals. \ theorem main: assumes \i \ nominals p\ shows \valid p \ nominals p, 1 \ [([\<^bold>\ p], i)]\ proof assume \valid p\ then show \nominals p, 1 \ [([\<^bold>\ p], i)]\ using completeness by blast next assume \nominals p, 1 \ [([\<^bold>\ p], i)]\ then show \valid p\ using assms soundness_fresh by fast qed text \The restricted validity implies validity in general.\ theorem valid_semantics: \valid p \ M, g, w \ p\ proof assume \valid p\ then have \i \ nominals p \ nominals p \ [([\<^bold>\ p], i)]\ for i using main by blast moreover have \\i. i \ nominals p\ by (simp add: finite_nominals ex_new_if_finite) ultimately show \M, g, w \ p\ using soundness_fresh by fast qed end