author | paulson |
Thu, 04 Apr 1996 10:24:38 +0200 (1996-04-04) | |
changeset 1639 | d3484e841d1e |
parent 1587 | e7d8a4957bac |
child 1711 | c06d01f75764 |
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 |
||
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
17 |
infix 1 THEN_MAYBE; |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
18 |
|
0 | 19 |
signature CLASSICAL_DATA = |
20 |
sig |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
21 |
val mp : thm (* [| P-->Q; P |] ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
22 |
val not_elim : thm (* [| ~P; P |] ==> R *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
23 |
val classical : thm (* (~P ==> P) ==> P *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
24 |
val sizef : thm -> int (* size function for BEST_FIRST *) |
0 | 25 |
val hyp_subst_tacs: (int -> tactic) list |
26 |
end; |
|
27 |
||
28 |
(*Higher precedence than := facilitates use of references*) |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
29 |
infix 4 addSIs addSEs addSDs addIs addEs addDs |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
30 |
setwrapper compwrapper addbefore addafter; |
0 | 31 |
|
32 |
||
33 |
signature CLASSICAL = |
|
34 |
sig |
|
35 |
type claset |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
36 |
type netpair |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
37 |
val empty_cs : claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
38 |
val addDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
39 |
val addEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
40 |
val addIs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
41 |
val addSDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
42 |
val addSEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
43 |
val addSIs : claset * thm list -> claset |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
44 |
val setwrapper : claset * (tactic->tactic) -> claset |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
45 |
val compwrapper : claset * (tactic->tactic) -> claset |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
46 |
val addbefore : claset * tactic -> claset |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
47 |
val addafter : claset * tactic -> claset |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
48 |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
49 |
val print_cs : claset -> unit |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
50 |
val rep_claset : |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
51 |
claset -> {safeIs: thm list, safeEs: thm list, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
52 |
hazIs: thm list, hazEs: thm list, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
53 |
wrapper: tactic -> tactic, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
54 |
safe0_netpair: netpair, safep_netpair: netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
55 |
haz_netpair: netpair, dup_netpair: netpair} |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
56 |
val getwrapper : claset -> tactic -> tactic |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
57 |
val THEN_MAYBE : tactic * tactic -> tactic |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
58 |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
59 |
val fast_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
60 |
val slow_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
61 |
val weight_ASTAR : int ref |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
62 |
val astar_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
63 |
val slow_astar_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
64 |
val best_tac : claset -> int -> tactic |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
65 |
val slow_best_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
66 |
val depth_tac : claset -> int -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
67 |
val deepen_tac : claset -> int -> int -> tactic |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
68 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
69 |
val contr_tac : int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
70 |
val dup_elim : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
71 |
val dup_intr : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
72 |
val dup_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
73 |
val eq_mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
74 |
val haz_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
75 |
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
|
76 |
val mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
77 |
val safe_tac : claset -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
78 |
val safe_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
79 |
val step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
80 |
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
81 |
val swapify : thm list -> thm list |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
82 |
val swap_res_tac : thm list -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
83 |
val inst_step_tac : claset -> int -> tactic |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
84 |
val inst0_step_tac : claset -> int -> tactic |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
85 |
val instp_step_tac : claset -> int -> tactic |
0 | 86 |
end; |
87 |
||
88 |
||
89 |
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
|
90 |
struct |
|
91 |
||
92 |
local open Data in |
|
93 |
||
94 |
(** Useful tactics for classical reasoning **) |
|
95 |
||
1524 | 96 |
val imp_elim = (*cannot use bind_thm within a structure!*) |
97 |
store_thm ("imp_elim", make_elim mp); |
|
0 | 98 |
|
99 |
(*Solve goal that assumes both P and ~P. *) |
|
100 |
val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; |
|
101 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
102 |
(*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
|
103 |
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
|
104 |
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; |
0 | 105 |
|
106 |
(*Like mp_tac but instantiates no variables*) |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
107 |
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
|
108 |
|
1524 | 109 |
val swap = |
110 |
store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical)); |
|
0 | 111 |
|
112 |
(*Creates rules to eliminate ~A, from rules to introduce A*) |
|
113 |
fun swapify intrs = intrs RLN (2, [swap]); |
|
114 |
||
115 |
(*Uses introduction rules in the normal way, or on negated assumptions, |
|
116 |
trying rules in order. *) |
|
117 |
fun swap_res_tac rls = |
|
54 | 118 |
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls |
119 |
in assume_tac ORELSE' |
|
120 |
contr_tac ORELSE' |
|
121 |
biresolve_tac (foldr addrl (rls,[])) |
|
0 | 122 |
end; |
123 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
124 |
(*Duplication of hazardous rules, for complete provers*) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
125 |
fun dup_intr th = standard (th RS classical); |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
126 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
127 |
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
|
128 |
rule_by_tactic (TRYALL (etac revcut_rl)); |
0 | 129 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
130 |
|
0 | 131 |
(*** Classical rule sets ***) |
132 |
||
133 |
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; |
|
134 |
||
135 |
datatype claset = |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
136 |
CS of {safeIs : thm list, (*safe introduction rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
137 |
safeEs : thm list, (*safe elimination rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
138 |
hazIs : thm list, (*unsafe introduction rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
139 |
hazEs : thm list, (*unsafe elimination rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
140 |
wrapper : tactic->tactic, (*for transforming step_tac*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
141 |
safe0_netpair : netpair, (*nets for trivial cases*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
142 |
safep_netpair : netpair, (*nets for >0 subgoals*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
143 |
haz_netpair : netpair, (*nets for unsafe rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
144 |
dup_netpair : netpair}; (*nets for duplication*) |
0 | 145 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
146 |
(*Desired invariants are |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
147 |
safe0_netpair = build safe0_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
148 |
safep_netpair = build safep_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
149 |
haz_netpair = build (joinrules(hazIs, hazEs)), |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
150 |
dup_netpair = build (joinrules(map dup_intr hazIs, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
151 |
map dup_elim hazEs))} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
152 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
153 |
where build = build_netpair(Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
154 |
safe0_brls contains all brules that solve the subgoal, and |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
155 |
safep_brls contains all brules that generate 1 or more new subgoals. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
156 |
Nets must be built incrementally, to save space and time. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
157 |
*) |
0 | 158 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
159 |
val empty_cs = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
160 |
CS{safeIs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
161 |
safeEs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
162 |
hazIs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
163 |
hazEs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
164 |
wrapper = I, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
165 |
safe0_netpair = (Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
166 |
safep_netpair = (Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
167 |
haz_netpair = (Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
168 |
dup_netpair = (Net.empty,Net.empty)}; |
0 | 169 |
|
170 |
fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
171 |
(writeln"Introduction rules"; prths hazIs; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
172 |
writeln"Safe introduction rules"; prths safeIs; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
173 |
writeln"Elimination rules"; prths hazEs; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
174 |
writeln"Safe elimination rules"; prths safeEs; |
0 | 175 |
()); |
176 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
177 |
fun rep_claset (CS args) = args; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
178 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
179 |
fun getwrapper (CS{wrapper,...}) = wrapper; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
180 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
181 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
182 |
(** Adding (un)safe introduction or elimination rules. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
183 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
184 |
In case of overlap, new rules are tried BEFORE old ones!! |
1010 | 185 |
**) |
0 | 186 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
187 |
(*For use with biresolve_tac. Combines intr rules with swap to handle negated |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
188 |
assumptions. Pairs elim rules with true. *) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
189 |
fun joinrules (intrs,elims) = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
190 |
(map (pair true) (elims @ swapify intrs) @ |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
191 |
map (pair false) intrs); |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
192 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
193 |
(*Priority: prefer rules with fewest subgoals, |
1231 | 194 |
then rules added most recently (preferring the head of the list).*) |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
195 |
fun tag_brls k [] = [] |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
196 |
| tag_brls k (brl::brls) = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
197 |
(1000000*subgoals_of_brl brl + k, brl) :: |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
198 |
tag_brls (k+1) brls; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
199 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
200 |
fun insert_tagged_list kbrls np = foldr insert_tagged_brl (kbrls, np); |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
201 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
202 |
(*Insert into netpair that already has nI intr rules and nE elim rules. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
203 |
Count the intr rules double (to account for swapify). Negate to give the |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
204 |
new insertions the lowest priority.*) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
205 |
fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
206 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
207 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
208 |
(** Safe rules **) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
209 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
210 |
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
211 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
212 |
addSIs ths = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
213 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
214 |
take_prefix (fn rl => nprems_of rl=0) ths |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
215 |
val nI = length safeIs + length ths |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
216 |
and nE = length safeEs |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
217 |
in CS{safeIs = ths@safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
218 |
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
219 |
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
220 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
221 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
222 |
hazEs = hazEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
223 |
wrapper = wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
224 |
haz_netpair = haz_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
225 |
dup_netpair = dup_netpair} |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
226 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
227 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
228 |
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
229 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
230 |
addSEs ths = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
231 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
232 |
take_prefix (fn rl => nprems_of rl=1) ths |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
233 |
val nI = length safeIs |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
234 |
and nE = length safeEs + length ths |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
235 |
in |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
236 |
CS{safeEs = ths@safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
237 |
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
238 |
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
239 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
240 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
241 |
hazEs = hazEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
242 |
wrapper = wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
243 |
haz_netpair = haz_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
244 |
dup_netpair = dup_netpair} |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
245 |
end; |
0 | 246 |
|
247 |
fun cs addSDs ths = cs addSEs (map make_elim ths); |
|
248 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
249 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
250 |
(** Hazardous (unsafe) rules **) |
0 | 251 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
252 |
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
253 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
254 |
addIs ths = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
255 |
let val nI = length hazIs + length ths |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
256 |
and nE = length hazEs |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
257 |
in |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
258 |
CS{hazIs = ths@hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
259 |
haz_netpair = insert (nI,nE) (ths, []) haz_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
260 |
dup_netpair = insert (nI,nE) (map dup_intr ths, []) dup_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
261 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
262 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
263 |
hazEs = hazEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
264 |
wrapper = wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
265 |
safe0_netpair = safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
266 |
safep_netpair = safep_netpair} |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
267 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
268 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
269 |
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
270 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
271 |
addEs ths = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
272 |
let val nI = length hazIs |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
273 |
and nE = length hazEs + length ths |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
274 |
in |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
275 |
CS{hazEs = ths@hazEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
276 |
haz_netpair = insert (nI,nE) ([], ths) haz_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
277 |
dup_netpair = insert (nI,nE) ([], map dup_elim ths) dup_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
278 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
279 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
280 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
281 |
wrapper = wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
282 |
safe0_netpair = safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
283 |
safep_netpair = safep_netpair} |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
284 |
end; |
0 | 285 |
|
286 |
fun cs addDs ths = cs addEs (map make_elim ths); |
|
287 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
288 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
289 |
(** Setting or modifying the wrapper tactical **) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
290 |
|
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
291 |
(*Set a new wrapper*) |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
292 |
fun (CS{safeIs, safeEs, hazIs, hazEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
293 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
294 |
setwrapper new_wrapper = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
295 |
CS{wrapper = new_wrapper, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
296 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
297 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
298 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
299 |
hazEs = hazEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
300 |
safe0_netpair = safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
301 |
safep_netpair = safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
302 |
haz_netpair = haz_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
303 |
dup_netpair = dup_netpair}; |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
304 |
|
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
305 |
(*Compose a tactical with the existing wrapper*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
306 |
fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs); |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
307 |
|
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
308 |
(*Execute tac1, but only execute tac2 if there are at least as many subgoals |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
309 |
as before. This ensures that tac2 is only applied to an outcome of tac1.*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
310 |
fun tac1 THEN_MAYBE tac2 = |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
311 |
STATE (fn state => |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
312 |
tac1 THEN |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
313 |
COND (has_fewer_prems (nprems_of state)) all_tac tac2); |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
314 |
|
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
315 |
(*Cause a tactic to be executed before/after the step tactic*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
316 |
fun cs addbefore tac2 = cs compwrapper (fn tac1 => tac2 THEN_MAYBE tac1); |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
317 |
fun cs addafter tac2 = cs compwrapper (fn tac1 => tac1 THEN_MAYBE tac2); |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
318 |
|
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
319 |
|
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
320 |
|
0 | 321 |
(*** Simple tactics for theorem proving ***) |
322 |
||
323 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
324 |
fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
|
325 |
FIRST' [eq_assume_tac, |
|
326 |
eq_mp_tac, |
|
327 |
bimatch_from_nets_tac safe0_netpair, |
|
328 |
FIRST' hyp_subst_tacs, |
|
329 |
bimatch_from_nets_tac safep_netpair] ; |
|
330 |
||
331 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
332 |
fun safe_tac cs = REPEAT_DETERM_FIRST (safe_step_tac cs); |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
333 |
|
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
334 |
(*But these unsafe steps at least solve a subgoal!*) |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
335 |
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
336 |
assume_tac APPEND' |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
337 |
contr_tac APPEND' |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
338 |
biresolve_from_nets_tac safe0_netpair; |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
339 |
|
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
340 |
(*These are much worse since they could generate more and more subgoals*) |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
341 |
fun instp_step_tac (CS{safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
342 |
biresolve_from_nets_tac safep_netpair; |
0 | 343 |
|
344 |
(*These steps could instantiate variables and are therefore unsafe.*) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
345 |
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; |
0 | 346 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
347 |
fun haz_step_tac (CS{haz_netpair,...}) = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
348 |
biresolve_from_nets_tac haz_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
349 |
|
0 | 350 |
(*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
|
351 |
fun step_tac cs i = |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
352 |
getwrapper cs |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
353 |
(FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]); |
0 | 354 |
|
355 |
(*Using a "safe" rule to instantiate variables is unsafe. This tactic |
|
356 |
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
|
357 |
fun slow_step_tac cs i = |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
358 |
getwrapper cs |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
359 |
(safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i)); |
0 | 360 |
|
361 |
(*** The following tactics all fail unless they solve one goal ***) |
|
362 |
||
363 |
(*Dumb but fast*) |
|
364 |
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
|
365 |
||
366 |
(*Slower but smarter than fast_tac*) |
|
367 |
fun best_tac cs = |
|
368 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); |
|
369 |
||
370 |
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
|
371 |
||
372 |
fun slow_best_tac cs = |
|
373 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
|
374 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
375 |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
376 |
(**ASTAR with weight weight_ASTAR, by Norbert Voelker*) |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
377 |
val weight_ASTAR = ref 5; |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
378 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
379 |
fun astar_tac cs = |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
380 |
SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
381 |
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
382 |
(step_tac cs 1)); |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
383 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
384 |
fun slow_astar_tac cs = |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
385 |
SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
386 |
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
387 |
(slow_step_tac cs 1)); |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
388 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
389 |
(*** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
390 |
of much experimentation! Changing APPEND to ORELSE below would prove |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
391 |
easy theorems faster, but loses completeness -- and many of the harder |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
392 |
theorems such as 43. ***) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
393 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
394 |
(*Non-deterministic! Could always expand the first unsafe connective. |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
395 |
That's hard to implement and did not perform better in experiments, due to |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
396 |
greater search depth required.*) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
397 |
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
|
398 |
biresolve_from_nets_tac dup_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
399 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
400 |
(*Searching to depth m.*) |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
401 |
fun depth_tac cs m i = STATE(fn state => |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
402 |
SELECT_GOAL |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
403 |
(REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
404 |
(DEPTH_SOLVE (depth_tac cs m 1), |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
405 |
inst0_step_tac cs 1 APPEND |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
406 |
COND (K(m=0)) no_tac |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
407 |
((instp_step_tac cs 1 APPEND dup_step_tac cs 1) |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
408 |
THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)))) |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
409 |
i); |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
410 |
|
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
411 |
(*Iterative deepening tactical. Allows us to "deepen" any search tactic*) |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
412 |
fun DEEPEN tacf m i = STATE(fn state => |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
413 |
if has_fewer_prems i state then no_tac |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
414 |
else (writeln ("Depth = " ^ string_of_int m); |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
415 |
tacf m i ORELSE DEEPEN tacf (m+2) i)); |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
416 |
|
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
417 |
fun safe_depth_tac cs m = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
418 |
SUBGOAL |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
419 |
(fn (prem,i) => |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
420 |
let val deti = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
421 |
(*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
|
422 |
case term_vars prem of |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
423 |
[] => DETERM |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
424 |
| _::_ => I |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
425 |
in SELECT_GOAL (TRY (safe_tac cs) THEN |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
426 |
DEPTH_SOLVE (deti (depth_tac cs m 1))) i |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
427 |
end); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
428 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
429 |
fun deepen_tac cs = DEEPEN (safe_depth_tac cs); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
430 |
|
0 | 431 |
end; |
432 |
end; |