author  wenzelm 
Fri, 13 May 2011 22:55:00 +0200  
changeset 42793  88bee9f6eec7 
parent 42792  85fb70b0c5e8 
child 42798  02c88bdabe75 
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 
42790  28 
val imp_elim: thm (* P > Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) 
29 
val not_elim: thm (* ~P ==> P ==> R *) 

30 
val swap: thm (* ~ P ==> (~ R ==> P) ==> R *) 

31 
val classical: thm (* (~ P ==> P) ==> P *) 

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 
42790  40 
val rep_cs: claset > 
41 
{safeIs: thm list, 

42 
safeEs: thm list, 

43 
hazIs: thm list, 

44 
hazEs: thm list, 

42793  45 
swrappers: (string * (Proof.context > wrapper)) list, 
46 
uwrappers: (string * (Proof.context > wrapper)) list, 

42790  47 
safe0_netpair: netpair, 
48 
safep_netpair: netpair, 

49 
haz_netpair: netpair, 

50 
dup_netpair: netpair, 

51 
xtra_netpair: Context_Rules.netpair} 

42793  52 
val print_claset: Proof.context > unit 
53 
val addDs: Proof.context * thm list > Proof.context 

54 
val addEs: Proof.context * thm list > Proof.context 

55 
val addIs: Proof.context * thm list > Proof.context 

56 
val addSDs: Proof.context * thm list > Proof.context 

57 
val addSEs: Proof.context * thm list > Proof.context 

58 
val addSIs: Proof.context * thm list > Proof.context 

59 
val delrules: Proof.context * thm list > Proof.context 

60 
val addSWrapper: claset * (string * (Proof.context > wrapper)) > claset 

42790  61 
val delSWrapper: claset * string > claset 
42793  62 
val addWrapper: claset * (string * (Proof.context > wrapper)) > claset 
42790  63 
val delWrapper: claset * string > claset 
64 
val addSbefore: claset * (string * (int > tactic)) > claset 

65 
val addSafter: claset * (string * (int > tactic)) > claset 

66 
val addbefore: claset * (string * (int > tactic)) > claset 

67 
val addafter: claset * (string * (int > tactic)) > claset 

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

69 
val addE2: claset * (string * thm) > claset 

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

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

42793  72 
val appSWrappers: Proof.context > wrapper 
73 
val appWrappers: Proof.context > wrapper 

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

74 

42790  75 
val global_claset_of: theory > claset 
76 
val claset_of: Proof.context > claset 

42793  77 
val map_claset: (claset > claset) > Proof.context > Proof.context 
78 
val put_claset: claset > Proof.context > Proof.context 

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

79 

42793  80 
val fast_tac: Proof.context > int > tactic 
81 
val slow_tac: Proof.context > int > tactic 

82 
val astar_tac: Proof.context > int > tactic 

83 
val slow_astar_tac: Proof.context > int > tactic 

84 
val best_tac: Proof.context > int > tactic 

85 
val first_best_tac: Proof.context > int > tactic 

86 
val slow_best_tac: Proof.context > int > tactic 

87 
val depth_tac: Proof.context > int > int > tactic 

88 
val deepen_tac: Proof.context > int > int > tactic 

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

89 

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

92 
val dup_intr: thm > thm 

42793  93 
val dup_step_tac: Proof.context > int > tactic 
42790  94 
val eq_mp_tac: int > tactic 
42793  95 
val haz_step_tac: Proof.context > int > tactic 
42790  96 
val joinrules: thm list * thm list > (bool * thm) list 
97 
val mp_tac: int > tactic 

42793  98 
val safe_tac: Proof.context > tactic 
99 
val safe_steps_tac: Proof.context > int > tactic 

100 
val safe_step_tac: Proof.context > int > tactic 

101 
val clarify_tac: Proof.context > int > tactic 

102 
val clarify_step_tac: Proof.context > int > tactic 

103 
val step_tac: Proof.context > int > tactic 

