author  wenzelm 
Fri, 20 Mar 2009 17:12:37 +0100  
changeset 30609  983e8b6e4e69 
parent 30558  2ef9892114fd 
child 31945  d5f186aa0bed 
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, 
48 
xtra_netpair: ContextRules.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 

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

72 
val claset_of: theory > claset 
15036  73 
val local_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 

77 
val weight_ASTAR : int ref 

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 

17880  116 
val get_claset: theory > claset 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

117 
val map_claset: (claset > claset) > theory > theory 
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 
7559  128 
val cla_meth: (claset > tactic) > thm list > Proof.context > Proof.method 
129 
val cla_meth': (claset > int > tactic) > thm list > 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 = 
19257  156 
if ObjectLogic.is_elim 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*) 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

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

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 = 
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

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' 

30190  204 
biresolve_tac (List.foldr 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 = 
13525  211 
rule_by_tactic (TRYALL (etac revcut_rl)) 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

213 

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

216 
datatype claset = 

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

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

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

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

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

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

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

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

0  228 

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

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

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

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

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

235 

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

237 
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

238 
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

239 
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

240 
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

241 
*) 
0  242 

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

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

248 
hazIs = [], 

249 
hazEs = [], 

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

6502  252 
safe0_netpair = empty_netpair, 
253 
safep_netpair = empty_netpair, 

254 
haz_netpair = empty_netpair, 

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

0  257 

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

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

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

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

8727  266 
> Pretty.chunks > Pretty.writeln 
3546  267 
end; 
0  268 

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

270 

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

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

273 

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

274 

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

276 

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

277 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  278 
***) 
0  279 

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

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

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

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

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

284 

12401  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 @ map (pair false) intrs; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

287 

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

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

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

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

294 

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

10736  297 

23178  298 
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

299 

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

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

301 
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

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

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

305 

23178  306 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  307 
fun delete x = delete_tagged_list (joinrules x); 
12401  308 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  309 

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

310 
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

311 
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

312 

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

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

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

315 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
18691  316 
if mem_thm safeIs th then 
26928  317 
warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th) 
18691  318 
else if mem_thm safeEs th then 
26928  319 
warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th) 
18691  320 
else if mem_thm hazIs th then 
26928  321 
warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th) 
18691  322 
else if mem_thm hazEs th then 
26928  323 
warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

325 

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

326 

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

328 

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

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

331 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  332 
if mem_thm safeIs th then 
26928  333 
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th); 
9938  334 
cs) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

337 
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

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

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

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

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

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

346 
hazIs = hazIs, 

347 
hazEs = hazEs, 

348 
swrappers = swrappers, 

349 
uwrappers = uwrappers, 

350 
haz_netpair = haz_netpair, 

351 
dup_netpair = dup_netpair, 

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

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

354 

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

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

357 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  358 
if mem_thm safeEs th then 
26928  359 
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th); 
9938  360 
cs) 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

361 
else if has_fewer_prems 1 th then 
26928  362 
error("Illformed elimination rule\n" ^ Display.string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

366 
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

367 
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

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

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

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

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

375 
hazIs = hazIs, 

376 
hazEs = hazEs, 

377 
swrappers = swrappers, 

378 
uwrappers = uwrappers, 

379 
haz_netpair = haz_netpair, 

380 
dup_netpair = dup_netpair, 

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

382 
end; 
0  383 

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

386 

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

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

388 
if has_fewer_prems 1 th then 
26928  389 
error("Illformed destruction rule\n" ^ Display.string_of_thm th) 
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

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

391 

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

392 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
0  393 

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

394 

1800  395 
(*** Hazardous (unsafe) rules ***) 
0  396 

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

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

399 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  400 
if mem_thm hazIs th then 
26928  401 
(warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th); 
9938  402 
cs) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

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

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

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

410 
dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair, 
10736  411 
safeIs = safeIs, 
9938  412 
safeEs = safeEs, 
413 
hazEs = hazEs, 

414 
swrappers = swrappers, 

415 
uwrappers = uwrappers, 

416 
safe0_netpair = safe0_netpair, 

417 
safep_netpair = safep_netpair, 

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

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

420 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
26928  421 
error ("Illformed introduction rule\n" ^ Display.string_of_thm th); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

422 

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

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

425 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
18691  426 
if mem_thm hazEs th then 
26928  427 
(warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th); 
9938  428 
cs) 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

