diff --git a/src/HOL/BNF_Composition.thy b/src/HOL/BNF_Composition.thy --- a/src/HOL/BNF_Composition.thy +++ b/src/HOL/BNF_Composition.thy @@ -1,194 +1,190 @@ (* Title: HOL/BNF_Composition.thy Author: Dmitriy Traytel, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Copyright 2012, 2013, 2014 Composition of bounded natural functors. *) section \Composition of Bounded Natural Functors\ theory BNF_Composition imports BNF_Def -keywords - "copy_bnf" :: thy_defn and - "lift_bnf" :: thy_goal_defn begin lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp lemma empty_natural: "(\_. {}) \ f = image g \ (\_. {})" by (rule ext) simp lemma Union_natural: "Union \ image (image f) = image f \ Union" by (rule ext) (auto simp only: comp_apply) lemma in_Union_o_assoc: "x \ (Union \ gset \ gmap) A \ x \ (Union \ (gset \ gmap)) A" by (unfold comp_assoc) lemma comp_single_set_bd: assumes fbd_Card_order: "Card_order fbd" and fset_bd: "\x. |fset x| \o fbd" and gset_bd: "\x. |gset x| \o gbd" shows "|\(fset ` gset x)| \o gbd *c fbd" apply simp apply (rule ordLeq_transitive) apply (rule card_of_UNION_Sigma) apply (subst SIGMA_CSUM) apply (rule ordLeq_transitive) apply (rule card_of_Csum_Times') apply (rule fbd_Card_order) apply (rule ballI) apply (rule fset_bd) apply (rule ordLeq_transitive) apply (rule cprod_mono1) apply (rule gset_bd) apply (rule ordIso_imp_ordLeq) apply (rule ordIso_refl) apply (rule Card_order_cprod) done lemma csum_dup: "cinfinite r \ Card_order r \ p +c p' =o r +c r \ p +c p' =o r" apply (erule ordIso_transitive) apply (frule csum_absorb2') apply (erule ordLeq_refl) by simp lemma cprod_dup: "cinfinite r \ Card_order r \ p *c p' =o r *c r \ p *c p' =o r" apply (erule ordIso_transitive) apply (rule cprod_infinite) by simp lemma Union_image_insert: "\(f ` insert a B) = f a \ \(f ` B)" by simp lemma Union_image_empty: "A \ \(f ` {}) = A" by simp lemma image_o_collect: "collect ((\f. image g \ f) ` F) = image g \ collect F" by (rule ext) (auto simp add: collect_def) lemma conj_subset_def: "A \ {x. P x \ Q x} = (A \ {x. P x} \ A \ {x. Q x})" by blast lemma UN_image_subset: "\(f ` g x) \ X = (g x \ {x. f x \ X})" by blast lemma comp_set_bd_Union_o_collect: "|\(\((\f. f x) ` X))| \o hbd \ |(Union \ collect X) x| \o hbd" by (unfold comp_apply collect_def) simp lemma Collect_inj: "Collect P = Collect Q \ P = Q" by blast lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)\\ OO Grp (Collect (case_prod R)) snd = R" unfolding Grp_def fun_eq_iff relcompp.simps by auto lemma OO_Grp_cong: "A = B \ (Grp A f)\\ OO Grp A g = (Grp B f)\\ OO Grp B g" by (rule arg_cong) lemma vimage2p_relcompp_mono: "R OO S \ T \ vimage2p f g R OO vimage2p g h S \ vimage2p f h T" unfolding vimage2p_def by auto lemma type_copy_map_cong0: "M (g x) = N (h x) \ (f \ M \ g) x = (f \ N \ h) x" by auto lemma type_copy_set_bd: "(\y. |S y| \o bd) \ |(S \ Rep) x| \o bd" by auto lemma vimage2p_cong: "R = S \ vimage2p f g R = vimage2p f g S" by simp lemma Ball_comp_iff: "(\x. Ball (A x) f) \ g = (\x. Ball ((A \ g) x) f)" unfolding o_def by auto lemma conj_comp_iff: "(\x. P x \ Q x) \ g = (\x. (P \ g) x \ (Q \ g) x)" unfolding o_def by auto context fixes Rep Abs assumes type_copy: "type_definition Rep Abs UNIV" begin lemma type_copy_map_id0: "M = id \ Abs \ M \ Rep = id" using type_definition.Rep_inverse[OF type_copy] by auto lemma type_copy_map_comp0: "M = M1 \ M2 \ f \ M \ g = (f \ M1 \ Rep) \ (Abs \ M2 \ g)" using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto lemma type_copy_set_map0: "S \ M = image f \ S' \ (S \ Rep) \ (Abs \ M \ g) = image f \ (S' \ g)" using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff) lemma type_copy_wit: "x \ (S \ Rep) (Abs y) \ x \ S y" using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) = Grp (Collect (\x. P (f x))) (Abs \ h \ f)" unfolding vimage2p_def Grp_def fun_eq_iff by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] type_definition.Rep_inverse[OF type_copy] dest: sym) lemma type_copy_vimage2p_Grp_Abs: "\h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\x. P (g x))) (Rep \ h \ g)" unfolding vimage2p_def Grp_def fun_eq_iff by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] type_definition.Rep_inverse[OF type_copy] dest: sym) lemma type_copy_ex_RepI: "(\b. F b) = (\b. F (Rep b))" proof safe fix b assume "F b" show "\b'. F (Rep b')" proof (rule exI) from \F b\ show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto qed qed blast lemma vimage2p_relcompp_converse: "vimage2p f g (R\\ OO S) = (vimage2p Rep f R)\\ OO vimage2p Rep g S" unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def by (auto simp: type_copy_ex_RepI) end bnf DEADID: 'a map: "id :: 'a \ 'a" bd: natLeq rel: "(=) :: 'a \ 'a \ bool" by (auto simp add: natLeq_card_order natLeq_cinfinite) definition id_bnf :: "'a \ 'a" where "id_bnf \ (\x. x)" lemma id_bnf_apply: "id_bnf x = x" unfolding id_bnf_def by simp bnf ID: 'a map: "id_bnf :: ('a \ 'b) \ 'a \ 'b" sets: "\x. {x}" bd: natLeq rel: "id_bnf :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" pred: "id_bnf :: ('a \ bool) \ 'a \ bool" unfolding id_bnf_def apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] done lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV" unfolding id_bnf_def by unfold_locales auto ML_file \Tools/BNF/bnf_comp_tactics.ML\ ML_file \Tools/BNF/bnf_comp.ML\ -ML_file \Tools/BNF/bnf_lift.ML\ hide_fact DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0 DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer end diff --git a/src/HOL/Datatype_Examples/Lift_BNF.thy b/src/HOL/Datatype_Examples/Lift_BNF.thy --- a/src/HOL/Datatype_Examples/Lift_BNF.thy +++ b/src/HOL/Datatype_Examples/Lift_BNF.thy @@ -1,90 +1,253 @@ (* Title: HOL/Datatype_Examples/Lift_BNF.thy Author: Dmitriy Traytel, ETH Zürich Copyright 2015 Demonstration of the "lift_bnf" command. *) section \Demonstration of the \textbf{lift_bnf} Command\ theory Lift_BNF imports Main begin +subsection \Lifting \textbf{typedef}s\ + typedef 'a nonempty_list = "{xs :: 'a list. xs \ []}" by blast +setup_lifting type_definition_nonempty_list lift_bnf (no_warn_wits) (neset: 'a) nonempty_list for map: nemap rel: nerel - by simp_all + by auto typedef ('a :: finite, 'b) fin_nonempty_list = "{(xs :: 'a set, ys :: 'b list). ys \ []}" by blast +setup_lifting type_definition_fin_nonempty_list -lift_bnf (dead 'a :: finite, 'b) fin_nonempty_list +lift_bnf (no_warn_wits) (dead 'a :: finite, 'b) fin_nonempty_list + [wits: "\b. ({} :: 'a :: finite set, [b :: 'b])"] by auto datatype 'a tree = Leaf | Node 'a "'a tree nonempty_list" record 'a point = xCoord :: 'a yCoord :: 'a -copy_bnf ('a, 's) point_ext + +copy_bnf (no_warn_transfer) ('a, 's) point_ext typedef 'a it = "UNIV :: 'a set" by blast +setup_lifting type_definition_it + copy_bnf (plugins del: size) 'a it typedef ('a, 'b) T_prod = "UNIV :: ('a \ 'b) set" by blast +setup_lifting type_definition_T_prod + copy_bnf ('a, 'b) T_prod typedef ('a, 'b, 'c) T_func = "UNIV :: ('a \ 'b * 'c) set" by blast +setup_lifting type_definition_T_func + copy_bnf ('a, 'b, 'c) T_func typedef ('a, 'b) sum_copy = "UNIV :: ('a + 'b) set" by blast +setup_lifting type_definition_sum_copy + copy_bnf ('a, 'b) sum_copy typedef ('a, 'b) T_sum = "{Inl x | x. True} :: ('a + 'b) set" by blast -lift_bnf (no_warn_wits) ('a, 'b) T_sum [wits: "Inl :: 'a \ 'a + 'b"] - by (auto simp: map_sum_def sum_set_defs split: sum.splits) +lift_bnf (no_warn_wits, no_warn_transfer) ('a, 'b) T_sum [wits: "Inl :: 'a \ 'a + 'b"] + by (force simp: map_sum_def sum_set_defs split: sum.splits)+ typedef ('key, 'value) alist = "{xs :: ('key \ 'value) list. (distinct \ map fst) xs}" morphisms impl_of Alist proof show "[] \ {xs. (distinct o map fst) xs}" by simp qed +setup_lifting type_definition_alist + lift_bnf (dead 'k, 'v) alist [wits: "Nil :: ('k \ 'v) list"] - by simp_all + by auto typedef 'a myopt = "{X :: 'a set. finite X \ card X \ 1}" by (rule exI[of _ "{}"]) auto lemma myopt_type_def: "type_definition (\X. if card (Rep_myopt X) = 1 then Some (the_elem (Rep_myopt X)) else None) (\x. Abs_myopt (case x of Some x \ {x} | _ \ {})) (UNIV :: 'a option set)" apply unfold_locales apply (auto simp: Abs_myopt_inverse dest!: card_eq_SucD split: option.splits) apply (metis Rep_myopt_inverse) apply (metis One_nat_def Rep_myopt Rep_myopt_inverse Suc_le_mono card_0_eq le0 le_antisym mem_Collect_eq nat.exhaust) done -copy_bnf 'a myopt via myopt_type_def +copy_bnf (no_warn_transfer) 'a myopt via myopt_type_def typedef ('k, 'v) fmap = "{M :: ('k \ 'v). finite (dom M)}" by (rule exI[of _ Map.empty]) simp_all +setup_lifting type_definition_fmap lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k \ 'v option"] by auto +typedef ('a, 'b) tuple_dead = "UNIV :: ('a \ 'b) set" .. +typedef ('a, 'b) tuple_dead1 = "UNIV :: ('a \ 'b) set" .. +typedef ('a, 'b) tuple_dead2 = "UNIV :: ('a \ 'b) set" .. +typedef ('a, 'b, 'c) triple_dead = "UNIV :: ('a \ 'b \ 'c) set" .. +typedef ('a, 'b, 'c) triple_dead1 = "UNIV :: ('a \ 'b \ 'c) set" .. +typedef ('a, 'b, 'c) triple_dead2 = "UNIV :: ('a \ 'b \ 'c) set" .. +typedef ('a, 'b, 'c) triple_dead3 = "UNIV :: ('a \ 'b \ 'c) set" .. +typedef ('a, 'b, 'c) triple_dead12 = "UNIV :: ('a \ 'b \ 'c) set" .. +typedef ('a, 'b, 'c) triple_dead13 = "UNIV :: ('a \ 'b \ 'c) set" .. +typedef ('a, 'b, 'c) triple_dead23 = "UNIV :: ('a \ 'b \ 'c) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead1 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead2 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead3 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead4 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead12 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead13 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead14 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead23 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead24 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead34 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead123 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead124 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead134 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +typedef ('a, 'b, 'c, 'd) quadruple_dead234 = "UNIV :: ('a \ 'b \ 'c \ 'd) set" .. +setup_lifting type_definition_tuple_dead +setup_lifting type_definition_tuple_dead1 +setup_lifting type_definition_tuple_dead2 +setup_lifting type_definition_triple_dead +setup_lifting type_definition_triple_dead1 +setup_lifting type_definition_triple_dead2 +setup_lifting type_definition_triple_dead3 +setup_lifting type_definition_triple_dead12 +setup_lifting type_definition_triple_dead13 +setup_lifting type_definition_triple_dead23 +setup_lifting type_definition_quadruple_dead +setup_lifting type_definition_quadruple_dead1 +setup_lifting type_definition_quadruple_dead2 +setup_lifting type_definition_quadruple_dead3 +setup_lifting type_definition_quadruple_dead4 +setup_lifting type_definition_quadruple_dead12 +setup_lifting type_definition_quadruple_dead13 +setup_lifting type_definition_quadruple_dead14 +setup_lifting type_definition_quadruple_dead23 +setup_lifting type_definition_quadruple_dead24 +setup_lifting type_definition_quadruple_dead34 +setup_lifting type_definition_quadruple_dead123 +setup_lifting type_definition_quadruple_dead124 +setup_lifting type_definition_quadruple_dead134 +setup_lifting type_definition_quadruple_dead234 + +lift_bnf (no_warn_wits) ( 'a, 'b) tuple_dead by auto +lift_bnf (no_warn_wits) (dead 'a, 'b) tuple_dead1 by auto +lift_bnf (no_warn_wits) ( 'a, dead 'b) tuple_dead2 by auto +lift_bnf (no_warn_wits) ( 'a, 'b, 'c) triple_dead by auto +lift_bnf (no_warn_wits) (dead 'a, 'b, 'c) triple_dead1 by auto +lift_bnf (no_warn_wits) ( 'a, dead 'b, 'c) triple_dead2 by auto +lift_bnf (no_warn_wits) ( 'a, 'b, dead 'c) triple_dead3 by auto +lift_bnf (no_warn_wits) (dead 'a, dead 'b, 'c) triple_dead12 by auto +lift_bnf (no_warn_wits) (dead 'a, 'b, dead 'c) triple_dead13 by auto +lift_bnf (no_warn_wits) ( 'a, dead 'b, dead 'c) triple_dead23 by auto +lift_bnf (no_warn_wits) ( 'a, 'b, 'c, 'd) quadruple_dead by auto +lift_bnf (no_warn_wits) (dead 'a, 'b, 'c, 'd) quadruple_dead1 by auto +lift_bnf (no_warn_wits) ( 'a, dead 'b, 'c, 'd) quadruple_dead2 by auto +lift_bnf (no_warn_wits) ( 'a, 'b, dead 'c, 'd) quadruple_dead3 by auto +lift_bnf (no_warn_wits) ( 'a, 'b, 'c, dead 'd) quadruple_dead4 by auto +lift_bnf (no_warn_wits) (dead 'a, dead 'b, 'c, 'd) quadruple_dead12 by auto +lift_bnf (no_warn_wits) (dead 'a, 'b, dead 'c, 'd) quadruple_dead13 by auto +lift_bnf (no_warn_wits) (dead 'a, 'b, 'c, dead 'd) quadruple_dead14 by auto +lift_bnf (no_warn_wits) ( 'a, dead 'b, dead 'c, 'd) quadruple_dead23 by auto +lift_bnf (no_warn_wits) ( 'a, dead 'b, 'c, dead 'd) quadruple_dead24 by auto +lift_bnf (no_warn_wits) ( 'a, 'b, dead 'c, dead 'd) quadruple_dead34 by auto +lift_bnf (no_warn_wits) (dead 'a, dead 'b, dead 'c, 'd) quadruple_dead123 by auto +lift_bnf (no_warn_wits) (dead 'a, dead 'b, 'c, dead 'd) quadruple_dead124 by auto +lift_bnf (no_warn_wits) (dead 'a, 'b, dead 'c, dead 'd) quadruple_dead134 by auto +lift_bnf (no_warn_wits) ( 'a, dead 'b, dead 'c, dead 'd) quadruple_dead234 by auto + +subsection \Lifting \textbf{quotient_type}s\ + +quotient_type 'a cpy_list = "'a list" / "(=)" + by (rule identity_equivp) + +lift_bnf 'a cpy_list [wits: "[]"] + by (auto intro: list_all2_trans) + +quotient_type ('a, 'b) funk = "('a \ 'b)" / "\f g. \a. f a = g a" + unfolding equivp_def by metis + +lemma funk_closure: "{(x, x'). \a. x a = x' a} `` {x. range x \ A} = {x. range x \ A}" + by auto + +lift_bnf (dead 'a, 'b) funk [wits: "\b _.b :: 'b"] + unfolding funk_closure rel_fun_def by (auto 0 10 split: if_splits) + +lemma assumes "equivp REL" + shows "REL OO REL OO R = REL OO R" + using equivp_transp[OF assms] equivp_reflp[OF assms] + by blast + +inductive ignore_Inl :: "'a + 'a \ 'a + 'a \ bool" where + "ignore_Inl (Inl x) (Inl y)" +| "ignore_Inl (Inr x) (Inr x)" + +inductive_simps [simp]: + "ignore_Inl (Inl x) y" + "ignore_Inl (Inr x') y" + "ignore_Inl y (Inl x)" + "ignore_Inl y (Inr x')" + +quotient_type 'a opt = "'a + 'a" / ignore_Inl + apply(auto intro!: equivpI simp add: reflp_def symp_def transp_def elim!: ignore_Inl.cases) + subgoal for x by(cases x) simp_all. + +lemma ignore_Inl_map_respect: + "(rel_fun (=) (rel_fun ignore_Inl ignore_Inl)) (\f. map_sum f f) (\f. map_sum f f)" + by(auto simp add: rel_fun_def elim: ignore_Inl.cases) + +lemma ignore_Inl_pos_distr: + "A OO B \ bot \ ignore_Inl OO rel_sum A A OO ignore_Inl OO rel_sum B B OO ignore_Inl \ + ignore_Inl OO rel_sum (A OO B) (A OO B) OO ignore_Inl" + by(fastforce elim!: ignore_Inl.cases simp add: relcompp_apply fun_eq_iff intro: exI[where x="Inl _"]) + +lemma ignore_Inl_Inter: + "\ S \ {}; \S \ {} \ \ (\A\S. {(x, y). ignore_Inl x y} `` {x. Basic_BNFs.setl x \ Basic_BNFs.setr x \ A}) \ {(x, y). ignore_Inl x y} `` (\A\S. {x. Basic_BNFs.setl x \ Basic_BNFs.setr x \ A})" + apply(clarsimp; safe; clarsimp) + subgoal for x A x' + apply(cases x) + apply(drule bspec[where x="Inl x'"]) + apply clarsimp + apply simp + apply clarsimp + apply(drule bspec[where x="Inr _"]) + apply simp + apply simp + done + done + +lift_bnf 'a opt [wits: "(Inl undefined :: 'a + 'a)"] + apply(auto simp add: rel_fun_def elim: ignore_Inl.cases)[] + apply(fastforce simp add: rel_sum.simps) + subgoal for Ss + using ignore_Inl_Inter[unfolded Plus_def, of Ss] + by blast + apply (auto simp: Ball_def image_iff sum_set_defs elim: ignore_Inl.cases split: sum.splits) [] + done + end diff --git a/src/HOL/Library/Finite_Map.thy b/src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy +++ b/src/HOL/Library/Finite_Map.thy @@ -1,1479 +1,1462 @@ (* Title: HOL/Library/Finite_Map.thy Author: Lars Hupel, TU München *) section \Type of finite maps defined as a subtype of maps\ theory Finite_Map imports FSet AList Conditional_Parametricity abbrevs "(=" = "\\<^sub>f" begin subsection \Auxiliary constants and lemmas over \<^type>\map\\ parametric_constant map_add_transfer[transfer_rule]: map_add_def parametric_constant map_of_transfer[transfer_rule]: map_of_def context includes lifting_syntax begin abbreviation rel_map :: "('b \ 'c \ bool) \ ('a \ 'b) \ ('a \ 'c) \ bool" where "rel_map f \ (=) ===> rel_option f" lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran" proof fix m n assume "rel_map A m n" show "rel_set A (ran m) (ran n)" proof (rule rel_setI) fix x assume "x \ ran m" then obtain a where "m a = Some x" unfolding ran_def by auto have "rel_option A (m a) (n a)" using \rel_map A m n\ by (auto dest: rel_funD) then obtain y where "n a = Some y" "A x y" unfolding \m a = _\ by cases auto then show "\y \ ran n. A x y" unfolding ran_def by blast next fix y assume "y \ ran n" then obtain a where "n a = Some y" unfolding ran_def by auto have "rel_option A (m a) (n a)" using \rel_map A m n\ by (auto dest: rel_funD) then obtain x where "m a = Some x" "A x y" unfolding \n a = _\ by cases auto then show "\x \ ran m. A x y" unfolding ran_def by blast qed qed lemma ran_alt_def: "ran m = (the \ m) ` dom m" unfolding ran_def dom_def by force parametric_constant dom_transfer[transfer_rule]: dom_def definition map_upd :: "'a \ 'b \ ('a \ 'b) \ ('a \ 'b)" where "map_upd k v m = m(k \ v)" parametric_constant map_upd_transfer[transfer_rule]: map_upd_def definition map_filter :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'b)" where "map_filter P m = (\x. if P x then m x else None)" parametric_constant map_filter_transfer[transfer_rule]: map_filter_def lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \ m. P k]" proof fix x show "map_filter P (map_of m) x = map_of [(k, _) \ m. P k] x" by (induct m) (auto simp: map_filter_def) qed lemma map_filter_finite[intro]: assumes "finite (dom m)" shows "finite (dom (map_filter P m))" proof - have "dom (map_filter P m) = Set.filter P (dom m)" unfolding map_filter_def Set.filter_def dom_def by auto then show ?thesis using assms by (simp add: Set.filter_def) qed definition map_drop :: "'a \ ('a \ 'b) \ ('a \ 'b)" where "map_drop a = map_filter (\a'. a' \ a)" parametric_constant map_drop_transfer[transfer_rule]: map_drop_def definition map_drop_set :: "'a set \ ('a \ 'b) \ ('a \ 'b)" where "map_drop_set A = map_filter (\a. a \ A)" parametric_constant map_drop_set_transfer[transfer_rule]: map_drop_set_def definition map_restrict_set :: "'a set \ ('a \ 'b) \ ('a \ 'b)" where "map_restrict_set A = map_filter (\a. a \ A)" parametric_constant map_restrict_set_transfer[transfer_rule]: map_restrict_set_def definition map_pred :: "('a \ 'b \ bool) \ ('a \ 'b) \ bool" where "map_pred P m \ (\x. case m x of None \ True | Some y \ P x y)" parametric_constant map_pred_transfer[transfer_rule]: map_pred_def definition rel_map_on_set :: "'a set \ ('b \ 'c \ bool) \ ('a \ 'b) \ ('a \ 'c) \ bool" where "rel_map_on_set S P = eq_onp (\x. x \ S) ===> rel_option P" definition set_of_map :: "('a \ 'b) \ ('a \ 'b) set" where "set_of_map m = {(k, v)|k v. m k = Some v}" lemma set_of_map_alt_def: "set_of_map m = (\k. (k, the (m k))) ` dom m" unfolding set_of_map_def dom_def by auto lemma set_of_map_finite: "finite (dom m) \ finite (set_of_map m)" unfolding set_of_map_alt_def by auto lemma set_of_map_inj: "inj set_of_map" proof fix x y assume "set_of_map x = set_of_map y" hence "(x a = Some b) = (y a = Some b)" for a b unfolding set_of_map_def by auto hence "x k = y k" for k by (metis not_None_eq) thus "x = y" .. qed lemma dom_comp: "dom (m \\<^sub>m n) \ dom n" unfolding map_comp_def dom_def by (auto split: option.splits) lemma dom_comp_finite: "finite (dom n) \ finite (dom (map_comp m n))" by (metis finite_subset dom_comp) parametric_constant map_comp_transfer[transfer_rule]: map_comp_def end subsection \Abstract characterisation\ typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \ 'b) set" morphisms fmlookup Abs_fmap proof show "Map.empty \ {m. finite (dom m)}" by auto qed setup_lifting type_definition_fmap lemma dom_fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))" using fmap.fmlookup by auto lemma fmap_ext: assumes "\x. fmlookup m x = fmlookup n x" shows "m = n" using assms by transfer' auto subsection \Operations\ context includes fset.lifting begin lift_definition fmran :: "('a, 'b) fmap \ 'b fset" is ran parametric ran_transfer by (rule finite_ran) lemma fmlookup_ran_iff: "y |\| fmran m \ (\x. fmlookup m x = Some y)" by transfer' (auto simp: ran_def) lemma fmranI: "fmlookup m x = Some y \ y |\| fmran m" by (auto simp: fmlookup_ran_iff) lemma fmranE[elim]: assumes "y |\| fmran m" obtains x where "fmlookup m x = Some y" using assms by (auto simp: fmlookup_ran_iff) lift_definition fmdom :: "('a, 'b) fmap \ 'a fset" is dom parametric dom_transfer . lemma fmlookup_dom_iff: "x |\| fmdom m \ (\a. fmlookup m x = Some a)" by transfer' auto lemma fmdom_notI: "fmlookup m x = None \ x |\| fmdom m" by (simp add: fmlookup_dom_iff) lemma fmdomI: "fmlookup m x = Some y \ x |\| fmdom m" by (simp add: fmlookup_dom_iff) lemma fmdom_notD[dest]: "x |\| fmdom m \ fmlookup m x = None" by (simp add: fmlookup_dom_iff) lemma fmdomE[elim]: assumes "x |\| fmdom m" obtains y where "fmlookup m x = Some y" using assms by (auto simp: fmlookup_dom_iff) lift_definition fmdom' :: "('a, 'b) fmap \ 'a set" is dom parametric dom_transfer . lemma fmlookup_dom'_iff: "x \ fmdom' m \ (\a. fmlookup m x = Some a)" by transfer' auto lemma fmdom'_notI: "fmlookup m x = None \ x \ fmdom' m" by (simp add: fmlookup_dom'_iff) lemma fmdom'I: "fmlookup m x = Some y \ x \ fmdom' m" by (simp add: fmlookup_dom'_iff) lemma fmdom'_notD[dest]: "x \ fmdom' m \ fmlookup m x = None" by (simp add: fmlookup_dom'_iff) lemma fmdom'E[elim]: assumes "x \ fmdom' m" obtains x y where "fmlookup m x = Some y" using assms by (auto simp: fmlookup_dom'_iff) lemma fmdom'_alt_def: "fmdom' m = fset (fmdom m)" by transfer' force lemma finite_fmdom'[simp]: "finite (fmdom' m)" unfolding fmdom'_alt_def by simp lemma dom_fmlookup[simp]: "dom (fmlookup m) = fmdom' m" by transfer' simp lift_definition fmempty :: "('a, 'b) fmap" is Map.empty by simp lemma fmempty_lookup[simp]: "fmlookup fmempty x = None" by transfer' simp lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp lemma fmran_empty[simp]: "fmran fmempty = fempty" by transfer' (auto simp: ran_def map_filter_def) lift_definition fmupd :: "'a \ 'b \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_upd parametric map_upd_transfer unfolding map_upd_def[abs_def] by simp lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')" by transfer' (auto simp: map_upd_def) lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def) lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def) lemma fmupd_reorder_neq: assumes "a \ b" shows "fmupd a x (fmupd b y m) = fmupd b y (fmupd a x m)" using assms by transfer' (auto simp: map_upd_def) lemma fmupd_idem[simp]: "fmupd a x (fmupd a y m) = fmupd a x m" by transfer' (auto simp: map_upd_def) lift_definition fmfilter :: "('a \ bool) \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_filter parametric map_filter_transfer by auto lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)" by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)" by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)" by transfer' (auto simp: map_filter_def) lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty" by transfer' (auto simp: map_filter_def) lemma fmfilter_true[simp]: assumes "\x y. fmlookup m x = Some y \ P x" shows "fmfilter P m = m" proof (rule fmap_ext) fix x have "fmlookup m x = None" if "\ P x" using that assms by fastforce then show "fmlookup (fmfilter P m) x = fmlookup m x" by simp qed lemma fmfilter_false[simp]: assumes "\x y. fmlookup m x = Some y \ \ P x" shows "fmfilter P m = fmempty" using assms by transfer' (fastforce simp: map_filter_def) lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\x. P x \ Q x) m" by transfer' (auto simp: map_filter_def) lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)" unfolding fmfilter_comp by meson lemma fmfilter_cong[cong]: assumes "\x y. fmlookup m x = Some y \ P x = Q x" shows "fmfilter P m = fmfilter Q m" proof (rule fmap_ext) fix x have "fmlookup m x = None" if "P x \ Q x" using that assms by fastforce then show "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x" by auto qed lemma fmfilter_cong'[fundef_cong]: assumes "m = n" "\x. x \ fmdom' m \ P x = Q x" shows "fmfilter P m = fmfilter Q n" using assms(2) unfolding assms(1) by (rule fmfilter_cong) (metis fmdom'I) lemma fmfilter_upd[simp]: "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)" by transfer' (auto simp: map_upd_def map_filter_def) lift_definition fmdrop :: "'a \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_drop parametric map_drop_transfer unfolding map_drop_def by auto lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None" by transfer' (auto simp: map_drop_def map_filter_def) lift_definition fmdrop_set :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_drop_set parametric map_drop_set_transfer unfolding map_drop_set_def by auto lift_definition fmdrop_fset :: "'a fset \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_drop_set parametric map_drop_set_transfer unfolding map_drop_set_def by auto lift_definition fmrestrict_set :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_restrict_set parametric map_restrict_set_transfer unfolding map_restrict_set_def by auto lift_definition fmrestrict_fset :: "'a fset \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_restrict_set parametric map_restrict_set_transfer unfolding map_restrict_set_def by auto lemma fmfilter_alt_defs: "fmdrop a = fmfilter (\a'. a' \ a)" "fmdrop_set A = fmfilter (\a. a \ A)" "fmdrop_fset B = fmfilter (\a. a |\| B)" "fmrestrict_set A = fmfilter (\a. a \ A)" "fmrestrict_fset B = fmfilter (\a. a |\| B)" by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+ lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \ A" unfolding fmfilter_alt_defs by auto lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\| A" unfolding fmfilter_alt_defs by auto lemma fmdrop_fmupd: "fmdrop x (fmupd y z m) = (if x = y then fmdrop x m else fmupd y z (fmdrop x m))" by transfer' (auto simp: map_drop_def map_filter_def map_upd_def) lemma fmdrop_idle: "x |\| fmdom B \ fmdrop x B = B" by transfer' (auto simp: map_drop_def map_filter_def) lemma fmdrop_idle': "x \ fmdom' B \ fmdrop x B = B" by transfer' (auto simp: map_drop_def map_filter_def) lemma fmdrop_fmupd_same: "fmdrop x (fmupd x y m) = fmdrop x m" by transfer' (auto simp: map_drop_def map_filter_def map_upd_def) lemma fmdom'_restrict_set_precise: "fmdom' (fmrestrict_set A m) = fmdom' m \ A" unfolding fmfilter_alt_defs by auto lemma fmdom'_restrict_fset_precise: "fmdom (fmrestrict_fset A m) = fmdom m |\| A" unfolding fmfilter_alt_defs by auto lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A" unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits) lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \ fset A" unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def) lemma fmlookup_drop[simp]: "fmlookup (fmdrop a m) x = (if x \ a then fmlookup m x else None)" unfolding fmfilter_alt_defs by simp lemma fmlookup_drop_set[simp]: "fmlookup (fmdrop_set A m) x = (if x \ A then fmlookup m x else None)" unfolding fmfilter_alt_defs by simp lemma fmlookup_drop_fset[simp]: "fmlookup (fmdrop_fset A m) x = (if x |\| A then fmlookup m x else None)" unfolding fmfilter_alt_defs by simp lemma fmlookup_restrict_set[simp]: "fmlookup (fmrestrict_set A m) x = (if x \ A then fmlookup m x else None)" unfolding fmfilter_alt_defs by simp lemma fmlookup_restrict_fset[simp]: "fmlookup (fmrestrict_fset A m) x = (if x |\| A then fmlookup m x else None)" unfolding fmfilter_alt_defs by simp lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m" by (rule fmap_ext) auto lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m" by (rule fmap_ext) auto lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty" unfolding fmfilter_alt_defs by simp lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty" unfolding fmfilter_alt_defs by simp lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty" unfolding fmfilter_alt_defs by simp lemma fmdrop_fset_fmdom[simp]: "fmdrop_fset (fmdom A) A = fmempty" by transfer' (auto simp: map_drop_set_def map_filter_def) lemma fmdrop_set_fmdom[simp]: "fmdrop_set (fmdom' A) A = fmempty" by transfer' (auto simp: map_drop_set_def map_filter_def) lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty" unfolding fmfilter_alt_defs by simp lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty" unfolding fmfilter_alt_defs by simp lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m" by (rule fmap_ext) auto lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m" by (rule fmap_ext) auto lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m" unfolding fmfilter_alt_defs by simp lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m" unfolding fmfilter_alt_defs by simp lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty" unfolding fmfilter_alt_defs by simp lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty" unfolding fmfilter_alt_defs by simp lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)" unfolding fmfilter_alt_defs by (rule fmfilter_comm) lemma fmdrop_set_insert[simp]: "fmdrop_set (insert x S) m = fmdrop x (fmdrop_set S m)" by (rule fmap_ext) auto lemma fmdrop_fset_insert[simp]: "fmdrop_fset (finsert x S) m = fmdrop x (fmdrop_fset S m)" by (rule fmap_ext) auto lemma fmrestrict_set_twice[simp]: "fmrestrict_set S (fmrestrict_set T m) = fmrestrict_set (S \ T) m" unfolding fmfilter_alt_defs by auto lemma fmrestrict_fset_twice[simp]: "fmrestrict_fset S (fmrestrict_fset T m) = fmrestrict_fset (S |\| T) m" unfolding fmfilter_alt_defs by auto lemma fmrestrict_set_drop[simp]: "fmrestrict_set S (fmdrop b m) = fmrestrict_set (S - {b}) m" unfolding fmfilter_alt_defs by auto lemma fmrestrict_fset_drop[simp]: "fmrestrict_fset S (fmdrop b m) = fmrestrict_fset (S - {| b |}) m" unfolding fmfilter_alt_defs by auto lemma fmdrop_fmrestrict_set[simp]: "fmdrop b (fmrestrict_set S m) = fmrestrict_set (S - {b}) m" by (rule fmap_ext) auto lemma fmdrop_fmrestrict_fset[simp]: "fmdrop b (fmrestrict_fset S m) = fmrestrict_fset (S - {| b |}) m" by (rule fmap_ext) auto lemma fmdrop_idem[simp]: "fmdrop a (fmdrop a m) = fmdrop a m" unfolding fmfilter_alt_defs by auto lemma fmdrop_set_twice[simp]: "fmdrop_set S (fmdrop_set T m) = fmdrop_set (S \ T) m" unfolding fmfilter_alt_defs by auto lemma fmdrop_fset_twice[simp]: "fmdrop_fset S (fmdrop_fset T m) = fmdrop_fset (S |\| T) m" unfolding fmfilter_alt_defs by auto lemma fmdrop_set_fmdrop[simp]: "fmdrop_set S (fmdrop b m) = fmdrop_set (insert b S) m" by (rule fmap_ext) auto lemma fmdrop_fset_fmdrop[simp]: "fmdrop_fset S (fmdrop b m) = fmdrop_fset (finsert b S) m" by (rule fmap_ext) auto lift_definition fmadd :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl "++\<^sub>f" 100) is map_add parametric map_add_transfer by simp lemma fmlookup_add[simp]: "fmlookup (m ++\<^sub>f n) x = (if x |\| fmdom n then fmlookup n x else fmlookup m x)" by transfer' (auto simp: map_add_def split: option.splits) lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\| fmdom n" by transfer' auto lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \ fmdom' n" by transfer' auto lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n" by (rule fmap_ext) auto lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n" by (rule fmap_ext) auto lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n" by transfer' (auto simp: map_filter_def map_add_def) lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n" unfolding fmfilter_alt_defs by simp lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n" unfolding fmfilter_alt_defs by simp lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n" unfolding fmfilter_alt_defs by simp lemma fmrestrict_set_add_distrib[simp]: "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n" unfolding fmfilter_alt_defs by simp lemma fmrestrict_fset_add_distrib[simp]: "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n" unfolding fmfilter_alt_defs by simp lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m" by (transfer'; auto)+ lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m" by transfer' (auto simp: map_add_def split: option.splits) lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p" by transfer' simp lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)" by (rule fmap_ext) simp lift_definition fmpred :: "('a \ 'b \ bool) \ ('a, 'b) fmap \ bool" is map_pred parametric map_pred_transfer . lemma fmpredI[intro]: assumes "\x y. fmlookup m x = Some y \ P x y" shows "fmpred P m" using assms by transfer' (auto simp: map_pred_def split: option.splits) lemma fmpredD[dest]: "fmpred P m \ fmlookup m x = Some y \ P x y" by transfer' (auto simp: map_pred_def split: option.split_asm) lemma fmpred_iff: "fmpred P m \ (\x y. fmlookup m x = Some y \ P x y)" by auto lemma fmpred_alt_def: "fmpred P m \ fBall (fmdom m) (\x. P x (the (fmlookup m x)))" unfolding fmpred_iff apply auto apply (rename_tac x y) apply (erule_tac x = x in fBallE) apply simp by (simp add: fmlookup_dom_iff) lemma fmpred_mono_strong: assumes "\x y. fmlookup m x = Some y \ P x y \ Q x y" shows "fmpred P m \ fmpred Q m" using assms unfolding fmpred_iff by auto lemma fmpred_mono[mono]: "P \ Q \ fmpred P \ fmpred Q" apply rule apply (rule fmpred_mono_strong[where P = P and Q = Q]) apply auto done lemma fmpred_empty[intro!, simp]: "fmpred P fmempty" by auto lemma fmpred_upd[intro]: "fmpred P m \ P x y \ fmpred P (fmupd x y m)" by transfer' (auto simp: map_pred_def map_upd_def) lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \ P x y" by auto lemma fmpred_add[intro]: "fmpred P m \ fmpred P n \ fmpred P (m ++\<^sub>f n)" by transfer' (auto simp: map_pred_def map_add_def split: option.splits) lemma fmpred_filter[intro]: "fmpred P m \ fmpred P (fmfilter Q m)" by transfer' (auto simp: map_pred_def map_filter_def) lemma fmpred_drop[intro]: "fmpred P m \ fmpred P (fmdrop a m)" by (auto simp: fmfilter_alt_defs) lemma fmpred_drop_set[intro]: "fmpred P m \ fmpred P (fmdrop_set A m)" by (auto simp: fmfilter_alt_defs) lemma fmpred_drop_fset[intro]: "fmpred P m \ fmpred P (fmdrop_fset A m)" by (auto simp: fmfilter_alt_defs) lemma fmpred_restrict_set[intro]: "fmpred P m \ fmpred P (fmrestrict_set A m)" by (auto simp: fmfilter_alt_defs) lemma fmpred_restrict_fset[intro]: "fmpred P m \ fmpred P (fmrestrict_fset A m)" by (auto simp: fmfilter_alt_defs) lemma fmpred_cases[consumes 1]: assumes "fmpred P m" obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y" using assms by auto lift_definition fmsubset :: "('a, 'b) fmap \ ('a, 'b) fmap \ bool" (infix "\\<^sub>f" 50) is map_le . lemma fmsubset_alt_def: "m \\<^sub>f n \ fmpred (\k v. fmlookup n k = Some v) m" by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits) lemma fmsubset_pred: "fmpred P m \ n \\<^sub>f m \ fmpred P n" unfolding fmsubset_alt_def fmpred_iff by auto lemma fmsubset_filter_mono: "m \\<^sub>f n \ fmfilter P m \\<^sub>f fmfilter P n" unfolding fmsubset_alt_def fmpred_iff by auto lemma fmsubset_drop_mono: "m \\<^sub>f n \ fmdrop a m \\<^sub>f fmdrop a n" unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) lemma fmsubset_drop_set_mono: "m \\<^sub>f n \ fmdrop_set A m \\<^sub>f fmdrop_set A n" unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) lemma fmsubset_drop_fset_mono: "m \\<^sub>f n \ fmdrop_fset A m \\<^sub>f fmdrop_fset A n" unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) lemma fmsubset_restrict_set_mono: "m \\<^sub>f n \ fmrestrict_set A m \\<^sub>f fmrestrict_set A n" unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) lemma fmsubset_restrict_fset_mono: "m \\<^sub>f n \ fmrestrict_fset A m \\<^sub>f fmrestrict_fset A n" unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) lemma fmfilter_subset[simp]: "fmfilter P m \\<^sub>f m" unfolding fmsubset_alt_def fmpred_iff by auto lemma fmsubset_drop[simp]: "fmdrop a m \\<^sub>f m" unfolding fmfilter_alt_defs by (rule fmfilter_subset) lemma fmsubset_drop_set[simp]: "fmdrop_set S m \\<^sub>f m" unfolding fmfilter_alt_defs by (rule fmfilter_subset) lemma fmsubset_drop_fset[simp]: "fmdrop_fset S m \\<^sub>f m" unfolding fmfilter_alt_defs by (rule fmfilter_subset) lemma fmsubset_restrict_set[simp]: "fmrestrict_set S m \\<^sub>f m" unfolding fmfilter_alt_defs by (rule fmfilter_subset) lemma fmsubset_restrict_fset[simp]: "fmrestrict_fset S m \\<^sub>f m" unfolding fmfilter_alt_defs by (rule fmfilter_subset) lift_definition fset_of_fmap :: "('a, 'b) fmap \ ('a \ 'b) fset" is set_of_map by (rule set_of_map_finite) lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap" apply rule apply transfer' using set_of_map_inj unfolding inj_def by auto lemma fset_of_fmap_iff[simp]: "(a, b) |\| fset_of_fmap m \ fmlookup m a = Some b" by transfer' (auto simp: set_of_map_def) lemma fset_of_fmap_iff'[simp]: "(a, b) \ fset (fset_of_fmap m) \ fmlookup m a = Some b" by transfer' (auto simp: set_of_map_def) lift_definition fmap_of_list :: "('a \ 'b) list \ ('a, 'b) fmap" is map_of parametric map_of_transfer by (rule finite_dom_map_of) lemma fmap_of_list_simps[simp]: "fmap_of_list [] = fmempty" "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)" by (transfer, simp add: map_upd_def)+ lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs" by transfer' simp lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]" by transfer' (auto simp: map_upd_def) lemma fmpred_of_list[intro]: assumes "\k v. (k, v) \ set xs \ P k v" shows "fmpred P (fmap_of_list xs)" using assms by (induction xs) (transfer'; auto simp: map_pred_def)+ lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \ (k, v) \ set xs" by transfer' (auto dest: map_of_SomeD) lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)" apply transfer' apply (subst dom_map_of_conv_image_fst) apply auto done lift_definition fmrel_on_fset :: "'a fset \ ('b \ 'c \ bool) \ ('a, 'b) fmap \ ('a, 'c) fmap \ bool" is rel_map_on_set . lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \ fBall S (\x. rel_option P (fmlookup m x) (fmlookup n x))" by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def) lemma fmrel_on_fsetI[intro]: assumes "\x. x |\| S \ rel_option P (fmlookup m x) (fmlookup n x)" shows "fmrel_on_fset S P m n" using assms unfolding fmrel_on_fset_alt_def by auto lemma fmrel_on_fset_mono[mono]: "R \ Q \ fmrel_on_fset S R \ fmrel_on_fset S Q" unfolding fmrel_on_fset_alt_def[abs_def] apply (intro le_funI fBall_mono) using option.rel_mono by auto lemma fmrel_on_fsetD: "x |\| S \ fmrel_on_fset S P m n \ rel_option P (fmlookup m x) (fmlookup n x)" unfolding fmrel_on_fset_alt_def by auto lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \ T |\| S \ fmrel_on_fset T R m n" unfolding fmrel_on_fset_alt_def by auto lemma fmrel_on_fset_unionI: "fmrel_on_fset A R m n \ fmrel_on_fset B R m n \ fmrel_on_fset (A |\| B) R m n" unfolding fmrel_on_fset_alt_def by auto lemma fmrel_on_fset_updateI: assumes "fmrel_on_fset S P m n" "P v\<^sub>1 v\<^sub>2" shows "fmrel_on_fset (finsert k S) P (fmupd k v\<^sub>1 m) (fmupd k v\<^sub>2 n)" using assms unfolding fmrel_on_fset_alt_def by auto lift_definition fmimage :: "('a, 'b) fmap \ 'a fset \ 'b fset" is "\m S. {b|a b. m a = Some b \ a \ S}" subgoal for m S apply (rule finite_subset[where B = "ran m"]) apply (auto simp: ran_def)[] by (rule finite_ran) done lemma fmimage_alt_def: "fmimage m S = fmran (fmrestrict_fset S m)" by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def) lemma fmimage_empty[simp]: "fmimage m fempty = fempty" by transfer' auto lemma fmimage_subset_ran[simp]: "fmimage m S |\| fmran m" by transfer' (auto simp: ran_def) lemma fmimage_dom[simp]: "fmimage m (fmdom m) = fmran m" by transfer' (auto simp: ran_def) lemma fmimage_inter: "fmimage m (A |\| B) |\| fmimage m A |\| fmimage m B" by transfer' auto lemma fimage_inter_dom[simp]: "fmimage m (fmdom m |\| A) = fmimage m A" "fmimage m (A |\| fmdom m) = fmimage m A" by (transfer'; auto)+ lemma fmimage_union[simp]: "fmimage m (A |\| B) = fmimage m A |\| fmimage m B" by transfer' auto lemma fmimage_Union[simp]: "fmimage m (ffUnion A) = ffUnion (fmimage m |`| A)" by transfer' auto lemma fmimage_filter[simp]: "fmimage (fmfilter P m) A = fmimage m (ffilter P A)" by transfer' (auto simp: map_filter_def) lemma fmimage_drop[simp]: "fmimage (fmdrop a m) A = fmimage m (A - {|a|})" by transfer' (auto simp: map_filter_def map_drop_def) lemma fmimage_drop_fset[simp]: "fmimage (fmdrop_fset B m) A = fmimage m (A - B)" by transfer' (auto simp: map_filter_def map_drop_set_def) lemma fmimage_restrict_fset[simp]: "fmimage (fmrestrict_fset B m) A = fmimage m (A |\| B)" by transfer' (auto simp: map_filter_def map_restrict_set_def) lemma fmfilter_ran[simp]: "fmran (fmfilter P m) = fmimage m (ffilter P (fmdom m))" by transfer' (auto simp: ran_def map_filter_def) lemma fmran_drop[simp]: "fmran (fmdrop a m) = fmimage m (fmdom m - {|a|})" by transfer' (auto simp: ran_def map_drop_def map_filter_def) lemma fmran_drop_fset[simp]: "fmran (fmdrop_fset A m) = fmimage m (fmdom m - A)" by transfer' (auto simp: ran_def map_drop_set_def map_filter_def) lemma fmran_restrict_fset: "fmran (fmrestrict_fset A m) = fmimage m (fmdom m |\| A)" by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def) lemma fmlookup_image_iff: "y |\| fmimage m A \ (\x. fmlookup m x = Some y \ x |\| A)" by transfer' (auto simp: ran_def) lemma fmimageI: "fmlookup m x = Some y \ x |\| A \ y |\| fmimage m A" by (auto simp: fmlookup_image_iff) lemma fmimageE[elim]: assumes "y |\| fmimage m A" obtains x where "fmlookup m x = Some y" "x |\| A" using assms by (auto simp: fmlookup_image_iff) lift_definition fmcomp :: "('b, 'c) fmap \ ('a, 'b) fmap \ ('a, 'c) fmap" (infixl "\\<^sub>f" 55) is map_comp parametric map_comp_transfer by (rule dom_comp_finite) lemma fmlookup_comp[simp]: "fmlookup (m \\<^sub>f n) x = Option.bind (fmlookup n x) (fmlookup m)" by transfer' (auto simp: map_comp_def split: option.splits) end subsection \BNF setup\ lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty] for map: fmmap rel: fmrel by auto declare fmap.pred_mono[mono] -context includes lifting_syntax begin - -lemma fmmap_transfer[transfer_rule]: - "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=)) (\f. (\) (map_option f)) fmmap" - unfolding fmmap_def - by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def) - -lemma fmran'_transfer[transfer_rule]: - "(pcr_fmap (=) (=) ===> (=)) (\x. \(set_option ` (range x))) fmran'" - unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce - -lemma fmrel_transfer[transfer_rule]: - "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=) ===> (=)) rel_map fmrel" - unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce - -end - lemma fmran'_alt_def: "fmran' m = fset (fmran m)" including fset.lifting by transfer' (auto simp: ran_def fun_eq_iff) lemma fmlookup_ran'_iff: "y \ fmran' m \ (\x. fmlookup m x = Some y)" by transfer' (auto simp: ran_def) lemma fmran'I: "fmlookup m x = Some y \ y \ fmran' m" by (auto simp: fmlookup_ran'_iff) lemma fmran'E[elim]: assumes "y \ fmran' m" obtains x where "fmlookup m x = Some y" using assms by (auto simp: fmlookup_ran'_iff) lemma fmrel_iff: "fmrel R m n \ (\x. rel_option R (fmlookup m x) (fmlookup n x))" by transfer' (auto simp: rel_fun_def) lemma fmrelI[intro]: assumes "\x. rel_option R (fmlookup m x) (fmlookup n x)" shows "fmrel R m n" using assms by transfer' auto lemma fmrel_upd[intro]: "fmrel P m n \ P x y \ fmrel P (fmupd k x m) (fmupd k y n)" by transfer' (auto simp: map_upd_def rel_fun_def) lemma fmrelD[dest]: "fmrel P m n \ rel_option P (fmlookup m x) (fmlookup n x)" by transfer' (auto simp: rel_fun_def) lemma fmrel_addI[intro]: assumes "fmrel P m n" "fmrel P a b" shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)" using assms apply transfer' apply (auto simp: rel_fun_def map_add_def) by (metis option.case_eq_if option.collapse option.rel_sel) lemma fmrel_cases[consumes 1]: assumes "fmrel P m n" obtains (none) "fmlookup m x = None" "fmlookup n x = None" | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b" proof - from assms have "rel_option P (fmlookup m x) (fmlookup n x)" by auto then show thesis using none some by (cases rule: option.rel_cases) auto qed lemma fmrel_filter[intro]: "fmrel P m n \ fmrel P (fmfilter Q m) (fmfilter Q n)" unfolding fmrel_iff by auto lemma fmrel_drop[intro]: "fmrel P m n \ fmrel P (fmdrop a m) (fmdrop a n)" unfolding fmfilter_alt_defs by blast lemma fmrel_drop_set[intro]: "fmrel P m n \ fmrel P (fmdrop_set A m) (fmdrop_set A n)" unfolding fmfilter_alt_defs by blast lemma fmrel_drop_fset[intro]: "fmrel P m n \ fmrel P (fmdrop_fset A m) (fmdrop_fset A n)" unfolding fmfilter_alt_defs by blast lemma fmrel_restrict_set[intro]: "fmrel P m n \ fmrel P (fmrestrict_set A m) (fmrestrict_set A n)" unfolding fmfilter_alt_defs by blast lemma fmrel_restrict_fset[intro]: "fmrel P m n \ fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)" unfolding fmfilter_alt_defs by blast lemma fmrel_on_fset_fmrel_restrict: "fmrel_on_fset S P m n \ fmrel P (fmrestrict_fset S m) (fmrestrict_fset S n)" unfolding fmrel_on_fset_alt_def fmrel_iff by auto lemma fmrel_on_fset_refl_strong: assumes "\x y. x |\| S \ fmlookup m x = Some y \ P y y" shows "fmrel_on_fset S P m m" unfolding fmrel_on_fset_fmrel_restrict fmrel_iff using assms by (simp add: option.rel_sel) lemma fmrel_on_fset_addI: assumes "fmrel_on_fset S P m n" "fmrel_on_fset S P a b" shows "fmrel_on_fset S P (m ++\<^sub>f a) (n ++\<^sub>f b)" using assms unfolding fmrel_on_fset_fmrel_restrict by auto lemma fmrel_fmdom_eq: assumes "fmrel P x y" shows "fmdom x = fmdom y" proof - have "a |\| fmdom x \ a |\| fmdom y" for a proof - have "rel_option P (fmlookup x a) (fmlookup y a)" using assms by (simp add: fmrel_iff) thus ?thesis by cases (auto intro: fmdomI) qed thus ?thesis by auto qed lemma fmrel_fmdom'_eq: "fmrel P x y \ fmdom' x = fmdom' y" unfolding fmdom'_alt_def by (metis fmrel_fmdom_eq) lemma fmrel_rel_fmran: assumes "fmrel P x y" shows "rel_fset P (fmran x) (fmran y)" proof - { fix b assume "b |\| fmran x" then obtain a where "fmlookup x a = Some b" by auto moreover have "rel_option P (fmlookup x a) (fmlookup y a)" using assms by auto ultimately have "\b'. b' |\| fmran y \ P b b'" by (metis option_rel_Some1 fmranI) } moreover { fix b assume "b |\| fmran y" then obtain a where "fmlookup y a = Some b" by auto moreover have "rel_option P (fmlookup x a) (fmlookup y a)" using assms by auto ultimately have "\b'. b' |\| fmran x \ P b' b" by (metis option_rel_Some2 fmranI) } ultimately show ?thesis unfolding rel_fset_alt_def by auto qed lemma fmrel_rel_fmran': "fmrel P x y \ rel_set P (fmran' x) (fmran' y)" unfolding fmran'_alt_def by (metis fmrel_rel_fmran rel_fset_fset) lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\_. P)" unfolding fmap.pred_set fmran'_alt_def including fset.lifting apply transfer' apply (rule ext) apply (auto simp: map_pred_def ran_def split: option.splits dest: ) done lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \ pred_fmap f m" unfolding fmap.pred_set fmap.set_map by simp lemma pred_fmapD: "pred_fmap P m \ x |\| fmran m \ P x" by auto lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)" by transfer' auto lemma fmpred_map[simp]: "fmpred P (fmmap f m) \ fmpred (\k v. P k (f v)) m" unfolding fmpred_iff pred_fmap_def fmap.set_map by auto lemma fmpred_id[simp]: "fmpred (\_. id) (fmmap f m) \ fmpred (\_. f) m" by simp lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n" by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits) lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty" by transfer auto lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m" including fset.lifting by transfer' simp lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m" by transfer' simp lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m" including fset.lifting by transfer' (auto simp: ran_def) lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m" by transfer' (auto simp: ran_def) lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)" by transfer' (auto simp: map_filter_def) lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp lemma fmmap_subset[intro]: "m \\<^sub>f n \ fmmap f m \\<^sub>f fmmap f n" by transfer' (auto simp: map_le_def) lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\(k, v). (k, f v)) |`| fset_of_fmap m" including fset.lifting by transfer' (auto simp: set_of_map_def) lemma fmmap_fmupd: "fmmap f (fmupd x y m) = fmupd x (f y) (fmmap f m)" by transfer' (auto simp: fun_eq_iff map_upd_def) subsection \\<^const>\size\ setup\ definition size_fmap :: "('a \ nat) \ ('b \ nat) \ ('a, 'b) fmap \ nat" where [simp]: "size_fmap f g m = size_fset (\(a, b). f a + g b) (fset_of_fmap m)" instantiation fmap :: (type, type) size begin definition size_fmap where size_fmap_overloaded_def: "size_fmap = Finite_Map.size_fmap (\_. 0) (\_. 0)" instance .. end lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)" unfolding size_fmap_overloaded_def by simp lemma fmap_size_o_map: "inj h \ size_fmap f g \ fmmap h = size_fmap f (g \ h)" unfolding size_fmap_def apply (auto simp: fun_eq_iff fmmap_fset_of_fmap) apply (subst sum.reindex) subgoal for m using prod.inj_map[unfolded map_prod_def, of "\x. x" h] unfolding inj_on_def by auto subgoal by (rule sum.cong) (auto split: prod.splits) done setup \ BNF_LFP_Size.register_size_global \<^type_name>\fmap\ \<^const_name>\size_fmap\ @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps} @{thms fmap_size_o_map} \ subsection \Additional operations\ lift_definition fmmap_keys :: "('a \ 'b \ 'c) \ ('a, 'b) fmap \ ('a, 'c) fmap" is "\f m a. map_option (f a) (m a)" unfolding dom_def by simp lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\a b. P a (f a b)) m" by transfer' (auto simp: map_pred_def split: option.splits) lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m" including fset.lifting by transfer' auto lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)" by transfer' simp lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)" by transfer' (auto simp: map_filter_def) lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)" unfolding fmfilter_alt_defs by simp lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp lemma fmmap_keys_subset[intro]: "m \\<^sub>f n \ fmmap_keys f m \\<^sub>f fmmap_keys f n" by transfer' (auto simp: map_le_def dom_def) definition sorted_list_of_fmap :: "('a::linorder, 'b) fmap \ ('a \ 'b) list" where "sorted_list_of_fmap m = map (\k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))" lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m" unfolding sorted_list_of_fmap_def curry_def list.pred_map apply (auto simp: list_all_iff) including fset.lifting by (transfer; auto simp: dom_def map_pred_def split: option.splits)+ lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m" unfolding sorted_list_of_fmap_def including fset.lifting by transfer (simp add: map_of_map_keys) subsection \Additional properties\ lemma fmchoice': assumes "finite S" "\x \ S. \y. Q x y" shows "\m. fmdom' m = S \ fmpred Q m" proof - obtain f where f: "Q x (f x)" if "x \ S" for x using assms by (metis bchoice) define f' where "f' x = (if x \ S then Some (f x) else None)" for x have "eq_onp (\m. finite (dom m)) f' f'" unfolding eq_onp_def f'_def dom_def using assms by auto show ?thesis apply (rule exI[where x = "Abs_fmap f'"]) apply (subst fmpred.abs_eq, fact) apply (subst fmdom'.abs_eq, fact) unfolding f'_def dom_def map_pred_def using f by auto qed subsection \Lifting/transfer setup\ context includes lifting_syntax begin lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty" by transfer auto lemma fmadd_transfer[transfer_rule]: "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd" by (intro fmrel_addI rel_funI) lemma fmupd_transfer[transfer_rule]: "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd" by auto end lemma Quotient_fmap_bnf[quot_map]: assumes "Quotient R Abs Rep T" shows "Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T)" unfolding Quotient_alt_def4 proof safe fix m n assume "fmrel T m n" then have "fmlookup (fmmap Abs m) x = fmlookup n x" for x apply (cases rule: fmrel_cases[where x = x]) using assms unfolding Quotient_alt_def by auto then show "fmmap Abs m = n" by (rule fmap_ext) next fix m show "fmrel T (fmmap Rep m) m" unfolding fmap.rel_map apply (rule fmap.rel_refl) using assms unfolding Quotient_alt_def by auto next from assms have "R = T OO T\\" unfolding Quotient_alt_def4 by simp then show "fmrel R = fmrel T OO (fmrel T)\\" by (simp add: fmap.rel_compp fmap.rel_conversep) qed subsection \View as datatype\ lemma fmap_distinct[simp]: "fmempty \ fmupd k v m" "fmupd k v m \ fmempty" by (transfer'; auto simp: map_upd_def fun_eq_iff)+ lifting_update fmap.lifting lemma fmap_exhaust[cases type: fmap]: obtains (fmempty) "m = fmempty" | (fmupd) x y m' where "m = fmupd x y m'" "x |\| fmdom m'" using that including fmap.lifting fset.lifting proof transfer fix m P assume "finite (dom m)" assume empty: P if "m = Map.empty" assume map_upd: P if "finite (dom m')" "m = map_upd x y m'" "x \ dom m'" for x y m' show P proof (cases "m = Map.empty") case True thus ?thesis using empty by simp next case False hence "dom m \ {}" by simp then obtain x where "x \ dom m" by blast let ?m' = "map_drop x m" show ?thesis proof (rule map_upd) show "finite (dom ?m')" using \finite (dom m)\ unfolding map_drop_def by auto next show "m = map_upd x (the (m x)) ?m'" using \x \ dom m\ unfolding map_drop_def map_filter_def map_upd_def by auto next show "x \ dom ?m'" unfolding map_drop_def map_filter_def by auto qed qed qed lemma fmap_induct[case_names fmempty fmupd, induct type: fmap]: assumes "P fmempty" assumes "(\x y m. P m \ fmlookup m x = None \ P (fmupd x y m))" shows "P m" proof (induction "fmdom m" arbitrary: m rule: fset_induct_stronger) case empty hence "m = fmempty" by (metis fmrestrict_fset_dom fmrestrict_fset_null) with assms show ?case by simp next case (insert x S) hence "S = fmdom (fmdrop x m)" by auto with insert have "P (fmdrop x m)" by auto have "x |\| fmdom m" using insert by auto then obtain y where "fmlookup m x = Some y" by auto hence "m = fmupd x y (fmdrop x m)" by (auto intro: fmap_ext) show ?case apply (subst \m = _\) apply (rule assms) apply fact apply simp done qed subsection \Code setup\ instantiation fmap :: (type, equal) equal begin definition "equal_fmap \ fmrel HOL.equal" instance proof fix m n :: "('a, 'b) fmap" have "fmrel (=) m n \ (m = n)" by transfer' (simp add: option.rel_eq rel_fun_eq) then show "equal_class.equal m n \ (m = n)" unfolding equal_fmap_def by (simp add: equal_eq[abs_def]) qed end lemma fBall_alt_def: "fBall S P \ (\x. x |\| S \ P x)" by force lemma fmrel_code: "fmrel R m n \ fBall (fmdom m) (\x. rel_option R (fmlookup m x) (fmlookup n x)) \ fBall (fmdom n) (\x. rel_option R (fmlookup m x) (fmlookup n x))" unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def by (metis option.collapse option.rel_sel) lemmas [code] = fmrel_code fmran'_alt_def fmdom'_alt_def fmfilter_alt_defs pred_fmap_fmpred fmsubset_alt_def fmupd_alt_def fmrel_on_fset_alt_def fmpred_alt_def code_datatype fmap_of_list quickcheck_generator fmap constructors: fmap_of_list context includes fset.lifting begin lemma fmlookup_of_list[code]: "fmlookup (fmap_of_list m) = map_of m" by transfer simp lemma fmempty_of_list[code]: "fmempty = fmap_of_list []" by transfer simp lemma fmran_of_list[code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)" by transfer (auto simp: ran_map_of) lemma fmdom_of_list[code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m" by transfer (auto simp: dom_map_of_conv_image_fst) lemma fmfilter_of_list[code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\(k, _). P k) m)" by transfer' auto lemma fmadd_of_list[code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)" by transfer (simp add: merge_conv') lemma fmmap_of_list[code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)" apply transfer apply (subst map_of_map[symmetric]) apply (auto simp: apsnd_def map_prod_def) done lemma fmmap_keys_of_list[code]: "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\(a, b). (a, f a b)) m)" apply transfer subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff) done lemma fmimage_of_list[code]: "fmimage (fmap_of_list m) A = fset_of_list (map snd (filter (\(k, _). k |\| A) (AList.clearjunk m)))" apply (subst fmimage_alt_def) apply (subst fmfilter_alt_defs) apply (subst fmfilter_of_list) apply (subst fmran_of_list) apply transfer' apply (subst AList.restrict_eq[symmetric]) apply (subst clearjunk_restrict) apply (subst AList.restrict_eq) by auto lemma fmcomp_list[code]: "fmap_of_list m \\<^sub>f fmap_of_list n = fmap_of_list (AList.compose n m)" by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits) end subsection \Instances\ lemma exists_map_of: assumes "finite (dom m)" shows "\xs. map_of xs = m" using assms proof (induction "dom m" arbitrary: m) case empty hence "m = Map.empty" by auto moreover have "map_of [] = Map.empty" by simp ultimately show ?case by blast next case (insert x F) hence "F = dom (map_drop x m)" unfolding map_drop_def map_filter_def dom_def by auto with insert have "\xs'. map_of xs' = map_drop x m" by auto then obtain xs' where "map_of xs' = map_drop x m" .. moreover obtain y where "m x = Some y" using insert unfolding dom_def by blast ultimately have "map_of ((x, y) # xs') = m" using \insert x F = dom m\ unfolding map_drop_def map_filter_def by auto thus ?case .. qed lemma exists_fmap_of_list: "\xs. fmap_of_list xs = m" by transfer (rule exists_map_of) lemma fmap_of_list_surj[simp, intro]: "surj fmap_of_list" proof - have "x \ range fmap_of_list" for x :: "('a, 'b) fmap" unfolding image_iff using exists_fmap_of_list by (metis UNIV_I) thus ?thesis by auto qed instance fmap :: (countable, countable) countable proof obtain to_nat :: "('a \ 'b) list \ nat" where "inj to_nat" by (metis ex_inj) moreover have "inj (inv fmap_of_list)" using fmap_of_list_surj by (rule surj_imp_inj_inv) ultimately have "inj (to_nat \ inv fmap_of_list)" by (rule inj_compose) thus "\to_nat::('a, 'b) fmap \ nat. inj to_nat" by auto qed instance fmap :: (finite, finite) finite proof show "finite (UNIV :: ('a, 'b) fmap set)" by (rule finite_imageD) auto qed lifting_update fmap.lifting lifting_forget fmap.lifting subsection \Tests\ \ \Code generation\ export_code fBall fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset fmupd fmrel_on_fset fmdrop fmdrop_set fmdrop_fset fmrestrict_set fmrestrict_fset fmimage fmlookup fmempty fmfilter fmadd fmmap fmmap_keys fmcomp checking SML Scala Haskell? OCaml? \ \\lifting\ through \<^type>\fmap\\ experiment begin context includes fset.lifting begin lift_definition test1 :: "('a, 'b fset) fmap" is "fmempty :: ('a, 'b set) fmap" by auto lift_definition test2 :: "'a \ 'b \ ('a, 'b fset) fmap" is "\a b. fmupd a {b} fmempty" by auto end end end \ No newline at end of file diff --git a/src/HOL/Lifting.thy b/src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy +++ b/src/HOL/Lifting.thy @@ -1,580 +1,580 @@ (* Title: HOL/Lifting.thy Author: Brian Huffman and Ondrej Kuncar Author: Cezary Kaliszyk and Christian Urban *) section \Lifting package\ theory Lifting imports Equiv_Relations Transfer keywords "parametric" and "print_quot_maps" "print_quotients" :: diag and "lift_definition" :: thy_goal_defn and "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl begin subsection \Function map\ context includes lifting_syntax begin lemma map_fun_id: "(id ---> id) = id" by (simp add: fun_eq_iff) subsection \Quotient Predicate\ definition "Quotient R Abs Rep T \ (\a. Abs (Rep a) = a) \ (\a. R (Rep a) (Rep a)) \ (\r s. R r s \ R r r \ R s s \ Abs r = Abs s) \ T = (\x y. R x x \ Abs x = y)" lemma QuotientI: assumes "\a. Abs (Rep a) = a" and "\a. R (Rep a) (Rep a)" and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" and "T = (\x y. R x x \ Abs x = y)" shows "Quotient R Abs Rep T" using assms unfolding Quotient_def by blast context fixes R Abs Rep T assumes a: "Quotient R Abs Rep T" begin lemma Quotient_abs_rep: "Abs (Rep a) = a" using a unfolding Quotient_def by simp lemma Quotient_rep_reflp: "R (Rep a) (Rep a)" using a unfolding Quotient_def by blast lemma Quotient_rel: "R r r \ R s s \ Abs r = Abs s \ R r s" \ \orientation does not loop on rewriting\ using a unfolding Quotient_def by blast lemma Quotient_cr_rel: "T = (\x y. R x x \ Abs x = y)" using a unfolding Quotient_def by blast lemma Quotient_refl1: "R r s \ R r r" using a unfolding Quotient_def by fast lemma Quotient_refl2: "R r s \ R s s" using a unfolding Quotient_def by fast lemma Quotient_rel_rep: "R (Rep a) (Rep b) \ a = b" using a unfolding Quotient_def by metis lemma Quotient_rep_abs: "R r r \ R (Rep (Abs r)) r" using a unfolding Quotient_def by blast lemma Quotient_rep_abs_eq: "R t t \ R \ (=) \ Rep (Abs t) = t" using a unfolding Quotient_def by blast lemma Quotient_rep_abs_fold_unmap: assumes "x' \ Abs x" and "R x x" and "Rep x' \ Rep' x'" shows "R (Rep' x') x" proof - have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto then show ?thesis using assms(3) by simp qed lemma Quotient_Rep_eq: assumes "x' \ Abs x" shows "Rep x' \ Rep x'" by simp lemma Quotient_rel_abs: "R r s \ Abs r = Abs s" using a unfolding Quotient_def by blast lemma Quotient_rel_abs2: assumes "R (Rep x) y" shows "x = Abs y" proof - from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs) then show ?thesis using assms(1) by (simp add: Quotient_abs_rep) qed lemma Quotient_symp: "symp R" using a unfolding Quotient_def using sympI by (metis (full_types)) lemma Quotient_transp: "transp R" using a unfolding Quotient_def using transpI by (metis (full_types)) lemma Quotient_part_equivp: "part_equivp R" by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) end lemma identity_quotient: "Quotient (=) id id (=)" unfolding Quotient_def by simp text \TODO: Use one of these alternatives as the real definition.\ lemma Quotient_alt_def: "Quotient R Abs Rep T \ (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ (\x y. R x y \ T x (Abs x) \ T y (Abs y) \ Abs x = Abs y)" apply safe apply (simp (no_asm_use) only: Quotient_def, fast) apply (simp (no_asm_use) only: Quotient_def, fast) apply (simp (no_asm_use) only: Quotient_def, fast) apply (simp (no_asm_use) only: Quotient_def, fast) apply (simp (no_asm_use) only: Quotient_def, fast) apply (simp (no_asm_use) only: Quotient_def, fast) apply (rule QuotientI) apply simp apply metis apply simp apply (rule ext, rule ext, metis) done lemma Quotient_alt_def2: "Quotient R Abs Rep T \ (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ (\x y. R x y \ T x (Abs y) \ T y (Abs x))" unfolding Quotient_alt_def by (safe, metis+) lemma Quotient_alt_def3: "Quotient R Abs Rep T \ (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ (\x y. R x y \ (\z. T x z \ T y z))" unfolding Quotient_alt_def2 by (safe, metis+) lemma Quotient_alt_def4: "Quotient R Abs Rep T \ (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ R = T OO conversep T" unfolding Quotient_alt_def3 fun_eq_iff by auto lemma Quotient_alt_def5: "Quotient R Abs Rep T \ T \ BNF_Def.Grp UNIV Abs \ BNF_Def.Grp UNIV Rep \ T\\ \ R = T OO T\\" unfolding Quotient_alt_def4 Grp_def by blast lemma fun_quotient: assumes 1: "Quotient R1 abs1 rep1 T1" assumes 2: "Quotient R2 abs2 rep2 T2" shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)" using assms unfolding Quotient_alt_def2 unfolding rel_fun_def fun_eq_iff map_fun_apply by (safe, metis+) lemma apply_rsp: fixes f g::"'a \ 'c" assumes q: "Quotient R1 Abs1 Rep1 T1" and a: "(R1 ===> R2) f g" "R1 x y" shows "R2 (f x) (g y)" using a by (auto elim: rel_funE) lemma apply_rsp': assumes a: "(R1 ===> R2) f g" "R1 x y" shows "R2 (f x) (g y)" using a by (auto elim: rel_funE) lemma apply_rsp'': assumes "Quotient R Abs Rep T" and "(R ===> S) f f" shows "S (f (Rep x)) (f (Rep x))" proof - from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) then show ?thesis using assms(2) by (auto intro: apply_rsp') qed subsection \Quotient composition\ lemma Quotient_compose: assumes 1: "Quotient R1 Abs1 Rep1 T1" assumes 2: "Quotient R2 Abs2 Rep2 T2" shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \ Abs1) (Rep1 \ Rep2) (T1 OO T2)" using assms unfolding Quotient_alt_def4 by fastforce lemma equivp_reflp2: "equivp R \ reflp R" by (erule equivpE) subsection \Respects predicate\ definition Respects :: "('a \ 'a \ bool) \ 'a set" where "Respects R = {x. R x x}" lemma in_respects: "x \ Respects R \ R x x" unfolding Respects_def by simp lemma UNIV_typedef_to_Quotient: assumes "type_definition Rep Abs UNIV" and T_def: "T \ (\x y. x = Rep y)" shows "Quotient (=) Abs Rep T" proof - interpret type_definition Rep Abs UNIV by fact from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis by (fastforce intro!: QuotientI fun_eq_iff) qed lemma UNIV_typedef_to_equivp: fixes Abs :: "'a \ 'b" and Rep :: "'b \ 'a" assumes "type_definition Rep Abs (UNIV::'a set)" shows "equivp ((=) ::'a\'a\bool)" by (rule identity_equivp) lemma typedef_to_Quotient: assumes "type_definition Rep Abs S" and T_def: "T \ (\x y. x = Rep y)" shows "Quotient (eq_onp (\x. x \ S)) Abs Rep T" proof - interpret type_definition Rep Abs S by fact from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis by (auto intro!: QuotientI simp: eq_onp_def fun_eq_iff) qed lemma typedef_to_part_equivp: assumes "type_definition Rep Abs S" shows "part_equivp (eq_onp (\x. x \ S))" proof (intro part_equivpI) interpret type_definition Rep Abs S by fact show "\x. eq_onp (\x. x \ S) x x" using Rep by (auto simp: eq_onp_def) next show "symp (eq_onp (\x. x \ S))" by (auto intro: sympI simp: eq_onp_def) next show "transp (eq_onp (\x. x \ S))" by (auto intro: transpI simp: eq_onp_def) qed lemma open_typedef_to_Quotient: assumes "type_definition Rep Abs {x. P x}" and T_def: "T \ (\x y. x = Rep y)" shows "Quotient (eq_onp P) Abs Rep T" using typedef_to_Quotient [OF assms] by simp lemma open_typedef_to_part_equivp: assumes "type_definition Rep Abs {x. P x}" shows "part_equivp (eq_onp P)" using typedef_to_part_equivp [OF assms] by simp lemma type_definition_Quotient_not_empty: "Quotient (eq_onp P) Abs Rep T \ \x. P x" unfolding eq_onp_def by (drule Quotient_rep_reflp) blast lemma type_definition_Quotient_not_empty_witness: "Quotient (eq_onp P) Abs Rep T \ P (Rep undefined)" unfolding eq_onp_def by (drule Quotient_rep_reflp) blast text \Generating transfer rules for quotients.\ context fixes R Abs Rep T assumes 1: "Quotient R Abs Rep T" begin lemma Quotient_right_unique: "right_unique T" using 1 unfolding Quotient_alt_def right_unique_def by metis lemma Quotient_right_total: "right_total T" using 1 unfolding Quotient_alt_def right_total_def by metis lemma Quotient_rel_eq_transfer: "(T ===> T ===> (=)) R (=)" using 1 unfolding Quotient_alt_def rel_fun_def by simp lemma Quotient_abs_induct: assumes "\y. R y y \ P (Abs y)" shows "P x" using 1 assms unfolding Quotient_def by metis end text \Generating transfer rules for total quotients.\ context fixes R Abs Rep T assumes 1: "Quotient R Abs Rep T" and 2: "reflp R" begin lemma Quotient_left_total: "left_total T" using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto lemma Quotient_bi_total: "bi_total T" using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto lemma Quotient_id_abs_transfer: "((=) ===> T) (\x. x) Abs" using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp lemma Quotient_total_abs_induct: "(\y. P (Abs y)) \ P x" using 1 2 unfolding Quotient_alt_def reflp_def by metis lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \ R x y" using Quotient_rel [OF 1] 2 unfolding reflp_def by simp end text \Generating transfer rules for a type defined with \typedef\.\ context fixes Rep Abs A T assumes type: "type_definition Rep Abs A" assumes T_def: "T \ (\(x::'a) (y::'b). x = Rep y)" begin lemma typedef_left_unique: "left_unique T" unfolding left_unique_def T_def by (simp add: type_definition.Rep_inject [OF type]) lemma typedef_bi_unique: "bi_unique T" unfolding bi_unique_def T_def by (simp add: type_definition.Rep_inject [OF type]) (* the following two theorems are here only for convinience *) lemma typedef_right_unique: "right_unique T" using T_def type Quotient_right_unique typedef_to_Quotient by blast lemma typedef_right_total: "right_total T" using T_def type Quotient_right_total typedef_to_Quotient by blast lemma typedef_rep_transfer: "(T ===> (=)) (\x. x) Rep" unfolding rel_fun_def T_def by simp end text \Generating the correspondence rule for a constant defined with \lift_definition\.\ lemma Quotient_to_transfer: assumes "Quotient R Abs Rep T" and "R c c" and "c' \ Abs c" shows "T c c'" using assms by (auto dest: Quotient_cr_rel) text \Proving reflexivity\ lemma Quotient_to_left_total: assumes q: "Quotient R Abs Rep T" and r_R: "reflp R" shows "left_total T" using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE) lemma Quotient_composition_ge_eq: assumes "left_total T" assumes "R \ (=)" shows "(T OO R OO T\\) \ (=)" using assms unfolding left_total_def by fast lemma Quotient_composition_le_eq: assumes "left_unique T" assumes "R \ (=)" shows "(T OO R OO T\\) \ (=)" using assms unfolding left_unique_def by blast lemma eq_onp_le_eq: "eq_onp P \ (=)" unfolding eq_onp_def by blast lemma reflp_ge_eq: "reflp R \ R \ (=)" unfolding reflp_def by blast text \Proving a parametrized correspondence relation\ definition POS :: "('a \ 'b \ bool) \ ('a \ 'b \ bool) \ bool" where "POS A B \ A \ B" definition NEG :: "('a \ 'b \ bool) \ ('a \ 'b \ bool) \ bool" where "NEG A B \ B \ A" lemma pos_OO_eq: shows "POS (A OO (=)) A" unfolding POS_def OO_def by blast lemma pos_eq_OO: shows "POS ((=) OO A) A" unfolding POS_def OO_def by blast lemma neg_OO_eq: shows "NEG (A OO (=)) A" unfolding NEG_def OO_def by auto lemma neg_eq_OO: shows "NEG ((=) OO A) A" unfolding NEG_def OO_def by blast lemma POS_trans: assumes "POS A B" assumes "POS B C" shows "POS A C" using assms unfolding POS_def by auto lemma NEG_trans: assumes "NEG A B" assumes "NEG B C" shows "NEG A C" using assms unfolding NEG_def by auto lemma POS_NEG: "POS A B \ NEG B A" unfolding POS_def NEG_def by auto lemma NEG_POS: "NEG A B \ POS B A" unfolding POS_def NEG_def by auto lemma POS_pcr_rule: assumes "POS (A OO B) C" shows "POS (A OO B OO X) (C OO X)" using assms unfolding POS_def OO_def by blast lemma NEG_pcr_rule: assumes "NEG (A OO B) C" shows "NEG (A OO B OO X) (C OO X)" using assms unfolding NEG_def OO_def by blast lemma POS_apply: assumes "POS R R'" assumes "R f g" shows "R' f g" using assms unfolding POS_def by auto text \Proving a parametrized correspondence relation\ lemma fun_mono: assumes "A \ C" assumes "B \ D" shows "(A ===> B) \ (C ===> D)" using assms unfolding rel_fun_def by blast lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \ ((R OO R') ===> (S OO S'))" unfolding OO_def rel_fun_def by blast lemma functional_relation: "right_unique R \ left_total R \ \x. \!y. R x y" unfolding right_unique_def left_total_def by blast lemma functional_converse_relation: "left_unique R \ right_total R \ \y. \!x. R x y" unfolding left_unique_def right_total_def by blast lemma neg_fun_distr1: assumes 1: "left_unique R" "right_total R" assumes 2: "right_unique R'" "left_total R'" shows "(R OO R' ===> S OO S') \ ((R ===> S) OO (R' ===> S')) " using functional_relation[OF 2] functional_converse_relation[OF 1] unfolding rel_fun_def OO_def apply clarify apply (subst all_comm) apply (subst all_conj_distrib[symmetric]) apply (intro choice) by metis lemma neg_fun_distr2: assumes 1: "right_unique R'" "left_total R'" assumes 2: "left_unique S'" "right_total S'" shows "(R OO R' ===> S OO S') \ ((R ===> S) OO (R' ===> S'))" using functional_converse_relation[OF 2] functional_relation[OF 1] unfolding rel_fun_def OO_def apply clarify apply (subst all_comm) apply (subst all_conj_distrib[symmetric]) apply (intro choice) by metis subsection \Domains\ lemma composed_equiv_rel_eq_onp: assumes "left_unique R" assumes "(R ===> (=)) P P'" assumes "Domainp R = P''" shows "(R OO eq_onp P' OO R\\) = eq_onp (inf P'' P)" using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def fun_eq_iff by blast lemma composed_equiv_rel_eq_eq_onp: assumes "left_unique R" assumes "Domainp R = P" shows "(R OO (=) OO R\\) = eq_onp P" using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def fun_eq_iff is_equality_def by metis lemma pcr_Domainp_par_left_total: assumes "Domainp B = P" assumes "left_total A" assumes "(A ===> (=)) P' P" shows "Domainp (A OO B) = P'" using assms unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def by (fast intro: fun_eq_iff) lemma pcr_Domainp_par: assumes "Domainp B = P2" assumes "Domainp A = P1" assumes "(A ===> (=)) P2' P2" shows "Domainp (A OO B) = (inf P1 P2')" using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def by (fast intro: fun_eq_iff) definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool" where "rel_pred_comp R P \ \x. \y. R x y \ P y" lemma pcr_Domainp: assumes "Domainp B = P" shows "Domainp (A OO B) = (\x. \y. A x y \ P y)" using assms by blast lemma pcr_Domainp_total: assumes "left_total B" assumes "Domainp A = P" shows "Domainp (A OO B) = P" using assms unfolding left_total_def by fast lemma Quotient_to_Domainp: assumes "Quotient R Abs Rep T" shows "Domainp T = (\x. R x x)" by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) lemma eq_onp_to_Domainp: assumes "Quotient (eq_onp P) Abs Rep T" shows "Domainp T = P" by (simp add: eq_onp_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) end (* needed for lifting_def_code_dt.ML (moved from Lifting_Set) *) -lemma right_total_UNIV_transfer: +lemma right_total_UNIV_transfer: assumes "right_total A" shows "(rel_set A) (Collect (Domainp A)) UNIV" using assms unfolding right_total_def rel_set_def Domainp_iff by blast subsection \ML setup\ ML_file \Tools/Lifting/lifting_util.ML\ named_theorems relator_eq_onp "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate" ML_file \Tools/Lifting/lifting_info.ML\ (* setup for the function type *) declare fun_quotient[quot_map] declare fun_mono[relator_mono] lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2 ML_file \Tools/Lifting/lifting_bnf.ML\ ML_file \Tools/Lifting/lifting_term.ML\ ML_file \Tools/Lifting/lifting_def.ML\ ML_file \Tools/Lifting/lifting_setup.ML\ ML_file \Tools/Lifting/lifting_def_code_dt.ML\ lemma pred_prod_beta: "pred_prod P Q xy \ P (fst xy) \ Q (snd xy)" by(cases xy) simp lemma pred_prod_split: "P (pred_prod Q R xy) \ (\x y. xy = (x, y) \ P (Q x \ R y))" by(cases xy) simp hide_const (open) POS NEG end diff --git a/src/HOL/Quotient.thy b/src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy +++ b/src/HOL/Quotient.thy @@ -1,743 +1,840 @@ (* Title: HOL/Quotient.thy Author: Cezary Kaliszyk and Christian Urban *) section \Definition of Quotient Types\ theory Quotient imports Lifting keywords "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and "quotient_type" :: thy_goal_defn and "/" and - "quotient_definition" :: thy_goal_defn + "quotient_definition" :: thy_goal_defn and + "copy_bnf" :: thy_defn and + "lift_bnf" :: thy_goal_defn begin text \ Basic definition for equivalence relations that are represented by predicates. \ text \Composition of Relations\ abbreviation rel_conj :: "('a \ 'b \ bool) \ ('b \ 'a \ bool) \ 'a \ 'b \ bool" (infixr "OOO" 75) where "r1 OOO r2 \ r1 OO r2 OO r1" lemma eq_comp_r: shows "((=) OOO R) = R" by (auto simp add: fun_eq_iff) context includes lifting_syntax begin subsection \Quotient Predicate\ definition "Quotient3 R Abs Rep \ (\a. Abs (Rep a) = a) \ (\a. R (Rep a) (Rep a)) \ (\r s. R r s \ R r r \ R s s \ Abs r = Abs s)" lemma Quotient3I: assumes "\a. Abs (Rep a) = a" and "\a. R (Rep a) (Rep a)" and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" shows "Quotient3 R Abs Rep" using assms unfolding Quotient3_def by blast context fixes R Abs Rep assumes a: "Quotient3 R Abs Rep" begin lemma Quotient3_abs_rep: "Abs (Rep a) = a" using a unfolding Quotient3_def by simp lemma Quotient3_rep_reflp: "R (Rep a) (Rep a)" using a unfolding Quotient3_def by blast lemma Quotient3_rel: "R r r \ R s s \ Abs r = Abs s \ R r s" \ \orientation does not loop on rewriting\ using a unfolding Quotient3_def by blast -lemma Quotient3_refl1: +lemma Quotient3_refl1: "R r s \ R r r" - using a unfolding Quotient3_def + using a unfolding Quotient3_def by fast -lemma Quotient3_refl2: +lemma Quotient3_refl2: "R r s \ R s s" - using a unfolding Quotient3_def + using a unfolding Quotient3_def by fast lemma Quotient3_rel_rep: "R (Rep a) (Rep b) \ a = b" using a unfolding Quotient3_def by metis lemma Quotient3_rep_abs: "R r r \ R (Rep (Abs r)) r" using a unfolding Quotient3_def by blast lemma Quotient3_rel_abs: "R r s \ Abs r = Abs s" using a unfolding Quotient3_def by blast lemma Quotient3_symp: "symp R" using a unfolding Quotient3_def using sympI by metis lemma Quotient3_transp: "transp R" using a unfolding Quotient3_def using transpI by (metis (full_types)) lemma Quotient3_part_equivp: "part_equivp R" by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI) lemma abs_o_rep: "Abs \ Rep = id" unfolding fun_eq_iff by (simp add: Quotient3_abs_rep) lemma equals_rsp: assumes b: "R xa xb" "R ya yb" shows "R xa ya = R xb yb" using b Quotient3_symp Quotient3_transp by (blast elim: sympE transpE) lemma rep_abs_rsp: assumes b: "R x1 x2" shows "R x1 (Rep (Abs x2))" using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp by metis lemma rep_abs_rsp_left: assumes b: "R x1 x2" shows "R (Rep (Abs x1)) x2" using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp by metis end lemma identity_quotient3: "Quotient3 (=) id id" unfolding Quotient3_def id_def by blast lemma fun_quotient3: assumes q1: "Quotient3 R1 abs1 rep1" and q2: "Quotient3 R2 abs2 rep2" shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" proof - have "(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" for a using q1 q2 by (simp add: Quotient3_def fun_eq_iff) moreover have "(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" for a by (rule rel_funI) (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2], simp (no_asm) add: Quotient3_def, simp) moreover have "(R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s)" for r s proof - have "(R1 ===> R2) r s \ (R1 ===> R2) r r" unfolding rel_fun_def - using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] + using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] by (metis (full_types) part_equivp_def) moreover have "(R1 ===> R2) r s \ (R1 ===> R2) s s" unfolding rel_fun_def - using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] + using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] by (metis (full_types) part_equivp_def) moreover have "(R1 ===> R2) r s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s" by (auto simp add: rel_fun_def fun_eq_iff) (use q1 q2 in \unfold Quotient3_def, metis\) moreover have "((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s) \ (R1 ===> R2) r s" by (auto simp add: rel_fun_def fun_eq_iff) (use q1 q2 in \unfold Quotient3_def, metis map_fun_apply\) ultimately show ?thesis by blast qed ultimately show ?thesis by (intro Quotient3I) (assumption+) qed lemma lambda_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" unfolding fun_eq_iff using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp lemma lambda_prs1: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" unfolding fun_eq_iff using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp text\ In the following theorem R1 can be instantiated with anything, but we know some of the types of the Rep and Abs functions; so by solving Quotient assumptions we can get a unique R1 that will be provable; which is why we need to use \apply_rsp\ and not the primed version\ lemma apply_rspQ3: fixes f g::"'a \ 'c" assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" "R1 x y" shows "R2 (f x) (g y)" using a by (auto elim: rel_funE) lemma apply_rspQ3'': assumes "Quotient3 R Abs Rep" and "(R ===> S) f f" shows "S (f (Rep x)) (f (Rep x))" proof - from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp) then show ?thesis using assms(2) by (auto intro: apply_rsp') qed subsection \lemmas for regularisation of ball and bex\ lemma ball_reg_eqv: fixes P :: "'a \ bool" assumes a: "equivp R" shows "Ball (Respects R) P = (All P)" using a unfolding equivp_def by (auto simp add: in_respects) lemma bex_reg_eqv: fixes P :: "'a \ bool" assumes a: "equivp R" shows "Bex (Respects R) P = (Ex P)" using a unfolding equivp_def by (auto simp add: in_respects) lemma ball_reg_right: assumes a: "\x. x \ R \ P x \ Q x" shows "All P \ Ball R Q" using a by fast lemma bex_reg_left: assumes a: "\x. x \ R \ Q x \ P x" shows "Bex R Q \ Ex P" using a by fast lemma ball_reg_left: assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" using a by (metis equivp_reflp in_respects) lemma bex_reg_right: assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" using a by (metis equivp_reflp in_respects) lemma ball_reg_eqv_range: fixes P::"'a \ bool" and x::"'a" assumes a: "equivp R2" shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" apply(rule iffI) apply(rule allI) apply(drule_tac x="\y. f x" in bspec) apply(simp add: in_respects rel_fun_def) apply(rule impI) using a equivp_reflp_symp_transp[of "R2"] apply (auto elim: equivpE reflpE) done lemma bex_reg_eqv_range: assumes a: "equivp R2" shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" apply(auto) apply(rule_tac x="\y. f x" in bexI) apply(simp) apply(simp add: Respects_def in_respects rel_fun_def) apply(rule impI) using a equivp_reflp_symp_transp[of "R2"] apply (auto elim: equivpE reflpE) done (* Next four lemmas are unused *) lemma all_reg: assumes a: "\x :: 'a. (P x \ Q x)" and b: "All P" shows "All Q" using a b by fast lemma ex_reg: assumes a: "\x :: 'a. (P x \ Q x)" and b: "Ex P" shows "Ex Q" using a b by fast lemma ball_reg: assumes a: "\x :: 'a. (x \ R \ P x \ Q x)" and b: "Ball R P" shows "Ball R Q" using a b by fast lemma bex_reg: assumes a: "\x :: 'a. (x \ R \ P x \ Q x)" and b: "Bex R P" shows "Bex R Q" using a b by fast lemma ball_all_comm: assumes "\y. (\x\P. A x y) \ (\x. B x y)" shows "(\x\P. \y. A x y) \ (\x. \y. B x y)" using assms by auto lemma bex_ex_comm: assumes "(\y. \x. A x y) \ (\y. \x\P. B x y)" shows "(\x. \y. A x y) \ (\x\P. \y. B x y)" using assms by auto subsection \Bounded abstraction\ definition Babs :: "'a set \ ('a \ 'b) \ 'a \ 'b" where "x \ p \ Babs p m x = m x" lemma babs_rsp: assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" apply (auto simp add: Babs_def in_respects rel_fun_def) apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") using a apply (simp add: Babs_def rel_fun_def) apply (simp add: in_respects rel_fun_def) using Quotient3_rel[OF q] by metis lemma babs_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" apply (rule ext) apply (simp add:) apply (subgoal_tac "Rep1 x \ Respects R1") apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) apply (simp add: in_respects Quotient3_rel_rep[OF q1]) done lemma babs_simp: assumes q: "Quotient3 R1 Abs Rep" shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" apply(rule iffI) apply(simp_all only: babs_rsp[OF q]) apply(auto simp add: Babs_def rel_fun_def) apply(metis Babs_def in_respects Quotient3_rel[OF q]) done (* If a user proves that a particular functional relation is an equivalence this may be useful in regularising *) lemma babs_reg_eqv: shows "equivp R \ Babs (Respects R) P = P" by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp) (* 3 lemmas needed for proving repabs_inj *) lemma ball_rsp: assumes a: "(R ===> (=)) f g" shows "Ball (Respects R) f = Ball (Respects R) g" using a by (auto simp add: Ball_def in_respects elim: rel_funE) lemma bex_rsp: assumes a: "(R ===> (=)) f g" shows "(Bex (Respects R) f = Bex (Respects R) g)" using a by (auto simp add: Bex_def in_respects elim: rel_funE) lemma bex1_rsp: assumes a: "(R ===> (=)) f g" shows "Ex1 (\x. x \ Respects R \ f x) = Ex1 (\x. x \ Respects R \ g x)" - using a by (auto elim: rel_funE simp add: Ex1_def in_respects) + using a by (auto elim: rel_funE simp add: Ex1_def in_respects) (* 2 lemmas needed for cleaning of quantifiers *) lemma all_prs: assumes a: "Quotient3 R absf repf" shows "Ball (Respects R) ((absf ---> id) f) = All f" using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def by metis lemma ex_prs: assumes a: "Quotient3 R absf repf" shows "Bex (Respects R) ((absf ---> id) f) = Ex f" using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def by metis subsection \\Bex1_rel\ quantifier\ definition Bex1_rel :: "('a \ 'a \ bool) \ ('a \ bool) \ bool" where "Bex1_rel R P \ (\x \ Respects R. P x) \ (\x \ Respects R. \y \ Respects R. ((P x \ P y) \ (R x y)))" lemma bex1_rel_aux: "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R x\ \ Bex1_rel R y" unfolding Bex1_rel_def by (metis in_respects) lemma bex1_rel_aux2: "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R y\ \ Bex1_rel R x" unfolding Bex1_rel_def by (metis in_respects) lemma bex1_rel_rsp: assumes a: "Quotient3 R absf repf" shows "((R ===> (=)) ===> (=)) (Bex1_rel R) (Bex1_rel R)" unfolding rel_fun_def by (metis bex1_rel_aux bex1_rel_aux2) lemma ex1_prs: assumes "Quotient3 R absf repf" shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" apply (auto simp: Bex1_rel_def Respects_def) apply (metis Quotient3_def assms) apply (metis (full_types) Quotient3_def assms) by (meson Quotient3_rel assms) lemma bex1_bexeq_reg: shows "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects) - + lemma bex1_bexeq_reg_eqv: assumes a: "equivp R" shows "(\!x. P x) \ Bex1_rel R P" using equivp_reflp[OF a] by (metis (full_types) Bex1_rel_def in_respects) subsection \Various respects and preserve lemmas\ lemma quot_rel_rsp: assumes a: "Quotient3 R Abs Rep" shows "(R ===> R ===> (=)) R R" apply(rule rel_funI)+ by (meson assms equals_rsp) lemma o_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" and q3: "Quotient3 R3 Abs3 Rep3" shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) (\) = (\)" and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) (\) = (\)" using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] by (simp_all add: fun_eq_iff) lemma o_rsp: "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) (\) (\)" "((=) ===> (R1 ===> (=)) ===> R1 ===> (=)) (\) (\)" by (force elim: rel_funE)+ lemma cond_prs: assumes a: "Quotient3 R absf repf" shows "absf (if a then repf b else repf c) = (if a then b else c)" using a unfolding Quotient3_def by auto lemma if_prs: assumes q: "Quotient3 R Abs Rep" shows "(id ---> Rep ---> Rep ---> Abs) If = If" using Quotient3_abs_rep[OF q] by (auto simp add: fun_eq_iff) lemma if_rsp: assumes q: "Quotient3 R Abs Rep" shows "((=) ===> R ===> R ===> R) If If" by force lemma let_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by (auto simp add: fun_eq_iff) lemma let_rsp: shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" by (force elim: rel_funE) lemma id_rsp: shows "(R ===> R) id id" by auto lemma id_prs: assumes a: "Quotient3 R Abs Rep" shows "(Rep ---> Abs) id = id" by (simp add: fun_eq_iff Quotient3_abs_rep [OF a]) end locale quot_type = fixes R :: "'a \ 'a \ bool" and Abs :: "'a set \ 'b" and Rep :: "'b \ 'a set" assumes equivp: "part_equivp R" and rep_prop: "\y. \x. R x x \ Rep y = Collect (R x)" and rep_inverse: "\x. Abs (Rep x) = x" and abs_inverse: "\c. (\x. ((R x x) \ (c = Collect (R x)))) \ (Rep (Abs c)) = c" and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" begin definition abs :: "'a \ 'b" where "abs x = Abs (Collect (R x))" definition rep :: "'b \ 'a" where "rep a = (SOME x. x \ Rep a)" lemma some_collect: assumes "R r r" shows "R (SOME x. x \ Collect (R r)) = R r" apply simp by (metis assms exE_some equivp[simplified part_equivp_def]) lemma Quotient: shows "Quotient3 R abs rep" unfolding Quotient3_def abs_def rep_def proof (intro conjI allI) fix a r s show x: "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" proof - obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto have "R (SOME x. x \ Rep a) x" using r rep some_collect by metis then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" using part_equivp_transp[OF equivp] by (metis \R (SOME x. x \ Rep a) x\) qed have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto have "R r r \ R s s \ Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" proof - assume "R r r" and "R s s" then have "Abs (Collect (R r)) = Abs (Collect (R s)) \ Collect (R r) = Collect (R s)" by (metis abs_inverse) also have "Collect (R r) = Collect (R s) \ (\A x. x \ A) (Collect (R r)) = (\A x. x \ A) (Collect (R s))" by rule simp_all finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" by simp qed then show "R r s \ R r r \ R s s \ (Abs (Collect (R r)) = Abs (Collect (R s)))" using equivp[simplified part_equivp_def] by metis qed end subsection \Quotient composition\ lemma OOO_quotient3: fixes R1 :: "'a \ 'a \ bool" fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" fixes R2' :: "'a \ 'a \ bool" fixes R2 :: "'b \ 'b \ bool" assumes R1: "Quotient3 R1 Abs1 Rep1" assumes R2: "Quotient3 R2 Abs2 Rep2" assumes Abs1: "\x y. R2' x y \ R1 x x \ R1 y y \ R2 (Abs1 x) (Abs1 y)" assumes Rep1: "\x y. R2 x y \ R2' (Rep1 x) (Rep1 y)" shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ Rep2)" proof - - have *: "(R1 OOO R2') r r \ (R1 OOO R2') s s \ (Abs2 \ Abs1) r = (Abs2 \ Abs1) s + have *: "(R1 OOO R2') r r \ (R1 OOO R2') s s \ (Abs2 \ Abs1) r = (Abs2 \ Abs1) s \ (R1 OOO R2') r s" for r s apply safe subgoal for a b c d apply simp apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) using Quotient3_refl1 R1 rep_abs_rsp apply fastforce apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI) apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) by (metis Quotient3_rel R1 rep_abs_rsp_left) subgoal for x y apply (drule Abs1) apply (erule Quotient3_refl2 [OF R1]) apply (erule Quotient3_refl1 [OF R1]) apply (drule Quotient3_refl1 [OF R2], drule Rep1) by (metis (full_types) Quotient3_def R1 relcompp.relcompI) subgoal for x y apply (drule Abs1) apply (erule Quotient3_refl2 [OF R1]) apply (erule Quotient3_refl1 [OF R1]) apply (drule Quotient3_refl2 [OF R2], drule Rep1) by (metis (full_types) Quotient3_def R1 relcompp.relcompI) subgoal for x y by simp (metis (full_types) Abs1 Quotient3_rel R1 R2) done show ?thesis apply (rule Quotient3I) using * apply (simp_all add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) apply (metis Quotient3_rep_reflp R1 R2 Rep1 relcompp.relcompI) done qed lemma OOO_eq_quotient3: fixes R1 :: "'a \ 'a \ bool" fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" assumes R1: "Quotient3 R1 Abs1 Rep1" assumes R2: "Quotient3 (=) Abs2 Rep2" shows "Quotient3 (R1 OOO (=)) (Abs2 \ Abs1) (Rep1 \ Rep2)" using assms by (rule OOO_quotient3) auto subsection \Quotient3 to Quotient\ lemma Quotient3_to_Quotient: assumes "Quotient3 R Abs Rep" and "T \ \x y. R x x \ Abs x = y" shows "Quotient R Abs Rep T" using assms unfolding Quotient3_def by (intro QuotientI) blast+ lemma Quotient3_to_Quotient_equivp: assumes q: "Quotient3 R Abs Rep" and T_def: "T \ \x y. Abs x = y" and eR: "equivp R" shows "Quotient R Abs Rep T" proof (intro QuotientI) fix a show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep) next fix a show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp) next fix r s show "R r s = (R r r \ R s s \ Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) next show "T = (\x y. R x x \ Abs x = y)" using T_def equivp_reflp[OF eR] by simp qed subsection \ML setup\ text \Auxiliary data for the quotient package\ named_theorems quot_equiv "equivalence relation theorems" and quot_respect "respectfulness theorems" and quot_preserve "preservation theorems" and id_simps "identity simp rules for maps" and quot_thm "quotient theorems" ML_file \Tools/Quotient/quotient_info.ML\ declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]] lemmas [quot_thm] = fun_quotient3 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp lemmas [quot_preserve] = if_prs o_prs let_prs id_prs lemmas [quot_equiv] = identity_equivp text \Lemmas about simplifying id's.\ lemmas [id_simps] = id_def[symmetric] map_fun_id id_apply id_o o_id eq_comp_r vimage_id text \Translation functions for the lifting process.\ ML_file \Tools/Quotient/quotient_term.ML\ text \Definitions of the quotient types.\ ML_file \Tools/Quotient/quotient_type.ML\ text \Definitions for quotient constants.\ ML_file \Tools/Quotient/quotient_def.ML\ text \ An auxiliary constant for recording some information about the lifted theorem in a tactic. \ definition Quot_True :: "'a \ bool" where "Quot_True x \ True" lemma shows QT_all: "Quot_True (All P) \ Quot_True P" and QT_ex: "Quot_True (Ex P) \ Quot_True P" and QT_ex1: "Quot_True (Ex1 P) \ Quot_True P" and QT_lam: "Quot_True (\x. P x) \ (\x. Quot_True (P x))" and QT_ext: "(\x. Quot_True (a x) \ f x = g x) \ (Quot_True a \ f = g)" by (simp_all add: Quot_True_def ext) lemma QT_imp: "Quot_True a \ Quot_True b" by (simp add: Quot_True_def) context includes lifting_syntax begin text \Tactics for proving the lifted theorems\ ML_file \Tools/Quotient/quotient_tacs.ML\ end subsection \Methods / Interface\ method_setup lifting = - \Attrib.thms >> (fn thms => fn ctxt => + \Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms))\ \lift theorems to quotient types\ method_setup lifting_setup = - \Attrib.thm >> (fn thm => fn ctxt => + \Attrib.thm >> (fn thm => fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm))\ \set up the three goals for the quotient lifting procedure\ method_setup descending = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt []))\ \decend theorems to the raw level\ method_setup descending_setup = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt []))\ \set up the three goals for the decending theorems\ method_setup partiality_descending = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt []))\ \decend theorems to the raw level\ method_setup partiality_descending_setup = - \Scan.succeed (fn ctxt => + \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))\ \set up the three goals for the decending theorems\ method_setup regularize = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt))\ \prove the regularization goals from the quotient lifting procedure\ method_setup injection = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt))\ \prove the rep/abs injection goals from the quotient lifting procedure\ method_setup cleaning = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt))\ \prove the cleaning goals from the quotient lifting procedure\ attribute_setup quot_lifted = \Scan.succeed Quotient_Tacs.lifted_attrib\ \lift theorems to quotient types\ no_notation rel_conj (infixr "OOO" 75) +section \Lifting of BNFs\ + +lemma sum_insert_Inl_unit: "x \ A \ (\y. x = Inr y \ Inr y \ B) \ x \ insert (Inl ()) B" + by (cases x) (simp_all) + +lemma lift_sum_unit_vimage_commute: + "insert (Inl ()) (Inr ` f -` A) = map_sum id f -` insert (Inl ()) (Inr ` A)" + by (auto simp: map_sum_def split: sum.splits) + +lemma insert_Inl_int_map_sum_unit: "insert (Inl ()) A \ range (map_sum id f) \ {}" + by (auto simp: map_sum_def split: sum.splits) + +lemma image_map_sum_unit_subset: + "A \ insert (Inl ()) (Inr ` B) \ map_sum id f ` A \ insert (Inl ()) (Inr ` f ` B)" + by auto + +lemma subset_lift_sum_unitD: "A \ insert (Inl ()) (Inr ` B) \ Inr x \ A \ x \ B" + unfolding insert_def by auto + +lemma UNIV_sum_unit_conv: "insert (Inl ()) (range Inr) = UNIV" + unfolding UNIV_sum UNIV_unit image_insert image_empty Un_insert_left sup_bot.left_neutral.. + +lemma subset_vimage_image_subset: "A \ f -` B \ f ` A \ B" + by auto + +lemma relcompp_mem_Grp_neq_bot: + "A \ range f \ {} \ (\x y. x \ A \ y \ A) OO (Grp UNIV f)\\ \ bot" + unfolding Grp_def relcompp_apply fun_eq_iff by blast + +lemma comp_projr_Inr: "projr \ Inr = id" + by auto + +lemma in_rel_sum_in_image_projr: + "B \ {(x,y). rel_sum ((=) :: unit \ unit \ bool) A x y} \ + Inr ` C = fst ` B \ snd ` B = Inr ` D \ map_prod projr projr ` B \ {(x,y). A x y}" + by (force simp: projr_def image_iff dest!: spec[of _ "Inl ()"] split: sum.splits) + +lemma subset_rel_sumI: "B \ {(x,y). A x y} \ rel_sum ((=) :: unit => unit => bool) A + (if x \ B then Inr (fst x) else Inl ()) + (if x \ B then Inr (snd x) else Inl ())" + by auto + +lemma relcompp_eq_Grp_neq_bot: "(=) OO (Grp UNIV f)\\ \ bot" + unfolding Grp_def relcompp_apply fun_eq_iff by blast + +lemma rel_fun_rel_OO1: "(rel_fun Q (rel_fun R (=))) A B \ conversep Q OO A OO R \ B" + by (auto simp: rel_fun_def) + +lemma rel_fun_rel_OO2: "(rel_fun Q (rel_fun R (=))) A B \ Q OO B OO conversep R \ A" + by (auto simp: rel_fun_def) + +lemma rel_sum_eq2_nonempty: "rel_sum (=) A OO rel_sum (=) B \ bot" + by (auto simp: fun_eq_iff relcompp_apply intro!: exI[of _ "Inl _"]) + +lemma rel_sum_eq3_nonempty: "rel_sum (=) A OO (rel_sum (=) B OO rel_sum (=) C) \ bot" + by (auto simp: fun_eq_iff relcompp_apply intro!: exI[of _ "Inl _"]) + +lemma hypsubst: "A = B \ x \ B \ (x \ A \ P) \ P" by simp + +lemma Quotient_crel_quotient: "Quotient R Abs Rep T \ equivp R \ T \ (\x y. Abs x = y)" + by (drule Quotient_cr_rel) (auto simp: fun_eq_iff equivp_reflp intro!: eq_reflection) + +lemma Quotient_crel_typedef: "Quotient (eq_onp P) Abs Rep T \ T \ (\x y. x = Rep y)" + unfolding Quotient_def + by (auto 0 4 simp: fun_eq_iff eq_onp_def intro: sym intro!: eq_reflection) + +lemma Quotient_crel_typecopy: "Quotient (=) Abs Rep T \ T \ (\x y. x = Rep y)" + by (subst (asm) eq_onp_True[symmetric]) (rule Quotient_crel_typedef) + +lemma equivp_add_relconj: + assumes equiv: "equivp R" "equivp R'" and le: "S OO T OO U \ R OO STU OO R'" + shows "R OO S OO T OO U OO R' \ R OO STU OO R'" +proof - + have trans: "R OO R \ R" "R' OO R' \ R'" + using equiv unfolding equivp_reflp_symp_transp transp_relcompp by blast+ + have "R OO S OO T OO U OO R' = R OO (S OO T OO U) OO R'" + unfolding relcompp_assoc .. + also have "\ \ R OO (R OO STU OO R') OO R'" + by (intro le relcompp_mono order_refl) + also have "\ \ (R OO R) OO STU OO (R' OO R')" + unfolding relcompp_assoc .. + also have "\ \ R OO STU OO R'" + by (intro trans relcompp_mono order_refl) + finally show ?thesis . +qed + +ML_file "Tools/BNF/bnf_lift.ML" + +hide_fact + sum_insert_Inl_unit lift_sum_unit_vimage_commute insert_Inl_int_map_sum_unit + image_map_sum_unit_subset subset_lift_sum_unitD UNIV_sum_unit_conv subset_vimage_image_subset + relcompp_mem_Grp_neq_bot comp_projr_Inr in_rel_sum_in_image_projr subset_rel_sumI + relcompp_eq_Grp_neq_bot rel_fun_rel_OO1 rel_fun_rel_OO2 rel_sum_eq2_nonempty rel_sum_eq3_nonempty + hypsubst equivp_add_relconj + end diff --git a/src/HOL/Tools/BNF/bnf_lift.ML b/src/HOL/Tools/BNF/bnf_lift.ML --- a/src/HOL/Tools/BNF/bnf_lift.ML +++ b/src/HOL/Tools/BNF/bnf_lift.ML @@ -1,452 +1,2022 @@ (* Title: HOL/Tools/BNF/bnf_lift.ML Author: Julian Biendarra, TU Muenchen + Author: Basil Fürer, ETH Zurich + Author: Joshua Schneider, ETH Zurich Author: Dmitriy Traytel, ETH Zurich - Copyright 2015 + Copyright 2015, 2019 Lifting of BNFs through typedefs. *) signature BNF_LIFT = sig datatype lift_bnf_option = Plugins_Option of Proof.context -> Plugin_Name.filter | No_Warn_Wits + | No_Warn_Transfer val copy_bnf: (((lift_bnf_option list * (binding option * (string * sort option)) list) * string) * thm option) * (binding * binding * binding) -> local_theory -> local_theory val copy_bnf_cmd: (((lift_bnf_option list * (binding option * (string * string option)) list) * string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) -> local_theory -> local_theory val lift_bnf: ((((lift_bnf_option list * (binding option * (string * sort option)) list) * string) * term list option) * thm option) * (binding * binding * binding) -> ({context: Proof.context, prems: thm list} -> tactic) list -> local_theory -> local_theory val lift_bnf_cmd: ((((lift_bnf_option list * (binding option * (string * string option)) list) * string) * string list) * (Facts.ref * Token.src list) option) * (binding * binding * binding) -> local_theory -> Proof.state end structure BNF_Lift : BNF_LIFT = struct open Ctr_Sugar_Tactics open BNF_Util open BNF_Comp open BNF_Def -(* typedef_bnf *) - datatype lift_bnf_option = Plugins_Option of Proof.context -> Plugin_Name.filter -| No_Warn_Wits; +| No_Warn_Wits +| No_Warn_Transfer; + +datatype lift_thm = Typedef of thm | Quotient of thm + +(** Util **) + +fun last2 [x, y] = ([], (x, y)) + | last2 (x :: xs) = last2 xs |>> (fn y => x :: y) + | last2 [] = raise Match; + +fun strip3 thm = (case Term.strip_comb (HOLogic.dest_Trueprop (Thm.prop_of thm)) of + (_, [x1, x2, x3]) => (x1, x2, x3) + | _ => error "strip3: wrong number of arguments"); + +val mk_Free = yield_singleton o mk_Frees; + +fun TWICE t = t THEN' t; + +fun prove lthy fvars tm tac = + Goal.prove_sorry lthy (map (fst o dest_Free) fvars) [] tm (fn {context, ...} => tac context); + +(** Term construction **) + +fun mk_relT aT bT = aT --> bT --> HOLogic.boolT; +fun mk_relcompp r s = let + val (rT, sT) = apply2 fastype_of (r, s); + val ((xT, _), (_, zTs)) = apply2 dest_funT (rT, sT); + val T = rT --> sT --> mk_relT xT (fst (dest_funT zTs)); + in Const (@{const_name relcompp}, T) $ r $ s end; +val mk_OO = fold_rev mk_relcompp; + +(* option from sum *) +fun mk_MaybeT T = mk_sumT (HOLogic.unitT, T); +fun mk_Nothing T = BNF_FP_Util.mk_Inl T HOLogic.unit; +val Just_const = BNF_FP_Util.Inr_const HOLogic.unitT; +fun mk_Just tm = Just_const (fastype_of tm) $ tm; +fun Maybe_map_const T = + let val (xT, yT) = dest_funT T in + Const (@{const_name map_sum}, (HOLogic.unitT --> HOLogic.unitT) --> T --> mk_MaybeT xT --> mk_MaybeT yT) $ + HOLogic.id_const HOLogic.unitT + end; +fun mk_Maybe_map tm = Maybe_map_const (fastype_of tm) $ tm; +fun fromJust_const T = Const (@{const_name sum.projr}, mk_MaybeT T --> T) + +fun rel_Maybe_const T U = + Const (@{const_name rel_sum}, (HOLogic.unitT --> HOLogic.unitT --> HOLogic.boolT) --> + (T --> U --> HOLogic.boolT) --> mk_MaybeT T --> mk_MaybeT U --> HOLogic.boolT) $ + HOLogic.eq_const HOLogic.unitT +fun set_Maybe_const T = Const (@{const_name Basic_BNFs.setr}, mk_MaybeT T --> HOLogic.mk_setT T) + +fun Inf_const T = Const (@{const_name Inf}, HOLogic.mk_setT T --> T); + +fun Image_const T = + let + val relT = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)); + val setT = HOLogic.mk_setT T; + in Const (@{const_name Image}, relT --> setT --> setT) end; + +fun bot_const T = Const (@{const_name bot}, T); + +fun mk_insert x S = + Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S; + +fun mk_vimage f s = + let val (xT, yT) = dest_funT (fastype_of f) in + Const (@{const_name vimage}, (xT --> yT) --> HOLogic.mk_setT yT --> HOLogic.mk_setT xT) $ f $ s + end; + +fun mk_case_prod (x, y) tm = let + val ((x, xT), (y, yT)) = apply2 dest_Free (x, y); + val prodT = HOLogic.mk_prodT (xT, yT); + in HOLogic.Collect_const prodT $ (Const (@{const_name case_prod}, + (xT --> yT --> HOLogic.boolT) --> prodT --> HOLogic.boolT) $ absfree (x, xT) + (absfree (y, yT) tm)) end; + +fun mk_Trueprop_implies (ps, c) = + Logic.list_implies (map HOLogic.mk_Trueprop ps, HOLogic.mk_Trueprop c); + +fun mk_Collect (v, tm) = let val (n, T) = dest_Free v in + HOLogic.mk_Collect (n, T, tm) end; + + +(** witnesses **) +fun prepare_wits is_quotient RepT wits opts alphas wits_F var_as var_as' sets lthy = + let + fun binder_types_until_eq V T = + let + fun strip (TU as Type ("fun", [T, U])) = if V = TU then [] else T :: strip U + | strip T = if V = T then [] else + error ("Bad type for witness: " ^ quote (Syntax.string_of_typ lthy T)); + in strip T end; + + val Iwits = the_default wits_F (Option.map (map (`(map (fn T => + find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits); + + val wit_goals = maps (BNF_Def.mk_wit_goals var_as var_as' sets) Iwits; + + val lost_wits = filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) wits_F; + + val _ = + if null lost_wits orelse exists (fn No_Warn_Wits => true | _ => false) opts then () + else + let + val what = (if is_quotient then "quotient type" else "typedef"); + val (suffix1, suffix2, be) = + (if length lost_wits = 1 then ("", "", "was") else ("s", "es", "were")) + in + lost_wits + |> map (Syntax.pretty_typ lthy o fastype_of o snd) + |> Pretty.big_list + ("The following type" ^ suffix1 ^ " of nonemptiness witness" ^ suffix2 ^ + " of the raw type's BNF " ^ be ^ " lost:") + |> (fn pt => Pretty.chunks [pt, + Pretty.para ("You can specify a liftable witness (e.g., a term of one of the above types\ + \ that satisfies the " ^ what ^ "'s invariant)\ + \ using the annotation [wits: ].")]) + |> Pretty.string_of + |> warning + end; + in (Iwits, wit_goals) end; + + +(** transfer theorems **) + +fun mk_transfer_thms' bnf_F bnf_G name consts Tss crel_def pcrel_def defs lthy = let + + val live = length (#alphas Tss); + + val (pcrel_tm, crel_tm) = apply2 (Thm.prop_of #> Logic.dest_equals #> fst #> head_of) + (pcrel_def, crel_def); + + val (var_Qs, var_Rs) = fold Variable.declare_typ (#alphas Tss @ #deads Tss) lthy + |> mk_Frees "Q" (map2 mk_relT (#alphas Tss) (#betas Tss)) + ||>> mk_Frees "R" (map2 mk_relT (#gammas Tss) (#deltas Tss)) + |> fst; + + (* get the "pcrel :: args_raw => rep => abs \ bool" term and instantiate types *) + val (args_raw, (rep, abs)) = pcrel_tm + |> fastype_of + |> binder_types + |> last2; + val thy = Proof_Context.theory_of lthy; + val tyenv_match = Vartab.empty + |> Sign.typ_match thy ((rep, #rep Tss)) + |> Sign.typ_match thy ((abs, #abs Tss)); + val args = map (Envir.subst_type tyenv_match) args_raw; + val (pcrel_a, pcrel_b) = Envir.subst_term (tyenv_match, Vartab.empty) pcrel_tm + |> `(subst_atomic_types (#alphas Tss @ #betas Tss ~~ #gammas Tss @ #deltas Tss)); + + (* match "crel :: {?a F} \ a G" with "rep_G :: {a F}" *) + val tyenv_match = Vartab.empty |> Sign.typ_match thy + (crel_tm |> fastype_of |> binder_types |> hd, #rep Tss); + val crel_b = Envir.subst_term (tyenv_match, Vartab.empty) crel_tm + |> subst_atomic_types (#alphas Tss ~~ #betas Tss) + val crel_d = subst_atomic_types (#betas Tss ~~ #deltas Tss) crel_b; + + (* instantiate pcrel with Qs and Rs*) + val dead_args = map binder_types args + |> map (fn [T,U] => if T = U then SOME T else NONE | _ => NONE); + val parametrize = let + fun go (SOME T :: dTs) tms = HOLogic.eq_const T :: go dTs tms + | go (_ :: dTs) (tm :: tms) = tm :: go dTs tms + | go (_ :: dTs) tms = go dTs tms + | go _ _ = []; + in go dead_args end; + + val pcrel_Qs = list_comb (pcrel_b, parametrize var_Qs); + val pcrel_Rs = list_comb (pcrel_a, parametrize var_Rs); + + (* get the order of the dead variables right *) + val Ds0 = maps the_list dead_args; + val permute_Ds = (mk_T_of_bnf Ds0 (#betas Tss) bnf_G, nth (binder_types (type_of pcrel_Qs)) 1) + |> apply2 (fn Type (_, Ts) => Ts | _ => []) |> op~~ |> typ_subst_atomic; + val Ds0 = map permute_Ds Ds0; + + (* terms for sets of the set_transfer thms *) + val rel_sets_Q = @{map 3} (fn aT => fn bT => fn Q => + mk_rel 1 [aT] [bT] @{term rel_set} $ Q) (#alphas Tss) (#betas Tss) var_Qs; + + (* rewrite rules for pcrel and BNF's relator: "pcrel Q = rel_F OO crel" *) + fun mk_pcr_rel_F_eq Ts Us pcrel vs crel = + let + val thm = HOLogic.mk_Trueprop (HOLogic.mk_eq (pcrel, mk_relcompp (list_comb + (mk_rel_of_bnf (#deads Tss) (Ts Tss) (Us Tss) bnf_F, vs)) crel)); + fun tac ctxt = unfold_thms_tac ctxt (pcrel_def :: defs @ @{thm id_bnf_apply} :: + Transfer.get_relator_eq ctxt) THEN (HEADGOAL (rtac ctxt refl)) + in prove lthy vs thm tac |> mk_abs_def end; + + val pcr_rel_F_eqs = + [mk_pcr_rel_F_eq #alphas #betas pcrel_Qs var_Qs crel_b, + mk_pcr_rel_F_eq #gammas #deltas pcrel_Rs var_Rs crel_d]; + + (* create transfer-relations from term('s type) *) + fun mk_transfer_rel' i tm = + let + fun go T' (n, q) = case T' of + Type ("fun", [T as Type ("fun", _), U]) => + go U (n+1, q) |>> mk_rel_fun (fst (go T (n, q))) + | Type ("fun", [T, U]) => + go T (n, q) |-> (fn x => fn st => go U st |>> mk_rel_fun x) + | Type (@{type_name bool}, _) => (HOLogic.eq_const HOLogic.boolT, (n, q)) + | Type (@{type_name set}, _) => (nth rel_sets_Q n, (n, q)) + | Type _ => (if q then pcrel_Qs else pcrel_Rs, (n, not q)) + | TFree _ => (nth (if q then var_Qs else var_Rs) n, (n, not q)) + | _ => raise Match + in go (fastype_of tm) (i, true) |> fst end; + + (* prove transfer rules *) + fun prove_transfer_thm' i vars new_tm const = + let + val tm = HOLogic.mk_Trueprop (mk_transfer_rel' i new_tm $ #raw const $ new_tm); + val tac = (fn ctxt => unfold_thms_tac ctxt (pcr_rel_F_eqs @ [crel_def]) THEN + #tac const {Rs=var_Rs,Qs=var_Qs} ctxt); + in prove lthy vars tm tac end; + val prove_transfer_thm = prove_transfer_thm' 0; + + (* map transfer: "((Q ===> R) ===> pcr_G Q ===> pcr_G R) map_F' map_G" *) + val map_G = mk_map_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G; + val map_transfer = prove_transfer_thm (var_Qs @ var_Rs) map_G (#map consts); + + (* pred_transfer: "((Q ===> (=)) ===> pcr_G Q ===> (=)) pred_F' pred_G" *) + val pred_G = mk_pred_of_bnf Ds0 (#betas Tss) bnf_G; + val pred_transfer = #pred consts |> Option.map (fn p => + ("pred", [prove_transfer_thm (var_Qs @ var_Rs) pred_G p])); + + (* rel_transfer: "((Q ===> R ===> (=)) ===> pcr_G Q ===> pcr_G R ===> (=)) rel_F' rel_G" *) + val rel_G = mk_rel_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G; + val rel_transfer = prove_transfer_thm (var_Qs @ var_Rs) rel_G (#rel consts); + + (* set_transfer: "(pcr_G Q ===> rel_set Q) set_F' set_G" *) + val sets_G = mk_sets_of_bnf (replicate live Ds0) (replicate live (#betas Tss)) bnf_G; + fun mk_set_transfer i set_G raw tac = prove_transfer_thm' i var_Qs set_G {raw=raw, tac=tac}; + val sets_transfer = @{map 4} mk_set_transfer + (0 upto (live-1)) sets_G (#raws (#sets consts)) (#tacs (#sets consts)); + + (* export transfer theorems *) + val transform = Morphism.thm (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) |> map; + val b = Binding.qualified_name name; + val qualify = + let val qs = Binding.path_of b; + in fold_rev (fn (s, mand) => Binding.qualify mand s) qs end; + fun mk_binding n = Binding.name (n ^ "_transfer_raw") + |> Binding.qualify true (Binding.name_of b) |> qualify; + val notes = [("map", [map_transfer]), ("rel", [rel_transfer])] @ the_list pred_transfer @ + [("set", sets_transfer)] |> map (fn (n, thms) => + ((mk_binding n, []), [(transform thms, @{attributes [transfer_rule]})])); + + in lthy |> Local_Theory.notes notes |> snd end; + +(* transfer theorems for map, pred (in case of a typedef), rel and sets *) +fun mk_transfer_thms quiet bnf_F bnf_G name consts thm Tss defs lthy = let + + fun mk_crel_def quot_thm = + (case thm of + Quotient equiv => @{thm Quotient_crel_quotient} OF [quot_thm, equiv] + | Typedef _ => hd ([quot_thm] RL @{thms Quotient_crel_typedef Quotient_crel_typecopy})); + fun no_quotient _ = [Pretty.para ("No quotient theorem has been registered for " ^ + Binding.name_of (name_of_bnf bnf_G) ^ "."), + Pretty.para "Use setup_lifting to register a quotient or type definition theorem."]; + fun wrong_quotient T lthy = [Pretty.para ("A wrong quotient theorem has been registered for " ^ + Binding.name_of (name_of_bnf bnf_G) ^ "."), + Pretty.para ("Expected raw type " ^ + Pretty.string_of (Syntax.pretty_typ lthy (T_of_bnf bnf_F)) ^ + " but the quotient theorem has raw type " ^ + Pretty.string_of (Syntax.pretty_typ lthy T) ^ "."), + Pretty.para "Use setup_lifting to register a different quotient or type definition theorem."]; + fun pcr_why _ = [Pretty.para ("The pcr_" ^ Binding.name_of (name_of_bnf bnf_G) ^ + " relator has not been defined.")]; + fun warn_transfer why lthy = + (Pretty.para "The transfer theorems can't be generated:" :: why lthy) + |> Pretty.chunks |> Pretty.string_of |> warning |> K lthy; + fun maybe_warn_transfer why = not quiet ? warn_transfer why; + in + case Lifting_Info.lookup_quotients lthy name of + SOME {pcr_info, quot_thm} => + (let + val crel_def = mk_crel_def quot_thm; + val rty = Lifting_Util.quot_thm_rty_qty quot_thm |> fst; + val thy = Proof_Context.theory_of lthy; + in + if Sign.typ_instance thy (rty, T_of_bnf bnf_F) then + (case pcr_info of + SOME {pcrel_def, ...} => + mk_transfer_thms' bnf_F bnf_G name consts Tss crel_def pcrel_def defs lthy + | _ => maybe_warn_transfer pcr_why lthy) + else maybe_warn_transfer (wrong_quotient rty) lthy + end) + | _ => maybe_warn_transfer no_quotient lthy + end; + + +(** typedef_bnf **) + +fun mk_typedef_transfer_tacs bnf_F bnf_G thms old_defs + map_raw rel_raw pred_raw sets_raw = let + + val live = live_of_bnf bnf_G; + val Abs_G_inverse = @{thm type_definition.Abs_inverse} OF [#typedef thms]; + val Rep_G = @{thm type_definition.Rep} OF [#typedef thms]; + + fun common_tac addefs tac = (fn _ => fn ctxt => + HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt addefs), + REPEAT_DETERM o rtac ctxt rel_funI, + SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply}), + REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE exE conjE}, + hyp_subst_tac ctxt]) THEN tac ctxt) + + fun map_tac ctxt = (HEADGOAL o EVERY') + [rtac ctxt @{thm relcomppI}, + etac ctxt (mk_rel_funDN (live+1) (map_transfer_of_bnf bnf_F)), + REPEAT_DETERM_N live o assume_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt [Abs_G_inverse OF [#map_closed thms] OF [Rep_G]]), + REPEAT_DETERM o rtac ctxt refl]; + val map_tac = common_tac [#map old_defs] map_tac; + + fun rel_tac ctxt = + HEADGOAL (etac ctxt (mk_rel_funDN (live+2) (rel_transfer_of_bnf bnf_F)) THEN' + REPEAT_DETERM_N (live+1) o assume_tac ctxt); + val rel_tac = common_tac (#rel old_defs :: @{thms vimage2p_def}) rel_tac; + + fun pred_tac ctxt = + HEADGOAL (etac ctxt (mk_rel_funDN (live+1) (pred_transfer_of_bnf bnf_F)) THEN' + REPEAT_DETERM_N live o (assume_tac ctxt)); + val pred_tac = common_tac [#pred old_defs] pred_tac; + + fun set_tac set_transfer_thm ctxt = + HEADGOAL (etac ctxt (rel_funD OF [set_transfer_thm])); + fun mk_set_tac set_def set_transfer = common_tac [set_def] (set_tac set_transfer); + val set_tacs = map2 mk_set_tac (#sets old_defs) (set_transfer_of_bnf bnf_F); + + in {map={raw=map_raw,tac=map_tac},rel={raw=rel_raw,tac=rel_tac}, + sets={raws=sets_raw,tacs=set_tacs},pred=SOME{raw=pred_raw,tac=pred_tac}} end; fun typedef_bnf thm wits specs map_b rel_b pred_b opts lthy = let val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) - |> the_default Plugin_Name.default_filter; - val no_warn_wits = exists (fn No_Warn_Wits => true | _ => false) opts; + |> the_default Plugin_Name.default_filter; (* extract Rep Abs F RepT AbsT *) - val (_, [Rep_G, Abs_G, F]) = Term.strip_comb (HOLogic.dest_Trueprop (Thm.prop_of thm)); + val (Rep_G, Abs_G, F) = strip3 thm; val typ_Abs_G = dest_funT (fastype_of Abs_G); val RepT = fst typ_Abs_G; (* F *) val AbsT = snd typ_Abs_G; (* G *) val AbsT_name = fst (dest_Type AbsT); val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar); val alpha0s = map (TFree o snd) specs; val _ = length tvs = length alpha0s orelse error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name); (* instantiate the new type variables newtvs to oldtvs *) val subst = subst_TVars (tvs ~~ alpha0s); val typ_subst = typ_subst_TVars (tvs ~~ alpha0s); val Rep_G = subst Rep_G; val Abs_G = subst Abs_G; val F = subst F; val RepT = typ_subst RepT; val AbsT = typ_subst AbsT; fun flatten_tyargs Ass = map dest_TFree alpha0s - |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass); + |> filter (fn T => exists (fn Ts => member op= Ts T) Ass); val Ds0 = filter (is_none o fst) specs |> map snd; (* get the bnf for RepT *) - val ((bnf, (deads, alphas)),((_, unfolds), lthy)) = + val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) = bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs [] Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy); val set_bs = map (fn T => find_index (fn U => T = U) alpha0s) alphas |> map (the_default Binding.empty o fst o nth specs); val _ = (case alphas of [] => error "No live variables" | _ => ()); val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds @ #pred_unfolds unfolds; (* number of live variables *) - val lives = length alphas; + val live = length alphas; (* state the three required properties *) val sorts = map Type.sort_of_atyp alphas; val names_lthy = fold Variable.declare_typ (alphas @ deads) lthy; - val (alphas', names_lthy) = mk_TFrees' sorts names_lthy; - val (betas, names_lthy) = mk_TFrees' sorts names_lthy; + val (((alphas', betas), betas'), names_lthy) = names_lthy + |> mk_TFrees' sorts + ||>> mk_TFrees' sorts + ||>> mk_TFrees' sorts; - val map_F = mk_map_of_bnf deads alphas betas bnf; + val map_F = mk_map_of_bnf deads alphas betas bnf_F; - val (typ_fs, typ_aF) = fastype_of map_F |> strip_typeN lives ||> domain_type; + val (typ_fs, typ_aF) = fastype_of map_F |> strip_typeN live ||> domain_type; val typ_pairs = map HOLogic.mk_prodT (alphas ~~ alphas'); val typ_subst_pair = typ_subst_atomic (alphas ~~ typ_pairs); val typ_pair = typ_subst_pair RepT; - val subst_b = subst_atomic_types (alphas ~~ betas); val subst_a' = subst_atomic_types (alphas ~~ alphas'); val subst_pair = subst_atomic_types (alphas ~~ typ_pairs); val aF_set = F; - val bF_set = subst_b F; val aF_set' = subst_a' F; val pairF_set = subst_pair F; - val map_F_fst = mk_map_of_bnf deads typ_pairs alphas bnf; - val map_F_snd = mk_map_of_bnf deads typ_pairs alphas' bnf; + val bF_set = subst_b F; + val map_F_fst = mk_map_of_bnf deads typ_pairs alphas bnf_F; + val map_F_snd = mk_map_of_bnf deads typ_pairs alphas' bnf_F + val sets_F_pairs = mk_sets_of_bnf (replicate live deads) (replicate live typ_pairs) bnf_F val wits_F = mk_wits_of_bnf - (replicate (nwits_of_bnf bnf) deads) - (replicate (nwits_of_bnf bnf) alphas) bnf; + (replicate (nwits_of_bnf bnf_F) deads) + (replicate (nwits_of_bnf bnf_F) alphas) bnf_F; (* val map_closed_F = @{term "\f x. x \ F \ map_F f x \ F"}; *) val (var_fs, names_lthy) = mk_Frees "f" typ_fs names_lthy; val (var_x, names_lthy) = mk_Frees "x" [typ_aF] names_lthy |>> the_single; val mem_x = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_x, aF_set)); val map_f = list_comb (map_F, var_fs); val mem_map = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_f $ var_x, bF_set)); val imp_map = Logic.mk_implies (mem_x, mem_map); val map_closed_F = fold_rev Logic.all var_fs (Logic.all var_x imp_map); - (* val zip_closed_F = @{term "\z. map_F fst z \ F \ map_F snd z \ F \ z \ F"}; *) - val (var_zs, names_lthy) = mk_Frees "z" [typ_pair] names_lthy; + (* val zip_closed_F = + @{term "\z. \map_F fst z \ F; map_F snd z \ F\ \ + \z' \ F. set_F z' \ set_F z \ map_F fst z' = map_F fst z \ map_F snd z' = map_F snd z"}; *) + val (var_z, names_lthy) = mk_Free "z" typ_pair names_lthy; + val (var_z', names_lthy) = mk_Free "z'" typ_pair names_lthy; val (pairs, names_lthy) = mk_Frees "tmp" typ_pairs names_lthy; - val var_z = hd var_zs; - val fsts = map (fst o Term.strip_comb o HOLogic.mk_fst) pairs; - val snds = map (fst o Term.strip_comb o HOLogic.mk_snd) pairs; - val map_fst = list_comb (list_comb (map_F_fst, fsts), var_zs); + + fun mk_map mfs f z = Term.list_comb (mfs, map (fst o Term.strip_comb o f) pairs) $ z; + fun mk_set var = map (fn t => t $ var) sets_F_pairs; + + val (map_fst', map_fst) = apply2 (mk_map map_F_fst HOLogic.mk_fst) (var_z', var_z); + val (map_snd', map_snd) = apply2 (mk_map map_F_snd HOLogic.mk_snd) (var_z', var_z); val mem_map_fst = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_fst, aF_set)); - val map_snd = list_comb (list_comb (map_F_snd, snds), var_zs); val mem_map_snd = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_snd, aF_set')); - val mem_z = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_z, pairF_set)); - val imp_zip = Logic.mk_implies (mem_map_fst, Logic.mk_implies (mem_map_snd, mem_z)); - val zip_closed_F = Logic.all var_z imp_zip; + val ex_conj = foldr1 HOLogic.mk_conj (map2 mk_leq (mk_set var_z') (mk_set var_z) @ + [HOLogic.mk_eq (map_fst', map_fst), HOLogic.mk_eq (map_snd', map_snd)]); + val zip_concl = HOLogic.mk_Trueprop (mk_Bex pairF_set (absfree (dest_Free var_z') ex_conj)); + val zip_closed_F = Logic.all var_z (Logic.list_implies ([mem_map_fst, mem_map_snd], zip_concl)); (* val wit_closed_F = @{term "wit_F a \ F"}; *) val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy; val (var_bs, _) = mk_Frees "a" alphas names_lthy; - fun binder_types_until_eq V T = - let - fun strip (TU as Type ("fun", [T, U])) = if V = TU then [] else T :: strip U - | strip T = if V = T then [] else - error ("Bad type for witness: " ^ quote (Syntax.string_of_typ lthy T)); - in strip T end; - val Iwits = the_default wits_F (Option.map (map (`(map (fn T => - find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits); + val sets = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; + val (Iwits, wit_goals) = + prepare_wits false RepT wits opts alphas wits_F var_as var_bs sets lthy; val wit_closed_Fs = Iwits |> map (fn (I, wit_F) => let val vars = map (nth var_as) I; val wit_a = list_comb (wit_F, vars); in fold_rev Logic.all vars (HOLogic.mk_Trueprop (HOLogic.mk_mem (wit_a, aF_set))) end); - val mk_wit_goals = mk_wit_goals var_as var_bs - (mk_sets_of_bnf (replicate lives deads) (replicate lives alphas) bnf); - val goals = [map_closed_F, zip_closed_F] @ wit_closed_Fs @ - (case wits of NONE => [] | _ => maps mk_wit_goals Iwits); - - val lost_wits = filter_out (fn (J, _) => exists (fn (I, _) => I = J) Iwits) wits_F; - val _ = - if null lost_wits orelse no_warn_wits then () - else - lost_wits - |> map (Syntax.pretty_typ lthy o fastype_of o snd) - |> Pretty.big_list - "The following types of nonemptiness witnesses of the raw type's BNF were lost:" - |> (fn pt => Pretty.chunks [pt, - Pretty.para "You can specify a liftable witness (e.g., a term of one of the above types\ - \ that satisfies the typedef's invariant)\ - \ using the annotation [wits: ]."]) - |> Pretty.string_of - |> warning; + (case wits of NONE => [] | _ => wit_goals); fun after_qed ([map_closed_thm] :: [zip_closed_thm] :: wit_thmss) lthy = let val (wit_closed_thms, wit_thms) = (case wits of - NONE => (map the_single wit_thmss, wit_thms_of_bnf bnf) + NONE => (map the_single wit_thmss, wit_thms_of_bnf bnf_F) | _ => chop (length wit_closed_Fs) (map the_single wit_thmss)) (* construct map set bd rel wit *) (* val map_G = @{term "\f. Abs_G o map_F f o Rep_G"}; *) val Abs_Gb = subst_b Abs_G; - val map_G = - fold_rev HOLogic.tupled_lambda var_fs + val map_G = fold_rev lambda var_fs (HOLogic.mk_comp (HOLogic.mk_comp (Abs_Gb, map_f), Rep_G)); + val map_raw = fold_rev lambda var_fs map_f; (* val sets_G = [@{term "set_F o Rep_G"}]; *) - val sets_F = mk_sets_of_bnf (replicate lives deads) (replicate lives alphas) bnf; + val sets_F = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; val sets_G = map (fn set_F => HOLogic.mk_comp (set_F, Rep_G)) sets_F; (* val bd_G = @{term "bd_F"}; *) - val bd_F = mk_bd_of_bnf deads alphas bnf; + val bd_F = mk_bd_of_bnf deads alphas bnf_F; val bd_G = bd_F; (* val rel_G = @{term "\R. BNF_Def.vimage2p Rep_G Rep_G (rel_F R)"}; *) - val rel_F = mk_rel_of_bnf deads alphas betas bnf; - val (typ_Rs, _) = strip_typeN lives (fastype_of rel_F); + val rel_F = mk_rel_of_bnf deads alphas betas bnf_F; + val (typ_Rs, _) = strip_typeN live (fastype_of rel_F); val (var_Rs, names_lthy) = mk_Frees "R" typ_Rs lthy; val Rep_Gb = subst_b Rep_G; val rel_G = fold_rev absfree (map dest_Free var_Rs) (mk_vimage2p Rep_G Rep_Gb $ list_comb (rel_F, var_Rs)); + val rel_raw = fold_rev absfree (map dest_Free var_Rs) (list_comb (rel_F, var_Rs)); (* val pred_G = @{term "\P. pred_F P o Rep_G"}; *) - val pred_F = mk_pred_of_bnf deads alphas bnf; - val (typ_Ps, _) = strip_typeN lives (fastype_of pred_F); + val pred_F = mk_pred_of_bnf deads alphas bnf_F; + val (typ_Ps, _) = strip_typeN live (fastype_of pred_F); val (var_Ps, names_lthy) = mk_Frees "P" typ_Ps names_lthy; val pred_G = fold_rev absfree (map dest_Free var_Ps) (HOLogic.mk_comp (list_comb (pred_F, var_Ps), Rep_G)); + val pred_raw = fold_rev absfree (map dest_Free var_Ps) (list_comb (pred_F, var_Ps)); (* val wits_G = [@{term "Abs_G o wit_F"}]; *) val (var_as, _) = mk_Frees "a" alphas names_lthy; val wits_G = map (fn (I, wit_F) => let val vs = map (nth var_as) I; in fold_rev absfree (map dest_Free vs) (Abs_G $ (list_comb (wit_F, vs))) end) Iwits; (* tactics *) val Rep_thm = thm RS @{thm type_definition.Rep}; val Abs_inverse_thm = thm RS @{thm type_definition.Abs_inverse}; val Abs_inject_thm = thm RS @{thm type_definition.Abs_inject}; val Rep_cases_thm = thm RS @{thm type_definition.Rep_cases}; val Rep_inverse_thm = thm RS @{thm type_definition.Rep_inverse}; fun map_id0_tac ctxt = HEADGOAL (EVERY' [rtac ctxt ext, - SELECT_GOAL (unfold_thms_tac ctxt [map_id0_of_bnf bnf, id_apply, o_apply, + SELECT_GOAL (unfold_thms_tac ctxt [map_id0_of_bnf bnf_F, id_apply, o_apply, Rep_inverse_thm]), rtac ctxt refl]); fun map_comp0_tac ctxt = HEADGOAL (EVERY' [rtac ctxt ext, - SELECT_GOAL (unfold_thms_tac ctxt [map_comp0_of_bnf bnf, o_apply, + SELECT_GOAL (unfold_thms_tac ctxt [map_comp0_of_bnf bnf_F, o_apply, Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]), rtac ctxt refl]); fun map_cong0_tac ctxt = HEADGOAL (EVERY' ([SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), rtac ctxt (([Rep_thm RS map_closed_thm, Rep_thm RS map_closed_thm] MRS Abs_inject_thm) RS iffD2), - rtac ctxt (map_cong0_of_bnf bnf)] @ replicate lives (Goal.assume_rule_tac ctxt))); + rtac ctxt (map_cong0_of_bnf bnf_F)] @ replicate live (Goal.assume_rule_tac ctxt))); val set_map0s_tac = map (fn set_map => fn ctxt => HEADGOAL (EVERY' [rtac ctxt ext, SELECT_GOAL (unfold_thms_tac ctxt [set_map, o_apply, Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]), rtac ctxt refl])) - (set_map_of_bnf bnf); + (set_map_of_bnf bnf_F); - fun card_order_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_card_order_of_bnf bnf)); + fun card_order_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_card_order_of_bnf bnf_F)); - fun cinfinite_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_cinfinite_of_bnf bnf)); + fun cinfinite_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_cinfinite_of_bnf bnf_F)); val set_bds_tac = map (fn set_bd => fn ctxt => HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), rtac ctxt set_bd])) - (set_bd_of_bnf bnf); + (set_bd_of_bnf bnf_F); fun le_rel_OO_tac ctxt = HEADGOAL (EVERY' [rtac ctxt @{thm vimage2p_relcompp_mono}, - rtac ctxt ((rel_OO_of_bnf bnf RS sym) RS @{thm ord_eq_le_trans}), + rtac ctxt ((rel_OO_of_bnf bnf_F RS sym) RS @{thm ord_eq_le_trans}), rtac ctxt @{thm order_refl}]); fun rel_OO_Grp_tac ctxt = HEADGOAL (EVERY' ([SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt ext))), SELECT_GOAL (unfold_thms_tac ctxt [@{thm OO_Grp_alt}, mem_Collect_eq, - o_apply, @{thm vimage2p_def}, in_rel_of_bnf bnf, Bex_def, mem_Collect_eq]), + o_apply, @{thm vimage2p_def}, in_rel_of_bnf bnf_F, Bex_def, mem_Collect_eq]), rtac ctxt iffI, - SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve0_tac [exE,conjE]))), - rtac ctxt (zip_closed_thm OF (replicate 2 (Rep_thm RSN (2, @{thm ssubst_mem}))) RS - Rep_cases_thm), + SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))), + forward_tac ctxt + [zip_closed_thm OF (replicate 2 (Rep_thm RSN (2, @{thm ssubst_mem})))], assume_tac ctxt, - assume_tac ctxt, + SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [bexE, conjE]))), + etac ctxt Rep_cases_thm, hyp_subst_tac ctxt, SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt exI))), rtac ctxt conjI] @ - replicate (lives - 1) (rtac ctxt conjI THEN' assume_tac ctxt) @ - [assume_tac ctxt, - SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt conjI))), - REPEAT_DETERM_N 2 o - etac ctxt (trans OF [iffD2 OF [Abs_inject_thm OF - [map_closed_thm OF [Rep_thm], Rep_thm]], Rep_inverse_thm]), - SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve0_tac [exE,conjE]))), + replicate live + (EVERY' [TRY o rtac ctxt conjI, etac ctxt @{thm order_trans}, assume_tac ctxt]) @ + [SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt conjI))), + REPEAT_DETERM_N 2 o EVERY' + [rtac ctxt (trans OF [iffD2 OF [Abs_inject_thm OF + [map_closed_thm OF [Rep_thm], Rep_thm]], Rep_inverse_thm]), + etac ctxt trans, assume_tac ctxt], + SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))), rtac ctxt exI, rtac ctxt conjI] @ - replicate (lives - 1) (rtac ctxt conjI THEN' assume_tac ctxt) @ + replicate (live-1) (rtac ctxt conjI THEN' assume_tac ctxt) @ [assume_tac ctxt, rtac ctxt conjI, REPEAT_DETERM_N 2 o EVERY' [rtac ctxt (iffD1 OF [Abs_inject_thm OF [map_closed_thm OF [Rep_thm], Rep_thm]]), etac ctxt (Rep_inverse_thm RS sym RSN (2, trans))]])); fun pred_set_tac ctxt = HEADGOAL (EVERY' - [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\f. f \ _"]} RS trans), + [rtac ctxt (pred_set_of_bnf bnf_F RS @{thm arg_cong[of _ _ "\f. f \ _"]} RS trans), SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]); fun wit_tac ctxt = HEADGOAL (EVERY' (map (fn thm => (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt (o_apply :: (wit_closed_thms RL [Abs_inverse_thm]))), dtac ctxt thm, assume_tac ctxt])) wit_thms)); val tactics = [map_id0_tac, map_comp0_tac, map_cong0_tac] @ set_map0s_tac @ [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @ [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac]; - val (bnf, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I + val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I tactics wit_tac NONE map_b rel_b pred_b set_bs (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G) lthy; - val (bnf, lthy) = - morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf + val old_defs = + {sets = set_defs_of_bnf bnf_G, map = map_def_of_bnf bnf_G, rel = rel_def_of_bnf bnf_G, + pred = pred_def_of_bnf bnf_G}; + + val unfold_morphism = Morphism.thm_morphism "BNF" (unfold_thms lthy defs); + val (bnf_G, lthy) = morph_bnf_defs unfold_morphism bnf_G |> (fn bnf => note_bnf_defs bnf lthy); + + val setup_lifting_thm = Typedef thm; + val quiet = exists (fn No_Warn_Transfer => true | _ => false) opts; + + val transfer_consts = mk_typedef_transfer_tacs bnf_F bnf_G + {map_closed=map_closed_thm,typedef=thm} old_defs map_raw rel_raw pred_raw sets_F; in - lthy |> BNF_Def.register_bnf plugins AbsT_name bnf + lthy |> BNF_Def.register_bnf plugins AbsT_name bnf_G |> + mk_transfer_thms quiet bnf_F bnf_G AbsT_name transfer_consts setup_lifting_thm + {abs=typ_subst_atomic (alphas ~~ alphas') AbsT, rep=RepT, Ds0=map TFree Ds0, + deads = deads, alphas=alphas, betas=alphas', gammas=betas, deltas=betas'} defs end | after_qed _ _ = raise Match; in (goals, after_qed, defs, lthy) end; -(* main commands *) +(** quotient_bnf **) + +fun mk_quotient_transfer_tacs bnf_F Tss live qthms thms set_F'_thmss old_defs + inst_REL_pos_distrI map_raw rel_raw sets_raw = let + + fun common_tac ctxt addefs = unfold_thms_tac ctxt (#REL qthms :: addefs) THEN + (REPEAT_DETERM o HEADGOAL) (rtac ctxt rel_funI); + + (* quotient.map_transfer tactic *) + val map_F_transfer = map_transfer_of_bnf bnf_F |> mk_rel_funDN (live+1); + fun map_transfer_q _ ctxt = + common_tac ctxt (#map old_defs :: @{thms o_def}) THEN + (HEADGOAL o EVERY') [REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE}, + rtac ctxt @{thm relcomppI[rotated]}, hyp_subst_tac ctxt THEN' EVERY' + (map (rtac ctxt) [#rel_abs qthms, #map_F_rsp thms, (#rep_abs_rsp qthms), (#reflp qthms)]), + hyp_subst_tac ctxt, rtac ctxt map_F_transfer, REPEAT_DETERM_N (live+1) o assume_tac ctxt]; + + (* quotient.rel_transfer tactic *) + val rel_F_maps = rel_map_of_bnf bnf_F; + val rel_F_map_iffD2s = map (fn thm => thm RS @{thm iffD2}) rel_F_maps; + fun inst_REL_pos_distrI_order_refls vs aTs bTs ctxt = inst_REL_pos_distrI live vs aTs bTs ctxt + OF (replicate (live+1) asm_rl @ replicate live @{thm order_refl}); + fun rel_transfer_q {Qs, Rs} ctxt = EVERY + [common_tac ctxt [#rel old_defs, @{thm vimage2p_def}], + HEADGOAL (rtac ctxt iffI), + (REPEAT_DETERM o ALLGOALS) + (eresolve_tac ctxt @{thms exE conjE relcomppE} ORELSE' hyp_subst_tac ctxt), + (HEADGOAL o EVERY') + [REPEAT_DETERM o dtac ctxt @{thm rel_fun_rel_OO1}, + rtac ctxt (inst_REL_pos_distrI 0 (map mk_conversep Qs) (#betas Tss) (#alphas Tss) ctxt), + rtac ctxt @{thm relcomppI}, + rtac ctxt (#symp qthms), + rtac ctxt (#map_F_rsp thms), + rtac ctxt (#rep_abs_rsp qthms), + rtac ctxt (#reflp qthms), + rtac ctxt @{thm relcomppI}, + rtac ctxt (rel_flip_of_bnf bnf_F RS @{thm iffD1}), + rtac ctxt (nth rel_F_map_iffD2s 0), + rtac ctxt (nth rel_F_map_iffD2s 1), + etac ctxt (#rel_monoD_rotated thms)], + (REPEAT_DETERM_N live o HEADGOAL o EVERY') + [rtac ctxt @{thm predicate2I}, + rtac ctxt @{thm conversepI}, + rtac ctxt @{thm Basic_BNFs.rel_sum_simps(4)[THEN iffD2]}, + etac ctxt @{thm conversepI}], + (HEADGOAL o EVERY') + [rtac ctxt (inst_REL_pos_distrI_order_refls Rs (#gammas Tss) (#deltas Tss) ctxt), + (SELECT_GOAL o REPEAT_DETERM o HEADGOAL) (etac ctxt @{thm relcomppI}), + rtac ctxt @{thm relcomppI[rotated]}, + rtac ctxt (#map_F_rsp thms), + rtac ctxt (#rep_abs_rsp qthms OF [#reflp qthms]), + SELECT_GOAL (unfold_thms_tac ctxt (@{thms rel_sum_simps} @ rel_F_maps)), + assume_tac ctxt], + (REPEAT_DETERM_N (2*live) o HEADGOAL) + (rtac ctxt @{thm rel_sum_eq2_nonempty} ORELSE' rtac ctxt @{thm rel_sum_eq3_nonempty}), + (REPEAT_DETERM_N live) + (unfold_thms_tac ctxt @{thms sum.rel_compp[symmetric] eq_OO} THEN + HEADGOAL (etac ctxt @{thm sum.rel_mono[OF order_refl]})), + (HEADGOAL o EVERY') + [(SELECT_GOAL o REPEAT_DETERM o HEADGOAL) (dtac ctxt @{thm rel_fun_rel_OO2}), + rtac ctxt (inst_REL_pos_distrI 0 Qs (#alphas Tss) (#betas Tss) ctxt), + rtac ctxt @{thm relcomppI}, + rtac ctxt (#reflp qthms), + rtac ctxt @{thm relcomppI}, + rtac ctxt (nth rel_F_map_iffD2s 0), + rtac ctxt (nth rel_F_map_iffD2s 1), + etac ctxt (#rel_monoD_rotated thms)], + (REPEAT_DETERM_N live o HEADGOAL o EVERY') + [rtac ctxt @{thm predicate2I}, rtac ctxt @{thm rel_sum.intros(2)}, assume_tac ctxt], + (HEADGOAL o EVERY') + [rtac ctxt + (inst_REL_pos_distrI_order_refls (map mk_conversep Rs) (#deltas Tss) (#gammas Tss) ctxt), + rtac ctxt @{thm relcomppI}, + etac ctxt (rotate_prems 1 (#transp qthms)), + rtac ctxt (#map_F_rsp thms), + rtac ctxt (#rep_abs_rsp qthms OF [#reflp qthms]), + etac ctxt @{thm relcomppI}, + rtac ctxt @{thm relcomppI}, + etac ctxt (#transp qthms), + rtac ctxt (#symp qthms), + rtac ctxt (#map_F_rsp thms), + rtac ctxt (#rep_abs_rsp qthms), + rtac ctxt (#reflp qthms), + rtac ctxt @{thm relcomppI[rotated]}, + rtac ctxt (#reflp qthms), + rtac ctxt (rel_flip_of_bnf bnf_F RS @{thm iffD1}), + rtac ctxt (nth rel_F_map_iffD2s 0), + rtac ctxt (nth rel_F_map_iffD2s 1), + etac ctxt (#rel_monoD_rotated thms)], + (REPEAT_DETERM_N live o HEADGOAL o EVERY') + [rtac ctxt @{thm predicate2I}, + rtac ctxt @{thm conversepI}, + rtac ctxt @{thm rel_sum.intros(2)}, + etac ctxt @{thm conversepI}], + (REPEAT_DETERM_N (2*live) o HEADGOAL) + (rtac ctxt @{thm rel_sum_eq2_nonempty} ORELSE' rtac ctxt @{thm rel_sum_eq3_nonempty}), + (REPEAT_DETERM_N live o EVERY) + [unfold_thms_tac ctxt @{thms sum.rel_compp[symmetric] eq_OO}, + HEADGOAL (etac ctxt @{thm sum.rel_mono[OF order_refl]})]]; + + (* quotient.set_transfer tactics *) + fun set_transfer_q set_G_def set_F'_thms _ ctxt = + let val set_F'_rsp = mk_rel_funDN 1 (#set_F'_respect set_F'_thms) in + common_tac ctxt (set_G_def :: @{thms o_def}) THEN + (HEADGOAL o EVERY') + [etac ctxt @{thm relcomppE}, hyp_subst_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt + [set_F'_rsp OF [#rep_abs qthms] OF [#reflp qthms], @{thm rel_set_def}]), + dtac ctxt (#rel_F_rel_F' thms), rtac ctxt conjI] THEN + (REPEAT_DETERM_N 2 o HEADGOAL o EVERY') + [SELECT_GOAL (unfold_thms_tac ctxt [#rel_F'_set thms]), + REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], + REPEAT_DETERM o dtac ctxt (mk_sym set_F'_rsp), + SELECT_GOAL (unfold_thms_tac ctxt [#set_map_F' set_F'_thms]), + rtac ctxt ballI, dtac ctxt @{thm equalityD1[THEN subsetD]}, assume_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt @{thms image_iff}), + etac ctxt bexE, dtac ctxt set_mp, assume_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt @{thms mem_Collect_eq case_prod_beta}), + rtac ctxt bexI, hyp_subst_tac ctxt, assume_tac ctxt, etac ctxt @{thm hypsubst}, + etac ctxt @{thm imageI}, assume_tac ctxt] + end; + in + {map={raw=map_raw, tac=map_transfer_q}, + rel={raw=rel_raw, tac=rel_transfer_q}, + sets={raws=sets_raw,tacs=map2 set_transfer_q (#sets old_defs) set_F'_thmss}, + pred=NONE} + end; + + +fun quotient_bnf {equiv_rel, equiv_thm, quot_thm, ...} _ wits specs map_b rel_b pred_b opts lthy = + let + (* extract rep_G and abs_G *) + val (_, abs_G, rep_G) = strip3 quot_thm; + val (repT, absT) = dest_funT (fastype_of abs_G); (* ("?'a F", "?'a G") *) + val absT_name = fst (dest_Type absT); + + val tvs = map (fst o dest_TVar) (snd (dest_Type absT)); + val _ = length tvs = length specs orelse + error ("Expected " ^ string_of_int (length tvs) ^ + " type argument" ^ (if (length tvs) = 1 then "" else "s") ^ " to " ^ quote absT_name); + + (* instantiate TVars *) + val alpha0s = map (TFree o snd) specs; + val typ_subst = typ_subst_TVars (tvs ~~ alpha0s); + val (repT, absT) = apply2 typ_subst (repT, absT); + + (* get the bnf for RepT *) + val Ds0 = filter (is_none o fst) specs |> map snd; + + fun flatten_tyargs Ass = + map dest_TFree alpha0s |> filter (fn T => exists (fn Ts => member op= Ts T) Ass); + + val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) = + bnf_of_typ true Dont_Inline (Binding.qualify true absT_name) flatten_tyargs + [] Ds0 repT ((empty_comp_cache, empty_unfolds), lthy); + val live = length alphas; + val _ = (if live = 0 then error "No live variables" else ()); + + val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds; + val set_bs = + map (fn T => find_index (fn U => T = U) alpha0s) alphas + |> map (the_default Binding.empty o fst o nth specs); + + (* create and instantiate all the needed type variables *) + val subst = subst_TVars (tvs ~~ alpha0s); + val (abs_G, rep_G) = apply2 subst (abs_G, rep_G); + + val sorts = map Type.sort_of_atyp alphas; + val (((betas, gammas), deltas), names_lthy) = fold Variable.declare_typ (alphas @ deads) lthy + |> mk_TFrees' sorts + ||>> mk_TFrees' sorts + ||>> mk_TFrees' sorts; + + fun subst_Ts tm Ts = subst_atomic_types (alphas ~~ Ts) tm; + val subst_b = subst_atomic_types (alphas ~~ betas); + val subst_Maybe = subst_atomic_types o map (swap o `mk_MaybeT); + val equiv_rel_a = subst equiv_rel; + val map_F = mk_map_of_bnf deads alphas betas bnf_F; + val rel_F_ab = mk_rel_of_bnf deads alphas betas bnf_F; + val rel_F_bc = mk_rel_of_bnf deads betas gammas bnf_F; + val rel_F_ac = mk_rel_of_bnf deads alphas gammas bnf_F; + val rel_F_option = mk_rel_of_bnf deads (map mk_MaybeT alphas) (map mk_MaybeT betas) bnf_F; + val sets_F = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; + val wits_F = mk_wits_of_bnf + (replicate (nwits_of_bnf bnf_F) deads) (replicate (nwits_of_bnf bnf_F) alphas) bnf_F; + + val (typ_fs, (typ_aF, typ_bF)) = strip_typeN live (fastype_of map_F) ||> dest_funT; + val typ_MaybeF = typ_subst_atomic (alphas ~~ map mk_MaybeT alphas) typ_aF; + val typ_a_sets = map HOLogic.mk_setT alphas; + val typ_pairs = map HOLogic.mk_prodT (alphas ~~ betas); + val typ_fs' = map (typ_subst_atomic (map (swap o `mk_MaybeT) betas)) typ_fs; + + (* create all the needed variables *) + val ((((((((((((((((((((((var_Ps, var_Qs), var_Rs), var_x), var_x'), var_y), var_y'), var_mx), + var_As), var_As'), var_Ss), var_Bs), var_as), var_as'), var_bs), var_bs'), var_R), var_fs), + var_fs'), var_gs), var_gs'), var_z), var_ts) = names_lthy + |> mk_Frees "Ps" (map2 mk_relT alphas betas) + ||>> mk_Frees "Qs" (map2 mk_relT betas gammas) + ||>> mk_Frees "Rs" (map2 mk_relT alphas gammas) + ||>> mk_Free "x" typ_aF + ||>> mk_Free "x'" typ_aF + ||>> mk_Free "y" typ_bF + ||>> mk_Free "y'" (typ_subst_atomic (alphas ~~ gammas) typ_aF) + ||>> mk_Free "mx" typ_MaybeF + ||>> mk_Frees "As" typ_a_sets + ||>> mk_Frees "As'" typ_a_sets + ||>> mk_Frees "Ss" (map HOLogic.mk_setT typ_a_sets) + ||>> mk_Frees "Bs" (map HOLogic.mk_setT betas) + ||>> mk_Frees "as" alphas + ||>> mk_Frees "as'" alphas + ||>> mk_Frees "bs" betas + ||>> mk_Frees "bs'" betas + ||>> mk_Free "R" (typ_aF --> typ_bF --> HOLogic.boolT) + ||>> mk_Frees "fs" typ_fs + ||>> mk_Frees "fs'" typ_fs' + ||>> mk_Frees "gs" typ_fs + ||>> mk_Frees "gs'" typ_fs' + ||>> mk_Free "z" (typ_subst_atomic (alphas ~~ typ_pairs) typ_aF) + ||>> mk_Frees "ts" typ_pairs + |> fst; + + (* create local definitions `b = tm` with n arguments *) + fun suffix tm s = (dest_Const tm |> fst |> Long_Name.base_name) ^ s; + fun define lthy b n tm = + let + val b = Binding.qualify true absT_name (Binding.qualified_name b); + val ((tm, (_, def)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd + |> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm))) + ||> `Local_Theory.close_target; + val phi = Proof_Context.export_morphism lthy_old lthy; + val tm = Term.subst_atomic_types + (map (`(Morphism.typ phi)) (alphas @ betas @ gammas @ map TFree Ds0)) + (Morphism.term phi tm); + val def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def)); + in ({def=def, tm=tm}, lthy) end; + + (* internally use REL, not the user-provided definition *) + val (REL, lthy) = define lthy "REL" 0 equiv_rel_a; + val REL_def = sym RS eq_reflection OF [#def REL]; + fun REL_rewr_all ctxt thm = Conv.fconv_rule + (Conv.top_conv (fn _ => Conv.try_conv (Conv.rewr_conv REL_def)) ctxt) thm; + + val equiv_rel_a' = equiv_rel_a; + val equiv_rel_a = #tm REL; + val (equiv_rel_b, equiv_rel_c) = apply2 (subst_Ts equiv_rel_a) (betas, gammas); + + (* map_F_respect: @{term "((=) ===> REL ===> REL) map_F map_F"} *) + val map_F_respect = HOLogic.mk_Trueprop (fold_rev mk_rel_fun (map2 (fn xT => fn yT => + HOLogic.eq_const (xT --> yT)) alphas betas @ [equiv_rel_a]) (equiv_rel_b) $ map_F $ map_F); + + (* rel_pos_distr: @{term "\A B. + A \\ B \ bot \ REL \\ rel_F A \\ REL \\ rel_F B \\ REL \ REL \\ rel_F (A \\ B) \\ REL"} *) + fun compp_not_bot comp aT cT = let + val T = mk_relT aT cT; + val mk_eq = HOLogic.eq_const T; + in HOLogic.mk_not (mk_eq $ comp $ bot_const T) end; + val ab_comps = map2 mk_relcompp var_Ps var_Qs; + val ne_comps = (@{map 3} compp_not_bot ab_comps alphas gammas); + val ab_prem = foldr1 HOLogic.mk_conj ne_comps; + + val REL_pos_distrI_tm = let + val le_relcomps = map2 mk_leq ab_comps var_Rs; + val assm = mk_OO [equiv_rel_a, list_comb (rel_F_ab, var_Ps), + equiv_rel_b, list_comb (rel_F_bc, var_Qs)] equiv_rel_c; + val concl = mk_OO [equiv_rel_a, list_comb (rel_F_ac, var_Rs)] equiv_rel_c; + in + mk_Trueprop_implies + ([assm $ var_x $ var_y'] @ ne_comps @ le_relcomps, concl $ var_x $ var_y') + end; + + val ab_concl = mk_leq + (mk_OO [list_comb (rel_F_ab, var_Ps), equiv_rel_b] (list_comb (rel_F_bc, var_Qs))) + (mk_OO [equiv_rel_a, list_comb (rel_F_ac, ab_comps)] (equiv_rel_c)); + val ab_imp = Logic.mk_implies (apply2 HOLogic.mk_Trueprop (ab_prem, ab_concl)); + val rel_pos_distr = fold_rev Logic.all (var_Ps @ var_Qs) ab_imp; + + (* {(x, y) . REL x y} *) + fun mk_rel_pairs rel = mk_case_prod (var_x, var_x') (rel $ var_x $ var_x') + val rel_pairs = mk_rel_pairs equiv_rel_a; + + (* rel_Inter: \S. \ S \ {}; \S \ {} \ \ + (\A\S. {(x, y). REL x y} `` {x. set_F x \ A}) \ {(x, y). REL x y} `` {x. set_F x \ \S} *) + fun rel_Inter_from_set_F (var_A, var_S) set_F = let + + val typ_aset = fastype_of var_A; + + (* \S *) + val inter_S = Inf_const typ_aset $ var_S; + + (* [S \ {}, \S \ {}] *) + fun not_empty x = let val ty = fastype_of x + in HOLogic.mk_not (HOLogic.mk_eq (x, bot_const ty)) end; + val prems = map (HOLogic.mk_Trueprop o not_empty) [var_S, inter_S]; + + (* {x. set_F x \ A} *) + val setF_sub_A = mk_in [var_A] [set_F] typ_aF; + + (* {x. set_F x \ \S} *) + val setF_sub_S = mk_in [inter_S] [set_F] typ_aF; + + val lhs = Inf_const (HOLogic.mk_setT typ_aF) $ (mk_image + (absfree (dest_Free var_A) (Image_const typ_aF $ rel_pairs $ setF_sub_A)) $ var_S); + val rhs = Image_const typ_aF $ rel_pairs $ setF_sub_S; + val concl = HOLogic.mk_Trueprop (mk_leq lhs rhs); + + in Logic.all var_S (Logic.list_implies (prems, concl)) end; + + val rel_Inters = map2 rel_Inter_from_set_F (var_As ~~ var_Ss) sets_F; + + (* map_F_Just = map_F Just *) + val map_F_Just = let + val option_tys = map mk_MaybeT alphas; + val somes = map Just_const alphas; + in list_comb (subst_atomic_types (betas ~~ option_tys) map_F, somes) end; + + fun mk_set_F'_tm typ_a set_F = + let + val typ_aset = HOLogic.mk_setT typ_a; + + (* set_F' x = (\y\{y. REL (map_F Just x) y}. UNION (set_F y) set_Maybe) *) + val sbind = mk_UNION (subst_Maybe alphas set_F $ var_mx) (set_Maybe_const typ_a); + val collection = HOLogic.Collect_const typ_MaybeF $ absfree (dest_Free var_mx) + (subst_Maybe alphas equiv_rel_a $ (map_F_Just $ var_x) $ var_mx); + val set_F'_tm = lambda var_x + (Inf_const typ_aset $ (mk_image (absfree (dest_Free var_mx) sbind) $ collection)); + in + set_F'_tm + end + + val sets = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F; + val sets' = map2 mk_set_F'_tm alphas sets; + + val (Iwits, wit_goals) = + prepare_wits true repT wits opts alphas wits_F var_as var_as' sets' lthy; + + val goals = map_F_respect :: rel_pos_distr :: rel_Inters @ + (case wits of NONE => [] | _ => wit_goals); + + val plugins = + get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |> + the_default Plugin_Name.default_filter; + + fun after_qed thmss lthy = + (case thmss of [map_F_respect_thm] :: [rel_pos_distr_thm0] :: thmss => + let + val equiv_thm' = REL_rewr_all lthy equiv_thm; + val rel_pos_distr_thm = + @{thm equivp_add_relconj} OF [equiv_thm', equiv_thm', rel_pos_distr_thm0]; + + val (rel_Inter_thms, wit_thmss) = apply2 (fn f => flat (f live thmss)) (take, drop); + val wit_thms = (case wit_thmss of + [] => wit_thms_of_bnf bnf_F + | _ => wit_thmss); + + (* construct map_G, sets_G, bd_G, rel_G and wits_G *) + + (* map_G f = abs_G o map_F f o rep_G *) + val map_G = fold_rev lambda var_fs (HOLogic.mk_comp (HOLogic.mk_comp + (subst_Ts abs_G betas, list_comb (map_F, var_fs)), rep_G)); + val map_raw = fold_rev lambda var_fs (list_comb (map_F, var_fs)) + |> subst_atomic_types (betas ~~ gammas); + + (* Define set_G and the three auxiliary definitions (set_F', F_in, F_in') *) + fun mk_set_G var_A set_F lthy = let + val typ_a = HOLogic.dest_setT (fastype_of var_A); + val set_F'_tm = mk_set_F'_tm typ_a set_F + + val (set_F', lthy) = define lthy (suffix set_F "'") 1 set_F'_tm; + + (* set_G = set_F' o rep_G *) + val set_G = HOLogic.mk_comp (#tm set_F', rep_G); + + (* F_in A = {x. set_F x \ A} *) + val F_in_tm = lambda var_A (mk_in [var_A] [set_F] typ_aF); + val (F_in, lthy) = define lthy (suffix set_F "_in") 1 F_in_tm; + + (* F_in' A = map_F Inr -` ({(x, y). REL x y} `` F_in (insert (Inl ()) (Inr ` A))) *) + val F_in' = lambda var_A (mk_vimage map_F_Just (Image_const typ_MaybeF $ + subst_Maybe alphas rel_pairs $ (subst_Maybe alphas (#tm F_in) $ mk_insert + (mk_Nothing typ_a) (mk_image (Just_const typ_a) $ var_A)))); + val (F_in', lthy) = define lthy (suffix set_F "_in'") 1 F_in'; + + in ((set_G, {set_F'=set_F', F_in=F_in, F_in'=F_in'}), lthy) end; + + val ((sets_G, set_F'_aux_defs), lthy) = + @{fold_map 2} mk_set_G var_As sets_F lthy |>> split_list; + + (* bd_G = bd_F *) + val bd_G = mk_bd_of_bnf deads alphas bnf_F; + + (* rel_F' A = + BNF_Def.vimage2p (map_F Just) (map_F Just) ((\) OO rel_F (rel_Maybe A) OO (\)) *) + val rel_Maybes = @{map 3} (fn v => fn aT => fn bT => rel_Maybe_const aT bT $ v); + val rel_F'_tm = let val equiv_equiv_rel_option = subst_Ts equiv_rel_a' o map mk_MaybeT in + mk_vimage2p map_F_Just (subst_atomic_types (alphas ~~ betas) map_F_Just) $ + mk_OO [equiv_equiv_rel_option alphas, list_comb (rel_F_option, rel_Maybes var_Ps alphas betas)] + (equiv_equiv_rel_option betas) end; + + val (rel_F', lthy) = + define lthy (suffix rel_F_ab "'") (live+2) (fold_rev lambda var_Ps rel_F'_tm); + + (* rel_G A = vimage2p rep_G rep_G (rel_F' A) *) + val rel_G = fold_rev lambda var_Ps (mk_vimage2p rep_G (subst_Ts rep_G betas) $ rel_F'_tm); + val rel_raw = fold_rev lambda var_Ps rel_F'_tm + |> subst_atomic_types (betas ~~ gammas); + + (* val wits_G = [abs_G o wit_F] *) + val wits_G = map (fn (I, wit) => let val vars = (map (fn n => nth var_as n) I) + in fold_rev lambda vars (abs_G $ list_comb (wit, vars)) end) Iwits; + + (* auxiliary lemmas *) + val bd_card_order = bd_card_order_of_bnf bnf_F; + val bd_cinfinite = bd_cinfinite_of_bnf bnf_F; + val in_rel = in_rel_of_bnf bnf_F; + val map_F_comp = map_comp_of_bnf bnf_F; + val map_F_comp0 = map_comp0_of_bnf bnf_F; + val map_F_cong = map_cong_of_bnf bnf_F; + val map_F_id0 = map_id0_of_bnf bnf_F; + val map_F_id = map_id_of_bnf bnf_F; + val rel_conversep = rel_conversep_of_bnf bnf_F; + val rel_Grp = rel_Grp_of_bnf bnf_F; + val rel_OO = rel_OO_of_bnf bnf_F; + val rel_map = rel_map_of_bnf bnf_F; + val rel_refl_strong = rel_refl_strong_of_bnf bnf_F; + val set_bd_thms = set_bd_of_bnf bnf_F; + val set_map_thms = set_map_of_bnf bnf_F; + + val rel_funD = mk_rel_funDN (live+1); + val map_F_rsp = (rel_funD map_F_respect_thm) OF (replicate live refl); + fun map_F_rsp_of tms ctxt = (infer_instantiate' ctxt (NONE :: NONE + :: map (SOME o Thm.cterm_of ctxt) tms) map_F_rsp) + + val qthms = let + fun equivp_THEN thm = REL_rewr_all lthy equiv_thm RS thm; + fun Quotient3_THEN thm = REL_rewr_all lthy quot_thm RS thm; + in + {abs_rep = Quotient3_THEN @{thm Quotient3_abs_rep}, + rel_abs = Quotient3_THEN @{thm Quotient3_rel_abs}, + rep_abs = Quotient3_THEN @{thm Quotient3_rep_abs}, + rep_reflp = Quotient3_THEN @{thm Quotient3_rep_reflp}, + rep_abs_rsp = Quotient3_THEN @{thm rep_abs_rsp}, + reflp = equivp_THEN @{thm equivp_reflp}, + symp = equivp_THEN @{thm equivp_symp}, + transp = equivp_THEN @{thm equivp_transp}, + REL = REL_def} + end; + + (* lemma REL_OO_REL_left: REL OO REL OO R = REL OO R *) + val REL_OO_REL_left_thm = let + val tm = mk_Trueprop_eq + (mk_OO [equiv_rel_a, equiv_rel_a] var_R, mk_relcompp equiv_rel_a var_R) + fun tac ctxt = HEADGOAL (EVERY' + [rtac ctxt ext, + rtac ctxt ext, + rtac ctxt iffI, + TWICE (etac ctxt @{thm relcomppE}), + rtac ctxt @{thm relcomppI}, + etac ctxt (#transp qthms), + TWICE (assume_tac ctxt), + etac ctxt @{thm relcomppE}, + etac ctxt @{thm relcomppI}, + rtac ctxt @{thm relcomppI}, + rtac ctxt (#reflp qthms), + assume_tac ctxt]); + in prove lthy [var_R] tm tac end; + + (* Generate theorems related to the setters *) + val map_F_fs = list_comb (map_F, var_fs); + + (* aset aset asetset bset typ_b typ_b *) + fun mk_set_F'_thmss (((((var_A, var_A'), var_S), var_B), var_b), var_b') + set_F {set_F', F_in, F_in'} rel_Inter_thm set_map_F_thm (idx, vf) = + let + val (var_f, var_fs') = case vf of + (f :: fs) => (f, fs) + | _ => error "won't happen"; + + val typ_a = fastype_of var_f |> dest_funT |> fst; + val typ_b = fastype_of var_b; + val (typ_asetset, typ_aset) = `HOLogic.mk_setT (fastype_of var_A); + + val map_F_fs_x = map_F_fs $ var_x; + + (* F_in'_mono: A \ B \ F_in' A \ F_in' B *) + val F_in'_mono_tm = mk_Trueprop_implies + ([mk_leq var_A var_A'], mk_leq (#tm F_in' $ var_A) (#tm F_in' $ var_A')); + fun F_in'_mono_tac ctxt = + unfold_thms_tac ctxt [#def F_in', #def F_in] THEN + HEADGOAL (EVERY' + [rtac ctxt subsetI, + etac ctxt vimageE, + etac ctxt @{thm ImageE}, + etac ctxt CollectE, + etac ctxt CollectE, + dtac ctxt @{thm case_prodD}, + hyp_subst_tac ctxt, + rtac ctxt (vimageI OF [refl]), + rtac ctxt @{thm ImageI}, + rtac ctxt CollectI, + rtac ctxt @{thm case_prodI}, + assume_tac ctxt ORELSE' rtac ctxt refl, + rtac ctxt CollectI, + etac ctxt subset_trans, + etac ctxt (@{thm insert_mono} OF [@{thm image_mono}])]); + val F_in'_mono_thm = prove lthy [var_A, var_A'] F_in'_mono_tm F_in'_mono_tac; + + (* F_in'_Inter: F_in' (\S) = (\A\S. F_in' A) *) + val F_in'_Inter_tm = mk_Trueprop_eq ((#tm F_in' $ (Inf_const typ_aset $ var_S)), + (Inf_const (HOLogic.mk_setT typ_aF) $ (mk_image (#tm F_in') $ var_S))); + fun F_in'_Inter_tac ctxt = + Local_Defs.unfold_tac ctxt [#def F_in', #def F_in] + THEN HEADGOAL (rtac ctxt (infer_instantiate' ctxt + [SOME (Thm.cterm_of ctxt (HOLogic.mk_eq (var_S, bot_const typ_asetset)))] @{thm case_split}) + THEN' EVERY' [ + hyp_subst_tac ctxt, + SELECT_GOAL + (unfold_thms_tac ctxt @{thms Inter_empty INT_empty UNIV_sum_unit_conv}), + rtac ctxt @{thm set_eqI}, + rtac ctxt iffI, + rtac ctxt UNIV_I, + rtac ctxt (vimageI OF [refl]), + rtac ctxt @{thm ImageI}, + rtac ctxt CollectI, + rtac ctxt @{thm case_prodI}, + rtac ctxt (#reflp qthms), + rtac ctxt CollectI, + rtac ctxt subset_UNIV, + etac ctxt @{thm exE[OF ex_in_conv[THEN iffD2]]}, + EqSubst.eqsubst_tac ctxt [0] @{thms image_INT[of _ UNIV _ id, simplified]}, + rtac ctxt @{thm inj_Inr}, + assume_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt @{thms INT_extend_simps vimage_INT[symmetric]}), + rtac ctxt @{thm arg_cong2[where f=vimage, OF refl]}, + rtac ctxt equalityI, + rtac ctxt subsetI, + rtac ctxt @{thm InterI}, + etac ctxt imageE, + etac ctxt @{thm ImageE}, + etac ctxt CollectE, + etac ctxt CollectE, + dtac ctxt @{thm case_prodD}, + hyp_subst_tac ctxt, + rtac ctxt @{thm ImageI[OF CollectI]}, + etac ctxt @{thm case_prodI} ORELSE' (SELECT_GOAL + (unfold_thms_tac ctxt @{thms prod.case}) THEN' rtac ctxt @{thm refl}), + rtac ctxt CollectI, + etac ctxt subset_trans, + etac ctxt @{thm INT_lower[OF imageI]}, + rtac ctxt (@{thm subset_trans} OF [asm_rl, rel_Inter_thm]), + K (unfold_thms_tac ctxt @{thms image_image}), + rtac ctxt subset_refl, + K (unfold_thms_tac ctxt @{thms INT_extend_simps ex_in_conv[symmetric]}), + rtac ctxt exI, + rtac ctxt imageI, + assume_tac ctxt, + rtac ctxt exI, + rtac ctxt @{thm InterI}, + etac ctxt imageE, + hyp_subst_tac ctxt, + rtac ctxt @{thm insertI1}]); + + val F_in'_Inter_thm = prove lthy [var_S] F_in'_Inter_tm F_in'_Inter_tac; + + (* set_F'_respect: (REL ===> (=)) set_F' set_F' *) + val set_F'_respect_tm = HOLogic.mk_Trueprop (mk_rel_fun equiv_rel_a + (HOLogic.eq_const typ_aset) $ #tm set_F' $ #tm set_F'); + fun set_F'_respect_tac ctxt = unfold_thms_tac ctxt (#def set_F' :: @{thms rel_fun_def}) + THEN HEADGOAL (EVERY' + [TWICE (rtac ctxt allI), + rtac ctxt impI, + dtac ctxt (map_F_rsp_of (map Just_const alphas) ctxt), + rtac ctxt @{thm INF_cong}, + rtac ctxt @{thm Collect_eqI}, + rtac ctxt iffI, + etac ctxt (#transp qthms OF [#symp qthms]), + assume_tac ctxt, + etac ctxt (#transp qthms), + assume_tac ctxt, + rtac ctxt refl]); + + (* F_in'_alt2: F_in' A = {x. set_F' x \ A} *) + val F_in'_alt2_tm = mk_Trueprop_eq + (#tm F_in' $ var_A, mk_in [var_A] [#tm set_F'] typ_aF); + fun F_in'_alt2_tac ctxt = HEADGOAL (rtac ctxt equalityI THEN' + (Subgoal.FOCUS o K) (unfold_thms_tac ctxt (map #def [set_F', F_in', F_in])) ctxt + THEN' EVERY' + [rtac ctxt subsetI, + rtac ctxt CollectI, + rtac ctxt subsetI, + dtac ctxt vimageD, + etac ctxt @{thm ImageE}, + etac ctxt CollectE, + etac ctxt CollectE, + dtac ctxt @{thm case_prodD}, + dtac ctxt @{thm InterD}, + rtac ctxt @{thm imageI[OF CollectI]}, + etac ctxt (#symp qthms), + etac ctxt @{thm UnionE}, + etac ctxt imageE, + hyp_subst_tac ctxt, + etac ctxt @{thm subset_lift_sum_unitD}, + etac ctxt @{thm setr.cases}, + hyp_subst_tac ctxt, + assume_tac ctxt]) + THEN unfold_thms_tac ctxt [#def set_F'] THEN + (HEADGOAL o EVERY') + [rtac ctxt subsetI, + etac ctxt CollectE, + etac ctxt (subsetD OF [F_in'_mono_thm]), + EqSubst.eqsubst_tac ctxt [0] [F_in'_Inter_thm], + rtac ctxt @{thm InterI}] THEN + REPEAT_DETERM (HEADGOAL (etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt)) THEN + (HEADGOAL o EVERY') + [etac ctxt CollectE, + SELECT_GOAL (unfold_thms_tac ctxt (map #def [F_in', F_in])), + rtac ctxt @{thm vimageI[OF refl]}, + rtac ctxt @{thm ImageI}, + rtac ctxt CollectI, + rtac ctxt @{thm case_prodI}, + etac ctxt (#symp qthms), + rtac ctxt CollectI, + rtac ctxt subsetI, + rtac ctxt @{thm sum_insert_Inl_unit}, + assume_tac ctxt, + hyp_subst_tac ctxt, + rtac ctxt imageI, + rtac ctxt @{thm UnionI}, + rtac ctxt imageI, + assume_tac ctxt, + rtac ctxt @{thm setr.intros[OF refl]}]; + val F_in'_alt2_thm = prove lthy [var_A] F_in'_alt2_tm F_in'_alt2_tac; + + (* set_F'_alt: set_F' x = \{A. x \ F_in' A} *) + val set_F'_alt_tm = mk_Trueprop_eq (#tm set_F' $ var_x, + Inf_const typ_aset $ mk_Collect (var_A, HOLogic.mk_mem (var_x, #tm F_in' $ var_A))); + fun set_F'_alt_tac ctxt = unfold_thms_tac ctxt [F_in'_alt2_thm] + THEN HEADGOAL (EVERY' + [rtac ctxt @{thm set_eqI}, + rtac ctxt iffI, + rtac ctxt @{thm InterI}, + etac ctxt CollectE, + etac ctxt CollectE, + dtac ctxt subsetD, + assume_tac ctxt, + assume_tac ctxt, + etac ctxt @{thm InterD}, + rtac ctxt CollectI, + rtac ctxt CollectI, + rtac ctxt subset_refl]); + val set_F'_alt_thm = prove lthy [var_x] set_F'_alt_tm set_F'_alt_tac; + + (* map_F_in_F_in'I: x \ F_in' B \ map_F f x \ F_in' (f ` B) *) + val map_F_in_F_in'I_tm = mk_Trueprop_implies ([HOLogic.mk_mem (var_x, #tm F_in' $ var_A')], + HOLogic.mk_mem (map_F_fs_x, subst_b (#tm F_in') $ (mk_image var_f $ var_A'))); + fun map_F_in_F_in'I_tac ctxt = + Local_Defs.unfold_tac ctxt ([#def F_in', #def F_in, Bex_def] @ @{thms vimage_def Image_iff}) THEN + HEADGOAL (EVERY' + [etac ctxt @{thm CollectE}, + etac ctxt exE, + etac ctxt conjE, + etac ctxt @{thm CollectE}, + etac ctxt @{thm CollectE}, + dtac ctxt @{thm case_prodD}, + rtac ctxt @{thm CollectI}, + rtac ctxt exI, + rtac ctxt @{thm conjI[rotated]}, + rtac ctxt @{thm CollectI}, + rtac ctxt @{thm case_prodI}, + dtac ctxt (map_F_rsp_of (map mk_Maybe_map var_fs) ctxt), + SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms o_def map_sum.simps})), + assume_tac ctxt, + rtac ctxt CollectI, + SELECT_GOAL (unfold_thms_tac ctxt set_map_thms), + etac ctxt @{thm image_map_sum_unit_subset}]); + val map_F_in_F_in'I_thm = + prove lthy (var_A' :: var_x :: var_fs) map_F_in_F_in'I_tm map_F_in_F_in'I_tac; + + (* REL_preimage_eq: C \ range f \ {} \ + {(a, b). REL a b} `` {x. set_F x \ f -` C} = + map_F f -` {(a, b). REL a b} `` {x. set_F x \ C} *) + val REL_preimage_eq_tm = mk_Trueprop_implies ([HOLogic.mk_not (HOLogic.mk_eq + (HOLogic.mk_binop @{const_name inf} (var_B, mk_image var_f $ HOLogic.mk_UNIV typ_a), + bot_const (HOLogic.mk_setT typ_b)))], HOLogic.mk_eq (Image_const typ_aF $ + rel_pairs $ mk_in [mk_vimage var_f var_B] [set_F] typ_aF, mk_vimage map_F_fs + (Image_const typ_bF $ subst_b rel_pairs $ mk_in [var_B] [subst_b set_F] typ_bF))); + + (* Bs \ range fs \ {} \ set_F xb \ Bs \ REL xb (map_F fs x) + \ x \ {(x, x'). REL x x'} `` {x. set_F x \ fs -` Bs} *) + fun subgoal_tac {context = ctxt, params, ...} = let + val (x, y) = case params of + [(_, x), _, (_, y)] => (x, y) + | _ => error "won't happen"; + val cond = HOLogic.mk_conj (apply2 HOLogic.mk_mem ((var_b, var_B), (var_b', var_B))); + + (* ["\x y. x \ B \ y \ B", "(Grp UNIV f_1)\\"] *) + val cvars = var_fs |> maps (fn f => let val fT = fastype_of f in + map (SOME o Thm.cterm_of ctxt) + [if f = var_f then + fold_rev lambda [var_b, var_b'] cond else HOLogic.eq_const (range_type fT), + mk_conversep (mk_Grp (HOLogic.mk_UNIV (domain_type fT)) f)] end); + val rel_pos_distr_thm_inst = infer_instantiate' ctxt (cvars @ [SOME y,SOME x]) + (@{thm predicate2D} OF [rel_pos_distr_thm]); + + (* GrpI[of "map_F f1 .. fN" x, OF refl CollectI, OF "B1 \ UNIV \ ... \ Bn \ UNIV"] *) + fun subset_UNIVs n = fold (fn a => fn b => conjI OF [a, b]) (replicate (n-1) + @{thm subset_UNIV}) @{thm subset_UNIV}; + val GrpI_inst = infer_instantiate' ctxt (map SOME [Thm.cterm_of ctxt map_F_fs, x]) + @{thm GrpI} OF [refl, CollectI] OF [subset_UNIVs live]; + + in EVERY [ + HEADGOAL (Method.insert_tac ctxt [rel_pos_distr_thm_inst]), + unfold_thms_tac ctxt [rel_conversep, rel_OO, rel_Grp], + HEADGOAL (etac ctxt @{thm meta_impE}), + REPEAT_DETERM_N (live-1) (HEADGOAL (rtac ctxt @{thm conjI[rotated]})), + REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm relcompp_mem_Grp_neq_bot} ORELSE' + rtac ctxt @{thm relcompp_eq_Grp_neq_bot})), + HEADGOAL (EVERY' [etac ctxt @{thm meta_impE}, + rtac ctxt @{thm relcomppI}, + rtac ctxt (#reflp qthms), + rtac ctxt @{thm relcomppI}, + rtac ctxt rel_refl_strong]), + REPEAT_DETERM_N idx (HEADGOAL (rtac ctxt refl)), + HEADGOAL (rtac ctxt conjI THEN' TWICE (etac ctxt subsetD THEN' assume_tac ctxt)), + REPEAT_DETERM_N (live-idx-1) (HEADGOAL (rtac ctxt refl)), + HEADGOAL (EVERY' + [rtac ctxt @{thm relcomppI}, + assume_tac ctxt, + rtac ctxt @{thm relcomppI}, + rtac ctxt @{thm conversepI}, + rtac ctxt GrpI_inst, + rtac ctxt (#reflp qthms), + etac ctxt @{thm relcomppE}, + etac ctxt @{thm relcomppE}, + etac ctxt @{thm relcomppE}, + etac ctxt @{thm conversepE}, + etac ctxt @{thm GrpE}, + hyp_subst_tac ctxt, + rtac ctxt @{thm ImageI}, + rtac ctxt CollectI, + rtac ctxt @{thm case_prodI}, + assume_tac ctxt, + EqSubst.eqsubst_asm_tac ctxt [1] rel_map, + EqSubst.eqsubst_asm_tac ctxt [1] [in_rel_of_bnf bnf_F], + etac ctxt exE, + etac ctxt CollectE, + etac ctxt conjE, + etac ctxt conjE, + etac ctxt CollectE, + hyp_subst_tac ctxt, + rtac ctxt CollectI]), + unfold_thms_tac ctxt set_map_thms, + HEADGOAL (rtac ctxt (subsetI OF [vimageI] OF [refl]) THEN' + etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt), + REPEAT_DETERM_N 6 (HEADGOAL (etac ctxt Drule.thin_rl)), + REPEAT_DETERM_N (live-1) (HEADGOAL (etac ctxt conjE)), + HEADGOAL (EVERY' [dtac ctxt subsetD, assume_tac ctxt, etac ctxt CollectE]), + unfold_thms_tac ctxt @{thms split_beta}, + HEADGOAL (etac ctxt conjunct2)] end; + + fun REL_preimage_eq_tac ctxt = HEADGOAL (EVERY' + [rtac ctxt @{thm set_eqI}, + rtac ctxt iffI, + etac ctxt @{thm ImageE}, + etac ctxt CollectE, + etac ctxt CollectE, + dtac ctxt @{thm case_prodD}, + rtac ctxt (vimageI OF [refl]), + rtac ctxt @{thm ImageI}, + rtac ctxt CollectI, + rtac ctxt @{thm case_prodI}, + etac ctxt map_F_rsp, + rtac ctxt CollectI, + EqSubst.eqsubst_tac ctxt [0] [set_map_F_thm], + etac ctxt @{thm subset_vimage_image_subset}, + etac ctxt vimageE, + etac ctxt @{thm ImageE}, + TWICE (etac ctxt CollectE), + dtac ctxt @{thm case_prodD}, + hyp_subst_tac ctxt, + Subgoal.FOCUS_PARAMS subgoal_tac ctxt]); + + val REL_preimage_eq_thm = prove lthy (var_B :: var_fs) REL_preimage_eq_tm REL_preimage_eq_tac; + + (* set_map_F': set_F' (map_F f x) = f ` set_F' x *) + val set_map_F'_tm = mk_Trueprop_eq (subst_b (#tm set_F') + $ map_F_fs_x, mk_image var_f $ (#tm set_F' $ var_x)); + fun set_map_F'_tac ctxt = HEADGOAL (EVERY' + [rtac ctxt @{thm set_eqI}, + rtac ctxt iffI, + EqSubst.eqsubst_asm_tac ctxt [0] [set_F'_alt_thm], + etac ctxt @{thm InterD}, + rtac ctxt CollectI, + rtac ctxt map_F_in_F_in'I_thm, + SELECT_GOAL (unfold_thms_tac ctxt [F_in'_alt2_thm]), + rtac ctxt CollectI, + rtac ctxt subset_refl, + SELECT_GOAL (unfold_thms_tac ctxt [set_F'_alt_thm]), + rtac ctxt @{thm InterI}, + etac ctxt imageE, + etac ctxt CollectE, + hyp_subst_tac ctxt, + etac ctxt @{thm vimageD[OF InterD]}, + rtac ctxt CollectI]) THEN + (* map_F f x \ F_in' X \ x \ F_in' (f -` X) *) + HEADGOAL (Subgoal.FOCUS_PARAMS (fn {context = ctxt, params, ...} => + let + val X = nth params 1 |> snd |> Thm.term_of; + val Inr_img = mk_image (Just_const (HOLogic.dest_setT (fastype_of X))) $ X; + fun cvars_of ctxt = map (SOME o Thm.cterm_of ctxt); + val cut_thm = infer_instantiate' ctxt (cvars_of ctxt [Inr_img, var_f]) + @{thm insert_Inl_int_map_sum_unit}; + val preimage_thm = infer_instantiate' ctxt (cvars_of ctxt + (filter (fn f => var_f <> f) var_fs |> map mk_Maybe_map)) + (cut_thm RS REL_preimage_eq_thm); + in EVERY [ + unfold_thms_tac ctxt (map #def [F_in', F_in] @ preimage_thm :: map_F_comp :: + @{thms lift_sum_unit_vimage_commute vimage_comp o_def map_sum.simps}), + unfold_thms_tac ctxt [@{thm o_def[symmetric]}, map_F_comp0], + Local_Defs.fold_tac ctxt @{thms vimage_comp}, + HEADGOAL (etac ctxt (vimageI OF [refl]))] end) ctxt); + + (* set_F'_subset: set_F' x \ set_F x *) + val set_F'_subset_tm = HOLogic.mk_Trueprop (mk_leq (#tm set_F' $ var_x) (set_F $ var_x)); + fun set_F'_subset_tac ctxt = + let val int_e_thm = infer_instantiate' ctxt + (replicate 3 NONE @ [SOME (Thm.cterm_of ctxt (map_F_Just $ var_x))]) @{thm INT_E}; + in HEADGOAL (EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [#def set_F']), + rtac ctxt subsetI, + etac ctxt int_e_thm, + SELECT_GOAL (unfold_thms_tac ctxt [set_map_F_thm]), + etac ctxt @{thm UN_E}, + etac ctxt imageE, + hyp_subst_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt @{thms sum_set_simps singleton_iff}), + hyp_subst_tac ctxt, + assume_tac ctxt, + etac ctxt notE, + rtac ctxt CollectI, + rtac ctxt (#reflp qthms)]) + end; + in + ({F_in'_mono = F_in'_mono_thm, + F_in'_Inter = F_in'_Inter_thm, + set_F'_respect = prove lthy [] set_F'_respect_tm set_F'_respect_tac, + F_in'_alt2 = F_in'_alt2_thm, + set_F'_alt = set_F'_alt_thm, + map_F_in_F_in'I = map_F_in_F_in'I_thm, + set_map_F' = prove lthy (var_x :: var_fs) set_map_F'_tm set_map_F'_tac, + set_F'_subset = prove lthy [var_x] set_F'_subset_tm set_F'_subset_tac, + set_F'_def = #def set_F', + F_in_def = #def F_in, + F_in'_def = #def F_in'}, (idx + 1, var_fs')) + end; + + val set_F'_thmss = @{fold_map 5} mk_set_F'_thmss + (var_As ~~ var_As' ~~ var_Ss ~~ var_Bs ~~ var_bs ~~ var_bs') sets_F set_F'_aux_defs + rel_Inter_thms set_map_thms (0, var_fs) + |> fst; + + (* F_in'D: x \ F_in' A \ \a\A. f a = g a \ REL (map_F f x) (map_F g x) *) + fun rel_map_F_fs_map_F_gs subst fs gs = subst equiv_rel_b $ + (list_comb (subst map_F, fs) $ var_x) $ (list_comb (subst map_F, gs) $ var_x); + val F_in'D_thm = let + fun mk_prem var_a var_Aset {F_in', ...} var_f var_g = + [HOLogic.mk_mem (var_x, #tm F_in' $ var_Aset), mk_Ball var_Aset + ((absfree (dest_Free var_a)) (HOLogic.mk_eq (var_f $ var_a, var_g $ var_a)))]; + val prems = @{map 5} mk_prem var_as var_As set_F'_aux_defs var_fs' var_gs'; + val F_in'D_tm = mk_Trueprop_implies (flat prems, + rel_map_F_fs_map_F_gs (subst_Maybe betas) var_fs' var_gs'); + + fun map_F_rsp_of_case_sums fs ctxt = map_F_rsp_of + (@{map 2} (fn f => fn T => BNF_FP_Util.mk_case_sum + (Term.absdummy HOLogic.unitT (mk_Nothing T), f)) fs betas) ctxt; + + fun mk_var_fgs n = take n var_gs' @ drop n var_fs'; + fun F_in'D_tac ctxt = EVERY + (unfold_thms_tac ctxt + (maps (fn {F_in'_def, F_in_def, ...} => [F_in'_def, F_in_def]) set_F'_thmss) :: + map (REPEAT_DETERM_N live o HEADGOAL) + [etac ctxt vimageE, + etac ctxt @{thm ImageE}, + etac ctxt CollectE THEN' etac ctxt CollectE, + dtac ctxt @{thm case_prodD}] @ + HEADGOAL (hyp_subst_tac ctxt THEN' rotate_tac (~live)) :: + map (fn i => (HEADGOAL o EVERY') + [if i < live then rtac ctxt (#transp qthms) else K all_tac, + Ctr_Sugar_Tactics.select_prem_tac ctxt live (dresolve_tac ctxt [asm_rl]) i, + rtac ctxt (#transp qthms), + dtac ctxt (map_F_rsp_of_case_sums (mk_var_fgs (i-1)) ctxt), + SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms case_sum_o_inj(2)})), + etac ctxt (#symp qthms), + dtac ctxt (map_F_rsp_of_case_sums (mk_var_fgs i) ctxt), + SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms case_sum_o_inj(2)})), + EqSubst.eqsubst_tac ctxt [0] [map_F_cong OF replicate i refl @ asm_rl :: replicate (live-i) refl], + rtac ctxt @{thm sum.case_cong[OF refl refl]}, + etac ctxt bspec, + hyp_subst_tac ctxt, + etac ctxt @{thm subset_lift_sum_unitD}, + assume_tac ctxt, + assume_tac ctxt]) (1 upto live)); + + in prove lthy (var_x :: var_As @ var_fs' @ var_gs') F_in'D_tm F_in'D_tac end; + + (* map_F_cong': (\a. a \ set_F' x \ f a = g a) \ REL (map_F f x) (map_F g x) *) + val map_F_cong'_thm = let + fun mk_prem {set_F', ...} var_a var_f var_g = Logic.all var_a + (mk_Trueprop_implies ([HOLogic.mk_mem (var_a, #tm set_F' $ var_x)], + HOLogic.mk_eq (var_f $ var_a, var_g $ var_a))); + val map_F_cong'_tm = Logic.list_implies + (@{map 4} mk_prem set_F'_aux_defs var_as var_fs var_gs, HOLogic.mk_Trueprop + (rel_map_F_fs_map_F_gs I var_fs var_gs)); + fun Just_o_fun bT f = HOLogic.mk_comp (Just_const bT, f); + fun map_F_Just_o_funs fs = list_comb + (subst_Maybe betas map_F, map2 Just_o_fun betas fs) $ var_x; + fun map_F_cong'_tac ctxt = let + val map_F_respect_inst = map_F_rsp + |> infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) + (map map_F_Just_o_funs [var_fs, var_gs] @ map fromJust_const betas)) + |> Local_Defs.unfold ctxt (map_F_comp :: @{thms o_assoc + Fun.o_apply[where f=projr and g=Inr, unfolded sum.sel] id_def[symmetric]}) + |> Local_Defs.unfold ctxt @{thms id_comp}; + in + HEADGOAL (rtac ctxt map_F_respect_inst THEN' rtac ctxt F_in'D_thm) THEN + EVERY (map (fn {F_in'_alt2, ...} => + unfold_thms_tac ctxt [F_in'_alt2] THEN + HEADGOAL (EVERY' + [rtac ctxt CollectI, + rtac ctxt subset_refl, + rtac ctxt ballI, + SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), + rtac ctxt @{thm arg_cong[where f=Inr]}, + asm_full_simp_tac ctxt])) set_F'_thmss) end; + in prove lthy (var_x :: var_fs @ var_gs) map_F_cong'_tm map_F_cong'_tac end; + + (* rel_F'_set: "rel_F' P x y \ + (\z. set_F' z \ {(x, y). P x y} \ REL (map_F fst z) x \ REL (map_F snd z) y)" *) + val rel_F'_set_thm = let + val lhs = list_comb (#tm rel_F', var_Ps) $ var_x $ var_y; + fun mk_subset_A var_a var_b var_P {set_F', ...} = let + val collect_A = mk_case_prod (var_a, var_b) (var_P $ var_a $ var_b); + in mk_leq (subst_atomic_types (alphas ~~ typ_pairs) (#tm set_F') $ var_z) collect_A end; + val subset_As = @{map 4} mk_subset_A var_as var_bs var_Ps set_F'_aux_defs; + fun mk_map mfs f z = + Term.list_comb (mfs, map (fst o Term.strip_comb o f) var_ts) $ z; + val map_F_fst = mk_map_of_bnf deads typ_pairs alphas bnf_F; + val map_F_snd = mk_map_of_bnf deads typ_pairs betas bnf_F; + val map_fst = equiv_rel_a $ (mk_map map_F_fst HOLogic.mk_fst var_z) $ var_x; + val map_snd = equiv_rel_b $ (mk_map map_F_snd HOLogic.mk_snd var_z) $ var_y; + val rhs = let val (z, T) = dest_Free var_z in + HOLogic.mk_exists (z, T, fold_rev (fn a => fn b => HOLogic.mk_conj (a, b)) + (subset_As @ [map_fst]) map_snd) end; + val rel_F'_set_tm = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + + val maybePairsTs = map HOLogic.mk_prodT (map mk_MaybeT alphas ~~ map mk_MaybeT betas) + fun mk_map_prod_projr aT bT = let + val (mabT, (maT, mbT)) = `HOLogic.mk_prodT (apply2 mk_MaybeT (aT, bT)); + val map_prod_const = Const (@{const_name map_prod}, + (maT --> aT) --> (mbT --> bT) --> mabT --> HOLogic.mk_prodT (aT, bT)); + in map_prod_const $ fromJust_const aT $ fromJust_const bT end; + + fun exI_OF_tac ctxt tm = rtac ctxt + (infer_instantiate' ctxt (NONE :: [SOME (Thm.cterm_of ctxt tm)]) exI); + + (* REL (map_F Inr x) (map_F fst z) \ REL (map_F snd z) (map_F Inr y) \ + set_F z \ {(x, y). rel_sum (=) P x y} \ + \z. set_F' z \ {(x, y). P x y} \ REL (map_F fst z) x \ REL (map_F snd z) y *) + fun subgoal1_tac {context = ctxt, params, ...} = + let + val z = (case params of + (_ :: _ :: (_, ct) :: _) => Thm.term_of ct + | _ => error "won't happen"); + val map_F_projr_z = list_comb (mk_map_of_bnf deads maybePairsTs typ_pairs bnf_F, + map2 mk_map_prod_projr alphas betas) $ z; + in + HEADGOAL (exI_OF_tac ctxt map_F_projr_z) THEN + HEADGOAL (EVERY' (maps (fn {set_F'_subset, set_F'_respect, set_map_F', ...} => + [rtac ctxt conjI, + dtac ctxt (set_F'_subset RS @{thm order_trans}), + TWICE (dtac ctxt (set_F'_respect RS @{thm rel_funD})), + SELECT_GOAL (unfold_thms_tac ctxt [set_map_F']), + etac ctxt @{thm in_rel_sum_in_image_projr}, + TWICE (assume_tac ctxt)]) set_F'_thmss)) THEN + HEADGOAL (EVERY' (map (fn Ts => FIRST' + [dtac ctxt (map_F_rsp_of (map fromJust_const Ts) ctxt), + etac ctxt sym , assume_tac ctxt]) [alphas, betas])) THEN + unfold_thms_tac ctxt (map_F_comp :: + @{thms fst_comp_map_prod snd_comp_map_prod comp_projr_Inr} @ [map_F_id]) THEN + HEADGOAL (rtac ctxt conjI) THEN + HEADGOAL (etac ctxt (#symp qthms) THEN' assume_tac ctxt + ORELSE' (EVERY' (maps (fn Ts => + [dtac ctxt (map_F_rsp_of (map fromJust_const Ts) ctxt), + SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: + @{thms fst_comp_map_prod snd_comp_map_prod comp_projr_Inr} @ [map_F_id])), + assume_tac ctxt]) [alphas, betas]))) end; + + (* set_F' z \ {(x, y). P x y} \ REL (map_F fst z) x \ REL (map_F snd z) y \ + \b. REL (map_F Inr x) b \ (\ba. rel_F (rel_sum (=) P) b ba \ REL ba (map_F Inr y)) *) + fun subgoal2_tac {context = ctxt, params, ...} = let + val z = (case params of + ((_, ct) :: _) => Thm.term_of ct + | _ => error "won't happen"); + + fun exI_map_Ifs_tac mk_proj Ts = exI_OF_tac ctxt (list_comb + (mk_map_of_bnf deads typ_pairs (map mk_MaybeT Ts) bnf_F, @{map 3} + (fn var_t => fn {set_F', ...} => fn T => lambda var_t (BNF_FP_Util.mk_If + (HOLogic.mk_mem (var_t, subst_Ts (#tm set_F') typ_pairs $ z)) + (mk_Just (mk_proj var_t)) (mk_Nothing T))) var_ts set_F'_aux_defs Ts) $ z) + + fun mk_REL_trans_map_F n = (rotate_prems n (#transp qthms) OF + [rel_funD map_F_respect_thm] OF (replicate live refl @ [#symp qthms])); + in + HEADGOAL (EVERY' + [exI_map_Ifs_tac HOLogic.mk_fst alphas, + rtac ctxt conjI, + etac ctxt (mk_REL_trans_map_F 0)]) THEN + unfold_thms_tac ctxt [map_F_comp, @{thm o_def}] THEN + HEADGOAL (rtac ctxt map_F_cong'_thm) THEN + REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm if_P[symmetric]})) THEN + HEADGOAL (EVERY' [exI_map_Ifs_tac HOLogic.mk_snd betas, rtac ctxt conjI]) THEN + unfold_thms_tac ctxt rel_map THEN + HEADGOAL (rtac ctxt rel_refl_strong) THEN + REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm subset_rel_sumI})) THEN + HEADGOAL (etac ctxt (mk_REL_trans_map_F 1 OF [#symp qthms])) THEN + unfold_thms_tac ctxt [map_F_comp, @{thm o_def}] THEN + HEADGOAL (rtac ctxt map_F_cong'_thm) THEN + REPEAT_DETERM_N live (HEADGOAL (etac ctxt @{thm if_P})) end; + + fun rel_F'_set_tac ctxt = EVERY + ([unfold_thms_tac ctxt (#def rel_F' :: #REL qthms :: @{thms vimage2p_def relcompp_apply}), + HEADGOAL (rtac ctxt iffI), + (HEADGOAL o TWICE) (etac ctxt exE THEN' etac ctxt conjE), + HEADGOAL (EVERY' + [dtac ctxt (in_rel RS iffD1), + etac ctxt exE, + TWICE (etac ctxt conjE), + etac ctxt CollectE, + hyp_subst_tac ctxt]), + (REPEAT_DETERM_N (live-1) o HEADGOAL) (etac ctxt conjE), + HEADGOAL (Subgoal.FOCUS_PARAMS subgoal1_tac ctxt THEN' etac ctxt exE), + (REPEAT_DETERM_N (live+1) o HEADGOAL) (etac ctxt conjE), + HEADGOAL (Subgoal.FOCUS_PARAMS subgoal2_tac ctxt)]); + + in prove lthy (var_x :: var_y :: var_Ps) rel_F'_set_tm rel_F'_set_tac end; + + (* tactics *) + + (* map_G_id0: abs_G \ map_F id \ rep_G = id *) + fun map_G_id0_tac ctxt = HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt + [@{thm fun_eq_iff}, o_apply, map_F_id0, id_apply, #abs_rep qthms]), + rtac ctxt allI, rtac ctxt refl]); + + (* map_G (g \ f) = map_G g \ map_G f *) + fun map_G_comp0_tac ctxt = HEADGOAL (EVERY' [rtac ctxt ext, rtac ctxt sym, + SELECT_GOAL (unfold_thms_tac ctxt [o_apply, map_F_comp0]), rtac ctxt (#rel_abs qthms), + rtac ctxt map_F_rsp, rtac ctxt (#rep_abs qthms), rtac ctxt (#reflp qthms)]); + + (* map_G_cong: (\z. z \ set_G x \ f z = g z) \ map_G f x = map_G g x *) + fun map_G_cong_tac ctxt = EVERY + [Local_Defs.fold_tac ctxt (map #set_F'_def set_F'_thmss), + unfold_thms_tac ctxt [o_apply], + HEADGOAL (rtac ctxt (#rel_abs qthms) THEN' rtac ctxt map_F_cong'_thm), + REPEAT_DETERM_N live (HEADGOAL (asm_full_simp_tac ctxt))]; + + (* set_G_map0_G: set_G \ map_G f = f ` set_G *) + fun mk_set_G_map0_G_tac thms ctxt = + HEADGOAL (rtac ctxt ext) THEN + EVERY [unfold_thms_tac ctxt [o_apply], + Local_Defs.fold_tac ctxt [#set_F'_def thms]] THEN + HEADGOAL (EVERY' (map (rtac ctxt) + [trans OF [#set_map_F' thms RS sym, sym] RS sym, + @{thm rel_funD} OF [#set_F'_respect thms], + #rep_abs qthms, + map_F_rsp, + #rep_reflp qthms])); + + (* bd_card_order: card_order bd_F *) + fun bd_card_order_tac ctxt = HEADGOAL (rtac ctxt bd_card_order); + + (* bd_cinfinite: BNF_Cardinal_Arithmetic.cinfinite bd_F *) + fun bd_cinfinite_tac ctxt = HEADGOAL (rtac ctxt bd_cinfinite); + + (*target: ordLeq3 (card_of (set_F' (rep_G x_))) bd_F*) + fun mk_set_G_bd_tac thms set_bd_thm ctxt = EVERY + [Local_Defs.fold_tac ctxt [#set_F'_def thms], + unfold_thms_tac ctxt [o_apply], + HEADGOAL (rtac ctxt (@{thm ordLeq_transitive} OF + [@{thm card_of_mono1} OF [#set_F'_subset thms], set_bd_thm]))]; + + (* rel_compp: rel_G R OO rel_G S \ rel_G (R OO S) *) + fun rel_compp_tac ctxt = EVERY + [unfold_thms_tac ctxt [#REL qthms], + HEADGOAL (TWICE (rtac ctxt @{thm vimage2p_relcompp_mono})), + (unfold_thms_tac ctxt (REL_OO_REL_left_thm :: @{thms relcompp_assoc})), + (unfold_thms_tac ctxt [Local_Defs.unfold ctxt @{thms eq_OO} + (infer_instantiate' ctxt [HOLogic.eq_const HOLogic.unitT |> Thm.cterm_of ctxt |> SOME] + @{thm sum.rel_compp})]), + HEADGOAL (rtac ctxt rel_pos_distr_thm), + unfold_thms_tac ctxt + @{thms fun_eq_iff bot_apply bot_bool_def not_all eq_False not_not OO_def}, + REPEAT_DETERM (HEADGOAL (resolve_tac ctxt [exI, conjI, @{thm rel_sum.intros(1)}, refl]))]; + + (* rel_G R_ = (\x y. \z. set_G z \ {(x, y). R x y} \ map_G fst z = x \ map_G snd z = y) *) + fun rel_compp_Grp_tac ctxt = let + val _ = () + in EVERY [Local_Defs.fold_tac ctxt (@{thm Grp_def} :: map #set_F'_def set_F'_thmss), + unfold_thms_tac ctxt + [o_apply, @{thm mem_Collect_eq}, @{thm OO_Grp_alt}, @{thm vimage2p_def}], + Local_Defs.fold_tac ctxt [Local_Defs.unfold ctxt @{thms vimage2p_def} (#def rel_F')], + unfold_thms_tac ctxt [rel_F'_set_thm], + HEADGOAL (TWICE (rtac ctxt ext)), + HEADGOAL (rtac ctxt iffI), + REPEAT_DETERM (ALLGOALS (eresolve_tac ctxt [exE, conjE])), + HEADGOAL (rtac ctxt exI), + REPEAT_FIRST (resolve_tac ctxt [conjI]), + HEADGOAL (EVERY' (maps (fn {set_F'_respect, ...} => + [etac ctxt @{thm subset_trans[rotated]}, + rtac ctxt equalityD1, + rtac ctxt (@{thm rel_funD} OF [set_F'_respect]), + rtac ctxt (#rep_abs qthms), + rtac ctxt (#reflp qthms)]) set_F'_thmss)), + (HEADGOAL o TWICE o EVERY') + [rtac ctxt (trans OF [asm_rl, #abs_rep qthms]), + rtac ctxt (#rel_abs qthms), + etac ctxt (rotate_prems 1 (#transp qthms)), + rtac ctxt map_F_rsp, + rtac ctxt (#rep_abs qthms), + rtac ctxt (#reflp qthms) + ], + HEADGOAL (rtac ctxt exI THEN' rtac ctxt conjI), + (REPEAT_DETERM_N live o HEADGOAL o EVERY') + [assume_tac ctxt, rtac ctxt conjI], + (HEADGOAL o TWICE o EVERY') [ + hyp_subst_tac ctxt, + rtac ctxt (#rep_abs_rsp qthms), + rtac ctxt map_F_rsp, + rtac ctxt (#rep_reflp qthms)]] + end; + + fun pred_G_set_G_tac ctxt = HEADGOAL (rtac ctxt refl); + + val tactics = map_G_id0_tac :: map_G_comp0_tac :: map_G_cong_tac :: + map mk_set_G_map0_G_tac set_F'_thmss @ + bd_card_order_tac :: bd_cinfinite_tac :: + map2 mk_set_G_bd_tac set_F'_thmss set_bd_thms @ + rel_compp_tac :: rel_compp_Grp_tac :: [pred_G_set_G_tac]; + + fun mk_wit_tacs ({set_F'_def, set_F'_respect, ...} :: set_F'_thmss) (w :: ws) ctxt = + EVERY [unfold_thms_tac ctxt [@{thm o_def}, + set_F'_respect RS @{thm rel_funD} OF [#rep_abs qthms OF [(#reflp qthms)]]], + unfold_thms_tac ctxt [set_F'_def], + HEADGOAL (etac ctxt w)] + THEN mk_wit_tacs set_F'_thmss ws ctxt + | mk_wit_tacs [] ws ctxt = mk_wit_tacs set_F'_thmss ws ctxt + | mk_wit_tacs _ _ _ = all_tac; + + val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I + tactics (mk_wit_tacs [] wit_thms) NONE map_b rel_b pred_b set_bs + (((((((Binding.empty, absT), map_G), sets_G), bd_G), wits_G), SOME rel_G), NONE) lthy; + + val old_defs = + {sets = set_defs_of_bnf bnf_G, map = map_def_of_bnf bnf_G, rel = rel_def_of_bnf bnf_G}; + + val set_F'_defs = map (mk_abs_def o #set_F'_def) set_F'_thmss; + val unfold_morphism = Morphism.thm_morphism "BNF" + (unfold_thms lthy (defs @ #def REL :: set_F'_defs)); + val (bnf_G, lthy) = morph_bnf_defs unfold_morphism bnf_G + |> (fn bnf => note_bnf_defs bnf lthy); + + (* auxiliary lemmas transfer for transfer *) + val rel_monoD_rotated = rotate_prems ~1 (rel_mono_of_bnf bnf_F RS @{thm predicate2D}); + + val REL_pos_distrI = let + fun tac ctxt = EVERY + [HEADGOAL (dtac ctxt (rotate_prems ~1 (rel_pos_distr_thm RS @{thm predicate2D}))), + (REPEAT_DETERM o HEADGOAL) (rtac ctxt conjI ORELSE' assume_tac ctxt), + (REPEAT_DETERM o HEADGOAL) (etac ctxt @{thm relcomppE}), + HEADGOAL (dtac ctxt rel_monoD_rotated), + (REPEAT_DETERM o HEADGOAL) + (assume_tac ctxt ORELSE' rtac ctxt @{thm relcomppI})]; + in prove lthy (var_x :: var_y' :: var_Ps @ var_Qs @ var_Rs) REL_pos_distrI_tm tac end; + + val rel_F_rel_F' = let + val rel_F = mk_rel_of_bnf deads alphas betas bnf_F; + val rel_F_rel_F'_tm = (rel_F, #tm rel_F') + |> apply2 (fn R => HOLogic.mk_Trueprop (list_comb (R, var_Ps) $ var_x $ var_y)) + |> Logic.mk_implies; + fun rel_F_rel_F'_tac ctxt = EVERY + [HEADGOAL (dtac ctxt (in_rel_of_bnf bnf_F RS iffD1)), + unfold_thms_tac ctxt (rel_F'_set_thm :: @{thms mem_Collect_eq}), + (REPEAT_DETERM o HEADGOAL) (eresolve_tac ctxt [exE, conjE]), + HEADGOAL (rtac ctxt exI), + HEADGOAL (EVERY' (maps (fn thms => + [rtac ctxt conjI, + rtac ctxt subsetI, + dtac ctxt (set_mp OF [#set_F'_subset thms]), + dtac ctxt subsetD, + assume_tac ctxt, assume_tac ctxt]) set_F'_thmss)), + (REPEAT_DETERM o HEADGOAL) + (rtac ctxt conjI ORELSE' hyp_subst_tac ctxt THEN' rtac ctxt (#reflp qthms))] + in prove lthy (var_x :: var_y :: var_Ps) rel_F_rel_F'_tm rel_F_rel_F'_tac end; + + fun inst_REL_pos_distrI n vs aTs bTs ctxt = + infer_instantiate' ctxt (replicate n NONE @ (rel_Maybes vs aTs bTs + |> map (SOME o Thm.cterm_of ctxt))) REL_pos_distrI; + + val Tss = {abs = typ_subst_atomic (alphas ~~ betas) absT, rep = repT, Ds0 = map TFree Ds0, + deads = deads, alphas = alphas, betas = betas, gammas = gammas, deltas = deltas}; + + val thms = + {map_F_rsp = map_F_rsp, + rel_F'_def = #def rel_F', + rel_F_rel_F' = rel_F_rel_F', + rel_F'_set = rel_F'_set_thm, + rel_monoD_rotated = rel_monoD_rotated} + + val transfer_consts = mk_quotient_transfer_tacs bnf_F Tss live + qthms thms set_F'_thmss old_defs inst_REL_pos_distrI + map_raw rel_raw (map (#tm o #set_F') set_F'_aux_defs); + val quiet = exists (fn No_Warn_Transfer => true | _ => false) opts; + in + lthy |> BNF_Def.register_bnf plugins absT_name bnf_G |> + mk_transfer_thms quiet bnf_F bnf_G absT_name transfer_consts (Quotient equiv_thm) Tss + (defs @ #def REL :: set_F'_defs) + end + | _ => raise Match); + + in (goals, after_qed, #def REL :: defs, lthy) end; + + +(** main commands **) local fun prepare_common prepare_name prepare_sort prepare_term prepare_thm - (((((plugins, raw_specs), raw_Tname), raw_wits), xthm_opt), (map_b, rel_b, pred_b)) lthy = + (((((plugins, raw_specs), raw_absT_name), raw_wits), xthm_opt), (map_b, rel_b, pred_b)) lthy = let - val Tname = prepare_name lthy raw_Tname; + val absT_name = prepare_name lthy raw_absT_name; + val input_thm = (case xthm_opt of SOME xthm => prepare_thm lthy xthm - | NONE => Typedef.get_info lthy Tname |> hd |> snd |> #type_definition); + | NONE => Typedef.get_info lthy absT_name |> hd |> snd |> #type_definition); val wits = (Option.map o map) (prepare_term lthy) raw_wits; val specs = - map (apsnd (apsnd (the_default \<^sort>\type\ o Option.map (prepare_sort lthy)))) raw_specs; + map (apsnd (apsnd (the_default @{sort type} o Option.map (prepare_sort lthy)))) raw_specs; - val _ = - (case HOLogic.dest_Trueprop (Thm.prop_of input_thm) of - Const (\<^const_name>\type_definition\, _) $ _ $ _ $ _ => () - | _ => error "Unsupported type of a theorem: only type_definition is supported"); + val which_bnf = (case Quotient_Info.lookup_quotients lthy absT_name of + SOME qs => quotient_bnf qs + | _ => typedef_bnf); + in - typedef_bnf input_thm wits specs map_b rel_b pred_b plugins lthy + which_bnf input_thm wits specs map_b rel_b pred_b plugins lthy end; fun prepare_lift_bnf prepare_name prepare_sort prepare_term prepare_thm = (fn (goals, after_qed, definitions, lthy) => lthy |> Proof.theorem NONE after_qed (map (single o rpair []) goals) |> Proof.refine_singleton (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions))) |> Proof.refine_singleton (Method.primitive_text (K I))) oo prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME)); fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs = (fn (goals, after_qed, definitions, lthy) => lthy - |> after_qed (map2 (fn goal => fn tac => [Goal.prove lthy [] [] goal + |> after_qed (map2 (fn goal => fn tac => [Goal.prove_sorry lthy [] [] goal (fn (ctxtprems as {context = ctxt, prems = _}) => unfold_thms_tac ctxt definitions THEN tac ctxtprems)]) goals (tacs (length goals)))) oo prepare_common prepare_name prepare_typ prepare_sort prepare_thm; in val lift_bnf_cmd = prepare_lift_bnf (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms); fun lift_bnf args tacs = prepare_solve (K I) (K I) (K I) (K I) (K tacs) args; +fun copy_bnf_tac {context = ctxt, prems = _} = + REPEAT_DETERM (resolve_tac ctxt [bexI, conjI, UNIV_I, refl, subset_refl] 1); + val copy_bnf = apfst (apfst (rpair NONE)) #> prepare_solve (K I) (K I) (K I) (K I) - (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1)); + (fn n => replicate n copy_bnf_tac); val copy_bnf_cmd = apfst (apfst (rpair NONE)) #> prepare_solve (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms) - (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1)); + (fn n => replicate n copy_bnf_tac); end; - -(* outer syntax *) +(** outer syntax **) local +(* parsers *) + val parse_wits = - \<^keyword>\[\ |-- (Parse.name --| \<^keyword>\:\ -- Scan.repeat Parse.term >> + @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.term >> (fn ("wits", Ts) => Ts | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| - \<^keyword>\]\ || Scan.succeed []; + @{keyword "]"} || Scan.succeed []; -val parse_options = - Scan.optional (\<^keyword>\(\ |-- +fun parse_common_opts p = + Scan.optional (@{keyword "("} |-- Parse.list1 (Parse.group (K "option") - (Plugin_Name.parse_filter >> Plugins_Option - || Parse.reserved "no_warn_wits" >> K No_Warn_Wits)) - --| \<^keyword>\)\) []; + (Scan.first (p :: [Plugin_Name.parse_filter >> Plugins_Option, + Parse.reserved "no_warn_transfer" >> K No_Warn_Transfer]))) + --| @{keyword ")"}) []; -val parse_plugins = - Scan.optional (\<^keyword>\(\ |-- Plugin_Name.parse_filter --| \<^keyword>\)\) - (K Plugin_Name.default_filter) >> Plugins_Option >> single; +val parse_lift_opts = Parse.reserved "no_warn_wits" >> K No_Warn_Wits |> parse_common_opts; -val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.thm); +val parse_copy_opts = parse_common_opts Scan.fail; + +val parse_xthm = Scan.option (Parse.reserved "via" |-- Parse.thm); in -val _ = - Outer_Syntax.local_theory_to_proof \<^command_keyword>\lift_bnf\ - "register a subtype of a bounded natural functor (BNF) as a BNF" - ((parse_options -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits -- - parse_typedef_thm -- parse_map_rel_pred_bindings) >> lift_bnf_cmd); +(* exposed commands *) val _ = - Outer_Syntax.local_theory \<^command_keyword>\copy_bnf\ + Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf} + "register a quotient type/subtype of a bounded natural functor (BNF) as a BNF" + ((parse_lift_opts -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits -- + parse_xthm -- parse_map_rel_pred_bindings) >> lift_bnf_cmd); + +val _ = + Outer_Syntax.local_theory @{command_keyword copy_bnf} "register a type copy of a bounded natural functor (BNF) as a BNF" - ((parse_plugins -- parse_type_args_named_constrained -- Parse.type_const -- - parse_typedef_thm -- parse_map_rel_pred_bindings) >> copy_bnf_cmd); + ((parse_copy_opts -- parse_type_args_named_constrained -- Parse.type_const -- + parse_xthm -- parse_map_rel_pred_bindings) >> copy_bnf_cmd); end; end;