Theory IMAP-proof-independent

section ‹Independence of IMAP Commands›

text‹In this section we show that two concurrent operations that reference to the same tag must be 
identical.›

theory
  "IMAP-proof-independent"
  imports
    "IMAP-def"
    "IMAP-proof-helpers"  
begin

lemma (in imap) Broadcast_Expunge_Deliver_prefix_closed:
  assumes "xs @ [Broadcast (i, Expunge e mo i)] prefix of j"
  shows "Deliver (mo, Append mo e)  set xs  
    ( mo2 . Deliver (mo, Store e mo2 mo)  set xs)"
proof -  
  obtain y where "apply_operations xs = Some y"
    using assms broadcast_only_valid_msgs by blast
  moreover hence "mo  snd (y e)"
    using broadcast_only_valid_msgs[of xs "(i, Expunge e mo i)" j] 
      valid_behaviours_def[of y "(i, Expunge e mo i)"] assms by auto
  ultimately show ?thesis
    using assms Deliver_added_files apply_operations_added_files by blast
qed

lemma (in imap) Broadcast_Store_Deliver_prefix_closed:
  assumes "xs @ [Broadcast (i, Store e mo i)] prefix of j"
  shows "Deliver (mo, Append mo e)  set xs  
    ( mo2 . Deliver (mo, Store e mo2 mo)  set xs)"
proof -  
  obtain y where "apply_operations xs = Some y"
    using assms broadcast_only_valid_msgs by blast
  moreover hence "mo  snd (y e)"
    using broadcast_only_valid_msgs[of xs "(i, Store e mo i)" j] 
      valid_behaviours_def[of y "(i, Store e mo i)"] assms by auto
  ultimately show ?thesis
    using assms Deliver_added_files apply_operations_added_files by blast
qed

lemma (in imap) Deliver_added_ids:
  assumes "xs prefix of j"
    and "i  set (added_ids xs e)"
  shows "Deliver (i, Create i e)  set xs  
    ( mo . Deliver (i, Expunge e mo i)  set xs)"
  using assms proof (induct xs rule: rev_induct, clarsimp)
  case (snoc x xs) thus ?case
  proof (cases x, force)
    case X: (Deliver e')
    moreover obtain a b where "e' = (a, b)" by force
    ultimately show ?thesis
      using snoc apply (case_tac b; clarify)
          apply (simp, metis added_ids_Deliver_Create_diff_collapse 
          added_ids_Deliver_Create_same_collapse empty_iff list.set(1) set_ConsD create_id_valid 
          in_set_conv_decomp prefix_of_appendD, force)
      using append_id_valid apply (simp, metis (no_types, lifting)  prefix_of_appendD, simp, metis 
          Un_iff added_ids_Deliver_Expunge_diff_collapse added_ids_Deliver_Expunge_same_collapse 
          empty_iff expunge_id_valid list.set(1) list.set_intros(1) prefix_of_appendD set_ConsD 
          set_append)
      by (simp, blast)
  qed
qed

lemma (in imap) Broadcast_Deliver_prefix_closed:
  assumes "xs @ [Broadcast (r, Delete ix e)] prefix of j"
    and "i  ix"
  shows "Deliver (i, Create i e)  set xs  
    Deliver (i, Append i e)  set xs  
    ( mo . Deliver (i, Expunge e mo i)  set xs)  
    ( mo . Deliver (i, Store e mo i)  set xs)"
proof -  
  obtain y where "apply_operations xs = Some y"
    using assms broadcast_only_valid_msgs by blast
  moreover hence "ix = fst (y e)  snd (y e)"
    by (metis (mono_tags, lifting) assms(1) broadcast_only_valid_msgs operation.case(2)
        option.simps(1) valid_behaviours_def case_prodD)
  ultimately show ?thesis
    using assms Deliver_added_ids apply_operations_added_ids
    by (metis Deliver_added_files Un_iff apply_operations_added_files le_iff_sup prefix_of_appendD)
qed

lemma (in imap) concurrent_create_delete_independent_technical:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Create i e)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e)  set (node_deliver_messages xs)"
  shows "hb (i, Create i e) (ir, Delete is e)"