429 
else if has_fewer_prems 1 th then 
26928  430 
error("Illformed elimination rule\n" ^ Display.string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

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

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

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

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

439 
dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair, 
10736  440 
safeIs = safeIs, 
9938  441 
safeEs = safeEs, 
442 
hazIs = hazIs, 

443 
swrappers = swrappers, 

444 
uwrappers = uwrappers, 

445 
safe0_netpair = safe0_netpair, 

446 
safep_netpair = safep_netpair, 

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

448 
end; 
0  449 

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

452 

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

453 
fun cs addDs ths = cs addEs (map make_elim ths); 
0  454 

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

455 

10736  456 
(*** Deletion of rules 
1800  457 
Working out what to delete, requires repeating much of the code used 
9938  458 
to insert. 
1800  459 
***) 
460 

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

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

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

466 
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

467 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  468 
safep_netpair = delete (safep_rls, []) safep_netpair, 
18691  469 
safeIs = rem_thm th safeIs, 
9938  470 
safeEs = safeEs, 
471 
hazIs = hazIs, 

472 
hazEs = hazEs, 

473 
swrappers = swrappers, 

474 
uwrappers = uwrappers, 

475 
haz_netpair = haz_netpair, 

476 
dup_netpair = dup_netpair, 

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

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

479 
else cs; 
1800  480 

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

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

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

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

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

487 
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

488 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  489 
safep_netpair = delete ([], safep_rls) safep_netpair, 
490 
safeIs = safeIs, 

18691  491 
safeEs = rem_thm th safeEs, 
9938  492 
hazIs = hazIs, 
493 
hazEs = hazEs, 

494 
swrappers = swrappers, 

495 
uwrappers = uwrappers, 

496 
haz_netpair = haz_netpair, 

497 
dup_netpair = dup_netpair, 

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

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

500 
else cs; 
1800  501 

502 

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

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

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

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

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

509 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
10736  510 
safeIs = safeIs, 
9938  511 
safeEs = safeEs, 
18691  512 
hazIs = rem_thm th hazIs, 
9938  513 
hazEs = hazEs, 
514 
swrappers = swrappers, 

515 
uwrappers = uwrappers, 

516 
safe0_netpair = safe0_netpair, 

517 
safep_netpair = safep_netpair, 

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

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

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

521 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
26928  522 
error ("Illformed introduction rule\n" ^ Display.string_of_thm th); 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

523 

1800  524 

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

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

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

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

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

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

531 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
10736  532 
safeIs = safeIs, 
9938  533 
safeEs = safeEs, 
534 
hazIs = hazIs, 

18691  535 
hazEs = rem_thm th hazEs, 
9938  536 
swrappers = swrappers, 
537 
uwrappers = uwrappers, 

538 
safe0_netpair = safe0_netpair, 

539 
safep_netpair = safep_netpair, 

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

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

542 
else cs; 
1800  543 

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

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

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

546 
let val th' = Tactic.make_elim th in 
18691  547 
if mem_thm safeIs th orelse mem_thm safeEs th orelse 
548 
mem_thm hazIs th orelse mem_thm hazEs th orelse 

549 
mem_thm safeEs th' orelse mem_thm hazEs th' 

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

550 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
26928  551 
else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs) 
9938  552 
end; 
1800  553 

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

554 
fun cs delrules ths = fold delrule ths cs; 
1800  555 

556 

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

557 
(*** Modifying the wrapper tacticals ***) 
22674  558 
fun map_swrappers f 
559 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

563 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  564 
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

565 

22674  566 
fun map_uwrappers f 
567 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

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

573 

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

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

577 

578 
fun delete_warn msg (key : string) xs = 

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

580 
else (warning msg; xs); 

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

581 

