# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265447096 -3600
# Node ID 44461d5615eb02e148443dffe4fb739cd4894ab2
# Parent  9a3d2a4f895605884537c21a59888e28dc218ad2
some tuning

diff -r 9a3d2a4f8956 -r 44461d5615eb Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Fri Feb 05 15:17:21 2010 +0100
+++ b/Quot/QuotMain.thy	Sat Feb 06 10:04:56 2010 +0100
@@ -181,7 +181,7 @@
   {* Proves automatically the cleaning goals from the lifting procedure. *}
 
 attribute_setup quot_lifted =
-  {* Scan.succeed Quotient_Tacs.lifted_attr *}
+  {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   {* Lifting of theorems to quotient types. *}
 
 end
diff -r 9a3d2a4f8956 -r 44461d5615eb Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Feb 05 15:17:21 2010 +0100
+++ b/Quot/quotient_tacs.ML	Sat Feb 06 10:04:56 2010 +0100
@@ -15,7 +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
+  val lifted_attrib: attribute
 end;
 
 structure Quotient_Tacs: QUOTIENT_TACS =
@@ -648,15 +648,19 @@
   THEN' RANGE (map mk_tac rthms)
 end
 
-(* The attribute *)
-fun lifted_attr_pre ctxt thm =
+(* An Attribute *)
+(* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *)
+fun lifted_attrib_pre context thm =
 let
-  val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
-  val glc = Syntax.check_term ctxt gl
+  val ctxt = Context.proof_of context
+  val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
+  val goal_chk = Syntax.check_term ctxt goal
+  val frees = Term.add_free_names goal_chk []
 in
-  (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1))
+  Goal.prove ctxt frees [] goal_chk 
+   (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)
+val lifted_attrib = Thm.rule_attribute lifted_attrib_pre
 
 end; (* structure *)
diff -r 9a3d2a4f8956 -r 44461d5615eb Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Feb 05 15:17:21 2010 +0100
+++ b/Quot/quotient_term.ML	Sat Feb 06 10:04:56 2010 +0100
@@ -473,18 +473,14 @@
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Ex1"}, ty) $ 
-      (Abs (n, _,
-        (Const (@{const_name "op &"}, _) $ 
-          (Const (@{const_name "op :"}, _) $ _ $ (Const (@{const_name "Respects"}, _) $ resrel)) $ 
-          (t $ _)
-        )
-      )), Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
+      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ 
+        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), 
+     Const (@{const_name "Ex1"}, ty') $ t') =>
        let
-         val t = incr_boundvars (~1) t
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+         val t_ = incr_boundvars (~1) t
+         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
-         val _ = tracing "bla"
        in
          if resrel <> needrel
          then term_mismatch "regularize (Bex1)" ctxt resrel needrel
@@ -689,19 +685,27 @@
   inj_repabs_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
 
-(*** Translating the goal automatically
+
+
+(*** Wrapper for transforming an rthm into a qthm ***)
 
+(*
 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 *)
+  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
@@ -715,6 +719,7 @@
     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 =
@@ -727,7 +732,7 @@
   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))
+  (ty_substs, const_substs @ rel_substs)
 end
 
 fun quotient_lift_all ctxt t =
@@ -745,7 +750,7 @@
             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')))
+            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)