author  wenzelm 
Sat, 08 Oct 2005 20:15:34 +0200  
changeset 17795  5b18c3343028 
parent 17257  0ab67cb765da 
child 17880  4494c023bf2a 
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*) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

18 
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules 
4651  19 
addSWrapper delSWrapper addWrapper delWrapper 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

20 
addSbefore addSafter addbefore addafter 
5523  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, 
10736  47 
swrappers: (string * wrapper) list, 
9938  48 
uwrappers: (string * wrapper) list, 
49 
safe0_netpair: netpair, safep_netpair: netpair, 

12401  50 
haz_netpair: netpair, dup_netpair: netpair, 
51 
xtra_netpair: ContextRules.netpair} 

9938  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 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

65 
val addSafter : claset * (string * (int > tactic)) > claset 
9938  66 
val addbefore : claset * (string * (int > tactic)) > claset 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

67 
val addafter : 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 

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

74 

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

75 
val claset_ref_of: theory > claset ref 
16424  76 
val claset_ref_of_sg: theory > claset ref (*obsolete*) 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

77 
val claset_of: theory > claset 
16424  78 
val claset_of_sg: theory > claset (*obsolete*) 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

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

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

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

82 
val claset_ref: unit > claset ref 
15036  83 
val local_claset_of : Proof.context > claset 
4079
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 Delrules : thm list > unit 

125 
val Safe_tac : tactic 

126 
val Safe_step_tac : int > tactic 

127 
val Clarify_tac : int > tactic 

128 
val Clarify_step_tac : int > tactic 

129 
val Step_tac : int > tactic 

130 
val Fast_tac : int > tactic 

131 
val Best_tac : int > tactic 

132 
val Slow_tac : int > tactic 

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

135 
end; 
1724  136 

5841  137 
signature CLASSICAL = 
138 
sig 

139 
include BASIC_CLASSICAL 

15036  140 
val add_context_safe_wrapper: string * (Proof.context > wrapper) > theory > theory 
141 
val del_context_safe_wrapper: string > theory > theory 

142 
val add_context_unsafe_wrapper: string * (Proof.context > wrapper) > theory > theory 

143 
val del_context_unsafe_wrapper: string > theory > theory 

5841  144 
val print_local_claset: Proof.context > unit 
145 
val get_local_claset: Proof.context > claset 

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

147 
val safe_dest_global: theory attribute 

148 
val safe_elim_global: theory attribute 

149 
val safe_intro_global: theory attribute 

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

152 
val haz_intro_global: theory attribute 

9938  153 
val rule_del_global: theory attribute 
6955  154 
val safe_dest_local: Proof.context attribute 
155 
val safe_elim_local: Proof.context attribute 

156 
val safe_intro_local: Proof.context attribute 

5885  157 
val haz_dest_local: Proof.context attribute 
158 
val haz_elim_local: Proof.context attribute 

159 
val haz_intro_local: Proof.context attribute 

9938  160 
val rule_del_local: Proof.context attribute 
7272  161 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  162 
val cla_meth: (claset > tactic) > thm list > Proof.context > Proof.method 
163 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 

15703  164 
val cla_method: (claset > tactic) > Method.src > Proof.context > Proof.method 
165 
val cla_method': (claset > int > tactic) > Method.src > Proof.context > Proof.method 

5841  166 
val setup: (theory > theory) list 
167 
end; 

168 

0  169 

5927  170 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  171 
struct 
172 

7354  173 
local open Data in 
0  174 

1800  175 
(*** Useful tactics for classical reasoning ***) 
0  176 

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

10736  180 
(*Prove goal that assumes both P and ~P. 
4392  181 
No backtracking if it finds an equal assumption. Perhaps should call 
182 
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) 

10736  183 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  184 
(eq_assume_tac ORELSE' assume_tac); 
0  185 

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

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

187 
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

188 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  189 

190 
(*Like mp_tac but instantiates no variables*) 

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

191 
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

192 

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

0  195 

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

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

12401  198 
fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x; 
0  199 

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

201 
trying rules in order. *) 

10736  202 
fun swap_res_tac rls = 
54  203 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
10736  204 
in assume_tac ORELSE' 
205 
contr_tac ORELSE' 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

206 
biresolve_tac (foldr addrl [] rls) 
0  207 
end; 
208 

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

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

