src/HOL/Basic_BNFs.thy
author traytel
Tue Feb 16 22:28:19 2016 +0100 (2016-02-16)
changeset 62324 ae44f16dcea5
parent 61681 ca53150406c9
child 62335 e85c42f4f30a
permissions -rw-r--r--
make predicator a first-class bnf citizen
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
wenzelm@60758
    10
section \<open>Registration of Basic Types as Bounded Natural Functors\<close>
blanchet@48975
    11
blanchet@48975
    12
theory Basic_BNFs
blanchet@49310
    13
imports BNF_Def
blanchet@48975
    14
begin
blanchet@48975
    15
traytel@58916
    16
inductive_set setl :: "'a + 'b \<Rightarrow> 'a set" for s :: "'a + 'b" where
traytel@58916
    17
  "s = Inl x \<Longrightarrow> x \<in> setl s"
traytel@58916
    18
inductive_set setr :: "'a + 'b \<Rightarrow> 'b set" for s :: "'a + 'b" where
traytel@58916
    19
  "s = Inr x \<Longrightarrow> x \<in> setr s"
blanchet@48975
    20
traytel@58916
    21
lemma sum_set_defs[code]:
traytel@58916
    22
  "setl = (\<lambda>x. case x of Inl z => {z} | _ => {})"
traytel@58916
    23
  "setr = (\<lambda>x. case x of Inr z => {z} | _ => {})"
traytel@58916
    24
  by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits)
blanchet@48975
    25
traytel@58916
    26
lemma rel_sum_simps[code, simp]:
blanchet@55943
    27
  "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
blanchet@55943
    28
  "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
blanchet@55943
    29
  "rel_sum R1 R2 (Inr a2) (Inl b1) = False"
blanchet@55943
    30
  "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
traytel@58916
    31
  by (auto intro: rel_sum.intros elim: rel_sum.cases)
blanchet@55083
    32
traytel@62324
    33
inductive
traytel@62324
    34
   pred_sum :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool" for P1 P2
traytel@62324
    35
where
traytel@62324
    36
  "P1 a \<Longrightarrow> pred_sum P1 P2 (Inl a)"
traytel@62324
    37
| "P2 b \<Longrightarrow> pred_sum P1 P2 (Inr b)"
traytel@62324
    38
traytel@54421
    39
bnf "'a + 'b"
blanchet@55931
    40
  map: map_sum
traytel@54421
    41
  sets: setl setr
traytel@54421
    42
  bd: natLeq
traytel@54421
    43
  wits: Inl Inr
blanchet@55943
    44
  rel: rel_sum
traytel@62324
    45
  pred: pred_sum
blanchet@48975
    46
proof -
blanchet@55931
    47
  show "map_sum id id = id" by (rule map_sum.id)
blanchet@48975
    48
next
blanchet@54486
    49
  fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
blanchet@55931
    50
  show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
blanchet@55931
    51
    by (rule map_sum.comp[symmetric])
blanchet@48975
    52
next
blanchet@54486
    53
  fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
blanchet@49451
    54
  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
blanchet@49451
    55
         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
blanchet@55931
    56
  thus "map_sum f1 f2 x = map_sum g1 g2 x"
blanchet@48975
    57
  proof (cases x)
traytel@58916
    58
    case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1))
blanchet@48975
    59
  next
traytel@58916
    60
    case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2))
blanchet@48975
    61
  qed
blanchet@48975
    62
next
blanchet@54486
    63
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@55931
    64
  show "setl o map_sum f1 f2 = image f1 o setl"
traytel@58916
    65
    by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
blanchet@48975
    66
next
blanchet@54486
    67
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@55931
    68
  show "setr o map_sum f1 f2 = image f2 o setr"
traytel@58916
    69
    by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
blanchet@48975
    70
next
blanchet@48975
    71
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
    72
next
blanchet@48975
    73
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
    74
next
blanchet@54486
    75
  fix x :: "'o + 'p"
blanchet@49451
    76
  show "|setl x| \<le>o natLeq"
blanchet@48975
    77
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    78
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
traytel@58916
    79
    by (simp add: sum_set_defs(1) split: sum.split)
blanchet@48975
    80
next
blanchet@54486
    81
  fix x :: "'o + 'p"
