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