author | wenzelm |
Wed, 31 Jul 2019 19:50:38 +0200 | |
changeset 70451 | 550a5a822edb |
parent 69101 | 991a3feaf270 |
child 74282 | c2ee8d993d6a |
permissions | -rw-r--r-- |
10805 | 1 |
(* Title: Pure/tactic.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
0 | 3 |
|
29276 | 4 |
Fundamental tactics. |
0 | 5 |
*) |
6 |
||
11774 | 7 |
signature BASIC_TACTIC = |
8 |
sig |
|
23223 | 9 |
val trace_goalno_tac: (int -> tactic) -> int -> tactic |
36546 | 10 |
val rule_by_tactic: Proof.context -> tactic -> thm -> thm |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
11 |
val assume_tac: Proof.context -> int -> tactic |
23223 | 12 |
val eq_assume_tac: int -> tactic |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset
|
13 |
val compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic |
23223 | 14 |
val make_elim: thm -> thm |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
15 |
val biresolve0_tac: (bool * thm) list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
16 |
val biresolve_tac: Proof.context -> (bool * thm) list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
17 |
val resolve0_tac: thm list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
18 |
val resolve_tac: Proof.context -> thm list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
19 |
val eresolve0_tac: thm list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
20 |
val eresolve_tac: Proof.context -> thm list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
21 |
val forward_tac: Proof.context -> thm list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
22 |
val dresolve0_tac: thm list -> int -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
23 |
val dresolve_tac: Proof.context -> thm list -> int -> tactic |
60774 | 24 |
val ares_tac: Proof.context -> thm list -> int -> tactic |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
25 |
val solve_tac: Proof.context -> thm list -> int -> tactic |
58957 | 26 |
val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic |
27 |
val match_tac: Proof.context -> thm list -> int -> tactic |
|
28 |
val ematch_tac: Proof.context -> thm list -> int -> tactic |
|
29 |
val dmatch_tac: Proof.context -> thm list -> int -> tactic |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
30 |
val flexflex_tac: Proof.context -> tactic |
23223 | 31 |
val distinct_subgoals_tac: tactic |
46704 | 32 |
val cut_tac: thm -> int -> tactic |
23223 | 33 |
val cut_rules_tac: thm list -> int -> tactic |
34 |
val cut_facts_tac: thm list -> int -> tactic |
|
35 |
val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list |
|
59164 | 36 |
val biresolution_from_nets_tac: Proof.context -> |
37 |
('a list -> (bool * thm) list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic |
|
38 |
val biresolve_from_nets_tac: Proof.context -> |
|
39 |
(int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic |
|
40 |
val bimatch_from_nets_tac: Proof.context -> |
|
41 |
(int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic |
|
42 |
val filt_resolve_from_net_tac: Proof.context -> int -> (int * thm) Net.net -> int -> tactic |
|
43 |
val resolve_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic |
|
44 |
val match_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic |
|
23223 | 45 |
val subgoals_of_brl: bool * thm -> int |
46 |
val lessb: (bool * thm) * (bool * thm) -> bool |
|
27243
d549b5b0f344
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
wenzelm
parents:
27209
diff
changeset
|
47 |
val rename_tac: string list -> int -> tactic |
23223 | 48 |
val rotate_tac: int -> int -> tactic |
49 |
val defer_tac: int -> tactic |
|
49865 | 50 |
val prefer_tac: int -> tactic |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
51 |
val filter_prems_tac: Proof.context -> (term -> bool) -> int -> tactic |
11774 | 52 |
end; |
0 | 53 |
|
11774 | 54 |
signature TACTIC = |
55 |
sig |
|
56 |
include BASIC_TACTIC |
|
23223 | 57 |
val insert_tagged_brl: 'a * (bool * thm) -> |
58 |
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> |
|
59 |
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net |
|
60 |
val delete_tagged_brl: bool * thm -> |
|
61 |
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> |
|
62 |
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net |
|
63 |
val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool |
|
32971 | 64 |
val build_net: thm list -> (int * thm) Net.net |
11774 | 65 |
end; |
0 | 66 |
|
11774 | 67 |
structure Tactic: TACTIC = |
0 | 68 |
struct |
69 |
||
1501 | 70 |
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) |
10817 | 71 |
fun trace_goalno_tac tac i st = |
4270 | 72 |
case Seq.pull(tac i st) of |
15531 | 73 |
NONE => Seq.empty |
12262 | 74 |
| seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |
10805 | 75 |
Seq.make(fn()=> seqcell)); |
0 | 76 |
|
77 |
(*Makes a rule by applying a tactic to an existing rule*) |
|
36546 | 78 |
fun rule_by_tactic ctxt tac rl = |
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset
|
79 |
let |
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51602
diff
changeset
|
80 |
val thy = Proof_Context.theory_of ctxt; |
36546 | 81 |
val ctxt' = Variable.declare_thm rl ctxt; |
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51602
diff
changeset
|
82 |
val ((_, [st]), ctxt'') = Variable.import true [Thm.transfer thy rl] ctxt'; |
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset
|
83 |
in |
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset
|
84 |
(case Seq.pull (tac st) of |
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset
|
85 |
NONE => raise THM ("rule_by_tactic", 0, [rl]) |
36546 | 86 |
| SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st')) |
2688 | 87 |
end; |
10817 | 88 |
|
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset
|
89 |
|
0 | 90 |
(*** Basic tactics ***) |
91 |
||
92 |
(*** The following fail if the goal number is out of range: |
|
93 |
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) |
|
94 |
||
95 |
(*Solve subgoal i by assumption*) |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
96 |
fun assume_tac ctxt i = PRIMSEQ (Thm.assumption (SOME ctxt) i); |
0 | 97 |
|
98 |
(*Solve subgoal i by assumption, using no unification*) |
|
31945 | 99 |
fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i); |
0 | 100 |
|
23223 | 101 |
|
0 | 102 |
(** Resolution/matching tactics **) |
103 |
||
104 |
(*The composition rule/state: no lifting or var renaming. |
|
31945 | 105 |
The arg = (bires_flg, orule, m); see Thm.bicompose for explanation.*) |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset
|
106 |
fun compose_tac ctxt arg i = |
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset
|
107 |
PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} arg i); |
0 | 108 |
|
67721 | 109 |
(*Converts a "destruct" rule like P \<and> Q \<Longrightarrow> P to an "elimination" rule |
110 |
like \<lbrakk>P \<and> Q; P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R *) |
|
0 | 111 |
fun make_elim rl = zero_var_indexes (rl RS revcut_rl); |
112 |
||
113 |
(*Attack subgoal i by resolution, using flags to indicate elimination rules*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
114 |
fun biresolve0_tac brules i = PRIMSEQ (Thm.biresolution NONE false brules i); |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
115 |
fun biresolve_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) false brules i); |
0 | 116 |
|
117 |
(*Resolution: the simple case, works for introduction rules*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
118 |
fun resolve0_tac rules = biresolve0_tac (map (pair false) rules); |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
119 |
fun resolve_tac ctxt rules = biresolve_tac ctxt (map (pair false) rules); |
0 | 120 |
|
121 |
(*Resolution with elimination rules only*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
122 |
fun eresolve0_tac rules = biresolve0_tac (map (pair true) rules); |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
123 |
fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules); |
0 | 124 |
|
125 |
(*Forward reasoning using destruction rules.*) |
|
60776 | 126 |
fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' assume_tac ctxt; |
0 | 127 |
|
128 |
(*Like forward_tac, but deletes the assumption after use.*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
129 |
fun dresolve0_tac rls = eresolve0_tac (map make_elim rls); |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
130 |
fun dresolve_tac ctxt rls = eresolve_tac ctxt (map make_elim rls); |
0 | 131 |
|
60774 | 132 |
(*Use an assumption or some rules*) |
133 |
fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules; |
|
0 | 134 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
135 |
fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt; |
5263 | 136 |
|
0 | 137 |
(*Matching tactics -- as above, but forbid updating of state*) |
58957 | 138 |
fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i); |
139 |
fun match_tac ctxt rules = bimatch_tac ctxt (map (pair false) rules); |
|
140 |
fun ematch_tac ctxt rules = bimatch_tac ctxt (map (pair true) rules); |
|
141 |
fun dmatch_tac ctxt rls = ematch_tac ctxt (map make_elim rls); |
|
0 | 142 |
|
143 |
(*Smash all flex-flex disagreement pairs in the proof state.*) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
144 |
fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt)); |
0 | 145 |
|
19056
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset
|
146 |
(*Remove duplicate subgoals.*) |
69101
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
147 |
fun distinct_subgoals_tac st = |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
148 |
let |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
149 |
val subgoals = Thm.cprems_of st; |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
150 |
val (tab, n) = |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
151 |
(subgoals, (Ctermtab.empty, 0)) |-> fold (fn ct => fn (tab, i) => |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
152 |
if Ctermtab.defined tab ct then (tab, i) |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
153 |
else (Ctermtab.update (ct, i) tab, i + 1)); |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
154 |
val st' = |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
155 |
if n = length subgoals then st |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
156 |
else |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
157 |
let |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
158 |
val thy = Thm.theory_of_thm st; |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
159 |
fun cert_prop i = Thm.global_cterm_of thy (Free (Name.bound i, propT)); |
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset
|
160 |
|
69101
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
161 |
val As = map (cert_prop o the o Ctermtab.lookup tab) subgoals; |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
162 |
val As' = map cert_prop (0 upto (n - 1)); |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
163 |
val C = cert_prop n; |
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset
|
164 |
|
69101
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
165 |
val template = Drule.list_implies (As, C); |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
166 |
val inst = |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
167 |
(dest_Free (Thm.term_of C), Thm.cconcl_of st) :: |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
168 |
Ctermtab.fold (fn (ct, i) => cons ((Name.bound i, propT), ct)) tab []; |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
169 |
in |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
170 |
Thm.assume template |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
171 |
|> fold (Thm.elim_implies o Thm.assume) As |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
172 |
|> fold_rev Thm.implies_intr As' |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
173 |
|> Thm.implies_intr template |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
174 |
|> Thm.instantiate_frees ([], inst) |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
175 |
|> Thm.elim_implies st |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
176 |
end; |
991a3feaf270
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
wenzelm
parents:
68825
diff
changeset
|
177 |
in Seq.single st' end; |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
178 |
|
1951 | 179 |
|
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
180 |
(*** Applications of cut_rl ***) |
0 | 181 |
|
182 |
(*The conclusion of the rule gets assumed in subgoal i, |
|
183 |
while subgoal i+1,... are the premises of the rule.*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset
|
184 |
fun cut_tac rule i = resolve0_tac [cut_rl] i THEN resolve0_tac [rule] (i + 1); |
0 | 185 |
|
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
186 |
(*"Cut" a list of rules into the goal. Their premises will become new |
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
187 |
subgoals.*) |
46704 | 188 |
fun cut_rules_tac ths i = EVERY (map (fn th => cut_tac th i) ths); |
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
189 |
|
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
190 |
(*As above, but inserts only facts (unconditional theorems); |
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
191 |
generates no additional subgoals. *) |
20232 | 192 |
fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths); |
0 | 193 |
|
194 |
||
195 |
(**** Indexing and filtering of theorems ****) |
|
196 |
||
197 |
(*Returns the list of potentially resolvable theorems for the goal "prem", |
|
10805 | 198 |
using the predicate could(subgoal,concl). |
0 | 199 |
Resulting list is no longer than "limit"*) |
200 |
fun filter_thms could (limit, prem, ths) = |
|
201 |
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*) |
|
202 |
fun filtr (limit, []) = [] |
|
10805 | 203 |
| filtr (limit, th::ths) = |
204 |
if limit=0 then [] |
|
59582 | 205 |
else if could(pb, Thm.concl_of th) then th :: filtr(limit-1, ths) |
10805 | 206 |
else filtr(limit,ths) |
0 | 207 |
in filtr(limit,ths) end; |
208 |
||
209 |
||
210 |
(*** biresolution and resolution using nets ***) |
|
211 |
||
212 |
(** To preserve the order of the rules, tag them with increasing integers **) |
|
213 |
||
214 |
(*insert one tagged brl into the pair of nets*) |
|
23178 | 215 |
fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) = |
12320 | 216 |
if eres then |
217 |
(case try Thm.major_prem_of th of |
|
16809 | 218 |
SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet) |
15531 | 219 |
| NONE => error "insert_tagged_brl: elimination rule with no premises") |
59582 | 220 |
else (Net.insert_term (K false) (Thm.concl_of th, kbrl) inet, enet); |
0 | 221 |
|
12320 | 222 |
(*delete one kbrl from the pair of nets*) |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21708
diff
changeset
|
223 |
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th') |
16809 | 224 |
|
23178 | 225 |
fun delete_tagged_brl (brl as (eres, th)) (inet, enet) = |
13925 | 226 |
(if eres then |
12320 | 227 |
(case try Thm.major_prem_of th of |
16809 | 228 |
SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet) |
15531 | 229 |
| NONE => (inet, enet)) (*no major premise: ignore*) |
16809 | 230 |
else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet)) |
13925 | 231 |
handle Net.DELETE => (inet,enet); |
1801 | 232 |
|
233 |
||
10817 | 234 |
(*biresolution using a pair of nets rather than rules. |
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
235 |
function "order" must sort and possibly filter the list of brls. |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
236 |
boolean "match" indicates matching or unification.*) |
59164 | 237 |
fun biresolution_from_nets_tac ctxt order match (inet, enet) = |
0 | 238 |
SUBGOAL |
59164 | 239 |
(fn (prem, i) => |
240 |
let |
|
241 |
val hyps = Logic.strip_assums_hyp prem; |
|
242 |
val concl = Logic.strip_assums_concl prem; |
|
243 |
val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps; |
|
244 |
in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order kbrls) i) end); |
|
0 | 245 |
|
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
246 |
(*versions taking pre-built nets. No filtering of brls*) |
59164 | 247 |
fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list false; |
248 |
fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list true; |
|
0 | 249 |
|
250 |
||
251 |
(*** Simpler version for resolve_tac -- only one net, and no hyps ***) |
|
252 |
||
253 |
(*insert one tagged rl into the net*) |
|
23178 | 254 |
fun insert_krl (krl as (k,th)) = |
59582 | 255 |
Net.insert_term (K false) (Thm.concl_of th, krl); |
0 | 256 |
|
257 |
(*build a net of rules for resolution*) |
|
10817 | 258 |
fun build_net rls = |
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
29276
diff
changeset
|
259 |
fold_rev insert_krl (tag_list 1 rls) Net.empty; |
0 | 260 |
|
261 |
(*resolution using a net rather than rules; pred supports filt_resolve_tac*) |
|
59164 | 262 |
fun filt_resolution_from_net_tac ctxt match pred net = |
263 |
SUBGOAL (fn (prem, i) => |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
264 |
let val krls = Net.unify_term net (Logic.strip_assums_concl prem) in |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
265 |
if pred krls then |
59164 | 266 |
PRIMSEQ (Thm.biresolution (SOME ctxt) match (map (pair false) (order_list krls)) i) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
267 |
else no_tac |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
268 |
end); |
0 | 269 |
|
270 |
(*Resolve the subgoal using the rules (making a net) unless too flexible, |
|
271 |
which means more than maxr rules are unifiable. *) |
|
59164 | 272 |
fun filt_resolve_from_net_tac ctxt maxr net = |
273 |
let fun pred krls = length krls <= maxr |
|
274 |
in filt_resolution_from_net_tac ctxt false pred net end; |
|
0 | 275 |
|
276 |
(*versions taking pre-built nets*) |
|
59164 | 277 |
fun resolve_from_net_tac ctxt = filt_resolution_from_net_tac ctxt false (K true); |
278 |
fun match_from_net_tac ctxt = filt_resolution_from_net_tac ctxt true (K true); |
|
0 | 279 |
|
280 |
||
281 |
(*** For Natural Deduction using (bires_flg, rule) pairs ***) |
|
282 |
||
283 |
(*The number of new subgoals produced by the brule*) |
|
59582 | 284 |
fun subgoals_of_brl (true, rule) = Thm.nprems_of rule - 1 |
285 |
| subgoals_of_brl (false, rule) = Thm.nprems_of rule; |
|
0 | 286 |
|
287 |
(*Less-than test: for sorting to minimize number of new subgoals*) |
|
288 |
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; |
|
289 |
||
290 |
||
27243
d549b5b0f344
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
wenzelm
parents:
27209
diff
changeset
|
291 |
(*Renaming of parameters in a subgoal*) |
d549b5b0f344
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
wenzelm
parents:
27209
diff
changeset
|
292 |
fun rename_tac xs i = |
59584 | 293 |
case find_first (not o Symbol_Pos.is_identifier) xs of |
15531 | 294 |
SOME x => error ("Not an identifier: " ^ x) |
31945 | 295 |
| NONE => PRIMITIVE (Thm.rename_params_rule (xs, i)); |
9535 | 296 |
|
1501 | 297 |
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from |
298 |
right to left if n is positive, and from left to right if n is negative.*) |
|
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset
|
299 |
fun rotate_tac 0 i = all_tac |
31945 | 300 |
| rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i); |
1209 | 301 |
|
59749 | 302 |
(*Rotate the given subgoal to be the last.*) |
31945 | 303 |
fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1); |
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset
|
304 |
|
59749 | 305 |
(*Rotate the given subgoal to be the first.*) |
49865 | 306 |
fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1); |
307 |
||
59749 | 308 |
(*Remove premises that do not satisfy pred; fails if all prems satisfy pred.*) |
309 |
fun filter_prems_tac ctxt pred = |
|
310 |
let |
|
311 |
fun Then NONE tac = SOME tac |
|
312 |
| Then (SOME tac) tac' = SOME (tac THEN' tac'); |
|
313 |
fun thins H (tac, n) = |
|
314 |
if pred H then (tac, n + 1) |
|
315 |
else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0); |
|
316 |
in |
|
317 |
SUBGOAL (fn (goal, i) => |
|
318 |
let val Hs = Logic.strip_assums_hyp goal in |
|
319 |
(case fst (fold thins Hs (NONE, 0)) of |
|
320 |
NONE => no_tac |
|
321 |
| SOME tac => tac i) |
|
322 |
end) |
|
5974 | 323 |
end; |
324 |
||
0 | 325 |
end; |
1501 | 326 |
|
32971 | 327 |
structure Basic_Tactic: BASIC_TACTIC = Tactic; |
328 |
open Basic_Tactic; |