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