src/ZF/ex/Acc.thy
author clasohm
Tue, 06 Feb 1996 12:27:17 +0100
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6117 f9aad8ccd590
permissions -rw-r--r--
expanded tabs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/ex/Acc.thy
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     5
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     6
Inductive definition of acc(r)
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     7
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    10
*)
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    11
809
1daa0269eb5d removed quotes around "Inductive"
lcp
parents: 578
diff changeset
    12
Acc = WF + Inductive +
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    13
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    14
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 809
diff changeset
    15
  acc :: i=>i
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    16
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    17
inductive
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    18
  domains "acc(r)" <= "field(r)"
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    19
  intrs
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    20
    vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    21
  monos     "[Pow_mono]"
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    22
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    23
end