Theory Trail_Induced_Ordering

theory Trail_Induced_Ordering
  imports
    (* Isabelle theories *)
    Main

    (* AFP theories *)
    "List-Index.List_Index"
begin

lemma wf_if_convertible_to_wf:
  fixes r :: "'a rel" and s :: "'b rel" and f :: "'a ⇒ 'b"
  assumes "wf s" and convertible: "⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s"
  shows "wf r"
proof (rule wfI_min[of r])
  fix x :: 'a and Q :: "'a set"
  assume "x ∈ Q"
  then obtain y where "y ∈ Q" and "⋀z. (f z, f y) ∈ s ⟹ z ∉ Q"
    by (auto elim: wfE_min[OF wf_inv_image[of s f, OF ‹wf s›], unfolded in_inv_image])
  thus "∃z ∈ Q. ∀y. (y, z) ∈ r ⟶ y ∉ Q"
    by (auto intro: convertible)
qed

lemma wfP_if_convertible_to_wfP: "wfP S ⟹ (⋀x y. R x y ⟹ S (f x) (f y)) ⟹ wfP R"
  using wf_if_convertible_to_wf[to_pred, of S R f] by simp

text ‹Converting to @{typ nat} is a very common special case that might be found more easily by
  Sledgehammer.›

lemma wfP_if_convertible_to_nat:
  fixes f :: "_ ⇒ nat"
  shows "(⋀x y. R x y ⟹ f x < f y) ⟹ wfP R"
  by (rule wfP_if_convertible_to_wfP[of "(<) :: nat ⇒ nat ⇒ bool", simplified])





definition trail_less_id_id where
  "trail_less_id_id Ls L K ⟷
    (∃i < length Ls. ∃j < length Ls. i > j ∧ L = Ls ! i ∧ K = Ls ! j)"

definition trail_less_comp_id where
  "trail_less_comp_id Ls L K ⟷
    (∃i < length Ls. ∃j < length Ls. i > j ∧ L = - (Ls ! i) ∧ K = Ls ! j)"

definition trail_less_id_comp where
  "trail_less_id_comp Ls L K ⟷
    (∃i < length Ls. ∃j < length Ls. i ≥ j ∧ L = Ls ! i ∧ K = - (Ls ! j))"

definition trail_less_comp_comp where
  "trail_less_comp_comp Ls L K ⟷
    (∃i < length Ls. ∃j < length Ls. i > j ∧ L = - (Ls ! i) ∧ K = - (Ls ! j))"

definition trail_less where
  "trail_less Ls L K ⟷ trail_less_id_id Ls L K ∨ trail_less_comp_id Ls L K ∨
    trail_less_id_comp Ls L K ∨ trail_less_comp_comp Ls L K"

definition trail_less' where
  "trail_less' Ls = (λL K.
    (∃i. i < length Ls ∧ L = Ls ! i ∧ K = - (Ls ! i)) ∨
    (∃i. Suc i < length Ls ∧ L = - (Ls ! Suc i) ∧ K = Ls ! i))⇧+⇧+"

