author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 10185  c452fea3ce74 
child 10309  a7f961fb62c6 
permissions  rwrr 
9938  1 
(* Title: Provers/classical.ML 
0  2 
ID: $Id$ 
9938  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Theorem prover for classical reasoning, including predicate calculus, set 

7 
theory, etc. 

8 

9563
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

9 
Rules must be classified as intro, elim, safe, hazardous (unsafe). 
0  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 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

17 
(*higher precedence than := facilitates use of references*) 
10034  18 
infix 4 addSIs addSEs addSDs addIs addEs addDs addXIs addXEs addXDs delrules 
4651  19 
addSWrapper delSWrapper addWrapper delWrapper 
5523  20 
addSbefore addSaltern addbefore addaltern 
21 
addD2 addE2 addSD2 addSE2; 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

22 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

23 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

24 
(*should be a type abbreviation in signature CLASSICAL*) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

25 
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; 
4651  26 
type wrapper = (int > tactic) > (int > tactic); 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

27 

0  28 
signature CLASSICAL_DATA = 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

29 
sig 
9171  30 
val make_elim : thm > thm (* Tactic.make_elim or a classical version*) 
9938  31 
val mp : thm (* [ P>Q; P ] ==> Q *) 
32 
val not_elim : thm (* [ ~P; P ] ==> R *) 

33 
val classical : thm (* (~P ==> P) ==> P *) 

34 
val sizef : thm > int (* size function for BEST_FIRST *) 

0  35 
val hyp_subst_tacs: (int > tactic) list 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

36 
end; 
0  37 

5841  38 
signature BASIC_CLASSICAL = 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

39 
sig 
0  40 
type claset 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

41 
val empty_cs: claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

42 
val print_cs: claset > unit 
4380  43 
val print_claset: theory > unit 
4653  44 
val rep_cs: (* BLAST_DATA in blast.ML dependent on this *) 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

45 
claset > {safeIs: thm list, safeEs: thm list, 
9938  46 
hazIs: thm list, hazEs: thm list, 
47 
xtraIs: thm list, xtraEs: thm list, 

48 
swrappers: (string * wrapper) list, 

49 
uwrappers: (string * wrapper) list, 

50 
safe0_netpair: netpair, safep_netpair: netpair, 

51 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} 

52 
val merge_cs : claset * claset > claset 

53 
val addDs : claset * thm list > claset 

54 
val addEs : claset * thm list > claset 

55 
val addIs : claset * thm list > claset 

56 
val addSDs : claset * thm list > claset 

57 
val addSEs : claset * thm list > claset 

58 
val addSIs : claset * thm list > claset 

10034  59 
val addXDs : claset * thm list > claset 
60 
val addXEs : claset * thm list > claset 

61 
val addXIs : claset * thm list > claset 

9938  62 
val delrules : claset * thm list > claset 
63 
val addSWrapper : claset * (string * wrapper) > claset 

64 
val delSWrapper : claset * string > claset 

65 
val addWrapper : claset * (string * wrapper) > claset 

66 
val delWrapper : claset * string > claset 

67 
val addSbefore : claset * (string * (int > tactic)) > claset 

68 
val addSaltern : claset * (string * (int > tactic)) > claset 

69 
val addbefore : claset * (string * (int > tactic)) > claset 

70 
val addaltern : claset * (string * (int > tactic)) > claset 

5523  71 
val addD2 : claset * (string * thm) > claset 
72 
val addE2 : claset * (string * thm) > claset 

73 
val addSD2 : claset * (string * thm) > claset 

74 
val addSE2 : claset * (string * thm) > claset 

9938  75 
val appSWrappers : claset > wrapper 
76 
val appWrappers : claset > wrapper 

77 
val trace_rules : bool ref 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

78 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

79 
val claset_ref_of_sg: Sign.sg > claset ref 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

80 
val claset_ref_of: theory > claset ref 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

81 
val claset_of_sg: Sign.sg > claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

82 
val claset_of: theory > claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

83 
val CLASET: (claset > tactic) > tactic 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

84 
val CLASET': (claset > 'a > tactic) > 'a > tactic 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

85 
val claset: unit > claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

86 
val claset_ref: unit > claset ref 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

87 

9938  88 
val fast_tac : claset > int > tactic 
89 
val slow_tac : claset > int > tactic 

90 
val weight_ASTAR : int ref 

91 
val astar_tac : claset > int > tactic 

92 
val slow_astar_tac : claset > int > tactic 

93 
val best_tac : claset > int > tactic 

94 
val first_best_tac : claset > int > tactic 

95 
val slow_best_tac : claset > int > tactic 

96 
val depth_tac : claset > int > int > tactic 

97 
val deepen_tac : claset > int > int > tactic 

1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

98 

9938  99 
val contr_tac : int > tactic 
100 
val dup_elim : thm > thm 

101 
val dup_intr : thm > thm 

102 
val dup_step_tac : claset > int > tactic 

103 
val eq_mp_tac : int > tactic 

104 
val haz_step_tac : claset > int > tactic 

105 
val joinrules : thm list * thm list > (bool * thm) list 

106 
val mp_tac : int > tactic 

107 
val safe_tac : claset > tactic 

108 
val safe_steps_tac : claset > int > tactic 

109 
val safe_step_tac : claset > int > tactic 

110 
val clarify_tac : claset > int > tactic 

111 
val clarify_step_tac : claset > int > tactic 

112 
val step_tac : claset > int > tactic 

113 
val slow_step_tac : claset > int > tactic 

114 
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) 

115 
val swapify : thm list > thm list 

116 
val swap_res_tac : thm list > int > tactic 

117 
val inst_step_tac : claset > int > tactic 

118 
val inst0_step_tac : claset > int > tactic 

119 
val instp_step_tac : claset > int > tactic 

1724  120 

9938  121 
val AddDs : thm list > unit 
122 
val AddEs : thm list > unit 

