author | wenzelm |
Mon, 12 Apr 2021 14:14:47 +0200 | |
changeset 73563 | 55b66a45bc94 |
parent 73139 | be9b73dfd3e0 |
child 74590 | 00ffae972fc0 |
permissions | -rw-r--r-- |
63653 | 1 |
(* Title: HOL/Equiv_Relations.thy |
2 |
Author: Lawrence C Paulson, 1996 Cambridge University Computer Laboratory |
|
15300 | 3 |
*) |
4 |
||
60758 | 5 |
section \<open>Equivalence Relations in Higher-Order Set Theory\<close> |
15300 | 6 |
|
7 |
theory Equiv_Relations |
|
66364 | 8 |
imports Groups_Big |
15300 | 9 |
begin |
10 |
||
60758 | 11 |
subsection \<open>Equivalence relations -- set version\<close> |
15300 | 12 |
|
63653 | 13 |
definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" |
14 |
where "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r" |
|
15300 | 15 |
|
63653 | 16 |
lemma equivI: "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r" |
40815 | 17 |
by (simp add: equiv_def) |
18 |
||
19 |
lemma equivE: |
|
20 |
assumes "equiv A r" |
|
21 |
obtains "refl_on A r" and "sym r" and "trans r" |
|
22 |
using assms by (simp add: equiv_def) |
|
23 |
||
60758 | 24 |
text \<open> |
63653 | 25 |
Suppes, Theorem 70: \<open>r\<close> is an equiv relation iff \<open>r\<inverse> O r = r\<close>. |
15300 | 26 |
|
63653 | 27 |
First half: \<open>equiv A r \<Longrightarrow> r\<inverse> O r = r\<close>. |
60758 | 28 |
\<close> |
15300 | 29 |
|
63653 | 30 |
lemma sym_trans_comp_subset: "sym r \<Longrightarrow> trans r \<Longrightarrow> r\<inverse> O r \<subseteq> r" |
31 |
unfolding trans_def sym_def converse_unfold by blast |
|
15300 | 32 |
|
63653 | 33 |
lemma refl_on_comp_subset: "refl_on A r \<Longrightarrow> r \<subseteq> r\<inverse> O r" |
34 |
unfolding refl_on_def by blast |
|
15300 | 35 |
|
63653 | 36 |
lemma equiv_comp_eq: "equiv A r \<Longrightarrow> r\<inverse> O r = r" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
37 |
unfolding equiv_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
38 |
by (iprover intro: sym_trans_comp_subset refl_on_comp_subset equalityI) |
15300 | 39 |
|
60758 | 40 |
text \<open>Second half.\<close> |
15300 | 41 |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
42 |
lemma comp_equivI: |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
43 |
assumes "r\<inverse> O r = r" "Domain r = A" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
44 |
shows "equiv A r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
45 |
proof - |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
46 |
have *: "\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
47 |
using assms by blast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
48 |
show ?thesis |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
49 |
unfolding equiv_def refl_on_def sym_def trans_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
50 |
using assms by (auto intro: *) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
51 |
qed |
15300 | 52 |
|
53 |
||
60758 | 54 |
subsection \<open>Equivalence classes\<close> |
15300 | 55 |
|
63653 | 56 |
lemma equiv_class_subset: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> r``{a} \<subseteq> r``{b}" |
61799 | 57 |
\<comment> \<open>lemma for the next result\<close> |
63653 | 58 |
unfolding equiv_def trans_def sym_def by blast |
15300 | 59 |
|
63653 | 60 |
theorem equiv_class_eq: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> r``{a} = r``{b}" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
61 |
by (intro equalityI equiv_class_subset; force simp add: equiv_def sym_def) |
15300 | 62 |
|
63653 | 63 |
lemma equiv_class_self: "equiv A r \<Longrightarrow> a \<in> A \<Longrightarrow> a \<in> r``{a}" |
64 |
unfolding equiv_def refl_on_def by blast |
|
15300 | 65 |
|
63653 | 66 |
lemma subset_equiv_class: "equiv A r \<Longrightarrow> r``{b} \<subseteq> r``{a} \<Longrightarrow> b \<in> A \<Longrightarrow> (a, b) \<in> r" |
61799 | 67 |
\<comment> \<open>lemma for the next result\<close> |
63653 | 68 |
unfolding equiv_def refl_on_def by blast |
15300 | 69 |
|
63653 | 70 |
lemma eq_equiv_class: "r``{a} = r``{b} \<Longrightarrow> equiv A r \<Longrightarrow> b \<in> A \<Longrightarrow> (a, b) \<in> r" |
17589 | 71 |
by (iprover intro: equalityD2 subset_equiv_class) |
15300 | 72 |
|
63653 | 73 |
lemma equiv_class_nondisjoint: "equiv A r \<Longrightarrow> x \<in> (r``{a} \<inter> r``{b}) \<Longrightarrow> (a, b) \<in> r" |
74 |
unfolding equiv_def trans_def sym_def by blast |
|
15300 | 75 |
|
63653 | 76 |
lemma equiv_type: "equiv A r \<Longrightarrow> r \<subseteq> A \<times> A" |
77 |
unfolding equiv_def refl_on_def by blast |
|
15300 | 78 |
|
63653 | 79 |
lemma equiv_class_eq_iff: "equiv A r \<Longrightarrow> (x, y) \<in> r \<longleftrightarrow> r``{x} = r``{y} \<and> x \<in> A \<and> y \<in> A" |
15300 | 80 |
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
81 |
||
63653 | 82 |
lemma eq_equiv_class_iff: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> r``{x} = r``{y} \<longleftrightarrow> (x, y) \<in> r" |
15300 | 83 |
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
84 |
||
85 |
||
60758 | 86 |
subsection \<open>Quotients\<close> |
15300 | 87 |
|
63653 | 88 |
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) |
89 |
where "A//r = (\<Union>x \<in> A. {r``{x}})" \<comment> \<open>set of equiv classes\<close> |
|
15300 | 90 |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
91 |
lemma quotientI: "x \<in> A \<Longrightarrow> r``{x} \<in> A//r" |
63653 | 92 |
unfolding quotient_def by blast |
15300 | 93 |
|
63653 | 94 |
lemma quotientE: "X \<in> A//r \<Longrightarrow> (\<And>x. X = r``{x} \<Longrightarrow> x \<in> A \<Longrightarrow> P) \<Longrightarrow> P" |
95 |
unfolding quotient_def by blast |
|
15300 | 96 |
|
63653 | 97 |
lemma Union_quotient: "equiv A r \<Longrightarrow> \<Union>(A//r) = A" |
98 |
unfolding equiv_def refl_on_def quotient_def by blast |
|
15300 | 99 |
|
63653 | 100 |
lemma quotient_disj: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> X = Y \<or> X \<inter> Y = {}" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
101 |
unfolding quotient_def equiv_def trans_def sym_def by blast |
15300 | 102 |
|
103 |
lemma quotient_eqI: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
104 |
assumes "equiv A r" "X \<in> A//r" "Y \<in> A//r" and xy: "x \<in> X" "y \<in> Y" "(x, y) \<in> r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
105 |
shows "X = Y" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
106 |
proof - |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
107 |
obtain a b where "a \<in> A" and a: "X = r `` {a}" and "b \<in> A" and b: "Y = r `` {b}" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
108 |
using assms by (auto elim!: quotientE) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
109 |
then have "(a,b) \<in> r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
110 |
using xy \<open>equiv A r\<close> unfolding equiv_def sym_def trans_def by blast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
111 |
then show ?thesis |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
112 |
unfolding a b by (rule equiv_class_eq [OF \<open>equiv A r\<close>]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
113 |
qed |
15300 | 114 |
|
115 |
lemma quotient_eq_iff: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
116 |
assumes "equiv A r" "X \<in> A//r" "Y \<in> A//r" and xy: "x \<in> X" "y \<in> Y" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
117 |
shows "X = Y \<longleftrightarrow> (x, y) \<in> r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
118 |
proof |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
119 |
assume L: "X = Y" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
120 |
with assms show "(x, y) \<in> r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
121 |
unfolding equiv_def sym_def trans_def by (blast elim!: quotientE) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
122 |
next |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
123 |
assume \<section>: "(x, y) \<in> r" show "X = Y" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
124 |
by (rule quotient_eqI) (use \<section> assms in \<open>blast+\<close>) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
125 |
qed |
15300 | 126 |
|
63653 | 127 |
lemma eq_equiv_class_iff2: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> {x}//r = {y}//r \<longleftrightarrow> (x, y) \<in> r" |
128 |
by (simp add: quotient_def eq_equiv_class_iff) |
|
15300 | 129 |
|
130 |
lemma quotient_empty [simp]: "{}//r = {}" |
|
63653 | 131 |
by (simp add: quotient_def) |
15300 | 132 |
|
63653 | 133 |
lemma quotient_is_empty [iff]: "A//r = {} \<longleftrightarrow> A = {}" |
134 |
by (simp add: quotient_def) |
|
15300 | 135 |
|
63653 | 136 |
lemma quotient_is_empty2 [iff]: "{} = A//r \<longleftrightarrow> A = {}" |
137 |
by (simp add: quotient_def) |
|
15300 | 138 |
|
15302 | 139 |
lemma singleton_quotient: "{x}//r = {r `` {x}}" |
63653 | 140 |
by (simp add: quotient_def) |
15302 | 141 |
|
63653 | 142 |
lemma quotient_diff1: "inj_on (\<lambda>a. {a}//r) A \<Longrightarrow> a \<in> A \<Longrightarrow> (A - {a})//r = A//r - {a}//r" |
143 |
unfolding quotient_def inj_on_def by blast |
|
144 |
||
15302 | 145 |
|
60758 | 146 |
subsection \<open>Refinement of one equivalence relation WRT another\<close> |
59528
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
147 |
|
63653 | 148 |
lemma refines_equiv_class_eq: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> R``(S``{a}) = S``{a}" |
59528
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
149 |
by (auto simp: equiv_class_eq_iff) |
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
150 |
|
63653 | 151 |
lemma refines_equiv_class_eq2: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> S``(R``{a}) = S``{a}" |
59528
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
152 |
by (auto simp: equiv_class_eq_iff) |
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
153 |
|
63653 | 154 |
lemma refines_equiv_image_eq: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> (\<lambda>X. S``X) ` (A//R) = A//S" |
59528
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
155 |
by (auto simp: quotient_def image_UN refines_equiv_class_eq2) |
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
156 |
|
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
157 |
lemma finite_refines_finite: |
63653 | 158 |
"finite (A//R) \<Longrightarrow> R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> finite (A//S)" |
159 |
by (erule finite_surj [where f = "\<lambda>X. S``X"]) (simp add: refines_equiv_image_eq) |
|
59528
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
160 |
|
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
161 |
lemma finite_refines_card_le: |
63653 | 162 |
"finite (A//R) \<Longrightarrow> R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> card (A//S) \<le> card (A//R)" |
163 |
by (subst refines_equiv_image_eq [of R S A, symmetric]) |
|
164 |
(auto simp: card_image_le [where f = "\<lambda>X. S``X"]) |
|
59528
4862f3dc9540
new lemmas re refinement of one equivalence relation WRT another
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
165 |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
166 |
|
60758 | 167 |
subsection \<open>Defining unary operations upon equivalence classes\<close> |
15300 | 168 |
|
63653 | 169 |
text \<open>A congruence-preserving function.\<close> |
40816
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset
|
170 |
|
63653 | 171 |
definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
172 |
where "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)" |
|
40816
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset
|
173 |
|
63653 | 174 |
lemma congruentI: "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f" |
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
175 |
by (auto simp add: congruent_def) |
40816
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset
|
176 |
|
63653 | 177 |
lemma congruentD: "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z" |
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
178 |
by (auto simp add: congruent_def) |
15300 | 179 |
|
63653 | 180 |
abbreviation RESPECTS :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr "respects" 80) |
181 |
where "f respects r \<equiv> congruent r f" |
|
15300 | 182 |
|
183 |
||
63653 | 184 |
lemma UN_constant_eq: "a \<in> A \<Longrightarrow> \<forall>y \<in> A. f y = c \<Longrightarrow> (\<Union>y \<in> A. f y) = c" |
61799 | 185 |
\<comment> \<open>lemma required to prove \<open>UN_equiv_class\<close>\<close> |
15300 | 186 |
by auto |
187 |
||
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
188 |
lemma UN_equiv_class: |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
189 |
assumes "equiv A r" "f respects r" "a \<in> A" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
190 |
shows "(\<Union>x \<in> r``{a}. f x) = f a" |
61799 | 191 |
\<comment> \<open>Conversion rule\<close> |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
192 |
proof - |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
193 |
have \<section>: "\<forall>x\<in>r `` {a}. f x = f a" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
194 |
using assms unfolding equiv_def congruent_def sym_def by blast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
195 |
show ?thesis |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
196 |
by (iprover intro: assms UN_constant_eq [OF equiv_class_self \<section>]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
197 |
qed |
15300 | 198 |
|
199 |
lemma UN_equiv_class_type: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
200 |
assumes r: "equiv A r" "f respects r" and X: "X \<in> A//r" and AB: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
201 |
shows "(\<Union>x \<in> X. f x) \<in> B" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
202 |
using assms unfolding quotient_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
203 |
by (auto simp: UN_equiv_class [OF r]) |
15300 | 204 |
|
60758 | 205 |
text \<open> |
15300 | 206 |
Sufficient conditions for injectiveness. Could weaken premises! |
63653 | 207 |
major premise could be an inclusion; \<open>bcong\<close> could be |
208 |
\<open>\<And>y. y \<in> A \<Longrightarrow> f y \<in> B\<close>. |
|
60758 | 209 |
\<close> |
15300 | 210 |
|
211 |
lemma UN_equiv_class_inject: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
212 |
assumes "equiv A r" "f respects r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
213 |
and eq: "(\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y)" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
214 |
and X: "X \<in> A//r" and Y: "Y \<in> A//r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
215 |
and fr: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> (x, y) \<in> r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
216 |
shows "X = Y" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
217 |
proof - |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
218 |
obtain a b where "a \<in> A" and a: "X = r `` {a}" and "b \<in> A" and b: "Y = r `` {b}" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
219 |
using assms by (auto elim!: quotientE) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
220 |
then have "\<Union> (f ` r `` {a}) = f a" "\<Union> (f ` r `` {b}) = f b" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
221 |
by (iprover intro: UN_equiv_class [OF \<open>equiv A r\<close>] assms)+ |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
222 |
then have "f a = f b" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
223 |
using eq unfolding a b by (iprover intro: trans sym) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
224 |
then have "(a,b) \<in> r" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
225 |
using fr \<open>a \<in> A\<close> \<open>b \<in> A\<close> by blast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
226 |
then show ?thesis |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
227 |
unfolding a b by (rule equiv_class_eq [OF \<open>equiv A r\<close>]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
228 |
qed |
15300 | 229 |
|
230 |
||
60758 | 231 |
subsection \<open>Defining binary operations upon equivalence classes\<close> |
15300 | 232 |
|
63653 | 233 |
text \<open>A congruence-preserving function of two arguments.\<close> |
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
234 |
|
63653 | 235 |
definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" |
236 |
where "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)" |
|
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
237 |
|
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
238 |
lemma congruent2I': |
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
239 |
assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2" |
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
240 |
shows "congruent2 r1 r2 f" |
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
241 |
using assms by (auto simp add: congruent2_def) |
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset
|
242 |
|
63653 | 243 |
lemma congruent2D: "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2" |
63092 | 244 |
by (auto simp add: congruent2_def) |
15300 | 245 |
|
63653 | 246 |
text \<open>Abbreviation for the common case where the relations are identical.\<close> |
247 |
abbreviation RESPECTS2:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr "respects2" 80) |
|
248 |
where "f respects2 r \<equiv> congruent2 r r f" |
|
19979 | 249 |
|
15300 | 250 |
|
251 |
lemma congruent2_implies_congruent: |
|
63653 | 252 |
"equiv A r1 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a \<in> A \<Longrightarrow> congruent r2 (f a)" |
253 |
unfolding congruent_def congruent2_def equiv_def refl_on_def by blast |
|
15300 | 254 |
|
255 |
lemma congruent2_implies_congruent_UN: |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
256 |
assumes "equiv A1 r1" "equiv A2 r2" "congruent2 r1 r2 f" "a \<in> A2" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
257 |
shows "congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2``{a}. f x1 x2)" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
258 |
unfolding congruent_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
259 |
proof clarify |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
260 |
fix c d |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
261 |
assume cd: "(c,d) \<in> r1" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
262 |
then have "c \<in> A1" "d \<in> A1" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
263 |
using \<open>equiv A1 r1\<close> by (auto elim!: equiv_type [THEN subsetD, THEN SigmaE2]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
264 |
with assms show "\<Union> (f c ` r2 `` {a}) = \<Union> (f d ` r2 `` {a})" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
265 |
proof (simp add: UN_equiv_class congruent2_implies_congruent) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
266 |
show "f c a = f d a" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
267 |
using assms cd unfolding congruent2_def equiv_def refl_on_def by blast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
268 |
qed |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
269 |
qed |
15300 | 270 |
|
271 |
lemma UN_equiv_class2: |
|
63653 | 272 |
"equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a1 \<in> A1 \<Longrightarrow> a2 \<in> A2 \<Longrightarrow> |
273 |
(\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2" |
|
274 |
by (simp add: UN_equiv_class congruent2_implies_congruent congruent2_implies_congruent_UN) |
|
15300 | 275 |
|
276 |
lemma UN_equiv_class_type2: |
|
63653 | 277 |
"equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f |
278 |
\<Longrightarrow> X1 \<in> A1//r1 \<Longrightarrow> X2 \<in> A2//r2 |
|
279 |
\<Longrightarrow> (\<And>x1 x2. x1 \<in> A1 \<Longrightarrow> x2 \<in> A2 \<Longrightarrow> f x1 x2 \<in> B) |
|
280 |
\<Longrightarrow> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B" |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
281 |
unfolding quotient_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
282 |
by (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
283 |
congruent2_implies_congruent quotientI) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
284 |
|
15300 | 285 |
|
286 |
lemma UN_UN_split_split_eq: |
|
287 |
"(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) = |
|
288 |
(\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)" |
|
61799 | 289 |
\<comment> \<open>Allows a natural expression of binary operators,\<close> |
290 |
\<comment> \<open>without explicit calls to \<open>split\<close>\<close> |
|
15300 | 291 |
by auto |
292 |
||
293 |
lemma congruent2I: |
|
63653 | 294 |
"equiv A1 r1 \<Longrightarrow> equiv A2 r2 |
295 |
\<Longrightarrow> (\<And>y z w. w \<in> A2 \<Longrightarrow> (y,z) \<in> r1 \<Longrightarrow> f y w = f z w) |
|
296 |
\<Longrightarrow> (\<And>y z w. w \<in> A1 \<Longrightarrow> (y,z) \<in> r2 \<Longrightarrow> f w y = f w z) |
|
297 |
\<Longrightarrow> congruent2 r1 r2 f" |
|
61799 | 298 |
\<comment> \<open>Suggested by John Harrison -- the two subproofs may be\<close> |
63653 | 299 |
\<comment> \<open>\<^emph>\<open>much\<close> simpler than the direct proof.\<close> |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
300 |
unfolding congruent2_def equiv_def refl_on_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
301 |
by (blast intro: trans) |
15300 | 302 |
|
303 |
lemma congruent2_commuteI: |
|
304 |
assumes equivA: "equiv A r" |
|
63653 | 305 |
and commute: "\<And>y z. y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> f y z = f z y" |
306 |
and congt: "\<And>y z w. w \<in> A \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> f w y = f w z" |
|
15300 | 307 |
shows "f respects2 r" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
308 |
proof (rule congruent2I [OF equivA equivA]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
309 |
note eqv = equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2] |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
310 |
show "\<And>y z w. \<lbrakk>w \<in> A; (y, z) \<in> r\<rbrakk> \<Longrightarrow> f y w = f z w" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
311 |
by (iprover intro: commute [THEN trans] sym congt elim: eqv) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
312 |
show "\<And>y z w. \<lbrakk>w \<in> A; (y, z) \<in> r\<rbrakk> \<Longrightarrow> f w y = f w z" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
313 |
by (iprover intro: congt elim: eqv) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
314 |
qed |
15300 | 315 |
|
24728 | 316 |
|
60758 | 317 |
subsection \<open>Quotients and finiteness\<close> |
24728 | 318 |
|
60758 | 319 |
text \<open>Suggested by Florian Kammüller\<close> |
24728 | 320 |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
321 |
lemma finite_quotient: |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
322 |
assumes "finite A" "r \<subseteq> A \<times> A" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
323 |
shows "finite (A//r)" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
324 |
\<comment> \<open>recall @{thm equiv_type}\<close> |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
325 |
proof - |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
326 |
have "A//r \<subseteq> Pow A" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
327 |
using assms unfolding quotient_def by blast |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
328 |
moreover have "finite (Pow A)" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
329 |
using assms by simp |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
330 |
ultimately show ?thesis |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
331 |
by (iprover intro: finite_subset) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
332 |
qed |
24728 | 333 |
|
63653 | 334 |
lemma finite_equiv_class: "finite A \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> X \<in> A//r \<Longrightarrow> finite X" |
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
335 |
unfolding quotient_def |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
336 |
by (erule rev_finite_subset) blast |
24728 | 337 |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
338 |
lemma equiv_imp_dvd_card: |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
339 |
assumes "finite A" "equiv A r" "\<And>X. X \<in> A//r \<Longrightarrow> k dvd card X" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
340 |
shows "k dvd card A" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
341 |
proof (rule Union_quotient [THEN subst]) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
342 |
show "k dvd card (\<Union> (A // r))" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
343 |
apply (rule dvd_partition) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
344 |
using assms |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
345 |
by (auto simp: Union_quotient dest: quotient_disj) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
346 |
qed (use assms in blast) |
24728 | 347 |
|
71608
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
348 |
lemma card_quotient_disjoint: |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
349 |
assumes "finite A" "inj_on (\<lambda>x. {x} // r) A" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
350 |
shows "card (A//r) = card A" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
351 |
proof - |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
352 |
have "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> r `` {j} \<noteq> r `` {i}" |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
353 |
using assms by (fastforce simp add: quotient_def inj_on_def) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
354 |
with assms show ?thesis |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
355 |
by (simp add: quotient_def card_UN_disjoint) |
856c68ab6f13
structured a lot of ancient, horrible proofs
paulson <lp15@cam.ac.uk>
parents:
71393
diff
changeset
|
356 |
qed |
24728 | 357 |
|
73139 | 358 |
text \<open>By Jakub Kądziołka:\<close> |
359 |
||
360 |
lemma sum_fun_comp: |
|
361 |
assumes "finite S" "finite R" "g ` S \<subseteq> R" |
|
362 |
shows "(\<Sum>x \<in> S. f (g x)) = (\<Sum>y \<in> R. of_nat (card {x \<in> S. g x = y}) * f y)" |
|
363 |
proof - |
|
364 |
let ?r = "relation_of (\<lambda>p q. g p = g q) S" |
|
365 |
have eqv: "equiv S ?r" |
|
366 |
unfolding relation_of_def by (auto intro: comp_equivI) |
|
367 |
have finite: "C \<in> S//?r \<Longrightarrow> finite C" for C |
|
368 |
by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]]) |
|
369 |
have disjoint: "A \<in> S//?r \<Longrightarrow> B \<in> S//?r \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}" for A B |
|
370 |
using eqv quotient_disj by blast |
|
371 |
||
372 |
let ?cls = "\<lambda>y. {x \<in> S. y = g x}" |
|
373 |
have quot_as_img: "S//?r = ?cls ` g ` S" |
|
374 |
by (auto simp add: relation_of_def quotient_def) |
|
375 |
have cls_inj: "inj_on ?cls (g ` S)" |
|
376 |
by (auto intro: inj_onI) |
|
377 |
||
378 |
have rest_0: "(\<Sum>y \<in> R - g ` S. of_nat (card (?cls y)) * f y) = 0" |
|
379 |
proof - |
|
380 |
have "of_nat (card (?cls y)) * f y = 0" if asm: "y \<in> R - g ` S" for y |
|
381 |
proof - |
|
382 |
from asm have *: "?cls y = {}" by auto |
|
383 |
show ?thesis unfolding * by simp |
|
384 |
qed |
|
385 |
thus ?thesis by simp |
|
386 |
qed |
|
387 |
||
388 |
have "(\<Sum>x \<in> S. f (g x)) = (\<Sum>C \<in> S//?r. \<Sum>x \<in> C. f (g x))" |
|
389 |
using eqv finite disjoint |
|
390 |
by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient) |
|
391 |
also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f (g x))" |
|
392 |
unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj]) |
|
393 |
also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f y)" |
|
394 |
by auto |
|
395 |
also have "... = (\<Sum>y \<in> g ` S. of_nat (card (?cls y)) * f y)" |
|
396 |
by (simp flip: sum_constant) |
|
397 |
also have "... = (\<Sum>y \<in> R. of_nat (card (?cls y)) * f y)" |
|
398 |
using rest_0 by (simp add: sum.subset_diff[OF \<open>g ` S \<subseteq> R\<close> \<open>finite R\<close>]) |
|
399 |
finally show ?thesis |
|
400 |
by (simp add: eq_commute) |
|
401 |
qed |
|
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
402 |
|
60758 | 403 |
subsection \<open>Projection\<close> |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
404 |
|
63653 | 405 |
definition proj :: "('b \<times> 'a) set \<Rightarrow> 'b \<Rightarrow> 'a set" |
406 |
where "proj r x = r `` {x}" |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
407 |
|
63653 | 408 |
lemma proj_preserves: "x \<in> A \<Longrightarrow> proj r x \<in> A//r" |
409 |
unfolding proj_def by (rule quotientI) |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
410 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
411 |
lemma proj_in_iff: |
63653 | 412 |
assumes "equiv A r" |
413 |
shows "proj r x \<in> A//r \<longleftrightarrow> x \<in> A" |
|
414 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
415 |
proof |
|
416 |
assume ?rhs |
|
417 |
then show ?lhs by (simp add: proj_preserves) |
|
418 |
next |
|
419 |
assume ?lhs |
|
420 |
then show ?rhs |
|
421 |
unfolding proj_def quotient_def |
|
422 |
proof clarsimp |
|
423 |
fix y |
|
424 |
assume y: "y \<in> A" and "r `` {x} = r `` {y}" |
|
425 |
moreover have "y \<in> r `` {y}" |
|
426 |
using assms y unfolding equiv_def refl_on_def by blast |
|
427 |
ultimately have "(x, y) \<in> r" by blast |
|
428 |
then show "x \<in> A" |
|
429 |
using assms unfolding equiv_def refl_on_def by blast |
|
430 |
qed |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
431 |
qed |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
432 |
|
63653 | 433 |
lemma proj_iff: "equiv A r \<Longrightarrow> {x, y} \<subseteq> A \<Longrightarrow> proj r x = proj r y \<longleftrightarrow> (x, y) \<in> r" |
434 |
by (simp add: proj_def eq_equiv_class_iff) |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
435 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
436 |
(* |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
437 |
lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x" |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
438 |
unfolding proj_def equiv_def refl_on_def by blast |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
439 |
*) |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
440 |
|
63653 | 441 |
lemma proj_image: "proj r ` A = A//r" |
442 |
unfolding proj_def[abs_def] quotient_def by blast |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
443 |
|
63653 | 444 |
lemma in_quotient_imp_non_empty: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> X \<noteq> {}" |
445 |
unfolding quotient_def using equiv_class_self by fast |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
446 |
|
63653 | 447 |
lemma in_quotient_imp_in_rel: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> {x, y} \<subseteq> X \<Longrightarrow> (x, y) \<in> r" |
448 |
using quotient_eq_iff[THEN iffD1] by fastforce |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
449 |
|
63653 | 450 |
lemma in_quotient_imp_closed: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> x \<in> X \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> X" |
451 |
unfolding quotient_def equiv_def trans_def by blast |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
452 |
|
63653 | 453 |
lemma in_quotient_imp_subset: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> X \<subseteq> A" |
454 |
using in_quotient_imp_in_rel equiv_type by fastforce |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
455 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54744
diff
changeset
|
456 |
|
60758 | 457 |
subsection \<open>Equivalence relations -- predicate version\<close> |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
458 |
|
63653 | 459 |
text \<open>Partial equivalences.\<close> |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
460 |
|
63653 | 461 |
definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
462 |
where "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)" |
|
61799 | 463 |
\<comment> \<open>John-Harrison-style characterization\<close> |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
464 |
|
63653 | 465 |
lemma part_equivpI: "\<exists>x. R x x \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R" |
45969 | 466 |
by (auto simp add: part_equivp_def) (auto elim: sympE transpE) |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
467 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
468 |
lemma part_equivpE: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
469 |
assumes "part_equivp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
470 |
obtains x where "R x x" and "symp R" and "transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
471 |
proof - |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
472 |
from assms have 1: "\<exists>x. R x x" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
473 |
and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y" |
63653 | 474 |
unfolding part_equivp_def by blast+ |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
475 |
from 1 obtain x where "R x x" .. |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
476 |
moreover have "symp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
477 |
proof (rule sympI) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
478 |
fix x y |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
479 |
assume "R x y" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
480 |
with 2 [of x y] show "R y x" by auto |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
481 |
qed |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
482 |
moreover have "transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
483 |
proof (rule transpI) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
484 |
fix x y z |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
485 |
assume "R x y" and "R y z" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
486 |
with 2 [of x y] 2 [of y z] show "R x z" by auto |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
487 |
qed |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
488 |
ultimately show thesis by (rule that) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
489 |
qed |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
490 |
|
63653 | 491 |
lemma part_equivp_refl_symp_transp: "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
492 |
by (auto intro: part_equivpI elim: part_equivpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
493 |
|
63653 | 494 |
lemma part_equivp_symp: "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
495 |
by (erule part_equivpE, erule sympE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
496 |
|
63653 | 497 |
lemma part_equivp_transp: "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
498 |
by (erule part_equivpE, erule transpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
499 |
|
63653 | 500 |
lemma part_equivp_typedef: "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}" |
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40945
diff
changeset
|
501 |
by (auto elim: part_equivpE) |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
502 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
503 |
|
63653 | 504 |
text \<open>Total equivalences.\<close> |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
505 |
|
63653 | 506 |
definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
507 |
where "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" \<comment> \<open>John-Harrison-style characterization\<close> |
|
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
508 |
|
63653 | 509 |
lemma equivpI: "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R" |
45969 | 510 |
by (auto elim: reflpE sympE transpE simp add: equivp_def) |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
511 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
512 |
lemma equivpE: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
513 |
assumes "equivp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
514 |
obtains "reflp R" and "symp R" and "transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
515 |
using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
516 |
|
63653 | 517 |
lemma equivp_implies_part_equivp: "equivp R \<Longrightarrow> part_equivp R" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
518 |
by (auto intro: part_equivpI elim: equivpE reflpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
519 |
|
63653 | 520 |
lemma equivp_equiv: "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45969
diff
changeset
|
521 |
by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set]) |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
522 |
|
63653 | 523 |
lemma equivp_reflp_symp_transp: "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
524 |
by (auto intro: equivpI elim: equivpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
525 |
|
67399 | 526 |
lemma identity_equivp: "equivp (=)" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
527 |
by (auto intro: equivpI reflpI sympI transpI) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
528 |
|
63653 | 529 |
lemma equivp_reflp: "equivp R \<Longrightarrow> R x x" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
530 |
by (erule equivpE, erule reflpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
531 |
|
63653 | 532 |
lemma equivp_symp: "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
533 |
by (erule equivpE, erule sympE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
534 |
|
63653 | 535 |
lemma equivp_transp: "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" |
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
536 |
by (erule equivpE, erule transpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
537 |
|
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
538 |
lemma equivp_rtranclp: "symp r \<Longrightarrow> equivp r\<^sup>*\<^sup>*" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
539 |
by(intro equivpI reflpI sympI transpI)(auto dest: sympD[OF symp_rtranclp]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
540 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
541 |
lemmas equivp_rtranclp_symclp [simp] = equivp_rtranclp[OF symp_symclp] |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
542 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
543 |
lemma equivp_vimage2p: "equivp R \<Longrightarrow> equivp (vimage2p f f R)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
544 |
by(auto simp add: equivp_def vimage2p_def dest: fun_cong) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
545 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
546 |
lemma equivp_imp_transp: "equivp R \<Longrightarrow> transp R" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
547 |
by(simp add: equivp_reflp_symp_transp) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
548 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
549 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
550 |
subsection \<open>Equivalence closure\<close> |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
551 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
552 |
definition equivclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
553 |
"equivclp r = (symclp r)\<^sup>*\<^sup>*" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
554 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
555 |
lemma transp_equivclp [simp]: "transp (equivclp r)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
556 |
by(simp add: equivclp_def) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
557 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
558 |
lemma reflp_equivclp [simp]: "reflp (equivclp r)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
559 |
by(simp add: equivclp_def) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
560 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
561 |
lemma symp_equivclp [simp]: "symp (equivclp r)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
562 |
by(simp add: equivclp_def) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
563 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
564 |
lemma equivp_evquivclp [simp]: "equivp (equivclp r)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
565 |
by(simp add: equivpI) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
566 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
567 |
lemma tranclp_equivclp [simp]: "(equivclp r)\<^sup>+\<^sup>+ = equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
568 |
by(simp add: equivclp_def) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
569 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
570 |
lemma rtranclp_equivclp [simp]: "(equivclp r)\<^sup>*\<^sup>* = equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
571 |
by(simp add: equivclp_def) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
572 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
573 |
lemma symclp_equivclp [simp]: "symclp (equivclp r) = equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
574 |
by(simp add: equivclp_def symp_symclp_eq) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
575 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
576 |
lemma equivclp_symclp [simp]: "equivclp (symclp r) = equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
577 |
by(simp add: equivclp_def) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
578 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
579 |
lemma equivclp_conversep [simp]: "equivclp (conversep r) = equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
580 |
by(simp add: equivclp_def) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
581 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
582 |
lemma equivclp_sym [sym]: "equivclp r x y \<Longrightarrow> equivclp r y x" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
583 |
by(rule sympD[OF symp_equivclp]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
584 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
585 |
lemma equivclp_OO_equivclp_le_equivclp: "equivclp r OO equivclp r \<le> equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
586 |
by(rule transp_relcompp_less_eq transp_equivclp)+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
587 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
588 |
lemma rtranlcp_le_equivclp: "r\<^sup>*\<^sup>* \<le> equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
589 |
unfolding equivclp_def by(rule rtranclp_mono)(simp add: symclp_pointfree) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
590 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
591 |
lemma rtranclp_conversep_le_equivclp: "r\<inverse>\<inverse>\<^sup>*\<^sup>* \<le> equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
592 |
unfolding equivclp_def by(rule rtranclp_mono)(simp add: symclp_pointfree) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
593 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
594 |
lemma symclp_rtranclp_le_equivclp: "symclp r\<^sup>*\<^sup>* \<le> equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
595 |
unfolding symclp_pointfree |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
596 |
by(rule le_supI)(simp_all add: rtranclp_conversep[symmetric] rtranlcp_le_equivclp rtranclp_conversep_le_equivclp) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
597 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
598 |
lemma r_OO_conversep_into_equivclp: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
599 |
"r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>* \<le> equivclp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
600 |
by(blast intro: order_trans[OF _ equivclp_OO_equivclp_le_equivclp] relcompp_mono rtranlcp_le_equivclp rtranclp_conversep_le_equivclp del: predicate2I) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
601 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
602 |
lemma equivclp_induct [consumes 1, case_names base step, induct pred: equivclp]: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
603 |
assumes a: "equivclp r a b" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
604 |
and cases: "P a" "\<And>y z. equivclp r a y \<Longrightarrow> r y z \<or> r z y \<Longrightarrow> P y \<Longrightarrow> P z" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
605 |
shows "P b" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
606 |
using a unfolding equivclp_def |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
607 |
by(induction rule: rtranclp_induct; fold equivclp_def; blast intro: cases elim: symclpE) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
608 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
609 |
lemma converse_equivclp_induct [consumes 1, case_names base step]: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
610 |
assumes major: "equivclp r a b" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
611 |
and cases: "P b" "\<And>y z. r y z \<or> r z y \<Longrightarrow> equivclp r z b \<Longrightarrow> P z \<Longrightarrow> P y" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
612 |
shows "P a" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
613 |
using major unfolding equivclp_def |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
614 |
by(induction rule: converse_rtranclp_induct; fold equivclp_def; blast intro: cases elim: symclpE) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
615 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
616 |
lemma equivclp_refl [simp]: "equivclp r x x" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
617 |
by(rule reflpD[OF reflp_equivclp]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
618 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
619 |
lemma r_into_equivclp [intro]: "r x y \<Longrightarrow> equivclp r x y" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
620 |
unfolding equivclp_def by(blast intro: symclpI) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
621 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
622 |
lemma converse_r_into_equivclp [intro]: "r y x \<Longrightarrow> equivclp r x y" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
623 |
unfolding equivclp_def by(blast intro: symclpI) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
624 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
625 |
lemma rtranclp_into_equivclp: "r\<^sup>*\<^sup>* x y \<Longrightarrow> equivclp r x y" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
626 |
using rtranlcp_le_equivclp[of r] by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
627 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
628 |
lemma converse_rtranclp_into_equivclp: "r\<^sup>*\<^sup>* y x \<Longrightarrow> equivclp r x y" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
629 |
by(blast intro: equivclp_sym rtranclp_into_equivclp) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
630 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
631 |
lemma equivclp_into_equivclp: "\<lbrakk> equivclp r a b; r b c \<or> r c b \<rbrakk> \<Longrightarrow> equivclp r a c" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
632 |
unfolding equivclp_def by(erule rtranclp.rtrancl_into_rtrancl)(auto intro: symclpI) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
633 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
634 |
lemma equivclp_trans [trans]: "\<lbrakk> equivclp r a b; equivclp r b c \<rbrakk> \<Longrightarrow> equivclp r a c" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
635 |
using equivclp_OO_equivclp_le_equivclp[of r] by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
67399
diff
changeset
|
636 |
|
55024 | 637 |
hide_const (open) proj |
638 |
||
15300 | 639 |
end |