2019

1 
(* Title: Option.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1996 TU Muenchen


5 


6 
Derived rules


7 
*)

4133

8 
open Option;


9 


10 
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"


11 
(K [option.induct_tac "x" 1, Auto_tac()]);


12 


13 
section "case analysis in premises";


14 


15 
val optionE = prove_goal thy


16 
"[ opt = None ==> P; !!x. opt = Some x ==> P ] ==> P" (fn prems => [


17 
case_tac "opt = None" 1,


18 
eresolve_tac prems 1,


19 
dtac (not_None_eq RS iffD1) 1,


20 
etac exE 1,


21 
eresolve_tac prems 1]);


22 
fun optionE_tac s i = EVERY [


23 
res_inst_tac [("opt",s)] optionE i,


24 
hyp_subst_tac (i+1),


25 
hyp_subst_tac i];


26 


27 
qed_goal "option_caseE" thy "[case x of None => P  Some y => Q y; \


28 
\ [x = None; P ] ==> R; \


29 
\ !!y. [x = Some y; Q y] ==> R] ==> R" (fn prems => [


30 
cut_facts_tac prems 1,


31 
res_inst_tac [("opt","x")] optionE 1,


32 
forward_tac prems 1,


33 
forward_tac prems 3,


34 
Auto_tac()]);


35 
fun option_case_tac i = EVERY [


36 
etac option_caseE i,


37 
hyp_subst_tac (i+1),


38 
hyp_subst_tac i];


39 


40 


41 
section "the";


42 


43 
qed_goalw "the_Some" thy [the_def]


44 
"the (Some x) = x" (K [Simp_tac 1]);


45 
Addsimps [the_Some];


46 


47 


48 
section "option_map";


49 


50 
qed_goalw "option_map_None" thy [option_map_def]


51 
"option_map f None = None" (K [Simp_tac 1]);


52 
qed_goalw "option_map_Some" thy [option_map_def]


53 
"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);


54 
Addsimps [option_map_None, option_map_Some];


55 


56 
val option_map_SomeD = prove_goalw thy [option_map_def]


57 
"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [


58 
optionE_tac "x" 1,


59 
Auto_tac()]);
