src/HOL/Induct/Acc.thy
author wenzelm
Fri Oct 08 15:09:14 1999 +0200 (1999-10-08)
changeset 7800 8ee919e42174
parent 7759 44dd5dc8e90f
child 7867 2efb66472812
permissions -rw-r--r--
improved presentation;
     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 header {* The acessible part of a relation *};
    13 
    14 theory Acc = WF + Inductive:;
    15 
    16 consts
    17   acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *};
    18 
    19 inductive "acc r"
    20   intrs
    21     accI [rulify_prems]:
    22       "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    23 
    24 syntax
    25   termi :: "('a * 'a)set => 'a set"
    26 translations
    27   "termi r" == "acc(r^-1)"
    28 
    29 end