author  wenzelm 
Sun, 15 Mar 2009 15:59:44 +0100  
changeset 30528  7173bf123335 
parent 30513  1796b8ea88aa 
child 30541  9f168bdc468a 
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 

17880  72 
val change_claset: (claset > claset) > unit 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

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

75 
val CLASET: (claset > tactic) > tactic 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

76 
val CLASET': (claset > 'a > tactic) > 'a > tactic 
15036  77 
val local_claset_of : Proof.context > claset 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

78 

9938  79 
val fast_tac : claset > int > tactic 
80 
val slow_tac : claset > int > tactic 

81 
val weight_ASTAR : int ref 

82 
val astar_tac : claset > int > tactic 

83 
val slow_astar_tac : claset > int > tactic 

84 
val best_tac : claset > int > tactic 

85 
val first_best_tac : claset > int > tactic 

86 
val slow_best_tac : claset > int > tactic 

87 
val depth_tac : claset > int > int > tactic 

88 
val deepen_tac : claset > int > int > tactic 

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

89 

9938  90 
val contr_tac : int > tactic 
91 
val dup_elim : thm > thm 

92 
val dup_intr : thm > thm 

93 
val dup_step_tac : claset > int > tactic 

94 
val eq_mp_tac : int > tactic 

95 
val haz_step_tac : claset > int > tactic 

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

97 
val mp_tac : int > tactic 

98 
val safe_tac : claset > tactic 

99 
val safe_steps_tac : claset > int > tactic 

100 
val safe_step_tac : claset > int > tactic 

101 
val clarify_tac : claset > int > tactic 

102 
val clarify_step_tac : claset > int > tactic 

103 
val step_tac : claset > int > tactic 

104 
val slow_step_tac : claset > int > tactic 

105 
val swapify : thm list > thm list 

106 
val swap_res_tac : thm list > int > tactic 

107 
val inst_step_tac : claset > int > tactic 

108 
val inst0_step_tac : claset > int > tactic 

109 
val instp_step_tac : claset > int > tactic 

1724  110 

9938  111 
val AddDs : thm list > unit 
112 
val AddEs : thm list > unit 

113 
val AddIs : thm list > unit 

114 
val AddSDs : thm list > unit 

115 
val AddSEs : thm list > unit 

116 
val AddSIs : thm list > unit 

117 
val Delrules : thm list > unit 

118 
val Safe_tac : tactic 

119 
val Safe_step_tac : int > tactic 

120 
val Clarify_tac : int > tactic 

121 
val Clarify_step_tac : int > tactic 

122 
val Step_tac : int > tactic 

123 
val Fast_tac : int > tactic 

124 
val Best_tac : int > tactic 

125 
val Slow_tac : int > tactic 

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

128 
end; 
1724  129 

5841  130 
signature CLASSICAL = 
131 
sig 

132 
include BASIC_CLASSICAL 

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

133 
val classical_rule: thm > thm 
15036  134 
val add_context_safe_wrapper: string * (Proof.context > wrapper) > theory > theory 
135 
val del_context_safe_wrapper: string > theory > theory 

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

137 
val del_context_unsafe_wrapper: string > theory > theory 

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

139 
val map_claset: (claset > claset) > theory > theory 
24021  140 
val get_cs: Context.generic > claset 
141 
val map_cs: (claset > claset) > Context.generic > Context.generic 

18728  142 
val safe_dest: int option > attribute 
143 
val safe_elim: int option > attribute 

144 
val safe_intro: int option > attribute 

145 
val haz_dest: int option > attribute 

146 
val haz_elim: int option > attribute 

147 
val haz_intro: int option > attribute 

148 
val rule_del: attribute 

30513  149 
val cla_modifiers: Method.modifier parser list 
7559  150 
val cla_meth: (claset > tactic) > thm list > Proof.context > Proof.method 
151 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 

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

18708  154 
val setup: theory > theory 
5841  155 
end; 
156 

0  157 

5927  158 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  159 
struct 
160 

7354  161 
local open Data in 
0  162 

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

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

164 

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

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

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

167 
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

168 

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

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

170 

26938  171 
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

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

173 

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

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

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

176 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

194 
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

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

196 

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

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

198 
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

199 

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

200 

1800  201 
(*** Useful tactics for classical reasoning ***) 
0  202 

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

