src/HOL/HOLCF/ex/Fix2.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 42151 4da4fc77664b
child 63549 b0d31c7def86
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/HOLCF/ex/Fix2.thy
     2     Author:     Franz Regensburger
     3 
     4 Show that fix is the unique least fixed-point operator.
     5 From axioms gix1_def,gix2_def it follows that fix = gix
     6 *)
     7 
     8 theory Fix2
     9 imports HOLCF
    10 begin
    11 
    12 axiomatization
    13   gix :: "('a->'a)->'a" where
    14   gix1_def: "F$(gix$F) = gix$F" and
    15   gix2_def: "F$y=y ==> gix$F << y"
    16 
    17 
    18 lemma lemma1: "fix = gix"
    19 apply (rule cfun_eqI)
    20 apply (rule below_antisym)
    21 apply (rule fix_least)
    22 apply (rule gix1_def)
    23 apply (rule gix2_def)
    24 apply (rule fix_eq [symmetric])
    25 done
    26 
    27 lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"
    28 apply (rule lemma1 [THEN subst])
    29 apply (rule fix_def2)
    30 done
    31 
    32 end