src/HOL/BNF/Basic_BNFs.thy
author blanchet
Tue Nov 19 01:30:14 2013 +0100 (2013-11-19)
changeset 54486 d8d276c922f2
parent 54485 b61b8c9e4cf7
child 54578 9387251b6a46
permissions -rw-r--r--
tuned proofs
blanchet@49509
     1
(*  Title:      HOL/BNF/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@48975
    16
lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
blanchet@48975
    17
blanchet@48975
    18
lemma natLeq_cinfinite: "cinfinite natLeq"
blanchet@48975
    19
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
blanchet@48975
    20
traytel@51893
    21
lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
traytel@51893
    22
  unfolding wpull_def Grp_def by auto
traytel@51893
    23
traytel@54421
    24
bnf ID: 'a
traytel@54421
    25
  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@54421
    26
  sets: "\<lambda>x. {x}"
traytel@54421
    27
  bd: natLeq
traytel@54421
    28
  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
traytel@51893
    29
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
blanchet@48975
    30
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
blanchet@49453
    31
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
blanchet@48975
    32
done
blanchet@48975
    33
traytel@54421
    34
bnf DEADID: 'a
traytel@54421
    35
  map: "id :: 'a \<Rightarrow> 'a"
traytel@54421
    36
  bd: "natLeq +c |UNIV :: 'a set|"
traytel@54421
    37
  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
traytel@52635
    38
by (auto simp add: wpull_Grp_def Grp_def
traytel@51446
    39
  card_order_csum natLeq_card_order card_of_card_order_on
traytel@51446
    40
  cinfinite_csum natLeq_cinfinite)
blanchet@48975
    41
blanchet@49451
    42
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
blanchet@49451
    43
"setl x = (case x of Inl z => {z} | _ => {})"
blanchet@48975
    44
blanchet@49451
    45
definition setr :: "'a + 'b \<Rightarrow> 'b set" where
blanchet@49451
    46
"setr x = (case x of Inr z => {z} | _ => {})"
blanchet@48975
    47
blanchet@49451
    48
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
blanchet@48975
    49
traytel@54421
    50
bnf "'a + 'b"
traytel@54421
    51
  map: sum_map
traytel@54421
    52
  sets: setl setr
traytel@54421
    53
  bd: natLeq
traytel@54421
    54
  wits: Inl Inr
traytel@54421
    55
  rel: sum_rel
blanchet@48975
    56
proof -
blanchet@48975
    57
  show "sum_map id id = id" by (rule sum_map.id)
blanchet@48975
    58
next
blanchet@54486
    59
  fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
blanchet@48975
    60
  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
blanchet@48975
    61
    by (rule sum_map.comp[symmetric])
blanchet@48975
    62
next
blanchet@54486
    63
  fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
blanchet@49451
    64
  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
blanchet@49451
    65
         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
blanchet@48975
    66
  thus "sum_map f1 f2 x = sum_map g1 g2 x"
blanchet@48975
    67
  proof (cases x)
blanchet@49451
    68
    case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
blanchet@48975
    69
  next
blanchet@49451
    70
    case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
blanchet@48975
    71
  qed
blanchet@48975
    72
next
blanchet@54486
    73
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@49451
    74
  show "setl o sum_map f1 f2 = image f1 o setl"
blanchet@49451
    75
    by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
blanchet@48975
    76
next
blanchet@54486
    77
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@49451
    78
  show "setr o sum_map f1 f2 = image f2 o setr"
blanchet@49451
    79
    by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
blanchet@48975
    80
next
blanchet@48975
    81
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
    82
next
blanchet@48975
    83
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
    84
next
blanchet@54486
    85
  fix x :: "'o + 'p"
blanchet@49451
    86
  show "|setl x| \<le>o natLeq"
blanchet@48975
    87
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    88
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
    89
    by (simp add: setl_def split: sum.split)
blanchet@48975
    90
next
blanchet@54486
    91
  fix x :: "'o + 'p"
blanchet@49451
    92
  show "|setr x| \<le>o natLeq"
blanchet@48975
    93
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    94
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
    95
    by (simp add: setr_def split: sum.split)
blanchet@48975
    96
next
blanchet@48975
    97
  fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
blanchet@48975
    98
  assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
blanchet@48975
    99
  hence
blanchet@48975
   100
    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
   101
    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
   102
    unfolding wpull_def by blast+
blanchet@49451
   103
  show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}