210 
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

211 

6967  212 
fun dup_elim th = 
13525  213 
(case try (fn () => 
214 
rule_by_tactic (TRYALL (etac revcut_rl)) 

17257
0ab67cb765da
introduced binding priority 1 for linear combinators etc.
haftmann
parents:
17084
diff
changeset

215 
((th RSN (2, revcut_rl)) > assumption 2 > Seq.hd)) () of 
15531  216 
SOME th' => th' 
6967  217 
 _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); 
0  218 

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

219 

1800  220 
(**** Classical rule sets ****) 
0  221 

222 
datatype claset = 

12401  223 
CS of {safeIs : thm list, (*safe introduction rules*) 
224 
safeEs : thm list, (*safe elimination rules*) 

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

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

227 
swrappers : (string * wrapper) list, (*for transforming safe_step_tac*) 

9938  228 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  229 
safe0_netpair : netpair, (*nets for trivial cases*) 
230 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

233 
xtra_netpair : ContextRules.netpair}; (*nets for extra rules*) 

0  234 

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

235 
(*Desired invariants are 
9938  236 
safe0_netpair = build safe0_brls, 
237 
safep_netpair = build safep_brls, 

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

10736  239 
dup_netpair = build (joinrules(map dup_intr hazIs, 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

240 
map dup_elim hazEs)) 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

241 

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

243 
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

244 
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

245 
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

246 
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

247 
*) 
0  248 

6502  249 
val empty_netpair = (Net.empty, Net.empty); 
250 

10736  251 
val empty_cs = 
9938  252 
CS{safeIs = [], 
253 
safeEs = [], 

254 
hazIs = [], 

255 
hazEs = [], 

4651  256 
swrappers = [], 
257 
uwrappers = [], 

6502  258 
safe0_netpair = empty_netpair, 
259 
safep_netpair = empty_netpair, 

260 
haz_netpair = empty_netpair, 

6955  261 
dup_netpair = empty_netpair, 
262 
xtra_netpair = empty_netpair}; 

0  263 

15036  264 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) = 
3546  265 
let val pretty_thms = map Display.pretty_thm in 
9760  266 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 
267 
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), 

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

15036  269 
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), 
270 
Pretty.strs ("safe wrappers:" :: map #1 swrappers), 

271 
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] 

8727  272 
> Pretty.chunks > Pretty.writeln 
3546  273 
end; 
0  274 

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

276 

10736  277 
local 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

278 
fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l; 
10736  279 
in 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

280 
fun appSWrappers (CS{swrappers,...}) = wrap swrappers; 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

281 
fun appWrappers (CS{uwrappers,...}) = wrap uwrappers; 
4651  282 
end; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

283 

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

284 

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

286 

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

287 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  288 
***) 
0  289 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

290 
(*For use with biresolve_tac. Combines intro rules with swap to handle negated 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

291 
assumptions. Pairs elim rules with true. *) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

292 
fun joinrules (intrs, elims) = 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

293 
(map (pair true) (elims @ swapify intrs) @ map (pair false) intrs); 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

294 

12401  295 
fun joinrules' (intrs, elims) = 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

297 

10736  298 
(*Priority: prefer rules with fewest subgoals, 
1231  299 
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

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

301 
 tag_brls k (brl::brls) = 
10736  302 
(1000000*subgoals_of_brl brl + k, brl) :: 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

304 

12401  305 
fun tag_brls' _ _ [] = [] 
306 
 tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; 

10736  307 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

308 
fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

309 

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

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

311 
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

312 
new insertions the lowest priority.*) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

313 
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 
12401  314 
fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules'; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

315 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

316 
fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls; 
12362  317 
fun delete x = delete_tagged_list (joinrules x); 
12401  318 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  319 

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

320 
val mem_thm = gen_mem Drule.eq_thm_prop 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

321 
and rem_thm = gen_rem Drule.eq_thm_prop; 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

322 

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

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

324 
is still allowed.*) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

325 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
10736  326 
if mem_thm (th, safeIs) then 
9938  327 
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

328 
else if mem_thm (th, safeEs) then 
9408  329 
warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) 
10736  330 
else if mem_thm (th, hazIs) then 
9760  331 
warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) 
10736  332 
else if mem_thm (th, hazEs) then 
9760  333 
warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

335 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

336 

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

338 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

