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