35762

1 
(* Title: ZF/Fixedpt.thy

1478

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

3 
Copyright 1992 University of Cambridge


4 
*)


5 

13356

6 
header{*Least and Greatest Fixed Points; the KnasterTarski Theorem*}


7 

16417

8 
theory Fixedpt imports equalities begin

13218

9 

24893

10 
definition

13218

11 
(*monotone operator from Pow(D) to itself*)

24893

12 
bnd_mono :: "[i,i=>i]=>o" where

46820

13 
"bnd_mono(D,h) == h(D)<=D & (\<forall>W X. W<=X \<longrightarrow> X<=D \<longrightarrow> h(W) \<subseteq> h(X))"

13218

14 

24893

15 
definition


16 
lfp :: "[i,i=>i]=>i" where

46820

17 
"lfp(D,h) == \<Inter>({X: Pow(D). h(X) \<subseteq> X})"

13218

18 

24893

19 
definition


20 
gfp :: "[i,i=>i]=>i" where

46820

21 
"gfp(D,h) == \<Union>({X: Pow(D). X \<subseteq> h(X)})"

13218

22 

14046

23 
text{*The theorem is proved in the lattice of subsets of @{term D},


24 
namely @{term "Pow(D)"}, with Inter as the greatest lower bound.*}

13218

25 

13356

26 
subsection{*Monotone Operators*}

13218

27 


28 
lemma bnd_monoI:


29 
"[ h(D)<=D;

46820

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

13218

31 
] ==> bnd_mono(D,h)"


32 
by (unfold bnd_mono_def, clarify, blast)


33 

46820

34 
lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) \<subseteq> D"

13218

35 
apply (unfold bnd_mono_def)


36 
apply (erule conjunct1)


37 
done


38 

46820

39 
lemma bnd_monoD2: "[ bnd_mono(D,h); W<=X; X<=D ] ==> h(W) \<subseteq> h(X)"

13218

40 
by (unfold bnd_mono_def, blast)


41 


42 
lemma bnd_mono_subset:

46820

43 
"[ bnd_mono(D,h); X<=D ] ==> h(X) \<subseteq> D"

13218

44 
by (unfold bnd_mono_def, clarify, blast)


45 


46 
lemma bnd_mono_Un:

46820

47 
"[ bnd_mono(D,h); A \<subseteq> D; B \<subseteq> D ] ==> h(A) \<union> h(B) \<subseteq> h(A \<union> B)"

13218

48 
apply (unfold bnd_mono_def)


49 
apply (rule Un_least, blast+)


50 
done


51 

13220

52 
(*unused*)


53 
lemma bnd_mono_UN:

46820

54 
"[ bnd_mono(D,h); \<forall>i\<in>I. A(i) \<subseteq> D ]


55 
==> (\<Union>i\<in>I. h(A(i))) \<subseteq> h((\<Union>i\<in>I. A(i)))"

13220

56 
apply (unfold bnd_mono_def)


57 
apply (rule UN_least)


58 
apply (elim conjE)


59 
apply (drule_tac x="A(i)" in spec)


60 
apply (drule_tac x="(\<Union>i\<in>I. A(i))" in spec)


61 
apply blast


62 
done


63 

13218

64 
(*Useful??*)


65 
lemma bnd_mono_Int:

46820

66 
"[ bnd_mono(D,h); A \<subseteq> D; B \<subseteq> D ] ==> h(A \<inter> B) \<subseteq> h(A) \<inter> h(B)"

13218

67 
apply (rule Int_greatest)


68 
apply (erule bnd_monoD2, rule Int_lower1, assumption)


69 
apply (erule bnd_monoD2, rule Int_lower2, assumption)


70 
done


71 

14046

72 
subsection{*Proof of KnasterTarski Theorem using @{term lfp}*}

13218

73 


74 
(*lfp is contained in each prefixedpoint*)


75 
lemma lfp_lowerbound:

46820

76 
"[ h(A) \<subseteq> A; A<=D ] ==> lfp(D,h) \<subseteq> A"

13218

77 
by (unfold lfp_def, blast)


78 


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

46820

80 
lemma lfp_subset: "lfp(D,h) \<subseteq> D"

13218

81 
by (unfold lfp_def Inter_def, blast)


82 


83 
(*Used in datatype package*)

46820

84 
lemma def_lfp_subset: "A == lfp(D,h) ==> A \<subseteq> D"

13218

85 
apply simp


86 
apply (rule lfp_subset)


87 
done


88 


89 
lemma lfp_greatest:

46820

90 
"[ h(D) \<subseteq> D; !!X. [ h(X) \<subseteq> X; X<=D ] ==> A<=X ] ==> A \<subseteq> lfp(D,h)"

13218

91 
by (unfold lfp_def, blast)


