author  wenzelm 
Sat, 23 Dec 2000 22:52:18 +0100  
changeset 10736  7f94cb4517fa 
parent 10394  eef9e422929a 
child 10821  dcb75538f542 
permissions  rwrr 
9938  1 
(* Title: Provers/classical.ML 
0  2 
ID: $Id$ 
9938  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

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

7 
theory, etc. 

8 

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

9 
Rules must be classified as intro, elim, safe, hazardous (unsafe). 
0  10 

11 
A rule is unsafe unless it can be applied blindly without harmful results. 

12 
For a rule to be safe, its premises and conclusion should be logically 

13 
equivalent. There should be no variables in the premises that are not in 

14 
the conclusion. 

15 
*) 

16 

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

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

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

22 

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

23 

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

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

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

27 

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

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

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

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

0  35 
val hyp_subst_tacs: (int > tactic) list 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

37 
end; 
0  38 

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

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

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

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

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

10736  49 
swrappers: (string * wrapper) list, 
9938  50 
uwrappers: (string * wrapper) list, 
51 
safe0_netpair: netpair, safep_netpair: netpair, 

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

53 
val merge_cs : claset * claset > claset 

54 
val addDs : claset * thm list > claset 

55 
val addEs : claset * thm list > claset 

56 
val addIs : claset * thm list > claset 

57 
val addSDs : claset * thm list > claset 

58 
val addSEs : claset * thm list > claset 

59 
val addSIs : claset * thm list > claset 

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

62 
val addXIs : claset * thm list > claset 

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

65 
val delSWrapper : claset * string > claset 

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

67 
val delWrapper : claset * string > claset 

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

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

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

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

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

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

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

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

78 
val trace_rules : bool ref 

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

79 

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

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

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

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

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

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

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

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

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

88 

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

91 
val weight_ASTAR : int ref 

92 
val astar_tac : claset > int > tactic 

93 
val slow_astar_tac : claset > int > tactic 

94 
val best_tac : claset > int > tactic 

95 
val first_best_tac : claset > int > tactic 

96 
val slow_best_tac : claset > int > tactic 

97 
val depth_tac : claset > int > int > tactic 

98 
val deepen_tac : claset > int > int > tactic 

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

99 

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

102 
val dup_intr : thm > thm 

103 
val dup_step_tac : claset > int > tactic 

104 
val eq_mp_tac : int > tactic 

105 
val haz_step_tac : claset > int > tactic 

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

107 
val mp_tac : int > tactic 

108 
val safe_tac : claset > tactic 

109 
val safe_steps_tac : claset > int > tactic 

110 
val safe_step_tac : claset > int > tactic 

111 
val clarify_tac : claset > int > tactic 

112 
val clarify_step_tac : claset > int > tactic 

113 
val step_tac : claset > int > tactic 

114 
val slow_step_tac : claset > int > tactic 

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

116 
val swapify : thm list > thm list 

117 
val swap_res_tac : thm list > int > tactic 

118 
val inst_step_tac : claset > int > tactic 

119 
val inst0_step_tac : claset > int > tactic 

120 
val instp_step_tac : claset > int > tactic 

1724  121 

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

124 
val AddIs : thm list > unit 

125 
val AddSDs : thm list > unit 

126 
val AddSEs : thm list > unit 

127 
val AddSIs : thm list > unit 

128 
val AddXDs : thm list > unit 

129 
val AddXEs : thm list > unit 

130 
val AddXIs : thm list > unit 

131 
val Delrules : thm list > unit 

132 
val Safe_tac : tactic 

133 
val Safe_step_tac : int > tactic 

134 
val Clarify_tac : int > tactic 

135 
val Clarify_step_tac : int > tactic 

136 
val Step_tac : int > tactic 

137 
val Fast_tac : int > tactic 

138 
val Best_tac : int > tactic 

139 
val Slow_tac : int > tactic 

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

142 
end; 
1724  143 

5841  144 
signature CLASSICAL = 
145 
sig 

146 
include BASIC_CLASSICAL 

147 
val print_local_claset: Proof.context > unit 

148 
val get_local_claset: Proof.context > claset 

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

150 
val safe_dest_global: theory attribute 

151 
val safe_elim_global: theory attribute 

152 
val safe_intro_global: theory attribute 

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

155 
val haz_intro_global: theory attribute 

156 
val xtra_dest_global: theory attribute 

157 
val xtra_elim_global: theory attribute 

