Theory Toy

(*  Title:       Toy.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
    Author:      Peter Höfner
*)

section "Simple toy example"

theory Toy
imports Main AWN_Main Qmsg_Lifting
begin

subsection "Messages used in the protocol"

datatype msg =
    Pkt data ip
  | Newpkt data ip

instantiation msg :: msg
begin
definition newpkt_def [simp]: "newpkt ≡ λ(d,did). Newpkt d did"
definition eq_newpkt_def: "eq_newpkt m ≡ case m of Newpkt d did  ⇒ True | _ ⇒ False" 

instance by intro_classes (simp add: eq_newpkt_def)
end

definition pkt :: "nat × nat ⇒ msg"
where "pkt ≡ λ(no, sid). Pkt no sid"

lemma pkt_simp [simp]:
  "pkt(no, sid) = Pkt no sid"
  unfolding pkt_def by simp

lemma not_eq_newpkt_pkt [simp]: "¬eq_newpkt (Pkt no sid)"
  unfolding eq_newpkt_def by simp

subsection "Protocol model"

record state =
  id    :: "nat"
  no    :: "nat"
  nhid  :: "nat"
  (* all locals *)
  msg    :: "msg"
  num    :: "nat"
  sid    :: "nat"

abbreviation toy_init :: "ip ⇒ state"
where "toy_init i ≡ ⦇
         id = i,
         no = 0,
         nhid = i,

         msg    = (SOME x. True),
         num    = (SOME x. True),
         sid    = (SOME x. True)
       ⦈"

lemma some_neq_not_eq [simp]: "¬((SOME x :: nat. x ≠ i) = i)"
  by (subst some_eq_ex) (metis zero_neq_numeral)

definition clear_locals :: "state ⇒ state"
where "clear_locals ξ = ξ ⦇
    msg    := (SOME x. True),
    num    := (SOME x. True),
    sid    := (SOME x. True)
  ⦈"

lemma clear_locals_but_not_globals [simp]:
  "id (clear_locals ξ) = id ξ"
  "no (clear_locals ξ) = no ξ"
  "nhid (clear_locals ξ) = nhid ξ"
  unfolding clear_locals_def by auto

definition is_newpkt
where "is_newpkt ξ ≡ case msg ξ of
                       Newpkt data did ⇒ { ξ⦇num := data⦈ }
                     | _ ⇒ {}"

definition is_pkt
where "is_pkt ξ ≡ case msg ξ of
                    Pkt num' sid' ⇒ { ξ⦇ num := num', sid := sid' ⦈ }
                  | _ ⇒ {}"

lemmas is_msg_defs =
  is_pkt_def is_newpkt_def

lemma is_msg_inv_id [simp]:
  "ξ' ∈ is_pkt ξ    ⟹ id ξ' = id ξ"
  "ξ' ∈ is_newpkt ξ ⟹ id ξ' = id ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_sid [simp]:
  "ξ' ∈ is_newpkt ξ ⟹ sid ξ' = sid ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_no [simp]:
  "ξ' ∈ is_pkt ξ    ⟹ no ξ' = no ξ"
  "ξ' ∈ is_newpkt ξ ⟹ no ξ' = no ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_nhid [simp]:
  "ξ' ∈ is_pkt ξ    ⟹ nhid ξ' = nhid ξ"
  "ξ' ∈ is_newpkt ξ ⟹ nhid ξ' = nhid ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_msg [simp]:
  "ξ' ∈ is_pkt ξ    ⟹ msg ξ' = msg ξ"
  "ξ' ∈ is_newpkt ξ ⟹ msg ξ' = msg ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

datatype pseqp =
    PToy

fun nat_of_seqp :: "pseqp ⇒ nat"
where
  "nat_of_seqp PToy = 1"

instantiation "pseqp" :: ord
begin
definition less_eq_seqp [iff]: "l1 ≤ l2 = (nat_of_seqp l1 ≤ nat_of_seqp l2)"
definition less_seqp [iff]:    "l1 < l2 = (nat_of_seqp l1 < nat_of_seqp l2)"
instance ..
end

abbreviation Toy
where
  "Toy ≡ λ_. ⟦clear_locals⟧ call(PToy)"

fun Γ⇩T⇩O⇩Y :: "(state, msg, pseqp, pseqp label) seqp_env"
where
  "Γ⇩T⇩O⇩Y PToy = labelled PToy (
     receive(λmsg' ξ. ξ ⦇ msg := msg' ⦈).
     ⟦ξ. ξ ⦇nhid := id ξ⦈⟧
     (   ⟨is_newpkt⟩ 
         (
             ⟦ξ. ξ ⦇no := max (no ξ) (num ξ)⦈⟧
             broadcast(λξ. pkt(no ξ, id ξ)). Toy()
         )
       ⊕ ⟨is_pkt⟩
       (
            ⟨ξ. num ξ > no ξ⟩
               ⟦ξ. ξ ⦇no := num ξ⦈⟧
               ⟦ξ. ξ ⦇nhid := sid ξ⦈⟧
               broadcast(λξ. pkt(no ξ, id ξ)). Toy()
         ⊕ ⟨ξ. num ξ ≤ no ξ⟩
               Toy()
       )
     ))"

declare Γ⇩T⇩O⇩Y.simps [simp del]
lemmas Γ⇩T⇩O⇩Y_simps [simp, code] = Γ⇩T⇩O⇩Y.simps [simplified]

fun Γ⇩T⇩O⇩Y_skeleton
where "Γ⇩T⇩O⇩Y_skeleton PToy = seqp_skeleton (Γ⇩T⇩O⇩Y PToy)"

