src/HOL/Library/Quotient_Set.thy
author wenzelm
Mon, 11 Apr 2016 15:26:58 +0200
changeset 62954 c5d0fdc260fa
parent 60500 903bb1495239
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned imports;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47455
26315a545e26 updated headers;
wenzelm
parents: 47308
diff changeset
     1
(*  Title:      HOL/Library/Quotient_Set.thy
44413
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Quotient infrastructure for the set type\<close>
44413
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
62954
c5d0fdc260fa tuned imports;
wenzelm
parents: 60500
diff changeset
     8
imports Quotient_Syntax
44413
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    11
subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close>
47626
f7b1034cb9ce move definition of set_rel into Library/Quotient_Set.thy
huffman
parents: 47455
diff changeset
    12
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    13
definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
47626
f7b1034cb9ce move definition of set_rel into Library/Quotient_Set.thy
huffman
parents: 47455
diff changeset
    14
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    15
lemma rel_vset_eq [id_simps]:
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    16
  "rel_vset op = = op ="
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    17
  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)
47626
f7b1034cb9ce move definition of set_rel into Library/Quotient_Set.thy
huffman
parents: 47455
diff changeset
    18
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    19
lemma rel_vset_equivp:
47626
f7b1034cb9ce move definition of set_rel into Library/Quotient_Set.thy
huffman
parents: 47455
diff changeset
    20
  assumes e: "equivp R"
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    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)"
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    22
  unfolding rel_vset_def
47626
f7b1034cb9ce move definition of set_rel into Library/Quotient_Set.thy
huffman
parents: 47455
diff changeset
    23
  using equivp_reflp[OF e]
f7b1034cb9ce move definition of set_rel into Library/Quotient_Set.thy
huffman
parents: 47455
diff changeset
    24
  by auto (metis, metis equivp_symp[OF e])
f7b1034cb9ce move definition of set_rel into Library/Quotient_Set.thy
huffman
parents: 47455
diff changeset
    25
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
lemma set_quotient [quot_thm]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    27
  assumes "Quotient3 R Abs Rep"
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    28
  shows "Quotient3 (rel_vset R) (vimage Rep) (vimage Abs)"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    29
proof (rule Quotient3I)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    30
  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
  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
    32
    unfolding vimage_def by auto
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
next
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    34
  show "\<And>xs. rel_vset R (Abs -` xs) (Abs -` xs)"
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    35
    unfolding rel_vset_def vimage_def
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    36
    by auto (metis Quotient3_rel_abs[OF assms])+
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
next
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
  fix r s
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    39
  show "rel_vset R r s = (rel_vset R r r \<and> rel_vset R s s \<and> Rep -` r = Rep -` s)"
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    40
    unfolding rel_vset_def vimage_def set_eq_iff
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    41
    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
qed
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    44
declare [[mapQ3 set = (rel_vset, set_quotient)]]
47094
1a7ad2601cb5 store the relational theorem for every relator
kuncar
parents: 45970
diff changeset
    45
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
lemma empty_set_rsp[quot_respect]:
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    47
  "rel_vset R {} {}"
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    48
  unfolding rel_vset_def by simp
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
lemma collect_rsp[quot_respect]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    51
  assumes "Quotient3 R Abs Rep"
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    52
  shows "((R ===> op =) ===> rel_vset R) Collect Collect"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55940
diff changeset
    53
  by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)
44413
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 collect_prs[quot_preserve]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    56
  assumes "Quotient3 R Abs Rep"
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
  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
    58
  unfolding fun_eq_iff
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    59
  by (simp add: Quotient3_abs_rep[OF assms])
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    60
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    61
lemma union_rsp[quot_respect]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    62
  assumes "Quotient3 R Abs Rep"
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    63
  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55940
diff changeset
    64
  by (intro rel_funI) (simp add: rel_vset_def)
44413
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 union_prs[quot_preserve]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    67
  assumes "Quotient3 R Abs Rep"
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
  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
    69
  unfolding fun_eq_iff
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    70
  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
lemma diff_rsp[quot_respect]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    73
  assumes "Quotient3 R Abs Rep"
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    74
  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55940
diff changeset
    75
  by (intro rel_funI) (simp add: rel_vset_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    76
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    77
lemma diff_prs[quot_preserve]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    78
  assumes "Quotient3 R Abs Rep"
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    79
  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
    80
  unfolding fun_eq_iff
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    81
  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    82
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    83
lemma inter_rsp[quot_respect]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    84
  assumes "Quotient3 R Abs Rep"
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
    85
  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55940
diff changeset
    86
  by (intro rel_funI) (auto simp add: rel_vset_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
lemma inter_prs[quot_preserve]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    89
  assumes "Quotient3 R Abs Rep"
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    90
  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
    91
  unfolding fun_eq_iff
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    92
  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    93
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    94
lemma mem_prs[quot_preserve]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    95
  assumes "Quotient3 R Abs Rep"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    96
  shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    97
  by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    98
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 44873
diff changeset
    99
lemma mem_rsp[quot_respect]:
55940
7339ef350739 renamed 'vset_rel' to 'rel_vset'
blanchet
parents: 53012
diff changeset
   100
  shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55940
diff changeset
   101
  by (intro rel_funI) (simp add: rel_vset_def)
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
   102
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   103
end