src/HOL/Wellfounded_Recursion.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10213 01c2744a3786
child 11137 9265b6415d76
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Wellfounded_Recursion.thy
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     5
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     6
Well-founded Recursion
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     7
*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     8
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     9
Wellfounded_Recursion = Transitive_Closure +
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    10
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    11
constdefs
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    12
  wf         :: "('a * 'a)set => bool"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    13
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    14
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    15
  acyclic :: "('a*'a)set => bool"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    16
  "acyclic r == !x. (x,x) ~: r^+"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    17
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    18
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    19
  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    20
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    21
  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    22
  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    23
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    24
  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    25
  "the_recfun r H a  == (@f. is_recfun r H a f)"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    26
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    27
  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    28
  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    29
                            r x)  x)"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    30
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    31
end