src/CCL/Fix.thy
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1474 3f7d67927fe2
child 3837 d7f033c74b38
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
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
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