author  wenzelm 
Fri, 03 Nov 2000 21:29:56 +0100  
changeset 10382  1fb807260ff1 
parent 10309  a7f961fb62c6 
child 10394  eef9e422929a 
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 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

37 
end; 
0  38 

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

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

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

43 
val print_cs: claset > unit 
4380  44 
val print_claset: theory > unit 
4653  45 
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

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

49 
swrappers: (string * wrapper) list, 

50 
uwrappers: (string * wrapper) list, 

51 
safe0_netpair: netpair, safep_netpair: netpair, 

52 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} 

53 
val merge_cs : claset * claset > claset 

54 
val addDs : claset * thm list > claset 

55 
val addEs : claset * thm list > claset 

56 
val addIs : claset * thm list > claset 

57 
val addSDs : claset * thm list > claset 

58 
val addSEs : claset * thm list > claset 

59 
val addSIs : claset * thm list > claset 

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

62 
val addXIs : claset * thm list > claset 

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

65 
val delSWrapper : claset * string > claset 

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

67 
val delWrapper : claset * string > claset 

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

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

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

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

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

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

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

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

78 
val trace_rules : bool ref 

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

79 

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

80 
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

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

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

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

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

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

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

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

88 

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

91 
val weight_ASTAR : int ref 

92 
val astar_tac : claset > int > tactic 

93 
val slow_astar_tac : claset > int > tactic 

94 
val best_tac : claset > int > tactic 

95 
val first_best_tac : claset > int > tactic 

96 
val slow_best_tac : claset > int > tactic 

97 
val depth_tac : claset > int > int > tactic 

98 
val deepen_tac : claset > int > int > tactic 

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

99 

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

102 
val dup_intr : thm > thm 

103 
val dup_step_tac : claset > int > tactic 

104 
val eq_mp_tac : int > tactic 

105 
val haz_step_tac : claset > int > tactic 

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

107 
val mp_tac : int > tactic 

108 
val safe_tac : claset > tactic 

109 
val safe_steps_tac : claset > int > tactic 

110 
val safe_step_tac : claset > int > tactic 

111 
val clarify_tac : claset > int > tactic 

112 
val clarify_step_tac : claset > int > tactic 

113 
val step_tac : claset > int > tactic 

114 
val slow_step_tac : claset > int > tactic 

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

116 
val swapify : thm list > thm list 

117 
val swap_res_tac : thm list > int > tactic 

118 
val inst_step_tac : claset > int > tactic 

119 
val inst0_step_tac : claset > int > tactic 

120 
val instp_step_tac : claset > int > tactic 

1724  121 

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

124 
val AddIs : thm list > unit 

125 
val AddSDs : thm list > unit 

126 
val AddSEs : thm list > unit 

127 
val AddSIs : thm list > unit 

128 
val AddXDs : thm list > unit 

129 
val AddXEs : thm list > unit 

130 
val AddXIs : thm list > unit 

131 
val Delrules : thm list > unit 

132 
val Safe_tac : tactic 

133 
val Safe_step_tac : int > tactic 

134 
val Clarify_tac : int > tactic 

135 
val Clarify_step_tac : int > tactic 

136 
val Step_tac : int > tactic 

137 
val Fast_tac : int > tactic 

138 
val Best_tac : int > tactic 

139 
val Slow_tac : int > tactic 

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

142 
end; 
1724  143 

5841  144 
signature CLASSICAL = 
145 
sig 

146 
include BASIC_CLASSICAL 

147 
val print_local_claset: Proof.context > unit 

148 
val get_local_claset: Proof.context > claset 

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

150 
val safe_dest_global: theory attribute 

151 
val safe_elim_global: theory attribute 

152 
val safe_intro_global: theory attribute 

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

155 
val haz_intro_global: theory attribute 

156 
val xtra_dest_global: theory attribute 

157 
val xtra_elim_global: theory attribute 

158 
val xtra_intro_global: theory attribute 

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

162 
val safe_intro_local: Proof.context attribute 

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

165 
val haz_intro_local: Proof.context attribute 

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

168 
val xtra_intro_local: Proof.context attribute 

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

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

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

177 

0  178 

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

7354  182 
local open Data in 
0  183 

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

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