158 
val xtra_intro_global: theory attribute 

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

162 
val safe_intro_local: Proof.context attribute 

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

165 
val haz_intro_local: Proof.context attribute 

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

168 
val xtra_intro_local: Proof.context attribute 

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

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

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

177 

0  178 

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

7354  182 
local open Data in 
0  183 

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

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

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

187 

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

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]); 

209 

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

211 
trying rules in order. *) 

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

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

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

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

220 
fun dup_intr th = zero_var_indexes (th RS classical); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

221 

6967  222 
fun dup_elim th = 
223 
(case try 

224 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

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

226 
Some th' => th' 

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

0  228 

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

229 

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

232 
datatype claset = 

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

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

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

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

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

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

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

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

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

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

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

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

0  246 

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

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

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

10736  251 
dup_netpair = build (joinrules(map dup_intr hazIs, 
9938  252 
map dup_elim hazEs)), 
253 
xtra_netpair = build (joinrules(xtraIs, xtraEs))} 

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

254 

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

256 
safe0_brls contains all brules that solve the subgoal, and 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

259 
Nets must be built incrementally, to save space and time. 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

260 
*) 
0  261 

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

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

267 
hazIs = [], 

268 
hazEs = [], 

269 
xtraIs = [], 

270 
xtraEs = [], 

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

6502  273 
safe0_netpair = empty_netpair, 
274 
safep_netpair = empty_netpair, 

275 
haz_netpair = empty_netpair, 

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

0  278 

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

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

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

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

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

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

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

291 

10736  292 
local 
4651  293 
fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac); 
10736  294 
in 
4651  295 
fun appSWrappers (CS{swrappers,...}) = calc_wrap swrappers; 
296 
fun appWrappers (CS{uwrappers,...}) = calc_wrap uwrappers; 

297 
end; 

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

298 

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

299 

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

301 

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

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

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

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

306 
assumptions. Pairs elim rules with true. *) 
10736  307 
fun joinrules (intrs,elims) = 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

310 

10736  311 
(*Priority: prefer rules with fewest subgoals, 
1231  312 
then rules added most recently (preferring the head of the list).*) 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

317 

10736  318 
fun recover_order k = k mod 1000000; 
319 

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

321 

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

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

323 
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

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

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

326 

1800  327 
fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

328 

1800  329 
val delete = delete_tagged_list o joinrules; 
330 

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

331 
val mem_thm = gen_mem eq_thm 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

332 
and rem_thm = gen_rem eq_thm; 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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.*) 
10736  336 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
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) 
10736  345 
else if mem_thm (th, xtraIs) then 
9408  346 
warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th) 
10736  347 
else if mem_thm (th, xtraEs) then 
9408  348 
warning ("Rule already declared as extra elimination (elim?)\n" ^ string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

350 

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

352 

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

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

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

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

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

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

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

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

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

369 
hazIs = hazIs, 

370 
hazEs = hazEs, 

371 
xtraIs = xtraIs, 

372 
xtraEs = xtraEs, 

373 
swrappers = swrappers, 

374 
uwrappers = uwrappers, 

375 
haz_netpair = haz_netpair, 

376 
dup_netpair = dup_netpair, 

377 
xtra_netpair = xtra_netpair} 

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

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

379 

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

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

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

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

387 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

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

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

396 
hazIs = hazIs, 

397 
hazEs = hazEs, 

398 
xtraIs = xtraIs, 

399 
xtraEs = xtraEs, 

400 
swrappers = swrappers, 

401 
uwrappers = uwrappers, 

402 
haz_netpair = haz_netpair, 

403 
dup_netpair = dup_netpair, 

404 
xtra_netpair = xtra_netpair} 

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

405 
end; 
0  406 

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

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

408 

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

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

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

411 

9938  412 
fun cs addSDs ths = cs addSEs (map Data.make_elim ths); 
0  413 

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

414 

1800  415 
(*** Hazardous (unsafe) rules ***) 
0  416 

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

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

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

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

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

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

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

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

10736  430 
safeIs = safeIs, 
9938  431 
safeEs = safeEs, 
432 
hazEs = hazEs, 

433 
xtraIs = xtraIs, 

434 
xtraEs = xtraEs, 

435 
swrappers = swrappers, 

436 
uwrappers = uwrappers, 

437 
safe0_netpair = safe0_netpair, 

438 
safep_netpair = safep_netpair, 

439 
xtra_netpair = xtra_netpair} 

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

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

