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,89 +1,103 @@ 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" 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, RETURN (to_nbaei (complement_4 A))) \ ?R" + shows "(?f :: ?'c, op_translate (complement_4 A)) \ ?R" by (autoref_monadic (plain)) concrete_definition complement_impl uses complement_impl[unfolded autoref_tag_defs] 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 - - have "(language ((nbae_nba \ nbaei_nbae) (complement_impl Ai)), language (id (complement_4 A))) \ - \\Id_on (alphabet (complement_4 A))\ stream_rel\ set_rel" - using complement_impl.refine[OF assms, unfolded to_nbaei_def id_apply, THEN RETURN_nres_relD] - by parametricity - also have "language (id (complement_4 A)) = streams (alphabet A) - language A" - using assms(1) complement_4_correct by simp + (* 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 diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Translate.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Translate.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Translate.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Translate.thy @@ -1,267 +1,248 @@ section \Explore and Enumerate Nodes of Nondeterministic Büchi Automata\ theory NBA_Translate imports NBA_Explicit begin subsection \Syntax\ (* TODO: this syntax has unnecessarily high inner binding strength, requiring extra parentheses the regular let syntax correctly uses inner binding strength 0: ("(2_ =/ _)" 10) *) no_syntax "_do_let" :: "[pttrn, 'a] \ do_bind" ("(2let _ =/ _)" [1000, 13] 13) syntax "_do_let" :: "[pttrn, 'a] \ do_bind" ("(2let _ =/ _)" 13) section \Image on Explicit Automata\ + (* TODO: this should not be needed, only use nba_image *) definition nbae_image where "nbae_image f A \ nbae (alphabete A) (f ` initiale A) ((\ (p, a, q). (f p, a, f q)) ` transitione A) (f ` acceptinge A)" lemma nbae_image_param[param]: "(nbae_image, nbae_image) \ (S \ T) \ \L, S\ nbae_rel \ \L, T\ nbae_rel" unfolding nbae_image_def by parametricity lemma nbae_image_id[simp]: "nbae_image id = id" unfolding nbae_image_def by auto lemma nbae_image_nba_nbae: "nbae_image f (nba_nbae A) = nbae (alphabet A) (f ` initial A) (\ p \ nodes A. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) (f ` {p \ nodes A. accepting A p})" unfolding nba_nbae_def nbae_image_def nbae.simps Set.filter_def by force section \Exploration and Translation\ definition trans_spec where "trans_spec A f \ \ p \ nodes A. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p" definition trans_algo where "trans_algo N L S f \ FOREACH N (\ p T. do { ASSERT (p \ N); FOREACH L (\ a T. do { ASSERT (a \ L); FOREACH (S a p) (\ q T. do { ASSERT (q \ S a p); ASSERT ((f p, a, f q) \ T); RETURN (insert (f p, a, f q) T) } ) T } ) T } ) {}" lemma trans_algo_refine: assumes "finite (nodes A)" "finite (alphabet A)" "inj_on f (nodes A)" assumes "N = nodes A" "L = alphabet A" "S = transition A" shows "(trans_algo N L S f, SPEC (HOL.eq (trans_spec A f))) \ \Id\ nres_rel" unfolding trans_algo_def trans_spec_def assms(4-6) proof (refine_vcg FOREACH_rule_insert_eq) show "finite (nodes A)" using assms(1) by this show "(\ p \ nodes A. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) = (\ p \ nodes A. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p)" by rule show "(\ p \ {}. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) = {}" by simp fix T x assume 1: "T \ nodes A" "x \ nodes A" "x \ T" show "finite (alphabet A)" using assms(2) by this show "(\ a \ {}. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) = (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p)" "(\ a \ alphabet A. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) = (\ p \ insert x T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p)" by auto fix Ta xa assume 2: "Ta \ alphabet A" "xa \ alphabet A" "xa \ Ta" show "finite (transition A xa x)" using 1 2 assms(1) by (meson infinite_subset nba.nodes_transition subsetI) show "(f ` {x} \ {xa} \ f ` transition A xa x) \ (\ a \ Ta. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) = (\ a \ insert xa Ta. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p)" by auto show "(f ` {x} \ {xa} \ f ` {}) \ (\ a \ Ta. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) = (\ a \ Ta. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p)" by auto fix Tb xb assume 3: "Tb \ transition A xa x" "xb \ transition A xa x" "xb \ Tb" show "(f x, xa, f xb) \ f ` {x} \ {xa} \ f ` Tb \ (\ a \ Ta. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p)" using 1 2 3 assms(3) by (blast dest: inj_onD) show "f ` {x} \ {xa} \ f ` insert xb Tb \ (\ a \ Ta. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p) = insert (f x, xa, f xb) (f ` {x} \ {xa} \ f ` Tb \ (\ a \ Ta. f ` {x} \ {a} \ f ` transition A a x) \ (\ p \ T. \ a \ alphabet A. f ` {p} \ {a} \ f ` transition A a p))" by auto qed - (* TODO: this operation is fundamentally nondeterministic, model it as such, instead of - putting everything in the relation *) - (* TODO: by setting this to id, we pretend that nothing is actually happening with this - translation and put all the weight on the relation, it would make more sense to model - the fact that a translation is happening explicitly *) - definition to_nbaei :: "('state, 'label) nba \ ('state, 'label) nba" - where "to_nbaei \ id" + (* TODO: move this to nondeterministic automaton + there, it will have to be treated more elementarily + at least until we abstract from NBA_Refine to do that there aswell *) + definition nba_image :: "('state\<^sub>1 \ 'state\<^sub>2) \ ('label, 'state\<^sub>1) nba \ ('label, 'state\<^sub>2) nba" where + "nba_image f A \ nba + (alphabet A) + (f ` initial A) + (\ a p. f ` transition A a (inv_into (nodes A) f p)) + (\ p. accepting A (inv_into (nodes A) f p))" + + lemma nba_image_rel[param]: + assumes "inj_on f (nodes A)" + shows "(A, nba_image f A) \ \Id_on (alphabet A), br f (\ p. p \ nodes A)\ nba_rel" + proof - + have "A = nba (alphabet A) (initial A) (transition A) (accepting A)" by simp + also have "(\, nba_image f A) \ \Id_on (alphabet A), br f (\ p. p \ nodes A)\ nba_rel" + using assms unfolding nba_image_def + by (parametricity) (auto intro: nba_rel_eq simp: in_br_conv br_set_rel_alt) + finally show ?thesis by this + qed + + lemma nba_image_nodes[simp]: + assumes "inj_on f (nodes A)" + shows "nodes (nba_image f A) = f ` nodes A" + proof - + have "(nodes A, nodes (nba_image f A)) \ \br f (\ p. p \ nodes A)\ set_rel" + using assms by parametricity + then show ?thesis unfolding br_set_rel_alt by simp + qed + lemma nba_image_language[simp]: + assumes "inj_on f (nodes A)" + shows "language (nba_image f A) = language A" + proof - + have "(language A, language (nba_image f A)) \ \\Id_on (alphabet A)\ stream_rel\ set_rel" + using assms by parametricity + then show ?thesis by simp + qed + + lemma nba_image_nbae: + assumes "inj_on f (nodes A)" + shows "nbae_image f (nba_nbae A) = nba_nbae (nba_image f A)" + unfolding nbae_image_nba_nbae + unfolding nba_nbae_def + unfolding nba_image_nodes[OF assms] + unfolding nbae.simps + unfolding nba_image_def + unfolding nba.sel + using assms by auto + + (* TODO: with this, maybe much of the nbae infrastructure is obsolete? + since now there is very little happening in terms of relations, maybe we can even make do + with just the abstraction function *) + definition op_translate :: "('label, 'state) nba \ ('label, nat) nbae nres" where + "op_translate A \ SPEC (\ B. \ f. inj_on f (nodes A) \ B = nba_nbae (nba_image f A))" (* TODO: make separate implementations for "nba_nbae" and "op_set_enumerate \ nbae_image" make sure to do regression tests along the way *) schematic_goal to_nbaei_impl: fixes S :: "('statei \ 'state) set" assumes [simp]: "finite (nodes 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, do { let N = nodes A; f \ op_set_enumerate N; ASSERT (dom f = N); ASSERT (\ p \ initial A. f p \ None); ASSERT (\ a \ alphabet A. \ p \ dom f. \ q \ transition A a p. f q \ None); T \ trans_algo N (alphabet A) (transition A) (\ x. the (f x)); RETURN (nbae (alphabet A) ((\ x. the (f x)) ` initial A) T ((\ x. the (f x)) ` {p \ N. accepting A p})) }) \ ?R" unfolding trans_algo_def by (autoref_monadic (plain)) concrete_definition to_nbaei_impl uses to_nbaei_impl lemma to_nbaei_impl_refine'': fixes S :: "('statei \ 'state) set" assumes "finite (nodes A)" assumes "is_bounded_hashcode S seq bhc" assumes "is_valid_def_hm_size TYPE('statei) hms" assumes "(seq, HOL.eq) \ S \ S \ bool_rel" assumes "(Ai, A) \ \L, S\ nbai_nba_rel" - shows "(RETURN (to_nbaei_impl seq bhc hms Ai), do { - f \ op_set_enumerate (nodes A); - RETURN (nbae_image (the \ f) (nba_nbae A)) - }) \ \\L, nat_rel\ nbaei_nbae_rel\ nres_rel" + shows "(RETURN (to_nbaei_impl seq bhc hms Ai), op_translate A) \ + \\L, nat_rel\ nbaei_nbae_rel\ nres_rel" proof - have 1: "finite (alphabet A)" using nbai_nba_param(2)[param_fo, OF assms(5)] list_set_rel_finite unfolding finite_set_rel_def by auto note to_nbaei_impl.refine[OF assms] also have "(do { let N = nodes A; f \ op_set_enumerate N; ASSERT (dom f = N); ASSERT (\ p \ initial A. f p \ None); ASSERT (\ a \ alphabet A. \ p \ dom f. \ q \ transition A a p. f q \ None); T \ trans_algo N (alphabet A) (transition A) (\ x. the (f x)); RETURN (nbae (alphabet A) ((\ x. the (f x)) ` initial A) T ((\ x. the (f x)) ` {p \ N. accepting A p})) }, do { f \ op_set_enumerate (nodes A); T \ SPEC (HOL.eq (trans_spec A (\ x. the (f x)))); RETURN (nbae (alphabet A) ((\ x. the (f x)) ` initial A) T ((\ x. the (f x)) ` {p \ nodes A. accepting A p})) }) \ \Id\ nres_rel" unfolding Let_def comp_apply op_set_enumerate_def using assms(1) 1 by (refine_vcg vcg0[OF trans_algo_refine]) (auto intro!: inj_on_map_the[unfolded comp_apply]) also have "(do { f \ op_set_enumerate (nodes A); T \ SPEC (HOL.eq (trans_spec A (\ x. the (f x)))); RETURN (nbae (alphabet A) ((\ x. the (f x)) ` initial A) T ((\ x. the (f x)) ` {p \ nodes A. accepting A p})) - }, do { + }, do { f \ op_set_enumerate (nodes A); RETURN (nbae_image (the \ f) (nba_nbae A)) }) \ \Id\ nres_rel" unfolding trans_spec_def nbae_image_nba_nbae by refine_vcg force + also have "(do { + f \ op_set_enumerate (nodes A); + RETURN (nbae_image (the \ f) (nba_nbae A)) + }, do { + f \ op_set_enumerate (nodes A); + RETURN (nba_nbae (nba_image (the \ f) A)) + }) \ \Id\ nres_rel" + unfolding op_set_enumerate_def by (refine_vcg) (simp add: inj_on_map_the nba_image_nbae) + also have "(do { + f \ op_set_enumerate (nodes A); + RETURN (nba_nbae (nba_image (the \ f) A)) + }, op_translate A) \ \Id\ nres_rel" + unfolding op_set_enumerate_def op_translate_def + by (refine_vcg) (metis Collect_mem_eq inj_on_map_the subset_Collect_conv) finally show ?thesis unfolding nres_rel_comp by simp qed - (* TODO: generalize L *) - context - fixes Ai A - fixes seq bhc hms - fixes S :: "('statei \ 'state) set" - assumes a: "finite (nodes A)" - assumes b: "is_bounded_hashcode S seq bhc" - assumes c: "is_valid_def_hm_size TYPE('statei) hms" - assumes d: "(seq, HOL.eq) \ S \ S \ bool_rel" - assumes e: "(Ai, A) \ \Id, S\ nbai_nba_rel" - begin - - definition f' where "f' \ SOME f'. - (to_nbaei_impl seq bhc hms Ai, nbae_image (the \ f') (nba_nbae A)) \ \Id, nat_rel\ nbaei_nbae_rel \ - dom f' = nodes A \ inj_on f' (nodes A)" - - lemma 1: "\ f'. (to_nbaei_impl seq bhc hms Ai, nbae_image (the \ f') (nba_nbae A)) \ - \Id, nat_rel\ nbaei_nbae_rel \ dom f' = nodes A \ inj_on f' (nodes A)" - using to_nbaei_impl_refine''[ - OF a b c d e, - unfolded op_set_enumerate_def bind_RES_RETURN_eq, - THEN nres_relD, - THEN RETURN_ref_SPECD] - by force - - lemma f'_refine: "(to_nbaei_impl seq bhc hms Ai, nbae_image (the \ f') (nba_nbae A)) \ - \Id, nat_rel\ nbaei_nbae_rel" using someI_ex[OF 1, folded f'_def] by auto - lemma f'_dom: "dom f' = nodes A" using someI_ex[OF 1, folded f'_def] by auto - lemma f'_inj: "inj_on f' (nodes A)" using someI_ex[OF 1, folded f'_def] by auto - - definition f where "f \ the \ f'" - definition g where "g = inv_into (nodes A) f" - lemma inj_f[intro!, simp]: "inj_on f (nodes A)" - using f'_inj f'_dom unfolding f_def by (simp add: inj_on_map_the) - lemma inj_g[intro!, simp]: "inj_on g (f ` nodes A)" - unfolding g_def by (simp add: inj_on_inv_into) - - definition rel where "rel \ {(f p, p) |p. p \ nodes A}" - lemma rel_alt_def: "rel = (br f (\ p. p \ nodes A))\" - unfolding rel_def by (auto simp: in_br_conv) - lemma rel_inv_def: "rel = br g (\ k. k \ f ` nodes A)" - unfolding rel_alt_def g_def by (auto simp: in_br_conv) - lemma rel_domain[simp]: "Domain rel = f ` nodes A" unfolding rel_def by force - lemma rel_range[simp]: "Range rel = nodes A" unfolding rel_def by auto - lemma rel_bijective[intro!, simp]: "bijective rel" unfolding rel_inv_def by (simp add: bijective_alt) - lemma [simp]: "Id_on (f ` nodes A) O rel = rel" unfolding rel_def by auto - lemma [simp]: "rel O Id_on (nodes A) = rel" unfolding rel_def by auto - - lemma [param]: "(f, f) \ Id_on (Range rel) \ Id_on (Domain rel)" unfolding rel_alt_def by auto - lemma [param]: "(g, g) \ Id_on (Domain rel) \ Id_on (Range rel)" unfolding rel_inv_def by auto - lemma [param]: "(id, f) \ rel \ Id_on (Domain rel)" unfolding rel_alt_def by (auto simp: in_br_conv) - lemma [param]: "(f, id) \ Id_on (Range rel) \ rel" unfolding rel_alt_def by (auto simp: in_br_conv) - lemma [param]: "(id, g) \ Id_on (Domain rel) \ rel" unfolding rel_inv_def by (auto simp: in_br_conv) - lemma [param]: "(g, id) \ rel \ Id_on (Range rel)" unfolding rel_inv_def by (auto simp: in_br_conv) - - lemma f_refine: "(to_nbaei_impl seq bhc hms Ai, nbae_image f (nba_nbae A)) \ - \Id, nat_rel\ nbaei_nbae_rel" using f'_refine unfolding f_def by this - - lemma nba_f_refine: "(nbae_nba (nbae_image f (nba_nbae A)), A) \ \Id_on (alphabet A), rel\ nba_rel" - proof - - have "(nbae_nba (nbae_image f (nba_nbae A)), nbae_nba (nbae_image id (nba_nbae A))) \ - \Id_on (alphabet A), rel\ nba_rel" using nba_rel_eq by parametricity auto - also have "nbae_nba (nbae_image id (nba_nbae A)) = (nbae_nba \ nba_nbae) A" by simp - also have "(\, id A) \ \Id_on (alphabet A), Id_on (nodes A)\ nba_rel" by parametricity - finally show ?thesis by simp - qed - lemma to_nbaei_impl_refine': - "(to_nbaei_impl seq bhc hms Ai, to_nbaei A) \ \Id_on (alphabet A), rel\ nbaei_nba_rel" - proof - - have "(nbae_nba (nbaei_nbae (to_nbaei_impl seq bhc hms Ai)), nbae_nba (id (nbae_image f (nba_nbae A)))) \ - \Id, nat_rel\ nba_rel" using f_refine by parametricity auto - also have "(nbae_nba (id (nbae_image f (nba_nbae A))), A) \ - \Id_on (alphabet A), rel\ nba_rel" using nba_f_refine by simp - finally show ?thesis unfolding nbaei_nba_rel_def to_nbaei_def by simp - qed - - end - context begin interpretation autoref_syn by this lemma to_nbaei_impl_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) \ \Id, S\ nbai_nba_rel" - shows "(to_nbaei_impl seq bhc hms Ai, - (OP to_nbaei ::: \Id, S\ nbai_nba_rel \ - \Id_on (alphabet A), rel Ai A seq bhc hms\ nbaei_nba_rel) $ A) \ - \Id_on (alphabet A), rel Ai A seq bhc hms\ nbaei_nba_rel" - using to_nbaei_impl_refine' assms unfolding autoref_tag_defs by this + assumes "(Ai, A) \ \L, S\ nbai_nba_rel" + shows "(RETURN (to_nbaei_impl seq bhc hms Ai), + (OP op_translate ::: \L, S\ nbai_nba_rel \ \\L, nat_rel\ nbaei_nbae_rel\ nres_rel) $ A) \ + \\L, nat_rel\ nbaei_nbae_rel\ nres_rel" + using to_nbaei_impl_refine'' assms unfolding autoref_tag_defs by this end end \ No newline at end of file