# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277771909 -3600
# Node ID 2505feaf2d70f0f4df5b3639a2c7334f0751c7b1
# Parent  e16495cfdde058fc5e6d18e849ac8f32baf944d8
separated the lifting and descending procedures in the quotient package

diff -r e16495cfdde0 -r 2505feaf2d70 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Mon Jun 28 16:20:39 2010 +0100
+++ b/src/HOL/Quotient.thy	Tue Jun 29 01:38:29 2010 +0100
@@ -764,13 +764,23 @@
 subsection {* Methods / Interface *}
 
 method_setup lifting =
-  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
+  {* Attrib.thms >> (fn thms => fn ctxt => 
+       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
   {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
-  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
+  {* Attrib.thm >> (fn thm => fn ctxt => 
+       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
   {* sets up the three goals for the quotient lifting procedure *}
 
+method_setup descending =
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
+  {* decends theorems to the raw level *}
+
+method_setup descending_setup =
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
+  {* sets up the three goals for the decending theorems *}
+
 method_setup regularize =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
   {* proves the regularization goals from the quotient lifting procedure *}
diff -r e16495cfdde0 -r 2505feaf2d70 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jun 28 16:20:39 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Jun 29 01:38:29 2010 +0100
@@ -11,10 +11,13 @@
   val injection_tac: Proof.context -> int -> tactic
   val all_injection_tac: Proof.context -> int -> tactic
   val clean_tac: Proof.context -> int -> tactic
-  val procedure_tac: Proof.context -> thm list -> int -> tactic
+  
+  val descend_procedure_tac: Proof.context -> int -> tactic
+  val descend_tac: Proof.context -> int -> tactic
+ 
+  val lift_procedure_tac: Proof.context -> thm -> int -> tactic
   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: typ list -> Proof.context -> thm -> thm
   val lifted_attrib: attribute
 end;
@@ -615,55 +618,64 @@
      SOME (cterm_of thy inj_goal)] lifting_procedure_thm
 end
 
-(* the tactic leaves three subgoals to be proved *)
-fun procedure_tac ctxt rthm =
+
+(** descending as tactic **)
+
+fun descend_procedure_tac ctxt =
   Object_Logic.full_atomize_tac
   THEN' gen_frees_tac ctxt
   THEN' SUBGOAL (fn (goal, i) =>
-    case rthm of
-      [] =>
         let
           val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
           val rtrm = derive_rtrm qtys goal ctxt
-          val rule = procedure_inst ctxt rtrm goal
+          val rule = procedure_inst ctxt rtrm  goal
         in
           rtac rule i
-        end
-    | [rthm'] =>
-        let
-          val rthm'' = atomize_thm rthm'
-          val rule = procedure_inst ctxt (prop_of rthm'') goal
-        in
-          (rtac rule THEN' rtac rthm'') i
-        end
-    | _ => error "more than one raw theorem given")
+        end)
+
+fun descend_tac ctxt =
+let
+  val mk_tac_raw =
+    descend_procedure_tac ctxt
+    THEN' RANGE
+      [Object_Logic.rulify_tac THEN' (K all_tac),
+       regularize_tac ctxt,
+       all_injection_tac ctxt,
+       clean_tac ctxt]
+in
+  Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
+end
 
 
-(* Automatic Proofs *)
+(** lifting as tactic **)
+
+(* the tactic leaves three subgoals to be proved *)
+fun lift_procedure_tac ctxt rthm =
+  Object_Logic.full_atomize_tac
+  THEN' gen_frees_tac ctxt
+  THEN' SUBGOAL (fn (goal, i) =>
+    let
+      val rthm' = atomize_thm rthm
+      val rule = procedure_inst ctxt (prop_of rthm') goal
+    in
+      (rtac rule THEN' rtac rthm') i
+    end)
 
 fun lift_tac ctxt rthms =
 let
   fun mk_tac rthm =
-    procedure_tac ctxt [rthm]
-    THEN' RANGE
-      [regularize_tac ctxt,
-       all_injection_tac ctxt,
-       clean_tac ctxt];
-  val mk_tac_raw =
-    procedure_tac ctxt []
+    lift_procedure_tac ctxt rthm
     THEN' RANGE
-      [fn _ => all_tac,
-       regularize_tac ctxt,
-       all_injection_tac ctxt,
-       clean_tac ctxt]
+      [ regularize_tac ctxt,
+        all_injection_tac ctxt,
+        clean_tac ctxt ]
 in
-  simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
-  THEN'
-    (case rthms of
-      [] => mk_tac_raw
-    | _ => RANGE (map mk_tac rthms))
+  Goal.conjunction_tac THEN' RANGE (map mk_tac rthms)
 end
 
+
+(** lifting as attribute **)
+
 fun lifted qtys ctxt thm =
 let
   (* When the theorem is atomized, eta redexes are contracted,
@@ -676,15 +688,12 @@
   |> singleton (ProofContext.export ctxt' ctxt)
 end;
 
-(* An attribute which automatically constructs the qthm 
-   using all quotients defined so far.
-*)
 val lifted_attrib = Thm.rule_attribute (fn context => 
-       let
-         val ctxt = Context.proof_of context
-         val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
-       in
-         lifted qtys ctxt
-       end)
+  let
+    val ctxt = Context.proof_of context
+    val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+  in
+    lifted qtys ctxt
+  end)
 
 end; (* structure *)