339 
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  340 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
341 
th) = 

10736  342 
if mem_thm (th, safeIs) then 
9938  343 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); 
344 
cs) 

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

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

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

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

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

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

352 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  353 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
354 
safeEs = safeEs, 

355 
hazIs = hazIs, 

356 
hazEs = hazEs, 

357 
swrappers = swrappers, 

358 
uwrappers = uwrappers, 

359 
haz_netpair = haz_netpair, 

360 
dup_netpair = dup_netpair, 

12401  361 
xtra_netpair = insert' 0 (nI,nE) ([th], []) xtra_netpair} 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

363 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

364 
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  365 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
366 
th) = 

10736  367 
if mem_thm (th, safeEs) then 
9938  368 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); 
369 
cs) 

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

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

371 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
15570  372 
List.partition (fn rl => nprems_of rl=1) [th] 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

377 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  378 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
379 
safeIs = safeIs, 

380 
hazIs = hazIs, 

381 
hazEs = hazEs, 

382 
swrappers = swrappers, 

383 
uwrappers = uwrappers, 

384 
haz_netpair = haz_netpair, 

385 
dup_netpair = dup_netpair, 

12401  386 
xtra_netpair = insert' 0 (nI,nE) ([], [th]) xtra_netpair} 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

387 
end; 
0  388 

15570  389 
fun rev_foldl f (e, l) = Library.foldl f (e, rev l); 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

390 

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

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

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

393 

17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

394 
(*Give new theorem a name, if it has one already.*) 
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

395 
fun name_make_elim th = 
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

396 
case Thm.name_of_thm th of 
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

397 
"" => Data.make_elim th 
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

398 
 a => Thm.name_thm (a ^ "_dest", Data.make_elim th); 
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

399 

fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

400 
fun cs addSDs ths = cs addSEs (map name_make_elim ths); 
0  401 

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

402 

1800  403 
(*** Hazardous (unsafe) rules ***) 
0  404 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

405 
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  406 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
407 
th)= 

10736  408 
if mem_thm (th, hazIs) then 
9938  409 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
410 
cs) 

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

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

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

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

414 
in warn_dup th cs; 
9938  415 
CS{hazIs = th::hazIs, 
416 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 

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

10736  418 
safeIs = safeIs, 
9938  419 
safeEs = safeEs, 
420 
hazEs = hazEs, 

421 
swrappers = swrappers, 

422 
uwrappers = uwrappers, 

423 
safe0_netpair = safe0_netpair, 

424 
safep_netpair = safep_netpair, 

12401  425 
xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair} 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

427 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

428 
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  429 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
430 
th) = 

10736  431 
if mem_thm (th, hazEs) then 
9938  432 
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); 
433 
cs) 

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

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

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

437 
in warn_dup th cs; 
9938  438 
CS{hazEs = th::hazEs, 
439 
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, 

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

10736  441 
safeIs = safeIs, 
9938  442 
safeEs = safeEs, 
443 
hazIs = hazIs, 

444 
swrappers = swrappers, 

445 
uwrappers = uwrappers, 

446 
safe0_netpair = safe0_netpair, 

447 
safep_netpair = safep_netpair, 

12401  448 
xtra_netpair = insert' 1 (nI,nE) ([], [th]) xtra_netpair} 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

449 
end; 
0  450 

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

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

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

453 

17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

454 
fun cs addDs ths = cs addEs (map name_make_elim ths); 
0  455 

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

456 

10736  457 
(*** Deletion of rules 
1800  458 
Working out what to delete, requires repeating much of the code used 
9938  459 
to insert. 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

460 
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

461 
searches in all the lists and chooses the relevant delXX functions. 
1800  462 
***) 
463 

10736  464 
fun delSI th 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

465 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  466 
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

467 
if mem_thm (th, safeIs) then 
15570  468 
let val (safe0_rls, safep_rls) = List.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

469 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  470 
safep_netpair = delete (safep_rls, []) safep_netpair, 
471 
safeIs = rem_thm (safeIs,th), 

472 
safeEs = safeEs, 

473 
hazIs = hazIs, 

474 
hazEs = hazEs, 

475 
swrappers = swrappers, 

476 
uwrappers = uwrappers, 

477 
haz_netpair = haz_netpair, 

478 
dup_netpair = dup_netpair, 

12401  479 
xtra_netpair = delete' ([th], []) xtra_netpair} 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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

481 
else cs; 
1800  482 

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

483 
fun delSE th 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

484 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  485 
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

486 
if mem_thm (th, safeEs) then 
15570  487 
let val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th] 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

