author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18500  8b1a4e8ed199 
child 18977  f24c416a4814 
permissions  rwrr 
10805  1 
(* Title: Pure/tactic.ML 
0  2 
ID: $Id$ 
10805  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

10805  6 
Tactics. 
0  7 
*) 
8 

11774  9 
signature BASIC_TACTIC = 
10 
sig 

10805  11 
val ares_tac : thm list > int > tactic 
12 
val assume_tac : int > tactic 

13 
val atac : int >tactic 

10817  14 
val bimatch_from_nets_tac: 
1501  15 
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > int > tactic 
10805  16 
val bimatch_tac : (bool*thm)list > int > tactic 
10817  17 
val biresolution_from_nets_tac: 
10805  18 
('a list > (bool * thm) list) > 
19 
bool > 'a Net.net * 'a Net.net > int > tactic 

10817  20 
val biresolve_from_nets_tac: 
1501  21 
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > int > tactic 
10805  22 
val biresolve_tac : (bool*thm)list > int > tactic 
23 
val build_net : thm list > (int*thm) Net.net 

1501  24 
val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > 
25 
(bool*thm)list > (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net 

10817  26 
val compose_inst_tac : (string*string)list > (bool*thm*int) > 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

27 
int > tactic 
10817  28 
val compose_tac : (bool * thm * int) > int > tactic 
10805  29 
val cut_facts_tac : thm list > int > tactic 
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

30 
val cut_rules_tac : thm list > int > tactic 
10817  31 
val cut_inst_tac : (string*string)list > thm > int > tactic 
7491  32 
val datac : thm > int > int > tactic 
10805  33 
val defer_tac : int > tactic 
34 
val distinct_subgoals_tac : tactic 

35 
val dmatch_tac : thm list > int > tactic 

36 
val dresolve_tac : thm list > int > tactic 

10817  37 
val dres_inst_tac : (string*string)list > thm > int > tactic 
10805  38 
val dtac : thm > int >tactic 
7491  39 
val eatac : thm > int > int > tactic 
10805  40 
val etac : thm > int >tactic 
10817  41 
val eq_assume_tac : int > tactic 
10805  42 
val ematch_tac : thm list > int > tactic 
43 
val eresolve_tac : thm list > int > tactic 

44 
val eres_inst_tac : (string*string)list > thm > int > tactic 

7491  45 
val fatac : thm > int > int > tactic 
10817  46 
val filter_prems_tac : (term > bool) > int > tactic 
10805  47 
val filter_thms : (term*term>bool) > int*term*thm list > thm list 
48 
val filt_resolve_tac : thm list > int > int > tactic 

49 
val flexflex_tac : tactic 

50 
val fold_goals_tac : thm list > tactic 

51 
val fold_rule : thm list > thm > thm 

52 
val fold_tac : thm list > tactic 

10817  53 
val forward_tac : thm list > int > tactic 
10805  54 
val forw_inst_tac : (string*string)list > thm > int > tactic 
55 
val ftac : thm > int >tactic 

12320  56 
val insert_tagged_brl : ('a * (bool * thm)) * 
57 
(('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) > 

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

59 
val delete_tagged_brl : (bool * thm) * 

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

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

10805  62 
val is_fact : thm > bool 
63 
val lessb : (bool * thm) * (bool * thm) > bool 

64 
val lift_inst_rule : thm * int * (string*string)list * thm > thm 

65 
val make_elim : thm > thm 

66 
val match_from_net_tac : (int*thm) Net.net > int > tactic 

67 
val match_tac : thm list > int > tactic 

68 
val metacut_tac : thm > int > tactic 

69 
val net_bimatch_tac : (bool*thm) list > int > tactic 

70 
val net_biresolve_tac : (bool*thm) list > int > tactic 

71 
val net_match_tac : thm list > int > tactic 

72 
val net_resolve_tac : thm list > int > tactic 

73 
val norm_hhf_tac : int > tactic 

74 
val prune_params_tac : tactic 

75 
val rename_params_tac : string list > int > tactic 

76 
val rename_tac : string > int > tactic 

77 
val rename_last_tac : string > string list > int > tactic 

78 
val resolve_from_net_tac : (int*thm) Net.net > int > tactic 

79 
val resolve_tac : thm list > int > tactic 

10817  80 
val res_inst_tac : (string*string)list > thm > int > tactic 
10444  81 
val rewrite_goal_tac : thm list > int > tactic 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

82 
val rewrite_goals_rule: thm list > thm > thm 
10805  83 
val rewrite_rule : thm list > thm > thm 
84 
val rewrite_goals_tac : thm list > tactic 

85 
val rewrite_tac : thm list > tactic 

17968  86 
val asm_rewrite_goal_tac: bool * bool * bool > (simpset > tactic) > simpset > int > tactic 
10805  87 
val rewtac : thm > tactic 
88 
val rotate_tac : int > int > tactic 

89 
val rtac : thm > int > tactic 

90 
val rule_by_tactic : tactic > thm > thm 

91 
val solve_tac : thm list > int > tactic 

92 
val subgoal_tac : string > int > tactic 

93 
val subgoals_tac : string list > int > tactic 

94 
val subgoals_of_brl : bool * thm > int 

95 
val term_lift_inst_rule : 

15797  96 
thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm 
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

97 
> thm 
10347  98 
val instantiate_tac : (string * string) list > tactic 
10805  99 
val thin_tac : string > int > tactic 
100 
val trace_goalno_tac : (int > tactic) > int > tactic 

18500
8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

101 
val CONJUNCTS: tactic > int > tactic 
8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

102 
val PRECISE_CONJUNCTS: int > tactic > int > tactic 
11774  103 
end; 
0  104 

11774  105 
signature TACTIC = 
106 
sig 

107 
include BASIC_TACTIC 

11929  108 
val innermost_params: int > thm > (string * typ) list 
11774  109 
val untaglist: (int * 'a) list > 'a list 
16809  110 
val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) > bool 
11774  111 
val orderlist: (int * 'a) list > 'a list 
112 
val rewrite: bool > thm list > cterm > thm 

113 
val simplify: bool > thm list > thm > thm 

18471  114 
val conjunction_tac: int > tactic 
115 
val precise_conjunction_tac: int > int > tactic 

15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

116 
val compose_inst_tac' : (indexname * string) list > (bool * thm * int) > 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

117 
int > tactic 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

118 
val lift_inst_rule' : thm * int * (indexname * string) list * thm > thm 
15464
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset

119 
val eres_inst_tac' : (indexname * string) list > thm > int > tactic 
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

120 
val res_inst_tac' : (indexname * string) list > thm > int > tactic 
15797  121 
val instantiate_tac' : (indexname * string) list > tactic 
11774  122 
end; 
0  123 

11774  124 
structure Tactic: TACTIC = 
0  125 
struct 
126 

1501  127 
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 
10817  128 
fun trace_goalno_tac tac i st = 
4270  129 
case Seq.pull(tac i st) of 
15531  130 
NONE => Seq.empty 
12262  131 
 seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); 
10805  132 
Seq.make(fn()=> seqcell)); 
0  133 

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

1501  135 
fun rule_by_tactic tac rl = 
2688  136 
let val (st, thaw) = freeze_thaw (zero_var_indexes rl) 
4270  137 
in case Seq.pull (tac st) of 
15531  138 
NONE => raise THM("rule_by_tactic", 0, [rl]) 
139 
 SOME(st',_) => Thm.varifyT (thaw st') 

2688  140 
end; 
10817  141 

0  142 
(*** Basic tactics ***) 
143 

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

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

146 

147 
(*Solve subgoal i by assumption*) 

148 
fun assume_tac i = PRIMSEQ (assumption i); 

149 

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

151 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

152 

153 
(** Resolution/matching tactics **) 

154 

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

156 
The arg = (bires_flg, orule, m) ; see bicompose for explanation.*) 

157 
fun compose_tac arg i = PRIMSEQ (bicompose false arg i); 

158 

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

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

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

162 

163 
(*Attack subgoal i by resolution, using flags to indicate elimination rules*) 

164 
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i); 

165 

166 
(*Resolution: the simple case, works for introduction rules*) 

167 
fun resolve_tac rules = biresolve_tac (map (pair false) rules); 

168 

169 
(*Resolution with elimination rules only*) 

170 
fun eresolve_tac rules = biresolve_tac (map (pair true) rules); 

171 

172 
(*Forward reasoning using destruction rules.*) 

173 
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac; 

174 

175 
(*Like forward_tac, but deletes the assumption after use.*) 

176 
fun dresolve_tac rls = eresolve_tac (map make_elim rls); 

177 

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

7491  179 
val atac = assume_tac; 
180 
fun rtac rl = resolve_tac [rl]; 

181 
fun dtac rl = dresolve_tac [rl]; 

1460  182 
fun etac rl = eresolve_tac [rl]; 
7491  183 
fun ftac rl = forward_tac [rl]; 
184 
fun datac thm j = EVERY' (dtac thm::replicate j atac); 

185 
fun eatac thm j = EVERY' (etac thm::replicate j atac); 

186 
fun fatac thm j = EVERY' (ftac thm::replicate j atac); 

0  187 

188 
(*Use an assumption or some rules ... A popular combination!*) 

189 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

190 

5263  191 
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac; 
192 

0  193 
(*Matching tactics  as above, but forbid updating of state*) 
194 
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i); 

195 
fun match_tac rules = bimatch_tac (map (pair false) rules); 

196 
fun ematch_tac rules = bimatch_tac (map (pair true) rules); 

197 
fun dmatch_tac rls = ematch_tac (map make_elim rls); 

198 

199 
(*Smash all flexflex disagreement pairs in the proof state.*) 

200 
val flexflex_tac = PRIMSEQ flexflex_rule; 

201 

3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

202 

c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

203 
(*Remove duplicate subgoals. By Mark Staples*) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

204 
local 
16666  205 
fun cterm_aconv (a,b) = term_of a aconv term_of b; 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

206 
in 
10817  207 
fun distinct_subgoals_tac state = 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

208 
let val (frozth,thawfn) = freeze_thaw state 
10805  209 
val froz_prems = cprems_of frozth 
210 
val assumed = implies_elim_list frozth (map assume froz_prems) 

211 
val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) 

