diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy @@ -1,45 +1,192 @@ section \Algorithms on Nondeterministic Generalized Büchi Automata\ theory NGBA_Algorithms imports + NGBA_Graphs NGBA_Implement NBA_Combine NBA_Algorithms Degeneralization_Refine begin + subsection \Operations\ + + definition op_language_empty where [simp]: "op_language_empty A \ NGBA.language A = {}" + + lemmas [autoref_op_pat] = op_language_empty_def[symmetric] + subsection \Implementations\ context begin interpretation autoref_syn by this + lemma ngba_g_ahs: "ngba_g A = \ g_V = UNIV, g_E = E_of_succ (\ p. CAST + ((\ a \ ngba.alphabet A. ngba.transition A a p ::: \S\ list_set_rel) ::: \S\ ahs_rel bhc)), + g_V0 = ngba.initial A \" + unfolding ngba_g_def ngba.successors_alt_def CAST_def id_apply autoref_tag_defs by rule + + schematic_goal ngbai_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\ ngbai_ngba_rel" + shows "(?f :: ?'a, RETURN (ngba_g A)) \ ?A" + unfolding ngba_g_ahs[where S = S and bhc = bhc] by (autoref_monadic (plain)) + concrete_definition ngbai_gi uses ngbai_gi + lemma ngbai_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 "(NGBA_Algorithms.ngbai_gi seq bhc hms, ngba_g) \ + \L, S\ ngbai_ngba_rel \ \unit_rel, S\ g_impl_rel_ext" + using ngbai_gi.refine[THEN RETURN_nres_relD] assms unfolding autoref_tag_defs by blast + + schematic_goal ngba_nodes: + fixes S :: "('statei \ 'state) set" + assumes [simp]: "finite ((g_E (ngba_g A))\<^sup>* `` g_V0 (ngba_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\ ngbai_ngba_rel" + shows "(?f :: ?'a, op_reachable (ngba_g A)) \ ?R" by autoref + concrete_definition ngba_nodes uses ngba_nodes + lemma ngba_nodes_refine[autoref_rules]: + fixes S :: "('statei \ 'state) set" + assumes "SIDE_PRECOND (finite (NGBA.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\ ngbai_ngba_rel" + shows "(NGBA_Algorithms.ngba_nodes seq bhc hms Ai, + (OP NGBA.nodes ::: \L, S\ ngbai_ngba_rel \ \S\ ahs_rel bhc) $ A) \ \S\ ahs_rel bhc" + proof - + have 1: "NGBA.nodes A = op_reachable (ngba_g A)" by (auto simp: ngba_g_V0 ngba_g_E_rtrancl) + have 2: "finite ((g_E (ngba_g A))\<^sup>* `` g_V0 (ngba_g A))" using assms(1) unfolding 1 by simp + show ?thesis using ngba_nodes.refine assms 2 unfolding autoref_tag_defs 1 by blast + qed + + lemma ngba_igbg_ahs: "ngba_igbg A = \ g_V = UNIV, g_E = E_of_succ (\ p. CAST + ((\ a \ NGBA.alphabet A. NGBA.transition A a p ::: \S\ list_set_rel) ::: \S\ ahs_rel bhc)), g_V0 = NGBA.initial A, + igbg_num_acc = length (NGBA.accepting A), igbg_acc = ngba_acc (NGBA.accepting A) \" + unfolding ngba_g_def ngba_igbg_def ngba.successors_alt_def CAST_def id_apply autoref_tag_defs + unfolding graph_rec.defs + by simp + + definition "ngba_acc_bs cs p \ fold (\ (k, c) bs. if c p then bs_insert k bs else bs) (List.enumerate 0 cs) (bs_empty ())" + + lemma ngba_acc_bs_empty[simp]: "ngba_acc_bs [] p = bs_empty ()" unfolding ngba_acc_bs_def by simp + lemma ngba_acc_bs_insert[simp]: + assumes "c p" + shows "ngba_acc_bs (cs @ [c]) p = bs_insert (length cs) (ngba_acc_bs cs p)" + using assms unfolding ngba_acc_bs_def by (simp add: enumerate_append_eq) + lemma ngba_acc_bs_skip[simp]: + assumes "\ c p" + shows "ngba_acc_bs (cs @ [c]) p = ngba_acc_bs cs p" + using assms unfolding ngba_acc_bs_def by (simp add: enumerate_append_eq) + + lemma ngba_acc_bs_correct[simp]: "bs_\ (ngba_acc_bs cs p) = ngba_acc cs p" + proof (induct cs rule: rev_induct) + case Nil + show ?case unfolding ngba_acc_def by simp + next + case (snoc c cs) + show ?case using less_Suc_eq snoc by (cases "c p") (force simp: ngba_acc_def)+ + qed + + lemma ngba_acc_impl_bs[autoref_rules]: "(ngba_acc_bs, ngba_acc) \ \S \ bool_rel\ list_rel \ S \ \nat_rel\ bs_set_rel" + proof - + have "(ngba_acc_bs, ngba_acc) \ \Id \ bool_rel\ list_rel \ Id \ \nat_rel\ bs_set_rel" + by (auto simp: bs_set_rel_def in_br_conv) + also have "(ngba_acc, ngba_acc) \ \S \ bool_rel\ list_rel \ S \ \nat_rel\ set_rel" by parametricity + finally show ?thesis by simp + qed + + schematic_goal ngbai_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\ ngbai_ngba_rel" + shows "(?f :: ?'a, RETURN (ngba_igbg A)) \ ?A" + unfolding ngba_igbg_ahs[where S = S and bhc = bhc] by (autoref_monadic (plain)) + concrete_definition ngbai_igbgi uses ngbai_igbgi + lemma ngbai_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 "(NGBA_Algorithms.ngbai_igbgi seq bhc hms, ngba_igbg) \ + \L, S\ ngbai_ngba_rel \ igbg_impl_rel_ext unit_rel S" + using ngbai_igbgi.refine[THEN RETURN_nres_relD] assms unfolding autoref_tag_defs by blast + + schematic_goal ngba_language_empty: + fixes S :: "('statei \ 'state) set" + assumes [simp]: "igb_fr_graph (ngba_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\ ngbai_ngba_rel" + shows "(?f :: ?'a, do { r \ op_find_lasso_spec (ngba_igbg A); RETURN (r = None)}) \ ?A" + by (autoref_monadic (plain)) + concrete_definition ngba_language_empty uses ngba_language_empty + lemma nba_language_empty_refine[autoref_rules]: + fixes S :: "('statei \ 'state) set" + assumes "SIDE_PRECOND (finite (NGBA.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\ ngbai_ngba_rel" + shows "(NGBA_Algorithms.ngba_language_empty seq bhc hms Ai, + (OP op_language_empty ::: \L, S\ ngbai_ngba_rel \ bool_rel) $ A) \ bool_rel" + proof - + have 1: "NGBA.nodes A = op_reachable (ngba_g A)" by (auto simp: ngba_g_V0 ngba_g_E_rtrancl) + have 2: "finite ((g_E (ngba_g A))\<^sup>* `` g_V0 (ngba_g A))" using assms(1) unfolding 1 by simp + interpret igb_fr_graph "ngba_igbg A" + using 2 unfolding ngba_igbg_def ngba_g_def graph_rec.defs ngba_acc_def by unfold_locales auto + have "(RETURN (NGBA_Algorithms.ngba_language_empty seq bhc hms Ai), + do { r \ find_lasso_spec; RETURN (r = None) }) \ \bool_rel\ nres_rel" + using ngba_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 "NGBA_Algorithms.ngba_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 "\ \ NGBA.language A = {}" using NGBA_Graphs.acc_run_language is_igb_graph by auto + finally show ?thesis by simp + qed + lemma degeneralize_alt_def: "degeneralize A = nba (ngba.alphabet A) ((\ p. (p, 0)) ` ngba.initial A) (\ a (p, k). (\ q. (q, Degeneralization.count (ngba.accepting A) p k)) ` ngba.transition A a p) (degen (ngba.accepting A))" unfolding degeneralization.degeneralize_def by auto schematic_goal ngba_degeneralize: "(?f :: ?'a, degeneralize) \ ?R" unfolding degeneralize_alt_def using degen_param[autoref_rules] count_param[autoref_rules] by autoref concrete_definition ngba_degeneralize uses ngba_degeneralize lemmas ngba_degeneralize_refine[autoref_rules] = ngba_degeneralize.refine schematic_goal nba_intersect': assumes [autoref_rules]: "(seq, HOL.eq) \ L \ L \ bool_rel" shows "(?f, intersect') \ \L, S\ nbai_nba_rel \ \L, T\ nbai_nba_rel \ \L, S \\<^sub>r T\ ngbai_ngba_rel" unfolding intersection.product_def by autoref concrete_definition nba_intersect' uses nba_intersect' lemma nba_intersect'_refine[autoref_rules]: assumes "GEN_OP seq HOL.eq (L \ L \ bool_rel)" shows "(nba_intersect' seq, intersect') \ \L, S\ nbai_nba_rel \ \L, T\ nbai_nba_rel \ \L, S \\<^sub>r T\ ngbai_ngba_rel" using nba_intersect'.refine assms unfolding autoref_tag_defs by this end end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Graphs.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Graphs.thy new file mode 100644 --- /dev/null +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Graphs.thy @@ -0,0 +1,152 @@ +section \Connecting Nondeterministic Generalized Büchi Automata to CAVA Automata Structures\ + +theory NGBA_Graphs +imports + NGBA + CAVA_Automata.Automata_Impl +begin + + no_notation build (infixr "##" 65) + + subsection \Regular Graphs\ + + definition ngba_g :: "('label, 'state) ngba \ 'state graph_rec" where + "ngba_g A \ \ g_V = UNIV, g_E = E_of_succ (successors A), g_V0 = initial A \" + + lemma ngba_g_graph[simp]: "graph (ngba_g A)" unfolding ngba_g_def graph_def by simp + + lemma ngba_g_V0: "g_V0 (ngba_g A) = initial A" unfolding ngba_g_def by simp + lemma ngba_g_E_rtrancl: "(g_E (ngba_g A))\<^sup>* = {(p, q). q \ reachable A p}" + unfolding ngba_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 ngba_g_rtrancl_path: "(g_E (ngba_g A))\<^sup>* = {(p, target r p) |r p. NGBA.path A r p}" + unfolding ngba_g_E_rtrancl by blast + lemma ngba_g_trancl_path: "(g_E (ngba_g A))\<^sup>+ = {(p, target r p) |r p. NGBA.path A r p \ r \ []}" + unfolding ngba_g_def graph_rec.simps E_of_succ_def + proof safe + show "\ r p. (x, y) = (p, target r p) \ NGBA.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 "NGBA.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" "NGBA.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 "NGBA.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 "NGBA.path A r p" "r \ []" for r p + using that by (induct) (fastforce intro: trancl_into_trancl2)+ + qed + + lemma ngba_g_ipath_run: + assumes "ipath (g_E (ngba_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 ngba_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 ngba.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 ngba.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 ngba_g_run_ipath: + assumes "run A (w ||| r) p" + shows "ipath (g_E (ngba_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: ngba.run_snth) + have 2: "r !! i \ successors A ((p ## r) !! i)" + using 1 unfolding sscan_scons_snth[symmetric] ngba.trace_alt_def by auto + show "((p ## r) !! i, (p ## r) !! Suc i) \ g_E (ngba_g A)" + using 2 unfolding ngba_g_def graph_rec.simps E_of_succ_def by simp + qed + + subsection \Indexed Generalized Büchi Graphs\ + + definition ngba_acc :: "'state pred gen \ 'state \ nat set" where + "ngba_acc cs p \ {k \ {0 ..< length cs}. (cs ! k) p}" + + lemma ngba_acc_param[param]: "(ngba_acc, ngba_acc) \ \S \ bool_rel\ list_rel \ S \ \nat_rel\ set_rel" + unfolding ngba_acc_def list_rel_def list_all2_conv_all_nth fun_rel_def by auto + + definition ngba_igbg :: "('label, 'state) ngba \ 'state igb_graph_rec" where + "ngba_igbg A \ graph_rec.extend (ngba_g A) \ igbg_num_acc = length (accepting A), igbg_acc = ngba_acc (accepting A) \" + + lemma acc_run_language: + assumes "igb_graph (ngba_igbg A)" + shows "Ex (igb_graph.is_acc_run (ngba_igbg A)) \ language A \ {}" + proof + interpret igb_graph "ngba_igbg A" using assms by this + have [simp]: "V0 = g_V0 (ngba_g A)" "E = g_E (ngba_g A)" "num_acc = length (accepting A)" + "k \ acc p \ k < length (accepting A) \ (accepting A ! k) p" for p k + unfolding ngba_igbg_def ngba_acc_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 ngba_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 ! k) (r 0 ## smap (r \ Suc) nats)" if "k < length (accepting A)" for k + using 2(3) that unfolding infs_infm is_acc_def 4 by simp + have "w \ language A" + proof + show "r 0 \ initial A" using ngba_g_V0 2(1) by force + show "run A (w ||| smap (r \ Suc) nats) (r 0)" using 3 by this + show "gen infs (accepting A) (r 0 ## smap (r \ Suc) nats)" + unfolding gen_def all_set_conv_all_nth 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" "gen infs (accepting A) (p ## r)" using 1 by rule + 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 ngba_g_V0 2(1) by force + show "ipath E (snth (p ## r))" using ngba_g_run_ipath 2(2) by force + show "is_acc (snth (p ## r))" using 2(3) unfolding gen_def infs_infm is_acc_def by simp + qed + then show ?thesis by auto + qed + qed + +end \ No newline at end of file