src/CCL/Fix.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3837 d7f033c74b38
child 17456 bcf7544875b2
permissions -rw-r--r--
tidying
clasohm@1474
     1
(*  Title:      CCL/Lazy/fix.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1474
     3
    Author:     Martin Coen
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Tentative attempt at including fixed point induction.
clasohm@0
     7
Justified by Smith.
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
Fix = Type + 
clasohm@0
    11
clasohm@0
    12
consts
clasohm@0
    13
clasohm@1474
    14
  idgen      ::       "[i]=>i"
clasohm@0
    15
  INCL      :: "[i=>o]=>o"
clasohm@0
    16
clasohm@0
    17
rules
clasohm@0
    18
clasohm@0
    19
  idgen_def
wenzelm@3837
    20
  "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
clasohm@0
    21
wenzelm@3837
    22
  INCL_def   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
wenzelm@3837
    23
  po_INCL    "INCL(%x. a(x) [= b(x))"
wenzelm@3837
    24
  INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
clasohm@0
    25
clasohm@0
    26
end