Theory Alpha_Beta_Linear

chapter ‹Linear Orders›

theory Alpha_Beta_Linear
imports
  "HOL-Library.Extended_Real" (* for quickcheck purposes *)
begin

section ‹Classes›

notation
  bot (‹⊥›) and
  top (‹⊤›)

class bounded_linorder = linorder + order_top + order_bot
begin

lemma bounded_linorder_collapse:
assumes "¬ ⊥ < ⊤" shows "(x::'a) = y"
proof -
  from assms have "⊤ ≤ ⊥" by(rule leI)
  have "x = ⊤" using order.trans[OF ‹⊤ ≤ ⊥› bot_least[of x]] top_unique by metis
  moreover
  have "y = ⊤" using order.trans[OF ‹⊤ ≤ ⊥› bot_least[of y]] top_unique by metis
  ultimately show ?thesis by blast
qed

end

class de_morgan_order = bounded_linorder + uminus +
assumes de_morgan_min: "- min x y = max (- x) (- y)"
assumes neg_neg[simp]: "- (- x) = x"
begin

lemma de_morgan_max: "- max x y = min (- x) (- y)"
by (metis de_morgan_min neg_neg)

lemma neg_top[simp]: "- ⊤ = ⊥"
by (metis de_morgan_max max_top2 min_bot neg_neg)

lemma neg_bot[simp]: "- ⊥ = ⊤"
using neg_neg neg_top by blast

lemma uminus_eq_iff[simp]: "-a = -b ⟷ a = b"
by (metis neg_neg)

lemma uminus_le_reorder: "(- a ≤ b) = (- b ≤ a)"
by (metis de_morgan_max max.absorb_iff1 min.absorb_iff1 neg_neg)

lemma uminus_less_reorder: "(- a < b) = (- b < a)"
by (metis order.strict_iff_not neg_neg uminus_le_reorder)

lemma minus_le_minus[simp]: "- a ≤ - b ⟷ b ≤ a"
by (metis neg_neg uminus_le_reorder)

lemma minus_less_minus[simp]: "- a < - b ⟷ b < a"
by (metis neg_neg uminus_less_reorder)

lemma less_uminus_reorder: "a < - b ⟷ b < - a"
by (metis neg_neg uminus_less_reorder)

end

(* For quickcheck: *)

instance bool :: bounded_linorder ..

instantiation ereal :: de_morgan_order
begin

instance
proof (standard, goal_cases)
  case 1
  thus ?case
    by (simp add: max_def)
next
  case 2
  thus ?case by (simp add: min_def)
qed

end


section ‹Game Tree Evaluation›

datatype 'a tree = Lf 'a | Nd "'a tree list"

datatype_compat tree

fun maxs :: "('a::bounded_linorder) list ⇒ 'a" where
"maxs [] = ⊥" |
"maxs (x#xs) = max x (maxs xs)"

fun mins :: "('a::bounded_linorder) list ⇒ 'a"where
"mins [] = ⊤" |
"mins (x#xs) = min x (mins xs)"

fun maxmin :: "('a::bounded_linorder) tree ⇒ 'a"
and minmax :: "('a::bounded_linorder) tree ⇒ 'a" where
"maxmin (Lf x) = x" |
"maxmin (Nd ts) = maxs (map minmax ts)" |
"minmax (Lf x) = x" |
"minmax (Nd ts) = mins (map maxmin ts)"

text ‹Cannot use @{const Max} instead of ‹maxs› because @{term "Max {}"} is undefined.›

text ‹No need for bounds if lists are nonempty:›

fun invar :: "'a tree ⇒ bool" where
"invar (Lf x) = True" |
"invar (Nd ts) = (ts ≠ [] ∧ (∀t ∈ set ts. invar t))"

fun maxs1 :: "('a::linorder) list ⇒ 'a" where
"maxs1 [x] = x" |
"maxs1 (x#xs) = max x (maxs1 xs)"

fun mins1 :: "('a::linorder) list ⇒ 'a"where
"mins1 [x] = x" |
"mins1 (x#xs) = min x (mins1 xs)"

fun maxmin1 :: "('a::bounded_linorder) tree ⇒ 'a"
and minmax1 :: "('a::bounded_linorder) tree ⇒ 'a" where
"maxmin1 (Lf x) = x" |
"maxmin1 (Nd ts) = maxs1 (map minmax1 ts)" |
"minmax1 (Lf x) = x" |
"minmax1 (Nd ts) = mins1 (map maxmin1 ts)"

lemma maxs1_maxs: "xs ≠ [] ⟹ maxs1 xs = maxs xs"
by(induction xs rule: maxs1.induct) auto

lemma mins1_mins: "xs ≠ [] ⟹ mins1 xs = mins xs"
by(induction xs rule: mins1.induct) auto

lemma maxmin1_maxmin:
shows "invar t ⟹ maxmin1 t = maxmin t"
and   "invar t ⟹ minmax1 t = minmax t"
proof(induction t rule: maxmin1_minmax1.induct)
  case 2 thus ?case by (simp add: maxs1_maxs cong: map_cong)
next
  case 4 thus ?case by (simp add: mins1_mins cong: map_cong)
qed auto


subsection ‹Parameterized by the orderings›

fun maxs_le :: "'a ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a" where
"maxs_le bo le [] = bo" |
"maxs_le bo le (x#xs) = (let m = maxs_le bo le xs in if le x m then m else x)"

fun maxmin_le :: "'a ⇒ 'a ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a tree ⇒ 'a" where
"maxmin_le _  _ _ (Lf x) = x" |
"maxmin_le bo to le (Nd ts) = maxs_le bo le (map (maxmin_le to bo (λx y. le y x)) ts)"

lemma maxs_le_maxs: "maxs_le ⊥ (≤) xs = maxs xs"
by(induction xs) (auto simp: Let_def)

lemma maxs_le_mins: "maxs_le ⊤ (≥) xs = mins xs"
by(induction xs) (auto simp: Let_def)

lemma maxmin_le_maxmin:
  shows "maxmin_le ⊥ ⊤ (≤) t = maxmin  t"
  and   "maxmin_le ⊤ ⊥ (≥) t = minmax t"
by(induction t and t rule: maxmin_minmax.induct)
  (auto simp add: Let_def max_def maxs_le_maxs maxs_le_mins cong: map_cong)


subsection ‹Negamax: de Morgan orders›

fun negmax :: "('a::de_morgan_order) tree ⇒ 'a" where
"negmax (Lf x) = x" |
"negmax (Nd ts) = maxs (map (λt. - negmax t) ts)"

lemma de_morgan_mins:
fixes f :: "'a ⇒ 'b::de_morgan_order"
shows "- mins (map f xs) = maxs (map (λx. - f x) xs)"
by(induction xs)(auto simp: de_morgan_min)

fun negate :: "bool ⇒ ('a::de_morgan_order) tree ⇒ ('a::de_morgan_order) tree" where
"negate b (Lf x) = Lf (if b then -x else x)" |
"negate b (Nd ts) = Nd (map (negate (¬b)) ts)"

lemma negate_negate: "negate f (negate f t) = t"
by(induction t arbitrary: f)(auto cong: map_cong)

lemma maxmin_negmax: "maxmin t = negmax (negate False t)"
and  minmax_negmax: "minmax t = - negmax (negate True t)"
by(induction t and t rule: maxmin_minmax.induct)
  (auto simp flip: de_morgan_mins cong: map_cong)

(* verbose only for presentation reasons (book) *)
lemma "maxmin t = negmax (negate False t)"
and  "minmax t = - negmax (negate True t)"
proof(induction t and t rule: maxmin_minmax.induct)
  case (2 ts)
  have "maxmin (Nd ts) = maxs (map minmax ts)"
    by simp
  also have "… = maxs (map (λt. - negmax (negate True t)) ts)"
    using "2.IH" by (simp cong: map_cong)
  also have "… = maxs (map ((λt. - negmax t) o (negate True)) ts)"
    by (metis comp_apply)
  also have "… = maxs (map (λt. - negmax t) (map (negate True) ts))"
    by(simp)
  also have "… = negmax (Nd (map (negate True) ts))"
    by simp
  also have "… = negmax (negate False (Nd ts))"
    by simp
  finally show ?case .
next
  case (4 ts)
  have "minmax (Nd ts) = mins (map maxmin ts)"
    by simp
  also have "… = mins (map (λt. negmax (negate False t)) ts)"
    using "4.IH" by (simp cong: map_cong)
  also have "… = - (- mins (map (λt. negmax (negate False t)) ts))"
    by simp
  also have "… = - maxs (map (λt. - negmax (negate False t)) ts)"
    by(simp only: de_morgan_mins)
  also have "… = - maxs (map ((λt. - negmax t) o (negate False)) ts)"
    by (metis comp_apply)
  also have "… = - maxs (map (λt. - negmax t) (map (negate False) ts))"
    by(simp)
  also have "… = - negmax (Nd (map (negate False) ts))"
    by simp
  also have "… = - negmax (negate True (Nd ts))"
    by simp
  finally show ?case .
qed (auto)

lemma shows negmax_maxmin: "negmax t = maxmin(negate False t)"
and "negmax t = - minmax(negate True t)"
  apply (simp add: maxmin_negmax negate_negate)
  by (simp add: minmax_negmax negate_negate)
(* verbose
proof(induction t and t rule: maxmin_minmax.induct)
  case (2 ts) (* verbose only for presentation reasons (book) *)
  have "negmax(Nd ts) = maxs (map (λt. - negmax t) ts)" by simp
  also have "… = maxs (map (λt. - (- minmax (negate True t))) ts)"
    using "2.IH" by (simp cong: map_cong)
  also have "… = maxs (map (λt. minmax (negate True t)) ts)" by simp
  also have "… = maxs (map (minmax o negate True) ts)"
    by (metis comp_apply)
  also have "… = maxs (map minmax (map (negate True) ts))"
    by simp
  also have "… = maxmin (Nd (map (negate True) ts))"
    by (rule maxmin.simps(2)[symmetric])
  also have "… = maxmin (negate False (Nd ts))" by simp
  finally show ?case .
next
  case (4 ts) (* verbose only for presentation reasons (book) *)
  have "negmax(Nd ts) = maxs (map (λt. - negmax t) ts)" by simp
  also have "… = maxs (map (λt. - maxmin (negate False t)) ts)"
    using "4.IH" by (simp cong: map_cong)
  also have "… = - mins (map (λt. maxmin (negate False t)) ts)" by(simp add: de_morgan_mins)
  also have "… = - mins (map (maxmin o negate False) ts)"
    by (metis comp_apply)
  also have "… = - mins (map maxmin (map (negate False) ts))"
    by simp
  also have "… = - minmax (Nd (map (negate False) ts))"
    by (simp)
  also have "… = - minmax (negate True (Nd ts))" by simp
  finally show ?case .
qed (auto simp add: de_morgan_mins cong: map_cong) (* could prove every case *)
*)

lemma maxs_append: "maxs (xs @ ys) = max (maxs xs) (maxs ys)"
by(induction xs) (auto simp: max.assoc)

lemma maxs_rev: "maxs (rev xs) = maxs xs"
by(induction xs) (auto simp: max.commute maxs_append)


section "Specifications"


subsection "The squash operator ‹max a (min x b)›"

abbreviation mm where "mm a x b == min (max a x) b"

lemma max_min_commute: "(a::_::linorder) ≤ b ⟹ max a (min x b) = min b (max x a)"
by (metis max.absorb2 max.commute min.commute max_min_distrib1)

lemma max_min_commute2: "(a::_::linorder) ≤ b ⟹ max a (min x b) = min (max a x) b"
by (metis max.absorb2 max.commute max_min_distrib1)

lemma max_min_neg: "a<b ⟹ max (a::_::de_morgan_order) (min x b) = - max (-b) (min (-x) (-a))"
by(simp add: max_min_commute de_morgan_min de_morgan_max)


subsection ‹Fail-Hard and Soft›

text ‹Specification of fail-hard; symmetric in ‹x› and ‹y›!›
abbreviation
 "knuth (a::_::linorder) b x y ==
  ((y ≤ a ⟶ x ≤ a) ∧ (a < y ∧ y < b ⟶ y = x) ∧ (b ≤ y ⟶ b ≤ x))"

abbreviation knuth2 :: "('a::linorder) ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" (‹(_ ≅/ _/ '(mod _,_'))› [51,51,0,0])
where "knuth2 x y a b ≡ knuth a b x y"

notation (latex output) knuth2 (‹(_ ≅/ _/ '(\<^latex>‹\textup{mod}› _,_'))› [51,51,0,0])

lemma knuth_bot_top: "knuth ⊥ ⊤ x y ⟹ x = (y::_::bounded_linorder)"
by (metis bot.extremum_uniqueI linorder_le_less_linear top.extremum_uniqueI)

text ‹The equational version of @{const knuth}. First, automatically:›

lemma knuth_iff_max_min: "a < b ⟹ knuth a b x y ⟷ max a (min x b) = max a (min y b)"
by (smt (verit) linorder_not_le max.absorb4 max_min_distrib2 max_min_same(1) min.absorb_iff2)

text ‹Needs ‹a < b›: take everything = ‹∞›, x = 0›
lemma knuth_if_mm: "a < b ⟹ mm a y b = mm a x b ⟹ knuth a b x y"
by (smt (verit, del_insts) le_max_iff_disj min_def nle_le nless_le)

lemma mm_if_knuth: "knuth a b y x ⟹ mm a y b = mm a x b"
by (metis leI max.orderE min.absorb_iff2 min_max_distrib1)

text ‹Now readable:›

lemma mm_iff_knuth: assumes "(a::_::linorder) < b"
shows "max a (min x b) = max a (min y b) ⟷ knuth a b y x" (is "?mm = ?h")
proof -
  have "max a (min x b) = max a (min y b) ⟷
    (min x b ≤ a ⟷ min y b ≤ a) ∧ (a < min x b ⟶ min x b = min y b)"
    by (metis linorder_not_le max_def nle_le)
  also have "… ⟷ (x ≤ a ⟷ y ≤ a) ∧ (a < x ⟶ min x b = min y b)"
    using assms apply (simp add: linorder_not_le) by (metis leD min_le_iff_disj)
  also have "… ⟷ (x ≤ a ⟷ y ≤ a) ∧ (a < x ⟶ (b ≤ x ⟷ b ≤ y) ∧ (x < b ⟶ x=y))"
    by (metis leI min.strict_order_iff min_absorb2)
  also have "… ⟷ (x ≤ a ⟷ y ≤ a) ∧ (a < x ⟶ (b ≤ x ⟷ b ≤ y)) ∧ (a < x ∧ x < b ⟶ x=y)"
    by blast
  also have "… ⟷ (x ≤ a ⟷ y ≤ a) ∧ (b ≤ x ⟷ b ≤ y) ∧ (a < x ∧ x < b ⟶ x=y)"
    using assms dual_order.strict_trans2 linorder_not_less by blast
  also have "… ⟷ (x ≤ a ⟶ y ≤ a) ∧ (x ≥ b ⟶ y ≥ b) ∧ (a < x ∧ x < b ⟶ x=y)"
    by (metis assms order.strict_trans linorder_le_less_linear nless_le)
  finally show ?thesis by blast
qed

corollary mm_iff_knuth': "a < b ⟹ max a (min x b) = max a (min y b) ⟷ knuth a b x y"
using mm_iff_knuth by (metis mm_iff_knuth)

(*text ‹Even in latex (relic)›
text‹
\begin{lemma}
@{thm [mode=iffSpace,break,margin=70] mm_iff_knuth}
\end{lemma}

\begin{proofx} We assume @{prop "a < b"} and prove the equivalence:
\begin{quote}
@{prop "max a (min x b) = max a (min y b)"}\\
‹⟷› ‹(›@{prop [mode=iff]"(min x b ≤ a ⟷ min y b ≤ a)"}‹) ∧›\\
\mbox{}\qquad\ ‹(›@{prop "(a < min x b ⟶ min x b = min y b)"}‹)›
\hfill by def.\ of @{const max}\\
‹⟷› ‹(›@{prop [mode=iff]"(x ≤ a ⟷ y ≤ a)"}‹) ∧›\\
\mbox{}\qquad\ ‹(›@{prop "(a < x ⟶ min x b = min y b)"}‹)›
\hfill by @{prop "a < b"} and def.\ of @{const min}\\
‹⟷› ‹(›@{prop [mode=iff]"(x ≤ a ⟷ y ≤ a)"}‹) ∧›\\
\mbox{}\qquad\ ‹(›@{prop [mode=iff]"(a < x ⟶ (b ≤ x ⟷ b ≤ y) ∧ (x < b ⟶ x=y))"}‹)›
  \hfill by def.\ of @{const min}\\
‹⟷› ‹(›@{prop [mode=iff]"(x ≤ a ⟷ y ≤ a)"}‹) ∧›\\
\mbox{}\qquad\ @{prop [mode=iff]"(a < x ⟶ (b ≤ x ⟷ b ≤ y)) ∧ (a < x ∧ x < b ⟶ x=y)"}\\
‹⟷› ‹(›@{prop [mode=iff]"(x ≤ a ⟷ y ≤ a)"}‹) ∧›\\
\mbox{}\qquad\ @{prop [mode=iff]"(b ≤ x ⟷ b ≤ y) ∧ (a < x ∧ x < b ⟶ x=y)"}
 \hfill by @{prop "a < b"}\\
‹⟷› ‹(›@{prop "(x ≤ a ⟶ y ≤ a)"}‹) ∧›\\
\mbox{}\qquad\ @{prop "(b ≤ x ⟶ b ≤ y) ∧ (a < x ∧ x < b ⟶ x=y)"}
 \hfill by @{prop "a < b"}\\
‹⟷› @{prop "(x ≤ a ⟶ y ≤ a) ∧ (b ≤ x ⟶ b ≤ y) ∧ (a < x ∧ x < b ⟶ x=y)"}
\end{quote}
where the final step follows from linearity and @{prop "a < b"}.
\end{proofx}
›
*)

corollary knuth_comm: "a<b ⟹ knuth a b x y ⟷ knuth a b y x"
using mm_iff_knuth[of a b x y] mm_iff_knuth[of a b y x]
by metis


text ‹Specification of fail-soft: ‹v› is the actual value, ‹ab› the approximation.›
abbreviation
 "fishburn (a::_::linorder) b v ab ==
  ((ab ≤ a ⟶ v ≤ ab) ∧ (a < ab ∧ ab < b ⟶ ab = v) ∧ (b ≤ ab ⟶ ab ≤ v))"

abbreviation fishburn2 :: "('a::linorder) ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" (‹(_ ≤/ _/ '(mod _,_'))› [51,51,0,0])
where "fishburn2 ab v a b ≡ fishburn a b v ab"

notation (latex output) fishburn2 (‹(_ ≤/ _/ '(\<^latex>‹\textup{mod}› _,_'))› [51,51,0,0])

lemma fishburn_iff_min_max: "a < b ⟹ fishburn a b v ab ⟷ min v b ≤ ab ∧ ab ≤ max v a"
by (metis (full_types) le_max_iff_disj linorder_not_le min_le_iff_disj nle_le)

lemma knuth_if_fishburn: "fishburn a b x y ⟹ knuth a b x y"
using order_trans by blast

corollary fishburn_bot_top: "fishburn ⊥ ⊤ (x::_::bounded_linorder) y ⟹ x = y"
by (metis bot.extremum bot.not_eq_extremum nle_le top.not_eq_extremum top_greatest)

lemma trans_fishburn: "fishburn a b x y ⟹ fishburn a b y z ⟹ fishburn a b x z"
using order.trans by blast

text ‹An simple alternative formulation:›

lemma fishburn2: "a < b ⟹ fishburn a b f g = ((g > a ⟶ f ≥ g) ∧ (g < b ⟶ f ≤ g))"
by auto

text ‹Like ‹fishburn2› above, but exchanging ‹f› and ‹g›. Not clearly related to @{const knuth} and ‹fishburn›.›

abbreviation "lb_ub a b f g ≡ ((f ≥ a ⟶ g ≥ a) ∧ (f ≤ b ⟶ g ≤ b))"

lemma "(a::nat) < b ⟹ knuth a b f g ⟹ lb_ub a b f g"
quickcheck[expect=counterexample]
oops

lemma "(a::nat) < b ⟹ lb_ub a b f g ⟹ knuth a b f g"
quickcheck[expect=counterexample]
oops

lemma "fishburn a b f g ⟹ lb_ub a b f g"
by (metis order.trans nle_le)

