author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18834  7e94af77cfce 
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 print_local_claset: Proof.context > unit 
144 
val get_local_claset: Proof.context > claset 

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

18728  146 
val safe_dest: int option > attribute 
147 
val safe_elim: int option > attribute 

148 
val safe_intro: int option > attribute 

149 
val haz_dest: int option > attribute 

150 
val haz_elim: int option > attribute 

151 
val haz_intro: int option > attribute 

152 
val rule_del: attribute 

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

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

18708  158 
val setup: theory > theory 
5841  159 
end; 
160 

0  161 

5927  162 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  163 
struct 
164 

7354  165 
local open Data in 
0  166 

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

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

168 

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

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

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

171 
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

172 

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

173 
[ 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

174 

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

175 
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

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

177 

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

178 
[ 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

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

180 

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

181 
local 
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 equal_concl concl prop = 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

184 
concl aconv Logic.strip_assums_concl prop; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

185 

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

186 
fun is_elim rule = 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

188 
val thy = Thm.theory_of_thm rule; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

191 
Term.is_Var (ObjectLogic.drop_judgment thy concl) andalso 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

192 
exists (equal_concl concl) (Thm.prems_of rule) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

194 

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

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

196 

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

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

198 
if is_elim rule then 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

202 
fun redundant_hyp goal = 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

203 
equal_concl concl' goal orelse 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

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

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

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

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

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

212 
> Seq.hd 
18571  213 
> Drule.zero_var_indexes 
18691  214 
> Thm.put_name_tags (Thm.get_name_tags rule); 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

215 
in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

217 

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

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

219 

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

220 

1800  221 
(*** Useful tactics for classical reasoning ***) 
0  222 

1524  223 
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

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

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

10736  229 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  230 
(eq_assume_tac ORELSE' assume_tac); 
0  231 

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

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

233 
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

234 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  235 

236 
(*Like mp_tac but instantiates no variables*) 

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

237 
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

238 

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

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

241 
(rule_by_tactic (etac thin_rl 1) (not_elim RS classical))); 
0  242 

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

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

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

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

248 
trying rules in order. *) 

10736  249 
fun swap_res_tac rls = 
54  250 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
10736  251 
in assume_tac ORELSE' 
252 
contr_tac ORELSE' 

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

253 
biresolve_tac (foldr addrl [] rls) 
0  254 
end; 
255 

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

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

257 
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

258 

6967  259 
fun dup_elim th = 
13525  260 
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

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

262 

1800  263 
(**** Classical rule sets ****) 
0  264 

265 
datatype claset = 

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

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

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

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

9938  271 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  272 
safe0_netpair : netpair, (*nets for trivial cases*) 
273 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

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

0  277 

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

278 
(*Desired invariants are 
9938  279 
safe0_netpair = build safe0_brls, 
280 
safep_netpair = build safep_brls, 

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

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

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

284 

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

286 
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

287 
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

288 
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

289 
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

290 
*) 
0  291 

6502  292 
val empty_netpair = (Net.empty, Net.empty); 
293 

10736  294 
val empty_cs = 
9938  295 
CS{safeIs = [], 
296 
safeEs = [], 

297 
hazIs = [], 

298 
hazEs = [], 

4651  299 
swrappers = [], 
300 
uwrappers = [], 

6502  301 
safe0_netpair = empty_netpair, 
302 
safep_netpair = empty_netpair, 

303 
haz_netpair = empty_netpair, 

6955  304 
dup_netpair = empty_netpair, 
305 
xtra_netpair = empty_netpair}; 

0  306 

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

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

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

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

8727  315 
> Pretty.chunks > Pretty.writeln 
3546  316 
end; 
0  317 

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

319 

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

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

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

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

326 

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

327 

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

329 

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

330 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  331 
***) 
0  332 

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

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

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

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

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

337 

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

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

340 

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

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

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

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

347 

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

10736  350 

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

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

352 

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

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

354 
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

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

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

358 

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

359 
fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls; 
12362  360 
fun delete x = delete_tagged_list (joinrules x); 
12401  361 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  362 

