author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2469  b50b8c0eec01 
permissions  rwrr 
1461  1 
(* Title: ZF/fixedpt.ML 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
For fixedpt.thy. Least and greatest fixed points; the KnasterTarski Theorem 

7 

8 
Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb 

9 
*) 

10 

11 
open Fixedpt; 

12 

13 
(*** Monotone operators ***) 

14 

15 
val prems = goalw Fixedpt.thy [bnd_mono_def] 

16 
"[ h(D)<=D; \ 

17 
\ !!W X. [ W<=D; X<=D; W<=X ] ==> h(W) <= h(X) \ 

18 
\ ] ==> bnd_mono(D,h)"; 

19 
by (REPEAT (ares_tac (prems@[conjI,allI,impI]) 1 

20 
ORELSE etac subset_trans 1)); 

760  21 
qed "bnd_monoI"; 
0  22 

23 
val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D"; 

24 
by (rtac (major RS conjunct1) 1); 

760  25 
qed "bnd_monoD1"; 
0  26 

27 
val major::prems = goalw Fixedpt.thy [bnd_mono_def] 

28 
"[ bnd_mono(D,h); W<=X; X<=D ] ==> h(W) <= h(X)"; 

29 
by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1); 

30 
by (REPEAT (resolve_tac prems 1)); 

760  31 
qed "bnd_monoD2"; 
0  32 

33 
val [major,minor] = goal Fixedpt.thy 

34 
"[ bnd_mono(D,h); X<=D ] ==> h(X) <= D"; 

35 
by (rtac (major RS bnd_monoD2 RS subset_trans) 1); 

36 
by (rtac (major RS bnd_monoD1) 3); 

37 
by (rtac minor 1); 

38 
by (rtac subset_refl 1); 

760  39 
qed "bnd_mono_subset"; 
0  40 

41 
goal Fixedpt.thy "!!A B. [ bnd_mono(D,h); A <= D; B <= D ] ==> \ 

42 
\ h(A) Un h(B) <= h(A Un B)"; 

43 
by (REPEAT (ares_tac [Un_upper1, Un_upper2, Un_least] 1 

44 
ORELSE etac bnd_monoD2 1)); 

760  45 
qed "bnd_mono_Un"; 
0  46 

47 
(*Useful??*) 

48 
goal Fixedpt.thy "!!A B. [ bnd_mono(D,h); A <= D; B <= D ] ==> \ 

49 
\ h(A Int B) <= h(A) Int h(B)"; 

50 
by (REPEAT (ares_tac [Int_lower1, Int_lower2, Int_greatest] 1 

51 
ORELSE etac bnd_monoD2 1)); 

760  52 
qed "bnd_mono_Int"; 
0  53 

54 
(**** Proof of KnasterTarski Theorem for the lfp ****) 

55 

56 
(*lfp is contained in each prefixedpoint*) 

744  57 
goalw Fixedpt.thy [lfp_def] 
58 
"!!A. [ h(A) <= A; A<=D ] ==> lfp(D,h) <= A"; 

59 
by (fast_tac ZF_cs 1); 

60 
(*or by (rtac (PowI RS CollectI RS Inter_lower) 1); *) 

760  61 
qed "lfp_lowerbound"; 
0  62 

63 
(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) 

64 
goalw Fixedpt.thy [lfp_def,Inter_def] "lfp(D,h) <= D"; 

65 
by (fast_tac ZF_cs 1); 

760  66 
qed "lfp_subset"; 
0  67 

68 
(*Used in datatype package*) 

69 
val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D"; 

70 
by (rewtac rew); 

71 
by (rtac lfp_subset 1); 

760  72 
qed "def_lfp_subset"; 
0  73 

74 
val prems = goalw Fixedpt.thy [lfp_def] 

75 
"[ h(D) <= D; !!X. [ h(X) <= X; X<=D ] ==> A<=X ] ==> \ 

76 
\ A <= lfp(D,h)"; 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

77 
by (rtac (Pow_top RS CollectI RS Inter_greatest) 1); 
0  78 
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1)); 
760  79 
qed "lfp_greatest"; 
0  80 