123 
val AddIs : thm list > unit 

124 
val AddSDs : thm list > unit 

125 
val AddSEs : thm list > unit 

126 
val AddSIs : thm list > unit 

127 
val AddXDs : thm list > unit 

128 
val AddXEs : thm list > unit 

129 
val AddXIs : thm list > unit 

130 
val Delrules : thm list > unit 

131 
val Safe_tac : tactic 

132 
val Safe_step_tac : int > tactic 

133 
val Clarify_tac : int > tactic 

134 
val Clarify_step_tac : int > tactic 

135 
val Step_tac : int > tactic 

136 
val Fast_tac : int > tactic 

137 
val Best_tac : int > tactic 

138 
val Slow_tac : int > tactic 

2066  139 
val Slow_best_tac : int > tactic 
9938  140 
val Deepen_tac : int > int > tactic 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

141 
end; 
1724  142 

5841  143 
signature CLASSICAL = 
144 
sig 

145 
include BASIC_CLASSICAL 

146 
val print_local_claset: Proof.context > unit 

147 
val get_local_claset: Proof.context > claset 

148 
val put_local_claset: claset > Proof.context > Proof.context 

149 
val safe_dest_global: theory attribute 

150 
val safe_elim_global: theory attribute 

151 
val safe_intro_global: theory attribute 

6955  152 
val haz_dest_global: theory attribute 
153 
val haz_elim_global: theory attribute 

154 
val haz_intro_global: theory attribute 

155 
val xtra_dest_global: theory attribute 

156 
val xtra_elim_global: theory attribute 

157 
val xtra_intro_global: theory attribute 

9938  158 
val rule_del_global: theory attribute 
6955  159 
val safe_dest_local: Proof.context attribute 
160 
val safe_elim_local: Proof.context attribute 

161 
val safe_intro_local: Proof.context attribute 

5885  162 
val haz_dest_local: Proof.context attribute 
163 
val haz_elim_local: Proof.context attribute 

164 
val haz_intro_local: Proof.context attribute 

6955  165 
val xtra_dest_local: Proof.context attribute 
166 
val xtra_elim_local: Proof.context attribute 

167 
val xtra_intro_local: Proof.context attribute 

9938  168 
val rule_del_local: Proof.context attribute 
7272  169 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  170 
val cla_meth: (claset > tactic) > thm list > Proof.context > Proof.method 
171 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 

5927  172 
val cla_method: (claset > tactic) > Args.src > Proof.context > Proof.method 
173 
val cla_method': (claset > int > tactic) > Args.src > Proof.context > Proof.method 

5841  174 
val setup: (theory > theory) list 
175 
end; 

176 

0  177 

5927  178 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  179 
struct 
180 

7354  181 
local open Data in 
0  182 

1800  183 
(*** Useful tactics for classical reasoning ***) 
0  184 

1524  185 
val imp_elim = (*cannot use bind_thm within a structure!*) 
9938  186 
store_thm ("imp_elim", Data.make_elim mp); 
0  187 

4392  188 
(*Prove goal that assumes both P and ~P. 
189 
No backtracking if it finds an equal assumption. Perhaps should call 

190 
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) 

191 
val contr_tac = eresolve_tac [not_elim] THEN' 

192 
(eq_assume_tac ORELSE' assume_tac); 

0  193 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

194 
(*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

195 
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

196 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  197 

198 
(*Like mp_tac but instantiates no variables*) 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

199 
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

200 

1524  201 
val swap = 
202 
store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical)); 

0  203 

204 
(*Creates rules to eliminate ~A, from rules to introduce A*) 

205 
fun swapify intrs = intrs RLN (2, [swap]); 

206 

207 
(*Uses introduction rules in the normal way, or on negated assumptions, 

208 
trying rules in order. *) 

209 
fun swap_res_tac rls = 

54  210 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
9938  211 
in assume_tac ORELSE' 
212 
contr_tac ORELSE' 

54  213 
biresolve_tac (foldr addrl (rls,[])) 
0  214 
end; 
215 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

216 
(*Duplication of hazardous rules, for complete provers*) 
2689
6d3d893453de
dup_intr & dup_elim no longer call standard  this
paulson
parents:
2630
diff
changeset

217 
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

218 

6967  219 
fun dup_elim th = 
220 
(case try 

221 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

222 
(th RSN (2, revcut_rl) > assumption 2 > Seq.hd) of 

223 
Some th' => th' 

224 
 _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); 

0  225 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

226 

1800  227 
(**** Classical rule sets ****) 
0  228 

229 
datatype claset = 

9938  230 
CS of {safeIs : thm list, (*safe introduction rules*) 
231 
safeEs : thm list, (*safe elimination rules*) 

232 
hazIs : thm list, (*unsafe introduction rules*) 

233 
hazEs : thm list, (*unsafe elimination rules*) 

234 
xtraIs : thm list, (*extra introduction rules*) 

235 
xtraEs : thm list, (*extra elimination rules*) 

236 
swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) 

237 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 

238 
safe0_netpair : netpair, (*nets for trivial cases*) 

239 
safep_netpair : netpair, (*nets for >0 subgoals*) 

240 
haz_netpair : netpair, (*nets for unsafe rules*) 

241 
dup_netpair : netpair, (*nets for duplication*) 

242 
xtra_netpair : netpair}; (*nets for extra rules*) 

0  243 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

244 
(*Desired invariants are 
9938  245 
safe0_netpair = build safe0_brls, 
246 
safep_netpair = build safep_brls, 

247 
haz_netpair = build (joinrules(hazIs, hazEs)), 

248 
dup_netpair = build (joinrules(map dup_intr hazIs, 

249 
map dup_elim hazEs)), 

250 
xtra_netpair = build (joinrules(xtraIs, xtraEs))} 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

251 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

252 
where build = build_netpair(Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

253 
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

254 
safep_brls contains all brules that generate 1 or more new subgoals. 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

255 
The theorem lists are largely comments, though they are used in merge_cs and print_cs. 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

256 
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

257 
*) 
0  258 