4651  582 
(*Add/replace a safe wrapper*) 
22674  583 
fun cs addSWrapper new_swrapper = map_swrappers 
584 
(update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; 

4651  585 

586 
(*Add/replace an unsafe wrapper*) 

22674  587 
fun cs addWrapper new_uwrapper = map_uwrappers 
588 
(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

589 

4651  590 
(*Remove a safe wrapper*) 
22674  591 
fun cs delSWrapper name = map_swrappers 
592 
(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

593 

4651  594 
(*Remove an unsafe wrapper*) 
22674  595 
fun cs delWrapper name = map_uwrappers 
596 
(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

597 

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

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

603 

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

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

609 

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

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

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

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

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

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

617 
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

618 

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

621 
treatment of priority might get muddled up.*) 

22674  622 
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, 
24358  623 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, 
22674  624 
swrappers, uwrappers, ...}) = 
24358  625 
if pointer_eq (cs, cs') then cs 
626 
else 

627 
let 

628 
val safeIs' = fold rem_thm safeIs safeIs2; 

629 
val safeEs' = fold rem_thm safeEs safeEs2; 

630 
val hazIs' = fold rem_thm hazIs hazIs2; 

631 
val hazEs' = fold rem_thm hazEs hazEs2; 

632 
val cs1 = cs addSIs safeIs' 

633 
addSEs safeEs' 

634 
addIs hazIs' 

635 
addEs hazEs'; 

636 
val cs2 = map_swrappers 

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

638 
val cs3 = map_uwrappers 

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

640 
in cs3 end; 

1711  641 

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

642 

1800  643 
(**** Simple tactics for theorem proving ****) 
0  644 

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

10736  646 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  647 
appSWrappers cs (FIRST' [ 
9938  648 
eq_assume_tac, 
649 
eq_mp_tac, 

650 
bimatch_from_nets_tac safe0_netpair, 

651 
FIRST' hyp_subst_tacs, 

652 
bimatch_from_nets_tac safep_netpair]); 

0  653 

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

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

660 

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

661 

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

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

663 

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

664 
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

665 

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

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

667 
create precisely n subgoals.*) 
10736  668 
fun n_bimatch_from_nets_tac n = 
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30541
diff
changeset

669 
biresolution_from_nets_tac (order_list 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

670 

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

671 
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

672 
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

673 

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

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

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

676 
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

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

678 

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

679 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  680 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  681 
appSWrappers cs (FIRST' [ 
9938  682 
eq_assume_contr_tac, 
683 
bimatch_from_nets_tac safe0_netpair, 

684 
FIRST' hyp_subst_tacs, 

685 
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

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

687 

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

688 
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

689 

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

690 

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

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

692 

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

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

695 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  696 
assume_tac APPEND' 
697 
contr_tac APPEND' 

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

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

699 

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

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

702 
biresolve_from_nets_tac safep_netpair; 
0  703 

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

705 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  706 

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

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

709 

0  710 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  711 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  712 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  713 

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

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

10736  716 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  717 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  718 

1800  719 
(**** The following tactics all fail unless they solve one goal ****) 
0  720 

721 
(*Dumb but fast*) 

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

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

723 
ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  724 

725 
(*Slower but smarter than fast_tac*) 

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

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

727 
ObjectLogic.atomize_prems_tac THEN' 
0  728 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
729 

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

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

732 
ObjectLogic.atomize_prems_tac THEN' 
9402  733 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
734 

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

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

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

737 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  738 

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

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

740 
ObjectLogic.atomize_prems_tac THEN' 
0  741 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
742 

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

743 

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

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

746 

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

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

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

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

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

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

752 

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

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

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

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

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

758 

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

760 
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

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

763 

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

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

765 
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

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

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

769 

5523  770 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  771 
local 
10736  772 
fun slow_step_tac' cs = appWrappers cs 
9938  773 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  774 
in fun depth_tac cs m i state = SELECT_GOAL 
775 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  779 
)) i state; 
780 
end; 

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

781 

10736  782 
(*Search, with depth bound m. 
2173  783 
This is the "entry point", which does safe inferences first.*) 
10736  784 
fun safe_depth_tac cs m = 
785 
SUBGOAL 

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

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

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

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

793 

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

794 
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

795 

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

796 

1724  797 

15036  798 
(** context dependent claset components **) 
799 

800 
datatype context_cs = ContextCS of 

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

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

803 

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

805 
let 

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

807 
in 

22674  808 
cs 
809 
> fold_rev (add_wrapper (op addSWrapper)) swrappers 

15036  810 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 
811 
end; 

812 

813 
fun make_context_cs (swrappers, uwrappers) = 

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

815 

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

817 

818 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

24358  819 
if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1 
820 
else 

821 
let 

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

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

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

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

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

15036  827 

828 

829 

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

831 

24021  832 
(* global clasets *) 
1724  833 

16424  834 
structure GlobalClaset = TheoryDataFun 
22846  835 
( 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

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

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

838 
val copy = I; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

839 
val extend = I; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

840 
fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) = 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

841 
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2)); 
22846  842 
); 
1724  843 

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

844 
val get_claset = #1 o GlobalClaset.get; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

