author  wenzelm 
Sat, 15 Jan 2011 20:51:22 +0100  
changeset 41581  72a02e3dec7e 
parent 36960  01594f816e3a 
child 42361  23f352990944 
permissions  rwrr 
9938  1 
(* Title: Provers/classical.ML 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

0  3 

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

5 
theory, etc. 

6 

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

7 
Rules must be classified as intro, elim, safe, hazardous (unsafe). 
0  8 

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

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

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

12 
the conclusion. 

13 
*) 

14 

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

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

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

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

20 

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

21 

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

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

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

25 

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

27 
sig 
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

28 
val imp_elim : thm (* P > Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) 
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

29 
val not_elim : thm (* ~P ==> P ==> R *) 
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

30 
val swap : thm (* ~ P ==> (~ R ==> P) ==> R *) 
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

31 
val classical : thm (* (~ P ==> P) ==> P *) 
9938  32 
val sizef : thm > int (* size function for BEST_FIRST *) 
0  33 
val hyp_subst_tacs: (int > tactic) list 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

34 
end; 
0  35 

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

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

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

40 
val print_cs: claset > unit 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

12401  47 
haz_netpair: netpair, dup_netpair: netpair, 
33369  48 
xtra_netpair: Context_Rules.netpair} 
9938  49 
val merge_cs : claset * claset > claset 
50 
val addDs : claset * thm list > claset 

51 
val addEs : claset * thm list > claset 

52 
val addIs : claset * thm list > claset 

53 
val addSDs : claset * thm list > claset 

54 
val addSEs : claset * thm list > claset 

55 
val addSIs : claset * thm list > claset 

56 
val delrules : claset * thm list > claset 

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

58 
val delSWrapper : claset * string > claset 

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

60 
val delWrapper : claset * string > claset 

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

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

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

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

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

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

9938  69 
val appSWrappers : claset > wrapper 
70 
val appWrappers : claset > wrapper 

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

71 

32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

72 
val global_claset_of : theory > claset 
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

73 
val claset_of : Proof.context > claset 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

74 

9938  75 
val fast_tac : claset > int > tactic 
76 
val slow_tac : claset > int > tactic 

32740  77 
val weight_ASTAR : int Unsynchronized.ref 
9938  78 
val astar_tac : claset > int > tactic 
79 
val slow_astar_tac : claset > int > tactic 

80 
val best_tac : claset > int > tactic 

81 
val first_best_tac : claset > int > tactic 

82 
val slow_best_tac : claset > int > tactic 

83 
val depth_tac : claset > int > int > tactic 

84 
val deepen_tac : claset > int > int > tactic 

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

85 

9938  86 
val contr_tac : int > tactic 
87 
val dup_elim : thm > thm 

88 
val dup_intr : thm > thm 

89 
val dup_step_tac : claset > int > tactic 

90 
val eq_mp_tac : int > tactic 

91 
val haz_step_tac : claset > int > tactic 

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

93 
val mp_tac : int > tactic 

94 
val safe_tac : claset > tactic 

95 
val safe_steps_tac : claset > int > tactic 

96 
val safe_step_tac : claset > int > tactic 

97 
val clarify_tac : claset > int > tactic 

98 
val clarify_step_tac : claset > int > tactic 

99 
val step_tac : claset > int > tactic 

100 
val slow_step_tac : claset > int > tactic 

101 
val swapify : thm list > thm list 

102 
val swap_res_tac : thm list > int > tactic 

103 
val inst_step_tac : claset > int > tactic 

104 
val inst0_step_tac : claset > int > tactic 

105 
val instp_step_tac : claset > int > tactic 

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

106 
end; 
1724  107 

5841  108 
signature CLASSICAL = 
109 
sig 

110 
include BASIC_CLASSICAL 

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

111 
val classical_rule: thm > thm 
15036  112 
val add_context_safe_wrapper: string * (Proof.context > wrapper) > theory > theory 
113 
val del_context_safe_wrapper: string > theory > theory 

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

115 
val del_context_unsafe_wrapper: string > theory > theory 

32261  116 
val get_claset: Proof.context > claset 
117 
val put_claset: claset > Proof.context > Proof.context 

24021  118 
val get_cs: Context.generic > claset 
119 
val map_cs: (claset > claset) > Context.generic > Context.generic 

18728  120 
val safe_dest: int option > attribute 
121 
val safe_elim: int option > attribute 

