author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24244  d7ee11ba1534 
child 25939  ddea202704b4 
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 

23223  11 
val trace_goalno_tac: (int > tactic) > int > tactic 
12 
val rule_by_tactic: tactic > thm > thm 

13 
val assume_tac: int > tactic 

14 
val eq_assume_tac: int > tactic 

15 
val compose_tac: (bool * thm * int) > int > tactic 

16 
val make_elim: thm > thm 

17 
val biresolve_tac: (bool * thm) list > int > tactic 

18 
val resolve_tac: thm list > int > tactic 

19 
val eresolve_tac: thm list > int > tactic 

20 
val forward_tac: thm list > int > tactic 

21 
val dresolve_tac: thm list > int > tactic 

22 
val atac: int > tactic 

23 
val rtac: thm > int > tactic 

24 
val dtac: thm > int >tactic 

25 
val etac: thm > int >tactic 

26 
val ftac: thm > int >tactic 

27 
val datac: thm > int > int > tactic 

28 
val eatac: thm > int > int > tactic 

29 
val fatac: thm > int > int > tactic 

30 
val ares_tac: thm list > int > tactic 

31 
val solve_tac: thm list > int > tactic 

32 
val bimatch_tac: (bool * thm) list > int > tactic 

33 
val match_tac: thm list > int > tactic 

34 
val ematch_tac: thm list > int > tactic 

35 
val dmatch_tac: thm list > int > tactic 

36 
val flexflex_tac: tactic 

37 
val distinct_subgoal_tac: int > tactic 

38 
val distinct_subgoals_tac: tactic 

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

40 
val term_lift_inst_rule: 

41 
thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm > thm 

42 
val compose_inst_tac: (string * string) list > (bool * thm * int) > int > tactic 

43 
val res_inst_tac: (string * string) list > thm > int > tactic 

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

45 
val cut_inst_tac: (string * string) list > thm > int > tactic 

46 
val forw_inst_tac: (string * string) list > thm > int > tactic 

47 
val dres_inst_tac: (string * string) list > thm > int > tactic 

48 
val instantiate_tac: (string * string) list > tactic 

49 
val thin_tac: string > int > tactic 

50 
val metacut_tac: thm > int > tactic 

51 
val cut_rules_tac: thm list > int > tactic 

52 
val cut_facts_tac: thm list > int > tactic 

53 
val subgoal_tac: string > int > tactic 

54 
val subgoals_tac: string list > int > tactic 

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