10736  206 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  207 
(eq_assume_tac ORELSE' assume_tac); 
0  208 

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

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

210 
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

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

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

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

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

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

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

221 
trying rules in order. *) 

10736  222 
fun swap_res_tac rls = 
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

223 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls 
10736  224 
in assume_tac ORELSE' 
225 
contr_tac ORELSE' 

30190  226 
biresolve_tac (List.foldr addrl [] rls) 
0  227 
end; 
228 

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

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

230 
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

231 

6967  232 
fun dup_elim th = 
13525  233 
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

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

235 

1800  236 
(**** Classical rule sets ****) 
0  237 

238 
datatype claset = 

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

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

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

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

9938  244 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  245 
safe0_netpair : netpair, (*nets for trivial cases*) 
246 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

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

0  250 

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

251 
(*Desired invariants are 
9938  252 
safe0_netpair = build safe0_brls, 
253 
safep_netpair = build safep_brls, 

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

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

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

257 

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

259 
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

260 
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

261 
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

262 
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

263 
*) 
0  264 

6502  265 
val empty_netpair = (Net.empty, Net.empty); 
266 

10736  267 
val empty_cs = 
9938  268 
CS{safeIs = [], 
269 
safeEs = [], 

270 
hazIs = [], 

271 
hazEs = [], 

4651  272 
swrappers = [], 
273 
uwrappers = [], 

6502  274 
safe0_netpair = empty_netpair, 
275 
safep_netpair = empty_netpair, 

276 
haz_netpair = empty_netpair, 

6955  277 
dup_netpair = empty_netpair, 
278 
xtra_netpair = empty_netpair}; 

0  279 

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

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

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

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

8727  288 
> Pretty.chunks > Pretty.writeln 
3546  289 
end; 
0  290 

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

292 

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

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

295 

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

296 

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

298 

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

299 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  300 
***) 
0  301 

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

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

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

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

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

306 

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

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

309 

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

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

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

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

316 

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

10736  319 

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

321 

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

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

323 
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

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

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

327 

23178  328 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  329 
fun delete x = delete_tagged_list (joinrules x); 
12401  330 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  331 

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

332 
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

333 
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

334 

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

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

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

337 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
18691  338 
if mem_thm safeIs th then 
26928  339 
warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th) 
18691  340 
else if mem_thm safeEs th then 
26928  341 
warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th) 
18691  342 
else if mem_thm hazIs th then 
26928  343 
warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th) 
18691  344 
else if mem_thm hazEs th then 
26928  345 
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

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

347 

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

348 

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

350 

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

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

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

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

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

359 
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

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

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

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

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

365 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  366 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
367 
safeEs = safeEs, 

368 
hazIs = hazIs, 

369 
hazEs = hazEs, 

370 
swrappers = swrappers, 

371 
uwrappers = uwrappers, 

372 
haz_netpair = haz_netpair, 

373 
dup_netpair = dup_netpair, 

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

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

376 

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

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

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

383 
else if has_fewer_prems 1 th then 
26928  384 
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

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

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

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

388 
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

389 
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

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

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

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

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

397 
hazIs = hazIs, 

398 
hazEs = hazEs, 

399 
swrappers = swrappers, 

400 
uwrappers = uwrappers, 

401 
haz_netpair = haz_netpair, 

402 
dup_netpair = dup_netpair, 

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

404 
end; 
0  405 

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

408 

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

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

410 
if has_fewer_prems 1 th then 
26928  411 
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

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

413 

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

414 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
0  415 

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

416 

1800  417 
(*** Hazardous (unsafe) rules ***) 
0  418 

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

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

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

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

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

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

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

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

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

432 
dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair, 
10736  433 
safeIs = safeIs, 
9938  434 
safeEs = safeEs, 
435 
hazEs = hazEs, 

436 
swrappers = swrappers, 

437 
uwrappers = uwrappers, 

438 
safe0_netpair = safe0_netpair, 

439 
safep_netpair = safep_netpair, 

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

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

442 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
26928  443 
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

444 

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

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

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

451 
else if has_fewer_prems 1 th then 
26928  452 
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

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

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

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

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

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

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

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

461 
dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair, 
10736  462 
safeIs = safeIs, 
9938  463 
safeEs = safeEs, 
464 
hazIs = hazIs, 

465 
swrappers = swrappers, 

