author  wenzelm 
Tue, 27 Feb 2007 00:33:49 +0100  
changeset 22367  6860f09242bf 
parent 21404  eb85850d3eb7 
child 22422  ee19cdb07528 
permissions  rwrr 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

1 
(* Title: HOL/Library/Continuity.thy 
11355  2 
ID: $Id$ 
3 
Author: David von Oheimb, TU Muenchen 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

4 
*) 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

5 

14706  6 
header {* Continuity and iterations (of set transformers) *} 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

7 

15131  8 
theory Continuity 
15140  9 
imports Main 
15131  10 
begin 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

11 

22367  12 
subsection {* Continuity for complete lattices *} 
21312  13 

22367  14 
definition 
15 
chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 

16 
"chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))" 

17 

18 
definition 

19 
continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool" where 

20 
"continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))" 

21312  21 

22 
abbreviation 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21312
diff
changeset

23 
bot :: "'a::order" where 
22367  24 
"bot \<equiv> Sup {}" 
21312  25 

26 
lemma SUP_nat_conv: 

22367  27 
"(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))" 
21312  28 
apply(rule order_antisym) 
29 
apply(rule SUP_leI) 

30 
apply(case_tac n) 

31 
apply simp 

32 
apply (blast intro:le_SUPI le_joinI2) 

33 
apply(simp) 

34 
apply (blast intro:SUP_leI le_SUPI) 

35 
done 

36 

37 
lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat" 

38 
assumes "continuous F" shows "mono F" 

39 
proof 

40 
fix A B :: "'a" assume "A <= B" 

41 
let ?C = "%i::nat. if i=0 then A else B" 

42 
have "chain ?C" using `A <= B` by(simp add:chain_def) 

43 
have "F B = join (F A) (F B)" 

44 
proof  

45 
have "join A B = B" using `A <= B` by (simp add:join_absorp2) 

46 
hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv) 

47 
also have "\<dots> = (SUP i. F(?C i))" 

48 
using `chain ?C` `continuous F` by(simp add:continuous_def) 

49 
also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv) 

50 
finally show ?thesis . 

51 
qed 

52 
thus "F A \<le> F B" by(subst le_def_join, simp) 

53 
qed 

54 

55 
lemma continuous_lfp: 

56 
assumes "continuous F" shows "lfp F = (SUP i. (F^i) bot)" 

57 
proof  

58 
note mono = continuous_mono[OF `continuous F`] 

59 
{ fix i have "(F^i) bot \<le> lfp F" 

60 
proof (induct i) 

61 
show "(F^0) bot \<le> lfp F" by simp 

62 
next 

63 
case (Suc i) 

64 
have "(F^(Suc i)) bot = F((F^i) bot)" by simp 

65 
also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc]) 

66 
also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric]) 

67 
finally show ?case . 

68 
qed } 

69 
hence "(SUP i. (F^i) bot) \<le> lfp F" by (blast intro!:SUP_leI) 

70 
moreover have "lfp F \<le> (SUP i. (F^i) bot)" (is "_ \<le> ?U") 

71 
proof (rule lfp_lowerbound) 

72 
have "chain(%i. (F^i) bot)" 

73 
proof  

74 
{ fix i have "(F^i) bot \<le> (F^(Suc i)) bot" 

75 
proof (induct i) 

76 
case 0 show ?case by simp 

77 
next 

78 
case Suc thus ?case using monoD[OF mono Suc] by auto 

79 
qed } 

80 
thus ?thesis by(auto simp add:chain_def) 

81 
qed 

82 
hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def) 

83 
also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI) 

84 
finally show "F ?U \<le> ?U" . 

85 
qed 

86 
ultimately show ?thesis by (blast intro:order_antisym) 

87 
qed 

88 

89 
text{* The following development is just for sets but presents an up 

90 
and a down version of chains and continuity and covers @{const gfp}. *} 

91 

92 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

93 
subsection "Chains" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

94 

19736  95 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21312
diff
changeset

96 
up_chain :: "(nat => 'a set) => bool" where 
19736  97 
"up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

98 