lemma "(a::nat) < b ⟹ lb_ub a b f g ⟹ fishburn a b f g"
quickcheck[expect=counterexample]
oops

lemma "a<(b::int) ⟹ fishburn a b f g ⟹ fishburn a b g f"
quickcheck[expect=counterexample]
oops

lemma "a<(b::int) ⟹ knuth a b f g ⟹ fishburn a b f g"
quickcheck[expect=counterexample]
oops

lemma fishburn_trans: "fishburn a b f g ⟹ fishburn a b g h ⟹ fishburn a b f h"
by auto

text ‹Exactness: if the real value is within the bounds, ‹ab› is exact.
More interesting would be the other way around.
The impact of the exactness lemmas below is unclear.›

lemma fishburn_exact: "a ≤ v ∧ v ≤ b ⟹ fishburn a b v ab ⟹ ab = v"
by auto

text ‹Let everyting = 0 and ‹ab› = 1:›
lemma mm_not_exact: "a ≤ (v::bool) ∧ v ≤ b ⟹ mm a v b = mm a ab b ⟹ ab = v"
quickcheck[expect=counterexample]
oops
lemma knuth_not_exact: "a ≤ (v::ereal) ∧ v ≤ b ⟹ knuth a b v ab ⟹ ab = v"
quickcheck[expect=counterexample]
oops
lemma mm_not_exact: "a < b ⟹ (a::ereal) ≤ v ∧ v ≤ b ⟹ mm a v b = mm a ab b ⟹ ab = v"
quickcheck[expect=counterexample]
oops


section ‹Alpha-Beta for Linear Orders›


subsection ‹From the Left›


subsubsection ‹Hard›

fun ab_max :: "'a ⇒ 'a ⇒ ('a::linorder)tree ⇒ 'a" and ab_maxs ab_min ab_mins where
"ab_max a b (Lf x) = x" |
"ab_max a b (Nd ts) = ab_maxs a b ts" |

"ab_maxs a b [] = a" |
"ab_maxs a b (t#ts) = (let a' = max a (ab_min a b t) in if a' ≥ b then a' else ab_maxs a' b ts)" |

"ab_min a b (Lf x) = x" |
"ab_min a b (Nd ts) = ab_mins a b ts" |

"ab_mins a b [] = b" |
"ab_mins a b (t#ts) = (let b' = min b (ab_max a b t) in if b' ≤ a then b' else ab_mins a b' ts)"

lemma ab_maxs_ge_a: "ab_maxs a b ts ≥ a"
apply(induction ts arbitrary: a)
by (auto simp: Let_def)(use max.bounded_iff in blast)

lemma ab_mins_le_b: "ab_mins a b ts ≤ b"
apply(induction ts arbitrary: b)
by (auto simp: Let_def)(use min.bounded_iff in blast)

text ‹Automatic ‹fishburn› proof:›

theorem (*fishburn_ab_max_auto: no_atp *)
  shows "a < b ⟹ fishburn a b (maxmin t)   (ab_max a b t)"
    and "a < b ⟹ fishburn a b (maxmin (Nd ts)) (ab_maxs a b ts)"
    and "a < b ⟹ fishburn a b (minmax t)   (ab_min a b t)"
    and "a < b ⟹ fishburn a b (minmax (Nd ts)) (ab_mins a b ts)"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  case (4 a b t ts)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, del_insts) ab_maxs_ge_a le_max_iff_disj linorder_not_le nle_le)
next
  case (8 a b t ts)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, del_insts) ab_mins_le_b linorder_not_le min.bounded_iff nle_le)
qed auto

text ‹Detailed  ‹fishburn› proof:›