186 
val atomize_tac = Method.atomize_tac atomize; 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

187 

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

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

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

194 
val contr_tac = eresolve_tac [not_elim] THEN' 

195 
(eq_assume_tac ORELSE' assume_tac); 

0  196 

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

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

198 
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

199 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  200 

201 
(*Like mp_tac but instantiates no variables*) 

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

202 
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

203 

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

0  206 

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

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

209 

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

211 
trying rules in order. *) 

212 
fun swap_res_tac rls = 

54  213 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
9938  214 
in assume_tac ORELSE' 
215 
contr_tac ORELSE' 

54  216 
biresolve_tac (foldr addrl (rls,[])) 
0  217 
end; 
218 

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

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

220 
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

221 

6967  222 
fun dup_elim th = 
223 
(case try 

224 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

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

226 
Some th' => th' 

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

0  228 

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

229 

1800  230 
(**** Classical rule sets ****) 
0  231 

232 
datatype claset = 

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

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

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

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

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

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

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

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

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

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

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

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

0  246 

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

247 
(*Desired invariants are 
9938  248 
safe0_netpair = build safe0_brls, 
249 
safep_netpair = build safep_brls, 

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

251 
dup_netpair = build (joinrules(map dup_intr hazIs, 

252 
map dup_elim hazEs)), 

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

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

254 

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

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

256 
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

257 
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

258 
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

259 
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

260 
*) 
0  261 

6502  262 
val empty_netpair = (Net.empty, Net.empty); 
263 

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

264 
val empty_cs = 
9938  265 
CS{safeIs = [], 
266 
safeEs = [], 

267 
hazIs = [], 

268 
hazEs = [], 

269 
xtraIs = [], 

270 
xtraEs = [], 

4651  271 
swrappers = [], 
272 
uwrappers = [], 

6502  273 
safe0_netpair = empty_netpair, 
274 
safep_netpair = empty_netpair, 

275 
haz_netpair = empty_netpair, 

6955  276 
dup_netpair = empty_netpair, 
277 
xtra_netpair = empty_netpair}; 

0  278 

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

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

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

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

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

8727  287 
> Pretty.chunks > Pretty.writeln 
3546  288 
end; 
0  289 

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

291 

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

294 
in 

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

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

297 
end; 

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

298 

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

299 

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

301 

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

302 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  303 
***) 
0  304 

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

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

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

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

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

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

310 

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

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

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

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

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

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

317 

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

319 

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

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

321 
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

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

323 
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

324 

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

326 

1800  327 
val delete = delete_tagged_list o joinrules; 
328 

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

329 
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

330 
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

331 

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

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

333 
is still allowed.*) 
6955  334 
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

335 
if mem_thm (th, safeIs) then 
9938  336 
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

337 
else if mem_thm (th, safeEs) then 
9408  338 
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

339 
else if mem_thm (th, hazIs) then 
9760  340 
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

341 
else if mem_thm (th, hazEs) then 
9760  342 
warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th) 
6955  343 
else if mem_thm (th, xtraIs) then 
9408  344 
warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th) 
6955  345 
else if mem_thm (th, xtraEs) then 
9408  346 
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

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

348 

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

350 

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

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

354 
if mem_thm (th, safeIs) then 
9938  355 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); 
356 
cs) 

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

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

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

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

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

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

364 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  365 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
366 
safeEs = safeEs, 

367 
hazIs = hazIs, 

368 
hazEs = hazEs, 

369 
xtraIs = xtraIs, 

370 
xtraEs = xtraEs, 

371 
swrappers = swrappers, 

372 
uwrappers = uwrappers, 

373 
haz_netpair = haz_netpair, 

374 
dup_netpair = dup_netpair, 

375 
xtra_netpair = xtra_netpair} 

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

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

377 

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

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

381 
if mem_thm (th, safeEs) then 
9938  382 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); 
383 
cs) 

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

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

385 
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

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

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

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

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

391 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  392 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
393 
safeIs = safeIs, 

394 
hazIs = hazIs, 

395 
hazEs = hazEs, 

396 
xtraIs = xtraIs, 

397 
xtraEs = xtraEs, 

398 
swrappers = swrappers, 

399 
uwrappers = uwrappers, 

400 
haz_netpair = haz_netpair, 

