author  wenzelm 
Sat, 06 Oct 2007 16:50:04 +0200  
changeset 24867  e5b55d7be9bb 
parent 24358  d75af3e90e82 
child 26412  0918f5c0bbca 
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 
9938  30 
val mp : thm (* [ P>Q; P ] ==> Q *) 
31 
val not_elim : thm (* [ ~P; P ] ==> R *) 

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

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

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

35 
end; 
0  36 

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

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

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

41 
val print_cs: claset > unit 
4380  42 
val print_claset: theory > unit 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

9938  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 

17880  74 
val change_claset_of: theory > (claset > claset) > unit 
75 
val change_claset: (claset > claset) > unit 

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

76 
val claset_of: theory > claset 
17880  77 
val claset: unit > claset 
4079
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 
15036  80 
val local_claset_of : Proof.context > claset 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

81 

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

84 
val weight_ASTAR : int ref 

85 
val astar_tac : claset > int > tactic 

86 
val slow_astar_tac : claset > int > tactic 

87 
val best_tac : claset > int > tactic 

88 
val first_best_tac : claset > int > tactic 

89 
val slow_best_tac : claset > int > tactic 

90 
val depth_tac : claset > int > int > tactic 

91 
val deepen_tac : claset > int > int > tactic 

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

92 

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

95 
val dup_intr : thm > thm 

96 
val dup_step_tac : claset > int > tactic 

97 
val eq_mp_tac : int > tactic 

98 
val haz_step_tac : claset > int > tactic 

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

100 
val mp_tac : int > tactic 

101 
val safe_tac : claset > tactic 

102 
val safe_steps_tac : claset > int > tactic 

103 
val safe_step_tac : claset > int > tactic 

104 
val clarify_tac : claset > int > tactic 

105 
val clarify_step_tac : claset > int > tactic 

106 
val step_tac : claset > int > tactic 

107 
val slow_step_tac : claset > int > tactic 

108 
val swapify : thm list > thm list 

109 
val swap_res_tac : thm list > int > tactic 

110 
val inst_step_tac : claset > int > tactic 

111 
val inst0_step_tac : claset > int > tactic 

112 
val instp_step_tac : claset > int > tactic 

1724  113 

9938  114 
val AddDs : thm list > unit 
115 
val AddEs : thm list > unit 

116 
val AddIs : thm list > unit 

117 
val AddSDs : thm list > unit 

118 
val AddSEs : thm list > unit 

119 
val AddSIs : thm list > unit 

120 
val Delrules : thm list > unit 

121 
val Safe_tac : tactic 

122 
val Safe_step_tac : int > tactic 

123 
val Clarify_tac : int > tactic 

124 
val Clarify_step_tac : int > tactic 

125 
val Step_tac : int > tactic 

126 
val Fast_tac : int > tactic 

127 
val Best_tac : int > tactic 

128 
val Slow_tac : int > tactic 

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

131 
end; 
1724  132 

5841  133 
signature CLASSICAL = 
134 
sig 

135 
include BASIC_CLASSICAL 

18374  136 
val swap: thm (* ~P ==> (~Q ==> P) ==> Q *) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

137 
val classical_rule: thm > thm 
15036  138 
val add_context_safe_wrapper: string * (Proof.context > wrapper) > theory > theory 
139 
val del_context_safe_wrapper: string > theory > theory 

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

141 
val del_context_unsafe_wrapper: string > theory > theory 

17880  142 
val get_claset: theory > claset 
5841  143 
val get_local_claset: Proof.context > claset 
144 
val put_local_claset: claset > Proof.context > Proof.context 

22846  145 
val print_local_claset: Proof.context > unit 
24021  146 
val get_cs: Context.generic > claset 
147 
val map_cs: (claset > claset) > Context.generic > Context.generic 

18728  148 
val safe_dest: int option > attribute 
149 
val safe_elim: int option > attribute 

150 
val safe_intro: int option > attribute 

151 
val haz_dest: int option > attribute 

152 
val haz_elim: int option > attribute 

153 
val haz_intro: int option > attribute 

154 
val rule_del: 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 

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

18708  160 
val setup: theory > theory 
5841  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 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

169 
(** classical elimination rules **) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

170 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

