src/HOL/Option.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9001 93af64f54bf2
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     1
(*  Title:      Option.thy
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     2
    ID:         $Id$
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     4
    Copyright   1994  TU Muenchen
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     5
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     6
Datatype 'a option
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     7
*)
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     8
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4752
diff changeset
     9
Option = Datatype +
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    10
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    11
datatype 'a option = None | Some 'a
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    12
9001
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    13
consts
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    14
  the :: "'a option => 'a"
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    15
  o2s :: "'a option => 'a set"
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    16
9001
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    17
primrec
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    18
 "the (Some x) = x"
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    19
9001
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    20
primrec
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    21
 "o2s  None    = {}"
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    22
 "o2s (Some x) = {x}"
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    23
93af64f54bf2 the is now defined using primrec, avoiding explicit use of arbitrary.
berghofe
parents: 5445
diff changeset
    24
constdefs
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    25
  option_map	:: "('a => 'b) => ('a option => 'b option)"
4192
c38ab5af38b5 replaced 8bit characters
oheimb
parents: 4133
diff changeset
    26
 "option_map == %f y. case y of None => None | Some x => Some (f x)"
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    27
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    28
end