Theory ResNormRewrite

theory ResNormRewrite
  imports
    ResNormalForm
    "Abstract-Rewriting.Abstract_Rewriting"
    Util
begin

section‹Rewriting Resource Term Normalisation›

text‹
  This resource term normalisation procedure is based on the following rewrite rules:
  ▪ @{text "Parallel [] → Empty"}
  ▪ @{text "Parallel [a] → a"}
  ▪ @{text "Parallel (x @ [Parallel y] @ z) → Parallel (x @ y @ z)"}
  ▪ @{text "Parallel (x @ [Empty] @ y) → Parallel (x @ y)"}

  This represents the one-directional, single-step version of resource term equivalence.
  Note that the last rule must be made explicit here, because its counterpart theorem
  @{thm res_term_equiv.drop} can only be derived thanks to symmetry.
›

subsection‹Rewriting Relation›

text‹
  The rewriting relation contains a rewriting rule for each introduction rule of
  @{const res_term_equiv} except for symmetry and transitivity, and an explicit rule for
  @{thm res_term_equiv.drop}.
›
inductive res_term_rewrite :: "('a, 'b) res_term ⇒ ('a, 'b) res_term ⇒ bool" where
  empty: "res_term_rewrite Empty Empty"
| anything: "res_term_rewrite Anything Anything"
| res: "res_term_rewrite (Res x) (Res x)"
| copyable: "res_term_rewrite (Copyable x) (Copyable x)"
| nil: "res_term_rewrite (Parallel []) Empty"
| singleton: "res_term_rewrite (Parallel [a]) a"
| merge: "res_term_rewrite (Parallel (x @ [Parallel y] @ z)) (Parallel (x @ y @ z))"
| drop: "res_term_rewrite (Parallel (x @ [Empty] @ z)) (Parallel (x @ z))"
| parallel: "list_all2 res_term_rewrite xs ys ⟹ res_term_rewrite (Parallel xs) (Parallel ys)"
| nondet: "⟦res_term_rewrite x y; res_term_rewrite u v⟧ ⟹ res_term_rewrite (NonD x u) (NonD y v)"
| executable: "⟦res_term_rewrite x y; res_term_rewrite u v⟧ ⟹
    res_term_rewrite (Executable x u) (Executable y v)"
| repeatable: "⟦res_term_rewrite x y; res_term_rewrite u v⟧ ⟹
    res_term_rewrite (Repeatable x u) (Repeatable y v)"

hide_fact (open) empty anything res copyable nil singleton merge drop parallel nondet executable
  repeatable

setup ‹Sign.mandatory_path "res_term_rewrite"›

text‹The rewrite relation is reflexive›
lemma refl [simp]:
  "res_term_rewrite x x"
proof (induct x)
     case Empty then show ?case by (rule res_term_rewrite.empty)
next case Anything then show ?case by (rule res_term_rewrite.anything)
next case (Res x) then show ?case by (rule res_term_rewrite.res)
next case (Copyable x) then show ?case by (rule res_term_rewrite.copyable)
next
  case (Parallel x)
  then show ?case
    by (simp add: res_term_rewrite.parallel list.rel_refl_strong)
next case (NonD x1 x2) then show ?case by (rule res_term_rewrite.nondet)
next case (Executable x1 x2) then show ?case by (rule res_term_rewrite.executable)
next case (Repeatable x1 x2) then show ?case by (rule res_term_rewrite.repeatable)
qed

lemma parallel_one:
  "res_term_rewrite a b ⟹ res_term_rewrite (Parallel (xs @ [a] @ ys)) (Parallel (xs @ [b] @ ys))"
  using res_term_rewrite.refl res_term_rewrite.parallel
  by (metis list.rel_refl list_all2_Cons2 list_all2_appendI)

setup ‹Sign.parent_path›

text‹Every term rewrites to an equivalent term›
lemma res_term_rewrite_imp_equiv:
  "res_term_rewrite x y ⟹ x ∼ y"
proof (induct x y rule: res_term_rewrite.induct)
     case empty then show ?case by (rule res_term_equiv.empty)
next case anything then show ?case by (rule res_term_equiv.anything)
next case (res x) then show ?case by (rule res_term_equiv.res)
next case (copyable x) then show ?case by (intro res_term_equiv.copyable)
next case nil then show ?case by (rule res_term_equiv.nil)
next case (singleton a) then show ?case by (rule res_term_equiv.singleton)
next case (merge x y z) then show ?case by (rule res_term_equiv.merge)
next case (drop x z) then show ?case by (rule res_term_equiv.drop)
next
  case (parallel xs ys)
  then show ?case
    using res_term_equiv.parallel list_all2_mono by blast
next case (nondet x y u v) then show ?case by (intro res_term_equiv.nondet)
next case (executable x y u v) then show ?case by (intro res_term_equiv.executable)
next case (repeatable x y u v) then show ?case by (intro res_term_equiv.repeatable)
qed

text‹By transitivity of the equivalence this holds for transitive closure of the rewriting›
lemma res_term_rewrite_trancl_imp_equiv:
  "res_term_rewrite⇧+⇧+ x y ⟹ x ∼ y"
proof (induct rule: tranclp_induct)
  case (base y)
  then show ?case using res_term_rewrite_imp_equiv by blast
next
  case (step y z)
  then show ?case using res_term_rewrite_imp_equiv res_term_equiv.trans by blast
qed

text‹Normalised terms have no distinct term to which they transition›
lemma res_term_rewrite_normalised:
  assumes "normalised x"
    shows "∄y. res_term_rewrite x y ∧ x ≠ y"