212 
assumed; 

15977  213 
in (*Applying Thm.varifyT to the result of thawfn would (re)generalize 
214 
all type variables that appear in the subgoals. Unfortunately, it 

215 
would also break the function AxClass.intro_classes_tac, even in the 

216 
trivial case where the type class has no axioms.*) 

217 
Seq.single (thawfn implied) 

218 
end 

10817  219 
end; 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

220 

c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

221 

11929  222 
(*Determine print names of goal parameters (reversed)*) 
223 
fun innermost_params i st = 

224 
let val (_, _, Bi, _) = dest_state (st, i) 

225 
in rename_wrt_term Bi (Logic.strip_params Bi) end; 

226 

15453  227 
(*params of subgoal i as they are printed*) 
228 
fun params_of_state st i = 

229 
let val (_, _, Bi, _) = dest_state(st,i) 

230 
val params = Logic.strip_params Bi 

231 
in rev(rename_wrt_term Bi params) end; 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

232 

15453  233 
(*read instantiations with respect to subgoal i of proof state st*) 
234 
fun read_insts_in_state (st, i, sinsts, rule) = 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

235 
let val thy = Thm.theory_of_thm st 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

236 
and params = params_of_state st i 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

237 
and rts = types_sorts rule and (types,sorts) = types_sorts st 
17271  238 
fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1)  sm => sm) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

