author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5838  a4122945d638 
child 5956  ab4d13e9e77a 
permissions  rwrr 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

1 
(* Title: Pure/tactic.ML 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

6 
Tactics 

7 
*) 

8 

9 
signature TACTIC = 

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

11 
val ares_tac : thm list > int > tactic 
0  12 
val asm_rewrite_goal_tac: 
4713  13 
bool*bool*bool > (meta_simpset > tactic) > meta_simpset > int > tactic 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

14 
val assume_tac : int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

15 
val atac : int >tactic 
670  16 
val bimatch_from_nets_tac: 
1501  17 
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > int > tactic 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

18 
val bimatch_tac : (bool*thm)list > int > tactic 
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

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

20 
('a list > (bool * thm) list) > 
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

21 
bool > 'a Net.net * 'a Net.net > int > tactic 
670  22 
val biresolve_from_nets_tac: 
1501  23 
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > int > tactic 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

24 
val biresolve_tac : (bool*thm)list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

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

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

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

30 
val compose_tac : (bool * thm * int) > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

31 
val cut_facts_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

32 
val cut_inst_tac : (string*string)list > thm > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

33 
val defer_tac : int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

35 
val dmatch_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

36 
val dresolve_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

37 
val dres_inst_tac : (string*string)list > thm > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

38 
val dtac : thm > int >tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

39 
val etac : thm > int >tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

40 
val eq_assume_tac : int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

41 
val ematch_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

42 
val eresolve_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

43 
val eres_inst_tac : (string*string)list > thm > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

44 
val filter_thms : (term*term>bool) > int*term*thm list > thm list 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

45 
val filt_resolve_tac : thm list > int > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

47 
val fold_goals_tac : thm list > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

48 
val fold_tac : thm list > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

49 
val forward_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

50 
val forw_inst_tac : (string*string)list > thm > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

51 
val insert_tagged_brl : ('a*(bool*thm)) * 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

52 
(('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) > 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

53 
('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

54 
val delete_tagged_brl : (bool*thm) * 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

55 
((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) > 
1801  56 
(int*(bool*thm))Net.net * (int*(bool*thm))Net.net 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

57 
val is_fact : thm > bool 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

58 
val lessb : (bool * thm) * (bool * thm) > bool 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

59 
val lift_inst_rule : thm * int * (string*string)list * thm > thm 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

60 
val make_elim : thm > thm 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

61 
val match_from_net_tac : (int*thm) Net.net > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

62 
val match_tac : thm list > int > tactic 
5838  63 
val metacut_tac : thm > int > tactic 
64 
val metacuts_tac : thm list > int > tactic 

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

65 
val net_bimatch_tac : (bool*thm) list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

66 
val net_biresolve_tac : (bool*thm) list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

67 
val net_match_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

68 
val net_resolve_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

69 
val orderlist : (int * 'a) list > 'a list 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

70 
val PRIMITIVE : (thm > thm) > tactic 
4270  71 
val PRIMSEQ : (thm > thm Seq.seq) > tactic 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

73 
val rename_tac : string > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

74 
val rename_last_tac : string > string list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

75 
val resolve_from_net_tac : (int*thm) Net.net > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

76 
val resolve_tac : thm list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

78 
val rewrite_goals_rule: thm list > thm > thm 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

79 
val rewrite_rule : thm list > thm > thm 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

80 
val rewrite_goals_tac : thm list > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

81 
val rewrite_tac : thm list > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

82 
val rewtac : thm > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

83 
val rotate_tac : int > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

84 
val rtac : thm > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

85 
val rule_by_tactic : tactic > thm > thm 
5263  86 
val solve_tac : thm list > int > tactic 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

87 
val subgoal_tac : string > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

88 
val subgoals_tac : string list > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

89 
val subgoals_of_brl : bool * thm > int 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

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

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

93 
val thin_tac : string > int > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

94 
val trace_goalno_tac : (int > tactic) > int > tactic 
1501  95 
end; 
0  96 

97 

1501  98 
structure Tactic : TACTIC = 
0  99 
struct 
100 

1501  101 
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 
102 
fun trace_goalno_tac tac i st = 

4270  103 
case Seq.pull(tac i st) of 
104 
None => Seq.empty 

0  105 
 seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
4270  106 
Seq.make(fn()=> seqcell)); 
0  107 

108 

2029  109 
(*Rotates the given subgoal to be the last. Useful when replaying 
110 
an old proof script, when the proof of an early subgoal fails. 

4611  111 
DOES NOT WORK FOR TYPE VARIABLES. 
112 
Similar to drule/rotate_prems*) 

2029  113 
fun defer_tac i state = 
114 
let val (state',thaw) = freeze_thaw state 

115 
val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) 

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2228
diff
changeset

116 
val hyp::hyps' = List.drop(hyps, i1) 
2029  117 
in implies_intr hyp (implies_elim_list state' (map assume hyps)) 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2228
diff
changeset

118 
> implies_intr_list (List.take(hyps, i1) @ hyps') 
2029  119 
> thaw 
4270  120 
> Seq.single 
2029  121 
end 
4270  122 
handle _ => Seq.empty; 
2029  123 

0  124 

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

1501  126 
fun rule_by_tactic tac rl = 
2688  127 
let val (st, thaw) = freeze_thaw (zero_var_indexes rl) 
4270  128 
in case Seq.pull (tac st) of 
1460  129 
None => raise THM("rule_by_tactic", 0, [rl]) 
2688  130 
 Some(st',_) => Thm.varifyT (thaw st') 
131 
end; 

0  132 

133 
(*** Basic tactics ***) 

134 

135 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm seq.*) 

4270  136 
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty; 
0  137 

138 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm.*) 

4270  139 
fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); 
0  140 

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

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

143 

144 
(*Solve subgoal i by assumption*) 

145 
fun assume_tac i = PRIMSEQ (assumption i); 

146 

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

148 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

149 

150 
(** Resolution/matching tactics **) 

151 

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

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

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

155 

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

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

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

159 

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

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

162 

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

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

165 

166 
(*Resolution with elimination rules only*) 

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

168 

169 
(*Forward reasoning using destruction rules.*) 

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

171 

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

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

174 

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

1460  176 
fun rtac rl = resolve_tac [rl]; 
177 
fun etac rl = eresolve_tac [rl]; 

178 
fun dtac rl = dresolve_tac [rl]; 

0  179 
val atac = assume_tac; 
180 

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

182 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

183 

5263  184 
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac; 
185 

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

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

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

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

191 

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

193 
val flexflex_tac = PRIMSEQ flexflex_rule; 

194 

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

195 

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

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

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

198 
fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b); 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

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

201 
let val (frozth,thawfn) = freeze_thaw state 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

202 
val froz_prems = cprems_of frozth 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

203 
val assumed = implies_elim_list frozth (map assume froz_prems) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

204 
val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

205 
assumed; 
4270  206 
in Seq.single (thawfn implied) end 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

208 

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

209 

0  210 
(*Lift and instantiate a rule wrt the given state and subgoal number *) 
1501  211 
fun lift_inst_rule (st, i, sinsts, rule) = 
212 
let val {maxidx,sign,...} = rep_thm st 

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

1460  214 
val params = Logic.strip_params Bi (*params of subgoal i*) 
0  215 
val params = rev(rename_wrt_term Bi params) (*as they are printed*) 
216 
val paramTs = map #2 params 

217 
and inc = maxidx+1 

218 
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs> incr_tvar inc T) 

219 
 liftvar t = raise TERM("Variable expected", [t]); 

220 
fun liftterm t = list_abs_free (params, 

1460  221 
Logic.incr_indexes(paramTs,inc) t) 
0  222 
(*Lifts instantiation pair over params*) 
230  223 
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) 
0  224 
fun lifttvar((a,i),ctyp) = 
1460  225 
let val {T,sign} = rep_ctyp ctyp 
226 
in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end 

1501  227 
val rts = types_sorts rule and (types,sorts) = types_sorts st 
0  228 
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1)  sm => sm) 
229 
 types'(ixn) = types ixn; 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

