diff --git a/thys/Buchi_Complementation/Complementation.thy b/thys/Buchi_Complementation/Complementation.thy --- a/thys/Buchi_Complementation/Complementation.thy +++ b/thys/Buchi_Complementation/Complementation.thy @@ -1,607 +1,607 @@ section \Complementation\ theory Complementation imports "Transition_Systems_and_Automata.Maps" "Ranking" begin subsection \Level Rankings and Complementation States\ type_synonym 'state lr = "'state \ nat" definition lr_succ :: "('label, 'state) nba \ 'label \ 'state lr \ 'state lr set" where "lr_succ A a f \ {g. dom g = \ (transition A a ` dom f) \ (\ p \ dom f. \ q \ transition A a p. the (g q) \ the (f p)) \ (\ q \ dom g. accepting A q \ even (the (g q)))}" type_synonym 'state st = "'state set" definition st_succ :: "('label, 'state) nba \ 'label \ 'state lr \ 'state st \ 'state st" where "st_succ A a g P \ {q \ if P = {} then dom g else \ (transition A a ` P). even (the (g q))}" type_synonym 'state cs = "'state lr \ 'state st" definition complement_succ :: "('label, 'state) nba \ 'label \ 'state cs \ 'state cs set" where "complement_succ A a \ \ (f, P). {(g, st_succ A a g P) |g. g \ lr_succ A a f}" definition complement :: "('label, 'state) nba \ ('label, 'state cs) nba" where "complement A \ nba (alphabet A) ({const (Some (2 * card (nodes A))) |` initial A} \ {{}}) (complement_succ A) (\ (f, P). P = {})" lemma dom_nodes: assumes "fP \ nodes (complement A)" shows "dom (fst fP) \ nodes A" using assms unfolding complement_def complement_succ_def lr_succ_def by (induct) (auto, blast) lemma ran_nodes: assumes "fP \ nodes (complement A)" shows "ran (fst fP) \ {0 .. 2 * card (nodes A)}" using assms proof induct case (initial fP) show ?case using initial unfolding complement_def by (auto) (metis eq_refl option.inject ran_restrictD) next case (execute fP agQ) obtain f P where 1: "fP = (f, P)" by force have 2: "ran f \ {0 .. 2 * card (nodes A)}" using execute(2) unfolding 1 by auto obtain a g Q where 3: "agQ = (a, (g, Q))" using prod_cases3 by this have 4: "p \ dom f \ q \ transition A a p \ the (g q) \ the (f p)" for p q using execute(3) unfolding 1 3 complement_def nba.simps complement_succ_def lr_succ_def by simp have 8: "dom g = \((transition A a) ` (dom f))" using execute(3) unfolding 1 3 complement_def nba.simps complement_succ_def lr_succ_def by simp show ?case unfolding 1 3 ran_def proof safe fix q k assume 5: "fst (snd (a, (g, Q))) q = Some k" have 6: "q \ dom g" using 5 by auto obtain p where 7: "p \ dom f" "q \ transition A a p" using 6 unfolding 8 by auto have "k = the (g q)" using 5 by auto also have "\ \ the (f p)" using 4 7 by this also have "\ \ 2 * card (nodes A)" using 2 7(1) by (simp add: domD ranI subset_eq) finally show "k \ {0 .. 2 * card (nodes A)}" by auto qed qed lemma states_nodes: assumes "fP \ nodes (complement A)" shows "snd fP \ nodes A" using assms proof induct case (initial fP) show ?case using initial unfolding complement_def by auto next case (execute fP agQ) obtain f P where 1: "fP = (f, P)" by force have 2: "P \ nodes A" using execute(2) unfolding 1 by auto obtain a g Q where 3: "agQ = (a, (g, Q))" using prod_cases3 by this have 11: "a \ alphabet A" using execute(3) unfolding 3 complement_def by auto have 10: "(g, Q) \ nodes (complement A)" using execute(1, 3) unfolding 1 3 by auto have 4: "dom g \ nodes A" using dom_nodes[OF 10] by simp have 5: "\ (transition A a ` P) \ nodes A" using 2 11 by auto have 6: "Q \ nodes A" using execute(3) unfolding 1 3 complement_def nba.simps complement_succ_def st_succ_def using 4 5 by (auto split: if_splits) show ?case using 6 unfolding 3 by auto qed theorem complement_finite: assumes "finite (nodes A)" shows "finite (nodes (complement A))" proof - let ?lrs = "{f. dom f \ nodes A \ ran f \ {0 .. 2 * card (nodes A)}}" have 1: "finite ?lrs" using finite_set_of_finite_maps' assms by auto let ?states = "Pow (nodes A)" have 2: "finite ?states" using assms by simp have "nodes (complement A) \ ?lrs \ ?states" by (force dest: dom_nodes ran_nodes states_nodes) also have "finite \" using 1 2 by simp finally show ?thesis by this qed lemma complement_trace_snth: assumes "run (complement A) (w ||| r) p" defines "m \ p ## trace (w ||| r) p" obtains "fst (m !! Suc k) \ lr_succ A (w !! k) (fst (m !! k))" "snd (m !! Suc k) = st_succ A (w !! k) (fst (m !! Suc k)) (snd (m !! k))" proof have 1: "r !! k \ transition (complement A) (w !! k) (m !! k)" using nba.run_snth assms by force show "fst (m !! Suc k) \ lr_succ A (w !! k) (fst (m !! k))" using assms(2) 1 unfolding complement_def complement_succ_def nba.trace_alt_def by auto show "snd (m !! Suc k) = st_succ A (w !! k) (fst (m !! Suc k)) (snd (m !! k))" using assms(2) 1 unfolding complement_def complement_succ_def nba.trace_alt_def by auto qed subsection \Word in Complement Language Implies Ranking\ lemma complement_ranking: assumes "w \ language (complement A)" obtains f where "ranking A w f" proof - obtain r p where 1: "run (complement A) (w ||| r) p" "p \ initial (complement A)" - "infs (accepting (complement A)) r" + "infs (accepting (complement A)) (p ## r)" using assms by rule let ?m = "p ## r" obtain 100: "fst (?m !! Suc k) \ lr_succ A (w !! k) (fst (?m !! k))" "snd (?m !! Suc k) = st_succ A (w !! k) (fst (?m !! Suc k)) (snd (?m !! k))" for k using complement_trace_snth 1(1) unfolding nba.trace_alt_def szip_smap_snd by metis define f where "f \ \ (k, q). the (fst (?m !! k) q)" define P where "P k \ snd (?m !! k)" for k have 2: "snd v \ dom (fst (?m !! fst v))" if "v \ gunodes A w" for v using that proof induct case (initial v) then show ?case using 1(2) unfolding complement_def by auto next case (execute v u) have "snd u \ \ ((transition A (w !! fst v)) ` (dom (fst (?m !! fst v))))" using execute(2, 3) by auto also have "\ = dom (fst (?m !! Suc (fst v)))" using 100 unfolding lr_succ_def by simp also have "Suc (fst v) = fst u" using execute(3) by auto finally show ?case by this qed have 3: "f u \ f v" if 10: "v \ gunodes A w" and 11: "u \ gusuccessors A w v" for u v proof - have 15: "snd u \ transition A (w !! fst v) (snd v)" using 11 by auto have 16: "snd v \ dom (fst (?m !! fst v))" using 2 10 by this have "f u = the (fst (?m !! fst u) (snd u))" unfolding f_def by (simp add: case_prod_beta) also have "fst u = Suc (fst v)" using 11 by auto also have "the (fst (?m !! \) (snd u)) \ the (fst (?m !! fst v) (snd v))" using 100 15 16 unfolding lr_succ_def by auto also have "\ = f v" unfolding f_def by (simp add: case_prod_beta) finally show "f u \ f v" by this qed have 4: "\ l \ k. P l = {}" for k proof - have 15: "infs (\ (k, P). P = {}) ?m" using 1(3) unfolding complement_def by auto obtain l where 17: "l \ k" "snd (?m !! l) = {}" using 15 unfolding infs_snth by force have 19: "P l = {}" unfolding P_def using 17 by auto show ?thesis using 19 17(1) by auto qed show ?thesis proof (rule that, unfold ranking_def, intro conjI ballI impI allI) fix v assume "v \ gunodes A w" then show "f v \ 2 * card (nodes A)" proof induct case (initial v) then show ?case using 1(2) unfolding complement_def f_def by auto next case (execute v u) have "f u \ f v" using 3[OF execute(1)] execute(3) by simp also have "\ \ 2 * card (nodes A)" using execute(2) by this finally show ?case by this qed next fix v u assume 10: "v \ gunodes A w" assume 11: "u \ gusuccessors A w v" show "f u \ f v" using 3 10 11 by this next fix v assume 10: "v \ gunodes A w" assume 11: "gaccepting A v" show "even (f v)" using 10 proof cases case (initial) then show ?thesis using 1(2) unfolding complement_def f_def by auto next case (execute u) have 12: "snd v \ dom (fst (?m !! fst v))" using execute graph.nodes.execute 2 by blast have 12: "snd v \ dom (fst (?m !! Suc (fst u)))" using 12 execute(2) by auto have 13: "accepting A (snd v)" using 11 by auto have "f v = the (fst (?m !! fst v) (snd v))" unfolding f_def by (simp add: case_prod_beta) also have "fst v = Suc (fst u)" using execute(2) by auto also have "even (the (fst (?m !! Suc (fst u)) (snd v)))" using 100 12 13 unfolding lr_succ_def by simp finally show ?thesis by this qed next fix v s k assume 10: "v \ gunodes A w" assume 11: "gurun A w s v" assume 12: "smap f (gtrace s v) = sconst k" show "odd k" proof assume 13: "even k" obtain t u where 14: "u \ ginitial A" "gupath A w t u" "v = gtarget t u" using 10 by auto obtain l where 15: "l \ length t" "P l = {}" using 4 by auto obtain l' where 16: "l' \ Suc l" "P l' = {}" using 4 by auto have 30: "gurun A w (t @- s) u" using 11 14 by auto have 21: "fst (gtarget (stake (Suc l) (t @- s)) u) = Suc l" for l unfolding sscan_snth[symmetric] using 30 14(1) by (auto elim!: grun_elim) have 17: "snd (gtarget (stake (Suc l + i) (t @- s)) u) \ P (Suc l + i)" for i proof (induct i) case (0) have 20: "gtarget (stake (Suc l) (t @- s)) u \ gunodes A w" using 14 11 by (force simp add: 15(1) le_SucI graph.run_stake stake_shift) have "snd (gtarget (stake (Suc l) (t @- s)) u) \ dom (fst (?m !! fst (gtarget (stake (Suc l) (t @- s)) u)))" using 2[OF 20] by this also have "fst (gtarget (stake (Suc l) (t @- s)) u) = Suc l" using 21 by this finally have 22: "snd (gtarget (stake (Suc l) (t @- s)) u) \ dom (fst (?m !! Suc l))" by this have "gtarget (stake (Suc l) (t @- s)) u = gtrace (t @- s) u !! l" unfolding sscan_snth by rule also have "\ = gtrace s v !! (l - length t)" using 15(1) by simp also have "f \ = smap f (gtrace s v) !! (l - length t)" by simp also have "smap f (gtrace s v) = sconst k" unfolding 12 by rule also have "sconst k !! (l - length t) = k" by simp finally have 23: "even (f (gtarget (stake (Suc l) (t @- s)) u))" using 13 by simp have 24: "snd (gtarget (stake (Suc l) (t @- s)) u) \ {p \ dom (fst (?m !! Suc l)). even (f (Suc l, p))}" using 21 22 23 by (metis (mono_tags, lifting) mem_Collect_eq prod.collapse) also have "\ = st_succ A (w !! l) (fst (?m !! Suc l)) (P l)" unfolding 15(2) st_succ_def f_def by simp also have "\ = P (Suc l)" using 100(2) unfolding P_def by rule also have "P (Suc l) = P (l + Suc 0)" by simp finally show ?case by auto next case (Suc i) have 20: "P (Suc l + i) \ {}" using Suc by auto have 21: "fst (gtarget (stake (Suc l + Suc i) (t @- s)) u) = Suc l + Suc i" using 21 by (simp add: stake_shift) have "gtarget (stake (Suc l + Suc i) (t @- s)) u = gtrace (t @- s) u !! (l + Suc i)" unfolding sscan_snth by simp also have "\ \ gusuccessors A w (gtarget (stake (Suc (l + i)) (t @- s)) u)" using graph.run_snth[OF 30, of "l + Suc i"] by simp finally have 220: "snd (gtarget (stake (Suc (Suc l + i)) (t @- s)) u) \ transition A (w !! (Suc l + i)) (snd (gtarget (stake (Suc (l + i)) (t @- s)) u))" using 21 by auto have 22: "snd (gtarget (stake (Suc l + Suc i) (t @- s)) u) \ \ (transition A (w !! (Suc l + i)) ` P (Suc l + i))" using 220 Suc by auto have "gtarget (stake (Suc l + Suc i) (t @- s)) u = gtrace (t @- s) u !! (l + Suc i)" unfolding sscan_snth by simp also have "\ = gtrace s v !! (l + Suc i - length t)" using 15(1) by (metis add.commute shift_snth_ge sscan_const trans_le_add2) also have "f \ = smap f (gtrace s v) !! (l + Suc i - length t)" by simp also have "smap f (gtrace s v) = sconst k" unfolding 12 by rule also have "sconst k !! (l + Suc i - length t) = k" by simp finally have 23: "even (f (gtarget (stake (Suc l + Suc i) (t @- s)) u))" using 13 by auto have "snd (gtarget (stake (Suc l + Suc i) (t @- s)) u) \ {p \ \ (transition A (w !! (Suc l + i)) ` P (Suc l + i)). even (f (Suc (Suc l + i), p))}" using 21 22 23 by (metis (mono_tags) add_Suc_right mem_Collect_eq prod.collapse) also have "\ = st_succ A (w !! (Suc l + i)) (fst (?m !! Suc (Suc l + i))) (P (Suc l + i))" unfolding st_succ_def f_def using 20 by simp also have "\ = P (Suc (Suc l + i))" unfolding 100(2)[folded P_def] by rule also have "\ = P (Suc l + Suc i)" by simp finally show ?case by this qed show "False" using 16 17 using nat_le_iff_add by auto qed qed qed subsection \Ranking Implies Word in Complement Language\ definition reach where "reach A w i \ {target r p |r p. path A r p \ p \ initial A \ map fst r = stake i w}" lemma reach_0[simp]: "reach A w 0 = initial A" unfolding reach_def by auto lemma reach_Suc_empty: assumes "w !! n \ alphabet A" shows "reach A w (Suc n) = {}" proof safe fix q assume 1: "q \ reach A w (Suc n)" obtain r p where 2: "q = target r p" "path A r p" "p \ initial A" "map fst r = stake (Suc n) w" using 1 unfolding reach_def by blast have 3: "path A (take n r @ drop n r) p" using 2(2) by simp have 4: "map fst r = stake n w @ [w !! n]" using 2(4) stake_Suc by auto have 5: "map snd r = take n (map snd r) @ [q]" using 2(1, 4) 4 by (metis One_nat_def Suc_inject Suc_neq_Zero Suc_pred append.right_neutral append_eq_conv_conj drop_map id_take_nth_drop last_ConsR last_conv_nth length_0_conv length_map length_stake lessI nba.target_alt_def nba.states_alt_def zero_less_Suc) have 6: "drop n r = [(w !! n, q)]" using 4 5 by (metis append_eq_conv_conj append_is_Nil_conv append_take_drop_id drop_map length_greater_0_conv length_stake stake_cycle_le stake_invert_Nil take_map zip_Cons_Cons zip_map_fst_snd) show "q \ {}" using assms 3 unfolding 6 by auto qed lemma reach_Suc_succ: assumes "w !! n \ alphabet A" shows "reach A w (Suc n) = \((transition A (w !! n) ` (reach A w n)))" proof safe fix q assume 1: "q \ reach A w (Suc n)" obtain r p where 2: "q = target r p" "path A r p" "p \ initial A" "map fst r = stake (Suc n) w" using 1 unfolding reach_def by blast have 3: "path A (take n r @ drop n r) p" using 2(2) by simp have 4: "map fst r = stake n w @ [w !! n]" using 2(4) stake_Suc by auto have 5: "map snd r = take n (map snd r) @ [q]" using 2(1, 4) 4 by (metis One_nat_def Suc_inject Suc_neq_Zero Suc_pred append.right_neutral append_eq_conv_conj drop_map id_take_nth_drop last_ConsR last_conv_nth length_0_conv length_map length_stake lessI nba.target_alt_def nba.states_alt_def zero_less_Suc) have 6: "drop n r = [(w !! n, q)]" using 4 5 by (metis append_eq_conv_conj append_is_Nil_conv append_take_drop_id drop_map length_greater_0_conv length_stake stake_cycle_le stake_invert_Nil take_map zip_Cons_Cons zip_map_fst_snd) show "q \ \((transition A (w !! n) ` (reach A w n)))" unfolding reach_def proof (intro UN_I CollectI exI conjI) show "target (take n r) p = target (take n r) p" by rule show "path A (take n r) p" using 3 by blast show "p \ initial A" using 2(3) by this show "map fst (take n r) = stake n w" using 2 by (metis length_stake lessI nat.distinct(1) stake_cycle_le stake_invert_Nil take_map take_stake) show "q \ transition A (w !! n) (target (take n r) p)" using 3 unfolding 6 by auto qed next fix p q assume 1: "p \ reach A w n" "q \ transition A (w !! n) p" obtain r x where 2: "p = target r x" "path A r x" "x \ initial A" "map fst r = stake n w" using 1(1) unfolding reach_def by blast show "q \ reach A w (Suc n)" unfolding reach_def proof (intro CollectI exI conjI) show "q = target (r @ [(w !! n, q)]) x" using 1 2 by auto show "path A (r @ [(w !! n, q)]) x" using assms 1(2) 2(1, 2) by auto show "x \ initial A" using 2(3) by this show "map fst (r @ [(w !! n, q)]) = stake (Suc n) w" using 1 2 by (metis eq_fst_iff list.simps(8) list.simps(9) map_append stake_Suc) qed qed lemma reach_Suc[simp]: "reach A w (Suc n) = (if w !! n \ alphabet A then \((transition A (w !! n) ` (reach A w n))) else {})" using reach_Suc_empty reach_Suc_succ by metis lemma reach_nodes: "reach A w i \ nodes A" by (induct i) (auto) lemma reach_gunodes: "{i} \ reach A w i \ gunodes A w" by (induct i) (auto intro: graph.nodes.execute) lemma ranking_complement: assumes "finite (nodes A)" "w \ streams (alphabet A)" "ranking A w f" shows "w \ language (complement A)" proof - define f' where "f' \ \ (k, p). if k = 0 then 2 * card (nodes A) else f (k, p)" have 0: "ranking A w f'" unfolding ranking_def proof (intro conjI ballI impI allI) show "\ v. v \ gunodes A w \ f' v \ 2 * card (nodes A)" using assms(3) unfolding ranking_def f'_def by auto show "\ v u. v \ gunodes A w \ u \ gusuccessors A w v \ f' u \ f' v" using assms(3) unfolding ranking_def f'_def by fastforce show "\ v. v \ gunodes A w \ gaccepting A v \ even (f' v)" using assms(3) unfolding ranking_def f'_def by auto next have 1: "v \ gunodes A w \ gurun A w r v \ smap f (gtrace r v) = sconst k \ odd k" for v r k using assms(3) unfolding ranking_def by meson fix v r k assume 2: "v \ gunodes A w" "gurun A w r v" "smap f' (gtrace r v) = sconst k" have 20: "shd r \ gureachable A w v" using 2 by (auto) (metis graph.reachable.reflexive graph.reachable_trace gtrace_alt_def subsetD shd_sset) obtain 3: "shd r \ gunodes A w" "gurun A w (stl r) (shd r)" "smap f' (gtrace (stl r) (shd r)) = sconst k" using 2 20 by (metis (no_types, lifting) eq_id_iff graph.nodes_trans graph.run_scons_elim siterate.simps(2) sscan.simps(2) stream.collapse stream.map_sel(2)) have 4: "k \ 0" if "(k, p) \ sset r" for k p proof - obtain ra ka pa where 1: "r = fromN (Suc ka) ||| ra" "v = (ka, pa)" using grun_elim[OF 2(2)] by this have 2: "k \ sset (fromN (Suc ka))" using 1(1) that by (metis image_eqI prod.sel(1) szip_smap_fst stream.set_map) show ?thesis using 2 by simp qed have 5: "smap f' (gtrace (stl r) (shd r)) = smap f (gtrace (stl r) (shd r))" proof (rule stream.map_cong) show "gtrace (stl r) (shd r) = gtrace (stl r) (shd r)" by rule next fix z assume 1: "z \ sset (gtrace (stl r) (shd r))" have 2: "fst z \ 0" using 4 1 by (metis gtrace_alt_def prod.collapse stl_sset) show "f' z = f z" using 2 unfolding f'_def by (auto simp: case_prod_beta) qed show "odd k" using 1 3 5 by simp qed define g where "g i p \ if p \ reach A w i then Some (f' (i, p)) else None" for i p have g_dom[simp]: "dom (g i) = reach A w i" for i unfolding g_def by (auto) (metis option.simps(3)) have g_0[simp]: "g 0 = const (Some (2 * card (nodes A))) |` initial A" unfolding g_def f'_def by auto have g_Suc[simp]: "g (Suc n) \ lr_succ A (w !! n) (g n)" for n unfolding lr_succ_def proof (intro CollectI conjI ballI impI) show "dom (g (Suc n)) = \ (transition A (w !! n) ` dom (g n))" using snth_in assms(2) by auto next fix p q assume 100: "p \ dom (g n)" "q \ transition A (w !! n) p" have 101: "q \ reach A w (Suc n)" using snth_in assms(2) 100 by auto have 102: "(n, p) \ gunodes A w" using 100(1) reach_gunodes g_dom by blast have 103: "(Suc n, q) \ gusuccessors A w (n, p)" using snth_in assms(2) 102 100(2) by auto have 104: "p \ reach A w n" using 100(1) by simp have "g (Suc n) q = Some (f' (Suc n, q))" using 101 unfolding g_def by simp also have "the \ = f' (Suc n, q)" by simp also have "\ \ f' (n, p)" using 0 unfolding ranking_def using 102 103 by simp also have "\ = the (Some (f' (n, p)))" by simp also have "Some (f' (n, p)) = g n p" using 104 unfolding g_def by simp finally show "the (g (Suc n) q) \ the (g n p)" by this next fix p assume 100: "p \ dom (g (Suc n))" "accepting A p" have 101: "p \ reach A w (Suc n)" using 100(1) by simp have 102: "(Suc n, p) \ gunodes A w" using 101 reach_gunodes by blast have 103: "gaccepting A (Suc n, p)" using 100(2) by simp have "the (g (Suc n) p) = f' (Suc n, p)" using 101 unfolding g_def by simp also have "even \" using 0 unfolding ranking_def using 102 103 by auto finally show "even (the (g (Suc n) p))" by this qed define P where "P \ rec_nat {} (\ n. st_succ A (w !! n) (g (Suc n)))" have P_0[simp]: "P 0 = {}" unfolding P_def by simp have P_Suc[simp]: "P (Suc n) = st_succ A (w !! n) (g (Suc n)) (P n)" for n unfolding P_def by simp have P_reach: "P n \ reach A w n" for n using snth_in assms(2) by (induct n) (auto simp add: st_succ_def) have "P n \ reach A w n" for n using P_reach by auto also have "\ n \ nodes A" for n using reach_nodes by this also have "finite (nodes A)" using assms(1) by this finally have P_finite: "finite (P n)" for n by this define s where "s \ smap g nats ||| smap P nats" show ?thesis proof show "run (complement A) (w ||| stl s) (shd s)" proof (intro nba.snth_run conjI, simp_all del: stake.simps stake_szip) fix k show "w !! k \ alphabet (complement A)" using snth_in assms(2) unfolding complement_def by auto have "stl s !! k = s !! Suc k" by simp also have "\ \ complement_succ A (w !! k) (s !! k)" unfolding complement_succ_def s_def using P_Suc by simp also have "\ = complement_succ A (w !! k) (target (stake k (w ||| stl s)) (shd s))" unfolding sscan_scons_snth[symmetric] nba.trace_alt_def by simp also have "\ = transition (complement A) (w !! k) (target (stake k (w ||| stl s)) (shd s))" unfolding complement_def nba.sel by rule finally show "stl s !! k \ transition (complement A) (w !! k) (target (stake k (w ||| stl s)) (shd s))" by this qed show "shd s \ initial (complement A)" unfolding complement_def s_def using P_0 by simp - show "infs (accepting (complement A)) (stl s)" + show "infs (accepting (complement A)) (shd s ## stl s)" proof - have 10: "\ n. \ k \ n. P k = {}" proof (rule ccontr) assume 20: "\ (\ n. \ k \ n. P k = {})" obtain k where 22: "P (k + n) \ {}" for n using 20 using le_add1 by blast define m where "m n S \ {p \ \((transition A (w !! n) ` S)). even (the (g (Suc n) p))}" for n S define R where "R i n S \ rec_nat S (\ i. m (n + i)) i" for i n S have R_0[simp]: "R 0 n = id" for n unfolding R_def by auto have R_Suc[simp]: "R (Suc i) n = m (n + i) \ R i n" for i n unfolding R_def by auto have R_Suc': "R (Suc i) n = R i (Suc n) \ m n" for i n unfolding R_Suc by (induct i) (auto) have R_reach: "R i n S \ reach A w (n + i)" if "S \ reach A w n" for i n S using snth_in assms(2) that m_def by (induct i) (auto) have P_R: "P (k + i) = R i k (P k)" for i using 22 by (induct i) (auto simp add: case_prod_beta' m_def st_succ_def) have 50: "R i n S = (\ p \ S. R i n {p})" for i n S by (induct i) (auto simp add: m_def prod.case_eq_if) have 51: "R (i + j) n S = {}" if "R i n S = {}" for i j n S using that by (induct j) (auto simp add: m_def prod.case_eq_if) have 52: "R j n S = {}" if "i \ j" "R i n S = {}" for i j n S using 51 by (metis le_add_diff_inverse that(1) that(2)) have 1: "\ p \ S. \ i. R i n {p} \ {}" if assms: "finite S" "\ i. R i n S \ {}" for n S proof (rule ccontr) assume 1: "\ (\ p \ S. \ i. R i n {p} \ {})" obtain f where 3: "\ p. p \ S \ R (f p) n {p} = {}" using 1 by metis have 4: "R (Sup (f ` S)) n {p} = {}" if "p \ S" for p proof (rule 52) show "f p \ Sup (f ` S)" using assms(1) that by (auto intro: le_cSup_finite) show "R (f p) n {p} = {}" using 3 that by this qed have "R (Sup (f ` S)) n S = (\ p \ S. R (Sup (f ` S)) n {p})" using 50 by this also have "\ = {}" using 4 by simp finally have 5: "R (Sup (f ` S)) n S = {}" by this show "False" using that(2) 5 by auto qed have 2: "\ i. R i (k + 0) (P k) \ {}" using 22 P_R by simp obtain p where 3: "p \ P k" "\ i. R i k {p} \ {}" using 1[OF P_finite 2] by auto define Q where "Q n p \ (\ i. R i (k + n) {p} \ {}) \ p \ P (k + n)" for n p have 5: "\ q \ transition A (w !! (k + n)) p. Q (Suc n) q" if "Q n p" for n p proof - have 11: "p \ P (k + n)" "\ i. R i (k + n) {p} \ {}" using that unfolding Q_def by auto have 12: "R (Suc i) (k + n) {p} \ {}" for i using 11(2) by this have 13: "R i (k + Suc n) (m (k + n) {p}) \ {}" for i using 12 unfolding R_Suc' by simp have "{p} \ P (k + n)" using 11(1) by auto also have "\ \ reach A w (k + n)" using P_reach by this finally have "R 1 (k + n) {p} \ reach A w (k + n + 1)" using R_reach by blast also have "\ \ nodes A" using reach_nodes by this also have "finite (nodes A)" using assms(1) by this finally have 14: "finite (m (k + n) {p})" by simp obtain q where 14: "q \ m (k + n) {p}" "\ i. R i (k + Suc n) {q} \ {}" using 1[OF 14 13] by auto show ?thesis unfolding Q_def prod.case proof (intro bexI conjI allI) show "\ i. R i (k + Suc n) {q} \ {}" using 14(2) by this show "q \ P (k + Suc n)" using 14(1) 11(1) 22 unfolding m_def by (auto simp add: st_succ_def) show "q \ transition A (w !! (k + n)) p" using 14(1) unfolding m_def by simp qed qed obtain r where 23: "run A r p" "\ i. Q i ((p ## trace r p) !! i)" "\ i. fst (r !! i) = w !! (k + i)" proof (rule nba.invariant_run_index[of Q 0 p A "\ n p a. fst a = w !! (k + n)"]) show "Q 0 p" unfolding Q_def using 3 by auto show "\ a. (fst a \ alphabet A \ snd a \ transition A (fst a) p) \ Q (Suc n) (snd a) \ fst a = w !! (k + n)" if "Q n p" for n p using snth_in assms(2) 5 that by fastforce qed auto have 20: "smap fst r = sdrop k w" using 23(3) by (intro eqI_snth) (simp add: case_prod_beta) have 21: "(p ## smap snd r) !! i \ P (k + i)" for i using 23(2) unfolding Q_def unfolding nba.trace_alt_def by simp obtain r where 23: "run A (sdrop k w ||| stl r) (shd r)" "\ i. r !! i \ P (k + i)" using 20 21 23(1) by (metis stream.sel(1) stream.sel(2) szip_smap) let ?v = "(k, shd r)" let ?r = "fromN (Suc k) ||| stl r" have "shd r = r !! 0" by simp also have "\ \ P k" using 23(2)[of 0] by simp also have "\ \ reach A w k" using P_reach by this finally have 24: "?v \ gunodes A w" using reach_gunodes by blast have 25: "gurun A w ?r ?v" using run_grun 23(1) by this obtain l where 26: "sset (smap f' (gtrace (sdrop l ?r) (gtarget (stake l ?r) ?v))) \ Collect odd" using ranking_stuck_odd 0 24 25 by this have 27: "f' (Suc (k + l), r !! Suc l) = shd (smap f' (gtrace (sdrop l ?r) (gtarget (stake l ?r) ?v)))" by (simp add: algebra_simps) also have "\ \ sset (smap f' (gtrace (sdrop l ?r) (gtarget (stake l ?r) ?v)))" using shd_sset by this also have "\ \ Collect odd" using 26 by this finally have 28: "odd (f' (Suc (k + l), r !! Suc l))" by simp have "r !! Suc l \ P (Suc (k + l))" using 23(2) by (metis add_Suc_right) also have "\ = {p \ \ (transition A (w !! (k + l)) ` P (k + l)). even (the (g (Suc (k + l)) p))}" using 23(2) by (auto simp: st_succ_def) also have "\ \ {p. even (the (g (Suc (k + l)) p))}" by auto finally have 29: "even (the (g (Suc (k + l)) (r !! Suc l)))" by auto have 30: "r !! Suc l \ reach A w (Suc (k + l))" using 23(2) P_reach by (metis add_Suc_right subsetCE) have 31: "even (f' (Suc (k + l), r !! Suc l))" using 29 30 unfolding g_def by simp show "False" using 28 31 by simp qed have 11: "infs (\ k. P k = {}) nats" using 10 unfolding infs_snth by simp have "infs (\ S. S = {}) (smap snd (smap g nats ||| smap P nats))" using 11 by (simp add: comp_def) then have "infs (\ x. snd x = {}) (smap g nats ||| smap P nats)" by (simp add: comp_def del: szip_smap_snd) then have "infs (\ (f, P). P = {}) (smap g nats ||| smap P nats)" by (simp add: case_prod_beta') then have "infs (\ (f, P). P = {}) (stl (smap g nats ||| smap P nats))" by blast then have "infs (\ (f, P). P = {}) (smap snd (w ||| stl (smap g nats ||| smap P nats)))" by simp then have "infs (\ (f, P). P = {}) (stl s)" unfolding s_def by simp then show ?thesis unfolding complement_def by auto qed qed qed subsection \Correctness Theorem\ theorem complement_language: assumes "finite (nodes A)" shows "language (complement A) = streams (alphabet A) - language A" proof (safe del: notI) have 1: "alphabet (complement A) = alphabet A" unfolding complement_def nba.sel by rule show "w \ streams (alphabet A)" if "w \ language (complement A)" for w using nba.language_alphabet that 1 by force show "w \ language A" if "w \ language (complement A)" for w using complement_ranking ranking_language that by metis show "w \ language (complement A)" if "w \ streams (alphabet A)" "w \ language A" for w using language_ranking ranking_complement assms that by blast qed end diff --git a/thys/Buchi_Complementation/Ranking.thy b/thys/Buchi_Complementation/Ranking.thy --- a/thys/Buchi_Complementation/Ranking.thy +++ b/thys/Buchi_Complementation/Ranking.thy @@ -1,478 +1,478 @@ section \Rankings\ theory Ranking imports "Alternate" "Graph" begin subsection \Rankings\ type_synonym 'state ranking = "'state node \ nat" definition ranking :: "('label, 'state) nba \ 'label stream \ 'state ranking \ bool" where "ranking A w f \ (\ v \ gunodes A w. f v \ 2 * card (nodes A)) \ (\ v \ gunodes A w. \ u \ gusuccessors A w v. f u \ f v) \ (\ v \ gunodes A w. gaccepting A v \ even (f v)) \ (\ v \ gunodes A w. \ r k. gurun A w r v \ smap f (gtrace r v) = sconst k \ odd k)" subsection \Ranking Implies Word not in Language\ lemma ranking_stuck: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n k where "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" proof - have 0: "f u \ f v" if "v \ gunodes A w" "u \ gusuccessors A w v" for v u using assms(1) that unfolding ranking_def by auto have 1: "shd (v ## gtrace r v) \ gunodes A w" using assms(2) by auto have 2: "sdescending (smap f (v ## gtrace r v))" using 1 assms(3) proof (coinduction arbitrary: r v rule: sdescending.coinduct) case sdescending obtain u s where 1: "r = u ## s" using stream.exhaust by blast have 2: "v \ gunodes A w" using sdescending(1) by simp have 3: "gurun A w (u ## s) v" using sdescending(2) 1 by auto have 4: "u \ gusuccessors A w v" using 3 by auto have 5: "u \ gureachable A w v" using graph.reachable_successors 4 by blast show ?case unfolding 1 proof (intro exI conjI disjI1) show "f u \ f v" using 0 2 4 by this show "shd (u ## gtrace s u) \ gunodes A w" using 2 5 by auto show "gurun A w s u" using 3 by auto qed auto qed obtain n k where 3: "sdrop n (smap f (v ## gtrace r v)) = sconst k" using sdescending_stuck[OF 2] by metis have "gtrace (sdrop (Suc n) r) (gtarget (stake (Suc n) r) v) = sdrop (Suc n) (gtrace r v)" using sscan_sdrop by rule also have "smap f \ = sdrop n (smap f (v ## gtrace r v))" by (auto, metis 3 id_apply sdrop_smap sdrop_stl siterate.simps(2) sscan_const stream.map stream.map_sel(2) stream.sel(2)) also have "\ = sconst k" using 3 by this finally show ?thesis using that by blast qed lemma ranking_stuck_odd: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n where "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) \ Collect odd" proof - obtain n k where 1: "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" using ranking_stuck assms by this have 2: "gtarget (stake n r) v \ gunodes A w" using assms(2, 3) by (simp add: graph.nodes_target graph.run_stake) have 3: "gurun A w (sdrop n r) (gtarget (stake n r) v)" using assms(2, 3) by (simp add: graph.run_sdrop) have 4: "odd k" using 1 2 3 assms(1) unfolding ranking_def by meson have "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) = sset (sconst k)" unfolding 1 by rule also have "\ \ Collect odd" using 4 by simp finally show ?thesis using that by simp qed lemma ranking_language: assumes "ranking A w f" shows "w \ language A" proof assume 1: "w \ language A" - obtain r p where 2: "run A (w ||| r) p" "p \ initial A" "infs (accepting A) r" using 1 by rule + obtain r p where 2: "run A (w ||| r) p" "p \ initial A" "infs (accepting A) (p ## r)" using 1 by rule let ?r = "fromN 1 ||| r" let ?v = "(0, p)" have 3: "?v \ gunodes A w" "gurun A w ?r ?v" using 2(1, 2) by (auto intro: run_grun) obtain n where 4: "sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v))) \ {a. odd a}" using ranking_stuck_odd assms 3 by this let ?s = "stake n ?r" let ?t = "sdrop n ?r" let ?u = "gtarget ?s ?v" have "sset (gtrace ?t ?u) \ gureachable A w ?v" proof (intro graph.reachable_trace graph.reachable_target graph.reachable.reflexive) show "gupath A w ?s ?v" using graph.run_stake 3(2) by this show "gurun A w ?t ?u" using graph.run_sdrop 3(2) by this qed also have "\ \ gunodes A w" using 3(1) by blast finally have 7: "sset (gtrace ?t ?u) \ gunodes A w" by this have 8: "\ p. p \ gunodes A w \ gaccepting A p \ even (f p)" using assms unfolding ranking_def by auto have 9: "\ p. p \ sset (gtrace ?t ?u) \ gaccepting A p \ even (f p)" using 7 8 by auto have 19: "infs (accepting A) (smap snd ?r)" using 2(3) by simp have 18: "infs (gaccepting A) ?r" using 19 by simp have 17: "infs (gaccepting A) (gtrace ?r ?v)" using 18 unfolding gtrace_alt_def by this have 16: "infs (gaccepting A) (gtrace (?s @- ?t) ?v)" using 17 unfolding stake_sdrop by this have 15: "infs (gaccepting A) (gtrace ?t ?u)" using 16 by simp have 13: "infs (even \ f) (gtrace ?t ?u)" using infs_mono[OF _ 15] 9 by simp have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by (simp add: comp_def) have 11: "Bex (sset (smap f (gtrace ?t ?u))) even" using 12 infs_any by metis show False using 4 11 by auto qed subsection \Word not in Language implies Ranking\ subsubsection \Removal of Endangered Nodes\ definition clean :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "clean A w V \ {v \ V. infinite (greachable A w V v)}" lemma clean_decreasing: "clean A w V \ V" unfolding clean_def by auto lemma clean_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ clean A w V \ v \ clean A w V" proof - assume 1: "u \ clean A w V" have 2: "u \ V" "infinite (greachable A w V u)" using 1 unfolding clean_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast have 5: "infinite (greachable A w V v)" using 2(2) 4 by (simp add: infinite_super) show "v \ clean A w V" unfolding clean_def using assms(1) 5 by simp qed subsubsection \Removal of Safe Nodes\ definition prune :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "prune A w V \ {v \ V. \ u \ greachable A w V v. gaccepting A u}" lemma prune_decreasing: "prune A w V \ V" unfolding prune_def by auto lemma prune_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ prune A w V \ v \ prune A w V" proof - assume 1: "u \ prune A w V" have 2: "u \ V" "\ x \ greachable A w V u. gaccepting A x" using 1 unfolding prune_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast show "v \ prune A w V" unfolding prune_def using assms(1) 2(2) 4 by auto qed subsubsection \Run Graph Interation\ definition graph :: "('label, 'state) nba \ 'label stream \ nat \ 'state node set" where "graph A w k \ alternate (clean A w) (prune A w) k (gunodes A w)" abbreviation "level A w k l \ {v \ graph A w k. fst v = l}" lemma graph_0[simp]: "graph A w 0 = gunodes A w" unfolding graph_def by simp lemma graph_Suc[simp]: "graph A w (Suc k) = (if even k then clean A w else prune A w) (graph A w k)" unfolding graph_def by simp lemma graph_antimono: "antimono (graph A w)" using alternate_antimono clean_decreasing prune_decreasing unfolding antimono_def le_fun_def graph_def by metis lemma graph_nodes: "graph A w k \ gunodes A w" using graph_0 graph_antimono le0 antimonoD by metis lemma graph_successors: assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "u \ graph A w k \ v \ graph A w k" using assms proof (induct k arbitrary: u v) case 0 show ?case using 0(2) by simp next case (Suc k) have 1: "v \ graph A w k" using Suc using antimono_iff_le_Suc graph_antimono rev_subsetD by blast show ?case using Suc(2) clean_successors[OF 1 Suc(4)] prune_successors[OF 1 Suc(4)] by auto qed lemma graph_level_finite: assumes "finite (nodes A)" shows "finite (level A w k l)" proof - have "level A w k l \ {v \ gunodes A w. fst v = l}" by (simp add: graph_nodes subset_CollectI) also have "{v \ gunodes A w. fst v = l} \ {l} \ nodes A" using gnodes_nodes by force also have "finite ({l} \ nodes A)" using assms(1) by simp finally show ?thesis by this qed lemma find_safe: assumes "w \ language A" assumes "V \ {}" "V \ gunodes A w" assumes "\ v. v \ V \ gsuccessors A w V v \ {}" obtains v where "v \ V" "\ u \ greachable A w V v. \ gaccepting A u" proof (rule ccontr) assume 1: "\ thesis" have 2: "\ v. v \ V \ \ u \ greachable A w V v. gaccepting A u" using that 1 by auto have 3: "\ r v. v \ initial A \ run A (w ||| r) v \ fins (accepting A) r" using assms(1) by auto obtain v where 4: "v \ V" using assms(2) by force obtain x where 5: "x \ greachable A w V v" "gaccepting A x" using 2 4 by blast obtain y where 50: "gpath A w V y v" "x = gtarget y v" using 5(1) by rule obtain r where 6: "grun A w V r x" "infs (\ x. x \ V \ gaccepting A x) r" proof (rule graph.recurring_condition) show "x \ V \ gaccepting A x" using greachable_subset 4 5 by blast next fix v assume 1: "v \ V \ gaccepting A v" obtain v' where 20: "v' \ gsuccessors A w V v" using assms(4) 1 by (meson IntE equals0I) have 21: "v' \ V" using 20 by auto have 22: "\ u \ greachable A w V v'. u \ V \ gaccepting A u" using greachable_subset 2 21 by blast obtain r where 30: "gpath A w V r v'" "gtarget r v' \ V \ gaccepting A (gtarget r v')" using 22 by blast show "\ r. r \ [] \ gpath A w V r v \ gtarget r v \ V \ gaccepting A (gtarget r v)" proof (intro exI conjI) show "v' # r \ []" by simp show "gpath A w V (v' # r) v" using 20 30 by auto show "gtarget (v' # r) v \ V" using 30 by simp show "gaccepting A (gtarget (v' # r) v)" using 30 by simp qed qed auto obtain u where 100: "u \ ginitial A" "v \ gureachable A w u" using 4 assms(3) by blast have 101: "gupath A w y v" using gpath_subset 50(1) subset_UNIV by this have 102: "gurun A w r x" using grun_subset 6(1) subset_UNIV by this obtain t where 103: "gupath A w t u" "v = gtarget t u" using 100(2) by rule have 104: "gurun A w (t @- y @- r) u" using 101 102 103 50(2) by auto obtain s q where 7: "t @- y @- r = fromN (Suc 0) ||| s" "u = (0, q)" using grun_elim[OF 104] 100(1) by blast have 8: "run A (w ||| s) q" using grun_run[OF 104[unfolded 7]] by simp have 9: "q \ initial A" using 100(1) 7(2) by auto have 91: "sset (trace (w ||| s) q) \ reachable A q" using nba.reachable_trace nba.reachable.reflexive 8 by this have 10: "fins (accepting A) s" using 3 9 8 by this have 12: "infs (gaccepting A) r" using infs_mono[OF _ 6(2)] by simp have "s = smap snd (t @- y @- r)" unfolding 7(1) by simp also have "infs (accepting A) \" using 12 by (simp add: comp_def) finally have 13: "infs (accepting A) s" by this show False using 10 13 by simp qed lemma remove_run: assumes "finite (nodes A)" "w \ language A" assumes "V \ gunodes A w" "clean A w V \ {}" obtains v r where "grun A w V r v" "sset (gtrace r v) \ clean A w V" "sset (gtrace r v) \ - prune A w (clean A w V)" proof - obtain u where 1: "u \ clean A w V" "\ x \ greachable A w (clean A w V) u. \ gaccepting A x" proof (rule find_safe) show "w \ language A" using assms(2) by this show "clean A w V \ {}" using assms(4) by this show "clean A w V \ gunodes A w" using assms(3) by (meson clean_decreasing subset_iff) next fix v assume 1: "v \ clean A w V" have 2: "v \ V" using 1 clean_decreasing by blast have 3: "infinite (greachable A w V v)" using 1 clean_def by auto have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 2 assms(1, 3) finite_nodes_gsuccessors by blast finally have 4: "finite (gsuccessors A w V v)" by this have 5: "infinite (insert v (\((greachable A w V) ` (gsuccessors A w V v))))" using graph.reachable_step 3 by metis obtain u where 6: "u \ gsuccessors A w V v" "infinite (greachable A w V u)" using 4 5 by auto have 7: "u \ clean A w V" using 6 unfolding clean_def by auto show "gsuccessors A w (clean A w V) v \ {}" using 6(1) 7 by auto qed auto have 2: "u \ V" using 1(1) unfolding clean_def by auto have 3: "infinite (greachable A w V u)" using 1(1) unfolding clean_def by simp have 4: "finite (gsuccessors A w V v)" if "v \ greachable A w V u" for v proof - have 1: "v \ V" using that greachable_subset 2 by blast have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 1 assms(1, 3) finite_nodes_gsuccessors by blast finally show ?thesis by this qed obtain r where 5: "grun A w V r u" using graph.koenig[OF 3 4] by this have 6: "greachable A w V u \ V" using 2 greachable_subset by blast have 7: "sset (gtrace r u) \ V" using graph.reachable_trace[OF graph.reachable.reflexive 5(1)] 6 by blast have 8: "sset (gtrace r u) \ clean A w V" unfolding clean_def using 7 infinite_greachable_gtrace[OF 5(1)] by auto have 9: "sset (gtrace r u) \ greachable A w (clean A w V) u" using 5 8 by (metis graph.reachable.reflexive graph.reachable_trace grun_subset) show ?thesis proof show "grun A w V r u" using 5(1) by this show "sset (gtrace r u) \ clean A w V" using 8 by this show "sset (gtrace r u) \ - prune A w (clean A w V)" proof (intro subsetI ComplI) fix p assume 10: "p \ sset (gtrace r u)" "p \ prune A w (clean A w V)" have 20: "\ x \ greachable A w (clean A w V) p. gaccepting A x" using 10(2) unfolding prune_def by auto have 30: "greachable A w (clean A w V) p \ greachable A w (clean A w V) u" using 10(1) 9 by blast show "False" using 1(2) 20 30 by force qed qed qed lemma level_bounded: assumes "finite (nodes A)" "w \ language A" obtains n where "\ l. l \ n \ card (level A w (2 * k) l) \ card (nodes A) - k" proof (induct k arbitrary: thesis) case (0) show ?case proof (rule 0) fix l :: nat have "finite ({l} \ nodes A)" using assms(1) by simp also have "level A w 0 l \ {l} \ nodes A" using gnodes_nodes by force also (card_mono) have "card \ = card (nodes A)" using assms(1) by simp finally show "card (level A w (2 * 0) l) \ card (nodes A) - 0" by simp qed next case (Suc k) show ?case proof (cases "graph A w (Suc (2 * k)) = {}") case True have 3: "graph A w (2 * Suc k) = {}" using True prune_decreasing by simp blast show ?thesis using Suc(2) 3 by simp next case False obtain v r where 1: "grun A w (graph A w (2 * k)) r v" "sset (gtrace r v) \ graph A w (Suc (2 * k))" "sset (gtrace r v) \ - graph A w (Suc (Suc (2 * k)))" proof (rule remove_run) show "finite (nodes A)" "w \ language A" using assms by this show "clean A w (graph A w (2 * k)) \ {}" using False by simp show "graph A w (2 * k) \ gunodes A w" using graph_nodes by this qed auto obtain l q where 2: "v = (l, q)" by force obtain n where 90: "\ l. n \ l \ card (level A w (2 * k) l) \ card (nodes A) - k" using Suc(1) by blast show ?thesis proof (rule Suc(2)) fix j assume 100: "n + Suc l \ j" have 6: "graph A w (Suc (Suc (2 * k))) \ graph A w (Suc (2 * k))" using graph_antimono antimono_iff_le_Suc by blast have 101: "gtrace r v !! (j - Suc l) \ graph A w (Suc (2 * k))" using 1(2) snth_sset by auto have 102: "gtrace r v !! (j - Suc l) \ graph A w (Suc (Suc (2 * k)))" using 1(3) snth_sset by blast have 103: "gtrace r v !! (j - Suc l) \ level A w (Suc (2 * k)) j" using 1(1) 100 101 2 by (auto elim: grun_elim) have 104: "gtrace r v !! (j - Suc l) \ level A w (Suc (Suc (2 * k))) j" using 100 102 by simp have "level A w (2 * Suc k) j = level A w (Suc (Suc (2 * k))) j" by simp also have "\ \ level A w (Suc (2 * k)) j" using 103 104 6 by blast also have "\ \ level A w (2 * k) j" by (simp add: Collect_mono clean_def) finally have 105: "level A w (2 * Suc k) j \ level A w (2 * k) j" by this have "card (level A w (2 * Suc k) j) < card (level A w (2 * k) j)" using assms(1) 105 by (simp add: graph_level_finite psubset_card_mono) also have "\ \ card (nodes A) - k" using 90 100 by simp finally show "card (level A w (2 * Suc k) j) \ card (nodes A) - Suc k" by simp qed qed qed lemma graph_empty: assumes "finite (nodes A)" "w \ language A" shows "graph A w (Suc (2 * card (nodes A))) = {}" proof - obtain n where 1: "\ l. l \ n \ card (level A w (2 * card (nodes A)) l) = 0" using level_bounded[OF assms(1, 2), of "card (nodes A)"] by auto have "graph A w (2 * card (nodes A)) = (\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ (\ l \ {n ..}. level A w (2 * card (nodes A)) l)" by auto also have "(\ l \ {n ..}. level A w (2 * card (nodes A)) l) = {}" using graph_level_finite assms(1) 1 by fastforce also have "finite ((\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ {})" using graph_level_finite assms(1) by auto finally have 100: "finite (graph A w (2 * card (nodes A)))" by this have 101: "finite (greachable A w (graph A w (2 * card (nodes A))) v)" for v using 100 greachable_subset[of A w "graph A w (2 * card (nodes A))" v] using finite_insert infinite_super by auto show ?thesis using 101 by (simp add: clean_def) qed lemma graph_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ graph A w k" shows "k \ 2 * card (nodes A)" using graph_empty graph_antimono assms by (metis (no_types, lifting) Suc_leI antimono_def basic_trans_rules(30) empty_iff not_le_imp_less) subsection \Node Ranks\ definition rank :: "('label, 'state) nba \ 'label stream \ 'state node \ nat" where "rank A w v \ GREATEST k. v \ graph A w k" lemma rank_member: assumes "finite (nodes A)" "w \ language A" "v \ gunodes A w" shows "v \ graph A w (rank A w v)" unfolding rank_def proof (rule GreatestI_nat) show "v \ graph A w 0" using assms(3) by simp show "\ k. v \ graph A w k \ k \ 2 * card (nodes A)" using graph_le assms(1, 2) by blast qed lemma rank_removed: assumes "finite (nodes A)" "w \ language A" shows "v \ graph A w (Suc (rank A w v))" proof assume "v \ graph A w (Suc (rank A w v))" then have 2: "Suc (rank A w v) \ rank A w v" unfolding rank_def using Greatest_le_nat graph_le assms by metis then show "False" by auto qed lemma rank_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "rank A w u \ rank A w v" unfolding rank_def proof (rule Greatest_le_nat) have 1: "u \ gureachable A w v" using graph.reachable_successors assms(4) by blast have 2: "u \ gunodes A w" using assms(3) 1 by auto show "v \ graph A w (GREATEST k. u \ graph A w k)" unfolding rank_def[symmetric] proof (rule graph_successors) show "v \ gunodes A w" using assms(3) by this show "u \ gusuccessors A w v" using assms(4) by this show "u \ graph A w (rank A w u)" using rank_member assms(1, 2) 2 by this qed show "\ k. v \ graph A w k \ k \ 2 * card (nodes A)" using graph_le assms(1, 2) by blast qed lemma language_ranking: assumes "finite (nodes A)" "w \ language A" shows "ranking A w (rank A w)" unfolding ranking_def proof (intro conjI ballI allI impI) fix v assume 1: "v \ gunodes A w" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1 by this show "rank A w v \ 2 * card (nodes A)" using graph_le assms 2 by this next fix v u assume 1: "v \ gunodes A w" "u \ gusuccessors A w v" show "rank A w u \ rank A w v" using rank_le assms 1 by this next fix v assume 1: "v \ gunodes A w" "gaccepting A v" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1(1) by this have 3: "v \ graph A w (Suc (rank A w v))" using rank_removed assms by this have 4: "v \ prune A w (graph A w (rank A w v))" using 2 1(2) unfolding prune_def by auto have 5: "graph A w (Suc (rank A w v)) \ prune A w (graph A w (rank A w v))" using 3 4 by blast show "even (rank A w v)" using 5 by auto next fix v r k assume 1: "v \ gunodes A w" "gurun A w r v" "smap (rank A w) (gtrace r v) = sconst k" have "sset (gtrace r v) \ gureachable A w v" using 1(2) by (metis graph.reachable.reflexive graph.reachable_trace) then have 6: "sset (gtrace r v) \ gunodes A w" using 1(1) by blast have 60: "rank A w ` sset (gtrace r v) \ {k}" using 1(3) by (metis equalityD1 sset_sconst stream.set_map) have 50: "sset (gtrace r v) \ graph A w k" using rank_member[OF assms] subsetD[OF 6] 60 unfolding image_subset_iff by auto have 70: "grun A w (graph A w k) r v" using grun_subset 1(2) 50 by this have 7: "sset (gtrace r v) \ clean A w (graph A w k)" unfolding clean_def using 50 infinite_greachable_gtrace[OF 70] by auto have 8: "sset (gtrace r v) \ graph A w (Suc k) = {}" using rank_removed[OF assms] 60 by blast have 9: "sset (gtrace r v) \ {}" using stream.set_sel(1) by auto have 10: "graph A w (Suc k) \ clean A w (graph A w k)" using 7 8 9 by blast show "odd k" using 10 unfolding graph_Suc by auto qed subsection \Correctness Theorem\ theorem language_ranking_iff: assumes "finite (nodes A)" shows "w \ language A \ (\ f. ranking A w f)" using ranking_language language_ranking assms by blast end diff --git a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA.thy --- a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA.thy @@ -1,29 +1,29 @@ section \Deterministic Büchi Automata\ theory DBA imports "../Deterministic" begin datatype ('label, 'state) dba = dba (alphabet: "'label set") (initial: "'state") (transition: "'label \ 'state \ 'state") (accepting: "'state pred") (* TODO: if we interpret everything at once, some abbreviations don't get folded back see DBA_Combine.intersection_list.combine_finite *) global_interpretation dba: automaton dba alphabet initial transition accepting defines path = dba.path and run = dba.run and reachable = dba.reachable and nodes = dba.nodes by unfold_locales auto - global_interpretation dba: automaton_run dba alphabet initial transition accepting "\ P w r p. infs P r" + global_interpretation dba: automaton_run dba alphabet initial transition accepting "\ P w r p. infs P (p ## r)" defines language = dba.language by standard abbreviation target where "target \ dba.target" abbreviation states where "states \ dba.states" abbreviation trace where "trace \ dba.trace" (* TODO: why does this happen? if I can fix it here, why can't the interpretation do it? same happens with reachable, requiring the use of defines directives *) abbreviation successors where "successors \ dba.successors TYPE('label)" end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy @@ -1,108 +1,108 @@ section \Deterministic Büchi Automata Combinations\ theory DBA_Combine imports DBA DGBA begin global_interpretation degeneralization: automaton_degeneralization_run - dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P r" - dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" + dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P (p ## r)" + dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" fst id defines degeneralize = degeneralization.degeneralize by (unfold_locales) (auto simp flip: sscan_smap) lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DBA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DBA.nodes_def] lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DBA.nodes_def] global_interpretation intersection: automaton_intersection_run - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" - dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P r" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" + dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ fst, c\<^sub>2 \ snd]" defines intersect' = intersection.combine by unfold_locales auto lemmas intersect'_language[simp] = intersection.combine_language[folded DGBA.language_def] lemmas intersect'_nodes_finite = intersection.combine_nodes_finite[folded DGBA.nodes_def] lemmas intersect'_nodes_card = intersection.combine_nodes_card[folded DGBA.nodes_def] global_interpretation union: automaton_union_run - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" "\ c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \ fst) pq \ (c\<^sub>2 \ snd) pq" defines union = union.combine by (unfold_locales) (simp del: comp_apply) lemmas union_language = union.combine_language lemmas union_nodes_finite = union.combine_nodes_finite lemmas union_nodes_card = union.combine_nodes_card global_interpretation intersection_list: automaton_intersection_list_run - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" - dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P r" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" + dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P (p ## r)" "\ cs. map (\ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]" defines intersect_list' = intersection_list.combine by (unfold_locales) (auto simp: gen_def comp_def) lemmas intersect_list'_language[simp] = intersection_list.combine_language[folded DGBA.language_def] lemmas intersect_list'_nodes_finite = intersection_list.combine_nodes_finite[folded DGBA.nodes_def] lemmas intersect_list'_nodes_card = intersection_list.combine_nodes_card[folded DGBA.nodes_def] global_interpretation union_list: automaton_union_list_run - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" "\ cs pp. \ k < length cs. (cs ! k) (pp ! k)" defines union_list = union_list.combine by (unfold_locales) (simp add: comp_def) lemmas union_list_language = union_list.combine_language lemmas union_list_nodes_finite = union_list.combine_nodes_finite lemmas union_list_nodes_card = union_list.combine_nodes_card (* TODO: these compound definitions are annoying, can we move those into Deterministic theory *) abbreviation intersect where "intersect A B \ degeneralize (intersect' A B)" lemma intersect_language[simp]: "DBA.language (intersect A B) = DBA.language A \ DBA.language B" by simp lemma intersect_nodes_finite: assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)" shows "finite (DBA.nodes (intersect A B))" using intersect'_nodes_finite assms by simp lemma intersect_nodes_card: assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)" shows "card (DBA.nodes (intersect A B)) \ 2 * card (DBA.nodes A) * card (DBA.nodes B)" proof - have "card (DBA.nodes (intersect A B)) \ max 1 (length (dgba.accepting (intersect' A B))) * card (DGBA.nodes (intersect' A B))" using degeneralize_nodes_card by this also have "length (dgba.accepting (intersect' A B)) = 2" by simp also have "card (DGBA.nodes (intersect' A B)) \ card (DBA.nodes A) * card (DBA.nodes B)" using intersect'_nodes_card assms by this finally show ?thesis by simp qed abbreviation intersect_list where "intersect_list AA \ degeneralize (intersect_list' AA)" lemma intersect_list_language[simp]: "DBA.language (intersect_list AA) = \ (DBA.language ` set AA)" by simp lemma intersect_list_nodes_finite: assumes "list_all (finite \ DBA.nodes) AA" shows "finite (DBA.nodes (intersect_list AA))" using intersect_list'_nodes_finite assms by simp lemma intersect_list_nodes_card: assumes "list_all (finite \ DBA.nodes) AA" shows "card (DBA.nodes (intersect_list AA)) \ max 1 (length AA) * prod_list (map (card \ DBA.nodes) AA)" proof - have "card (DBA.nodes (intersect_list AA)) \ max 1 (length (dgba.accepting (intersect_list' AA))) * card (DGBA.nodes (intersect_list' AA))" using degeneralize_nodes_card by this also have "length (dgba.accepting (intersect_list' AA)) = length AA" by simp also have "card (DGBA.nodes (intersect_list' AA)) \ prod_list (map (card \ DBA.nodes) AA)" using intersect_list'_nodes_card assms by this finally show ?thesis by simp qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy --- a/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy @@ -1,25 +1,25 @@ section \Deterministic Generalized Büchi Automata\ theory DGBA imports "../Deterministic" begin datatype ('label, 'state) dgba = dgba (alphabet: "'label set") (initial: "'state") (transition: "'label \ 'state \ 'state") (accepting: "'state pred gen") global_interpretation dgba: automaton dgba alphabet initial transition accepting defines path = dgba.path and run = dgba.run and reachable = dgba.reachable and nodes = dgba.nodes by unfold_locales auto - global_interpretation dgba: automaton_run dgba alphabet initial transition accepting "\ P w r p. gen infs P r" + global_interpretation dgba: automaton_run dgba alphabet initial transition accepting "\ P w r p. gen infs P (p ## r)" defines language = dgba.language by standard abbreviation target where "target \ dgba.target" abbreviation states where "states \ dgba.states" abbreviation trace where "trace \ dgba.trace" abbreviation successors where "successors \ dgba.successors TYPE('label)" end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy --- a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy @@ -1,25 +1,25 @@ section \Deterministic Co-Büchi Automata\ theory DCA imports "../Deterministic" begin datatype ('label, 'state) dca = dca (alphabet: "'label set") (initial: "'state") (transition: "'label \ 'state \ 'state") (rejecting: "'state \ bool") global_interpretation dca: automaton dca alphabet initial transition rejecting defines path = dca.path and run = dca.run and reachable = dca.reachable and nodes = dca.nodes by unfold_locales auto - global_interpretation dca: automaton_run dca alphabet initial transition rejecting "\ P w r p. fins P r" + global_interpretation dca: automaton_run dca alphabet initial transition rejecting "\ P w r p. fins P (p ## r)" defines language = dca.language by standard abbreviation target where "target \ dca.target" abbreviation states where "states \ dca.states" abbreviation trace where "trace \ dca.trace" abbreviation successors where "successors \ dca.successors TYPE('label)" end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy @@ -1,110 +1,110 @@ section \Deterministic Co-Büchi Automata Combinations\ theory DCA_Combine imports DCA DGCA begin global_interpretation degeneralization: automaton_degeneralization_run - dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P r" - dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" + dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P (p ## r)" + dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" fst id defines degeneralize = degeneralization.degeneralize by (unfold_locales) (auto simp flip: sscan_smap) lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DCA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DCA.nodes_def] lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DCA.nodes_def] global_interpretation intersection: automaton_intersection_run - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" "\ c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \ fst) pq \ (c\<^sub>2 \ snd) pq" defines intersect = intersection.combine by (unfold_locales) (simp del: comp_apply) lemmas intersect_language = intersection.combine_language lemmas intersect_nodes_finite = intersection.combine_nodes_finite lemmas intersect_nodes_card = intersection.combine_nodes_card global_interpretation union: automaton_union_run - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" - dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P r" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" + dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ fst, c\<^sub>2 \ snd]" defines union' = union.combine by unfold_locales auto lemmas union'_language[simp] = union.combine_language[folded DGCA.language_def] lemmas union'_nodes_finite = union.combine_nodes_finite[folded DGCA.nodes_def] lemmas union'_nodes_card = union.combine_nodes_card[folded DGCA.nodes_def] global_interpretation intersection_list: automaton_intersection_list_run - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" "\ cs pp. \ k < length cs. (cs ! k) (pp ! k)" defines intersect_list = intersection_list.combine by (unfold_locales) (simp add: comp_def) lemmas intersect_list_language = intersection_list.combine_language lemmas intersect_list_nodes_finite = intersection_list.combine_nodes_finite lemmas intersect_list_nodes_card = intersection_list.combine_nodes_card global_interpretation union_list: automaton_union_list_run - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" - dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P r" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" + dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P (p ## r)" "\ cs. map (\ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]" defines union_list' = union_list.combine by (unfold_locales) (auto simp: cogen_def comp_def) lemmas union_list'_language[simp] = union_list.combine_language[folded DGCA.language_def] lemmas union_list'_nodes_finite = union_list.combine_nodes_finite[folded DGCA.nodes_def] lemmas union_list'_nodes_card = union_list.combine_nodes_card[folded DGCA.nodes_def] abbreviation union where "union A B \ degeneralize (union' A B)" lemma union_language[simp]: assumes "dca.alphabet A = dca.alphabet B" shows "DCA.language (union A B) = DCA.language A \ DCA.language B" using assms by simp lemma union_nodes_finite: assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)" shows "finite (DCA.nodes (union A B))" using union'_nodes_finite assms by simp lemma union_nodes_card: assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)" shows "card (DCA.nodes (union A B)) \ 2 * card (DCA.nodes A) * card (DCA.nodes B)" proof - have "card (DCA.nodes (union A B)) \ max 1 (length (dgca.rejecting (union' A B))) * card (DGCA.nodes (union' A B))" using degeneralize_nodes_card by this also have "length (dgca.rejecting (union' A B)) = 2" by simp also have "card (DGCA.nodes (union' A B)) \ card (DCA.nodes A) * card (DCA.nodes B)" using union'_nodes_card assms by this finally show ?thesis by simp qed abbreviation union_list where "union_list AA \ degeneralize (union_list' AA)" lemma union_list_language[simp]: assumes "\ (dca.alphabet ` set AA) = \ (dca.alphabet ` set AA)" shows "DCA.language (union_list AA) = \ (DCA.language ` set AA)" using assms by simp lemma union_list_nodes_finite: assumes "list_all (finite \ DCA.nodes) AA" shows "finite (DCA.nodes (union_list AA))" using union_list'_nodes_finite assms by simp lemma union_list_nodes_card: assumes "list_all (finite \ DCA.nodes) AA" shows "card (DCA.nodes (union_list AA)) \ max 1 (length AA) * prod_list (map (card \ DCA.nodes) AA)" proof - have "card (DCA.nodes (union_list AA)) \ max 1 (length (dgca.rejecting (union_list' AA))) * card (DGCA.nodes (union_list' AA))" using degeneralize_nodes_card by this also have "length (dgca.rejecting (union_list' AA)) = length AA" by simp also have "card (DGCA.nodes (union_list' AA)) \ prod_list (map (card \ DCA.nodes) AA)" using union_list'_nodes_card assms by this finally show ?thesis by simp qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DGCA.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DGCA.thy --- a/thys/Transition_Systems_and_Automata/Automata/DCA/DGCA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DGCA.thy @@ -1,25 +1,25 @@ section \Deterministic Co-Generalized Co-Büchi Automata\ theory DGCA imports "../Deterministic" begin datatype ('label, 'state) dgca = dgca (alphabet: "'label set") (initial: "'state") (transition: "'label \ 'state \ 'state") (rejecting: "'state pred gen") global_interpretation dgca: automaton dgca alphabet initial transition rejecting defines path = dgca.path and run = dgca.run and reachable = dgca.reachable and nodes = dgca.nodes by unfold_locales auto - global_interpretation dgca: automaton_run dgca alphabet initial transition rejecting "\ P w r p. cogen fins P r" + global_interpretation dgca: automaton_run dgca alphabet initial transition rejecting "\ P w r p. cogen fins P (p ## r)" defines language = dgca.language by standard abbreviation target where "target \ dgca.target" abbreviation states where "states \ dgca.states" abbreviation trace where "trace \ dgca.trace" abbreviation successors where "successors \ dgca.successors TYPE('label)" end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA.thy b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA.thy --- a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA.thy @@ -1,25 +1,25 @@ section \Deterministic Rabin Automata\ theory DRA imports "../Deterministic" begin datatype ('label, 'state) dra = dra (alphabet: "'label set") (initial: "'state") (transition: "'label \ 'state \ 'state") (condition: "'state rabin gen") global_interpretation dra: automaton dra alphabet initial transition condition defines path = dra.path and run = dra.run and reachable = dra.reachable and nodes = dra.nodes by unfold_locales auto - global_interpretation dra: automaton_run dra alphabet initial transition condition "\ P w r p. cogen rabin P r" + global_interpretation dra: automaton_run dra alphabet initial transition condition "\ P w r p. cogen rabin P (p ## r)" defines language = dra.language by standard abbreviation target where "target \ dra.target" abbreviation states where "states \ dra.states" abbreviation trace where "trace \ dra.trace" abbreviation successors where "successors \ dra.successors TYPE('label)" end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy @@ -1,33 +1,33 @@ section \Deterministic Rabin Automata Combinations\ theory DRA_Combine imports "DRA" "../DBA/DBA" "../DCA/DCA" begin global_interpretation intersection_bc: automaton_intersection_run - dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P r" - dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P r" - dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P r" + dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" + dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" + dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [(c\<^sub>1 \ fst, c\<^sub>2 \ snd)]" defines intersect_bc = intersection_bc.combine by (unfold_locales) (simp add: cogen_def rabin_def) (* TODO: why are only the constants of the first interpretation folded back correctly? *) lemmas intersect_bc_language[simp] = intersection_bc.combine_language[folded DCA.language_def DRA.language_def] lemmas intersect_bc_nodes_finite = intersection_bc.combine_nodes_finite[folded DCA.nodes_def DRA.nodes_def] lemmas intersect_bc_nodes_card = intersection_bc.combine_nodes_card[folded DCA.nodes_def DRA.nodes_def] (* TODO: are there some statements about the rabin constant hidden in here? same for gen/cogen, also in other combinations, shouldn't have to unfold those *) global_interpretation union_list: automaton_union_list_run - dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P r" - dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P r" + dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P (p ## r)" + dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P (p ## r)" "\ cs. do { k \ [0 ..< length cs]; (f, g) \ cs ! k; [(\ pp. f (pp ! k), \ pp. g (pp ! k))] }" defines union_list = union_list.combine by (unfold_locales) (auto simp: cogen_def rabin_def comp_def split_beta) lemmas union_list_language = union_list.combine_language lemmas union_list_nodes_finite = union_list.combine_nodes_finite lemmas union_list_nodes_card = union_list.combine_nodes_card end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Refine.thy b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Refine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Refine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Refine.thy @@ -1,88 +1,88 @@ section \Relations on Deterministic Rabin Automata\ theory DRA_Refine imports "DRA" "../../Basic/Acceptance_Refine" "../../Transition_Systems/Transition_System_Refine" begin definition dra_rel :: "('label\<^sub>1 \ 'label\<^sub>2) set \ ('state\<^sub>1 \ 'state\<^sub>2) set \ (('label\<^sub>1, 'state\<^sub>1) dra \ ('label\<^sub>2, 'state\<^sub>2) dra) set" where [to_relAPP]: "dra_rel L S \ {(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \ \L\ set_rel \ (initial A\<^sub>1, initial A\<^sub>2) \ S \ (transition A\<^sub>1, transition A\<^sub>2) \ L \ S \ S \ (condition A\<^sub>1, condition A\<^sub>2) \ \rabin_rel S\ list_rel}" lemma dra_param[param]: "(dra, dra) \ \L\ set_rel \ S \ (L \ S \ S) \ \rabin_rel S\ list_rel \ \L, S\ dra_rel" "(alphabet, alphabet) \ \L, S\ dra_rel \ \L\ set_rel" "(initial, initial) \ \L, S\ dra_rel \ S" "(transition, transition) \ \L, S\ dra_rel \ L \ S \ S" "(condition, condition) \ \L, S\ dra_rel \ \rabin_rel S\ list_rel" unfolding dra_rel_def fun_rel_def by auto lemma dra_rel_id[simp]: "\Id, Id\ dra_rel = Id" unfolding dra_rel_def using dra.expand by auto lemma dra_rel_comp[trans]: assumes [param]: "(A, B) \ \L\<^sub>1, S\<^sub>1\ dra_rel" "(B, C) \ \L\<^sub>2, S\<^sub>2\ dra_rel" shows "(A, C) \ \L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\ dra_rel" proof - have "(condition A, condition B) \ \rabin_rel S\<^sub>1\ list_rel" by parametricity also have "(condition B, condition C) \ \rabin_rel S\<^sub>2\ list_rel" by parametricity finally have 1: "(condition A, condition C) \ \rabin_rel S\<^sub>1 O rabin_rel S\<^sub>2\ list_rel" by simp have 2: "rabin_rel S\<^sub>1 O rabin_rel S\<^sub>2 \ rabin_rel (S\<^sub>1 O S\<^sub>2)" by (force simp: fun_rel_def) have 3: "(condition A, condition C) \ \rabin_rel (S\<^sub>1 O S\<^sub>2)\ list_rel" using 1 2 list_rel_mono by blast have "(transition A, transition B) \ L\<^sub>1 \ S\<^sub>1 \ S\<^sub>1" by parametricity also have "(transition B, transition C) \ L\<^sub>2 \ S\<^sub>2 \ S\<^sub>2" by parametricity finally have 4: "(transition A, transition C) \ L\<^sub>1 O L\<^sub>2 \ S\<^sub>1 O S\<^sub>2 \ S\<^sub>1 O S\<^sub>2" by this show ?thesis unfolding dra_rel_def mem_Collect_eq prod.case set_rel_compp using 3 4 using dra_param(2 - 5)[THEN fun_relD, OF assms(1)] using dra_param(2 - 5)[THEN fun_relD, OF assms(2)] by auto qed lemma dra_rel_converse[simp]: "(\L, S\ dra_rel)\ = \L\, S\\ dra_rel" proof - have 1: "\L\ set_rel = (\L\\ set_rel)\" by simp have 2: "\S\ set_rel = (\S\\ set_rel)\" by simp have 3: "L \ S \ S = (L\ \ S\ \ S\)\" by simp have 4: "\rabin_rel S\ list_rel = (\rabin_rel (S\)\ list_rel)\" by simp show ?thesis unfolding dra_rel_def unfolding 3 unfolding 1 2 4 by fastforce qed lemma dra_rel_eq: "(A, A) \ \Id_on (alphabet A), Id_on (nodes A)\ dra_rel" unfolding dra_rel_def prod_rel_def using list_all2_same[to_set] by auto lemma enableds_param[param]: "(dra.enableds, dra.enableds) \ \L, S\ dra_rel \ S \ \L\ set_rel" unfolding dra.enableds_def Collect_mem_eq by parametricity lemma paths_param[param]: "(dra.paths, dra.paths) \ \L, S\ dra_rel \ S \ \\L\ list_rel\ set_rel" using enableds_param[param_fo] by parametricity lemma runs_param[param]: "(dra.runs, dra.runs) \ \L, S\ dra_rel \ S \ \\L\ stream_rel\ set_rel" using enableds_param[param_fo] by parametricity lemma reachable_param[param]: "(reachable, reachable) \ \L, S\ dra_rel \ S \ \S\ set_rel" proof - have 1: "reachable A p = (\ w. target A w p) ` dra.paths A p" for A :: "('label, 'state) dra" and p unfolding dra.reachable_alt_def dra.paths_def by auto show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity qed lemma nodes_param[param]: "(nodes, nodes) \ \L, S\ dra_rel \ \S\ set_rel" proof - have 1: "nodes A = reachable A (initial A)" for A :: "('label, 'state) dra" unfolding dra.nodes_alt_def by simp show ?thesis unfolding 1 by parametricity qed lemma language_param[param]: "(language, language) \ \L, S\ dra_rel \ \\L\ stream_rel\ set_rel" proof - have 1: "language A = (\ w \ dra.runs A (initial A). - if cogen rabin (condition A) (trace A w (initial A)) then {w} else {})" + if cogen rabin (condition A) (initial A ## trace A w (initial A)) then {w} else {})" for A :: "('label, 'state) dra" unfolding dra.language_def dra.runs_def by auto show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA.thy @@ -1,100 +1,100 @@ section \Nondeterministic Büchi Automata\ theory NBA imports "../Nondeterministic" begin datatype ('label, 'state) nba = nba (alphabet: "'label set") (initial: "'state set") (transition: "'label \ 'state \ 'state set") (accepting: "'state pred") global_interpretation nba: automaton nba alphabet initial transition accepting defines path = nba.path and run = nba.run and reachable = nba.reachable and nodes = nba.nodes by unfold_locales auto - global_interpretation nba: automaton_run nba alphabet initial transition accepting "\ P w r p. infs P r" + global_interpretation nba: automaton_run nba alphabet initial transition accepting "\ P w r p. infs P (p ## r)" defines language = nba.language by standard abbreviation target where "target \ nba.target" abbreviation states where "states \ nba.states" abbreviation trace where "trace \ nba.trace" abbreviation successors where "successors \ nba.successors TYPE('label)" instantiation nba :: (type, type) order begin definition less_eq_nba :: "('a, 'b) nba \ ('a, 'b) nba \ bool" where "A \ B \ alphabet A \ alphabet B \ initial A \ initial B \ transition A \ transition B \ accepting A \ accepting B" definition less_nba :: "('a, 'b) nba \ ('a, 'b) nba \ bool" where "less_nba A B \ A \ B \ A \ B" instance by (intro_classes) (auto simp: less_eq_nba_def less_nba_def nba.expand) end lemma nodes_mono: "mono nodes" proof fix A B :: "('label, 'state) nba" assume 1: "A \ B" have 2: "alphabet A \ alphabet B" using 1 unfolding less_eq_nba_def by auto have 3: "initial A \ initial B" using 1 unfolding less_eq_nba_def by auto have 4: "transition A a p \ transition B a p" for a p using 1 unfolding less_eq_nba_def le_fun_def by auto have 5: "p \ nodes B" if "p \ nodes A" for p using that 2 3 4 by induct fastforce+ show "nodes A \ nodes B" using 5 by auto qed lemma language_mono: "mono language" proof fix A B :: "('label, 'state) nba" assume 1: "A \ B" have 2: "alphabet A \ alphabet B" using 1 unfolding less_eq_nba_def by auto have 3: "initial A \ initial B" using 1 unfolding less_eq_nba_def by auto have 4: "transition A a p \ transition B a p" for a p using 1 unfolding less_eq_nba_def le_fun_def by auto have 5: "accepting A p \ accepting B p" for p using 1 unfolding less_eq_nba_def by auto have 6: "run B wr p" if "run A wr p" for wr p using that 2 4 by coinduct auto have 7: "infs (accepting B) w" if "infs (accepting A) w" for w using infs_mono that 5 by metis show "language A \ language B" using 3 6 7 by blast qed lemma simulation_language: assumes "alphabet A \ alphabet B" assumes "\ p. p \ initial A \ \ q \ initial B. (p, q) \ R" assumes "\ a p p' q. p' \ transition A a p \ (p, q) \ R \ \ q' \ transition B a q. (p', q') \ R" assumes "\ p q. (p, q) \ R \ accepting A p \ accepting B q" shows "language A \ language B" proof fix w assume 1: "w \ language A" - obtain r p where 2: "p \ initial A" "run A (w ||| r) p" "infs (accepting A) r" using 1 by rule + obtain r p where 2: "p \ initial A" "run A (w ||| r) p" "infs (accepting A) (p ## r)" using 1 by rule define P where "P n q \ (target (stake n (w ||| r)) p, q) \ R" for n q obtain q where 3: "q \ initial B" "(p, q) \ R" using assms(2) 2(1) by auto obtain ws where 4: "run B ws q" "\ i. P (0 + i) (target (stake i ws) q)" "\ i. fst (ws !! i) = w !! (0 + i)" proof (rule nba.invariant_run_index) have "stake k (w ||| r) @- (w !! k, target (stake (Suc k) (w ||| r)) p) ## sdrop (Suc k) (w ||| r) = w ||| r" for k by (metis id_stake_snth_sdrop snth_szip sscan_snth szip_smap_snd nba.trace_alt_def) also have "run A \ p" using 2(2) by this finally show "\ a. (fst a \ alphabet B \ snd a \ transition B (fst a) q) \ P (Suc n) (snd a) \ fst a = w !! n" if "P n q" for n q using assms(1, 3) that unfolding P_def by fastforce show "P 0 q" unfolding P_def using 3(2) by auto qed rule obtain s where 5: "ws = w ||| s" using 4(3) by (metis add.left_neutral eqI_snth snth_smap szip_smap) show "w \ language B" proof show "q \ initial B" using 3(1) by this show "run B (w ||| s) q" using 4(1) unfolding 5 by this have 6: "(\ a b. (a, b) \ R) \ (\ a b. accepting A a \ accepting B b)" using assms(4) by auto have 7: "stream_all2 (\ p q. (p, q) \ R) (trace (w ||| r) p) (trace (w ||| s) q)" using 4(2) unfolding P_def 5 by (simp add: stream_rel_snth del: stake.simps(2)) have 8: "stream_all2 (\ a b. accepting A a \ accepting B b) r s" using stream.rel_mono 6 7 unfolding nba.trace_alt_def by auto - show "infs (accepting B) s" using infs_mono_strong 8 2(3) by this + show "infs (accepting B) (q ## s)" using infs_mono_strong 8 2(3) by simp qed qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy @@ -1,90 +1,90 @@ section \Nondeterministic Büchi Automata Combinations\ theory NBA_Combine imports NBA NGBA begin global_interpretation degeneralization: automaton_degeneralization_run - ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P r" - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" + ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P (p ## r)" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" fst id defines degeneralize = degeneralization.degeneralize by (unfold_locales) (auto simp flip: sscan_smap) lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded NBA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded NBA.nodes_def] global_interpretation intersection: automaton_intersection_run - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" - ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P r" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" + ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ fst, c\<^sub>2 \ snd]" defines intersect' = intersection.intersect by unfold_locales auto lemmas intersect'_language[simp] = intersection.intersect_language[folded NGBA.language_def] lemmas intersect'_nodes_finite[intro] = intersection.intersect_nodes_finite[folded NGBA.nodes_def] global_interpretation union: automaton_union_run - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" case_sum defines union = union.union by (unfold_locales) (auto simp: comp_def) lemmas union_language = union.union_language lemmas union_nodes_finite = union.union_nodes_finite global_interpretation intersection_list: automaton_intersection_list_run - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" - ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P r" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" + ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P (p ## r)" "\ cs. map (\ k ps. (cs ! k) (ps ! k)) [0 ..< length cs]" defines intersect_list' = intersection_list.intersect proof unfold_locales fix cs :: "('b \ bool) list" and rs :: "'b stream list" and w :: "'a stream" and ps :: "'b list" assume 1: "length rs = length cs" "length ps = length cs" - have "gen infs (map (\ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]) (stranspose rs) \ - (\ k < length cs. infs (\ pp. (cs ! k) (pp ! k)) (stranspose rs))" + have "gen infs (map (\ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]) (ps ## stranspose rs) \ + (\ k < length cs. infs (\ pp. (cs ! k) (pp ! k)) (ps ## stranspose rs))" by (auto simp: gen_def) - also have "\ \ (\ k < length cs. infs (cs ! k) (smap (\ pp. pp ! k) (stranspose rs)))" + also have "\ \ (\ k < length cs. infs (cs ! k) (smap (\ pp. pp ! k) (ps ## stranspose rs)))" by (simp add: comp_def) also have "\ \ (\ k < length cs. infs (cs ! k) (rs ! k))" using 1 by simp - also have "\ \ list_all (\ (c, r, p). infs c r) (cs || rs || ps)" + also have "\ \ list_all (\ (c, r, p). infs c (p ## r)) (cs || rs || ps)" using 1 unfolding list_all_length by simp - finally show "gen infs (map (\ k ps. (cs ! k) (ps ! k)) [0 ..< length cs]) (stranspose rs) \ - list_all (\ (c, r, p). infs c r) (cs || rs || ps)" by this + finally show "gen infs (map (\ k ps. (cs ! k) (ps ! k)) [0 ..< length cs]) (ps ## stranspose rs) \ + list_all (\ (c, r, p). infs c (p ## r)) (cs || rs || ps)" by this qed lemmas intersect_list'_language[simp] = intersection_list.intersect_language[folded NGBA.language_def] lemmas intersect_list'_nodes_finite[intro] = intersection_list.intersect_nodes_finite[folded NGBA.nodes_def] global_interpretation union_list: automaton_union_list_run - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" - nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P r" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" + nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" "\ cs (k, p). (cs ! k) p" defines union_list = union_list.union by (unfold_locales) (auto simp: szip_sconst_smap_fst comp_def) lemmas union_list_language = union_list.union_language lemmas union_list_nodes_finite = union_list.union_nodes_finite abbreviation intersect where "intersect A B \ degeneralize (intersect' A B)" lemma intersect_language[simp]: "NBA.language (intersect A B) = NBA.language A \ NBA.language B" by simp lemma intersect_nodes_finite[intro]: assumes "finite (NBA.nodes A)" "finite (NBA.nodes B)" shows "finite (NBA.nodes (intersect A B))" using intersect'_nodes_finite assms by simp abbreviation intersect_list where "intersect_list AA \ degeneralize (intersect_list' AA)" lemma intersect_list_language[simp]: "NBA.language (intersect_list AA) = \ (NBA.language ` set AA)" by simp lemma intersect_list_nodes_finite[intro]: assumes "list_all (finite \ NBA.nodes) AA" shows "finite (NBA.nodes (intersect_list AA))" using intersect_list'_nodes_finite assms by simp end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Graphs.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Graphs.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Graphs.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Graphs.thy @@ -1,147 +1,147 @@ section \Connecting Nondeterministic Büchi Automata to CAVA Automata Structures\ theory NBA_Graphs imports NBA CAVA_Automata.Automata_Impl begin no_notation build (infixr "##" 65) subsection \Regular Graphs\ definition nba_g :: "('label, 'state) nba \ 'state graph_rec" where "nba_g A \ \ g_V = UNIV, g_E = E_of_succ (successors A), g_V0 = initial A \" lemma nba_g_graph[simp]: "graph (nba_g A)" unfolding nba_g_def graph_def by simp lemma nba_g_V0: "g_V0 (nba_g A) = initial A" unfolding nba_g_def by simp lemma nba_g_E_rtrancl: "(g_E (nba_g A))\<^sup>* = {(p, q). q \ reachable A p}" unfolding nba_g_def graph_rec.simps E_of_succ_def proof safe show "(p, q) \ {(p, q). q \ successors A p}\<^sup>*" if "q \ reachable A p" for p q using that by (induct) (auto intro: rtrancl_into_rtrancl) show "q \ reachable A p" if "(p, q) \ {(p, q). q \ successors A p}\<^sup>*" for p q using that by induct auto qed lemma nba_g_rtrancl_path: "(g_E (nba_g A))\<^sup>* = {(p, target r p) |r p. NBA.path A r p}" unfolding nba_g_E_rtrancl by blast lemma nba_g_trancl_path: "(g_E (nba_g A))\<^sup>+ = {(p, target r p) |r p. NBA.path A r p \ r \ []}" unfolding nba_g_def graph_rec.simps E_of_succ_def proof safe show "\ r p. (x, y) = (p, target r p) \ NBA.path A r p \ r \ []" if "(x, y) \ {(p, q). q \ successors A p}\<^sup>+" for x y using that proof induct case (base y) obtain a where 1: "a \ alphabet A" "y \ transition A a x" using base by auto show ?case proof (intro exI conjI) show "(x, y) = (x, target [(a, y)] x)" by simp show "NBA.path A [(a, y)] x" using 1 by auto show "[(a, y)] \ []" by simp qed next case (step y z) obtain r where 1: "y = target r x" "NBA.path A r x" "r \ []" using step(3) by auto obtain a where 2: "a \ alphabet A" "z \ transition A a y" using step(2) by auto show ?case proof (intro exI conjI) show "(x, z) = (x, target (r @ [(a, z)]) x)" by simp show "NBA.path A (r @ [(a, z)]) x" using 1 2 by auto show "r @ [(a, z)] \ []" by simp qed qed show "(p, target r p) \ {(u, v). v \ successors A u}\<^sup>+" if "NBA.path A r p" "r \ []" for r p using that by (induct) (fastforce intro: trancl_into_trancl2)+ qed lemma nba_g_ipath_run: assumes "ipath (g_E (nba_g A)) r" obtains w where "run A (w ||| smap (r \ Suc) nats) (r 0)" proof - have 1: "\ a \ alphabet A. r (Suc i) \ transition A a (r i)" for i using assms unfolding ipath_def nba_g_def E_of_succ_def by auto obtain wr where 2: "run A wr (r 0)" "\ i. target (stake i wr) (r 0) = r i" proof (rule nba.invariant_run_index) show "\ aq. (fst aq \ alphabet A \ snd aq \ transition A (fst aq) p) \ snd aq = r (Suc i) \ True" if "p = r i" for i p using that 1 by auto show "r 0 = r 0" by rule qed auto have 3: "smap (r \ Suc) nats = smap snd wr" proof (rule eqI_snth) fix i have "smap (r \ Suc) nats !! i = r (Suc i)" by simp also have "\ = target (stake (Suc i) wr) (r 0)" unfolding 2(2) by rule also have "\ = (r 0 ## trace wr (r 0)) !! Suc i" by simp also have "\ = smap snd wr !! i" unfolding nba.trace_alt_def by simp finally show "smap (r \ Suc) nats !! i = smap snd wr !! i" by this qed show ?thesis proof show "run A (smap fst wr ||| smap (r \ Suc) nats) (r 0)" using 2(1) unfolding 3 by auto qed qed lemma nba_g_run_ipath: assumes "run A (w ||| r) p" shows "ipath (g_E (nba_g A)) (snth (p ## r))" proof fix i have 1: "w !! i \ alphabet A" "r !! i \ transition A (w !! i) (target (stake i (w ||| r)) p)" using assms by (auto dest: nba.run_snth) have 2: "r !! i \ successors A ((p ## r) !! i)" using 1 unfolding sscan_scons_snth[symmetric] nba.trace_alt_def by auto show "((p ## r) !! i, (p ## r) !! Suc i) \ g_E (nba_g A)" using 2 unfolding nba_g_def graph_rec.simps E_of_succ_def by simp qed subsection \Indexed Generalized Büchi Graphs\ definition nba_igbg :: "('label, 'state) nba \ 'state igb_graph_rec" where "nba_igbg A \ graph_rec.extend (nba_g A) \ igbg_num_acc = 1, igbg_acc = \ p. if accepting A p then {0} else {} \" lemma acc_run_language: assumes "igb_graph (nba_igbg A)" shows "Ex (igb_graph.is_acc_run (nba_igbg A)) \ language A \ {}" proof interpret igb_graph "nba_igbg A" using assms by this have [simp]: "V0 = g_V0 (nba_g A)" "E = g_E (nba_g A)" "num_acc = 1" "0 \ acc p \ accepting A p" for p unfolding nba_igbg_def graph_rec.defs by simp+ show "language A \ {}" if run: "Ex is_acc_run" proof - obtain r where 1: "is_acc_run r" using run by rule have 2: "r 0 \ V0" "ipath E r" "is_acc r" using 1 unfolding is_acc_run_def graph_defs.is_run_def by auto obtain w where 3: "run A (w ||| smap (r \ Suc) nats) (r 0)" using nba_g_ipath_run 2(2) by auto have 4: "r 0 ## smap (r \ Suc) nats = smap r nats" by (simp) (metis stream.map_comp smap_siterate) have 5: "infs (accepting A) (r 0 ## smap (r \ Suc) nats)" using 2(3) unfolding infs_infm is_acc_def 4 by simp have "w \ language A" proof show "r 0 \ initial A" using nba_g_V0 2(1) by force show "run A (w ||| smap (r \ Suc) nats) (r 0)" using 3 by this - show "infs (accepting A) (smap (r \ Suc) nats)" using 5 by simp + show "infs (accepting A) (r 0 ## smap (r \ Suc) nats)" using 5 by simp qed then show ?thesis by auto qed show "Ex is_acc_run" if language: "language A \ {}" proof - obtain w where 1: "w \ language A" using language by auto - obtain r p where 2: "p \ initial A" "run A (w ||| r) p" "infs (accepting A) r" using 1 by rule + obtain r p where 2: "p \ initial A" "run A (w ||| r) p" "infs (accepting A) (p ## r)" using 1 by rule have 3: "infs (accepting A) (p ## r)" using 2(3) by simp have "is_acc_run (snth (p ## r))" unfolding is_acc_run_def graph_defs.is_run_def proof safe show "(p ## r) !! 0 \ V0" using nba_g_V0 2(1) by force show "ipath E (snth (p ## r))" using nba_g_run_ipath 2(2) by force show "is_acc (snth (p ## r))" using 3 unfolding infs_infm is_acc_def by simp qed then show ?thesis by auto qed qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Refine.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Refine.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Refine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Refine.thy @@ -1,82 +1,82 @@ section \Relations on Nondeterministic Büchi Automata\ theory NBA_Refine imports "NBA" "../../Transition_Systems/Transition_System_Refine" begin definition nba_rel :: "('label\<^sub>1 \ 'label\<^sub>2) set \ ('state\<^sub>1 \ 'state\<^sub>2) set \ (('label\<^sub>1, 'state\<^sub>1) nba \ ('label\<^sub>2, 'state\<^sub>2) nba) set" where [to_relAPP]: "nba_rel L S \ {(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \ \L\ set_rel \ (initial A\<^sub>1, initial A\<^sub>2) \ \S\ set_rel \ (transition A\<^sub>1, transition A\<^sub>2) \ L \ S \ \S\ set_rel \ (accepting A\<^sub>1, accepting A\<^sub>2) \ S \ bool_rel}" lemma nba_param[param]: "(nba, nba) \ \L\ set_rel \ \S\ set_rel \ (L \ S \ \S\ set_rel) \ (S \ bool_rel) \ \L, S\ nba_rel" "(alphabet, alphabet) \ \L, S\ nba_rel \ \L\ set_rel" "(initial, initial) \ \L, S\ nba_rel \ \S\ set_rel" "(transition, transition) \ \L, S\ nba_rel \ L \ S \ \S\ set_rel" "(accepting, accepting) \ \L, S\ nba_rel \ S \ bool_rel" unfolding nba_rel_def fun_rel_def by auto lemma nba_rel_id[simp]: "\Id, Id\ nba_rel = Id" unfolding nba_rel_def using nba.expand by auto lemma nba_rel_comp[trans]: assumes [param]: "(A, B) \ \L\<^sub>1, S\<^sub>1\ nba_rel" "(B, C) \ \L\<^sub>2, S\<^sub>2\ nba_rel" shows "(A, C) \ \L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\ nba_rel" proof - have "(accepting A, accepting B) \ S\<^sub>1 \ bool_rel" by parametricity also have "(accepting B, accepting C) \ S\<^sub>2 \ bool_rel" by parametricity finally have 1: "(accepting A, accepting C) \ S\<^sub>1 O S\<^sub>2 \ bool_rel" by simp have "(transition A, transition B) \ L\<^sub>1 \ S\<^sub>1 \ \S\<^sub>1\ set_rel" by parametricity also have "(transition B, transition C) \ L\<^sub>2 \ S\<^sub>2 \ \S\<^sub>2\ set_rel" by parametricity finally have 2: "(transition A, transition C) \ L\<^sub>1 O L\<^sub>2 \ S\<^sub>1 O S\<^sub>2 \ \S\<^sub>1\ set_rel O \S\<^sub>2\ set_rel" by simp show ?thesis unfolding nba_rel_def mem_Collect_eq prod.case set_rel_compp using 1 2 using nba_param(2 - 5)[THEN fun_relD, OF assms(1)] using nba_param(2 - 5)[THEN fun_relD, OF assms(2)] by auto qed lemma nba_rel_converse[simp]: "(\L, S\ nba_rel)\ = \L\, S\\ nba_rel" proof - have 1: "\L\ set_rel = (\L\\ set_rel)\" by simp have 2: "\S\ set_rel = (\S\\ set_rel)\" by simp have 3: "L \ S \ \S\ set_rel = (L\ \ S\ \ \S\\ set_rel)\" by simp have 4: "S \ bool_rel = (S\ \ bool_rel)\" by simp show ?thesis unfolding nba_rel_def unfolding 3 unfolding 1 2 4 by fastforce qed lemma nba_rel_eq: "(A, A) \ \Id_on (alphabet A), Id_on (nodes A)\ nba_rel" unfolding nba_rel_def by auto lemma enableds_param[param]: "(nba.enableds, nba.enableds) \ \L, S\ nba_rel \ S \ \L \\<^sub>r S\ set_rel" using nba_param(2, 4) unfolding nba.enableds_def fun_rel_def set_rel_def by fastforce lemma paths_param[param]: "(nba.paths, nba.paths) \ \L, S\ nba_rel \ S \ \\L \\<^sub>r S\ list_rel\ set_rel" using enableds_param[param_fo] by parametricity lemma runs_param[param]: "(nba.runs, nba.runs) \ \L, S\ nba_rel \ S \ \\L \\<^sub>r S\ stream_rel\ set_rel" using enableds_param[param_fo] by parametricity lemma reachable_param[param]: "(reachable, reachable) \ \L, S\ nba_rel \ S \ \S\ set_rel" proof - have 1: "reachable A p = (\ wr. target wr p) ` nba.paths A p" for A :: "('label, 'state) nba" and p unfolding nba.reachable_alt_def nba.paths_def by auto show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity qed lemma nodes_param[param]: "(nodes, nodes) \ \L, S\ nba_rel \ \S\ set_rel" unfolding nba.nodes_alt_def Collect_mem_eq by parametricity lemma language_param[param]: "(language, language) \ \L, S\ nba_rel \ \\L\ stream_rel\ set_rel" proof - have 1: "language A = (\ p \ initial A. \ wr \ nba.runs A p. - if infs (accepting A) (smap snd wr) then {smap fst wr} else {})" + if infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {})" for A :: "('label, 'state) nba" unfolding nba.language_def nba.runs_def image_def by (auto iff: split_szip_ex simp del: alw_smap) show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA.thy @@ -1,25 +1,25 @@ section \Nondeterministic Generalized Büchi Automata\ theory NGBA imports "../Nondeterministic" begin datatype ('label, 'state) ngba = ngba (alphabet: "'label set") (initial: "'state set") (transition: "'label \ 'state \ 'state set") (accepting: "'state pred gen") global_interpretation ngba: automaton ngba alphabet initial transition accepting defines path = ngba.path and run = ngba.run and reachable = ngba.reachable and nodes = ngba.nodes by unfold_locales auto - global_interpretation ngba: automaton_run ngba alphabet initial transition accepting "\ P w r p. gen infs P r" + global_interpretation ngba: automaton_run ngba alphabet initial transition accepting "\ P w r p. gen infs P (p ## r)" defines language = ngba.language by standard abbreviation target where "target \ ngba.target" abbreviation states where "states \ ngba.states" abbreviation trace where "trace \ ngba.trace" abbreviation successors where "successors \ ngba.successors TYPE('label)" end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Refine.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Refine.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Refine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Refine.thy @@ -1,58 +1,58 @@ section \Relations on Nondeterministic Generalized Büchi Automata\ theory NGBA_Refine imports "NGBA" "../../Transition_Systems/Transition_System_Refine" begin definition ngba_rel :: "('label\<^sub>1 \ 'label\<^sub>2) set \ ('state\<^sub>1 \ 'state\<^sub>2) set \ (('label\<^sub>1, 'state\<^sub>1) ngba \ ('label\<^sub>2, 'state\<^sub>2) ngba) set" where [to_relAPP]: "ngba_rel L S \ {(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \ \L\ set_rel \ (initial A\<^sub>1, initial A\<^sub>2) \ \S\ set_rel \ (transition A\<^sub>1, transition A\<^sub>2) \ L \ S \ \S\ set_rel \ (accepting A\<^sub>1, accepting A\<^sub>2) \ \S \ bool_rel\ list_rel}" lemma ngba_param[param]: "(ngba, ngba) \ \L\ set_rel \ \S\ set_rel \ (L \ S \ \S\ set_rel) \ \S \ bool_rel\ list_rel \ \L, S\ ngba_rel" "(alphabet, alphabet) \ \L, S\ ngba_rel \ \L\ set_rel" "(initial, initial) \ \L, S\ ngba_rel \ \S\ set_rel" "(transition, transition) \ \L, S\ ngba_rel \ L \ S \ \S\ set_rel" "(accepting, accepting) \ \L, S\ ngba_rel \ \S \ bool_rel\ list_rel" unfolding ngba_rel_def fun_rel_def by auto lemma ngba_rel_id[simp]: "\Id, Id\ ngba_rel = Id" unfolding ngba_rel_def using ngba.expand by auto lemma enableds_param[param]: "(ngba.enableds, ngba.enableds) \ \L, S\ ngba_rel \ S \ \L \\<^sub>r S\ set_rel" using ngba_param(2, 4) unfolding ngba.enableds_def fun_rel_def set_rel_def by fastforce lemma paths_param[param]: "(ngba.paths, ngba.paths) \ \L, S\ ngba_rel \ S \ \\L \\<^sub>r S\ list_rel\ set_rel" using enableds_param[param_fo] by parametricity lemma runs_param[param]: "(ngba.runs, ngba.runs) \ \L, S\ ngba_rel \ S \ \\L \\<^sub>r S\ stream_rel\ set_rel" using enableds_param[param_fo] by parametricity lemma reachable_param[param]: "(reachable, reachable) \ \L, S\ ngba_rel \ S \ \S\ set_rel" proof - have 1: "reachable A p = (\ wr. target wr p) ` ngba.paths A p" for A :: "('label, 'state) ngba" and p unfolding ngba.reachable_alt_def ngba.paths_def by auto show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity qed lemma nodes_param[param]: "(nodes, nodes) \ \L, S\ ngba_rel \ \S\ set_rel" unfolding ngba.nodes_alt_def Collect_mem_eq by parametricity (* TODO: move *) lemma gen_param[param]: "(gen, gen) \ (A \ B \ bool_rel) \ \A\ list_rel \ B \ bool_rel" unfolding gen_def by parametricity lemma language_param[param]: "(language, language) \ \L, S\ ngba_rel \ \\L\ stream_rel\ set_rel" proof - have 1: "language A = (\ p \ initial A. \ wr \ ngba.runs A p. - if gen infs (accepting A) (smap snd wr) then {smap fst wr} else {})" + if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {})" for A :: "('label, 'state) ngba" unfolding ngba.language_def ngba.runs_def image_def by (auto iff: split_szip_ex simp del: alw_smap) show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity qed end \ No newline at end of file