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