230 
val used = add_term_tvarnames 
1501  231 
(#prop(rep_thm st) $ #prop(rep_thm rule),[]) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

232 
val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts 
0  233 
in instantiate (map lifttvar Tinsts, map liftpair insts) 
1501  234 
(lift_rule (st,i) rule) 
0  235 
end; 
236 

3984  237 
(* 
238 
Like lift_inst_rule but takes terms, not strings, where the terms may contain 

239 
Bounds referring to parameters of the subgoal. 

240 

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

242 

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

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

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

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

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

248 

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

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

251 
*) 

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

252 
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = 
1966  253 
let val {maxidx,sign,...} = rep_thm st 
254 
val (_, _, Bi, _) = dest_state(st,i) 

255 
val params = Logic.strip_params Bi (*params of subgoal i*) 

256 
val paramTs = map #2 params 

257 
and inc = maxidx+1 

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

258 
fun liftvar ((a,j), T) = Var((a, j+inc), paramTs> incr_tvar inc T) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

259 
(*lift only Var, not term, which must be lifted already*) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

260 
fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

261 
fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T)) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

262 
in instantiate (map liftTpair Tinsts, map liftpair insts) 
1966  263 
(lift_rule (st,i) rule) 
264 
end; 

0  265 

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

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

268 

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

3538  270 
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = st > 
271 
(compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i 

272 
handle TERM (msg,_) => (writeln msg; no_tac) 

273 
 THM (msg,_,_) => (writeln msg; no_tac)); 

