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;
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
wenzelm@7800
    21
    accI [rulify_prems]:
wenzelm@7800
    22
      "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
paulson@3120
    23
wenzelm@7800
    24
syntax
wenzelm@7800
    25
  termi :: "('a * 'a)set => 'a set"
wenzelm@7800
    26
translations
wenzelm@7800
    27
  "termi r" == "acc(r^-1)"
nipkow@5273
    28
paulson@3120
    29
end