lemma Γ⇩T⇩O⇩Y_skeleton_wf [simp]:
  "wellformed Γ⇩T⇩O⇩Y_skeleton"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ⇩T⇩O⇩Y_skeleton pn)"
      by (cases pn) simp_all
  qed

declare Γ⇩T⇩O⇩Y_skeleton.simps [simp del]
lemmas Γ⇩T⇩O⇩Y_skeleton_simps [simp, code] = Γ⇩T⇩O⇩Y_skeleton.simps [simplified Γ⇩T⇩O⇩Y_simps seqp_skeleton.simps]

lemma toy_proc_cases [dest]:
  fixes p pn
  assumes "p ∈ ctermsl (Γ⇩T⇩O⇩Y pn)"
    shows "p ∈ ctermsl (Γ⇩T⇩O⇩Y PToy)"
  using assms
  by (cases pn) simp_all

definition σ⇩T⇩O⇩Y :: "ip ⇒ (state × (state, msg, pseqp, pseqp label) seqp) set"
where "σ⇩T⇩O⇩Y i ≡ {(toy_init i, Γ⇩T⇩O⇩Y PToy)}"

abbreviation ptoy
  :: "ip ⇒ (state × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "ptoy i ≡ ⦇ init = σ⇩T⇩O⇩Y i, trans = seqp_sos Γ⇩T⇩O⇩Y ⦈"

lemma toy_trans: "trans (ptoy i) = seqp_sos Γ⇩T⇩O⇩Y"
  by simp

lemma toy_control_within [simp]: "control_within Γ⇩T⇩O⇩Y (init (ptoy i))"
  unfolding σ⇩T⇩O⇩Y_def by (rule control_withinI) (auto simp del: Γ⇩T⇩O⇩Y_simps)

lemma toy_wf [simp]:
  "wellformed Γ⇩T⇩O⇩Y"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ⇩T⇩O⇩Y pn)"
      by (cases pn) simp_all
  qed

lemmas toy_labels_not_empty [simp] = labels_not_empty [OF toy_wf]

lemma toy_ex_label [intro]: "∃l. l∈labels Γ⇩T⇩O⇩Y p"
  by (metis toy_labels_not_empty all_not_in_conv)

lemma toy_ex_labelE [elim]:
  assumes "∀l∈labels Γ⇩T⇩O⇩Y p. P l p"
      and "∃p l. P l p ⟹ Q"
    shows "Q"
 using assms by (metis toy_ex_label) 

lemma toy_simple_labels [simp]: "simple_labels Γ⇩T⇩O⇩Y"
  proof
    fix pn p
    assume "p∈subterms(Γ⇩T⇩O⇩Y pn)"
    thus "∃!l. labels Γ⇩T⇩O⇩Y p = {l}"
    by (cases pn) (simp_all cong: seqp_congs | elim disjE)+
  qed

lemma σ⇩T⇩O⇩Y_labels [simp]: "(ξ, p) ∈ σ⇩T⇩O⇩Y i ⟹  labels Γ⇩T⇩O⇩Y p = {PToy-:0}"
  unfolding σ⇩T⇩O⇩Y_def by simp

text ‹By default, we no longer let the simplifier descend into process terms.›

declare seqp_congs [cong]

(* configure the inv_cterms tactic *)
declare
  Γ⇩T⇩O⇩Y_simps [cterms_env]
  toy_proc_cases [ctermsl_cases]
  seq_invariant_ctermsI [OF toy_wf toy_control_within toy_simple_labels toy_trans, cterms_intros]
  seq_step_invariant_ctermsI [OF toy_wf toy_control_within toy_simple_labels toy_trans, cterms_intros]

subsection "Define an open version of the protocol"

definition σ⇩O⇩T⇩O⇩Y :: "((ip ⇒ state) × ((state, msg, pseqp, pseqp label) seqp)) set"
where "σ⇩O⇩T⇩O⇩Y ≡ {(toy_init, Γ⇩T⇩O⇩Y PToy)}"

abbreviation optoy
  :: "ip ⇒ ((ip ⇒ state) × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "optoy i ≡ ⦇ init = σ⇩O⇩T⇩O⇩Y, trans = oseqp_sos Γ⇩T⇩O⇩Y i ⦈"

lemma initiali_toy [intro!, simp]: "initiali i (init (optoy i)) (init (ptoy i))"
  unfolding σ⇩T⇩O⇩Y_def σ⇩O⇩T⇩O⇩Y_def by rule simp_all

lemma oaodv_control_within [simp]: "control_within Γ⇩T⇩O⇩Y (init (optoy i))"
  unfolding σ⇩O⇩T⇩O⇩Y_def by (rule control_withinI) (auto simp del: Γ⇩T⇩O⇩Y_simps)

lemma σ⇩O⇩T⇩O⇩Y_labels [simp]: "(σ, p) ∈ σ⇩O⇩T⇩O⇩Y ⟹  labels Γ⇩T⇩O⇩Y p = {PToy-:0}"
  unfolding σ⇩O⇩T⇩O⇩Y_def by simp

lemma otoy_trans: "trans (optoy i) = oseqp_sos Γ⇩T⇩O⇩Y i"
  by simp

(* configure the inv_cterms tactic *)
declare
  oseq_invariant_ctermsI [OF toy_wf oaodv_control_within toy_simple_labels otoy_trans, cterms_intros]
  oseq_step_invariant_ctermsI [OF toy_wf oaodv_control_within toy_simple_labels otoy_trans, cterms_intros]

subsection "Predicates"

definition msg_sender :: "msg ⇒ ip"
where "msg_sender m ≡ case m of Pkt _ ipc ⇒ ipc"

lemma msg_sender_simps [simp]:
  "⋀d did sid. msg_sender (Pkt d sid) = sid"
  unfolding msg_sender_def by simp_all