488 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  489 
safep_netpair = delete ([], safep_rls) safep_netpair, 
490 
safeIs = safeIs, 

491 
safeEs = rem_thm (safeEs,th), 

492 
hazIs = hazIs, 

493 
hazEs = hazEs, 

494 
swrappers = swrappers, 

495 
uwrappers = uwrappers, 

496 
haz_netpair = haz_netpair, 

497 
dup_netpair = dup_netpair, 

12401  498 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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

500 
else cs; 
1800  501 

502 

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

503 
fun delI th 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

504 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  505 
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

506 
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

507 
CS{haz_netpair = delete ([th], []) haz_netpair, 
9938  508 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
10736  509 
safeIs = safeIs, 
9938  510 
safeEs = safeEs, 
511 
hazIs = rem_thm (hazIs,th), 

512 
hazEs = hazEs, 

513 
swrappers = swrappers, 

514 
uwrappers = uwrappers, 

515 
safe0_netpair = safe0_netpair, 

516 
safep_netpair = safep_netpair, 

12401  517 
xtra_netpair = delete' ([th], []) xtra_netpair} 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

518 
else cs; 
1800  519 

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

520 
fun delE th 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

521 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  522 
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

523 
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

524 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
9938  525 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
10736  526 
safeIs = safeIs, 
9938  527 
safeEs = safeEs, 
528 
hazIs = hazIs, 

529 
hazEs = rem_thm (hazEs,th), 

530 
swrappers = swrappers, 

531 
uwrappers = uwrappers, 

532 
safe0_netpair = safe0_netpair, 

533 
safep_netpair = safep_netpair, 

12401  534 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
6955  535 
else cs; 
536 

1800  537 

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

538 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

539 
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) = 
9938  540 
let val th' = Data.make_elim th in 
541 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 

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

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

543 
mem_thm (th', safeEs) orelse mem_thm (th', hazEs) 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

544 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
9938  545 
else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs) 
546 
end; 

1800  547 

15570  548 
val op delrules = Library.foldl delrule; 
1800  549 

550 

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

551 
(*** Modifying the wrapper tacticals ***) 
10736  552 
fun update_swrappers 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

553 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
6955  554 
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

555 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

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

557 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  558 
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

559 

10736  560 
fun update_uwrappers 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

561 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
6955  562 
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

563 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

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

565 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  566 
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

567 

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

568 

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

570 
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => 
9721  571 
overwrite_warn (swrappers, new_swrapper) 
572 
("Overwriting safe wrapper " ^ fst new_swrapper)); 

4651  573 

574 
(*Add/replace an unsafe wrapper*) 

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

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

578 

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

580 
fun cs delSWrapper name = update_swrappers cs (fn swrappers => 
17795  581 
let val swrappers' = filter_out (equal name o fst) swrappers in 
15036  582 
if length swrappers <> length swrappers' then swrappers' 
583 
else (warning ("No such safe wrapper in claset: "^ name); swrappers) 

584 
end); 

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

585 

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

587 
fun cs delWrapper name = update_uwrappers cs (fn uwrappers => 
17795  588 
let val uwrappers' = filter_out (equal name o fst) uwrappers in 
15036  589 
if length uwrappers <> length uwrappers' then uwrappers' 
590 
else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers) 

591 
end); 

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

592 

11168  593 
(* compose a safe tactic alternatively before/after safe_step_tac *) 
10736  594 
fun cs addSbefore (name, tac1) = 
5523  595 
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

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

598 

11168  599 
(*compose a tactic alternatively before/after the step tactic *) 
10736  600 
fun cs addbefore (name, tac1) = 
5523  601 
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

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

604 

10736  605 
fun cs addD2 (name, thm) = 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

606 
cs addafter (name, datac thm 1); 
10736  607 
fun cs addE2 (name, thm) = 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

608 
cs addafter (name, eatac thm 1); 
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

609 
fun cs addSD2 (name, thm) = 
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

610 
cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); 
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

611 
fun cs addSE2 (name, thm) = 
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset

612 
cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

613 

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

