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