src/HOL/ex/Acc.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1570 fd1b9c721ac7
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1266
diff changeset
     1
(*  Title:      HOL/ex/Acc.thy
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1266
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     6
Inductive definition of acc(r)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     7
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    10
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    11
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    12
Acc = WF + 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    13
1570
fd1b9c721ac7 added constdefs section
clasohm
parents: 1476
diff changeset
    14
constdefs
fd1b9c721ac7 added constdefs section
clasohm
parents: 1476
diff changeset
    15
  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
fd1b9c721ac7 added constdefs section
clasohm
parents: 1476
diff changeset
    16
  "pred x r == {y. (y,x):r}"
fd1b9c721ac7 added constdefs section
clasohm
parents: 1476
diff changeset
    17
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    18
consts
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1266
diff changeset
    19
  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
inductive "acc(r)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
  intrs
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    23
    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    24
  monos     "[Pow_mono]"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    25
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    26
end