src/HOL/Codatatype/BNF_Library.thy
author blanchet
Mon Sep 10 17:35:53 2012 +0200 (2012-09-10)
changeset 49255 2ecc533d6697
parent 49125 5fc5211cf104
child 49263 669a820ef213
permissions -rw-r--r--
use balanced sums for constructors (to gracefully handle 100 constructors or more)
     1 (*  Title:      HOL/Codatatype/BNF_Library.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Library for bounded natural functors.
     6 *)
     7 
     8 header {* Library for Bounded Natural Functors *}
     9 
    10 theory BNF_Library
    11 imports
    12   "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
    13   "~~/src/HOL/Library/Prefix_Order"
    14   Equiv_Relations_More
    15 begin
    16 
    17 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    18 by (erule iffI) (erule contrapos_pn)
    19 
    20 lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
    21 
    22 lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
    23 
    24 lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
    25 by presburger
    26 
    27 lemma case_unit: "(case u of () => f) = f"
    28 by (cases u) (hypsubst, rule unit.cases)
    29 
    30 lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
    31 by presburger
    32 
    33 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    34 by blast
    35 
    36 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})"
    37 by blast
    38 
    39 lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X"
    40 by simp
    41 
    42 lemma image_comp: "image (f o g) = image f o image g"
    43 by (rule ext) (auto simp only: o_apply image_def)
    44 
    45 lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
    46 by (rule ext) simp
    47 
    48 lemma Union_natural: "Union o image (image f) = image f o Union"
    49 by (rule ext) (auto simp only: o_apply)
    50 
    51 lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    52 by (unfold o_assoc)
    53 
    54 lemma comp_single_set_bd:
    55   assumes fbd_Card_order: "Card_order fbd" and
    56     fset_bd: "\<And>x. |fset x| \<le>o fbd" and
    57     gset_bd: "\<And>x. |gset x| \<le>o gbd"
    58   shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd"
    59 apply (subst sym[OF SUP_def])
    60 apply (rule ordLeq_transitive)
    61 apply (rule card_of_UNION_Sigma)
    62 apply (subst SIGMA_CSUM)
    63 apply (rule ordLeq_transitive)
    64 apply (rule card_of_Csum_Times')
    65 apply (rule fbd_Card_order)
    66 apply (rule ballI)
    67 apply (rule fset_bd)
    68 apply (rule ordLeq_transitive)
    69 apply (rule cprod_mono1)
    70 apply (rule gset_bd)
    71 apply (rule ordIso_imp_ordLeq)
    72 apply (rule ordIso_refl)
    73 apply (rule Card_order_cprod)
    74 done
    75 
    76 lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B"
    77 by simp
    78 
    79 lemma Union_image_empty: "A \<union> \<Union>f ` {} = A"
    80 by simp
    81 
    82 definition collect where
    83   "collect F x = (\<Union>f \<in> F. f x)"
    84 
    85 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
    86 by (rule ext) (auto simp only: o_apply collect_def)
    87 
    88 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
    89 by (rule ext) (auto simp add: collect_def)
    90 
    91 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    92 by blast
    93 
    94 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
    95 by blast
    96 
    97 lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
    98 by simp
    99 
   100 lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
   101 by simp
   102 
   103 lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
   104 by blast
   105 
   106 lemma image_Collect_subsetI:
   107   "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
   108 by blast
   109 
   110 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
   111 by (unfold o_apply collect_def SUP_def)
   112 
   113 lemma sum_case_comp_Inl:
   114 "sum_case f g \<circ> Inl = f"
   115 unfolding comp_def by simp
   116 
   117 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
   118 by (auto split: sum.splits)
   119 
   120 lemma converse_mono:
   121 "R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
   122 unfolding converse_def by auto
   123 
   124 lemma converse_shift:
   125 "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
   126 unfolding converse_def by auto
   127 
   128 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
   129 by auto
   130 
   131 lemma equiv_triv1:
   132 assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
   133 shows "(b, c) \<in> R"
   134 using assms unfolding equiv_def sym_def trans_def by blast
   135 
   136 lemma equiv_triv2:
   137 assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
   138 shows "(a, c) \<in> R"
   139 using assms unfolding equiv_def trans_def by blast
   140 
   141 lemma equiv_proj:
   142   assumes e: "equiv A R" and "z \<in> R"
   143   shows "(proj R o fst) z = (proj R o snd) z"
   144 proof -
   145   from assms(2) have z: "(fst z, snd z) \<in> R" by auto
   146   have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
   147   have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
   148   with P show ?thesis unfolding proj_def[abs_def] by auto
   149 qed
   150 
   151 
   152 section{* Weak pullbacks: *}
   153 
   154 definition csquare where
   155 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
   156 
   157 definition wpull where
   158 "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
   159  (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
   160 
   161 lemma wpull_cong:
   162 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
   163 by simp
   164 
   165 lemma wpull_id: "wpull UNIV B1 B2 id id id id"
   166 unfolding wpull_def by simp
   167 
   168 
   169 (* Weak pseudo-pullbacks *)
   170 
   171 definition wppull where
   172 "wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
   173  (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
   174            (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
   175 
   176 
   177 (* The pullback of sets *)
   178 definition thePull where
   179 "thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
   180 
   181 lemma wpull_thePull:
   182 "wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
   183 unfolding wpull_def thePull_def by auto
   184 
   185 lemma wppull_thePull:
   186 assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
   187 shows
   188 "\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
   189    j a' \<in> A \<and>
   190    e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
   191 (is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
   192 proof(rule bchoice[of ?A' ?phi], default)
   193   fix a' assume a': "a' \<in> ?A'"
   194   hence "fst a' \<in> B1" unfolding thePull_def by auto
   195   moreover
   196   from a' have "snd a' \<in> B2" unfolding thePull_def by auto
   197   moreover have "f1 (fst a') = f2 (snd a')"
   198   using a' unfolding csquare_def thePull_def by auto
   199   ultimately show "\<exists> ja'. ?phi a' ja'"
   200   using assms unfolding wppull_def by auto
   201 qed
   202 
   203 lemma wpull_wppull:
   204 assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
   205 1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
   206 shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
   207 unfolding wppull_def proof safe
   208   fix b1 b2
   209   assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
   210   then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
   211   using wp unfolding wpull_def by blast
   212   show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
   213   apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
   214 qed
   215 
   216 lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
   217    wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2"
   218 by (erule wpull_wppull) auto
   219 
   220 
   221 (* Operators: *)
   222 definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
   223 definition "Gr A f = {(a,f a) | a. a \<in> A}"
   224 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
   225 
   226 lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
   227 unfolding diag_def by simp
   228 
   229 lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
   230 unfolding diag_def by simp
   231 
   232 lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
   233 unfolding diag_def by auto
   234 
   235 lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
   236 unfolding diag_def by auto
   237 
   238 lemma diag_UNIV: "diag UNIV = Id"
   239 unfolding diag_def by auto
   240 
   241 lemma diag_converse: "diag A = (diag A) ^-1"
   242 unfolding diag_def by auto
   243 
   244 lemma diag_Comp: "diag A = diag A O diag A"
   245 unfolding diag_def by auto
   246 
   247 lemma diag_Gr: "diag A = Gr A id"
   248 unfolding diag_def Gr_def by simp
   249 
   250 lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
   251 unfolding diag_def by auto
   252 
   253 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
   254 unfolding image2_def by auto
   255 
   256 lemma Id_def': "Id = {(a,b). a = b}"
   257 by auto
   258 
   259 lemma Id_alt: "Id = Gr UNIV id"
   260 unfolding Gr_def by auto
   261 
   262 lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}"
   263 by auto
   264 
   265 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
   266 by auto
   267 
   268 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
   269 unfolding image2_def Gr_def by auto
   270 
   271 lemma GrI: "\<lbrakk>x \<in> A; f x = fx\<rbrakk> \<Longrightarrow> (x, fx) \<in> Gr A f"
   272 unfolding Gr_def by simp
   273 
   274 lemma GrE: "(x, fx) \<in> Gr A f \<Longrightarrow> (x \<in> A \<Longrightarrow> f x = fx \<Longrightarrow> P) \<Longrightarrow> P"
   275 unfolding Gr_def by simp
   276 
   277 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
   278 unfolding Gr_def by simp
   279 
   280 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
   281 unfolding Gr_def by simp
   282 
   283 lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
   284 unfolding Gr_def by auto
   285 
   286 lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
   287 unfolding Gr_def by auto
   288 
   289 lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
   290 unfolding Gr_def by auto
   291 
   292 lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
   293 by simp
   294 
   295 lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)"
   296 by auto
   297 
   298 lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'"
   299 by blast
   300 
   301 lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
   302 by auto
   303 
   304 lemma wpull_Gr:
   305 "wpull (Gr A f) A (f ` A) f id fst snd"
   306 unfolding wpull_def Gr_def by auto
   307 
   308 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
   309 unfolding Gr_def by auto
   310 
   311 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})"
   312 unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD)
   313 
   314 definition relImage where
   315 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
   316 
   317 definition relInvImage where
   318 "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
   319 
   320 lemma relImage_Gr:
   321 "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
   322 unfolding relImage_def Gr_def relcomp_def by auto
   323 
   324 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"
   325 unfolding Gr_def relcomp_def image_def relInvImage_def by auto
   326 
   327 lemma relImage_mono:
   328 "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
   329 unfolding relImage_def by auto
   330 
   331 lemma relInvImage_mono:
   332 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
   333 unfolding relInvImage_def by auto
   334 
   335 lemma relInvImage_diag:
   336 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
   337 unfolding relInvImage_def diag_def by auto
   338 
   339 lemma relInvImage_UNIV_relImage:
   340 "R \<subseteq> relInvImage UNIV (relImage R f) f"
   341 unfolding relInvImage_def relImage_def by auto
   342 
   343 lemma relImage_proj:
   344 assumes "equiv A R"
   345 shows "relImage R (proj R) \<subseteq> diag (A//R)"
   346 unfolding relImage_def diag_def apply safe
   347 using proj_iff[OF assms]
   348 by (metis assms equiv_Image proj_def proj_preserves)
   349 
   350 lemma relImage_relInvImage:
   351 assumes "R \<subseteq> f ` A <*> f ` A"
   352 shows "relImage (relInvImage A R f) f = R"
   353 using assms unfolding relImage_def relInvImage_def by fastforce
   354 
   355 
   356 (* Relation composition as a weak pseudo-pullback *)
   357 
   358 (* pick middle *)
   359 definition "pickM P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
   360 
   361 lemma pickM:
   362 assumes "(a,c) \<in> P O Q"
   363 shows "(a, pickM P Q a c) \<in> P \<and> (pickM P Q a c, c) \<in> Q"
   364 unfolding pickM_def apply(rule someI_ex)
   365 using assms unfolding relcomp_def by auto
   366 
   367 definition fstO where "fstO P Q ac = (fst ac, pickM P Q (fst ac) (snd ac))"
   368 definition sndO where "sndO P Q ac = (pickM P Q (fst ac) (snd ac), snd ac)"
   369 
   370 lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
   371 by (metis assms fstO_def pickM surjective_pairing)
   372 
   373 lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
   374 unfolding comp_def fstO_def by simp
   375 
   376 lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
   377 unfolding comp_def sndO_def by simp
   378 
   379 lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
   380 by (metis assms sndO_def pickM surjective_pairing)
   381 
   382 lemma csquare_fstO_sndO:
   383 "csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
   384 unfolding csquare_def fstO_def sndO_def using pickM by auto
   385 
   386 lemma wppull_fstO_sndO:
   387 shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
   388 using pickM unfolding wppull_def fstO_def sndO_def relcomp_def by auto
   389 
   390 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
   391 by simp
   392 
   393 lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
   394 by (simp split: prod.split)
   395 
   396 lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
   397 by (simp split: prod.split)
   398 
   399 lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
   400 by auto
   401 
   402 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
   403 by simp
   404 
   405 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
   406 by simp
   407 
   408 lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
   409 by simp
   410 
   411 lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
   412 by simp
   413 
   414 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
   415 by simp
   416 
   417 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
   418 by simp
   419 
   420 lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
   421 by auto
   422 
   423 lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
   424 by auto
   425 
   426 lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
   427 by auto
   428 
   429 lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j"
   430 unfolding rel.underS_def by simp
   431 
   432 lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
   433 unfolding rel.underS_def by simp
   434 
   435 lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R"
   436 unfolding rel.underS_def Field_def by auto
   437 
   438 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
   439 unfolding Field_def by auto
   440 
   441 
   442 subsection {* Convolution product *}
   443 
   444 definition convol ("<_ , _>") where
   445 "<f , g> \<equiv> %a. (f a, g a)"
   446 
   447 lemma fst_convol:
   448 "fst o <f , g> = f"
   449 apply(rule ext)
   450 unfolding convol_def by simp
   451 
   452 lemma snd_convol:
   453 "snd o <f , g> = g"
   454 apply(rule ext)
   455 unfolding convol_def by simp
   456 
   457 lemma fst_convol': "fst (<f, g> x) = f x"
   458 using fst_convol unfolding convol_def by simp
   459 
   460 lemma snd_convol': "snd (<f, g> x) = g x"
   461 using snd_convol unfolding convol_def by simp
   462 
   463 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"
   464 unfolding convol_def by auto
   465 
   466 lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
   467 unfolding convol_def by auto
   468 
   469 subsection{* Facts about functions *}
   470 
   471 lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
   472 unfolding o_def fun_eq_iff by simp
   473 
   474 lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
   475 unfolding o_def fun_eq_iff by simp
   476 
   477 definition inver where
   478   "inver g f A = (ALL a : A. g (f a) = a)"
   479 
   480 lemma bij_betw_iff_ex:
   481   "bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R")
   482 proof (rule iffI)
   483   assume ?L
   484   hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto
   485   let ?phi = "% b a. a : A \<and> f a = b"
   486   have "ALL b : B. EX a. ?phi b a" using f by blast
   487   then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b"
   488     using bchoice[of B ?phi] by blast
   489   hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
   490   have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f)
   491   moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
   492   moreover have "A \<le> g ` B"
   493   proof safe
   494     fix a assume a: "a : A"
   495     hence "f a : B" using f by auto
   496     moreover have "a = g (f a)" using a gf unfolding inver_def by auto
   497     ultimately show "a : g ` B" by blast
   498   qed
   499   ultimately show ?R by blast
   500 next
   501   assume ?R
   502   then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast
   503   show ?L unfolding bij_betw_def
   504   proof safe
   505     show "inj_on f A" unfolding inj_on_def
   506     proof safe
   507       fix a1 a2 assume a: "a1 : A"  "a2 : A" and "f a1 = f a2"
   508       hence "g (f a1) = g (f a2)" by simp
   509       thus "a1 = a2" using a g unfolding inver_def by simp
   510     qed
   511   next
   512     fix a assume "a : A"
   513     then obtain b where b: "b : B" and a: "a = g b" using g by blast
   514     hence "b = f (g b)" using g unfolding inver_def by auto
   515     thus "f a : B" unfolding a using b by simp
   516   next
   517     fix b assume "b : B"
   518     hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto
   519     thus "b : f ` A" by auto
   520   qed
   521 qed
   522 
   523 lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
   524 unfolding bij_def inj_on_def by auto blast
   525 
   526 lemma bij_betw_ex_weakE:
   527   "\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B"
   528 by (auto simp only: bij_betw_iff_ex)
   529 
   530 lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A"
   531 unfolding inver_def by auto (rule rev_image_eqI, auto)
   532 
   533 lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A"
   534 unfolding inver_def by auto
   535 
   536 lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)"
   537 unfolding inver_def by simp
   538 
   539 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
   540 unfolding bij_betw_def by auto
   541 
   542 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
   543 unfolding bij_betw_def by auto
   544 
   545 lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x"
   546 unfolding inver_def by auto
   547 
   548 lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A"
   549 unfolding bij_betw_def inver_def by auto
   550 
   551 lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B"
   552 unfolding bij_betw_def inver_def by auto
   553 
   554 lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B"
   555 by (metis bij_betw_iff_ex bij_betw_imageE)
   556 
   557 lemma bij_betwI':
   558   "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
   559     \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
   560     \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
   561 unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI)
   562 
   563 lemma o_bij:
   564   assumes gf: "g o f = id" and fg: "f o g = id"
   565   shows "bij f"
   566 unfolding bij_def inj_on_def surj_def proof safe
   567   fix a1 a2 assume "f a1 = f a2"
   568   hence "g ( f a1) = g (f a2)" by simp
   569   thus "a1 = a2" using gf unfolding fun_eq_iff by simp
   570 next
   571   fix b
   572   have "b = f (g b)"
   573   using fg unfolding fun_eq_iff by simp
   574   thus "EX a. b = f a" by blast
   575 qed
   576 
   577 lemma surj_fun_eq:
   578   assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
   579   shows "g1 = g2"
   580 proof (rule ext)
   581   fix y
   582   from surj_on obtain x where "x \<in> X" and "y = f x" by blast
   583   thus "g1 y = g2 y" using eq_on by simp
   584 qed
   585 
   586 lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
   587 unfolding wo_rel_def card_order_on_def by blast 
   588 
   589 lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
   590   \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
   591 unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
   592 
   593 lemma Card_order_trans:
   594   "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
   595 unfolding card_order_on_def well_order_on_def linear_order_on_def
   596   partial_order_on_def preorder_on_def trans_def antisym_def by blast
   597 
   598 lemma Cinfinite_limit2:
   599  assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
   600  shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
   601 proof -
   602   from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
   603     unfolding card_order_on_def well_order_on_def linear_order_on_def
   604       partial_order_on_def preorder_on_def by auto
   605   obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
   606     using Cinfinite_limit[OF x1 r] by blast
   607   obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
   608     using Cinfinite_limit[OF x2 r] by blast
   609   show ?thesis
   610   proof (cases "y1 = y2")
   611     case True with y1 y2 show ?thesis by blast
   612   next
   613     case False
   614     with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
   615       unfolding total_on_def by auto
   616     thus ?thesis
   617     proof
   618       assume *: "(y1, y2) \<in> r"
   619       with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
   620       with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
   621     next
   622       assume *: "(y2, y1) \<in> r"
   623       with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
   624       with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
   625     qed
   626   qed
   627 qed
   628 
   629 lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
   630  \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
   631 proof (induct X rule: finite_induct)
   632   case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
   633 next
   634   case (insert x X)
   635   then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
   636   then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r"
   637     using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
   638   show ?case by (metis Card_order_trans insert(5) insertE y(2) z)
   639 qed
   640 
   641 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
   642 by auto
   643 
   644 (*helps resolution*)
   645 lemma well_order_induct_imp:
   646   "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
   647      x \<in> Field r \<longrightarrow> P x"
   648 by (erule wo_rel.well_order_induct)
   649 
   650 lemma meta_spec2:
   651   assumes "(\<And>x y. PROP P x y)"
   652   shows "PROP P x y"
   653 by (rule `(\<And>x y. PROP P x y)`)
   654 
   655 (*Extended Sublist*)
   656 
   657 definition prefCl where
   658   "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
   659 definition PrefCl where
   660   "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
   661 
   662 lemma prefCl_UN:
   663   "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
   664 unfolding prefCl_def PrefCl_def by fastforce
   665 
   666 definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
   667 definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
   668 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
   669 
   670 lemmas sh_def = Shift_def shift_def
   671 
   672 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
   673 unfolding Shift_def Succ_def by simp
   674 
   675 lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
   676 unfolding Shift_def clists_def Field_card_of by auto
   677 
   678 lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
   679 unfolding prefCl_def Shift_def
   680 proof safe
   681   fix kl1 kl2
   682   assume "\<forall>kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
   683     "kl1 \<le> kl2" "k # kl2 \<in> Kl"
   684   thus "k # kl1 \<in> Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast
   685 qed
   686 
   687 lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
   688 unfolding Shift_def by simp
   689 
   690 lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
   691 unfolding Succ_def proof
   692   assume "prefCl Kl" "k # kl \<in> Kl"
   693   moreover have "k # [] \<le> k # kl" by auto
   694   ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
   695   thus "[] @ [k] \<in> Kl" by simp
   696 qed
   697 
   698 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
   699 unfolding Succ_def by simp
   700 
   701 lemmas SuccE = SuccD[elim_format]
   702 
   703 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
   704 unfolding Succ_def by simp
   705 
   706 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
   707 unfolding Shift_def by simp
   708 
   709 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
   710 unfolding Succ_def Shift_def by auto
   711 
   712 lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
   713 unfolding Shift_def by simp
   714 
   715 lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
   716 unfolding cexp_def Field_card_of by (simp only: card_of_refl)
   717 
   718 lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
   719 unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
   720 
   721 lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
   722 unfolding cpow_def clists_def
   723 by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric])
   724    (erule notE, erule ordIso_transitive, rule czero_ordIso)
   725 
   726 lemma incl_UNION_I:
   727 assumes "i \<in> I" and "A \<subseteq> F i"
   728 shows "A \<subseteq> UNION I F"
   729 using assms by auto
   730 
   731 lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
   732 unfolding clists_def Field_card_of by auto
   733 
   734 lemma Cons_clists:
   735   "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
   736 unfolding clists_def Field_card_of by auto
   737 
   738 lemma length_Cons: "length (x#xs) = Suc (length xs)"
   739 by simp
   740 
   741 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
   742 by simp
   743 
   744 (*injection into the field of a cardinal*)
   745 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
   746 definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
   747 
   748 lemma ex_toCard_pred:
   749 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
   750 unfolding toCard_pred_def
   751 using card_of_ordLeq[of A "Field r"]
   752       ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
   753 by blast
   754 
   755 lemma toCard_pred_toCard:
   756   "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
   757 unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
   758 
   759 lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
   760   toCard A r x = toCard A r y \<longleftrightarrow> x = y"
   761 using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
   762 
   763 lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
   764 using toCard_pred_toCard unfolding toCard_pred_def by blast
   765 
   766 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
   767 
   768 lemma fromCard_toCard:
   769 "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
   770 unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
   771 
   772 (* pick according to the weak pullback *)
   773 definition pickWP_pred where
   774 "pickWP_pred A p1 p2 b1 b2 a \<equiv>
   775  a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
   776 
   777 definition pickWP where
   778 "pickWP A p1 p2 b1 b2 \<equiv>
   779  SOME a. pickWP_pred A p1 p2 b1 b2 a"
   780 
   781 lemma pickWP_pred:
   782 assumes "wpull A B1 B2 f1 f2 p1 p2" and
   783 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
   784 shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a"
   785 using assms unfolding wpull_def pickWP_pred_def by blast
   786 
   787 lemma pickWP_pred_pickWP:
   788 assumes "wpull A B1 B2 f1 f2 p1 p2" and
   789 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
   790 shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)"
   791 unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred])
   792 
   793 lemma pickWP:
   794 assumes "wpull A B1 B2 f1 f2 p1 p2" and
   795 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
   796 shows "pickWP A p1 p2 b1 b2 \<in> A"
   797       "p1 (pickWP A p1 p2 b1 b2) = b1"
   798       "p2 (pickWP A p1 p2 b1 b2) = b2"
   799 using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+
   800 
   801 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
   802 
   803 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
   804 unfolding Field_card_of csum_def by auto
   805 
   806 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
   807 unfolding Field_card_of csum_def by auto
   808 
   809 lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
   810 by auto
   811 
   812 lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
   813 by auto
   814 
   815 lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
   816 by auto
   817 
   818 lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
   819 by auto
   820 
   821 lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q"
   822 by simp
   823 
   824 lemma sum_case_step:
   825   "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
   826   "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
   827 by auto
   828 
   829 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   830 by simp
   831 
   832 lemma obj_sumE_f:
   833 "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
   834 by (metis sum.exhaust)
   835 
   836 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   837 by (cases s) auto
   838 
   839 lemma obj_sum_step:
   840   "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
   841 by (metis obj_sumE)
   842 
   843 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   844 by simp
   845 
   846 end