Theory ResTerm

theory ResTerm
  imports Main
begin

section‹Resource Terms›

text‹
  Resource terms describe resources with atoms drawn from two types, linear and copyable, combined
  in a number of ways:
  ▪ Parallel resources represent their simultaneous presence,
  ▪ Non-deterministic resource represent exactly one of two options,
  ▪ Executable resources represent a single potential execution of a process transforming one
    resource into another,
  ▪ Repeatably executable resources represent an unlimited amount of such potential executions.

  We define two distinguished resources on top of the atoms:
  ▪ Empty, to represent the absence of a resource and serve as the unit for parallel combination,
  ▪ Anything, to represent a resource about which we have no information.
›
datatype (discs_sels) ('a, 'b) res_term =
  Res 'a
    ― ‹Linear resource atom›
  | Copyable 'b
    ― ‹Copyable resource atom›
  | is_Empty: Empty
    ― ‹The absence of a resource›
  | is_Anything: Anything
    ― ‹Resource about which we know nothing›
  | Parallel "('a, 'b) res_term list"
    ― ‹Parallel combination›
  | NonD "('a, 'b) res_term" "('a, 'b) res_term"
    ― ‹Non-deterministic combination›
  | Executable "('a, 'b) res_term" "('a, 'b) res_term"
    ― ‹Executable resource›
  | Repeatable "('a, 'b) res_term" "('a, 'b) res_term"
    ― ‹Repeatably executable resource›

text‹Every child of @{const Parallel} is smaller than it›
lemma parallel_child_smaller:
  "x ∈ set xs ⟹ size_res_term f g x < size_res_term f g (Parallel xs)"
proof (induct xs)
  case Nil then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by simp (metis add_Suc_right less_SucI less_add_Suc1 trans_less_add2)
qed

text‹No singleton @{const Parallel} is equal to its own child, because the child has to be smaller›
lemma parallel_neq_single [simp]:
  "Parallel [a] ≠ a"
proof -
  have "⋀f g. size_res_term f g a < size_res_term f g (Parallel [a])"
    using parallel_child_smaller by simp
  then show ?thesis
    by fastforce
qed

subsection‹Resource Term Equivalence›

text‹
  Some resource terms are different descriptions of the same situation.
  We express this by relating resource terms as follows:
  ▪ @{term "Parallel []"} with @{term "Empty"}
  ▪ @{term "Parallel [x]"} with @{term "x"}
  ▪ @{term "Parallel (xs @ [Parallel ys] @ zs)"} with @{term "Parallel (xs @ ys @ zs)"}

  We extend this with the reflexive base cases, recursive cases and symmetric-transitive closure.
  As a result, we get an equivalence relation on resource terms, which we will later use to quotient
  the terms and form a type of resources.
›
inductive res_term_equiv :: "('a, 'b) res_term ⇒ ('a, 'b) res_term ⇒ bool" (infix "∼" 100)
  where
    nil: "Parallel [] ∼ Empty"
  | singleton: "Parallel [a] ∼ a"
  | merge: "Parallel (x @ [Parallel y] @ z) ∼ Parallel (x @ y @ z)"
  | empty: "Empty ∼ Empty"
  | anything: "Anything ∼ Anything"
  | res: "Res x ∼ Res x"
  | copyable: "Copyable x ∼ Copyable x"
  | parallel: "list_all2 (∼) xs ys ⟹ Parallel xs ∼ Parallel ys"
  | nondet: "⟦x ∼ y; u ∼ v⟧ ⟹ NonD x u ∼ NonD y v"
  | executable: "⟦x ∼ y; u ∼ v⟧ ⟹ Executable x u ∼ Executable y v"
  | repeatable: "⟦x ∼ y; u ∼ v⟧ ⟹ Repeatable x u ∼ Repeatable y v"
  | sym [sym]: "x ∼ y ⟹ y ∼ x"
  | trans [trans]: "⟦x ∼ y; y ∼ z⟧ ⟹ x ∼ z"

text‹Add some of the rules for the simplifier›
lemmas [simp] =
  nil nil[symmetric]
  singleton singleton[symmetric]

