Theory DYNAMIC_Post_ISSUER

theory DYNAMIC_Post_ISSUER
  imports
    "Post_Observation_Setup_ISSUER"
    DYNAMIC_Post_Value_Setup_ISSUER
    "Bounded_Deducibility_Security.Compositional_Reasoning"
begin


subsubsection ‹Issuer declassification bound›

text ‹\label{sec:dynamic-post-issuer}
We verify that a group of users of some node ‹i›,
allowed to take normal actions to the system and observe their outputs
\emph{and additionally allowed to observe communication},
can learn nothing about the updates to a post located at node ‹i›
and the sends of that post to other nodes beyond:

(1) the updates that occur during the times when one of the following holds,
and the ∗‹last› update ∗‹before› one of the following holds
(because, for example, observers can see the current version of the post when it is made public):
\begin{itemize}
\item either a user in the group is the post's owner or the administrator
\item or a user in the group is a friend of the owner
\item or the group has at least one registered user and the post is marked "public"
\end{itemize}

(2) the presence of the sends (i.e., the number of the sending actions)

(3) the public knowledge that what is being sent is always the last version (modeled as
the correlation predicate)

See \<^cite>‹‹Appendix C› in "cosmedis-SandP2017"› for more details. This is the dynamic-trigger
(i.e., trigger-incorporating inductive bound) version of the property proved in
Section~\ref{sec:post-issuer}.
For a discussion of this ``while-or-last-before'' style of formalizing bounds,
see \<^cite>‹‹Section 3.4› in "cosmed-jar2018"› about the the corresponding property of CoSMed.
›

context Post
begin

fun T :: "(state,act,out) trans ⇒ bool" where "T _ = False"

inductive BC :: "value list ⇒ value list ⇒ bool"
and BO :: "value list ⇒ value list ⇒ bool"
where
 BC_PVal[simp,intro!]:
  "list_all (Not o isOVal) ul ⟹ list_all (Not o isOVal) ul1 ⟹
   map tgtAPI (filter isPValS ul) = map tgtAPI (filter isPValS ul1) ⟹
   (ul = [] ⟶ ul1 = [])
   ⟹ BC ul ul1"
