src/HOL/Datatype.thy
author wenzelm
Sat Sep 30 21:39:20 2006 +0200 (2006-09-30)
changeset 20798 3275b03e2fff
parent 20588 c847c56edf0c
child 20819 cb6ae81dd0be
permissions -rw-r--r--
removed obsolete sum_case_Inl/Inr;
moved 'hide' to Datatype_Universe;
tuned proofs;
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@19770
     9
imports Datatype_Universe
nipkow@15131
    10
begin
wenzelm@11954
    11
haftmann@20588
    12
setup "DatatypeCodegen.setup2"
haftmann@20588
    13
wenzelm@11954
    14
subsection {* Representing primitive types *}
berghofe@5181
    15
berghofe@5759
    16
rep_datatype bool
wenzelm@11954
    17
  distinct True_not_False False_not_True
wenzelm@11954
    18
  induction bool_induct
wenzelm@11954
    19
wenzelm@11954
    20
declare case_split [cases type: bool]
wenzelm@11954
    21
  -- "prefer plain propositional version"
wenzelm@11954
    22
wenzelm@11954
    23
rep_datatype unit
wenzelm@11954
    24
  induction unit_induct
berghofe@5181
    25
berghofe@5181
    26
rep_datatype prod
wenzelm@11954
    27
  inject Pair_eq
wenzelm@11954
    28
  induction prod_induct
wenzelm@11954
    29
wenzelm@12918
    30
rep_datatype sum
wenzelm@12918
    31
  distinct Inl_not_Inr Inr_not_Inl
wenzelm@12918
    32
  inject Inl_eq Inr_eq
wenzelm@12918
    33
  induction sum_induct
wenzelm@12918
    34
wenzelm@12918
    35
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
wenzelm@12918
    36
  apply (rule_tac s = s in sumE)
wenzelm@12918
    37
   apply (erule ssubst)
wenzelm@20798
    38
   apply (rule sum.cases(1))
wenzelm@12918
    39
  apply (erule ssubst)
wenzelm@20798
    40
  apply (rule sum.cases(2))
wenzelm@12918
    41
  done
wenzelm@12918
    42
wenzelm@12918
    43
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
wenzelm@12918
    44
  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
wenzelm@20798
    45
  by simp
wenzelm@12918
    46
wenzelm@12918
    47
lemma sum_case_inject:
wenzelm@12918
    48
  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
wenzelm@12918
    49
proof -
wenzelm@12918
    50
  assume a: "sum_case f1 f2 = sum_case g1 g2"
wenzelm@12918
    51
  assume r: "f1 = g1 ==> f2 = g2 ==> P"
wenzelm@12918
    52
  show P
wenzelm@12918
    53
    apply (rule r)
wenzelm@12918
    54
     apply (rule ext)
paulson@14208
    55
     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
wenzelm@12918
    56
    apply (rule ext)
paulson@14208
    57
    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
wenzelm@12918
    58
    done
wenzelm@12918
    59
qed
wenzelm@12918
    60
berghofe@13635
    61
constdefs
berghofe@13635
    62
  Suml :: "('a => 'c) => 'a + 'b => 'c"
berghofe@13635
    63
  "Suml == (%f. sum_case f arbitrary)"
berghofe@13635
    64
berghofe@13635
    65
  Sumr :: "('b => 'c) => 'a + 'b => 'c"
berghofe@13635
    66
  "Sumr == sum_case arbitrary"
berghofe@13635
    67
berghofe@13635
    68
lemma Suml_inject: "Suml f = Suml g ==> f = g"
berghofe@13635
    69
  by (unfold Suml_def) (erule sum_case_inject)
berghofe@13635
    70
berghofe@13635
    71
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
berghofe@13635
    72
  by (unfold Sumr_def) (erule sum_case_inject)
berghofe@13635
    73
wenzelm@20798
    74
hide (open) const Suml Sumr
berghofe@13635
    75
wenzelm@12918
    76
wenzelm@12918
    77
subsection {* Further cases/induct rules for tuples *}
wenzelm@11954
    78
wenzelm@20798
    79
lemma prod_cases3 [cases type]:
wenzelm@20798
    80
  obtains (fields) a b c where "y = (a, b, c)"
wenzelm@20798
    81
  by (cases y, case_tac b) blast
wenzelm@11954
    82
wenzelm@11954
    83
lemma prod_induct3 [case_names fields, induct type]:
wenzelm@11954
    84
    "(!!a b c. P (a, b, c)) ==> P x"
wenzelm@11954
    85
  by (cases x) blast
wenzelm@11954
    86
wenzelm@20798
    87
lemma prod_cases4 [cases type]:
wenzelm@20798
    88
  obtains (fields) a b c d where "y = (a, b, c, d)"
wenzelm@20798
    89
  by (cases y, case_tac c) blast
wenzelm@11954
    90
wenzelm@11954
    91
lemma prod_induct4 [case_names fields, induct type]:
wenzelm@11954
    92
    "(!!a b c d. P (a, b, c, d)) ==> P x"
