author | lcp |
Wed, 02 Nov 1994 12:48:22 +0100 | |
changeset 681 | 9b02474744ca |
parent 469 | b571d997178d |
child 747 | bdc066781063 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: Provers/classical |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
Theorem prover for classical reasoning, including predicate calculus, set |
|
7 |
theory, etc. |
|
8 |
||
9 |
Rules must be classified as intr, elim, safe, hazardous. |
|
10 |
||
11 |
A rule is unsafe unless it can be applied blindly without harmful results. |
|
12 |
For a rule to be safe, its premises and conclusion should be logically |
|
13 |
equivalent. There should be no variables in the premises that are not in |
|
14 |
the conclusion. |
|
15 |
*) |
|
16 |
||
17 |
signature CLASSICAL_DATA = |
|
18 |
sig |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
19 |
val mp : thm (* [| P-->Q; P |] ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
20 |
val not_elim : thm (* [| ~P; P |] ==> R *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
21 |
val classical : thm (* (~P ==> P) ==> P *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
22 |
val sizef : thm -> int (* size function for BEST_FIRST *) |
0 | 23 |
val hyp_subst_tacs: (int -> tactic) list |
24 |
end; |
|
25 |
||
26 |
(*Higher precedence than := facilitates use of references*) |
|
27 |
infix 4 addSIs addSEs addSDs addIs addEs addDs; |
|
28 |
||
29 |
||
30 |
signature CLASSICAL = |
|
31 |
sig |
|
32 |
type claset |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
33 |
val empty_cs : claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
34 |
val addDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
35 |
val addEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
36 |
val addIs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
37 |
val addSDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
38 |
val addSEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
39 |
val addSIs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
40 |
val print_cs : claset -> unit |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
41 |
val rep_claset : claset -> {safeIs: thm list, safeEs: thm list, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
42 |
hazIs: thm list, hazEs: thm list} |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
43 |
val best_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
44 |
val contr_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
45 |
val depth_tac : claset -> int -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
46 |
val deepen_tac : claset -> int -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
47 |
val dup_elim : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
48 |
val dup_intr : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
49 |
val dup_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
50 |
val eq_mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
51 |
val fast_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
52 |
val haz_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
53 |
val joinrules : thm list * thm list -> (bool * thm) list |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
54 |
val mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
55 |
val safe_tac : claset -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
56 |
val safe_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
57 |
val slow_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
58 |
val slow_best_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
59 |
val slow_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
60 |
val step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
61 |
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
62 |
val swapify : thm list -> thm list |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
63 |
val swap_res_tac : thm list -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
64 |
val inst_step_tac : claset -> int -> tactic |
0 | 65 |
end; |
66 |
||
67 |
||
68 |
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
|
69 |
struct |
|
70 |
||
71 |
local open Data in |
|
72 |
||
73 |
(** Useful tactics for classical reasoning **) |
|
74 |
||
75 |
val imp_elim = make_elim mp; |
|
76 |
||
77 |
(*Solve goal that assumes both P and ~P. *) |
|
78 |
val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; |
|
79 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
80 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q. |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
81 |
Could do the same thing for P<->Q and P... *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
82 |
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; |
0 | 83 |
|
84 |
(*Like mp_tac but instantiates no variables*) |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
85 |
fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
86 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
87 |
val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical); |
0 | 88 |
|
89 |
(*Creates rules to eliminate ~A, from rules to introduce A*) |
|
90 |
fun swapify intrs = intrs RLN (2, [swap]); |
|
91 |
||
92 |
(*Uses introduction rules in the normal way, or on negated assumptions, |
|
93 |
trying rules in order. *) |
|
94 |
fun swap_res_tac rls = |
|
54 | 95 |
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls |
96 |
in assume_tac ORELSE' |
|
97 |
contr_tac ORELSE' |
|
98 |
biresolve_tac (foldr addrl (rls,[])) |
|
0 | 99 |
end; |
100 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
101 |
(*Duplication of hazardous rules, for complete provers*) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
102 |
fun dup_intr th = standard (th RS classical); |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
103 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
104 |
fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
105 |
rule_by_tactic (TRYALL (etac revcut_rl)); |
0 | 106 |
|
107 |
(*** Classical rule sets ***) |
|
108 |
||
109 |
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; |
|
110 |
||
111 |
datatype claset = |
|
112 |
CS of {safeIs : thm list, |
|
113 |
safeEs : thm list, |
|
114 |
hazIs : thm list, |
|
115 |
hazEs : thm list, |
|
116 |
safe0_netpair : netpair, |
|
117 |
safep_netpair : netpair, |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
118 |
haz_netpair : netpair, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
119 |
dup_netpair : netpair}; |
0 | 120 |
|
121 |
fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,...}) = |
|
122 |
{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; |
|
123 |
||
124 |
(*For use with biresolve_tac. Combines intrs with swap to catch negated |
|
125 |
assumptions; pairs elims with true; sorts. *) |
|
126 |
fun joinrules (intrs,elims) = |
|
127 |
sort lessb |
|
128 |
(map (pair true) (elims @ swapify intrs) @ |
|
129 |
map (pair false) intrs); |
|
130 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
131 |
val build = build_netpair(Net.empty,Net.empty); |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
132 |
|
0 | 133 |
(*Make a claset from the four kinds of rules*) |
134 |
fun make_cs {safeIs,safeEs,hazIs,hazEs} = |
|
135 |
let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) |
|
136 |
take_prefix (fn brl => subgoals_of_brl brl=0) |
|
137 |
(joinrules(safeIs, safeEs)) |
|
138 |
in CS{safeIs = safeIs, |
|
139 |
safeEs = safeEs, |
|
140 |
hazIs = hazIs, |
|
141 |
hazEs = hazEs, |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
142 |
safe0_netpair = build safe0_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
143 |
safep_netpair = build safep_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
144 |
haz_netpair = build (joinrules(hazIs, hazEs)), |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
145 |
dup_netpair = build (joinrules(map dup_intr hazIs, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
146 |
map dup_elim hazEs))} |
0 | 147 |
end; |
148 |
||
149 |
(*** Manipulation of clasets ***) |
|
150 |
||
151 |
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; |
|
152 |
||
153 |
fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = |
|
154 |
(writeln"Introduction rules"; prths hazIs; |
|
155 |
writeln"Safe introduction rules"; prths safeIs; |
|
156 |
writeln"Elimination rules"; prths hazEs; |
|
157 |
writeln"Safe elimination rules"; prths safeEs; |
|
158 |
()); |
|
159 |
||
160 |
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = |
|
161 |
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; |
|
162 |
||
163 |
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = |
|
164 |
make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs}; |
|
165 |
||
166 |
fun cs addSDs ths = cs addSEs (map make_elim ths); |
|
167 |
||
168 |
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths = |
|
169 |
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs}; |
|
170 |
||
171 |
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths = |
|
172 |
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs}; |
|
173 |
||
174 |
fun cs addDs ths = cs addEs (map make_elim ths); |
|
175 |
||
176 |
(*** Simple tactics for theorem proving ***) |
|
177 |
||
178 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
179 |
fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
|
180 |
FIRST' [eq_assume_tac, |
|
181 |
eq_mp_tac, |
|
182 |
bimatch_from_nets_tac safe0_netpair, |
|
183 |
FIRST' hyp_subst_tacs, |
|
184 |
bimatch_from_nets_tac safep_netpair] ; |
|
185 |
||
186 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
|
187 |
fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs)); |
|
188 |
||
189 |
(*These steps could instantiate variables and are therefore unsafe.*) |
|
190 |
fun inst_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
|
191 |
assume_tac APPEND' |
|
192 |
contr_tac APPEND' |
|
193 |
biresolve_from_nets_tac safe0_netpair APPEND' |
|
194 |
biresolve_from_nets_tac safep_netpair; |
|
195 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
196 |
fun haz_step_tac (cs as (CS{haz_netpair,...})) = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
197 |
biresolve_from_nets_tac haz_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
198 |
|
0 | 199 |
(*Single step for the prover. FAILS unless it makes progress. *) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
200 |
fun step_tac cs i = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
201 |
FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]; |
0 | 202 |
|
203 |
(*Using a "safe" rule to instantiate variables is unsafe. This tactic |
|
204 |
allows backtracking from "safe" rules to "unsafe" rules here.*) |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
205 |
fun slow_step_tac cs i = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
206 |
safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i); |
0 | 207 |
|
208 |
(*** The following tactics all fail unless they solve one goal ***) |
|
209 |
||
210 |
(*Dumb but fast*) |
|
211 |
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
|
212 |
||
213 |
(*Slower but smarter than fast_tac*) |
|
214 |
fun best_tac cs = |
|
215 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); |
|
216 |
||
217 |
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
|
218 |
||
219 |
fun slow_best_tac cs = |
|
220 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
|
221 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
222 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
223 |
(*** Complete(?) tactic, loosely based upon LeanTaP ***) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
224 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
225 |
(*Not deterministic. A different approach would always expand the first |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
226 |
unsafe connective. That's harder in Isabelle because etac can pick up |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
227 |
any assumption. One way is to express *all* unsafe connectives in terms |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
228 |
of universal quantification.*) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
229 |
fun dup_step_tac (cs as (CS{dup_netpair,...})) = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
230 |
biresolve_from_nets_tac dup_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
231 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
232 |
(*Searching to depth m of duplicative steps |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
233 |
Uses DEPTH_SOLVE (tac 1) instead of (ALLGOALS tac) since the latter |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
234 |
solves the subgoals in reverse order!*) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
235 |
fun depth_tac cs m = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
236 |
SUBGOAL |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
237 |
(fn (prem,i) => |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
238 |
let val deti = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
239 |
(*No Vars in the goal? No need to backtrack between goals.*) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
240 |
case term_vars prem of |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
241 |
[] => DETERM |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
242 |
| _::_ => I |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
243 |
in SELECT_GOAL (TRY (safe_tac cs) THEN |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
244 |
DEPTH_SOLVE (deti (depth_aux_tac cs m 1))) i |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
245 |
end) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
246 |
and depth_aux_tac cs m = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
247 |
SELECT_GOAL |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
248 |
(inst_step_tac cs 1 THEN DEPTH_SOLVE (depth_tac cs m 1) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
249 |
APPEND |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
250 |
COND (K(m=0)) no_tac |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
251 |
(dup_step_tac cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))); |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
252 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
253 |
fun deepen_tac cs m i = STATE(fn state => |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
254 |
if has_fewer_prems i state then no_tac |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
255 |
else (writeln ("Depth = " ^ string_of_int m); |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
256 |
depth_tac cs m i ORELSE deepen_tac cs (m+1) i)); |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
257 |
|
0 | 258 |
end; |
259 |
end; |