18691  363 
val mem_thm = member Drule.eq_thm_prop 
364 
and rem_thm = remove Drule.eq_thm_prop; 

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

365 

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

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

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

368 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
18691  369 
if mem_thm safeIs th then 
9938  370 
warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) 
18691  371 
else if mem_thm safeEs th then 
9408  372 
warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) 
18691  373 
else if mem_thm hazIs th then 
9760  374 
warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) 
18691  375 
else if mem_thm hazEs th then 
9760  376 
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

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

378 

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

379 

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

381 

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

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

384 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  385 
if mem_thm safeIs th then 
9938  386 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); 
387 
cs) 

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

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

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

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

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

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

395 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  396 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
397 
safeEs = safeEs, 

398 
hazIs = hazIs, 

399 
hazEs = hazEs, 

400 
swrappers = swrappers, 

401 
uwrappers = uwrappers, 

402 
haz_netpair = haz_netpair, 

403 
dup_netpair = dup_netpair, 

18691  404 
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

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

406 

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

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

409 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  410 
if mem_thm safeEs th then 
9938  411 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); 
412 
cs) 

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

413 
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

414 
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

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

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

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

418 
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

419 
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

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

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

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

424 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  425 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
426 
safeIs = safeIs, 

427 
hazIs = hazIs, 

428 
hazEs = hazEs, 

429 
swrappers = swrappers, 

430 
uwrappers = uwrappers, 

431 
haz_netpair = haz_netpair, 

432 
dup_netpair = dup_netpair, 

18691  433 
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

434 
end; 
0  435 

18691  436 
fun cs addSIs ths = fold_rev (addSI NONE) ths cs; 
437 
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

438 

17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

439 
(*Give new theorem a name, if it has one already.*) 
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

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

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

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

443 
else 
17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

444 
case Thm.name_of_thm th of 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

445 
"" => Tactic.make_elim th 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

446 
 a => Thm.name_thm (a ^ "_dest", Tactic.make_elim th); 
17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

447 

fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

448 
fun cs addSDs ths = cs addSEs (map name_make_elim ths); 
0  449 

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

450 

1800  451 
(*** Hazardous (unsafe) rules ***) 
0  452 

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

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

455 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  456 
if mem_thm hazIs th then 
9938  457 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
458 
cs) 

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

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

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

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

462 
in warn_dup th cs; 
9938  463 
CS{hazIs = th::hazIs, 
464 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 

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

10736  466 
safeIs = safeIs, 
9938  467 
safeEs = safeEs, 
468 
hazEs = hazEs, 

469 
swrappers = swrappers, 

470 
uwrappers = uwrappers, 

471 
safe0_netpair = safe0_netpair, 

472 
safep_netpair = safep_netpair, 

18691  473 
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

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

475 
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

476 
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

477 

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

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

480 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  481 
if mem_thm hazEs th then 
9938  482 
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); 
483 
cs) 

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

484 
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

485 
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

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

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

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

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

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

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

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

494 
dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair, 
10736  495 
safeIs = safeIs, 
9938  496 
safeEs = safeEs, 
497 
hazIs = hazIs, 

498 
swrappers = swrappers, 

499 
uwrappers = uwrappers, 

500 
safe0_netpair = safe0_netpair, 

501 
safep_netpair = safep_netpair, 

18691  502 
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

503 
end; 
0  504 

18691  505 
fun cs addIs ths = fold_rev (addI NONE) ths cs; 
506 
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

507 

17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

508 
fun cs addDs ths = cs addEs (map name_make_elim ths); 
0  509 

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

510 

10736  511 
(*** Deletion of rules 
1800  512 
Working out what to delete, requires repeating much of the code used 
9938  513 
to insert. 
1800  514 
***) 
515 

10736  516 
fun delSI 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 safeIs th then 
15570  520 
let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th] 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

521 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  522 
safep_netpair = delete (safep_rls, []) safep_netpair, 
18691  523 
safeIs = rem_thm th safeIs, 
9938  524 
safeEs = safeEs, 
525 
hazIs = hazIs, 

