author  hoelzl 
Wed, 14 Sep 2011 10:08:52 0400  
changeset 44928  7ef6505bde7f 
parent 32960  69916a850301 
child 46508  ec9630fe9ca7 
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 
Author: David von Oheimb, TU Muenchen 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

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

4 

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

6 

15131  7 
theory Continuity 
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
30950
diff
changeset

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

10 

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

22367  13 
definition 
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22431
diff
changeset

14 
chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where 
22367  15 
"chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))" 
16 

17 
definition 

22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22431
diff
changeset

18 
continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where 
22367  19 
"continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))" 
21312  20 

21 
lemma SUP_nat_conv: 

22431  22 
"(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))" 
21312  23 
apply(rule order_antisym) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
32960
diff
changeset

24 
apply(rule SUP_least) 
21312  25 
apply(case_tac n) 
26 
apply simp 

44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
32960
diff
changeset

27 
apply (fast intro:SUP_upper le_supI2) 
21312  28 
apply(simp) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
32960
diff
changeset

29 
apply (blast intro:SUP_least SUP_upper) 
21312  30 
done 
31 

22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22431
diff
changeset

32 
lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice" 
21312  33 
assumes "continuous F" shows "mono F" 
34 
proof 

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

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

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

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22367
diff
changeset

38 
have "F B = sup (F A) (F B)" 
21312  39 
proof  
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22367
diff
changeset

40 
have "sup A B = B" using `A <= B` by (simp add:sup_absorb2) 
22431  41 
hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp 
21312  42 
also have "\<dots> = (SUP i. F(?C i))" 
43 
using `chain ?C` `continuous F` by(simp add:continuous_def) 

22431  44 
also have "\<dots> = sup (F A) (F B)" by (subst SUP_nat_conv) simp 
21312  45 
finally show ?thesis . 
46 
qed 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22367
diff
changeset

47 
thus "F A \<le> F B" by(subst le_iff_sup, simp) 
21312  48 
qed 
49 

50 
lemma continuous_lfp: 

30971  51 
assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" 
21312  52 
proof  
53 
note mono = continuous_mono[OF `continuous F`] 

30971  54 
{ fix i have "(F ^^ i) bot \<le> lfp F" 
21312  55 
proof (induct i) 
30971  56 
show "(F ^^ 0) bot \<le> lfp F" by simp 
21312  57 
next 
58 
case (Suc i) 

30971  59 
have "(F ^^ Suc i) bot = F((F ^^ i) bot)" by simp 
21312  60 
also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc]) 
61 
also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric]) 

62 
finally show ?case . 

63 
qed } 

44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
32960
diff
changeset

64 
hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_least) 
30971  65 
moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U") 
21312  66 
proof (rule lfp_lowerbound) 
30971  67 
have "chain(%i. (F ^^ i) bot)" 
21312  68 
proof  
30971  69 
{ fix i have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

70 
proof (induct i) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

71 
case 0 show ?case by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

72 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

73 
case Suc thus ?case using monoD[OF mono Suc] by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

74 
qed } 
21312  75 
thus ?thesis by(auto simp add:chain_def) 
76 
qed 

30971  77 
hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
32960
diff
changeset

78 
also have "\<dots> \<le> ?U" by(fast intro:SUP_least SUP_upper) 
21312  79 
finally show "F ?U \<le> ?U" . 
80 
qed 

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

82 
qed 

83 

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

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

86 

87 

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

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

89 

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

91 
up_chain :: "(nat => 'a set) => bool" where 
19736  92 
"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

93 

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

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

96 

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

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

99 

19736  100 
lemma up_chain_less_mono: 
101 
"up_chain F ==> x < y ==> F x \<subseteq> F y" 

102 
apply (induct y) 

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

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

105 

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

108 
apply (blast dest: up_chain_less_mono) 

109 
done 

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

110 

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

111 

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

113 
down_chain :: "(nat => 'a set) => bool" where 
19736  114 
"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

115 

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

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

118 

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

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

121 

19736  122 
lemma down_chain_less_mono: 
123 
"down_chain F ==> x < y ==> F y \<subseteq> F x" 

124 
apply (induct y) 

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

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

127 

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

130 
apply (blast dest: down_chain_less_mono) 

131 
done 

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

132 

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

133 

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

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

135 

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

137 
up_cont :: "('a set => 'a set) => bool" where 
19736  138 
"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

139 

11355  140 
lemma up_contI: 
24331  141 
"(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f" 
142 
apply (unfold up_cont_def) 

143 
apply blast 

144 
done 

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

145 

11355  146 
lemma up_contD: 
24331  147 
"up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)" 
148 
apply (unfold up_cont_def) 

