Quelle  Swap.thy

section ‹Swap lemmas›

text ‹›

theory Swap
  imports
    Distributed_System

begin

context distributed_system

begin

lemma swap_msgs_Trans_Trans:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isTrans ev" and
    "isTrans ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain u u' where "ev = Trans ?p u u'" 
    by (metis assms(3) event.collapse(1))
  obtain u'' u''' where "ev' = Trans ?q u'' u'''" 
    by (metis assms(4) event.collapse(1))
  then have "msgs d' i = msgs d i" 
    by (metis Trans_msg assms(1) assms(3) assms(4) assms(5))
  then have "msgs e i = msgs e' i" 
    using Trans_msg assms(2) assms(3) assms(4) assms(6) by auto
  then show ?thesis by blast
qed

lemma swap_msgs_Send_Send:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSend ev" and
    "isSend ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Send_ev: "ev = Send i' ?p r u u' m" 
    by (metis assms(3) event.collapse(2))
  obtain i'' s u'' u''' m' where Send_ev': "ev' = Send i'' ?q s u'' u''' m'" 
    by (metis assms(4) event.collapse(2))
  have "i' ≠ i''"
    by (metis (mono_tags, lifting) ‹ev = Send i' (occurs_on ev) r u u' m› ‹ev' = Send i'' (occurs_on ev') s u'' u''' m'› assms(1) assms(2) assms(7) can_occur_def event.simps(27) happen_implies_can_occur option.simps(1) prod.simps(1))
  then show ?thesis
  proof (cases "i = i' ∨ i = i''")
    case True
    then show ?thesis
    proof (elim disjE)
      assume "i = i'"
      then have "msgs d i = msgs c i @ [Msg m]" 
        by (metis ‹ev = Send i' (occurs_on ev) r u u' m› assms(1) next_send)
      moreover have "msgs e i = msgs d i" 
        by (metis ‹ev' = Send i'' (occurs_on ev') s u'' u''' m'› ‹i = i'› ‹i' ≠ i''› assms(2) assms(4) event.sel(8) msgs_unchanged_for_other_is regular_event)
      moreover have "msgs d' i = msgs c i" 
        by (metis ‹ev' = Send i'' (occurs_on ev') s u'' u''' m'› ‹i = i'› ‹i' ≠ i''› assms(4) assms(5) event.sel(8) msgs_unchanged_for_other_is regular_event)
      moreover have "msgs e' i = msgs d' i @ [Msg m]" 
        by (metis ‹ev = Send i' (occurs_on ev) r u u' m› ‹i = i'› assms(6) next_send)
      ultimately show ?thesis by simp
    next
      assume "i = i''"
      then have "msgs d i = msgs c i" 
        by (metis Send_ev ‹i' ≠ i''› assms(1) assms(3) event.sel(8) msgs_unchanged_for_other_is regular_event)
      moreover have "msgs e i = msgs d i @ [Msg m']" 
        by (metis Send_ev' ‹i = i''› assms(2) next_send)
      moreover have "msgs d' i = msgs c i @ [Msg m']" 
        by (metis Send_ev' ‹i = i''› assms(5) next_send)
      moreover have "msgs e' i = msgs d' i" 
        by (metis Send_ev ‹i = i''› ‹i' ≠ i''› assms(3) assms(6) event.sel(8) msgs_unchanged_for_other_is regular_event)
      ultimately show ?thesis by simp
    qed
  next
    case False
    then have "msgs e i = msgs d i" using Send_ev' assms 
      by (metis event.sel(8) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs c i" 
      by (metis False Send_ev assms(1) assms(3) event.sel(8) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs d' i" 
      by (metis (no_types, opaque_lifting) ‹msgs d i = msgs c i› assms(2) assms(4) assms(5) calculation regular_event same_messages_imply_same_resulting_messages)
    also have "... = msgs e' i" 
      by (metis (no_types, opaque_lifting) ‹msgs c i = msgs d' i› ‹msgs d i = msgs c i› assms(1) assms(3) assms(6) regular_event same_messages_imply_same_resulting_messages)
    finally show ?thesis by simp
  qed
qed

lemma swap_msgs_Recv_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Recv_ev: "ev = Recv i' ?p r u u' m" 
    by (metis assms(3) event.collapse(3))
  obtain i'' s u'' u''' m' where Recv_ev': "ev' = Recv i'' ?q s u'' u''' m'" 
    by (metis assms(4) event.collapse(3))
  have "i' ≠ i''" 
    by (metis Recv_ev Recv_ev' assms(1) assms(2) assms(7) can_occur_Recv happen_implies_can_occur option.simps(1) prod.simps(1))
  show ?thesis
  proof (cases "i = i' ∨ i = i''")
    case True
    then show ?thesis
    proof (elim disjE)
      assume "i = i'"
      then have "Msg m # msgs d i = msgs c i" using Recv_ev assms by (metis next_recv)
      moreover have "msgs e i = msgs d i" 
        by (metis Recv_ev' ‹i = i'› ‹i' ≠ i''› assms(2) assms(4) event.sel(9) msgs_unchanged_for_other_is regular_event)
      moreover have "msgs d' i = msgs c i" 
        by (metis Recv_ev' ‹i = i'› ‹i' ≠ i''› assms(4) assms(5) event.sel(9) msgs_unchanged_for_other_is regular_event)
      moreover have "Msg m # msgs e' i = msgs d' i" 
        by (metis Recv_ev ‹i = i'› assms(6) next_recv)
      ultimately show ?thesis by (metis list.inject)
    next
      assume "i = i''"
      then have "msgs d i = msgs c i" 
        by (metis Recv_ev ‹i' ≠ i''› assms(1) assms(3) event.sel(9) msgs_unchanged_for_other_is regular_event)
      moreover have "Msg m' # msgs e i = msgs d i" 
        by (metis Recv_ev' ‹i = i''› assms(2) next_recv)
      moreover have "Msg m' # msgs d' i = msgs c i" 
        by (metis Recv_ev' ‹i = i''› assms(5) next_recv)
      moreover have "msgs e' i = msgs d' i" 
        by (metis Recv_ev ‹i = i''› ‹i' ≠ i''› assms(3) assms(6) event.sel(9) msgs_unchanged_for_other_is regular_event)
      ultimately show ?thesis by (metis list.inject)
    qed
  next
    case False
    then have "msgs e i = msgs d i" 
      by (metis Recv_ev' assms(2) assms(4) event.sel(9) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs c i" 
      by (metis False Recv_ev assms(1) assms(3) event.sel(9) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs d' i" 
      by (metis (no_types, opaque_lifting) ‹msgs d i = msgs c i› assms(2) assms(4) assms(5) calculation regular_event same_messages_imply_same_resulting_messages)
    also have "... = msgs e' i" 
      by (metis (no_types, lifting) ‹msgs c i = msgs d' i› ‹msgs d i = msgs c i› assms(1) assms(3) assms(6) regular_event same_messages_imply_same_resulting_messages)
    finally show ?thesis by simp
  qed
qed

lemma swap_msgs_Send_Trans:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSend ev" and
    "isTrans ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Send: "ev = Send i' ?p r u u' m" 
    by (metis assms(3) event.collapse(2))
  obtain u'' u''' where Trans: "ev' = Trans ?q u'' u'''" 
    by (metis assms(4) event.collapse(1))
  show ?thesis
  proof (cases "i = i'")
    case True
    then have "msgs d i = msgs c i @ [Msg m]" 
      by (metis Send assms(1) next_send)
    moreover have "msgs e i = msgs d i"
      using Trans_msg assms(2) assms(4) by auto
    moreover have "msgs d' i = msgs c i" 
      using Trans_msg assms(4) assms(5) by auto
    moreover have "msgs e' i = msgs d' i @ [Msg m]" 
      by (metis Send True assms(6) next_send)
    ultimately show ?thesis by simp 
  next
    case False
    then have "msgs e i = msgs d i" 
      using Trans_msg assms(2) assms(4) by auto
    also have "... = msgs c i" 
      by (metis False Send assms(1) assms(3) event.sel(8) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs d' i" 
      using Trans_msg assms(4) assms(5) by blast
    also have "... = msgs e' i" 
      by (metis (no_types, lifting) ‹msgs c i = msgs d' i› ‹msgs d i = msgs c i› assms(1) assms(3) assms(6) regular_event same_messages_imply_same_resulting_messages)
    finally show ?thesis by simp
  qed
qed

lemma swap_msgs_Trans_Send:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isTrans ev" and
    "isSend ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_msgs_Send_Trans by auto

lemma swap_msgs_Recv_Trans:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isTrans ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Recv: "ev = Recv i' ?p r u u' m" 
    by (metis assms(3) event.collapse(3))
  obtain u'' u''' where Trans: "ev' = Trans ?q u'' u'''" 
    by (metis assms(4) event.collapse(1))
  show ?thesis
  proof (cases "i = i'")
    case True
    then have "Msg m # msgs d i = msgs c i" 
      by (metis Recv assms(1) next_recv)
    moreover have "msgs e i = msgs d i" 
      using Trans_msg assms(2) assms(4) by auto
    moreover have "msgs d' i = msgs c i" 
      using Trans_msg assms(4) assms(5) by auto
    moreover have "Msg m # msgs e' i = msgs d' i" 
      by (metis Recv True assms(6) next_recv)
    ultimately show ?thesis by (metis list.inject) 
  next
    case False
    then have "msgs e i = msgs d i" 
      using Trans_msg assms(2) assms(4) by auto
    also have "... = msgs c i" 
      by (metis False Recv assms(1) assms(3) event.sel(9) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs d' i" 
      using Trans_msg assms(4) assms(5) by blast
    also have "... = msgs e' i" 
      by (metis False Recv assms(6) next_recv)
    finally show ?thesis by simp
  qed
qed

lemma swap_msgs_Trans_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isTrans ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_msgs_Recv_Trans by auto

lemma swap_msgs_Send_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSend ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Send: "ev = Send i' ?p r u u' m" 
    by (metis assms(3) event.collapse(2))
  obtain i'' s u'' u''' m' where Recv: "ev' = Recv i'' ?q s u'' u''' m'" 
    by (metis assms(4) event.collapse(3))
  show ?thesis
  proof (cases "i = i'"; cases "i = i''", goal_cases)
    case 1
    then have "msgs e' i = msgs d' i @ [Msg m]" 
      by (metis Send assms(6) next_send)
    moreover have "Msg m' # msgs d' i = msgs c i" 
      by (metis "1"(2) Recv assms(5) next_recv)
    moreover have "msgs d i = msgs c i @ [Msg m]" 
      by (metis "1"(1) Send assms(1) next_send)
    moreover have "Msg m' # msgs e i = msgs d i" 
      by (metis "1"(2) Recv assms(2) next_recv)
    ultimately show ?thesis 
      by (metis list.sel(2) list.sel(3) not_Cons_self2 tl_append2)
  next
    case 2
    then have "msgs d i = msgs c i @ [Msg m]" 
      by (metis Send assms(1) next_send)
    moreover have "msgs e i = msgs d i" 
      by (metis "2"(2) Recv assms(2) assms(4) event.sel(9) msgs_unchanged_for_other_is regular_event)
    moreover have "msgs d' i = msgs c i" 
      by (metis "2"(2) Recv assms(4) assms(5) event.sel(9) msgs_unchanged_for_other_is regular_event)
    moreover have "msgs e' i = msgs d' i @ [Msg m]" 
      by (metis Send 2(1) assms(6) next_send)
    ultimately show ?thesis by simp 
  next
    assume 3: "i ≠ i'" "i = i''"
    then have "msgs d i = msgs c i" 
      by (metis Send assms(1) assms(3) event.sel(8) msgs_unchanged_for_other_is regular_event)
    moreover have "Msg m' # msgs e i = msgs d i" using 3 Recv assms by (metis next_recv)
    moreover have "Msg m' # msgs d' i = msgs c i" 
      by (metis "3"(2) Recv assms(5) next_recv)
    moreover have "msgs e' i = msgs d' i" 
      by (metis "3"(1) Send assms(6) next_send)
    ultimately show ?thesis by (metis list.inject)
  next
    assume 4: "i ≠ i'" "i ≠ i''"
    then have "msgs e i = msgs d i" 
      by (metis Recv assms(2) assms(4) event.sel(9) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs c i" 
      by (metis "4"(1) Send assms(1) assms(3) event.sel(8) msgs_unchanged_for_other_is regular_event)
    also have "... = msgs d' i" 
      by (metis "4"(2) Recv assms(5) next_recv)
    also have "... = msgs e' i" 
      by (metis "4"(1) Send assms(6) next_send)
    finally show ?thesis by simp
  qed
qed

lemma swap_msgs_Recv_Send:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isSend ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_msgs_Send_Recv by auto

lemma same_cs_implies_same_resulting_cs:
  assumes
    "cs c i = cs d i"
    "c ⊨ ev ↦ c'" and
    "d ⊨ ev ↦ d'" and
    "regular_event ev"
  shows
    "cs c' i = cs d' i"
proof -
  have "isTrans ev ∨ isSend ev ∨ isRecv ev" using assms by simp
  then show ?thesis
  proof (elim disjE)
    assume "isTrans ev"
    then show ?thesis 
      by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) event.distinct_disc(4) no_cs_change_if_no_event)
  next
    assume "isSend ev"
    then show ?thesis 
      by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) event.distinct_disc(10) no_cs_change_if_no_event)
  next
    assume "isRecv ev"
    then obtain i' r s u u' m where Recv: "ev = Recv i' r s u u' m" 
      by (meson isRecv_def)
    then show ?thesis
    proof (cases "i' = i")
      case True
      with assms Recv show ?thesis by (cases "snd (cs c i) = Recording", auto)
    next
      case False
      then show ?thesis using assms Recv by simp
    qed
  qed
qed

lemma regular_event_implies_same_channel_snapshot_Recv_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "cs e i = cs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Recv_ev: "ev = Recv i' ?p r u u' m" 
    by (metis assms(3) event.collapse(3))
  obtain i'' s u'' u''' m' where Recv_ev': "ev' = Recv i'' ?q s u'' u''' m'" 
    by (metis assms(4) event.collapse(3))
  have "i' ≠ i''" 
    by (metis Recv_ev Recv_ev' assms(1) assms(5) assms(7) can_occur_Recv happen_implies_can_occur option.simps(1) prod.simps(1))
  show ?thesis
  proof (cases "i = i' ∨ i = i''")
    case True
    then show ?thesis
    proof (elim disjE)
      assume "i = i'"
      then have "cs d' i = cs c i" 
        using assms(4) assms(5) assms(7) no_cs_change_if_no_event
        by (metis Recv_ev' ‹i' ≠ i''› event.sel(9) regular_event)
      then have "cs e' i = cs d i" 
        using assms(1) assms(3) assms(6) distributed_system.same_cs_implies_same_resulting_cs distributed_system_axioms regular_event by blast
      then have "cs d i = cs e i" 
        by (metis Recv_ev' ‹i = i'› ‹i' ≠ i''› assms(2) assms(4) event.sel(9) no_cs_change_if_no_event regular_event)
      then show ?thesis
        by (simp add: ‹cs e' i = cs d i›)
    next
      assume "i = i''"
      then have "cs d i = cs c i" 
        by (metis Recv_ev ‹i' ≠ i''› assms(1) assms(3) event.sel(9) no_cs_change_if_no_event regular_event)
      then have "cs e i = cs d' i"
        using assms(2) assms(4) assms(5) regular_event same_cs_implies_same_resulting_cs by blast
      then have "cs d' i = cs e' i" 
        by (metis Recv_ev ‹i = i''› ‹i' ≠ i''› assms(3) assms(6) event.sel(9) no_cs_change_if_no_event regular_event)
      then show ?thesis 
        by (simp add: ‹cs e i = cs d' i›)
    qed
  next
    case False
    then show ?thesis 
      by (metis Recv_ev Recv_ev' assms(1) assms(2) assms(5) assms(6) next_recv)
  qed
qed

lemma regular_event_implies_same_channel_snapshot_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "~ isRecv ev" and
    "regular_event ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "cs e i = cs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' s u'' u''' m' where Recv: "ev' = Recv i' ?q s u'' u''' m'" 
    by (metis assms(5) event.collapse(3))
  show ?thesis
  proof (cases "i = i'")
    case True
    then have "cs d i = cs c i" 
      using assms(1) assms(3) assms(7) no_cs_change_if_no_event ‹regular_event ev› ‹~ isRecv ev› by auto
    then have "cs e i = cs d' i"
      using assms(2) assms(5) assms(6) regular_event same_cs_implies_same_resulting_cs by blast
    then have "cs d' i = cs e' i" 
      using True assms(3) assms(6) assms(7) no_cs_change_if_no_event ‹regular_event ev› ‹~ isRecv ev› by auto
    then show ?thesis 
      by (simp add: ‹cs e i = cs d' i›)
  next
    case False
    then have "cs d i = cs c i" 
      using assms(1) assms(3) assms(4) no_cs_change_if_no_event by auto
    then have "cs d' i = cs e i" 
      by (metis (no_types, lifting) assms(2) assms(5) assms(6) regular_event same_cs_implies_same_resulting_cs)
    then show "cs e i = cs e' i" 
      using assms(3) assms(4) assms(7) no_cs_change_if_no_event by auto 
  qed
qed

lemma same_messages_2:
  assumes
    "∀p. has_snapshotted c p = has_snapshotted d p" and
    "msgs c i = msgs d i" and
    "c ⊨ ev ↦ c'" and
    "d ⊨ ev ↦ d'" and
    "~ regular_event ev"
  shows
    "msgs c' i = msgs d' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    using assms(2) assms(3) assms(4) no_msgs_change_if_no_channel by auto
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  have "isSnapshot ev ∨ isRecvMarker ev"
    using assms(5) event.exhaust_disc by auto
  then show ?thesis
  proof (elim disjE)
    assume "isSnapshot ev"
    then obtain r where Snapshot: "ev = Snapshot r" by (meson isSnapshot_def)
    then show ?thesis
    proof (cases "r = p")
      case True
      then have "msgs c' i = msgs c i @ [Marker]" using chan Snapshot assms by simp
      moreover have "msgs d' i = msgs d i @ [Marker]" using chan Snapshot assms True by simp
      ultimately show ?thesis using assms by simp
    next
      case False
      then have "msgs c' i = msgs c i" using chan Snapshot assms by simp
      moreover have "msgs d' i = msgs d i" using chan Snapshot assms False by simp
      ultimately show ?thesis using assms by simp
    qed
  next
    assume "isRecvMarker ev"
    then obtain i' r s where RecvMarker: "ev = RecvMarker i' r s"
      by (meson isRecvMarker_def)
    then show ?thesis
    proof (cases "has_snapshotted c r")
      case snap: True
      then show ?thesis
      proof (cases "i = i'")
        case True
        then have "Marker # msgs c' i = msgs c i" using chan RecvMarker assms snap by simp
        moreover have "Marker # msgs d' i = msgs d i" using chan RecvMarker assms snap True by simp
        ultimately show ?thesis using assms by (metis list.inject)
      next
        case False
        then have "msgs d' i = msgs d i" 
          using RecvMarker assms(1) assms(4) snap by auto
        also have "... = msgs c i" using assms by simp
        also have "... = msgs c' i" 
          using False RecvMarker snap assms by auto
        finally show ?thesis using snap by simp
      qed
    next
      case no_snap: False
      then show ?thesis
      proof (cases "i = i'")
        case True
        then have "Marker # msgs c' i = msgs c i" using chan RecvMarker assms by simp
        moreover have "Marker # msgs d' i = msgs d i" using chan RecvMarker assms True by simp
        ultimately show ?thesis using assms by (metis list.inject)
      next
        case not_i: False
        then show ?thesis
        proof (cases "r = p")
          case True
          then have "msgs c' i = msgs c i @ [Marker]"
            using no_snap RecvMarker assms True chan not_i by auto
          moreover have "msgs d' i = msgs d i @ [Marker]"
          proof -
            have "~ has_snapshotted d r" using assms no_snap True by simp
            then show ?thesis
              using no_snap RecvMarker assms True chan not_i by auto
          qed
          ultimately show ?thesis using assms by simp
        next
          case False
          then have "msgs c i = msgs c' i" using False RecvMarker no_snap chan assms not_i by simp
          moreover have "msgs d' i = msgs d i"
          proof -
            have "~ has_snapshotted d r" using assms no_snap False by simp
            then show ?thesis
              using False RecvMarker no_snap chan assms not_i by simp
          qed
          ultimately show ?thesis using assms by simp
        qed
      qed
    qed
  qed
qed

lemma same_cs_2:
  assumes
    "∀p. has_snapshotted c p = has_snapshotted d p" and
    "cs c i = cs d i" and
    "c ⊨ ev ↦ c'" and
    "d ⊨ ev ↦ d'"
  shows
    "cs c' i = cs d' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    using assms(2) assms(3) assms(4) no_cs_change_if_no_channel by auto
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  then show ?thesis
  proof (cases ev)
    case (Snapshot r)
    with assms chan show ?thesis by (cases "r = q", auto)
  next
    case (RecvMarker i' r s)
    then show ?thesis
    proof (cases "has_snapshotted c r")
      case snap: True
      then have sdr: "has_snapshotted d r" using assms by auto
      then show ?thesis
      proof (cases "i = i'")
        case True
        then have "cs c' i = (fst (cs c i), Done)" 
          using RecvMarker assms(3) next_recv_marker by blast
        also have "... = cs d' i" 
          using RecvMarker True assms(2) assms(4) by auto
        finally show ?thesis using True by simp
      next
        case False
        then have "cs c' i = cs c i" using RecvMarker assms snap by auto
        also have "... = cs d' i" using RecvMarker assms snap sdr False by auto
        finally show ?thesis by simp
      qed
    next
      case no_snap: False
      then have nsdr: "~ has_snapshotted d r" using assms by blast
      show ?thesis
      proof (cases "i = i'")
        case True
        then have "cs c' i = (fst (cs c i), Done)" 
          using RecvMarker assms(3) next_recv_marker by blast
        also have "... = cs d' i" 
          using RecvMarker True assms(2) assms(4) by auto
        finally show ?thesis using True by simp
      next
        case not_i: False
        with assms RecvMarker chan no_snap show ?thesis by (cases "r = q", auto)
      qed
    qed
  next
    case (Trans r u u')
    then show ?thesis 
      by (metis assms(2) assms(3) assms(4) event.disc(1) regular_event same_cs_implies_same_resulting_cs)
  next
    case (Send i' r s u u' m)
    then show ?thesis 
      by (metis assms(2) assms(3) assms(4) event.disc(7) regular_event same_cs_implies_same_resulting_cs)
  next
    case (Recv i' r s u u' m)
    then show ?thesis  
      by (metis assms(2) assms(3) assms(4) event.disc(13) regular_event same_cs_implies_same_resulting_cs)
  qed
qed

lemma swap_Snapshot_Trans:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSnapshot ev" and
    "isTrans ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof -
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  have "ev = Snapshot ?p"
    by (metis assms(3) event.collapse(4))
  obtain u'' u''' where "ev' = Trans ?q u'' u'''" 
    by (metis assms(4) event.collapse(1))
  have "msgs c i = msgs d' i" 
    using Trans_msg assms(4) assms(5) by blast
  then have "msgs e' i = msgs d i"
  proof -
    have "∀p. has_snapshotted c p = has_snapshotted d' p" 
      using assms(4) assms(5) regular_event_preserves_process_snapshots by auto
    moreover have "msgs c i = msgs d' i" using ‹msgs c i = msgs d' i› by auto
    moreover have "c ⊨ ev ↦ d" using assms by auto
    moreover have "d' ⊨ ev ↦ e'" using assms by auto
    moreover have "~ regular_event ev" using assms by auto
    ultimately show ?thesis by (blast intro: same_messages_2[symmetric])
  qed
  then have "msgs d i = msgs e i" 
    using Trans_msg assms(2) assms(4) by blast
  then show ?thesis 
    by (simp add: ‹msgs e' i = msgs d i›)
qed

lemma swap_msgs_Trans_RecvMarker:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecvMarker ev" and
    "isTrans ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e' i = msgs e i"
proof -
  have nr: "~ regular_event ev" 
    using assms(3) nonregular_event by blast
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r where RecvMarker: "ev = RecvMarker i' ?p r"
    by (metis assms(3) event.collapse(5))
  obtain u'' u''' where Trans: "ev' = Trans ?q u'' u'''" 
    by (metis assms(4) event.collapse(1))
  have "msgs c i = msgs d' i" 
    using Trans_msg assms(4) assms(5) by blast
  then have "msgs e' i = msgs d i"
  proof -
    have "∀p. has_snapshotted d' p = has_snapshotted c p" 
      using assms(4) assms(5) regular_event_preserves_process_snapshots by auto
    moreover have "~ regular_event ev" using assms by auto
    moreover have "∀n. msgs d' n = msgs c n" (* why does he need this assumption? *)
      by (metis Trans assms(5) local.next.simps(3))
    ultimately show ?thesis
      using assms(1) assms(6) same_messages_2 by blast
  qed
  thm same_messages_2
  then have "msgs d i = msgs e i" 
    using Trans_msg assms(2) assms(4) by blast
  then show ?thesis 
    by (simp add: ‹msgs e' i = msgs d i›)
qed

lemma swap_Trans_Snapshot:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isTrans ev" and
    "isSnapshot ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_Snapshot_Trans by auto

lemma swap_Send_Snapshot:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSend ev" and
    "isSnapshot ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_msgs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Send: "ev = Send i' ?p r u u' m" 
    by (metis assms(3) event.collapse(2))
  have Snapshot: "ev' = Snapshot ?q" 
    by (metis assms(4) event.collapse(4))
  show ?thesis
  proof (cases "i = i'"; cases "p = ?q")
    assume asm: "i = i'" "p = ?q"
    then have "?p = p"
    proof -
      have "channel i' = Some (p, q)" using chan asm by simp
      then show ?thesis using assms can_occur_def Send chan 
        by (metis (mono_tags, lifting) event.simps(27) happen_implies_can_occur option.inject prod.inject)
    qed
    then show ?thesis using assms asm by simp
  next
    assume "i = i'" "p ≠ ?q"
    then have "msgs d i = msgs c i @ [Msg m]" 
      by (metis Send assms(1) next_send)
    moreover have "msgs e i = msgs d i" 
      by (metis Pair_inject Snapshot ‹p ≠ occurs_on ev'› assms(2) chan next_snapshot option.inject)
    moreover have "msgs d' i = msgs c i"
      by (metis Pair_inject Snapshot ‹p ≠ occurs_on ev'› assms(5) chan next_snapshot option.inject)
    moreover have "msgs e' i = msgs d' i @ [Msg m]" 
      by (metis Send ‹i = i'› assms(6) next_send)
    ultimately show ?thesis by simp
  next
    assume asm: "i ≠ i'" "p = ?q"
    then have "msgs d i = msgs c i" 
      by (metis Send assms(1) assms(3) event.sel(8) msgs_unchanged_for_other_is regular_event)
    moreover have "msgs e i = msgs c i @ [Marker]" 
      by (metis (full_types) Snapshot asm(2) assms(2) calculation chan next_snapshot)
    moreover have "msgs d' i = msgs c i @ [Marker]" 
      by (metis (full_types) Snapshot asm(2) assms(5) chan next_snapshot)
    moreover have "msgs e' i = msgs d' i" 
      by (metis Send asm(1) assms(6) next_send)
    ultimately show ?thesis by simp
  next
    assume "i ≠ i'" "p ≠ ?q"
    then have "msgs c i = msgs d i" 
      by (metis Send assms(1) assms(3) event.sel(8) msgs_unchanged_for_other_is regular_event)
    then have "msgs e i = msgs d' i"
      by (metis Pair_inject Snapshot ‹p ≠ occurs_on ev'› assms(2,5) chan next_snapshot option.inject)
    then show ?thesis 
      by (metis Send ‹i ≠ i'› assms(6) next_send)
  qed
qed

lemma swap_Snapshot_Send:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSnapshot ev" and
    "isSend ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_Send_Snapshot by auto

lemma swap_Recv_Snapshot:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isSnapshot ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_msgs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Recv: "ev = Recv i' ?p r u u' m" 
    by (metis assms(3) event.collapse(3))
  have Snapshot: "ev' = Snapshot ?q" 
    by (metis assms(4) event.collapse(4))
  show ?thesis
  proof (cases "i = i'"; cases "p = ?q")
    assume "i = i'" "p = ?q"
    then have "Msg m # msgs d i = msgs c i" 
      by (metis Recv assms(1) next_recv)
    moreover have "msgs e i = msgs d i @ [Marker]" 
      by (metis (full_types) Snapshot ‹p = occurs_on ev'› assms(2) chan next_snapshot)
    moreover have "msgs d' i = msgs c i @ [Marker]" 
      by (metis (full_types) Snapshot ‹p = occurs_on ev'› assms(5) chan next_snapshot)
    moreover have "Msg m # msgs e' i = msgs d' i" 
      by (metis Recv ‹i = i'› assms(6) next_recv)
    ultimately show ?thesis 
      by (metis list.sel(3) neq_Nil_conv tl_append2)
  next
    assume "i = i'" "p ≠ ?q"
    then have "Msg m # msgs d i = msgs c i" 
      by (metis Recv assms(1) next_recv)
    moreover have "msgs e i = msgs d i"
      by (metis Pair_inject Snapshot ‹p ≠ occurs_on ev'› assms(2) chan next_snapshot option.inject)
    moreover have "msgs d' i = msgs c i"
      by (metis Pair_inject Snapshot ‹p ≠ occurs_on ev'› assms(5) chan next_snapshot option.inject)
    moreover have "Msg m # msgs e' i = msgs d' i" 
      by (metis Recv ‹i = i'› assms(6) next_recv)
    ultimately show ?thesis by (metis list.inject)
  next
    assume "i ≠ i'" "p = ?q"
    then have "msgs d i = msgs c i" 
      by (metis Recv assms(1) next_recv)
    moreover have "msgs e i = msgs d i @ [Marker]" 
      by (metis (full_types) Snapshot ‹p = occurs_on ev'› assms(2) chan next_snapshot)
    moreover have "msgs d' i = msgs c i @ [Marker]" 
      by (metis (full_types) Snapshot ‹p = occurs_on ev'› assms(5) chan next_snapshot)
    moreover have "msgs e' i = msgs d' i" 
      by (metis Recv ‹i ~= i'› assms(6) next_recv)
    ultimately show ?thesis by simp
  next
    assume "i ≠ i'" "p ≠ ?q"
    then have "msgs d i = msgs c i" 
      by (metis Recv assms(1) next_recv)
    moreover have "msgs e i = msgs d i"
      by (metis Pair_inject Snapshot ‹p ≠ occurs_on ev'› assms(2) chan next_snapshot option.inject)
    moreover have "msgs d' i = msgs c i"
      by (metis Pair_inject Snapshot ‹p ≠ occurs_on ev'› assms(5) chan next_snapshot option.inject)
    moreover have "msgs e' i = msgs d' i" 
      by (metis Recv ‹i ~= i'› assms(6) next_recv)
    ultimately show ?thesis by auto
  qed
qed

lemma swap_Snapshot_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSnapshot ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_Recv_Snapshot by auto

lemma swap_msgs_Recv_RecvMarker:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isRecvMarker ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_msgs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  obtain i' p' r u u' m where Recv: "ev = Recv i' p' r u u' m" 
    by (metis assms(3) event.collapse(3))
  obtain i'' q' s where RecvMarker: "ev' = RecvMarker i'' q' s" 
    by (metis assms(4) event.collapse(5))
  have "i' ≠ i''"
  proof (rule ccontr)
    assume "~ i' ≠ i''"
    then have "channel i' = channel i''" by auto
    then have "Some (r, p') = Some (s, q')" using assms can_occur_def Recv RecvMarker by simp
    then show False using assms 
      by (metis Recv RecvMarker event.sel(3,5) option.inject prod.inject)
  qed
  then show ?thesis
  proof (cases "i = i' ∨ i = i''")
    case True
    then show ?thesis
    proof (elim disjE)
      assume "i = i'"
      then have pqrp: "(p, q) = (r, p')" 
        by (metis Recv assms(1) chan distributed_system.can_occur_Recv distributed_system_axioms next_recv option.inject)
      then show ?thesis
      proof (cases "has_snapshotted c q'")
        case snap: True
        then have "Msg m # msgs d i = msgs c i" 
          by (metis Recv ‹i = i'› assms(1) next_recv)
        moreover have "msgs c i = msgs d' i" 
          using RecvMarker ‹i = i'› ‹i' ≠ i''› assms(5) msgs_unchanged_if_snapshotted_RecvMarker_for_other_is snap by blast
        moreover have "msgs d i = msgs e i" 
          using RecvMarker ‹i = i'› ‹i' ≠ i''› assms(1) assms(2) snap snapshot_state_unchanged by auto
        moreover have "Msg m # msgs e' i = msgs d' i" 
          by (metis Recv ‹i = i'› assms(6) next_recv)
        ultimately show ?thesis by (metis list.inject)
      next
        case no_snap: False
        then have msgs_d: "Msg m # msgs d i = msgs c i" 
          by (metis Recv ‹i = i'› assms(1) next_recv)
        then show ?thesis
        proof (cases "q' = r")
          case True
          then have "msgs d' i = msgs c i @ [Marker]"
          proof -
            have "channel i = Some (q', q)" 
              using True chan pqrp by blast
            then show ?thesis using RecvMarker assms no_snap 
              by (simp add: no_snap ‹i = i'› ‹i' ≠ i''›)
          qed
          moreover have "Msg m # msgs e' i = msgs d' i" 
            by (metis Recv ‹i = i'› assms(6) next_recv)
          moreover have "msgs e i = msgs d i @ [Marker]"
          proof -
            have "ps d q' = ps c q'" 
              using assms(1) assms(7) no_state_change_if_no_event RecvMarker by auto
            then show ?thesis
              using RecvMarker ‹i = i'› ‹i' ≠ i''› assms True chan no_snap pqrp by simp
          qed
          ultimately show ?thesis using msgs_d 
            by (metis append_self_conv2 list.inject list.sel(3) message.distinct(1) tl_append2)
        next
          case False
          then have "msgs e i = msgs d i"
          proof -
            have "~ has_snapshotted d q'" 
              using assms(1) assms(7) no_snap no_state_change_if_no_event RecvMarker by auto
            moreover have "∄r. channel i = Some (q', r)" using chan False pqrp by auto
            moreover have "i ≠ i''" using ‹i = i'› ‹i' ≠ i''› by simp
            ultimately show ?thesis using RecvMarker assms by simp
          qed
          moreover have "msgs d' i = msgs c i"
          proof -
            have "∄r. channel i = Some (q', r)" 
              using False chan pqrp by auto
            moreover have "i ≠ i''" using ‹i = i'› ‹i' ≠ i''› by simp
            ultimately show ?thesis using RecvMarker assms(5) no_snap by auto
          qed
          moreover have "Msg m # msgs e' i = msgs d' i" 
            by (metis Recv ‹i = i'› assms(6) next_recv)
          ultimately show ?thesis using msgs_d 
            by (metis list.inject)
        qed
      qed
    next
      assume "i = i''"
      then have "msgs d i = msgs c i" using assms
        by (metis Recv ‹i' ≠ i''› next_recv) 
      moreover have "msgs e i = msgs d' i"
      proof -
        have "∀p. has_snapshotted c p = has_snapshotted d p" 
          by (metis Recv assms(1) next_recv)
        then show ?thesis 
          by (meson assms(2) assms(5) calculation same_messages_2 same_messages_imply_same_resulting_messages)
      qed
      moreover have "msgs e' i = msgs d' i"
        using assms by (metis Recv ‹i' ≠ i''› ‹i = i''› next_recv)
      ultimately show ?thesis by simp
    qed
  next
    assume asm: "~ (i = i' ∨ i = i'')"
    then have "msgs c i = msgs d i" 
      by (metis Recv assms(1) assms(3) event.distinct_disc(16,18) event.sel(9) msgs_unchanged_for_other_is nonregular_event)
    then have "msgs d' i = msgs e i"
    proof -
      have "∀p. has_snapshotted c p = has_snapshotted d p" 
        using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
      then show ?thesis 
        by (meson ‹msgs c i = msgs d i› assms(2) assms(5) same_messages_2 same_messages_imply_same_resulting_messages)
    qed
    then show ?thesis 
      by (metis Recv asm assms(3) assms(6) event.distinct_disc(16,18) event.sel(9) msgs_unchanged_for_other_is nonregular_event)
  qed
qed

lemma swap_RecvMarker_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecvMarker ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_msgs_Recv_RecvMarker by auto

lemma swap_msgs_Send_RecvMarker:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSend ev" and
    "isRecvMarker ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_msgs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' p' r u u' m where Send: "ev = Send i' p' r u u' m" 
    by (metis assms(3) event.collapse(2))
  obtain i'' q' s where RecvMarker: "ev' = RecvMarker i'' q' s" 
    by (metis assms(4) event.collapse(5))
  have "p' ≠ q'" using Send RecvMarker assms by simp
  show ?thesis
  proof (cases "i = i'"; cases "i = i''", goal_cases)
    case 1
    then have "msgs e' i = msgs d' i @ [Msg m]" 
      by (metis Send assms(6) next_send)
    moreover have "Marker # msgs d' i = msgs c i" using ‹i = i''› RecvMarker assms by simp
    moreover have "msgs d i = msgs c i @ [Msg m]" 
      by (metis "1"(1) Send assms(1) next_send)
    moreover have "Marker # msgs e i = msgs d i" using ‹i = i''› RecvMarker assms by simp
    ultimately show ?thesis 
      by (metis append_self_conv2 list.inject list.sel(3) message.distinct(1) tl_append2)
  next
    case 2
    then have pqpr: "(p, q) = (p', r)" using chan Send can_occur_def assms by simp
    then have "msgs d i = msgs c i @ [Msg m]" 
      by (metis 2(1) Send assms(1) next_send)
    moreover have "msgs e' i = msgs d' i @ [Msg m]" 
      by (metis "2"(1) Send assms(6) next_send)
    moreover have "msgs d' i = msgs c i"
    proof -
      have "∄r. channel i = Some (q', r)" using ‹p' ≠ q'› chan pqpr by simp
      with RecvMarker ‹i ≠ i''› ‹i = i'› assms show ?thesis by (cases "has_snapshotted c q'", auto)
    qed
    moreover have "msgs e i = msgs d i"
    proof -
      have "∄r. channel i = Some (q', r)" using ‹p' ≠ q'› chan pqpr by simp
      with RecvMarker ‹i ≠ i''› ‹i = i'› assms show ?thesis by (cases "has_snapshotted d q'", auto)
    qed
    ultimately show ?thesis by simp
  next
    assume 3: "i ≠ i'" "i = i''"
    then have mcd: "msgs c i = msgs d i" 
      by (metis Send assms(1) next_send)
    moreover have "msgs e i = msgs d' i"
    proof -
      have "∀p. has_snapshotted c p = has_snapshotted d p" 
        using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
      moreover have "~ regular_event ev'" using assms by auto
      ultimately show ?thesis using mcd assms(2,5) by (blast intro: same_messages_2[symmetric])
    qed
    moreover have "msgs e' i = msgs d' i" 
      by (metis "3"(1) Send assms(6) next_send)
    ultimately show ?thesis by simp
  next
    assume 4: "i ≠ i'" "i ≠ i''"
    have mcd: "msgs c i = msgs d i" 
      by (metis "4"(1) Send assms(1) assms(3) event.distinct_disc(12,14) event.sel(8) msgs_unchanged_for_other_is nonregular_event)
    have "msgs d' i = msgs e i"
    proof -
      have "∀p. has_snapshotted c p = has_snapshotted d p" 
        using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
      moreover have "~ regular_event ev'" using assms by auto
      ultimately show ?thesis using mcd assms(2,5) same_messages_2 by blast
    qed
    moreover have "msgs e' i = msgs d' i"
      by (metis "4"(1) Send assms(6) next_send)
    ultimately show ?thesis by simp
  qed
qed

lemma swap_RecvMarker_Send:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecvMarker ev" and
    "isSend ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "msgs e i = msgs e' i"
  using assms swap_msgs_Send_RecvMarker by auto

lemma swap_cs_Trans_Snapshot:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isTrans ev" and
    "isSnapshot ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_cs_change_if_no_channel)
next
  case False
  then obtain p q where "channel i = Some (p, q)" by auto
  have nr: "~ regular_event ev'" 
    using assms(4) nonregular_event by blast
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain u'' u''' where "ev = Trans ?p u'' u'''" 
    by (metis assms(3) event.collapse(1))
  have "ev' = Snapshot ?q"
    by (metis assms(4) event.collapse(4))
  have "cs d i = cs c i" 
    by (metis assms(1) assms(3) event.distinct_disc(4) no_cs_change_if_no_event regular_event)
  then have "cs e i = cs d' i"
  proof -
    have "∀p. has_snapshotted d p = has_snapshotted c p" 
      using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
    then show ?thesis 
      using ‹cs d i = cs c i› assms(2) assms(5) same_cs_2 by blast
  qed
  also have "... = cs e' i" 
    using assms(3) assms(6) no_cs_change_if_no_event regular_event by blast
  finally show ?thesis by simp
qed

lemma swap_cs_Snapshot_Trans:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSnapshot ev" and
    "isTrans ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
  using swap_cs_Trans_Snapshot assms by auto

lemma swap_cs_Send_Snapshot:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSend ev" and
    "isSnapshot ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_cs_change_if_no_channel)
next
  case False
  then obtain p q where "channel i = Some (p, q)" by auto
  have nr: "~ regular_event ev'" 
    using assms(4) nonregular_event by blast
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Send: "ev = Send i' ?p r u u' m" 
    by (metis assms(3) event.collapse(2))
  have Snapshot: "ev' = Snapshot ?q"
    by (metis assms(4) event.collapse(4))
  have "cs d i = cs c i" 
    by (metis Send assms(1) next_send)
  then have "cs e i = cs d' i"
  proof -
    have "∀p. has_snapshotted d p = has_snapshotted c p" 
      using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
    then show ?thesis 
      using ‹cs d i = cs c i› assms(2) assms(5) same_cs_2 by blast
  qed
  also have "... = cs e' i" 
    using assms(3) assms(6) no_cs_change_if_no_event regular_event by blast
  finally show ?thesis by simp
qed

lemma swap_cs_Snapshot_Send:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSnapshot ev" and
    "isSend ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
  using swap_cs_Send_Snapshot assms by auto

lemma swap_cs_Recv_Snapshot:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isSnapshot ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "cs e i = cs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_cs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  have nr: "~ regular_event ev'" 
    using assms(4) nonregular_event by blast
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Recv: "ev = Recv i' ?p r u u' m" 
    by (metis assms(3) event.collapse(3))
  have Snapshot: "ev' = Snapshot ?q"
    by (metis assms(4) event.collapse(4))
  show ?thesis
  proof (cases "i = i'")
    case True
    then show ?thesis
    proof (cases "snd (cs c i) = Recording")
      case True
      then have "cs d i = (fst (cs c i) @ [m], Recording)" using Recv assms True ‹i = i'› chan 
        by (metis next_recv)
      moreover have "cs e i = cs d i"
        by (metis Snapshot assms(2) calculation fst_conv next_snapshot)
      moreover have "cs c i = cs d' i"
        by (metis Snapshot True assms(5) next_snapshot prod.collapse)
      moreover have "cs e' i = (fst (cs d' i) @ [m], Recording)" 
        by (metis (mono_tags, lifting) Recv assms(1) assms(6) calculation(1) calculation(3) next_recv)
      ultimately show ?thesis by simp
    next
      case False
      have "cs d i = cs c i" 
        by (metis False Recv assms(1) next_recv)
      have "cs e i = cs d' i"
      proof -
        have "∀p. has_snapshotted d p = has_snapshotted c p" 
          using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
        then show ?thesis 
          using ‹cs d i = cs c i› assms(2) assms(5) same_cs_2 by blast
      qed
      moreover have "cs d' i = cs e' i"
      proof -
        have "cs d' i = cs c i" 
          by (metis Pair_inject Recv Snapshot True assms(1) assms(5) assms(7) can_occur_Recv distributed_system.happen_implies_can_occur distributed_system.next_snapshot distributed_system_axioms option.inject)
        then show ?thesis using chan ‹i = i'› False Recv assms 
          by (metis next_recv)
      qed
      ultimately show ?thesis by simp
    qed
  next
    case False
    have "cs d i = cs c i" 
      by (metis False Recv assms(1) next_recv)
    then have "cs e i = cs d' i"
    proof -
      have "∀p. has_snapshotted d p = has_snapshotted c p" 
        using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
      then show ?thesis 
        using ‹cs d i = cs c i› assms(2) assms(5) same_cs_2 by blast
    qed
    also have "... = cs e' i" 
      by (metis False Recv assms(6) next_recv)
    finally show ?thesis by simp
  qed
qed

lemma swap_cs_Snapshot_Recv:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSnapshot ev" and
    "isRecv ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "cs e i = cs e' i"
  using swap_cs_Recv_Snapshot assms by auto

lemma swap_cs_Trans_RecvMarker:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isTrans ev" and
    "isRecvMarker ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_cs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  have nr: "~ regular_event ev'" 
    using assms(4) nonregular_event by blast
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain u'' u''' where "ev = Trans ?p u'' u'''" 
    by (metis assms(3) event.collapse(1))
  obtain i' s where "ev' = RecvMarker i' ?q s"
    by (metis assms(4) event.collapse(5))
  have "cs d i = cs c i" 
    by (metis assms(1) assms(3) event.distinct_disc(4) no_cs_change_if_no_event regular_event)
  then have "cs e i = cs d' i"
  proof -
    have "∀p. has_snapshotted d p = has_snapshotted c p" 
      using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
    then show ?thesis 
      using ‹cs d i = cs c i› assms(2) assms(5) same_cs_2 by blast
  qed
  also have "... = cs e' i" 
    using assms(3) assms(6) no_cs_change_if_no_event regular_event by blast
  finally show ?thesis by simp
qed

lemma swap_cs_RecvMarker_Trans:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecvMarker ev" and
    "isTrans ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
  using swap_cs_Trans_RecvMarker assms by auto

lemma swap_cs_Send_RecvMarker:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isSend ev" and
    "isRecvMarker ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_cs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  have nr: "~ regular_event ev'" 
    using assms(4) nonregular_event by blast
  let ?p = "occurs_on ev"
  let ?q = "occurs_on ev'"
  obtain i' r u u' m where Send: "ev = Send i' ?p r u u' m" 
    by (metis assms(3) event.collapse(2))
  obtain i'' s where RecvMarker: "ev' = RecvMarker i'' ?q s"
    by (metis assms(4) event.collapse(5))
  have "cs d i = cs c i" 
    by (metis assms(1) assms(3) event.distinct_disc(10,12,14) no_cs_change_if_no_event nonregular_event)
  then have "cs e i = cs d' i"
  proof -
    have "∀p. has_snapshotted d p = has_snapshotted c p" 
      using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
    then show ?thesis 
      using ‹cs d i = cs c i› assms(2) assms(5) same_cs_2 by blast
  qed
  also have "... = cs e' i" 
    using assms(3) assms(6) no_cs_change_if_no_event regular_event by blast
  finally show ?thesis by simp
qed

lemma swap_cs_RecvMarker_Send:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecvMarker ev" and
    "isSend ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'"
  shows
    "cs e i = cs e' i"
  using swap_cs_Send_RecvMarker assms by auto

lemma swap_cs_Recv_RecvMarker:
  assumes
    "c ⊨ ev ↦ d" and
    "d ⊨ ev' ↦ e" and
    "isRecv ev" and
    "isRecvMarker ev'" and
    "c ⊨ ev' ↦ d'" and
    "d' ⊨ ev ↦ e'" and
    "occurs_on ev ≠ occurs_on ev'"
  shows
    "cs e i = cs e' i"
proof (cases "channel i = None")
  case True
  then show ?thesis 
    by (metis assms(1) assms(2) assms(5) assms(6) no_cs_change_if_no_channel)
next
  case False
  then obtain p q where chan: "channel i = Some (p, q)" by auto
  have nr: "~ regular_event ev'" 
    using assms(4) nonregular_event by blast
  obtain i' p' r u u' m where Recv: "ev = Recv i' p' r u u' m" 
    by (metis assms(3) event.collapse(3))
  obtain i'' q' s where RecvMarker: "ev' = RecvMarker i'' q' s"
    by (metis assms(4) event.collapse(5))
  have "i' ≠ i''"
  proof (rule ccontr)
    assume "~ i' ≠ i''"
    then have "channel i' = channel i''" by simp
    then have "(r, p') = (s, q')" using Recv RecvMarker assms can_occur_def by simp
    then show False using Recv RecvMarker assms can_occur_def by simp
  qed
  show ?thesis
  proof (cases "i = i'")
    case True
    then have pqrp: "(p, q) = (r, p')" using Recv assms can_occur_def chan by simp
    then show ?thesis
    proof (cases "snd (cs c i)")
      case NotStarted
      then have "cs d i = cs c i" using assms Recv ‹i = i'› by simp
      moreover have "cs d' i = cs e i"
      proof -
        have "∀p. has_snapshotted c p = has_snapshotted d p" 
          using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
        with assms(2,5) calculation show ?thesis  by (blast intro: same_cs_2[symmetric])
      qed
      thm same_cs_2
      moreover have "cs d' i = cs e' i"
      proof -
        have "cs d' i = cs c i"
        proof -
          have "∄r. channel i = Some (r, q')" 
            using Recv RecvMarker assms(7) chan pqrp by auto
          with RecvMarker assms chan ‹i = i'› ‹i' ≠ i''› show ?thesis
            by (cases "has_snapshotted c q'", auto)
        qed
        then show ?thesis using assms Recv ‹i = i'› NotStarted by simp
      qed
      ultimately show ?thesis by simp
    next
      case Done
      then have "cs d i = cs c i" using assms Recv ‹i = i'› by simp
      moreover have "cs d' i = cs e i"
      proof -
        have "∀p. has_snapshotted c p = has_snapshotted d p" 
          using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
        then show ?thesis using assms(2,5) calculation by (blast intro: same_cs_2[symmetric])
      qed
      moreover have "cs d' i = cs e' i"
      proof -
        have "cs d' i = cs c i"
        proof -
          have "∄r. channel i = Some (r, q')" 
            using Recv RecvMarker assms(7) chan pqrp by auto
          with RecvMarker assms chan ‹i = i'› ‹i' ≠ i''› show ?thesis
            by (cases "has_snapshotted c q'", auto)
        qed
        then show ?thesis using assms Recv ‹i = i'› Done by simp
      qed
      ultimately show ?thesis by simp
    next
      case Recording
      have "cs d i = (fst (cs c i) @ [m], Recording)" 
        using Recording Recv True assms(1) by auto
      moreover have "cs e i = cs d i"
      proof -
        have "∄r. channel i = Some (r, q')" 
          using Recv RecvMarker assms(7) chan pqrp by auto
        with RecvMarker assms chan ‹i = i'› ‹i' ≠ i''› show ?thesis
          by (cases "has_snapshotted d q'", auto)
      qed
      moreover have "cs c i = cs d' i " 
      proof -
        have "∄r. channel i = Some (r, q')" 
          using Recv RecvMarker assms(7) chan pqrp by auto
        with RecvMarker assms chan ‹i = i'› ‹i' ≠ i''› show ?thesis
          by (cases "has_snapshotted c q'", auto)
      qed
      moreover have "cs e' i = (fst (cs d' i) @ [m], Recording)" 
        using Recording Recv True assms(6) calculation(3) by auto
      ultimately show ?thesis by simp
    qed
  next
    case False
    have "cs d i = cs c i" 
      using False Recv assms(1) by auto
    then have "cs e i = cs d' i"
    proof -
      have "∀p. has_snapshotted d p = has_snapshotted c p" 
        using assms(1) assms(3) regular_event_preserves_process_snapshots by auto
      then show ?thesis 
        using ‹cs d i = cs c i› assms(2) assms(5) same_cs_2 by blast
    qed
    also have "... = cs e' i" 
      using False Recv assms(6) by auto
    finally show ?thesis by simp
  qed
qed

end (* context distributed_system *)

end (* theory Swap *)