122 
val safe_intro: int option > attribute 

123 
val haz_dest: int option > attribute 

124 
val haz_elim: int option > attribute 

125 
val haz_intro: int option > attribute 

126 
val rule_del: attribute 

30513  127 
val cla_modifiers: Method.modifier parser list 
35613  128 
val cla_meth: (claset > tactic) > Proof.context > Proof.method 
129 
val cla_meth': (claset > int > tactic) > Proof.context > Proof.method 

30541  130 
val cla_method: (claset > tactic) > (Proof.context > Proof.method) context_parser 
131 
val cla_method': (claset > int > tactic) > (Proof.context > Proof.method) context_parser 

18708  132 
val setup: theory > theory 
5841  133 
end; 
134 

0  135 

5927  136 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  137 
struct 
138 

7354  139 
local open Data in 
0  140 

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

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

142 

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

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

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

145 
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

146 

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

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

148 

26938  149 
Such rules can cause fast_tac to fail and blast_tac to report "PROOF 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

151 

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

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

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

154 

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

155 
fun classical_rule rule = 
41581
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
36960
diff
changeset

156 
if is_some (Object_Logic.elim_concl rule) then 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

174 

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

175 
(*flatten nested meta connectives in prems*) 
35625  176 
val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems); 
18534
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 

1800  179 
(*** Useful tactics for classical reasoning ***) 
0  180 

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

10736  184 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  185 
(eq_assume_tac ORELSE' assume_tac); 
0  186 

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

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

188 
Could do the same thing for P<>Q and P... *) 
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

189 
fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i THEN assume_tac i; 
0  190 

191 
(*Like mp_tac but instantiates no variables*) 

26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

192 
fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i THEN eq_assume_tac i; 
0  193 

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

26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

195 
fun swapify intrs = intrs RLN (2, [Data.swap]); 
30528  196 
val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap)); 
0  197 

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

199 
trying rules in order. *) 

10736  200 
fun swap_res_tac rls = 
33339  201 
let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls 
10736  202 
in assume_tac ORELSE' 
203 
contr_tac ORELSE' 

33339  204 
biresolve_tac (fold_rev addrl rls []) 
0  205 
end; 
206 

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

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

208 
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

209 

6967  210 
fun dup_elim th = 
36546  211 
let 
212 
val rl = (th RSN (2, revcut_rl)) > Thm.assumption 2 > Seq.hd; 

36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36546
diff
changeset

213 
val ctxt = ProofContext.init_global (Thm.theory_of_thm rl); 
36546  214 
in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; 
215 

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

216 

1800  217 
(**** Classical rule sets ****) 
0  218 

219 
datatype claset = 

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

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

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

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

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

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

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

33369  230 
xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*) 
0  231 

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

232 
(*Desired invariants are 
9938  233 
safe0_netpair = build safe0_brls, 
234 
safep_netpair = build safep_brls, 

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

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

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

238 

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

240 
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

241 
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

242 
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

243 
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

244 
*) 
0  245 

6502  246 
val empty_netpair = (Net.empty, Net.empty); 
247 

10736  248 
val empty_cs = 
9938  249 
CS{safeIs = [], 
250 
safeEs = [], 

251 
hazIs = [], 

252 
hazEs = [], 

4651  253 
swrappers = [], 
254 
uwrappers = [], 

6502  255 
safe0_netpair = empty_netpair, 
256 
safep_netpair = empty_netpair, 

257 
haz_netpair = empty_netpair, 

6955  258 
dup_netpair = empty_netpair, 
259 
xtra_netpair = empty_netpair}; 

0  260 

15036  261 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

262 
let val pretty_thms = map Display.pretty_thm_without_context in 
9760  263 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 
264 
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), 

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

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

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

8727  269 
> Pretty.chunks > Pretty.writeln 
3546  270 
end; 
0  271 

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

273 

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

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

276 

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

277 

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

279 

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

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

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

