# HG changeset patch
# User huffman
# Date 1333542440 -7200
# Node ID fc7de207e488560eb3bc5dc08e57978c0b43fff8
# Parent  e0bff2ae939faa8c533715b0d299b16fd9fd3cd4# Parent  803729c9fd4dc20b14110268d4b078321fd6fcab
merged

diff -r 803729c9fd4d -r fc7de207e488 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Apr 04 14:08:24 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed Apr 04 14:27:20 2012 +0200
@@ -273,6 +273,11 @@
   show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
 qed
 
+lemma Quotient_to_transfer:
+  assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
+  shows "T c c'"
+  using assms by (auto dest: Quotient_cr_rel)
+
 subsection {* ML setup *}
 
 text {* Auxiliary data for the lifting package *}
diff -r 803729c9fd4d -r fc7de207e488 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 14:08:24 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 14:27:20 2012 +0200
@@ -165,7 +165,8 @@
 fun add_lift_def var qty rhs rsp_thm lthy =
   let
     val rty = fastype_of rhs
-    val absrep_trm =  Lifting_Term.absrep_fun lthy (rty, qty)
+    val quotient_thm = Lifting_Term.prove_quot_theorem lthy (rty, qty)
+    val absrep_trm =  Lifting_Term.quot_thm_abs quotient_thm
     val rty_forced = (domain_type o fastype_of) absrep_trm
     val forced_rhs = force_rty_type lthy rty_forced rhs
     val lhs = Free (Binding.print (#1 var), qty)
@@ -176,15 +177,19 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
+    val transfer_thm = def_thm RS (rsp_thm RS (quotient_thm RS @{thm Quotient_to_transfer}))
+
     fun qualify defname suffix = Binding.name suffix
       |> Binding.qualify true defname
 
     val lhs_name = Binding.name_of (#1 var)
     val rsp_thm_name = qualify lhs_name "rsp"
     val code_eqn_thm_name = qualify lhs_name "rep_eq"
+    val transfer_thm_name = qualify lhs_name "transfer"
   in
     lthy'
       |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
+      |> (snd oo Local_Theory.note) ((transfer_thm_name, []), [transfer_thm])
       |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
   end
 
diff -r 803729c9fd4d -r fc7de207e488 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 04 14:08:24 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 04 14:27:20 2012 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/Lifting/lifting_setup.ML
     Author:     Ondrej Kuncar
 
-Setting the lifting infranstructure up.
+Setting up the lifting infrastructure.
 *)
 
 signature LIFTING_SETUP =
@@ -39,7 +39,7 @@
       Const (@{const_name equivp}, _) $ _ => abs_fun_graph
       | Const (@{const_name part_equivp}, _) $ rel => 
         HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
-      | _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem"
+      | _ => raise SETUP_LIFTING_INFR "unsupported equivalence theorem"
       )
     val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
     val qty_name = (fst o dest_Type) qty
@@ -107,7 +107,7 @@
 
 val _ = 
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
-    "Setup lifting infrastracture" 
+    "Setup lifting infrastructure" 
       (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
 
 end;
diff -r 803729c9fd4d -r fc7de207e488 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Apr 04 14:08:24 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Apr 04 14:27:20 2012 +0200
@@ -106,13 +106,13 @@
     (domain_type abs_type, range_type abs_type)
   end
 
-fun prove_quot_theorem ctxt (rty, qty) =
+fun prove_quot_theorem' ctxt (rty, qty) =
   case (rty, qty) of
     (Type (s, tys), Type (s', tys')) =>
       if s = s'
       then
         let
-          val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+          val args = map (prove_quot_theorem' ctxt) (tys ~~ tys')
         in
           if forall is_id_quot args
           then
@@ -126,7 +126,7 @@
           val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
           val qtyenv = match ctxt equiv_match_err qty_pat qty
           val rtys' = map (Envir.subst_type qtyenv) rtys
-          val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
+          val args = map (prove_quot_theorem' ctxt) (tys ~~ rtys')
         in
           if forall is_id_quot args
           then
@@ -152,22 +152,18 @@
     Thm.instantiate (ty_inst, []) quot_thm
   end
 
-fun absrep_fun ctxt (rty, qty) = 
+fun prove_quot_theorem ctxt (rty, qty) =
   let
     val thy = Proof_Context.theory_of ctxt
-    val quot_thm = prove_quot_theorem ctxt (rty, qty)
-    val forced_quot_thm = force_qty_type thy qty quot_thm
+    val quot_thm = prove_quot_theorem' ctxt (rty, qty)
   in
-    quot_thm_abs forced_quot_thm
+    force_qty_type thy qty quot_thm
   end
 
+fun absrep_fun ctxt (rty, qty) =
+  quot_thm_abs (prove_quot_theorem ctxt (rty, qty))
+
 fun equiv_relation ctxt (rty, qty) =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val quot_thm = prove_quot_theorem ctxt (rty, qty)
-    val forced_quot_thm = force_qty_type thy qty quot_thm
-  in
-    quot_thm_rel forced_quot_thm
-  end
+  quot_thm_rel (prove_quot_theorem ctxt (rty, qty))
 
 end;