src/HOL/Algebra/Congruence.thy
 author wenzelm Thu Mar 26 20:08:55 2009 +0100 (2009-03-26) changeset 30729 461ee3e49ad3 parent 29237 e90d9d51106b child 35355 613e133966ea permissions -rw-r--r--
interpretation/interpret: prefixes are mandatory by default;
1 (*
2   Title:  Algebra/Congruence.thy
3   Author: Clemens Ballarin, started 3 January 2008
4   Copyright: Clemens Ballarin
5 *)
7 theory Congruence imports Main begin
9 section {* Objects *}
11 subsection {* Structure with Carrier Set. *}
13 record 'a partial_object =
14   carrier :: "'a set"
17 subsection {* Structure with Carrier and Equivalence Relation @{text eq} *}
19 record 'a eq_object = "'a partial_object" +
20   eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
22 constdefs (structure S)
23   elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
24   "x .\<in> A \<equiv> (\<exists>y \<in> A. x .= y)"
26   set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
27   "A {.=} B == ((\<forall>x \<in> A. x .\<in> B) \<and> (\<forall>x \<in> B. x .\<in> A))"
29   eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
30   "class_of x == {y \<in> carrier S. x .= y}"
32   eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
33   "closure_of A == {y \<in> carrier S. y .\<in> A}"
35   eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
36   "is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
38 syntax
39   not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
40   not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
41   set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
43 translations
44   "x .\<noteq>\<index> y" == "~(x .=\<index> y)"
45   "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
46   "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
48 locale equivalence =
49   fixes S (structure)
50   assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x"
51     and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x"
52     and trans [trans]: "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
54 (* Lemmas by Stephan Hohe *)
56 lemma elemI:
57   fixes R (structure)
58   assumes "a' \<in> A" and "a .= a'"
59   shows "a .\<in> A"
60 unfolding elem_def
61 using assms
62 by fast
64 lemma (in equivalence) elem_exact:
65   assumes "a \<in> carrier S" and "a \<in> A"
66   shows "a .\<in> A"
67 using assms
68 by (fast intro: elemI)
70 lemma elemE:
71   fixes S (structure)
72   assumes "a .\<in> A"
73     and "\<And>a'. \<lbrakk>a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
74   shows "P"
75 using assms
76 unfolding elem_def
77 by fast
79 lemma (in equivalence) elem_cong_l [trans]:
80   assumes cong: "a' .= a"
81     and a: "a .\<in> A"
82     and carr: "a \<in> carrier S"  "a' \<in> carrier S"
83     and Acarr: "A \<subseteq> carrier S"
84   shows "a' .\<in> A"
85 using a
86 apply (elim elemE, intro elemI)
87 proof assumption
88   fix b
89   assume bA: "b \<in> A"
90   note [simp] = carr bA[THEN subsetD[OF Acarr]]
91   note cong
92   also assume "a .= b"
93   finally show "a' .= b" by simp
94 qed
96 lemma (in equivalence) elem_subsetD:
97   assumes "A \<subseteq> B"
98     and aA: "a .\<in> A"
99   shows "a .\<in> B"
100 using assms
101 by (fast intro: elemI elim: elemE dest: subsetD)
103 lemma (in equivalence) mem_imp_elem [simp, intro]:
104   "[| x \<in> A; x \<in> carrier S |] ==> x .\<in> A"
105   unfolding elem_def by blast
107 lemma set_eqI:
108   fixes R (structure)
109   assumes ltr: "\<And>a. a \<in> A \<Longrightarrow> a .\<in> B"
110     and rtl: "\<And>b. b \<in> B \<Longrightarrow> b .\<in> A"
111   shows "A {.=} B"
112 unfolding set_eq_def
113 by (fast intro: ltr rtl)
115 lemma set_eqI2:
116   fixes R (structure)
117   assumes ltr: "\<And>a b. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a .= b"
118     and rtl: "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. b .= a"
119   shows "A {.=} B"
120   by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+
122 lemma set_eqD1:
123   fixes R (structure)
124   assumes AA': "A {.=} A'"
125     and "a \<in> A"
126   shows "\<exists>a'\<in>A'. a .= a'"
127 using assms
128 unfolding set_eq_def elem_def
129 by fast
131 lemma set_eqD2:
132   fixes R (structure)
133   assumes AA': "A {.=} A'"
134     and "a' \<in> A'"
135   shows "\<exists>a\<in>A. a' .= a"
136 using assms
137 unfolding set_eq_def elem_def
138 by fast
140 lemma set_eqE:
141   fixes R (structure)
142   assumes AB: "A {.=} B"
143     and r: "\<lbrakk>\<forall>a\<in>A. a .\<in> B; \<forall>b\<in>B. b .\<in> A\<rbrakk> \<Longrightarrow> P"
144   shows "P"
145 using AB
146 unfolding set_eq_def
147 by (blast dest: r)
149 lemma set_eqE2:
150   fixes R (structure)
151   assumes AB: "A {.=} B"
152     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"
153   shows "P"
154 using AB
155 unfolding set_eq_def elem_def
156 by (blast dest: r)
158 lemma set_eqE':
159   fixes R (structure)
160   assumes AB: "A {.=} B"
161     and aA: "a \<in> A" and bB: "b \<in> B"
162     and r: "\<And>a' b'. \<lbrakk>a' \<in> A; b .= a'; b' \<in> B; a .= b'\<rbrakk> \<Longrightarrow> P"
163   shows "P"
164 proof -
165   from AB aA
166       have "\<exists>b'\<in>B. a .= b'" by (rule set_eqD1)
167   from this obtain b'
168       where b': "b' \<in> B" "a .= b'" by auto
170   from AB bB
171       have "\<exists>a'\<in>A. b .= a'" by (rule set_eqD2)
172   from this obtain a'
173       where a': "a' \<in> A" "b .= a'" by auto
175   from a' b'
176       show "P" by (rule r)
177 qed
179 lemma (in equivalence) eq_elem_cong_r [trans]:
180   assumes a: "a .\<in> A"
181     and cong: "A {.=} A'"
182     and carr: "a \<in> carrier S"
183     and Carr: "A \<subseteq> carrier S" "A' \<subseteq> carrier S"
184   shows "a .\<in> A'"
185 using a cong
186 proof (elim elemE set_eqE)
187   fix b
188   assume bA: "b \<in> A"
189      and inA': "\<forall>b\<in>A. b .\<in> A'"
190   note [simp] = carr Carr Carr[THEN subsetD] bA
191   assume "a .= b"
192   also from bA inA'
193        have "b .\<in> A'" by fast
194   finally
195        show "a .\<in> A'" by simp
196 qed
198 lemma (in equivalence) set_eq_sym [sym]:
199   assumes "A {.=} B"
200     and "A \<subseteq> carrier S" "B \<subseteq> carrier S"
201   shows "B {.=} A"
202 using assms
203 unfolding set_eq_def elem_def
204 by fast
206 (* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
207 (* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
209 lemma (in equivalence) equal_set_eq_trans [trans]:
210   assumes AB: "A = B" and BC: "B {.=} C"
211   shows "A {.=} C"
212   using AB BC by simp
214 lemma (in equivalence) set_eq_equal_trans [trans]:
215   assumes AB: "A {.=} B" and BC: "B = C"
216   shows "A {.=} C"
217   using AB BC by simp
220 lemma (in equivalence) set_eq_trans [trans]:
221   assumes AB: "A {.=} B" and BC: "B {.=} C"
222     and carr: "A \<subseteq> carrier S"  "B \<subseteq> carrier S"  "C \<subseteq> carrier S"
223   shows "A {.=} C"
224 proof (intro set_eqI)
225   fix a
226   assume aA: "a \<in> A"
227   with carr have "a \<in> carrier S" by fast
228   note [simp] = carr this
230   from aA
231        have "a .\<in> A" by (simp add: elem_exact)
232   also note AB
233   also note BC
234   finally
235        show "a .\<in> C" by simp
236 next
237   fix c
238   assume cC: "c \<in> C"
239   with carr have "c \<in> carrier S" by fast
240   note [simp] = carr this
242   from cC
243        have "c .\<in> C" by (simp add: elem_exact)
244   also note BC[symmetric]
245   also note AB[symmetric]
246   finally
247        show "c .\<in> A" by simp
248 qed
250 (* FIXME: generalise for insert *)
252 (*
253 lemma (in equivalence) set_eq_insert:
254   assumes x: "x .= x'"
255     and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
256   shows "insert x A {.=} insert x' A"
257   unfolding set_eq_def elem_def
258 apply rule
259 apply rule
260 apply (case_tac "xa = x")
261 using x apply fast
262 apply (subgoal_tac "xa \<in> A") prefer 2 apply fast
263 apply (rule_tac x=xa in bexI)
264 using carr apply (rule_tac refl) apply auto 
265 apply safe
266 *)
268 lemma (in equivalence) set_eq_pairI:
269   assumes xx': "x .= x'"
270     and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
271   shows "{x, y} {.=} {x', y}"
272 unfolding set_eq_def elem_def
273 proof safe
274   have "x' \<in> {x', y}" by fast
275   with xx' show "\<exists>b\<in>{x', y}. x .= b" by fast
276 next
277   have "y \<in> {x', y}" by fast
278   with carr show "\<exists>b\<in>{x', y}. y .= b" by fast
279 next
280   have "x \<in> {x, y}" by fast
281   with xx'[symmetric] carr
282   show "\<exists>a\<in>{x, y}. x' .= a" by fast
283 next
284   have "y \<in> {x, y}" by fast
285   with carr show "\<exists>a\<in>{x, y}. y .= a" by fast
286 qed
288 lemma (in equivalence) is_closedI:
289   assumes closed: "!!x y. [| x .= y; x \<in> A; y \<in> carrier S |] ==> y \<in> A"
290     and S: "A \<subseteq> carrier S"
291   shows "is_closed A"
292   unfolding eq_is_closed_def eq_closure_of_def elem_def
293   using S
294   by (blast dest: closed sym)
296 lemma (in equivalence) closure_of_eq:
297   "[| x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> closure_of A"
298   unfolding eq_closure_of_def elem_def
299   by (blast intro: trans sym)
301 lemma (in equivalence) is_closed_eq [dest]:
302   "[| x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> A"
303   unfolding eq_is_closed_def
304   using closure_of_eq [where A = A]
305   by simp
307 lemma (in equivalence) is_closed_eq_rev [dest]:
308   "[| x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x \<in> A"
309   by (drule sym) (simp_all add: is_closed_eq)
311 lemma closure_of_closed [simp, intro]:
312   fixes S (structure)
313   shows "closure_of A \<subseteq> carrier S"
314 unfolding eq_closure_of_def
315 by fast
317 lemma closure_of_memI:
318   fixes S (structure)
319   assumes "a .\<in> A"
320     and "a \<in> carrier S"
321   shows "a \<in> closure_of A"
322 unfolding eq_closure_of_def
323 using assms
324 by fast
326 lemma closure_ofI2:
327   fixes S (structure)
328   assumes "a .= a'"
329     and "a' \<in> A"
330     and "a \<in> carrier S"
331   shows "a \<in> closure_of A"
332 unfolding eq_closure_of_def elem_def
333 using assms
334 by fast
336 lemma closure_of_memE:
337   fixes S (structure)
338   assumes p: "a \<in> closure_of A"
339     and r: "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
340   shows "P"
341 proof -
342   from p
343       have acarr: "a \<in> carrier S"
344       and "a .\<in> A"
345       by (simp add: eq_closure_of_def)+
346   thus "P" by (rule r)
347 qed
349 lemma closure_ofE2:
350   fixes S (structure)
351   assumes p: "a \<in> closure_of A"
352     and r: "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
353   shows "P"
354 proof -
355   from p have acarr: "a \<in> carrier S" by (simp add: eq_closure_of_def)
357   from p have "\<exists>a'\<in>A. a .= a'" by (simp add: eq_closure_of_def elem_def)
358   from this obtain a'
359       where "a' \<in> A" and "a .= a'" by auto
361   from acarr and this
362       show "P" by (rule r)
363 qed
365 (*
366 lemma (in equivalence) classes_consistent:
367   assumes Acarr: "A \<subseteq> carrier S"
368   shows "is_closed (closure_of A)"
369 apply (blast intro: elemI elim elemE)
370 using assms
371 apply (intro is_closedI closure_of_memI, simp)
372  apply (elim elemE closure_of_memE)
373 proof -
374   fix x a' a''
375   assume carr: "x \<in> carrier S" "a' \<in> carrier S"
376   assume a''A: "a'' \<in> A"
377   with Acarr have "a'' \<in> carrier S" by fast
378   note [simp] = carr this Acarr
380   assume "x .= a'"
381   also assume "a' .= a''"
382   also from a''A
383        have "a'' .\<in> A" by (simp add: elem_exact)
384   finally show "x .\<in> A" by simp
385 qed
386 *)
387 (*
388 lemma (in equivalence) classes_small:
389   assumes "is_closed B"
390     and "A \<subseteq> B"
391   shows "closure_of A \<subseteq> B"
392 using assms
393 by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE)
395 lemma (in equivalence) classes_eq:
396   assumes "A \<subseteq> carrier S"
397   shows "A {.=} closure_of A"
398 using assms
399 by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE)
401 lemma (in equivalence) complete_classes:
402   assumes c: "is_closed A"
403   shows "A = closure_of A"
404 using assms
405 by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
406 *)
408 end