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