Theory AWN

(*  Title:       AWN.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Terms of the Algebra for Wireless Networks"

theory AWN
imports Lib
begin

subsection "Sequential Processes"

type_synonym ip = nat
type_synonym data = nat

text ‹
  Most of AWN is independent of the type of messages, but the closed layer turns
  newpkt actions into the arrival of newpkt messages. We use a type class to maintain
  some abstraction (and independence from the definition of particular protocols).
›

class msg =
  fixes newpkt :: "data × ip ⇒ 'a"
    and eq_newpkt :: "'a ⇒ bool"
  assumes eq_newpkt_eq [simp]: "eq_newpkt (newpkt (d, i))"

text ‹
  Sequential process terms abstract over the types of data states (@{typ 's}),
  messages (@{typ 'm}), process names (@{typ 'p}),and labels (@{typ 'l}).
›

datatype (dead 's, dead 'm, dead 'p, 'l) seqp =
    GUARD "'l" "'s ⇒ 's set" "('s, 'm, 'p, 'l) seqp"
  | ASSIGN "'l" "'s ⇒ 's" "('s, 'm, 'p, 'l) seqp"
  | CHOICE "('s, 'm, 'p, 'l) seqp" "('s, 'm, 'p, 'l) seqp"
  | UCAST "'l" "'s ⇒ ip" "'s ⇒ 'm" "('s, 'm, 'p, 'l) seqp" "('s, 'm, 'p, 'l) seqp"
  | BCAST "'l" "'s ⇒ 'm" "('s, 'm, 'p, 'l) seqp"
  | GCAST "'l" "'s ⇒ ip set" "'s ⇒ 'm" "('s, 'm, 'p, 'l) seqp"
  | SEND "'l" "'s ⇒ 'm" "('s, 'm, 'p, 'l) seqp"
  | DELIVER "'l" "'s ⇒ data" "('s, 'm, 'p, 'l) seqp"
  | RECEIVE "'l" "'m ⇒ 's ⇒ 's" "('s, 'm, 'p, 'l) seqp"
  | CALL 'p
  for map: labelmap

syntax
  "_guard"    :: "['a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(‹unbreakable›⟨_⟩)//_› [0, 60] 60)
  "_lguard"   :: "['a, 'a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹{_}(‹unbreakable›⟨_⟩)//_› [0, 0, 60] 60)
  "_ifguard"  :: "[pttrn, bool,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(‹unbreakable›⟨_. _⟩)//_› [0, 0, 60] 60)

  "_bassign"  :: "[pttrn, 'a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(‹unbreakable›⟦_. _⟧)//_› [0, 0, 60] 60)
  "_lbassign" :: "['a, pttrn, 'a, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹{_}(‹unbreakable›⟦_. _⟧)//_› [0, 0, 0, 60] 60)

  "_assign"  :: "['a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹((‹unbreakable›⟦_⟧))//_› [0, 60] 60)
  "_lassign" :: "['a, 'a, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹({_}(‹unbreakable›⟦_⟧))//_› [0, 0, 60] 60)

  "_unicast"  :: "['a, 'a,  ('s, 'm, 'p, unit) seqp,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(3unicast'((1(3_),/ (3_))') .//(_)/ (2▹ _))› [0, 0, 60, 60] 60)
  "_lunicast" :: "['a, 'a, 'a, ('s, 'm, 'p, 'a) seqp, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹(3{_}unicast'((1(3_),/ (3_))') .//(_)/ (2▹ _))› [0, 0, 0, 60, 60] 60)

  "_bcast"    :: "['a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(3broadcast'((1(_))') .)//_› [0, 60] 60)
  "_lbcast"   :: "['a, 'a, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹(3{_}broadcast'((1(_))') .)//_› [0, 0, 60] 60)

  "_gcast"    :: "['a, 'a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(3groupcast'((1(_),/ (_))') .)//_› [0, 0, 60] 60)
  "_lgcast"   :: "['a, 'a, 'a, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹(3{_}groupcast'((1(_),/ (_))') .)//_› [0, 0, 0, 60] 60)

  "_send"     :: "['a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(3send'((_)') .)//_› [0, 60] 60)
  "_lsend"    :: "['a, 'a, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹(3{_}send'((_)') .)//_› [0, 0, 60] 60)

  "_deliver"  :: "['a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(3deliver'((_)') .)//_› [0, 60] 60)
  "_ldeliver" :: "['a, 'a, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹(3{_}deliver'((_)') .)//_› [0, 0, 60] 60)

  "_receive"  :: "['a,  ('s, 'm, 'p, unit) seqp] ⇒  ('s, 'm, 'p, unit) seqp"
                 (‹(3receive'((_)') .)//_› [0, 60] 60)
  "_lreceive" :: "['a, 'a, ('s, 'm, 'p, 'a) seqp] ⇒ ('s, 'm, 'p, 'a) seqp"
                 (‹(3{_}receive'((_)') .)//_› [0, 0, 60] 60)

syntax_consts
  "_guard" "_lguard" "_ifguard" ⇌ GUARD and
  "_assign" "_lassign" "_bassign" "_lbassign" ⇌ ASSIGN and
  "_unicast" "_lunicast" ⇌ UCAST and
  "_bcast" "_lbcast" ⇌ BCAST and
  "_gcast" "_lgcast" ⇌ GCAST and
  "_send" "_lsend" ⇌ SEND and
  "_deliver" "_ldeliver" ⇌ DELIVER and
  "_receive" "_lreceive" ⇌ RECEIVE

translations
  "_guard f p"     ⇌ "CONST GUARD () f p"
  "_lguard l f p"  ⇌ "CONST GUARD l f p"
  "_ifguard ξ e p" ⇀ "CONST GUARD () (λξ. if e then {ξ} else {}) p"

  "_assign f p"    ⇌ "CONST ASSIGN () f p"
  "_lassign l f p" ⇌ "CONST ASSIGN l f p"

  "_bassign ξ e p"    ⇌ "CONST ASSIGN () (λξ. e) p"
  "_lbassign l ξ e p" ⇌ "CONST ASSIGN l (λξ. e) p"

  "_unicast fip fmsg p q"    ⇌ "CONST UCAST () fip fmsg p q"
  "_lunicast l fip fmsg p q" ⇌ "CONST UCAST l fip fmsg p q"

  "_bcast fmsg p"    ⇌ "CONST BCAST () fmsg p"
  "_lbcast l fmsg p" ⇌ "CONST BCAST l fmsg p"

  "_gcast fipset fmsg p"    ⇌ "CONST GCAST () fipset fmsg p"
  "_lgcast l fipset fmsg p" ⇌ "CONST GCAST l fipset fmsg p"

  "_send fmsg p"    ⇌ "CONST SEND () fmsg p"
  "_lsend l fmsg p" ⇌ "CONST SEND l fmsg p"

  "_deliver fdata p"    ⇌ "CONST DELIVER () fdata p"
  "_ldeliver l fdata p" ⇌ "CONST DELIVER l fdata p"

  "_receive fmsg p"    ⇌ "CONST RECEIVE () fmsg p"
  "_lreceive l fmsg p" ⇌ "CONST RECEIVE l fmsg p"

notation "CHOICE" (‹((_)//⊕//(_))› [56, 55] 55)
     and "CALL"   (‹(3call'((3_)'))› [0] 60)

definition not_call :: "('s, 'm, 'p, 'l) seqp ⇒ bool"
where "not_call p ≡ ∀pn. p ≠ call(pn)"

lemma not_call_simps [simp]:
  "⋀l fg p.         not_call ({l}⟨fg⟩ p)"
  "⋀l fa p.         not_call ({l}⟦fa⟧ p)"
  "⋀p1 p2.          not_call (p1 ⊕ p2)"
  "⋀l fip fmsg p q. not_call ({l}unicast(fip, fmsg).p ▹ q)"
  "⋀l fmsg p.       not_call ({l}broadcast(fmsg).p)"
  "⋀l fips fmsg p.  not_call ({l}groupcast(fips, fmsg).p)"
  "⋀l fmsg p.       not_call ({l}send(fmsg).p)"
  "⋀l fdata p.      not_call ({l}deliver(fdata).p)"
  "⋀l fmsg p.       not_call ({l}receive(fmsg).p)"
  "⋀l pn.         ¬(not_call (call(pn)))"
  unfolding not_call_def by auto

definition not_choice :: "('s, 'm, 'p, 'l) seqp ⇒ bool"
where "not_choice p ≡ ∀p1 p2. p ≠ p1 ⊕ p2"

lemma not_choice_simps [simp]:
  "⋀l fg p.         not_choice ({l}⟨fg⟩ p)"
  "⋀l fa p.         not_choice ({l}⟦fa⟧ p)"
  "⋀p1 p2.        ¬(not_choice (p1 ⊕ p2))"
  "⋀l fip fmsg p q. not_choice ({l}unicast(fip, fmsg).p ▹ q)"
  "⋀l fmsg p.       not_choice ({l}broadcast(fmsg).p)"
  "⋀l fips fmsg p.  not_choice ({l}groupcast(fips, fmsg).p)"
  "⋀l fmsg p.       not_choice ({l}send(fmsg).p)"
  "⋀l fdata p.      not_choice ({l}deliver(fdata).p)"
  "⋀l fmsg p.       not_choice ({l}receive(fmsg).p)"
  "⋀l pn.           not_choice (call(pn))"
  unfolding not_choice_def by auto

lemma seqp_congs:
  "⋀l fg p. {l}⟨fg⟩ p = {l}⟨fg⟩ p"
  "⋀l fa p. {l}⟦fa⟧ p = {l}⟦fa⟧ p"
  "⋀p1 p2. p1 ⊕ p2 = p1 ⊕ p2"
  "⋀l fip fmsg p q. {l}unicast(fip, fmsg).p ▹ q = {l}unicast(fip, fmsg).p ▹ q"
  "⋀l fmsg p. {l}broadcast(fmsg).p = {l}broadcast(fmsg).p"
  "⋀l fips fmsg p. {l}groupcast(fips, fmsg).p = {l}groupcast(fips, fmsg).p"
  "⋀l fmsg p. {l}send(fmsg).p = {l}send(fmsg).p"
  "⋀l fdata p. {l}deliver(fdata).p = {l}deliver(fdata).p"
  "⋀l fmsg p. {l}receive(fmsg).p = {l}receive(fmsg).p"
  "⋀l pn. call(pn) = call(pn)"
  by auto

text ‹Remove data expressions from process terms.›

fun seqp_skeleton :: "('s, 'm, 'p, 'l) seqp ⇒ (unit, unit, 'p, 'l) seqp"
where
    "seqp_skeleton ({l}⟨_⟩ p)                 = {l}⟨λ_. {()}⟩ (seqp_skeleton p)"
  | "seqp_skeleton ({l}⟦_⟧ p)                 = {l}⟦λ_. ()⟧ (seqp_skeleton p)"
  | "seqp_skeleton (p ⊕ q)                   = (seqp_skeleton p) ⊕ (seqp_skeleton q)"
  | "seqp_skeleton ({l}unicast(_, _). p ▹ q) = {l}unicast(λ_. 0, λ_. ()). (seqp_skeleton p) ▹ (seqp_skeleton q)"
  | "seqp_skeleton ({l}broadcast(_). p)      = {l}broadcast(λ_. ()). (seqp_skeleton p)"
  | "seqp_skeleton ({l}groupcast(_, _). p)   = {l}groupcast(λ_. {}, λ_. ()). (seqp_skeleton p)"
  | "seqp_skeleton ({l}send(_). p)           = {l}send(λ_. ()). (seqp_skeleton p)"
  | "seqp_skeleton ({l}deliver(_). p)        = {l}deliver(λ_. 0). (seqp_skeleton p)"
  | "seqp_skeleton ({l}receive(_). p)        = {l}receive(λ_ _. ()). (seqp_skeleton p)"
  | "seqp_skeleton (call(pn))                = call(pn)"

text ‹Calculate the subterms of a term.›

fun subterms :: "('s, 'm, 'p, 'l) seqp ⇒ ('s, 'm, 'p, 'l) seqp set"
where
    "subterms ({l}⟨fg⟩ p) = {{l}⟨fg⟩ p} ∪ subterms p"
  | "subterms ({l}⟦fa⟧ p) = {{l}⟦fa⟧ p} ∪ subterms p"
  | "subterms (p1 ⊕ p2) = {p1 ⊕ p2} ∪ subterms p1 ∪ subterms p2"
  | "subterms ({l}unicast(fip, fmsg). p ▹ q) =
       {{l}unicast(fip, fmsg). p ▹ q} ∪ subterms p ∪ subterms q"
  | "subterms ({l}broadcast(fmsg). p) = {{l}broadcast(fmsg). p} ∪ subterms p"
  | "subterms ({l}groupcast(fips, fmsg). p) = {{l}groupcast(fips, fmsg). p} ∪ subterms p"
  | "subterms ({l}send(fmsg). p) = {{l}send(fmsg).p} ∪ subterms p"
  | "subterms ({l}deliver(fdata). p) = {{l}deliver(fdata).p} ∪ subterms p"
  | "subterms ({l}receive(fmsg). p) = {{l}receive(fmsg).p} ∪ subterms p"
  | "subterms (call(pn)) = {call(pn)}"

lemma subterms_refl [simp]: "p ∈ subterms p"
  by (cases p) simp_all

lemma subterms_trans [elim]:
  assumes "q ∈ subterms p"
      and "r ∈ subterms q"
    shows "r ∈ subterms p"
  using assms by (induction p) auto

lemma root_in_subterms [simp]:
   "⋀Γ pn. ∃pn'. Γ pn ∈ subterms (Γ pn')"
  by (rule_tac x=pn in exI) simp

lemma deriv_in_subterms [elim, dest]:
  "⋀l f p q. {l}⟨f⟩ q ∈ subterms p ⟹ q ∈ subterms p"
  "⋀l fa p q. {l}⟦fa⟧ q ∈ subterms p ⟹ q ∈ subterms p"
  "⋀p1 p2 p. p1 ⊕ p2 ∈ subterms p ⟹ p1 ∈ subterms p"
  "⋀p1 p2 p. p1 ⊕ p2 ∈ subterms p ⟹ p2 ∈ subterms p"
  "⋀l fip fmsg p q r. {l}unicast(fip, fmsg). q ▹ r ∈ subterms p ⟹ q ∈ subterms p"
  "⋀l fip fmsg p q r. {l}unicast(fip, fmsg). q ▹ r ∈ subterms p ⟹ r ∈ subterms p"
  "⋀l fmsg p q. {l}broadcast(fmsg). q ∈ subterms p ⟹ q ∈ subterms p"
  "⋀l fips fmsg p q. {l}groupcast(fips, fmsg). q ∈ subterms p ⟹ q ∈ subterms p"
  "⋀l fmsg p q. {l}send(fmsg). q ∈ subterms p ⟹ q ∈ subterms p"
  "⋀l fdata p q. {l}deliver(fdata). q ∈ subterms p ⟹ q ∈ subterms p"
  "⋀l fmsg p q. {l}receive(fmsg). q ∈ subterms p ⟹ q ∈ subterms p"
  by auto

subsection "Actions"

text ‹
  There are two sorts of ‹τ› actions in AWN: one at the level of individual processes
  (within nodes), and one at the network level (outside nodes). We define a class so that
  we can ignore this distinction whenever it is not critical.
›

class tau =
  fixes tau :: "'a" (‹τ›)

subsubsection "Sequential Actions (and related predicates)"

datatype 'm seq_action =
    broadcast 'm
  | groupcast "ip set" 'm
  | unicast ip 'm
  | notunicast ip           (‹¬unicast _› [1000] 60)
  | send 'm
  | deliver data
  | receive 'm
  | seq_tau                 (‹τs›)

instantiation "seq_action" :: (type) tau
begin
definition step_seq_tau [simp]: "τ ≡ τs"
instance ..
end

definition recvmsg :: "('m ⇒ bool) ⇒ 'm seq_action ⇒ bool"
where "recvmsg P a ≡ case a of receive m ⇒ P m
                             | _ ⇒ True"

lemma recvmsg_simps[simp]:
  "⋀m.     recvmsg P (broadcast m)     = True"
  "⋀ips m. recvmsg P (groupcast ips m) = True"
  "⋀ip m.  recvmsg P (unicast ip m)    = True"
  "⋀ip.    recvmsg P (notunicast ip)   = True"
  "⋀m.     recvmsg P (send m)          = True"
  "⋀d.     recvmsg P (deliver d)       = True"
  "⋀m.     recvmsg P (receive m)       = P m"
  "        recvmsg P τs                 = True"
  unfolding recvmsg_def by simp_all

lemma recvmsgTT [simp]: "recvmsg TT a"
  by (cases a) simp_all

lemma recvmsgE [elim]:
  assumes "recvmsg (R σ) a"
      and "⋀m. R σ m ⟹ R σ' m"
    shows "recvmsg (R σ') a"
  using assms(1) by (cases a) (auto elim!: assms(2))

definition anycast :: "('m ⇒ bool) ⇒ 'm seq_action ⇒ bool"
where "anycast P a ≡ case a of broadcast m ⇒ P m
                             | groupcast _ m ⇒ P m
                             | unicast _ m ⇒ P m
                             | _ ⇒ True"

lemma anycast_simps [simp]:
  "⋀m.     anycast P (broadcast m)     = P m"
  "⋀ips m. anycast P (groupcast ips m) = P m"
  "⋀ip m.  anycast P (unicast ip m)    = P m"
  "⋀ip.    anycast P (notunicast ip)   = True"
  "⋀m.     anycast P (send m)          = True"
  "⋀d.     anycast P (deliver d)       = True"
  "⋀m.     anycast P (receive m)       = True"
  "        anycast P τs                 = True"
  unfolding anycast_def by simp_all

definition orecvmsg :: "((ip ⇒ 's) ⇒ 'm ⇒ bool) ⇒ (ip ⇒ 's) ⇒ 'm seq_action ⇒ bool"
where "orecvmsg P σ a ≡ (case a of receive m ⇒ P σ m
                                         | _ ⇒ True)"

lemma orecvmsg_simps [simp]:
  "⋀m.     orecvmsg P σ (broadcast m)     = True"
  "⋀ips m. orecvmsg P σ (groupcast ips m) = True"
  "⋀ip m.  orecvmsg P σ (unicast ip m)    = True"
  "⋀ip.    orecvmsg P σ (notunicast ip)   = True"
  "⋀m.     orecvmsg P σ (send m)          = True"
  "⋀d.     orecvmsg P σ (deliver d)       = True"
  "⋀m.     orecvmsg P σ (receive m)       = P σ m"
  "         orecvmsg P σ τs                = True"
  unfolding orecvmsg_def by simp_all

lemma orecvmsgEI [elim]:
  "⟦ orecvmsg P σ a; ⋀σ a. P σ a ⟹ Q σ a ⟧ ⟹ orecvmsg Q σ a"
  by (cases a) simp_all

lemma orecvmsg_stateless_recvmsg [elim]:
  "orecvmsg (λ_. P) σ a ⟹ recvmsg P a"
  by (cases a) simp_all

lemma orecvmsg_recv_weaken [elim]:
  "⟦ orecvmsg P σ a; ⋀σ a. P σ a ⟹ Q a ⟧ ⟹ recvmsg Q a"
  by (cases a) simp_all

lemma orecvmsg_recvmsg [elim]:
  "orecvmsg P σ a ⟹ recvmsg (P σ) a"
  by (cases a) simp_all

definition sendmsg :: "('m ⇒ bool) ⇒ 'm seq_action ⇒ bool"
where "sendmsg P a ≡ case a of send m ⇒ P m | _ ⇒ True"

lemma sendmsg_simps [simp]:
  "⋀m.     sendmsg P (broadcast m)     = True"
  "⋀ips m. sendmsg P (groupcast ips m) = True"
  "⋀ip m.  sendmsg P (unicast ip m)    = True"
  "⋀ip.    sendmsg P (notunicast ip)   = True"
  "⋀m.     sendmsg P (send m)          = P m"
  "⋀d.     sendmsg P (deliver d)       = True"
  "⋀m.     sendmsg P (receive m)       = True"
  "        sendmsg P τs                 = True"
  unfolding sendmsg_def by simp_all

type_synonym ('s, 'm, 'p, 'l) seqp_env = "'p ⇒ ('s, 'm, 'p, 'l) seqp"

subsubsection "Node Actions (and related predicates)"

datatype 'm node_action =
    node_cast "ip set" 'm             (‹_:*cast'(_')›       [200, 200] 200)                                                 
  | node_deliver ip data              (‹_:deliver'(_')›     [200, 200] 200)
  | node_arrive "ip set" "ip set" 'm  (‹_¬_:arrive'(_')›    [200, 200, 200] 200)
  | node_connect ip ip                (‹connect'(_, _')›    [200, 200] 200)
  | node_disconnect ip ip             (‹disconnect'(_, _')› [200, 200] 200)
  | node_newpkt ip data ip            (‹_:newpkt'(_, _')›   [200, 200, 200] 200)
  | node_tau                          (‹τn›)

instantiation "node_action" :: (type) tau
begin
definition step_node_tau [simp]: "τ ≡ τn"
instance ..
end

definition arrivemsg :: "ip ⇒ ('m ⇒ bool) ⇒ 'm node_action ⇒ bool"
where "arrivemsg i P a ≡ case a of node_arrive ii ni m ⇒ ((ii = {i} ⟶ P m))
                                  | _ ⇒ True"

lemma arrivemsg_simps[simp]:
  "⋀R m.       arrivemsg i P (R:*cast(m))         = True"
  "⋀d m.       arrivemsg i P (d:deliver(m))       = True"
  "⋀i ii ni m. arrivemsg i P (ii¬ni:arrive(m))    = (ii = {i} ⟶ P m)"
  "⋀i1 i2.     arrivemsg i P (connect(i1, i2))    = True"
  "⋀i1 i2.     arrivemsg i P (disconnect(i1, i2)) = True"
  "⋀i i' d di. arrivemsg i P (i':newpkt(d, di))   = True"
  "             arrivemsg i P τn                   = True"
  unfolding arrivemsg_def by simp_all

lemma arrivemsgTT [simp]: "arrivemsg i TT = TT"
  by (rule ext) (clarsimp simp: arrivemsg_def split: node_action.split)

definition oarrivemsg :: "((ip ⇒ 's) ⇒ 'm ⇒ bool) ⇒ (ip ⇒ 's) ⇒ 'm node_action ⇒ bool"
where "oarrivemsg P σ a ≡ case a of node_arrive ii ni m ⇒ P σ m | _ ⇒ True"

lemma oarrivemsg_simps[simp]:
  "⋀R m.       oarrivemsg P σ (R:*cast(m))         = True"
  "⋀d m.       oarrivemsg P σ (d:deliver(m))       = True"
  "⋀i ii ni m. oarrivemsg P σ (ii¬ni:arrive(m))    = P σ m"
  "⋀i1 i2.     oarrivemsg P σ (connect(i1, i2))    = True"
  "⋀i1 i2.     oarrivemsg P σ (disconnect(i1, i2)) = True"
  "⋀i i' d di. oarrivemsg P σ (i':newpkt(d, di))   = True"
  "             oarrivemsg P σ τn                   = True"
  unfolding oarrivemsg_def by simp_all

lemma oarrivemsg_True [simp, intro]: "oarrivemsg (λ_ _. True) σ a"
  by (cases a) auto

definition castmsg :: "('m ⇒ bool) ⇒ 'm node_action ⇒ bool"
where "castmsg P a ≡ case a of _:*cast(m) ⇒ P m
                              | _ ⇒ True"

lemma castmsg_simps[simp]:
  "⋀R m.       castmsg P (R:*cast(m))         = P m"
  "⋀d m.       castmsg P (d:deliver(m))       = True"
  "⋀i ii ni m. castmsg P (ii¬ni:arrive(m))    = True"
  "⋀i1 i2.     castmsg P (connect(i1, i2))    = True"
  "⋀i1 i2.     castmsg P (disconnect(i1, i2)) = True"
  "⋀i i' d di. castmsg P (i':newpkt(d, di))   = True"
  "             castmsg P τn                   = True"
  unfolding castmsg_def by simp_all

subsection "Networks"

datatype net_tree =
    Node ip "ip set"          (‹⟨_; _⟩›)
  | Subnet net_tree net_tree  (infixl ‹∥› 90)

declare net_tree.induct [[induct del]]
lemmas net_tree_induct [induct type: net_tree] = net_tree.induct [rename_abs i R p1 p2]

datatype 's net_state =
    NodeS ip 's "ip set"
  | SubnetS "'s net_state" "'s net_state"

fun net_ips :: "'s net_state ⇒ ip set"
where
    "net_ips (NodeS i s R) = {i}"
  | "net_ips (SubnetS n1 n2) = net_ips n1 ∪ net_ips n2"

fun net_tree_ips :: "net_tree ⇒ ip set"
where
    "net_tree_ips (p1 ∥ p2) = net_tree_ips p1 ∪ net_tree_ips p2"
  | "net_tree_ips (⟨i; R⟩) = {i}"

lemma net_tree_ips_commute:
  "net_tree_ips (p1 ∥ p2) = net_tree_ips (p2 ∥ p1)"
  by simp (rule Un_commute)

fun wf_net_tree :: "net_tree ⇒ bool"
where
   "wf_net_tree (p1 ∥ p2) = (net_tree_ips p1 ∩ net_tree_ips p2 = {}
                             ∧ wf_net_tree p1 ∧ wf_net_tree p2)"
 | "wf_net_tree (⟨i; R⟩) = True"

lemma wf_net_tree_children [elim]:
  assumes "wf_net_tree (p1 ∥ p2)"
  obtains "wf_net_tree p1"
      and "wf_net_tree p2"
  using assms by simp

fun netmap :: "'s net_state ⇒ ip ⇒ 's option"
where
    "netmap (NodeS i p Ri) = [i ↦ p]"
  | "netmap (SubnetS s t) = netmap s ++ netmap t"

lemma not_in_netmap [simp]:
  assumes "i ∉ net_ips ns"
    shows "netmap ns i = None"
  using assms by (induction ns) simp_all

lemma netmap_none_not_in_net_ips:
  assumes "netmap ns i = None"
    shows "i∉net_ips ns"
  using assms by (induction ns) auto

lemma net_ips_is_dom_netmap: "net_ips s = dom(netmap s)"
  proof (induction s)
    fix i Ri and p :: 's
    show "net_ips (NodeS i p Ri) = dom (netmap (NodeS i p Ri))"
      by auto
  next
    fix s1 s2 :: "'s net_state"
    assume "net_ips s1 = dom (netmap s1)"
       and "net_ips s2 = dom (netmap s2)"
    thus "net_ips (SubnetS s1 s2) = dom (netmap (SubnetS s1 s2))"
      by auto
  qed

lemma in_netmap [simp]:
  assumes "i ∈ net_ips ns"
    shows "netmap ns i ≠ None"
  using assms by (auto simp add: net_ips_is_dom_netmap)

lemma netmap_subnets_same:
  assumes "netmap s1 i = x"
      and "netmap s2 i = x"
    shows "netmap (SubnetS s1 s2) i = x"
  using assms by simp (metis map_add_dom_app_simps(1) map_add_dom_app_simps(3))

lemma netmap_subnets_samef:
  assumes "netmap s1 = f"
      and "netmap s2 = f"
    shows "netmap (SubnetS s1 s2) = f"
  using assms by simp (metis map_add_le_mapI map_le_antisym map_le_map_add map_le_refl)

lemma netmap_add_disjoint [elim]:
  assumes "∀i∈net_ips s1 ∪ net_ips s2. the ((netmap s1 ++ netmap s2) i) = σ i"
      and "net_ips s1 ∩ net_ips s2 = {}"
    shows "∀i∈net_ips s1. the (netmap s1 i) = σ i"
  proof
    fix i
    assume "i ∈ net_ips s1"
    hence "i ∈ dom(netmap s1)" by (simp add: net_ips_is_dom_netmap)
    moreover with assms(2) have "i ∉ dom(netmap s2)" by (auto simp add: net_ips_is_dom_netmap)
    ultimately have "the (netmap s1 i) = the ((netmap s1 ++ netmap s2) i)"
      by (simp add: map_add_dom_app_simps)
    with assms(1) and ‹i∈net_ips s1› show "the (netmap s1 i) = σ i" by simp
  qed

lemma netmap_add_disjoint2 [elim]:
  assumes "∀i∈net_ips s1 ∪ net_ips s2. the ((netmap s1 ++ netmap s2) i) = σ i"
    shows "∀i∈net_ips s2. the (netmap s2 i) = σ i"
  using assms by (simp add: net_ips_is_dom_netmap)
                 (metis Un_iff map_add_dom_app_simps(1))

lemma net_ips_netmap_subnet [elim]:
  assumes "net_ips s1 ∩ net_ips s2 = {}"
      and "∀i∈net_ips (SubnetS s1 s2). the (netmap (SubnetS s1 s2) i) = σ i"
    shows "∀i∈net_ips s1. the (netmap s1 i) = σ i"
      and "∀i∈net_ips s2. the (netmap s2 i) = σ i"
  proof -
    from assms(2) have "∀i∈net_ips s1 ∪ net_ips s2. the ((netmap s1 ++ netmap s2) i) = σ i" by auto
    with assms(1) show "∀i∈net_ips s1. the (netmap s1 i) = σ i"
      by - (erule(1) netmap_add_disjoint)
  next
    from assms(2) have "∀i∈net_ips s1 ∪ net_ips s2. the ((netmap s1 ++ netmap s2) i) = σ i" by auto
    thus "∀i∈net_ips s2. the (netmap s2 i) = σ i"
      by - (erule netmap_add_disjoint2)
  qed

fun inoclosed :: "'s ⇒ 'm::msg node_action ⇒ bool"
where
    "inoclosed _ (node_arrive ii ni m) = eq_newpkt m"
  | "inoclosed _ (node_newpkt i d di)  = False"
  | "inoclosed _ _ = True"

lemma inclosed_simps [simp]:
  "⋀σ ii ni. inoclosed σ (ii¬ni:arrive(m))   = eq_newpkt m"
  "⋀σ d di.  inoclosed σ (i:newpkt(d, di))   = False"
  "⋀σ R m.   inoclosed σ (R:*cast(m))        = True"
  "⋀σ i d.   inoclosed σ (i:deliver(d))      = True"
  "⋀σ i i'.  inoclosed σ (connect(i, i'))    = True"
  "⋀σ i i'.  inoclosed σ (disconnect(i, i')) = True"
  "⋀σ.       inoclosed σ (τ)                 = True"
  by auto

definition
  netmask :: "ip set ⇒ ((ip ⇒ 's) × 'l) ⇒ ((ip ⇒ 's option) × 'l)"
where
  "netmask I s ≡ (λi. if i∈I then Some (fst s i) else None, snd s)"

lemma netmask_def' [simp]:
  "netmask I (σ, ζ) = (λi. if i∈I then Some (σ i) else None, ζ)"
  unfolding netmask_def by auto

fun netgmap :: "('s ⇒ 'g × 'l) ⇒ 's net_state ⇒ (nat ⇒ 'g option) × 'l net_state"
  where
    "netgmap sr (NodeS i s R) = ([i ↦ fst (sr s)], NodeS i (snd (sr s)) R)"
  | "netgmap sr (SubnetS s1 s2) = (let (σ1, ss) = netgmap sr s1 in
                                   let (σ2, tt) = netgmap sr s2 in
                                   (σ1 ++ σ2, SubnetS ss tt))"

lemma dom_fst_netgmap [simp, intro]: "dom (fst (netgmap sr n)) = net_ips n"
  proof (induction n)
    fix i s R
    show "dom (fst (netgmap sr (NodeS i s R))) = net_ips (NodeS i s R)"
      by simp
  next
    fix n1 n2
    assume a1: "dom (fst (netgmap sr n1)) = net_ips n1"
       and a2: "dom (fst (netgmap sr n2)) = net_ips n2"
    obtain σ1 ζ1 σ2 ζ2 where nm1: "netgmap sr n1 = (σ1, ζ1)"
                        and nm2: "netgmap sr n2 = (σ2, ζ2)"
      by (metis surj_pair)
    hence "netgmap sr (SubnetS n1 n2) = (σ1 ++ σ2, SubnetS ζ1 ζ2)" by simp
    hence "dom (fst (netgmap sr (SubnetS n1 n2))) = dom (σ1 ++ σ2)" by simp
    also from a1 a2 nm1 nm2 have "dom (σ1 ++ σ2) = net_ips (SubnetS n1 n2)" by auto
    finally show "dom (fst (netgmap sr (SubnetS n1 n2))) = net_ips (SubnetS n1 n2)" .
  qed

lemma netgmap_pair_dom [elim]:
  obtains σ ζ where "netgmap sr n = (σ, ζ)"
                and "dom σ = net_ips n"
    by (metis dom_fst_netgmap surjective_pairing)

lemma net_ips_netgmap [simp]:
  "net_ips (snd (netgmap sr s)) = net_ips s"
  proof (induction s)
    fix s1 s2
    assume "net_ips (snd (netgmap sr s1)) = net_ips s1"
       and "net_ips (snd (netgmap sr s2)) = net_ips s2"
    thus "net_ips (snd (netgmap sr (SubnetS s1 s2))) = net_ips (SubnetS s1 s2)"
      by (cases "netgmap sr s1", cases "netgmap sr s2") auto
  qed simp

lemma some_the_fst_netgmap:
  assumes "i ∈ net_ips s"
    shows "Some (the (fst (netgmap sr s) i)) = fst (netgmap sr s) i"
  using assms by (metis domIff dom_fst_netgmap option.collapse)


lemma fst_netgmap_none [simp]:
  assumes "i ∉ net_ips s"
    shows "fst (netgmap sr s) i = None"
  using assms by (metis domIff dom_fst_netgmap)

lemma fst_netgmap_subnet [simp]:
  "fst (case netgmap sr s1 of (σ1, ss) ⇒
        case netgmap sr s2 of (σ2, tt) ⇒
        (σ1 ++ σ2, SubnetS ss tt)) = (fst (netgmap sr s1) ++ fst (netgmap sr s2))"
  by (metis (mono_tags) fst_conv netgmap_pair_dom split_conv)

