20 val term_vars: term -> term list |
20 val term_vars: term -> term list |
21 val add_term_frees: term * term list -> term list |
21 val add_term_frees: term * term list -> term list |
22 val term_frees: term -> term list |
22 val term_frees: term -> term list |
23 val mk_defpair: term * term -> string * term |
23 val mk_defpair: term * term -> string * term |
24 val get_def: theory -> xstring -> thm |
24 val get_def: theory -> xstring -> thm |
25 val METAHYPS: (thm list -> tactic) -> int -> tactic |
25 val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic |
26 val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) |
26 val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) |
27 val freeze_thaw: thm -> thm * (thm -> thm) |
27 val freeze_thaw: thm -> thm * (thm -> thm) |
28 end; |
28 end; |
29 |
29 |
30 structure Misc_Legacy: MISC_LEGACY = |
30 structure Misc_Legacy: MISC_LEGACY = |
156 (*replace the hyps_vars by Frees*) |
156 (*replace the hyps_vars by Frees*) |
157 val prem' = subst_atomic insts prem |
157 val prem' = subst_atomic insts prem |
158 val (params,hyps,concl) = strip_context prem' |
158 val (params,hyps,concl) = strip_context prem' |
159 in (insts,params,hyps,concl) end; |
159 in (insts,params,hyps,concl) end; |
160 |
160 |
161 fun metahyps_aux_tac tacf (prem,gno) state = |
161 fun metahyps_aux_tac ctxt tacf (prem,gno) state = |
162 let val (insts,params,hyps,concl) = metahyps_split_prem prem |
162 let val (insts,params,hyps,concl) = metahyps_split_prem prem |
163 val maxidx = Thm.maxidx_of state |
163 val maxidx = Thm.maxidx_of state |
164 val cterm = Thm.cterm_of (Thm.theory_of_thm state) |
164 val cterm = Thm.cterm_of (Thm.theory_of_thm state) |
165 val chyps = map cterm hyps |
165 val chyps = map cterm hyps |
166 val hypths = map Thm.assume chyps |
166 val hypths = map Thm.assume chyps |
202 (implies_intr_list emBs |
202 (implies_intr_list emBs |
203 (forall_intr_list cparams (implies_intr_list chyps Cth))) |
203 (forall_intr_list cparams (implies_intr_list chyps Cth))) |
204 end |
204 end |
205 (*function to replace the current subgoal*) |
205 (*function to replace the current subgoal*) |
206 fun next st = |
206 fun next st = |
207 Thm.bicompose NONE {flatten = true, match = false, incremented = false} |
207 Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} |
208 (false, relift st, nprems_of st) gno state |
208 (false, relift st, nprems_of st) gno state |
209 in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end; |
209 in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end; |
210 |
210 |
211 fun print_vars_terms n thm = |
211 fun print_vars_terms ctxt n thm = |
212 let |
212 let |
213 val thy = theory_of_thm thm |
213 fun typed s ty = " " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty; |
214 fun typed s ty = |
|
215 " " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty; |
|
216 fun find_vars (Const (c, ty)) = |
214 fun find_vars (Const (c, ty)) = |
217 if null (Term.add_tvarsT ty []) then I |
215 if null (Term.add_tvarsT ty []) then I |
218 else insert (op =) (typed c ty) |
216 else insert (op =) (typed c ty) |
219 | find_vars (Var (xi, ty)) = |
217 | find_vars (Var (xi, ty)) = |
220 insert (op =) (typed (Term.string_of_vname xi) ty) |
218 insert (op =) (typed (Term.string_of_vname xi) ty) |
226 val tms = find_vars prem [] |
224 val tms = find_vars prem [] |
227 in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end; |
225 in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end; |
228 |
226 |
229 in |
227 in |
230 |
228 |
231 fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm |
229 fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm |
232 handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty) |
230 handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty) |
233 |
231 |
234 end; |
232 end; |
235 |
233 |
236 |
234 |
237 (* generating identifiers -- often fresh *) |
235 (* generating identifiers -- often fresh *) |