# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1277711316 -7200
# Node ID a47bb386b2382fd4c9cf5a3106791b0e45be2e71
# Parent  6cf28a1dfd75eca2c74e2e011265735c4c1f1408
Quotient package reverse lifting

diff -r 6cf28a1dfd75 -r a47bb386b238 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Mon Jun 28 07:38:39 2010 +0200
+++ b/src/HOL/Quotient.thy	Mon Jun 28 09:48:36 2010 +0200
@@ -768,7 +768,7 @@
   {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
-  {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
+  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
   {* sets up the three goals for the quotient lifting procedure *}
 
 method_setup regularize =
diff -r 6cf28a1dfd75 -r a47bb386b238 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jun 28 07:38:39 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jun 28 09:48:36 2010 +0200
@@ -49,7 +49,8 @@
 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
 let
   val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
-  val _ = if is_Const rhs then () else error "The definiens should be a constant"
+  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+  val _ = if is_Const rhs then () else warning "The definiens is not a constant"
   
   fun sanity_test NONE _ = true
     | sanity_test (SOME bind) str =
diff -r 6cf28a1dfd75 -r a47bb386b238 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jun 28 07:38:39 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jun 28 09:48:36 2010 +0200
@@ -11,7 +11,7 @@
   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 -> int -> tactic
+  val procedure_tac: Proof.context -> thm list -> 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
@@ -620,12 +620,23 @@
   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)
+    case rthm of
+      [] =>
+        let
+          val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+          val rtrm = derive_qtrm qtys goal true ctxt
+          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")
 
 
 (* Automatic Proofs *)
@@ -633,14 +644,24 @@
 fun lift_tac ctxt rthms =
 let
   fun mk_tac rthm =
-    procedure_tac ctxt rthm
+    procedure_tac ctxt [rthm]
     THEN' RANGE
       [regularize_tac ctxt,
        all_injection_tac ctxt,
+       clean_tac ctxt];
+  val mk_tac_raw =
+    procedure_tac ctxt []
+    THEN' RANGE
+      [fn _ => all_tac,
+       regularize_tac ctxt,
+       all_injection_tac ctxt,
        clean_tac ctxt]
 in
   simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
-  THEN' RANGE (map mk_tac rthms)
+  THEN'
+    (case rthms of
+      [] => mk_tac_raw
+    | _ => RANGE (map mk_tac rthms))
 end
 
 fun lifted qtys ctxt thm =
diff -r 6cf28a1dfd75 -r a47bb386b238 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 07:38:39 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 09:48:36 2010 +0200
@@ -759,9 +759,9 @@
      |> map (fn (x, y) => if reverse then (y, x) else (x, y))
 
   val rel_substs =
-    if reverse then [] else
     Quotient_Info.quotdata_dest ctxt
      |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
+     |> map (fn (x, y) => if reverse then (y, x) else (x, y))
 in
   filter proper (const_substs @ rel_substs)
 end