src/HOL/Library/Quotient_Set.thy
 author Cezary Kaliszyk Tue Aug 23 03:34:17 2011 +0900 (2011-08-23) changeset 44413 80d460bc6fa8 child 44459 079ccfb074d9 permissions -rw-r--r--
Quotient Package: some infrastructure for lifting inside sets
```     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 (auto 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) (auto 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) (auto 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 end
```