abbreviation not_Pkt :: "msg ⇒ bool"
where "not_Pkt m ≡ case m of Pkt _ _ ⇒ False | _ ⇒ True"

definition nos_inc :: "state ⇒ state ⇒ bool"
where "nos_inc ξ ξ' ≡ (no ξ ≤ no ξ')"

definition msg_ok :: "(ip ⇒ state) ⇒ msg ⇒ bool"
where "msg_ok σ m ≡ case m of Pkt num' sid' ⇒ num' ≤ no (σ sid') | _ ⇒ True"

lemma msg_okI [intro]:
  assumes "⋀num' sid'. m = Pkt num' sid' ⟹ num' ≤ no (σ sid')"
    shows "msg_ok σ m"
  using assms unfolding msg_ok_def
  by (auto split: msg.split)

lemma msg_ok_Pkt [simp]:
  "msg_ok σ (Pkt data src) = (data ≤ no (σ src))"
  unfolding msg_ok_def by simp

lemma msg_ok_pkt [simp]:
  "msg_ok σ (pkt(data, src)) = (data ≤ no (σ src))"
  unfolding msg_ok_def by simp

lemma msg_ok_Newpkt [simp]:
  "msg_ok σ (Newpkt data dst)"
  unfolding msg_ok_def by simp

lemma msg_ok_newpkt [simp]:
  "msg_ok σ (newpkt(data, dst))"
  unfolding msg_ok_def by simp

subsection "Sequential Invariants"

lemma seq_no_leq_num:
  "ptoy i ⊫ onl Γ⇩T⇩O⇩Y (λ(ξ, l). l∈{PToy-:7..PToy-:8} ⟶ no ξ ≤ num ξ)"
  by inv_cterms

lemma seq_nos_incs:
  "ptoy i ⊫⇩A onll Γ⇩T⇩O⇩Y (λ((ξ, _), _, (ξ', _)). nos_inc ξ ξ')"
  unfolding nos_inc_def
  by (inv_cterms inv add: onl_invariant_sterms [OF toy_wf seq_no_leq_num])

lemma seq_nos_incs':
  "ptoy i ⊫⇩A (λ((ξ, _), _, (ξ', _)). nos_inc ξ ξ')"
  by (rule step_invariant_weakenE [OF seq_nos_incs]) (auto dest!: onllD)

lemma sender_ip_valid:
  "ptoy i ⊫⇩A onll Γ⇩T⇩O⇩Y (λ((ξ, _), a, _). anycast (λm. msg_sender m = id ξ) a)"
  by inv_cterms

lemma id_constant:
  "ptoy i ⊫ onl Γ⇩T⇩O⇩Y (λ(ξ, _). id ξ = i)"
  by inv_cterms (simp add: σ⇩T⇩O⇩Y_def)

lemma nhid_eq_id:
  "ptoy i ⊫ onl Γ⇩T⇩O⇩Y (λ(ξ, l). l∈{PToy-:2..PToy-:8} ⟶ nhid ξ = id ξ)"
  by inv_cterms

lemma seq_msg_ok:
  "ptoy i ⊫⇩A onll Γ⇩T⇩O⇩Y (λ((ξ, _), a, _).
                anycast (λm. case m of Pkt num' sid' ⇒ num' = no ξ ∧ sid' = i | _ ⇒ True) a)"
  by (inv_cterms inv add: onl_invariant_sterms [OF toy_wf id_constant])

lemma nhid_eq_i:
  "ptoy i ⊫ onl Γ⇩T⇩O⇩Y (λ(ξ, l). l∈{PToy-:2..PToy-:8} ⟶ nhid ξ = i)"
  proof (rule invariant_arbitraryI, clarify intro!: onlI impI)
    fix ξ p l n
    assume "(ξ, p) ∈ reachable (ptoy i) TT"
       and "l ∈ labels Γ⇩T⇩O⇩Y p"
       and "l ∈ {PToy-:2..PToy-:8}"
    from this(1-3) have "nhid ξ = id ξ"
      by - (drule invariantD [OF nhid_eq_id], auto)
    moreover with ‹(ξ, p) ∈ reachable (ptoy i) TT› and ‹l ∈ labels Γ⇩T⇩O⇩Y p› have "id ξ = i"
      by (auto dest: invariantD [OF id_constant])
    ultimately show "nhid ξ = i"
      by simp
  qed

subsection "Global Invariants"

lemma nos_incD [dest]:
  assumes "nos_inc ξ ξ'"
    shows "no ξ ≤ no ξ'"
  using assms unfolding nos_inc_def .

lemma nos_inc_simp [simp]:
  "nos_inc ξ ξ' = (no ξ ≤ no ξ')"
  unfolding nos_inc_def ..

lemmas oseq_nos_incs =
  open_seq_step_invariant [OF seq_nos_incs initiali_toy otoy_trans toy_trans,
                           simplified seqll_onll_swap]

lemmas oseq_no_leq_num =
  open_seq_invariant [OF seq_no_leq_num initiali_toy otoy_trans toy_trans,
                      simplified seql_onl_swap]