56 
val biresolution_from_nets_tac: ('a list > (bool * thm) list) > 

57 
bool > 'a Net.net * 'a Net.net > int > tactic 

58 
val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > 

59 
int > tactic 

60 
val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > 

61 
int > tactic 

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

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

64 
val build_net: thm list > (int * thm) Net.net 

65 
val filt_resolve_tac: thm list > int > int > tactic 

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

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

68 
val net_resolve_tac: thm list > int > tactic 

69 
val net_match_tac: thm list > int > tactic 

70 
val subgoals_of_brl: bool * thm > int 

71 
val lessb: (bool * thm) * (bool * thm) > bool 

72 
val rename_params_tac: string list > int > tactic 

73 
val rename_tac: string > int > tactic 

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

75 
val rotate_tac: int > int > tactic 

76 
val defer_tac: int > tactic 

77 
val filter_prems_tac: (term > bool) > int > tactic 

11774  78 
end; 
0  79 

11774  80 
signature TACTIC = 
81 
sig 

82 
include BASIC_TACTIC 

11929  83 
val innermost_params: int > thm > (string * typ) list 
23223  84 
val lift_inst_rule': thm * int * (indexname * string) list * thm > thm 
85 
val compose_inst_tac': (indexname * string) list > (bool * thm * int) > int > tactic 

86 
val res_inst_tac': (indexname * string) list > thm > int > tactic 

87 
val eres_inst_tac': (indexname * string) list > thm > int > tactic 

88 
val make_elim_preserve: thm > thm 

89 
val instantiate_tac': (indexname * string) list > tactic 

11774  90 
val untaglist: (int * 'a) list > 'a list 
91 
val orderlist: (int * 'a) list > 'a list 

23223  92 
val insert_tagged_brl: 'a * (bool * thm) > 
93 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net > 

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

95 
val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > 

96 
(bool * thm) list > (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net 

97 
val delete_tagged_brl: bool * thm > 

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

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

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

11774  101 
end; 
0  102 

11774  103 
structure Tactic: TACTIC = 
0  104 
struct 
105 

1501  106 
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 
10817  107 
fun trace_goalno_tac tac i st = 
4270  108 
case Seq.pull(tac i st) of 
15531  109 
NONE => Seq.empty 
12262  110 
 seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); 
10805  111 
Seq.make(fn()=> seqcell)); 
0  112 

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

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

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

116 
val ctxt = Variable.thm_context rl; 
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
22560
diff
changeset

117 
val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt; 
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

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

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

120 
NONE => raise THM ("rule_by_tactic", 0, [rl]) 
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

121 
 SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st')) 
2688  122 
end; 
10817  123 

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

124 

0  125 
(*** Basic tactics ***) 
126 

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

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

129 

130 
(*Solve subgoal i by assumption*) 

131 
fun assume_tac i = PRIMSEQ (assumption i); 

132 

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

134 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

135 

23223  136 

0  137 
(** Resolution/matching tactics **) 
138 

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

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

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

142 

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

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

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

146 

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

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

149 

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

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

152 

153 
(*Resolution with elimination rules only*) 

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

155 

156 
(*Forward reasoning using destruction rules.*) 

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

158 

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

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

161 

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

7491  163 
val atac = assume_tac; 
164 
fun rtac rl = resolve_tac [rl]; 

165 
fun dtac rl = dresolve_tac [rl]; 

1460  166 
fun etac rl = eresolve_tac [rl]; 
7491  167 
fun ftac rl = forward_tac [rl]; 
168 
fun datac thm j = EVERY' (dtac thm::replicate j atac); 

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

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

0  171 

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

173 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

174 

5263  175 
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac; 
176 

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

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

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

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

182 

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

184 
val flexflex_tac = PRIMSEQ flexflex_rule; 

185 

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

186 
(*Remove duplicate subgoals.*) 
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

187 
val perm_tac = PRIMITIVE oo Thm.permute_prems; 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

188 

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

189 
fun distinct_tac (i, k) = 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

190 
perm_tac 0 (i  1) THEN 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

191 
perm_tac 1 (k  1) THEN 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

192 
DETERM (PRIMSEQ (fn st => 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

193 
Thm.compose_no_flatten false (st, 0) 1 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

194 
(Drule.incr_indexes st Drule.distinct_prems_rl))) THEN 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

195 
perm_tac 1 (1  k) THEN 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

196 
perm_tac 0 (1  i); 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

197 

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

198 
fun distinct_subgoal_tac i st = 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

199 
(case Library.drop (i  1, Thm.prems_of st) of 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

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

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

202 
st > EVERY (fold (fn (B, k) => 
23223  203 
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

204 

10817  205 
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

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

207 
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

208 
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

209 
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

210 

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

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

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

215 

15453  216 
(*params of subgoal i as they are printed*) 
19532  217 
fun params_of_state i st = rev (innermost_params i st); 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

218 

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

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

221 
let val thy = Thm.theory_of_thm st 
19532  222 
and params = params_of_state i st 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16325
diff
changeset

223 
and rts = types_sorts rule and (types,sorts) = types_sorts st 
17271  224 
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

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

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

227 
in read_insts thy rts (types',sorts) used sinsts end; 
15453  228 

0  229 
(*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

230 
fun lift_inst_rule' (st, i, sinsts, rule) = 
15453  231 
let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) 
232 
and {maxidx,...} = rep_thm st 

19532  233 
and params = params_of_state i st 
0  234 
val paramTs = map #2 params 
235 
and inc = maxidx+1 

16876  236 
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs> Logic.incr_tvar inc T) 
0  237 
 liftvar t = raise TERM("Variable expected", [t]); 
10817  238 
fun liftterm t = list_abs_free (params, 
10805  239 
Logic.incr_indexes(paramTs,inc) t) 
0  240 
(*Lifts instantiation pair over params*) 
230  241 
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) 
16876  242 
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

243 
in Drule.instantiate (map lifttvar Tinsts, map liftpair insts) 
18145  244 
(Thm.lift_rule (Thm.cprem_of st i) rule) 
0  245 
end; 
246 

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

247 
fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule' 
24244  248 
(st, i, map (apfst Lexicon.read_indexname) sinsts, rule); 
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset

249 

3984  250 
(* 
251 
Like lift_inst_rule but takes terms, not strings, where the terms may contain 

252 
Bounds referring to parameters of the subgoal. 

253 

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

255 

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

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

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

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

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

261 

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

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

264 
*) 

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

265 
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

266 
let val {maxidx,thy,...} = rep_thm st 
19532  267 
val paramTs = map #2 (params_of_state i st) 
1966  268 
and inc = maxidx+1 
16876  269 
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

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

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

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

275 
in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) 
18145  276 
(Thm.lift_rule (Thm.cprem_of st i) rule) 
1966  277 
end; 
0  278 

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

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

281 

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

283 
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

284 
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

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

286 
(compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i 
12262  287 
handle TERM (msg,_) => (warning msg; no_tac) 
288 
 THM (msg,_,_) => (warning msg; no_tac)); 

0  289 

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

290 
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

291 
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

292 

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

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

296 

2029  297 
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

298 
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

299 
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

300 
goals. 
761  301 
*) 
0  302 
fun res_inst_tac sinsts rule i = 
303 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

304 

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

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

306 
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

307 

1501  308 
(*eresolve elimination version*) 
0  309 
fun eres_inst_tac sinsts rule i = 
310 
compose_inst_tac sinsts (true, rule, nprems_of rule) i; 

311 

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

312 
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

313 
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

314 

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

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

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

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

319 
fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT)); 
10817  320 
val revcut_rl' = 
10805  321 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
322 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 