proof -
  have f1: "Deliver (i, Create i e)  set (history j)"
    using assms prefix_msg_in_history by blast
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f2: "Deliver (i, Create i e)  set pre  
                  Deliver (i, Append i e)  set pre  
                  ( mo . Deliver (i, Expunge e mo i)  set pre)  
                  ( mo . Deliver (i, Store e mo i)  set pre)"
    using Broadcast_Deliver_prefix_closed assms by auto
  have f3: "Deliver (i, Append i e)  set pre" using f1 P 
    by (metis (full_types) Pair_inject fst_conv network.delivery_has_a_cause network.msg_id_unique 
        network_axioms operation.simps(9) prefix_elem_to_carriers prefix_of_appendD)
  have f4: " mo . Deliver (i, Expunge e mo i)  set pre" using f1 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.simps(11)
        prefix_elem_to_carriers prefix_of_appendD)
  have " mo . Deliver (i, Store e mo i)  set pre" using f1 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.simps(13)
        prefix_elem_to_carriers prefix_of_appendD) 
  thus ?thesis using f2 f3 f4  P events_in_local_order hb_deliver by blast
qed

lemma (in imap) concurrent_store_expunge_independent_technical:
  assumes "xs prefix of j"
    and "(i, Store e mo i)  set (node_deliver_messages xs)" 
    and "(r, Expunge e i r)  set (node_deliver_messages xs)"
  shows "hb (i, Store e mo i) (r, Expunge e i r)"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Expunge e i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  moreover hence f1: "Deliver (i, Append i e)  set pre  
  ( mo2 . Deliver (i, Store e mo2 i)  set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1) by auto
  hence f2: "Deliver (i, Append i e)  set (history k)"
    by (metis Pair_inject assms(1) assms(2) fst_conv msg_id_unique network.delivery_has_a_cause 
        network_axioms operation.distinct(17) prefix_msg_in_history)
  from f1 obtain mo2 :: 'a where
    "Deliver (i, Store e mo2 i)  set (history k)" using f2
    using P prefix_elem_to_carriers by blast  
  hence "Deliver (i, Store e mo i)  set (history k)" using assms f1 f2 P 
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        prefix_msg_in_history)    
  then show ?thesis
    using hb.intros(2) events_in_local_order f1 f2 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique node_histories.prefix_of_appendD 
        node_histories_axioms prefix_elem_to_carriers)
qed

lemma (in imap) concurrent_store_expunge_independent_technical2:
  assumes "xs prefix of j"
    and "(i, Store e1 mo2 i)  set (node_deliver_messages xs)" 
    and "(r, Expunge e mo r)  set (node_deliver_messages xs)"
  shows "mo2  r"
proof -
  obtain oid :: "'a × ('a, 'b) operation  nat" where
    oid: "p n. Deliver p  set (history n)  Broadcast p  set (history (oid p))"
    by (metis (no_types) delivery_has_a_cause)
  hence f1: "Broadcast (r, Expunge e mo r)  set (history (oid (r, Expunge e mo r)))"
    using assms(1) assms(3) prefix_msg_in_history by blast
  obtain k :: "'a  'b  ('a × ('a, 'b) operation) event list  'a" where k: 
    "i e pre. (mo. Deliver (i, Store e mo i)  set pre) = 
    (Deliver (i, Store e (k i e pre) i)  set pre)"
    by moura
  obtain pre :: "nat  ('a × ('a, 'b) operation) event  ('a × ('a, 'b) operation) event list" 
    where pre: "k op1. (op2. op2 @ [op1] prefix of k) = (pre k op1 @ [op1] prefix of k)"
    by moura
  hence f2: "e n. e  set (history n)  pre n e @ [e] prefix of n"
    using events_before_exist by simp
  hence f3: "pre (oid (i, Store e1 mo2 i)) (Broadcast (i, Store e1 mo2 i))
  prefix of oid (i, Store e1 mo2 i)"
    using oid  assms(1) assms(2) prefix_msg_in_history by blast
  have f4: "Deliver (r, Append r e1)  set (history (oid (i, Store e1 mo2 i)))"
    by (metis (no_types) oid f1 fst_conv msg_id_unique old.prod.inject operation.distinct(15))
  have "Deliver (r, Store e1 (k r e1 (pre (oid (i, Store e1 mo2 i)) 
  (Broadcast (i, Store e1 mo2 i)))) r)  set (history (oid (i, Store e1 mo2 i)))"
    by (metis (no_types) oid f1 fst_conv msg_id_unique old.prod.inject operation.distinct(19))
  thus ?thesis using oid k f2 f3 f4 assms
    by (metis (no_types, lifting) Broadcast_Store_Deliver_prefix_closed 
        network.prefix_msg_in_history network_axioms prefix_elem_to_carriers)
