equal
deleted
inserted
replaced
65 quotient_type 'a rel = "('a * 'a) set" / "(op =)" |
65 quotient_type 'a rel = "('a * 'a) set" / "(op =)" |
66 morphisms set_of_rel rel_of_set by (metis identity_equivp) |
66 morphisms set_of_rel rel_of_set by (metis identity_equivp) |
67 |
67 |
68 lemma [simp]: |
68 lemma [simp]: |
69 "rel_of_set (set_of_rel S) = S" |
69 "rel_of_set (set_of_rel S) = S" |
70 by (rule Quotient_abs_rep[OF Quotient_rel]) |
70 by (rule Quotient3_abs_rep[OF Quotient3_rel]) |
71 |
71 |
72 lemma [simp]: |
72 lemma [simp]: |
73 "set_of_rel (rel_of_set R) = R" |
73 "set_of_rel (rel_of_set R) = R" |
74 by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl) |
74 by (rule Quotient3_rep_abs[OF Quotient3_rel]) (rule refl) |
75 |
75 |
76 lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"] |
76 lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"] |
77 |
77 |
78 quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done |
78 quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done |
79 |
79 |