616 
treatment of priority might get muddled up.*) 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

617 
fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

618 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) = 
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

619 
let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs) 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

620 
val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs) 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

621 
val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs) 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

622 
val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

623 
val cs1 = cs addSIs safeIs' 
9938  624 
addSEs safeEs' 
625 
addIs hazIs' 

626 
addEs hazEs' 

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

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

628 
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); 
10736  629 
in cs3 
1711  630 
end; 
631 

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

632 

1800  633 
(**** Simple tactics for theorem proving ****) 
0  634 

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

10736  636 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  637 
appSWrappers cs (FIRST' [ 
9938  638 
eq_assume_tac, 
639 
eq_mp_tac, 

640 
bimatch_from_nets_tac safe0_netpair, 

641 
FIRST' hyp_subst_tacs, 

642 
bimatch_from_nets_tac safep_netpair]); 

0  643 

5757  644 
(*Repeatedly attack a subgoal using safe inferences  it's deterministic!*) 
10736  645 
fun safe_steps_tac cs = REPEAT_DETERM1 o 
9938  646 
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); 
5757  647 

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

650 

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

651 

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

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

653 

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

654 
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

655 

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

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

657 
create precisely n subgoals.*) 
10736  658 
fun n_bimatch_from_nets_tac n = 
15570  659 
biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

660 

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

661 
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

662 
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

663 

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

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

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

666 
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

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

668 

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

669 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  670 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  671 
appSWrappers cs (FIRST' [ 
9938  672 
eq_assume_contr_tac, 
673 
bimatch_from_nets_tac safe0_netpair, 

674 
FIRST' hyp_subst_tacs, 

675 
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

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

677 

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

678 
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

679 

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

680 

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

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

682 

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

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

685 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  686 
assume_tac APPEND' 
687 
contr_tac APPEND' 

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

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

689 

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

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

692 
biresolve_from_nets_tac safep_netpair; 
0  693 

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

695 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  696 

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

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

699 

0  700 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  701 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  702 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  703 

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

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

10736  706 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  707 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  708 

1800  709 
(**** The following tactics all fail unless they solve one goal ****) 
0  710 

711 
(*Dumb but fast*) 

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

712 
fun fast_tac cs = 
11754  713 
ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  714 

715 
(*Slower but smarter than fast_tac*) 

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

716 
fun best_tac cs = 
11754  717 
ObjectLogic.atomize_tac THEN' 
0  718 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
719 

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

721 
fun first_best_tac cs = 
11754  722 
ObjectLogic.atomize_tac THEN' 
9402  723 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
724 

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

725 
fun slow_tac cs = 
11754  726 
ObjectLogic.atomize_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

727 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  728 

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

729 
fun slow_best_tac cs = 
11754  730 
ObjectLogic.atomize_tac THEN' 
0  731 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
732 

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

733 

10736  734 
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
735 
val weight_ASTAR = ref 5; 

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

736 

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

737 
fun astar_tac cs = 
11754  738 
ObjectLogic.atomize_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

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

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

742 

10736  743 
fun slow_astar_tac cs = 
11754  744 
ObjectLogic.atomize_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

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

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

748 

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

750 
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

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

753 

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

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

755 
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

756 
greater search depth required.*) 
10736  757 
fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

759 

5523  760 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  761 
local 
10736  762 
fun slow_step_tac' cs = appWrappers cs 
9938  763 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  764 
in fun depth_tac cs m i state = SELECT_GOAL 
765 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  769 
)) i state; 
770 
end; 

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

771 

10736  772 
(*Search, with depth bound m. 
2173  773 
This is the "entry point", which does safe inferences first.*) 
10736  774 
fun safe_depth_tac cs m = 
775 
SUBGOAL 

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

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

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

10736  780 
[] => DETERM 
9938  781 
 _::_ => I 
10736  782 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  783 
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

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

785 

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

786 
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

787 

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

788 

1724  789 

15036  790 
(** context dependent claset components **) 
791 

792 
datatype context_cs = ContextCS of 

793 
{swrappers: (string * (Proof.context > wrapper)) list, 

794 
uwrappers: (string * (Proof.context > wrapper)) list}; 

795 

796 
fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) = 

797 
let 

798 
fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt)); 

799 
in 

800 
cs > fold_rev (add_wrapper (op addSWrapper)) swrappers 

801 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 