441 

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

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

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

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

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

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

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

10736  455 
safeIs = safeIs, 
9938  456 
safeEs = safeEs, 
457 
hazIs = hazIs, 

458 
xtraIs = xtraIs, 

459 
xtraEs = xtraEs, 

460 
swrappers = swrappers, 

461 
uwrappers = uwrappers, 

462 
safe0_netpair = safe0_netpair, 

463 
safep_netpair = safep_netpair, 

464 
xtra_netpair = xtra_netpair} 

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

465 
end; 
0  466 

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

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

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

469 

9938  470 
fun cs addDs ths = cs addEs (map Data.make_elim ths); 
0  471 

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

472 

6955  473 
(*** Extra (single step) rules ***) 
474 

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

9938  476 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
477 
th)= 

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

6955  481 
else 
482 
let val nI = length xtraIs + 1 

483 
and nE = length xtraEs 

484 
in warn_dup th cs; 

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

10736  487 
safeIs = safeIs, 
9938  488 
safeEs = safeEs, 
489 
hazIs = hazIs, 

490 
hazEs = hazEs, 

491 
xtraEs = xtraEs, 

492 
swrappers = swrappers, 

493 
uwrappers = uwrappers, 

494 
safe0_netpair = safe0_netpair, 

495 
safep_netpair = safep_netpair, 

496 
haz_netpair = haz_netpair, 

497 
dup_netpair = dup_netpair} 

6955  498 
end; 
499 

10736  500 
fun addXE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  501 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 
502 
th) = 

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

6955  506 
else 
10736  507 
let val nI = length xtraIs 
6955  508 
and nE = length xtraEs + 1 
509 
in warn_dup th cs; 

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

10736  512 
safeIs = safeIs, 
9938  513 
safeEs = safeEs, 
514 
hazIs = hazIs, 

515 
hazEs = hazEs, 

516 
xtraIs = xtraIs, 

517 
swrappers = swrappers, 

518 
uwrappers = uwrappers, 

519 
safe0_netpair = safe0_netpair, 

520 
safep_netpair = safep_netpair, 

521 
haz_netpair = haz_netpair, 

522 
dup_netpair = dup_netpair} 

6955  523 
end; 
524 

525 
val op addXIs = rev_foldl addXI; 

526 
val op addXEs = rev_foldl addXE; 

527 

9938  528 
fun cs addXDs ths = cs addXEs (map Data.make_elim ths); 
6955  529 

530 

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

534 
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

535 
searches in all the lists and chooses the relevant delXX functions. 
1800  536 
***) 
537 

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

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

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

546 
safeEs = safeEs, 

547 
hazIs = hazIs, 

548 
hazEs = hazEs, 

549 
xtraIs = xtraIs, 

550 
xtraEs = xtraEs, 

551 
swrappers = swrappers, 

552 
uwrappers = uwrappers, 

553 
haz_netpair = haz_netpair, 

554 
dup_netpair = dup_netpair, 

555 
xtra_netpair = xtra_netpair} 

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

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

557 
else cs; 
1800  558 

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

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

562 
if mem_thm (th, safeEs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

563 
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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

567 
safeEs = rem_thm (safeEs,th), 

568 
hazIs = hazIs, 

569 
hazEs = hazEs, 

570 
xtraIs = xtraIs, 

571 
xtraEs = xtraEs, 

572 
swrappers = swrappers, 

573 
uwrappers = uwrappers, 

574 
haz_netpair = haz_netpair, 

575 
dup_netpair = dup_netpair, 

576 
xtra_netpair = xtra_netpair} 

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

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

578 
else cs; 
1800  579 

580 

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

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

584 
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

585 
CS{haz_netpair = delete ([th], []) haz_netpair, 
9938  586 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
10736  587 
safeIs = safeIs, 
9938  588 
safeEs = safeEs, 
589 
hazIs = rem_thm (hazIs,th), 

590 
hazEs = hazEs, 

591 
xtraIs = xtraIs, 

592 
xtraEs = xtraEs, 

593 
swrappers = swrappers, 

594 
uwrappers = uwrappers, 

595 
safe0_netpair = safe0_netpair, 

596 
safep_netpair = safep_netpair, 

597 
xtra_netpair = xtra_netpair} 

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

598 
else cs; 
1800  599 

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

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

603 
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

604 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
9938  605 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
10736  606 
safeIs = safeIs, 
9938  607 
safeEs = safeEs, 
608 
hazIs = hazIs, 