283 
(*For use with biresolve_tac. Combines intro rules with swap to handle negated 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

287 

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

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

290 

10736  291 
(*Priority: prefer rules with fewest subgoals, 
1231  292 
then rules added most recently (preferring the head of the list).*) 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

297 

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

10736  300 

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

302 

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

303 
(*Insert into netpair that already has nI intr rules and nE elim rules. 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

304 
Count the intr rules double (to account for swapify). Negate to give the 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

308 

23178  309 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  310 
fun delete x = delete_tagged_list (joinrules x); 
12401  311 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  312 

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

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

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

315 

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

316 
(*Warn if the rule is already present ELSEWHERE in the claset. The addition 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

318 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

319 
if mem_thm safeIs th then 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

320 
warning ("Rule already declared as safe introduction (intro!)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

321 
Display.string_of_thm_without_context th) 
18691  322 
else if mem_thm safeEs th then 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

323 
warning ("Rule already declared as safe elimination (elim!)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

324 
Display.string_of_thm_without_context th) 
18691  325 
else if mem_thm hazIs th then 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

326 
warning ("Rule already declared as introduction (intro)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

327 
Display.string_of_thm_without_context th) 
18691  328 
else if mem_thm hazEs th then 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

329 
warning ("Rule already declared as elimination (elim)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

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

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

332 

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

333 

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

335 

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

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

338 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  339 
if mem_thm safeIs th then 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

340 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

341 
Display.string_of_thm_without_context th); cs) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

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

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

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

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

350 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  351 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
352 
safeEs = safeEs, 

353 
hazIs = hazIs, 

354 
hazEs = hazEs, 

355 
swrappers = swrappers, 

356 
uwrappers = uwrappers, 

357 
haz_netpair = haz_netpair, 

358 
dup_netpair = dup_netpair, 

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

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

361 

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

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

364 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  365 
if mem_thm safeEs th then 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

366 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

367 
Display.string_of_thm_without_context th); cs) 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

368 
else if has_fewer_prems 1 th then 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

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

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

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

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

373 
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

374 
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

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

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

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

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

382 
hazIs = hazIs, 

383 
hazEs = hazEs, 

384 
swrappers = swrappers, 

385 
uwrappers = uwrappers, 

386 
haz_netpair = haz_netpair, 

387 
dup_netpair = dup_netpair, 

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

389 
end; 
0  390 

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

393 

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

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

395 
if has_fewer_prems 1 th then 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

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

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

398 

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

399 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
0  400 

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

401 

1800  402 
(*** Hazardous (unsafe) rules ***) 
0  403 

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

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

406 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  407 
if mem_thm hazIs th then 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

408 
(warning ("Ignoring duplicate introduction (intro)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

409 
Display.string_of_thm_without_context th); cs) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

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

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

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

417 
dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair, 
10736  418 
safeIs = safeIs, 
9938  419 
safeEs = safeEs, 
420 
hazEs = hazEs, 

421 
swrappers = swrappers, 

422 
uwrappers = uwrappers, 

423 
safe0_netpair = safe0_netpair, 

424 
safep_netpair = safep_netpair, 

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

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

427 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

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

429 

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

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

432 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  433 
if mem_thm hazEs th then 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

434 
(warning ("Ignoring duplicate elimination (elim)\n" ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

435 
Display.string_of_thm_without_context th); cs) 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

436 
else if has_fewer_prems 1 th then 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

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

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

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

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

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

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

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

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

446 
dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair, 
10736  447 
safeIs = safeIs, 
9938  448 
safeEs = safeEs, 
449 
hazIs = hazIs, 

450 
swrappers = swrappers, 

451 
uwrappers = uwrappers, 

452 
safe0_netpair = safe0_netpair, 

453 
safep_netpair = safep_netpair, 

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

455 
end; 
0  456 

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

459 

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

460 
fun cs addDs ths = cs addEs (map make_elim ths); 
0  461 

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

462 

10736  463 
(*** Deletion of rules 
1800  464 
Working out what to delete, requires repeating much of the code used 
9938  465 
to insert. 
1800  466 
***) 
467 

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

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

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

473 
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

474 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  475 
safep_netpair = delete (safep_rls, []) safep_netpair, 
18691  476 
safeIs = rem_thm th safeIs, 
9938  477 
safeEs = safeEs, 
478 
hazIs = hazIs, 

479 
hazEs = hazEs, 

480 
swrappers = swrappers, 

481 
uwrappers = uwrappers, 

482 
haz_netpair = haz_netpair, 

483 
dup_netpair = dup_netpair, 

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

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

486 
else cs; 
1800  487 

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

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

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

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

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

494 
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

495 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  496 
safep_netpair = delete ([], safep_rls) safep_netpair, 
497 
safeIs = safeIs, 

18691  498 
safeEs = rem_thm th safeEs, 
9938  499 
hazIs = hazIs, 
500 
hazEs = hazEs, 

