# HG changeset patch
# User Andreas Lochbihler
# Date 1380203433 -7200
# Node ID abe2b313f0e5caa66614dbe8bf210e36946228b3
# Parent  0fc622be018571a1859437396d10d66ad839a671
add lemmas

diff -r 0fc622be0185 -r abe2b313f0e5 src/HOL/Fun.thy
--- 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"
diff -r 0fc622be0185 -r abe2b313f0e5 src/HOL/Lifting.thy
--- 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
diff -r 0fc622be0185 -r abe2b313f0e5 src/HOL/Lifting_Set.thy
--- 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
diff -r 0fc622be0185 -r abe2b313f0e5 src/HOL/Transfer.thy
--- 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