src/HOL/UNITY/Network.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
     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 open Network;
    12 
    13 val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = 
    14 goalw thy [stable_def]
    15    "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
    16 \      !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
    17 \      !! m proc. stable Acts {s. m <= s(proc,Sent)};  \
    18 \      !! n proc. stable Acts {s. n <= s(proc,Rcvd)};  \
    19 \      !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
    20 \                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
    21 \      !! n proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
    22 \                                 {s. s(proc,Sent) = n} \
    23 \   |] ==> stable Acts {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
    24 \                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
    25 \                         s(Bproc,Sent) = s(Aproc,Rcvd) & \
    26 \                         s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
    27 
    28 val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec;
    29 val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec;
    30 val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec;
    31 val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec;
    32 val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle;
    33 val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle;
    34 val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle;
    35 val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle;
    36 
    37 val rs_AB = [rsA, rsB] MRS constrains_Int;
    38 val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int;
    39 val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int;
    40 val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int;
    41 val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int;
    42 val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int;
    43 val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int;
    44 val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int;
    45 
    46 by (rtac constrainsI 1);
    47 by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
    48 by (assume_tac 1);
    49 by (ALLGOALS Asm_full_simp_tac);
    50 by (Blast_tac 1);
    51 by (Clarify_tac 1);
    52 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
    53 		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
    54 by (REPEAT (blast_tac (claset() addIs [le_anti_sym, le_trans, eq_imp_le]) 2));
    55 
    56 by (Asm_simp_tac 1);
    57 result();
    58 
    59 
    60 
    61