src/HOL/Lifting_Set.thy
changeset 53927 abe2b313f0e5
parent 53012 cb82606b8215
child 53945 4191acef9d0e
     1.1 --- a/src/HOL/Lifting_Set.thy	Thu Sep 26 13:51:08 2013 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Thu Sep 26 15:50:33 2013 +0200
     1.3 @@ -19,6 +19,10 @@
     1.4    shows "set_rel R A B"
     1.5    using assms unfolding set_rel_def by simp
     1.6  
     1.7 +lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
     1.8 +  and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
     1.9 +by(simp_all add: set_rel_def)
    1.10 +
    1.11  lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
    1.12    unfolding set_rel_def by auto
    1.13  
    1.14 @@ -153,6 +157,15 @@
    1.15      set_rel set_rel"
    1.16    unfolding fun_rel_def set_rel_def by fast
    1.17  
    1.18 +lemma SUPR_parametric [transfer_rule]:
    1.19 +  "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
    1.20 +proof(rule fun_relI)+
    1.21 +  fix A B f and g :: "'b \<Rightarrow> 'c"
    1.22 +  assume AB: "set_rel R A B"
    1.23 +    and fg: "(R ===> op =) f g"
    1.24 +  show "SUPR A f = SUPR B g"
    1.25 +    by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
    1.26 +qed
    1.27  
    1.28  subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
    1.29  
    1.30 @@ -268,6 +281,47 @@
    1.31    "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
    1.32    by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
    1.33  
    1.34 +lemma vimage_parametric [transfer_rule]:
    1.35 +  assumes [transfer_rule]: "bi_total A" "bi_unique B"
    1.36 +  shows "((A ===> B) ===> set_rel B ===> set_rel A) vimage vimage"
    1.37 +unfolding vimage_def[abs_def] by transfer_prover
    1.38 +
    1.39 +lemma setsum_parametric [transfer_rule]:
    1.40 +  assumes "bi_unique A"
    1.41 +  shows "((A ===> op =) ===> set_rel A ===> op =) setsum setsum"
    1.42 +proof(rule fun_relI)+
    1.43 +  fix f :: "'a \<Rightarrow> 'c" and g S T
    1.44 +  assume fg: "(A ===> op =) f g"
    1.45 +    and ST: "set_rel A S T"
    1.46 +  show "setsum f S = setsum g T"
    1.47 +  proof(rule setsum_reindex_cong)
    1.48 +    let ?f = "\<lambda>t. THE s. A s t"
    1.49 +    show "S = ?f ` T"
    1.50 +      by(blast dest: set_relD1[OF ST] set_relD2[OF ST] bi_uniqueDl[OF assms] 
    1.51 +           intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
    1.52 +
    1.53 +    show "inj_on ?f T"
    1.54 +    proof(rule inj_onI)
    1.55 +      fix t1 t2
    1.56 +      assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
    1.57 +      from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: set_relD2)
    1.58 +      hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
    1.59 +      moreover
    1.60 +      from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: set_relD2)
    1.61 +      hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
    1.62 +      ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
    1.63 +      with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
    1.64 +    qed
    1.65 +
    1.66 +    fix t
    1.67 +    assume "t \<in> T"
    1.68 +    with ST obtain s where "A s t" "s \<in> S" by(auto dest: set_relD2)
    1.69 +    hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
    1.70 +    moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
    1.71 +    ultimately show "g t = f (?f t)" by simp
    1.72 +  qed
    1.73 +qed
    1.74 +
    1.75  end
    1.76  
    1.77  end