diff --git a/thys/Buchi_Complementation/Complementation_Final.thy b/thys/Buchi_Complementation/Complementation_Final.thy --- a/thys/Buchi_Complementation/Complementation_Final.thy +++ b/thys/Buchi_Complementation/Complementation_Final.thy @@ -1,103 +1,105 @@ section \Complementation to Explicit Büchi Automaton\ theory Complementation_Final imports "Complementation_Implement" "Transition_Systems_and_Automata.NBA_Translate" "HOL-Library.Permutation" begin definition "hci k \ uint32_of_nat k * 1103515245 + 12345" definition "hc \ \ (p, q, b). hci p + hci q * 31 + (if b then 1 else 0)" definition "list_hash xs \ fold (bitXOR \ hc) xs 0" lemma list_hash_eq: assumes "distinct xs" "distinct ys" "set xs = set ys" shows "list_hash xs = list_hash ys" proof - have "remdups xs <~~> remdups ys" using eq_set_perm_remdups assms(3) by this then have "xs <~~> ys" using assms(1, 2) by (simp add: distinct_remdups_id) then have "fold (bitXOR \ hc) xs a = fold (bitXOR \ hc) ys a" for a proof (induct arbitrary: a) case (swap y x l) have "x XOR y XOR a = y XOR x XOR a" for x y by (transfer) (simp add: word_bw_lcs(3)) then show ?case by simp qed simp+ then show ?thesis unfolding list_hash_def by this qed definition state_hash :: "nat \ Complementation_Implement.state \ nat" where "state_hash n p \ nat_of_hashcode (list_hash p) mod n" + (* there should be a simpler way to prove this (and others) from some "state_hash is a + valid hash function lemma *) lemma state_hash_bounded_hashcode[autoref_ga_rules]: "is_bounded_hashcode state_rel (gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (\))) state_hash" proof show [param]: "(gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (\)), (=)) \ state_rel \ state_rel \ bool_rel" by autoref show "state_hash n xs = state_hash n ys" if "xs \ Domain state_rel" "ys \ Domain state_rel" "gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (=)) xs ys" for xs ys n proof - have 1: "distinct (map fst xs)" "distinct (map fst ys)" using that(1, 2) unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv) have 2: "distinct xs" "distinct ys" using 1 by (auto intro: distinct_mapI) have 3: "(xs, map_of xs) \ state_rel" "(ys, map_of ys) \ state_rel" using 1 unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv) have 4: "(gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (\)) xs ys, map_of xs = map_of ys) \ bool_rel" using 3 by parametricity have 5: "map_to_set (map_of xs) = map_to_set (map_of ys)" using that(3) 4 by simp have 6: "set xs = set ys" using map_to_set_map_of 1 5 by blast show "state_hash n xs = state_hash n ys" unfolding state_hash_def using list_hash_eq 2 6 by metis qed show "state_hash n x < n" if "1 < n" for n x using that unfolding state_hash_def by simp qed schematic_goal complement_impl: assumes [simp]: "finite (nodes A)" assumes [autoref_rules]: "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" shows "(?f :: ?'c, op_translate (complement_4 A)) \ ?R" by (autoref_monadic (plain)) - concrete_definition complement_impl uses complement_impl[unfolded autoref_tag_defs] + concrete_definition complement_impl uses complement_impl theorem complement_impl_correct: assumes "finite (nodes A)" assumes "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" shows "language (nbae_nba (nbaei_nbae (complement_impl Ai))) = streams (alphabet A) - language A" proof - (* TODO: can we leave all this inside the nres without explicit obtain? *) (* TODO: or at least avoid unfolding op_translate and reasoning about injectivity? *) obtain f where 1: "(complement_impl Ai, nba_nbae (nba_image f (complement_4 A))) \ \Id, nat_rel\ nbaei_nbae_rel" "inj_on f (nodes (complement_4 A))" using complement_impl.refine[OF assms, unfolded in_nres_rel_iff op_translate_def, THEN RETURN_ref_SPECD] by metis let ?C = "nba_image f (complement_4 A)" have "(nbae_nba (nbaei_nbae (complement_impl Ai)), nbae_nba (id (nba_nbae ?C))) \ \Id, nat_rel\ nba_rel" using 1(1) by parametricity auto also have "nbae_nba (id (nba_nbae ?C)) = (nbae_nba \ nba_nbae) ?C" by simp also have "(\, id ?C) \ \Id_on (alphabet ?C), Id_on (nodes ?C)\ nba_rel" by parametricity finally have 2: "(nbae_nba (nbaei_nbae (complement_impl Ai)), ?C) \ \Id_on (alphabet ?C), Id_on (nodes ?C)\ nba_rel" by simp have "(language (nbae_nba (nbaei_nbae (complement_impl Ai))), language ?C) \ \\Id_on (alphabet ?C)\ stream_rel\ set_rel" using 2 by parametricity also have "language ?C = language (complement_4 A)" using 1(2) by simp also have "language (complement_4 A) = streams (alphabet A) - language A" using complement_4_correct assms(1) by this finally show ?thesis by simp qed definition nbaei_nbai :: "(String.literal, nat) nbaei \ (String.literal, nat) nbai" where "nbaei_nbai \ nbae_nba_impl (=) (=)" (* TODO: possible optimizations: - introduce op_map_map operation for maps instead of manually iterating via FOREACH - consolidate various binds and maps in expand_map_get_7 *) export_code nat_of_integer integer_of_nat nbaei alphabetei initialei transitionei acceptingei nbaei_nbai complement_impl in SML module_name Complementation file_prefix Complementation_Export end \ No newline at end of file