Theory AbstractCommutativity

section ‹Soundness of CommCSL›

subsection ‹Abstract Commutativity›

theory AbstractCommutativity
  imports Main CommCSL "HOL-Library.Multiset"
begin

datatype ('i, 'a, 'b) action = Shared (get_s: 'a) | Unique (get_i: 'i) (get_u: 'b)

text ‹We consider a family of unique actions indexed by 'i›

lemma sabstract:
  assumes "all_axioms α sact spre uact upre"
  shows "α v = α v' ∧ spre sarg sarg' ⟹ α (sact v sarg) = α (sact v' sarg')"
  using all_axioms_def[of α sact spre uact upre] assms by fast

lemma uabstract:
  assumes "all_axioms α sact spre uact upre"
  shows "α v = α v' ∧ upre i uarg uarg' ⟹ α (uact i v uarg) = α (uact i v' uarg')"
  using all_axioms_def[of α sact spre uact upre] assms by fast

lemma spre_refl:
  assumes "all_axioms α sact spre uact upre"
  shows "spre sarg sarg' ⟹ spre sarg' sarg'"
  using all_axioms_def[of α sact spre uact upre] assms by fast

lemma upre_refl:
  assumes "all_axioms α sact spre uact upre"
  shows "upre i uarg uarg' ⟹ upre i uarg' uarg'"
  using all_axioms_def[of α sact spre uact upre] assms by fast

lemma ss_com:
  assumes "all_axioms α sact spre uact upre"
  shows "α v = α v' ⟹ spre sarg sarg ∧ spre sarg' sarg' ⟹ α (sact (sact v sarg) sarg') = α (sact (sact v' sarg') sarg)"
  using all_axioms_def[of α sact spre uact upre] assms by blast

lemma su_com:
  assumes "all_axioms α sact spre uact upre"
  shows "α v = α v' ⟹ spre sarg sarg ∧ upre i uarg uarg ⟹ α (sact (uact i v uarg) sarg) = α (uact i (sact v' sarg) uarg)"
  using all_axioms_def[of α sact spre uact upre] assms by blast

lemma uu_com:
  assumes "all_axioms α sact spre uact upre"
      and "i ≠ i'"
      and "α v = α v'"
      and "upre i' uarg' uarg'"
      and "upre i uarg uarg"
    shows "α (uact i' (uact i v uarg) uarg') = α (uact i (uact i' v' uarg') uarg)"
proof -
  have "⋀v v' uarg uarg' i i'.
             i ≠ i' ∧ α v = α v' ∧ upre i uarg uarg ∧ upre i' uarg' uarg' ⟶ α (uact i' (uact i v uarg) uarg') = α (uact i (uact i' v' uarg') uarg)"
  using all_axioms_def[of α sact spre uact upre] assms(1)
  by blast
  then show ?thesis
    using assms(2) assms(3) assms(4) assms(5) by blast
qed


definition PRE_shared :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
  "PRE_shared spre sargs sargs' ⟷ (∃ms. image_mset fst ms = sargs ∧ image_mset snd ms = sargs' ∧ (∀x ∈# ms. spre (fst x) (snd x)))"

lemma PRE_shared_same_size:
  assumes "PRE_shared spre sargs sargs'"
  shows "size sargs = size sargs'"
proof -
  obtain ms where "image_mset fst ms = sargs ∧ image_mset snd ms = sargs' ∧ (∀x ∈# ms. spre (fst x) (snd x))"
    by (metis PRE_shared_def assms)
  then have "size sargs = size ms ∧ size ms = size sargs'"
    by force
  then show ?thesis
    by simp
qed

definition is_Unique :: "('i, 'a, 'b) action ⇒ bool" where
  "is_Unique a ⟷ ¬ is_Shared a"

definition is_Unique_i :: "'i ⇒ ('i, 'a, 'b) action ⇒ bool" where
  "is_Unique_i i a ⟷ is_Unique a ∧ get_i a = i"

definition possible_sequence :: "'a multiset ⇒ ('i ⇒ 'b list) ⇒ ('i, 'a, 'b) action list ⇒ bool" where
  "possible_sequence sargs uargs s ⟷ ((∀i. uargs i = map get_u (filter (is_Unique_i i) s)) ∧ sargs = image_mset get_s (filter_mset is_Shared (mset s)))"

lemma possible_sequenceI:
  assumes "⋀i. uargs i = map get_u (filter (is_Unique_i i) s)"
      and "sargs = image_mset get_s (filter_mset is_Shared (mset s))"
    shows "possible_sequence sargs uargs s"
  using assms(1) assms(2) possible_sequence_def by blast

fun remove_at_index :: "nat ⇒ 'd list ⇒ 'd list" where
  "remove_at_index _ [] = []"
| "remove_at_index 0 (x # xs) = xs"
| "remove_at_index (Suc n) (x # xs) = x # (remove_at_index n xs)"

lemma remove_at_index:
  assumes "n < length l"
  shows "length (remove_at_index n l) = length l - 1"
    and "i ≥ 0 ∧ i < n ⟹ remove_at_index n l ! i = l ! i"
    and "i ≥ n ∧ i < length l - 1 ⟹ remove_at_index n l ! i = l ! (i + 1)"
  using assms
proof (induct l arbitrary: n i)
  case (Cons a l)
  {
    case 1
    then show ?case
    proof (cases n)
      case (Suc k)
      then show ?thesis
        using "1" Cons.hyps(1) by force
    qed (simp)
  next
    case 2
    then show ?case
    proof (cases n)
      case (Suc k)
      then show ?thesis
        using "2.prems"(1) "2.prems"(2) Cons.hyps(2) Suc_less_eq2 less_Suc_eq_0_disj by auto
    qed (simp)
  next
    case 3
    then show ?case
    proof (cases n)
      case (Suc k)
      then have "remove_at_index (Suc k) (a # l) ! i = (a # l) ! (i + 1)"
        apply (cases i)
        using "3.prems"(1) apply blast
        using "3.prems"(1) Cons.hyps(3) Suc_less_eq2 by auto
      then show "remove_at_index n (a # l) ! i = (a # l) ! (i + 1)"
        using Suc by blast
    qed (simp)
  }
qed (auto)

fun insert_at :: "nat ⇒ 'd ⇒ 'd list ⇒ 'd list" where
  "insert_at 0 x l = x # l"
| "insert_at _ x [] = [x]"
| "insert_at (Suc n) x (h # xs) = h # (insert_at n x xs)"

lemma insert_at_index:
  assumes "n ≤ length l"
  shows "length (insert_at n x l) = length l + 1"
    and "i ≥ 0 ∧ i < n ⟹ insert_at n x l ! i = l ! i"
    and "n ≥ 0 ⟹ insert_at n x l ! n = x"
    and "i > n ∧ i < length l + 1 ⟹ insert_at n x l ! i = l ! (i - 1)"
  using assms