blanchet@49451
   104
  {x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22}
blanchet@48975
   105
  (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
blanchet@48975
   106
    (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
blanchet@48975
   107
  proof (unfold wpull_def)
blanchet@48975
   108
    { fix B1 B2
blanchet@48975
   109
      assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
blanchet@48975
   110
      have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
blanchet@48975
   111
      proof (cases B1)
blanchet@48975
   112
        case (Inl b1)
blanchet@48975
   113
        { fix b2 assume "B2 = Inr b2"
blanchet@48975
   114
          with Inl *(3) have False by simp
blanchet@48975
   115
        } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
blanchet@48975
   116
        with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
blanchet@49451
   117
        by (simp add: setl_def)+
blanchet@48975
   118
        with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
blanchet@48975
   119
        with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
blanchet@48975
   120
        by (simp add: sum_set_defs)+
blanchet@48975
   121
        thus ?thesis by blast
blanchet@48975
   122
      next
blanchet@48975
   123
        case (Inr b1)
blanchet@48975
   124
        { fix b2 assume "B2 = Inl b2"
blanchet@48975
   125
          with Inr *(3) have False by simp
blanchet@48975
   126
        } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
blanchet@48975
   127
        with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
blanchet@48975
   128
        by (simp add: sum_set_defs)+
blanchet@48975
   129
        with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
blanchet@48975
   130
        with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
blanchet@48975
   131
        by (simp add: sum_set_defs)+
blanchet@48975
   132
        thus ?thesis by blast
blanchet@48975
   133
      qed
blanchet@48975
   134
    }
blanchet@48975
   135
    thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
blanchet@48975
   136
      (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
blanchet@48975
   137
  qed
blanchet@49453
   138
next
blanchet@49453
   139
  fix R S
traytel@51893
   140
  show "sum_rel R S =
traytel@51893
   141
        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
traytel@51893
   142
        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
traytel@51893
   143
  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   144
  by (fastforce split: sum.splits)
blanchet@48975
   145
qed (auto simp: sum_set_defs)
blanchet@48975
   146
blanchet@48975
   147
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
blanchet@48975
   148
"fsts x = {fst x}"
blanchet@48975
   149
blanchet@48975
   150
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
blanchet@48975
   151
"snds x = {snd x}"
blanchet@48975
   152
blanchet@48975
   153
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
blanchet@48975
   154
traytel@54421
   155
bnf "'a \<times> 'b"
traytel@54421
   156
  map: map_pair
traytel@54421
   157
  sets: fsts snds
traytel@54421
   158
  bd: natLeq
traytel@54421
   159
  rel: prod_rel
blanchet@48975
   160
proof (unfold prod_set_defs)
blanchet@48975
   161
  show "map_pair id id = id" by (rule map_pair.id)
blanchet@48975
   162
next
blanchet@48975
   163
  fix f1 f2 g1 g2
blanchet@48975
   164
  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
blanchet@48975
   165
    by (rule map_pair.comp[symmetric])
blanchet@48975
   166
next
blanchet@48975
   167
  fix x f1 f2 g1 g2
blanchet@48975
   168
  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
   169
  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
blanchet@48975
   170
next
blanchet@48975
   171
  fix f1 f2
blanchet@48975
   172
  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
blanchet@48975
   173
    by (rule ext, unfold o_apply) simp
blanchet@48975
   174
next
blanchet@48975
   175
  fix f1 f2
blanchet@48975
   176
  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
blanchet@48975
   177
    by (rule ext, unfold o_apply) simp
blanchet@48975
   178
next
traytel@52635
   179
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   180
next
traytel@52635
   181
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   182
next
blanchet@48975
   183
  fix x
traytel@52635
   184
  show "|{fst x}| \<le>o natLeq"
traytel@52635
   185
    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
blanchet@48975
   186
next
traytel@52635
   187
  fix x
traytel@52635
   188
  show "|{snd x}| \<le>o natLeq"
traytel@52635
   189
    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
blanchet@48975
   190
next
blanchet@48975
   191
  fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
blanchet@48975
   192
  assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
blanchet@48975
   193
  thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
blanchet@48975
   194
    {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
blanchet@48975
   195
   (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
blanchet@48975
   196
    unfolding wpull_def by simp fast
blanchet@49453
   197
next
blanchet@49453
   198
  fix R S
traytel@51893
   199
  show "prod_rel R S =
traytel@51893
   200
        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
traytel@51893
   201
        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
traytel@51893
   202
  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   203
  by auto
traytel@54189
   204
qed
blanchet@48975
   205
blanchet@48975
   206
(* Categorical version of pullback: *)
blanchet@48975
   207
lemma wpull_cat:
blanchet@48975
   208
assumes p: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   209
and c: "f1 o q1 = f2 o q2"
blanchet@48975
   210
and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
blanchet@48975
   211
obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
blanchet@48975
   212
proof-
blanchet@48975
   213
  have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
blanchet@48975
   214
  proof safe
blanchet@48975
   215
    fix d
blanchet@48975
   216
    have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
blanchet@48975
   217
    moreover
blanchet@48975
   218
    have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
blanchet@48975
   219
    ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
blanchet@48975
   220
      using p unfolding wpull_def by auto
blanchet@48975
   221
  qed
blanchet@48975
   222
  then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
blanchet@48975
   223
  thus ?thesis using that by fastforce
blanchet@48975
   224
qed
blanchet@48975
   225
traytel@54421
   226
bnf "'a \<Rightarrow> 'b"
traytel@54421
   227
  map: "op \<circ>"
traytel@54421
   228
  sets: range
traytel@54421
   229
  bd: "natLeq +c |UNIV :: 'a set|"
traytel@54421
   230
  rel: "fun_rel op ="
blanchet@48975
   231
proof
blanchet@48975
   232
  fix f show "id \<circ> f = id f" by simp
blanchet@48975
   233
next
blanchet@48975
   234
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
blanchet@48975
   235
  unfolding comp_def[abs_def] ..
blanchet@48975
   236
next
blanchet@48975
   237
  fix x f g
blanchet@48975
   238
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
blanchet@48975
   239
  thus "f \<circ> x = g \<circ> x" by auto
blanchet@48975
   240
next
blanchet@48975
   241
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
blanchet@48975
   242
  unfolding image_def comp_def[abs_def] by auto
blanchet@48975
   243
next
blanchet@48975
   244
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
blanchet@48975
   245
  apply (rule card_order_csum)
blanchet@48975
   246
  apply (rule natLeq_card_order)
blanchet@48975
   247
  by (rule card_of_card_order_on)
blanchet@48975
   248
(*  *)
blanchet@48975
   249
  show "cinfinite (natLeq +c ?U)"
blanchet@48975
   250
    apply (rule cinfinite_csum)
blanchet@48975
   251
    apply (rule disjI1)
blanchet@48975
   252
    by (rule natLeq_cinfinite)
blanchet@48975
   253
next
blanchet@48975
   254
  fix f :: "'d => 'a"
blanchet@48975
   255
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
blanchet@54486
   256
  also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
blanchet@48975
   257
  finally show "|range f| \<le>o natLeq +c ?U" .
blanchet@48975
   258
next
blanchet@48975
   259
  fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   260
  show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
blanchet@48975
   261
    (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
blanchet@48975
   262
  unfolding wpull_def
blanchet@48975
   263
  proof safe
blanchet@48975
   264
    fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
blanchet@48975
   265
    and c: "f1 \<circ> g1 = f2 \<circ> g2"
blanchet@48975
   266
    show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
blanchet@48975
   267
    using wpull_cat[OF p c r] by simp metis
blanchet@48975
   268
  qed
blanchet@49453
   269
next
blanchet@49463
   270
  fix R
traytel@51893
   271
  show "fun_rel op = R =
traytel@51893
   272
        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
traytel@51893
   273
         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
traytel@51893
   274
  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
blanchet@54486
   275
  by auto (force, metis (no_types) pair_collapse)
traytel@54189
   276
qed
traytel@54191
   277
blanchet@48975
   278
end