tuned signature;
authorwenzelm
Thu May 30 17:21:11 2013 +0200 (2013-05-30)
changeset 52245f76fb8858e0b
parent 52244 cb15da7bd550
child 52246 54c0d4128b30
tuned signature;
tuned;
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:10:13 2013 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu May 30 17:21:11 2013 +0200
     1.3 @@ -23,9 +23,6 @@
     1.4  
     1.5  signature ISA_ND =
     1.6  sig
     1.7 -  (* inserting meta level params for frees in the conditions *)
     1.8 -  val allify_conditions: (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
     1.9 -
    1.10    val variant_names: Proof.context -> term list -> string list -> string list
    1.11  
    1.12    (* meta level fixed params (i.e. !! vars) *)
    1.13 @@ -40,29 +37,6 @@
    1.14  structure IsaND : ISA_ND =
    1.15  struct
    1.16  
    1.17 -(* Given ctertmify function, (string,type) pairs capturing the free
    1.18 -vars that need to be allified in the assumption, and a theorem with
    1.19 -assumptions possibly containing the free vars, then we give back the
    1.20 -assumptions allified as hidden hyps.
    1.21 -
    1.22 -Given: x
    1.23 -th: A vs ==> B vs
    1.24 -Results in: "B vs" [!!x. A x]
    1.25 -*)
    1.26 -fun allify_conditions ctermify Ts th =
    1.27 -  let
    1.28 -    val premts = Thm.prems_of th;
    1.29 -
    1.30 -    fun allify_prem_var (vt as (n, ty)) t =
    1.31 -      Logic.all_const ty $ Abs (n, ty, Term.abstract_over (Free vt, t))
    1.32 -
    1.33 -    val allify_prem = fold_rev allify_prem_var
    1.34 -
    1.35 -    val cTs = map (ctermify o Free) Ts
    1.36 -    val cterm_asms = map (ctermify o allify_prem Ts) premts
    1.37 -    val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
    1.38 -  in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    1.39 -
    1.40  (* make free vars into schematic vars with index zero *)
    1.41  fun unfix_frees frees =
    1.42     fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
     2.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 17:10:13 2013 +0200
     2.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 17:21:11 2013 +0200
     2.3 @@ -21,6 +21,28 @@
     2.4  structure RW_Inst: RW_INST =
     2.5  struct
     2.6  
     2.7 +(* Given (string,type) pairs capturing the free vars that need to be
     2.8 +allified in the assumption, and a theorem with assumptions possibly
     2.9 +containing the free vars, then we give back the assumptions allified
    2.10 +as hidden hyps.
    2.11 +
    2.12 +Given: x
    2.13 +th: A vs ==> B vs
    2.14 +Results in: "B vs" [!!x. A x]
    2.15 +*)
    2.16 +fun allify_conditions Ts th =
    2.17 +  let
    2.18 +    val cert = Thm.cterm_of (Thm.theory_of_thm th);
    2.19 +
    2.20 +    fun allify (x, T) t =
    2.21 +      Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
    2.22 +
    2.23 +    val cTs = map (cert o Free) Ts;
    2.24 +    val cterm_asms = map (cert o fold_rev allify Ts) (Thm.prems_of th);
    2.25 +    val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
    2.26 +  in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    2.27 +
    2.28 +
    2.29  (* Given a list of variables that were bound, and a that has been
    2.30  instantiated with free variable placeholders for the bound vars, it
    2.31  creates an abstracted version of the theorem, with local bound vars as
    2.32 @@ -62,7 +84,7 @@
    2.33        |> Drule.forall_elim_list tonames;
    2.34  
    2.35      (* make unconditional rule and prems *)
    2.36 -    val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule';
    2.37 +    val (uncond_rule, cprems) = allify_conditions (rev Ts') rule';
    2.38  
    2.39      (* using these names create lambda-abstracted version of the rule *)
    2.40      val abstractions = rev (Ts' ~~ tonames);