|
1 (* Title: LK/lk.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Tactics and lemmas for lk.thy (thanks also to Philippe de Groote) |
|
7 *) |
|
8 |
|
9 open LK; |
|
10 |
|
11 (*Higher precedence than := facilitates use of references*) |
|
12 infix 4 add_safes add_unsafes; |
|
13 |
|
14 signature LK_RESOLVE = |
|
15 sig |
|
16 datatype pack = Pack of thm list * thm list |
|
17 val add_safes: pack * thm list -> pack |
|
18 val add_unsafes: pack * thm list -> pack |
|
19 val allL_thin: thm |
|
20 val best_tac: pack -> int -> tactic |
|
21 val could_res: term * term -> bool |
|
22 val could_resolve_seq: term * term -> bool |
|
23 val cutL_tac: string -> int -> tactic |
|
24 val cutR_tac: string -> int -> tactic |
|
25 val conL: thm |
|
26 val conR: thm |
|
27 val empty_pack: pack |
|
28 val exR_thin: thm |
|
29 val fast_tac: pack -> int -> tactic |
|
30 val filseq_resolve_tac: thm list -> int -> int -> tactic |
|
31 val forms_of_seq: term -> term list |
|
32 val has_prems: int -> thm -> bool |
|
33 val iffL: thm |
|
34 val iffR: thm |
|
35 val less: thm * thm -> bool |
|
36 val LK_dup_pack: pack |
|
37 val LK_pack: pack |
|
38 val pc_tac: pack -> int -> tactic |
|
39 val prop_pack: pack |
|
40 val repeat_goal_tac: pack -> int -> tactic |
|
41 val reresolve_tac: thm list -> int -> tactic |
|
42 val RESOLVE_THEN: thm list -> (int -> tactic) -> int -> tactic |
|
43 val safe_goal_tac: pack -> int -> tactic |
|
44 val step_tac: pack -> int -> tactic |
|
45 val symL: thm |
|
46 val TrueR: thm |
|
47 end; |
|
48 |
|
49 |
|
50 structure LK_Resolve : LK_RESOLVE = |
|
51 struct |
|
52 |
|
53 (*Cut and thin, replacing the right-side formula*) |
|
54 fun cutR_tac (sP: string) i = |
|
55 res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i; |
|
56 |
|
57 (*Cut and thin, replacing the left-side formula*) |
|
58 fun cutL_tac (sP: string) i = |
|
59 res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1); |
|
60 |
|
61 |
|
62 (** If-and-only-if rules **) |
|
63 val iffR = prove_goalw LK.thy [iff_def] |
|
64 "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" |
|
65 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]); |
|
66 |
|
67 val iffL = prove_goalw LK.thy [iff_def] |
|
68 "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" |
|
69 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]); |
|
70 |
|
71 val TrueR = prove_goalw LK.thy [True_def] |
|
72 "$H |- $E, True, $F" |
|
73 (fn _=> [ rtac impR 1, rtac basic 1 ]); |
|
74 |
|
75 |
|
76 (** Weakened quantifier rules. Incomplete, they let the search terminate.**) |
|
77 |
|
78 val allL_thin = prove_goal LK.thy |
|
79 "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E" |
|
80 (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]); |
|
81 |
|
82 val exR_thin = prove_goal LK.thy |
|
83 "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F" |
|
84 (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]); |
|
85 |
|
86 (* Symmetry of equality in hypotheses *) |
|
87 val symL = prove_goal LK.thy |
|
88 "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" |
|
89 (fn prems=> |
|
90 [ (rtac cut 1), |
|
91 (rtac thinL 2), |
|
92 (resolve_tac prems 2), |
|
93 (resolve_tac [basic RS sym] 1) ]); |
|
94 |
|
95 |
|
96 (**** Theorem Packs ****) |
|
97 |
|
98 datatype pack = Pack of thm list * thm list; |
|
99 |
|
100 (*A theorem pack has the form (safe rules, unsafe rules) |
|
101 An unsafe rule is incomplete or introduces variables in subgoals, |
|
102 and is tried only when the safe rules are not applicable. *) |
|
103 |
|
104 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2); |
|
105 |
|
106 val empty_pack = Pack([],[]); |
|
107 |
|
108 fun (Pack(safes,unsafes)) add_safes ths = |
|
109 Pack(sort less (ths@safes), unsafes); |
|
110 |
|
111 fun (Pack(safes,unsafes)) add_unsafes ths = |
|
112 Pack(safes, sort less (ths@unsafes)); |
|
113 |
|
114 (*The rules of LK*) |
|
115 val prop_pack = empty_pack add_safes |
|
116 [basic, refl, conjL, conjR, disjL, disjR, impL, impR, |
|
117 notL, notR, iffL, iffR]; |
|
118 |
|
119 val LK_pack = prop_pack add_safes [allR, exL] |
|
120 add_unsafes [allL_thin, exR_thin]; |
|
121 |
|
122 val LK_dup_pack = prop_pack add_safes [allR, exL] |
|
123 add_unsafes [allL, exR]; |
|
124 |
|
125 |
|
126 |
|
127 (*Returns the list of all formulas in the sequent*) |
|
128 fun forms_of_seq (Const("Seqof",_) $ P $ u) = P :: forms_of_seq u |
|
129 | forms_of_seq (H $ u) = forms_of_seq u |
|
130 | forms_of_seq _ = []; |
|
131 |
|
132 (*Tests whether two sequences (left or right sides) could be resolved. |
|
133 seqp is a premise (subgoal), seqc is a conclusion of an object-rule. |
|
134 Assumes each formula in seqc is surrounded by sequence variables |
|
135 -- checks that each concl formula looks like some subgoal formula. |
|
136 It SHOULD check order as well, using recursion rather than forall/exists*) |
|
137 fun could_res (seqp,seqc) = |
|
138 forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) |
|
139 (forms_of_seq seqp)) |
|
140 (forms_of_seq seqc); |
|
141 |
|
142 (*Tests whether two sequents G|-H could be resolved, comparing each side.*) |
|
143 fun could_resolve_seq (prem,conc) = |
|
144 case (prem,conc) of |
|
145 (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp), |
|
146 _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) => |
|
147 could_res (leftp,leftc) andalso could_res (rightp,rightc) |
|
148 | _ => false; |
|
149 |
|
150 |
|
151 (*Like filt_resolve_tac, using could_resolve_seq |
|
152 Much faster than resolve_tac when there are many rules. |
|
153 Resolve subgoal i using the rules, unless more than maxr are compatible. *) |
|
154 fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) => |
|
155 let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules) |
|
156 in if length rls > maxr then no_tac else resolve_tac rls i |
|
157 end); |
|
158 |
|
159 |
|
160 (*Predicate: does the rule have n premises? *) |
|
161 fun has_prems n rule = (nprems_of rule = n); |
|
162 |
|
163 (*Continuation-style tactical for resolution. |
|
164 The list of rules is partitioned into 0, 1, 2 premises. |
|
165 The resulting tactic, gtac, tries to resolve with rules. |
|
166 If successful, it recursively applies nextac to the new subgoals only. |
|
167 Else fails. (Treatment of goals due to Ph. de Groote) |
|
168 Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *) |
|
169 |
|
170 (*Takes rule lists separated in to 0, 1, 2, >2 premises. |
|
171 The abstraction over state prevents needless divergence in recursion. |
|
172 The 9999 should be a parameter, to delay treatment of flexible goals. *) |
|
173 fun RESOLVE_THEN rules = |
|
174 let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules; |
|
175 fun tac nextac i = STATE (fn state => |
|
176 filseq_resolve_tac rls0 9999 i |
|
177 ORELSE |
|
178 (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i)) |
|
179 ORELSE |
|
180 (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1)) |
|
181 THEN TRY(nextac i)) ) |
|
182 in tac end; |
|
183 |
|
184 |
|
185 (*repeated resolution applied to the designated goal*) |
|
186 fun reresolve_tac rules = |
|
187 let val restac = RESOLVE_THEN rules; (*preprocessing done now*) |
|
188 fun gtac i = restac gtac i |
|
189 in gtac end; |
|
190 |
|
191 (*tries the safe rules repeatedly before the unsafe rules. *) |
|
192 fun repeat_goal_tac (Pack(safes,unsafes)) = |
|
193 let val restac = RESOLVE_THEN safes |
|
194 and lastrestac = RESOLVE_THEN unsafes; |
|
195 fun gtac i = restac gtac i ORELSE lastrestac gtac i |
|
196 in gtac end; |
|
197 |
|
198 |
|
199 (*Tries safe rules only*) |
|
200 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes; |
|
201 |
|
202 (*Tries a safe rule or else a unsafe rule. Single-step for tracing. *) |
|
203 fun step_tac (thm_pack as Pack(safes,unsafes)) = |
|
204 safe_goal_tac thm_pack ORELSE' |
|
205 filseq_resolve_tac unsafes 9999; |
|
206 |
|
207 |
|
208 (* Tactic for reducing a goal, using Predicate Calculus rules. |
|
209 A decision procedure for Propositional Calculus, it is incomplete |
|
210 for Predicate-Calculus because of allL_thin and exR_thin. |
|
211 Fails if it can do nothing. *) |
|
212 fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1)); |
|
213 |
|
214 (*The following two tactics are analogous to those provided by |
|
215 Provers/classical. In fact, pc_tac is usually FASTER than fast_tac!*) |
|
216 fun fast_tac thm_pack = |
|
217 SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1)); |
|
218 |
|
219 fun best_tac thm_pack = |
|
220 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) |
|
221 (step_tac thm_pack 1)); |
|
222 |
|
223 (** Contraction. Useful since some rules are not complete. **) |
|
224 |
|
225 val conR = prove_goal LK.thy |
|
226 "$H |- $E, P, $F, P ==> $H |- $E, P, $F" |
|
227 (fn prems=> |
|
228 [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]); |
|
229 |
|
230 val conL = prove_goal LK.thy |
|
231 "$H, P, $G, P |- $E ==> $H, P, $G |- $E" |
|
232 (fn prems=> |
|
233 [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]); |
|
234 |
|
235 end; |
|
236 |
|
237 open LK_Resolve; |