src/HOL/Library/Quotient_Set.thy
author huffman
Sat Apr 21 10:59:52 2012 +0200 (2012-04-21)
changeset 47647 ec29cc09599d
parent 47626 f7b1034cb9ce
child 47648 6b9d20a095ae
permissions -rw-r--r--
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
     1 (*  Title:      HOL/Library/Quotient_Set.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 
     5 header {* Quotient infrastructure for the set type *}
     6 
     7 theory Quotient_Set
     8 imports Main Quotient_Syntax
     9 begin
    10 
    11 subsection {* set map (vimage) and set relation *}
    12 
    13 definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
    14 
    15 lemma vset_rel_eq [id_simps]:
    16   "vset_rel op = = op ="
    17   by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff vset_rel_def)
    18 
    19 lemma vset_rel_equivp:
    20   assumes e: "equivp R"
    21   shows "vset_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    22   unfolding vset_rel_def
    23   using equivp_reflp[OF e]
    24   by auto (metis, metis equivp_symp[OF e])
    25 
    26 lemma set_quotient [quot_thm]:
    27   assumes "Quotient3 R Abs Rep"
    28   shows "Quotient3 (vset_rel R) (vimage Rep) (vimage Abs)"
    29 proof (rule Quotient3I)
    30   from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
    31   then show "\<And>xs. Rep -` (Abs -` xs) = xs"
    32     unfolding vimage_def by auto
    33 next
    34   show "\<And>xs. vset_rel R (Abs -` xs) (Abs -` xs)"
    35     unfolding vset_rel_def vimage_def
    36     by auto (metis Quotient3_rel_abs[OF assms])+
    37 next
    38   fix r s
    39   show "vset_rel R r s = (vset_rel R r r \<and> vset_rel R s s \<and> Rep -` r = Rep -` s)"
    40     unfolding vset_rel_def vimage_def set_eq_iff
    41     by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
    42 qed
    43 
    44 declare [[mapQ3 set = (vset_rel, set_quotient)]]
    45 
    46 lemma empty_set_rsp[quot_respect]:
    47   "vset_rel R {} {}"
    48   unfolding vset_rel_def by simp
    49 
    50 lemma collect_rsp[quot_respect]:
    51   assumes "Quotient3 R Abs Rep"
    52   shows "((R ===> op =) ===> vset_rel R) Collect Collect"
    53   by (intro fun_relI) (simp add: fun_rel_def vset_rel_def)
    54 
    55 lemma collect_prs[quot_preserve]:
    56   assumes "Quotient3 R Abs Rep"
    57   shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
    58   unfolding fun_eq_iff
    59   by (simp add: Quotient3_abs_rep[OF assms])
    60 
    61 lemma union_rsp[quot_respect]:
    62   assumes "Quotient3 R Abs Rep"
    63   shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<union> op \<union>"
    64   by (intro fun_relI) (simp add: vset_rel_def)
    65 
    66 lemma union_prs[quot_preserve]:
    67   assumes "Quotient3 R Abs Rep"
    68   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
    69   unfolding fun_eq_iff
    70   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    71 
    72 lemma diff_rsp[quot_respect]:
    73   assumes "Quotient3 R Abs Rep"
    74   shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op - op -"
    75   by (intro fun_relI) (simp add: vset_rel_def)
    76 
    77 lemma diff_prs[quot_preserve]:
    78   assumes "Quotient3 R Abs Rep"
    79   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
    80   unfolding fun_eq_iff
    81   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
    82 
    83 lemma inter_rsp[quot_respect]:
    84   assumes "Quotient3 R Abs Rep"
    85   shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<inter> op \<inter>"
    86   by (intro fun_relI) (auto simp add: vset_rel_def)
    87 
    88 lemma inter_prs[quot_preserve]:
    89   assumes "Quotient3 R Abs Rep"
    90   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
    91   unfolding fun_eq_iff
    92   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    93 
    94 lemma mem_prs[quot_preserve]:
    95   assumes "Quotient3 R Abs Rep"
    96   shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
    97   by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
    98 
    99 lemma mem_rsp[quot_respect]:
   100   shows "(R ===> vset_rel R ===> op =) op \<in> op \<in>"
   101   by (intro fun_relI) (simp add: vset_rel_def)
   102 
   103 end