501 
swrappers = swrappers, 

502 
uwrappers = uwrappers, 

503 
haz_netpair = haz_netpair, 

504 
dup_netpair = dup_netpair, 

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

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

507 
else cs; 
1800  508 

509 

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

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

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

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

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

516 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
10736  517 
safeIs = safeIs, 
9938  518 
safeEs = safeEs, 
18691  519 
hazIs = rem_thm th hazIs, 
9938  520 
hazEs = hazEs, 
521 
swrappers = swrappers, 

522 
uwrappers = uwrappers, 

523 
safe0_netpair = safe0_netpair, 

524 
safep_netpair = safep_netpair, 

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

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

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

528 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

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

530 

1800  531 

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

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

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

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

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

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

538 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
10736  539 
safeIs = safeIs, 
9938  540 
safeEs = safeEs, 
541 
hazIs = hazIs, 

18691  542 
hazEs = rem_thm th hazEs, 
9938  543 
swrappers = swrappers, 
544 
uwrappers = uwrappers, 

545 
safe0_netpair = safe0_netpair, 

546 
safep_netpair = safep_netpair, 

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

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

549 
else cs; 
1800  550 

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

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

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

553 
let val th' = Tactic.make_elim th in 
18691  554 
if mem_thm safeIs th orelse mem_thm safeEs th orelse 
555 
mem_thm hazIs th orelse mem_thm hazEs th orelse 

556 
mem_thm safeEs th' orelse mem_thm hazEs th' 

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

557 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

558 
else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs) 
9938  559 
end; 
1800  560 

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

561 
fun cs delrules ths = fold delrule ths cs; 
1800  562 

563 

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

564 
(*** Modifying the wrapper tacticals ***) 
22674  565 
fun map_swrappers f 
566 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

570 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  571 
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

572 

22674  573 
fun map_uwrappers f 
574 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

578 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  579 
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

580 

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

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

584 

585 
fun delete_warn msg (key : string) xs = 

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

587 
else (warning msg; xs); 

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

588 

4651  589 
(*Add/replace a safe wrapper*) 
22674  590 
fun cs addSWrapper new_swrapper = map_swrappers 
591 
(update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; 

4651  592 

593 
(*Add/replace an unsafe wrapper*) 

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

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

596 

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

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

600 

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

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

604 

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

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

610 

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

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

616 

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

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

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

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

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

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

624 
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

625 

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

628 
treatment of priority might get muddled up.*) 

22674  629 
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, 
24358  630 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, 
22674  631 
swrappers, uwrappers, ...}) = 
24358  632 
if pointer_eq (cs, cs') then cs 
633 
else 

634 
let 

635 
val safeIs' = fold rem_thm safeIs safeIs2; 

636 
val safeEs' = fold rem_thm safeEs safeEs2; 

637 
val hazIs' = fold rem_thm hazIs hazIs2; 

638 
val hazEs' = fold rem_thm hazEs hazEs2; 

639 
val cs1 = cs addSIs safeIs' 

640 
addSEs safeEs' 

641 
addIs hazIs' 

642 
addEs hazEs'; 

643 
val cs2 = map_swrappers 

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

645 
val cs3 = map_uwrappers 

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

647 
in cs3 end; 

1711  648 

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

649 

1800  650 
(**** Simple tactics for theorem proving ****) 
0  651 

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

10736  653 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  654 
appSWrappers cs (FIRST' [ 
9938  655 
eq_assume_tac, 
656 
eq_mp_tac, 

657 
bimatch_from_nets_tac safe0_netpair, 

658 
FIRST' hyp_subst_tacs, 

659 
bimatch_from_nets_tac safep_netpair]); 

0  660 

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

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

667 

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

668 

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

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

670 

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

671 
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

672 

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

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

674 
create precisely n subgoals.*) 
10736  675 
fun n_bimatch_from_nets_tac n = 
33317  676 
biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

677 

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

678 
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

679 
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

680 

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

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

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

683 
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

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

685 

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

