src/HOL/UNITY/Comp/AllocBase.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,31 @@
+(*  Title:      HOL/UNITY/AllocBase.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Common declarations for Chandy and Charpentier's Allocator
+*)
+
+AllocBase = Rename + Follows + 
+
+consts
+  NbT      :: nat       (*Number of tokens in system*)
+  Nclients :: nat       (*Number of clients*)
+
+rules
+  NbT_pos  "0 < NbT"
+
+(*This function merely sums the elements of a list*)
+consts tokens     :: nat list => nat
+primrec 
+  "tokens [] = 0"
+  "tokens (x#xs) = x + tokens xs"
+
+consts
+  bag_of :: 'a list => 'a multiset
+
+primrec
+  "bag_of []     = {#}"
+  "bag_of (x#xs) = {#x#} + bag_of xs"
+
+end