src/HOL/UNITY/Comp/Counterc.thy
 author paulson Wed Jan 29 16:34:51 2003 +0100 (2003-01-29) changeset 13792 d1811693899c parent 12338 de0f4a63baa5 child 13812 91713a1915ee permissions -rw-r--r--
converted more UNITY theories to new-style
1 (*  Title:      HOL/UNITY/Counterc
2     ID:         \$Id\$
3     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
4     Copyright   2001  University of Cambridge
6 A family of similar counters, version with a full use of "compatibility "
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 *)
14 Counterc =  UNITY_Main +
16 types state
17 arities state :: type
19 consts
20   C :: "state=>int"
21   c :: "state=>nat=>int"
23 consts
24   sum  :: "[nat,state]=>int"
25   sumj :: "[nat, nat, state]=>int"
27 primrec (* sum I s = sigma_{i<I}. c s i *)
28   "sum 0 s = 0"
29   "sum (Suc i) s = (c s) i + sum i s"
31 primrec
32   "sumj 0 i s = 0"
33   "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
35 types command = "(state*state)set"
37 constdefs
38   a :: "nat=>command"
39  "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
41   Component :: "nat => state program"
42   "Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i},
43 	       UN G: preserves (%s. (c s) i). Acts G)"
44 end