609 
hazEs = rem_thm (hazEs,th), 

610 
xtraIs = xtraIs, 

611 
xtraEs = xtraEs, 

612 
swrappers = swrappers, 

613 
uwrappers = uwrappers, 

614 
safe0_netpair = safe0_netpair, 

615 
safep_netpair = safep_netpair, 

616 
xtra_netpair = xtra_netpair} 

6955  617 
else cs; 
618 

619 

620 
fun delXI th 

10736  621 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  622 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
6955  623 
if mem_thm (th, xtraIs) then 
624 
CS{xtra_netpair = delete ([th], []) xtra_netpair, 

10736  625 
safeIs = safeIs, 
9938  626 
safeEs = safeEs, 
627 
hazIs = hazIs, 

628 
hazEs = hazEs, 

629 
xtraIs = rem_thm (xtraIs,th), 

630 
xtraEs = xtraEs, 

631 
swrappers = swrappers, 

632 
uwrappers = uwrappers, 

633 
safe0_netpair = safe0_netpair, 

634 
safep_netpair = safep_netpair, 

635 
haz_netpair = haz_netpair, 

636 
dup_netpair = dup_netpair} 

6955  637 
else cs; 
638 

639 
fun delXE th 

10736  640 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
9938  641 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
6955  642 
if mem_thm (th, xtraEs) then 
643 
CS{xtra_netpair = delete ([], [th]) xtra_netpair, 

10736  644 
safeIs = safeIs, 
9938  645 
safeEs = safeEs, 
646 
hazIs = hazIs, 

647 
hazEs = hazEs, 

648 
xtraIs = xtraIs, 

649 
xtraEs = rem_thm (xtraEs,th), 

650 
swrappers = swrappers, 

651 
uwrappers = uwrappers, 

652 
safe0_netpair = safe0_netpair, 

653 
safep_netpair = safep_netpair, 

654 
haz_netpair = haz_netpair, 

655 
dup_netpair = dup_netpair} 

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

656 
else cs; 
1800  657 

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

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

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

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

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

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

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

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

668 
end; 

1800  669 

670 
val op delrules = foldl delrule; 

671 

672 

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

673 
(*** Modifying the wrapper tacticals ***) 
10736  674 
fun update_swrappers 
675 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

6955  676 
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

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

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

680 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  681 
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

682 

10736  683 
fun update_uwrappers 
684 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

6955  685 
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

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

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

689 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  690 
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

691 

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

692 

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

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

4651  697 

698 
(*Add/replace an unsafe wrapper*) 

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

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

702 

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

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

705 
let val (del,rest) = partition (fn (n,_) => n=name) swrappers 
10736  706 
in if null del then (warning ("No such safe wrapper in claset: "^ name); 
9938  707 
swrappers) else rest end); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

708 

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

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

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

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

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

714 

2630  715 
(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) 
10736  716 
fun cs addSbefore (name, tac1) = 
5523  717 
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); 
10736  718 
fun cs addSaltern (name, tac2) = 
5523  719 
cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

720 

2630  721 
(*compose a tactic sequentially before/alternatively after the step tactic*) 
10736  722 
fun cs addbefore (name, tac1) = 
5523  723 
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

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

726 

10736  727 
fun cs addD2 (name, thm) = 
5523  728 
cs addaltern (name, dtac thm THEN' atac); 
10736  729 
fun cs addE2 (name, thm) = 
5523  730 
cs addaltern (name, etac thm THEN' atac); 
10736  731 
fun cs addSD2 (name, thm) = 
5523  732 
cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac); 
10736  733 
fun cs addSE2 (name, thm) = 
5523  734 
cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

735 

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

738 
treatment of priority might get muddled up.*) 

739 
fun merge_cs 

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

2630  745 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
746 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

6955  747 
val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) 
748 
val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) 

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

749 
val cs1 = cs addSIs safeIs' 
9938  750 
addSEs safeEs' 
751 
addIs hazIs' 

752 
addEs hazEs' 

753 
addXIs xtraIs' 

754 
addXEs xtraEs' 

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

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

756 
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); 
10736  757 
in cs3 
1711  758 
end; 
759 

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

760 

1800  761 
(**** Simple tactics for theorem proving ****) 
0  762 

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

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

768 
bimatch_from_nets_tac safe0_netpair, 

769 
FIRST' hyp_subst_tacs, 

