src/HOL/UNITY/AllocBase.thy
author paulson
Tue May 23 12:31:38 2000 +0200 (2000-05-23)
changeset 8928 1d3bf47a4ecc
child 8974 a76f80911eb9
permissions -rw-r--r--
new files for the Allocator
paulson@8928
     1
(*  Title:      HOL/UNITY/AllocBase
paulson@8928
     2
    ID:         $Id$
paulson@8928
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8928
     4
    Copyright   1998  University of Cambridge
paulson@8928
     5
paulson@8928
     6
Common declarations for Chandy and Charpentier's Allocator
paulson@8928
     7
*)
paulson@8928
     8
paulson@8928
     9
AllocBase = Rename + Follows + 
paulson@8928
    10
paulson@8928
    11
consts
paulson@8928
    12
  NbT      :: nat       (*Number of tokens in system*)
paulson@8928
    13
  Nclients :: nat       (*Number of clients*)
paulson@8928
    14
paulson@8928
    15
rules
paulson@8928
    16
  NbT_pos  "0 < NbT"
paulson@8928
    17
paulson@8928
    18
(*This function merely sums the elements of a list*)
paulson@8928
    19
consts tokens     :: nat list => nat
paulson@8928
    20
primrec 
paulson@8928
    21
  "tokens [] = 0"
paulson@8928
    22
  "tokens (x#xs) = x + tokens xs"
paulson@8928
    23
paulson@8928
    24
end