src/HOL/Induct/Acc.thy
author berghofe
Fri, 24 Jul 1998 13:39:47 +0200
changeset 5191 8ceaa19f7717
parent 5102 8c782c25a11e
child 5273 70f478d55606
permissions -rw-r--r--
Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Acc.thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
Inductive definition of acc(r)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
5102
8c782c25a11e Adapted to new inductive definition package.
berghofe
parents: 3120
diff changeset
    12
Acc = WF + Inductive +
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
constdefs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
  "pred x r == {y. (y,x):r}"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
consts
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
inductive "acc(r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
  intrs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
  monos     "[Pow_mono]"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
end