src/HOL/UNITY/AllocBase.thy
author paulson
Fri Jun 02 17:48:17 2000 +0200 (2000-06-02)
changeset 9024 b1f37f6819c4
parent 8989 8791e3304748
child 9109 0085c32a533b
permissions -rw-r--r--
new constant bag_of
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@8974
    27
(*Or could be setsum...(lessThan n)*)
paulson@8974
    28
consts sum_below :: "[nat=>'a, nat] => ('a::plus_ac0)"
paulson@8974
    29
primrec 
paulson@8974
    30
  sum_below_0    "sum_below f 0 = 0"
paulson@8974
    31
  sum_below_Suc  "sum_below f (Suc n) = f(n) + sum_below f n"
paulson@8974
    32
paulson@8989
    33
constdefs sublist :: "['a list, nat set] => 'a list"
paulson@8989
    34
    "sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))"
paulson@8989
    35
paulson@9024
    36
paulson@9024
    37
consts
paulson@9024
    38
  bag_of :: 'a list => 'a multiset
paulson@9024
    39
paulson@9024
    40
primrec
paulson@9024
    41
  "bag_of []     = {#}"
paulson@9024
    42
  "bag_of (x#xs) = {#x#} + bag_of xs"
paulson@9024
    43
paulson@8928
    44
end