239 
 types' ixn = types ixn; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

240 
val used = Drule.add_used rule (Drule.add_used st []); 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

241 
in read_insts thy rts (types',sorts) used sinsts end; 
15453  242 

0  243 
(*Lift and instantiate a rule wrt the given state and subgoal number *) 
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

244 
fun lift_inst_rule' (st, i, sinsts, rule) = 
15453  245 
let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) 
246 
and {maxidx,...} = rep_thm st 

247 
and params = params_of_state st i 

0  248 
val paramTs = map #2 params 
249 
and inc = maxidx+1 

16876  250 
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs> Logic.incr_tvar inc T) 
0  251 
 liftvar t = raise TERM("Variable expected", [t]); 
10817  252 
fun liftterm t = list_abs_free (params, 
10805  253 
Logic.incr_indexes(paramTs,inc) t) 
0  254 
(*Lifts instantiation pair over params*) 
230  255 
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) 
16876  256 
val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc)) 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
7596
diff
changeset

257 
in Drule.instantiate (map lifttvar Tinsts, map liftpair insts) 
18145  258 
(Thm.lift_rule (Thm.cprem_of st i) rule) 
0  259 
end; 
260 

15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

261 
fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule' 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

262 
(st, i, map (apfst Syntax.indexname) sinsts, rule); 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