401 
dup_netpair = dup_netpair, 

402 
xtra_netpair = xtra_netpair} 

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

403 
end; 
0  404 

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

405 
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

406 

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

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

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

409 

9938  410 
fun cs addSDs ths = cs addSEs (map Data.make_elim ths); 
0  411 

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

412 

1800  413 
(*** Hazardous (unsafe) rules ***) 
0  414 

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

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

418 
if mem_thm (th, hazIs) then 
9938  419 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
420 
cs) 

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

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

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

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

424 
in warn_dup th cs; 
9938  425 
CS{hazIs = th::hazIs, 
426 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 

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

428 
safeIs = safeIs, 

429 
safeEs = safeEs, 

430 
hazEs = hazEs, 

431 
xtraIs = xtraIs, 

432 
xtraEs = xtraEs, 

433 
swrappers = swrappers, 

434 
uwrappers = uwrappers, 

435 
safe0_netpair = safe0_netpair, 

436 
safep_netpair = safep_netpair, 

437 
xtra_netpair = xtra_netpair} 

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

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

439 

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

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

443 
if mem_thm (th, hazEs) then 
9938  444 
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); 
445 
cs) 

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

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

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

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

449 
in warn_dup th cs; 
9938  450 
CS{hazEs = th::hazEs, 
451 
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, 

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

453 
safeIs = safeIs, 

454 
safeEs = safeEs, 

455 
hazIs = hazIs, 

456 
xtraIs = xtraIs, 

457 
xtraEs = xtraEs, 

458 
swrappers = swrappers, 

459 
uwrappers = uwrappers, 

460 
safe0_netpair = safe0_netpair, 

461 
safep_netpair = safep_netpair, 

462 
xtra_netpair = xtra_netpair} 

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

463 
end; 
0  464 

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

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

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

467 

9938  468 
fun cs addDs ths = cs addEs (map Data.make_elim ths); 
0  469 

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

470 

6955  471 
(*** Extra (single step) rules ***) 
472 

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

9938  474 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
475 
th)= 

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

6955  479 
else 
480 
let val nI = length xtraIs + 1 

481 
and nE = length xtraEs 

482 
in warn_dup th cs; 

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

485 
safeIs = safeIs, 

486 
safeEs = safeEs, 

487 
hazIs = hazIs, 

488 
hazEs = hazEs, 

489 
xtraEs = xtraEs, 

490 
swrappers = swrappers, 

491 
uwrappers = uwrappers, 

492 
safe0_netpair = safe0_netpair, 

493 
safep_netpair = safep_netpair, 

494 
haz_netpair = haz_netpair, 

495 
dup_netpair = dup_netpair} 

6955  496 
end; 
497 

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

9938  499 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
500 
th) = 

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

6955  504 
else 
505 
let val nI = length xtraIs 

506 
and nE = length xtraEs + 1 

507 
in warn_dup th cs; 

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

510 
safeIs = safeIs, 

511 
safeEs = safeEs, 

512 
hazIs = hazIs, 

513 
hazEs = hazEs, 

514 
xtraIs = xtraIs, 

515 
swrappers = swrappers, 

516 
uwrappers = uwrappers, 

517 
safe0_netpair = safe0_netpair, 

518 
safep_netpair = safep_netpair, 

519 
haz_netpair = haz_netpair, 

520 
dup_netpair = dup_netpair} 

6955  521 
end; 
522 

523 
val op addXIs = rev_foldl addXI; 

524 
val op addXEs = rev_foldl addXE; 

525 

9938  526 
fun cs addXDs ths = cs addXEs (map Data.make_elim ths); 
6955  527 

528 

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

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

532 
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

533 
searches in all the lists and chooses the relevant delXX functions. 
1800  534 
***) 
535 

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

536 
fun delSI th 
6955  537 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  538 
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

539 
if mem_thm (th, safeIs) then 
7559  540 
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

541 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  542 
safep_netpair = delete (safep_rls, []) safep_netpair, 
543 
safeIs = rem_thm (safeIs,th), 

544 
safeEs = safeEs, 

545 
hazIs = hazIs, 

546 
hazEs = hazEs, 

547 
xtraIs = xtraIs, 

548 
xtraEs = xtraEs, 

549 
swrappers = swrappers, 

550 
uwrappers = uwrappers, 

551 
haz_netpair = haz_netpair, 

552 
dup_netpair = dup_netpair, 

553 
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

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

555 
else cs; 
1800  556 

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

557 
fun delSE th 
6955  558 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  559 
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

560 
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

561 
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

562 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  563 
safep_netpair = delete ([], safep_rls) safep_netpair, 
564 
safeIs = safeIs, 

565 
safeEs = rem_thm (safeEs,th), 

566 
hazIs = hazIs, 

567 
hazEs = hazEs, 

568 
xtraIs = xtraIs, 

569 
xtraEs = xtraEs, 

570 
swrappers = swrappers, 

571 
uwrappers = uwrappers, 

572 
haz_netpair = haz_netpair, 

573 
dup_netpair = dup_netpair, 

574 
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

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

576 
else cs; 
1800  577 

578 

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

579 
fun delI th 
6955  580 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  581 
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

582 
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

583 
CS{haz_netpair = delete ([th], []) haz_netpair, 
9938  584 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
585 
safeIs = safeIs, 

586 
safeEs = safeEs, 

587 
hazIs = rem_thm (hazIs,th), 

588 
hazEs = hazEs, 

589 
xtraIs = xtraIs, 

590 
xtraEs = xtraEs, 

591 
swrappers = swrappers, 

592 
uwrappers = uwrappers, 

593 
safe0_netpair = safe0_netpair, 

594 
safep_netpair = safep_netpair, 

595 
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

596 
else cs; 
1800  597 

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

598 
fun delE th 
9938  599 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
600 
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

601 
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

602 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
9938  603 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
604 
safeIs = safeIs, 

605 
safeEs = safeEs, 

606 
hazIs = hazIs, 

607 
hazEs = rem_thm (hazEs,th), 

608 
xtraIs = xtraIs, 

609 
xtraEs = xtraEs, 

610 
swrappers = swrappers, 

611 
uwrappers = uwrappers, 

612 
safe0_netpair = safe0_netpair, 

613 
safep_netpair = safep_netpair, 

614 
xtra_netpair = xtra_netpair} 

6955  615 
else cs; 
616 

617 

618 
fun delXI th 

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

9938  620 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
6955  621 
if mem_thm (th, xtraIs) then 
622 
CS{xtra_netpair = delete ([th], []) xtra_netpair, 

9938  623 
safeIs = safeIs, 
624 
safeEs = safeEs, 

625 
hazIs = hazIs, 

626 
hazEs = hazEs, 

627 
xtraIs = rem_thm (xtraIs,th), 

628 
xtraEs = xtraEs, 

629 
swrappers = swrappers, 

630 
uwrappers = uwrappers, 

631 
safe0_netpair = safe0_netpair, 

632 
safep_netpair = safep_netpair, 

633 
haz_netpair = haz_netpair, 

634 
dup_netpair = dup_netpair} 

6955  635 
else cs; 
636 

637 
fun delXE th 

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

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

9938  642 
safeIs = safeIs, 
643 
safeEs = safeEs, 

644 
hazIs = hazIs, 

645 
hazEs = hazEs, 

646 
xtraIs = xtraIs, 

647 
xtraEs = rem_thm (xtraEs,th), 

648 
swrappers = swrappers, 

649 
uwrappers = uwrappers, 

650 
safe0_netpair = safe0_netpair, 

651 
safep_netpair = safep_netpair, 

652 
haz_netpair = haz_netpair, 

653 
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

654 
else cs; 
1800  655 

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

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

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

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

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

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

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

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

666 
end; 

1800  667 

668 
val op delrules = foldl delrule; 

669 

670 

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

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

672 
fun update_swrappers 
6955  673 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
674 
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

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

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

678 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  679 
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

680 

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

681 
fun update_uwrappers 
6955  682 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
683 
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

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

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

687 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  688 
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

689 

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

690 

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

692 
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => 
9721  693 
overwrite_warn (swrappers, new_swrapper) 
694 
("Overwriting safe wrapper " ^ fst new_swrapper)); 

4651  695 

696 
(*Add/replace an unsafe wrapper*) 

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

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

700 

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

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

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

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

706 

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

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

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

710 
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

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

712 

2630  713 
(*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

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

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

718 

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

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

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

724 

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

727 
fun cs addE2 (name, thm) = 

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

729 
fun cs addSD2 (name, thm) = 

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

731 
fun cs addSE2 (name, thm) = 

732 
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

733 

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

736 
treatment of priority might get muddled up.*) 

737 
fun merge_cs 

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

2630  743 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
744 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

6955  745 
val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) 
746 
val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) 

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

747 
val cs1 = cs addSIs safeIs' 
9938  748 
addSEs safeEs' 
749 
addIs hazIs' 

750 
addEs hazEs' 

751 
addXIs xtraIs' 

752 
addXEs xtraEs' 

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

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

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

755 
in cs3 
1711  756 
end; 
757 

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

758 

1800  759 
(**** Simple tactics for theorem proving ****) 
0  760 

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

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

766 
bimatch_from_nets_tac safe0_netpair, 

767 
FIRST' hyp_subst_tacs, 

768 
bimatch_from_nets_tac safep_netpair]); 

0  769 

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

9938  772 
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); 
5757  773 

0  774 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
5757  775 
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

776 

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

777 

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

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

779 

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

780 
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

781 

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

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

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

784 
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

785 
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

786 

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

787 
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

788 
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

789 

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

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

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

792 
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

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

794 

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

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

796 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  797 
appSWrappers cs (FIRST' [ 
9938  798 
eq_assume_contr_tac, 
799 
bimatch_from_nets_tac safe0_netpair, 

800 
FIRST' hyp_subst_tacs, 

801 
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

802 
bimatch2_tac safep_netpair]); 
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 
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

805 

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

806 

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

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

808 

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

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

811 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
9938  812 
assume_tac APPEND' 
813 
contr_tac APPEND' 

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

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

815 

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

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

818 
biresolve_from_nets_tac safep_netpair; 
0  819 

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

821 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  822 

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

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

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

825 

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

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

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

5523  832 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  833 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  834 

1800  835 
(**** The following tactics all fail unless they solve one goal ****) 
0  836 

837 
(*Dumb but fast*) 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

838 
fun fast_tac cs = 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

839 
atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  840 

841 
(*Slower but smarter than fast_tac*) 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

842 
fun best_tac cs = 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

843 
atomize_tac THEN' 
0  844 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
845 

9402  846 
(*even a bit smarter than best_tac*) 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

847 
fun first_best_tac cs = 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

848 
atomize_tac THEN' 
9402  849 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
850 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

851 
fun slow_tac cs = 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

852 
atomize_tac THEN' 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

853 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  854 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

855 
fun slow_best_tac cs = 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

856 
atomize_tac THEN' 
0  857 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
858 

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

859 

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

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

862 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

863 
fun astar_tac cs = 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

864 
atomize_tac THEN' 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

865 
SELECT_GOAL 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

866 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev) 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

867 
(step_tac cs 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

868 

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

869 
fun slow_astar_tac cs = 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

870 
atomize_tac THEN' 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

871 
SELECT_GOAL 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

872 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev) 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

873 
(slow_step_tac cs 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

874 

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

876 
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

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

879 

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

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

881 
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

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

883 
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

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

885 

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

9938  889 
(instp_step_tac cs APPEND' dup_step_tac cs); 
5757  890 
in fun depth_tac cs m i state = SELECT_GOAL 
891 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  895 
)) i state; 
896 
end; 

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

897 

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

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

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

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

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

906 
[] => DETERM 

907 
 _::_ => I 

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

908 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  909 
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

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

911 

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

912 
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

913 

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

914 

1724  915 

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

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

917 

7354  918 
(* theory data kind 'Provers/claset' *) 
1724  919 

7354  920 
structure GlobalClasetArgs = 
921 
struct 

922 
val name = "Provers/claset"; 

923 
type T = claset ref; 

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

924 

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

6556  927 
val prep_ext = copy; 
7354  928 
fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2)); 
929 
fun print _ (ref cs) = print_cs cs; 

930 
end; 

1724  931 

7354  932 
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); 
933 
val print_claset = GlobalClaset.print; 

934 
val claset_ref_of_sg = GlobalClaset.get_sg; 

935 
val claset_ref_of = GlobalClaset.get; 

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

936 

1724  937 

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

938 
(* access claset *) 
1724  939 

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

940 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  941 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  942 

6391  943 
fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; 
944 
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

945 

5028  946 
val claset = claset_of o Context.the_context; 
6391  947 
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

948 

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

949 

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

950 
(* change claset *) 
1800  951 

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

952 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  953 

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

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

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

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

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

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

959 
val AddSIs = change_claset (op addSIs); 
6955  960 
val AddXDs = change_claset (op addXDs); 
961 
val AddXEs = change_claset (op addXEs); 

962 
val AddXIs = change_claset (op addXIs); 

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

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

964 

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

965 

5841  966 
(* proof data kind 'Provers/claset' *) 
967 

968 
structure LocalClasetArgs = 

969 
struct 

970 
val name = "Provers/claset"; 

971 
type T = claset; 

972 
val init = claset_of; 

973 
fun print _ cs = print_cs cs; 

974 
end; 

975 

976 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

977 
val print_local_claset = LocalClaset.print; 

978 
val get_local_claset = LocalClaset.get; 

979 
val put_local_claset = LocalClaset.put; 

980 

981 

5885  982 
(* attributes *) 
983 

984 
fun change_global_cs f (thy, th) = 

985 
let val r = claset_ref_of thy 

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

988 
fun change_local_cs f (ctxt, th) = 

6096  989 
let val cs = f (get_local_claset ctxt, [th]) 
5885  990 
in (put_local_claset cs ctxt, th) end; 
991 

992 
val safe_dest_global = change_global_cs (op addSDs); 

993 
val safe_elim_global = change_global_cs (op addSEs); 

994 
val safe_intro_global = change_global_cs (op addSIs); 

6955  995 
val haz_dest_global = change_global_cs (op addDs); 
996 
val haz_elim_global = change_global_cs (op addEs); 

997 
val haz_intro_global = change_global_cs (op addIs); 

998 
val xtra_dest_global = change_global_cs (op addXDs); 

999 
val xtra_elim_global = change_global_cs (op addXEs); 

1000 
val xtra_intro_global = change_global_cs (op addXIs); 

9938  1001 
val rule_del_global = change_global_cs (op delrules); 
5885  1002 

6955  1003 
val safe_dest_local = change_local_cs (op addSDs); 
1004 
val safe_elim_local = change_local_cs (op addSEs); 

1005 
val safe_intro_local = change_local_cs (op addSIs); 

5885  1006 
val haz_dest_local = change_local_cs (op addDs); 
1007 
val haz_elim_local = change_local_cs (op addEs); 

1008 
val haz_intro_local = change_local_cs (op addIs); 

6955  1009 
val xtra_dest_local = change_local_cs (op addXDs); 
1010 
val xtra_elim_local = change_local_cs (op addXEs); 

1011 
val xtra_intro_local = change_local_cs (op addXIs); 

9938  1012 
val rule_del_local = change_local_cs (op delrules); 
5885  1013 

1014 

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

1015 
(* tactics referring to the implicit claset *) 
1800  1016 

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

1017 
(*the abstraction over the proof state delays the dereferencing*) 
9938  1018 
fun Safe_tac st = safe_tac (claset()) st; 
1019 
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

1020 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  1021 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
1022 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  1028 

1800  1029 

0  1030 
end; 
5841  1031 

1032 

1033 

5885  1034 
(** concrete syntax of attributes **) 
5841  1035 

1036 
(* add / del rules *) 

1037 

1038 
val introN = "intro"; 

1039 
val elimN = "elim"; 

1040 
val destN = "dest"; 

9938  1041 
val ruleN = "rule"; 
5841  1042 

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

6955  1046 
fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); 
9938  1047 

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

1051 

1052 
(* setup_attrs *) 

1053 

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

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

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

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

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

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

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

1064 

1065 

7230  1066 
(** proof methods **) 
1067 

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

1069 

1070 
local 

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

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

1073 
in 

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

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

1076 
end; 

1077 

1078 

