src/HOL/Basic_BNFs.thy
author blanchet
Thu Mar 06 13:36:15 2014 +0100 (2014-03-06)
changeset 55931 62156e694f3d
parent 55811 aa1acc25126b
child 55932 68c5104d2204
permissions -rw-r--r--
renamed 'map_sum' to 'sum_map'
blanchet@55075
     1
(*  Title:      HOL/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
traytel@54421
    16
bnf ID: 'a
traytel@54421
    17
  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@54421
    18
  sets: "\<lambda>x. {x}"
traytel@54421
    19
  bd: natLeq
traytel@54421
    20
  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
traytel@51893
    21
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
blanchet@48975
    22
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
blanchet@49453
    23
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
blanchet@48975
    24
done
blanchet@48975
    25
traytel@54421
    26
bnf DEADID: 'a
traytel@54421
    27
  map: "id :: 'a \<Rightarrow> 'a"
traytel@55707
    28
  bd: natLeq
traytel@54421
    29
  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
traytel@55707
    30
by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
blanchet@48975
    31
blanchet@49451
    32
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
blanchet@49451
    33
"setl x = (case x of Inl z => {z} | _ => {})"
blanchet@48975
    34
blanchet@49451
    35
definition setr :: "'a + 'b \<Rightarrow> 'b set" where
blanchet@49451
    36
"setr x = (case x of Inr z => {z} | _ => {})"
blanchet@48975
    37
blanchet@49451
    38
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
blanchet@48975
    39
blanchet@55083
    40
definition
blanchet@55083
    41
   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
blanchet@55083
    42
where
blanchet@55083
    43
   "sum_rel R1 R2 x y =
blanchet@55083
    44
     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
blanchet@55083
    45
     | (Inr x, Inr y) \<Rightarrow> R2 x y
blanchet@55083
    46
     | _ \<Rightarrow> False)"
blanchet@55083
    47
blanchet@55083
    48
lemma sum_rel_simps[simp]:
blanchet@55083
    49
  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
blanchet@55083
    50
  "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
blanchet@55083
    51
  "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
blanchet@55083
    52
  "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
blanchet@55083
    53
  unfolding sum_rel_def by simp_all
blanchet@55083
    54
traytel@54421
    55
bnf "'a + 'b"
blanchet@55931
    56
  map: map_sum
traytel@54421
    57
  sets: setl setr
traytel@54421
    58
  bd: natLeq
traytel@54421
    59
  wits: Inl Inr
traytel@54421
    60
  rel: sum_rel
blanchet@48975
    61
proof -
blanchet@55931
    62
  show "map_sum id id = id" by (rule map_sum.id)
blanchet@48975
    63
next
blanchet@54486
    64
  fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
blanchet@55931
    65
  show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
blanchet@55931
    66
    by (rule map_sum.comp[symmetric])
blanchet@48975
    67
next
blanchet@54486
    68
  fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
blanchet@49451
    69
  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
blanchet@49451
    70
         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
blanchet@55931
    71
  thus "map_sum f1 f2 x = map_sum g1 g2 x"
blanchet@48975
    72
  proof (cases x)
blanchet@49451
    73
    case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
blanchet@48975
    74
  next
blanchet@49451
    75
    case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
blanchet@48975
    76
  qed
blanchet@48975
    77
next
blanchet@54486
    78
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@55931
    79
  show "setl o map_sum f1 f2 = image f1 o setl"
blanchet@49451
    80
    by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
blanchet@48975
    81
next
blanchet@54486
    82
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@55931
    83
  show "setr o map_sum f1 f2 = image f2 o setr"
blanchet@49451
    84
    by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
blanchet@48975
    85
next
blanchet@48975
    86
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
    87
next
blanchet@48975
    88
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
    89
next
blanchet@54486
    90
  fix x :: "'o + 'p"
blanchet@49451
    91
  show "|setl x| \<le>o natLeq"
blanchet@48975
    92
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    93
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
    94
    by (simp add: setl_def split: sum.split)
blanchet@48975
    95
next
blanchet@54486
    96
  fix x :: "'o + 'p"
blanchet@49451
    97
  show "|setr x| \<le>o natLeq"
blanchet@48975
    98
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    99
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
   100
    by (simp add: setr_def split: sum.split)
blanchet@48975
   101
next
traytel@54841
   102
  fix R1 R2 S1 S2
traytel@54841
   103
  show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
traytel@54841
   104
    by (auto simp: sum_rel_def split: sum.splits)
blanchet@49453
   105
next
blanchet@49453
   106
  fix R S
traytel@51893
   107
  show "sum_rel R S =
blanchet@55931
   108
        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
blanchet@55931
   109
        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
traytel@51893
   110
  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   111
  by (fastforce split: sum.splits)
blanchet@48975
   112
qed (auto simp: sum_set_defs)
blanchet@48975
   113
blanchet@48975
   114
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
blanchet@48975
   115
"fsts x = {fst x}"
blanchet@48975
   116
blanchet@48975
   117
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
blanchet@48975
   118
