author  wenzelm 
Fri, 17 Jun 2005 18:33:05 +0200  
changeset 16424  18a07ad8fea8 
parent 15735  953f188e16c6 
child 16806  916387f7afd2 
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 

15452  17 

18 
(*added: get_delta_claset, put_delta_claset. 

19 
changed: safe_{dest,elim,intro}_local and haz_{dest,elim,intro}_local 

20 
06/01/05 

21 
*) 

22 

23 

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

24 
(*higher precedence than := facilitates use of references*) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

27 
addSbefore addSafter addbefore addafter 
5523  28 
addD2 addE2 addSD2 addSE2; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

29 

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

30 

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

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

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

34 

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

36 
sig 
9171  37 
val make_elim : thm > thm (* Tactic.make_elim or a classical version*) 
9938  38 
val mp : thm (* [ P>Q; P ] ==> Q *) 
39 
val not_elim : thm (* [ ~P; P ] ==> R *) 

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

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

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

43 
end; 
0  44 

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

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

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

49 
val print_cs: claset > unit 
4380  50 
val print_claset: theory > unit 
4653  51 
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

52 
claset > {safeIs: thm list, safeEs: thm list, 
9938  53 
hazIs: thm list, hazEs: thm list, 
10736  54 
swrappers: (string * wrapper) list, 
9938  55 
uwrappers: (string * wrapper) list, 
56 
safe0_netpair: netpair, safep_netpair: netpair, 

12401  57 
haz_netpair: netpair, dup_netpair: netpair, 
58 
xtra_netpair: ContextRules.netpair} 

9938  59 
val merge_cs : claset * claset > claset 
60 
val addDs : claset * thm list > claset 

61 
val addEs : claset * thm list > claset 

62 
val addIs : claset * thm list > claset 

63 
val addSDs : claset * thm list > claset 

64 
val addSEs : claset * thm list > claset 

65 
val addSIs : claset * thm list > claset 

66 
val delrules : claset * thm list > claset 

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

68 
val delSWrapper : claset * string > claset 

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

70 
val delWrapper : claset * string > claset 

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

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

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

74 
val addafter : claset * (string * (int > tactic)) > claset 
5523  75 
val addD2 : claset * (string * thm) > claset 
76 
val addE2 : claset * (string * thm) > claset 

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

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

9938  79 
val appSWrappers : claset > wrapper 
80 
val appWrappers : claset > wrapper 

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

81 

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

82 
val claset_ref_of: theory > claset ref 
16424  83 
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

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

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

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

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

89 
val claset_ref: unit > claset ref 
15036  90 
val local_claset_of : Proof.context > claset 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

91 

9938  92 
val fast_tac : claset > int > tactic 
93 
val slow_tac : claset > int > tactic 

94 
val weight_ASTAR : int ref 

95 
val astar_tac : claset > int > tactic 

96 
val slow_astar_tac : claset > int > tactic 

97 
val best_tac : claset > int > tactic 

98 
val first_best_tac : claset > int > tactic 

99 
val slow_best_tac : claset > int > tactic 

100 
val depth_tac : claset > int > int > tactic 

101 
val deepen_tac : claset > int > int > tactic 

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

102 

9938  103 
val contr_tac : int > tactic 
104 
val dup_elim : thm > thm 

105 
val dup_intr : thm > thm 

106 
val dup_step_tac : claset > int > tactic 

107 
val eq_mp_tac : int > tactic 

108 
val haz_step_tac : claset > int > tactic 

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

110 
val mp_tac : int > tactic 

111 
val safe_tac : claset > tactic 

112 
val safe_steps_tac : claset > int > tactic 

113 
val safe_step_tac : claset > int > tactic 

114 
val clarify_tac : claset > int > tactic 

115 
val clarify_step_tac : claset > int > tactic 

116 
val step_tac : claset > int > tactic 

117 
val slow_step_tac : claset > int > tactic 

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

119 
val swapify : thm list > thm list 

120 
val swap_res_tac : thm list > int > tactic 

