1 (* Title: Option.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 Derived rules |
|
7 *) |
|
8 |
|
9 Goal "(x ~= None) = (? y. x = Some y)"; |
|
10 by (induct_tac "x" 1); |
|
11 by Auto_tac; |
|
12 qed "not_None_eq"; |
|
13 AddIffs[not_None_eq]; |
|
14 |
|
15 Goal "(!y. x ~= Some y) = (x = None)"; |
|
16 by (induct_tac "x" 1); |
|
17 by Auto_tac; |
|
18 qed "not_Some_eq"; |
|
19 AddIffs[not_Some_eq]; |
|
20 |
|
21 |
|
22 section "case analysis in premises"; |
|
23 |
|
24 val prems = Goal |
|
25 "[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P"; |
|
26 by (case_tac "opt = None" 1); |
|
27 by (eresolve_tac prems 1); |
|
28 by (dtac (not_None_eq RS iffD1) 1); |
|
29 by (etac exE 1); |
|
30 by (eresolve_tac prems 1); |
|
31 qed "optionE"; |
|
32 |
|
33 val prems = Goal |
|
34 "[| case x of None => P | Some y => Q y; \ |
|
35 \ [| x = None; P |] ==> R; \ |
|
36 \ !!y. [|x = Some y; Q y|] ==> R|] ==> R"; |
|
37 by (cut_facts_tac prems 1); |
|
38 by (res_inst_tac [("opt","x")] optionE 1); |
|
39 by (forward_tac prems 1); |
|
40 by (forward_tac prems 3); |
|
41 by Auto_tac; |
|
42 qed "option_caseE"; |
|
43 |
|
44 |
|
45 section "option_map"; |
|
46 |
|
47 Goalw [option_map_def] "option_map f None = None"; |
|
48 by (Simp_tac 1); |
|
49 qed "option_map_None"; |
|
50 |
|
51 Goalw [option_map_def] "option_map f (Some x) = Some (f x)"; |
|
52 by (Simp_tac 1); |
|
53 qed "option_map_Some"; |
|
54 |
|
55 Addsimps [option_map_None, option_map_Some]; |
|
56 |
|
57 Goalw [option_map_def] |
|
58 "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)"; |
|
59 by (asm_full_simp_tac (simpset() addsplits [option.split]) 1); |
|
60 qed "option_map_eq_Some"; |
|
61 AddIffs[option_map_eq_Some]; |
|
62 |
|
63 Goal |
|
64 "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"; |
|
65 by (rtac ext 1); |
|
66 by (simp_tac (simpset() addsplits [sum.split]) 1); |
|
67 qed "option_map_o_sum_case"; |
|
68 Addsimps [option_map_o_sum_case]; |
|
69 |
|
70 |
|
71 section "o2s"; |
|
72 |
|
73 Goal "[| !x:o2s A. P x; A = Some x |] ==> P x"; |
|
74 by Auto_tac; |
|
75 qed "ospec"; |
|
76 AddDs[ospec]; |
|
77 |
|
78 claset_ref() := claset() addSD2 ("ospec", ospec); |
|
79 |
|
80 |
|
81 Goal "(x : o2s xo) = (xo = Some x)"; |
|
82 by (case_tac "xo" 1); |
|
83 by Auto_tac; |
|
84 qed "elem_o2s"; |
|
85 AddIffs [elem_o2s]; |
|
86 |
|
87 Goal "(o2s xo = {}) = (xo = None)"; |
|
88 by (case_tac "xo" 1); |
|
89 by Auto_tac; |
|
90 qed "o2s_empty_eq"; |
|
91 |
|
92 Addsimps [o2s_empty_eq]; |
|
93 |
|