526 
hazEs = hazEs, 

527 
swrappers = swrappers, 

528 
uwrappers = uwrappers, 

529 
haz_netpair = haz_netpair, 

530 
dup_netpair = dup_netpair, 

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

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

533 
else cs; 
1800  534 

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

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

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

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

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

541 
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

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

18691  545 
safeEs = rem_thm th safeEs, 
9938  546 
hazIs = hazIs, 
547 
hazEs = hazEs, 

548 
swrappers = swrappers, 

549 
uwrappers = uwrappers, 

550 
haz_netpair = haz_netpair, 

551 
dup_netpair = dup_netpair, 

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

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

554 
else cs; 
1800  555 

556 

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

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

558 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  559 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  560 
if mem_thm hazIs th then 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

561 
CS{haz_netpair = delete ([th], []) haz_netpair, 
9938  562 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
10736  563 
safeIs = safeIs, 
9938  564 
safeEs = safeEs, 
18691  565 
hazIs = rem_thm th hazIs, 
9938  566 
hazEs = hazEs, 
567 
swrappers = swrappers, 

568 
uwrappers = uwrappers, 

569 
safe0_netpair = safe0_netpair, 

570 
safep_netpair = safep_netpair, 

12401  571 
xtra_netpair = delete' ([th], []) xtra_netpair} 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

573 
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

574 
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

575 

1800  576 

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

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

578 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
9938  579 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

580 
let val th' = classical_rule th in 
18691  581 
if mem_thm hazEs th then 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

583 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
10736  584 
safeIs = safeIs, 
9938  585 
safeEs = safeEs, 
586 
hazIs = hazIs, 

18691  587 
hazEs = rem_thm th hazEs, 
9938  588 
swrappers = swrappers, 
589 
uwrappers = uwrappers, 

590 
safe0_netpair = safe0_netpair, 

591 
safep_netpair = safep_netpair, 

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

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

594 
end; 
6955  595 

1800  596 

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

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

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

599 
let val th' = Tactic.make_elim th in 
18691  600 
if mem_thm safeIs th orelse mem_thm safeEs th orelse 
601 
mem_thm hazIs th orelse mem_thm hazEs th orelse 

602 
mem_thm safeEs th' orelse mem_thm hazEs th' 

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

603 
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

604 
else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs) 
9938  605 
end; 
1800  606 

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

607 
fun cs delrules ths = fold delrule ths cs; 
1800  608 

609 

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

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

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

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

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

616 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  617 
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

618 

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

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

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

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

624 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  625 
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

626 

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

627 

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

629 
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => 
9721  630 
overwrite_warn (swrappers, new_swrapper) 
631 
("Overwriting safe wrapper " ^ fst new_swrapper)); 

4651  632 

633 
(*Add/replace an unsafe wrapper*) 

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

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

637 

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

639 
fun cs delSWrapper name = update_swrappers cs (fn swrappers => 
17795  640 
let val swrappers' = filter_out (equal name o fst) swrappers in 
15036  641 
if length swrappers <> length swrappers' then swrappers' 
642 
else (warning ("No such safe wrapper in claset: "^ name); swrappers) 

643 
end); 

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

644 

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

646 
fun cs delWrapper name = update_uwrappers cs (fn uwrappers => 
17795  647 
let val uwrappers' = filter_out (equal name o fst) uwrappers in 
15036  648 
if length uwrappers <> length uwrappers' then uwrappers' 
649 
else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers) 

650 
end); 

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

651 

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

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

657 

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

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

663 

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

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

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

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

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

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

671 
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

672 

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

675 
treatment of priority might get muddled up.*) 

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

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

677 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) = 
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

678 
let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs) 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

679 
val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs) 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

680 
val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs) 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

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

682 
val cs1 = cs addSIs safeIs' 
9938  683 
addSEs safeEs' 
684 
addIs hazIs' 

685 
addEs hazEs' 

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

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