770 
bimatch_from_nets_tac safep_netpair]); 

0  771 

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

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

778 

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

779 

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

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

781 

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

782 
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

783 

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

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

785 
create precisely n subgoals.*) 
10736  786 
fun n_bimatch_from_nets_tac n = 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

787 
biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

788 

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

789 
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

790 
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

791 

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

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

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

794 
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

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

796 

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

797 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  798 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  799 
appSWrappers cs (FIRST' [ 
9938  800 
eq_assume_contr_tac, 
801 
bimatch_from_nets_tac safe0_netpair, 

802 
FIRST' hyp_subst_tacs, 

803 
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

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

805 

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

806 
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

807 

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

808 

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

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

810 

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

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

813 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  814 
assume_tac APPEND' 
815 
contr_tac APPEND' 

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

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

817 

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

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

820 
biresolve_from_nets_tac safep_netpair; 
0  821 

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

823 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  824 

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

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

827 

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

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

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

10736  834 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  835 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  836 

1800  837 
(**** The following tactics all fail unless they solve one goal ****) 
0  838 

839 
(*Dumb but fast*) 

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

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

841 
atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  842 

843 
(*Slower but smarter than fast_tac*) 

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

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

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

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

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

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

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

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

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

855 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  856 

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

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

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

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

861 

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

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

864 

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

865 
fun astar_tac cs = 
10736  866 
atomize_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

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

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

870 

10736  871 
fun slow_astar_tac cs = 
872 
atomize_tac THEN' 

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

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

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

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

876 

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

878 
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

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

881 

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

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

883 
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

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

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

887 

5523  888 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  889 
local 
10736  890 
fun slow_step_tac' cs = appWrappers cs 
9938  891 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  892 
in fun depth_tac cs m i state = SELECT_GOAL 
893 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  897 
)) i state; 
898 
end; 

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

899 

10736  900 
(*Search, with depth bound m. 
2173  901 
This is the "entry point", which does safe inferences first.*) 
10736  902 
fun safe_depth_tac cs m = 
903 
SUBGOAL 

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

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

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

10736  908 
[] => DETERM 
9938  909 
 _::_ => I 
10736  910 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  911 
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

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

913 

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

914 
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

915 

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

916 

1724  917 

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

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

919 

7354  920 
(* theory data kind 'Provers/claset' *) 
1724  921 

7354  922 
structure GlobalClasetArgs = 
923 
struct 

924 
val name = "Provers/claset"; 

925 
type T = claset ref; 

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

926 

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

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

932 
end; 

1724  933 

7354  934 
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); 
935 
val print_claset = GlobalClaset.print; 

936 
val claset_ref_of_sg = GlobalClaset.get_sg; 

937 
val claset_ref_of = GlobalClaset.get; 

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

938 

1724  939 

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

940 
(* access claset *) 
1724  941 

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

942 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  943 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  944 

6391  945 
fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; 
946 
fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state; 

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

947 

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

950 

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

951 

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

952 
(* change claset *) 
1800  953 

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

954 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  955 

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

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

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

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

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

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

961 
val AddSIs = change_claset (op addSIs); 
6955  962 
val AddXDs = change_claset (op addXDs); 
963 
val AddXEs = change_claset (op addXEs); 

964 
val AddXIs = change_claset (op addXIs); 

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

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

966 

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

967 

5841  968 
(* proof data kind 'Provers/claset' *) 
969 

970 
structure LocalClasetArgs = 

971 
struct 

972 
val name = "Provers/claset"; 

973 
type T = claset; 

974 
val init = claset_of; 

975 
fun print _ cs = print_cs cs; 

976 
end; 

977 

978 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

979 
val print_local_claset = LocalClaset.print; 

980 
val get_local_claset = LocalClaset.get; 

981 
val put_local_claset = LocalClaset.put; 

982 

983 

5885  984 
(* attributes *) 
985 

986 
fun change_global_cs f (thy, th) = 

987 
let val r = claset_ref_of thy 

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

990 
fun change_local_cs f (ctxt, th) = 

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

994 
val safe_dest_global = change_global_cs (op addSDs); 

995 
val safe_elim_global = change_global_cs (op addSEs); 

996 
val safe_intro_global = change_global_cs (op addSIs); 

6955  997 
val haz_dest_global = change_global_cs (op addDs); 
998 
val haz_elim_global = change_global_cs (op addEs); 

999 
val haz_intro_global = change_global_cs (op addIs); 

