wenzelm@37781
|
1 |
(* Title: Tools/misc_legacy.ML
|
wenzelm@37781
|
2 |
|
wenzelm@37781
|
3 |
Misc legacy stuff -- to be phased out eventually.
|
wenzelm@37781
|
4 |
*)
|
wenzelm@37781
|
5 |
|
wenzelm@37781
|
6 |
signature MISC_LEGACY =
|
wenzelm@37781
|
7 |
sig
|
wenzelm@45004
|
8 |
val add_term_names: term * string list -> string list
|
wenzelm@45004
|
9 |
val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
|
wenzelm@45004
|
10 |
val add_typ_tfree_names: typ * string list -> string list
|
wenzelm@45004
|
11 |
val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
|
wenzelm@45004
|
12 |
val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
|
wenzelm@45004
|
13 |
val add_term_tfrees: term * (string * sort) list -> (string * sort) list
|
wenzelm@45004
|
14 |
val add_term_tfree_names: term * string list -> string list
|
wenzelm@45004
|
15 |
val typ_tfrees: typ -> (string * sort) list
|
wenzelm@45004
|
16 |
val typ_tvars: typ -> (indexname * sort) list
|
wenzelm@45004
|
17 |
val term_tfrees: term -> (string * sort) list
|
wenzelm@45004
|
18 |
val term_tvars: term -> (indexname * sort) list
|
wenzelm@45004
|
19 |
val add_term_vars: term * term list -> term list
|
wenzelm@45004
|
20 |
val term_vars: term -> term list
|
wenzelm@45004
|
21 |
val add_term_frees: term * term list -> term list
|
wenzelm@45004
|
22 |
val term_frees: term -> term list
|
wenzelm@37781
|
23 |
val mk_defpair: term * term -> string * term
|
wenzelm@37781
|
24 |
val get_def: theory -> xstring -> thm
|
wenzelm@37781
|
25 |
val METAHYPS: (thm list -> tactic) -> int -> tactic
|
wenzelm@47893
|
26 |
val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
|
wenzelm@47893
|
27 |
val freeze_thaw: thm -> thm * (thm -> thm)
|
wenzelm@37781
|
28 |
end;
|
wenzelm@37781
|
29 |
|
wenzelm@37781
|
30 |
structure Misc_Legacy: MISC_LEGACY =
|
wenzelm@37781
|
31 |
struct
|
wenzelm@37781
|
32 |
|
wenzelm@45004
|
33 |
(*iterate a function over all types in a term*)
|
wenzelm@45004
|
34 |
fun it_term_types f =
|
wenzelm@45004
|
35 |
let fun iter(Const(_,T), a) = f(T,a)
|
wenzelm@45004
|
36 |
| iter(Free(_,T), a) = f(T,a)
|
wenzelm@45004
|
37 |
| iter(Var(_,T), a) = f(T,a)
|
wenzelm@45004
|
38 |
| iter(Abs(_,T,t), a) = iter(t,f(T,a))
|
wenzelm@45004
|
39 |
| iter(f$u, a) = iter(f, iter(u, a))
|
wenzelm@45004
|
40 |
| iter(Bound _, a) = a
|
wenzelm@45004
|
41 |
in iter end
|
wenzelm@45004
|
42 |
|
wenzelm@45004
|
43 |
(*Accumulates the names in the term, suppressing duplicates.
|
wenzelm@45004
|
44 |
Includes Frees and Consts. For choosing unambiguous bound var names.*)
|
wenzelm@45004
|
45 |
fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
|
wenzelm@45004
|
46 |
| add_term_names (Free(a,_), bs) = insert (op =) a bs
|
wenzelm@45004
|
47 |
| add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
|
wenzelm@45004
|
48 |
| add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
|
wenzelm@45004
|
49 |
| add_term_names (_, bs) = bs;
|
wenzelm@45004
|
50 |
|
wenzelm@45004
|
51 |
(*Accumulates the TVars in a type, suppressing duplicates.*)
|
wenzelm@45004
|
52 |
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
|
wenzelm@45004
|
53 |
| add_typ_tvars(TFree(_),vs) = vs
|
wenzelm@45004
|
54 |
| add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
|
wenzelm@45004
|
55 |
|
wenzelm@45004
|
56 |
(*Accumulates the TFrees in a type, suppressing duplicates.*)
|
wenzelm@45004
|
57 |
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
|
wenzelm@45004
|
58 |
| add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
|
wenzelm@45004
|
59 |
| add_typ_tfree_names(TVar(_),fs) = fs;
|
wenzelm@45004
|
60 |
|
wenzelm@45004
|
61 |
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
|
wenzelm@45004
|
62 |
| add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
|
wenzelm@45004
|
63 |
| add_typ_tfrees(TVar(_),fs) = fs;
|
wenzelm@45004
|
64 |
|
wenzelm@45004
|
65 |
(*Accumulates the TVars in a term, suppressing duplicates.*)
|
wenzelm@45004
|
66 |
val add_term_tvars = it_term_types add_typ_tvars;
|
wenzelm@45004
|
67 |
|
wenzelm@45004
|
68 |
(*Accumulates the TFrees in a term, suppressing duplicates.*)
|
wenzelm@45004
|
69 |
val add_term_tfrees = it_term_types add_typ_tfrees;
|
wenzelm@45004
|
70 |
val add_term_tfree_names = it_term_types add_typ_tfree_names;
|
wenzelm@45004
|
71 |
|
wenzelm@45004
|
72 |
(*Non-list versions*)
|
wenzelm@45004
|
73 |
fun typ_tfrees T = add_typ_tfrees(T,[]);
|
wenzelm@45004
|
74 |
fun typ_tvars T = add_typ_tvars(T,[]);
|
wenzelm@45004
|
75 |
fun term_tfrees t = add_term_tfrees(t,[]);
|
wenzelm@45004
|
76 |
fun term_tvars t = add_term_tvars(t,[]);
|
wenzelm@45004
|
77 |
|
wenzelm@45004
|
78 |
|
wenzelm@45004
|
79 |
(*Accumulates the Vars in the term, suppressing duplicates.*)
|
wenzelm@45004
|
80 |
fun add_term_vars (t, vars: term list) = case t of
|
wenzelm@45004
|
81 |
Var _ => Ord_List.insert Term_Ord.term_ord t vars
|
wenzelm@45004
|
82 |
| Abs (_,_,body) => add_term_vars(body,vars)
|
wenzelm@45004
|
83 |
| f$t => add_term_vars (f, add_term_vars(t, vars))
|
wenzelm@45004
|
84 |
| _ => vars;
|
wenzelm@45004
|
85 |
|
wenzelm@45004
|
86 |
fun term_vars t = add_term_vars(t,[]);
|
wenzelm@45004
|
87 |
|
wenzelm@45004
|
88 |
(*Accumulates the Frees in the term, suppressing duplicates.*)
|
wenzelm@45004
|
89 |
fun add_term_frees (t, frees: term list) = case t of
|
wenzelm@45004
|
90 |
Free _ => Ord_List.insert Term_Ord.term_ord t frees
|
wenzelm@45004
|
91 |
| Abs (_,_,body) => add_term_frees(body,frees)
|
wenzelm@45004
|
92 |
| f$t => add_term_frees (f, add_term_frees(t, frees))
|
wenzelm@45004
|
93 |
| _ => frees;
|
wenzelm@45004
|
94 |
|
wenzelm@45004
|
95 |
fun term_frees t = add_term_frees(t,[]);
|
wenzelm@45004
|
96 |
|
wenzelm@45004
|
97 |
|
wenzelm@37781
|
98 |
fun mk_defpair (lhs, rhs) =
|
wenzelm@37781
|
99 |
(case Term.head_of lhs of
|
wenzelm@37781
|
100 |
Const (name, _) =>
|
wenzelm@47780
|
101 |
(Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs))
|
wenzelm@37781
|
102 |
| _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
|
wenzelm@37781
|
103 |
|
wenzelm@37781
|
104 |
|
wenzelm@37781
|
105 |
fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
|
wenzelm@37781
|
106 |
|
wenzelm@37781
|
107 |
|
wenzelm@37781
|
108 |
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
|
wenzelm@37781
|
109 |
METAHYPS (fn prems => tac prems) i
|
wenzelm@37781
|
110 |
|
wenzelm@37781
|
111 |
converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
|
wenzelm@37781
|
112 |
proof state A==>A, supplying A1,...,An as meta-level assumptions (in
|
wenzelm@37781
|
113 |
"prems"). The parameters x1,...,xm become free variables. If the
|
wenzelm@37781
|
114 |
resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
|
wenzelm@37781
|
115 |
then it is lifted back into the original context, yielding k subgoals.
|
wenzelm@37781
|
116 |
|
wenzelm@37781
|
117 |
Replaces unknowns in the context by Frees having the prefix METAHYP_
|
wenzelm@37781
|
118 |
New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
|
wenzelm@37781
|
119 |
DOES NOT HANDLE TYPE UNKNOWNS.
|
wenzelm@37781
|
120 |
|
wenzelm@37781
|
121 |
|
wenzelm@37781
|
122 |
NOTE: This version does not observe the proof context, and thus cannot
|
wenzelm@37781
|
123 |
work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for
|
wenzelm@37781
|
124 |
properly localized variants of the same idea.
|
wenzelm@37781
|
125 |
****)
|
wenzelm@37781
|
126 |
|
wenzelm@37781
|
127 |
local
|
wenzelm@37781
|
128 |
|
wenzelm@37781
|
129 |
(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B )
|
wenzelm@37781
|
130 |
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters.
|
wenzelm@37781
|
131 |
Main difference from strip_assums concerns parameters:
|
wenzelm@37781
|
132 |
it replaces the bound variables by free variables. *)
|
wenzelm@37781
|
133 |
fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
|
wenzelm@37781
|
134 |
strip_context_aux (params, H :: Hs, B)
|
wenzelm@37781
|
135 |
| strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
|
wenzelm@43156
|
136 |
let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
|
wenzelm@37781
|
137 |
in strip_context_aux ((b, T) :: params, Hs, u) end
|
wenzelm@37781
|
138 |
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
|
wenzelm@37781
|
139 |
|
wenzelm@37781
|
140 |
fun strip_context A = strip_context_aux ([], [], A);
|
wenzelm@37781
|
141 |
|
wenzelm@37781
|
142 |
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
|
wenzelm@37781
|
143 |
Instantiates distinct free variables by terms of same type.*)
|
wenzelm@37781
|
144 |
fun free_instantiate ctpairs =
|
wenzelm@37781
|
145 |
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
|
wenzelm@37781
|
146 |
|
wenzelm@37781
|
147 |
fun free_of s ((a, i), T) =
|
wenzelm@37781
|
148 |
Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
|
wenzelm@37781
|
149 |
|
wenzelm@37781
|
150 |
fun mk_inst v = (Var v, free_of "METAHYP1_" v)
|
wenzelm@37781
|
151 |
|
wenzelm@37781
|
152 |
fun metahyps_split_prem prem =
|
wenzelm@37781
|
153 |
let (*find all vars in the hyps -- should find tvars also!*)
|
wenzelm@37781
|
154 |
val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
|
wenzelm@37781
|
155 |
val insts = map mk_inst hyps_vars
|
wenzelm@37781
|
156 |
(*replace the hyps_vars by Frees*)
|
wenzelm@37781
|
157 |
val prem' = subst_atomic insts prem
|
wenzelm@37781
|
158 |
val (params,hyps,concl) = strip_context prem'
|
wenzelm@37781
|
159 |
in (insts,params,hyps,concl) end;
|
wenzelm@37781
|
160 |
|
wenzelm@37781
|
161 |
fun metahyps_aux_tac tacf (prem,gno) state =
|
wenzelm@37781
|
162 |
let val (insts,params,hyps,concl) = metahyps_split_prem prem
|
wenzelm@37781
|
163 |
val maxidx = Thm.maxidx_of state
|
wenzelm@37781
|
164 |
val cterm = Thm.cterm_of (Thm.theory_of_thm state)
|
wenzelm@37781
|
165 |
val chyps = map cterm hyps
|
wenzelm@37781
|
166 |
val hypths = map Thm.assume chyps
|
wenzelm@37781
|
167 |
val subprems = map (Thm.forall_elim_vars 0) hypths
|
wenzelm@37781
|
168 |
val fparams = map Free params
|
wenzelm@37781
|
169 |
val cparams = map cterm fparams
|
wenzelm@37781
|
170 |
fun swap_ctpair (t,u) = (cterm u, cterm t)
|
wenzelm@37781
|
171 |
(*Subgoal variables: make Free; lift type over params*)
|
wenzelm@37781
|
172 |
fun mk_subgoal_inst concl_vars (v, T) =
|
wenzelm@37781
|
173 |
if member (op =) concl_vars (v, T)
|
wenzelm@37781
|
174 |
then ((v, T), true, free_of "METAHYP2_" (v, T))
|
wenzelm@37781
|
175 |
else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
|
wenzelm@37781
|
176 |
(*Instantiate subgoal vars by Free applied to params*)
|
wenzelm@37781
|
177 |
fun mk_ctpair (v, in_concl, u) =
|
wenzelm@37781
|
178 |
if in_concl then (cterm (Var v), cterm u)
|
wenzelm@37781
|
179 |
else (cterm (Var v), cterm (list_comb (u, fparams)))
|
wenzelm@37781
|
180 |
(*Restore Vars with higher type and index*)
|
wenzelm@37781
|
181 |
fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
|
wenzelm@37781
|
182 |
if in_concl then (cterm u, cterm (Var ((a, i), T)))
|
wenzelm@37781
|
183 |
else (cterm u, cterm (Var ((a, i + maxidx), U)))
|
wenzelm@37781
|
184 |
(*Embed B in the original context of params and hyps*)
|
wenzelm@47086
|
185 |
fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
|
wenzelm@37781
|
186 |
(*Strip the context using elimination rules*)
|
wenzelm@37781
|
187 |
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
|
wenzelm@37781
|
188 |
(*A form of lifting that discharges assumptions.*)
|
wenzelm@37781
|
189 |
fun relift st =
|
wenzelm@37781
|
190 |
let val prop = Thm.prop_of st
|
wenzelm@37781
|
191 |
val subgoal_vars = (*Vars introduced in the subgoals*)
|
wenzelm@37781
|
192 |
fold Term.add_vars (Logic.strip_imp_prems prop) []
|
wenzelm@37781
|
193 |
and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
|
wenzelm@37781
|
194 |
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
|
wenzelm@37781
|
195 |
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
|
wenzelm@37781
|
196 |
val emBs = map (cterm o embed) (prems_of st')
|
wenzelm@37781
|
197 |
val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs)
|
wenzelm@37781
|
198 |
in (*restore the unknowns to the hypotheses*)
|
wenzelm@37781
|
199 |
free_instantiate (map swap_ctpair insts @
|
wenzelm@37781
|
200 |
map mk_subgoal_swap_ctpair subgoal_insts)
|
wenzelm@37781
|
201 |
(*discharge assumptions from state in same order*)
|
wenzelm@37781
|
202 |
(implies_intr_list emBs
|
wenzelm@37781
|
203 |
(forall_intr_list cparams (implies_intr_list chyps Cth)))
|
wenzelm@37781
|
204 |
end
|
wenzelm@37781
|
205 |
(*function to replace the current subgoal*)
|
wenzelm@37781
|
206 |
fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
|
wenzelm@37781
|
207 |
in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
|
wenzelm@37781
|
208 |
|
wenzelm@37781
|
209 |
fun print_vars_terms n thm =
|
wenzelm@37781
|
210 |
let
|
wenzelm@37781
|
211 |
val thy = theory_of_thm thm
|
wenzelm@37781
|
212 |
fun typed s ty =
|
wenzelm@37781
|
213 |
" " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
|
wenzelm@37781
|
214 |
fun find_vars (Const (c, ty)) =
|
wenzelm@37781
|
215 |
if null (Term.add_tvarsT ty []) then I
|
wenzelm@37781
|
216 |
else insert (op =) (typed c ty)
|
wenzelm@37781
|
217 |
| find_vars (Var (xi, ty)) =
|
wenzelm@37781
|
218 |
insert (op =) (typed (Term.string_of_vname xi) ty)
|
wenzelm@37781
|
219 |
| find_vars (Free _) = I
|
wenzelm@37781
|
220 |
| find_vars (Bound _) = I
|
wenzelm@37781
|
221 |
| find_vars (Abs (_, _, t)) = find_vars t
|
wenzelm@37781
|
222 |
| find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
|
wenzelm@37781
|
223 |
val prem = Logic.nth_prem (n, Thm.prop_of thm)
|
wenzelm@37781
|
224 |
val tms = find_vars prem []
|
wenzelm@37781
|
225 |
in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
|
wenzelm@37781
|
226 |
|
wenzelm@37781
|
227 |
in
|
wenzelm@37781
|
228 |
|
wenzelm@37781
|
229 |
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
|
wenzelm@37781
|
230 |
handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
|
wenzelm@37781
|
231 |
|
wenzelm@37781
|
232 |
end;
|
wenzelm@37781
|
233 |
|
wenzelm@47893
|
234 |
|
wenzelm@47893
|
235 |
(* generating identifiers -- often fresh *)
|
wenzelm@47893
|
236 |
|
wenzelm@47893
|
237 |
local
|
wenzelm@47893
|
238 |
(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
|
wenzelm@47893
|
239 |
fun gensym_char i =
|
wenzelm@47893
|
240 |
if i<26 then chr (ord "A" + i)
|
wenzelm@47893
|
241 |
else if i<52 then chr (ord "a" + i - 26)
|
wenzelm@47893
|
242 |
else chr (ord "0" + i - 52);
|
wenzelm@47893
|
243 |
|
wenzelm@47893
|
244 |
val char_vec = Vector.tabulate (62, gensym_char);
|
wenzelm@47893
|
245 |
fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
|
wenzelm@47893
|
246 |
|
wenzelm@47893
|
247 |
val gensym_seed = Unsynchronized.ref (0: int);
|
wenzelm@47893
|
248 |
|
wenzelm@47893
|
249 |
in
|
wenzelm@47893
|
250 |
fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
|
wenzelm@37781
|
251 |
end;
|
wenzelm@37781
|
252 |
|
wenzelm@47893
|
253 |
|
wenzelm@47893
|
254 |
(*Convert all Vars in a theorem to Frees. Also return a function for
|
wenzelm@47893
|
255 |
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*)
|
wenzelm@47893
|
256 |
|
wenzelm@47893
|
257 |
fun freeze_thaw_robust th =
|
wenzelm@47893
|
258 |
let val fth = Thm.legacy_freezeT th
|
wenzelm@47893
|
259 |
val thy = Thm.theory_of_thm fth
|
wenzelm@47893
|
260 |
in
|
wenzelm@47893
|
261 |
case Thm.fold_terms Term.add_vars fth [] of
|
haftmann@48447
|
262 |
[] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*)
|
wenzelm@47893
|
263 |
| vars =>
|
wenzelm@47893
|
264 |
let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
|
wenzelm@47893
|
265 |
val alist = map newName vars
|
wenzelm@47893
|
266 |
fun mk_inst (v,T) =
|
wenzelm@47893
|
267 |
(cterm_of thy (Var(v,T)),
|
wenzelm@47893
|
268 |
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
|
wenzelm@47893
|
269 |
val insts = map mk_inst vars
|
wenzelm@47893
|
270 |
fun thaw i th' = (*i is non-negative increment for Var indexes*)
|
wenzelm@47893
|
271 |
th' |> forall_intr_list (map #2 insts)
|
wenzelm@47893
|
272 |
|> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
|
wenzelm@47893
|
273 |
in (Thm.instantiate ([],insts) fth, thaw) end
|
wenzelm@47893
|
274 |
end;
|
wenzelm@47893
|
275 |
|
wenzelm@47893
|
276 |
(*Basic version of the function above. No option to rename Vars apart in thaw.
|
wenzelm@47893
|
277 |
The Frees created from Vars have nice names.*)
|
wenzelm@47893
|
278 |
fun freeze_thaw th =
|
wenzelm@47893
|
279 |
let val fth = Thm.legacy_freezeT th
|
wenzelm@47893
|
280 |
val thy = Thm.theory_of_thm fth
|
wenzelm@47893
|
281 |
in
|
wenzelm@47893
|
282 |
case Thm.fold_terms Term.add_vars fth [] of
|
wenzelm@47893
|
283 |
[] => (fth, fn x => x)
|
wenzelm@47893
|
284 |
| vars =>
|
wenzelm@47893
|
285 |
let fun newName (ix, _) (pairs, used) =
|
wenzelm@47893
|
286 |
let val v = singleton (Name.variant_list used) (string_of_indexname ix)
|
wenzelm@47893
|
287 |
in ((ix,v)::pairs, v::used) end;
|
wenzelm@47893
|
288 |
val (alist, _) =
|
wenzelm@47893
|
289 |
fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
|
wenzelm@47893
|
290 |
fun mk_inst (v, T) =
|
wenzelm@47893
|
291 |
(cterm_of thy (Var(v,T)),
|
wenzelm@47893
|
292 |
cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
|
wenzelm@47893
|
293 |
val insts = map mk_inst vars
|
wenzelm@47893
|
294 |
fun thaw th' =
|
wenzelm@47893
|
295 |
th' |> forall_intr_list (map #2 insts)
|
wenzelm@47893
|
296 |
|> forall_elim_list (map #1 insts)
|
wenzelm@47893
|
297 |
in (Thm.instantiate ([],insts) fth, thaw) end
|
wenzelm@47893
|
298 |
end;
|
wenzelm@47893
|
299 |
|
wenzelm@47893
|
300 |
end;
|
wenzelm@47893
|
301 |
|