92 


93 
lemma lfp_lemma1:

46820

94 
"[ bnd_mono(D,h); h(A)<=A; A<=D ] ==> h(lfp(D,h)) \<subseteq> A"

13218

95 
apply (erule bnd_monoD2 [THEN subset_trans])


96 
apply (rule lfp_lowerbound, assumption+)


97 
done

3923

98 

46820

99 
lemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) \<subseteq> lfp(D,h)"

13218

100 
apply (rule bnd_monoD1 [THEN lfp_greatest])


101 
apply (rule_tac [2] lfp_lemma1)


102 
apply (assumption+)


103 
done


104 


105 
lemma lfp_lemma3:

46820

106 
"bnd_mono(D,h) ==> lfp(D,h) \<subseteq> h(lfp(D,h))"

13218

107 
apply (rule lfp_lowerbound)


108 
apply (rule bnd_monoD2, assumption)


109 
apply (rule lfp_lemma2, assumption)


110 
apply (erule_tac [2] bnd_mono_subset)


111 
apply (rule lfp_subset)+


112 
done


113 


114 
lemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"


115 
apply (rule equalityI)


116 
apply (erule lfp_lemma3)


117 
apply (erule lfp_lemma2)


118 
done


119 


120 
(*Definition form, to control unfolding*)


121 
lemma def_lfp_unfold:


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


123 
apply simp


124 
apply (erule lfp_unfold)


125 
done


126 

13356

127 
subsection{*General Induction Rule for Least Fixedpoints*}

13218

128 


129 
lemma Collect_is_pre_fixedpt:

46820

130 
"[ bnd_mono(D,h); !!x. x \<in> h(Collect(lfp(D,h),P)) ==> P(x) ]


131 
==> h(Collect(lfp(D,h),P)) \<subseteq> Collect(lfp(D,h),P)"

13218

132 
by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD]


133 
lfp_subset [THEN subsetD])


134 


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


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


137 
lemma induct:

46820

138 
"[ bnd_mono(D,h); a \<in> lfp(D,h);


139 
!!x. x \<in> h(Collect(lfp(D,h),P)) ==> P(x)

13218

140 
] ==> P(a)"


141 
apply (rule Collect_is_pre_fixedpt


142 
[THEN lfp_lowerbound, THEN subsetD, THEN CollectD2])


143 
apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]],


144 
blast+)


145 
done


146 


147 
(*Definition form, to control unfolding*)


148 
lemma def_induct:


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

46820

150 
!!x. x \<in> h(Collect(A,P)) ==> P(x)

13218

151 
] ==> P(a)"


152 
by (rule induct, blast+)


153 


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

46820

155 
second premise could simply be h(D \<inter> A) \<subseteq> D or !!X. X<=D ==> h(X)<=D *)

13218

156 
lemma lfp_Int_lowerbound:

46820

157 
"[ h(D \<inter> A) \<subseteq> A; bnd_mono(D,h) ] ==> lfp(D,h) \<subseteq> A"

13218

158 
apply (rule lfp_lowerbound [THEN subset_trans])


159 
apply (erule bnd_mono_subset [THEN Int_greatest], blast+)


160 
done


161 


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


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


164 
lemma lfp_mono:


165 
assumes hmono: "bnd_mono(D,h)"


166 
and imono: "bnd_mono(E,i)"

46820

167 
and subhi: "!!X. X<=D ==> h(X) \<subseteq> i(X)"


168 
shows "lfp(D,h) \<subseteq> lfp(E,i)"

13218

169 
apply (rule bnd_monoD1 [THEN lfp_greatest])


170 
apply (rule imono)


171 
apply (rule hmono [THEN [2] lfp_Int_lowerbound])


172 
apply (rule Int_lower1 [THEN subhi, THEN subset_trans])


173 
apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto)


174 
done

0

175 

13218

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


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


178 
lemma lfp_mono2:

46820

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

13218

180 
apply (rule lfp_greatest, assumption)


181 
apply (rule lfp_lowerbound, blast, assumption)


182 
done


183 

14046

184 
lemma lfp_cong:

46820

185 
"[D=D'; !!X. X \<subseteq> D' ==> h(X) = h'(X)] ==> lfp(D,h) = lfp(D',h')"

14046

186 
apply (simp add: lfp_def)


187 
apply (rule_tac t=Inter in subst_context)


188 
apply (rule Collect_cong, simp_all)


189 
done

13218

190 

14046

191 


192 
subsection{*Proof of KnasterTarski Theorem using @{term gfp}*}

13218

193 


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

46820

195 
lemma gfp_upperbound: "[ A \<subseteq> h(A); A<=D ] ==> A \<subseteq> gfp(D,h)"

13218

196 
apply (unfold gfp_def)