104 
val slow_step_tac: Proof.context > int > tactic 

42790  105 
val swapify: thm list > thm list 
106 
val swap_res_tac: thm list > int > tactic 

42793  107 
val inst_step_tac: Proof.context > int > tactic 
108 
val inst0_step_tac: Proof.context > int > tactic 

109 
val instp_step_tac: Proof.context > int > tactic 

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

110 
end; 
1724  111 

5841  112 
signature CLASSICAL = 
113 
sig 

114 
include BASIC_CLASSICAL 

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

115 
val classical_rule: thm > thm 
24021  116 
val get_cs: Context.generic > claset 
117 
val map_cs: (claset > claset) > Context.generic > Context.generic 

18728  118 
val safe_dest: int option > attribute 
119 
val safe_elim: int option > attribute 

120 
val safe_intro: int option > attribute 

121 
val haz_dest: int option > attribute 

122 
val haz_elim: int option > attribute 

123 
val haz_intro: int option > attribute 

124 
val rule_del: attribute 

30513  125 
val cla_modifiers: Method.modifier parser list 
42793  126 
val cla_method: 
127 
(Proof.context > tactic) > (Proof.context > Proof.method) context_parser 

128 
val cla_method': 

129 
(Proof.context > int > tactic) > (Proof.context > Proof.method) context_parser 

18708  130 
val setup: theory > theory 
5841  131 
end; 
132 

0  133 

5927  134 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  135 
struct 
136 

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

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

138 

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

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

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

141 
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

142 

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

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

144 

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

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

147 

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

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

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

150 

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

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

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

153 
let 
42792  154 
val rule' = rule RS Data.classical; 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

168 
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

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

170 

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

171 
(*flatten nested meta connectives in prems*) 
35625  172 
val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems); 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

173 

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

174 

1800  175 
(*** Useful tactics for classical reasoning ***) 
0  176 

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

42792  180 
val contr_tac = 
181 
eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac); 

0  182 

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

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

184 
Could do the same thing for P<>Q and P... *) 
42792  185 
fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i; 
0  186 

187 
(*Like mp_tac but instantiates no variables*) 

42792  188 
fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; 
0  189 

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

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

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

195 
trying rules in order. *) 

10736  196 
fun swap_res_tac rls = 
42792  197 
let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in 
198 
assume_tac ORELSE' 

199 
contr_tac ORELSE' 

200 
biresolve_tac (fold_rev addrl rls []) 

201 
end; 

0  202 

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

203 
(*Duplication of hazardous rules, for complete provers*) 
42792  204 
fun dup_intr th = zero_var_indexes (th RS Data.classical); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

205 

42793  206 
fun dup_elim th = (* FIXME proper context!? *) 
36546  207 
let 
208 
val rl = (th RSN (2, revcut_rl)) > Thm.assumption 2 > Seq.hd; 

42361  209 
val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl); 
36546  210 
in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; 
211 

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

212 

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

215 
datatype claset = 

42793  216 
CS of 
217 
{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 * (Proof.context > wrapper)) list, (*for transforming safe_step_tac*) 

222 
uwrappers : (string * (Proof.context > wrapper)) list, (*for transforming step_tac*) 

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 : Context_Rules.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 = 
42793  246 
CS 
247 
{safeIs = [], 

248 
safeEs = [], 

249 
hazIs = [], 

250 
hazEs = [], 

251 
swrappers = [], 

252 
uwrappers = [], 

253 
safe0_netpair = empty_netpair, 

254 
safep_netpair = empty_netpair, 

255 
haz_netpair = empty_netpair, 

256 
dup_netpair = empty_netpair, 

257 
xtra_netpair = empty_netpair}; 

0  258 

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

260 

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

261 

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

263 

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

264 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  265 
***) 
0  266 

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

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

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

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

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

271 

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

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

274 

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

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

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

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

281 

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

10736  284 

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

286 

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

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

288 
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

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

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

292 