text‹Constrain all these rules to the resource term equivalence namespace›
hide_fact (open) empty anything res copyable nil singleton merge parallel nondet executable
  repeatable sym trans

text‹Next we derive a handful of rules for the equivalence, placing them in its namespace›
setup ‹Sign.mandatory_path "res_term_equiv"›

text‹It can be shown to be reflexive›
lemma refl [simp]:
  "a ∼ a"
  by (induct a ; rule res_term_equiv.intros ; simp add: list_all2_same)

lemma reflI:
  "a = b ⟹ a ∼ b"
  by simp

lemma equivp [simp]:
  "equivp res_term_equiv"
  by (simp add: equivpI reflpI res_term_equiv.sym res_term_equiv.trans sympI transpI)

text‹Parallel resource terms can be related by splitting them into parts›
lemma decompose:
  assumes "Parallel x1 ∼ Parallel y1"
      and "Parallel x2 ∼ Parallel y2"
    shows "Parallel (x1 @ x2) ∼ Parallel (y1 @ y2)"
proof -
  have "Parallel [Parallel x1, Parallel x2] ∼ Parallel [Parallel y1, Parallel y2]"
    by (simp add: assms res_term_equiv.parallel)
  then have "Parallel (Parallel x1 # x2) ∼ Parallel (Parallel y1 # y2)"
    using res_term_equiv.merge[of "[Parallel x1]" x2 Nil, simplified]
          res_term_equiv.merge[of "[Parallel y1]" y2 Nil, simplified]
    by (meson res_term_equiv.sym res_term_equiv.trans)
  then show "Parallel (x1 @ x2) ∼ Parallel (y1 @ y2)"
    using res_term_equiv.merge[of Nil y1 y2, simplified]
          res_term_equiv.merge[of Nil x1 x2, simplified]
    by (meson res_term_equiv.sym res_term_equiv.trans)
qed

text‹We can drop a unit from any parallel resource term›
lemma drop:
  "Parallel (x @ [Empty] @ y) ∼ Parallel (x @ y)"
proof -
  have "Parallel [Empty] ∼ Parallel [Parallel []]"
    using res_term_equiv.nil res_term_equiv.sym res_term_equiv.trans res_term_equiv.singleton
    by blast
  then have "Parallel (x @ [Empty] @ y) ∼ Parallel (x @ [Parallel []] @ y)"
    using res_term_equiv.decompose[OF res_term_equiv.refl, of "[Empty] @ y" "[Parallel []] @ y" x]
          res_term_equiv.decompose[OF _ res_term_equiv.refl, of "[Empty]" "[Parallel []]" y]
    by blast
  then show ?thesis
    using res_term_equiv.merge res_term_equiv.trans by fastforce
qed

text‹Equivalent resource terms remain equivalent wrapped in a parallel›
lemma singleton_both:
  "x ∼ y ⟹ Parallel [x] ∼ Parallel [y]"
  by (simp add: res_term_equiv.parallel)

text‹We can reduce a resource term equivalence given equivalences for both sides›
lemma trans_both:
  "⟦a ∼ x; y ∼ b; x ∼ y⟧ ⟹ a ∼ b"
  by (rule res_term_equiv.trans[OF res_term_equiv.trans])

setup ‹Sign.parent_path›

experiment begin
lemma "Parallel [Parallel [], Empty] ∼ Empty"
proof -
  have "Parallel [Parallel [], Empty] ∼ Parallel [Parallel []]"
    using res_term_equiv.drop[of "[Parallel []]"] by simp
  also have "... ∼ Parallel []" by simp
  also have "... ∼ Empty" by simp
  finally show ?thesis .
qed
end

text‹Inserting equivalent terms anywhere in equivalent parallel terms preserves the equivalence›
lemma res_term_parallel_insert:
  assumes "Parallel x ∼ Parallel y"
      and "Parallel u ∼ Parallel v"
      and "a ∼ b"
    shows "Parallel (x @ [a] @ u) ∼ Parallel (y @ [b] @ v)"
  by (meson assms res_term_equiv.decompose res_term_equiv.singleton_both)