171 
(* 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

172 
Classical reasoning requires stronger elimination rules. For 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

173 
instance, make_elim of Pure transforms the HOL rule injD into 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

174 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

175 
[ inj f; f x = f y; x = y ==> PROP W ] ==> PROP W 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

176 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

177 
Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

178 
FAILED"; classical_rule will strenthen this to 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

179 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

180 
[ inj f; ~ W ==> f x = f y; x = y ==> W ] ==> W 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

181 
*) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

182 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

183 
fun classical_rule rule = 
19257  184 
if ObjectLogic.is_elim rule then 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

185 
let 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

186 
val rule' = rule RS classical; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

187 
val concl' = Thm.concl_of rule'; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

188 
fun redundant_hyp goal = 
19257  189 
concl' aconv Logic.strip_assums_concl goal orelse 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

190 
(case Logic.strip_assums_hyp goal of 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

191 
hyp :: hyps => exists (fn t => t aconv hyp) hyps 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

192 
 _ => false); 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

193 
val rule'' = 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

194 
rule' > ALLGOALS (SUBGOAL (fn (goal, i) => 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

195 
if i = 1 orelse redundant_hyp goal 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

196 
then Tactic.etac thin_rl i 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

197 
else all_tac)) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

198 
> Seq.hd 
21963  199 
> Drule.zero_var_indexes; 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset

200 
in if Thm.equiv_thm (rule, rule'') then rule else rule'' end 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

201 
else rule; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

202 

23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

203 
(*flatten nested meta connectives in prems*) 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

204 
val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems); 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

205 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

206 

1800  207 
(*** Useful tactics for classical reasoning ***) 
0  208 

1524  209 
val imp_elim = (*cannot use bind_thm within a structure!*) 
18586
588e80289658
store_thm: transfer to current context, i.e. the target theory;
wenzelm
parents:
18571
diff
changeset

210 
store_thm ("imp_elim", Thm.transfer (the_context ()) (classical_rule (Tactic.make_elim mp))); 
0  211 

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

10736  215 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  216 
(eq_assume_tac ORELSE' assume_tac); 
0  217 

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

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

219 
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

220 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  221 

222 
(*Like mp_tac but instantiates no variables*) 

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

223 
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

224 

1524  225 
val swap = 
18586
588e80289658
store_thm: transfer to current context, i.e. the target theory;
wenzelm
parents:
18571
diff
changeset

226 
store_thm ("swap", Thm.transfer (the_context ()) 
588e80289658
store_thm: transfer to current context, i.e. the target theory;
wenzelm
parents:
18571
diff
changeset

227 
(rule_by_tactic (etac thin_rl 1) (not_elim RS classical))); 
0  228 

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

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

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

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

234 
trying rules in order. *) 

10736  235 
fun swap_res_tac rls = 
54  236 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
10736  237 
in assume_tac ORELSE' 
238 
contr_tac ORELSE' 

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

239 
biresolve_tac (foldr addrl [] rls) 
0  240 
end; 
241 

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

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

243 
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

244 

6967  245 
fun dup_elim th = 
13525  246 
rule_by_tactic (TRYALL (etac revcut_rl)) 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

247 
((th RSN (2, revcut_rl)) > assumption 2 > Seq.hd); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

248 

1800  249 
(**** Classical rule sets ****) 
0  250 

251 
datatype claset = 

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

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

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

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

9938  257 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  258 
safe0_netpair : netpair, (*nets for trivial cases*) 
259 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

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

0  263 

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

264 
(*Desired invariants are 
9938  265 
safe0_netpair = build safe0_brls, 
266 
safep_netpair = build safep_brls, 

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

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

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

270 

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

272 
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

273 
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

274 
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

275 
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

276 
*) 
0  277 

6502  278 
val empty_netpair = (Net.empty, Net.empty); 
279 

10736  280 
val empty_cs = 
9938  281 
CS{safeIs = [], 
282 
safeEs = [], 

283 
hazIs = [], 

284 
hazEs = [], 

4651  285 
swrappers = [], 
286 
uwrappers = [], 

6502  287 
safe0_netpair = empty_netpair, 
288 
safep_netpair = empty_netpair, 

289 
haz_netpair = empty_netpair, 

6955  290 
dup_netpair = empty_netpair, 
291 
xtra_netpair = empty_netpair}; 

0  292 

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

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

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

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

8727  301 
> Pretty.chunks > Pretty.writeln 
3546  302 
end; 
0  303 

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

305 

22674  306 
fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers; 
307 
fun appWrappers (CS {uwrappers, ...}) = fold snd uwrappers; 

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

308 

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

309 

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

311 

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

