--- a/src/HOL/Lifting.thy Wed Apr 18 10:52:49 2012 +0200
+++ b/src/HOL/Lifting.thy Wed Apr 18 12:15:20 2012 +0200
@@ -341,6 +341,9 @@
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]
@@ -355,7 +358,7 @@
"((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])
+ by (rule typedef_transfer_All)
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 10:52:49 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 12:15:20 2012 +0200
@@ -138,6 +138,8 @@
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
[[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_rep_transfer}])
+ |> (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}])