lemma snd_netgmap_subnet [simp]:
  "snd (case netgmap sr s1 of (σ1, ss) ⇒
        case netgmap sr s2 of (σ2, tt) ⇒
        (σ1 ++ σ2, SubnetS ss tt)) = (SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2)))"
  by (metis (lifting, no_types) Pair_inject split_beta' surjective_pairing)

lemma fst_netgmap_not_none [simp]:
  assumes "i ∈ net_ips s"
    shows "fst (netgmap sr s) i ≠ None"
  using assms by (induction s) auto

lemma netgmap_netgmap_not_rhs [simp]:
  assumes "i ∉ net_ips s2"
    shows "(fst (netgmap sr s1) ++ fst (netgmap sr s2)) i = (fst (netgmap sr s1)) i"
  proof -
    from assms(1) have "i ∉ dom (fst (netgmap sr s2))" by simp
    thus ?thesis by (simp add: map_add_dom_app_simps)
  qed

lemma netgmap_netgmap_rhs [simp]:
  assumes "i ∈ net_ips s2"
    shows "(fst (netgmap sr s1) ++ fst (netgmap sr s2)) i = (fst (netgmap sr s2)) i"
  using assms by (simp add: map_add_dom_app_simps)

lemma netgmap_netmask_subnets [elim]:
  assumes "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
      and "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
    shows "fst (netgmap sr (SubnetS s1 s2))
            = fst (netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr (SubnetS s1 s2))))"
  proof (rule ext)
    fix i
    have "i ∈ net_tree_ips n1 ∨ i ∈ net_tree_ips n2 ∨ (i∉net_tree_ips n1 ∪ net_tree_ips n2)"
      by auto
    thus "fst (netgmap sr (SubnetS s1 s2)) i
            = fst (netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr (SubnetS s1 s2)))) i"
    proof (elim disjE)
      assume "i ∈ net_tree_ips n1"
      with ‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
           ‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
        show ?thesis
          by (cases "netgmap sr s1", cases "netgmap sr s2", clarsimp)
             (metis (lifting, mono_tags) map_add_Some_iff)
    next
      assume "i ∈ net_tree_ips n2"
      with ‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
        show ?thesis
          by simp (metis (lifting, mono_tags) fst_conv map_add_find_right)
    next
      assume "i∉net_tree_ips n1 ∪ net_tree_ips n2"
      with ‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
           ‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
        show ?thesis
          by simp (metis (lifting, mono_tags) fst_conv)
    qed
  qed

