equal
deleted
inserted
replaced
150 lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b" |
150 lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b" |
151 using a unfolding Quotient_def |
151 using a unfolding Quotient_def |
152 by metis |
152 by metis |
153 |
153 |
154 lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
154 lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
|
155 using a unfolding Quotient_def |
|
156 by blast |
|
157 |
|
158 lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t" |
155 using a unfolding Quotient_def |
159 using a unfolding Quotient_def |
156 by blast |
160 by blast |
157 |
161 |
158 lemma Quotient_rep_abs_fold_unmap: |
162 lemma Quotient_rep_abs_fold_unmap: |
159 assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" |
163 assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" |