Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
yts806.mco
Sprache: Unknown
(* 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
[ Verzeichnis aufwärts0.18unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
