Theory AC_Equivalence (Isabelle2017: October 2017)

(*
Author:  Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at> (2015)
Author:  Christian Sternagel <c.sternagel@gmail.com> (2015)
License: LGPL (see file COPYING.LESSER)
*)

chapter ‹AC-Equivalence›

theory AC_Equivalence
imports 
  "Check-NT.AC_Rewriting_Base"
begin

section ‹Associativity›

subsection ‹Abstract A-normal forms›

(* A-algebra 'a (or a subtype thereof) + homomorphism from T_'f('v) *)
locale abstract_anf =
  fixes nf :: "('f, 'v) term ⇒ 'a" -- ‹compute A-normal form›
    and A :: "'f set" -- ‹associative function symbols›
  assumes nf_assoc [simp]: "f ∈ A ⟹ nf (Bin f (Bin f s t) u) = nf (Bin f s (Bin f t u))"
    and nf_FunI [intro]: "map nf ss = map nf ts ⟹ nf (Fun f ss) = nf (Fun f ts)"
begin

lemma nf_BinI:
  "nf s = nf s' ⟹ nf t = nf t' ⟹ nf (Bin f s t) = nf (Bin f s' t')"
by (auto)

lemma nf_eq_ctxt:
  "nf s = nf t ⟹ nf (C⟨s⟩) = nf (C⟨t⟩)"
by (induct C) auto

end

lemma A_class_eq_conv [simp]:
  "A_class A s = A_class A t ⟷ (s, t) ∈ (astep A)⇧^↔⇧^*"
by (auto simp: A_class_def) (metis conversion_def conversion_inv rtrancl_trans)+

interpretation A_class_abstract_anf: abstract_anf where nf = "A_class A"
by (unfold_locales) (auto simp: map_eq_conv' args_aconv_imp_aconv)

subsection ‹Algebraic version of A-normal forms (executable)›

text ‹Smart constructor for associative function symbols.›
fun aBin :: "'f ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f, 'v) term"
where
  "aBin f (Bin g s t) u = (if f = g then Bin f s (aBin f t u) else Bin f (Bin g s t) u)"
| "aBin f s t = Bin f s t"

context
  fixes A :: "'f set"
begin

function anf :: "('f, 'v) term ⇒ ('f, 'v) term"
where
  "anf (Var x) = Var x"
| "anf (Bin f s t) = (if f ∈ A then aBin f (anf s) (anf t) else Bin f (anf s) (anf t))"
| "⋀f ts. ∀u v. ts ≠ [u, v] ⟹ anf (Fun f ts) = Fun f (map anf ts)"
by (auto, atomize_elim, insert Bin_cases, auto)
termination by (lexicographic_order)

function is_anf :: "('f, 'v) term ⇒ bool"
where
  "is_anf (Var x) ⟷ True"
| "is_anf (Bin f s t) ⟷ is_anf s ∧ is_anf t ∧ (f ∈ A ⟶ (∀u v. s ≠ Bin f u v))"
| "⋀f ts. ∀u v. ts ≠ [u, v] ⟹ is_anf (Fun f ts) ⟷ (∀t ∈ set ts. is_anf t)"
by (auto, atomize_elim, insert Bin_cases, auto)
termination by (lexicographic_order)

lemma anf_code [code]:
  "anf (Var x) = Var x"
  "anf (Bin f s t) = (if f ∈ A then aBin f (anf s) (anf t) else Bin f (anf s) (anf t))"
  "anf (Fun f []) = Fun f []"
  "anf (Fun f [t]) = Fun f [anf t]"
  "anf (Fun f (s # t # u # us)) = Fun f (anf s # anf t # anf u # map anf us)"
by simp_all

end

lemma aBin_assoc [simp]:
  "aBin f (aBin f s t) u = aBin f s (aBin f t u)"
by (induct f s t rule: aBin.induct) simp_all

lemma is_anf_aBin [intro]:
  "is_anf A s ⟹ is_anf A t ⟹ is_anf A (aBin f s t)"
by (induct f s t rule: aBin.induct) auto

lemma is_anf_anf [intro]: "is_anf A (anf A t)"
proof (induct t rule: anf.induct [of _ A])
  case (3 f ts)
  then show ?case using Bin_cases[of "Fun f (map (anf A) ts)"] by auto
qed auto

interpretation anf_abstract_anf: abstract_anf where nf = "anf A"
proof (unfold_locales)
  fix f and ss ts :: "('a, 'b) term  list"
  assume "map (anf A) ss = map (anf A) ts"
  then show "anf A (Fun f ss) = anf A (Fun f ts)"
    using Bin_cases[of "Fun f ss"] Bin_cases[of "Fun f ts"] by force
qed auto

subsection ‹Relate abstract A-normal forms to @{const anf} and @{const A_class}›

context abstract_anf
begin

text ‹A-rewriting preserves abstract normal forms.›

lemma astep_imp_nf_eq:
  "(s, t) ∈ astep A ⟹ nf s = nf t"
by (force intro: nf_eq_ctxt simp: A_rules_def)

(* A_class s = A_class t ⟹ nf s = nf t *)
lemma aconv_imp_nf_eq:
  "(s, t) ∈ (astep A)⇧^↔⇧^* ⟹ nf s = nf t"
unfolding conversion_def
by (induct rule: rtrancl_induct) (auto simp: astep_imp_nf_eq simp del: reverseTrs)

text ‹The normalization function @{const anf} preserves abstract normal forms.›

lemma nf_aBin [simp]:
  "f ∈ A ⟹ nf (aBin f s t) = nf (Bin f s t)"
by (induct f s t rule: aBin.induct) force+

(* anf A t = anf A s ==> nf t = nf s   +   anf A (anf A t) = anf A t *)
lemma nf_anf: "nf (anf A t) = nf t"
by (induct t rule: anf.induct [of _ A]) force+

end


subsection ‹The main result for associativity›

(* A_class s = A_class t <--> anf A s = anf A t *)
lemma aconv_iff [code_unfold]:
  "(s, t) ∈ (astep A)⇧^↔⇧^* ⟷ anf A s = anf A t"
proof
  assume "anf A s = anf A t"
  then have "A_class A (anf A s) = A_class A (anf A t)" by simp
  then show "(s, t) ∈ (astep A)⇧^↔⇧^*"
    by (simp add: A_class_abstract_anf.nf_anf)
qed (simp add: anf_abstract_anf.aconv_imp_nf_eq)


section ‹Associativity and commutativity›

subsection ‹Abstract AC-normal forms›

text ‹All function symbols are either associative and commutative, or neither.›
locale abstract_acnf =
  abstract_anf +
  assumes nf_commute [simp]: "f ∈ A ⟹ nf (Bin f s t) = nf (Bin f t s)"
begin

lemma nf_left_commute [simp]:
  "f ∈ A ⟹ nf (Bin f s (Bin f t u)) = nf (Bin f t (Bin f s u))"
by (auto simp only: nf_assoc [symmetric] nf_BinI [OF nf_commute [of f s]])

end

lemma AC_class_eq_conv [simp]:
  "AC_class A C s = AC_class A C t ⟷ (s, t) ∈ (acstep A C)⇧^↔⇧^*"
by (auto simp: AC_class_def) (metis conversion_def conversion_inv rtrancl_trans)+

interpretation AC_class_abstract_acnf: abstract_acnf where nf = "AC_class A A"
by (unfold_locales) (auto simp: map_eq_conv' args_acconv_imp_acconv)


subsection ‹Algebraic version of AC-normal forms (executable)›

datatype ('f, 'v) acterm =
  AVar 'v
| AFun 'f "('f, 'v) acterm list"
| AAC 'f "('f, 'v) acterm multiset"

abbreviation (input) "ABin f s t ≡ AFun f [s, t]"

fun actop :: "'f ⇒ ('f, 'v) term ⇒ ('f, 'v) term multiset"
where
  "actop f (Bin g s t) = (if f = g then actop f s + actop f t else {# Bin g s t #})"
| "actop f t = {# t #}"

lemma actop_non_Bin [simp]:
  "∀u v. ts ≠ [u, v] ⟹ actop h (Fun f ts) = {# Fun f ts #}"
by (induct f "Fun f ts" rule: actop.induct) auto

lemma Melem_actop_size [termination_simp]:
  "s ∈# actop f t ⟹ size s < Suc (size t + q)"
  "s ∈# actop f t ⟹ size s < Suc (q + size t)"
by (induct f t rule: actop.induct) (auto split: if_splits)

context
  fixes A :: "'f set"
begin

function acnf :: "('f, 'v) term ⇒ ('f, 'v) acterm"
where
  "acnf (Var x) = AVar x"
| "acnf (Bin f s t) =
    (if f ∈ A then AAC f (image_mset acnf (actop f (Bin f s t)))
    else ABin f (acnf s) (acnf t))"
| "⋀f ts. ∀u v. ts ≠ [u, v] ⟹ acnf (Fun f ts) = AFun f (map acnf ts)"
by (auto, atomize_elim, insert Bin_cases, auto)
termination by (lexicographic_order)

function acnf_schema :: "('f, 'v) term ⇒ ('f, 'v) acterm"
where
  "acnf_schema (Var v) = AVar v"
| "acnf_schema (Bin f s t) =
    (if f ∈ A then AAC f (image_mset acnf_schema (actop f (Fun f [s, t])) + {# acnf_schema t #})
    else ABin f (acnf_schema s) (acnf_schema t))"
| "⋀f ts. ∀u v. ts ≠ [u, v] ⟹ acnf_schema (Fun f ts) = AFun f (map acnf_schema ts)"
by (auto, atomize_elim, insert Bin_cases, auto)
termination by (lexicographic_order)

lemma acnf_code [code]:
  "acnf (Var x) = AVar x"
  "acnf (Bin f s t) =
    (if f ∈ A then AAC f (image_mset acnf (actop f (Bin f s t)))
    else ABin f (acnf s) (acnf t))"
  "acnf (Fun f []) = AFun f []"
  "acnf (Fun f [t]) = AFun f [acnf t]"
  "acnf (Fun f (s # t # u # us)) = AFun f (acnf s # acnf t # acnf u # map acnf us)"
by simp_all

end

lemma image_mset_acnf_actop:
  assumes "f ∈ A" and "acnf A s = acnf A t"
  shows "image_mset (acnf A) (actop f s) = image_mset (acnf A) (actop f t)"
using assms by (cases s rule: acnf.cases; cases t rule: acnf.cases) (auto split: if_splits)

interpretation acnf_abstract_acnf: abstract_acnf where nf = "acnf A"
proof (unfold_locales)
  fix f and ss ts :: "('a, 'b) term list"
  assume "map (acnf A) ss = map (acnf A) ts"
  then show "acnf A (Fun f ss) = acnf A (Fun f ts)"
    using Bin_cases[of "Fun f ss"] Bin_cases[of "Fun f ts"]
    by auto (auto intro: arg_cong2[of _ _ _ _ "op +"] image_mset_acnf_actop)
qed (auto simp: ac_simps)


subsection ‹Relate abstract AC-normal forms to @{const acnf} and @{const AC_class}›

lemma actop_singleton [simp]:
  "(⋀u v. s ≠ Bin g u v) ⟹ actop g s = {# s #}"
by (cases "(g, s)" rule: actop.cases) auto

lemma non_empty_plus_non_empty_not_single:
  assumes "a ≠ {#}" "b ≠ {#}" shows "a + b ≠ {# x #}"
using assms by (simp add: union_is_single)

lemma image_actop_nonempty:
  "image_mset h (actop f t) ≠ {#}"
by (induct f t rule: actop.induct) auto

lemmas image_actop_plus_image_actop_not_single =
  non_empty_plus_non_empty_not_single [OF image_actop_nonempty image_actop_nonempty]
  non_empty_plus_non_empty_not_single [OF image_actop_nonempty image_actop_nonempty, symmetric]

fun del_actop :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f, 'v) term"
where
  "del_actop s' (Bin f s t) =
    (if s = s' then t else if t = s' then s else Bin f s (del_actop s' t))"

lemma trivial_Bin_facts [simp]:
  "s ≠ Bin f s t" "s ≠ Bin f t s" "Bin f s t ≠ s" "Bin f t s ≠ s" "¬ Bin f u v ∈# actop f s"
proof (induct s)
  fix g ts
  assume "(⋀t. t ∈ set ts ⟹ ¬ Fun f [u, v] ∈# actop f t)"
  then show "¬ Bin f u v ∈# actop f (Fun g ts)"
    using Bin_cases[of "Fun g ts"] by (auto split: if_splits)
qed (auto, (metis list.set_intros)+)

lemma is_anf_actops:
  assumes "is_anf A t" and "s ∈# actop f t"
  shows "is_anf A s" and "∀u v. Bin f u v ≠ s"
using assms by (induct t rule: is_anf.induct) (auto split: if_splits)

context abstract_acnf
begin

text ‹AC-rewriting preserves abstract normal forms.›

lemma acstep_imp_nf_eq:
  "(s, t) ∈ acstep A A ⟹ nf s = nf t"
by (force intro: nf_eq_ctxt simp: AC_rules_def A_rules_def C_rules_def)

(* AC_class s = AC_class t ==> nf s = nf t *)
lemma acconv_imp_nf_eq:
  "(s, t) ∈ (acstep A A)⇧^↔⇧^* ⟹ nf s = nf t"
unfolding conversion_def
by (induct rule: rtrancl_induct) (auto simp: acstep_imp_nf_eq simp del: reverseTrs)

text ‹Terms with the same @{const acnf} have the same abstract normal form. This is the hard part.›

lemma acnf_eq_intro:
  assumes "f ∈ A" and "image_mset (acnf A) (actop f s) = image_mset (acnf A) (actop f t)"
  shows "acnf A s = acnf A t"
using assms
by (cases s rule: acnf.cases; cases t rule: acnf.cases)
   (auto split: if_splits simp: image_actop_plus_image_actop_not_single)

lemma shuffle_actop:
  assumes "f ∈ A" and "is_anf A (Bin f s t)" and "s' ∈# actop f (Bin f s t)"
  shows "nf (Bin f s t) = nf (Bin f s' (del_actop s' (Bin f s t))) ∧
    is_anf A (Bin f s' (del_actop s' (Bin f s t)))"
using assms
proof (induct t arbitrary: s rule: bterm_induct)
  case (Bin g t u s)
  show ?case using Bin(3-5) nf_commute Bin(2)[of t]
    by (auto split: if_splits simp del: nf_commute)
       (subst (2) nf_left_commute, simp, metis nf_BinI)+
qed (auto split: if_splits)

lemma acnf_eq_imp_nf_eq':
  "is_anf A s ⟹ is_anf A u ⟹ acnf A s = acnf A u ⟹ nf s = nf u"
proof (induct s arbitrary: u rule: acnf_schema.induct [of _ A, case_names Var Bin Fun])
  case (Var v u) thus ?case by (cases u rule: is_anf.cases) (auto split: if_splits)
next
  case (Fun f ts u)
  then obtain g us where [simp]: "u = Fun g us" by (cases u) (auto split: if_splits)
  have "length ts = length us"
    using Fun by (cases "∀u v. us ≠ [u, v]") (auto dest: map_eq_imp_length_eq split: if_splits)
  thus ?case using Fun
    by (cases "∀u v. us ≠ [u, v]")
       (auto intro!: nth_equalityI nf_BinI dest!: map_nth_conv split: if_splits)
next
  case (Bin f s t u)
  obtain v w where u[simp]: "u = Bin f v w" using Bin(5-7) by (cases u rule: is_anf.cases) (auto split: if_splits)
  show ?case
  proof (cases "f ∈ A")
    case False thus ?thesis using Bin(3-7)
      by (cases u rule: is_anf.cases)
         (auto simp only: acnf.simps is_anf.simps split: if_splits intro: nf_BinI, force+)
  next
    case [simp]: True
    have s: "actop f s = {# s #}" "s ∈# actop f (Bin f s t)"
      using Bin(5) by (auto split: if_splits)
    obtain s' where s': "s' ∈# actop f u" "acnf A s = acnf A s'"
      using s(2) arg_cong[OF image_mset_acnf_actop[OF True Bin(7)], of "set_mset"]
      by auto blast+
    hence 0: "nf (Bin f s t) = nf (Bin f s' t)" and *: "⋀u v. s' ≠ Bin f u v"
      using is_anf_actops[of A u s' f] Bin(1)[of s s'] Bin(5,6) by auto
    def t' ≡ "del_actop s' u"
    have 1: "nf (Bin f s' t') = nf u" and t': "acnf A (Bin f s' t') = acnf A u" "is_anf A (Bin f s' t')"
      using Bin(6) s' shuffle_actop[of f v w s'] acnf_abstract_acnf.shuffle_actop[of f A v w s']
      by (auto simp: t'_def)
    have "acnf A t = acnf A t'" using Bin(7) s'(2) *
      by (auto intro: acnf_eq_intro[of f] simp: s(1) t'(1)[symmetric] simp del: u)
    hence 2: "nf (Bin f s' t) = nf (Bin f s' t')"
      using Bin(5) t'(2) by (fastforce intro: Bin(2) nf_BinI split: if_splits)
    show ?thesis by (simp add: 0 1 2)
  qed
qed

(* acnf A s = acnf A t ==> nf s = nf t *)
lemma acnf_eq_imp_nf_eq: "acnf A s = acnf A t ⟹ nf s = nf t"
using acnf_eq_imp_nf_eq' [of "anf A s" "anf A t"] by (auto simp: nf_anf acnf_abstract_acnf.nf_anf)

end


subsection ‹The main result for associativity and commutativity›

(* AC_class s = AC_classt <--> acnf A s = acnf A t *)
lemma acconv_iff [code_unfold]:
  "(s, t) ∈ (acstep A A)⇧^↔⇧^* ⟷ acnf A s = acnf A t"
by (auto dest: AC_class_abstract_acnf.acnf_eq_imp_nf_eq intro: acnf_abstract_acnf.acconv_imp_nf_eq)


section ‹A ∨ C - Symbols›

locale abstract_cnf =
  fixes nf :: "('f, 'v) term ⇒ 'a" -- ‹compute C-normal form›
    and F⇩_C :: "'f set" -- ‹commutative function symbols›
  assumes nf_commute [simp]: "f ∈ F⇩_C ⟹ nf (Bin f s t) = nf (Bin f t s)"
    and nf_FunI [intro]: "map nf ss = map nf ts ⟹ nf (Fun f ss) = nf (Fun f ts)"
begin

lemma nf_BinI:
  "nf s = nf s' ⟹ nf t = nf t' ⟹ nf (Bin f s t) = nf (Bin f s' t')"
by (auto)

lemma nf_eq_ctxt:
  "nf s = nf t ⟹ nf (C⟨s⟩) = nf (C⟨t⟩)"
by (induct C) auto

end

lemma C_class_eq_conv [simp]:
  "C_class C s = C_class C t ⟷ (s, t) ∈ (cstep C)⇧^↔⇧^*"
by (auto simp: C_class_def) (metis conversion_def conversion_inv rtrancl_trans)+

interpretation C_class_abstract_cnf: abstract_cnf where nf = "C_class F⇩_C"
by (unfold_locales) (auto simp: map_eq_conv' args_cconv_imp_cconv)

context
  fixes F⇩_C :: "'f set"
begin

function cnf :: "('f, 'v) term ⇒ ('f, 'v) acterm"
where
  "cnf (Var x) = AVar x"
| "cnf (Bin f s t) = (if f ∈ F⇩_C then AAC f {#cnf s, cnf t#} else ABin f (cnf s) (cnf t))"
| "⋀f ts. ∀u v. ts ≠ [u, v] ⟹ cnf (Fun f ts) = AFun f (map cnf ts)"
by (auto, atomize_elim, insert Bin_cases, auto)
termination by (lexicographic_order)

lemma cnf_code [code]:
  "cnf (Var x) = AVar x"
  "cnf (Bin f s t) =
    (let s' = cnf s; t' = cnf t in if f ∈ F⇩_C then AAC f {#s', t'#} else ABin f s' t')"
  "cnf (Fun f []) = AFun f []"
  "cnf (Fun f [t]) = AFun f [cnf t]"
  "cnf (Fun f (s # t # u # us)) = AFun f (cnf s # cnf t # cnf u # map cnf us)"
by (simp_all add: Let_def)

end

interpretation cnf_abstract_cnf: abstract_cnf where nf = "cnf F⇩_C"
proof (unfold_locales)
  fix f and ss ts :: "('a, 'b) term  list"
  assume "map (cnf F⇩_C) ss = map (cnf F⇩_C) ts"
  then show "cnf F⇩_C (Fun f ss) = cnf F⇩_C (Fun f ts)"
    using Bin_cases [of "Fun f ss"] Bin_cases [of "Fun f ts"] by auto
qed auto

context abstract_cnf
begin

lemma cstep_imp_nf_eq:
  "(s, t) ∈ cstep F⇩_C ⟹ nf s = nf t"
by (force intro: nf_eq_ctxt simp: C_rules_def)

lemma cconv_imp_nf_eq:
  "(s, t) ∈ (cstep F⇩_C)⇧^↔⇧^* ⟹ nf s = nf t"
unfolding conversion_def
by (induct rule: rtrancl_induct) (auto simp: cstep_imp_nf_eq simp del: reverseTrs)

end

locale abstract_aocnf =
  anf: abstract_anf nf F⇩_A +
  cnf: abstract_cnf nf F⇩_C
  for nf :: "('f, 'v) term ⇒ 'a" and F⇩_A F⇩_C
begin

abbreviation (input) "AC ≡ F⇩_A ∩ F⇩_C"

lemma nf_left_commute [simp]:
  "f ∈ AC ⟹ nf (Bin f s (Bin f t u)) = nf (Bin f t (Bin f s u))"
by (auto simp only: anf.nf_assoc [symmetric] anf.nf_BinI [OF cnf.nf_commute [of f s]])

end

interpretation AC_class_abstract_aocnf: abstract_aocnf where nf = "AC_class F⇩_A F⇩_C"
by (unfold_locales) (auto simp: map_eq_conv' args_acconv_imp_acconv)

text ‹Smart constructor for associative function symbols.›
fun aABin :: "'f ⇒ ('f, 'v) acterm ⇒ ('f, 'v) acterm ⇒ ('f, 'v) acterm"
where
  "aABin f (ABin g s t) u = (if f = g then ABin f s (aABin f t u) else ABin f (ABin g s t) u)"
| "aABin f s t = ABin f s t"

lemma aABin_simps [simp]:
  "∀u v. s ≠ AFun f [u, v] ⟹ aABin f s t = ABin f s t"
by (induct f s t rule: aABin.induct) auto

lemma aABin_assoc [simp]:
  "aABin f (aABin f s t) u = aABin f s (aABin f t u)"
by (induct f s t rule: aABin.induct) simp_all

lemma aABin_neq_AAC [simp]:
  "aABin f s t ≠ AAC g T"
  "AAC g T ≠ aABin f s t"
  "aABin f s t ≠ AVar x"
  "AVar x ≠ aABin f s t"
  "∀u v. ts ≠ [u, v] ⟹ aABin f s t ≠ AFun h ts"
  "∀u v. ts ≠ [u, v] ⟹ AFun h ts ≠ aABin f s t"
by (induct f s t rule: aABin.induct) auto

context
  fixes F⇩_A F⇩_C :: "'f set"
begin

function aocnf :: "('f, 'v) term ⇒ ('f, 'v) acterm"
where
  "aocnf (Var x) = AVar x"
| "aocnf (Bin f s t) =
    (if f ∈ F⇩_A ∩ F⇩_C then AAC f (image_mset aocnf (actop f (Bin f s t)))
    else if f ∈ F⇩_A then aABin f (aocnf s) (aocnf t)
    else if f ∈ F⇩_C then AAC f {#aocnf s, aocnf t#}
    else ABin f (aocnf s) (aocnf t))"
| "⋀f ts. ∀u v. ts ≠ [u, v] ⟹ aocnf (Fun f ts) = AFun f (map aocnf ts)"
by (auto, atomize_elim, insert Bin_cases, auto)
termination by (lexicographic_order)

function aocnf_schema :: "('f, 'v) term ⇒ ('f, 'v) acterm"
where
  "aocnf_schema (Var v) = AVar v"
| "aocnf_schema (Bin f s t) =
    (if f ∈ F⇩_A ∩ F⇩_C then
      AAC f (image_mset aocnf_schema (actop f (Fun f [s, t])) + {# aocnf_schema t #})
    else ABin f (aocnf_schema s) (aocnf_schema t))"
| "⋀f ts. ∀u v. ts ≠ [u, v] ⟹ aocnf_schema (Fun f ts) = AFun f (map aocnf_schema ts)"
by (auto, atomize_elim, insert Bin_cases, auto)
termination by (lexicographic_order)

lemma aocnf_code [code]:
  "aocnf (Var x) = AVar x"
  "aocnf (Bin f s t) = (let A = f ∈ F⇩_A; C = f ∈ F⇩_C in
    (if A ∧ C then AAC f (image_mset aocnf (actop f (Bin f s t)))
    else if A then aABin f (aocnf s) (aocnf t)
    else if C then AAC f {#aocnf s, aocnf t#}
    else ABin f (aocnf s) (aocnf t)))"
  "aocnf (Fun f []) = AFun f []"
  "aocnf (Fun f [t]) = AFun f [aocnf t]"
  "aocnf (Fun f (s # t # u # us)) = AFun f (aocnf s # aocnf t # aocnf u # map aocnf us)"
by simp_all

end

lemma image_mset_aocnf_actop:
  assumes "f ∈ A ∩ C" and "aocnf A C s = aocnf A C t"
  shows "image_mset (aocnf A C) (actop f s) = image_mset (aocnf A C) (actop f t)"
using assms
by (cases s rule: aocnf.cases; cases t rule: aocnf.cases)
   (auto simp: split: if_splits elim: aABin.cases)

interpretation aocnf_abstract_aocnf: abstract_aocnf where nf = "aocnf F⇩_A F⇩_C"
proof (unfold_locales)
  fix f and ss ts :: "('a, 'b) term list"
  assume "map (aocnf F⇩_A F⇩_C) ss = map (aocnf F⇩_A F⇩_C) ts"
  then show "aocnf F⇩_A F⇩_C (Fun f ss) = aocnf F⇩_A F⇩_C (Fun f ts)"
    using Bin_cases[of "Fun f ss"] Bin_cases[of "Fun f ts"]
    by auto (auto intro: arg_cong2 [of _ _ _ _ "op +"] image_mset_aocnf_actop)
qed (auto simp: ac_simps)

context abstract_aocnf
begin

text ‹A ∨ C - rewriting preserves abstract normal forms.›

lemma acstep_imp_nf_eq:
  "(s, t) ∈ acstep F⇩_A F⇩_C ⟹ nf s = nf t"
by (force intro: anf.nf_eq_ctxt simp: AC_rules_def A_rules_def C_rules_def)

(* AC_class s = AC_class t ==> nf s = nf t *)
lemma acconv_imp_nf_eq:
  "(s, t) ∈ (acstep F⇩_A F⇩_C)⇧^↔⇧^* ⟹ nf s = nf t"
unfolding conversion_def
by (induct rule: rtrancl_induct) (auto simp: acstep_imp_nf_eq simp del: reverseTrs)

text ‹Terms with the same @{const aocnf} have the same abstract normal form. This is the hard part.›

lemma aocnf_eq_intro:
  assumes "f ∈ AC" and "image_mset (aocnf F⇩_A F⇩_C) (actop f s) = image_mset (aocnf F⇩_A F⇩_C) (actop f t)"
  shows "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C t"
using assms
by (cases s rule: aocnf.cases; cases t rule: aocnf.cases)
   (auto split: if_splits simp: image_actop_plus_image_actop_not_single)

lemma shuffle_actop:
  assumes "f ∈ AC" and "is_anf F⇩_A (Bin f s t)"
    and "s' ∈# actop f (Bin f s t)"
  shows "nf (Bin f s t) = nf (Bin f s' (del_actop s' (Bin f s t))) ∧
    is_anf F⇩_A (Bin f s' (del_actop s' (Bin f s t)))"
using assms
proof (induct t arbitrary: s rule: bterm_induct)
  case (Bin g t u s)
  show ?case
    using Bin(3-5) cnf.nf_commute [of f] Bin(2)[of t]
    by (auto split: if_splits simp del: cnf.nf_commute)
       (subst (2) nf_left_commute, simp, metis cnf.nf_BinI)+
qed (auto split: if_splits)

lemma map_not_bin: "∀u v. ts ≠ [u, v] ⟹ ∀u v. map f ts ≠ [u, v]" by auto

lemma aocnf_not_ABin: "∀u v. t ≠ Bin f u v ⟹ ∀u v. aocnf F⇩_A F⇩_C t ≠ ABin f u v"
apply (induct t rule: aocnf_schema.induct [of _ F⇩_A F⇩_C])
apply auto
apply (metis (no_types, lifting) aABin.simps(1) aABin_simps acterm.inject(2))+
done

lemma aABin_roots: "aABin f s t = aABin g u v ⟹ g = f"
apply (induct f s t arbitrary: u v rule: aABin.induct)
apply (auto split: if_splits)
apply (metis aABin.simps(1) aABin_simps acterm.inject(2))+
done

lemma aABin_AFun_roots:
  "aABin f s t = AFun g us ⟹ g = f ∧ length us = 2"
  "AFun g us = aABin f s t ⟹ g = f ∧ length us = 2"
by (induct f s t arbitrary: us rule: aABin.induct) (auto split: if_splits)

lemma aocnf_roots:
  "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C t ⟹ root s = root t"
proof (induct s arbitrary: t rule: aocnf_schema.induct [of _ F⇩_A F⇩_C])
  case (1 x)
  then show ?case using Bin_cases [of t] by (auto split: if_splits)
next
  case (2 f u v)
  then show ?case using Bin_cases [of t]
    by (auto split: if_splits dest!: aABin_roots aABin_AFun_roots)
next
  case (3 f ts)
  then show ?case
    using Bin_cases [of t] by (auto split: if_splits simp: map_not_bin dest: map_eq_imp_length_eq)
qed

lemma aocnf_Fun_roots:
  "aocnf F⇩_A F⇩_C (Fun f ss) = aocnf F⇩_A F⇩_C (Fun g ts) ⟹ g = f"
using aocnf_roots [of "Fun f ss" "Fun g ts"] by simp

lemma is_anf_Bin_aocnf_simp:
  "f ∈ F⇩_A ⟹ f ∉ F⇩_C ⟹ is_anf F⇩_A (Bin f s t) ⟹
    aocnf F⇩_A F⇩_C (Bin f s t) = ABin f (aocnf F⇩_A F⇩_C s) (aocnf F⇩_A F⇩_C t)"
by (simp add: aocnf_not_ABin)

lemma aocnf_eq_imp_nf_eq':
  assumes "is_anf F⇩_A s"
    and "is_anf F⇩_A u"
    and "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C u"
  shows "nf s = nf u"
using assms
proof (induct s arbitrary: u rule: aocnf_schema.induct [of _ F⇩_A F⇩_C, case_names Var Bin Fun])
  case (Var v u) then show ?case by (cases u rule: is_anf.cases) (auto split: if_splits)
next
  case (Fun f ts u)
  then obtain g us where [simp]: "u = Fun g us" by (cases u) (auto split: if_splits)
  have *: "∀u v. map (aocnf F⇩_A F⇩_C) ts ≠ [u, v]" using Fun by auto
  then have "length ts = length us"
    using Fun by (cases "∀u v. us ≠ [u, v]") (auto dest: map_eq_imp_length_eq split: if_splits)
  then show ?case using Fun and *
    by (cases "∀u v. us ≠ [u, v]")
       (auto intro!: nth_equalityI cnf.nf_BinI dest!: map_nth_conv split: if_splits)
next
  case (Bin f s t u)
  obtain v w where u [simp]: "u = Bin f v w"
    using Bin(5-7) by (cases u rule: is_anf.cases) (auto split: if_splits simp: aocnf_not_ABin)
  show ?case
  proof (cases "f ∈ AC")
    case False
    moreover
    { assume "f ∉ F⇩_A" and "f ∉ F⇩_C"
      then have ?thesis using Bin(3-7) by (auto intro: cnf.nf_BinI) }
    moreover
    { assume f: "f ∉ F⇩_A" "f ∈ F⇩_C"
      then have "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C v ∧ aocnf F⇩_A F⇩_C t = aocnf F⇩_A F⇩_C w ∨
        aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C w ∧ aocnf F⇩_A F⇩_C t = aocnf F⇩_A F⇩_C v"
        using Bin(7) by (auto simp: single_is_union add_eq_conv_diff)
      moreover
      { assume "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C v" and "aocnf F⇩_A F⇩_C t = aocnf F⇩_A F⇩_C w"
        then have ?thesis using Bin(3-6) and f by (auto intro: cnf.nf_BinI) }
      moreover
      { assume "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C w" and "aocnf F⇩_A F⇩_C t = aocnf F⇩_A F⇩_C v"
        then have ?thesis
        using Bin(3-6) and f
        by (subst cnf.nf_commute) (auto simp only: u is_anf.simps intro: cnf.nf_BinI) }
      ultimately have ?thesis by blast }
    moreover
    { assume "f ∈ F⇩_A" and "f ∉ F⇩_C"
      then have ?thesis
        using Bin(3-7)
        by (simp_all only: u) (unfold is_anf_Bin_aocnf_simp [of f], auto intro: cnf.nf_BinI) }
    ultimately show ?thesis using False by blast
  next
    case True
    then have s: "actop f s = {# s #}" "s ∈# actop f (Bin f s t)"
      using Bin(5) by (auto split: if_splits)
    obtain s' where s': "s' ∈# actop f u" "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C s'"
      using s(2) arg_cong[OF image_mset_aocnf_actop[OF True Bin(7)], of "set_mset"]
      by auto blast+
    hence 0: "nf (Bin f s t) = nf (Bin f s' t)" and *: "⋀u v. s' ≠ Bin f u v"
      using Bin(1) [of s s'] and Bin(5,6) and True
      by (auto split: if_splits intro: cnf.nf_BinI is_anf_actops)
    def t' ≡ "del_actop s' u"
    have 1: "nf (Bin f s' t') = nf u"
      and t': "aocnf F⇩_A F⇩_C (Bin f s' t') = aocnf F⇩_A F⇩_C u" "is_anf F⇩_A (Bin f s' t')"
      using Bin(5,6) s' shuffle_actop[of f v w s'] and True
      and aocnf_abstract_aocnf.shuffle_actop[of f F⇩_A F⇩_C v w s']
      by (auto simp: t'_def)
    have "aocnf F⇩_A F⇩_C t = aocnf F⇩_A F⇩_C t'" using Bin(7) s'(2) * and True
      by (auto intro: aocnf_eq_intro [of f] simp: s(1) t'(1) [symmetric] simp del: u split: if_splits)
    then have 2: "nf (Bin f s' t) = nf (Bin f s' t')"
      using True and Bin(2, 5,6) and shuffle_actop [OF True, of v w s'] and s'
      by (intro cnf.nf_BinI) (auto simp: t'_def)
    show ?thesis by (simp add: 0 1 2)
  qed
qed

lemma aocnf_eq_imp_nf_eq:
  "aocnf F⇩_A F⇩_C s = aocnf F⇩_A F⇩_C t ⟹ nf s = nf t"
using aocnf_eq_imp_nf_eq' [of "anf F⇩_A s" "anf F⇩_A t"]
by (auto simp: anf.nf_anf aocnf_abstract_aocnf.anf.nf_anf)

end

lemma aocconv_iff [code_unfold]:
  "(s, t) ∈ (acstep A C)⇧^↔⇧^* ⟷ aocnf A C s = aocnf A C t"
by (auto dest: AC_class_abstract_aocnf.aocnf_eq_imp_nf_eq intro: aocnf_abstract_aocnf.acconv_imp_nf_eq)

end