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