author  wenzelm 
Sat, 31 Dec 2005 21:49:42 +0100  
changeset 18534  6799b38ed872 
parent 18374  598e7fd7438b 
child 18557  60a0f9caa0a2 
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 

146 
val safe_dest_global: theory attribute 

147 
val safe_elim_global: theory attribute 

148 
val safe_intro_global: theory attribute 

6955  149 
val haz_dest_global: theory attribute 
150 
val haz_elim_global: theory attribute 

151 
val haz_intro_global: theory attribute 

9938  152 
val rule_del_global: theory attribute 
6955  153 
val safe_dest_local: Proof.context attribute 
154 
val safe_elim_local: Proof.context attribute 

155 
val safe_intro_local: Proof.context attribute 

5885  156 
val haz_dest_local: Proof.context attribute 
157 
val haz_elim_local: Proof.context attribute 

158 
val haz_intro_local: Proof.context attribute 

9938  159 
val rule_del_local: Proof.context attribute 
7272  160 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  161 
val cla_meth: (claset > tactic) > thm list > Proof.context > Proof.method 
162 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 

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

5841  165 
val setup: (theory > theory) list 
166 
end; 

167 

0  168 

5927  169 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  170 
struct 
171 

7354  172 
local open Data in 
0  173 

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

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

175 

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 
Classical reasoning requires stronger elimination rules. For 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

178 
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

179 

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

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

181 

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

182 
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

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

184 

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

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

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

187 

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

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

189 

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

190 
fun equal_concl concl prop = 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

192 

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

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

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

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

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

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

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

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

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

201 

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

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

203 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

221 
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

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

223 

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

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

225 

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

226 

1800  227 
(*** Useful tactics for classical reasoning ***) 
0  228 

1524  229 
val imp_elim = (*cannot use bind_thm within a structure!*) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

230 
store_thm ("imp_elim", classical_rule (Tactic.make_elim mp)); 
0  231 

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

10736  235 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  236 
(eq_assume_tac ORELSE' assume_tac); 
0  237 

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

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

239 
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

240 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  241 

242 
(*Like mp_tac but instantiates no variables*) 

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

243 
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

244 

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

0  247 

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

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

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

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

253 
trying rules in order. *) 

10736  254 
fun swap_res_tac rls = 
54  255 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
10736  256 
in assume_tac ORELSE' 
257 
contr_tac ORELSE' 

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

258 
biresolve_tac (foldr addrl [] rls) 
0  259 
end; 
260 

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

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

262 
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

263 

6967  264 
fun dup_elim th = 
13525  265 
(case try (fn () => 
266 
rule_by_tactic (TRYALL (etac revcut_rl)) 

17257
0ab67cb765da
introduced binding priority 1 for linear combinators etc.
haftmann
parents:
17084
diff
changeset

267 
((th RSN (2, revcut_rl)) > assumption 2 > Seq.hd)) () of 
15531  268 
SOME th' => th' 
6967  269 
 _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); 
0  270 

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

271 

1800  272 
(**** Classical rule sets ****) 
0  273 

274 
datatype claset = 

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

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

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

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

9938  280 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  281 
safe0_netpair : netpair, (*nets for trivial cases*) 
282 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

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

0  286 

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

287 
(*Desired invariants are 
9938  288 
safe0_netpair = build safe0_brls, 
289 
safep_netpair = build safep_brls, 

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

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

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

293 

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

295 
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

296 
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

297 
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

298 
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

299 
*) 
0  300 

6502  301 
val empty_netpair = (Net.empty, Net.empty); 
302 

10736  303 
val empty_cs = 
9938  304 
CS{safeIs = [], 
305 
safeEs = [], 

306 
hazIs = [], 

307 
hazEs = [], 

4651  308 
swrappers = [], 
309 
uwrappers = [], 

6502  310 
safe0_netpair = empty_netpair, 
311 
safep_netpair = empty_netpair, 

312 
haz_netpair = empty_netpair, 

6955  313 
dup_netpair = empty_netpair, 
314 
xtra_netpair = empty_netpair}; 

0  315 

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

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

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

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

