added o2s
authoroheimb
Tue Mar 24 15:51:37 1998 +0100 (1998-03-24)
changeset 47521c334bd00038
parent 4751 6fbd9838ccae
child 4753 b3aab5c73b52
added o2s
src/HOL/Option.ML
src/HOL/Option.thy
     1.1 --- a/src/HOL/Option.ML	Tue Mar 24 15:49:32 1998 +0100
     1.2 +++ b/src/HOL/Option.ML	Tue Mar 24 15:51:37 1998 +0100
     1.3 @@ -57,3 +57,16 @@
     1.4  	"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
     1.5  	optionE_tac "x" 1,
     1.6  	 Auto_tac]);
     1.7 +
     1.8 +section "o2s";
     1.9 +
    1.10 +val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
    1.11 + (K [	optionE_tac "xo" 1,
    1.12 +	 Auto_tac]);
    1.13 +AddSDs [elem_o2s RS iffD1];
    1.14 +Addsimps [elem_o2s];
    1.15 +
    1.16 +val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
    1.17 + (K [	optionE_tac "xo" 1,
    1.18 +	 Auto_tac]);
    1.19 +Addsimps [o2s_empty_eq];
     2.1 --- a/src/HOL/Option.thy	Tue Mar 24 15:49:32 1998 +0100
     2.2 +++ b/src/HOL/Option.thy	Tue Mar 24 15:51:37 1998 +0100
     2.3 @@ -18,4 +18,13 @@
     2.4    option_map	:: "('a => 'b) => ('a option => 'b option)"
     2.5   "option_map == %f y. case y of None => None | Some x => Some (f x)"
     2.6  
     2.7 +consts
     2.8 +
     2.9 +  o2s	   :: "'a option => 'a set"
    2.10 +
    2.11 +primrec o2s option
    2.12 +
    2.13 + "o2s  None    = {}"
    2.14 + "o2s (Some x) = {x}"
    2.15 +
    2.16  end