Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
to their abstract counterparts, while other binary numerals work correctly.
(* Title: HOL/UNITY/Counterc
ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
A family of similar counters, version with a full use of "compatibility "
From Charpentier and Chandy,
Examples of Program Composition Illustrating the Use of Universal Properties
In J. Rolim (editor), Parallel and Distributed Processing,
Spriner LNCS 1586 (1999), pages 1215-1227.
*)
Counterc = Comp +
types state
arities state :: term
consts
C :: "state=>int"
c :: "state=>nat=>int"
consts
sum :: "[nat,state]=>int"
sumj :: "[nat, nat, state]=>int"
primrec (* sum I s = sigma_{i<I}. c s i *)
"sum 0 s = 0"
"sum (Suc i) s = (c s) i + sum i s"
primrec
"sumj 0 i s = 0"
"sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
types command = "(state*state)set"
constdefs
a :: "nat=>command"
"a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
Component :: "nat => state program"
"Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i},
UN G: preserves (%s. (c s) i). Acts G)"
end