687 
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); 
10736  688 
in cs3 
1711  689 
end; 
690 

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

691 

1800  692 
(**** Simple tactics for theorem proving ****) 
0  693 

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

10736  695 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  696 
appSWrappers cs (FIRST' [ 
9938  697 
eq_assume_tac, 
698 
eq_mp_tac, 

699 
bimatch_from_nets_tac safe0_netpair, 

700 
FIRST' hyp_subst_tacs, 

701 
bimatch_from_nets_tac safep_netpair]); 

0  702 

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

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

709 

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

710 

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

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

712 

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

713 
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

714 

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

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

716 
create precisely n subgoals.*) 
10736  717 
fun n_bimatch_from_nets_tac n = 
15570  718 
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

719 

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

720 
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

721 
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

722 

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

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

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

725 
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

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

727 

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

728 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  729 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  730 
appSWrappers cs (FIRST' [ 
9938  731 
eq_assume_contr_tac, 
732 
bimatch_from_nets_tac safe0_netpair, 

733 
FIRST' hyp_subst_tacs, 

734 
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

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

736 

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

737 
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

738 

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

739 

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

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

741 

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

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

744 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  745 
assume_tac APPEND' 
746 
contr_tac APPEND' 

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

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

748 

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

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

751 
biresolve_from_nets_tac safep_netpair; 
0  752 

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

754 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  755 

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

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

758 

0  759 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  760 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  761 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  762 

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

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

10736  765 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  766 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  767 

1800  768 
(**** The following tactics all fail unless they solve one goal ****) 
0  769 

770 
(*Dumb but fast*) 

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

771 
fun fast_tac cs = 
11754  772 
ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  773 

774 
(*Slower but smarter than fast_tac*) 

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

775 
fun best_tac cs = 
11754  776 
ObjectLogic.atomize_tac THEN' 
0  777 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
778 

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

780 
fun first_best_tac cs = 
11754  781 
ObjectLogic.atomize_tac THEN' 
9402  782 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
783 

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

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

786 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  787 

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

788 
fun slow_best_tac cs = 
11754  789 
ObjectLogic.atomize_tac THEN' 
0  790 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
791 

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

792 

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

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

795 

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

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

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

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

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

801 

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

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

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

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

807 

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

809 
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

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

812 

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

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

814 
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

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

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

818 

5523  819 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  820 
local 
10736  821 
fun slow_step_tac' cs = appWrappers cs 
9938  822 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  823 
in fun depth_tac cs m i state = SELECT_GOAL 
824 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  828 
)) i state; 
829 
end; 

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

830 

10736  831 
(*Search, with depth bound m. 
2173  832 
This is the "entry point", which does safe inferences first.*) 
10736  833 
fun safe_depth_tac cs m = 
834 
SUBGOAL 

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

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

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

10736  839 
[] => DETERM 
9938  840 
 _::_ => I 
10736  841 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  842 
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

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

844 

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

845 
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

846 

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

847 

1724  848 

15036  849 
(** context dependent claset components **) 
850 

851 
datatype context_cs = ContextCS of 

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

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

854 

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

856 
let 

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

858 
in 

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

860 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 

861 
end; 

862 

863 
fun make_context_cs (swrappers, uwrappers) = 

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

865 

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

867 

868 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

869 
let 

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

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

872 

873 
val swrappers' = merge_alists swrappers1 swrappers2; 

874 
val uwrappers' = merge_alists uwrappers1 uwrappers2; 

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

876 

877 

878 

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

880 

18691  881 
(* global claset *) 
1724  882 

16424  883 
structure GlobalClaset = TheoryDataFun 
884 
(struct 

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

887 

15036  888 
val empty = (ref empty_cs, empty_context_cs); 
16424  889 
fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; 
890 
val extend = copy; 

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

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

16424  894 
end); 
1724  895 

7354  896 
val print_claset = GlobalClaset.print; 
17880  897 
val get_claset = ! o #1 o GlobalClaset.get; 
898 

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

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

902 

