Theory Friend_Request
theory Friend_Request
imports
"Friend_Request_Value_Setup"
"Bounded_Deducibility_Security.Compositional_Reasoning"
begin
subsection ‹Declassification bound›
context Friend
begin
fun T :: "(state,act,out) trans ⇒ bool"
where "T trn = False"
text ‹Friendship updates form an alternating sequence of friending and unfriending,
and every successful friend creation is preceded by one or two friendship requests.›
fun validValSeq :: "value list ⇒ bool ⇒ bool ⇒ bool ⇒ bool" where
"validValSeq [] _ _ _ = True"
| "validValSeq (FRVal U1 req # vl) st r1 r2 ⟷ (¬st) ∧ (¬r1) ∧ validValSeq vl st True r2"
| "validValSeq (FRVal U2 req # vl) st r1 r2 ⟷ (¬st) ∧ (¬r2) ∧ validValSeq vl st r1 True"
| "validValSeq (FVal True # vl) st r1 r2 ⟷ (¬st) ∧ (r1 ∨ r2) ∧ validValSeq vl True False False"
| "validValSeq (FVal False # vl) st r1 r2 ⟷ st ∧ (¬r1) ∧ (¬r2) ∧ validValSeq vl False False False"
| "validValSeq (OVal True # vl) st r1 r2 ⟷ validValSeq vl st r1 r2"
| "validValSeq (OVal False # vl) st r1 r2 ⟷ validValSeq vl st r1 r2"
abbreviation validValSeqFrom :: "value list ⇒ state ⇒ bool"
where "validValSeqFrom vl s
≡ validValSeq vl (friends12 s) (UID1 ∈∈ pendingFReqs s UID2) (UID2 ∈∈ pendingFReqs s UID1)"
text ‹With respect to the friendship status updates, we use the same
``while-or-last-before'' bound as for friendship status confidentiality.›
inductive BO :: "value list ⇒ value list ⇒ bool"
and BC :: "value list ⇒ value list ⇒ bool"
where
BO_FVal[simp,intro!]:
"BO (map FVal fs) (map FVal fs)"
|BO_BC[intro]:
"BC vl vl1 ⟹
BO (map FVal fs @ OVal False # vl) (map FVal fs @ OVal False # vl1)"
|BC_FVal[simp,intro!]:
"BC (map FVal fs) (map FVal fs1)"
|BC_BO[intro]:
"BO vl vl1 ⟹ (fs = [] ⟷ fs1 = []) ⟹ (fs ≠ [] ⟹ last fs = last fs1) ⟹
BC (map FVal fs @ OVal True # vl)
(map FVal fs1 @ OVal True # vl1)"
text ‹Taking into account friendship requests, two value sequences ‹vl› and ‹vl1› are in the bound if
▪ ‹vl1› (with friendship requests) forms a valid value sequence,
▪ ‹vl› and ‹vl1› are in ‹BO› (without friendship requests),
▪ ‹vl1› is empty if ‹vl› is empty, and
▪ ‹vl1› begins with \<^term>‹OVal False› if ‹vl› begins with \<^term>‹OVal False›.
The last two points are due to the fact that \<^term>‹UID1› and \<^term>‹UID1› might not exist yet
if ‹vl› is empty (or before \<^term>‹OVal False›), in which case the observer can deduce that no
friendship request has happened yet.›
definition "B vl vl1 ≡ BO (filter (Not o isFRVal) vl) (filter (Not o isFRVal) vl1) ∧
validValSeqFrom vl1 istate ∧
(vl = [] ⟶ vl1 = []) ∧
(vl ≠ [] ∧ hd vl = OVal False ⟶ vl1 ≠ [] ∧ hd vl1 = OVal False)"
lemma BO_Nil_iff: "BO vl vl1 ⟹ vl = [] ⟷ vl1 = []"
by (cases rule: BO.cases) auto
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
subsection ‹Unwinding proof›
lemma validFrom_validValSeq:
assumes "validFrom s tr"
and "reach s"
shows "validValSeqFrom (V tr) s"
using assms proof (induction tr arbitrary: s)
case (Cons trn tr s)
then obtain a ou s' where trn: "trn = Trans s a ou s'"
and step: "step s a = (ou, s')"
and tr: "validFrom s' tr"
and s': "reach s'"
by (cases trn) (auto iff: validFrom_Cons intro: reach_PairI)
then have vVS_tr: "validValSeqFrom (V tr) s'" by (intro Cons.IH)
show ?case proof cases
assume φ: "φ (Trans s a ou s')"
then have V: "V (Trans s a ou s' # tr) = f (Trans s a ou s') # V tr" by auto
from φ vVS_tr Cons.prems step show ?thesis unfolding trn V by (elim φE) auto
next
assume "¬φ (Trans s a ou s')"
then have "V (Trans s a ou s' # tr) = V tr" and "friends12 s' = friends12 s"
and "UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2"
and "UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1"
using step_friends12_φ[OF step] step_pendingFReqs_φ[OF step] by auto
with vVS_tr show ?thesis unfolding trn by auto
qed
qed auto
lemma "validFrom istate tr ⟹ validValSeqFrom (V tr) istate"
using validFrom_validValSeq[of istate] reach.Istate unfolding istate_def friends12_def
by auto
lemma produce_FRVal:
assumes rs: "reach s"
and IDs: "IDsOK s [UID1, UID2] [] [] []"
and vVS: "validValSeqFrom (FRVal u req # vl) s"
obtains a uid uid' s'
where "step s a = (outOK, s')"
and "a = Cact (cFriendReq uid (pass s uid) uid' req)"
and "uid = UID1 ∧ uid' = UID2 ∨ uid = UID2 ∧ uid' = UID1"
and "φ (Trans s a outOK s')"
and "f (Trans s a outOK s') = FRVal u req"
and "validValSeqFrom vl s'"
proof (cases u)
case U1
then have "step s (Cact (cFriendReq UID1 (pass s UID1) UID2 req)) =
(outOK, createFriendReq s UID1 (pass s UID1) UID2 req)"
and "¬friends12 (createFriendReq s UID1 (pass s UID1) UID2 req)"
using IDs vVS reach_friendIDs_symmetric[OF rs] by (auto simp: c_defs friends12_def)
then show thesis using U1 vVS UID1_UID2 by (intro that[of _ _ UID1 UID2]) (auto simp: c_defs)
next
case U2
then have "step s (Cact (cFriendReq UID2 (pass s UID2) UID1 req)) =
(outOK, createFriendReq s UID2 (pass s UID2) UID1 req)"
and "¬friends12 (createFriendReq s UID2 (pass s UID2) UID1 req)"
using IDs vVS reach_friendIDs_symmetric[OF rs] by (auto simp: c_defs friends12_def)
then show thesis using U2 vVS UID1_UID2 by (intro that[of _ _ UID2 UID1]) (auto simp: c_defs)
qed
lemma toggle_friends12_True:
assumes rs: "reach s"
and IDs: "IDsOK s [UID1, UID2] [] [] []"
and nf12: "¬friends12 s"
and vVS: "validValSeqFrom (FVal True # vl) s"
obtains a uid uid' s'
where "step s a = (outOK, s')"
and "a = Cact (cFriend uid (pass s uid) uid')"
and "s' = createFriend s UID1 (pass s UID1) UID2"
and "uid = UID1 ∧ uid' = UID2 ∨ uid = UID2 ∧ uid' = UID1"
and "friends12 s'"
and "eqButUID s s'"
and "φ (Trans s a outOK s')"
and "f (Trans s a outOK s') = FVal True"
and "¬γ (Trans s a outOK s')"
and "validValSeqFrom vl s'"
proof -
from vVS have "UID1 ∈∈ pendingFReqs s UID2 ∨ UID2 ∈∈ pendingFReqs s UID1" by auto
then show thesis proof
assume pFR: "UID1 ∈∈ pendingFReqs s UID2"
let ?a = "Cact (cFriend UID2 (pass s UID2) UID1)"
let ?s' = "createFriend s UID1 (pass s UID1) UID2"
let ?trn = "Trans s ?a outOK ?s'"
have step: "step s ?a = (outOK, ?s')" using IDs pFR UID1_UID2
unfolding createFriend_sym[of "s" "UID1" "pass s UID1" "UID2" "pass s UID2"]
by (auto simp add: c_defs)
moreover then have "φ ?trn" and "f ?trn = FVal True" and "friends12 ?s'"
and "UID1 ∉ set (pendingFReqs ?s' UID2)"
and "UID2 ∉ set (pendingFReqs ?s' UID1)"
using reach_distinct_friends_reqs[OF rs] by (auto simp: c_defs friends12_def)
moreover have "¬γ ?trn" using UID1_UID2_UIDs by auto
ultimately show thesis using nf12 rs vVS
by (intro that[of "?a" "?s'" UID2 UID1]) (auto intro: Cact_cFriend_step_eqButUID)
next
assume pFR: "UID2 ∈∈ pendingFReqs s UID1"
let ?a = "Cact (cFriend UID1 (pass s UID1) UID2)"
let ?s' = "createFriend s UID1 (pass s UID1) UID2"
let ?trn = "Trans s ?a outOK ?s'"
have step: "step s ?a = (outOK, ?s')" using IDs pFR UID1_UID2 by (auto simp add: c_defs)
moreover then have "φ ?trn" and "f ?trn = FVal True" and "friends12 ?s'"
and "UID1 ∉ set (pendingFReqs ?s' UID2)"
and "UID2 ∉ set (pendingFReqs ?s' UID1)"
using reach_distinct_friends_reqs[OF rs] by (auto simp: c_defs friends12_def)
moreover have "¬γ ?trn" using UID1_UID2_UIDs by auto
ultimately show thesis using nf12 rs vVS
by (intro that[of "?a" "?s'" UID1 UID2]) (auto intro: Cact_cFriend_step_eqButUID)
qed
qed
lemma toggle_friends12_False:
assumes rs: "reach s"
and IDs: "IDsOK s [UID1, UID2] [] [] []"
and f12: "friends12 s"
and vVS: "validValSeqFrom (FVal False # vl) s"
obtains a s'
where "step s a = (outOK, s')"
and "a = Dact (dFriend UID1 (pass s UID1) UID2)"
and "s' = deleteFriend s UID1 (pass s UID1) UID2"
and "¬friends12 s'"
and "eqButUID s s'"
and "φ (Trans s a outOK s')"
and "f (Trans s a outOK s') = FVal False"
and "¬γ (Trans s a outOK s')"
and "validValSeqFrom vl s'"
proof -
let ?a = "Dact (dFriend UID1 (pass s UID1) UID2)"
let ?s' = "deleteFriend s UID1 (pass s UID1) UID2"
let ?trn = "Trans s ?a outOK ?s'"
have "UID1 ∉ set (pendingFReqs s UID2)" "UID2 ∉ set (pendingFReqs s UID1)"
using f12 reach_distinct_friends_reqs[OF rs] unfolding friends12_def by auto
then have step: "step s ?a = (outOK, ?s')"
and "UID1 ∉ set (pendingFReqs ?s' UID2)" "UID2 ∉ set (pendingFReqs ?s' UID1)"
using IDs f12 UID1_UID2 by (auto simp add: d_defs friends12_def)
moreover then have "φ ?trn" and "f ?trn = FVal False" and "¬friends12 ?s'"
using reach_friendIDs_symmetric[OF rs] by (auto simp: d_defs friends12_def)
moreover have "¬γ ?trn" using UID1_UID2_UIDs by auto
ultimately show thesis using f12 rs vVS
by (intro that[of ?a ?s']) (auto intro: Dact_dFriend_step_eqButUID)
qed
lemma toggle_friends12:
assumes rs: "reach s"
and IDs: "IDsOK s [UID1, UID2] [] [] []"
and f12: "friends12 s ≠ fv"
and vVS: "validValSeqFrom (FVal fv # vl) s"
obtains a s'
where "step s a = (outOK, s')"
and "friends12 s' = fv"
and "eqButUID s s'"
and "φ (Trans s a outOK s')"
and "f (Trans s a outOK s') = FVal fv"
and "¬γ (Trans s a outOK s')"
and "validValSeqFrom vl s'"
proof (cases "friends12 s")
case True
moreover then have "UID1 ∉ set (pendingFReqs s UID2)" "UID2 ∉ set (pendingFReqs s UID1)"
and "fv = False"
and vVS: "validValSeqFrom (FVal False # vl) s"
using reach_distinct_friends_reqs[OF rs] vVS f12 unfolding friends12_def by auto
moreover then have "UID1 ∉ set (pendingFReqs (deleteFriend s UID1 (pass s UID1) UID2) UID2)"
"UID2 ∉ set (pendingFReqs (deleteFriend s UID1 (pass s UID1) UID2) UID1)"
by (auto simp: d_defs)
ultimately show thesis using assms
by (elim toggle_friends12_False, blast, blast, blast) (elim that, blast+)
next
case False
moreover then have "fv = True"
and vVS: "validValSeqFrom (FVal True # vl) s"
using vVS f12 by auto
moreover have "UID1 ∉ set (pendingFReqs (createFriend s UID1 (pass s UID1) UID2) UID2)"
"UID2 ∉ set (pendingFReqs (createFriend s UID1 (pass s UID1) UID2) UID1)"
using reach_distinct_friends_reqs[OF rs] by (auto simp: c_defs)
ultimately show thesis using assms
by (elim toggle_friends12_True, blast, blast, blast) (elim that, blast+)
qed
lemma BO_cases:
assumes "BO vl vl1"
obtains (Nil) "vl = []" and "vl1 = []"
| (FVal) fv vl' vl1' where "vl = FVal fv # vl'" and "vl1 = FVal fv # vl1'" and "BO vl' vl1'"
| (OVal) vl' vl1' where "vl = OVal False # vl'" and "vl1 = OVal False # vl1'" and "BC vl' vl1'"
using assms proof (cases rule: BO.cases)
case (BO_FVal fs) then show thesis by (cases fs) (auto intro: Nil FVal) next
case (BO_BC vl'' vl1'' fs) then show thesis by (cases fs) (auto intro: FVal OVal)
qed
lemma BC_cases:
assumes "BC vl vl1"
obtains (Nil) "vl = []" and "vl1 = []"
| (FVal) fv fs where "vl = FVal fv # map FVal fs" and "vl1 = []"
| (FVal1) fv fs fs1 where "vl = map FVal fs" and "vl1 = FVal fv # map FVal fs1"
| (BO_FVal) fv fv' fs vl' vl1' where "vl = FVal fv # map FVal fs @ FVal fv' # OVal True # vl'"
and "vl1 = FVal fv' # OVal True # vl1'" and "BO vl' vl1'"
| (BO_FVal1) fv fv' fs fs1 vl' vl1' where "vl = map FVal fs @ FVal fv' # OVal True # vl'"
and "vl1 = FVal fv # map FVal fs1 @ FVal fv' # OVal True # vl1'"
and "BO vl' vl1'"
| (FVal_BO) fv vl' vl1' where "vl = FVal fv # OVal True # vl'"
and "vl1 = FVal fv # OVal True # vl1'" and "BO vl' vl1'"
| (OVal) vl' vl1' where "vl = OVal True # vl'" and "vl1 = OVal True # vl1'" and "BO vl' vl1'"
using assms proof (cases rule: BC.cases)
case (BC_FVal fs fs1)
then show ?thesis proof (induction fs1)
case Nil then show ?case by (induction fs) (auto intro: that(1,2)) next
case (Cons fv fs1') then show ?case by (intro that(3)) auto
qed
next
case (BC_BO vl' vl1' fs fs1)
then show ?thesis proof (cases fs1 rule: rev_cases)
case Nil then show ?thesis using BC_BO by (intro that(7)) auto next
case (snoc fs1' fv')
moreover then obtain fs' where "fs = fs' ## fv'" using BC_BO
by (induction fs rule: rev_induct) auto
ultimately show ?thesis using BC_BO proof (induction fs1')
case Nil
then show ?thesis proof (induction fs')
case Nil then show ?thesis by (intro that(6)) auto next
case (Cons fv'' fs'') then show ?thesis by (intro that(4)) auto
qed
next
case (Cons fv'' fs1'') then show ?thesis by (intro that(5)) auto
qed
qed
qed
definition Δ0 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ0 s vl s1 vl1 ≡
s = s1 ∧ B vl vl1 ∧ open s ∧ (¬IDsOK s [UID1, UID2] [] [] [])"
definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡
eqButUID s s1 ∧ friendIDs s = friendIDs s1 ∧ open s ∧
BO (filter (Not o isFRVal) vl) (filter (Not o isFRVal) vl1) ∧
validValSeqFrom vl1 s1 ∧
IDsOK s1 [UID1, UID2] [] [] []"
definition Δ2 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ2 s vl s1 vl1 ≡ (∃fs fs1.
eqButUID s s1 ∧ ¬open s ∧
validValSeqFrom vl1 s1 ∧
filter (Not o isFRVal) vl = map FVal fs ∧
filter (Not o isFRVal) vl1 = map FVal fs1)"
definition Δ3 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ3 s vl s1 vl1 ≡ (∃fs fs1 vlr vlr1.
eqButUID s s1 ∧ ¬open s ∧ BO vlr vlr1 ∧
validValSeqFrom vl1 s1 ∧
(fs = [] ⟷ fs1 = []) ∧
(fs ≠ [] ⟶ last fs = last fs1) ∧
(fs = [] ⟶ friendIDs s = friendIDs s1) ∧
filter (Not o isFRVal) vl = map FVal fs @ OVal True # vlr ∧
filter (Not o isFRVal) vl1 = map FVal fs1 @ OVal True # vlr1)"
lemma Δ2_I:
assumes "eqButUID s s1" "¬open s"
"validValSeqFrom vl1 s1"
"filter (Not o isFRVal) vl = map FVal fs"
"filter (Not o isFRVal) vl1 = map FVal fs1"
shows "Δ2 s vl s1 vl1"
using assms unfolding Δ2_def by blast
lemma Δ3_I:
assumes "eqButUID s s1" "¬open s" "BO vlr vlr1"
"validValSeqFrom vl1 s1"
"fs = [] ⟷ fs1 = []" "fs ≠ [] ⟶ last fs = last fs1"
"fs = [] ⟶ friendIDs s = friendIDs s1"
"filter (Not o isFRVal) vl = map FVal fs @ OVal True # vlr"
"filter (Not o isFRVal) vl1 = map FVal fs1 @ OVal True # vlr1"
shows "Δ3 s vl s1 vl1"
using assms unfolding Δ3_def by blast
lemma istate_Δ0:
assumes B: "B vl vl1"
shows "Δ0 istate vl istate vl1"
using assms unfolding Δ0_def istate_def B_def open_def openByA_def openByF_def friends12_def
by auto
lemma unwind_cont_Δ0: "unwind_cont Δ0 {Δ0,Δ1,Δ2,Δ3}"
proof(rule, simp)
let ?Δ = "λs vl s1 vl1. Δ0 s vl s1 vl1 ∨
Δ1 s vl s1 vl1 ∨
Δ2 s vl s1 vl1 ∨
Δ3 s vl s1 vl1"
fix s s1 :: state and vl vl1 :: "value list"
assume rsT: "reachNT s" and rs1: "reach s1" and Δ0: "Δ0 s vl s1 vl1"
then have rs: "reach s" and ss1: "s1 = s" and B: "B vl vl1" and os: "open s"
and IDs: "¬IDsOK s [UID1, UID2] [] [] []"
using reachNT_reach unfolding Δ0_def by auto
from IDs have "UID1 ∉ set (pendingFReqs s UID2)" and "¬friends12 s"
and "UID2 ∉ set (pendingFReqs s UID1)"
using reach_IDs_used_IDsOK[OF rs] unfolding friends12_def by auto
with B have BO: "BO (filter (Not ∘ isFRVal) vl) (filter (Not ∘ isFRVal) vl1)"
and vl_vl1: "vl = [] ⟶ vl1 = []"
and vl_OVal: "vl ≠ [] ∧ hd vl = OVal False ⟶ vl1 ≠ [] ∧ hd vl1 = OVal False"
and vVS: "validValSeqFrom vl1 s"
unfolding B_def by (auto simp: istate_def friends12_def)
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'"
assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
proof cases
assume φ: "φ ?trn"
then obtain uid p uid' p' where a: "a = Cact (cUser uid p uid' p')"
"¬openByA s'" "¬openByF s'"
"ou = outOK" "f ?trn = OVal False"
"friends12 s' = friends12 s"
"UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2"
"UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1"
using step rs IDs by (elim φE) (auto simp: openByA_def)
with c φ have vl: "vl = OVal False # vl'" unfolding consume_def by auto
with vl_OVal obtain vl1' where vl1: "vl1 = OVal False # vl1'" by (cases vl1) auto
from BO vl vl1 have BC': "BC (filter (Not ∘ isFRVal) vl') (filter (Not ∘ isFRVal) vl1')"
by (cases rule: BO_cases) auto
then have "Δ2 s' vl' s' vl1' ∨ Δ3 s' vl' s' vl1'" using vVS a unfolding vl1
proof (cases rule: BC.cases)
case BC_FVal
then show ?thesis using vVS a unfolding vl1
by (intro disjI1 Δ2_I) (auto simp: open_def)
next
case BC_BO
then show ?thesis using vVS a unfolding vl1
by (intro disjI2 Δ3_I) (auto simp: open_def)
qed
then have ?match using step a φ unfolding ss1 vl1
by (intro matchI[of s a ou s']) (auto simp: consume_def)
then show ?thesis ..
next
assume nφ: "¬φ ?trn"
then have s': "open s'" "friends12 s' = friends12 s"
"UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2"
"UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1"
using os step_open_φ[OF step] step_friends12_φ[OF step] step_pendingFReqs_φ[OF step]
by auto
moreover have "vl' = vl" using nφ c by (auto simp: consume_def)
ultimately have "Δ0 s' vl' s' vl1 ∨ Δ1 s' vl' s' vl1"
using vVS B BO unfolding Δ0_def Δ1_def
by (cases "IDsOK s' [UID1, UID2] [] [] []") auto
then have ?match using step c nφ unfolding ss1
by (intro matchI[of s a ou s']) (auto simp: consume_def)
then show ?thesis ..
qed
qed
then show ?thesis using vl_vl1 by auto
qed
qed
lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1,Δ2,Δ3}"
proof(rule, simp)
let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨
Δ2 s vl s1 vl1 ∨
Δ3 s vl s1 vl1"
fix s s1 :: state and vl vl1 :: "value list"
assume rsT: "reachNT s" and rs1: "reach s1" and Δ1: "Δ1 s vl s1 vl1"
then have rs: "reach s" and ss1: "eqButUID s s1" and fIDs: "friendIDs s = friendIDs s1"
and os: "open s" and BO: "BO (filter (Not o isFRVal) vl) (filter (Not o isFRVal) vl1)"
and vVS1: "validValSeq vl1 (friends12 s1)
(UID1 ∈∈ pendingFReqs s1 UID2)
(UID2 ∈∈ pendingFReqs s1 UID1)" (is "?vVS vl1 s1")
and IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
using reachNT_reach unfolding Δ1_def by auto
show "iaction ?Δ s vl s1 vl1 ∨
((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
proof cases
assume "∃u req vl1'. vl1 = FRVal u req # vl1'"
then obtain u req vl1' where vl1: "vl1 = FRVal u req # vl1'" by auto
obtain a uid uid' s1' where step1: "step s1 a = (outOK, s1')" and "φ (Trans s1 a outOK s1')"
and a: "a = Cact (cFriendReq uid (pass s1 uid) uid' req)"
and uid: "uid = UID1 ∧ uid' = UID2 ∨ uid = UID2 ∧ uid' = UID1"
and "f (Trans s1 a outOK s1') = FRVal u req" and "?vVS vl1' s1'"
using rs1 IDs1 vVS1 UID1_UID2_UIDs unfolding vl1 by (blast intro: produce_FRVal)
moreover then have "¬γ (Trans s1 a outOK s1')" using UID1_UID2_UIDs by auto
moreover have "eqButUID s1 s1'" using step1 a uid by (auto intro: Cact_cFriendReq_step_eqButUID)
moreover have "friendIDs s1' = friendIDs s1" and "IDsOK s1' [UID1, UID2] [] [] []"
using step1 a uid by (auto simp: c_defs)
ultimately have "?iact" using ss1 fIDs os BO unfolding vl1
by (intro iactionI[of s1 a "outOK" s1']) (auto simp: consume_def Δ1_def intro: eqButUID_trans)
then show ?thesis ..
next
assume nFRVal1: "¬ (∃u req vl1'. vl1 = FRVal u req # vl1')"
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'"
show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
proof cases
assume φ: "φ ?trn"
then have vl: "vl = f ?trn # vl'" using c by (auto simp: consume_def)
from BO show ?thesis proof (cases "f ?trn")
case (FVal fv)
with BO obtain vl1' where vl1: "vl1 = f ?trn # vl1'"
using BO_Nil_iff[OF BO] FVal vl nFRVal1
by (cases rule: BO_cases; cases vl1; cases "hd vl1") auto
with BO have BO': "BO (filter (Not o isFRVal) vl') (filter (Not o isFRVal) vl1')"
using FVal vl by (cases rule: BO_cases) auto
from fIDs have f12: "friends12 s = friends12 s1" unfolding friends12_def by auto
have ?match using φ step rs FVal proof (cases rule: φE)
case (Friend uid p uid')
then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
using ss1 unfolding eqButUID_def by auto
let ?s1' = "createFriend s1 UID1 (pass s1 UID1) UID2"
have s': "s' = createFriend s UID1 p UID2"
using Friend step by (auto simp: createFriend_sym)
have ss': "eqButUID s s'" using rs step Friend
by (auto intro: Cact_cFriend_step_eqButUID)
moreover then have os': "open s'" using os eqButUID_open_eq by auto
moreover obtain a1 uid1 uid1' p1
where "step s1 a1 = (outOK, ?s1')" "friends12 ?s1'"
"a1 = Cact (cFriend uid1 p1 uid1')"
"uid1 = UID1 ∧ uid1' = UID2 ∨ uid1 = UID2 ∧ uid1' = UID1"
"φ (Trans s1 a1 outOK ?s1')"
"f (Trans s1 a1 outOK ?s1') = FVal True"
"eqButUID s1 ?s1'" "?vVS vl1' ?s1'"
using rs1 IDs1 Friend vVS1 unfolding vl1 f12 Friend(3)
by (elim toggle_friends12_True) blast+
moreover then have "IDsOK ?s1' [UID1, UID2] [] [] []" by (auto simp: c_defs)
moreover have "friendIDs s' = friendIDs ?s1'"
using Friend(6) f12 unfolding s'
by (intro eqButUID_createFriend12_friendIDs_eq[OF ss1 rs rs1]) auto
ultimately show ?match using ss1 BO' Friend UID1_UID2_UIDs unfolding vl1 Δ1_def
by (intro matchI[of s1 a1 "outOK" ?s1'])
(auto simp: consume_def intro: eqButUID_trans eqButUID_sym)
next
case (Unfriend uid p uid')
then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
using ss1 unfolding eqButUID_def by auto
let ?s1' = "deleteFriend s1 UID1 (pass s1 UID1) UID2"
have s': "s' = deleteFriend s UID1 p UID2"
using Unfriend step by (auto simp: deleteFriend_sym)
have ss': "eqButUID s s'" using rs step Unfriend
by (auto intro: Dact_dFriend_step_eqButUID)
moreover then have os': "open s'" using os eqButUID_open_eq by auto
moreover obtain a1 uid1 uid1' p1
where "step s1 a1 = (outOK, ?s1')" "¬friends12 ?s1'"
"a1 = Dact (dFriend uid1 p1 uid1')"
"uid1 = UID1 ∧ uid1' = UID2 ∨ uid1 = UID2 ∧ uid1' = UID1"
"φ (Trans s1 a1 outOK ?s1')"
"f (Trans s1 a1 outOK ?s1') = FVal False"
"eqButUID s1 ?s1'" "?vVS vl1' ?s1'"
using rs1 IDs1 Unfriend vVS1 unfolding vl1 f12 Unfriend(3)
by (elim toggle_friends12_False) blast+
moreover have "friendIDs s' = friendIDs ?s1'" "IDsOK ?s1' [UID1, UID2] [] [] []"
using fIDs IDs1 unfolding s' by (auto simp: d_defs)
ultimately show ?match using ss1 BO' Unfriend UID1_UID2_UIDs unfolding vl1 Δ1_def
by (intro matchI[of s1 a1 "outOK" ?s1'])
(auto simp: consume_def intro: eqButUID_trans eqButUID_sym)
qed auto
then show ?thesis ..
next
case (OVal ov)
with BO obtain vl1' where vl1': "vl1 = OVal False # vl1'"
using BO_Nil_iff[OF BO] OVal vl nFRVal1
by (cases rule: BO_cases; cases vl1; cases "hd vl1") auto
with BO have BC': "BC (filter (Not o isFRVal) vl') (filter (Not o isFRVal) vl1')"
using OVal vl by (cases rule: BO_cases) auto
from BO vl OVal have "f ?trn = OVal False" by (cases rule: BO_cases) auto
with φ step rs have ?match proof (cases rule: φE)
case (CloseF uid p uid')
let ?s1' = "deleteFriend s1 uid p uid'"
let ?trn1 = "Trans s1 a outOK ?s1'"
have s': "s' = deleteFriend s uid p uid'" using CloseF step by auto
have step1: "step s1 a = (outOK, ?s1')"
and pFR1': "pendingFReqs ?s1' = pendingFReqs s1"
using CloseF step ss1 fIDs unfolding eqButUID_def by (auto simp: d_defs)
have s's1': "eqButUID s' ?s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
moreover have os': "¬open s'" using CloseF os unfolding open_def by auto
moreover have fIDs': "friendIDs s' = friendIDs ?s1'"
using fIDs unfolding s' by (auto simp: d_defs)
moreover have f12s1: "friends12 s1 = friends12 ?s1'"
using CloseF(2) UID1_UID2_UIDs unfolding friends12_def d_defs by auto
from BC' have "Δ2 s' vl' ?s1' vl1' ∨ Δ3 s' vl' ?s1' vl1'"
proof (cases rule: BC.cases)
case (BC_FVal fs fs1)
then show ?thesis using vVS1 os' fIDs' f12s1 s's1' pFR1'
unfolding Δ2_def vl1' by auto
next
case (BC_BO vlr vlr1 fs fs1)
then have "Δ3 s' vl' ?s1' vl1'" using s's1' os' vVS1 f12s1 fIDs' pFR1'
unfolding vl1' by (intro Δ3_I[of _ _ _ _ _ fs fs1]) auto
then show ?thesis ..
qed
moreover have "open s1" "¬open ?s1'"
using ss1 os s's1' os' by (auto simp: eqButUID_open_eq)
moreover then have "φ ?trn1" unfolding CloseF by auto
ultimately show ?match using step1 vl1' CloseF UID1_UID2 UID1_UID2_UIDs
by (intro matchI[of s1 a outOK ?s1' vl1 vl1']) (auto simp: consume_def)
next
case (CloseA uid p uid' p')
let ?s1' = "createUser s1 uid p uid' p'"
let ?trn1 = "Trans s1 a outOK ?s1'"
have s': "s' = createUser s uid p uid' p'" using CloseA step by auto
have step1: "step s1 a = (outOK, ?s1')"
and pFR1': "pendingFReqs ?s1' = pendingFReqs s1"
using CloseA step ss1 unfolding eqButUID_def by (auto simp: c_defs)
have s's1': "eqButUID s' ?s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
moreover have os': "¬open s'" using CloseA os unfolding open_def by auto
moreover have fIDs': "friendIDs s' = friendIDs ?s1'"
using fIDs unfolding s' by (auto simp: c_defs)
moreover have f12s1: "friends12 s1 = friends12 ?s1'"
unfolding friends12_def by (auto simp: c_defs)
from BC' have "Δ2 s' vl' ?s1' vl1' ∨ Δ3 s' vl' ?s1' vl1'"
proof (cases rule: BC.cases)
case (BC_FVal fs fs1)
then show ?thesis using vVS1 os' fIDs' f12s1 s's1' pFR1'
unfolding Δ2_def vl1' by auto
next
case (BC_BO vlr vlr1 fs fs1)
then have "Δ3 s' vl' ?s1' vl1'" using s's1' os' vVS1 f12s1 fIDs' pFR1'
unfolding vl1' by (intro Δ3_I[of _ _ _ _ _ fs fs1]) auto
then show ?thesis ..
qed
moreover have "open s1" "¬open ?s1'"
using ss1 os s's1' os' by (auto simp: eqButUID_open_eq)
moreover then have "φ ?trn1" unfolding CloseA by auto
ultimately show ?match using step1 vl1' CloseA UID1_UID2 UID1_UID2_UIDs
by (intro matchI[of s1 a outOK ?s1' vl1 vl1']) (auto simp: consume_def)
qed auto
then show ?thesis ..
next
case (FRVal u req)
obtain p
where a: "(a = Cact (cFriendReq UID1 p UID2 req) ∧ UID1 ∈∈ pendingFReqs s' UID2 ∧
UID1 ∉ set (pendingFReqs s UID2) ∧
(UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1)) ∨
(a = Cact (cFriendReq UID2 p UID1 req) ∧ UID2 ∈∈ pendingFReqs s' UID1 ∧
UID2 ∉ set (pendingFReqs s UID1) ∧
(UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2))"
"ou = outOK" "¬friends12 s" "¬friends12 s'" "open s' = open s"
using φ step rs FRVal by (cases rule: φE) fastforce+
then have fIDs': "friendIDs s' = friendIDs s" using step by (auto simp: c_defs)
have "eqButUID s s'" using a step
by (auto intro: Cact_cFriendReq_step_eqButUID)
then have "Δ1 s' vl' s1 vl1"
unfolding Δ1_def using ss1 fIDs' fIDs os a(5) vVS1 IDs1 BO vl FRVal
by (auto intro: eqButUID_trans eqButUID_sym)
moreover from φ step rs a have "¬γ (Trans s a ou s')"
using UID1_UID2_UIDs by (cases rule: φE) auto
ultimately have ?ignore by (intro ignoreI) auto
then show ?thesis ..
qed
next
assume nφ: "¬φ ?trn"
then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
using step_open_φ[OF step] step_friends12_φ[OF step] by auto
have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
show ?thesis proof (cases "∀req. a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
a ≠ Cact (cFriendReq UID2 (pass s UID2) UID1 req) ∧
a ≠ Cact (cFriendReq UID1 (pass s UID1) UID2 req) ∧
a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
case True
obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
let ?trn1 = "Trans s1 a ou1 s1'"
have fIDs': "friendIDs s' = friendIDs s1'" using True
by (intro eqButUID_step_friendIDs_eq[OF ss1 rs rs1 step step1 _ fIDs]) auto
from True nφ have nφ': "¬φ ?trn1" using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
then have f12s1': "friends12 s1 = friends12 s1'"
and pFRs': "UID1 ∈∈ pendingFReqs s1 UID2 ⟷ UID1 ∈∈ pendingFReqs s1' UID2"
"UID2 ∈∈ pendingFReqs s1 UID1 ⟷ UID2 ∈∈ pendingFReqs s1' UID1"
using step_friends12_φ[OF step1] step_pendingFReqs_φ[OF step1]
by auto
have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
then have "Δ1 s' vl' s1' vl1" using os fIDs' vVS1 BO IDsOK_mono[OF step1 IDs1]
unfolding Δ1_def os' f12s1' pFRs' vl' by auto
then have ?match
using step1 nφ' fIDs eqButUID_step_γ_out[OF ss1 step step1]
by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
then show "?match ∨ ?ignore" ..
next
case False
with nφ have "ou ≠ outOK" by auto
then have "s' = s" using step False by auto
then have ?ignore using Δ1 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
then show "?match ∨ ?ignore" ..
qed
qed
qed
moreover have "vl = [] ⟶ vl1 = []" proof
assume "vl = []"
with BO have "filter (Not ∘ isFRVal) vl1 = []" using BO_Nil_iff[OF BO] by auto
with nFRVal1 show "vl1 = []" by (cases vl1; cases "hd vl1") auto
qed
ultimately show ?thesis by auto
qed
qed
lemma unwind_cont_Δ2: "unwind_cont Δ2 {Δ2, Δ1}"
proof(rule, simp)
let ?Δ = "λs vl s1 vl1. Δ2 s vl s1 vl1 ∨ Δ1 s vl s1 vl1"
fix s s1 :: state and vl vl1 :: "value list"
assume rsT: "reachNT s" and rs1: "reach s1" and 2: "Δ2 s vl s1 vl1"
from rsT have rs: "reach s" by (intro reachNT_reach)
from 2 obtain fs fs1
where ss1: "eqButUID s s1" and os: "¬open s"
and vVS1: "validValSeqFrom vl1 s1"
and fs: "filter (Not o isFRVal) vl = map FVal fs"
and fs1: "filter (Not o isFRVal) vl1 = map FVal fs1"
unfolding Δ2_def by auto
from os have IDs: "IDsOK s [UID1, UID2] [] [] []" unfolding open_defs by auto
then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []" using ss1 unfolding eqButUID_def by auto
show "iaction ?Δ s vl s1 vl1 ∨
((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
proof cases
assume vl1: "vl1 = []"
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'"
show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
proof cases
assume φ: "φ ?trn"
with c have vl: "vl = f ?trn # vl'" by (auto simp: consume_def)
with fs have ?ignore proof (cases "f ?trn")
case (FRVal u req)
obtain p
where a: "(a = Cact (cFriendReq UID1 p UID2 req) ∧ UID1 ∈∈ pendingFReqs s' UID2 ∧
UID1 ∉ set (pendingFReqs s UID2) ∧
(UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1)) ∨
(a = Cact (cFriendReq UID2 p UID1 req) ∧ UID2 ∈∈ pendingFReqs s' UID1 ∧
UID2 ∉ set (pendingFReqs s UID1) ∧
(UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2))"
"ou = outOK" "¬friends12 s" "¬friends12 s'" "open s' = open s"
using φ step rs FRVal by (cases rule: φE) fastforce+
then have fIDs': "friendIDs s' = friendIDs s" using step by (auto simp: c_defs)
have "eqButUID s s'" using a step
by (auto intro: Cact_cFriendReq_step_eqButUID)
then have "Δ2 s' vl' s1 vl1"
unfolding Δ2_def using ss1 os a(5) vVS1 vl fs fs1
by (auto intro: eqButUID_trans eqButUID_sym)
moreover from φ step rs a have "¬γ (Trans s a ou s')"
using UID1_UID2_UIDs by (cases rule: φE) auto
ultimately show ?ignore by (intro ignoreI) auto
next
case (FVal fv)
with fs vl obtain fs' where fs': "fs = fv # fs'" by (cases fs) auto
from φ step rs FVal have ss': "eqButUID s s'"
by (elim φE) (auto intro: Cact_cFriend_step_eqButUID Dact_dFriend_step_eqButUID)
then have "¬open s'" using os by (auto simp: eqButUID_open_eq)
moreover have "eqButUID s' s1" using ss1 ss' by (auto intro: eqButUID_sym eqButUID_trans)
ultimately have "Δ2 s' vl' s1 vl1"
using vVS1 fs' fs unfolding Δ2_def vl vl1 FVal by auto
moreover have "¬γ ?trn" using φ step rs FVal UID1_UID2_UIDs by (elim φE) auto
ultimately show ?ignore by (intro ignoreI) auto
qed auto
then show ?thesis ..
next
assume nφ: "¬φ ?trn"
then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
using step_open_φ[OF step] step_friends12_φ[OF step] by auto
have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
show ?thesis proof (cases "∀req. a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
a ≠ Cact (cFriendReq UID2 (pass s UID2) UID1 req) ∧
a ≠ Cact (cFriendReq UID1 (pass s UID1) UID2 req) ∧
a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
case True
obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
let ?trn1 = "Trans s1 a ou1 s1'"
from True nφ have nφ': "¬φ ?trn1"
using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
then have f12s1': "friends12 s1 = friends12 s1'"
and pFRs': "UID1 ∈∈ pendingFReqs s1 UID2 ⟷ UID1 ∈∈ pendingFReqs s1' UID2"
"UID2 ∈∈ pendingFReqs s1 UID1 ⟷ UID2 ∈∈ pendingFReqs s1' UID1"
using step_friends12_φ[OF step1] step_pendingFReqs_φ[OF step1]
by auto
have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
then have "Δ2 s' vl' s1' vl1" using os vVS1 fs fs1
unfolding Δ2_def os' f12s1' pFRs' vl' by auto
then have ?match
using step1 nφ' os eqButUID_step_γ_out[OF ss1 step step1]
by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
then show "?match ∨ ?ignore" ..
next
case False
with nφ have "ou ≠ outOK" by auto
then have "s' = s" using step False by auto
then have ?ignore using 2 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
then show "?match ∨ ?ignore" ..
qed
qed
qed
then show ?thesis using vl1 by auto
next
assume "vl1 ≠ []"
then obtain v vl1' where vl1: "vl1 = v # vl1'" by (cases vl1) auto
with fs1 have ?iact proof (cases v)
case (FRVal u req)
obtain a uid uid' s1' where step1: "step s1 a = (outOK, s1')" and "φ (Trans s1 a outOK s1')"
and a: "a = Cact (cFriendReq uid (pass s1 uid) uid' req)"
and uid: "uid = UID1 ∧ uid' = UID2 ∨ uid = UID2 ∧ uid' = UID1"
and "f (Trans s1 a outOK s1') = FRVal u req"
and vVS1': "validValSeqFrom vl1' s1'"
using rs1 IDs1 vVS1 UID1_UID2_UIDs unfolding vl1 FRVal by (blast intro: produce_FRVal)
moreover then have "¬γ (Trans s1 a outOK s1')" using UID1_UID2_UIDs by auto
moreover have "eqButUID s1 s1'" using step1 a uid
by (auto intro: Cact_cFriendReq_step_eqButUID)
moreover then have "Δ2 s vl s1' vl1'" using ss1 os vVS1' fs fs1 unfolding vl1 FRVal
by (intro Δ2_I[of s s1' vl1' vl fs fs1]) (auto intro: eqButUID_trans)
ultimately show "?iact" using ss1 os unfolding vl1 FRVal
by (intro iactionI[of s1 a "outOK" s1']) (auto simp: consume_def intro: eqButUID_trans)
next
case (FVal fv)
then obtain fs1' where fs1': "fs1 = fv # fs1'"
using vl1 fs1 by (cases fs1) auto
from FVal vVS1 vl1 have f12: "friends12 s1 ≠ fv"
and vVS1: "validValSeqFrom (FVal fv # vl1') s1" by auto
then show ?iact using rs1 IDs1 vl1 FVal ss1 os fs fs1 fs1' vl1 FVal
by (elim toggle_friends12[of s1 fv vl1'], blast, blast, blast)
(intro iactionI[of s1 _ _ _ vl1 vl1'],
auto simp: consume_def intro: Δ2_I[of s _ vl1' vl fs fs1'] eqButUID_trans)
qed auto
then show ?thesis ..
qed
qed
lemma unwind_cont_Δ3: "unwind_cont Δ3 {Δ3,Δ1}"
proof(rule, simp)
let ?Δ = "λs vl s1 vl1. Δ3 s vl s1 vl1 ∨ Δ1 s vl s1 vl1"
fix s s1 :: state and vl vl1 :: "value list"
assume rsT: "reachNT s" and rs1: "reach s1" and 3: "Δ3 s vl s1 vl1"
from rsT have rs: "reach s" by (intro reachNT_reach)
obtain fs fs1 vlr vlr1
where ss1: "eqButUID s s1" and os: "¬open s" and BO: "BO vlr vlr1"
and vVS1: "validValSeqFrom vl1 s1"
and fs: "filter (Not o isFRVal) vl = map FVal fs @ OVal True # vlr"
and fs1: "filter (Not o isFRVal) vl1 = map FVal fs1 @ OVal True # vlr1"
and fs_fs1: "fs = [] ⟷ fs1 = []"
and last_fs: "fs ≠ [] ⟶ last fs = last fs1"
and fs_fIDs: "fs = [] ⟶ friendIDs s = friendIDs s1"
using 3 unfolding Δ3_def by auto
have BC: "BC (map FVal fs @ OVal True # vlr) (map FVal fs1 @ OVal True # vlr1)"
using fs fs1 fs_fs1 last_fs BO by auto
from os have IDs: "IDsOK s [UID1, UID2] [] [] []" unfolding open_defs by auto
then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []" using ss1 unfolding eqButUID_def by auto
show "iaction ?Δ s vl s1 vl1 ∨
((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
proof cases
assume "∃u req vl1'. vl1 = FRVal u req # vl1'"
then obtain u req vl1' where vl1: "vl1 = FRVal u req # vl1'" by auto
obtain a uid uid' s1' where step1: "step s1 a = (outOK, s1')" and φ: "φ (Trans s1 a outOK s1')"
and a: "a = Cact (cFriendReq uid (pass s1 uid) uid' req)"
and uid: "uid = UID1 ∧ uid' = UID2 ∨ uid = UID2 ∧ uid' = UID1"
and f: "f (Trans s1 a outOK s1') = FRVal u req"
and "validValSeqFrom vl1' s1'"
using rs1 IDs1 vVS1 UID1_UID2_UIDs unfolding vl1 by (blast intro: produce_FRVal)
moreover have "eqButUID s1 s1'" using step1 a uid by (auto intro: Cact_cFriendReq_step_eqButUID)
moreover have "friendIDs s1' = friendIDs s1" and "IDsOK s1' [UID1, UID2] [] [] []"
using step1 a uid by (auto simp: c_defs)
ultimately have "Δ3 s vl s1' vl1'" using ss1 os BO fs_fs1 last_fs fs_fIDs fs fs1 unfolding vl1
by (intro Δ3_I[of _ _ vlr vlr1 vl1' fs fs1 vl])
(auto simp: consume_def intro: eqButUID_trans)
moreover have "¬γ (Trans s1 a outOK s1')" using a uid UID1_UID2_UIDs by auto
ultimately have "?iact" using step1 φ f unfolding vl1
by (intro iactionI[of s1 a "outOK" s1']) (auto simp: consume_def)
then show ?thesis ..
next
assume nFRVal1: "¬(∃u req vl1'. vl1 = FRVal u req # vl1')"
from BC show ?thesis proof (cases rule: BC_cases)
case (BO_FVal fv fv' fs' vl'' vl1'')
then have fs': "filter (Not o isFRVal) vl = map FVal (fv # fs' ## fv') @ OVal True # vl''"
and fs1': "filter (Not o isFRVal) vl1 = FVal fv' # OVal True # vl1''"
using fs fs1 by auto
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'"
show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
proof cases
assume φ: "φ ?trn"
with c have vl: "vl = f ?trn # vl'" by (auto simp: consume_def)
with fs' have ?ignore proof (cases "f ?trn")
case (FRVal u req)
obtain p
where a: "(a = Cact (cFriendReq UID1 p UID2 req) ∧ UID1 ∈∈ pendingFReqs s' UID2 ∧
UID1 ∉ set (pendingFReqs s UID2) ∧
(UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1)) ∨
(a = Cact (cFriendReq UID2 p UID1 req) ∧ UID2 ∈∈ pendingFReqs s' UID1 ∧
UID2 ∉ set (pendingFReqs s UID1) ∧
(UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2))"
"ou = outOK" "¬friends12 s" "¬friends12 s'" "open s' = open s"
using φ step rs FRVal by (cases rule: φE) fastforce+
then have fIDs': "friendIDs s' = friendIDs s" using step by (auto simp: c_defs)
have "eqButUID s s'" using a step
by (auto intro: Cact_cFriendReq_step_eqButUID)
then have "Δ3 s' vl' s1 vl1"
using ss1 a os BO vVS1 fs_fs1 last_fs fs_fIDs fs fs1 fIDs' vl FRVal
by (intro Δ3_I[of s' s1 vlr vlr1 vl1 fs fs1 vl'])
(auto intro: eqButUID_trans eqButUID_sym)
moreover from φ step rs a have "¬γ (Trans s a ou s')"
using UID1_UID2_UIDs by (cases rule: φE) auto
ultimately show ?ignore by (intro ignoreI) auto
next
case (FVal fv'')
with vl fs' have FVal: "f ?trn = FVal fv"
and vl': "filter (Not ∘ isFRVal) vl' = map FVal (fs' ## fv') @ OVal True # vl''"
by auto
from φ step rs FVal have ss': "eqButUID s s'"
by (elim φE) (auto intro: Cact_cFriend_step_eqButUID Dact_dFriend_step_eqButUID)
then have "¬open s'" using os by (auto simp: eqButUID_open_eq)
moreover have "eqButUID s' s1" using ss1 ss' by (auto intro: eqButUID_sym eqButUID_trans)
ultimately have "Δ3 s' vl' s1 vl1" using BO_FVal(3) vVS1 vl' fs1'
by (intro Δ3_I[of s' s1 vl'' vl1'' vl1 "fs' ## fv'" "[fv']" vl']) auto
moreover have "¬γ ?trn" using φ step rs FVal UID1_UID2_UIDs by (elim φE) auto
ultimately show ?ignore by (intro ignoreI) auto
qed auto
then show ?thesis ..
next
assume nφ: "¬φ ?trn"
then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
using step_open_φ[OF step] step_friends12_φ[OF step] by auto
have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
show ?thesis proof (cases "∀req. a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
a ≠ Cact (cFriendReq UID2 (pass s UID2) UID1 req) ∧
a ≠ Cact (cFriendReq UID1 (pass s UID1) UID2 req) ∧
a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
case True
obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
let ?trn1 = "Trans s1 a ou1 s1'"
from True nφ have nφ': "¬φ ?trn1"
using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
then have f12s1': "friends12 s1 = friends12 s1'"
and pFRs': "UID1 ∈∈ pendingFReqs s1 UID2 ⟷ UID1 ∈∈ pendingFReqs s1' UID2"
"UID2 ∈∈ pendingFReqs s1 UID1 ⟷ UID2 ∈∈ pendingFReqs s1' UID1"
using step_friends12_φ[OF step1] step_pendingFReqs_φ[OF step1]
by auto
have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
thm Δ3_I[of s' s1' vl'' vl1'' vl1 "fv # fs' ## fv'" "[fv']" vl']
then have "Δ3 s' vl' s1' vl1" using os vVS1 fs' fs1' BO_FVal
unfolding os' f12s1' pFRs' vl'
by (intro Δ3_I[of s' s1' vl'' vl1'' vl1 "fv # fs' ## fv'" "[fv']" vl]) auto
then have ?match
using step1 nφ' os eqButUID_step_γ_out[OF ss1 step step1]
by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
then show "?match ∨ ?ignore" ..
next
case False
with nφ have "ou ≠ outOK" by auto
then have "s' = s" using step False by auto
then have ?ignore using 3 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
then show "?match ∨ ?ignore" ..
qed
qed
qed
then show ?thesis using fs' by auto
next
case (BO_FVal1 fv fv' fs' fs1' vl'' vl1'')
then have fs': "filter (Not o isFRVal) vl = map FVal (fs' ## fv') @ OVal True # vl''"
and fs1': "filter (Not o isFRVal) vl1 = map FVal (fv # fs1' ## fv') @ OVal True # vl1''"
using fs fs1 by auto
with nFRVal1 obtain vl1'
where vl1: "vl1 = FVal fv # vl1'"
and vl1': "filter (Not o isFRVal) vl1' = map FVal (fs1' ## fv') @ OVal True # vl1''"
by (cases vl1; cases "hd vl1") auto
with vVS1 have f12: "friends12 s1 ≠ fv"
and vVS1: "validValSeqFrom (FVal fv # vl1') s1" by auto
then have ?iact using rs1 IDs1 vl1 ss1 os BO_FVal1(3) fs' vl1'
by (elim toggle_friends12[of s1 fv vl1'], blast, blast, blast)
(intro iactionI[of s1 _ _ _ vl1 vl1'],
auto simp: consume_def
intro: Δ3_I[of s _ vl'' vl1'' vl1' "fs' ## fv'" "fs1' ## fv'" vl]
eqButUID_trans)
then show ?thesis ..
next
case (FVal_BO fv vl'' vl1'')
then have fs': "filter (Not o isFRVal) vl = FVal fv # OVal True # vl''"
and fs1': "filter (Not o isFRVal) vl1 = FVal fv # OVal True # vl1''"
using fs fs1 by auto
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'"
show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
proof cases
assume φ: "φ ?trn"
with c have vl: "vl = f ?trn # vl'" by (auto simp: consume_def)
with fs' show ?thesis proof (cases "f ?trn")
case (FRVal u req)
obtain p
where a: "(a = Cact (cFriendReq UID1 p UID2 req) ∧ UID1 ∈∈ pendingFReqs s' UID2 ∧
UID1 ∉ set (pendingFReqs s UID2) ∧
(UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1)) ∨
(a = Cact (cFriendReq UID2 p UID1 req) ∧ UID2 ∈∈ pendingFReqs s' UID1 ∧
UID2 ∉ set (pendingFReqs s UID1) ∧
(UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2))"
"ou = outOK" "¬friends12 s" "¬friends12 s'" "open s' = open s"
using φ step rs FRVal by (cases rule: φE) fastforce+
then have fIDs': "friendIDs s' = friendIDs s" using step by (auto simp: c_defs)
have "eqButUID s s'" using a step
by (auto intro: Cact_cFriendReq_step_eqButUID)
then have "Δ3 s' vl' s1 vl1"
using ss1 a os BO vVS1 fs_fs1 last_fs fs_fIDs fs fs1 fIDs' vl FRVal
by (intro Δ3_I[of s' s1 vlr vlr1 vl1 fs fs1 vl'])
(auto intro: eqButUID_trans eqButUID_sym)
moreover from φ step rs a have "¬γ (Trans s a ou s')"
using UID1_UID2_UIDs by (cases rule: φE) auto
ultimately have ?ignore by (intro ignoreI) auto
then show ?thesis ..
next
case (FVal fv'')
with vl fs' have FVal: "f ?trn = FVal fv"
and vl': "filter (Not ∘ isFRVal) vl' = OVal True # vl''"
by auto
from fs1' nFRVal1 obtain vl1'
where vl1: "vl1 = FVal fv # vl1'"
and vl1': "filter (Not ∘ isFRVal) vl1' = OVal True # vl1''"
by (cases vl1; cases "hd vl1") auto
have ?match using φ step rs FVal proof (cases rule: φE)
case (Friend uid p uid')
then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
and f12s1: "¬friends12 s1"
and fv: "fv = True"
using ss1 vVS1 FVal unfolding eqButUID_def vl1 by auto
let ?s1' = "createFriend s1 UID1 (pass s1 UID1) UID2"
have s': "s' = createFriend s UID1 p UID2"
using Friend step by (auto simp: createFriend_sym)
have ss': "eqButUID s s'" using rs step Friend
by (auto intro: Cact_cFriend_step_eqButUID)
moreover then have os': "¬open s'" using os eqButUID_open_eq by auto
moreover obtain a1 uid1 uid1' p1
where "step s1 a1 = (outOK, ?s1')" "friends12 ?s1'"
"a1 = Cact (cFriend uid1 p1 uid1')"
"uid1 = UID1 ∧ uid1' = UID2 ∨ uid1 = UID2 ∧ uid1' = UID1"
"φ (Trans s1 a1 outOK ?s1')"
"f (Trans s1 a1 outOK ?s1') = FVal True"
"eqButUID s1 ?s1'" "validValSeqFrom vl1' ?s1'"
using rs1 IDs1 Friend vVS1 f12s1 unfolding vl1 FVal
by (elim toggle_friends12_True; blast)
moreover then have "IDsOK ?s1' [UID1, UID2] [] [] []" by (auto simp: c_defs)
moreover have "friendIDs s' = friendIDs ?s1'"
using Friend(6) f12s1 unfolding s'
by (intro eqButUID_createFriend12_friendIDs_eq[OF ss1 rs rs1]) auto
ultimately show ?match
using ss1 FVal_BO Friend UID1_UID2_UIDs vl' vl1' unfolding vl1 fv
by (intro matchI[of s1 a1 "outOK" ?s1'])
(auto simp: consume_def intro: eqButUID_trans eqButUID_sym
intro!: Δ3_I[of s' ?s1' vl'' vl1'' vl1' "[]" "[]" vl'])
next
case (Unfriend uid p uid')
then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
and f12s1: "friends12 s1"
and fv: "fv = False"
using ss1 vVS1 FVal unfolding eqButUID_def vl1 by auto
let ?s1' = "deleteFriend s1 UID1 (pass s1 UID1) UID2"
have s': "s' = deleteFriend s UID1 p UID2"
using Unfriend step by (auto simp: deleteFriend_sym)
have ss': "eqButUID s s'" using rs step Unfriend
by (auto intro: Dact_dFriend_step_eqButUID)
moreover then have os': "¬open s'" using os eqButUID_open_eq by auto
moreover obtain a1 uid1 uid1' p1
where "step s1 a1 = (outOK, ?s1')" "¬friends12 ?s1'"
"a1 = Dact (dFriend uid1 p1 uid1')"
"uid1 = UID1 ∧ uid1' = UID2 ∨ uid1 = UID2 ∧ uid1' = UID1"
"φ (Trans s1 a1 outOK ?s1')"
"f (Trans s1 a1 outOK ?s1') = FVal False"
"eqButUID s1 ?s1'" "validValSeqFrom vl1' ?s1'"
using rs1 IDs1 Unfriend vVS1 f12s1 unfolding vl1 FVal
by (elim toggle_friends12_False; blast)
moreover then have "IDsOK ?s1' [UID1, UID2] [] [] []" by (auto simp: d_defs)
moreover have "friendIDs s' = friendIDs ?s1'"
using Unfriend(6) f12s1 unfolding s'
by (intro eqButUID_deleteFriend12_friendIDs_eq[OF ss1 rs rs1])
ultimately show ?match
using ss1 FVal_BO Unfriend UID1_UID2_UIDs vl' vl1' unfolding vl1 fv
by (intro matchI[of s1 a1 "outOK" ?s1'])
(auto simp: consume_def intro: eqButUID_trans eqButUID_sym
intro!: Δ3_I[of s' ?s1' vl'' vl1'' vl1' "[]" "[]" vl'])
qed auto
then show ?thesis ..
qed auto
next
assume nφ: "¬φ ?trn"
then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
using step_open_φ[OF step] step_friends12_φ[OF step] by auto
have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
show ?thesis proof (cases "∀req. a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
a ≠ Cact (cFriendReq UID2 (pass s UID2) UID1 req) ∧
a ≠ Cact (cFriendReq UID1 (pass s UID1) UID2 req) ∧
a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
case True
obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
let ?trn1 = "Trans s1 a ou1 s1'"
from True nφ have nφ': "¬φ ?trn1"
using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
then have f12s1': "friends12 s1 = friends12 s1'"
and pFRs': "UID1 ∈∈ pendingFReqs s1 UID2 ⟷ UID1 ∈∈ pendingFReqs s1' UID2"
"UID2 ∈∈ pendingFReqs s1 UID1 ⟷ UID2 ∈∈ pendingFReqs s1' UID1"
using step_friends12_φ[OF step1] step_pendingFReqs_φ[OF step1]
by auto
have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
thm Δ3_I[of s' s1' vl'' vl1'' vl1 "[fv]" "[fv]" vl']
then have "Δ3 s' vl' s1' vl1" using os vVS1 fs' fs1' FVal_BO
unfolding os' f12s1' pFRs' vl'
by (intro Δ3_I[of s' s1' vl'' vl1'' vl1 "[fv]" "[fv]" vl]) auto
then have ?match
using step1 nφ' os eqButUID_step_γ_out[OF ss1 step step1]
by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
then show "?match ∨ ?ignore" ..
next
case False
with nφ have "ou ≠ outOK" by auto
then have "s' = s" using step False by auto
then have ?ignore using 3 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
then show "?match ∨ ?ignore" ..
qed
qed
qed
then show ?thesis using fs' by auto
next
case (OVal vl'' vl1'')
then have fs': "filter (Not o isFRVal) vl = OVal True # vl''"
and fs1': "filter (Not o isFRVal) vl1 = OVal True # vl1''"
and BO'': "BO vl'' vl1''"
using fs fs1 by auto
from fs fs' have fs: "fs = []" by (cases fs) auto
with fs_fIDs have fIDs: "friendIDs s = friendIDs s1" by auto
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'"
show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
proof cases
assume φ: "φ ?trn"
with c have vl: "vl = f ?trn # vl'" by (auto simp: consume_def)
with fs' show ?thesis proof (cases "f ?trn")
case (FRVal u req)
obtain p
where a: "(a = Cact (cFriendReq UID1 p UID2 req) ∧ UID1 ∈∈ pendingFReqs s' UID2 ∧
UID1 ∉ set (pendingFReqs s UID2) ∧
(UID2 ∈∈ pendingFReqs s' UID1 ⟷ UID2 ∈∈ pendingFReqs s UID1)) ∨
(a = Cact (cFriendReq UID2 p UID1 req) ∧ UID2 ∈∈ pendingFReqs s' UID1 ∧
UID2 ∉ set (pendingFReqs s UID1) ∧
(UID1 ∈∈ pendingFReqs s' UID2 ⟷ UID1 ∈∈ pendingFReqs s UID2))"
"ou = outOK" "¬friends12 s" "¬friends12 s'" "open s' = open s"
using φ step rs FRVal by (cases rule: φE) fastforce+
then have fIDs': "friendIDs s' = friendIDs s" using step by (auto simp: c_defs)
have "eqButUID s s'" using a step
by (auto intro: Cact_cFriendReq_step_eqButUID)
then have "Δ3 s' vl' s1 vl1"
using ss1 a os OVal(3) vVS1 fs' fs1' fs fs_fs1 fIDs' fIDs unfolding vl FRVal
by (intro Δ3_I[of s' s1 vl'' vl1'' vl1 fs fs1 vl'])
(auto intro: eqButUID_trans eqButUID_sym)
moreover from φ step rs a have "¬γ (Trans s a ou s')"
using UID1_UID2_UIDs by (cases rule: φE) auto
ultimately have ?ignore by (intro ignoreI) auto
then show ?thesis ..
next
case (OVal ov')
with vl fs' have OVal: "f ?trn = OVal True"
and vl': "filter (Not ∘ isFRVal) vl' = vl''"
by auto
from fs1' nFRVal1 obtain vl1'
where vl1: "vl1 = OVal True # vl1'"
and vl1': "filter (Not ∘ isFRVal) vl1' = vl1''"
by (cases vl1; cases "hd vl1") auto
have ?match using φ step rs OVal proof (cases rule: φE)
case (OpenF uid p uid')
let ?s1' = "createFriend s1 uid p uid'"
have s': "s' = createFriend s uid p uid'"
using OpenF step by auto
from OpenF(2) have uids: "uid ≠ UID1 ∧ uid ≠ UID2 ∧ uid' = UID1 ∨
uid ≠ UID1 ∧ uid ≠ UID2 ∧ uid' = UID2 ∨
uid' ≠ UID1 ∧ uid' ≠ UID2 ∧ uid = UID1 ∨
uid' ≠ UID1 ∧ uid' ≠ UID2 ∧ uid = UID2"
using UID1_UID2_UIDs by auto
have "eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
using ss1 unfolding eqButUID_def by auto
then have "uid' ∈∈ pendingFReqs s uid ⟷ uid' ∈∈ pendingFReqs s1 uid"
using OpenF by (intro eqButUIDf_not_UID') auto
then have step1: "step s1 a = (outOK, ?s1')"
using OpenF step ss1 fIDs unfolding eqButUID_def by (auto simp: c_defs)
have s's1': "eqButUID s' ?s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
moreover have os': "open s'" using OpenF unfolding open_def by auto
moreover have fIDs': "friendIDs s' = friendIDs ?s1'"
using fIDs unfolding s' by (auto simp: c_defs)
moreover have f12s1: "friends12 s1 = friends12 ?s1'"
"UID1 ∈∈ pendingFReqs s1 UID2 ⟷ UID1 ∈∈ pendingFReqs ?s1' UID2"
"UID2 ∈∈ pendingFReqs s1 UID1 ⟷ UID2 ∈∈ pendingFReqs ?s1' UID1"
using uids unfolding friends12_def c_defs by auto
moreover then have "validValSeqFrom vl1' ?s1'" using vVS1 unfolding vl1 by auto
ultimately have "Δ1 s' vl' ?s1' vl1'"
using BO'' IDsOK_mono[OF step1 IDs1] unfolding Δ1_def vl' vl1' by auto
moreover have "φ ?trn ⟷ φ (Trans s1 a outOK ?s1')"
using OpenF(1) uids by (intro eqButUID_step_φ[OF ss1 rs rs1 step step1]) auto
ultimately show ?match using step1 φ OpenF(1,3,4) unfolding vl1
by (intro matchI[of s1 a outOK ?s1' _ vl1']) (auto simp: consume_def)
qed auto
then show ?thesis ..
qed auto
next
assume nφ: "¬φ ?trn"
then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
using step_open_φ[OF step] step_friends12_φ[OF step] by auto
have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
show ?thesis proof (cases "∀req. a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
a ≠ Cact (cFriendReq UID2 (pass s UID2) UID1 req) ∧
a ≠ Cact (cFriendReq UID1 (pass s UID1) UID2 req) ∧
a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
case True
obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
let ?trn1 = "Trans s1 a ou1 s1'"
from True nφ have nφ': "¬φ ?trn1"
using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
then have f12s1': "friends12 s1 = friends12 s1'"
and pFRs': "UID1 ∈∈ pendingFReqs s1 UID2 ⟷ UID1 ∈∈ pendingFReqs s1' UID2"
"UID2 ∈∈ pendingFReqs s1 UID1 ⟷ UID2 ∈∈ pendingFReqs s1' UID1"
using step_friends12_φ[OF step1] step_pendingFReqs_φ[OF step1]
by auto
have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
moreover have "friendIDs s' = friendIDs s1'"
using eqButUID_step_friendIDs_eq[OF ss1 rs rs1 step step1 _ fIDs] True
by auto
ultimately have "Δ3 s' vl' s1' vl1" using os vVS1 fs' fs1' OVal
unfolding os' f12s1' pFRs' vl'
by (intro Δ3_I[of s' s1' vl'' vl1'' vl1 "[]" "[]" vl]) auto
then have ?match
using step1 nφ' os eqButUID_step_γ_out[OF ss1 step step1]
by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
then show "?match ∨ ?ignore" ..
next
case False
with nφ have "ou ≠ outOK" by auto
then have "s' = s" using step False by auto
then have ?ignore using 3 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
then show "?match ∨ ?ignore" ..
qed
qed
qed
then show ?thesis using fs' by auto
next
case (FVal1 fv fs' fs1')
from this(1) have "False" proof (induction fs' arbitrary: fs)
case (Cons fv'' fs'')
then obtain fs''' where "map FVal (fv'' # fs''') @ OVal True # vlr = map FVal (fv'' # fs'')"
by (cases fs) auto
with Cons.IH[of fs'''] show "False" by auto
qed auto
then show ?thesis ..
next
case (FVal) then show ?thesis by (induction fs) auto next
case (Nil) then show ?thesis by auto
qed
qed
qed
definition Gr where
"Gr =
{
(Δ0, {Δ0,Δ1,Δ2,Δ3}),
(Δ1, {Δ1,Δ2,Δ3}),
(Δ2, {Δ2,Δ1}),
(Δ3, {Δ3,Δ1})
}"
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_Δ2 unwind_cont_Δ3
unfolding Gr_def by (auto intro: unwind_cont_mono)
end
end