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