src/HOL/Library/Quotient_Set.thy
author kuncar
Fri Mar 23 14:20:09 2012 +0100 (2012-03-23)
changeset 47094 1a7ad2601cb5
parent 45970 b6d0cff57d96
child 47308 9caab698dbe4
permissions -rw-r--r--
store the relational theorem for every relator
kaliszyk@44413
     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
kaliszyk@44413
    11
lemma set_quotient [quot_thm]:
kaliszyk@44413
    12
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    13
  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
kaliszyk@44413
    14
proof (rule QuotientI)
kaliszyk@44413
    15
  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
kaliszyk@44413
    16
  then show "\<And>xs. Rep -` (Abs -` xs) = xs"
kaliszyk@44413
    17
    unfolding vimage_def by auto
kaliszyk@44413
    18
next
kaliszyk@44413
    19
  show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
kaliszyk@44413
    20
    unfolding set_rel_def vimage_def
kaliszyk@44413
    21
    by auto (metis Quotient_rel_abs[OF assms])+
kaliszyk@44413
    22
next
kaliszyk@44413
    23
  fix r s
kaliszyk@44413
    24
  show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
kaliszyk@44413
    25
    unfolding set_rel_def vimage_def set_eq_iff
kaliszyk@44413
    26
    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
kaliszyk@44413
    27
qed
kaliszyk@44413
    28
kuncar@47094
    29
declare [[map set = (set_rel, set_quotient)]]
kuncar@47094
    30
kaliszyk@44413
    31
lemma empty_set_rsp[quot_respect]:
kaliszyk@44413
    32
  "set_rel R {} {}"
kaliszyk@44413
    33
  unfolding set_rel_def by simp
kaliszyk@44413
    34
kaliszyk@44413
    35
lemma collect_rsp[quot_respect]:
kaliszyk@44413
    36
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    37
  shows "((R ===> op =) ===> set_rel R) Collect Collect"
kaliszyk@44459
    38
  by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
kaliszyk@44413
    39
kaliszyk@44413
    40
lemma collect_prs[quot_preserve]:
kaliszyk@44413
    41
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    42
  shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
kaliszyk@44413
    43
  unfolding fun_eq_iff
kaliszyk@44413
    44
  by (simp add: Quotient_abs_rep[OF assms])
kaliszyk@44413
    45
kaliszyk@44413
    46
lemma union_rsp[quot_respect]:
kaliszyk@44413
    47
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    48
  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
kaliszyk@44459
    49
  by (intro fun_relI) (simp add: set_rel_def)
kaliszyk@44413
    50
kaliszyk@44413
    51
lemma union_prs[quot_preserve]:
kaliszyk@44413
    52
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    53
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
kaliszyk@44413
    54
  unfolding fun_eq_iff
kaliszyk@44413
    55
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
kaliszyk@44413
    56
kaliszyk@44413
    57
lemma diff_rsp[quot_respect]:
kaliszyk@44413
    58
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    59
  shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
kaliszyk@44459
    60
  by (intro fun_relI) (simp add: set_rel_def)
kaliszyk@44413
    61
kaliszyk@44413
    62
lemma diff_prs[quot_preserve]:
kaliszyk@44413
    63
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    64
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
kaliszyk@44413
    65
  unfolding fun_eq_iff
kaliszyk@44413
    66
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
kaliszyk@44413
    67
kaliszyk@44413
    68
lemma inter_rsp[quot_respect]:
kaliszyk@44413
    69
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    70
  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
kaliszyk@44413
    71
  by (intro fun_relI) (auto simp add: set_rel_def)
kaliszyk@44413
    72
kaliszyk@44413
    73
lemma inter_prs[quot_preserve]:
kaliszyk@44413
    74
  assumes "Quotient R Abs Rep"
kaliszyk@44413
    75
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
kaliszyk@44413
    76
  unfolding fun_eq_iff
kaliszyk@44413
    77
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
kaliszyk@44413
    78
kaliszyk@44459
    79
lemma mem_prs[quot_preserve]:
kaliszyk@44459
    80
  assumes "Quotient R Abs Rep"
kaliszyk@44459
    81
  shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
kaliszyk@44459
    82
  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
kaliszyk@44459
    83
haftmann@45970
    84
lemma mem_rsp[quot_respect]:
kaliszyk@44459
    85
  shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
kaliszyk@44459
    86
  by (intro fun_relI) (simp add: set_rel_def)
kaliszyk@44459
    87
kaliszyk@44413
    88
end