author  wenzelm 
Fri, 24 Jul 2015 22:20:22 +0200  
changeset 60776  2164e7b47454 
parent 60775  4592a9118d0b 
child 60793  bbcd4ab6d26e 
permissions  rwrr 
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 fallback 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 
23223  24 
val atac: int > tactic 
25 
val rtac: thm > int > tactic 

31251  26 
val dtac: thm > int > tactic 
27 
val etac: thm > int > tactic 

60774  28 
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

29 
val solve_tac: Proof.context > thm list > int > tactic 
58957  30 
val bimatch_tac: Proof.context > (bool * thm) list > int > tactic 
31 
val match_tac: Proof.context > thm list > int > tactic 

32 
val ematch_tac: Proof.context > thm list > int > tactic 

33 
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

34 
val flexflex_tac: Proof.context > tactic 
23223  35 
val distinct_subgoal_tac: int > tactic 
36 
val distinct_subgoals_tac: tactic 

46704  37 
val cut_tac: thm > int > tactic 
23223  38 
val cut_rules_tac: thm list > int > tactic 
39 
val cut_facts_tac: thm list > int > tactic 

40 
val filter_thms: (term * term > bool) > int * term * thm list > thm list 

59164  41 
val biresolution_from_nets_tac: Proof.context > 
42 
('a list > (bool * thm) list) > bool > 'a Net.net * 'a Net.net > int > tactic 

43 
val biresolve_from_nets_tac: Proof.context > 

44 
(int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > int > tactic 

45 
val bimatch_from_nets_tac: Proof.context > 

46 
(int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > int > tactic 

47 
val filt_resolve_from_net_tac: Proof.context > int > (int * thm) Net.net > int > tactic 

48 
val resolve_from_net_tac: Proof.context > (int * thm) Net.net > int > tactic 

49 
val match_from_net_tac: Proof.context > (int * thm) Net.net > int > tactic 

23223  50 
val subgoals_of_brl: bool * thm > int 
51 
val lessb: (bool * thm) * (bool * thm) > bool 

27243
d549b5b0f344
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
wenzelm
parents:
27209
diff
changeset

52 
val rename_tac: string list > int > tactic 
23223  53 
val rotate_tac: int > int > tactic 
54 
val defer_tac: int > tactic 

49865  55 
val prefer_tac: int > tactic 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

56 
val filter_prems_tac: Proof.context > (term > bool) > int > tactic 
11774  57 
end; 
0  58 

11774  59 
signature TACTIC = 
60 
sig 

61 
include BASIC_TACTIC 

23223  62 
val insert_tagged_brl: 'a * (bool * thm) > 
63 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net > 

64 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net 

65 
val delete_tagged_brl: bool * thm > 

66 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net > 

67 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net 

68 
val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) > bool 

32971  69 
val build_net: thm list > (int * thm) Net.net 
11774  70 
end; 
0  71 

11774  72 
structure Tactic: TACTIC = 
0  73 
struct 
74 

1501  75 
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 
10817  76 
fun trace_goalno_tac tac i st = 
4270  77 
case Seq.pull(tac i st) of 
15531  78 
NONE => Seq.empty 
12262  79 
 seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); 
10805  80 
Seq.make(fn()=> seqcell)); 
0  81 

82 
(*Makes a rule by applying a tactic to an existing rule*) 

36546  83 
fun rule_by_tactic ctxt tac rl = 
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

84 
let 
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51602
diff
changeset

85 
val thy = Proof_Context.theory_of ctxt; 
36546  86 
val ctxt' = Variable.declare_thm rl ctxt; 
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51602
diff
changeset

87 
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

88 
in 
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

89 
(case Seq.pull (tac st) of 
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

90 
NONE => raise THM ("rule_by_tactic", 0, [rl]) 
36546  91 
 SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st')) 
2688  92 
end; 
10817  93 

19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

94 

0  95 
(*** Basic tactics ***) 
96 

97 
(*** The following fail if the goal number is out of range: 

98 
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) 

99 

100 
(*Solve subgoal i by assumption*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

101 
fun assume_tac ctxt i = PRIMSEQ (Thm.assumption (SOME ctxt) i); 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

102 
fun atac i = PRIMSEQ (Thm.assumption NONE i); 
0  103 

104 
(*Solve subgoal i by assumption, using no unification*) 

31945  105 
fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i); 
0  106 

23223  107 

0  108 
(** Resolution/matching tactics **) 
109 

110 
(*The composition rule/state: no lifting or var renaming. 

31945  111 
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

112 
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

113 
PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} arg i); 
0  114 

115 
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule 

116 
like [ P&Q; P==>R ] ==> R *) 

117 
fun make_elim rl = zero_var_indexes (rl RS revcut_rl); 

118 

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

120 
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

121 
fun biresolve_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) false brules i); 
0  122 

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

124 
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

125 
fun resolve_tac ctxt rules = biresolve_tac ctxt (map (pair false) rules); 
0  126 

127 
(*Resolution with elimination rules only*) 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

128 
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

129 
fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules); 
0  130 

131 
(*Forward reasoning using destruction rules.*) 

60776  132 
fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' assume_tac ctxt; 
0  133 

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

135 
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

136 
fun dresolve_tac ctxt rls = eresolve_tac ctxt (map make_elim rls); 
0  137 

138 
(*Shorthand versions: for resolution with a single theorem*) 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

139 
fun rtac rl = resolve0_tac [rl]; 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

140 
fun dtac rl = dresolve0_tac [rl]; 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

141 
fun etac rl = eresolve0_tac [rl]; 
0  142 

60774  143 
(*Use an assumption or some rules*) 
144 
fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules; 

0  145 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

146 
fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt; 
5263  147 

0  148 
(*Matching tactics  as above, but forbid updating of state*) 
58957  149 
fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i); 
150 
fun match_tac ctxt rules = bimatch_tac ctxt (map (pair false) rules); 

151 
fun ematch_tac ctxt rules = bimatch_tac ctxt (map (pair true) rules); 

152 
fun dmatch_tac ctxt rls = ematch_tac ctxt (map make_elim rls); 

0  153 

154 
(*Smash all flexflex 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

155 
fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt)); 
0  156 

19056
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

157 
(*Remove duplicate subgoals.*) 
50081  158 
val permute_tac = PRIMITIVE oo Thm.permute_prems; 
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

159 
fun distinct_tac (i, k) = 
50081  160 
permute_tac 0 (i  1) THEN 
161 
permute_tac 1 (k  1) THEN 

51602
4c7fdc00bd59
tuned  Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
wenzelm
parents:
50239
diff
changeset

162 
PRIMITIVE (fn st => Drule.comp_no_flatten (st, 0) 1 Drule.distinct_prems_rl) THEN 
50081  163 
permute_tac 1 (1  k) THEN 
164 
permute_tac 0 (1  i); 

22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

165 

f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

166 
fun distinct_subgoal_tac i st = 
33957  167 
(case drop (i  1) (Thm.prems_of st) of 
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

168 
[] => no_tac st 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

169 
 A :: Bs => 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

170 
st > EVERY (fold (fn (B, k) => 
23223  171 
if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) [])); 
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

172 

10817  173 
fun distinct_subgoals_tac state = 
19056
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

174 
let 
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

175 
val goals = Thm.prems_of state; 
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

176 
val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals)); 
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

177 
in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state 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(limit1, 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 prebuilt 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 prebuilt 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 
(*Lessthan 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; 