81 
val hmono::prems = goal Fixedpt.thy 

82 
"[ bnd_mono(D,h); h(A)<=A; A<=D ] ==> h(lfp(D,h)) <= A"; 

83 
by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1); 

84 
by (rtac lfp_lowerbound 1); 

85 
by (REPEAT (resolve_tac prems 1)); 

760  86 
qed "lfp_lemma1"; 
0  87 

88 
val [hmono] = goal Fixedpt.thy 

89 
"bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)"; 

90 
by (rtac (bnd_monoD1 RS lfp_greatest) 1); 

91 
by (rtac lfp_lemma1 2); 

92 
by (REPEAT (ares_tac [hmono] 1)); 

760  93 
qed "lfp_lemma2"; 
0  94 

95 
val [hmono] = goal Fixedpt.thy 

96 
"bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))"; 

97 
by (rtac lfp_lowerbound 1); 

98 
by (rtac (hmono RS bnd_monoD2) 1); 

99 
by (rtac (hmono RS lfp_lemma2) 1); 

100 
by (rtac (hmono RS bnd_mono_subset) 2); 

101 
by (REPEAT (rtac lfp_subset 1)); 

760  102 
qed "lfp_lemma3"; 
0  103 

104 
val prems = goal Fixedpt.thy 

105 
"bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"; 

106 
by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1)); 

760  107 
qed "lfp_Tarski"; 
0  108 

109 
(*Definition form, to control unfolding*) 

110 
val [rew,mono] = goal Fixedpt.thy 

111 
"[ A==lfp(D,h); bnd_mono(D,h) ] ==> A = h(A)"; 

112 
by (rewtac rew); 

113 
by (rtac (mono RS lfp_Tarski) 1); 

760  114 
qed "def_lfp_Tarski"; 
0  115 

116 
(*** General induction rule for least fixedpoints ***) 

117 

118 
val [hmono,indstep] = goal Fixedpt.thy 

119 
"[ bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ 

120 
\ ] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)"; 

121 
by (rtac subsetI 1); 

122 
by (rtac CollectI 1); 

123 
by (etac indstep 2); 

124 
by (rtac (hmono RS lfp_lemma2 RS subsetD) 1); 

125 
by (rtac (hmono RS bnd_monoD2 RS subsetD) 1); 

126 
by (REPEAT (ares_tac [Collect_subset, lfp_subset] 1)); 

760  127 
qed "Collect_is_pre_fixedpt"; 
0  128 

129 
(*This rule yields an induction hypothesis in which the components of a 

130 
data structure may be assumed to be elements of lfp(D,h)*) 

131 
val prems = goal Fixedpt.thy 

1461  132 
"[ bnd_mono(D,h); a : lfp(D,h); \ 
133 
\ !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ 

0  134 
\ ] ==> P(a)"; 
135 
by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1); 

136 
by (rtac (lfp_subset RS (Collect_subset RS subset_trans)) 3); 

137 
by (REPEAT (ares_tac prems 1)); 

760  138 
qed "induct"; 
0  139 

140 
(*Definition form, to control unfolding*) 

141 
val rew::prems = goal Fixedpt.thy 

142 
"[ A == lfp(D,h); bnd_mono(D,h); a:A; \ 

143 
\ !!x. x : h(Collect(A,P)) ==> P(x) \ 

144 
\ ] ==> P(a)"; 

145 
by (rtac induct 1); 

146 
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); 

760  147 
qed "def_induct"; 
0  148 

149 
(*This version is useful when "A" is not a subset of D; 

150 
second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *) 

151 
val [hsub,hmono] = goal Fixedpt.thy 

152 
"[ h(D Int A) <= A; bnd_mono(D,h) ] ==> lfp(D,h) <= A"; 

153 
by (rtac (lfp_lowerbound RS subset_trans) 1); 

154 
by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1); 

155 
by (REPEAT (resolve_tac [hsub,Int_lower1,Int_lower2] 1)); 

760  156 
qed "lfp_Int_lowerbound"; 
0  157 

