src/HOL/Basic_BNFs.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 58916 229765cc3414
child 60758 d8d85a8172b5
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
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@58889
    10
section {* 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@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@54421
    33
bnf "'a + 'b"
blanchet@55931
    34
  map: map_sum
traytel@54421
    35
  sets: setl setr
traytel@54421
    36
  bd: natLeq
traytel@54421
    37
  wits: Inl Inr
blanchet@55943
    38
  rel: rel_sum
blanchet@48975
    39
proof -
blanchet@55931
    40
  show "map_sum id id = id" by (rule map_sum.id)
blanchet@48975
    41
next
blanchet@54486
    42
  fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
blanchet@55931
    43
  show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
blanchet@55931
    44
    by (rule map_sum.comp[symmetric])
blanchet@48975
    45
next
blanchet@54486
    46
  fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
blanchet@49451
    47
  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
blanchet@49451
    48
         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
blanchet@55931
    49
  thus "map_sum f1 f2 x = map_sum g1 g2 x"
blanchet@48975
    50
  proof (cases x)
traytel@58916
    51
    case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1))
blanchet@48975
    52
  next
traytel@58916
    53
    case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2))
blanchet@48975
    54
  qed
blanchet@48975
    55
next
blanchet@54486
    56
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@55931
    57
  show "setl o map_sum f1 f2 = image f1 o setl"
traytel@58916
    58
    by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
blanchet@48975
    59
next
blanchet@54486
    60
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@55931
    61
  show "setr o map_sum f1 f2 = image f2 o setr"
traytel@58916
    62
    by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
blanchet@48975
    63
next
blanchet@48975
    64
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
    65
next
blanchet@48975
    66
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
    67
next
blanchet@54486
    68
  fix x :: "'o + 'p"
blanchet@49451
    69
  show "|setl x| \<le>o natLeq"
blanchet@48975
    70
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    71
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
traytel@58916
    72
    by (simp add: sum_set_defs(1) split: sum.split)
blanchet@48975
    73
next
blanchet@54486
    74
  fix x :: "'o + 'p"
blanchet@49451
    75
  show "|setr x| \<le>o natLeq"
blanchet@48975
    76
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    77
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
traytel@58916
    78
    by (simp add: sum_set_defs(2) split: sum.split)
blanchet@48975
    79
next
traytel@54841
    80
  fix R1 R2 S1 S2
blanchet@55943
    81
  show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
traytel@58916
    82
    by (force elim: rel_sum.cases)
blanchet@49453
    83
next
blanchet@49453
    84
  fix R S
blanchet@55943
    85
  show "rel_sum R S =
blanchet@55931
    86
        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
blanchet@55931
    87
        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
traytel@58916
    88
  unfolding sum_set_defs Grp_def relcompp.simps conversep.simps fun_eq_iff
traytel@58916
    89
  by (fastforce elim: rel_sum.cases split: sum.splits)
blanchet@48975
    90
qed (auto simp: sum_set_defs)
blanchet@48975
    91
traytel@58916
    92
inductive_set fsts :: "'a \<times> 'b \<Rightarrow> 'a set" for p :: "'a \<times> 'b" where
traytel@58916
    93
  "fst p \<in> fsts p"
traytel@58916
    94
inductive_set snds :: "'a \<times> 'b \<Rightarrow> 'b set" for p :: "'a \<times> 'b" where
traytel@58916
    95
  "snd p \<in> snds p"
blanchet@48975
    96
traytel@58916
    97
lemma prod_set_defs[code]: "fsts = (\<lambda>p. {fst p})" "snds = (\<lambda>p. {snd p})"
traytel@58916
    98
  by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases)
blanchet@48975
    99
traytel@58916
   100
inductive
traytel@58916
   101
  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
   102
where
traytel@58916
   103
  "\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
traytel@58916
   104
traytel@58916
   105
hide_fact rel_prod_def
traytel@58916
   106
traytel@58916
   107
lemma rel_prod_apply [code, simp]:
traytel@58916
   108
  "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
traytel@58916
   109
  by (auto intro: rel_prod.intros elim: rel_prod.cases)
traytel@58916
   110
traytel@58916
   111
lemma rel_prod_conv:
blanchet@55944
   112
  "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
traytel@58916
   113
  by (rule ext, rule ext) auto
blanchet@55083
   114
traytel@54421
   115
bnf "'a \<times> 'b"
blanchet@55932
   116
  map: map_prod
traytel@54421
   117
  sets: fsts snds
