author  wenzelm 
Wed, 05 Dec 2001 03:12:52 +0100  
changeset 12376  480303e3fa08 
parent 12362  57cd572103c4 
child 12401  4363432ef0cd 
permissions  rwrr 
9938  1 
(* Title: Provers/classical.ML 
0  2 
ID: $Id$ 
9938  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

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

7 
theory, etc. 

8 

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

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

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

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

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

14 
the conclusion. 

15 
*) 

16 

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

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

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

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

22 

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

23 

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

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

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

27 

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

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

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

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

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

36 
end; 
0  37 

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

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

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

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

45 
claset > {safeIs: thm list, safeEs: thm list, 
9938  46 
hazIs: thm list, hazEs: thm list, 
10736  47 
swrappers: (string * wrapper) list, 
9938  48 
uwrappers: (string * wrapper) list, 
49 
safe0_netpair: netpair, safep_netpair: netpair, 

50 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} 

51 
val merge_cs : claset * claset > claset 

52 
val addDs : claset * thm list > claset 

53 
val addEs : claset * thm list > claset 

54 
val addIs : claset * thm list > claset 

55 
val addSDs : claset * thm list > claset 

56 
val addSEs : claset * thm list > claset 

57 
val addSIs : claset * thm list > claset 

58 
val delrules : claset * thm list > claset 

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

60 
val delSWrapper : claset * string > claset 

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

62 
val delWrapper : claset * string > claset 

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

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

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

66 
val addafter : claset * (string * (int > tactic)) > claset 
5523  67 
val addD2 : claset * (string * thm) > claset 
68 
val addE2 : claset * (string * thm) > claset 

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

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

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

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

73 

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

74 
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

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

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

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

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

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

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

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

82 

9938  83 
val fast_tac : claset > int > tactic 
84 
val slow_tac : claset > int > tactic 

85 
val weight_ASTAR : int ref 

86 
val astar_tac : claset > int > tactic 

87 
val slow_astar_tac : claset > int > tactic 

88 
val best_tac : claset > int > tactic 

89 
val first_best_tac : claset > int > tactic 

90 
val slow_best_tac : claset > int > tactic 

91 
val depth_tac : claset > int > int > tactic 

92 
val deepen_tac : claset > int > int > tactic 

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

93 

9938  94 
val contr_tac : int > tactic 
95 
val dup_elim : thm > thm 

96 
val dup_intr : thm > thm 

97 
val dup_step_tac : claset > int > tactic 

98 
val eq_mp_tac : int > tactic 

99 
val haz_step_tac : claset > int > tactic 

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

101 
val mp_tac : int > tactic 

102 
val safe_tac : claset > tactic 

103 
val safe_steps_tac : claset > int > tactic 

104 
val safe_step_tac : claset > int > tactic 

105 
val clarify_tac : claset > int > tactic 

106 
val clarify_step_tac : claset > int > tactic 

107 
val step_tac : claset > int > tactic 

108 
val slow_step_tac : claset > int > tactic 

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

110 
val swapify : thm list > thm list 

111 
val swap_res_tac : thm list > int > tactic 

112 
val inst_step_tac : claset > int > tactic 

113 
val inst0_step_tac : claset > int > tactic 

114 
val instp_step_tac : claset > int > tactic 

1724  115 

9938  116 
val AddDs : thm list > unit 
117 
val AddEs : thm list > unit 

118 
val AddIs : thm list > unit 

119 
val AddSDs : thm list > unit 

120 
val AddSEs : thm list > unit 

121 
val AddSIs : thm list > unit 

122 
val Delrules : thm list > unit 

123 
val Safe_tac : tactic 

124 
val Safe_step_tac : int > tactic 

125 
val Clarify_tac : int > tactic 

126 
val Clarify_step_tac : int > tactic 

127 
val Step_tac : int > tactic 

128 
val Fast_tac : int > tactic 

129 
val Best_tac : int > tactic 

130 
val Slow_tac : int > tactic 

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

133 
end; 
1724  134 

5841  135 
signature CLASSICAL = 
136 
sig 

137 
include BASIC_CLASSICAL 

138 
val print_local_claset: Proof.context > unit 

139 
val get_local_claset: Proof.context > claset 

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

141 
val safe_dest_global: theory attribute 

142 
val safe_elim_global: theory attribute 

143 
val safe_intro_global: theory attribute 

6955  144 
val haz_dest_global: theory attribute 
145 
val haz_elim_global: theory attribute 

146 
val haz_intro_global: theory attribute 

