src/HOL/BNF_Greatest_Fixpoint.thy
changeset 58128 43a1ba26a8cb
parent 58104 c5316f843f72
child 58352 37745650a3f4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Sep 01 16:34:40 2014 +0200
     1.3 @@ -0,0 +1,300 @@
     1.4 +(*  Title:      HOL/BNF_Greatest_Fixpoint.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Lorenz Panny, TU Muenchen
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8 +    Copyright   2012, 2013, 2014
     1.9 +
    1.10 +Greatest fixed point operation on bounded natural functors.
    1.11 +*)
    1.12 +
    1.13 +header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
    1.14 +
    1.15 +theory BNF_Greatest_Fixpoint
    1.16 +imports BNF_Fixpoint_Base String
    1.17 +keywords
    1.18 +  "codatatype" :: thy_decl and
    1.19 +  "primcorecursive" :: thy_goal and
    1.20 +  "primcorec" :: thy_decl
    1.21 +begin
    1.22 +
    1.23 +setup {*
    1.24 +Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
    1.25 +*}
    1.26 +
    1.27 +lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.28 +  by simp
    1.29 +
    1.30 +lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.31 +  by (cases s) auto
    1.32 +
    1.33 +lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    1.34 +  by (erule notE, rule TrueI)
    1.35 +
    1.36 +lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
    1.37 +  by fast
    1.38 +
    1.39 +lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
    1.40 +  by (auto split: sum.splits)
    1.41 +
    1.42 +lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    1.43 +  apply rule
    1.44 +   apply (rule ext, force split: sum.split)
    1.45 +  by (rule ext, metis case_sum_o_inj(2))
    1.46 +
    1.47 +lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    1.48 +  by fast
    1.49 +
    1.50 +lemma equiv_proj:
    1.51 +  assumes e: "equiv A R" and m: "z \<in> R"
    1.52 +  shows "(proj R o fst) z = (proj R o snd) z"
    1.53 +proof -
    1.54 +  from m have z: "(fst z, snd z) \<in> R" by auto
    1.55 +  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.56 +    unfolding equiv_def sym_def trans_def by blast+
    1.57 +  then show ?thesis unfolding proj_def[abs_def] by auto
    1.58 +qed
    1.59 +
    1.60 +(* Operators: *)
    1.61 +definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
    1.62 +
    1.63 +lemma Id_on_Gr: "Id_on A = Gr A id"
    1.64 +  unfolding Id_on_def Gr_def by auto
    1.65 +
    1.66 +lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
    1.67 +  unfolding image2_def by auto
    1.68 +
    1.69 +lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
    1.70 +  by auto
    1.71 +
    1.72 +lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
    1.73 +  unfolding image2_def Gr_def by auto
    1.74 +
    1.75 +lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
    1.76 +  unfolding Gr_def by simp
    1.77 +
    1.78 +lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
    1.79 +  unfolding Gr_def by simp
    1.80 +
    1.81 +lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
    1.82 +  unfolding Gr_def by auto
    1.83 +
    1.84 +lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    1.85 +  by blast
    1.86 +
    1.87 +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.88 +  by blast
    1.89 +
    1.90 +lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
    1.91 +  unfolding fun_eq_iff by auto
    1.92 +
    1.93 +lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
    1.94 +  by auto
    1.95 +
    1.96 +lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    1.97 +  by force
    1.98 +
    1.99 +lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
   1.100 +  unfolding fun_eq_iff by auto
   1.101 +
   1.102 +lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
   1.103 +  unfolding fun_eq_iff by auto
   1.104 +
   1.105 +lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
   1.106 +  unfolding Gr_def Grp_def fun_eq_iff by auto
   1.107 +
   1.108 +definition relImage where
   1.109 +  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
   1.110 +
   1.111 +definition relInvImage where
   1.112 +  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
   1.113 +
   1.114 +lemma relImage_Gr:
   1.115 +  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
   1.116 +  unfolding relImage_def Gr_def relcomp_def by auto
   1.117 +
   1.118 +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.119 +  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
   1.120 +
   1.121 +lemma relImage_mono:
   1.122 +  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
   1.123 +  unfolding relImage_def by auto
   1.124 +
   1.125 +lemma relInvImage_mono:
   1.126 +  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
   1.127 +  unfolding relInvImage_def by auto
   1.128 +
   1.129 +lemma relInvImage_Id_on:
   1.130 +  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
   1.131 +  unfolding relInvImage_def Id_on_def by auto
   1.132 +
   1.133 +lemma relInvImage_UNIV_relImage:
   1.134 +  "R \<subseteq> relInvImage UNIV (relImage R f) f"
   1.135 +  unfolding relInvImage_def relImage_def by auto
   1.136 +
   1.137 +lemma relImage_proj:
   1.138 +  assumes "equiv A R"
   1.139 +  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
   1.140 +  unfolding relImage_def Id_on_def
   1.141 +  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
   1.142 +  by (auto simp: proj_preserves)
   1.143 +
   1.144 +lemma relImage_relInvImage:
   1.145 +  assumes "R \<subseteq> f ` A <*> f ` A"
   1.146 +  shows "relImage (relInvImage A R f) f = R"
   1.147 +  using assms unfolding relImage_def relInvImage_def by fast
   1.148 +
   1.149 +lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
   1.150 +  by simp
   1.151 +
   1.152 +lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
   1.153 +lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
   1.154 +
   1.155 +lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
   1.156 +lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
   1.157 +lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
   1.158 +lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
   1.159 +
   1.160 +definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
   1.161 +definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
   1.162 +definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
   1.163 +
   1.164 +lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
   1.165 +  unfolding Shift_def Succ_def by simp
   1.166 +
   1.167 +lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
   1.168 +  unfolding Succ_def by simp
   1.169 +
   1.170 +lemmas SuccE = SuccD[elim_format]
   1.171 +
   1.172 +lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
   1.173 +  unfolding Succ_def by simp
   1.174 +
   1.175 +lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
   1.176 +  unfolding Shift_def by simp
   1.177 +
   1.178 +lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
   1.179 +  unfolding Succ_def Shift_def by auto
   1.180 +
   1.181 +lemma length_Cons: "length (x # xs) = Suc (length xs)"
   1.182 +  by simp
   1.183 +
   1.184 +lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
   1.185 +  by simp
   1.186 +
   1.187 +(*injection into the field of a cardinal*)
   1.188 +definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
   1.189 +definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
   1.190 +
   1.191 +lemma ex_toCard_pred:
   1.192 +  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
   1.193 +  unfolding toCard_pred_def
   1.194 +  using card_of_ordLeq[of A "Field r"]
   1.195 +    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
   1.196 +  by blast
   1.197 +
   1.198 +lemma toCard_pred_toCard:
   1.199 +  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
   1.200 +  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
   1.201 +
   1.202 +lemma 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"
   1.203 +  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
   1.204 +
   1.205 +definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
   1.206 +
   1.207 +lemma fromCard_toCard:
   1.208 +  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
   1.209 +  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
   1.210 +
   1.211 +lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
   1.212 +  unfolding Field_card_of csum_def by auto
   1.213 +
   1.214 +lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
   1.215 +  unfolding Field_card_of csum_def by auto
   1.216 +
   1.217 +lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
   1.218 +  by auto
   1.219 +
   1.220 +lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
   1.221 +  by auto
   1.222 +
   1.223 +lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
   1.224 +  by auto
   1.225 +
   1.226 +lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
   1.227 +  by auto
   1.228 +
   1.229 +lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   1.230 +  by simp
   1.231 +
   1.232 +definition image2p where
   1.233 +  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
   1.234 +
   1.235 +lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
   1.236 +  unfolding image2p_def by blast
   1.237 +
   1.238 +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.239 +  unfolding image2p_def by blast
   1.240 +
   1.241 +lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
   1.242 +  unfolding rel_fun_def image2p_def by auto
   1.243 +
   1.244 +lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
   1.245 +  unfolding rel_fun_def image2p_def by auto
   1.246 +
   1.247 +
   1.248 +subsection {* Equivalence relations, quotients, and Hilbert's choice *}
   1.249 +
   1.250 +lemma equiv_Eps_in:
   1.251 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
   1.252 +  apply (rule someI2_ex)
   1.253 +  using in_quotient_imp_non_empty by blast
   1.254 +
   1.255 +lemma equiv_Eps_preserves:
   1.256 +  assumes ECH: "equiv A r" and X: "X \<in> A//r"
   1.257 +  shows "Eps (%x. x \<in> X) \<in> A"
   1.258 +  apply (rule in_mono[rule_format])
   1.259 +   using assms apply (rule in_quotient_imp_subset)
   1.260 +  by (rule equiv_Eps_in) (rule assms)+
   1.261 +
   1.262 +lemma proj_Eps:
   1.263 +  assumes "equiv A r" and "X \<in> A//r"
   1.264 +  shows "proj r (Eps (%x. x \<in> X)) = X"
   1.265 +unfolding proj_def
   1.266 +proof auto
   1.267 +  fix x assume x: "x \<in> X"
   1.268 +  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
   1.269 +next
   1.270 +  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
   1.271 +  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
   1.272 +qed
   1.273 +
   1.274 +definition univ where "univ f X == f (Eps (%x. x \<in> X))"
   1.275 +
   1.276 +lemma univ_commute:
   1.277 +assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
   1.278 +shows "(univ f) (proj r x) = f x"
   1.279 +proof (unfold univ_def)
   1.280 +  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
   1.281 +  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
   1.282 +  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
   1.283 +  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
   1.284 +  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
   1.285 +qed
   1.286 +
   1.287 +lemma univ_preserves:
   1.288 +  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
   1.289 +  shows "\<forall>X \<in> A//r. univ f X \<in> B"
   1.290 +proof
   1.291 +  fix X assume "X \<in> A//r"
   1.292 +  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
   1.293 +  hence "univ f X = f x" using ECH RES univ_commute by fastforce
   1.294 +  thus "univ f X \<in> B" using x PRES by simp
   1.295 +qed
   1.296 +
   1.297 +ML_file "Tools/BNF/bnf_gfp_util.ML"
   1.298 +ML_file "Tools/BNF/bnf_gfp_tactics.ML"
   1.299 +ML_file "Tools/BNF/bnf_gfp.ML"
   1.300 +ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
   1.301 +ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
   1.302 +
   1.303 +end