src/HOL/Library/Quotient_Set.thy
author kuncar
Fri, 23 Mar 2012 14:20:09 +0100
changeset 47094 1a7ad2601cb5
parent 45970 b6d0cff57d96
child 47308 9caab698dbe4
permissions -rw-r--r--
store the relational theorem for every relator
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
47094
1a7ad2601cb5 store the relational theorem for every relator
kuncar
parents: 45970
diff changeset
    29
declare [[map set = (set_rel, set_quotient)]]
1a7ad2601cb5 store the relational theorem for every relator
kuncar
parents: 45970
diff changeset
    30
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
lemma empty_set_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
  "set_rel R {} {}"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
  unfolding set_rel_def by simp
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
lemma collect_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
  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
    38
  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
    39
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
lemma collect_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
  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
    43
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
  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
    45
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
lemma union_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    47
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
  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
    49
  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
    50
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
lemma union_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
  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
    54
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
  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
    56
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
lemma diff_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    58
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
  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
    60
  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
    61
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    62
lemma diff_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    64
  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
    65
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    66
  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
    67
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
lemma inter_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
  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
    71
  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
    72
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    73
lemma inter_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    74
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    75
  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
    76
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    77
  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
    78
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    79
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
    80
  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
    81
  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
    82
  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
    83
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 44873
diff changeset
    84
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
    85
  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
    86
  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
    87
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
end