traytel@54421
   118
  bd: natLeq
blanchet@55944
   119
  rel: rel_prod
blanchet@48975
   120
proof (unfold prod_set_defs)
blanchet@55932
   121
  show "map_prod id id = id" by (rule map_prod.id)
blanchet@48975
   122
next
blanchet@48975
   123
  fix f1 f2 g1 g2
blanchet@55932
   124
  show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
blanchet@55932
   125
    by (rule map_prod.comp[symmetric])
blanchet@48975
   126
next
blanchet@48975
   127
  fix x f1 f2 g1 g2
blanchet@48975
   128
  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
   129
  thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
blanchet@48975
   130
next
blanchet@48975
   131
  fix f1 f2
blanchet@55932
   132
  show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
blanchet@48975
   133
    by (rule ext, unfold o_apply) simp
blanchet@48975
   134
next
blanchet@48975
   135
  fix f1 f2
blanchet@55932
   136
  show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
blanchet@48975
   137
    by (rule ext, unfold o_apply) simp
blanchet@48975
   138
next
traytel@52635
   139
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   140
next
traytel@52635
   141
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   142
next
blanchet@48975
   143
  fix x
traytel@52635
   144
  show "|{fst x}| \<le>o natLeq"
traytel@55811
   145
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   146
next
traytel@52635
   147
  fix x
traytel@52635
   148
  show "|{snd x}| \<le>o natLeq"
traytel@55811
   149
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   150
next
traytel@54841
   151
  fix R1 R2 S1 S2
blanchet@55944
   152
  show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
blanchet@49453
   153
next
blanchet@49453
   154
  fix R S
blanchet@55944
   155
  show "rel_prod R S =
blanchet@55932
   156
        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
blanchet@55932
   157
        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
traytel@58916
   158
  unfolding prod_set_defs rel_prod_apply Grp_def relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   159
  by auto
traytel@54189
   160
qed
blanchet@48975
   161
traytel@54421
   162
bnf "'a \<Rightarrow> 'b"
traytel@54421
   163
  map: "op \<circ>"
traytel@54421
   164
  sets: range
traytel@54421
   165
  bd: "natLeq +c |UNIV :: 'a set|"
blanchet@55945
   166
  rel: "rel_fun op ="
blanchet@48975
   167
proof
blanchet@48975
   168
  fix f show "id \<circ> f = id f" by simp
blanchet@48975
   169
next
blanchet@48975
   170
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
blanchet@48975
   171
  unfolding comp_def[abs_def] ..
blanchet@48975
   172
next
blanchet@48975
   173
  fix x f g
blanchet@48975
   174
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
blanchet@48975
   175
  thus "f \<circ> x = g \<circ> x" by auto
blanchet@48975
   176
next
blanchet@48975
   177
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
haftmann@56077
   178
    by (auto simp add: fun_eq_iff)
blanchet@48975
   179
next
blanchet@48975
   180
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
blanchet@48975
   181
  apply (rule card_order_csum)
blanchet@48975
   182
  apply (rule natLeq_card_order)
blanchet@48975
   183
  by (rule card_of_card_order_on)
blanchet@48975
   184
(*  *)
blanchet@48975
   185
  show "cinfinite (natLeq +c ?U)"
blanchet@48975
   186
    apply (rule cinfinite_csum)
blanchet@48975
   187
    apply (rule disjI1)
blanchet@48975
   188
    by (rule natLeq_cinfinite)
blanchet@48975
   189
next
blanchet@48975
   190
  fix f :: "'d => 'a"
blanchet@48975
   191
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
blanchet@54486
   192
  also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
blanchet@48975
   193
  finally show "|range f| \<le>o natLeq +c ?U" .
blanchet@48975
   194
next
traytel@54841
   195
  fix R S
blanchet@55945
   196
  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
   197
next
blanchet@49463
   198
  fix R
blanchet@55945
   199
  show "rel_fun op = R =
traytel@51893
   200
        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
traytel@51893
   201
         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
blanchet@55945
   202
  unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
traytel@55811
   203
    comp_apply mem_Collect_eq split_beta bex_UNIV
traytel@55811
   204
  proof (safe, unfold fun_eq_iff[symmetric])
traytel@55811
   205
    fix x xa a b c xb y aa ba
traytel@55811
   206
    assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
traytel@55811
   207
       **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
traytel@55811
   208
    show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
traytel@55811
   209
  qed force
traytel@54189
   210
qed
traytel@54191
   211
blanchet@48975
   212
end