1(* Title: HOL/BNF_Greatest_Fixpoint.thy 2 Author: Dmitriy Traytel, TU Muenchen 3 Author: Lorenz Panny, TU Muenchen 4 Author: Jasmin Blanchette, TU Muenchen 5 Copyright 2012, 2013, 2014 6 7Greatest fixpoint (codatatype) operation on bounded natural functors. 8*) 9 10section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close> 11 12theory BNF_Greatest_Fixpoint 13imports BNF_Fixpoint_Base String 14keywords 15 "codatatype" :: thy_decl and 16 "primcorecursive" :: thy_goal and 17 "primcorec" :: thy_decl 18begin 19 20alias proj = Equiv_Relations.proj 21 22lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 23 by simp 24 25lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" 26 by (cases s) auto 27 28lemma not_TrueE: "\<not> True \<Longrightarrow> P" 29 by (erule notE, rule TrueI) 30 31lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P" 32 by fast 33 34lemma converse_Times: "(A \<times> B)\<inverse> = B \<times> A" 35 by fast 36 37lemma equiv_proj: 38 assumes e: "equiv A R" and m: "z \<in> R" 39 shows "(proj R \<circ> fst) z = (proj R \<circ> snd) z" 40proof - 41 from m have z: "(fst z, snd z) \<in> R" by auto 42 with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" 43 unfolding equiv_def sym_def trans_def by blast+ 44 then show ?thesis unfolding proj_def[abs_def] by auto 45qed 46 47(* Operators: *) 48definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" 49 50lemma Id_on_Gr: "Id_on A = Gr A id" 51 unfolding Id_on_def Gr_def by auto 52 53lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g" 54 unfolding image2_def by auto 55 56lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b" 57 by auto 58 59lemma image2_Gr: "image2 A f g = (Gr A f)\<inverse> O (Gr A g)" 60 unfolding image2_def Gr_def by auto 61 62lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A" 63 unfolding Gr_def by simp 64 65lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx" 66 unfolding Gr_def by simp 67 68lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B" 69 unfolding Gr_def by auto 70 71lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" 72 by blast 73 74lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})" 75 by blast 76 77lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X" 78 unfolding fun_eq_iff by auto 79 80lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))" 81 by auto 82 83lemma Collect_case_prod_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R" 84 by force 85 86lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)" 87 unfolding fun_eq_iff by auto 88 89lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)" 90 unfolding fun_eq_iff by auto 91 92lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f" 93 unfolding Gr_def Grp_def fun_eq_iff by auto 94 95definition relImage where 96 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}" 97 98definition relInvImage where 99 "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}" 100 101lemma relImage_Gr: 102 "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)\<inverse> O R O Gr A f" 103 unfolding relImage_def Gr_def relcomp_def by auto 104 105lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)\<inverse>" 106 unfolding Gr_def relcomp_def image_def relInvImage_def by auto 107 108lemma relImage_mono: 109 "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f" 110 unfolding relImage_def by auto 111 112lemma relInvImage_mono: 113 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f" 114 unfolding relInvImage_def by auto 115 116lemma relInvImage_Id_on: 117 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id" 118 unfolding relInvImage_def Id_on_def by auto 119 120lemma relInvImage_UNIV_relImage: 121 "R \<subseteq> relInvImage UNIV (relImage R f) f" 122 unfolding relInvImage_def relImage_def by auto 123 124lemma relImage_proj: 125 assumes "equiv A R" 126 shows "relImage R (proj R) \<subseteq> Id_on (A//R)" 127 unfolding relImage_def Id_on_def 128 using proj_iff[OF assms] equiv_class_eq_iff[OF assms] 129 by (auto simp: proj_preserves) 130 131lemma relImage_relInvImage: 132 assumes "R \<subseteq> f ` A \<times> f ` A" 133 shows "relImage (relInvImage A R f) f = R" 134 using assms unfolding relImage_def relInvImage_def by fast 135 136lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)" 137 by simp 138 139lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp 140lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp 141 142lemma fst_diag_fst: "fst \<circ> ((\<lambda>x. (x, x)) \<circ> fst) = fst" by auto 143lemma snd_diag_fst: "snd \<circ> ((\<lambda>x. (x, x)) \<circ> fst) = fst" by auto 144lemma fst_diag_snd: "fst \<circ> ((\<lambda>x. (x, x)) \<circ> snd) = snd" by auto 145lemma snd_diag_snd: "snd \<circ> ((\<lambda>x. (x, x)) \<circ> snd) = snd" by auto 146 147definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}" 148definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}" 149definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))" 150 151lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k" 152 unfolding Shift_def Succ_def by simp 153 154lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl" 155 unfolding Succ_def by simp 156 157lemmas SuccE = SuccD[elim_format] 158 159lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl" 160 unfolding Succ_def by simp 161 162lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl" 163 unfolding Shift_def by simp 164 165lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)" 166 unfolding Succ_def Shift_def by auto 167 168lemma length_Cons: "length (x # xs) = Suc (length xs)" 169 by simp 170 171lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)" 172 by simp 173 174(*injection into the field of a cardinal*) 175definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r" 176definition "toCard A r \<equiv> SOME f. toCard_pred A r f" 177 178lemma ex_toCard_pred: 179 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f" 180 unfolding toCard_pred_def 181 using card_of_ordLeq[of A "Field r"] 182 ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"] 183 by blast 184 185lemma toCard_pred_toCard: 186 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)" 187 unfolding toCard_def using someI_ex[OF ex_toCard_pred] . 188 189lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y" 190 using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast 191 192definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k" 193 194lemma fromCard_toCard: 195 "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b" 196 unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) 197 198lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)" 199 unfolding Field_card_of csum_def by auto 200 201lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)" 202 unfolding Field_card_of csum_def by auto 203 204lemma rec_nat_0_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f 0 = f1" 205 by auto 206 207lemma rec_nat_Suc_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)" 208 by auto 209 210lemma rec_list_Nil_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1" 211 by auto 212 213lemma rec_list_Cons_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)" 214 by auto 215 216lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" 217 by simp 218 219definition image2p where 220 "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)" 221 222lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)" 223 unfolding image2p_def by blast 224 225lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P" 226 unfolding image2p_def by blast 227 228lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)" 229 unfolding rel_fun_def image2p_def by auto 230 231lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g" 232 unfolding rel_fun_def image2p_def by auto 233 234 235subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close> 236 237lemma equiv_Eps_in: 238"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (\<lambda>x. x \<in> X) \<in> X" 239 apply (rule someI2_ex) 240 using in_quotient_imp_non_empty by blast 241 242lemma equiv_Eps_preserves: 243 assumes ECH: "equiv A r" and X: "X \<in> A//r" 244 shows "Eps (\<lambda>x. x \<in> X) \<in> A" 245 apply (rule in_mono[rule_format]) 246 using assms apply (rule in_quotient_imp_subset) 247 by (rule equiv_Eps_in) (rule assms)+ 248 249lemma proj_Eps: 250 assumes "equiv A r" and "X \<in> A//r" 251 shows "proj r (Eps (\<lambda>x. x \<in> X)) = X" 252unfolding proj_def 253proof auto 254 fix x assume x: "x \<in> X" 255 thus "(Eps (\<lambda>x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast 256next 257 fix x assume "(Eps (\<lambda>x. x \<in> X),x) \<in> r" 258 thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast 259qed 260 261definition univ where "univ f X == f (Eps (\<lambda>x. x \<in> X))" 262 263lemma univ_commute: 264assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A" 265shows "(univ f) (proj r x) = f x" 266proof (unfold univ_def) 267 have prj: "proj r x \<in> A//r" using x proj_preserves by fast 268 hence "Eps (\<lambda>y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast 269 moreover have "proj r (Eps (\<lambda>y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast 270 ultimately have "(x, Eps (\<lambda>y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast 271 thus "f (Eps (\<lambda>y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce 272qed 273 274lemma univ_preserves: 275 assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B" 276 shows "\<forall>X \<in> A//r. univ f X \<in> B" 277proof 278 fix X assume "X \<in> A//r" 279 then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast 280 hence "univ f X = f x" using ECH RES univ_commute by fastforce 281 thus "univ f X \<in> B" using x PRES by simp 282qed 283 284ML_file "Tools/BNF/bnf_gfp_util.ML" 285ML_file "Tools/BNF/bnf_gfp_tactics.ML" 286ML_file "Tools/BNF/bnf_gfp.ML" 287ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML" 288ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML" 289 290end 291