lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)

--- a/src/Provers/eqsubst.ML	Fri May 13 19:55:09 2005 +0200
+++ b/src/Provers/eqsubst.ML	Fri May 13 20:21:41 2005 +0200
@@ -27,6 +27,9 @@
 signature EQSUBST_TAC = 
 sig
 
+  exception eqsubst_occL_exp of 
+            string * (int list) * (Thm.thm list) * int * Thm.thm;
+
   type match = 
        ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *)
         * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *)
@@ -273,9 +276,29 @@
 
     in (stepthms :-> rewrite_with_thm) end;
 
+(* Tactic.distinct_subgoals_tac *)
+
+(* custom version of distinct subgoals that works with term and 
+   type variables. Asssumes th is in beta-eta normal form. 
+   Also, does nothing if flexflex contraints are present. *)
+fun distinct_subgoals th =
+    if List.null (Thm.tpairs_of th) then
+      let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
+        val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
+      in
+        IsaND.unfix_frees_and_tfrees 
+          fixes
+          (Drule.implies_intr_list 
+             (Library.gen_distinct 
+                (fn (x, y) => Thm.term_of x = Thm.term_of y)
+                cprems) fixedthconcl)
+      end
+    else th;
 
 (* General substiuttion of multiple occurances using one of 
    the given theorems*)
+exception eqsubst_occL_exp of 
+          string * (int list) * (Thm.thm list) * int * Thm.thm;
 fun eqsubst_occL tac occL thms i th = 
     let val nprems = Thm.nprems_of th in
       if nprems < i then Seq.empty else
@@ -287,10 +310,15 @@
                                  (i + ((Thm.nprems_of th) - nprems))
                                  th);
       in
-        Seq.EVERY (map apply_occ (Library.sort (Library.rev_order o Library.int_ord) occL)) 
-                  th
+        Seq.map distinct_subgoals
+                (Seq.EVERY (map apply_occ 
+                                (Library.sort (Library.rev_order 
+                                               o Library.int_ord) occL)) th)
       end
-    end;
+    end
+    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
+
+        
 
 (* implicit argus: occL thms i th *)
 val eqsubst_tac = eqsubst_occL eqsubst_tac';

--- a/src/Pure/IsaPlanner/isand.ML	Fri May 13 19:55:09 2005 +0200
+++ b/src/Pure/IsaPlanner/isand.ML	Fri May 13 20:21:41 2005 +0200
@@ -208,7 +208,9 @@
     let 
       val sign = Thm.sign_of_thm th;
       val ctypify = Thm.ctyp_of sign;
-      val renamings = fix_tvars_to_tfrees_in_terms [] [Thm.prop_of th];
+      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
+      val renamings = fix_tvars_to_tfrees_in_terms 
+                        [] ((Thm.prop_of th) :: tpairs);
       val crenamings = 
           map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
               renamings;
@@ -237,7 +239,9 @@
 fun fix_vars_to_frees th = 
     let 
       val ctermify = Thm.cterm_of (Thm.sign_of_thm th)
-      val renamings = fix_vars_to_frees_in_terms [] [Thm.prop_of th];
+      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
+      val renamings = fix_vars_to_frees_in_terms 
+                        [] ([Thm.prop_of th] @ tpairs);
       val crenamings = 
           map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
               renamings;
@@ -248,8 +252,9 @@
     let 
       val sgn = Thm.sign_of_thm th;
       val ctypify = Thm.ctyp_of sgn
+      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
       val prop = (Thm.prop_of th);
-      val tvars = Term.term_tvars prop;
+      val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
       val ctyfixes = 
           Library.mapfilter 
             (fn (v as ((s,i),ty)) => 
@@ -260,8 +265,10 @@
     let 
       val sgn = Thm.sign_of_thm th;
       val ctermify = Thm.cterm_of sgn
+      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
       val prop = (Thm.prop_of th);
-      val vars = map Term.dest_Var (Term.term_vars prop);
+      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
+                                               [] (prop :: tpairs));
       val cfixes = 
           Library.mapfilter 
             (fn (v as ((s,i),ty)) => 
@@ -282,8 +289,10 @@
     in ((vars, tvars), th'') end;
 
 (* implicit Thm.thm argument *)
+(* assumes: vars may contain fixed versions of the frees *)
+(* THINK: what if vs already has types varified? *)
 fun unfix_frees_and_tfrees (vs,tvs) = 
-    (unfix_frees vs o unfix_tfrees tvs);
+    (unfix_tfrees tvs o unfix_frees vs);
 
 (* datatype to capture an exported result, ie a fix or assume. *)
 datatype export = 

--- a/src/Pure/IsaPlanner/rw_inst.ML	Fri May 13 19:55:09 2005 +0200
+++ b/src/Pure/IsaPlanner/rw_inst.ML	Fri May 13 20:21:41 2005 +0200
@@ -201,13 +201,15 @@
     in cross_instL (insts, []) end;
 
 
-(* assume that rule and target_thm have distinct var names *)
-(* THINK: efficient version with tables for vars for: target vars,
-introduced vars, and rule vars, for quicker instantiation? *)
-(* The outerterm defines which part of the target_thm was modified *)
-(* Note: we take Ts in the upterm order, ie last abstraction first.,
-and with an outeterm where the abstracted subterm has the arguments in
-the revered order, ie first abstraction first. *)
+(* assume that rule and target_thm have distinct var names. THINK:
+efficient version with tables for vars for: target vars, introduced
+vars, and rule vars, for quicker instantiation?  The outerterm defines
+which part of the target_thm was modified.  Note: we take Ts in the
+upterm order, ie last abstraction first., and with an outeterm where
+the abstracted subterm has the arguments in the revered order, ie
+first abstraction first.  FakeTs has abstractions using the fake name
+- ie the name distinct from all other abstractions. *)
+
 fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
     let 
       (* general signature info *)
@@ -219,12 +221,14 @@
       val (fixtyinsts, othertfrees) = 
           mk_fixtvar_tyinsts nonfixed_typinsts
                              [Thm.prop_of rule, Thm.prop_of target_thm];
-          
+      val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
+                               fixtyinsts;
       val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
 
       (* certified instantiations for types *)
       val ctyp_insts = 
-          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) typinsts;
+          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
+              typinsts;
 
       (* type instantiated versions *)
       val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
@@ -234,6 +238,11 @@
       (* type instanitated outer term *)
       val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
 
+      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
+                              FakeTs;
+      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
+                          Ts;
+
       (* type-instantiate the var instantiations *)
       val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
                             (ix, (Term.typ_subst_TVars term_typ_inst ty, 
@@ -268,7 +277,7 @@
       val couter_inst = Thm.reflexive (ctermify outerterm_inst);
       val (cprems, abstract_rule_inst) = 
           rule_inst |> Thm.instantiate ([], cterm_renamings)
-                    |> mk_abstractedrule FakeTs Ts;
+                    |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
       val specific_tgt_rule = 
           beta_eta_contract
             (Thm.combination couter_inst abstract_rule_inst);