| author | wenzelm |
| Sat, 24 Nov 2001 17:21:47 +0100 | |
| changeset 12294 | 2ef49890aede |
| parent 11194 | ea13ff5a26d1 |
| child 13786 | ab8f39f48a6f |
| permissions | -rw-r--r-- |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Handshake.thy |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
Handshake Protocol |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
*) |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
Handshake = Union + |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
record state = |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
BB :: bool |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
NF :: nat |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
NG :: nat |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
constdefs |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
(*F's program*) |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
cmdF :: "(state*state) set" |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
"cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
F :: "state program" |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
"F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
(*G's program*) |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
cmdG :: "(state*state) set" |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
"cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
G :: "state program" |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
"G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
(*the joint invariant*) |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
invFG :: "state set" |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
"invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
|
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
end |