AddIffs[not_None_eq];
authoroheimb
Wed Sep 09 17:23:42 1998 +0200 (1998-09-09)
changeset 54453905974ad555
parent 5444 ffc64812a70b
child 5446 506259e4e546
AddIffs[not_None_eq];
made wrapper ospec really safe
src/HOL/Option.ML
src/HOL/Option.thy
     1.1 --- a/src/HOL/Option.ML	Wed Sep 09 17:21:33 1998 +0200
     1.2 +++ b/src/HOL/Option.ML	Wed Sep 09 17:23:42 1998 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
     1.6  	(K [induct_tac "x" 1, Auto_tac]);
     1.7 +AddIffs[not_None_eq];
     1.8 +
     1.9  
    1.10  section "case analysis in premises";
    1.11  
    1.12 @@ -42,6 +44,7 @@
    1.13  Addsimps [the_Some];
    1.14  
    1.15  
    1.16 +
    1.17  section "option_map";
    1.18  
    1.19  qed_goalw "option_map_None" thy [option_map_def] 
    1.20 @@ -55,11 +58,14 @@
    1.21   (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
    1.22  AddIffs[option_map_eq_Some];
    1.23  
    1.24 +
    1.25  section "o2s";
    1.26  
    1.27  qed_goal "ospec" thy 
    1.28  	"!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]);
    1.29 -claset_ref() := claset() addSaltern ("ospec", dtac ospec THEN' atac);
    1.30 +claset_ref() := claset() addSaltern ("ospec", 
    1.31 +				dmatch_tac [ospec] THEN' eq_assume_tac);
    1.32 +
    1.33  
    1.34  val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
    1.35   (K [optionE_tac "xo" 1, Auto_tac]);
     2.1 --- a/src/HOL/Option.thy	Wed Sep 09 17:21:33 1998 +0200
     2.2 +++ b/src/HOL/Option.thy	Wed Sep 09 17:23:42 1998 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4    o2s	   :: "'a option => 'a set"
     2.5  
     2.6  primrec
     2.7 +
     2.8   "o2s  None    = {}"
     2.9   "o2s (Some x) = {x}"
    2.10