author  wenzelm 
Thu, 06 Dec 2001 00:41:37 +0100  
changeset 12401  4363432ef0cd 
parent 12376  480303e3fa08 
child 13105  3d1e7a199bdc 
permissions  rwrr 
9938  1 
(* Title: Provers/classical.ML 
0  2 
ID: $Id$ 
9938  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

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

7 
theory, etc. 

8 

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

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

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

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

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

14 
the conclusion. 

15 
*) 

16 

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

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

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

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

22 

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

23 

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

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

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

27 

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

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

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

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

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

36 
end; 
0  37 

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

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

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

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

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

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

9938  52 
val merge_cs : claset * claset > claset 
53 
val addDs : claset * thm list > claset 

54 
val addEs : claset * thm list > claset 

55 
val addIs : claset * thm list > claset 

56 
val addSDs : claset * thm list > claset 

57 
val addSEs : claset * thm list > claset 

58 
val addSIs : claset * thm list > claset 

59 
val delrules : claset * thm list > claset 

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

61 
val delSWrapper : claset * string > claset 

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

63 
val delWrapper : claset * string > claset 

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

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

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

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

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

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

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

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

74 

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

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

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

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

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

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

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

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

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

83 

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

86 
val weight_ASTAR : int ref 

87 
val astar_tac : claset > int > tactic 

88 
val slow_astar_tac : claset > int > tactic 

89 
val best_tac : claset > int > tactic 

90 
val first_best_tac : claset > int > tactic 

91 
val slow_best_tac : claset > int > tactic 

92 
val depth_tac : claset > int > int > tactic 

93 
val deepen_tac : claset > int > int > tactic 

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

94 

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

97 
val dup_intr : thm > thm 

98 
val dup_step_tac : claset > int > tactic 

99 
val eq_mp_tac : int > tactic 

100 
val haz_step_tac : claset > int > tactic 

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

102 
val mp_tac : int > tactic 

103 
val safe_tac : claset > tactic 

104 
val safe_steps_tac : claset > int > tactic 

105 
val safe_step_tac : claset > int > tactic 

106 
val clarify_tac : claset > int > tactic 

107 
val clarify_step_tac : claset > int > tactic 

108 
val step_tac : claset > int > tactic 

109 
val slow_step_tac : claset > int > tactic 

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

111 
val swapify : thm list > thm list 

112 
val swap_res_tac : thm list > int > tactic 

113 
val inst_step_tac : claset > int > tactic 

114 
val inst0_step_tac : claset > int > tactic 

115 
val instp_step_tac : claset > int > tactic 

1724  116 

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

119 
val AddIs : thm list > unit 

120 
val AddSDs : thm list > unit 

121 
val AddSEs : thm list > unit 

122 
val AddSIs : thm list > unit 

123 
val Delrules : thm list > unit 

124 
val Safe_tac : tactic 

125 
val Safe_step_tac : int > tactic 

126 
val Clarify_tac : int > tactic 

127 
val Clarify_step_tac : int > tactic 

128 
val Step_tac : int > tactic 

129 
val Fast_tac : int > tactic 

130 
val Best_tac : int > tactic 

131 
val Slow_tac : int > tactic 

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

134 
end; 
1724  135 

5841  136 
signature CLASSICAL = 
137 
sig 

138 
include BASIC_CLASSICAL 

139 
val print_local_claset: Proof.context > unit 

140 
val get_local_claset: Proof.context > claset 

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

142 
val safe_dest_global: theory attribute 

143 
val safe_elim_global: theory attribute 

144 
val safe_intro_global: theory attribute 

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

147 
val haz_intro_global: theory attribute 

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

151 
val safe_intro_local: Proof.context attribute 

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

154 
val haz_intro_local: Proof.context attribute 

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

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

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

163 

0  164 

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

7354  168 
local open Data in 
0  169 

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

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

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

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

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

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

182 
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

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

185 
(*Like mp_tac but instantiates no variables*) 

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

186 
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

187 

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

0  190 

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

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

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

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

196 
trying rules in order. *) 

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

