src/HOL/UNITY/Comp/AllocBase.thy

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp

(*  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