src/HOL/Datatype.thy
author wenzelm
Thu Feb 21 20:08:09 2002 +0100 (2002-02-21)
changeset 12918 bca45be2d25b
parent 12029 7df1d840d01d
child 13635 c41e88151b54
permissions -rw-r--r--
theory Option has been assimilated by Datatype;
berghofe@5181
     1
(*  Title:      HOL/Datatype.thy
berghofe@5181
     2
    ID:         $Id$
wenzelm@11954
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
wenzelm@11954
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@5181
     5
*)
berghofe@5181
     6
wenzelm@12918
     7
header {* Datatypes *}
wenzelm@11954
     8
wenzelm@11954
     9
theory Datatype = Datatype_Universe:
wenzelm@11954
    10
wenzelm@12918
    11
subsection {* Finishing the datatype package setup *}
wenzelm@12918
    12
wenzelm@12029
    13
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
wenzelm@11954
    14
hide const Node Atom Leaf Numb Lim Funs Split Case
wenzelm@11954
    15
hide type node item
wenzelm@11954
    16
wenzelm@11954
    17
wenzelm@11954
    18
subsection {* Representing primitive types *}
berghofe@5181
    19
berghofe@5759
    20
rep_datatype bool
wenzelm@11954
    21
  distinct True_not_False False_not_True
wenzelm@11954
    22
  induction bool_induct
wenzelm@11954
    23
wenzelm@11954
    24
declare case_split [cases type: bool]
wenzelm@11954
    25
  -- "prefer plain propositional version"
wenzelm@11954
    26
wenzelm@11954
    27
rep_datatype unit
wenzelm@11954
    28
  induction unit_induct
berghofe@5181
    29
berghofe@5181
    30
rep_datatype prod
wenzelm@11954
    31
  inject Pair_eq
wenzelm@11954
    32
  induction prod_induct
wenzelm@11954
    33
wenzelm@12918
    34
rep_datatype sum
wenzelm@12918
    35
  distinct Inl_not_Inr Inr_not_Inl
wenzelm@12918
    36
  inject Inl_eq Inr_eq
wenzelm@12918
    37
  induction sum_induct
wenzelm@12918
    38
wenzelm@12918
    39
ML {*
wenzelm@12918
    40
  val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
wenzelm@12918
    41
  bind_thm ("sum_case_Inl", sum_case_Inl);
wenzelm@12918
    42
  bind_thm ("sum_case_Inr", sum_case_Inr);
wenzelm@12918
    43
*} -- {* compatibility *}
wenzelm@12918
    44
wenzelm@12918
    45
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
wenzelm@12918
    46
  apply (rule_tac s = s in sumE)
wenzelm@12918
    47
   apply (erule ssubst)
wenzelm@12918
    48
   apply (rule sum_case_Inl)
wenzelm@12918
    49
  apply (erule ssubst)
wenzelm@12918
    50
  apply (rule sum_case_Inr)
wenzelm@12918
    51
  done
wenzelm@12918
    52
wenzelm@12918
    53
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
wenzelm@12918
    54
  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
wenzelm@12918
    55
  by (erule arg_cong)
wenzelm@12918
    56
wenzelm@12918
    57
lemma sum_case_inject:
wenzelm@12918
    58
  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
wenzelm@12918
    59
proof -
wenzelm@12918
    60
  assume a: "sum_case f1 f2 = sum_case g1 g2"
wenzelm@12918
    61
  assume r: "f1 = g1 ==> f2 = g2 ==> P"
wenzelm@12918
    62
  show P
wenzelm@12918
    63
    apply (rule r)
wenzelm@12918
    64
     apply (rule ext)
wenzelm@12918
    65
     apply (cut_tac x = "Inl x" in a [THEN fun_cong])
wenzelm@12918
    66
     apply simp
wenzelm@12918
    67
    apply (rule ext)
wenzelm@12918
    68
    apply (cut_tac x = "Inr x" in a [THEN fun_cong])
wenzelm@12918
    69
    apply simp
wenzelm@12918
    70
    done
wenzelm@12918
    71
qed
wenzelm@12918
    72
wenzelm@12918
    73
wenzelm@12918
    74
subsection {* Further cases/induct rules for tuples *}
wenzelm@11954
    75
wenzelm@11954
    76
lemma prod_cases3 [case_names fields, cases type]:
wenzelm@11954
    77
    "(!!a b c. y = (a, b, c) ==> P) ==> P"
wenzelm@11954
    78
  apply (cases y)
wenzelm@11954
    79
  apply (case_tac b)
wenzelm@11954
    80
  apply blast
wenzelm@11954
    81
  done
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@11954
    87
lemma prod_cases4 [case_names fields, cases type]:
wenzelm@11954
    88
    "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
wenzelm@11954
    89
  apply (cases y)
wenzelm@11954
    90
  apply (case_tac c)
wenzelm@11954
    91
  apply blast
wenzelm@11954
    92
  done
wenzelm@11954
    93
wenzelm@11954
    94