466 
uwrappers = uwrappers, 

467 
safe0_netpair = safe0_netpair, 

468 
safep_netpair = safep_netpair, 

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

470 
end; 
0  471 

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

474 

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

475 
fun cs addDs ths = cs addEs (map make_elim ths); 
0  476 

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

477 

10736  478 
(*** Deletion of rules 
1800  479 
Working out what to delete, requires repeating much of the code used 
9938  480 
to insert. 
1800  481 
***) 
482 

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

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

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

488 
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

489 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
9938  490 
safep_netpair = delete (safep_rls, []) safep_netpair, 
18691  491 
safeIs = rem_thm th safeIs, 
9938  492 
safeEs = safeEs, 
493 
hazIs = hazIs, 

494 
hazEs = hazEs, 

495 
swrappers = swrappers, 

496 
uwrappers = uwrappers, 

497 
haz_netpair = haz_netpair, 

498 
dup_netpair = dup_netpair, 

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

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

501 
else cs; 
1800  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 delSE 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 safeEs th then 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

509 
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

510 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
9938  511 
safep_netpair = delete ([], safep_rls) safep_netpair, 
512 
safeIs = safeIs, 

18691  513 
safeEs = rem_thm th safeEs, 
9938  514 
hazIs = hazIs, 
515 
hazEs = hazEs, 

516 
swrappers = swrappers, 

517 
uwrappers = uwrappers, 

518 
haz_netpair = haz_netpair, 

519 
dup_netpair = dup_netpair, 

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

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

522 
else cs; 
1800  523 

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 delI 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}) = 
18691  528 
if mem_thm hazIs th then 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

529 
let val th' = 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, 
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

531 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
10736  532 
safeIs = safeIs, 
9938  533 
safeEs = safeEs, 
18691  534 
hazIs = rem_thm th hazIs, 
9938  535 
hazEs = hazEs, 
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 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

543 
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) 
26928  544 
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

545 

1800  546 

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

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

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

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

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

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

553 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
10736  554 
safeIs = safeIs, 
9938  555 
safeEs = safeEs, 
556 
hazIs = hazIs, 

18691  557 
hazEs = rem_thm th hazEs, 
9938  558 
swrappers = swrappers, 
559 
uwrappers = uwrappers, 

560 
safe0_netpair = safe0_netpair, 

561 
safep_netpair = safep_netpair, 

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

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

564 
else cs; 
1800  565 

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

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

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

568 
let val th' = Tactic.make_elim th in 
18691  569 
if mem_thm safeIs th orelse mem_thm safeEs th orelse 
570 
mem_thm hazIs th orelse mem_thm hazEs th orelse 

571 
mem_thm safeEs th' orelse mem_thm hazEs th' 

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

572 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
26928  573 
else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs) 
9938  574 
end; 
1800  575 

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

576 
fun cs delrules ths = fold delrule ths cs; 
1800  577 

578 

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

579 
(*** Modifying the wrapper tacticals ***) 
22674  580 
fun map_swrappers f 
581 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

585 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  586 
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

587 

22674  588 
fun map_uwrappers f 
589 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

593 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  594 
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

595 

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

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

599 

600 
fun delete_warn msg (key : string) xs = 

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

602 
else (warning msg; xs); 

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

603 

4651  604 
(*Add/replace a safe wrapper*) 
22674  605 
fun cs addSWrapper new_swrapper = map_swrappers 
606 
(update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; 

4651  607 

608 
(*Add/replace an unsafe wrapper*) 

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

611 

4651  612 
(*Remove a safe wrapper*) 
22674  613 
fun cs delSWrapper name = map_swrappers 
614 
(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

615 

4651  616 
(*Remove an unsafe wrapper*) 
22674  617 
fun cs delWrapper name = map_uwrappers 
618 
(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

619 

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

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

625 

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

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

631 

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

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

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

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

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

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

639 
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

640 

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

643 
treatment of priority might get muddled up.*) 

22674  644 
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, 
24358  645 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, 
22674  646 
swrappers, uwrappers, ...}) = 
24358  647 
if pointer_eq (cs, cs') then cs 
648 
else 

649 
let 

650 
val safeIs' = fold rem_thm safeIs safeIs2; 

651 
val safeEs' = fold rem_thm safeEs safeEs2; 

652 
val hazIs' = fold rem_thm hazIs hazIs2; 

653 
val hazEs' = fold rem_thm hazEs hazEs2; 

654 
val cs1 = cs addSIs safeIs' 

655 
addSEs safeEs' 

656 
addIs hazIs' 

657 
addEs hazEs'; 

658 
val cs2 = map_swrappers 

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

660 
val cs3 = map_uwrappers 

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

662 
in cs3 end; 

1711  663 

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

664 

1800  665 
(**** Simple tactics for theorem proving ****) 
0  666 

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

10736  668 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  669 
appSWrappers cs (FIRST' [ 
9938  670 
eq_assume_tac, 
671 
eq_mp_tac, 

672 
bimatch_from_nets_tac safe0_netpair, 

673 
FIRST' hyp_subst_tacs, 

674 
bimatch_from_nets_tac safep_netpair]); 