54  201 
biresolve_tac (foldr addrl (rls,[])) 
0  202 
end; 
203 

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

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

205 
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

206 

6967  207 
fun dup_elim th = 
208 
(case try 

209 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

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

211 
Some th' => th' 

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

0  213 

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

214 

1800  215 
(**** Classical rule sets ****) 
0  216 

217 
datatype claset = 

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

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

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

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

9938  223 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  224 
safe0_netpair : netpair, (*nets for trivial cases*) 
225 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

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

0  229 

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

230 
(*Desired invariants are 
9938  231 
safe0_netpair = build safe0_brls, 
232 
safep_netpair = build safep_brls, 

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

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

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

236 

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

238 
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

239 
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

240 
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

241 
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

242 
*) 
0  243 

6502  244 
val empty_netpair = (Net.empty, Net.empty); 
245 

10736  246 
val empty_cs = 
9938  247 
CS{safeIs = [], 
248 
safeEs = [], 

249 
hazIs = [], 

250 
hazEs = [], 

4651  251 
swrappers = [], 
252 
uwrappers = [], 

6502  253 
safe0_netpair = empty_netpair, 
254 
safep_netpair = empty_netpair, 

255 
haz_netpair = empty_netpair, 

6955  256 
dup_netpair = empty_netpair, 
257 
xtra_netpair = empty_netpair}; 

0  258 

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

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

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

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

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

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

269 

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

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

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

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

276 

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

277 

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

279 

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

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

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

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

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

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

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

287 

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

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

290 

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

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

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

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

297 

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

10736  300 

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

301 
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

302 

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

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

304 
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

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

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

308 

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

309 
fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl (brls, netpr); 
12362  310 
fun delete x = delete_tagged_list (joinrules x); 
12401  311 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  312 

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

313 
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

314 
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

315 

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

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

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

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

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

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

328 

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

329 

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

331 

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

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

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

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

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

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

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

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

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

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

348 
hazIs = hazIs, 

349 
hazEs = hazEs, 

350 
swrappers = swrappers, 

351 
uwrappers = uwrappers, 

352 
haz_netpair = haz_netpair, 

353 
dup_netpair = dup_netpair, 

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

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

356 

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

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

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

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

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

364 
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

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

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

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

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

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

373 
hazIs = hazIs, 

374 
hazEs = hazEs, 

375 
swrappers = swrappers, 

376 
uwrappers = uwrappers, 

377 
haz_netpair = haz_netpair, 

378 
dup_netpair = dup_netpair, 

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

380 
end; 
0  381 

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

382 
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

383 

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

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

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

386 

9938  387 
fun cs addSDs ths = cs addSEs (map Data.make_elim ths); 
0  388 

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

389 

1800  390 
(*** Hazardous (unsafe) rules ***) 
0  391 

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

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

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

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

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

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

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

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

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

10736  405 
safeIs = safeIs, 
9938  406 
safeEs = safeEs, 
407 
hazEs = hazEs, 

408 
swrappers = swrappers, 

409 
uwrappers = uwrappers, 

410 
safe0_netpair = safe0_netpair, 

411 
safep_netpair = safep_netpair, 

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

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

414 

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

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

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

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

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

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

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

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

10736  428 
safeIs = safeIs, 
9938  429 
safeEs = safeEs, 
430 
hazIs = hazIs, 

431 
swrappers = swrappers, 

432 
uwrappers = uwrappers, 

433 
safe0_netpair = safe0_netpair, 

434 
safep_netpair = safep_netpair, 

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

436 
end; 
0  437 

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

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

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

440 

9938  441 
fun cs addDs ths = cs addEs (map Data.make_elim ths); 
0  442 

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

443 

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

447 
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

448 
searches in all the lists and chooses the relevant delXX functions. 
1800  449 
***) 
450 

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

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

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

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

459 
safeEs = safeEs, 

460 
hazIs = hazIs, 

461 
hazEs = hazEs, 

462 
swrappers = swrappers, 

463 
uwrappers = uwrappers, 

464 
haz_netpair = haz_netpair, 

465 
dup_netpair = dup_netpair, 

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

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

468 
else cs; 
1800  469 

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

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

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