proof (induct l arbitrary: n i)
  case (Cons a l)
  {
    case 1
    then show ?case by (cases n) (simp_all add: Cons.hyps(1))
  next
    case 2
    then show ?case apply (cases n)
       apply blast
      using Cons.hyps(2) less_Suc_eq_0_disj by force
  next
    case 3
    then show ?case apply (cases n)
       apply simp
      by (simp add: Cons.hyps(3))
  next
    case 4
    then show ?case apply (cases n)
       apply simp
      by (metis (no_types, lifting) "4.prems"(1) "4.prems"(2) Cons.hyps(4) Nat.add_0_right One_nat_def Suc_le_length_iff Suc_less_eq Suc_pred add_Suc_right bot_nat_0.not_eq_extremum insert_at.simps(3) less_zeroE list.inject list.size(4) nat.simps(3) nth_Cons' nth_Cons_Suc)
  }
qed (simp_all)

lemma list_ext:
  assumes "length a = length b"
      and "⋀i. i ≥ 0 ∧ i < length a ⟹ a ! i = b ! i"
    shows "a = b"
  by (meson assms(1) assms(2) bot_nat_0.extremum nth_equalityI)

lemma mset_remove_index:
  assumes "i ≥ 0 ∧ i < length l"
  shows "mset l = mset (remove_at_index i l) + {# l ! i #}"
  using assms
proof (induct l arbitrary: i)
  case (Cons a l)
  then show ?case
  proof (cases i)
    case (Suc k)
    then show ?thesis
      using Cons.hyps Cons.prems by force
  qed (auto)
qed (simp)

lemma filter_remove:
  assumes "k ≥ 0 ∧ k < length s"
      and "¬ P (s ! k)"
    shows "filter P (remove_at_index k s) = filter P s"
  using assms
proof (induct k arbitrary: s)
  case 0
  then have "s = hd s # tl s"
    by simp
  then show ?case
    by (metis "0.prems"(2) filter.simps(2) nth_Cons_0 remove_at_index.simps(2))
next
  case (Suc k)
  then show ?case
    by (cases s) simp_all
qed

lemma exists_index_in_sequence_shared:
  assumes "a ∈# sargs"
      and "possible_sequence sargs uargs s"
    shows "∃i. i ≥ 0 ∧ i < length s ∧ s ! i = Shared a ∧ possible_sequence (sargs - {# a #}) uargs (remove_at_index i s)"
proof -
  have "a ∈# image_mset get_s (filter_mset is_Shared (mset s))"
    by (metis assms(1) assms(2) possible_sequence_def)
  then have "Shared a ∈ set s"
    by fastforce
  then obtain i where "i ≥ 0 ∧ i < length s ∧ s ! i = Shared a"
    by (meson bot_nat_0.extremum in_set_conv_nth)
  let ?s = "remove_at_index i s"
  have "sargs - {# a #} = image_mset get_s (filter_mset is_Shared (mset ?s))"
  proof -
    have "sargs = image_mset get_s (filter_mset is_Shared (mset s))"
      using possible_sequence_def assms(2) by blast
    moreover have "mset s = mset ?s + {# Shared a #}"
      by (metis ‹0 ≤ i ∧ i < length s ∧ s ! i = Shared a› mset_remove_index)
    ultimately show ?thesis
      by simp
  qed
  moreover have "⋀i. uargs i = map get_u (filter (is_Unique_i i) ?s)"
    by (metis ‹0 ≤ i ∧ i < length s ∧ s ! i = Shared a› action.disc(1) assms(2) filter_remove is_Unique_def is_Unique_i_def possible_sequence_def)
  ultimately show ?thesis
    using ‹0 ≤ i ∧ i < length s ∧ s ! i = Shared a› possible_sequence_def by blast
qed

lemma head_possible_exists_first_unique:
  assumes "a = hd (uargs j)"
      and "uargs j ≠ []"
      and "possible_sequence sargs uargs s"
    shows "∃i. i ≥ 0 ∧ i < length s ∧ s ! i = Unique j a ∧ (∀k. k ≥ 0 ∧ k < i ⟶ ¬ is_Unique_i j (s ! k))"
  using assms
proof (induct s arbitrary: sargs uargs)
  case Nil
  then show ?case by (simp add: possible_sequence_def)
next
  case (Cons x xs)
  then show "∃i≥0. i < length (x # xs) ∧ (x # xs) ! i = Unique j a ∧ (∀k. 0 ≤ k ∧ k < i ⟶ ¬ is_Unique_i j ((x # xs) ! k))"
  proof (cases x)
    case (Shared sarg)
    moreover have "possible_sequence (sargs - {# sarg #}) uargs xs"
    proof (rule possible_sequenceI)
      show "sargs - {#sarg#} = image_mset get_s (filter_mset is_Shared (mset xs))"
        using Cons.prems(3) action.disc(1) action.sel(1) add_mset_remove_trivial[of sarg ]
          calculation
          filter_mset_add_mset image_mset_add_mset mset.simps(2) possible_sequence_def[of sargs uargs "x # xs"]
        by auto
      fix i show "uargs i = map get_u (filter (is_Unique_i i) xs)"
        using Cons.prems(3) action.disc(1) calculation filter_remove is_Unique_def is_Unique_i_def
          le_numeral_extra(3) length_greater_0_conv list.discI nth_Cons_0 possible_sequence_def[of sargs uargs "x # xs"]
          remove_at_index.simps(2)
        by metis
    qed
    then obtain i where "i ≥ 0 ∧ i < length xs ∧ xs ! i = Unique j a ∧ (∀k. 0 ≤ k ∧ k < i ⟶ ¬ is_Unique_i j (xs ! k))"
      using Cons.hyps[of uargs] Cons.prems(1) Cons.prems(2) by auto
    moreover have "⋀k. 0 ≤ k ∧ k < i + 1 ⟶ ¬ is_Unique_i j ((x # xs) ! k)"
    proof 
      fix k assume "0 ≤ k ∧ k < i + 1"
      then show "¬ is_Unique_i j ((x # xs) ! k)"
        apply (cases k)
         apply (simp add: Shared is_Unique_def is_Unique_i_def)
        by (simp add: calculation(2))
    qed
    ultimately show ?thesis
      by (metis Suc_eq_plus1 Suc_less_eq bot_nat_0.extremum length_Cons nth_Cons_Suc)
  next
    case (Unique k uarg)
    then show ?thesis
    proof (cases "j = k")
      case True
      then have "uargs j = map get_u (filter (is_Unique_i j) (x # xs))"
        by (meson Cons.prems(3) possible_sequence_def)
      then have "uarg = a"
        by (simp add: True Unique Cons.prems(1) is_Unique_def is_Unique_i_def)
      then show ?thesis
        using True Unique by fastforce
    next
      case False
      moreover have "possible_sequence sargs (uargs(k := tl (uargs k))) xs"
      proof (rule possible_sequenceI)
        show "sargs = image_mset get_s (filter_mset is_Shared (mset xs))"
          by (metis (mono_tags, lifting) Cons.prems(3) Unique action.disc(2) filter_mset_add_mset mset.simps(2) possible_sequence_def)
        fix i show "(uargs(k := tl (uargs k))) i = map get_u (filter (is_Unique_i i) xs)"
        proof (cases "i = k")
          case True
          then show ?thesis
            using Cons.prems(3) Unique action.disc(2) action.sel(2) filter.simps(2) fun_upd_same
              is_Unique_def is_Unique_i_def list.sel(3) map_tl possible_sequence_def[of sargs uargs "x # xs"]
            by metis
        next
          case False
          then show ?thesis
            using Cons.prems(3) Unique action.sel(2) filter_remove fun_upd_apply is_Unique_i_def
            le_numeral_extra(3) length_greater_0_conv list.discI nth_Cons_0 possible_sequence_def[of sargs uargs "x # xs"]
            remove_at_index.simps(2) by metis
        qed
      qed
      then obtain i where "i ≥ 0 ∧ i < length xs ∧ xs ! i = Unique j a ∧ (∀k. 0 ≤ k ∧ k < i ⟶ ¬ is_Unique_i j (xs ! k))"
        by (metis Cons.hyps Cons.prems(1) Cons.prems(2) calculation fun_upd_other)
      moreover have "⋀k. 0 ≤ k ∧ k < i + 1 ⟶ ¬ is_Unique_i j ((x # xs) ! k)"
      proof 
        fix k assume "0 ≤ k ∧ k < i + 1"
        then show "¬ is_Unique_i j ((x # xs) ! k)"
          apply (cases k)
           apply (metis False Unique action.sel(2) is_Unique_i_def nth_Cons_0)
          by (simp add: calculation(2))
      qed
      ultimately show ?thesis
        by (metis Suc_eq_plus1 Suc_less_eq bot_nat_0.extremum length_Cons nth_Cons_Suc)
    qed
  qed
qed

lemma remove_at_index_filter:
  assumes "i ≥ 0 ∧ i < length s ∧ P (s ! i)"
      and "⋀j. j ≥ 0 ∧ j < i ⟹ ¬ P (s ! j)"
    shows "tl (map get_u (filter P s)) = map get_u (filter P (remove_at_index i s))"
  using assms
proof (induct s arbitrary: i)
  case (Cons a s)
  then show ?case
  proof (cases i)
    case 0
    then show ?thesis
      using Cons.prems(1) by auto
  next
    case (Suc k)
    then have "tl (map get_u (filter P s)) = map get_u (filter P (remove_at_index k s))"
      apply (cases s)
       apply simp
      by (metis Cons.hyps Cons.prems(1) Cons.prems(2) Suc_less_eq bot_nat_0.extremum length_Cons nth_Cons_Suc)
    then show ?thesis
      by (metis Cons.prems(2) Suc bot_nat_0.extremum filter.simps(2) nth_Cons_0 remove_at_index.simps(3) zero_less_Suc)
  qed
qed (simp)

definition tail_kth where
  "tail_kth uargs k = uargs(k := tl (uargs k))"

lemma exists_index_in_sequence_unique:
  assumes "a = hd (uargs k)"
      and "uargs k ≠ []"
      and "possible_sequence sargs uargs s"
    shows "∃i. i ≥ 0 ∧ i < length s ∧ s ! i = Unique k a ∧ possible_sequence sargs (tail_kth uargs k) (remove_at_index i s)
          ∧ (∀j. j ≥ 0 ∧ j < i ⟶ ¬ is_Unique_i k (s ! j))"
proof -
  obtain i where "i ≥ 0 ∧ i < length s ∧ s ! i = Unique k a ∧ (∀j. j ≥ 0 ∧ j < i ⟶ ¬ is_Unique_i k (s ! j))"
    by (metis assms(1) assms(2) assms(3) head_possible_exists_first_unique)
  let ?s = "remove_at_index i s"
  have "sargs = image_mset get_s (filter_mset is_Shared (mset ?s))" 
    by (metis ‹0 ≤ i ∧ i < length s ∧ s ! i = Unique k a ∧ (∀j. 0 ≤ j ∧ j < i ⟶ ¬ is_Unique_i k (s ! j))› action.disc(2) add.right_neutral assms(3) filter_single_mset filter_union_mset mset_remove_index possible_sequence_def)
  moreover have "tl (uargs k) = map get_u (filter (is_Unique_i k) ?s)"
  proof -
    have "uargs k = map get_u (filter (is_Unique_i k) s)"
      by (meson assms(3) possible_sequence_def)
    then show ?thesis
      by (metis ‹0 ≤ i ∧ i < length s ∧ s ! i = Unique k a ∧ (∀j. 0 ≤ j ∧ j < i ⟶ ¬ is_Unique_i k (s ! j))› action.disc(2) action.sel(2) is_Unique_def is_Unique_i_def remove_at_index_filter)
  qed
  moreover have "possible_sequence sargs (tail_kth uargs k) (remove_at_index i s)"
  proof (rule possible_sequenceI)
    show "sargs = image_mset get_s (filter_mset is_Shared (mset (remove_at_index i s)))"
      by (simp add: calculation(1))
    fix ia show "tail_kth uargs k ia = map get_u (filter (is_Unique_i ia) (remove_at_index i s))"
      by (metis (mono_tags, lifting) ‹0 ≤ i ∧ i < length s ∧ s ! i = Unique k a ∧ (∀j. 0 ≤ j ∧ j < i ⟶ ¬ is_Unique_i k (s ! j))› action.sel(2) assms(3) calculation(2) filter_remove fun_upd_other fun_upd_same is_Unique_i_def possible_sequence_def tail_kth_def)
  qed
  ultimately show ?thesis
    using ‹0 ≤ i ∧ i < length s ∧ s ! i = Unique k a ∧ (∀j. 0 ≤ j ∧ j < i ⟶ ¬ is_Unique_i k (s ! j))› by blast
qed

lemma possible_sequence_where_is_unique:
  assumes "possible_sequence sargs uargs (Unique k a # s)"
  shows "a = hd (uargs k)"
proof -
  let ?s = "Unique k a # s"
  have "Unique k a = hd (filter is_Unique ?s)"
    by (simp add: is_Unique_def)
  then have "a = hd (map get_u (filter is_Unique ?s))"
    by (simp add: is_Unique_def)
  then show ?thesis
    using action.disc(2) action.sel(2) assms filter.simps(2) hd_map is_Unique_def
      is_Unique_i_def list.discI list.sel(1) possible_sequence_def[of sargs uargs "Unique k a # s"]
    by metis
qed

lemma possible_sequence_where_is_shared:
  assumes "possible_sequence sargs uargs (Shared a # s)"
  shows "a ∈# sargs"
proof -
  let ?s = "Shared a # s"
  have "a ∈ set (map get_s (filter is_Shared ?s))"
    by simp
  then show ?thesis
    by (metis (no_types, lifting) assms mset_filter mset_map possible_sequence_def set_mset_mset)
qed


lemma PRE_unique_tlI:
  assumes "PRE_unique upre qa qb"
      and "upre ta tb"
    shows "PRE_unique upre (ta # qa) (tb # qb)"
proof (rule PRE_uniqueI)
  show "length (ta # qa) = length (tb # qb)"
    using PRE_unique_def assms(1) by auto
  fix i
  show "0 ≤ i ∧ i < length (tb # qb) ⟹ upre ((ta # qa) ! i) ((tb # qb) ! i)"
  proof (cases i)
    case 0
    then show ?thesis
      using assms(2) by auto
  next
    case (Suc k)
    assume "0 ≤ i ∧ i < length (tb # qb)"
    then have "(ta # qa) ! i = qa ! k ∧ (tb # qb) ! i = qb ! k"
      by (simp add: Suc)
    then show ?thesis using assms(1) PRE_unique_def
      using Suc ‹0 ≤ i ∧ i < length (tb # qb)› by auto
  qed
qed

fun abstract_pre :: "('a ⇒ 'a ⇒ bool) ⇒ ('i ⇒ 'b ⇒ 'b ⇒ bool) ⇒ ('i, 'a, 'b) action ⇒ ('i, 'a, 'b) action ⇒ bool" where
  "abstract_pre spre upre (Shared sarg) (Shared sarg') ⟷ spre sarg sarg'"
| "abstract_pre spre upre (Unique k uarg) (Unique k' uarg') ⟷ k = k' ∧ upre k uarg uarg'"
| "abstract_pre spre upre _ _ ⟷ False"

definition PRE_sequence :: "('a ⇒ 'a ⇒ bool) ⇒ ('i => 'b ⇒ 'b ⇒ bool) ⇒ ('i, 'a, 'b) action list ⇒ ('i, 'a, 'b) action list ⇒ bool" where
  "PRE_sequence spre upre s s' ⟷ length s = length s' ∧ (∀i. i ≥ 0 ∧ i < length s ⟶ abstract_pre spre upre (s ! i) (s' ! i))"

lemma PRE_sequenceE:
  assumes "PRE_sequence spre upre s s'"
      and "i ≥ 0 ∧ i < length s"
    shows "abstract_pre spre upre (s ! i) (s' ! i)"
  using PRE_sequence_def assms(1) assms(2) by blast

lemma PRE_sequenceI:
  assumes "length s = length s'"
      and "⋀i. i ≥ 0 ∧ i < length s ⟹ abstract_pre spre upre (s ! i) (s' ! i)"
    shows "PRE_sequence spre upre s s'"
  by (simp add: PRE_sequence_def assms(1) assms(2))

lemma PRE_sequenceI_rec:
  assumes "PRE_sequence spre upre s s'"
      and "abstract_pre spre upre a b"
    shows "PRE_sequence spre upre (a # s) (b # s')"
  using PRE_sequence_def[of spre upre "a # s" "b # s'"] PRE_sequence_def[of spre upre s s']
  assms(1) assms(2) less_Suc_eq_0_disj length_Cons less_Suc_eq_le nth_Cons_0 nth_Cons_Suc
  by force
  
lemma PRE_sequenceE_rec:
  assumes "PRE_sequence spre upre (a # s) (b # s')"
  shows "PRE_sequence spre upre s s'"
      and "abstract_pre spre upre a b"
  using PRE_sequence_def[of spre upre "a # s" "b # s'"] PRE_sequence_def[of spre upre s s']
  apply (metis Suc_less_eq assms bot_nat_0.extremum diff_Suc_1 length_Cons nth_Cons_Suc)
  by (metis PRE_sequenceE assms length_Cons list.size(3) nth_Cons_0 remdups_adj.simps(1) remdups_adj_length zero_less_Suc)

fun compute :: "('v ⇒ 'a ⇒ 'v) ⇒ ('i ⇒ 'v ⇒ 'b ⇒ 'v) ⇒ 'v ⇒ ('i, 'a, 'b) action list ⇒ 'v" where
  "compute sact uact v0 [] = v0"
| "compute sact uact v0 (Shared sarg # s) = sact (compute sact uact v0 s) sarg"
| "compute sact uact v0 (Unique k uarg # s) = uact k (compute sact uact v0 s) uarg"


lemma obtain_other_elem_ms:
  assumes "PRE_shared spre sargs sargs'"
      and "sarg ∈# sargs"
    shows "∃sarg'. sarg' ∈# sargs' ∧ spre sarg sarg' ∧ PRE_shared spre (sargs - {# sarg #}) (sargs' - {# sarg' #})"
proof -
  obtain ms where asm: "image_mset fst ms = sargs ∧ image_mset snd ms = sargs' ∧ (∀x ∈# ms. spre (fst x) (snd x))"
    using PRE_shared_def assms(1) by blast
  then obtain x where "x ∈# ms" "fst x = sarg"
    using assms(2) by auto
  then have "snd x ∈# sargs' ∧ spre sarg (snd x)"
    using asm by force
  moreover have "PRE_shared spre (sargs - {# sarg #}) (sargs' - {# snd x #})"
  proof -
    let ?ms = "ms - {# x #}"
    have "image_mset fst ?ms = (sargs - {# sarg #}) ∧ image_mset snd ?ms = (sargs' - {# snd x #})"
      by (simp add: ‹fst x = sarg› ‹x ∈# ms› asm image_mset_Diff)
    moreover have "⋀y. y ∈# ?ms ⟹ spre (fst y) (snd y)"
      by (meson asm in_diffD)
    ultimately show ?thesis
      using PRE_shared_def by blast
  qed
  ultimately show ?thesis
    by blast
qed

lemma exists_aligned_sequence:
  assumes "possible_sequence sargs uargs s"
      and "possible_sequence sargs' uargs' s'"

      and "PRE_shared spre sargs sargs'"
      and "⋀k. PRE_unique (upre k) (uargs k) (uargs' k)"

    shows "∃s''. possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre s s''"
  using assms
proof (induct s arbitrary: sargs uargs sargs' uargs' s')
  case Nil
  then have "sargs = mset [] ∧ (∀k. uargs k = [])"
    by (simp add: possible_sequence_def)
  then have "sargs' = {#} ∧ (∀k. uargs' k = [])"
    by (metis Nil.prems(3) Nil.prems(4) PRE_shared_same_size PRE_unique_def length_0_conv mset.simps(1) size_eq_0_iff_empty)
  then show "∃s''. possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre [] s''"
    by (simp add: PRE_sequence_def possible_sequence_def)
next
  case (Cons act s)

  show "∃s''. possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre (act # s) s''"
  proof (cases act)
    case (Shared sarg)

    then have "sarg ∈# sargs"
      by (metis Cons.prems(1) possible_sequence_where_is_shared)
    then obtain sarg' where "sarg' ∈# sargs'" "spre sarg sarg'" "PRE_shared spre (sargs - {# sarg #}) (sargs' - {# sarg' #})"
      by (metis Cons.prems(3) obtain_other_elem_ms)
    let ?sargs = "sargs - {# sarg #}"
    let ?sargs' = "sargs' - {# sarg' #}"
    have "possible_sequence ?sargs uargs s"
    proof (rule possible_sequenceI)
      show "⋀i. uargs i = map get_u (filter (is_Unique_i i) s)"
        using Cons.prems(1) Shared action.disc(1) filter.simps(2) is_Unique_def is_Unique_i_def
          possible_sequence_def[of sargs uargs "act # s"]
        by metis
      have "sargs = image_mset get_s (filter_mset is_Shared (mset(Shared sarg # s)))"
        using Cons.prems(1) Shared possible_sequence_def by blast
      then show "sargs - {#sarg#} = image_mset get_s (filter_mset is_Shared (mset s))" by simp
    qed

    obtain i where "i ≥ 0 ∧ i < length s' ∧ s' ! i = Shared sarg' ∧ possible_sequence ?sargs' uargs' (remove_at_index i s')"
      by (meson Cons.prems(2) ‹sarg' ∈# sargs'› exists_index_in_sequence_shared)
    
    then obtain s'' where "possible_sequence ?sargs' uargs' s'' ∧ PRE_sequence spre upre s s''"
      using Cons.hyps Cons.prems(4) ‹PRE_shared spre (sargs - {#sarg#}) (sargs' - {#sarg'#})› ‹possible_sequence (sargs - {#sarg#}) uargs s› by blast

    let ?s'' = "Shared sarg' # s''"

    have "possible_sequence sargs' uargs' ?s''"
    proof (rule possible_sequenceI)
      show "⋀i. uargs' i = map get_u (filter (is_Unique_i i) (Shared sarg' # s''))"
        by (metis ‹possible_sequence (sargs' - {#sarg'#}) uargs' s'' ∧ PRE_sequence spre upre s s''› action.disc(1) filter.simps(2) is_Unique_def is_Unique_i_def possible_sequence_def)
      show "sargs' = image_mset get_s (filter_mset is_Shared (mset (Shared sarg' # s'')))"
        using ‹possible_sequence (sargs' - {#sarg'#}) uargs' s'' ∧ PRE_sequence spre upre s s''› ‹sarg' ∈# sargs'›
          insert_DiffM[of sarg' sargs'] possible_sequence_def[of "sargs' - {#sarg'#}" uargs' s'']
          action.disc(1) action.sel(1) filter_mset_add_mset msed_map_invL mset.simps(2)
        by auto
    qed

    moreover have "PRE_sequence spre upre (act # s) ?s''"
      by (simp add: PRE_sequenceI_rec Shared ‹possible_sequence (sargs' - {#sarg'#}) uargs' s'' ∧ PRE_sequence spre upre s s''› ‹spre sarg sarg'›)

    ultimately show "∃s''. possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre (act # s) s''" by auto
  next
    case (Unique k uarg)
    then have "hd (uargs k) = uarg"
      by (metis Cons.prems(1) possible_sequence_where_is_unique)
    moreover have "uargs k ≠ []"
      by (metis (no_types, lifting) Cons.prems(1) Unique action.disc(2) action.sel(2) dropWhile_eq_Cons_conv dropWhile_eq_self_iff filter.simps(2) is_Unique_def is_Unique_i_def list.map_disc_iff possible_sequence_def)
    ultimately have "uargs k = uarg # tl (uargs k)"
      by fastforce
    moreover have "uargs' k = hd (uargs' k) # tl (uargs' k)"
      by (metis Cons.prems(4) PRE_unique_def calculation length_Cons list.exhaust_sel list.size(3) nat.simps(3))
    ultimately have "upre k uarg (hd (uargs' k))"
      by (metis Cons.prems(4) PRE_unique_def length_greater_0_conv list.simps(3) list.size(3) nth_Cons_0 remdups_adj.simps(1) remdups_adj_length)
    moreover have "PRE_unique (upre k) (tl (uargs k)) (tl (uargs' k))"
      by (metis Cons.prems(4) PRE_unique_implies_tl ‹uargs k = uarg # tl (uargs k)› ‹uargs' k = hd (uargs' k) # tl (uargs' k)›)
    moreover have "possible_sequence sargs (tail_kth uargs k) s"
    proof (rule possible_sequenceI)
      show "⋀i. tail_kth uargs k i = map get_u (filter (is_Unique_i i) s)"
      proof -
        fix i 
        obtain ii where asms: "ii ≥ 0" "ii < length (act # s) ∧
           (act # s) ! ii = Unique k uarg ∧
           possible_sequence sargs (tail_kth uargs k) (remove_at_index ii (act # s)) ∧ (∀j. 0 ≤ j ∧ j < ii ⟶ ¬ is_Unique_i k ((act # s) ! j))"
          by (metis Cons.prems(1) ‹hd (uargs k) = uarg› ‹uargs k ≠ []› exists_index_in_sequence_unique)
        then show "tail_kth uargs k i = map get_u (filter (is_Unique_i i) s)"
          by (metis Unique action.disc(2) action.sel(2) bot_nat_0.extremum bot_nat_0.not_eq_extremum is_Unique_def is_Unique_i_def nth_Cons_0 possible_sequence_def remove_at_index.simps(2))
      qed
      show "sargs = image_mset get_s (filter_mset is_Shared (mset s))"
        by (metis (mono_tags, lifting) Cons.prems(1) Unique action.disc(2) filter_mset_add_mset mset.simps(2) possible_sequence_def)
    qed
    let ?uarg' = "hd (uargs' k)"
    
    obtain i where "i ≥ 0 ∧ i < length s' ∧ s' ! i = Unique k ?uarg' ∧ possible_sequence sargs' (tail_kth uargs' k) (remove_at_index i s')"
      by (metis Cons.prems(2) ‹uargs' k = hd (uargs' k) # tl (uargs' k)› exists_index_in_sequence_unique list.discI)
    then obtain s'' where "possible_sequence sargs' (tail_kth uargs' k) s'' ∧ PRE_sequence spre upre s s''"
      using Cons.hyps[of sargs "tail_kth uargs k" sargs' "tail_kth uargs' k"] Cons.prems(3) ‹possible_sequence sargs (tail_kth uargs k) s› calculation(2)
        Cons.prems(4) fun_upd_other fun_upd_same tail_kth_def
      by metis

    let ?s'' = "Unique k (hd (uargs' k)) # s''" 
    have "PRE_sequence spre upre (act # s) ?s''"
      by (simp add: PRE_sequenceI_rec Unique ‹possible_sequence sargs' (tail_kth uargs' k) s'' ∧ PRE_sequence spre upre s s''› calculation(1))
    moreover have "possible_sequence sargs' uargs' ?s''"
    proof (rule possible_sequenceI)
      show "⋀i. uargs' i = map get_u (filter (is_Unique_i i) (Unique k (hd (uargs' k)) # s''))"
      proof -
        fix i
        obtain ii where ii_def: "ii ≥ 0 ∧ ii < length s' ∧
       s' ! ii = Unique k (hd (uargs' k)) ∧
       possible_sequence sargs' (tail_kth uargs' k) (remove_at_index ii s') ∧ (∀j. 0 ≤ j ∧ j < ii ⟶ ¬ is_Unique_i k (s' ! j))"
          by (metis Cons.prems(2) ‹uargs' k = hd (uargs' k) # tl (uargs' k)› exists_index_in_sequence_unique list.discI)
        then show "uargs' i = map get_u (filter (is_Unique_i i) (Unique k (hd (uargs' k)) # s''))"
          using filter_remove[of ii s' "is_Unique_i i"] remove_at_index_filter[of ii s' "is_Unique_i i"]
            Cons.prems(2) ‹possible_sequence sargs' (tail_kth uargs' k) s'' ∧ PRE_sequence spre upre s s''›
            ‹uargs' k = hd (uargs' k) # tl (uargs' k)› action.sel(2) action.sel(3)
            filter.simps(2)[of "is_Unique_i i" "Unique k (hd (uargs' k))" s'']
             is_Unique_i_def list.simps(9)[of get_u]
            possible_sequence_def[of sargs' "tail_kth uargs' k" "remove_at_index ii s'"]
            possible_sequence_def[of sargs' uargs' s']
            possible_sequence_def[of sargs' "tail_kth uargs' k" s''] ii_def
          by metis
      qed
      show "sargs' = image_mset get_s (filter_mset is_Shared (mset (Unique k (hd (uargs' k)) # s'')))"
        using ‹possible_sequence sargs' (tail_kth uargs' k) s'' ∧ PRE_sequence spre upre s s''› possible_sequence_def by auto
    qed
    ultimately show "∃s''. possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre (act # s) s''" by blast
  qed
qed

lemma insert_remove_same_list:
  assumes "k ≥ 0 ∧ k < length s"
      and "s ! k = x"
  shows "s = insert_at k x (remove_at_index k s)"
proof (rule list_ext)
  show "length s = length (insert_at k x (remove_at_index k s))"
    by (metis One_nat_def Suc_pred add.commute assms(1) insert_at_index(1) length_greater_0_conv less_Suc_eq_le linorder_not_le list.size(3) plus_1_eq_Suc remove_at_index(1))
  fix i assume asm0: "0 ≤ i ∧ i < length s"
  show "s ! i = insert_at k x (remove_at_index k s) ! i"
  proof (cases "i < k")
    case True
    then show ?thesis
      by (metis (no_types, lifting) One_nat_def Suc_pred asm0 assms(1) insert_at_index(2) less_Suc_eq_le order_le_less_trans remove_at_index(1) remove_at_index(2))
  next
    case False
    then have "i ≥ k" by simp
    then show ?thesis
    proof (cases "i = k")
      case True
      then show ?thesis
        by (metis (no_types, lifting) One_nat_def Suc_pred assms(1) assms(2) insert_at_index(3) less_Suc_eq_le order_le_less_trans remove_at_index(1))
    next
      case False
      then have "i > k"
        using ‹k ≤ i› nless_le by blast
      then show "s ! i = insert_at k x (remove_at_index k s) ! i"
        apply (cases i)
         apply blast
        using Groups.add_ac(2) One_nat_def Suc_less_eq Suc_pred asm0 assms(1)
          insert_at_index(4)[of k _ i x]
          less_Suc_eq_le order_le_less_trans plus_1_eq_Suc remove_at_index(1)[of k s]
          remove_at_index(3)[of k s  ]
        by fastforce
    qed
  qed
qed

lemma swap_works:
  assumes "length s = length s'"
      and "k < length s - 1"
      and "⋀i. i ≥ 0 ∧ i < length s ∧ i ≠ k ∧ i ≠ k + 1 ⟹ s ! i = s' ! i"
      and "s ! k = s' ! (k + 1)"
      and "s' ! k = s ! (k + 1)"
      and "PRE_sequence spre upre s s"
      and "α v0 = α v0'"
      and "¬ (∃k'. is_Unique_i k' (s ! k) ∧ is_Unique_i k' (s ! (k + 1)))"
      and "all_axioms α sact spre uact upre"
    shows "α (compute sact uact v0 s) = α (compute sact uact v0' s')" (is "?A = ?B")
  using assms
proof (induct k arbitrary: s s')
  case 0
  then obtain x1 x2 xs where "s = x1 # x2 # xs"
    by (metis Suc_length_conv Suc_pred add_0 le_add_diff_inverse less_diff_conv less_imp_le_nat plus_1_eq_Suc)
  then have "hd s' = x2"
    by (metis "0.prems"(1) "0.prems"(2) "0.prems"(5) One_nat_def add_0 hd_conv_nth length_greater_0_conv length_tl list.sel(2) nth_Cons_0 nth_Cons_Suc)
  moreover have "hd (tl s') = x1"
    by (metis "0.prems"(1) "0.prems"(2) "0.prems"(4) Suc_eq_plus1 ‹s = x1 # x2 # xs› hd_conv_nth length_greater_0_conv length_tl nth_Cons_0 nth_tl)
  ultimately obtain xs' where "s' = x2 # x1 # xs'"
    by (metis "0.prems"(1) "0.prems"(2) length_greater_0_conv length_tl list.collapse list.sel(2))
  moreover have "xs = xs'"
  proof (rule list_ext)
    show "length xs = length xs'"
      using "0.prems"(1) ‹s = x1 # x2 # xs› calculation by auto
    fix i assume "0 ≤ i ∧ i < length xs"
    then show "xs ! i = xs' ! i"
      by (metis "0.prems"(3) Suc_eq_plus1 Suc_less_eq ‹s = x1 # x2 # xs› bot_nat_0.extremum calculation diff_Suc_1 length_Cons nat.simps(3) nth_Cons_Suc)
  qed
  have "PRE_sequence spre upre xs xs"
    apply (cases x1) apply (cases x2)
    using "0.prems"(6) ‹s = x1 # x2 # xs› PRE_sequenceE_rec(1) by blast+
  then have "α (compute sact uact v0 xs) = α (compute sact uact v0' xs)"
    using assms(7)
  proof (induct xs)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    then have "α (compute sact uact v0 xs) = α (compute sact uact v0' xs)"
      using PRE_sequenceE_rec(1) by blast
    then show "α (compute sact uact v0 (a # xs)) = α (compute sact uact v0' (a # xs))"
    proof (cases a)
      case (Shared x1)
      then show ?thesis
        by (metis ‹all_axioms α sact spre uact upre› Cons.prems(1) PRE_sequenceE_rec(2) ‹α (compute sact uact v0 xs) = α (compute sact uact v0' xs)› abstract_pre.simps(1) compute.simps(2) sabstract)
    next
      case (Unique x2)
      then show ?thesis
        by (metis ‹all_axioms α sact spre uact upre› Cons.prems(1) PRE_sequenceE_rec(2) ‹α (compute sact uact v0 xs) = α (compute sact uact v0' xs)› abstract_pre.simps(2) compute.simps(3) uabstract)
    qed
  qed
  then show ?case
  proof (cases x1)
    case (Shared sarg1)
    then have "x1 = Shared sarg1" by simp
    then show ?thesis
    proof (cases x2)
      case (Shared sarg2)
      then show "α (compute sact uact v0 s) = α (compute sact uact v0' s')"
        using ‹all_axioms α sact spre uact upre› "0.prems"(2) "0.prems"(5) "0.prems"(6) One_nat_def
          PRE_sequenceE_rec(2)[of spre upre x1 "x2 # xs" x1 "x2 # xs"]
          PRE_sequence_def[of spre upre s s] Suc_eq_plus1
          ‹α (compute sact uact v0 xs) = α (compute sact uact v0' xs)› ‹s = x1 # x2 # xs›
          ‹x1 = Shared sarg1› ‹xs = xs'›
          abstract_pre.simps(1)[of spre upre sarg2 sarg2]
          abstract_pre.simps(1)[of spre upre sarg1 sarg1]
          calculation compute.simps(2)[of sact uact v0]
          calculation compute.simps(2)[of sact uact v0']
          nth_Cons_0 ss_com[of α sact spre uact upre] zero_less_diff zero_less_one_class.zero_le_one
        by metis
    next
      case (Unique uarg2)
      then show ?thesis
        using ‹all_axioms α sact spre uact upre› "0.prems"(6) PRE_sequenceE_rec(1)[of spre upre x1 "x2 # xs" x1 "x2 # xs"]
          PRE_sequenceE_rec(2)[of spre upre ]
          Shared ‹α (compute sact uact v0 xs) = α (compute sact uact v0' xs)› ‹s = x1 # x2 # xs› ‹xs = xs'›
          abstract_pre.simps(1)[of spre upre] abstract_pre.simps(2)[of spre upre] calculation
          compute.simps(2)[of sact uact ] compute.simps(3)[of sact uact]
          su_com[of α sact spre uact upre]
        by metis
    qed
  next
    case (Unique k1 uarg1)
    then have "x1 = Unique k1 uarg1" by simp
    then show ?thesis
    proof (cases x2)
      case (Shared sarg2)
      then have "spre sarg2 sarg2 ∧ upre k1 uarg1 uarg1"
        by (metis "0.prems"(6) PRE_sequenceE_rec(1) PRE_sequenceE_rec(2) Unique ‹s = x1 # x2 # xs› abstract_pre.simps(1) abstract_pre.simps(2))
      then show ?thesis
      using ‹all_axioms α sact spre uact upre› Unique ‹α (compute sact uact v0 xs) = α (compute sact uact v0' xs)›
        ‹s = x1 # x2 # xs› ‹s' = x2 # x1 # xs'› ‹xs = xs'› compute.simps(2)[of sact uact]
        compute.simps(3)[of sact uact] su_com[of α sact spre uact upre]
      by (metis Shared)
    next
      case (Unique k2 uarg2)
      then have "k1 ≠ k2"
        by (metis "0.prems"(5) "0.prems"(8) Suc_eq_plus1 ‹⋀thesis. (⋀xs'. s' = x2 # x1 # xs' ⟹ thesis) ⟹ thesis› ‹s = x1 # x2 # xs› ‹x1 = Unique k1 uarg1› action.disc(2) action.sel(2) is_Unique_def is_Unique_i_def nth_Cons_0)
      then have "upre k2 uarg2 uarg2 ∧ upre k1 uarg1 uarg1"
        by (metis "0.prems"(6) PRE_sequenceE_rec(1) PRE_sequenceE_rec(2) Unique ‹s = x1 # x2 # xs› ‹x1 = Unique k1 uarg1› abstract_pre.simps(2))

      then show ?thesis
      using ‹all_axioms α sact spre uact upre› Unique ‹α (compute sact uact v0 xs) = α (compute sact uact v0' xs)›
        ‹s = x1 # x2 # xs› ‹s' = x2 # x1 # xs'› ‹xs = xs'› compute.simps(2)[of sact uact]
        uu_com[of α sact spre uact upre k1 k2 "compute sact uact v0' xs" "compute sact uact v0 xs"]
         ‹k1 ≠ k2› ‹x1 = Unique k1 uarg1› compute.simps(3)
      by auto
    qed
  qed
next
  case (Suc k)
  then obtain x xs x' xs' where "s = x # xs" "s' = x' # xs'"
    by (metis diff_0_eq_0 length_0_conv neq_Nil_conv not_less_zero)
  then have "x = x'"
    using Suc.prems(3) by force
  moreover have "α (compute sact uact v0 (tl s)) = α (compute sact uact v0' (tl s'))"
  proof (rule Suc(1))
    show "length (tl s) = length (tl s')"
      by (simp add: Suc.prems(1))
    show "k < length (tl s) - 1"
      using Suc.prems(2) by auto
    show "⋀i. 0 ≤ i ∧ i < length (tl s) ∧ i ≠ k ∧ i ≠ k + 1 ⟹ tl s ! i = tl s' ! i"
      by (metis Suc.prems(3) Suc_eq_plus1 ‹length (tl s) = length (tl s')› length_tl less_diff_conv nat.inject nat_le_linear not_less_eq_eq nth_tl)
    show "tl s ! k = tl s' ! (k + 1)"
      by (metis Suc.prems(4) Suc_eq_plus1 ‹s = x # xs› ‹s' = x' # xs'› add_diff_cancel_right' add_gr_0 le_neq_implies_less list.sel(3) not_one_le_zero nth_Cons_pos zero_less_one_class.zero_le_one)
    show "tl s' ! k = tl s ! (k + 1)"
      by (metis Suc.prems(5) Suc_eq_plus1 ‹s = x # xs› ‹s' = x' # xs'› list.sel(3) nth_Cons_Suc)
    show "PRE_sequence spre upre (tl s) (tl s)"
      by (metis Suc.prems(6) ‹s = x # xs› PRE_sequenceE_rec(1) list.sel(3))
    show "α v0 = α v0'"
      by (simp add: assms(7))
    show "¬ (∃k'. is_Unique_i k' (tl s ! k) ∧ is_Unique_i k' (tl s ! (k + 1)))"
      using Suc.prems(8) ‹s = x # xs› by force
    show "all_axioms α sact spre uact upre"
      by (simp add: Suc.prems(9))
  qed
  ultimately show ?case
  proof (cases x)
    case (Shared x1)
    then show ?thesis
      using ‹all_axioms α sact spre uact upre› PRE_sequenceE_rec(2) Suc.prems(6) ‹α (compute sact uact v0 (tl s)) = α (compute sact uact v0' (tl s'))› ‹s = x # xs› ‹s' = x' # xs'› ‹x = x'› sabstract 
      by fastforce
  next
    case (Unique x2)
    then show ?thesis
      using ‹all_axioms α sact spre uact upre› PRE_sequenceE_rec(2) Suc.prems(6)
        ‹α (compute sact uact v0 (tl s)) = α (compute sact uact v0' (tl s'))› ‹s = x # xs› ‹s' = x' # xs'›
        ‹x = x'› uabstract[of α sact spre uact upre]
      by fastforce
  qed
qed

lemma mset_remove:
  assumes "k ≥ 0 ∧ k < length s"
  shows "mset s = mset (remove_at_index k s) + {# s ! k #}"
  using assms
proof (induct s arbitrary: k)
  case Nil
  then show ?case
    by simp
next
  case (Cons a s)
  then show ?case
    using less_Suc_eq_0_disj by auto
qed

lemma abstract_pre_refl:
  assumes "abstract_pre spre upre a b"
      and "all_axioms α sact spre uact upre"
  shows "abstract_pre spre upre b b"
  apply (cases a)
   apply (cases b)
  using abstract_pre.simps(1) assms spre_refl apply metis
  using assms apply force
   apply (cases b)
  using assms apply force
  using abstract_pre.simps(2) assms upre_refl by metis

lemma PRE_sequence_refl:
  assumes "PRE_sequence spre upre s s'"
      and "all_axioms α sact spre uact upre"
  shows "PRE_sequence spre upre s' s'"
proof (rule PRE_sequenceI)
  show "length s' = length s'"
    by simp
  fix i assume "0 ≤ i ∧ i < length s'"
  then show "abstract_pre spre upre (s' ! i) (s' ! i)"
    by (metis PRE_sequence_def abstract_pre_refl assms)
qed

lemma PRE_sequence_removes:
  assumes "PRE_sequence spre upre s s"
  shows "PRE_sequence spre upre (remove_at_index n s) (remove_at_index n s)"
  using assms
proof (induct n arbitrary: s)
  case 0
  then show ?case
    by (metis PRE_sequenceE_rec(1) nat.simps(3) remove_at_index.elims)
next
  case (Suc n)
  then show ?case
    apply (cases s)
     apply force
    by (metis PRE_sequenceE_rec(1) PRE_sequenceE_rec(2) PRE_sequenceI_rec remove_at_index.simps(3))
qed

lemma PRE_sequence_insert:
  assumes "abstract_pre spre upre x x"
    and "PRE_sequence spre upre s s"
    shows "PRE_sequence spre upre (insert_at n x s) (insert_at n x s)"
  using assms
proof (induct n arbitrary: s)
  case 0
  then show ?case
    by (simp add: PRE_sequenceI_rec)
next
  case (Suc n)
  then show ?case
    apply (cases s)
     apply (simp add: PRE_sequenceI_rec)
    by (metis PRE_sequenceE_rec(1) PRE_sequenceE_rec(2) PRE_sequenceI_rec insert_at.simps(3))
qed

lemma empty_possible_sequence:
  assumes "possible_sequence sargs uargs []"
      and "possible_sequence sargs uargs s'"
  shows "s' = []"
proof (rule ccontr)
  assume "s' ≠ []"
  then obtain x q where "s' = x # q"
    by (meson neq_Nil_conv)
  then show False
  proof (cases x)
    case (Shared x1)
    then show ?thesis
      by (metis ‹s' = x # q› assms(1) assms(2) exists_index_in_sequence_shared less_zeroE list.size(3) possible_sequence_where_is_shared)
  next
    case (Unique k uarg)
    then have "uargs k ≠ []"
      by (metis (no_types, lifting) ‹s' = x # q› action.disc(2) action.sel(2) assms(2) filter.simps(2) is_Unique_def is_Unique_i_def list.discI list.map_disc_iff possible_sequence_def)
    then show ?thesis
      by (metis assms(1) exists_index_in_sequence_unique less_nat_zero_code list.size(3))
  qed
qed

lemma it_all_commutes:
  assumes "possible_sequence sargs uargs s"
      and "possible_sequence sargs uargs s'"
      and "α v0 = α v0'"
      and "PRE_sequence spre upre s s"
      and "PRE_sequence spre upre s' s'"
      and "all_axioms α sact spre uact upre"
    shows "α (compute sact uact v0 s) = α (compute sact uact v0' s')"
  using assms
proof (induct "size s" arbitrary: sargs uargs s s')
  case 0
  then have "s = [] ∧ s' = []"
    by (simp add: empty_possible_sequence)
  then show ?case
    by (simp add: "0.prems"(1) "0.prems"(2) assms(3))
next
  case (Suc n)
  moreover obtain x s1 where "s = x # s1"
    by (meson Suc.hyps(2) Suc_length_conv)
  then have "abstract_pre spre upre x x"
    using Suc.prems(4) PRE_sequenceE_rec(2) by blast
  then show ?case
  proof (cases x)
    case (Shared sarg)
    then have "Shared sarg ∈ set s'"
      by (metis Suc.prems(1) Suc.prems(2) ‹s = x # s1› exists_index_in_sequence_shared nth_mem possible_sequence_where_is_shared)
    then obtain k where "k ≥ 0 ∧ k < length s' ∧ s' ! k = x"
      by (metis Shared bot_nat_0.extremum in_set_conv_nth)

    let ?s' = "remove_at_index k s'"
    have "length ?s' = length s' - 1"
      by (simp add: ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› remove_at_index(1))
    moreover have "k < length s'"
      by (simp add: ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x›)
    then have "s' = insert_at k x ?s'"
      by (simp add: ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› insert_remove_same_list)
    define i :: nat where "i = k"
    have "i ≥ 0 ∧ i ≤ k ⟹ α (compute sact uact v0' (insert_at (k - i) x ?s')) = α (compute sact uact v0' s')" 
    proof (induct i)
      case 0
      then show ?case
        using ‹s' = insert_at k x (remove_at_index k s')› by auto
    next
      case (Suc i)
      then have "α (compute sact uact v0' (insert_at (k - i) x (remove_at_index k s'))) = α (compute sact uact v0' s')"
        using Suc_leD by blast
      moreover have "α (compute sact uact v0' (insert_at (k - Suc i) x (remove_at_index k s'))) = α (compute sact uact v0' (insert_at (k - i) x (remove_at_index k s')))"
      proof (rule swap_works)
        show "length (insert_at (k - Suc i) x (remove_at_index k s')) = length (insert_at (k - i) x (remove_at_index k s'))"
          by (metis (no_types, lifting) Suc_pred' ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› ‹length (remove_at_index k s') = length s' - 1› diff_le_self insert_at_index(1) less_Suc_eq_le order_le_less_trans)
        show "PRE_sequence spre upre (insert_at (k - Suc i) x (remove_at_index k s')) (insert_at (k - Suc i) x (remove_at_index k s'))"
        proof -
          have "PRE_sequence spre upre (remove_at_index k s') (remove_at_index k s')" using ‹PRE_sequence spre upre s' s'›
            using PRE_sequence_removes by auto
          then show ?thesis using PRE_sequence_insert ‹abstract_pre spre upre x x› by blast
        qed
        show "α v0' = α v0'" by simp
        let ?k = "k - Suc i"

        show "?k < length (insert_at (k - Suc i) x (remove_at_index k s')) - 1"
          using One_nat_def Suc.prems Suc_diff_Suc Suc_le_lessD ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1›
            ‹s' = insert_at k x (remove_at_index k s')› diff_le_self diff_zero
            insert_at_index(1)[of "k - Suc i" _ x] insert_at_index(1)[of k _ x] less_Suc_eq_le order_le_less_trans
          by simp
        show "insert_at (k - Suc i) x (remove_at_index k s') ! ?k = insert_at (k - i) x (remove_at_index k s') ! (?k + 1)"
          apply (cases k)
          using Suc.prems apply blast
          apply (cases ?k)
           apply (metis (no_types, lifting) Suc.prems Suc_eq_plus1 Suc_leI ‹k - Suc i < length (insert_at (k - Suc i) x (remove_at_index k s')) - 1› add_diff_cancel_right' diff_diff_cancel diff_zero insert_at_index(1) insert_at_index(3) le_numeral_extra(3) length_greater_0_conv list.size(3) nat_less_le plus_1_eq_Suc)
        proof -
          fix nat nata assume r: "k = Suc nat" "k - Suc i = Suc nata"
          moreover have "insert_at (k - i) x (remove_at_index k s') ! (k - i) = x"
            by (metis Suc_pred' ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› bot_nat_0.extremum diff_le_self insert_at_index(3) less_Suc_eq_le order_le_less_trans)
          moreover have "⋀x. insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i) = x"
            by (metis Suc_leI Suc_le_mono Suc_pred' ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› ‹length (remove_at_index k s') = length s' - 1› bot_nat_0.extremum diff_le_self insert_at_index(3) order_le_less_trans)
          ultimately show ?thesis
            by (metis Suc.prems Suc_diff_Suc Suc_eq_plus1 Suc_le_lessD)
        qed
        show "insert_at (k - i) x (remove_at_index k s') ! ?k = insert_at (k - Suc i) x (remove_at_index k s') ! (?k + 1)"
        proof -
          have "insert_at (k - i) x (remove_at_index k s') ! (k - Suc i) = remove_at_index k s' ! (k - Suc i)"
            by (metis (no_types, lifting) Suc.prems Suc_diff_Suc Suc_eq_plus1 Suc_leI Suc_le_lessD ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› add_leE insert_at_index(2) le_add_diff_inverse2 le_add_same_cancel2 lessI less_Suc_eq_le)
          moreover have "length (insert_at (k - Suc i) x (remove_at_index k s')) = length (remove_at_index k s') + 1"
            by (metis Suc_eq_plus1 ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› ‹length (remove_at_index k s') = length s' - 1› add_le_imp_le_diff insert_at_index(1) less_eq_Suc_le less_imp_diff_less)
          then have "insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i + 1) = remove_at_index k s' ! (k - Suc i + 1 - 1)"
            by (metis ‹k - Suc i < length (insert_at (k - Suc i) x (remove_at_index k s')) - 1› add_diff_cancel_right' insert_at_index(4) less_add_one less_diff_conv less_imp_le_nat)
          ultimately show ?thesis
            by simp
        qed

        show "¬ (∃k'. is_Unique_i k' (insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i)) ∧
         is_Unique_i k' (insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i + 1)))"
          by (metis (no_types, lifting) One_nat_def Shared Suc.prems Suc_diff_Suc ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› action.disc(1) add_leE diff_zero insert_at_index(3) is_Unique_def is_Unique_i_def le_add_diff_inverse2 le_add_same_cancel2 less_Suc_eq_le order_le_less_trans)

        show "⋀j. 0 ≤ j ∧ j < length (insert_at (k - Suc i) x (remove_at_index k s')) ∧ j ≠ ?k ∧ j ≠ ?k + 1 ⟹
         insert_at (k - Suc i) x (remove_at_index k s') ! j = insert_at (k - i) x (remove_at_index k s') ! j"
        proof (clarify)
          fix j assume "0 ≤ j" "j < length (insert_at (k - Suc i) x (remove_at_index k s'))" "j ≠ k - Suc i" "j ≠ k - Suc i + 1"
          moreover have "length (insert_at (k - Suc i) x (remove_at_index k s')) = length (remove_at_index k s') + 1"
            by (metis (no_types, lifting) One_nat_def Suc.prems Suc_diff_Suc ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› add_leE diff_zero insert_at_index(1) le_add_diff_inverse2 less_Suc_eq_le order_le_less_trans)
          moreover have "k - Suc i ≤ length (remove_at_index k s')"
            using ‹k - Suc i < length (insert_at (k - Suc i) x (remove_at_index k s')) - 1› calculation(5) by force
          ultimately show "insert_at (k - Suc i) x (remove_at_index k s') ! j = insert_at (k - i) x (remove_at_index k s') ! j"
            apply (cases "j < k - Suc i")
            using insert_at_index(2)[of "k - Suc i" "remove_at_index k s'" j x] insert_at_index(2)[of "k - i" "remove_at_index k s'" j x]
            apply (metis Suc.prems Suc_diff_le Suc_eq_plus1 Suc_leI ‹k - Suc i < length (insert_at (k - Suc i) x (remove_at_index k s')) - 1› diff_Suc_1 diff_Suc_Suc less_Suc_eq)
            by (simp add: insert_at_index(4) nat_neq_iff)
        qed
        show "all_axioms α sact spre uact upre"
          by (simp add: assms(6))
      qed
      ultimately show ?case
        by presburger
    qed
    then have "α (compute sact uact v0' (x # ?s')) = α (compute sact uact v0' s')"
      using i_def by force
    moreover have "α (compute sact uact v0 s1) = α (compute sact uact v0' ?s')"
    proof (rule Suc(1))
      show "n = length s1"
        using Suc.hyps(2) ‹s = x # s1› by auto
      show "α v0 = α v0'"
        using assms(3) by auto
      show "PRE_sequence spre upre s1 s1"
        using PRE_sequenceE_rec(1) Suc.prems(4) ‹s = x # s1› by blast
      show "possible_sequence (sargs - {# sarg #}) uargs s1"
      proof (rule possible_sequenceI)
        show "⋀i. uargs i = map get_u (filter (is_Unique_i i) s1)"
          by (metis (mono_tags, lifting) Shared Suc.hyps(2) Suc.prems(1) ‹s = x # s1› action.disc(1) filter_remove is_Unique_def is_Unique_i_def le_numeral_extra(3) nth_Cons_0 possible_sequence_def remove_at_index.simps(2) zero_less_Suc)
        show "sargs - {#sarg#} = image_mset get_s (filter_mset is_Shared (mset s1))"
          using Shared Suc.prems(1) ‹s = x # s1› action.disc(1)[of sarg] action.sel(1)[of sarg] add_mset_diff_bothsides diff_empty
            filter_mset_add_mset msed_map_invL mset.simps(2) possible_sequence_def[of sargs uargs s]
          by simp
      qed

      show "possible_sequence (sargs - {#sarg#}) uargs (remove_at_index k s')"
      proof (rule possible_sequenceI)
        show "⋀i. uargs i = map get_u (filter (is_Unique_i i) (remove_at_index k s'))"
        proof (rule list_ext)
          have "filter is_Unique (remove_at_index k s') = filter is_Unique s'"
            by (simp add: Shared ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› filter_remove is_Unique_def)
          then show "⋀i. length (uargs i) = length (map get_u (filter (is_Unique_i i) (remove_at_index k s')))"
            by (metis Shared Suc.prems(2) ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› action.disc(1) filter_remove is_Unique_def is_Unique_i_def possible_sequence_def)
          show "⋀i ia. 0 ≤ ia ∧ ia < length (uargs i) ⟹ uargs i ! ia = map get_u (filter (is_Unique_i i) (remove_at_index k s')) ! ia"
            by (metis Shared Suc.prems(2) ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› action.disc(1) filter_remove is_Unique_def is_Unique_i_def possible_sequence_def)
        qed
        have "sargs = image_mset get_s (filter_mset is_Shared (mset s'))"
          using Suc.prems(2) possible_sequence_def by blast
        show "sargs - {#sarg#} = image_mset get_s (filter_mset is_Shared (mset (remove_at_index k s')))"
        proof -
          have "mset s' = mset (remove_at_index k s') + {# x #}"
            using ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› mset_remove_index by blast
          then show ?thesis
            by (simp add: Shared ‹sargs = image_mset get_s (filter_mset is_Shared (mset s'))›)
        qed
      qed
      show "PRE_sequence spre upre (remove_at_index k s') (remove_at_index k s')" using Suc.prems(5) PRE_sequence_removes by blast
      show "all_axioms α sact spre uact upre" by (simp add: assms(6))
    qed
    ultimately show ?thesis
      using ‹all_axioms α sact spre uact upre› PRE_sequenceE_rec(2) Shared Suc.prems(4) ‹s = x # s1› abstract_pre.simps(1) compute.simps(2) sabstract
      by fastforce
  next
    case (Unique ind uarg)
    let ?uargs = "uargs ind"
    have "hd ?uargs = uarg"
      by (metis Unique ‹s = x # s1› calculation(3) possible_sequence_where_is_unique)
    moreover have "?uargs ≠ []"
      by (metis (no_types, opaque_lifting) Suc.prems(1) Unique ‹s = x # s1› action.disc(2) action.sel(2) filter.simps(2) is_Unique_def is_Unique_i_def list.distinct(1) list.map_disc_iff possible_sequence_def)
    ultimately have "?uargs = uarg # tl ?uargs"
      by force
    then obtain k where "k ≥ 0 ∧ k < length s' ∧ s' ! k = x" "⋀j. j ≥ 0 ∧ j < k ⟹ ¬ is_Unique_i ind (s' ! j)"
      by (metis Suc.prems(2) Unique ‹hd (uargs ind) = uarg› ‹uargs ind ≠ []› exists_index_in_sequence_unique)
    let ?s' = "remove_at_index k s'"
    have "length ?s' = length s' - 1"
      by (simp add: ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› remove_at_index(1))
    moreover have "k < length s'"
      by (simp add: ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x›)
    then have "s' = insert_at k x ?s'"
      by (simp add: ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› insert_remove_same_list)
    define i :: nat where "i = k"
    have "i ≥ 0 ∧ i ≤ k ⟹ α (compute sact uact v0' (insert_at (k - i) x ?s')) = α (compute sact uact v0' s')" 
    proof (induct i)
      case 0
      then show ?case
        using ‹s' = insert_at k x (remove_at_index k s')› by auto
    next
      case (Suc i)
      then have "α (compute sact uact v0' (insert_at (k - i) x (remove_at_index k s'))) = α (compute sact uact v0' s')"
        using Suc_leD by blast
      moreover have "α (compute sact uact v0' (insert_at (k - Suc i) x (remove_at_index k s'))) = α (compute sact uact v0' (insert_at (k - i) x (remove_at_index k s')))"
      proof (rule swap_works)
        show "length (insert_at (k - Suc i) x (remove_at_index k s')) = length (insert_at (k - i) x (remove_at_index k s'))"
          by (metis (no_types, lifting) Suc_pred' ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› ‹length (remove_at_index k s') = length s' - 1› insert_at_index(1) less_Suc_eq_le less_imp_diff_less order_le_less_trans)
        show "PRE_sequence spre upre (insert_at (k - Suc i) x (remove_at_index k s')) (insert_at (k - Suc i) x (remove_at_index k s'))"
        proof -
          have "PRE_sequence spre upre (remove_at_index k s') (remove_at_index k s')"
            using ‹PRE_sequence spre upre s' s'›
            by (simp add: PRE_sequence_removes)
          then show ?thesis
            using ‹abstract_pre spre upre x x› PRE_sequence_insert by blast
        qed

        show "α v0' = α v0'" by simp
        let ?k = "k - Suc i"


        show "?k < length (insert_at (k - Suc i) x (remove_at_index k s')) - 1"
          using One_nat_def Suc.prems Suc_diff_Suc Suc_le_lessD ‹k < length s'›
            ‹length (remove_at_index k s') = length s' - 1› ‹s' = insert_at k x (remove_at_index k s')›
            diff_le_self diff_zero insert_at_index(1)[of k "remove_at_index k s'" x] insert_at_index(1)[of "k - Suc i" "remove_at_index k s'" x]
            less_Suc_eq_le order_le_less_trans
          by simp
        show "insert_at (k - Suc i) x (remove_at_index k s') ! ?k = insert_at (k - i) x (remove_at_index k s') ! (?k + 1)"
        proof -
          have "insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i) = x"
            by (metis Suc_pred' ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› bot_nat_0.extremum diff_self_eq_0 insert_at_index(3) less_Suc_eq_le less_imp_diff_less)
          moreover have "insert_at (k - i) x (remove_at_index k s') ! (k - i) = x"
            by (metis Suc_pred' ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› bot_nat_0.extremum insert_at_index(3) less_Suc_eq_le less_imp_diff_less less_nat_zero_code not_gr_zero)
          ultimately show ?thesis
            by (simp add: Suc.prems Suc_diff_Suc Suc_le_lessD)
        qed
        have "insert_at (k - i) x (remove_at_index k s') ! (k - Suc i) = remove_at_index k s' ! (k - Suc i)"
          by (metis (no_types, lifting) Suc.prems Suc_diff_Suc Suc_eq_plus1 Suc_leI Suc_le_lessD ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› add_leE insert_at_index(2) le_add_diff_inverse2 le_add_same_cancel2 lessI less_Suc_eq_le)
        then 
        show "insert_at (k - i) x (remove_at_index k s') ! ?k = insert_at (k - Suc i) x (remove_at_index k s') ! (?k + 1)"
          using  One_nat_def Suc.prems Suc_diff_Suc ‹k - Suc i < length (insert_at (k - Suc i) x (remove_at_index k s')) - 1›
            ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› add_diff_cancel_right'
            add_leE diff_zero insert_at_index(1)[of "k - Suc i" "remove_at_index k s'" x] insert_at_index(4)[of "k - Suc i" "remove_at_index k s'"]
            le_add_diff_inverse2 less_Suc_eq_le
            less_add_same_cancel1 less_diff_conv order_le_less_trans zero_less_one
          by simp

        have "insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i + 1) = remove_at_index k s' ! (k - Suc i + 1 - 1)"
          using ‹insert_at (k - i) x (remove_at_index k s') ! (k - Suc i) = insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i + 1)› ‹insert_at (k - i) x (remove_at_index k s') ! (k - Suc i) = remove_at_index k s' ! (k - Suc i)› by auto
        then have "¬ is_Unique_i ind (insert_at (k - Suc i) x (remove_at_index k s') ! (?k + 1))"
          by (metis One_nat_def Suc.prems Suc_le_lessD ‹⋀j. 0 ≤ j ∧ j < k ⟹ ¬ is_Unique_i ind (s' ! j)› ‹k < length s'› add_diff_cancel_right' add_leE diff_Suc_less le_add2 le_add_same_cancel2 plus_1_eq_Suc remove_at_index(2))
        then show "¬ (∃k'. is_Unique_i k' (insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i)) ∧
         is_Unique_i k' (insert_at (k - Suc i) x (remove_at_index k s') ! (k - Suc i + 1)))"
          by (metis (no_types, lifting) One_nat_def Suc.prems Suc_diff_Suc Unique ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› action.sel(2) diff_zero insert_at_index(3) is_Unique_i_def le_add2 le_add_diff_inverse le_add_same_cancel2 less_Suc_eq_le order_le_less_trans)
        show "⋀j. 0 ≤ j ∧ j < length (insert_at (k - Suc i) x (remove_at_index k s')) ∧ j ≠ ?k ∧ j ≠ ?k + 1 ⟹
         insert_at (k - Suc i) x (remove_at_index k s') ! j = insert_at (k - i) x (remove_at_index k s') ! j"
        proof -
          fix j assume "0 ≤ j ∧ j < length (insert_at (k - Suc i) x (remove_at_index k s')) ∧ j ≠ ?k ∧ j ≠ ?k + 1"
          moreover have "k - Suc i ≤ length (remove_at_index k s')"
            using ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› ‹length (remove_at_index k s') = length s' - 1› by force
          moreover have "k - i ≤ length (remove_at_index k s')"
            using ‹k < length s'› ‹length (remove_at_index k s') = length s' - 1› by linarith
          then show "insert_at (k - Suc i) x (remove_at_index k s') ! j = insert_at (k - i) x (remove_at_index k s') ! j"
            apply (cases "j < k - i")
            apply (metis Suc.prems Suc_diff_Suc Suc_le_lessD calculation(1) calculation(2) insert_at_index(2) less_Suc_eq)
            by (metis Suc.prems Suc_diff_Suc Suc_eq_plus1 Suc_le_lessD calculation(1) calculation(2) insert_at_index(1) insert_at_index(4) linorder_le_less_linear linorder_neqE_nat)
        qed
        show "all_axioms α sact spre uact upre" by (simp add: assms(6))
      qed
      ultimately show ?case
        by presburger
    qed
    then have "α (compute sact uact v0' (x # ?s')) = α (compute sact uact v0' s')"
      using i_def by force
    moreover have "α (compute sact uact v0 s1) = α (compute sact uact v0' ?s')"
    proof (rule Suc(1))
      show "all_axioms α sact spre uact upre" by (simp add: assms(6))
      show "n = length s1"
        using Suc.hyps(2) ‹s = x # s1› by auto
      show "α v0 = α v0'"
        using assms(3) by auto
      show "PRE_sequence spre upre s1 s1"
        using Suc.prems(4) ‹s = x # s1› PRE_sequenceE_rec(1) by blast
      show "possible_sequence sargs (tail_kth uargs ind) s1"
      proof (rule possible_sequenceI)
        show "⋀i. tail_kth uargs ind i = map get_u (filter (is_Unique_i i) s1)"
        proof -
          fix i show "tail_kth uargs ind i = map get_u (filter (is_Unique_i i) s1)"
          proof (cases "i = ind")
            case True
            then have "tail_kth uargs ind i = tl ?uargs"
              by (simp add: tail_kth_def)
            then show ?thesis using exists_index_in_sequence_unique[of uarg uargs ind sargs s]
              by (metis Suc.prems(1) Unique ‹hd (uargs ind) = uarg› ‹s = x # s1› ‹uargs ind ≠ []› action.disc(2) action.sel(2) is_Unique_def is_Unique_i_def le_eq_less_or_eq nth_Cons_0 possible_sequence_def remove_at_index.simps(2))
          next
            case False
            then show ?thesis
              using Suc.hyps(2) Suc.prems(1) Unique ‹s = x # s1› action.sel(2) filter_remove
                fun_upd_apply is_Unique_i_def le_numeral_extra(3) nth_Cons_0[of x s1] possible_sequence_def[of sargs uargs s]
                remove_at_index.simps(2)[of x s1] tail_kth_def zero_less_Suc
              by metis
          qed
        qed
        show "sargs = image_mset get_s (filter_mset is_Shared (mset s1))"
          by (metis Suc.prems(1) Unique ‹s = x # s1› action.disc(2) filter_mset_add_mset mset.simps(2) possible_sequence_def)
      qed
      show "possible_sequence sargs (tail_kth uargs ind) (remove_at_index k s')"
      proof (rule possible_sequenceI)
        show "⋀i. tail_kth uargs ind i = map get_u (filter (is_Unique_i i) (remove_at_index k s'))"
          using Suc.prems(1) Suc.prems(2) Unique ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› ‹⋀j. 0 ≤ j ∧ j < k ⟹ ¬ is_Unique_i ind (s' ! j)›
            ‹possible_sequence sargs (tail_kth uargs ind) s1› ‹s = x # s1› action.sel(2) filter.simps(2)
            filter_remove fun_upd_same is_Unique_i_def possible_sequence_def[of sargs "tail_kth uargs ind" s1]
            possible_sequence_def[of sargs uargs s] possible_sequence_def[of sargs uargs s']
            remove_at_index_filter tail_kth_def
          by metis
        show "sargs = image_mset get_s (filter_mset is_Shared (mset (remove_at_index k s')))"
          by (metis Suc.prems(2) Unique ‹0 ≤ k ∧ k < length s' ∧ s' ! k = x› action.disc(2) filter_remove mset_filter possible_sequence_def)
      qed
      show "PRE_sequence spre upre (remove_at_index k s') (remove_at_index k s')"
        using PRE_sequence_removes Suc.prems(5) by auto
    qed
    ultimately show ?thesis
      using Unique ‹abstract_pre spre upre x x› ‹s = x # s1› abstract_pre.simps(2)[of ]
        assms(6) compute.simps(3)[of sact uact] uabstract[of α sact spre uact upre ]
      by metis
  qed
qed

lemma PRE_sequence_same_abstract:
  assumes "PRE_sequence spre upre s s'"
      and "α v0 = α v0'"
      and "all_axioms α sact spre uact upre"
    shows "α (compute sact uact v0 s) = α (compute sact uact v0' s')"
  using assms
proof (induct s' arbitrary: s v0 v0')
  case Nil
  then show ?case
    by (simp add: PRE_sequence_def)
next
  case (Cons act' s')
  then show ?case
  proof (cases act')
    case (Shared sarg')
    then obtain sarg s0 where "s = Shared sarg # s0" "spre sarg sarg'" "PRE_sequence spre upre s0 s'"
      by (metis Cons.prems(1) PRE_sequenceE_rec(1) PRE_sequenceE_rec(2) PRE_sequence_def abstract_pre.simps(1) abstract_pre.simps(3) action.exhaust length_0_conv neq_Nil_conv)
    then show ?thesis
      using Cons.hyps Cons.prems(2) Cons.prems(3) Shared sabstract by fastforce
  next
    case (Unique k uarg')
    then obtain uarg s0 where "s = Unique k uarg # s0" "upre k uarg uarg'" "PRE_sequence spre upre s0 s'"
      by (metis Cons.prems(1) PRE_sequenceE_rec(1) PRE_sequenceE_rec(2) PRE_sequence_def abstract_pre.simps(2) abstract_pre.simps(4) action.exhaust length_0_conv neq_Nil_conv)
    then show ?thesis
      using Cons.hyps Cons.prems(2) Unique assms(3) uabstract by fastforce
  qed
qed

lemma simple_possible_PRE_seq:
  assumes "possible_sequence sargs uargs s"
      and "possible_sequence sargs' uargs' s'"
      and "PRE_shared spre sargs sargs'"
      and "⋀k. PRE_unique (upre k) (uargs k) (uargs' k)"
      and "all_axioms α sact spre uact upre"
    shows "PRE_sequence spre upre s' s'"
proof (rule PRE_sequenceI)
  show "length s' = length s'" by simp
  fix i assume "0 ≤ i ∧ i < length s'"
  then show "abstract_pre spre upre (s' ! i) (s' ! i)"
  proof (cases "s' ! i")
    case (Shared sarg')
    then have "Shared sarg' ∈# filter_mset is_Shared (mset s')"
      using ‹0 ≤ i ∧ i < length s'› nth_mem_mset by fastforce
    then have "sarg' ∈# sargs'"
      by (metis (mono_tags, lifting) action.sel(1) assms(2) imageI possible_sequence_def set_image_mset)
    moreover obtain ms where "image_mset fst ms = sargs ∧ image_mset snd ms = sargs' ∧ (∀x ∈# ms. spre (fst x) (snd x))"
      using PRE_shared_def assms(3) by blast
    then obtain x where "x ∈# ms" "snd x = sarg'"
      using calculation by fastforce
    then show ?thesis
      using Shared ‹image_mset fst ms = sargs ∧ image_mset snd ms = sargs' ∧ (∀x∈#ms. spre (fst x) (snd x))› spre_refl
      by (metis abstract_pre.simps(1) assms(5))
  next
    case (Unique k uarg')
    then have "Unique k uarg' ∈ set (filter is_Unique s')"
      by (metis ‹0 ≤ i ∧ i < length s'› is_Unique_def action.disc(2) filter_set member_filter nth_mem)
    then have "uarg' ∈ set (map get_u (filter (is_Unique_i k) s'))"
      by (metis (no_types, lifting) action.sel(2) action.sel(3) filter_set image_eqI is_Unique_i_def list.set_map member_filter)
    then obtain i where "i ≥ 0 ∧ i < length (uargs' k) ∧ uarg' = (uargs' k) ! i"
      by (metis assms(2) gr_implies_not_zero in_set_conv_nth linorder_le_less_linear possible_sequence_def)
    then have "upre k ((uargs k) ! i) ((uargs' k) ! i)"
      using PRE_unique_def assms(4) by blast
    then show ?thesis
      using Unique ‹0 ≤ i ∧ i < length (uargs' k) ∧ uarg' = uargs' k ! i› assms(5) upre_refl by fastforce
  qed
qed

lemma main_lemma:
  assumes "possible_sequence sargs uargs s"
      and "possible_sequence sargs' uargs' s'"

      and "PRE_shared spre sargs sargs'"
      and "⋀k. PRE_unique (upre k) (uargs k) (uargs' k)"

      and "α v0 = α v0'"
      and "all_axioms α sact spre uact upre"

    shows "α (compute sact uact v0 s) = α (compute sact uact v0' s')"
proof -
  obtain s'' where "possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre s s''"
    using assms(1) assms(2) assms(3) assms(4) exists_aligned_sequence by blast
  have "α (compute sact uact v0' s'') = α (compute sact uact v0' s')"
  proof (rule it_all_commutes)
    show "possible_sequence sargs' uargs' s''"
      by (simp add: ‹possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre s s''›)
    show "possible_sequence sargs' uargs' s'"
      by (simp add: assms(2))
    show "α v0' = α v0'"
      by simp
    show "PRE_sequence spre upre s'' s''"
      using ‹possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre s s''› PRE_sequence_refl assms(6) by blast
    show "PRE_sequence spre upre s' s'"
      using simple_possible_PRE_seq assms(1) assms(2) assms(3) assms(4) assms(6) by blast
    show "all_axioms α sact spre uact upre"
      using assms(6) by auto
  qed
  moreover have "α (compute sact uact v0' s'') = α (compute sact uact v0 s)"
    using PRE_sequence_same_abstract ‹possible_sequence sargs' uargs' s'' ∧ PRE_sequence spre upre s s''› assms(1) assms(5) assms(6) by metis
  ultimately show ?thesis
    by auto
qed

inductive reachable_value :: "('v ⇒ 'a ⇒ 'v) ⇒ ('i ⇒ 'v ⇒ 'b ⇒ 'v) ⇒ 'v ⇒ 'a multiset ⇒ ('i ⇒ 'b list) ⇒ 'v ⇒ bool" where
  Self: "reachable_value sact uact v0 {#} (λk. []) v0"
| SharedStep: "reachable_value sact uact v0 sargs uargs v1 ⟹ reachable_value sact uact v0 (sargs + {# sarg #}) uargs (sact v1 sarg)"
| UniqueStep: "reachable_value sact uact v0 sargs uargs v1 ⟹ reachable_value sact uact v0 sargs (uargs(k := uarg # uargs k)) (uact k v1 uarg)"

lemma reachable_then_possible_sequence_and_compute:
  assumes "reachable_value sact uact v0 sargs uargs v1"
  shows "∃s. possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s"
  using assms
proof (induct rule: reachable_value.induct)
  case (Self sact uact v0)
  have "possible_sequence {#} (λk. []) [] ∧ v0 = compute sact uact v0 []"
    by (simp add: possible_sequenceI)
  then show ?case by blast
next
  case (SharedStep sact uact v0 sargs uargs v1 sarg)
  then obtain s where "possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s" by blast
  let ?s = "Shared sarg # s"
  have "possible_sequence (sargs + {#sarg#}) uargs ?s"
  proof (rule possible_sequenceI)
    show "⋀i. uargs i = map get_u (filter (is_Unique_i i) (Shared sarg # s))"
      by (metis ‹possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s› action.disc(1) filter.simps(2) is_Unique_def is_Unique_i_def possible_sequence_def)
    show "sargs + {#sarg#} = image_mset get_s (filter_mset is_Shared (mset (Shared sarg # s)))"
      using ‹possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s› possible_sequence_def by auto
  qed
  then show ?case
    using ‹possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s› by auto
next
  case (UniqueStep sact uact v0 sargs uargs v1 k uarg)
  then obtain s where "possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s" by blast
  let ?s = "Unique k uarg # s"
  have "possible_sequence sargs (uargs(k := uarg # uargs k)) ?s"
  proof (rule possible_sequenceI)
    show "⋀i. (uargs(k := uarg # uargs k)) i = map get_u (filter (is_Unique_i i) (Unique k uarg # s))"
    proof -
      fix i show "(uargs(k := uarg # uargs k)) i = map get_u (filter (is_Unique_i i) (Unique k uarg # s))"
      proof (cases "i = k")
        case True
        then show ?thesis
          using Cons_eq_map_conv ‹possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s›
            action.disc(2) action.sel(2) action.sel(3) filter.simps(2) fun_upd_same is_Unique_def
            is_Unique_i_def possible_sequence_def[of sargs uargs s]
          by fastforce
      next
        case False
        then show ?thesis
          by (metis ‹possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s› action.sel(2) filter.simps(2) fun_upd_other is_Unique_i_def possible_sequence_def)
      qed
    qed
    show "sargs = image_mset get_s (filter_mset is_Shared (mset (Unique k uarg # s)))"
      using ‹possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s› possible_sequence_def by force
  qed
  then show ?case using ‹possible_sequence sargs uargs s ∧ v1 = compute sact uact v0 s›
    by (metis compute.simps(3))
qed

lemma PRE_shared_simpler_implies:
  assumes "PRE_shared_simpler spre a b"
  shows "PRE_shared spre a b"
  using assms
proof (induct rule: PRE_shared_simpler.induct)
  case (Empty spre)
  then show ?case
    by (simp add: PRE_shared_def)
next
  case (Step spre a b xa xb)
  then obtain ms where "image_mset fst ms = a ∧ image_mset snd ms = b ∧ (∀x∈#ms. spre (fst x) (snd x))"
    by (metis PRE_shared_def)
  then have "image_mset fst (ms + {# (xa, xb) #}) = (a + {#xa#}) ∧ image_mset snd (ms + {# (xa, xb) #}) = (b + {#xb#}) ∧ (∀x∈#(ms + {# (xa, xb) #}). spre (fst x) (snd x))"
    using Step.hyps(3) by auto
  then show ?case using PRE_shared_def by blast
qed

theorem main_result:
  assumes "reachable_value sact uact v0 sargs uargs v"
      and "reachable_value sact uact v0' sargs' uargs' v'"
      and "PRE_shared_simpler spre sargs sargs'"
      and "⋀k. PRE_unique (upre k) (uargs k) (uargs' k)"
      and "α v0 = α v0'"
      and "all_axioms α sact spre uact upre"
    shows "α v = α v'"
proof -
  obtain s s' where "possible_sequence sargs uargs s ∧ v = compute sact uact v0 s" "possible_sequence sargs' uargs' s' ∧ v' = compute sact uact v0' s'" 
    using assms(1) assms(2) reachable_then_possible_sequence_and_compute
    by metis
  then show ?thesis
    by (meson PRE_shared_simpler_implies assms(3) assms(4) assms(5) assms(6) main_lemma)
qed

end