lemma transp_trail_less': "transp (trail_less' Ls)"
proof (rule transpI)
  show "⋀x y z. trail_less' Ls x y ⟹ trail_less' Ls y z ⟹ trail_less' Ls x z"
    by (metis (no_types, lifting) trail_less'_def tranclp_trans)
qed

lemma trail_less'_Suc:
  assumes "Suc i < length Ls"
  shows "trail_less' Ls (Ls ! Suc i) (Ls ! i)"
proof -
  have "trail_less' Ls (Ls ! Suc i) (- (Ls ! Suc i))"
    unfolding trail_less'_def
    using assms by blast
  moreover have "trail_less' Ls (- (Ls ! Suc i)) (Ls ! i)"
    by (metis (mono_tags, lifting) assms trail_less'_def tranclp.r_into_trancl)
  ultimately show ?thesis
    using transp_trail_less'[THEN transpD] by auto
qed

lemma trail_less'_comp_Suc_comp:
  assumes "Suc i < length Ls"
  shows "trail_less' Ls (- (Ls ! Suc i)) (- (Ls ! i))"
proof -
  have "trail_less' Ls (- (Ls ! Suc i)) (Ls ! i)"
    unfolding trail_less'_def
    using assms Suc_lessD by blast
  moreover have "trail_less' Ls (Ls ! i) (- (Ls ! i))"
    unfolding trail_less'_def
    using assms Suc_lessD by blast
  ultimately show ?thesis
    using transp_trail_less'[THEN transpD] by auto
qed

lemma trail_less'_id_id: "j < i ⟹ i < length Ls ⟹ trail_less' Ls (Ls ! i) (Ls ! j)"
proof (induction i arbitrary: j)
  case 0
  then show ?case
    by simp
next
  case (Suc i)
  then show ?case
    using trail_less'_Suc
    by (metis Suc_lessD less_Suc_eq transpD transp_trail_less')
qed

lemma trail_less'_comp_comp:
  "j < i ⟹ i < length Ls ⟹ trail_less' Ls (- (Ls ! i)) (- (Ls ! j))"
proof (induction i arbitrary: j)
  case 0
  then show ?case
    by simp
next
  case (Suc i)
  then show ?case
    using trail_less'_comp_Suc_comp
    by (metis Suc_lessD less_Suc_eq transpD transp_trail_less')
qed

lemma trail_less'_id_comp:
  assumes "j < i" and "i < length Ls"
  shows "trail_less' Ls (Ls ! i) (- (Ls ! j))"
proof -
  have "trail_less' Ls (Ls ! j) (- (Ls ! j))"
    unfolding trail_less'_def
    using assms dual_order.strict_trans by blast
  thus ?thesis
    using trail_less'_id_id[OF assms]
    using transp_trail_less'[THEN transpD] by auto
qed

lemma trail_less'_comp_id:
  assumes "j < i" and "i < length Ls"
  shows "trail_less' Ls (- (Ls ! i)) (Ls ! j)"
proof (cases i)
  case 0
  then show ?thesis
    using assms(1) by blast
next
  case (Suc i')
  hence "trail_less' Ls (- Ls ! i) (Ls ! i')"
    unfolding trail_less'_def
    using Suc_lessD assms(2) by blast
  show ?thesis
  proof (cases "i' = j")
    case True
    then show ?thesis
      using ‹trail_less' Ls (- Ls ! i) (Ls ! i')› by metis
  next
    case False
    hence "trail_less' Ls (Ls ! i') (Ls ! j)"
      by (metis Suc Suc_lessD assms(1) assms(2) less_SucE trail_less'_id_id)
    then show ?thesis
      using ‹trail_less' Ls (- Ls ! i) (Ls ! i')›
      using transp_trail_less'[THEN transpD] by auto
  qed
qed

lemma trail_less_eq_trail_less':
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
  shows "trail_less Ls = trail_less' Ls"
proof (intro ext iffI)
  fix L K
  show "trail_less Ls L K ⟹ trail_less' Ls L K"
    unfolding trail_less_def
  proof (elim disjE)
    assume "trail_less_id_id Ls L K"
    thus ?thesis
      using trail_less'_id_id by (metis trail_less_id_id_def)
  next
    show "trail_less_comp_id Ls L K ⟹ ?thesis"
      using trail_less'_comp_id by (metis trail_less_comp_id_def)
  next
    show "trail_less_id_comp Ls L K ⟹ ?thesis"
      using trail_less'_id_comp
      unfolding trail_less_id_comp_def
      by (metis (mono_tags, lifting) le_eq_less_or_eq trail_less'_def tranclp.r_into_trancl)
  next
    show "trail_less_comp_comp Ls L K ⟹ ?thesis"
      using trail_less'_comp_comp
      by (metis trail_less_comp_comp_def)
  qed
next
  fix L K
  show "trail_less' Ls L K ⟹ trail_less Ls L K"
    unfolding trail_less'_def
  proof (induction K rule: tranclp_induct)
    case (base K)
    then show ?case
    proof (elim exE conjE disjE)
      fix i assume "i < length Ls" and "L = Ls ! i" and "K = - (Ls ! i)"
      hence "trail_less_id_comp Ls L K"
        by (auto simp: trail_less_id_comp_def)
      thus "trail_less Ls L K"
        by (simp add: trail_less_def)
    next
      fix i assume "Suc i < length Ls" and "L = - (Ls ! Suc i)" and "K = Ls ! i"
      hence "trail_less_comp_id Ls L K"
        unfolding trail_less_comp_id_def
        using Suc_lessD by blast
      thus "trail_less Ls L K"
        by (simp add: trail_less_def)
    qed
  next
    case (step y z)
    from step.hyps(2) show ?case
    proof (elim exE conjE disjE)
      fix i assume "i < length Ls" and "y = Ls ! i" and "z = - (Ls ! i)"

      from step.IH[unfolded trail_less_def] show "trail_less Ls L z"
      proof (elim disjE)
        assume "trail_less_id_id Ls L y"
        hence "trail_less_id_comp Ls L z"
          unfolding trail_less_id_id_def trail_less_id_comp_def
          by (metis ‹y = Ls ! i› ‹z = - Ls ! i› less_or_eq_imp_le)
        thus "trail_less Ls L z"
          by (simp add: trail_less_def)
      next
        assume "trail_less_comp_id Ls L y"
        hence "trail_less_comp_comp Ls L z"
          unfolding trail_less_comp_id_def trail_less_comp_comp_def
          by (metis ‹y = Ls ! i› ‹z = - Ls ! i›)
        thus "trail_less Ls L z"
          by (simp add: trail_less_def)
      next
        assume "trail_less_id_comp Ls L y"
        hence "trail_less_id_comp Ls L z"
          unfolding trail_less_id_comp_def
          by (metis ‹i < length Ls› ‹y = Ls ! i› ‹z = - Ls ! i› pairwise_distinct)
        thus "trail_less Ls L z"
          by (simp add: trail_less_def)
      next
        assume "trail_less_comp_comp Ls L y"
        hence "trail_less_comp_comp Ls L z"
          unfolding trail_less_comp_comp_def
          by (metis ‹i < length Ls› ‹y = Ls ! i› ‹z = - Ls ! i› pairwise_distinct)
        thus "trail_less Ls L z"
          by (simp add: trail_less_def)
      qed
    next
      fix i assume "Suc i < length Ls" and "y = - Ls ! Suc i" and "z = Ls ! i"

      from step.IH[unfolded trail_less_def] show "trail_less Ls L z"
      proof (elim disjE)
        show "trail_less_id_id Ls L y ⟹ trail_less Ls L z"
          by (metis ‹Suc i < length Ls› ‹y = - Ls ! Suc i› ‹z = Ls ! i› not_less_eq
              order_less_imp_not_less pairwise_distinct trail_less_def trail_less_id_id_def)
      next
        show "trail_less_comp_id Ls L y ⟹ trail_less Ls L z"
          by (smt (verit, best) ‹Suc i < length Ls› ‹y = - Ls ! Suc i› ‹z = Ls ! i›
              dual_order.strict_trans lessI pairwise_distinct trail_less_comp_id_def trail_less_def)
      next
        assume "trail_less_id_comp Ls L y"
        hence "trail_less_id_id Ls L z"
          unfolding trail_less_def trail_less_id_comp_def trail_less_id_id_def
          by (metis Suc_le_lessD Suc_lessD ‹Suc i < length Ls› ‹y = - Ls ! Suc i› ‹z = Ls ! i›
              pairwise_distinct uminus_uminus_id)
        thus "trail_less Ls L z"
          by (simp add: trail_less_def)
      next
        assume "trail_less_comp_comp Ls L y"
        hence "trail_less_comp_id Ls L z"
          unfolding trail_less_comp_comp_def trail_less_comp_id_def
          by (metis Suc_lessD ‹Suc i < length Ls› ‹y = - Ls ! Suc i› ‹z = Ls ! i› pairwise_distinct
              uminus_uminus_id)
        thus "trail_less Ls L z"
          by (simp add: trail_less_def)
      qed
    qed
  qed
qed




subsection ‹Examples›

experiment
  fixes L0 L1 L2 :: "'a :: uminus"
begin

lemma "trail_less_id_comp [L2, L1, L0] L2 (- L2)"
  unfolding trail_less_id_comp_def
proof (intro exI conjI)
  show "(0 :: nat) ≤ 0" by presburger
qed simp_all

lemma "trail_less_comp_id [L2, L1, L0] (- L1) L2"
  unfolding trail_less_comp_id_def
proof (intro exI conjI)
  show "(0 :: nat) < 1" by presburger
qed simp_all

lemma "trail_less_id_comp [L2, L1, L0] L1 (- L1)"
  unfolding trail_less_id_comp_def
proof (intro exI conjI)
  show "(1 :: nat) ≤ 1" by presburger
qed simp_all

lemma "trail_less_comp_id [L2, L1, L0] (- L0) L1"
  unfolding trail_less_comp_id_def
proof (intro exI conjI)
  show "(1 :: nat) < 2" by presburger
qed simp_all

lemma "trail_less_id_comp [L2, L1, L0] L0 (- L0)"
  unfolding trail_less_id_comp_def
proof (intro exI conjI)
  show "(2 :: nat) ≤ 2" by presburger
qed simp_all

lemma "trail_less_id_id [L2, L1, L0] L1 L2"
  unfolding trail_less_id_id_def
proof (intro exI conjI)
  show "(0 :: nat) < 1" by presburger
qed simp_all

lemma "trail_less_id_id [L2, L1, L0] L0 L1"
  unfolding trail_less_id_id_def
proof (intro exI conjI)
  show "(1 :: nat) < 2" by presburger
qed simp_all

lemma "trail_less_comp_comp [L2, L1, L0] (- L1) (- L2)"
  unfolding trail_less_comp_comp_def
proof (intro exI conjI)
  show "(0 :: nat) < 1" by presburger
qed simp_all

lemma "trail_less_comp_comp [L2, L1, L0] (- L0) (- L1)"
  unfolding trail_less_comp_comp_def
proof (intro exI conjI)
  show "(1 :: nat) < 2" by presburger
qed simp_all

end


subsection ‹Miscellaneous Lemmas›

lemma not_trail_less_Nil: "¬ trail_less [] L K"
  unfolding trail_less_def trail_less_id_id_def trail_less_comp_id_def
    trail_less_id_comp_def trail_less_comp_comp_def
  by simp


lemma defined_if_trail_less:
  assumes "trail_less Ls L K"
  shows "L ∈ set Ls ∪ uminus ` set Ls" "K ∈ set Ls ∪ uminus ` set Ls"
   apply (atomize (full))
  using assms unfolding trail_less_def trail_less_id_id_def trail_less_comp_id_def
    trail_less_id_comp_def trail_less_comp_comp_def
  by (elim disjE exE conjE) simp_all

lemma not_less_if_undefined:
  fixes L :: "'a :: uminus"
  assumes
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    "L ∉ set Ls" "- L ∉ set Ls"
  shows "¬ trail_less Ls L K" "¬ trail_less Ls K L"
  using assms
  unfolding trail_less_def trail_less_id_id_def trail_less_comp_id_def trail_less_id_comp_def
    trail_less_comp_comp_def
  by auto

lemma defined_conv:
  fixes L :: "'a :: uminus"
  assumes uminus_uminus_id: "⋀x :: 'a. - (- x) = x"
  shows "L ∈ set Ls ∪ uminus ` set Ls ⟷ L ∈ set Ls ∨ - L ∈ set Ls"
  by (auto simp: rev_image_eqI uminus_uminus_id)

lemma trail_less_comp_rightI: "L ∈ set Ls ⟹ trail_less Ls L (- L)"
  by (metis in_set_conv_nth le_eq_less_or_eq trail_less_def trail_less_id_comp_def)

lemma trail_less_comp_leftI:
  fixes Ls :: "('a :: uminus) list"
  assumes uminus_uminus_id: "⋀x :: 'a. - (- x) = x"
  shows "- L ∈ set Ls ⟹ trail_less Ls (- L) L"
  by (rule trail_less_comp_rightI[of "- L", unfolded uminus_uminus_id])


subsection ‹Well-Defined›

lemma trail_less_id_id_well_defined:
  assumes
    pairwise_distinct: "∀x ∈ set Ls. ∀y ∈ set Ls. x ≠ - y" and
    L_le_K: "trail_less_id_id Ls L K"
  shows
    "¬ trail_less_id_comp Ls L K"
    "¬ trail_less_comp_id Ls L K"
    "¬ trail_less_comp_comp Ls L K"
  using L_le_K
  unfolding trail_less_id_id_def trail_less_comp_id_def trail_less_id_comp_def
    trail_less_comp_comp_def
  using pairwise_distinct[rule_format, OF nth_mem nth_mem]
  by metis+

lemma trail_less_id_comp_well_defined:
  assumes
    pairwise_distinct: "∀x ∈ set Ls. ∀y ∈ set Ls. x ≠ - y" and
    L_le_K: "trail_less_id_comp Ls L K"
  shows
    "¬ trail_less_id_id Ls L K"
    "¬ trail_less_comp_id Ls L K"
    "¬ trail_less_comp_comp Ls L K"
  using L_le_K
  unfolding trail_less_id_id_def trail_less_comp_id_def trail_less_id_comp_def
    trail_less_comp_comp_def
  using pairwise_distinct[rule_format, OF nth_mem nth_mem]
  by metis+

lemma trail_less_comp_id_well_defined:
  assumes
    pairwise_distinct: "∀x ∈ set Ls. ∀y ∈ set Ls. x ≠ - y" and
    L_le_K: "trail_less_comp_id Ls L K"
  shows
    "¬ trail_less_id_id Ls L K"
    "¬ trail_less_id_comp Ls L K"
    "¬ trail_less_comp_comp Ls L K"
  using L_le_K
  unfolding trail_less_id_id_def trail_less_comp_id_def trail_less_id_comp_def
    trail_less_comp_comp_def
  using pairwise_distinct[rule_format, OF nth_mem nth_mem]
  by metis+

lemma trail_less_comp_comp_well_defined:
  assumes
    pairwise_distinct: "∀x ∈ set Ls. ∀y ∈ set Ls. x ≠ - y" and
    L_le_K: "trail_less_comp_comp Ls L K"
  shows
    "¬ trail_less_id_id Ls L K"
    "¬ trail_less_id_comp Ls L K"
    "¬ trail_less_comp_id Ls L K"
  using L_le_K
  unfolding trail_less_id_id_def trail_less_comp_id_def trail_less_id_comp_def
    trail_less_comp_comp_def
  using pairwise_distinct[rule_format, OF nth_mem nth_mem]
  by metis+


subsection ‹Strict Partial Order›

lemma irreflp_trail_less:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
  shows "irreflp (trail_less Ls)"
proof (rule irreflpI, rule notI)
  fix L :: 'a
  assume "trail_less Ls L L"
  then show False
    unfolding trail_less_def
  proof (elim disjE)
    show "trail_less_id_id Ls L L ⟹ False"
      unfolding trail_less_id_id_def
      using pairwise_distinct by fastforce
  next
    show "trail_less_comp_id Ls L L ⟹ False"
      unfolding trail_less_comp_id_def
      by (metis pairwise_distinct uminus_not_id)
  next
    show "trail_less_id_comp Ls L L ⟹ False"
      unfolding trail_less_id_comp_def
      by (metis pairwise_distinct uminus_not_id)
  next
    show "trail_less_comp_comp Ls L L ⟹ False"
      unfolding trail_less_comp_comp_def
      by (metis pairwise_distinct uminus_uminus_id nat_less_le)
  qed
qed

lemma transp_trail_less:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
  shows "transp (trail_less Ls)"
proof (rule transpI)
  fix L K H :: 'a
  show "trail_less Ls L K ⟹ trail_less Ls K H ⟹ trail_less Ls L H"
    using pairwise_distinct[rule_format] uminus_not_id uminus_uminus_id
    unfolding trail_less_def trail_less_id_id_def trail_less_comp_id_def
      trail_less_id_comp_def trail_less_comp_comp_def
    (* Approximately 3 seconds on AMD Ryzen 7 PRO 5850U CPU. *)
    by (smt (verit, best) le_eq_less_or_eq order.strict_trans)
qed

lemma asymp_trail_less:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
  shows "asymp (trail_less Ls)"
  using irreflp_trail_less[OF assms] transp_trail_less[OF assms]
  using asymp_on_iff_irreflp_on_if_transp_on
  by auto


subsection ‹Strict Total (w.r.t. Elements in Trail) Order›

lemma totalp_on_trail_less:
  "totalp_on (set Ls ∪ uminus ` set Ls) (trail_less Ls)"
proof (rule totalp_onI, unfold Un_iff, elim disjE)
  fix L K
  assume "L ∈ set Ls" and "K ∈ set Ls" and "L ≠ K"
  then obtain i j where "i < length Ls" "Ls ! i = L" "j < length Ls" "Ls ! j = K"
    unfolding in_set_conv_nth by auto
  thus "trail_less Ls L K ∨ trail_less Ls K L"
    using ‹L ≠ K› less_linear[of i j]
    by (meson trail_less_def trail_less_id_id_def)
next
  fix L K
  assume "L ∈ set Ls" and "K ∈ uminus ` set Ls" and "L ≠ K"
  then obtain i j where "i < length Ls" "Ls ! i = L" "j < length Ls" "- (Ls ! j) = K"
    unfolding in_set_conv_nth image_set length_map by auto
  thus "trail_less Ls L K ∨ trail_less Ls K L"
    using  less_linear[of i j]
    by (metis le_eq_less_or_eq trail_less_comp_id_def trail_less_def trail_less_id_comp_def)
next
  fix L K
  assume "L ∈ uminus ` set Ls" and "K ∈ set Ls" and "L ≠ K"
  then obtain i j where "i < length Ls" "- (Ls ! i) = L" "j < length Ls" "Ls ! j = K"
    unfolding in_set_conv_nth image_set length_map by auto
  thus "trail_less Ls L K ∨ trail_less Ls K L"
    using less_linear[of i j]
    by (metis le_eq_less_or_eq trail_less_comp_id_def trail_less_def trail_less_id_comp_def)
next
  fix L K
  assume "L ∈ uminus ` set Ls" and "K ∈ uminus ` set Ls" and "L ≠ K"
  then obtain i j where "i < length Ls" "- (Ls ! i) = L" "j < length Ls" "- (Ls ! j) = K"
    unfolding in_set_conv_nth image_set length_map by auto
  thus "trail_less Ls L K ∨ trail_less Ls K L"
    using ‹L ≠ K› less_linear[of i j]
    by (metis trail_less_comp_comp_def trail_less_def)
qed


subsection ‹Well-Founded›

lemma not_trail_less_Cons_id_comp:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length (L # Ls). ∀j < length (L # Ls). i ≠ j ⟶
        (L # Ls) ! i ≠ (L # Ls) ! j ∧ (L # Ls) ! i ≠ - ((L # Ls) ! j)"
  shows "¬ trail_less (L # Ls) (- L) L"
proof (rule notI, unfold trail_less_def, elim disjE)
  show "trail_less_id_id (L # Ls) (- L) L ⟹ False"
    unfolding trail_less_id_id_def
    using pairwise_distinct uminus_not_id by metis
next
  show "trail_less_comp_id (L # Ls) (- L) L ⟹ False"
    unfolding trail_less_comp_id_def
    using pairwise_distinct uminus_uminus_id
    by (metis less_not_refl)
next
  show "trail_less_id_comp (L # Ls) (- L) L ⟹ False"
    unfolding trail_less_id_comp_def
    using pairwise_distinct uminus_not_id
    by (metis length_pos_if_in_set nth_Cons_0 nth_mem)
next
  show "trail_less_comp_comp (L # Ls) (- L) L ⟹ False"
    unfolding trail_less_comp_comp_def
    using pairwise_distinct uminus_not_id uminus_uminus_id by metis
qed

lemma not_trail_less_if_undefined:
  fixes L :: "'a :: uminus"
  assumes
    undefined: "L ∉ set Ls" "- L ∉ set Ls" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x"
  shows "¬ trail_less Ls L K" "¬ trail_less Ls K L"
  using undefined[unfolded in_set_conv_nth] uminus_uminus_id
  unfolding trail_less_def trail_less_id_id_def trail_less_comp_id_def
    trail_less_id_comp_def trail_less_comp_comp_def
  by (smt (verit))+

lemma trail_less_ConsD:
  fixes L H K :: "'a :: uminus"
  assumes uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    L_neq_K: "L ≠ K" and L_neq_minus_K: "L ≠ - K" and
    less_Cons: "trail_less (L # Ls) H K"
  shows "trail_less Ls H K"
  using less_Cons[unfolded trail_less_def]
proof (elim disjE)
  assume "trail_less_id_id (L # Ls) H K"
  hence "trail_less_id_id Ls H K"
    unfolding trail_less_id_id_def
    using L_neq_K less_Suc_eq_0_disj by fastforce
  thus ?thesis
    unfolding trail_less_def by simp
next
  assume "trail_less_comp_id (L # Ls) H K"
  hence "trail_less_comp_id Ls H K"
    unfolding trail_less_comp_id_def
    using L_neq_K less_Suc_eq_0_disj by fastforce
  thus ?thesis
    unfolding trail_less_def by simp
next
  assume "trail_less_id_comp (L # Ls) H K"
  hence "trail_less_id_comp Ls H K"
    unfolding trail_less_id_comp_def
    using L_neq_minus_K uminus_uminus_id less_Suc_eq_0_disj by fastforce
  thus ?thesis
    unfolding trail_less_def by simp
next
  assume "trail_less_comp_comp (L # Ls) H K"
  hence "trail_less_comp_comp Ls H K"
    unfolding trail_less_comp_comp_def
    using L_neq_minus_K uminus_uminus_id less_Suc_eq_0_disj by fastforce
  thus ?thesis
    unfolding trail_less_def by simp
qed

lemma trail_subset_empty_or_ex_smallest:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
  shows "Q ⊆ set Ls ∪ uminus ` set Ls ⟹ Q = {} ∨ (∃z ∈ Q. ∀y. trail_less Ls y z ⟶ y ∉ Q)"
  using pairwise_distinct
proof (induction Ls arbitrary: Q)
  case Nil
  thus ?case by simp
next
  case Cons_ind: (Cons L Ls)
  from Cons_ind.prems have pairwise_distinct_L_Ls:
    "∀i<length (L # Ls). ∀j<length (L # Ls). i ≠ j ⟶
      (L # Ls) ! i ≠ (L # Ls) ! j ∧ (L # Ls) ! i ≠ - (L # Ls) ! j"
    by simp
  hence pairwise_distinct_Ls:
    "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
    by (metis distinct.simps(2) distinct_conv_nth length_Cons not_less_eq nth_Cons_Suc)
  show ?case
  proof (cases "Q = {}")
    case True
    thus ?thesis by simp
  next
    case Q_neq_empty: False
    have Q_minus_subset: "Q - {L, - L} ⊆ set Ls ∪ uminus ` set Ls" using Cons_ind.prems(1) by auto

    have irreflp_gt_L_Ls: "irreflp (trail_less (L # Ls))"
      by (rule irreflp_trail_less[OF uminus_not_id uminus_uminus_id pairwise_distinct_L_Ls])

    have "∃z∈Q. ∀y. trail_less (L # Ls) y z ⟶ y ∉ Q"
      using Cons_ind.IH[OF Q_minus_subset pairwise_distinct_Ls]
    proof (elim disjE bexE)
      assume "Q - {L, -L} = {}"
      with Q_neq_empty have "Q ⊆ {L, -L}" by simp
      have ?thesis if "L ∈ Q"
        apply (intro bexI[OF _ ‹L ∈ Q›] allI impI)
        apply (erule contrapos_pn)
        apply (drule set_rev_mp[OF _ ‹Q ⊆ {L, -L}›])
        apply simp
        using irreflp_gt_L_Ls[THEN irreflpD, of L]
        using not_trail_less_Cons_id_comp[OF uminus_not_id uminus_uminus_id
            pairwise_distinct_L_Ls]
        by fastforce
      moreover have ?thesis if "L ∉ Q"
      proof -
        from ‹L ∉ Q› have "Q = {- L}"
          using Q_neq_empty ‹Q ⊆ {L, -L}› by auto
        thus ?thesis
          using irreflp_gt_L_Ls[THEN irreflpD, of "- L"] by auto
      qed
      ultimately show ?thesis by metis
    next
      fix K
      assume K_in_Q_minus: "K ∈ Q - {L, -L}" and "∀y. trail_less Ls y K ⟶ y ∉ Q - {L, -L}"
      from K_in_Q_minus have "L ≠ K" "- L ≠ K" by auto
      from K_in_Q_minus have "L ≠ - K" using ‹- L ≠ K› uminus_uminus_id by blast
      show ?thesis
      proof (intro bexI allI impI)
        show "K ∈ Q"
          using K_in_Q_minus by simp
      next
        fix H
        assume "trail_less (L # Ls) H K"
        hence "trail_less Ls H K"
          by (rule trail_less_ConsD[OF uminus_uminus_id ‹L ≠ K› ‹L ≠ - K›])
        hence "H ∉ Q - {L, -L}"
          using ‹∀y. trail_less Ls y K ⟶ y ∉ Q - {L, -L}› by simp
        moreover have "H ≠ L ∧  H ≠ - L"
          using uminus_uminus_id pairwise_distinct_L_Ls ‹trail_less Ls H K›
          by (metis (no_types, lifting) distinct.simps(2) distinct_conv_nth in_set_conv_nth
              list.set_intros(1,2) not_trail_less_if_undefined(1))
        ultimately show "H ∉ Q"
          by simp
      qed
    qed
    thus ?thesis by simp
  qed
qed

lemma wfP_trail_less:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)"
  shows "wfP (trail_less Ls)"
  unfolding wfp_eq_minimal
proof (intro allI impI)
  fix M :: "'a set" and L :: 'a
  assume "L ∈ M"
  show "∃z ∈ M. ∀y. trail_less Ls y z ⟶ y ∉ M"
  proof (cases "M ∩ (set Ls ∪ uminus ` set Ls) = {}")
    case True
    with ‹L ∈ M› have L_not_in_Ls: "L ∉ set Ls ∧ - L ∉ set Ls"
      unfolding disjoint_iff by (metis UnCI image_eqI uminus_uminus_id)
    then show ?thesis
    proof (intro bexI[OF _ ‹L ∈ M›] allI impI)
      fix K
      assume "trail_less Ls K L"
      hence False
        using L_not_in_Ls not_trail_less_if_undefined[OF _ _ uminus_uminus_id] by simp
      thus "K ∉ M" ..
    qed
  next
    case False
    hence "M ∩ (set Ls ∪ uminus ` set Ls) ⊆ set Ls ∪ uminus ` set Ls"
      by simp
    with False obtain H where
      H_in: "H ∈ M ∩ (set Ls ∪ uminus ` set Ls)" and
      all_lt_H_no_in: "∀y. trail_less Ls y H ⟶ y ∉ M ∩ (set Ls ∪ uminus ` set Ls)"
      using trail_subset_empty_or_ex_smallest[OF uminus_not_id uminus_uminus_id pairwise_distinct]
      by meson
    show ?thesis
    proof (rule bexI)
      show "H ∈ M" using H_in by simp
    next
      show "∀y. trail_less Ls y H ⟶ y ∉ M"
        using all_lt_H_no_in uminus_uminus_id
        by (metis Int_iff Un_iff image_eqI not_trail_less_if_undefined(1))
    qed
  qed
qed


subsection ‹Extension on All Literals›

definition trail_less_ex where
  "trail_less_ex lt Ls L K ⟷
    (if L ∈ set Ls ∨ - L ∈ set Ls then
      if K ∈ set Ls ∨ - K ∈ set Ls then
        trail_less Ls L K
      else
        True
    else
      if K ∈ set Ls ∨ - K ∈ set Ls then
        False
      else
        lt L K)"

lemma
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x"
  shows "K ∈ set Ls ∨ - K ∈ set Ls ⟹ trail_less_ex lt Ls L K ⟷ trail_less Ls L K"
  using not_less_if_undefined[OF uminus_uminus_id]
  by (simp add: trail_less_ex_def)

lemma trail_less_ex_if_trail_less:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x"
  shows "trail_less Ls L K ⟹ trail_less_ex lt Ls L K"
  unfolding trail_less_ex_def
  using defined_if_trail_less[THEN defined_conv[OF uminus_uminus_id, THEN iffD1]]
  by auto

lemma
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x"
  shows "L ∈ set Ls ∪ uminus ` set Ls ⟹ K ∉ set Ls ∪ uminus ` set Ls ⟹ trail_less_ex lt Ls L K"
  using defined_conv uminus_uminus_id
  by (auto simp add: trail_less_ex_def)
  

lemma irreflp_trail_ex_less:
  fixes Ls :: "('a :: uminus) list" and lt :: "'a ⇒ 'a ⇒ bool"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)" and
    irreflp_lt: "irreflp lt"
  shows "irreflp (trail_less_ex lt Ls)"
  unfolding trail_less_ex_def
  using irreflp_trail_less[OF uminus_not_id uminus_uminus_id pairwise_distinct] irreflp_lt
  by (simp add: irreflpD irreflpI)

lemma transp_trail_less_ex:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)" and
    transp_lt: "transp lt"
  shows "transp (trail_less_ex lt Ls)"
  unfolding trail_less_ex_def
  using transp_trail_less[OF uminus_not_id uminus_uminus_id pairwise_distinct] transp_lt
  by (smt (verit, ccfv_SIG) transp_def)

lemma asymp_trail_less_ex:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)" and
    asymp_lt: "asymp lt"
  shows "asymp (trail_less_ex lt Ls)"
  unfolding trail_less_ex_def
  using asymp_trail_less[OF uminus_not_id uminus_uminus_id pairwise_distinct] asymp_lt
  by (auto intro: asympI dest: asympD)

lemma totalp_on_trail_less_ex:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    totalp_on_lt: "totalp_on A lt"
  shows "totalp_on (A ∪ set Ls ∪ uminus ` set Ls) (trail_less_ex lt Ls)"
  using totalp_on_trail_less[of Ls]
  using totalp_on_lt
  unfolding trail_less_ex_def
  by (smt (verit, best) Un_iff defined_conv totalp_on_def uminus_uminus_id)


subsubsection ‹Well-Founded›

lemma wfP_trail_less_ex:
  fixes Ls :: "('a :: uminus) list"
  assumes
    uminus_not_id: "⋀x :: 'a. - x ≠ x" and
    uminus_uminus_id: "⋀x :: 'a. - (- x) = x" and
    pairwise_distinct:
      "∀i < length Ls. ∀j < length Ls. i ≠ j ⟶ Ls ! i ≠ Ls ! j ∧ Ls ! i ≠ - (Ls ! j)" and
    wfP_lt: "wfP lt"
  shows "wfP (trail_less_ex lt Ls)"
  unfolding wfp_eq_minimal
proof (intro allI impI)
  fix Q :: "'a set" and x :: 'a
  assume "x ∈ Q"
  show "∃z∈Q. ∀y. trail_less_ex lt Ls y z ⟶ y ∉ Q "
  proof (cases "Q ∩ (set Ls ∪ uminus ` set Ls) = {}")
    case True
    then show ?thesis
      using wfP_lt[unfolded wfp_eq_minimal, rule_format, OF ‹x ∈ Q›]
      by (metis (no_types, lifting) defined_conv disjoint_iff trail_less_ex_def uminus_uminus_id)
  next
    case False
    then show ?thesis
      using trail_subset_empty_or_ex_smallest[OF uminus_not_id uminus_uminus_id pairwise_distinct,
        unfolded wfp_eq_minimal, of "Q ∩ (set Ls ∪ uminus ` set Ls)", simplified]
      by (metis (no_types, lifting) IntD1 IntD2 UnE defined_conv trail_less_ex_def uminus_uminus_id)
  qed
qed


subsection ‹Alternative only for terms›


(* definition trail_term_less where
  "trail_term_less ts = (λt1 t2. ∃i. Suc i < length ts ∧ t1 = ts ! Suc i ∧ t2 = ts ! i)⇧+⇧+"

lemma transp_trail_term_less: "transp (trail_term_less ts)"
proof (rule transpI)
  fix t1 t2 t3
  assume "trail_term_less ts t1 t2" and "trail_term_less ts t2 t3"
  then show "trail_term_less ts t1 t3"
    by (simp add: trail_term_less_def)
qed *)

definition trail_term_less where
  "trail_term_less ts t1 t2 ⟷ (∃i < length ts. ∃j < i. t1 = ts ! i ∧ t2 = ts ! j)"

lemma transp_trail_term_less:
  assumes "distinct ts"
  shows "transp (trail_term_less ts)"
  by (rule transpI)
    (smt (verit, ccfv_SIG) Suc_lessD assms less_trans_Suc nth_eq_iff_index_eq trail_term_less_def)

lemma asymp_trail_term_less:
  assumes "distinct ts"
  shows "asymp (trail_term_less ts)"
  by (rule asympI)
    (metis assms distinct_Ex1 dual_order.strict_trans nth_mem order_less_imp_not_less
      trail_term_less_def)

lemma irreflp_trail_term_less:
  assumes "distinct ts"
  shows "irreflp (trail_term_less ts)"
  using assms irreflp_on_if_asymp_on[OF asymp_trail_term_less] by metis

lemma totalp_on_trail_term_less:
  shows "totalp_on (set ts) (trail_term_less ts)"
  by (rule totalp_onI) (metis in_set_conv_nth nat_neq_iff trail_term_less_def)

lemma wfP_trail_term_less:
  assumes "distinct ts"
  shows "wfP (trail_term_less ts)"
proof (rule wfP_if_convertible_to_nat)
  fix t1 t2 assume "trail_term_less ts t1 t2"
  then obtain i j where "i<length ts" and "j<i" and "t1 = ts ! i" and "t2 = ts ! j"
    unfolding trail_term_less_def by auto
  then show "index (rev ts) t1 < index (rev ts) t2"
    using assms diff_commute index_nth_id index_rev by fastforce
qed

lemma trail_term_less_Cons_if_mem:
  assumes "y ∈ set xs"
  shows "trail_term_less (x # xs) y x"
proof -
  from assms obtain i where "i < length xs" and "xs ! i = y"
    by (meson in_set_conv_nth)
  thus ?thesis
    unfolding trail_term_less_def
  proof (intro exI conjI)
    show "Suc i < length (x # xs)"
      using ‹i < length xs› by simp
  next
    show "0 < Suc i"
      by simp
  next
    show "y = (x # xs) ! Suc i"
      using ‹xs ! i = y› by simp
  next
    show "x = (x # xs) ! 0"
      by simp
  qed
qed

end