Quelle Complete_Lattice.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section "Abstract Interpretation"

subsection "Complete Lattice"

theory Complete_Lattice
imports Main
begin

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 index_lfp: "lfp f \ L"
by(auto simp: lfp_def intro: Glb_in_L)

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

quality96%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.