Quelle Fix2.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/ex/Fix2.thy
    Author:     Franz Regensburger

Show that fix is the unique least fixed-point operator.
From axioms gix1_def,gix2_def it follows that fix = gix
*)

theory Fix2
imports HOLCF
begin

axiomatization
  gix :: "('a \ 'a) \'a" where
  gix1_def: "F\(gix\F) = gix\F" and
  gix2_def: "F\y = y \ gix\F << y"

lemma lemma1: "fix = gix"
apply (rule cfun_eqI)
apply (rule below_antisym)
apply (rule fix_least)
apply (rule gix1_def)
apply (rule gix2_def)
apply (rule fix_eq [symmetric])
done

lemma lemma2: "gix\F = lub (range (\i. iterate i\F\UU))"
apply (rule lemma1 [THEN subst])
apply (rule fix_def2)
done

end

quality100%

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