author | paulson |
Tue, 23 May 2000 12:35:18 +0200 | |
changeset 8931 | ac2aac644b9f |
parent 8251 | 9be357df93d4 |
child 9403 | aad13b59b8d9 |
permissions | -rw-r--r-- |
5636 | 1 |
(* Title: HOL/UNITY/Client.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Distributed Resource Management System: the Client |
|
7 |
*) |
|
8 |
||
8931 | 9 |
Client = Rename + AllocBase + |
5636 | 10 |
|
11 |
types |
|
12 |
tokbag = nat (*tokbags could be multisets...or any ordered type?*) |
|
13 |
||
14 |
record state = |
|
15 |
giv :: tokbag list (*input history: tokens granted*) |
|
16 |
ask :: tokbag list (*output history: tokens requested*) |
|
17 |
rel :: tokbag list (*output history: tokens released*) |
|
18 |
tok :: tokbag (*current token request*) |
|
19 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
20 |
record 'a state_u = |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
21 |
state + |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
22 |
extra :: 'a (*new variables*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
23 |
|
5636 | 24 |
|
25 |
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *) |
|
26 |
||
27 |
constdefs |
|
28 |
||
29 |
(** Release some tokens **) |
|
30 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
31 |
rel_act :: "('a state_u * 'a state_u) set" |
5636 | 32 |
"rel_act == {(s,s'). |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
33 |
EX nrel. nrel = size (rel s) & |
5636 | 34 |
s' = s (| rel := rel s @ [giv s!nrel] |) & |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
35 |
nrel < size (giv s) & |
5636 | 36 |
ask s!nrel <= giv s!nrel}" |
37 |
||
38 |
(** Choose a new token requirement **) |
|
39 |
||
40 |
(** Including s'=s suppresses fairness, allowing the non-trivial part |
|
41 |
of the action to be ignored **) |
|
42 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
43 |
tok_act :: "('a state_u * 'a state_u) set" |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
44 |
"tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
8216 | 45 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
46 |
ask_act :: "('a state_u * 'a state_u) set" |
5636 | 47 |
"ask_act == {(s,s'). s'=s | |
8216 | 48 |
(s' = s (|ask := ask s @ [tok s]|))}" |
5636 | 49 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
50 |
Client :: 'a state_u program |
8216 | 51 |
"Client == mk_program ({s. tok s : atMost NbT & |
52 |
giv s = [] & ask s = [] & rel s = []}, |
|
53 |
{rel_act, tok_act, ask_act})" |
|
5636 | 54 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
55 |
(*Maybe want a special theory section to declare such maps*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
56 |
non_extra :: 'a state_u => state |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
57 |
"non_extra s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
58 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
59 |
(*Renaming map to put a Client into the standard form*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
60 |
client_map :: "'a state_u => state*'a" |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
61 |
"client_map == funPair non_extra extra" |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
62 |
|
5636 | 63 |
end |