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,4395 +1,4820 @@ 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 \\ (\v \ R M (g i). g i = v)\ 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 and an opening nominal. The opening nominal is not necessarily in the list. A branch is a list of blocks. All blocks have an opening nominal; there is no possibility of an unnamed initial block. \ 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\ accounts for the opening nominal when checking if a formula is on a 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)\ -definition new :: \('a, 'b) fm \ 'b \ ('a, 'b) branch \ bool\ where - \new p a branch \ \ps. (ps, a) \. branch \ p on (ps, a)\ - 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)\ +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 number in front of the turnstile is the number of available coins to spend on GoTo. \ -inductive ST :: \('a, 'b) branch \ bool\ (\\ _\ [50] 50) where +inductive ST :: \nat \ ('a, 'b) branch \ bool\ (\_ \ _\ [50, 50] 50) where Close: \p at i in branch \ (\<^bold>\ p) at i in branch \ - \ branch\ + n \ branch\ | Neg: \(\<^bold>\ \<^bold>\ p) at a in (ps, a) # branch \ new p a ((ps, a) # branch) \ - \ (p # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ (p # ps, a) # branch \ + 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) \ - \ (p # ps, a) # branch \ \ (q # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ (p # ps, a) # branch \ Suc n \ (q # ps, a) # branch \ + 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) \ - \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch \ + n \ (ps, a) # branch\ | DiaP: \(\<^bold>\ p) at a in (ps, a) # branch \ i \ branch_nominals ((ps, a) # branch) \ \a. p = Nom a \ \ witnessed p a ((ps, a) # branch) \ - \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch \ + 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) \ - \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch \ + n \ (ps, a) # branch\ | SatP: \(\<^bold>@ a p) at b in (ps, a) # branch \ new p a ((ps, a) # branch) \ - \ (p # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ (p # ps, a) # branch \ + n \ (ps, a) # branch\ | SatN: \(\<^bold>\ (\<^bold>@ a p)) at b in (ps, a) # branch \ new (\<^bold>\ p) a ((ps, a) # branch) \ - \ ((\<^bold>\ p) # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ ((\<^bold>\ p) # ps, a) # branch \ + n \ (ps, a) # branch\ | GoTo: \i \ branch_nominals branch \ - \ ([], i) # branch \ - \ branch\ + n \ ([], i) # branch \ + Suc n \ branch\ | Nom: \p at b in (ps, a) # branch \ Nom i at b in (ps, a) # branch \ Nom i at a in (ps, a) # branch \ new p a ((ps, a) # branch) \ - \ (p # ps, a) # branch \ - \ (ps, a) # branch\ + Suc n \ (p # ps, a) # branch \ + n \ (ps, a) # branch\ + +abbreviation ST_ex :: \('a, 'b) branch \ bool\ (\\ _\ [50] 50) where + \\ branch \ \n. n \ branch\ + +lemma ST_Suc: \n \ branch \ Suc n \ branch\ + by (induct n branch rule: ST.induct) (simp_all add: ST.intros) text \A verified derivation in the calculus.\ lemma fixes i defines \p \ \<^bold>\ (\<^bold>@ i (Nom i))\ - shows \\ [([p], a)]\ + shows \Suc n \ [([p], a)]\ proof - have \i \ branch_nominals [([p], a)]\ unfolding p_def branch_nominals_def by simp - then have ?thesis if \\ [([], i), ([p], a)]\ + then have ?thesis if \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 \\ [([\<^bold>\ Nom i], i), ([p], a)]\ + ultimately have ?thesis if \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': \\ branch \ M, g \\<^sub>\ branch \ False\ +lemma soundness': \n \ branch \ M, g \\<^sub>\ branch \ False\ proof (induct branch arbitrary: g rule: ST.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 i g) have \M, g, g b \ p\ \M, g, g b \ Nom i\ using Nom(1-2, 7) by fastforce+ then have \M, g, g i \ p\ by simp moreover have \M, g, g a \ Nom i\ using Nom(3, 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 \\ branch\ + assumes \n \ branch\ shows \\block \ set branch. \p on block. \ M, g, w \ p\ using assms soundness' branch_sat by fast -corollary \\ \ []\ +corollary \\ n \ []\ using soundness by fastforce theorem soundness_fresh: - assumes \\ [([\<^bold>\ p], i)]\ \i \ nominals p\ + assumes \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 coins when we apply GoTo twice in a row. + Otherwise another rule will have been applied in-between that justifies the GoTo. + Therefore by avoiding detours we can close any closeable branch starting from 1 coin. +\ + +primrec nonempty :: \('a, 'b) block \ bool\ where + \nonempty (ps, i) = (ps \ [])\ + +lemma nonempty_Suc: + assumes + \n \ (ps, a) # filter nonempty left @ right\ + \q at a in (ps, a) # filter nonempty left @ right\ \q \ Nom a\ + shows \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 +qed + +lemma ST_nonempty: + \n \ left @ right \ Suc m \ filter nonempty left @ right\ +proof (induct n \left @ right\ arbitrary: left right rule: ST.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 +next + case (Neg p a ps branch n) + then show ?case + proof (cases left) + case Nil + then have \Suc m \ (p # ps, a) # branch\ + using Neg(4) by fastforce + then have \m \ (ps, a) # branch\ + using Neg(1-2) ST.Neg by fast + then show ?thesis + using Nil Neg(5) ST_Suc by auto + next + case (Cons _ left') + then have \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 \m \ (ps, a) # filter nonempty left' @ right\ + using ST.Neg by fast + then have \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 \Suc m \ (p # ps, a) # branch\ \Suc m \ (q # ps, a) # branch\ + using DisP(5, 7) by fastforce+ + then have \m \ (ps, a) # branch\ + using DisP(1-3) ST.DisP by fast + then show ?thesis + using Nil DisP(8) ST_Suc by auto + next + case (Cons _ left') + then have + \Suc m \ (p # ps, a) # filter nonempty left' @ right\ + \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 \m \ (ps, a) # filter nonempty left' @ right\ + using ST.DisP by fast + then have \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 \Suc m \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch\ + using DisN(4) by fastforce + then have \m \ (ps, a) # branch\ + using DisN(1-2) ST.DisN by fast + then show ?thesis + using Nil DisN(5) ST_Suc by auto + next + case (Cons _ left') + then have \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 \m \ (ps, a) # filter nonempty left' @ right\ + using ST.DisN by metis + then have \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 \Suc m \ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch\ + using DiaP(6) by fastforce + then have \m \ (ps, a) # branch\ + using DiaP(1-4) ST.DiaP by fast + then show ?thesis + using Nil DiaP(7) ST_Suc by auto + next + case (Cons _ left') + then have \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 \ 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 \m \ (ps, a) # filter nonempty left' @ right\ + using DiaP(3) ST.DiaP by fast + then have \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 \Suc m \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch\ + using DiaN(5) by fastforce + then have \m \ (ps, a) # branch\ + using DiaN(1-3) ST.DiaN by fast + then show ?thesis + using Nil DiaN(6) ST_Suc by auto + next + case (Cons _ left') + then have \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 \m \ (ps, a) # filter nonempty left' @ right\ + using ST.DiaN by fast + then have \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 \Suc m \ (p # ps, a) # branch\ + using SatP(4) by fastforce + then have \m \ (ps, a) # branch\ + using SatP(1-2) ST.SatP by fast + then show ?thesis + using Nil SatP(5) ST_Suc by auto + next + case (Cons _ left') + then have \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 *: \m \ (ps, a) # filter nonempty left' @ right\ + using ST.SatP by fast + then have \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 + 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 \Suc m \ ((\<^bold>\ p) # ps, a) # branch\ + using SatN(4) by fastforce + then have \m \ (ps, a) # branch\ + using SatN(1-2) ST.SatN by fast + then show ?thesis + using Nil SatN(5) ST_Suc by auto + next + case (Cons _ left') + then have \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 *: \m \ (ps, a) # filter nonempty left' @ right\ + using ST.SatN by fast + then have \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 + 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 i n) + then show ?case + proof (cases left) + case Nil + then have \Suc m \ (p # ps, a) # branch\ + using Nom(6) by fastforce + then have \m \ (ps, a) # branch\ + using Nom(1-4) ST.Nom by fast + then show ?thesis + using Nil Nom(7) ST_Suc by auto + next + case (Cons _ left') + then have \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\ + \Nom i at b in (ps, a) # filter nonempty left' @ right\ + \Nom i at a in (ps, a) # filter nonempty left' @ right\ + using Cons Nom(1-4, 7) unfolding new_def 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 *: \m \ (ps, a) # filter nonempty left' @ right\ + using ST.Nom by fast + then have \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)\ + proof (cases \i = a\) + case True + then have \Nom a at b in left' @ right\ + using \a \ b\ Nom(2, 7) Cons by auto + then show ?thesis + unfolding branch_nominals_def using \a \ b\ by fastforce + next + case False + then have \Nom i at a in left' @ right\ + using Nom(3, 7) Nil Cons by auto + then show ?thesis + unfolding branch_nominals_def using False by fastforce + qed + then show ?thesis + using * Nil GoTo by auto + next + case Cons + then show ?thesis + using * ST_Suc by auto + qed + then show ?thesis + using Cons Nom(7) by auto + qed +qed + +theorem ST_coins: \n \ branch \ Suc m \ branch\ + using ST_nonempty[where left=\[]\] by auto + +corollary ST_one: \n \ branch \ 1 \ branch\ + using ST_coins by auto + +subsection \Free GoTo\ + +text \The above result allows us to derive a version of GoTo that works "for free."\ + +lemma GoTo': + assumes \Suc n \ ([], i) # branch\ \i \ branch_nominals branch\ + shows \Suc n \ branch\ + using assms GoTo ST_coins by fast + section \Indexed Mapping\ text \This section contains some machinery for deriving 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 in 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 lemma Dup_opening: assumes \Dup p i branch xs\ \(v, v') \ xs\ \branch !. v = Some (ps, a)\ shows \i = a\ using assms unfolding Dup_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 \Dup p 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 Dup_opening by fast then have \omit (proj xs v) ps = ps\ using omit_id by auto ultimately show ?thesis by simp qed lemma 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 lemma omit_branch_mem_diff_formula: assumes \Dup 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) Dup_all_is v 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 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 omit_branch_mem_same_opening omit_branch_mem_diff_formula 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 Dup_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 Dup_list_nominals: assumes \all_is p ps xs\ shows \nominals p \ list_nominals (omit xs ps) = nominals p \ list_nominals ps\ using assms Dup_set by fastforce lemma Dup_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: Dup_list_nominals) lemma Dup_branch_nominals': assumes \Dup 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 Dup_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 Dup_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 * 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 Dup_branch_nominals' 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: - assumes \\ branch\ \Dup q i branch xs\ - shows \\ omit_branch xs branch\ + assumes \n \ branch\ \Dup q i branch xs\ + shows \n \ omit_branch xs branch\ using assms -proof (induct branch) - case (Close p i' branch) +proof (induct n branch) + case (Close p i' branch n) have \p at i' in omit_branch xs branch\ using Close(1, 3) omit_branch_mem by fast moreover have \(\<^bold>\ p) at i' in omit_branch xs branch\ using Close(2, 3) omit_branch_mem by fast ultimately show ?case using ST.Close by fast next - case (Neg p a ps branch) - have \\ omit_branch xs ((p # ps, a) # branch)\ + case (Neg p a ps branch n) + have \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 - \\ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ + \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) 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) next - case (DisP p q a ps branch) + case (DisP p q a ps branch n) have - \\ omit_branch xs ((p # ps, a) # branch)\ - \\ omit_branch xs ((q # ps, a) # branch)\ + \Suc n \ omit_branch xs ((p # ps, a) # branch)\ + \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 - \\ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ - \\ (q # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ + \Suc n \ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ + \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) 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) next - case (DisN p q a ps branch) - have \\ omit_branch xs (((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch)\ + case (DisN p q a ps branch n) + have \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 - \\ ((\<^bold>\ q) # (\<^bold>\ p) # omit (proj xs (length branch)) ps, 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) 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) next - case (DiaP p a ps branch i) - have \\ omit_branch xs (((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch)\ + case (DiaP p a ps branch i n) + have \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 - \\ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # omit (proj xs (length branch)) ps, 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) omit_branch_mem by fast moreover have \i \ 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) next - case (DiaN p a ps branch i) - have \\ omit_branch xs (((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch)\ + case (DiaN p a ps branch i n) + have \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 - \\ ((\<^bold>\ (\<^bold>@ i p)) # omit (proj xs (length branch)) ps, 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) omit_branch_mem by fast moreover have \(\<^bold>\ Nom i) at a in omit_branch xs ((ps, a) # branch)\ using DiaN(2, 6) 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) next - case (SatP a p b ps branch) - have \\ omit_branch xs ((p # ps, a) # branch)\ + case (SatP a p b ps branch n) + have \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 - \\ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ + \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) 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) next - case (SatN a p b ps branch) - have \\ omit_branch xs (((\<^bold>\ p) # ps, a) # branch)\ + case (SatN a p b ps branch n) + have \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 - \\ ((\<^bold>\ p) # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ + \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) 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) next - case (GoTo i branch) - then have \\ omit_branch xs (([], i) # branch)\ + case (GoTo i branch n) + then have \n \ omit_branch xs (([], i) # branch)\ using Dup_branch[where extra=\[([], i)]\] by fastforce - then have \\ ([], i) # omit_branch xs branch\ + then have \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) next - case (Nom p b ps a branch i') - have \\ omit_branch xs ((p # ps, a) # branch)\ + case (Nom p b ps a branch i' n) + have \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 - \\ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch\ + \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) omit_branch_mem by fast moreover have \Nom i' at b in omit_branch xs ((ps, a) # branch)\ using Nom(2, 7) omit_branch_mem by fast moreover have \Nom i' at a in omit_branch xs ((ps, a) # branch)\ using Nom(3, 7) 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 by (simp add: omit_branch_def ST.Nom) qed theorem Dup: - assumes \\ (p # ps, a) # branch\ \\ new p a ((ps, a) # branch)\ - shows \\ (ps, a) # branch\ + assumes \n \ (p # ps, a) # branch\ \\ new p a ((ps, a) # branch)\ + shows \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 \\ omit_branch ?xs ((p # ps, a) # branch)\ + then have \n \ omit_branch ?xs ((p # ps, a) # branch)\ using assms(1) ST_Dup by fast - then have \\ (omit (proj ?xs (length branch)) ps, a) # omit_branch ?xs branch\ + then have \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: \n \ branch \ m + n \ branch\ + using ST_Suc by (induct m) auto + +lemma ST_le: \n \ branch \ n \ m \ m \ branch\ + using ST_add by (metis le_add_diff_inverse2) + lemma Neg': assumes \(\<^bold>\ \<^bold>\ p) at a in (ps, a) # branch\ - \\ (p # ps, a) # branch\ - shows \\ (ps, a) # branch\ - using assms Neg Dup by metis + \n \ (p # ps, a) # branch\ + shows \n \ (ps, a) # branch\ + using assms Neg Dup ST_Suc by metis lemma DisP': assumes \(p \<^bold>\ q) at a in (ps, a) # branch\ - \\ (p # ps, a) # branch\ \\ (q # ps, a) # branch\ - shows \\ (ps, a) # branch\ - using assms DisP Dup by metis + \n \ (p # ps, a) # branch\ \n \ (q # ps, a) # branch\ + shows \n \ (ps, a) # branch\ +proof (cases \new p a ((ps, a) # branch) \ new q a ((ps, a) # branch)\) + case True + then show ?thesis + using assms DisP ST_Suc 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\ + \n \ (p # ps, a) # branch\ \m \ (q # ps, a) # branch\ + shows \max n m \ (ps, a) # branch\ +proof (cases \n \ m\) + case True + then have \m \ (p # ps, a) # branch\ + using assms(2) ST_le by blast + then show ?thesis + using assms True by (simp add: DisP' max.absorb2) +next + case False + then have \n \ (q # ps, a) # branch\ + using assms(3) ST_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\ - \\ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch\ - shows \\ (ps, a) # branch\ - using assms DisN Dup - by (metis (no_types, lifting) list.set_intros(1-2) new_def on.simps set_ConsD) + \n \ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a) # branch\ + shows \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 +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 DiaN': assumes \(\<^bold>\ (\<^bold>\ p)) at a in (ps, a) # branch\ \(\<^bold>\ Nom i) at a in (ps, a) # branch\ - \\ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch\ - shows \\ (ps, a) # branch\ - using assms DiaN Dup by metis + \n \ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch\ + shows \n \ (ps, a) # branch\ + using assms DiaN Dup ST_Suc by fast lemma SatP': assumes \(\<^bold>@ a p) at b in (ps, a) # branch\ - \\ (p # ps, a) # branch\ - shows \\ (ps, a) # branch\ - using assms SatP Dup by metis + \n \ (p # ps, a) # branch\ + shows \n \ (ps, a) # branch\ + using assms SatP Dup ST_Suc by fast lemma SatN': assumes \(\<^bold>\ (\<^bold>@ a p)) at b in (ps, a) # branch\ - \\ ((\<^bold>\ p) # ps, a) # branch\ - shows \\ (ps, a) # branch\ - using assms SatN Dup by metis + \n \ ((\<^bold>\ p) # ps, a) # branch\ + shows \n \ (ps, a) # branch\ + using assms SatN Dup ST_Suc by fast lemma Nom': assumes \p at b in (ps, a) # branch\ \Nom i at b in (ps, a) # branch\ \Nom i at a in (ps, a) # branch\ - \\ (p # ps, a) # branch\ - shows \\ (ps, a) # branch\ - using assms Nom Dup by metis + \n \ (p # ps, a) # branch\ + shows \n \ (ps, a) # branch\ + using assms Nom Dup ST_Suc by fast 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 -text \If a branch has a closing tableau then so does any branch obtained by renaming nominals.\ +text \ + If a branch has a closing tableau then so does any branch obtained by renaming nominals. + Since some formulas on the renamed branch may no longer be new, they do not contribute + any fuel and so we existentially quantify over the fuel needed to close the new branch. +\ lemma ST_sub': fixes f :: \'b \ 'c\ assumes \\(f :: 'b \ 'c) i A. finite A \ i \ A \ \j. j \ f ` A\ - shows \\ branch \ \ sub_branch f branch\ + shows \n \ branch \ \ sub_branch f branch\ proof (induct branch arbitrary: f rule: ST.induct) case (Close p i branch) 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 next - case (Neg p a ps branch) + case (Neg p a ps branch n) then have \\ (sub f p # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp - moreover have \sub f (\<^bold>\ \<^bold>\ p) at f a in (sub_list f ps, f a) # sub_branch f branch\ - using Neg(1) at_in_sub_branch by fast - ultimately show ?case - unfolding sub_branch_def by (simp add: Neg') + 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 \\ (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) + case (DisP p q a ps branch n) then have \\ (sub f p # sub_list f ps, f a) # sub_branch f branch\ \\ (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>\ q) at f a in (sub_list f ps, f a) # sub_branch f branch\ - using DisP(1) at_in_sub_branch by fast - ultimately show ?case - unfolding sub_branch_def by (simp add: DisP') + 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 \\ (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) + case (DisN p q a ps branch n) then have \\ ((\<^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 \sub f (\<^bold>\ (p \<^bold>\ q)) at f a in (sub_list f ps, f a) # sub_branch f branch\ - using DisN(1) at_in_sub_branch by fast - ultimately show ?case - unfolding sub_branch_def by (simp add: DisN') + 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 \\ (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) + case (DiaP p a ps branch i n) 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 \\ ((\<^bold>@ (?f i) (sub ?f p)) # (\<^bold>\ Nom (?f i)) # sub_list ?f ps, ?f a) # ?branch\ using DiaP(6)[where f=\?f\] unfolding sub_branch_def by simp then have \\ ((\<^bold>@ i' (sub f p)) # (\<^bold>\ Nom i') # sub_list f ps, f a) # sub_branch f branch\ using p ** by simp then have \\ ((\<^bold>\ Nom i') # sub_list f ps, f a) # sub_branch f branch\ using rs' by (meson Nom' on.simps) then have \\ (sub_list f ps, f a) # sub_branch f branch\ using ts by (meson Nom' on.simps) then show ?thesis - unfolding sub_branch_def by simp + unfolding sub_branch_def by auto next case False have \finite (branch_nominals ((ps, a) # branch))\ by (simp add: finite_branch_nominals) then obtain j where *: \j \ f ` branch_nominals ((ps, a) # branch)\ using DiaP(2) assms 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 \\ ((\<^bold>@ (?f i) (sub ?f p)) # (\<^bold>\ Nom (?f i)) # sub_list ?f ps, ?f a) # ?branch\ - using DiaP(6)[where f=\?f\] unfolding sub_branch_def by simp + using DiaP(6)[where f=\?f\] ST_Suc unfolding sub_branch_def 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 \?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 \\ (sub_list ?f ps, ?f a) # ?branch\ - using w ST.DiaP by fast + using w ST.DiaP ST_Suc by fast then show ?thesis using *** unfolding sub_branch_def by simp qed next - case (DiaN p a ps branch i) + case (DiaN p a ps branch i n) then have \\ ((\<^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 \sub f (\<^bold>\ (\<^bold>\ p)) at f a in (sub_list f ps, f a) # sub_branch f branch\ - using DiaN(1) at_in_sub_branch by fast - moreover have \sub f (\<^bold>\ Nom i) at f a in (sub_list f ps, f a) # sub_branch f branch\ - using DiaN(2) at_in_sub_branch by fast - ultimately show ?case - unfolding sub_branch_def by (simp add: DiaN') + 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 \\ (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) + case (SatP a p b ps branch n) then have \\ (sub f p # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp - moreover have \sub f (\<^bold>@ a p) at f b in (sub_list f ps, f a) # sub_branch f branch\ - using SatP(1) at_in_sub_branch by fast - ultimately show ?case - unfolding sub_branch_def by (simp add: SatP') + 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 \\ (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) + case (SatN a p b ps branch n) then have \\ ((\<^bold>\ sub f p) # sub_list f ps, f a) # sub_branch f branch\ unfolding sub_branch_def by simp - moreover have \sub f (\<^bold>\ (\<^bold>@ a p)) at f b in (sub_list f ps, f a) # sub_branch f branch\ - using SatN(1) at_in_sub_branch by fast - ultimately show ?case - unfolding sub_branch_def by (simp add: SatN') + 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 \\ (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) + case (GoTo i branch n) then have \\ ([], 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 - then have \f i \ branch_nominals (sub_branch f branch)\ - unfolding sub_branch_def by simp ultimately show ?case - by (simp add: ST.GoTo sub_branch_def) + using ST.GoTo by fast next - case (Nom p b ps a branch i) + case (Nom p b ps a branch i n) then have \\ (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 \sub f (Nom i) at f b in (sub_list f ps, f a) # sub_branch f branch\ - using Nom(2) at_in_sub_branch by fast - moreover have \sub f (Nom i) at f a in (sub_list f ps, f a) # sub_branch f branch\ - using Nom(3) at_in_sub_branch by fast - ultimately show ?case - unfolding sub_branch_def by (simp add: Nom') + moreover have \Nom (f i) 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 \Nom (f i) at f a in (sub_list f ps, f a) # sub_branch f branch\ + using Nom(3) at_in_sub_branch by (metis (no_types, hide_lams) sub.simps(2)) + ultimately have \\ (sub_list f ps, f a) # sub_branch f branch\ + using Nom' by fast + 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 -lemma ST_sub_gt: +corollary ST_sub_gt: fixes f :: \'b \ 'c\ assumes \\g :: 'c \ 'b. surj g\ \\ branch\ shows \\ sub_branch f branch\ using assms ex_fresh_gt ST_sub' by metis -lemma ST_sub_inf: +corollary ST_sub_inf: fixes f :: \'b \ 'c\ - assumes \infinite (UNIV :: 'c set)\ \\ branch\ + assumes \infinite (UNIV :: 'c set)\ \n \ branch\ shows \\ 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 qed -lemma ST_sub: +corollary ST_sub: fixes f :: \'b \ 'b\ assumes \\ branch\ shows \\ 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 qed subsection \Unrestricted \(\<^bold>\)\ rule\ lemma DiaP': assumes \(\<^bold>\ p) at a in (ps, a) # branch\ + \\a. p = Nom a\ \i \ branch_nominals ((ps, a) # branch)\ \\ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch\ - \\a. p = Nom a\ \i \ branch_nominals ((ps, a) # branch)\ shows \\ (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 \\ sub_branch ?f (((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # branch)\ - using assms(2) ST_sub by blast + using assms(4) ST_sub by blast then have \\ ((\<^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-2, 4) unfolding branch_nominals_def by fastforce+ + 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 \\ ((\<^bold>@ i' p) # (\<^bold>\ Nom i') # ps, a) # branch\ by simp then have \\ ((\<^bold>\ Nom i') # ps, a) # branch\ using rs' by (meson Nom' on.simps) then show ?thesis using ts by (meson Nom' on.simps) next case False then show ?thesis - using assms DiaP by fast + using assms DiaP ST_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: - assumes \set ps \ set qs\ \(qs, a) \. branch\ \\ (ps @ ps', a) # branch\ - shows \\ (ps', a) # branch\ + assumes \set ps \ set qs\ \(qs, a) \. branch\ \n \ (ps @ ps', a) # branch\ + shows \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 Nom' list.set_intros(2) on.simps) qed qed text \We can drop a block if it is subsumed by another block.\ lemma ST_drop_block: assumes \set ps \ set ps'\ \(ps', a) \. branch\ - \\ (ps, a) # branch\ - shows \\ branch\ + \n \ (ps, a) # branch\ + shows \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) # (qs, b) # branch\ + then have \n \ ([], a) # (qs, b) # branch\ using Cons(2-4) ST_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 \\ (qs, b) # branch\ + ultimately have \Suc n \ (qs, b) # branch\ by (simp add: GoTo) then show ?thesis using Pair Dup by fast qed qed lemma ST_drop_block': - assumes \\ (ps, a) # branch\ \(ps, a) \. branch\ - shows \\ branch\ + assumes \n \ (ps, a) # branch\ \(ps, a) \. branch\ + shows \Suc n \ branch\ using assms ST_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: fixes branch :: \('a, 'b) branch\ assumes inf: \infinite (UNIV :: 'b set)\ and - \\ branch\ \set branch \ set branch'\ + \n \ branch\ \set branch \ set branch'\ shows \\ branch'\ using assms(2-3) -proof (induct branch arbitrary: branch' rule: ST.induct) +proof (induct n branch arbitrary: branch' rule: ST.induct) case (Close p i branch) then show ?case using ST.Close by fast next - case (Neg p a ps branch) + case (Neg p a ps branch n) have \\ (p # ps, a) # branch'\ using Neg(4-5) 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 \\ (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 next case (DisP p q a ps branch) have \\ (p # ps, a) # branch'\ \\ (q # ps, a) # branch'\ using DisP(5, 7-8) 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 \\ (ps, a) # branch'\ - using DisP' by fast + using DisP'' by fast moreover have \(ps, a) \. branch'\ using DisP(8) by simp ultimately show ?case using ST_drop_block' by fast next - case (DisN p q a ps branch) + case (DisN p q a ps branch n) have \\ ((\<^bold>\ q) # (\<^bold>\ p) # ps, a)# branch'\ using DisN(4-5) 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 \\ (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 next - case (DiaP p a ps branch i) + case (DiaP p a ps branch i n) have \finite (branch_nominals branch')\ by (simp add: finite_branch_nominals) then obtain j where j: \j \ 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 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 metis ultimately have i: \i \ branch_nominals ((ps, a) # ?branch')\ unfolding branch_nominals_def by simp have \\ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ps, a) # ?branch'\ - using DiaP(6) * by (simp add: subset_code(1)) + 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 \\ (ps, a) # ?branch'\ - using inf DiaP(3) i by (simp add: DiaP') + using inf DiaP(3) i DiaP' by metis then have \\ sub_branch ?f ((ps, a) # ?branch')\ using ST_sub by blast then have \\ (ps, a) # branch'\ using 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 next - case (DiaN p a ps branch i) + case (DiaN p a ps branch i n) have \\ ((\<^bold>\ (\<^bold>@ i p)) # ps, a) # branch'\ using DiaN(5-6) 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 \\ (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 next - case (SatP a p b ps branch) + case (SatP a p b ps branch n) have \\ (p # ps, a) # branch'\ using SatP(4-5) 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 \\ (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 next - case (SatN a p b ps branch) - have \\ ((\<^bold>\ p) # ps, a) # branch'\ + case (SatN a p b ps branch n) + have\\ ((\<^bold>\ p) # ps, a) # branch'\ using SatN(4-5) 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 \\ (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 next - case (GoTo i branch) + case (GoTo i branch n) then have \\ ([], 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) by (simp add: ST.GoTo) + using GoTo(2) ST.GoTo by fast next - case (Nom p b ps a branch i) + case (Nom p b ps a branch i n) have \\ (p # ps, a) # branch'\ using Nom(6-7) by (simp add: subset_code(1)) moreover have \p at b in (ps, a) # branch'\ using Nom(1, 7) by auto moreover have \Nom i at b in (ps, a) # branch'\ using Nom(2, 7) by auto moreover have \Nom i at a in (ps, a) # branch'\ using Nom(3, 7) by auto ultimately have \\ (ps, a) # branch'\ using Nom' by fast moreover have \(ps, a) \. branch'\ using Nom(7) by simp ultimately show ?case using ST_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: fixes branch :: \('a, 'b) branch\ assumes inf: \infinite (UNIV :: 'b set)\ and - \\ (ps, a) # branch\ \set ps \ set ps'\ + \n \ (ps, a) # branch\ \set ps \ set ps'\ shows \\ (ps', a) # branch\ using assms(2-3) proof (induct \(ps, a) # branch\ arbitrary: ps ps' rule: ST.induct) - case (Close p i ts ts') + 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 next - case (Neg p ps) + case (Neg p ps n) then have \(\<^bold>\ \<^bold>\ p) at a in (ps', a) # branch\ by auto moreover have \\ (p # ps', a) # branch\ using Neg(4-5) by (simp add: subset_code(1)) ultimately show ?case using Neg' by fast next - case (DisP p q ps) + case (DisP p q ps n) then have \(p \<^bold>\ q) at a in (ps', a) # branch\ by auto moreover have \\ (p # ps', a) # branch\ \\ (q # ps', a) # branch\ using DisP(5, 7-8) by (simp_all add: subset_code(1)) ultimately show ?case - using DisP' by fast + using DisP'' by fast next - case (DisN p q ps) + case (DisN p q ps n) then have \(\<^bold>\ (p \<^bold>\ q)) at a in (ps', a) # branch\ by auto moreover have \\ ((\<^bold>\ q) # (\<^bold>\ p) # ps', a) # branch\ using DisN(4-5) by (simp add: subset_code(1)) ultimately show ?case using DisN' by fast next - case (DiaP p ps i) + case (DiaP p ps i n) have \finite (branch_nominals ((ps', a) # branch))\ using finite_branch_nominals by blast then obtain j where j: \j \ 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 \(\<^bold>\ p) at a in (?ps', a) # branch\ using DiaP(1) * by fastforce moreover have \\ ((\<^bold>@ i p) # (\<^bold>\ Nom i) # ?ps', a) # branch\ using * DiaP(6) by (simp add: subset_code(1)) moreover have \i \ branch_nominals ((?ps', a) # branch)\ using DiaP(2) \i \ block_nominals (?ps', a)\ unfolding branch_nominals_def by simp ultimately have \\ (?ps', a) # branch\ using DiaP(3) DiaP' by fast then have \\ sub_branch ?f ((?ps', a) # branch)\ using ST_sub by blast then have \\ (sub_list ?f ?ps', ?f a) # sub_branch ?f branch\ unfolding sub_branch_def by simp then show ?case using \?f a = a\ ps' branch by simp next - case (DiaN p ps i) + 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 \\ ((\<^bold>\ (\<^bold>@ i p)) # ps', a) # branch\ using DiaN(5-6) by (simp add: subset_code(1)) ultimately show ?case using DiaN' by fast next - case (SatP p b ps) + case (SatP p b ps n) then have \(\<^bold>@ a p) at b in (ps', a) # branch\ by auto moreover have \\ (p # ps', a) # branch\ using SatP(4-5) by (simp add: subset_code(1)) ultimately show ?case using SatP' by fast next - case (SatN p b ps) + case (SatN p b ps n) then have \(\<^bold>\ (\<^bold>@ a p)) at b in (ps', a) # branch\ by auto moreover have \\ ((\<^bold>\ p) # ps', a) # branch\ using SatN(4-5) by (simp add: subset_code(1)) ultimately show ?case using SatN' by fast next - case (GoTo i ps) - then have \\ (ps, a) # branch\ + case (GoTo i n ps) + then have \Suc n \ (ps, a) # branch\ using ST.GoTo by fast - then have \\ (ps, a) # (ps', a) # branch\ + then obtain m where \m \ (ps, a) # (ps', a) # branch\ using inf ST_struct[where branch'=\(ps, a) # _ # _\] by fastforce + then have \Suc m \ (ps', a) # branch\ + using GoTo(4) by (simp add: ST_drop_block[where a=a]) then show ?case - using GoTo(4) by (simp add: ST_drop_block[where a=a]) + by blast next case (Nom p b ps i) have \p at b in (ps', a) # branch\ using Nom(1, 7) by auto moreover have \Nom i at b in (ps', a) # branch\ using Nom(2, 7) by auto moreover have \Nom i at a in (ps', a) # branch\ using Nom(3, 7) by auto moreover have \\ (p # ps', a) # branch\ using Nom(6-7) by (simp add: subset_code(1)) ultimately show ?case using Nom' by fast qed section \Unrestricted \(\<^bold>@)\ and \(\<^bold>\ \<^bold>@)\ rules\ text \We can derive more general versions of the \(\<^bold>@)\ and \(\<^bold>\ \<^bold>@)\ rules using weakening and \Nom\.\ lemma SatP'': fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \(\<^bold>@ i p) at b in (ps, a) # branch\ \Nom i at a in (ps, a) # branch\ \\ (p # ps, a) # branch\ shows \\ (ps, a) # branch\ proof - have \i \ branch_nominals ((ps, a) # branch)\ using assms(2) unfolding branch_nominals_def by fastforce then have ?thesis if \\ ([], i) # (ps, a) # branch\ - using that by (simp add: GoTo) + using that GoTo by fast then have ?thesis if \\ ([Nom a], i) # (ps, a) # branch\ using that assms(3) by (meson Nom' list.set_intros(1) on.simps set_subset_Cons subsetD) then have ?thesis if \\ ([p, Nom a], i) # (ps, a) # branch\ using that assms(2) by (meson SatP' set_subset_Cons subsetD) then have ?thesis if \\ (ps, a) # ([p, Nom a], i) # branch\ - using that inf ST_struct[where branch'=\_ # _ # _\] by fastforce + using that inf ST_struct[where branch'=\([p, Nom a], i) # (ps, a) # branch\] by fastforce then have ?thesis if \\ (p # ps, a) # ([p, Nom a], i) # branch\ using that by (meson Nom' list.set_intros(1) on.simps set_subset_Cons subsetD) then show ?thesis - using inf assms(4) ST_struct[where branch'=\_ # ([_, _], _) # _\] by fastforce + using inf assms(4) ST_struct[where branch'=\(p # ps, a) # ([p, Nom a], i) # branch\] + by fastforce qed lemma SatN'': fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \(\<^bold>\ (\<^bold>@ i p)) at b in (ps, a) # branch\ \Nom i at a in (ps, a) # branch\ \\ ((\<^bold>\ p) # ps, a) # branch\ shows \\ (ps, a) # branch\ proof - have \i \ branch_nominals ((ps, a) # branch)\ using assms(2) unfolding branch_nominals_def by fastforce then have ?thesis if \\ ([], i) # (ps, a) # branch\ - using that by (simp add: GoTo) + using that GoTo by fast then have ?thesis if \\ ([Nom a], i) # (ps, a) # branch\ using that assms(3) by (meson Nom' list.set_intros(1) on.simps set_subset_Cons subsetD) then have ?thesis if \\ ([\<^bold>\ p, Nom a], i) # (ps, a) # branch\ using that assms(2) by (meson SatN' set_subset_Cons subsetD) then have ?thesis if \\ (ps, a) # ([\<^bold>\ p, Nom a], i) # branch\ - using that inf ST_struct[where branch'=\_ # _ # _\] by fastforce + using that inf ST_struct[where branch'=\([\<^bold>\ p, Nom a], i) # (ps, a) # branch\] by fastforce then have ?thesis if \\ ((\<^bold>\ p) # ps, a) # ([\<^bold>\ p, Nom a], i) # branch\ using that by (meson Nom' list.set_intros(1) on.simps set_subset_Cons subsetD) then show ?thesis - using inf assms(4) ST_struct[where branch'=\_ # ([_, _], _) # _\] by fastforce + using inf assms(4) ST_struct[where branch'=\((\<^bold>\ p) # ps, a) # ([\<^bold>\ p, Nom a], i) # branch\] + by fastforce qed section \Bridge\ text \ We are going to 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 will 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 derive the Bridge rule. \ 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 j at a in branch\ \Nom k at a in branch\ shows \branch_nominals (mapi_branch (bridge k j xs) branch) = branch_nominals branch\ proof - let ?f = \bridge k j xs\ have \Nom j at a in mapi_branch ?f branch\ using assms(1) nom_at_in_bridge by fast then have \j \ branch_nominals (mapi_branch ?f branch)\ unfolding branch_nominals_def by fastforce moreover have \Nom k at a in mapi_branch ?f branch\ using assms(2) nom_at_in_bridge by fast then have \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(1-2) 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 j at b in branch \ Nom j at a 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 j) then have \(extra @ branch) !. v = Some (qs, a)\ \(extra @ branch) !. w = Some (rs, b)\ using rev_nth_append by fast+ moreover have \Nom j at b in (extra @ branch)\ \Nom j at a in (extra @ branch)\ using Copied(8-9) by auto ultimately show ?case using Copied(2-4, 5-7, 9) 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 j) 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 j at b in (ps' @ ps, a) # branch\ using Copied(8) by fastforce moreover have \Nom j at a' in (ps' @ ps, a) # branch\ using Copied(9) 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': fixes a :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and - \\ (ps, a) # branch\ + \n \ (ps, a) # branch\ \descendants k i ((ps, a) # branch) xs\ \Nom j at c in branch\ \Nom k at c in branch\ shows \\ mapi_branch (bridge k j xs) ((ps, a) # branch)\ using assms(2-) -proof (induct \(ps, a) # branch\ arbitrary: ps a branch xs rule: ST.induct) +proof (induct n \(ps, a) # branch\ arbitrary: ps a branch xs rule: ST.induct) case (Close p i') 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 j: \Nom j at c in ?branch\ using Close(4) nom_at_in_bridge unfolding mapi_branch_def by fastforce have k: \Nom k at c in ?branch\ using Close(5) 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 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 \\ ([], i') # ?branch\ - using that by (simp add: GoTo) + 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 \\ ([\<^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 \\ ([], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ - using that by (simp add: GoTo) - moreover have - \Nom j at c in ([], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ - \Nom k at c in ([], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ - using j k by auto + using that GoTo by fast + moreover have \Nom j at c in ([], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ + using j by auto + moreover have \Nom k at c in ([], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ + using k by auto ultimately have ?thesis if \\ ([Nom k], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ using that by (meson Nom' list.set_intros(1) on.simps) moreover have \(\<^bold>\ (\<^bold>@ j (Nom k))) at i' in ([Nom k], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ by fastforce ultimately have ?thesis if \\ ([\<^bold>\ Nom k, 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, Nom k], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ by fastforce moreover have \(\<^bold>\ Nom k) at j in ([\<^bold>\ Nom k, Nom k], j) # ([\<^bold>\ (\<^bold>@ j (Nom k))], i') # ?branch\ by fastforce ultimately show ?thesis using ST.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 \\ ([], i') # ?branch\ - using that by (simp add: GoTo) + using that GoTo by fast moreover have \(mapi (?f w) rs, i') \. ([], i') # ?branch\ using w by simp ultimately have ?thesis if \\ ([\<^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 j by fastforce ultimately have ?thesis if \\ ([], j) # ([\<^bold>@ k r], i') # ?branch\ - using that j by (simp add: GoTo) + using that j GoTo by fast moreover have \Nom j at c in ([], j) # ([\<^bold>@ k r], i') # ?branch\ \Nom k at c in ([], j) # ([\<^bold>@ k r], i') # ?branch\ using j k by auto ultimately have ?thesis if \\ ([Nom k], j) # ([\<^bold>@ k r], i') # ?branch\ using that by (meson Nom' list.set_intros(1) on.simps) then have ?thesis if \\ ([r, Nom k], j) # ([\<^bold>@ k r], i') # ?branch\ using that inf by (meson SatP'' list.set_intros(1) list.set_intros(2) on.simps) moreover have \(mapi (?f v) qs, i') \. ([r, Nom k], j) # ([\<^bold>@ k r], i') # ?branch\ using v by simp ultimately have ?thesis if \\ ([\<^bold>\ r, r, Nom k], j) # ([\<^bold>@ k r], i') # ?branch\ using that *(1) by (meson SatN') moreover have \r at j in ([\<^bold>\ r, r, Nom k], j) # ([\<^bold>@ k r], i') # ?branch\ by fastforce moreover have \(\<^bold>\ r) at j in ([\<^bold>\ r, r, Nom k], j) # ([\<^bold>@ k r], i') # ?branch\ by fastforce ultimately show ?thesis using ST.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 j by fastforce then have ?thesis if \\ ([], j) # ?branch\ - using that by (simp add: GoTo) + using that GoTo by fast moreover have \Nom j at c in ([], j) # ?branch\ \Nom k at c in ([], j) # ?branch\ using j k by auto ultimately have ?thesis if \\ ([Nom k], j) # ?branch\ using that by (meson Nom' list.set_intros(1) on.simps) moreover have \(mapi (?f v) qs, i') \. ([Nom k], j) # ?branch\ using v by simp ultimately have ?thesis if \\ ([r, Nom k], j) # ?branch\ using that *(1) inf by (meson SatP'' list.set_intros(1) on.simps) moreover have \(mapi (?f w) rs, i') \. ([r, Nom k], j) # ?branch\ using w by simp ultimately have ?thesis if \\ ([\<^bold>\ r, r, Nom k], j) # ?branch\ using that *(2) by (meson SatN') moreover have \r at j in ([\<^bold>\ r, r, Nom k], j) # ?branch\ by fastforce moreover have \(\<^bold>\ r) at j in ([\<^bold>\ r, r, Nom k], j) # ?branch\ by fastforce ultimately show ?thesis using ST.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 qed qed next case (Neg p a ps branch) 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 \\ 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 \\ (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 show ?case - unfolding mapi_branch_def by (simp add: Neg') + ultimately have \\ (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) 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 \\ mapi_branch ?f ((p # ps, a) # branch)\ \\ 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 \\ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ \\ (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 show ?case - unfolding mapi_branch_def by (simp add: DisP') + ultimately have \\ (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) 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 \\ 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 \\ ((\<^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 show ?case - unfolding mapi_branch_def by (simp add: DisN') + ultimately have \\ (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') 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' \ 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 \descendants k i (((\<^bold>@ i' p) # (\<^bold>\ Nom i') # ps, a) # branch) xs\ using DiaP(7) descendants_block[where ps'=\[_, _]\] by fastforce then have \\ mapi_branch ?f (((\<^bold>@ i' p) # (\<^bold>\ Nom i') # ps, a) # branch)\ using DiaP(4-) by blast - then have \\ ((\<^bold>@ i' p) # (\<^bold>\ Nom i') # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ + then have \\ ((\<^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 \\ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ - using i' DiaP(3) by (simp add: DiaP') + using i' DiaP(3) DiaP' by fast then show ?case unfolding mapi_branch_def by simp next case (DiaN p a ps branch i') 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 \\ mapi_branch ?f (((\<^bold>\ (\<^bold>@ k p)) # ps, a) # branch)\ using \i' = k\ DiaN(5-) by blast then have \\ ((\<^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 \\ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ by (meson DiaN') then have \\ (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 \\ 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 \\ ((\<^bold>\ (\<^bold>@ i' p)) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ + ultimately have \\ ((\<^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 \\ (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) 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 \\ 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 \\ (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 show ?case - unfolding mapi_branch_def by (simp add: SatP') + ultimately have \\ (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) 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 \\ 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 \\ ((\<^bold>\ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def using \a = k\ by simp then have *: \\ ((\<^bold>\ p) # Nom j # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using inf ST_struct_block[where ps'=\(\<^bold>\ p) # Nom j # _\] by fastforce 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>@ 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 obtain qs' where \(qs', b) \. (Nom j # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ \(\<^bold>\ (\<^bold>@ j p)) on (qs', b)\ by fastforce then have \\ (Nom j # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using * inf by (meson SatN'' list.set_intros(1) on.simps) moreover have \Nom j at c in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using SatN(6) nom_at_in_bridge unfolding mapi_branch_def by fastforce moreover have \Nom k at c in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using SatN(7) nom_at_in_bridge unfolding mapi_branch_def by fastforce ultimately have \\ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using \a = k\ by (meson Nom' list.set_intros(1) on.simps) then show ?thesis unfolding mapi_branch_def by simp 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 \\ 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 \\ ((\<^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 \\ (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' ps a branch) + 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 \\ mapi_branch ?f (([], i') # (ps, a) # branch)\ using GoTo(3, 5-) by auto then have \\ ([], 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 next case (Nom p b ps a branch i') 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 \\ 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 \\ (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 i' at b in mapi_branch ?f ((ps, a) # branch)\ using Nom(2) True nom_at_in_bridge by fast then have \Nom i' at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \Nom i' at a in mapi_branch ?f ((ps, a) # branch)\ using Nom(3) True nom_at_in_bridge by fast then have \Nom i' at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp ultimately have \\ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using Nom' by fast 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 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 i' 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 moreover have \Nom i' at a in (p # ps, a) # branch\ using Nom(3) by fastforce ultimately have \descendants k i ((p # ps, a) # branch) ?xs\ using True Copied by fast then have \\ mapi_branch ?f ((p # ps, a) # branch)\ using Nom(6-) by blast then have \\ (?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 i' at b in mapi_branch ?f ((ps, a) # branch)\ using Nom(2) nom_at_in_bridge by fast then have \Nom i' at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \Nom i' at a in mapi_branch ?f ((ps, a) # branch)\ using Nom(3) nom_at_in_bridge by fast then have \Nom i' at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp ultimately have \\ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using Nom' by fast then have \\ (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 \\ 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 \\ (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 i' at b in mapi_branch ?f ((ps, a) # branch)\ using Nom(2) nom_at_in_bridge by fast then have \Nom i' at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp moreover have \Nom i' at a in mapi_branch ?f ((ps, a) # branch)\ using Nom(3) nom_at_in_bridge by fast then have \Nom i' at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ unfolding mapi_branch_def by simp ultimately have \\ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch\ using Nom' by fast then show ?thesis unfolding mapi_branch_def by simp qed qed qed lemma ST_bridge: fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \\ branch\ \descendants k i branch xs\ \Nom j at c in branch\ \Nom k at c in branch\ shows \\ mapi_branch (bridge k j xs) branch\ proof - have \\ ([], j) # branch\ using inf assms(2) ST_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 \\ mapi_branch (bridge k j xs) (([], j) # branch)\ using ST_bridge' inf assms(3-) by fast then have *: \\ ([], 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 * by (simp add: GoTo) + using * GoTo by fast qed subsection \Derivation\ theorem Bridge: fixes i :: 'b assumes inf: \infinite (UNIV :: 'b set)\ and \Nom i at b in branch\ \(\<^bold>\ Nom j) at b in branch\ \Nom i at a in branch\ \Nom j at c in branch\ \Nom k at c in branch\ \\ ((\<^bold>\ Nom k) # ps, a) # branch\ shows \\ (ps, a) # branch\ proof - let ?xs = \{(length branch, length ps)}\ have \descendants k a (((\<^bold>\ Nom k) # ps, a) # branch) ?xs\ using Initial by force moreover have \Nom j at c in ((\<^bold>\ Nom k) # ps, a) # branch\ \Nom k at c in ((\<^bold>\ Nom k) # ps, a) # branch\ using assms(5-6) by auto ultimately have \\ mapi_branch (bridge k j ?xs) (((\<^bold>\ Nom k) # ps, a) # branch)\ using ST_bridge inf assms(7) by fast then have \\ ((\<^bold>\ Nom j) # mapi (bridge k j ?xs (length branch)) ps, a) # 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 \\ ((\<^bold>\ Nom j) # ps, a) # branch\ using mapi_block_id[where ps=ps] mapi_branch_id[where branch=branch] by simp then show ?thesis using assms(2-5) by (meson Nom' set_subset_Cons subsetD) 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)\ + text \ A set of blocks is Hintikka if it satisfies the following requirements. Intuitively, if it corresponds to an exhausted open branch. \ definition hintikka :: \('a, 'b) block set \ bool\ where \hintikka H \ - ((\x i j. (\ps. (ps, i) \ H \ Nom j on (ps, i)) \ (\qs. (qs, j) \ H \ Pro x on (qs, j)) \ - (\rs. (rs, i) \ H \ (\<^bold>\ Pro x) on (rs, i))) \ - (\a i. (\ps. (ps, i) \ H \ Nom a on (ps, i)) \ (\qs. (qs, i) \ H \ (\<^bold>\ Nom a) on (qs, i))) \ - (\i j. (\ps. (ps, i) \ H \ (\<^bold>\ Nom j) on (ps, i)) \ - (\qs. (qs, i) \ H \ (\<^bold>\ (\<^bold>\ Nom j)) on (qs, i))) \ - (\p i. i \ nominals p \ (\block \ H. p on block) \ (\qs. (qs, i) \ H)) \ - (\i j. (\ps. (ps, i) \ H \ Nom j on (ps, i)) \ (\qs. (qs, j) \ H \ Nom i on (qs, j))) \ - (\i j k. (\ps. (ps, i) \ H \ Nom j on (ps, i)) \ (\qs. (qs, j) \ H \ Nom k on (qs, j)) \ - (\rs. (rs, i) \ H \ Nom k on (rs, i))) \ - (\i j k. (\ps. (ps, i) \ H \ (\<^bold>\ Nom j) on (ps, i)) \ - (\qs. (qs, j) \ H \ Nom k on (qs, j)) \ (\rs. (rs, i) \ H \ (\<^bold>\ Nom k) on (rs, i))) \ - (\i j k. (\ps. (ps, i) \ H \ (\<^bold>\ Nom j) on (ps, i)) \ - (\qs. (qs, i) \ H \ Nom k on (qs, i)) \ (\rs. (rs, k) \ H \ (\<^bold>\ Nom j) on (rs, k))) \ - (\p q i. (\ps. (ps, i) \ H \ (p \<^bold>\ q) on (ps, i)) \ - (\qs. (qs, i) \ H \ (p on (qs, i) \ q on (qs, i)))) \ - (\p q i. (\ps. (ps, i) \ H \ (\<^bold>\ (p \<^bold>\ q)) on (ps, i)) \ - (\qs. (qs, i) \ H \ (\<^bold>\ p) on (qs, i) \ (\<^bold>\ q) on (qs, i))) \ - (\p i. (\ps. (ps, i) \ H \ (\<^bold>\ \<^bold>\ p) on (ps, i)) \ (\qs. (qs, i) \ H \ p on (qs, i))) \ - (\p i. (\block \ H. (\<^bold>@ i p) on block) \ (\qs. (qs, i) \ H \ p on (qs, i))) \ - (\p i. (\block \ H. (\<^bold>\ (\<^bold>@ i p)) on block) \ (\qs. (qs, i) \ H \ (\<^bold>\ p) on (qs, i))) \ - (\p i. (\a. p = Nom a) \ (\ps. (ps, i) \ H \ (\<^bold>\ p) on (ps, i)) \ - (\j. (\qs. (qs, i) \ H \ (\<^bold>\ Nom j) on (qs, i)) \ (\rs. (rs, i) \ H \ (\<^bold>@ j p) on (rs, i)))) \ - (\p i j. (\ps. (ps, i) \ H \ (\<^bold>\ (\<^bold>\ p)) on (ps, i)) \ - (\qs. (qs, i) \ H \ (\<^bold>\ Nom j) on (qs, i)) \ - (\rs. (rs, i) \ H \ (\<^bold>\ (\<^bold>@ j p)) on (rs, i))))\ + (\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. Nom j at i in' H \ + Nom i at j in' H) \ + (\i j k. Nom j at i in' H \ Nom k at j in' H \ + Nom k at i in' H) \ + (\i j k. (\<^bold>\ Nom j) at i in' H \ Nom k at j in' H \ + (\<^bold>\ Nom k) at i in' H) \ + (\i j k. (\<^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)\ 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 shown to be an equivalence relation. \ definition hequiv :: \('a, 'b) block set \ 'b \ 'b \ bool\ where - \hequiv H i j \ \ps. (ps, i) \ H \ Nom j on (ps, i)\ + \hequiv H i j \ Nom j at i in' H\ abbreviation hequiv_rel :: \('a, 'b) block set \ ('b \ 'b) set\ where \hequiv_rel H \ {(i, j) |i j. hequiv H i j}\ definition names :: \('a, 'b) block set \ 'b set\ where - \names H \ {i |block i. (block, i) \ H}\ + \names H \ {i |ps i. (ps, i) \ H}\ lemma hequiv_refl: \hintikka H \ i \ names H \ hequiv H i i\ unfolding hintikka_def hequiv_def names_def by auto lemma hequiv_refl': \hintikka H \ (ps, i) \ H \ hequiv H i i\ using hequiv_refl unfolding names_def by fast lemma hequiv_sym: \hintikka H \ hequiv H i j = hequiv H j i\ unfolding hintikka_def hequiv_def by meson lemma hequiv_trans: \hintikka H \ hequiv H i j \ hequiv H j k \ hequiv H i k\ unfolding hintikka_def hequiv_def by meson lemma hequiv_names: \hequiv H i j \ i \ names H\ unfolding hequiv_def names_def by blast lemma hequiv_names_rel: \hintikka H \ hequiv_rel H \ names H \ names H\ using hequiv_sym hequiv_names by fast lemma hequiv_refl_rel: \hintikka H \ refl_on (names H) (hequiv_rel H)\ unfolding refl_on_def using hequiv_refl hequiv_names_rel by fast lemma hequiv_sym_rel: \hintikka H \ sym (hequiv_rel H)\ unfolding sym_def using hequiv_sym by fast lemma hequiv_trans_rel: \hintikka H \ trans (hequiv_rel H)\ unfolding trans_def using hequiv_trans by fast lemma hequiv_rel: \hintikka H \ equiv (names H) (hequiv_rel H)\ using hequiv_refl_rel hequiv_sym_rel hequiv_trans_rel by (rule equivI) subsubsection \Named model\ text \ Given a Hintikka set \H\ and a formula \p\ on a block in \H\ we will construct a model that satisfies \p\. The worlds of our model are sets of equivalent nominals and nominals are assigned to their equivalence class. 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 :: \('a, 'b) block set \ 'b \ 'b set\ where - \assign H i \ Equiv_Relations.proj (hequiv_rel H) i\ + \assign H i \ proj (hequiv_rel H) i\ definition reach :: \('a, 'b) block set \ 'b set \ 'b set set\ where - \reach H is \ {assign H j |i j ps. i \ is \ (ps, i) \ H \ (\<^bold>\ Nom j) on (ps, i)}\ + \reach H is \ {assign 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. \ps. (ps, i) \ H \ Pro x on (ps, i)\ + \val H is x \ \i \ is. Pro x at i in' H\ lemma hequiv_assign: \hintikka H \ hequiv H i j \ assign H i = assign H j\ unfolding proj_def assign_def using equiv_class_eq hequiv_rel by fast lemma hequiv_model: assumes \hintikka H\ \hequiv H i j\ shows \(Model (reach H) (val H), assign H, assign H i \ p) = (Model (reach H) (val H), assign H, assign H j \ p)\ using assms hequiv_assign by fastforce lemma assign_refl: \hintikka H \ i \ names H \ i \ assign H i\ unfolding proj_def assign_def using hequiv_refl by fastforce lemma assign_refl': \hintikka H \ (ps, i) \ H \ i \ assign H i\ using assign_refl unfolding names_def by fast lemma assign_named: \hintikka H \ i \ names H \ \j \ assign H i. \ps. (ps, j) \ H\ using hequiv_sym unfolding proj_def assign_def hequiv_def by fast lemma nominal_in_names: assumes \hintikka 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 H\ unfolding hintikka_def by meson then show ?thesis unfolding names_def using assms(2) by fastforce qed lemma assign_sym: \hintikka H \ j \ assign H i \ i \ assign H j\ unfolding proj_def assign_def using hequiv_sym by fast lemma hintikka_model: - assumes \hintikka H\ \(ps, i) \ H\ + assumes \hintikka H\ shows - \p on (ps, i) \ Model (reach H) (val H), assign H, assign H i \ p\ - \(\<^bold>\ p) on (ps, i) \ \ Model (reach H) (val H), assign H, assign H i \ p\ - using assms(2) -proof (induct p arbitrary: i ps) - fix ps i + \p at i in' H \ Model (reach H) (val H), assign H, assign H i \ p\ + \(\<^bold>\ p) at i in' H \ \ Model (reach H) (val H), assign H, assign H i \ p\ +proof (induct p arbitrary: i) + fix i case (Pro x) - assume \Pro x on (ps, i)\ \(ps, i) \ H\ + assume \Pro x at i in' H\ then show \Model (reach H) (val H), assign H, assign H i \ Pro x\ using assms(1) assign_refl' unfolding val_def by fastforce next - fix ps i + fix i case (Pro x) - assume \(\<^bold>\ Pro x) on (ps, i)\ \(ps, i) \ H\ - then have \\qs. (qs, j) \ H \ Pro x on (qs, j)\ - if \\ps. (ps, i) \ H \ Nom j on (ps, i)\ for j + assume \(\<^bold>\ Pro x) at i in' H\ + then have \\ Pro x at j in' H\ if \Nom j at i in' H\ for j using that assms(1) unfolding hintikka_def by meson - then have \\qs. (qs, j) \ H \ Pro x on (qs, j)\ if \hequiv H i j\ for j + then have \\ Pro x at j in' H\ if \hequiv H i j\ for j using that unfolding hequiv_def by simp then have \\ val H (assign H i) x\ unfolding proj_def val_def assign_def by blast then show \\ Model (reach H) (val H), assign H, assign H i \ Pro x\ by simp next - fix ps i + fix i case (Nom a) - assume \Nom a on (ps, i)\ \(ps, i) \ H\ + assume \Nom a at i in' H\ then have \assign H a = assign H i\ using assms(1) hequiv_assign hequiv_sym unfolding hequiv_def by fast then show \Model (reach H) (val H), assign H, assign H i \ Nom a\ by simp next - fix ps i + fix i case (Nom a) - assume \(\<^bold>\ Nom a) on (ps, i)\ \(ps, i) \ H\ - then have \\qs. (qs, i) \ H \ Nom a on (qs, i)\ + assume \(\<^bold>\ Nom a) at i in' H\ + then have \\ Nom a at i in' H\ using assms(1) unfolding hintikka_def by meson then have \\ hequiv H i a\ unfolding hequiv_def by blast then have \\ hequiv H a i\ using assms(1) hequiv_sym by fast moreover have \hequiv H i i\ - using assms(1) \(ps, i) \ H\ hequiv_refl' by fast + using assms(1) \(\<^bold>\ Nom a) at i in' H\ hequiv_refl' by fast ultimately have \assign H a \ assign H i\ unfolding proj_def assign_def by blast then show \\ Model (reach H) (val H), assign H, assign H i \ Nom a\ by simp next - fix ps i + fix i case (Neg p) - moreover assume \(\<^bold>\ p) on (ps, i)\ \(ps, i) \ H\ + moreover assume \(\<^bold>\ p) at i in' H\ ultimately show \Model (reach H) (val H), assign H, assign H i \ \<^bold>\ p\ using assms(1) by simp next - fix ps i + fix i case (Neg p) - moreover assume \(\<^bold>\ \<^bold>\ p) on (ps, i)\ \(ps, i) \ H\ - then have \\ps. (ps, i) \ H \ p on (ps, i)\ + moreover assume \(\<^bold>\ \<^bold>\ p) at i in' H\ + then have \p at i in' H\ using assms(1) unfolding hintikka_def by meson ultimately show \\ Model (reach H) (val H), assign H, assign H i \ \<^bold>\ p\ using assms(1) by auto next - fix ps i + fix i case (Dis p q) - moreover assume \(p \<^bold>\ q) on (ps, i)\ \(ps, i) \ H\ - then have \\ps. (ps, i) \ H \ (p on (ps, i) \ q on (ps, i))\ + 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 ultimately show \Model (reach H) (val H), assign H, assign H i \ (p \<^bold>\ q)\ by (meson semantics.simps(4)) next - fix ps i + fix i case (Dis p q) - moreover assume \(\<^bold>\ (p \<^bold>\ q)) on (ps, i)\ \(ps, i) \ H\ - then have \\ps. (ps, i) \ H \ (\<^bold>\ p) on (ps, i) \ (\<^bold>\ q) on (ps, i)\ - using assms(1) unfolding hintikka_def by meson + 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+ ultimately show \\ Model (reach H) (val H), assign H, assign H i \ (p \<^bold>\ q)\ by auto next - fix ps i + fix i case (Dia p) - moreover assume \(\<^bold>\ p) on (ps, i)\ \(ps, i) \ H\ + moreover assume \(\<^bold>\ p) at i in' H\ ultimately show \Model (reach H) (val H), assign H, assign H i \ \<^bold>\ p\ proof (cases \\j. p = Nom j\) case True then obtain j where \p = Nom j\ by blast have \i \ assign H i\ - using assms(1) \(ps, i) \ H\ assign_refl' by fast + using assms(1) \(\<^bold>\ p) at i in' H\ assign_refl' by fast moreover have \j \ nominals (\<^bold>\ p)\ using \p = Nom j\ by simp then have \(\block \ H. (\<^bold>\ p) on block) \ (\qs. (qs, j) \ H)\ using assms(1) unfolding hintikka_def by meson then have \\bl. (bl, j) \ H\ - using \(\<^bold>\ p) on (ps, i)\ \(ps, i) \ H\ by blast + using \(\<^bold>\ p) at i in' H\ by blast then have \j \ assign H j\ - using assms(1) \(ps, i) \ H\ assign_refl' by fast - moreover have \(\<^bold>\ Nom j) on (ps, i)\ - using \p = Nom j\ \(\<^bold>\ p) on (ps, i)\ by blast + using assms(1) \(\<^bold>\ p) at i in' H\ assign_refl' by fast + moreover have \(\<^bold>\ Nom j) at i in' H\ + using \p = Nom j\ \(\<^bold>\ p) at i in' H\ by blast ultimately have \assign H j \ reach H (assign H i)\ - using \(ps, i) \ H\ unfolding reach_def by auto + using \(\<^bold>\ p) at i in' H\ unfolding reach_def by auto then show ?thesis using \p = Nom j\ by simp next case False - then have \\j. - (\qs. (qs, i) \ H \ (\<^bold>\ Nom j) on (qs, i)) \ - (\rs. (rs, i) \ H \ (\<^bold>@ j p) on (rs, i))\ - using assms \(\<^bold>\ p) on (ps, i)\ \(ps, i) \ H\ unfolding hintikka_def by blast - then obtain j qs rs where - qs: \(qs, i) \ H\ \(\<^bold>\ Nom j) on (qs, i)\ and - rs: \(rs, i) \ H\ \(\<^bold>@ j p) on (rs, i)\ + then have \\j. (\<^bold>\ Nom j) at i in' H \ (\<^bold>@ j p) at i in' H\ + using assms \(\<^bold>\ p) at i in' H\ unfolding hintikka_def by blast + then obtain j where *: \(\<^bold>\ Nom j) at i in' H\ \(\<^bold>@ j p) at i in' H\ by blast - from rs have \\ts. (ts, j) \ H \ p on (ts, j)\ + from *(2) have \p at j in' H\ using assms(1) unfolding hintikka_def by blast then have \Model (reach H) (val H), assign H, assign H j \ p\ using Dia by blast have \i \ assign H i\ - using assms(1) assign_refl' \(ps, i) \ H\ by fast + using assms(1) assign_refl' \(\<^bold>\ p) at i in' H\ by fast moreover have \j \ assign H j\ - using assms(1) assign_refl' \\ts. (ts, j) \ H \ p on (ts, j)\ by fast + using assms(1) assign_refl' \p at j in' H\ by fast ultimately have \assign H j \ reach H (assign H i)\ - using qs unfolding reach_def by auto + using *(1) unfolding reach_def by auto then show ?thesis using \Model (reach H) (val H), assign H, assign H j \ p\ by auto qed next - fix ps i + fix i case (Dia p) - assume \(\<^bold>\ (\<^bold>\ p)) on (ps, i)\ \(ps, i) \ H\ + assume \(\<^bold>\ (\<^bold>\ p)) at i in' H\ show \\ Model (reach H) (val H), assign H, assign H i \ \<^bold>\ p\ proof assume \Model (reach H) (val H), assign H, assign H i \ \<^bold>\ p\ - then obtain i' j qs where + then obtain i' j where \Model (reach H) (val H), assign H, assign H j \ p\ - \i' \ assign H i\ \(qs, i') \ H\ \(\<^bold>\ Nom j) on (qs, i')\ + \i' \ assign H i\ \(\<^bold>\ Nom j) at i' in' H\ unfolding reach_def by auto - have \\rs. (rs, i) \ H \ Nom i' on (rs, i)\ - using \i' \ assign H i\ \(qs, i') \ H\ + have \Nom i' at i in' H\ + using \i' \ assign H i\ \(\<^bold>\ Nom j) at i' in' H\ unfolding hequiv_def proj_def assign_def by auto - then have \\rs. (rs, i') \ H \ Nom i on (rs, i')\ + then have \Nom i at i' in' H\ using assms(1) unfolding hintikka_def by meson - then have \\rs. (rs, i) \ H \ (\<^bold>\ Nom j) on (rs, i)\ - using assms(1) \(\<^bold>\ Nom j) on (qs, i')\ \(qs, i') \ H\ + then have \(\<^bold>\ Nom j) at i in' H\ + using assms(1) \(\<^bold>\ Nom j) at i' in' H\ unfolding hintikka_def by meson - then have \\rs. (rs, i) \ H \ (\<^bold>\ (\<^bold>@ j p)) on (rs, i)\ - using assms(1) \(\<^bold>\ (\<^bold>\ p)) on (ps, i)\ \(ps, i) \ H\ + then have \(\<^bold>\ (\<^bold>@ j p)) at i in' H\ + using assms(1) \(\<^bold>\ (\<^bold>\ p)) at i in' H\ unfolding hintikka_def by meson - moreover have \\qs. (qs, j) \ H \ (\<^bold>\ p) on (qs, j)\ - if \\block \ H. (\<^bold>\ (\<^bold>@ j p)) on block\ - using that assms(1) unfolding hintikka_def by meson - ultimately obtain rs where \(rs, j) \ H\ \(\<^bold>\ p) on (rs, j)\ + 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 blast + ultimately have \(\<^bold>\ p) at j in' H\ by blast then have \\ Model (reach H) (val H), assign H, assign H j \ p\ using Dia by blast then show False using \Model (reach H) (val H), assign H, assign H j \ p\ by blast qed next - fix ps i + fix i case (Sat j p) - assume \(\<^bold>@ j p) on (ps, i)\ \(ps, i) \ H\ - moreover have \\qs. (qs, j) \ H \ p on (qs, j)\ - if \\block \ H. (\<^bold>@ j p) on block\ + assume \(\<^bold>@ j p) at i in' H\ + 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 - ultimately obtain qs where \(qs, j) \ H\ \p on (qs, j)\ + ultimately have \p at j in' H\ by blast then show \Model (reach H) (val H), assign H, assign H i \ \<^bold>@ j p\ using Sat by simp next - fix ps i + fix i case (Sat j p) - assume \(\<^bold>\ (\<^bold>@ j p)) on (ps, i)\ \(ps, i) \ H\ - moreover have \\qs. (qs, j) \ H \ (\<^bold>\ p) on (qs, j)\ - if \\block \ H. (\<^bold>\ (\<^bold>@ j p)) on block\ + assume \(\<^bold>\ (\<^bold>@ j p)) at i in' H\ + 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 - ultimately obtain qs where \(qs, j) \ H\ \(\<^bold>\ p) on (qs, j)\ + ultimately have \(\<^bold>\ p) at j in' H\ by blast then show \\ Model (reach H) (val H), assign H, assign H i \ \<^bold>@ j p\ using Sat by simp 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. \ definition consistent :: \('a, 'b) block set \ bool\ where \consistent S \ \S'. set S' \ S \ \ 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 :: \('a, 'b) block set \ (nat \ ('a, 'b) block) \ nat \ ('a, 'b) block set\ where \extend S f 0 = S\ | \extend S f (Suc n) = (if \ consistent ({f n} \ extend S f n) then extend S f n else - (if \p. (\<^bold>\ p) on f n - then {f n} \ extend S f n - else - let used = (\block \ {f n} \ extend S f n. block_nominals block) - in {f n, witness (f n) used} \ extend S f n))\ + let used = (\block \ {f n} \ extend S f n. block_nominals block) + in {f n, witness (f n) used} \ extend S f n)\ definition Extend :: \('a, 'b) block set \ (nat \ ('a, 'b) block) \ ('a, 'b) block set\ where \Extend S f \ (\n. extend S f n)\ lemma extend_chain: \extend S f n \ extend S f (Suc n)\ by auto lemma extend_mem: \S \ extend S f n\ by (induct n) auto lemma Extend_mem: \S \ Extend S f\ unfolding Extend_def using extend_mem by blast 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 cons: \consistent ({(p # ps, a)} \ S)\ shows \consistent ({(ps, a)} \ S)\ unfolding consistent_def proof - assume \\S'. set S' \ {(ps, a)} \ S \ \ S'\ - then obtain S' where \set S' \ {(ps, a)} \ S\ \(ps, a) \. S'\ \\ S'\ + assume \\S'. set S' \ {(ps, a)} \ S \ (\n. n \ S')\ + then obtain S' n where \set S' \ {(ps, a)} \ S\ \(ps, a) \. S'\ \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 \\ (ps, a) # S''\ - using inf ST_struct \\ S'\ by blast + using inf ST_struct \n \ S'\ by blast then have \\ (p # ps, a) # S''\ - using inf ST_struct_block[where ps'=\p # ps\] by auto + using inf ST_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 ({block} \ S) \ consistent S\ unfolding consistent_def by blast lemma inconsistent_weaken: \\ consistent S \ S \ S' \ \ consistent 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 S\ \finite S\ - \(ps, a) \ S\ \finite used\ \(\block \ S. block_nominals block) \ used\ + assumes inf: \infinite (UNIV :: 'b set)\ and \consistent S\ + \(ps, a) \ S\ \finite used\ \(\ (block_nominals ` S)) \ used\ shows \consistent ({(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 then show ?case using \consistent S\ by simp next case (Cons p ps) have \{(p # ps, a)} \ S = S\ using \(p # ps, a) \ S\ by blast then have \consistent ({(p # ps, a)} \ S)\ using \consistent S\ by simp then have \consistent ({(ps, a)} \ S)\ using inf consistent_drop_single by fast - moreover have \finite ({(ps, a)} \ S)\ - using \finite S\ by simp moreover have \(ps, a) \ {(ps, a)} \ S\ by simp moreover have \\ (block_nominals ` ({(ps, a)} \ S)) \ extra \ used\ for extra using \(p # ps, a) \ S\ \\ (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 ({(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 ({(witness_list ps used, a)} \ ({(ps, a)} \ S))\ using cons[where extra=\{}\] by simp then have \consistent ({(witness_list ps used, a)} \ S)\ using consistent_drop_block[where block=\(ps, a)\] by simp ultimately show ?thesis by simp next case (Some q) let ?i = \SOME i. i \ used\ have \\i. i \ used\ using \finite used\ inf ex_new_if_finite by metis then have \?i \ used\ using someI_ex by metis then have i: \?i \ \ (block_nominals ` S)\ using Cons by blast then have \?i \ block_nominals (p # ps, a)\ using Cons by blast let ?tail = \witness_list ps ({?i} \ used)\ have \consistent ({(?tail, a)} \ ({(ps, a)} \ S))\ using cons[where extra=\{?i}\] by simp then have *: \consistent ({(?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 ({((\<^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 \ \ S'\ - then obtain S' where - \\ S'\ and S': + assume \\S'. set S' \ {((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a)} \ S \ (\n. n \ S')\ + then obtain S' n where + \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 \\ ((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) # S''\ - using inf ST_struct \\ S'\ by blast + using inf ST_struct \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 **: \\ ((\<^bold>@ ?i q) # (\<^bold>\ Nom ?i) # ?tail, a) # (p # ps, a) # S''\ using inf ST_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 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 \\ (?tail, a) # (p # ps, a) # S''\ using ** DiaP' by fast moreover have \set ((p # ps, a) # S'') \ S\ using Cons 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 S\ \finite S\ \block \ S\ - shows \consistent ({witness block ((\block \ S. block_nominals block))} \ S)\ - using assms -proof (induct block) - case (Pair ps i) - then have \finite (\block \ S. block_nominals block)\ - using finite_nominals_set by blast - then show ?case - using Pair consistent_witness_list[where ps=ps] by simp -qed - -lemma finite_extend: \finite S \ finite (extend S f n)\ - by (induct n) simp_all + \consistent S\ \finite (\ (block_nominals ` S))\ \block \ S\ + shows \consistent ({witness block (\ (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 \consistent (extend S f n)\ \finite S\ + assumes inf: \infinite (UNIV :: 'b set)\ and + \consistent (extend S f n)\ \finite (\ (block_nominals ` extend S f n))\ shows \consistent (extend S f (Suc n))\ proof - consider (inconsistent) \\ consistent ({f n} \ extend S f n)\ | - (clear) \consistent ({f n} \ extend S f n) \ (\p. (\<^bold>\ p) on f n)\ | - (dia) \consistent ({f n} \ extend S f n) \ (\p. (\<^bold>\ p) on f n)\ + (consistent) \consistent ({f n} \ extend S f n)\ by blast then show ?thesis proof cases case inconsistent then show ?thesis using assms by simp next - case clear - then show ?thesis - by simp - next - case dia + case consistent let ?used = \\block \ {f n} \ extend S f n. block_nominals block\ have *: \extend S f (n + 1) = {f n, witness (f n) ?used} \ extend S f n\ - using dia by simp + using consistent by simp have \consistent ({f n} \ extend S f n)\ - using dia by simp - moreover have \finite ({f n} \ extend S f n)\ - using \finite S\ finite_extend by blast + using consistent by simp + moreover have \finite ((\ (block_nominals ` ({f n} \ extend S f n))))\ + using \finite (\ (block_nominals ` extend S f n))\ finite_nominals_set by force moreover have \f n \ {f n} \ extend S f n\ by simp ultimately have \consistent ({witness (f n) ?used} \ ({f n} \ extend S f n))\ using inf consistent_witness by blast then show ?thesis using * by simp qed qed +lemma finite_nominals_extend: + assumes \finite (\ (block_nominals ` S))\ + shows \finite (\ (block_nominals ` extend S f n))\ + using assms by (induct n) (simp_all add: finite_block_nominals) + lemma consistent_extend': fixes S :: \('a, 'b) block set\ - assumes inf: \infinite (UNIV :: 'b set)\ and \consistent S\ \finite S\ + assumes inf: \infinite (UNIV :: 'b set)\ and \consistent S\ \finite (\ (block_nominals ` S))\ shows \consistent (extend S f n)\ - using assms by (induct n) (simp, metis consistent_extend) + using assms by (induct n) (simp, metis consistent_extend finite_nominals_extend) 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 S f n) = extend S f m\ proof (induct m) case (Suc m) have \\ (extend S f ` {..Suc m}) = \ (extend S f ` {..m}) \ extend S f (Suc m)\ using atMost_Suc by auto also have \\ = extend S f m \ extend S f (Suc m)\ using Suc by blast also have \\ = extend 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 \consistent S\ \finite S\ + assumes inf: \infinite (UNIV :: 'b set)\ and + \consistent S\ \finite (\ (block_nominals ` S))\ shows \consistent (Extend S f)\ unfolding Extend_def proof (rule ccontr) assume \\ consistent (\ (range (extend S f)))\ - then obtain S' where - \\ S'\ + then obtain S' n where + \n \ S'\ \set S' \ (\n. extend S f n)\ unfolding consistent_def by blast moreover have \finite (set S')\ by simp ultimately obtain m where \set S' \ (\n \ m. extend S f n)\ using UN_finite_bound by metis then have \set S' \ extend S f m\ using extend_bound by blast moreover have \consistent (extend S f m)\ using assms consistent_extend' by blast ultimately show False - unfolding consistent_def using \\ S'\ by blast + unfolding consistent_def using \n \ S'\ by blast qed subsubsection \Maximality\ text \A set of blocks is maximally consistent if any proper extension makes it inconsistent.\ definition maximal :: \('a, 'b) block set \ bool\ where \maximal S \ consistent S \ (\block. block \ S \ \ consistent ({block} \ S))\ lemma extend_not_mem: \f n \ extend S f (Suc n) \ \ consistent ({f n} \ extend 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 \consistent S\ \finite S\ \surj f\ + assumes inf: \infinite (UNIV :: 'b set)\ and + \consistent S\ \finite (\ (block_nominals ` S))\ \surj f\ shows \maximal (Extend S f)\ proof (rule ccontr) assume \\ maximal (Extend S f)\ then obtain block where \block \ Extend S f\ \consistent ({block} \ Extend S f)\ unfolding maximal_def using assms consistent_Extend by blast obtain n where n: \f n = block\ using \surj f\ unfolding surj_def by metis then have \block \ extend S f (Suc n)\ using \block \ Extend S f\ extend_chain unfolding Extend_def by blast then have \\ consistent ({block} \ extend S f n)\ using n extend_not_mem by blast moreover have \block \ extend S f n\ using \block \ extend S f (Suc n)\ extend_chain by auto then have \{block} \ extend S f n \ {block} \ Extend S f\ unfolding Extend_def by blast ultimately have \\ consistent ({block} \ Extend S f)\ using inconsistent_weaken by blast then show False using \consistent ({block} \ Extend S f)\ by blast 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 \ \(ps, i) \ S. \p. - (\<^bold>\ p) on (ps, i) \ (\a. p = Nom a) \ (\j. - (\qs. (qs, i) \ S \ (\<^bold>@ j p) on (qs, i)) \ - (\rs. (rs, i) \ S \ (\<^bold>\ Nom j) on (rs, i)))\ + \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 \consistent S\ \finite S\ \surj f\ + assumes inf: \infinite (UNIV :: 'b set)\ and + \consistent S\ \finite (\ (block_nominals ` S))\ \surj f\ shows \saturated (Extend S f)\ unfolding saturated_def proof safe fix ps i p assume \(ps, i) \ Extend 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 = \(\block \ {f n} \ extend S f n. block_nominals block)\ have \extend S f n \ Extend S f\ unfolding Extend_def by auto moreover have \consistent (Extend S f)\ using assms consistent_Extend by blast ultimately have \consistent ({(ps, i)} \ extend S f n)\ using \(ps, i) \ Extend S f\ inconsistent_weaken by blast then have \extend S f (Suc n) = {f n, witness (f n) ?used} \ extend S f n\ using n \(\<^bold>\ p) on (ps, i)\ by auto then have \witness (f n) ?used \ Extend S f\ unfolding Extend_def by blast then have *: \(witness_list ps ?used, i) \ Extend 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 S f \ (\<^bold>@ j p) on (qs, i)) \ (\rs. (rs, i) \ Extend S f \ (\<^bold>\ Nom j) on (rs, i))\ using * by blast qed subsection \Smullyan-Fitting\ lemma hintikka_Extend: fixes S :: \('a, 'b) block set\ assumes inf: \infinite (UNIV :: 'b set)\ and \maximal S\ \consistent S\ \saturated S\ shows \hintikka 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 \\ \ [(ps, i), (qs, j), (rs, i)]\ + then have \\ n \ [(ps, i), (qs, j), (rs, i)]\ for n using \consistent S\ unfolding consistent_def by simp - moreover have \\ [(Pro x # ps, i), (qs, j), (rs, i)]\ - using ps(2) rs(2) Close[where p=\Pro x\ and i=i] by force - then have \\ [(ps, i), (qs, j), (rs, i)]\ + moreover have \n \ [(Pro x # ps, i), (qs, j), (rs, i)]\ for n + using ps(2) rs(2) by (meson Close list.set_intros(1) on.simps set_subset_Cons subsetD) + then have \n \ [(ps, i), (qs, j), (rs, i)]\ for n using ps qs rev_nth_on by (meson Nom' list.set_intros(1) rev_nth_on 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 \\ \ [(ps, i), (qs, i)]\ + then have \\ n \ [(ps, i), (qs, i)]\ for n using \consistent S\ unfolding consistent_def by simp - moreover have \\ [(ps, i), (qs, i)]\ - using ps(2) qs(2) Close[where p=\Nom a\ and i=i] by force + moreover have \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 \\ \ [(ps, i), (qs, i)]\ + then have \\ n \ [(ps, i), (qs, i)]\ for n using \consistent S\ unfolding consistent_def by simp - moreover have \\ [(ps, i), (qs, i)]\ + moreover have \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\ proof (rule ccontr) assume \\qs. (qs, i) \ S\ - then obtain S' where - \\ S'\ and S': \set S' \ {([], i)} \ S\ and \([], i) \. S'\ - using \maximal S\ unfolding maximal_def consistent_def by fast + then obtain S' n where + \n \ S'\ and S': \set S' \ {([], i)} \ S\ and \([], i) \. S'\ + using \maximal 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 \\ ([], i) # (ps, a) # S''\ - using inf ST_struct[where branch'=\([], i) # (ps, a) # _\] \\ S'\ by auto + using inf ST_struct[where branch'=\([], i) # (ps, a) # S''\] \n \ S'\ by fastforce moreover have \i \ branch_nominals ((ps, a) # S'')\ using i ps unfolding branch_nominals_def by auto ultimately have \\ (ps, a) # S''\ - by (simp add: GoTo) + using GoTo by fast moreover have \set ((ps, a) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent S\ unfolding consistent_def by blast qed next fix i j ps assume 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' where - \\ S'\ and S': \set S' \ {([Nom i], j)} \ S\ and \([Nom i], j) \. S'\ + then obtain S' n where + \n \ S'\ and S': \set S' \ {([Nom i], j)} \ S\ and \([Nom i], j) \. S'\ using \maximal 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 \\ ([Nom i], j) # (ps, i) # S''\ - using inf ST_struct[where branch'=\([Nom i], j) # (ps, i) # _\] \\ S'\ - by auto + using inf ST_struct[where branch'=\([Nom i], j) # (ps, i) # S''\] \n \ S'\ by fastforce then have \\ ([], j) # (ps, i) # S''\ - using \Nom j on (ps, i)\ - by (meson Nom' list.set_intros(1) list.set_intros(2) on.simps) + using \Nom j on (ps, i)\ by (meson Nom' 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 \\ (ps, i) # S''\ - by (simp add: GoTo) + using GoTo by fast moreover have \set ((ps, i) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent 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)\ 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' where - \\ S'\ and S': \set S' \ {([Nom k], i)} \ S\ and \([Nom k], i) \. S'\ + then obtain S' n where + \n \ S'\ and S': \set S' \ {([Nom k], i)} \ S\ and \([Nom k], i) \. S'\ using \maximal 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 \\ ([Nom k], i) # (Nom k # ps, i) # (qs, j) # S''\ - using inf ST_struct[where branch'=\([Nom k], i) # (Nom k # ps, i) # (qs, j) # _\] \\ S'\ - by auto + using inf ST_struct[where branch'=\([Nom k], i) # (Nom k # ps, i) # (qs, j) # S''\] \n \ S'\ + by fastforce then have \\ ([], i) # (Nom k # ps, i) # (qs, j) # S''\ by (meson Nom' list.set_intros(1-2) on.simps) moreover have \i \ branch_nominals ((Nom k # ps, i) # (qs, j) # S'')\ unfolding branch_nominals_def by simp ultimately have \\ (Nom k # ps, i) # (qs, j) # S''\ - by (simp add: GoTo) + using GoTo by fast then have \\ (ps, i) # (qs, j) # S''\ using ps qs by (meson Nom' list.set_intros(1-2) on.simps) moreover have \set ((ps, i) # (qs, j) # S'') \ S\ using S' S'' ps qs by auto ultimately show False using \consistent 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)\ 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' where - \\ S'\ and S': \set S' \ {([\<^bold>\ Nom k], i)} \ S\ and \([\<^bold>\ Nom k], i) \. S'\ + then obtain S' n where + \n \ S'\ and S': \set S' \ {([\<^bold>\ Nom k], i)} \ S\ and \([\<^bold>\ Nom k], i) \. S'\ using \maximal 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 \\ ([\<^bold>\ Nom k], i) # (ps, i) # (qs, j) # S''\ - using inf ST_struct[where branch'=\([\<^bold>\ Nom k], i) # (ps, i) # (qs, j) # S''\] \\ S'\ - by auto + using inf ST_struct[where branch'=\([\<^bold>\ Nom k], i) # (ps, i) # (qs, j) # S''\] \n \ S'\ + by fastforce then have \\ ([], i) # (ps, i) # (qs, j) # S''\ - using ps qs inf by (meson Bridge list.set_intros(1) on.simps set_subset_Cons subset_iff) + using ps(2) qs(2) inf 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 \\ (ps, i) # (qs, j) # S''\ - by (simp add: GoTo) + 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 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)\ 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' where - \\ S'\ and S': \set S' \ {([\<^bold>\ Nom j], k)} \ S\ and \([\<^bold>\ Nom j], k) \. S'\ + then obtain S' n where + \n \ S'\ and S': \set S' \ {([\<^bold>\ Nom j], k)} \ S\ and \([\<^bold>\ Nom j], k) \. S'\ using \maximal 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 \\ ([\<^bold>\ Nom j], k) # (Nom k # ps, i) # (qs, i) # S''\ - using inf ST_struct[where branch'=\([\<^bold>\ Nom j], k) # (Nom k # ps, i) # (qs, i) # S''\] \\ S'\ - by auto + using inf ST_struct[where branch'=\([\<^bold>\ Nom j], k) # (Nom k # ps, i) # (qs, i) # S''\] \n \ S'\ + by fastforce then have \\ ([], k) # (Nom k # ps, i) # (qs, i) # S''\ - using ps by (meson Nom' fm.simps(22) list.set_intros(1-2) on.simps) + using ps(2) by (meson Nom' fm.simps(22) list.set_intros(1-2) on.simps) moreover have \k \ branch_nominals ((Nom k # ps, i) # (qs, i) # S'')\ unfolding branch_nominals_def by simp ultimately have \\ (Nom k # ps, i) # (qs, i) # S''\ - by (simp add: GoTo) + using GoTo by fast then have \\ (ps, i) # (qs, i) # S''\ - using ps qs by (meson Nom' list.set_intros(1-2) on.simps) + using ps(2) qs(2) by (meson Nom' list.set_intros(1-2) on.simps) moreover have \set ((ps, i) # (qs, i) # S'') \ S\ using S' S'' ps qs by auto ultimately show False using \consistent S\ unfolding consistent_def by blast qed next fix p q i ps - assume ps: \(ps, i) \ S\ \(p \<^bold>\ q) on (ps, i)\ - show \\qs. (qs, i) \ S \ (p on (qs, i) \ q on (qs, i))\ + 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 *: \\qs. (qs, i) \ S \ (p on (qs, i) \ q on (qs, i))\ - then obtain Sp' where - \\ Sp'\ and Sp': \set Sp' \ {(p # ps, i)} \ S\ and \(p # ps, i) \. Sp'\ + assume \\ p at i in' S\ + then obtain Sp' np where + \np \ Sp'\ and Sp': \set Sp' \ {(p # ps, i)} \ S\ and \(p # ps, i) \. Sp'\ using \maximal 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 \\ (p # ps, i) # Sp''\ - using \\ Sp'\ inf ST_struct by blast - - obtain Sq' where - \\ Sq'\ and Sq': \set Sq' \ {(q # ps, i)} \ S\ and \(q # ps, i) \. Sq'\ + using \np \ Sp'\ inf ST_struct by blast + + obtain Sq' nq where + \nq \ Sq'\ and Sq': \set Sq' \ {(q # ps, i)} \ S\ and \(q # ps, i) \. Sq'\ using * \maximal 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 \\ (q # ps, i) # Sq''\ - using \\ Sq'\ inf ST_struct by blast + using \nq \ Sq'\ inf ST_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 \\ (p # ps, i) # S''\ \\ (q # ps, i) # S''\ using \\ (p # ps, i) # Sp''\ \\ (q # ps, i) # Sq''\ inf ST_struct by blast+ then have \\ (ps, i) # S''\ - using ps by (meson DisP' list.set_intros(1)) + 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 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 \\qs. (qs, i) \ S \ (\<^bold>\ p) on (qs, i) \ (\<^bold>\ q) on (qs, i)\ + show \(\<^bold>\ p) at i in' S\ proof (rule ccontr) - assume \\qs. (qs, i) \ S \ (\<^bold>\ p) on (qs, i) \ (\<^bold>\ q) on (qs, i)\ + assume \\ (\<^bold>\ p) at i in' S\ + then obtain S' where + \\ S'\ and + S': \set S' \ {((\<^bold>\ q) # (\<^bold>\ p) # ps, i)} \ S\ and + \((\<^bold>\ q) # (\<^bold>\ p) # ps, i) \. S'\ + using \maximal 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 \\ ((\<^bold>\ q) # (\<^bold>\ p) # ps, i) # S''\ + using inf ST_struct \\ S'\ by blast + then have \\ (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 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 \\ S'\ and S': \set S' \ {((\<^bold>\ q) # (\<^bold>\ p) # ps, i)} \ S\ and \((\<^bold>\ q) # (\<^bold>\ p) # ps, i) \. S'\ using \maximal 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 \\ ((\<^bold>\ q) # (\<^bold>\ p) # ps, i) # S''\ using inf ST_struct \\ S'\ by blast then have \\ (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 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)\ proof (rule ccontr) assume \\qs. (qs, i) \ S \ p on (qs, i)\ - then obtain S' where - \\ S'\ and S': \set S' \ {(p # ps, i)} \ S\ and \(p # ps, i) \. S'\ + then obtain S' n where + \n \ S'\ and S': \set S' \ {(p # ps, i)} \ S\ and \(p # ps, i) \. S'\ using \maximal 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 \\ (p # ps, i) # S''\ - using inf ST_struct \\ S'\ by blast + using inf ST_struct \n \ S'\ by blast then have \\ (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 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)\ proof (rule ccontr) assume \\qs. (qs, i) \ S \ p on (qs, i)\ - then obtain S' where - \\ S'\ and S': \set S' \ {([p], i)} \ S\ and \([p], i) \. S'\ + then obtain S' n where + \n \ S'\ and S': \set S' \ {([p], i)} \ S\ and \([p], i) \. S'\ using \maximal 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 \\ ([p], i) # S''\ - using inf ST_struct \\ S'\ by blast + using inf ST_struct \n \ S'\ by blast moreover have \set (([p], i) # S'') \ set (([p], i) # (ps, a) # S'')\ by auto ultimately have \\ ([p], i) # (ps, a) # S''\ - using inf ST_struct \\ S'\ by blast + using inf ST_struct \n \ S'\ by blast then have \\ ([], 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 \\ (ps, a) # S''\ - by (simp add: GoTo) + using GoTo by fast moreover have \set ((ps, a) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent 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)\ proof (rule ccontr) assume \\qs. (qs, i) \ S \ (\<^bold>\ p) on (qs, i)\ - then obtain S' where - \\ S'\ and S': \set S' \ {([\<^bold>\ p], i)} \ S\ and \([\<^bold>\ p], i) \. S'\ + then obtain S' n where + \n \ S'\ and S': \set S' \ {([\<^bold>\ p], i)} \ S\ and \([\<^bold>\ p], i) \. S'\ using \maximal 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 \\ ([\<^bold>\ p], i) # S''\ - using inf ST_struct \\ S'\ by blast + using inf ST_struct \n \ S'\ by blast then have \\ ([\<^bold>\ p], i) # (ps, a) # S''\ - using inf ST_struct[where branch'=\([\<^bold>\ p], i) # _ # S''\] \\ S'\ + using inf ST_struct[where branch'=\([\<^bold>\ p], i) # _ # S''\] \n \ S'\ by fastforce then have \\ ([], 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 \\ (ps, a) # S''\ - by (simp add: GoTo) + using GoTo by fast moreover have \set ((ps, a) # S'') \ S\ using S' S'' ps by auto ultimately show False using \consistent 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)\ proof (rule ccontr) assume \\qs. (qs, i) \ S \ (\<^bold>\ (\<^bold>@ j p)) on (qs, i)\ - then obtain S' where - \\ S'\ and S': \set S' \ {([\<^bold>\ (\<^bold>@ j p)], i)} \ S\ and \([\<^bold>\ (\<^bold>@ j p)], i) \. S'\ + then obtain S' n where + \n\ S'\ and S': \set S' \ {([\<^bold>\ (\<^bold>@ j p)], i)} \ S\ and \([\<^bold>\ (\<^bold>@ j p)], i) \. S'\ using \maximal 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>\ (\<^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 \\ ([\<^bold>\ (\<^bold>@ j p)], i) # S''\ - using inf ST_struct \\ S'\ by blast + using inf ST_struct \n \ S'\ by blast then have \\ ([\<^bold>\ (\<^bold>@ j p)], i) # (ps, i) # (qs, i) # S''\ - using inf ST_struct[where branch'=\([_], _) # (ps, i) # (qs, i) # S''\] \\ S'\ + using inf ST_struct[where branch'=\([_], _) # (ps, i) # (qs, i) # S''\] \n \ S'\ by fastforce then have \\ ([], i) # (ps, i) # (qs, i) # S''\ - using ps qs by (meson DiaN' list.set_intros(1) set_subset_Cons subset_iff) + 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 \\ (ps, i) # (qs, i) # S''\ - by (simp add: GoTo) + 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 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 \\ [([\<^bold>\ p], i)]\ -proof (rule ccontr) - assume \\ \ [([\<^bold>\ p], i)]\ - then have *: \consistent {([\<^bold>\ p], i)}\ - unfolding consistent_def using ST_struct inf by fastforce - - let ?S = \Extend {([\<^bold>\ p], i)} from_nat\ - - have \consistent ?S\ - using consistent_Extend inf * by blast - moreover have \maximal ?S\ - using maximal_Extend inf * by fastforce - moreover have \saturated ?S\ - using saturated_Extend inf * by fastforce - ultimately have \hintikka ?S\ - using hintikka_Extend inf by blast - moreover have \([\<^bold>\ p], i) \ ?S\ - using Extend_mem by blast - moreover have \(\<^bold>\ p) on ([\<^bold>\ p], i)\ - by simp - ultimately have \\ Model (reach ?S) (val ?S), assign ?S, assign ?S i \ p\ - using hintikka_model by fast - then show False - using valid by blast + shows \1 \ [([\<^bold>\ p], i)]\ +proof - + have \\ [([\<^bold>\ p], i)]\ + proof (rule ccontr) + assume \\ \ [([\<^bold>\ p], i)]\ + then have *: \consistent {([\<^bold>\ p], i)}\ + unfolding consistent_def using ST_struct inf + by (metis empty_set list.simps(15)) + + let ?S = \Extend {([\<^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 ?S\ + using consistent_Extend inf * fin by blast + moreover have \maximal ?S\ + using maximal_Extend inf * fin by fastforce + moreover have \saturated ?S\ + using saturated_Extend inf * fin by fastforce + ultimately have \hintikka ?S\ + using hintikka_Extend inf by blast + moreover have \([\<^bold>\ p], i) \ ?S\ + using Extend_mem by blast + moreover have \(\<^bold>\ p) on ([\<^bold>\ p], i)\ + by simp + ultimately have \\ Model (reach ?S) (val ?S), assign ?S, assign ?S i \ p\ + using hintikka_model by fast + then show False + using valid by blast + qed + then show ?thesis + using ST_one by blast 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.\ theorem main: assumes \i \ nominals p\ - shows \valid p \ \ [([\<^bold>\ p], i)]\ + shows \valid p \ 1 \ [([\<^bold>\ p], i)]\ proof assume \valid p\ - then show \\ [([\<^bold>\ p], i)]\ + then show \1 \ [([\<^bold>\ p], i)]\ using completeness by blast next - assume \\ [([\<^bold>\ p], i)]\ + assume \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 \ \ [([\<^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 diff --git a/thys/Hybrid_Logic/document/root.tex b/thys/Hybrid_Logic/document/root.tex --- a/thys/Hybrid_Logic/document/root.tex +++ b/thys/Hybrid_Logic/document/root.tex @@ -1,89 +1,91 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed \usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage{eurosym} %for \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \, \, \, \, %\ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \begin{document} \title{Formalizing a Seligman-Style Tableau System for Hybrid Logic} \author{Asta Halkjær From} \maketitle \begin{abstract} This work is a formalization of soundness and completeness proofs for a Seligman-style tableau system for hybrid logic~\cite{jlog17}. The completeness result is obtained via a synthetic approach using maximally consistent sets of tableau blocks~\cite{aiml16}. The formalization differs from the cited work in a few ways. First, to avoid the need to backtrack in the construction of a tableau, the formalized system has no unnamed initial segment, and therefore no \textit{Name} rule. Second, I show that the full \textit{Bridge} rule is derivable in the system. Third, I start from rules restricted to only extend the branch with new formulas, including only witnessing diamonds that are not already witnessed, and show that the unrestricted rules are derivable. Similarly, I start from simpler versions of the \( @ \)-rules and derive the general ones. + Finally, the \textit{GoTo} rule is restricted using a notion of coins such that each application consumes a coin and coins are earned through applications of the remaining rules. + I show that if a branch can be closed then it can be closed starting from a single coin. These restrictions are imposed to rule out some means of nontermination~\cite{jlog17}. \end{abstract} \section*{Preamble} The formalization is part of the author's MSc thesis in Computer Science and Engineering at the Technical University of Denmark (DTU). \paragraph{Supervisors:} \begin{itemize} \item Jørgen Villadsen \item Alexander Birch Jensen \item Patrick Blackburn (Roskilde University, external supervisor) \end{itemize} \newpage \tableofcontents \newpage % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} \nocite{*} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \addcontentsline{toc}{section}{References} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: