author  wenzelm 
Tue, 12 Sep 2000 17:38:49 +0200  
changeset 9938  cb6a7572d0a1 
parent 9899  5a9081c3b869 
child 9941  fe05af7ec816 
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*) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

18 
infix 4 addSIs addSEs addSDs addIs addEs addDs 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 

59 
val delrules : claset * thm list > claset 

60 
val addSWrapper : claset * (string * wrapper) > claset 

61 
val delSWrapper : claset * string > claset 

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

63 
val delWrapper : claset * string > claset 

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

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

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

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

5523  68 
val addD2 : claset * (string * thm) > claset 
69 
val addE2 : claset * (string * thm) > claset 

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

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

9938  72 
val appSWrappers : claset > wrapper 
73 
val appWrappers : claset > wrapper 

74 
val trace_rules : bool ref 

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

75 

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

76 
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

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

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

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

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

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

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

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

84 

9938  85 
val fast_tac : claset > int > tactic 
86 
val slow_tac : claset > int > tactic 

87 
val weight_ASTAR : int ref 

88 
val astar_tac : claset > int > tactic 

89 
val slow_astar_tac : claset > int > tactic 

90 
val best_tac : claset > int > tactic 

91 
val first_best_tac : claset > int > tactic 

92 
val slow_best_tac : claset > int > tactic 

93 
val depth_tac : claset > int > int > tactic 

94 
val deepen_tac : claset > int > int > tactic 

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

95 

9938  96 
val contr_tac : int > tactic 
97 
val dup_elim : thm > thm 

98 
val dup_intr : thm > thm 

99 
val dup_step_tac : claset > int > tactic 

100 
val eq_mp_tac : int > tactic 

101 
val haz_step_tac : claset > int > tactic 

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

103 
val mp_tac : int > tactic 

104 
val safe_tac : claset > tactic 

105 
val safe_steps_tac : claset > int > tactic 

106 
val safe_step_tac : claset > int > tactic 

107 
val clarify_tac : claset > int > tactic 

108 
val clarify_step_tac : claset > int > tactic 

109 
val step_tac : claset > int > tactic 

110 
val slow_step_tac : claset > int > tactic 

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

112 
val swapify : thm list > thm list 

113 
val swap_res_tac : thm list > int > tactic 

114 
val inst_step_tac : claset > int > tactic 

115 
val inst0_step_tac : claset > int > tactic 

116 
val instp_step_tac : claset > int > tactic 

1724  117 

9938  118 
val AddDs : thm list > unit 
119 
val AddEs : thm list > unit 

120 
val AddIs : thm list > unit 

121 
val AddSDs : thm list > unit 

122 
val AddSEs : thm list > unit 

123 
val AddSIs : thm list > unit 

124 
val AddXDs : thm list > unit 

125 
val AddXEs : thm list > unit 

126 
val AddXIs : thm list > unit 

127 
val Delrules : thm list > unit 

128 
val Safe_tac : tactic 

129 
val Safe_step_tac : int > tactic 

130 
val Clarify_tac : int > tactic 

131 
val Clarify_step_tac : int > tactic 

132 
val Step_tac : int > tactic 

133 
val Fast_tac : int > tactic 

134 
val Best_tac : int > tactic 

135 
val Slow_tac : int > tactic 

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

138 
end; 
1724  139 

5841  140 
signature CLASSICAL = 
141 
sig 

142 
include BASIC_CLASSICAL 

143 
val print_local_claset: Proof.context > unit 

144 
val get_local_claset: Proof.context > claset 

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

146 
val safe_dest_global: theory attribute 

147 
val safe_elim_global: theory attribute 

148 
val safe_intro_global: theory attribute 

6955  149 
val haz_dest_global: theory attribute 
150 
val haz_elim_global: theory attribute 

151 
val haz_intro_global: theory attribute 

152 
val xtra_dest_global: theory attribute 

153 
val xtra_elim_global: theory attribute 

154 
val xtra_intro_global: theory attribute 

9938  155 
val rule_del_global: theory attribute 
6955  156 
val safe_dest_local: Proof.context attribute 
157 
val safe_elim_local: Proof.context attribute 

158 
val safe_intro_local: Proof.context attribute 

5885  159 
val haz_dest_local: Proof.context attribute 
160 
val haz_elim_local: Proof.context attribute 

161 
val haz_intro_local: Proof.context attribute 

6955  162 
val xtra_dest_local: Proof.context attribute 
163 
val xtra_elim_local: Proof.context attribute 

164 
val xtra_intro_local: Proof.context attribute 

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

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

5841  171 
val setup: (theory > theory) list 
172 
end; 

173 

0  174 

5927  175 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  176 
struct 
177 

7354  178 
local open Data in 
0  179 

1800  180 
(*** Useful tactics for classical reasoning ***) 
0  181 

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

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

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

188 
val contr_tac = eresolve_tac [not_elim] THEN' 

189 
(eq_assume_tac ORELSE' assume_tac); 

0  190 

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

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

192 
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

193 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  194 

195 
(*Like mp_tac but instantiates no variables*) 

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

196 
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

197 

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

0  200 

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

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

203 

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

205 
trying rules in order. *) 

206 
fun swap_res_tac rls = 

54  207 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
9938  208 
in assume_tac ORELSE' 
209 
contr_tac ORELSE' 

54  210 
biresolve_tac (foldr addrl (rls,[])) 
0  211 
end; 
212 

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

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

214 
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

215 

6967  216 
fun dup_elim th = 
217 
(case try 

218 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

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

220 
Some th' => th' 

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

0  222 

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

223 

1800  224 
(**** Classical rule sets ****) 
0  225 

226 
datatype claset = 

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

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

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

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

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

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

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

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

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

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

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

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

0  240 

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

241 
(*Desired invariants are 
9938  242 
safe0_netpair = build safe0_brls, 
243 
safep_netpair = build safep_brls, 

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

245 
dup_netpair = build (joinrules(map dup_intr hazIs, 

246 
map dup_elim hazEs)), 

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

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

248 

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

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

250 
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

251 
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

252 
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

253 
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

254 
*) 
0  255 

6502  256 
val empty_netpair = (Net.empty, Net.empty); 
257 

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

258 
val empty_cs = 
9938  259 
CS{safeIs = [], 
260 
safeEs = [], 

261 
hazIs = [], 

262 
hazEs = [], 

263 
xtraIs = [], 

264 
xtraEs = [], 

4651  265 
swrappers = [], 
266 
uwrappers = [], 

6502  267 
safe0_netpair = empty_netpair, 
268 
safep_netpair = empty_netpair, 

269 
haz_netpair = empty_netpair, 

6955  270 
dup_netpair = empty_netpair, 
271 
xtra_netpair = empty_netpair}; 

0  272 

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

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

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

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

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

8727  281 
> Pretty.chunks > Pretty.writeln 
3546  282 
end; 
0  283 

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

285 

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

288 
in 

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

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

291 
end; 

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

292 

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

293 

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

295 

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

296 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  297 
***) 
0  298 

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

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

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

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

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

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

304 

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

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

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

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

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

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

311 

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

313 

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

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

315 
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

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

317 
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

318 

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

320 

1800  321 
val delete = delete_tagged_list o joinrules; 
322 

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

323 
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

324 
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

325 

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

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

327 
is still allowed.*) 
6955  328 
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

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

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

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

335 
else if mem_thm (th, hazEs) then 
9760  336 
warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th) 
6955  337 
else if mem_thm (th, xtraIs) then 
9408  338 
warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th) 
6955  339 
else if mem_thm (th, xtraEs) then 
9408  340 
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

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

342 

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

344 

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

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

348 
if mem_thm (th, safeIs) then 
9938  349 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); 
350 
cs) 

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

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

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

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

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

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

358 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  359 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
360 
safeEs = safeEs, 

361 
hazIs = hazIs, 

362 
hazEs = hazEs, 

363 
xtraIs = xtraIs, 

364 
xtraEs = xtraEs, 

365 
swrappers = swrappers, 

366 
uwrappers = uwrappers, 

367 
haz_netpair = haz_netpair, 

368 
dup_netpair = dup_netpair, 

369 
xtra_netpair = xtra_netpair} 

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

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

371 

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

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

375 
if mem_thm (th, safeEs) then 
9938  376 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); 
377 
cs) 

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

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

379 
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

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

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

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

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

385 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  386 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
387 
safeIs = safeIs, 

388 
hazIs = hazIs, 

389 
hazEs = hazEs, 

390 
xtraIs = xtraIs, 

391 
xtraEs = xtraEs, 

392 
swrappers = swrappers, 

393 
uwrappers = uwrappers, 

394 
haz_netpair = haz_netpair, 

395 
dup_netpair = dup_netpair, 

396 
xtra_netpair = xtra_netpair} 

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

397 
end; 
0  398 

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

399 
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

400 

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

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

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

403 

9938  404 
fun cs addSDs ths = cs addSEs (map Data.make_elim ths); 
0  405 

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

406 

1800  407 
(*** Hazardous (unsafe) rules ***) 
0  408 

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

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

412 
if mem_thm (th, hazIs) then 
9938  413 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
414 
cs) 

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

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

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

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

418 
in warn_dup th cs; 
9938  419 
CS{hazIs = th::hazIs, 
420 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 

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

422 
safeIs = safeIs, 

423 
safeEs = safeEs, 

424 
hazEs = hazEs, 

425 
xtraIs = xtraIs, 

426 
xtraEs = xtraEs, 

427 
swrappers = swrappers, 

428 
uwrappers = uwrappers, 

429 
safe0_netpair = safe0_netpair, 

430 
safep_netpair = safep_netpair, 

431 
xtra_netpair = xtra_netpair} 

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

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

433 

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

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

437 
if mem_thm (th, hazEs) then 
9938  438 
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); 
439 
cs) 

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

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

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

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

443 
in warn_dup th cs; 
9938  444 
CS{hazEs = th::hazEs, 
445 
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, 

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

447 
safeIs = safeIs, 

448 
safeEs = safeEs, 

449 
hazIs = hazIs, 

450 
xtraIs = xtraIs, 

451 
xtraEs = xtraEs, 

452 
swrappers = swrappers, 

453 
uwrappers = uwrappers, 

454 
safe0_netpair = safe0_netpair, 

455 
safep_netpair = safep_netpair, 

456 
xtra_netpair = xtra_netpair} 

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

457 
end; 
0  458 

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

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

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

461 

9938  462 
fun cs addDs ths = cs addEs (map Data.make_elim ths); 
0  463 

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

464 

6955  465 
(*** Extra (single step) rules ***) 
466 

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

9938  468 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
469 
th)= 

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

6955  473 
else 
474 
let val nI = length xtraIs + 1 

475 
and nE = length xtraEs 

476 
in warn_dup th cs; 

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

479 
safeIs = safeIs, 

480 
safeEs = safeEs, 

481 
hazIs = hazIs, 

482 
hazEs = hazEs, 

483 
xtraEs = xtraEs, 

484 
swrappers = swrappers, 

485 
uwrappers = uwrappers, 

486 
safe0_netpair = safe0_netpair, 

487 
safep_netpair = safep_netpair, 

488 
haz_netpair = haz_netpair, 

489 
dup_netpair = dup_netpair} 

6955  490 
end; 
491 

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

9938  493 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
494 
th) = 

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

6955  498 
else 
499 
let val nI = length xtraIs 

500 
and nE = length xtraEs + 1 

501 
in warn_dup th cs; 

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

504 
safeIs = safeIs, 

505 
safeEs = safeEs, 

506 
hazIs = hazIs, 

507 
hazEs = hazEs, 

508 
xtraIs = xtraIs, 

509 
swrappers = swrappers, 

510 
uwrappers = uwrappers, 

511 
safe0_netpair = safe0_netpair, 

512 
safep_netpair = safep_netpair, 

513 
haz_netpair = haz_netpair, 

514 
dup_netpair = dup_netpair} 

6955  515 
end; 
516 

517 
infix 4 addXIs addXEs addXDs; 

518 

519 
val op addXIs = rev_foldl addXI; 

520 
val op addXEs = rev_foldl addXE; 

521 

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

524 

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

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

528 
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

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

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

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

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

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

540 
safeEs = safeEs, 

541 
hazIs = hazIs, 

542 
hazEs = hazEs, 

543 
xtraIs = xtraIs, 

544 
xtraEs = xtraEs, 

545 
swrappers = swrappers, 

546 
uwrappers = uwrappers, 

547 
haz_netpair = haz_netpair, 

548 
dup_netpair = dup_netpair, 

549 
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

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

551 
else cs; 
1800  552 

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

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

556 
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

557 
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

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

561 
safeEs = rem_thm (safeEs,th), 

562 
hazIs = hazIs, 

563 
hazEs = hazEs, 

564 
xtraIs = xtraIs, 

565 
xtraEs = xtraEs, 

566 
swrappers = swrappers, 

567 
uwrappers = uwrappers, 

568 
haz_netpair = haz_netpair, 

569 
dup_netpair = dup_netpair, 

570 
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

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

572 
else cs; 
1800  573 

574 

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

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

578 
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

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

582 
safeEs = safeEs, 

583 
hazIs = rem_thm (hazIs,th), 

584 
hazEs = hazEs, 

585 
xtraIs = xtraIs, 

586 
xtraEs = xtraEs, 

587 
swrappers = swrappers, 

588 
uwrappers = uwrappers, 

589 
safe0_netpair = safe0_netpair, 

590 
safep_netpair = safep_netpair, 

591 
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

592 
else cs; 
1800  593 

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

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

597 
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

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

601 
safeEs = safeEs, 

602 
hazIs = hazIs, 

603 
hazEs = rem_thm (hazEs,th), 

604 
xtraIs = xtraIs, 

605 
xtraEs = xtraEs, 

606 
swrappers = swrappers, 

607 
uwrappers = uwrappers, 

608 
safe0_netpair = safe0_netpair, 

609 
safep_netpair = safep_netpair, 

610 
xtra_netpair = xtra_netpair} 

6955  611 
else cs; 
612 

613 

614 
fun delXI th 

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

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

9938  619 
safeIs = safeIs, 
620 
safeEs = safeEs, 

621 
hazIs = hazIs, 

622 
hazEs = hazEs, 

623 
xtraIs = rem_thm (xtraIs,th), 

624 
xtraEs = xtraEs, 

625 
swrappers = swrappers, 

626 
uwrappers = uwrappers, 

627 
safe0_netpair = safe0_netpair, 

628 
safep_netpair = safep_netpair, 

629 
haz_netpair = haz_netpair, 

630 
dup_netpair = dup_netpair} 

6955  631 
else cs; 
632 

633 
fun delXE th 

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

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

9938  638 
safeIs = safeIs, 
639 
safeEs = safeEs, 

640 
hazIs = hazIs, 

641 
hazEs = hazEs, 

642 
xtraIs = xtraIs, 

643 
xtraEs = rem_thm (xtraEs,th), 

644 
swrappers = swrappers, 

645 
uwrappers = uwrappers, 

646 
safe0_netpair = safe0_netpair, 

647 
safep_netpair = safep_netpair, 

648 
haz_netpair = haz_netpair, 

649 
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

650 
else cs; 
1800  651 

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

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

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

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

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

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

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

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

662 
end; 

1800  663 

664 
val op delrules = foldl delrule; 

665 

666 

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

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

668 
fun update_swrappers 
6955  669 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
670 
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

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

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

674 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  675 
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

676 

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

677 
fun update_uwrappers 
6955  678 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
679 
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

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

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

683 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  684 
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

685 

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

686 

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

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

4651  691 

692 
(*Add/replace an unsafe wrapper*) 

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

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

696 

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

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

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

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

702 

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

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

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

706 
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

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

708 

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

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

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

714 

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

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

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

720 

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

723 
fun cs addE2 (name, thm) = 

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

725 
fun cs addSD2 (name, thm) = 

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

727 
fun cs addSE2 (name, thm) = 

728 
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

729 

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

732 
treatment of priority might get muddled up.*) 

733 
fun merge_cs 

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

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

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

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

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

746 
addEs hazEs' 

747 
addXIs xtraIs' 

748 
addXEs xtraEs' 

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

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

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

751 
in cs3 
1711  752 
end; 
753 

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

754 

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

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

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

762 
bimatch_from_nets_tac safe0_netpair, 

763 
FIRST' hyp_subst_tacs, 

764 
bimatch_from_nets_tac safep_netpair]); 

0  765 

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

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

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

772 

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

773 

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

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

775 

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

776 
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

777 

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

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

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

780 
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

781 
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

782 

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

783 
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

784 
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

785 

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

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

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

788 
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

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

790 

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

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

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

796 
FIRST' hyp_subst_tacs, 

797 
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

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

799 

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

800 
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

801 

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

804 

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

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

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

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

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

811 

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

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

814 
biresolve_from_nets_tac safep_netpair; 
0  815 

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

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

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

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

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

821 

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

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

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

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

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

833 
(*Dumb but fast*) 

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

835 

836 
(*Slower but smarter than fast_tac*) 

837 
fun best_tac cs = 

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

839 

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

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

843 

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

846 
fun slow_best_tac cs = 

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

848 

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

849 

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

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

852 

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

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

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

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

857 

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

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

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

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

862 

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

864 
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

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

867 

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

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

869 
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

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

871 
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

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

873 

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

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

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

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

5757  883 
)) i state; 
884 
end; 

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

885 

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

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

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

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

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

894 
[] => DETERM 

895 
 _::_ => I 

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

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

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

899 

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

900 
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

901 

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

902 

1724  903 

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

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

905 

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

7354  908 
structure GlobalClasetArgs = 
909 
struct 

910 
val name = "Provers/claset"; 

911 
type T = claset ref; 

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

912 

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

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

918 
end; 

1724  919 

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

922 
val claset_ref_of_sg = GlobalClaset.get_sg; 

923 
val claset_ref_of = GlobalClaset.get; 

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

924 

1724  925 

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

926 
(* access claset *) 
1724  927 

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

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

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

933 

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

936 

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

937 

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

938 
(* change claset *) 
1800  939 

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

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

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

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

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

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

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

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

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

950 
val AddXIs = change_claset (op addXIs); 

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

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

952 

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

953 

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

956 
structure LocalClasetArgs = 

957 
struct 

958 
val name = "Provers/claset"; 

959 
type T = claset; 

960 
val init = claset_of; 

961 
fun print _ cs = print_cs cs; 

962 
end; 

963 

964 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

965 
val print_local_claset = LocalClaset.print; 

966 
val get_local_claset = LocalClaset.get; 

967 
val put_local_claset = LocalClaset.put; 

968 

969 

5885  970 
(* attributes *) 
971 

972 
fun change_global_cs f (thy, th) = 

973 
let val r = claset_ref_of thy 

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

976 
fun change_local_cs f (ctxt, th) = 

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

980 
val safe_dest_global = change_global_cs (op addSDs); 

981 
val safe_elim_global = change_global_cs (op addSEs); 

982 
val safe_intro_global = change_global_cs (op addSIs); 

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

985 
val haz_intro_global = change_global_cs (op addIs); 

986 
val xtra_dest_global = change_global_cs (op addXDs); 

987 
val xtra_elim_global = change_global_cs (op addXEs); 

988 
val xtra_intro_global = change_global_cs (op addXIs); 

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

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

993 
val safe_intro_local = change_local_cs (op addSIs); 

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

996 
val haz_intro_local = change_local_cs (op addIs); 

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

999 
val xtra_intro_local = change_local_cs (op addXIs); 

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

1002 

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

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

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

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

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

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

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

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

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

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

2066  1016 

1800  1017 

0  1018 
end; 
5841  1019 

1020 

1021 

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

1024 
(* add / del rules *) 

1025 

1026 
val introN = "intro"; 

1027 
val elimN = "elim"; 

1028 
val destN = "dest"; 

9938  1029 
val ruleN = "rule"; 
5841  1030 
val delN = "del"; 
1031 

8382  1032 
val colon = Args.$$$ ":"; 
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8168
diff
changeset

1033 
val query = Args.$$$ "?"; 
9408  1034 
val bang = Args.$$$ "!"; 
8382  1035 
val query_colon = Args.$$$ "?:"; 
9408  1036 
val bang_colon = Args.$$$ "!:"; 
5841  1037 

6955  1038 
fun cla_att change xtra haz safe = Attrib.syntax 
9563
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

1039 
(Scan.lift ((query >> K xtra  bang >> K safe  Scan.succeed haz) >> change)); 
5841  1040 

6955  1041 
fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); 
9938  1042 

1043 
fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ delN) >> K att); 

1044 
val rule_del_attr = (del_args rule_del_global, del_args rule_del_local); 

5841  1045 

1046 

1047 
(* setup_attrs *) 

1048 

9938  1049 
fun elimified x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x; 
9184  1050 

5841  1051 
val setup_attrs = Attrib.add_attributes 
9899  1052 
[("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"), 
1053 
(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"), 

1054 
(elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"), 

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

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

1058 

1059 

7230  1060 
(** proof methods **) 
1061 

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

1063 

1064 
local 

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

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

1067 
in 

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

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

1070 
end; 

1071 

1072 

1073 
(* METHOD_CLASET' *) 

5841  1074 

8098  1075 
fun METHOD_CLASET' tac ctxt = 
8671  1076 
Method.METHOD (HEADGOAL o tac (get_local_claset ctxt)); 
7230  1077 

1078 

1079 
val trace_rules = ref false; 

5841  1080 

7230  1081 
local 
1082 

1083 
fun trace rules i = 

1084 
if not (! trace_rules) then () 

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

1086 
(map Display.pretty_thm rules)); 

1087 

1088 

5841  1089 
fun order_rules xs = map snd (Tactic.orderlist xs); 
1090 

1091 
fun find_rules concl nets = 

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

1093 
in flat (map rules_of nets) end; 

1094 

1095 
fun find_erules [] _ = [] 

6955  1096 
 find_erules (fact :: _) nets = 
5841  1097 
let 
6502  1098 
fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; 
6955  1099 
fun erules_of (_, enet) = order_rules (may_unify enet fact); 
6502  1100 
in flat (map erules_of nets) end; 
5841  1101 

1102 

7230  1103 
fun some_rule_tac cs facts = 
5841  1104 
let 
7230  1105 
val nets = get_nets cs; 
6492  1106 
val erules = find_erules facts nets; 
5841  1107 

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

1109 
let 

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

1111 
val rules = erules @ irules; 

7425  1112 
val ruleq = Method.multi_resolves facts rules; 
7230  1113 
in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); 
5841  1114 
in tac end; 
1115 

7281  1116 
fun rule_tac [] cs facts = some_rule_tac cs facts 
1117 
 rule_tac rules _ facts = Method.rule_tac rules facts; 

1118 

7230  1119 
in 
7281  1120 
val rule = METHOD_CLASET' o rule_tac; 
7230  1121 
end; 
5841  1122 

1123 

7230  1124 
(* intro / elim methods *) 
1125 

1126 
local 

1127 

7329  1128 
fun intro_elim_tac netpair_of res_tac rules cs facts = 
1129 
let 

8342  1130 
val tac = 
9449  1131 
if null rules then FIRST' (map (bimatch_from_nets_tac o netpair_of) (get_nets cs)) 
7329  1132 
else res_tac rules; 
8342  1133 
in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end; 
6502  1134 

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

7230  1137 

1138 
in 

1139 
val intro = METHOD_CLASET' o intro_tac; 

1140 
val elim = METHOD_CLASET' o elim_tac; 

1141 
end; 

1142 

1143 

1144 
(* contradiction method *) 

6502  1145 

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

1148 

1149 
(* automatic methods *) 

5841  1150 

5927  1151 
val cla_modifiers = 
9408  1152 
[Args.$$$ destN  query_colon >> K ((I, xtra_dest_local):Method.modifier), 
9563
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

1153 
Args.$$$ destN  bang_colon >> K (I, safe_dest_local), 
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

1154 
Args.$$$ destN  colon >> K (I, haz_dest_local), 
9408  1155 
Args.$$$ elimN  query_colon >> K (I, xtra_elim_local), 
9563
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

1156 
Args.$$$ elimN  bang_colon >> K (I, safe_elim_local), 
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

1157 
Args.$$$ elimN  colon >> K (I, haz_elim_local), 
9408  1158 
Args.$$$ introN  query_colon >> K (I, xtra_intro_local), 
9563
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

1159 
Args.$$$ introN  bang_colon >> K (I, safe_intro_local), 
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset

1160 
Args.$$$ introN  colon >> K (I, haz_intro_local), 
9938  1161 
Args.$$$ delN  colon >> K (I, rule_del_local)]; 
5927  1162 

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

7132  1165 

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

7559  1169 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1170 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1171 

1172 

1173 

1174 
(** setup_methods **) 

1175 

1176 
val setup_methods = Method.add_methods 

9441  1177 
[("default", Method.thms_ctxt_args rule, "apply some rule (classical)"), 
1178 
("rule", Method.thms_ctxt_args rule, "apply some rule (classical)"), 

6502  1179 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
8098  1180 
("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"), 
1181 
("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"), 

9441  1182 
("clarify", cla_method' clarify_tac, "repeatedly apply safe steps"), 
7004  1183 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1184 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1185 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
1186 
("safe", cla_method safe_tac, "classical prover (apply safe rules)")]; 

5841  1187 

1188 

1189 

1190 
(** theory setup **) 

1191 

7354  1192 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1193 

1194 

8667  1195 

1196 
(** outer syntax **) 

1197 

1198 
val print_clasetP = 

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

1200 
OuterSyntax.Keyword.diag 

9513  1201 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1202 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1203 

1204 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1205 

1206 

5841  1207 
end; 