--- a/src/Tools/IsaPlanner/isand.ML Thu May 30 17:10:13 2013 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Thu May 30 17:21:11 2013 +0200
@@ -23,9 +23,6 @@
signature ISA_ND =
sig
- (* inserting meta level params for frees in the conditions *)
- val allify_conditions: (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
-
val variant_names: Proof.context -> term list -> string list -> string list
(* meta level fixed params (i.e. !! vars) *)
@@ -40,29 +37,6 @@
structure IsaND : ISA_ND =
struct
-(* Given ctertmify function, (string,type) pairs capturing the free
-vars that need to be allified in the assumption, and a theorem with
-assumptions possibly containing the free vars, then we give back the
-assumptions allified as hidden hyps.
-
-Given: x
-th: A vs ==> B vs
-Results in: "B vs" [!!x. A x]
-*)
-fun allify_conditions ctermify Ts th =
- let
- val premts = Thm.prems_of th;
-
- fun allify_prem_var (vt as (n, ty)) t =
- Logic.all_const ty $ Abs (n, ty, Term.abstract_over (Free vt, t))
-
- val allify_prem = fold_rev allify_prem_var
-
- val cTs = map (ctermify o Free) Ts
- val cterm_asms = map (ctermify o allify_prem Ts) premts
- val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
- in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
-
(* make free vars into schematic vars with index zero *)
fun unfix_frees frees =
fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
--- a/src/Tools/IsaPlanner/rw_inst.ML Thu May 30 17:10:13 2013 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Thu May 30 17:21:11 2013 +0200
@@ -21,6 +21,28 @@
structure RW_Inst: RW_INST =
struct
+(* Given (string,type) pairs capturing the free vars that need to be
+allified in the assumption, and a theorem with assumptions possibly
+containing the free vars, then we give back the assumptions allified
+as hidden hyps.
+
+Given: x
+th: A vs ==> B vs
+Results in: "B vs" [!!x. A x]
+*)
+fun allify_conditions Ts th =
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_thm th);
+
+ fun allify (x, T) t =
+ Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
+
+ val cTs = map (cert o Free) Ts;
+ val cterm_asms = map (cert o fold_rev allify Ts) (Thm.prems_of th);
+ val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
+ in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
+
+
(* Given a list of variables that were bound, and a that has been
instantiated with free variable placeholders for the bound vars, it
creates an abstracted version of the theorem, with local bound vars as
@@ -62,7 +84,7 @@
|> Drule.forall_elim_list tonames;
(* make unconditional rule and prems *)
- val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule';
+ val (uncond_rule, cprems) = allify_conditions (rev Ts') rule';
(* using these names create lambda-abstracted version of the rule *)
val abstractions = rev (Ts' ~~ tonames);