# Theory Syntactic_Ordinal_Bridge

theory Syntactic_Ordinal_Bridge
imports OrdinalOmega Syntactic_Ordinal
```(*  Title:       Syntactic Ordinals in Cantor Normal Form
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2017
Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
*)

theory Syntactic_Ordinal_Bridge
imports "HOL-Library.Sublist" Ordinal.OrdinalOmega Syntactic_Ordinal
abbrevs
"!h" = "⇩h"
begin

section ‹Bridge between Huffman's Ordinal Library and the Syntactic Ordinals›

subsection ‹Missing Lemmas about Huffman's Ordinals›

instantiation ordinal :: order_bot
begin

definition bot_ordinal :: ordinal where
"bot_ordinal = 0"

instance

end

lemma insort_bot[simp]: "insort bot xs = bot # xs" for xs :: "'a::{order_bot,linorder} list"

lemmas insort_0_ordinal[simp] = insort_bot[of "xs :: ordinal list" for xs, unfolded bot_ordinal_def]

lemma from_cnf_less_ω_exp:
assumes "∀k ∈ set ks. k < l"
shows "from_cnf ks < ω ** l"

lemma from_cnf_0_iff[simp]: "from_cnf ks = 0 ⟷ ks = []"
by (induct ks) (auto simp: ordinal_plus_not_0)

lemma from_cnf_append[simp]: "from_cnf (ks @ ls) = from_cnf ks + from_cnf ls"
by (induct ks) (auto simp: ordinal_plus_assoc)

lemma subseq_from_cnf_less_eq: "Sublist.subseq ks ls ⟹ from_cnf ks ≤ from_cnf ls"
by (induct rule: list_emb.induct) (auto intro: ordinal_le_plusL order_trans)

subsection ‹Embedding of Syntactic Ordinals into Huffman's Ordinals›

abbreviation ω⇩h :: hmultiset where
"ω⇩h ≡ Syntactic_Ordinal.ω"

abbreviation ω⇩h_exp :: "hmultiset ⇒ hmultiset" ("ω⇩h^") where
"ω⇩h^ ≡ Syntactic_Ordinal.ω_exp"

primrec ordinal_of_hmset :: "hmultiset ⇒ ordinal" where
"ordinal_of_hmset (HMSet M) =
from_cnf (rev (sorted_list_of_multiset (image_mset ordinal_of_hmset M)))"

lemma ordinal_of_hmset_0[simp]: "ordinal_of_hmset 0 = 0"
unfolding zero_hmultiset_def by simp

lemma ordinal_of_hmset_suc[simp]: "ordinal_of_hmset (k + 1) = ordinal_of_hmset k + 1"
unfolding plus_hmultiset_def one_hmultiset_def by (cases k) simp

lemma ordinal_of_hmset_1[simp]: "ordinal_of_hmset 1 = 1"
using ordinal_of_hmset_suc[of 0] by simp

lemma ordinal_of_hmset_ω[simp]: "ordinal_of_hmset ω⇩h = ω"
by simp

lemma ordinal_of_hmset_singleton[simp]: "ordinal_of_hmset (ω^k) = ω ** ordinal_of_hmset k"
by simp

lemma ordinal_of_hmset_iff[simp]: "ordinal_of_hmset k = 0 ⟷ k = 0"
by (induct k) auto

lemma less_imp_ordinal_of_hmset_less: "k < l ⟹ ordinal_of_hmset k < ordinal_of_hmset l"
proof (simp only: atomize_imp,
rule measure_induct_rule[of "λ(k, l). {#k, l#}"
"λ(k, l). k < l ⟶ ordinal_of_hmset k < ordinal_of_hmset l" "(k, l)",
simplified prod.case],
simp only: split_paired_all prod.case atomize_imp[symmetric])
fix k l
assume
ih: "⋀ka la. {#ka, la#} < {#k, l#} ⟹ ka < la ⟹ ordinal_of_hmset ka < ordinal_of_hmset la" and
k_lt_l: "k < l"

show "ordinal_of_hmset k < ordinal_of_hmset l"
proof (cases "k = 0")
case True
thus ?thesis
using k_lt_l ordinal_neq_0 by fastforce
next
case k_nz: False

have l_nz: "l ≠ 0"
using k_lt_l by auto

define K where K: "K = hmsetmset k"
define L where L: "L = hmsetmset l"

have k: "k = HMSet K" and l: "l = HMSet L"

have K_lt_L: "K < L"
unfolding K L using k_lt_l by simp

define x where x: "x = Max_mset K"
define Ka where Ka: "Ka = K - {#x#}"

have k_eq_xKa: "k = HMSet (add_mset x Ka)"
using K x Ka k_nz by auto
have x_max: "∀a ∈# Ka. a ≤ x"
unfolding x Ka by (meson Max_ge finite_set_mset in_diffD)

have ord_x_max: "∀a ∈# Ka. ordinal_of_hmset a ≤ ordinal_of_hmset x"
proof
fix a
assume a_in: "a ∈# Ka"

have a_le_x: "a ≤ x"
moreover
{
assume a_lt_x: "a < x"
moreover have x_lt_k: "x < k"
unfolding k_eq_xKa by (rule mem_imp_less_HMSet) simp
ultimately have a_lt_k: "a < k"
by simp

have "{#a, x#} < {#k#}"
using x_lt_k a_lt_k by simp
also have "… < {#k, l#}"
unfolding k_eq_xKa using a_in
by simp
finally have "ordinal_of_hmset a < ordinal_of_hmset x"
by (rule ih[OF _ a_lt_x])
}
ultimately show "ordinal_of_hmset a ≤ ordinal_of_hmset x"
by force
qed

define y where y: "y = Max_mset L"
define La where La: "La = L - {#y#}"

have l_eq_yLa: "l = HMSet (add_mset y La)"
using L y La l_nz by auto
have y_max: "∀b ∈# La. b ≤ y"
unfolding y La by (meson Max_ge finite_set_mset in_diffD)

have ord_y_max: "∀b ∈# La. ordinal_of_hmset b ≤ ordinal_of_hmset y"
proof
fix b
assume b_in: "b ∈# La"

have b_le_y: "b ≤ y"
moreover
{
assume b_lt_y: "b < y"
moreover have y_lt_l: "y < l"
unfolding l_eq_yLa by (rule mem_imp_less_HMSet) simp
ultimately have b_lt_l: "b < l"
by simp

have "{#b, y#} < {#l#}"
using y_lt_l b_lt_l by simp
also have "… < {#k, l#}"
unfolding l_eq_yLa using b_in
by simp
finally have "ordinal_of_hmset b < ordinal_of_hmset y"
by (rule ih[OF _ b_lt_y])
}
ultimately show "ordinal_of_hmset b ≤ ordinal_of_hmset y"
by force
qed

{
assume x_eq_y: "x = y"

have "ordinal_of_hmset (HMSet Ka) < ordinal_of_hmset (HMSet La)"
proof (rule ih)
show "{#HMSet Ka, HMSet La#} < {#k, l#}"
unfolding k l
le_multiset_right_total mset_lt_single_iff union_less_mono)
next
have "ω^x + HMSet Ka < ω^y + HMSet La"
using k_lt_l[unfolded k_eq_xKa l_eq_yLa]
thus "HMSet Ka < HMSet La"
using x_eq_y by simp
qed
hence ?thesis
unfolding k_eq_xKa l_eq_yLa
by (simp, subst (1 2) sorted_insort_is_snoc, simp_all add: ord_x_max ord_y_max,
force simp: x_eq_y)
}
moreover
{
assume x_ne_y: "x ≠ y"

have x_lt_y: "x < y"
less_imp_not_less mset_lt_single_iff neqE x x_ne_y y)

have ord_y_smax_K: "ordinal_of_hmset a < ordinal_of_hmset y" if a_in_K: "a ∈# K" for a
proof (rule ih)
show "{#a, y#} < {#k, l#}"
unfolding k_eq_xKa l_eq_yLa using a_in_K k k_eq_xKa
union_single_eq_member)
next
show "a < y"
by (metis Max_ge finite_set_mset less_le_trans not_less_iff_gr_or_eq that x x_lt_y)
qed

have "ordinal_of_hmset k < ordinal_of_hmset (ω^y)"
proof (cases La)
case empty
show ?thesis
unfolding k by (auto intro!: from_cnf_less_ω_exp simp: ord_y_smax_K)
next
show ?thesis
proof (rule ih)
show "{#k, ω^y#} < {#k, l#}"
unfolding l_eq_yLa La by simp
next
show "k < ω^y"
proof -
have "⋀m. x < Max_mset (add_mset y m)"
by (meson Max_ge finite_set_mset less_le_trans union_single_eq_member x_lt_y)
then show ?thesis
mset_lt_single_iff x_lt_y)
qed
qed
qed
also have "… ≤ ordinal_of_hmset l"
unfolding l_eq_yLa
by (auto simp del: from_cnf.simps intro!: subseq_from_cnf_less_eq
simp: subseq_from_cnf_less_eq sorted_insort_is_snoc ord_y_max)
ultimately have ?thesis
by simp
}
ultimately show ?thesis
by sat
qed
qed

lemma ordinal_of_hmset_less[simp]: "ordinal_of_hmset k < ordinal_of_hmset l ⟷ k < l"
using less_imp_not_less less_imp_ordinal_of_hmset_less neq_iff by blast

end
```