src/HOL/Library/Quotient_Set.thy
changeset 52359 0eafa146b399
parent 51994 82cc2aeb7d13
child 53012 cb82606b8215
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Mon Jun 10 06:08:12 2013 -0700
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Mon Jun 10 06:08:14 2013 -0700
     1.3 @@ -217,32 +217,48 @@
     1.4    shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter"
     1.5    unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast
     1.6  
     1.7 +lemma bi_unique_set_rel_lemma:
     1.8 +  assumes "bi_unique R" and "set_rel 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 +  let ?f = "\<lambda>x. THE y. R x y"
    1.12 +  from assms show f: "\<forall>x\<in>X. R x (?f x)"
    1.13 +    apply (clarsimp simp add: set_rel_def)
    1.14 +    apply (drule (1) bspec, clarify)
    1.15 +    apply (rule theI2, assumption)
    1.16 +    apply (simp add: bi_unique_def)
    1.17 +    apply assumption
    1.18 +    done
    1.19 +  from assms show "Y = image ?f X"
    1.20 +    apply safe
    1.21 +    apply (clarsimp simp add: set_rel_def)
    1.22 +    apply (drule (1) bspec, clarify)
    1.23 +    apply (rule image_eqI)
    1.24 +    apply (rule the_equality [symmetric], assumption)
    1.25 +    apply (simp add: bi_unique_def)
    1.26 +    apply assumption
    1.27 +    apply (clarsimp simp add: set_rel_def)
    1.28 +    apply (frule (1) bspec, clarify)
    1.29 +    apply (rule theI2, assumption)
    1.30 +    apply (clarsimp simp add: bi_unique_def)
    1.31 +    apply (simp add: bi_unique_def, metis)
    1.32 +    done
    1.33 +  show "inj_on ?f X"
    1.34 +    apply (rule inj_onI)
    1.35 +    apply (drule f [rule_format])
    1.36 +    apply (drule f [rule_format])
    1.37 +    apply (simp add: assms(1) [unfolded bi_unique_def])
    1.38 +    done
    1.39 +qed
    1.40 +
    1.41  lemma finite_transfer [transfer_rule]:
    1.42 -  assumes "bi_unique A"
    1.43 -  shows "(set_rel A ===> op =) finite finite"
    1.44 -  apply (rule fun_relI, rename_tac X Y)
    1.45 -  apply (rule iffI)
    1.46 -  apply (subgoal_tac "Y \<subseteq> (\<lambda>x. THE y. A x y) ` X")
    1.47 -  apply (erule finite_subset, erule finite_imageI)
    1.48 -  apply (rule subsetI, rename_tac y)
    1.49 -  apply (clarsimp simp add: set_rel_def)
    1.50 -  apply (drule (1) bspec, clarify)
    1.51 -  apply (rule image_eqI)
    1.52 -  apply (rule the_equality [symmetric])
    1.53 -  apply assumption
    1.54 -  apply (simp add: assms [unfolded bi_unique_def])
    1.55 -  apply assumption
    1.56 -  apply (subgoal_tac "X \<subseteq> (\<lambda>y. THE x. A x y) ` Y")
    1.57 -  apply (erule finite_subset, erule finite_imageI)
    1.58 -  apply (rule subsetI, rename_tac x)
    1.59 -  apply (clarsimp simp add: set_rel_def)
    1.60 -  apply (drule (1) bspec, clarify)
    1.61 -  apply (rule image_eqI)
    1.62 -  apply (rule the_equality [symmetric])
    1.63 -  apply assumption
    1.64 -  apply (simp add: assms [unfolded bi_unique_def])
    1.65 -  apply assumption
    1.66 -  done
    1.67 +  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) finite finite"
    1.68 +  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma,
    1.69 +    auto dest: finite_imageD)
    1.70 +
    1.71 +lemma card_transfer [transfer_rule]:
    1.72 +  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
    1.73 +  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
    1.74  
    1.75  subsection {* Setup for lifting package *}
    1.76