8727  324 
> Pretty.chunks > Pretty.writeln 
3546  325 
end; 
0  326 

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

328 

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

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

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

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

335 

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

336 

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

338 

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

339 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  340 
***) 
0  341 

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

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

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

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

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

346 

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

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

349 

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

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

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

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

356 

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

10736  359 

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

360 
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

361 

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

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

363 
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

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

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

367 

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

368 
fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls; 
12362  369 
fun delete x = delete_tagged_list (joinrules x); 
12401  370 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  371 

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

372 
val mem_thm = gen_mem Drule.eq_thm_prop 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset

373 
and rem_thm = gen_rem 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

374 

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

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

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

377 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
10736  378 
if mem_thm (th, safeIs) then 
9938  379 
warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

380 
else if mem_thm (th, safeEs) then 
9408  381 
warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) 
10736  382 
else if mem_thm (th, hazIs) then 
9760  383 
warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) 
10736  384 
else if mem_thm (th, hazEs) then 
9760  385 
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

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

387 

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

388 

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

390 

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

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

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

393 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
10736  394 
if mem_thm (th, safeIs) then 
9938  395 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); 
396 
cs) 

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

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

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

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

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

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

404 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  405 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
406 
safeEs = safeEs, 

407 
hazIs = hazIs, 

408 
hazEs = hazEs, 

409 
swrappers = swrappers, 

410 
uwrappers = uwrappers, 

411 
haz_netpair = haz_netpair, 

412 
dup_netpair = dup_netpair, 

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

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

415 

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

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

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

418 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
10736  419 
if mem_thm (th, safeEs) then 
9938  420 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); 
421 
cs) 

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

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

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

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

425 
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

426 
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

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

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

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

431 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  432 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
433 
safeIs = safeIs, 

434 
hazIs = hazIs, 

435 
hazEs = hazEs, 

436 
swrappers = swrappers, 

437 
uwrappers = uwrappers, 

438 
haz_netpair = haz_netpair, 

439 
dup_netpair = dup_netpair, 

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

441 
end; 
0  442 

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

443 
fun cs addSIs ths = fold_rev addSI ths cs; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

444 
fun cs addSEs ths = fold_rev addSE ths cs; 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

445 

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

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

447 
fun name_make_elim th = 
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset

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

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

450 
 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

451 

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

452 
fun cs addSDs ths = cs addSEs (map name_make_elim ths); 
0  453 

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

454 

1800  455 
(*** Hazardous (unsafe) rules ***) 
0  456 

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

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

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

459 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
10736  460 
if mem_thm (th, hazIs) then 
9938  461 
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); 
462 
cs) 

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

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

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

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

466 
in warn_dup th cs; 
9938  467 
CS{hazIs = th::hazIs, 
468 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 

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

10736  470 
safeIs = safeIs, 
9938  471 
safeEs = safeEs, 
472 
hazEs = hazEs, 

473 
swrappers = swrappers, 

474 
uwrappers = uwrappers, 

475 
safe0_netpair = safe0_netpair, 

476 
safep_netpair = safep_netpair, 

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

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

479 

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

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

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

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

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, 

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

503 
end; 
0  504 

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

505 
fun cs addIs ths = fold_rev addI ths cs; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

506 
fun cs addEs ths = fold_rev addE 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. 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

514 
Separate functions delSI, etc., are not exported; instead delrules 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

515 
searches in all the lists and chooses the relevant delXX functions. 
1800  516 
***) 
517 

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

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

521 
if mem_thm (th, safeIs) then 
15570  522 
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

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

526 
safeEs = safeEs, 

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

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

535 
else cs; 
1800  536 

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

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

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

540 
if mem_thm (th, safeEs) then 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

543 
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

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

547 
safeEs = rem_thm (safeEs,th), 

548 
hazIs = hazIs, 

549 
hazEs = hazEs, 

550 
swrappers = swrappers, 

551 
uwrappers = uwrappers, 

552 
haz_netpair = haz_netpair, 

553 
dup_netpair = dup_netpair, 

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

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

556 
else cs; 
1800  557 

558 

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

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

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

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

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

