src/Pure/thm.ML

--- a/src/Pure/thm.ML	Tue Sep 12 12:12:55 2006 +0200
+++ b/src/Pure/thm.ML	Tue Sep 12 12:12:57 2006 +0200
@@ -15,6 +15,7 @@
    {thy: theory,
     sign: theory,       (*obsolete*)
     T: typ,
+    maxidx: int,
     sorts: sort list}
   val theory_of_ctyp: ctyp -> theory
   val typ_of: ctyp -> typ
@@ -186,26 +187,34 @@
 
 (** certified types **)
 
-datatype ctyp = Ctyp of {thy_ref: theory_ref, T: typ, sorts: sort list};
+datatype ctyp = Ctyp of
+ {thy_ref: theory_ref,
+  T: typ,
+  maxidx: int,
+  sorts: sort list};
 
-fun rep_ctyp (Ctyp {thy_ref, T, sorts}) =
+fun rep_ctyp (Ctyp {thy_ref, T, maxidx, sorts}) =
   let val thy = Theory.deref thy_ref
-  in {thy = thy, sign = thy, T = T, sorts = sorts} end;
+  in {thy = thy, sign = thy, T = T, maxidx = maxidx, sorts = sorts} end;
 
 fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
 
 fun typ_of (Ctyp {T, ...}) = T;
 
 fun ctyp_of thy raw_T =
-  let val T = Sign.certify_typ thy raw_T
-  in Ctyp {thy_ref = Theory.self_ref thy, T = T, sorts = may_insert_typ_sorts thy T []} end;
+  let val T = Sign.certify_typ thy raw_T in
+    Ctyp {thy_ref = Theory.self_ref thy, T = T,
+      maxidx = Term.maxidx_of_typ T, sorts = may_insert_typ_sorts thy T []}
+  end;
 
 fun read_ctyp thy s =
-  let val T = Sign.read_typ (thy, K NONE) s
-  in Ctyp {thy_ref = Theory.self_ref thy, T = T, sorts = may_insert_typ_sorts thy T []} end;
+  let val T = Sign.read_typ (thy, K NONE) s in
+    Ctyp {thy_ref = Theory.self_ref thy, T = T,
+      maxidx = Term.maxidx_of_typ T, sorts = may_insert_typ_sorts thy T []}
+  end;
 
-fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), sorts}) =
-      map (fn T => Ctyp {thy_ref = thy_ref, T = T, sorts = sorts}) Ts
+fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), maxidx, sorts}) =
+      map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts
   | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
 
 
@@ -228,15 +237,16 @@
 
 fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
   let val thy = Theory.deref thy_ref in
-   {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T, sorts = sorts},
+   {thy = thy, sign = thy, t = t,
+      T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts},
     maxidx = maxidx, sorts = sorts}
   end;
 
 fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
 fun term_of (Cterm {t, ...}) = t;
 
-fun ctyp_of_term (Cterm {thy_ref, T, sorts, ...}) =
-  Ctyp {thy_ref = thy_ref, T = T, sorts = sorts};
+fun ctyp_of_term (Cterm {thy_ref, T, maxidx, sorts, ...}) =
+  Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts};
 
 fun cterm_of thy tm =
   let
@@ -295,20 +305,19 @@
 
 (*Matching of cterms*)
 fun gen_cterm_match match
-    (ct1 as Cterm {t = t1, maxidx = maxidx1, sorts = sorts1, ...},
-     ct2 as Cterm {t = t2, maxidx = maxidx2, sorts = sorts2, ...}) =
+    (ct1 as Cterm {t = t1, sorts = sorts1, ...},
+     ct2 as Cterm {t = t2, sorts = sorts2, ...}) =
   let
     val thy_ref = merge_thys0 ct1 ct2;
     val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2) (Vartab.empty, Vartab.empty);
-    val maxidx = Int.max (maxidx1, maxidx2);
     val sorts = Sorts.union sorts1 sorts2;