263 

3984  264 
(* 
265 
Like lift_inst_rule but takes terms, not strings, where the terms may contain 

266 
Bounds referring to parameters of the subgoal. 

267 

268 
insts: [...,(vj,tj),...] 

269 

270 
The tj may contain references to parameters of subgoal i of the state st 

271 
in the form of Bound k, i.e. the tj may be subterms of the subgoal. 

272 
To saturate the lose bound vars, the tj are enclosed in abstractions 

273 
corresponding to the parameters of subgoal i, thus turning them into 

274 
functions. At the same time, the types of the vj are lifted. 

275 

276 
NB: the types in insts must be correctly instantiated already, 

277 
i.e. Tinsts is not applied to insts. 

278 
*) 

1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

279 
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

280 
let val {maxidx,thy,...} = rep_thm st 
15453  281 
val paramTs = map #2 (params_of_state st i) 
1966  282 
and inc = maxidx+1 
16876  283 
fun liftvar ((a,j), T) = Var((a, j+inc), paramTs> Logic.incr_tvar inc T) 
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

284 
(*lift only Var, not term, which must be lifted already*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

285 
fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t) 
15797  286 
fun liftTpair (((a, i), S), T) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

287 
(ctyp_of thy (TVar ((a, i + inc), S)), 
16876  288 
ctyp_of thy (Logic.incr_tvar inc T)) 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
7596
diff
changeset

289 
in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) 
18145  290 
(Thm.lift_rule (Thm.cprem_of st i) rule) 
1966  291 
end; 
0  292 

293 
(*** Resolve after lifting and instantation; may refer to parameters of the 

294 
subgoal. Fails if "i" is out of range. ***) 

295 

296 
(*compose version: arguments are as for bicompose.*) 

15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

297 
fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st = 
8977
dd8bc754a072
res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents:
8129
diff
changeset

298 
if i > nprems_of st then no_tac st 
dd8bc754a072
res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents:
8129
diff
changeset

299 
else st > 
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

300 
(compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i 
12262  301 
handle TERM (msg,_) => (warning msg; no_tac) 
302 
 THM (msg,_,_) => (warning msg; no_tac)); 

0  303 

15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

304 
val compose_inst_tac = gen_compose_inst_tac lift_inst_rule; 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

305 
val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule'; 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

306 

761  307 
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the 
308 
terms that are substituted contain (term or type) unknowns from the 

309 
goal, because it is unable to instantiate goal unknowns at the same time. 

310 

2029  311 
The type checker is instructed not to freeze flexible type vars that 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

312 
were introduced during type inference and still remain in the term at the 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

313 
end. This increases flexibility but can introduce schematic type vars in 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

314 
goals. 
761  315 
*) 
0  316 
fun res_inst_tac sinsts rule i = 
317 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

318 

15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

319 
fun res_inst_tac' sinsts rule i = 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

320 
compose_inst_tac' sinsts (false, rule, nprems_of rule) i; 
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

321 

1501  322 
(*eresolve elimination version*) 
0  323 
fun eres_inst_tac sinsts rule i = 
324 
compose_inst_tac sinsts (true, rule, nprems_of rule) i; 

