src/HOL/BNF_GFP.thy
 changeset 55058 4e700eb471d4 parent 55024 05cc0dbf3a50 child 55059 ef2e0fb783c6
1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/BNF_GFP.thy	Mon Jan 20 18:24:56 2014 +0100
1.3 @@ -0,0 +1,356 @@
1.4 +(*  Title:      HOL/BNF/BNF_GFP.thy
1.5 +    Author:     Dmitriy Traytel, TU Muenchen
1.6 +    Copyright   2012
1.7 +
1.8 +Greatest fixed point operation on bounded natural functors.
1.9 +*)
1.10 +
1.11 +header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
1.12 +
1.13 +theory BNF_GFP
1.14 +imports BNF_FP_Base
1.15 +keywords
1.16 +  "codatatype" :: thy_decl and
1.17 +  "primcorecursive" :: thy_goal and
1.18 +  "primcorec" :: thy_decl
1.19 +begin
1.20 +
1.21 +setup {*
1.22 +Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
1.23 +*}
1.24 +
1.25 +lemma not_TrueE: "\<not> True \<Longrightarrow> P"
1.26 +by (erule notE, rule TrueI)
1.27 +
1.28 +lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
1.29 +by fast
1.30 +
1.31 +lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
1.32 +by (auto split: sum.splits)
1.33 +
1.34 +lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f"
1.35 +apply rule
1.36 + apply (rule ext, force split: sum.split)
1.37 +by (rule ext, metis sum_case_o_inj(2))
1.38 +
1.39 +lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
1.40 +by fast
1.41 +
1.42 +lemma equiv_proj:
1.43 +  assumes e: "equiv A R" and "z \<in> R"
1.44 +  shows "(proj R o fst) z = (proj R o snd) z"
1.45 +proof -
1.46 +  from assms(2) have z: "(fst z, snd z) \<in> R" by auto
1.47 +  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"
1.48 +    unfolding equiv_def sym_def trans_def by blast+
1.49 +  then show ?thesis unfolding proj_def[abs_def] by auto
1.50 +qed
1.51 +
1.52 +(* Operators: *)
1.53 +definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
1.54 +
1.55 +lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
1.56 +unfolding Id_on_def by simp
1.57 +
1.58 +lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
1.59 +unfolding Id_on_def by auto
1.60 +
1.61 +lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
1.62 +unfolding Id_on_def by auto
1.63 +
1.64 +lemma Id_on_UNIV: "Id_on UNIV = Id"
1.65 +unfolding Id_on_def by auto
1.66 +
1.67 +lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
1.68 +unfolding Id_on_def by auto
1.69 +
1.70 +lemma Id_on_Gr: "Id_on A = Gr A id"
1.71 +unfolding Id_on_def Gr_def by auto
1.72 +
1.73 +lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
1.74 +unfolding image2_def by auto
1.75 +
1.76 +lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
1.77 +by auto
1.78 +
1.79 +lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
1.80 +unfolding image2_def Gr_def by auto
1.81 +
1.82 +lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
1.83 +unfolding Gr_def by simp
1.84 +
1.85 +lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
1.86 +unfolding Gr_def by simp
1.87 +
1.88 +lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
1.89 +unfolding Gr_def by auto
1.90 +
1.91 +lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
1.92 +by blast
1.93 +
1.94 +lemma 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})"
1.95 +by blast
1.96 +
1.97 +lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
1.98 +unfolding fun_eq_iff by auto
1.99 +
1.100 +lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
1.101 +by auto
1.103 +lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
1.104 +by force
1.106 +lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
1.107 +by auto
1.109 +lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
1.110 +unfolding fun_eq_iff by auto
1.112 +lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
1.113 +unfolding fun_eq_iff by auto
1.115 +lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
1.116 +unfolding Gr_def Grp_def fun_eq_iff by auto
1.118 +lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
1.119 +unfolding fun_eq_iff by auto
1.121 +definition relImage where
1.122 +"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
1.124 +definition relInvImage where
1.125 +"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
1.127 +lemma relImage_Gr:
1.128 +"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
1.129 +unfolding relImage_def Gr_def relcomp_def by auto
1.131 +lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
1.132 +unfolding Gr_def relcomp_def image_def relInvImage_def by auto
1.134 +lemma relImage_mono:
1.135 +"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
1.136 +unfolding relImage_def by auto
1.138 +lemma relInvImage_mono:
1.139 +"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
1.140 +unfolding relInvImage_def by auto
1.142 +lemma relInvImage_Id_on:
1.143 +"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
1.144 +unfolding relInvImage_def Id_on_def by auto
1.146 +lemma relInvImage_UNIV_relImage:
1.147 +"R \<subseteq> relInvImage UNIV (relImage R f) f"
1.148 +unfolding relInvImage_def relImage_def by auto
1.150 +lemma relImage_proj:
1.151 +assumes "equiv A R"
1.152 +shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
1.153 +unfolding relImage_def Id_on_def
1.154 +using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
1.155 +by (auto simp: proj_preserves)
1.157 +lemma relImage_relInvImage:
1.158 +assumes "R \<subseteq> f ` A <*> f ` A"
1.159 +shows "relImage (relInvImage A R f) f = R"
1.160 +using assms unfolding relImage_def relInvImage_def by fast
1.162 +lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
1.163 +by simp
1.165 +lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
1.166 +by simp
1.168 +lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
1.169 +by simp
1.171 +lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x"
1.172 +unfolding convol_def by auto
1.174 +(*Extended Sublist*)
1.176 +definition clists where "clists r = |lists (Field r)|"
1.178 +definition prefCl where
1.179 +  "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
1.180 +definition PrefCl where
1.181 +  "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
1.183 +lemma prefCl_UN:
1.184 +  "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
1.185 +unfolding prefCl_def PrefCl_def by fastforce
1.187 +definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
1.188 +definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
1.189 +definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
1.191 +lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
1.192 +unfolding Shift_def Succ_def by simp
1.194 +lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
1.195 +unfolding Shift_def clists_def Field_card_of by auto
1.197 +lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
1.198 +unfolding prefCl_def Shift_def
1.199 +proof safe
1.200 +  fix kl1 kl2
1.201 +  assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
1.202 +    "prefixeq kl1 kl2" "k # kl2 \<in> Kl"
1.203 +  thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast
1.204 +qed
1.206 +lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
1.207 +unfolding Shift_def by simp
1.209 +lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
1.210 +unfolding Succ_def by simp
1.212 +lemmas SuccE = SuccD[elim_format]
1.214 +lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
1.215 +unfolding Succ_def by simp
1.217 +lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
1.218 +unfolding Shift_def by simp
1.220 +lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
1.221 +unfolding Succ_def Shift_def by auto
1.223 +lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
1.224 +unfolding clists_def Field_card_of by auto
1.226 +lemma Cons_clists:
1.227 +  "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
1.228 +unfolding clists_def Field_card_of by auto
1.230 +lemma length_Cons: "length (x # xs) = Suc (length xs)"
1.231 +by simp
1.233 +lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
1.234 +by simp
1.236 +(*injection into the field of a cardinal*)
1.237 +definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
1.238 +definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
1.240 +lemma ex_toCard_pred:
1.241 +"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
1.242 +unfolding toCard_pred_def
1.243 +using card_of_ordLeq[of A "Field r"]
1.244 +      ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
1.245 +by blast
1.247 +lemma toCard_pred_toCard:
1.248 +  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
1.249 +unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
1.251 +lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
1.252 +  toCard A r x = toCard A r y \<longleftrightarrow> x = y"
1.253 +using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
1.255 +lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
1.256 +using toCard_pred_toCard unfolding toCard_pred_def by blast
1.258 +definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
1.260 +lemma fromCard_toCard:
1.261 +"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
1.262 +unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
1.264 +lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
1.265 +unfolding Field_card_of csum_def by auto
1.267 +lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
1.268 +unfolding Field_card_of csum_def by auto
1.270 +lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
1.271 +by auto
1.273 +lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
1.274 +by auto
1.276 +lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
1.277 +by auto
1.279 +lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
1.280 +by auto
1.282 +lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
1.283 +by simp
1.285 +lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
1.286 +by auto
1.288 +definition image2p where
1.289 +  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
1.291 +lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
1.292 +  unfolding image2p_def by blast
1.294 +lemma 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"
1.295 +  unfolding image2p_def by blast
1.297 +lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
1.298 +  unfolding fun_rel_def image2p_def by auto
1.300 +lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
1.301 +  unfolding fun_rel_def image2p_def by auto
1.304 +subsection {* Equivalence relations, quotients, and Hilbert's choice *}
1.306 +lemma equiv_Eps_in:
1.307 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
1.308 +apply (rule someI2_ex)
1.309 +using in_quotient_imp_non_empty by blast
1.311 +lemma equiv_Eps_preserves:
1.312 +assumes ECH: "equiv A r" and X: "X \<in> A//r"
1.313 +shows "Eps (%x. x \<in> X) \<in> A"
1.314 +apply (rule in_mono[rule_format])
1.315 + using assms apply (rule in_quotient_imp_subset)
1.316 +by (rule equiv_Eps_in) (rule assms)+
1.318 +lemma proj_Eps:
1.319 +assumes "equiv A r" and "X \<in> A//r"
1.320 +shows "proj r (Eps (%x. x \<in> X)) = X"
1.321 +unfolding proj_def proof auto
1.322 +  fix x assume x: "x \<in> X"
1.323 +  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
1.324 +next
1.325 +  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
1.326 +  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
1.327 +qed
1.329 +definition univ where "univ f X == f (Eps (%x. x \<in> X))"
1.331 +lemma univ_commute:
1.332 +assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
1.333 +shows "(univ f) (proj r x) = f x"
1.334 +unfolding univ_def proof -
1.335 +  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
1.336 +  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
1.337 +  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
1.338 +  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
1.339 +  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
1.340 +qed
1.342 +lemma univ_preserves:
1.343 +assumes ECH: "equiv A r" and RES: "f respects r" and
1.344 +        PRES: "\<forall> x \<in> A. f x \<in> B"
1.345 +shows "\<forall> X \<in> A//r. univ f X \<in> B"
1.346 +proof
1.347 +  fix X assume "X \<in> A//r"
1.348 +  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
1.349 +  hence "univ f X = f x" using assms univ_commute by fastforce
1.350 +  thus "univ f X \<in> B" using x PRES by simp
1.351 +qed
1.353 +ML_file "Tools/bnf_gfp_rec_sugar_tactics.ML"
1.354 +ML_file "Tools/bnf_gfp_rec_sugar.ML"
1.355 +ML_file "Tools/bnf_gfp_util.ML"
1.356 +ML_file "Tools/bnf_gfp_tactics.ML"
1.357 +ML_file "Tools/bnf_gfp.ML"
1.359 +end