121 
val inst_step_tac : claset > int > tactic 

122 
val inst0_step_tac : claset > int > tactic 

123 
val instp_step_tac : claset > int > tactic 

1724  124 

9938  125 
val AddDs : thm list > unit 
126 
val AddEs : thm list > unit 

127 
val AddIs : thm list > unit 

128 
val AddSDs : thm list > unit 

129 
val AddSEs : thm list > unit 

130 
val AddSIs : thm list > unit 

131 
val Delrules : thm list > unit 

132 
val Safe_tac : tactic 

133 
val Safe_step_tac : int > tactic 

134 
val Clarify_tac : int > tactic 

135 
val Clarify_step_tac : int > tactic 

136 
val Step_tac : int > tactic 

137 
val Fast_tac : int > tactic 

138 
val Best_tac : int > tactic 

139 
val Slow_tac : int > tactic 

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

142 
end; 
1724  143 

5841  144 
signature CLASSICAL = 
145 
sig 

146 
include BASIC_CLASSICAL 

15036  147 
val add_context_safe_wrapper: string * (Proof.context > wrapper) > theory > theory 
148 
val del_context_safe_wrapper: string > theory > theory 

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

150 
val del_context_unsafe_wrapper: string > theory > theory 

5841  151 
val print_local_claset: Proof.context > unit 
152 
val get_local_claset: Proof.context > claset 

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

154 
val safe_dest_global: theory attribute 

155 
val safe_elim_global: theory attribute 

156 
val safe_intro_global: theory attribute 

6955  157 
val haz_dest_global: theory attribute 
158 
val haz_elim_global: theory attribute 

159 
val haz_intro_global: theory attribute 

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

163 
val safe_intro_local: Proof.context attribute 

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

166 
val haz_intro_local: Proof.context attribute 

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

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

5841  173 
val setup: (theory > theory) list 
15452  174 

175 
val get_delta_claset: ProofContext.context > claset 

176 
val put_delta_claset: claset > ProofContext.context > ProofContext.context 

177 

5841  178 
end; 
179 

0  180 

5927  181 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  182 
struct 
183 

7354  184 
local open Data in 
0  185 

1800  186 
(*** Useful tactics for classical reasoning ***) 
0  187 

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

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

10736  194 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  195 
(eq_assume_tac ORELSE' assume_tac); 
0  196 

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

197 
(*Finds P>Q and P in the assumptions, replaces implication by Q. 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

198 
Could do the same thing for P<>Q and P... *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

201 
(*Like mp_tac but instantiates no variables*) 

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

202 
fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

203 

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

0  206 

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

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

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

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

212 
trying rules in order. *) 

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

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

217 
biresolve_tac (foldr addrl [] rls) 
0  218 
end; 
219 

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

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

221 
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

222 

6967  223 
fun dup_elim th = 
13525  224 
(case try (fn () => 
225 
rule_by_tactic (TRYALL (etac revcut_rl)) 

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

15531  227 
SOME th' => th' 
6967  228 
 _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); 
0  229 

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

230 

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

233 
datatype claset = 

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

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

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

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

9938  239 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  240 
safe0_netpair : netpair, (*nets for trivial cases*) 
241 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

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

0  245 

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

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

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

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

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

252 

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

254 
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

255 
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

256 
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

257 
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

258 
*) 
0  259 

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

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

265 
hazIs = [], 

266 
hazEs = [], 

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

6502  269 
safe0_netpair = empty_netpair, 
270 
safep_netpair = empty_netpair, 

271 
haz_netpair = empty_netpair, 

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

0  274 

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

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

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

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

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

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

287 

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

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

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

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

294 

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

295 

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

297 

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

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

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

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

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

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

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

305 

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

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

308 

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

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

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

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

315 

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

10736  318 

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

319 
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

320 

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

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

322 
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

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

324 
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 
12401  325 
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

326 

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

327 
fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls; 
12362  328 
fun delete x = delete_tagged_list (joinrules x); 
12401  329 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  330 

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

331 
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

332 
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

333 

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

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

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

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

339 
else if mem_thm (th, safeEs) then 
9408  340 
warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) 
10736  341 
else if mem_thm (th, hazIs) then 
9760  342 
warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) 
10736  343 
else if mem_thm (th, hazEs) then 
9760  344 
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

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

