src/HOL/Library/Quotient_Set.thy
 author blanchet Thu Mar 06 15:40:33 2014 +0100 (2014-03-06) changeset 55945 e96383acecf9 parent 55940 7339ef350739 child 58881 b9556a055632 permissions -rw-r--r--
renamed 'fun_rel' to 'rel_fun'
```     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 {* Contravariant set map (vimage) and set relator, rules for the Quotient package *}
```
```    12
```
```    13 definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
```
```    14
```
```    15 lemma rel_vset_eq [id_simps]:
```
```    16   "rel_vset op = = op ="
```
```    17   by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)
```
```    18
```
```    19 lemma rel_vset_equivp:
```
```    20   assumes e: "equivp R"
```
```    21   shows "rel_vset R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
```
```    22   unfolding rel_vset_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 (rel_vset 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. rel_vset R (Abs -` xs) (Abs -` xs)"
```
```    35     unfolding rel_vset_def vimage_def
```
```    36     by auto (metis Quotient3_rel_abs[OF assms])+
```
```    37 next
```
```    38   fix r s
```
```    39   show "rel_vset R r s = (rel_vset R r r \<and> rel_vset R s s \<and> Rep -` r = Rep -` s)"
```
```    40     unfolding rel_vset_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 = (rel_vset, set_quotient)]]
```
```    45
```
```    46 lemma empty_set_rsp[quot_respect]:
```
```    47   "rel_vset R {} {}"
```
```    48   unfolding rel_vset_def by simp
```
```    49
```
```    50 lemma collect_rsp[quot_respect]:
```
```    51   assumes "Quotient3 R Abs Rep"
```
```    52   shows "((R ===> op =) ===> rel_vset R) Collect Collect"
```
```    53   by (intro rel_funI) (simp add: rel_fun_def rel_vset_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 "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
```
```    64   by (intro rel_funI) (simp add: rel_vset_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 "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
```
```    75   by (intro rel_funI) (simp add: rel_vset_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 "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
```
```    86   by (intro rel_funI) (auto simp add: rel_vset_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 ===> rel_vset R ===> op =) op \<in> op \<in>"
```
```   101   by (intro rel_funI) (simp add: rel_vset_def)
```
```   102
```
```   103 end
```