merged

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 25 18:38:49 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 25 18:46:22 2010 +0200
@@ -310,7 +310,7 @@
 
 
 
-(* Injection means to prove that the regularised theorem implies
+(* Injection means to prove that the regularized theorem implies
    the abs/rep injected one.
 
    The deterministic part:
@@ -541,8 +541,7 @@
 end
 
 
-
-(** Tactic for Generalising Free Variables in a Goal **)
+(* Tactic for Generalising Free Variables in a Goal *)
 
 fun inst_spec ctrm =
    Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
@@ -649,13 +648,20 @@
 
 (** lifting as a 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
+      (* full_atomize_tac contracts eta redexes,
+         so we do it also in the original theorem *)
+      val rthm' = 
+        rthm |> Drule.eta_contraction_rule 
+             |> Thm.forall_intr_frees
+             |> atomize_thm 
+
       val rule = procedure_inst ctxt (prop_of rthm') goal
     in
       (rtac rule THEN' rtac rthm') i
@@ -679,18 +685,13 @@
 fun lifted ctxt qtys simps rthm =
 let
   val ss = (mk_minimal_ss ctxt) addsimps simps
+  val rthm' = asm_full_simplify ss rthm
 
-  (* When the theorem is atomized, eta redexes are contracted,
-     so we do it both in the original theorem *)
-  val rthm' =
-    rthm 
-    |> asm_full_simplify ss
-    |> Drule.eta_contraction_rule 
   val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
   val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
 in
   Goal.prove ctxt' [] [] goal 
-    (K ((asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm') 1))
+    (K (EVERY1 [asm_full_simp_tac ss, lift_single_tac ctxt' rthm'']))
   |> singleton (ProofContext.export ctxt' ctxt)
 end
 

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Wed Aug 25 18:38:49 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Wed Aug 25 18:46:22 2010 +0200
@@ -68,7 +68,7 @@
 let
   val thy = ProofContext.theory_of ctxt
   val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
-  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
+  val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exn
 in
   Const (mapfun, dummyT)
 end
@@ -105,7 +105,7 @@
 let
   val thy = ProofContext.theory_of ctxt
   val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
+  val qdata = quotdata_lookup thy s handle NotFound => raise exn
 in
   (#rtyp qdata, #qtyp qdata)
 end
@@ -277,7 +277,7 @@
 let
   val thy = ProofContext.theory_of ctxt
   val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
-  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
+  val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exn
 in
   Const (relmap, dummyT)
 end
@@ -301,7 +301,7 @@
   val thy = ProofContext.theory_of ctxt
   val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
 in
-  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+  #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exn
 end
 
 fun equiv_match_err ctxt ty_pat ty =
@@ -436,7 +436,7 @@
         if length rtys <> length qtys then false else
         forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
       else
-        (case Quotient_Info.quotdata_lookup_raw thy qs of
+        (case quotdata_lookup_raw thy qs of
           SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
         | NONE => false)
   | _ => false
@@ -446,7 +446,7 @@
 
    - the result might contain dummyTs
 
-   - for regularisation we do not need any
+   - for regularization we do not need any
      special treatment of bound variables
 *)
 fun regularize_trm ctxt (rtrm, qtrm) =
@@ -550,7 +550,7 @@
          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
        in
          if rel' aconv rel then rtrm
-         else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
+         else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
        end
 
   | (_, Const _) =>
@@ -563,10 +563,10 @@
          else
            let
              val rtrm' = #rconst (qconsts_lookup thy qtrm)
-               handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
+               handle NotFound => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
            in
              if Pattern.matches thy (rtrm', rtrm)
-             then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
+             then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
            end
        end
 
@@ -751,7 +751,7 @@
 let
   val thy = ProofContext.theory_of ctxt  
 in
-  Quotient_Info.quotdata_dest ctxt
+  quotdata_dest ctxt
    |> map (fn x => (#rtyp x, #qtyp x))
    |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
    |> map (if direction then swap else I)
@@ -763,12 +763,12 @@
   fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
 
   val const_substs = 
-    Quotient_Info.qconsts_dest ctxt
+    qconsts_dest ctxt
      |> map (fn x => (#rconst x, #qconst x))
      |> map (if direction then swap else I)
 
   val rel_substs =
-    Quotient_Info.quotdata_dest ctxt
+    quotdata_dest ctxt
      |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
      |> map (if direction then swap else I)
 in