# Theory Fixedpt

Up to index of Isabelle/ZF

theory Fixedpt
imports equalities
`(*  Title:      ZF/Fixedpt.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1992  University of Cambridge*)header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}theory Fixedpt imports equalities begindefinition   (*monotone operator from Pow(D) to itself*)  bnd_mono :: "[i,i=>i]=>o"  where     "bnd_mono(D,h) == h(D)<=D & (∀W X. W<=X --> X<=D --> h(W) ⊆ h(X))"definition   lfp      :: "[i,i=>i]=>i"  where     "lfp(D,h) == \<Inter>({X: Pow(D). h(X) ⊆ X})"definition   gfp      :: "[i,i=>i]=>i"  where     "gfp(D,h) == \<Union>({X: Pow(D). X ⊆ h(X)})"text{*The theorem is proved in the lattice of subsets of @{term D},       namely @{term "Pow(D)"}, with Inter as the greatest lower bound.*}subsection{*Monotone Operators*}lemma bnd_monoI:    "[| h(D)<=D;           !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) ⊆ h(X)        |] ==> bnd_mono(D,h)"by (unfold bnd_mono_def, clarify, blast)  lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) ⊆ D"apply (unfold bnd_mono_def)apply (erule conjunct1)donelemma bnd_monoD2: "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) ⊆ h(X)"by (unfold bnd_mono_def, blast)lemma bnd_mono_subset:    "[| bnd_mono(D,h);  X<=D |] ==> h(X) ⊆ D"by (unfold bnd_mono_def, clarify, blast) lemma bnd_mono_Un:     "[| bnd_mono(D,h);  A ⊆ D;  B ⊆ D |] ==> h(A) ∪ h(B) ⊆ h(A ∪ B)"apply (unfold bnd_mono_def)apply (rule Un_least, blast+)done(*unused*)lemma bnd_mono_UN:     "[| bnd_mono(D,h);  ∀i∈I. A(i) ⊆ D |]       ==> (\<Union>i∈I. h(A(i))) ⊆ h((\<Union>i∈I. A(i)))"apply (unfold bnd_mono_def) apply (rule UN_least)apply (elim conjE) apply (drule_tac x="A(i)" in spec)apply (drule_tac x="(\<Union>i∈I. A(i))" in spec) apply blast done(*Useful??*)lemma bnd_mono_Int:     "[| bnd_mono(D,h);  A ⊆ D;  B ⊆ D |] ==> h(A ∩ B) ⊆ h(A) ∩ h(B)"apply (rule Int_greatest) apply (erule bnd_monoD2, rule Int_lower1, assumption) apply (erule bnd_monoD2, rule Int_lower2, assumption) donesubsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}(*lfp is contained in each pre-fixedpoint*)lemma lfp_lowerbound:     "[| h(A) ⊆ A;  A<=D |] ==> lfp(D,h) ⊆ A"by (unfold lfp_def, blast)(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)lemma lfp_subset: "lfp(D,h) ⊆ D"by (unfold lfp_def Inter_def, blast)(*Used in datatype package*)lemma def_lfp_subset:  "A == lfp(D,h) ==> A ⊆ D"apply simpapply (rule lfp_subset)donelemma lfp_greatest:      "[| h(D) ⊆ D;  !!X. [| h(X) ⊆ X;  X<=D |] ==> A<=X |] ==> A ⊆ lfp(D,h)"by (unfold lfp_def, blast) lemma lfp_lemma1:      "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) ⊆ A"apply (erule bnd_monoD2 [THEN subset_trans])apply (rule lfp_lowerbound, assumption+)donelemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) ⊆ lfp(D,h)"apply (rule bnd_monoD1 [THEN lfp_greatest])apply (rule_tac [2] lfp_lemma1)apply (assumption+)donelemma lfp_lemma3:     "bnd_mono(D,h) ==> lfp(D,h) ⊆ h(lfp(D,h))"apply (rule lfp_lowerbound)apply (rule bnd_monoD2, assumption)apply (rule lfp_lemma2, assumption)apply (erule_tac [2] bnd_mono_subset)apply (rule lfp_subset)+donelemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"apply (rule equalityI) apply (erule lfp_lemma3) apply (erule lfp_lemma2) done(*Definition form, to control unfolding*)lemma def_lfp_unfold:    "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"apply simpapply (erule lfp_unfold)donesubsection{*General Induction Rule for Least Fixedpoints*}lemma Collect_is_pre_fixedpt:    "[| bnd_mono(D,h);  !!x. x ∈ h(Collect(lfp(D,h),P)) ==> P(x) |]     ==> h(Collect(lfp(D,h),P)) ⊆ Collect(lfp(D,h),P)"by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD]                  lfp_subset [THEN subsetD]) (*This rule yields an induction hypothesis in which the components of a  data structure may be assumed to be elements of lfp(D,h)*)lemma induct:    "[| bnd_mono(D,h);  a ∈ lfp(D,h);                            !!x. x ∈ h(Collect(lfp(D,h),P)) ==> P(x)              |] ==> P(a)"apply (rule Collect_is_pre_fixedpt              [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2])apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]],        blast+)done(*Definition form, to control unfolding*)lemma def_induct:    "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;            !!x. x ∈ h(Collect(A,P)) ==> P(x)       |] ==> P(a)"by (rule induct, blast+)(*This version is useful when "A" is not a subset of D  second premise could simply be h(D ∩ A) ⊆ D or !!X. X<=D ==> h(X)<=D *)lemma lfp_Int_lowerbound:    "[| h(D ∩ A) ⊆ A;  bnd_mono(D,h) |] ==> lfp(D,h) ⊆ A" apply (rule lfp_lowerbound [THEN subset_trans])apply (erule bnd_mono_subset [THEN Int_greatest], blast+)done(*Monotonicity of lfp, where h precedes i under a domain-like partial order  monotonicity of h is not strictly necessary; h must be bounded by D*)lemma lfp_mono:  assumes hmono: "bnd_mono(D,h)"      and imono: "bnd_mono(E,i)"      and subhi: "!!X. X<=D ==> h(X) ⊆ i(X)"    shows "lfp(D,h) ⊆ lfp(E,i)"apply (rule bnd_monoD1 [THEN lfp_greatest])apply (rule imono)apply (rule hmono [THEN [2] lfp_Int_lowerbound])apply (rule Int_lower1 [THEN subhi, THEN subset_trans])apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) done(*This (unused) version illustrates that monotonicity is not really needed,  but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)lemma lfp_mono2:    "[| i(D) ⊆ D;  !!X. X<=D ==> h(X) ⊆ i(X)  |] ==> lfp(D,h) ⊆ lfp(D,i)"apply (rule lfp_greatest, assumption)apply (rule lfp_lowerbound, blast, assumption)donelemma lfp_cong:     "[|D=D'; !!X. X ⊆ D' ==> h(X) = h'(X)|] ==> lfp(D,h) = lfp(D',h')"apply (simp add: lfp_def)apply (rule_tac t=Inter in subst_context)apply (rule Collect_cong, simp_all) done subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*}(*gfp contains each post-fixedpoint that is contained in D*)lemma gfp_upperbound: "[| A ⊆ h(A);  A<=D |] ==> A ⊆ gfp(D,h)"apply (unfold gfp_def)apply (rule PowI [THEN CollectI, THEN Union_upper])apply (assumption+)donelemma gfp_subset: "gfp(D,h) ⊆ D"by (unfold gfp_def, blast)(*Used in datatype package*)lemma def_gfp_subset: "A==gfp(D,h) ==> A ⊆ D"apply simpapply (rule gfp_subset)donelemma gfp_least:     "[| bnd_mono(D,h);  !!X. [| X ⊆ h(X);  X<=D |] ==> X<=A |] ==>       gfp(D,h) ⊆ A"apply (unfold gfp_def)apply (blast dest: bnd_monoD1) donelemma gfp_lemma1:     "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A ⊆ h(gfp(D,h))"apply (rule subset_trans, assumption)apply (erule bnd_monoD2)apply (rule_tac [2] gfp_subset)apply (simp add: gfp_upperbound)donelemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) ⊆ h(gfp(D,h))"apply (rule gfp_least)apply (rule_tac [2] gfp_lemma1)apply (assumption+)donelemma gfp_lemma3:     "bnd_mono(D,h) ==> h(gfp(D,h)) ⊆ gfp(D,h)"apply (rule gfp_upperbound)apply (rule bnd_monoD2, assumption)apply (rule gfp_lemma2, assumption)apply (erule bnd_mono_subset, rule gfp_subset)+donelemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"apply (rule equalityI) apply (erule gfp_lemma2) apply (erule gfp_lemma3) done(*Definition form, to control unfolding*)lemma def_gfp_unfold:    "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"apply simpapply (erule gfp_unfold)donesubsection{*Coinduction Rules for Greatest Fixed Points*}(*weak version*)lemma weak_coinduct: "[| a: X;  X ⊆ h(X);  X ⊆ D |] ==> a ∈ gfp(D,h)"by (blast intro: gfp_upperbound [THEN subsetD])lemma coinduct_lemma:    "[| X ⊆ h(X ∪ gfp(D,h));  X ⊆ D;  bnd_mono(D,h) |] ==>        X ∪ gfp(D,h) ⊆ h(X ∪ gfp(D,h))"apply (erule Un_least)apply (rule gfp_lemma2 [THEN subset_trans], assumption)apply (rule Un_upper2 [THEN subset_trans])apply (rule bnd_mono_Un, assumption+) apply (rule gfp_subset)done(*strong version*)lemma coinduct:     "[| bnd_mono(D,h);  a: X;  X ⊆ h(X ∪ gfp(D,h));  X ⊆ D |]      ==> a ∈ gfp(D,h)"apply (rule weak_coinduct)apply (erule_tac [2] coinduct_lemma)apply (simp_all add: gfp_subset Un_subset_iff) done(*Definition form, to control unfolding*)lemma def_coinduct:    "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X ⊆ h(X ∪ A);  X ⊆ D |] ==>       a ∈ A"apply simpapply (rule coinduct, assumption+)done(*The version used in the induction/coinduction package*)lemma def_Collect_coinduct:    "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));           a: X;  X ⊆ D;  !!z. z: X ==> P(X ∪ A, z) |] ==>       a ∈ A"apply (rule def_coinduct, assumption+, blast+)done(*Monotonicity of gfp!*)lemma gfp_mono:    "[| bnd_mono(D,h);  D ⊆ E;                          !!X. X<=D ==> h(X) ⊆ i(X)  |] ==> gfp(D,h) ⊆ gfp(E,i)"apply (rule gfp_upperbound)apply (rule gfp_lemma2 [THEN subset_trans], assumption)apply (blast del: subsetI intro: gfp_subset) apply (blast del: subsetI intro: subset_trans gfp_subset) doneend`