proof safe
  fix y
  assume "res_term_rewrite x y"
  then have "x = y"
    using assms
  proof (induct x y rule: res_term_rewrite.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 by simp
  next case (drop x z) then show ?case by simp
  next
    case (parallel xs ys)
    then show ?case
      by simp (smt (z3) Ball_set list.rel_eq list.rel_mono_strong)
  next case (nondet x y u v) then show ?case by simp
  next case (executable x y u v) then show ?case by simp
  next case (repeatable x y u v) then show ?case by simp
  qed
  moreover assume "x ≠ y"
  ultimately show False
    by metis
qed

lemma res_term_rewrite_normalisedD:
  "⟦res_term_rewrite x y; normalised x⟧ ⟹ x = y"
  by (drule res_term_rewrite_normalised) clarsimp

text‹Whereas other terms have a distinct term to which they transition›
lemma res_term_rewrite_not_normalised:
  assumes "¬ normalised x"
    shows "∃y. res_term_rewrite x y ∧ x ≠ y"
  using assms
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 (cases "list_ex is_Parallel xs")
    case True
    then obtain a b c where "xs = a @ [Parallel b] @ c" and "list_all (λx. ¬ is_Parallel x) a"
      using obtain_first_parallel by metis
    then show ?thesis
      using Parallel res_term_rewrite.merge
      by (metis append_eq_append_conv parallel_neq_single res_term.sel(3))
  next
    case no_par: False
    then show ?thesis
    proof (cases "list_ex is_Empty xs")
      case True
    then obtain a c where "xs = a @ [Empty] @ c" and "list_all (λx. ¬ is_Empty x) a"
      using obtain_first_empty by metis
    then show ?thesis
      using no_par Parallel res_term_rewrite.drop by blast
    next
      case no_empty: False
      then show ?thesis
      proof (cases "list_ex (λx. ¬ normalised x) xs")
        case True
        then obtain a b c
          where xs: "xs = a @ [b] @ c" and "list_all normalised a" and "¬ normalised b"
          using obtain_first_unnormalised by metis
        then obtain b' where "res_term_rewrite b b'" and "b ≠ b'"
          using Parallel by (metis append_eq_Cons_conv in_set_conv_decomp)
        then have "res_term_rewrite (Parallel (a @ [b] @ c)) (Parallel (a @ [b'] @ c))"
              and "Parallel (a @ [b] @ c) ≠ Parallel (a @ [b'] @ c)"
          using res_term_rewrite.parallel_one by blast+
        then show ?thesis
          using xs by metis
      next
        case all_normal: False
        then consider "xs = []" | a where "xs = [a]"
          using no_par no_empty Parallel by (metis Bex_set normalised_parallelise parallelise.elims)
        then show ?thesis
          using res_term_rewrite.nil res_term_rewrite.singleton
          by (metis parallel_neq_single res_term.distinct(29))
      qed
    qed
  qed
next
  case (NonD x1 x2)
  then show ?case
    by (metis normalised.simps(6) res_term.inject(4) res_term_rewrite.nondet res_term_rewrite.refl)
next
  case (Executable x1 x2)
  then show ?case
    by (metis normalised.simps(7) res_term.inject(5) res_term_rewrite.executable
        res_term_rewrite.refl)
next
  case (Repeatable x1 x2)
  then show ?case
    by (metis normalised.simps(8) res_term.inject(6) res_term_rewrite.repeatable
        res_term_rewrite.refl)
qed

text‹Therefore a term is normalised iff it rewrites only back to itself›
lemma normalised_is_rewrite_refl:
  "normalised x = (∀y. res_term_rewrite x y ⟶ x = y)"
  using res_term_rewrite_normalised res_term_rewrite_not_normalised by metis

text‹Every term rewrites to one of at most equal size›
lemma res_term_rewrite_not_increase_size:
  "res_term_rewrite x y ⟹ size_res_term f g y ≤ size_res_term f g x"
  by (induct x y rule: res_term_rewrite.induct)
     (simp_all add: list_all2_conv_all_nth size_list_conv_sum_list sum_list_mono_list_all2)

subsection‹Rewriting Bound›

text‹
  There is an upper bound to how many rewriting steps could be applied to a term.
  We find it by considering the worst (most un-normalised) possible case of each node.
›
primrec res_term_rewrite_bound :: "('a, 'b) res_term ⇒ nat"
  where
    "res_term_rewrite_bound Empty = 0"
  | "res_term_rewrite_bound Anything = 0"
  | "res_term_rewrite_bound (Res a) = 0"
  | "res_term_rewrite_bound (Copyable x) = 0"
  | "res_term_rewrite_bound (Parallel xs) =
      sum_list (map res_term_rewrite_bound xs) + length xs + 1"
    ― ‹All the steps of the children, plus one for every child that could need to be merged/dropped
        and another if in the end there are less than two children.›
  | "res_term_rewrite_bound (NonD x y) = res_term_rewrite_bound x + res_term_rewrite_bound y"
  | "res_term_rewrite_bound (Executable x y) = res_term_rewrite_bound x + res_term_rewrite_bound y"
  | "res_term_rewrite_bound (Repeatable x y) = res_term_rewrite_bound x + res_term_rewrite_bound y"

text‹For un-normalised terms the bound is non-zero›
lemma res_term_rewrite_bound_not_normalised:
  "¬ normalised x ⟹ res_term_rewrite_bound x ≠ 0"
  by (induct x ; fastforce)

text‹Rewriting relation does not increase this bound›
lemma res_term_rewrite_non_increase_bound:
  "res_term_rewrite x y ⟹ res_term_rewrite_bound y ≤ res_term_rewrite_bound x"
  by (induct x y rule: res_term_rewrite.induct)
     (simp_all add: sum_list_mono_list_all2 list_all2_conv_all_nth)

subsection‹Step›

text‹
  The rewriting step function implements a specific algorithm for the rewriting relation by picking
  one approach where the relation allows multiple rewriting paths.
  To help define its parallel resource case, we first define a function to remove one @{const Empty}
  term from a list and another to merge the children of one @{const Parallel} term up into the
  containing list of terms.
›

subsubsection‹Removing One Empty›

text‹Remove the first @{const Empty} from a list of term›
fun remove_one_empty :: "('a, 'b) res_term list ⇒ ('a, 'b) res_term list"
  where
    "remove_one_empty [] = []"
  | "remove_one_empty (Empty # xs) = xs"
  | "remove_one_empty (x # xs) = x # remove_one_empty xs"

lemma remove_one_empty_cons [simp]:
  "is_Empty x ⟹ remove_one_empty (x # xs) = xs"
  "¬ is_Empty x ⟹ remove_one_empty (x # xs) = x # remove_one_empty xs"
  by (cases x ; simp)+

lemma remove_one_empty_append:
  "list_all (λx. ¬ is_Empty x) a ⟹ remove_one_empty (a @ d) = a @ remove_one_empty d"
  by (induct a ; simp)

lemma remove_one_empty_distinct:
  "list_ex is_Empty xs ⟹ remove_one_empty 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‹This is identity when there are no @{const Empty} terms›
lemma remove_one_empty_none [simp]:
  "¬ list_ex is_Empty xs ⟹ remove_one_empty xs = xs"
  by (induct xs rule: remove_one_empty.induct ; simp)

text‹This decreases length by one when there are @{const Empty} terms›
lemma length_remove_one_empty [simp]:
  "list_ex is_Empty xs ⟹ length (remove_one_empty xs) + 1 = length xs"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (cases "is_Empty a" ; simp)
qed

text‹Removing an @{const Empty} term does not increase the size›
lemma remove_one_empty_not_increase_size:
  "size_res_term f g (Parallel (remove_one_empty xs)) ≤ size_res_term f g (Parallel xs)"
  by (induct xs rule: remove_one_empty.induct ; simp)

text‹Any @{const Parallel} term is equivalent to itself with an @{const Empty} term removed›
lemma remove_one_empty_equiv:
  "Parallel xs ∼ Parallel (remove_one_empty xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
  proof (cases "is_Empty a")
    case True
    then show ?thesis
      using res_term_equiv.drop[of Nil] Cons by (fastforce simp add: is_Empty_def)
  next
    case False
    then show ?thesis
      using Cons by (simp add: res_term_parallel_cons)
  qed
qed

text‹Removing an @{const Empty} term commutes with the resource term map›
lemma remove_one_empty_map:
  "map (map_res_term f g) (remove_one_empty xs) = remove_one_empty (map (map_res_term f g) xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases "is_Empty a" ; simp)
qed

text‹
  The result of dropping an @{const Empty} from a list of resource terms is a subset of the original
  list
›
lemma remove_one_empty_subset:
  "x ∈ set (remove_one_empty xs) ⟹ x ∈ set xs"
proof (induct xs)
  case Nil then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (cases "is_Empty a" ; simp) blast
qed

subsubsection‹Merging One Parallel›

text‹Merge the first @{const Parallel} in a list of terms›
fun merge_one_parallel :: "('a, 'b) res_term list ⇒ ('a, 'b) res_term list"
  where
    "merge_one_parallel [] = []"
  | "merge_one_parallel (Parallel x # xs) = x @ xs"
  | "merge_one_parallel (x # xs) = x # merge_one_parallel xs"

lemma merge_one_parallel_cons_not [simp]:
  "¬ is_Parallel x ⟹ merge_one_parallel (x # xs) = x # merge_one_parallel xs"
  by (cases x ; simp)

lemma merge_one_parallel_append:
  "list_all (λx. ¬ is_Parallel x) a ⟹ merge_one_parallel (a @ d) = a @ merge_one_parallel d"
  for a d
  by (induct a ; simp)

lemma merge_one_parallel_distinct:
  "list_ex is_Parallel xs ⟹ merge_one_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) (metis parallel_neq_single)
qed

text‹This is identity when there are no @{const Parallel} terms›
lemma merge_one_parallel_none [simp]:
  "¬ list_ex is_Parallel xs ⟹ merge_one_parallel xs = xs"
  by (induct xs rule: merge_one_parallel.induct ; simp)

text‹Merging a @{const Parallel} term does not increase the size›
lemma merge_one_parallel_not_increase_size:
  "size_res_term f g (Parallel (merge_one_parallel xs)) ≤ 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 (cases a ; simp)
qed

text‹Any @{const Parallel} term is equivalent to itself with a @{const Parallel} term merged›
lemma merge_one_parallel_equiv:
  "Parallel xs ∼ Parallel (merge_one_parallel xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
  proof (cases "is_Parallel a")
    case True
    then show ?thesis
      using Cons res_term_equiv.merge[of Nil] by (fastforce simp add: is_Parallel_def)
  next
    case False
    then show ?thesis
      using Cons by (simp add: res_term_parallel_cons)
  qed
qed

text‹Merging a @{const Parallel} term commutes with the resource term map›
lemma merge_one_parallel_map:
  "map (map_res_term f g) (merge_one_parallel xs) = merge_one_parallel (map (map_res_term f g) xs)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp)
qed

subsubsection‹Rewriting Step Function›

text‹
  The rewriting step function itself performs one rewrite for any un-normalised input term.
  Where there are multiple choices, it proceeds as follows:
  ▪ For binary internal nodes (@{const NonD}, @{const Executable} and @{const Repeatable}), first
    fully rewrite the first child until normalised and only then start rewriting the second.
  ▪ For @{const Parallel} nodes proceed in phases:
    ▪ If any child is not normalised, rewrite all children; otherwise
    ▪ If there is some nested @{const Parallel} node in the children, merge one up; otherwise
    ▪ If there is some @{const Empty} node in the children, remove one; otherwise
    ▪ If there are no children, then return @{const Empty}; otherwise
    ▪ If there is exactly one child, then return that term; otherwise
    ▪ Do nothing and return the same term.
›
primrec step :: "('a, 'b) res_term ⇒ ('a, 'b) res_term"
  where
    "step Empty = Empty"
  | "step Anything = Anything"
  | "step (Res x) = Res x"
  | "step (Copyable x) = Copyable x"
  | "step (NonD x y) =
      ( if ¬ normalised x then NonD (step x) y
        else if ¬ normalised y then NonD x (step y)
        else NonD x y)"
  | "step (Executable x y) =
      ( if ¬ normalised x then Executable (step x) y
        else if ¬ normalised y then Executable x (step y)
        else Executable x y)"
  | "step (Repeatable x y) =
      ( if ¬ normalised x then Repeatable (step x) y
        else if ¬ normalised y then Repeatable x (step y)
        else Repeatable x y)"
  | "step (Parallel xs) =
      ( if list_ex (λx. ¬ normalised x) xs then Parallel (map step xs)
        else if list_ex is_Parallel xs then Parallel (merge_one_parallel xs)
        else if list_ex is_Empty xs then Parallel (remove_one_empty xs)
        else (case xs of
                [] ⇒ Empty
              | [a] ⇒ a
              | _ ⇒ Parallel xs))"

text‹Case split and induction for step fully expanded›
lemma step_cases
  [case_names Empty Anything Res Copyable NonD_L NonD_R NonD Executable_L Executable_R Executable
              Repeatable_L Repeatable_R Repeatable Par_Norm Par_Par Par_Empty Par_Nil Par_Single
              Par]:
  assumes "x = Empty ⟹ P"
      and "x = Anything ⟹ P"
      and "⋀a. x = Res a ⟹ P"
      and "⋀u. x = Copyable u ⟹ P"
      and "⋀u v. ⟦¬ normalised u; x = NonD u v⟧ ⟹ P"
      and "⋀u v. ⟦normalised u; ¬ normalised v; x = NonD u v⟧ ⟹ P"
      and "⋀u v. ⟦normalised u; normalised v; x = NonD u v⟧ ⟹ P"
      and "⋀u v. ⟦¬ normalised u; x = Executable u v⟧ ⟹ P"
      and "⋀u v. ⟦normalised u; ¬ normalised v; x = Executable u v⟧ ⟹ P"
      and "⋀u v. ⟦normalised u; normalised v; x = Executable u v⟧ ⟹ P"
      and "⋀u v. ⟦¬ normalised u; x = Repeatable u v⟧ ⟹ P"
      and "⋀u v. ⟦normalised u; ¬ normalised v; x = Repeatable u v⟧ ⟹ P"
      and "⋀u v. ⟦normalised u; normalised v; x = Repeatable u v⟧ ⟹ P"
      and "⋀xs. ⟦x = Parallel xs; ∃a. a ∈ set xs ∧ ¬ normalised a⟧ ⟹ P"
      and "⋀xs. ⟦x = Parallel xs; ∀a. a ∈ set xs ⟶ normalised a; list_ex is_Parallel xs⟧ ⟹ P"
      and "⋀xs. ⟦x = Parallel xs; ∀a. a ∈ set xs ⟶ normalised a;
                  list_all (λx. ¬ is_Parallel x) xs; list_ex is_Empty xs⟧ ⟹ P"
      and "x = Parallel [] ⟹ P"
      and "⋀u. ⟦x = Parallel [u]; normalised u; ¬ is_Parallel u; ¬ is_Empty u⟧ ⟹ P"
      and "⋀v vb vc. ⟦x = Parallel (v # vb # vc); ∀a. a ∈ set (v # vb # vc) ⟶ normalised a;
                      list_all (λx. ¬ is_Parallel x) (v # vb # vc);
                      list_all (λx. ¬ is_Empty x) (v # vb # vc)⟧
            ⟹ P"
    shows P
proof (cases x)
     case Empty then show ?thesis using assms by simp
next case Anything then show ?thesis using assms by simp
next case (Res x3) then show ?thesis using assms by simp
next case (Copyable x4) then show ?thesis using assms by simp
next
  case (Parallel xs)
  then show ?thesis
  proof (cases "list_ex (λx. ¬ normalised x) xs")
    case True
    then show ?thesis
      using assms(14) by (meson Bex_set Parallel)
  next
    case not_norm: False
    then show ?thesis
    proof (cases "list_ex is_Parallel xs")
      case True
      then show ?thesis
        using Parallel assms(14,15) by blast
    next
      case not_par: False
      then show ?thesis
      proof (cases "list_ex is_Empty xs")
        case True
        then show ?thesis
          by (metis not_par Parallel assms(14,16) not_list_ex)
      next
        case not_empty: False
        then show ?thesis
        proof (cases xs rule: remdups_adj.cases)
          case 1
          then show ?thesis
            by (simp add: Parallel assms(17))
        next
          case (2 x)
          then show ?thesis
            using Parallel assms(14,18) not_empty not_par by fastforce
        next
          case (3 x y xs)
          then show ?thesis
            by (metis Parallel assms(14,19) not_empty not_list_ex not_par)
        qed
      qed
    qed
  qed
next case (NonD x61 x62) then show ?thesis using assms(5-7) by blast
next case (Executable x71 x72) then show ?thesis using assms(8-10) by blast
next case (Repeatable x71 x72) then show ?thesis using assms(11-13) by blast
qed

lemma step_induct
  [case_names Empty Anything Res Copyable NonD_L NonD_R NonD Executable_L Executable_R Executable
              Repeatable_L Repeatable_R Repeatable Par_Norm Par_Par Par_Empty Par_Nil Par_Single
              Par]:
  assumes "P Empty"
      and "P Anything"
      and "⋀a. P (Res a)"
      and "⋀x. P (Copyable x)"
      and "⋀x y. ⟦P x; P y; ¬ normalised x⟧ ⟹ P (NonD x y)"
      and "⋀x y. ⟦P x; P y; normalised x; ¬ normalised y⟧ ⟹ P (NonD x y)"
      and "⋀x y. ⟦P x; P y; normalised x; normalised y⟧ ⟹ P (NonD x y)"
      and "⋀x y. ⟦P x; P y; ¬ normalised x⟧ ⟹ P (Executable x y)"
      and "⋀x y. ⟦P x; P y; normalised x; ¬ normalised y⟧ ⟹ P (Executable x y)"
      and "⋀x y. ⟦P x; P y; normalised x; normalised y⟧ ⟹ P (Executable x y)"
      and "⋀x y. ⟦P x; P y; ¬ normalised x⟧ ⟹ P (Repeatable x y)"
      and "⋀x y. ⟦P x; P y; normalised x; ¬ normalised y⟧ ⟹ P (Repeatable x y)"
      and "⋀x y. ⟦P x; P y; normalised x; normalised y⟧ ⟹ P (Repeatable x y)"
      and "⋀xs. ⟦⋀x. x ∈ set xs ⟹ P x; ∃a. a ∈ set xs ∧ ¬ normalised a⟧ ⟹ P (Parallel xs)"
      and "⋀xs. ⟦⋀x. x ∈ set xs ⟹ P x; ∀a. a ∈ set xs ⟶ normalised a; list_ex is_Parallel xs⟧
            ⟹ P (Parallel xs)"
      and "⋀xs. ⟦ ⋀x. x ∈ set xs ⟹ P x; ∀a. a ∈ set xs ⟶ normalised a
                ; list_all (λx. ¬ is_Parallel x) xs; list_ex is_Empty xs⟧
            ⟹ P (Parallel xs)"
      and "P (Parallel [])"
      and "⋀u. ⟦P u; normalised u; ¬ is_Parallel u; ¬ is_Empty u⟧ ⟹ P (Parallel [u])"
      and "⋀v vb vc.
              ⟦ ⋀x. x ∈ set (v # vb # vc) ⟹ P x; ∀a. a ∈ set (v # vb # vc) ⟶ normalised a
              ; list_all (λx. ¬ is_Parallel x) (v # vb # vc)
              ; list_all (λx. ¬ is_Empty x) (v # vb # vc)⟧
            ⟹ P (Parallel (v # vb # vc))"
    shows "P x"
proof (induct x)
     case Empty then show ?case using assms by simp
next case Anything then show ?case using assms by simp
next case (Res x) then show ?case using assms by simp
next case (Copyable x) then show ?case using assms by simp
next
  case (Parallel xs)
  then show ?case
  proof (cases "list_ex (λx. ¬ normalised x) xs")
    case True
    then show ?thesis
      using assms(14) by (metis Bex_set Parallel)
  next
    case not_norm: False
    then show ?thesis
    proof (cases "list_ex is_Parallel xs")
      case True
      then show ?thesis
        using Parallel assms(14,15) by blast
    next
      case not_par: False
      then show ?thesis
      proof (cases "list_ex is_Empty xs")
        case True
        then show ?thesis
          by (metis not_par Parallel assms(14,16) not_list_ex)
      next
        case not_empty: False
        then show ?thesis
        proof (cases xs rule: remdups_adj.cases)
          case 1
          then show ?thesis
            by (simp add: Parallel assms(17))
        next
          case (2 x)
          then show ?thesis
            using Parallel assms(14,18) not_empty not_par by fastforce
        next
          case (3 x y xs)
          then show ?thesis
            by (metis Parallel assms(14,19) not_empty not_list_ex not_par)
        qed
      qed
    qed
  qed
next case (NonD x61 x62) then show ?case using assms(5-7) by blast
next case (Executable x71 x72) then show ?case using assms(8-10) by blast
next case (Repeatable x71 x72) then show ?case using assms(11-13) by blast
qed

text‹Variant of induction with some relevant step results is also useful›
lemma step_induct'
  [case_names Empty Anything Res Copyable NonD_L NonD_R NonD Executable_L Executable_R Executable
              Repeatable_L Repeatable_R Repeatable Par_Norm Par_Par Par_Empty Par_Nil Par_Single
              Par]:
  assumes "P Empty"
      and "P Anything"
      and "⋀a. P (Res a)"
      and "⋀x. P (Copyable x)"
      and "⋀x y. ⟦P x; P y; ¬ normalised x; step (NonD x y) = NonD (step x) y⟧ ⟹ P (NonD x y)"
      and "⋀x y. ⟦P x; P y; normalised x; ¬ normalised y; step (NonD x y) = NonD x (step y)⟧
            ⟹ P (NonD x y)"
      and "⋀x y. ⟦P x; P y; normalised x; normalised y; step (NonD x y) = NonD x y⟧
            ⟹ P (NonD x y)"
      and "⋀x y. ⟦P x; P y; ¬ normalised x; step (Executable x y) = Executable (step x) y⟧
            ⟹ P (Executable x y)"
      and "⋀x y. ⟦ P x; P y; normalised x; ¬ normalised y
                  ; step (Executable x y) = Executable x (step y)⟧
            ⟹ P (Executable x y)"
      and "⋀x y. ⟦P x; P y; normalised x; normalised y; step (Executable x y) = Executable x y⟧
            ⟹ P (Executable x y)"
      and "⋀x y. ⟦P x; P y; ¬ normalised x; step (Repeatable x y) = Repeatable (step x) y⟧
            ⟹ P (Repeatable x y)"
      and "⋀x y. ⟦ P x; P y; normalised x; ¬ normalised y
                  ; step (Repeatable x y) = Repeatable x (step y)⟧
            ⟹ P (Repeatable x y)"
      and "⋀x y. ⟦P x; P y; normalised x; normalised y; step (Repeatable x y) = Repeatable x y⟧
            ⟹ P (Repeatable x y)"
      and "⋀xs. ⟦⋀x. x ∈ set xs ⟹ P x; ∃a. a ∈ set xs ∧ ¬ normalised a
                ; step (Parallel xs) = Parallel (map step xs)⟧
            ⟹ P (Parallel xs)"
      and "⋀xs. ⟦⋀x. x ∈ set xs ⟹ P x; ∀a. a ∈ set xs ⟶ normalised a; list_ex is_Parallel xs;
                  step (Parallel xs) = Parallel (merge_one_parallel xs)⟧
            ⟹ P (Parallel xs)"
      and "⋀xs. ⟦⋀x. x ∈ set xs ⟹ P x; ∀a. a ∈ set xs ⟶ normalised a
                ; list_all (λx. ¬ is_Parallel x) xs; list_ex is_Empty xs
                ; step (Parallel xs) = Parallel (remove_one_empty xs)⟧
            ⟹ P (Parallel xs)"
      and "P (Parallel [])"
      and "⋀u. ⟦P u; normalised u; ¬ is_Parallel u; ¬ is_Empty u; step (Parallel [u]) = u⟧
            ⟹ P (Parallel [u])"
      and "⋀v vb vc.
            ⟦ ⋀x. x ∈ set (v # vb # vc) ⟹ P x; ∀a. a ∈ set (v # vb # vc) ⟶ normalised a
            ; list_all (λx. ¬ is_Parallel x) (v # vb # vc)
            ; list_all (λx. ¬ is_Empty x) (v # vb # vc)
            ; step (Parallel (v # vb # vc)) = Parallel (v # vb # vc)⟧
            ⟹ P (Parallel (v # vb # vc))"
    shows "P x"
proof (induct x rule: step_induct)
     case Empty then show ?case using assms(1) by simp
next case Anything then show ?case using assms(2) by simp
next case (Res a) then show ?case using assms(3) by simp
next case (Copyable x) then show ?case using assms(4) by simp
next case (NonD_L x y) then show ?case using assms(5) by simp
next case (NonD_R x y) then show ?case using assms(6) by simp
next case (NonD x y) then show ?case using assms(7) by simp
next case (Executable_L x y) then show ?case using assms(8) by simp
next case (Executable_R x y) then show ?case using assms(9) by simp
next case (Executable x y) then show ?case using assms(10) by simp
next case (Repeatable_L x y) then show ?case using assms(11) by simp
next case (Repeatable_R x y) then show ?case using assms(12) by simp
next case (Repeatable x y) then show ?case using assms(13) by simp
next case (Par_Norm xs) then show ?case using assms(14) by (simp add: Bex_set[symmetric] Bex_def)
next case (Par_Par xs) then show ?case using assms(15) by (simp add: Bex_set[symmetric] Bex_def)
next
  case (Par_Empty xs)
  then show ?case
    using assms(15,16) by (metis (mono_tags, lifting) list_ex_iff step.simps(8))
next case Par_Nil then show ?case using assms(17) by simp
next case (Par_Single u) then show ?case using assms(18) by simp
next
  case (Par v vb vc)
  then show ?case
  proof (rule assms(19))
    show "⋀x. x ∈ set (v # vb # vc) ⟹ x ∈ set (v # vb # vc)"
      by simp
    show "step (Parallel (v # vb # vc)) = Parallel (v # vb # vc)"
      using Par by (simp add: Ball_set[symmetric] Bex_set[symmetric])
  qed
qed

text‹Set of atoms remains unchanged by rewriting step›
lemma set1_res_term_step [simp]:
  "set1_res_term (step x) = set1_res_term x"
proof (induct x rule: step_induct')
     case Empty then show ?case by simp
next case Anything then show ?case by simp
next case (Res a) then show ?case by simp
next case (Copyable x) then show ?case by simp
next case (NonD_L x y) then show ?case by simp
next case (NonD_R x y) then show ?case by simp
next case (NonD x y) then show ?case by simp
next case (Executable_L x y) then show ?case by simp
next case (Executable_R x y) then show ?case by simp
next case (Executable x y) then show ?case by simp
next case (Repeatable_L x y) then show ?case by simp
next case (Repeatable_R x y) then show ?case by simp
next case (Repeatable x y) then show ?case by simp
next case (Par_Norm xs) then show ?case by simp
next
  case (Par_Par xs)
  then show ?case
    by (fastforce elim!: obtain_first_parallel simp add: merge_one_parallel_append)
next
  case (Par_Empty xs)
  then show ?case
    by (fastforce elim!: obtain_first_empty simp add: remove_one_empty_append)
next case Par_Nil then show ?case by simp
next case (Par_Single u) then show ?case by simp
next case (Par v vb vc) then show ?case by simp
qed

lemma set2_res_term_step [simp]:
  "set2_res_term (step x) = set2_res_term x"
proof (induct x rule: step_induct')
     case Empty then show ?case by simp
next case Anything then show ?case by simp
next case (Res a) then show ?case by simp
next case (Copyable x) then show ?case by simp
next case (NonD_L x y) then show ?case by simp
next case (NonD_R x y) then show ?case by simp
next case (NonD x y) then show ?case by simp
next case (Executable_L x y) then show ?case by simp
next case (Executable_R x y) then show ?case by simp
next case (Executable x y) then show ?case by simp
next case (Repeatable_L x y) then show ?case by simp
next case (Repeatable_R x y) then show ?case by simp
next case (Repeatable x y) then show ?case by simp
next case (Par_Norm xs) then show ?case by simp
next
  case (Par_Par xs)
  then show ?case
    by (fastforce elim!: obtain_first_parallel simp add: merge_one_parallel_append)
next
  case (Par_Empty xs)
  then show ?case
    by (fastforce elim!: obtain_first_empty simp add: remove_one_empty_append)
next case Par_Nil then show ?case by simp
next case (Par_Single u) then show ?case by simp
next case (Par v vb vc) then show ?case by simp
qed

text‹
  Resource term rewriting relation contains the step function graph.
  In other words, the step function is a particular strategy implementing that rewriting.
›
lemma res_term_rewrite_contains_step:
  "res_term_rewrite x (step x)"
proof (induct x rule: step_induct')
     case Empty then show ?case by simp
next case Anything then show ?case by simp
next case (Res a) then show ?case by simp
next case (Copyable x) then show ?case by simp
next case (NonD_L x y) then show ?case by (simp add: res_term_rewrite.nondet)
next case (NonD_R x y) then show ?case by (simp add: res_term_rewrite.nondet)
next case (NonD x y) then show ?case by simp
next case (Executable_L x y) then show ?case by (simp add: res_term_rewrite.executable)
next case (Executable_R x y) then show ?case by (simp add: res_term_rewrite.executable)
next case (Executable x y) then show ?case by simp
next case (Repeatable_L x y) then show ?case by (simp add: res_term_rewrite.repeatable)
next case (Repeatable_R x y) then show ?case by (simp add: res_term_rewrite.repeatable)
next case (Repeatable x y) then show ?case by simp
next
  case (Par_Norm xs)
  then show ?case
    by (simp add: Bex_set[symmetric] res_term_rewrite.intros(9) list.rel_map(2) list_all2_same)
next
  case (Par_Par xs)
  moreover obtain a b c where "xs = a @ [Parallel b] @ c" and "list_all (λx. ¬ is_Parallel x) a"
    using Par_Par(3) obtain_first_parallel by blast
  moreover have "res_term_rewrite (Parallel (a @ [Parallel b] @ c)) (Parallel (a @ b @ c))"
    using res_term_rewrite.intros(7) .
  ultimately show ?case
    by (simp add: Bex_set[symmetric] merge_one_parallel_append)
next
  case (Par_Empty xs)
  moreover obtain a c where "xs = a @ [Empty] @ c" and "list_all (λx. ¬ is_Empty x) a"
    using Par_Empty(4) obtain_first_empty by blast
  moreover have "res_term_rewrite (Parallel (a @ [Empty] @ c)) (Parallel (a @ c))"
    using res_term_rewrite.intros(8) .
  ultimately show ?case
    by (simp add: Bex_set[symmetric] remove_one_empty_append)
next case Par_Nil then show ?case by (simp add: res_term_rewrite.intros(5))
next case (Par_Single u) then show ?case by (simp add: res_term_rewrite.intros(6))
next case (Par v vb vc) then show ?case by simp
qed

text‹Resource term being normalised is the same as the step not changing it›
lemma normalised_is_step_id:
  "normalised x = (step x = x)"
proof
  show "normalised x ⟹ step x = x"
  by (metis res_term_rewrite_contains_step res_term_rewrite_normalised)
  show "step x = x ⟹ normalised x"
  proof (induct x rule: step_induct')
       case Empty then show ?case by simp
  next case Anything then show ?case by simp
  next case (Res a) then show ?case by simp
  next case (Copyable x) then show ?case by simp
  next case (NonD_L x y) then show ?case by simp
  next case (NonD_R x y) then show ?case by simp
  next case (NonD x y) then show ?case by simp
  next case (Executable_L x y) then show ?case by simp
  next case (Executable_R x y) then show ?case by simp
  next case (Executable x y) then show ?case by simp
  next case (Repeatable_L x y) then show ?case by simp
  next case (Repeatable_R x y) then show ?case by simp
  next case (Repeatable x y) then show ?case by simp
  next case (Par_Norm xs) then show ?case by simp (metis map_eq_conv map_ident)
  next case (Par_Par xs) then show ?case by (simp add: merge_one_parallel_distinct)
  next case (Par_Empty xs) then show ?case by (simp add: remove_one_empty_distinct)
  next case Par_Nil then show ?case by simp
  next case (Par_Single u) then show ?case by simp
  next case (Par v vb vc) then show ?case by (simp add: Ball_set[symmetric])
  qed
qed

text‹So, for normalised terms we can drop any step applied to them›
lemma step_normalised [simp]:
  "normalised x ⟹ step x = x"
  using normalised_is_step_id by (rule iffD1)

text‹Rewriting step never increases the term size›
lemma step_not_increase_size:
  "size_res_term f g (step x) ≤ size_res_term f g x"
  using res_term_rewrite_not_increase_size res_term_rewrite_contains_step by blast

text‹Every resource is equivalent to itself after the step›
lemma res_term_equiv_step:
  "x ∼ step x"
  using res_term_rewrite_contains_step res_term_rewrite_imp_equiv by blast

text‹Normalisation step commutes with the resource term map›
lemma step_map:
  "map_res_term f g (step x) = step (map_res_term f g x)"
proof (induct x rule: step_induct')
     case Empty then show ?case by simp
next case Anything then show ?case by simp
next case (Res a) then show ?case by simp
next case (Copyable x) then show ?case by simp
next case (NonD_L x y) then show ?case by (simp add: normalised_map)
next case (NonD_R x y) then show ?case by (simp add: normalised_map)
next case (NonD x y) then show ?case by simp
next case (Executable_L x y) then show ?case by (simp add: normalised_map)
next case (Executable_R x y) then show ?case by (simp add: normalised_map)
next case (Executable x y) then show ?case by simp
next case (Repeatable_L x y) then show ?case by (simp add: normalised_map)
next case (Repeatable_R x y) then show ?case by (simp add: normalised_map)
next case (Repeatable x y) then show ?case by simp
next
  case (Par_Norm xs)
  then show ?case
    by (fastforce simp add: Bex_set[symmetric] normalised_map)
next
  case (Par_Par xs)
  then show ?case
    by (fastforce simp add: Bex_set[symmetric] normalised_map merge_one_parallel_map)
next
  case (Par_Empty xs)
  then show ?case
    by (simp add: Bex_set[symmetric] normalised_map remove_one_empty_map)
       (metis Ball_set)
next case Par_Nil then show ?case by simp
next case (Par_Single u) then show ?case by (simp add: normalised_map)
next
  case (Par v vb vc)
  then show ?case
    by (fastforce simp add: Bex_set[symmetric] Ball_set normalised_map)
qed

text‹Because it implements the rewriting relation, the non-increasing of bound extends to the step›
lemmas res_term_rewrite_bound_step_non_increase =
  res_term_rewrite_non_increase_bound[OF res_term_rewrite_contains_step]

text‹
  On un-normalised terms, the step actually strictly decreases the bound.
  While this should also be true of the rewriting relation it implements, the stricter way the step
  proceeds makes this proof more tractable.
›
lemma res_term_rewrite_bound_step_decrease:
  "¬ normalised x ⟹ res_term_rewrite_bound (step x) < res_term_rewrite_bound x"
proof (induct x rule: step_induct')
     case Empty then show ?case by simp
next case Anything then show ?case by simp
next case (Res a) then show ?case by simp
next case (Copyable x) then show ?case by simp
next case (NonD_L x y) then show ?case by simp
next case (NonD_R x y) then show ?case by simp
next case (NonD x y) then show ?case by simp
next case (Executable_L x y) then show ?case by simp
next case (Executable_R x y) then show ?case by simp
next case (Executable x y) then show ?case by simp
next case (Repeatable_L x y) then show ?case by simp
next case (Repeatable_R x y) then show ?case by simp
next case (Repeatable x y) then show ?case by simp
next
  case (Par_Norm xs)
  then have "(∑x←xs. res_term_rewrite_bound (step x)) < sum_list (map res_term_rewrite_bound xs)"
    by (meson res_term_rewrite_bound_step_non_increase sum_list_mono_one_strict)
  then show ?case
    using Par_Norm.hyps by (simp add: comp_def)
next
  case (Par_Par xs)
  then show ?case
    by (fastforce elim: obtain_first_parallel simp add: merge_one_parallel_append)
next
  case (Par_Empty xs)
  then show ?case
    by (fastforce elim: obtain_first_empty simp add: remove_one_empty_append)
next case Par_Nil then show ?case by simp
next case (Par_Single u) then show ?case by simp
next case (Par v vb vc) then show ?case using normalised_is_step_id by blast
qed

subsection‹Normalisation Procedure›

text‹Rewrite a resource term until normalised›
function normal_rewr :: "('a, 'b) res_term ⇒ ('a, 'b) res_term"
  where "normal_rewr x = (if normalised x then x else normal_rewr (step x))"
  by pat_completeness auto

text‹This terminates with the rewriting bound as measure, because the step keeps decreasing it›
termination normal_rewr
  using res_term_rewrite_bound_step_decrease
  by (relation "Wellfounded.measure res_term_rewrite_bound", auto)

text‹We remove the normalisation procedure definition from the simplifier, because it can loop›
lemmas [simp del] = normal_rewr.simps

text‹However, the terminal case can be safely used for simplification›
lemma normalised_normal_rewr [simp]:
  "normalised x ⟹ normal_rewr x = x"
  by (simp add: normal_rewr.simps)

text‹Normalisation produces actually normalised terms›
lemma normal_rewr_normalised:
  "normalised (normal_rewr x)"
  by (induct x rule: normal_rewr.induct, simp add: normal_rewr.simps)

text‹Normalisation is idempotent›
lemma normal_rewr_idempotent [simp]:
  "normal_rewr (normal_rewr x) = normal_rewr x"
  using normal_rewr_normalised normalised_normal_rewr by blast

text‹Normalisation absorbs rewriting step›
lemma normal_rewr_step:
  "normal_rewr x = normal_rewr (step x)"
  by (cases "normalised x") (simp_all add: normal_rewr.simps)

text‹Normalisation leaves leaf terms unchanged›
lemma normal_rewr_leaf:
  "normal_rewr Empty = Empty"
  "normal_rewr Anything = Anything"
  "normal_rewr (Res x) = Res x"
  "normal_rewr (Copyable x) = Copyable x"
  by simp_all

text‹
  Normalisation passes through @{const NonD}, @{const Executable} and @{const Repeatable}
  constructors
›
lemma normal_rewr_nondet:
  "normal_rewr (NonD x y) =  NonD (normal_rewr x) (normal_rewr y)"
proof (induct x rule: normal_rewr.induct)
  case x: (1 x)
  then show ?case
  proof (induct y rule: normal_rewr.induct)
    case y: (1 y)
    then show ?case
      by (metis normal_rewr_step normalised.simps(6) normalised_normal_rewr step.simps(5))
  qed
qed
lemma normal_rewr_executable:
  "normal_rewr (Executable x y) = Executable (normal_rewr x) (normal_rewr y)"
proof (induct x rule: normal_rewr.induct)
  case x: (1 x)
  then show ?case
  proof (induct y rule: normal_rewr.induct)
    case y: (1 y)
    then show ?case
      by (metis normal_rewr_step normalised.simps(7) normalised_normal_rewr step.simps(6))
  qed
qed
lemma normal_rewr_repeatable:
  "normal_rewr (Repeatable x y) = Repeatable (normal_rewr x) (normal_rewr y)"
proof (induct x rule: normal_rewr.induct)
  case x: (1 x)
  then show ?case
  proof (induct y rule: normal_rewr.induct)
    case y: (1 y)
    then show ?case
      by (metis normal_rewr_step normalised.simps(8) normalised_normal_rewr step.simps(7))
  qed
qed

text‹Normalisation simplifies empty @{const Parallel} terms›
lemma normal_rewr_parallel_empty:
  "normal_rewr (Parallel []) = Empty"
  by (simp add: normal_rewr.simps)

text‹Every resource is equivalent to its normalisation›
lemma res_term_equiv_normal_rewr:
  "x ∼ normal_rewr x"
proof (induct x rule: normal_rewr.induct)
  case (1 x)
  then show ?case
  proof (cases "normalised x")
    case True
    then show ?thesis by (simp add: normal_rewr.simps)
  next
    case False
    then have "step x ∼ normal_rewr (step x)"
      using 1 by simp
    then have "x ∼ normal_rewr (step x)"
      using res_term_equiv.trans res_term_equiv_step by blast
    then show ?thesis
      by (simp add: normal_rewr.simps)
  qed
qed

text‹And, by transitivity, resource terms with equal normalisations are equivalent›
lemma normal_rewr_imp_equiv:
  "normal_rewr x = normal_rewr y ⟹ x ∼ y"
  using res_term_equiv_normal_rewr[of x] res_term_equiv_normal_rewr[of y, symmetric]
  by (metis res_term_equiv.trans)

text‹Resource normalisation commutes with the resource map›
lemma normal_rewr_map:
  "map_res_term f g (normal_rewr x) = normal_rewr (map_res_term f g x)"
proof (induct x rule: normal_rewr.induct)
  case (1 x)
  then show ?case
  proof (cases "normalised x")
    case True
    then show ?thesis
      by (simp add: normalised_map normal_rewr.simps)
  next
    case False
    have "map_res_term f g (normal_rewr x) = map_res_term f g (normal_rewr (step x))"
      using False by (simp add: normal_rewr.simps)
    also have "... = normal_rewr (map_res_term f g (step x))"
      using 1 False by simp
    also have "... = normal_rewr (step (map_res_term f g x))"
      using step_map[of f g x] by simp
    also have "... = normal_rewr (map_res_term f g x)"
      using False by (simp add: normalised_map normal_rewr.simps)
    finally show ?thesis .
  qed
qed

text‹Normalisation is contained in transitive closure of the rewriting›
lemma res_term_rewrite_tranclp_normal_rewr:
  "res_term_rewrite⇧+⇧+ x (normal_rewr x)"
proof (induct x rule: normal_rewr.induct)
  case (1 x)
  then show ?case
  proof (cases "normalised x")
    case True
    then show ?thesis
      by (simp add: tranclp.r_into_trancl)
  next
    case False
    then show ?thesis
      using 1 res_term_rewrite_contains_step tranclp_into_tranclp2 normal_rewr_step by metis
  qed
qed

subsection‹As Abstract Rewriting System›

text‹
  The normalisation procedure described above implements an abstract rewriting system.
  Their theory allows us to prove that equality of normal forms is the same as term equivalence by
  reasoning about how equivalent terms are joinable by the rewriting.
›

subsubsection‹Rewriting System Properties›

text‹
  In the ARS mechanisation normal forms are terminal elements of the rewriting relation, while in
  our case they are fixpoints.
  To interface with that property, we use the irreflexive graph of @{const step}.
›
definition step_irr :: "('a, 'b) res_term rel"
  where "step_irr = {(x,y). x ≠ y ∧ step x = y}"

lemma step_irr_inI:
  "x ≠ step x ⟹ (x, step x) ∈ step_irr"
  by (simp add: step_irr_def)

text‹Graph of @{const normal_rewr} is in the transitive-reflexive closure of irreflexive step›
lemma normal_rewr_in_step_rtrancl:
  "(x, normal_rewr x) ∈ step_irr⇧*"
proof (induct x rule: normal_rewr.induct)
  case (1 x)
  then show ?case
  proof (cases "normalised x")
    case True
    then show ?thesis by simp
  next
    case False
    moreover have "(x, step x) ∈ step_irr"
      using False normalised_is_step_id by (fastforce simp add: step_irr_def)
    ultimately show ?thesis
      by (metis 1 converse_rtrancl_into_rtrancl normal_rewr.elims)
  qed
qed

text‹Normal forms of irreflexive step are exactly the normalised terms›
lemma step_nf_is_normalised:
  "NF step_irr = {x. normalised x}"
proof safe
  fix x :: "('a, 'b) res_term"
  show "x ∈ NF step_irr ⟹ normalised x"
    by (metis NF_not_suc normal_rewr_in_step_rtrancl normal_rewr_normalised)
  show "normalised x ⟹ x ∈ NF step_irr"
    by (simp add: NF_I step_irr_def)
qed

text‹As such, every value of @{const normal_rewr} is a normal form of irreflexive step›
lemma normal_rewr_NF [simp]:
  "normal_rewr x ∈ NF step_irr"
  by (simp add: normal_rewr_normalised step_nf_is_normalised)

text‹Terms related by reflexive-transitive step are equivalent›
lemma step_rtrancl_equivalent:
  "(a,b) ∈ step_irr⇧* ⟹ a ∼ b"
proof (induct rule: rtrancl_induct)
  case base
  then show ?case by simp
next
  case (step y z)
  then show ?case
    by (metis (mono_tags, lifting) Product_Type.Collect_case_prodD fst_conv res_term_equiv.refl
        res_term_equiv.trans_both snd_conv res_term_equiv_step step_irr_def)
qed

text‹Irreflexive step is locally and strongly confluent because it's part of a function›
lemma step_irr_locally_confluent:
  "WCR step_irr"
  unfolding step_irr_def by standard fastforce

lemma step_irr_strongly_confluent:
  "strongly_confluent step_irr"
  unfolding step_irr_def by standard fastforce

text‹Therefore it is Church-Rosser and has unique normal forms›
lemma step_CR: "CR step_irr"
  using step_irr_strongly_confluent strong_confluence_imp_CR CR_imp_UNC CR_imp_UNF by blast
lemma step_UNC: "UNC step_irr"
  using step_CR CR_imp_UNC by blast
lemma step_UNF: "UNF step_irr"
  using step_CR CR_imp_UNF by blast

text‹Irreflexive step is strongly normalising because it decreases the well-founded rewriting bound›
lemma step_SN:
  "SN step_irr"
  unfolding SN_def
  using SN_onI
proof
  fix x :: "('a, 'b) res_term" and f
  show "⟦f 0 ∈ {x}; ∀i. (f i, f (Suc i)) ∈ step_irr⟧ ⟹ False"
    ― ‹Irreflexivity of step is essential here to get the needed contradiction›
    ― ‹Strong induction is needed because bound may decrease by more than 1›
  proof (induct "res_term_rewrite_bound x" arbitrary: f x rule: less_induct)
    case less
    then show ?case
      using less(1)[where x = "step x" and f = "λx. f (Suc x)"]
      by (metis (mono_tags, lifting) case_prodD mem_Collect_eq normalised_is_step_id
          res_term_rewrite_bound_step_decrease singleton_iff step_irr_def)
  qed
qed

text‹Normalisability relation of irreflexive step is exactly the graph of @{const normal_rewr}›
lemma step_normalizability_normal_rewr:
  "step_irr⇧! = {(x, y). y = normal_rewr x}"
proof safe
  fix a b :: "('a, 'b) res_term"
  assume "(a, b) ∈ step_irr⇧!"
  then show "b = normal_rewr a"
    by (meson UNF_onE UNIV_I normal_rewr_NF normal_rewr_in_step_rtrancl normalizability_I step_UNF)
next
  fix a :: "('a, 'b) res_term"
  show "(a, normal_rewr a) ∈ step_irr⇧!"
    using normal_rewr_NF normal_rewr_in_step_rtrancl by blast
qed

text‹The unique normal form, @{const the_NF} in the ARS language, is @{const normal_rewr}›
lemma step_irr_the_NF [simp]:
  "the_NF step_irr x = normal_rewr x"
  by (meson UNF_onE UNIV_I normal_rewr_NF normal_rewr_in_step_rtrancl normalizability_I
      step_CR step_SN step_UNF the_NF)

text‹Terms related by reflexive-transitive step have the same normal form›
lemma step_rtrancl_eq_normal:
  "(x,y) ∈ step_irr⇧* ⟹ normal_rewr x = normal_rewr y"
  by (metis normal_rewr_NF normal_rewr_in_step_rtrancl rtrancl_trans some_NF_UNF step_UNF)

subsubsection‹@{const NonD} Joinability›

text‹Two @{const NonD} terms are joinable if their corresponding children are joinable›

lemma step_rtrancl_nondL:
  "(x,u) ∈ step_irr⇧* ⟹ (NonD x y, NonD u y) ∈ step_irr⇧*"
proof (induct rule: rtrancl_induct)
  case base
  then show ?case by simp
next
  case (step y z)
  then show ?case
    by (fastforce intro: rtrancl_into_rtrancl simp add: step_irr_def)
qed

lemma step_rtrancl_nondR:
  "⟦(y,v) ∈ step_irr⇧*; normalised x⟧ ⟹ (NonD x y, NonD x v) ∈ step_irr⇧*"
proof (induct rule: rtrancl_induct)
  case base
  then show ?case by simp
next
  case (step y z)
  then show ?case
    by (fastforce intro: rtrancl_into_rtrancl simp add: step_irr_def)
qed

lemma step_rtrancl_nond:
  "⟦(x,u) ∈ step_irr⇧*; normalised u; (y,v) ∈ step_irr⇧*⟧ ⟹ (NonD x y, NonD u v) ∈ step_irr⇧*"
  using step_rtrancl_nondL step_rtrancl_nondR by (metis rtrancl_trans)

lemma step_join_apply_nondet:
  assumes "(x,u) ∈ step_irr⇧↓" and "(y,v) ∈ step_irr⇧↓" shows "(NonD x y, NonD u v) ∈ step_irr⇧↓"
proof (rule joinI)
  have "(NonD x y, NonD (normal_rewr x) y) ∈ step_irr⇧*"
    using step_rtrancl_nondL normal_rewr_in_step_rtrancl by metis
  also have "(NonD (normal_rewr x) y, NonD (normal_rewr x) (normal_rewr y)) ∈ step_irr⇧*"
    using step_rtrancl_nondR normal_rewr_in_step_rtrancl normal_rewr_normalised by metis
  finally show "(NonD x y, NonD (normal_rewr x) (normal_rewr y)) ∈ step_irr⇧*" .


  have "(NonD u v, NonD (normal_rewr u) v) ∈ step_irr⇧*"
    using step_rtrancl_nondL normal_rewr_in_step_rtrancl by metis
  also have "(NonD (normal_rewr u) v, NonD (normal_rewr u) (normal_rewr v)) ∈ step_irr⇧*"
    using step_rtrancl_nondR normal_rewr_in_step_rtrancl normal_rewr_normalised by metis
  also have
    "(NonD (normal_rewr u) (normal_rewr v), NonD (normal_rewr x) (normal_rewr y)) ∈ step_irr⇧*"
    using assms joinD step_rtrancl_eq_normal rtrancl.rtrancl_refl by metis
  finally show "(NonD u v, NonD (normal_rewr x) (normal_rewr y)) ∈ step_irr⇧*" .
qed

subsubsection‹@{const Executable} and @{const Repeatable} Joinability›

text‹
  Two (repeatably) executable resource terms are joinable if their corresponding children are
  joinable
›

lemma step_join_apply_executable:
  "⟦(x,u) ∈ step_irr⇧↓; (y,v) ∈ step_irr⇧↓⟧ ⟹ (Executable x y, Executable u v) ∈ step_irr⇧↓"
  using joinI[where c = "Executable (normal_rewr x) (normal_rewr y)"] normal_rewr_executable
  by (metis (mono_tags, lifting) joinD normal_rewr_in_step_rtrancl step_rtrancl_eq_normal)

lemma step_join_apply_repeatable:
  "⟦(x,u) ∈ step_irr⇧↓; (y,v) ∈ step_irr⇧↓⟧ ⟹ (Repeatable x y, Repeatable u v) ∈ step_irr⇧↓"
  using joinI[where c = "Repeatable (normal_rewr x) (normal_rewr y)"] normal_rewr_repeatable
  by (metis (mono_tags, lifting) joinD normal_rewr_in_step_rtrancl step_rtrancl_eq_normal)

subsubsection‹@{const Parallel} Joinability›

text‹From two lists of joinable terms we can obtain a list of common destination terms›
lemma list_all2_join:
  assumes "list_all2 (λx y. (x, y) ∈ R⇧↓) xs ys"
  obtains cs
    where "list_all2 (λx c. (x, c) ∈ R⇧*) xs cs"
      and "list_all2 (λy c. (y, c) ∈ R⇧*) ys cs"
  using assms by (induct rule: list_all2_induct ; blast)

text‹
  Every parallel resource term with at least two elements is related to a parallel resource term
  with the contents normalised
›
lemma step_rtrancl_map_normal:
  "(Parallel xs, Parallel (map normal_rewr xs)) ∈ step_irr⇧*"
proof (induct "sum_list (map res_term_rewrite_bound xs)" arbitrary: xs rule: less_induct)
  case less
  then show ?case
  proof (cases "list_all normalised xs")
    case True
    then show ?thesis
      by (metis Ball_set map_idI normalised_normal_rewr rtrancl.rtrancl_refl)
  next
    case False
    then have unnorm: "¬ normalised (Parallel xs)"
      by simp

    have step: "step (Parallel xs) = Parallel (map step xs)"
      using False by (simp add: not_list_all)
    moreover have "Parallel xs ≠ Parallel (map step xs)"
      using unnorm by (metis calculation normalised_is_step_id)
    ultimately have "(Parallel xs, Parallel (map step xs)) ∈ step_irr"
      using step_irr_inI by metis
    moreover have "(Parallel (map step xs), Parallel (map normal_rewr (map step xs))) ∈ step_irr⇧*"
      using less[of "map step xs"] False step unnorm
      by (smt (verit, ccfv_threshold) ab_semigroup_add_class.add_ac(1)
          add_mono_thms_linordered_field(3) dual_order.refl length_map not_less_eq plus_1_eq_Suc
          res_term_rewrite_bound.simps(5) res_term_rewrite_bound_step_decrease)
    moreover have "map normal_rewr (map step xs) = map normal_rewr xs"
      by (simp ; safe ; rule normal_rewr_step[symmetric])
    ultimately show ?thesis
      by (metis (no_types, lifting) converse_rtrancl_into_rtrancl)
  qed
qed

text‹Two lists of joinable terms have the same normal forms›
lemma list_all2_join_normal_eq:
  "list_all2 (λu v. (u, v) ∈ step_irr⇧↓) xs ys ⟹ map normal_rewr xs = map normal_rewr ys"
proof (induct rule: list_all2_induct)
  case Nil
  then show ?case by simp
next
  case (Cons x xs y ys)
  then show ?case by simp (metis (no_types, lifting) joinD step_rtrancl_eq_normal)
qed

text‹Parallel resource terms whose contents are joinable are themselves joinable›
lemma step_join_apply_parallel:
  assumes "list_all2 (λu v. (u,v) ∈ step_irr⇧↓) xs ys"
  shows "(Parallel xs, Parallel ys) ∈ step_irr⇧↓"
  by (metis assms joinI list_all2_join_normal_eq step_rtrancl_map_normal)

text‹Removing all @{const Empty} terms absorbs the removal of one›
lemma remove_all_empty_subsumes_remove_one:
  "remove_all_empty (remove_one_empty xs) = 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 ; fastforce)
qed

text‹For any list with an @{const Empty} term, removing one strictly decreases their count›
lemma remove_one_empty_count_if_decrease:
  "list_ex is_Empty xs ⟹ count_if is_Empty (remove_one_empty xs) < count_if is_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 all @{const Empty} terms from children of a @{const Parallel} term, that are already all
  normalised and none of which are nested @{const Parallel} terms, is related by transitive and
  reflexive closure of irreflexive step.
›
lemma step_rtrancl_remove_all_empty:
  assumes "⋀x. x ∈ set xs ⟹ normalised x"
      and "¬ list_ex is_Parallel xs"
    shows "(Parallel xs, Parallel (remove_all_empty xs)) ∈ step_irr⇧*"
  using assms
proof (induct "count_if is_Empty xs" arbitrary: xs rule: less_induct)
  case less
  then show ?case
  proof (cases "list_ex is_Empty xs")
    case True
    then have a: "step (Parallel xs) = Parallel (remove_one_empty xs)"
      using less by (metis Bex_set step.simps(8))
    moreover have b: "count_if is_Empty (remove_one_empty xs) < count_if is_Empty xs"
      using True by (rule remove_one_empty_count_if_decrease)
    moreover have c: "⋀x. x ∈ set (remove_one_empty xs) ⟹ normalised x"
      using remove_one_empty_subset less(2) by fast
    moreover have "¬ list_ex is_Parallel (remove_one_empty xs)"
      using remove_one_empty_subset less(3) not_list_ex
      by (metis (mono_tags, lifting) Ball_set)
    ultimately show ?thesis
      using less remove_all_empty_subsumes_remove_one
      by (metis converse_rtrancl_into_rtrancl step_irr_inI)
  next
    case False
    then show ?thesis
      by (simp add: joinI_right remove_all_empty_none)
  qed
qed

text‹
  After merging all @{const Parallel} elements of a list of normalised terms, there remain no more
  @{const Parallel} terms in it
›
lemma merge_all_parallel_map_normal_result:
  assumes "⋀x. x ∈ set xs ⟹ normalised x"
    shows "¬ list_ex is_Parallel (merge_all_parallel xs)"
  using assms merge_all_parallel_result normalised.simps(5) not_list_ex by blast

text‹
  For any list with a @{const Parallel} term, removing one strictly decreases their count if no
  element contains further nested @{const Parallel} terms within it
›
lemma merge_one_parallel_count_if_decrease:
  assumes "list_ex is_Parallel xs"
      and "⋀y ys. ⟦y ∈ set xs; y = Parallel ys⟧ ⟹ ¬ list_ex is_Parallel ys"
    shows "count_if is_Parallel (merge_one_parallel xs) < count_if is_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) (simp_all add: count_if_0_conv)
qed

text‹
  Merging all @{const Parallel} terms absorbs the merging of one if no element contains further
  nested @{const Parallel} terms within it
›
lemma merge_all_parallel_subsumes_merge_one:
  assumes "⋀y ys. ⟦y ∈ set xs; y = Parallel ys⟧ ⟹ ¬ list_ex is_Parallel ys"
    shows "merge_all_parallel (merge_one_parallel xs) = merge_all_parallel xs"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
  proof (cases a)
       case Empty then show ?thesis using Cons by simp
  next case Anything then show ?thesis using Cons by simp
  next case (Res x3) then show ?thesis using Cons by simp
  next case (Copyable x4) then show ?thesis using Cons by simp
  next
    case (Parallel x5)
    then show ?thesis
      using Cons by (simp add: merge_all_parallel_append merge_all_parallel_none)
  next case (NonD x61 x62) then show ?thesis using Cons by simp
  next case (Executable x71 x72) then show ?thesis using Cons by simp
  next case (Repeatable x81 x82) then show ?thesis using Cons by simp
  qed
qed

text‹Merging one @{const Parallel} term in a list of normalised terms keeps them normalised›
lemma merge_one_parallel_preserve_normalised:
  "⟦⋀x. x ∈ set xs ⟹ normalised x; a ∈ set (merge_one_parallel xs)⟧ ⟹ normalised a"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp ; (presburger | metis normalised_parallel_children))
qed

text‹Merging all @{const Parallel} terms in a list of normalised terms keeps them normalised›
lemma merge_all_parallel_preserve_normalised:
  "⟦⋀x. x ∈ set xs ⟹ normalised x; a ∈ set (merge_all_parallel xs)⟧ ⟹ normalised a"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases a ; simp ; (presburger | metis normalised_parallel_children))
qed

text‹
  Merging all @{const Parallel} terms from children of a @{const Parallel} term, that are already
  all normalised, is related by transitive and reflexive closure of irreflexive step.
›
lemma step_rtrancl_merge_all_parallel:
  assumes "⋀x. x ∈ set xs ⟹ normalised x"
  shows "(Parallel xs, Parallel (merge_all_parallel xs)) ∈ step_irr⇧*"
  using assms
proof (induct "count_if is_Parallel xs" arbitrary: xs rule: less_induct)
  case less
  then show ?case
  proof (cases "list_ex is_Parallel xs")
    case False
    then show ?thesis
      using merge_all_parallel_none by (metis rtrancl.rtrancl_refl)
  next
    case True
    then have "step (Parallel xs) = Parallel (merge_one_parallel xs)"
      using less by (metis Bex_set step.simps(8))
    moreover have "⋀x. x ∈ set (merge_one_parallel xs) ⟹ normalised x"
      using merge_one_parallel_preserve_normalised less(2) by blast
    moreover have "count_if is_Parallel (merge_one_parallel xs) < count_if is_Parallel xs"
      using less(2) True merge_one_parallel_count_if_decrease normalised.simps(5) not_list_ex
      by blast
    ultimately show ?thesis
      using less merge_all_parallel_subsumes_merge_one
      by (metis converse_rtrancl_into_rtrancl normalised.simps(5) not_list_ex step_irr_inI)
  qed
qed

text‹Thus, there is a general rewriting path that @{const Parallel} terms take›
lemma step_rtrancl_parallel:
  "(Parallel xs, Parallel (remove_all_empty (merge_all_parallel (map normal_rewr xs)))) ∈ step_irr⇧*"
proof -
  have "(Parallel xs, Parallel (map normal_rewr xs)) ∈ step_irr⇧*"
    by (rule step_rtrancl_map_normal)
  also have
    " (Parallel (map normal_rewr xs), Parallel (merge_all_parallel (map normal_rewr xs)))
    ∈ step_irr⇧*"
    by (metis ex_map_conv normal_rewr_normalised step_rtrancl_merge_all_parallel)
  also have "(Parallel (merge_all_parallel (map normal_rewr xs)),
              Parallel (remove_all_empty (merge_all_parallel (map normal_rewr xs)))) ∈ step_irr⇧*"
    using merge_all_parallel_map_normal_result merge_all_parallel_preserve_normalised
          normal_rewr_normalised step_rtrancl_remove_all_empty
    by (metis (mono_tags, lifting) imageE list.set_map)
  finally show ?thesis .
qed

subsubsection‹Other Helpful Lemmas›

text‹For Church-Rosser strongly normalising rewriting systems, joinability is transitive›
lemma CR_SN_join_trans:
  assumes "CR R"
      and "SN R"
      and "(x, y) ∈ R⇧↓"
      and "(y, z) ∈ R⇧↓"
    shows "(x, z) ∈ R⇧↓"
proof -
  obtain a where a: "(x, a) ∈ R⇧*" "(y, a) ∈ R⇧*"
    using assms(3) joinE by metis
  then have "the_NF R y = the_NF R a"
    using assms(1,2) the_NF_steps by metis
  moreover obtain b where b: "(y, b) ∈ R⇧*" "(z, b) ∈ R⇧*"
    using assms(4) joinE by metis
  then have "the_NF R y = the_NF R b"
    using assms(1,2) the_NF_steps by metis
  ultimately show ?thesis
    using assms(1,2) a b by (meson CR_join_right_I joinI join_rtrancl_join)
qed

text‹More generally, for such systems, two joinable pairs can be bridged by a third›
lemma CR_SN_join_both:
  "⟦CR R; SN R; (a, b) ∈ R⇧↓; (x, y) ∈ R⇧↓; (b, y) ∈ R⇧↓⟧ ⟹ (a, x) ∈ R⇧↓"
  by (meson CR_SN_join_trans join_sym)

text‹With irreflexive step being one such rewriting system›
lemmas step_irr_join_trans = CR_SN_join_trans[OF step_CR step_SN]
lemmas step_irr_join_both = CR_SN_join_both[OF step_CR step_SN]

text‹@{const Parallel} term with no work left in children normalises in three possible ways›
lemma normal_rewr_parallel_cases:
  assumes "∀x. x ∈ set xs ⟶ normalised x"
      and "¬ list_ex is_Empty xs"
      and "¬ list_ex is_Parallel xs"
    obtains
      (Parallel) "normalised (Parallel xs)" and "normal_rewr (Parallel xs) = Parallel xs"
    | (Empty) "xs = []" and "normal_rewr (Parallel xs) = Empty"
    | (Single) a where "xs = [a]" and "normal_rewr (Parallel xs) = a"
proof (cases xs rule: remdups_adj.cases)
  case 1
  then show ?thesis using that normal_rewr_parallel_empty by fastforce
next
  case (2 x)
  then have "normal_rewr (Parallel [x]) = step (Parallel [x])"
    using assms by (subst normal_rewr.simps) simp
  then show ?thesis
    using that assms 2 by simp
next
  case (3 x y xs)
  then show ?thesis
    using assms that
    by (metis normal_rewr.simps normalised_parallelise parallelise.simps(3))
qed

text‹
  For a list of already normalised terms with no @{const Empty} or @{const Parallel} terms, the
  normalisation procedure acts like @{const parallel_parts} followed by @{const parallelise}.
  It only does simplifications related to the number of elements.
›
lemma normal_rewr_parallelise:
  assumes "∀x. x ∈ set xs ⟶ normalised x"
      and "¬ list_ex is_Empty xs"
      and "¬ list_ex is_Parallel xs"
    shows "normal_rewr (Parallel xs) = parallelise (parallel_parts (Parallel xs))"
proof -
  show ?thesis
    using assms
  proof (cases rule: normal_rewr_parallel_cases)
    case Parallel
    then show ?thesis
      using parallel_parts_no_empty_parallel assms
      by (metis list_obtain_2 normalised.simps(5) parallelise.simps(3))
  next case Empty then show ?thesis by simp
  next case (Single a) then show ?thesis using assms by (cases a ; simp)
  qed
qed

text‹Removing all @{const Empty} terms has no effect on number of @{const Parallel} terms›
lemma parallel_remove_all_empty:
  "list_ex is_Parallel (remove_all_empty xs) = list_ex is_Parallel 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

text‹
  Removing all @{const Empty} terms is idempotent because there are no @{const Empty} terms to
  remove on the second pass
›
lemma remove_all_empty_idempotent:
  shows "remove_all_empty (remove_all_empty xs) = remove_all_empty xs"
  by (induct xs) simp_all

text‹
  Every @{const Parallel} term rewrites to the parallelisation of normalised children with all
  @{const Empty} terms removed and all @{const Parallel} terms merged
›
lemma normal_rewr_to_parallelise:
  " normal_rewr (Parallel xs)
  = parallelise (remove_all_empty (merge_all_parallel (map normal_rewr xs)))"
proof -
  have
    " normal_rewr (Parallel xs)
    = normal_rewr (Parallel (remove_all_empty (merge_all_parallel (map normal_rewr xs))))"
    using step_rtrancl_parallel step_rtrancl_eq_normal by metis
  also have " ...
    = parallelise (parallel_parts (Parallel
        (remove_all_empty (merge_all_parallel (map normal_rewr xs)))))"
    using merge_all_parallel_preserve_normalised normal_rewr_parallelise parallel_remove_all_empty
    using merge_all_parallel_map_normal_result remove_all_empty_result normal_rewr_normalised
    by (smt (verit, ccfv_threshold) imageE list.set_map remove_all_empty_subset)
  also have "... = parallelise (remove_all_empty (merge_all_parallel (map normal_rewr xs)))"
    using parallel_parts_no_empty_parallel parallel_remove_all_empty
    using merge_all_parallel_map_normal_result remove_all_empty_result normal_rewr_normalised
    by (metis (mono_tags, lifting) imageE list.set_map)
  finally show ?thesis .
qed

text‹
  @{const Parallel} term that normalises to @{const Empty} must have had no children left after
  normalising them, merging @{const Parallel} terms and removing @{const Empty} terms
›
lemma normal_rewr_to_empty:
  assumes "normal_rewr (Parallel xs) = Empty"
    shows "remove_all_empty (merge_all_parallel (map normal_rewr xs)) = []"
  using assms normal_rewr_to_parallelise parallelise_to_empty_eq remove_all_empty_result
  by (metis list_ex_simps(1) res_term.disc(19))

text‹
  @{const Parallel} term that normalises to another @{const Parallel} must have had those children
  left after normalising its own, merging @{const Parallel} terms and removing @{const Empty} terms
›
lemma normal_rewr_to_parallel:
  assumes "normal_rewr (Parallel xs) = Parallel ys"
    shows "remove_all_empty (merge_all_parallel (map normal_rewr xs)) = remove_all_empty ys"
proof -
  have "¬ list_ex is_Parallel (remove_all_empty (merge_all_parallel (map normal_rewr xs)))"
    using merge_all_parallel_map_normal_result normal_rewr_normalised parallel_remove_all_empty
    by (metis (mono_tags, lifting) imageE list.set_map)
  then have "remove_all_empty (merge_all_parallel (map normal_rewr xs)) = ys"
    by (metis assms normal_rewr_to_parallelise normal_rewr_normalised normalised_parallel_parts_eq
        parallel_parts_no_empty_parallel parallel_parts_parallelise_eq remove_all_empty_result)
  then show ?thesis
    using assms remove_all_empty_idempotent by metis
qed

text‹
  @{const Parallel} that normalises to anything else must have had that as the only term left after
  normalising its own, merging @{const Parallel} terms and removing @{const Empty} terms
›
lemma normal_rewr_to_other:
  assumes "normal_rewr (Parallel xs) = a"
      and "¬ is_Empty a"
      and "¬ is_Parallel a"
    shows "remove_all_empty (merge_all_parallel (map normal_rewr xs)) = [a]"
  using assms by (simp add: normal_rewr_to_parallelise parallelise_to_single_eq)

subsubsection‹Equivalent Term Joinability›

text‹Equivalent resource terms are joinable by irreflexive step›
lemma res_term_equiv_joinable:
  "x ∼ y ⟹ (x, y) ∈ step_irr⇧↓"
proof (induct rule: res_term_equiv.induct)
     case empty then show ?case by blast
next case anything then show ?case by blast
next case (res x) then show ?case by blast
next case (copyable x) then show ?case by blast
next
  case nil
  then show ?case
    by (metis joinI_left normal_rewr_in_step_rtrancl normal_rewr_parallel_empty)
next
  case (singleton a)
  then show ?case
  proof (induct "res_term_rewrite_bound a" arbitrary: a rule: less_induct)
    case less
      then show ?case
    proof (cases "normalised a")
      case True
      then show ?thesis
      proof (cases a)
        case Empty
        moreover have "(Parallel [Empty], Empty) ∈ step_irr⇧*"
        proof -
          have "step (Parallel [Empty]) = Parallel []"
            by simp
          then show ?thesis
            using normal_rewr_in_step_rtrancl normal_rewr_parallel_empty
            by (metis converse_rtrancl_into_rtrancl step_irr_inI)
        qed
        ultimately show ?thesis
          using joinI_left by simp
      next
        case Anything
        then have "step (Parallel [a]) = a"
          by simp
        then show ?thesis
          using step_irr_inI parallel_neq_single r_into_rtrancl joinI_left by metis
      next
        case (Res x3)
        then have "step (Parallel [a]) = a"
          by simp
        then show ?thesis
          using step_irr_inI parallel_neq_single r_into_rtrancl joinI_left by metis
      next
        case (Copyable x4)
        then have "step (Parallel [a]) = a"
          using True by simp
        then show ?thesis
          using step_irr_inI parallel_neq_single r_into_rtrancl joinI_left by metis
      next
        case (Parallel x5)
        then have "step (Parallel [Parallel x5]) = Parallel x5"
          using True by simp
        then show ?thesis
          using step_irr_inI parallel_neq_single r_into_rtrancl joinI_left Parallel by metis
      next
        case (NonD x61 x62)
        then have "step (Parallel [a]) = a"
          using True by simp
        then show ?thesis
          using step_irr_inI parallel_neq_single r_into_rtrancl joinI_left by metis
      next
        case (Executable x71 x72)
        then have "step (Parallel [a]) = a"
          using True by simp
        then show ?thesis
          using step_irr_inI parallel_neq_single r_into_rtrancl joinI_left by metis
      next
        case (Repeatable x71 x72)
        then have "step (Parallel [a]) = a"
          using True by simp
        then show ?thesis
          using step_irr_inI parallel_neq_single r_into_rtrancl joinI_left by metis
      qed
    next
      case False
      then have "step (Parallel [a]) = Parallel [step a]"
        by simp
      moreover have "res_term_rewrite_bound (step a) < res_term_rewrite_bound a"
        using res_term_rewrite_bound_step_decrease False by blast
      ultimately show ?thesis
        using less normal_rewr_in_step_rtrancl step_irr_join_trans step_normalised
        by (metis joinI normal_rewr.elims)
    qed
  qed
next
  case (merge x y z)
  have
    "( Parallel (x @ y @ z)
     ,  Parallel (remove_all_empty (merge_all_parallel (map normal_rewr (x @ y @ z))))
     ) ∈ step_irr⇧*"
    using step_rtrancl_parallel .
  also have
    "( Parallel (remove_all_empty (merge_all_parallel (map normal_rewr (x @ y @ z))))
      , Parallel (remove_all_empty (merge_all_parallel (map normal_rewr (x @ [Parallel y] @ z))))
     ) ∈ step_irr⇧*"
  proof (cases "normal_rewr (Parallel y)")
    case Empty
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_empty)
  next
    case Anything
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_other)
  next
    case (Res x3)
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_other)
  next
    case (Copyable x4)
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_other)
  next
    case (Parallel x5)
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_parallel)
  next
    case (NonD x61 x62)
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_other)
  next
    case (Executable x71 x72)
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_other)
  next
    case (Repeatable x81 x82)
    then show ?thesis
      by (simp add: merge_all_parallel_append remove_all_empty_append normal_rewr_to_other)
  qed
  finally show ?case
    using step_rtrancl_parallel by blast
next
  case (parallel xs ys)
  then show ?case
    by (simp add: list_all2_mono step_join_apply_parallel)
next
  case (nondet x y u v)
  then show ?case using step_join_apply_nondet by blast
next
  case (executable x y u v)
  then show ?case using step_join_apply_executable by blast
next
  case (repeatable x y u v)
  then show ?case using step_join_apply_repeatable by blast
next
  case (sym x y)
  then show ?case by (simp add: join_sym)
next
  case (trans x y z)
  then show ?case by (meson joinE CR_join_right_I joinI join_rtrancl_join step_CR)
qed

text‹Therefore this rewriting-based normalisation brings equivalent terms to the same normal form›
lemma res_term_equiv_imp_normal_rewr:
  assumes "x ∼ y" shows "normal_rewr x = normal_rewr y"
proof (rule join_NF_imp_eq)
  have "normal_rewr x ∼ x"
    using res_term_equiv_normal_rewr res_term_equiv.sym by blast
  moreover have "y ∼ normal_rewr y"
    by (rule res_term_equiv_normal_rewr)
  ultimately have "normal_rewr x ∼ normal_rewr y"
    using assms by (rule res_term_equiv.trans_both)
  then show "(normal_rewr x, normal_rewr y) ∈ step_irr⇧↓"
    by (rule res_term_equiv_joinable)

  show "normal_rewr x ∈ NF step_irr"
   and "normal_rewr y ∈ NF step_irr"
    by (rule normal_rewr_NF)+
qed

text‹And resource term equivalence is equal to having equal normal forms›
theorem res_term_equiv_is_normal_rewr:
  "x ∼ y = (normal_rewr x = normal_rewr y)"
  using res_term_equiv_imp_normal_rewr normal_rewr_imp_equiv by standard

subsection‹Term Equivalence as Rewriting Closure›

text‹
  We can now show that @{const res_term_equiv} is the equivalence closure of
  @{const res_term_rewrite}.

  An equivalence closure is a reflexive, transitive and symmetric closure.
  In our case, the rewriting is already reflexive, so we only need to verify the symmetric and
  transitive closure.

  As such, the core difficulty in this section is to prove the following equality:
  @{term "x ∼ y = (symclp res_term_rewrite)⇧+⇧+ x y"}
›

text‹One direction is simpler, because rewriting implies equivalence›
lemma res_term_rewrite_equivclp_imp_equiv:
  "(symclp res_term_rewrite)⇧+⇧+ x y ⟹ x ∼ y"
proof (induct rule: tranclp.induct)
  case (r_into_trancl a b)
  then show ?case
    by (metis symclp_def res_term_rewrite_imp_equiv res_term_equiv.sym)
next
  case (trancl_into_trancl a b c)
  then have "b ∼ c"
    by (metis symclp_def res_term_rewrite_imp_equiv res_term_equiv.sym)
  then show ?case
    by (metis trancl_into_trancl(2) res_term_equiv.trans)
qed

text‹Trying to prove the other direction purely through facts about the rewriting itself fails›
lemma
  "x ∼ y ⟹ (symclp res_term_rewrite)⇧+⇧+ x y"
proof (induct x y rule: res_term_equiv.induct)
     case empty then show ?case by (simp add: tranclp.r_into_trancl)
next case anything then show ?case by (simp add: tranclp.r_into_trancl)
next case (res x) then show ?case by (simp add: tranclp.r_into_trancl)
next case (copyable x) then show ?case by (simp add: tranclp.r_into_trancl)
next
  case nil
  then show ?case
    by (simp add: res_term_rewrite.nil tranclp.r_into_trancl)
next
  case (singleton a)
  then show ?case
    by (simp add: res_term_rewrite.singleton tranclp.r_into_trancl)
next
  case (merge x y z)
  then show ?case
    by (meson res_term_rewrite.merge symclp_def tranclp.r_into_trancl)
next
  case (sym x y)
  then show ?case
    by (metis rtranclpD rtranclp_symclp_sym tranclp_into_rtranclp)
next case (trans x y z) then show ?case by simp
next
  case (parallel xs ys)
  then show ?case
    ― ‹While we do know that corresponding parallel terms are related, the rewrite rule
        @{thm res_term_rewrite.parallel} needs all rewrites to be in a uniform direction.
        Such an issue arises with all remaining cases.›
oops

text‹But, we can take advantage of the normalisation procedure to prove it›
lemma res_term_rewrite_equiv_imp_equivclp:
  assumes "x ∼ y"
  shows "(symclp res_term_rewrite)⇧+⇧+ x y"
proof -
  have "normal_rewr x = normal_rewr y"
    using assms res_term_equiv_is_normal_rewr by metis
  then have "(symclp res_term_rewrite)⇧+⇧+ (normal_rewr x) (normal_rewr y)"
    by (simp add: tranclp.r_into_trancl)
  moreover have "(symclp res_term_rewrite)⇧+⇧+ x (normal_rewr x)"
    using res_term_rewrite_tranclp_normal_rewr symclp_def res_term_rewrite.refl
    by (metis equivclp_def rev_predicate2D rtranclp_into_tranclp2 rtranlcp_le_equivclp
        tranclp_into_rtranclp)
  moreover have "(symclp res_term_rewrite)⇧+⇧+ (normal_rewr y) y"
    using res_term_rewrite_tranclp_normal_rewr symclp_def res_term_rewrite.refl
    by (metis conversepD equivclp_def rev_predicate2D rtranclpD rtranlcp_le_equivclp
        symp_conv_conversep_eq symp_rtranclp_symclp tranclp.r_into_trancl tranclp_into_rtranclp)
  ultimately show ?thesis
    by simp
qed

text‹Thus, we prove that resource term equivalence is the equivalence closure of the rewriting›
lemma res_term_equiv_is_rewrite_closure:
  "(∼) = equivclp res_term_rewrite"
proof -
  have "equivclp res_term_rewrite x y = (symclp res_term_rewrite)⇧+⇧+ x y"
    for x y :: "('a, 'b) res_term"
    by (metis equivclp_def res_term_equiv.refl res_term_rewrite_equiv_imp_equivclp rtranclpD
        tranclp_into_rtranclp)
  then have "x ∼ y = equivclp res_term_rewrite x y"
    for x y :: "('a, 'b) res_term"
    using res_term_rewrite_equivclp_imp_equiv res_term_rewrite_equiv_imp_equivclp by metis
  then show ?thesis
    by blast
qed


end