325 

15464
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset

326 
fun eres_inst_tac' sinsts rule i = 
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset

327 
compose_inst_tac' sinsts (true, rule, nprems_of rule) i; 
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset

328 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

329 
(*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

330 
increment revcut_rl instead.*) 
10817  331 
fun make_elim_preserve rl = 
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

332 
let val {maxidx,...} = rep_thm rl 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

333 
fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT)); 
10817  334 
val revcut_rl' = 
10805  335 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
336 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 

0  337 
val arg = (false, rl, nprems_of rl) 
4270  338 
val [th] = Seq.list_of (bicompose false arg 1 revcut_rl') 
0  339 
in th end 
340 
handle Bind => raise THM("make_elim_preserve", 1, [rl]); 

341 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

342 
(*instantiate and cut  for a FACT, anyway...*) 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

343 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  344 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

345 
(*forward tactic applies a RULE to an assumption without deleting it*) 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

346 
fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac; 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

347 

d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

348 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  349 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
350 

10347  351 
(*instantiate variables in the whole state*) 
352 
val instantiate_tac = PRIMITIVE o read_instantiate; 

353 

15797  354 
val instantiate_tac' = PRIMITIVE o Drule.read_instantiate'; 
355 

1951  356 
(*Deletion of an assumption*) 
357 
fun thin_tac s = eres_inst_tac [("V",s)] thin_rl; 

358 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

359 
(*** Applications of cut_rl ***) 
0  360 

361 
(*Used by metacut_tac*) 

362 
fun bires_cut_tac arg i = 

1460  363 
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; 
0  364 

365 
(*The conclusion of the rule gets assumed in subgoal i, 

366 
while subgoal i+1,... are the premises of the rule.*) 

367 
fun metacut_tac rule = bires_cut_tac [(false,rule)]; 

368 

369 
(*Recognizes theorems that are not rules, but simple propositions*) 

370 
fun is_fact rl = 

371 
case prems_of rl of 

10805  372 
[] => true  _::_ => false; 
0  373 

13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

374 
(*"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

375 
subgoals.*) 
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

376 
fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths); 
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

377 

31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

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

379 
generates no additional subgoals. *) 
15570  380 
fun cut_facts_tac ths = cut_rules_tac (List.filter is_fact ths); 
0  381 

382 
(*Introduce the given proposition as a lemma and subgoal*) 

12847
afa356dbcb15
fixed subgoal_tac; fails on nonexistent subgoal;
wenzelm
parents:
12801
diff
changeset

383 
fun subgoal_tac sprop = 
afa356dbcb15
fixed subgoal_tac; fails on nonexistent subgoal;
wenzelm
parents:
12801
diff
changeset

384 
DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) => 
afa356dbcb15
fixed subgoal_tac; fails on nonexistent subgoal;
wenzelm
parents:
12801
diff
changeset

385 
let val concl' = Logic.strip_assums_concl prop in 
4178
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset

386 
if null (term_tvars concl') then () 
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset

387 
else warning"Type variables in new subgoal: add a type constraint?"; 
12847
afa356dbcb15
fixed subgoal_tac; fails on nonexistent subgoal;
wenzelm
parents:
12801
diff
changeset

388 
all_tac 
afa356dbcb15
fixed subgoal_tac; fails on nonexistent subgoal;
wenzelm
parents:
12801
diff
changeset

389 
end); 
0  390 

439  391 
(*Introduce a list of lemmas and subgoals*) 
392 
fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); 

393 

0  394 

395 
(**** Indexing and filtering of theorems ****) 

396 

397 
(*Returns the list of potentially resolvable theorems for the goal "prem", 

10805  398 
using the predicate could(subgoal,concl). 
0  399 
Resulting list is no longer than "limit"*) 
400 
fun filter_thms could (limit, prem, ths) = 

401 
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*) 

402 
fun filtr (limit, []) = [] 

10805  403 
 filtr (limit, th::ths) = 
404 
if limit=0 then [] 

405 
else if could(pb, concl_of th) then th :: filtr(limit1, ths) 

