src/HOL/UNITY/AllocBase.thy
author wenzelm
Wed Oct 18 23:42:18 2000 +0200 (2000-10-18)
changeset 10265 4e004b548049
parent 9336 9ae89b9ce206
permissions -rw-r--r--
use Multiset from HOL/Library;
wenzelm@10265
     1
(*  Title:      HOL/UNITY/AllocBase.thy
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@9024
     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@9024
    24
consts
paulson@9024
    25
  bag_of :: 'a list => 'a multiset
paulson@9024
    26
paulson@9024
    27
primrec
paulson@9024
    28
  "bag_of []     = {#}"
paulson@9024
    29
  "bag_of (x#xs) = {#x#} + bag_of xs"
paulson@9024
    30
paulson@8928
    31
end