| author | berghofe |
| Thu, 07 Oct 1999 15:40:32 +0200 | |
| changeset 7786 | cf9d07ad62af |
| parent 7537 | 875754b599df |
| child 8251 | 9be357df93d4 |
| permissions | -rw-r--r-- |
| 7513 | 1 |
(* Title: HOL/UNITY/TimerArray.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
A trivial example of reasoning about an array of processes |
|
7 |
*) |
|
8 |
||
9 |
TimerArray = PPROD + |
|
10 |
||
11 |
constdefs |
|
| 7537 | 12 |
decr :: "(nat*nat) set" |
13 |
"decr == UN n. {(Suc n, n)}"
|
|
14 |
||
| 7513 | 15 |
Timer :: nat program |
| 7537 | 16 |
"Timer == mk_program (UNIV, {decr})"
|
| 7513 | 17 |
|
18 |
end |