9938  147 
val rule_del_global: theory attribute 
6955  148 
val safe_dest_local: Proof.context attribute 
149 
val safe_elim_local: Proof.context attribute 

150 
val safe_intro_local: Proof.context attribute 

5885  151 
val haz_dest_local: Proof.context attribute 
152 
val haz_elim_local: Proof.context attribute 

153 
val haz_intro_local: Proof.context attribute 

9938  154 
val rule_del_local: Proof.context attribute 
7272  155 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  156 
val cla_meth: (claset > tactic) > thm list > Proof.context > Proof.method 
157 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 

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

5841  160 
val setup: (theory > theory) list 
161 
end; 

162 

0  163 

5927  164 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  165 
struct 
166 

7354  167 
local open Data in 
0  168 

1800  169 
(*** Useful tactics for classical reasoning ***) 
0  170 

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

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

10736  177 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  178 
(eq_assume_tac ORELSE' assume_tac); 
0  179 

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

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

181 
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

182 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  183 

184 
(*Like mp_tac but instantiates no variables*) 

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

185 
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

186 

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

0  189 

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

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

192 

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

194 
trying rules in order. *) 

10736  195 
fun swap_res_tac rls = 
54  196 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
10736  197 
in assume_tac ORELSE' 
198 
contr_tac ORELSE' 

54  199 
biresolve_tac (foldr addrl (rls,[])) 
0  200 
end; 
201 

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

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

203 
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

204 

6967  205 
fun dup_elim th = 
206 
(case try 

207 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

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

209 
Some th' => th' 

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

0  211 

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

212 

1800  213 
(**** Classical rule sets ****) 
0  214 

215 
datatype claset = 

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

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

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

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

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

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

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

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

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

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

0  227 

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

228 
(*Desired invariants are 
9938  229 
safe0_netpair = build safe0_brls, 
230 
safep_netpair = build safep_brls, 

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

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

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

234 

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

236 
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

237 
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

238 
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

239 
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

240 
*) 
0  241 

6502  242 
val empty_netpair = (Net.empty, Net.empty); 
243 

10736  244 
val empty_cs = 
9938  245 
CS{safeIs = [], 
246 
safeEs = [], 

247 
hazIs = [], 

248 
hazEs = [], 

4651  249 
swrappers = [], 
250 
uwrappers = [], 

6502  251 
safe0_netpair = empty_netpair, 
252 
safep_netpair = empty_netpair, 

253 
haz_netpair = empty_netpair, 

6955  254 
dup_netpair = empty_netpair, 
255 
xtra_netpair = empty_netpair}; 

0  256 

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

257 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
3546  258 
let val pretty_thms = map Display.pretty_thm in 
9760  259 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 
260 
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), 

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

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

262 
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs)] 
8727  263 
> Pretty.chunks > Pretty.writeln 
3546  264 
end; 
0  265 

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

267 

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

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

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

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

274 

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

275 

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

277 

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

278 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  279 
***) 
0  280 

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

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

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

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

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

285 

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

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

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

288 

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

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

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

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

295 

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

296 
fun tag_brls_simple k [] = [] 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

297 
 tag_brls_simple k (brl::brls) = (k, brl) :: tag_brls_simple (k+1) brls; 
10736  298 

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

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

300 

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

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

302 
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

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

304 
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

305 
fun insert_simple (nI, nE) = insert_tagged_list o tag_brls_simple (~(nI + nE)) o joinrules_simple; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

306 

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

307 
fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl (brls, netpr); 
12362  308 
fun delete x = delete_tagged_list (joinrules x); 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

309 
fun delete_simple x = delete_tagged_list (joinrules_simple x); 
1800  310 

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

311 
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

312 
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

313 

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

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

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

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

319 
else if mem_thm (th, safeEs) then 
9408  320 
warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) 
10736  321 
else if mem_thm (th, hazIs) then 
9760  322 
warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) 
10736  323 
else if mem_thm (th, hazEs) then 
9760  324 
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

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

326 

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

327 

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

329 

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

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

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

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

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

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

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

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

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

343 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  344 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
345 
safeEs = safeEs, 

346 
hazIs = hazIs, 

347 
hazEs = hazEs, 

348 
swrappers = swrappers, 

349 
uwrappers = uwrappers, 

350 
haz_netpair = haz_netpair, 

351 
dup_netpair = dup_netpair, 

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

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

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

354 

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

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

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

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

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

362 
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

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

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

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

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

368 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  369 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
370 
safeIs = safeIs, 

371 
hazIs = hazIs, 

372 
hazEs = hazEs, 

373 
swrappers = swrappers, 

374 
uwrappers = uwrappers, 

