author | blanchet |
Mon, 23 Jan 2012 17:40:32 +0100 | |
changeset 46320 | 0b8b73b49848 |
parent 45970 | b6d0cff57d96 |
child 47094 | 1a7ad2601cb5 |
permissions | -rw-r--r-- |
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 |