author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 53012 | cb82606b8215 |
child 55940 | 7339ef350739 |
permissions | -rw-r--r-- |
47455 | 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 |
|
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 |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
52359
diff
changeset
|
11 |
subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *} |
47626
f7b1034cb9ce
move definition of set_rel into Library/Quotient_Set.thy
huffman
parents:
47455
diff
changeset
|
12 |
|
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
13 |
definition "vset_rel 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 |
|
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
15 |
lemma vset_rel_eq [id_simps]: |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
16 |
"vset_rel op = = op =" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
17 |
by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff vset_rel_def) |
47626
f7b1034cb9ce
move definition of set_rel into Library/Quotient_Set.thy
huffman
parents:
47455
diff
changeset
|
18 |
|
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
19 |
lemma vset_rel_equivp: |
47626
f7b1034cb9ce
move definition of set_rel into Library/Quotient_Set.thy
huffman
parents:
47455
diff
changeset
|
20 |
assumes e: "equivp R" |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
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)" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
22 |
unfolding vset_rel_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 | 27 |
assumes "Quotient3 R Abs Rep" |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
28 |
shows "Quotient3 (vset_rel R) (vimage Rep) (vimage Abs)" |
47308 | 29 |
proof (rule Quotient3I) |
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 |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
34 |
show "\<And>xs. vset_rel R (Abs -` xs) (Abs -` xs)" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
35 |
unfolding vset_rel_def vimage_def |
47308 | 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 |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
39 |
show "vset_rel R r s = (vset_rel R r r \<and> vset_rel R s s \<and> Rep -` r = Rep -` s)" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
40 |
unfolding vset_rel_def vimage_def set_eq_iff |
47308 | 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 |
|
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
44 |
declare [[mapQ3 set = (vset_rel, set_quotient)]] |
47094 | 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]: |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
47 |
"vset_rel R {} {}" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
48 |
unfolding vset_rel_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 | 51 |
assumes "Quotient3 R Abs Rep" |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
52 |
shows "((R ===> op =) ===> vset_rel R) Collect Collect" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
53 |
by (intro fun_relI) (simp add: fun_rel_def vset_rel_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 | 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 | 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 | 62 |
assumes "Quotient3 R Abs Rep" |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
63 |
shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<union> op \<union>" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
64 |
by (intro fun_relI) (simp add: vset_rel_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 | 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 | 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 | 73 |
assumes "Quotient3 R Abs Rep" |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
74 |
shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op - op -" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
75 |
by (intro fun_relI) (simp add: vset_rel_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 | 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 | 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 | 84 |
assumes "Quotient3 R Abs Rep" |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
85 |
shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<inter> op \<inter>" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
86 |
by (intro fun_relI) (auto simp add: vset_rel_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 | 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 | 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 | 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 | 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]: |
47647
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
100 |
shows "(R ===> vset_rel R ===> op =) op \<in> op \<in>" |
ec29cc09599d
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
huffman
parents:
47626
diff
changeset
|
101 |
by (intro fun_relI) (simp add: vset_rel_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 |