|BC_BO[intro]:
  "BO vl vl1 ⟹
   list_all (Not o isOVal) ul ⟹ list_all (Not o isOVal) ul1 ⟹
   map tgtAPI (filter isPValS ul) = map tgtAPI (filter isPValS ul1) ⟹
   (ul = [] ⟷ ul1 = []) ⟹
   (ul ≠ [] ⟹ isPVal (last ul) ∧ last ul = last ul1) ⟹
   list_all isPValS sul
   ⟹
   BC (ul  @ sul @ OVal True # vl)
      (ul1 @ sul @ OVal True # vl1)"
(*  *)
|BO_PVal[simp,intro!]:
  "list_all (Not o isOVal) ul ⟹ BO ul ul"
|BO_BC[intro]:
  "BC vl vl1 ⟹
   list_all (Not o isOVal) ul
   ⟹
   BO (ul @ OVal False # vl) (ul @ OVal False # vl1)"

lemma list_all_filter_Not_isOVal:
assumes "list_all (Not ∘ isOVal) ul"
and "filter isPValS ul = []" and "filter isPVal ul = []"
shows "ul = []"
using assms value.exhaust_disc by (induct ul) auto

lemma BC_not_Nil: "BC vl vl1 ⟹ vl = [] ⟹ vl1 = []"
by(auto elim: BC.cases)

lemma BC_OVal_True:
assumes "BC (OVal True # vl') vl1"
shows "∃ vl1'. BO vl' vl1' ∧ vl1 = OVal True # vl1'"
proof-
  define vl where vl: "vl ≡ OVal True # vl'"
  have "BC vl vl1" using assms unfolding vl by auto
  thus ?thesis proof cases
    case (BC_BO vll vll1 ul ul1 sul)
    hence ul: "ul = []" unfolding vl apply simp
    by (metis (no_types) Post.value.disc(9) append_eq_Cons_conv
         list.map(2) list.pred_inject(2) list_all_map)
    have sul: "sul = []" using BC_BO unfolding vl ul apply simp
    by (metis Post.value.disc(6) append_eq_Cons_conv list.pred_inject(2))
    show ?thesis
    apply - apply(rule exI[of _ "vll1"])
    using BC_BO using list_all_filter_Not_isOVal[of ul1]
    unfolding ul sul vl by auto
  qed(unfold vl, auto)
qed

(* Correlation is defined to mean: always send what was last uploaded, or emptyPost
if nothing had been uploaded. This needs the auxiliary notion of "correlation from" *)
fun corrFrom :: "post ⇒ value list ⇒ bool" where
 "corrFrom pst [] = True"
|"corrFrom pst (PVal pstt # vl) = corrFrom pstt vl"
|"corrFrom pst (PValS aid pstt # vl) = (pst = pstt ∧ corrFrom pst vl)"
|"corrFrom pst (OVal b # vl) = (corrFrom pst vl)"


abbreviation corr :: "value list ⇒ bool" where "corr ≡ corrFrom emptyPost"

definition B where
"B vl vl1 ≡ BC vl vl1 ∧ corr vl1"

(* lemma vl_Nil_filter_not:
assumes "filter (%v. isPVal v ∨ isOVal v) Vl = [] ∧ filter (Not o isPVal) Vl = []"
shows "Vl = []"
using assms by (induct Vl) auto *)

lemma B_not_Nil:
assumes B: "B vl vl1" and vl: "vl = []"
shows "vl1 = []"
using B Post.BC_not_Nil Post.B_def vl by blast


sublocale BD_Security_IO where
istate = istate and step = step and
φ = φ and f = f and γ = γ and g = g and T = T and B = B
done

subsubsection ‹Issuer unwinding proof›

lemma reach_PublicV_imples_FriendV[simp]:
assumes "reach s"
and "vis s pid ≠ PublicV"
shows "vis s pid = FriendV"
using assms reach_vis by auto


(* major *) lemma eqButPID_step_γ_out:
assumes ss1: "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and op: "¬ open s"
and sT: "reachNT s" and s1: "reach s1"
and γ: "γ (Trans s a ou s')"
shows "(∃ uid p aid pid. a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
       ou = ou1"
proof-
  note [simp] = all_defs
                open_def
  note s = reachNT_reach[OF sT]
  note willUse =
    step step1 γ
    not_open_eqButPID[OF op ss1]
    reach_vis[OF s]
    eqButPID_stateSelectors[OF ss1] (* eqButPID_postSelectors[OF ss1]  *)
    eqButPID_actions[OF ss1]
    eqButPID_update[OF ss1] (* eqButPID_setTextPost[OF ss1] *) eqButPID_not_PID[OF ss1]
  (* added to cope with extra leak towards the admin, when moving from CoSMed to CosMeDis: *)
    (* eqButPID_eqButT[OF ss1] *) eqButPID_eqButF[OF ss1]
    eqButPID_setShared[OF ss1] eqButPID_updateShared[OF ss1]
    eeqButPID_F_not_PID eqButPID_not_PID_sharedWith
    eqButPID_insert2[OF ss1]
  show ?thesis
  proof (cases a)
    case (Sact x1)
    with willUse show ?thesis by (cases x1) auto
  next
    case (Cact x2)
    with willUse show ?thesis by (cases x2) auto
  next
    case (Dact x3)
    with willUse show ?thesis by (cases x3) auto
  next
    case (Uact x4)
    with willUse show ?thesis by (cases x4) auto
  next
    case (Ract x5)
    with willUse show ?thesis
    proof (cases x5)
      case (rPost uid p pid)
      with Ract willUse show ?thesis by (cases "pid = PID") auto
    qed auto
  next
    case (Lact x6)
    with willUse show ?thesis
    proof (cases x6)
      case (lClientsPost uid p pid)
      with Lact willUse show ?thesis by (cases "pid = PID") auto
    qed auto
  next
    case (COMact x7)
    with willUse show ?thesis by (cases x7) auto
  qed
qed

(* major *) lemma eqButPID_step_eq:
assumes ss1: "eqButPID s s1"
and a: "a = Uact (uPost uid p PID pst)" "ou = outOK"
and step: "step s a = (ou, s')" and step1: "step s1 a = (ou', s1')"
shows "s' = s1'"
using ss1 step step1
using eqButPID_stateSelectors[OF ss1]
eqButPID_update[OF ss1] (* eqButPID_setTextPost[OF ss1] *) eqButPID_setShared[OF ss1]
unfolding a by (auto simp: u_defs)


definition Δ0 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ0 s vl s1 vl1 ≡
 ¬ PID ∈∈ postIDs s ∧
 s = s1 ∧ BC vl vl1 ∧
 corr vl1"

definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡
 PID ∈∈ postIDs s ∧
 list_all (Not o isOVal) vl ∧ list_all (Not o isOVal) vl1 ∧
 map tgtAPI (filter isPValS vl) = map tgtAPI (filter isPValS vl1) ∧
 (vl = [] ⟶ vl1 = []) ∧
 eqButPID s s1 ∧ ¬ open s ∧
 corrFrom (post s1 PID) vl1"

definition Δ11 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ11 s vl s1 vl1 ≡
 PID ∈∈ postIDs s ∧
 vl = [] ∧ list_all isPVal vl1 ∧
 eqButPID s s1 ∧ ¬ open s ∧
 corrFrom (post s1 PID) vl1"

definition Δ2 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ2 s vl s1 vl1 ≡
 PID ∈∈ postIDs s ∧
 list_all (Not o isOVal) vl ∧
 vl = vl1 ∧
 s = s1 ∧ open s ∧
 corrFrom (post s1 PID) vl1"

definition Δ31 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ31 s vl s1 vl1 ≡
 PID ∈∈ postIDs s ∧
 (∃ ul ul1 sul vll vll1.
    BO vll vll1 ∧
    list_all (Not o isOVal) ul ∧ list_all (Not o isOVal) ul1 ∧
    map tgtAPI (filter isPValS ul) = map tgtAPI (filter isPValS ul1) ∧
    ul ≠ [] ∧ ul1 ≠ [] ∧
    isPVal (last ul) ∧ last ul = last ul1 ∧
    list_all isPValS sul ∧
    vl = ul @ sul @ OVal True # vll ∧ vl1 = ul1 @ sul @ OVal True # vll1) ∧
 eqButPID s s1 ∧ ¬ open s ∧
 corrFrom (post s1 PID) vl1"

definition Δ32 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ32 s vl s1 vl1 ≡
 PID ∈∈ postIDs s ∧
 (∃ sul vll vll1.
    BO vll vll1 ∧
    list_all isPValS sul ∧
    vl = sul @ OVal True # vll ∧ vl1 = sul @ OVal True # vll1) ∧
 s = s1 ∧ ¬ open s ∧
 corrFrom (post s1 PID) vl1"

definition Δ4 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ4 s vl s1 vl1 ≡
 PID ∈∈ postIDs s ∧
 (∃ ul vll vll1.
    BC vll vll1 ∧
    list_all (Not o isOVal) ul ∧
    vl = ul @ OVal False # vll ∧ vl1 = ul @ OVal False # vll1) ∧
 s = s1 ∧ open s ∧
 corrFrom (post s1 PID) vl1"

lemma istate_Δ0:
assumes B: "B vl vl1"
shows "Δ0 istate vl istate vl1"
using assms unfolding Δ0_def istate_def B_def by auto
(* by (auto simp: list_all_isOVal_filter_isPValS)
(auto intro!: exI[of _ "[]"]) *)

lemma list_all_filter[simp]:
assumes "list_all PP xs"
shows "filter PP xs = xs"
using assms by (induct xs) auto

lemma unwind_cont_Δ0: "unwind_cont Δ0 {Δ0,Δ1,Δ2,Δ31,Δ32,Δ4}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ0 s vl s1 vl1 ∨
                           Δ1 s vl s1 vl1 ∨ Δ2 s vl s1 vl1 ∨
                           Δ31 s vl s1 vl1 ∨ Δ32 s vl s1 vl1 ∨ Δ4 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ0 s vl s1 vl1"
  hence rs: "reach s" and ss1: "s1 = s" and BC: "BC vl vl1" and PID: "¬ PID ∈∈ postIDs s"
  and cor1: "corr vl1" using reachNT_reach unfolding Δ0_def by auto
  have vis: "vis s PID = FriendV" using reach_not_postIDs_friendV[OF rs PID] .
  have pPID: "post s1 PID = emptyPost" by (simp add: PID reach_not_postIDs_emptyPost rs ss1)
  have vlvl1: "vl = [] ⟹ vl1 = []" using BC_not_Nil BC by auto
  have op: "¬ open s" using PID unfolding open_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      hence pPID': "post s' PID = emptyPost"
        using step pPID ss1 PID
        apply(cases a)
        subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
        subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
        subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
        subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
        subgoal by (fastforce simp: d_defs)
        subgoal by (fastforce simp: d_defs)
        subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
        done
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have ?match
        proof(cases "∃ uid p. a = Cact (cPost uid p PID) ∧ ou = outOK")
          case True
          then obtain uid p where a: "a = Cact (cPost uid p PID)" and ou: "ou = outOK" by auto
          have PID': "PID ∈∈ postIDs s'"
          using step PID unfolding a ou by (auto simp: c_defs)
          show ?thesis proof(cases
             "∃ uid' ∈ UIDs. uid' ∈∈ userIDs s ∧
                             (uid' = admin s ∨ uid' = uid ∨ uid' ∈∈ friendIDs s uid)")
            case True note uid = True
            have op': "open s'" using uid using step PID' unfolding a ou by (auto simp: c_defs open_def)
            have φ: "φ ?trn" using op op' unfolding φ_def2[OF step] by simp
            then obtain v where vl: "vl = v # vl'" and f: "f ?trn = v"
            using c unfolding consume_def φ_def2 by(cases vl) auto
            have v: "v = OVal True" using f op op' unfolding a by simp
            then obtain ul1 vl1' where BO': "BO vl' vl1'" and vl1: "vl1 = ul1 @ OVal True # vl1'"
            and ul1: "list_all (Not ∘ isOVal) ul1"
            using BC_OVal_True[OF BC[unfolded vl v]] by auto
            have ul1: "ul1 = []"
              using BC BC_OVal_True list_all_Not_isOVal_OVal_True ul1 v vl vl1 by blast
            hence vl1: "vl1 = OVal True # vl1'" using vl1 by simp
            show ?thesis proof
              show "validTrans ?trn1" unfolding ss1 using step by simp
            next
              show "consume ?trn1 vl1 vl1'" using φ f unfolding vl1 v consume_def ss1 by simp
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
            next
              show "?Δ s' vl' s' vl1'" using BO' proof(cases rule: BO.cases)
                case (BO_PVal)
                hence "Δ2 s' vl' s' vl1'" using PID' op' cor1 unfolding Δ2_def vl1 pPID' by auto
                thus ?thesis by simp
              next
                case (BO_BC vll vll1 textl)
                hence "Δ4 s' vl' s' vl1'" using PID' op' cor1 unfolding Δ4_def vl1 pPID' by auto
                thus ?thesis by simp
              qed
            qed
          next
            case False note uid = False
            have op': "¬ open s'" using step op uid vis unfolding open_def a by (auto simp: c_defs)
            have φ: "¬ φ ?trn" using op op' a unfolding φ_def2[OF step] by auto
            hence vl': "vl' = vl" using c unfolding consume_def by simp
            show ?thesis proof
              show "validTrans ?trn1" unfolding ss1 using step by simp
            next
              show "consume ?trn1 vl1 vl1" using φ unfolding consume_def ss1 by auto
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
            next
              show "?Δ s' vl' s' vl1" using BC proof(cases rule: BC.cases)
                case (BC_PVal)
                hence "Δ1 s' vl' s' vl1" using PID' op' cor1 unfolding Δ1_def vl' pPID' by auto
                thus ?thesis by simp
              next
                case (BC_BO vll vll1 ul ul1 sul)
                show ?thesis
                proof(cases "ul ≠ [] ∧ ul1 ≠ []")
                  case True
                  hence "Δ31 s' vl' s' vl1" using BC_BO PID' op' cor1
                  unfolding Δ31_def vl' pPID' apply auto
                  apply (rule exI[of _ "ul"]) apply (rule exI[of _ "ul1"])
                  apply (rule exI[of _ "sul"])
                  apply (rule exI[of _ "vll"]) apply (rule exI[of _ "vll1"])
                  by auto
                  thus ?thesis by simp
                next
                  case False
                  hence 0: "ul = [] ∧ ul1 = []" using BC_BO by simp
                  hence 1: "list_all isPValS ul ∧ list_all isPValS ul1"
                  using ‹list_all (Not ∘ isOVal) ul› ‹list_all (Not ∘ isOVal) ul1›
                  using filter_list_all_isPValS_isOVal by auto
                  (* have "map tgtAPI ul = map tgtAPI ul1" using 1BC_BO by auto *)
                  have "Δ32 s' vl' s' vl1" using BC_BO PID' op' cor1 0 1
                  unfolding Δ32_def vl' pPID' apply simp
                  apply(rule exI[of _ "sul"])
                  apply(rule exI[of _ vll]) apply(rule exI[of _ vll1])
                  by auto
                  thus ?thesis by simp
                qed
              qed
            qed
          qed
        next
          case False note a = False
          have op': "¬ open s'"
            using a step PID op unfolding open_def
            apply(cases a)
            subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
            subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
            subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
            subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
            subgoal by (fastforce simp: u_defs)
            subgoal by (fastforce simp: u_defs)
            subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
            done
          have φ: "¬ φ ?trn" using PID step op op' unfolding φ_def2[OF step]
          by (auto simp: u_defs com_defs)
          hence vl': "vl' = vl" using c unfolding consume_def by simp
          have PID': "¬ PID ∈∈ postIDs s'"
            using step PID a
            apply(cases a)
            subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
            subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
            subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
            subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
            subgoal by (fastforce simp: u_defs)
            subgoal by (fastforce simp: u_defs)
            subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
            done
          show ?thesis proof
            show "validTrans ?trn1" unfolding ss1 using step by simp
          next
            show "consume ?trn1 vl1 vl1" using φ unfolding consume_def ss1 by auto
          next
            show "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
          next
            have "Δ0 s' vl' s' vl1" using a BC PID' cor1 unfolding Δ0_def vl' by simp
            thus "?Δ s' vl' s' vl1" by simp
          qed
        qed
        thus ?thesis by simp
      qed
    qed
  thus ?thesis using vlvl1 by simp
  qed
qed

lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1,Δ11}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨ Δ11 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ1 s vl s1 vl1"
  then obtain
  lvl: "list_all (Not ∘ isOVal) vl" and lvl1: "list_all (Not ∘ isOVal) vl1"
  and map: "map tgtAPI (filter isPValS vl) = map tgtAPI (filter isPValS vl1)"
  and rs: "reach s" and ss1: "eqButPID s s1" and op: "¬ open s" and PID: "PID ∈∈ postIDs s"
  and vlvl1: "vl = [] ⟹ vl1 = []" and cor1: "corrFrom (post s1 PID) vl1"
  using reachNT_reach unfolding Δ1_def by auto
  have PID1: "PID ∈∈ postIDs s1" using eqButPID_stateSelectors[OF ss1] PID by auto
  have own: "owner s PID ∈ set (userIDs s)" using reach_owner_userIDs[OF rs PID] .
  hence own1: "owner s1 PID ∈ set (userIDs s1)" using eqButPID_stateSelectors[OF ss1] by auto
  have adm: "admin s ∈ set (userIDs s)" using reach_admin_userIDs[OF rs own] .
  hence adm1: "admin s1 ∈ set (userIDs s1)" using eqButPID_stateSelectors[OF ss1] by auto
  have op1: "¬ open s1" using op ss1 eqButPID_open by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof(cases vl1)
    case (Cons v1 vll1) note vl1 = Cons
    show ?thesis proof(cases v1)
      case (PVal pst1) note v1 = PVal
      define uid where uid: "uid ≡ owner s PID"  define p where p: "p ≡ pass s uid"
      define a1 where a1: "a1 ≡ Uact (uPost uid p PID pst1)"
      have uid1: "uid = owner s1 PID" and p1: "p = pass s1 uid" unfolding uid p
      using eqButPID_stateSelectors[OF ss1] by auto
      obtain ou1 s1' where step1: "step s1 a1 = (ou1, s1')" by(cases "step s1 a1") auto
      have ou1: "ou1 = outOK" using step1 PID1 own1 unfolding a1 uid1 p1 by (auto simp: u_defs)
      have op1': "¬ open s1'" using step1 op1 unfolding a1 ou1 open_def by (auto simp: u_defs)
      have uid: "uid ∉ UIDs" unfolding uid using op PID own unfolding open_def by auto
      have pPID1': "post s1' PID = pst1" using step1 unfolding a1 ou1 by (auto simp: u_defs)
      let ?trn1 = "Trans s1 a1 ou1 s1'"
      have ?iact proof
        show "step s1 a1 = (ou1, s1')" using step1 .
      next
        show φ: "φ ?trn1" unfolding φ_def2[OF step1] a1 ou1 by simp
        show "consume ?trn1 vl1 vll1"
        using φ unfolding vl1 consume_def v1 a1 by auto
      next
        show "¬ γ ?trn1" using uid unfolding a1 by auto
      next
        have "eqButPID s1 s1'" using Uact_uPaperC_step_eqButPID[OF _ step1] a1 by auto
        hence ss1': "eqButPID s s1'" using eqButPID_trans ss1 by blast
        show "?Δ s vl s1' vll1" using PID op ss1' lvl lvl1 map vlvl1 cor1
        unfolding Δ1_def vl1 v1 pPID1' by auto
      qed
      thus ?thesis by simp
    next
      case (PValS aid1 pst1) note v1 = PValS
      have pPID1: "post s1 PID = pst1" using cor1 unfolding vl1 v1 by auto
      then obtain v vll where vl: "vl = v # vll"
      using map unfolding vl1 v1 by (cases vl) auto
      have ?react proof
        fix a :: act and ou :: out and s' :: state and vl'
        let ?trn = "Trans s a ou s'"
        assume step: "step s a = (ou, s')" and c: "consume ?trn vl vl'"
        have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
        obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
        let ?trn1 = "Trans s1 a ou1 s1'"
        show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'"
            (is "?match ∨ ?ignore")
        proof(cases "φ ?trn")
          case True note φ = True
          then obtain f: "f ?trn = v" and vl': "vl' = vll"
          using c unfolding vl consume_def φ_def2 by auto
          show ?thesis
          proof(cases v)
            case (PVal pst) note v = PVal
            have vll: "vll ≠ []" using map unfolding vl1 v1 vl v by auto
            define uid where uid: "uid ≡ owner s PID"  define p where p: "p ≡ pass s uid"
            have a: "a = Uact (uPost uid p PID pst)"
            using f_eq_PVal[OF step φ f[unfolded v]] unfolding uid p .
            have "eqButPID s s'" using Uact_uPaperC_step_eqButPID[OF a step] by auto
            hence s's1: "eqButPID s' s1" using eqButPID_sym eqButPID_trans ss1 by blast
            have op': "¬ open s'" using uPost_comSendPost_open_eq[OF step] a op by auto
            have ?ignore proof
              show γ: "¬ γ ?trn" using step_open_φ_f_PVal_γ[OF rs step PID op φ f[unfolded v]] .
              show "?Δ s' vl' s1 vl1"
              using lvl1 lvl PID' map s's1 op' vll cor1 unfolding Δ1_def vl1 vl vl' v
              by auto
            qed
            thus ?thesis by simp
          next
            case (PValS aid pst) note v = PValS
            define uid where uid: "uid ≡ admin s" define p where p: "p ≡ pass s uid"
            have a: "a = COMact (comSendPost (admin s) p aid PID)"
            using f_eq_PValS[OF step φ f[unfolded v]] unfolding uid p .
            have op': "¬ open s'" using uPost_comSendPost_open_eq[OF step] a op by auto
            have aid1: "aid1 = aid" using map unfolding vl1 v1 vl v by simp
            have uid1: "uid = admin s1" and p1: "p = pass s1 uid" unfolding uid p
            using eqButPID_stateSelectors[OF ss1] by auto
            obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
            have pPID1': "post s1' PID = pst1" using pPID1 step1 unfolding a
            by (auto simp: com_defs)
            have uid: "uid ∉ UIDs" unfolding uid using op PID adm unfolding open_def by auto
            have op1': "¬ open s1'" using step1 op1 unfolding a open_def
            by (auto simp: u_defs com_defs)
            let ?trn1 = "Trans s1 a ou1 s1'"
            have φ1: "φ ?trn1" using eqButPID_step_φ_imp[OF ss1 step step1 φ] .
            have ou1: "ou1 =
                O_sendPost (aid, clientPass s1 aid, PID, post s1 PID, owner s1 PID, vis s1 PID)"
              using φ1 step1 adm1 PID1 unfolding a by (cases ou1, auto simp: com_defs)
            have f1: "f ?trn1 = v1" using φ1 unfolding φ_def2[OF step1] v1 a ou1 aid1 pPID1 by auto
            have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
            have ?match proof
              show "validTrans ?trn1" using step1 by simp
            next
              show "consume ?trn1 vl1 vll1" using φ1 unfolding consume_def vl1 f1 by simp
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" note γ = this
              have ou: "(∃ uid p aid pid.
                       a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
                                        ou = ou1"
              using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
              thus "g ?trn = g ?trn1" by (cases a) auto
            next
              show "?Δ s' vl' s1' vll1"
              proof(cases "vll = []")
                case True note vll = True
                hence "filter isPValS vll1 = []" using map lvl lvl1 unfolding vl vl1 v v1 by simp
                hence lvl1: "list_all isPVal vll1"
                using filter_list_all_isPVal_isOVal lvl1 unfolding vl1 v1 by auto
                hence "Δ11 s' vl' s1' vll1" using s's1' op1' op' PID' lvl lvl1 map cor1 pPID1 pPID1'
                unfolding Δ11_def vl vl' vl1 v v1 vll by auto
                thus ?thesis by auto
              next
                case False note vll = False
                hence "Δ1 s' vl' s1' vll1" using s's1' op1' op' PID' lvl lvl1 map cor1 pPID1 pPID1'
                unfolding Δ1_def vl vl' vl1 v v1 by auto
                thus ?thesis by auto
              qed
            qed
          thus ?thesis using vl by simp
        qed(insert lvl vl, auto)
      next
        case False note φ = False
        hence vl': "vl' = vl" using c unfolding consume_def by auto
        obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
        have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
        let ?trn1 = "Trans s1 a ou1 s1'"
        have φ1: "¬ φ ?trn1" using φ ss1 by (simp add: eqButPID_step_φ step step1)
        have pPID1': "post s1' PID = pst1" using PID1 pPID1 step1 φ1 (* unfolding φ_def2[OF step1] *)
          apply(cases a)
          subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
          subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
          subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
          subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
          subgoal by (fastforce simp: u_defs)
          subgoal by (fastforce simp: u_defs)
          subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
          done
        have op': "¬ open s'"
        using PID step φ op unfolding φ_def2[OF step] by auto
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" using φ1 unfolding consume_def by simp
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" note γ = this
          have ou: "(∃ uid p aid pid.
                   a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
                   ou = ou1"
          using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
          thus "g ?trn = g ?trn1" by (cases a) auto
        next
          have "Δ1 s' vl' s1' vl1" using s's1' PID' pPID1 pPID1' lvl lvl1 map cor1 op'
          unfolding Δ1_def vl vl' by auto
          thus "?Δ s' vl' s1' vl1" by simp
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vlvl1 by simp
  qed(insert lvl1 vl1, auto)
next
  case Nil note vl1 = Nil
  have ?react proof
    fix a :: act and ou :: out and s' :: state and vl'
    let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
      obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
      let ?trn1 = "Trans s1 a ou1 s1'"
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof(cases "∃ uid p pstt. a = Uact (uPost uid p PID pstt) ∧ ou = outOK")
        case True then obtain uid p pstt where
        a: "a = Uact (uPost uid p PID pstt)" and ou: "ou = outOK" by auto
        hence φ: "φ ?trn" unfolding φ_def2[OF step] by auto
        then obtain v where vl: "vl = v # vl'" and f: "f ?trn = v"
        using c unfolding consume_def φ_def2 by (cases vl) auto
        obtain pst where v: "v = PVal pst" using map lvl unfolding vl vl1 by (cases v) auto
        have pstt: "pstt = pst" using f unfolding a v by auto
        have uid: "uid ∉ UIDs" using step op PID unfolding a ou open_def by (auto simp: u_defs)
        have "eqButPID s s'" using Uact_uPaperC_step_eqButPID[OF a step] by auto
        hence s's1: "eqButPID s' s1" using eqButPID_sym eqButPID_trans ss1 by blast
        have op': "¬ open s'" using step PID' op unfolding a ou open_def by (auto simp: u_defs)
        have ?ignore proof
          show "¬ γ ?trn" unfolding a using uid by auto
        next
          show "?Δ s' vl' s1 vl1" using PID' s's1 op' lvl map
          unfolding Δ1_def vl1 vl by auto
        qed
        thus ?thesis by simp
      next
        case False note a = False
        {assume φ: "φ ?trn"
         then obtain v vl' where vl: "vl = v # vl'" and f: "f ?trn = v"
         using c unfolding consume_def by (cases vl) auto
         obtain pst where v: "v = PVal pst" using map lvl unfolding vl vl1 by (cases v) auto
         have False using f f_eq_PVal[OF step φ, of pst] a φ v by auto
        }
        hence φ: "¬ φ ?trn" by auto
        have φ1: "¬ φ ?trn1" by (metis φ eqButPID_step_φ step ss1 step1)
        have op': "¬ open s'" using a op φ unfolding φ_def2[OF step] by auto
        have vl': "vl' = vl" using c φ unfolding consume_def by auto
        have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
        have op1': "¬ open s1'" using op' eqButPID_open[OF s's1'] by simp
        have "⋀ uid p pst. e_updatePost s1 uid p PID pst ⟷ e_updatePost s uid p PID pst"
        using eqButPID_stateSelectors[OF ss1] unfolding u_defs by auto
        hence ou1: "⋀ uid p pst. a = Uact (uPost uid p PID pst) ⟹ ou1 = ou"
        using step step1 by auto
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" using φ1 unfolding consume_def by simp
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" note γ = this
          have ou: "(∃ uid p aid pid.
                       a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
                                        ou = ou1"
          using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
          thus "g ?trn = g ?trn1" by (cases a) auto
        next
          show "?Δ s' vl' s1' vl1" using s's1' op' PID' lvl map
          unfolding Δ1_def vl' vl1 by auto
        qed
      thus ?thesis by simp
      qed
    qed
    thus ?thesis using vlvl1 by simp
  qed
qed

lemma unwind_cont_Δ11: "unwind_cont Δ11 {Δ11}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ11 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ11 s vl s1 vl1"
  hence  vl: "vl = []" and lvl1: "list_all isPVal vl1"
  and rs: "reach s" and ss1: "eqButPID s s1" and op: "¬ open s" and PID: "PID ∈∈ postIDs s"
  and cor1: "corrFrom (post s1 PID) vl1"
  using reachNT_reach unfolding Δ11_def by auto
  have PID1: "PID ∈∈ postIDs s1" using eqButPID_stateSelectors[OF ss1] PID by auto
  have own: "owner s PID ∈ set (userIDs s)" using reach_owner_userIDs[OF rs PID] .
  hence own1: "owner s1 PID ∈ set (userIDs s1)" using eqButPID_stateSelectors[OF ss1] by auto
  have adm: "admin s ∈ set (userIDs s)" using reach_admin_userIDs[OF rs own] .
  hence adm1: "admin s1 ∈ set (userIDs s1)" using eqButPID_stateSelectors[OF ss1] by auto
  have op1: "¬ open s1" using op ss1 eqButPID_open by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof(cases vl1)
    case (Cons v1 vll1) note vl1 = Cons
    then obtain pst1 where v1: "v1 = PVal pst1" using lvl1 unfolding vl1 by (cases v1) auto
    define uid where uid: "uid ≡ owner s PID"  define p where p: "p ≡ pass s uid"
    define a1 where a1: "a1 ≡ Uact (uPost uid p PID pst1)"
    have uid1: "uid = owner s1 PID" and p1: "p = pass s1 uid" unfolding uid p
    using eqButPID_stateSelectors[OF ss1] by auto
    obtain ou1 s1' where step1: "step s1 a1 = (ou1, s1')" by(cases "step s1 a1") auto
    have ou1: "ou1 = outOK" using step1 PID1 own1 unfolding a1 uid1 p1 by (auto simp: u_defs)
    have op1': "¬ open s1'" using step1 op1 unfolding a1 ou1 open_def by (auto simp: u_defs)
    have uid: "uid ∉ UIDs" unfolding uid using op PID own unfolding open_def by auto
    have pPID1': "post s1' PID = pst1" using step1 unfolding a1 ou1 by (auto simp: u_defs)
    let ?trn1 = "Trans s1 a1 ou1 s1'"
    have ?iact proof
      show "step s1 a1 = (ou1, s1')" using step1 .
    next
      show φ: "φ ?trn1" unfolding φ_def2[OF step1] a1 ou1 by simp
      show "consume ?trn1 vl1 vll1"
      using φ unfolding vl1 consume_def v1 a1 by auto
    next
      show "¬ γ ?trn1" using uid unfolding a1 by auto
    next
      have "eqButPID s1 s1'" using Uact_uPaperC_step_eqButPID[OF _ step1] a1 by auto
      hence ss1': "eqButPID s s1'" using eqButPID_trans ss1 by blast
      show "?Δ s vl s1' vll1"
      using PID op ss1' lvl1 cor1 unfolding Δ11_def vl1 v1 vl pPID1' by auto
    qed
    thus ?thesis by simp
  next
    case Nil note vl1 = Nil
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
      obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
      let ?trn1 = "Trans s1 a ou1 s1'"
      have φ: "¬ φ ?trn" using c unfolding consume_def vl by auto
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'"
          (is "?match ∨ ?ignore")
      proof-
        have vl': "vl' = vl" using c unfolding vl consume_def by auto
        obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
        have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
        let ?trn1 = "Trans s1 a ou1 s1'"
        have φ1: "¬ φ ?trn1" using φ ss1 by (simp add: eqButPID_step_φ step step1)
        have pPID1': "post s1' PID = post s1 PID" using PID1 step1 φ1
          apply(cases a)
          subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
          subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
          subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
          subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
          subgoal by fastforce
          subgoal by fastforce
          subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
          done
        have op': "¬ open s'" using PID step φ op unfolding φ_def2[OF step] by auto
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" using φ1 unfolding consume_def by simp
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" note γ = this
          have ou: "(∃ uid p aid pid.
                   a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
                   ou = ou1"
          using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
          thus "g ?trn = g ?trn1" by (cases a) auto
        next
          have "?Δ s' vl' s1' vl1" using s's1' PID' pPID1' lvl1 cor1 op'
          unfolding Δ11_def vl vl' by auto
          thus "?Δ s' vl' s1' vl1" by simp
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl1 by simp
  qed
qed

lemma unwind_cont_Δ31: "unwind_cont Δ31 {Δ31,Δ32}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ31 s vl s1 vl1 ∨ Δ32 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ31 s vl s1 vl1"
  then obtain ul ul1 sul vll vll1 where
  lul: "list_all (Not ∘ isOVal) ul" and lul1: "list_all (Not ∘ isOVal) ul1"
  and map: "map tgtAPI (filter isPValS ul) = map tgtAPI (filter isPValS ul1)"
  and rs: "reach s" and ss1: "eqButPID s s1" and op: "¬ open s" and PID: "PID ∈∈ postIDs s"
  and cor1: "corrFrom (post s1 PID) vl1"
  and ful: "ul ≠ []" and ful1: "ul1 ≠ []"
  and lastul: "isPVal (last ul)" and ulul1: "last ul = last ul1"
  and lsul: "list_all isPValS sul"
  and vl: "vl = ul @ sul @ OVal True # vll"
  and vl1: "vl1 = ul1 @ sul @ OVal True # vll1"
  and BO: "BO vll vll1"
  using reachNT_reach unfolding Δ31_def by auto
  have ulNE: "ul ≠ []" and ul1NE: "ul1 ≠ []" using ful ful1 by auto
  have PID1: "PID ∈∈ postIDs s1" using eqButPID_stateSelectors[OF ss1] PID by auto
  have own: "owner s PID ∈ set (userIDs s)" using reach_owner_userIDs[OF rs PID] .
  hence own1: "owner s1 PID ∈ set (userIDs s1)" using eqButPID_stateSelectors[OF ss1] by auto
  have adm: "admin s ∈ set (userIDs s)" using reach_admin_userIDs[OF rs own] .
  hence adm1: "admin s1 ∈ set (userIDs s1)" using eqButPID_stateSelectors[OF ss1] by auto
  have op1: "¬ open s1" using op ss1 eqButPID_open by auto
  obtain v1 ull1 where ul1: "ul1 = v1 # ull1" using ful1 by (cases ul1) auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof(cases v1)
    case (PVal pst1) note v1 = PVal
    show ?thesis proof(cases "list_ex isPVal ull1")
      case True note lull1 = True
      hence full1: "filter isPVal ull1 ≠ []" by (induct ull1) auto
      hence ull1NE: "ull1 ≠ []" by auto
      define uid where uid: "uid ≡ owner s PID"  define p where p: "p ≡ pass s uid"
      define a1 where a1: "a1 ≡ Uact (uPost uid p PID pst1)"
      have uid1: "uid = owner s1 PID" and p1: "p = pass s1 uid" unfolding uid p
      using eqButPID_stateSelectors[OF ss1] by auto
      obtain ou1 s1' where step1: "step s1 a1 = (ou1, s1')" by(cases "step s1 a1") auto
      have ou1: "ou1 = outOK" using step1 PID1 own1 unfolding a1 uid1 p1 by (auto simp: u_defs)
      have op1': "¬ open s1'" using step1 op1 unfolding a1 ou1 open_def by (auto simp: u_defs)
      have uid: "uid ∉ UIDs" unfolding uid using op PID own unfolding open_def by auto
      have pPID1': "post s1' PID = pst1" using step1 unfolding a1 ou1 by (auto simp: u_defs)
      let ?trn1 = "Trans s1 a1 ou1 s1'"
      let ?vl1' = "ull1 @ sul @ OVal True # vll1"
      have ?iact proof
        show "step s1 a1 = (ou1, s1')" using step1 .
      next
        show φ: "φ ?trn1" unfolding φ_def2[OF step1] a1 ou1 by simp
        show "consume ?trn1 vl1 ?vl1'"
        using φ unfolding vl1 ul1 consume_def v1 a1 by simp
      next
        show "¬ γ ?trn1" using uid unfolding a1 by auto
      next
        have "eqButPID s1 s1'" using Uact_uPaperC_step_eqButPID[OF _ step1] a1 by auto
        hence ss1': "eqButPID s s1'" using eqButPID_trans ss1 by blast
        have "Δ31 s vl s1' ?vl1'"
        using PID op ss1' lul lul1 map ulul1 cor1 BO ull1NE ful ful1 full1 lastul ulul1 lsul
        unfolding Δ31_def vl vl1 ul1 v1 pPID1' apply auto
        apply(rule exI[of _ "ul"]) apply(rule exI[of _ "ull1"]) apply(rule exI[of _ sul])
        apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
        thus "?Δ s vl s1' ?vl1'" by auto
      qed
      thus ?thesis by simp
    next
      case False note lull1 = False
      hence ull1: "ull1 = []" using lastul unfolding ulul1 ul1 v1 by simp(meson Bex_set last_in_set)
      hence ul1: "ul1 = [PVal pst1]" unfolding ul1 v1 by simp
      obtain ulll where ul_ulll: "ul = ulll ## PVal pst1" using lastul ulul1 ulNE unfolding ul1 ull1 v1
      by (cases ul rule: rev_cases) auto
      hence ulNE: "ul ≠ []" by simp
      (* then obtain v ul' where ul: "ul = v # ul'" by (cases ul) auto *)
      have "filter isPValS ulll = []" using map unfolding ul_ulll ul1 v1 ull1 by simp
      hence lull: "list_all isPVal ulll" using lul filter_list_all_isPVal_isOVal
      unfolding ul_ulll by auto
      have ?react  proof
        fix a :: act and ou :: out and s' :: state and vl'
        let ?trn = "Trans s a ou s'"
        assume step: "step s a = (ou, s')" and c: "consume ?trn vl vl'"
        have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
        obtain ul' where cc: "consume ?trn ul ul'" and
        vl': "vl' = ul' @ sul @ OVal True # vll" using c ulNE unfolding consume_def vl
        by (cases "φ ?trn") auto
        obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
        let ?trn1 = "Trans s1 a ou1 s1'"
        show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'"
             (is "?match ∨ ?ignore")
        proof(cases ulll)
          case Nil
          hence ul: "ul = [PVal pst1]" unfolding ul_ulll by simp
          have ?match proof(cases "φ ?trn")
            case True note φ = True
            then obtain f: "f ?trn = PVal pst1" and ul': "ul' = []"
            using cc unfolding ul consume_def φ_def2 by auto
            define uid where uid: "uid ≡ owner s PID"  define p where p: "p ≡ pass s uid"
            have a: "a = Uact (uPost uid p PID pst1)"
            using f_eq_PVal[OF step φ f] unfolding uid p .
            have uid1: "uid = owner s1 PID" and p1: "p = pass s1 uid" unfolding uid p
            using eqButPID_stateSelectors[OF ss1] by auto
            obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
            let ?trn1 = "Trans s1 a ou1 s1'"
            have φ1: "φ ?trn1" using eqButPID_step_φ_imp[OF ss1 step step1 φ] .
            have ou1: "ou1 = outOK"
            using φ1 step1 PID1 unfolding a by (cases ou1, auto simp: com_defs)
            have pPID': "post s' PID = pst1" using step φ unfolding a by (auto simp: u_defs)
            have pPID1': "post s1' PID = pst1" using step1 φ1 unfolding a by (auto simp: u_defs)
            have uid: "uid ∉ UIDs" unfolding uid using op PID own unfolding open_def by auto
            have op1': "¬ open s1'" using step1 op1 unfolding a open_def
            by (auto simp: u_defs com_defs)
            have f1: "f ?trn1 = PVal pst1" using φ1 unfolding φ_def2[OF step1] v1 a ou1 by auto
            have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
            have op': "¬ open s'" using uPost_comSendPost_open_eq[OF step] a op by auto
            have ou: "ou = outOK" using φ op op' unfolding φ_def2[OF step] a by auto
            let ?vl' = "sul @ OVal True # vll"
            let ?vl1' = "sul @ OVal True # vll1"
            show ?thesis proof
              show "validTrans ?trn1" using step1 by simp
            next
              show "consume ?trn1 vl1 ?vl1'"
              using φ1 unfolding consume_def ul1 f1 vl1 by simp
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" note γ = this
              thus "g ?trn = g ?trn1" using ou ou1 by (cases a) auto
            next
              have s': "s' = s1'" using eqButPID_step_eq[OF ss1 a ou step step1] .
              have corr1: "corrFrom (post s1' PID) ?vl1'"
              using cor1 unfolding vl1 ul1 v1 pPID1' by auto
              have "Δ32 s' vl' s1' ?vl1'"
              using PID' op1 op' s's1' lul lul1 map ulul1 cor1 BO ful ful1 lastul ulul1 lsul corr1
              unfolding Δ32_def vl vl1 v1 vl' ul' ul ul1 s' apply simp
              apply(rule exI[of _ sul])
              apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
              thus "?Δ s' vl' s1' ?vl1'" by simp
            qed
          next
            case False note φ = False
            hence ul': "ul' = ul" using cc unfolding consume_def by auto
            obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
            have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
            let ?trn1 = "Trans s1 a ou1 s1'"
            have φ1: "¬ φ ?trn1" using φ ss1 by (simp add: eqButPID_step_φ step step1)
            have pPID1': "post s1' PID = post s1 PID" using PID1 step1 φ1
              apply(cases a)
              subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
              subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
              subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
              subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
              subgoal by fastforce
              subgoal by fastforce
              subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
              done
            have op': "¬ open s'" using PID step φ op unfolding φ_def2[OF step] by auto
            have ?match proof
              show "validTrans ?trn1" using step1 by simp
            next
              show "consume ?trn1 vl1 vl1" using φ1 unfolding consume_def by simp
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" note γ = this
              have ou: "(∃ uid p aid pid.
                 a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
                 ou = ou1"
              using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
              thus "g ?trn = g ?trn1" by (cases a) auto
            next
              have "Δ31 s' vl' s1' vl1"
              using PID' pPID1' op' s's1' lul lul1 map ulul1 cor1
              BO ful ful1 lastul ulul1 lsul cor1
              unfolding Δ31_def vl vl1 v1 vl' ul' apply simp
              apply(rule exI[of _ "ul"]) apply(rule exI[of _ "ul1"]) apply(rule exI[of _ sul])
              apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
              thus "?Δ s' vl' s1' vl1" by simp
            qed
            thus ?thesis by simp
          qed
          thus ?thesis by simp
        next
          case (Cons v ullll) note ulll = Cons
          then obtain pst where v: "v = PVal pst" using lull ul_ulll ulll lul by (cases v) auto
          define ull where ull: "ull ≡ ullll ## PVal pst1"
          have ul: "ul = v # ull" unfolding ul_ulll ull ulll by simp
          show ?thesis proof(cases "φ ?trn")
            case True note φ = True
            then obtain f: "f ?trn = v" and ul': "ul' = ull"
            using cc unfolding ul consume_def φ_def2 by auto
            define uid where uid: "uid ≡ owner s PID"  define p where p: "p ≡ pass s uid"
            have a: "a = Uact (uPost uid p PID pst)"
            using f_eq_PVal[OF step φ f[unfolded v]] unfolding uid p .
            have "eqButPID s s'" using Uact_uPaperC_step_eqButPID[OF a step] by auto
            hence s's1: "eqButPID s' s1" using eqButPID_sym eqButPID_trans ss1 by blast
            have op': "¬ open s'" using uPost_comSendPost_open_eq[OF step] a op by auto
            have ?ignore proof
              show γ: "¬ γ ?trn" using step_open_φ_f_PVal_γ[OF rs step PID op φ f[unfolded v]] .
              have "Δ31 s' vl' s1 vl1"
              using PID' op' s's1 lul lul1 map ulul1 cor1 BO ful ful1 lastul ulul1 lsul ull
              unfolding Δ31_def vl vl1 v1 vl' ul' ul v apply simp
              apply(rule exI[of _ "ull"]) apply(rule exI[of _ "ul1"]) apply(rule exI[of _ sul])
              apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
              thus "?Δ s' vl' s1 vl1" by auto
            qed
            thus ?thesis by simp
          next
            case False note φ = False
            hence ul': "ul' = ul" using cc unfolding consume_def by auto
            obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
            have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
            let ?trn1 = "Trans s1 a ou1 s1'"
            have φ1: "¬ φ ?trn1" using φ ss1 by (simp add: eqButPID_step_φ step step1)
            have pPID1': "post s1' PID = post s1 PID" using PID1 step1 φ1
              apply(cases a)
              subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
              subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
              subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
              subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
              subgoal by fastforce
              subgoal by fastforce
              subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
              done
            have op': "¬ open s'" using PID step φ op unfolding φ_def2[OF step] by auto
            have ?match proof
              show "validTrans ?trn1" using step1 by simp
            next
              show "consume ?trn1 vl1 vl1" using φ1 unfolding consume_def by simp
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" note γ = this
              have ou: "(∃ uid p aid pid.
                 a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
                 ou = ou1"
              using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
              thus "g ?trn = g ?trn1" by (cases a) auto
            next
              have "Δ31 s' vl' s1' vl1"
              using PID' pPID1' op' s's1' lul lul1 map ulul1 cor1
              BO ful ful1 lastul ulul1 lsul cor1
              unfolding Δ31_def vl vl1 v1 vl' ul' apply simp
              apply(rule exI[of _ "ul"]) apply(rule exI[of _ "ul1"]) apply(rule exI[of _ sul])
              apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
              thus "?Δ s' vl' s1' vl1" by simp
            qed
          thus ?thesis by simp
          qed
        qed
      qed
      thus ?thesis using vl by simp
    qed
  next
    case (PValS aid1 pst1) note v1 = PValS
    have pPID1: "post s1 PID = pst1" using cor1 unfolding vl1 ul1 v1 by auto
    then obtain v ull where ul: "ul = v # ull"
    using map unfolding ul1 v1 by (cases ul) auto
    let ?vl1' = "ull1 @ sul @ OVal True # vll1"
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
      obtain ul' where cc: "consume ?trn ul ul'" and
      vl': "vl' = ul' @ sul @ OVal True # vll" using c ul unfolding consume_def vl
      by (cases "φ ?trn") auto
      obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
      let ?trn1 = "Trans s1 a ou1 s1'"
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'"
          (is "?match ∨ ?ignore")
      proof(cases "φ ?trn")
        case True note φ = True
        then obtain f: "f ?trn = v" and ul': "ul' = ull"
        using cc unfolding ul consume_def φ_def2 by auto
        show ?thesis
        proof(cases v)
          case (PVal pst) note v = PVal
          have full: "ull ≠ []" using map unfolding ul1 v1 ul v by auto
          define uid where uid: "uid ≡ owner s PID"  define p where p: "p ≡ pass s uid"
          have a: "a = Uact (uPost uid p PID pst)"
          using f_eq_PVal[OF step φ f[unfolded v]] unfolding uid p .
          have "eqButPID s s'" using Uact_uPaperC_step_eqButPID[OF a step] by auto
          hence s's1: "eqButPID s' s1" using eqButPID_sym eqButPID_trans ss1 by blast
          have op': "¬ open s'" using uPost_comSendPost_open_eq[OF step] a op by auto
          (* have "list_ex isPVal ull1" using lastul not_list_ex_filter
          using ful1 not_list_ex_filter ul1 v1 unfolding ulul1 by auto
          hence lull: "list_ex isPVal ull" using lastul ulul1 ull unfolding ul ul1 v v1
          by (metis filter_empty_conv last_ConsR last_in_set not_list_ex_filter)
          hence full: "filter isPVal ull ≠ []" by (induct ull) auto *)
          have ?ignore proof
            show γ: "¬ γ ?trn" using step_open_φ_f_PVal_γ[OF rs step PID op φ f[unfolded v]] .
            have "Δ31 s' vl' s1 vl1"
            using PID' op' s's1 lul lul1 map ulul1 cor1 BO ful ful1 lastul ulul1 lsul full
            unfolding Δ31_def vl vl1 v1 vl' ul' ul v apply simp
            apply(rule exI[of _ "ull"]) apply(rule exI[of _ "ul1"]) apply(rule exI[of _ sul])
            apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
            thus "?Δ s' vl' s1 vl1" by auto
          qed
          thus ?thesis by simp
        next
          case (PValS aid pst) note v = PValS
          define uid where uid: "uid ≡ admin s" define p where p: "p ≡ pass s uid"
          have a: "a = COMact (comSendPost (admin s) p aid PID)"
          using f_eq_PValS[OF step φ f[unfolded v]] unfolding uid p .
          have op': "¬ open s'" using uPost_comSendPost_open_eq[OF step] a op by auto
          have aid1: "aid1 = aid" using map unfolding ul1 v1 ul v by simp
          have uid1: "uid = admin s1" and p1: "p = pass s1 uid" unfolding uid p
          using eqButPID_stateSelectors[OF ss1] by auto
          obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
          have pPID1': "post s1' PID = pst1" using pPID1 step1 unfolding a
          by (auto simp: com_defs)
          have uid: "uid ∉ UIDs" unfolding uid using op PID adm unfolding open_def by auto
          have op1': "¬ open s1'" using step1 op1 unfolding a open_def
          by (auto simp: u_defs com_defs)
          let ?trn1 = "Trans s1 a ou1 s1'"
          have φ1: "φ ?trn1" using eqButPID_step_φ_imp[OF ss1 step step1 φ] .
          have ou1: "ou1 =
            O_sendPost (aid, clientPass s1 aid, PID, post s1 PID, owner s1 PID, vis s1 PID)"
          using φ1 step1 adm1 PID1 unfolding a by (cases ou1, auto simp: com_defs)
          have f1: "f ?trn1 = v1" using φ1 unfolding φ_def2[OF step1] v1 a ou1 aid1 pPID1 by auto
          have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
          have ?match proof
            show "validTrans ?trn1" using step1 by simp
          next
            show "consume ?trn1 vl1 ?vl1'" using φ1 unfolding consume_def ul1 f1 vl1 by simp
          next
            show "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" note γ = this
            have ou: "(∃ uid p aid pid.
               a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
               ou = ou1"
            using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
            thus "g ?trn = g ?trn1" by (cases a) auto
          next
            have corr1: "corrFrom (post s1' PID) ?vl1'"
            using cor1 unfolding vl1 ul1 v1 pPID1' by auto
            have ullull1: "ull1 ≠ [] ⟶ ull ≠ []" using ul ul1 lastul ulul1 unfolding v v1
            by fastforce
            have "Δ31 s' vl' s1' ?vl1'"
            using PID' op' s's1' lul lul1 map ulul1 cor1 BO ful ful1 lastul ulul1 lsul corr1 ullull1
            unfolding Δ31_def vl vl1 v1 vl' ul' ul ul1 v apply auto
            apply(rule exI[of _ "ull"]) apply(rule exI[of _ "ull1"]) apply(rule exI[of _ sul])
            apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
            thus "?Δ s' vl' s1' ?vl1'" by simp
          qed
          thus ?thesis using ul by simp
        next
        qed(insert lul ul, auto)
      next
        case False note φ = False
        hence ul': "ul' = ul" using cc unfolding consume_def by auto
        obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by(cases "step s1 a") auto
        have s's1': "eqButPID s' s1'" using eqButPID_step[OF ss1 step step1] .
        let ?trn1 = "Trans s1 a ou1 s1'"
        have φ1: "¬ φ ?trn1" using φ ss1 by (simp add: eqButPID_step_φ step step1)
        have pPID1': "post s1' PID = pst1" using PID1 pPID1 step1 φ1
          apply(cases a)
          subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
          subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
          subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
          subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
          subgoal by fastforce
          subgoal by fastforce
          subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
          done
        have op': "¬ open s'" using PID step φ op unfolding φ_def2[OF step] by auto
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" using φ1 unfolding consume_def by simp
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" note γ = this
          have ou: "(∃ uid p aid pid.
                 a = COMact (comSendPost uid p aid pid) ∧ outPurge ou = outPurge ou1) ∨
                 ou = ou1"
          using eqButPID_step_γ_out[OF ss1 step step1 op rsT rs1 γ] .
          thus "g ?trn = g ?trn1" by (cases a) auto
        next
          have "Δ31 s' vl' s1' vl1"
          using PID' pPID1 pPID1' op' s's1' lul lul1 map ulul1 cor1
            BO ful ful1 lastul ulul1 lsul cor1
          unfolding Δ31_def vl vl1 v1 vl' ul' apply simp
          apply(rule exI[of _ "ul"]) apply(rule exI[of _ "ul1"]) apply(rule exI[of _ sul])
          apply(rule exI[of _ "vll"]) apply(rule exI[of _ "vll1"]) by auto
          thus "?Δ s' vl' s1' vl1" by simp
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl by simp
  qed(insert lul1 ul1, auto)
qed

lemma unwind_cont_Δ32: "unwind_cont Δ32 {Δ2,Δ32,Δ4}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ2 s vl s1 vl1 ∨ Δ32 s vl s1 vl1 ∨ Δ4 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ32 s vl s1 vl1"
  then obtain ul vll vll1 where
  lul: "list_all isPValS ul"
  and rs: "reach s" and ss1: "s1 = s" and op: "¬ open s" and PID: "PID ∈∈ postIDs s"
  and cor1: "corrFrom (post s1 PID) vl1"
  and vl: "vl = ul @ OVal True # vll"
  and vl1: "vl1 = ul @ OVal True # vll1"
  and BO: "BO vll vll1"
  using reachNT_reach unfolding Δ32_def by blast
  have own: "owner s PID ∈ set (userIDs s)" using reach_owner_userIDs[OF rs PID] .
  have adm: "admin s ∈ set (userIDs s)" using reach_admin_userIDs[OF rs own] .
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'" let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'"
          (is "?match ∨ ?ignore")
      proof-
        have ?match proof(cases "ul = []")
          case False note ul = False
          then obtain ul' where cc: "consume ?trn ul ul'"
          and vl': "vl' = ul' @ OVal True # vll" using vl c unfolding consume_def
          by (cases "φ ?trn") auto
          let ?vl1' = "ul' @ OVal True # vll1"
          show ?thesis proof
            show "validTrans ?trn1" using step unfolding ss1 by simp
          next
            show "consume ?trn1 vl1 ?vl1'" using cc ul unfolding vl1 consume_def ss1
            by (cases "φ ?trn") auto
          next
            show "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" note γ = this
            thus "g ?trn = g ?trn1" unfolding ss1 by simp
          next
            have "Δ32 s' vl' s' ?vl1'"
            proof(cases "φ ?trn")
              case True note φ = True
              then obtain v where f: "f ?trn = v" and  ul: "ul = v # ul'"
              using cc unfolding consume_def by (cases ul) auto
              define uid where uid: "uid ≡ admin s" define p where p: "p ≡ pass s uid"
              obtain aid pst where v: "v = PValS aid pst" using lul unfolding ul by (cases v) auto
              have a: "a = COMact (comSendPost (admin s) p aid PID)"
              using f_eq_PValS[OF step φ f[unfolded v]] unfolding uid p .
              have op': "¬ open s'" using uPost_comSendPost_open_eq[OF step] a op by auto
              have pPID': "post s' PID = post s PID"
              using step unfolding a by (auto simp: com_defs)
              show ?thesis using PID' pPID' op' cor1 BO lul
              unfolding Δ32_def vl1 ul ss1 v vl' by auto
            next
              case False note φ = False
              hence ul: "ul = ul'" using cc unfolding consume_def by (cases ul) auto
              have pPID': "post s' PID = post s PID"
                using step φ PID op
                apply(cases a)
                subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
                subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
                subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
                subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
                subgoal by fastforce
                subgoal by fastforce
                subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
                done
              have op': "¬ open s'" using PID step φ op unfolding φ_def2[OF step] by auto
              show ?thesis using PID' pPID' op' cor1 BO lul
              unfolding Δ32_def vl1 ul ss1 vl' by auto
            qed
            thus "?Δ s' vl' s' ?vl1'" by simp
          qed
        next
          case True note ul = True
          show ?thesis proof(cases "φ ?trn")
            case True note φ = True
            hence f: "f ?trn = OVal True" and vl': "vl' = vll"
            using vl c unfolding consume_def ul by auto
            have op': "open s'" using f_eq_OVal[OF step φ f] op by simp
            show ?thesis proof
              show "validTrans ?trn1" using step unfolding ss1 by simp
            next
              show "consume ?trn1 vl1 vll1" using ul φ c
              unfolding vl1 vl' vl ss1 consume_def by auto
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" note γ = this
              thus "g ?trn = g ?trn1" unfolding ss1 by simp
            next
              have pPID': "post s' PID = post s PID"
                using step φ PID op op' f
                apply(cases a)
                subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
                subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
                subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
                subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
                subgoal by fastforce
                subgoal by fastforce
                subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
                done
              show "?Δ s' vl' s' vll1" using BO proof cases
                case BO_PVal
                hence "Δ2 s' vl' s' vll1" using PID' pPID' op' cor1 BO lul
                unfolding Δ2_def vl1 ul ss1 vl' by auto
                thus ?thesis by simp
              next
                case BO_BC
                hence "Δ4 s' vl' s' vll1" using PID' pPID' op' cor1 BO lul
                unfolding Δ4_def vl1 ul ss1 vl' by auto
                thus ?thesis by simp
              qed
            qed
          next
            case False note φ = False
            hence vl': "vl' = vl" using c unfolding consume_def by auto
            have pPID': "post s' PID = post s PID"
              using step φ PID op
              apply(cases a)
              subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
              subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
              subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
              subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
              subgoal by fastforce
              subgoal by fastforce
              subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
              done
            have op': "¬ open s'" using PID step φ op unfolding φ_def2[OF step] by auto
            show ?thesis proof
              show "validTrans ?trn1" using step unfolding ss1 by simp
            next
              show "consume ?trn1 vl1 vl1" using ul φ unfolding vl1 consume_def ss1 by simp
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" note γ = this
              thus "g ?trn = g ?trn1" unfolding ss1 by simp
            next
              have "Δ32 s' vl' s' vl1" using PID' pPID' op' cor1 BO lul
              unfolding Δ32_def vl vl1 ul ss1 vl' apply simp
              apply(rule exI[of _ "[]"])
              apply(rule exI[of _ vll]) apply(rule exI[of _ vll1]) by auto
              thus "?Δ s' vl' s' vl1" by simp
            qed
          qed
        qed
        thus ?thesis by simp
      qed
    qed
  thus ?thesis using vl by simp
  qed
qed

lemma unwind_cont_Δ2: "unwind_cont Δ2 {Δ2}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ2 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ2 s vl s1 vl1"
  hence vlvl1: "vl = vl1"
  and rs: "reach s" and ss1: "s1 = s" and op: "open s" and PID: "PID ∈∈ postIDs s"
  and cor1: "corrFrom (post s1 PID) vl1" and lvl: "list_all (Not ∘ isOVal) vl"
  using reachNT_reach unfolding Δ2_def by auto
  have own: "owner s PID ∈ set (userIDs s)" using reach_owner_userIDs[OF rs PID] .
  have adm: "admin s ∈ set (userIDs s)" using reach_admin_userIDs[OF rs own] .
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have ?match proof(cases "φ ?trn")
          case True note φ = True
          then obtain v where vl: "vl = v # vl'" and f: "f ?trn = v"
          using c unfolding consume_def φ_def2 by(cases vl) auto
          show ?thesis proof(cases v)
            case (PVal pst) note v = PVal
            have a: "a = Uact (uPost (owner s PID) (pass s (owner s PID)) PID pst)"
            using f_eq_PVal[OF step φ f[unfolded v]] .
            have ou: "ou = outOK" using step own PID unfolding a by (auto simp: u_defs)
            have op': "open s'" using step op PID PID' φ
            unfolding open_def a by (auto simp: u_defs)
            have pPID': "post s' PID = pst"
            using step φ PID op f op' unfolding a by(auto simp: u_defs)
            show ?thesis proof
              show "validTrans ?trn1" unfolding ss1 using step by simp
            next
              show "consume ?trn1 vl1 vl'" using φ vlvl1 unfolding ss1 consume_def vl f by auto
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
            next
              show "?Δ s' vl' s' vl'" using cor1 PID' pPID' op' lvl vlvl1 ss1
              unfolding Δ2_def vl v by auto
            qed
          next
            case (PValS aid pid) note v = PValS
            have a: "a = COMact (comSendPost (admin s) (pass s (admin s)) aid PID)"
            using f_eq_PValS[OF step φ f[unfolded v]] .
            have op': "open s'" using step op PID PID' φ
            unfolding open_def a by (auto simp: com_defs)
            have ou: "ou ≠ outErr" using φ op op' unfolding φ_def2[OF step] unfolding a by auto
            have pPID': "post s' PID = post s PID"
            using step φ PID op f op' unfolding a by(auto simp: com_defs)
            show ?thesis proof
              show "validTrans ?trn1" unfolding ss1 using step by simp
            next
              show "consume ?trn1 vl1 vl'" using φ vlvl1 unfolding ss1 consume_def vl f by auto
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
            next
              show "?Δ s' vl' s' vl'" using cor1 PID' pPID' op' lvl vlvl1 ss1
              unfolding Δ2_def vl v by auto
            qed
          qed(insert vl lvl, auto)
        next
          case False note φ = False
          hence vl': "vl' = vl" using c unfolding consume_def by auto
          have pPID': "post s' PID = post s PID"
            using step φ PID op
            apply(cases a)
            subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
            subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
            subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
            subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
            subgoal by fastforce
            subgoal by fastforce
            subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
            done
          have op': "open s'" using PID step φ op unfolding φ_def2[OF step] by auto
          show ?thesis proof
            show "validTrans ?trn1" unfolding ss1 using step by simp
          next
            show "consume ?trn1 vl1 vl" using φ vlvl1 unfolding ss1 consume_def vl' by simp
          next
            show "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
          next
            show "?Δ s' vl' s' vl" using cor1 PID' op' lvl vlvl1 pPID'
            unfolding Δ2_def vl' ss1 by auto
          qed
        qed
      thus ?thesis by simp
      qed
    qed
  thus ?thesis using vlvl1 by simp
  qed
qed

lemma unwind_cont_Δ4: "unwind_cont Δ4 {Δ1,Δ31,Δ32,Δ4}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨ Δ31 s vl s1 vl1 ∨ Δ32 s vl s1 vl1 ∨ Δ4 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ4 s vl s1 vl1"
  then obtain ul vll vll1 where vl: "vl = ul @ OVal False # vll" and vl1: "vl1 = ul @ OVal False # vll1"
  and rs: "reach s" and ss1: "s1 = s" and op: "open s" and PID: "PID ∈∈ postIDs s"
  and cor1: "corrFrom (post s1 PID) vl1" and lul: "list_all (Not ∘ isOVal) ul"
  and BC: "BC vll vll1"
  using reachNT_reach unfolding Δ4_def by blast
  have own: "owner s PID ∈ set (userIDs s)" using reach_owner_userIDs[OF rs PID] .
  have adm: "admin s ∈ set (userIDs s)" using reach_admin_userIDs[OF rs own] .
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ postIDs s'" using reach_postIDs_persist[OF PID step] .
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have ?match proof(cases "φ ?trn")
          case True note φ = True
          then obtain v where vl_vl': "vl = v # vl'" and f: "f ?trn = v"
          using c unfolding consume_def φ_def2 by(cases vl) auto
          show ?thesis proof(cases "ul = []")
            case False note ul = False
            then obtain ul' where ul: "ul = v # ul'" and vl': "vl' = ul' @ OVal False # vll"
            using c φ f unfolding consume_def vl by (cases ul) auto
            let ?vl1' = "ul' @ OVal False # vll1"
            show ?thesis proof(cases v)
              case (PVal pst) note v = PVal
              have a: "a = Uact (uPost (owner s PID) (pass s (owner s PID)) PID pst)"
              using f_eq_PVal[OF step φ f[unfolded v]] .
              have ou: "ou = outOK" using step own PID unfolding a by (auto simp: u_defs)
              have op': "open s'" using step op PID PID' φ
              unfolding open_def a by (auto simp: u_defs)
              have pPID': "post s' PID = pst"
              using step φ PID op f op' unfolding a by(auto simp: u_defs)
              show ?thesis proof
                show "validTrans ?trn1" unfolding ss1 using step by simp
              next
                show "consume ?trn1 vl1 ?vl1'" using φ
                unfolding ss1 consume_def vl f ul vl1 vl' by simp
              next
                show "γ ?trn = γ ?trn1" unfolding ss1 by simp
              next
                assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
              next
                have "Δ4 s' vl' s' ?vl1'" using cor1 PID' pPID' op' vl1 ss1 lul BC
                unfolding Δ4_def vl v ul vl' apply simp
                apply(rule exI[of _ ul'])
                apply(rule exI[of _ vll]) apply(rule exI[of _ vll1])
                by auto
                thus "?Δ s' vl' s' ?vl1'" by simp
              qed
            next
              case (PValS aid pid) note v = PValS
              have a: "a = COMact (comSendPost (admin s) (pass s (admin s)) aid PID)"
              using f_eq_PValS[OF step φ f[unfolded v]] .
              have op': "open s'" using step op PID PID' φ
              unfolding open_def a by (auto simp: com_defs)
              have ou: "ou ≠ outErr" using φ op op' unfolding φ_def2[OF step] unfolding a by auto
              have pPID': "post s' PID = post s PID"
              using step φ PID op f op' unfolding a by(auto simp: com_defs)
              show ?thesis proof
                show "validTrans ?trn1" unfolding ss1 using step by simp
              next
                show "consume ?trn1 vl1 ?vl1'" using φ
                unfolding ss1 consume_def vl f ul vl1 vl' by simp
              next
                show "γ ?trn = γ ?trn1" unfolding ss1 by simp
              next
                assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
              next
                have "Δ4 s' vl' s' ?vl1'" using cor1 PID' pPID' op' vl1 ss1 lul BC
                unfolding Δ4_def vl v ul vl' by auto
                thus "?Δ s' vl' s' ?vl1'" by simp
              qed
            qed(insert vl lul ul, auto)
          next
            case True note ul = True
            hence f: "f ?trn = OVal False" and vl': "vl' = vll"
            using vl c f φ unfolding consume_def ul by auto
            have op': "¬ open s'" using f_eq_OVal[OF step φ f] op by simp
            show ?thesis proof
              show "validTrans ?trn1" using step unfolding ss1 by simp
            next
              show "consume ?trn1 vl1 vll1" using ul φ c
              unfolding vl1 vl' vl ss1 consume_def by auto
            next
              show "γ ?trn = γ ?trn1" unfolding ss1 by simp
            next
              assume "γ ?trn" note γ = this
              thus "g ?trn = g ?trn1" unfolding ss1 by simp
            next
              have pPID': "post s' PID = post s PID"
                using step φ PID op op' f
                apply(cases a)
                subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
                subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
                subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
                subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
                subgoal by fastforce
                subgoal by fastforce
                subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
                done
              show "?Δ s' vl' s' vll1" using BC proof cases
                case BC_PVal
                hence "Δ1 s' vl' s' vll1" using PID' pPID' op' cor1 BC lul
                unfolding Δ1_def vl1 ul ss1 vl' by auto
                thus ?thesis by simp
              next
                case (BC_BO Vll Vll1 Ul Ul1 Sul)
                show ?thesis proof(cases "Ul ≠ [] ∧ Ul1 ≠ []")
                  case True
                  hence "Δ31 s' vl' s' vll1" using PID' pPID' op' cor1 BC BC_BO lul
                  unfolding Δ31_def vl1 ul ss1 vl' apply simp
                  apply(rule exI[of _ Ul]) apply(rule exI[of _ Ul1])
                  apply(rule exI[of _ Sul])
                  apply(rule exI[of _ Vll]) apply(rule exI[of _ Vll1])
                  by auto
                  thus ?thesis by simp
                next
                  case False
                  hence 0: "Ul = []" "Ul1 = []" using BC_BO by auto
                  hence "Δ32 s' vl' s' vll1" using PID' pPID' op' cor1 BC BC_BO lul
                  unfolding Δ32_def vl1 ul ss1 vl' apply simp
                  apply(rule exI[of _ Sul])
                  apply(rule exI[of _ Vll]) apply(rule exI[of _ Vll1])
                  by auto
                  thus ?thesis by simp
                qed
              qed
            qed
          qed
        next
          case False note φ = False
          hence vl': "vl' = vl" using c unfolding consume_def by auto
          have pPID': "post s' PID = post s PID"
            using step φ PID op
            apply(cases a)
            subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
            subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
            subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
            subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
            subgoal by fastforce
            subgoal by fastforce
            subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
            done
          have op': "open s'" using PID step φ op unfolding φ_def2[OF step] by auto
          show ?thesis proof
            show "validTrans ?trn1" unfolding ss1 using step by simp
          next
            show "consume ?trn1 vl1 vl1" using φ unfolding ss1 consume_def vl' vl vl1 by simp
          next
            show "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
          next
            have "Δ4 s' vl' s' vl1" using cor1 PID' pPID' op' vl1 ss1 lul BC
            unfolding Δ4_def vl vl' by auto
            thus "?Δ s' vl' s' vl1" by simp
          qed
        qed
      thus ?thesis by simp
      qed
    qed
  thus ?thesis using vl by simp
  qed
qed

definition Gr where
"Gr =
 {
 (Δ0, {Δ0,Δ1,Δ2,Δ31,Δ32,Δ4}),
 (Δ1, {Δ1,Δ11}),
 (Δ11, {Δ11}),
 (Δ2, {Δ2}),
 (Δ31, {Δ31,Δ32}),
 (Δ32, {Δ2,Δ32,Δ4}),
 (Δ4, {Δ1,Δ31,Δ32,Δ4})
 }"


theorem secure: secure
apply (rule unwind_decomp_secure_graph[of Gr Δ0])
unfolding Gr_def
apply (simp, smt insert_subset order_refl)
using
istate_Δ0 unwind_cont_Δ0 unwind_cont_Δ1 unwind_cont_Δ11
unwind_cont_Δ31 unwind_cont_Δ32 unwind_cont_Δ2 unwind_cont_Δ4
unfolding Gr_def by auto




end

end