src/HOL/BNF/BNF_GFP.thy
 author traytel Tue Nov 13 12:06:43 2012 +0100 (2012-11-13) changeset 50058 bb1fadeba35e parent 49635 fc0777f04205 child 51446 a6ebb12cc003 permissions -rw-r--r--
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
```     1 (*  Title:      HOL/BNF/BNF_GFP.thy
```
```     2     Author:     Dmitriy Traytel, TU Muenchen
```
```     3     Copyright   2012
```
```     4
```
```     5 Greatest fixed point operation on bounded natural functors.
```
```     6 *)
```
```     7
```
```     8 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
```
```     9
```
```    10 theory BNF_GFP
```
```    11 imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Sublist"
```
```    12 keywords
```
```    13   "codata" :: thy_decl
```
```    14 begin
```
```    15
```
```    16 lemma sum_case_comp_Inl:
```
```    17 "sum_case f g \<circ> Inl = f"
```
```    18 unfolding comp_def by simp
```
```    19
```
```    20 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
```
```    21 by (auto split: sum.splits)
```
```    22
```
```    23 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
```
```    24 by auto
```
```    25
```
```    26 lemma equiv_triv1:
```
```    27 assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
```
```    28 shows "(b, c) \<in> R"
```
```    29 using assms unfolding equiv_def sym_def trans_def by blast
```
```    30
```
```    31 lemma equiv_triv2:
```
```    32 assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
```
```    33 shows "(a, c) \<in> R"
```
```    34 using assms unfolding equiv_def trans_def by blast
```
```    35
```
```    36 lemma equiv_proj:
```
```    37   assumes e: "equiv A R" and "z \<in> R"
```
```    38   shows "(proj R o fst) z = (proj R o snd) z"
```
```    39 proof -
```
```    40   from assms(2) have z: "(fst z, snd z) \<in> R" by auto
```
```    41   have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
```
```    42   have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
```
```    43   with P show ?thesis unfolding proj_def[abs_def] by auto
```
```    44 qed
```
```    45
```
```    46 (* Operators: *)
```
```    47 definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
```
```    48 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
```
```    49
```
```    50 lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
```
```    51 unfolding diag_def by simp
```
```    52
```
```    53 lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
```
```    54 unfolding diag_def by simp
```
```    55
```
```    56 lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
```
```    57 unfolding diag_def by auto
```
```    58
```
```    59 lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
```
```    60 unfolding diag_def by auto
```
```    61
```
```    62 lemma diag_UNIV: "diag UNIV = Id"
```
```    63 unfolding diag_def by auto
```
```    64
```
```    65 lemma diag_converse: "diag A = (diag A) ^-1"
```
```    66 unfolding diag_def by auto
```
```    67
```
```    68 lemma diag_Comp: "diag A = diag A O diag A"
```
```    69 unfolding diag_def by auto
```
```    70
```
```    71 lemma diag_Gr: "diag A = Gr A id"
```
```    72 unfolding diag_def Gr_def by simp
```
```    73
```
```    74 lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
```
```    75 unfolding diag_def by auto
```
```    76
```
```    77 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
```
```    78 unfolding image2_def by auto
```
```    79
```
```    80 lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}"
```
```    81 by auto
```
```    82
```
```    83 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
```
```    84 by auto
```
```    85
```
```    86 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
```
```    87 unfolding image2_def Gr_def by auto
```
```    88
```
```    89 lemma GrI: "\<lbrakk>x \<in> A; f x = fx\<rbrakk> \<Longrightarrow> (x, fx) \<in> Gr A f"
```
```    90 unfolding Gr_def by simp
```
```    91
```
```    92 lemma GrE: "(x, fx) \<in> Gr A f \<Longrightarrow> (x \<in> A \<Longrightarrow> f x = fx \<Longrightarrow> P) \<Longrightarrow> P"
```
```    93 unfolding Gr_def by simp
```
```    94
```
```    95 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
```
```    96 unfolding Gr_def by simp
```
```    97
```
```    98 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
```
```    99 unfolding Gr_def by simp
```
```   100
```
```   101 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
```
```   102 unfolding Gr_def by auto
```
```   103
```
```   104 definition relImage where
```
```   105 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
```
```   106
```
```   107 definition relInvImage where
```
```   108 "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
```
```   109
```
```   110 lemma relImage_Gr:
```
```   111 "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
```
```   112 unfolding relImage_def Gr_def relcomp_def by auto
```
```   113
```
```   114 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"
```
```   115 unfolding Gr_def relcomp_def image_def relInvImage_def by auto
```
```   116
```
```   117 lemma relImage_mono:
```
```   118 "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
```
```   119 unfolding relImage_def by auto
```
```   120
```
```   121 lemma relInvImage_mono:
```
```   122 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
```
```   123 unfolding relInvImage_def by auto
```
```   124
```
```   125 lemma relInvImage_diag:
```
```   126 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
```
```   127 unfolding relInvImage_def diag_def by auto
```
```   128
```
```   129 lemma relInvImage_UNIV_relImage:
```
```   130 "R \<subseteq> relInvImage UNIV (relImage R f) f"
```
```   131 unfolding relInvImage_def relImage_def by auto
```
```   132
```
```   133 lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})"
```
```   134 unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD)
```
```   135
```
```   136 lemma relImage_proj:
```
```   137 assumes "equiv A R"
```
```   138 shows "relImage R (proj R) \<subseteq> diag (A//R)"
```
```   139 unfolding relImage_def diag_def apply safe
```
```   140 using proj_iff[OF assms]
```
```   141 by (metis assms equiv_Image proj_def proj_preserves)
```
```   142
```
```   143 lemma relImage_relInvImage:
```
```   144 assumes "R \<subseteq> f ` A <*> f ` A"
```
```   145 shows "relImage (relInvImage A R f) f = R"
```
```   146 using assms unfolding relImage_def relInvImage_def by fastforce
```
```   147
```
```   148 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
```
```   149 by simp
```
```   150
```
```   151 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
```
```   152 by simp
```
```   153
```
```   154 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
```
```   155 by simp
```
```   156
```
```   157 lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
```
```   158 by auto
```
```   159
```
```   160 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"
```
```   161 unfolding convol_def by auto
```
```   162
```
```   163 (*Extended Sublist*)
```
```   164
```
```   165 definition prefCl where
```
```   166   "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
```
```   167 definition PrefCl where
```
```   168   "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
```
```   169
```
```   170 lemma prefCl_UN:
```
```   171   "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
```
```   172 unfolding prefCl_def PrefCl_def by fastforce
```
```   173
```
```   174 definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
```
```   175 definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
```
```   176 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
```
```   177
```
```   178 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
```
```   179 unfolding Shift_def Succ_def by simp
```
```   180
```
```   181 lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
```
```   182 unfolding Shift_def clists_def Field_card_of by auto
```
```   183
```
```   184 lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
```
```   185 unfolding prefCl_def Shift_def
```
```   186 proof safe
```
```   187   fix kl1 kl2
```
```   188   assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
```
```   189     "prefixeq kl1 kl2" "k # kl2 \<in> Kl"
```
```   190   thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast
```
```   191 qed
```
```   192
```
```   193 lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
```
```   194 unfolding Shift_def by simp
```
```   195
```
```   196 lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
```
```   197 unfolding Succ_def proof
```
```   198   assume "prefCl Kl" "k # kl \<in> Kl"
```
```   199   moreover have "prefixeq (k # []) (k # kl)" by auto
```
```   200   ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
```
```   201   thus "[] @ [k] \<in> Kl" by simp
```
```   202 qed
```
```   203
```
```   204 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
```
```   205 unfolding Succ_def by simp
```
```   206
```
```   207 lemmas SuccE = SuccD[elim_format]
```
```   208
```
```   209 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
```
```   210 unfolding Succ_def by simp
```
```   211
```
```   212 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
```
```   213 unfolding Shift_def by simp
```
```   214
```
```   215 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
```
```   216 unfolding Succ_def Shift_def by auto
```
```   217
```
```   218 lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
```
```   219 unfolding Shift_def by simp
```
```   220
```
```   221 lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
```
```   222 unfolding cexp_def Field_card_of by (simp only: card_of_refl)
```
```   223
```
```   224 lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
```
```   225 unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
```
```   226
```
```   227 lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
```
```   228 unfolding cpow_def clists_def
```
```   229 by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric])
```
```   230    (erule notE, erule ordIso_transitive, rule czero_ordIso)
```
```   231
```
```   232 lemma incl_UNION_I:
```
```   233 assumes "i \<in> I" and "A \<subseteq> F i"
```
```   234 shows "A \<subseteq> UNION I F"
```
```   235 using assms by auto
```
```   236
```
```   237 lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
```
```   238 unfolding clists_def Field_card_of by auto
```
```   239
```
```   240 lemma Cons_clists:
```
```   241   "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
```
```   242 unfolding clists_def Field_card_of by auto
```
```   243
```
```   244 lemma length_Cons: "length (x # xs) = Suc (length xs)"
```
```   245 by simp
```
```   246
```
```   247 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
```
```   248 by simp
```
```   249
```
```   250 (*injection into the field of a cardinal*)
```
```   251 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
```
```   252 definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
```
```   253
```
```   254 lemma ex_toCard_pred:
```
```   255 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
```
```   256 unfolding toCard_pred_def
```
```   257 using card_of_ordLeq[of A "Field r"]
```
```   258       ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
```
```   259 by blast
```
```   260
```
```   261 lemma toCard_pred_toCard:
```
```   262   "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
```
```   263 unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
```
```   264
```
```   265 lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
```
```   266   toCard A r x = toCard A r y \<longleftrightarrow> x = y"
```
```   267 using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
```
```   268
```
```   269 lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
```
```   270 using toCard_pred_toCard unfolding toCard_pred_def by blast
```
```   271
```
```   272 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
```
```   273
```
```   274 lemma fromCard_toCard:
```
```   275 "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
```
```   276 unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
```
```   277
```
```   278 (* pick according to the weak pullback *)
```
```   279 definition pickWP_pred where
```
```   280 "pickWP_pred A p1 p2 b1 b2 a \<equiv> a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
```
```   281
```
```   282 definition pickWP where
```
```   283 "pickWP A p1 p2 b1 b2 \<equiv> SOME a. pickWP_pred A p1 p2 b1 b2 a"
```
```   284
```
```   285 lemma pickWP_pred:
```
```   286 assumes "wpull A B1 B2 f1 f2 p1 p2" and
```
```   287 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
```
```   288 shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a"
```
```   289 using assms unfolding wpull_def pickWP_pred_def by blast
```
```   290
```
```   291 lemma pickWP_pred_pickWP:
```
```   292 assumes "wpull A B1 B2 f1 f2 p1 p2" and
```
```   293 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
```
```   294 shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)"
```
```   295 unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred])
```
```   296
```
```   297 lemma pickWP:
```
```   298 assumes "wpull A B1 B2 f1 f2 p1 p2" and
```
```   299 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
```
```   300 shows "pickWP A p1 p2 b1 b2 \<in> A"
```
```   301       "p1 (pickWP A p1 p2 b1 b2) = b1"
```
```   302       "p2 (pickWP A p1 p2 b1 b2) = b2"
```
```   303 using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+
```
```   304
```
```   305 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
```
```   306 unfolding Field_card_of csum_def by auto
```
```   307
```
```   308 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
```
```   309 unfolding Field_card_of csum_def by auto
```
```   310
```
```   311 lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
```
```   312 by auto
```
```   313
```
```   314 lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
```
```   315 by auto
```
```   316
```
```   317 lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
```
```   318 by auto
```
```   319
```
```   320 lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
```
```   321 by auto
```
```   322
```
```   323 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
```
```   324 by simp
```
```   325
```
```   326 ML_file "Tools/bnf_gfp_util.ML"
```
```   327 ML_file "Tools/bnf_gfp_tactics.ML"
```
```   328 ML_file "Tools/bnf_gfp.ML"
```
```   329
```
```   330 end
```