src/HOL/Option.ML
changeset 4836 fc5773ae2790
parent 4800 97c3a45d092b
child 5183 89f162de39cf
equal deleted inserted replaced
4835:f90a427d903f 4836:fc5773ae2790
    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 [split_option_case]) 1]);
    59 AddSDs[option_map_eq_Some RS iffD1];
    59 AddIffs[option_map_eq_Some];
    60 Addsimps [option_map_eq_Some];
       
    61 
    60 
    62 section "o2s";
    61 section "o2s";
    63 
    62 
    64 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)"
    65  (K [optionE_tac "xo" 1, Auto_tac]);
    64  (K [optionE_tac "xo" 1, Auto_tac]);