author | wenzelm |
Mon, 12 Jun 2006 21:19:00 +0200 | |
changeset 19861 | 620d90091788 |
parent 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
17309 | 1 |
(* |
2 |
File: Intensional.ML |
|
3 |
ID: $Id$ |
|
3807 | 4 |
Author: Stephan Merz |
6255 | 5 |
Copyright: 1998 University of Munich |
3807 | 6 |
|
7 |
Lemmas and tactics for "intensional" logics. |
|
8 |
*) |
|
9 |
||
6255 | 10 |
val intensional_rews = [unl_con,unl_lift,unl_lift2,unl_lift3,unl_Rall,unl_Rex,unl_Rex1]; |
11 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
12 |
Goalw [Valid_def,unl_lift2] "|- x=y ==> (x==y)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
13 |
by (rtac eq_reflection 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
14 |
by (rtac ext 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
15 |
by (etac spec 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
16 |
qed "inteq_reflection"; |
3807 | 17 |
|
17309 | 18 |
val [prem] = goalw (the_context ()) [Valid_def] "(!!w. w |= A) ==> |- A"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
19 |
by (REPEAT (resolve_tac [allI,prem] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
20 |
qed "intI"; |
6255 | 21 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
22 |
Goalw [Valid_def] "|- A ==> w |= A"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
23 |
by (etac spec 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
24 |
qed "intD"; |
6255 | 25 |
|
26 |
(** Lift usual HOL simplifications to "intensional" level. **) |
|
3807 | 27 |
local |
28 |
||
17309 | 29 |
fun prover s = (prove_goal (the_context ()) s |
30 |
(fn _ => [rewrite_goals_tac (Valid_def::intensional_rews), |
|
6255 | 31 |
blast_tac HOL_cs 1])) RS inteq_reflection |
3807 | 32 |
|
33 |
in |
|
34 |
||
35 |
val int_simps = map prover |
|
6255 | 36 |
[ "|- (x=x) = #True", |
37 |
"|- (~#True) = #False", "|- (~#False) = #True", "|- (~~ P) = P", |
|
17309 | 38 |
"|- ((~P) = P) = #False", "|- (P = (~P)) = #False", |
6255 | 39 |
"|- (P ~= Q) = (P = (~Q))", |
40 |
"|- (#True=P) = P", "|- (P=#True) = P", |
|
17309 | 41 |
"|- (#True --> P) = P", "|- (#False --> P) = #True", |
6255 | 42 |
"|- (P --> #True) = #True", "|- (P --> P) = #True", |
43 |
"|- (P --> #False) = (~P)", "|- (P --> ~P) = (~P)", |
|
17309 | 44 |
"|- (P & #True) = P", "|- (#True & P) = P", |
45 |
"|- (P & #False) = #False", "|- (#False & P) = #False", |
|
6255 | 46 |
"|- (P & P) = P", "|- (P & ~P) = #False", "|- (~P & P) = #False", |
17309 | 47 |
"|- (P | #True) = #True", "|- (#True | P) = #True", |
48 |
"|- (P | #False) = P", "|- (#False | P) = P", |
|
6255 | 49 |
"|- (P | P) = P", "|- (P | ~P) = #True", "|- (~P | P) = #True", |
17309 | 50 |
"|- (! x. P) = P", "|- (? x. P) = P", |
6255 | 51 |
"|- (~Q --> ~P) = (P --> Q)", |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
52 |
"|- (P|Q --> R) = ((P-->R)&(Q-->R))" ] |
3807 | 53 |
end; |
54 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
55 |
Goal "|- #True"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
56 |
by (simp_tac (simpset() addsimps [Valid_def,unl_con]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
57 |
qed "TrueW"; |
3807 | 58 |
|
6255 | 59 |
Addsimps (TrueW::intensional_rews); |
60 |
Addsimps int_simps; |
|
61 |
AddSIs [intI]; |
|
62 |
AddDs [intD]; |
|
3807 | 63 |
|
64 |
||
65 |
(* ======== Functions to "unlift" intensional implications into HOL rules ====== *) |
|
66 |
||
67 |
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. |
|
6255 | 68 |
|- F = G becomes F w = G w |
69 |
|- F --> G becomes F w --> G w |
|
3807 | 70 |
*) |
71 |
||
6255 | 72 |
fun int_unlift th = |
73 |
rewrite_rule intensional_rews ((th RS intD) handle _ => th); |
|
3807 | 74 |
|
6255 | 75 |
(* Turn |- F = G into meta-level rewrite rule F == G *) |
17309 | 76 |
fun int_rewrite th = |
6255 | 77 |
zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection)); |
3807 | 78 |
|
6255 | 79 |
(* flattening turns "-->" into "==>" and eliminates conjunctions in the |
80 |
antecedent. For example, |
|
81 |
||
82 |
P & Q --> (R | S --> T) becomes [| P; Q; R | S |] ==> T |
|
3807 | 83 |
|
6255 | 84 |
Flattening can be useful with "intensional" lemmas (after unlifting). |
85 |
Naive resolution with mp and conjI may run away because of higher-order |
|
86 |
unification, therefore the code is a little awkward. |
|
87 |
*) |
|
88 |
fun flatten t = |
|
17309 | 89 |
let |
6255 | 90 |
(* analogous to RS, but using matching instead of resolution *) |
91 |
fun matchres tha i thb = |
|
19861 | 92 |
case Seq.chop 2 (biresolution true [(false,tha)] i thb) of |
17309 | 93 |
([th],_) => th |
94 |
| ([],_) => raise THM("matchres: no match", i, [tha,thb]) |
|
95 |
| _ => raise THM("matchres: multiple unifiers", i, [tha,thb]) |
|
3807 | 96 |
|
6255 | 97 |
(* match tha with some premise of thb *) |
98 |
fun matchsome tha thb = |
|
99 |
let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb]) |
|
17309 | 100 |
| hmatch n = (matchres tha n thb) handle _ => hmatch (n-1) |
6255 | 101 |
in hmatch (nprems_of thb) end |
3807 | 102 |
|
6255 | 103 |
fun hflatten t = |
104 |
case (concl_of t) of |
|
105 |
Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp) |
|
106 |
| _ => (hflatten (matchsome conjI t)) handle _ => zero_var_indexes t |
|
107 |
in |
|
108 |
hflatten t |
|
109 |
end; |
|
3807 | 110 |
|
6255 | 111 |
fun int_use th = |
112 |
case (concl_of th) of |
|
113 |
Const _ $ (Const ("Intensional.Valid", _) $ _) => |
|
114 |
((flatten (int_unlift th)) handle _ => th) |
|
115 |
| _ => th; |
|
3807 | 116 |
|
117 |
(* ========================================================================= *) |
|
118 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
119 |
Goalw [Valid_def] "|- (~(! x. F x)) = (? x. ~F x)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
120 |
by (Simp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
121 |
qed "Not_Rall"; |
3807 | 122 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
123 |
Goalw [Valid_def] "|- (~ (? x. F x)) = (! x. ~ F x)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
124 |
by (Simp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
125 |
qed "Not_Rex"; |