1(* Title: HOL/BNF_Composition.thy 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 Copyright 2012, 2013, 2014 5 6Composition of bounded natural functors. 7*) 8 9section \<open>Composition of Bounded Natural Functors\<close> 10 11theory BNF_Composition 12imports BNF_Def 13keywords 14 "copy_bnf" :: thy_decl and 15 "lift_bnf" :: thy_goal 16begin 17 18lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" 19 by simp 20 21lemma empty_natural: "(\<lambda>_. {}) \<circ> f = image g \<circ> (\<lambda>_. {})" 22 by (rule ext) simp 23 24lemma Union_natural: "Union \<circ> image (image f) = image f \<circ> Union" 25 by (rule ext) (auto simp only: comp_apply) 26 27lemma in_Union_o_assoc: "x \<in> (Union \<circ> gset \<circ> gmap) A \<Longrightarrow> x \<in> (Union \<circ> (gset \<circ> gmap)) A" 28 by (unfold comp_assoc) 29 30lemma comp_single_set_bd: 31 assumes fbd_Card_order: "Card_order fbd" and 32 fset_bd: "\<And>x. |fset x| \<le>o fbd" and 33 gset_bd: "\<And>x. |gset x| \<le>o gbd" 34 shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd" 35 apply simp 36 apply (rule ordLeq_transitive) 37 apply (rule card_of_UNION_Sigma) 38 apply (subst SIGMA_CSUM) 39 apply (rule ordLeq_transitive) 40 apply (rule card_of_Csum_Times') 41 apply (rule fbd_Card_order) 42 apply (rule ballI) 43 apply (rule fset_bd) 44 apply (rule ordLeq_transitive) 45 apply (rule cprod_mono1) 46 apply (rule gset_bd) 47 apply (rule ordIso_imp_ordLeq) 48 apply (rule ordIso_refl) 49 apply (rule Card_order_cprod) 50 done 51 52lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r" 53 apply (erule ordIso_transitive) 54 apply (frule csum_absorb2') 55 apply (erule ordLeq_refl) 56 by simp 57 58lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r" 59 apply (erule ordIso_transitive) 60 apply (rule cprod_infinite) 61 by simp 62 63lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)" 64 by simp 65 66lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A" 67 by simp 68 69lemma image_o_collect: "collect ((\<lambda>f. image g \<circ> f) ` F) = image g \<circ> collect F" 70 by (rule ext) (auto simp add: collect_def) 71 72lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" 73 by blast 74 75lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" 76 by blast 77 78lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd" 79 by (unfold comp_apply collect_def) simp 80 81lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q" 82 by blast 83 84lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)\<inverse>\<inverse> OO Grp (Collect (case_prod R)) snd = R" 85 unfolding Grp_def fun_eq_iff relcompp.simps by auto 86 87lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)\<inverse>\<inverse> OO Grp A g = (Grp B f)\<inverse>\<inverse> OO Grp B g" 88 by (rule arg_cong) 89 90lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow> 91 vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T" 92 unfolding vimage2p_def by auto 93 94lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f \<circ> M \<circ> g) x = (f \<circ> N \<circ> h) x" 95 by auto 96 97lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S \<circ> Rep) x| \<le>o bd" 98 by auto 99 100lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S" 101 by simp 102 103lemma Ball_comp_iff: "(\<lambda>x. Ball (A x) f) \<circ> g = (\<lambda>x. Ball ((A \<circ> g) x) f)" 104 unfolding o_def by auto 105 106lemma conj_comp_iff: "(\<lambda>x. P x \<and> Q x) \<circ> g = (\<lambda>x. (P \<circ> g) x \<and> (Q \<circ> g) x)" 107 unfolding o_def by auto 108 109context 110 fixes Rep Abs 111 assumes type_copy: "type_definition Rep Abs UNIV" 112begin 113 114lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs \<circ> M \<circ> Rep = id" 115 using type_definition.Rep_inverse[OF type_copy] by auto 116 117lemma type_copy_map_comp0: "M = M1 \<circ> M2 \<Longrightarrow> f \<circ> M \<circ> g = (f \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> g)" 118 using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto 119 120lemma type_copy_set_map0: "S \<circ> M = image f \<circ> S' \<Longrightarrow> (S \<circ> Rep) \<circ> (Abs \<circ> M \<circ> g) = image f \<circ> (S' \<circ> g)" 121 using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff) 122 123lemma type_copy_wit: "x \<in> (S \<circ> Rep) (Abs y) \<Longrightarrow> x \<in> S y" 124 using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto 125 126lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) = 127 Grp (Collect (\<lambda>x. P (f x))) (Abs \<circ> h \<circ> f)" 128 unfolding vimage2p_def Grp_def fun_eq_iff 129 by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] 130 type_definition.Rep_inverse[OF type_copy] dest: sym) 131 132lemma type_copy_vimage2p_Grp_Abs: 133 "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep \<circ> h \<circ> g)" 134 unfolding vimage2p_def Grp_def fun_eq_iff 135 by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] 136 type_definition.Rep_inverse[OF type_copy] dest: sym) 137 138lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))" 139proof safe 140 fix b assume "F b" 141 show "\<exists>b'. F (Rep b')" 142 proof (rule exI) 143 from \<open>F b\<close> show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto 144 qed 145qed blast 146 147lemma vimage2p_relcompp_converse: 148 "vimage2p f g (R\<inverse>\<inverse> OO S) = (vimage2p Rep f R)\<inverse>\<inverse> OO vimage2p Rep g S" 149 unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def 150 by (auto simp: type_copy_ex_RepI) 151 152end 153 154bnf DEADID: 'a 155 map: "id :: 'a \<Rightarrow> 'a" 156 bd: natLeq 157 rel: "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" 158 by (auto simp add: natLeq_card_order natLeq_cinfinite) 159 160definition id_bnf :: "'a \<Rightarrow> 'a" where 161 "id_bnf \<equiv> (\<lambda>x. x)" 162 163lemma id_bnf_apply: "id_bnf x = x" 164 unfolding id_bnf_def by simp 165 166bnf ID: 'a 167 map: "id_bnf :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 168 sets: "\<lambda>x. {x}" 169 bd: natLeq 170 rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" 171 pred: "id_bnf :: ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" 172 unfolding id_bnf_def 173 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) 174 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) 175 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] 176 done 177 178lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV" 179 unfolding id_bnf_def by unfold_locales auto 180 181ML_file "Tools/BNF/bnf_comp_tactics.ML" 182ML_file "Tools/BNF/bnf_comp.ML" 183ML_file "Tools/BNF/bnf_lift.ML" 184 185hide_fact 186 DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0 187 DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer 188 DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq 189 DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer 190 ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id 191 ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep 192 ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer 193 194end 195