158 
(*Monotonicity of lfp, where h precedes i under a domainlike partial order 

159 
monotonicity of h is not strictly necessary; h must be bounded by D*) 

160 
val [hmono,imono,subhi] = goal Fixedpt.thy 

1461  161 
"[ bnd_mono(D,h); bnd_mono(E,i); \ 
0  162 
\ !!X. X<=D ==> h(X) <= i(X) ] ==> lfp(D,h) <= lfp(E,i)"; 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

163 
by (rtac (bnd_monoD1 RS lfp_greatest) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

164 
by (rtac imono 1); 
0  165 
by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1); 
166 
by (rtac (Int_lower1 RS subhi RS subset_trans) 1); 

167 
by (rtac (imono RS bnd_monoD2 RS subset_trans) 1); 

168 
by (REPEAT (ares_tac [Int_lower2] 1)); 

760  169 
qed "lfp_mono"; 
0  170 

171 
(*This (unused) version illustrates that monotonicity is not really needed, 

172 
but both lfp's must be over the SAME set D; Inter is antimonotonic!*) 

173 
val [isubD,subhi] = goal Fixedpt.thy 

174 
"[ i(D) <= D; !!X. X<=D ==> h(X) <= i(X) ] ==> lfp(D,h) <= lfp(D,i)"; 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

175 
by (rtac lfp_greatest 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

176 
by (rtac isubD 1); 
0  177 
by (rtac lfp_lowerbound 1); 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

178 
by (etac (subhi RS subset_trans) 1); 
0  179 
by (REPEAT (assume_tac 1)); 
760  180 
qed "lfp_mono2"; 
0  181 

182 

183 
(**** Proof of KnasterTarski Theorem for the gfp ****) 

184 

185 
(*gfp contains each postfixedpoint that is contained in D*) 

186 
val prems = goalw Fixedpt.thy [gfp_def] 

187 
"[ A <= h(A); A<=D ] ==> A <= gfp(D,h)"; 

188 
by (rtac (PowI RS CollectI RS Union_upper) 1); 

189 
by (REPEAT (resolve_tac prems 1)); 

760  190 
qed "gfp_upperbound"; 
0  191 

192 
goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D"; 

193 
by (fast_tac ZF_cs 1); 

760  194 
qed "gfp_subset"; 
0  195 

196 
(*Used in datatype package*) 

197 
val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D"; 

198 
by (rewtac rew); 

199 
by (rtac gfp_subset 1); 

760  200 
qed "def_gfp_subset"; 
0  201 

202 
val hmono::prems = goalw Fixedpt.thy [gfp_def] 

203 
"[ bnd_mono(D,h); !!X. [ X <= h(X); X<=D ] ==> X<=A ] ==> \ 

204 
\ gfp(D,h) <= A"; 

205 
by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1); 

760  206 
qed "gfp_least"; 
0  207 

208 
val hmono::prems = goal Fixedpt.thy 

209 
"[ bnd_mono(D,h); A<=h(A); A<=D ] ==> A <= h(gfp(D,h))"; 

210 
by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1); 

211 
by (rtac gfp_subset 3); 

212 
by (rtac gfp_upperbound 2); 

213 
by (REPEAT (resolve_tac prems 1)); 

760  214 
qed "gfp_lemma1"; 
0  215 

216 
val [hmono] = goal Fixedpt.thy 

217 
"bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))"; 

218 
by (rtac gfp_least 1); 

219 
by (rtac gfp_lemma1 2); 

220 
by (REPEAT (ares_tac [hmono] 1)); 

760  221 
qed "gfp_lemma2"; 
0  222 

223 
val [hmono] = goal Fixedpt.thy 

224 
"bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)"; 

225 
by (rtac gfp_upperbound 1); 

226 
by (rtac (hmono RS bnd_monoD2) 1); 

227 
by (rtac (hmono RS gfp_lemma2) 1); 

228 
by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1)); 

760  229 
qed "gfp_lemma3"; 
0  230 

231 
val prems = goal Fixedpt.thy 