312 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  313 
***) 
0  314 

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

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

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

317 
fun joinrules (intrs, elims) = 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

319 

12401  320 
fun joinrules' (intrs, elims) = 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

322 

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

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

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

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

329 

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

10736  332 

23178  333 
fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

334 

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

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

336 
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

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

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

340 

23178  341 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  342 
fun delete x = delete_tagged_list (joinrules x); 
12401  343 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  344 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset

345 
val mem_thm = member Thm.eq_thm_prop 
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset

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

347 

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

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

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

350 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
18691  351 
if mem_thm safeIs th then 
9938  352 
warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) 
18691  353 
else if mem_thm safeEs th then 
9408  354 
warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) 
18691  355 
else if mem_thm hazIs th then 
9760  356 
warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) 
18691  357 
else if mem_thm hazEs th then 
9760  358 
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

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

360 

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

361 

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

363 

18691  364 
fun addSI w th 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

365 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

366 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  367 
if mem_thm safeIs th then 
9938  368 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); 
369 
cs) 

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

370 
else 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

371 
let val th' = flat_rule th 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

372 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

373 
List.partition Thm.no_prems [th'] 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

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

381 
hazIs = hazIs, 

382 
hazEs = hazEs, 

383 
swrappers = swrappers, 

384 
uwrappers = uwrappers, 

385 
haz_netpair = haz_netpair, 

386 
dup_netpair = dup_netpair, 

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

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

389 

18691  390 
fun addSE w th 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

391 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

392 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  393 
if mem_thm safeEs th then 
9938  394 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); 
395 
cs) 

18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

396 
else if has_fewer_prems 1 th then 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

397 
error("Illformed elimination rule\n" ^ string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

398 
else 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

399 
let 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

400 
val th' = classical_rule (flat_rule th) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

401 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

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

407 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  408 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
409 
safeIs = safeIs, 

410 
hazIs = hazIs, 

411 
hazEs = hazEs, 

412 
swrappers = swrappers, 

413 
uwrappers = uwrappers, 

414 
haz_netpair = haz_netpair, 

415 
dup_netpair = dup_netpair, 

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

417 
end; 
0  418 

18691  419 
fun cs addSIs ths = fold_rev (addSI NONE) ths cs; 
420 
fun cs addSEs ths = fold_rev (addSE NONE) ths cs; 

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

421 

21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

422 
fun make_elim th = 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

423 
if has_fewer_prems 1 th then 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

424 
error("Illformed destruction rule\n" ^ string_of_thm th) 
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

425 
else Tactic.make_elim th; 
17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

426 

21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

427 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
0  428 

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

429 

1800  430 
(*** Hazardous (unsafe) rules ***) 
0  431 

18691  432 
fun addI w th 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

433 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

434 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  435 
if mem_thm hazIs th then 
9938  436 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
437 
cs) 

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

438 
else 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

439 
let val th' = flat_rule th 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

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

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

442 
in warn_dup th cs; 
9938  443 
CS{hazIs = th::hazIs, 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

444 
haz_netpair = insert (nI,nE) ([th'], []) haz_netpair, 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

445 
dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair, 
10736  446 
safeIs = safeIs, 
9938  447 
safeEs = safeEs, 
448 
hazEs = hazEs, 

449 
swrappers = swrappers, 

450 
uwrappers = uwrappers, 

451 
safe0_netpair = safe0_netpair, 

452 
safep_netpair = safep_netpair, 

18691  453 
xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair} 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

454 
end 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

455 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

456 
error ("Illformed introduction rule\n" ^ string_of_thm th); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

457 

18691  458 
fun addE w th 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

459 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

460 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  461 
if mem_thm hazEs th then 
9938  462 
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); 
463 
cs) 

18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

464 
else if has_fewer_prems 1 th then 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

