# Theory OrdinalArith

(*  Title:       Countable Ordinals

Author:      Brian Huffman, 2005
Maintainer:  Brian Huffman <brianh at cse.ogi.edu>
*)

section ‹Ordinal Arithmetic›

theory OrdinalArith
imports OrdinalRec
begin

instantiation ordinal :: plus
begin

definition
"(+) = (λx. ordinal_rec x (λp. oSuc))"

instance ..

end

lemma normal_plus: "normal ((+) x)"

lemma ordinal_plus_0 [simp]: "x + 0 = (x::ordinal)"

lemma ordinal_plus_oSuc [simp]: "x + oSuc y = oSuc (x + y)"

lemma ordinal_plus_oLimit [simp]: "x + oLimit f = oLimit (λn. x + f n)"

lemma ordinal_0_plus [simp]: "0 + x = (x::ordinal)"
by (rule_tac a=x in oLimit_induct, simp_all)

lemma ordinal_plus_assoc: "(x + y) + z = x + (y + z::ordinal)"
by (rule_tac a=z in oLimit_induct, simp_all)

lemma ordinal_plus_monoL [rule_format]:
"x x'. x  x'  x + y  x' + (y::ordinal)"
apply (rule_tac a=y in oLimit_induct, simp_all)
apply clarify
apply (rule oLimit_leI, clarify)
apply (rule_tac n=n in le_oLimitI)
apply simp
done

lemma ordinal_plus_monoR: "y  y'  x + y  x + (y'::ordinal)"
by (rule normal.monoD[OF normal_plus])

lemma ordinal_plus_mono:
"x  x'; y  y'  x + y  x' + (y'::ordinal)"
by (rule order_trans[OF ordinal_plus_monoL ordinal_plus_monoR])

lemma ordinal_plus_strict_monoR: "y < y'  x + y < x + (y'::ordinal)"
by (rule normal.strict_monoD[OF normal_plus])

lemma ordinal_le_plusL [simp]: "y  x + (y::ordinal)"
by (cut_tac ordinal_plus_monoL[OF ordinal_0_le], simp)

lemma ordinal_le_plusR [simp]: "x  x + (y::ordinal)"
by (cut_tac ordinal_plus_monoR[OF ordinal_0_le], simp)

lemma ordinal_less_plusR: "0 < y  x < x + (y::ordinal)"
by (drule_tac ordinal_plus_strict_monoR, simp)

lemma ordinal_plus_left_cancel [simp]:
"(w + x = w + y) = (x = (y::ordinal))"
by (rule normal.cancel_eq[OF normal_plus])

lemma ordinal_plus_left_cancel_le [simp]:
"(w + x  w + y) = (x  (y::ordinal))"
by (rule normal.cancel_le[OF normal_plus])

lemma ordinal_plus_left_cancel_less [simp]:
"(w + x < w + y) = (x < (y::ordinal))"
by (rule normal.cancel_less[OF normal_plus])

lemma ordinal_plus_not_0: "(0 < x + y) = (0 < x  0 < (y::ordinal))"
by (metis ordinal_le_0 ordinal_le_plusL ordinal_neq_0 ordinal_plus_0)

lemma not_inject: "(¬ P) = (¬ Q)  P = Q"
by auto

lemma ordinal_plus_eq_0:
"((x::ordinal) + y = 0) = (x = 0  y = 0)"
by (rule not_inject, simp add: ordinal_plus_not_0)

subsection ‹Subtraction›

instantiation ordinal :: minus
begin

definition
minus_ordinal_def:
"x - y = ordinal_rec 0 (λp w. if y  p then oSuc w else w) x"

instance ..

end

lemma continuous_minus: "continuous (λx. x - y)"
unfolding minus_ordinal_def

lemma ordinal_0_minus [simp]: "0 - x = (0::ordinal)"

lemma ordinal_oSuc_minus [simp]: "y  x  oSuc x - y = oSuc (x - y)"

lemma ordinal_oLimit_minus [simp]: "oLimit f - y = oLimit (λn. f n - y)"
by (rule continuousD[OF continuous_minus])

lemma ordinal_minus_0 [simp]: "x - 0 = (x::ordinal)"
by (rule_tac a=x in oLimit_induct, simp_all)

lemma ordinal_oSuc_minus2: "x < y  oSuc x - y = x - y"

lemma ordinal_minus_eq_0 [rule_format, simp]:
"x  y  x - y = (0::ordinal)"
apply (rule_tac a=x in oLimit_induct)
apply simp
apply (simp add: ordinal_oSuc_minus2 order_less_imp_le oSuc_le_eq_less)
done

