src/ZF/Fixedpt.thy
 author wenzelm Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago) changeset 49566 66cbf8bb4693 parent 46820 c656222c4dc1 child 58871 c399ae4b836f permissions -rw-r--r--
basic integration of graphview into document model;
 wenzelm@35762 ` 1` ```(* Title: ZF/Fixedpt.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 3` ``` Copyright 1992 University of Cambridge ``` clasohm@0 ` 4` ```*) ``` clasohm@0 ` 5` paulson@13356 ` 6` ```header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*} ``` paulson@13356 ` 7` haftmann@16417 ` 8` ```theory Fixedpt imports equalities begin ``` paulson@13218 ` 9` wenzelm@24893 ` 10` ```definition ``` paulson@13218 ` 11` ``` (*monotone operator from Pow(D) to itself*) ``` wenzelm@24893 ` 12` ``` bnd_mono :: "[i,i=>i]=>o" where ``` paulson@46820 ` 13` ``` "bnd_mono(D,h) == h(D)<=D & (\W X. W<=X \ X<=D \ h(W) \ h(X))" ``` paulson@13218 ` 14` wenzelm@24893 ` 15` ```definition ``` wenzelm@24893 ` 16` ``` lfp :: "[i,i=>i]=>i" where ``` paulson@46820 ` 17` ``` "lfp(D,h) == \({X: Pow(D). h(X) \ X})" ``` paulson@13218 ` 18` wenzelm@24893 ` 19` ```definition ``` wenzelm@24893 ` 20` ``` gfp :: "[i,i=>i]=>i" where ``` paulson@46820 ` 21` ``` "gfp(D,h) == \({X: Pow(D). X \ h(X)})" ``` paulson@13218 ` 22` paulson@14046 ` 23` ```text{*The theorem is proved in the lattice of subsets of @{term D}, ``` paulson@14046 ` 24` ``` namely @{term "Pow(D)"}, with Inter as the greatest lower bound.*} ``` paulson@13218 ` 25` paulson@13356 ` 26` ```subsection{*Monotone Operators*} ``` paulson@13218 ` 27` paulson@13218 ` 28` ```lemma bnd_monoI: ``` paulson@13218 ` 29` ``` "[| h(D)<=D; ``` paulson@46820 ` 30` ``` !!W X. [| W<=D; X<=D; W<=X |] ==> h(W) \ h(X) ``` paulson@13218 ` 31` ``` |] ==> bnd_mono(D,h)" ``` paulson@13218 ` 32` ```by (unfold bnd_mono_def, clarify, blast) ``` paulson@13218 ` 33` paulson@46820 ` 34` ```lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) \ D" ``` paulson@13218 ` 35` ```apply (unfold bnd_mono_def) ``` paulson@13218 ` 36` ```apply (erule conjunct1) ``` paulson@13218 ` 37` ```done ``` paulson@13218 ` 38` paulson@46820 ` 39` ```lemma bnd_monoD2: "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) \ h(X)" ``` paulson@13218 ` 40` ```by (unfold bnd_mono_def, blast) ``` paulson@13218 ` 41` paulson@13218 ` 42` ```lemma bnd_mono_subset: ``` paulson@46820 ` 43` ``` "[| bnd_mono(D,h); X<=D |] ==> h(X) \ D" ``` paulson@13218 ` 44` ```by (unfold bnd_mono_def, clarify, blast) ``` paulson@13218 ` 45` paulson@13218 ` 46` ```lemma bnd_mono_Un: ``` paulson@46820 ` 47` ``` "[| bnd_mono(D,h); A \ D; B \ D |] ==> h(A) \ h(B) \ h(A \ B)" ``` paulson@13218 ` 48` ```apply (unfold bnd_mono_def) ``` paulson@13218 ` 49` ```apply (rule Un_least, blast+) ``` paulson@13218 ` 50` ```done ``` paulson@13218 ` 51` paulson@13220 ` 52` ```(*unused*) ``` paulson@13220 ` 53` ```lemma bnd_mono_UN: ``` paulson@46820 ` 54` ``` "[| bnd_mono(D,h); \i\I. A(i) \ D |] ``` paulson@46820 ` 55` ``` ==> (\i\I. h(A(i))) \ h((\i\I. A(i)))" ``` paulson@13220 ` 56` ```apply (unfold bnd_mono_def) ``` paulson@13220 ` 57` ```apply (rule UN_least) ``` paulson@13220 ` 58` ```apply (elim conjE) ``` paulson@13220 ` 59` ```apply (drule_tac x="A(i)" in spec) ``` paulson@13220 ` 60` ```apply (drule_tac x="(\i\I. A(i))" in spec) ``` paulson@13220 ` 61` ```apply blast ``` paulson@13220 ` 62` ```done ``` paulson@13220 ` 63` paulson@13218 ` 64` ```(*Useful??*) ``` paulson@13218 ` 65` ```lemma bnd_mono_Int: ``` paulson@46820 ` 66` ``` "[| bnd_mono(D,h); A \ D; B \ D |] ==> h(A \ B) \ h(A) \ h(B)" ``` paulson@13218 ` 67` ```apply (rule Int_greatest) ``` paulson@13218 ` 68` ```apply (erule bnd_monoD2, rule Int_lower1, assumption) ``` paulson@13218 ` 69` ```apply (erule bnd_monoD2, rule Int_lower2, assumption) ``` paulson@13218 ` 70` ```done ``` paulson@13218 ` 71` paulson@14046 ` 72` ```subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*} ``` paulson@13218 ` 73` paulson@13218 ` 74` ```(*lfp is contained in each pre-fixedpoint*) ``` paulson@13218 ` 75` ```lemma lfp_lowerbound: ``` paulson@46820 ` 76` ``` "[| h(A) \ A; A<=D |] ==> lfp(D,h) \ A" ``` paulson@13218 ` 77` ```by (unfold lfp_def, blast) ``` paulson@13218 ` 78` paulson@13218 ` 79` ```(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) ``` paulson@46820 ` 80` ```lemma lfp_subset: "lfp(D,h) \ D" ``` paulson@13218 ` 81` ```by (unfold lfp_def Inter_def, blast) ``` paulson@13218 ` 82` paulson@13218 ` 83` ```(*Used in datatype package*) ``` paulson@46820 ` 84` ```lemma def_lfp_subset: "A == lfp(D,h) ==> A \ D" ``` paulson@13218 ` 85` ```apply simp ``` paulson@13218 ` 86` ```apply (rule lfp_subset) ``` paulson@13218 ` 87` ```done ``` paulson@13218 ` 88` paulson@13218 ` 89` ```lemma lfp_greatest: ``` paulson@46820 ` 90` ``` "[| h(D) \ D; !!X. [| h(X) \ X; X<=D |] ==> A<=X |] ==> A \ lfp(D,h)" ``` paulson@13218 ` 91` ```by (unfold lfp_def, blast) ``` paulson@13218 ` 92` paulson@13218 ` 93` ```lemma lfp_lemma1: ``` paulson@46820 ` 94` ``` "[| bnd_mono(D,h); h(A)<=A; A<=D |] ==> h(lfp(D,h)) \ A" ``` paulson@13218 ` 95` ```apply (erule bnd_monoD2 [THEN subset_trans]) ``` paulson@13218 ` 96` ```apply (rule lfp_lowerbound, assumption+) ``` paulson@13218 ` 97` ```done ``` wenzelm@3923 ` 98` paulson@46820 ` 99` ```lemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) \ lfp(D,h)" ``` paulson@13218 ` 100` ```apply (rule bnd_monoD1 [THEN lfp_greatest]) ``` paulson@13218 ` 101` ```apply (rule_tac [2] lfp_lemma1) ``` paulson@13218 ` 102` ```apply (assumption+) ``` paulson@13218 ` 103` ```done ``` paulson@13218 ` 104` paulson@13218 ` 105` ```lemma lfp_lemma3: ``` paulson@46820 ` 106` ``` "bnd_mono(D,h) ==> lfp(D,h) \ h(lfp(D,h))" ``` paulson@13218 ` 107` ```apply (rule lfp_lowerbound) ``` paulson@13218 ` 108` ```apply (rule bnd_monoD2, assumption) ``` paulson@13218 ` 109` ```apply (rule lfp_lemma2, assumption) ``` paulson@13218 ` 110` ```apply (erule_tac [2] bnd_mono_subset) ``` paulson@13218 ` 111` ```apply (rule lfp_subset)+ ``` paulson@13218 ` 112` ```done ``` paulson@13218 ` 113` paulson@13218 ` 114` ```lemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))" ``` paulson@13218 ` 115` ```apply (rule equalityI) ``` paulson@13218 ` 116` ```apply (erule lfp_lemma3) ``` paulson@13218 ` 117` ```apply (erule lfp_lemma2) ``` paulson@13218 ` 118` ```done ``` paulson@13218 ` 119` paulson@13218 ` 120` ```(*Definition form, to control unfolding*) ``` paulson@13218 ` 121` ```lemma def_lfp_unfold: ``` paulson@13218 ` 122` ``` "[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)" ``` paulson@13218 ` 123` ```apply simp ``` paulson@13218 ` 124` ```apply (erule lfp_unfold) ``` paulson@13218 ` 125` ```done ``` paulson@13218 ` 126` paulson@13356 ` 127` ```subsection{*General Induction Rule for Least Fixedpoints*} ``` paulson@13218 ` 128` paulson@13218 ` 129` ```lemma Collect_is_pre_fixedpt: ``` paulson@46820 ` 130` ``` "[| bnd_mono(D,h); !!x. x \ h(Collect(lfp(D,h),P)) ==> P(x) |] ``` paulson@46820 ` 131` ``` ==> h(Collect(lfp(D,h),P)) \ Collect(lfp(D,h),P)" ``` paulson@13218 ` 132` ```by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD] ``` paulson@13218 ` 133` ``` lfp_subset [THEN subsetD]) ``` paulson@13218 ` 134` paulson@13218 ` 135` ```(*This rule yields an induction hypothesis in which the components of a ``` paulson@13218 ` 136` ``` data structure may be assumed to be elements of lfp(D,h)*) ``` paulson@13218 ` 137` ```lemma induct: ``` paulson@46820 ` 138` ``` "[| bnd_mono(D,h); a \ lfp(D,h); ``` paulson@46820 ` 139` ``` !!x. x \ h(Collect(lfp(D,h),P)) ==> P(x) ``` paulson@13218 ` 140` ``` |] ==> P(a)" ``` paulson@13218 ` 141` ```apply (rule Collect_is_pre_fixedpt ``` paulson@13218 ` 142` ``` [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2]) ``` paulson@13218 ` 143` ```apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]], ``` paulson@13218 ` 144` ``` blast+) ``` paulson@13218 ` 145` ```done ``` paulson@13218 ` 146` paulson@13218 ` 147` ```(*Definition form, to control unfolding*) ``` paulson@13218 ` 148` ```lemma def_induct: ``` paulson@13218 ` 149` ``` "[| A == lfp(D,h); bnd_mono(D,h); a:A; ``` paulson@46820 ` 150` ``` !!x. x \ h(Collect(A,P)) ==> P(x) ``` paulson@13218 ` 151` ``` |] ==> P(a)" ``` paulson@13218 ` 152` ```by (rule induct, blast+) ``` paulson@13218 ` 153` paulson@13218 ` 154` ```(*This version is useful when "A" is not a subset of D ``` paulson@46820 ` 155` ``` second premise could simply be h(D \ A) \ D or !!X. X<=D ==> h(X)<=D *) ``` paulson@13218 ` 156` ```lemma lfp_Int_lowerbound: ``` paulson@46820 ` 157` ``` "[| h(D \ A) \ A; bnd_mono(D,h) |] ==> lfp(D,h) \ A" ``` paulson@13218 ` 158` ```apply (rule lfp_lowerbound [THEN subset_trans]) ``` paulson@13218 ` 159` ```apply (erule bnd_mono_subset [THEN Int_greatest], blast+) ``` paulson@13218 ` 160` ```done ``` paulson@13218 ` 161` paulson@13218 ` 162` ```(*Monotonicity of lfp, where h precedes i under a domain-like partial order ``` paulson@13218 ` 163` ``` monotonicity of h is not strictly necessary; h must be bounded by D*) ``` paulson@13218 ` 164` ```lemma lfp_mono: ``` paulson@13218 ` 165` ``` assumes hmono: "bnd_mono(D,h)" ``` paulson@13218 ` 166` ``` and imono: "bnd_mono(E,i)" ``` paulson@46820 ` 167` ``` and subhi: "!!X. X<=D ==> h(X) \ i(X)" ``` paulson@46820 ` 168` ``` shows "lfp(D,h) \ lfp(E,i)" ``` paulson@13218 ` 169` ```apply (rule bnd_monoD1 [THEN lfp_greatest]) ``` paulson@13218 ` 170` ```apply (rule imono) ``` paulson@13218 ` 171` ```apply (rule hmono [THEN [2] lfp_Int_lowerbound]) ``` paulson@13218 ` 172` ```apply (rule Int_lower1 [THEN subhi, THEN subset_trans]) ``` paulson@13218 ` 173` ```apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) ``` paulson@13218 ` 174` ```done ``` clasohm@0 ` 175` paulson@13218 ` 176` ```(*This (unused) version illustrates that monotonicity is not really needed, ``` paulson@13218 ` 177` ``` but both lfp's must be over the SAME set D; Inter is anti-monotonic!*) ``` paulson@13218 ` 178` ```lemma lfp_mono2: ``` paulson@46820 ` 179` ``` "[| i(D) \ D; !!X. X<=D ==> h(X) \ i(X) |] ==> lfp(D,h) \ lfp(D,i)" ``` paulson@13218 ` 180` ```apply (rule lfp_greatest, assumption) ``` paulson@13218 ` 181` ```apply (rule lfp_lowerbound, blast, assumption) ``` paulson@13218 ` 182` ```done ``` paulson@13218 ` 183` paulson@14046 ` 184` ```lemma lfp_cong: ``` paulson@46820 ` 185` ``` "[|D=D'; !!X. X \ D' ==> h(X) = h'(X)|] ==> lfp(D,h) = lfp(D',h')" ``` paulson@14046 ` 186` ```apply (simp add: lfp_def) ``` paulson@14046 ` 187` ```apply (rule_tac t=Inter in subst_context) ``` paulson@14046 ` 188` ```apply (rule Collect_cong, simp_all) ``` paulson@14046 ` 189` ```done ``` paulson@13218 ` 190` paulson@14046 ` 191` paulson@14046 ` 192` ```subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*} ``` paulson@13218 ` 193` paulson@13218 ` 194` ```(*gfp contains each post-fixedpoint that is contained in D*) ``` paulson@46820 ` 195` ```lemma gfp_upperbound: "[| A \ h(A); A<=D |] ==> A \ gfp(D,h)" ``` paulson@13218 ` 196` ```apply (unfold gfp_def) ``` paulson@13218 ` 197` ```apply (rule PowI [THEN CollectI, THEN Union_upper]) ``` paulson@13218 ` 198` ```apply (assumption+) ``` paulson@13218 ` 199` ```done ``` paulson@13218 ` 200` paulson@46820 ` 201` ```lemma gfp_subset: "gfp(D,h) \ D" ``` paulson@13218 ` 202` ```by (unfold gfp_def, blast) ``` paulson@13218 ` 203` paulson@13218 ` 204` ```(*Used in datatype package*) ``` paulson@46820 ` 205` ```lemma def_gfp_subset: "A==gfp(D,h) ==> A \ D" ``` paulson@13218 ` 206` ```apply simp ``` paulson@13218 ` 207` ```apply (rule gfp_subset) ``` paulson@13218 ` 208` ```done ``` paulson@13218 ` 209` paulson@13218 ` 210` ```lemma gfp_least: ``` paulson@46820 ` 211` ``` "[| bnd_mono(D,h); !!X. [| X \ h(X); X<=D |] ==> X<=A |] ==> ``` paulson@46820 ` 212` ``` gfp(D,h) \ A" ``` paulson@13218 ` 213` ```apply (unfold gfp_def) ``` paulson@13218 ` 214` ```apply (blast dest: bnd_monoD1) ``` paulson@13218 ` 215` ```done ``` paulson@13218 ` 216` paulson@13218 ` 217` ```lemma gfp_lemma1: ``` paulson@46820 ` 218` ``` "[| bnd_mono(D,h); A<=h(A); A<=D |] ==> A \ h(gfp(D,h))" ``` paulson@13218 ` 219` ```apply (rule subset_trans, assumption) ``` paulson@13218 ` 220` ```apply (erule bnd_monoD2) ``` paulson@13218 ` 221` ```apply (rule_tac [2] gfp_subset) ``` paulson@13218 ` 222` ```apply (simp add: gfp_upperbound) ``` paulson@13218 ` 223` ```done ``` paulson@13218 ` 224` paulson@46820 ` 225` ```lemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) \ h(gfp(D,h))" ``` paulson@13218 ` 226` ```apply (rule gfp_least) ``` paulson@13218 ` 227` ```apply (rule_tac [2] gfp_lemma1) ``` paulson@13218 ` 228` ```apply (assumption+) ``` paulson@13218 ` 229` ```done ``` paulson@13218 ` 230` paulson@13218 ` 231` ```lemma gfp_lemma3: ``` paulson@46820 ` 232` ``` "bnd_mono(D,h) ==> h(gfp(D,h)) \ gfp(D,h)" ``` paulson@13218 ` 233` ```apply (rule gfp_upperbound) ``` paulson@13218 ` 234` ```apply (rule bnd_monoD2, assumption) ``` paulson@13218 ` 235` ```apply (rule gfp_lemma2, assumption) ``` paulson@13218 ` 236` ```apply (erule bnd_mono_subset, rule gfp_subset)+ ``` paulson@13218 ` 237` ```done ``` paulson@13218 ` 238` paulson@13218 ` 239` ```lemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))" ``` paulson@13218 ` 240` ```apply (rule equalityI) ``` paulson@13218 ` 241` ```apply (erule gfp_lemma2) ``` paulson@13218 ` 242` ```apply (erule gfp_lemma3) ``` paulson@13218 ` 243` ```done ``` paulson@13218 ` 244` paulson@13218 ` 245` ```(*Definition form, to control unfolding*) ``` paulson@13218 ` 246` ```lemma def_gfp_unfold: ``` paulson@13218 ` 247` ``` "[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)" ``` paulson@13218 ` 248` ```apply simp ``` paulson@13218 ` 249` ```apply (erule gfp_unfold) ``` paulson@13218 ` 250` ```done ``` paulson@13218 ` 251` paulson@13218 ` 252` paulson@13356 ` 253` ```subsection{*Coinduction Rules for Greatest Fixed Points*} ``` paulson@13218 ` 254` paulson@13218 ` 255` ```(*weak version*) ``` paulson@46820 ` 256` ```lemma weak_coinduct: "[| a: X; X \ h(X); X \ D |] ==> a \ gfp(D,h)" ``` paulson@13218 ` 257` ```by (blast intro: gfp_upperbound [THEN subsetD]) ``` clasohm@0 ` 258` paulson@13218 ` 259` ```lemma coinduct_lemma: ``` paulson@46820 ` 260` ``` "[| X \ h(X \ gfp(D,h)); X \ D; bnd_mono(D,h) |] ==> ``` paulson@46820 ` 261` ``` X \ gfp(D,h) \ h(X \ gfp(D,h))" ``` paulson@13218 ` 262` ```apply (erule Un_least) ``` paulson@13218 ` 263` ```apply (rule gfp_lemma2 [THEN subset_trans], assumption) ``` paulson@13218 ` 264` ```apply (rule Un_upper2 [THEN subset_trans]) ``` paulson@13218 ` 265` ```apply (rule bnd_mono_Un, assumption+) ``` paulson@13218 ` 266` ```apply (rule gfp_subset) ``` paulson@13218 ` 267` ```done ``` paulson@13218 ` 268` paulson@13218 ` 269` ```(*strong version*) ``` paulson@13218 ` 270` ```lemma coinduct: ``` paulson@46820 ` 271` ``` "[| bnd_mono(D,h); a: X; X \ h(X \ gfp(D,h)); X \ D |] ``` paulson@46820 ` 272` ``` ==> a \ gfp(D,h)" ``` paulson@13218 ` 273` ```apply (rule weak_coinduct) ``` paulson@13218 ` 274` ```apply (erule_tac [2] coinduct_lemma) ``` paulson@13218 ` 275` ```apply (simp_all add: gfp_subset Un_subset_iff) ``` paulson@13218 ` 276` ```done ``` paulson@13218 ` 277` paulson@13218 ` 278` ```(*Definition form, to control unfolding*) ``` paulson@13218 ` 279` ```lemma def_coinduct: ``` paulson@46820 ` 280` ``` "[| A == gfp(D,h); bnd_mono(D,h); a: X; X \ h(X \ A); X \ D |] ==> ``` paulson@46820 ` 281` ``` a \ A" ``` paulson@13218 ` 282` ```apply simp ``` paulson@13218 ` 283` ```apply (rule coinduct, assumption+) ``` paulson@13218 ` 284` ```done ``` paulson@13218 ` 285` paulson@13218 ` 286` ```(*The version used in the induction/coinduction package*) ``` paulson@13218 ` 287` ```lemma def_Collect_coinduct: ``` paulson@13218 ` 288` ``` "[| A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); ``` paulson@46820 ` 289` ``` a: X; X \ D; !!z. z: X ==> P(X \ A, z) |] ==> ``` paulson@46820 ` 290` ``` a \ A" ``` paulson@13218 ` 291` ```apply (rule def_coinduct, assumption+, blast+) ``` paulson@13218 ` 292` ```done ``` clasohm@0 ` 293` paulson@13218 ` 294` ```(*Monotonicity of gfp!*) ``` paulson@13218 ` 295` ```lemma gfp_mono: ``` paulson@46820 ` 296` ``` "[| bnd_mono(D,h); D \ E; ``` paulson@46820 ` 297` ``` !!X. X<=D ==> h(X) \ i(X) |] ==> gfp(D,h) \ gfp(E,i)" ``` paulson@13218 ` 298` ```apply (rule gfp_upperbound) ``` paulson@13218 ` 299` ```apply (rule gfp_lemma2 [THEN subset_trans], assumption) ``` paulson@13218 ` 300` ```apply (blast del: subsetI intro: gfp_subset) ``` paulson@13218 ` 301` ```apply (blast del: subsetI intro: subset_trans gfp_subset) ``` paulson@13218 ` 302` ```done ``` paulson@13218 ` 303` clasohm@0 ` 304` ```end ```