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;
     1 (*  Title:      HOL/UNITY/AllocBase.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Common declarations for Chandy and Charpentier's Allocator
     7 *)
     8 
     9 AllocBase = Rename + Follows + 
    10 
    11 consts
    12   NbT      :: nat       (*Number of tokens in system*)
    13   Nclients :: nat       (*Number of clients*)
    14 
    15 rules
    16   NbT_pos  "0 < NbT"
    17 
    18 (*This function merely sums the elements of a list*)
    19 consts tokens     :: nat list => nat
    20 primrec 
    21   "tokens [] = 0"
    22   "tokens (x#xs) = x + tokens xs"
    23 
    24 consts
    25   bag_of :: 'a list => 'a multiset
    26 
    27 primrec
    28   "bag_of []     = {#}"
    29   "bag_of (x#xs) = {#x#} + bag_of xs"
    30 
    31 end