473 
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

474 
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

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

478 
safeEs = rem_thm (safeEs,th), 

479 
hazIs = hazIs, 

480 
hazEs = hazEs, 

481 
swrappers = swrappers, 

482 
uwrappers = uwrappers, 

483 
haz_netpair = haz_netpair, 

484 
dup_netpair = dup_netpair, 

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

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

487 
else cs; 
1800  488 

489 

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

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

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

493 
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

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

499 
hazEs = hazEs, 

500 
swrappers = swrappers, 

501 
uwrappers = uwrappers, 

502 
safe0_netpair = safe0_netpair, 

503 
safep_netpair = safep_netpair, 

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

505 
else cs; 
1800  506 

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

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

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

510 
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

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

516 
hazEs = rem_thm (hazEs,th), 

517 
swrappers = swrappers, 

518 
uwrappers = uwrappers, 

519 
safe0_netpair = safe0_netpair, 

520 
safep_netpair = safep_netpair, 

12401  521 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
6955  522 
else cs; 
523 

1800  524 

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

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

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

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

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

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

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

1800  534 

535 
val op delrules = foldl delrule; 

536 

537 

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

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

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

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

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

544 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  545 
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

546 

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

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

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

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

552 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  553 
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

554 

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

555 

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

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

4651  560 

561 
(*Add/replace an unsafe wrapper*) 

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

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

565 

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

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

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

571 

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

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

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

575 
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

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

577 

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

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

583 

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

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

589 

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

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

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

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

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

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

597 
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

598 

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

601 
treatment of priority might get muddled up.*) 

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

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

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

2630  606 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
607 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

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

608 
val cs1 = cs addSIs safeIs' 
9938  609 
addSEs safeEs' 
610 
addIs hazIs' 

611 
addEs hazEs' 

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

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

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

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

617 

1800  618 
(**** Simple tactics for theorem proving ****) 
0  619 

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

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

625 
bimatch_from_nets_tac safe0_netpair, 

626 
FIRST' hyp_subst_tacs, 

627 
bimatch_from_nets_tac safep_netpair]); 

0  628 

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

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

635 

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

638 

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

639 
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

640 

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

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

642 
create precisely n subgoals.*) 
10736  643 
fun n_bimatch_from_nets_tac n = 
11783  644 
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

645 

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

646 
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

647 
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

648 

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

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

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

651 
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

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

653 

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

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

659 
FIRST' hyp_subst_tacs, 

660 
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

661 
bimatch2_tac safep_netpair]); 
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 
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

664 

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

665 

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

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

667 

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

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

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

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

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

674 

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

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

677 
biresolve_from_nets_tac safep_netpair; 
0  678 

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

680 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  681 

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

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

684 

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

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

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

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

1800  694 
(**** The following tactics all fail unless they solve one goal ****) 
0  695 

696 
(*Dumb but fast*) 

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

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

700 
(*Slower but smarter than fast_tac*) 

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

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

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

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

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

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

712 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  713 

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

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

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

718 

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

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

721 

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

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

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

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

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

727 

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

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

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

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

733 

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

735 
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

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

738 

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

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

740 
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

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

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

744 

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

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

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

5757  754 
)) i state; 
755 
end; 

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

756 

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

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

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

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

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

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

770 

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

771 
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

772 

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

773 

1724  774 

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

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

776 

7354  777 
(* theory data kind 'Provers/claset' *) 
1724  778 

7354  779 
structure GlobalClasetArgs = 
780 
struct 

781 
val name = "Provers/claset"; 

782 
type T = claset ref; 

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

783 

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

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

789 
end; 

1724  790 

7354  791 
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); 
792 
val print_claset = GlobalClaset.print; 

793 
val claset_ref_of_sg = GlobalClaset.get_sg; 

794 
val claset_ref_of = GlobalClaset.get; 

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

795 

1724  796 

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

797 
(* access claset *) 
1724  798 

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

799 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  800 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  801 

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

804 

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

807 

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

808 

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

809 
(* change claset *) 
1800  810 

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

811 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  812 

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

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

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

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

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

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

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

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

