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
nipkow@10213
     1
(*  Title:      HOL/Wellfounded_Recursion.thy
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Tobias Nipkow
nipkow@10213
     4
    Copyright   1992  University of Cambridge
nipkow@10213
     5
nipkow@10213
     6
Well-founded Recursion
nipkow@10213
     7
*)
nipkow@10213
     8
paulson@11451
     9
Wellfounded_Recursion = Transitive_Closure + 
nipkow@10213
    10
berghofe@11328
    11
consts
berghofe@11328
    12
  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set"
berghofe@11328
    13
berghofe@11328
    14
inductive "wfrec_rel R F"
berghofe@11328
    15
intrs
berghofe@11328
    16
  wfrecI "ALL z. (z, x) : R --> (z, g z) : wfrec_rel R F ==>
berghofe@11328
    17
            (x, F g x) : wfrec_rel R F"
berghofe@11328
    18
nipkow@10213
    19
constdefs
nipkow@10213
    20
  wf         :: "('a * 'a)set => bool"
nipkow@10213
    21
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
nipkow@10213
    22
nipkow@10213
    23
  acyclic :: "('a*'a)set => bool"
nipkow@10213
    24
  "acyclic r == !x. (x,x) ~: r^+"
nipkow@10213
    25
nipkow@10213
    26
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
nipkow@10213
    27
  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
nipkow@10213
    28
berghofe@11328
    29
  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
berghofe@11328
    30
  "adm_wf R F == ALL f g x.
berghofe@11328
    31
     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
nipkow@10213
    32
berghofe@11328
    33
  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
paulson@11451
    34
  "wfrec R F == %x. THE y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
nipkow@10213
    35
oheimb@11137
    36
axclass
oheimb@11137
    37
  wellorder < linorder
oheimb@11137
    38
  wf "wf {(x,y::'a::ord). x<y}"
oheimb@11137
    39
nipkow@10213
    40
end