346 

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

347 

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

349 

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

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

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

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

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

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

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

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

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

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

366 
hazIs = hazIs, 

367 
hazEs = hazEs, 

368 
swrappers = swrappers, 

369 
uwrappers = uwrappers, 

370 
haz_netpair = haz_netpair, 

371 
dup_netpair = dup_netpair, 

12401  372 
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

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

374 

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

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

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

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

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

382 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
15570  383 
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

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

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

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

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

391 
hazIs = hazIs, 

392 
hazEs = hazEs, 

393 
swrappers = swrappers, 

394 
uwrappers = uwrappers, 

395 
haz_netpair = haz_netpair, 

396 
dup_netpair = dup_netpair, 

12401  397 
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

398 
end; 
0  399 

15570  400 
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

401 

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

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

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

404 

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

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

407 

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

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

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

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

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

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

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

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

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

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

10736  423 
safeIs = safeIs, 
9938  424 
safeEs = safeEs, 
425 
hazEs = hazEs, 

426 
swrappers = swrappers, 

427 
uwrappers = uwrappers, 

428 
safe0_netpair = safe0_netpair, 

429 
safep_netpair = safep_netpair, 

12401  430 
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

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

432 

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

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

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

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

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

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

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

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

10736  446 
safeIs = safeIs, 
9938  447 
safeEs = safeEs, 
448 
hazIs = hazIs, 

449 
swrappers = swrappers, 

450 
uwrappers = uwrappers, 

451 
safe0_netpair = safe0_netpair, 

452 
safep_netpair = safep_netpair, 

12401  453 
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

454 
end; 
0  455 

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

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

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

458 

9938  459 
fun cs addDs ths = cs addEs (map Data.make_elim ths); 
0  460 

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

461 

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

465 
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

466 
searches in all the lists and chooses the relevant delXX functions. 
1800  467 
***) 
468 

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

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

472 
if mem_thm (th, safeIs) then 
15570  473 
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

474 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  475 
safep_netpair = delete (safep_rls, []) safep_netpair, 
476 
safeIs = rem_thm (safeIs,th), 

477 
safeEs = safeEs, 

478 
hazIs = hazIs, 

479 
hazEs = hazEs, 

480 
swrappers = swrappers, 

481 
uwrappers = uwrappers, 

482 
haz_netpair = haz_netpair, 

483 
dup_netpair = dup_netpair, 

12401  484 
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

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

486 
else cs; 
1800  487 

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

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

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

491 
if mem_thm (th, safeEs) then 
15570  492 
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

493 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  494 
safep_netpair = delete ([], safep_rls) safep_netpair, 
495 
safeIs = safeIs, 

496 
safeEs = rem_thm (safeEs,th), 

497 
hazIs = hazIs, 

498 
hazEs = hazEs, 

499 
swrappers = swrappers, 

500 
uwrappers = uwrappers, 

501 
haz_netpair = haz_netpair, 

502 
dup_netpair = dup_netpair, 

12401  503 
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

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

505 
else cs; 
1800  506 

507 

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

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

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

511 
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

512 
CS{haz_netpair = delete ([th], []) haz_netpair, 
9938  513 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
10736  514 
safeIs = safeIs, 
9938  515 
safeEs = safeEs, 
516 
hazIs = rem_thm (hazIs,th), 

517 
hazEs = hazEs, 

518 
swrappers = swrappers, 

519 
uwrappers = uwrappers, 

520 
safe0_netpair = safe0_netpair, 

521 
safep_netpair = safep_netpair, 

12401  522 
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

523 
else cs; 
1800  524 

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

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

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

528 
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

529 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
9938  530 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
10736  531 
safeIs = safeIs, 
9938  532 
safeEs = safeEs, 
533 
hazIs = hazIs, 

534 
hazEs = rem_thm (hazEs,th), 

535 
swrappers = swrappers, 

536 
uwrappers = uwrappers, 

537 
safe0_netpair = safe0_netpair, 

538 
safep_netpair = safep_netpair, 

12401  539 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
6955  540 
else cs; 
541 

1800  542 

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

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

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

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

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

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

549 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
9938  550 
else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs) 
551 
end; 