theorem fishburn_val_ab:
  shows "a < b ⟹ fishburn a b (maxmin t)   (ab_max a b t)"
    and "a < b ⟹ fishburn a b (maxmin (Nd ts)) (ab_maxs a b ts)"
    and "a < b ⟹ fishburn a b (minmax t)   (ab_min a b t)"
    and "a < b ⟹ fishburn a b (minmax (Nd ts)) (ab_mins a b ts)"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  case (4 a b t ts)
  let ?abt = "ab_min a b t" let ?a' = "max a ?abt" let ?abts = "ab_maxs ?a' b ts"
  let ?mmt = "minmax t" let ?mmts = "maxmin (Nd ts)"
  let ?abtts = "ab_maxs a b (t # ts)" let ?mmtts = "maxmin (Nd (t # ts))"
  note IH1 = "4.IH"(1)[OF ‹a<b›]

  have 1: "?mmtts ≤ ?abtts" if ab: "?abtts ≤ a"
  proof (cases "b ≤ ?a'")
    case True(*impossible*)
    note ‹a<b›
    also note True
    also have "?a' = ?abtts" using True by simp
    also note ‹… ≤ a›
    finally have False by simp
    thus ?thesis ..
  next
    case False
    hence IH2: "fishburn ?a' b ?mmts ?abts" using 4(2)[OF refl] ‹a<b› linorder_not_le by blast
    from False ab have ab: "?abts ≤ a" by(simp)
    have "?a' ≤ ?abts" by(rule ab_maxs_ge_a)
    (*In fact: ‹?abts = ?a' = a›*)
    hence "?mmt ≤ ?abt" using IH1 ab by (metis order.trans linorder_not_le max.absorb4)
    have "?abts ≤ ?a'" using ab le_max_iff_disj by blast
    have "?a' ≤ a" using ‹?a' ≤ ?abts› ab by(rule order.trans)
    hence "?mmts ≤ ?abts" using IH2 ‹?abts ≤ ?a'› by blast
    with ‹?mmt ≤ ?abt› show ?thesis using False ‹?a' ≤ ?abts› by(auto)
  qed

  have 2: "?abtts ≤ ?mmtts" if ab: "b ≤ ?abtts"
  proof (cases "b ≤ ?a'")
    case True
    hence "b ≤ ?abt" using ‹a<b› by (metis linorder_not_le max_less_iff_conj)
    hence "?abt ≤ ?mmt" using IH1 by blast
    moreover
    then have "a ≤ ?mmt" using ‹a<b› ‹b ≤ ?abt› by (simp)
    ultimately show ?thesis using True by (simp add: max.coboundedI1)
  next
    case False
    hence "b ≤ ?abts" using ab by simp
    hence "?abts ≤ ?mmts" using "4.IH"(2)[OF refl] False by (meson linorder_not_le)
    then show ?thesis using False by (simp add: le_max_iff_disj)
  qed

  have 3: "?abtts = ?mmtts" if ab: "a < ?abtts" "?abtts < b"
  proof (cases "b ≤ ?a'")
    case True(*impossible*)
    also have "?a' = ?abtts" using True by simp
    also note ab(2)
    finally have False by simp
    thus ?thesis ..
  next
    case False
    hence IH2: "fishburn ?a' b ?mmts ?abts" using 4(2)[OF refl] ‹a<b› linorder_not_le by blast
    have "?abtts = ?abts" using False by(simp)
    have "?mmtts = max ?mmt ?mmts" by simp
    note IH11 = IH1[THEN conjunct1] note IH12 = IH1[THEN conjunct2,THEN conjunct1]
    note IH21 = IH2[THEN conjunct1] note IH22 = IH2[THEN conjunct2,THEN conjunct1]
    have arecb: "a < ?abts ∧ ?abts < b" using ab False by(auto)
    have "?abt ≤ a ∨ a < ?abt" by auto
    hence "?abts = max ?mmt ?mmts"
    proof
      assume "?abt ≤ a"
      hence "?a' = a" by simp
      hence "?abts = ?mmts" using IH22 arecb by presburger
      moreover
      have "?mmt ≤ ?mmts" using IH11 ‹?abt ≤ a› arecb ‹?abts = ?mmts› by auto
      ultimately show ?thesis by(simp add:Let_def)
    next
      assume "a < ?abt"
      have "?abt < b" by (meson False linorder_not_le max_less_iff_conj)
      hence "?abt = ?mmt" using IH12 ‹a < ?abt› by blast
      have "?a' < ?abts ∨ ?a' = ?abts" using ab_maxs_ge_a[of ?a' b ts] order_le_less by blast
      thus ?thesis
      proof
        assume "?a' < ?abts"
        thus ?thesis using ‹?abt = ?mmt› IH22 arecb by(simp)
      next
        assume "?a' = ?abts"
        then show ?thesis using ‹?abt = ?mmt› ‹a < ?abt› IH21 by(simp)
      qed
    qed
    thus ?thesis using ‹?abtts = ?abts› ‹?mmtts = max ?mmt ?mmts› by simp
  qed

  show ?case using 1 2 3 by blast
next
  case 8 thus ?case
    apply(simp add: Let_def)
    by (smt (verit, del_insts) ab_mins_le_b linorder_le_cases linorder_not_le min_le_iff_disj order_antisym)
qed auto

corollary ab_max_bot_top: "ab_max ⊥ ⊤ t = maxmin t"
by (metis bounded_linorder_collapse fishburn_val_ab(1) fishburn_bot_top)

text ‹A detailed @{const knuth} proof, similar to @{thm fishburn_val_ab} proof:›

theorem knuth_val_ab:
  shows "a < b ⟹ knuth a b (maxmin t)   (ab_max a b t)"
    and "a < b ⟹ knuth a b (maxmin (Nd ts)) (ab_maxs a b ts)"
    and "a < b ⟹ knuth a b (minmax t)   (ab_min a b t)"
    and "a < b ⟹ knuth a b (minmax (Nd ts)) (ab_mins a b ts)"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  case (4 a b t ts)
  let ?abt = "ab_min a b t" let ?a' = "max a ?abt" let ?abts = "ab_maxs ?a' b ts"
  let ?mmt = "minmax t" let ?mmts = "maxmin (Nd ts)"
  note IH1 = "4.IH"(1)[OF ‹a<b›]

  have 1: "maxmin (Nd (t # ts)) ≤ a" if ab: "ab_maxs a b (t # ts) ≤ a"
  proof (cases "b ≤ ?a'")
    case True(*impossible*)
    note ‹a<b›
    also note True
    also have "?a' = ab_maxs a b (t # ts)" using True by simp
    also note ‹… ≤ a›
    finally have False by simp
    thus ?thesis ..
  next
    case False
    hence IH2: "knuth ?a' b ?mmts ?abts"
      using 4(2)[OF refl] ‹a<b› linorder_not_le by blast
    from False ab have ab: "ab_maxs ?a' b ts ≤ a" by(simp)
    have "?a' ≤ ?abts" by(rule ab_maxs_ge_a)
    (*In fact: ‹?abts = ?a' = a›*)
    hence "?mmt ≤ a" using IH1 ab by (metis order.trans linorder_not_le max.absorb4)
    have "?abts ≤ ?a'" using ab le_max_iff_disj by blast
    from ‹?a' ≤ ?abts› ab have "?a' ≤ a" by(rule order.trans)
    hence "?mmts ≤ a" using IH2 ‹?abts ≤ ?a'› order.trans by blast
    with ‹?mmt ≤ a› show ?thesis by simp
  qed

  have 2: "b ≤ maxmin (Nd (t # ts))" if ab: "b ≤ ab_maxs a b (t # ts)"
  proof (cases "b ≤ ?a'")
    case True
    hence "b ≤ ?abt" using ‹a<b› by (metis linorder_not_le max_less_iff_conj)
    hence "b ≤ ?mmt" using IH1 by blast
    thus ?thesis by (simp add: le_max_iff_disj)
  next
    case False
    hence "b ≤ ?abts" using ab by simp
    hence "b ≤ ?mmts" using "4.IH"(2)[OF refl] False by (meson linorder_not_le)
    then show ?thesis by (simp add: le_max_iff_disj)
  qed

  have 3: "ab_maxs a b (t # ts) = maxmin (Nd (t # ts))"
   if ab: "a < ab_maxs a b (t # ts)" "ab_maxs a b (t # ts) < b"
  proof (cases "b ≤ ?a'")
    case True(*impossible*)
    also have "?a' = ab_maxs a b (t # ts)" using True by simp
    also note ab(2)
    finally have False by simp
    thus ?thesis ..
  next
    case False
    hence IH2: "knuth ?a' b ?mmts ?abts" using 4(2)[OF refl] ‹a<b› linorder_not_le by blast
    have "ab_maxs a b (t # ts) = ?abts" using False by(simp)
    note IH11 = IH1[THEN conjunct1] note IH12 = IH1[THEN conjunct2,THEN conjunct1]
    note IH21 = IH2[THEN conjunct1] note IH22 = IH2[THEN conjunct2,THEN conjunct1]
    have "?abt < b" by (meson False linorder_not_le max_less_iff_conj) (*used?*)
    have arecb: "a < ?abts ∧ ?abts < b" using ab False by(auto)
    have "?abt ≤ a ∨ a < ?abt" by auto
    thus ?thesis
    proof
      assume "?abt ≤ a"
      hence "?a' = a" by simp
      hence "?abts = ?mmts" using IH22 arecb by presburger
      moreover
      have "?mmt ≤ ?mmts" using IH11 ‹?abt ≤ a› arecb ‹?abts = ?mmts› by auto
      ultimately show ?thesis using ‹ab_maxs a b (t # ts) = ?abts› by(simp add:Let_def)
    next
      assume "a < ?abt"
      have "?abt = minmax t" using IH12 ‹a < ?abt› ‹?abt < b› by blast
      have "?a' < ?abts ∨ ?a' = ?abts" using ab_maxs_ge_a[of ?a' b ts] order_le_less by blast
      thus ?thesis
      proof
        assume "?a' < ?abts"
        then show ?thesis using ‹?abt = ?mmt› False IH22 arecb by(simp)
      next
        assume "?a' = ?abts"
        then show ?thesis using ‹?abt = ?mmt› False ‹a < ?abt› IH21 by(simp)
      qed
    qed
  qed

  show ?case using 1 2 3 by blast
next
  case 8 thus ?case
    apply(simp add: Let_def)
    by (smt (verit, del_insts) ab_mins_le_b linorder_le_cases linorder_not_le min_le_iff_disj order_antisym)
qed auto

text ‹Towards exactness:›

lemma ab_max_le_b: "⟦ a ≤ b; maxmin t ≤ b ⟧ ⟹ ab_max a b t ≤ b"
and  "⟦ a ≤ b; maxmin (Nd ts) ≤ b ⟧ ⟹ ab_maxs a b ts ≤ b"
and "⟦ a ≤ minmax t; a ≤ b ⟧ ⟹ a ≤ ab_min a b t"
and  "⟦ a ≤ minmax (Nd ts); a ≤ b ⟧ ⟹ a ≤ ab_mins a b ts"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  case (4 a b t ts)
  show ?case
  proof (cases t)
    case Lf
    then show ?thesis using "4.IH"(2) "4.prems" by(simp add: Let_def)
  next
    case Nd
    then show ?thesis
      apply(simp add: Let_def leI ab_mins_le_b)
      using "4.IH"(2) "4.prems" ab_mins_le_b by auto
  qed
next
  case (8 a b t ts)
  show ?case
  proof (cases t)
    case Lf
    then show ?thesis using "8.IH"(2) "8.prems" by(simp add: Let_def)
  next
    case Nd
    then show ?thesis
      apply(simp add: Let_def leI ab_maxs_ge_a)
      using "8.IH"(2) "8.prems" ab_maxs_ge_a by auto
  qed
qed auto

lemma ab_max_exact:
assumes "v = maxmin t" "a ≤ v ∧ v ≤ b"
shows "ab_max a b t = v"
proof (cases t)
  case Lf with assms show ?thesis by simp
next
  case Nd
  then show ?thesis using assms
    by (smt (verit) ab_max.simps(2) ab_max_le_b ab_maxs_ge_a order.order_iff_strict order_le_less_trans fishburn_val_ab(1))
qed


subsubsection ‹Hard, max/min flag›

fun ab_minmax :: "bool ⇒ ('a::linorder) ⇒ 'a ⇒ 'a tree ⇒ 'a" and ab_minmaxs where
"ab_minmax mx a b (Lf x) = x" |
"ab_minmax mx a b (Nd ts) = ab_minmaxs mx a b ts" |

"ab_minmaxs mx a b [] = a" |
"ab_minmaxs mx a b (t#ts) =
 (let abt = ab_minmax (¬mx) b a t;
      a' = (if mx then max else min) a abt
  in if (if mx then (≥) else (≤)) a' b then a' else ab_minmaxs mx a' b ts)"

lemma ab_max_ab_minmax:
  shows "ab_max a b t = ab_minmax True a b t"
  and   "ab_maxs a b ts = ab_minmaxs True a b ts"
  and   "ab_min b a t = ab_minmax False a b t"
  and   "ab_mins b a ts = ab_minmaxs False a b ts"
proof(induction a b t and a b ts and b a t and b a ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
qed (auto simp add: Let_def)


subsubsection ‹Hard, abstracted over ‹≤››

fun ab_le :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ ('a::linorder)tree ⇒ 'a" and ab_les where
"ab_le le a b (Lf x) = x" |
"ab_le le a b (Nd ts) = ab_les le a b ts" |

"ab_les le a b [] = a" |
"ab_les le a b (t#ts) = (let abt = ab_le (λx y. le y x) b a t;
  a' = if le a abt then abt else a in if le b a' then a' else ab_les le a' b ts)"

lemma ab_max_ab_le:
  shows "ab_max a b t = ab_le (≤) a b t"
  and   "ab_maxs a b ts = ab_les (≤) a b ts"
  and   "ab_min b a t = ab_le (≥) a b t"
  and   "ab_mins b a ts = ab_les (≥) a b ts"
proof(induction a b t and a b ts and b a t and b a ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
qed (auto simp add: Let_def)

text ‹Delayed test:›

fun ab_le3 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ ('a::linorder)tree ⇒ 'a" and ab_les3 where
"ab_le3 le a b (Lf x) = x" |
"ab_le3 le a b (Nd ts) = ab_les3 le a b ts" |

"ab_les3 le a b [] = a" |
"ab_les3 le a b (t#ts) =
 (if le b a then a else
  let abt = ab_le3 (λx y. le y x) b a t;
      a' = if le a abt then abt else a
  in ab_les3 le a' b ts)"

lemma ab_max_ab_le3:
  shows "a < b ⟹ ab_max a b t = ab_le3 (≤) a b t"
  and   "a < b ⟹ ab_maxs a b ts = ab_les3 (≤) a b ts"
  and   "a > b ⟹ ab_min b a t = ab_le3 (≥) a b t"
  and   "a > b ⟹ ab_mins b a ts = ab_les3 (≥) a b ts"
proof(induction a b t and a b ts and b a t and b a ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  case (4 a b t ts)
  show ?case
  proof (cases ts)
    case Nil
    then show ?thesis using 4 by (simp add: Let_def)
  next
    case Cons
    then show ?thesis using 4 by (auto simp add: Let_def le_max_iff_disj)
  qed
next
  case (8 a b t ts)
  show ?case
  proof (cases ts)
    case Nil
    then show ?thesis using 8 by (simp add: Let_def)
  next
    case Cons
    then show ?thesis using 8 by (auto simp add: Let_def min_le_iff_disj)
  qed
qed auto

corollary ab_le3_bot_top: "ab_le3 (≤) ⊥ ⊤ t = maxmin t"
by (metis (mono_tags, lifting) ab_max_ab_le3(1) ab_max_bot_top bounded_linorder_collapse)


subsubsection ‹Hard, ‹max/min› in ‹Lf››

text ‹Idea due to Bird and Hughes›

fun ab_max2 :: "'a ⇒ 'a ⇒ ('a::linorder)tree ⇒ 'a" and ab_maxs2 and ab_min2 and ab_mins2 where
"ab_max2 a b (Lf x) = max a (min x b)" |
"ab_max2 a b (Nd ts) = ab_maxs2 a b ts" |

"ab_maxs2 a b [] = a" |
"ab_maxs2 a b (t#ts) = (let a' = ab_min2 a b t in if a' = b then a' else ab_maxs2 a' b ts)" |

"ab_min2 a b (Lf x) = max a (min x b)" |
"ab_min2 a b (Nd ts) = ab_mins2 a b ts" |

"ab_mins2 a b [] = b" |
"ab_mins2 a b (t#ts) = (let b' = ab_max2 a b t in if a = b' then b' else ab_mins2 a b' ts)"

lemma ab_max2_max_min_maxmin:
shows "a ≤ b ⟹ ab_max2 a b t = max a (min (maxmin t) b)" (* TODO: find equational proof! *)
and "a ≤ b ⟹ ab_maxs2 a b ts = max a (min (maxmin (Nd ts)) b)"
and "a ≤ b ⟹ ab_min2 a b t = max a (min (minmax t) b)"
and "a ≤ b ⟹ ab_mins2 a b ts = max a (min (minmax (Nd ts)) b)"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max2_ab_maxs2_ab_min2_ab_mins2.induct)
  case 4 thus ?case apply (simp add: Let_def)
    by (metis (no_types, lifting) max.assoc max_min_same(4) min_max_distrib1)
next
  case 8 thus ?case apply (simp add: Let_def)
    by (metis (no_types, opaque_lifting) max.left_idem max_min_distrib2 max_min_same(1) min.assoc min.commute)
qed auto

corollary ab_max2_bot_top: "ab_max2 ⊥ ⊤ t = maxmin t"
by(simp add: ab_max2_max_min_maxmin)

text ‹Now for the ‹ab› version parameterized with ‹le›:›

fun ab_le2 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ ('a::linorder)tree ⇒ 'a" and ab_les2 where
"ab_le2 le a b (Lf x) =
 (let xb = if le x b then x else b
  in if le a xb then xb else a)" |
"ab_le2 le a b (Nd ts) = ab_les2 le a b ts" |

"ab_les2 le a b [] = a" |
"ab_les2 le a b (t#ts) = (let a' = ab_le2 (λx y. le y x) b a t in if a' = b then a' else ab_les2 le a' b ts)"

text ‹Relate @{const ab_le2} back to @{const ab_max2} (using @{thm ab_max2_max_min_maxmin}!):›

lemma ab_le2_ab_max2:
fixes a :: "_ :: bounded_linorder"
shows "a ≤ b ⟹ ab_le2 (≤) a b t = ab_max2 a b t"
and   "a ≤ b ⟹ ab_les2 (≤) a b ts = ab_maxs2 a b ts"
and   "a ≤ b ⟹ ab_le2 (≥) b a t = ab_min2 a b t"
and   "a ≤ b ⟹ ab_les2 (≥) b a ts = ab_mins2 a b ts"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max2_ab_maxs2_ab_min2_ab_mins2.induct)
  case (4 a b t ts) thus ?case
    apply (simp add: Let_def)
    by (metis ab_max2_max_min_maxmin(3) max.boundedI min.cobounded2)
next
  case 8 thus ?case
    apply (simp add: Let_def)
    by (metis ab_max2_max_min_maxmin(1) max.cobounded1)
qed auto

corollary ab_le2_bot_top: "ab_le2 (≤) ⊥ ⊤ t = maxmin t"
by (simp add: ab_le2_ab_max2(1) ab_max2_bot_top)


subsubsection ‹Hard, Delayed Test›

fun ab_max3 :: "'a ⇒ 'a ⇒ ('a::linorder)tree ⇒ 'a" and ab_maxs3 and ab_min3 and ab_mins3 where
"ab_max3 a b (Lf x) = x" |
"ab_max3 a b (Nd ts) = ab_maxs3 a b ts" |

"ab_maxs3 a b [] = a" |
"ab_maxs3 a b (t#ts) = (if a ≥ b then a else ab_maxs3 (max a (ab_min3 a b t)) b ts)" |

"ab_min3 a b (Lf x) = x" |
"ab_min3 a b (Nd ts) = ab_mins3 a b ts" |

"ab_mins3 a b [] = b" |
"ab_mins3 a b (t#ts) = (if a ≥ b then b else ab_mins3 a (min b (ab_max3 a b t)) ts)"

lemma ab_max3_ab_max:
shows "a<b ⟹ ab_max3 a b t = ab_max a b t"
and "a<b ⟹ ab_maxs3 a b ts = ab_maxs a b ts"
and "a<b ⟹ ab_min3 a b t = ab_min a b t"
and "a<b ⟹ ab_mins3 a b ts = ab_mins a b ts"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max3_ab_maxs3_ab_min3_ab_mins3.induct)
  case (4 a b t ts)
  show ?case
  proof (cases ts)
    case Nil
    then show ?thesis using 4 by (simp add: Let_def)
  next
    case Cons
    then show ?thesis using 4 by (auto simp add: Let_def le_max_iff_disj)
  qed
next
  case (8 a b t ts)
  show ?case
  proof (cases ts)
    case Nil
    then show ?thesis using 8 by (simp add: Let_def)
  next
    case Cons
    then show ?thesis using 8 by (auto simp add: Let_def min_le_iff_disj)
  qed
qed auto

corollary ab_max3_bot_top: "ab_max3 ⊥ ⊤ t = maxmin t"
by(metis fishburn_bot_top ab_max3_ab_max(1) fishburn_val_ab(1) bounded_linorder_collapse)


subsubsection ‹Soft›

text ‹Fishburn›

fun ab_max' :: "'a::bounded_linorder ⇒ 'a ⇒ 'a tree ⇒ 'a" and ab_maxs' ab_min' ab_mins' where
"ab_max' a b (Lf x) = x" |
"ab_max' a b (Nd ts) = ab_maxs' a b ⊥ ts" |

"ab_maxs' a b m [] = m" |
"ab_maxs' a b m (t#ts) =
  (let m' = max m (ab_min' (max m a) b t) in if m' ≥ b then m' else ab_maxs' a b m' ts)" |

"ab_min' a b (Lf x) = x" |
"ab_min' a b (Nd ts) = ab_mins' a b ⊤ ts" |

"ab_mins' a b m [] = m" |
"ab_mins' a b m (t#ts) =
  (let m' = min m (ab_max' a (min m b) t) in if m' ≤ a then m' else ab_mins' a b m' ts)"

lemma ab_maxs'_ge_a: "ab_maxs' a b m ts ≥ m"
apply(induction ts arbitrary: a b m)
by (auto simp: Let_def)(use max.bounded_iff in blast)


lemma ab_mins'_le_a: "ab_mins' a b m ts ≤ m"
apply(induction ts arbitrary: a b m)
by (auto simp: Let_def)(use min.bounded_iff in blast)

(* TODO: Exercise? *)
text‹Find ‹a›, ‹b› and ‹t› such that ‹a < b› and fail-soft is closer to the real value than fail-hard.›
lemma "let a = - ∞; b = ereal 0; t = Nd [Nd []]
 in a < b ∧ ab_max a b t = 0 ∧ ab_max' a b t = ∞ ∧ maxmin t = ∞"
by eval

(* TODO? readable proofs of ‹fishburn_val_ab'›*)

theorem fishburn_val_ab':
shows "a < b ⟹ fishburn a b (maxmin t) (ab_max' a b t)"
  and "max m a < b ⟹ fishburn (max m a) b (maxmin (Nd ts)) (ab_maxs' a b m ts)"
  and "a < b ⟹ fishburn a b (minmax t) (ab_min' a b t)"
  and "a < min m b ⟹ fishburn a (min m b) (minmax (Nd ts)) (ab_mins' a b m ts)"
proof(induction a b t and a b m ts and a b t and a b m ts rule: ab_max'_ab_maxs'_ab_min'_ab_mins'.induct)
  case (4 a b m t ts)
  then show ?case
    apply (simp add: Let_def)
  by (smt (verit, best) ab_maxs'_ge_a max.absorb_iff2 max.coboundedI1 max.commute nle_le nless_le)
next
  case (8 a b m t ts)
  then show ?case
    apply (simp add: Let_def)
    by (smt (z3) ab_mins'_le_a linorder_not_le min.absorb_iff2 min.coboundedI1 min_def)
qed auto

theorem fishburn_ab'_ab:
  shows "a < b ⟹ fishburn a b (ab_max' a b t)   (ab_max a b t)"
    and "max m a < b ⟹ fishburn a b (ab_maxs' a b m ts) (ab_maxs (max m a) b ts)"
    and "a < b ⟹ fishburn a b (ab_min' a b t)   (ab_min a b t)"
    and "a < min m b ⟹ a < m ⟹ fishburn a b (ab_mins' a b m ts) (ab_mins a (min m b) ts)"
proof(induction a b t and a b m ts and a b t and a b m ts rule: ab_max'_ab_maxs'_ab_min'_ab_mins'.induct)
  case 3 thus ?case apply simp
    by (metis linorder_not_le max.absorb4 max.order_iff)
next
  case (4 a b m t ts)
  thus ?case using [[simp_depth_limit=2]] apply (simp add: Let_def)
    by (smt (verit, ccfv_threshold) linorder_not_le max.absorb2 max_less_iff_conj nle_le)
next
  case 6 thus ?case
    apply simp using top.extremum_strict top.not_eq_extremum by blast
next
  case 7 thus ?case apply simp
    by (metis linorder_not_le min.absorb4 min.order_iff)
next
  case (8 a b m t ts)
  thus ?case using [[simp_depth_limit=2]] apply (simp add: Let_def)
    by (smt (verit) linorder_not_le min_def nle_le fishburn2)
qed auto

text ‹Fail-soft can be more precise than fail-hard:›
lemma "let a = ereal 0; b = 1; t = Nd [] in
  maxmin t = ab_max' a b t ∧ maxmin t ≠ ab_max a b t"
by eval

(* Towards dubious exactness: *)
lemma ab_max'_lb_ub:
shows "a ≤ b ⟹ lb_ub a b (maxmin t) (ab_max' a b t)"
and "a ≤ b ⟹ lb_ub a b (max i (maxmin (Nd ts))) (ab_maxs' a b i ts)"
and "a ≤ b ⟹ lb_ub a b (minmax t) (ab_min' a b t)"
and "a ≤ b ⟹ lb_ub a b (min i (minmax (Nd ts))) (ab_mins' a b i ts)"
proof(induction a b t and a b i ts and a b t and a b i ts rule: ab_max'_ab_maxs'_ab_min'_ab_mins'.induct)
  case (4 a b m t ts)
  then show ?case
    apply(simp_all add: Let_def)
    by (smt (verit) max.coboundedI1 max.coboundedI2 max_def)
next
  case (8 a b m t ts)
  then show ?case
    apply(simp_all add: Let_def)
    by (smt (verit, del_insts) min.coboundedI1 min.coboundedI2 min_def)
qed auto

lemma ab_max'_exact_less: "⟦ a<b; v = maxmin t; a ≤ v ∧ v ≤ b ⟧ ⟹ ab_max' a b t = v"
using fishburn_val_ab'(1) by force

lemma ab_max'_exact: "⟦ v = maxmin t; a ≤ v ∧ v ≤ b ⟧ ⟹ ab_max' a b t = v"
using ab_max'_exact_less ab_max'_lb_ub(1)
by (metis order.strict_trans2 nless_le)


subsubsection ‹Searched trees›

text ‹Hard:›

fun abt_max :: "('a::linorder) ⇒ 'a ⇒ 'a tree ⇒ 'a tree" and abt_maxs abt_min abt_mins where
"abt_max a b (Lf x) = Lf x" |
"abt_max a b (Nd ts) = Nd (abt_maxs a b ts)" |

"abt_maxs a b [] = []" |
"abt_maxs a b (t#ts) = (let u = abt_min a b t; a' = max a (ab_min a b t) in
  u # (if a' ≥ b then [] else abt_maxs a' b ts))" |

"abt_min a b (Lf x) = Lf x" |
"abt_min a b (Nd ts) = Nd (abt_mins a b ts)" |

"abt_mins a b [] = []" |
"abt_mins a b (t#ts) = (let u = abt_max a b t; b' = min b (ab_max a b t) in
  u # (if b' ≤ a then [] else abt_mins a b' ts))"

text ‹Soft:›

fun abt_max' :: "('a::bounded_linorder) ⇒ 'a ⇒ 'a tree ⇒ 'a tree" and abt_maxs' abt_min' abt_mins' where
"abt_max' a b (Lf x) = Lf x" |
"abt_max' a b (Nd ts) = Nd (abt_maxs' a b ⊥ ts)" |

"abt_maxs' a b m [] = []" |
"abt_maxs' a b m (t#ts) =
 (let u = abt_min' (max m a) b t; m' = max m (ab_min' (max m a) b t) in
  u # (if m' ≥ b then [] else abt_maxs' a b m' ts))" |

"abt_min' a b (Lf x) = Lf x" |
"abt_min' a b (Nd ts) = Nd (abt_mins' a b ⊤ ts)" |

"abt_mins' a b m [] = []" |
"abt_mins' a b m (t#ts) =
 (let u = abt_max' a (min m b) t; m' = min m (ab_max' a (min m b) t) in
  u # (if m' ≤ a then [] else abt_mins' a b m' ts))"

lemma abt_max'_abt_max:
shows "a < b ⟹ abt_max' a b t = abt_max a b t"
and "max m a < b ⟹ abt_maxs' a b m ts = abt_maxs (max m a) b ts"
and "a < b ⟹ abt_min' a b t = abt_min a b t"
and "a < min m b ⟹ abt_mins' a b m ts = abt_mins a (min m b) ts"
proof(induction a b t and a b m ts and a b t and a b m ts rule: abt_max'_abt_maxs'_abt_min'_abt_mins'.induct)
  case (4 a b m t ts)
  thus ?case unfolding abt_maxs'.simps(2) abt_maxs.simps(2) Let_def
    using fishburn_ab'_ab(3)
    by (smt (verit, best) le_max_iff_disj linorder_not_le max_def nless_le)
next
  case (8 a b m t ts)
  then show ?case unfolding abt_mins'.simps(2) abt_mins.simps(2) Let_def
    using fishburn_ab'_ab(1)
    by (smt (verit, del_insts) linorder_not_le min.absorb1 min.absorb3 min.commute min_le_iff_disj)
qed (auto)

text ‹An annotated tree of ‹ab› calls with the ‹a,b› window.›

datatype 'a tri = Ma 'a 'a "'a tr" | Mi 'a 'a "'a tr"
and 'a tr = No "'a tri list" | Le 'a

fun abtr_max :: "('a::linorder) ⇒ 'a ⇒ 'a tree ⇒ 'a tri" and abtr_maxs abtr_min abtr_mins where
"abtr_max a b (Lf x) = Ma a b (Le x)" |
"abtr_max a b (Nd ts) = Ma a b (No (abtr_maxs a b ts))" |

"abtr_maxs a b [] = []" |
"abtr_maxs a b (t#ts) = (let u = abtr_min a b t; a' = max a (ab_min a b t) in
  u # (if a' ≥ b then [] else abtr_maxs a' b ts))" |

"abtr_min a b (Lf x) = Mi a b (Le x)" |
"abtr_min a b (Nd ts) = Mi a b (No (abtr_mins a b ts))" |

"abtr_mins a b [] = []" |
"abtr_mins a b (t#ts) = (let u = abtr_max a b t; b' = min b (ab_max a b t) in
  u # (if b' ≤ a then [] else abtr_mins a b' ts))"

text ‹For better readability get rid of ‹ereal›:›
fun de :: "ereal ⇒ real" where
"de (ereal x) = x" |
"de PInfty = 100" |
"de MInfty = -100"

fun detri and detr where
"detri (Ma a b t) = Ma (de a) (de b) (detr t)" |
"detri (Mi a b t) = Mi (de a) (de b) (detr t)" |
"detr (No ts) = No (map detri ts)" |
"detr (Le x) = Le (de x)"

text ‹Example in Knuth and Moore. Evaluation confirms that all subtrees ‹u› are pruned.›
value "let
 t11 = Nd[Nd[Lf 3,Lf 1,Lf 4], Nd[Lf 1,t], Nd[Lf 2,Lf 6,Lf 5]];
 t12 = Nd[Nd[Lf 3,Lf 5,Lf 8], u]; t13 = Nd[Nd[Lf 8,Lf 4,Lf 6], u];
 t21 = Nd[Nd[Lf 3,Lf 2],Nd[Lf 9,Lf 5,Lf 0],Nd[Lf 2,u]];
 t31 = Nd[Nd[Lf 0,u],Nd[Lf 4,Lf 9,Lf 4],Nd[Lf 4,u]];
 t32 = Nd[Nd[Lf 2,u],Nd[Lf 7,Lf 8,Lf 1],Nd[Lf 6,Lf 4,Lf 0]];
  t = Nd[Nd[t11, t12, t13], Nd[t21,u], Nd[t31,t32,u]]
in (ab_max (-∞::ereal) ∞ t,abt_max (-∞::ereal) ∞ t,detri(abtr_max (-∞::ereal) ∞ t))"


subsubsection ‹Soft, generalized, attempts›

text ‹Attempts to prove correct General version due to Junkang Li et al.›

text ‹This first version (not worth following!) stops the list iteration as soon as ‹max m a ≥ b›
(I call this "delayed test", it complicates proofs a little.)
and the initial value is fixed ‹a› (not ‹i0/1›)›

fun abil0' :: "('a::bounded_linorder)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abils0' abil1' abils1' where
"abil0' (Lf x) a b = x" |
"abil0' (Nd ts) a b = abils0' ts a b a" |

"abils0' [] a b m = m" |
"abils0' (t#ts) a b m =
  (if max m a ≥ b then m else abils0' ts (max m a) b (max m (abil1' t b (max m a))))" |

"abil1' (Lf x) a b = x" |
"abil1' (Nd ts) a b = abils1' ts a b a" |

"abils1' [] a b m = m" |
"abils1' (t#ts) a b m =
  (if min m a ≤ b then m else  abils1' ts (min m a) b (min m (abil0' t b (min m a))))"

lemma abils0'_ge_i: "abils0' ts a b i ≥ i"
apply(induction ts arbitrary: i a)
by (auto simp: Let_def)(use max.bounded_iff in blast)

lemma abils1'_le_i: "abils1' ts a b i ≤ i"
apply(induction ts arbitrary: i a)
by (auto simp: Let_def)(use min.bounded_iff in blast)

lemma fishburn_abil01':
  shows "a < b ⟹ fishburn a b (maxmin t)           (abil0' t a b)"
    and "a < b ⟹ i < b ⟹ fishburn (max a i) b (maxmin (Nd ts)) (abils0' ts a b i)"
    and "a > b ⟹ fishburn b a (minmax t)           (abil1' t a b)"
    and "a > b ⟹ i > b ⟹ fishburn b (min a i) (minmax (Nd ts)) (abils1' ts a b i)"
proof(induction t a b and ts a b i and t a b and ts a b i rule: abil0'_abils0'_abil1'_abils1'.induct)
  case (4 t ts a b m)
  thus ?case apply (simp add: Let_def)
    by (smt (verit) abils0'.elims abils0'_ge_i max.absorb_iff1 max.coboundedI2 max_def nless_le)
next
  case (8 t ts a b m)
  thus ?case apply (simp add: Let_def)
    by (smt (verit, best) abils1'.elims abils1'_le_i linorder_not_le min.absorb2 min_def min_le_iff_disj)
qed auto

text ‹This second computes the value of ‹t› before deciding if it needs to look at ‹ts› as well.
This simplifies the proof (also in other versions, independently of initialization).
The initial value is not fixed but determined by ‹i0/1›. The "real" constraint on ‹i0/1›
is commented out and replaced by the simplified value ‹a›.›

locale LeftSoft =
fixes i0 i1 :: "'a::bounded_linorder tree list ⇒ 'a ⇒ 'a"
assumes i0: "i0 ts a ≤ a ―‹max a (maxmin (Nd ts))›" and i1: "i1 ts a ≥ a―‹min a (minmax (Nd ts))›"
begin

fun abil0' :: "('a::bounded_linorder)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abils0' abil1' abils1' where
"abil0' (Lf x) a b = x" |
"abil0' (Nd ts) a b = abils0' ts a b (i0 ts a)" |

"abils0' [] a b m = m" |
"abils0' (t#ts) a b m =
  (let m' = max m (abil1' t b (max m a)) in if m' ≥ b then m' else abils0' ts a b m')" |

"abil1' (Lf x) a b = x" |
"abil1' (Nd ts) a b = abils1' ts a b (i1 ts a)" |

"abils1' [] a b m = m" |
"abils1' (t#ts) a b m =
  (let m' = min m (abil0' t b (min m a)) in if m' ≤ b then m' else abils1' ts a b m')"

lemma abils0'_ge_i: "abils0' ts a b i ≥ i"
apply(induction ts arbitrary: i)
by (auto simp: Let_def)(use max.bounded_iff in blast)

lemma abils1'_le_i: "abils1' ts a b i ≤ i"
apply(induction ts arbitrary: i)
by (auto simp: Let_def)(use min.bounded_iff in blast)

text ‹Generalizations that don't seem to work:
a) ‹max a i → max (max a (maxmin (Nd ts))) i›
b) ‹ ?››

lemma fishburn_abil01':
  shows "a < b ⟹ fishburn a b (maxmin t)           (abil0' t a b)"
    and "a < b ⟹ i < b ⟹ fishburn (max a i) b (maxmin (Nd ts)) (abils0' ts a b i)"
    and "a > b ⟹ fishburn b a (minmax t)           (abil1' t a b)"
    and "a > b ⟹ i > b ⟹ fishburn b (min a i) (minmax (Nd ts)) (abils1' ts a b i)"
proof(induction t a b and ts a b i and t a b and ts a b i rule: abil0'_abils0'_abil1'_abils1'.induct)
  case (2 ts a b)
  thus ?case using i0[of ts a] by auto
next
  case (4 i t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (verit) abils0'_ge_i le_max_iff_disj linorder_not_le max.absorb1 nle_le)
next
  case (6 ts a b)
  thus ?case using i1[of a ts] by simp
next
  case (8 i t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (verit, best) abils1'_le_i linorder_not_le min_def min_less_iff_conj nle_le)
qed auto

text ‹Note the ‹a ≤ b› instead of the ‹a < b› in theorem ‹fishburn_abir01'›:›

lemma abil0'lb_ub:
shows "a ≤ b ⟹ lb_ub a b (maxmin t) (abil0' t a b)"
and "a ≤ b ⟹ lb_ub a b (max i (maxmin (Nd ts))) (abils0' ts a b i)"
and "a ≥ b ⟹ lb_ub b a (minmax t) (abil1' t a b)"
and "a ≥ b ⟹ lb_ub b a (min i (minmax (Nd ts))) (abils1' ts a b i)"
proof(induction t a b and ts a b i and t a b and ts a b i rule: abil0'_abils0'_abil1'_abils1'.induct)
  case (2 ts a b)
  then show ?case by simp (meson order.trans i0 le_max_iff_disj)
next
  case (4 t ts a b m)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, best) max.coboundedI1 max.coboundedI2 max_def)
next
  case (6 ts a b)
  then show ?case
    by simp (meson i1 min.coboundedI2 order_trans)
next
  case (8 t ts a b m)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, del_insts) min.coboundedI1 min.coboundedI2 min_def)
qed auto

lemma abil0'_exact_less: "⟦ a<b; v = maxmin t; a ≤ v ∧ v ≤ b ⟧ ⟹ abil0' t a b = v"
using fishburn_abil01'(1) by force

lemma abil0'_exact: "⟦ v = maxmin t; a ≤ v ∧ v ≤ b⟧ ⟹ abil0' t a b = v"
by (metis abil0'_exact_less abil0'lb_ub(1) order.trans leD order_le_imp_less_or_eq)

end


subsubsection ‹Transposition Table / Graph / Repeated AB›

(* Marsland/Li, repeated evaluation of same position with different a/b. Transposition table!

"In alpha-beta search with cache for totally ordered values (for instance [Marsland, 1986]),
one can exploit the fact that with usual value initialisation, the value f(n,α,β) satisfies
f(n,α,β) < β ⇒ v(n) ≤ f(n,α,β) and f(n,α,β) > α ⇒ v(n) ≥ f(n,α,β).
In particular, if α < f(n,α,β) < β, then f(n,α,β) = v(n).
Hence by comparing f(n,α,β) to α and β, one can determine whether it is exact,
a lower, or an upper bound, and store it in the cache with an appropriate flag."

These lemmas show what can be done.
Lemma 1: The initial call is ‹abf a b t > a›. Thus ‹abf a b t› is a lower bound for ‹maxmin t›.
Thus the second call ‹abf a' b' t› can be made with ‹max a' (abf a b t)›.
Lemma 2: The initial call is ‹abf t a b < b›. Thus ‹abf a b t› is an upper bound for ‹maxmin t›.
Thus the second call ‹abf a' b' t› can be made with ‹min b' (abf a b t)›.

Works as long as ‹abf› satisfies fishburn.

TODO: ab function with cache.
*)

lemma ab_twice_lb:
 "⟦ ∀a b. fishburn a b (maxmin t) (abf a b t); b ≤ abf a b t; max a' (abf a b t) < b' ⟧ ⟹
  fishburn a' b' (maxmin t) (abf (max a' (abf a b t)) b' t)"
by (smt (verit, del_insts) order.eq_iff order.strict_trans leI max_less_iff_conj)

lemma ab_twice_ub:
 "⟦ ∀a b. fishburn a b (maxmin t) (abf a b t); abf a b t ≤ a; min b' (abf a b t) > a' ⟧ ⟹
  fishburn a' b' (maxmin t) (abf a' (min b' (abf a b t)) t)"
by (smt (verit, best) linorder_not_le min.absorb1 min.absorb2 min.strict_boundedE nless_le)

text ‹But what does a narrower window achieve?
Less precise bounds but prefix of search space. For fail-hard and fail-soft.›

fun prefix prefixs where
"prefix (Lf x) (Lf y) = (x=y)" |
"prefix (Nd ts) (Nd us) = prefixs ts us" |
"prefix _ _ = False" |

"prefixs [] us = True" |
"prefixs (t#ts) (u#us) = (prefix t u ∧ prefixs ts us)" |
"prefixs _ _ = False"

lemma fishburn_ab_max_windows:
shows "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ fishburn a b (ab_max a' b' t) (ab_max a b t)"
and   "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ fishburn a b (ab_maxs a' b' ts) (ab_maxs a b ts)"
and   "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ fishburn a b (ab_min a' b' t) (ab_min a b t)"
and   "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ fishburn a b (ab_mins a' b' ts) (ab_mins a b ts)"
proof (induction a b t and a b ts and a b t and a b ts
       arbitrary: a' b' and a' b' and a' b' and a' b'
       rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  case 2 show ?case
    using "2.prems" apply simp
    using "2.IH" by presburger
next
  case (4 a b t ts) show ?case using "4.prems"
    apply (simp add: Let_def)
    using "4.IH"
    by (smt (verit, del_insts) ab_maxs_ge_a le_max_iff_disj linorder_not_le max_def nle_le)
next
  case 6 show ?case
    using "6.prems" apply simp
    using "6.IH" by presburger
next
  case (8 a b t ts) show ?case using "8.prems"
    apply (simp add: Let_def)
    using "8.IH"
    by (smt (verit, best) ab_mins_le_b order.strict_trans1 linorder_not_le min.absorb1 min.absorb2 nle_le)
qed auto

lemma abt_max_prefix_windows:
shows "⟦ a' ≤ a; b ≤ b' ⟧ ⟹ prefix (abt_max a b t) (abt_max a' b' t)"
and "⟦ a' ≤ a; b ≤ b' ⟧ ⟹ prefixs (abt_maxs a b ts) (abt_maxs a' b' ts)"
and "⟦ a' ≤ a; b ≤ b' ⟧ ⟹ prefix (abt_min a b t) (abt_min a' b' t)"
and "⟦ a' ≤ a; b ≤ b' ⟧ ⟹ prefixs (abt_mins a b ts) (abt_mins a' b' ts)"
proof (induction a b t and a b ts and a b t and a b ts
       arbitrary: a' b' and a' b' and a' b' and a' b'
       rule: abt_max_abt_maxs_abt_min_abt_mins.induct)
  case (4 a b t ts)
  then show ?case
    apply (simp add: Let_def)
    by (smt (verit, del_insts) fishburn_ab_max_windows(3) linorder_not_le max.coboundedI1 max.orderI max_def)
next
  case (8 a b t ts)
  then show ?case
    apply (simp add: Let_def)
    by (smt (verit, del_insts) fishburn_ab_max_windows(1) le_cases3 linorder_not_less min_def_raw knuth_if_fishburn)
qed auto

lemma fishburn_ab_max'_windows:
shows "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ fishburn a b (ab_max' a' b' t) (ab_max' a b t)"
and "⟦ max m a < b; a' ≤ a; b ≤ b'; m' ≤ m ⟧ ⟹ fishburn (max m a) b (ab_maxs' a' b' m' ts) (ab_maxs' a b m ts)"
and   "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ fishburn a b (ab_min' a' b' t) (ab_min' a b t)"
and "⟦ a < min m b; a' ≤ a; b ≤ b'; m ≤ m' ⟧ ⟹ fishburn a (min m b) (ab_mins' a' b' m' ts) (ab_mins' a b m ts)"
proof (induction a b t and a b m ts and a b t and a b m ts
       arbitrary: a' b' and a' b' m' and a' b' and a' b' m'
       rule: ab_max'_ab_maxs'_ab_min'_ab_mins'.induct)
  case (2 a b ts)
  show ?case
    using "2.prems" apply simp
    using "2.IH" by (metis max_bot nle_le)
next
  case (4 a b m t ts)
  show ?case
    using "4.prems" apply (simp add: Let_def)
    using "4.IH" ab_maxs'_ge_a
    by (smt (z3) le_max_iff_disj linorder_not_le max.cobounded2 max.commute max_def)
next
  case (6 a b ts)
  show ?case
    using "6.prems" apply simp
    using "6.IH" by (metis min_top nle_le)
next
  case (8 a b m t ts)
  show ?case
    using "8.prems" apply (simp add: Let_def)
    using "8.IH" ab_mins'_le_a
    by (smt (z3) leD linorder_linear min.absorb1 min.absorb2 min.bounded_iff not_le_imp_less)
qed auto

text ‹Example of reduced search space:›

lemma "let a = 0; b = (1::ereal); a' = 0; b' = 2; t = Nd [Lf 1, Lf 0]
  in abt_max' a b t = Nd [Lf 1] ∧ abt_max' a' b' t = t"
by eval

lemma abt_max'_prefix_windows:
shows "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ prefix (abt_max' a b t) (abt_max' a' b' t)"
and "⟦ max m a < b; a' ≤ a; b ≤ b'; m' ≤ m ⟧ ⟹ prefixs (abt_maxs' a b m ts) (abt_maxs' a' b' m' ts)"
and "⟦ a < b; a' ≤ a; b ≤ b' ⟧ ⟹ prefix (abt_min' a b t) (abt_min' a' b' t)"
and "⟦ a < min m b; a' ≤ a; b ≤ b'; m ≤ m' ⟧ ⟹ prefixs (abt_mins' a b m ts) (abt_mins' a' b' m' ts)"
proof (induction a b t and a b m ts and a b t and a b m ts
       arbitrary: a' b' and a' b' m' and a' b' and a' b' m'
       rule: abt_max'_abt_maxs'_abt_min'_abt_mins'.induct)
  case (4 a b m t ts)
  then show ?case apply (simp add: Let_def)
    using fishburn_ab_max'_windows(3)
    by (smt (verit, ccfv_threshold) add_mono linorder_le_cases max.absorb2 max.assoc max.order_iff order.strict_iff_not trans_le_add1)
next
  case (8 a b t ts)
  then show ?case apply (simp add: Let_def)
    using fishburn_ab_max'_windows(1)
    by (smt (verit, best)add_le_mono le_add1 linorder_not_less min.mono min_less_iff_conj order.trans nle_le)
qed auto


subsection ‹From the Right›

text ‹The literature uniformly considers iteration from the left only.
Iteration from the right is technically simpler but needs to go through all successors,
which means generating all of them.
This is typically done anyway to reorder them based on heuristic evaluations.
This rules out an infinite list of successors, but it is unclear if there are any applications.›

text ‹Naming convention: 0 = max, 1 = min›

subsubsection ‹Hard›

fun abr0 :: "('a::linorder)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abrs0 and abr1 and abrs1 where
"abr0 (Lf x) a b = x" |
"abr0 (Nd ts) a b = abrs0 ts a b" |

"abrs0 [] a b = a" |
"abrs0 (t#ts) a b = (let m = abrs0 ts a b in if m ≥ b then m else max (abr1 t b m) m)" |

"abr1 (Lf x) a b = x" |
"abr1 (Nd ts) a b = abrs1 ts a b" |

"abrs1 [] a b = a" |
"abrs1 (t#ts) a b = (let m = abrs1 ts a b in if m ≤ b then m else min (abr0 t b m) m)"

lemma abrs0_ge_a: "abrs0 ts a b ≥ a"
apply(induction ts arbitrary: a)
by (auto simp: Let_def)(use max.coboundedI2 in blast)

lemma abrs1_le_a: "abrs1 ts a b ≤ a"
apply(induction ts arbitrary: a)
by (auto simp: Let_def)(use min.coboundedI2 in blast)

theorem abr01_mm:
  shows "mm a (abr0 t a b) b = mm a (maxmin t) b"
    and "mm a (abrs0 ts a b) b = mm a (maxmin (Nd ts)) b"
    and "mm b (abr1 t a b) a = mm b (minmax t) a"
    and "mm b (abrs1 ts a b) a = mm b (minmax (Nd ts)) a"
proof(induction t a b and ts a b and t a b and ts a b rule: abr0_abrs0_abr1_abrs1.induct)
  case (4 t ts a b)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit) max.left_commute max_def_raw min.commute min.orderE min_max_distrib1)
