src/CCL/fix.thy
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 0 a5a9c433f639
permissions -rw-r--r--
added HOL/Prolog
clasohm@0
     1
(*  Title: 	CCL/Lazy/fix.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     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@0
    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
clasohm@0
    20
  "idgen(f) == lam t.case(t,true,false,%x y.<f`x, f`y>,%u.lam x.f ` u(x))"
clasohm@0
    21
clasohm@0
    22
  INCL_def   "INCL(%x.P(x)) == (ALL f.(ALL n:Nat.P(f^n`bot)) --> P(fix(f)))"
clasohm@0
    23
  po_INCL    "INCL(%x.a(x) [= b(x))"
clasohm@0
    24
  INCL_subst "INCL(P) ==> INCL(%x.P((g::i=>i)(x)))"
clasohm@0
    25
clasohm@0
    26
end