[STATEMENT]
theorem post_accountability:
assumes v: "valid tr" and i: "srcOf (hd tr) = istate"
and PIDin: "PID \<in>\<in> postIDs (tgtOf (last tr))"
and PID: "vis (tgtOf (last tr)) PID = VIS"
shows "proper tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper tr
[PROOF STEP]
proof(cases "VIS = FriendV")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. VIS = FriendV \<Longrightarrow> proper tr
 2. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
VIS = FriendV

goal (2 subgoals):
 1. VIS = FriendV \<Longrightarrow> proper tr
 2. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
VIS = FriendV

goal (1 subgoal):
 1. proper tr
[PROOF STEP]
unfolding proper_def
[PROOF STATE]
proof (prove)
using this:
VIS = FriendV

goal (1 subgoal):
 1. VIS = FriendV \<or> (\<exists>uid tr1 trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proper tr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
VIS \<noteq> FriendV

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "proper2 tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper2 tr
[PROOF STEP]
using proper2_valid_istate[OF False v i PIDin]
[PROOF STATE]
proof (prove)
using this:
proper2 tr

goal (1 subgoal):
 1. proper2 tr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proper2 tr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proper2 tr
[PROOF STEP]
obtain uid tr1 trn trr where
  tr: "tr = tr1 @ trn # trr" and SNC: "SNC uid trn"
[PROOF STATE]
proof (prove)
using this:
proper2 tr

goal (1 subgoal):
 1. (\<And>tr1 trn trr uid. \<lbrakk>tr = tr1 @ trn # trr; SNC uid trn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proper2_def
[PROOF STATE]
proof (prove)
using this:
\<exists>uid tr1 trn tr2. tr = tr1 @ trn # tr2 \<and> SNC uid trn

goal (1 subgoal):
 1. (\<And>tr1 trn trr uid. \<lbrakk>tr = tr1 @ trn # trr; SNC uid trn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tr = tr1 @ trn # trr
SNC uid trn

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence trn: "validTrans trn" and r: "reach (srcOf trn)"
[PROOF STATE]
proof (prove)
using this:
tr = tr1 @ trn # trr
SNC uid trn

goal (1 subgoal):
 1. validTrans trn &&& reach (srcOf trn)
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
tr = tr1 @ trn # trr
SNC uid trn
valid tr

goal (1 subgoal):
 1. validTrans trn &&& reach (srcOf trn)
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
tr1 @ trn # trr = tr1 @ trn # trr
SNC uid trn
valid (tr1 @ trn # trr)

goal (1 subgoal):
 1. validTrans trn &&& reach (srcOf trn)
[PROOF STEP]
apply (metis list.distinct(2) self_append_conv2 valid_ConsE valid_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach (srcOf trn)
[PROOF STEP]
by (metis (mono_tags, lifting) append_Cons hd_append i list.sel(1) reach.simps tr v valid_append valid_init_reach)
[PROOF STATE]
proof (state)
this:
validTrans trn
reach (srcOf trn)

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence N: "PID \<in>\<in> postIDs (tgtOf trn)" "vis (tgtOf trn) PID \<noteq> VIS"
[PROOF STATE]
proof (prove)
using this:
validTrans trn
reach (srcOf trn)

goal (1 subgoal):
 1. PID \<in>\<in> postIDs (tgtOf trn) &&& vis (tgtOf trn) PID \<noteq> VIS
[PROOF STEP]
using SNC_postIDs SNC_visPost False SNC
[PROOF STATE]
proof (prove)
using this:
validTrans trn
reach (srcOf trn)
\<lbrakk>validTrans ?trn; SNC ?uid ?trn\<rbrakk> \<Longrightarrow> PID \<in>\<in> postIDs (tgtOf ?trn)
\<lbrakk>VIS \<noteq> FriendV; validTrans ?trn; SNC ?uid ?trn; reach (srcOf ?trn)\<rbrakk> \<Longrightarrow> vis (tgtOf ?trn) PID \<noteq> VIS
VIS \<noteq> FriendV
SNC uid trn

goal (1 subgoal):
 1. PID \<in>\<in> postIDs (tgtOf trn) &&& vis (tgtOf trn) PID \<noteq> VIS
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence trrNE: "trr \<noteq> []" and 1: "last tr = last trr"
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS

goal (1 subgoal):
 1. trr \<noteq> [] &&& last tr = last trr
[PROOF STEP]
using PID
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS
vis (tgtOf (last tr)) PID = VIS

goal (1 subgoal):
 1. trr \<noteq> [] &&& last tr = last trr
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS
vis (tgtOf (last (tr1 @ trn # trr))) PID = VIS

goal (1 subgoal):
 1. trr \<noteq> [] &&& last (tr1 @ trn # trr) = last trr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trr \<noteq> []
last tr = last trr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence trr_v: "valid trr"
[PROOF STATE]
proof (prove)
using this:
trr \<noteq> []
last tr = last trr

goal (1 subgoal):
 1. valid trr
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
trr \<noteq> []
last tr = last trr
valid tr

goal (1 subgoal):
 1. valid trr
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
trr \<noteq> []
last (tr1 @ trn # trr) = last trr
valid (tr1 @ trn # trr)

goal (1 subgoal):
 1. valid trr
[PROOF STEP]
by (metis valid_Cons_iff append_self_conv2 list.distinct(1) valid_append)
[PROOF STATE]
proof (state)
this:
valid trr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have 0: "tgtOf trn = srcOf (hd trr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tgtOf trn = srcOf (hd trr)
[PROOF STEP]
using v trrNE
[PROOF STATE]
proof (prove)
using this:
valid tr
trr \<noteq> []

goal (1 subgoal):
 1. tgtOf trn = srcOf (hd trr)
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
valid (tr1 @ trn # trr)
trr \<noteq> []

goal (1 subgoal):
 1. tgtOf trn = srcOf (hd trr)
[PROOF STEP]
by (metis valid_append list.distinct(2) self_append_conv2 valid_ConsE)
[PROOF STATE]
proof (state)
this:
tgtOf trn = srcOf (hd trr)

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "proper1 trr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper1 trr
[PROOF STEP]
using proper1_valid[OF False trr_v N[unfolded 0] PID[unfolded 1]]
[PROOF STATE]
proof (prove)
using this:
proper1 trr

goal (1 subgoal):
 1. proper1 trr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proper1 trr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
from proper1_never[OF trr_v N(1)[unfolded 0] this PID[unfolded 1]]
[PROOF STATE]
proof (chain)
picking this:
\<exists>tr2 trnn tr3. trr = tr2 @ trnn # tr3 \<and> SNVU (owner (srcOf trnn) PID) VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3)
[PROOF STEP]
obtain tr2 trnn tr3 where
  trr: "trr = tr2 @ trnn # tr3" and SNVU: "SNVU (owner (srcOf trnn) PID) VIS trnn"
  and vis: "\<forall> vis. never (SNVU (owner (srcOf trnn) PID) vis) tr3"
[PROOF STATE]
proof (prove)
using this:
\<exists>tr2 trnn tr3. trr = tr2 @ trnn # tr3 \<and> SNVU (owner (srcOf trnn) PID) VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3)

goal (1 subgoal):
 1. (\<And>tr2 trnn tr3. \<lbrakk>trr = tr2 @ trnn # tr3; SNVU (owner (srcOf trnn) PID) VIS trnn; \<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trr = tr2 @ trnn # tr3
SNVU (owner (srcOf trnn) PID) VIS trnn
\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have 00: "srcOf (hd (tr2 @ [trnn])) = tgtOf trn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. srcOf (hd (tr2 ## trnn)) = tgtOf trn
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
valid tr

goal (1 subgoal):
 1. srcOf (hd (tr2 ## trnn)) = tgtOf trn
[PROOF STEP]
unfolding tr trr
[PROOF STATE]
proof (prove)
using this:
valid (tr1 @ trn # tr2 @ trnn # tr3)

goal (1 subgoal):
 1. srcOf (hd (tr2 ## trnn)) = tgtOf trn
[PROOF STEP]
by (metis "0" append_self_conv2 hd_append2 list.sel(1) trr)
[PROOF STATE]
proof (state)
this:
srcOf (hd (tr2 ## trnn)) = tgtOf trn

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have trnn: "validTrans trnn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans trnn
[PROOF STEP]
using trr_v
[PROOF STATE]
proof (prove)
using this:
valid trr

goal (1 subgoal):
 1. validTrans trnn
[PROOF STEP]
unfolding trr
[PROOF STATE]
proof (prove)
using this:
valid (tr2 @ trnn # tr3)

goal (1 subgoal):
 1. validTrans trnn
[PROOF STEP]
by (metis valid_Cons_iff append_self_conv2 list.distinct(1) valid_append)
[PROOF STATE]
proof (state)
this:
validTrans trnn

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have vv: "valid (tr2 @ [trnn])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid (tr2 ## trnn)
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
valid tr

goal (1 subgoal):
 1. valid (tr2 ## trnn)
[PROOF STEP]
unfolding tr trr
[PROOF STATE]
proof (prove)
using this:
valid (tr1 @ trn # tr2 @ trnn # tr3)

goal (1 subgoal):
 1. valid (tr2 ## trnn)
[PROOF STEP]
by (smt Nil_is_append_conv append_self_conv2 hd_append2 list.distinct(1) list.sel(1)
        valid_Cons_iff valid_append)
[PROOF STATE]
proof (state)
this:
valid (tr2 ## trnn)

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "uid = owner (tgtOf trn) PID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uid = owner (tgtOf trn) PID
[PROOF STEP]
using SNC trn SNC_owner
[PROOF STATE]
proof (prove)
using this:
SNC uid trn
validTrans trn
\<lbrakk>validTrans ?trn; SNC ?uid ?trn\<rbrakk> \<Longrightarrow> ?uid = owner (tgtOf ?trn) PID

goal (1 subgoal):
 1. uid = owner (tgtOf trn) PID
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uid = owner (tgtOf trn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
uid = owner (tgtOf trn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "... = owner (tgtOf trnn) PID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. owner (tgtOf trn) PID = owner (tgtOf trnn) PID
[PROOF STEP]
using owner_valid[OF vv] N(1)
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (srcOf (hd (tr2 ## trnn))) \<Longrightarrow> owner (srcOf (hd (tr2 ## trnn))) PID = owner (tgtOf (last (tr2 ## trnn))) PID
PID \<in>\<in> postIDs (tgtOf trn)

goal (1 subgoal):
 1. owner (tgtOf trn) PID = owner (tgtOf trnn) PID
[PROOF STEP]
unfolding 00
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn) \<Longrightarrow> owner (tgtOf trn) PID = owner (tgtOf (last (tr2 ## trnn))) PID
PID \<in>\<in> postIDs (tgtOf trn)

goal (1 subgoal):
 1. owner (tgtOf trn) PID = owner (tgtOf trnn) PID
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
owner (tgtOf trn) PID = owner (tgtOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
owner (tgtOf trn) PID = owner (tgtOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "... = owner (srcOf trnn) PID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. owner (tgtOf trnn) PID = owner (srcOf trnn) PID
[PROOF STEP]
using SNVU trnn SNVU_postIDs owner_validTrans
[PROOF STATE]
proof (prove)
using this:
SNVU (owner (srcOf trnn) PID) VIS trnn
validTrans trnn
\<lbrakk>validTrans ?trn; SNVU ?uid ?vs ?trn\<rbrakk> \<Longrightarrow> PID \<in>\<in> postIDs (srcOf ?trn)
\<lbrakk>validTrans ?trn; PID \<in>\<in> postIDs (srcOf ?trn)\<rbrakk> \<Longrightarrow> owner (srcOf ?trn) PID = owner (tgtOf ?trn) PID

goal (1 subgoal):
 1. owner (tgtOf trnn) PID = owner (srcOf trnn) PID
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
owner (tgtOf trnn) PID = owner (srcOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
uid = owner (srcOf trnn) PID
[PROOF STEP]
have uid: "uid = owner (srcOf trnn) PID"
[PROOF STATE]
proof (prove)
using this:
uid = owner (srcOf trnn) PID

goal (1 subgoal):
 1. uid = owner (srcOf trnn) PID
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
uid = owner (srcOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper tr
[PROOF STEP]
unfolding proper_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VIS = FriendV \<or> (\<exists>uid tr1 trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3))
[PROOF STEP]
apply(rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>uid tr1 trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
apply(intro exI[of _ uid] exI[of _ tr1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
apply(rule exI[of _ trn], rule exI[of _ tr2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
apply(intro exI[of _ trnn] exI[of _ tr3])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
using SNC SNVU vis
[PROOF STATE]
proof (prove)
using this:
SNC uid trn
SNVU (owner (srcOf trnn) PID) VIS trnn
\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3

goal (1 subgoal):
 1. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
unfolding tr trr uid
[PROOF STATE]
proof (prove)
using this:
SNC (owner (srcOf trnn) PID) trn
SNVU (owner (srcOf trnn) PID) VIS trnn
\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3

goal (1 subgoal):
 1. tr1 @ trn # tr2 @ trnn # tr3 = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC (owner (srcOf trnn) PID) trn \<and> SNVU (owner (srcOf trnn) PID) VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proper tr

goal:
No subgoals!
[PROOF STEP]
qed