--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Counter.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/UNITY/Counter
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version close to the original.
+
+From Charpentier and Chandy,
+Examples of Program Composition Illustrating the Use of Universal Properties
+ In J. Rolim (editor), Parallel and Distributed Processing,
+ Spriner LNCS 1586 (1999), pages 1215-1227.
+*)
+
+Counter = Comp +
+(* Variables are names *)
+datatype name = C | c nat
+types state = name=>int
+
+consts
+ sum :: "[nat,state]=>int"
+ sumj :: "[nat, nat, state]=>int"
+
+primrec (* sum I s = sigma_{i<I}. s (c i) *)
+ "sum 0 s = #0"
+ "sum (Suc i) s = s (c i) + sum i s"
+
+primrec
+ "sumj 0 i s = #0"
+ "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
+
+types command = "(state*state)set"
+
+constdefs
+ a :: "nat=>command"
+ "a i == {(s, s'). s'=s(c i:= s (c i) + #1, C:= s C + #1)}"
+
+ Component :: "nat => state program"
+ "Component i ==
+ mk_program({s. s C = #0 & s (c i) = #0}, {a i},
+ UN G: preserves (%s. s (c i)). Acts G)"
+end