17880  903 
val change_claset_of = change o #1 o GlobalClaset.get; 
904 
fun change_claset f = change_claset_of (Context.the_context ()) f; 

1800  905 

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

906 
fun claset_of thy = 
17880  907 
let val (cs_ref, ctxt_cs) = GlobalClaset.get thy 
908 
in context_cs (Context.init_proof thy) (! cs_ref) (ctxt_cs) end; 

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

910 

17880  911 
fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st; 
912 
fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st; 

1724  913 

17880  914 
fun AddDs args = change_claset (fn cs => cs addDs args); 
915 
fun AddEs args = change_claset (fn cs => cs addEs args); 

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

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

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

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

920 
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

921 

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

922 

15036  923 
(* context dependent components *) 
924 

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

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

927 

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

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

930 

931 

18691  932 
(* local claset *) 
5841  933 

16424  934 
structure LocalClaset = ProofDataFun 
935 
(struct 

5841  936 
val name = "Provers/claset"; 
937 
type T = claset; 

17880  938 
val init = get_claset; 
15036  939 
fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt)); 
16424  940 
end); 
5841  941 

942 
val print_local_claset = LocalClaset.print; 

943 
val get_local_claset = LocalClaset.get; 

944 
val put_local_claset = LocalClaset.put; 

945 

15036  946 
fun local_claset_of ctxt = 
947 
context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt); 

948 

5841  949 

5885  950 
(* attributes *) 
951 

18728  952 
fun attrib f = Thm.declaration_attribute (fn th => 
18691  953 
fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy) 
954 
 Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt)); 

5885  955 

18691  956 
fun safe_dest w = attrib (addSE w o name_make_elim); 
957 
val safe_elim = attrib o addSE; 

958 
val safe_intro = attrib o addSI; 

959 
fun haz_dest w = attrib (addE w o name_make_elim); 

960 
val haz_elim = attrib o addE; 

961 
val haz_intro = attrib o addI; 

962 
val rule_del = attrib delrule o ContextRules.rule_del; 

5885  963 

964 

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

965 
(* tactics referring to the implicit claset *) 
1800  966 

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

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

970 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  971 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
972 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  978 

1800  979 

10736  980 
end; 
5841  981 

982 

983 

5885  984 
(** concrete syntax of attributes **) 
5841  985 

986 
val introN = "intro"; 

987 
val elimN = "elim"; 

988 
val destN = "dest"; 

9938  989 
val ruleN = "rule"; 
5841  990 

991 
val setup_attrs = Attrib.add_attributes 

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

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

1000 
"remove declaration of intro/elim/dest rule")]; 
5841  1001 

1002 

1003 

7230  1004 
(** proof methods **) 
1005 

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

1006 
fun METHOD_CLASET tac ctxt = 
15036  1007 
Method.METHOD (tac ctxt (local_claset_of ctxt)); 
5841  1008 

8098  1009 
fun METHOD_CLASET' tac ctxt = 
15036  1010 
Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); 
7230  1011 

1012 

1013 
local 

1014 

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

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

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

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

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

1023 
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

1024 
end); 
5841  1025 

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

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

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

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

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

1031 
AxClass.default_intro_classes_tac facts; 
10309  1032 

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

1035 
val default = METHOD_CLASET o default_tac; 
7230  1036 
end; 
5841  1037 

1038 

7230  1039 
(* contradiction method *) 
6502  1040 

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

1043 

1044 
(* automatic methods *) 

5841  1045 

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

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

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

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

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

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

5927  1054 

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

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

7559  1061 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1062 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1063 

1064 

1065 

1066 
(** setup_methods **) 

1067 

1068 
val setup_methods = Method.add_methods 

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

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

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

1079 

1080 

1081 
(** theory setup **) 

1082 

18708  1083 
val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods; 
5841  1084 

1085 

8667  1086 

1087 
(** outer syntax **) 

1088 

1089 
val print_clasetP = 

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

17057  1091 
OuterKeyword.diag 
9513  1092 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1093 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1094 

1095 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1096 

1097 

5841  1098 
end; 