23178  293 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  294 
fun delete x = delete_tagged_list (joinrules x); 
12401  295 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  296 

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

297 
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

298 
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

299 

42793  300 
fun string_of_thm NONE = Display.string_of_thm_without_context 
301 
 string_of_thm (SOME context) = 

302 
Display.string_of_thm (Context.cases Syntax.init_pretty_global I context); 

303 

304 
fun make_elim context th = 

305 
if has_fewer_prems 1 th then 

306 
error ("Illformed destruction rule\n" ^ string_of_thm context th) 

307 
else Tactic.make_elim th; 

42790  308 

42793  309 
fun warn context msg rules th = 
310 
mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true); 

311 

312 
fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 

313 
warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse 

314 
warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse 

315 
warn context "Rule already declared as introduction (intro)\n" hazIs th orelse 

316 
warn context "Rule already declared as elimination (elim)\n" hazEs th; 

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

317 

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

318 

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

320 

42793  321 
fun addSI w context th 
42790  322 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
323 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

42793  324 
if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

325 
else 
42790  326 
let 
327 
val th' = flat_rule th; 

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

328 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
42790  329 
List.partition Thm.no_prems [th']; 
330 
val nI = length safeIs + 1; 

331 
val nE = length safeEs; 

42793  332 
val _ = warn_other context th cs; 
42790  333 
in 
334 
CS 

335 
{safeIs = th::safeIs, 

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

336 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  337 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
42790  338 
safeEs = safeEs, 
339 
hazIs = hazIs, 

340 
hazEs = hazEs, 

341 
swrappers = swrappers, 

342 
uwrappers = uwrappers, 

343 
haz_netpair = haz_netpair, 

344 
dup_netpair = dup_netpair, 

18691  345 
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} 
42790  346 
end; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

347 

42793  348 
fun addSE w context th 
42790  349 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
350 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

42793  351 
if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

354 
else 
42790  355 
let 
356 
val th' = classical_rule (flat_rule th); 

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

357 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
42790  358 
List.partition (fn rl => nprems_of rl=1) [th']; 
359 
val nI = length safeIs; 

360 
val nE = length safeEs + 1; 

42793  361 
val _ = warn_other context th cs; 
42790  362 
in 
363 
CS 

364 
{safeEs = th::safeEs, 

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, 
42790  367 
safeIs = safeIs, 
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} 
42790  375 
end; 
0  376 

42793  377 
fun addSD w context th = addSE w context (make_elim context th); 
378 

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

379 

1800  380 
(*** Hazardous (unsafe) rules ***) 
0  381 

42793  382 
fun addI w context th 
42790  383 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
384 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

42793  385 
if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

386 
else 
42790  387 
let 
388 
val th' = flat_rule th; 

389 
val nI = length hazIs + 1; 

390 
val nE = length hazEs; 

42793  391 
val _ = warn_other context th cs; 
42790  392 
in 
393 
CS 

394 
{hazIs = th :: hazIs, 

395 
haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, 

396 
dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, 

397 
safeIs = safeIs, 

398 
safeEs = safeEs, 

399 
hazEs = hazEs, 

400 
swrappers = swrappers, 

401 
uwrappers = uwrappers, 

9938  402 
safe0_netpair = safe0_netpair, 
403 
safep_netpair = safep_netpair, 

42790  404 
xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} 
405 
end 

406 
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) 

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

408 

42793  409 
fun addE w context th 
42790  410 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
411 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

42793  412 
if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

415 
else 
42790  416 
let 
417 
val th' = classical_rule (flat_rule th); 

418 
val nI = length hazIs; 

419 
val nE = length hazEs + 1; 

42793  420 
val _ = warn_other context th cs; 
42790  421 
in 
422 
CS 

423 
{hazEs = th :: hazEs, 

424 
haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, 

425 
dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair, 

426 
safeIs = safeIs, 

427 
safeEs = safeEs, 

428 
hazIs = hazIs, 

429 
swrappers = swrappers, 

430 
uwrappers = uwrappers, 

9938  431 
safe0_netpair = safe0_netpair, 
432 
safep_netpair = safep_netpair, 

42790  433 
xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} 
434 
end; 

0  435 

42793  436 
fun addD w context th = addE w context (make_elim context th); 
437 

0  438 

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

439 

10736  440 
(*** Deletion of rules 
1800  441 
Working out what to delete, requires repeating much of the code used 
9938  442 
to insert. 
1800  443 
***) 
444 

10736  445 
fun delSI th 
42790  446 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
447 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

448 
if mem_thm safeIs th then 

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

449 
let 
42790  450 
val th' = flat_rule th; 
451 
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; 

452 
in 

453 
CS 

454 
{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 

455 
safep_netpair = delete (safep_rls, []) safep_netpair, 

456 
safeIs = rem_thm th safeIs, 

457 
safeEs = safeEs, 

458 
hazIs = hazIs, 

459 
hazEs = hazEs, 

460 
swrappers = swrappers, 

461 
uwrappers = uwrappers, 

462 
haz_netpair = haz_netpair, 

463 
dup_netpair = dup_netpair, 

464 
xtra_netpair = delete' ([th], []) xtra_netpair} 

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

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

466 
else cs; 
1800  467 

42790  468 
fun delSE th 
469 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

471 
if mem_thm safeEs th then 

472 
let 

473 
val th' = classical_rule (flat_rule th); 

474 
val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th']; 

475 
in 

476 
CS 

477 
{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 

478 
safep_netpair = delete ([], safep_rls) safep_netpair, 

479 
safeIs = safeIs, 

480 
safeEs = rem_thm th safeEs, 

481 
hazIs = hazIs, 

482 
hazEs = hazEs, 

483 
swrappers = swrappers, 

484 
uwrappers = uwrappers, 

485 
haz_netpair = haz_netpair, 

486 
dup_netpair = dup_netpair, 

487 
xtra_netpair = delete' ([], [th]) xtra_netpair} 

488 
end 

489 
else cs; 

1800  490 

42793  491 
fun delI context th 
42790  492 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
493 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

494 
if mem_thm hazIs th then 

495 
let val th' = flat_rule th in 

496 
CS 

497 
{haz_netpair = delete ([th'], []) haz_netpair, 

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

498 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
42790  499 
safeIs = safeIs, 
500 
safeEs = safeEs, 

501 
hazIs = rem_thm th hazIs, 

502 
hazEs = hazEs, 

503 
swrappers = swrappers, 

504 
uwrappers = uwrappers, 

9938  505 
safe0_netpair = safe0_netpair, 
506 
safep_netpair = safep_netpair, 

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

508 
end 
42790  509 
else cs 
510 
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) 

42793  511 
error ("Illformed introduction rule\n" ^ string_of_thm context th); 
1800  512 

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

513 
fun delE th 
42790  514 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
515 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

516 
if mem_thm hazEs th then 

517 
let val th' = classical_rule (flat_rule th) in 

518 
CS 

519 
{haz_netpair = delete ([], [th']) haz_netpair, 

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

520 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
42790  521 
safeIs = safeIs, 
522 
safeEs = safeEs, 

523 
hazIs = hazIs, 

524 
hazEs = rem_thm th hazEs, 

525 
swrappers = swrappers, 

526 
uwrappers = uwrappers, 

9938  527 
safe0_netpair = safe0_netpair, 
528 
safep_netpair = safep_netpair, 

12401  529 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
42790  530 
end 
531 
else cs; 

1800  532 

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

533 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
42793  534 
fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
535 
let val th' = Tactic.make_elim th in 

18691  536 
if mem_thm safeIs th orelse mem_thm safeEs th orelse 
537 
mem_thm hazIs th orelse mem_thm hazEs th orelse 

538 
mem_thm safeEs th' orelse mem_thm hazEs th' 

42793  539 
then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs))))) 
540 
else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs) 

9938  541 
end; 
1800  542 

543 

42793  544 

545 
(** claset data **) 

42790  546 

42793  547 
(* wrappers *) 
42790  548 

22674  549 
fun map_swrappers f 
550 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

554 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  555 
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

556 

22674  557 
fun map_uwrappers f 
42793  558 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
22674  559 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
560 
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 

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

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

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

564 

22674  565 

42793  566 
(* merge_cs *) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

567 

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

570 
treatment of priority might get muddled up.*) 

22674  571 
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, 
24358  572 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, 
22674  573 
swrappers, uwrappers, ...}) = 
24358  574 
if pointer_eq (cs, cs') then cs 
575 
else 

576 
let 

577 
val safeIs' = fold rem_thm safeIs safeIs2; 

578 
val safeEs' = fold rem_thm safeEs safeEs2; 

579 
val hazIs' = fold rem_thm hazIs hazIs2; 

580 
val hazEs' = fold rem_thm hazEs hazEs2; 

42793  581 
in 
582 
cs 

583 
> fold_rev (addSI NONE NONE) safeIs' 

584 
> fold_rev (addSE NONE NONE) safeEs' 

585 
> fold_rev (addI NONE NONE) hazIs' 

586 
> fold_rev (addE NONE NONE) hazEs' 

587 
> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) 

