--- a/src/HOL/Option.ML Tue Mar 24 15:49:32 1998 +0100
+++ b/src/HOL/Option.ML Tue Mar 24 15:51:37 1998 +0100
@@ -57,3 +57,16 @@
"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
optionE_tac "x" 1,
Auto_tac]);
+
+section "o2s";
+
+val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
+ (K [ optionE_tac "xo" 1,
+ Auto_tac]);
+AddSDs [elem_o2s RS iffD1];
+Addsimps [elem_o2s];
+
+val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
+ (K [ optionE_tac "xo" 1,
+ Auto_tac]);
+Addsimps [o2s_empty_eq];
--- a/src/HOL/Option.thy Tue Mar 24 15:49:32 1998 +0100
+++ b/src/HOL/Option.thy Tue Mar 24 15:51:37 1998 +0100
@@ -18,4 +18,13 @@
option_map :: "('a => 'b) => ('a option => 'b option)"
"option_map == %f y. case y of None => None | Some x => Some (f x)"
+consts
+
+ o2s :: "'a option => 'a set"
+
+primrec o2s option
+
+ "o2s None = {}"
+ "o2s (Some x) = {x}"
+
end