src/HOL/Induct/Acc.thy
author wenzelm
Thu Oct 14 15:05:35 1999 +0200 (1999-10-14)
changeset 7867 2efb66472812
parent 7800 8ee919e42174
child 9101 b643f4d7b9e9
permissions -rw-r--r--
fixed comment;
     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 accessible 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