src/HOL/Lifting.thy
changeset 47545 a2850a16e30f
parent 47544 e455cdaac479
child 47575 b90cd7016d4f
--- a/src/HOL/Lifting.thy	Wed Apr 18 15:48:32 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed Apr 18 17:04:03 2012 +0200
@@ -353,39 +353,27 @@
   unfolding bi_unique_def T_def
   by (simp add: type_definition.Rep_inject [OF type])
 
-lemma typedef_right_total: "right_total T"
-  unfolding right_total_def T_def by simp
-
 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   unfolding fun_rel_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"
+lemma typedef_All_transfer: "((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_bforall:
+lemma typedef_Ex_transfer: "((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_forall_transfer:
   "((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)
+  by (rule typedef_All_transfer)
 
 end
 
-text {* Generating transfer rules for a type copy. *}
-
-lemma copy_type_bi_total:
-  assumes type: "type_definition Rep Abs UNIV"
-  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "bi_total T"
-  unfolding bi_total_def T_def
-  by (metis type_definition.Abs_inverse [OF type] UNIV_I)
-
 text {* Generating the correspondence rule for a constant defined with
   @{text "lift_definition"}. *}