# 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"
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"
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"
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"
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"
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"
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"
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"
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]

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

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

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"
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```