# HG changeset patch
# User huffman
# Date 1333606420 -7200
# Node ID eabfb53cfca809e43ea21fc32c07d80b2befa51c
# Parent  f483be2fecb9464db3b32642a25e1aba17148444# Parent  97097a58335d0d45afa9c0bb5dc780a84bb92131
merged

diff -r 97097a58335d -r eabfb53cfca8 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu Apr 05 00:37:22 2012 +0100
+++ b/src/HOL/Lifting.thy	Thu Apr 05 08:13:40 2012 +0200
@@ -297,6 +297,54 @@
   show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
 qed
 
+text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
+
+lemma typedef_bi_unique:
+  assumes type: "type_definition Rep Abs A"
+  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
+  shows "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"
+  unfolding right_total_def T_def by simp
+
+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)
+
+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"}. *}
+
 lemma Quotient_to_transfer:
   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   shows "T c c'"