lemma prod_induct4 [case_names fields, induct type]:
wenzelm@11954
    95
    "(!!a b c d. P (a, b, c, d)) ==> P x"
wenzelm@11954
    96
  by (cases x) blast
berghofe@5181
    97
wenzelm@11954
    98
lemma prod_cases5 [case_names fields, cases type]:
wenzelm@11954
    99
    "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
wenzelm@11954
   100
  apply (cases y)
wenzelm@11954
   101
  apply (case_tac d)
wenzelm@11954
   102
  apply blast
wenzelm@11954
   103
  done
wenzelm@11954
   104
wenzelm@11954
   105
lemma prod_induct5 [case_names fields, induct type]:
wenzelm@11954
   106
    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
wenzelm@11954
   107
  by (cases x) blast
wenzelm@11954
   108
wenzelm@11954
   109
lemma prod_cases6 [case_names fields, cases type]:
wenzelm@11954
   110
    "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
wenzelm@11954
   111
  apply (cases y)
wenzelm@11954
   112
  apply (case_tac e)
wenzelm@11954
   113
  apply blast
wenzelm@11954
   114
  done
wenzelm@11954
   115
wenzelm@11954
   116
lemma prod_induct6 [case_names fields, induct type]:
wenzelm@11954
   117
    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
wenzelm@11954
   118
  by (cases x) blast
wenzelm@11954
   119
wenzelm@11954
   120
lemma prod_cases7 [case_names fields, cases type]:
wenzelm@11954
   121
    "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
wenzelm@11954
   122
  apply (cases y)
wenzelm@11954
   123
  apply (case_tac f)
wenzelm@11954
   124
  apply blast
wenzelm@11954
   125
  done
wenzelm@11954
   126
wenzelm@11954
   127
lemma prod_induct7 [case_names fields, induct type]:
wenzelm@11954
   128
    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
wenzelm@11954
   129
  by (cases x) blast
berghofe@5759
   130
wenzelm@12918
   131
wenzelm@12918
   132
subsection {* The option type *}
wenzelm@12918
   133
wenzelm@12918
   134
datatype 'a option = None | Some 'a
wenzelm@12918
   135
wenzelm@12918
   136
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
wenzelm@12918
   137
  by (induct x) auto
wenzelm@12918
   138
wenzelm@12918
   139
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
wenzelm@12918
   140
  by (induct x) auto
wenzelm@12918
   141
wenzelm@12918
   142
lemma option_caseE:
wenzelm@12918
   143
  "(case x of None => P | Some y => Q y) ==>
wenzelm@12918
   144
    (x = None ==> P ==> R) ==>
wenzelm@12918
   145
    (!!y. x = Some y ==> Q y ==> R) ==> R"
wenzelm@12918
   146
  by (cases x) simp_all
wenzelm@12918
   147
wenzelm@12918
   148
wenzelm@12918
   149
subsubsection {* Operations *}
wenzelm@12918
   150
wenzelm@12918
   151
consts
wenzelm@12918
   152
  the :: "'a option => 'a"
wenzelm@12918
   153
primrec
wenzelm@12918
   154
  "the (Some x) = x"
wenzelm@12918
   155
wenzelm@12918
   156
consts
wenzelm@12918
   157
  o2s :: "'a option => 'a set"
wenzelm@12918
   158
primrec
wenzelm@12918
   159
  "o2s None = {}"
wenzelm@12918
   160
  "o2s (Some x) = {x}"
wenzelm@12918
   161
wenzelm@12918
   162
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
wenzelm@12918
   163
  by simp
wenzelm@12918
   164
wenzelm@12918
   165
ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
wenzelm@12918
   166
wenzelm@12918
   167
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
wenzelm@12918
   168
  by (cases xo) auto
wenzelm@12918
   169
wenzelm@12918
   170
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
wenzelm@12918
   171
  by (cases xo) auto
wenzelm@12918
   172
wenzelm@12918
   173
wenzelm@12918
   174
constdefs
wenzelm@12918
   175
  option_map :: "('a => 'b) => ('a option => 'b option)"
wenzelm@12918
   176
  "option_map == %f y. case y of None => None | Some x => Some (f x)"
wenzelm@12918
   177
wenzelm@12918
   178
lemma option_map_None [simp]: "option_map f None = None"
wenzelm@12918
   179
  by (simp add: option_map_def)
wenzelm@12918
   180
wenzelm@12918
   181
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
wenzelm@12918
   182
  by (simp add: option_map_def)
wenzelm@12918
   183
wenzelm@12918
   184
lemma option_map_eq_Some [iff]:
wenzelm@12918
   185
    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
wenzelm@12918
   186
  by (simp add: option_map_def split add: option.split)
wenzelm@12918
   187
wenzelm@12918
   188
lemma option_map_o_sum_case [simp]:
wenzelm@12918
   189
    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
wenzelm@12918
   190
  apply (rule ext)
wenzelm@12918
   191
  apply (simp split add: sum.split)
wenzelm@12918
   192
  done
wenzelm@12918
   193
berghofe@5181
   194
end