64 qed |
64 qed |
65 |
65 |
66 text {* Relator for 'a endofun. *} |
66 text {* Relator for 'a endofun. *} |
67 |
67 |
68 definition |
68 definition |
69 endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" |
69 rel_endofun' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" |
70 where |
70 where |
71 "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)" |
71 "rel_endofun' R = (\<lambda>f g. (R ===> R) f g)" |
72 |
72 |
73 quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is |
73 quotient_definition "rel_endofun :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is |
74 endofun_rel' done |
74 rel_endofun' done |
75 |
75 |
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 (endofun_rel 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 (hide_lams, 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. endofun_rel 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 endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_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) |
87 next |
87 next |
88 have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" |
88 have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" |
89 by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun]) |
89 by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun]) |
90 fix r s |
90 fix r s |
91 show "endofun_rel R r s = |
91 show "rel_endofun R r s = |
92 (endofun_rel R r r \<and> |
92 (rel_endofun R r r \<and> |
93 endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)" |
93 rel_endofun R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)" |
94 apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def) |
94 apply(auto simp add: rel_endofun_def rel_endofun'_def map_endofun_def map_endofun'_def) |
95 using fun_quotient3[OF a a,THEN Quotient3_refl1] |
95 using fun_quotient3[OF a a,THEN Quotient3_refl1] |
96 apply metis |
96 apply metis |
97 using fun_quotient3[OF a a,THEN Quotient3_refl2] |
97 using fun_quotient3[OF a a,THEN Quotient3_refl2] |
98 apply metis |
98 apply metis |
99 using fun_quotient3[OF a a, THEN Quotient3_rel] |
99 using fun_quotient3[OF a a, THEN Quotient3_rel] |
100 apply metis |
100 apply metis |
101 by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq) |
101 by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq) |
102 qed |
102 qed |
103 |
103 |
104 declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]] |
104 declare [[mapQ3 endofun = (rel_endofun, endofun_quotient)]] |
105 |
105 |
106 quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done |
106 quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done |
107 |
107 |
108 term endofun_id_id |
108 term endofun_id_id |
109 thm endofun_id_id_def |
109 thm endofun_id_id_def |