src/Pure/IsaPlanner/rw_inst.ML
changeset 15959 366d39e95d3c
parent 15915 b0e8b37642a4
child 16179 fa7e70be26b0
     1.1 --- a/src/Pure/IsaPlanner/rw_inst.ML	Fri May 13 19:55:09 2005 +0200
     1.2 +++ b/src/Pure/IsaPlanner/rw_inst.ML	Fri May 13 20:21:41 2005 +0200
     1.3 @@ -201,13 +201,15 @@
     1.4      in cross_instL (insts, []) end;
     1.5  
     1.6  
     1.7 -(* assume that rule and target_thm have distinct var names *)
     1.8 -(* THINK: efficient version with tables for vars for: target vars,
     1.9 -introduced vars, and rule vars, for quicker instantiation? *)
    1.10 -(* The outerterm defines which part of the target_thm was modified *)
    1.11 -(* Note: we take Ts in the upterm order, ie last abstraction first.,
    1.12 -and with an outeterm where the abstracted subterm has the arguments in
    1.13 -the revered order, ie first abstraction first. *)
    1.14 +(* assume that rule and target_thm have distinct var names. THINK:
    1.15 +efficient version with tables for vars for: target vars, introduced
    1.16 +vars, and rule vars, for quicker instantiation?  The outerterm defines
    1.17 +which part of the target_thm was modified.  Note: we take Ts in the
    1.18 +upterm order, ie last abstraction first., and with an outeterm where
    1.19 +the abstracted subterm has the arguments in the revered order, ie
    1.20 +first abstraction first.  FakeTs has abstractions using the fake name
    1.21 +- ie the name distinct from all other abstractions. *)
    1.22 +
    1.23  fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
    1.24      let 
    1.25        (* general signature info *)
    1.26 @@ -219,12 +221,14 @@
    1.27        val (fixtyinsts, othertfrees) = 
    1.28            mk_fixtvar_tyinsts nonfixed_typinsts
    1.29                               [Thm.prop_of rule, Thm.prop_of target_thm];
    1.30 -          
    1.31 +      val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
    1.32 +                               fixtyinsts;
    1.33        val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
    1.34  
    1.35        (* certified instantiations for types *)
    1.36        val ctyp_insts = 
    1.37 -          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) typinsts;
    1.38 +          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
    1.39 +              typinsts;
    1.40  
    1.41        (* type instantiated versions *)
    1.42        val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
    1.43 @@ -234,6 +238,11 @@
    1.44        (* type instanitated outer term *)
    1.45        val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
    1.46  
    1.47 +      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
    1.48 +                              FakeTs;
    1.49 +      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
    1.50 +                          Ts;
    1.51 +
    1.52        (* type-instantiate the var instantiations *)
    1.53        val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
    1.54                              (ix, (Term.typ_subst_TVars term_typ_inst ty, 
    1.55 @@ -268,7 +277,7 @@
    1.56        val couter_inst = Thm.reflexive (ctermify outerterm_inst);
    1.57        val (cprems, abstract_rule_inst) = 
    1.58            rule_inst |> Thm.instantiate ([], cterm_renamings)
    1.59 -                    |> mk_abstractedrule FakeTs Ts;
    1.60 +                    |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
    1.61        val specific_tgt_rule = 
    1.62            beta_eta_contract
    1.63              (Thm.combination couter_inst abstract_rule_inst);