1800  552 

15570  553 
val op delrules = Library.foldl delrule; 
1800  554 

555 

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

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

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

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

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

562 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  563 
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

564 

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

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

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

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

570 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  571 
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

572 

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

573 

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

575 
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => 
9721  576 
overwrite_warn (swrappers, new_swrapper) 
577 
("Overwriting safe wrapper " ^ fst new_swrapper)); 

4651  578 

579 
(*Add/replace an unsafe wrapper*) 

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

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

583 

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

585 
fun cs delSWrapper name = update_swrappers cs (fn swrappers => 
15036  586 
let val swrappers' = filter_out (equal name o #1) swrappers in 
587 
if length swrappers <> length swrappers' then swrappers' 

588 
else (warning ("No such safe wrapper in claset: "^ name); swrappers) 

589 
end); 

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

590 

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

592 
fun cs delWrapper name = update_uwrappers cs (fn uwrappers => 
15036  593 
let val uwrappers' = filter_out (equal name o #1) uwrappers in 
594 
if length uwrappers <> length uwrappers' then uwrappers' 

595 
else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers) 

596 
end); 

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

597 

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

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

603 

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

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

609 

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

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

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

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

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

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

617 
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

618 

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

621 
treatment of priority might get muddled up.*) 

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

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

623 
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

624 
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

625 
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

626 
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

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

628 
val cs1 = cs addSIs safeIs' 
9938  629 
addSEs safeEs' 
630 
addIs hazIs' 

631 
addEs hazEs' 

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

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

633 
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); 
10736  634 
in cs3 
1711  635 
end; 
636 

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

637 

1800  638 
(**** Simple tactics for theorem proving ****) 
0  639 

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

10736  641 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  642 
appSWrappers cs (FIRST' [ 
9938  643 
eq_assume_tac, 
644 
eq_mp_tac, 

645 
bimatch_from_nets_tac safe0_netpair, 

646 
FIRST' hyp_subst_tacs, 

647 
bimatch_from_nets_tac safep_netpair]); 

0  648 

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

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

655 

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

656 

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

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

658 

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

659 
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

660 

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

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

662 
create precisely n subgoals.*) 
10736  663 
fun n_bimatch_from_nets_tac n = 
15570  664 
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

665 

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

666 
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

667 
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

668 

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

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

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

671 
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

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

673 

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

674 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  675 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  676 
appSWrappers cs (FIRST' [ 
9938  677 
eq_assume_contr_tac, 
678 
bimatch_from_nets_tac safe0_netpair, 

679 
FIRST' hyp_subst_tacs, 

680 
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

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

682 

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

683 
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

684 

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

685 

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

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

687 

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

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

690 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  691 
assume_tac APPEND' 
692 
contr_tac APPEND' 

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

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

694 

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

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

697 
biresolve_from_nets_tac safep_netpair; 
0  698 

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

700 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  701 

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

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

704 

0  705 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  706 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  707 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  708 

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

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

10736  711 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  712 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  713 

1800  714 
(**** The following tactics all fail unless they solve one goal ****) 
0  715 

716 
(*Dumb but fast*) 

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

717 
fun fast_tac cs = 
11754  718 
ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  719 

720 
(*Slower but smarter than fast_tac*) 

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

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

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

726 
fun first_best_tac cs = 
11754  727 
ObjectLogic.atomize_tac THEN' 
9402  728 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
729 

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

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

732 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  733 

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

734 
fun slow_best_tac cs = 
11754  735 
ObjectLogic.atomize_tac THEN' 
0  736 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
737 

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

738 

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

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

741 

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

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

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

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

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

747 

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

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

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

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

753 

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

755 
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

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

758 

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

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

760 
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

761 
greater search depth required.*) 
10736  762 
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

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

