# HG changeset patch
# User paulson
# Date 959077898 -7200
# Node ID 1d3bf47a4ecc846efbe172c2fdd80bcb369b7309
# Parent  1cf815412d78da2f2f1aca86eef6b01e134f0a9f
new files for the Allocator

diff -r 1cf815412d78 -r 1d3bf47a4ecc src/HOL/UNITY/AllocBase.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/AllocBase.ML	Tue May 23 12:31:38 2000 +0200
@@ -0,0 +1,24 @@
+(*  Title:      HOL/UNITY/AllocBase
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Basis declarations for Chandy and Charpentier's Allocator
+*)
+
+Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (dres_inst_tac [("x","n")] spec 1);
+by Auto_tac;
+by (arith_tac 1);
+qed_spec_mp "sum_mono";
+
+Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
+by (induct_tac "ys" 1);
+by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
+qed_spec_mp "tokens_mono_prefix";
+
+Goalw [mono_def] "mono tokens";
+by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
+qed "mono_tokens";
diff -r 1cf815412d78 -r 1d3bf47a4ecc src/HOL/UNITY/AllocBase.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/AllocBase.thy	Tue May 23 12:31:38 2000 +0200
@@ -0,0 +1,24 @@
+(*  Title:      HOL/UNITY/AllocBase
+    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"
+
+end