"snds x = {snd x}"
blanchet@48975
   119
blanchet@48975
   120
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
blanchet@48975
   121
blanchet@55083
   122
definition
blanchet@55083
   123
  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
blanchet@55083
   124
where
blanchet@55083
   125
  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
blanchet@55083
   126
blanchet@55083
   127
lemma prod_rel_apply [simp]:
blanchet@55083
   128
  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
blanchet@55083
   129
  by (simp add: prod_rel_def)
blanchet@55083
   130
traytel@54421
   131
bnf "'a \<times> 'b"
traytel@54421
   132
  map: map_pair
traytel@54421
   133
  sets: fsts snds
traytel@54421
   134
  bd: natLeq
traytel@54421
   135
  rel: prod_rel
blanchet@48975
   136
proof (unfold prod_set_defs)
blanchet@48975
   137
  show "map_pair id id = id" by (rule map_pair.id)
blanchet@48975
   138
next
blanchet@48975
   139
  fix f1 f2 g1 g2
blanchet@48975
   140
  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
blanchet@48975
   141
    by (rule map_pair.comp[symmetric])
blanchet@48975
   142
next
blanchet@48975
   143
  fix x f1 f2 g1 g2
blanchet@48975
   144
  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
   145
  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
blanchet@48975
   146
next
blanchet@48975
   147
  fix f1 f2
blanchet@48975
   148
  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
blanchet@48975
   149
    by (rule ext, unfold o_apply) simp
blanchet@48975
   150
next
blanchet@48975
   151
  fix f1 f2
blanchet@48975
   152
  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
blanchet@48975
   153
    by (rule ext, unfold o_apply) simp
blanchet@48975
   154
next
traytel@52635
   155
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   156
next
traytel@52635
   157
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   158
next
blanchet@48975
   159
  fix x
traytel@52635
   160
  show "|{fst x}| \<le>o natLeq"
traytel@55811
   161
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   162
next
traytel@52635
   163
  fix x
traytel@52635
   164
  show "|{snd x}| \<le>o natLeq"
traytel@55811
   165
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   166
next
traytel@54841
   167
  fix R1 R2 S1 S2
traytel@54841
   168
  show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
blanchet@49453
   169
next
blanchet@49453
   170
  fix R S
traytel@51893
   171
  show "prod_rel R S =
traytel@51893
   172
        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
traytel@51893
   173
        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
traytel@51893
   174
  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   175
  by auto
traytel@54189
   176
qed
blanchet@48975
   177
traytel@54421
   178
bnf "'a \<Rightarrow> 'b"
traytel@54421
   179
  map: "op \<circ>"
traytel@54421
   180
  sets: range
traytel@54421
   181
  bd: "natLeq +c |UNIV :: 'a set|"
traytel@54421
   182
  rel: "fun_rel op ="
blanchet@48975
   183
proof
blanchet@48975
   184
  fix f show "id \<circ> f = id f" by simp
blanchet@48975
   185
next
blanchet@48975
   186
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
blanchet@48975
   187
  unfolding comp_def[abs_def] ..
blanchet@48975
   188
next
blanchet@48975
   189
  fix x f g
blanchet@48975
   190
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
blanchet@48975
   191
  thus "f \<circ> x = g \<circ> x" by auto
blanchet@48975
   192
next
blanchet@48975
   193
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
blanchet@48975
   194
  unfolding image_def comp_def[abs_def] by auto
blanchet@48975
   195
next
blanchet@48975
   196
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
blanchet@48975
   197
  apply (rule card_order_csum)
blanchet@48975
   198
  apply (rule natLeq_card_order)
blanchet@48975
   199
  by (rule card_of_card_order_on)
blanchet@48975
   200
(*  *)
blanchet@48975
   201
  show "cinfinite (natLeq +c ?U)"
blanchet@48975
   202
    apply (rule cinfinite_csum)
blanchet@48975
   203
    apply (rule disjI1)
blanchet@48975
   204
    by (rule natLeq_cinfinite)
blanchet@48975
   205
next
blanchet@48975
   206
  fix f :: "'d => 'a"
blanchet@48975
   207
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
blanchet@54486
   208
  also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
blanchet@48975
   209
  finally show "|range f| \<le>o natLeq +c ?U" .
blanchet@48975
   210
next
traytel@54841
   211
  fix R S
traytel@54841
   212
  show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
blanchet@49453
   213
next
blanchet@49463
   214
  fix R
traytel@51893
   215
  show "fun_rel op = R =
traytel@51893
   216
        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
traytel@51893
   217
         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
traytel@55811
   218
  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
traytel@55811
   219
    comp_apply mem_Collect_eq split_beta bex_UNIV
traytel@55811
   220
  proof (safe, unfold fun_eq_iff[symmetric])
traytel@55811
   221
    fix x xa a b c xb y aa ba
traytel@55811
   222
    assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
traytel@55811
   223
       **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
traytel@55811
   224
    show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
traytel@55811
   225
  qed force
traytel@54189
   226
qed
traytel@54191
   227
blanchet@48975
   228
end