6502  259 
val empty_netpair = (Net.empty, Net.empty); 
260 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

261 
val empty_cs = 
9938  262 
CS{safeIs = [], 
263 
safeEs = [], 

264 
hazIs = [], 

265 
hazEs = [], 

266 
xtraIs = [], 

267 
xtraEs = [], 

4651  268 
swrappers = [], 
269 
uwrappers = [], 

6502  270 
safe0_netpair = empty_netpair, 
271 
safep_netpair = empty_netpair, 

272 
haz_netpair = empty_netpair, 

6955  273 
dup_netpair = empty_netpair, 
274 
xtra_netpair = empty_netpair}; 

0  275 

6955  276 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
3546  277 
let val pretty_thms = map Display.pretty_thm in 
9760  278 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 
279 
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), 

280 
Pretty.big_list "extra introduction rules (intro?):" (pretty_thms xtraIs), 

281 
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), 

282 
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), 

283 
Pretty.big_list "extra elimination rules (elim?):" (pretty_thms xtraEs)] 

8727  284 
> Pretty.chunks > Pretty.writeln 
3546  285 
end; 
0  286 

4653  287 
fun rep_cs (CS args) = args; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

288 

4651  289 
local 
290 
fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac); 

291 
in 

292 
fun appSWrappers (CS{swrappers,...}) = calc_wrap swrappers; 

293 
fun appWrappers (CS{uwrappers,...}) = calc_wrap uwrappers; 

294 
end; 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

295 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

296 

1800  297 
(*** Adding (un)safe introduction or elimination rules. 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

298 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

299 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  300 
***) 
0  301 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

302 
(*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

303 
assumptions. Pairs elim rules with true. *) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

304 
fun joinrules (intrs,elims) = 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

305 
(map (pair true) (elims @ swapify intrs) @ 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

306 
map (pair false) intrs); 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

307 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

308 
(*Priority: prefer rules with fewest subgoals, 
1231  309 
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

310 
fun tag_brls k [] = [] 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

311 
 tag_brls k (brl::brls) = 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

312 
(1000000*subgoals_of_brl brl + k, brl) :: 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

313 
tag_brls (k+1) brls; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

314 

1800  315 
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

316 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

317 
(*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

318 
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

319 
new insertions the lowest priority.*) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

320 
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

321 

1800  322 
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

323 

1800  324 
val delete = delete_tagged_list o joinrules; 
325 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

326 
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

327 
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

328 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

329 
(*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

330 
is still allowed.*) 
6955  331 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

332 
if mem_thm (th, safeIs) then 
9938  333 
warning ("Rule already declared as safe introduction (intro!)\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

334 
else if mem_thm (th, safeEs) then 
9408  335 
warning ("Rule already declared as safe elimination (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

336 
else if mem_thm (th, hazIs) then 
9760  337 
warning ("Rule already declared as introduction (intro)\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

338 
else if mem_thm (th, hazEs) then 
9760  339 
warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th) 
6955  340 
else if mem_thm (th, xtraIs) then 
9408  341 
warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th) 
6955  342 
else if mem_thm (th, xtraEs) then 
9408  343 
warning ("Rule already declared as extra elimination (elim?)\n" ^ string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

344 
else (); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

345 

1800  346 
(*** Safe rules ***) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

347 

6955  348 
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  349 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
350 
th) = 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

351 
if mem_thm (th, safeIs) then 
9938  352 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); 
353 
cs) 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

354 
else 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

355 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
7559  356 
partition Thm.no_prems [th] 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

357 
val nI = length safeIs + 1 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

358 
and nE = length safeEs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

359 
in warn_dup th cs; 
9938  360 
CS{safeIs = th::safeIs, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

361 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  362 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
363 
safeEs = safeEs, 

364 
hazIs = hazIs, 

365 
hazEs = hazEs, 

366 
xtraIs = xtraIs, 

367 
xtraEs = xtraEs, 

368 
swrappers = swrappers, 

369 
uwrappers = uwrappers, 

370 
haz_netpair = haz_netpair, 

371 
dup_netpair = dup_netpair, 

372 
xtra_netpair = xtra_netpair} 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

373 
end; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

374 

6955  375 
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  376 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
377 
th) = 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

378 
if mem_thm (th, safeEs) then 
9938  379 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); 
380 
cs) 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

381 
else 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

382 
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

383 
partition (fn rl => nprems_of rl=1) [th] 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

384 
val nI = length safeIs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

385 
and nE = length safeEs + 1 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

386 
in warn_dup th cs; 
9938  387 
CS{safeEs = th::safeEs, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

388 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  389 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
390 
safeIs = safeIs, 

391 
hazIs = hazIs, 

392 
hazEs = hazEs, 

393 
xtraIs = xtraIs, 

394 
xtraEs = xtraEs, 

395 
swrappers = swrappers, 

396 
uwrappers = uwrappers, 

397 
haz_netpair = haz_netpair, 

398 
dup_netpair = dup_netpair, 

399 
xtra_netpair = xtra_netpair} 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

400 
end; 
0  401 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

402 
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

403 

6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

404 
val op addSIs = rev_foldl addSI; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

405 
val op addSEs = rev_foldl addSE; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

406 

9938  407 
fun cs addSDs ths = cs addSEs (map Data.make_elim ths); 
0  408 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

409 

1800  410 
(*** Hazardous (unsafe) rules ***) 
0  411 

6955  412 
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  413 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
414 
th)= 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

415 
if mem_thm (th, hazIs) then 
9938  416 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
417 
cs) 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

418 
else 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

419 
let val nI = length hazIs + 1 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

420 
and nE = length hazEs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

