tuned instantiate (avoid subst_atomic, subst_atomic_types);
authorwenzelm
Tue Jul 19 17:21:56 2005 +0200 (2005-07-19)
changeset 168841678a796b6b2
parent 16883 a89fafe1cbd8
child 16885 cabcd33cde18
tuned instantiate (avoid subst_atomic, subst_atomic_types);
Logic.incr_tvar;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Tue Jul 19 17:21:55 2005 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Jul 19 17:21:56 2005 +0200
     1.3 @@ -309,7 +309,7 @@
     1.4    if i < 0 then raise CTERM "negative increment"
     1.5    else if i = 0 then ct
     1.6    else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t,
     1.7 -    T = Term.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
     1.8 +    T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
     1.9  
    1.10  
    1.11  
    1.12 @@ -374,7 +374,7 @@
    1.13  
    1.14  fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
    1.15  val union_tpairs = gen_merge_lists eq_tpairs;
    1.16 -val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t o Term.maxidx_term u);
    1.17 +val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u);
    1.18  
    1.19  fun attach_tpairs tpairs prop =
    1.20    Logic.list_implies (map Logic.mk_equals tpairs, prop);
    1.21 @@ -897,7 +897,7 @@
    1.22          let
    1.23            val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
    1.24              (*remove trivial tpairs, of the form t==t*)
    1.25 -            |> List.filter (not o op aconv);
    1.26 +            |> filter_out (op aconv);
    1.27            val prop' = Envir.norm_term env prop;
    1.28          in
    1.29            Thm {thy_ref = thy_ref,
    1.30 @@ -921,29 +921,34 @@
    1.31  fun pretty_typing thy t T =
    1.32    Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T];
    1.33  
    1.34 -fun add_ctpair ((thy, sorts), (ct, cu)) =
    1.35 +fun add_inst (ct, cu) (thy_ref, sorts) =
    1.36    let
    1.37 -    val Cterm {t = t, T = T, sorts = sorts1, ...} = ct
    1.38 -    and Cterm {t = u, T = U, sorts = sorts2, ...} = cu;
    1.39 -    val thy' = Theory.merge (thy, Theory.deref (merge_thys0 ct cu));
    1.40 -    val sorts' = Sorts.union sorts2 (Sorts.union sorts1 sorts);
    1.41 +    val Cterm {t = t, T = T, ...} = ct
    1.42 +    and Cterm {t = u, T = U, sorts = sorts_u, ...} = cu;
    1.43 +    val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu);
    1.44 +    val sorts' = Sorts.union sorts_u sorts;
    1.45    in
    1.46 -    if T = U then ((thy', sorts'), (t, u))
    1.47 -    else raise TYPE (Pretty.string_of (Pretty.block
    1.48 -     [Pretty.str "instantiate: type conflict",
    1.49 -      Pretty.fbrk, pretty_typing thy' t T,
    1.50 -      Pretty.fbrk, pretty_typing thy' u U]), [T,U], [t,u])
    1.51 +    (case t of Var v =>
    1.52 +      if T = U then ((v, u), (thy_ref', sorts'))
    1.53 +      else raise TYPE (Pretty.string_of (Pretty.block
    1.54 +       [Pretty.str "instantiate: type conflict",
    1.55 +        Pretty.fbrk, pretty_typing (Theory.deref thy_ref') t T,
    1.56 +        Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u])
    1.57 +    | _ => raise TYPE (Pretty.string_of (Pretty.block
    1.58 +       [Pretty.str "instantiate: not a variable",
    1.59 +        Pretty.fbrk, Sign.pretty_term (Theory.deref thy_ref') t]), [], [t]))
    1.60    end;
    1.61  
    1.62 -fun add_ctyp ((thy, sorts), (cT, cU)) =
    1.63 +fun add_instT (cT, cU) (thy_ref, sorts) =
    1.64    let
    1.65 -    val Ctyp {T, thy_ref = thy_ref1, sorts = sorts1, ...} = cT
    1.66 -    and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts2, ...} = cU;
    1.67 -    val thy' = Theory.merge (thy, Theory.deref (Theory.merge_refs (thy_ref1, thy_ref2)));
    1.68 -    val sorts' = Sorts.union sorts2 (Sorts.union sorts1 sorts);
    1.69 +    val Ctyp {T, thy_ref = thy_ref1, ...} = cT
    1.70 +    and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, ...} = cU;
    1.71 +    val thy_ref' = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2));
    1.72 +    val thy' = Theory.deref thy_ref';
    1.73 +    val sorts' = Sorts.union sorts_U sorts;
    1.74    in
    1.75 -    (case T of TVar (_, S) =>
    1.76 -      if Type.of_sort (Sign.tsig_of thy') (U, S) then ((thy', sorts'), (T, U))
    1.77 +    (case T of TVar (v as (_, S)) =>
    1.78 +      if Type.of_sort (Sign.tsig_of thy') (U, S) then ((v, U), (thy_ref', sorts'))
    1.79        else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], [])
    1.80      | _ => raise TYPE (Pretty.string_of (Pretty.block
    1.81          [Pretty.str "instantiate: not a type variable",
    1.82 @@ -956,26 +961,26 @@
    1.83    Instantiates distinct Vars by terms of same type.
    1.84    Does NOT normalize the resulting theorem!*)
    1.85  fun instantiate ([], []) th = th
    1.86 -  | instantiate (vcTs, ctpairs) th =
    1.87 +  | instantiate (instT, inst) th =
    1.88        let
    1.89 -        val Thm {thy_ref, der, hyps, shyps, tpairs = dpairs, prop, ...} = th;
    1.90 -        val (context, tpairs) = foldl_map add_ctpair ((Theory.deref thy_ref, shyps), ctpairs);
    1.91 -        val ((thy', shyps'), vTs) = foldl_map add_ctyp (context, vcTs);
    1.92 -        fun subst t = subst_atomic tpairs (subst_atomic_types vTs t);
    1.93 +        val Thm {thy_ref, der, hyps, shyps, tpairs, prop, ...} = th;
    1.94 +        val (inst', (instT', (thy_ref', shyps'))) =
    1.95 +          (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
    1.96 +        val subst = Term.instantiate (instT', inst');
    1.97          val prop' = subst prop;
    1.98 -        val dpairs' = map (pairself subst) dpairs;
    1.99 +        val tpairs' = map (pairself subst) tpairs;
   1.100        in
   1.101 -        if not (forall (is_Var o #1) tpairs andalso null (gen_duplicates eq_fst tpairs)) then
   1.102 +        if has_duplicates (fn ((v, _), (v', _)) => Term.eq_var (v, v')) inst' then
   1.103            raise THM ("instantiate: variables not distinct", 0, [th])
   1.104 -        else if not (null (gen_duplicates eq_fst vTs)) then
   1.105 +        else if has_duplicates (fn ((v, _), (v', _)) => Term.eq_tvar (v, v')) instT' then
   1.106            raise THM ("instantiate: type variables not distinct", 0, [th])
   1.107          else
   1.108 -          Thm {thy_ref = Theory.self_ref thy',
   1.109 -            der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der,
   1.110 -            maxidx = maxidx_tpairs dpairs' (maxidx_of_term prop'),
   1.111 +          Thm {thy_ref = thy_ref',
   1.112 +            der = Pt.infer_derivs' (Pt.instantiate (instT', inst')) der,
   1.113 +            maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
   1.114              shyps = shyps',
   1.115              hyps = hyps,
   1.116 -            tpairs = dpairs',
   1.117 +            tpairs = tpairs',
   1.118              prop = prop'}
   1.119        end
   1.120        handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
   1.121 @@ -1083,7 +1088,8 @@
   1.122    else if i = 0 then thm
   1.123    else
   1.124      Thm {thy_ref = thy_ref,
   1.125 -      der = Pt.infer_derivs' (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i)) der,
   1.126 +      der = Pt.infer_derivs'
   1.127 +        (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
   1.128        maxidx = maxidx + i,
   1.129        shyps = shyps,
   1.130        hyps = hyps,