406 
else filtr(limit,ths) 

0  407 
in filtr(limit,ths) end; 
408 

409 

410 
(*** biresolution and resolution using nets ***) 

411 

412 
(** To preserve the order of the rules, tag them with increasing integers **) 

413 

414 
(*insert tags*) 

415 
fun taglist k [] = [] 

416 
 taglist k (x::xs) = (k,x) :: taglist (k+1) xs; 

417 

418 
(*remove tags and suppress duplicates  list is assumed sorted!*) 

419 
fun untaglist [] = [] 

420 
 untaglist [(k:int,x)] = [x] 

421 
 untaglist ((k,x) :: (rest as (k',x')::_)) = 

422 
if k=k' then untaglist rest 

423 
else x :: untaglist rest; 

424 

425 
(*return list elements in original order*) 

10817  426 
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); 
0  427 

428 
(*insert one tagged brl into the pair of nets*) 

12320  429 
fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) = 
430 
if eres then 

431 
(case try Thm.major_prem_of th of 

16809  432 
SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet) 
15531  433 
 NONE => error "insert_tagged_brl: elimination rule with no premises") 
16809  434 
else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet); 
0  435 

436 
(*build a pair of nets for biresolution*) 

10817  437 
fun build_netpair netpair brls = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

438 
foldr insert_tagged_brl netpair (taglist 1 brls); 
0  439 

12320  440 
(*delete one kbrl from the pair of nets*) 
16809  441 
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th') 
442 

12320  443 
fun delete_tagged_brl (brl as (eres, th), (inet, enet)) = 
13925  444 
(if eres then 
12320  445 
(case try Thm.major_prem_of th of 
16809  446 
SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet) 
15531  447 
 NONE => (inet, enet)) (*no major premise: ignore*) 
16809  448 
else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet)) 
13925  449 
handle Net.DELETE => (inet,enet); 
1801  450 

451 

10817  452 
(*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

453 
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

454 
boolean "match" indicates matching or unification.*) 
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

455 
fun biresolution_from_nets_tac order match (inet,enet) = 
0  456 
SUBGOAL 
457 
(fn (prem,i) => 

458 
let val hyps = Logic.strip_assums_hyp prem 

10817  459 
and concl = Logic.strip_assums_concl prem 
0  460 
val kbrls = Net.unify_term inet concl @ 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset

461 
List.concat (map (Net.unify_term enet) hyps) 
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

462 
in PRIMSEQ (biresolution match (order kbrls) i) end); 
0  463 

3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

464 
(*versions taking prebuilt nets. No filtering of brls*) 
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

465 
val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false; 
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

466 
val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist true; 
0  467 

468 
(*fast versions using nets internally*) 

670  469 
val net_biresolve_tac = 
470 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

471 

472 
val net_bimatch_tac = 

473 
bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty); 

0  474 

475 
(*** Simpler version for resolve_tac  only one net, and no hyps ***) 

476 

477 
(*insert one tagged rl into the net*) 

478 
fun insert_krl (krl as (k,th), net) = 

16809  479 
Net.insert_term (K false) (concl_of th, krl) net; 
0  480 

481 
(*build a net of rules for resolution*) 

10817  482 
fun build_net rls = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

483 
foldr insert_krl Net.empty (taglist 1 rls); 
0  484 

485 
(*resolution using a net rather than rules; pred supports filt_resolve_tac*) 

486 
fun filt_resolution_from_net_tac match pred net = 

487 
SUBGOAL 

488 
(fn (prem,i) => 

489 
let val krls = Net.unify_term net (Logic.strip_assums_concl prem) 

10817  490 
in 
491 
if pred krls 

0  492 
then PRIMSEQ 
10805  493 
(biresolution match (map (pair false) (orderlist krls)) i) 
0  494 
else no_tac 
495 
end); 

496 

497 
(*Resolve the subgoal using the rules (making a net) unless too flexible, 

498 
which means more than maxr rules are unifiable. *) 

10817  499 
fun filt_resolve_tac rules maxr = 
0  500 
let fun pred krls = length krls <= maxr 
501 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

