src/HOL/Datatype.thy
author krauss
Fri May 05 17:17:21 2006 +0200 (2006-05-05)
changeset 19564 d3e2f532459a
parent 19347 e2e709f3f955
child 19770 be5c23ebe1eb
permissions -rw-r--r--
First usable version of the new function definition package (HOL/function_packake/...).
Moved Accessible_Part.thy from Library to Main.
berghofe@5181
     1
(*  Title:      HOL/Datatype.thy
berghofe@5181
     2
    ID:         $Id$
wenzelm@11954
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
berghofe@5181
     4
*)
berghofe@5181
     5
wenzelm@12918
     6
header {* Datatypes *}
wenzelm@11954
     7
nipkow@15131
     8
theory Datatype
krauss@19564
     9
imports Datatype_Universe FunDef
krauss@19564
    10
uses ("Tools/function_package/fundef_datatype.ML")
nipkow@15131
    11
begin
wenzelm@11954
    12
wenzelm@11954
    13
subsection {* Representing primitive types *}
berghofe@5181
    14
berghofe@5759
    15
rep_datatype bool
wenzelm@11954
    16
  distinct True_not_False False_not_True
wenzelm@11954
    17
  induction bool_induct
wenzelm@11954
    18
wenzelm@11954
    19
declare case_split [cases type: bool]
wenzelm@11954
    20
  -- "prefer plain propositional version"
wenzelm@11954
    21
wenzelm@11954
    22
rep_datatype unit
wenzelm@11954
    23
  induction unit_induct
berghofe@5181
    24
berghofe@5181
    25
rep_datatype prod
wenzelm@11954
    26
  inject Pair_eq
wenzelm@11954
    27
  induction prod_induct
wenzelm@11954
    28
wenzelm@12918
    29
rep_datatype sum
wenzelm@12918
    30
  distinct Inl_not_Inr Inr_not_Inl
wenzelm@12918
    31
  inject Inl_eq Inr_eq
wenzelm@12918
    32
  induction sum_induct
wenzelm@12918
    33
wenzelm@12918
    34
ML {*
wenzelm@12918
    35
  val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
wenzelm@12918
    36
  bind_thm ("sum_case_Inl", sum_case_Inl);
wenzelm@12918
    37
  bind_thm ("sum_case_Inr", sum_case_Inr);
wenzelm@12918
    38
*} -- {* compatibility *}
wenzelm@12918
    39
wenzelm@12918
    40
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
wenzelm@12918
    41
  apply (rule_tac s = s in sumE)
wenzelm@12918
    42
   apply (erule ssubst)
wenzelm@12918
    43
   apply (rule sum_case_Inl)
wenzelm@12918
    44
  apply (erule ssubst)
wenzelm@12918
    45
  apply (rule sum_case_Inr)
wenzelm@12918
    46
  done
wenzelm@12918
    47
wenzelm@12918
    48
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
wenzelm@12918
    49
  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
wenzelm@12918
    50
  by (erule arg_cong)
wenzelm@12918
    51
wenzelm@12918
    52
lemma sum_case_inject:
wenzelm@12918
    53
  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
wenzelm@12918
    54
proof -
wenzelm@12918
    55
  assume a: "sum_case f1 f2 = sum_case g1 g2"
wenzelm@12918
    56
  assume r: "f1 = g1 ==> f2 = g2 ==> P"
wenzelm@12918
    57
  show P
wenzelm@12918
    58
    apply (rule r)
wenzelm@12918
    59
     apply (rule ext)
paulson@14208
    60
     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
wenzelm@12918
    61
    apply (rule ext)
paulson@14208
    62
    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
wenzelm@12918
    63
    done
wenzelm@12918
    64
qed
wenzelm@12918
    65
berghofe@13635
    66
constdefs
berghofe@13635
    67
  Suml :: "('a => 'c) => 'a + 'b => 'c"
berghofe@13635
    68
  "Suml == (%f. sum_case f arbitrary)"
berghofe@13635
    69
berghofe@13635
    70
  Sumr :: "('b => 'c) => 'a + 'b => 'c"
berghofe@13635
    71
  "Sumr == sum_case arbitrary"
berghofe@13635
    72
berghofe@13635
    73
lemma Suml_inject: "Suml f = Suml g ==> f = g"
berghofe@13635
    74
  by (unfold Suml_def) (erule sum_case_inject)
