diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Algorithms.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Algorithms.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Algorithms.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Algorithms.thy @@ -1,146 +1,146 @@ section \Algorithms on Nondeterministic Büchi Automata\ theory NBA_Algorithms imports NBA_Graphs NBA_Implement DFS_Framework.Reachable_Nodes Gabow_SCC.Gabow_GBG_Code begin subsection \Miscellaneous Amendments\ lemma (in igb_fr_graph) acc_run_lasso_prpl: "Ex is_acc_run \ Ex is_lasso_prpl" using accepted_lasso is_lasso_prpl_of_lasso by blast lemma (in igb_fr_graph) lasso_prpl_acc_run_iff: "Ex is_lasso_prpl \ Ex is_acc_run" using acc_run_lasso_prpl lasso_prpl_acc_run by auto lemma [autoref_rel_intf]: "REL_INTF igbg_impl_rel_ext i_igbg" by (rule REL_INTFI) subsection \Operations\ - definition [simp]: "op_language_empty A \ language A = {}" + definition op_language_empty where [simp]: "op_language_empty A \ language A = {}" lemmas [autoref_op_pat] = op_language_empty_def[symmetric] subsection \Implementations\ context begin interpretation autoref_syn by this lemma nba_g_ahs: "nba_g A = \ g_V = UNIV, g_E = E_of_succ (\ p. CAST ((\ a \ alphabet A. transition A a p ::: \S\ list_set_rel) ::: \S\ ahs_rel bhc)), g_V0 = initial A \" unfolding nba_g_def nba.successors_alt_def CAST_def id_apply autoref_tag_defs by rule schematic_goal nbai_gi: notes [autoref_ga_rules] = map2set_to_list fixes S :: "('statei \ 'state) set" assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc" assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms" assumes [autoref_rules]: "(seq, HOL.eq) \ S \ S \ bool_rel" assumes [autoref_rules]: "(Ai, A) \ \L, S\ nbai_nba_rel" shows "(?f :: ?'a, RETURN (nba_g A)) \ ?A" unfolding nba_g_ahs[where S = S and bhc = bhc] by (autoref_monadic (plain)) concrete_definition nbai_gi uses nbai_gi lemma nbai_gi_refine[autoref_rules]: fixes S :: "('statei \ 'state) set" assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)" assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)" assumes "GEN_OP seq HOL.eq (S \ S \ bool_rel)" shows "(NBA_Algorithms.nbai_gi seq bhc hms, nba_g) \ \L, S\ nbai_nba_rel \ \unit_rel, S\ g_impl_rel_ext" using nbai_gi.refine[THEN RETURN_nres_relD] assms unfolding autoref_tag_defs by blast schematic_goal nba_nodes: fixes S :: "('statei \ 'state) set" assumes [simp]: "finite ((g_E (nba_g A))\<^sup>* `` g_V0 (nba_g A))" assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc" assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms" assumes [autoref_rules]: "(seq, HOL.eq) \ S \ S \ bool_rel" assumes [autoref_rules]: "(Ai, A) \ \L, S\ nbai_nba_rel" shows "(?f :: ?'a, op_reachable (nba_g A)) \ ?R" by autoref concrete_definition nba_nodes uses nba_nodes lemma nba_nodes_refine[autoref_rules]: fixes S :: "('statei \ 'state) set" assumes "SIDE_PRECOND (finite (nodes A))" assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)" assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)" assumes "GEN_OP seq HOL.eq (S \ S \ bool_rel)" assumes "(Ai, A) \ \L, S\ nbai_nba_rel" shows "(NBA_Algorithms.nba_nodes seq bhc hms Ai, (OP nodes ::: \L, S\ nbai_nba_rel \ \S\ ahs_rel bhc) $ A) \ \S\ ahs_rel bhc" proof - have 1: "nodes A = op_reachable (nba_g A)" by (auto simp: nba_g_V0 nba_g_E_rtrancl) have 2: "finite ((g_E (nba_g A))\<^sup>* `` g_V0 (nba_g A))" using assms(1) unfolding 1 by simp show ?thesis using nba_nodes.refine assms 2 unfolding autoref_tag_defs 1 by blast qed lemma nba_igbg_ahs: "nba_igbg A = \ g_V = UNIV, g_E = E_of_succ (\ p. CAST ((\ a \ alphabet A. transition A a p ::: \S\ list_set_rel) ::: \S\ ahs_rel bhc)), g_V0 = initial A, igbg_num_acc = 1, igbg_acc = \ p. if accepting A p then {0} else {} \" unfolding nba_g_def nba_igbg_def nba.successors_alt_def CAST_def id_apply autoref_tag_defs unfolding graph_rec.defs by simp schematic_goal nbai_igbgi: notes [autoref_ga_rules] = map2set_to_list fixes S :: "('statei \ 'state) set" assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc" assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms" assumes [autoref_rules]: "(seq, HOL.eq) \ S \ S \ bool_rel" assumes [autoref_rules]: "(Ai, A) \ \L, S\ nbai_nba_rel" shows "(?f :: ?'a, RETURN (nba_igbg A)) \ ?A" unfolding nba_igbg_ahs[where S = S and bhc = bhc] by (autoref_monadic (plain)) concrete_definition nbai_igbgi uses nbai_igbgi lemma nbai_igbgi_refine[autoref_rules]: fixes S :: "('statei \ 'state) set" assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)" assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)" assumes "GEN_OP seq HOL.eq (S \ S \ bool_rel)" shows "(NBA_Algorithms.nbai_igbgi seq bhc hms, nba_igbg) \ \L, S\ nbai_nba_rel \ igbg_impl_rel_ext unit_rel S" using nbai_igbgi.refine[THEN RETURN_nres_relD] assms unfolding autoref_tag_defs by blast schematic_goal nba_language_empty: fixes S :: "('statei \ 'state) set" assumes [simp]: "igb_fr_graph (nba_igbg A)" assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhs" assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms" assumes [autoref_rules]: "(seq, HOL.eq) \ S \ S \ bool_rel" assumes [autoref_rules]: "(Ai, A) \ \L, S\ nbai_nba_rel" shows "(?f :: ?'a, do { r \ op_find_lasso_spec (nba_igbg A); RETURN (r = None)}) \ ?A" by (autoref_monadic (plain)) concrete_definition nba_language_empty uses nba_language_empty lemma nba_language_empty_refine[autoref_rules]: fixes S :: "('statei \ 'state) set" assumes "SIDE_PRECOND (finite (nodes A))" assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)" assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)" assumes "GEN_OP seq HOL.eq (S \ S \ bool_rel)" assumes "(Ai, A) \ \L, S\ nbai_nba_rel" shows "(NBA_Algorithms.nba_language_empty seq bhc hms Ai, (OP op_language_empty ::: \L, S\ nbai_nba_rel \ bool_rel) $ A) \ bool_rel" proof - have 1: "nodes A = op_reachable (nba_g A)" by (auto simp: nba_g_V0 nba_g_E_rtrancl) have 2: "finite ((g_E (nba_g A))\<^sup>* `` g_V0 (nba_g A))" using assms(1) unfolding 1 by simp interpret igb_fr_graph "nba_igbg A" using 2 unfolding nba_igbg_def nba_g_def graph_rec.defs by unfold_locales auto have "(RETURN (NBA_Algorithms.nba_language_empty seq bhc hms Ai), do { r \ find_lasso_spec; RETURN (r = None) }) \ \bool_rel\ nres_rel" using nba_language_empty.refine assms igb_fr_graph_axioms by simp also have "(do { r \ find_lasso_spec; RETURN (r = None) }, RETURN (\ Ex is_lasso_prpl)) \ \bool_rel\ nres_rel" unfolding find_lasso_spec_def by (refine_vcg) (auto split: option.splits) finally have "NBA_Algorithms.nba_language_empty seq bhc hms Ai \ \ Ex is_lasso_prpl" unfolding nres_rel_comp using RETURN_nres_relD by force also have "\ \ \ Ex is_acc_run" using lasso_prpl_acc_run_iff by auto also have "\ \ language A = {}" using acc_run_language is_igb_graph by auto finally show ?thesis by simp qed end 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,146 @@ 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) (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) (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 + show "is_acc (snth (p ## r))" using 2(3) unfolding infs_infm is_acc_def by simp qed then show ?thesis by auto qed qed end \ No newline at end of file