Theory Signed_Syntactic_Ordinal
section ‹Signed Syntactic Ordinals in Cantor Normal Form›
theory Signed_Syntactic_Ordinal
imports Signed_Hereditary_Multiset Syntactic_Ordinal
begin
subsection ‹Natural (Hessenberg) Product›
instantiation zhmultiset :: comm_ring_1
begin
abbreviation ω⇩z_exp :: "hmultiset ⇒ zhmultiset" ("ω⇩z^") where
"ω⇩z^ ≡ λm. ZHMSet {#m#}⇩z"
lift_definition one_zhmultiset :: zhmultiset is "{#0#}⇩z" .
abbreviation ω⇩z :: zhmultiset where
"ω⇩z ≡ ω⇩z^1"
lemma ω⇩z_as_ω: "ω⇩z = zhmset_of ω"
by simp
lift_definition times_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ zhmultiset" is
"λM N.
zmset_of (hmsetmset (HMSet (mset_pos M) * HMSet (mset_pos N)))
- zmset_of (hmsetmset (HMSet (mset_pos M) * HMSet (mset_neg N)))
+ zmset_of (hmsetmset (HMSet (mset_neg M) * HMSet (mset_neg N)))
- zmset_of (hmsetmset (HMSet (mset_neg M) * HMSet (mset_pos N)))" .
lemmas zhmsetmset_times = times_zhmultiset.rep_eq
instance
proof (intro_classes, goal_cases mult_assoc mult_comm mult_1 distrib zero_neq_one)
case (mult_assoc a b c)
show ?case
by (transfer,
simp add: algebra_simps zmset_of_plus[symmetric] hmsetmset_plus[symmetric] HMSet_diff,
rule triple_cross_mult_hmset)
next
case (mult_comm a b)
show ?case
by transfer (auto simp: algebra_simps)
next
case (mult_1 a)
show ?case
by transfer (auto simp: algebra_simps mset_pos_neg_partition[symmetric])
next
case (distrib a b c)
show ?case
by (simp add: times_zhmultiset_def ZHMSet_plus[symmetric] zmset_of_plus[symmetric]
hmsetmset_plus[symmetric] algebra_simps hmset_pos_plus hmset_neg_plus)
(simp add: mult.commute[of _ "hmset_pos c"] mult.commute[of _ "hmset_neg c"]
add.commute[of "hmset_neg c * M" "hmset_pos c * N" for M N]
add.assoc[symmetric] ring_distribs(1)[symmetric] hmset_pos_neg_dual)
next
case zero_neq_one
show ?case
unfolding zero_zhmultiset_def one_zhmultiset_def by simp
qed
end
lemma zhmset_of_1: "zhmset_of 1 = 1"
by (simp add: one_hmultiset_def one_zhmultiset_def)
lemma zhmset_of_times: "zhmset_of (A * B) = zhmset_of A * zhmset_of B"
by transfer simp
lemma zhmset_of_prod_list:
"zhmset_of (prod_list Ms) = prod_list (map zhmset_of Ms)"
by (induct Ms) (auto simp: one_hmultiset_def one_zhmultiset_def zhmset_of_times)
subsection ‹Embedding of Natural Numbers›
lemma of_nat_zhmset: "of_nat n = zhmset_of (of_nat n)"
by (induct n) (auto simp: zero_zhmultiset_def zhmset_of_plus zhmset_of_1)
lemma of_nat_inject_zhmset[simp]: "(of_nat m :: zhmultiset) = of_nat n ⟷ m = n"
unfolding of_nat_zhmset by simp
lemma plus_of_nat_plus_of_nat_zhmset:
"k + of_nat m + of_nat n = k + of_nat (m + n)" for k :: zhmultiset
by simp
lemma plus_of_nat_minus_of_nat_zhmset:
fixes k :: zhmultiset
assumes "n ≤ m"
shows "k + of_nat m - of_nat n = k + of_nat (m - n)"
using assms by (simp add: of_nat_diff)
lemma of_nat_lt_ω⇩z[simp]: "of_nat n < ω⇩z"
unfolding ω⇩z_as_ω using of_nat_lt_ω of_nat_zhmset zhmset_of_less by presburger
lemma of_nat_ne_ω⇩z[simp]: "of_nat n ≠ ω⇩z"
by (metis of_nat_lt_ω⇩z mset_le_asym mset_lt_single_iff)
subsection ‹Embedding of Extended Natural Numbers›
primrec zhmset_of_enat :: "enat ⇒ zhmultiset" where
"zhmset_of_enat (enat n) = of_nat n"
| "zhmset_of_enat ∞ = ω⇩z"
lemma zhmset_of_enat_0[simp]: "zhmset_of_enat 0 = 0"
by (simp add: zero_enat_def)
lemma zhmset_of_enat_1[simp]: "zhmset_of_enat 1 = 1"
by (simp add: one_enat_def del: One_nat_def)
lemma zhmset_of_enat_of_nat[simp]: "zhmset_of_enat (of_nat n) = of_nat n"
using of_nat_eq_enat by auto
lemma zhmset_of_enat_numeral[simp]: "zhmset_of_enat (numeral n) = numeral n"
by (simp add: numeral_eq_enat)
lemma zhmset_of_enat_le_ω⇩z[simp]: "zhmset_of_enat n ≤ ω⇩z"
using of_nat_lt_ω⇩z[THEN less_imp_le] by (cases n) auto
lemma zhmset_of_enat_eq_ω⇩z_iff[simp]: "zhmset_of_enat n = ω⇩z ⟷ n = ∞"
by (cases n) auto
subsection ‹Inequalities and Some (Dis)equalities›
instance zhmultiset :: zero_less_one
by (intro_classes, transfer, transfer, auto)
instantiation zhmultiset :: linordered_idom
begin
definition sgn_zhmultiset :: "zhmultiset ⇒ zhmultiset" where
"sgn_zhmultiset M = (if M = 0 then 0 else if M > 0 then 1 else -1)"
definition abs_zhmultiset :: "zhmultiset ⇒ zhmultiset" where
"abs_zhmultiset M = (if M < 0 then - M else M)"
lemma gt_0_times_gt_0_imp:
fixes a b :: zhmultiset
assumes a_gt0: "a > 0" and b_gt0: "b > 0"
shows "a * b > 0"
proof -
show ?thesis
using a_gt0 b_gt0
by (subst (asm) (2 4) zhmset_pos_neg_partition, simp, transfer,
simp del: HMSet_less add: algebra_simps zmset_of_plus[symmetric] hmsetmset_plus[symmetric]
zmset_of_less HMSet_less[symmetric])
(rule mono_cross_mult_less_hmset)
qed
instance
proof intro_classes
fix a b c :: zhmultiset
assume
a_lt_b: "a < b" and
zero_lt_c: "0 < c"
have "c * b < c * b + c * (b - a)"
using gt_0_times_gt_0_imp by (simp add: a_lt_b zero_lt_c)
hence "c * a + c * (b - a) < c * b + c * (b - a)"
by (simp add: right_diff_distrib')
thus "c * a < c * b"
by simp
qed (auto simp: sgn_zhmultiset_def abs_zhmultiset_def)
end
lemma le_zhmset_of_pos: "M ≤ zhmset_of (hmset_pos M)"
by (simp add: less_eq_zhmultiset.rep_eq mset_pos_supset subset_eq_imp_le_zmset)
lemma minus_zhmset_of_pos_le: "- zhmset_of (hmset_neg M) ≤ M"
by (metis le_zhmset_of_pos minus_le_iff mset_pos_uminus zhmsetmset_uminus)
lemma zhmset_of_nonneg[simp]: "zhmset_of M ≥ 0"
by (metis hmsetmset_0 zero_le_hmset zero_zhmultiset_def zhmset_of_le zmset_of_empty)
lemma
fixes n :: zhmultiset
assumes "0 ≤ m"
shows
le_add1_hmset: "n ≤ n + m" and
le_add2_hmset: "n ≤ m + n"
using assms by simp+
lemma less_iff_add1_le_zhmset: "m < n ⟷ m + 1 ≤ n" for m n :: zhmultiset
proof
assume m_lt_n: "m < n"
show "m + 1 ≤ n"
proof -
obtain hh :: hmultiset and zz :: zhmultiset and hha :: hmultiset where
f1: "m = zhmset_of hh + zz ∧ n = zhmset_of hha + zz ∧ hh < hha"
using less_hmset_zhmsetE[OF m_lt_n] by metis
hence "zhmset_of (hh + 1) ≤ zhmset_of hha"
by (metis (no_types) less_iff_add1_le_hmset zhmset_of_le)
thus ?thesis
using f1 by (simp add: zhmset_of_1 zhmset_of_plus)
qed
qed simp
lemma gt_0_lt_mult_gt_1_zhmset:
fixes m n :: zhmultiset
assumes "m > 0" and "n > 1"
shows "m < m * n"
using assms by simp
lemma zero_less_iff_1_le_zhmset: "0 < n ⟷ 1 ≤ n" for n :: zhmultiset
by (rule less_iff_add1_le_zhmset[of 0, simplified])
lemma less_add_1_iff_le_hmset: "m < n + 1 ⟷ m ≤ n" for m n :: zhmultiset
by (rule less_iff_add1_le_zhmset[of m "n + 1", simplified])
lemma nonneg_le_mult_right_mono_zhmset:
fixes x y z :: zhmultiset
assumes x: "0 ≤ x" and y: "0 < y" and z: "x ≤ z"
shows "x ≤ y * z"
using x zero_less_iff_1_le_zhmset[THEN iffD1, OF y] z
by (meson dual_order.trans leD mult_less_cancel_right2 not_le_imp_less)
instance hmultiset :: ordered_cancel_comm_semiring
by intro_classes
instance hmultiset :: linordered_semiring_1_strict
by intro_classes
instance hmultiset :: bounded_lattice_bot
by intro_classes
instance hmultiset :: zero_less_one
by intro_classes
instance hmultiset :: linordered_nonzero_semiring
by intro_classes
instance hmultiset :: semiring_no_zero_divisors
by intro_classes
lemma zero_lt_ω⇩z[simp]: "0 < ω⇩z"
by (metis of_nat_lt_ω⇩z of_nat_0)
lemma one_lt_ω[simp]: "1 < ω⇩z"
by (metis enat_defs(2) zhmset_of_enat.simps(1) zhmset_of_enat_1 of_nat_lt_ω⇩z)
lemma numeral_lt_ω⇩z[simp]: "numeral n < ω⇩z"
using zhmset_of_enat_numeral[symmetric] zhmset_of_enat.simps(1) of_nat_lt_ω⇩z numeral_eq_enat
by presburger
lemma one_le_ω⇩z[simp]: "1 ≤ ω⇩z"
by (simp add: less_imp_le)
lemma of_nat_le_ω⇩z[simp]: "of_nat n ≤ ω⇩z"
by (simp add: le_less)
lemma numeral_le_ω⇩z[simp]: "numeral n ≤ ω⇩z"
by (simp add: less_imp_le)
lemma not_ω⇩z_lt_1[simp]: "¬ ω⇩z < 1"
by (simp add: not_less)
lemma not_ω⇩z_lt_of_nat[simp]: "¬ ω⇩z < of_nat n"
by (simp add: not_less)
lemma not_ω⇩z_lt_numeral[simp]: "¬ ω⇩z < numeral n"
by (simp add: not_less)
lemma not_ω⇩z_le_1[simp]: "¬ ω⇩z ≤ 1"
by (simp add: not_le)
lemma not_ω⇩z_le_of_nat[simp]: "¬ ω⇩z ≤ of_nat n"
by (simp add: not_le)
lemma not_ω⇩z_le_numeral[simp]: "¬ ω⇩z ≤ numeral n"
by (simp add: not_le)
lemma zero_ne_ω⇩z[simp]: "0 ≠ ω⇩z"
using zero_lt_ω⇩z by linarith
lemma one_ne_ω⇩z[simp]: "1 ≠ ω⇩z"
using not_ω⇩z_le_1 by force
lemma numeral_ne_ω⇩z[simp]: "numeral n ≠ ω⇩z"
by (metis not_ω⇩z_le_numeral numeral_le_ω⇩z)
lemma
ω⇩z_ne_0[simp]: "ω⇩z ≠ 0" and
ω⇩z_ne_1[simp]: "ω⇩z ≠ 1" and
ω⇩z_ne_of_nat[simp]: "ω⇩z ≠ of_nat m" and
ω⇩z_ne_numeral[simp]: "ω⇩z ≠ numeral n"
using zero_ne_ω⇩z one_ne_ω⇩z of_nat_ne_ω⇩z numeral_ne_ω⇩z by metis+
lemma
zhmset_of_enat_inject[simp]: "zhmset_of_enat m = zhmset_of_enat n ⟷ m = n" and
zhmset_of_enat_lt_iff_lt[simp]: "zhmset_of_enat m < zhmset_of_enat n ⟷ m < n" and
zhmset_of_enat_le_iff_le[simp]: "zhmset_of_enat m ≤ zhmset_of_enat n ⟷ m ≤ n"
by (cases m; cases n; simp)+
lemma of_nat_lt_zhmset_of_enat_iff: "of_nat m < zhmset_of_enat n ⟷ enat m < n"
by (metis zhmset_of_enat.simps(1) zhmset_of_enat_lt_iff_lt)
lemma of_nat_le_zhmset_of_enat_iff: "of_nat m ≤ zhmset_of_enat n ⟷ enat m ≤ n"
by (metis zhmset_of_enat.simps(1) zhmset_of_enat_le_iff_le)
lemma zhmset_of_enat_lt_iff_ne_infinity: "zhmset_of_enat x < ω⇩z ⟷ x ≠ ∞"
by (cases x; simp)
subsection ‹An Example›
text ‹
A new proof of @{thm ludwig_waldmann_less}:
›
lemma
fixes α1 α2 β1 β2 γ δ :: hmultiset
assumes
αβ2γ_lt_αβ1γ: "α2 + β2 * γ < α1 + β1 * γ" and
β2_le_β1: "β2 ≤ β1" and
γ_lt_δ: "γ < δ"
shows "α2 + β2 * δ < α1 + β1 * δ"
proof -
let ?z = zhmset_of
note αβ2γ_lt_αβ1γ' = αβ2γ_lt_αβ1γ[THEN zhmset_of_less[THEN iffD2],
simplified zhmset_of_plus zhmset_of_times]
note β2_le_β1' = β2_le_β1[THEN zhmset_of_le[THEN iffD2]]
note γ_lt_δ' = γ_lt_δ[THEN zhmset_of_less[THEN iffD2]]
have "?z α2 + ?z β2 * ?z δ < ?z α1 + ?z β1 * ?z γ + ?z β2 * (?z δ - ?z γ)"
using αβ2γ_lt_αβ1γ' by (simp add: algebra_simps)
also have "… ≤ ?z α1 + ?z β1 * ?z γ + ?z β1 * (?z δ - ?z γ)"
using β2_le_β1' γ_lt_δ' by simp
finally show ?thesis
by (simp add: zmset_of_less zhmset_of_times[symmetric] zhmset_of_plus[symmetric] algebra_simps)
qed
end