375 
haz_netpair = haz_netpair, 

376 
dup_netpair = dup_netpair, 

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

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

378 
end; 
0  379 

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

380 
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

381 

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

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

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

384 

9938  385 
fun cs addSDs ths = cs addSEs (map Data.make_elim ths); 
0  386 

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

387 

1800  388 
(*** Hazardous (unsafe) rules ***) 
0  389 

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

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

10736  393 
if mem_thm (th, hazIs) then 
9938  394 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
395 
cs) 

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

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

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

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

399 
in warn_dup th cs; 
9938  400 
CS{hazIs = th::hazIs, 
401 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 

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

10736  403 
safeIs = safeIs, 
9938  404 
safeEs = safeEs, 
405 
hazEs = hazEs, 

406 
swrappers = swrappers, 

407 
uwrappers = uwrappers, 

408 
safe0_netpair = safe0_netpair, 

409 
safep_netpair = safep_netpair, 

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

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

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

412 

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

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

10736  416 
if mem_thm (th, hazEs) then 
9938  417 
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); 
418 
cs) 

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

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

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

422 
in warn_dup th cs; 
9938  423 
CS{hazEs = th::hazEs, 
424 
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, 

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

10736  426 
safeIs = safeIs, 
9938  427 
safeEs = safeEs, 
428 
hazIs = hazIs, 

429 
swrappers = swrappers, 

430 
uwrappers = uwrappers, 

431 
safe0_netpair = safe0_netpair, 

432 
safep_netpair = safep_netpair, 

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

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

434 
end; 
0  435 

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

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

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

438 

9938  439 
fun cs addDs ths = cs addEs (map Data.make_elim ths); 
0  440 

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

441 

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

445 
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

446 
searches in all the lists and chooses the relevant delXX functions. 
1800  447 
***) 
448 

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

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

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

454 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  455 
safep_netpair = delete (safep_rls, []) safep_netpair, 
456 
safeIs = rem_thm (safeIs,th), 

457 
safeEs = safeEs, 

458 
hazIs = hazIs, 

459 
hazEs = hazEs, 

460 
swrappers = swrappers, 

461 
uwrappers = uwrappers, 

462 
haz_netpair = haz_netpair, 

463 
dup_netpair = dup_netpair, 

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

464 
xtra_netpair = delete_simple ([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

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

466 
else cs; 
1800  467 

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

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

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

471 
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

472 
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

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

476 
safeEs = rem_thm (safeEs,th), 

477 
hazIs = hazIs, 

478 
hazEs = hazEs, 

479 
swrappers = swrappers, 

480 
uwrappers = uwrappers, 

481 
haz_netpair = haz_netpair, 

482 
dup_netpair = dup_netpair, 

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

483 
xtra_netpair = delete_simple ([], [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

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

485 
else cs; 
1800  486 

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 delI 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, hazIs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

492 
CS{haz_netpair = delete ([th], []) haz_netpair, 
9938  493 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
10736  494 
safeIs = safeIs, 
9938  495 
safeEs = safeEs, 
496 
hazIs = rem_thm (hazIs,th), 

497 
hazEs = hazEs, 

498 
swrappers = swrappers, 

499 
uwrappers = uwrappers, 

500 
safe0_netpair = safe0_netpair, 

501 
safep_netpair = safep_netpair, 

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

502 
xtra_netpair = delete_simple ([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

503 
else cs; 
1800  504 

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

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

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

508 
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

509 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
9938  510 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
10736  511 
safeIs = safeIs, 
9938  512 
safeEs = safeEs, 
513 
hazIs = hazIs, 

514 
hazEs = rem_thm (hazEs,th), 

515 
swrappers = swrappers, 

516 
uwrappers = uwrappers, 

517 
safe0_netpair = safe0_netpair, 

518 
safep_netpair = safep_netpair, 

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

519 
xtra_netpair = delete_simple ([], [th]) xtra_netpair} 
6955  520 
else cs; 
521 

1800  522 

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

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

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

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

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

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

529 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
9938  530 
else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs) 
531 
end; 

1800  532 

533 
val op delrules = foldl delrule; 

534 

535 

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

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

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

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

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

542 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  543 
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

544 

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

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

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

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

550 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  551 
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

552 

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

553 

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

555 
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => 
9721  556 
overwrite_warn (swrappers, new_swrapper) 
557 
("Overwriting safe wrapper " ^ fst new_swrapper)); 

4651  558 

559 
(*Add/replace an unsafe wrapper*) 

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

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

563 

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

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

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

569 

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

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

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

573 
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

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

575 

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

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

581 

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

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

587 

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

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

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

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

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

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

595 
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

596 

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

599 
treatment of priority might get muddled up.*) 

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

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

601 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) = 
1711  602 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 
603 
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) 

2630  604 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
605 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

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

606 
val cs1 = cs addSIs safeIs' 
9938  607 
addSEs safeEs' 
608 
addIs hazIs' 

609 
addEs hazEs' 

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

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

611 
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); 
10736  612 
in cs3 
1711  613 
end; 
614 

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