lemma netgmap_netmask_subnets' [elim]:
  assumes "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
      and "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
      and "s = SubnetS s1 s2"
    shows "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s))"
  by (simp only: assms(3))
     (rule prod_eqI [OF netgmap_netmask_subnets [OF assms(1-2)]], simp)

lemma netgmap_subnet_split1:
  assumes "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
      and "net_tree_ips n1 ∩ net_tree_ips n2 = {}"
      and "net_ips s1 = net_tree_ips n1"
      and "net_ips s2 = net_tree_ips n2"
    shows "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
  proof (rule prod_eqI)
    show "fst (netgmap sr s1) = fst (netmask (net_tree_ips n1) (σ, snd (netgmap sr s1)))"
    proof (rule ext, simp, intro conjI impI)
      fix i
      assume "i∈net_tree_ips n1"
      with ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}› have "i∉net_tree_ips n2"
        by auto
      from assms(1) [simplified prod_eq_iff]
        have "(fst (netgmap sr s1) ++ fst (netgmap sr s2)) i =
                 (if i ∈ net_tree_ips n1 ∨ i ∈ net_tree_ips n2 then Some (σ i) else None)"
          by simp
      also from ‹i∉net_tree_ips n2› and ‹net_ips s2 = net_tree_ips n2›
        have "(fst (netgmap sr s1) ++ fst (netgmap sr s2)) i = fst (netgmap sr s1) i"
          by (metis dom_fst_netgmap map_add_dom_app_simps(3))
      finally show "fst (netgmap sr s1) i = Some (σ i)"
        using ‹i∈net_tree_ips n1› by simp
    next
      fix i
      assume "i ∉ net_tree_ips n1"
      with ‹net_ips s1 = net_tree_ips n1› have "i ∉ net_ips s1" by simp
      thus "fst (netgmap sr s1) i = None" by simp
    qed
  qed simp