text‹With inserting at the start being just a special case›
lemma res_term_parallel_cons:
  assumes "Parallel x ∼ Parallel y"
      and "a ∼ b"
    shows "Parallel (a # x) ∼ Parallel (b # y)"
  using res_term_parallel_insert[OF res_term_equiv.refl assms, of Nil] by simp

text‹@{const Empty} is a unit for binary @{const Parallel}›
lemma res_term_parallel_emptyR [simp]: "Parallel [x, Empty] ∼ x"
  using res_term_equiv.drop[of "[x]" Nil] by (simp add: res_term_equiv.trans)
lemma res_term_parallel_emptyL [simp]: "Parallel [Empty, x] ∼ x"
  using res_term_equiv.drop[of Nil "[x]"] by (simp add: res_term_equiv.trans)

text‹Term equivalence is preserved by parallel on either side›
lemma res_term_equiv_parallel [simp]:
  "x ∼ y ⟹ x ∼ Parallel [y]"
  using res_term_equiv.singleton res_term_equiv.sym res_term_equiv.trans by blast
lemmas [simp] = res_term_equiv_parallel[symmetric]

text‹Resource term map preserves equivalence:›
lemma map_res_term_preserves_equiv [simp]:
  "x ∼ y ⟹ map_res_term f g x ∼ map_res_term f g y"
proof (induct rule: res_term_equiv.induct)
     case empty then show ?case by simp
next case anything then show ?case by simp
next case (res x) then show ?case by simp
next case (copyable x) then show ?case by simp
next case nil then show ?case by simp
next case (singleton a) then show ?case by simp
next case (merge x y z) then show ?case using res_term_equiv.merge by fastforce
next
  case (parallel xs ys)
  then show ?case
    by (simp add: list_all2_conv_all_nth res_term_equiv.parallel)
next case (nondet x y u v) then show ?case by (simp add: res_term_equiv.nondet)
next case (executable x y u v) then show ?case by (simp add: res_term_equiv.executable)
next case (repeatable x y u v) then show ?case by (simp add: res_term_equiv.repeatable)
next case (sym x y) then show ?case by (simp add: res_term_equiv.sym)
next case (trans x y z) then show ?case using res_term_equiv.trans by blast
qed

text‹
  The other direction is not true in general, because they may be new equivalences created by
  mapping different atoms to the same one.
  However, the counter-example proof requires a decision procedure for the equivalence to prove
  that two distinct atoms are not equivalent terms.
  As such, we delay it until normalisation for the terms is established.
›

subsection‹Parallel Parts›

text‹
  Parallel resources often arise in processes, because they describe the frequent situation of
  having multiple resources be simultaneously present.
  With resource terms, the way this situation is expressed can get complex.
  To simplify it, we define a function to extract the list of parallel resource terms, traversing
  nested @{const Parallel} terms and dropping any @{const Empty} resources in them.
  We call these the parallel parts.
›
primrec parallel_parts :: "('a, 'b) res_term ⇒ ('a, 'b) res_term list"
  where
    "parallel_parts Empty = []"
  | "parallel_parts Anything = [Anything]"
  | "parallel_parts (Res a) = [Res a]"
  | "parallel_parts (Copyable a) = [Copyable a]"
  | "parallel_parts (Parallel xs) = concat (map parallel_parts xs)"
  | "parallel_parts (NonD a b) = [NonD a b]"
  | "parallel_parts (Executable a b) = [Executable a b]"
  | "parallel_parts (Repeatable a b) = [Repeatable a b]"

text‹Every resource is equivalent to combining its parallel parts in parallel›
lemma parallel_parts_eq:
  "x ∼ Parallel (parallel_parts x)"
proof (induct x)
     case Empty then show ?case by simp
next case Anything then show ?case by simp
next case (Res x) then show ?case by simp
next case (Copyable x) then show ?case by simp
next
  case (Parallel xs)
  then show ?case
  proof (induct xs)
    case Nil then show ?case by simp
  next
    case (Cons a x)
    then have a1: "a ∼ Parallel (parallel_parts a)"
          and a2: "Parallel x ∼ Parallel (parallel_parts (Parallel x))"
      by simp_all

    have "Parallel [a] ∼ Parallel (parallel_parts a)"
      using a1 res_term_equiv.trans res_term_equiv.singleton by blast
    then have "Parallel (a # x) ∼ Parallel (parallel_parts a @ parallel_parts (Parallel x))"
      using res_term_equiv.decompose[OF _ a2, of "[a]"] by simp
    then show ?case
      by simp
  qed
