src/HOL/UNITY/Comp/Counterc.thy
 author paulson Sat Feb 08 16:05:33 2003 +0100 (2003-02-08) changeset 13812 91713a1915ee parent 13792 d1811693899c child 14088 61bd46feb919 permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
```     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 =  UNITY_Main +
```
```    15
```
```    16 types state
```
```    17 arities state :: type
```
```    18
```
```    19 consts
```
```    20   C :: "state=>int"
```
```    21   c :: "state=>nat=>int"
```
```    22
```
```    23 consts
```
```    24   sum  :: "[nat,state]=>int"
```
```    25   sumj :: "[nat, nat, state]=>int"
```
```    26
```
```    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"
```
```    30
```
```    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)"
```
```    34
```
```    35 types command = "(state*state)set"
```
```    36
```
```    37 constdefs
```
```    38   a :: "nat=>command"
```
```    39  "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
```
```    40
```
```    41   Component :: "nat => state program"
```
```    42   "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
```
```    43 				   {a i},
```
```    44  	                           \\<Union>G \\<in> preserves (%s. (c s) i). Acts G)"
```
```    45 end
```