lemma netgmap_subnet_split2:
  assumes "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
      and "net_ips s1 = net_tree_ips n1"
      and "net_ips s2 = net_tree_ips n2"
    shows "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
  proof (rule prod_eqI)
    show "fst (netgmap sr s2) = fst (netmask (net_tree_ips n2) (σ, snd (netgmap sr s2)))"
    proof (rule ext, simp, intro conjI impI)
      fix i
      assume "i∈net_tree_ips n2"
      from assms(1) [simplified prod_eq_iff]
        have "(fst (netgmap sr s1) ++ fst (netgmap sr s2)) i =
                 (if i ∈ net_tree_ips n1 ∨ i ∈ net_tree_ips n2 then Some (σ i) else None)"
          by simp
      also from ‹i∈net_tree_ips n2› and ‹net_ips s2 = net_tree_ips n2›
        have "(fst (netgmap sr s1) ++ fst (netgmap sr s2)) i = fst (netgmap sr s2) i"
          by (metis dom_fst_netgmap map_add_dom_app_simps(1))
      finally show "fst (netgmap sr s2) i = Some (σ i)"
        using ‹i∈net_tree_ips n2› by simp
    next
      fix i
      assume "i ∉ net_tree_ips n2"
      with ‹net_ips s2 = net_tree_ips n2› have "i ∉ net_ips s2" by simp
      thus "fst (netgmap sr s2) i = None" by simp
    qed
  qed simp