764 

5523  765 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  766 
local 
10736  767 
fun slow_step_tac' cs = appWrappers cs 
9938  768 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  769 
in fun depth_tac cs m i state = SELECT_GOAL 
770 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  774 
)) i state; 
775 
end; 

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

776 

10736  777 
(*Search, with depth bound m. 
2173  778 
This is the "entry point", which does safe inferences first.*) 
10736  779 
fun safe_depth_tac cs m = 
780 
SUBGOAL 

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

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

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

10736  785 
[] => DETERM 
9938  786 
 _::_ => I 
10736  787 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  788 
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

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

790 

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

791 
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

792 

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

793 

1724  794 

15036  795 
(** context dependent claset components **) 
796 

797 
datatype context_cs = ContextCS of 

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

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

800 

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

802 
let 

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

804 
in 

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

806 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 

807 
end; 

808 

809 
fun make_context_cs (swrappers, uwrappers) = 

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

811 

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

813 

814 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

815 
let 

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

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

818 

819 
val swrappers' = merge_alists swrappers1 swrappers2; 

820 
val uwrappers' = merge_alists uwrappers1 uwrappers2; 

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

822 

823 

824 

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

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

826 

7354  827 
(* theory data kind 'Provers/claset' *) 
1724  828 

16424  829 
structure GlobalClaset = TheoryDataFun 
830 
(struct 

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

833 

15036  834 
val empty = (ref empty_cs, empty_context_cs); 
16424  835 
fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; 
836 
val extend = copy; 

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

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

16424  840 
end); 
1724  841 

7354  842 
val print_claset = GlobalClaset.print; 
15036  843 
val claset_ref_of = #1 o GlobalClaset.get; 
16424  844 
val claset_ref_of_sg = claset_ref_of; 
15036  845 
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; 
846 

847 
fun map_context_cs f = GlobalClaset.map (apsnd 

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

849 

1724  850 

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

851 
(* access claset *) 
1724  852 

16424  853 
val claset_of = ! o claset_ref_of; 
854 
val claset_of_sg = claset_of; 

1800  855 

16424  856 
fun CLASET tacf state = tacf (claset_of (Thm.theory_of_thm state)) state; 
857 
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

858 

5028  859 
val claset = claset_of o Context.the_context; 
16424  860 
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

861 

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

862 

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

863 
(* change claset *) 
1800  864 

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

865 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  866 

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

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

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

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

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

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

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

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

874 

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

875 

15036  876 
(* context dependent components *) 
877 

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

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

880 

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

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

883 

884 

5841  885 
(* proof data kind 'Provers/claset' *) 
886 

16424  887 
structure LocalClaset = ProofDataFun 
888 
(struct 

5841  889 
val name = "Provers/claset"; 
890 
type T = claset; 

891 
val init = claset_of; 

15036  892 
fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt)); 
16424  893 
end); 
5841  894 

895 
val print_local_claset = LocalClaset.print; 

896 
val get_local_claset = LocalClaset.get; 

897 
val put_local_claset = LocalClaset.put; 

898 

15036  899 
fun local_claset_of ctxt = 
900 
context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt); 

901 

15452  902 
(* added for delta_claset: 06/01/05 *) 
15735  903 
(* CB: changed "delta clasets" to context data, 
904 
moved counter to here, it is no longer a ref *) 

15452  905 

906 
structure DeltaClasetArgs = 

907 
struct 

15735  908 
val name = "Provers/delta_claset"; 
909 
type T = claset * int; 

910 
fun init _ = (empty_cs, 0) 

911 
fun print ctxt cs = (); 

15452  912 
end; 
913 

15735  914 
structure DeltaClasetData = ProofDataFun(DeltaClasetArgs); 
915 
val get_delta_claset = #1 o DeltaClasetData.get; 

916 
fun put_delta_claset cs = DeltaClasetData.map (fn (_, i) => (cs, i)); 

