equal
deleted
inserted
replaced
23 fix r s |
23 fix r s |
24 show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)" |
24 show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)" |
25 unfolding set_rel_def vimage_def set_eq_iff |
25 unfolding set_rel_def vimage_def set_eq_iff |
26 by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+ |
26 by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+ |
27 qed |
27 qed |
|
28 |
|
29 declare [[map set = (set_rel, set_quotient)]] |
28 |
30 |
29 lemma empty_set_rsp[quot_respect]: |
31 lemma empty_set_rsp[quot_respect]: |
30 "set_rel R {} {}" |
32 "set_rel R {} {}" |
31 unfolding set_rel_def by simp |
33 unfolding set_rel_def by simp |
32 |
34 |