src/HOL/Induct/Acc.thy
author wenzelm
Mon Aug 14 18:13:14 2000 +0200 (2000-08-14)
changeset 9596 6d6bf351b2cc
parent 9101 b643f4d7b9e9
child 9802 adda1dc18bb8
permissions -rw-r--r--
intros;
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@9101
    12
header {* The accessible part of a relation *}
wenzelm@7759
    13
wenzelm@9101
    14
theory Acc = Main:
paulson@3120
    15
paulson@3120
    16
consts
wenzelm@9101
    17
  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
paulson@3120
    18
berghofe@7721
    19
inductive "acc r"
wenzelm@9596
    20
  intros
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