tuned the setup of lifting; generate transfer rules for typedef and Quotient thms

--- a/src/HOL/Lifting.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/Lifting.thy	Tue Apr 17 19:16:13 2012 +0200
@@ -218,6 +218,10 @@
     done
 qed
 
+lemma equivp_reflp2:
+  "equivp R \<Longrightarrow> reflp R"
+  by (erule equivpE)
+
 subsection {* Invariant *}
 
 definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Apr 17 19:16:13 2012 +0200
@@ -8,7 +8,9 @@
 sig
   exception SETUP_LIFTING_INFR of string
 
-  val setup_lifting_infr: thm -> thm -> local_theory -> local_theory
+  val setup_lifting_infr: thm -> local_theory -> local_theory
+
+  val setup_by_quotient: thm -> thm option -> local_theory -> local_theory
 
   val setup_by_typedef_thm: thm -> local_theory -> local_theory
 end;
@@ -76,7 +78,7 @@
                                                 @ (map Pretty.string_of errs)))
   end
 
-fun setup_lifting_infr quot_thm equiv_thm lthy =
+fun setup_lifting_infr quot_thm lthy =
   let
     val _ = quot_thm_sanity_check lthy quot_thm
     val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
@@ -90,36 +92,73 @@
       |> define_abs_type quot_thm
   end
 
+fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
+  let
+    val transfer_attr = Attrib.internal (K Transfer.transfer_add)
+    val lthy' = case maybe_reflp_thm of
+      SOME reflp_thm => lthy
+        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+          [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
+        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+          [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
+      | NONE => lthy
+  in
+    lthy'
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [quot_thm RS @{thm Quotient_right_unique}])
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [quot_thm RS @{thm Quotient_right_total}])
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [quot_thm RS @{thm Quotient_rel_eq_transfer}])
+      |> setup_lifting_infr quot_thm
+  end
+
 fun setup_by_typedef_thm typedef_thm lthy =
   let
-    fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
-      let
-        val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
-        val equiv_thm = typedef_thm RS to_equiv_thm
-        val (T_def, lthy') = define_cr_rel rep_fun lthy
-        val quot_thm =  [typedef_thm, T_def] MRSL to_quot_thm
-      in
-        (quot_thm, equiv_thm, lthy')
-      end
+    val transfer_attr = Attrib.internal (K Transfer.transfer_add)
+    val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
+    val (T_def, lthy') = define_cr_rel rep_fun lthy
+    
+    val quot_thm = (case typedef_set of
+      Const ("Orderings.top_class.top", _) => 
+        [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
+      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
+        [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
+      | _ => 
+        [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient})
 
-    val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
-    val (quot_thm, equiv_thm, lthy') = (case typedef_set of
-      Const ("Orderings.top_class.top", _) => 
-        derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp} 
-          typedef_thm lthy
-      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
-        derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp} 
-          typedef_thm lthy
-      | _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp} 
-          typedef_thm lthy)
+    val lthy'' = (case typedef_set of
+      Const ("Orderings.top_class.top", _) => (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [[typedef_thm,T_def] MRSL @{thm copy_type_bi_total}]) lthy'
+      | _ => lthy')
   in
-    setup_lifting_infr quot_thm equiv_thm lthy'
+    lthy''
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [T_def RS @{thm typedef_right_total}])
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}])
+      |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
+        [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}])
+      |> setup_lifting_infr quot_thm
   end
 
-fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy
+fun setup_lifting_cmd xthm lthy =
+  let 
+    val input_thm = singleton (Attrib.eval_thms lthy) xthm
+    val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
+  in
+    case input_term of
+      (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy
+      | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy
+      | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
+  end
 
 val _ = 
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     "Setup lifting infrastructure" 
-      (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
+      (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm))
 end;

--- a/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 17 19:16:13 2012 +0200
@@ -139,16 +139,18 @@
     val (rty, qty) = (dest_funT o fastype_of) abs_fun
     val qty_name = (fst o dest_Type) qty
     val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) 
-    val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
-      Const (@{const_name equivp}, _) $ _ => 
-        [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}
-      | Const (@{const_name part_equivp}, _) $ _ => 
-        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient}
+    val (reflp_thm, quot_thm) = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
+      Const (@{const_name equivp}, _) $ _ =>
+        (SOME (equiv_thm RS @{thm equivp_reflp2}),
+         [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp})
+      | Const (@{const_name part_equivp}, _) $ _ =>
+        (NONE,
+        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient})
       | _ => error "unsupported equivalence theorem"
       )
   in
     lthy'
-      |> Lifting_Setup.setup_lifting_infr quot_thm equiv_thm
+      |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm
       |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
   end
 

--- a/src/HOL/Word/Word.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/Word/Word.thy	Tue Apr 17 19:16:13 2012 +0200
@@ -244,26 +244,10 @@
   by (simp add: reflp_def)
 
 local_setup {*
-  Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm reflp_word}
+  Lifting_Setup.setup_by_quotient @{thm Quotient_word} (SOME @{thm reflp_word})
 *}
 
-text {* TODO: The next several lemmas could be generated automatically. *}
-
-lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word"
-  using Quotient_word reflp_word by (rule Quotient_bi_total)
-
-lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word"
-  using Quotient_word by (rule Quotient_right_unique)
-
-lemma word_eq_transfer [transfer_rule]:
-  "(fun_rel cr_word (fun_rel cr_word op =))
-    (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
-    (op = :: 'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool)"
-  using Quotient_word by (rule Quotient_rel_eq_transfer)
-
-lemma word_of_int_transfer [transfer_rule]:
-  "(fun_rel op = cr_word) (\<lambda>x. x) word_of_int"
-  using Quotient_word reflp_word by (rule Quotient_id_abs_transfer)
+text {* TODO: The next lemma could be generated automatically. *}
 
 lemma uint_transfer [transfer_rule]:
   "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))