From f903644cca7c81ea07d27addcde6d8b34f648075 Mon Sep 17 00:00:00 2001 From: Dmitriy Traytel Date: Tue, 5 Mar 2024 19:05:50 +0100 Subject: [PATCH] Labeled FSet formalization --- thys/POPLmark/Labeled_FSet.thy | 372 +++++++++++++++++++++++++++++++++ thys/POPLmark/SystemFSub.thy | 6 +- 2 files changed, 377 insertions(+), 1 deletion(-) create mode 100644 thys/POPLmark/Labeled_FSet.thy diff --git a/thys/POPLmark/Labeled_FSet.thy b/thys/POPLmark/Labeled_FSet.thy new file mode 100644 index 00000000..77922301 --- /dev/null +++ b/thys/POPLmark/Labeled_FSet.thy @@ -0,0 +1,372 @@ +theory Labeled_FSet + imports Binders.MRBNF_Composition "HOL-Library.FSet" +begin + +abbreviation nonrep_pair :: "'a \ 'b \ bool" where "nonrep_pair _ \ True" +abbreviation nonrep_fset :: "'a fset \ bool" where "nonrep_fset _ \ True" +definition nonrep_lfset :: "('a \ 'b) fset \ bool" where + "nonrep_lfset X = (nonrep_fset X \ (\x \ fset X. nonrep_pair x) \ + (\x \ fset X. \y \ fset X. x \ y \ Basic_BNFs.fsts x \ Basic_BNFs.fsts y = {}))" + +lemma nonrep_lfset_alt: + "nonrep_lfset X = (\a b c. (a, b) |\| X \ (a, c) |\| X \ b = c)" + unfolding nonrep_lfset_def prod_set_defs by fastforce + +typedef ('a, 'b) G = "UNIV :: ('a \ 'b) fset set" by auto +context notes [[bnf_internals]] begin +copy_bnf ('a, 'b) G +end +setup_lifting type_definition_G + +lemma map_G_transfer[transfer_rule]: + "rel_fun (=) (rel_fun (=) (rel_fun (pcr_G (=) (=)) (pcr_G (=) (=)))) (\f g. (|`|) (map_prod f g)) map_G" + by (tactic \Local_Defs.unfold_tac @{context} + [BNF_Def.bnf_of @{context} @{type_name G} |> the |> BNF_Def.map_def_of_bnf]\) + (simp add: rel_fun_def pcr_G_def cr_G_def prod.rel_eq fset.rel_eq relcompp_apply Abs_G_inverse) + +lift_definition nonrep_G :: "('a, 'b) G \ bool" is nonrep_lfset . + +lemma nonrep_G_map: "bij f \ nonrep_G x \ nonrep_G (map_G f g x)" + by (transfer fixing: f g) + (force simp: nonrep_lfset_alt map_prod_def fimage_iff the_inv_f_f bij_is_inj + dest!: bij_the_inv_revert[of f, THEN iffD2, rotated]) + +lemma nonrep_G_map_fst_snd: + "nonrep_G (map_G f fst x) \ nonrep_G (map_G f snd x) \ nonrep_G (map_G f id x)" + apply transfer + apply (auto simp: nonrep_lfset_alt map_prod_def image_iff split_beta) + by (metis fst_conv snd_conv)+ + +lemma nonrep_G_map_fst_snd_bij: + "bij f \ nonrep_G (map_G f fst x) \ nonrep_G (map_G f snd x) \ nonrep_G x" + apply (transfer fixing: f) + apply (auto simp: nonrep_lfset_alt map_prod_def image_iff split_beta) + by (metis fst_conv snd_conv)+ + +class large_G = + fixes dummy :: 'a + assumes large_G: "bd_G \o |UNIV :: 'a set|" + +instantiation nat :: large_G begin +instance proof +qed (metis Card_order_iff_ordLeq_card_of card_order_on_Card_order G.bd_card_order) +end + +instantiation prod :: (type, large_G) large_G begin +instance proof +qed (subst UNIV_prod, auto simp only: intro!: ordLeq_transitive[OF large_G card_of_Times2]) +end + +typedef ('a, 'b) lfset = "{x :: ('a :: large_G, 'b) G . nonrep_G x}" + unfolding mem_Collect_eq + by transfer (auto simp: nonrep_lfset_alt) + +definition map_lfset :: "('a :: large_G \ 'a :: large_G) \ ('b \ 'b') \ ('a, 'b) lfset \ ('a, 'b') lfset" where + "map_lfset f g = Abs_lfset o map_G f g o Rep_lfset" + +definition labels :: "('a :: large_G, 'b) lfset \ 'a set" where + "labels = set1_G o Rep_lfset" + +definition "values" :: "('a :: large_G, 'b) lfset \ 'b set" where + "values = set2_G o Rep_lfset" + +definition rel_lfset :: "('a :: large_G \ 'a :: large_G) \ ('b \ 'b' \ bool) \ ('a, 'b) lfset \ ('a, 'b') lfset \ bool" where + "rel_lfset f S = BNF_Def.vimage2p Rep_lfset Rep_lfset (rel_G (Grp f) S)" + +theorem lfset_map_id: "map_lfset id id = id" + unfolding map_lfset_def G.map_id fun_eq_iff o_apply Rep_lfset_inverse id_apply + by (rule allI, rule refl) + +theorem lfset_map_comp: "bij u \ map_lfset (v o u) (f o g) = map_lfset v f o map_lfset u g" + by (simp only: map_lfset_def fun_eq_iff o_apply simp_thms G.map_comp + Abs_lfset_inverse[unfolded mem_Collect_eq] nonrep_G_map Rep_lfset[unfolded mem_Collect_eq]) + +theorem lfset_set1_map: "bij u \ labels o map_lfset u g = image u o labels" + by (simp only: labels_def map_lfset_def fun_eq_iff o_apply simp_thms G.set_map + Abs_lfset_inverse[unfolded mem_Collect_eq] nonrep_G_map Rep_lfset[unfolded mem_Collect_eq]) + +theorem lfset_set2_map: "bij u \ values o map_lfset u g = image g o values" + by (simp only: values_def map_lfset_def fun_eq_iff o_apply simp_thms G.set_map + Abs_lfset_inverse[unfolded mem_Collect_eq] nonrep_G_map Rep_lfset[unfolded mem_Collect_eq]) + +theorem lfset_map_cong: + assumes "\a. a \ labels p \ u a = v a" "\a. a \ values p \ g a = h a" + shows "map_lfset u g p = map_lfset v h p" + by (simp only: map_lfset_def o_apply labels_def values_def assms cong: G.map_cong) + +theorem lfset_set_bd: "|labels p| rel_lfset f R x y = (\z. values z \ {(x,y). R x y} \ map_lfset id fst z = x \ map_lfset f snd z = y)" + unfolding rel_lfset_def vimage2p_def G.in_rel + apply safe + subgoal for z + apply (subgoal_tac "nonrep_G (map_G fst id z)") + apply (rule exI[of _ "Abs_lfset (map_G fst id z)"]) + apply (cases x; cases y) + apply (auto simp: map_lfset_def values_def Grp_def + Abs_lfset_inverse Rep_lfset[simplified] nonrep_G_map G.set_map G.map_comp + G.map_comp[of "inv f" id snd snd, simplified, symmetric] + intro!: Abs_lfset_inject[THEN iffD2] G.map_cong nonrep_G_map_fst_snd + arg_cong[of _ _ nonrep_G, OF G.map_cong[of _ _ fst "inv f o snd" snd snd, OF refl], THEN iffD2] + elim!: arg_cong[of _ _ nonrep_G, THEN iffD1, rotated]) + done + subgoal for z + apply (rule exI[of _ "map_G (\x. (x, f x)) id (Rep_lfset z)"]) + apply (auto simp: G.set_map G.map_comp Grp_def values_def map_lfset_def Abs_lfset_inverse Rep_lfset[simplified] nonrep_G_map + intro!: G.map_cong) + done + done + +theorem lfset_rel_compp_le: + "rel_lfset f R OO rel_lfset g S \ rel_lfset (g o f) (R OO S)" + unfolding rel_lfset_def G.rel_compp Grp_o + by (rule vimage2p_relcompp_mono[OF order_refl]) +(* + unfolding vimage2p_Grp fun_eq_iff relcompp_apply conversep_iff eqTrueI[OF UNIV_I] simp_thms + apply (safe elim!: GrpE) + subgoal premises prems for x y _ _ z + proof (cases z rule: Rep_lfset_cases[unfolded mem_Collect_eq, case_names nonrep_G Rep_lfset]) + case nonrep_G + with prems(2,5) Rep_lfset[of x] show ?case + + apply (auto simp: G.in_rel Grp_def) find_theorems nonrep_G sorry + next + case (Rep_lfset x) + with prems show ?thesis by (auto simp: Grp_def) + qed + done +*) + +(* TODO @ Jan +mrbnf "('a :: large_G, 'b) lfset" + map: map_lfset + sets: bound: labels live: "values" + bd: "bd_G" + rel: "rel_lfset id" + var_class: large_G + subgoal by (rule ext, transfer) simp + subgoal apply (rule ext, transfer) by (simp add: stream.map_comp inj_on_def) + subgoal apply transfer by (simp cong: stream.map_cong inj_on_cong) + subgoal apply (rule ext, transfer) by (simp add: inj_on_def) + subgoal by (rule infinite_regular_card_order_card_suc[OF natLeq_card_order natLeq_Cinfinite]) + subgoal + apply (rule card_suc_greater_set[OF natLeq_card_order]) + apply transfer + apply (simp flip: countable_card_le_natLeq add: countable_sset) + done + subgoal by blast + subgoal by (clarsimp, transfer) auto + done +*) + +(* locale+interpretation as a trick to get automatic proofs and replace new constants + by existing ones afterwards *) +locale AUX +lift_bnf (in AUX) (dead 'a :: large_G, aux_set_lfset: 'b) lfset [wits: "Abs_G {||} :: ('a :: large_G, 'b) G"] + for map: aux_map_lfset rel: aux_rel_lfset + by (auto simp add: nonrep_G.abs_eq nonrep_lfset_def Abs_G_inverse set2_G_def + intro: nonrep_G_map nonrep_G_map_fst_snd_bij) + +(*FIXME for J: problem with tactic in datatype and primrec otherwise*) +definition [simp]: "map_lfset_id = map_lfset id" +definition [simp]: "rel_lfset_id = rel_lfset id" + +interpretation AUX + rewrites "AUX.aux_map_lfset = map_lfset_id" and "AUX.aux_rel_lfset = rel_lfset_id" and "AUX.aux_set_lfset = values" + by (tactic \Local_Defs.unfold_tac @{context} (@{thms values_def map_lfset_def rel_lfset_def map_lfset_id_def rel_lfset_id_def eq_alt[symmetric]} @ + maps (fn f => BNF_Def.bnf_of @{context} @{type_name lfset} |> the |> f) [BNF_Def.set_defs_of_bnf, + single o BNF_Def.map_def_of_bnf, single o BNF_Def.rel_def_of_bnf])\) (rule refl)+ + +context begin + +qualified definition "Rep = Rep_G o Rep_lfset" +qualified definition "Abs = Abs_lfset o Abs_G" + +lemma type_definition_lfset: + "type_definition Rep Abs {X. nonrep_lfset X}" + by unfold_locales + (auto simp: Rep_def Abs_def Rep_lfset[unfolded mem_Collect_eq] nonrep_G.abs_eq[symmetric] + Rep_G_inverse Rep_lfset_inverse Abs_lfset_inverse Abs_G_inverse) + +setup_lifting type_definition_lfset + +lemma map_lfset_id_transfer[transfer_rule]: + "rel_fun (=) (rel_fun (pcr_lfset (=) (=)) (pcr_lfset (=) (=))) (\g. fimage (map_prod id g)) (map_lfset id)" + unfolding rel_fun_def pcr_lfset_def cr_lfset_def prod.rel_eq fset.rel_eq eq_OO map_lfset_def Rep_def o_apply + by (subst Abs_lfset_inverse; simp add: Rep_lfset[simplified] nonrep_G_map) + (tactic \Local_Defs.unfold_tac @{context} + [BNF_Def.bnf_of @{context} @{type_name G} |> the |> BNF_Def.map_def_of_bnf]\, simp add: Abs_G_inverse) + +lemma labels_transfer[transfer_rule]: + "rel_fun (pcr_lfset (=) (=)) (rel_set (=)) (image fst o fset) labels" + unfolding rel_fun_def pcr_lfset_def cr_lfset_def prod.rel_eq fset.rel_eq eq_OO labels_def Rep_def o_apply + by (tactic \Local_Defs.unfold_tac @{context} + (BNF_Def.bnf_of @{context} @{type_name G} |> the |> BNF_Def.set_defs_of_bnf)\) + (auto simp: rel_fun_def rel_set_eq elim: image_eqI[rotated]) + +lemma values_transfer[transfer_rule]: + "rel_fun (pcr_lfset (=) (=)) (rel_set (=)) (image snd o fset) values" + unfolding rel_fun_def pcr_lfset_def cr_lfset_def prod.rel_eq fset.rel_eq eq_OO values_def Rep_def o_apply + by (tactic \Local_Defs.unfold_tac @{context} + (BNF_Def.bnf_of @{context} @{type_name G} |> the |> BNF_Def.set_defs_of_bnf)\) + (auto simp: rel_fun_def rel_set_eq elim: image_eqI[rotated]) + +lemma rel_lfset_eq_transfer[transfer_rule]: + "rel_fun (=) (rel_fun (pcr_lfset (=) (=)) (rel_fun (pcr_lfset (=) (=)) (=))) (\R. rel_fset (rel_prod (=) R)) (rel_lfset id)" + unfolding rel_fun_def pcr_lfset_def cr_lfset_def prod.rel_eq fset.rel_eq eq_OO rel_lfset_def Rep_def o_apply + by (tactic \Local_Defs.unfold_tac @{context} + [BNF_Def.bnf_of @{context} @{type_name G} |> the |> BNF_Def.rel_def_of_bnf]\, + simp add: Abs_G_inverse vimage2p_def eq_alt[symmetric]) + +end + +lift_definition lfin :: "('a \ 'b) \ ('a::large_G, 'b) lfset \ bool" (infix "\\" 50) is fmember . + +lemma lfin_map_lfset: "(a, b) \\ map_lfset id g x \ (\c. b = g c \ (a, c) \\ x)" + by transfer force + +lemma lfin_label_inject: "(a, b) \\ x \ (a, c) \\ x \ b = c" + by transfer (auto simp: nonrep_lfset_alt) + +lift_definition lfempty :: "('a::large_G, 'b) lfset" is "{||} :: ('a \ 'b) fset" + by (auto simp: nonrep_lfset_alt) + +lemma labels_lfempty[simp]: "labels lfempty = {}" + by transfer auto + +lemma labels_empty_iff[simp]: "labels X = {} \ X = lfempty" + by transfer auto + +lemma values_lfempty[simp]: "values lfempty = {}" + by transfer auto + +lemma lfin_lfempty[simp]: "x \\ lfempty = False" + by transfer auto + +lemma lfin_values: "(l, c) \\ x \ c \ values x" + by transfer force + +lemma finite_labels[simp]: "finite (labels x)" + by transfer auto + +lemma finite_values[simp]: "finite (values x)" + by transfer auto + +lemma values_lfin: "c \ values x \ \l. (l, c) \\ x" + by transfer force + +lemma pred_lfset_lfempty[simp]: "pred_lfset P lfempty = True" + unfolding lfset.pred_set by auto + +lift_definition lfinsert :: "'a \ 'b \ ('a::large_G, 'b) lfset \ ('a, 'b) lfset" + is "\a b X. if \c. b \ c \ (a, c) |\| X then X else finsert (a, b) X" + by (auto simp: nonrep_lfset_alt split_beta split: if_splits) metis + +lift_definition lfupdate :: "('a::large_G, 'b) lfset \ 'a \ 'b \ ('a, 'b) lfset" + is "\X a b. finsert (a, b) (ffilter (\(a', _). a \ a') X)" + by (auto simp: nonrep_lfset_alt) + +lift_definition lfunion :: "('a::large_G, 'b) lfset \ ('a, 'b) lfset \ ('a, 'b) lfset" + is "\X Y. funion Y (ffilter (\(a, _). a |\| fst |`| Y) X)" + by (auto simp: nonrep_lfset_alt image_iff) + +nonterminal lfupdbinds and lfupdbind + +syntax + "_lfupdbind" :: "'a \ 'a \ lfupdbind" ("(2_ :=/ _)") + "" :: "lfupdbind \ lfupdbinds" ("_") + "_lfupdbinds":: "lfupdbind \ lfupdbinds \ lfupdbinds" ("_,/ _") + "_lfUpdate" :: "'a \ lfupdbinds \ 'a" ("_/\(_)\" [1000, 0] 900) + +translations + "_lfUpdate f (_lfupdbinds b bs)" \ "_lfUpdate (_lfUpdate f b) bs" + "f\x:=y\" \ "CONST lfupdate f x y" + + +subsection \Size setup\ + +lift_definition size_lfset :: "('a::large_G \ nat) \ ('b \ nat) \ ('a, 'b) lfset \ nat" is + "\f g. size_fset (size_prod f g)" . + +instantiation lfset :: (large_G,type) size begin +definition size_lfset where + size_lfset_overloaded_def: "size_lfset = Labeled_FSet.size_lfset (\_. 0) (\_. 0)" +instance .. +end + +lemmas size_lfset_simps = + size_lfset_def[THEN meta_eq_to_obj_eq, THEN fun_cong, THEN fun_cong, + unfolded map_fun_def comp_def id_apply] + +lemmas size_lfset_overloaded_simps = + size_lfset_simps[of "\_. 0" "\_. 0", unfolded add_0_left add_0_right, + folded size_lfset_overloaded_def] + +lemma lfset_size_o_map: + "inj f \ size_lfset (\_. 0) g \ map_lfset_id f = size_lfset (\_. 0) (g \ f)" + unfolding fun_eq_iff o_apply map_lfset_id_def + by transfer + (subst fun_cong[OF fset_size_o_map, unfolded o_apply], + auto simp add: inj_on_def split_beta map_prod_def size_prod_simp) + +setup \ +BNF_LFP_Size.register_size_global @{type_name lfset} @{const_name size_lfset} + @{thm size_lfset_overloaded_def} @{thms size_lfset_simps size_lfset_overloaded_simps} + @{thms lfset_size_o_map} +\ + +lemma size_fset_estimation[termination_simp]: "x \ fset X \ y < f x \ y < size_fset f X" + by (auto elim!: order.strict_trans2 + intro: order_trans[OF member_le_sum ordered_comm_monoid_add_class.sum_mono]) + +lemma size_fset_estimation'[termination_simp]: "x \ fset X \ y \ f x \ y \ size_fset f X" + by (auto elim!: order_trans + intro: order_trans[OF member_le_sum ordered_comm_monoid_add_class.sum_mono]) + +lemma size_lfset_estimation[termination_simp]: + "x \ values X \ y < f x \ y < size_lfset (\_. 0) f X" + by transfer (auto simp del: size_fset_simps intro!: size_fset_estimation) + +lemma size_lfset_estimation'[termination_simp]: + "x \ values X \ y \ f x \ y \ size_lfset (\_. 0) f X" + by transfer (auto simp del: size_fset_simps intro!: size_fset_estimation') + +lift_definition apply_lfset :: "('a::large_G, 'b \ 'c) lfset \ ('a, 'b) lfset \ ('a, 'c) lfset" + is "\F X. if fst |`| F |\| fst |`| X then (\(a, f). (a, f (THE b. (a, b) |\| X))) |`| F else {||}" + by (force simp: nonrep_lfset_def) + +lemma lfin_apply_lfset: "labels F \ labels X \ + (a, fx) \\ apply_lfset F X \ (\f x. fx = f x \ (a, f) \\ F \ (a, x) \\ X)" + apply transfer + apply auto + subgoal for F X a f + apply (drule set_mp[where c = a], force) + apply safe + subgoal for a' x + apply (subst the1_equality[of _ x]) + apply (force simp: nonrep_lfset_def intro!: exI[of _ f] exI[of _ x])+ + done + done + subgoal for F X a f x + apply (erule image_eqI[rotated]) + apply simp + apply (subst the1_equality[of _ x]) + apply (force simp: nonrep_lfset_def)+ + done + done + +lifting_update lfset.lifting +lifting_forget lfset.lifting +declare fun_cong[OF lfset_size_o_map, +unfolded id_def inj_on_def, simplified, termination_simp] + +hide_fact (open) FSet.bex_simps FSet.ball_simps + + +end \ No newline at end of file diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy index dfada38e..41c26fc2 100644 --- a/thys/POPLmark/SystemFSub.thy +++ b/thys/POPLmark/SystemFSub.thy @@ -4,17 +4,21 @@ theory SystemFSub "Binders.Generic_Barendregt_Enhanced_Rule_Induction" "Prelim.Curry_LFP" "Prelim.FixedCountableVars" + "Labeled_FSet" begin declare bij_swap[simp] declare supp_id_bound[simp] +(*type_synonym label = nat*) + ML \ val ctors = [ (("TyVar", (NONE : mixfix option)), [@{typ 'var}]), (("Top", (NONE : mixfix option)), []), (("Fun", NONE), [@{typ 'rec}, @{typ 'rec}]), - (("Forall", NONE), [@{typ 'bvar}, @{typ 'rec}, @{typ 'brec}]) + (("Forall", NONE), [@{typ 'bvar}, @{typ 'rec}, @{typ 'brec}]) (*, + (("Rec", NONE), [@{typ "(label, 'rec) lfset"}]) *) ] val spec = {