588 
> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) 

589 
end; 

590 

591 

592 
(* data *) 

593 

594 
structure Claset = Generic_Data 

595 
( 

596 
type T = claset; 

597 
val empty = empty_cs; 

598 
val extend = I; 

599 
val merge = merge_cs; 

600 
); 

601 

602 
val global_claset_of = Claset.get o Context.Theory; 

603 
val claset_of = Claset.get o Context.Proof; 

604 
val rep_claset_of = rep_cs o claset_of; 

605 

606 
val get_cs = Claset.get; 

607 
val map_cs = Claset.map; 

608 

609 
fun map_claset f = Context.proof_map (map_cs f); 

610 
fun put_claset cs = map_claset (K cs); 

611 

612 
fun print_claset ctxt = 

613 
let 

614 
val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; 

615 
val pretty_thms = map (Display.pretty_thm ctxt); 

616 
in 

617 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 

618 
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), 

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

620 
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), 

621 
Pretty.strs ("safe wrappers:" :: map #1 swrappers), 

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

623 
> Pretty.chunks > Pretty.writeln 

624 
end; 

625 

626 

627 
(* oldstyle declarations *) 

628 

629 
fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt; 

630 

631 
val op addSIs = decl (addSI NONE); 

632 
val op addSEs = decl (addSE NONE); 

633 
val op addSDs = decl (addSD NONE); 

634 
val op addIs = decl (addI NONE); 

635 
val op addEs = decl (addE NONE); 

636 
val op addDs = decl (addD NONE); 

637 
val op delrules = decl delrule; 

638 

639 

640 

641 
(*** Modifying the wrapper tacticals ***) 

642 

643 
fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); 

