author | wenzelm |
Thu, 16 Oct 1997 15:33:06 +0200 | |
changeset 3906 | 5ae0e1324c56 |
parent 3727 | ed63c05d7992 |
child 4066 | 7b508ac609f7 |
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 |
||
2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
17 |
(*Should be a type abbreviation in signature CLASSICAL*) |
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
18 |
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; |
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
19 |
|
0 | 20 |
signature CLASSICAL_DATA = |
21 |
sig |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
22 |
val mp : thm (* [| P-->Q; P |] ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
23 |
val not_elim : thm (* [| ~P; P |] ==> R *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
24 |
val classical : thm (* (~P ==> P) ==> P *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
25 |
val sizef : thm -> int (* size function for BEST_FIRST *) |
0 | 26 |
val hyp_subst_tacs: (int -> tactic) list |
27 |
end; |
|
28 |
||
29 |
(*Higher precedence than := facilitates use of references*) |
|
1800 | 30 |
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules |
2630 | 31 |
setSWrapper compSWrapper setWrapper compWrapper |
32 |
addSbefore addSaltern addbefore addaltern; |
|
0 | 33 |
|
34 |
||
35 |
signature CLASSICAL = |
|
36 |
sig |
|
37 |
type claset |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
38 |
val empty_cs : claset |
1711 | 39 |
val merge_cs : claset * claset -> claset |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
40 |
val addDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
41 |
val addEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
42 |
val addIs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
43 |
val addSDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
44 |
val addSEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
45 |
val addSIs : claset * thm list -> claset |
1800 | 46 |
val delrules : claset * thm list -> claset |
2630 | 47 |
val setSWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset |
48 |
val compSWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset |
|
49 |
val setWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset |
|
50 |
val compWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset |
|
51 |
val addSbefore : claset * (int -> tactic) -> claset |
|
52 |
val addSaltern : claset * (int -> tactic) -> claset |
|
53 |
val addbefore : claset * (int -> tactic) -> claset |
|
54 |
val addaltern : claset * (int -> tactic) -> claset |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
55 |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
56 |
val print_cs : claset -> unit |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
57 |
val rep_claset : |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
58 |
claset -> {safeIs: thm list, safeEs: thm list, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
59 |
hazIs: thm list, hazEs: thm list, |
2630 | 60 |
uwrapper: (int -> tactic) -> (int -> tactic), |
61 |
swrapper: (int -> tactic) -> (int -> tactic), |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
62 |
safe0_netpair: netpair, safep_netpair: netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
63 |
haz_netpair: netpair, dup_netpair: netpair} |
2630 | 64 |
val getWrapper : claset -> (int -> tactic) -> (int -> tactic) |
65 |
val getSWrapper : claset -> (int -> tactic) -> (int -> tactic) |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
66 |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
67 |
val fast_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
68 |
val slow_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
69 |
val weight_ASTAR : int ref |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
70 |
val astar_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
71 |
val slow_astar_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
72 |
val best_tac : claset -> int -> tactic |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
73 |
val slow_best_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
74 |
val depth_tac : claset -> int -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
75 |
val deepen_tac : claset -> int -> int -> tactic |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
76 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
77 |
val contr_tac : int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
78 |
val dup_elim : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
79 |
val dup_intr : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
80 |
val dup_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
81 |
val eq_mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
82 |
val haz_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
83 |
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
|
84 |
val mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
85 |
val safe_tac : claset -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
86 |
val safe_step_tac : claset -> int -> tactic |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
87 |
val clarify_tac : claset -> int -> tactic |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
88 |
val clarify_step_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
89 |
val step_tac : claset -> int -> tactic |
2630 | 90 |
val slow_step_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
91 |
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
92 |
val swapify : thm list -> thm list |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
93 |
val swap_res_tac : thm list -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
94 |
val inst_step_tac : claset -> int -> tactic |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
95 |
val inst0_step_tac : claset -> int -> tactic |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
96 |
val instp_step_tac : claset -> int -> tactic |
1724 | 97 |
|
98 |
val claset : claset ref |
|
99 |
val AddDs : thm list -> unit |
|
100 |
val AddEs : thm list -> unit |
|
101 |
val AddIs : thm list -> unit |
|
102 |
val AddSDs : thm list -> unit |
|
103 |
val AddSEs : thm list -> unit |
|
104 |
val AddSIs : thm list -> unit |
|
1807 | 105 |
val Delrules : thm list -> unit |
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
106 |
val Safe_tac : tactic |
1814 | 107 |
val Safe_step_tac : int -> tactic |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
108 |
val Clarify_tac : int -> tactic |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
109 |
val Clarify_step_tac : int -> tactic |
1800 | 110 |
val Step_tac : int -> tactic |
1724 | 111 |
val Fast_tac : int -> tactic |
1800 | 112 |
val Best_tac : int -> tactic |
2066 | 113 |
val Slow_tac : int -> tactic |
114 |
val Slow_best_tac : int -> tactic |
|
1800 | 115 |
val Deepen_tac : int -> int -> tactic |
1724 | 116 |
|
0 | 117 |
end; |
118 |
||
119 |
||
120 |
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
|
121 |
struct |
|
122 |
||
123 |
local open Data in |
|
124 |
||
1800 | 125 |
(*** Useful tactics for classical reasoning ***) |
0 | 126 |
|
1524 | 127 |
val imp_elim = (*cannot use bind_thm within a structure!*) |
128 |
store_thm ("imp_elim", make_elim mp); |
|
0 | 129 |
|
130 |
(*Solve goal that assumes both P and ~P. *) |
|
131 |
val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; |
|
132 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
133 |
(*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
|
134 |
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
|
135 |
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; |
0 | 136 |
|
137 |
(*Like mp_tac but instantiates no variables*) |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
138 |
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
|
139 |
|
1524 | 140 |
val swap = |
141 |
store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical)); |
|
0 | 142 |
|
143 |
(*Creates rules to eliminate ~A, from rules to introduce A*) |
|
144 |
fun swapify intrs = intrs RLN (2, [swap]); |
|
145 |
||
146 |
(*Uses introduction rules in the normal way, or on negated assumptions, |
|
147 |
trying rules in order. *) |
|
148 |
fun swap_res_tac rls = |
|
54 | 149 |
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls |
150 |
in assume_tac ORELSE' |
|
151 |
contr_tac ORELSE' |
|
152 |
biresolve_tac (foldr addrl (rls,[])) |
|
0 | 153 |
end; |
154 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
155 |
(*Duplication of hazardous rules, for complete provers*) |
2689
6d3d893453de
dup_intr & dup_elim no longer call standard -- this
paulson
parents:
2630
diff
changeset
|
156 |
fun dup_intr th = zero_var_indexes (th RS classical); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
157 |
|
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
158 |
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
|
159 |
rule_by_tactic (TRYALL (etac revcut_rl)); |
0 | 160 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
161 |
|
1800 | 162 |
(**** Classical rule sets ****) |
0 | 163 |
|
164 |
datatype claset = |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
165 |
CS of {safeIs : thm list, (*safe introduction rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
166 |
safeEs : thm list, (*safe elimination rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
167 |
hazIs : thm list, (*unsafe introduction rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
168 |
hazEs : thm list, (*unsafe elimination rules*) |
2630 | 169 |
uwrapper : (int -> tactic) -> |
170 |
(int -> tactic), (*for transforming step_tac*) |
|
171 |
swrapper : (int -> tactic) -> |
|
172 |
(int -> tactic), (*for transform. safe_step_tac*) |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
173 |
safe0_netpair : netpair, (*nets for trivial cases*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
174 |
safep_netpair : netpair, (*nets for >0 subgoals*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
175 |
haz_netpair : netpair, (*nets for unsafe rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
176 |
dup_netpair : netpair}; (*nets for duplication*) |
0 | 177 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
178 |
(*Desired invariants are |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
179 |
safe0_netpair = build safe0_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
180 |
safep_netpair = build safep_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
181 |
haz_netpair = build (joinrules(hazIs, hazEs)), |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
182 |
dup_netpair = build (joinrules(map dup_intr hazIs, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
183 |
map dup_elim hazEs))} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
184 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
185 |
where build = build_netpair(Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
186 |
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
|
187 |
safep_brls contains all brules that generate 1 or more new subgoals. |
1800 | 188 |
The theorem lists are largely comments, though they are used in merge_cs. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
189 |
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
|
190 |
*) |
0 | 191 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
192 |
val empty_cs = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
193 |
CS{safeIs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
194 |
safeEs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
195 |
hazIs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
196 |
hazEs = [], |
2630 | 197 |
uwrapper = I, |
198 |
swrapper = I, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
199 |
safe0_netpair = (Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
200 |
safep_netpair = (Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
201 |
haz_netpair = (Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
202 |
dup_netpair = (Net.empty,Net.empty)}; |
0 | 203 |
|
3546 | 204 |
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) = |
205 |
let val pretty_thms = map Display.pretty_thm in |
|
206 |
Pretty.writeln (Pretty.big_list "introduction rules:" (pretty_thms hazIs)); |
|
207 |
Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs)); |
|
208 |
Pretty.writeln (Pretty.big_list "elimination rules:" (pretty_thms hazEs)); |
|
209 |
Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)) |
|
210 |
end; |
|
0 | 211 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
212 |
fun rep_claset (CS args) = args; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
213 |
|
2630 | 214 |
fun getWrapper (CS{uwrapper,...}) = uwrapper; |
215 |
||
216 |
fun getSWrapper (CS{swrapper,...}) = swrapper; |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
217 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
218 |
|
1800 | 219 |
(*** Adding (un)safe introduction or elimination rules. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
220 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
221 |
In case of overlap, new rules are tried BEFORE old ones!! |
1800 | 222 |
***) |
0 | 223 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
224 |
(*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
|
225 |
assumptions. Pairs elim rules with true. *) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
226 |
fun joinrules (intrs,elims) = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
227 |
(map (pair true) (elims @ swapify intrs) @ |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
228 |
map (pair false) intrs); |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
229 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
230 |
(*Priority: prefer rules with fewest subgoals, |
1231 | 231 |
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
|
232 |
fun tag_brls k [] = [] |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
233 |
| tag_brls k (brl::brls) = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
234 |
(1000000*subgoals_of_brl brl + k, brl) :: |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
235 |
tag_brls (k+1) brls; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
236 |
|
1800 | 237 |
fun insert_tagged_list kbrls netpr = foldr insert_tagged_brl (kbrls, netpr); |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
238 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
239 |
(*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
|
240 |
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
|
241 |
new insertions the lowest priority.*) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
242 |
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
|
243 |
|
1800 | 244 |
fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
245 |
|
1800 | 246 |
val delete = delete_tagged_list o joinrules; |
247 |
||
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
248 |
val mem_thm = gen_mem eq_thm |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
249 |
and rem_thm = gen_rem eq_thm; |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
250 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
251 |
(*Warn if the rule is already present ELSEWHERE in the claset. The addition |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
252 |
is still allowed.*) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
253 |
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
254 |
if mem_thm (th, safeIs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
255 |
warning ("rule already in claset as Safe Intr\n" ^ string_of_thm th) |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
256 |
else if mem_thm (th, safeEs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
257 |
warning ("rule already in claset as Safe Elim\n" ^ string_of_thm th) |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
258 |
else if mem_thm (th, hazIs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
259 |
warning ("rule already in claset as unsafe Intr\n" ^ string_of_thm th) |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
260 |
else if mem_thm (th, hazEs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
261 |
warning ("rule already in claset as unsafe Elim\n" ^ string_of_thm th) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
262 |
else (); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
263 |
|
1800 | 264 |
(*** Safe rules ***) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
265 |
|
2630 | 266 |
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
267 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
268 |
th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
269 |
if mem_thm (th, safeIs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
270 |
(warning ("ignoring duplicate Safe Intr\n" ^ string_of_thm th); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
271 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
272 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
273 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
274 |
partition (fn rl => nprems_of rl=0) [th] |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
275 |
val nI = length safeIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
276 |
and nE = length safeEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
277 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
278 |
CS{safeIs = th::safeIs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
279 |
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
280 |
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
281 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
282 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
283 |
hazEs = hazEs, |
2630 | 284 |
uwrapper = uwrapper, |
285 |
swrapper = swrapper, |
|
286 |
haz_netpair = haz_netpair, |
|
287 |
dup_netpair = dup_netpair} |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
288 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
289 |
|
2630 | 290 |
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
291 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
292 |
th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
293 |
if mem_thm (th, safeEs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
294 |
(warning ("ignoring duplicate Safe Elim\n" ^ string_of_thm th); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
295 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
296 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
297 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
298 |
partition (fn rl => nprems_of rl=1) [th] |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
299 |
val nI = length safeIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
300 |
and nE = length safeEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
301 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
302 |
CS{safeEs = th::safeEs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
303 |
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
304 |
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
305 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
306 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
307 |
hazEs = hazEs, |
2630 | 308 |
uwrapper = uwrapper, |
309 |
swrapper = swrapper, |
|
310 |
haz_netpair = haz_netpair, |
|
311 |
dup_netpair = dup_netpair} |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
312 |
end; |
0 | 313 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
314 |
fun rev_foldl f (e, l) = foldl f (e, rev l); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
315 |
|
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
316 |
val op addSIs = rev_foldl addSI; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
317 |
val op addSEs = rev_foldl addSE; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
318 |
|
0 | 319 |
fun cs addSDs ths = cs addSEs (map make_elim ths); |
320 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
321 |
|
1800 | 322 |
(*** Hazardous (unsafe) rules ***) |
0 | 323 |
|
2630 | 324 |
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
325 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
326 |
th)= |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
327 |
if mem_thm (th, hazIs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
328 |
(warning ("ignoring duplicate unsafe Intr\n" ^ string_of_thm th); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
329 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
330 |
else |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
331 |
let val nI = length hazIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
332 |
and nE = length hazEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
333 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
334 |
CS{hazIs = th::hazIs, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
335 |
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
336 |
dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
337 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
338 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
339 |
hazEs = hazEs, |
2630 | 340 |
uwrapper = uwrapper, |
341 |
swrapper = swrapper, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
342 |
safe0_netpair = safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
343 |
safep_netpair = safep_netpair} |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
344 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
345 |
|
2630 | 346 |
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
347 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
348 |
th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
349 |
if mem_thm (th, hazEs) then |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
350 |
(warning ("ignoring duplicate unsafe Elim\n" ^ string_of_thm th); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
351 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
352 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
353 |
let val nI = length hazIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
354 |
and nE = length hazEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
355 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
356 |
CS{hazEs = th::hazEs, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
357 |
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
358 |
dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
359 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
360 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
361 |
hazIs = hazIs, |
2630 | 362 |
uwrapper = uwrapper, |
363 |
swrapper = swrapper, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
364 |
safe0_netpair = safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
365 |
safep_netpair = safep_netpair} |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
366 |
end; |
0 | 367 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
368 |
val op addIs = rev_foldl addI; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
369 |
val op addEs = rev_foldl addE; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
370 |
|
0 | 371 |
fun cs addDs ths = cs addEs (map make_elim ths); |
372 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
373 |
|
1800 | 374 |
(*** Deletion of rules |
375 |
Working out what to delete, requires repeating much of the code used |
|
376 |
to insert. |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
377 |
Separate functions delSI, etc., are not exported; instead delrules |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
378 |
searches in all the lists and chooses the relevant delXX functions. |
1800 | 379 |
***) |
380 |
||
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
381 |
fun delSI th |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
382 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
383 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
384 |
if mem_thm (th, safeIs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
385 |
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
386 |
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
387 |
safep_netpair = delete (safep_rls, []) safep_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
388 |
safeIs = rem_thm (safeIs,th), |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
389 |
safeEs = safeEs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
390 |
hazIs = hazIs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
391 |
hazEs = hazEs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
392 |
uwrapper = uwrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
393 |
swrapper = swrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
394 |
haz_netpair = haz_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
395 |
dup_netpair = dup_netpair} |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
396 |
end |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
397 |
else cs; |
1800 | 398 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
399 |
fun delSE th |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
400 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
401 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
402 |
if mem_thm (th, safeEs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
403 |
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
404 |
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
405 |
safep_netpair = delete ([], safep_rls) safep_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
406 |
safeIs = safeIs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
407 |
safeEs = rem_thm (safeEs,th), |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
408 |
hazIs = hazIs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
409 |
hazEs = hazEs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
410 |
uwrapper = uwrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
411 |
swrapper = swrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
412 |
haz_netpair = haz_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
413 |
dup_netpair = dup_netpair} |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
414 |
end |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
415 |
else cs; |
1800 | 416 |
|
417 |
||
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
418 |
fun delI th |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
419 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
420 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
421 |
if mem_thm (th, hazIs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
422 |
CS{haz_netpair = delete ([th], []) haz_netpair, |
1800 | 423 |
dup_netpair = delete ([dup_intr th], []) dup_netpair, |
424 |
safeIs = safeIs, |
|
425 |
safeEs = safeEs, |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
426 |
hazIs = rem_thm (hazIs,th), |
1800 | 427 |
hazEs = hazEs, |
2630 | 428 |
uwrapper = uwrapper, |
429 |
swrapper = swrapper, |
|
1800 | 430 |
safe0_netpair = safe0_netpair, |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
431 |
safep_netpair = safep_netpair} |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
432 |
else cs; |
1800 | 433 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
434 |
fun delE th |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
435 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
436 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
437 |
if mem_thm (th, hazEs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
438 |
CS{haz_netpair = delete ([], [th]) haz_netpair, |
1800 | 439 |
dup_netpair = delete ([], [dup_elim th]) dup_netpair, |
440 |
safeIs = safeIs, |
|
441 |
safeEs = safeEs, |
|
442 |
hazIs = hazIs, |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
443 |
hazEs = rem_thm (hazEs,th), |
2630 | 444 |
uwrapper = uwrapper, |
445 |
swrapper = swrapper, |
|
1800 | 446 |
safe0_netpair = safe0_netpair, |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
447 |
safep_netpair = safep_netpair} |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
448 |
else cs; |
1800 | 449 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
450 |
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) |
1800 | 451 |
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
452 |
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
453 |
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
454 |
then delSI th (delSE th (delI th (delE th cs))) |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
455 |
else (warning ("rule not in claset\n" ^ (string_of_thm th)); |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
456 |
cs); |
1800 | 457 |
|
458 |
val op delrules = foldl delrule; |
|
459 |
||
460 |
||
2630 | 461 |
(*** Setting or modifying the wrapper tacticals ***) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
462 |
|
2630 | 463 |
(*Set a new uwrapper*) |
464 |
fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
465 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) |
2630 | 466 |
setWrapper new_uwrapper = |
467 |
CS{safeIs = safeIs, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
468 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
469 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
470 |
hazEs = hazEs, |
2630 | 471 |
uwrapper = new_uwrapper, |
472 |
swrapper = swrapper, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
473 |
safe0_netpair = safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
474 |
safep_netpair = safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
475 |
haz_netpair = haz_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
476 |
dup_netpair = dup_netpair}; |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
477 |
|
2630 | 478 |
(*Set a new swrapper*) |
479 |
fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, |
|
480 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) |
|
481 |
setSWrapper new_swrapper = |
|
482 |
CS{safeIs = safeIs, |
|
483 |
safeEs = safeEs, |
|
484 |
hazIs = hazIs, |
|
485 |
hazEs = hazEs, |
|
486 |
uwrapper = uwrapper, |
|
487 |
swrapper = new_swrapper, |
|
488 |
safe0_netpair = safe0_netpair, |
|
489 |
safep_netpair = safep_netpair, |
|
490 |
haz_netpair = haz_netpair, |
|
491 |
dup_netpair = dup_netpair}; |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
492 |
|
2630 | 493 |
(*Compose a tactical with the existing uwrapper*) |
494 |
fun cs compWrapper uwrapper' = cs setWrapper (uwrapper' o getWrapper cs); |
|
495 |
||
496 |
(*Compose a tactical with the existing swrapper*) |
|
497 |
fun cs compSWrapper swrapper' = cs setSWrapper (swrapper' o getSWrapper cs); |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
498 |
|
2630 | 499 |
(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) |
500 |
fun cs addSbefore tac1 = cs compSWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); |
|
501 |
fun cs addSaltern tac2 = cs compSWrapper (fn tac1 => tac1 ORELSE' tac2); |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
502 |
|
2630 | 503 |
(*compose a tactic sequentially before/alternatively after the step tactic*) |
504 |
fun cs addbefore tac1 = cs compWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); |
|
505 |
fun cs addaltern tac2 = cs compWrapper (fn tac1 => tac1 APPEND' tac2); |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
506 |
|
1711 | 507 |
(*Merge works by adding all new rules of the 2nd claset into the 1st claset. |
508 |
Merging the term nets may look more efficient, but the rather delicate |
|
509 |
treatment of priority might get muddled up.*) |
|
510 |
fun merge_cs |
|
2630 | 511 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, |
1711 | 512 |
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) = |
513 |
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) |
|
514 |
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) |
|
2630 | 515 |
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) |
516 |
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) |
|
1711 | 517 |
in cs addSIs safeIs' |
518 |
addSEs safeEs' |
|
519 |
addIs hazIs' |
|
520 |
addEs hazEs' |
|
521 |
end; |
|
522 |
||
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
523 |
|
1800 | 524 |
(**** Simple tactics for theorem proving ****) |
0 | 525 |
|
526 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
2630 | 527 |
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
528 |
getSWrapper cs (FIRST' [ |
|
529 |
eq_assume_tac, |
|
530 |
eq_mp_tac, |
|
531 |
bimatch_from_nets_tac safe0_netpair, |
|
532 |
FIRST' hyp_subst_tacs, |
|
533 |
bimatch_from_nets_tac safep_netpair]); |
|
0 | 534 |
|
535 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
|
2630 | 536 |
fun safe_tac cs = REPEAT_DETERM_FIRST |
537 |
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
538 |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
539 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
540 |
(*** Clarify_tac: do safe steps without causing branching ***) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
541 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
542 |
fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
543 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
544 |
(*version of bimatch_from_nets_tac that only applies rules that |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
545 |
create precisely n subgoals.*) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
546 |
fun n_bimatch_from_nets_tac n = |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
547 |
biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
548 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
549 |
fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
550 |
val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
551 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
552 |
(*Two-way branching is allowed only if one of the branches immediately closes*) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
553 |
fun bimatch2_tac netpair i = |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
554 |
n_bimatch_from_nets_tac 2 netpair i THEN |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
555 |
(eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1)); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
556 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
557 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
558 |
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
559 |
getSWrapper cs (FIRST' [ |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
560 |
eq_assume_contr_tac, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
561 |
bimatch_from_nets_tac safe0_netpair, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
562 |
FIRST' hyp_subst_tacs, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
563 |
n_bimatch_from_nets_tac 1 safep_netpair, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
564 |
bimatch2_tac safep_netpair]); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
565 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
566 |
fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
567 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
568 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
569 |
(*** Unsafe steps instantiate variables or lose information ***) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
570 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
571 |
(*But these unsafe steps at least solve a subgoal!*) |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
572 |
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
573 |
assume_tac APPEND' |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
574 |
contr_tac APPEND' |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
575 |
biresolve_from_nets_tac safe0_netpair; |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
576 |
|
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
577 |
(*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
|
578 |
fun instp_step_tac (CS{safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
579 |
biresolve_from_nets_tac safep_netpair; |
0 | 580 |
|
581 |
(*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
|
582 |
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; |
0 | 583 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
584 |
fun haz_step_tac (CS{haz_netpair,...}) = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
585 |
biresolve_from_nets_tac haz_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
586 |
|
0 | 587 |
(*Single step for the prover. FAILS unless it makes progress. *) |
2630 | 588 |
fun step_tac cs i = getWrapper cs |
589 |
(K (safe_tac cs) ORELSE' (inst_step_tac cs ORELSE' haz_step_tac cs)) i; |
|
0 | 590 |
|
591 |
(*Using a "safe" rule to instantiate variables is unsafe. This tactic |
|
592 |
allows backtracking from "safe" rules to "unsafe" rules here.*) |
|
2630 | 593 |
fun slow_step_tac cs i = getWrapper cs |
594 |
(K (safe_tac cs) ORELSE' (inst_step_tac cs APPEND' haz_step_tac cs)) i; |
|
0 | 595 |
|
1800 | 596 |
(**** The following tactics all fail unless they solve one goal ****) |
0 | 597 |
|
598 |
(*Dumb but fast*) |
|
599 |
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
|
600 |
||
601 |
(*Slower but smarter than fast_tac*) |
|
602 |
fun best_tac cs = |
|
603 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); |
|
604 |
||
605 |
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
|
606 |
||
607 |
fun slow_best_tac cs = |
|
608 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
|
609 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
610 |
|
1800 | 611 |
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
612 |
val weight_ASTAR = ref 5; |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
613 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
614 |
fun astar_tac cs = |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
615 |
SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
616 |
, 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
|
617 |
(step_tac cs 1)); |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
618 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
619 |
fun slow_astar_tac cs = |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
620 |
SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
621 |
, 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
|
622 |
(slow_step_tac cs 1)); |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
623 |
|
1800 | 624 |
(**** 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
|
625 |
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
|
626 |
easy theorems faster, but loses completeness -- and many of the harder |
1800 | 627 |
theorems such as 43. ****) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
628 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
629 |
(*Non-deterministic! Could always expand the first unsafe connective. |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
630 |
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
|
631 |
greater search depth required.*) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
632 |
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
|
633 |
biresolve_from_nets_tac dup_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
634 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
635 |
(*Searching to depth m.*) |
3537 | 636 |
fun depth_tac cs m i state = |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
637 |
SELECT_GOAL |
2630 | 638 |
(getWrapper cs |
3204
c1653e2e146d
corrected depth_tac: no call for safe_step_tac if subgoal not present
oheimb
parents:
2868
diff
changeset
|
639 |
(fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac |
c1653e2e146d
corrected depth_tac: no call for safe_step_tac if subgoal not present
oheimb
parents:
2868
diff
changeset
|
640 |
(safe_step_tac cs i)) THEN_ELSE |
2630 | 641 |
(DEPTH_SOLVE (depth_tac cs m i), |
642 |
inst0_step_tac cs i APPEND |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
643 |
COND (K(m=0)) no_tac |
2630 | 644 |
((instp_step_tac cs i APPEND dup_step_tac cs i) |
645 |
THEN DEPTH_SOLVE (depth_tac cs (m-1) i)))) 1) |
|
3537 | 646 |
i state; |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
647 |
|
2173 | 648 |
(*Search, with depth bound m. |
649 |
This is the "entry point", which does safe inferences first.*) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
650 |
fun safe_depth_tac cs m = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
651 |
SUBGOAL |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
652 |
(fn (prem,i) => |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
653 |
let val deti = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
654 |
(*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
|
655 |
case term_vars prem of |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
656 |
[] => DETERM |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
657 |
| _::_ => I |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
658 |
in SELECT_GOAL (TRY (safe_tac cs) THEN |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
659 |
DEPTH_SOLVE (deti (depth_tac cs m 1))) i |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
660 |
end); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
661 |
|
2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
662 |
fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
663 |
|
1724 | 664 |
val claset = ref empty_cs; |
665 |
||
666 |
fun AddDs ts = (claset := !claset addDs ts); |
|
667 |
||
668 |
fun AddEs ts = (claset := !claset addEs ts); |
|
669 |
||
670 |
fun AddIs ts = (claset := !claset addIs ts); |
|
671 |
||
672 |
fun AddSDs ts = (claset := !claset addSDs ts); |
|
673 |
||
674 |
fun AddSEs ts = (claset := !claset addSEs ts); |
|
675 |
||
676 |
fun AddSIs ts = (claset := !claset addSIs ts); |
|
677 |
||
1807 | 678 |
fun Delrules ts = (claset := !claset delrules ts); |
679 |
||
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
680 |
(** The abstraction over the proof state delays the dereferencing **) |
1800 | 681 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
682 |
fun Safe_tac st = safe_tac (!claset) st; |
1814 | 683 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
684 |
fun Safe_step_tac i st = safe_step_tac (!claset) i st; |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
685 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
686 |
fun Clarify_step_tac i st = clarify_step_tac (!claset) i st; |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
687 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
688 |
fun Clarify_tac i st = clarify_tac (!claset) i st; |
1800 | 689 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
690 |
fun Step_tac i st = step_tac (!claset) i st; |
1724 | 691 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
692 |
fun Fast_tac i st = fast_tac (!claset) i st; |
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
693 |
|
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
694 |
fun Best_tac i st = best_tac (!claset) i st; |
1800 | 695 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
696 |
fun Slow_tac i st = slow_tac (!claset) i st; |
2066 | 697 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
698 |
fun Slow_best_tac i st = slow_best_tac (!claset) i st; |
2066 | 699 |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
700 |
fun Deepen_tac m = deepen_tac (!claset) m; |
1800 | 701 |
|
0 | 702 |
end; |
703 |
end; |
|
2630 | 704 |
|
705 |