--- a/src/HOL/Fun.thy Thu Sep 26 13:51:08 2013 +0200
+++ b/src/HOL/Fun.thy Thu Sep 26 15:50:33 2013 +0200
@@ -491,8 +491,11 @@
apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
done
+lemma inj_on_image_eq_iff: "\<lbrakk> inj_on f C; A \<subseteq> C; B \<subseteq> C \<rbrakk> \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
+by(fastforce simp add: inj_on_def)
+
lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
-by(blast dest: inj_onD)
+by(erule inj_on_image_eq_iff) simp_all
lemma inj_on_image_Int:
"[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B"
--- a/src/HOL/Lifting.thy Thu Sep 26 13:51:08 2013 +0200
+++ b/src/HOL/Lifting.thy Thu Sep 26 15:50:33 2013 +0200
@@ -38,9 +38,21 @@
obtains "(\<And>x. \<exists>y. R x y)"
using assms unfolding left_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 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)
+
+lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
+unfolding left_unique_def by blast
+
+lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
+unfolding left_unique_def by blast
+
lemma left_total_fun:
"\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
unfolding left_total_def fun_rel_def
--- a/src/HOL/Lifting_Set.thy Thu Sep 26 13:51:08 2013 +0200
+++ b/src/HOL/Lifting_Set.thy Thu Sep 26 15:50:33 2013 +0200
@@ -19,6 +19,10 @@
shows "set_rel R A B"
using assms unfolding set_rel_def by simp
+lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
+ and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
+by(simp_all add: set_rel_def)
+
lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
unfolding set_rel_def by auto
@@ -153,6 +157,15 @@
set_rel set_rel"
unfolding fun_rel_def set_rel_def by fast
+lemma SUPR_parametric [transfer_rule]:
+ "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
+proof(rule fun_relI)+
+ fix A B f and g :: "'b \<Rightarrow> 'c"
+ assume AB: "set_rel R A B"
+ and fg: "(R ===> op =) f g"
+ show "SUPR A f = SUPR B g"
+ by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
+qed
subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
@@ -268,6 +281,47 @@
"bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
+lemma vimage_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_unique B"
+ shows "((A ===> B) ===> set_rel B ===> set_rel A) vimage vimage"
+unfolding vimage_def[abs_def] by transfer_prover
+
+lemma setsum_parametric [transfer_rule]:
+ assumes "bi_unique A"
+ shows "((A ===> op =) ===> set_rel A ===> op =) setsum setsum"
+proof(rule fun_relI)+
+ fix f :: "'a \<Rightarrow> 'c" and g S T
+ assume fg: "(A ===> op =) f g"
+ and ST: "set_rel A S T"
+ show "setsum f S = setsum g T"
+ proof(rule setsum_reindex_cong)
+ let ?f = "\<lambda>t. THE s. A s t"
+ show "S = ?f ` T"
+ by(blast dest: set_relD1[OF ST] set_relD2[OF ST] bi_uniqueDl[OF assms]
+ intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
+
+ show "inj_on ?f T"
+ proof(rule inj_onI)
+ fix t1 t2
+ assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
+ from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: set_relD2)
+ hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
+ moreover
+ from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: set_relD2)
+ hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
+ ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
+ with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
+ qed
+
+ fix t
+ assume "t \<in> T"
+ with ST obtain s where "A s t" "s \<in> S" by(auto dest: set_relD2)
+ hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
+ moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
+ ultimately show "g t = f (?f t)" by simp
+ qed
+qed
+
end
end
--- a/src/HOL/Transfer.thy Thu Sep 26 13:51:08 2013 +0200
+++ b/src/HOL/Transfer.thy Thu Sep 26 15:50:33 2013 +0200
@@ -158,6 +158,18 @@
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
+by(simp add: bi_unique_def)
+
+lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
+by(simp add: bi_unique_def)
+
+lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
+unfolding right_unique_def by blast
+
+lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
+unfolding right_unique_def by blast
+
lemma right_total_alt_def:
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
unfolding right_total_def fun_rel_def