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
```