|
1 |
|
2 open Lattice; |
|
3 |
|
4 |
|
5 (** basic properties of "&&" and "||" **) |
|
6 |
|
7 (* unique existence *) |
|
8 |
|
9 goalw thy [inf_def] "is_inf x y (x && y)"; |
|
10 br (ex_inf RS spec RS spec RS selectI1) 1; |
|
11 qed "inf_is_inf"; |
|
12 |
|
13 goal thy "is_inf x y inf --> x && y = inf"; |
|
14 br impI 1; |
|
15 br (is_inf_uniq RS mp) 1; |
|
16 br conjI 1; |
|
17 br inf_is_inf 1; |
|
18 ba 1; |
|
19 qed "inf_uniq"; |
|
20 |
|
21 goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf"; |
|
22 by (safe_tac HOL_cs); |
|
23 by (step_tac HOL_cs 1); |
|
24 by (step_tac HOL_cs 1); |
|
25 br inf_is_inf 1; |
|
26 br (inf_uniq RS mp RS sym) 1; |
|
27 ba 1; |
|
28 qed "ex1_inf"; |
|
29 |
|
30 |
|
31 goalw thy [sup_def] "is_sup x y (x || y)"; |
|
32 br (ex_sup RS spec RS spec RS selectI1) 1; |
|
33 qed "sup_is_sup"; |
|
34 |
|
35 goal thy "is_sup x y sup --> x || y = sup"; |
|
36 br impI 1; |
|
37 br (is_sup_uniq RS mp) 1; |
|
38 br conjI 1; |
|
39 br sup_is_sup 1; |
|
40 ba 1; |
|
41 qed "sup_uniq"; |
|
42 |
|
43 goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup"; |
|
44 by (safe_tac HOL_cs); |
|
45 by (step_tac HOL_cs 1); |
|
46 by (step_tac HOL_cs 1); |
|
47 br sup_is_sup 1; |
|
48 br (sup_uniq RS mp RS sym) 1; |
|
49 ba 1; |
|
50 qed "ex1_sup"; |
|
51 |
|
52 |
|
53 (* "&&" yields g.l.bs, "||" yields l.u.bs. --- in pieces *) |
|
54 |
|
55 val tac = |
|
56 cut_facts_tac [inf_is_inf] 1 THEN |
|
57 rewrite_goals_tac [inf_def, is_inf_def] THEN |
|
58 fast_tac HOL_cs 1; |
|
59 |
|
60 goal thy "x && y [= x"; |
|
61 by tac; |
|
62 qed "inf_lb1"; |
|
63 |
|
64 goal thy "x && y [= y"; |
|
65 by tac; |
|
66 qed "inf_lb2"; |
|
67 |
|
68 val prems = goal thy "[| z [= x; z [= y |] ==> z [= x && y"; |
|
69 by (cut_facts_tac prems 1); |
|
70 by tac; |
|
71 qed "inf_ub_lbs"; |
|
72 |
|
73 |
|
74 val tac = |
|
75 cut_facts_tac [sup_is_sup] 1 THEN |
|
76 rewrite_goals_tac [sup_def, is_sup_def] THEN |
|
77 fast_tac HOL_cs 1; |
|
78 |
|
79 goal thy "x [= x || y"; |
|
80 by tac; |
|
81 qed "sup_ub1"; |
|
82 |
|
83 goal thy "y [= x || y"; |
|
84 by tac; |
|
85 qed "sup_ub2"; |
|
86 |
|
87 val prems = goal thy "[| x [= z; y [= z |] ==> x || y [= z"; |
|
88 by (cut_facts_tac prems 1); |
|
89 by tac; |
|
90 qed "sup_lb_ubs"; |
|
91 |
|
92 |
|
93 |
|
94 (** some equations concerning "&&" and "||" vs. "[=" **) |
|
95 |
|
96 (* the Connection Theorems: "[=" expressed via "&&" or "||" *) |
|
97 |
|
98 goal thy "(x && y = x) = (x [= y)"; |
|
99 br iffI 1; |
|
100 (*==>*) |
|
101 be subst 1; |
|
102 br inf_lb2 1; |
|
103 (*<==*) |
|
104 br (inf_uniq RS mp) 1; |
|
105 by (rewrite_goals_tac [is_inf_def]); |
|
106 by (REPEAT_FIRST (rtac conjI)); |
|
107 br le_refl 1; |
|
108 ba 1; |
|
109 by (fast_tac HOL_cs 1); |
|
110 qed "inf_connect"; |
|
111 |
|
112 goal thy "(x || y = y) = (x [= y)"; |
|
113 br iffI 1; |
|
114 (*==>*) |
|
115 be subst 1; |
|
116 br sup_ub1 1; |
|
117 (*<==*) |
|
118 br (sup_uniq RS mp) 1; |
|
119 by (rewrite_goals_tac [is_sup_def]); |
|
120 by (REPEAT_FIRST (rtac conjI)); |
|
121 ba 1; |
|
122 br le_refl 1; |
|
123 by (fast_tac HOL_cs 1); |
|
124 qed "sup_connect"; |
|
125 |
|
126 |
|
127 (* minorized infs / majorized sups *) |
|
128 |
|
129 goal thy "(x [= y && z) = (x [= y & x [= z)"; |
|
130 br iffI 1; |
|
131 (*==> (level 1)*) |
|
132 by (cut_facts_tac [inf_lb1, inf_lb2] 1); |
|
133 br conjI 1; |
|
134 br (le_trans RS mp) 1; |
|
135 be conjI 1; |
|
136 ba 1; |
|
137 br (le_trans RS mp) 1; |
|
138 be conjI 1; |
|
139 ba 1; |
|
140 (*<== (level 9)*) |
|
141 be conjE 1; |
|
142 be inf_ub_lbs 1; |
|
143 ba 1; |
|
144 qed "le_inf_eq"; |
|
145 |
|
146 goal thy "(x || y [= z) = (x [= z & y [= z)"; |
|
147 br iffI 1; |
|
148 (*==> (level 1)*) |
|
149 by (cut_facts_tac [sup_ub1, sup_ub2] 1); |
|
150 br conjI 1; |
|
151 br (le_trans RS mp) 1; |
|
152 be conjI 1; |
|
153 ba 1; |
|
154 br (le_trans RS mp) 1; |
|
155 be conjI 1; |
|
156 ba 1; |
|
157 (*<== (level 9)*) |
|
158 be conjE 1; |
|
159 be sup_lb_ubs 1; |
|
160 ba 1; |
|
161 qed "ge_sup_eq"; |
|
162 |
|
163 |
|
164 (** algebraic properties of "&&" and "||": A, C, I, AB **) |
|
165 |
|
166 (* associativity *) |
|
167 |
|
168 goal thy "(x && y) && z = x && (y && z)"; |
|
169 by (stac (inf_uniq RS mp RS sym) 1); |
|
170 back(); |
|
171 back(); |
|
172 back(); |
|
173 back(); |
|
174 back(); |
|
175 back(); |
|
176 back(); |
|
177 back(); |
|
178 br refl 2; |
|
179 br (is_inf_assoc RS mp) 1; |
|
180 by (REPEAT_FIRST (rtac conjI)); |
|
181 by (REPEAT_FIRST (rtac inf_is_inf)); |
|
182 qed "inf_assoc"; |
|
183 |
|
184 goal thy "(x || y) || z = x || (y || z)"; |
|
185 by (stac (sup_uniq RS mp RS sym) 1); |
|
186 back(); |
|
187 back(); |
|
188 back(); |
|
189 back(); |
|
190 back(); |
|
191 back(); |
|
192 back(); |
|
193 back(); |
|
194 br refl 2; |
|
195 br (is_sup_assoc RS mp) 1; |
|
196 by (REPEAT_FIRST (rtac conjI)); |
|
197 by (REPEAT_FIRST (rtac sup_is_sup)); |
|
198 qed "sup_assoc"; |
|
199 |
|
200 |
|
201 (* commutativity *) |
|
202 |
|
203 goalw thy [inf_def] "x && y = y && x"; |
|
204 by (stac (is_inf_commut RS ext) 1); |
|
205 br refl 1; |
|
206 qed "inf_commut"; |
|
207 |
|
208 goalw thy [sup_def] "x || y = y || x"; |
|
209 by (stac (is_sup_commut RS ext) 1); |
|
210 br refl 1; |
|
211 qed "sup_commut"; |
|
212 |
|
213 |
|
214 (* idempotency *) |
|
215 |
|
216 goal thy "x && x = x"; |
|
217 by (stac inf_connect 1); |
|
218 br le_refl 1; |
|
219 qed "inf_idemp"; |
|
220 |
|
221 goal thy "x || x = x"; |
|
222 by (stac sup_connect 1); |
|
223 br le_refl 1; |
|
224 qed "sup_idemp"; |
|
225 |
|
226 |
|
227 (* absorption *) |
|
228 |
|
229 goal thy "x || (x && y) = x"; |
|
230 by (stac sup_commut 1); |
|
231 by (stac sup_connect 1); |
|
232 br inf_lb1 1; |
|
233 qed "sup_inf_absorb"; |
|
234 |
|
235 goal thy "x && (x || y) = x"; |
|
236 by (stac inf_connect 1); |
|
237 br sup_ub1 1; |
|
238 qed "inf_sup_absorb"; |
|
239 |
|
240 |
|
241 (* monotonicity *) |
|
242 |
|
243 val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y"; |
|
244 by (cut_facts_tac prems 1); |
|
245 by (stac le_inf_eq 1); |
|
246 br conjI 1; |
|
247 br (le_trans RS mp) 1; |
|
248 br conjI 1; |
|
249 br inf_lb1 1; |
|
250 ba 1; |
|
251 br (le_trans RS mp) 1; |
|
252 br conjI 1; |
|
253 br inf_lb2 1; |
|
254 ba 1; |
|
255 qed "inf_mon"; |
|
256 |
|
257 val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y"; |
|
258 by (cut_facts_tac prems 1); |
|
259 by (stac ge_sup_eq 1); |
|
260 br conjI 1; |
|
261 br (le_trans RS mp) 1; |
|
262 br conjI 1; |
|
263 ba 1; |
|
264 br sup_ub1 1; |
|
265 br (le_trans RS mp) 1; |
|
266 br conjI 1; |
|
267 ba 1; |
|
268 br sup_ub2 1; |
|
269 qed "sup_mon"; |