equal
deleted
inserted
replaced
17 case_tac "opt = None" 1, |
17 case_tac "opt = None" 1, |
18 eresolve_tac prems 1, |
18 eresolve_tac prems 1, |
19 dtac (not_None_eq RS iffD1) 1, |
19 dtac (not_None_eq RS iffD1) 1, |
20 etac exE 1, |
20 etac exE 1, |
21 eresolve_tac prems 1]); |
21 eresolve_tac prems 1]); |
22 fun optionE_tac s i = EVERY [ |
22 fun optionE_tac s = res_inst_tac [("opt",s)] optionE THEN_ALL_NEW hyp_subst_tac; |
23 res_inst_tac [("opt",s)] optionE i, |
|
24 hyp_subst_tac (i+1), |
|
25 hyp_subst_tac i]; |
|
26 |
23 |
27 qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \ |
24 qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \ |
28 \ [|x = None; P |] ==> R; \ |
25 \ [|x = None; P |] ==> R; \ |
29 \ !!y. [|x = Some y; Q y|] ==> R|] ==> R" (fn prems => [ |
26 \ !!y. [|x = Some y; Q y|] ==> R|] ==> R" (fn prems => [ |
30 cut_facts_tac prems 1, |
27 cut_facts_tac prems 1, |
58 (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]); |
55 (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]); |
59 AddIffs[option_map_eq_Some]; |
56 AddIffs[option_map_eq_Some]; |
60 |
57 |
61 section "o2s"; |
58 section "o2s"; |
62 |
59 |
|
60 qed_goal "ospec" thy |
|
61 "!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]); |
|
62 claset_ref() := claset() addSaltern ("ospec", dtac ospec THEN' atac); |
|
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, Auto_tac]); |
65 (K [optionE_tac "xo" 1, Auto_tac]); |
65 AddSDs [elem_o2s RS iffD1]; |
66 AddIffs [elem_o2s]; |
66 Addsimps [elem_o2s]; |
|
67 |
67 |
68 val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)" |
68 val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)" |
69 (K [optionE_tac "xo" 1, Auto_tac]); |
69 (K [optionE_tac "xo" 1, Auto_tac]); |
70 Addsimps [o2s_empty_eq]; |
70 Addsimps [o2s_empty_eq]; |
|
71 |