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]; |