502 

503 
(*versions taking prebuilt nets*) 

504 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

505 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

506 

507 
(*fast versions using nets internally*) 

508 
val net_resolve_tac = resolve_from_net_tac o build_net; 

509 
val net_match_tac = match_from_net_tac o build_net; 

510 

511 

512 
(*** For Natural Deduction using (bires_flg, rule) pairs ***) 

513 

514 
(*The number of new subgoals produced by the brule*) 

1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

515 
fun subgoals_of_brl (true,rule) = nprems_of rule  1 
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

516 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  517 

518 
(*Lessthan test: for sorting to minimize number of new subgoals*) 

519 
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; 

520 

521 

522 
(*** MetaRewriting Tactics ***) 

523 

3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

524 
val simple_prover = 
15021  525 
SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss))); 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

526 

11768
48bc55f43774
unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents:
11762
diff
changeset

527 
val rewrite = MetaSimplifier.rewrite_aux simple_prover; 
48bc55f43774
unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents:
11762
diff
changeset

528 
val simplify = MetaSimplifier.simplify_aux simple_prover; 
48bc55f43774
unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents:
11762
diff
changeset

529 
val rewrite_rule = simplify true; 
10415
e6d7b77a0574
moved rewriting functions from Drule to MetaSimplifier
berghofe
parents:
10347
diff
changeset

530 
val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover; 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

531 

17968  532 
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) 
533 
fun asm_rewrite_goal_tac mode prover_tac ss = 

534 
SELECT_GOAL 

535 
(PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1)); 

536 

10444  537 
fun rewrite_goal_tac rews = 
17892  538 
let val ss = MetaSimplifier.empty_ss addsimps rews in 
17968  539 
fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac) 
17892  540 
(MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st 
541 
end; 

10444  542 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

543 
(*Rewrite throughout proof state. *) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

544 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  545 

546 
(*Rewrite subgoals only, not main goal. *) 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

547 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
1460  548 
fun rewtac def = rewrite_goals_tac [def]; 
0  549 

12782  550 
val norm_hhf_tac = 
551 
rtac Drule.asm_rl (*cheap approximation  thanks to builtin Logic.flatten_params*) 

552 
THEN' SUBGOAL (fn (t, i) => 

12801  553 
if Drule.is_norm_hhf t then all_tac 
12782  554 
else rewrite_goal_tac [Drule.norm_hhf_eq] i); 
10805  555 

0  556 

1501  557 
(*** for folding definitions, handling critical pairs ***) 
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

558 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

559 
(*The depth of nesting in a term*) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

560 
fun term_depth (Abs(a,T,t)) = 1 + term_depth t 
2145  561 
 term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t) 
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

562 
 term_depth _ = 0; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

563 

12801  564 
val lhs_of_thm = #1 o Logic.dest_equals o prop_of; 
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

565 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

566 
(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

567 
Returns longest lhs first to avoid folding its subexpressions.*) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

568 
fun sort_lhs_depths defs = 
17496  569 
let val keylist = AList.make (term_depth o lhs_of_thm) defs 
4438  570 
val keys = distinct (sort (rev_order o int_ord) (map #2 keylist)) 
17496  571 
in map (AList.find (op =) keylist) keys end; 
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

572 

7596  573 
val rev_defs = sort_lhs_depths o map symmetric; 
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

574 

15570  575 
fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs); 
7596  576 
fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs)); 
577 
fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs)); 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

578 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

579 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

580 
(*** Renaming of parameters in a subgoal 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

581 
Names may contain letters, digits or primes and must be 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

582 
separated by blanks ***) 
0  583 

9535  584 
fun rename_params_tac xs i = 
14673  585 
case Library.find_first (not o Syntax.is_identifier) xs of 
15531  586 
SOME x => error ("Not an identifier: " ^ x) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

587 
 NONE => 
13559
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
13105
diff
changeset

588 
(if !Logic.auto_rename 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

589 
then (warning "Resetting Logic.auto_rename"; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

590 
Logic.auto_rename := false) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

591 
else (); PRIMITIVE (rename_params_rule (xs, i))); 
9535  592 

