src/HOL/UNITY/AllocBase.thy
author paulson
Fri Jul 14 14:47:15 2000 +0200 (2000-07-14)
changeset 9336 9ae89b9ce206
parent 9109 0085c32a533b
child 10265 4e004b548049
permissions -rw-r--r--
moved sublist from UNITY/AllocBase to List
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@8989
     7
paulson@9024
     8
add_path "../Induct";
paulson@9024
     9
time_use_thy "AllocBase";
paulson@8928
    10
*)
paulson@8928
    11
paulson@9024
    12
AllocBase = Rename + Follows + 
paulson@8928
    13
paulson@8928
    14
consts
paulson@8928
    15
  NbT      :: nat       (*Number of tokens in system*)
paulson@8928
    16
  Nclients :: nat       (*Number of clients*)
paulson@8928
    17
paulson@8928
    18
rules
paulson@8928
    19
  NbT_pos  "0 < NbT"
paulson@8928
    20
paulson@8928
    21
(*This function merely sums the elements of a list*)
paulson@8928
    22
consts tokens     :: nat list => nat
paulson@8928
    23
primrec 
paulson@8928
    24
  "tokens [] = 0"
paulson@8928
    25
  "tokens (x#xs) = x + tokens xs"
paulson@8928
    26
paulson@9024
    27
consts
paulson@9024
    28
  bag_of :: 'a list => 'a multiset
paulson@9024
    29
paulson@9024
    30
primrec
paulson@9024
    31
  "bag_of []     = {#}"
paulson@9024
    32
  "bag_of (x#xs) = {#x#} + bag_of xs"
paulson@9024
    33
paulson@8928
    34
end