644 
fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); 

645 

646 
fun update_warn msg (p as (key : string, _)) xs = 

647 
(if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); 

648 

649 
fun delete_warn msg (key : string) xs = 

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

651 
else (warning msg; xs); 

652 

653 
(*Add/replace a safe wrapper*) 

654 
fun cs addSWrapper new_swrapper = 

655 
map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; 

656 

657 
(*Add/replace an unsafe wrapper*) 

658 
fun cs addWrapper new_uwrapper = 

659 
map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; 

660 

661 
(*Remove a safe wrapper*) 

662 
fun cs delSWrapper name = 

663 
map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; 

664 

665 
(*Remove an unsafe wrapper*) 

666 
fun cs delWrapper name = 

667 
map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; 

668 

669 
(* compose a safe tactic alternatively before/after safe_step_tac *) 

670 
fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2); 

671 
fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2); 

672 

673 
(*compose a tactic alternatively before/after the step tactic *) 

674 
fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2); 

675 
fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2); 

676 

677 
fun cs addD2 (name, thm) = cs addafter (name, datac thm 1); 

678 
fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1); 

679 
fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); 

680 
fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); 

681 

1711  682 

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

683 

1800  684 
(**** Simple tactics for theorem proving ****) 
0  685 

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

42793  687 
fun safe_step_tac ctxt = 
688 
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in 

