src/HOL/Option.ML
changeset 5183 89f162de39cf
parent 4836 fc5773ae2790
child 5293 4ce5539aa969
equal deleted inserted replaced
5182:69917bbbce45 5183:89f162de39cf
     6 Derived rules
     6 Derived rules
     7 *)
     7 *)
     8 open Option;
     8 open Option;
     9 
     9 
    10 qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
    10 qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
    11 	(K [option.induct_tac "x" 1, Auto_tac]);
    11 	(K [induct_tac "x" 1, Auto_tac]);
    12 
    12 
    13 section "case analysis in premises";
    13 section "case analysis in premises";
    14 
    14 
    15 val optionE = prove_goal thy 
    15 val optionE = prove_goal thy 
    16 	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" (fn prems => [
    16 	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" (fn prems => [
    53 	"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);
    53 	"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);
    54 Addsimps [option_map_None, option_map_Some];
    54 Addsimps [option_map_None, option_map_Some];
    55 
    55 
    56 val option_map_eq_Some = prove_goalw thy [option_map_def]
    56 val option_map_eq_Some = prove_goalw thy [option_map_def]
    57 	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
    57 	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
    58  (K [asm_full_simp_tac (simpset() addsplits [split_option_case]) 1]);
    58  (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
    59 AddIffs[option_map_eq_Some];
    59 AddIffs[option_map_eq_Some];
    60 
    60 
    61 section "o2s";
    61 section "o2s";
    62 
    62 
    63 val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
    63 val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"