0  675 

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

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

682 

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

683 

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

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

685 

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

686 
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

687 

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

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

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

692 

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

693 
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

694 
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

695 

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

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

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

698 
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

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

700 

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

701 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  702 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  703 
appSWrappers cs (FIRST' [ 
9938  704 
eq_assume_contr_tac, 
705 
bimatch_from_nets_tac safe0_netpair, 

706 
FIRST' hyp_subst_tacs, 

707 
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

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

709 

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

710 
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

711 

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

712 

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

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

714 

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

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

717 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
10736  718 
assume_tac APPEND' 
719 
contr_tac APPEND' 

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

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

721 

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

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

724 
biresolve_from_nets_tac safep_netpair; 
0  725 

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

727 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  728 

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

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

731 

0  732 
(*Single step for the prover. FAILS unless it makes progress. *) 
10736  733 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  734 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 
0  735 

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

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

10736  738 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
9938  739 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 
0  740 

1800  741 
(**** The following tactics all fail unless they solve one goal ****) 
0  742 

743 
(*Dumb but fast*) 

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

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

745 
ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  746 

747 
(*Slower but smarter than fast_tac*) 

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

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

749 
ObjectLogic.atomize_prems_tac THEN' 
0  750 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
751 

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

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

754 
ObjectLogic.atomize_prems_tac THEN' 
9402  755 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
756 

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

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

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

759 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  760 

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

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

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

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

765 

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

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

768 

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

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

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

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

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

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

774 

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

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

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

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

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

780 

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

782 
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

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

785 

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

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

787 
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

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

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

791 

5523  792 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  793 
local 
10736  794 
fun slow_step_tac' cs = appWrappers cs 
9938  795 
(instp_step_tac cs APPEND' dup_step_tac cs); 
10736  796 
in fun depth_tac cs m i state = SELECT_GOAL 
797 
(safe_steps_tac cs 1 THEN_ELSE 

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

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

5757  801 
)) i state; 
802 
end; 

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

803 

10736  804 
(*Search, with depth bound m. 
2173  805 
This is the "entry point", which does safe inferences first.*) 
10736  806 
fun safe_depth_tac cs m = 
807 
SUBGOAL 

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

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

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

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

815 

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

816 
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

817 

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

818 

1724  819 

15036  820 
(** context dependent claset components **) 
821 

822 
datatype context_cs = ContextCS of 

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

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

825 

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

827 
let 

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

829 
in 

22674  830 
cs 
831 
> fold_rev (add_wrapper (op addSWrapper)) swrappers 

15036  832 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 
833 
end; 

834 

835 
fun make_context_cs (swrappers, uwrappers) = 

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

837 

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

839 

840 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

24358  841 
if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1 
842 
else 

843 
let 

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

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

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

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

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

15036  849 

850 

851 

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

853 

24021  854 
(* global clasets *) 
1724  855 

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

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

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

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

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

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

863 
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2)); 
22846  864 
); 
1724  865 

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

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

867 
val map_claset = GlobalClaset.map o apfst; 
17880  868 

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

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

872 

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

873 
fun change_claset f = Context.>> (Context.map_theory (map_claset f)); 
1800  874 

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

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

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

877 
in context_cs (ProofContext.init thy) cs (ctxt_cs) end; 
26425
6561665c5cb1
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26412
diff
changeset

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

879 

17880  880 
fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st; 
881 
fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st; 

1724  882 

17880  883 
fun AddDs args = change_claset (fn cs => cs addDs args); 
884 
fun AddEs args = change_claset (fn cs => cs addEs args); 

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

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

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

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

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

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

