(* Title: HOLCF/ex/Fix2.thy ID: $Id: Fix2.thy,v 1.7 2005/09/06 17:28:58 wenzelm Exp $ 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 consts gix :: "('a->'a)->'a" axioms gix1_def: "F$(gix$F) = gix$F" gix2_def: "F$y=y ==> gix$F << y" ML {* use_legacy_bindings (the_context ()) *} end
theorem lemma1:
fix = gix
theorem lemma2:
gix·F = (LUB i. iterate i F UU)