lemma ordinal_plus_minus1 [simp]: "(x + y) - x = (y::ordinal)"
by (rule_tac a=y in oLimit_induct, simp_all)

lemma ordinal_plus_minus2 [simp]: "x  y  x + (y - x) = (y::ordinal)"
apply (subgoal_tac "z. y < x + z  x + (y - x) = y")
apply (drule_tac x="oSuc y" in spec, erule mp)
apply (rule order_less_le_trans[OF less_oSuc], simp)
apply (rule allI, rule_tac a=z in oLimit_induct)
apply (clarsimp, drule less_oLimitD, clarsimp)
done

lemma ordinal_minusI: "x = y + z  x - y = (z::ordinal)"
by simp

lemma ordinal_minus_less_eq [simp]:
"(y::ordinal)  x  (x - y < z) = (x < y + z)"
by (metis ordinal_plus_left_cancel_less ordinal_plus_minus2)

lemma ordinal_minus_le_eq [simp]: "(x - y  z) = (x  y + (z::ordinal))"
proof (rule linorder_le_cases)
assume "x  y" then show ?thesis
using order_trans by force
next
assume "y  x" then show ?thesis
by (metis ordinal_plus_left_cancel_le ordinal_plus_minus2)
qed

lemma ordinal_minus_monoL: "x  y  x - z  y - (z::ordinal)"
by (erule continuous.monoD[OF continuous_minus])

lemma ordinal_minus_monoR: "x  y  z - y  z - (x::ordinal)"
by (metis linorder_le_cases order_trans ordinal_minus_le_eq ordinal_plus_monoL)

subsection ‹Multiplication›

instantiation ordinal :: times
begin

definition
times_ordinal_def: "(*) = (λx. ordinal_rec 0 (λp w. w + x))"

instance ..

end

lemma continuous_times: "continuous ((*) x)"

lemma normal_times: "0 < x  normal ((*) x)"
unfolding times_ordinal_def

lemma ordinal_times_0 [simp]: "x * 0 = (0::ordinal)"

lemma ordinal_times_oSuc [simp]: "x * oSuc y = (x * y) + x"

lemma ordinal_times_oLimit [simp]: "x * oLimit f = oLimit (λn. x * f n)"

lemma ordinal_0_times [simp]: "0 * x = (0::ordinal)"
by (rule_tac a=x in oLimit_induct, simp_all)

lemma ordinal_1_times [simp]: "oSuc 0 * x = (x::ordinal)"
by (rule_tac a=x in oLimit_induct, simp_all)

lemma ordinal_times_1 [simp]: "x * oSuc 0 = (x::ordinal)"
by simp

lemma ordinal_times_distrib:
"x * (y + z) = (x * y) + (x * z::ordinal)"
by (rule_tac a=z in oLimit_induct, simp_all add: ordinal_plus_assoc)

lemma ordinal_times_assoc:
"(x * y::ordinal) * z = x * (y * z)"
by (rule_tac a=z in oLimit_induct, simp_all add: ordinal_times_distrib)

lemma ordinal_times_monoL [rule_format]:
"x x'. x  x'  x * y  x' * (y::ordinal)"
apply (rule_tac a=y in oLimit_induct)
apply simp
apply clarify
apply clarsimp
apply (rule oLimit_leI, clarify)
apply (rule_tac n=n in le_oLimitI)
apply simp
done

lemma ordinal_times_monoR: "y  y'  x * y  x * (y'::ordinal)"
by (rule continuous.monoD[OF continuous_times])

lemma ordinal_times_mono:
"x  x'; y  y'  x * y  x' * (y'::ordinal)"
by (rule order_trans[OF ordinal_times_monoL ordinal_times_monoR])

lemma ordinal_times_strict_monoR:
"y < y'; 0 < x  x * y < x * (y'::ordinal)"
by (rule normal.strict_monoD[OF normal_times])

lemma ordinal_le_timesL [simp]: "0 < x  y  x * (y::ordinal)"
by (drule ordinal_times_monoL[OF oSuc_leI], simp)

lemma ordinal_le_timesR [simp]: "0 < y  x  x * (y::ordinal)"
by (drule ordinal_times_monoR[OF oSuc_leI], simp)

lemma ordinal_less_timesR: "0 < x; oSuc 0 < y  x < x * (y::ordinal)"
by (drule ordinal_times_strict_monoR, assumption, simp)

lemma ordinal_times_left_cancel [simp]:
"0 < w  (w * x = w * y) = (x = (y::ordinal))"
by (rule normal.cancel_eq[OF normal_times])

