# HG changeset patch
# User huffman
# Date 1334739169 -7200
# Node ID 06cc372a80ed6473f0b4e38b3540fb8f53fefb79
# Parent  5afe54e0540638288991283fb59b54797f6bde55
use context block to organize typedef lifting theorems

diff -r 5afe54e05406 -r 06cc372a80ed src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Apr 18 10:53:28 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed Apr 18 10:52:49 2012 +0200
@@ -328,18 +328,37 @@
 
 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
 
-lemma typedef_bi_unique:
+context
+  fixes Rep Abs A T
   assumes type: "type_definition Rep Abs A"
-  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "bi_unique T"
+  assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
+begin
+
+lemma typedef_bi_unique: "bi_unique T"
   unfolding bi_unique_def T_def
   by (simp add: type_definition.Rep_inject [OF type])
 
-lemma typedef_right_total:
-  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "right_total T"
+lemma typedef_right_total: "right_total T"
   unfolding right_total_def T_def by simp
 
+lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
+  unfolding T_def fun_rel_def
+  by (metis type_definition.Rep [OF type]
+    type_definition.Abs_inverse [OF type])
+
+lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
+  unfolding T_def fun_rel_def
+  by (metis type_definition.Rep [OF type]
+    type_definition.Abs_inverse [OF type])
+
+lemma typedef_transfer_bforall:
+  "((T ===> op =) ===> op =)
+    (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
+  unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
+  by (rule typedef_transfer_All [OF assms])
+
+end
+
 lemma copy_type_bi_total:
   assumes type: "type_definition Rep Abs UNIV"
   assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
@@ -347,30 +366,6 @@
   unfolding bi_total_def T_def
   by (metis type_definition.Abs_inverse [OF type] UNIV_I)
 
-lemma typedef_transfer_All:
-  assumes type: "type_definition Rep Abs A"
-  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "((T ===> op =) ===> op =) (Ball A) All"
-  unfolding T_def fun_rel_def
-  by (metis type_definition.Rep [OF type]
-    type_definition.Abs_inverse [OF type])
-
-lemma typedef_transfer_Ex:
-  assumes type: "type_definition Rep Abs A"
-  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "((T ===> op =) ===> op =) (Bex A) Ex"
-  unfolding T_def fun_rel_def
-  by (metis type_definition.Rep [OF type]
-    type_definition.Abs_inverse [OF type])
-
-lemma typedef_transfer_bforall:
-  assumes type: "type_definition Rep Abs A"
-  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "((T ===> op =) ===> op =)
-    (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
-  unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
-  by (rule typedef_transfer_All [OF assms])
-
 text {* Generating the correspondence rule for a constant defined with
   @{text "lift_definition"}. *}
 
diff -r 5afe54e05406 -r 06cc372a80ed src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 10:53:28 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 10:52:49 2012 +0200
@@ -136,7 +136,7 @@
       |> (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}])
+        [[typedef_thm, T_def] MRSL @{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]),