src/HOL/Library/Quotient_Set.thy
changeset 51956 a4d81cdebf8b
parent 51377 7da251a6c16e
child 51994 82cc2aeb7d13
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Mon May 13 12:13:24 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Mon May 13 13:59:04 2013 +0200
     1.3 @@ -40,6 +40,16 @@
     1.4    apply (simp add: set_rel_def, fast)
     1.5    done
     1.6  
     1.7 +lemma Domainp_set[relator_domain]:
     1.8 +  assumes "Domainp T = R"
     1.9 +  shows "Domainp (set_rel T) = (\<lambda>A. Ball A R)"
    1.10 +using assms unfolding set_rel_def Domainp_iff[abs_def]
    1.11 +apply (intro ext)
    1.12 +apply (rule iffI) 
    1.13 +apply blast
    1.14 +apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
    1.15 +done
    1.16 +
    1.17  lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
    1.18    unfolding reflp_def set_rel_def by fast
    1.19  
    1.20 @@ -136,13 +146,19 @@
    1.21      set_rel set_rel"
    1.22    unfolding fun_rel_def set_rel_def by fast
    1.23  
    1.24 -subsubsection {* Rules requiring bi-unique or bi-total relations *}
    1.25 +
    1.26 +subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
    1.27  
    1.28  lemma member_transfer [transfer_rule]:
    1.29    assumes "bi_unique A"
    1.30    shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)"
    1.31    using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
    1.32  
    1.33 +lemma right_total_Collect_transfer[transfer_rule]:
    1.34 +  assumes "right_total A"
    1.35 +  shows "((A ===> op =) ===> set_rel A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
    1.36 +  using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast
    1.37 +
    1.38  lemma Collect_transfer [transfer_rule]:
    1.39    assumes "bi_total A"
    1.40    shows "((A ===> op =) ===> set_rel A) Collect Collect"
    1.41 @@ -165,21 +181,43 @@
    1.42    shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"
    1.43    unfolding subset_eq [abs_def] by transfer_prover
    1.44  
    1.45 +lemma right_total_UNIV_transfer[transfer_rule]: 
    1.46 +  assumes "right_total A"
    1.47 +  shows "(set_rel A) (Collect (Domainp A)) UNIV"
    1.48 +  using assms unfolding right_total_def set_rel_def Domainp_iff by blast
    1.49 +
    1.50  lemma UNIV_transfer [transfer_rule]:
    1.51    assumes "bi_total A"
    1.52    shows "(set_rel A) UNIV UNIV"
    1.53    using assms unfolding set_rel_def bi_total_def by simp
    1.54  
    1.55 +lemma right_total_Compl_transfer [transfer_rule]:
    1.56 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
    1.57 +  shows "(set_rel A ===> set_rel A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus"
    1.58 +  unfolding Compl_eq [abs_def]
    1.59 +  by (subst Collect_conj_eq[symmetric]) transfer_prover
    1.60 +
    1.61  lemma Compl_transfer [transfer_rule]:
    1.62    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
    1.63    shows "(set_rel A ===> set_rel A) uminus uminus"
    1.64    unfolding Compl_eq [abs_def] by transfer_prover
    1.65  
    1.66 +lemma right_total_Inter_transfer [transfer_rule]:
    1.67 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
    1.68 +  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
    1.69 +  unfolding Inter_eq[abs_def]
    1.70 +  by (subst Collect_conj_eq[symmetric]) transfer_prover
    1.71 +
    1.72  lemma Inter_transfer [transfer_rule]:
    1.73    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
    1.74    shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter"
    1.75    unfolding Inter_eq [abs_def] by transfer_prover
    1.76  
    1.77 +lemma filter_transfer [transfer_rule]:
    1.78 +  assumes [transfer_rule]: "bi_unique A"
    1.79 +  shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter"
    1.80 +  unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast
    1.81 +
    1.82  lemma finite_transfer [transfer_rule]:
    1.83    assumes "bi_unique A"
    1.84    shows "(set_rel A ===> op =) finite finite"