author | kuncar |
Tue, 03 Apr 2012 16:26:48 +0200 | |
changeset 47308 | 9caab698dbe4 |
parent 47094 | 1a7ad2601cb5 |
child 47455 | 26315a545e26 |
permissions | -rw-r--r-- |
47308 | 1 |
(* Title: HOL/Library/Quotient3_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 |
|
80d460bc6fa8
Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
lemma set_quotient [quot_thm]: |
47308 | 12 |
assumes "Quotient3 R Abs Rep" |
13 |
shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)" |
|
14 |
proof (rule Quotient3I) |
|
15 |
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
|
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 |
47308 | 21 |
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
|
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 |
47308 | 26 |
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
|
27 |
qed |
80d460bc6fa8
Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
47308 | 29 |
declare [[mapQ3 set = (set_rel, set_quotient)]] |
47094 | 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]: |
47308 | 36 |
assumes "Quotient3 R Abs Rep" |
44413
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]: |
47308 | 41 |
assumes "Quotient3 R Abs Rep" |
44413
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 |
47308 | 44 |
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
|
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]: |
47308 | 47 |
assumes "Quotient3 R Abs Rep" |
44413
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]: |
47308 | 52 |
assumes "Quotient3 R Abs Rep" |
44413
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 |
47308 | 55 |
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
|
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]: |
47308 | 58 |
assumes "Quotient3 R Abs Rep" |
44413
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]: |
47308 | 63 |
assumes "Quotient3 R Abs Rep" |
44413
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 |
47308 | 66 |
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
|
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]: |
47308 | 69 |
assumes "Quotient3 R Abs Rep" |
44413
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]: |
47308 | 74 |
assumes "Quotient3 R Abs Rep" |
44413
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 |
47308 | 77 |
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
|
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]: |
47308 | 80 |
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
|
81 |
shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>" |
47308 | 82 |
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
|
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 |