author | paulson |
Mon, 06 Aug 2001 16:43:40 +0200 | |
changeset 11467 | 1064effe37f6 |
parent 11195 | 65ede8dfe304 |
child 11701 | 3d51fbf81c17 |
permissions | -rw-r--r-- |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Network |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
The Communication Network |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
Goalw [stable_def] |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
"[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
\ !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
\ !! m proc. F : stable {s. m <= s(proc,Sent)}; \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
\ !! n proc. F : stable {s. n <= s(proc,Rcvd)}; \ |
11467 | 17 |
\ !! m proc. F : {s. s(proc,Idle) = 1' & s(proc,Rcvd) = m} co \ |
18 |
\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1'}; \ |
|
19 |
\ !! n proc. F : {s. s(proc,Idle) = 1' & s(proc,Sent) = n} co \ |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
\ {s. s(proc,Sent) = n} \ |
11467 | 21 |
\ |] ==> F : stable {s. s(Aproc,Idle) = 1' & s(Bproc,Idle) = 1' & \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
\ s(Aproc,Sent) = s(Bproc,Rcvd) & \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
\ s(Bproc,Sent) = s(Aproc,Rcvd) & \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
\ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
val rs_AB = [rsA, rsB] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
38 |
val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
42 |
val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
by (rtac constrainsI 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
45 |
by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
46 |
by (assume_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
47 |
by (ALLGOALS Asm_full_simp_tac); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
by (blast_tac (HOL_cs addIs [order_refl]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
by (Clarify_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)", |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
51 |
"s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
52 |
by (REPEAT |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
53 |
(blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
54 |
by (Asm_simp_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
55 |
result(); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
56 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
57 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
58 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
59 |