--- a/src/HOL/Lifting.thy Fri Sep 27 14:43:26 2013 +0200
+++ b/src/HOL/Lifting.thy Fri Sep 27 14:43:26 2013 +0200
@@ -38,12 +38,26 @@
obtains "(\<And>x. \<exists>y. R x y)"
using assms unfolding left_total_def by blast
+lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
+unfolding left_total_def right_total_def bi_total_def by blast
+
lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
by(simp add: left_total_def right_total_def bi_total_def)
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma left_unique_transfer [transfer_rule]:
+ assumes [transfer_rule]: "right_total A"
+ assumes [transfer_rule]: "right_total B"
+ assumes [transfer_rule]: "bi_unique A"
+ shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
+using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
+by metis
+
+lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
+unfolding left_unique_def right_unique_def bi_unique_def by blast
+
lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
by(auto simp add: left_unique_def right_unique_def bi_unique_def)
@@ -286,6 +300,11 @@
shows "invariant P x x \<equiv> P x"
using assms by (auto simp add: invariant_def)
+lemma invariant_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "((A ===> op=) ===> A ===> A ===> op=) Lifting.invariant Lifting.invariant"
+unfolding invariant_def[abs_def] by transfer_prover
+
lemma UNIV_typedef_to_Quotient:
assumes "type_definition Rep Abs UNIV"
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"