src/HOL/Datatype.thy
author haftmann
Tue, 17 Jan 2006 16:36:57 +0100
changeset 18702 7dc7dcd63224
parent 18576 8d98b7711e47
child 18757 f0d901bc0686
permissions -rw-r--r--
substantial improvements in code generator
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Datatype.thy
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     4
*)
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
     5
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
     6
header {* Datatypes *}
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14981
diff changeset
     8
theory Datatype
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     9
imports Datatype_Universe
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14981
diff changeset
    10
begin
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    11
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    12
subsection {* Representing primitive types *}
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    13
5759
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
    14
rep_datatype bool
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    15
  distinct True_not_False False_not_True
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    16
  induction bool_induct
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    17
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    18
declare case_split [cases type: bool]
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    19
  -- "prefer plain propositional version"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    20
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    21
rep_datatype unit
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    22
  induction unit_induct
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    23
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
    24
rep_datatype prod
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    25
  inject Pair_eq
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    26
  induction prod_induct
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    27
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    28
rep_datatype sum
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    29
  distinct Inl_not_Inr Inr_not_Inl
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    30
  inject Inl_eq Inr_eq
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    31
  induction sum_induct
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    32
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    33
ML {*
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    34
  val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    35
  bind_thm ("sum_case_Inl", sum_case_Inl);
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    36
  bind_thm ("sum_case_Inr", sum_case_Inr);
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    37
*} -- {* compatibility *}
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    38
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    39
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    40
  apply (rule_tac s = s in sumE)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    41
   apply (erule ssubst)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    42
   apply (rule sum_case_Inl)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    43
  apply (erule ssubst)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    44
  apply (rule sum_case_Inr)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    45
  done
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    46
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    47
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    48
  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    49
  by (erule arg_cong)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    50
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    51
lemma sum_case_inject:
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    52
  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    53
proof -
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    54
  assume a: "sum_case f1 f2 = sum_case g1 g2"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    55
  assume r: "f1 = g1 ==> f2 = g2 ==> P"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    56
  show P
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    57
    apply (rule r)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    58
     apply (rule ext)
14208
144f45277d5a misc tidying
paulson
parents: 14187
diff changeset
    59
     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    60
    apply (rule ext)
14208
144f45277d5a misc tidying
paulson
parents: 14187
diff changeset
    61
    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    62
    done
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    63
qed
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    64
13635
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    65
constdefs
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    66
  Suml :: "('a => 'c) => 'a + 'b => 'c"
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    67
  "Suml == (%f. sum_case f arbitrary)"
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    68
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    69
  Sumr :: "('b => 'c) => 'a + 'b => 'c"
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    70
  "Sumr == sum_case arbitrary"
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    71
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    72
lemma Suml_inject: "Suml f = Suml g ==> f = g"
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    73
  by (unfold Suml_def) (erule sum_case_inject)
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    74
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    75
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    76
  by (unfold Sumr_def) (erule sum_case_inject)
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    77
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    78
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    79
subsection {* Finishing the datatype package setup *}
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    80
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    81
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
18230
4dc1f30af6a1 Datatype_Universe: hide base names only;
wenzelm
parents: 17876
diff changeset
    82
hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
4dc1f30af6a1 Datatype_Universe: hide base names only;
wenzelm
parents: 17876
diff changeset
    83
hide (open) type node item
13635
c41e88151b54 Added functions Suml and Sumr which are useful for constructing
berghofe
parents: 12918
diff changeset
    84
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    85
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
    86
