src/HOL/Option.thy
author oheimb
Wed, 09 Sep 1998 17:23:42 +0200
changeset 5445 3905974ad555
parent 5183 89f162de39cf
child 9001 93af64f54bf2
permissions -rw-r--r--
AddIffs[not_None_eq]; made wrapper ospec really safe
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
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    13
constdefs
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    14
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    15
  the		:: "'a option => 'a"
4192
c38ab5af38b5 replaced 8bit characters
oheimb
parents: 4133
diff changeset
    16
 "the == %y. case y of None => arbitrary | Some x => x"
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    17
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 2019
diff changeset
    18
  option_map	:: "('a => 'b) => ('a option => 'b option)"
4192
c38ab5af38b5 replaced 8bit characters
oheimb
parents: 4133
diff changeset
    19
 "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
    20
4752
1c334bd00038 added o2s
oheimb
parents: 4192
diff changeset
    21
consts
1c334bd00038 added o2s
oheimb
parents: 4192
diff changeset
    22
1c334bd00038 added o2s
oheimb
parents: 4192
diff changeset
    23
  o2s	   :: "'a option => 'a set"
1c334bd00038 added o2s
oheimb
parents: 4192
diff changeset
    24
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4752
diff changeset
    25
primrec
5445
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5183
diff changeset
    26
4752
1c334bd00038 added o2s
oheimb
parents: 4192
diff changeset
    27
 "o2s  None    = {}"
1c334bd00038 added o2s
oheimb
parents: 4192
diff changeset
    28
 "o2s (Some x) = {x}"
1c334bd00038 added o2s
oheimb
parents: 4192
diff changeset
    29
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    30
end