(* Author: Alexander Maletzky *)

section ‹Computable Term Orders›

theory Term_Order
  imports OAlist_Poly_Mapping "HOL-Library.Product_Lexorder"
begin

subsection ‹Type Class ‹nat››

class nat = zero + plus + minus + order + equal +
  fixes rep_nat :: "'a → nat"
    and abs_nat :: "nat → 'a"
  assumes rep_inverse [simp]: "abs_nat (rep_nat x) = x"
    and abs_inverse [simp]: "rep_nat (abs_nat n) = n"
    and abs_zero [simp]: "abs_nat 0 = 0"
    and abs_plus: "abs_nat m + abs_nat n = abs_nat (m + n)"
    and abs_minus: "abs_nat m - abs_nat n = abs_nat (m - n)"
    and abs_ord: "m ≤ n ==> abs_nat m ≤ abs_nat n"
begin

lemma rep_inj:
  assumes "rep_nat x = rep_nat y"
  shows "x = y"
proof -
  have "abs_nat (rep_nat x) = abs_nat (rep_nat y)" by (simp only: assms)
  thus ?thesis by (simp only: rep_inverse)
qed

corollary rep_eq_iff: "(rep_nat x = rep_nat y) ⟷ (x = y)"
  by (auto elim: rep_inj)

lemma abs_inj:
  assumes "abs_nat m = abs_nat n"
  shows "m = n"
proof -
  have "rep_nat (abs_nat m) = rep_nat (abs_nat n)" by (simp only: assms)
  thus ?thesis by (simp only: abs_inverse)
qed

corollary abs_eq_iff: "(abs_nat m = abs_nat n) ⟷ (m = n)"
  by (auto elim: abs_inj)

lemma rep_zero [simp]: "rep_nat 0 = 0"
  using abs_inverse abs_zero by fastforce

lemma rep_zero_iff: "(rep_nat x = 0) ⟷ (x = 0)"
  using rep_eq_iff by fastforce

lemma plus_eq: "x + y = abs_nat (rep_nat x + rep_nat y)"
  by (metis abs_plus rep_inverse)

lemma rep_plus: "rep_nat (x + y) = rep_nat x + rep_nat y"
  by (simp add: plus_eq)

lemma minus_eq: "x - y = abs_nat (rep_nat x - rep_nat y)"
  by (metis abs_minus rep_inverse)

lemma rep_minus: "rep_nat (x - y) = rep_nat x - rep_nat y"
  by (simp add: minus_eq)

lemma ord_iff:
  "x ≤ y ⟷ rep_nat x ≤ rep_nat y" (is ?thesis1)
  "x < y ⟷ rep_nat x < rep_nat y" (is ?thesis2)
proof -
  show ?thesis1
  proof
    assume "x ≤ y"
    show "rep_nat x ≤ rep_nat y"
    proof (rule ccontr)
      assume "¬ rep_nat x ≤ rep_nat y"
      hence "rep_nat y ≤ rep_nat x" and "rep_nat x ≠ rep_nat y" by simp_all
      from this(1) have "abs_nat (rep_nat y) ≤ abs_nat (rep_nat x)" by (rule abs_ord)
      hence "y ≤ x" by (simp only: rep_inverse)
      moreover from ‹rep_nat x ≠ rep_nat y› have "y ≠ x" using rep_inj by auto
      ultimately have "y < x" by simp
      with ‹x ≤ y› show False by simp
    qed
  next
    assume "rep_nat x ≤ rep_nat y"
    hence "abs_nat (rep_nat x) ≤ abs_nat (rep_nat y)" by (rule abs_ord)
    thus "x ≤ y" by (simp only: rep_inverse)
  qed
  thus ?thesis2 using rep_inj[of x y] by (auto simp: less_le Nat.nat_less_le)
qed

lemma ex_iff_abs: "(∃x::'a. P x) ⟷ (∃n::nat. P (abs_nat n))"
  by (metis rep_inverse)

lemma ex_iff_abs': "(∃x<abs_nat m. P x) ⟷ (∃n::nat<m. P (abs_nat n))"
  by (metis abs_inverse rep_inverse ord_iff(2))

lemma all_iff_abs: "(∀x::'a. P x) ⟷ (∀n::nat. P (abs_nat n))"
  by (metis rep_inverse)

lemma all_iff_abs': "(∀x<abs_nat m. P x) ⟷ (∀n::nat<m. P (abs_nat n))"
  by (metis abs_inverse rep_inverse ord_iff(2))

subclass linorder by (standard, auto simp: ord_iff rep_inj)

lemma comparator_of_rep [simp]: "comparator_of (rep_nat x) (rep_nat y) = comparator_of x y"
  by (simp add: comparator_of_def linorder_class.comparator_of_def ord_iff rep_inj)

subclass wellorder
proof
  fix P::"'a → bool" and a::'a
  let ?P = "λn::nat. P (abs_nat n)"
  assume a: "∧x. (∧y. y < x ==> P y) ==> P x"
  have "P (abs_nat (rep_nat a))"
  proof (rule less_induct[of _ "rep_nat a"])
    fix n::nat
    assume b: "∧m. m < n ==> ?P m"
    show "?P n"
    proof (rule a)
      fix y
      assume "y < abs_nat n"
      hence "rep_nat y < n" by (simp only: ord_iff abs_inverse)
      hence "?P (rep_nat y)" by (rule b)
      thus "P y" by (simp only: rep_inverse)
    qed
  qed
  thus "P a" by (simp only: rep_inverse)
qed

subclass comm_monoid_add by (standard, auto simp: plus_eq intro: arg_cong)

lemma sum_rep: "sum (rep_nat ∘ f) A = rep_nat (sum f A)" for f :: "'b → 'a" and A :: "'b set"
proof (induct A rule: infinite_finite_induct)
  case (infinite A)
  thus ?case by simp
next
  case empty
  show ?case by simp
next
  case (insert a A)
  from insert(1, 2) show ?case by (simp del: comp_apply add: insert(3) rep_plus, simp)
qed

subclass ordered_comm_monoid_add by (standard, simp add: ord_iff plus_eq)

subclass countable by intro_classes (intro exI[of _ rep_nat] injI, elim rep_inj)

subclass cancel_comm_monoid_add
  apply standard
  subgoal by (simp add: minus_eq rep_plus)
  subgoal by (simp add: minus_eq rep_plus)
  done

subclass add_wellorder
  apply standard
  subgoal by (simp add: ord_iff rep_plus)
  subgoal unfolding ord_iff by (drule le_imp_add, metis abs_plus rep_inverse)
  subgoal by (simp add: ord_iff)
  done

end

lemma the_min_eq_zero: "the_min = (0::'a::{the_min,nat})"
proof -
  have "the_min ≤ (0::'a)" by (fact the_min_min)
  hence "rep_nat (the_min::'a) ≤ rep_nat (0::'a)" by (simp only: ord_iff)
  also have "... = 0" by simp
  finally have "rep_nat (the_min::'a) = 0" by simp
  thus ?thesis by (simp only: rep_zero_iff)
qed

instantiation nat :: nat
begin

definition rep_nat_nat :: "nat → nat" where rep_nat_nat_def [code_unfold]: "rep_nat_nat = (λx. x)"
definition abs_nat_nat :: "nat → nat" where abs_nat_nat_def [code_unfold]: "abs_nat_nat = (λx. x)"

instance by (standard, simp_all add: rep_nat_nat_def abs_nat_nat_def)

end

instantiation natural :: nat
begin

definition rep_nat_natural :: "natural → nat"
  where rep_nat_natural_def [code_unfold]: "rep_nat_natural = nat_of_natural"
definition abs_nat_natural :: "nat → natural"
  where abs_nat_natural_def [code_unfold]: "abs_nat_natural = natural_of_nat"

instance by (standard, simp_all add: rep_nat_natural_def abs_nat_natural_def, metis minus_natural.rep_eq nat_of_natural_of_nat of_nat_of_natural)

end

subsection ‹Term Orders›

subsubsection ‹Type Classes›

class nat_pp_compare = linorder + zero + plus +
  fixes rep_nat_pp :: "'a → (nat, nat) pp"
    and abs_nat_pp :: "(nat, nat) pp → 'a"
    and lex_comp' :: "'a comparator"
    and deg' :: "'a → nat"
  assumes rep_nat_pp_inverse [simp]: "abs_nat_pp (rep_nat_pp x) = x"
    and abs_nat_pp_inverse [simp]: "rep_nat_pp (abs_nat_pp t) = t"
    and lex_comp': "lex_comp' x y = comp_of_ord lex_pp (rep_nat_pp x) (rep_nat_pp y)"
    and deg': "deg' x = deg_pp (rep_nat_pp x)"
    and le_pp: "rep_nat_pp x ≤ rep_nat_pp y ==> x ≤ y"
    and zero_pp: "rep_nat_pp 0 = 0"
    and plus_pp: "rep_nat_pp (x + y) = rep_nat_pp x + rep_nat_pp y"
begin

lemma less_pp:
  assumes "rep_nat_pp x < rep_nat_pp y"
  shows "x < y"
proof -
  from assms have 1: "rep_nat_pp x ≤ rep_nat_pp y" and 2: "rep_nat_pp x ≠ rep_nat_pp y" by simp_all
  from 1 have "x ≤ y" by (rule le_pp)
  moreover from 2 have "x ≠ y" by auto
  ultimately show ?thesis by simp
qed

lemma rep_nat_pp_inj:
  assumes "rep_nat_pp x = rep_nat_pp y"
  shows "x = y"
proof -
  have "abs_nat_pp (rep_nat_pp x) = abs_nat_pp (rep_nat_pp y)" by (simp only: assms)
  thus ?thesis by simp
qed

lemma lex_comp'_EqD:
  assumes "lex_comp' x y = Eq"
  shows "x = y"