421 
in warn_dup th cs; 
9938  422 
CS{hazIs = th::hazIs, 
423 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 

424 
dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, 

425 
safeIs = safeIs, 

426 
safeEs = safeEs, 

427 
hazEs = hazEs, 

428 
xtraIs = xtraIs, 

429 
xtraEs = xtraEs, 

430 
swrappers = swrappers, 

431 
uwrappers = uwrappers, 

432 
safe0_netpair = safe0_netpair, 

433 
safep_netpair = safep_netpair, 

434 
xtra_netpair = xtra_netpair} 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

435 
end; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

436 

6955  437 
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  438 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
439 
th) = 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

440 
if mem_thm (th, hazEs) then 
9938  441 
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); 
442 
cs) 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

443 
else 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

444 
let val nI = length hazIs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

445 
and nE = length hazEs + 1 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

446 
in warn_dup th cs; 
9938  447 
CS{hazEs = th::hazEs, 
448 
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, 

449 
dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, 

450 
safeIs = safeIs, 

451 
safeEs = safeEs, 

452 
hazIs = hazIs, 

453 
xtraIs = xtraIs, 

454 
xtraEs = xtraEs, 

455 
swrappers = swrappers, 

456 
uwrappers = uwrappers, 

457 
safe0_netpair = safe0_netpair, 

458 
safep_netpair = safep_netpair, 

459 
xtra_netpair = xtra_netpair} 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

460 
end; 
0  461 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

462 
val op addIs = rev_foldl addI; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

463 
val op addEs = rev_foldl addE; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

464 

9938  465 
fun cs addDs ths = cs addEs (map Data.make_elim ths); 
0  466 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

467 

6955  468 
(*** Extra (single step) rules ***) 
469 

470 
fun addXI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

9938  471 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
472 
th)= 

6955  473 
if mem_thm (th, xtraIs) then 
9938  474 
(warning ("Ignoring duplicate extra introduction (intro?)\n" ^ string_of_thm th); 
475 
cs) 

6955  476 
else 
477 
let val nI = length xtraIs + 1 

478 
and nE = length xtraEs 

479 
in warn_dup th cs; 

9938  480 
CS{xtraIs = th::xtraIs, 
481 
xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair, 

482 
safeIs = safeIs, 

483 
safeEs = safeEs, 

484 
hazIs = hazIs, 

485 
hazEs = hazEs, 

486 
xtraEs = xtraEs, 

487 
swrappers = swrappers, 

488 
uwrappers = uwrappers, 

489 
safe0_netpair = safe0_netpair, 

490 
safep_netpair = safep_netpair, 

491 
haz_netpair = haz_netpair, 

492 
dup_netpair = dup_netpair} 

6955  493 
end; 
494 

495 
fun addXE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

9938  496 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
497 
th) = 

6955  498 
if mem_thm (th, xtraEs) then 
9938  499 
(warning ("Ignoring duplicate extra elimination (elim?)\n" ^ string_of_thm th); 
500 
cs) 

6955  501 
else 
502 
let val nI = length xtraIs 

503 
and nE = length xtraEs + 1 

504 
in warn_dup th cs; 

9938  505 
CS{xtraEs = th::xtraEs, 
506 
xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair, 

507 
safeIs = safeIs, 

508 
safeEs = safeEs, 

509 
hazIs = hazIs, 

510 
hazEs = hazEs, 

511 
xtraIs = xtraIs, 

512 
swrappers = swrappers, 

513 
uwrappers = uwrappers, 

514 
safe0_netpair = safe0_netpair, 

515 
safep_netpair = safep_netpair, 

516 
haz_netpair = haz_netpair, 

517 
dup_netpair = dup_netpair} 

6955  518 
end; 
519 

520 
val op addXIs = rev_foldl addXI; 

521 
val op addXEs = rev_foldl addXE; 

522 

9938  523 
fun cs addXDs ths = cs addXEs (map Data.make_elim ths); 
6955  524 

525 

1800  526 
(*** Deletion of rules 
527 
Working out what to delete, requires repeating much of the code used 

9938  528 
to insert. 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

529 
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

530 
searches in all the lists and chooses the relevant delXX functions. 
1800  531 
***) 
532 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

533 
fun delSI th 
6955  534 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  535 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

536 
if mem_thm (th, safeIs) then 
7559  537 
let val (safe0_rls, safep_rls) = partition Thm.no_prems [th] 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

538 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  539 
safep_netpair = delete (safep_rls, []) safep_netpair, 
540 
safeIs = rem_thm (safeIs,th), 

541 
safeEs = safeEs, 

542 
hazIs = hazIs, 

543 
hazEs = hazEs, 

544 
xtraIs = xtraIs, 

545 
xtraEs = xtraEs, 

546 
swrappers = swrappers, 

547 
uwrappers = uwrappers, 

548 
haz_netpair = haz_netpair, 

549 
dup_netpair = dup_netpair, 

550 
xtra_netpair = xtra_netpair} 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

551 
end 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

552 
else cs; 
1800  553 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

554 
fun delSE th 
6955  555 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  556 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

557 
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

558 
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

559 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  560 
safep_netpair = delete ([], safep_rls) safep_netpair, 
561 
safeIs = safeIs, 

562 
safeEs = rem_thm (safeEs,th), 

563 
hazIs = hazIs, 

564 
hazEs = hazEs, 

565 
xtraIs = xtraIs, 

566 
xtraEs = xtraEs, 

567 
swrappers = swrappers, 

568 
uwrappers = uwrappers, 

569 
haz_netpair = haz_netpair, 

570 
dup_netpair = dup_netpair, 

571 
xtra_netpair = xtra_netpair} 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

572 
end 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

573 
else cs; 
1800  574 

575 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

576 
fun delI th 
6955  577 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  578 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

579 
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

