81 apply(simp add: thm10) |
81 apply(simp add: thm10) |
82 apply(simp add: REP_refl) |
82 apply(simp add: REP_refl) |
83 apply(subst thm11[symmetric]) |
83 apply(subst thm11[symmetric]) |
84 apply(simp add: equivp[simplified equivp_def]) |
84 apply(simp add: equivp[simplified equivp_def]) |
85 done |
85 done |
86 |
|
87 lemma R_trans: |
|
88 assumes ab: "R a b" |
|
89 and bc: "R b c" |
|
90 shows "R a c" |
|
91 proof - |
|
92 have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp |
|
93 moreover have ab: "R a b" by fact |
|
94 moreover have bc: "R b c" by fact |
|
95 ultimately show "R a c" unfolding transp_def by blast |
|
96 qed |
|
97 |
|
98 lemma R_sym: |
|
99 assumes ab: "R a b" |
|
100 shows "R b a" |
|
101 proof - |
|
102 have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp |
|
103 then show "R b a" using ab unfolding symp_def by blast |
|
104 qed |
|
105 |
|
106 lemma R_trans2: |
|
107 assumes ac: "R a c" |
|
108 and bd: "R b d" |
|
109 shows "R a b = R c d" |
|
110 using ac bd |
|
111 by (blast intro: R_trans R_sym) |
|
112 |
|
113 lemma REPS_same: |
|
114 shows "R (REP a) (REP b) \<equiv> (a = b)" |
|
115 proof - |
|
116 have "R (REP a) (REP b) = (a = b)" |
|
117 proof |
|
118 assume as: "R (REP a) (REP b)" |
|
119 from rep_prop |
|
120 obtain x y |
|
121 where eqs: "Rep a = R x" "Rep b = R y" by blast |
|
122 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
|
123 then have "R x (Eps (R y))" using lem9 by simp |
|
124 then have "R (Eps (R y)) x" using R_sym by blast |
|
125 then have "R y x" using lem9 by simp |
|
126 then have "R x y" using R_sym by blast |
|
127 then have "ABS x = ABS y" using thm11 by simp |
|
128 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp |
|
129 then show "a = b" using rep_inverse by simp |
|
130 next |
|
131 assume ab: "a = b" |
|
132 have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp |
|
133 then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto |
|
134 qed |
|
135 then show "R (REP a) (REP b) \<equiv> (a = b)" by simp |
|
136 qed |
|
137 |
86 |
138 end |
87 end |
139 |
88 |
140 section {* type definition for the quotient type *} |
89 section {* type definition for the quotient type *} |
141 |
90 |