equal
deleted
inserted
replaced
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 types 'a state = "nat * 'a" (*second component allows new variables*) |
|
12 |
|
13 constdefs |
|
14 count :: "'a state => nat" |
|
15 "count s == fst s" |
|
16 |
|
17 decr :: "('a state * 'a state) set" |
|
18 "decr == UN n uu. {((Suc n, uu), (n,uu))}" |
|
19 |
|
20 Timer :: 'a state program |
|
21 "Timer == mk_program (UNIV, {decr}, UNIV)" |
|
22 |
|
23 end |
|