197 
apply (rule PowI [THEN CollectI, THEN Union_upper])


198 
apply (assumption+)


199 
done


200 

46820

201 
lemma gfp_subset: "gfp(D,h) \<subseteq> D"

13218

202 
by (unfold gfp_def, blast)


203 


204 
(*Used in datatype package*)

46820

205 
lemma def_gfp_subset: "A==gfp(D,h) ==> A \<subseteq> D"

13218

206 
apply simp


207 
apply (rule gfp_subset)


208 
done


209 


210 
lemma gfp_least:

46820

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


212 
gfp(D,h) \<subseteq> A"

13218

213 
apply (unfold gfp_def)


214 
apply (blast dest: bnd_monoD1)


215 
done


216 


217 
lemma gfp_lemma1:

46820

218 
"[ bnd_mono(D,h); A<=h(A); A<=D ] ==> A \<subseteq> h(gfp(D,h))"

13218

219 
apply (rule subset_trans, assumption)


220 
apply (erule bnd_monoD2)


221 
apply (rule_tac [2] gfp_subset)


222 
apply (simp add: gfp_upperbound)


223 
done


224 

46820

225 
lemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) \<subseteq> h(gfp(D,h))"

13218

226 
apply (rule gfp_least)


227 
apply (rule_tac [2] gfp_lemma1)


228 
apply (assumption+)


229 
done


230 


231 
lemma gfp_lemma3:

46820

232 
"bnd_mono(D,h) ==> h(gfp(D,h)) \<subseteq> gfp(D,h)"

13218

233 
apply (rule gfp_upperbound)


234 
apply (rule bnd_monoD2, assumption)


235 
apply (rule gfp_lemma2, assumption)


236 
apply (erule bnd_mono_subset, rule gfp_subset)+


237 
done


238 


239 
lemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"


240 
apply (rule equalityI)


241 
apply (erule gfp_lemma2)


242 
apply (erule gfp_lemma3)


243 
done


244 


245 
(*Definition form, to control unfolding*)


246 
lemma def_gfp_unfold:


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


248 
apply simp


249 
apply (erule gfp_unfold)


250 
done


251 


252 

13356

253 
subsection{*Coinduction Rules for Greatest Fixed Points*}

13218

254 


255 
(*weak version*)

46820

256 
lemma weak_coinduct: "[ a: X; X \<subseteq> h(X); X \<subseteq> D ] ==> a \<in> gfp(D,h)"

13218

257 
by (blast intro: gfp_upperbound [THEN subsetD])

0

258 

13218

259 
lemma coinduct_lemma:

46820

260 
"[ X \<subseteq> h(X \<union> gfp(D,h)); X \<subseteq> D; bnd_mono(D,h) ] ==>


261 
X \<union> gfp(D,h) \<subseteq> h(X \<union> gfp(D,h))"

13218

262 
apply (erule Un_least)


263 
apply (rule gfp_lemma2 [THEN subset_trans], assumption)


264 
apply (rule Un_upper2 [THEN subset_trans])


265 
apply (rule bnd_mono_Un, assumption+)


266 
apply (rule gfp_subset)


267 
done


268 


269 
(*strong version*)


270 
lemma coinduct:

46820

271 
"[ bnd_mono(D,h); a: X; X \<subseteq> h(X \<union> gfp(D,h)); X \<subseteq> D ]


272 
==> a \<in> gfp(D,h)"

13218

273 
apply (rule weak_coinduct)


274 
apply (erule_tac [2] coinduct_lemma)


275 
apply (simp_all add: gfp_subset Un_subset_iff)


276 
done


277 


278 
(*Definition form, to control unfolding*)


279 
lemma def_coinduct:

46820

280 
"[ A == gfp(D,h); bnd_mono(D,h); a: X; X \<subseteq> h(X \<union> A); X \<subseteq> D ] ==>


281 
a \<in> A"

13218

282 
apply simp


283 
apply (rule coinduct, assumption+)


284 
done


285 


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


287 
lemma def_Collect_coinduct:


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

46820

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


290 
a \<in> A"

13218

291 
apply (rule def_coinduct, assumption+, blast+)


292 
done

0

293 

13218

294 
(*Monotonicity of gfp!*)


295 
lemma gfp_mono:

46820

296 
"[ bnd_mono(D,h); D \<subseteq> E;


297 
!!X. X<=D ==> h(X) \<subseteq> i(X) ] ==> gfp(D,h) \<subseteq> gfp(E,i)"

13218

298 
apply (rule gfp_upperbound)


299 
apply (rule gfp_lemma2 [THEN subset_trans], assumption)


300 
apply (blast del: subsetI intro: gfp_subset)


301 
apply (blast del: subsetI intro: subset_trans gfp_subset)


302 
done


303 

0

304 
end