1079 
(* METHOD_CLASET' *) 

5841  1080 

8098  1081 
fun METHOD_CLASET' tac ctxt = 
8671  1082 
Method.METHOD (HEADGOAL o tac (get_local_claset ctxt)); 
7230  1083 

1084 

1085 
val trace_rules = ref false; 

5841  1086 

7230  1087 
local 
1088 

1089 
fun trace rules i = 

1090 
if not (! trace_rules) then () 

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

1092 
(map Display.pretty_thm rules)); 

1093 

1094 

5841  1095 
fun order_rules xs = map snd (Tactic.orderlist xs); 
1096 

1097 
fun find_rules concl nets = 

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

1099 
in flat (map rules_of nets) end; 

1100 

1101 
fun find_erules [] _ = [] 

6955  1102 
 find_erules (fact :: _) nets = 
5841  1103 
let 
6502  1104 
fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; 
6955  1105 
fun erules_of (_, enet) = order_rules (may_unify enet fact); 
6502  1106 
in flat (map erules_of nets) end; 
5841  1107 

1108 

7230  1109 
fun some_rule_tac cs facts = 
5841  1110 
let 
7230  1111 
val nets = get_nets cs; 
6492  1112 
val erules = find_erules facts nets; 
5841  1113 

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

1115 
let 

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

1117 
val rules = erules @ irules; 

7425  1118 
val ruleq = Method.multi_resolves facts rules; 
7230  1119 
in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); 
5841  1120 
in tac end; 
1121 

7281  1122 
fun rule_tac [] cs facts = some_rule_tac cs facts 
1123 
 rule_tac rules _ facts = Method.rule_tac rules facts; 

1124 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

1125 
fun default_tac rules ctxt cs facts = 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

1126 
rule_tac rules cs facts ORELSE' 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

1127 
Method.some_rule_tac rules ctxt facts ORELSE' 
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

1128 
AxClass.default_intro_classes_tac facts; 
10309  1129 

7230  1130 
in 
7281  1131 
val rule = METHOD_CLASET' o rule_tac; 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

1132 
fun default rules ctxt = METHOD_CLASET' (default_tac rules ctxt) ctxt; 
7230  1133 
end; 
5841  1134 

1135 

7230  1136 
(* intro / elim methods *) 
1137 

1138 
local 

1139 

7329  1140 
fun intro_elim_tac netpair_of res_tac rules cs facts = 
1141 
let 

8342  1142 
val tac = 
9449  1143 
if null rules then FIRST' (map (bimatch_from_nets_tac o netpair_of) (get_nets cs)) 
7329  1144 
else res_tac rules; 
8342  1145 
in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end; 
6502  1146 

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

7230  1149 

1150 
in 

1151 
val intro = METHOD_CLASET' o intro_tac; 

1152 
val elim = METHOD_CLASET' o elim_tac; 

1153 
end; 

1154 

1155 

1156 
(* contradiction method *) 

6502  1157 

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

1160 

1161 
(* automatic methods *) 

5841  1162 

5927  1163 
val cla_modifiers = 
10034  1164 
[Args.$$$ destN  Args.query_colon >> K ((I, xtra_dest_local):Method.modifier), 
1165 
Args.$$$ destN  Args.bang_colon >> K (I, safe_dest_local), 

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

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

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

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

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

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

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

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

5927  1174 

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

7132  1177 

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

7559  1181 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1182 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1183 

1184 

1185 

1186 
(** setup_methods **) 

1187 

1188 
val setup_methods = Method.add_methods 

10309  1189 
[("default", Method.thms_ctxt_args default, "apply some rule (classical)"), 
9441  1190 
("rule", Method.thms_ctxt_args rule, "apply some rule (classical)"), 
6502  1191 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
8098  1192 
("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"), 
1193 
("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"), 

10185  1194 
("clarify", cla_method' (CHANGED oo clarify_tac), "repeatedly apply safe steps"), 
7004  1195 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1196 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1197 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
1198 
("safe", cla_method safe_tac, "classical prover (apply safe rules)")]; 

5841  1199 

1200 

1201 

1202 
(** theory setup **) 

1203 

7354  1204 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1205 

1206 

8667  1207 

1208 
(** outer syntax **) 

1209 

1210 
val print_clasetP = 

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

1212 
OuterSyntax.Keyword.diag 

9513  1213 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1214 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1215 

1216 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1217 

1218 

5841  1219 
end; 