proof (rule rep_nat_pp_inj)
  from assms show "rep_nat_pp x = rep_nat_pp y" by (simp add: lex_comp' comp_of_ord_def split: if_split_asm)
qed

lemma lex_comp'_valE:
  assumes "lex_comp' s t ≠ Eq"
  obtains x where "x ∈ keys_pp (rep_nat_pp s) ∪ keys_pp (rep_nat_pp t)"
    and "comparator_of (lookup_pp (rep_nat_pp s) x) (lookup_pp (rep_nat_pp t) x) = lex_comp' s t"
    and "∧y. y < x ==> lookup_pp (rep_nat_pp s) y = lookup_pp (rep_nat_pp t) y"
proof (cases "lex_comp' s t")
  case Eq
  with assms show ?thesis ..
next
  case Lt
  hence "rep_nat_pp s ≠ rep_nat_pp t" and "lex_pp (rep_nat_pp s) (rep_nat_pp t)"
    by (auto simp: lex_comp' comp_of_ord_def split: if_split_asm)
  hence "∃x. lookup_pp (rep_nat_pp s) x < lookup_pp (rep_nat_pp t) x ∧
             (∀y<x. lookup_pp (rep_nat_pp s) y = lookup_pp (rep_nat_pp t) y)"
    by (simp add: lex_pp_alt)
  then obtain x where 1: "lookup_pp (rep_nat_pp s) x < lookup_pp (rep_nat_pp t) x"
    and 2: "∧y. y < x ==> lookup_pp (rep_nat_pp s) y = lookup_pp (rep_nat_pp t) y" by blast
  show ?thesis
  proof
    show "x ∈ keys_pp (rep_nat_pp s) ∪ keys_pp (rep_nat_pp t)"
    proof (rule ccontr)
      assume "x ∉ keys_pp (rep_nat_pp s) ∪ keys_pp (rep_nat_pp t)"
      with 1 show False by (simp add: keys_pp_iff)
    qed
  next
    show "comparator_of (lookup_pp (rep_nat_pp s) x) (lookup_pp (rep_nat_pp t) x) = lex_comp' s t"
      by (simp add: linorder_class.comparator_of_def 1 Lt)
  qed (fact 2)
next
  case Gt
  hence "¬ lex_pp (rep_nat_pp s) (rep_nat_pp t)"
    by (auto simp: lex_comp' comp_of_ord_def split: if_split_asm)
  hence "lex_pp (rep_nat_pp t) (rep_nat_pp s)" by (rule lex_pp_lin')
  moreover have "rep_nat_pp t ≠ rep_nat_pp s"
  proof
    assume "rep_nat_pp t = rep_nat_pp s"
    moreover from this have "lex_pp (rep_nat_pp s) (rep_nat_pp t)" by (simp add: lex_pp_refl)
    ultimately have "lex_comp' s t = Eq" by (simp add: lex_comp' comp_of_ord_def)
    with Gt show False by simp
  qed
  ultimately have "∃x. lookup_pp (rep_nat_pp t) x < lookup_pp (rep_nat_pp s) x ∧
                    (∀y<x. lookup_pp (rep_nat_pp t) y = lookup_pp (rep_nat_pp s) y)"
    by (simp add: lex_pp_alt)
  then obtain x where 1: "lookup_pp (rep_nat_pp t) x < lookup_pp (rep_nat_pp s) x"
    and 2: "∧y. y < x ==> lookup_pp (rep_nat_pp t) y = lookup_pp (rep_nat_pp s) y" by blast
  show ?thesis
  proof
    show "x ∈ keys_pp (rep_nat_pp s) ∪ keys_pp (rep_nat_pp t)"
    proof (rule ccontr)
      assume "x ∉ keys_pp (rep_nat_pp s) ∪ keys_pp (rep_nat_pp t)"
      with 1 show False by (simp add: keys_pp_iff)
    qed
  next
    from 1 have "¬ lookup_pp (rep_nat_pp s) x < lookup_pp (rep_nat_pp t) x"
      and "lookup_pp (rep_nat_pp s) x ≠ lookup_pp (rep_nat_pp t) x" by simp_all
    thus "comparator_of (lookup_pp (rep_nat_pp s) x) (lookup_pp (rep_nat_pp t) x) = lex_comp' s t"
      by (simp add: linorder_class.comparator_of_def Gt)
  qed (simp add: 2)
qed

end

class nat_term_compare = linorder + nat_term +
  fixes is_scalar :: "'a itself → bool"
    and lex_comp :: "'a comparator"
    and deg_comp :: "'a comparator → 'a comparator"
    and pot_comp :: "'a comparator → 'a comparator"
  assumes zero_component: "∃x. snd (rep_nat_term x) = 0"
    and is_scalar: "is_scalar = (λ_. ∀x. snd (rep_nat_term x) = 0)"
    and lex_comp: "lex_comp = lex_comp_aux" ―‹For being able to implement ‹lex_comp› efficiently.›
    and deg_comp: "deg_comp cmp = (λx y. case comparator_of (deg_pp (fst (rep_nat_term x))) (deg_pp (fst (rep_nat_term y))) of Eq → cmp x y | val → val)"
    and pot_comp: "pot_comp cmp = (λx y. case comparator_of (snd (rep_nat_term x)) (snd (rep_nat_term y)) of Eq → cmp x y | val → val)"
    and le_term: "rep_nat_term x ≤ rep_nat_term y ==> x ≤ y"
begin

text ‹There is no need to add something like ‹top_comp› for TOP orders to class @{class nat_term_compare},
 because by default all comparators should @{emph ‹first›} compare power-products and @{emph ‹then›} positions.
 ‹lex_comp› obviously does.›

lemma less_term:
  assumes "rep_nat_term x < rep_nat_term y"
  shows "x < y"
proof -
  from assms have 1: "rep_nat_term x ≤ rep_nat_term y" and 2: "rep_nat_term x ≠ rep_nat_term y" by simp_all
  from 1 have "x ≤ y" by (rule le_term)
  moreover from 2 have "x ≠ y" by auto
  ultimately show ?thesis by simp
qed

lemma lex_comp_alt: "lex_comp = (comparator_of::'a comparator)"
proof -
  from lex_pp_antisym have as: "antisymp lex_pp" by (rule antisympI)
  interpret lex: comparator "comp_of_ord (lex_pp::(nat, nat) pp → _)"
    unfolding comp_of_ord_eq_comp_of_ords[OF as]
    by (rule comp_of_ords, unfold_locales,
        auto simp: lex_pp_refl intro: lex_pp_trans lex_pp_lin' elim!: lex_pp_antisym)

  have 1: "x = y" if "fst (rep_nat_term x) = fst (rep_nat_term y)"
                  and "snd (rep_nat_term x) = snd (rep_nat_term y)" for x y
    by (rule rep_nat_term_inj, rule prod_eqI, fact+)
  have 2: "x < y" if "fst (rep_nat_term x) = fst (rep_nat_term y)"
                  and "snd (rep_nat_term x) < snd (rep_nat_term y)" for x y
    by (rule less_term, simp add: less_prod_def that)
  have 3: False if "fst (rep_nat_term x) = fst (rep_nat_term y)"
                and "¬ snd (rep_nat_term x) < snd (rep_nat_term y)" and "x < y" for x y
  proof -
    from that(2) have a: "snd (rep_nat_term y) ≤ snd (rep_nat_term x)" by simp
    have "y ≤ x" by (rule le_term, simp add: less_eq_prod_def that(1) a)
    also have "... < y" by fact
    finally show False ..
  qed
  have 4: "x < y" if "fst (rep_nat_term x) ≠ fst (rep_nat_term y)"
                  and "lex_pp (fst (rep_nat_term x)) (fst (rep_nat_term y))" for x y
  proof -
    from that(2) have "fst (rep_nat_term x) ≤ fst (rep_nat_term y)" by (simp only: less_eq_pp_def)
    with that(1) have "fst (rep_nat_term x) < fst (rep_nat_term y)" by simp
    hence "rep_nat_term x < rep_nat_term y" by (simp add: less_prod_def)
    thus ?thesis by (rule less_term)
  qed
  have 5: False if "fst (rep_nat_term x) ≠ fst (rep_nat_term y)"
                and "¬ lex_pp (fst (rep_nat_term x)) (fst (rep_nat_term y))" and "x < y" for x y
  proof -
    from that(2) have a: "lex_pp (fst (rep_nat_term y)) (fst (rep_nat_term x))" by (rule lex_pp_lin')
    with that(1)[symmetric] have "y < x" by (rule 4)
    also have "... < y" by fact
    finally show False ..
  qed

  show ?thesis
    by (intro ext, simp add: lex_comp lex_comp_aux_def comparator_of_def linorder_class.comparator_of_def lex.eq split: order.splits,
        auto simp: lex_pp_refl comp_of_ord_def elim: 1 2 3 4 5)
qed

lemma full_component_zeroE: obtains x where "rep_nat_term x = (t, 0)"
proof -
  from zero_component obtain x' where "snd (rep_nat_term x') = 0" ..
  then obtain x where "rep_nat_term x = (t, 0)" by (rule full_componentE)
  thus ?thesis ..
qed

end

(* For some reason, the following lemmas cannot be stated in context "nat_term_compare". *)

lemma comparator_lex_comp: "comparator lex_comp"
  unfolding lex_comp by (fact comparator_lex_comp_aux)

lemma nat_term_comp_lex_comp: "nat_term_comp lex_comp"
  unfolding lex_comp by (fact nat_term_comp_lex_comp_aux)

lemma comparator_deg_comp:
  assumes "comparator cmp"
  shows "comparator (deg_comp cmp)"
  unfolding deg_comp using comparator_of assms by (rule comparator_lexicographic)

lemma comparator_pot_comp:
  assumes "comparator cmp"
  shows "comparator (pot_comp cmp)"
  unfolding pot_comp using comparator_of assms by (rule comparator_lexicographic)

lemma deg_comp_zero_min:
  assumes "comparator cmp" and "snd (rep_nat_term u) = snd (rep_nat_term v)" and "fst (rep_nat_term u) = 0"
  shows "deg_comp cmp u v ≠ Gt"
proof (simp add: deg_comp assms(3) comparator_of_def split: order.split, intro impI)
  assume "fst (rep_nat_term v) = 0"
  with assms(3) have "fst (rep_nat_term u) = fst (rep_nat_term v)" by simp
  hence "rep_nat_term u = rep_nat_term v" using assms(2) by (rule prod_eqI)
  hence "u = v" by (rule rep_nat_term_inj)
  from assms(1) interpret c: comparator cmp .
  show "cmp u v ≠ Gt" by (simp add: ‹u = v›)
qed

lemma deg_comp_pos:
  assumes "cmp u v = Lt" and "fst (rep_nat_term u) = fst (rep_nat_term v)"
  shows "deg_comp cmp u v = Lt"
  by (simp add: deg_comp assms split: order.split)

lemma deg_comp_monotone:
  assumes "cmp u v = Lt ==> cmp (splus t u) (splus t v) = Lt" and "deg_comp cmp u v = Lt"
  shows "deg_comp cmp (splus t u) (splus t v) = Lt"
  using assms(2) by (auto simp: deg_comp splus_term pprod.splus_def comparator_of_def deg_pp_plus
                          split: order.splits if_splits intro: assms(1))

lemma pot_comp_zero_min:
  assumes "cmp u v ≠ Gt" and "snd (rep_nat_term u) = snd (rep_nat_term v)"
  shows "pot_comp cmp u v ≠ Gt"
  by (simp add: pot_comp comparator_of_def assms split: order.split)

lemma pot_comp_pos:
  assumes "snd (rep_nat_term u) < snd (rep_nat_term v)"
  shows "pot_comp cmp u v = Lt"
  by (simp add: pot_comp comparator_of_def assms split: order.split)

lemma pot_comp_monotone:
  assumes "cmp u v = Lt ==> cmp (splus t u) (splus t v) = Lt" and "pot_comp cmp u v = Lt"
  shows "pot_comp cmp (splus t u) (splus t v) = Lt"
  using assms(2) by (auto simp: pot_comp splus_term pprod.splus_def comparator_of_def deg_pp_plus
                          split: order.splits if_splits intro: assms(1))

lemma deg_comp_cong:
  assumes "deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v)) ==> to1 u v = to2 u v"
  shows "deg_comp to1 u v = deg_comp to2 u v"
  using assms by (simp add: deg_comp comparator_of_def split: order.split)

lemma pot_comp_cong:
  assumes "snd (rep_nat_term u) = snd (rep_nat_term v) ==> to1 u v = to2 u v"
  shows "pot_comp to1 u v = pot_comp to2 u v"
  using assms by (simp add: pot_comp comparator_of_def split: order.split)

instantiation pp :: (nat, nat) nat_pp_compare
begin

definition rep_nat_pp_pp :: "('a, 'b) pp → (nat, nat) pp"
  where rep_nat_pp_pp_def [code del]: "rep_nat_pp_pp x = pp_of_fun (λn::nat. rep_nat (lookup_pp x (abs_nat n)))"

definition abs_nat_pp_pp :: "(nat, nat) pp → ('a, 'b) pp"
  where abs_nat_pp_pp_def [code del]: "abs_nat_pp_pp t = pp_of_fun (λn::'a. abs_nat (lookup_pp t (rep_nat n)))"

definition lex_comp'_pp :: "('a, 'b) pp comparator"
  where lex_comp'_pp_def [code del]: "lex_comp'_pp = comp_of_ord lex_pp"

definition deg'_pp :: "('a, 'b) pp → nat"
  where "deg'_pp x = rep_nat (deg_pp x)"

lemma lookup_rep_nat_pp_pp:
  "lookup_pp (rep_nat_pp t) = (λn::nat. rep_nat (lookup_pp t (abs_nat n)))"
  unfolding rep_nat_pp_pp_def
proof (rule lookup_pp_of_fun)
  have "{n. lookup_pp t (abs_nat n) ≠ 0} ⊆ rep_nat ` {x. lookup_pp t x ≠ 0}"
  proof
    fix n
    have "n = rep_nat (abs_nat n)" by (simp only: nat_class.abs_inverse)
    assume "n ∈ {n. lookup_pp t (abs_nat n) ≠ 0}"
    hence "abs_nat n ∈ {x. lookup_pp t x ≠ 0}" by simp
    with ‹n = rep_nat (abs_nat n)› show "n ∈ rep_nat ` {x. lookup_pp t x ≠ 0}" ..
  qed
  also have "finite ..." by (rule finite_imageI, transfer, simp)
  also (finite_subset) have "{n. lookup_pp t (abs_nat n) ≠ 0} = {n. rep_nat (lookup_pp t (abs_nat n)) ≠ 0}"
    by (metis rep_inj rep_zero)
  finally show "finite {x. rep_nat (lookup_pp t (abs_nat x)) ≠ 0}" .
qed

lemma lookup_abs_nat_pp_pp:
  "lookup_pp (abs_nat_pp t) = (λn::'a. abs_nat (lookup_pp t (rep_nat n)))"
  unfolding abs_nat_pp_pp_def
proof (rule lookup_pp_of_fun)
  have "{n::'a. lookup_pp t (rep_nat n) ≠ 0} ⊆ abs_nat ` {x. lookup_pp t x ≠ 0}"
  proof
    fix n :: 'a
    have "n = abs_nat (rep_nat n)" by (simp only: nat_class.rep_inverse)
    assume "n ∈ {n. lookup_pp t (rep_nat n) ≠ 0}"
    hence "rep_nat n ∈ {x. lookup_pp t x ≠ 0}" by simp
    with ‹n = abs_nat (rep_nat n)› show "n ∈ abs_nat ` {x. lookup_pp t x ≠ 0}" ..
  qed
  also have "finite ..." by (rule finite_imageI, transfer, simp)
  also (finite_subset) have "{n::'a. lookup_pp t (rep_nat n) ≠ 0} = {n. abs_nat (lookup_pp t (rep_nat n)) ≠ 0}"
    by (metis abs_inverse abs_zero)
  finally show "finite {n::'a. abs_nat (lookup_pp t (rep_nat n)) ≠ 0}" .
qed

lemma keys_rep_nat_pp_pp: "keys_pp (rep_nat_pp t) = rep_nat ` keys_pp t"
  by (rule set_eqI,
      simp add: keys_pp_iff lookup_rep_nat_pp_pp image_iff Bex_def ex_iff_abs[where 'a='a] rep_zero_iff del: neq0_conv)

lemma rep_nat_pp_pp_inverse: "abs_nat_pp (rep_nat_pp x) = x" for x::"('a, 'b) pp"
  by (rule pp_eqI, simp add: lookup_abs_nat_pp_pp lookup_rep_nat_pp_pp)

lemma abs_nat_pp_pp_inverse: "rep_nat_pp ((abs_nat_pp t)::('a, 'b) pp) = t"
  by (rule pp_eqI, simp add: lookup_abs_nat_pp_pp lookup_rep_nat_pp_pp)

corollary rep_nat_pp_pp_inj:
  fixes x y :: "('a, 'b) pp"
  assumes "rep_nat_pp x = rep_nat_pp y"
  shows "x = y"
  by (metis (no_types) rep_nat_pp_pp_inverse assms)

corollary rep_nat_pp_pp_eq_iff: "(rep_nat_pp x = rep_nat_pp y) ⟷ (x = y)" for x y :: "('a, 'b) pp"
  by (auto elim: rep_nat_pp_pp_inj)

lemma lex_rep_nat_pp: "lex_pp (rep_nat_pp x) (rep_nat_pp y) ⟷ lex_pp x y"
  by (simp add: lex_pp_alt rep_nat_pp_pp_eq_iff lookup_rep_nat_pp_pp rep_eq_iff
      ord_iff[symmetric] ex_iff_abs[where 'a='a] all_iff_abs')

corollary lex_comp'_pp: "lex_comp' x y = comp_of_ord lex_pp (rep_nat_pp x) (rep_nat_pp y)" for x y :: "('a, 'b) pp"
  by (simp add: lex_comp'_pp_def comp_of_ord_def rep_nat_pp_pp_eq_iff lex_rep_nat_pp)

corollary le_pp_pp: "rep_nat_pp x ≤ rep_nat_pp y ==> x ≤ y" for x y :: "('a, 'b) pp"
  by (simp only: less_eq_pp_def lex_rep_nat_pp)

lemma deg_rep_nat_pp: "deg_pp (rep_nat_pp t) = rep_nat (deg_pp t)" for t :: "('a, 'b) pp"
proof -
  have "keys_pp (rep_nat_pp t) = rep_nat ` keys_pp t"
    by (rule set_eqI, simp add: keys_pp_iff image_iff lookup_rep_nat_pp_pp Bex_def ex_iff_abs[where 'a='a] rep_zero_iff del: neq0_conv)
  hence "deg_pp (rep_nat_pp t) = sum (lookup_pp (rep_nat_pp t)) (rep_nat ` keys_pp t)"
    by (simp add: deg_pp_alt)
  also have "... = sum (lookup_pp (rep_nat_pp t) ∘ rep_nat) (keys_pp t)"
    by (rule sum.reindex, rule inj_onI, elim rep_inj)
  also have "... = sum (rep_nat ∘ (lookup_pp t)) (keys_pp t)"
    by (simp add: lookup_rep_nat_pp_pp)
  also have "... = rep_nat (deg_pp t)" by (simp only: deg_pp_alt sum_rep)
  finally show ?thesis .
qed

corollary deg'_pp: "deg' t = deg_pp (rep_nat_pp t)" for t :: "('a, 'b) pp"
  by (simp add: deg'_pp_def deg_rep_nat_pp)

lemma zero_pp_pp: "rep_nat_pp (0::('a, 'b) pp) = 0"
  by (rule pp_eqI, simp add: lookup_rep_nat_pp_pp)

lemma plus_pp_pp: "rep_nat_pp (x + y) = rep_nat_pp x + rep_nat_pp y"
  for x y :: "('a, 'b) pp"
  by (rule pp_eqI, simp add: lookup_rep_nat_pp_pp lookup_plus_pp rep_plus)

instance
  apply intro_classes
  subgoal by (fact rep_nat_pp_pp_inverse)
  subgoal by (fact abs_nat_pp_pp_inverse)
  subgoal by (fact lex_comp'_pp)
  subgoal by (fact deg'_pp)
  subgoal by (rule le_pp_pp)
  subgoal by (fact zero_pp_pp)
  subgoal by (fact plus_pp_pp)
  done

end

instantiation pp :: (nat, nat) nat_term
begin

definition rep_nat_term_pp :: "('a, 'b) pp → (nat, nat) pp × nat"
  where rep_nat_term_pp_def [code del]: "rep_nat_term_pp t = (rep_nat_pp t, 0)"

definition splus_pp :: "('a, 'b) pp → ('a, 'b) pp → ('a, 'b) pp"
  where splus_pp_def [code del]: "splus_pp = (+)"

instance proof
  fix x y :: "('a, 'b) pp"
  assume "rep_nat_term x = rep_nat_term y"
  hence "rep_nat_pp x = rep_nat_pp y" by (simp add: rep_nat_term_pp_def)
  thus "x = y" by (rule rep_nat_pp_pp_inj)
next
  fix x::"('a, 'b) pp" and i t
  assume "snd (rep_nat_term x) = i"
  hence "i = 0" by (simp add: rep_nat_term_pp_def)
  show "∃y::('a, 'b) pp. rep_nat_term y = (t, i)" unfolding ‹i = 0›
  proof
    show "rep_nat_term ((abs_nat_pp t)::('a, 'b) pp) = (t, 0)" by (simp add: rep_nat_term_pp_def)
  qed
next
  fix x y :: "('a, 'b) pp"
  show "rep_nat_term (splus x y) = pprod.splus (fst (rep_nat_term x)) (rep_nat_term y)"
    by (simp add: splus_pp_def rep_nat_term_pp_def pprod.splus_def plus_pp_pp)
qed

end

instantiation pp :: (nat, nat) nat_term_compare
begin

definition is_scalar_pp :: "('a, 'b) pp itself → bool"
  where is_scalar_pp_def [code_unfold]: "is_scalar_pp = (λ_. True)"

definition lex_comp_pp :: "('a, 'b) pp comparator"
  where lex_comp_pp_def [code_unfold]: "lex_comp_pp = lex_comp'"

definition deg_comp_pp :: "('a, 'b) pp comparator → ('a, 'b) pp comparator"
  where deg_comp_pp_def: "deg_comp_pp cmp = (λx y. case comparator_of (deg_pp x) (deg_pp y) of Eq → cmp x y | val → val)"

definition pot_comp_pp :: "('a, 'b) pp comparator → ('a, 'b) pp comparator"
  where pot_comp_pp_def [code_unfold]: "pot_comp_pp = (λcmp. cmp)"

instance proof
  show "∃x::('a, 'b) pp. snd (rep_nat_term x) = 0"
  proof
    show "snd (rep_nat_term (0::('a, 'b) pp)) = 0" by (simp add: rep_nat_term_pp_def)
  qed
next
  show "is_scalar = (λ_::('a, 'b) pp itself. ∀x::('a, 'b) pp. snd (rep_nat_term x) = 0)"
    by (simp add: is_scalar_pp_def rep_nat_term_pp_def)
next
  show "lex_comp = (lex_comp_aux::('a, 'b) pp comparator)"
    by (auto simp: lex_comp_pp_def lex_comp_aux_def rep_nat_term_pp_def lex_comp'_pp split: order.split intro!: ext)
next
  fix cmp :: "('a, 'b) pp comparator"
  show "deg_comp cmp =
         (λx y. case comparator_of (deg_pp (fst (rep_nat_term x))) (deg_pp (fst (rep_nat_term y))) of Eq → cmp x y
                      | Lt → Lt | Gt → Gt)"
    by (simp add: rep_nat_term_pp_def deg_comp_pp_def deg_rep_nat_pp comparator_of_rep)
next
  fix cmp :: "('a, 'b) pp comparator"
  show "pot_comp cmp =
         (λx y. case comparator_of (snd (rep_nat_term x)) (snd (rep_nat_term y)) of Eq → cmp x y | Lt → Lt | Gt → Gt)"
    by (simp add: rep_nat_term_pp_def pot_comp_pp_def)
next
  fix x y :: "('a, 'b) pp"
  assume "rep_nat_term x ≤ rep_nat_term y"
  hence "rep_nat_pp x ≤ rep_nat_pp y" by (auto simp: rep_nat_term_pp_def)
  thus "x ≤ y" by (rule le_pp_pp)
qed

end

instance pp :: (nat, nat) nat_pp_term
proof
  show "rep_nat_term (0::('a, 'b) pp) = (0, 0)"
    by (simp add: rep_nat_term_pp_def) (metis deg_pp_eq_0_iff deg_rep_nat_pp rep_zero)
next
  show "splus = ((+)::('a, 'b) pp → _)" by (simp add: splus_pp_def)
qed

instantiation prod :: ("{nat_pp_compare, comm_powerprod}", nat) nat_term
begin

definition rep_nat_term_prod :: "('a × 'b) → ((nat, nat) pp × nat)"
  where rep_nat_term_prod_def [code del]: "rep_nat_term_prod u = (rep_nat_pp (fst u), rep_nat (snd u))"

definition splus_prod :: "('a × 'b) → ('a × 'b) → ('a × 'b)"
  where splus_prod_def [code del]: "splus_prod t u = pprod.splus (fst t) u"

instance proof
  fix x y :: "'a × 'b"
  assume "rep_nat_term x = rep_nat_term y"
  hence 1: "rep_nat_pp (fst x) = rep_nat_pp (fst y)" and 2: "rep_nat (snd x) = rep_nat (snd y)"
    by (simp_all add: rep_nat_term_prod_def)
  from 1 have "fst x = fst y" by (rule rep_nat_pp_inj)
  moreover from 2 have "snd x = snd y" by (rule rep_inj)
  ultimately show "x = y" by (rule prod_eqI)
next
  fix i t
  show "∃y::'a × 'b. rep_nat_term y = (t, i)"
  proof
    show "rep_nat_term (abs_nat_pp t, abs_nat i) = (t, i)" by (simp add: rep_nat_term_prod_def)
  qed
next
  fix x y :: "'a × 'b"
  show "rep_nat_term (splus x y) = pprod.splus (fst (rep_nat_term x)) (rep_nat_term y)"
    by (simp add: splus_prod_def rep_nat_term_prod_def pprod.splus_def plus_pp)
qed

end

instantiation prod :: ("{nat_pp_compare, comm_powerprod}", nat) nat_term_compare
begin

definition is_scalar_prod :: "('a × 'b) itself → bool"
  where is_scalar_prod_def [code_unfold]: "is_scalar_prod = (λ_. False)"

definition lex_comp_prod :: "('a × 'b) comparator"
  where "lex_comp_prod = (λu v. case lex_comp' (fst u) (fst v) of Eq → comparator_of (snd u) (snd v) | val → val)"

definition deg_comp_prod :: "('a × 'b) comparator → ('a × 'b) comparator"
  where deg_comp_prod_def: "deg_comp_prod cmp = (λx y. case comparator_of (deg' (fst x)) (deg' (fst y)) of Eq → cmp x y | val → val)"

definition pot_comp_prod :: "('a × 'b) comparator → ('a × 'b) comparator"
  where "pot_comp_prod cmp = (λu v. case comparator_of (snd u) (snd v) of Eq → cmp u v | val → val)"

instance proof
  show "∃x::'a × 'b. snd (rep_nat_term x) = 0"
  proof
    show "snd (rep_nat_term (abs_nat_pp 0, 0)) = 0" by (simp add: rep_nat_term_prod_def)
  qed
next
  have "¬ (∀a. rep_nat (a::'b) = 0)"
  proof
    assume "∀a. rep_nat (a::'b) = 0"
    hence "rep_nat ((abs_nat 1)::'b) = 0" by blast
    hence "((abs_nat 1)::'b) = 0" by (simp only: rep_zero_iff)
    hence "(1::nat) = 0" by (metis abs_inj abs_zero)
    thus False by simp
  qed
  thus "is_scalar = (λ_::('a × 'b) itself. ∀x. snd (rep_nat_term (x::'a × 'b)) = 0)"
    by (auto simp add: is_scalar_prod_def rep_nat_term_prod_def intro!: ext)
next
  show "lex_comp = (lex_comp_aux::('a × 'b) comparator)"
    by (auto simp: lex_comp_prod_def lex_comp_aux_def rep_nat_term_prod_def lex_comp' comparator_of_rep split: order.split intro!: ext)
next
  fix cmp :: "('a × 'b) comparator"
  show "deg_comp cmp =
         (λx y. case comparator_of (deg_pp (fst (rep_nat_term x))) (deg_pp (fst (rep_nat_term y))) of Eq → cmp x y
                   | Lt → Lt | Gt → Gt)"
    by (simp add: rep_nat_term_prod_def deg_comp_prod_def deg')
next
  fix cmp :: "('a × 'b) comparator"
  show "pot_comp cmp =
         (λx y. case comparator_of (snd (rep_nat_term x)) (snd (rep_nat_term y)) of Eq → cmp x y | Lt → Lt | Gt → Gt)"
    by (simp add: rep_nat_term_prod_def pot_comp_prod_def comparator_of_rep)
next
  fix x y :: "'a × 'b"
  assume "rep_nat_term x ≤ rep_nat_term y"
  hence "rep_nat_pp (fst x) < rep_nat_pp (fst y) ∨ (rep_nat_pp (fst x) ≤ rep_nat_pp (fst y) ∧ rep_nat (snd x) ≤ rep_nat (snd y))"
    by (simp add: rep_nat_term_prod_def)
  thus "x ≤ y" by (auto simp: less_eq_prod_def ord_iff[symmetric] intro: le_pp less_pp)
qed

end

lemmas [code del] = deg_pp.rep_eq plus_pp.abs_eq minus_pp.abs_eq

lemma rep_nat_pp_nat [code_unfold]: "(rep_nat_pp::(nat, nat) pp → (nat, nat) pp) = (λx. x)"
  by (intro ext pp_eqI, simp add: lookup_rep_nat_pp_pp abs_nat_nat_def rep_nat_nat_def)

subsubsection ‹‹LEX›, ‹DRLEX›, ‹DEG› and ‹POT››

definition LEX :: "'a::nat_term_compare nat_term_order" where "LEX = Abs_nat_term_order lex_comp"

definition DRLEX :: "'a::nat_term_compare nat_term_order"
  where "DRLEX = Abs_nat_term_order (deg_comp (pot_comp (λx y. lex_comp y x)))"

definition DEG :: "'a::nat_term_compare nat_term_order → 'a nat_term_order"
  where "DEG to = Abs_nat_term_order (deg_comp (nat_term_compare to))"

definition POT :: "'a::nat_term_compare nat_term_order → 'a nat_term_order"
  where "POT to = Abs_nat_term_order (pot_comp (nat_term_compare to))"

text ‹@{const DRLEX} must apply @{const pot_comp}, for otherwise it does not satisfy
 the second condition of @{const nat_term_comp}.›

text ‹Instead of @{const DRLEX} one could also introduce another unary constructor ‹DEGREV›, analogous
 to @{const DEG} and @{const POT}. Then, however, proving (in)equalities of the term orders gets
 really messy (think of @{prop "DEG (POT to) = DEGREV (DEGREV to)"}, for instance).
 So, we restrict the formalization to @{const DRLEX} only.›

abbreviation "DLEX ≡ DEG LEX"

code_datatype LEX DRLEX DEG POT

lemma nat_term_compare_LEX [code]: "nat_term_compare LEX = lex_comp"
  unfolding LEX_def using comparator_lex_comp nat_term_comp_lex_comp
  by (rule nat_term_compare_Abs_nat_term_order_id)

lemma nat_term_compare_DRLEX [code]: "nat_term_compare DRLEX = deg_comp (pot_comp (λx y. lex_comp y x))"
proof -
  have cmp: "comparator (pot_comp (λx y. lex_comp y x))"
    by (rule comparator_pot_comp, rule comparator_converse, fact comparator_lex_comp)
  show ?thesis unfolding DRLEX_def
  proof (rule nat_term_compare_Abs_nat_term_order_id)
    from cmp show "comparator (deg_comp (pot_comp (λx y::'a. lex_comp y x)))"
      by (rule comparator_deg_comp)
  next
    show "nat_term_comp (deg_comp (pot_comp (λx y::'a. lex_comp y x)))"
    proof (rule nat_term_compI)
      fix u v :: 'a
      assume "snd (rep_nat_term u) = snd (rep_nat_term v)" and "fst (rep_nat_term u) = 0"
      with cmp show "deg_comp (pot_comp (λx y::'a. lex_comp y x)) u v ≠ Gt"
        by (rule deg_comp_zero_min)
    next
      fix u v :: 'a
      assume "snd (rep_nat_term u) < snd (rep_nat_term v)"
      hence "pot_comp (λx y. lex_comp y x) u v = Lt" by (rule pot_comp_pos)
      moreover assume "fst (rep_nat_term u) = fst (rep_nat_term v)"
      ultimately show "deg_comp (pot_comp (λx y. lex_comp y x)) u v = Lt" by (rule deg_comp_pos)
    next
      fix t u v :: 'a
      have "pot_comp (λx y. lex_comp y x) (splus t u) (splus t v) = Lt"
        if "pot_comp (λx y. lex_comp y x) u v = Lt" using _ that
      proof (rule pot_comp_monotone)
        assume "lex_comp v u = Lt"
        with nat_term_comp_lex_comp show "lex_comp (splus t v) (splus t u) = Lt"
          by (rule nat_term_compD3)
      qed
      moreover assume "deg_comp (pot_comp (λx y. lex_comp y x)) u v = Lt"
      ultimately show "deg_comp (pot_comp (λx y. lex_comp y x)) (splus t u) (splus t v) = Lt"
        by (rule deg_comp_monotone)
    next
      fix u v a b :: 'a
      assume "fst (rep_nat_term v) = fst (rep_nat_term b)" and "fst (rep_nat_term u) = fst (rep_nat_term a)"
        and "snd (rep_nat_term u) = snd (rep_nat_term v)" and "snd (rep_nat_term a) = snd (rep_nat_term b)"
      moreover from comparator_lex_comp nat_term_comp_lex_comp this(1, 2) this(3, 4)[symmetric]
      have "lex_comp v u = lex_comp b a" by (rule nat_term_compD4')
      moreover assume "deg_comp (pot_comp (λx y. lex_comp y x)) a b = Lt"
      ultimately show "deg_comp (pot_comp (λx y. lex_comp y x)) u v = Lt"
        by (simp add: deg_comp pot_comp split: order.splits)
    qed
  qed
qed

lemma nat_term_compare_DEG [code]: "nat_term_compare (DEG to) = deg_comp (nat_term_compare to)"
  unfolding DEG_def
proof (rule nat_term_compare_Abs_nat_term_order_id)
  from comparator_nat_term_compare show "comparator (deg_comp (nat_term_compare to))"
    by (rule comparator_deg_comp)
next
  show "nat_term_comp (deg_comp (nat_term_compare to))"
  proof (rule nat_term_compI)
    fix u v :: 'a
    assume "snd (rep_nat_term u) = snd (rep_nat_term v)" and "fst (rep_nat_term u) = 0"
    with comparator_nat_term_compare show "deg_comp (nat_term_compare to) u v ≠ Gt"
      by (rule deg_comp_zero_min)
  next
    fix u v :: 'a
    assume a: "fst (rep_nat_term u) = fst (rep_nat_term v)" and "snd (rep_nat_term u) < snd (rep_nat_term v)"
    with nat_term_comp_nat_term_compare have "nat_term_compare to u v = Lt" by (rule nat_term_compD2)
    thus "deg_comp (nat_term_compare to) u v = Lt" using a by (rule deg_comp_pos)
  next
    fix t u v :: 'a
    from nat_term_comp_nat_term_compare
    have "nat_term_compare to u v = Lt ==> nat_term_compare to (splus t u) (splus t v) = Lt"
      by (rule nat_term_compD3)
    moreover assume "deg_comp (nat_term_compare to) u v = Lt"
    ultimately show "deg_comp (nat_term_compare to) (splus t u) (splus t v) = Lt" by (rule deg_comp_monotone)
  next
    fix u v a b :: 'a
    assume "fst (rep_nat_term u) = fst (rep_nat_term a)" and "fst (rep_nat_term v) = fst (rep_nat_term b)"
      and "snd (rep_nat_term u) = snd (rep_nat_term v)" and "snd (rep_nat_term a) = snd (rep_nat_term b)"
    moreover from comparator_nat_term_compare nat_term_comp_nat_term_compare this
    have "nat_term_compare to u v = nat_term_compare to a b"
      by (rule nat_term_compD4')
    moreover assume "deg_comp (nat_term_compare to) a b = Lt"
    ultimately show "deg_comp (nat_term_compare to) u v = Lt"
      by (simp add: deg_comp split: order.splits)
  qed
qed

lemma nat_term_compare_POT [code]: "nat_term_compare (POT to) = pot_comp (nat_term_compare to)"
  unfolding POT_def
proof (rule nat_term_compare_Abs_nat_term_order_id)
  from comparator_nat_term_compare show "comparator (pot_comp (nat_term_compare to))"
    by (rule comparator_pot_comp)
next
  show "nat_term_comp (pot_comp (nat_term_compare to))"
  proof (rule nat_term_compI)
    fix u v :: 'a
    assume a: "snd (rep_nat_term u) = snd (rep_nat_term v)" and "fst (rep_nat_term u) = 0"
    with nat_term_comp_nat_term_compare have "nat_term_compare to u v ≠ Gt" by (rule nat_term_compD1)
    thus "pot_comp (nat_term_compare to) u v ≠ Gt" using a by (rule pot_comp_zero_min)
  next
    fix u v :: 'a
    assume "snd (rep_nat_term u) < snd (rep_nat_term v)"
    thus "pot_comp (nat_term_compare to) u v = Lt" by (rule pot_comp_pos)
  next
    fix t u v :: 'a
    from nat_term_comp_nat_term_compare
    have "nat_term_compare to u v = Lt ==> nat_term_compare to (splus t u) (splus t v) = Lt"
      by (rule nat_term_compD3)
    moreover assume "pot_comp (nat_term_compare to) u v = Lt"
    ultimately show "pot_comp (nat_term_compare to) (splus t u) (splus t v) = Lt" by (rule pot_comp_monotone)
  next
    fix u v a b :: 'a
    assume "fst (rep_nat_term u) = fst (rep_nat_term a)" and "fst (rep_nat_term v) = fst (rep_nat_term b)"
      and "snd (rep_nat_term u) = snd (rep_nat_term v)" and "snd (rep_nat_term a) = snd (rep_nat_term b)"
    moreover from comparator_nat_term_compare nat_term_comp_nat_term_compare this
    have "nat_term_compare to u v = nat_term_compare to a b"
      by (rule nat_term_compD4')
    moreover assume "pot_comp (nat_term_compare to) a b = Lt"
    ultimately show "pot_comp (nat_term_compare to) u v = Lt"
      by (simp add: pot_comp split: order.splits)
  qed
qed

lemma nat_term_compare_POT_DRLEX [code]:
  "nat_term_compare (POT DRLEX) = pot_comp (deg_comp (λx y. lex_comp y x))"
  unfolding nat_term_compare_POT nat_term_compare_DRLEX
  by (intro ext pot_comp_cong deg_comp_cong, simp add: pot_comp)

lemma compute_lex_pp [code]: "lex_pp p q = (lex_comp' p q ≠ Gt)"
  by (simp add: lex_comp'_pp_def comp_of_ord_def)

lemma compute_dlex_pp [code]: "dlex_pp p q = (deg_comp lex_comp' p q ≠ Gt)"
  by (simp add: deg_comp_pp_def dlex_pp_alt compute_lex_pp comparator_of_def)

lemma compute_drlex_pp [code]: "drlex_pp p q = (deg_comp (λx y. lex_comp' y x) p q ≠ Gt)"
  by (simp add: deg_comp_pp_def drlex_pp_alt compute_lex_pp comparator_of_def)

lemma nat_pp_order_of_le_nat_pp [code]: "nat_term_order_of_le = LEX"
  by (simp add: nat_term_order_of_le_def LEX_def lex_comp_alt)

subsubsection ‹Equality of Term Orders›

definition nat_term_order_eq :: "'a nat_term_order → 'a::nat_term_compare nat_term_order → bool → bool → bool"
  where nat_term_order_eq_def [code del]:
      "nat_term_order_eq to1 to2 dg ps =
                (∀u v. (dg ⟶ deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))) ⟶
                       (ps ⟶ snd (rep_nat_term u) = snd (rep_nat_term v)) ⟶
                       nat_term_compare to1 u v = nat_term_compare to2 u v)"

lemma nat_term_order_eqI:
  assumes "∧u v. (dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))) ==>
                  (ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)) ==>
                  nat_term_compare to1 u v = nat_term_compare to2 u v"
  shows "nat_term_order_eq to1 to2 dg ps"
  unfolding nat_term_order_eq_def using assms by blast

lemma nat_term_order_eqD:
  assumes "nat_term_order_eq to1 to2 dg ps"
    and "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
    and "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
  shows "nat_term_compare to1 u v = nat_term_compare to2 u v"
  using assms unfolding nat_term_order_eq_def by blast

lemma nat_term_order_eq_sym: "nat_term_order_eq to1 to2 dg ps ⟷ nat_term_order_eq to2 to1 dg ps"
  by (auto simp: nat_term_order_eq_def)

lemma nat_term_order_eq_DEG_dg:
  "nat_term_order_eq (DEG to1) to2 True ps ⟷ nat_term_order_eq to1 to2 True ps"
  by (auto simp: nat_term_order_eq_def nat_term_compare_DEG deg_comp)

lemma nat_term_order_eq_DEG_dg':
  "nat_term_order_eq to1 (DEG to2) True ps ⟷ nat_term_order_eq to1 to2 True ps"
  by (simp add: nat_term_order_eq_sym[of to1] nat_term_order_eq_DEG_dg)

lemma nat_term_order_eq_POT_ps:
  assumes "ps ∨ is_scalar TYPE('a::nat_term_compare)"
  shows "nat_term_order_eq (POT (to1::'a nat_term_order)) to2 dg ps ⟷ nat_term_order_eq to1 to2 dg ps"
  using assms
proof
  assume "ps"
  thus ?thesis by (auto simp: nat_term_order_eq_def nat_term_compare_POT pot_comp)
next
  assume "is_scalar TYPE('a)"
  hence "snd (rep_nat_term x) = 0" for x::'a by (simp add: is_scalar)
  thus ?thesis by (auto simp: nat_term_order_eq_def nat_term_compare_POT pot_comp)
qed

lemma nat_term_order_eq_POT_ps':
  assumes "ps ∨ is_scalar TYPE('a::nat_term_compare)"
  shows "nat_term_order_eq to1 (POT (to2::'a nat_term_order)) dg ps ⟷ nat_term_order_eq to1 to2 dg ps"
  using assms by (simp add: nat_term_order_eq_sym[of to1] nat_term_order_eq_POT_ps)

lemma snd_rep_nat_term_eqI:
  assumes "ps ∨ is_scalar TYPE('a::nat_term_compare)" and "ps ==> snd (rep_nat_term (u::'a)) = snd (rep_nat_term (v::'a))"
  shows "snd (rep_nat_term u) = snd (rep_nat_term v)"
  using assms(1)
proof
  assume "is_scalar TYPE('a)"
  thus ?thesis by (simp add: is_scalar)
qed (fact assms(2))

definition of_exps :: "nat → nat → nat → 'a::nat_term_compare"
  where "of_exps a b i =
        (THE u. rep_nat_term u = (pp_of_fun (λx. if x = 0 then a else if x = 1 then b else 0),
                                  if (∃v::'a. snd (rep_nat_term v) = i) then i else 0))"

text ‹@{const of_exps} is an auxiliary function needed for proving the equalities of the various
 term orders.›

lemma rep_nat_term_of_exps:
  "rep_nat_term ((of_exps a b i)::'a::nat_term_compare) =
    (pp_of_fun (λx::nat. if x = 0 then a else if x = 1 then b else 0), if (∃y::'a. snd (rep_nat_term y) = i) then i else 0)"
proof (cases "∃y::'a. snd (rep_nat_term y) = i")
  case True
  then obtain y::'a where "snd (rep_nat_term y) = i" ..
  then obtain u::'a where u: "rep_nat_term u = (pp_of_fun (λx::nat. if x = 0 then a else if x = 1 then b else 0), i)"
    by (rule full_componentE)
  from True have eq: "(if ∃y::'a. snd (rep_nat_term y) = i then i else 0) = i" by simp
  show ?thesis unfolding of_exps_def eq
  proof (rule theI)
    fix v :: 'a
    assume "rep_nat_term v = (pp_of_fun (λx::nat. if x = 0 then a else if x = 1 then b else 0), i)"
    thus "v = u" unfolding u[symmetric] by (rule rep_nat_term_inj)
  qed (fact u)
next
  case False
  hence eq: "(if ∃y::'a. snd (rep_nat_term y) = i then i else 0) = 0" by simp
  obtain u::'a where u: "rep_nat_term u = (pp_of_fun (λx::nat. if x = 0 then a else if x = 1 then b else 0), 0)"
    by (rule full_component_zeroE)
  show ?thesis unfolding of_exps_def eq
  proof (rule theI)
    fix v :: 'a
    assume "rep_nat_term v = (pp_of_fun (λx::nat. if x = 0 then a else if x = 1 then b else 0), 0)"
    thus "v = u" unfolding u[symmetric] by (rule rep_nat_term_inj)
  qed (fact u)
qed

lemma lookup_pp_of_exps:
  "lookup_pp (fst (rep_nat_term (of_exps a b i))) = (λx. if x = 0 then a else if x = 1 then b else 0)"
  unfolding rep_nat_term_of_exps fst_conv
proof (rule lookup_pp_of_fun)
  have "{x. (if x = 0 then a else if x = 1 then b else 0) ≠ 0} ⊆ {0, 1}"
    by (rule, simp split: if_split_asm)
  also have "finite ..." by simp
  finally(finite_subset) show "finite {x. (if x = 0 then a else if x = 1 then b else 0) ≠ 0}" .
qed

lemma keys_pp_of_exps: "keys_pp (fst (rep_nat_term (of_exps a b i))) ⊆ {0, 1}"
  by (rule, simp add: keys_pp_iff lookup_pp_of_exps split: if_split_asm)

lemma deg_pp_of_exps [simp]: "deg_pp (fst (rep_nat_term ((of_exps a b i)::'a::nat_term_compare))) = a + b"
proof -
  let ?u = "(of_exps a b i)::'a"
  have "sum (lookup_pp (fst (rep_nat_term ?u))) (keys_pp (fst (rep_nat_term ?u))) =
        sum (lookup_pp (fst (rep_nat_term ?u))) {0, 1}"
  proof (rule sum.mono_neutral_left, simp, fact keys_pp_of_exps, intro ballI)
    fix x
    assume "x ∈ {0, 1} - keys_pp (fst (rep_nat_term ?u))"
    thus "lookup_pp (fst (rep_nat_term ?u)) x = 0" by (simp add: keys_pp_iff)
  qed
  also have "... = a + b" by (simp add: lookup_pp_of_exps)
  finally show ?thesis by (simp only: deg_pp_alt)
qed

lemma snd_of_exps:
  assumes "snd (rep_nat_term (x::'a)) = i"
  shows "snd (rep_nat_term ((of_exps a b i)::'a::nat_term_compare)) = i"
proof -
  from assms have "∃x::'a. snd (rep_nat_term (x::'a)) = i" ..
  thus ?thesis by (simp add: rep_nat_term_of_exps)
qed

lemma snd_of_exps_zero [simp]: "snd (rep_nat_term ((of_exps a b 0)::'a::nat_term_compare)) = 0"
proof -
  from zero_component obtain x::'a where "snd (rep_nat_term (x::'a)) = 0" ..
  thus ?thesis by (rule snd_of_exps)
qed

lemma eq_of_exps:
  "(fst (rep_nat_term (of_exps a1 b1 i)) = fst (rep_nat_term (of_exps a2 b2 j))) ⟷ (a1 = a2 ∧ b1 = b2)"
proof -
  have "a1 = a2 ∧ b1 = b2"
    if "(λx::nat. if x = 0 then a1 else if x = 1 then b1 else 0) = (λx. if x = 0 then a2 else if x = 1 then b2 else 0)"
  proof
    from fun_cong[OF that, of 0] show "a1 = a2" by simp
  next
    from fun_cong[OF that, of 1] show "b1 = b2" by simp
  qed
  thus ?thesis by (auto simp: pp_eq_iff lookup_pp_of_exps)
qed

lemma lex_pp_of_exps:
  "lex_pp (fst (rep_nat_term ((of_exps a1 b1 i)::'a))) (fst (rep_nat_term ((of_exps a2 b2 j)::'a::nat_term_compare))) ⟷
    (a1 < a2 ∨ (a1 = a2 ∧ b1 ≤ b2))" (is "?L ⟷ ?R")
proof -
  let ?u = "fst (rep_nat_term ((of_exps a1 b1 i)::'a))"
  let ?v = "fst (rep_nat_term ((of_exps a2 b2 j)::'a))"
  show ?thesis
  proof
    assume ?L
    hence "?u = ?v ∨ (∃x. lookup_pp ?u x < lookup_pp ?v x ∧ (∀y<x. lookup_pp ?u y = lookup_pp ?v y))"
      by (simp only: lex_pp_alt)
    thus ?R
    proof
      assume "?u = ?v"
      thus ?thesis by (simp add: eq_of_exps)
    next
      assume "∃x. lookup_pp ?u x < lookup_pp ?v x ∧ (∀y<x. lookup_pp ?u y = lookup_pp ?v y)"
      then obtain x where 1: "lookup_pp ?u x < lookup_pp ?v x" and 2: "∧y. y < x ==> lookup_pp ?u y = lookup_pp ?v y"
        by auto
      from 1 have "lookup_pp ?v x ≠ 0" by simp
      hence "x ∈ keys_pp ?v" by (simp add: keys_pp_iff)
      also have "... ⊆ {0, 1}" by (fact keys_pp_of_exps)
      finally have "x = 0 ∨ x = 1" by simp
      thus ?thesis
      proof
        assume "x = 0"
        from 1 show ?thesis by (simp add: lookup_pp_of_exps ‹x = 0›)
      next
        assume "x = 1"
        hence "0 < x" by simp
        hence "lookup_pp ?u 0 = lookup_pp ?v 0" by (rule 2)
        hence "a1 = a2" by (simp add: lookup_pp_of_exps)
        from 1 show ?thesis by (simp add: lookup_pp_of_exps ‹x = 1› ‹a1 = a2›)
      qed
    qed
  next
    assume ?R
    thus ?L
    proof
      assume "a1 < a2"
      show ?thesis unfolding lex_pp_alt
      proof (intro disjI2 exI conjI allI impI)
        from ‹a1 < a2› show "lookup_pp ?u 0 < lookup_pp ?v 0" by (simp add: lookup_pp_of_exps)
      next
        fix y::nat
        assume "y < 0"
        thus "lookup_pp ?u y = lookup_pp ?v y" by simp
      qed
    next
      assume "a1 = a2 ∧ b1 ≤ b2"
      hence "a1 = a2" and "b1 ≤ b2" by simp_all
      from this(2) have "b1 < b2 ∨ b1 = b2" by auto
      thus ?thesis
      proof
        assume "b1 < b2"
        show ?thesis unfolding lex_pp_alt
        proof (intro disjI2 exI conjI allI impI)
          from ‹b1 < b2› show "lookup_pp ?u 1 < lookup_pp ?v 1" by (simp add: lookup_pp_of_exps)
        next
          fix y::nat
          assume "y < 1"
          hence "y = 0" by simp
          show "lookup_pp ?u y = lookup_pp ?v y" by (simp add: lookup_pp_of_exps ‹y = 0› ‹a1 = a2›)
        qed
      next
        assume "b1 = b2"
        show ?thesis by (simp add: lex_pp_alt eq_of_exps ‹a1 = a2› ‹b1 = b2›)
      qed
    qed
  qed
qed

lemma LEX_eq [code]:
  "nat_term_order_eq LEX (LEX::'a nat_term_order) dg ps = True" (is ?thesis1)
  "nat_term_order_eq LEX (DRLEX::'a nat_term_order) dg ps = False" (is ?thesis2)
  "nat_term_order_eq LEX (DEG (to::'a nat_term_order)) dg ps =
    (dg ∧ nat_term_order_eq LEX to dg ps)" (is ?thesis3)
  "nat_term_order_eq LEX (POT (to::'a nat_term_order)) dg ps =
    ((ps ∨ is_scalar TYPE('a::nat_term_compare)) ∧ nat_term_order_eq LEX to dg ps)" (is ?thesis4)
proof -
  show ?thesis1 by (simp add: nat_term_order_eq_def)
next
  show ?thesis2
  proof (intro iffI)
    assume a: "nat_term_order_eq LEX (DRLEX::'a nat_term_order) dg ps"
    let ?u = "(of_exps 0 1 0)::'a"
    let ?v = "(of_exps 1 0 0)::'a"
    have "nat_term_compare LEX ?u ?v = nat_term_compare DRLEX ?u ?v"
      by (rule nat_term_order_eqD, fact a, simp_all)
    thus False
      by (simp add: nat_term_compare_LEX lex_comp lex_comp_aux_def nat_term_compare_DRLEX deg_comp
          pot_comp comparator_of_def comp_of_ord_def lex_pp_of_exps eq_of_exps)
  qed (rule FalseE)
next
  show ?thesis3
  proof (intro iffI)
    assume a: "nat_term_order_eq LEX (DEG to) dg ps"
    have dg
    proof (rule ccontr)
      assume "¬ dg"
      let ?u = "(of_exps 0 2 0)::'a"
      let ?v = "(of_exps 1 0 0)::'a"
      have "nat_term_compare LEX ?u ?v = nat_term_compare (DEG to) ?u ?v"
        by (rule nat_term_order_eqD, fact a, simp_all add: ‹¬ dg›)
      thus False
        by (simp add: nat_term_compare_LEX lex_comp lex_comp_aux_def nat_term_compare_DEG deg_comp
            comparator_of_def comp_of_ord_def lex_pp_of_exps eq_of_exps)
    qed
    show "dg ∧ nat_term_order_eq LEX to dg ps"
    proof (intro conjI ‹dg› nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
      from ‹dg› have eq: "deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))" by (rule 1)
      assume "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      with a 1 have "nat_term_compare LEX u v = nat_term_compare (DEG to) u v"
        by (rule nat_term_order_eqD)
      also have "... = nat_term_compare to u v" by (simp add: nat_term_compare_DEG deg_comp eq)
      finally show "nat_term_compare LEX u v = nat_term_compare to u v" .
    qed
  next
    assume "dg ∧ nat_term_order_eq LEX to dg ps"
    hence dg and a: "nat_term_order_eq LEX to dg ps" by auto
    show "nat_term_order_eq LEX (DEG to) dg ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
      from ‹dg› have eq: "deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))" by (rule 1)
      assume "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      with a 1 have "nat_term_compare LEX u v = nat_term_compare to u v" by (rule nat_term_order_eqD)
      also have "... = nat_term_compare (DEG to) u v" by (simp add: nat_term_compare_DEG deg_comp eq)
      finally show "nat_term_compare LEX u v = nat_term_compare (DEG to) u v" .
    qed
  qed
next
  show ?thesis4
  proof (intro iffI)
    assume a: "nat_term_order_eq LEX (POT to) dg ps"
    have *: "ps ∨ is_scalar TYPE('a)"
    proof (rule ccontr)
      assume "¬ (ps ∨ is_scalar TYPE('a))"
      hence "¬ ps" and "¬ is_scalar TYPE('a)" by simp_all
      from this(2) obtain x::'a where "snd (rep_nat_term x) ≠ 0" unfolding is_scalar by auto
      moreover define i::nat where "i = snd (rep_nat_term x)"
      ultimately have "i ≠ 0" by simp
      let ?u = "(of_exps 0 1 i)::'a"
      let ?v = "(of_exps 1 0 0)::'a"
      from i_def[symmetric] have eq: "snd (rep_nat_term ?u) = i" by (rule snd_of_exps)
      have "nat_term_compare LEX ?u ?v = nat_term_compare (POT to) ?u ?v"
        by (rule nat_term_order_eqD, fact a, simp_all add: ‹¬ ps›)
      thus False
        by (simp add: nat_term_compare_LEX lex_comp lex_comp_aux_def pot_comp nat_term_compare_POT
            comparator_of_def comp_of_ord_def lex_pp_of_exps eq_of_exps eq ‹i ≠ 0› del: One_nat_def)
    qed
    show "(ps ∨ is_scalar TYPE('a)) ∧ nat_term_order_eq LEX to dg ps"
    proof (intro conjI * nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
      assume 2: "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      with * have eq: "snd (rep_nat_term u) = snd (rep_nat_term v)" by (rule snd_rep_nat_term_eqI)
      from a 1 2 have "nat_term_compare LEX u v = nat_term_compare (POT to) u v"
        by (rule nat_term_order_eqD)
      also have "... = nat_term_compare to u v" by (simp add: nat_term_compare_POT eq pot_comp)
      finally show "nat_term_compare LEX u v = nat_term_compare to u v" .
    qed
  next
    assume "(ps ∨ is_scalar TYPE('a)) ∧ nat_term_order_eq LEX to dg ps"
    hence *: "ps ∨ is_scalar TYPE('a)" and a: "nat_term_order_eq LEX to dg ps" by auto
    show "nat_term_order_eq LEX (POT to) dg ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
      assume 2: "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      with * have eq: "snd (rep_nat_term u) = snd (rep_nat_term v)" by (rule snd_rep_nat_term_eqI)
      from a 1 2 have "nat_term_compare LEX u v = nat_term_compare to u v" by (rule nat_term_order_eqD)
      also have "... = nat_term_compare (POT to) u v" by (simp add: nat_term_compare_POT eq pot_comp)
      finally show "nat_term_compare LEX u v = nat_term_compare (POT to) u v" .
    qed
  qed
qed

lemma DRLEX_eq [code]:
  "nat_term_order_eq DRLEX (LEX::'a nat_term_order) dg ps = False" (is ?thesis1)
  "nat_term_order_eq DRLEX DRLEX dg ps = True" (is ?thesis2)
  "nat_term_order_eq DRLEX (DEG (to::'a nat_term_order)) dg ps =
    nat_term_order_eq DRLEX to True ps" (is ?thesis3)
  "nat_term_order_eq DRLEX (POT (to::'a nat_term_order)) dg ps =
    ((dg ∨ ps ∨ is_scalar TYPE('a::nat_term_compare)) ∧ nat_term_order_eq DRLEX to dg True)" (is ?thesis4)
proof -
  from nat_term_order_eq_sym[of "DRLEX::'a nat_term_order"] show ?thesis1 by (simp only: LEX_eq)
next
  show ?thesis2 by (simp add: nat_term_order_eq_def)
next
  show ?thesis3
  proof (intro iffI)
    assume a: "nat_term_order_eq DRLEX (DEG to) dg ps"
    show "nat_term_order_eq DRLEX to True ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "True ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
        and "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      with a have "nat_term_compare DRLEX u v = nat_term_compare (DEG to) u v"
        by (rule nat_term_order_eqD, blast+)
      also have "... = nat_term_compare to u v" by (simp add: nat_term_compare_DEG deg_comp 1)
      finally show "nat_term_compare DRLEX u v = nat_term_compare to u v" .
    qed
  next
    assume a: "nat_term_order_eq DRLEX to True ps"
    show "nat_term_order_eq DRLEX (DEG to) dg ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      show "nat_term_compare DRLEX u v = nat_term_compare (DEG to) u v"
      proof (simp add: nat_term_compare_DRLEX nat_term_compare_DEG deg_comp comparator_of_def split: order.split, rule)
        assume 2: "deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
        with a have "nat_term_compare DRLEX u v = nat_term_compare to u v"
          using 1 by (rule nat_term_order_eqD)
        thus "pot_comp (λx y. lex_comp y x) u v = nat_term_compare to u v"
          by (simp add: nat_term_compare_DRLEX deg_comp 2)
      qed
    qed
  qed
next
  show ?thesis4
  proof (intro iffI)
    assume a: "nat_term_order_eq DRLEX (POT to) dg ps"
    have *: "dg ∨ ps ∨ is_scalar TYPE('a)"
    proof (rule ccontr)
      assume "¬ (dg ∨ ps ∨ is_scalar TYPE('a))"
      hence "¬ dg" and "¬ ps" and "¬ is_scalar TYPE('a)" by simp_all
      from this(3) obtain x::'a where "snd (rep_nat_term x) ≠ 0" unfolding is_scalar by auto
      moreover define i::nat where "i = snd (rep_nat_term x)"
      ultimately have "i ≠ 0" by simp
      let ?u = "(of_exps 1 0 i)::'a"
      let ?v = "(of_exps 2 0 0)::'a"
      from i_def[symmetric] have eq: "snd (rep_nat_term ?u) = i" by (rule snd_of_exps)
      have "nat_term_compare DRLEX ?u ?v = nat_term_compare (POT to) ?u ?v"
        by (rule nat_term_order_eqD, fact a, simp_all add: ‹¬ ps› ‹¬ dg›)
      thus False
        by (simp add: nat_term_compare_DRLEX deg_comp pot_comp nat_term_compare_POT
            comparator_of_def eq ‹i ≠ 0› del: One_nat_def)
    qed
    show "(dg ∨ ps ∨ is_scalar TYPE('a)) ∧ nat_term_order_eq DRLEX to dg True"
    proof (intro conjI * nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
      assume 2: "True ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      from a 1 2 have "nat_term_compare DRLEX u v = nat_term_compare (POT to) u v"
        by (rule nat_term_order_eqD, blast+)
      also have "... = nat_term_compare to u v" by (simp add: nat_term_compare_POT 2 pot_comp)
      finally show "nat_term_compare DRLEX u v = nat_term_compare to u v" .
    qed
  next
    assume "(dg ∨ ps ∨ is_scalar TYPE('a)) ∧ nat_term_order_eq DRLEX to dg True"
    hence disj: "dg ∨ ps ∨ is_scalar TYPE('a)" and a: "nat_term_order_eq DRLEX to dg True" by auto
    show "nat_term_order_eq DRLEX (POT to) dg ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume 1: "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
      assume 2: "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      from disj show "nat_term_compare DRLEX u v = nat_term_compare (POT to) u v"
      proof
        assume dg
        hence eq1: "deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))" by (rule 1)
        show ?thesis
        proof (simp add: nat_term_compare_DRLEX deg_comp eq1 nat_term_compare_POT pot_comp comparator_of_def split: order.split, rule)
          assume eq2: "snd (rep_nat_term u) = snd (rep_nat_term v)"
          with a 1 have "nat_term_compare DRLEX u v = nat_term_compare to u v" by (rule nat_term_order_eqD)
          thus "lex_comp v u = nat_term_compare to u v"
            by (simp add: nat_term_compare_DRLEX deg_comp eq1 pot_comp eq2)
        qed
      next
        assume "ps ∨ is_scalar TYPE('a)"
        hence eq: "snd (rep_nat_term u) = snd (rep_nat_term v)" using 2 by (rule snd_rep_nat_term_eqI)
        with a 1 have "nat_term_compare DRLEX u v = nat_term_compare to u v" by (rule nat_term_order_eqD)
        also have "... = nat_term_compare (POT to) u v" by (simp add: nat_term_compare_POT pot_comp eq)
        finally show ?thesis .
      qed
    qed
  qed
qed

lemma DEG_eq [code]:
  "nat_term_order_eq (DEG to) (LEX::'a nat_term_order) dg ps = nat_term_order_eq LEX (DEG to) dg ps"
  "nat_term_order_eq (DEG to) (DRLEX::'a nat_term_order) dg ps = nat_term_order_eq DRLEX (DEG to) dg ps"
  "nat_term_order_eq (DEG to1) (DEG (to2::'a nat_term_order)) dg ps =
    nat_term_order_eq to1 to2 True ps" (is ?thesis3)
  "nat_term_order_eq (DEG to1) (POT (to2::'a nat_term_order)) dg ps =
    (if dg then nat_term_order_eq to1 (POT to2) dg ps
    else ((ps ∨ is_scalar TYPE('a::nat_term_compare)) ∧ nat_term_order_eq (DEG to1) to2 dg ps))" (is ?thesis4)
proof -
  show ?thesis3
  proof (rule iffI)
    assume a: "nat_term_order_eq (DEG to1) (DEG to2) dg ps"
    show "nat_term_order_eq to1 to2 True ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume b: "True ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
        and "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      with a have "nat_term_compare (DEG to1) u v = nat_term_compare (DEG to2) u v"
        by (rule nat_term_order_eqD, blast+)
      thus "nat_term_compare to1 u v = nat_term_compare to2 u v"
        by (simp add: nat_term_compare_DEG deg_comp comparator_of_def b)
    qed
  next
    assume a: "nat_term_order_eq to1 to2 True ps"
    show "nat_term_order_eq (DEG to1) (DEG to2) dg ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume b: "ps ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      show "nat_term_compare (DEG to1) u v = nat_term_compare (DEG to2) u v"
      proof (simp add: nat_term_compare_DEG deg_comp comparator_of_def split: order.split, rule impI)
        assume "deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
        with a show "nat_term_compare to1 u v = nat_term_compare to2 u v" using b by (rule nat_term_order_eqD)
      qed
    qed
  qed
next
  show ?thesis4
  proof (simp add: nat_term_order_eq_DEG_dg split: if_split, intro impI)
    show "nat_term_order_eq (DEG to1) (POT to2) False ps =
            ((ps ∨ is_scalar TYPE('a)) ∧ nat_term_order_eq (DEG to1) to2 False ps)"
    proof (intro iffI)
      assume a: "nat_term_order_eq (DEG to1) (POT to2) False ps"
      have *: "ps ∨ is_scalar TYPE('a)"
      proof (rule ccontr)
        assume "¬ (ps ∨ is_scalar TYPE('a))"
        hence "¬ ps" and "¬ is_scalar TYPE('a)" by simp_all
        from this(2) obtain x::'a where "snd (rep_nat_term x) ≠ 0" unfolding is_scalar by auto
        moreover define i::nat where "i = snd (rep_nat_term x)"
        ultimately have "i ≠ 0" by simp
        let ?u = "(of_exps 1 0 i)::'a"
        let ?v = "(of_exps 2 0 0)::'a"
        from i_def[symmetric] have eq: "snd (rep_nat_term ?u) = i" by (rule snd_of_exps)
        have "nat_term_compare (DEG to1) ?u ?v = nat_term_compare (POT to2) ?u ?v"
          by (rule nat_term_order_eqD, fact a, simp_all add: ‹¬ ps›)
        thus False
          by (simp add: nat_term_compare_DEG deg_comp pot_comp nat_term_compare_POT
              comparator_of_def comp_of_ord_def lex_pp_of_exps eq_of_exps eq ‹i ≠ 0› del: One_nat_def)
      qed
      moreover from this a have "nat_term_order_eq (DEG to1) to2 False ps" by (simp add: nat_term_order_eq_POT_ps')
      ultimately show "(ps ∨ is_scalar TYPE('a)) ∧ nat_term_order_eq (DEG to1) to2 False ps" ..
    qed (simp add: nat_term_order_eq_POT_ps')
  qed
qed (fact nat_term_order_eq_sym)+

lemma POT_eq [code]:
  "nat_term_order_eq (POT to) LEX dg ps = nat_term_order_eq LEX (POT to) dg ps"
  "nat_term_order_eq (POT to1) (DEG to2) dg ps = nat_term_order_eq (DEG to2) (POT to1) dg ps"
  "nat_term_order_eq (POT to1) DRLEX dg ps = nat_term_order_eq DRLEX (POT to1) dg ps"
  "nat_term_order_eq (POT to1) (POT (to2::'a::nat_term_compare nat_term_order)) dg ps =
    nat_term_order_eq to1 to2 dg True" (is ?thesis4)
proof -
  show ?thesis4
  proof (rule iffI)
    assume a: "nat_term_order_eq (POT to1) (POT to2) dg ps"
    show "nat_term_order_eq to1 to2 dg True"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
        and b: "True ==> snd (rep_nat_term u) = snd (rep_nat_term v)"
      with a have "nat_term_compare (POT to1) u v = nat_term_compare (POT to2) u v"
        by (rule nat_term_order_eqD, blast+)
      thus "nat_term_compare to1 u v = nat_term_compare to2 u v"
        by (simp add: nat_term_compare_POT pot_comp comparator_of_def b)
    qed
  next
    assume a: "nat_term_order_eq to1 to2 dg True"
    show "nat_term_order_eq (POT to1) (POT to2) dg ps"
    proof (rule nat_term_order_eqI)
      fix u v :: 'a
      assume b: "dg ==> deg_pp (fst (rep_nat_term u)) = deg_pp (fst (rep_nat_term v))"
      show "nat_term_compare (POT to1) u v = nat_term_compare (POT to2) u v"
      proof (simp add: nat_term_compare_POT pot_comp comparator_of_def split: order.split, rule impI)
        assume "snd (rep_nat_term u) = snd (rep_nat_term v)"
        with a b show "nat_term_compare to1 u v = nat_term_compare to2 u v" by (rule nat_term_order_eqD)
      qed
    qed
  qed
qed (fact nat_term_order_eq_sym)+

lemma nat_term_order_equal [code]: "HOL.equal to1 to2 = nat_term_order_eq to1 to2 False False"
  by (auto simp: nat_term_order_eq_def equal_eq nat_term_compare_inject[symmetric])

hide_const (open) of_exps

value [code] "DEG (POT DRLEX) = (DRLEX::((nat, nat) pp × nat) nat_term_order)"

value [code] "POT LEX = (LEX::((nat, nat) pp × nat) nat_term_order)"

value [code] "POT LEX = (LEX::(nat, nat) pp nat_term_order)"

end (*theory*)