next case (NonD x1 x2) then show ?case by simp
next case (Executable x1 x2) then show ?case by simp
next case (Repeatable x1 x2) then show ?case by simp
qed

text‹Equivalent parallel parts is the same as equivalent resource terms›
lemma equiv_parallel_parts:
  "list_all2 (∼) (parallel_parts a) (parallel_parts b) = a ∼ b"
proof
  show "list_all2 (∼) (parallel_parts a) (parallel_parts b) ⟹ a ∼ b"
    by (meson res_term_equiv.parallel parallel_parts_eq res_term_equiv.sym res_term_equiv.trans)
  show "a ∼ b ⟹ list_all2 (∼) (parallel_parts a) (parallel_parts b)"
  proof (induct rule: res_term_equiv.induct)
       case empty then show ?case by simp
  next case anything then show ?case by simp
  next case (res x) then show ?case by simp
  next case (copyable x) then show ?case by simp
  next case nil then show ?case by simp
  next case (singleton a) then show ?case by (simp add: list_all2_refl)
  next case (merge x y z) then show ?case by (simp add: list_all2_refl)
  next
    case (parallel xs ys)
    then show ?case
      by (induct rule: list_all2_induct ; simp add: list_all2_appendI)
  next case (nondet x y u v) then show ?case by (simp add: res_term_equiv.nondet)
  next case (executable x y u v) then show ?case by (simp add: res_term_equiv.executable)
  next case (repeatable x y u v) then show ?case by (simp add: res_term_equiv.repeatable)
  next case (sym x y) then show ?case by (simp add: list_all2_conv_all_nth res_term_equiv.sym)
  next case (trans x y z) then show ?case using res_term_equiv.trans list_all2_trans by blast
  qed
qed

text‹Note that resource term equivalence does not imply parallel parts equality›
lemma
  obtains x y where "x ∼ y" and "parallel_parts x ≠ parallel_parts y"
proof
  let ?x = "NonD (Parallel [Anything, Empty]) (Parallel [])"
  let ?y = "NonD Anything Empty"

  show "?x ∼ ?y"
    by (simp add: res_term_equiv.nondet)
  show "parallel_parts ?x ≠ parallel_parts ?y"
    by simp
qed
text‹But it does imply that both have equal number of parallel parts›
lemma parallel_parts_length_eq:
  "x ∼ y ⟹ length (parallel_parts x) = length (parallel_parts y)"
  using equiv_parallel_parts list_all2_lengthD by blast

text‹Empty parallel parts, however, is the same as equivalence to the unit›
lemma parallel_parts_nil_equiv_empty:
  "(parallel_parts a = []) = a ∼ Empty"
  using equiv_parallel_parts list.rel_sel parallel_parts.simps(1) by blast

text‹Singleton parallel parts imply equivalence to the one element›
lemma parallel_parts_single_equiv_element:
  "parallel_parts a = [x] ⟹ a ∼ x"
  using parallel_parts_eq res_term_equiv.trans by force

text‹No element of parallel parts is @{const Parallel} or @{const Empty}›
lemma parallel_parts_have_no_empty:
  "x ∈ set (parallel_parts a) ⟹ ¬ is_Empty x"
  by (induct a) fastforce+
lemma parallel_parts_have_no_par:
  "x ∈ set (parallel_parts a) ⟹ ¬ is_Parallel x"
  by (induct a) fastforce+

text‹Every parallel part of a resource is at most as big as it›
lemma parallel_parts_not_bigger:
  "x ∈ set (parallel_parts a) ⟹ size_res_term f g x ≤ (size_res_term f g a)"
proof (induct a)
     case Empty then show ?case by simp