blanchet@49451
    82
  show "|setr x| \<le>o natLeq"
blanchet@48975
    83
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    84
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
traytel@58916
    85
    by (simp add: sum_set_defs(2) split: sum.split)
blanchet@48975
    86
next
traytel@54841
    87
  fix R1 R2 S1 S2
blanchet@55943
    88
  show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
traytel@58916
    89
    by (force elim: rel_sum.cases)
blanchet@49453
    90
next
blanchet@49453
    91
  fix R S
traytel@62324
    92
  show "rel_sum R S = (\<lambda>x y.
traytel@62324
    93
    \<exists>z. (setl z \<subseteq> {(x, y). R x y} \<and> setr z \<subseteq> {(x, y). S x y}) \<and>
traytel@62324
    94
    map_sum fst fst z = x \<and> map_sum snd snd z = y)"
traytel@62324
    95
  unfolding sum_set_defs relcompp.simps conversep.simps fun_eq_iff
traytel@58916
    96
  by (fastforce elim: rel_sum.cases split: sum.splits)
traytel@62324
    97
qed (auto simp: sum_set_defs fun_eq_iff pred_sum.simps split: sum.splits)
blanchet@48975
    98
traytel@58916
    99
inductive_set fsts :: "'a \<times> 'b \<Rightarrow> 'a set" for p :: "'a \<times> 'b" where
traytel@58916
   100
  "fst p \<in> fsts p"
traytel@58916
   101
inductive_set snds :: "'a \<times> 'b \<Rightarrow> 'b set" for p :: "'a \<times> 'b" where
traytel@58916
   102
  "snd p \<in> snds p"
blanchet@48975
   103
traytel@58916
   104
lemma prod_set_defs[code]: "fsts = (\<lambda>p. {fst p})" "snds = (\<lambda>p. {snd p})"
traytel@58916
   105
  by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases)
blanchet@48975
   106
traytel@58916
   107
inductive
traytel@58916
   108
  rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" for R1 R2
blanchet@55083
   109
where
traytel@58916
   110
  "\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
traytel@58916
   111
traytel@62324
   112
inductive
traytel@62324
   113
  pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" for P1 P2
traytel@62324
   114
where
traytel@62324
   115
  "\<lbrakk>P1 a; P2 b\<rbrakk> \<Longrightarrow> pred_prod P1 P2 (a, b)"
traytel@62324
   116
traytel@58916
   117
lemma rel_prod_apply [code, simp]:
traytel@58916
   118
  "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
traytel@58916
   119
  by (auto intro: rel_prod.intros elim: rel_prod.cases)
traytel@58916
   120
traytel@62324
   121
lemma pred_prod_apply [code, simp]:
traytel@62324
   122
  "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
traytel@62324
   123
  by (auto intro: pred_prod.intros elim: pred_prod.cases)
traytel@62324
   124
traytel@58916
   125
lemma rel_prod_conv:
blanchet@55944
   126
  "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
traytel@58916
   127
  by (rule ext, rule ext) auto
blanchet@55083
   128
traytel@62324
   129
definition
traytel@62324
   130
  pred_fun :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
traytel@62324
   131
where
traytel@62324
   132
  "pred_fun A B = (\<lambda>f. \<forall>x. A x \<longrightarrow> B (f x))"
traytel@62324
   133
traytel@62324
   134
lemma pred_funI: "(\<And>x. A x \<Longrightarrow> B (f x)) \<Longrightarrow> pred_fun A B f"
traytel@62324
   135
  unfolding pred_fun_def by simp
traytel@62324
   136
traytel@54421
   137
bnf "'a \<times> 'b"
blanchet@55932
   138
  map: map_prod
traytel@54421
   139
  sets: fsts snds
traytel@54421
   140
  bd: natLeq
blanchet@55944
   141
  rel: rel_prod
traytel@62324
   142
  pred: pred_prod
blanchet@48975
   143
proof (unfold prod_set_defs)
blanchet@55932
   144
  show "map_prod id id = id" by (rule map_prod.id)
blanchet@48975
   145
next
blanchet@48975
   146
  fix f1 f2 g1 g2
blanchet@55932
   147
  show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
