author  huffman 
Tue, 02 Mar 2010 17:21:10 0800  
changeset 35525  fa231b86cb1e 
parent 33808  31169fdc5ae7 
child 37678  0040bafffdef 
permissions  rwrr 
25903  1 
(* Title: HOLCF/Bifinite.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Bifinite domains and approximation *} 

6 

7 
theory Bifinite 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

8 
imports Deflation 
25903  9 
begin 
10 

26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
25923
diff
changeset

11 
subsection {* Omegaprofinite and bifinite domains *} 
25903  12 

29614
1f7b1b0df292
simplified handling of base sort, dropped axclass
haftmann
parents:
29252
diff
changeset

13 
class profinite = 
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

14 
fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a" 
27310  15 
assumes chain_approx [simp]: "chain approx" 
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

16 
assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x" 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

17 
assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

18 
assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}" 
25903  19 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

20 
class bifinite = profinite + pcpo 
25909
6b96b9392873
add class bifinite_cpo for possiblyunpointed bifinite domains
huffman
parents:
25903
diff
changeset

21 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

22 
lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

23 
proof  
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

24 
have "chain (\<lambda>i. approx i\<cdot>x)" by simp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

25 
hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

26 
thus "approx i\<cdot>x \<sqsubseteq> x" by simp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

27 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

28 

253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

29 
lemma finite_deflation_approx: "finite_deflation (approx i)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

30 
proof 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

31 
fix x :: 'a 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

32 
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

33 
by (rule approx_idem) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

34 
show "approx i\<cdot>x \<sqsubseteq> x" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

35 
by (rule approx_below) 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

36 
show "finite {x. approx i\<cdot>x = x}" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

37 
by (rule finite_fixes_approx) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

38 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

39 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29614
diff
changeset

40 
interpretation approx: finite_deflation "approx i" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

41 
by (rule finite_deflation_approx) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

42 

28234
fc420a5cf72e
Do not rely on locale assumption in interpretation.
ballarin
parents:
27402
diff
changeset

43 
lemma (in deflation) deflation: "deflation d" .. 
fc420a5cf72e
Do not rely on locale assumption in interpretation.
ballarin
parents:
27402
diff
changeset

44 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

45 
lemma deflation_approx: "deflation (approx i)" 
28234
fc420a5cf72e
Do not rely on locale assumption in interpretation.
ballarin
parents:
27402
diff
changeset

46 
by (rule approx.deflation) 
25903  47 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

48 
lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)" 
25903  49 
by (rule ext_cfun, simp add: contlub_cfun_fun) 
50 

27309  51 
lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

52 
by (rule UU_I, rule approx_below) 
25903  53 

54 
lemma approx_approx1: 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

55 
"i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

56 
apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx]) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25909
diff
changeset

57 
apply (erule chain_mono [OF chain_approx]) 
25903  58 
done 
59 

60 
lemma approx_approx2: 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

61 
"j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

62 
apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx]) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25909
diff
changeset

63 
apply (erule chain_mono [OF chain_approx]) 
25903  64 
done 
65 

66 
lemma approx_approx [simp]: 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

67 
"approx i\<cdot>(approx j\<cdot>x) = approx (min i j)\<cdot>x" 
25903  68 
apply (rule_tac x=i and y=j in linorder_le_cases) 
69 
apply (simp add: approx_approx1 min_def) 

70 
apply (simp add: approx_approx2 min_def) 

71 
done 

72 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

73 
lemma finite_image_approx: "finite ((\<lambda>x. approx n\<cdot>x) ` A)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

74 
by (rule approx.finite_image) 
25903  75 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

76 
lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

77 
by (rule approx.finite_range) 
27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

78 

416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

79 
lemma compact_approx [simp]: "compact (approx n\<cdot>x)" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

80 
by (rule approx.compact) 
25903  81 

27309  82 
lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

83 
by (rule admD2, simp_all) 
25903  84 

27309  85 
lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)" 
25903  86 
apply (rule iffI) 
27309  87 
apply (erule profinite_compact_eq_approx) 
25903  88 
apply (erule exE) 
89 
apply (erule subst) 

90 
apply (rule compact_approx) 

91 
done 

92 

93 
lemma approx_induct: 

94 
assumes adm: "adm P" and P: "\<And>n x. P (approx n\<cdot>x)" 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

95 
shows "P x" 
25903  96 
proof  
97 
have "P (\<Squnion>n. approx n\<cdot>x)" 