next case Anything then show ?case by simp
next case (Res x) then show ?case by simp
next case (Copyable x) then show ?case by simp
next
  case (Parallel x)
  then show ?case
    by (clarsimp simp add: le_SucI size_list_estimation')
next case (NonD a1 a2) then show ?case by simp
next case (Executable a1 a2) then show ?case by simp
next case (Repeatable a1 a2) then show ?case by simp
qed

text‹Any resource that is not @{const Empty} or @{const Parallel} has itself as parallel part›
lemma parallel_parts_self [simp]:
  "⟦¬ is_Empty x; ¬ is_Parallel x⟧ ⟹ parallel_parts x = [x]"
  by (cases x) simp_all

text‹
  List of terms with no @{const Empty} or @{const Parallel} elements is the same as parallel parts
  of the @{const Parallel} term build from it
›
lemma parallel_parts_no_empty_parallel:
  assumes "¬ list_ex is_Empty xs"
      and "¬ list_ex is_Parallel xs"
    shows "parallel_parts (Parallel xs) = xs"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp)
qed

subsection‹Parallelisation›

text‹
  In the opposite direction of parallel parts, we can take a list of resource terms and combine them
  in parallel in a way smarter than just using @{const Parallel}.
  This rests in checking the list length, using the @{const Empty} resource if it is empty and
  skipping the wrapping in @{const Parallel} if it has only a single element.
  We call this parallelisation.
›
fun parallelise :: "('a, 'b) res_term list ⇒ ('a, 'b) res_term"
  where
    "parallelise [] = Empty"
  | "parallelise [x] = x"
  | "parallelise xs = Parallel xs"

text‹This produces equivalent results to the @{const Parallel} constructor›
lemma parallelise_equiv:
  "parallelise xs ∼ Parallel xs"
  by (cases xs rule: parallelise.cases) simp_all

text‹Lists of equal length that parallelise to the same term must have been equal›
lemma parallelise_same_length:
  "⟦parallelise x = parallelise y; length x = length y⟧ ⟹ x = y"
  by (elim parallelise.elims) simp_all

text‹Parallelisation and naive parallel combination have the same parallel parts›
lemma parallel_parts_parallelise_eq:
  "parallel_parts (parallelise xs) = parallel_parts (Parallel xs)"
  by (cases xs rule: parallelise.cases) simp_all

text‹
  Parallelising to a @{const Parallel} term means the input is either:
  ▪ A singleton set containing just that resulting @{const Parallel} term, or
  ▪ Exactly the children of the output and with at least two elements.
›
lemma parallelise_to_parallel_conv:
  "(parallelise xs = Parallel ys) = (xs = [Parallel ys] ∨ (1 < length xs ∧ xs = ys))"
proof
  show "parallelise xs = Parallel ys ⟹ xs = [Parallel ys] ∨ 1 < length xs ∧ xs = ys"
    by (fastforce elim: parallelise.elims)
  have "xs = [Parallel ys] ⟹ parallelise xs = Parallel ys"
    by simp
  moreover have "1 < length xs ∧ xs = ys ⟹ parallelise xs = Parallel ys"
    by simp (metis Suc_lessD length_Cons list.size(3) nat_neq_iff parallelise.elims)
  ultimately show "xs = [Parallel ys] ∨ 1 < length xs ∧ xs = ys ⟹ parallelise xs = Parallel ys"
    by blast
qed

text‹
  So parallelising to a @{const Parallel} term with the same children is the same as the list having
  at least two elements
›
lemma parallelise_to_parallel_same_length:
  "(parallelise xs = Parallel xs) = (1 < length xs)"
  by (simp add: parallelise_to_parallel_conv) (metis parallel_neq_single)

text‹
  If the output of parallelisation contains a nested @{const Parallel} term then so must have the
  input list
›
lemma parallelise_to_parallel_has_paralell:
  assumes "parallelise xs = Parallel ys"
      and "list_ex is_Parallel ys"
    shows "list_ex is_Parallel xs"
  using assms by (induct xs rule: parallelise.induct) simp_all

text‹If the output of parallelisation contains @{const Empty} then so must have the input›
lemma parallelise_to_parallel_has_empty:
  assumes "parallelise xs = Parallel ys"
  obtains "xs = [Parallel ys]"
        | "xs = ys"
  using assms parallelise_to_parallel_conv by blast

