src/HOL/Library/Quotient_Set.thy
author krauss
Sat Sep 10 22:43:17 2011 +0200 (2011-09-10)
changeset 44873 045fedcfadf6
parent 44459 079ccfb074d9
child 45970 b6d0cff57d96
permissions -rw-r--r--
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
     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 "Quotient R Abs Rep"
    13   shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
    14 proof (rule QuotientI)
    15   from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_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 Quotient_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 Quotient_def])+
    27 qed
    28 
    29 lemma empty_set_rsp[quot_respect]:
    30   "set_rel R {} {}"
    31   unfolding set_rel_def by simp
    32 
    33 lemma collect_rsp[quot_respect]:
    34   assumes "Quotient R Abs Rep"
    35   shows "((R ===> op =) ===> set_rel R) Collect Collect"
    36   by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
    37 
    38 lemma collect_prs[quot_preserve]:
    39   assumes "Quotient R Abs Rep"
    40   shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
    41   unfolding fun_eq_iff
    42   by (simp add: Quotient_abs_rep[OF assms])
    43 
    44 lemma union_rsp[quot_respect]:
    45   assumes "Quotient R Abs Rep"
    46   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
    47   by (intro fun_relI) (simp add: set_rel_def)
    48 
    49 lemma union_prs[quot_preserve]:
    50   assumes "Quotient R Abs Rep"
    51   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
    52   unfolding fun_eq_iff
    53   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
    54 
    55 lemma diff_rsp[quot_respect]:
    56   assumes "Quotient R Abs Rep"
    57   shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
    58   by (intro fun_relI) (simp add: set_rel_def)
    59 
    60 lemma diff_prs[quot_preserve]:
    61   assumes "Quotient R Abs Rep"
    62   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
    63   unfolding fun_eq_iff
    64   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
    65 
    66 lemma inter_rsp[quot_respect]:
    67   assumes "Quotient R Abs Rep"
    68   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
    69   by (intro fun_relI) (auto simp add: set_rel_def)
    70 
    71 lemma inter_prs[quot_preserve]:
    72   assumes "Quotient R Abs Rep"
    73   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
    74   unfolding fun_eq_iff
    75   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
    76 
    77 lemma mem_prs[quot_preserve]:
    78   assumes "Quotient R Abs Rep"
    79   shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>"
    80 using Quotient_abs_rep[OF assms]
    81 by(simp add: fun_eq_iff mem_def)
    82 
    83 lemma mem_rsp[quot_respect]:
    84   "(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)"
    85   by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE)
    86 
    87 lemma mem_prs2:
    88   assumes "Quotient R Abs Rep"
    89   shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
    90   by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
    91 
    92 lemma mem_rsp2:
    93   shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
    94   by (intro fun_relI) (simp add: set_rel_def)
    95 
    96 end