580 
CS{haz_netpair = delete ([th], []) haz_netpair, 
9938  581 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
582 
safeIs = safeIs, 

583 
safeEs = safeEs, 

584 
hazIs = rem_thm (hazIs,th), 

585 
hazEs = hazEs, 

586 
xtraIs = xtraIs, 

587 
xtraEs = xtraEs, 

588 
swrappers = swrappers, 

589 
uwrappers = uwrappers, 

590 
safe0_netpair = safe0_netpair, 

591 
safep_netpair = safep_netpair, 

592 
xtra_netpair = xtra_netpair} 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

593 
else cs; 
1800  594 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

595 
fun delE th 
9938  596 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
597 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

598 
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

599 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
9938  600 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
601 
safeIs = safeIs, 

602 
safeEs = safeEs, 

603 
hazIs = hazIs, 

604 
hazEs = rem_thm (hazEs,th), 

605 
xtraIs = xtraIs, 

606 
xtraEs = xtraEs, 

607 
swrappers = swrappers, 

608 
uwrappers = uwrappers, 

609 
safe0_netpair = safe0_netpair, 

610 
safep_netpair = safep_netpair, 

611 
xtra_netpair = xtra_netpair} 

6955  612 
else cs; 
613 

614 

615 
fun delXI th 

616 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

9938  617 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
6955  618 
if mem_thm (th, xtraIs) then 
619 
CS{xtra_netpair = delete ([th], []) xtra_netpair, 

9938  620 
safeIs = safeIs, 
621 
safeEs = safeEs, 

622 
hazIs = hazIs, 

623 
hazEs = hazEs, 

624 
xtraIs = rem_thm (xtraIs,th), 

625 
xtraEs = xtraEs, 

626 
swrappers = swrappers, 

627 
uwrappers = uwrappers, 

628 
safe0_netpair = safe0_netpair, 

629 
safep_netpair = safep_netpair, 

630 
haz_netpair = haz_netpair, 

631 
dup_netpair = dup_netpair} 

6955  632 
else cs; 
633 

634 
fun delXE th 

9938  635 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
636 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

6955  637 
if mem_thm (th, xtraEs) then 
638 
CS{xtra_netpair = delete ([], [th]) xtra_netpair, 

9938  639 
safeIs = safeIs, 
640 
safeEs = safeEs, 

641 
hazIs = hazIs, 

642 
hazEs = hazEs, 

643 
xtraIs = xtraIs, 

644 
xtraEs = rem_thm (xtraEs,th), 

645 
swrappers = swrappers, 

646 
uwrappers = uwrappers, 

647 
safe0_netpair = safe0_netpair, 

648 
safep_netpair = safep_netpair, 

649 
haz_netpair = haz_netpair, 

650 
dup_netpair = dup_netpair} 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

651 
else cs; 
1800  652 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

653 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
6955  654 
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, th) = 
9938  655 
let val th' = Data.make_elim th in 
656 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 

657 
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse 

658 
mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) orelse 

