author  huffman 
Wed, 02 Jan 2008 18:57:40 +0100  
changeset 25786  6b3c79acac1f 
parent 25758  89c7c22e64b4 
child 25827  c2adeb1bae5c 
permissions  rwrr 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

1 
(* Title: HOLCF/FunCpo.thy 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

2 
ID: $Id$ 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

3 
Author: Franz Regensburger 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

4 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

5 
Definition of the partial ordering for the type of all functions => (fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

6 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

7 
Class instance of => (fun) for class pcpo. 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

8 
*) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

9 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

10 
header {* Class instances for the full function space *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

11 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

12 
theory Ffun 
25786  13 
imports Cont 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

14 
begin 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

15 

18291  16 
subsection {* Full function space is a partial order *} 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

17 

25758  18 
instantiation "fun" :: (type, sq_ord) sq_ord 
19 
begin 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

20 

25758  21 
definition 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

22 
less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

23 

25758  24 
instance .. 
25 
end 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

26 

25758  27 
instance "fun" :: (type, po) po 
28 
proof 

29 
fix f :: "'a \<Rightarrow> 'b" 

30 
show "f \<sqsubseteq> f" 

31 
by (simp add: less_fun_def) 

32 
next 

33 
fix f g :: "'a \<Rightarrow> 'b" 

34 
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g" 

35 
by (simp add: less_fun_def expand_fun_eq antisym_less) 

36 
next 

37 
fix f g h :: "'a \<Rightarrow> 'b" 

38 
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h" 

39 
unfolding less_fun_def by (fast elim: trans_less) 

40 
qed 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

41 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

42 
text {* make the symbol @{text "<<"} accessible for type fun *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

43 

17831  44 
lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

45 
by (simp add: less_fun_def) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

46 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

47 
lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

48 
by (simp add: less_fun_def) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

49 

18291  50 
subsection {* Full function space is chain complete *} 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

51 

25786  52 
text {* function application is monotone *} 
53 

54 
lemma monofun_app: "monofun (\<lambda>f. f x)" 

55 
by (rule monofunI, simp add: less_fun_def) 

56 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

57 
text {* chains of functions yield chains in the po range *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

58 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

59 
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

60 
by (simp add: chain_def less_fun_def) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

61 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17831
diff
changeset

62 
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

63 
by (simp add: chain_def less_fun_def) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

64 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

65 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

66 
text {* upper bounds of function chains yield upper bound in the po range *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

67 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

68 
lemma ub2ub_fun: 
25786  69 
"range (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::po) < u \<Longrightarrow> range (\<lambda>i. S i x) < u x" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

70 
by (auto simp add: is_ub_def less_fun_def) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

71 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

72 
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

73 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

74 
lemma lub_fun: 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

75 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

76 
\<Longrightarrow> range S << (\<lambda>x. \<Squnion>i. S i x)" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

77 
apply (rule is_lubI) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

78 
apply (rule ub_rangeI) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

79 
apply (rule less_fun_ext) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

80 
apply (rule is_ub_thelub) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

81 
apply (erule ch2ch_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

82 
apply (rule less_fun_ext) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

83 
apply (rule is_lub_thelub) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

84 
apply (erule ch2ch_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

85 
apply (erule ub2ub_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

86 
done 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

87 

25786  88 
lemma lub_fun': 
89 
fixes S :: "('a::type \<Rightarrow> 'b::dcpo) set" 

90 
assumes S: "directed S" 

91 
shows "S << (\<lambda>x. \<Squnion>f\<in>S. f x)" 

92 
apply (rule is_lubI) 

93 
apply (rule is_ubI) 

94 
apply (rule less_fun_ext) 

95 
apply (rule is_ub_thelub') 

96 
apply (rule dir2dir_monofun [OF monofun_app S]) 

97 
apply (erule imageI) 

98 
apply (rule less_fun_ext) 

99 
apply (rule is_lub_thelub') 

100 
apply (rule dir2dir_monofun [OF monofun_app S]) 

101 
apply (erule ub2ub_monofun' [OF monofun_app]) 

102 
done 

103 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

104 
lemma thelub_fun: 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

105 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

106 
\<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

107 
by (rule lub_fun [THEN thelubI]) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

108 

25786  109 
lemma thelub_fun': 
110 
"directed (S::('a::type \<Rightarrow> 'b::dcpo) set) 

111 
\<Longrightarrow> lub S = (\<lambda>x. \<Squnion>f\<in>S. f x)" 

112 
by (rule lub_fun' [THEN thelubI]) 

113 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

114 
lemma cpo_fun: 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

115 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S << x" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

116 
by (rule exI, erule lub_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

117 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset

118 
instance "fun" :: (type, cpo) cpo 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

119 
by intro_classes (rule cpo_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

120 

25786  121 
lemma dcpo_fun: 
122 
"directed (S::('a::type \<Rightarrow> 'b::dcpo) set) \<Longrightarrow> \<exists>x. S << x" 

123 
by (rule exI, erule lub_fun') 

124 

125 
instance "fun" :: (type, dcpo) dcpo 

126 
by intro_classes (rule dcpo_fun) 

127 

18291  128 
subsection {* Full function space is pointed *} 
17831  129 

130 
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" 

131 
by (simp add: less_fun_def) 

132 

25786  133 
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" 
17831  134 
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) 
135 
apply (rule minimal_fun [THEN allI]) 

136 
done 

137 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset

138 
instance "fun" :: (type, pcpo) pcpo 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

139 
by intro_classes (rule least_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

140 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

141 
text {* for compatibility with old HOLCFVersion *} 
17831  142 
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

143 
by (rule minimal_fun [THEN UU_I, symmetric]) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

144 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

145 
text {* function application is strict in the left argument *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

146 
lemma app_strict [simp]: "\<bottom> x = \<bottom>" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

147 
by (simp add: inst_fun_pcpo) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

148 

25786  149 
text {* 
150 
The following results are about application for functions in @{typ "'a=>'b"} 

151 
*} 

152 

153 
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" 

154 
by (simp add: less_fun_def) 

155 

156 
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" 

157 
by (rule monofunE) 

158 

159 
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y" 

160 
by (rule trans_less [OF monofun_fun_arg monofun_fun_fun]) 

161 

162 
subsection {* Propagation of monotonicity and continuity *} 

163 

164 
text {* the lub of a chain of monotone functions is monotone *} 

165 

166 
lemma monofun_lub_fun: 

167 
"\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk> 

168 
\<Longrightarrow> monofun (\<Squnion>i. F i)" 

169 
apply (rule monofunI) 

170 
apply (simp add: thelub_fun) 

171 
apply (rule lub_mono [rule_format]) 

172 
apply (erule ch2ch_fun) 

173 
apply (erule ch2ch_fun) 

174 
apply (simp add: monofunE) 

175 
done 

176 

177 
text {* the lub of a chain of continuous functions is continuous *} 

178 

179 
declare range_composition [simp del] 

180 

181 
lemma contlub_lub_fun: 

182 
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)" 

183 
apply (rule contlubI) 

184 
apply (simp add: thelub_fun) 

185 
apply (simp add: cont2contlubE) 

186 
apply (rule ex_lub) 

187 
apply (erule ch2ch_fun) 

188 
apply (simp add: ch2ch_cont) 

189 
done 

190 

191 
lemma cont_lub_fun: 

192 
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)" 

193 
apply (rule monocontlub2cont) 

194 
apply (erule monofun_lub_fun) 

195 
apply (simp add: cont2mono) 

196 
apply (erule (1) contlub_lub_fun) 

197 
done 

198 

199 
lemma cont2cont_lub: 

200 
"\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)" 

201 
by (simp add: thelub_fun [symmetric] cont_lub_fun) 

202 

203 
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" 

204 
apply (rule monofunI) 

205 
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) 

206 
done 

207 

208 
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" 

209 
apply (rule monocontlub2cont) 

210 
apply (erule cont2mono [THEN mono2mono_fun]) 

211 
apply (rule contlubI) 

212 
apply (simp add: cont2contlubE) 

213 
apply (simp add: thelub_fun ch2ch_cont) 

214 
done 

215 

216 
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *} 

217 

218 
lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f" 

219 
apply (rule monofunI) 

220 
apply (rule less_fun_ext) 

221 
apply (blast dest: monofunE) 

222 
done 

223 

224 
lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f" 

225 
apply (subgoal_tac "monofun f") 

226 
apply (rule monocontlub2cont) 

227 
apply assumption 

228 
apply (rule contlubI) 

229 
apply (rule ext) 

230 
apply (simp add: thelub_fun ch2ch_monofun) 

231 
apply (blast dest: cont2contlubE) 

232 
apply (simp add: mono2mono_lambda cont2mono) 

233 
done 

234 

235 
text {* What D.A.Schmidt calls continuity of abstraction; never used here *} 

236 

237 
lemma contlub_lambda: 

238 
"(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo)) 

239 
\<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))" 

240 
by (simp add: thelub_fun ch2ch_lambda) 

241 

242 
lemma contlub_abstraction: 

243 
"\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow> 

244 
(\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))" 

245 
apply (rule thelub_fun [symmetric]) 

246 
apply (rule ch2ch_cont) 

247 
apply (simp add: cont2cont_lambda) 

248 
apply assumption 

249 
done 

250 

251 
lemma mono2mono_app: 

252 
"\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))" 

253 
apply (rule monofunI) 

254 
apply (simp add: monofun_fun monofunE) 

255 
done 

256 

257 
lemma cont2contlub_app: 

258 
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))" 

259 
apply (rule contlubI) 

260 
apply (subgoal_tac "chain (\<lambda>i. f (Y i))") 

261 
apply (subgoal_tac "chain (\<lambda>i. t (Y i))") 

262 
apply (simp add: cont2contlubE thelub_fun) 

263 
apply (rule diag_lub) 

264 
apply (erule ch2ch_fun) 

265 
apply (drule spec) 

266 
apply (erule (1) ch2ch_cont) 

267 
apply (erule (1) ch2ch_cont) 

268 
apply (erule (1) ch2ch_cont) 

269 
done 

270 

271 
lemma cont2cont_app: 

272 
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))" 

273 
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) 

274 

275 
lemmas cont2cont_app2 = cont2cont_app [rule_format] 

276 

277 
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))" 

278 
by (rule cont2cont_app2 [OF cont_const]) 

279 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

280 
end 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

281 