-    fun mk_cTinst (ixn, (S, T)) =
-      (Ctyp {T = TVar (ixn, S), thy_ref = thy_ref, sorts = sorts},
-       Ctyp {T = T, thy_ref = thy_ref, sorts = sorts});
-    fun mk_ctinst (ixn, (T, t)) =
+    fun mk_cTinst ((a, i), (S, T)) =
+      (Ctyp {T = TVar ((a, i), S), thy_ref = thy_ref, maxidx = i, sorts = sorts},
+       Ctyp {T = T, thy_ref = thy_ref, maxidx = Term.maxidx_of_typ T, sorts = sorts});
+    fun mk_ctinst ((x, i), (T, t)) =
       let val T = Envir.typ_subst_TVars Tinsts T in
-        (Cterm {t = Var (ixn, T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
-         Cterm {t = t, T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
+        (Cterm {t = Var ((x, i), T), T = T, thy_ref = thy_ref, maxidx = i, sorts = sorts},
+         Cterm {t = t, T = T, thy_ref = thy_ref, maxidx = Term.maxidx_of_term t, sorts = sorts})
       end;
   in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;
 
@@ -676,8 +685,8 @@
     fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
   in
     case prop of
-      imp $ A $ B =>
-        if imp = Term.implies andalso A aconv propA then
+      Const ("==>", _) $ A $ B =>
+        if A aconv propA then
           Thm {thy_ref = merge_thys2 thAB thA,
             der = Pt.infer_derivs (curry Pt.%%) der derA,
             maxidx = Int.max (maxA, maxidx),
@@ -1001,7 +1010,7 @@
         val _ = exists bad_term hyps andalso
           raise THM ("generalize: variable free in assumptions", 0, [th]);
 
-        val gen = Term.generalize (tfrees, frees) idx;
+        val gen = TermSubst.generalize (tfrees, frees) idx;
         val prop' = gen prop;
         val tpairs' = map (pairself gen) tpairs;
         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
@@ -1031,12 +1040,12 @@
 fun add_inst (ct, cu) (thy_ref, sorts) =
   let
     val Cterm {t = t, T = T, ...} = ct
-    and Cterm {t = u, T = U, sorts = sorts_u, ...} = cu;
+    and Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
     val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu);
     val sorts' = Sorts.union sorts_u sorts;
   in
     (case t of Var v =>
-      if T = U then ((v, u), (thy_ref', sorts'))
+      if T = U then ((v, (u, maxidx_u)), (thy_ref', sorts'))
       else raise TYPE (Pretty.string_of (Pretty.block
        [Pretty.str "instantiate: type conflict",
         Pretty.fbrk, pretty_typing (Theory.deref thy_ref') t T,
@@ -1049,13 +1058,13 @@
 fun add_instT (cT, cU) (thy_ref, sorts) =
   let
     val Ctyp {T, thy_ref = thy_ref1, ...} = cT
-    and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, ...} = cU;
+    and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
     val thy_ref' = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2));
     val thy' = Theory.deref thy_ref';
     val sorts' = Sorts.union sorts_U sorts;
   in
     (case T of TVar (v as (_, S)) =>
-      if Sign.of_sort thy' (U, S) then ((v, U), (thy_ref', sorts'))
+      if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy_ref', sorts'))
       else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], [])
     | _ => raise TYPE (Pretty.string_of (Pretty.block
         [Pretty.str "instantiate: not a type variable",
@@ -1073,9 +1082,10 @@
         val Thm {thy_ref, der, hyps, shyps, tpairs, prop, ...} = th;
         val (inst', (instT', (thy_ref', shyps'))) =
           (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
-        val subst = Term.instantiate (instT', inst');
-        val prop' = subst prop;
-        val tpairs' = map (pairself subst) tpairs;
+        val subst = TermSubst.instantiate_maxidx (instT', inst');
+        val (prop', maxidx1) = subst prop ~1;
+        val (tpairs', maxidx') =
+          fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
       in
         if has_duplicates (fn ((v, _), (v', _)) => Term.eq_var (v, v')) inst' then
           raise THM ("instantiate: variables not distinct", 0, [th])
@@ -1083,8 +1093,9 @@
           raise THM ("instantiate: type variables not distinct", 0, [th])
         else
           Thm {thy_ref = thy_ref',
-            der = Pt.infer_derivs' (Pt.instantiate (instT', inst')) der,
-            maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
+            der = Pt.infer_derivs' (fn d =>
+              Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
+            maxidx = maxidx',
             shyps = shyps',
             hyps = hyps,
             tpairs = tpairs',