845 
val map_claset = GlobalClaset.map o apfst; 
17880  846 

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

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

850 

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

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

852 
let val (cs, ctxt_cs) = GlobalClaset.get thy 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

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

854 

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

855 

15036  856 
(* context dependent components *) 
857 

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

858 
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

859 
fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name))); 
15036  860 

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

861 
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

862 
fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name))); 
15036  863 

864 

24021  865 
(* local clasets *) 
5841  866 

16424  867 
structure LocalClaset = ProofDataFun 
22846  868 
( 
5841  869 
type T = claset; 
17880  870 
val init = get_claset; 
22846  871 
); 
5841  872 

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

874 
context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt); 
22846  875 

5841  876 

24021  877 
(* generic clasets *) 
878 

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

879 
val get_cs = Context.cases claset_of local_claset_of; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

880 
fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f); 
24021  881 

882 

5885  883 
(* attributes *) 
884 

18728  885 
fun attrib f = Thm.declaration_attribute (fn th => 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

886 
Context.mapping (map_claset (f th)) (LocalClaset.map (f th))); 
5885  887 

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

888 
fun safe_dest w = attrib (addSE w o make_elim); 
18691  889 
val safe_elim = attrib o addSE; 
890 
val safe_intro = attrib o addSI; 

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

891 
fun haz_dest w = attrib (addE w o make_elim); 
18691  892 
val haz_elim = attrib o addE; 
893 
val haz_intro = attrib o addI; 

894 
val rule_del = attrib delrule o ContextRules.rule_del; 

5885  895 

896 

10736  897 
end; 
5841  898 

899 

900 

5885  901 
(** concrete syntax of attributes **) 
5841  902 

903 
val introN = "intro"; 

904 
val elimN = "elim"; 

905 
val destN = "dest"; 

9938  906 
val ruleN = "rule"; 
5841  907 

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

910 
"classical swap of introduction rule" #> 

911 
Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query) 

912 
"declaration of Classical destruction rule" #> 

913 
Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query) 

914 
"declaration of Classical elimination rule" #> 

915 
Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query) 

916 
"declaration of Classical introduction rule" #> 

917 
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) 

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

5841  919 

920 

921 

7230  922 
(** proof methods **) 
923 

924 
local 

925 

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

926 
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 
5841  927 
let 
12401  928 
val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt; 
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

929 
val CS {xtra_netpair, ...} = local_claset_of ctxt; 
12401  930 
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

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

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

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

935 
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) 
18834  936 
end) 
21687  937 
THEN_ALL_NEW Goal.norm_hhf_tac; 
5841  938 

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

939 
in 
7281  940 

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

941 
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

942 
 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

943 

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

944 
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

945 
HEADGOAL (rule_tac ctxt rules facts) ORELSE 
26470  946 
Class.default_intro_tac ctxt facts; 
10309  947 

7230  948 
end; 
5841  949 

950 

7230  951 
(* contradiction method *) 
6502  952 

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

955 

956 
(* automatic methods *) 

5841  957 

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

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

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

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

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

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

5927  966 

30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30190
diff
changeset

967 
fun cla_meth tac prems ctxt = METHOD (fn facts => 
15036  968 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); 
7132  969 

30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30190
diff
changeset

970 
fun cla_meth' tac prems ctxt = METHOD (fn facts => 
15036  971 
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt))); 
5841  972 

30541  973 
fun cla_method tac = Args.bang_facts  Method.sections cla_modifiers >> (cla_meth tac); 
974 
fun cla_method' tac = Args.bang_facts  Method.sections cla_modifiers >> (cla_meth' tac); 

5841  975 

976 

977 

978 
(** setup_methods **) 

979 

30541  980 
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

981 
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

982 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules))) 
30541  983 
"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

984 
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

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

988 
"proof by contradiction" #> 

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

990 
"repeatedly apply safe steps" #> 

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

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

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

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

995 
"classical prover (iterative deepening)" #> 

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

997 
"classical prover (apply safe rules)"; 

5841  998 

999 

1000 

1001 
(** theory setup **) 

1002 

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

1003 
val setup = setup_attrs #> setup_methods; 
5841  1004 

1005 

8667  1006 

1007 
(** outer syntax **) 

1008 

24867  1009 
val _ = 
8667  1010 
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" 
17057  1011 
OuterKeyword.diag 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

1012 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

1013 
Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of))); 
8667  1014 

5841  1015 
end; 