lemma all_nos_inc:
  shows "optoy i ⊨⇩A (otherwith nos_inc {i} S,
                      other nos_inc {i} →)
                       onll Γ⇩T⇩O⇩Y (λ((σ, _), a, (σ', _)). (∀j. nos_inc (σ j) (σ' j)))"
  proof -
    have *: "⋀σ σ' a. ⟦ otherwith nos_inc {i} S σ σ' a; no (σ i) ≤ no (σ' i) ⟧
                       ⟹ ∀j. no (σ j) ≤ no (σ' j)"
      by (auto dest!: otherwith_syncD)
    show ?thesis
      by (inv_cterms
            inv add: oseq_step_invariant_sterms [OF oseq_nos_incs [THEN oinvariant_step_anyact]
                                                                                   toy_wf otoy_trans]
            simp add: seqllsimp) (auto elim!: *)
  qed

lemma oreceived_msg_inv:
  assumes other: "⋀σ σ' m. ⟦ P σ m; other Q {i} σ σ' ⟧ ⟹ P σ' m"
      and local: "⋀σ m. P σ m ⟹ P (σ(i := σ i⦇msg := m⦈)) m"
    shows "optoy i ⊨ (otherwith Q {i} (orecvmsg P), other Q {i} →)
                       onl Γ⇩T⇩O⇩Y (λ(σ, l). l ∈ {PToy-:1} ⟶ P σ (msg (σ i)))"
  proof (inv_cterms, intro impI)
    fix σ σ' l
    assume "l = PToy-:1 ⟶ P σ (msg (σ i))"
       and "l = PToy-:1"
       and "other Q {i} σ σ'"
    from this(1-2) have "P σ (msg (σ i))" ..
    hence "P σ' (msg (σ i))" using ‹other Q {i} σ σ'›
      by (rule other)
    moreover from ‹other Q {i} σ σ'› have "σ' i = σ i" ..
    ultimately show "P σ' (msg (σ' i))" by simp
  next
    fix σ σ' msg
    assume "otherwith Q {i} (orecvmsg P) σ σ' (receive msg)"
       and "σ' i = σ i⦇msg := msg⦈"
    from this(1) have "P σ msg"
                 and "∀j. j≠i ⟶ Q (σ j) (σ' j)" by auto
    from this(1) have "P (σ(i := σ i⦇msg := msg⦈)) msg" by (rule local)
    thus "P σ' msg"
    proof (rule other)
      from ‹σ' i = σ i⦇msg := msg⦈› and ‹∀j. j≠i ⟶ Q (σ j) (σ' j)›
        show "other Q {i} (σ(i := σ i⦇msg := msg⦈)) σ'"
          by - (rule otherI, auto)
    qed
  qed

lemma msg_ok_other_nos_inc [elim]:
  assumes "msg_ok σ m"
      and "other nos_inc {i} σ σ'"
    shows "msg_ok σ' m"
  proof (cases m)
    fix num sid
    assume "m = Pkt num sid"
    with ‹msg_ok σ m› have "num ≤ no (σ sid)" by simp
    also from ‹other nos_inc {i} σ σ'› have "no (σ sid) ≤ no (σ' sid)"
      by (rule otherE) (metis eq_iff nos_incD)
    finally have "num ≤ no (σ' sid)" .
    with ‹m = Pkt num sid› show ?thesis
      by simp
  qed simp

lemma msg_ok_no_leq_no [simp, elim]:
  assumes "msg_ok σ m"
      and "∀j. no (σ j) ≤ no (σ' j)"
    shows "msg_ok σ' m"
  using assms(1) proof (cases m)
    fix num sid
    assume "m = Pkt num sid"
    with ‹msg_ok σ m› have "num ≤ no (σ sid)" by simp
    also from ‹∀j. no (σ j) ≤ no (σ' j)› have "no (σ sid) ≤ no (σ' sid)"
      by simp
    finally have "num ≤ no (σ' sid)" .
    with ‹m = Pkt num sid› show ?thesis
      by simp
  qed (simp add: assms(1))

lemma oreceived_msg_ok:
  "optoy i ⊨ (otherwith nos_inc {i} (orecvmsg msg_ok),
               other nos_inc {i} →)
              onl Γ⇩T⇩O⇩Y (λ(σ, l). l∈{PToy-:1..} ⟶ msg_ok σ (msg (σ i)))"
  (is "_ ⊨ (?S, ?U →) _")
  proof (inv_cterms inv add: oseq_step_invariant_sterms [OF all_nos_inc toy_wf otoy_trans],
         intro impI, elim impE)
    fix σ σ'
    assume "msg_ok σ (msg (σ i))"
       and other: "other nos_inc {i} σ σ'"
    moreover from other have "msg (σ' i) = msg (σ i)"
      by (clarsimp elim!: otherE)
    ultimately show "msg_ok σ' (msg (σ' i))"
      by (auto)
  next
    fix p l σ a q l' σ' pp p' m
    assume a1: "(σ', p') ∈ oreachable (optoy i) ?S ?U"
       and a2: "PToy-:1 ∈ labels Γ⇩T⇩O⇩Y p'"
       and a3: "σ' i = σ i⦇msg := m⦈"
    have inv: "optoy i ⊨ (?S, ?U →) onl Γ⇩T⇩O⇩Y (λ(σ, l). l ∈ {PToy-:1} ⟶ msg_ok σ (msg (σ i)))"
    proof (rule oreceived_msg_inv)
      fix σ σ' m
      assume "msg_ok σ m"
         and "other nos_inc {i} σ σ'"
      thus "msg_ok σ' m" ..
    next
      fix σ m
      assume "msg_ok σ m"
      thus "msg_ok (σ(i := σ i⦇msg := m⦈)) m"
        by (cases m) auto
    qed
    from a1 a2 a3 show "msg_ok σ' m"
      by (clarsimp dest!: oinvariantD [OF inv] onlD)
  qed simp

