186 |
183 |
187 unl_Rall: "w |= ALL x. A x == ALL x. (w |= A x)" |
184 unl_Rall: "w |= ALL x. A x == ALL x. (w |= A x)" |
188 unl_Rex: "w |= EX x. A x == EX x. (w |= A x)" |
185 unl_Rex: "w |= EX x. A x == EX x. (w |= A x)" |
189 unl_Rex1: "w |= EX! x. A x == EX! x. (w |= A x)" |
186 unl_Rex1: "w |= EX! x. A x == EX! x. (w |= A x)" |
190 |
187 |
191 ML {* use_legacy_bindings (the_context ()) *} |
188 |
|
189 subsection {* Lemmas and tactics for "intensional" logics. *} |
|
190 |
|
191 lemmas intensional_rews [simp] = |
|
192 unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1 |
|
193 |
|
194 lemma inteq_reflection: "|- x=y ==> (x==y)" |
|
195 apply (unfold Valid_def unl_lift2) |
|
196 apply (rule eq_reflection) |
|
197 apply (rule ext) |
|
198 apply (erule spec) |
|
199 done |
|
200 |
|
201 lemma intI [intro!]: "(!!w. w |= A) ==> |- A" |
|
202 apply (unfold Valid_def) |
|
203 apply (rule allI) |
|
204 apply (erule meta_spec) |
|
205 done |
|
206 |
|
207 lemma intD [dest]: "|- A ==> w |= A" |
|
208 apply (unfold Valid_def) |
|
209 apply (erule spec) |
|
210 done |
|
211 |
|
212 (** Lift usual HOL simplifications to "intensional" level. **) |
|
213 |
|
214 lemma int_simps: |
|
215 "|- (x=x) = #True" |
|
216 "|- (~#True) = #False" "|- (~#False) = #True" "|- (~~ P) = P" |
|
217 "|- ((~P) = P) = #False" "|- (P = (~P)) = #False" |
|
218 "|- (P ~= Q) = (P = (~Q))" |
|
219 "|- (#True=P) = P" "|- (P=#True) = P" |
|
220 "|- (#True --> P) = P" "|- (#False --> P) = #True" |
|
221 "|- (P --> #True) = #True" "|- (P --> P) = #True" |
|
222 "|- (P --> #False) = (~P)" "|- (P --> ~P) = (~P)" |
|
223 "|- (P & #True) = P" "|- (#True & P) = P" |
|
224 "|- (P & #False) = #False" "|- (#False & P) = #False" |
|
225 "|- (P & P) = P" "|- (P & ~P) = #False" "|- (~P & P) = #False" |
|
226 "|- (P | #True) = #True" "|- (#True | P) = #True" |
|
227 "|- (P | #False) = P" "|- (#False | P) = P" |
|
228 "|- (P | P) = P" "|- (P | ~P) = #True" "|- (~P | P) = #True" |
|
229 "|- (! x. P) = P" "|- (? x. P) = P" |
|
230 "|- (~Q --> ~P) = (P --> Q)" |
|
231 "|- (P|Q --> R) = ((P-->R)&(Q-->R))" |
|
232 apply (unfold Valid_def intensional_rews) |
|
233 apply blast+ |
|
234 done |
|
235 |
|
236 declare int_simps [THEN inteq_reflection, simp] |
|
237 |
|
238 lemma TrueW [simp]: "|- #True" |
|
239 by (simp add: Valid_def unl_con) |
|
240 |
|
241 |
|
242 |
|
243 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *) |
|
244 |
|
245 ML {* |
|
246 |
|
247 local |
|
248 val intD = thm "intD"; |
|
249 val inteq_reflection = thm "inteq_reflection"; |
|
250 val intensional_rews = thms "intensional_rews"; |
|
251 in |
|
252 |
|
253 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. |
|
254 |- F = G becomes F w = G w |
|
255 |- F --> G becomes F w --> G w |
|
256 *) |
|
257 |
|
258 fun int_unlift th = |
|
259 rewrite_rule intensional_rews (th RS intD handle THM _ => th); |
|
260 |
|
261 (* Turn |- F = G into meta-level rewrite rule F == G *) |
|
262 fun int_rewrite th = |
|
263 zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection)) |
|
264 |
|
265 (* flattening turns "-->" into "==>" and eliminates conjunctions in the |
|
266 antecedent. For example, |
|
267 |
|
268 P & Q --> (R | S --> T) becomes [| P; Q; R | S |] ==> T |
|
269 |
|
270 Flattening can be useful with "intensional" lemmas (after unlifting). |
|
271 Naive resolution with mp and conjI may run away because of higher-order |
|
272 unification, therefore the code is a little awkward. |
|
273 *) |
|
274 fun flatten t = |
|
275 let |
|
276 (* analogous to RS, but using matching instead of resolution *) |
|
277 fun matchres tha i thb = |
|
278 case Seq.chop 2 (biresolution true [(false,tha)] i thb) of |
|
279 ([th],_) => th |
|
280 | ([],_) => raise THM("matchres: no match", i, [tha,thb]) |
|
281 | _ => raise THM("matchres: multiple unifiers", i, [tha,thb]) |
|
282 |
|
283 (* match tha with some premise of thb *) |
|
284 fun matchsome tha thb = |
|
285 let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb]) |
|
286 | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1) |
|
287 in hmatch (nprems_of thb) end |
|
288 |
|
289 fun hflatten t = |
|
290 case (concl_of t) of |
|
291 Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp) |
|
292 | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t |
|
293 in |
|
294 hflatten t |
|
295 end |
|
296 |
|
297 fun int_use th = |
|
298 case (concl_of th) of |
|
299 Const _ $ (Const ("Intensional.Valid", _) $ _) => |
|
300 (flatten (int_unlift th) handle THM _ => th) |
|
301 | _ => th |
192 |
302 |
193 end |
303 end |
|
304 *} |
|
305 |
|
306 setup {* |
|
307 Attrib.add_attributes [ |
|
308 ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""), |
|
309 ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""), |
|
310 ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""), |
|
311 ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")] |
|
312 *} |
|
313 |
|
314 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)" |
|
315 by (simp add: Valid_def) |
|
316 |
|
317 lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)" |
|
318 by (simp add: Valid_def) |
|
319 |
|
320 end |