src/HOL/Induct/Acc.thy
author berghofe
Wed Oct 21 17:48:02 1998 +0200 (1998-10-21)
changeset 5717 0d28dbe484b6
parent 5273 70f478d55606
child 7721 cb353d802ade
permissions -rw-r--r--
Changed syntax of inductive.
paulson@3120
     1
(*  Title:      HOL/ex/Acc.thy
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120
     4
    Copyright   1994  University of Cambridge
paulson@3120
     5
paulson@3120
     6
Inductive definition of acc(r)
paulson@3120
     7
paulson@3120
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
paulson@3120
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
paulson@3120
    10
*)
paulson@3120
    11
berghofe@5102
    12
Acc = WF + Inductive +
paulson@3120
    13
paulson@3120
    14
constdefs
paulson@3120
    15
  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
paulson@3120
    16
  "pred x r == {y. (y,x):r}"
paulson@3120
    17
paulson@3120
    18
consts
paulson@3120
    19
  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
paulson@3120
    20
paulson@3120
    21
inductive "acc(r)"
paulson@3120
    22
  intrs
paulson@3120
    23
    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
berghofe@5717
    24
  monos     Pow_mono
paulson@3120
    25
nipkow@5273
    26
syntax        termi :: "('a * 'a)set => 'a set"
nipkow@5273
    27
translations "termi r" == "acc(r^-1)"
nipkow@5273
    28
paulson@3120
    29
end