author | kuncar |
Fri, 23 Mar 2012 14:17:29 +0100 | |
changeset 47092 | fa3538d6004b |
parent 45799 | 7fa9410c746a |
child 47097 | 987cb55cac44 |
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 |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
9 |
imports Main |
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 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
12 |
text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. |
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 |
|
47092 | 66 |
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
|
67 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
68 |
term endofun_id_id |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
69 |
thm endofun_id_id_def |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
70 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
71 |
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
|
72 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
73 |
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
|
74 |
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
|
75 |
|
47092 | 76 |
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
|
77 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
78 |
term endofun'_id_id |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
79 |
thm endofun'_id_id_def |
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
80 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
81 |
|
7fa9410c746a
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar
parents:
diff
changeset
|
82 |
end |