src/HOL/UNITY/Simple/Network.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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 theory Network imports UNITY begin
    12 
    13 (*The state assigns a number to each process variable*)
    14 
    15 datatype pvar = Sent | Rcvd | Idle
    16 
    17 datatype pname = Aproc | Bproc
    18 
    19 types state = "pname * pvar => nat"
    20 
    21 locale F_props =
    22   fixes F 
    23   assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}"
    24       and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}"
    25     and sent_nondec: "F \<in> stable {s. m \<le> s(proc,Sent)}"
    26     and rcvd_nondec: "F \<in> stable {s. n \<le> s(proc,Rcvd)}"
    27     and rcvd_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m}
    28                         co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}"
    29     and sent_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n}
    30                         co {s. s(proc,Sent) = n}"
    31   
    32 
    33 lemmas (in F_props) 
    34         sent_nondec_A = sent_nondec [of _ Aproc]
    35     and sent_nondec_B = sent_nondec [of _ Bproc]
    36     and rcvd_nondec_A = rcvd_nondec [of _ Aproc]
    37     and rcvd_nondec_B = rcvd_nondec [of _ Bproc]
    38     and rcvd_idle_A = rcvd_idle [of Aproc]
    39     and rcvd_idle_B = rcvd_idle [of Bproc]
    40     and sent_idle_A = sent_idle [of Aproc]
    41     and sent_idle_B = sent_idle [of Bproc]
    42 
    43     and rs_AB = stable_Int [OF rsA rsB]
    44     and sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B]
    45     and rcvd_nondec_AB = stable_Int [OF rcvd_nondec_A rcvd_nondec_B]
    46     and rcvd_idle_AB = constrains_Int [OF rcvd_idle_A rcvd_idle_B]
    47     and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B]
    48     and 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     and nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def] 
    51                                          idle_AB]
    52 
    53 lemma (in F_props)
    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}"
    58 apply (unfold stable_def) 
    59 apply (rule constrainsI)
    60 apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle, 
    61                              THEN constrainsD], assumption)
    62 apply simp_all
    63 apply (blast del: le0, clarify) 
    64 apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)")
    65 apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)") 
    66 apply simp 
    67 apply (blast intro: order_antisym le_trans eq_imp_le)+
    68 done
    69 
    70 end