lemma ordinal_times_left_cancel_le [simp]:
"0 < w  (w * x  w * y) = (x  (y::ordinal))"
by (rule normal.cancel_le[OF normal_times])

lemma ordinal_times_left_cancel_less [simp]:
"0 < w  (w * x < w * y) = (x < (y::ordinal))"
by (rule normal.cancel_less[OF normal_times])

lemma ordinal_times_eq_0:
"((x::ordinal) * y = 0) = (x = 0  y = 0)"
by (metis ordinal_0_times ordinal_neq_0 ordinal_times_0 ordinal_times_strict_monoR)

lemma ordinal_times_not_0 [simp]:
"((0::ordinal) < x * y) = (0 < x  0 < y)"
by (metis ordinal_neq_0 ordinal_times_eq_0)

subsection ‹Exponentiation›

definition
exp_ordinal :: "[ordinal, ordinal]  ordinal" (infixr "**" 75) where
"(**) = (λx. if 0 < x then ordinal_rec 1 (λp w. w * x)
else (λy. if y = 0 then 1 else 0))"

lemma continuous_exp: "0 < x  continuous ((**) x)"

lemma ordinal_exp_0 [simp]: "x ** 0 = (1::ordinal)"

lemma ordinal_exp_oSuc [simp]: "x ** oSuc y = (x ** y) * x"

lemma ordinal_exp_oLimit [simp]:
"0 < x  x ** oLimit f = oLimit (λn. x ** f n)"
by (rule continuousD[OF continuous_exp])

lemma ordinal_0_exp [simp]: "0 ** x = (if x = 0 then 1 else 0)"

lemma ordinal_1_exp [simp]:
by (rule_tac a=x in oLimit_induct, simp_all)

lemma ordinal_exp_1 [simp]: "x ** oSuc 0 = x"
by simp

lemma ordinal_exp_distrib:
"x ** (y + z) = (x ** y) * (x ** (z::ordinal))"
apply (case_tac "x = 0", simp_all add: ordinal_plus_not_0)
apply (rule_tac a=z in oLimit_induct, simp_all add: ordinal_times_assoc)
done

lemma ordinal_exp_not_0 [simp]: "(0 < x ** y) = (0 < x  y = 0)"
apply auto
apply (erule contrapos_pp, simp)
apply (rule_tac a=y in oLimit_induct, simp_all)
apply (rule less_oLimitI, erule spec)
done

lemma ordinal_exp_eq_0 [simp]: "(x ** y = 0) = (x = 0  0 < y)"
by (rule not_inject, simp)

lemma ordinal_exp_assoc:
"(x ** y) ** z = x ** (y * z)"
apply (case_tac "x = 0", simp_all)
apply (rule_tac a=z in oLimit_induct, simp_all add: ordinal_exp_distrib)
done

lemma ordinal_exp_monoL [rule_format]:
"x x'. x  x'  x ** y  x' ** (y::ordinal)"
apply (rule_tac a=y in oLimit_induct)
apply simp
apply clarsimp
apply (case_tac "x = 0", simp)
apply (case_tac "x' = 0", simp_all)
apply (rule oLimit_leI, clarify)
apply (rule_tac n=n in le_oLimitI)
apply simp
done

lemma normal_exp: "oSuc 0 < x  normal ((**) x)"
using order_less_trans[OF less_oSuc]

lemma ordinal_exp_monoR:
"0 < x; y  y'  x ** y  x ** (y'::ordinal)"
by (rule continuous.monoD[OF continuous_exp])

lemma ordinal_exp_mono:
"0 < x'; x  x'; y  y'  x ** y  x' ** (y'::ordinal)"
by (rule order_trans[OF ordinal_exp_monoL ordinal_exp_monoR])

lemma ordinal_exp_strict_monoR:
"oSuc 0 < x; y < y'  x ** y < x ** (y'::ordinal)"
by (rule normal.strict_monoD[OF normal_exp])

lemma ordinal_le_expR [simp]: "0 < y  x  x ** (y::ordinal)"
by (metis leI nless_le oSuc_le_eq_less ordinal_exp_1 ordinal_exp_mono ordinal_le_0)

lemma ordinal_exp_left_cancel [simp]:
"oSuc 0 < w  (w ** x = w ** y) = (x = y)"
by (rule normal.cancel_eq[OF normal_exp])

lemma ordinal_exp_left_cancel_le [simp]:
"oSuc 0 < w  (w ** x  w ** y) = (x  y)"
by (rule normal.cancel_le[OF normal_exp])

lemma ordinal_exp_left_cancel_less [simp]:
"oSuc 0 < w  (w ** x < w ** y) = (x < y)"
by (rule normal.cancel_less[OF normal_exp])

end