src/HOLCF/ex/Fix2.thy
author wenzelm
Thu, 16 Sep 2010 15:37:12 +0200
changeset 39438 c5ece2a7a86e
parent 35174 e15040ae75d7
child 40002 c5b5f7a3a3b1
permissions -rw-r--r--
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);

(*  Title:      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 ext_cfun)
apply (rule antisym_less)
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