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
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/ex/Fix2.thy
clasohm@1479
     2
    Author:     Franz Regensburger
regensbu@1274
     3
wenzelm@17291
     4
Show that fix is the unique least fixed-point operator.
wenzelm@12036
     5
From axioms gix1_def,gix2_def it follows that fix = gix
regensbu@1274
     6
*)
regensbu@1274
     7
wenzelm@17291
     8
theory Fix2
wenzelm@17291
     9
imports HOLCF
wenzelm@17291
    10
begin
regensbu@1274
    11
wenzelm@25135
    12
axiomatization
wenzelm@25135
    13
  gix :: "('a->'a)->'a" where
wenzelm@25135
    14
  gix1_def: "F$(gix$F) = gix$F" and
wenzelm@17291
    15
  gix2_def: "F$y=y ==> gix$F << y"
regensbu@1274
    16
wenzelm@19742
    17
wenzelm@19742
    18
lemma lemma1: "fix = gix"
huffman@40002
    19
apply (rule cfun_eqI)
huffman@40431
    20
apply (rule below_antisym)
wenzelm@19742
    21
apply (rule fix_least)
wenzelm@19742
    22
apply (rule gix1_def)
wenzelm@19742
    23
apply (rule gix2_def)
wenzelm@19742
    24
apply (rule fix_eq [symmetric])
wenzelm@19742
    25
done
wenzelm@19742
    26
wenzelm@19742
    27
lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"
wenzelm@19742
    28
apply (rule lemma1 [THEN subst])
wenzelm@19742
    29
apply (rule fix_def2)
wenzelm@19742
    30
done
regensbu@1274
    31
regensbu@1274
    32
end