Quelle  Toy.thy

(*  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 Γ_TOY :: "(state, msg, pseqp, pseqp label) seqp_env"
where
  "Γ_TOY 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 Γ_TOY.simps [simp del, code del]
lemmas Γ_{TOY_simps} [simp, code] = Γ_TOY.simps [simplified]

fun Γ_{TOY_skeleton}
where "Γ_{TOY_skeleton} PToy = seqp_skeleton (Γ_TOY PToy)"

lemma Γ_{TOY_skeleton_wf} [simp]:
  "wellformed Γ_{TOY_skeleton}"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ_{TOY_skeleton} pn)"
      by (cases pn) simp_all
  qed

declare Γ_{TOY_skeleton}.simps [simp del, code del]
lemmas Γ_{TOY_skeleton_simps} [simp, code] = Γ_{TOY_skeleton}.simps [simplified Γ_{TOY_simps} seqp_skeleton.simps]

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

definition σ_TOY :: "ip ==> (state × (state, msg, pseqp, pseqp label) seqp) set"
where "σ_TOY i ≡ {(toy_init i, Γ_TOY PToy)}"

abbreviation ptoy
  :: "ip ==> (state × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "ptoy i ≡ ( init = σ_TOY i, trans = seqp_sos Γ_TOY )"

lemma toy_trans: "trans (ptoy i) = seqp_sos Γ_TOY"
  by simp

lemma toy_control_within [simp]: "control_within Γ_TOY (init (ptoy i))"
  unfolding σ_{TOY_def} by (rule control_withinI) (auto simp del: Γ_{TOY_simps})

lemma toy_wf [simp]:
  "wellformed Γ_TOY"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ_TOY 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 Γ_TOY p"
  by (metis toy_labels_not_empty all_not_in_conv)

lemma toy_ex_labelE [elim]:
  assumes "∀l∈labels Γ_TOY 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 Γ_TOY"
  proof
    fix pn p
    assume "p∈subterms(Γ_TOY pn)"
    thus "∃!l. labels Γ_TOY p = {l}"
    by (cases pn) (simp_all cong: seqp_congs | elim disjE)+
  qed

lemma σ_{TOY_labels} [simp]: "(ξ, p) ∈ σ_TOY i ==> labels Γ_TOY p = {PToy-:0}"
  unfolding σ_{TOY_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
  Γ_{TOY_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 σ_OTOY :: "((ip ==> state) × ((state, msg, pseqp, pseqp label) seqp)) set"
where "σ_OTOY ≡ {(toy_init, Γ_TOY PToy)}"

abbreviation optoy
  :: "ip ==> ((ip ==> state) × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "optoy i ≡ ( init = σ_OTOY, trans = oseqp_sos Γ_TOY i )"

lemma initiali_toy [intro!, simp]: "initiali i (init (optoy i)) (init (ptoy i))"
  unfolding σ_{TOY_def} σ_{OTOY_def} by rule simp_all

lemma oaodv_control_within [simp]: "control_within Γ_TOY (init (optoy i))"
  unfolding σ_{OTOY_def} by (rule control_withinI) (auto simp del: Γ_{TOY_simps})

lemma σ_{OTOY_labels} [simp]: "(σ, p) ∈ σ_OTOY ==> labels Γ_TOY p = {PToy-:0}"
  unfolding σ_{OTOY_def} by simp

lemma otoy_trans: "trans (optoy i) = oseqp_sos Γ_TOY 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 Γ_TOY (λ(ξ, l). l∈{PToy-:7..PToy-:8} ⟶ no ξ ≤ num ξ)"
  by inv_cterms

lemma seq_nos_incs:
  "ptoy i ⊨!!!_A onll Γ_TOY (λ((ξ, _), _, (ξ', _)). 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 Γ_TOY (λ((ξ, _), a, _). anycast (λm. msg_sender m = id ξ) a)"
  by inv_cterms

lemma id_constant:
  "ptoy i ⊨!!! onl Γ_TOY (λ(ξ, _). id ξ = i)"
  by inv_cterms (simp add: σ_{TOY_def})

lemma nhid_eq_id:
  "ptoy i ⊨!!! onl Γ_TOY (λ(ξ, l). l∈{PToy-:2..PToy-:8} ⟶ nhid ξ = id ξ)"
  by inv_cterms

lemma seq_msg_ok:
  "ptoy i ⊨!!!_A onll Γ_TOY (λ((ξ, _), 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 Γ_TOY (λ(ξ, 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 Γ_TOY 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 Γ_TOY 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 Γ_TOY (λ((σ, _), 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 Γ_TOY (λ(σ, 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 Γ_TOY (λ(σ, 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 Γ_TOY p'"
       and a3: "σ' i = σ i(msg := m)"
    have inv: "optoy i ⊨ (?S, ?U →) onl Γ_TOY (λ(σ, 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 Γ_TOY (λ(σ, 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 Γ_TOY (λ(σ, 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 Γ_TOY (λ(σ, 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 Γ_TOY (λ(σ, 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) ∈ σ_OTOY"
      thus "no (σ i) ≤ no (σ (nhid (σ i)))"
        by (simp add: σ_{OTOY_def})
    next
      fix σ σ' p l
      assume or: "(σ, p) ∈ oreachable (optoy i) ?S ?U"
         and "l ∈ labels Γ_TOY 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ qmsg ⊨_A (λσ _. orecvmsg (λ_ _. True) σ, other (λ_ _. True) {i} →)
                                   globala (λ(σ, a, _). anycast (msg_ok σ) a)"
        by (rule lift_step_into_qmsg_statelessassm) auto
      thus "optoy 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ 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 ⟨⟨ 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, ζ) ∈ σ_TOY i ∧ (∀j. j ≠ i ⟶ σ j ∈ fst ` σ<sub>TOY</sub> j)} ⊆ σ<sub>OTOY</sub>"
        unfolding σ<sub>TOY_def</sub> σ<sub>OTOY_def</sub>
        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 σ_{TOY_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 σ_{TOY_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 σ_{TOY_def} σ_{QMSG_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 σ_{TOY_def} σ_{QMSG_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