# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265363149 -3600
# Node ID 62e54830590f300672e8503f3d4e712684253dd6
# Parent  3664eafcad0940fee8e5d38bb6813ba571d418a4
A proper version of the attribute

diff -r 3664eafcad09 -r 62e54830590f Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Feb 04 18:09:20 2010 +0100
+++ b/Quot/QuotMain.thy	Fri Feb 05 10:45:49 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
 
diff -r 3664eafcad09 -r 62e54830590f Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Feb 04 18:09:20 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Feb 05 10:45:49 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 =
@@ -658,4 +659,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 *)