# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260286540 -3600
# Node ID d23416464f621e2704e95ea8478b227f86e6991e
# Parent  a11b9b757f89aa2695a14b9bd1156cd110c8f508
added methods for the lifting_tac and the other tacs

diff -r a11b9b757f89 -r d23416464f62 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 14:00:48 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 16:35:40 2009 +0100
@@ -141,10 +141,10 @@
 done
 
 lemma "PLUS a b = PLUS a b"
-apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *}) 
+apply(lifting_setup rule: test1)
+apply(regularize)
+apply(injection)
+apply(cleaning)
 done
 
 thm lambda_prs
diff -r a11b9b757f89 -r d23416464f62 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 14:00:48 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 16:35:40 2009 +0100
@@ -359,8 +359,8 @@
 *}
 
 ML {*
-(* produces a regularized version of rtm      *)
-(* - the result is still not completely typed *)
+(* produces a regularized version of rtrm     *)
+(* - the result is contains dummyT            *)
 (* - does not need any special treatment of   *)
 (*   bound variables                          *)
 
@@ -370,8 +370,7 @@
        let
          val subtrm = Abs(x, ty, regularize_trm lthy t t')
        in
-         if ty = ty'
-         then subtrm
+         if ty = ty' then subtrm
          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
        end
 
@@ -395,8 +394,7 @@
 
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
-         if ty = ty'
-         then rtrm
+         if ty = ty' then rtrm
          else mk_resp_arg lthy (domain_type ty, domain_type ty') 
 
   | (* in this case we check whether the given equivalence relation is correct *) 
@@ -407,8 +405,7 @@
          val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
        in 
          if rel' = rel
-         then rtrm
-         else raise exc
+         then rtrm else raise exc
        end  
   | (_, Const (s, _)) =>
        let 
@@ -438,12 +435,11 @@
        raise (LIFT_MATCH "regularize (frees)")
 
   | (Bound i, Bound i') =>
-       if i = i' 
-       then rtrm 
+       if i = i' then rtrm 
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
   | (rt, qt) =>
-       raise (LIFT_MATCH "regularize (default)")
+       raise (LIFT_MATCH "regularize failed (default)")
 *}
 
 section {* Regularize Tactic *}
@@ -1156,5 +1152,36 @@
                     (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
+ML {*
+val rule_spec =  Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm
+
+(* FIXME: if the argument order changes then this can be just one function *)
+fun mk_method1 tac thm ctxt =
+  SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) 
+
+fun mk_method2 tac ctxt =
+  SIMPLE_METHOD (HEADGOAL (tac ctxt)) 
+*}
+
+method_setup lifting =
+  {* rule_spec >> (mk_method1 lift_tac) *}
+  {* Lifting of theorems to quotient types. *}
+
+method_setup lifting_setup =
+  {* rule_spec >> (mk_method1 procedure_tac) *}
+  {* Sets up the three goals for the lifting procedure. *}
+
+method_setup regularize =
+  {* Scan.succeed (mk_method2 regularize_tac)  *}
+  {* Proves automatically the regularization goals from the lifting procedure. *}
+
+method_setup injection =
+  {* Scan.succeed (mk_method2 all_inj_repabs_tac) *}
+  {* Proves automatically the rep/abs injection goals from the lifting procedure. *}
+
+method_setup cleaning =
+  {* Scan.succeed (mk_method2 clean_tac) *}
+  {* Proves automatically the cleaning goals from the lifting procedure. *}
+
 end