lemma is_pkt_handler_num_leq_no:
  shows "optoy i ⊨ (otherwith nos_inc {i} (orecvmsg msg_ok),
                      other nos_inc {i} →)
                    onl Γ⇩T⇩O⇩Y (λ(σ, l). l∈{PToy-:6..PToy-:10} ⟶ num (σ i) ≤ no (σ (sid (σ i))))"
  proof -
    { fix σ σ'
      assume "∀j. no (σ j) ≤ no (σ' j)"
         and "num (σ i) ≤ no (σ (sid (σ i)))"
      have "num (σ i) ≤ no (σ' (sid (σ i)))"
      proof -
        note ‹num (σ i) ≤ no (σ (sid (σ i)))›
        also from ‹∀j. no (σ j) ≤ no (σ' j)› have "no (σ (sid (σ i))) ≤ no (σ' (sid (σ i)))"
          by auto
        finally show ?thesis .
      qed
    } note solve_step = this
    show ?thesis
    proof (inv_cterms inv add: oseq_step_invariant_sterms [OF all_nos_inc toy_wf otoy_trans]
                               onl_oinvariant_sterms [OF toy_wf oreceived_msg_ok]
                        solve: solve_step, intro impI, elim impE)
      fix σ σ'
      assume *: "num (σ i) ≤ no (σ (sid (σ i)))"
         and "other nos_inc {i} σ σ'"
      from this(2) obtain "∀i∈{i}. σ' i = σ i"
                      and "∀j. j ∉ {i} ⟶ nos_inc (σ j) (σ' j)" ..
      show "num (σ' i) ≤ no (σ' (sid (σ' i)))"      
      proof (cases "sid (σ i) = i")
        assume "sid (σ i) = i"
        with * ‹∀i∈{i}. σ' i = σ i›
        show ?thesis by simp
      next
        assume "sid (σ i) ≠ i"
        with ‹∀j. j ∉ {i} ⟶ nos_inc (σ j) (σ' j)›
          have "no (σ (sid (σ i))) ≤ no (σ' (sid (σ i)))" by simp
        with * ‹∀i∈{i}. σ' i = σ i›
        show ?thesis by simp
      qed
    next
      fix p l σ a q l' σ' pp p'
      assume "msg_ok σ (msg (σ i))"
         and "∀j. no (σ j) ≤ no (σ' j)"
         and "σ' i ∈ is_pkt (σ i)"
      show "num (σ' i) ≤ no (σ' (sid (σ' i)))"
      proof (cases "msg (σ i)")
        fix num' sid'
        assume "msg (σ i) = Pkt num' sid'"
        with ‹σ' i ∈ is_pkt (σ i)› obtain "num (σ' i) = num'"
                                      and "sid (σ' i) = sid'"
          unfolding is_pkt_def by auto
        with ‹msg (σ i) = Pkt num' sid'› and ‹msg_ok σ (msg (σ i))›
          have "num (σ' i) ≤ no (σ (sid (σ' i)))"
            by simp
        also from ‹∀j. no (σ j) ≤ no (σ' j)› have "no (σ (sid (σ' i))) ≤ no (σ' (sid (σ' i)))" ..
        finally show ?thesis .
      next
        fix num' sid'
        assume "msg (σ i) = Newpkt num' sid'"
        with ‹σ' i ∈ is_pkt (σ i)› have False
          unfolding is_pkt_def by simp
        thus ?thesis ..
      qed
    qed
  qed

lemmas oseq_id_constant =
  open_seq_invariant [OF id_constant initiali_toy otoy_trans toy_trans,
                      simplified seql_onl_swap]

lemmas oseq_nhid_eq_i =
  open_seq_invariant [OF nhid_eq_i initiali_toy otoy_trans toy_trans,
                      simplified seql_onl_swap]
  
lemmas oseq_nhid_eq_id =
  open_seq_invariant [OF nhid_eq_id initiali_toy otoy_trans toy_trans,
                      simplified seql_onl_swap]

