37781
|
1 |
(* Title: Tools/misc_legacy.ML
|
|
2 |
|
|
3 |
Misc legacy stuff -- to be phased out eventually.
|
|
4 |
*)
|
|
5 |
|
|
6 |
signature MISC_LEGACY =
|
|
7 |
sig
|
44121
|
8 |
val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
|
|
9 |
val add_term_names: term * string list -> string list
|
|
10 |
val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
|
|
11 |
val add_typ_tfree_names: typ * string list -> string list
|
|
12 |
val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
|
|
13 |
val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
|
|
14 |
val add_term_tfrees: term * (string * sort) list -> (string * sort) list
|
|
15 |
val add_term_tfree_names: term * string list -> string list
|
|
16 |
val typ_tfrees: typ -> (string * sort) list
|
|
17 |
val typ_tvars: typ -> (indexname * sort) list
|
|
18 |
val term_tfrees: term -> (string * sort) list
|
|
19 |
val term_tvars: term -> (indexname * sort) list
|
|
20 |
val add_term_vars: term * term list -> term list
|
|
21 |
val term_vars: term -> term list
|
|
22 |
val add_term_frees: term * term list -> term list
|
|
23 |
val term_frees: term -> term list
|
37781
|
24 |
val mk_defpair: term * term -> string * term
|
|
25 |
val get_def: theory -> xstring -> thm
|
|
26 |
val simple_read_term: theory -> typ -> string -> term
|
|
27 |
val METAHYPS: (thm list -> tactic) -> int -> tactic
|
|
28 |
end;
|
|
29 |
|
|
30 |
structure Misc_Legacy: MISC_LEGACY =
|
|
31 |
struct
|
|
32 |
|
44121
|
33 |
(*iterate a function over all types in a term*)
|
|
34 |
fun it_term_types f =
|
|
35 |
let fun iter(Const(_,T), a) = f(T,a)
|
|
36 |
| iter(Free(_,T), a) = f(T,a)
|
|
37 |
| iter(Var(_,T), a) = f(T,a)
|
|
38 |
| iter(Abs(_,T,t), a) = iter(t,f(T,a))
|
|
39 |
| iter(f$u, a) = iter(f, iter(u, a))
|
|
40 |
| iter(Bound _, a) = a
|
|
41 |
in iter end
|
|
42 |
|
|
43 |
(*Accumulates the names in the term, suppressing duplicates.
|
|
44 |
Includes Frees and Consts. For choosing unambiguous bound var names.*)
|
|
45 |
fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
|
|
46 |
| add_term_names (Free(a,_), bs) = insert (op =) a bs
|
|
47 |
| add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
|
|
48 |
| add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
|
|
49 |
| add_term_names (_, bs) = bs;
|
|
50 |
|
|
51 |
(*Accumulates the TVars in a type, suppressing duplicates.*)
|
|
52 |
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
|
|
53 |
| add_typ_tvars(TFree(_),vs) = vs
|
|
54 |
| add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
|
|
55 |
|
|
56 |
(*Accumulates the TFrees in a type, suppressing duplicates.*)
|
|
57 |
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
|
|
58 |
| add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
|
|
59 |
| add_typ_tfree_names(TVar(_),fs) = fs;
|
|
60 |
|
|
61 |
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
|
|
62 |
| add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
|
|
63 |
| add_typ_tfrees(TVar(_),fs) = fs;
|
|
64 |
|
|
65 |
(*Accumulates the TVars in a term, suppressing duplicates.*)
|
|
66 |
val add_term_tvars = it_term_types add_typ_tvars;
|
|
67 |
|
|
68 |
(*Accumulates the TFrees in a term, suppressing duplicates.*)
|
|
69 |
val add_term_tfrees = it_term_types add_typ_tfrees;
|
|
70 |
val add_term_tfree_names = it_term_types add_typ_tfree_names;
|
|
71 |
|
|
72 |
(*Non-list versions*)
|
|
73 |
fun typ_tfrees T = add_typ_tfrees(T,[]);
|
|
74 |
fun typ_tvars T = add_typ_tvars(T,[]);
|
|
75 |
fun term_tfrees t = add_term_tfrees(t,[]);
|
|
76 |
fun term_tvars t = add_term_tvars(t,[]);
|
|
77 |
|
|
78 |
|
|
79 |
(*Accumulates the Vars in the term, suppressing duplicates.*)
|
|
80 |
fun add_term_vars (t, vars: term list) = case t of
|
|
81 |
Var _ => Ord_List.insert Term_Ord.term_ord t vars
|
|
82 |
| Abs (_,_,body) => add_term_vars(body,vars)
|
|
83 |
| f$t => add_term_vars (f, add_term_vars(t, vars))
|
|
84 |
| _ => vars;
|
|
85 |
|
|
86 |
fun term_vars t = add_term_vars(t,[]);
|
|
87 |
|
|
88 |
(*Accumulates the Frees in the term, suppressing duplicates.*)
|
|
89 |
fun add_term_frees (t, frees: term list) = case t of
|
|
90 |
Free _ => Ord_List.insert Term_Ord.term_ord t frees
|
|
91 |
| Abs (_,_,body) => add_term_frees(body,frees)
|
|
92 |
| f$t => add_term_frees (f, add_term_frees(t, frees))
|
|
93 |
| _ => frees;
|
|
94 |
|
|
95 |
fun term_frees t = add_term_frees(t,[]);
|
|
96 |
|
|
97 |
|
37781
|
98 |
fun mk_defpair (lhs, rhs) =
|
|
99 |
(case Term.head_of lhs of
|
|
100 |
Const (name, _) =>
|
|
101 |
(Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
|
|
102 |
| _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
|
|
103 |
|
|
104 |
|
|
105 |
fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
|
|
106 |
|
|
107 |
|
|
108 |
fun simple_read_term thy T s =
|
|
109 |
let
|
42361
|
110 |
val ctxt = Proof_Context.init_global thy
|
|
111 |
|> Proof_Context.allow_dummies
|
|
112 |
|> Proof_Context.set_mode Proof_Context.mode_schematic;
|
37781
|
113 |
val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
|
39288
|
114 |
in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
|
37781
|
115 |
|
|
116 |
|
|
117 |
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
|
|
118 |
METAHYPS (fn prems => tac prems) i
|
|
119 |
|
|
120 |
converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
|
|
121 |
proof state A==>A, supplying A1,...,An as meta-level assumptions (in
|
|
122 |
"prems"). The parameters x1,...,xm become free variables. If the
|
|
123 |
resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
|
|
124 |
then it is lifted back into the original context, yielding k subgoals.
|
|
125 |
|
|
126 |
Replaces unknowns in the context by Frees having the prefix METAHYP_
|
|
127 |
New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
|
|
128 |
DOES NOT HANDLE TYPE UNKNOWNS.
|
|
129 |
|
|
130 |
|
|
131 |
NOTE: This version does not observe the proof context, and thus cannot
|
|
132 |
work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for
|
|
133 |
properly localized variants of the same idea.
|
|
134 |
****)
|
|
135 |
|
|
136 |
local
|
|
137 |
|
|
138 |
(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B )
|
|
139 |
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters.
|
|
140 |
Main difference from strip_assums concerns parameters:
|
|
141 |
it replaces the bound variables by free variables. *)
|
|
142 |
fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
|
|
143 |
strip_context_aux (params, H :: Hs, B)
|
|
144 |
| strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
|
42284
|
145 |
let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
|
37781
|
146 |
in strip_context_aux ((b, T) :: params, Hs, u) end
|
|
147 |
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
|
|
148 |
|
|
149 |
fun strip_context A = strip_context_aux ([], [], A);
|
|
150 |
|
|
151 |
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
|
|
152 |
Instantiates distinct free variables by terms of same type.*)
|
|
153 |
fun free_instantiate ctpairs =
|
|
154 |
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
|
|
155 |
|
|
156 |
fun free_of s ((a, i), T) =
|
|
157 |
Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
|
|
158 |
|
|
159 |
fun mk_inst v = (Var v, free_of "METAHYP1_" v)
|
|
160 |
|
|
161 |
fun metahyps_split_prem prem =
|
|
162 |
let (*find all vars in the hyps -- should find tvars also!*)
|
|
163 |
val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
|
|
164 |
val insts = map mk_inst hyps_vars
|
|
165 |
(*replace the hyps_vars by Frees*)
|
|
166 |
val prem' = subst_atomic insts prem
|
|
167 |
val (params,hyps,concl) = strip_context prem'
|
|
168 |
in (insts,params,hyps,concl) end;
|
|
169 |
|
|
170 |
fun metahyps_aux_tac tacf (prem,gno) state =
|
|
171 |
let val (insts,params,hyps,concl) = metahyps_split_prem prem
|
|
172 |
val maxidx = Thm.maxidx_of state
|
|
173 |
val cterm = Thm.cterm_of (Thm.theory_of_thm state)
|
|
174 |
val chyps = map cterm hyps
|
|
175 |
val hypths = map Thm.assume chyps
|
|
176 |
val subprems = map (Thm.forall_elim_vars 0) hypths
|
|
177 |
val fparams = map Free params
|
|
178 |
val cparams = map cterm fparams
|
|
179 |
fun swap_ctpair (t,u) = (cterm u, cterm t)
|
|
180 |
(*Subgoal variables: make Free; lift type over params*)
|
|
181 |
fun mk_subgoal_inst concl_vars (v, T) =
|
|
182 |
if member (op =) concl_vars (v, T)
|
|
183 |
then ((v, T), true, free_of "METAHYP2_" (v, T))
|
|
184 |
else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
|
|
185 |
(*Instantiate subgoal vars by Free applied to params*)
|
|
186 |
fun mk_ctpair (v, in_concl, u) =
|
|
187 |
if in_concl then (cterm (Var v), cterm u)
|
|
188 |
else (cterm (Var v), cterm (list_comb (u, fparams)))
|
|
189 |
(*Restore Vars with higher type and index*)
|
|
190 |
fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
|
|
191 |
if in_concl then (cterm u, cterm (Var ((a, i), T)))
|
|
192 |
else (cterm u, cterm (Var ((a, i + maxidx), U)))
|
|
193 |
(*Embed B in the original context of params and hyps*)
|
|
194 |
fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
|
|
195 |
(*Strip the context using elimination rules*)
|
|
196 |
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
|
|
197 |
(*A form of lifting that discharges assumptions.*)
|
|
198 |
fun relift st =
|
|
199 |
let val prop = Thm.prop_of st
|
|
200 |
val subgoal_vars = (*Vars introduced in the subgoals*)
|
|
201 |
fold Term.add_vars (Logic.strip_imp_prems prop) []
|
|
202 |
and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
|
|
203 |
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
|
|
204 |
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
|
|
205 |
val emBs = map (cterm o embed) (prems_of st')
|
|
206 |
val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs)
|
|
207 |
in (*restore the unknowns to the hypotheses*)
|
|
208 |
free_instantiate (map swap_ctpair insts @
|
|
209 |
map mk_subgoal_swap_ctpair subgoal_insts)
|
|
210 |
(*discharge assumptions from state in same order*)
|
|
211 |
(implies_intr_list emBs
|
|
212 |
(forall_intr_list cparams (implies_intr_list chyps Cth)))
|
|
213 |
end
|
|
214 |
(*function to replace the current subgoal*)
|
|
215 |
fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
|
|
216 |
in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
|
|
217 |
|
|
218 |
fun print_vars_terms n thm =
|
|
219 |
let
|
|
220 |
val thy = theory_of_thm thm
|
|
221 |
fun typed s ty =
|
|
222 |
" " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
|
|
223 |
fun find_vars (Const (c, ty)) =
|
|
224 |
if null (Term.add_tvarsT ty []) then I
|
|
225 |
else insert (op =) (typed c ty)
|
|
226 |
| find_vars (Var (xi, ty)) =
|
|
227 |
insert (op =) (typed (Term.string_of_vname xi) ty)
|
|
228 |
| find_vars (Free _) = I
|
|
229 |
| find_vars (Bound _) = I
|
|
230 |
| find_vars (Abs (_, _, t)) = find_vars t
|
|
231 |
| find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
|
|
232 |
val prem = Logic.nth_prem (n, Thm.prop_of thm)
|
|
233 |
val tms = find_vars prem []
|
|
234 |
in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
|
|
235 |
|
|
236 |
in
|
|
237 |
|
|
238 |
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
|
|
239 |
handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
|
|
240 |
|
|
241 |
end;
|
|
242 |
|
|
243 |
end;
|
|
244 |
|