Theory Signed_Syntactic_Ordinal

theory Signed_Syntactic_Ordinal
imports Signed_Hereditary_Multiset Syntactic_Ordinal
(*  Title:       Signed Syntactic Ordinals in Cantor Normal Form
    Author:      Jasmin Blanchette <jasmin.blanchette at>, 2016
    Author:      Mathias Fleury <mfleury at>, 2016
    Author:      Dmitriy Traytel <traytel at>, 2016
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at>

section ‹Signed Syntactic Ordinals in Cantor Normal Form›

theory Signed_Syntactic_Ordinal
imports Signed_Hereditary_Multiset Syntactic_Ordinal

subsection ‹Natural (Hessenberg) Product›

instantiation zhmultiset :: comm_ring_1

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

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)
  case (mult_comm a b)
  show ?case
    by transfer (auto simp: algebra_simps)
  case (mult_1 a)
  show ?case
    by transfer (auto simp: algebra_simps mset_pos_neg_partition[symmetric])
  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)
  case zero_neq_one
  show ?case
    unfolding zero_zhmultiset_def one_zhmultiset_def by simp


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

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)

proof intro_classes
  fix a b c :: zhmultiset

    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)


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)

  fixes n :: zhmultiset
  assumes "0 ≤ m"
    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
  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 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)

  ω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+

  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}:

  fixes α1 α2 β1 β2 γ δ :: hmultiset
    αβ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)