berghofe@13635
    75
berghofe@13635
    76
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
berghofe@13635
    77
  by (unfold Sumr_def) (erule sum_case_inject)
berghofe@13635
    78
berghofe@13635
    79
berghofe@13635
    80
subsection {* Finishing the datatype package setup *}
berghofe@13635
    81
berghofe@13635
    82
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
wenzelm@18230
    83
hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
wenzelm@18230
    84
hide (open) type node item
berghofe@13635
    85
wenzelm@12918
    86
wenzelm@12918
    87
subsection {* Further cases/induct rules for tuples *}
wenzelm@11954
    88
wenzelm@11954
    89
lemma prod_cases3 [case_names fields, cases type]:
wenzelm@11954
    90
    "(!!a b c. y = (a, b, c) ==> P) ==> P"
wenzelm@11954
    91
  apply (cases y)
paulson@14208
    92
  apply (case_tac b, blast)
wenzelm@11954
    93
  done
wenzelm@11954
    94
wenzelm@11954
    95
lemma prod_induct3 [case_names fields, induct type]:
wenzelm@11954
    96
    "(!!a b c. P (a, b, c)) ==> P x"
wenzelm@11954
    97
  by (cases x) blast
wenzelm@11954
    98
wenzelm@11954
    99
lemma prod_cases4 [case_names fields, cases type]:
wenzelm@11954
   100
    "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
wenzelm@11954
   101
  apply (cases y)
paulson@14208
   102
  apply (case_tac c, blast)
wenzelm@11954
   103
  done
wenzelm@11954
   104
wenzelm@11954
   105
lemma prod_induct4 [case_names fields, induct type]:
wenzelm@11954
   106
    "(!!a b c d. P (a, b, c, d)) ==> P x"
wenzelm@11954
   107
  by (cases x) blast
berghofe@5181
   108
wenzelm@11954
   109
lemma prod_cases5 [case_names fields, cases type]:
wenzelm@11954
   110
    "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
wenzelm@11954
   111
  apply (cases y)
paulson@14208
   112
  apply (case_tac d, blast)
wenzelm@11954
   113
  done
wenzelm@11954
   114
wenzelm@11954
   115
lemma prod_induct5 [case_names fields, induct type]:
wenzelm@11954
   116
    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
wenzelm@11954
   117
  by (cases x) blast
wenzelm@11954
   118
wenzelm@11954
   119
lemma prod_cases6 [case_names fields, cases type]:
wenzelm@11954
   120
    "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
wenzelm@11954
   121
  apply (cases y)
paulson@14208
   122
  apply (case_tac e, blast)
wenzelm@11954
   123
  done
wenzelm@11954
   124
wenzelm@11954
   125
lemma prod_induct6 [case_names fields, induct type]:
wenzelm@11954
   126
    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
wenzelm@11954
   127
  by (cases x) blast
wenzelm@11954
   128
wenzelm@11954
   129
lemma prod_cases7 [case_names fields, cases type]:
wenzelm@11954
   130
    "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
wenzelm@11954
   131
  apply (cases y)
paulson@14208
   132
  apply (case_tac f, blast)
wenzelm@11954
   133
  done
wenzelm@11954
   134
wenzelm@11954
   135
lemma prod_induct7 [case_names fields, induct type]:
wenzelm@11954
   136
    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
wenzelm@11954
   137
  by (cases x) blast
berghofe@5759
   138
wenzelm@12918
   139
wenzelm@12918
   140
subsection {* The option type *}
wenzelm@12918
   141
wenzelm@12918
   142
datatype 'a option = None | Some 'a
wenzelm@12918
   143
nipkow@18576
   144
lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)"
nipkow@18576
   145
  by (induct x) auto
nipkow@18576
   146
nipkow@18576
   147
lemma not_Some_eq[iff]: "(ALL y. x ~= Some y) = (x = None)"
paulson@18447
   148
  by (induct x) auto
paulson@18447
   149
nipkow@18576
   150
text{*Although it may appear that both of these equalities are helpful
nipkow@18576
   151
only when applied to assumptions, in practice it seems better to give
nipkow@18576
   152
them the uniform iff attribute. *}
wenzelm@12918
   153
nipkow@18576
   154
