(* Title: ZF/fixedpt.thy ID: $Id: Fixedpt.thy,v 1.16 2005/06/17 14:15:09 haftmann Exp $ 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 begin constdefs (*monotone operator from Pow(D) to itself*) bnd_mono :: "[i,i=>i]=>o" "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))" lfp :: "[i,i=>i]=>i" "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})" gfp :: "[i,i=>i]=>i" "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) done lemma 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) Un h(B) <= h(A Un 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 Int B) <= h(A) Int h(B)" apply (rule Int_greatest) apply (erule bnd_monoD2, rule Int_lower1, assumption) apply (erule bnd_monoD2, rule Int_lower2, assumption) done subsection{*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 simp apply (rule lfp_subset) done lemma 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+) done lemma 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+) done lemma 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)+ done lemma 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 simp apply (erule lfp_unfold) done subsection{*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 Int A) <= D or !!X. X<=D ==> h(X)<=D *) lemma lfp_Int_lowerbound: "[| h(D Int 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) done lemma 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+) done lemma 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 simp apply (rule gfp_subset) done lemma 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) done lemma 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) done lemma 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+) done lemma 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)+ done lemma 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 simp apply (erule gfp_unfold) done subsection{*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 Un gfp(D,h)); X <= D; bnd_mono(D,h) |] ==> X Un gfp(D,h) <= h(X Un 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 Un 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 Un A); X <= D |] ==> a : A" apply simp apply (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 Un 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) done ML {* val bnd_mono_def = thm "bnd_mono_def"; val lfp_def = thm "lfp_def"; val gfp_def = thm "gfp_def"; val bnd_monoI = thm "bnd_monoI"; val bnd_monoD1 = thm "bnd_monoD1"; val bnd_monoD2 = thm "bnd_monoD2"; val bnd_mono_subset = thm "bnd_mono_subset"; val bnd_mono_Un = thm "bnd_mono_Un"; val bnd_mono_Int = thm "bnd_mono_Int"; val lfp_lowerbound = thm "lfp_lowerbound"; val lfp_subset = thm "lfp_subset"; val def_lfp_subset = thm "def_lfp_subset"; val lfp_greatest = thm "lfp_greatest"; val lfp_unfold = thm "lfp_unfold"; val def_lfp_unfold = thm "def_lfp_unfold"; val Collect_is_pre_fixedpt = thm "Collect_is_pre_fixedpt"; val induct = thm "induct"; val def_induct = thm "def_induct"; val lfp_Int_lowerbound = thm "lfp_Int_lowerbound"; val lfp_mono = thm "lfp_mono"; val lfp_mono2 = thm "lfp_mono2"; val gfp_upperbound = thm "gfp_upperbound"; val gfp_subset = thm "gfp_subset"; val def_gfp_subset = thm "def_gfp_subset"; val gfp_least = thm "gfp_least"; val gfp_unfold = thm "gfp_unfold"; val def_gfp_unfold = thm "def_gfp_unfold"; val weak_coinduct = thm "weak_coinduct"; val coinduct = thm "coinduct"; val def_coinduct = thm "def_coinduct"; val def_Collect_coinduct = thm "def_Collect_coinduct"; val gfp_mono = thm "gfp_mono"; *} end
lemma bnd_monoI:
[| h(D) ⊆ D; !!W X. [| W ⊆ D; X ⊆ D; W ⊆ X |] ==> h(W) ⊆ h(X) |] ==> bnd_mono(D, h)
lemma bnd_monoD1:
bnd_mono(D, h) ==> h(D) ⊆ D
lemma bnd_monoD2:
[| bnd_mono(D, h); W ⊆ X; X ⊆ D |] ==> h(W) ⊆ h(X)
lemma bnd_mono_subset:
[| bnd_mono(D, h); X ⊆ D |] ==> h(X) ⊆ D
lemma bnd_mono_Un:
[| bnd_mono(D, h); A ⊆ D; B ⊆ D |] ==> h(A) ∪ h(B) ⊆ h(A ∪ B)
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))
lemma bnd_mono_Int:
[| bnd_mono(D, h); A ⊆ D; B ⊆ D |] ==> h(A ∩ B) ⊆ h(A) ∩ h(B)
lemma lfp_lowerbound:
[| h(A) ⊆ A; A ⊆ D |] ==> lfp(D, h) ⊆ A
lemma lfp_subset:
lfp(D, h) ⊆ D
lemma def_lfp_subset:
A == lfp(D, h) ==> A ⊆ D
lemma lfp_greatest:
[| h(D) ⊆ D; !!X. [| h(X) ⊆ X; X ⊆ D |] ==> A ⊆ X |] ==> A ⊆ lfp(D, h)
lemma lfp_lemma1:
[| bnd_mono(D, h); h(A) ⊆ A; A ⊆ D |] ==> h(lfp(D, h)) ⊆ A
lemma lfp_lemma2:
bnd_mono(D, h) ==> h(lfp(D, h)) ⊆ lfp(D, h)
lemma lfp_lemma3:
bnd_mono(D, h) ==> lfp(D, h) ⊆ h(lfp(D, h))
lemma lfp_unfold:
bnd_mono(D, h) ==> lfp(D, h) = h(lfp(D, h))
lemma def_lfp_unfold:
[| A == lfp(D, h); bnd_mono(D, h) |] ==> A = h(A)
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)
lemma induct:
[| bnd_mono(D, h); a ∈ lfp(D, h); !!x. x ∈ h(Collect(lfp(D, h), P)) ==> P(x) |] ==> P(a)
lemma def_induct:
[| A == lfp(D, h); bnd_mono(D, h); a ∈ A; !!x. x ∈ h(Collect(A, P)) ==> P(x) |] ==> P(a)
lemma lfp_Int_lowerbound:
[| h(D ∩ A) ⊆ A; bnd_mono(D, h) |] ==> lfp(D, h) ⊆ A
lemma lfp_mono:
[| bnd_mono(D, h); bnd_mono(E, i); !!X. X ⊆ D ==> h(X) ⊆ i(X) |] ==> lfp(D, h) ⊆ lfp(E, i)
lemma lfp_mono2:
[| i(D) ⊆ D; !!X. X ⊆ D ==> h(X) ⊆ i(X) |] ==> lfp(D, h) ⊆ lfp(D, i)
lemma lfp_cong:
[| D = D'; !!X. X ⊆ D' ==> h(X) = h'(X) |] ==> lfp(D, h) = lfp(D', h')
lemma gfp_upperbound:
[| A ⊆ h(A); A ⊆ D |] ==> A ⊆ gfp(D, h)
lemma gfp_subset:
gfp(D, h) ⊆ D
lemma def_gfp_subset:
A == gfp(D, h) ==> A ⊆ D
lemma gfp_least:
[| bnd_mono(D, h); !!X. [| X ⊆ h(X); X ⊆ D |] ==> X ⊆ A |] ==> gfp(D, h) ⊆ A
lemma gfp_lemma1:
[| bnd_mono(D, h); A ⊆ h(A); A ⊆ D |] ==> A ⊆ h(gfp(D, h))
lemma gfp_lemma2:
bnd_mono(D, h) ==> gfp(D, h) ⊆ h(gfp(D, h))
lemma gfp_lemma3:
bnd_mono(D, h) ==> h(gfp(D, h)) ⊆ gfp(D, h)
lemma gfp_unfold:
bnd_mono(D, h) ==> gfp(D, h) = h(gfp(D, h))
lemma def_gfp_unfold:
[| A == gfp(D, h); bnd_mono(D, h) |] ==> A = h(A)
lemma weak_coinduct:
[| a ∈ X; X ⊆ h(X); X ⊆ D |] ==> a ∈ gfp(D, h)
lemma coinduct_lemma:
[| X ⊆ h(X ∪ gfp(D, h)); X ⊆ D; bnd_mono(D, h) |] ==> X ∪ gfp(D, h) ⊆ h(X ∪ gfp(D, h))
lemma coinduct:
[| bnd_mono(D, h); a ∈ X; X ⊆ h(X ∪ gfp(D, h)); X ⊆ D |] ==> a ∈ gfp(D, h)
lemma def_coinduct:
[| A == gfp(D, h); bnd_mono(D, h); a ∈ X; X ⊆ h(X ∪ A); X ⊆ D |] ==> a ∈ A
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
lemma gfp_mono:
[| bnd_mono(D, h); D ⊆ E; !!X. X ⊆ D ==> h(X) ⊆ i(X) |] ==> gfp(D, h) ⊆ gfp(E, i)