10817  593 
fun rename_tac str i = 
594 
let val cs = Symbol.explode str in 

4693  595 
case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of 
9535  596 
[] => rename_params_tac (scanwords Symbol.is_letdig cs) i 
0  597 
 c::_ => error ("Illegal character: " ^ c) 
598 
end; 

599 

1501  600 
(*Rename recent parameters using names generated from a and the suffixes, 
601 
provided the string a, which represents a term, is an identifier. *) 

10817  602 
fun rename_last_tac a sufs i = 
0  603 
let val names = map (curry op^ a) sufs 
604 
in if Syntax.is_identifier a 

605 
then PRIMITIVE (rename_params_rule (names,i)) 

606 
else all_tac 

607 
end; 

608 

2043  609 
(*Prunes all redundant parameters from the proof state by rewriting. 
610 
DOES NOT rewrite main goal, where quantification over an unused bound 

611 
variable is sometimes done to avoid the need for cut_facts_tac.*) 

612 
val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; 

0  613 

1501  614 
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from 
615 
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

616 
fun rotate_tac 0 i = all_tac 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset

617 
 rotate_tac k i = PRIMITIVE (rotate_rule k i); 
1209  618 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset

619 
(*Rotates the given subgoal to be the last.*) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset

620 
fun defer_tac i = PRIMITIVE (permute_prems (i1) 1); 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset

621 

5974  622 
(* remove premises that do not satisfy p; fails if all prems satisfy p *) 
623 
fun filter_prems_tac p = 

15531  624 
let fun Then NONE tac = SOME tac 
625 
 Then (SOME tac) tac' = SOME(tac THEN' tac'); 

5974  626 
fun thins ((tac,n),H) = 
627 
if p H then (tac,n+1) 

628 
else (Then tac (rotate_tac n THEN' etac thin_rl),0); 

629 
in SUBGOAL(fn (subg,n) => 

630 
let val Hs = Logic.strip_assums_hyp subg 

15570  631 
in case fst(Library.foldl thins ((NONE,0),Hs)) of 
15531  632 
NONE => no_tac  SOME tac => tac n 
5974  633 
end) 
634 
end; 

635 

11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset

636 

18471  637 
(* metalevel conjunction *) 
638 

639 
val conj_tac = SUBGOAL (fn (goal, i) => 

640 
if can Logic.dest_conjunction goal then 

641 
(fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st) 

642 
else no_tac); 

643 

644 
val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac; 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

645 

18471  646 
val precise_conjunction_tac = 
647 
let 

648 
fun tac 0 i = eq_assume_tac i 

649 
 tac 1 i = SUBGOAL (K all_tac) i 

650 
 tac n i = conj_tac i THEN TRY (fn st => tac (n  1) (i + 1) st); 

651 
in TRY oo tac end; 

12139  652 

18500
8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

653 
fun CONJUNCTS tac = 
8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

654 
SELECT_GOAL (conjunction_tac 1 
8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

655 
THEN tac 
8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

656 
THEN PRIMITIVE Drule.conj_curry); 
8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

657 

8b1a4e8ed199
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents:
18471
diff
changeset

658 
fun PRECISE_CONJUNCTS n tac = 
18471  659 
SELECT_GOAL (precise_conjunction_tac n 1 
18209
6bcd9b2ca49b
added CONJUNCTS: treat conjunction as separate subgoals;
wenzelm
parents:
18145
diff
changeset

660 
THEN tac 
6bcd9b2ca49b
added CONJUNCTS: treat conjunction as separate subgoals;
wenzelm
parents:
18145
diff
changeset

661 
THEN PRIMITIVE Drule.conj_curry); 
6bcd9b2ca49b
added CONJUNCTS: treat conjunction as separate subgoals;
wenzelm
parents:
18145
diff
changeset

662 

0  663 
end; 
1501  664 

11774  665 
structure BasicTactic: BASIC_TACTIC = Tactic; 
666 
open BasicTactic; 