659 
mem_thm (th', safeEs) orelse mem_thm (th', hazEs) orelse mem_thm (th', xtraEs) 

660 
then delSI th (delSE th (delI th (delE th (delXI th (delXE th 

661 
(delSE th' (delE th' (delXE th' cs)))))))) 

662 
else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs) 

663 
end; 

1800  664 

665 
val op delrules = foldl delrule; 

666 

667 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

668 
(*** Modifying the wrapper tacticals ***) 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

669 
fun update_swrappers 
6955  670 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
671 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

672 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
6955  673 
xtraIs = xtraIs, xtraEs = xtraEs, 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

674 
swrappers = f swrappers, uwrappers = uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

675 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  676 
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

677 

b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

678 
fun update_uwrappers 
6955  679 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
680 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

681 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
6955  682 
xtraIs = xtraIs, xtraEs = xtraEs, 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

683 
swrappers = swrappers, uwrappers = f uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

684 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  685 
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

686 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

687 

4651  688 
(*Add/replace a safe wrapper*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

689 
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => 
9721  690 
overwrite_warn (swrappers, new_swrapper) 
691 
("Overwriting safe wrapper " ^ fst new_swrapper)); 

4651  692 

693 
(*Add/replace an unsafe wrapper*) 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

694 
fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers => 
9721  695 
overwrite_warn (uwrappers, new_uwrapper) 
9938  696 
("Overwriting unsafe wrapper "^fst new_uwrapper)); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

697 

4651  698 
(*Remove a safe wrapper*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

699 
fun cs delSWrapper name = update_swrappers cs (fn swrappers => 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

700 
let val (del,rest) = partition (fn (n,_) => n=name) swrappers 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

701 
in if null del then (warning ("No such safe wrapper in claset: "^ name); 
9938  702 
swrappers) else rest end); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

703 

4651  704 
(*Remove an unsafe wrapper*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

705 
fun cs delWrapper name = update_uwrappers cs (fn uwrappers => 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

706 
let val (del,rest) = partition (fn (n,_) => n=name) uwrappers 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

707 
in if null del then (warning ("No such unsafe wrapper in claset: " ^ name); 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

708 
uwrappers) else rest end); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

709 

2630  710 
(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

711 
fun cs addSbefore (name, tac1) = 
5523  712 
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

713 
fun cs addSaltern (name, tac2) = 
5523  714 
cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

715 

2630  716 
(*compose a tactic sequentially before/alternatively after the step tactic*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

717 
fun cs addbefore (name, tac1) = 
5523  718 
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

719 
fun cs addaltern (name, tac2) = 
5523  720 
cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

721 

5523  722 
fun cs addD2 (name, thm) = 
723 
cs addaltern (name, dtac thm THEN' atac); 

724 
fun cs addE2 (name, thm) = 

725 
cs addaltern (name, etac thm THEN' atac); 

726 
fun cs addSD2 (name, thm) = 

727 
cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac); 

728 
fun cs addSE2 (name, thm) = 

729 
cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac); 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

730 

1711  731 
(*Merge works by adding all new rules of the 2nd claset into the 1st claset. 
732 
Merging the term nets may look more efficient, but the rather delicate 

733 
treatment of priority might get muddled up.*) 

734 
fun merge_cs 

6955  735 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, 
4765  736 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, 
9938  737 
xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) = 
1711  738 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 
739 
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) 

2630  740 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
741 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

6955  742 
val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) 
743 
val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

744 
val cs1 = cs addSIs safeIs' 
9938  745 
addSEs safeEs' 
746 
addIs hazIs' 

747 
addEs hazEs' 

748 
addXIs xtraIs' 

749 
addXEs xtraEs' 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

750 
val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers); 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

751 
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

752 
in cs3 
1711  753 
end; 
754 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

755 

1800  756 
(**** Simple tactics for theorem proving ****) 
0  757 

758 
(*Attack subgoals using safe inferences  matching, not resolution*) 

2630  759 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  760 
appSWrappers cs (FIRST' [ 
9938  761 
eq_assume_tac, 
762 
eq_mp_tac, 

763 
bimatch_from_nets_tac safe0_netpair, 

764 
FIRST' hyp_subst_tacs, 

765 
bimatch_from_nets_tac safep_netpair]); 

0  766 

5757  767 
(*Repeatedly attack a subgoal using safe inferences  it's deterministic!*) 
768 
fun safe_steps_tac cs = REPEAT_DETERM1 o 

9938  769 
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); 
5757  770 

0  771 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
5757  772 
fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs)); 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

773 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

774 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

775 
(*** 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

776 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

777 
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

778 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

779 
(*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

780 
create precisely n subgoals.*) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

781 
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

782 
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

783 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

784 
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

785 
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

786 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

787 
(*Twoway 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

788 
fun bimatch2_tac netpair i = 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

789 
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

790 
(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

791 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

792 
(*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

793 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  794 
appSWrappers cs (FIRST' [ 
9938  795 
eq_assume_contr_tac, 
796 
bimatch_from_nets_tac safe0_netpair, 

797 
FIRST' hyp_subst_tacs, 

798 
n_bimatch_from_nets_tac 1 safep_netpair, 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

799 
bimatch2_tac safep_netpair]); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

800 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

801 
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

802 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

803 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

804 
(*** 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

805 

4066  806 
(*Backtracking is allowed among the various these unsafe ways of 
807 
proving a subgoal. *) 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

808 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
9938  809 
assume_tac APPEND' 
810 
contr_tac APPEND' 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

811 
biresolve_from_nets_tac safe0_netpair; 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

812 

4066  813 
(*These unsafe steps could generate more subgoals.*) 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

814 
fun instp_step_tac (CS{safep_netpair,...}) = 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

815 
biresolve_from_nets_tac safep_netpair; 
0  816 

817 
(*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

818 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  819 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

820 
fun haz_step_tac (CS{haz_netpair,...}) = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

821 
biresolve_from_nets_tac haz_netpair; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

822 

0  823 
(*Single step for the prover. FAILS unless it makes progress. *) 
5523  824 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  825 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  826 

827 
(*Using a "safe" rule to instantiate variables is unsafe. This tactic 

828 
allows backtracking from "safe" rules to "unsafe" rules here.*) 

5523  829 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  830 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  831 

1800  832 
(**** The following tactics all fail unless they solve one goal ****) 
0  833 

834 
(*Dumb but fast*) 

835 
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 

836 

837 
(*Slower but smarter than fast_tac*) 

838 
fun best_tac cs = 

839 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 

840 

9402  841 
(*even a bit smarter than best_tac*) 
842 
fun first_best_tac cs = 

843 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 

844 

0  845 
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
846 

847 
fun slow_best_tac cs = 

848 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 

849 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

850 

1800  851 
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

852 
val weight_ASTAR = ref 5; 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

853 

e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

854 
fun astar_tac cs = 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

855 
SELECT_GOAL ( ASTAR (has_fewer_prems 1 
9938  856 
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
857 
(step_tac cs 1)); 

1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

858 

e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

859 
fun slow_astar_tac cs = 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

860 
SELECT_GOAL ( ASTAR (has_fewer_prems 1 
9938  861 
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
862 
(slow_step_tac cs 1)); 

1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

863 

1800  864 
(**** 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

865 
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

866 
easy theorems faster, but loses completeness  and many of the harder 
1800  867 
theorems such as 43. ****) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

868 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

869 
(*Nondeterministic! Could always expand the first unsafe connective. 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

870 
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

871 
greater search depth required.*) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

872 
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

873 
biresolve_from_nets_tac dup_netpair; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

874 

5523  875 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  876 
local 
877 
fun slow_step_tac' cs = appWrappers cs 

9938  878 
(instp_step_tac cs APPEND' dup_step_tac cs); 
5757  879 
in fun depth_tac cs m i state = SELECT_GOAL 
880 
(safe_steps_tac cs 1 THEN_ELSE 

9938  881 
(DEPTH_SOLVE (depth_tac cs m 1), 
882 
inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac 

883 
(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m1) 1)) 

5757  884 
)) i state; 
885 
end; 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

886 

2173  887 
(*Search, with depth bound m. 
888 
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

889 
fun safe_depth_tac cs m = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

890 
SUBGOAL 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

891 
(fn (prem,i) => 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

892 
let val deti = 
9938  893 
(*No Vars in the goal? No need to backtrack between goals.*) 
894 
case term_vars prem of 

895 
[] => DETERM 

896 
 _::_ => I 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

897 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  898 
DEPTH_SOLVE (deti (depth_tac cs m 1))) i 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

899 
end); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

900 

2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset

901 
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

902 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

903 

1724  904 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

905 
(** claset theory data **) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

906 

7354  907 
(* theory data kind 'Provers/claset' *) 
1724  908 

7354  909 
structure GlobalClasetArgs = 
910 
struct 

911 
val name = "Provers/claset"; 

912 
type T = claset ref; 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

913 

7354  914 
val empty = ref empty_cs; 
915 
fun copy (ref cs) = (ref cs): T; (*create new reference!*) 

6556  916 
val prep_ext = copy; 
7354  917 
fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2)); 
918 
fun print _ (ref cs) = print_cs cs; 

919 
end; 

1724  920 

7354  921 
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); 
922 
val print_claset = GlobalClaset.print; 

923 
val claset_ref_of_sg = GlobalClaset.get_sg; 

924 
val claset_ref_of = GlobalClaset.get; 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

925 

1724  926 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

927 
(* access claset *) 
1724  928 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

929 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  930 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  931 

6391  932 
fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; 
933 
fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state; 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

934 

5028  935 
val claset = claset_of o Context.the_context; 
6391  936 
val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

937 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

938 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

939 
(* change claset *) 
1800  940 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

941 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  942 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

943 
val AddDs = change_claset (op addDs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

944 
val AddEs = change_claset (op addEs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

945 
val AddIs = change_claset (op addIs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

946 
val AddSDs = change_claset (op addSDs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

947 
val AddSEs = change_claset (op addSEs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

948 
val AddSIs = change_claset (op addSIs); 
6955  949 
val AddXDs = change_claset (op addXDs); 
950 
val AddXEs = change_claset (op addXEs); 

951 
val AddXIs = change_claset (op addXIs); 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

952 
val Delrules = change_claset (op delrules); 
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

953 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

954 

5841  955 
(* proof data kind 'Provers/claset' *) 
956 

957 
structure LocalClasetArgs = 

958 
struct 

959 
val name = "Provers/claset"; 

960 
type T = claset; 

961 
val init = claset_of; 

962 
fun print _ cs = print_cs cs; 

963 
end; 

964 

965 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

966 
val print_local_claset = LocalClaset.print; 

967 
val get_local_claset = LocalClaset.get; 

968 
val put_local_claset = LocalClaset.put; 

969 

970 

5885  971 
(* attributes *) 
972 

973 
fun change_global_cs f (thy, th) = 

974 
let val r = claset_ref_of thy 

6096  975 
in r := f (! r, [th]); (thy, th) end; 
5885  976 

977 
fun change_local_cs f (ctxt, th) = 

6096  978 
let val cs = f (get_local_claset ctxt, [th]) 
5885  979 
in (put_local_claset cs ctxt, th) end; 
980 

981 
val safe_dest_global = change_global_cs (op addSDs); 

982 
val safe_elim_global = change_global_cs (op addSEs); 

983 
val safe_intro_global = change_global_cs (op addSIs); 

6955  984 
val haz_dest_global = change_global_cs (op addDs); 
985 
val haz_elim_global = change_global_cs (op addEs); 

986 
val haz_intro_global = change_global_cs (op addIs); 

987 
val xtra_dest_global = change_global_cs (op addXDs); 

988 
val xtra_elim_global = change_global_cs (op addXEs); 

989 
val xtra_intro_global = change_global_cs (op addXIs); 

9938  990 
val rule_del_global = change_global_cs (op delrules); 
5885  991 

6955  992 
val safe_dest_local = change_local_cs (op addSDs); 
993 
val safe_elim_local = change_local_cs (op addSEs); 

994 
val safe_intro_local = change_local_cs (op addSIs); 

5885  995 
val haz_dest_local = change_local_cs (op addDs); 
996 
val haz_elim_local = change_local_cs (op addEs); 

997 
val haz_intro_local = change_local_cs (op addIs); 

6955  998 
val xtra_dest_local = change_local_cs (op addXDs); 
999 
val xtra_elim_local = change_local_cs (op addXEs); 

1000 
val xtra_intro_local = change_local_cs (op addXIs); 

9938  1001 
val rule_del_local = change_local_cs (op delrules); 
5885  1002 

1003 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

1004 
(* tactics referring to the implicit claset *) 
1800  1005 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

1006 
(*the abstraction over the proof state delays the dereferencing*) 
9938  1007 
fun Safe_tac st = safe_tac (claset()) st; 
1008 
fun Safe_step_tac i st = safe_step_tac (claset()) i st; 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

1009 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  1010 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
1011 
fun Step_tac i st = step_tac (claset()) i st; 

1012 
fun Fast_tac i st = fast_tac (claset()) i st; 

1013 
fun Best_tac i st = best_tac (claset()) i st; 

1014 
fun Slow_tac i st = slow_tac (claset()) i st; 

1015 
fun Slow_best_tac i st = slow_best_tac (claset()) i st; 

1016 
fun Deepen_tac m = deepen_tac (claset()) m; 

2066  1017 

1800  1018 

0  1019 
end; 
5841  1020 

1021 

1022 

5885  1023 
(** concrete syntax of attributes **) 
5841  1024 

1025 
(* add / del rules *) 

1026 

1027 
val introN = "intro"; 

1028 
val elimN = "elim"; 

1029 
val destN = "dest"; 

9938  1030 
val ruleN = "rule"; 
5841  1031 

6955  1032 
fun cla_att change xtra haz safe = Attrib.syntax 
10034  1033 
(Scan.lift ((Args.query >> K xtra  Args.bang >> K safe  Scan.succeed haz) >> change)); 
5841  1034 

6955  1035 
fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); 
9938  1036 

10034  1037 
fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att); 
9938  1038 
val rule_del_attr = (del_args rule_del_global, del_args rule_del_local); 
5841  1039 

1040 

1041 
(* setup_attrs *) 

1042 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9938
diff
changeset

1043 
fun elim_format x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x; 
9184  1044 

5841  1045 
val setup_attrs = Attrib.add_attributes 
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9938
diff
changeset

1046 
[("elim_format", (elim_format, elim_format), 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9938
diff
changeset

1047 
"destruct rule turned into elimination rule format (classical)"), 
9899  1048 
(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"), 
1049 
(elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"), 

1050 
(introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"), 

9938  1051 
(ruleN, rule_del_attr, "remove declaration of intro/elim/dest rule")]; 
5841  1052 

1053 

1054 

7230  1055 
(** proof methods **) 
1056 

1057 
(* get nets (appropriate order for semiautomatic methods) *) 

1058 

1059 
local 

1060 
val imp_elim_netpair = insert (0, 0) ([], [imp_elim]) empty_netpair; 

1061 
val not_elim_netpair = insert (0, 0) ([], [Data.not_elim]) empty_netpair; 

1062 
in 

1063 
fun get_nets (CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair, ...}) = 

1064 
[imp_elim_netpair, safe0_netpair, safep_netpair, not_elim_netpair, haz_netpair, dup_netpair, xtra_netpair]; 

1065 
end; 

1066 

1067 

1068 
(* METHOD_CLASET' *) 

5841  1069 

8098  1070 
fun METHOD_CLASET' tac ctxt = 
8671  1071 
Method.METHOD (HEADGOAL o tac (get_local_claset ctxt)); 
7230  1072 

1073 

1074 
val trace_rules = ref false; 

5841  1075 

7230  1076 
local 
1077 

1078 
fun trace rules i = 

1079 
if not (! trace_rules) then () 

1080 
else Pretty.writeln (Pretty.big_list ("trying standard rule(s) on goal #" ^ string_of_int i ^ ":") 

1081 
(map Display.pretty_thm rules)); 

1082 

1083 

5841  1084 
fun order_rules xs = map snd (Tactic.orderlist xs); 
1085 

1086 
fun find_rules concl nets = 

1087 
let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl) 

1088 
in flat (map rules_of nets) end; 

1089 

1090 
fun find_erules [] _ = [] 

6955  1091 
 find_erules (fact :: _) nets = 
5841  1092 
let 
6502  1093 
fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; 
6955  1094 
fun erules_of (_, enet) = order_rules (may_unify enet fact); 
6502  1095 
in flat (map erules_of nets) end; 
5841  1096 

1097 

7230  1098 
fun some_rule_tac cs facts = 
5841  1099 
let 
7230  1100 
val nets = get_nets cs; 
6492  1101 
val erules = find_erules facts nets; 
5841  1102 

1103 
val tac = SUBGOAL (fn (goal, i) => 

1104 
let 

1105 
val irules = find_rules (Logic.strip_assums_concl goal) nets; 

1106 
val rules = erules @ irules; 

7425  1107 
val ruleq = Method.multi_resolves facts rules; 
7230  1108 
in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); 
5841  1109 
in tac end; 
1110 

7281  1111 
fun rule_tac [] cs facts = some_rule_tac cs facts 
1112 
 rule_tac rules _ facts = Method.rule_tac rules facts; 

1113 

7230  1114 
in 
7281  1115 
val rule = METHOD_CLASET' o rule_tac; 
7230  1116 
end; 
5841  1117 

1118 

7230  1119 
(* intro / elim methods *) 
1120 

1121 
local 

1122 

7329  1123 
fun intro_elim_tac netpair_of res_tac rules cs facts = 
1124 
let 

8342  1125 
val tac = 
9449  1126 
if null rules then FIRST' (map (bimatch_from_nets_tac o netpair_of) (get_nets cs)) 
7329  1127 
else res_tac rules; 
8342  1128 
in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end; 
6502  1129 

8699  1130 
val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) Tactic.match_tac; 
1131 
val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) Tactic.ematch_tac; 

7230  1132 

1133 
in 

1134 
val intro = METHOD_CLASET' o intro_tac; 

1135 
val elim = METHOD_CLASET' o elim_tac; 

1136 
end; 

1137 

1138 

1139 
(* contradiction method *) 

6502  1140 

7425  1141 
val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl]; 
6502  1142 

1143 

1144 
(* automatic methods *) 

5841  1145 

5927  1146 
val cla_modifiers = 
10034  1147 
[Args.$$$ destN  Args.query_colon >> K ((I, xtra_dest_local):Method.modifier), 
1148 
Args.$$$ destN  Args.bang_colon >> K (I, safe_dest_local), 

1149 
Args.$$$ destN  Args.colon >> K (I, haz_dest_local), 

1150 
Args.$$$ elimN  Args.query_colon >> K (I, xtra_elim_local), 

1151 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim_local), 

1152 
Args.$$$ elimN  Args.colon >> K (I, haz_elim_local), 

1153 
Args.$$$ introN  Args.query_colon >> K (I, xtra_intro_local), 

1154 
Args.$$$ introN  Args.bang_colon >> K (I, safe_intro_local), 

1155 
Args.$$$ introN  Args.colon >> K (I, haz_intro_local), 

1156 
Args.del  Args.colon >> K (I, rule_del_local)]; 

5927  1157 

7559  1158 
fun cla_meth tac prems ctxt = Method.METHOD (fn facts => 
1159 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt)); 

7132  1160 

7559  1161 
fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => 
8168  1162 
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt))); 
5841  1163 

7559  1164 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1165 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1166 

1167 

1168 

1169 
(** setup_methods **) 

1170 

1171 
val setup_methods = Method.add_methods 

9441  1172 
[("default", Method.thms_ctxt_args rule, "apply some rule (classical)"), 
1173 
("rule", Method.thms_ctxt_args rule, "apply some rule (classical)"), 

6502  1174 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
8098  1175 
("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"), 
1176 
("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"), 

10185  1177 
("clarify", cla_method' (CHANGED oo clarify_tac), "repeatedly apply safe steps"), 
7004  1178 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1179 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1180 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
1181 
("safe", cla_method safe_tac, "classical prover (apply safe rules)")]; 

5841  1182 

1183 

1184 

1185 
(** theory setup **) 

1186 

7354  1187 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1188 

1189 

8667  1190 

1191 
(** outer syntax **) 

1192 

1193 
val print_clasetP = 

1194 
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" 

1195 
OuterSyntax.Keyword.diag 

9513  1196 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1197 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1198 

1199 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1200 

1201 

5841  1202 
end; 