src/HOL/Library/Quotient_Set.thy
author wenzelm
Fri Apr 13 14:00:26 2012 +0200 (2012-04-13)
changeset 47455 26315a545e26
parent 47308 9caab698dbe4
child 47626 f7b1034cb9ce
permissions -rw-r--r--
updated headers;
     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 lemma set_quotient [quot_thm]:
    12   assumes "Quotient3 R Abs Rep"
    13   shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
    14 proof (rule Quotient3I)
    15   from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
    16   then show "\<And>xs. Rep -` (Abs -` xs) = xs"
    17     unfolding vimage_def by auto
    18 next
    19   show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
    20     unfolding set_rel_def vimage_def
    21     by auto (metis Quotient3_rel_abs[OF assms])+
    22 next
    23   fix r s
    24   show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
    25     unfolding set_rel_def vimage_def set_eq_iff
    26     by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
    27 qed
    28 
    29 declare [[mapQ3 set = (set_rel, set_quotient)]]
    30 
    31 lemma empty_set_rsp[quot_respect]:
    32   "set_rel R {} {}"
    33   unfolding set_rel_def by simp
    34 
    35 lemma collect_rsp[quot_respect]:
    36   assumes "Quotient3 R Abs Rep"
    37   shows "((R ===> op =) ===> set_rel R) Collect Collect"
    38   by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
    39 
    40 lemma collect_prs[quot_preserve]:
    41   assumes "Quotient3 R Abs Rep"
    42   shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
    43   unfolding fun_eq_iff
    44   by (simp add: Quotient3_abs_rep[OF assms])
    45 
    46 lemma union_rsp[quot_respect]:
    47   assumes "Quotient3 R Abs Rep"
    48   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
    49   by (intro fun_relI) (simp add: set_rel_def)
    50 
    51 lemma union_prs[quot_preserve]:
    52   assumes "Quotient3 R Abs Rep"
    53   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
    54   unfolding fun_eq_iff
    55   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    56 
    57 lemma diff_rsp[quot_respect]:
    58   assumes "Quotient3 R Abs Rep"
    59   shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
    60   by (intro fun_relI) (simp add: set_rel_def)
    61 
    62 lemma diff_prs[quot_preserve]:
    63   assumes "Quotient3 R Abs Rep"
    64   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
    65   unfolding fun_eq_iff
    66   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
    67 
    68 lemma inter_rsp[quot_respect]:
    69   assumes "Quotient3 R Abs Rep"
    70   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
    71   by (intro fun_relI) (auto simp add: set_rel_def)
    72 
    73 lemma inter_prs[quot_preserve]:
    74   assumes "Quotient3 R Abs Rep"
    75   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
    76   unfolding fun_eq_iff
    77   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    78 
    79 lemma mem_prs[quot_preserve]:
    80   assumes "Quotient3 R Abs Rep"
    81   shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
    82   by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
    83 
    84 lemma mem_rsp[quot_respect]:
    85   shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
    86   by (intro fun_relI) (simp add: set_rel_def)
    87 
    88 end