src/HOL/Wellfounded_Recursion.thy
author paulson
Fri, 29 Oct 2004 15:16:02 +0200
changeset 15270 8b3f707a78a7
parent 11451 8abfb4f7bd02
child 15341 254f6f00b60e
permissions -rw-r--r--
fixed reference to renamed theorem
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
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 11328
diff changeset
     9
Wellfounded_Recursion = Transitive_Closure + 
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    10
11328
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    11
consts
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    12
  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set"
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    13
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    14
inductive "wfrec_rel R F"
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    15
intrs
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    16
  wfrecI "ALL z. (z, x) : R --> (z, g z) : wfrec_rel R F ==>
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    17
            (x, F g x) : wfrec_rel R F"
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    18
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    19
constdefs
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    20
  wf         :: "('a * 'a)set => bool"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    21
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    22
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    23
  acyclic :: "('a*'a)set => bool"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    24
  "acyclic r == !x. (x,x) ~: r^+"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    25
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    26
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    27
  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    28
11328
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    29
  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    30
  "adm_wf R F == ALL f g x.
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    31
     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    32
11328
956ec01b46e0 Inductive characterization of wfrec combinator.
berghofe
parents: 11137
diff changeset
    33
  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 11328
diff changeset
    34
  "wfrec R F == %x. THE y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    35
11137
9265b6415d76 added wellorder axclass
oheimb
parents: 10213
diff changeset
    36
axclass
9265b6415d76 added wellorder axclass
oheimb
parents: 10213
diff changeset
    37
  wellorder < linorder
9265b6415d76 added wellorder axclass
oheimb
parents: 10213
diff changeset
    38
  wf "wf {(x,y::'a::ord). x<y}"
9265b6415d76 added wellorder axclass
oheimb
parents: 10213
diff changeset
    39
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    40
end