src/HOL/BNF/Basic_BNFs.thy
author traytel
Wed Dec 18 11:03:40 2013 +0100 (2013-12-18)
changeset 54841 af71b753c459
parent 54581 1502a1f707d9
permissions -rw-r--r--
express weak pullback property of bnfs only in terms of the relator
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
traytel@54581
    14
   (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
traytel@54581
    15
  Lifting_Sum
traytel@54581
    16
  Lifting_Product
traytel@54581
    17
  Main
blanchet@48975
    18
begin
blanchet@48975
    19
traytel@54421
    20
bnf ID: 'a
traytel@54421
    21
  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@54421
    22
  sets: "\<lambda>x. {x}"
traytel@54421
    23
  bd: natLeq
traytel@54421
    24
  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
traytel@51893
    25
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
blanchet@48975
    26
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
blanchet@49453
    27
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
blanchet@48975
    28
done
blanchet@48975
    29
traytel@54421
    30
bnf DEADID: 'a
traytel@54421
    31
  map: "id :: 'a \<Rightarrow> 'a"
traytel@54421
    32
  bd: "natLeq +c |UNIV :: 'a set|"
traytel@54421
    33
  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
traytel@54841
    34
by (auto simp add: Grp_def
traytel@51446
    35
  card_order_csum natLeq_card_order card_of_card_order_on
traytel@51446
    36
  cinfinite_csum natLeq_cinfinite)
blanchet@48975
    37
blanchet@49451
    38
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
blanchet@49451
    39
"setl x = (case x of Inl z => {z} | _ => {})"
blanchet@48975
    40
blanchet@49451
    41
definition setr :: "'a + 'b \<Rightarrow> 'b set" where
blanchet@49451
    42
"setr x = (case x of Inr z => {z} | _ => {})"
blanchet@48975
    43
blanchet@49451
    44
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
blanchet@48975
    45
traytel@54421
    46
bnf "'a + 'b"
traytel@54421
    47
  map: sum_map
traytel@54421
    48
  sets: setl setr
traytel@54421
    49
  bd: natLeq
traytel@54421
    50
  wits: Inl Inr
traytel@54421
    51
  rel: sum_rel
blanchet@48975
    52
proof -
blanchet@48975
    53
  show "sum_map id id = id" by (rule sum_map.id)
blanchet@48975
    54
next
blanchet@54486
    55
  fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
blanchet@48975
    56
  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
blanchet@48975
    57
    by (rule sum_map.comp[symmetric])
blanchet@48975
    58
next
blanchet@54486
    59
  fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
blanchet@49451
    60
  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
blanchet@49451
    61
         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
blanchet@48975
    62
  thus "sum_map f1 f2 x = sum_map g1 g2 x"
blanchet@48975
    63
  proof (cases x)
blanchet@49451
    64
    case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
blanchet@48975
    65
  next
blanchet@49451
    66
    case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
blanchet@48975
    67
  qed
blanchet@48975
    68
next
blanchet@54486
    69
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@49451
    70
  show "setl o sum_map f1 f2 = image f1 o setl"
blanchet@49451
    71
    by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
blanchet@48975
    72
next
blanchet@54486
    73
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
blanchet@49451
    74
  show "setr o sum_map f1 f2 = image f2 o setr"
blanchet@49451
    75
    by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
blanchet@48975
    76
next
blanchet@48975
    77
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
    78
next
blanchet@48975
    79
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
    80
next
blanchet@54486
    81
  fix x :: "'o + 'p"
blanchet@49451
    82
  show "|setl x| \<le>o natLeq"
blanchet@48975
    83
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    84
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
    85
    by (simp add: setl_def split: sum.split)
blanchet@48975
    86
next
blanchet@54486
    87
  fix x :: "'o + 'p"
blanchet@49451
    88
  show "|setr x| \<le>o natLeq"
blanchet@48975
    89
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
    90
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@49451
    91
    by (simp add: setr_def split: sum.split)
blanchet@48975
    92
next
traytel@54841
    93
  fix R1 R2 S1 S2
traytel@54841
    94
  show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
traytel@54841
    95
    by (auto simp: sum_rel_def split: sum.splits)
blanchet@49453
    96
next
blanchet@49453
    97
  fix R S
traytel@51893
    98
  show "sum_rel R S =
traytel@51893
    99
        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
traytel@51893
   100
        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
traytel@51893
   101
  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   102
  by (fastforce split: sum.splits)
blanchet@48975
   103
qed (auto simp: sum_set_defs)
blanchet@48975
   104
blanchet@48975
   105
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
blanchet@48975
   106
"fsts x = {fst x}"
blanchet@48975
   107
blanchet@48975
   108
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
blanchet@48975
   109
"snds x = {snd x}"
blanchet@48975
   110
blanchet@48975
   111
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
blanchet@48975
   112
traytel@54421
   113
bnf "'a \<times> 'b"
traytel@54421
   114
  map: map_pair
traytel@54421
   115
  sets: fsts snds
traytel@54421
   116
  bd: natLeq
traytel@54421
   117
  rel: prod_rel
blanchet@48975
   118
proof (unfold prod_set_defs)
blanchet@48975
   119
  show "map_pair id id = id" by (rule map_pair.id)
blanchet@48975
   120
next
blanchet@48975
   121
  fix f1 f2 g1 g2
blanchet@48975
   122
  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
blanchet@48975
   123
    by (rule map_pair.comp[symmetric])
blanchet@48975
   124
next
blanchet@48975
   125
  fix x f1 f2 g1 g2
blanchet@48975
   126
  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
   127
  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
blanchet@48975
   128
next
blanchet@48975
   129
  fix f1 f2
blanchet@48975
   130
  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
blanchet@48975
   131
    by (rule ext, unfold o_apply) simp
blanchet@48975
   132
next
blanchet@48975
   133
  fix f1 f2
blanchet@48975
   134
  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
blanchet@48975
   135
    by (rule ext, unfold o_apply) simp
blanchet@48975
   136
next
traytel@52635
   137
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   138
next
traytel@52635
   139
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   140
next
blanchet@48975
   141
  fix x
traytel@52635
   142
  show "|{fst x}| \<le>o natLeq"
traytel@52635
   143
    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
blanchet@48975
   144
next
traytel@52635
   145
  fix x
traytel@52635
   146
  show "|{snd x}| \<le>o natLeq"
traytel@52635
   147
    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
blanchet@48975
   148
next
traytel@54841
   149
  fix R1 R2 S1 S2
traytel@54841
   150
  show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
blanchet@49453
   151
next
blanchet@49453
   152
  fix R S
traytel@51893
   153
  show "prod_rel R S =
traytel@51893
   154
        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
traytel@51893
   155
        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
traytel@51893
   156
  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
blanchet@49453
   157
  by auto
traytel@54189
   158
qed
blanchet@48975
   159
traytel@54421
   160
bnf "'a \<Rightarrow> 'b"
traytel@54421
   161
  map: "op \<circ>"
traytel@54421
   162
  sets: range
traytel@54421
   163
  bd: "natLeq +c |UNIV :: 'a set|"
traytel@54421
   164
  rel: "fun_rel op ="
blanchet@48975
   165
proof
blanchet@48975
   166
  fix f show "id \<circ> f = id f" by simp
blanchet@48975
   167
next
blanchet@48975
   168
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
blanchet@48975
   169
  unfolding comp_def[abs_def] ..
blanchet@48975
   170
next
blanchet@48975
   171
  fix x f g
blanchet@48975
   172
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
blanchet@48975
   173
  thus "f \<circ> x = g \<circ> x" by auto
blanchet@48975
   174
next
blanchet@48975
   175
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
blanchet@48975
   176
  unfolding image_def comp_def[abs_def] by auto
blanchet@48975
   177
next
blanchet@48975
   178
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
blanchet@48975
   179
  apply (rule card_order_csum)
blanchet@48975
   180
  apply (rule natLeq_card_order)
blanchet@48975
   181
  by (rule card_of_card_order_on)
blanchet@48975
   182
(*  *)
blanchet@48975
   183
  show "cinfinite (natLeq +c ?U)"
blanchet@48975
   184
    apply (rule cinfinite_csum)
blanchet@48975
   185
    apply (rule disjI1)
blanchet@48975
   186
    by (rule natLeq_cinfinite)
blanchet@48975
   187
next
blanchet@48975
   188
  fix f :: "'d => 'a"
blanchet@48975
   189
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
blanchet@54486
   190
  also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
blanchet@48975
   191
  finally show "|range f| \<le>o natLeq +c ?U" .
blanchet@48975
   192
next
traytel@54841
   193
  fix R S
traytel@54841
   194
  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
   195
next
blanchet@49463
   196
  fix R
traytel@51893
   197
  show "fun_rel op = R =
traytel@51893
   198
        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
traytel@51893
   199
         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
traytel@51893
   200
  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
blanchet@54486
   201
  by auto (force, metis (no_types) pair_collapse)
traytel@54189
   202
qed
traytel@54191
   203
blanchet@48975
   204
end