1000 
val xtra_dest_global = change_global_cs (op addXDs); 

1001 
val xtra_elim_global = change_global_cs (op addXEs); 

1002 
val xtra_intro_global = change_global_cs (op addXIs); 

9938  1003 
val rule_del_global = change_global_cs (op delrules); 
5885  1004 

6955  1005 
val safe_dest_local = change_local_cs (op addSDs); 
1006 
val safe_elim_local = change_local_cs (op addSEs); 

1007 
val safe_intro_local = change_local_cs (op addSIs); 

5885  1008 
val haz_dest_local = change_local_cs (op addDs); 
1009 
val haz_elim_local = change_local_cs (op addEs); 

1010 
val haz_intro_local = change_local_cs (op addIs); 

6955  1011 
val xtra_dest_local = change_local_cs (op addXDs); 
1012 
val xtra_elim_local = change_local_cs (op addXEs); 

1013 
val xtra_intro_local = change_local_cs (op addXIs); 

9938  1014 
val rule_del_local = change_local_cs (op delrules); 
5885  1015 

1016 

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

1017 
(* tactics referring to the implicit claset *) 
1800  1018 

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

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

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

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

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

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

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

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

2066  1030 

1800  1031 

10736  1032 
end; 
5841  1033 

1034 

1035 

5885  1036 
(** concrete syntax of attributes **) 
5841  1037 

1038 
(* add / del rules *) 

1039 

1040 
val introN = "intro"; 

1041 
val elimN = "elim"; 

1042 
val destN = "dest"; 

9938  1043 
val ruleN = "rule"; 
5841  1044 

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

6955  1048 
fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); 
9938  1049 

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

1053 

1054 
(* setup_attrs *) 

1055 

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

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

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

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

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

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

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

1066 

1067 

7230  1068 
(** proof methods **) 
1069 

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

1071 

1072 
local 

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

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

1075 
in 

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

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

1078 
end; 

1079 

1080 

1081 
(* METHOD_CLASET' *) 

5841  1082 

8098  1083 
fun METHOD_CLASET' tac ctxt = 
10394  1084 
Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt)); 
7230  1085 

1086 

1087 
val trace_rules = ref false; 

5841  1088 

7230  1089 
local 
1090 

1091 
fun trace rules i = 

1092 
if not (! trace_rules) then () 

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

1094 
(map Display.pretty_thm rules)); 

1095 

1096 

10736  1097 
fun order_rules xs = map snd (Tactic.orderlist (map (apfst recover_order) xs)); 
5841  1098 

1099 
fun find_rules concl nets = 

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

1101 
in flat (map rules_of nets) end; 

1102 

1103 
fun find_erules [] _ = [] 

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

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

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

1116 
let 

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

1118 
val rules = erules @ irules; 

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

10394  1123 
fun rule_tac [] ctxt cs facts = 
1124 
some_rule_tac cs facts ORELSE' Method.some_rule_tac [] ctxt facts 

1125 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 

7281  1126 

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

1127 
fun default_tac rules ctxt cs facts = 
10394  1128 
rule_tac rules ctxt cs facts ORELSE' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

1129 
AxClass.default_intro_classes_tac facts; 
10309  1130 

7230  1131 
in 
7281  1132 
val rule = METHOD_CLASET' o rule_tac; 
10394  1133 
val default = METHOD_CLASET' o default_tac; 
7230  1134 
end; 
5841  1135 

1136 

7230  1137 
(* intro / elim methods *) 
1138 

1139 
local 

1140 

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

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

7230  1150 

1151 
in 

1152 
val intro = METHOD_CLASET' o intro_tac; 

1153 
val elim = METHOD_CLASET' o elim_tac; 

1154 
end; 

1155 

1156 

1157 
(* contradiction method *) 

6502  1158 

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

1161 

1162 
(* automatic methods *) 

5841  1163 

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

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

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

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

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

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

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

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

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

5927  1175 

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

7132  1178 

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

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

5841  1184 

1185 

1186 

1187 
(** setup_methods **) 

1188 

1189 
val setup_methods = Method.add_methods 

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

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

5841  1200 

1201 

1202 

1203 
(** theory setup **) 

1204 

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

1207 

8667  1208 

1209 
(** outer syntax **) 

1210 

1211 
val print_clasetP = 

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

1213 
OuterSyntax.Keyword.diag 

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

1217 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1218 

1219 

5841  1220 
end; 