|
10782
|
1 |
(* Title: HOL/UNITY/Counter
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 2001 University of Cambridge
|
|
|
5 |
|
|
|
6 |
A family of similar counters, version close to the original.
|
|
|
7 |
|
|
|
8 |
From Charpentier and Chandy,
|
|
|
9 |
Examples of Program Composition Illustrating the Use of Universal Properties
|
|
|
10 |
In J. Rolim (editor), Parallel and Distributed Processing,
|
|
|
11 |
Spriner LNCS 1586 (1999), pages 1215-1227.
|
|
|
12 |
*)
|
|
|
13 |
|
|
|
14 |
Counter = Comp +
|
|
|
15 |
(* Variables are names *)
|
|
|
16 |
datatype name = C | c nat
|
|
|
17 |
types state = name=>int
|
|
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
sum :: "[nat,state]=>int"
|
|
|
21 |
sumj :: "[nat, nat, state]=>int"
|
|
|
22 |
|
|
|
23 |
primrec (* sum I s = sigma_{i<I}. s (c i) *)
|
|
|
24 |
"sum 0 s = #0"
|
|
|
25 |
"sum (Suc i) s = s (c i) + sum i s"
|
|
|
26 |
|
|
|
27 |
primrec
|
|
|
28 |
"sumj 0 i s = #0"
|
|
|
29 |
"sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
|
|
|
30 |
|
|
|
31 |
types command = "(state*state)set"
|
|
|
32 |
|
|
|
33 |
constdefs
|
|
|
34 |
a :: "nat=>command"
|
|
|
35 |
"a i == {(s, s'). s'=s(c i:= s (c i) + #1, C:= s C + #1)}"
|
|
|
36 |
|
|
|
37 |
Component :: "nat => state program"
|
|
|
38 |
"Component i ==
|
|
|
39 |
mk_program({s. s C = #0 & s (c i) = #0}, {a i},
|
|
|
40 |
UN G: preserves (%s. s (c i)). Acts G)"
|
|
|
41 |
end
|