lemma netmap_fst_netgmap_rel:
  shows "(λi. map_option (fst o sr) (netmap s i)) = fst (netgmap sr s)"
  proof (induction s)
    fix ii s R
    show "(λi. map_option (fst ∘ sr) (netmap (NodeS ii s R) i)) = fst (netgmap sr (NodeS ii s R))"
      by auto
  next
    fix s1 s2
    assume a1: "(λi. map_option (fst ∘ sr) (netmap s1 i)) = fst (netgmap sr s1)"
       and a2: "(λi. map_option (fst ∘ sr) (netmap s2 i)) = fst (netgmap sr s2)"
    show "(λi. map_option (fst ∘ sr) (netmap (SubnetS s1 s2) i)) = fst (netgmap sr (SubnetS s1 s2))"
    proof (rule ext)
      fix i
      from a1 a2 have "map_option (fst ∘ sr) ((netmap s1 ++ netmap s2) i)
                                    = (fst (netgmap sr s1) ++ fst (netgmap sr s2)) i"
        by (metis fst_conv map_add_dom_app_simps(1) map_add_dom_app_simps(3)
                  net_ips_is_dom_netmap netgmap_pair_dom)
      thus "map_option (fst ∘ sr) (netmap (SubnetS s1 s2) i) = fst (netgmap sr (SubnetS s1 s2)) i"
        by simp
    qed
  qed