98 
by (rule admD [OF adm], simp, simp add: P) 

99 
thus "P x" by simp 

100 
qed 

101 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

102 
lemma profinite_below_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y" 
25903  103 
apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp) 
25923  104 
apply (rule lub_mono, simp, simp, simp) 
25903  105 
done 
106 

31113
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

107 
subsection {* Instance for product type *} 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

108 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

109 
definition 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

110 
cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

111 
where 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

112 
"cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

113 

b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

114 
lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

115 
unfolding cprod_map_def by simp 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

116 

33808  117 
lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID" 
118 
unfolding expand_cfun_eq by auto 

119 

33587  120 
lemma cprod_map_map: 
121 
"cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) = 

122 
cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" 

123 
by (induct p) simp 

124 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

125 
lemma ep_pair_cprod_map: 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

126 
assumes "ep_pair e1 p1" and "ep_pair e2 p2" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

127 
shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

128 
proof 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

129 
interpret e1p1: ep_pair e1 p1 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

130 
interpret e2p2: ep_pair e2 p2 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

131 
fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

132 
by (induct x) simp 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

133 
fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

134 
by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

135 
qed 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

136 

b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

137 
lemma deflation_cprod_map: 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

138 
assumes "deflation d1" and "deflation d2" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

139 
shows "deflation (cprod_map\<cdot>d1\<cdot>d2)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

140 
proof 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

141 
interpret d1: deflation d1 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

142 
interpret d2: deflation d2 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

143 
fix x 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

144 
show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

145 
by (induct x) (simp add: d1.idem d2.idem) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

146 
show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

147 
by (induct x) (simp add: d1.below d2.below) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

148 
qed 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

149 

b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

150 
lemma finite_deflation_cprod_map: 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

151 
assumes "finite_deflation d1" and "finite_deflation d2" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

152 
shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

153 
proof (intro finite_deflation.intro finite_deflation_axioms.intro) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

154 
interpret d1: finite_deflation d1 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

155 
interpret d2: finite_deflation d2 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

156 
have "deflation d1" and "deflation d2" by fact+ 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

157 
thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

158 
have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

159 
by clarsimp 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

160 
thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

161 
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

162 
qed 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

163 

31113
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

164 
instantiation "*" :: (profinite, profinite) profinite 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

165 
begin 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

166 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

167 
definition 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

168 
approx_prod_def: 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

169 
"approx = (\<lambda>n. cprod_map\<cdot>(approx n)\<cdot>(approx n))" 
31113
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

170 

15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

171 
instance proof 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

172 
fix i :: nat and x :: "'a \<times> 'b" 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

173 
show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)" 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

174 
unfolding approx_prod_def by simp 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

175 
show "(\<Squnion>i. approx i\<cdot>x) = x" 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

176 
unfolding approx_prod_def cprod_map_def 
31113
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

177 
by (simp add: lub_distribs thelub_Pair) 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

178 
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

179 
unfolding approx_prod_def cprod_map_def by simp 
31113
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

180 
have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq> 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

181 
{x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}" 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

182 
unfolding approx_prod_def by clarsimp 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

183 
thus "finite {x::'a \<times> 'b. approx i\<cdot>x = x}" 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

184 
by (rule finite_subset, 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

185 
intro finite_cartesian_product finite_fixes_approx) 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

186 
qed 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

187 

15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

188 
end 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

189 

15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

190 
instance "*" :: (bifinite, bifinite) bifinite .. 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

191 

15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

192 
lemma approx_Pair [simp]: 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

193 
"approx i\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)" 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

194 
unfolding approx_prod_def by simp 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

195 

15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

196 
lemma fst_approx: "fst (approx i\<cdot>p) = approx i\<cdot>(fst p)" 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

197 
by (induct p, simp) 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

198 

15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

199 
lemma snd_approx: "snd (approx i\<cdot>p) = approx i\<cdot>(snd p)" 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

200 
by (induct p, simp) 
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

201 

15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset

202 

25903  203 
subsection {* Instance for continuous function space *} 
204 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

205 
definition 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

206 
cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

207 
where 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

208 
"cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

209 

b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

210 
lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

211 
unfolding cfun_map_def by simp 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

212 

33808  213 
lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID" 
214 
unfolding expand_cfun_eq by simp 

215 

33587  216 
lemma cfun_map_map: 
217 
"cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) = 

218 
cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" 

219 
by (rule ext_cfun) simp 

220 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