689 
appSWrappers ctxt 

690 
(FIRST' 

691 
[eq_assume_tac, 

9938  692 
eq_mp_tac, 
693 
bimatch_from_nets_tac safe0_netpair, 

42792  694 
FIRST' Data.hyp_subst_tacs, 
42793  695 
bimatch_from_nets_tac safep_netpair]) 
696 
end; 

0  697 

5757  698 
(*Repeatedly attack a subgoal using safe inferences  it's deterministic!*) 
42793  699 
fun safe_steps_tac ctxt = 
700 
REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i)); 

5757  701 

0  702 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
42793  703 
fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt)); 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

704 

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

705 

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

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

707 

42790  708 
fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n); 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

709 

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

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

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

714 

42792  715 
fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

716 
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

717 

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

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

719 
fun bimatch2_tac netpair i = 
42790  720 
n_bimatch_from_nets_tac 2 netpair i THEN 
721 
(eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1)); 

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

722 

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

723 
(*Attack subgoals using safe inferences  matching, not resolution*) 
42793  724 
fun clarify_step_tac ctxt = 
725 
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in 

726 
appSWrappers ctxt 

727 
(FIRST' 

728 
[eq_assume_contr_tac, 

9938  729 
bimatch_from_nets_tac safe0_netpair, 
42792  730 
FIRST' Data.hyp_subst_tacs, 
9938  731 
n_bimatch_from_nets_tac 1 safep_netpair, 
42793  732 
bimatch2_tac safep_netpair]) 
733 
end; 

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

734 

42793  735 
fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1)); 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

736 

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

737 

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

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

739 

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

42793  742 
fun inst0_step_tac ctxt = 
32862  743 
assume_tac APPEND' 
744 
contr_tac APPEND' 

42793  745 
biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt)); 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

746 

4066  747 
(*These unsafe steps could generate more subgoals.*) 
42793  748 
fun instp_step_tac ctxt = 
749 
biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt)); 

0  750 

751 
(*These steps could instantiate variables and are therefore unsafe.*) 

42793  752 
fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; 
0  753 

42793  754 
fun haz_step_tac ctxt = 
755 
biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt)); 

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

756 

0  757 
(*Single step for the prover. FAILS unless it makes progress. *) 
42793  758 
fun step_tac ctxt i = 
759 
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i; 

0  760 

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

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

42793  763 
fun slow_step_tac ctxt i = 
764 
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i; 

0  765 

42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

766 

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

769 
(*Dumb but fast*) 

42793  770 
fun fast_tac ctxt = 
771 
Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); 

0  772 

773 
(*Slower but smarter than fast_tac*) 

42793  774 
fun best_tac ctxt = 
35625  775 
Object_Logic.atomize_prems_tac THEN' 
42793  776 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); 
0  777 

9402  778 
(*even a bit smarter than best_tac*) 
42793  779 
fun first_best_tac ctxt = 
35625  780 
Object_Logic.atomize_prems_tac THEN' 
42793  781 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); 
9402  782 

42793  783 
fun slow_tac ctxt = 
35625  784 
Object_Logic.atomize_prems_tac THEN' 
42793  785 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1)); 
0  786 

42793  787 
fun slow_best_tac ctxt = 
35625  788 
Object_Logic.atomize_prems_tac THEN' 
42793  789 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); 
0  790 

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

791 

10736  792 
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

793 

36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

794 
val weight_ASTAR = 5; 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

795 

42793  796 
fun astar_tac ctxt = 
35625  797 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

798 
SELECT_GOAL 
42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