(*
paulson@18447
   155
lemmas not_None_eq_D = not_None_eq [THEN iffD1]
paulson@18447
   156
declare not_None_eq_D [dest!]
paulson@18447
   157
paulson@18447
   158
lemmas not_Some_eq_D = not_Some_eq [THEN iffD1]
paulson@18447
   159
declare not_Some_eq_D [dest!]
nipkow@18576
   160
*)
wenzelm@12918
   161
wenzelm@12918
   162
lemma option_caseE:
wenzelm@12918
   163
  "(case x of None => P | Some y => Q y) ==>
wenzelm@12918
   164
    (x = None ==> P ==> R) ==>
wenzelm@12918
   165
    (!!y. x = Some y ==> Q y ==> R) ==> R"
wenzelm@12918
   166
  by (cases x) simp_all
wenzelm@12918
   167
wenzelm@12918
   168
wenzelm@12918
   169
subsubsection {* Operations *}
wenzelm@12918
   170
wenzelm@12918
   171
consts
wenzelm@12918
   172
  the :: "'a option => 'a"
wenzelm@12918
   173
primrec
wenzelm@12918
   174
  "the (Some x) = x"
wenzelm@12918
   175
wenzelm@12918
   176
consts
wenzelm@12918
   177
  o2s :: "'a option => 'a set"
wenzelm@12918
   178
primrec
wenzelm@12918
   179
  "o2s None = {}"
wenzelm@12918
   180
  "o2s (Some x) = {x}"
wenzelm@12918
   181
wenzelm@12918
   182
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
wenzelm@12918
   183
  by simp
wenzelm@12918
   184
wenzelm@17876
   185
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
wenzelm@12918
   186
wenzelm@12918
   187
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
wenzelm@12918
   188
  by (cases xo) auto
wenzelm@12918
   189
wenzelm@12918
   190
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
wenzelm@12918
   191
  by (cases xo) auto
wenzelm@12918
   192
wenzelm@12918
   193
wenzelm@12918
   194
constdefs
wenzelm@12918
   195
  option_map :: "('a => 'b) => ('a option => 'b option)"
wenzelm@12918
   196
  "option_map == %f y. case y of None => None | Some x => Some (f x)"
wenzelm@12918
   197
wenzelm@12918
   198
lemma option_map_None [simp]: "option_map f None = None"
wenzelm@12918
   199
  by (simp add: option_map_def)
wenzelm@12918
   200
wenzelm@12918
   201
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
wenzelm@12918
   202
  by (simp add: option_map_def)
wenzelm@12918
   203
nipkow@14187
   204
lemma option_map_is_None[iff]:
nipkow@14187
   205
 "(option_map f opt = None) = (opt = None)"
nipkow@14187
   206
by (simp add: option_map_def split add: option.split)
nipkow@14187
   207
wenzelm@12918
   208
lemma option_map_eq_Some [iff]:
wenzelm@12918
   209
    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
nipkow@14187
   210
by (simp add: option_map_def split add: option.split)
nipkow@14187
   211
nipkow@14187
   212
lemma option_map_comp:
nipkow@14187
   213
 "option_map f (option_map g opt) = option_map (f o g) opt"
nipkow@14187
   214
by (simp add: option_map_def split add: option.split)
wenzelm@12918
   215
wenzelm@12918
   216
lemma option_map_o_sum_case [simp]:
wenzelm@12918
   217
    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
wenzelm@12918
   218
  apply (rule ext)
wenzelm@12918
   219
  apply (simp split add: sum.split)
wenzelm@12918
   220
  done
wenzelm@12918
   221
wenzelm@17458
   222
lemmas [code] = imp_conv_disj
wenzelm@17458
   223
haftmann@18702
   224
subsubsection {* Codegenerator setup *}
haftmann@18702
   225
haftmann@19347
   226
lemma [code fun]:
haftmann@19138
   227
  "(\<not> True) = False" by (rule HOL.simp_thms)
haftmann@19138
   228
haftmann@19347
   229
lemma [code fun]:
haftmann@19138
   230
  "(\<not> False) = True" by (rule HOL.simp_thms)
haftmann@19138
   231
haftmann@19347
   232
lemma [code fun]:
nipkow@19179
   233
  shows "(False \<and> x) = False"
nipkow@19179
   234
  and   "(True \<and> x) = x"
nipkow@19179
   235
  and   "(x \<and> False) = False"
nipkow@19179
   236
  and   "(x \<and> True) = x" by simp_all