917 
fun delta_increment ctxt = 

918 
let val ctxt' = DeltaClasetData.map (fn (ss, i) => (ss, i+1)) ctxt 

919 
in (ctxt', #2 (DeltaClasetData.get ctxt')) 

920 
end; 

15452  921 

16424  922 
local 
15452  923 
fun rename_thm' (ctxt,thm) = 
15735  924 
let val (new_ctxt, new_id) = delta_increment ctxt 
925 
val new_name = "anon_cla_" ^ (string_of_int new_id) 

15452  926 
in 
15735  927 
(new_ctxt, Thm.name_thm(new_name,thm)) 
15452  928 
end; 
929 

930 
in 

931 

932 
(* rename thm if call_atp is true *) 

15735  933 
fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm); 
15452  934 

935 
end 

16424  936 

5841  937 

5885  938 
(* attributes *) 
939 

940 
fun change_global_cs f (thy, th) = 

941 
let val r = claset_ref_of thy 

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

944 
fun change_local_cs f (ctxt, th) = 

6096  945 
let val cs = f (get_local_claset ctxt, [th]) 
5885  946 
in (put_local_claset cs ctxt, th) end; 
947 

948 
val safe_dest_global = change_global_cs (op addSDs); 

949 
val safe_elim_global = change_global_cs (op addSEs); 

950 
val safe_intro_global = change_global_cs (op addSIs); 

6955  951 
val haz_dest_global = change_global_cs (op addDs); 
952 
val haz_elim_global = change_global_cs (op addEs); 

953 
val haz_intro_global = change_global_cs (op addIs); 

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

954 
val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; 
5885  955 

15452  956 

957 
(* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *) 

958 
fun safe_dest_local (ctxt,th) = 

959 
let val thm_name = Thm.name_of_thm th 

15735  960 
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) 
961 
val delta_cs = get_delta_claset ctxt' 

16424  962 
val new_dcs = delta_cs addSDs [th'] 
963 
val ctxt'' = put_delta_claset new_dcs ctxt' 

15452  964 
in 
16424  965 
change_local_cs (op addSDs) (ctxt'',th) 
15452  966 
end; 
967 

16424  968 
fun safe_elim_local (ctxt, th)= 
15452  969 
let val thm_name = Thm.name_of_thm th 
15735  970 
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) 
971 
val delta_cs = get_delta_claset ctxt' 

16424  972 
val new_dcs = delta_cs addSEs [th'] 
973 
val ctxt'' = put_delta_claset new_dcs ctxt' 

15452  974 
in 
16424  975 
change_local_cs (op addSEs) (ctxt'',th) 
15452  976 
end; 
977 

16424  978 
fun safe_intro_local (ctxt, th) = 
15452  979 
let val thm_name = Thm.name_of_thm th 
15735  980 
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) 
981 
val delta_cs = get_delta_claset ctxt' 

16424  982 
val new_dcs = delta_cs addSIs [th'] 
983 
val ctxt'' = put_delta_claset new_dcs ctxt' 

15452  984 
in 
16424  985 
change_local_cs (op addSIs) (ctxt'',th) 
15452  986 
end; 
987 

16424  988 
fun haz_dest_local (ctxt, th)= 
15452  989 
let val thm_name = Thm.name_of_thm th 
15735  990 
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th) 
991 
val delta_cs = get_delta_claset ctxt' 

16424  992 
val new_dcs = delta_cs addDs [th'] 
993 
val ctxt'' = put_delta_claset new_dcs ctxt' 

15452  994 
in 
16424  995 
change_local_cs (op addDs) (ctxt'',th) 
15452  996 
end; 
997 

998 
fun haz_elim_local (ctxt,th) = 

999 
let val thm_name = Thm.name_of_thm th 

15735  1000 
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) 
1001 
val delta_cs = get_delta_claset ctxt' 