lemma netmap_is_fst_netgmap':
  assumes "netmap s' i = netmap s i"
    shows "fst (netgmap sr s') i = fst (netgmap sr s) i"
  using assms by (metis netmap_fst_netgmap_rel)

lemma netmap_is_fst_netgmap:
  assumes "netmap s' = netmap s"
    shows "fst (netgmap sr s') = fst (netgmap sr s)"
  by (rule ext) (metis assms netmap_fst_netgmap_rel)

lemma fst_netgmap_pair_fst [simp]:
  "fst (netgmap (λ(p, q). (fst p, snd p, q)) s) = fst (netgmap fst s)"
  by (induction s) auto

text ‹Introduce streamlined alternatives to netgmap to simplify certain property
        statements and thus make them easier to understand and to present.›

fun netlift :: "('s ⇒ 'g × 'l) ⇒ 's net_state ⇒ (nat ⇒ 'g option)"
  where
    "netlift sr (NodeS i s R) = [i ↦ fst (sr s)]"
  | "netlift sr (SubnetS s t) = (netlift sr s) ++ (netlift sr t)"

lemma fst_netgmap_netlift:
  "fst (netgmap sr s) = netlift sr s"
  by (induction s) simp_all

fun netliftl :: "('s ⇒ 'g × 'l) ⇒ 's net_state ⇒ 'l net_state"
  where
    "netliftl sr (NodeS i s R) = NodeS i (snd (sr s)) R"
  | "netliftl sr (SubnetS s t) = SubnetS (netliftl sr s) (netliftl sr t)"

lemma snd_netgmap_netliftl:
  "snd (netgmap sr s) = netliftl sr s"
  by (induction s) simp_all
 
lemma netgmap_netlift_netliftl: "netgmap sr s = (netlift sr s, netliftl sr s)"
  by rule (simp_all add: fst_netgmap_netlift snd_netgmap_netliftl)

end