lemma oseq_bigger_than_next:
  shows "optoy i ⊨ (otherwith nos_inc {i} (orecvmsg msg_ok),
                      other nos_inc {i} →) global (λσ. no (σ i) ≤ no (σ (nhid (σ i))))"
    (is "_ ⊨ (?S, ?U →) ?P")
  proof -
    have nhidinv: "optoy i ⊨ (?S, ?U →)
                              onl Γ⇩T⇩O⇩Y (λ(σ, l). l∈{PToy-:2..PToy-:8}
                                                    ⟶ nhid (σ i) = id (σ i))"
      by (rule oinvariant_weakenE [OF oseq_nhid_eq_id]) (auto simp: seqlsimp)
    have idinv: "optoy i ⊨ (?S, ?U →) onl Γ⇩T⇩O⇩Y (λ(σ, l). id (σ i) = i)"
      by (rule oinvariant_weakenE [OF oseq_id_constant]) (auto simp: seqlsimp)
    { fix σ σ' a
      assume "no (σ i) ≤ no (σ (nhid (σ i)))"
         and "∀j. nos_inc (σ j) (σ' j)"
      note this(1)
      also from ‹∀j. nos_inc (σ j) (σ' j)› have "no (σ (nhid (σ i))) ≤ no (σ' (nhid (σ i)))"
        by auto
      finally have "no (σ i) ≤ no (σ' (nhid (σ i)))" ..
    } note * = this
    have "optoy i ⊨ (otherwith nos_inc {i} (orecvmsg msg_ok),
                      other nos_inc {i} →)
                     onl Γ⇩T⇩O⇩Y (λ(σ, l). no (σ i) ≤ no (σ (nhid (σ i))))"
    proof (inv_cterms
             inv add: onl_oinvariant_sterms [OF toy_wf oseq_no_leq_num [THEN oinvariant_anyact]]
                      oseq_step_invariant_sterms [OF all_nos_inc toy_wf otoy_trans]
                      onl_oinvariant_sterms [OF toy_wf is_pkt_handler_num_leq_no]
                      onl_oinvariant_sterms [OF toy_wf nhidinv]
                      onl_oinvariant_sterms [OF toy_wf idinv]
             simp add: seqlsimp seqllsimp
             simp del: nos_inc_simp
                solve: *)
      fix σ p l
      assume "(σ, p) ∈ σ⇩O⇩T⇩O⇩Y"
      thus "no (σ i) ≤ no (σ (nhid (σ i)))"
        by (simp add: σ⇩O⇩T⇩O⇩Y_def)
    next
      fix σ σ' p l
      assume or: "(σ, p) ∈ oreachable (optoy i) ?S ?U"
         and "l ∈ labels Γ⇩T⇩O⇩Y p"
         and "no (σ i) ≤ no (σ (nhid (σ i)))"
         and "other nos_inc {i} σ σ'"
      show "no (σ' i) ≤ no (σ' (nhid (σ' i)))"
      proof (cases "nhid (σ' i) = i")
        assume "nhid (σ' i) = i"
        with ‹no (σ i) ≤ no (σ (nhid (σ i)))› show ?thesis
          by simp
      next
        assume "nhid (σ' i) ≠ i"
        moreover from ‹other nos_inc {i} σ σ'› [THEN other_localD] have "σ' i = σ i"
          by simp
        ultimately have "no (σ (nhid (σ i))) ≤ no (σ' (nhid (σ' i)))"
          using ‹other nos_inc {i} σ σ'› and ‹σ' i = σ i› by (auto)
        with ‹no (σ i) ≤ no (σ (nhid (σ i)))› and ‹σ' i = σ i› show ?thesis
          by simp
      qed
    next
      fix p l σ a q l' σ' pp p'
      assume "no (σ i) ≤ num (σ i)"
         and "num (σ i) ≤ no (σ (sid (σ i)))"
         and "∀j. nos_inc (σ j) (σ' j)"
      from this(1-2) have "no (σ i) ≤ no (σ (sid (σ i)))"
        by (rule le_trans)
      also from ‹∀j. nos_inc (σ j) (σ' j)›
        have "no (σ (sid (σ i))) ≤ no (σ' (sid (σ i)))"
          by auto
      finally show "no (σ i) ≤ no (σ' (sid (σ i)))" ..
    qed
    thus ?thesis
      by (rule oinvariant_weakenE)
         (auto simp: onl_def)
  qed

lemma anycast_weakenE [elim]:
  assumes "anycast P a"
      and "⋀m. P m ⟹ Q m"
  shows "anycast Q a"
  using assms unfolding anycast_def
  by (auto split: seq_action.split)

lemma oseq_msg_ok:
  "optoy i ⊨⇩A (act TT, other U {i} →) globala (λ(σ, a, _). anycast (msg_ok σ) a)"
  by (rule ostep_invariant_weakenE [OF open_seq_step_invariant
            [OF seq_msg_ok initiali_toy otoy_trans toy_trans, simplified seql_onl_swap]])
     (auto simp: seqllsimp dest!: onllD elim!: anycast_weakenE intro!: msg_okI)

subsection "Lifting"

lemma opar_bigger_than_next:
  shows "optoy i ⟨⟨⇘i⇙ qmsg ⊨ (otherwith nos_inc {i} (orecvmsg msg_ok),
                      other nos_inc {i} →) global (λσ. no (σ i) ≤ no (σ (nhid (σ i))))"
  proof (rule lift_into_qmsg [OF oseq_bigger_than_next])
    fix σ σ' m
    assume "∀j. nos_inc (σ j) (σ' j)"
       and "msg_ok σ m"
    from this(2) show "msg_ok σ' m"
    proof (cases m, simp only: msg_ok_Pkt)
      fix num' sid'
      assume "num' ≤ no (σ sid')"
      also from ‹∀j. nos_inc (σ j) (σ' j)› have "no (σ sid') ≤ no (σ' sid')"
        by simp
      finally show "num' ≤ no (σ' sid')" .
    qed simp
  next
    show "optoy i ⊨⇩A (otherwith nos_inc {i} (orecvmsg msg_ok), other nos_inc {i} →)
                      globala (λ(σ, _, σ'). nos_inc (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF open_seq_step_invariant
                                         [OF seq_nos_incs initiali_toy otoy_trans toy_trans]])
         (auto simp: seqllsimp dest!: onllD)
  qed simp

lemma onode_bigger_than_next:
  "⟨i : optoy i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o
     ⊨ (otherwith nos_inc {i} (oarrivemsg msg_ok), other nos_inc {i} →)
        global (λσ. no (σ i) ≤ no (σ (nhid (σ i))))"
  by (rule node_lift [OF opar_bigger_than_next])

