src/HOL/Algebra/Congruence.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66453 cc19f7ca2ed6 child 67091 1393c2340eec permissions -rw-r--r--
tuned: each session has at most one defining entry;
1 (*  Title:      HOL/Algebra/Congruence.thy
2     Author:     Clemens Ballarin, started 3 January 2008
3     Copyright:  Clemens Ballarin
4 *)
6 theory Congruence
7 imports
8   Main
9   "HOL-Library.FuncSet"
10 begin
12 section \<open>Objects\<close>
14 subsection \<open>Structure with Carrier Set.\<close>
16 record 'a partial_object =
17   carrier :: "'a set"
19 lemma funcset_carrier:
20   "\<lbrakk> f \<in> carrier X \<rightarrow> carrier Y; x \<in> carrier X \<rbrakk> \<Longrightarrow> f x \<in> carrier Y"
21   by (fact funcset_mem)
23 lemma funcset_carrier':
24   "\<lbrakk> f \<in> carrier A \<rightarrow> carrier A; x \<in> carrier A \<rbrakk> \<Longrightarrow> f x \<in> carrier A"
25   by (fact funcset_mem)
28 subsection \<open>Structure with Carrier and Equivalence Relation \<open>eq\<close>\<close>
30 record 'a eq_object = "'a partial_object" +
31   eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
33 definition
34   elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
35   where "x .\<in>\<^bsub>S\<^esub> A \<longleftrightarrow> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
37 definition
38   set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
39   where "A {.=}\<^bsub>S\<^esub> B \<longleftrightarrow> ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
41 definition
42   eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index>")
43   where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
45 definition
46   eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index>")
47   where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
49 definition
50   eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index>")
51   where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
53 abbreviation
54   not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
55   where "x .\<noteq>\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)"
57 abbreviation
58   not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
59   where "x .\<notin>\<^bsub>S\<^esub> A == ~(x .\<in>\<^bsub>S\<^esub> A)"
61 abbreviation
62   set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
63   where "A {.\<noteq>}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)"
65 locale equivalence =
66   fixes S (structure)
67   assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x"
68     and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x"
69     and trans [trans]:
70       "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
72 (* Lemmas by Stephan Hohe *)
74 lemma elemI:
75   fixes R (structure)
76   assumes "a' \<in> A" and "a .= a'"
77   shows "a .\<in> A"
78 unfolding elem_def
79 using assms
80 by fast
82 lemma (in equivalence) elem_exact:
83   assumes "a \<in> carrier S" and "a \<in> A"
84   shows "a .\<in> A"
85 using assms
86 by (fast intro: elemI)
88 lemma elemE:
89   fixes S (structure)
90   assumes "a .\<in> A"
91     and "\<And>a'. \<lbrakk>a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
92   shows "P"
93 using assms
94 unfolding elem_def
95 by fast
97 lemma (in equivalence) elem_cong_l [trans]:
98   assumes cong: "a' .= a"
99     and a: "a .\<in> A"
100     and carr: "a \<in> carrier S"  "a' \<in> carrier S"
101     and Acarr: "A \<subseteq> carrier S"
102   shows "a' .\<in> A"
103 using a
104 apply (elim elemE, intro elemI)
105 proof assumption
106   fix b
107   assume bA: "b \<in> A"
108   note [simp] = carr bA[THEN subsetD[OF Acarr]]
109   note cong
110   also assume "a .= b"
111   finally show "a' .= b" by simp
112 qed
114 lemma (in equivalence) elem_subsetD:
115   assumes "A \<subseteq> B"
116     and aA: "a .\<in> A"
117   shows "a .\<in> B"
118 using assms
119 by (fast intro: elemI elim: elemE dest: subsetD)
121 lemma (in equivalence) mem_imp_elem [simp, intro]:
122   "[| x \<in> A; x \<in> carrier S |] ==> x .\<in> A"
123   unfolding elem_def by blast
125 lemma set_eqI:
126   fixes R (structure)
127   assumes ltr: "\<And>a. a \<in> A \<Longrightarrow> a .\<in> B"
128     and rtl: "\<And>b. b \<in> B \<Longrightarrow> b .\<in> A"
129   shows "A {.=} B"
130 unfolding set_eq_def
131 by (fast intro: ltr rtl)
133 lemma set_eqI2:
134   fixes R (structure)
135   assumes ltr: "\<And>a b. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a .= b"
136     and rtl: "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. b .= a"
137   shows "A {.=} B"
138   by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+
140 lemma set_eqD1:
141   fixes R (structure)
142   assumes AA': "A {.=} A'"
143     and "a \<in> A"
144   shows "\<exists>a'\<in>A'. a .= a'"
145 using assms
146 unfolding set_eq_def elem_def
147 by fast
149 lemma set_eqD2:
150   fixes R (structure)
151   assumes AA': "A {.=} A'"
152     and "a' \<in> A'"
153   shows "\<exists>a\<in>A. a' .= a"
154 using assms
155 unfolding set_eq_def elem_def
156 by fast
158 lemma set_eqE:
159   fixes R (structure)
160   assumes AB: "A {.=} B"
161     and r: "\<lbrakk>\<forall>a\<in>A. a .\<in> B; \<forall>b\<in>B. b .\<in> A\<rbrakk> \<Longrightarrow> P"
162   shows "P"
163 using AB
164 unfolding set_eq_def
165 by (blast dest: r)
167 lemma set_eqE2:
168   fixes R (structure)
169   assumes AB: "A {.=} B"
170     and r: "\<lbrakk>\<forall>a\<in>A. (\<exists>b\<in>B. a .= b); \<forall>b\<in>B. (\<exists>a\<in>A. b .= a)\<rbrakk> \<Longrightarrow> P"
171   shows "P"
172 using AB
173 unfolding set_eq_def elem_def
174 by (blast dest: r)
176 lemma set_eqE':
177   fixes R (structure)
178   assumes AB: "A {.=} B"
179     and aA: "a \<in> A" and bB: "b \<in> B"
180     and r: "\<And>a' b'. \<lbrakk>a' \<in> A; b .= a'; b' \<in> B; a .= b'\<rbrakk> \<Longrightarrow> P"
181   shows "P"
182 proof -
183   from AB aA
184       have "\<exists>b'\<in>B. a .= b'" by (rule set_eqD1)
185   from this obtain b'
186       where b': "b' \<in> B" "a .= b'" by auto
188   from AB bB
189       have "\<exists>a'\<in>A. b .= a'" by (rule set_eqD2)
190   from this obtain a'
191       where a': "a' \<in> A" "b .= a'" by auto
193   from a' b'
194       show "P" by (rule r)
195 qed
197 lemma (in equivalence) eq_elem_cong_r [trans]:
198   assumes a: "a .\<in> A"
199     and cong: "A {.=} A'"
200     and carr: "a \<in> carrier S"
201     and Carr: "A \<subseteq> carrier S" "A' \<subseteq> carrier S"
202   shows "a .\<in> A'"
203 using a cong
204 proof (elim elemE set_eqE)
205   fix b
206   assume bA: "b \<in> A"
207      and inA': "\<forall>b\<in>A. b .\<in> A'"
208   note [simp] = carr Carr Carr[THEN subsetD] bA
209   assume "a .= b"
210   also from bA inA'
211        have "b .\<in> A'" by fast
212   finally
213        show "a .\<in> A'" by simp
214 qed
216 lemma (in equivalence) set_eq_sym [sym]:
217   assumes "A {.=} B"
218     and "A \<subseteq> carrier S" "B \<subseteq> carrier S"
219   shows "B {.=} A"
220 using assms
221 unfolding set_eq_def elem_def
222 by fast
224 (* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
225 (* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
227 lemma (in equivalence) equal_set_eq_trans [trans]:
228   assumes AB: "A = B" and BC: "B {.=} C"
229   shows "A {.=} C"
230   using AB BC by simp
232 lemma (in equivalence) set_eq_equal_trans [trans]:
233   assumes AB: "A {.=} B" and BC: "B = C"
234   shows "A {.=} C"
235   using AB BC by simp
238 lemma (in equivalence) set_eq_trans [trans]:
239   assumes AB: "A {.=} B" and BC: "B {.=} C"
240     and carr: "A \<subseteq> carrier S"  "B \<subseteq> carrier S"  "C \<subseteq> carrier S"
241   shows "A {.=} C"
242 proof (intro set_eqI)
243   fix a
244   assume aA: "a \<in> A"
245   with carr have "a \<in> carrier S" by fast
246   note [simp] = carr this
248   from aA
249        have "a .\<in> A" by (simp add: elem_exact)
250   also note AB
251   also note BC
252   finally
253        show "a .\<in> C" by simp
254 next
255   fix c
256   assume cC: "c \<in> C"
257   with carr have "c \<in> carrier S" by fast
258   note [simp] = carr this
260   from cC
261        have "c .\<in> C" by (simp add: elem_exact)
262   also note BC[symmetric]
263   also note AB[symmetric]
264   finally
265        show "c .\<in> A" by simp
266 qed
268 (* FIXME: generalise for insert *)
270 (*
271 lemma (in equivalence) set_eq_insert:
272   assumes x: "x .= x'"
273     and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
274   shows "insert x A {.=} insert x' A"
275   unfolding set_eq_def elem_def
276 apply rule
277 apply rule
278 apply (case_tac "xa = x")
279 using x apply fast
280 apply (subgoal_tac "xa \<in> A") prefer 2 apply fast
281 apply (rule_tac x=xa in bexI)
282 using carr apply (rule_tac refl) apply auto 
283 apply safe
284 *)
286 lemma (in equivalence) set_eq_pairI:
287   assumes xx': "x .= x'"
288     and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
289   shows "{x, y} {.=} {x', y}"
290 unfolding set_eq_def elem_def
291 proof safe
292   have "x' \<in> {x', y}" by fast
293   with xx' show "\<exists>b\<in>{x', y}. x .= b" by fast
294 next
295   have "y \<in> {x', y}" by fast
296   with carr show "\<exists>b\<in>{x', y}. y .= b" by fast
297 next
298   have "x \<in> {x, y}" by fast
299   with xx'[symmetric] carr
300   show "\<exists>a\<in>{x, y}. x' .= a" by fast
301 next
302   have "y \<in> {x, y}" by fast
303   with carr show "\<exists>a\<in>{x, y}. y .= a" by fast
304 qed
306 lemma (in equivalence) is_closedI:
307   assumes closed: "!!x y. [| x .= y; x \<in> A; y \<in> carrier S |] ==> y \<in> A"
308     and S: "A \<subseteq> carrier S"
309   shows "is_closed A"
310   unfolding eq_is_closed_def eq_closure_of_def elem_def
311   using S
312   by (blast dest: closed sym)
314 lemma (in equivalence) closure_of_eq:
315   "[| x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> closure_of A"
316   unfolding eq_closure_of_def elem_def
317   by (blast intro: trans sym)
319 lemma (in equivalence) is_closed_eq [dest]:
320   "[| x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> A"
321   unfolding eq_is_closed_def
322   using closure_of_eq [where A = A]
323   by simp
325 lemma (in equivalence) is_closed_eq_rev [dest]:
326   "[| x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x \<in> A"
327   by (drule sym) (simp_all add: is_closed_eq)
329 lemma closure_of_closed [simp, intro]:
330   fixes S (structure)
331   shows "closure_of A \<subseteq> carrier S"
332 unfolding eq_closure_of_def
333 by fast
335 lemma closure_of_memI:
336   fixes S (structure)
337   assumes "a .\<in> A"
338     and "a \<in> carrier S"
339   shows "a \<in> closure_of A"
340 unfolding eq_closure_of_def
341 using assms
342 by fast
344 lemma closure_ofI2:
345   fixes S (structure)
346   assumes "a .= a'"
347     and "a' \<in> A"
348     and "a \<in> carrier S"
349   shows "a \<in> closure_of A"
350 unfolding eq_closure_of_def elem_def
351 using assms
352 by fast
354 lemma closure_of_memE:
355   fixes S (structure)
356   assumes p: "a \<in> closure_of A"
357     and r: "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
358   shows "P"
359 proof -
360   from p
361       have acarr: "a \<in> carrier S"
362       and "a .\<in> A"
363       by (simp add: eq_closure_of_def)+
364   thus "P" by (rule r)
365 qed
367 lemma closure_ofE2:
368   fixes S (structure)
369   assumes p: "a \<in> closure_of A"
370     and r: "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
371   shows "P"
372 proof -
373   from p have acarr: "a \<in> carrier S" by (simp add: eq_closure_of_def)
375   from p have "\<exists>a'\<in>A. a .= a'" by (simp add: eq_closure_of_def elem_def)
376   from this obtain a'
377       where "a' \<in> A" and "a .= a'" by auto
379   from acarr and this
380       show "P" by (rule r)
381 qed
383 (*
384 lemma (in equivalence) classes_consistent:
385   assumes Acarr: "A \<subseteq> carrier S"
386   shows "is_closed (closure_of A)"
387 apply (blast intro: elemI elim elemE)
388 using assms
389 apply (intro is_closedI closure_of_memI, simp)
390  apply (elim elemE closure_of_memE)
391 proof -
392   fix x a' a''
393   assume carr: "x \<in> carrier S" "a' \<in> carrier S"
394   assume a''A: "a'' \<in> A"
395   with Acarr have "a'' \<in> carrier S" by fast
396   note [simp] = carr this Acarr
398   assume "x .= a'"
399   also assume "a' .= a''"
400   also from a''A
401        have "a'' .\<in> A" by (simp add: elem_exact)
402   finally show "x .\<in> A" by simp
403 qed
404 *)
405 (*
406 lemma (in equivalence) classes_small:
407   assumes "is_closed B"
408     and "A \<subseteq> B"
409   shows "closure_of A \<subseteq> B"
410 using assms
411 by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE)
413 lemma (in equivalence) classes_eq:
414   assumes "A \<subseteq> carrier S"
415   shows "A {.=} closure_of A"
416 using assms
417 by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE)
419 lemma (in equivalence) complete_classes:
420   assumes c: "is_closed A"
421   shows "A = closure_of A"
422 using assms
423 by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
424 *)
426 lemma equivalence_subset:
427   assumes "equivalence L" "A \<subseteq> carrier L"
428   shows "equivalence (L\<lparr> carrier := A \<rparr>)"
429 proof -
430   interpret L: equivalence L
431     by (simp add: assms)
432   show ?thesis
433     by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD)
434 qed
436 end