src/HOL/Option.ML
changeset 4800 97c3a45d092b
parent 4752 1c334bd00038
child 4836 fc5773ae2790
equal deleted inserted replaced
4799:82b0ed20c2cb 4800:97c3a45d092b
    51 	"option_map f None = None" (K [Simp_tac 1]);
    51 	"option_map f None = None" (K [Simp_tac 1]);
    52 qed_goalw "option_map_Some" thy [option_map_def] 
    52 qed_goalw "option_map_Some" thy [option_map_def] 
    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_SomeD = prove_goalw thy [option_map_def]
    56 val option_map_eq_Some = prove_goalw thy [option_map_def]
    57 	"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
    57 	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
    58 	optionE_tac "x" 1,
    58  (K [asm_full_simp_tac (simpset() addsplits [split_option_case]) 1]);
    59 	 Auto_tac]);
    59 AddSDs[option_map_eq_Some RS iffD1];
       
    60 Addsimps [option_map_eq_Some];
    60 
    61 
    61 section "o2s";
    62 section "o2s";
    62 
    63 
    63 val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
    64 val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
    64  (K [	optionE_tac "xo" 1,
    65  (K [optionE_tac "xo" 1, Auto_tac]);
    65 	 Auto_tac]);
       
    66 AddSDs [elem_o2s RS iffD1];
    66 AddSDs [elem_o2s RS iffD1];
    67 Addsimps [elem_o2s];
    67 Addsimps [elem_o2s];
    68 
    68 
    69 val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
    69 val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
    70  (K [	optionE_tac "xo" 1,
    70  (K [optionE_tac "xo" 1, Auto_tac]);
    71 	 Auto_tac]);
       
    72 Addsimps [o2s_empty_eq];
    71 Addsimps [o2s_empty_eq];