author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9001  93af64f54bf2 
permissions  rwrr 
2019  1 
(* Title: Option.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1994 TU Muenchen 

5 

6 
Datatype 'a option 

7 
*) 

8 

5183  9 
Option = Datatype + 
4133  10 

2019  11 
datatype 'a option = None  Some 'a 
4133  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  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  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  25 
option_map :: "('a => 'b) => ('a option => 'b option)" 
4192  26 
"option_map == %f y. case y of None => None  Some x => Some (f x)" 
4133  27 

2019  28 
end 