221 
lemma ep_pair_cfun_map: 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

222 
assumes "ep_pair e1 p1" and "ep_pair e2 p2" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

223 
shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

224 
proof 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

225 
interpret e1p1: ep_pair e1 p1 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

226 
interpret e2p2: ep_pair e2 p2 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

227 
fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

228 
by (simp add: expand_cfun_eq) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

229 
fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

230 
apply (rule below_cfun_ext, simp) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

231 
apply (rule below_trans [OF e2p2.e_p_below]) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

232 
apply (rule monofun_cfun_arg) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

233 
apply (rule e1p1.e_p_below) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

234 
done 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

235 
qed 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

236 

b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

237 
lemma deflation_cfun_map: 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

238 
assumes "deflation d1" and "deflation d2" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

239 
shows "deflation (cfun_map\<cdot>d1\<cdot>d2)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

240 
proof 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

241 
interpret d1: deflation d1 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

242 
interpret d2: deflation d2 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

243 
fix f 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

244 
show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

245 
by (simp add: expand_cfun_eq d1.idem d2.idem) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

246 
show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

247 
apply (rule below_cfun_ext, simp) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

248 
apply (rule below_trans [OF d2.below]) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

249 
apply (rule monofun_cfun_arg) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

250 
apply (rule d1.below) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

251 
done 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

252 
qed 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

253 

b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

254 
lemma finite_range_cfun_map: 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

255 
assumes a: "finite (range (\<lambda>x. a\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

256 
assumes b: "finite (range (\<lambda>y. b\<cdot>y))" 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

257 
shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))" (is "finite (range ?h)") 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

258 
proof (rule finite_imageD) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

259 
let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

260 
show "finite (?f ` range ?h)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

261 
proof (rule finite_subset) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

262 
let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

263 
show "?f ` range ?h \<subseteq> ?B" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

264 
by clarsimp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

265 
show "finite ?B" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

266 
by (simp add: a b) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

267 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

268 
show "inj_on ?f (range ?h)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

269 
proof (rule inj_onI, rule ext_cfun, clarsimp) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

270 
fix x f g 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

271 
assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

272 
hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

273 
by (rule equalityD1) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

274 
hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

275 
by (simp add: subset_eq) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

276 
then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

277 
by (rule rangeE) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

278 
thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

279 
by clarsimp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

280 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

281 
qed 
25903  282 

33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

283 
lemma finite_deflation_cfun_map: 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

284 
assumes "finite_deflation d1" and "finite_deflation d2" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

285 
shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

286 
proof (intro finite_deflation.intro finite_deflation_axioms.intro) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

287 
interpret d1: finite_deflation d1 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

288 
interpret d2: finite_deflation d2 by fact 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

289 
have "deflation d1" and "deflation d2" by fact+ 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

290 
thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

291 
have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

292 
using d1.finite_range d2.finite_range 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

293 
by (rule finite_range_cfun_map) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

294 
thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

295 
by (rule finite_range_imp_finite_fixes) 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

296 
qed 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

297 

35525  298 
instantiation cfun :: (profinite, profinite) profinite 
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

299 
begin 
25903  300 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

301 
definition 
25903  302 
approx_cfun_def: 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

303 
"approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))" 
25903  304 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

305 
instance proof 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

306 
show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

307 
unfolding approx_cfun_def by simp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

308 
next 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

309 
fix x :: "'a \<rightarrow> 'b" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

310 
show "(\<Squnion>i. approx i\<cdot>x) = x" 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

311 
unfolding approx_cfun_def cfun_map_def 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

312 
by (simp add: lub_distribs eta_cfun) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

313 
next 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

314 
fix i :: nat and x :: "'a \<rightarrow> 'b" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

315 
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

316 
unfolding approx_cfun_def cfun_map_def by simp 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

317 
next 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

318 
fix i :: nat 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

319 
show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}" 
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

320 
unfolding approx_cfun_def 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

321 
by (intro finite_deflation.finite_fixes 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

322 
finite_deflation_cfun_map 
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset

323 
finite_deflation_approx) 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

324 
qed 
25903  325 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

326 
end 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

327 

35525  328 
instance cfun :: (profinite, bifinite) bifinite .. 
25909
6b96b9392873
add class bifinite_cpo for possiblyunpointed bifinite domains
huffman
parents:
25903
diff
changeset

329 

25903  330 
lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))" 
331 
by (simp add: approx_cfun_def) 

332 

333 
end 