subsection {* Further cases/induct rules for tuples *}
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    87
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    88
lemma prod_cases3 [case_names fields, cases type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    89
    "(!!a b c. y = (a, b, c) ==> P) ==> P"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    90
  apply (cases y)
14208
144f45277d5a misc tidying
paulson
parents: 14187
diff changeset
    91
  apply (case_tac b, blast)
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    92
  done
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    93
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    94
lemma prod_induct3 [case_names fields, induct type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    95
    "(!!a b c. P (a, b, c)) ==> P x"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    96
  by (cases x) blast
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    97
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    98
lemma prod_cases4 [case_names fields, cases type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
    99
    "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   100
  apply (cases y)
14208
144f45277d5a misc tidying
paulson
parents: 14187
diff changeset
   101
  apply (case_tac c, blast)
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   102
  done
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   103
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   104
lemma prod_induct4 [case_names fields, induct type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   105
    "(!!a b c d. P (a, b, c, d)) ==> P x"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   106
  by (cases x) blast
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
   107
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   108
lemma prod_cases5 [case_names fields, cases type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   109
    "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   110
  apply (cases y)
14208
144f45277d5a misc tidying
paulson
parents: 14187
diff changeset
   111
  apply (case_tac d, blast)
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   112
  done
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   113
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   114
lemma prod_induct5 [case_names fields, induct type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   115
    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   116
  by (cases x) blast
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   117
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   118
lemma prod_cases6 [case_names fields, cases type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   119
    "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   120
  apply (cases y)
14208
144f45277d5a misc tidying
paulson
parents: 14187
diff changeset
   121
  apply (case_tac e, blast)
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   122
  done
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   123
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   124
lemma prod_induct6 [case_names fields, induct type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   125
    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   126
  by (cases x) blast
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   127
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   128
lemma prod_cases7 [case_names fields, cases type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   129
    "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   130
  apply (cases y)
14208
144f45277d5a misc tidying
paulson
parents: 14187
diff changeset
   131
  apply (case_tac f, blast)
11954
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   132
  done
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   133
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   134
lemma prod_induct7 [case_names fields, induct type]:
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   135
    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
3d1780208bf3 made new-style theory;
wenzelm
parents: 10212
diff changeset
   136
  by (cases x) blast
5759
bf5d9e5b8cdf unit and bool are now represented as datatypes.
berghofe
parents: 5714
diff changeset
   137
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   138
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   139
subsection {* The option type *}
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   140
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   141
datatype 'a option = None | Some 'a
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   142
18576
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   143
lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)"
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   144
  by (induct x) auto
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   145
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   146
lemma not_Some_eq[iff]: "(ALL y. x ~= Some y) = (x = None)"
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 18230
diff changeset
   147
  by (induct x) auto
da548623916a removed or modified some instances of [iff]
paulson
parents: 18230
diff changeset
   148
18576
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   149
text{*Although it may appear that both of these equalities are helpful
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   150
only when applied to assumptions, in practice it seems better to give
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   151
them the uniform iff attribute. *}
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   152
18576
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   153
(*
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 18230
diff changeset
   154
lemmas not_None_eq_D = not_None_eq [THEN iffD1]
da548623916a removed or modified some instances of [iff]
paulson
parents: 18230
diff changeset
   155
declare not_None_eq_D [dest!]
da548623916a removed or modified some instances of [iff]
paulson
parents: 18230
diff changeset
   156
da548623916a removed or modified some instances of [iff]
paulson
parents: 18230
diff changeset
   157
lemmas not_Some_eq_D = not_Some_eq [THEN iffD1]
da548623916a removed or modified some instances of [iff]
paulson
parents: 18230
diff changeset
   158
declare not_Some_eq_D [dest!]
18576
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18447
diff changeset
   159
*)
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   160
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   161
lemma option_caseE:
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   162
  "(case x of None => P | Some y => Q y) ==>
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   163
    (x = None ==> P ==> R) ==>
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   164
    (!!y. x = Some y ==> Q y ==> R) ==> R"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   165
  by (cases x) simp_all
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   166
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   167
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   168
subsubsection {* Operations *}
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   169
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   170
consts
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   171
  the :: "'a option => 'a"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   172
primrec
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   173
  "the (Some x) = x"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   174
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   175
consts
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   176
  o2s :: "'a option => 'a set"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   177
primrec
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   178
  "o2s None = {}"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   179
  "o2s (Some x) = {x}"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   180
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   181
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   182
  by simp
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   183
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17458
diff changeset
   184
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   185
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   186
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   187
  by (cases xo) auto
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   188
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   189
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   190
  by (cases xo) auto
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   191
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   192
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   193
constdefs
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   194
  option_map :: "('a => 'b) => ('a option => 'b option)"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   195
  "option_map == %f y. case y of None => None | Some x => Some (f x)"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   196
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   197
lemma option_map_None [simp]: "option_map f None = None"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   198
  by (simp add: option_map_def)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   199
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   200
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   201
  by (simp add: option_map_def)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   202
14187
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   203
lemma option_map_is_None[iff]:
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   204
 "(option_map f opt = None) = (opt = None)"
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   205
by (simp add: option_map_def split add: option.split)
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   206
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   207
lemma option_map_eq_Some [iff]:
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   208
    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
14187
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   209
by (simp add: option_map_def split add: option.split)
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   210
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   211
lemma option_map_comp:
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   212
 "option_map f (option_map g opt) = option_map (f o g) opt"
26dfcd0ac436 Added new theorems
nipkow
parents: 13635
diff changeset
   213
by (simp add: option_map_def split add: option.split)
12918
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   214
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   215
lemma option_map_o_sum_case [simp]:
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   216
    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   217
  apply (rule ext)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   218
  apply (simp split add: sum.split)
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   219
  done
bca45be2d25b theory Option has been assimilated by Datatype;
wenzelm
parents: 12029
diff changeset
   220
17458
e42bfad176eb lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents: 15140
diff changeset
   221
lemmas [code] = imp_conv_disj
e42bfad176eb lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents: 15140
diff changeset
   222
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   223
subsubsection {* Codegenerator setup *}
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   224
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   225
code_syntax_const
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   226
  True
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   227
    ml (atom "true")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   228
    haskell (atom "True")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   229
  False
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   230
    ml (atom "false")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   231
    haskell (atom "False")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   232
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   233
code_syntax_const
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   234
  Pair
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   235
    ml (atom "(__,/ __)")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   236
    haskell (atom "(__,/ __)")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   237
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   238
code_syntax_const
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   239
  1 :: "nat"
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   240
    ml ("{*Suc 0*}")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   241
    haskell ("{*Suc 0*}")
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18576
diff changeset
   242
5181
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff changeset
   243
end