568 
hazEs = hazEs, 

569 
swrappers = swrappers, 

570 
uwrappers = uwrappers, 

571 
safe0_netpair = safe0_netpair, 

572 
safep_netpair = safep_netpair, 

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

574 
else cs; 
1800  575 

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

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

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

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

580 
if mem_thm (th, hazEs) then 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

586 
hazEs = rem_thm (hazEs,th), 

587 
swrappers = swrappers, 

588 
uwrappers = uwrappers, 

589 
safe0_netpair = safe0_netpair, 

590 
safep_netpair = safep_netpair, 

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

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

593 
end; 
6955  594 

1800  595 

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

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

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

598 
let val th' = Tactic.make_elim th in 
9938  599 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 
600 
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse 

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

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

602 
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

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

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

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

608 

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

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

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

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

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

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

617 

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

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

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

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

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

625 

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

626 

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

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

4651  631 

632 
(*Add/replace an unsafe wrapper*) 

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

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

636 

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

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

642 
end); 

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

643 

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

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

649 
end); 

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

650 

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

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

656 

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

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

662 

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

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

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

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

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

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

670 
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

671 

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

674 
treatment of priority might get muddled up.*) 

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

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

676 
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

677 
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

678 
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

679 
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

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

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

684 
addEs hazEs' 

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

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

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

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

690 

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

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

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

698 
bimatch_from_nets_tac safe0_netpair, 

699 
FIRST' hyp_subst_tacs, 

700 
bimatch_from_nets_tac safep_netpair]); 

0  701 

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

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

708 

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

709 

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

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

711 

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

712 
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

713 

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

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

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

718 

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

719 
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

720 
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

721 

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

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

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

724 
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

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

726 

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

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

732 
FIRST' hyp_subst_tacs, 

733 
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

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

735 

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

736 
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

737 

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

740 

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

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

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

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

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

747 

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

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

750 
biresolve_from_nets_tac safep_netpair; 
0  751 

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

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

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

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

757 

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

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

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

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

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

769 
(*Dumb but fast*) 

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

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

773 
(*Slower but smarter than fast_tac*) 

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

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

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

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

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

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

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

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

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

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

791 

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

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

794 

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

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

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

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

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

800 

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

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

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

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

806 

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

808 
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

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

811 

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

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

813 
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

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

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

817 

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

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

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

5757  827 
)) i state; 
828 
end; 

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

829 

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

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

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

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

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

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

843 

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

844 
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

845 

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

846 

1724  847 

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

850 
datatype context_cs = ContextCS of 

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

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

853 

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

855 
let 

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

857 
in 

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

859 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 

860 
end; 

861 

862 
fun make_context_cs (swrappers, uwrappers) = 

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

864 

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

866 

867 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

868 
let 

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

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

871 

872 
val swrappers' = merge_alists swrappers1 swrappers2; 

873 
val uwrappers' = merge_alists uwrappers1 uwrappers2; 

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

875 

876 

877 

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

879 

17880  880 
(* global clasets *) 
1724  881 

16424  882 
structure GlobalClaset = TheoryDataFun 
883 
(struct 

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

886 

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

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

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

16424  893 
end); 
1724  894 

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

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

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

901 

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

1800  904 

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

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

5028  908 
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

909 

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

1724  912 

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

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

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

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

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

919 
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

920 

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

921 

15036  922 
(* context dependent components *) 
923 

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

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

926 

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

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

929 

930 

5841  931 
(* proof data kind 'Provers/claset' *) 
932 