qed

lemma (in imap) concurrent_store_delete_independent_technical:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Store e mo i)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e)  set (node_deliver_messages xs)"
  shows "hb (i, Store e mo i) (ir, Delete is e)"
proof -
  have f1: "Deliver (i, Store e mo i)  set (history j)" using assms prefix_msg_in_history by auto
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f2: "Deliver (i, Create i e)  set pre  
  Deliver (i, Append i e)  set pre 
  ( mo . Deliver (i, Expunge e mo i)  set pre)  
  ( mo . Deliver (i, Store e mo i)  set pre)"  
    using Broadcast_Deliver_prefix_closed assms(1) by auto    
  have f3: "Deliver (i, Create i e)  set pre" using f1 P 
    by (metis Pair_inject delivery_has_a_cause fst_conv msg_id_unique operation.distinct(7) 
        prefix_elem_to_carriers prefix_of_appendD)
  have f4: "Deliver (i, Append i e)  set pre" using f1 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique operation.distinct(17) 
        prefix_elem_to_carriers prefix_of_appendD prod.inject)
  have " mo . Deliver (i, Expunge e mo i)  set pre" using f1 P
    by (metis Pair_inject delivery_has_a_cause fst_conv msg_id_unique operation.simps(25) 
        prefix_elem_to_carriers prefix_of_appendD)
  hence "Deliver (i, Store e mo i)  set pre" using f1 f2 f3 f4 P
    by (metis delivery_has_a_cause fst_conv msg_id_unique node_histories.prefix_of_appendD 
        node_histories_axioms prefix_elem_to_carriers)     
  thus ?thesis using P events_in_local_order hb_deliver by blast
qed

lemma (in imap) concurrent_append_delete_independent_technical:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Append i e)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e)  set (node_deliver_messages xs)"
  shows "hb (i, Append i e) (ir, Delete is e)"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f1: "Deliver (i, Create i e)  set pre  
  Deliver (i, Append i e)  set pre  
  ( mo . Deliver (i, Expunge e mo i)  set pre)  
  ( mo . Deliver (i, Store e mo i)  set pre)"
    using Broadcast_Deliver_prefix_closed assms(1) by auto
  hence "Deliver (i, Append i e)  set pre" using assms P f1
    by (metis (no_types, opaque_lifting) delivery_has_a_cause events_in_local_order fst_conv 
        hb_broadcast_exists1 hb_deliver msg_id_unique prefix_msg_in_history)
  thus ?thesis using P events_in_local_order hb_deliver by blast
qed

lemma (in imap) concurrent_append_expunge_independent_technical:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e)  set (node_deliver_messages xs)" 
    and "(r, Expunge e mo r)  set (node_deliver_messages xs)"
  shows "hb (i, Append i e) (r, Expunge e mo r)"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Expunge e mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f1: "Deliver (mo, Append mo e)  set pre  
  ( mo2 . Deliver (mo, Store e mo2 mo)  set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1) by auto
  hence "( mo2 . Deliver (mo, Store e mo2 mo)  set pre)" using P assms 
  proof -
    have "Deliver (mo, Append mo e)  set (history j)"
      using assms(1) assms(2) assms(3) prefix_msg_in_history by blast
    thus ?thesis
      by (metis (no_types) P Pair_inject delivery_has_a_cause fst_conv msg_id_unique 
          operation.simps(23) prefix_elem_to_carriers prefix_of_appendD)
  qed
  thus ?thesis
    using hb.intros(2) events_in_local_order assms(1) P f1 by blast
qed

lemma (in imap) concurrent_append_store_independent_technical:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e)  set (node_deliver_messages xs)" 
    and "(r, Store e mo r)  set (node_deliver_messages xs)"
  shows "hb (i, Append i e) (r, Store e mo r)"
proof -
  obtain pre k where pre: "pre@[Broadcast (r, Store e mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  moreover hence f1: "Deliver (mo, Append mo e)  set pre  
  ( mo2 . Deliver (mo, Store e mo2 mo)  set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1) by auto
  have f2: "Deliver (i, Append i e)  set (history j)"
    by (meson assms network.prefix_msg_in_history network_axioms)
  then show ?thesis using assms f1 
    by (metis  pre delivery_has_a_cause events_in_local_order fst_conv hb_deliver 
        msg_id_unique node_histories.prefix_of_appendD node_histories_axioms 
        prefix_elem_to_carriers)
