1 (* Title: HOL/BCV/Opt.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 *) |
|
6 |
|
7 Goalw [lesub_def,le_def] |
|
8 "o1 <=_(le r) o2 = \ |
|
9 \ (case o2 of None => o1=None | \ |
|
10 \ Some y => (case o1 of None => True | Some x => x <=_r y))"; |
|
11 by (rtac refl 1); |
|
12 qed "unfold_le_opt"; |
|
13 |
|
14 Goal "order r ==> o1 <=_(le r) o1"; |
|
15 by (asm_simp_tac (simpset() addsimps [unfold_le_opt] addsplits [option.split]) 1); |
|
16 qed "le_opt_refl"; |
|
17 |
|
18 Goal "order r ==> \ |
|
19 \ o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> o1 <=_(le r) o3"; |
|
20 by (simp_tac (simpset() addsimps [unfold_le_opt] addsplits [option.split]) 1); |
|
21 by (blast_tac (claset() addIs [order_trans]) 1); |
|
22 qed_spec_mp "le_opt_trans"; |
|
23 |
|
24 Goal "order r ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> o1=o2"; |
|
25 by (simp_tac (simpset() addsimps [unfold_le_opt] addsplits [option.split]) 1); |
|
26 by (blast_tac (claset() addIs [order_antisym]) 1); |
|
27 qed_spec_mp "le_opt_antisym"; |
|
28 |
|
29 Goal "order r ==> order(le r)"; |
|
30 by (stac order_def 1); |
|
31 by (blast_tac (claset() addIs [le_opt_refl,le_opt_trans,le_opt_antisym]) 1); |
|
32 qed "order_le_opt"; |
|
33 AddSIs [order_le_opt]; |
|
34 Addsimps [order_le_opt]; |
|
35 |
|
36 Goalw [lesub_def,le_def] "None <=_(le r) ox"; |
|
37 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
38 qed "None_bot"; |
|
39 AddIffs [None_bot]; |
|
40 |
|
41 Goalw [lesub_def,le_def] |
|
42 "(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)"; |
|
43 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
44 qed "Some_le"; |
|
45 AddIffs [Some_le]; |
|
46 |
|
47 Goalw [lesub_def,le_def] "(ox <=_(le r) None) = (ox = None)"; |
|
48 by (simp_tac (simpset() addsplits [option.split]) 1); |
|
49 qed "le_None"; |
|
50 AddIffs [le_None]; |
|
51 |
|
52 |
|
53 Goalw [Opt.sl_def,semilat_def,closed_def, split_conv RS eq_reflection] |
|
54 "!!L. semilat L ==> semilat (Opt.sl L)"; |
|
55 by (split_all_tac 1); |
|
56 by (asm_full_simp_tac (simpset() addsplits [option.split] |
|
57 addsimps [lesub_def,Opt.le_def,plussub_def,Opt.sup_def,opt_def,Bex_def]) 1); |
|
58 by (asm_full_simp_tac (simpset() addsimps [order_def,lesub_def]) 1); |
|
59 qed "semilat_opt"; |
|
60 |
|
61 |
|
62 Goalw [top_def] "top (le r) (Some T) = top r T"; |
|
63 by (rtac iffI 1); |
|
64 by (Blast_tac 1); |
|
65 by (rtac allI 1); |
|
66 by (case_tac "x" 1); |
|
67 by (ALLGOALS Asm_simp_tac); |
|
68 qed "top_le_opt_Some"; |
|
69 AddIffs [top_le_opt_Some]; |
|
70 |
|
71 Goalw [top_def] "[| order r; top r T |] ==> (T <=_r x) = (x = T)"; |
|
72 by (blast_tac (claset() addIs [order_antisym]) 1); |
|
73 qed "Top_le_conv"; |
|
74 |
|
75 |
|
76 Goalw [opt_def] "None : opt A"; |
|
77 by (Simp_tac 1); |
|
78 qed "None_in_opt"; |
|
79 AddIffs [None_in_opt]; |
|
80 |
|
81 Goalw [opt_def] "(Some x : opt A) = (x:A)"; |
|
82 by (Auto_tac); |
|
83 qed "Some_in_opt"; |
|
84 AddIffs [Some_in_opt]; |
|
85 |
|
86 Goalw [acc_def,lesub_def,le_def,lesssub_def] "acc r ==> acc(le r)"; |
|
87 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal] addsplits [option.split]) 1); |
|
88 by (Clarify_tac 1); |
|
89 by (case_tac "? a. Some a : Q" 1); |
|
90 by (eres_inst_tac [("x","{a . Some a : Q}")] allE 1); |
|
91 by (Blast_tac 1); |
|
92 by (case_tac "x" 1); |
|
93 by (Blast_tac 1); |
|
94 by (Blast_tac 1); |
|
95 qed "acc_le_optI"; |
|
96 AddSIs [acc_le_optI]; |
|
97 |
|
98 |
|
99 Goalw [option_map_def] |
|
100 "[| ox : opt S; !x:S. ox = Some x --> f x : S |] \ |
|
101 \ ==> option_map f ox : opt S"; |
|
102 by (asm_simp_tac (simpset() addsplits [option.split]) 1); |
|
103 by (Blast_tac 1); |
|
104 qed "option_map_in_optionI"; |
|
105 |
|