0  323 
val arg = (false, rl, nprems_of rl) 
4270  324 
val [th] = Seq.list_of (bicompose false arg 1 revcut_rl') 
0  325 
in th end 
326 
handle Bind => raise THM("make_elim_preserve", 1, [rl]); 

327 

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

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

329 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  330 

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

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

332 
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

333 

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

334 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  335 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
336 

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

339 

15797  340 
val instantiate_tac' = PRIMITIVE o Drule.read_instantiate'; 
341 

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

344 

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

345 
(*** Applications of cut_rl ***) 
0  346 

347 
(*Used by metacut_tac*) 

348 
fun bires_cut_tac arg i = 

1460  349 
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; 
0  350 

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

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

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

354 

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

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

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

357 
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

358 

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

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

360 
generates no additional subgoals. *) 
20232  361 
fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths); 
0  362 

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

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

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

365 
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

366 
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

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

368 
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

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

370 
end); 
0  371 

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

374 

0  375 

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

377 

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

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

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

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

10805  384 
 filtr (limit, th::ths) = 
385 
if limit=0 then [] 

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

387 
else filtr(limit,ths) 

0  388 
in filtr(limit,ths) end; 
389 

390 

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

392 

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

394 

395 
(*insert tags*) 

396 
fun taglist k [] = [] 

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

398 

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

400 
fun untaglist [] = [] 

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

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

403 
if k=k' then untaglist rest 

404 
else x :: untaglist rest; 

405 

406 
(*return list elements in original order*) 

10817  407 
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); 
0  408 

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

23178  410 
fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) = 
12320  411 
if eres then 
412 
(case try Thm.major_prem_of th of 

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

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

10817  418 
fun build_netpair netpair brls = 
23178  419 
fold_rev insert_tagged_brl (taglist 1 brls) netpair; 
0  420 

12320  421 
(*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

422 
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th') 
16809  423 

23178  424 
fun delete_tagged_brl (brl as (eres, th)) (inet, enet) = 
13925  425 
(if eres then 
12320  426 
(case try Thm.major_prem_of th of 
16809  427 
SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet) 
15531  428 
 NONE => (inet, enet)) (*no major premise: ignore*) 
16809  429 
else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet)) 
13925  430 
handle Net.DELETE => (inet,enet); 
1801  431 

