src/HOL/Induct/Acc.thy
author berghofe
Tue Jun 30 20:51:15 1998 +0200 (1998-06-30)
changeset 5102 8c782c25a11e
parent 3120 c58423c20740
child 5273 70f478d55606
permissions -rw-r--r--
Adapted to new inductive definition package.
     1 (*  Title:      HOL/ex/Acc.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Inductive definition of acc(r)
     7 
     8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
     9 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    10 *)
    11 
    12 Acc = WF + Inductive +
    13 
    14 constdefs
    15   pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
    16   "pred x r == {y. (y,x):r}"
    17 
    18 consts
    19   acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
    20 
    21 inductive "acc(r)"
    22   intrs
    23     pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
    24   monos     "[Pow_mono]"
    25 
    26 end