locale Complete_Lattice = fixes L :: "'a::order set"and Glb :: "'a set \ 'a" assumes Glb_lower: "A \ L \ a \ A \ Glb A \ a" and Glb_greatest: "b \ L \ \a\A. b \ a \ b \ Glb A" and Glb_in_L: "A \ L \ Glb A \ L" begin
definition lfp :: "('a \ 'a) \ 'a" where "lfp f = Glb {a : L. f a \ a}"
lemma lfp_lowerbound: "\ a \ L; f a \ a \ \ lfp f \ a" by (auto simp add: lfp_def intro: Glb_lower)
lemma lfp_greatest: "\ a \ L; \u. \ u \ L; f u \ u\ \ a \ u \ \ a \ lfp f" by (auto simp add: lfp_def intro: Glb_greatest)
lemma lfp_unfold: assumes"\x. f x \ L \ x \ L" and mono: "mono f"shows"lfp f = f (lfp f)"
proof- note assms(1)[simp] index_lfp[simp] have 1: "f (lfp f) \ lfp f" apply(rule lfp_greatest) apply simp by (blast intro: lfp_lowerbound monoD[OF mono] order_trans) have"lfp f \ f (lfp f)" by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound) with 1 show ?thesis by(blast intro: order_antisym) qed
end
end
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
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.
