Theory Alpha_Beta_Linear
chapter ‹Linear Orders›
theory Alpha_Beta_Linear
imports
"HOL-Library.Extended_Real"
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
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›