author | bulwahn |
Wed, 14 Dec 2011 16:30:32 +0100 | |
changeset 45873 | 37ffb8797a63 |
parent 44873 | 045fedcfadf6 |
child 45970 | b6d0cff57d96 |
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" |
44873
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
79 |
shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>" |
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
80 |
using Quotient_abs_rep[OF assms] |
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
81 |
by(simp add: fun_eq_iff mem_def) |
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
82 |
|
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
83 |
lemma mem_rsp[quot_respect]: |
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
84 |
"(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)" |
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
85 |
by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE) |
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
86 |
|
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
87 |
lemma mem_prs2: |
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
88 |
assumes "Quotient R Abs Rep" |
44459
079ccfb074d9
Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44413
diff
changeset
|
89 |
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
|
90 |
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
|
91 |
|
44873
045fedcfadf6
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents:
44459
diff
changeset
|
92 |
lemma mem_rsp2: |
44459
079ccfb074d9
Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44413
diff
changeset
|
93 |
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
|
94 |
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
|
95 |
|
44413
80d460bc6fa8
Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
96 |
end |