14 the conclusion. |
14 the conclusion. |
15 *) |
15 *) |
16 |
16 |
17 signature CLASSICAL_DATA = |
17 signature CLASSICAL_DATA = |
18 sig |
18 sig |
19 val mp: thm (* [| P-->Q; P |] ==> Q *) |
19 val mp : thm (* [| P-->Q; P |] ==> Q *) |
20 val not_elim: thm (* [| ~P; P |] ==> R *) |
20 val not_elim : thm (* [| ~P; P |] ==> R *) |
21 val swap: thm (* ~P ==> (~Q ==> P) ==> Q *) |
21 val classical : thm (* (~P ==> P) ==> P *) |
22 val sizef : thm -> int (* size function for BEST_FIRST *) |
22 val sizef : thm -> int (* size function for BEST_FIRST *) |
23 val hyp_subst_tacs: (int -> tactic) list |
23 val hyp_subst_tacs: (int -> tactic) list |
24 end; |
24 end; |
25 |
25 |
26 (*Higher precedence than := facilitates use of references*) |
26 (*Higher precedence than := facilitates use of references*) |
27 infix 4 addSIs addSEs addSDs addIs addEs addDs; |
27 infix 4 addSIs addSEs addSDs addIs addEs addDs; |
28 |
28 |
29 |
29 |
30 signature CLASSICAL = |
30 signature CLASSICAL = |
31 sig |
31 sig |
32 type claset |
32 type claset |
33 val empty_cs: claset |
33 val empty_cs : claset |
34 val addDs : claset * thm list -> claset |
34 val addDs : claset * thm list -> claset |
35 val addEs : claset * thm list -> claset |
35 val addEs : claset * thm list -> claset |
36 val addIs : claset * thm list -> claset |
36 val addIs : claset * thm list -> claset |
37 val addSDs: claset * thm list -> claset |
37 val addSDs : claset * thm list -> claset |
38 val addSEs: claset * thm list -> claset |
38 val addSEs : claset * thm list -> claset |
39 val addSIs: claset * thm list -> claset |
39 val addSIs : claset * thm list -> claset |
40 val print_cs: claset -> unit |
40 val print_cs : claset -> unit |
41 val rep_claset: claset -> |
41 val rep_claset : claset -> {safeIs: thm list, safeEs: thm list, |
42 {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list} |
42 hazIs: thm list, hazEs: thm list} |
43 val best_tac : claset -> int -> tactic |
43 val best_tac : claset -> int -> tactic |
44 val contr_tac : int -> tactic |
44 val contr_tac : int -> tactic |
45 val eq_mp_tac: int -> tactic |
45 val depth_tac : claset -> int -> int -> tactic |
46 val fast_tac : claset -> int -> tactic |
46 val deepen_tac : claset -> int -> int -> tactic |
47 val joinrules : thm list * thm list -> (bool * thm) list |
47 val dup_elim : thm -> thm |
48 val mp_tac: int -> tactic |
48 val dup_intr : thm -> thm |
49 val safe_tac : claset -> tactic |
49 val dup_step_tac : claset -> int -> tactic |
50 val safe_step_tac : claset -> int -> tactic |
50 val eq_mp_tac : int -> tactic |
51 val slow_step_tac : claset -> int -> tactic |
51 val fast_tac : claset -> int -> tactic |
52 val slow_best_tac : claset -> int -> tactic |
52 val haz_step_tac : claset -> int -> tactic |
53 val slow_tac : claset -> int -> tactic |
53 val joinrules : thm list * thm list -> (bool * thm) list |
54 val step_tac : claset -> int -> tactic |
54 val mp_tac : int -> tactic |
55 val swapify : thm list -> thm list |
55 val safe_tac : claset -> tactic |
56 val swap_res_tac : thm list -> int -> tactic |
56 val safe_step_tac : claset -> int -> tactic |
57 val inst_step_tac : claset -> int -> tactic |
57 val slow_step_tac : claset -> int -> tactic |
|
58 val slow_best_tac : claset -> int -> tactic |
|
59 val slow_tac : claset -> int -> tactic |
|
60 val step_tac : claset -> int -> tactic |
|
61 val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
|
62 val swapify : thm list -> thm list |
|
63 val swap_res_tac : thm list -> int -> tactic |
|
64 val inst_step_tac : claset -> int -> tactic |
58 end; |
65 end; |
59 |
66 |
60 |
67 |
61 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
68 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
62 struct |
69 struct |
68 val imp_elim = make_elim mp; |
75 val imp_elim = make_elim mp; |
69 |
76 |
70 (*Solve goal that assumes both P and ~P. *) |
77 (*Solve goal that assumes both P and ~P. *) |
71 val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; |
78 val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; |
72 |
79 |
73 (*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
80 (*Finds P-->Q and P in the assumptions, replaces implication by Q. |
74 fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac i; |
81 Could do the same thing for P<->Q and P... *) |
|
82 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; |
75 |
83 |
76 (*Like mp_tac but instantiates no variables*) |
84 (*Like mp_tac but instantiates no variables*) |
77 fun eq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i THEN eq_assume_tac i; |
85 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; |
|
86 |
|
87 val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical); |
78 |
88 |
79 (*Creates rules to eliminate ~A, from rules to introduce A*) |
89 (*Creates rules to eliminate ~A, from rules to introduce A*) |
80 fun swapify intrs = intrs RLN (2, [swap]); |
90 fun swapify intrs = intrs RLN (2, [swap]); |
81 |
91 |
82 (*Uses introduction rules in the normal way, or on negated assumptions, |
92 (*Uses introduction rules in the normal way, or on negated assumptions, |
98 safeEs : thm list, |
113 safeEs : thm list, |
99 hazIs : thm list, |
114 hazIs : thm list, |
100 hazEs : thm list, |
115 hazEs : thm list, |
101 safe0_netpair : netpair, |
116 safe0_netpair : netpair, |
102 safep_netpair : netpair, |
117 safep_netpair : netpair, |
103 haz_netpair : netpair}; |
118 haz_netpair : netpair, |
|
119 dup_netpair : netpair}; |
104 |
120 |
105 fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,...}) = |
121 fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,...}) = |
106 {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; |
122 {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; |
107 |
123 |
108 (*For use with biresolve_tac. Combines intrs with swap to catch negated |
124 (*For use with biresolve_tac. Combines intrs with swap to catch negated |
109 assumptions; pairs elims with true; sorts. *) |
125 assumptions; pairs elims with true; sorts. *) |
110 fun joinrules (intrs,elims) = |
126 fun joinrules (intrs,elims) = |
111 sort lessb |
127 sort lessb |
112 (map (pair true) (elims @ swapify intrs) @ |
128 (map (pair true) (elims @ swapify intrs) @ |
113 map (pair false) intrs); |
129 map (pair false) intrs); |
|
130 |
|
131 val build = build_netpair(Net.empty,Net.empty); |
114 |
132 |
115 (*Make a claset from the four kinds of rules*) |
133 (*Make a claset from the four kinds of rules*) |
116 fun make_cs {safeIs,safeEs,hazIs,hazEs} = |
134 fun make_cs {safeIs,safeEs,hazIs,hazEs} = |
117 let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) |
135 let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) |
118 take_prefix (fn brl => subgoals_of_brl brl=0) |
136 take_prefix (fn brl => subgoals_of_brl brl=0) |
119 (joinrules(safeIs, safeEs)) |
137 (joinrules(safeIs, safeEs)) |
120 in CS{safeIs = safeIs, |
138 in CS{safeIs = safeIs, |
121 safeEs = safeEs, |
139 safeEs = safeEs, |
122 hazIs = hazIs, |
140 hazIs = hazIs, |
123 hazEs = hazEs, |
141 hazEs = hazEs, |
124 safe0_netpair = build_netpair safe0_brls, |
142 safe0_netpair = build safe0_brls, |
125 safep_netpair = build_netpair safep_brls, |
143 safep_netpair = build safep_brls, |
126 haz_netpair = build_netpair (joinrules(hazIs, hazEs))} |
144 haz_netpair = build (joinrules(hazIs, hazEs)), |
|
145 dup_netpair = build (joinrules(map dup_intr hazIs, |
|
146 map dup_elim hazEs))} |
127 end; |
147 end; |
128 |
148 |
129 (*** Manipulation of clasets ***) |
149 (*** Manipulation of clasets ***) |
130 |
150 |
131 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; |
151 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; |
171 assume_tac APPEND' |
191 assume_tac APPEND' |
172 contr_tac APPEND' |
192 contr_tac APPEND' |
173 biresolve_from_nets_tac safe0_netpair APPEND' |
193 biresolve_from_nets_tac safe0_netpair APPEND' |
174 biresolve_from_nets_tac safep_netpair; |
194 biresolve_from_nets_tac safep_netpair; |
175 |
195 |
|
196 fun haz_step_tac (cs as (CS{haz_netpair,...})) = |
|
197 biresolve_from_nets_tac haz_netpair; |
|
198 |
176 (*Single step for the prover. FAILS unless it makes progress. *) |
199 (*Single step for the prover. FAILS unless it makes progress. *) |
177 fun step_tac (cs as (CS{haz_netpair,...})) i = |
200 fun step_tac cs i = |
178 FIRST [safe_tac cs, |
201 FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]; |
179 inst_step_tac cs i, |
|
180 biresolve_from_nets_tac haz_netpair i]; |
|
181 |
202 |
182 (*Using a "safe" rule to instantiate variables is unsafe. This tactic |
203 (*Using a "safe" rule to instantiate variables is unsafe. This tactic |
183 allows backtracking from "safe" rules to "unsafe" rules here.*) |
204 allows backtracking from "safe" rules to "unsafe" rules here.*) |
184 fun slow_step_tac (cs as (CS{haz_netpair,...})) i = |
205 fun slow_step_tac cs i = |
185 safe_tac cs ORELSE |
206 safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i); |
186 (inst_step_tac cs i APPEND biresolve_from_nets_tac haz_netpair i); |
|
187 |
207 |
188 (*** The following tactics all fail unless they solve one goal ***) |
208 (*** The following tactics all fail unless they solve one goal ***) |
189 |
209 |
190 (*Dumb but fast*) |
210 (*Dumb but fast*) |
191 fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
211 fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
197 fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
217 fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
198 |
218 |
199 fun slow_best_tac cs = |
219 fun slow_best_tac cs = |
200 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
220 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
201 |
221 |
|
222 |
|
223 (*** Complete(?) tactic, loosely based upon LeanTaP ***) |
|
224 |
|
225 (*Not deterministic. A different approach would always expand the first |
|
226 unsafe connective. That's harder in Isabelle because etac can pick up |
|
227 any assumption. One way is to express *all* unsafe connectives in terms |
|
228 of universal quantification.*) |
|
229 fun dup_step_tac (cs as (CS{dup_netpair,...})) = |
|
230 biresolve_from_nets_tac dup_netpair; |
|
231 |
|
232 (*Searching to depth m of duplicative steps |
|
233 Uses DEPTH_SOLVE (tac 1) instead of (ALLGOALS tac) since the latter |
|
234 solves the subgoals in reverse order!*) |
|
235 fun depth_tac cs m = |
|
236 SUBGOAL |
|
237 (fn (prem,i) => |
|
238 let val deti = |
|
239 (*No Vars in the goal? No need to backtrack between goals.*) |
|
240 case term_vars prem of |
|
241 [] => DETERM |
|
242 | _::_ => I |
|
243 in SELECT_GOAL (TRY (safe_tac cs) THEN |
|
244 DEPTH_SOLVE (deti (depth_aux_tac cs m 1))) i |
|
245 end) |
|
246 and depth_aux_tac cs m = |
|
247 SELECT_GOAL |
|
248 (inst_step_tac cs 1 THEN DEPTH_SOLVE (depth_tac cs m 1) |
|
249 APPEND |
|
250 COND (K(m=0)) no_tac |
|
251 (dup_step_tac cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))); |
|
252 |
|
253 fun deepen_tac cs m i = STATE(fn state => |
|
254 if has_fewer_prems i state then no_tac |
|
255 else (writeln ("Depth = " ^ string_of_int m); |
|
256 depth_tac cs m i ORELSE deepen_tac cs (m+1) i)); |
|
257 |
202 end; |
258 end; |
203 end; |
259 end; |