465 
error("Illformed elimination rule\n" ^ string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

466 
else 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

467 
let 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

468 
val th' = classical_rule (flat_rule th) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

471 
in warn_dup th cs; 
9938  472 
CS{hazEs = th::hazEs, 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

473 
haz_netpair = insert (nI,nE) ([], [th']) haz_netpair, 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

474 
dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair, 
10736  475 
safeIs = safeIs, 
9938  476 
safeEs = safeEs, 
477 
hazIs = hazIs, 

478 
swrappers = swrappers, 

479 
uwrappers = uwrappers, 

480 
safe0_netpair = safe0_netpair, 

481 
safep_netpair = safep_netpair, 

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

483 
end; 
0  484 

18691  485 
fun cs addIs ths = fold_rev (addI NONE) ths cs; 
486 
fun cs addEs ths = fold_rev (addE NONE) ths cs; 

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

487 

21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

488 
fun cs addDs ths = cs addEs (map make_elim ths); 
0  489 

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

490 

10736  491 
(*** Deletion of rules 
1800  492 
Working out what to delete, requires repeating much of the code used 
9938  493 
to insert. 
1800  494 
***) 
495 

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

497 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  498 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  499 
if mem_thm safeIs th then 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

500 
let val th' = flat_rule th 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

501 
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'] 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

502 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  503 
safep_netpair = delete (safep_rls, []) safep_netpair, 
18691  504 
safeIs = rem_thm th safeIs, 
9938  505 
safeEs = safeEs, 
506 
hazIs = hazIs, 

507 
hazEs = hazEs, 

508 
swrappers = swrappers, 

509 
uwrappers = uwrappers, 

510 
haz_netpair = haz_netpair, 

511 
dup_netpair = dup_netpair, 

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

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

514 
else cs; 
1800  515 

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

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

517 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  518 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  519 
if mem_thm safeEs th then 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

520 
let 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

521 
val th' = classical_rule (flat_rule th) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

522 
val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th'] 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

523 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  524 
safep_netpair = delete ([], safep_rls) safep_netpair, 
525 
safeIs = safeIs, 

18691  526 
safeEs = rem_thm th safeEs, 
9938  527 
hazIs = hazIs, 
528 
hazEs = hazEs, 

529 
swrappers = swrappers, 

530 
uwrappers = uwrappers, 

531 
haz_netpair = haz_netpair, 

532 
dup_netpair = dup_netpair, 

12401  533 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

534 
end 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

535 
else cs; 
1800  536 

537 

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

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

539 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  540 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  541 
if mem_thm hazIs th then 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

542 
let val th' = flat_rule th 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

543 
in CS{haz_netpair = delete ([th'], []) haz_netpair, 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

544 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
10736  545 
safeIs = safeIs, 
9938  546 
safeEs = safeEs, 
18691  547 
hazIs = rem_thm th hazIs, 
9938  548 
hazEs = hazEs, 
549 
swrappers = swrappers, 

550 
uwrappers = uwrappers, 

551 
safe0_netpair = safe0_netpair, 

552 
safep_netpair = safep_netpair, 

12401  553 
xtra_netpair = delete' ([th], []) xtra_netpair} 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

554 
end 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

555 
else cs 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

556 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

557 
error ("Illformed introduction rule\n" ^ string_of_thm th); 
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

558 

1800  559 

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

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

561 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  562 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

563 
if mem_thm hazEs th then 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

564 
let val th' = classical_rule (flat_rule th) 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

565 
in CS{haz_netpair = delete ([], [th']) haz_netpair, 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

566 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
10736  567 
safeIs = safeIs, 
9938  568 
safeEs = safeEs, 
569 
hazIs = hazIs, 

18691  570 
hazEs = rem_thm th hazEs, 
9938  571 
swrappers = swrappers, 
572 
uwrappers = uwrappers, 

573 
safe0_netpair = safe0_netpair, 

574 
safep_netpair = safep_netpair, 

12401  575 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

576 
end 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

577 
else cs; 
1800  578 

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

579 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

580 
fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

581 
let val th' = Tactic.make_elim th in 
18691  582 
if mem_thm safeIs th orelse mem_thm safeEs th orelse 
583 
mem_thm hazIs th orelse mem_thm hazEs th orelse 

584 
mem_thm safeEs th' orelse mem_thm hazEs th' 

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

585 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

586 
else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs) 
9938  587 
end; 
1800  588 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

589 
fun cs delrules ths = fold delrule ths cs; 
1800  590 

591 

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

592 
(*** Modifying the wrapper tacticals ***) 
22674  593 
fun map_swrappers f 
594 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

595 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

596 
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 

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

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

598 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  599 
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

600 

22674  601 
fun map_uwrappers f 
602 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

603 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

604 
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 

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

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

606 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  607 
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

608 

22674  609 
fun update_warn msg (p as (key : string, _)) xs = 
610 
(if AList.defined (op =) xs key then warning msg else (); 

611 
AList.update (op =) p xs); 

612 

613 
fun delete_warn msg (key : string) xs = 

614 
if AList.defined (op =) xs key then AList.delete (op =) key xs 

615 
else (warning msg; xs); 

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

616 

4651  617 
(*Add/replace a safe wrapper*) 
22674  618 
fun cs addSWrapper new_swrapper = map_swrappers 
619 
(update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; 

4651  620 

621 
(*Add/replace an unsafe wrapper*) 

22674  622 
fun cs addWrapper new_uwrapper = map_uwrappers 
623 
(update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; 

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

624 

4651  625 
(*Remove a safe wrapper*) 
22674  626 
fun cs delSWrapper name = map_swrappers 
627 
(delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; 

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

628 

4651  629 
(*Remove an unsafe wrapper*) 
22674  630 
fun cs delWrapper name = map_uwrappers 
631 
(delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; 

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

632 

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

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

638 

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

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

644 

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

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

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

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

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

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

652 
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

653 

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

656 
treatment of priority might get muddled up.*) 

22674  657 
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, 
24358  658 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, 
22674  659 
swrappers, uwrappers, ...}) = 
24358  660 
if pointer_eq (cs, cs') then cs 
661 
else 

662 
let 

663 
val safeIs' = fold rem_thm safeIs safeIs2; 

664 
val safeEs' = fold rem_thm safeEs safeEs2; 

665 
val hazIs' = fold rem_thm hazIs hazIs2; 

666 
val hazEs' = fold rem_thm hazEs hazEs2; 

667 
val cs1 = cs addSIs safeIs' 

668 
addSEs safeEs' 

669 
addIs hazIs' 

670 
addEs hazEs'; 

671 
val cs2 = map_swrappers 

672 
(fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1; 

673 
val cs3 = map_uwrappers 

674 
(fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2; 

675 
in cs3 end; 

1711  676 

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

677 

1800  678 
(**** Simple tactics for theorem proving ****) 
0  679 

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

10736  681 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  682 
appSWrappers cs (FIRST' [ 
9938  683 
eq_assume_tac, 
684 
eq_mp_tac, 

685 
bimatch_from_nets_tac safe0_netpair, 

686 
FIRST' hyp_subst_tacs, 

687 
bimatch_from_nets_tac safep_netpair]); 

0  688 

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

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

695 

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

696 

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

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

698 

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

699 
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

700 

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

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

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

705 

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

706 
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

707 
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

708 

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

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

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

711 
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

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

713 

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

714 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  715 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  716 
appSWrappers cs (FIRST' [ 
9938  717 
eq_assume_contr_tac, 
718 
bimatch_from_nets_tac safe0_netpair, 

719 
FIRST' hyp_subst_tacs, 

720 
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

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

722 

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

723 
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

724 

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

725 

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

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

727 

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

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

730 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  731 
assume_tac APPEND' 
732 
contr_tac APPEND' 

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

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

734 

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

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

737 
biresolve_from_nets_tac safep_netpair; 
0  738 

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

740 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  741 

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

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

744 

0  745 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  746 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  747 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  748 

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

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

10736  751 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  752 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  753 

1800  754 
(**** The following tactics all fail unless they solve one goal ****) 
0  755 

756 
(*Dumb but fast*) 

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

757 
fun fast_tac cs = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

758 
ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  759 

760 
(*Slower but smarter than fast_tac*) 

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

761 
fun best_tac cs = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

762 
ObjectLogic.atomize_prems_tac THEN' 
0  763 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
764 

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

766 
fun first_best_tac cs = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

767 
ObjectLogic.atomize_prems_tac THEN' 
9402  768 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
769 

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

770 
fun slow_tac cs = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

771 
ObjectLogic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

772 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  773 

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

774 
fun slow_best_tac cs = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

775 
ObjectLogic.atomize_prems_tac THEN' 
0  776 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
777 

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

778 

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

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

781 

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

782 
fun astar_tac cs = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

783 
ObjectLogic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

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

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

787 

10736  788 
fun slow_astar_tac cs = 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

789 
ObjectLogic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

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

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

793 

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

795 
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

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

798 

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

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

800 
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

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

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

804 

5523  805 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  806 
local 
10736  807 
fun slow_step_tac' cs = appWrappers cs 
9938  808 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  809 
in fun depth_tac cs m i state = SELECT_GOAL 
810 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  814 
)) i state; 
815 
end; 

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

816 

10736  817 
(*Search, with depth bound m. 
2173  818 
This is the "entry point", which does safe inferences first.*) 
10736  819 
fun safe_depth_tac cs m = 
820 
SUBGOAL 

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

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

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

10736  825 
[] => DETERM 
9938  826 
 _::_ => I 
10736  827 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  828 
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

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

830 

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

831 
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

832 

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

833 

1724  834 

15036  835 
(** context dependent claset components **) 
836 

837 
datatype context_cs = ContextCS of 

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

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

840 

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

842 
let 

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

844 
in 

22674  845 
cs 
846 
> fold_rev (add_wrapper (op addSWrapper)) swrappers 

15036  847 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 
848 
end; 

849 

850 
fun make_context_cs (swrappers, uwrappers) = 

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

852 

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

854 

855 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

24358  856 
if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1 
857 
else 

858 
let 

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

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

861 
val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2); 

862 
val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2); 

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

15036  864 

865 

866 

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

868 

24021  869 
(* global clasets *) 
1724  870 

16424  871 
structure GlobalClaset = TheoryDataFun 
22846  872 
( 
15036  873 
type T = claset ref * context_cs; 
874 
val empty = (ref empty_cs, empty_context_cs); 

16424  875 
fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; 
876 
val extend = copy; 

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

15036  878 
(ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2)); 
22846  879 
); 
1724  880 

22846  881 
val print_claset = print_cs o ! o #1 o GlobalClaset.get; 
17880  882 
val get_claset = ! o #1 o GlobalClaset.get; 
883 

15036  884 
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; 
885 
fun map_context_cs f = GlobalClaset.map (apsnd 

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

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

887 

17880  888 
val change_claset_of = change o #1 o GlobalClaset.get; 
22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21963
diff
changeset

889 
fun change_claset f = change_claset_of (ML_Context.the_context ()) f; 
1800  890 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

891 
fun claset_of thy = 
17880  892 
let val (cs_ref, ctxt_cs) = GlobalClaset.get thy 
21516  893 
in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end; 
22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21963
diff
changeset

894 
val claset = claset_of o ML_Context.the_context; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

895 

17880  896 
fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st; 
897 
fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st; 

1724  898 

17880  899 
fun AddDs args = change_claset (fn cs => cs addDs args); 
900 
fun AddEs args = change_claset (fn cs => cs addEs args); 

901 
fun AddIs args = change_claset (fn cs => cs addIs args); 

902 
fun AddSDs args = change_claset (fn cs => cs addSDs args); 

903 
fun AddSEs args = change_claset (fn cs => cs addSEs args); 

904 
fun AddSIs args = change_claset (fn cs => cs addSIs args); 

905 
fun Delrules args = change_claset (fn cs => cs delrules args); 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

906 

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

907 

15036  908 
(* context dependent components *) 
909 

22674  910 
fun add_context_safe_wrapper wrapper = (map_context_cs o apfst) 
911 
(AList.update (op =) wrapper); 

912 
fun del_context_safe_wrapper name = (map_context_cs o apfst) 

913 
(AList.delete (op =) name); 

15036  914 

22674  915 
fun add_context_unsafe_wrapper wrapper = (map_context_cs o apsnd) 
916 
(AList.update (op =) wrapper); 

917 
fun del_context_unsafe_wrapper name = (map_context_cs o apsnd) 

918 
(AList.delete (op =) name); 

15036  919 

920 

24021  921 
(* local clasets *) 
5841  922 

16424  923 
structure LocalClaset = ProofDataFun 
22846  924 
( 
5841  925 
type T = claset; 
17880  926 
val init = get_claset; 
22846  927 
); 
5841  928 

929 
val get_local_claset = LocalClaset.get; 

930 
val put_local_claset = LocalClaset.put; 

931 

15036  932 
fun local_claset_of ctxt = 
933 
context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt); 

934 

22846  935 
val print_local_claset = print_cs o local_claset_of; 
936 

5841  937 

24021  938 
(* generic clasets *) 
939 

940 
fun get_cs (Context.Theory thy) = claset_of thy 

941 
 get_cs (Context.Proof ctxt) = local_claset_of ctxt; 

942 

943 
fun map_cs f (Context.Theory thy) = (change_claset_of thy f; Context.Theory thy) 

944 
 map_cs f (Context.Proof ctxt) = Context.Proof (LocalClaset.map f ctxt); 

945 

946 

5885  947 
(* attributes *) 
948 

18728  949 
fun attrib f = Thm.declaration_attribute (fn th => 
18691  950 
fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy) 
951 
 Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt)); 

5885  952 

21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

953 
fun safe_dest w = attrib (addSE w o make_elim); 
18691  954 
val safe_elim = attrib o addSE; 
955 
val safe_intro = attrib o addSI; 

21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

956 
fun haz_dest w = attrib (addE w o make_elim); 
18691  957 
val haz_elim = attrib o addE; 
958 
val haz_intro = attrib o addI; 

959 
val rule_del = attrib delrule o ContextRules.rule_del; 

5885  960 

961 

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

962 
(* tactics referring to the implicit claset *) 
1800  963 

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

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

967 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  968 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
969 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  975 

1800  976 

10736  977 
end; 
5841  978 

979 

980 

5885  981 
(** concrete syntax of attributes **) 
5841  982 

983 
val introN = "intro"; 

984 
val elimN = "elim"; 

985 
val destN = "dest"; 

9938  986 
val ruleN = "rule"; 
5841  987 

988 
val setup_attrs = Attrib.add_attributes 

18728  989 
[("swapped", swapped, "classical swap of introduction rule"), 
990 
(destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query, 

18688  991 
"declaration of Classical destruction rule"), 
18728  992 
(elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query, 
18688  993 
"declaration of Classical elimination rule"), 
18728  994 
(introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query, 
18688  995 
"declaration of Classical introduction rule"), 
18728  996 
(ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del), 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

997 
"remove declaration of intro/elim/dest rule")]; 
5841  998 

999 

1000 

7230  1001 
(** proof methods **) 
1002 

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

1003 
fun METHOD_CLASET tac ctxt = 
15036  1004 
Method.METHOD (tac ctxt (local_claset_of ctxt)); 
5841  1005 

8098  1006 
fun METHOD_CLASET' tac ctxt = 
15036  1007 
Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); 
7230  1008 

1009 

1010 
local 

1011 

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

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

1016 
val rules = rules1 @ rules2 @ rules3 @ rules4; 
18223  1017 
val ruleq = Drule.multi_resolves facts rules; 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

1020 
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) 
18834  1021 
end) 
21687  1022 
THEN_ALL_NEW Goal.norm_hhf_tac; 
5841  1023 

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

1024 
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts 
10394  1025 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 
7281  1026 

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

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

1028 
HEADGOAL (rule_tac rules ctxt cs facts) ORELSE 
24218  1029 
Class.default_intro_classes_tac facts; 
10309  1030 

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

1033 
val default = METHOD_CLASET o default_tac; 
7230  1034 
end; 
5841  1035 

1036 

7230  1037 
(* contradiction method *) 
6502  1038 

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

1041 

1042 
(* automatic methods *) 

5841  1043 

5927  1044 
val cla_modifiers = 
18728  1045 
[Args.$$$ destN  Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier), 
1046 
Args.$$$ destN  Args.colon >> K (I, haz_dest NONE), 

1047 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim NONE), 

1048 
Args.$$$ elimN  Args.colon >> K (I, haz_elim NONE), 

1049 
Args.$$$ introN  Args.bang_colon >> K (I, safe_intro NONE), 

1050 
Args.$$$ introN  Args.colon >> K (I, haz_intro NONE), 

1051 
Args.del  Args.colon >> K (I, rule_del)]; 

5927  1052 

7559  1053 
fun cla_meth tac prems ctxt = Method.METHOD (fn facts => 
15036  1054 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); 
7132  1055 

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

7559  1059 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1060 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1061 

1062 

1063 

1064 
(** setup_methods **) 

1065 

1066 
val setup_methods = Method.add_methods 

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

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

1068 
("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"), 
6502  1069 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
10821  1070 
("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"), 
7004  1071 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1072 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1073 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
18015  1074 
("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"), 
10821  1075 
("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")]; 
5841  1076 

1077 

1078 

1079 
(** theory setup **) 

1080 

22846  1081 
val setup = GlobalClaset.init #> setup_attrs #> setup_methods; 
5841  1082 

1083 

8667  1084 

1085 
(** outer syntax **) 

1086 

24867  1087 
val _ = 
8667  1088 
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" 
17057  1089 
OuterKeyword.diag 
9513  1090 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
20956  1091 
(Toplevel.node_case 
1092 
(Context.cases print_claset print_local_claset) 

1093 
(print_local_claset o Proof.context_of))))); 

8667  1094 

5841  1095 
end; 