next
  case (8 t ts a b)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit) max.left_idem max.orderE max_min_distrib2 max_min_same(4) min.assoc)
qed auto

text ‹As a corollary:›
corollary knuth_abr01_cor: "a < b ⟹ knuth a b (maxmin t) (abr0 t a b)"
by (meson knuth_if_mm abr01_mm(1))

corollary maxmin_mm_abr0: "⟦ a ≤ maxmin t; maxmin t ≤ b ⟧ ⟹ maxmin t = mm a (abr0 t a b) b"
by (metis max_def min.absorb1 abr01_mm(1))
corollary maxmin_mm_abrs0: "⟦ a ≤ maxmin (Nd ts); maxmin (Nd ts) ≤ b ⟧
 ⟹ maxmin (Nd ts) = mm a (abrs0 ts a b) b"
by (metis max_def min.absorb1 abr01_mm(2))

text ‹The stronger @{const fishburn} spec:›

text ‹Needs ‹a<b›.›
theorem fishburn_abr01:
  shows "a < b ⟹ fishburn a b (maxmin t)   (abr0 t a b)"
    and "a < b ⟹ fishburn a b (maxmin (Nd ts)) (abrs0 ts a b)"
    and "a > b ⟹ fishburn b a (minmax t)   (abr1 t a b)"
    and "a > b ⟹ fishburn b a (minmax (Nd ts)) (abrs1 ts a b)"
proof(induction t a b and ts a b and t a b and ts a b rule: abr0_abrs0_abr1_abrs1.induct)
  case (4 t ts a b)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, best) leI max.absorb_iff2 max.coboundedI1 max.orderE order.strict_iff_not)
next
  case (8 t ts a b)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, best) order.trans linorder_not_le min.absorb3 min.absorb_iff2 nle_le)
qed auto

text ‹Above lemma does not work for ‹a = b› and ‹a > b›.
 Not fishburn: ‹abr0 ≤ a› but not ‹maxmin ≤ abr0›.
 Not knuth: ‹abr0 ≤ a› but not ‹maxmin ≤ a››
lemma "let a = 0::ereal; t = Nd [Lf 1, Lf 0] in abr0 t a a = 0 ∧ maxmin t = 1"
by eval
lemma "let a = 0::ereal; b = -1; t = Nd [Lf 1, Lf 0] in abr0 t a b = 0 ∧ maxmin t = 1"
by eval

text ‹The following lemma does not follow from ‹fishburn› because of the weaker assumption ‹a ≤ b›
that is required for the later exactness lemma.›

lemma abr0_le_b: "⟦ a ≤ b; maxmin t ≤ b ⟧ ⟹ abr0 t a b ≤ b"
and  "⟦ a ≤ b; maxmin (Nd ts) ≤ b ⟧ ⟹ abrs0 ts a b ≤ b"
and "⟦ b ≤ minmax t; b ≤ a ⟧ ⟹ b ≤ abr1 t a b"
and  "⟦ b ≤ minmax (Nd ts); b ≤ a ⟧ ⟹ b ≤ abrs1 ts a b"
proof(induction t a b and ts a b and t a b and ts a b rule: abr0_abrs0_abr1_abrs1.induct)
  case (4 t ts a b)
  show ?case
  proof (cases t)
    case Lf
    then show ?thesis using "4.IH"(1) "4.prems" by(simp add: Let_def)
  next
    case Nd
    then show ?thesis
      apply(simp add: Let_def leI abrs1_le_a)
      using "4.IH"(1) "4.prems" by auto
  qed
next
  case (8 t ts a b)
  show ?case
  proof (cases t)
    case Lf
    then show ?thesis using "8.IH"(1) "8.prems" by(simp add: Let_def)
  next
    case Nd
    then show ?thesis
      apply(simp add: Let_def leI abrs0_ge_a)
      using "8.IH"(1) "8.prems" by auto
  qed
qed auto

lemma abr0_exact_less:
assumes "a < b" "v = maxmin t" "a ≤ v ∧ v ≤ b"
shows "abr0 t a b = v"
using fishburn_exact[OF assms(3)] fishburn_abr01[OF assms(1)] assms(2) by metis

lemma abr0_exact:
assumes "v = maxmin t" "a ≤ v ∧ v ≤ b"
shows "abr0 t a b = v"
using  abr0_exact_less abr0_le_b abrs0_ge_a assms(1,2) abr0.elims
by (smt (verit, best) dual_order.trans leD maxmin.simps(1) order_le_imp_less_or_eq)

text ‹Another proof:›
lemma abr0_exact2:
assumes "v = maxmin t" "a ≤ v ∧ v ≤ b"
shows "abr0 t a b = v"
proof (cases t)
  case Lf with assms show ?thesis by simp
next
  case Nd
  then show ?thesis using assms
    by (smt (verit, del_insts) abr0.simps(2) abr0_le_b abrs0_ge_a order.order_iff_strict order_le_less_trans fishburn_abr01(1))
(*    by (smt (verit, ccfv_threshold) abr0.simps(2) abrs0_ge_a max_def min_def abr0_le_b abr01_mm(1))*)
qed


subsubsection ‹Soft›

text ‹Starting at ‹⊥› (after Fishburn)›

fun abr0' :: "('a::bounded_linorder)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abrs0' and abr1' and abrs1' where
"abr0' (Lf x) a b = x" |
"abr0' (Nd ts) a b = abrs0' ts a b" |

"abrs0' [] a b = ⊥" |
"abrs0' (t#ts) a b = (let m = abrs0' ts a b in if m ≥ b then m else max (abr1' t b (max m a)) m)" |

"abr1' (Lf x) a b = x" |
"abr1' (Nd ts) a b = abrs1' ts a b" |

"abrs1' [] a b = ⊤" |
"abrs1' (t#ts) a b = (let m = abrs1' ts a b in if m ≤ b then m else min (abr0' t b (min m a)) m)"

theorem fishburn_abr01':
  shows "a < b ⟹ fishburn a b (maxmin t)   (abr0' t a b)"
    and "a < b ⟹ fishburn a b (maxmin (Nd ts)) (abrs0' ts a b)"
    and "a > b ⟹ fishburn b a (minmax t)   (abr1' t a b)"
    and "a > b ⟹ fishburn b a (minmax (Nd ts)) (abrs1' ts a b)"
proof(induction t a b and ts a b and t a b and ts a b rule: abr0'_abrs0'_abr1'_abrs1'.induct)
  case (4 t ts a b)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, ccfv_SIG) le_max_iff_disj linorder_not_le max.absorb3 max.absorb_iff2)
next
  case (8 t ts a b)
  then show ?case
    apply(simp add: Let_def)
    by (smt (verit, best) linorder_not_le min.absorb_iff1 min.absorb_iff2 nle_le fishburn2)
qed auto

text ‹Same as for ‹abr0›: Above lemma does not work for ‹a = b› and ‹a > b›.
 Not fishburn: ‹abr0' ≤ a› but not ‹maxmin ≤ abr0'›.
 Not knuth: ‹abr0' ≤ a› but not ‹maxmin ≤ a››
lemma "let a = 0::ereal; t = Nd [Lf 1, Lf 0] in abr0' t a a = 0 ∧ maxmin t = 1"
by eval
lemma "let a = 0::ereal; b = -1; t = Nd [Lf 1, Lf 0] in abr0' t a b = 0 ∧ maxmin t = 1"
by eval

text ‹Fails for a=b=-1 and t = Nd []›
theorem fishburn2_abr01_abr01':
  shows "a < b ⟹ fishburn a b (abr0' t a b)   (abr0 t a b)"
    and "a < b ⟹ fishburn a b (abrs0' ts a b) (abrs0 ts a b)"
    and "a > b ⟹ fishburn b a (abr1' t a b)   (abr1 t a b)"
    and "a > b ⟹ fishburn b a (abrs1' ts a b) (abrs1 ts a b)"
