# HG changeset patch
# User oheimb
# Date 890751097 -3600
# Node ID 1c334bd00038cb4c10b84b7b23af35c1caf430fa
# Parent  6fbd9838ccae9b3e43356910ce1162f216b7387d
added o2s

diff -r 6fbd9838ccae -r 1c334bd00038 src/HOL/Option.ML
--- 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];
diff -r 6fbd9838ccae -r 1c334bd00038 src/HOL/Option.thy
--- 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