Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Complete_Lattice.thy Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.13 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.