add lemmas
authorAndreas Lochbihler
Thu Sep 26 15:50:33 2013 +0200 (2013-09-26)
changeset 53927abe2b313f0e5
parent 53918 0fc622be0185
child 53928 2e75da4fe4b6
add lemmas
src/HOL/Fun.thy
src/HOL/Lifting.thy
src/HOL/Lifting_Set.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Sep 26 13:51:08 2013 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Sep 26 15:50:33 2013 +0200
     1.3 @@ -491,8 +491,11 @@
     1.4  apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
     1.5  done
     1.6  
     1.7 +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"
     1.8 +by(fastforce simp add: inj_on_def)
     1.9 +
    1.10  lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
    1.11 -by(blast dest: inj_onD)
    1.12 +by(erule inj_on_image_eq_iff) simp_all
    1.13  
    1.14  lemma inj_on_image_Int:
    1.15     "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"
     2.1 --- a/src/HOL/Lifting.thy	Thu Sep 26 13:51:08 2013 +0200
     2.2 +++ b/src/HOL/Lifting.thy	Thu Sep 26 15:50:33 2013 +0200
     2.3 @@ -38,9 +38,21 @@
     2.4    obtains "(\<And>x. \<exists>y. R x y)"
     2.5  using assms unfolding left_total_def by blast
     2.6  
     2.7 +lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
     2.8 +by(simp add: left_total_def right_total_def bi_total_def)
     2.9 +
    2.10  definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    2.11    where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    2.12  
    2.13 +lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
    2.14 +by(auto simp add: left_unique_def right_unique_def bi_unique_def)
    2.15 +
    2.16 +lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
    2.17 +unfolding left_unique_def by blast
    2.18 +
    2.19 +lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
    2.20 +unfolding left_unique_def by blast
    2.21 +
    2.22  lemma left_total_fun:
    2.23    "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
    2.24    unfolding left_total_def fun_rel_def
     3.1 --- a/src/HOL/Lifting_Set.thy	Thu Sep 26 13:51:08 2013 +0200
     3.2 +++ b/src/HOL/Lifting_Set.thy	Thu Sep 26 15:50:33 2013 +0200
     3.3 @@ -19,6 +19,10 @@
     3.4    shows "set_rel R A B"
     3.5    using assms unfolding set_rel_def by simp
     3.6  
     3.7 +lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
     3.8 +  and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
     3.9 +by(simp_all add: set_rel_def)
    3.10 +
    3.11  lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
    3.12    unfolding set_rel_def by auto
    3.13  
    3.14 @@ -153,6 +157,15 @@
    3.15      set_rel set_rel"
    3.16    unfolding fun_rel_def set_rel_def by fast
    3.17  
    3.18 +lemma SUPR_parametric [transfer_rule]:
    3.19 +  "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
    3.20 +proof(rule fun_relI)+
    3.21 +  fix A B f and g :: "'b \<Rightarrow> 'c"
    3.22 +  assume AB: "set_rel R A B"
    3.23 +    and fg: "(R ===> op =) f g"
    3.24 +  show "SUPR A f = SUPR B g"
    3.25 +    by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
    3.26 +qed
    3.27  
    3.28  subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
    3.29  
    3.30 @@ -268,6 +281,47 @@
    3.31    "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
    3.32    by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
    3.33  
    3.34 +lemma vimage_parametric [transfer_rule]:
    3.35 +  assumes [transfer_rule]: "bi_total A" "bi_unique B"
    3.36 +  shows "((A ===> B) ===> set_rel B ===> set_rel A) vimage vimage"
    3.37 +unfolding vimage_def[abs_def] by transfer_prover
    3.38 +
    3.39 +lemma setsum_parametric [transfer_rule]:
    3.40 +  assumes "bi_unique A"
    3.41 +  shows "((A ===> op =) ===> set_rel A ===> op =) setsum setsum"
    3.42 +proof(rule fun_relI)+
    3.43 +  fix f :: "'a \<Rightarrow> 'c" and g S T
    3.44 +  assume fg: "(A ===> op =) f g"
    3.45 +    and ST: "set_rel A S T"
    3.46 +  show "setsum f S = setsum g T"
    3.47 +  proof(rule setsum_reindex_cong)
    3.48 +    let ?f = "\<lambda>t. THE s. A s t"
    3.49 +    show "S = ?f ` T"
    3.50 +      by(blast dest: set_relD1[OF ST] set_relD2[OF ST] bi_uniqueDl[OF assms] 
    3.51 +           intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
    3.52 +
    3.53 +    show "inj_on ?f T"
    3.54 +    proof(rule inj_onI)
    3.55 +      fix t1 t2
    3.56 +      assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
    3.57 +      from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: set_relD2)
    3.58 +      hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
    3.59 +      moreover
    3.60 +      from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: set_relD2)
    3.61 +      hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
    3.62 +      ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
    3.63 +      with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
    3.64 +    qed
    3.65 +
    3.66 +    fix t
    3.67 +    assume "t \<in> T"
    3.68 +    with ST obtain s where "A s t" "s \<in> S" by(auto dest: set_relD2)
    3.69 +    hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
    3.70 +    moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
    3.71 +    ultimately show "g t = f (?f t)" by simp
    3.72 +  qed
    3.73 +qed
    3.74 +
    3.75  end
    3.76  
    3.77  end
     4.1 --- a/src/HOL/Transfer.thy	Thu Sep 26 13:51:08 2013 +0200
     4.2 +++ b/src/HOL/Transfer.thy	Thu Sep 26 15:50:33 2013 +0200
     4.3 @@ -158,6 +158,18 @@
     4.4      (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
     4.5      (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
     4.6  
     4.7 +lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
     4.8 +by(simp add: bi_unique_def)
     4.9 +
    4.10 +lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
    4.11 +by(simp add: bi_unique_def)
    4.12 +
    4.13 +lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
    4.14 +unfolding right_unique_def by blast
    4.15 +
    4.16 +lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
    4.17 +unfolding right_unique_def by blast
    4.18 +
    4.19  lemma right_total_alt_def:
    4.20    "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
    4.21    unfolding right_total_def fun_rel_def