src/HOL/Library/Quotient_Set.thy
author haftmann
Sat, 24 Dec 2011 15:53:10 +0100
changeset 45970 b6d0cff57d96
parent 44873 045fedcfadf6
child 47094 1a7ad2601cb5
permissions -rw-r--r--
adjusted to set/pred distinction by means of type constructor `set`
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
(*  Title:      HOL/Library/Quotient_Set.thy
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk and Christian Urban
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
*)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
header {* Quotient infrastructure for the set type *}
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
theory Quotient_Set
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
imports Main Quotient_Syntax
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
begin
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
lemma set_quotient [quot_thm]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
proof (rule QuotientI)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
  then show "\<And>xs. Rep -` (Abs -` xs) = xs"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
    unfolding vimage_def by auto
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
next
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
  show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
    unfolding set_rel_def vimage_def
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
    by auto (metis Quotient_rel_abs[OF assms])+
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
next
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
  fix r s
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
  show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    25
    unfolding set_rel_def vimage_def set_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
qed
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
lemma empty_set_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
  "set_rel R {} {}"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
  unfolding set_rel_def by simp
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
lemma collect_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
  shows "((R ===> op =) ===> set_rel R) Collect Collect"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    36
  by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
lemma collect_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
  shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
  by (simp add: Quotient_abs_rep[OF assms])
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
lemma union_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    47
  by (intro fun_relI) (simp add: set_rel_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
lemma union_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
lemma diff_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
  shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    58
  by (intro fun_relI) (simp add: set_rel_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    60
lemma diff_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    61
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    62
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    64
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    65
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    66
lemma inter_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    67
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
  by (intro fun_relI) (auto simp add: set_rel_def)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
lemma inter_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    73
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    74
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    75
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    76
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    77
lemma mem_prs[quot_preserve]:
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    78
  assumes "Quotient R Abs Rep"
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    79
  shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    80
  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    81
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 44873
diff changeset
    82
lemma mem_rsp[quot_respect]:
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    83
  shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    84
  by (intro fun_relI) (simp add: set_rel_def)
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    85
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    86
end