Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Fixedpt.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      ZF/Fixedpt.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section\<open>Least and Greatest Fixed Points; the Knaster-Tarski Theorem\<close>

theory Fixedpt imports equalities begin

definition
  (*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) == \({X: Pow(D). h(X) \ X})"

definition
  gfp      :: "[i,i=>i]=>i"  where
     "gfp(D,h) == \({X: Pow(D). X \ h(X)})"

text\<open>The theorem is proved in the lattice of subsets of \<^term>\<open>D\<close>,
      namely \<^term>\<open>Pow(D)\<close>, with Inter as the greatest lower bound.\<close>

subsection\<open>Monotone Operators\<close>

lemma bnd_monoI:
    "[| h(D)<=D;
        !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) \<subseteq> 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) \ 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\<in>I. h(A(i))) \<subseteq> h((\<Union>i\<in>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="(\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)
done

subsection\<open>Proof of Knaster-Tarski Theorem using \<^term>\<open>lfp\<close>\<close>

(*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\<open>General Induction Rule for Least Fixedpoints\<close>

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)) \<subseteq> 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 \<in> 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 \<in> 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 \<inter> A) \<subseteq> 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)
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\<open>Proof of Knaster-Tarski Theorem using \<^term>\<open>gfp\<close>\<close>

(*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) \<subseteq> 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\<open>Coinduction Rules for Greatest Fixed Points\<close>

(*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 \<union> gfp(D,h) \<subseteq> h(X \<union> 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 \<in> 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 \<in> 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 \<subseteq> D;  !!z. z: X ==> P(X \<union> A, z) |] ==>
     a \<in> 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) \<subseteq> i(X)  |] ==> gfp(D,h) \<subseteq> 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

end

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.