src/HOL/Wellfounded_Recursion.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 11451 8abfb4f7bd02
child 15341 254f6f00b60e
permissions -rw-r--r--
import -> imports
     1 (*  Title:      HOL/Wellfounded_Recursion.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1992  University of Cambridge
     5 
     6 Well-founded Recursion
     7 *)
     8 
     9 Wellfounded_Recursion = Transitive_Closure + 
    10 
    11 consts
    12   wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set"
    13 
    14 inductive "wfrec_rel R F"
    15 intrs
    16   wfrecI "ALL z. (z, x) : R --> (z, g z) : wfrec_rel R F ==>
    17             (x, F g x) : wfrec_rel R F"
    18 
    19 constdefs
    20   wf         :: "('a * 'a)set => bool"
    21   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
    22 
    23   acyclic :: "('a*'a)set => bool"
    24   "acyclic r == !x. (x,x) ~: r^+"
    25 
    26   cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    27   "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
    28 
    29   adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
    30   "adm_wf R F == ALL f g x.
    31      (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    32 
    33   wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    34   "wfrec R F == %x. THE y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
    35 
    36 axclass
    37   wellorder < linorder
    38   wf "wf {(x,y::'a::ord). x<y}"
    39 
    40 end