blanchet@55932
   148
    by (rule map_prod.comp[symmetric])
blanchet@48975
   149
next
blanchet@48975
   150
  fix x f1 f2 g1 g2
blanchet@48975
   151
  assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
blanchet@55932
   152
  thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
blanchet@48975
   153
next
blanchet@48975
   154
  fix f1 f2
blanchet@55932
   155
  show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
blanchet@48975
   156
    by (rule ext, unfold o_apply) simp
blanchet@48975
   157
next
blanchet@48975
   158
  fix f1 f2
blanchet@55932
   159
  show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
blanchet@48975
   160
    by (rule ext, unfold o_apply) simp
blanchet@48975
   161
next
traytel@52635
   162
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   163
next
traytel@52635
   164
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   165
next
blanchet@48975
   166
  fix x
traytel@52635
   167
  show "|{fst x}| \<le>o natLeq"
traytel@55811
   168
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   169
next
traytel@52635
   170
  fix x
traytel@52635
   171
  show "|{snd x}| \<le>o natLeq"
traytel@55811
   172
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   173
next
traytel@54841
   174
  fix R1 R2 S1 S2
blanchet@55944
   175
  show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
blanchet@49453
   176
next
blanchet@49453
   177
  fix R S
traytel@62324
   178
  show "rel_prod R S = (\<lambda>x y.
traytel@62324
   179
    \<exists>z. ({fst z} \<subseteq> {(x, y). R x y} \<and> {snd z} \<subseteq> {(x, y). S x y}) \<and>
traytel@62324
   180
      map_prod fst fst z = x \<and> map_prod snd snd z = y)"
traytel@62324
   181
  unfolding prod_set_defs rel_prod_apply relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   182
  by auto
traytel@62324
   183
qed auto
blanchet@48975
   184
traytel@54421
   185
bnf "'a \<Rightarrow> 'b"
traytel@54421
   186
  map: "op \<circ>"
traytel@54421
   187
  sets: range
traytel@54421
   188
  bd: "natLeq +c |UNIV :: 'a set|"
blanchet@55945
   189
  rel: "rel_fun op ="
traytel@62324
   190
  pred: "pred_fun (\<lambda>_. True)"
blanchet@48975
   191
proof
blanchet@48975
   192
  fix f show "id \<circ> f = id f" by simp
blanchet@48975
   193
next
blanchet@48975
   194
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
blanchet@48975
   195
  unfolding comp_def[abs_def] ..
blanchet@48975
   196
next
blanchet@48975
   197
  fix x f g
blanchet@48975
   198
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
blanchet@48975
   199
  thus "f \<circ> x = g \<circ> x" by auto
blanchet@48975
   200
next
blanchet@48975
   201
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
haftmann@56077
   202
    by (auto simp add: fun_eq_iff)
blanchet@48975
   203
next
blanchet@48975
   204
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
blanchet@48975
   205
  apply (rule card_order_csum)
blanchet@48975
   206
  apply (rule natLeq_card_order)
blanchet@48975
   207
  by (rule card_of_card_order_on)
blanchet@48975
   208
(*  *)
blanchet@48975
   209
  show "cinfinite (natLeq +c ?U)"
blanchet@48975
   210
    apply (rule cinfinite_csum)
blanchet@48975
   211
    apply (rule disjI1)
blanchet@48975
   212
    by (rule natLeq_cinfinite)
blanchet@48975
   213
next
blanchet@48975
   214
  fix f :: "'d => 'a"
blanchet@48975
   215
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
blanchet@54486
   216
  also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
blanchet@48975
   217
  finally show "|range f| \<le>o natLeq +c ?U" .
blanchet@48975
   218
next
traytel@54841
   219
  fix R S
blanchet@55945
   220
  show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def)
blanchet@49453
   221
next
blanchet@49463
   222
  fix R
traytel@62324
   223
  show "rel_fun op = R = (\<lambda>x y.
traytel@62324
   224
    \<exists>z. range z \<subseteq> {(x, y). R x y} \<and> fst \<circ> z = x \<and> snd \<circ> z = y)"
traytel@62324
   225
  unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric])
traytel@62324
   226
qed (auto simp: pred_fun_def)
traytel@54191
   227
blanchet@48975
   228
end