qed

lemma (in imap) concurrent_expunge_delete_independent_technical:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Expunge e mo i)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e)  set (node_deliver_messages xs)"
  shows "hb (i, Expunge e mo i) (ir, Delete is e)"
proof -
  obtain pre k where pre: "pre@[Broadcast (ir, Delete is e)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  moreover hence A: "Deliver (i, Create i e)  set pre  
  Deliver (i, Append i e)  set pre  
  ( mo . Deliver (i, Expunge e mo i)  set pre)  
  ( mo . Deliver (i, Store e mo i)  set pre)"
    using Broadcast_Deliver_prefix_closed assms(1) by auto      
  hence "Deliver (i, Expunge e mo i)  set pre" using assms
  proof -
    have f1: "e. e  set pre  e  set (history k)"
      using pre prefix_elem_to_carriers by blast
    have f2: "Deliver (i, Expunge e mo i)  set (history j)"
      by (meson assms network.prefix_msg_in_history network_axioms)
    then show ?thesis using f1 A 
      by (metis (no_types, lifting) fst_conv msg_id_unique network.delivery_has_a_cause 
          network_axioms)
  qed     
  ultimately show ?thesis
    using hb.intros(2) events_in_local_order by blast
qed

lemma (in imap) concurrent_store_store_independent_technical:
  assumes "xs prefix of j"
    and "(i, Store e mo i)  set (node_deliver_messages xs)" 
    and "(r, Store e i r)  set (node_deliver_messages xs)"
  shows "hb (i, Store e mo i) (r, Store e i r)"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Store e i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  hence f1: "e. e  set pre  e  set (history k)"
    using prefix_elem_to_carriers by blast
  have f2: "Deliver (i, Append i e)  set pre  ( mo2 . Deliver (i, Store e mo2 i)  set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1) P by auto     
  hence "Deliver (i, Store e mo i)  set pre" using assms f1 
    by (metis delivery_has_a_cause fst_conv msg_id_unique prefix_msg_in_history)
  then show ?thesis
    using hb.intros(2) events_in_local_order P by blast
qed

lemma (in imap) expunge_delete_tag_causality:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Expunge e1 mo i)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e2)  set (node_deliver_messages xs)" 
    and "pre@[Broadcast (ir, Delete is e2)] prefix of k"
  shows "Deliver (i, Expunge e2 mo i)  set (history k)"
proof- 
  have f1: "Deliver (i, Append i e2)  set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(15) prefix_msg_in_history)
  have f2: "Deliver (i, Create i e2)  set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(5) prefix_msg_in_history)
  have f3: " mo. Deliver (i, Store e2 mo i)  set (history k)" using assms
    by (metis Pair_inject fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        operation.simps(25) prefix_msg_in_history)
  hence " mo1. Deliver (i, Expunge e2 mo1 i)  set (history k)" using assms f1 f2 
    by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms node_histories.prefix_of_appendD 
        node_histories_axioms prefix_elem_to_carriers)
  then obtain mo1 :: 'a where
    "Deliver (i, Expunge e2 mo1 i)  set (history k)" by blast
  then show ?thesis  using assms f1 f2 f3
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.inject(4) prefix_msg_in_history)
qed

lemma (in imap) expunge_delete_ids_imply_messages_same:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Expunge e1 mo i)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e2)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  hence "Deliver (i, Expunge e2 mo i)  set (history k)" using assms expunge_delete_tag_causality
    by blast
  then show ?thesis using assms
    by (metis delivery_has_a_cause fst_conv network.msg_id_unique network_axioms 
        operation.inject(4) prefix_msg_in_history prod.inject)
qed