0  274 

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

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

278 

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

280 
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

281 
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

282 
goals. 
761  283 
*) 
0  284 
fun res_inst_tac sinsts rule i = 
285 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

286 

1501  287 
(*eresolve elimination version*) 
0  288 
fun eres_inst_tac sinsts rule i = 
289 
compose_inst_tac sinsts (true, rule, nprems_of rule) i; 

290 

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

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

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

294 
let val {maxidx,...} = rep_thm rl 
3991  295 
fun cvar ixn = cterm_of (sign_of ProtoPure.thy) (Var(ixn,propT)); 
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

296 
val revcut_rl' = 
1460  297 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
298 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 

0  299 
val arg = (false, rl, nprems_of rl) 
4270  300 
val [th] = Seq.list_of (bicompose false arg 1 revcut_rl') 
0  301 
in th end 
302 
handle Bind => raise THM("make_elim_preserve", 1, [rl]); 

303 

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

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

305 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  306 

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

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

308 
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

309 

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

310 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  311 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
312 

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

315 

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

316 
(*** Applications of cut_rl ***) 
0  317 

318 
(*Used by metacut_tac*) 

319 
fun bires_cut_tac arg i = 

1460  320 
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; 
0  321 

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

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

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

5838  325 
fun metacuts_tac rules i = EVERY (map (fn th => metacut_tac th i) rules); 
0  326 

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

328 
fun is_fact rl = 

329 
case prems_of rl of 

1460  330 
[] => true  _::_ => false; 
0  331 

332 
(*"Cut" all facts from theorem list into the goal as assumptions. *) 

333 
fun cut_facts_tac ths i = 

334 
EVERY (map (fn th => metacut_tac th i) (filter is_fact ths)); 

335 

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

4178
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset

337 
fun subgoal_tac sprop i st = 
4270  338 
let val st' = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st) 
4178
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset

339 
val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i)) 
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset

340 
in 
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset

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

342 
else warning"Type variables in new subgoal: add a type constraint?"; 
4270  343 
Seq.single st' 
4178
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset

344 
end; 
0  345 

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

348 

0  349 

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

351 

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

1460  353 
using the predicate could(subgoal,concl). 
0  354 
Resulting list is no longer than "limit"*) 
355 
fun filter_thms could (limit, prem, ths) = 

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

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

1460  358 
 filtr (limit, th::ths) = 
359 
if limit=0 then [] 

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

361 
else filtr(limit,ths) 

0  362 
in filtr(limit,ths) end; 
363 

364 

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

366 

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

368 

369 
(*insert tags*) 

370 
fun taglist k [] = [] 

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

372 

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

374 
fun untaglist [] = [] 

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

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

377 
if k=k' then untaglist rest 

378 
else x :: untaglist rest; 

379 

380 
(*return list elements in original order*) 

4438  381 
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); 
0  382 

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

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

384 
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = 
0  385 
if eres then 
1460  386 
case prems_of th of 
387 
prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) 

388 
 [] => error"insert_tagged_brl: elimination rule with no premises" 

0  389 
else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); 
390 

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

670  392 
fun build_netpair netpair brls = 
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

393 
foldr insert_tagged_brl (taglist 1 brls, netpair); 
0  394 

1801  395 
(*delete one kbrl from the pair of nets; 
396 
we don't know the value of k, so we use 0 and ignore it in the comparison*) 

397 
local 

398 
fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th') 

399 
in 

400 
fun delete_tagged_brl (brl as (eres,th), (inet,enet)) = 

401 
if eres then 

402 
case prems_of th of 

403 
prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl)) 

2814
a318f7f3a65c
delete_tagged_brl just ignores nonelimination rules instead of complaining
paulson
parents:
2688
diff
changeset

404 
 [] => (inet,enet) (*no major premise: ignore*) 
1801  405 
else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet); 
406 
end; 

407 

408 

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

