|
10782
|
1 |
(* Title: HOL/UNITY/Counterc
|
|
|
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 with a full use of "compatibility "
|
|
|
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 |
Counterc = Comp +
|
|
|
15 |
types state
|
|
|
16 |
arities state :: term
|
|
|
17 |
|
|
|
18 |
consts
|
|
|
19 |
C :: "state=>int"
|
|
|
20 |
c :: "state=>nat=>int"
|
|
|
21 |
|
|
|
22 |
consts
|
|
|
23 |
sum :: "[nat,state]=>int"
|
|
|
24 |
sumj :: "[nat, nat, state]=>int"
|
|
|
25 |
|
|
|
26 |
primrec (* sum I s = sigma_{i<I}. c s i *)
|
|
|
27 |
"sum 0 s = #0"
|
|
|
28 |
"sum (Suc i) s = (c s) i + sum i s"
|
|
|
29 |
|
|
|
30 |
primrec
|
|
|
31 |
"sumj 0 i s = #0"
|
|
|
32 |
"sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
|
|
|
33 |
|
|
|
34 |
types command = "(state*state)set"
|
|
|
35 |
|
|
|
36 |
constdefs
|
|
|
37 |
a :: "nat=>command"
|
|
|
38 |
"a i == {(s, s'). (c s') i = (c s) i + #1 & (C s') = (C s) + #1}"
|
|
|
39 |
|
|
|
40 |
Component :: "nat => state program"
|
|
|
41 |
"Component i == mk_program({s. C s = #0 & (c s) i = #0}, {a i},
|
|
|
42 |
UN G: preserves (%s. (c s) i). Acts G)"
|
|
|
43 |
end
|