149 
apply auto 

150 
done 

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

151 

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

152 

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

153 
lemma up_cont_mono: "up_cont f ==> mono f" 
24331  154 
apply (rule monoI) 
25076  155 
apply (drule_tac F = "\<lambda>i. if i = 0 then x else y" in up_contD) 
24331  156 
apply (rule up_chainI) 
157 
apply simp 

158 
apply (drule Un_absorb1) 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
30971
diff
changeset

159 
apply (auto split:split_if_asm) 
24331  160 
done 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

161 

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

162 

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

164 
down_cont :: "('a set => 'a set) => bool" where 
19736  165 
"down_cont f = 
166 
(\<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

167 

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

170 
down_cont f" 

171 
apply (unfold down_cont_def) 

172 
apply blast 

173 
done 

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

174 

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

177 
apply (unfold down_cont_def) 

178 
apply auto 

179 
done 

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

180 

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

181 
lemma down_cont_mono: "down_cont f ==> mono f" 
24331  182 
apply (rule monoI) 
25076  183 
apply (drule_tac F = "\<lambda>i. if i = 0 then y else x" in down_contD) 
24331  184 
apply (rule down_chainI) 
185 
apply simp 

186 
apply (drule Int_absorb1) 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
30971
diff
changeset

187 
apply (auto split:split_if_asm) 
24331  188 
done 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

189 

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

190 

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

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

192 

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

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

196 

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

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

199 

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

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

202 

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

203 
lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)" 
11355  204 
apply (rule up_chainI) 
205 
apply (induct_tac i) 

206 
apply simp+ 

207 
apply (erule (1) monoD) 

208 
done 

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

209 

11355  210 
lemma UNION_up_iterate_is_fp: 
211 
"up_cont F ==> 

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

213 
apply (frule up_cont_mono [THEN up_iterate_chain]) 

214 
apply (drule (1) up_contD) 

215 
apply simp 

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

217 
apply (case_tac xa) 

218 
apply auto 

219 
done 

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

220 

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

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

224 
apply fast 

225 
apply (induct_tac i) 

226 
prefer 2 apply (drule (1) monoD) 

227 
apply auto 

228 
done 

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

229 

11355  230 
lemma UNION_up_iterate_is_lfp: 
231 
"up_cont F ==> lfp F = UNION UNIV (up_iterate F)" 

232 
apply (rule set_eq_subset [THEN iffD2]) 

233 
apply (rule conjI) 

234 
prefer 2 

235 
apply (drule up_cont_mono) 

236 
apply (rule UNION_up_iterate_lowerbound) 

237 
apply assumption 

238 
apply (erule lfp_unfold [symmetric]) 

239 
apply (rule lfp_lowerbound) 

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

241 
apply (erule UNION_up_iterate_is_fp [symmetric]) 

242 
done 

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

243 

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

244 

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

246 
down_iterate :: "('a set => 'a set) => nat => 'a set" where 
30971  247 
"down_iterate f n = (f ^^ n) UNIV" 
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 
lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV" 
11355  250 
by (simp add: down_iterate_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

251 

11355  252 
lemma down_iterate_Suc [simp]: 
253 
"down_iterate f (Suc i) = f (down_iterate f i)" 

254 
by (simp add: down_iterate_def) 

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

255 

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

256 
lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)" 
11355  257 
apply (rule down_chainI) 
258 
apply (induct_tac i) 

259 
apply simp+ 

260 
apply (erule (1) monoD) 

261 
done 

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

262 

11355  263 
lemma INTER_down_iterate_is_fp: 
264 
"down_cont F ==> 

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

266 
apply (frule down_cont_mono [THEN down_iterate_chain]) 

267 
apply (drule (1) down_contD) 

268 
apply simp 

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

270 
apply (case_tac xa) 

271 
apply auto 

272 
done 

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

273 

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

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

277 
apply fast 

278 
apply (induct_tac i) 

279 
prefer 2 apply (drule (1) monoD) 

280 
apply auto 

281 
done 

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

282 

11355  283 
lemma INTER_down_iterate_is_gfp: 
284 
"down_cont F ==> gfp F = INTER UNIV (down_iterate F)" 

285 
apply (rule set_eq_subset [THEN iffD2]) 

286 
apply (rule conjI) 

287 
apply (drule down_cont_mono) 

288 
apply (rule INTER_down_iterate_upperbound) 

289 
apply assumption 

290 
apply (erule gfp_unfold [symmetric]) 

291 
apply (rule gfp_upperbound) 

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

293 
apply (erule INTER_down_iterate_is_fp) 

294 
done 

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

295 

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

296 
end 