src/HOL/Option.ML
changeset 4133 0a08c2b9b1ed
parent 4071 4747aefbbc52
child 4477 b3e5857d8d99
equal deleted inserted replaced
4132:daff3c9987cc 4133:0a08c2b9b1ed
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     4     Copyright   1996  TU Muenchen
     5 
     5 
     6 Derived rules
     6 Derived rules
     7 *)
     7 *)
       
     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()]);