haftmann@19138
   237
haftmann@19347
   238
lemma [code fun]:
nipkow@19179
   239
  shows "(False \<or> x) = x"
nipkow@19179
   240
  and   "(True \<or> x) = True"
nipkow@19179
   241
  and   "(x \<or> False) = x"
nipkow@19179
   242
  and   "(x \<or> True) = True" by simp_all
haftmann@19138
   243
haftmann@19138
   244
declare
haftmann@19347
   245
  if_True [code fun]
haftmann@19347
   246
  if_False [code fun]
nipkow@19179
   247
  fst_conv [code]
nipkow@19179
   248
  snd_conv [code]
haftmann@19138
   249
haftmann@19347
   250
lemma [code unfolt]:
haftmann@19202
   251
  "1 == Suc 0" by simp
haftmann@19202
   252
haftmann@19138
   253
code_generate True False Not "op &" "op |" If
haftmann@19138
   254
haftmann@19138
   255
code_syntax_tyco bool
haftmann@19138
   256
  ml (target_atom "bool")
haftmann@19138
   257
  haskell (target_atom "Bool")
haftmann@19138
   258
haftmann@18702
   259
code_syntax_const
haftmann@18702
   260
  True
haftmann@18757
   261
    ml (target_atom "true")
haftmann@18757
   262
    haskell (target_atom "True")
haftmann@18702
   263
  False
haftmann@18757
   264
    ml (target_atom "false")
haftmann@18757
   265
    haskell (target_atom "False")
haftmann@19138
   266
  Not
haftmann@19138
   267
    ml (target_atom "not")
haftmann@19138
   268
    haskell (target_atom "not")
haftmann@19138
   269
  "op &"
haftmann@19138
   270
    ml (infixl 1 "andalso")
haftmann@19138
   271
    haskell (infixl 3 "&&")
haftmann@19138
   272
  "op |"
haftmann@19138
   273
    ml (infixl 0 "orelse")
haftmann@19138
   274
    haskell (infixl 2 "||")
haftmann@19138
   275
  If
haftmann@19138
   276
    ml (target_atom "(if __/ then __/ else __)")
haftmann@19138
   277
    haskell (target_atom "(if __/ then __/ else __)")
haftmann@19138
   278
haftmann@19138
   279
code_generate Pair
haftmann@19138
   280
haftmann@19138
   281
code_syntax_tyco
haftmann@19138
   282
  *
haftmann@19138
   283
    ml (infix 2 "*")
haftmann@19138
   284
    haskell (target_atom "(__,/ __)")
haftmann@18702
   285
haftmann@18702
   286
code_syntax_const
haftmann@18702
   287
  Pair
haftmann@18757
   288
    ml (target_atom "(__,/ __)")
haftmann@18757
   289
    haskell (target_atom "(__,/ __)")
haftmann@18702
   290
haftmann@19150
   291
code_generate Unity
haftmann@19150
   292
haftmann@19150
   293
code_syntax_tyco
haftmann@19150
   294
  unit
haftmann@19150
   295
    ml (target_atom "unit")
haftmann@19150
   296
    haskell (target_atom "()")
haftmann@19150
   297
haftmann@19150
   298
code_syntax_const
haftmann@19150
   299
  Unity
haftmann@19150
   300
    ml (target_atom "()")
haftmann@19150
   301
    haskell (target_atom "()")
haftmann@19150
   302
haftmann@19150
   303
code_generate None Some
haftmann@19150
   304
haftmann@19150
   305
code_syntax_tyco
haftmann@19150
   306
  option
haftmann@19150
   307
    ml ("_ option")
haftmann@19150
   308
    haskell ("Maybe _")
haftmann@19150
   309
haftmann@19150
   310
code_syntax_const
haftmann@19150
   311
  None
haftmann@19150
   312
    ml (target_atom "NONE")
haftmann@19150
   313
    haskell (target_atom "Nothing")
haftmann@19150
   314
  Some
haftmann@19150
   315
    ml (target_atom "SOME")
haftmann@19150
   316
    haskell (target_atom "Just")
haftmann@19150
   317
krauss@19564
   318
krauss@19564
   319
use "Tools/function_package/fundef_datatype.ML"
krauss@19564
   320
setup FundefDatatype.setup
krauss@19564
   321
krauss@19564
   322
berghofe@5181
   323
end