232 
"bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"; 

233 
by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1)); 

760  234 
qed "gfp_Tarski"; 
0  235 

236 
(*Definition form, to control unfolding*) 

237 
val [rew,mono] = goal Fixedpt.thy 

238 
"[ A==gfp(D,h); bnd_mono(D,h) ] ==> A = h(A)"; 

239 
by (rewtac rew); 

240 
by (rtac (mono RS gfp_Tarski) 1); 

760  241 
qed "def_gfp_Tarski"; 
0  242 

243 

244 
(*** Coinduction rules for greatest fixed points ***) 

245 

246 
(*weak version*) 

247 
goal Fixedpt.thy "!!X h. [ a: X; X <= h(X); X <= D ] ==> a : gfp(D,h)"; 

248 
by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1)); 

760  249 
qed "weak_coinduct"; 
0  250 

251 
val [subs_h,subs_D,mono] = goal Fixedpt.thy 

252 
"[ X <= h(X Un gfp(D,h)); X <= D; bnd_mono(D,h) ] ==> \ 

253 
\ X Un gfp(D,h) <= h(X Un gfp(D,h))"; 

254 
by (rtac (subs_h RS Un_least) 1); 

255 
by (rtac (mono RS gfp_lemma2 RS subset_trans) 1); 

256 
by (rtac (Un_upper2 RS subset_trans) 1); 

257 
by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1); 

760  258 
qed "coinduct_lemma"; 
0  259 

260 
(*strong version*) 

261 
goal Fixedpt.thy 

262 
"!!X D. [ bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D ] ==> \ 

263 
\ a : gfp(D,h)"; 

647
fb7345cccddc
ZF/Fixedpt/coinduct: modified proof to suppress deep unification
lcp
parents:
484
diff
changeset

264 
by (rtac weak_coinduct 1); 
fb7345cccddc
ZF/Fixedpt/coinduct: modified proof to suppress deep unification
lcp
parents:
484
diff
changeset

265 
by (etac coinduct_lemma 2); 
0  266 
by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1)); 
760  267 
qed "coinduct"; 
0  268 

269 
(*Definition form, to control unfolding*) 

270 
val rew::prems = goal Fixedpt.thy 

271 
"[ A == gfp(D,h); bnd_mono(D,h); a: X; X <= h(X Un A); X <= D ] ==> \ 

272 
\ a : A"; 

273 
by (rewtac rew); 

274 
by (rtac coinduct 1); 

275 
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); 

760  276 
qed "def_coinduct"; 
0  277 

278 
(*Lemma used immediately below!*) 

279 
val [subsA,XimpP] = goal ZF.thy 

280 
"[ X <= A; !!z. z:X ==> P(z) ] ==> X <= Collect(A,P)"; 

281 
by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1); 

282 
by (assume_tac 1); 

283 
by (etac XimpP 1); 

760  284 
qed "subset_Collect"; 
0  285 

286 
(*The version used in the induction/coinduction package*) 

287 
val prems = goal Fixedpt.thy 

288 
"[ A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); \ 

289 
\ a: X; X <= D; !!z. z: X ==> P(X Un A, z) ] ==> \ 

290 
\ a : A"; 

291 
by (rtac def_coinduct 1); 

292 
by (REPEAT (ares_tac (subset_Collect::prems) 1)); 

760  293 
qed "def_Collect_coinduct"; 
0  294 

295 
(*Monotonicity of gfp!*) 

296 
val [hmono,subde,subhi] = goal Fixedpt.thy 

1461  297 
"[ bnd_mono(D,h); D <= E; \ 
0  298 
\ !!X. X<=D ==> h(X) <= i(X) ] ==> gfp(D,h) <= gfp(E,i)"; 
299 
by (rtac gfp_upperbound 1); 

300 
by (rtac (hmono RS gfp_lemma2 RS subset_trans) 1); 

301 
by (rtac (gfp_subset RS subhi) 1); 

302 
by (rtac ([gfp_subset, subde] MRS subset_trans) 1); 

760  303 
qed "gfp_mono"; 
0  304 