11355  99 
lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F" 
100 
by (simp add: up_chain_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

101 

11355  102 
lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)" 
103 
by (simp add: up_chain_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

104 

19736  105 
lemma up_chain_less_mono: 
106 
"up_chain F ==> x < y ==> F x \<subseteq> F y" 

107 
apply (induct y) 

108 
apply (blast dest: up_chainD elim: less_SucE)+ 

11355  109 
done 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

110 

11355  111 
lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y" 
112 
apply (drule le_imp_less_or_eq) 

113 
apply (blast dest: up_chain_less_mono) 

114 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

115 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

116 

19736  117 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21312
diff
changeset

118 
down_chain :: "(nat => 'a set) => bool" where 
19736  119 
"down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

120 

11355  121 
lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F" 
122 
by (simp add: down_chain_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

123 

11355  124 
lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i" 
125 
by (simp add: down_chain_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

126 

19736  127 
lemma down_chain_less_mono: 
128 
"down_chain F ==> x < y ==> F y \<subseteq> F x" 

129 
apply (induct y) 

130 
apply (blast dest: down_chainD elim: less_SucE)+ 

11355  131 
done 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

132 

11355  133 
lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x" 
134 
apply (drule le_imp_less_or_eq) 

135 
apply (blast dest: down_chain_less_mono) 

136 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

137 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

138 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

139 
subsection "Continuity" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

140 

19736  141 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21312
diff
changeset

142 
up_cont :: "('a set => 'a set) => bool" where 
19736  143 
"up_cont f = (\<forall>F. up_chain F > f (\<Union>(range F)) = \<Union>(f ` range F))" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

144 

11355  145 
lemma up_contI: 
146 
"(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f" 

147 
apply (unfold up_cont_def) 

148 
apply blast 

149 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

150 

11355  151 
lemma up_contD: 
152 
"up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)" 

153 
apply (unfold up_cont_def) 

154 
apply auto 

155 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

156 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

157 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

158 
lemma up_cont_mono: "up_cont f ==> mono f" 
11355  159 
apply (rule monoI) 
160 
apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD) 

161 
apply (rule up_chainI) 

162 
apply simp+ 

163 
apply (drule Un_absorb1) 

11461  164 
apply (auto simp add: nat_not_singleton) 
11355  165 
done 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

166 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

167 

19736  168 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21312
diff
changeset

169 
down_cont :: "('a set => 'a set) => bool" where 
19736  170 
"down_cont f = 
171 
(\<forall>F. down_chain F > f (Inter (range F)) = Inter (f ` range F))" 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

172 

11355  173 
lemma down_contI: 
174 
"(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==> 

175 
down_cont f" 

176 
apply (unfold down_cont_def) 

177 
apply blast 

178 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

179 

11355  180 
lemma down_contD: "down_cont f ==> down_chain F ==> 
181 
f (Inter (range F)) = Inter (f ` range F)" 

182 
apply (unfold down_cont_def) 

183 
apply auto 

184 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

185 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

186 
lemma down_cont_mono: "down_cont f ==> mono f" 
11355  187 
apply (rule monoI) 
188 
apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD) 

189 
apply (rule down_chainI) 

190 
apply simp+ 

191 
apply (drule Int_absorb1) 

11461  192 
apply (auto simp add: nat_not_singleton) 
11355  193 
done 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

194 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

195 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

196 
subsection "Iteration" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

197 

19736  198 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21312
diff
changeset

199 
up_iterate :: "('a set => 'a set) => nat => 'a set" where 
19736  200 
"up_iterate f n = (f^n) {}" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

201 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

202 
lemma up_iterate_0 [simp]: "up_iterate f 0 = {}" 
11355  203 
by (simp add: up_iterate_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

204 

11355  205 
lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)" 
206 
by (simp add: up_iterate_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

207 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

208 
lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)" 
11355  209 
apply (rule up_chainI) 
210 
apply (induct_tac i) 

211 
apply simp+ 

212 
apply (erule (1) monoD) 

213 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

214 

11355  215 
lemma UNION_up_iterate_is_fp: 
216 
"up_cont F ==> 

217 
F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)" 

218 
apply (frule up_cont_mono [THEN up_iterate_chain]) 

219 
apply (drule (1) up_contD) 

220 
apply simp 

221 
apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric]) 

222 
apply (case_tac xa) 

223 
apply auto 

224 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

225 

11355  226 
lemma UNION_up_iterate_lowerbound: 
227 
"mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P" 

228 
apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)") 

229 
apply fast 

230 
apply (induct_tac i) 

231 
prefer 2 apply (drule (1) monoD) 

232 
apply auto 

233 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

234 

11355  235 
lemma UNION_up_iterate_is_lfp: 
236 
"up_cont F ==> lfp F = UNION UNIV (up_iterate F)" 

237 
apply (rule set_eq_subset [THEN iffD2]) 

238 
apply (rule conjI) 

239 
prefer 2 

240 
apply (drule up_cont_mono) 

241 
apply (rule UNION_up_iterate_lowerbound) 

242 
apply assumption 

243 
apply (erule lfp_unfold [symmetric]) 

244 
apply (rule lfp_lowerbound) 

245 
apply (rule set_eq_subset [THEN iffD1, THEN conjunct2]) 

246 
apply (erule UNION_up_iterate_is_fp [symmetric]) 

247 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

248 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

249 

19736  250 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21312
diff
changeset

251 
down_iterate :: "('a set => 'a set) => nat => 'a set" where 
19736  252 
"down_iterate f n = (f^n) UNIV" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

253 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

254 
lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV" 
11355  255 
by (simp add: down_iterate_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

256 

11355  257 
lemma down_iterate_Suc [simp]: 
258 
"down_iterate f (Suc i) = f (down_iterate f i)" 

259 
by (simp add: down_iterate_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

260 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

261 
lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)" 
11355  262 
apply (rule down_chainI) 
263 
apply (induct_tac i) 

264 
apply simp+ 

265 
apply (erule (1) monoD) 

266 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

267 

11355  268 
lemma INTER_down_iterate_is_fp: 
269 
"down_cont F ==> 

270 
F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)" 

271 
apply (frule down_cont_mono [THEN down_iterate_chain]) 

272 
apply (drule (1) down_contD) 

273 
apply simp 

274 
apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric]) 

275 
apply (case_tac xa) 

276 
apply auto 

277 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

278 

11355  279 
lemma INTER_down_iterate_upperbound: 
280 
"mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)" 

281 
apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)") 

282 
apply fast 

283 
apply (induct_tac i) 

284 
prefer 2 apply (drule (1) monoD) 

285 
apply auto 

286 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

287 

11355  288 
lemma INTER_down_iterate_is_gfp: 
289 
"down_cont F ==> gfp F = INTER UNIV (down_iterate F)" 

290 
apply (rule set_eq_subset [THEN iffD2]) 

291 
apply (rule conjI) 

292 
apply (drule down_cont_mono) 

293 
apply (rule INTER_down_iterate_upperbound) 

294 
apply assumption 

295 
apply (erule gfp_unfold [symmetric]) 

296 
apply (rule gfp_upperbound) 

297 
apply (rule set_eq_subset [THEN iffD1, THEN conjunct2]) 

298 
apply (erule INTER_down_iterate_is_fp) 

299 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

300 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

301 
end 