409 
(*biresolution using a pair of nets rather than rules. 
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

410 
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

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

412 
fun biresolution_from_nets_tac order match (inet,enet) = 
0  413 
SUBGOAL 
414 
(fn (prem,i) => 

415 
let val hyps = Logic.strip_assums_hyp prem 

416 
and concl = Logic.strip_assums_concl prem 

417 
val kbrls = Net.unify_term inet concl @ 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset

418 
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

419 
in PRIMSEQ (biresolution match (order kbrls) i) end); 
0  420 

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

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

422 
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

423 
val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist true; 
0  424 

425 
(*fast versions using nets internally*) 

670  426 
val net_biresolve_tac = 
427 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

428 

429 
val net_bimatch_tac = 

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

0  431 

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

433 

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

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

436 
Net.insert_term ((concl_of th, krl), net, K false); 

437 

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

439 
fun build_net rls = 

440 
foldr insert_krl (taglist 1 rls, Net.empty); 

441 

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

443 
fun filt_resolution_from_net_tac match pred net = 

444 
SUBGOAL 

445 
(fn (prem,i) => 

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

447 
in 

1460  448 
if pred krls 
0  449 
then PRIMSEQ 
1460  450 
(biresolution match (map (pair false) (orderlist krls)) i) 
0  451 
else no_tac 
452 
end); 

453 

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

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

456 
fun filt_resolve_tac rules maxr = 

457 
let fun pred krls = length krls <= maxr 

458 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

459 

460 
(*versions taking prebuilt nets*) 

461 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

462 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

463 

464 
(*fast versions using nets internally*) 

465 
val net_resolve_tac = resolve_from_net_tac o build_net; 

466 
val net_match_tac = match_from_net_tac o build_net; 

467 

468 

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

470 

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

472 
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

473 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  474 

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

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

477 

478 

479 
(*** MetaRewriting Tactics ***) 

480 

481 
fun result1 tacf mss thm = 

4270  482 
apsome fst (Seq.pull (tacf mss thm)); 
0  483 

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

484 
val simple_prover = 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

485 
result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss))); 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

486 

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

487 
val rewrite_rule = Drule.rewrite_rule_aux simple_prover; 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset

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

489 

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

490 

2145  491 
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) 
492 
fun asm_rewrite_goal_tac mode prover_tac mss = 

493 
SELECT_GOAL 

494 
(PRIMITIVE 

495 
(rewrite_goal_rule mode (result1 prover_tac) mss 1)); 

0  496 

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

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

498 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  499 

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

501 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  502 

1460  503 
fun rewtac def = rewrite_goals_tac [def]; 
0  504 

505 

1501  506 
(*** 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

507 

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

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

509 
fun term_depth (Abs(a,T,t)) = 1 + term_depth t 
2145  510 
 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

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

512 

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

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

514 

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

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

516 
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

517 
fun sort_lhs_depths defs = 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

518 
let val keylist = make_keylist (term_depth o lhs_of_thm) defs 
4438  519 
val keys = distinct (sort (rev_order o int_ord) (map #2 keylist)) 
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

520 
in map (keyfilter keylist) keys end; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

521 

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

522 
fun fold_tac defs = EVERY 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

523 
(map rewrite_tac (sort_lhs_depths (map symmetric defs))); 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

524 

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

525 
fun fold_goals_tac defs = EVERY 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

526 
(map rewrite_goals_tac (sort_lhs_depths (map symmetric defs))); 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

527 

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

528 

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

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

530 
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

531 
separated by blanks ***) 
0  532 

533 
(*Calling this will generate the warning "Same as previous level" since 

534 
it affects nothing but the names of bound variables!*) 

535 
fun rename_tac str i = 

4693  536 
let val cs = Symbol.explode str 
0  537 
in 
538 
if !Logic.auto_rename 

4213  539 
then (warning "Resetting Logic.auto_rename"; 
1460  540 
Logic.auto_rename := false) 
0  541 
else (); 
4693  542 
case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of 
543 
[] => PRIMITIVE (rename_params_rule (scanwords Symbol.is_letdig cs, i)) 

0  544 
 c::_ => error ("Illegal character: " ^ c) 
545 
end; 

546 

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

0  549 
fun rename_last_tac a sufs i = 
550 
let val names = map (curry op^ a) sufs 

551 
in if Syntax.is_identifier a 

552 
then PRIMITIVE (rename_params_rule (names,i)) 

553 
else all_tac 

554 
end; 

555 

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

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

559 
val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; 

0  560 

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

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

564 
 rotate_tac k i = PRIMITIVE (rotate_rule k i); 
1209  565 

0  566 
end; 
1501  567 

568 
open Tactic; 