0

1 
(* Title: ZF/fixedpt.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


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));


21 
val bnd_monoI = result();


22 


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


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


25 
val bnd_monoD1 = result();


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));


31 
val bnd_monoD2 = result();


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);


39 
val bnd_mono_subset = result();


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));


45 
val bnd_mono_Un = result();


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));


52 
val bnd_mono_Int = result();


53 


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


55 


56 
(*lfp is contained in each prefixedpoint*)


57 
val prems = goalw Fixedpt.thy [lfp_def]


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


59 
by (rtac (PowI RS CollectI RS Inter_lower) 1);


60 
by (REPEAT (resolve_tac prems 1));


61 
val lfp_lowerbound = result();


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);


66 
val lfp_subset = result();


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);


72 
val def_lfp_subset = result();


73 


74 
val subset0_cs = FOL_cs


75 
addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]


76 
addIs [bexI, UnionI, ReplaceI, RepFunI]


77 
addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE,


78 
CollectE, emptyE]


79 
addEs [rev_ballE, InterD, make_elim InterD, subsetD];


80 


81 
val subset_cs = subset0_cs


82 
addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,


83 
Inter_greatest,Int_greatest,RepFun_subset]


84 
addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]


85 
addIs [Union_upper,Inter_lower]


86 
addSEs [cons_subsetE];


87 


88 
val prems = goalw Fixedpt.thy [lfp_def]


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


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


91 
br (Pow_top RS CollectI RS Inter_greatest) 1;


92 
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));


93 
val lfp_greatest = result();


94 


95 
val hmono::prems = goal Fixedpt.thy


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


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


98 
by (rtac lfp_lowerbound 1);


99 
by (REPEAT (resolve_tac prems 1));


100 
val lfp_lemma1 = result();


101 


102 
val [hmono] = goal Fixedpt.thy


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


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


105 
by (rtac lfp_lemma1 2);


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


107 
val lfp_lemma2 = result();


108 


109 
val [hmono] = goal Fixedpt.thy


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


111 
by (rtac lfp_lowerbound 1);


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


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


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


115 
by (REPEAT (rtac lfp_subset 1));


116 
val lfp_lemma3 = result();


117 


118 
val prems = goal Fixedpt.thy


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


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


121 
val lfp_Tarski = result();


122 


123 
(*Definition form, to control unfolding*)


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


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


126 
by (rewtac rew);


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


128 
val def_lfp_Tarski = result();


129 


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


131 


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


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


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


135 
by (rtac subsetI 1);


136 
by (rtac CollectI 1);


137 
by (etac indstep 2);


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


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


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


141 
val Collect_is_pre_fixedpt = result();


142 


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


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


145 
val prems = goal Fixedpt.thy


146 
"[ bnd_mono(D,h); a : lfp(D,h); \


147 
\ !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \


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


149 
by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1);


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


151 
by (REPEAT (ares_tac prems 1));


152 
val induct = result();


153 


154 
(*Definition form, to control unfolding*)


155 
val rew::prems = goal Fixedpt.thy


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


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


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


159 
by (rtac induct 1);


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


161 
val def_induct = result();


162 


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


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


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


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


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


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


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


170 
val lfp_Int_lowerbound = result();


171 


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


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


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


175 
"[ bnd_mono(D,h); bnd_mono(E,i); \


176 
\ !!X. X<=D ==> h(X) <= i(X) ] ==> lfp(D,h) <= lfp(E,i)";


177 
br (bnd_monoD1 RS lfp_greatest) 1;


178 
br imono 1;


179 
by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);


180 
by (rtac (Int_lower1 RS subhi RS subset_trans) 1);


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


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


183 
val lfp_mono = result();


184 


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


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


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


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


189 
br lfp_greatest 1;


190 
br isubD 1;


191 
by (rtac lfp_lowerbound 1);


192 
be (subhi RS subset_trans) 1;


193 
by (REPEAT (assume_tac 1));


194 
val lfp_mono2 = result();


195 


196 


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


198 


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


200 
val prems = goalw Fixedpt.thy [gfp_def]


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


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


203 
by (REPEAT (resolve_tac prems 1));


204 
val gfp_upperbound = result();


205 


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


207 
by (fast_tac ZF_cs 1);


208 
val gfp_subset = result();


209 


210 
(*Used in datatype package*)


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


212 
by (rewtac rew);


213 
by (rtac gfp_subset 1);


214 
val def_gfp_subset = result();


215 


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


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


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


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


220 
val gfp_least = result();


221 


222 
val hmono::prems = goal Fixedpt.thy


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


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


225 
by (rtac gfp_subset 3);


226 
by (rtac gfp_upperbound 2);


227 
by (REPEAT (resolve_tac prems 1));


228 
val gfp_lemma1 = result();


229 


230 
val [hmono] = goal Fixedpt.thy


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


232 
by (rtac gfp_least 1);


233 
by (rtac gfp_lemma1 2);


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


235 
val gfp_lemma2 = result();


236 


237 
val [hmono] = goal Fixedpt.thy


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


239 
by (rtac gfp_upperbound 1);


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


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


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


243 
val gfp_lemma3 = result();


244 


245 
val prems = goal Fixedpt.thy


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


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


248 
val gfp_Tarski = result();


249 


250 
(*Definition form, to control unfolding*)


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


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


253 
by (rewtac rew);


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


255 
val def_gfp_Tarski = result();


256 


257 


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


259 


260 
(*weak version*)


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


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


263 
val weak_coinduct = result();


264 


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


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


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


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


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


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


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


272 
val coinduct_lemma = result();


273 


274 
(*strong version*)


275 
goal Fixedpt.thy


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


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


278 
by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);


279 
by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1));


280 
val coinduct = result();


281 


282 
(*Definition form, to control unfolding*)


283 
val rew::prems = goal Fixedpt.thy


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


285 
\ a : A";


286 
by (rewtac rew);


287 
by (rtac coinduct 1);


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


289 
val def_coinduct = result();


290 


291 
(*Lemma used immediately below!*)


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


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


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


295 
by (assume_tac 1);


296 
by (etac XimpP 1);


297 
val subset_Collect = result();


298 


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


300 
val prems = goal Fixedpt.thy


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


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


303 
\ a : A";


304 
by (rtac def_coinduct 1);


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


306 
val def_Collect_coinduct = result();


307 


308 
(*Monotonicity of gfp!*)


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


310 
"[ bnd_mono(D,h); D <= E; \


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


312 
by (rtac gfp_upperbound 1);


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


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


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


316 
val gfp_mono = result();


317 