686 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  687 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  688 
appSWrappers cs (FIRST' [ 
9938  689 
eq_assume_contr_tac, 
690 
bimatch_from_nets_tac safe0_netpair, 

691 
FIRST' hyp_subst_tacs, 

692 
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

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

694 

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

695 
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

696 

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

697 

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

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

699 

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

32862  702 
fun inst0_step_tac (CS {safe0_netpair, ...}) = 
703 
assume_tac APPEND' 

704 
contr_tac APPEND' 

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

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

706 

4066  707 
(*These unsafe steps could generate more subgoals.*) 
32862  708 
fun instp_step_tac (CS {safep_netpair, ...}) = 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

709 
biresolve_from_nets_tac safep_netpair; 
0  710 

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

712 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  713 

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

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

716 

0  717 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  718 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  719 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  720 

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

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

10736  723 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  724 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  725 

1800  726 
(**** The following tactics all fail unless they solve one goal ****) 
0  727 

728 
(*Dumb but fast*) 

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

729 
fun fast_tac cs = 
35625  730 
Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  731 

732 
(*Slower but smarter than fast_tac*) 

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

733 
fun best_tac cs = 
35625  734 
Object_Logic.atomize_prems_tac THEN' 
0  735 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
736 

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

738 
fun first_best_tac cs = 
35625  739 
Object_Logic.atomize_prems_tac THEN' 
9402  740 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
741 

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

742 
fun slow_tac cs = 
35625  743 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

744 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  745 

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

746 
fun slow_best_tac cs = 
35625  747 
Object_Logic.atomize_prems_tac THEN' 
0  748 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
749 

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

750 

10736  751 
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
32740  752 
val weight_ASTAR = Unsynchronized.ref 5; 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

753 

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

754 
fun astar_tac cs = 
35625  755 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

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

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

759 

10736  760 
fun slow_astar_tac cs = 
35625  761 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

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

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

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

765 

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

767 
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

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

770 

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

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

772 
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

773 
greater search depth required.*) 
32863  774 
fun dup_step_tac (CS {dup_netpair, ...}) = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

776 

5523  777 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  778 
local 
10736  779 
fun slow_step_tac' cs = appWrappers cs 
9938  780 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  781 
in fun depth_tac cs m i state = SELECT_GOAL 
782 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  786 
)) i state; 
787 
end; 

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

788 

10736  789 
(*Search, with depth bound m. 
2173  790 
This is the "entry point", which does safe inferences first.*) 
10736  791 
fun safe_depth_tac cs m = 
792 
SUBGOAL 

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

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

794 
let val deti = 
9938  795 
(*No Vars in the goal? No need to backtrack between goals.*) 
29267  796 
if exists_subterm (fn Var _ => true  _ => false) prem then DETERM else I 
10736  797 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
9938  798 
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

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

800 

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

801 
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

802 

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

803 

1724  804 

15036  805 
(** context dependent claset components **) 
806 

807 
datatype context_cs = ContextCS of 

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

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

810 

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

812 
let 

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

814 
in 

22674  815 
cs 
816 
> fold_rev (add_wrapper (op addSWrapper)) swrappers 

15036  817 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 
818 
end; 

819 

820 
fun make_context_cs (swrappers, uwrappers) = 

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

822 

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

824 

825 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

24358  826 
if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1 
827 
else 

828 
let 

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

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

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

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

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

15036  834 

835 

836 

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

838 

24021  839 
(* global clasets *) 
1724  840 

33522  841 
structure GlobalClaset = Theory_Data 
22846  842 
( 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

843 
type T = claset * context_cs; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

844 
val empty = (empty_cs, empty_context_cs); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

845 
val extend = I; 
33522  846 
fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) = 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

847 
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2)); 
22846  848 
); 
1724  849 

32261  850 
val get_global_claset = #1 o GlobalClaset.get; 
851 
val map_global_claset = GlobalClaset.map o apfst; 

17880  852 

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

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

856 

32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

857 
fun global_claset_of thy = 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

858 
let val (cs, ctxt_cs) = GlobalClaset.get thy 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36546
diff
changeset

859 
in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end; 
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

860 

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

861 

15036  862 
(* context dependent components *) 
863 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

864 
fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper))); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

865 
fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name))); 
15036  866 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

867 
fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper))); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

868 
fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name))); 
15036  869 

870 

24021  871 
(* local clasets *) 
5841  872 

33519  873 
structure LocalClaset = Proof_Data 
22846  874 
( 
5841  875 
type T = claset; 
32261  876 
val init = get_global_claset; 
22846  877 
); 
5841  878 

32261  879 
val get_claset = LocalClaset.get; 
880 
val put_claset = LocalClaset.put; 

881 

32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

882 
fun claset_of ctxt = 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

883 
context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt); 
22846  884 

5841  885 

24021  886 
(* generic clasets *) 
887 