proof(induction t a b and ts a b and t a b and ts a b rule: abr0_abrs0_abr1_abrs1.induct)
  case (4 t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (verit) abrs0_ge_a max.absorb2 max.assoc max.commute nle_le order_le_imp_less_or_eq)
next
  case (8 t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (verit, ccfv_threshold) abrs1_le_a min.absorb_iff2 min.bounded_iff nle_le order.strict_iff_order)
qed auto

text ‹Towards `exactness':›

text ‹No need for restricting ‹a,b›, but only corollaries:›
corollary abr0'_mm: "mm a (abr0' t a b) b = mm a (maxmin t) b"
by (smt (verit) max.absorb1 max.cobounded2 max.strict_order_iff min.absorb2 min.absorb3 min.cobounded1 mm_if_knuth fishburn_abr01'(1))
corollary abrs0'_mm: "mm a (abrs0' ts a b) b = mm a (maxmin (Nd ts)) b"
by (metis abr0'.simps(2) abr0'_mm)
corollary abr1'_mm: "mm b (abr1' t a b) a = mm b (minmax t) a"
by (smt (verit, best) linorder_not_le max.absorb1 max_less_iff_conj min.absorb2 fishburn_abr01'(3))
corollary abrs1'_mm: "mm b (abrs1' ts a b) a = mm b (minmax (Nd ts)) a"
by (metis abr1'.simps(2) abr1'_mm)

corollary li1: "⟦ a ≤ maxmin t;  maxmin t ≤ b⟧ ⟹ mm a (abr0' t a b) b = maxmin t"
  by (simp add: abr0'_mm)

text ‹Note the ‹a ≤ b› instead of the ‹a < b› in @{thm fishburn_abr01'}:›

lemma abr01'lb_ub:
shows "a ≤ b ⟹ lb_ub a b (maxmin t)   (abr0' t a b)"
  and "a ≤ b ⟹ lb_ub a b (maxmin (Nd ts)) (abrs0' ts a b)"
  and "a ≥ b ⟹ lb_ub b a (minmax t)   (abr1' t a b)"
  and "a ≥ b ⟹ lb_ub b a (minmax (Nd ts)) (abrs1' ts a b)"
apply(induction t a b and ts a b and t a b and ts a b rule: abr0'_abrs0'_abr1'_abrs1'.induct)
by(auto simp add: Let_def le_max_iff_disj  min_le_iff_disj)

lemma abr0'_exact_less: "⟦ a<b; v = maxmin t; a ≤ v ∧ v ≤ b ⟧ ⟹ abr0' t a b = v"
using fishburn_abr01'(1) by force

lemma abr0'_exact: "⟦ v = maxmin t; a ≤ v ∧ v ≤ b⟧ ⟹ abr0' t a b = v"
by (metis abr0'_exact_less abr01'lb_ub(1) order.trans leD order_le_imp_less_or_eq)


subsubsection ‹Also returning the searched tree›

text ‹Hard:›

fun abtr0 :: "('a::linorder) tree ⇒ 'a ⇒ 'a ⇒ 'a * 'a tree" and abtrs0 and abtr1 and abtrs1 where
"abtr0 (Lf x) a b = (x, Lf x)" |
"abtr0 (Nd ts) a b = (let (m,us) = abtrs0 ts a b in (m, Nd us))" |

"abtrs0 [] a b = (a,[])" |
"abtrs0 (t#ts) a b = (let (m,us) = abtrs0 ts a b in
  if m ≥ b then (m,us) else let (n,u) = abtr1 t b m in (max n m,u#us))" |

"abtr1 (Lf x) a b = (x, Lf x)" |
"abtr1 (Nd ts) a b = (let (m,us) = abtrs1 ts a b in (m, Nd us))" |

"abtrs1 [] a b = (a,[])" |
"abtrs1 (t#ts) a b = (let (m,us) = abtrs1 ts a b in
  if m ≤ b then (m,us) else let (n,u) = abtr0 t b m in (min n m,u#us))"

text ‹Soft:›

fun abtr0' :: "('a::bounded_linorder) tree ⇒ 'a ⇒ 'a ⇒ 'a * 'a tree" and abtrs0' and abtr1' and abtrs1' where
"abtr0' (Lf x) a b = (x, Lf x)" |
"abtr0' (Nd ts) a b = (let (m,us) = abtrs0' ts a b in (m, Nd us))" |

"abtrs0' [] a b = (⊥,[])" |
"abtrs0' (t#ts) a b = (let (m,us) = abtrs0' ts a b in
  if m ≥ b then (m,us) else let (n,u) = abtr1' t b (max m a) in (max n m,u#us))" |

"abtr1' (Lf x) a b = (x, Lf x)" |
"abtr1' (Nd ts) a b = (let (m,us) = abtrs1' ts a b in (m, Nd us))" |

"abtrs1' [] a b = (⊤,[])" |
"abtrs1' (t#ts) a b = (let (m,us) = abtrs1' ts a b in
  if m ≤ b then (m,us) else let (n,u) = abtr0' t b (min m a) in (min n m,u#us))"

lemma fst_abtr01:
shows "fst(abtr0 t a b) = abr0 t a b"
and "fst(abtrs0 ts a b) = abrs0 ts a b"
and "fst(abtr1 t a b) = abr1 t a b"
and "fst(abtrs1 ts a b) = abrs1 ts a b"
by(induction t a b and ts a b and t a b and ts a b rule: abtr0_abtrs0_abtr1_abtrs1.induct)
  (auto simp: Let_def split: prod.split)

lemma fst_abtr01':
shows "fst(abtr0' t a b) = abr0' t a b"
and "fst(abtrs0' ts a b) = abrs0' ts a b"
and "fst(abtr1' t a b) = abr1' t a b"
and "fst(abtrs1' ts a b) = abrs1' ts a b"
by(induction t a b and ts a b and t a b and ts a b rule: abtr0'_abtrs0'_abtr1'_abtrs1'.induct)
  (auto simp: Let_def split: prod.split)

lemma snd_abtr01'_abtr01:
shows "a < b ⟹ snd(abtr0' t a b) = snd(abtr0 t a b)"
and "a < b ⟹ snd(abtrs0' ts a b) = snd(abtrs0 ts a b)"
and "a > b ⟹ snd(abtr1' t a b) = snd(abtr1 t a b)"
and "a > b ⟹ snd(abtrs1' ts a b) = snd(abtrs1 ts a b)"
proof(induction t a b and ts a b and t a b and ts a b rule: abtr0'_abtrs0'_abtr1'_abtrs1'.induct)
  case (4 t ts a b)
  then show ?case
    apply(simp add: Let_def split: prod.split)
    using fst_abtr01(2) fst_abtr01'(2) fishburn2_abr01_abr01'(2) abrs0_ge_a
    by (smt (verit, best) fst_conv le_max_iff_disj linorder_not_le max.absorb1 nle_le sndI)
next
  case (8 t ts a b)
  then show ?case
    apply(simp add: Let_def split: prod.split)
    using fst_abtr01(4) fst_abtr01'(4) fishburn2_abr01_abr01'(4) abrs1_le_a
    by (smt (verit, ccfv_threshold) fst_conv linorder_not_le min.absorb1 min.absorb_iff2 order.strict_trans2 snd_conv)
qed (auto simp add: split_beta)


subsubsection ‹Generalized›

text ‹General version due to Junkang Li et al.:›

locale SoftGeneral =
fixes i0 i1 :: "'a::bounded_linorder tree list ⇒ 'a ⇒ 'a"
assumes i0: "i0 ts a ≤ max a (maxmin(Nd ts))" and i1: "i1 ts a ≥ min a (minmax (Nd ts))"
begin

fun abir0' :: "('a::bounded_linorder)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abirs0' and abir1' and abirs1' where
"abir0' (Lf x) a b = x" |
"abir0' (Nd ts) a b = abirs0' (i0 ts a) ts a b" |

"abirs0' i [] a b = i" |
"abirs0' i (t#ts) a b =
  (let m = abirs0' i ts a b in if m ≥ b then m else max (abir1' t b (max m a)) m)" |

"abir1' (Lf x) a b = x" |
"abir1' (Nd ts) a b = abirs1' (i1 ts a) ts a b" |

"abirs1' i [] a b = i" |
"abirs1' i (t#ts) a b =
  (let m = abirs1' i ts a b in if m ≤ b then m else min (abir0' t b (min m a)) m)"

text ‹Unused:›
lemma abirs0'_ge_i: "abirs0' i ts a b ≥ i"
apply(induction ts)
by (auto simp: Let_def) (metis max.coboundedI2)

lemma abirs1'_le_i: "abirs1' i ts a b ≤ i"
apply(induction ts)
by (auto simp: Let_def) (metis min.coboundedI2)

lemma fishburn_abir01':
  shows "a < b ⟹ fishburn a b (maxmin t)           (abir0' t a b)"
    and "a < b ⟹ fishburn a b (max i (maxmin (Nd ts))) (abirs0' i ts a b)"
    and "a > b ⟹ fishburn b a (minmax t)           (abir1' t a b)"
    and "a > b ⟹ fishburn b a (min i (minmax (Nd ts))) (abirs1' i ts a b)"
proof(induction t a b and i ts a b and t a b and i ts a b rule: abir0'_abirs0'_abir1'_abirs1'.induct)
  case (2 ts a b)
  thus ?case using i0[of ts a] apply simp
    by (smt (verit, best) leD le_max_iff_disj max_def)
next
  case (4 i t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (z3) linorder_not_le max.coboundedI2 max_def nle_le)
next
  case (6 ts a b)
  thus ?case
    using i1[of a ts] apply simp by (smt (verit, del_insts) leD min_le_iff_disj nle_le)
next
  case (8 i t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (verit, ccfv_SIG) linorder_not_le min.absorb2 min_le_iff_disj nle_le)
qed auto

text ‹Note the ‹a ≤ b› instead of the ‹a < b› in @{thm fishburn_abir01'}:›

lemma abir0'lb_ub:
shows "a ≤ b ⟹ lb_ub a b (maxmin t) (abir0' t a b)"
and "a ≤ b ⟹ lb_ub a b (max i (maxmin (Nd ts))) (abirs0' i ts a b)"
and "a ≥ b ⟹ lb_ub b a (minmax t) (abir1' t a b)"
and "a ≥ b ⟹ lb_ub b a (min i (minmax (Nd ts))) (abirs1' i ts a b)"
  by(induction t a b and i ts a b and t a b and i ts a b rule: abir0'_abirs0'_abir1'_abirs1'.induct)
    (auto simp add: Let_def le_max_iff_disj  min_le_iff_disj
      intro: order_trans[OF i0] order_trans[OF _ i1])

lemma abir0'_exact_less: "⟦ a<b; v = maxmin t; a ≤ v ∧ v ≤ b ⟧ ⟹ abir0' t a b = v"
using fishburn_abir01'(1) by force

lemma abir0'_exact: "⟦ v = maxmin t; a ≤ v ∧ v ≤ b⟧ ⟹ abir0' t a b = v"
by (metis abir0'_exact_less abir0'lb_ub(1) order.trans leD order_le_imp_less_or_eq)

end

text ‹Now with explicit parameters ‹i0› and ‹i1› such that we can vary them:›

fun abir0' :: "_ ⇒ _ ⇒ ('a::bounded_linorder)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abirs0' and abir1' and abirs1' where
"abir0' i0 i1 (Lf x) a b = x" |
"abir0' i0 i1 (Nd ts) a b = abirs0' i0 i1 (i0 ts a) ts a b" |

"abirs0' i0 i1 i [] a b = i" |
"abirs0' i0 i1 i (t#ts) a b =
  (let m = abirs0' i0 i1 i ts a b in if m ≥ b then m else max (abir1' i0 i1 t b (max m a)) m)" |

"abir1' i0 i1 (Lf x) a b = x" |
"abir1' i0 i1 (Nd ts) a b = abirs1' i0 i1 (i1 ts a) ts a b" |

"abirs1' i0 i1 i [] a b = i" |
"abirs1' i0 i1 i (t#ts) a b =
  (let m = abirs1' i0 i1 i ts a b in if m ≤ b then m else min (abir0' i0 i1 t b (min m a)) m)"

text ‹First, the same theorem as in the locale ‹SoftGeneral›:›

definition "bnd i0 i1 ≡
  ∀ts a. i0 ts a ≤ max a (maxmin(Nd ts)) ∧ i1 ts a ≥ min a (minmax (Nd ts))"

declare [[unify_search_bound=400,unify_trace_bound=400]] (* Because of complex induction rules *)

lemma fishburn_abir01':
  shows "a < b ⟹ bnd i0 i1 ⟹ fishburn a b (maxmin t)           (abir0' i0 i1 t a b)"
    and "a < b ⟹ bnd i0 i1 ⟹ fishburn a b (max i (maxmin (Nd ts))) (abirs0' i0 i1 i ts a b)"
    and "a > b ⟹ bnd i0 i1 ⟹ fishburn b a (minmax t)           (abir1' i0 i1 t a b)"
    and "a > b ⟹ bnd i0 i1 ⟹ fishburn b a (min i (minmax (Nd ts))) (abirs1' i0 i1 i ts a b)"
proof(induction i0 i1 t a b and i0 i1 i ts a b and i0 i1 t a b and i0 i1 i ts a b
      rule: abir0'_abirs0'_abir1'_abirs1'.induct)
  case (2 ts a b)
  thus ?case unfolding bnd_def apply simp
    by (smt (verit, best) leD le_max_iff_disj max_def)
next
  case (4 i t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (z3) linorder_not_le max.coboundedI2 max_def nle_le)
next
  case (6 ts a b)
  thus ?case
    unfolding bnd_def apply simp
    by (smt (verit, ccfv_threshold) linorder_not_le min.absorb2 min_def min_le_iff_disj)
next
  case (8 i t ts a b)
  thus ?case apply (simp add: Let_def)
    by (smt (verit, ccfv_SIG) linorder_not_le min.absorb2 min_le_iff_disj nle_le)
qed (auto)

text ‹Unused:›
lemma abirs0'_ge_i: "abirs0' i0 i1 i ts a b ≥ i"
by(induction ts) (auto simp: Let_def max.coboundedI2)

lemma abirs0'_eq_i: "i ≥ b ⟹ abirs0' i0 i1 i ts a b = i"
by(induction ts) (auto simp: Let_def)

lemma abirs1'_le_i: "abirs1' i0 i1 i ts a b ≤ i"
by(induction ts) (auto simp: Let_def min.coboundedI2)


text ‹Monotonicity wrt the init functions, below/above ‹a›:›

definition "bnd_mono i0 i1 i0' i1' =
 (∀ts a. i0' ts a ≤ a ∧ i1' ts a ≥ a ∧ i0 ts a ≤ i0' ts a ∧ i1 ts a ≥ i1' ts a)"

lemma fishburn_abir0'_mono: 
shows "a < b ⟹ bnd_mono i0 i1 i0' i1' ⟹ fishburn a b (abir0' i0 i1 t a b) (abir0' i0' i1' t a b)"
  and "a < b ⟹ bnd_mono i0 i1 i0' i1' ⟹ i = i0 (ts0 @ ts) a ⟹
        fishburn a b (abirs0' i0 i1 i ts a b) (abirs0' i0' i1' (i0' (ts0 @ ts) a) ts a b)"
 and "a > b ⟹ bnd_mono i0 i1 i0' i1' ⟹ fishburn b a (abir1' i0 i1 t a b) (abir1' i0' i1' t a b)"
 and "a > b ⟹ bnd_mono i0 i1 i0' i1' ⟹ i = i1 (ts0@ts) a ⟹
        fishburn b a (abirs1' i0 i1 i ts a b) (abirs1' i0' i1' (i1' (ts0 @ ts) a) ts a b)"
proof(induction i0 i1 t a b and i0 i1 i ts a b and i0 i1 t a b and i0 i1 i ts a b
    arbitrary: i0' i1' and i0' i1' ts0 and i0' i1' and i0' i1' ts0
    rule: abir0'_abirs0'_abir1'_abirs1'.induct)
  case 1
  then show ?case by simp
next
  case 2
  then show ?case by (metis abir0'.simps(2) append_Nil)
next
  case 3
  then show ?case unfolding bnd_mono_def
    apply simp by (metis order.strict_trans1 leD)
next
  case (4 i0 i1 i t ts a b)
  show ?case
    using "4.prems" "4.IH"(2)[OF refl, of i0' i1'] "4.IH"(1)[OF ‹a<b›, of i0' i1' "ts0 @ [t]"]
    by (smt (z3) Cons_eq_appendI abirs0'.simps(2) append_eq_append_conv2 append_self_conv linorder_not_less max_def_raw nless_le order.strict_trans1)
next
  case 5
  then show ?case by simp
next
  case 6
  then show ?case by (metis abir1'.simps(2) append_Nil)
next
  case 7
  then show ?case unfolding bnd_mono_def
    apply simp by (metis leD order_le_less_trans)
next
  case (8 i0 i1 i t ts a b)
  then show ?case
    using "8.prems" "8.IH"(2)[OF refl, of i0' i1'] "8.IH"(1)[OF ‹a>b›, of i0' i1' "ts0 @ [t]"]
    by (smt (verit) Cons_eq_appendI abirs1'.simps(2) append_eq_append_conv2 linorder_le_less_linear min.absorb2 min.absorb3 min.order_iff min_less_iff_conj self_append_conv)
qed

text ‹The ‹i0› bound of ‹a› cannot be increased to ‹max a (maxmin(Nd ts)›
(as the theorem ‹fishburn_abir0'› might suggest).
Problem: if ‹b ≤ i0 a ts < i0' a ts› then it can happen that
  ‹b ≤ abirs0' i0 i1 t a b < abirs0' i0' i1' t a b›, which violates ‹fishburn›.›

value "let  a = - ∞; b = 0::ereal; t = Nd [Lf (1::ereal)] in
 (abir0' (λts a. max a (maxmin(Nd ts))) i1' t a b,
  abir0' (λts a. max a (maxmin(Nd ts))-1) i1 t a b)"

lemma "let  a = - ∞; b = 0::ereal; ts = [Lf (1::ereal)] in
  abirs0' (λts a. max a (maxmin(Nd ts))-1) (λ_ a. a+1) (max a (maxmin(Nd ts))-1) ts a b = 0"
unfolding Let_def
using [[simp_trace]] by (simp add:Let_def)



section ‹Alpha-Beta for De Morgan Orders›

subsection ‹From the Left, Fail-Hard›

text ‹Like Knuth.›

fun ab_negmax :: "'a ⇒ 'a ⇒ ('a::de_morgan_order)tree ⇒ 'a" and ab_negmaxs where
"ab_negmax a b (Lf x) = x" |
"ab_negmax a b (Nd ts) = ab_negmaxs a b ts" |

"ab_negmaxs a b [] = a" |
"ab_negmaxs a b (t#ts) = (let a' = max a (- ab_negmax (-b) (-a) t) in if a' ≥ b then a' else ab_negmaxs a' b ts)"

text ‹Via ‹foldl›. Wasteful: ‹foldl› consumes whole list.›

definition ab_negmaxf :: "('a::de_morgan_order) ⇒ 'a ⇒ 'a tree ⇒ 'a" where
"ab_negmaxf b = (λa t. if a ≥ b then a else max a (- ab_negmax (-b) (-a) t))"

lemma foldl_ab_negmaxf_idemp:
  "b ≤ a ⟹ foldl (ab_negmaxf b) a ts = a"
by(induction ts) (auto simp: ab_negmaxf_def)

lemma ab_negmaxs_foldl:
  "(a::'a::de_morgan_order) < b ⟹ ab_negmaxs a b ts = foldl (ab_negmaxf b) a ts"
using foldl_ab_negmaxf_idemp[where 'a='a]
by(induction ts arbitrary: a) (auto simp: ab_negmaxf_def Let_def dest: not_le_imp_less)

text ‹Also returning the searched tree.›

(*TODO: mk ab_negmax, add ab_negmax', finish proofs*)fun abtl :: "'a ⇒ 'a ⇒ ('a::de_morgan_order)tree ⇒ 'a * ('a::de_morgan_order)tree" and abtls where
"abtl a b (Lf x) = (x, Lf x)" |
"abtl a b (Nd ts) = (let (m,us) = abtls a b ts in (m, Nd us))" |

"abtls a b [] = (a,[])" |
"abtls a b (t#ts) = (let (a',u) = abtl (-b) (-a) t; a' = max a (-a') in
  if a' ≥ b then (a',[u]) else let (n,us) = abtls a' b ts in (n,u#us))"

lemma fst_abtl:
shows "fst(abtl a b t) = ab_negmax a b t"
and "fst(abtls a b ts) = ab_negmaxs a b ts"
by(induction a b t and a b ts rule: abtl_abtls.induct)
  (auto simp: Let_def split: prod.split)

subsubsection "Correctness Proofs"

text ‹First, a very direct proof.›

lemma ab_negmaxs_ge_a: "ab_negmaxs a b ts ≥ a"
apply(induction ts arbitrary: a)
by (auto simp: Let_def) (metis max.bounded_iff)

lemma fishburn_val_ab_neg:
shows "a < b ⟹ fishburn a b (negmax t) (ab_negmax (a) b t)"
and "a < b ⟹ fishburn a b (negmax (Nd ts)) (ab_negmaxs (a) b ts)"
proof(induction a b t and a b ts rule: ab_negmax_ab_negmaxs.induct)
  case (4 a b t ts)
  then show ?case
    apply(simp add: Let_def less_uminus_reorder)
    by (smt (verit, ccfv_threshold) ab_negmaxs_ge_a le_max_iff_disj linorder_not_le minus_less_minus nle_le uminus_less_reorder)
qed auto

text "Now an indirect one by reduction to the min/max alpha-beta. Direct proof is simpler!"

text ‹Relate ordinary and negmax ab:›
theorem ab_max_negmax:
shows "ab_max a b t = ab_negmax a b (negate False t)"
and   "ab_maxs a b ts = ab_negmaxs a b (map (negate True) ts)"
and   "ab_min a b t = - ab_negmax (-b) (-a) (negate True t)"
and   "ab_mins a b ts = - ab_negmaxs (-b) (-a) (map (negate False) ts)"
proof(induction a b t and a b ts and a b t and a b ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  case 8
  then show ?case by(simp add: Let_def de_morgan_max de_morgan_min uminus_le_reorder)
qed (simp_all add: Let_def)

corollary fishburn_negmax_ab_negmax: "a < b ⟹ fishburn a b (negmax t) (ab_negmax a b t)"
using fishburn_val_ab(1) ab_max_negmax(1) negmax_maxmin(1) negate_negate
by (metis (no_types, lifting))

(*
Currently unused and can be proved equationally from earlier lemmas.
Might come in useful if one tries to interconnect the ab-variants in a different order.
*)
lemma ab_negmax_ab_le:
  shows "ab_negmax a b t = ab_le (≤) a b (negate False t)"
  and   "ab_negmaxs a b ts = ab_les (≤) a b (map (negate True) ts)"
  and   "ab_negmax a b t = - ab_le (≥) (-a) (-b) (negate True t)"
  and   "ab_negmaxs a b ts = - ab_les (≥) (-a) (-b) (map (negate False) ts)"
by(induction a b t and a b ts and b a t and b a ts rule: ab_max_ab_maxs_ab_min_ab_mins.induct)
  (auto simp add: Let_def max_def ab_max_ab_le[symmetric] ab_max_negmax negate_negate o_def)

text ‹Pointless? Weaker than fishburn and direct proof rather than corollary as via ‹ab_max_negmax››
text ‹Weaker max-min property. Proof: Case False one eqn chain, but dualized IH:›
theorem
shows ab_negmax_negmax2: "max a (min (ab_negmax a b t) b) = max a (min (negmax t) b)"
and ab_negmaxs_maxs_neg3: "a < b ⟹ min (ab_negmaxs a b ts) b = max a (min (negmax (Nd ts)) b)"
proof(induction a b t and a b ts rule: ab_negmax_ab_negmaxs.induct)
  case 2
  thus ?case apply simp
    by (metis leI max_absorb1 max_def min.coboundedI2)
next
  case (4 a b t ts)
  let ?abt = "ab_negmax (- b) (- a) t" let ?a' = "max a (- ?abt)"
  let ?T = "negmax t" let ?S = "negmax (Nd ts)"
  show ?case
(* apply (simp add: Let_def) using 4
    by (smt (verit) ereal_minus_less_minus ereal_uminus_less_reorder linorder_neq_iff linorder_not_le max.absorb3 max.absorb4 max.absorb_iff2 min.absorb3 min.absorb4 min_less_iff_conj)
*)
  proof (cases "b ≤ ?a'")
    case True
    have "min b (max (-?abt) a) = min b (max (- ?T) a)" using "4.IH"(1) "4.prems"
      by (metis (no_types) neg_neg de_morgan_min)
    hence "b = min b (max (- ?T) a)" using True
      by (metis max.commute min.orderE)
    hence "b ≤ max (- ?T) a"
      by (metis min.cobounded2)
    hence b: "b ≤ - ?T"
      by (meson "4.prems" leD le_max_iff_disj)
    have "min (ab_negmaxs a b (t # ts)) b = min ?a' b"
      using True by simp
    also have "… = b"
      using True min.absorb2 by blast
    also have "… = max a (max (min (- ?T) b) (min ?S b))"
      using b "4.prems" by simp
    also have "… = max a (min (max (- ?T) ?S) b)"
      by (metis min_max_distrib1)
    also have "… = max a (min (negmax (Nd (t # ts))) b)"
      by simp
    finally show ?thesis .
  next
    case False
    hence 1: "- ?abt < b"
      by (metis le_max_iff_disj linorder_not_le)
    have IH1: "max a (min (- ?abt) b) = max a (min (- ?T) b)"
      using "4.IH"(1) ‹a<b› by (metis max_min_neg neg_neg)
    have "min (ab_negmaxs a b (t # ts)) b = min (ab_negmaxs (max a (- ?abt)) b ts) b"
      using False by(simp)
    also have "… = max (max a (- ?abt)) (min ?S b)"
      using "4.IH"(2) "4.prems" 1 False by(simp)
    also have "… = max (max a (min (-?abt) b)) (max a (min ?S b))"
      using 1 by (simp add: max.assoc max.left_commute)
    also have "… = max (max a (min (- ?T) b)) (max a (min ?S b))"
      using IH1 by presburger
    also have "… = max a (min (max (- ?T) ?S) b)"
      by (metis (no_types, lifting) max.assoc max.commute max.right_idem min_max_distrib1)
    also have "… =  max a (min (negmax (Nd (t # ts))) b)" by simp
    finally show ?thesis .
  qed
qed auto

corollary ab_negmax_negmax_cor2: "ab_negmax ⊥ ⊤ t = negmax t"
using ab_negmax_negmax2[of ⊥ ⊤ t] by (simp)


subsection ‹From the Left, Fail-Soft›

text ‹After Fishburn›

fun ab_negmax' :: "'a ⇒ 'a ⇒ ('a::de_morgan_order)tree ⇒ 'a" and ab_negmaxs' where
"ab_negmax' a b (Lf x) = x" |
"ab_negmax' a b (Nd ts) = (ab_negmaxs' a b ⊥ ts)" |

"ab_negmaxs' a b m [] = m" |
"ab_negmaxs' a b m (t#ts) = (let m' = max m (- ab_negmax' (-b) (- max m a) t) in
      if m' ≥ b then m' else ab_negmaxs' a b m' ts)"

lemma ab_negmaxs'_ge_a: "ab_negmaxs' a b m ts ≥ m"
apply(induction ts arbitrary: a b m)
by (auto simp: Let_def) (metis max.bounded_iff)

(* TODO? readble proofs *)

theorem fishburn_val_ab_neg':
shows "a < b ⟹ fishburn a b (negmax t) (ab_negmax' a b t)"
  and "max a m < b ⟹ fishburn (max a m) b (negmax (Nd ts)) (ab_negmaxs' a b m ts)"
proof(induction a b t and a b m ts rule: ab_negmax'_ab_negmaxs'.induct)
  case (4 a b m t ts)
  then show ?case
    apply (simp add: Let_def)
    by (smt (verit, del_insts) ab_negmaxs'_ge_a minus_le_minus uminus_le_reorder linorder_not_le max.absorb1 max.absorb4 max.coboundedI2 max.commute)
qed auto

(* Trickier than r version ‹fishburn_abr_abr'› below because of additional parameter m;
   does not look like one could simplify matters by porting r to l via mirror *)
theorem fishburn_ab'_ab_neg:
shows "a < b ⟹ fishburn a b (ab_negmax' a b t) (ab_negmax a b t)"
  and "max m a < b ⟹ fishburn a b (ab_negmaxs' a b m ts) (ab_negmaxs (max m a) b ts)"
proof(induction a b t and a b m ts rule: ab_negmax'_ab_negmaxs'.induct)
  case 1
  then show ?case by auto
next
  case 2
  then show ?case
    by fastforce
next
  case 3
  then show ?case apply simp
    by (metis linorder_linear linorder_not_le max.commute max.orderE)
next
  case (4 a b m t ts)
  then show ?case
    apply (simp)
    by (smt (verit) minus_le_minus neg_neg leD linorder_le_less_linear linorder_linear max.absorb_iff1 max.assoc max.commute nle_le)
qed

text ‹Another proof of ‹fishburn_negmax_ab_negmax›, just by transitivity:›
corollary "a < b ⟹ fishburn a b (negmax t) (ab_negmax a b t)"
by(rule trans_fishburn[OF fishburn_val_ab_neg'(1) fishburn_ab'_ab_neg(1)])

text ‹Now fail-soft with traversed trees.›

fun abtl' :: "'a ⇒ 'a ⇒ ('a::de_morgan_order)tree ⇒ 'a * ('a::de_morgan_order)tree" and abtls' where
"abtl' a b (Lf x) = (x, Lf x)" |
"abtl' a b (Nd ts) = (let (m,us) = abtls' a b ⊥ ts in (m, Nd us))" |

"abtls' a b m [] = (m,[])" |
"abtls' a b m (t#ts) = (let (m',u) = abtl' (-b) (- max m a) t; m' = max m (- m') in
      if m' ≥ b then (m',[u]) else let (n,us) = abtls' a b m' ts in (n,u#us))"

lemma fst_abtl':
shows "fst(abtl' a b t) = ab_negmax' a b t"
and "fst(abtls' a b m ts) = ab_negmaxs' a b m ts"
by(induction a b t and a b m ts rule: abtl'_abtls'.induct)
  (auto simp: Let_def split: prod.split)

text ‹Fail-hard and fail-soft search the same part of the tree:›

lemma snd_abtl'_abtl:
shows "a < b ⟹ abtl' a b t = (ab_negmax' a b t, snd(abtl a b t))"
and "max m a < b ⟹ abtls' a b m ts = (ab_negmaxs' a b m ts, snd(abtls (max m a) b ts))"
proof(induction a b t and a b m ts rule: abtl'_abtls'.induct)
  case (4 t ts a b)
  then show ?case
    apply(simp add: Let_def split: prod.split)
    by (smt (verit) fishburn_ab'_ab_neg(1) fst_abtl(1) fst_conv linorder_neq_iff max.absorb3 max.cobounded2 max.coboundedI2 max_def minus_less_minus snd_conv uminus_less_reorder)
qed (auto simp add: split_beta)


subsubsection "‹min›/‹max› in ‹Lf›"

fun ab_negmax2 :: " ('a::de_morgan_order) ⇒ 'a ⇒ 'a tree ⇒ 'a" and ab_negmaxs2 where
"ab_negmax2 a b (Lf x) = max a (min x b)" |
"ab_negmax2 a b (Nd ts) = ab_negmaxs2 a b ts" |

"ab_negmaxs2 a b [] = a" |
"ab_negmaxs2 a b (t#ts) = (let a' = - ab_negmax2 (-b) (-a) t in if a' = b then a' else ab_negmaxs2 a' b ts)"

lemma ab_negmax2_max_min_negmax:
shows "a < b ⟹ ab_negmax2 a b t = max a (min (negmax t) b)"
and "a < b ⟹ ab_negmaxs2 a b ts = max a (min (negmax (Nd ts)) b)"
proof(induction a b t and a b ts rule: ab_negmax2_ab_negmaxs2.induct)
next
  case 4 thus ?case
    apply (simp add: Let_def)
    by (smt (z3) de_morgan_max le_max_iff_disj linorder_not_le max.commute max_def neg_neg uminus_less_reorder)
qed auto

corollary ab_negmax2_bot_top: "ab_negmax2 ⊥ ⊤ t = negmax t"
by (metis ab_negmax2_max_min_negmax(1) bounded_linorder_collapse max_bot min_top2)


subsubsection "Delayed test"

text ‹Now a variant that delays the test to the next call of ‹ab_negmaxs›.
Like Bird and Hughes' version, except that ‹ab_negmax3› does not cut off the return value.›

fun ab_negmax3 :: "('a::de_morgan_order) ⇒ 'a ⇒ 'a tree ⇒ 'a" and ab_negmaxs3 where
"ab_negmax3 a b (Lf x) = x" |
"ab_negmax3 a b (Nd ts) = ab_negmaxs3 a b ts" |

"ab_negmaxs3 a b [] = a" |
"ab_negmaxs3 a b (t#ts) = (if a ≥ b then a else ab_negmaxs3 (max a (- ab_negmax3 (-b) (-a) t)) b ts)"

lemma ab_negmax3_ab_negmax:
shows "a<b ⟹ ab_negmax3 a b t = ab_negmax a b t"
and "a<b ⟹ ab_negmaxs3 a b ts = ab_negmaxs a b ts"
proof(induction a b t and a b ts rule: ab_negmax3_ab_negmaxs3.induct)
  case (4 a b t ts)
  show ?case
  proof (cases ts)
    case Nil
    then show ?thesis using 4 by (simp add: Let_def)
  next
    case Cons
    then show ?thesis using 4 by (auto simp add: Let_def le_max_iff_disj)
  qed
qed auto

corollary ab_negmax3_bot_top: "ab_negmax3 ⊥ ⊤ t = negmax t"
by(metis fishburn_negmax_ab_negmax ab_negmax3_ab_negmax(1) bounded_linorder_collapse fishburn_bot_top)

lemma ab_negmaxs3_foldl:
  "ab_negmaxs3 a b ts = foldl (λa t. if a ≥ b then a else max a (- ab_negmax3 (-b) (-a) t)) a ts"
apply(induction ts arbitrary: a)
by (auto simp: Let_def) (metis ab_negmaxs3.elims)


subsection ‹From the Right, Fail-Hard›

fun abr :: "('a::de_morgan_order)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abrs where
"abr (Lf x) a b = x" |
"abr (Nd ts) a b = abrs ts a b" |

"abrs [] a b = a" |
"abrs (t#ts) a b = (let m = abrs ts a b in if m ≥ b then m else max (- abr t (-b) (-m)) m)"

lemma Lf_eq_negateD: "Lf x = negate f t ⟹ t = Lf(if f then -x else x)"
by(cases t) auto

lemma Nd_eq_negateD: "Nd ts' = negate f t ⟹ ∃ts. t = Nd ts ∧ ts' = map (negate (¬f)) ts"
by(cases t) (auto simp: comp_def cong: map_cong)

lemma abr01_negate:
shows "abr0 (negate f t) a b = - abr1 (negate (¬f) t) (-a) (-b)"
and  "abrs0 (map (negate f) ts) a b = - abrs1 (map (negate (¬f)) ts) (-a) (-b)"
and "abr1 (negate f t) a b = - abr0 (negate (¬f) t) (-a) (-b)"
and  "abrs1 (map (negate f) ts) a b = - abrs0 (map (negate (¬f)) ts) (-a) (-b)"
proof(induction "negate f t" a b and "map (negate f) ts" a b and "negate f t" a b and "map (negate f) ts" a b arbitrary: f t and f ts and f t and f ts rule: abr0_abrs0_abr1_abrs1.induct)
  case (1 x a b)
  from Lf_eq_negateD[OF this] show ?case by simp
next
  case (2 ts a b)
  from Nd_eq_negateD[OF 2(2)] 2(1) show ?case by auto
next
  case (3 a b)
  then show ?case by simp
next
  case (4 t ts a b)
  from Cons_eq_map_D[OF 4(3)] 4(1) 4(2)[OF refl] show ?case
    by (auto simp: Let_def de_morgan_min) (metis neg_neg uminus_le_reorder)+
next
  case (5 x a b)
  from Lf_eq_negateD[OF this] show ?case by simp
next
  case (6 ts a b)
  from Nd_eq_negateD[OF 6(2)] 6(1) show ?case by auto
next
  case (7 a b)
  then show ?case by simp
next
  case (8 t ts a b)
  from Cons_eq_map_D[OF 8(3)] 8(1) 8(2)[OF refl] show ?case
    by (auto simp: Let_def de_morgan_max uminus_le_reorder)
qed

lemma abr_abr0:
 shows "abr t a b = abr0 (negate False t) a b"
 and "abrs ts a b = abrs0 (map (negate True) ts) a b"
proof (induction t a b and ts a b rule: abr_abrs.induct)
  case (1 x a b)
  then show ?case by simp
next
  case (2 ts a b)
  then show ?case by simp
next
  case (3 a b)
  then show ?case by simp
next
  case (4 t ts a b)
  then show ?case
    by (simp add: Let_def abr01_negate(3))
qed

subsubsection ‹Relationship to ‹foldr››

fun foldr :: "('a ⇒ 'b ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b" where
"foldr f v [] = v" |
"foldr f v (x#xs) = f x (foldr f v xs)"

definition "abrsf b = (λt m. if m ≥ b then m else max (- abr t (-b) (-m)) m)"

lemma abrs_foldr: "abrs ts a b = foldr (abrsf b) a ts"
by(induction ts arbitrary: a) (auto simp: abrsf_def Let_def)

text ‹A direct (rather than mutually) recursive def of ‹abr››
lemma abr_Nd_foldr:
  "abr (Nd ts) a b = foldr (abrsf b) a ts"
by (simp add: abrs_foldr)

text ‹Direct correctness proof of ‹foldr› version is no simpler than proof via ‹abr/abrs›:›

lemma fishburn_abr_foldr: "a < b ⟹ fishburn a b (negmax t) (abr t a b)"
proof(induction t arbitrary: a b)
  case (Lf)
  then show ?case by simp
next
  case (Nd ts)
  then show ?case
  proof(induction ts)
    case Nil
    then show ?case apply simp using linorder_not_less by blast
  next
    case (Cons t ts)
    then show ?case using Nd
      apply (simp add: abrsf_def abr_Nd_foldr)
      by (smt (verit) max.absorb3 max.bounded_iff max.commute minus_le_minus nle_le nless_le uminus_less_reorder)
  qed
qed


text ‹The long proofs that follows are duplicated from the ‹bounded_linorder› section.›

subsubsection ‹‹fishburn› Proofs›

lemma abrs_ge_a: "abrs ts a b ≥ a"
by (simp add: abr_abr0(2) abrs0_ge_a)

text ‹Automatic correctness proof, also works for @{const knuth} instead of @{const fishburn}:›

corollary fishburn_abr_negmax:
  shows "a < b ⟹ fishburn a b (negmax t)   (abr t a b)"
    and "a < b ⟹ fishburn a b (negmax (Nd ts)) (abrs ts a b)"
apply (metis abr_abr0(1) negmax_maxmin fishburn_abr01(1))
by (metis abr.simps(2) abr_abr0(1) negmax_maxmin fishburn_abr01(1))

corollary knuth_abr_negmax: "a < b ⟹ knuth a b (negmax t) (abr t a b)"
by (meson order.trans fishburn_abr_negmax(1))

corollary abr_cor: "abr t ⊥ ⊤ = negmax t"
by (metis (mono_tags) bot.extremum_strict knuth_abr_negmax knuth_bot_top linorder_not_less)

text ‹Detailed ‹fishburn2› proof (85 lines):›

theorem fishburn2_abr:
  shows "a < b ⟹ fishburn a b (negmax t)   (abr t a b)"
    and "a < b ⟹ fishburn a b (negmax (Nd ts)) (abrs ts a b)"
unfolding fishburn2
proof(induction t a b and ts a b rule: abr_abrs.induct)
  case (4 t ts a b)
(*
thus ?case
apply(simp add: Let_def)
  by (smt (verit, ccfv_threshold) ereal_minus_less_minus ereal_uminus_less_reorder linorder_not_le max.absorb_iff2 max.order_iff nle_le order.strict_trans1)
*)
  let ?m = "abrs ts a b"
  let ?ab = "abrs (t # ts) a b"
  let ?nm1 = "negmax t"
  let ?nms = "negmax (Nd ts)"
  let ?nm1s = "negmax (Nd (t # ts))"
  let ?r = "abr t (- b) (- ?m)"

  have 1: "?nm1s ≤ ?ab" if asm: "?ab < b"
  proof -
    have "¬ b ≤ ?m" using asm by(auto simp add: Let_def)
    hence "?ab = max (- ?r) ?m" by(simp add: Let_def)
    hence "- b < ?r" using uminus_less_reorder asm by auto
    have ‹?nm1s = max (- ?nm1) ?nms› by simp
    also have "… ≤ max (- ?r) ?m"
    proof -
      have "- ?nm1 ≤ - ?r"
        using "4.IH"(2)[OF refl, THEN conjunct1] ‹- b < ?r› ‹¬ b ≤ ?m› by auto
      moreover have "?nms ≤ ?m"
        using "4.IH"(1)[OF ‹a < b›, THEN conjunct2] ‹¬ b ≤ ?m› leI by blast
      ultimately show ?thesis by (metis max.mono)
    qed
    also note ‹?ab = max (- ?r) ?m›[symmetric]
    finally show ?thesis .
  qed

  have 2: "?ab ≤ ?nm1s" if "a < ?ab"
  proof cases
    assume "b ≤ ?m"
    have "?ab = ?m" using ‹b ≤ ?m› by(simp)
    also have "… ≤ ?nms" using "4.IH"(1)[OF ‹a < b›, THEN conjunct1]
      by (metis order.strict_trans2[OF ‹a<b› ‹b ≤ ?m›])
    also have "… ≤ max (-?nm1) ?nms"
      using max.cobounded2 by blast
    also have "… = ?nm1s" by simp
    finally show ?thesis .
  next
    assume "¬ b ≤ ?m"
    hence IH2: "?r < - ?m ⟶ ?nm1 ≤ ?r"
        using "4.IH"(2)[OF refl,THEN conjunct2] minus_less_minus linorder_not_le by blast
    have "a < ?m ∨ ¬ a < ?m ∧ a < - ?r" using ‹a < ?ab› ‹¬ b ≤ ?m›
      by(auto simp: Let_def less_max_iff_disj)
    then show ?thesis
    proof
      assume "a < ?m"
      hence IH1: "?m ≤ ?nms"
        using "4.IH"(1)[OF ‹a<b›, THEN conjunct1] by blast
      have 1: "- ?r ≤ ?nm1s"
      proof cases
        assume "?r < - ?m"
        thus ?thesis using IH2 by (simp add: le_max_iff_disj)
      next
        assume "¬ ?r < - ?m"
        thus ?thesis using IH1
          apply simp
          by (smt (verit) le_max_iff_disj linorder_le_less_linear order.trans that uminus_le_reorder)
      qed
      have 2: "?m ≤ ?nm1s"
        using IH1 by(auto simp: le_max_iff_disj)
      show ?thesis
        using ‹¬ b ≤ ?m› 1 2 by(simp add: Let_def not_le_imp_less)
    next
      assume a: "¬ a < ?m ∧ a < - ?r"
      have 1 : "- ?r ≤ - ?nm1"
        using ‹¬ a < ?m ∧ a < - ?r› IH2 less_uminus_reorder
        by (metis abrs_ge_a linorder_not_le minus_le_minus nle_le)
      have 2: "?m ≤ - ?nm1"
        using a "4.IH"(1)[OF ‹a<b›, THEN conjunct1] 1
        by (meson dual_order.strict_iff_not order.trans nle_le)
      have "?ab = max (- ?r) ?m"
        using a ‹¬ b ≤ ?m› by(simp add: Let_def)
      also have "… ≤ max (- ?nm1) ?nms"
        using 1 2 by (simp add: max.coboundedI1)
      also have "… = ?nm1s"
        by simp
      finally show ?thesis .
    qed
  qed
  show ?case using 1 2 by blast
qed auto

text ‹Detailed ‹fishburn› proof (100 lines):›

theorem fishburn_abr:
  shows "a < b ⟹ fishburn a b (negmax t)   (abr t a b)"
    and "a < b ⟹ fishburn a b (negmax (Nd ts)) (abrs ts a b)"
proof(induction t a b and ts a b rule: abr_abrs.induct)
  case (4 t ts a b)
  let ?m = "abrs ts a b"
  let ?ab = "abrs (t # ts) a b"
  let ?r = "abr t (- b) (- ?m)"
  let ?nm1 = "negmax t"
  let ?nms = "negmax (Nd ts)"
  let ?nm1s = "negmax (Nd (t # ts))"
  have "?nm1s = max (- ?nm1) ?nms" by simp

  have 1: "?nm1s ≤ ?ab" if asm: "?ab ≤ a"
  proof -
    have "¬ b ≤ ?m" by (rule ccontr) (use ‹?ab ≤ a› ‹a < b› in simp) (* more detail *)
    hence *: "?ab = max (- ?r) ?m" by(simp add: Let_def)
    hence "?m ≤ a" "- ?r ≤ a" using asm by auto
    have "- b < ?r" using ‹- ?r ≤ a› ‹a < b› uminus_less_reorder order_le_less_trans by blast
    note ‹?nm1s = _›
    also have "max (- ?nm1) ?nms ≤ max (- ?r) ?m"
    proof -
      have "- ?nm1 ≤ - ?r"
      proof cases (* uses totality of the ordering here (and in other places) *)
        assume "- ?m ≤ ?r"
        thus ?thesis using "4.IH"(2)[THEN conjunct2, THEN conjunct2] ‹¬ b ≤ ?m› by auto
      next
        assume "¬ - ?m ≤ ?r"
        thus ?thesis using  "4.IH"(2)[THEN conjunct2, THEN conjunct1] ‹¬ b ≤ ?m› ‹- b < ?r› by (simp)
      qed
      moreover have "?nms ≤ ?m"
        using ‹?m ≤ a› "4.IH"(1)[OF "4.prems", THEN conjunct1] by (auto)
      ultimately show ?thesis by (metis max.mono)
    qed
    also note *[symmetric]
    finally show ?thesis .
  qed

  have 2: "?ab ≤ ?nm1s" if "b ≤ ?ab"
  proof cases
    assume "?m ≥ b"
    show ?thesis using ‹?m ≥ b›
      using "4.IH"(1)[OF ‹a < b›,THEN conjunct2,THEN conjunct2] max.coboundedI2 by auto
  next
    assume "¬ ?m ≥ b"
    hence "?ab = max (-?r) ?m" by(simp add: Let_def)
    hence "-?r ≥ b" using ‹b ≤ ?ab› ‹¬ ?m ≥ b› by (metis le_max_iff_disj)
    hence "?ab = -?r"
      using ‹?ab = _› ‹¬ b ≤ ?m› by(metis not_le_imp_less less_le_trans max.absorb3)
    also have "… ≤ - ?nm1" using  "4.IH"(2)[OF refl,THEN conjunct1] ‹¬ b ≤ ?m› ‹b ≤ -?r›
      by (metis minus_le_minus uminus_le_reorder linorder_not_le)
    also have "… ≤ max (- ?nm1) ?nms" by auto
    also note  ‹?nm1s = …›[symmetric]
    finally show ?thesis .
  qed

  have 3: "?ab = ?nm1s" if asm: "a < ?ab" "?ab < b"
  proof -
    have "¬ b ≤ ?m" by (rule ccontr) (use ‹?ab < b› in simp) (* more detail *)
    hence *: "?ab = max (- ?r) ?m" by(simp add: Let_def)
    hence "- ?r < b" using ‹?ab < b› by auto
    note *
    also have "max (- ?r) ?m = ?nm1s"
    proof -
      have "?r = ?nm1 ∧ ?nms ≤ - ?r" if ‹¬ - ?r ≤ ?m›
      proof
        have " - b < ?r ∧ ?r < - ?m"
          using ‹- ?r < b› ‹¬ - ?r ≤ ?m›
          by (metis minus_less_minus neg_neg linorder_not_le)
        thus "?r = ?nm1"
          using "4.IH"(2)[OF refl, THEN conjunct2,THEN conjunct1] ‹¬ b ≤ ?m›
          using order.strict_trans by blast
        show "?nms ≤ - ?r"
        proof cases
          assume "?m ≤ a"
          thus ?thesis using "4.IH"(1)[OF ‹a<b›,THEN conjunct1] ‹¬ - ?r ≤ ?m› by simp
        next
          assume "¬ ?m ≤ a"
          thus ?thesis
            using "4.IH"(1)[OF ‹a<b›,THEN conjunct2, THEN conjunct1] ‹¬ - ?r ≤ ?m› ‹¬ b ≤ ?m› by auto
        qed
      qed
      moreover have "?m = ?nms ∧ - ?nm1 ≤ ?m" if "- ?r ≤ ?m"
      proof
        note ‹a < ?ab›
        also note *
        also have "max (- ?r) ?m = ?m" using ‹- ?r ≤ ?m› using max.absorb2 by blast
        finally have "a < ?m" .
        thus "?m = ?nms"
          using "4.IH"(1)[OF ‹a < b›,THEN conjunct2,THEN conjunct1] ‹¬ b ≤ ?m› not_le by blast
        have "- ?nm1 ≤ - ?r"
          using  "4.IH"(2)[OF refl,THEN conjunct2,THEN conjunct2]  ‹¬ b ≤ ?m›  ‹- ?r ≤ ?m›
          by (metis neg_neg not_le minus_le_minus)
        also note ‹- ?r ≤ ?m›
        finally show "- ?nm1 ≤ ?m" .
      qed
      ultimately show ?thesis using ‹?nm1s = _› by fastforce
    qed
    finally show ?thesis .
  qed
  show ?case using 1 2 3 by blast
qed auto


subsubsection ‹Explicit equational @{const knuth} proofs via min/max›

text ‹Not mm, only min and max. Only min in abrs. ‹a<b› required: a=1, b=-1, t=[]›

theorem shows abr_negmax3: "max a (min (abr t a b) b) = max a (min (negmax t) b)"
    and "a < b ⟹ min (abrs ts a b) b = max a (min (negmax (Nd ts)) b)"
proof(induction t a b and ts a b rule: abr_abrs.induct)
  case (2 ts a b)
  then show ?case apply simp
    by (metis max_def min.strict_boundedE order_neq_le_trans)
next
  case (4 t ts a b)
  let ?abts = "abrs ts a b" let ?abt = "abr t (- b) (- ?abts)"
  show ?case
  proof (cases "b ≤ ?abts")
    case True
    thus ?thesis using "4.IH"(1)[OF "4.prems"] apply (simp add: Let_def)
      by (metis (no_types) max.left_commute max_min_same(2) min.commute min_max_distrib2)
  next
    case False
(* automatic:
    show ?thesis apply (simp add: Let_def) using 4
      by (smt (verit) Orderings.order_eq_iff antisym_conv3 ereal_uminus_eq_reorder max.absorb1 max.commute max.left_commute de_morgan_min min.absorb3 min.commute min.orderI)
*)
    have IH2: "min b (max (-?abt) ?abts) = min b (max (- negmax t) ?abts)"
      using "4.IH"(2) False by (metis (no_types) neg_neg de_morgan_max)
    have "min (abrs (t # ts) a b) b = min (max (- ?abt) ?abts) b"
      using False by (simp add: Let_def)
    also have "… = min b (max (- ?abt) ?abts)"
      by (metis min.commute)
    also have "… = min b (max (- negmax t) ?abts)"
      using IH2 by blast
    also have "… = max (min (- negmax t) b) (min ?abts b)"
      by (metis min.commute min_max_distrib2)
    also have "… = max (min (- negmax t) b) (max a (min (negmax (Nd ts)) b))"
      using "4.IH"(1)[OF "4.prems"] by presburger
    also have "… = max a (min (max (- negmax t) (negmax (Nd ts))) b)"
      by (metis max.left_commute min_max_distrib1)
    finally show ?thesis by simp
  qed
qed auto

text ‹Not mm, only min and max. Also max in abrs:›

theorem shows abr_negmax2: "max a (min (abr t a b) b) = max a (min (negmax t) b)"
    and "a < b ⟹ max a (min (abrs ts a b) b) = max a (min (negmax (Nd ts)) b)"
proof(induction t a b and ts a b rule: abr_abrs.induct)
  case 2
  thus ?case apply simp
    by (metis max.orderE min.strict_boundedE not_le_imp_less)
  case (4 t ts a b)
  let ?abts = "abrs ts a b" let ?abt = "abr t (- b) (- ?abts)"
  show ?case
  proof (cases "b ≤ ?abts")
    case True
    thus ?thesis using "4.IH"(1)[OF "4.prems"] apply (simp add: Let_def)
      by (metis (no_types) max.left_commute max_min_same(2) min.commute min_max_distrib2)
  next
    case False
(* automatic:
    show ?thesis apply (simp add: Let_def) using 4
      by (smt (z3) False ereal_uminus_eq_reorder ereal_uminus_less_reorder max.left_commute de_morgan_min min.absorb_iff2 min.commute min.strict_order_iff min_max_distrib1 de_morgan_max nle_le)
*)
    hence "max a (min (abrs (t # ts) a b) b) = max a (min (max (- ?abt) ?abts) b)"
      by (simp add: Let_def linorder_not_le)
    also have "… = max a (-(max (min ?abt (- ?abts)) (-b)))"
      by (metis neg_neg de_morgan_max)
    also have "… = max a (-(max (-b) (min ?abt (- ?abts))))"
      by (metis max.commute)
    also have "… = max a (-(max (- b) (min (negmax t) (- ?abts))))"
      using "4.IH"(2)[OF refl] False by (simp add: linorder_not_le)
    also have "… = max a ((min b (max (- negmax t) ?abts)))"
      by (metis neg_neg de_morgan_min)
    also have "… = max (min (- negmax t) b) (max a (min ?abts b))"
      by (metis max.left_commute min.commute min_max_distrib2)
    also have "… = max (min (- negmax t) b) (max a (min (negmax (Nd ts)) b))"
      using "4.IH"(1)[OF "4.prems"] by presburger
    also have "… = max a (min (max (- negmax t) (negmax (Nd ts))) b)"
      by (metis max.left_commute min_max_distrib1)
    finally show ?thesis by simp
  qed
qed auto


subsubsection "Relating iteration from right and left"

text ‹Enables porting ‹abr› lemmas to ‹ab_negmax› lemmas, eg correctness.›

fun mirror :: "'a tree ⇒ 'a tree" where
"mirror (Lf x) = Lf x" |
"mirror (Nd ts) = Nd (rev (map mirror ts))"

lemma abrs_append:
  "abrs (ts1 @ ts2) a b = (let m = abrs ts2 a b in if m ≥ b then m else abrs ts1 m b)"
by(induction ts1 arbitrary: ts2) (auto simp add: Let_def)

lemma ab_negmax_abr_mirror:
shows "a<b ⟹ ab_negmax a b t = abr (mirror t) a b"
  and "a<b ⟹ ab_negmaxs a b ts = abrs (rev (map mirror ts)) a b"
proof(induction a b t and a b ts rule: ab_negmax_ab_negmaxs.induct)
  case 4
  then show ?case by (fastforce simp: Let_def abrs_append max.commute)
qed auto

lemma negmax_mirror:
fixes t :: "'a::de_morgan_order tree" and ts :: "'a::de_morgan_order tree list"
shows "negmax (mirror t) = negmax t ∧ negmax (Nd (rev (map mirror ts))) = negmax (Nd ts)"
by(rule compat_tree_tree_list.induct)(auto simp: max.commute maxs_rev maxs_append)

text ‹Correctness of ‹ab_negmax› from correctness of ‹abr›:›

theorem fishburn_ab_negmax_negmax_mirror:
shows "a < b ⟹ fishburn a b (negmax t)   (ab_negmax a b t)"
  and "a < b ⟹ fishburn a b (negmax (Nd ts)) (ab_negmaxs a b ts)"
apply (metis (no_types) ab_negmax_abr_mirror(1) negmax_mirror fishburn_abr_negmax(1))
by (metis (no_types) ab_negmax_abr_mirror(2) negmax_mirror fishburn_abr_negmax(2))


subsection ‹From the Right, Fail-Soft ›

text ‹Starting at ‹⊥› (after Fishburn)›

fun abr' :: "('a::de_morgan_order)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abrs' where
"abr' (Lf x) a b = x" |
"abr' (Nd ts) a b = abrs' ts a b" |

"abrs' [] a b = ⊥" |
"abrs' (t#ts) a b = (let m = abrs' ts a b in
  if m ≥ b then m else max (- abr' t (-b) (- max m a)) m)"


lemma abr01'_negate:
shows "abr0' (negate f t) a b = - abr1' (negate (¬f) t) (-a) (-b)"
and  "abrs0' (map (negate f) ts) a b = - abrs1' (map (negate (¬f)) ts) (-a) (-b)"
and "abr1' (negate f t) a b = - abr0' (negate (¬f) t) (-a) (-b)"
and  "abrs1' (map (negate f) ts) a b = - abrs0' (map (negate (¬f)) ts) (-a) (-b)"
proof(induction "negate f t" a b and "map (negate f) ts" a b and "negate f t" a b and "map (negate f) ts" a b arbitrary: f t and f ts and f t and f ts rule: abr0'_abrs0'_abr1'_abrs1'.induct)
  case (1 x a b)
  from Lf_eq_negateD[OF this] show ?case by simp
next
  case (2 ts a b)
  from Nd_eq_negateD[OF 2(2)] 2(1) show ?case by auto
next
  case (3 a b)
  then show ?case by simp
next
  case (4 t ts a b)
  from Cons_eq_map_D[OF 4(3)] 4(1) 4(2)[OF refl] show ?case
    apply (clarsimp simp add: Let_def de_morgan_max de_morgan_min)
    by (metis neg_neg uminus_le_reorder)
next
  case (5 x a b)
  from Lf_eq_negateD[OF this] show ?case by simp
next
  case (6 ts a b)
  from Nd_eq_negateD[OF 6(2)] 6(1) show ?case by auto
next
  case (7 a b)
  then show ?case by simp
next
  case (8 t ts a b)
  from Cons_eq_map_D[OF 8(3)] 8(1) 8(2)[OF refl] show ?case
    by (auto simp: Let_def de_morgan_max de_morgan_min uminus_le_reorder)
qed

lemma abr_abr0':
 shows "abr' t a b = abr0' (negate False t) a b"
 and "abrs' ts a b = abrs0' (map (negate True) ts) a b"
proof (induction t a b and ts a b rule: abr'_abrs'.induct)
  case (1 x a b)
  then show ?case by simp
next
  case (2 ts a b)
  then show ?case by simp
next
  case (3 a b)
  then show ?case by simp
next
  case (4 t ts a b)
  then show ?case
    by (simp add: Let_def abr01'_negate(3))
qed

corollary fishburn_abr'_negmax_cor:
  shows "a < b ⟹ fishburn a b (negmax t)   (abr' t a b)"
    and "a < b ⟹ fishburn a b (negmax (Nd ts)) (abrs' ts a b)"
apply (metis abr_abr0'(1) negmax_maxmin fishburn_abr01'(1))
by (metis abr'.simps(2) abr_abr0'(1) negmax_maxmin fishburn_abr01'(1))

lemma abr'_exact: "⟦ v = negmax t; a ≤ v ∧ v ≤ b⟧ ⟹ abr' t a b = v"
by (simp add: abr0'_exact abr_abr0'(1) negmax_maxmin)


text ‹Now a lot of copy-paste-modify from ‹bounded_linorder›.›

theorem (*fishburn_abr_abr': The point: can prove the r version below very simply;
 l version trickier: see ‹fishburn_abl_abl'› *) 
  shows "a < b ⟹ fishburn a b (abr' t a b) (abr t a b)"
    and "a < b ⟹ fishburn a b (abrs' ts a b) (abrs ts a b)"
proof(induction t a b  and ts a b rule: abr_abrs.induct)
  case (4 t ts a b)
  then show ?case apply (simp add: Let_def)
    by (smt (verit) order_eq_iff abrs_ge_a le_max_iff_disj less_uminus_reorder max_def minus_less_minus nless_le)
qed auto

theorem fishburn2_abr_abr':
  shows "a < b ⟹ fishburn a b (abr' t a b) (abr t a b)"
    and "a < b ⟹ fishburn a b (abrs' ts a b) (abrs ts a b)"
unfolding fishburn2
proof(induction t a b  and ts a b rule: abr_abrs.induct)
  case (4 t ts a b)
(* automatic:
  thus ?case apply (simp add: Let_def)
    by (smt (verit, ccfv_SIG) abrs_ge_a ereal_minus_less_minus ereal_uminus_less_reorder less_eq_ereal_def linorder_linear max.absorb_iff2 max.cobounded2 max.coboundedI1 max.strict_order_iff)
*)
  let ?m = "abrs ts a b"
  let ?ab = "abrs (t # ts) a b"
  let ?r = "abr t (- b) (- ?m)"
  let ?m' = "abrs' ts a b"
  let ?ab' = "abrs' (t # ts) a b"
  let ?r' = "abr' t (- b) (- max ?m' a)"
  note IH1 = "4.IH"(1)[OF ‹a < b›] note IH11 = IH1[THEN conjunct1] note IH12 = IH1[THEN conjunct2]

  have 1: "?ab ≤ ?ab'" if "a < ?ab"
  proof cases
    assume "b ≤ ?m"
    thus ?thesis using IH11 ‹a<b› by (auto simp: Let_def)
  next
    assume "¬ b ≤ ?m"
    hence "?ab = max (- ?r) ?m" by (simp add: Let_def)
    hence "a < max (- ?r) ?m" using ‹a < ?ab› by presburger
    have IH22: "?r < - ?m ⟶ abr' t (- b) (- ?m) ≤ ?r"
      using ‹¬ b ≤ ?m› "4.IH"(2) by auto
    have "¬ b ≤ ?m'" using IH12 ‹¬ b ≤ ?m› by auto
    hence "?ab' = max (- ?r') ?m'" by (simp add: Let_def)
    have "?m' ≤ ?m" using IH12 ‹¬ b ≤ ?m› linorder_not_le by blast
    have "max ?m' a = ?m"
    proof cases
      assume "?m ≤ a"
      thus ?thesis using ‹?m' ≤ ?m› abrs_ge_a
        by (metis max.absorb1 max.commute)
    next
      assume "¬ ?m ≤ a"
      thus ?thesis using IH11 ‹?m' ≤ ?m› by auto
    qed
    have "- ?r ≤ max (- ?r') ?m'"
    proof cases
      assume "?r < - ?m"
      thus ?thesis using IH22 ‹max ?m' a = ?m›
        by (simp add: max.coboundedI1) (* more detail *)
    next
      assume "¬ ?r < - ?m"
      hence "?m = ?m'" using ‹a < max (-?r) ?m› ‹max ?m' a = ?m›
        by (metis linorder_not_le max.commute max.order_iff nle_le uminus_le_reorder)
      thus ‹- ?r ≤ max (- ?r') ?m'› using ‹¬ ?r < - ?m›
        by (simp add: max.coboundedI2 uminus_le_reorder)
    qed
    moreover have "?m ≤ max (- ?r') (?m')"
    proof cases
      assume "a < ?m"
      hence "?m ≤ ?m'" using IH11 by simp
      then show ?thesis using le_max_iff_disj by blast
    next
      assume "¬ a < ?m"
      hence "?m ≤ a" by simp
      also have "a < - ?r" using ‹a < max (-?r) ?m› ‹¬ a < ?m› less_max_iff_disj by blast
      also note ‹- ?r ≤ max (- ?r') ?m'›
      finally show ?thesis using order.order_iff_strict by blast 
    qed
    ultimately show ?thesis using ‹?ab = _› ‹?ab' = _› by (metis max.bounded_iff)
  qed

  have 2: "?ab' ≤ ?ab" if "?ab < b"
  proof cases
    assume "b ≤ ?m"
    thus ?thesis
      using ‹?ab < b› by (simp add: Let_def)
  next
    assume "¬ b ≤ ?m"
    hence "- ?r < b" using ‹?ab < b› by(auto simp: Let_def)
    with "4.IH"(2) ‹¬ b ≤ ?m›
    have IH21: "?r ≤ abr' t (- b) (- ?m)"
      by (metis linorder_le_less_linear minus_less_minus uminus_less_reorder)
    have "¬ b ≤ ?m'" "?m' ≤ ?m" using IH12 ‹¬ b ≤ ?m› by auto
    have "?ab = max (- ?r) ?m" using ‹¬ b ≤ ?m› by (simp add: Let_def)
    hence "?ab' = max (- ?r') ?m'" using ‹¬ b ≤ ?m'› by (simp add: Let_def)
    have "- ?r' ≤ - ?r"
    proof cases
      assume "a < ?m"
      hence "?m' = ?m" using IH11 ‹?m' ≤ ?m› nle_le by blast
      hence "- ?r' = - abr' t (- b) (- ?m)" using ‹a < ?m› by simp
      also have "… ≤ - ?r" using IH21 minus_le_minus by blast
      finally show ?thesis .
    next
      assume "¬ a < ?m"
      have "?m = a" using ‹¬ a < abrs ts a b› abrs_ge_a by (metis order_le_imp_less_or_eq)
      hence "max ?m' a = a" using ‹?m' ≤ ?m› by simp
      with ‹?m = a› show ?thesis using IH21 by simp
    qed
    then have "- ?r' ≤ max (- ?r) ?m" using max.coboundedI1 by blast
    hence "max (- ?r') ?m' ≤ max (- ?r) ?m"
      using ‹?m' ≤ ?m› by (metis max.absorb2 max.bounded_iff max.cobounded2)
    thus ?thesis using ‹?ab = _› ‹?ab' = _› by metis
  qed

  show ?case using "1" "2" by blast

qed(auto simp add: bot_ereal_def)

theorem fishburn_abr'_negmax:
  shows "a < b ⟹ fishburn a b (negmax t)   (abr' t a b)"
    and "a < b ⟹ fishburn a b (negmax (Nd ts)) (abrs' ts a b)"
unfolding fishburn2
proof(induction t a b and ts a b rule: abr'_abrs'.induct)
  case (4 t ts a b)
(*
thus ?case
apply(simp add: Let_def)
  by (smt (verit, ccfv_threshold) ereal_minus_less_minus ereal_uminus_less_reorder linorder_not_le max.absorb_iff2 max.order_iff nle_le order.strict_trans1)
*)
  let ?m = "abrs' ts a b"
  let ?ab = "abrs' (t # ts) a b"
  let ?nm1 = "negmax t"
  let ?nms = "negmax (Nd ts)"
  let ?nm1s = "negmax (Nd (t # ts))"
  let ?r = "abr' t (- b) (- max ?m a)"

  have 1: "?nm1s ≤ ?ab" if asm: "?ab < b"
  proof -
    have "¬ b ≤ ?m" using asm by(auto simp add: Let_def)
    hence "?ab = max (- ?r) ?m" by(simp add: Let_def)
    hence "- b < ?r" using uminus_less_reorder asm by auto
    have ‹?nm1s = max (- ?nm1) ?nms› by simp
    also have "… ≤ max (- ?r) ?m"
    proof -
      have "- ?nm1 ≤ - ?r"
        using "4.IH"(2)[OF refl, THEN conjunct1] ‹a<b› ‹- b < ?r› ‹¬ b ≤ ?m› by auto
      moreover have "?nms ≤ ?m"
        using "4.IH"(1)[OF ‹a < b›, THEN conjunct2] ‹¬ b ≤ ?m› leI by blast
      ultimately show ?thesis by (metis max.mono)
    qed
    also note ‹?ab = max (- ?r) ?m›[symmetric]
    finally show ?thesis .
  qed

  have 2: "?ab ≤ ?nm1s" if "a < ?ab"
  proof cases
    assume "b ≤ ?m"
    have "?ab = ?m" using ‹b ≤ ?m› by(simp)
    also have "… ≤ ?nms" using "4.IH"(1)[OF ‹a < b›, THEN conjunct1]
      by (metis order.strict_trans2[OF ‹a<b› ‹b ≤ ?m›])
    also have "… ≤ max (-?nm1) ?nms"
      using max.cobounded2 by blast
    also have "… = ?nm1s" by simp
    finally show ?thesis .
  next
    assume "¬ b ≤ ?m"
    hence IH2: "?r < - ?m ⟶ ?nm1 ≤ ?r" (* more detail, esp why ‹a < ?ab›? *)
      using "4.IH"(2)[OF refl, THEN conjunct2] ‹a<b› ‹a < ?ab› by (auto simp: less_uminus_reorder)
    have "a < ?m ∨ ¬ a < ?m ∧ a < - ?r" using ‹a < ?ab› ‹¬ b ≤ ?m›
      by(auto simp: Let_def less_max_iff_disj)
    then show ?thesis
    proof
      assume "a < ?m"
      hence IH1: "?m ≤ ?nms"
        using "4.IH"(1)[OF ‹a<b›, THEN conjunct1] by blast
      have 1: "- ?r ≤ ?nm1s"
      proof cases
        assume "?r < - ?m"
        thus ?thesis using IH2 by (simp add: le_max_iff_disj)
      next
        assume "¬ ?r < - ?m"
        thus ?thesis using IH1
          by (simp add: less_uminus_reorder max.coboundedI2)
      qed
      have 2: "?m ≤ ?nm1s"
        using IH1 by(auto simp: le_max_iff_disj)
      show ?thesis
        using ‹¬ b ≤ ?m› 1 2 by(simp add: Let_def not_le_imp_less)
    next
      assume a: "¬ a < ?m ∧ a < - ?r"
      have 1 : "- ?r ≤ - ?nm1"
        using ‹¬ a < ?m ∧ a < - ?r› IH2 by (auto simp: less_uminus_reorder)
      have 2: "?m ≤ - ?nm1"
        using a "4.IH"(1)[OF ‹a<b›, THEN conjunct1] 1
        by (meson dual_order.strict_iff_not order.trans nle_le)
      have "?ab = max (- ?r) ?m"
        using a ‹¬ b ≤ ?m› by(simp add: Let_def)
      also have "… ≤ max (- ?nm1) ?nms"
        using 1 2 by (simp add: max.coboundedI1)
      also have "… = ?nm1s"
        by simp
      finally show ?thesis .
    qed
  qed
  show ?case using 1 2 by blast
qed (auto simp add: bot_ereal_def)

text ‹Automatic proof:›

theorem
  shows "a < b ⟹ fishburn a b (negmax t)   (abr' t a b)"
    and "a < b ⟹ fishburn a b (negmax (Nd ts)) (abrs' ts a b)"
unfolding fishburn2
proof(induction t a b and ts a b rule: abr'_abrs'.induct)
  case (4 t ts a b)
  then show ?case
    apply (simp add: Let_def)
    by (smt (verit, best) abrs_ge_a less_uminus_reorder uminus_less_reorder linorder_not_le max.absorb1 max.absorb_iff2 nle_le order.trans)
qed (auto simp add: bot_ereal_def)


subsubsection ‹Also returning the searched tree›

text ‹Hard:›

fun abtr :: "('a::de_morgan_order) tree ⇒ 'a ⇒ 'a ⇒ 'a * 'a tree" and abtrs where
"abtr (Lf x) a b = (x, Lf x)" |
"abtr (Nd ts) a b = (let (m,us) = abtrs ts a b in (m, Nd us))" |

"abtrs [] a b = (a,[])" |
"abtrs (t#ts) a b = (let (m,us) = abtrs ts a b in
  if m ≥ b then (m,us) else let (n,u) = abtr t (-b) (-m) in (max (-n) m,u#us))"

text ‹Soft:›

fun abtr' :: "('a::de_morgan_order) tree ⇒ 'a ⇒ 'a ⇒ 'a * 'a tree" and abtrs' where
"abtr' (Lf x) a b = (x, Lf x)" |
"abtr' (Nd ts) a b = (let (m,us) = abtrs' ts a b in (m, Nd us))" |

"abtrs' [] a b = (⊥,[])" |
"abtrs' (t#ts) a b = (let (m,us) = abtrs' ts a b in
  if m ≥ b then (m,us) else let (n,u) = abtr' t (-b) (- max m a) in (max (-n) m,u#us))"

lemma fst_abtr:
shows "fst(abtr t a b) = abr t a b"
and "fst(abtrs ts a b) = abrs ts a b"
by(induction t a b and ts a b rule: abtr_abtrs.induct)
  (auto simp: Let_def split: prod.split)

lemma fst_abtr':
shows "fst(abtr' t a b) = abr' t a b"
and "fst(abtrs' ts a b) = abrs' ts a b"
by(induction t a b and ts a b rule: abtr'_abtrs'.induct)
  (auto simp: Let_def split: prod.split)

lemma snd_abtr'_abtr:
shows "a < b ⟹ snd(abtr' t a b) = snd(abtr t a b)"
and "a < b ⟹ snd(abtrs' ts a b) = snd(abtrs ts a b)"
proof(induction t a b and ts a b rule: abtr'_abtrs'.induct)
  case (4 t ts a b)
  then show ?case
    apply(simp add: Let_def split: prod.split)
    using fst_abtr(2) fst_abtr'(2) fishburn2_abr_abr'(2) abrs_ge_a
    by (smt (verit, best) fst_conv le_max_iff_disj linorder_not_le max.absorb1 nle_le sndI)
qed (auto simp add: split_beta)


subsubsection ‹Fail-Soft Generalized›

fun abir' :: "_ ⇒ ('a::de_morgan_order)tree ⇒ 'a ⇒ 'a ⇒ 'a" and abirs' where
"abir' i0 (Lf x) a b = x" |
"abir' i0 (Nd ts) a b = abirs' i0 (i0 (map (negate True) ts) a) ts a b" |

"abirs' i0 i [] a b = i" |
"abirs' i0 i (t#ts) a b =
  (let m = abirs' i0 i ts a b
   in if m ≥ b then m else max (- abir' i0 t (- b) (- max m a)) m)"

abbreviation "neg_all ≡ negate True o negate False"

lemma neg_all_negate: "neg_all (negate f t) = negate (¬f) t"
proof(induction t arbitrary: f)
  case (Nd ts)
  { fix t
    assume "t ∈ set ts"
    from Nd[OF this, of True] have "neg_all t = negate False (negate True t)"
      by (metis comp_apply negate_negate)
  }
  with Nd[of _ False] show ?case
    by (cases f) (auto simp: negate_negate)
qed simp

lemma neg_all_negate': "neg_all o negate f = negate (¬f)"
  using neg_all_negate by fastforce

lemma abir01'_negate:
shows "∀ts a. i1 ts a = - i0 (map neg_all ts) (-a) ⟹
  abir0' i0 i1 (negate f t) a b = - abir1' i0 i1 (negate (¬f) t) (-a) (-b)"
and  "∀ts a. i1 ts a = - i0 (map neg_all ts) (-a) ⟹
  abirs0' i0 i1 i (map (negate f) ts) a b = - abirs1' i0 i1 (-i) (map (negate (¬f)) ts) (-a) (-b)"
and "∀ts a. i1 ts a = - i0 (map neg_all ts) (-a) ⟹
  abir1' i0 i1 (negate f t) a b = - abir0' i0 i1 (negate (¬f) t) (-a) (-b)"
and  "∀ts a. i1 ts a = - i0 (map neg_all ts) (-a) ⟹
  abirs1' i0 i1 i (map (negate f) ts) a b = - abirs0' i0 i1 (-i) (map (negate (¬f)) ts) (-a) (-b)"
proof(induction i0 i1 "negate f t" a b and i0 i1 i "map (negate f) ts" a b and i0 i1 "negate f t" a b and i0 i1 i "map (negate f) ts" a b arbitrary: f t and f ts and f t and f ts rule: abir0'_abirs0'_abir1'_abirs1'.induct)
  case (1 x a b)
  from Lf_eq_negateD this show ?case by fastforce
next
  case (2 i0 i1 ts a b)
  from Nd_eq_negateD[OF 2(2)] 2(1,3) show ?case by (auto simp: neg_all_negate')
next
  case (3 a b)
  then show ?case by simp
next
  case (4 i0 i1 i t ts a b)
  from Cons_eq_map_D[OF 4(3)] 4(1,4) 4(2)[OF refl] show ?case
    apply (clarsimp simp: Let_def de_morgan_min de_morgan_max)
    by (metis neg_neg uminus_le_reorder)
next
  case (5 i0 i1 x a b)
  from Lf_eq_negateD this show ?case by fastforce
next
  case (6 i0 i1 ts a b)
  from Nd_eq_negateD[OF 6(2)] obtain us where "t = Nd us" "ts = map (negate (¬ f)) us" by blast
  with 6(1)[of "Not f" us] 6(3) show ?case by (auto simp: neg_all_negate')
next
  case (7 i0 i1 i a b)
  then show ?case by simp
next
  case (8 i0 i1 i t ts a b)
  from Cons_eq_map_D[OF 8(3)] 8(1,4) 8(2)[OF refl] show ?case
    by (auto simp: Let_def de_morgan_max de_morgan_min uminus_le_reorder)
qed
(* Alternative:
lemma abir01'_negate:
shows "∀f ts a. i1 (map (negate f) ts) a = - i0 (map (negate (¬f)) ts) (-a) ⟹
  abir0' i0 i1 (negate f t) a b = - abir1' i0 i1 (negate (¬f) t) (-a) (-b)"
and  "∀f ts a. i1 (map (negate f) ts) a = - i0 (map (negate (¬f)) ts) (-a) ⟹
  abirs0' i0 i1 i (map (negate f) ts) a b = - abirs1' i0 i1 (-i) (map (negate (¬f)) ts) (-a) (-b)"
and "∀f ts a. i1 (map (negate f) ts) a = - i0 (map (negate (¬f)) ts) (-a) ⟹
  abir1' i0 i1 (negate f t) a b = - abir0' i0 i1 (negate (¬f) t) (-a) (-b)"
and  "∀f ts a. i1 (map (negate f) ts) a = - i0 (map (negate (¬f)) ts) (-a) ⟹
  abirs1' i0 i1 i (map (negate f) ts) a b = - abirs0' i0 i1 (-i) (map (negate (¬f)) ts) (-a) (-b)"
proof(induction i0 i1 "negate f t" a b and i0 i1 i "map (negate f) ts" a b and i0 i1 "negate f t" a b and i0 i1 i "map (negate f) ts" a b arbitrary: f t and f ts and f t and f ts rule: abir0'_abirs0'_abir1'_abirs1'.induct)
  case (1 x a b)
  from Lf_eq_negateD this show ?case by fastforce
next
  case (2 i0 i1 ts a b)
  from Nd_eq_negateD[OF 2(2)] 2(1,3) show ?case by auto
next
  case (3 a b)
  then show ?case by simp
next
  case (4 i0 i1 i t ts a b)
  from Cons_eq_map_D[OF 4(3)] 4(1,4) 4(2)[OF refl] show ?case
    apply (auto simp: Let_def de_morgan_min)
    apply (metis neg_neg uminus_le_reorder)
    apply (metis neg_neg uminus_le_reorder)
    by (simp add: de_morgan_max)
next
  case (5 i0 i1 x a b)
  from Lf_eq_negateD this show ?case by fastforce
next
  case (6 i0 i1 ts a b)
  from Nd_eq_negateD[OF 6(2)] 6(1,3) show ?case by fastforce
next
  case (7 i0 i1 i a b)
  then show ?case by simp
next
  case (8 i0 i1 i t ts a b)
  from Cons_eq_map_D[OF 8(3)] 8(1,4) 8(2)[OF refl] show ?case
    by (auto simp: Let_def de_morgan_max de_morgan_min uminus_le_reorder)
qed
*)

lemma abir'_abir0':
shows "abir' i0 t a b
  = abir0' i0 (λts a. - i0 (map neg_all ts) (-a)) (negate False t) a b"
and "abirs' i0 i ts a b
  = abirs0' i0 (λts a. - i0 (map neg_all ts) (-a)) i (map (negate True) ts) a b"
proof(induction i0 t a b and i0 i ts a b rule: abir'_abirs'.induct)
  case (1 i0 x a b)
  then show ?case by simp
next
  case (2 i0 ts a b)
  then show ?case by simp
next
  case (3 i0 i a b)
  then show ?case by simp
next
  case (4 i0 i t ts a b)
  then show ?case
    by (auto simp add: Let_def abir01'_negate(3) o_def)
qed


corollary fishburn_abir'_negmax_cor:
  shows "a < b ⟹ bnd i0 (λts a. - i0 (map neg_all ts) (-a)) ⟹ fishburn a b (negmax t)           (abir' i0 t a b)"
    and "a < b ⟹ bnd i0 (λts a. - i0 (map neg_all ts) (-a)) ⟹ fishburn a b (max i (negmax (Nd ts))) (abirs' i0 i ts a b)"
unfolding bnd_def
apply (metis (no_types, lifting) bnd_def abir'_abir0'(1) negmax_maxmin fishburn_abir01'(1))
by (smt (verit, ccfv_threshold) bnd_def abir'_abir0'(2) negate.simps(2) negmax_maxmin fishburn_abir01'(2))

end