author  ballarin 
Tue, 30 Dec 2008 11:10:01 +0100  
changeset 29252  ea97aa6aeba2 
parent 29237  e90d9d51106b 
parent 29138  661a8db7e647 
child 29614  1f7b1b0df292 
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 

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

13 
class profinite = cpo + 
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 

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

22 
lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x" 
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" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

35 
by (rule approx_less) 
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 

29237  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>" 
25903  52 
by (rule UU_I, rule approx_less) 
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" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

56 
apply (rule deflation_less_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" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

62 
apply (rule deflation_less_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 

27309  102 
lemma profinite_less_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 

107 
subsection {* Instance for continuous function space *} 

108 

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

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

110 
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

111 
assumes b: "finite (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

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

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

114 
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

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

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

117 
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

118 
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

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

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

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

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

123 
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

124 
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

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

126 
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

127 
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

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

129 
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

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

131 
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

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

133 
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

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

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

136 
qed 
25903  137 

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

138 
instantiation ">" :: (profinite, profinite) profinite 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

139 
begin 
25903  140 

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

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

143 
"approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))" 
25903  144 

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

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

146 
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

147 
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

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

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

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

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

152 
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

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

154 
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

155 
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

156 
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

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

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

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

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

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

162 
apply (intro finite_range_cfun_lemma finite_range_approx) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

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

164 
qed 
25903  165 

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

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

167 

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

168 
instance ">" :: (profinite, bifinite) bifinite .. 
25909
6b96b9392873
add class bifinite_cpo for possiblyunpointed bifinite domains
huffman
parents:
25903
diff
changeset

169 

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

172 

173 
end 