32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

888 
val get_cs = Context.cases global_claset_of claset_of; 
32261  889 
fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f); 
24021  890 

891 

5885  892 
(* attributes *) 
893 

18728  894 
fun attrib f = Thm.declaration_attribute (fn th => 
32261  895 
Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th))); 
5885  896 

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

897 
fun safe_dest w = attrib (addSE w o make_elim); 
18691  898 
val safe_elim = attrib o addSE; 
899 
val safe_intro = attrib o addSI; 

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

900 
fun haz_dest w = attrib (addE w o make_elim); 
18691  901 
val haz_elim = attrib o addE; 
902 
val haz_intro = attrib o addI; 

33369  903 
val rule_del = attrib delrule o Context_Rules.rule_del; 
5885  904 

905 

10736  906 
end; 
5841  907 

908 

909 

5885  910 
(** concrete syntax of attributes **) 
5841  911 

912 
val introN = "intro"; 

913 
val elimN = "elim"; 

914 
val destN = "dest"; 

915 

30528  916 
val setup_attrs = 
917 
Attrib.setup @{binding swapped} (Scan.succeed swapped) 

918 
"classical swap of introduction rule" #> 

33369  919 
Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query) 
30528  920 
"declaration of Classical destruction rule" #> 
33369  921 
Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query) 
30528  922 
"declaration of Classical elimination rule" #> 
33369  923 
Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query) 
30528  924 
"declaration of Classical introduction rule" #> 
925 
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) 

926 
"remove declaration of intro/elim/dest rule"; 

5841  927 

928 

929 

7230  930 
(** proof methods **) 
931 

932 
local 

933 

30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

934 
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 
5841  935 
let 
33369  936 
val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; 
32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

937 
val CS {xtra_netpair, ...} = claset_of ctxt; 
33369  938 
val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair; 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

942 
Method.trace ctxt rules; 
32952  943 
fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq 
18834  944 
end) 
21687  945 
THEN_ALL_NEW Goal.norm_hhf_tac; 
5841  946 

30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

947 
in 
7281  948 

30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

949 
fun rule_tac ctxt [] facts = some_rule_tac ctxt facts 
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

950 
 rule_tac _ rules facts = Method.rule_tac rules facts; 
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

951 

983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

952 
fun default_tac ctxt rules facts = 
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

953 
HEADGOAL (rule_tac ctxt rules facts) ORELSE 
26470  954 
Class.default_intro_tac ctxt facts; 
10309  955 

7230  956 
end; 
5841  957 

958 

7230  959 
(* contradiction method *) 
6502  960 

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

963 

964 
(* automatic methods *) 

5841  965 

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

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

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

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

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

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

5927  974 

35613  975 
fun cla_meth tac ctxt = METHOD (fn facts => 
976 
ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt)); 

7132  977 

35613  978 
fun cla_meth' tac ctxt = METHOD (fn facts => 
979 
HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt))); 

5841  980 

35613  981 
fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac); 
982 
fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac); 

5841  983 

984 

985 

986 
(** setup_methods **) 

987 

30541  988 
val setup_methods = 
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

989 
Method.setup @{binding default} 
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

990 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules))) 
30541  991 
"apply some intro/elim rule (potentially classical)" #> 
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

992 
Method.setup @{binding rule} 
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

993 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) 
30541  994 
"apply some intro/elim rule (potentially classical)" #> 
995 
Method.setup @{binding contradiction} (Scan.succeed (K contradiction)) 

996 
"proof by contradiction" #> 

997 
Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac)) 

998 
"repeatedly apply safe steps" #> 

999 
Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depthfirst)" #> 

1000 
Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depthfirst)" #> 

1001 
Method.setup @{binding best} (cla_method' best_tac) "classical prover (bestfirst)" #> 

1002 
Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4)) 

1003 
"classical prover (iterative deepening)" #> 

1004 
Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) 

1005 
"classical prover (apply safe rules)"; 

5841  1006 

1007 

1008 

1009 
(** theory setup **) 

1010 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

1011 
val setup = setup_attrs #> setup_methods; 
5841  1012 

1013 

8667  1014 

1015 
(** outer syntax **) 

1016 

24867  1017 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

1018 
Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner" 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

1019 
Keyword.diag 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

1020 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o 
32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

1021 
Toplevel.keep (print_cs o claset_of o Toplevel.context_of))); 
8667  1022 

5841  1023 
end; 