Theory Rewriting_Pterm_Elim

section ‹Higher-order term rewriting with explicit pattern matching›

theory Rewriting_Pterm_Elim
imports
  Rewriting_Nterm
  "../Terms/Pterm"
begin

subsection ‹Intermediate rule sets›

type_synonym irules = "(term list × pterm) fset"
type_synonym irule_set = "(name × irules) fset"

locale pre_irules = constants C_info "fst |`| rs" for C_info and rs :: "irule_set"

locale irules = pre_irules +
  assumes fmap: "is_fmap rs"
  assumes nonempty: "rs ≠ {||}"
  assumes inner:
    "fBall rs (λ(_, irs).
      arity_compatibles irs ∧
      is_fmap irs ∧
      patterns_compatibles irs ∧
      irs ≠ {||} ∧
      fBall irs (λ(pats, rhs).
        linears pats ∧
        abs_ish pats rhs ∧
        closed_except rhs (freess pats) ∧
        fdisjnt (freess pats) all_consts ∧
        wellformed rhs ∧
        ¬ shadows_consts rhs ∧
        welldefined rhs))"

lemma (in pre_irules) irulesI:
  assumes "⋀name irs. (name, irs) |∈| rs ⟹ arity_compatibles irs"
  assumes "⋀name irs. (name, irs) |∈| rs ⟹ is_fmap irs"
  assumes "⋀name irs. (name, irs) |∈| rs ⟹ patterns_compatibles irs"
  assumes "⋀name irs. (name, irs) |∈| rs ⟹ irs ≠ {||}"
  assumes "⋀name irs pats rhs. (name, irs) |∈| rs ⟹ (pats, rhs) |∈| irs ⟹ linears pats"
  assumes "⋀name irs pats rhs. (name, irs) |∈| rs ⟹ (pats, rhs) |∈| irs ⟹ abs_ish pats rhs"
  assumes "⋀name irs pats rhs. (name, irs) |∈| rs ⟹ (pats, rhs) |∈| irs ⟹ fdisjnt (freess pats) all_consts"
  assumes "⋀name irs pats rhs. (name, irs) |∈| rs ⟹ (pats, rhs) |∈| irs ⟹ closed_except rhs (freess pats)"
  assumes "⋀name irs pats rhs. (name, irs) |∈| rs ⟹ (pats, rhs) |∈| irs ⟹ wellformed rhs"
  assumes "⋀name irs pats rhs. (name, irs) |∈| rs ⟹ (pats, rhs) |∈| irs ⟹ ¬ shadows_consts rhs"
  assumes "⋀name irs pats rhs. (name, irs) |∈| rs ⟹ (pats, rhs) |∈| irs ⟹ welldefined rhs"
  assumes "is_fmap rs" "rs ≠ {||}"
  shows "irules C_info rs"
proof unfold_locales
  show "is_fmap rs"
    using assms(12) .
next
  show "rs ≠ {||}"
    using assms(13) .
next
  show "fBall rs (λ(_, irs). Rewriting_Nterm.arity_compatibles irs ∧ is_fmap irs ∧
    patterns_compatibles irs ∧ irs ≠ {||} ∧
    fBall irs (λ(pats, rhs). linears pats ∧ abs_ish pats rhs ∧ closed_except rhs (freess pats) ∧
      fdisjnt (freess pats) all_consts ∧ pre_strong_term_class.wellformed rhs ∧
      ¬ shadows_consts rhs ∧ consts rhs |⊆| all_consts))"
    using assms(1-11)
    by (intro prod_BallI conjI) metis+
qed

lemmas irulesI[intro!] = pre_irules.irulesI[unfolded pre_irules_def]

subsubsection ‹Translation from @{typ nterm} to @{typ pterm}›

fun nterm_to_pterm :: "nterm ⇒ pterm" where
"nterm_to_pterm (Nvar s) = Pvar s" |
"nterm_to_pterm (Nconst s) = Pconst s" |
"nterm_to_pterm (t⇩1 $⇩n t⇩2) = nterm_to_pterm t⇩1 $⇩p nterm_to_pterm t⇩2" |
"nterm_to_pterm (Λ⇩n x. t) = (Λ⇩p x. nterm_to_pterm t)"

lemma nterm_to_pterm_inj: "nterm_to_pterm x = nterm_to_pterm y ⟹ x = y"
by (induction y arbitrary: x) (auto elim: nterm_to_pterm.elims)

lemma nterm_to_pterm:
  assumes "no_abs t"
  shows "nterm_to_pterm t = convert_term t"
using assms
apply induction
apply auto
by (auto simp: free_nterm_def free_pterm_def const_nterm_def const_pterm_def app_nterm_def app_pterm_def)

lemma nterm_to_pterm_frees[simp]: "frees (nterm_to_pterm t) = frees t"
by (induct t) auto

lemma closed_nterm_to_pterm[intro]: "closed_except (nterm_to_pterm t) (frees t)"
unfolding closed_except_def by simp

lemma (in constants) shadows_nterm_to_pterm[simp]: "shadows_consts (nterm_to_pterm t) = shadows_consts t"
by (induct t) (auto simp: shadows_consts_def fdisjnt_alt_def)

lemma wellformed_nterm_to_pterm[intro]: "wellformed (nterm_to_pterm t)"
by (induct t) auto

lemma consts_nterm_to_pterm[simp]: "consts (nterm_to_pterm t) = consts t"
by (induct t) auto

subsubsection ‹Translation from @{typ crule_set} to @{typ irule_set}›

definition translate_crules :: "crules ⇒ irules" where
"translate_crules = fimage (map_prod id nterm_to_pterm)"

definition compile :: "crule_set ⇒ irule_set" where
"compile = fimage (map_prod id translate_crules)"

lemma compile_heads: "fst |`| compile rs = fst |`| rs"
unfolding compile_def by simp

