equal
deleted
inserted
replaced
76 lemma endofun_quotient: |
76 lemma endofun_quotient: |
77 assumes a: "Quotient3 R Abs Rep" |
77 assumes a: "Quotient3 R Abs Rep" |
78 shows "Quotient3 (rel_endofun R) (map_endofun Abs Rep) (map_endofun Rep Abs)" |
78 shows "Quotient3 (rel_endofun R) (map_endofun Abs Rep) (map_endofun Rep Abs)" |
79 proof (intro Quotient3I) |
79 proof (intro Quotient3I) |
80 show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a" |
80 show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a" |
81 by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs) |
81 by (metis (opaque_lifting, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs) |
82 next |
82 next |
83 show "\<And>a. rel_endofun R (map_endofun Rep Abs a) (map_endofun Rep Abs a)" |
83 show "\<And>a. rel_endofun R (map_endofun Rep Abs a) (map_endofun Rep Abs a)" |
84 using fun_quotient3[OF a a, THEN Quotient3_rep_reflp] |
84 using fun_quotient3[OF a a, THEN Quotient3_rep_reflp] |
85 unfolding rel_endofun_def map_endofun_def map_fun_def o_def map_endofun'_def rel_endofun'_def id_def |
85 unfolding rel_endofun_def map_endofun_def map_fun_def o_def map_endofun'_def rel_endofun'_def id_def |
86 by (metis (mono_tags) Quotient3_endofun rep_abs_rsp) |
86 by (metis (mono_tags) Quotient3_endofun rep_abs_rsp) |