802 
end; 

803 

804 
fun make_context_cs (swrappers, uwrappers) = 

805 
ContextCS {swrappers = swrappers, uwrappers = uwrappers}; 

806 

807 
val empty_context_cs = make_context_cs ([], []); 

808 

809 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

810 
let 

811 
val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1; 

812 
val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2; 

813 

814 
val swrappers' = merge_alists swrappers1 swrappers2; 

815 
val uwrappers' = merge_alists uwrappers1 uwrappers2; 

816 
in make_context_cs (swrappers', uwrappers') end; 

817 

818 

819 

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

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

821 

7354  822 
(* theory data kind 'Provers/claset' *) 
1724  823 

16424  824 
structure GlobalClaset = TheoryDataFun 
825 
(struct 

7354  826 
val name = "Provers/claset"; 
15036  827 
type T = claset ref * context_cs; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

828 

15036  829 
val empty = (ref empty_cs, empty_context_cs); 
16424  830 
fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; 
831 
val extend = copy; 

832 
fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) = 

15036  833 
(ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2)); 
834 
fun print _ (ref cs, _) = print_cs cs; 

16424  835 
end); 
1724  836 

7354  837 
val print_claset = GlobalClaset.print; 
15036  838 
val claset_ref_of = #1 o GlobalClaset.get; 
16424  839 
val claset_ref_of_sg = claset_ref_of; 
15036  840 
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; 
841 

842 
fun map_context_cs f = GlobalClaset.map (apsnd 

843 
(fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers)))); 

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

844 

1724  845 

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

846 
(* access claset *) 
1724  847 

16424  848 
val claset_of = ! o claset_ref_of; 
849 
val claset_of_sg = claset_of; 

1800  850 

16424  851 
fun CLASET tacf state = tacf (claset_of (Thm.theory_of_thm state)) state; 
852 
fun CLASET' tacf i state = tacf (claset_of (Thm.theory_of_thm state)) i state; 

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

853 

5028  854 
val claset = claset_of o Context.the_context; 
16424  855 
val claset_ref = claset_ref_of o Context.the_context; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

856 

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

857 

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

858 
(* change claset *) 
1800  859 

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

860 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  861 

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

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

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

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

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

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

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

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

869 

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

870 

15036  871 
(* context dependent components *) 
872 

873 
fun add_context_safe_wrapper wrapper = map_context_cs (apfst (merge_alists [wrapper])); 

874 
fun del_context_safe_wrapper name = map_context_cs (apfst (filter_out (equal name o #1))); 

875 

876 
fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd (merge_alists [wrapper])); 

877 
fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1))); 

878 

879 

5841  880 
(* proof data kind 'Provers/claset' *) 
881 

16424  882 
structure LocalClaset = ProofDataFun 
883 
(struct 

5841  884 
val name = "Provers/claset"; 
885 
type T = claset; 

886 
val init = claset_of; 

15036  887 
fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt)); 
16424  888 
end); 
5841  889 

890 
val print_local_claset = LocalClaset.print; 

891 
val get_local_claset = LocalClaset.get; 

892 
val put_local_claset = LocalClaset.put; 

893 

15036  894 
fun local_claset_of ctxt = 
895 
context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt); 

896 

5841  897 

5885  898 
(* attributes *) 
899 

900 
fun change_global_cs f (thy, th) = 

901 
let val r = claset_ref_of thy 

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

904 
fun change_local_cs f (ctxt, th) = 

6096  905 
let val cs = f (get_local_claset ctxt, [th]) 
5885  906 
in (put_local_claset cs ctxt, th) end; 
907 

908 
val safe_dest_global = change_global_cs (op addSDs); 

909 
val safe_elim_global = change_global_cs (op addSEs); 

910 
val safe_intro_global = change_global_cs (op addSIs); 

6955  911 
val haz_dest_global = change_global_cs (op addDs); 
912 
val haz_elim_global = change_global_cs (op addEs); 

913 
val haz_intro_global = change_global_cs (op addIs); 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

914 
val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; 
5885  915 

16806  916 
val safe_dest_local = change_local_cs (op addSDs); 
917 
val safe_elim_local = change_local_cs (op addSEs); 

918 
val safe_intro_local = change_local_cs (op addSIs); 

919 
val haz_dest_local = change_local_cs (op addDs); 