lemma (in imap) store_delete_ids_imply_messages_same:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Store e1 mo i)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e2)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast 
  have f1: "Deliver (i, Append i e2)  set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(17) prefix_msg_in_history)
  have f2: " mo. Deliver (i, Expunge e2 mo i)  set (history k)" using assms
    by (metis Pair_inject fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        operation.distinct(19) prefix_msg_in_history)
  have f3: "Deliver (i, Create i e2)  set (history k)" using assms
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.distinct(8) prefix_msg_in_history)
  hence "( mo1. Deliver (i, Store e2 mo1 i)  set pre)" using assms P f1 f2 imap_axioms 
    by (meson imap.Broadcast_Deliver_prefix_closed prefix_elem_to_carriers prefix_of_appendD)
  then obtain mo1 :: 'a where
    f3: "Deliver (i, Store e2 mo1 i)  set pre" by blast
  then have f4: "Deliver (i, Store e2 mo1 i)  set (history k)"
    using P prefix_elem_to_carriers by blast 
  hence "Deliver (i, Store e2 mo i)  set pre" using f2 f3 assms 
    by (metis fst_conv msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.inject(5) prefix_msg_in_history)
  moreover have "Deliver(i, Store e1 mo i)  set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast 
  ultimately show ?thesis using f4
    by (metis delivery_has_a_cause fst_conv msg_id_unique old.prod.inject operation.inject(5))
qed

lemma (in imap) create_delete_ids_imply_messages_same:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Create i e1)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e2)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast
  have f1: "Deliver (i, Append i e2)  set (history k)"
    by (metis assms(2) assms(3) delivery_has_a_cause fst_conv network.msg_id_unique 
        network.prefix_msg_in_history network_axioms operation.distinct(3) prod.inject)
  have f2: " mo. Deliver (i, Expunge e2 mo i)  set (history k)"
    by (metis assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        old.prod.inject operation.distinct(5) prefix_msg_in_history)
  have f3: " mo. Deliver (i, Store e2 mo i)  set (history k)"
    by (metis Pair_inject assms(2) assms(3) delivery_has_a_cause fst_conv msg_id_unique 
        operation.distinct(7) prefix_msg_in_history)
  hence "Deliver (i, Create i e2)  set pre" using assms P f2 f1 imap_axioms
    by (meson imap.Broadcast_Deliver_prefix_closed  prefix_elem_to_carriers prefix_of_appendD)
  then show ?thesis using f1 f2 f3
    by (metis (no_types, lifting) P assms(2) assms(3) delivery_has_a_cause fst_conv msg_id_unique 
        node_histories.prefix_of_appendD node_histories_axioms old.prod.inject operation.inject(1) 
        prefix_elem_to_carriers prefix_msg_in_history)
qed

lemma (in imap) append_delete_ids_imply_messages_same:
  assumes "i  is"
    and "xs prefix of j"
    and "(i, Append i e1)  set (node_deliver_messages xs)" 
    and "(ir, Delete is e2)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (ir, Delete is e2)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  hence f1: "e. e  set pre  e  set (history k)" using prefix_elem_to_carriers by blast
  have f2: "Deliver (i, Create i e2)  set pre" using P f1
    by (metis assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause network_axioms 
        old.prod.inject operation.distinct(3) prefix_msg_in_history)
  moreover have D1: " mo. Deliver (i, Expunge e2 mo i)  set pre" using P f1
    by (metis Pair_inject assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause 
        network_axioms operation.distinct(15) prefix_msg_in_history)
  moreover have D2: " mo. Deliver (i, Store e2 mo i)  set pre" using P f1
    by (metis Pair_inject assms(2) assms(3) fst_conv msg_id_unique network.delivery_has_a_cause 
        network_axioms operation.simps(23) prefix_msg_in_history)
  moreover hence "Deliver (i, Append i e2)  set pre" 
    using P D1 D2 f2 assms(1) Broadcast_Deliver_prefix_closed by blast
  moreover have "Deliver (i, Append i e1)  set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast
  ultimately show ?thesis using assms 
    by (metis f1 msg_id_unique network.delivery_has_a_cause network_axioms old.prod.inject 
        operation.inject(3) prod.sel(1))
qed

