author  wenzelm 
Wed, 23 Jul 1997 10:22:30 +0200  
changeset 3554  b1013660aeff 
parent 3538  ed9de44032e0 
child 3575  4e9beacb5339 
permissions  rwrr 
1460  1 
(* Title: tactic 
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: 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset

13 
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 
670  19 
val biresolve_from_nets_tac: 
1501  20 
(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

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

22 
val build_net : thm list > (int*thm) Net.net 
1501  23 
val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > 
24 
(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

25 
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

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

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

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

29 
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

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

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

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

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

34 
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

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

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

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

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

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

40 
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

41 
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

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

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

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

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

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

47 
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

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

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

50 
(('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

51 
('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

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

53 
((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) > 
1801  54 
(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

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

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

57 
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

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

59 
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

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

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

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

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

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

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

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

67 
val PRIMITIVE : (thm > thm) > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

68 
val PRIMSEQ : (thm > thm Sequence.seq) > tactic 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

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

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

72 
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

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

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

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

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

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

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

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

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

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

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

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

84 
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

85 
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

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

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

88 
val trace_goalno_tac : (int > tactic) > int > tactic 
1501  89 
end; 
0  90 

91 

1501  92 
structure Tactic : TACTIC = 
0  93 
struct 
94 

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

97 
case Sequence.pull(tac i st) of 

1460  98 
None => Sequence.null 
0  99 
 seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
1501  100 
Sequence.seqof(fn()=> seqcell)); 
0  101 

102 

2029  103 
(*Convert all Vars in a theorem to Frees. Also return a function for 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

104 
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

105 
Similar code in type/freeze_thaw*) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

107 
let val fth = freezeT th 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

108 
val {prop,sign,...} = rep_thm fth 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

109 
val used = add_term_names (prop, []) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

110 
and vars = term_vars prop 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

111 
fun newName (Var(ix,_), (pairs,used)) = 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

112 
let val v = variant used (string_of_indexname ix) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

113 
in ((ix,v)::pairs, v::used) end; 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

114 
val (alist, _) = foldr newName (vars, ([], used)) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

115 
fun mk_inst (Var(v,T)) = 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

116 
(cterm_of sign (Var(v,T)), 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

117 
cterm_of sign (Free(the (assoc(alist,v)), T))) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

118 
val insts = map mk_inst vars 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

119 
fun thaw th' = 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

120 
th' > forall_intr_list (map #2 insts) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

121 
> forall_elim_list (map #1 insts) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

122 
in (instantiate ([],insts) fth, thaw) end; 
2029  123 

124 

125 
(*Rotates the given subgoal to be the last. Useful when replaying 

126 
an old proof script, when the proof of an early subgoal fails. 

127 
DOES NOT WORK FOR TYPE VARIABLES.*) 

128 
fun defer_tac i state = 

129 
let val (state',thaw) = freeze_thaw state 

130 
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

131 
val hyp::hyps' = List.drop(hyps, i1) 
2029  132 
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

133 
> implies_intr_list (List.take(hyps, i1) @ hyps') 
2029  134 
> thaw 
135 
> Sequence.single 

136 
end 

137 
handle _ => Sequence.null; 

138 

0  139 

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

1501  141 
fun rule_by_tactic tac rl = 
2688  142 
let val (st, thaw) = freeze_thaw (zero_var_indexes rl) 
143 
in case Sequence.pull (tac st) of 

1460  144 
None => raise THM("rule_by_tactic", 0, [rl]) 
2688  145 
 Some(st',_) => Thm.varifyT (thaw st') 
146 
end; 

0  147 

148 
(*** Basic tactics ***) 

149 

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

1501  151 
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Sequence.null; 
0  152 

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

154 
fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun); 

155 

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

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

158 

159 
(*Solve subgoal i by assumption*) 

160 
fun assume_tac i = PRIMSEQ (assumption i); 

161 

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

163 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

164 

165 
(** Resolution/matching tactics **) 

166 

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

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

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

170 

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

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

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

174 

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

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

177 

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

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

180 

181 
(*Resolution with elimination rules only*) 

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

183 

184 
(*Forward reasoning using destruction rules.*) 

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

186 

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

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

189 

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

1460  191 
fun rtac rl = resolve_tac [rl]; 
192 
fun etac rl = eresolve_tac [rl]; 

193 
fun dtac rl = dresolve_tac [rl]; 

0  194 
val atac = assume_tac; 
195 

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

197 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

198 

199 
(*Matching tactics  as above, but forbid updating of state*) 

200 
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i); 

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

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

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

204 

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

206 
val flexflex_tac = PRIMSEQ flexflex_rule; 

207 

3409
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 
(*Remove duplicate subgoals. By Mark Staples*) 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

211 
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

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

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

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

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

216 
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

217 
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

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

219 
in Sequence.single (thawfn implied) end 
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

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

221 

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

222 

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

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

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

230 
and inc = maxidx+1 

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

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

233 
fun liftterm t = list_abs_free (params, 

1460  234 
Logic.incr_indexes(paramTs,inc) t) 
0  235 
(*Lifts instantiation pair over params*) 
230  236 
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) 
0  237 
fun lifttvar((a,i),ctyp) = 
1460  238 
let val {T,sign} = rep_ctyp ctyp 
239 
in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end 

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

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

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

245 
val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts 
0  246 
in instantiate (map lifttvar Tinsts, map liftpair insts) 
1501  247 
(lift_rule (st,i) rule) 
0  248 
end; 
249 

1966  250 
(*Like lift_inst_rule but takes cterms, not strings. 
251 
The cterms must be functions of the parameters of the subgoal, 

252 
i.e. they are assumed to be lifted already! 

253 
Also: types of Vars must be fully instantiated already *) 

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

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

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

258 
val paramTs = map #2 params 

259 
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

260 
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

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

262 
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

263 
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

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

0  267 

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

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

270 

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

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

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

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

0  276 

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

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

280 

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

282 
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

283 
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

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

288 

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

292 

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

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

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

296 
let val {maxidx,...} = rep_thm rl 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
761
diff
changeset

297 
fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT)); 
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

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

0  301 
val arg = (false, rl, nprems_of rl) 
302 
val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') 

303 
in th end 

304 
handle Bind => raise THM("make_elim_preserve", 1, [rl]); 

305 

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

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

307 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  308 

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

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

310 
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

311 

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

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

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

317 

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

318 
(*** Applications of cut_rl ***) 
0  319 

320 
(*Used by metacut_tac*) 

321 
fun bires_cut_tac arg i = 

1460  322 
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; 
0  323 

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

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

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

327 

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

329 
fun is_fact rl = 

330 
case prems_of rl of 

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

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

334 
fun cut_facts_tac ths i = 

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

336 

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

338 
fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl; 

339 

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

342 

0  343 

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

345 

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

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

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

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

1460  352 
 filtr (limit, th::ths) = 
353 
if limit=0 then [] 

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

355 
else filtr(limit,ths) 

0  356 
in filtr(limit,ths) end; 
357 

358 

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

360 

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

362 

363 
(*insert tags*) 

364 
fun taglist k [] = [] 

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

366 

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

368 
fun untaglist [] = [] 

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

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

371 
if k=k' then untaglist rest 

372 
else x :: untaglist rest; 

373 

374 
(*return list elements in original order*) 

2228
f381c1a98209
Etaexpansion of a function definition, for value polymorphism
paulson
parents:
2145
diff
changeset

375 
fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
0  376 

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

378 
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = 
0  379 
if eres then 
1460  380 
case prems_of th of 
381 
prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) 

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

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

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

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

387 
foldr insert_tagged_brl (taglist 1 brls, netpair); 
0  388 

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

391 
local 

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

393 
in 

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

395 
if eres then 

396 
case prems_of th of 

397 
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

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

401 

402 

0  403 
(*biresolution using a pair of nets rather than rules*) 
404 
fun biresolution_from_nets_tac match (inet,enet) = 

405 
SUBGOAL 

406 
(fn (prem,i) => 

407 
let val hyps = Logic.strip_assums_hyp prem 

408 
and concl = Logic.strip_assums_concl prem 

409 
val kbrls = Net.unify_term inet concl @ 

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

410 
List.concat (map (Net.unify_term enet) hyps) 
0  411 
in PRIMSEQ (biresolution match (orderlist kbrls) i) end); 
412 

413 
(*versions taking prebuilt nets*) 

414 
val biresolve_from_nets_tac = biresolution_from_nets_tac false; 

415 
val bimatch_from_nets_tac = biresolution_from_nets_tac true; 

416 

417 
(*fast versions using nets internally*) 

670  418 
val net_biresolve_tac = 
419 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

420 

421 
val net_bimatch_tac = 

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

0  423 

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

425 

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

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

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

429 

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

431 
fun build_net rls = 

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

433 

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

435 
fun filt_resolution_from_net_tac match pred net = 

436 
SUBGOAL 

437 
(fn (prem,i) => 

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

439 
in 

1460  440 
if pred krls 
0  441 
then PRIMSEQ 
1460  442 
(biresolution match (map (pair false) (orderlist krls)) i) 
0  443 
else no_tac 
444 
end); 

445 

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

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

448 
fun filt_resolve_tac rules maxr = 

449 
let fun pred krls = length krls <= maxr 

450 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

451 

452 
(*versions taking prebuilt nets*) 

453 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

454 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

455 

456 
(*fast versions using nets internally*) 

457 
val net_resolve_tac = resolve_from_net_tac o build_net; 

458 
val net_match_tac = match_from_net_tac o build_net; 

459 

460 

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

462 

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

464 
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

465 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  466 

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

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

469 

470 

471 
(*** MetaRewriting Tactics ***) 

472 

473 
fun result1 tacf mss thm = 

3554  474 
apsome fst (Sequence.pull (tacf mss thm)); 
0  475 

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

478 
SELECT_GOAL 

479 
(PRIMITIVE 

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

0  481 

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

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

483 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  484 

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

486 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  487 

1460  488 
fun rewtac def = rewrite_goals_tac [def]; 
0  489 

490 

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

492 

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

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

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

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

497 

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

498 
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

499 

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

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

501 
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

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

503 
let val keylist = make_keylist (term_depth o lhs_of_thm) defs 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

504 
val keys = distinct (sort op> (map #2 keylist)) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

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

506 

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

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

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

509 

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

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

511 
(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

512 

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

513 

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

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

515 
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

516 
separated by blanks ***) 
0  517 

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

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

520 
fun rename_tac str i = 

521 
let val cs = explode str 

522 
in 

523 
if !Logic.auto_rename 

524 
then (writeln"Note: setting Logic.auto_rename := false"; 

1460  525 
Logic.auto_rename := false) 
0  526 
else (); 
527 
case #2 (take_prefix (is_letdig orf is_blank) cs) of 

528 
[] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i)) 

529 
 c::_ => error ("Illegal character: " ^ c) 

530 
end; 

531 

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

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

536 
in if Syntax.is_identifier a 

537 
then PRIMITIVE (rename_params_rule (names,i)) 

538 
else all_tac 

539 
end; 

540 

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

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

544 
val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; 

0  545 

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

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

549 
 rotate_tac k i = PRIMITIVE (rotate_rule k i); 
1209  550 

0  551 
end; 
1501  552 

553 
open Tactic; 