equal
deleted
inserted
replaced
10 ("quotient_def.ML") |
10 ("quotient_def.ML") |
11 ("quotient_term.ML") |
11 ("quotient_term.ML") |
12 ("quotient_tacs.ML") |
12 ("quotient_tacs.ML") |
13 begin |
13 begin |
14 |
14 |
|
15 |
15 text {* |
16 text {* |
16 Basic definition for equivalence relations |
17 Basic definition for equivalence relations |
17 that are represented by predicates. |
18 that are represented by predicates. |
18 *} |
19 *} |
19 |
20 |
20 definition |
21 definition |
21 "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))" |
22 "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)" |
22 |
23 |
23 definition |
24 definition |
24 "reflp E \<longleftrightarrow> (\<forall>x. E x x)" |
25 "reflp E \<equiv> \<forall>x. E x x" |
25 |
26 |
26 definition |
27 definition |
27 "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)" |
28 "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x" |
28 |
29 |
29 definition |
30 definition |
30 "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)" |
31 "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z" |
31 |
32 |
32 lemma equivp_reflp_symp_transp: |
33 lemma equivp_reflp_symp_transp: |
33 shows "equivp E = (reflp E \<and> symp E \<and> transp E)" |
34 shows "equivp E = (reflp E \<and> symp E \<and> transp E)" |
34 unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq |
35 unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq |
35 by blast |
36 by blast |
49 lemma equivpI: |
50 lemma equivpI: |
50 assumes "reflp R" "symp R" "transp R" |
51 assumes "reflp R" "symp R" "transp R" |
51 shows "equivp R" |
52 shows "equivp R" |
52 using assms by (simp add: equivp_reflp_symp_transp) |
53 using assms by (simp add: equivp_reflp_symp_transp) |
53 |
54 |
54 lemma eq_imp_rel: |
|
55 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
|
56 by (simp add: equivp_reflp) |
|
57 |
|
58 lemma identity_equivp: |
55 lemma identity_equivp: |
59 shows "equivp (op =)" |
56 shows "equivp (op =)" |
60 unfolding equivp_def |
57 unfolding equivp_def |
61 by auto |
58 by auto |
62 |
59 |
63 |
|
64 text {* Partial equivalences: not yet used anywhere *} |
60 text {* Partial equivalences: not yet used anywhere *} |
65 definition |
61 |
66 "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))" |
62 definition |
|
63 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
67 |
64 |
68 lemma equivp_implies_part_equivp: |
65 lemma equivp_implies_part_equivp: |
69 assumes a: "equivp E" |
66 assumes a: "equivp E" |
70 shows "part_equivp E" |
67 shows "part_equivp E" |
71 using a |
68 using a |
86 section {* Respects predicate *} |
83 section {* Respects predicate *} |
87 |
84 |
88 definition |
85 definition |
89 Respects |
86 Respects |
90 where |
87 where |
91 "Respects R x \<longleftrightarrow> (R x x)" |
88 "Respects R x \<equiv> R x x" |
92 |
89 |
93 lemma in_respects: |
90 lemma in_respects: |
94 shows "(x \<in> Respects R) = R x x" |
91 shows "(x \<in> Respects R) = R x x" |
95 unfolding mem_def Respects_def |
92 unfolding mem_def Respects_def |
96 by simp |
93 by simp |
128 |
125 |
129 |
126 |
130 section {* Quotient Predicate *} |
127 section {* Quotient Predicate *} |
131 |
128 |
132 definition |
129 definition |
133 "Quotient E Abs Rep \<longleftrightarrow> |
130 "Quotient E Abs Rep \<equiv> |
134 (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and> |
131 (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and> |
135 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
132 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
136 |
133 |
137 lemma Quotient_abs_rep: |
134 lemma Quotient_abs_rep: |
138 assumes a: "Quotient E Abs Rep" |
135 assumes a: "Quotient E Abs Rep" |
352 apply(rule impI) |
349 apply(rule impI) |
353 using a equivp_reflp_symp_transp[of "R2"] |
350 using a equivp_reflp_symp_transp[of "R2"] |
354 apply(simp add: reflp_def) |
351 apply(simp add: reflp_def) |
355 done |
352 done |
356 |
353 |
|
354 (* Next four lemmas are unused *) |
357 lemma all_reg: |
355 lemma all_reg: |
358 assumes a: "!x :: 'a. (P x --> Q x)" |
356 assumes a: "!x :: 'a. (P x --> Q x)" |
359 and b: "All P" |
357 and b: "All P" |
360 shows "All Q" |
358 shows "All Q" |
361 using a b by (metis) |
359 using a b by (metis) |
375 lemma bex_reg: |
373 lemma bex_reg: |
376 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
374 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
377 and b: "Bex R P" |
375 and b: "Bex R P" |
378 shows "Bex R Q" |
376 shows "Bex R Q" |
379 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
377 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
|
378 |
380 |
379 |
381 lemma ball_all_comm: |
380 lemma ball_all_comm: |
382 assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)" |
381 assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)" |
383 shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)" |
382 shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)" |
384 using assms by auto |
383 using assms by auto |