432 

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

434 
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

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

436 
fun biresolution_from_nets_tac order match (inet,enet) = 
0  437 
SUBGOAL 
438 
(fn (prem,i) => 

439 
let val hyps = Logic.strip_assums_hyp prem 

10817  440 
and concl = Logic.strip_assums_concl prem 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

441 
val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps 
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

442 
in PRIMSEQ (biresolution match (order kbrls) i) end); 
0  443 

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

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

445 
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

446 
val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist true; 
0  447 

448 
(*fast versions using nets internally*) 

670  449 
val net_biresolve_tac = 
450 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

451 

452 
val net_bimatch_tac = 

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

0  454 

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

456 

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

23178  458 
fun insert_krl (krl as (k,th)) = 
459 
Net.insert_term (K false) (concl_of th, krl); 

0  460 

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

10817  462 
fun build_net rls = 
23178  463 
fold_rev insert_krl (taglist 1 rls) Net.empty; 
0  464 

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

466 
fun filt_resolution_from_net_tac match pred net = 

467 
SUBGOAL 

468 
(fn (prem,i) => 

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

10817  470 
in 
471 
if pred krls 

0  472 
then PRIMSEQ 
10805  473 
(biresolution match (map (pair false) (orderlist krls)) i) 
0  474 
else no_tac 
475 
end); 

476 

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

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

10817  479 
fun filt_resolve_tac rules maxr = 
0  480 
let fun pred krls = length krls <= maxr 
481 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

482 

483 
(*versions taking prebuilt nets*) 

484 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

485 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

486 

487 
(*fast versions using nets internally*) 

488 
val net_resolve_tac = resolve_from_net_tac o build_net; 

489 
val net_match_tac = match_from_net_tac o build_net; 

490 

491 

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

493 

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

495 
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

496 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  497 

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

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

500 

501 

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

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

503 
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

504 
separated by blanks ***) 
0  505 

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

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

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

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

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

513 
else (); PRIMITIVE (rename_params_rule (xs, i))); 
9535  514 

22583
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

515 
(*scan a list of characters into "words" composed of "letters" (recognized by 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

516 
is_let) and separated by any number of non"letters"*) 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

517 
fun scanwords is_let cs = 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

518 
let fun scan1 [] = [] 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

519 
 scan1 cs = 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

520 
let val (lets, rest) = take_prefix is_let cs 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

521 
in implode lets :: scanwords is_let rest end; 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

522 
in scan1 (#2 (take_prefix (not o is_let) cs)) end; 
4b1ecb19b411
added scanwords from library.ML (for obsolete rename_tac);
wenzelm
parents:
22568
diff
changeset

523 

10817  524 
fun rename_tac str i = 
525 
let val cs = Symbol.explode str in 

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

530 

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

10817  533 
fun rename_last_tac a sufs i = 
0  534 
let val names = map (curry op^ a) sufs 
535 
in if Syntax.is_identifier a 

536 
then PRIMITIVE (rename_params_rule (names,i)) 

537 
else all_tac 

538 
end; 

539 

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

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

543 
 rotate_tac k i = PRIMITIVE (rotate_rule k i); 
1209  544 

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

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

546 
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

547 

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

15531  550 
let fun Then NONE tac = SOME tac 
551 
 Then (SOME tac) tac' = SOME(tac THEN' tac'); 

19473  552 
fun thins H (tac,n) = 
5974  553 
if p H then (tac,n+1) 
554 
else (Then tac (rotate_tac n THEN' etac thin_rl),0); 

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

556 
let val Hs = Logic.strip_assums_hyp subg 

19473  557 
in case fst(fold thins Hs (NONE,0)) of 
15531  558 
NONE => no_tac  SOME tac => tac n 
5974  559 
end) 
560 
end; 

561 

0  562 
end; 
1501  563 

11774  564 
structure BasicTactic: BASIC_TACTIC = Tactic; 
565 
open BasicTactic; 