1 (* |
1 (* |
2 File: Intensional.ML |
2 File: Intensional.ML |
3 Author: Stephan Merz |
3 Author: Stephan Merz |
4 Copyright: 1997 University of Munich |
4 Copyright: 1998 University of Munich |
5 |
5 |
6 Lemmas and tactics for "intensional" logics. |
6 Lemmas and tactics for "intensional" logics. |
7 *) |
7 *) |
8 |
8 |
9 val intensional_rews = [unl_con,unl_lift,unl_lift2,unl_lift3,unl_Rall,unl_Rex]; |
9 val intensional_rews = [unl_con,unl_lift,unl_lift2,unl_lift3,unl_Rall,unl_Rex,unl_Rex1]; |
10 |
10 |
11 (** Lift usual HOL simplifications to "intensional" level. |
11 qed_goalw "inteq_reflection" Intensional.thy [Valid_def,unl_lift2] |
12 Convert s .= t into rewrites s == t, so we can use the standard |
12 "|- x=y ==> (x==y)" |
13 simplifier. |
13 (fn [prem] => [rtac eq_reflection 1, rtac ext 1, rtac (prem RS spec) 1 ]); |
14 **) |
14 |
|
15 qed_goalw "intI" Intensional.thy [Valid_def] "(!!w. w |= A) ==> |- A" |
|
16 (fn [prem] => [REPEAT (resolve_tac [allI,prem] 1)]); |
|
17 |
|
18 qed_goalw "intD" Intensional.thy [Valid_def] "|- A ==> w |= A" |
|
19 (fn [prem] => [rtac (prem RS spec) 1]); |
|
20 |
|
21 |
|
22 (** Lift usual HOL simplifications to "intensional" level. **) |
15 local |
23 local |
16 |
24 |
17 fun prover s = (prove_goal Intensional.thy s |
25 fun prover s = (prove_goal Intensional.thy s |
18 (fn _ => [rewrite_goals_tac (int_valid::intensional_rews), |
26 (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews), |
19 blast_tac HOL_cs 1])) RS inteq_reflection; |
27 blast_tac HOL_cs 1])) RS inteq_reflection |
20 |
28 |
21 in |
29 in |
22 |
30 |
23 val int_simps = map prover |
31 val int_simps = map prover |
24 [ "(x.=x) .= #True", |
32 [ "|- (x=x) = #True", |
25 "(.~#True) .= #False", "(.~#False) .= #True", "(.~ .~ P) .= P", |
33 "|- (~#True) = #False", "|- (~#False) = #True", "|- (~~ P) = P", |
26 "((.~P) .= P) .= #False", "(P .= (.~P)) .= #False", |
34 "|- ((~P) = P) = #False", "|- (P = (~P)) = #False", |
27 "(P .~= Q) .= (P .= (.~Q))", |
35 "|- (P ~= Q) = (P = (~Q))", |
28 "(#True.=P) .= P", "(P.=#True) .= P", |
36 "|- (#True=P) = P", "|- (P=#True) = P", |
29 "(#True .-> P) .= P", "(#False .-> P) .= #True", |
37 "|- (#True --> P) = P", "|- (#False --> P) = #True", |
30 "(P .-> #True) .= #True", "(P .-> P) .= #True", |
38 "|- (P --> #True) = #True", "|- (P --> P) = #True", |
31 "(P .-> #False) .= (.~P)", "(P .-> .~P) .= (.~P)", |
39 "|- (P --> #False) = (~P)", "|- (P --> ~P) = (~P)", |
32 "(P .& #True) .= P", "(#True .& P) .= P", |
40 "|- (P & #True) = P", "|- (#True & P) = P", |
33 "(P .& #False) .= #False", "(#False .& P) .= #False", |
41 "|- (P & #False) = #False", "|- (#False & P) = #False", |
34 "(P .& P) .= P", "(P .& .~P) .= #False", "(.~P .& P) .= #False", |
42 "|- (P & P) = P", "|- (P & ~P) = #False", "|- (~P & P) = #False", |
35 "(P .| #True) .= #True", "(#True .| P) .= #True", |
43 "|- (P | #True) = #True", "|- (#True | P) = #True", |
36 "(P .| #False) .= P", "(#False .| P) .= P", |
44 "|- (P | #False) = P", "|- (#False | P) = P", |
37 "(P .| P) .= P", "(P .| .~P) .= #True", "(.~P .| P) .= #True", |
45 "|- (P | P) = P", "|- (P | ~P) = #True", "|- (~P | P) = #True", |
38 "(RALL x. P) .= P", "(REX x. P) .= P", |
46 "|- (! x. P) = P", "|- (? x. P) = P", |
39 "(.~Q .-> .~P) .= (P .-> Q)", |
47 "|- (~Q --> ~P) = (P --> Q)", |
40 "(P.|Q .-> R) .= ((P.->R).&(Q.->R))" ]; |
48 "|- (P|Q --> R) = ((P-->R)&(Q-->R))" ]; |
41 |
|
42 end; |
49 end; |
43 |
50 |
44 Addsimps (intensional_rews @ int_simps); |
51 qed_goal "TrueW" Intensional.thy "|- #True" |
|
52 (fn _ => [simp_tac (simpset() addsimps [Valid_def,unl_con]) 1]); |
45 |
53 |
46 (* Derive introduction and destruction rules from definition of |
54 Addsimps (TrueW::intensional_rews); |
47 intensional validity. |
55 Addsimps int_simps; |
48 *) |
56 AddSIs [intI]; |
49 qed_goal "intI" Intensional.thy "(!!w. w |= A) ==> A" |
57 AddDs [intD]; |
50 (fn prems => [rewtac int_valid, |
|
51 resolve_tac prems 1 |
|
52 ]); |
|
53 |
58 |
54 qed_goalw "intD" Intensional.thy [int_valid] "A ==> w |= A" |
|
55 (fn [prem] => [ rtac (forall_elim_var 0 prem) 1 ]); |
|
56 |
59 |
57 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *) |
60 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *) |
58 |
61 |
59 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. |
62 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. |
60 F .= G gets (w |= F) = (w |= G) |
63 |- F = G becomes F w = G w |
61 F .-> G gets (w |= F) --> (w |= G) |
64 |- F --> G becomes F w --> G w |
62 *) |
|
63 fun int_unlift th = rewrite_rule intensional_rews (th RS intD); |
|
64 |
|
65 (* F .-> G becomes w |= F ==> w |= G *) |
|
66 fun int_mp th = zero_var_indexes ((int_unlift th) RS mp); |
|
67 |
|
68 (* F .-> G becomes [| w |= F; w |= G ==> R |] ==> R |
|
69 so that it can be used as an elimination rule |
|
70 *) |
|
71 fun int_impE th = zero_var_indexes ((int_unlift th) RS impE); |
|
72 |
|
73 (* F .& G .-> H becomes [| w |= F; w |= G |] ==> w |= H *) |
|
74 fun int_conjmp th = zero_var_indexes (conjI RS (int_mp th)); |
|
75 |
|
76 (* F .& G .-> H becomes [| w |= F; w |= G; (w |= H ==> R) |] ==> R *) |
|
77 fun int_conjimpE th = zero_var_indexes (conjI RS (int_impE th)); |
|
78 |
|
79 (* Turn F .= G into meta-level rewrite rule F == G *) |
|
80 fun int_rewrite th = (rewrite_rule intensional_rews (th RS inteq_reflection)); |
|
81 |
|
82 (* Make the simplifier accept "intensional" goals by first unlifting them. |
|
83 This is the standard way of proving "intensional" theorems; apply |
|
84 int_rewrite (or action_rewrite, temp_rewrite) to convert "x .= y" into "x == y" |
|
85 if you want to rewrite without unlifting. |
|
86 *) |
|
87 fun maybe_unlift th = |
|
88 (case concl_of th of |
|
89 Const("Intensional.TrueInt",_) $ p => int_unlift th |
|
90 | _ => th); |
|
91 |
|
92 simpset_ref() := simpset() setmksimps ((mksimps mksimps_pairs) o maybe_unlift); |
|
93 |
|
94 |
|
95 (* ==================== Rewrites for abstractions ==================== *) |
|
96 |
|
97 (* The following are occasionally useful. Don't add them to the default |
|
98 simpset, or it will loop! Alternatively, we could replace the "unl_XXX" |
|
99 rules by definitions of lifting via lambda abstraction, but then proof |
|
100 states would have lots of lambdas, and would be hard to read. |
|
101 *) |
65 *) |
102 |
66 |
103 qed_goal "con_abs" Intensional.thy "(%w. c) == #c" |
67 fun int_unlift th = |
104 (fn _ => [rtac inteq_reflection 1, |
68 rewrite_rule intensional_rews ((th RS intD) handle _ => th); |
105 rtac intI 1, |
|
106 rewrite_goals_tac intensional_rews, |
|
107 rtac refl 1 |
|
108 ]); |
|
109 |
69 |
110 qed_goal "lift_abs" Intensional.thy "(%w. f(x w)) == (f[x])" |
70 (* Turn |- F = G into meta-level rewrite rule F == G *) |
111 (fn _ => [rtac inteq_reflection 1, |
71 fun int_rewrite th = |
112 rtac intI 1, |
72 zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection)); |
113 rewrite_goals_tac intensional_rews, |
|
114 rtac refl 1 |
|
115 ]); |
|
116 |
73 |
117 qed_goal "lift2_abs" Intensional.thy "(%w. f(x w) (y w)) == (f[x,y])" |
74 (* flattening turns "-->" into "==>" and eliminates conjunctions in the |
118 (fn _ => [rtac inteq_reflection 1, |
75 antecedent. For example, |
119 rtac intI 1, |
|
120 rewrite_goals_tac intensional_rews, |
|
121 rtac refl 1 |
|
122 ]); |
|
123 |
76 |
124 qed_goal "lift2_abs_con1" Intensional.thy "(%w. f x (y w)) == (f[#x,y])" |
77 P & Q --> (R | S --> T) becomes [| P; Q; R | S |] ==> T |
125 (fn _ => [rtac inteq_reflection 1, |
|
126 rtac intI 1, |
|
127 rewrite_goals_tac intensional_rews, |
|
128 rtac refl 1 |
|
129 ]); |
|
130 |
78 |
131 qed_goal "lift2_abs_con2" Intensional.thy "(%w. f(x w) y) == (f[x,#y])" |
79 Flattening can be useful with "intensional" lemmas (after unlifting). |
132 (fn _ => [rtac inteq_reflection 1, |
80 Naive resolution with mp and conjI may run away because of higher-order |
133 rtac intI 1, |
81 unification, therefore the code is a little awkward. |
134 rewrite_goals_tac intensional_rews, |
82 *) |
135 rtac refl 1 |
83 fun flatten t = |
136 ]); |
84 let |
|
85 (* analogous to RS, but using matching instead of resolution *) |
|
86 fun matchres tha i thb = |
|
87 case Seq.chop (2, biresolution true [(false,tha)] i thb) of |
|
88 ([th],_) => th |
|
89 | ([],_) => raise THM("matchres: no match", i, [tha,thb]) |
|
90 | _ => raise THM("matchres: multiple unifiers", i, [tha,thb]) |
137 |
91 |
138 qed_goal "lift3_abs" Intensional.thy "(%w. f(x w) (y w) (z w)) == (f[x,y,z])" |
92 (* match tha with some premise of thb *) |
139 (fn _ => [rtac inteq_reflection 1, |
93 fun matchsome tha thb = |
140 rtac intI 1, |
94 let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb]) |
141 rewrite_goals_tac intensional_rews, |
95 | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1) |
142 rtac refl 1 |
96 in hmatch (nprems_of thb) end |
143 ]); |
|
144 |
97 |
145 qed_goal "lift3_abs_con1" Intensional.thy "(%w. f x (y w) (z w)) == (f[#x,y,z])" |
98 fun hflatten t = |
146 (fn _ => [rtac inteq_reflection 1, |
99 case (concl_of t) of |
147 rtac intI 1, |
100 Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp) |
148 rewrite_goals_tac intensional_rews, |
101 | _ => (hflatten (matchsome conjI t)) handle _ => zero_var_indexes t |
149 rtac refl 1 |
102 in |
150 ]); |
103 hflatten t |
|
104 end; |
151 |
105 |
152 qed_goal "lift3_abs_con2" Intensional.thy "(%w. f (x w) y (z w)) == (f[x,#y,z])" |
106 fun int_use th = |
153 (fn _ => [rtac inteq_reflection 1, |
107 case (concl_of th) of |
154 rtac intI 1, |
108 Const _ $ (Const ("Intensional.Valid", _) $ _) => |
155 rewrite_goals_tac intensional_rews, |
109 ((flatten (int_unlift th)) handle _ => th) |
156 rtac refl 1 |
110 | _ => th; |
157 ]); |
|
158 |
111 |
159 qed_goal "lift3_abs_con3" Intensional.thy "(%w. f (x w) (y w) z) == (f[x,y,#z])" |
112 (*** |
160 (fn _ => [rtac inteq_reflection 1, |
113 (* Make the simplifier accept "intensional" goals by either turning them into |
161 rtac intI 1, |
114 a meta-equality or by unlifting them. |
162 rewrite_goals_tac intensional_rews, |
115 *) |
163 rtac refl 1 |
|
164 ]); |
|
165 |
116 |
166 qed_goal "lift3_abs_con12" Intensional.thy "(%w. f x y (z w)) == (f[#x,#y,z])" |
117 let |
167 (fn _ => [rtac inteq_reflection 1, |
118 val ss = simpset_ref() |
168 rtac intI 1, |
119 fun try_rewrite th = (int_rewrite th) handle _ => (int_use th) handle _ => th |
169 rewrite_goals_tac intensional_rews, |
120 in |
170 rtac refl 1 |
121 ss := !ss setmksimps ((mksimps mksimps_pairs) o try_rewrite) |
171 ]); |
122 end; |
172 |
123 ***) |
173 qed_goal "lift3_abs_con13" Intensional.thy "(%w. f x (y w) z) == (f[#x,y,#z])" |
|
174 (fn _ => [rtac inteq_reflection 1, |
|
175 rtac intI 1, |
|
176 rewrite_goals_tac intensional_rews, |
|
177 rtac refl 1 |
|
178 ]); |
|
179 |
|
180 qed_goal "lift3_abs_con23" Intensional.thy "(%w. f (x w) y z) == (f[x,#y,#z])" |
|
181 (fn _ => [rtac inteq_reflection 1, |
|
182 rtac intI 1, |
|
183 rewrite_goals_tac intensional_rews, |
|
184 rtac refl 1 |
|
185 ]); |
|
186 |
124 |
187 (* ========================================================================= *) |
125 (* ========================================================================= *) |
188 |
126 |
189 qed_goal "Not_rall" Intensional.thy |
127 qed_goal "Not_Rall" Intensional.thy |
190 "(.~ (RALL x. F(x))) .= (REX x. .~ F(x))" |
128 "|- (~(! x. F x)) = (? x. ~F x)" |
191 (fn _ => [rtac intI 1, |
129 (fn _ => [simp_tac (simpset() addsimps [Valid_def]) 1]); |
192 rewrite_goals_tac intensional_rews, |
|
193 fast_tac HOL_cs 1 |
|
194 ]); |
|
195 |
130 |
196 qed_goal "Not_rex" Intensional.thy |
131 qed_goal "Not_Rex" Intensional.thy |
197 "(.~ (REX x. F(x))) .= (RALL x. .~ F(x))" |
132 "|- (~ (? x. F x)) = (! x. ~ F x)" |
198 (fn _ => [rtac intI 1, |
133 (fn _ => [simp_tac (simpset() addsimps [Valid_def]) 1]); |
199 rewrite_goals_tac intensional_rews, |
|
200 fast_tac HOL_cs 1 |
|
201 ]); |
|
202 |
134 |
203 (* IntLemmas.ML contains a collection of further lemmas about "intensional" logic. |
135 (* IntLemmas.ML contains a collection of further lemmas about "intensional" logic. |
204 These are not loaded by default because they are not required for the |
136 These are not loaded by default because they are not required for the |
205 standard proof procedures that first unlift proof goals to the HOL level. |
137 standard proof procedures that first unlift proof goals to the HOL level. |
206 |
138 |