author | wenzelm |
Sun, 16 Aug 2015 11:46:08 +0200 | |
changeset 60943 | 7cf1ea00a020 |
parent 60942 | 0af3e522406c |
child 60944 | bb75b61dba5d |
permissions | -rw-r--r-- |
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 |
||
60943 | 7 |
Rules must be classified as intro, elim, safe, 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 |
|
0 | 21 |
signature CLASSICAL_DATA = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
22 |
sig |
42790 | 23 |
val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) |
24 |
val not_elim: thm (* ~P ==> P ==> R *) |
|
25 |
val swap: thm (* ~ P ==> (~ R ==> P) ==> R *) |
|
26 |
val classical: thm (* (~ P ==> P) ==> P *) |
|
50062 | 27 |
val sizef: thm -> int (* size function for BEST_FIRST, typically size_of_thm *) |
51798 | 28 |
val hyp_subst_tacs: (Proof.context -> int -> tactic) list (* optional tactics for |
29 |
substitution in the hypotheses; assumed to be safe! *) |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
30 |
end; |
0 | 31 |
|
5841 | 32 |
signature BASIC_CLASSICAL = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
33 |
sig |
42812 | 34 |
type wrapper = (int -> tactic) -> int -> tactic |
0 | 35 |
type claset |
42793 | 36 |
val print_claset: Proof.context -> unit |
37 |
val addDs: Proof.context * thm list -> Proof.context |
|
38 |
val addEs: Proof.context * thm list -> Proof.context |
|
39 |
val addIs: Proof.context * thm list -> Proof.context |
|
40 |
val addSDs: Proof.context * thm list -> Proof.context |
|
41 |
val addSEs: Proof.context * thm list -> Proof.context |
|
42 |
val addSIs: Proof.context * thm list -> Proof.context |
|
43 |
val delrules: Proof.context * thm list -> Proof.context |
|
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
44 |
val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
45 |
val delSWrapper: Proof.context * string -> Proof.context |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
46 |
val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
47 |
val delWrapper: Proof.context * string -> Proof.context |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
48 |
val addSbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
49 |
val addSafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
50 |
val addbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
51 |
val addafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
52 |
val addD2: Proof.context * (string * thm) -> Proof.context |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
53 |
val addE2: Proof.context * (string * thm) -> Proof.context |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
54 |
val addSD2: Proof.context * (string * thm) -> Proof.context |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
55 |
val addSE2: Proof.context * (string * thm) -> Proof.context |
42793 | 56 |
val appSWrappers: Proof.context -> wrapper |
57 |
val appWrappers: Proof.context -> wrapper |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
58 |
|
42790 | 59 |
val claset_of: Proof.context -> claset |
42793 | 60 |
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
|
61 |
|
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
62 |
val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
63 |
|
42793 | 64 |
val fast_tac: Proof.context -> int -> tactic |
65 |
val slow_tac: Proof.context -> int -> tactic |
|
66 |
val astar_tac: Proof.context -> int -> tactic |
|
67 |
val slow_astar_tac: Proof.context -> int -> tactic |
|
68 |
val best_tac: Proof.context -> int -> tactic |
|
69 |
val first_best_tac: Proof.context -> int -> tactic |
|
70 |
val slow_best_tac: Proof.context -> int -> tactic |
|
71 |
val depth_tac: Proof.context -> int -> int -> tactic |
|
72 |
val deepen_tac: Proof.context -> int -> int -> tactic |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
73 |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
74 |
val contr_tac: Proof.context -> int -> tactic |
59970 | 75 |
val dup_elim: Proof.context -> thm -> thm |
42790 | 76 |
val dup_intr: thm -> thm |
42793 | 77 |
val dup_step_tac: Proof.context -> int -> tactic |
58957 | 78 |
val eq_mp_tac: Proof.context -> int -> tactic |
60943 | 79 |
val unsafe_step_tac: Proof.context -> int -> tactic |
42790 | 80 |
val joinrules: thm list * thm list -> (bool * thm) list |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
81 |
val mp_tac: Proof.context -> int -> tactic |
42793 | 82 |
val safe_tac: Proof.context -> tactic |
83 |
val safe_steps_tac: Proof.context -> int -> tactic |
|
84 |
val safe_step_tac: Proof.context -> int -> tactic |
|
85 |
val clarify_tac: Proof.context -> int -> tactic |
|
86 |
val clarify_step_tac: Proof.context -> int -> tactic |
|
87 |
val step_tac: Proof.context -> int -> tactic |
|
88 |
val slow_step_tac: Proof.context -> int -> tactic |
|
42790 | 89 |
val swapify: thm list -> thm list |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
90 |
val swap_res_tac: Proof.context -> thm list -> int -> tactic |
42793 | 91 |
val inst_step_tac: Proof.context -> int -> tactic |
92 |
val inst0_step_tac: Proof.context -> int -> tactic |
|
93 |
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
|
94 |
end; |
1724 | 95 |
|
5841 | 96 |
signature CLASSICAL = |
97 |
sig |
|
98 |
include BASIC_CLASSICAL |
|
59970 | 99 |
val classical_rule: Proof.context -> thm -> thm |
42812 | 100 |
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net |
101 |
val rep_cs: claset -> |
|
102 |
{safeIs: thm Item_Net.T, |
|
103 |
safeEs: thm Item_Net.T, |
|
60943 | 104 |
unsafeIs: thm Item_Net.T, |
105 |
unsafeEs: thm Item_Net.T, |
|
42812 | 106 |
swrappers: (string * (Proof.context -> wrapper)) list, |
107 |
uwrappers: (string * (Proof.context -> wrapper)) list, |
|
108 |
safe0_netpair: netpair, |
|
109 |
safep_netpair: netpair, |
|
60943 | 110 |
unsafe_netpair: netpair, |
42812 | 111 |
dup_netpair: netpair, |
60942 | 112 |
extra_netpair: Context_Rules.netpair} |
24021 | 113 |
val get_cs: Context.generic -> claset |
114 |
val map_cs: (claset -> claset) -> Context.generic -> Context.generic |
|
18728 | 115 |
val safe_dest: int option -> attribute |
116 |
val safe_elim: int option -> attribute |
|
117 |
val safe_intro: int option -> attribute |
|
60943 | 118 |
val unsafe_dest: int option -> attribute |
119 |
val unsafe_elim: int option -> attribute |
|
120 |
val unsafe_intro: int option -> attribute |
|
18728 | 121 |
val rule_del: attribute |
30513 | 122 |
val cla_modifiers: Method.modifier parser list |
42793 | 123 |
val cla_method: |
124 |
(Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser |
|
125 |
val cla_method': |
|
126 |
(Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser |
|
5841 | 127 |
end; |
128 |
||
0 | 129 |
|
42799 | 130 |
functor Classical(Data: CLASSICAL_DATA): CLASSICAL = |
0 | 131 |
struct |
132 |
||
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
133 |
(** classical elimination rules **) |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
134 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
135 |
(* |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
136 |
Classical reasoning requires stronger elimination rules. For |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
137 |
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
|
138 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
139 |
[| 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
|
140 |
|
26938 | 141 |
Such rules can cause fast_tac to fail and blast_tac to report "PROOF |
59119 | 142 |
FAILED"; classical_rule will strengthen this to |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
143 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
144 |
[| 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
|
145 |
*) |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
146 |
|
59970 | 147 |
fun classical_rule ctxt rule = |
148 |
if is_some (Object_Logic.elim_concl ctxt rule) then |
|
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
149 |
let |
60817 | 150 |
val thy = Proof_Context.theory_of ctxt; |
42792 | 151 |
val rule' = rule RS Data.classical; |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
152 |
val concl' = Thm.concl_of rule'; |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
153 |
fun redundant_hyp goal = |
19257 | 154 |
concl' aconv Logic.strip_assums_concl goal orelse |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
155 |
(case Logic.strip_assums_hyp goal of |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
156 |
hyp :: hyps => exists (fn t => t aconv hyp) hyps |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
157 |
| _ => false); |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
158 |
val rule'' = |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
159 |
rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
160 |
if i = 1 orelse redundant_hyp goal |
60757 | 161 |
then eresolve_tac ctxt [thin_rl] i |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
162 |
else all_tac)) |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
163 |
|> Seq.hd |
21963 | 164 |
|> Drule.zero_var_indexes; |
60817 | 165 |
in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
166 |
else rule; |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
167 |
|
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
168 |
(*flatten nested meta connectives in prems*) |
59970 | 169 |
fun flat_rule ctxt = |
170 |
Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)); |
|
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
171 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
172 |
|
1800 | 173 |
(*** Useful tactics for classical reasoning ***) |
0 | 174 |
|
10736 | 175 |
(*Prove goal that assumes both P and ~P. |
4392 | 176 |
No backtracking if it finds an equal assumption. Perhaps should call |
177 |
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
178 |
fun contr_tac ctxt = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
179 |
eresolve_tac ctxt [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); |
0 | 180 |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
181 |
(*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
|
182 |
Could do the same thing for P<->Q and P... *) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
183 |
fun mp_tac ctxt i = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
184 |
eresolve_tac ctxt [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i; |
0 | 185 |
|
186 |
(*Like mp_tac but instantiates no variables*) |
|
58957 | 187 |
fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; |
0 | 188 |
|
189 |
(*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
|
190 |
fun swapify intrs = intrs RLN (2, [Data.swap]); |
30528 | 191 |
val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap)); |
0 | 192 |
|
193 |
(*Uses introduction rules in the normal way, or on negated assumptions, |
|
194 |
trying rules in order. *) |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
195 |
fun swap_res_tac ctxt rls = |
42792 | 196 |
let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
197 |
assume_tac ctxt ORELSE' |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
198 |
contr_tac ctxt ORELSE' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
199 |
biresolve_tac ctxt (fold_rev addrl rls []) |
42792 | 200 |
end; |
0 | 201 |
|
60943 | 202 |
(*Duplication of unsafe rules, for complete provers*) |
42792 | 203 |
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
|
204 |
|
59970 | 205 |
fun dup_elim ctxt th = |
206 |
let val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd; |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
207 |
in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end; |
36546 | 208 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
209 |
|
1800 | 210 |
(**** Classical rule sets ****) |
0 | 211 |
|
42812 | 212 |
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; |
213 |
type wrapper = (int -> tactic) -> int -> tactic; |
|
214 |
||
0 | 215 |
datatype claset = |
42793 | 216 |
CS of |
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
217 |
{safeIs : thm Item_Net.T, (*safe introduction rules*) |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
218 |
safeEs : thm Item_Net.T, (*safe elimination rules*) |
60943 | 219 |
unsafeIs : thm Item_Net.T, (*unsafe introduction rules*) |
220 |
unsafeEs : thm Item_Net.T, (*unsafe elimination rules*) |
|
42793 | 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*) |
|
60943 | 225 |
unsafe_netpair : netpair, (*nets for unsafe rules*) |
42793 | 226 |
dup_netpair : netpair, (*nets for duplication*) |
60942 | 227 |
extra_netpair : Context_Rules.netpair}; (*nets for extra rules*) |
0 | 228 |
|
6502 | 229 |
val empty_netpair = (Net.empty, Net.empty); |
230 |
||
10736 | 231 |
val empty_cs = |
42793 | 232 |
CS |
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
233 |
{safeIs = Thm.full_rules, |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
234 |
safeEs = Thm.full_rules, |
60943 | 235 |
unsafeIs = Thm.full_rules, |
236 |
unsafeEs = Thm.full_rules, |
|
42793 | 237 |
swrappers = [], |
238 |
uwrappers = [], |
|
239 |
safe0_netpair = empty_netpair, |
|
240 |
safep_netpair = empty_netpair, |
|
60943 | 241 |
unsafe_netpair = empty_netpair, |
42793 | 242 |
dup_netpair = empty_netpair, |
60942 | 243 |
extra_netpair = empty_netpair}; |
0 | 244 |
|
4653 | 245 |
fun rep_cs (CS args) = args; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
246 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
247 |
|
1800 | 248 |
(*** Adding (un)safe introduction or elimination rules. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
249 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
250 |
In case of overlap, new rules are tried BEFORE old ones!! |
1800 | 251 |
***) |
0 | 252 |
|
59970 | 253 |
fun default_context (SOME context) _ = Context.proof_of context |
254 |
| default_context NONE th = Proof_Context.init_global (Thm.theory_of_thm th); |
|
255 |
||
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
256 |
(*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
|
257 |
assumptions. Pairs elim rules with true. *) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
258 |
fun joinrules (intrs, elims) = |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
259 |
(map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs; |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
260 |
|
12401 | 261 |
fun joinrules' (intrs, elims) = |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
262 |
map (pair true) elims @ map (pair false) intrs; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
263 |
|
10736 | 264 |
(*Priority: prefer rules with fewest subgoals, |
1231 | 265 |
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
|
266 |
fun tag_brls k [] = [] |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
267 |
| tag_brls k (brl::brls) = |
10736 | 268 |
(1000000*subgoals_of_brl brl + k, brl) :: |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
269 |
tag_brls (k+1) brls; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
270 |
|
12401 | 271 |
fun tag_brls' _ _ [] = [] |
272 |
| tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; |
|
10736 | 273 |
|
23178 | 274 |
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
|
275 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
276 |
(*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
|
277 |
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
|
278 |
new insertions the lowest priority.*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
279 |
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; |
12401 | 280 |
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
|
281 |
|
23178 | 282 |
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; |
12362 | 283 |
fun delete x = delete_tagged_list (joinrules x); |
12401 | 284 |
fun delete' x = delete_tagged_list (joinrules' x); |
1800 | 285 |
|
60650 | 286 |
fun bad_thm (SOME context) msg th = |
287 |
error (msg ^ "\n" ^ Display.string_of_thm (Context.proof_of context) th) |
|
288 |
| bad_thm NONE msg th = raise THM (msg, 0, [th]); |
|
42793 | 289 |
|
60650 | 290 |
fun make_elim opt_context th = |
291 |
if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed destruction rule" th |
|
42793 | 292 |
else Tactic.make_elim th; |
42790 | 293 |
|
52699 | 294 |
fun warn_thm (SOME (Context.Proof ctxt)) msg th = |
57859
29e728588163
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
wenzelm
parents:
56334
diff
changeset
|
295 |
if Context_Position.is_really_visible ctxt |
52699 | 296 |
then warning (msg ^ Display.string_of_thm ctxt th) else () |
297 |
| warn_thm _ _ _ = (); |
|
42793 | 298 |
|
60650 | 299 |
fun warn_rules opt_context msg rules th = |
300 |
Item_Net.member rules th andalso (warn_thm opt_context msg th; true); |
|
42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset
|
301 |
|
60943 | 302 |
fun warn_claset opt_context th (CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = |
60650 | 303 |
warn_rules opt_context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse |
304 |
warn_rules opt_context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse |
|
60943 | 305 |
warn_rules opt_context "Rule already declared as introduction (intro)\n" unsafeIs th orelse |
306 |
warn_rules opt_context "Rule already declared as elimination (elim)\n" unsafeEs th; |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
307 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
308 |
|
1800 | 309 |
(*** Safe rules ***) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
310 |
|
60650 | 311 |
fun addSI w opt_context th |
60943 | 312 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
313 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
60650 | 314 |
if warn_rules opt_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
|
315 |
else |
42790 | 316 |
let |
60650 | 317 |
val ctxt = default_context opt_context th; |
59970 | 318 |
val th' = flat_rule ctxt th; |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
319 |
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
42790 | 320 |
List.partition Thm.no_prems [th']; |
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
321 |
val nI = Item_Net.length safeIs + 1; |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
322 |
val nE = Item_Net.length safeEs; |
60650 | 323 |
val _ = warn_claset opt_context th cs; |
42790 | 324 |
in |
325 |
CS |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
326 |
{safeIs = Item_Net.update th safeIs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
327 |
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
9938 | 328 |
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
42790 | 329 |
safeEs = safeEs, |
60943 | 330 |
unsafeIs = unsafeIs, |
331 |
unsafeEs = unsafeEs, |
|
42790 | 332 |
swrappers = swrappers, |
333 |
uwrappers = uwrappers, |
|
60943 | 334 |
unsafe_netpair = unsafe_netpair, |
42790 | 335 |
dup_netpair = dup_netpair, |
60942 | 336 |
extra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) extra_netpair} |
42790 | 337 |
end; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
338 |
|
60650 | 339 |
fun addSE w opt_context th |
60943 | 340 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
341 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
60650 | 342 |
if warn_rules opt_context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs |
343 |
else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
344 |
else |
42790 | 345 |
let |
60650 | 346 |
val ctxt = default_context opt_context th; |
59970 | 347 |
val th' = classical_rule ctxt (flat_rule ctxt th); |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
348 |
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
59582 | 349 |
List.partition (fn rl => Thm.nprems_of rl=1) [th']; |
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
350 |
val nI = Item_Net.length safeIs; |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
351 |
val nE = Item_Net.length safeEs + 1; |
60650 | 352 |
val _ = warn_claset opt_context th cs; |
42790 | 353 |
in |
354 |
CS |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
355 |
{safeEs = Item_Net.update th safeEs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
356 |
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
9938 | 357 |
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
42790 | 358 |
safeIs = safeIs, |
60943 | 359 |
unsafeIs = unsafeIs, |
360 |
unsafeEs = unsafeEs, |
|
42790 | 361 |
swrappers = swrappers, |
362 |
uwrappers = uwrappers, |
|
60943 | 363 |
unsafe_netpair = unsafe_netpair, |
42790 | 364 |
dup_netpair = dup_netpair, |
60942 | 365 |
extra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) extra_netpair} |
42790 | 366 |
end; |
0 | 367 |
|
60650 | 368 |
fun addSD w opt_context th = addSE w opt_context (make_elim opt_context th); |
42793 | 369 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
370 |
|
1800 | 371 |
(*** Hazardous (unsafe) rules ***) |
0 | 372 |
|
60650 | 373 |
fun addI w opt_context th |
60943 | 374 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
375 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
376 |
if warn_rules opt_context "Ignoring duplicate introduction (intro)\n" unsafeIs th then cs |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
377 |
else |
42790 | 378 |
let |
60650 | 379 |
val ctxt = default_context opt_context th; |
59970 | 380 |
val th' = flat_rule ctxt th; |
60943 | 381 |
val nI = Item_Net.length unsafeIs + 1; |
382 |
val nE = Item_Net.length unsafeEs; |
|
60650 | 383 |
val _ = warn_claset opt_context th cs; |
42790 | 384 |
in |
385 |
CS |
|
60943 | 386 |
{unsafeIs = Item_Net.update th unsafeIs, |
387 |
unsafe_netpair = insert (nI, nE) ([th'], []) unsafe_netpair, |
|
42790 | 388 |
dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, |
389 |
safeIs = safeIs, |
|
390 |
safeEs = safeEs, |
|
60943 | 391 |
unsafeEs = unsafeEs, |
42790 | 392 |
swrappers = swrappers, |
393 |
uwrappers = uwrappers, |
|
9938 | 394 |
safe0_netpair = safe0_netpair, |
395 |
safep_netpair = safep_netpair, |
|
60942 | 396 |
extra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) extra_netpair} |
42790 | 397 |
end |
398 |
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) |
|
60650 | 399 |
bad_thm opt_context "Ill-formed introduction rule" th; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
400 |
|
60650 | 401 |
fun addE w opt_context th |
60943 | 402 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
403 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
404 |
if warn_rules opt_context "Ignoring duplicate elimination (elim)\n" unsafeEs th then cs |
|
60650 | 405 |
else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
406 |
else |
42790 | 407 |
let |
60650 | 408 |
val ctxt = default_context opt_context th; |
59970 | 409 |
val th' = classical_rule ctxt (flat_rule ctxt th); |
60943 | 410 |
val nI = Item_Net.length unsafeIs; |
411 |
val nE = Item_Net.length unsafeEs + 1; |
|
60650 | 412 |
val _ = warn_claset opt_context th cs; |
42790 | 413 |
in |
414 |
CS |
|
60943 | 415 |
{unsafeEs = Item_Net.update th unsafeEs, |
416 |
unsafe_netpair = insert (nI, nE) ([], [th']) unsafe_netpair, |
|
59970 | 417 |
dup_netpair = insert (nI, nE) ([], [dup_elim ctxt th']) dup_netpair, |
42790 | 418 |
safeIs = safeIs, |
419 |
safeEs = safeEs, |
|
60943 | 420 |
unsafeIs = unsafeIs, |
42790 | 421 |
swrappers = swrappers, |
422 |
uwrappers = uwrappers, |
|
9938 | 423 |
safe0_netpair = safe0_netpair, |
424 |
safep_netpair = safep_netpair, |
|
60942 | 425 |
extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair} |
42790 | 426 |
end; |
0 | 427 |
|
60650 | 428 |
fun addD w opt_context th = addE w opt_context (make_elim opt_context th); |
42793 | 429 |
|
0 | 430 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
431 |
|
10736 | 432 |
(*** Deletion of rules |
1800 | 433 |
Working out what to delete, requires repeating much of the code used |
9938 | 434 |
to insert. |
1800 | 435 |
***) |
436 |
||
60650 | 437 |
fun delSI opt_context th |
60943 | 438 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
439 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
440 |
if Item_Net.member safeIs th then |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
441 |
let |
60650 | 442 |
val ctxt = default_context opt_context th; |
59970 | 443 |
val th' = flat_rule ctxt th; |
42790 | 444 |
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; |
445 |
in |
|
446 |
CS |
|
447 |
{safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
|
448 |
safep_netpair = delete (safep_rls, []) safep_netpair, |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
449 |
safeIs = Item_Net.remove th safeIs, |
42790 | 450 |
safeEs = safeEs, |
60943 | 451 |
unsafeIs = unsafeIs, |
452 |
unsafeEs = unsafeEs, |
|
42790 | 453 |
swrappers = swrappers, |
454 |
uwrappers = uwrappers, |
|
60943 | 455 |
unsafe_netpair = unsafe_netpair, |
42790 | 456 |
dup_netpair = dup_netpair, |
60942 | 457 |
extra_netpair = delete' ([th], []) extra_netpair} |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
458 |
end |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
459 |
else cs; |
1800 | 460 |
|
60650 | 461 |
fun delSE opt_context th |
60943 | 462 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
463 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
464 |
if Item_Net.member safeEs th then |
42790 | 465 |
let |
60650 | 466 |
val ctxt = default_context opt_context th; |
59970 | 467 |
val th' = classical_rule ctxt (flat_rule ctxt th); |
59582 | 468 |
val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th']; |
42790 | 469 |
in |
470 |
CS |
|
471 |
{safe0_netpair = delete ([], safe0_rls) safe0_netpair, |
|
472 |
safep_netpair = delete ([], safep_rls) safep_netpair, |
|
473 |
safeIs = safeIs, |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
474 |
safeEs = Item_Net.remove th safeEs, |
60943 | 475 |
unsafeIs = unsafeIs, |
476 |
unsafeEs = unsafeEs, |
|
42790 | 477 |
swrappers = swrappers, |
478 |
uwrappers = uwrappers, |
|
60943 | 479 |
unsafe_netpair = unsafe_netpair, |
42790 | 480 |
dup_netpair = dup_netpair, |
60942 | 481 |
extra_netpair = delete' ([], [th]) extra_netpair} |
42790 | 482 |
end |
483 |
else cs; |
|
1800 | 484 |
|
60650 | 485 |
fun delI opt_context th |
60943 | 486 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
487 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
488 |
if Item_Net.member unsafeIs th then |
|
59970 | 489 |
let |
60650 | 490 |
val ctxt = default_context opt_context th; |
59970 | 491 |
val th' = flat_rule ctxt th; |
492 |
in |
|
42790 | 493 |
CS |
60943 | 494 |
{unsafe_netpair = delete ([th'], []) unsafe_netpair, |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
495 |
dup_netpair = delete ([dup_intr th'], []) dup_netpair, |
42790 | 496 |
safeIs = safeIs, |
497 |
safeEs = safeEs, |
|
60943 | 498 |
unsafeIs = Item_Net.remove th unsafeIs, |
499 |
unsafeEs = unsafeEs, |
|
42790 | 500 |
swrappers = swrappers, |
501 |
uwrappers = uwrappers, |
|
9938 | 502 |
safe0_netpair = safe0_netpair, |
503 |
safep_netpair = safep_netpair, |
|
60942 | 504 |
extra_netpair = delete' ([th], []) extra_netpair} |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
505 |
end |
42790 | 506 |
else cs |
507 |
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) |
|
60650 | 508 |
bad_thm opt_context "Ill-formed introduction rule" th; |
1800 | 509 |
|
60650 | 510 |
fun delE opt_context th |
60943 | 511 |
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
512 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
513 |
if Item_Net.member unsafeEs th then |
|
59970 | 514 |
let |
60650 | 515 |
val ctxt = default_context opt_context th; |
59970 | 516 |
val th' = classical_rule ctxt (flat_rule ctxt th); |
517 |
in |
|
42790 | 518 |
CS |
60943 | 519 |
{unsafe_netpair = delete ([], [th']) unsafe_netpair, |
59970 | 520 |
dup_netpair = delete ([], [dup_elim ctxt th']) dup_netpair, |
42790 | 521 |
safeIs = safeIs, |
522 |
safeEs = safeEs, |
|
60943 | 523 |
unsafeIs = unsafeIs, |
524 |
unsafeEs = Item_Net.remove th unsafeEs, |
|
42790 | 525 |
swrappers = swrappers, |
526 |
uwrappers = uwrappers, |
|
9938 | 527 |
safe0_netpair = safe0_netpair, |
528 |
safep_netpair = safep_netpair, |
|
60942 | 529 |
extra_netpair = delete' ([], [th]) extra_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)*) |
60943 | 534 |
fun delrule opt_context th (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = |
42793 | 535 |
let val th' = Tactic.make_elim th in |
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
536 |
if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse |
60943 | 537 |
Item_Net.member unsafeIs th orelse Item_Net.member unsafeEs th orelse |
538 |
Item_Net.member safeEs th' orelse Item_Net.member unsafeEs th' |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
539 |
then |
60942 | 540 |
cs |
541 |
|> delE opt_context th' |
|
542 |
|> delSE opt_context th' |
|
543 |
|> delE opt_context th |
|
544 |
|> delI opt_context th |
|
545 |
|> delSE opt_context th |
|
546 |
|> delSI opt_context th |
|
60650 | 547 |
else (warn_thm opt_context "Undeclared classical rule\n" th; cs) |
9938 | 548 |
end; |
1800 | 549 |
|
550 |
||
42793 | 551 |
|
552 |
(** claset data **) |
|
42790 | 553 |
|
42793 | 554 |
(* wrappers *) |
42790 | 555 |
|
22674 | 556 |
fun map_swrappers f |
60943 | 557 |
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
558 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
559 |
CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
560 |
swrappers = f swrappers, uwrappers = uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
561 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
60943 | 562 |
unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
563 |
|
22674 | 564 |
fun map_uwrappers f |
60943 | 565 |
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, |
566 |
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = |
|
567 |
CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
568 |
swrappers = swrappers, uwrappers = f uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
569 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
60943 | 570 |
unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
571 |
|
22674 | 572 |
|
42793 | 573 |
(* merge_cs *) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
574 |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
575 |
(*Merge works by adding all new rules of the 2nd claset into the 1st claset, |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
576 |
in order to preserve priorities reliably.*) |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
577 |
|
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
578 |
fun merge_thms add thms1 thms2 = |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
579 |
fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2); |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
580 |
|
60943 | 581 |
fun merge_cs (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}, |
582 |
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, unsafeIs = unsafeIs2, unsafeEs = unsafeEs2, |
|
22674 | 583 |
swrappers, uwrappers, ...}) = |
24358 | 584 |
if pointer_eq (cs, cs') then cs |
585 |
else |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
586 |
cs |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
587 |
|> merge_thms (addSI NONE NONE) safeIs safeIs2 |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
588 |
|> merge_thms (addSE NONE NONE) safeEs safeEs2 |
60943 | 589 |
|> merge_thms (addI NONE NONE) unsafeIs unsafeIs2 |
590 |
|> merge_thms (addE NONE NONE) unsafeEs unsafeEs2 |
|
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
591 |
|> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) |
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset
|
592 |
|> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)); |
42793 | 593 |
|
594 |
||
595 |
(* data *) |
|
596 |
||
597 |
structure Claset = Generic_Data |
|
598 |
( |
|
599 |
type T = claset; |
|
600 |
val empty = empty_cs; |
|
601 |
val extend = I; |
|
602 |
val merge = merge_cs; |
|
603 |
); |
|
604 |
||
605 |
val claset_of = Claset.get o Context.Proof; |
|
606 |
val rep_claset_of = rep_cs o claset_of; |
|
607 |
||
608 |
val get_cs = Claset.get; |
|
609 |
val map_cs = Claset.map; |
|
610 |
||
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
611 |
fun map_theory_claset f thy = |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
612 |
let |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
613 |
val ctxt' = f (Proof_Context.init_global thy); |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
614 |
val thy' = Proof_Context.theory_of ctxt'; |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
615 |
in Context.theory_map (Claset.map (K (claset_of ctxt'))) thy' end; |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
616 |
|
42793 | 617 |
fun map_claset f = Context.proof_map (map_cs f); |
618 |
fun put_claset cs = map_claset (K cs); |
|
619 |
||
620 |
fun print_claset ctxt = |
|
621 |
let |
|
60943 | 622 |
val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; |
51584 | 623 |
val pretty_thms = map (Display.pretty_thm_item ctxt) o Item_Net.content; |
42793 | 624 |
in |
625 |
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), |
|
60943 | 626 |
Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs), |
42793 | 627 |
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), |
60943 | 628 |
Pretty.big_list "elimination rules (elim):" (pretty_thms unsafeEs), |
42793 | 629 |
Pretty.strs ("safe wrappers:" :: map #1 swrappers), |
630 |
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] |
|
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
54742
diff
changeset
|
631 |
|> Pretty.writeln_chunks |
42793 | 632 |
end; |
633 |
||
634 |
||
635 |
(* old-style declarations *) |
|
636 |
||
637 |
fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt; |
|
638 |
||
639 |
val op addSIs = decl (addSI NONE); |
|
640 |
val op addSEs = decl (addSE NONE); |
|
641 |
val op addSDs = decl (addSD NONE); |
|
642 |
val op addIs = decl (addI NONE); |
|
643 |
val op addEs = decl (addE NONE); |
|
644 |
val op addDs = decl (addD NONE); |
|
645 |
val op delrules = decl delrule; |
|
646 |
||
647 |
||
648 |
||
649 |
(*** Modifying the wrapper tacticals ***) |
|
650 |
||
651 |
fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); |
|
652 |
fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); |
|
653 |
||
654 |
fun update_warn msg (p as (key : string, _)) xs = |
|
655 |
(if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); |
|
656 |
||
657 |
fun delete_warn msg (key : string) xs = |
|
658 |
if AList.defined (op =) xs key then AList.delete (op =) key xs |
|
659 |
else (warning msg; xs); |
|
660 |
||
661 |
(*Add/replace a safe wrapper*) |
|
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
662 |
fun ctxt addSWrapper new_swrapper = ctxt |> map_claset |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
663 |
(map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper)); |
42793 | 664 |
|
665 |
(*Add/replace an unsafe wrapper*) |
|
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
666 |
fun ctxt addWrapper new_uwrapper = ctxt |> map_claset |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
667 |
(map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper)); |
42793 | 668 |
|
669 |
(*Remove a safe wrapper*) |
|
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
670 |
fun ctxt delSWrapper name = ctxt |> map_claset |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
671 |
(map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name)); |
42793 | 672 |
|
673 |
(*Remove an unsafe wrapper*) |
|
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
674 |
fun ctxt delWrapper name = ctxt |> map_claset |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset
|
675 |
(map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name)); |
42793 | 676 |
|
677 |
(* compose a safe tactic alternatively before/after safe_step_tac *) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
678 |
fun ctxt addSbefore (name, tac1) = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
679 |
ctxt addSWrapper (name, fn ctxt => fn tac2 => tac1 ctxt ORELSE' tac2); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
680 |
fun ctxt addSafter (name, tac2) = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
681 |
ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt); |
42793 | 682 |
|
683 |
(*compose a tactic alternatively before/after the step tactic *) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
684 |
fun ctxt addbefore (name, tac1) = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
685 |
ctxt addWrapper (name, fn ctxt => fn tac2 => tac1 ctxt APPEND' tac2); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
686 |
fun ctxt addafter (name, tac2) = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
687 |
ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt); |
42793 | 688 |
|
58957 | 689 |
fun ctxt addD2 (name, thm) = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
690 |
ctxt addafter (name, fn ctxt' => dresolve_tac ctxt' [thm] THEN' assume_tac ctxt'); |
58957 | 691 |
fun ctxt addE2 (name, thm) = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
692 |
ctxt addafter (name, fn ctxt' => eresolve_tac ctxt' [thm] THEN' assume_tac ctxt'); |
58957 | 693 |
fun ctxt addSD2 (name, thm) = |
694 |
ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac); |
|
695 |
fun ctxt addSE2 (name, thm) = |
|
696 |
ctxt addSafter (name, fn ctxt' => ematch_tac ctxt' [thm] THEN' eq_assume_tac); |
|
42793 | 697 |
|
1711 | 698 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
699 |
|
1800 | 700 |
(**** Simple tactics for theorem proving ****) |
0 | 701 |
|
702 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
42793 | 703 |
fun safe_step_tac ctxt = |
704 |
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in |
|
705 |
appSWrappers ctxt |
|
706 |
(FIRST' |
|
707 |
[eq_assume_tac, |
|
58957 | 708 |
eq_mp_tac ctxt, |
59164 | 709 |
bimatch_from_nets_tac ctxt safe0_netpair, |
51798 | 710 |
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), |
59164 | 711 |
bimatch_from_nets_tac ctxt safep_netpair]) |
42793 | 712 |
end; |
0 | 713 |
|
5757 | 714 |
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) |
42793 | 715 |
fun safe_steps_tac ctxt = |
716 |
REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i)); |
|
5757 | 717 |
|
0 | 718 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
42793 | 719 |
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
|
720 |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
721 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
722 |
(*** 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
|
723 |
|
42790 | 724 |
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
|
725 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
726 |
(*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
|
727 |
create precisely n subgoals.*) |
59164 | 728 |
fun n_bimatch_from_nets_tac ctxt n = |
729 |
biresolution_from_nets_tac ctxt (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
|
730 |
|
58957 | 731 |
fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i; |
732 |
fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt; |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
733 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
734 |
(*Two-way branching is allowed only if one of the branches immediately closes*) |
58957 | 735 |
fun bimatch2_tac ctxt netpair i = |
59164 | 736 |
n_bimatch_from_nets_tac ctxt 2 netpair i THEN |
58957 | 737 |
(eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1)); |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
738 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
739 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
42793 | 740 |
fun clarify_step_tac ctxt = |
741 |
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in |
|
742 |
appSWrappers ctxt |
|
743 |
(FIRST' |
|
58957 | 744 |
[eq_assume_contr_tac ctxt, |
59164 | 745 |
bimatch_from_nets_tac ctxt safe0_netpair, |
51798 | 746 |
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), |
59164 | 747 |
n_bimatch_from_nets_tac ctxt 1 safep_netpair, |
58957 | 748 |
bimatch2_tac ctxt safep_netpair]) |
42793 | 749 |
end; |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
750 |
|
42793 | 751 |
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
|
752 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
753 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
754 |
(*** 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
|
755 |
|
4066 | 756 |
(*Backtracking is allowed among the various these unsafe ways of |
757 |
proving a subgoal. *) |
|
42793 | 758 |
fun inst0_step_tac ctxt = |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
759 |
assume_tac ctxt APPEND' |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58958
diff
changeset
|
760 |
contr_tac ctxt APPEND' |
59164 | 761 |
biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt)); |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
762 |
|
4066 | 763 |
(*These unsafe steps could generate more subgoals.*) |
42793 | 764 |
fun instp_step_tac ctxt = |
59164 | 765 |
biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt)); |
0 | 766 |
|
767 |
(*These steps could instantiate variables and are therefore unsafe.*) |
|
42793 | 768 |
fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; |
0 | 769 |
|
60943 | 770 |
fun unsafe_step_tac ctxt = |
771 |
biresolve_from_nets_tac ctxt (#unsafe_netpair (rep_claset_of ctxt)); |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
772 |
|
0 | 773 |
(*Single step for the prover. FAILS unless it makes progress. *) |
42793 | 774 |
fun step_tac ctxt i = |
60943 | 775 |
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' unsafe_step_tac ctxt) i; |
0 | 776 |
|
777 |
(*Using a "safe" rule to instantiate variables is unsafe. This tactic |
|
778 |
allows backtracking from "safe" rules to "unsafe" rules here.*) |
|
42793 | 779 |
fun slow_step_tac ctxt i = |
60943 | 780 |
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' unsafe_step_tac ctxt) i; |
0 | 781 |
|
42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset
|
782 |
|
1800 | 783 |
(**** The following tactics all fail unless they solve one goal ****) |
0 | 784 |
|
785 |
(*Dumb but fast*) |
|
42793 | 786 |
fun fast_tac ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
787 |
Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); |
0 | 788 |
|
789 |
(*Slower but smarter than fast_tac*) |
|
42793 | 790 |
fun best_tac ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
791 |
Object_Logic.atomize_prems_tac ctxt THEN' |
42793 | 792 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); |
0 | 793 |
|
9402 | 794 |
(*even a bit smarter than best_tac*) |
42793 | 795 |
fun first_best_tac ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
796 |
Object_Logic.atomize_prems_tac ctxt THEN' |
42793 | 797 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); |
9402 | 798 |
|
42793 | 799 |
fun slow_tac ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
800 |
Object_Logic.atomize_prems_tac ctxt THEN' |
42793 | 801 |
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1)); |
0 | 802 |
|
42793 | 803 |
fun slow_best_tac ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
804 |
Object_Logic.atomize_prems_tac ctxt THEN' |
42793 | 805 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); |
0 | 806 |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
807 |
|
10736 | 808 |
(***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
|
809 |
|
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset
|
810 |
val weight_ASTAR = 5; |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
811 |
|
42793 | 812 |
fun astar_tac ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
813 |
Object_Logic.atomize_prems_tac ctxt THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
814 |
SELECT_GOAL |
52462
a241826ed003
actually use Data.sizef, not hardwired size_of_thm;
wenzelm
parents:
51798
diff
changeset
|
815 |
(ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) |
42793 | 816 |
(step_tac ctxt 1)); |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
817 |
|
42793 | 818 |
fun slow_astar_tac ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
819 |
Object_Logic.atomize_prems_tac ctxt THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
820 |
SELECT_GOAL |
52462
a241826ed003
actually use Data.sizef, not hardwired size_of_thm;
wenzelm
parents:
51798
diff
changeset
|
821 |
(ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) |
42793 | 822 |
(slow_step_tac ctxt 1)); |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
823 |
|
42790 | 824 |
|
1800 | 825 |
(**** 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
|
826 |
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
|
827 |
easy theorems faster, but loses completeness -- and many of the harder |
1800 | 828 |
theorems such as 43. ****) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
829 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
830 |
(*Non-deterministic! Could always expand the first unsafe connective. |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
831 |
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
|
832 |
greater search depth required.*) |
42793 | 833 |
fun dup_step_tac ctxt = |
59164 | 834 |
biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt)); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
835 |
|
5523 | 836 |
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) |
5757 | 837 |
local |
42793 | 838 |
fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt); |
42790 | 839 |
in |
42793 | 840 |
fun depth_tac ctxt m i state = SELECT_GOAL |
841 |
(safe_steps_tac ctxt 1 THEN_ELSE |
|
842 |
(DEPTH_SOLVE (depth_tac ctxt m 1), |
|
843 |
inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac |
|
844 |
(slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state; |
|
5757 | 845 |
end; |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
846 |
|
10736 | 847 |
(*Search, with depth bound m. |
2173 | 848 |
This is the "entry point", which does safe inferences first.*) |
42793 | 849 |
fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) => |
850 |
let |
|
851 |
val deti = (*No Vars in the goal? No need to backtrack between goals.*) |
|
852 |
if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I; |
|
42790 | 853 |
in |
42793 | 854 |
SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i |
42790 | 855 |
end); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
856 |
|
42793 | 857 |
fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); |
24021 | 858 |
|
859 |
||
5885 | 860 |
(* attributes *) |
861 |
||
42793 | 862 |
fun attrib f = |
60650 | 863 |
Thm.declaration_attribute (fn th => fn opt_context => |
864 |
map_cs (f (SOME opt_context) th) opt_context); |
|
5885 | 865 |
|
18691 | 866 |
val safe_elim = attrib o addSE; |
867 |
val safe_intro = attrib o addSI; |
|
42793 | 868 |
val safe_dest = attrib o addSD; |
60943 | 869 |
val unsafe_elim = attrib o addE; |
870 |
val unsafe_intro = attrib o addI; |
|
871 |
val unsafe_dest = attrib o addD; |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset
|
872 |
|
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset
|
873 |
val rule_del = |
60650 | 874 |
Thm.declaration_attribute (fn th => fn opt_context => |
875 |
opt_context |> map_cs (delrule (SOME opt_context) th) |> |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset
|
876 |
Thm.attribute_declaration Context_Rules.rule_del th); |
5885 | 877 |
|
878 |
||
5841 | 879 |
|
5885 | 880 |
(** concrete syntax of attributes **) |
5841 | 881 |
|
882 |
val introN = "intro"; |
|
883 |
val elimN = "elim"; |
|
884 |
val destN = "dest"; |
|
885 |
||
58826 | 886 |
val _ = |
887 |
Theory.setup |
|
888 |
(Attrib.setup @{binding swapped} (Scan.succeed swapped) |
|
889 |
"classical swap of introduction rule" #> |
|
60943 | 890 |
Attrib.setup @{binding dest} (Context_Rules.add safe_dest unsafe_dest Context_Rules.dest_query) |
58826 | 891 |
"declaration of Classical destruction rule" #> |
60943 | 892 |
Attrib.setup @{binding elim} (Context_Rules.add safe_elim unsafe_elim Context_Rules.elim_query) |
58826 | 893 |
"declaration of Classical elimination rule" #> |
60943 | 894 |
Attrib.setup @{binding intro} (Context_Rules.add safe_intro unsafe_intro Context_Rules.intro_query) |
58826 | 895 |
"declaration of Classical introduction rule" #> |
896 |
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) |
|
897 |
"remove declaration of intro/elim/dest rule"); |
|
5841 | 898 |
|
899 |
||
900 |
||
7230 | 901 |
(** proof methods **) |
902 |
||
903 |
local |
|
904 |
||
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset
|
905 |
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => |
5841 | 906 |
let |
33369 | 907 |
val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; |
60942 | 908 |
val {extra_netpair, ...} = rep_claset_of ctxt; |
909 |
val rules3 = Context_Rules.find_rules_netpair true facts goal extra_netpair; |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
910 |
val rules = rules1 @ rules2 @ rules3 @ rules4; |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58893
diff
changeset
|
911 |
val ruleq = Drule.multi_resolves (SOME ctxt) facts rules; |
52732 | 912 |
val _ = Method.trace ctxt rules; |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
913 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
914 |
fn st => Seq.maps (fn rule => resolve_tac ctxt [rule] i st) ruleq |
18834 | 915 |
end) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
916 |
THEN_ALL_NEW Goal.norm_hhf_tac ctxt; |
5841 | 917 |
|
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset
|
918 |
in |
7281 | 919 |
|
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset
|
920 |
fun rule_tac ctxt [] facts = some_rule_tac ctxt facts |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
921 |
| rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts; |
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset
|
922 |
|
60619
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset
|
923 |
fun standard_tac ctxt facts = |
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset
|
924 |
HEADGOAL (some_rule_tac ctxt facts) ORELSE |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
925 |
Class.standard_intro_classes_tac ctxt facts; |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
926 |
|
60619
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset
|
927 |
fun default_tac ctxt facts st = |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
928 |
(if Method.detect_closure_state st then |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
929 |
legacy_feature |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
930 |
("Old method \"default\"; use \"standard\" instead" ^ Position.here (Position.thread_data ())) |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
931 |
else (); |
60619
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset
|
932 |
standard_tac ctxt facts st); |
10309 | 933 |
|
7230 | 934 |
end; |
5841 | 935 |
|
936 |
||
6502 | 937 |
(* automatic methods *) |
5841 | 938 |
|
5927 | 939 |
val cla_modifiers = |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset
|
940 |
[Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) @{here}), |
60943 | 941 |
Args.$$$ destN -- Args.colon >> K (Method.modifier (unsafe_dest NONE) @{here}), |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset
|
942 |
Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) @{here}), |
60943 | 943 |
Args.$$$ elimN -- Args.colon >> K (Method.modifier (unsafe_elim NONE) @{here}), |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset
|
944 |
Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) @{here}), |
60943 | 945 |
Args.$$$ introN -- Args.colon >> K (Method.modifier (unsafe_intro NONE) @{here}), |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset
|
946 |
Args.del -- Args.colon >> K (Method.modifier rule_del @{here})]; |
5927 | 947 |
|
42793 | 948 |
fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac); |
949 |
fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); |
|
5841 | 950 |
|
951 |
||
952 |
||
58826 | 953 |
(** method setup **) |
5841 | 954 |
|
58826 | 955 |
val _ = |
956 |
Theory.setup |
|
60619
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset
|
957 |
(Method.setup @{binding standard} (Scan.succeed (METHOD o standard_tac)) |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
958 |
"standard proof step: classical intro/elim rule or class introduction" #> |
60619
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset
|
959 |
Method.setup @{binding default} (Scan.succeed (METHOD o default_tac)) |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset
|
960 |
"standard proof step: classical intro/elim rule or class introduction (legacy)" #> |
58826 | 961 |
Method.setup @{binding rule} |
962 |
(Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) |
|
963 |
"apply some intro/elim rule (potentially classical)" #> |
|
964 |
Method.setup @{binding contradiction} |
|
965 |
(Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])) |
|
966 |
"proof by contradiction" #> |
|
967 |
Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac)) |
|
968 |
"repeatedly apply safe steps" #> |
|
969 |
Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #> |
|
970 |
Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #> |
|
971 |
Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #> |
|
972 |
Method.setup @{binding deepen} |
|
973 |
(Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers |
|
974 |
>> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n))) |
|
975 |
"classical prover (iterative deepening)" #> |
|
976 |
Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) |
|
977 |
"classical prover (apply safe rules)" #> |
|
978 |
Method.setup @{binding safe_step} (cla_method' safe_step_tac) |
|
979 |
"single classical step (safe rules)" #> |
|
980 |
Method.setup @{binding inst_step} (cla_method' inst_step_tac) |
|
981 |
"single classical step (safe rules, allow instantiations)" #> |
|
982 |
Method.setup @{binding step} (cla_method' step_tac) |
|
983 |
"single classical step (safe and unsafe rules)" #> |
|
984 |
Method.setup @{binding slow_step} (cla_method' slow_step_tac) |
|
985 |
"single classical step (safe and unsafe rules, allow backtracking)" #> |
|
986 |
Method.setup @{binding clarify_step} (cla_method' clarify_step_tac) |
|
987 |
"single classical step (safe rules, without splitting)"); |
|
5841 | 988 |
|
8667 | 989 |
|
990 |
(** outer syntax **) |
|
991 |
||
24867 | 992 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59582
diff
changeset
|
993 |
Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner" |
60097
d20ca79d50e4
discontinued pointless warnings: commands are only defined inside a theory context;
wenzelm
parents:
59970
diff
changeset
|
994 |
(Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of))); |
8667 | 995 |
|
5841 | 996 |
end; |