src/HOL/Lifting_Set.thy
changeset 57129 7edb7550663e
parent 56524 f4ba736040fa
child 57599 7ef939f89776
     1.1 --- a/src/HOL/Lifting_Set.thy	Fri May 30 12:54:42 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Fri May 30 14:55:10 2014 +0200
     1.3 @@ -85,6 +85,26 @@
     1.4    "rel_set (eq_onp P) = eq_onp (\<lambda>A. Ball A P)"
     1.5    unfolding fun_eq_iff rel_set_def eq_onp_def Ball_def by fast
     1.6  
     1.7 +lemma bi_unique_rel_set_lemma:
     1.8 +  assumes "bi_unique R" and "rel_set R X Y"
     1.9 +  obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
    1.10 +proof
    1.11 +  def f \<equiv> "\<lambda>x. THE y. R x y"
    1.12 +  { fix x assume "x \<in> X"
    1.13 +    with `rel_set R X Y` `bi_unique R` have "R x (f x)"
    1.14 +      by (simp add: bi_unique_def rel_set_def f_def) (metis theI)
    1.15 +    with assms `x \<in> X` 
    1.16 +    have  "R x (f x)" "\<forall>x'\<in>X. R x' (f x) \<longrightarrow> x = x'" "\<forall>y\<in>Y. R x y \<longrightarrow> y = f x" "f x \<in> Y"
    1.17 +      by (fastforce simp add: bi_unique_def rel_set_def)+ }
    1.18 +  note * = this
    1.19 +  moreover
    1.20 +  { fix y assume "y \<in> Y"
    1.21 +    with `rel_set R X Y` *(3) `y \<in> Y` have "\<exists>x\<in>X. y = f x"
    1.22 +      by (fastforce simp: rel_set_def) }
    1.23 +  ultimately show "\<forall>x\<in>X. R x (f x)" "Y = image f X" "inj_on f X"
    1.24 +    by (auto simp: inj_on_def image_iff)
    1.25 +qed
    1.26 +
    1.27  subsection {* Quotient theorem for the Lifting package *}
    1.28  
    1.29  lemma Quotient_set[quot_map]:
    1.30 @@ -231,90 +251,37 @@
    1.31    shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter"
    1.32    unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast
    1.33  
    1.34 -lemma bi_unique_rel_set_lemma:
    1.35 -  assumes "bi_unique R" and "rel_set R X Y"
    1.36 -  obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
    1.37 -proof
    1.38 -  let ?f = "\<lambda>x. THE y. R x y"
    1.39 -  from assms show f: "\<forall>x\<in>X. R x (?f x)"
    1.40 -    apply (clarsimp simp add: rel_set_def)
    1.41 -    apply (drule (1) bspec, clarify)
    1.42 -    apply (rule theI2, assumption)
    1.43 -    apply (simp add: bi_unique_def)
    1.44 -    apply assumption
    1.45 -    done
    1.46 -  from assms show "Y = image ?f X"
    1.47 -    apply safe
    1.48 -    apply (clarsimp simp add: rel_set_def)
    1.49 -    apply (drule (1) bspec, clarify)
    1.50 -    apply (rule image_eqI)
    1.51 -    apply (rule the_equality [symmetric], assumption)
    1.52 -    apply (simp add: bi_unique_def)
    1.53 -    apply assumption
    1.54 -    apply (clarsimp simp add: rel_set_def)
    1.55 -    apply (frule (1) bspec, clarify)
    1.56 -    apply (rule theI2, assumption)
    1.57 -    apply (clarsimp simp add: bi_unique_def)
    1.58 -    apply (simp add: bi_unique_def, metis)
    1.59 -    done
    1.60 -  show "inj_on ?f X"
    1.61 -    apply (rule inj_onI)
    1.62 -    apply (drule f [rule_format])
    1.63 -    apply (drule f [rule_format])
    1.64 -    apply (simp add: assms(1) [unfolded bi_unique_def])
    1.65 -    done
    1.66 -qed
    1.67 -
    1.68  lemma finite_transfer [transfer_rule]:
    1.69    "bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite"
    1.70 -  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma,
    1.71 -    auto dest: finite_imageD)
    1.72 +  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
    1.73 +     (auto dest: finite_imageD)
    1.74  
    1.75  lemma card_transfer [transfer_rule]:
    1.76    "bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card"
    1.77 -  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
    1.78 +  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
    1.79 +     (simp add: card_image)
    1.80  
    1.81  lemma vimage_parametric [transfer_rule]:
    1.82    assumes [transfer_rule]: "bi_total A" "bi_unique B"
    1.83    shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
    1.84 -unfolding vimage_def[abs_def] by transfer_prover
    1.85 -
    1.86 -lemma setsum_parametric [transfer_rule]:
    1.87 -  assumes "bi_unique A"
    1.88 -  shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum"
    1.89 -proof(rule rel_funI)+
    1.90 -  fix f :: "'a \<Rightarrow> 'c" and g S T
    1.91 -  assume fg: "(A ===> op =) f g"
    1.92 -    and ST: "rel_set A S T"
    1.93 -  show "setsum f S = setsum g T"
    1.94 -  proof(rule setsum_reindex_cong)
    1.95 -    let ?f = "\<lambda>t. THE s. A s t"
    1.96 -    show "S = ?f ` T"
    1.97 -      by(blast dest: rel_setD1[OF ST] rel_setD2[OF ST] bi_uniqueDl[OF assms] 
    1.98 -           intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
    1.99 -
   1.100 -    show "inj_on ?f T"
   1.101 -    proof(rule inj_onI)
   1.102 -      fix t1 t2
   1.103 -      assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
   1.104 -      from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: rel_setD2)
   1.105 -      hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
   1.106 -      moreover
   1.107 -      from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: rel_setD2)
   1.108 -      hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
   1.109 -      ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
   1.110 -      with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
   1.111 -    qed
   1.112 -
   1.113 -    fix t
   1.114 -    assume "t \<in> T"
   1.115 -    with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2)
   1.116 -    hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
   1.117 -    moreover from fg `A s t` have "f s = g t" by(rule rel_funD)
   1.118 -    ultimately show "g t = f (?f t)" by simp
   1.119 -  qed
   1.120 -qed
   1.121 +  unfolding vimage_def[abs_def] by transfer_prover
   1.122  
   1.123  end
   1.124  
   1.125 +lemma (in comm_monoid_set) F_parametric [transfer_rule]:
   1.126 +  fixes A :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
   1.127 +  assumes "bi_unique A"
   1.128 +  shows "rel_fun (rel_fun A (op =)) (rel_fun (rel_set A) (op =)) F F"
   1.129 +proof(rule rel_funI)+
   1.130 +  fix f :: "'b \<Rightarrow> 'a" and g S T
   1.131 +  assume "rel_fun A (op =) f g" "rel_set A S T"
   1.132 +  with `bi_unique A` obtain i where "bij_betw i S T" "\<And>x. x \<in> S \<Longrightarrow> f x = g (i x)"
   1.133 +    by (auto elim: bi_unique_rel_set_lemma simp: rel_fun_def bij_betw_def)
   1.134 +  then show "F f S = F g T"
   1.135 +    by (simp add: reindex_bij_betw)
   1.136 +qed
   1.137 +
   1.138 +lemmas setsum_parametric = setsum.F_parametric
   1.139 +lemmas setprod_parametric = setprod.F_parametric
   1.140 +
   1.141  end