author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47308  9caab698dbe4 
child 47455  26315a545e26 
permissions  rwrr 
47308  1 
(* Title: HOL/Quotient3_Examples/Lift_Fun.thy 
45799
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  
47308  56 
have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def) 
45799
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 

47308  60 
have a:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient3_endofun 
61 
Quotient3_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast 

45799
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: 

47308  77 
assumes a: "Quotient3 R Abs Rep" 
78 
shows "Quotient3 (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)" 

79 
proof (intro Quotient3I) 

47097  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)" 

47308  84 
using fun_quotient3[OF a a, THEN Quotient3_rep_reflp] 
47097  85 
unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
47308  86 
by (metis (mono_tags) Quotient3_endofun rep_abs_rsp) 
47097  87 
next 
47116  88 
have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" 
47308  89 
by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun]) 
47116  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) 

47308  95 
using fun_quotient3[OF a a,THEN Quotient3_refl1] 
47097  96 
apply metis 
47308  97 
using fun_quotient3[OF a a,THEN Quotient3_refl2] 
47097  98 
apply metis 
47308  99 
using fun_quotient3[OF a a, THEN Quotient3_rel] 
47097  100 
apply metis 
47308  101 
by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq) 
47097  102 
qed 
103 

47308  104 
declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]] 
47097  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 