890 

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

891 

15036  892 
(* context dependent components *) 
893 

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

894 
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

895 
fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name))); 
15036  896 

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

897 
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

898 
fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name))); 
15036  899 

900 

24021  901 
(* local clasets *) 
5841  902 

16424  903 
structure LocalClaset = ProofDataFun 
22846  904 
( 
5841  905 
type T = claset; 
17880  906 
val init = get_claset; 
22846  907 
); 
5841  908 

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

910 
context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt); 
22846  911 

5841  912 

24021  913 
(* generic clasets *) 
914 

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

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

916 
fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f); 
24021  917 

918 

5885  919 
(* attributes *) 
920 

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

922 
Context.mapping (map_claset (f th)) (LocalClaset.map (f th))); 
5885  923 

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

924 
fun safe_dest w = attrib (addSE w o make_elim); 
18691  925 
val safe_elim = attrib o addSE; 
926 
val safe_intro = attrib o addSI; 

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

927 
fun haz_dest w = attrib (addE w o make_elim); 
18691  928 
val haz_elim = attrib o addE; 
929 
val haz_intro = attrib o addI; 

930 
val rule_del = attrib delrule o ContextRules.rule_del; 

5885  931 

932 

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

933 
(* tactics referring to the implicit claset *) 
1800  934 

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

935 
(*the abstraction over the proof state delays the dereferencing*) 
9938  936 
fun Safe_tac st = safe_tac (claset()) st; 
937 
fun Safe_step_tac i st = safe_step_tac (claset()) i st; 

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

938 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9938  939 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
940 
fun Step_tac i st = step_tac (claset()) i st; 

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

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

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

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

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

2066  946 

1800  947 

10736  948 
end; 
5841  949 

950 

951 

5885  952 
(** concrete syntax of attributes **) 
5841  953 

954 
val introN = "intro"; 

955 
val elimN = "elim"; 

956 
val destN = "dest"; 

9938  957 
val ruleN = "rule"; 
5841  958 

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

961 
"classical swap of introduction rule" #> 

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

963 
"declaration of Classical destruction rule" #> 

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

965 
"declaration of Classical elimination rule" #> 

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

967 
"declaration of Classical introduction rule" #> 

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

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

5841  970 

971 

972 

7230  973 
(** proof methods **) 
974 

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

975 
fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt)); 
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30190
diff
changeset

976 
fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); 
7230  977 

978 

979 
local 

980 

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

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

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

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

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

989 
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) 
18834  990 
end) 
21687  991 
THEN_ALL_NEW Goal.norm_hhf_tac; 
5841  992 

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

993 
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts 
10394  994 
 rule_tac rules _ _ facts = Method.rule_tac rules facts; 
7281  995 

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

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

997 
HEADGOAL (rule_tac rules ctxt cs facts) ORELSE 
26470  998 
Class.default_intro_tac ctxt facts; 
10309  999 

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

1002 
val default = METHOD_CLASET o default_tac; 
7230  1003 
end; 
5841  1004 

1005 

7230  1006 
(* contradiction method *) 
6502  1007 

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

1010 

1011 
(* automatic methods *) 

5841  1012 

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

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

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

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

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

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

5927  1021 

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

1022 
fun cla_meth tac prems ctxt = METHOD (fn facts => 
15036  1023 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); 
7132  1024 

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

1025 
fun cla_meth' tac prems ctxt = METHOD (fn facts => 
15036  1026 
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt))); 
5841  1027 

7559  1028 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1029 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1030 

1031 

1032 

1033 
(** setup_methods **) 

1034 

1035 
val setup_methods = Method.add_methods 

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

1036 
[("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"), 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

1037 
("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"), 
6502  1038 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
10821  1039 
("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"), 
7004  1040 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
9806  1041 
("slow", cla_method' slow_tac, "classical prover (slow depthfirst)"), 
9773  1042 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 
18015  1043 
("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"), 
10821  1044 
("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")]; 
5841  1045 

1046 

1047 

1048 
(** theory setup **) 

1049 

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

1050 
val setup = setup_attrs #> setup_methods; 
5841  1051 

1052 

8667  1053 

1054 
(** outer syntax **) 

1055 

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

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

1060 
Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of))); 
8667  1061 

5841  1062 
end; 