--- a/Quot/Nominal/Nominal2_Eqvt.thy	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Fri Feb 05 14:52:27 2010 +0100
@@ -226,6 +226,8 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
+
+
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
@@ -233,8 +235,7 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  permute_eqvt supp_eqvt fresh_eqvt
-  permute_pure
+  supp_eqvt fresh_eqvt permute_pure
 
   (* datatypes *)
   permute_prod.simps
@@ -244,6 +245,8 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt
 
+lemmas [eqvt_raw] = permute_eqvt
+
 thm eqvts
 thm eqvts_raw
 

--- a/Quot/Nominal/nominal_permeq.ML	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/Nominal/nominal_permeq.ML	Fri Feb 05 14:52:27 2010 +0100
@@ -59,7 +59,7 @@
         then_conv Conv.comb_conv (eqvt_conv ctxt),
       eqvt_lambda_conv ctxt
         then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
-      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_raw_thms ctxt),
+      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),
       Conv.all_conv
     ] ct
 

--- a/Quot/Nominal/nominal_thmdecls.ML	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/Nominal/nominal_thmdecls.ML	Fri Feb 05 14:52:27 2010 +0100
@@ -3,18 +3,18 @@
 
   Infrastructure for the lemma collection "eqvts".
 
-  Provides the attributes [eqvt] and [eqvt_force], and the theorem
-  lists eqvts and eqvts_raw. The first attribute will store the theorem
-  in the eqvts list and also in the eqvts_raw list. For the latter 
-  the theorem is expected to be of the form
+  Provides the attributes [eqvt] and [eqvt_raw], and the theorem
+  lists eqvts and eqvts_raw. The first attribute will store the 
+  theorem in the eqvts list and also in the eqvts_raw list. For 
+  the latter the theorem is expected to be of the form
 
     p o (c x1 x2 ...) = c (p o x1) (p o x2) ...
 
-  and is stored in the form
+  and it is stored in the form
 
     p o c == c
 
-  The [eqvt_force] attribute just adds the theorem to eqvts.
+  The [eqvt_raw] attribute just adds the theorem to eqvts_raw.
 
   TODO:
 
@@ -27,36 +27,41 @@
 sig
   val eqvt_add: attribute
   val eqvt_del: attribute
-  val eqvt_force_add: attribute
-  val eqvt_force_del: attribute
+  val eqvt_raw_add: attribute
+  val eqvt_raw_del: attribute
   val setup: theory -> theory
-  val get_eqvt_thms: Proof.context -> thm list
-  val get_eqvt_raw_thms: Proof.context -> thm list
+  val get_eqvts_thms: Proof.context -> thm list
+  val get_eqvts_raw_thms: Proof.context -> thm list
 
 end;
 
 structure Nominal_ThmDecls: NOMINAL_THMDECLS =
 struct
 
+
 structure EqvtData = Generic_Data
-(
-  type T = (thm * thm option) Item_Net.T;
-  val empty = Item_Net.init (eq_fst Thm.eq_thm_prop) (single o Thm.full_prop_of o fst)
+( type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
   val extend = I;
-  val merge = Item_Net.merge;
-);
+  val merge = Item_Net.merge );
 
-val eqvts = (map fst) o Item_Net.content o EqvtData.get;
-val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get;
+structure EqvtRawData = Generic_Data
+( type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
+  val extend = I;
+  val merge = Item_Net.merge );
 
-val get_eqvt_thms = eqvts o Context.Proof; 
-val get_eqvt_raw_thms = eqvts_raw o Context.Proof; 
+val eqvts = Item_Net.content o EqvtData.get;
+val eqvts_raw = Item_Net.content o EqvtRawData.get;
+
+val get_eqvts_thms = eqvts o Context.Proof; 
+val get_eqvts_raw_thms = eqvts_raw o Context.Proof; 
 
 val add_thm = EqvtData.map o Item_Net.update;
 val del_thm = EqvtData.map o Item_Net.remove;
 
-val add_force_thm = EqvtData.map o Item_Net.update;
-val del_force_thm = EqvtData.map o Item_Net.remove;
+val add_raw_thm = EqvtRawData.map o Item_Net.update;
+val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM("dest_perm", [t])
@@ -94,7 +99,7 @@
     (fn _ => eqvt_transform_tac thm 1)
 end
 
-fun transform addel_fn thm context = 
+fun transform addel_fun thm context = 
 let
   val ctxt = Context.proof_of context
   val trm = HOLogic.dest_Trueprop (prop_of thm)
@@ -102,27 +107,28 @@
   case trm of
     Const (@{const_name "op ="}, _) $ lhs $ rhs =>
       let 
-        val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
+        val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
       in
-        addel_fn (thm, SOME thm2) context
+        addel_fun thm' context
       end
   | _ => raise (error "only (op=) case implemented yet")
 end 
 
-val eqvt_add = Thm.declaration_attribute (transform add_thm);
-val eqvt_del = Thm.declaration_attribute (transform del_thm);
+val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));
+val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm));
 
-val eqvt_force_add = Thm.declaration_attribute (add_force_thm o rpair NONE);
-val eqvt_force_del = Thm.declaration_attribute (del_force_thm o rpair NONE);
+val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
+val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;
 
 val setup =
   Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) 
     (cat_lines ["declaration of equivariance lemmas - they will automtically be",  
        "brought into the form p o c = c"]) #>