text‹Parallelising to @{const Empty} means the input list was either empty or contained just that›
lemma parallelise_to_empty_eq:
  assumes "parallelise xs = Empty"
  obtains "xs = []"
        | "xs = [Empty]"
  using assms parallelise.elims by blast

text‹
  If a list parallelises to anything but @{const Parallel} or @{const Empty}, then it must have been
  a singleton of that term
›
lemma parallelise_to_single_eq:
  assumes "parallelise xs = a"
      and "¬ is_Empty a"
      and "¬ is_Parallel a"
    shows "xs = [a]"
  using assms by (cases xs rule: parallelise.cases ; fastforce)

text‹Sets of atoms after parallelisation are unions of those atoms sets for the inputs›
lemma set1_res_term_parallelise [simp]:
  "set1_res_term (ResTerm.parallelise xs) = ⋃(set1_res_term ` set xs)"
  by (induct xs rule: parallelise.induct) simp_all
lemma set2_res_term_parallelise [simp]:
  "set2_res_term (ResTerm.parallelise xs) = ⋃(set2_res_term ` set xs)"
  by (induct xs rule: parallelise.induct) simp_all

subsection‹Refinement›

text‹
  Resource term refinement applies two functions to the linear and copyable atoms in a term.
  Unlike @{const map_res_term}, the first function (applied to linear atoms) is allowed to produce
  full resource terms, not just other atoms.
  (The second function must still produce other atoms, because we cannot replace a copyable atom
  with an arbitrary, possibly not copyable, resource.)
  This allows us to refine atoms into potentially complex terms.
›
primrec refine_res_term ::
    "('a ⇒ ('x, 'y) res_term) ⇒ ('b ⇒ 'y) ⇒ ('a, 'b) res_term ⇒ ('x, 'y) res_term"
  where
    "refine_res_term f g Empty = Empty"
  | "refine_res_term f g Anything = Anything"
  | "refine_res_term f g (Res a) = f a"
  | "refine_res_term f g (Copyable x) = Copyable (g x)"
  | "refine_res_term f g (Parallel xs) = Parallel (map (refine_res_term f g) xs)"
  | "refine_res_term f g (NonD x y) = NonD (refine_res_term f g x) (refine_res_term f g y)"
  | "refine_res_term f g (Executable x y) =
      Executable (refine_res_term f g x) (refine_res_term f g y)"
  | "refine_res_term f g (Repeatable x y) =
      Repeatable (refine_res_term f g x) (refine_res_term f g y)"

text‹
  Two refined resources are equivalent if:
  ▪ the original resources were equivalent,
  ▪ the linear atom refinements produce equivalent terms and
  ▪ the copyable atom refinements produce identical atoms.
›
lemma refine_res_term_eq:
  assumes "x ∼ y"
      and "⋀x. f x ∼ f' x"
      and "⋀x. g x = g' x"
    shows "refine_res_term f g x ∼ refine_res_term f' g' y"