wenzelm@11954
    93
  by (cases x) blast
berghofe@5181
    94
wenzelm@20798
    95
lemma prod_cases5 [cases type]:
wenzelm@20798
    96
  obtains (fields) a b c d e where "y = (a, b, c, d, e)"
wenzelm@20798
    97
  by (cases y, case_tac d) blast
wenzelm@11954
    98
wenzelm@11954
    99
lemma prod_induct5 [case_names fields, induct type]:
wenzelm@11954
   100
    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
wenzelm@11954
   101
  by (cases x) blast
wenzelm@11954
   102
wenzelm@20798
   103
lemma prod_cases6 [cases type]:
wenzelm@20798
   104
  obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
wenzelm@20798
   105
  by (cases y, case_tac e) blast
wenzelm@11954
   106
wenzelm@11954
   107
lemma prod_induct6 [case_names fields, induct type]:
wenzelm@11954
   108
    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
wenzelm@11954
   109
  by (cases x) blast
wenzelm@11954
   110
wenzelm@20798
   111
lemma prod_cases7 [cases type]:
wenzelm@20798
   112
  obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
wenzelm@20798
   113
  by (cases y, case_tac f) blast
wenzelm@11954
   114
wenzelm@11954
   115
lemma prod_induct7 [case_names fields, induct type]:
wenzelm@11954
   116
    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
wenzelm@11954
   117
  by (cases x) blast
berghofe@5759
   118
wenzelm@12918
   119
wenzelm@12918
   120
subsection {* The option type *}
wenzelm@12918
   121
wenzelm@12918
   122
datatype 'a option = None | Some 'a
wenzelm@12918
   123
wenzelm@20798
   124
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
nipkow@18576
   125
  by (induct x) auto
nipkow@18576
   126
wenzelm@20798
   127
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
paulson@18447
   128
  by (induct x) auto
paulson@18447
   129
nipkow@18576
   130
text{*Although it may appear that both of these equalities are helpful
nipkow@18576
   131
only when applied to assumptions, in practice it seems better to give
nipkow@18576
   132
them the uniform iff attribute. *}
wenzelm@12918
   133
wenzelm@12918
   134
lemma option_caseE:
wenzelm@20798
   135
  assumes c: "(case x of None => P | Some y => Q y)"
wenzelm@20798
   136
  obtains
wenzelm@20798
   137
    (None) "x = None" and P
wenzelm@20798
   138
  | (Some) y where "x = Some y" and "Q y"
wenzelm@20798
   139
  using c by (cases x) simp_all
wenzelm@12918
   140
wenzelm@12918
   141
wenzelm@12918
   142
subsubsection {* Operations *}
wenzelm@12918
   143
wenzelm@12918
   144
consts
wenzelm@12918
   145
  the :: "'a option => 'a"
wenzelm@12918
   146
primrec
wenzelm@12918
   147
  "the (Some x) = x"
wenzelm@12918
   148
wenzelm@12918
   149
consts
wenzelm@12918
   150
  o2s :: "'a option => 'a set"
wenzelm@12918
   151
primrec
wenzelm@12918
   152
  "o2s None = {}"
wenzelm@12918
   153
  "o2s (Some x) = {x}"
wenzelm@12918
   154
wenzelm@12918
   155
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
wenzelm@12918
   156
  by simp
wenzelm@12918
   157
wenzelm@17876
   158
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
wenzelm@12918
   159
wenzelm@12918
   160
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
wenzelm@12918
   161
  by (cases xo) auto
wenzelm@12918
   162
wenzelm@12918
   163
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
wenzelm@12918
   164
  by (cases xo) auto
wenzelm@12918
   165
wenzelm@12918
   166
wenzelm@12918
   167
constdefs
wenzelm@12918
   168
  option_map :: "('a => 'b) => ('a option => 'b option)"
wenzelm@12918
   169
  "option_map == %f y. case y of None => None | Some x => Some (f x)"
wenzelm@12918
   170
wenzelm@12918
   171
lemma option_map_None [simp]: "option_map f None = None"
wenzelm@12918
   172
  by (simp add: option_map_def)
wenzelm@12918
   173
wenzelm@12918
   174
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
wenzelm@12918
   175
  by (simp add: option_map_def)
wenzelm@12918
   176
wenzelm@20798
   177
lemma option_map_is_None [iff]:
wenzelm@20798
   178
    "(option_map f opt = None) = (opt = None)"
wenzelm@20798
   179
  by (simp add: option_map_def split add: option.split)
nipkow@14187
   180
wenzelm@12918
   181
lemma option_map_eq_Some [iff]:
wenzelm@12918
   182
    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
wenzelm@20798
   183
  by (simp add: option_map_def split add: option.split)
nipkow@14187
   184
nipkow@14187
   185
lemma option_map_comp:
wenzelm@20798
   186
    "option_map f (option_map g opt) = option_map (f o g) opt"
