--- 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)"
--- a/src/HOL/Lifting_Set.thy Fri Sep 27 14:43:26 2013 +0200
+++ b/src/HOL/Lifting_Set.thy Fri Sep 27 14:43:26 2013 +0200
@@ -162,6 +162,10 @@
by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
qed
+lemma bind_transfer [transfer_rule]:
+ "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) Set.bind Set.bind"
+unfolding bind_UNION[abs_def] by transfer_prover
+
subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
lemma member_transfer [transfer_rule]:
--- a/src/HOL/Transfer.thy Fri Sep 27 14:43:26 2013 +0200
+++ b/src/HOL/Transfer.thy Fri Sep 27 14:43:26 2013 +0200
@@ -292,6 +292,17 @@
subsection {* Transfer rules *}
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+ by auto
+
+lemma Domainp_forall_transfer [transfer_rule]:
+ assumes "right_total A"
+ shows "((A ===> op =) ===> op =)
+ (transfer_bforall (Domainp A)) transfer_forall"
+ using assms unfolding right_total_def
+ unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
+ by metis
+
text {* Transfer rules using implication instead of equality on booleans. *}
lemma transfer_forall_transfer [transfer_rule]:
@@ -324,9 +335,6 @@
shows "(A ===> A ===> op =) (op =) (op =)"
using assms unfolding bi_unique_def fun_rel_def by auto
-lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
- by auto
-
lemma right_total_Ex_transfer[transfer_rule]:
assumes "right_total A"
shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
@@ -379,17 +387,50 @@
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
unfolding funpow_def by transfer_prover
-lemma Domainp_forall_transfer [transfer_rule]:
- assumes "right_total A"
- shows "((A ===> op =) ===> op =)
- (transfer_bforall (Domainp A)) transfer_forall"
- using assms unfolding right_total_def
- unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
- by metis
+lemma mono_transfer[transfer_rule]:
+ assumes [transfer_rule]: "bi_total A"
+ assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>"
+ assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>"
+ shows "((A ===> B) ===> op=) mono mono"
+unfolding mono_def[abs_def] by transfer_prover
+
+lemma right_total_relcompp_transfer[transfer_rule]:
+ assumes [transfer_rule]: "right_total B"
+ shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=)
+ (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO"
+unfolding OO_def[abs_def] by transfer_prover
+
+lemma relcompp_transfer[transfer_rule]:
+ assumes [transfer_rule]: "bi_total B"
+ shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO"
+unfolding OO_def[abs_def] by transfer_prover
-lemma forall_transfer [transfer_rule]:
- "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
- unfolding transfer_forall_def by (rule All_transfer)
+lemma right_total_Domainp_transfer[transfer_rule]:
+ assumes [transfer_rule]: "right_total B"
+ shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp"
+apply(subst(2) Domainp_iff[abs_def]) by transfer_prover
+
+lemma Domainp_transfer[transfer_rule]:
+ assumes [transfer_rule]: "bi_total B"
+ shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp"
+unfolding Domainp_iff[abs_def] by transfer_prover
+
+lemma reflp_transfer[transfer_rule]:
+ "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp"
+ "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
+ "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
+ "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
+ "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
+using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def
+by fast+
+
+lemma right_unique_transfer [transfer_rule]:
+ assumes [transfer_rule]: "right_total A"
+ assumes [transfer_rule]: "right_total B"
+ assumes [transfer_rule]: "bi_unique B"
+ shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
+using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
+by metis
end