16424  933 
structure LocalClaset = ProofDataFun 
934 
(struct 

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

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

941 
val print_local_claset = LocalClaset.print; 

942 
val get_local_claset = LocalClaset.get; 

943 
val put_local_claset = LocalClaset.put; 

944 

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

947 

5841  948 

5885  949 
(* attributes *) 
950 

17880  951 
fun change_global_cs f (thy, th) = (change_claset_of thy (fn cs => f (cs, [th])); (thy, th)); 
952 
fun change_local_cs f (ctxt, th) = (LocalClaset.map (fn cs => f (cs, [th])) ctxt, th); 

5885  953 

954 
val safe_dest_global = change_global_cs (op addSDs); 

955 
val safe_elim_global = change_global_cs (op addSEs); 

956 
val safe_intro_global = change_global_cs (op addSIs); 

6955  957 
val haz_dest_global = change_global_cs (op addDs); 
958 
val haz_elim_global = change_global_cs (op addEs); 

959 
val haz_intro_global = change_global_cs (op addIs); 

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

960 
val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; 
5885  961 

16806  962 
val safe_dest_local = change_local_cs (op addSDs); 
963 
val safe_elim_local = change_local_cs (op addSEs); 

964 
val safe_intro_local = change_local_cs (op addSIs); 

965 
val haz_dest_local = change_local_cs (op addDs); 

966 
val haz_elim_local = change_local_cs (op addEs); 

967 
val haz_intro_local = change_local_cs (op addIs); 

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

968 
val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; 
5885  969 

970 

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

971 
(* tactics referring to the implicit claset *) 
1800  972 

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

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

976 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  977 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
978 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  984 

1800  985 

10736  986 
end; 
5841  987 

988 

989 

5885  990 
(** concrete syntax of attributes **) 
5841  991 

992 
(* add / del rules *) 

993 

994 
val introN = "intro"; 

995 
val elimN = "elim"; 

996 
val destN = "dest"; 

9938  997 
val ruleN = "rule"; 
5841  998 

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

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

1000 
(Scan.lift (Args.query  Scan.option Args.nat >> xtra  Args.bang >> K safe  
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1001 
Scan.succeed haz)); 
5841  1002 

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

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

1005 

1006 
(* setup_attrs *) 

1007 

1008 
val setup_attrs = Attrib.add_attributes 

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

1009 
[("swapped", (swapped, swapped), "classical swap of introduction rule"), 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

1011 
(add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1012 
add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

1015 
(add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1016 
add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

1019 
(add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global, 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1020 
add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

1023 
"remove declaration of intro/elim/dest rule")]; 
5841  1024 

1025 

1026 

7230  1027 
(** proof methods **) 
1028 

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

1029 
fun METHOD_CLASET tac ctxt = 
15036  1030 
Method.METHOD (tac ctxt (local_claset_of ctxt)); 
5841  1031 

8098  1032 
fun METHOD_CLASET' tac ctxt = 
15036  1033 
Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); 
7230  1034 

1035 

1036 
local 

1037 

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

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

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

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

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

1046 
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

1047 
end); 
5841  1048 

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

1049 
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts 
10394  1050 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 
7281  1051 

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

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

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

1054 
AxClass.default_intro_classes_tac facts; 
10309  1055 

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

1058 
val default = METHOD_CLASET o default_tac; 
7230  1059 
end; 
5841  1060 

1061 

7230  1062 
(* contradiction method *) 
6502  1063 

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

1066 

1067 
(* automatic methods *) 

5841  1068 

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

1070 
[Args.$$$ destN  Args.bang_colon >> K ((I, safe_dest_local): Method.modifier), 
10034  1071 
Args.$$$ destN  Args.colon >> K (I, haz_dest_local), 
1072 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim_local), 

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

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

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

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

5927  1077 

7559  1078 
fun cla_meth tac prems ctxt = Method.METHOD (fn facts => 
15036  1079 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); 
7132  1080 

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

7559  1084 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1085 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1086 

1087 

1088 

1089 
(** setup_methods **) 

1090 

1091 
val setup_methods = Method.add_methods 

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

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

1093 
("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"), 
6502  1094 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
10821  1095 
("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"), 
7004  1096 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1097 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1098 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
18015  1099 
("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"), 
10821  1100 
("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")]; 
5841  1101 

1102 

1103 

1104 
(** theory setup **) 

1105 

16806  1106 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1107 

1108 

8667  1109 

1110 
(** outer syntax **) 

1111 

1112 
val print_clasetP = 

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

17057  1114 
OuterKeyword.diag 
9513  1115 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep 
9010  1116 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 
8667  1117 

1118 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1119 

1120 

5841  1121 
end; 