proof -
  have reflexivity: "refine_res_term f g a ∼ refine_res_term f' g' a" for a
  ― ‹First we prove the simpler case where the two resources are equal, so we can use it later›
  proof (induct a)
       case Empty then show ?case by simp
  next case Anything then show ?case by simp
  next case (Res x) then show ?case using assms(2) by simp
  next case (Copyable x) then show ?case using assms(3) by simp
  next
    case (Parallel x)
    then show ?case
      by (clarsimp intro!: res_term_equiv.parallel)
         (metis (mono_tags, lifting) length_map list_all2_all_nthI nth_map nth_mem)
  next case (NonD a1 a2) then show ?case by (simp add: res_term_equiv.nondet)
  next case (Executable a1 a2) then show ?case by (simp add: res_term_equiv.executable)
  next case (Repeatable a1 a2) then show ?case by (simp add: res_term_equiv.repeatable)
  qed

  from assms show ?thesis
  ― ‹Then we prove the general statement by induction on assumed equivalence›
  proof (induct rule: res_term_equiv.induct)
       case empty then show ?case by simp
  next case anything then show ?case by simp
  next case (res x) then show ?case by simp
  next case (copyable x) then show ?case by simp
  next case nil then show ?case by simp
  next
    case (singleton a)
    then have "refine_res_term f g (Parallel [a]) ∼ refine_res_term f g a"
      by simp
    then show ?case
      using reflexivity res_term_equiv.trans by metis
  next
    case (merge x y z)
    have
      " length (map (refine_res_term f g') x @
          map (refine_res_term f g') y @ map (refine_res_term f g') z)
      = length (map (refine_res_term f' g') x @
          map (refine_res_term f' g') y @ map (refine_res_term f' g') z)"
      by simp
    moreover have
      " ((map (refine_res_term f g) x @
            map (refine_res_term f g) y @ map (refine_res_term f g) z) ! i)
      ∼ ((map (refine_res_term f' g') x @
            map (refine_res_term f' g') y @ map (refine_res_term f' g') z) ! i)"
      if "i < length x + length y + length z" for i
      by (metis append.assoc length_append map_append nth_map reflexivity that)
    ultimately have
      " list_all2 (∼)
          ( map (refine_res_term f g) x
          @ map (refine_res_term f g) y
          @ map (refine_res_term f g) z)
          ( map (refine_res_term f' g') x
          @ map (refine_res_term f' g') y
          @ map (refine_res_term f' g') z)"
      by (smt (verit, del_insts) append_assoc length_append length_map list_all2_all_nthI)
    then have
      " Parallel (map (refine_res_term f g) x @
          [Parallel (map (refine_res_term f g) y)] @ map (refine_res_term f g) z)
      ∼ Parallel (map (refine_res_term f' g') x @
          map (refine_res_term f' g') y @ map (refine_res_term f' g') z)"
      using res_term_equiv.merge res_term_equiv.parallel res_term_equiv.trans by blast
    then show ?case
      by simp
  next
    case (parallel xs ys)
    then show ?case
      by (simp add: res_term_equiv.parallel list_all2_conv_all_nth)
  next case (nondet x y u v) then show ?case by (simp add: res_term_equiv.nondet)
  next case (executable x y u v) then show ?case by (simp add: res_term_equiv.executable)
  next case (repeatable x y u v) then show ?case by (simp add: res_term_equiv.repeatable)
  next
    case (sym x y)
    then show ?case
      by (metis res_term_equiv.sym res_term_equiv.trans reflexivity)
  next
    case (trans x y z)
    then show ?case
      by (metis res_term_equiv.sym res_term_equiv.trans reflexivity)
  qed
qed

subsection‹Removing @{const Empty} Terms From a List›

text‹
  As part of simplifying resource terms, it is sometimes useful to be able to take a list of terms
  and drop from it any empty resource.
›
primrec remove_all_empty :: "('a, 'b) res_term list ⇒ ('a, 'b) res_term list"
  where
    "remove_all_empty [] = []"
  | "remove_all_empty (x#xs) = (if is_Empty x then remove_all_empty xs else x#remove_all_empty xs)"

text‹
  The result of dropping @{const Empty} terms from a list of resource terms is a subset of the
  original list
›
lemma remove_all_empty_subset:
  "x ∈ set (remove_all_empty xs) ⟹ x ∈ set xs"
proof (induct xs)
  case Nil then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by simp (metis (full_types) set_ConsD)
qed

text‹If there are no @{const Empty} terms then removing them is the same as not doing anything›
lemma remove_all_empty_none:
  "¬ list_ex is_Empty xs ⟹ remove_all_empty xs = xs"
  by (induct xs ; force)

text‹There are no @{const Empty} terms left after they are removed›
lemma remove_all_empty_result:
  "¬ list_ex is_Empty (remove_all_empty xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp)
qed

text‹Removing @{const Empty} terms distributes over appending lists›
lemma remove_all_empty_append:
  "remove_all_empty (xs @ ys) = remove_all_empty xs @ remove_all_empty ys"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp)
qed

text‹Removing @{const Empty} terms distributes over constructing lists›
lemma remove_all_empty_Cons:
  "remove_all_empty (x # xs) = remove_all_empty [x] @ remove_all_empty xs"
  using remove_all_empty_append by (metis append.left_neutral append_Cons)