lemma (in imap) append_expunge_ids_imply_messages_same:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e1)  set (node_deliver_messages xs)" 
    and "(r, Expunge e2 mo r)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where pre: "pre@[Broadcast (r, Expunge e2 mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  moreover hence "Deliver (mo, Append mo e2)  set pre  
  ( mo2 . Deliver (mo, Store e2 mo2 mo)  set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1)
    by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms)      
  hence "Deliver (i, Append i e2)  set pre" using assms
    by (metis (no_types, lifting) pre delivery_has_a_cause fst_conv hb_broadcast_exists1 
        msg_id_unique network.hb_deliver network.prefix_msg_in_history network_axioms 
        node_histories.events_in_local_order node_histories_axioms operation.distinct(17) 
        prod.inject)     
  moreover have "Deliver (i, Append i e1)  set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast
  ultimately show ?thesis
    by (metis (no_types, lifting) fst_conv network.delivery_has_a_cause network.msg_id_unique 
        network_axioms operation.inject(3) prefix_elem_to_carriers prefix_of_appendD prod.inject)
qed

lemma (in imap) append_store_ids_imply_messages_same:
  assumes "i = mo"
    and "xs prefix of j"
    and "(i, Append i e1)  set (node_deliver_messages xs)" 
    and "(r, Store e2 mo r)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Store e2 mo r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  moreover hence A: "Deliver (mo, Append mo e2)  set pre  
  ( mo2 . Deliver (mo, Store e2 mo2 mo)  set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1)
    by (meson imap.Broadcast_Deliver_prefix_closed imap_axioms)
  have f1: "Deliver (i, Append i e1)  set (history j)"
    using assms(2) assms(3) prefix_msg_in_history by blast
  hence "Deliver (i, Append i e2)  set pre" using assms P A
    by (metis Pair_inject assms(1) P delivery_has_a_cause fst_conv msg_id_unique 
        operation.simps(23) prefix_elem_to_carriers prefix_of_appendD)
  then show ?thesis using f1
    by (metis P delivery_has_a_cause fst_conv msg_id_unique 
        node_histories.prefix_of_appendD node_histories_axioms operation.inject(3) 
        prefix_elem_to_carriers prod.inject)
qed

lemma (in imap) expunge_store_ids_imply_messages_same:
  assumes "xs prefix of j"
    and "(i, Store e1 mo i)  set (node_deliver_messages xs)" 
    and "(r, Expunge e2 i r)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Expunge e2 i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast 
  hence pprefix: "pre prefix of k"
    using P by blast
  have A: "Deliver (i, Append i e2)  set pre  
  ( mo2 . Deliver (i, Store e2 mo2 i)  set pre)"
    using Broadcast_Expunge_Deliver_prefix_closed assms(1) P by blast      
  have "Deliver (i, Store e2 mo i)  set pre" using assms A P
  proof -
    obtain op1 :: "'a × ('a, 'b) operation  nat" where
      f1: "Broadcast (i, Store e1 mo i)  set (history (op1 (i, Store e1 mo i)))"
      by (meson assms(1) assms(2) delivery_has_a_cause prefix_msg_in_history)
    then show ?thesis 
      using f1 A pprefix delivery_has_a_cause network.msg_id_unique network_axioms 
        node_histories.prefix_to_carriers node_histories_axioms 
      by fastforce
  qed
  moreover have "Deliver (i, Store e1 mo i)  set (history j)"
    using assms(1) assms(2) prefix_msg_in_history by auto
  ultimately show ?thesis using assms P
    by (metis delivery_has_a_cause fst_conv msg_id_unique operation.inject(5) 
        prefix_elem_to_carriers prefix_of_appendD prod.inject) 
qed

lemma (in imap) store_store_ids_imply_messages_same:
  assumes "xs prefix of j"
    and "(i, Store e1 mo i)  set (node_deliver_messages xs)" 
    and "(r, Store e2 i r)  set (node_deliver_messages xs)"
  shows "e1 = e2"
proof -
  obtain pre k where P: "pre@[Broadcast (r, Store e2 i r)] prefix of k"
    using assms delivery_has_a_cause events_before_exist prefix_msg_in_history by blast  
  moreover hence A: "Deliver (i, Append i e2)  set pre 
    ( mo2 . Deliver (i, Store e2 mo2 i)  set pre)"
    using Broadcast_Store_Deliver_prefix_closed assms(1) by blast
  have "e. e  set pre  e  set (history k)"
    using P prefix_elem_to_carriers by auto
  hence "Deliver (i, Store e2 mo i)  set pre" 
    by (metis A assms(1) assms(2) delivery_has_a_cause fst_conv msg_id_unique 
        operation.distinct(17) operation.inject(5) prefix_msg_in_history prod.inject)
  moreover have "Deliver (i, Store e1 mo i)  set (history j)"
    using assms(1) assms(2) prefix_msg_in_history by auto
  ultimately show ?thesis using assms
    by (metis Pair_inject delivery_has_a_cause msg_id_unique operation.simps(5) 
        prefix_elem_to_carriers prefix_of_appendD prod.sel(1))
qed 

end