# Theory Network

Up to index of Isabelle/HOL/UNITY

theory Network
imports UNITY
begin

    (*  Title:      HOL/UNITY/Network
        ID:         $Id: Network.thy,v 1.4 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    The Communication Network

    From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
    *)

    theory Network imports UNITY begin

    (*The state assigns a number to each process variable*)

    datatype pvar = Sent | Rcvd | Idle

    datatype pname = Aproc | Bproc

    types state = "pname * pvar => nat"

    locale F_props =
      fixes F
      assumes rsA: "F ∈ stable {s. s(Bproc,Rcvd) ≤ s(Aproc,Sent)}"
          and rsB: "F ∈ stable {s. s(Aproc,Rcvd) ≤ s(Bproc,Sent)}"
        and sent_nondec: "F ∈ stable {s. m ≤ s(proc,Sent)}"
        and rcvd_nondec: "F ∈ stable {s. n ≤ s(proc,Rcvd)}"
        and rcvd_idle: "F ∈ {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m}
                            co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}"
        and sent_idle: "F ∈ {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n}
                            co {s. s(proc,Sent) = n}"

    lemmas (in F_props)
            sent_nondec_A = sent_nondec [of _ Aproc]
        and sent_nondec_B = sent_nondec [of _ Bproc]
        and rcvd_nondec_A = rcvd_nondec [of _ Aproc]
        and rcvd_nondec_B = rcvd_nondec [of _ Bproc]
        and rcvd_idle_A = rcvd_idle [of Aproc]
        and rcvd_idle_B = rcvd_idle [of Bproc]
        and sent_idle_A = sent_idle [of Aproc]
        and sent_idle_B = sent_idle [of Bproc]

        and rs_AB = stable_Int [OF rsA rsB]
        and sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B]
        and rcvd_nondec_AB = stable_Int [OF rcvd_nondec_A rcvd_nondec_B]
        and rcvd_idle_AB = constrains_Int [OF rcvd_idle_A rcvd_idle_B]
        and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B]
        and nondec_AB = stable_Int [OF sent_nondec_AB rcvd_nondec_AB]
        and idle_AB = constrains_Int [OF rcvd_idle_AB sent_idle_AB]
        and nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def]
                                             idle_AB]

    lemma (in F_props)
      shows "F ∈ stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 &
                            s(Aproc,Sent) = s(Bproc,Rcvd) &
                            s(Bproc,Sent) = s(Aproc,Rcvd) &
                            s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}"
    apply (unfold stable_def)
    apply (rule constrainsI)
    apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle,
                                 THEN constrainsD], assumption)
    apply simp_all
    apply (blast del: le0, clarify)
    apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)")
    apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)")
    apply simp
    apply (blast intro: order_antisym le_trans eq_imp_le)+
    done

    end

lemmas sent_nondec_A:

      F_props F ==> F ∈ stable {s. m ≤ s (Aproc, Sent)}

and sent_nondec_B:

      F_props F ==> F ∈ stable {s. m ≤ s (Bproc, Sent)}

and rcvd_nondec_A:

      F_props F ==> F ∈ stable {s. n ≤ s (Aproc, Rcvd)}

and rcvd_nondec_B:

      F_props F ==> F ∈ stable {s. n ≤ s (Bproc, Rcvd)}

and rcvd_idle_A:

      F_props F
      ==> F ∈ {s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Rcvd) = m} co
              {s. s (Aproc, Rcvd) = m --> s (Aproc, Idle) = Suc 0}

and rcvd_idle_B:

      F_props F
      ==> F ∈ {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Rcvd) = m} co
              {s. s (Bproc, Rcvd) = m --> s (Bproc, Idle) = Suc 0}

and sent_idle_A:

      F_props F
      ==> F ∈ {s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Sent) = n} co
              {s. s (Aproc, Sent) = n}

and sent_idle_B:

      F_props F
      ==> F ∈ {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Sent) = n} co
              {s. s (Bproc, Sent) = n}

and rs_AB:

      F_props F
      ==> F ∈ stable
               ({s. s (Bproc, Rcvd) ≤ s (Aproc, Sent)} ∩
                {s. s (Aproc, Rcvd) ≤ s (Bproc, Sent)})

and sent_nondec_AB:

      F_props F ==> F ∈ stable ({s. ma ≤ s (Aproc, Sent)} ∩ {s. m ≤ s (Bproc, Sent)})

and rcvd_nondec_AB:

      F_props F ==> F ∈ stable ({s. na ≤ s (Aproc, Rcvd)} ∩ {s. n ≤ s (Bproc, Rcvd)})

and rcvd_idle_AB:

      F_props F
      ==> F ∈ {s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Rcvd) = ma} ∩
              {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Rcvd) = m} co
              {s. s (Aproc, Rcvd) = ma --> s (Aproc, Idle) = Suc 0} ∩
              {s. s (Bproc, Rcvd) = m --> s (Bproc, Idle) = Suc 0}

and sent_idle_AB:

      F_props F
      ==> F ∈ {s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Sent) = na} ∩
              {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Sent) = n} co
              {s. s (Aproc, Sent) = na} ∩ {s. s (Bproc, Sent) = n}

and nondec_AB:

      F_props F
      ==> F ∈ stable
               ({s. ma ≤ s (Aproc, Sent)} ∩ {s. m ≤ s (Bproc, Sent)} ∩
                ({s. na ≤ s (Aproc, Rcvd)} ∩ {s. n ≤ s (Bproc, Rcvd)}))

and idle_AB:

      F_props F
      ==> F ∈ {s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Rcvd) = ma} ∩
              {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Rcvd) = m} ∩
              ({s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Sent) = na} ∩
               {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Sent) = n}) co
              {s. s (Aproc, Rcvd) = ma --> s (Aproc, Idle) = Suc 0} ∩
              {s. s (Bproc, Rcvd) = m --> s (Bproc, Idle) = Suc 0} ∩
              ({s. s (Aproc, Sent) = na} ∩ {s. s (Bproc, Sent) = n})

and nondec_idle:

      F_props F
      ==> F ∈ {s. mc ≤ s (Aproc, Sent)} ∩ {s. mb ≤ s (Bproc, Sent)} ∩
              ({s. nc ≤ s (Aproc, Rcvd)} ∩ {s. nb ≤ s (Bproc, Rcvd)}) ∩
              ({s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Rcvd) = ma} ∩
               {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Rcvd) = m} ∩
               ({s. s (Aproc, Idle) = Suc 0 ∧ s (Aproc, Sent) = na} ∩
                {s. s (Bproc, Idle) = Suc 0 ∧ s (Bproc, Sent) = n})) co
              {s. mc ≤ s (Aproc, Sent)} ∩ {s. mb ≤ s (Bproc, Sent)} ∩
              ({s. nc ≤ s (Aproc, Rcvd)} ∩ {s. nb ≤ s (Bproc, Rcvd)}) ∩
              ({s. s (Aproc, Rcvd) = ma --> s (Aproc, Idle) = Suc 0} ∩
               {s. s (Bproc, Rcvd) = m --> s (Bproc, Idle) = Suc 0} ∩
               ({s. s (Aproc, Sent) = na} ∩ {s. s (Bproc, Sent) = n}))

lemma

      F_props F
      ==> F ∈ stable
               {s. s (Aproc, Idle) = Suc 0 ∧
                   s (Bproc, Idle) = Suc 0 ∧
                   s (Aproc, Sent) = s (Bproc, Rcvd) ∧
                   s (Bproc, Sent) = s (Aproc, Rcvd) ∧
                   s (Aproc, Rcvd) = m ∧ s (Bproc, Rcvd) = n}