src/HOL/Codatatype/Basic_BNFs.thy
author blanchet
Thu Sep 20 02:42:49 2012 +0200 (2012-09-20)
changeset 49463 83ac281bcdc2
parent 49455 3cd2622d4466
child 49507 8826d5a4332b
permissions -rw-r--r--
provide predicator, define relator
blanchet@48975
     1
(*  Title:      HOL/Codatatype/Basic_BNFs.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     5
    Copyright   2012
blanchet@48975
     6
blanchet@49309
     7
Registration of basic types as bounded natural functors.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@49309
    10
header {* Registration of Basic Types as Bounded Natural Functors *}
blanchet@48975
    11
blanchet@48975
    12
theory Basic_BNFs
blanchet@49310
    13
imports BNF_Def
blanchet@48975
    14
begin
blanchet@48975
    15
blanchet@49312
    16
lemma wpull_id: "wpull UNIV B1 B2 id id id id"
blanchet@49312
    17
unfolding wpull_def by simp
blanchet@49312
    18
blanchet@48975
    19
lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
blanchet@48975
    20
blanchet@48975
    21
lemma ctwo_card_order: "card_order ctwo"
blanchet@48975
    22
using Card_order_ctwo by (unfold ctwo_def Field_card_of)
blanchet@48975
    23
blanchet@48975
    24
lemma natLeq_cinfinite: "cinfinite natLeq"
blanchet@48975
    25
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
blanchet@48975
    26
traytel@49434
    27
bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
blanchet@49463
    28
  "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
blanchet@48975
    29
apply auto
blanchet@48975
    30
apply (rule natLeq_card_order)
blanchet@48975
    31
apply (rule natLeq_cinfinite)
blanchet@48975
    32
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
blanchet@49453
    33
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
blanchet@48975
    34
apply (rule ordLeq_transitive)
blanchet@48975
    35
apply (rule ordLeq_cexp1[of natLeq])
blanchet@48975
    36
apply (rule Cinfinite_Cnotzero)
blanchet@48975
    37
apply (rule conjI)
blanchet@48975
    38
apply (rule natLeq_cinfinite)
blanchet@48975
    39
apply (rule natLeq_Card_order)
blanchet@48975
    40
apply (rule card_of_Card_order)
blanchet@48975
    41
apply (rule cexp_mono1)
blanchet@48975
    42
apply (rule ordLeq_csum1)
blanchet@48975
    43
apply (rule card_of_Card_order)
blanchet@48975
    44
apply (rule disjI2)
blanchet@48975
    45
apply (rule cone_ordLeq_cexp)
blanchet@48975
    46
apply (rule ordLeq_transitive)
blanchet@48975
    47
apply (rule cone_ordLeq_ctwo)
blanchet@48975
    48
apply (rule ordLeq_csum2)
blanchet@48975
    49
apply (rule Card_order_ctwo)
blanchet@48975
    50
apply (rule natLeq_Card_order)
blanchet@49453
    51
apply (auto simp: Gr_def fun_eq_iff)
blanchet@48975
    52
done
blanchet@48975
    53
blanchet@49463
    54
bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
blanchet@49463
    55
  "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
blanchet@48975
    56
apply (auto simp add: wpull_id)
blanchet@48975
    57
apply (rule card_order_csum)
blanchet@48975
    58
apply (rule natLeq_card_order)
blanchet@48975
    59
apply (rule card_of_card_order_on)
blanchet@48975
    60
apply (rule cinfinite_csum)
blanchet@48975
    61
apply (rule disjI1)
blanchet@48975
    62
apply (rule natLeq_cinfinite)
blanchet@48975
    63
apply (rule ordLess_imp_ordLeq)
blanchet@48975
    64
apply (rule ordLess_ordLeq_trans)
blanchet@48975
    65
apply (rule ordLess_ctwo_cexp)
blanchet@48975
    66
apply (rule card_of_Card_order)
blanchet@48975
    67
apply (rule cexp_mono2'')
blanchet@48975
    68
apply (rule ordLeq_csum2)
blanchet@48975
    69
apply (rule card_of_Card_order)
blanchet@48975
    70
apply (rule ctwo_Cnotzero)
blanchet@49453
    71
apply (rule card_of_Card_order)
blanchet@49463
    72
apply (auto simp: Id_def Gr_def fun_eq_iff)
blanchet@49453
    73
done
blanchet@48975
    74
blanchet@49451
    75
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
blanchet@49451
    76
"setl x = (case x of Inl z => {z} | _ => {})"
blanchet@48975
    77
blanchet@49451
    78
definition setr :: "'a + 'b \<Rightarrow> 'b set" where
blanchet@49451
    79
"setr x = (case x of Inr z => {z} | _ => {})"
blanchet@48975
    80
blanchet@49451
    81
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
blanchet@48975
    82
blanchet@49463
    83
definition sum_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
blanchet@49463
    84
"sum_pred \<phi> \<psi> x y =
blanchet@49463
    85
 (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
blanchet@49463
    86
          | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
blanchet@49453
    87
blanchet@49463
    88
bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_pred
blanchet@48975
    89
proof -
blanchet@48975
    90
  show "sum_map id id = id" by (rule sum_map.id)
blanchet@48975
    91
next
blanchet@48975
    92
  fix f1 f2 g1 g2
blanchet@48975
    93
  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
blanchet@48975
    94
    by (rule sum_map.comp[symmetric])
blanchet@48975
    95
next
blanchet@48975
    96
  fix x f1 f2 g1 g2
blanchet@49451
    97
  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
blanchet@49451
    98
         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
blanchet@48975
    99
  thus "sum_map f1 f2 x = sum_map g1 g2 x"
blanchet@48975
   100
  proof (cases x)
blanchet@49451
   101
    case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
blanchet@48975
   102
  next
blanchet@49451
   103
    case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
blanchet@48975
   104
  qed
blanchet@48975
   105
next
blanchet@48975
   106
  fix f1 f2
blanchet@49451
   107
  show "setl o sum_map f1 f2 = image f1 o setl"
blanchet@49451
   108
    by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
blanchet@48975
   109
next
blanchet@48975
   110
  fix f1 f2
blanchet@49451
   111
  show "setr o sum_map f1 f2 = image f2 o setr"
blanchet@49451
   112
    by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
blanchet@48975
   113
next
blanchet@48975
   114
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   115
next
blanchet@48975
   116
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   117
next
blanchet@48975
   118
  fix x
blanchet@49451
   119
  show "|setl x| \<le>o natLeq"
blanchet@48975
   120
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
   121
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
   122
    by (simp add: setl_def split: sum.split)
blanchet@48975
   123
next
blanchet@48975
   124
  fix x
blanchet@49451
   125
  show "|setr x| \<le>o natLeq"
blanchet@48975
   126
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
   127
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
   128
    by (simp add: setr_def split: sum.split)
blanchet@48975
   129
next
blanchet@48975
   130
  fix A1 :: "'a set" and A2 :: "'b set"
blanchet@48975
   131
  have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and>
blanchet@48975
   132
    (case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R")
blanchet@48975
   133
  proof safe
blanchet@48975
   134
    fix x :: "'a + 'b"
blanchet@48975
   135
    assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2"
blanchet@48975
   136
    hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+
blanchet@48975
   137
    thus "x \<in> A1 <+> A2" by blast
blanchet@48975
   138
  qed (auto split: sum.split)
blanchet@49451
   139
  show "|{x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}| \<le>o
blanchet@48975
   140
    (( |A1| +c |A2| ) +c ctwo) ^c natLeq"
blanchet@48975
   141
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   142
    apply (rule card_of_ordIso_subst)
blanchet@48975
   143
    apply (unfold sum_set_defs)
blanchet@48975
   144
    apply (rule in_alt)
blanchet@48975
   145
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   146
    apply (rule Plus_csum)
blanchet@48975
   147
    apply (rule ordLeq_transitive)
blanchet@48975
   148
    apply (rule ordLeq_csum1)
blanchet@48975
   149
    apply (rule Card_order_csum)
blanchet@48975
   150
    apply (rule ordLeq_cexp1)
blanchet@48975
   151
    apply (rule conjI)
blanchet@48975
   152
    using Field_natLeq UNIV_not_empty czeroE apply fast
blanchet@48975
   153
    apply (rule natLeq_Card_order)
blanchet@48975
   154
    by (rule Card_order_csum)
blanchet@48975
   155
next
blanchet@48975
   156
  fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
blanchet@48975
   157
  assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
blanchet@48975
   158
  hence
blanchet@48975
   159
    pull1: "\<And>b1 b2. \<lbrakk>b1 \<in> B11; b2 \<in> B21; f11 b1 = f21 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A1. p11 a = b1 \<and> p21 a = b2"
blanchet@48975
   160
    and pull2: "\<And>b1 b2. \<lbrakk>b1 \<in> B12; b2 \<in> B22; f12 b1 = f22 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A2. p12 a = b1 \<and> p22 a = b2"
blanchet@48975
   161
    unfolding wpull_def by blast+
blanchet@49451
   162
  show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}
blanchet@49451
   163
  {x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22}
blanchet@48975
   164
  (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
blanchet@48975
   165
    (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
blanchet@48975
   166
  proof (unfold wpull_def)
blanchet@48975
   167
    { fix B1 B2
blanchet@48975
   168
      assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
blanchet@48975
   169
      have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
blanchet@48975
   170
      proof (cases B1)
blanchet@48975
   171
        case (Inl b1)
blanchet@48975
   172
        { fix b2 assume "B2 = Inr b2"
blanchet@48975
   173
          with Inl *(3) have False by simp
blanchet@48975
   174
        } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
blanchet@48975
   175
        with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
blanchet@49451
   176
        by (simp add: setl_def)+
blanchet@48975
   177
        with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
blanchet@48975
   178
        with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
blanchet@48975
   179
        by (simp add: sum_set_defs)+
blanchet@48975
   180
        thus ?thesis by blast
blanchet@48975
   181
      next
blanchet@48975
   182
        case (Inr b1)
blanchet@48975
   183
        { fix b2 assume "B2 = Inl b2"
blanchet@48975
   184
          with Inr *(3) have False by simp
blanchet@48975
   185
        } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
blanchet@48975
   186
        with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
blanchet@48975
   187
        by (simp add: sum_set_defs)+
blanchet@48975
   188
        with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
blanchet@48975
   189
        with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
blanchet@48975
   190
        by (simp add: sum_set_defs)+
blanchet@48975
   191
        thus ?thesis by blast
blanchet@48975
   192
      qed
blanchet@48975
   193
    }
blanchet@48975
   194
    thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
blanchet@48975
   195
      (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
blanchet@48975
   196
  qed
blanchet@49453
   197
next
blanchet@49453
   198
  fix R S
blanchet@49463
   199
  show "{p. sum_pred (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
blanchet@49463
   200
        (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
blanchet@49463
   201
        Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
blanchet@49463
   202
  unfolding setl_def setr_def sum_pred_def Gr_def relcomp_unfold converse_unfold
blanchet@49453
   203
  by (fastforce split: sum.splits)
blanchet@48975
   204
qed (auto simp: sum_set_defs)
blanchet@48975
   205
blanchet@48975
   206
lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq"
blanchet@48975
   207
  apply (rule ordLeq_transitive)
blanchet@48975
   208
  apply (rule ordLeq_cprod2)
blanchet@48975
   209
  apply (rule ctwo_Cnotzero)
blanchet@48975
   210
  apply (auto simp: Field_card_of intro: card_of_card_order_on)
blanchet@48975
   211
  apply (rule cprod_mono2)
blanchet@48975
   212
  apply (rule ordLess_imp_ordLeq)
blanchet@48975
   213
  apply (unfold finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   214
  by simp
blanchet@48975
   215
blanchet@48975
   216
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
blanchet@48975
   217
"fsts x = {fst x}"
blanchet@48975
   218
blanchet@48975
   219
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
blanchet@48975
   220
"snds x = {snd x}"
blanchet@48975
   221
blanchet@48975
   222
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
blanchet@48975
   223
blanchet@49463
   224
definition prod_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
blanchet@49463
   225
"prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
blanchet@49453
   226
blanchet@49463
   227
bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_pred
blanchet@48975
   228
proof (unfold prod_set_defs)
blanchet@48975
   229
  show "map_pair id id = id" by (rule map_pair.id)
blanchet@48975
   230
next
blanchet@48975
   231
  fix f1 f2 g1 g2
blanchet@48975
   232
  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
blanchet@48975
   233
    by (rule map_pair.comp[symmetric])
blanchet@48975
   234
next
blanchet@48975
   235
  fix x f1 f2 g1 g2
blanchet@48975
   236
  assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
blanchet@48975
   237
  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
blanchet@48975
   238
next
blanchet@48975
   239
  fix f1 f2
blanchet@48975
   240
  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
blanchet@48975
   241
    by (rule ext, unfold o_apply) simp
blanchet@48975
   242
next
blanchet@48975
   243
  fix f1 f2
blanchet@48975
   244
  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
blanchet@48975
   245
    by (rule ext, unfold o_apply) simp
blanchet@48975
   246
next
blanchet@48975
   247
  show "card_order (ctwo *c natLeq)"
blanchet@48975
   248
    apply (rule card_order_cprod)
blanchet@48975
   249
    apply (rule ctwo_card_order)
blanchet@48975
   250
    by (rule natLeq_card_order)
blanchet@48975
   251
next
blanchet@48975
   252
  show "cinfinite (ctwo *c natLeq)"
blanchet@48975
   253
    apply (rule cinfinite_cprod2)
blanchet@48975
   254
    apply (rule ctwo_Cnotzero)
blanchet@48975
   255
    apply (rule conjI[OF _ natLeq_Card_order])
blanchet@48975
   256
    by (rule natLeq_cinfinite)
blanchet@48975
   257
next
blanchet@48975
   258
  fix x
blanchet@48975
   259
  show "|{fst x}| \<le>o ctwo *c natLeq"
blanchet@48975
   260
    by (rule singleton_ordLeq_ctwo_natLeq)
blanchet@48975
   261
next
blanchet@48975
   262
  fix x
blanchet@48975
   263
  show "|{snd x}| \<le>o ctwo *c natLeq"
blanchet@48975
   264
    by (rule singleton_ordLeq_ctwo_natLeq)
blanchet@48975
   265
next
blanchet@48975
   266
  fix A1 :: "'a set" and A2 :: "'b set"
blanchet@48975
   267
  have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto
blanchet@48975
   268
  show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o
blanchet@48975
   269
    ( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)"
blanchet@48975
   270
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   271
    apply (rule card_of_ordIso_subst)
blanchet@48975
   272
    apply (rule in_alt)
blanchet@48975
   273
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   274
    apply (rule Times_cprod)
blanchet@48975
   275
    apply (rule ordLeq_transitive)
blanchet@48975
   276
    apply (rule cprod_csum_cexp)
blanchet@48975
   277
    apply (rule cexp_mono)
blanchet@48975
   278
    apply (rule ordLeq_csum1)
blanchet@48975
   279
    apply (rule Card_order_csum)
blanchet@48975
   280
    apply (rule ordLeq_cprod1)
blanchet@48975
   281
    apply (rule Card_order_ctwo)
blanchet@48975
   282
    apply (rule Cinfinite_Cnotzero)
blanchet@48975
   283
    apply (rule conjI[OF _ natLeq_Card_order])
blanchet@48975
   284
    apply (rule natLeq_cinfinite)
blanchet@48975
   285
    apply (rule disjI2)
blanchet@48975
   286
    apply (rule cone_ordLeq_cexp)
blanchet@48975
   287
    apply (rule ordLeq_transitive)
blanchet@48975
   288
    apply (rule cone_ordLeq_ctwo)
blanchet@48975
   289
    apply (rule ordLeq_csum2)
blanchet@48975
   290
    apply (rule Card_order_ctwo)
blanchet@48975
   291
    apply (rule notE)
blanchet@48975
   292
    apply (rule ctwo_not_czero)
blanchet@48975
   293
    apply assumption
blanchet@48975
   294
    by (rule Card_order_ctwo)
blanchet@48975
   295
next
blanchet@48975
   296
  fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
blanchet@48975
   297
  assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
blanchet@48975
   298
  thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
blanchet@48975
   299
    {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
blanchet@48975
   300
   (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
blanchet@48975
   301
    unfolding wpull_def by simp fast
blanchet@49453
   302
next
blanchet@49453
   303
  fix R S
blanchet@49463
   304
  show "{p. prod_pred (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
blanchet@49463
   305
        (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
blanchet@49463
   306
        Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
blanchet@49463
   307
  unfolding prod_set_defs prod_pred_def Gr_def relcomp_unfold converse_unfold
blanchet@49453
   308
  by auto
blanchet@48975
   309
qed simp+
blanchet@48975
   310
blanchet@48975
   311
(* Categorical version of pullback: *)
blanchet@48975
   312
lemma wpull_cat:
blanchet@48975
   313
assumes p: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   314
and c: "f1 o q1 = f2 o q2"
blanchet@48975
   315
and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
blanchet@48975
   316
obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
blanchet@48975
   317
proof-
blanchet@48975
   318
  have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
blanchet@48975
   319
  proof safe
blanchet@48975
   320
    fix d
blanchet@48975
   321
    have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
blanchet@48975
   322
    moreover
blanchet@48975
   323
    have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
blanchet@48975
   324
    ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
blanchet@48975
   325
      using p unfolding wpull_def by auto
blanchet@48975
   326
  qed
blanchet@48975
   327
  then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
blanchet@48975
   328
  thus ?thesis using that by fastforce
blanchet@48975
   329
qed
blanchet@48975
   330
blanchet@48975
   331
lemma card_of_bounded_range:
blanchet@48975
   332
  "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
blanchet@48975
   333
proof -
blanchet@48975
   334
  let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None"
blanchet@48975
   335
  have "inj_on ?f ?LHS" unfolding inj_on_def
blanchet@48975
   336
  proof (unfold fun_eq_iff, safe)
blanchet@48975
   337
    fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
blanchet@48975
   338
    assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
blanchet@48975
   339
    hence "f x \<in> B" "g x \<in> B" by auto
blanchet@48975
   340
    with eq have "Some (f x) = Some (g x)" by metis
blanchet@48975
   341
    thus "f x = g x" by simp
blanchet@48975
   342
  qed
blanchet@48975
   343
  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
blanchet@48975
   344
  ultimately show ?thesis using card_of_ordLeq by fast
blanchet@48975
   345
qed
blanchet@48975
   346
blanchet@49463
   347
definition fun_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b) \<Rightarrow> bool" where
blanchet@49463
   348
"fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
blanchet@49453
   349
blanchet@49453
   350
bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
blanchet@49463
   351
  fun_pred
blanchet@48975
   352
proof
blanchet@48975
   353
  fix f show "id \<circ> f = id f" by simp
blanchet@48975
   354
next
blanchet@48975
   355
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
blanchet@48975
   356
  unfolding comp_def[abs_def] ..
blanchet@48975
   357
next
blanchet@48975
   358
  fix x f g
blanchet@48975
   359
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
blanchet@48975
   360
  thus "f \<circ> x = g \<circ> x" by auto
blanchet@48975
   361
next
blanchet@48975
   362
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
blanchet@48975
   363
  unfolding image_def comp_def[abs_def] by auto
blanchet@48975
   364
next
blanchet@48975
   365
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
blanchet@48975
   366
  apply (rule card_order_csum)
blanchet@48975
   367
  apply (rule natLeq_card_order)
blanchet@48975
   368
  by (rule card_of_card_order_on)
blanchet@48975
   369
(*  *)
blanchet@48975
   370
  show "cinfinite (natLeq +c ?U)"
blanchet@48975
   371
    apply (rule cinfinite_csum)
blanchet@48975
   372
    apply (rule disjI1)
blanchet@48975
   373
    by (rule natLeq_cinfinite)
blanchet@48975
   374
next
blanchet@48975
   375
  fix f :: "'d => 'a"
blanchet@48975
   376
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
blanchet@48975
   377
  also have "?U \<le>o natLeq +c ?U"  by (rule ordLeq_csum2) (rule card_of_Card_order)
blanchet@48975
   378
  finally show "|range f| \<le>o natLeq +c ?U" .
blanchet@48975
   379
next
blanchet@48975
   380
  fix B :: "'a set"
blanchet@48975
   381
  have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range)
blanchet@48975
   382
  also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|"
blanchet@48975
   383
    unfolding cexp_def Field_card_of by (rule card_of_refl)
blanchet@48975
   384
  also have "|B| ^c |UNIV :: 'd set| \<le>o
blanchet@48975
   385
             ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )"
blanchet@48975
   386
    apply (rule cexp_mono)
blanchet@48975
   387
     apply (rule ordLeq_csum1) apply (rule card_of_Card_order)
blanchet@48975
   388
     apply (rule ordLeq_csum2) apply (rule card_of_Card_order)
blanchet@48975
   389
     apply (rule disjI2) apply (rule cone_ordLeq_cexp)
blanchet@48975
   390
      apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2)
blanchet@48975
   391
      apply (rule Card_order_ctwo)
blanchet@48975
   392
     apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast
blanchet@48975
   393
     apply (rule card_of_Card_order)
blanchet@48975
   394
  done
blanchet@48975
   395
  finally
blanchet@48975
   396
  show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o
blanchet@48975
   397
        ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" .
blanchet@48975
   398
next
blanchet@48975
   399
  fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   400
  show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
blanchet@48975
   401
    (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
blanchet@48975
   402
  unfolding wpull_def
blanchet@48975
   403
  proof safe
blanchet@48975
   404
    fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
blanchet@48975
   405
    and c: "f1 \<circ> g1 = f2 \<circ> g2"
blanchet@48975
   406
    show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
blanchet@48975
   407
    using wpull_cat[OF p c r] by simp metis
blanchet@48975
   408
  qed
blanchet@49453
   409
next
blanchet@49463
   410
  fix R
blanchet@49463
   411
  show "{p. fun_pred (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
blanchet@49463
   412
        (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
blanchet@49463
   413
  unfolding fun_pred_def Gr_def relcomp_unfold converse_unfold
blanchet@49453
   414
  by (auto intro!: exI dest!: in_mono)
blanchet@48975
   415
qed auto
blanchet@48975
   416
blanchet@48975
   417
end