lemma (in crules) compile_rules: "irules C_info (compile rs)"
proof
  have "is_fmap rs"
    using fmap by simp
  thus "is_fmap (compile rs)"
    unfolding compile_def map_prod_def id_apply by (rule is_fmap_image)

  show "compile rs ≠ {||}"
    using nonempty unfolding compile_def by auto

  show "constants C_info (fst |`| compile rs)"
    proof
      show "fdisjnt (fst |`| compile rs) C"
        using disjnt unfolding compile_def
        by force
    next
      show "distinct all_constructors"
        by (fact distinct_ctr)
    qed

  fix name irs
  assume irs: "(name, irs) |∈| compile rs"
  then obtain irs' where "(name, irs') |∈| rs" "irs = translate_crules irs'"
    unfolding compile_def by force
  hence "arity_compatibles irs'"
    using inner
    by (metis (no_types, lifting) case_prodD)
  thus "arity_compatibles irs"
    unfolding ‹irs = translate_crules irs'› translate_crules_def
    by (force dest: fpairwiseD)

  have "patterns_compatibles irs'"
    using ‹(name, irs') |∈| rs› inner
    by (blast dest: fpairwiseD)
  thus "patterns_compatibles irs"
    unfolding ‹irs = _› translate_crules_def
    by (auto dest: fpairwiseD)

  have "is_fmap irs'"
    using ‹(name, irs') |∈| rs› inner by auto
  thus "is_fmap irs"
    unfolding ‹irs = translate_crules irs'› translate_crules_def map_prod_def id_apply
    by (rule is_fmap_image)

  have "irs' ≠ {||}"
    using ‹(name, irs') |∈| rs› inner by auto
  thus "irs ≠ {||}"
    unfolding ‹irs = translate_crules irs'› translate_crules_def by simp

  fix pats rhs
  assume "(pats, rhs) |∈| irs"
  then obtain rhs' where "(pats, rhs') |∈| irs'" "rhs = nterm_to_pterm rhs'"
    unfolding ‹irs = translate_crules irs'› translate_crules_def by force
  hence "linears pats" "pats ≠ []" "frees rhs' |⊆| freess pats" "¬ shadows_consts rhs'"
    using fbspec[OF inner ‹(name, irs') |∈| rs›]
    by blast+

  show "linears pats" by fact
  show "closed_except rhs (freess pats)"
    unfolding ‹rhs = nterm_to_pterm rhs'›
    using ‹frees rhs' |⊆| freess pats›
    by (metis dual_order.trans closed_nterm_to_pterm closed_except_def)

  show "wellformed rhs"
    unfolding ‹rhs = nterm_to_pterm rhs'› by auto

  have "fdisjnt (freess pats) all_consts"
    using ‹(pats, rhs') |∈| irs'› ‹(name, irs') |∈| rs› inner
    by auto
  thus "fdisjnt (freess pats) (pre_constants.all_consts C_info (fst |`| compile rs))"
    unfolding compile_def by simp

  have "¬ shadows_consts rhs"
    unfolding ‹rhs = _› using ‹¬ shadows_consts _› by simp
  thus "¬ pre_constants.shadows_consts C_info (fst |`| compile rs) rhs"
    unfolding compile_heads .

  show "abs_ish pats rhs"
    using ‹pats ≠ []› unfolding abs_ish_def by simp

  have "welldefined rhs'"
    using fbspec[OF inner ‹(name, irs') |∈| rs›, simplified]
    using ‹(pats, rhs') |∈| irs'›
    by blast

  thus "pre_constants.welldefined C_info (fst |`| compile rs) rhs"
    unfolding compile_def ‹rhs = _›
    by simp
qed

sublocale crules ⊆ crules_as_irules: irules C_info "compile rs"
by (fact compile_rules)

subsubsection ‹Transformation of @{typ irule_set}›

definition transform_irules :: "irules ⇒ irules" where
"transform_irules rs = (
  if arity rs = 0 then rs
  else map_prod id Pabs |`| fgroup_by (λ(pats, rhs). (butlast pats, (last pats, rhs))) rs)"

lemma arity_compatibles_transform_irules:
  assumes "arity_compatibles rs"
  shows "arity_compatibles (transform_irules rs)"
proof (cases "arity rs = 0")
  case True
  thus ?thesis
    unfolding transform_irules_def using assms by simp
next
  case False
  let ?rs' = "transform_irules rs"
  let ?f = "λ(pats, rhs). (butlast pats, (last pats, rhs))"
  let ?grp = "fgroup_by ?f rs"
  have rs': "?rs' = map_prod id Pabs |`| ?grp"
    using False unfolding transform_irules_def by simp
  show ?thesis
    proof safe
      fix pats⇩1 rhs⇩1 pats⇩2 rhs⇩2
      assume "(pats⇩1, rhs⇩1) |∈| ?rs'" "(pats⇩2, rhs⇩2) |∈| ?rs'"
      then obtain rhs⇩1' rhs⇩2' where "(pats⇩1, rhs⇩1') |∈| ?grp" "(pats⇩2, rhs⇩2') |∈| ?grp"
        unfolding rs' by auto
      then obtain pats⇩1' pats⇩2' x y ― ‹dummies›
        where "fst (?f (pats⇩1', x)) = pats⇩1" "(pats⇩1', x) |∈| rs"
          and "fst (?f (pats⇩2', y)) = pats⇩2" "(pats⇩2', y) |∈| rs"
        by (fastforce simp: split_beta elim: fgroup_byE2)
      hence "pats⇩1 = butlast pats⇩1'" "pats⇩2 = butlast pats⇩2'" "length pats⇩1' = length pats⇩2'"
        using assms by (force dest: fpairwiseD)+
      thus "length pats⇩1 = length pats⇩2"
        by auto
    qed
qed

lemma arity_transform_irules:
  assumes "arity_compatibles rs" "rs ≠ {||}"
  shows "arity (transform_irules rs) = (if arity rs = 0 then 0 else arity rs - 1)"
proof (cases "arity rs = 0")
  case True
  thus ?thesis
    unfolding transform_irules_def by simp
next
  case False
  let ?f = "λ(pats, rhs). (butlast pats, (last pats, rhs))"
  let ?grp = "fgroup_by ?f rs"
  let ?rs' = "map_prod id Pabs |`| ?grp"

  have "arity ?rs' = arity rs - 1"
    proof (rule arityI)
      show "fBall ?rs' (λ(pats, _). length pats = arity rs - 1)"
        proof (rule prod_fBallI)
          fix pats rhs
          assume "(pats, rhs) |∈| ?rs'"
          then obtain cs where "(pats, cs) |∈| ?grp" "rhs = Pabs cs"
            by force
          then obtain pats' x ― ‹dummy›
            where "pats = butlast pats'" "(pats', x) |∈| rs"
            by (fastforce simp: split_beta elim: fgroup_byE2)
          hence "length pats' = arity rs"
            using assms by (metis arity_compatible_length)
          thus "length pats = arity rs - 1"
            unfolding ‹pats = butlast pats'› using False by simp
        qed
    next
      show "?rs' ≠ {||}"
        using assms by (simp add: fgroup_by_nonempty)
    qed

  with False show ?thesis
    unfolding transform_irules_def by simp
qed

definition transform_irule_set :: "irule_set ⇒ irule_set" where
"transform_irule_set = fimage (map_prod id transform_irules)"

lemma transform_irule_set_heads: "fst |`| transform_irule_set rs = fst |`| rs"
unfolding transform_irule_set_def by simp

lemma (in irules) rules_transform: "irules C_info (transform_irule_set rs)"
proof
  have "is_fmap rs"
    using fmap by simp
  thus "is_fmap (transform_irule_set rs)"
    unfolding transform_irule_set_def map_prod_def id_apply by (rule is_fmap_image)

  show "transform_irule_set rs ≠ {||}"
    using nonempty unfolding transform_irule_set_def by auto

  show "constants C_info (fst |`| transform_irule_set rs)"
    proof
      show "fdisjnt (fst |`| transform_irule_set rs) C"
        using disjnt unfolding transform_irule_set_def
        by force
    next
      show "distinct all_constructors"
        by (fact distinct_ctr)
    qed

  fix name irs
  assume irs: "(name, irs) |∈| transform_irule_set rs"
  then obtain irs' where "(name, irs') |∈| rs" "irs = transform_irules irs'"
    unfolding transform_irule_set_def by force
  hence "arity_compatibles irs'"
    using inner
    by (metis (no_types, lifting) case_prodD)
  thus "arity_compatibles irs"
    unfolding ‹irs = transform_irules irs'› by (rule arity_compatibles_transform_irules)

  have "irs' ≠ {||}"
    using ‹(name, irs') |∈| rs› inner by blast
  thus "irs ≠ {||}"
    unfolding ‹irs = transform_irules irs'› transform_irules_def
    by (simp add: fgroup_by_nonempty)

  let ?f = "λ(pats, rhs). (butlast pats, (last pats, rhs))"
  let ?grp = "fgroup_by ?f irs'"

  have "patterns_compatibles irs'"
    using ‹(name, irs') |∈| rs› inner
    by (blast dest: fpairwiseD)
  show "patterns_compatibles irs"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        using ‹patterns_compatibles irs'› by simp
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp

      show ?thesis
        proof safe
          fix pats⇩1 rhs⇩1 pats⇩2 rhs⇩2
          assume "(pats⇩1, rhs⇩1) |∈| irs" "(pats⇩2, rhs⇩2) |∈| irs"
          with irs' obtain cs⇩1 cs⇩2 where "(pats⇩1, cs⇩1) |∈| ?grp" "(pats⇩2, cs⇩2) |∈| ?grp"
            by force
          then obtain pats⇩1' pats⇩2' and x y ― ‹dummies›
            where "(pats⇩1', x) |∈| irs'" "(pats⇩2', y) |∈| irs'"
              and "pats⇩1 = butlast pats⇩1'" "pats⇩2 = butlast pats⇩2'"
            unfolding irs'
            by (fastforce elim: fgroup_byE2)
          hence "patterns_compatible pats⇩1' pats⇩2'"
            using ‹patterns_compatibles irs'› by (auto dest: fpairwiseD)
          thus "patterns_compatible pats⇩1 pats⇩2"
            unfolding ‹pats⇩1 = _› ‹pats⇩2 = _›
            by auto
        qed
    qed

  have "is_fmap irs'"
    using ‹(name, irs') |∈| rs› inner by blast
  show "is_fmap irs"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        using ‹is_fmap irs'› by simp
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp

      show ?thesis
        proof
          fix pats rhs⇩1 rhs⇩2
          assume "(pats, rhs⇩1) |∈| irs" "(pats, rhs⇩2) |∈| irs"
          with irs' obtain cs⇩1 cs⇩2
            where "(pats, cs⇩1) |∈| ?grp" "rhs⇩1 = Pabs cs⇩1"
              and "(pats, cs⇩2) |∈| ?grp" "rhs⇩2 = Pabs cs⇩2"
            by force
          moreover have "is_fmap ?grp"
            by auto
          ultimately show "rhs⇩1 = rhs⇩2"
            by (auto dest: is_fmapD)
        qed
    qed

  fix pats rhs
  assume "(pats, rhs) |∈| irs"

  show "linears pats"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        using ‹(pats, rhs) |∈| irs› ‹(name, irs') |∈| rs› inner
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        by auto
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp
      then obtain cs where "(pats, cs) |∈| ?grp"
        using ‹(pats, rhs) |∈| irs› by force
      then obtain pats' x ― ‹dummy›
        where "fst (?f (pats', x)) = pats" "(pats', x) |∈| irs'"
        by (fastforce simp: split_beta elim: fgroup_byE2)
      hence "pats = butlast pats'"
        by simp
      moreover have "linears pats'"
        using ‹(pats', x) |∈| irs'› ‹(name, irs') |∈| rs› inner
        by auto
      ultimately show ?thesis
        by auto
    qed

  have "fdisjnt (freess pats) all_consts"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        using ‹(pats, rhs) |∈| irs› ‹(name, irs') |∈| rs› inner
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        by auto
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp
      then obtain cs where "(pats, cs) |∈| ?grp"
        using ‹(pats, rhs) |∈| irs› by force
      then obtain pats' x ― ‹dummy›
        where "fst (?f (pats', x)) = pats" "(pats', x) |∈| irs'"
        by (fastforce simp: split_beta elim: fgroup_byE2)
      hence "pats = butlast pats'"
        by simp
      moreover have "fdisjnt (freess pats') all_consts"
        using ‹(pats', x) |∈| irs'› ‹(name, irs') |∈| rs› inner by auto
      ultimately show ?thesis
        by (metis subsetI in_set_butlastD freess_subset fdisjnt_subset_left)
    qed

  thus "fdisjnt (freess pats) (pre_constants.all_consts C_info (fst |`| transform_irule_set rs))"
    unfolding transform_irule_set_def by simp

  show "closed_except rhs (freess pats)"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        using ‹(pats, rhs) |∈| irs› ‹(name, irs') |∈| rs› inner
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        by auto
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp
      then obtain cs where "(pats, cs) |∈| ?grp" "rhs = Pabs cs"
        using ‹(pats, rhs) |∈| irs› by force

      show ?thesis
        unfolding ‹rhs = Pabs cs› closed_except_simps
        proof safe
          fix pat t
          assume "(pat, t) |∈| cs"
          then obtain pats' where "(pats', t) |∈| irs'" "?f (pats', t) = (pats, (pat, t))"
            using ‹(pats, cs) |∈| ?grp› by auto
          hence "closed_except t (freess pats')"
            using ‹(name, irs') |∈| rs› inner by auto

          have "pats' ≠ []"
            using ‹arity_compatibles irs'› ‹(pats', t) |∈| irs'› False
            by (metis list.size(3) arity_compatible_length)
          hence "pats' = pats @ [pat]"
            using ‹?f (pats', t) = (pats, (pat, t))›
            by (fastforce simp: split_beta snoc_eq_iff_butlast)
          hence "freess pats |∪| frees pat = freess pats'"
            unfolding freess_def by auto

          thus "closed_except t (freess pats |∪| frees pat)"
            using ‹closed_except t (freess pats')› by simp
        qed
    qed

  show "wellformed rhs"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        using ‹(pats, rhs) |∈| irs› ‹(name, irs') |∈| rs› inner
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        by auto
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp
      then obtain cs where "(pats, cs) |∈| ?grp" "rhs = Pabs cs"
        using ‹(pats, rhs) |∈| irs› by force

      show ?thesis
        unfolding ‹rhs = Pabs cs›
        proof (rule wellformed_PabsI)
          show "cs ≠ {||}"
            using ‹(pats, cs) |∈| ?grp› ‹irs' ≠ {||}›
            by (meson femptyE fgroup_by_nonempty_inner)
        next
          show "is_fmap cs"
            proof
              fix pat t⇩1 t⇩2
              assume "(pat, t⇩1) |∈| cs" "(pat, t⇩2) |∈| cs"
              then obtain pats⇩1' pats⇩2'
                where "(pats⇩1', t⇩1) |∈| irs'" "?f (pats⇩1', t⇩1) = (pats, (pat, t⇩1))"
                  and "(pats⇩2', t⇩2) |∈| irs'" "?f (pats⇩2', t⇩2) = (pats, (pat, t⇩2))"
                using ‹(pats, cs) |∈| ?grp› by force
              moreover hence "pats⇩1' ≠ []" "pats⇩2' ≠ []"
                using ‹arity_compatibles irs'› False
                unfolding prod.case
                by (metis list.size(3) arity_compatible_length)+
              ultimately have "pats⇩1' = pats @ [pat]" "pats⇩2' = pats @ [pat]"
                unfolding split_beta fst_conv snd_conv
                by (metis prod.inject snoc_eq_iff_butlast)+
              with ‹is_fmap irs'› show "t⇩1 = t⇩2"
                using ‹(pats⇩1', t⇩1) |∈| irs'› ‹(pats⇩2', t⇩2) |∈| irs'›
                by (blast dest: is_fmapD)
            qed
        next
          show "pattern_compatibles cs"
            proof safe
              fix pat⇩1 rhs⇩1 pat⇩2 rhs⇩2
              assume "(pat⇩1, rhs⇩1) |∈| cs" "(pat⇩2, rhs⇩2) |∈| cs"
              then obtain pats⇩1' pats⇩2'
                where "(pats⇩1', rhs⇩1) |∈| irs'" "?f (pats⇩1', rhs⇩1) = (pats, (pat⇩1, rhs⇩1))"
                  and "(pats⇩2', rhs⇩2) |∈| irs'" "?f (pats⇩2', rhs⇩2) = (pats, (pat⇩2, rhs⇩2))"
                using ‹(pats, cs) |∈| ?grp›
                by force
              moreover hence "pats⇩1' ≠ []" "pats⇩2' ≠ []"
                using ‹arity_compatibles irs'› False
                unfolding prod.case
                by (metis list.size(3) arity_compatible_length)+
              ultimately have "pats⇩1' = pats @ [pat⇩1]" "pats⇩2' = pats @ [pat⇩2]"
                unfolding split_beta fst_conv snd_conv
                by (metis prod.inject snoc_eq_iff_butlast)+
              moreover have "patterns_compatible pats⇩1' pats⇩2'"
                using ‹(pats⇩1', rhs⇩1) |∈| irs'› ‹(pats⇩2', rhs⇩2) |∈| irs'› ‹patterns_compatibles irs'›
                by (auto dest: fpairwiseD)
              ultimately show "pattern_compatible pat⇩1 pat⇩2"
                by (auto elim: rev_accum_rel_snoc_eqE)
            qed
        next
          fix pat t
          assume "(pat, t) |∈| cs"
          then obtain pats' where "(pats', t) |∈| irs'" "pat = last pats'"
            using ‹(pats, cs) |∈| ?grp› by auto
          moreover hence "pats' ≠ []"
            using ‹arity_compatibles irs'› False
            by (metis list.size(3) arity_compatible_length)
          ultimately have "pat ∈ set pats'"
            by auto

          moreover have "linears pats'"
            using ‹(pats', t) |∈| irs'› ‹(name, irs') |∈| rs› inner by auto
          ultimately show "linear pat"
            by (metis linears_linear)

          show "wellformed t"
            using ‹(pats', t) |∈| irs'› ‹(name, irs') |∈| rs› inner by auto
        qed
    qed

  have "¬ shadows_consts rhs"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        using ‹(pats, rhs) |∈| irs› ‹(name, irs') |∈| rs› inner
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        by auto
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp
      then obtain cs where "(pats, cs) |∈| ?grp" "rhs = Pabs cs"
        using ‹(pats, rhs) |∈| irs› by force

      show ?thesis
        unfolding ‹rhs = _›
        proof
          assume "shadows_consts (Pabs cs)"
          then obtain pat t where "(pat, t) |∈| cs" "shadows_consts t ∨ shadows_consts pat"
            by force
          then obtain pats' where "(pats', t) |∈| irs'" "pat = last pats'"
            using ‹(pats, cs) |∈| ?grp› by auto
          moreover hence "pats' ≠ []"
            using ‹arity_compatibles irs'› False
            by (metis list.size(3) arity_compatible_length)
          ultimately have "pat ∈ set pats'"
            by auto

          show False
            using ‹shadows_consts t ∨ shadows_consts pat›
            proof
              assume "shadows_consts t"
              thus False
                using ‹(name, irs') |∈| rs› ‹(pats', t) |∈| irs'› inner by auto
            next
              assume "shadows_consts pat"

              have "fdisjnt (freess pats') all_consts"
                using ‹(name, irs') |∈| rs› ‹(pats', t) |∈| irs'› inner by auto
              have "fdisjnt (frees pat) all_consts"
                apply (rule fdisjnt_subset_left)
                 apply (subst freess_single[symmetric])
                 apply (rule freess_subset)
                 apply simp
                 apply fact+
                done

              thus False
                using ‹shadows_consts pat›
                unfolding shadows_consts_def fdisjnt_alt_def by auto
          qed
        qed
    qed
  thus "¬ pre_constants.shadows_consts C_info (fst |`| transform_irule_set rs) rhs"
    by (simp add: transform_irule_set_heads)

  show "abs_ish pats rhs"
    proof (cases "arity irs' = 0")
      case True
      thus ?thesis
        using ‹(pats, rhs) |∈| irs› ‹(name, irs') |∈| rs› inner
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        by auto
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp
      then obtain cs where "(pats, cs) |∈| ?grp" "rhs = Pabs cs"
        using ‹(pats, rhs) |∈| irs› by force
      thus ?thesis
        unfolding abs_ish_def by (simp add: is_abs_def term_cases_def)
    qed

  have "welldefined rhs"
    proof (cases "arity irs' = 0")
      case True
      hence ‹(pats, rhs) |∈| irs'›
        using ‹(pats, rhs) |∈| irs› ‹(name, irs') |∈| rs› inner
        unfolding ‹irs = transform_irules irs'› transform_irules_def
        by (smt fBallE split_conv)
      thus ?thesis
        unfolding transform_irule_set_def
        using fbspec[OF inner ‹(name, irs') |∈| rs›, simplified]
        by force
    next
      case False
      hence irs': "irs = map_prod id Pabs |`| ?grp"
        unfolding ‹irs = transform_irules irs'› transform_irules_def by simp
      then obtain cs where "(pats, cs) |∈| ?grp" "rhs = Pabs cs"
        using ‹(pats, rhs) |∈| irs› by force
      show ?thesis
        unfolding ‹rhs = _›
        apply simp
        apply (rule ffUnion_least)
        unfolding ball_simps
        apply rule
        apply (rename_tac x, case_tac x, hypsubst_thin)
        apply simp
        subgoal premises prems for pat t
          proof -
            from prems obtain pats' where "(pats', t) |∈| irs'"
              using ‹(pats, cs) |∈| ?grp› by auto
            hence "welldefined t"
              using fbspec[OF inner ‹(name, irs') |∈| rs›, simplified]
              by blast
            thus ?thesis
              unfolding transform_irule_set_def
              by simp
          qed
        done
    qed
  thus "pre_constants.welldefined C_info (fst |`| transform_irule_set rs) rhs"
    unfolding transform_irule_set_heads .
qed


subsubsection ‹Matching and rewriting›

definition irewrite_step :: "name ⇒ term list ⇒ pterm ⇒ pterm ⇒ pterm option" where
"irewrite_step name pats rhs t = map_option (subst rhs) (match (name $$ pats) t)"

abbreviation irewrite_step' :: "name ⇒ term list ⇒ pterm ⇒ pterm ⇒ pterm ⇒ bool" ("_, _, _ ⊢⇩i/ _ →/ _" [50,0,50] 50) where
"name, pats, rhs ⊢⇩i t → u ≡ irewrite_step name pats rhs t = Some u"

lemma irewrite_stepI:
  assumes "match (name $$ pats) t = Some env" "subst rhs env = u"
  shows "name, pats, rhs ⊢⇩i t → u"
using assms unfolding irewrite_step_def by simp

inductive irewrite :: "irule_set ⇒ pterm ⇒ pterm ⇒ bool" ("_/ ⊢⇩i/ _ ⟶/ _" [50,0,50] 50) for irs where
step: "⟦ (name, rs) |∈| irs; (pats, rhs) |∈| rs; name, pats, rhs ⊢⇩i t → t' ⟧ ⟹ irs ⊢⇩i t ⟶ t'" |
beta: "⟦ c |∈| cs; c ⊢ t → t' ⟧ ⟹ irs ⊢⇩i Pabs cs $⇩p t ⟶ t'" |
"fun": "irs ⊢⇩i t ⟶ t' ⟹ irs ⊢⇩i t $⇩p u ⟶ t' $⇩p u" |
arg: "irs ⊢⇩i u ⟶ u' ⟹ irs ⊢⇩i t $⇩p u ⟶ t $⇩p u'"

global_interpretation irewrite: rewriting "irewrite rs" for rs
by standard (auto intro: irewrite.intros simp: app_pterm_def)+

abbreviation irewrite_rt :: "irule_set ⇒ pterm ⇒ pterm ⇒ bool" ("_/ ⊢⇩i/ _ ⟶*/ _" [50,0,50] 50) where
"irewrite_rt rs ≡ (irewrite rs)⇧*⇧*"

lemma (in irules) irewrite_closed:
  assumes "rs ⊢⇩i t ⟶ u" "closed t"
  shows "closed u"
using assms proof induction
  case (step name rs pats rhs t t')
  then obtain env where "match (name $$ pats) t = Some env" "t' = subst rhs env"
    unfolding irewrite_step_def by auto
  hence "closed_env env"
    using step by (auto intro: closed.match)

  show ?case
    unfolding ‹t' = _›
    apply (subst closed_except_def)
    apply (subst subst_frees)
     apply fact
    apply (subst match_dom)
     apply fact
    apply (subst frees_list_comb)
    apply simp
    apply (subst closed_except_def[symmetric])
    using inner step by fastforce
next
  case (beta c cs t t')
  then obtain pat rhs where "c = (pat, rhs)"
    by (cases c) auto
  with beta obtain env where "match pat t = Some env" "t' = subst rhs env"
    by auto
  moreover have "closed t"
    using beta unfolding closed_except_def by simp
  ultimately have "closed_env env"
    using beta by (auto intro: closed.match)

  show ?case
    unfolding ‹t' = subst rhs env›
    apply (subst closed_except_def)
    apply (subst subst_frees)
     apply fact
    apply (subst match_dom)
     apply fact
    apply simp
    apply (subst closed_except_def[symmetric])
    using inner beta ‹c = _› by (auto simp: closed_except_simps)
qed (auto simp: closed_except_def)

corollary (in irules) irewrite_rt_closed:
  assumes "rs ⊢⇩i t ⟶* u" "closed t"
  shows "closed u"
using assms by induction (auto intro: irewrite_closed)

subsubsection ‹Correctness of translation›

abbreviation irelated :: "nterm ⇒ pterm ⇒ bool" ("_ ≈⇩i _" [0,50] 50) where
"n ≈⇩i p ≡ nterm_to_pterm n = p"

global_interpretation irelated: term_struct_rel_strong irelated
by standard
   (auto simp: app_pterm_def app_nterm_def const_pterm_def const_nterm_def elim: nterm_to_pterm.elims)

lemma irelated_vars: "t ≈⇩i u ⟹ frees t = frees u"
by auto

lemma irelated_no_abs:
  assumes "t ≈⇩i u"
  shows "no_abs t ⟷ no_abs u"
using assms
apply (induction arbitrary: t)
 apply (auto elim!: nterm_to_pterm.elims)
   apply (fold const_nterm_def const_pterm_def free_nterm_def free_pterm_def app_pterm_def app_nterm_def)
by auto

lemma irelated_subst:
  assumes "t ≈⇩i u" "irelated.P_env nenv penv"
  shows "subst t nenv ≈⇩i subst u penv"
using assms proof (induction arbitrary: nenv penv u rule: nterm_to_pterm.induct)
  case (1 s)
  then show ?case
    by (auto elim!: fmrel_cases[where x = s])
next
  case 4
  from 4(2)[symmetric] show ?case
    apply simp
    apply (rule 4)
     apply simp
    using 4(3)
    by (simp add: fmrel_drop)
qed auto

lemma related_irewrite_step:
  assumes "name, pats, nterm_to_pterm rhs ⊢⇩i u → u'" "t ≈⇩i u"
  obtains t' where "unsplit_rule (name, pats, rhs) ⊢ t → t'" "t' ≈⇩i u'"
proof -
  let ?rhs' = "nterm_to_pterm rhs"
  let ?x = "name $$ pats"

  from assms obtain env where "match ?x u = Some env" "u' = subst ?rhs' env"
    unfolding irewrite_step_def by blast
  then obtain nenv where "match ?x t = Some nenv" "irelated.P_env nenv env"
    using assms
    by (metis Option.is_none_def not_None_eq option.rel_distinct(1) option.sel rel_option_unfold irelated.match_rel)

  show thesis
    proof
      show "unsplit_rule (name, pats, rhs) ⊢ t → subst rhs nenv"
        using ‹match ?x t = _› by auto
    next
      show "subst rhs nenv ≈⇩i u'"
        unfolding ‹u' = _› using ‹irelated.P_env nenv env›
        by (auto intro: irelated_subst)
    qed
qed

theorem (in nrules) compile_correct:
  assumes "compile (consts_of rs) ⊢⇩i u ⟶ u'" "t ≈⇩i u" "closed t"
  obtains t' where "rs ⊢⇩n t ⟶ t'" "t' ≈⇩i u'"
using assms(1-3) proof (induction arbitrary: t thesis rule: irewrite.induct)
  case (step name irs pats rhs u u')
  then obtain crs where "irs = translate_crules crs" "(name, crs) |∈| consts_of rs"
    unfolding compile_def by force
  moreover with step obtain rhs' where "rhs = nterm_to_pterm rhs'" "(pats, rhs') |∈| crs"
    unfolding translate_crules_def by force
  ultimately obtain rule where "split_rule rule = (name, (pats, rhs'))" "rule |∈| rs"
    unfolding consts_of_def by blast
  hence "nrule rule"
    using all_rules by blast

  obtain t' where "unsplit_rule (name, pats, rhs') ⊢ t → t'" "t' ≈⇩i u'"
    using ‹name, pats, rhs ⊢⇩i u → u'› ‹t ≈⇩i u› unfolding ‹rhs = nterm_to_pterm rhs'›
    by (elim related_irewrite_step)
  hence "rule ⊢ t → t'"
    using ‹nrule rule› ‹split_rule rule = (name, (pats, rhs'))›
    by (metis unsplit_split)

  show ?case
    proof (rule step.prems)
      show "rs ⊢⇩n t ⟶ t'"
        apply (rule nrewrite.step)
         apply fact
        apply fact
        done
    next
      show "t' ≈⇩i u'"
        by fact
    qed
next
  case (beta c cs u u')
  then obtain pat rhs where "c = (pat, rhs)" "(pat, rhs) |∈| cs"
    by (cases c) auto
  obtain v w where "t = v $⇩n w" "v ≈⇩i Pabs cs" "w ≈⇩i u"
    using ‹t ≈⇩i Pabs cs $⇩p u› by (auto elim: nterm_to_pterm.elims)
  obtain x nrhs irhs where "v = (Λ⇩n x. nrhs)" "cs = {| (Free x, irhs) |}" "nrhs ≈⇩i irhs"
    using ‹v ≈⇩i Pabs cs› by (auto elim: nterm_to_pterm.elims)
  hence "t = (Λ⇩n x. nrhs) $⇩n w" "Λ⇩n x. nrhs ≈⇩i Λ⇩p x. irhs"
    unfolding ‹t = v $⇩n w› using ‹v ≈⇩i Pabs cs› by auto

  have "pat = Free x" "rhs = irhs"
    using ‹cs = {| (Free x, irhs) |}› ‹(pat, rhs) |∈| cs› by auto
  hence "(Free x, irhs) ⊢ u → u'"
    using beta ‹c = _› by simp
  hence "u' = subst irhs (fmap_of_list [(x, u)])"
    by simp

  show ?case
    proof (rule beta.prems)
      show "rs ⊢⇩n t ⟶ subst nrhs (fmap_of_list [(x, w)])"
        unfolding ‹t = (Λ⇩n x. nrhs) $⇩n w›
        by (rule nrewrite.beta)
    next
      show "subst nrhs (fmap_of_list [(x, w)]) ≈⇩i u'"
        unfolding ‹u' = subst irhs _›
        apply (rule irelated_subst)
         apply fact
        apply simp
        apply rule
         apply rule
        apply fact
        done
    qed
next
  case ("fun" v v' u)
  obtain w x where "t = w $⇩n x" "w ≈⇩i v" "x ≈⇩i u"
    using ‹t ≈⇩i v $⇩p u› by (auto elim: nterm_to_pterm.elims)
  with "fun" obtain w' where "rs ⊢⇩n w ⟶ w'" "w' ≈⇩i v'"
    unfolding closed_except_def by auto

  show ?case
    proof (rule fun.prems)
      show "rs ⊢⇩n t ⟶ w' $⇩n x"
        unfolding ‹t = w $⇩n x›
        by (rule nrewrite.fun) fact
    next
      show "w' $⇩n x ≈⇩i v' $⇩p u"
        by auto fact+
    qed
next
  case (arg u u' v)
  obtain w x where "t = w $⇩n x" "w ≈⇩i v" "x ≈⇩i u"
    using ‹ t ≈⇩i v $⇩p u› by (auto elim: nterm_to_pterm.elims)
  with arg obtain x' where "rs ⊢⇩n x ⟶ x'" "x' ≈⇩i u'"
    unfolding closed_except_def by auto

  show ?case
    proof (rule arg.prems)
      show "rs ⊢⇩n t ⟶ w $⇩n x'"
        unfolding ‹t = w $⇩n x›
        by (rule nrewrite.arg) fact
    next
      show "w $⇩n x' ≈⇩i v $⇩p u'"
        by auto fact+
    qed
qed

corollary (in nrules) compile_correct_rt:
  assumes "compile (consts_of rs) ⊢⇩i u ⟶* u'" "t ≈⇩i u" "closed t"
  obtains t' where "rs ⊢⇩n t ⟶* t'" "t' ≈⇩i u'"
using assms proof (induction arbitrary: thesis t) (* FIXME clone of transform_correct_rt, maybe locale? *)
  case (step u' u'')

  obtain t' where "rs ⊢⇩n t ⟶* t'" "t' ≈⇩i u'"
    using step by blast

  obtain t'' where "rs ⊢⇩n t' ⟶* t''" "t'' ≈⇩i u''"
    proof (rule compile_correct)
      show "compile (consts_of rs) ⊢⇩i u' ⟶ u''" "t' ≈⇩i u'"
        by fact+
    next
      show "closed t'"
        using ‹rs ⊢⇩n t ⟶* t'› ‹closed t›
        by (rule nrewrite_rt_closed)
    qed blast

  show ?case
    proof (rule step.prems)
      show "rs ⊢⇩n t ⟶* t''"
        using ‹rs ⊢⇩n t ⟶* t'› ‹rs ⊢⇩n t' ⟶* t''› by auto
    qed fact
qed blast

subsubsection ‹Completeness of translation›

lemma (in nrules) compile_complete:
  assumes "rs ⊢⇩n t ⟶ t'" "closed t"
  shows "compile (consts_of rs) ⊢⇩i nterm_to_pterm t ⟶ nterm_to_pterm t'"
  using assms proof induction
  case (step r t t')
  then obtain pat rhs' where "r = (pat, rhs')"
    by force
  then have "(pat, rhs') |∈| rs" "(pat, rhs') ⊢ t → t'"
    using step by blast+
  then have "nrule (pat, rhs')"
    using all_rules by blast
  then obtain name pats where "(name, (pats, rhs')) = split_rule r" "pat = name $$ pats"
    unfolding split_rule_def ‹r = _›
    apply atomize_elim
    by (auto simp: split_beta)

  obtain crs where "(name, crs) |∈| consts_of rs" "(pats, rhs') |∈| crs"
    using step ‹_ = split_rule r› ‹r = _›
    by (metis consts_of_def fgroup_by_complete fst_conv snd_conv)
  then obtain irs where "irs = translate_crules crs"
    by blast
  then have "(name, irs) |∈| compile (consts_of rs)"
    unfolding compile_def
    using ‹(name, _) |∈| _›
    by (metis fimageI id_def map_prod_simp)
  obtain rhs where "rhs = nterm_to_pterm rhs'" "(pats, rhs) |∈| irs"
    using ‹irs = _› ‹_ |∈| crs›
    unfolding translate_crules_def
    by (metis fimageI id_def map_prod_simp)

  from step obtain env' where "match pat t = Some env'" "t' = subst rhs' env'"
    unfolding ‹r = _› using rewrite_step.simps
    by force
  then obtain env where "match pat (nterm_to_pterm t) = Some env" "irelated.P_env env' env"
    by (metis irelated.match_rel option_rel_Some1)
  then have "subst rhs env = nterm_to_pterm t'"
    unfolding ‹t' = _›
    apply -
    apply (rule sym)
    apply (rule irelated_subst)
    unfolding ‹rhs = _›
    by auto

  have "name, pats, rhs ⊢⇩i nterm_to_pterm t → nterm_to_pterm t'"
    apply (rule irewrite_stepI)
    using ‹match _ _ = Some env› unfolding ‹pat = _›
     apply assumption
    by fact

  show ?case
    by rule fact+
next
  case (beta x t t')
  obtain c where "c = (Free x, nterm_to_pterm t)"
    by blast
  from beta have "closed (nterm_to_pterm t')"
    using closed_nterm_to_pterm[where t = t']
    unfolding closed_except_def
    by auto
  show ?case
    apply simp
    apply rule
    using ‹c = _›
    by (fastforce intro: irelated_subst[THEN sym])+
next
  case ("fun" t t' u)
  show ?case
    apply simp
    apply rule
    apply (rule "fun")
    using "fun"
    unfolding closed_except_def
    apply simp
    done
next
  case (arg u u' t)
  show ?case
    apply simp
    apply rule
    apply (rule arg)
    using arg
    unfolding closed_except_def
    by simp
qed


subsubsection ‹Correctness of transformation›

abbreviation irules_deferred_matches :: "pterm list ⇒ irules ⇒ (term × pterm) fset" where
"irules_deferred_matches args ≡ fselect
  (λ(pats, rhs). map_option (λenv. (last pats, subst rhs env)) (matchs (butlast pats) args))"

context irules begin

inductive prelated :: "pterm ⇒ pterm ⇒ bool" ("_ ≈⇩p _" [0,50] 50) where
const: "Pconst x ≈⇩p Pconst x" |
var: "Pvar x ≈⇩p Pvar x" |
app: "t⇩1 ≈⇩p u⇩1 ⟹ t⇩2 ≈⇩p u⇩2 ⟹ t⇩1 $⇩p t⇩2 ≈⇩p u⇩1 $⇩p u⇩2" |
pat: "rel_fset (rel_prod (=) prelated) cs⇩1 cs⇩2 ⟹ Pabs cs⇩1 ≈⇩p Pabs cs⇩2" |
"defer":
  "(name, rsi) |∈| rs ⟹ 0 < arity rsi ⟹
   rel_fset (rel_prod (=) prelated) (irules_deferred_matches args rsi) cs ⟹
   list_all closed args ⟹
   name $$ args ≈⇩p Pabs cs"

inductive_cases prelated_absE[consumes 1, case_names pat "defer"]: "t ≈⇩p Pabs cs"

lemma prelated_refl[intro!]: "t ≈⇩p t"
proof (induction t)
  case Pabs
  thus ?case
    by (auto simp: snds.simps intro!: prelated.pat rel_fset_refl_strong rel_prod.intros)
qed (auto intro: prelated.intros)

sublocale prelated: term_struct_rel prelated
by standard (auto simp: const_pterm_def app_pterm_def intro: prelated.intros elim: prelated.cases)

lemma prelated_pvars:
  assumes "t ≈⇩p u"
  shows "frees t = frees u"
using assms proof (induction rule: prelated.induct)
  case (pat cs⇩1 cs⇩2)
  show ?case
    apply simp
    apply (rule arg_cong[where f = ffUnion])
    apply (rule rel_fset_image_eq)
     apply fact
    apply auto
    done
next
  case ("defer" name rsi args cs)

  {
    fix pat t
    assume "(pat, t) |∈| cs"
    with "defer" obtain t'
      where "(pat, t') |∈| irules_deferred_matches args rsi" "frees t = frees t'"
      by (auto elim: rel_fsetE2)
    then obtain pats rhs env
      where "pat = last pats" "(pats, rhs) |∈| rsi"
        and "matchs (butlast pats) args = Some env" "t' = subst rhs env"
      by auto

    have "closed_except rhs (freess pats)" "linears pats"
      using ‹(pats, rhs) |∈| rsi› ‹(name, rsi) |∈| rs› inner by auto

    have "arity_compatibles rsi"
      using "defer" inner
      by (metis (no_types, lifting) case_prodD)
    have "length pats > 0"
      by (subst arity_compatible_length) fact+
    hence "pats = butlast pats @ [last pats]"
      by simp

    note ‹frees t = frees t'›
    also have "frees t' = frees rhs - fmdom env"
      unfolding ‹t' = _›
      apply (rule subst_frees)
      apply (rule closed.matchs)
       apply fact+
      done
    also have "… = frees rhs - freess (butlast pats)"
      using ‹matchs _ _ = _› by (metis matchs_dom)
    also have "… |⊆| freess pats - freess (butlast pats)"
      using ‹closed_except _ _›
      by (auto simp: closed_except_def)
    also have "… = frees (last pats) |-| freess (butlast pats)"
      by (subst ‹pats = _›) (simp add: funion_fminus)
    also have "… = frees (last pats)"
      proof (rule fminus_triv)
        have "fdisjnt (freess (butlast pats)) (freess [last pats])"
          using ‹linears pats› ‹pats = _›
          by (metis linears_appendD)
        thus "frees (last pats) |∩| freess (butlast pats) = {||}"
          by (fastforce simp: fdisjnt_alt_def)
      qed
    also have "… = frees pat" unfolding ‹pat = _› ..
    finally have "frees t |⊆| frees pat" .
  }
  hence "closed (Pabs cs)"
    unfolding closed_except_simps
    by (auto simp: closed_except_def)
  moreover have "closed (name $$ args)"
    unfolding closed_list_comb by fact
  ultimately show ?case
    unfolding closed_except_def by simp
qed auto

corollary prelated_closed: "t ≈⇩p u ⟹ closed t ⟷ closed u"
unfolding closed_except_def
by (auto simp: prelated_pvars)

lemma prelated_no_abs_right:
  assumes "t ≈⇩p u" "no_abs u"
  shows "t = u"
using assms
apply (induction rule: prelated.induct)
    apply auto
 apply (fold app_pterm_def)
 apply auto
done

corollary env_prelated_refl[intro!]: "prelated.P_env env env"
by (auto intro: fmap.rel_refl)

text ‹
  The following, more general statement does not hold:
    @{prop "t ≈⇩p u ⟹ rel_option prelated.P_env (match x t) (match x u)"}
  If @{text t} and @{text u} are related because of the @{thm [source=true] prelated.defer} rule,
  they have completely different shapes.
  Establishing @{prop "is_abs t ⟷ is_abs u"} as a precondition would rule out this case, but at
  the same time be too restrictive.

  Instead, we use @{thm prelated.related_match}.
›

lemma prelated_subst:
  assumes "t⇩1 ≈⇩p t⇩2" "prelated.P_env env⇩1 env⇩2"
  shows "subst t⇩1 env⇩1 ≈⇩p subst t⇩2 env⇩2"
using assms proof (induction arbitrary: env⇩1 env⇩2 rule: prelated.induct)
  case (var x)
  thus ?case
    proof (cases rule: fmrel_cases[where x = x])
      case none
      thus ?thesis
        by (auto intro: prelated.var)
    next
      case (some t u)
      thus ?thesis
        by simp
    qed
next
  case (pat cs⇩1 cs⇩2)
  let ?drop = "λenv. λ(pat::term). fmdrop_fset (frees pat) env"
  from pat have "prelated.P_env (?drop env⇩1 pat) (?drop env⇩2 pat)" for pat
    by blast
  with pat show ?case
    by (auto intro!: prelated.pat rel_fset_image)
next
  case ("defer" name rsi args cs)
  have "name $$ args ≈⇩p Pabs cs"
    apply (rule prelated.defer)
       apply fact+
     apply (rule fset.rel_mono_strong)
      apply fact
     apply force
    apply fact
    done
  moreover have "closed (name $$ args)"
    unfolding closed_list_comb by fact
  ultimately have "closed (Pabs cs)"
    by (metis prelated_closed)

  let ?drop = "λenv. λpat. fmdrop_fset (frees pat) env"
  let ?f = "λenv. (λ(pat, rhs). (pat, subst rhs (?drop env pat)))"

  have "name $$ args ≈⇩p Pabs (?f env⇩2 |`| cs)"
    proof (rule prelated.defer)
      show "(name, rsi) |∈| rs" "0 < arity rsi" "list_all closed args"
        using "defer" by auto
    next
      {
        fix pat⇩1 rhs⇩1
        fix pat⇩2 rhs⇩2
        assume "(pat⇩2, rhs⇩2) |∈| cs"
        assume "pat⇩1 = pat⇩2" "rhs⇩1 ≈⇩p rhs⇩2"
        have "rhs⇩1 ≈⇩p subst rhs⇩2 (fmdrop_fset (frees pat⇩2) env⇩2)"
          by (subst subst_closed_pabs) fact+
      }
      hence "rel_fset (rel_prod (=) prelated) (id |`| irules_deferred_matches args rsi) (?f env⇩2 |`| cs)"
        by (force intro!: rel_fset_image[OF ‹rel_fset _ _ _›])

      thus "rel_fset (rel_prod (=) prelated) (irules_deferred_matches args rsi) (?f env⇩2 |`| cs)"
        by simp
    qed

  moreover have "map (λt. subst t env⇩1) args = args"
    apply (rule map_idI)
    apply (rule subst_closed_id)
    using "defer" by (simp add: list_all_iff)

  ultimately show ?case
    by (simp add: subst_list_comb)
qed (auto intro: prelated.intros)

lemma prelated_step:
  assumes "name, pats, rhs ⊢⇩i u → u'" "t ≈⇩p u"
  obtains t' where "name, pats, rhs ⊢⇩i t → t'" "t' ≈⇩p u'"
proof -
  let ?lhs = "name $$ pats"
  from assms obtain env where "match ?lhs u = Some env" "u' = subst rhs env"
    unfolding irewrite_step_def by blast
  then obtain env' where "match ?lhs t = Some env'" "prelated.P_env env' env"
    using assms by (auto elim: prelated.related_match)
  hence "subst rhs env' ≈⇩p subst rhs env"
    using assms by (auto intro: prelated_subst)

  show thesis
    proof
      show "name, pats, rhs ⊢⇩i t → subst rhs env'"
        unfolding irewrite_step_def using ‹match ?lhs t = Some env'›
        by simp
    next
      show "subst rhs env' ≈⇩p u'"
        unfolding ‹u' = subst rhs env›
        by fact
    qed
qed

(* FIXME write using relators *)
lemma prelated_beta: ― ‹same problem as @{thm [source=true] prelated.related_match}›
  assumes "(pat, rhs⇩2) ⊢ t⇩2 → u⇩2" "rhs⇩1 ≈⇩p rhs⇩2" "t⇩1 ≈⇩p t⇩2"
  obtains u⇩1 where "(pat, rhs⇩1) ⊢ t⇩1 → u⇩1" "u⇩1 ≈⇩p u⇩2"
proof -
  from assms obtain env⇩2 where "match pat t⇩2 = Some env⇩2" "u⇩2 = subst rhs⇩2 env⇩2"
    by auto
  with assms obtain env⇩1 where "match pat t⇩1 = Some env⇩1" "prelated.P_env env⇩1 env⇩2"
    by (auto elim: prelated.related_match)
  with assms have "subst rhs⇩1 env⇩1 ≈⇩p subst rhs⇩2 env⇩2"
    by (auto intro: prelated_subst)

  show thesis
    proof
      show "(pat, rhs⇩1) ⊢ t⇩1 → subst rhs⇩1 env⇩1"
        using ‹match pat t⇩1 = _› by simp
    next
      show "subst rhs⇩1 env⇩1 ≈⇩p u⇩2"
        unfolding ‹u⇩2 = _› by fact
    qed
qed

theorem transform_correct:
  assumes "transform_irule_set rs ⊢⇩i u ⟶ u'" "t ≈⇩p u" "closed t"
  obtains t' where "rs ⊢⇩i t ⟶* t'" ― ‹zero or one step› and "t' ≈⇩p u'"
using assms(1-3) proof (induction arbitrary: t thesis rule: irewrite.induct)
  case (beta c cs⇩2 u⇩2 x⇩2')
  obtain v u⇩1 where "t = v $⇩p u⇩1" "v ≈⇩p Pabs cs⇩2" "u⇩1 ≈⇩p u⇩2"
    using ‹t ≈⇩p Pabs cs⇩2 $⇩p u⇩2› by cases
  with beta have "closed u⇩1"
    by (simp add: closed_except_def)

  obtain pat rhs⇩2 where "c = (pat, rhs⇩2)" by (cases c) auto

  from ‹v ≈⇩p Pabs cs⇩2› show ?case
    proof (cases rule: prelated_absE)
      case (pat cs⇩1)
      with beta ‹c = _› obtain rhs⇩1 where "(pat, rhs⇩1) |∈| cs⇩1" "rhs⇩1 ≈⇩p rhs⇩2"
        by (auto elim: rel_fsetE2)
      with beta obtain x⇩1' where "(pat, rhs⇩1) ⊢ u⇩1 → x⇩1'" "x⇩1' ≈⇩p x⇩2'"
        using ‹u⇩1 ≈⇩p u⇩2› assms ‹c = _›
        by (auto elim: prelated_beta simp del: rewrite_step.simps)

      show ?thesis
        proof (rule beta.prems)
          show "rs ⊢⇩i t ⟶* x⇩1'"
            unfolding ‹t = _› ‹v = _›
            by (intro r_into_rtranclp irewrite.beta) fact+
        next
          show "x⇩1' ≈⇩p x⇩2'"
            by fact
      qed
    next
      case ("defer" name rsi args)
      with beta ‹c = _› obtain rhs⇩1' where "(pat, rhs⇩1') |∈| irules_deferred_matches args rsi" "rhs⇩1' ≈⇩p rhs⇩2"
        by (auto elim: rel_fsetE2)
      then obtain env⇩a rhs⇩1 pats
        where "matchs (butlast pats) args = Some env⇩a" "pat = last pats" "rhs⇩1' = subst rhs⇩1 env⇩a"
          and "(pats, rhs⇩1) |∈| rsi"
        by auto
      hence "linears pats"
        using ‹(name, rsi) |∈| rs› inner unfolding irules_def by auto

      have "arity_compatibles rsi"
        using "defer" inner
        by (metis (no_types, lifting) case_prodD)
      have "length pats > 0"
        by (subst arity_compatible_length) fact+
      hence "pats = butlast pats @ [pat]"
        unfolding ‹pat = _› by simp

      from beta ‹c = _› obtain env⇩b where "match pat u⇩2 = Some env⇩b" "x⇩2' = subst rhs⇩2 env⇩b"
        by fastforce
      with ‹u⇩1 ≈⇩p u⇩2› obtain env⇩b' where "match pat u⇩1 = Some env⇩b'" "prelated.P_env env⇩b' env⇩b"
        by (metis prelated.related_match)

      have "closed_env env⇩a"
        by (rule closed.matchs) fact+
      have "closed_env env⇩b'"
        apply (rule closed.matchs[where pats = "[pat]" and ts = "[u⇩1]"])
         apply simp
         apply fact
        apply simp
        apply fact
        done

      have "fmdom env⇩a = freess (butlast pats)"
        by (rule matchs_dom) fact
      moreover have "fmdom env⇩b' = frees pat"
        by (rule match_dom) fact
      moreover have "fdisjnt (freess (butlast pats)) (frees pat)"
        using ‹pats = _› ‹linears pats›
        by (metis freess_single linears_appendD(3))
      ultimately have "fdisjnt (fmdom env⇩a) (fmdom env⇩b')"
        by simp

      show ?thesis
        proof (rule beta.prems)
          have "rs ⊢⇩i name $$ args $⇩p u⇩1 ⟶ subst rhs⇩1' env⇩b'"
            proof (rule irewrite.step)
              show "(name, rsi) |∈| rs" "(pats, rhs⇩1) |∈| rsi"
                by fact+
            next
              show "name, pats, rhs⇩1 ⊢⇩i name $$ args $⇩p u⇩1 → subst rhs⇩1' env⇩b'"
                apply (rule irewrite_stepI)
                 apply (fold app_pterm_def)
                 apply (subst list_comb_snoc)
                 apply (subst matchs_match_list_comb)
                 apply (subst ‹pats = _›)
                 apply (rule matchs_appI)
                  apply fact
                 apply simp
                 apply fact
                unfolding ‹rhs⇩1' = _›
                apply (rule subst_indep')
                 apply fact+
                done
            qed
          thus "rs ⊢⇩i t ⟶* subst rhs⇩1' env⇩b'"
            unfolding ‹t = _› ‹v = _›
            by (rule r_into_rtranclp)
        next
          show "subst rhs⇩1' env⇩b' ≈⇩p x⇩2'"
            unfolding ‹x⇩2' = _›
            by (rule prelated_subst) fact+
        qed
    qed
next
  case (step name rs⇩2 pats rhs u u')
  then obtain rs⇩1 where "rs⇩2 = transform_irules rs⇩1" "(name, rs⇩1) |∈| rs"
    unfolding transform_irule_set_def by force
  hence "arity_compatibles rs⇩1"
    using inner
    by (metis (no_types, lifting) case_prodD)

  show ?case
    proof (cases "arity rs⇩1 = 0")
      case True
      hence "rs⇩2 = rs⇩1"
        unfolding ‹rs⇩2 = _› transform_irules_def by simp
      with step have "(pats, rhs) |∈| rs⇩1"
        by simp
      from step obtain t' where "name, pats, rhs ⊢⇩i t → t'" "t' ≈⇩p u'"
        using assms
        by (auto elim: prelated_step)

      show ?thesis
        proof (rule step.prems)
          show "rs ⊢⇩i t ⟶* t'"
            by (intro conjI exI r_into_rtranclp irewrite.step) fact+
        qed fact
    next
      let ?f = "λ(pats, rhs). (butlast pats, last pats, rhs)"
      let ?grp = "fgroup_by ?f rs⇩1"

      case False
      hence "rs⇩2 = map_prod id Pabs |`| ?grp"
        unfolding ‹rs⇩2 = _› transform_irules_def by simp
      with step obtain cs where "rhs = Pabs cs" "(pats, cs) |∈| ?grp"
        by force

      from step obtain env⇩2 where "match (name $$ pats) u = Some env⇩2" "u' = subst rhs env⇩2"
        unfolding irewrite_step_def by auto
      then obtain args⇩2 where "u = name $$ args⇩2" "matchs pats args⇩2 = Some env⇩2"
        by (auto elim: match_list_combE)
      with step obtain args⇩1 where "t = name $$ args⇩1" "list_all2 prelated args⇩1 args⇩2"
        by (auto elim: prelated.list_combE)

      then obtain env⇩1 where "matchs pats args⇩1 = Some env⇩1" "prelated.P_env env⇩1 env⇩2"
        using ‹matchs pats args⇩2 = _› by (metis prelated.related_matchs)
      hence "fmdom env⇩1 = freess pats"
        by (auto simp: matchs_dom)

      obtain cs' where "u' = Pabs cs'"
        unfolding ‹u' = _› ‹rhs = _› by auto

      hence "cs' = (λ(pat, rhs). (pat, subst rhs (fmdrop_fset (frees pat) env⇩2 ))) |`| cs"
        using ‹u' = subst rhs env⇩2› unfolding ‹rhs = _›
        by simp

      show ?thesis
        proof (rule step.prems)
          show "rs ⊢⇩i t ⟶* t"
            by (rule rtranclp.rtrancl_refl)
        next
          show "t ≈⇩p u'"
            unfolding ‹u' = Pabs cs'› ‹t = _›
            proof (intro prelated.defer rel_fsetI; safe?)
              show "(name, rs⇩1) |∈| rs"
                by fact
            next
              show "0 < arity rs⇩1"
                using False by simp
            next
              show "list_all closed args⇩1"
                using ‹closed t› unfolding ‹t = _› closed_list_comb .
            next
              fix pat rhs'
              assume "(pat, rhs') |∈| irules_deferred_matches args⇩1 rs⇩1"
              then obtain pats' rhs env
                where "(pats', rhs) |∈| rs⇩1"
                  and "matchs (butlast pats') args⇩1 = Some env" "pat = last pats'" "rhs' = subst rhs env"
                by auto
              with False have "pats' ≠ []"
                using ‹arity_compatibles rs⇩1›
                by (metis list.size(3) arity_compatible_length)
              hence "butlast pats' @ [last pats'] = pats'"
                by simp

              from ‹(pats, cs) |∈| ?grp› obtain pats⇩e rhs⇩e
                where "(pats⇩e, rhs⇩e) |∈| rs⇩1" "pats = butlast pats⇩e"
                by (auto elim: fgroup_byE2)

              have "patterns_compatible (butlast pats') pats"
                unfolding ‹pats = _›
                apply (rule rev_accum_rel_butlast)
                using ‹(pats', rhs) |∈| rs⇩1› ‹(pats⇩e, rhs⇩e) |∈| rs⇩1› ‹(name, rs⇩1) |∈| rs› inner
                by (blast dest: fpairwiseD)

              interpret irules': irules C_info "transform_irule_set rs" by (rule rules_transform)

              have "butlast pats' = pats" "env = env⇩1"
                 apply (rule matchs_compatible_eq)
                subgoal by fact
                subgoal
                  apply (rule linears_butlastI)
                  using ‹(pats', rhs) |∈| rs⇩1› ‹(name, rs⇩1) |∈| rs› inner by auto
                subgoal
                  using ‹(pats, _) |∈| rs⇩2› ‹(name, rs⇩2) |∈| transform_irule_set rs›
                  using irules'.inner by auto
                  apply fact+
                subgoal
                  apply (rule matchs_compatible_eq)
                      apply fact
                     apply (rule linears_butlastI)
                  using ‹(pats', rhs) |∈| rs⇩1› ‹(name, rs⇩1) |∈| rs› inner
                  apply auto []
                  using ‹(pats, _) |∈| rs⇩2› ‹(name, rs⇩2) |∈| transform_irule_set rs›
                  using irules'.inner apply auto[]
                  by fact+
                done

              let ?rhs_subst = "λenv. subst rhs (fmdrop_fset (frees pat) env)"

              have "fmdom env⇩2 = freess pats"
                using ‹match (_ $$ _) _ = Some env⇩2›
                by (simp add: match_dom)

              show "fBex cs' (rel_prod (=) prelated (pat, rhs'))"
                unfolding ‹rhs' = _›
                proof (rule fBexI, rule rel_prod.intros)
                  have "fdisjnt (freess (butlast pats')) (frees (last pats'))"
                    apply (subst freess_single[symmetric])
                    apply (rule linears_appendD)
                    apply (subst ‹butlast pats' @ [last pats'] = pats'›)
                    using ‹(pats', rhs) |∈| rs⇩1› ‹(name, rs⇩1) |∈| rs› inner
                    by auto

                  show "subst rhs env ≈⇩p ?rhs_subst env⇩2"
                    apply (rule prelated_subst)
                     apply (rule prelated_refl)
                    unfolding fmfilter_alt_defs
                    apply (subst fmfilter_true)
                    subgoal premises prems for x y
                      using fmdomI[OF prems]
                      unfolding ‹pat = _› ‹fmdom env⇩2 = _›
                      apply (subst (asm) ‹butlast pats' = pats›[symmetric])
                      using ‹fdisjnt (freess (butlast pats')) (frees (last pats'))›
                      by (auto simp: fdisjnt_alt_def)
                    subgoal
                      unfolding ‹env = _›
                      by fact
                    done
                next
                  have "(pat, rhs) |∈| cs"
                    unfolding ‹pat = _›
                    apply (rule fgroup_byD[where a = "(x, y)" for x y])
                      apply fact
                     apply simp
                     apply (intro conjI)
                       apply fact
                      apply (rule refl)+
                    apply fact
                    done
                  thus "(pat, ?rhs_subst env⇩2) |∈| cs'"
                    unfolding ‹cs' = _› by force
                qed simp
            next
              fix pat rhs'
              assume "(pat, rhs') |∈| cs'"
              then obtain rhs
                where "(pat, rhs) |∈| cs"
                  and "rhs' = subst rhs (fmdrop_fset (frees pat) env⇩2 )"
                unfolding ‹cs' = _› by auto
              with ‹(pats, cs) |∈| ?grp› obtain pats'
                where "(pats', rhs) |∈| rs⇩1" "pats = butlast pats'" "pat = last pats'"
                by auto
              with False have "length pats' ≠ 0"
                using ‹arity_compatibles _› by (metis arity_compatible_length)
              hence "pats' = pats @ [pat]"
                unfolding ‹pats = _› ‹pat = _› by auto
              moreover have "linears pats'"
                using ‹(pats', rhs) |∈| rs⇩1› ‹(name, rs⇩1) |∈| _› inner by auto
              ultimately have "fdisjnt (fmdom env⇩1) (frees pat)"
                unfolding ‹fmdom env⇩1 = _›
                by (auto dest: linears_appendD)

              let ?rhs_subst = "λenv. subst rhs (fmdrop_fset (frees pat) env)"

              show "fBex (irules_deferred_matches args⇩1 rs⇩1) (λe. rel_prod (=) prelated e (pat, rhs'))"
                unfolding ‹rhs' = _›
                proof (rule fBexI, rule rel_prod.intros)
                  show "?rhs_subst env⇩1 ≈⇩p ?rhs_subst env⇩2"
                    using ‹prelated.P_env env⇩1 env⇩2› inner
                    by (auto intro: prelated_subst)
                next
                  have "matchs (butlast pats') args⇩1 = Some env⇩1"
                    using ‹matchs pats args⇩1 = _› ‹pats = _› by simp
                  moreover have "subst rhs env⇩1 = ?rhs_subst env⇩1"
                    apply (rule arg_cong[where f = "subst rhs"])
                    unfolding fmfilter_alt_defs
                    apply (rule fmfilter_true[symmetric])
                    using ‹fdisjnt (fmdom env⇩1) _›
                    by (auto simp: fdisjnt_alt_def intro: fmdomI)
                  ultimately show "(pat, ?rhs_subst env⇩1) |∈| irules_deferred_matches args⇩1 rs⇩1"
                    using ‹(pats', rhs) |∈| rs⇩1› ‹pat = last pats'›
                    by auto
                qed simp
            qed
        qed
    qed
next
  case ("fun" v v' u)
  obtain w x where "t = w $⇩p x" "w ≈⇩p v" "x ≈⇩p u" "closed w"
    using ‹t ≈⇩p v $⇩p u› ‹closed t› by cases (auto simp: closed_except_def)
  with "fun" obtain w' where "rs ⊢⇩i w ⟶* w'" "w' ≈⇩p v'"
    by blast

  show ?case
    proof (rule fun.prems)
      show "rs ⊢⇩i t ⟶* w' $⇩p x"
        unfolding ‹t = _›
        by (intro irewrite.rt_comb[unfolded app_pterm_def] rtranclp.rtrancl_refl) fact
    next
      show "w' $⇩p x ≈⇩p v' $⇩p u"
        by (rule prelated.app) fact+
    qed
next
  case (arg u u' v)
  obtain w x where "t = w $⇩p x" "w ≈⇩p v" "x ≈⇩p u" "closed x"
    using ‹t ≈⇩p v $⇩p u› ‹closed t› by cases (auto simp: closed_except_def)
  with arg obtain x' where "rs ⊢⇩i x ⟶* x'" "x' ≈⇩p u'"
    by blast

  show ?case
    proof (rule arg.prems)
      show "rs ⊢⇩i t ⟶* w $⇩p x'"
        unfolding ‹t = w $⇩p x›
        by (intro irewrite.rt_comb[unfolded app_pterm_def] rtranclp.rtrancl_refl) fact
    next
      show "w $⇩p x' ≈⇩p v $⇩p u'"
        by (rule prelated.app) fact+
    qed
qed

end

subsubsection ‹Completeness of transformation›

lemma (in irules) transform_completeness:
  assumes "rs ⊢⇩i t ⟶ t'" "closed t"
  shows "transform_irule_set rs ⊢⇩i t ⟶* t'"
using assms proof induction
  case (step name irs' pats' rhs' t t')
  then obtain irs where "irs = transform_irules irs'" "(name, irs) |∈| transform_irule_set rs"
    unfolding transform_irule_set_def
    by (metis fimageI id_apply map_prod_simp)
  show ?case
  proof (cases "arity irs' = 0")
    case True
    hence "irs = irs'"
      unfolding ‹irs = _›
      unfolding transform_irules_def
      by simp
    with step have "(pats', rhs') |∈| irs" "name, pats', rhs' ⊢⇩i t → t'"
      by blast+
    have "transform_irule_set rs ⊢⇩i t ⟶* t'"
      apply (rule r_into_rtranclp)
      apply rule
      by fact+

    show ?thesis by fact
  next
    let ?f = "λ(pats, rhs). (butlast pats, last pats, rhs)"
    let ?grp = "fgroup_by ?f irs'"
    note closed_except_def [simp add]
    case False
    then have "irs = map_prod id Pabs |`| ?grp"
      unfolding ‹irs = _›
      unfolding transform_irules_def
      by simp
    with False have "irs = transform_irules irs'"
      unfolding transform_irules_def
      by simp
    obtain pat pats where "pat = last pats'" "pats = butlast pats'"
      by blast
    from step False have "length pats' ≠ 0"
      using arity_compatible_length inner
      by (smt (verit, ccfv_threshold) case_prodD)
    then have "pats' = pats @ [pat]"
      unfolding ‹pat = _› ‹pats = _›
      by simp
    from step have "linears pats'"
      using inner by auto
    then have "fdisjnt (freess pats) (frees pat)"
      unfolding ‹pats' = _›
      using linears_appendD(3) freess_single
      by force

    from step obtain cs where "(pats, cs) |∈| ?grp"
      unfolding ‹pats = _›
      by (metis (no_types, lifting) fgroup_by_complete fst_conv prod.simps(2))
    with step have "(pat, rhs') |∈| cs"
      unfolding ‹pat = _› ‹pats = _›
      by (meson fgroup_byD old.prod.case)
    have "(pats, Pabs cs) |∈| irs"
      using ‹irs = map_prod id Pabs |`| ?grp› ‹(pats, cs) |∈| _›
      by (metis (no_types, lifting) eq_snd_iff fst_conv fst_map_prod id_def rev_fimage_eqI snd_map_prod)
    from step obtain env' where "match (name $$ pats') t = Some env'" "subst rhs' env' = t'"
      using irewrite_step_def by auto
    have "name $$ pats' = (name $$ pats) $ pat"
      unfolding ‹pats' = _›
      by (simp add: app_term_def)
    then obtain t⇩0 t⇩1 env⇩0 env⇩1 where "t = t⇩0 $⇩p t⇩1" "match (name $$ pats) t⇩0 = Some env⇩0" "match pat t⇩1 = Some env⇩1" "env' = env⇩0 ++⇩f env⇩1"
      using match_appE_split[OF ‹match (name $$ pats') _ = _›[unfolded ‹name $$ pats' = _›], unfolded app_pterm_def]
      by blast
    with step have "closed t⇩0" "closed t⇩1"
      by auto
    then have "closed_env env⇩0" "closed_env env⇩1"
      using match_vars[OF ‹match _ t⇩0 = _›] match_vars[OF ‹match _ t⇩1 = _›]
      unfolding closed_except_def
      by auto
    obtain t⇩0' where "subst (Pabs cs) env⇩0 = t⇩0'"
      by blast
    then obtain cs' where "t⇩0' = Pabs cs'" "cs' = ((λ(pat, rhs). (pat, subst rhs (fmdrop_fset (frees pat) env⇩0))) |`| cs)"
      using subst_pterm.simps(3) by blast
    obtain rhs where "subst rhs' (fmdrop_fset (frees pat) env⇩0) = rhs"
      by blast
    then have "(pat, rhs) |∈| cs'"
      unfolding ‹cs' = _›
      using ‹_ |∈| cs›
      by (metis (mono_tags, lifting) old.prod.case rev_fimage_eqI)
    have "env⇩0 ++⇩f env⇩1 = (fmdrop_fset (frees pat) env⇩0) ++⇩f env⇩1"
      apply (subst fmadd_drop_left_dom[symmetric])
      using ‹match pat _ = _› match_dom
      by metis
    have "fdisjnt (fmdom env⇩0) (fmdom env⇩1)"
      using match_dom
      using ‹match pat _ = _› ‹match (name $$ pats) _ = _›
      using ‹fdisjnt _ _›
      unfolding fdisjnt_alt_def
      by (metis matchs_dom match_list_combE)
    have "subst rhs env⇩1 = t'"
      unfolding ‹_ = rhs›[symmetric]
      unfolding ‹_ = t'›[symmetric]
      unfolding ‹env' = _›
      unfolding ‹env⇩0 ++⇩f _ = _›
      apply (subst subst_indep')
      using ‹closed_env env⇩0›
        apply blast
      using ‹fdisjnt (fmdom _) _›
      unfolding fdisjnt_alt_def
      by auto

    show ?thesis
      unfolding ‹t = _›
      apply rule
       apply (rule r_into_rtranclp)
       apply (rule irewrite.intros(3))
       apply rule
         apply fact+
       apply (rule irewrite_stepI)
        apply fact+
      unfolding ‹t⇩0' = _›
      apply rule
       apply fact
      using ‹match pat t⇩1 = _› ‹subst rhs _ = _›
      by force
  qed
qed (auto intro: irewrite.rt_comb[unfolded app_pterm_def] intro!: irewrite.intros simp: closed_except_def)


subsubsection ‹Computability›

export_code
  compile transform_irules
  checking Scala SML

end