author | kuncar |
Mon, 26 Mar 2012 18:32:22 +0200 | |
changeset 47119 | 81ada90d8220 |
parent 47116 | 529d2a949bd4 |
child 47308 | 9caab698dbe4 |
permissions | -rw-r--r-- |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
1 |
(* Title: HOL/Quotient_Examples/Lift_Fun.thy |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
2 |
Author: Ondrej Kuncar |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
3 |
*) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
4 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
5 |
header {* Example of lifting definitions with contravariant or co/contravariant type variables *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
6 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
7 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
8 |
theory Lift_Fun |
47097 | 9 |
imports Main "~~/src/HOL/Library/Quotient_Syntax" |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
10 |
begin |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
11 |
|
47119 | 12 |
text {* This file is meant as a test case. |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
13 |
It contains examples of lifting definitions with quotients that have contravariant |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
14 |
type variables or type variables which are covariant and contravariant in the same time. *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
15 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
16 |
subsection {* Contravariant type variables *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
17 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
18 |
text {* 'a is a contravariant type variable and we are able to map over this variable |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
19 |
in the following four definitions. This example is based on HOL/Fun.thy. *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
20 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
21 |
quotient_type |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
22 |
('a, 'b) fun' (infixr "\<rightarrow>" 55) = "'a \<Rightarrow> 'b" / "op =" |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
23 |
by (simp add: identity_equivp) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
24 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
25 |
quotient_definition "comp' :: ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c" is |
47092 | 26 |
"comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
27 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
28 |
quotient_definition "fcomp' :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" is |
47092 | 29 |
fcomp done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
30 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
31 |
quotient_definition "map_fun' :: ('c \<rightarrow> 'a) \<rightarrow> ('b \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'c \<rightarrow> 'd" |
47092 | 32 |
is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
33 |
|
47092 | 34 |
quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
35 |
|
47092 | 36 |
quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
37 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
38 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
39 |
subsection {* Co/Contravariant type variables *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
40 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
41 |
text {* 'a is a covariant and contravariant type variable in the same time. |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
42 |
The following example is a bit artificial. We haven't had a natural one yet. *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
43 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
44 |
quotient_type 'a endofun = "'a \<Rightarrow> 'a" / "op =" by (simp add: identity_equivp) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
45 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
46 |
definition map_endofun' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ('a => 'a) \<Rightarrow> ('b => 'b)" |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
47 |
where "map_endofun' f g e = map_fun g f e" |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
48 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
49 |
quotient_definition "map_endofun :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun" is |
47092 | 50 |
map_endofun' done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
51 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
52 |
text {* Registration of the map function for 'a endofun. *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
53 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
54 |
enriched_type map_endofun : map_endofun |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
55 |
proof - |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
56 |
have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient_endofun by (auto simp: Quotient_def) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
57 |
then show "map_endofun id id = id" |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
58 |
by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
59 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
60 |
have a:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient_endofun |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
61 |
Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
62 |
show "\<And>f g h i. map_endofun f g \<circ> map_endofun h i = map_endofun (f \<circ> h) (i \<circ> g)" |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
63 |
by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
64 |
qed |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
65 |
|
47097 | 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 |
|
47116 | 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: Quotient_rep_abs[OF Quotient_endofun]) |
|
90 |
fix r s |
|
91 |
show "endofun_rel R r s = |
|
47097 | 92 |
(endofun_rel R r r \<and> |
93 |
endofun_rel 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) |
|
95 |
using fun_quotient[OF a a,THEN Quotient_refl1] |
|
96 |
apply metis |
|
97 |
using fun_quotient[OF a a,THEN Quotient_refl2] |
|
98 |
apply metis |
|
99 |
using fun_quotient[OF a a, THEN Quotient_rel] |
|
100 |
apply metis |
|
47116 | 101 |
by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq) |
47097 | 102 |
qed |
103 |
||
104 |
declare [[map endofun = (endofun_rel, endofun_quotient)]] |
|
105 |
||
47092 | 106 |
quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
107 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
108 |
term endofun_id_id |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
109 |
thm endofun_id_id_def |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
110 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
111 |
quotient_type 'a endofun' = "'a endofun" / "op =" by (simp add: identity_equivp) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
112 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
113 |
text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting) |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
114 |
over a type variable which is a covariant and contravariant type variable. *} |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
115 |
|
47092 | 116 |
quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id done |
45799
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
117 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
118 |
term endofun'_id_id |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
119 |
thm endofun'_id_id_def |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
120 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
121 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
122 |
end |