820 

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

821 

5841  822 
(* proof data kind 'Provers/claset' *) 
823 

824 
structure LocalClasetArgs = 

825 
struct 

826 
val name = "Provers/claset"; 

827 
type T = claset; 

828 
val init = claset_of; 

829 
fun print _ cs = print_cs cs; 

830 
end; 

831 

832 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

833 
val print_local_claset = LocalClaset.print; 

834 
val get_local_claset = LocalClaset.get; 

835 
val put_local_claset = LocalClaset.put; 

836 

837 

5885  838 
(* attributes *) 
839 

840 
fun change_global_cs f (thy, th) = 

841 
let val r = claset_ref_of thy 

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

844 
fun change_local_cs f (ctxt, th) = 

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

848 
val safe_dest_global = change_global_cs (op addSDs); 

849 
val safe_elim_global = change_global_cs (op addSEs); 

850 
val safe_intro_global = change_global_cs (op addSIs); 

6955  851 
val haz_dest_global = change_global_cs (op addDs); 
852 
val haz_elim_global = change_global_cs (op addEs); 

853 
val haz_intro_global = change_global_cs (op addIs); 

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

854 
val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; 
5885  855 

6955  856 
val safe_dest_local = change_local_cs (op addSDs); 
857 
val safe_elim_local = change_local_cs (op addSEs); 

858 
val safe_intro_local = change_local_cs (op addSIs); 

5885  859 
val haz_dest_local = change_local_cs (op addDs); 
860 
val haz_elim_local = change_local_cs (op addEs); 

861 
val haz_intro_local = change_local_cs (op addIs); 

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

862 
val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; 
5885  863 

864 

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

865 
(* tactics referring to the implicit claset *) 
1800  866 

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

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

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

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

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

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

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

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

2066  878 

1800  879 

10736  880 
end; 
5841  881 

882 

883 

5885  884 
(** concrete syntax of attributes **) 
5841  885 

886 
(* add / del rules *) 

887 

888 
val introN = "intro"; 

889 
val elimN = "elim"; 

890 
val destN = "dest"; 

9938  891 
val ruleN = "rule"; 
5841  892 

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

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

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

895 
Scan.succeed haz)); 
5841  896 

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

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

899 

900 
(* setup_attrs *) 

901 

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

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

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

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

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

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

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

910 
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

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

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

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

914 
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

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

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

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

918 
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

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

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

921 
"remove declaration of intro/elim/dest rule")]; 
5841  922 

923 

924 

7230  925 
(** proof methods **) 
926 

927 
(* METHOD_CLASET' *) 

5841  928 

8098  929 
fun METHOD_CLASET' tac ctxt = 
10394  930 
Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt)); 
7230  931 

932 

933 
local 

934 

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

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

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

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

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

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

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

943 
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

944 
end); 
5841  945 

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

946 
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts 
10394  947 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 
7281  948 

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

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

951 
AxClass.default_intro_classes_tac facts; 
10309  952 

7230  953 
in 
7281  954 
val rule = METHOD_CLASET' o rule_tac; 
10394  955 
val default = METHOD_CLASET' o default_tac; 
7230  956 
end; 
5841  957 

958 

7230  959 
(* contradiction method *) 
6502  960 

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

963 

964 
(* automatic methods *) 

5841  965 

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

967 
[Args.$$$ destN  Args.bang_colon >> K ((I, safe_dest_local): Method.modifier), 
10034  968 
Args.$$$ destN  Args.colon >> K (I, haz_dest_local), 
969 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim_local), 

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

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

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

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

5927  974 

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

7132  977 

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

7559  981 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
982 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  983 

984 

985 

986 
(** setup_methods **) 

987 

988 
val setup_methods = Method.add_methods 

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

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

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

998 

999 

1000 
(** theory setup **) 

1001 

7354  1002 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1003 

1004 

8667  1005 

1006 
(** outer syntax **) 

1007 

1008 
val print_clasetP = 

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

1010 
OuterSyntax.Keyword.diag 

9513  1011 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1012 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1013 

1014 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1015 

1016 

5841  1017 
end; 