-  Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) 
+  Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) 
     (cat_lines ["declaration of equivariance lemmas - no",
        "transformation is performed"]) #>
   PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
   PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);
 
+
 end;

--- a/Quot/QuotMain.thy	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/QuotMain.thy	Fri Feb 05 14:52:27 2010 +0100
@@ -150,7 +150,6 @@
 text {* Tactics for proving the lifted theorems *}
 use "quotient_tacs.ML"
 
-
 section {* Methods / Interface *}
 
 ML {*
@@ -181,5 +180,9 @@
   {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
   {* Proves automatically the cleaning goals from the lifting procedure. *}
 
+attribute_setup quot_lifted =
+  {* Scan.succeed Quotient_Tacs.lifted_attr *}
+  {* Lifting of theorems to quotient types. *}
+
 end
 

--- a/Quot/quotient_tacs.ML	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Feb 05 14:52:27 2010 +0100
@@ -15,6 +15,7 @@
   val lift_tac: Proof.context -> thm list -> int -> tactic
   val quotient_tac: Proof.context -> int -> tactic
   val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
+  val lifted_attr: attribute
 end;
 
 structure Quotient_Tacs: QUOTIENT_TACS =
@@ -647,4 +648,15 @@
   THEN' RANGE (map mk_tac rthms)
 end
 
+(* The attribute *)
+fun lifted_attr_pre ctxt thm =
+let
+  val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
+  val glc = Syntax.check_term ctxt gl
+in
+  (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1))
+end;
+
+val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t)
+
 end; (* structure *)

--- a/Quot/quotient_term.ML	Fri Feb 05 10:32:21 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Feb 05 14:52:27 2010 +0100
@@ -689,48 +689,74 @@
   inj_repabs_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
 
-(* Finds subterms of a term that are lifted to constants and replaces
-   those as well as occurrences of the equivalence relation and replaces
-   those by equality.
-   Currently types are not checked so because of the dummyTs it may
-   not be complete *)
+(*** Translating the goal automatically
+
+Finds subterms of a term that can be lifted and:
+* replaces subterms matching lifted constants by the lifted constants
+* replaces equivalence relations by equalities
+* In constants, frees and schematic variables replaces
+  subtypes matching lifted types by those types *)
+
+fun subst_ty thy ty (rty, qty) r =
+  if r <> NONE then r else
+  case try (Sign.typ_match thy (ty, rty)) Vartab.empty of
+    SOME inst => SOME (Envir.subst_type inst qty)
+  | NONE => NONE
+fun subst_tys thy substs ty =
+  case fold (subst_ty thy ty) substs NONE of
+    SOME ty => ty
+  | NONE =>
+      (case ty of
+        Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
+      | x => x)
+
+fun subst_trm thy t (rt, qt) s =
+  if s <> NONE then s else
+    case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of
+      SOME inst => SOME (Envir.subst_term inst qt)
+    | NONE => NONE;
+fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
+
+fun get_ty_trm_substs ctxt =
+let
+  val thy = ProofContext.theory_of ctxt
+  val quot_infos = Quotient_Info.quotdata_dest ctxt
+  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
+  val const_infos = Quotient_Info.qconsts_dest ctxt
+  val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
+  fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
+  val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
+in
+  (ty_substs, (const_substs @ rel_substs))
+end
+
 fun quotient_lift_all ctxt t =
 let
   val thy = ProofContext.theory_of ctxt
-  val const_infos = Quotient_Info.qconsts_dest ctxt
-  val rel_infos = Quotient_Info.quotdata_dest ctxt
-  fun treat_const_info t qc_info s =
-    if s <> NONE then s else
-      case try (Pattern.match thy (t, #rconst qc_info)) (Vartab.empty, Vartab.empty) of
-        SOME inst => SOME (Envir.subst_term inst (#qconst qc_info))
-      | NONE => NONE;
-  fun treat_const t = fold (treat_const_info t) const_infos NONE
-  fun treat_rel_info t rel_info s =
-    if s <> NONE then s else
-    if Pattern.matches thy (t, #equiv_rel rel_info) then SOME (Const ("op =", dummyT))
-    else NONE
-  fun treat_rel t = fold (treat_rel_info t) rel_infos NONE
+  val (ty_substs, substs) = get_ty_trm_substs ctxt
   fun lift_aux t =
-    case treat_const t of
+    case subst_trms thy substs t of
       SOME x => x
     | NONE =>
-      (case treat_rel t of
-        SOME x => x
-      | NONE =>
-        (case t of
-          a $ b => lift_aux a $ lift_aux b
-        | Abs(a, T, s) =>
-            let val (y, s') = Term.dest_abs (a, T, s) in
-            Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s')))
-            end
-        | Free(n, _) => Free(n, dummyT)
-        | Var(n, _) => Var(n, dummyT)
-        | Bound i => Bound i
-        | Const(s, _) => Const(s, dummyT)))
+      (case t of
+        a $ b => lift_aux a $ lift_aux b
+      | Abs(a, ty, s) =>
+          let
+            val (y, s') = Term.dest_abs (a, ty, s)
+            val nty = subst_tys thy ty_substs ty
+          in
+          Abs(y, nty, abstract_over (Free (y, nty), (lift_aux s')))
+          end
+      | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
+      | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
+      | Bound i => Bound i
+      | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
 in
   lift_aux t
 end
 
+
+
 end; (* structure *)