920 
val haz_elim_local = change_local_cs (op addEs); 

921 
val haz_intro_local = change_local_cs (op addIs); 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

922 
val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; 
5885  923 

924 

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

925 
(* tactics referring to the implicit claset *) 
1800  926 

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

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

930 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  931 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
932 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  938 

1800  939 

10736  940 
end; 
5841  941 

942 

943 

5885  944 
(** concrete syntax of attributes **) 
5841  945 

946 
(* add / del rules *) 

947 

948 
val introN = "intro"; 

949 
val elimN = "elim"; 

950 
val destN = "dest"; 

9938  951 
val ruleN = "rule"; 
5841  952 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

953 
fun add_rule xtra haz safe = Attrib.syntax 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

954 
(Scan.lift (Args.query  Scan.option Args.nat >> xtra  Args.bang >> K safe  
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

955 
Scan.succeed haz)); 
5841  956 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

957 
fun del_rule att = Attrib.syntax (Scan.lift Args.del >> K att); 
5841  958 

959 

960 
(* setup_attrs *) 

961 

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

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

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

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

966 
"destruct rule turned into elimination rule format (classical)"), 
12401  967 
("swapped", (swapped, swapped), "classical swap of introduction rule"), 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

968 
(destN, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

969 
(add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

970 
add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

971 
"declaration of destruction rule"), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

972 
(elimN, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

973 
(add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

974 
add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

975 
"declaration of elimination rule"), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

976 
(introN, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

977 
(add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

978 
add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

979 
"declaration of introduction rule"), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

980 
(ruleN, (del_rule rule_del_global, del_rule rule_del_local), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

981 
"remove declaration of intro/elim/dest rule")]; 
5841  982 

983 

984 

7230  985 
(** proof methods **) 
986 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset

987 
fun METHOD_CLASET tac ctxt = 
15036  988 
Method.METHOD (tac ctxt (local_claset_of ctxt)); 
5841  989 

8098  990 
fun METHOD_CLASET' tac ctxt = 
15036  991 
Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); 
7230  992 

993 

994 
local 

995 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

996 
fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) => 
5841  997 
let 
12401  998 
val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt; 
999 
val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair; 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1000 
val rules = rules1 @ rules2 @ rules3 @ rules4; 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1001 
val ruleq = Method.multi_resolves facts rules; 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1002 
in 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1003 
Method.trace ctxt rules; 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1004 
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1005 
end); 
5841  1006 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1007 
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts 
10394  1008 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 
7281  1009 

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

1010 
fun default_tac rules ctxt cs facts = 
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset

1011 
HEADGOAL (rule_tac rules ctxt cs facts) ORELSE 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

1012 
AxClass.default_intro_classes_tac facts; 
10309  1013 

7230  1014 
in 
7281  1015 
val rule = METHOD_CLASET' o rule_tac; 
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset

1016 
val default = METHOD_CLASET o default_tac; 
7230  1017 
end; 
5841  1018 

1019 

7230  1020 
(* contradiction method *) 
6502  1021 

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

1024 

1025 
(* automatic methods *) 

5841  1026 

5927  1027 
val cla_modifiers = 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1028 
[Args.$$$ destN  Args.bang_colon >> K ((I, safe_dest_local): Method.modifier), 
10034  1029 
Args.$$$ destN  Args.colon >> K (I, haz_dest_local), 
1030 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim_local), 

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

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

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

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

5927  1035 

7559  1036 
fun cla_meth tac prems ctxt = Method.METHOD (fn facts => 
15036  1037 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); 
7132  1038 

7559  1039 
fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => 
15036  1040 
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt))); 
5841  1041 

7559  1042 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1043 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1044 

1045 

1046 

1047 
(** setup_methods **) 

1048 

1049 
val setup_methods = Method.add_methods 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1050 
[("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1051 
("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"), 
6502  1052 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
10821  1053 
("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"), 
7004  1054 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1055 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1056 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
10821  1057 
("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")]; 
5841  1058 

1059 

1060 

1061 
(** theory setup **) 

1062 

16806  1063 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1064 

1065 

8667  1066 

1067 
(** outer syntax **) 

1068 

1069 
val print_clasetP = 

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

17057  1071 
OuterKeyword.diag 
9513  1072 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1073 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1074 

1075 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1076 

1077 

5841  1078 
end; 