799 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev) 
42793  800 
(step_tac ctxt 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

801 

42793  802 
fun slow_astar_tac ctxt = 
35625  803 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

804 
SELECT_GOAL 
42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

805 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev) 
42793  806 
(slow_step_tac ctxt 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

807 

42790  808 

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

810 
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

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

813 

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

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

815 
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

816 
greater search depth required.*) 
42793  817 
fun dup_step_tac ctxt = 
818 
biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt)); 

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

819 

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

826 
(DEPTH_SOLVE (depth_tac ctxt m 1), 

827 
inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac 

828 
(slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m  1) 1)))) i state; 

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

830 

10736  831 
(*Search, with depth bound m. 
2173  832 
This is the "entry point", which does safe inferences first.*) 
42793  833 
fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) => 
834 
let 

835 
val deti = (*No Vars in the goal? No need to backtrack between goals.*) 

836 
if exists_subterm (fn Var _ => true  _ => false) prem then DETERM else I; 

42790  837 
in 
42793  838 
SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i 
42790  839 
end); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

840 

42793  841 
fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); 
24021  842 

843 

5885  844 
(* attributes *) 
845 

42793  846 
fun attrib f = 
847 
Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context); 

5885  848 

18691  849 
val safe_elim = attrib o addSE; 
850 
val safe_intro = attrib o addSI; 

42793  851 
val safe_dest = attrib o addSD; 
18691  852 
val haz_elim = attrib o addE; 
853 
val haz_intro = attrib o addI; 

42793  854 
val haz_dest = attrib o addD; 
33369  855 
val rule_del = attrib delrule o Context_Rules.rule_del; 
5885  856 

857 

5841  858 

5885  859 
(** concrete syntax of attributes **) 
5841  860 

861 
val introN = "intro"; 

862 
val elimN = "elim"; 

863 
val destN = "dest"; 

864 

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

867 
"classical swap of introduction rule" #> 

33369  868 
Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query) 
30528  869 
"declaration of Classical destruction rule" #> 
33369  870 
Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query) 
30528  871 
"declaration of Classical elimination rule" #> 
33369  872 
Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query) 
30528  873 
"declaration of Classical introduction rule" #> 
874 
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) 

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

5841  876 

877 

878 

7230  879 
(** proof methods **) 
880 

881 
local 

882 

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

883 
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 
5841  884 
let 
33369  885 
val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; 
42793  886 
val {xtra_netpair, ...} = rep_claset_of ctxt; 
33369  887 
val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair; 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

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

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

891 
Method.trace ctxt rules; 
32952  892 
fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq 
18834  893 
end) 
21687  894 
THEN_ALL_NEW Goal.norm_hhf_tac; 
5841  895 

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

896 
in 
7281  897 

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

898 
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

899 
 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

900 

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

901 
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

902 
HEADGOAL (rule_tac ctxt rules facts) ORELSE 
26470  903 
Class.default_intro_tac ctxt facts; 
10309  904 

7230  905 
end; 
5841  906 

907 

7230  908 
(* contradiction method *) 
6502  909 

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

912 

913 
(* automatic methods *) 

5841  914 

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

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

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

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

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

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

5927  923 

42793  924 
fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac); 
925 
fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); 

5841  926 

927 

928 

929 
(** setup_methods **) 

930 

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

932 
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

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

935 
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

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

939 
"proof by contradiction" #> 

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

941 
"repeatedly apply safe steps" #> 

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

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

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

42793  945 
Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4)) 
30541  946 
"classical prover (iterative deepening)" #> 
947 
Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) 

948 
"classical prover (apply safe rules)"; 

5841  949 

950 

951 

952 
(** theory setup **) 

953 

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

954 
val setup = setup_attrs #> setup_methods; 
5841  955 

956 

8667  957 

958 
(** outer syntax **) 

959 

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

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

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

963 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o 
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

964 
Toplevel.keep (fn state => 
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

965 
let val ctxt = Toplevel.context_of state 
42793  966 
in print_claset ctxt end))); 
8667  967 

5841  968 
end; 