1(*  Title:      HOL/UNITY/Simple/Network.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5The Communication Network.
6
7From Misra, "A Logic for Concurrent Programming" (1994), section 5.7.
8*)
9
10theory Network imports "../UNITY" begin
11
12(*The state assigns a number to each process variable*)
13
14datatype pvar = Sent | Rcvd | Idle
15
16datatype pname = Aproc | Bproc
17
18type_synonym state = "pname * pvar => nat"
19
20locale F_props =
21  fixes F 
22  assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}"
23      and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}"
24    and sent_nondec: "F \<in> stable {s. m \<le> s(proc,Sent)}"
25    and rcvd_nondec: "F \<in> stable {s. n \<le> s(proc,Rcvd)}"
26    and rcvd_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m}
27                        co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}"
28    and sent_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n}
29                        co {s. s(proc,Sent) = n}"
30begin
31
32lemmas sent_nondec_A = sent_nondec [of _ Aproc]
33    and sent_nondec_B = sent_nondec [of _ Bproc]
34    and rcvd_nondec_A = rcvd_nondec [of _ Aproc]
35    and rcvd_nondec_B = rcvd_nondec [of _ Bproc]
36    and rcvd_idle_A = rcvd_idle [of Aproc]
37    and rcvd_idle_B = rcvd_idle [of Bproc]
38    and sent_idle_A = sent_idle [of Aproc]
39    and sent_idle_B = sent_idle [of Bproc]
40
41    and rs_AB = stable_Int [OF rsA rsB]
42
43lemmas sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B]
44    and rcvd_nondec_AB = stable_Int [OF rcvd_nondec_A rcvd_nondec_B]
45    and rcvd_idle_AB = constrains_Int [OF rcvd_idle_A rcvd_idle_B]
46    and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B]
47
48lemmas nondec_AB = stable_Int [OF sent_nondec_AB rcvd_nondec_AB]
49    and idle_AB = constrains_Int [OF rcvd_idle_AB sent_idle_AB]
50
51lemmas nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def] idle_AB]
52
53lemma
54  shows "F \<in> stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 &  
55                        s(Aproc,Sent) = s(Bproc,Rcvd) &  
56                        s(Bproc,Sent) = s(Aproc,Rcvd) &  
57                        s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}"
58apply (unfold stable_def) 
59apply (rule constrainsI)
60apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle, 
61                             THEN constrainsD], assumption)
62apply simp_all
63apply (blast del: le0, clarify) 
64apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)")
65apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)") 
66apply simp 
67apply (blast intro: order_antisym le_trans eq_imp_le)+
68done
69
70end
71
72end
73