615 

1800  616 
(**** Simple tactics for theorem proving ****) 
0  617 

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

10736  619 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  620 
appSWrappers cs (FIRST' [ 
9938  621 
eq_assume_tac, 
622 
eq_mp_tac, 

623 
bimatch_from_nets_tac safe0_netpair, 

624 
FIRST' hyp_subst_tacs, 

625 
bimatch_from_nets_tac safep_netpair]); 

0  626 

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

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

633 

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

634 

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

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

636 

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

637 
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

638 

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

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

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

643 

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

644 
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

645 
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

646 

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

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

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

649 
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

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

651 

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

652 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  653 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  654 
appSWrappers cs (FIRST' [ 
9938  655 
eq_assume_contr_tac, 
656 
bimatch_from_nets_tac safe0_netpair, 

657 
FIRST' hyp_subst_tacs, 

658 
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

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

660 

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

661 
fun 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

662 

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

663 

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

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

665 

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

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

668 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  669 
assume_tac APPEND' 
670 
contr_tac APPEND' 

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

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

672 

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

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

675 
biresolve_from_nets_tac safep_netpair; 
0  676 

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

678 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  679 

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

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

682 

0  683 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  684 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  685 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  686 

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

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

10736  689 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  690 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  691 

1800  692 
(**** The following tactics all fail unless they solve one goal ****) 
0  693 

694 
(*Dumb but fast*) 

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

695 
fun fast_tac cs = 
11754  696 
ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  697 

698 
(*Slower but smarter than fast_tac*) 

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

699 
fun best_tac cs = 
11754  700 
ObjectLogic.atomize_tac THEN' 
0  701 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
702 

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

704 
fun first_best_tac cs = 
11754  705 
ObjectLogic.atomize_tac THEN' 
9402  706 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
707 

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

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

710 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  711 

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

712 
fun slow_best_tac cs = 
11754  713 
ObjectLogic.atomize_tac THEN' 
0  714 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
715 

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

716 

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

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

719 

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

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

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

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

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

725 

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

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

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

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

731 

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

733 
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

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

736 

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

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

738 
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

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

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

742 

5523  743 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  744 
local 
10736  745 
fun slow_step_tac' cs = appWrappers cs 
9938  746 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  747 
in fun depth_tac cs m i state = SELECT_GOAL 
748 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  752 
)) i state; 
753 
end; 

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

754 

10736  755 
(*Search, with depth bound m. 
2173  756 
This is the "entry point", which does safe inferences first.*) 
10736  757 
fun safe_depth_tac cs m = 
758 
SUBGOAL 

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

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

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

10736  763 
[] => DETERM 
9938  764 
 _::_ => I 
10736  765 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  766 
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

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

768 

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

769 
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

770 

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

771 

1724  772 

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

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

774 

7354  775 
(* theory data kind 'Provers/claset' *) 
1724  776 

7354  777 
structure GlobalClasetArgs = 
778 
struct 

779 
val name = "Provers/claset"; 

780 
type T = claset ref; 

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

781 

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

6556  784 
val prep_ext = copy; 
7354  785 
fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2)); 
786 
fun print _ (ref cs) = print_cs cs; 

787 
end; 

1724  788 

7354  789 
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); 
790 
val print_claset = GlobalClaset.print; 

791 
val claset_ref_of_sg = GlobalClaset.get_sg; 

792 
val claset_ref_of = GlobalClaset.get; 

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

793 

1724  794 

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

795 
(* access claset *) 
1724  796 

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

797 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  798 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  799 

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

802 

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

805 

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

806 

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

807 
(* change claset *) 
1800  808 

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

809 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  810 

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

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

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

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

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

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

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

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

818 

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

819 

5841  820 
(* proof data kind 'Provers/claset' *) 
821 

822 
structure LocalClasetArgs = 

823 
struct 

824 
val name = "Provers/claset"; 

825 
type T = claset; 

826 
val init = claset_of; 

827 
fun print _ cs = print_cs cs; 

828 
end; 

829 

830 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

831 
val print_local_claset = LocalClaset.print; 

832 
val get_local_claset = LocalClaset.get; 

