src/ZF/ex/Acc.thy
author paulson
Wed Jan 13 15:14:47 1999 +0100 (1999-01-13)
changeset 6117 f9aad8ccd590
parent 1478 2b8c2a7547ab
child 11316 b4e71bd751e4
permissions -rw-r--r--
tidying of datatype and inductive definitions
clasohm@1478
     1
(*  Title:      ZF/ex/Acc.thy
lcp@515
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Inductive definition of acc(r)
lcp@515
     7
lcp@515
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
lcp@515
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
lcp@515
    10
*)
lcp@515
    11
lcp@809
    12
Acc = WF + Inductive +
lcp@515
    13
lcp@515
    14
consts
clasohm@1401
    15
  acc :: i=>i
lcp@515
    16
lcp@515
    17
inductive
lcp@515
    18
  domains "acc(r)" <= "field(r)"
lcp@515
    19
  intrs
lcp@515
    20
    vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
paulson@6117
    21
  monos      Pow_mono
lcp@515
    22
lcp@515
    23
end