wenzelm@20798
   187
  by (simp add: option_map_def split add: option.split)
wenzelm@12918
   188
wenzelm@12918
   189
lemma option_map_o_sum_case [simp]:
wenzelm@12918
   190
    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
wenzelm@20798
   191
  by (rule ext) (simp split: sum.split)
wenzelm@12918
   192
haftmann@19787
   193
haftmann@19817
   194
subsubsection {* Codegenerator setup *}
haftmann@19817
   195
haftmann@19787
   196
consts
haftmann@19787
   197
  is_none :: "'a option \<Rightarrow> bool"
haftmann@19787
   198
primrec
haftmann@19787
   199
  "is_none None = True"
haftmann@19787
   200
  "is_none (Some x) = False"
haftmann@19787
   201
haftmann@20105
   202
lemma is_none_none [code inline]:
wenzelm@20798
   203
    "(x = None) = (is_none x)" 
wenzelm@20798
   204
  by (cases x) simp_all
haftmann@19787
   205
wenzelm@17458
   206
lemmas [code] = imp_conv_disj
wenzelm@17458
   207
krauss@20523
   208
lemma [code func]:
haftmann@19138
   209
  "(\<not> True) = False" by (rule HOL.simp_thms)
haftmann@19138
   210
krauss@20523
   211
lemma [code func]:
haftmann@19138
   212
  "(\<not> False) = True" by (rule HOL.simp_thms)
haftmann@19138
   213
krauss@20523
   214
lemma [code func]:
nipkow@19179
   215
  shows "(False \<and> x) = False"
wenzelm@20798
   216
    and "(True \<and> x) = x"
wenzelm@20798
   217
    and "(x \<and> False) = False"
wenzelm@20798
   218
    and "(x \<and> True) = x" by simp_all
haftmann@19138
   219
krauss@20523
   220
lemma [code func]:
nipkow@19179
   221
  shows "(False \<or> x) = x"
wenzelm@20798
   222
    and "(True \<or> x) = True"
wenzelm@20798
   223
    and "(x \<or> False) = x"
wenzelm@20798
   224
    and "(x \<or> True) = True" by simp_all
haftmann@19138
   225
haftmann@19138
   226
declare
krauss@20523
   227
  if_True [code func]
krauss@20523
   228
  if_False [code func]
nipkow@19179
   229
  fst_conv [code]
nipkow@19179
   230
  snd_conv [code]
haftmann@19138
   231
haftmann@20105
   232
lemma split_is_prod_case [code inline]:
wenzelm@20798
   233
    "split = prod_case"
wenzelm@20798
   234
  by (simp add: expand_fun_eq split_def prod.cases)
haftmann@20105
   235
haftmann@20453
   236
code_type bool
haftmann@20453
   237
  (SML target_atom "bool")
haftmann@20453
   238
  (Haskell target_atom "Bool")
haftmann@19138
   239
haftmann@20453
   240
code_const True and False and Not and "op &" and "op |" and If
haftmann@20453
   241
  (SML target_atom "true" and target_atom "false" and target_atom "not"
haftmann@20453
   242
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@20453
   243
    and target_atom "(if __/ then __/ else __)")
haftmann@20453
   244
  (Haskell target_atom "True" and target_atom "False" and target_atom "not"
haftmann@20453
   245
    and infixl 3 "&&" and infixl 2 "||"
haftmann@20453
   246
    and target_atom "(if __/ then __/ else __)")
haftmann@20453
   247
haftmann@20453
   248
code_type *
haftmann@20453
   249
  (SML infix 2 "*")
haftmann@20453
   250
  (Haskell target_atom "(__,/ __)")
haftmann@19138
   251
haftmann@20453
   252
code_const Pair
haftmann@20453
   253
  (SML target_atom "(__,/ __)")
haftmann@20453
   254
  (Haskell target_atom "(__,/ __)")
haftmann@18702
   255
haftmann@20453
   256
code_type unit
haftmann@20453
   257
  (SML target_atom "unit")
haftmann@20453
   258
  (Haskell target_atom "()")
haftmann@19150
   259
haftmann@20453
   260
code_const Unity
haftmann@20453
   261
  (SML target_atom "()")
haftmann@20453
   262
  (Haskell target_atom "()")
haftmann@19150
   263
haftmann@20453
   264
code_type option
haftmann@20453
   265
  (SML "_ option")
haftmann@20453
   266
  (Haskell "Maybe _")
haftmann@19150
   267
haftmann@20453
   268
code_const None and Some
haftmann@20453
   269
  (SML target_atom "NONE" and target_atom "SOME")
haftmann@20453
   270
  (Haskell target_atom "Nothing" and target_atom "Just")
haftmann@19150
   271
haftmann@20588
   272
code_instance option :: eq
haftmann@20588
   273
  (Haskell -)
haftmann@20588
   274
haftmann@20588
   275
code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
haftmann@20588
   276
  (Haskell infixl 4 "==")
haftmann@20588
   277
berghofe@5181
   278
end