833 
val put_local_claset = LocalClaset.put; 

834 

835 

5885  836 
(* attributes *) 
837 

838 
fun change_global_cs f (thy, th) = 

839 
let val r = claset_ref_of thy 

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

842 
fun change_local_cs f (ctxt, th) = 

6096  843 
let val cs = f (get_local_claset ctxt, [th]) 
5885  844 
in (put_local_claset cs ctxt, th) end; 
845 

846 
val safe_dest_global = change_global_cs (op addSDs); 

847 
val safe_elim_global = change_global_cs (op addSEs); 

848 
val safe_intro_global = change_global_cs (op addSIs); 

6955  849 
val haz_dest_global = change_global_cs (op addDs); 
850 
val haz_elim_global = change_global_cs (op addEs); 

851 
val haz_intro_global = change_global_cs (op addIs); 

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

852 
val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; 
5885  853 

6955  854 
val safe_dest_local = change_local_cs (op addSDs); 
855 
val safe_elim_local = change_local_cs (op addSEs); 

856 
val safe_intro_local = change_local_cs (op addSIs); 

5885  857 
val haz_dest_local = change_local_cs (op addDs); 
858 
val haz_elim_local = change_local_cs (op addEs); 

859 
val haz_intro_local = change_local_cs (op addIs); 

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

860 
val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; 
5885  861 

862 

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

863 
(* tactics referring to the implicit claset *) 
1800  864 

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

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

868 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  869 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
870 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  876 

1800  877 

10736  878 
end; 
5841  879 

880 

881 

5885  882 
(** concrete syntax of attributes **) 
5841  883 

884 
(* add / del rules *) 

885 

886 
val introN = "intro"; 

887 
val elimN = "elim"; 

888 
val destN = "dest"; 

9938  889 
val ruleN = "rule"; 
5841  890 

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

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

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

893 
Scan.succeed haz)); 
5841  894 

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

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

897 

898 
(* setup_attrs *) 

899 

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

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

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

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

904 
"destruct rule turned into elimination rule format (classical)"), 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

907 
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

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

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

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

911 
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

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

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

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

915 
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

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

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

918 
"remove declaration of intro/elim/dest rule")]; 
5841  919 

920 

921 

7230  922 
(** proof methods **) 
923 

924 
(* METHOD_CLASET' *) 

5841  925 

8098  926 
fun METHOD_CLASET' tac ctxt = 
10394  927 
Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt)); 
7230  928 

929 

930 
local 

931 

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

932 
fun may_unify t net = map snd (Tactic.orderlist (Net.unify_term net t)); 
5841  933 

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

934 
fun find_erules [] = K [] 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

935 
 find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact))); 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

936 
fun find_irules goal = may_unify (Logic.strip_assums_concl goal); 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

937 
fun find_rules (inet, enet) facts goal = find_erules facts enet @ find_irules goal inet; 
5841  938 

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

939 
fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) => 
5841  940 
let 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

941 
val [rules1, rules2, rules4] = ContextRules.find_rules ctxt facts goal; 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

942 
val rules3 = find_rules xtra_netpair facts goal; 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

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

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

947 
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

948 
end); 
5841  949 

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

950 
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts 
10394  951 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 
7281  952 

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

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

955 
AxClass.default_intro_classes_tac facts; 
10309  956 

7230  957 
in 
7281  958 
val rule = METHOD_CLASET' o rule_tac; 
10394  959 
val default = METHOD_CLASET' o default_tac; 
7230  960 
end; 
5841  961 

962 

7230  963 
(* contradiction method *) 
6502  964 

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

967 

968 
(* automatic methods *) 

5841  969 

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

971 
[Args.$$$ destN  Args.bang_colon >> K ((I, safe_dest_local): Method.modifier), 
10034  972 
Args.$$$ destN  Args.colon >> K (I, haz_dest_local), 
973 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim_local), 

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

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

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

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

5927  978 

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

7132  981 

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

7559  985 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
986 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  987 

988 

989 

990 
(** setup_methods **) 

991 

992 
val setup_methods = Method.add_methods 

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

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

994 
("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"), 
6502  995 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
10821  996 
("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"), 
7004  997 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  998 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  999 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
10821  1000 
("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")]; 
5841  1001 

1002 

1003 

1004 
(** theory setup **) 

1005 

7354  1006 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1007 

1008 

8667  1009 

1010 
(** outer syntax **) 

1011 

1012 
val print_clasetP = 

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

1014 
OuterSyntax.Keyword.diag 

9513  1015 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1016 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1017 

1018 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1019 

1020 

5841  1021 
end; 