16424  1002 
val new_dcs = delta_cs addEs [th'] 
1003 
val ctxt'' = put_delta_claset new_dcs ctxt' 

1004 
in 

1005 
change_local_cs (op addEs) (ctxt'',th) 

15452  1006 
end; 
1007 

16424  1008 
fun haz_intro_local (ctxt,th) = 
15452  1009 
let val thm_name = Thm.name_of_thm th 
15735  1010 
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) 
1011 
val delta_cs = get_delta_claset ctxt' 

16424  1012 
val new_dcs = delta_cs addIs [th'] 
1013 
val ctxt'' = put_delta_claset new_dcs ctxt' 

1014 
in 

1015 
change_local_cs (op addIs) (ctxt'',th) 

15452  1016 
end; 
1017 

1018 

1019 
(* when a rule is removed from local_claset, it is not removed from delta_claset in ProofContext.context. But this is unlikely to happen. *) 

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

1020 
val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; 
5885  1021 

1022 

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

1023 
(* tactics referring to the implicit claset *) 
1800  1024 

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

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

1028 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  1029 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
1030 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  1036 

1800  1037 

10736  1038 
end; 
5841  1039 

1040 

1041 

5885  1042 
(** concrete syntax of attributes **) 
5841  1043 

1044 
(* add / del rules *) 

1045 

1046 
val introN = "intro"; 

1047 
val elimN = "elim"; 

1048 
val destN = "dest"; 

9938  1049 
val ruleN = "rule"; 
5841  1050 

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

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

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

1053 
Scan.succeed haz)); 
5841  1054 

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

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

1057 

1058 
(* setup_attrs *) 

1059 

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

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

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

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

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

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

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

1068 
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

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

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

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

1072 
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

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

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

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

1076 
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

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

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

1079 
"remove declaration of intro/elim/dest rule")]; 
5841  1080 

1081 

1082 

7230  1083 
(** proof methods **) 
1084 

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

1085 
fun METHOD_CLASET tac ctxt = 
15036  1086 
Method.METHOD (tac ctxt (local_claset_of ctxt)); 
5841  1087 

8098  1088 
fun METHOD_CLASET' tac ctxt = 
15036  1089 
Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); 
7230  1090 

1091 

1092 
local 

1093 

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

1094 
fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) => 
5841  1095 
let 
12401  1096 
val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt; 
1097 
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

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

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

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

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

1102 
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

1103 
end); 
5841  1104 

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

1105 
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts 
10394  1106 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 
7281  1107 

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

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

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

1110 
AxClass.default_intro_classes_tac facts; 
10309  1111 

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

1114 
val default = METHOD_CLASET o default_tac; 
7230  1115 
end; 
5841  1116 

1117 

7230  1118 
(* contradiction method *) 
6502  1119 

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

1122 

1123 
(* automatic methods *) 

5841  1124 

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

1126 
[Args.$$$ destN  Args.bang_colon >> K ((I, safe_dest_local): Method.modifier), 
10034  1127 
Args.$$$ destN  Args.colon >> K (I, haz_dest_local), 
1128 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim_local), 

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

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

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

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

5927  1133 

7559  1134 
fun cla_meth tac prems ctxt = Method.METHOD (fn facts => 
15036  1135 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); 
7132  1136 

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

7559  1140 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1141 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1142 

1143 

1144 

1145 
(** setup_methods **) 

1146 

1147 
val setup_methods = Method.add_methods 

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

1148 
[("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

1149 
("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"), 
6502  1150 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
10821  1151 
("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"), 
7004  1152 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1153 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1154 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
10821  1155 
("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")]; 
5841  1156 

1157 

1158 

1159 
(** theory setup **) 

1160 

15735  1161 
val setup = [GlobalClaset.init, LocalClaset.init, DeltaClasetData.init, 
1162 
setup_attrs, setup_methods]; 

5841  1163 

1164 

8667  1165 

1166 
(** outer syntax **) 

1167 

1168 
val print_clasetP = 

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

1170 
OuterSyntax.Keyword.diag 

9513  1171 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1172 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1173 

1174 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1175 

1176 

5841  1177 
end; 
15707  1178 