src/HOL/Induct/Acc.thy
author berghofe
Tue Oct 05 15:31:42 1999 +0200 (1999-10-05)
changeset 7721 cb353d802ade
parent 5717 0d28dbe484b6
child 7759 44dd5dc8e90f
permissions -rw-r--r--
Tuned inductive definition.
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
berghofe@7721
    12
theory Acc = WF + Inductive:
paulson@3120
    13
paulson@3120
    14
consts
paulson@3120
    15
  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
paulson@3120
    16
berghofe@7721
    17
inductive "acc r"
paulson@3120
    18
  intrs
berghofe@7721
    19
    accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
berghofe@7721
    20
paulson@3120
    21
nipkow@5273
    22
syntax        termi :: "('a * 'a)set => 'a set"
nipkow@5273
    23
translations "termi r" == "acc(r^-1)"
nipkow@5273
    24
paulson@3120
    25
end