src/HOL/BNF_Greatest_Fixpoint.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 62905 52c5a25e0c96 child 64413 c0d5e78eb647 permissions -rw-r--r--
tuned proofs;
```     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
```
```     7 Greatest fixpoint (codatatype) operation on bounded natural functors.
```
```     8 *)
```
```     9
```
```    10 section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close>
```
```    11
```
```    12 theory BNF_Greatest_Fixpoint
```
```    13 imports BNF_Fixpoint_Base String
```
```    14 keywords
```
```    15   "codatatype" :: thy_decl and
```
```    16   "primcorecursive" :: thy_goal and
```
```    17   "primcorec" :: thy_decl
```
```    18 begin
```
```    19
```
```    20 setup \<open>Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\<close>
```
```    21
```
```    22 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
```
```    23   by simp
```
```    24
```
```    25 lemma 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
```
```    28 lemma not_TrueE: "\<not> True \<Longrightarrow> P"
```
```    29   by (erule notE, rule TrueI)
```
```    30
```
```    31 lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
```
```    32   by fast
```
```    33
```
```    34 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
```
```    35   by fast
```
```    36
```
```    37 lemma equiv_proj:
```
```    38   assumes e: "equiv A R" and m: "z \<in> R"
```
```    39   shows "(proj R o fst) z = (proj R o snd) z"
```
```    40 proof -
```
```    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
```
```    45 qed
```
```    46
```
```    47 (* Operators: *)
```
```    48 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
```
```    49
```
```    50 lemma Id_on_Gr: "Id_on A = Gr A id"
```
```    51   unfolding Id_on_def Gr_def by auto
```
```    52
```
```    53 lemma 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
```
```    56 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
```
```    57   by auto
```
```    58
```
```    59 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
```
```    60   unfolding image2_def Gr_def by auto
```
```    61
```
```    62 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
```
```    63   unfolding Gr_def by simp
```
```    64
```
```    65 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
```
```    66   unfolding Gr_def by simp
```
```    67
```
```    68 lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
```
```    69   unfolding Gr_def by auto
```
```    70
```
```    71 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
```
```    72   by blast
```
```    73
```
```    74 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})"
```
```    75   by blast
```
```    76
```
```    77 lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X"
```
```    78   unfolding fun_eq_iff by auto
```
```    79
```
```    80 lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
```
```    81   by auto
```
```    82
```
```    83 lemma 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
```
```    86 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
```
```    87   unfolding fun_eq_iff by auto
```
```    88
```
```    89 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
```
```    90   unfolding fun_eq_iff by auto
```
```    91
```
```    92 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
```
```    93   unfolding Gr_def Grp_def fun_eq_iff by auto
```
```    94
```
```    95 definition relImage where
```
```    96   "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
```
```    97
```
```    98 definition 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
```
```   101 lemma relImage_Gr:
```
```   102   "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
```
```   103   unfolding relImage_def Gr_def relcomp_def by auto
```
```   104
```
```   105 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"
```
```   106   unfolding Gr_def relcomp_def image_def relInvImage_def by auto
```
```   107
```
```   108 lemma relImage_mono:
```
```   109   "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
```
```   110   unfolding relImage_def by auto
```
```   111
```
```   112 lemma relInvImage_mono:
```
```   113   "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
```
```   114   unfolding relInvImage_def by auto
```
```   115
```
```   116 lemma 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
```
```   120 lemma relInvImage_UNIV_relImage:
```
```   121   "R \<subseteq> relInvImage UNIV (relImage R f) f"
```
```   122   unfolding relInvImage_def relImage_def by auto
```
```   123
```
```   124 lemma 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
```
```   131 lemma 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
```
```   136 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
```
```   137   by simp
```
```   138
```
```   139 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
```
```   140 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
```
```   141
```
```   142 lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
```
```   143 lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
```
```   144 lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
```
```   145 lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
```
```   146
```
```   147 definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
```
```   148 definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
```
```   149 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
```
```   150
```
```   151 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
```
```   152   unfolding Shift_def Succ_def by simp
```
```   153
```
```   154 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
```
```   155   unfolding Succ_def by simp
```
```   156
```
```   157 lemmas SuccE = SuccD[elim_format]
```
```   158
```
```   159 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
```
```   160   unfolding Succ_def by simp
```
```   161
```
```   162 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
```
```   163   unfolding Shift_def by simp
```
```   164
```
```   165 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
```
```   166   unfolding Succ_def Shift_def by auto
```
```   167
```
```   168 lemma length_Cons: "length (x # xs) = Suc (length xs)"
```
```   169   by simp
```
```   170
```
```   171 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
```
```   172   by simp
```
```   173
```
```   174 (*injection into the field of a cardinal*)
```
```   175 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
```
```   176 definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
```
```   177
```
```   178 lemma 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
```
```   185 lemma 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
```
```   189 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"
```
```   190   using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
```
```   191
```
```   192 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
```
```   193
```
```   194 lemma 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
```
```   198 lemma 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
```
```   201 lemma 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
```
```   204 lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
```
```   205   by auto
```
```   206
```
```   207 lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
```
```   208   by auto
```
```   209
```
```   210 lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
```
```   211   by auto
```
```   212
```
```   213 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)"
```
```   214   by auto
```
```   215
```
```   216 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
```
```   217   by simp
```
```   218
```
```   219 definition 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
```
```   222 lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
```
```   223   unfolding image2p_def by blast
```
```   224
```
```   225 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"
```
```   226   unfolding image2p_def by blast
```
```   227
```
```   228 lemma 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
```
```   231 lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
```
```   232   unfolding rel_fun_def image2p_def by auto
```
```   233
```
```   234
```
```   235 subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
```
```   236
```
```   237 lemma equiv_Eps_in:
```
```   238 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
```
```   239   apply (rule someI2_ex)
```
```   240   using in_quotient_imp_non_empty by blast
```
```   241
```
```   242 lemma equiv_Eps_preserves:
```
```   243   assumes ECH: "equiv A r" and X: "X \<in> A//r"
```
```   244   shows "Eps (%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
```
```   249 lemma proj_Eps:
```
```   250   assumes "equiv A r" and "X \<in> A//r"
```
```   251   shows "proj r (Eps (%x. x \<in> X)) = X"
```
```   252 unfolding proj_def
```
```   253 proof auto
```
```   254   fix x assume x: "x \<in> X"
```
```   255   thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
```
```   256 next
```
```   257   fix x assume "(Eps (%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
```
```   259 qed
```
```   260
```
```   261 definition univ where "univ f X == f (Eps (%x. x \<in> X))"
```
```   262
```
```   263 lemma univ_commute:
```
```   264 assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
```
```   265 shows "(univ f) (proj r x) = f x"
```
```   266 proof (unfold univ_def)
```
```   267   have prj: "proj r x \<in> A//r" using x proj_preserves by fast
```
```   268   hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
```
```   269   moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
```
```   270   ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
```
```   271   thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
```
```   272 qed
```
```   273
```
```   274 lemma 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"
```
```   277 proof
```
```   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
```
```   282 qed
```
```   283
```
```   284 ML_file "Tools/BNF/bnf_gfp_util.ML"
```
```   285 ML_file "Tools/BNF/bnf_gfp_tactics.ML"
```
```   286 ML_file "Tools/BNF/bnf_gfp.ML"
```
```   287 ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
```
```   288 ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
```
```   289
```
```   290 end
```