lemma node_local_nos_inc:
  "⟨i : optoy i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o ⊨⇩A (λσ _. oarrivemsg (λ_ _. True) σ, other (λ_ _. True) {i} →)
                                     globala (λ(σ, _, σ'). nos_inc (σ i) (σ' i))"
  proof (rule node_lift_step_statelessassm)
    have "optoy i ⊨⇩A (λσ _. orecvmsg (λ_ _. True) σ, other (λ_ _. True) {i} →)
                      globala (λ(σ, _, σ'). nos_inc (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF oseq_nos_incs])
         (auto simp: seqllsimp dest!: onllD)
    thus "optoy i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_ _. True) σ, other (λ_ _. True) {i} →)
                                globala (λ(σ, _, σ'). nos_inc (σ i) (σ' i))"
      by (rule lift_step_into_qmsg_statelessassm) auto
  qed simp

lemma opnet_bigger_than_next:
  "opnet (λi. optoy i ⟨⟨⇘i⇙ qmsg) n
     ⊨ (otherwith nos_inc (net_tree_ips n) (oarrivemsg msg_ok),
         other nos_inc (net_tree_ips n) →)
        global (λσ. ∀i∈net_tree_ips n. no (σ i) ≤ no (σ (nhid (σ i))))"
  proof (rule pnet_lift [OF onode_bigger_than_next])
    fix i R⇩i
    have "⟨i : optoy i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o ⊨⇩A (λσ _. oarrivemsg msg_ok σ, other (λ_ _. True) {i} →)
                                            globala (λ(σ, a, _). castmsg (msg_ok σ) a)"
    proof (rule node_lift_anycast_statelessassm)
      have "optoy i ⊨⇩A (λσ _. orecvmsg (λ_ _. True) σ, other (λ_ _. True) {i} →)
                        globala (λ(σ, a, _). anycast (msg_ok σ) a)"
        by (rule ostep_invariant_weakenE [OF oseq_msg_ok]) auto
      hence "optoy i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_ _. True) σ, other (λ_ _. True) {i} →)
                                   globala (λ(σ, a, _). anycast (msg_ok σ) a)"
        by (rule lift_step_into_qmsg_statelessassm) auto
      thus "optoy i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg msg_ok σ, other (λ_ _. True) {i} →)
                                  globala (λ(σ, a, _). anycast (msg_ok σ) a)"
        by (rule ostep_invariant_weakenE) auto
    qed
    thus "⟨i : optoy i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o ⊨⇩A (λσ _. oarrivemsg msg_ok σ, other nos_inc {i} →)
                                            globala (λ(σ, a, _). castmsg (msg_ok σ) a)"
      by (rule ostep_invariant_weakenE) auto
  next
    fix i R⇩i
    show "⟨i : optoy i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o ⊨⇩A (λσ _. oarrivemsg msg_ok σ,
                                            other nos_inc {i} →)
             globala (λ(σ, a, σ'). a ≠ τ ∧ (∀d. a ≠ i:deliver(d)) ⟶ nos_inc (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF node_local_nos_inc]) auto
  next
    fix i R
    show "⟨i : optoy i ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg msg_ok σ,
                                           other nos_inc {i} →)
             globala (λ(σ, a, σ'). a = τ ∨ (∃d. a = i:deliver(d)) ⟶ nos_inc (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF node_local_nos_inc]) auto
  qed simp_all

lemma ocnet_bigger_than_next:
  "oclosed (opnet (λi. optoy i ⟨⟨⇘i⇙ qmsg) n)
     ⊨ (λ_ _ _. True, other nos_inc (net_tree_ips n) →)
        global (λσ. ∀i∈net_tree_ips n. no (σ i) ≤ no (σ (nhid (σ i))))"
  proof (rule inclosed_closed)
    show "opnet (λi. optoy i ⟨⟨⇘i⇙ qmsg) n
            ⊨ (otherwith (=) (net_tree_ips n) inoclosed, other nos_inc (net_tree_ips n) →)
               global (λσ. ∀i∈net_tree_ips n. no (σ i) ≤ no (σ (nhid (σ i))))"
    proof (rule oinvariant_weakenE [OF opnet_bigger_than_next])
      fix s s':: "nat ⇒ state" and a :: "msg node_action"
      assume "otherwith (=) (net_tree_ips n) inoclosed s s' a"
      thus "otherwith nos_inc (net_tree_ips n) (oarrivemsg msg_ok) s s' a"
      proof (rule otherwithE, intro otherwithI)
        assume "inoclosed s a"
           and "∀j. j ∉ net_tree_ips n ⟶ s j = s' j"
           and "otherwith ((=)) (net_tree_ips n) inoclosed s s' a"
        thus "oarrivemsg msg_ok s a"
          by (cases a) auto
      qed auto
    qed simp
  qed

subsection "Transfer"

definition
  initmissing :: "(nat ⇒ state option) × 'a ⇒ (nat ⇒ state) × 'a"
where
  "initmissing σ = (λi. case (fst σ) i of None ⇒ toy_init i | Some s ⇒ s, snd σ)"

lemma not_in_net_ips_fst_init_missing [simp]:
  assumes "i ∉ net_ips σ"
    shows "fst (initmissing (netgmap fst σ)) i = toy_init i"
  using assms unfolding initmissing_def by simp

lemma fst_initmissing_netgmap_pair_fst [simp]:
  "fst (initmissing (netgmap (λ(p, q). (fst (Fun.id p), snd (Fun.id p), q)) s))
                                               = fst (initmissing (netgmap fst s))"
  unfolding initmissing_def by auto

interpretation toy_openproc: openproc ptoy optoy Fun.id
  rewrites "toy_openproc.initmissing = initmissing"
  proof -
    show "openproc ptoy optoy Fun.id"
    proof unfold_locales
      fix i :: ip
      have "{(σ, ζ). (σ i, ζ) ∈ σ⇩T⇩O⇩Y i ∧ (∀j. j ≠ i ⟶ σ j ∈ fst ` σ⇩T⇩O⇩Y j)} ⊆ σ⇩O⇩T⇩O⇩Y"
        unfolding σ⇩T⇩O⇩Y_def σ⇩O⇩T⇩O⇩Y_def
        proof (rule equalityD1)
          show "⋀f p. {(σ, ζ). (σ i, ζ) ∈ {(f i, p)} ∧ (∀j. j ≠ i
                      ⟶ σ j ∈ fst ` {(f j, p)})} = {(f, p)}"
            by (rule set_eqI) auto
        qed
      thus "{ (σ, ζ) |σ ζ s. s ∈ init (ptoy i)
                             ∧ (σ i, ζ) = Fun.id s
                             ∧ (∀j. j≠i ⟶ σ j ∈ (fst o Fun.id) ` init (ptoy j)) } ⊆ init (optoy i)"
        by simp
    next
      show "∀j. init (ptoy j) ≠ {}"
        unfolding σ⇩T⇩O⇩Y_def by simp
    next
      fix i s a s' σ σ'
      assume "σ i = fst (Fun.id s)"
         and "σ' i = fst (Fun.id s')"
         and "(s, a, s') ∈ trans (ptoy i)"
      then obtain q q' where "s = (σ i, q)"
                         and "s' = (σ' i, q')"
                         and "((σ i, q), a, (σ' i, q')) ∈ trans (ptoy i)" 
         by (cases s, cases s') auto
      from this(3) have "((σ, q), a, (σ', q')) ∈ trans (optoy i)"
        by simp (rule open_seqp_action [OF toy_wf])

      with ‹s = (σ i, q)› and ‹s' = (σ' i, q')›
        show "((σ, snd (Fun.id s)), a, (σ', snd (Fun.id s'))) ∈ trans (optoy i)"
          by simp
    qed
    then interpret op0: openproc ptoy optoy Fun.id .
    have [simp]: "⋀i. (SOME x. x ∈ (fst o Fun.id) ` init (ptoy i)) = toy_init i"
      unfolding σ⇩T⇩O⇩Y_def by simp
    hence "⋀i. openproc.initmissing ptoy Fun.id i = initmissing i"
      unfolding op0.initmissing_def op0.someinit_def initmissing_def
      by (auto split: option.split)
    thus "openproc.initmissing ptoy Fun.id = initmissing" ..
  qed

lemma fst_initmissing_netgmap_default_toy_init_netlift:
  "fst (initmissing (netgmap sr s)) = default toy_init (netlift sr s)"
  unfolding initmissing_def default_def
  by (simp add: fst_netgmap_netlift del: One_nat_def)

definition
  netglobal :: "((nat ⇒ state) ⇒ bool) ⇒ ((state × 'b) × 'c) net_state ⇒ bool"
where
  "netglobal P ≡ (λs. P (default toy_init (netlift fst s)))"

interpretation toy_openproc_par_qmsg: openproc_parq ptoy optoy Fun.id qmsg
  rewrites "toy_openproc_par_qmsg.netglobal = netglobal"
    and "toy_openproc_par_qmsg.initmissing = initmissing"
  proof -
    show "openproc_parq ptoy optoy Fun.id qmsg"
      by (unfold_locales) simp
    then interpret opq: openproc_parq ptoy optoy Fun.id qmsg .

    have im: "⋀σ. openproc.initmissing (λi. ptoy i ⟨⟨ qmsg) (λ(p, q). (fst (Fun.id p), snd (Fun.id p), q)) σ
                                                                                    = initmissing σ"
      unfolding opq.initmissing_def opq.someinit_def initmissing_def
      unfolding σ⇩T⇩O⇩Y_def σ⇩Q⇩M⇩S⇩G_def by (clarsimp cong: option.case_cong)
    thus "openproc.initmissing (λi. ptoy i ⟨⟨ qmsg) (λ(p, q). (fst (Fun.id p), snd (Fun.id p), q)) = initmissing"
      by (rule ext)

    have "⋀P σ. openproc.netglobal (λi. ptoy i ⟨⟨ qmsg) (λ(p, q). (fst (Fun.id p), snd (Fun.id p), q)) P σ
                                                                                = netglobal P σ"
      unfolding opq.netglobal_def netglobal_def opq.initmissing_def initmissing_def opq.someinit_def
      unfolding σ⇩T⇩O⇩Y_def σ⇩Q⇩M⇩S⇩G_def
      by (clarsimp cong: option.case_cong
                   simp del: One_nat_def
                   simp add: fst_initmissing_netgmap_default_toy_init_netlift
                                                  [symmetric, unfolded initmissing_def])
    thus "openproc.netglobal (λi. ptoy i ⟨⟨ qmsg) (λ(p, q). (fst (Fun.id p), snd (Fun.id p), q)) = netglobal"
      by auto
  qed

subsection "Final result"

lemma bigger_than_next:
  assumes "wf_net_tree n"
  shows "closed (pnet (λi. ptoy i ⟨⟨ qmsg) n) ⊫ netglobal (λσ. ∀i. no (σ i) ≤ no (σ (nhid (σ i))))"
        (is "_ ⊫ netglobal (λσ. ∀i. ?inv σ i)")
  proof -
    from ‹wf_net_tree n›
      have proto: "closed (pnet (λi. ptoy i ⟨⟨ qmsg) n)
                      ⊫ netglobal (λσ. ∀i∈net_tree_ips n. no (σ i) ≤ no (σ (nhid (σ i))))"
        by (rule toy_openproc_par_qmsg.close_opnet [OF _ ocnet_bigger_than_next])
    show ?thesis
    unfolding invariant_def opnet_sos.opnet_tau1
    proof (rule, simp only: toy_openproc_par_qmsg.netglobalsimp
                            fst_initmissing_netgmap_pair_fst, rule allI)
      fix σ i
      assume sr: "σ ∈ reachable (closed (pnet (λi. ptoy i ⟨⟨ qmsg) n)) TT"
      hence "∀i∈net_tree_ips n. ?inv (fst (initmissing (netgmap fst σ))) i"
        by - (drule invariantD [OF proto],
              simp only: toy_openproc_par_qmsg.netglobalsimp
                         fst_initmissing_netgmap_pair_fst)
      thus "?inv (fst (initmissing (netgmap fst σ))) i"
      proof (cases "i∈net_tree_ips n")
        assume "i∉net_tree_ips n"
        from sr have "σ ∈ reachable (pnet (λi. ptoy i ⟨⟨ qmsg) n) TT" ..
        hence "net_ips σ = net_tree_ips n" ..
        with ‹i∉net_tree_ips n› have "i∉net_ips σ" by simp
        hence "(fst (initmissing (netgmap fst σ))) i = toy_init i"
          by simp
        thus ?thesis by simp
      qed metis
    qed
  qed

end