equal
deleted
inserted
replaced
15 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
15 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
16 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
16 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
17 begin |
17 begin |
18 |
18 |
19 definition |
19 definition |
20 ABS::"'a \<Rightarrow> 'b" |
20 abs::"'a \<Rightarrow> 'b" |
21 where |
21 where |
22 "ABS x \<equiv> Abs (R x)" |
22 "abs x \<equiv> Abs (R x)" |
23 |
23 |
24 definition |
24 definition |
25 REP::"'b \<Rightarrow> 'a" |
25 rep::"'b \<Rightarrow> 'a" |
26 where |
26 where |
27 "REP a = Eps (Rep a)" |
27 "rep a = Eps (Rep a)" |
28 |
28 |
29 lemma lem9: |
29 lemma lem9: |
30 shows "R (Eps (R x)) = R x" |
30 shows "R (Eps (R x)) = R x" |
31 proof - |
31 proof - |
32 have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) |
32 have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) |
34 then show "R (Eps (R x)) = R x" |
34 then show "R (Eps (R x)) = R x" |
35 using equivp unfolding equivp_def by simp |
35 using equivp unfolding equivp_def by simp |
36 qed |
36 qed |
37 |
37 |
38 theorem thm10: |
38 theorem thm10: |
39 shows "ABS (REP a) \<equiv> a" |
39 shows "abs (rep a) \<equiv> a" |
40 apply (rule eq_reflection) |
40 apply (rule eq_reflection) |
41 unfolding ABS_def REP_def |
41 unfolding abs_def rep_def |
42 proof - |
42 proof - |
43 from rep_prop |
43 from rep_prop |
44 obtain x where eq: "Rep a = R x" by auto |
44 obtain x where eq: "Rep a = R x" by auto |
45 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
45 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
46 also have "\<dots> = Abs (R x)" using lem9 by simp |
46 also have "\<dots> = Abs (R x)" using lem9 by simp |
48 also have "\<dots> = a" using rep_inverse by simp |
48 also have "\<dots> = a" using rep_inverse by simp |
49 finally |
49 finally |
50 show "Abs (R (Eps (Rep a))) = a" by simp |
50 show "Abs (R (Eps (Rep a))) = a" by simp |
51 qed |
51 qed |
52 |
52 |
53 lemma REP_refl: |
53 lemma rep_refl: |
54 shows "R (REP a) (REP a)" |
54 shows "R (rep a) (rep a)" |
55 unfolding REP_def |
55 unfolding rep_def |
56 by (simp add: equivp[simplified equivp_def]) |
56 by (simp add: equivp[simplified equivp_def]) |
57 |
57 |
58 lemma lem7: |
58 lemma lem7: |
59 shows "(R x = R y) = (Abs (R x) = Abs (R y))" |
59 shows "(R x = R y) = (Abs (R x) = Abs (R y))" |
60 apply(rule iffI) |
60 apply(rule iffI) |
62 apply(drule rep_inject[THEN iffD2]) |
62 apply(drule rep_inject[THEN iffD2]) |
63 apply(simp add: abs_inverse) |
63 apply(simp add: abs_inverse) |
64 done |
64 done |
65 |
65 |
66 theorem thm11: |
66 theorem thm11: |
67 shows "R r r' = (ABS r = ABS r')" |
67 shows "R r r' = (abs r = abs r')" |
68 unfolding ABS_def |
68 unfolding abs_def |
69 by (simp only: equivp[simplified equivp_def] lem7) |
69 by (simp only: equivp[simplified equivp_def] lem7) |
70 |
70 |
71 |
71 |
72 lemma REP_ABS_rsp: |
72 lemma rep_abs_rsp: |
73 shows "R f (REP (ABS g)) = R f g" |
73 shows "R f (rep (abs g)) = R f g" |
74 and "R (REP (ABS g)) f = R g f" |
74 and "R (rep (abs g)) f = R g f" |
75 by (simp_all add: thm10 thm11) |
75 by (simp_all add: thm10 thm11) |
76 |
76 |
77 lemma Quotient: |
77 lemma Quotient: |
78 "Quotient R ABS REP" |
78 "Quotient R abs rep" |
79 apply(unfold Quotient_def) |
79 apply(unfold Quotient_def) |
80 apply(simp add: thm10) |
80 apply(simp add: thm10) |
81 apply(simp add: REP_refl) |
81 apply(simp add: rep_refl) |
82 apply(subst thm11[symmetric]) |
82 apply(subst thm11[symmetric]) |
83 apply(simp add: equivp[simplified equivp_def]) |
83 apply(simp add: equivp[simplified equivp_def]) |
84 done |
84 done |
85 |
85 |
86 end |
86 end |