4 |
4 |
5 header {* Example of lifting definitions with contravariant or co/contravariant type variables *} |
5 header {* Example of lifting definitions with contravariant or co/contravariant type variables *} |
6 |
6 |
7 |
7 |
8 theory Lift_Fun |
8 theory Lift_Fun |
9 imports Main |
9 imports Main "~~/src/HOL/Library/Quotient_Syntax" |
10 begin |
10 begin |
11 |
11 |
12 text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. |
12 text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. |
13 It contains examples of lifting definitions with quotients that have contravariant |
13 It contains examples of lifting definitions with quotients that have contravariant |
14 type variables or type variables which are covariant and contravariant in the same time. *} |
14 type variables or type variables which are covariant and contravariant in the same time. *} |
61 Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast |
61 Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast |
62 show "\<And>f g h i. map_endofun f g \<circ> map_endofun h i = map_endofun (f \<circ> h) (i \<circ> g)" |
62 show "\<And>f g h i. map_endofun f g \<circ> map_endofun h i = map_endofun (f \<circ> h) (i \<circ> g)" |
63 by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) |
63 by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) |
64 qed |
64 qed |
65 |
65 |
|
66 text {* Relator for 'a endofun. *} |
|
67 |
|
68 definition |
|
69 endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" |
|
70 where |
|
71 "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)" |
|
72 |
|
73 quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is |
|
74 endofun_rel' done |
|
75 |
|
76 lemma endofun_quotient: |
|
77 assumes a: "Quotient R Abs Rep" |
|
78 shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)" |
|
79 proof (intro QuotientI) |
|
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) |
|
82 next |
|
83 show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)" |
|
84 using fun_quotient[OF a a, THEN Quotient_rep_reflp] |
|
85 unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def |
|
86 by (metis (mono_tags) Quotient_endofun rep_abs_rsp) |
|
87 next |
|
88 show "\<And>r s. endofun_rel R r s = |
|
89 (endofun_rel R r r \<and> |
|
90 endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)" |
|
91 apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def) |
|
92 using fun_quotient[OF a a,THEN Quotient_refl1] |
|
93 apply metis |
|
94 using fun_quotient[OF a a,THEN Quotient_refl2] |
|
95 apply metis |
|
96 using fun_quotient[OF a a, THEN Quotient_rel] |
|
97 apply metis |
|
98 using fun_quotient[OF a a, THEN Quotient_rel] |
|
99 by (smt Quotient_endofun rep_abs_rsp) |
|
100 qed |
|
101 |
|
102 declare [[map endofun = (endofun_rel, endofun_quotient)]] |
|
103 |
66 quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done |
104 quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done |
67 |
105 |
68 term endofun_id_id |
106 term endofun_id_id |
69 thm endofun_id_id_def |
107 thm endofun_id_id_def |
70 |
108 |