text‹
  Removing @{const Empty} terms from children of a parallel resource term results in an equivalent
  term
›
lemma remove_all_empty_equiv:
  "Parallel xs ∼ Parallel (remove_all_empty xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (metis append.left_neutral append_Cons remove_all_empty.simps(2) res_term_equiv.drop
        res_term_equiv.refl res_term_equiv.trans res_term_parallel_cons is_Empty_def)
qed

text‹Removing @{const Empty} terms does not affect the atom sets›
lemma set1_res_term_remove_all_empty [simp]:
  "⋃(set1_res_term ` set (remove_all_empty xs)) = ⋃(set1_res_term ` set xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (cases a) simp_all
qed
lemma set2_res_term_remove_all_empty [simp]:
  "⋃(set2_res_term ` set (remove_all_empty xs)) = ⋃(set2_res_term ` set xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (cases a) simp_all
qed

subsection‹Merging Nested @{const Parallel} Terms in a List›

text‹
  Similarly, it is sometimes useful to be able to take a list of terms and merge the children of any
  @{const Parallel} term in it up into the list itself
›
primrec merge_all_parallel :: "('a, 'b) res_term list ⇒ ('a, 'b) res_term list"
  where
    "merge_all_parallel [] = []"
  | "merge_all_parallel (x#xs) =
      (case x of Parallel y ⇒ y @ merge_all_parallel xs | _ ⇒ x # merge_all_parallel xs)"

text‹If there are no @{const Parallel} terms then merging them is the same as not doing anything›
lemma merge_all_parallel_none:
  "¬ list_ex is_Parallel xs ⟹ merge_all_parallel xs = xs"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp)
qed

text‹
  If no element of the input list has itself nested @{const Parallel} terms then there will be none
  left after merging @{const Parallel} terms in the list
›
lemma merge_all_parallel_result:
  assumes "⋀ys. Parallel ys ∈ set xs ⟹ ¬ list_ex is_Parallel ys"
    shows "¬ list_ex is_Parallel (merge_all_parallel xs)"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; fastforce)
qed

text‹Merging nested @{const Parallel} terms distributes over appending lists›
lemma merge_all_parallel_append:
  "merge_all_parallel (xs @ ys) = merge_all_parallel xs @ merge_all_parallel ys"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp)
qed

text‹Merging @{const Parallel} terms distributes over constructing lists›
lemma merge_all_parallel_Cons:
  "merge_all_parallel (x # xs) = merge_all_parallel [x] @ merge_all_parallel xs"
  using merge_all_parallel_append by (metis append.left_neutral append_Cons)

text‹
  Merging @{const Parallel} terms nested in another @{const Parallel} term results in an equivalent
  term
›
lemma merge_all_parallel_equiv:
  "Parallel xs ∼ Parallel (merge_all_parallel xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  have ?case if "a = Parallel as" for as
    using Cons
    by (simp add: that)
       (metis append.left_neutral append_Cons res_term_equiv.decompose res_term_equiv.singleton)
  moreover have ?case if "⋀as. a ≠ Parallel as"
    using Cons by (cases a) (simp_all add: that res_term_parallel_cons)
  ultimately show ?case
    by metis
qed

text‹
  If the output of @{const merge_all_parallel} contains @{const Empty} then:
  ▪ It was nested in one of the input elements, or
  ▪ It was in the input.
›
lemma merge_all_parallel_has_empty:
  assumes "list_ex is_Empty (merge_all_parallel xs)"
  obtains ys where "Parallel ys ∈ set xs" and "list_ex is_Empty ys"
        | "list_ex is_Empty xs"
  using assms
proof (induct xs)
  case Nil then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a) fastforce+
qed

text‹Merging @{const Parallel} terms does not affect the atom sets›
lemma set1_res_term_merge_all_parallel [simp]:
  "⋃(set1_res_term ` set (merge_all_parallel xs)) = ⋃(set1_res_term ` set xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (cases a) simp_all
qed
lemma set2_res_term_merge_all_parallel [simp]:
  "⋃(set2_res_term ` set (merge_all_parallel xs)) = ⋃(set2_res_term ` set xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (cases a) simp_all
qed

end