src/HOL/Induct/Acc.thy
author wenzelm
Wed Jun 21 18:09:09 2000 +0200 (2000-06-21)
changeset 9101 b643f4d7b9e9
parent 7867 2efb66472812
child 9596 6d6bf351b2cc
permissions -rw-r--r--
fixed deps;
     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 = Main:
    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