Theory Kirby

```section ‹Addition and Multiplication of Sets›

theory Kirby
imports ZFC_Cardinals

begin

text ‹Source: Laurence Kirby, Addition and multiplication of sets
Math. Log. Quart. 53, No. 1, 52-65 (2007) / DOI 10.1002/malq.200610026
@{url "http://faculty.baruch.cuny.edu/lkirby/mlqarticlejan2007.pdf"}›

instantiation V :: plus
begin

text‹This definition is credited to Tarski›
definition plus_V :: "V ⇒ V ⇒ V"
where "plus_V x ≡ transrec (λf z. x ⊔ set (f ` elts z))"

instance ..
end

definition lift :: "V ⇒ V ⇒ V"
where "lift x y ≡ set (plus x ` elts y)"

lemma plus: "x + y = x ⊔ set ((+)x ` elts y)"
unfolding plus_V_def  by (subst transrec) auto

lemma plus_eq_lift: "x + y = x ⊔ lift x y"
unfolding lift_def  using plus by blast

text‹Lemma 3.2›
lemma lift_sup_distrib: "lift x (a ⊔ b) = lift x a ⊔ lift x b"
by (simp add: image_Un lift_def sup_V_def)

lemma lift_Sup_distrib: "small Y ⟹ lift x (⨆ Y) = ⨆ (lift x ` Y)"
by (auto simp: lift_def Sup_V_def image_Union)

fixes x::V shows "y ≠ 0 ⟹ x + (⨆z∈elts y. f z) = (⨆z∈elts y. x + f z)"
by (auto simp: plus_eq_lift SUP_sup_distrib lift_Sup_distrib image_image)

fixes x::V shows "Limit α ⟹ x + (⨆z∈elts α. f z) = (⨆z∈elts α. x + f z)"

text‹Proposition 3.3(ii)›
begin
instance
proof
show "a + b + c = a + (b + c)" for a b c :: V
proof (induction c rule: eps_induct)
case (step c)
have "(a+b) + c = a + b ⊔ set ((+) (a + b) ` elts c)"
by (metis plus)
also have "… = a ⊔ lift a b ⊔ set ((λu. a + (b+u)) ` elts c)"
using plus_eq_lift step.IH by auto
also have "… = a ⊔ lift a (b + c)"
proof -
have "lift a b ⊔ set ((λu. a + (b + u)) ` elts c) = lift a (b + c)"
unfolding lift_def
by (metis elts_of_set image_image lift_def lift_sup_distrib plus_eq_lift replacement small_elts)
then show ?thesis
qed
also have "… = a + (b + c)"
using plus_eq_lift by auto
finally show ?case .
qed
show "0 + x = x" for x :: V
proof (induction rule: eps_induct)
case (step x)
then show ?case
by (subst plus) auto
qed
show "x + 0 = x" for x :: V
by (subst plus) auto
qed
end

lemma lift_0 [simp]: "lift 0 x = x"

lemma lift_by0 [simp]: "lift x 0 = 0"

lemma lift_by1 [simp]: "lift x 1 = set{x}"

fixes x y::V
shows "x+y = 0 ⟷ x=0 ∧ y=0"
proof safe
show "x = 0" if "x + y = 0"
by (metis that le_imp_less_or_eq not_less_0 plus sup_ge1)
then show "y = 0" if "x + y = 0"
using that by auto
qed auto

lemma plus_vinsert: "x + vinsert z y = vinsert (x+z) (x + y)"
proof -
have f1: "elts (x + y) = elts x ∪ (+) x ` elts y"
by (metis elts_of_set lift_def plus_eq_lift replacement small_Un small_elts sup_V_def)
moreover have "lift x (vinsert z y) = set ((+) x ` elts (set (insert z (elts y))))"
using vinsert_def lift_def by presburger
ultimately show ?thesis
by (simp add: vinsert_def plus_eq_lift sup_V_def)
qed

lemma plus_V_succ_right: "x + succ y = succ (x + y)"
by (metis plus_vinsert succ_def)

lemma succ_eq_add1: "succ x = x + 1"

lemma ord_of_nat_add: "ord_of_nat (m+n) = ord_of_nat m + ord_of_nat n"
by (induction n) (auto simp: plus_V_succ_right)

lemma succ_0_plus_eq [simp]:
assumes "α ∈ elts ω"
shows "succ 0 + α = succ α"
proof -
obtain n where "α = ord_of_nat n"
using assms elts_ω by blast
then show ?thesis
by (metis One_nat_def ord_of_nat.simps ord_of_nat_add plus_1_eq_Suc)
qed

assumes "α ∈ elts ω" "β ∈ elts ω" shows "α+β ∈ elts ω"
proof -
obtain m n where "α = ord_of_nat m" "β = ord_of_nat n"
using assms elts_ω by auto
then have "α+β = ord_of_nat (m+n)"
then show ?thesis
qed

lemma mem_plus_V_E:
assumes l: "l ∈ elts (x + y)"
obtains "l ∈ elts x" | z where "z ∈ elts y" "l = x + z"
using l by (auto simp: plus [of x y] split: if_split_asm)

lemma not_add_less_right: assumes "Ord y" shows "¬ (x + y < x)"
using assms
proof (induction rule: Ord_induct)
case (step i)
then show ?case
by (metis less_le_not_le plus sup_ge1)
qed

lemma not_add_mem_right: "¬ (x + y ∈ elts x)"
by (metis sup_ge1 mem_not_refl plus vsubsetD)

text‹Proposition 3.3(iii)›
lemma add_not_less_TC_self: "¬ x + y ⊏ x"
proof (induction y arbitrary: x rule: eps_induct)
case (step y)
then show ?case
using less_TC_imp_not_le plus_eq_lift by fastforce
qed

lemma TC_sup_lift: "TC x ⊓ lift x y = 0"
proof -
have "elts (TC x) ∩ elts (set ((+) x ` elts y)) = {}"
using add_not_less_TC_self by (auto simp: less_TC_def)
then have "TC x ⊓ set ((+) x ` elts y) = set {}"
by (metis inf_V_def)
then show ?thesis
using lift_def by auto
qed

lemma lift_lift: "lift x (lift y z) = lift (x+y) z"
using add.assoc  by (auto simp: lift_def)

lemma lift_self_disjoint: "x ⊓ lift x u = 0"
by (metis TC_sup_lift arg_subset_TC inf.absorb_iff2 inf_assoc inf_sup_aci(3) lift_0)

lemma sup_lift_eq_lift:
assumes "x ⊔ lift x u = x ⊔ lift x v"
shows "lift x u = lift x v"
by (metis (no_types) assms inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup_commute sup_inf_absorb)

text‹Proposition 3.4(i)›
proposition lift_eq_lift: "lift x y = lift x z ⟹ y = z"
proof (induction y arbitrary: z rule: eps_induct)
case (step y)
show ?case
proof (intro vsubsetI order_antisym)
show "u ∈ elts z" if "u ∈ elts y" for u
proof -
have "x+u ∈ elts (lift x z)"
using lift_def step.prems that by fastforce
then obtain v where "v ∈ elts z" "x+u = x+v"
using lift_def by auto
then have "lift x u = lift x v"
using sup_lift_eq_lift by (simp add: plus_eq_lift)
then have "u=v"
using step.IH that by blast
then show ?thesis
using ‹v ∈ elts z› by blast
qed
show "u ∈ elts y" if "u ∈ elts z" for u
proof -
have "x+u ∈ elts (lift x y)"
using lift_def step.prems that by fastforce
then obtain v where "v ∈ elts y" "x+u = x+v"
using lift_def by auto
then have "lift x u = lift x v"
using sup_lift_eq_lift by (simp add: plus_eq_lift)
then have "u=v"
using step.IH by (metis ‹v ∈ elts y›)
then show ?thesis
using ‹v ∈ elts y› by auto
qed
qed
qed

corollary inj_lift: "inj_on (lift x) A"
by (auto simp: inj_on_def dest: lift_eq_lift)

fixes x y z::V shows "x+y = x+z ⟷ y=z"
by (metis lift_eq_lift plus_eq_lift sup_lift_eq_lift)

fixes x y z::V shows "x+y ∈ elts (x+z) ⟷ y ∈ elts z"
apply safe
by (metis ZFC_in_HOL.ext dual_order.antisym elts_vinsert insert_subset order_refl plus_vinsert)

fixes x y z::V shows "x+y ≤ x+z ⟷ y≤z"
by auto (metis add_mem_right_cancel mem_plus_V_E plus sup_ge1 vsubsetD)

fixes x y z::V shows "x+y < x+z ⟷ y<z"

corollary lift_le_self [simp]: "lift x y ≤ x ⟷ y = 0"
by (auto simp: inf.absorb_iff2 lift_eq_lift lift_self_disjoint)

lemma succ_less_ω_imp: "succ x < ω ⟹ x < ω"

text‹Proposition 3.5›
lemma card_lift: "vcard (lift x y) = vcard y"
proof (rule cardinal_cong)
have "bij_betw ((+)x) (elts y) (elts (lift x y))"
unfolding bij_betw_def
then show "elts (lift x y) ≈ elts y"
using eqpoll_def eqpoll_sym by blast
qed

lemma eqpoll_lift: "elts (lift x y) ≈ elts y"
by (metis card_lift cardinal_eqpoll eqpoll_sym eqpoll_trans)

lemma vcard_add: "vcard (x + y) = vcard x ⊕ vcard y"
using card_lift [of x y] lift_self_disjoint [of x]

assumes "countable (elts A)" "countable (elts B)"
shows "countable (elts (A+B))"
proof -
have "vcard A ≤ ℵ0" "vcard B ≤ ℵ0"
using assms countable_iff_le_Aleph0 by blast+
then have "vcard (A+B) ≤ ℵ0"
by (metis Aleph_0 Card_ω InfCard_cdouble_eq InfCard_def cadd_le_mono order_refl)
then show ?thesis
qed

text‹Proposition 3.6›
proposition TC_add: "TC (x + y) = TC x ⊔ lift x (TC y)"
proof (induction y rule: eps_induct)
case (step y)
have *: "⨆ (TC ` (+) x ` elts y) = TC x ⊔ (⨆u∈elts y. TC (set ((+) x ` elts u)))"
if "elts y ≠ {}"
proof -
obtain w where "w ∈ elts y"
using ‹elts y ≠ {}› by blast
then have "TC x ≤ TC (x + w)"
then have †: "TC x ≤ (⨆w∈elts y. TC (x + w))"
using ‹w ∈ elts y› by blast
show ?thesis
using that
apply (intro conjI ballI impI order_antisym; clarsimp simp add: image_comp †)
apply(metis TC_sup_distrib Un_iff elts_sup_iff plus)
by (metis TC_least Transset_TC arg_subset_TC le_sup_iff plus vsubsetD)
qed
have "TC (x + y) = (x + y) ⊔ ⨆ (TC ` elts (x + y))"
using TC by blast
also have "… = x ⊔ lift x y ⊔ ⨆ (TC ` elts x) ⊔ ⨆ ((λu. TC (x+u)) ` elts y)"
apply (simp add: plus_eq_lift image_Un Sup_Un_distrib sup.left_commute sup_assoc TC_sup_distrib SUP_sup_distrib)
apply (simp add: lift_def sup.commute sup_aci *)
done
also have "… = x ⊔ ⨆ (TC ` elts x) ⊔ lift x y ⊔ ⨆ ((λu. TC x ⊔ lift x (TC u)) ` elts y)"
also have "… = TC x ⊔ lift x y ⊔ ⨆ ((λu. lift x (TC u)) ` elts y)"
by (simp add: sup_aci SUP_sup_distrib flip: TC [of x])
also have "… = TC x ⊔ lift x (y ⊔ ⨆ (TC ` elts y))"
by (metis (no_types) elts_of_set lift_Sup_distrib image_image lift_sup_distrib replacement small_elts sup_assoc)
also have "… = TC x ⊔ lift x (TC y)"
by (simp add: TC [of y])
finally show ?case .
qed

corollary TC_add': "z ⊏ x + y ⟷ z ⊏ x ∨ (∃v. v ⊏ y ∧ z = x + v)"
using TC_add by (force simp: less_TC_def lift_def)

text‹Corollary 3.7›
corollary vcard_TC_add: "vcard (TC (x+y)) = vcard (TC x) ⊕ vcard (TC y)"

text‹Corollary 3.8›
corollary TC_lift:
assumes "y ≠ 0"
shows "TC (lift x y) = TC x ⊔ lift x (TC y)"
proof -
have "TC (lift x y) = lift x y ⊔ ⨆ ((λu. TC(x+u)) ` elts y)"
unfolding TC [of "lift x y"]  by (simp add: lift_def image_image)
also have "… = lift x y ⊔ (⨆u∈elts y. TC x ⊔ lift x (TC u))"
also have "… = lift x y ⊔ TC x ⊔ (⨆u∈elts y. lift x (TC u))"
using assms by (auto simp: SUP_sup_distrib)
also have "… = TC x ⊔ lift x (TC y)"
by (simp add: TC [of y] sup_aci image_image lift_sup_distrib lift_Sup_distrib)
finally show ?thesis .
qed

proposition rank_add_distrib: "rank (x+y) = rank x + rank y"
proof (induction y rule: eps_induct)
case (step y)
show ?case
proof (cases "y=0")
case False
then obtain e where e: "e ∈ elts y"
by fastforce
have "rank (x+y) = (⨆u∈elts (x ⊔ ZFC_in_HOL.set ((+) x ` elts y)). succ (rank u))"
by (metis plus rank_Sup)
also have "… = (⨆x∈elts x. succ (rank x)) ⊔ (⨆z∈elts y. succ (rank x + rank z))"
apply (simp add: Sup_Un_distrib image_Un image_image)
apply (simp add: step cong: SUP_cong_simp)
done
also have "… = (⨆z ∈ elts y. rank x + succ (rank z))"
proof -
have "rank x ≤ (⨆z∈elts y. ZFC_in_HOL.succ (rank x + rank z))"
using ‹y ≠ 0›
by (auto simp: plus_eq_lift intro: order_trans [OF _ cSUP_upper [OF e]])
then show ?thesis
by (force simp: plus_V_succ_right simp flip: rank_Sup [of x] intro!: order_antisym)
qed
also have "… = rank x + (⨆z ∈ elts y. succ (rank z))"
also have "… = rank x + rank y"
by (simp add: rank_Sup [of y])
finally show ?thesis .
qed auto
qed

lemma Ord_add [simp]: "⟦Ord x; Ord y⟧ ⟹ Ord (x+y)"
proof (induction y rule: eps_induct)
case (step y)
then show ?case
qed

lemma add_Sup_distrib_id: "A ≠ 0 ⟹ x + ⨆(elts A) = (⨆z∈elts A. x + z)"

lemma add_Limit: "Limit α ⟹ x + α = (⨆z∈elts α. x + z)"
by (metis Limit_add_Sup_distrib Limit_eq_Sup_self image_ident image_image)

assumes "Ord α" "Ord β" shows "β ≤ α+β"
using ‹Ord β›
proof (induction rule: Ord_induct3)
case 0
then show ?case
by auto
next
case (succ α)
then show ?case
by (auto simp: plus_V_succ_right Ord_mem_iff_lt assms(1))
next
case (Limit μ)
then have k: "μ = (⨆β ∈ elts μ. β)"
also have "…  ≤ (⨆β ∈ elts μ. α + β)"
using Limit.IH by auto
also have "… = α + (⨆β ∈ elts μ. β)"
finally show ?case
using k by simp
qed

lemma plus_ω_equals_ω:
assumes "α ∈ elts ω"  shows "α + ω = ω"
proof (rule antisym)
show "α + ω ≤ ω"
using Ord_trans assms by (auto simp: elim!: mem_plus_V_E)
show "ω ≤ α + ω"
qed

lemma one_plus_ω_equals_ω [simp]: "1 + ω = ω"

subsubsection ‹Cancellation / set subtraction›

definition vle :: "V ⇒ V ⇒ bool" (infix "⊴" 50)
where "x ⊴ y ≡ ∃z::V. x+z = y"

lemma vle_refl [iff]: "x ⊴ x"

lemma vle_antisym: "⟦x ⊴ y; y ⊴ x⟧ ⟹ x = y"
by (metis V_equalityI plus_eq_lift sup_ge1 vle_def vsubsetD)

lemma vle_trans [trans]: "⟦x ⊴ y; y ⊴ z⟧ ⟹ x ⊴ z"

definition vle_comparable :: "V ⇒ V ⇒ bool"
where "vle_comparable x y ≡ x ⊴ y ∨ y ⊴ x"

text‹Lemma 3.13›
lemma comparable:
assumes "a+b = c+d"
shows "vle_comparable a c"
unfolding vle_comparable_def
proof (rule ccontr)
assume non: "¬ (a ⊴ c ∨ c ⊴ a)"
let ?φ = "λx. ∀z. a+x ≠ c+z"
have "?φ x" for x
proof (induction x rule: eps_induct)
case (step x)
show ?case
proof (cases "x=0")
case True
with non nonzero_less_TC show ?thesis
using vle_def by auto
next
case False
then obtain v where "v ∈ elts x"
show ?thesis
proof clarsimp
fix z
assume eq: "a + x = c + z"
then have "z ≠ 0"
using vle_def non by auto
have av: "a+v ∈ elts (a+x)"
by (simp add: ‹v ∈ elts x›)
moreover have "a+x = c ⊔ lift c z"
using eq plus_eq_lift by fastforce
ultimately have "a+v ∈ elts (c ⊔ lift c z)"
by simp
moreover
define u where "u ≡ set (elts x - {v})"
have u: "v ∉ elts u" and xeq: "x = vinsert v u"
using ‹v ∈ elts x› by (auto simp: u_def intro: order_antisym)
have case1: "a+v ∉ elts c"
proof
assume avc: "a + v ∈ elts c"
then have "a ≤ c"
by clarify (metis Un_iff elts_sup_iff eq mem_not_sym mem_plus_V_E plus_eq_lift)
moreover have "a ⊔ lift a x = c ⊔ lift c z"
using eq by (simp add: plus_eq_lift)
ultimately have "lift c z ≤ lift a x"
by (metis inf.absorb_iff2 inf_commute inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup.commute)
also have "… = vinsert (a+v) (lift a u)"
by (simp add: lift_def vinsert_def xeq)
finally have *: "lift c z ≤ vinsert (a + v) (lift a u)" .
have "lift c z ≤ lift a u"
proof -
have "a + v ∉ elts (lift c z)"
using lift_self_disjoint [of c z] avc V_disjoint_iff by auto
then show ?thesis
using * less_eq_V_def by auto
qed
{ fix e
assume "e ∈ elts z"
then have "c+e ∈ elts (lift c z)"
then have "c+e ∈ elts (lift a u)"
using ‹lift c z ≤ lift a u› by blast
then obtain y where "y ∈ elts u" "c+e = a+y"
using lift_def by auto
then have False
by (metis elts_vinsert insert_iff step.IH xeq)
}
then show False
using ‹z ≠ 0› by fastforce
qed
ultimately show False
by (metis (no_types) ‹v ∈ elts x› av case1 eq mem_plus_V_E step.IH)
qed
qed
qed
then show False
using assms by blast
qed

lemma vle1: "x ⊴ y ⟹ x ≤ y"
using vle_def plus_eq_lift by auto

lemma vle2: "x ⊴ y ⟹ x ⊑ y"

lemma vle_iff_le_Ord:
assumes "Ord α" "Ord β"
shows "α ⊴ β ⟷ α ≤ β"
proof
show "α ≤ β" if "α ⊴ β"
using that by (simp add: vle1)
show "α ⊴ β" if "α ≤ β"
using ‹Ord α› ‹Ord β› that
proof (induction α arbitrary: β rule: Ord_induct)
case (step γ)
then show ?case
unfolding vle_def
qed
qed

fixes x::V shows "x ≤ x+z"

fixes x::V shows "x < x+z ⟷ 0<z"

lemma le_Ord_diff:
assumes "α ≤ β" "Ord α" "Ord β"
obtains γ where "α+γ = β" "γ ≤ β" "Ord γ"
proof -
obtain γ where γ: "α+γ = β" "γ ≤ β"
then have "Ord γ"
using Ord_def Transset_def ‹Ord β› by force
with γ that show thesis by blast
qed

lemma plus_Ord_le:
assumes "α ∈ elts ω" "Ord β" shows "α+β ≤ β+α"
proof (cases "β ∈ elts ω")
case True
with assms have "α+β = β+α"
then show ?thesis by simp
next
case False
then have "ω ≤ β"
using Ord_linear2 Ord_mem_iff_lt ‹Ord β› by auto
then obtain γ where "ω+γ = β" "γ ≤ β" "Ord γ"
using ‹Ord β› le_Ord_diff by auto
then have "α+β = β"
then show ?thesis
by simp
qed

lemma add_right_mono: "⟦α ≤ β; Ord α; Ord β; Ord γ⟧ ⟹ α+γ ≤ β+γ"

lemma add_strict_mono: "⟦α < β; γ < δ; Ord α; Ord β; Ord γ; Ord δ⟧ ⟹ α+γ < β+δ"

lemma add_right_strict_mono: "⟦α ≤ β; γ < δ; Ord α; Ord β; Ord γ; Ord δ⟧ ⟹ α+γ < β+δ"

assumes "Limit μ" "Ord β" shows "Limit (β + μ)"
unfolding Limit_def
proof (intro conjI allI impI)
show "Ord (β + μ)"
using Limit_def assms by auto
show "0 ∈ elts (β + μ)"
using Limit_def add_le_left assms by auto
next
fix γ
assume "γ ∈ elts (β + μ)"
then consider "γ ∈ elts β" | ξ where "ξ ∈ elts μ" "γ = β + ξ"
using mem_plus_V_E by blast
then show "succ γ ∈ elts (β + μ)"
proof cases
case 1
then show ?thesis
next
case 2
then show ?thesis
by (metis Limit_def add_mem_right_cancel assms(1) plus_V_succ_right)
qed
qed

subsection ‹Generalised Difference›

definition odiff where "odiff y x ≡ THE z::V. (x+z = y) ∨ (z=0 ∧ ¬ x ⊴ y)"

lemma vle_imp_odiff_eq: "x ⊴ y ⟹ x + (odiff y x) = y"
by (auto simp: vle_def odiff_def)

lemma not_vle_imp_odiff_0: "¬ x ⊴ y ⟹ (odiff y x) = 0"
by (auto simp: vle_def odiff_def)

lemma Ord_odiff_eq:
assumes "α ≤ β" "Ord α" "Ord β"
shows "α + odiff β α = β"
by (simp add: assms vle_iff_le_Ord vle_imp_odiff_eq)

lemma Ord_odiff:
assumes "Ord α" "Ord β" shows "Ord (odiff β α)"
proof (cases "α ⊴ β")
case True
then show ?thesis
by (metis add_right_cancel assms le_Ord_diff vle1 vle_imp_odiff_eq)
next
case False
then show ?thesis
qed

lemma Ord_odiff_le:
assumes  "Ord α" "Ord β" shows "odiff β α ≤ β"
proof (cases "α ⊴ β")
case True
then show ?thesis
by (metis add_right_cancel assms le_Ord_diff vle1 vle_imp_odiff_eq)
next
case False
then show ?thesis
qed

lemma odiff_0_right [simp]: "odiff x 0 = x"

lemma odiff_succ: "y ⊴ x ⟹ odiff (succ x) y = succ (odiff x y)"
unfolding odiff_def
by (metis add_right_cancel odiff_def plus_V_succ_right vle_def vle_imp_odiff_eq)

lemma odiff_eq_iff: "z ⊴ x ⟹ odiff x z = y ⟷ x = z + y"
by (auto simp: odiff_def vle_def)

lemma odiff_le_iff: "z ⊴ x ⟹ odiff x z ≤ y ⟷ x ≤ z + y"
by (auto simp: odiff_def vle_def)

lemma odiff_less_iff: "z ⊴ x ⟹ odiff x z < y ⟷ x < z + y"
by (auto simp: odiff_def vle_def)

lemma odiff_ge_iff: "z ⊴ x ⟹ odiff x z ≥ y ⟷ x ≥ z + y"
by (auto simp: odiff_def vle_def)

lemma Ord_odiff_le_iff: "⟦α ≤ x; Ord x; Ord α⟧ ⟹ odiff x α ≤ y ⟷ x ≤ α + y"

lemma odiff_le_odiff:
assumes "x ⊴ y" shows "odiff x z ≤ odiff y z"
proof (cases "z ⊴ x")
case True
then show ?thesis
using assms odiff_le_iff vle1 vle_imp_odiff_eq vle_trans by presburger
next
case False
then show ?thesis
qed

lemma Ord_odiff_le_odiff: "⟦x ≤ y; Ord x; Ord y⟧ ⟹ odiff x α ≤ odiff y α"

lemma Ord_odiff_less_odiff: "⟦α ≤ x; x < y; Ord x; Ord y; Ord α⟧ ⟹ odiff x α < odiff y α"
by (metis Ord_odiff_eq Ord_odiff_le_odiff dual_order.strict_trans less_V_def)

lemma Ord_odiff_less_imp_less: "⟦odiff x α < odiff y α; Ord x; Ord y⟧ ⟹ x < y"
by (meson Ord_linear2 leD odiff_le_odiff vle_iff_le_Ord)

lemma odiff_add_cancel [simp]: "odiff (x + y) x = y"

lemma odiff_add_cancel_0 [simp]: "odiff x x = 0"

lemma odiff_add_cancel_both [simp]: "odiff (x + y) (x + z) = odiff y z"

subsection ‹Generalised Multiplication›

text ‹Credited to Dana Scott›

instantiation V :: times
begin

text‹This definition is credited to Tarski›
definition times_V :: "V ⇒ V ⇒ V"
where "times_V x ≡ transrec (λf y. ⨆ ((λu. lift (f u) x) ` elts y))"

instance ..
end

lemma mult: "x * y = (⨆u∈elts y. lift (x * u) x)"
unfolding times_V_def  by (subst transrec) (force simp:)

lemma elts_multE:
assumes "z ∈ elts (x * y)"
obtains u v where "u ∈ elts x" "v ∈ elts y" "z = x*v + u"
using mult [of x y] lift_def assms by auto

text ‹Lemma 4.2›

lemma mult_zero_right [simp]:
fixes x::V shows "x * 0 = 0"
by (metis ZFC_in_HOL.Sup_empty elts_0 image_empty mult)

lemma mult_insert: "x * (vinsert y z) = x*z ⊔ lift (x*y) x"
by (metis (no_types, lifting) elts_vinsert image_insert replacement small_elts sup_commute mult Sup_V_insert)

lemma mult_succ: "x * succ y = x*y + x"
by (simp add: mult_insert plus_eq_lift succ_def)

lemma ord_of_nat_mult: "ord_of_nat (m*n) = ord_of_nat m * ord_of_nat n"
proof (induction n)
case (Suc n)
then show ?case
qed auto

lemma omega_closed_mult [intro]:
assumes "α ∈ elts ω" "β ∈ elts ω" shows "α*β ∈ elts ω"
proof -
obtain m n where "α = ord_of_nat m" "β = ord_of_nat n"
using assms elts_ω by auto
then have "α*β = ord_of_nat (m*n)"
then show ?thesis
qed

lemma zero_imp_le_mult: "0 ∈ elts y ⟹ x ≤ x*y"
by (auto simp: mult [of x y])

subsubsection‹Proposition 4.3›

lemma mult_zero_left [simp]:
fixes x::V shows "0 * x = 0"
proof (induction x rule: eps_induct)
case (step x)
then show ?case
by (subst mult) auto
qed

lemma mult_sup_distrib:
fixes x::V shows "x * (y ⊔ z) = x*y ⊔ x*z"
unfolding mult [of x "y ⊔ z"] mult [of x y] mult [of x z]

lemma mult_Sup_distrib: "small Y ⟹ x * (⨆Y) = ⨆ ((*) x ` Y)" for Y:: "V set"
unfolding mult [of x "⨆Y"]
by (simp add: cSUP_UNION) (metis mult)

lemma mult_lift_imp_distrib: "x * (lift y z) = lift (x*y) (x*z) ⟹ x * (y+z) = x*y + x*z"

lemma mult_lift: "x * (lift y z) = lift (x*y) (x*z)"
proof (induction z rule: eps_induct)
case (step z)
have "x * lift y z = (⨆u∈elts (lift y z). lift (x * u) x)"
using mult by blast
also have "… = (⨆v∈elts z. lift (x * (y + v)) x)"
using lift_def by auto
also have "… = (⨆v∈elts z. lift (x * y + x * v) x)"
using mult_lift_imp_distrib step.IH by auto
also have "… = (⨆v∈elts z. lift (x * y) (lift (x * v) x))"
also have "… = lift (x * y) (⨆v∈elts z. lift (x * v) x)"
also have "… = lift (x*y) (x*z)"
by (metis mult)
finally show ?case .
qed

lemma mult_Limit: "Limit γ ⟹ x * γ = ⨆ ((*) x ` elts γ)"
by (metis Limit_eq_Sup_self mult_Sup_distrib small_elts)

lemma add_mult_distrib: "x * (y+z) = x*y + x*z" for x::V

instantiation V :: monoid_mult
begin
instance
proof
show "1 * x = x" for x :: V
proof (induction x rule: eps_induct)
case (step x)
then show ?case
by (subst mult) auto
qed
show "x * 1 = x" for x :: V
by (subst mult) auto
show "(x * y) * z = x * (y * z)" for x y z::V
proof (induction z rule: eps_induct)
case (step z)
have "(x * y) * z = (⨆u∈elts z. lift (x * y * u) (x * y))"
using mult by blast
also have "… = (⨆u∈elts z. lift (x * (y * u)) (x * y))"
using step.IH by auto
also have "… = (⨆u∈elts z. x * lift (y * u) y)"
using mult_lift by auto
also have "… = x * (⨆u∈elts z. lift (y * u) y)"
also have "… = x * (y * z)"
by (metis mult)
finally show ?case .
qed
qed

end

lemma le_mult:
assumes "Ord β" "β ≠ 0" shows "α ≤ α * β"
using assms
proof (induction rule: Ord_induct3)
case (succ α)
then show ?case
using mult_insert succ_def by fastforce
next
case (Limit μ)
have "α ∈ (*) α ` elts μ"
using Limit.hyps Limit_def one_V_def by (metis imageI mult.right_neutral)
then have "α ≤ ⨆ ((*) α ` elts μ)"
by auto
then show ?case
qed auto

lemma mult_sing_1 [simp]:
fixes x::V shows "x * set{1} = lift x x"
by (subst mult) auto

lemma mult_2_right [simp]:
fixes x::V shows "x * set{0,1} = x+x"
by (subst mult) (auto simp: Sup_V_insert plus_eq_lift)

lemma Ord_mult [simp]: "⟦Ord y; Ord x⟧ ⟹ Ord (x*y)"
proof (induction y rule: Ord_induct3)
case 0
then show ?case
by auto
next
case (succ k)
then show ?case
next
case (Limit k)
then have "Ord (x * ⨆ (elts k))"
by (metis Ord_Sup imageE mult_Sup_distrib small_elts)
then show ?case
using Limit.hyps Limit_eq_Sup_self by auto
qed

subsubsection ‹Proposition 4.4-5›
proposition rank_mult_distrib: "rank (x*y) = rank x * rank y"
proof (induction y rule: eps_induct)
case (step y)
have "rank (x*y) = (⨆y∈elts (⨆u∈elts y. lift (x * u) x). succ (rank y))"
by (metis rank_Sup mult)
also have "… = (⨆u∈elts y. ⨆r∈elts x. succ (rank (x * u + r)))"
apply (simp add: lift_def image_image image_UN)
done
also have "… = (⨆u∈elts y. ⨆r∈elts x. succ (rank (x * u) + rank r))"
also have "… = (⨆u∈elts y. ⨆r∈elts x. succ (rank x * rank u + rank r))"
using step arg_cong [where f = Sup] by auto
also have "… = (⨆u∈elts y. rank x * rank u + rank x)"
proof (rule SUP_cong)
show "(⨆r∈elts x. succ (rank x * rank u + rank r)) = rank x * rank u + rank x"
if "u ∈ elts y" for u
proof (cases "x=0")
case False
have "(⨆r∈elts x. succ (rank x * rank u + rank r)) = rank x * rank u + (⨆y∈elts x. succ (rank y))"
proof (rule order_antisym)
show "(⨆r∈elts x. succ (rank x * rank u + rank r)) ≤ rank x * rank u + (⨆y∈elts x. succ (rank y))"
by (auto simp: Sup_le_iff simp flip: plus_V_succ_right)
have "rank x * rank u + (⨆y∈elts x. succ (rank y)) = (⨆y∈elts x. rank x * rank u + succ (rank y))"
also have "… ≤ (⨆r∈elts x. succ (rank x * rank u + rank r))"
using plus_V_succ_right by auto
finally show "rank x * rank u + (⨆y∈elts x. succ (rank y)) ≤ (⨆r∈elts x. succ (rank x * rank u + rank r))" .
qed
also have "… = rank x * rank u + rank x"
by (metis rank_Sup)
finally show ?thesis .
qed auto
qed auto
also have "… = rank x * rank y"
by (simp add: rank_Sup [of y] mult_Sup_distrib mult_succ image_image)
finally show ?case .
qed

lemma mult_le1:
fixes y::V assumes "y ≠ 0" shows "x ⊑ x * y"
proof (cases "x = 0")
case False
then obtain r where r: "r ∈ elts x"
by fastforce
from ‹y ≠ 0› show ?thesis
proof (induction y rule: eps_induct)
case (step y)
show ?case
proof (cases "y = 1")
case False
with ‹y ≠ 0› obtain p where p: "p ∈ elts y" "p ≠ 0"
by (metis V_equalityI elts_1 insertI1 singletonD trad_foundation)
then have "x*p + r ∈ elts (lift (x*p) x)"
moreover have "lift (x*p) x ≤ x*y"
by (metis bdd_above_iff_small cSUP_upper2 order_refl ‹p ∈ elts y› replacement small_elts mult)
ultimately have "x*p + r ∈ elts (x*y)"
by blast
moreover have "x*p ⊑ x*p + r"
ultimately show ?thesis
using step.IH [OF p] le_TC_trans less_TC_iff by blast
qed auto
qed
qed auto

lemma mult_eq_0_iff [simp]:
fixes y::V shows "x * y = 0 ⟷ x=0 ∨ y=0"
proof
show "x = 0 ∨ y = 0" if "x * y = 0"
by (metis le_0 le_TC_def less_TC_imp_not_le mult_le1 that)
qed auto

lemma lift_lemma:
assumes "x ≠ 0" "y ≠ 0"  shows "¬ lift (x * y) x ≤ x"
using assms mult_le1 [of concl: x y]
by (auto simp: le_TC_def TC_lift less_TC_def less_TC_imp_not_le)

lemma mult_le2:
fixes y::V assumes "x ≠ 0" "y ≠ 0" "y ≠ 1" shows "x ⊏ x * y"
proof -
obtain v where v: "v ∈ elts y" "v ≠ 0"
using assms by fastforce
have "x ≠ x * y"
using lift_lemma [of x v]
by (metis ‹x ≠ 0› bdd_above_iff_small cSUP_upper2 order_refl replacement small_elts mult v)
then show ?thesis
using assms mult_le1 [of y x]
by (auto simp: le_TC_def)
qed

lemma elts_mult_ωE:
assumes "x ∈ elts (y * ω)"
obtains n where "n ≠ 0" "x ∈ elts (y * ord_of_nat n)" "⋀m. m < n ⟹ x ∉ elts (y * ord_of_nat m)"
proof -
obtain k where k:  "k ≠ 0 ∧ x ∈ elts (y * ord_of_nat k)"
using assms
by (metis mult_eq_0_iff elts_0 ex_in_conv ord_of_eq_0_iff that)
define n where "n ≡ (LEAST k. k ≠ 0 ∧ x ∈ elts (y * ord_of_nat k))"
show thesis
proof
show "n ≠ 0" "x ∈ elts (y * ord_of_nat n)"
unfolding n_def by (metis (mono_tags, lifting) LeastI_ex k)+
show "⋀m. m < n ⟹ x ∉ elts (y * ord_of_nat m)"
by (metis (mono_tags, lifting) mult_eq_0_iff elts_0 empty_iff n_def not_less_Least ord_of_eq_0_iff)
qed
qed

subsubsection‹Theorem 4.6›

theorem mult_eq_imp_0:
assumes "a*x = a*y + b" "b ⊏ a"
shows "b=0"
proof (cases "a=0 ∨ x=0")
case True
with assms show ?thesis
by (metis add_le_cancel_left mult_eq_0_iff eq_iff le_0)
next
case False
then have "a≠0" "x≠0"
by auto
then show ?thesis
proof (cases "y=0")
case True
then show ?thesis
using assms less_asym_TC mult_le2 by force
next
case False
have "b=0" if "Ord α" "x ∈ elts (Vset α)" "y ∈ elts (Vset α)" for α
using that assms
proof (induction α arbitrary: x y b rule: Ord_induct3)
case 0
then show ?case by auto
next
case (succ k)
define Φ where "Φ ≡ λx y. ∃r. 0 ⊏ r ∧ r ⊏ a ∧ a*x = a*y + r"
show ?case
proof (rule ccontr)
assume "b ≠ 0"
then have "0 ⊏ b"
by (metis nonzero_less_TC)
then have "Φ x y"
unfolding Φ_def using succ.prems by blast
then obtain x' where "Φ x' y" "x' ⊑ x" and min: "⋀x''. x'' ⊏ x' ⟹ ¬ Φ x'' y"
using less_TC_minimal [of "λx. Φ x y" x] by blast
then obtain b' where "0 ⊏ b'" "b' ⊏ a" and eq: "a*x' = a*y + b'"
using Φ_def by blast
have "a*y ⊏ a*x'"
using TC_add' ‹0 ⊏ b'› eq by auto
then obtain p where "p ∈ elts (a * x')" "a * y ⊑ p"
using less_TC_iff by blast
then have "p ∉ elts (a * y)"
using less_TC_iff less_irrefl_TC by blast
then have "p ∈ ⋃ (elts ` (λv. lift (a * v) a) ` elts x')"
by (metis ‹p ∈ elts (a * x')› elts_Sup replacement small_elts mult)
then obtain u c where "u ∈ elts x'" "c ∈ elts a" "p = a*u + c"
using lift_def by auto
then have "p ∈ elts (lift (a*y) b')"
using ‹p ∈ elts (a * x')› ‹p ∉ elts (a * y)› eq plus_eq_lift by auto
then obtain d where d: "d ∈ elts b'" "p = a*y + d" "p = a*u + c"
by (metis ‹p = a * u + c› ‹p ∈ elts (a * x')› ‹p ∉ elts (a * y)› eq mem_plus_V_E)
have noteq: "a*y ≠ a*u"
proof
assume "a*y = a*u"
then have "lift (a*y) a = lift (a*u) a"
by metis
also have "… ≤ a*x'"
unfolding mult [of _ x'] using ‹u ∈ elts x'› by (auto intro: cSUP_upper)
also have "… = a*y ⊔ lift (a*y) b'"
finally have "lift (a*y) a ≤ a*y ⊔ lift (a*y) b'" .
then have "lift (a*y) a ≤ lift (a*y) b'"
using add_le_cancel_left less_TC_imp_not_le plus_eq_lift ‹b' ⊏ a› by auto
then have "a ≤ b'"
by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
then show False
using ‹b' ⊏ a› less_TC_imp_not_le by auto
qed
consider "a*y ⊴ a*u" | "a*u ⊴ a*y"
using d comparable vle_comparable_def by auto
then show False
proof cases
case 1
then obtain e where e: "a*u = a*y + e" "e ≠ 0"
moreover have "e + c = d"
by (metis e add_right_cancel ‹p = a * u + c› ‹p = a * y + d› add.assoc)
with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
by (meson less_TC_iff less_TC_trans vle2 vle_def)
ultimately show False
using min unfolding Φ_def by (meson ‹u ∈ elts x'› le_TC_def less_TC_iff nonzero_less_TC)
next
case 2
then obtain e where e: "a*y = a*u + e" "e ≠ 0"
moreover have "e + d = c"
by (metis e add_right_cancel ‹p = a * u + c› ‹p = a * y + d› add.assoc)
with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
by (metis ‹c ∈ elts a› less_TC_iff vle2 vle_def)
ultimately have "Φ y u"
unfolding Φ_def using nonzero_less_TC by blast
then obtain y' where "Φ y' u" "y' ⊑ y" and min: "⋀x''. x'' ⊏ y' ⟹ ¬ Φ x'' u"
using less_TC_minimal [of "λx. Φ x u" y] by blast
then obtain b' where "0 ⊏ b'" "b' ⊏ a" and eq: "a*y' = a*u + b'"
using Φ_def by blast
have u_k: "u ∈ elts (Vset k)"
using ‹u ∈ elts x'› ‹x' ⊑ x› succ Vset_succ_TC less_TC_iff less_le_TC_trans by blast
have "a*u ⊏ a*y'"
using TC_add' ‹0 ⊏ b'› eq by auto
then obtain p where "p ∈ elts (a * y')" "a * u ⊑ p"
using less_TC_iff by blast
then have "p ∉ elts (a * u)"
using less_TC_iff less_irrefl_TC by blast
then have "p ∈ ⋃ (elts ` (λv. lift (a * v) a) ` elts y')"
by (metis ‹p ∈ elts (a * y')› elts_Sup replacement small_elts mult)
then obtain v c where "v ∈ elts y'" "c ∈ elts a" "p = a*v + c"
using lift_def by auto
then have "p ∈ elts (lift (a*u) b')"
using ‹p ∈ elts (a * y')› ‹p ∉ elts (a * u)› eq plus_eq_lift by auto
then obtain d where d: "d ∈ elts b'" "p = a*u + d" "p = a*v + c"
by (metis ‹p = a * v + c› ‹p ∈ elts (a * y')› ‹p ∉ elts (a * u)› eq mem_plus_V_E)
have v_k: "v ∈ elts (Vset k)"
using Vset_succ_TC ‹v ∈ elts y'› ‹y' ⊑ y› less_TC_iff less_le_TC_trans succ.hyps succ.prems(2) by blast
have noteq: "a*u ≠ a*v"
proof
assume "a*u = a*v"
then have "lift (a*v) a ≤ a*y'"
unfolding mult [of _ y'] using ‹v ∈ elts y'› by (auto intro: cSUP_upper)
also have "… = a*u ⊔ lift (a*u) b'"
finally have "lift (a*v) a ≤ a*u ⊔ lift (a*u) b'" .
then have "lift (a*u) a ≤ lift (a*u) b'"
by (metis ‹a * u = a * v› le_iff_sup lift_sup_distrib sup_left_commute sup_lift_eq_lift)
then have "a ≤ b'"
by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
then show False
using ‹b' ⊏ a› less_TC_imp_not_le by auto
qed
consider "a*u ⊴ a*v" | "a*v ⊴ a*u"
using d comparable vle_comparable_def by auto
then show False
proof cases
case 1
then obtain e where e: "a*v = a*u + e" "e ≠ 0"
moreover have "e + c = d"
by (metis add_right_cancel ‹p = a * u + d› ‹p = a * v + c› add.assoc e)
with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
by (meson less_TC_iff less_TC_trans vle2 vle_def)
ultimately show False
using succ.IH u_k v_k by blast
next
case 2
then obtain e where e: "a*u = a*v + e" "e ≠ 0"
moreover have "e + d = c"
with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
by (metis ‹c ∈ elts a› less_TC_iff vle2 vle_def)
ultimately show False
using succ.IH u_k v_k by blast
qed
qed
qed
next
case (Limit k)
obtain i j where k: "i ∈ elts k" "j ∈ elts k"
and x: "x ∈ elts (Vset i)"
and y: "y ∈ elts (Vset j)"
using that Limit by (auto simp: Limit_Vfrom_eq)
show ?case
proof (rule Limit.IH [of "i ⊔ j"])
show "i ⊔ j ∈ elts k"
by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff)
show "x ∈ elts (Vset (i ⊔ j))" "y ∈ elts (Vset (i ⊔ j))"
using x y by (auto simp: Vfrom_sup)
qed (use Limit.prems in auto)
qed
then show ?thesis
by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt)
qed
qed

subsubsection‹Theorem 4.7›

lemma mult_cancellation_half:
assumes "a*x + r ≤ a*y + s" "r ⊏ a" "s ⊏ a"
shows "x ≤ y"
proof -
have "x ≤ y" if "Ord α" "x ∈ elts (Vset α)" "y ∈ elts (Vset α)" for α
using that assms
proof (induction α arbitrary: x y r s rule: Ord_induct3)
case 0
then show ?case
by auto
next
case (succ k)
show ?case
proof
fix u
assume u: "u ∈ elts x"
have u_k: "u ∈ elts (Vset k)"
using Vset_succ succ.hyps succ.prems(1) u by auto
obtain r' where "r' ∈ elts a" "r ⊑ r'"
using less_TC_iff succ.prems(4) by blast
have "a*u + r' ∈ elts (lift (a*u) a)"
by (simp add: ‹r' ∈ elts a› lift_def)
also have "… ≤ elts (a*x)"
using u by (force simp: mult [of _ x])
also have "… ≤ elts (a*y + s)"
using plus_eq_lift succ.prems(3) by auto
also have "… = elts (a*y) ∪ elts (lift (a*y) s)"
finally have "a * u + r' ∈ elts (a * y) ∪ elts (lift (a * y) s)" .
then show "u ∈ elts y"
proof
assume *: "a * u + r' ∈ elts (a * y)"
show "u ∈ elts y"
proof -
obtain v e where v: "v ∈ elts y" "e ∈ elts a" "a * u + r' = a * v + e"
using * by (auto simp: mult [of _ y] lift_def)
then have v_k: "v ∈ elts (Vset k)"
using Vset_succ_TC less_TC_iff succ.prems(2) by blast
then show ?thesis
by (metis ‹r' ∈ elts a› antisym le_TC_refl less_TC_iff order_refl succ.IH u_k v)
qed
next
assume "a * u + r' ∈ elts (lift (a * y) s)"
then obtain t where "t ∈ elts s" and t: "a * u + r' = a * y + t"
using lift_def by auto
have noteq: "a*y ≠ a*u"
proof
assume "a*y = a*u"
then have "lift (a*y) a = lift (a*u) a"
by metis
also have "… ≤ a*x"
unfolding mult [of _ x] using ‹u ∈ elts x› by (auto intro: cSUP_upper)
also have "… ≤ a*y ⊔ lift (a*y) s"
using ‹elts (a * x) ⊆ elts (a * y + s)› plus_eq_lift by auto
finally have "lift (a*y) a ≤ a*y ⊔ lift (a*y) s" .
then have "lift (a*y) a ≤ lift (a*y) s"
using add_le_cancel_left less_TC_imp_not_le plus_eq_lift ‹s ⊏ a› by auto
then have "a ≤ s"
by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
then show False
using ‹s ⊏ a› less_TC_imp_not_le by auto
qed
consider "a * u ⊴ a * y" | "a * y ⊴ a * u"
using t comparable vle_comparable_def by blast
then have "False"
proof cases
case 1
then obtain c where "a*y = a*u + c"
by (metis vle_def)
then have "c+t = r'"
then have "c ⊏ a"
using ‹r' ∈ elts a› less_TC_iff vle2 vle_def by force
moreover have "c ≠ 0"
using ‹a * y = a * u + c› noteq by auto
ultimately show ?thesis
using ‹a * y = a * u + c› mult_eq_imp_0 by blast
next
case 2
then obtain c where "a*u = a*y + c"
by (metis vle_def)
then have "c+r' = t"
then have "c ⊏ a"
by (metis ‹t ∈ elts s› less_TC_iff less_TC_trans ‹s ⊏ a› vle2 vle_def)
moreover have "c ≠ 0"
using ‹a * u = a * y + c› noteq by auto
ultimately show ?thesis
using ‹a * u = a * y + c› mult_eq_imp_0 by blast
qed
then show "u ∈ elts y" ..
qed
qed
next
case (Limit k)
obtain i j where k: "i ∈ elts k" "j ∈ elts k"
and x: "x ∈ elts (Vset i)" and y: "y ∈ elts (Vset j)"
using that Limit by (auto simp: Limit_Vfrom_eq)
show ?case
proof (rule Limit.IH [of "i ⊔ j"])
show "i ⊔ j ∈ elts k"
by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff)
show "x ∈ elts (Vset (i ⊔ j))" "y ∈ elts (Vset (i ⊔ j))"
using x y by (auto simp: Vfrom_sup)
show "a * x + r ≤ a * y + s"
qed (auto simp: Limit.prems)
qed
then show ?thesis
by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt)
qed

theorem mult_cancellation_lemma:
assumes "a*x + r = a*y + s" "r ⊏ a" "s ⊏ a"
shows "x=y ∧ r=s"
by (metis assms leD less_V_def mult_cancellation_half odiff_add_cancel order_refl)

corollary mult_cancellation [simp]:
fixes a::V
assumes "a ≠ 0"
shows "a*x = a*y ⟷ x=y"
by (metis assms nonzero_less_TC mult_cancellation_lemma)

corollary mult_cancellation_less:
assumes lt: "a*x + r < a*y + s" and "r ⊏ a" "s ⊏ a"
obtains "x < y" | "x = y" "r < s"
proof -
have "x ≤ y"
by (meson assms dual_order.strict_implies_order mult_cancellation_half)
then consider "x < y" | "x = y"
using less_V_def by blast
with lt that show ?thesis by blast
qed

corollary lift_mult_TC_disjoint:
fixes x::V
assumes "x ≠ y"
shows "lift (a*x) (TC a) ⊓ lift (a*y) (TC a) = 0"
apply (rule V_equalityI)
using assms
by (auto simp: less_TC_def inf_V_def lift_def image_iff dest: mult_cancellation_lemma)

corollary lift_mult_disjoint:
fixes x::V
assumes "x ≠ y"
shows "lift (a*x) a ⊓ lift (a*y) a = 0"
proof -
have "lift (a*x) a ⊓ lift (a*y) a ≤ lift (a*x) (TC a) ⊓ lift (a*y) (TC a)"
by (metis TC' inf_mono lift_sup_distrib sup_ge1)
then show ?thesis
using assms lift_mult_TC_disjoint by auto
qed

assumes "a*x + r ∈ elts (a*y)" "r ⊏ a"
shows "x ∈ elts y" "r ∈ elts a"
proof -
obtain v s where v: "a * x + r = a * v + s" "v ∈ elts y" "s ∈ elts a"
using assms unfolding mult [of a y] lift_def by auto
then show "x ∈ elts y"
by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma vsubsetD)
show "r ∈ elts a"
by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma v(1) v(3) vsubsetD)
qed

lemma mult_add_mem_0 [simp]: "a*x ∈ elts (a*y) ⟷ x ∈ elts y ∧ 0 ∈ elts a"
proof -
have "x ∈ elts y"
if "a * x ∈ elts (a * y) ∧ 0 ∈ elts a"
using that   using mult_add_mem [of a x 0]
using nonzero_less_TC by force
moreover have "a * x ∈ elts (a * y)"
if "x ∈ elts y" "0 ∈ elts a"
using that  by (force simp: image_iff mult [of a y] lift_def)
ultimately show ?thesis
qed

lemma zero_mem_mult_iff: "0 ∈ elts (x*y) ⟷ 0 ∈ elts x ∧ 0 ∈ elts y"

lemma zero_less_mult_iff [simp]: "0 < x*y ⟷ 0 < x ∧ 0 < y" if "Ord x"
using Kirby.mult_eq_0_iff ZFC_in_HOL.neq0_conv by blast

lemma mult_cancel_less_iff [simp]:
"⟦Ord α; Ord β; Ord γ⟧ ⟹ α*β < α*γ ⟷ β < γ ∧ 0 < α"
using mult_add_mem_0 [of α β γ]
by (meson Ord_0 Ord_mem_iff_lt Ord_mult)

lemma mult_cancel_le_iff [simp]:
"⟦Ord α; Ord β; Ord γ⟧ ⟹ α*β ≤ α*γ ⟷ β ≤ γ ∨ α=0"
by (metis Ord_linear2 Ord_mult eq_iff leD mult_cancel_less_iff mult_cancellation)

lemma mult_Suc_add_less: "⟦α < γ; β < γ; Ord α; Ord β; Ord γ⟧  ⟹ γ * ord_of_nat m + α < γ * ord_of_nat (Suc m) + β"

assumes "m < n" "α < γ" "β < γ" and ord: "Ord α" "Ord β" "Ord γ"
shows "γ * ord_of_nat m + α < γ * ord_of_nat n + β"
proof -
have "Suc m ≤ n"
using ‹m < n› by auto
have "γ * ord_of_nat m + α < γ * ord_of_nat (Suc m) + β"
also have "… ≤ γ * ord_of_nat n + β"
using Ord_mult Ord_ord_of_nat add_right_mono ‹Suc m ≤ n› ord mult_cancel_le_iff ord_of_nat_mono_iff by presburger
finally show ?thesis .
qed

assumes "x < y" "x ∈ elts β" "y ∈ elts β" "μ ∈ elts α" "ν ∈ elts α" "Ord α" "Ord β"
shows "α*x + μ < α*y + ν"
proof -
obtain "Ord x" "Ord y"
using Ord_in_Ord assms by blast
then obtain δ where "0 ∈ elts δ" "y = x + δ"
by (metis add.right_neutral ‹x < y› le_Ord_diff less_V_def mem_0_Ord)
then show ?thesis
by (meson OrdmemD add_le_cancel_left0 ‹μ ∈ elts α› ‹Ord α› less_le_trans zero_imp_le_mult)
qed

assumes "γ ∈ elts α" "ν ∈ elts β" "Ord α" "Ord β"
shows "α * ν + γ ∈ elts (α * β)"
proof -
have "Ord ν"
using Ord_in_Ord assms by blast
with assms show ?thesis
by (metis Ord_mem_iff_lt Ord_succ add_mem_right_cancel mult_cancel_le_iff mult_succ succ_le_iff vsubsetD)
qed

assumes "β ∈ elts γ" "β' ∈ elts γ" "Ord α" "Ord α'" "Ord γ"
shows "γ * α + β ∈ elts (γ * α' + β') ⟷ α ∈ elts α' ∨ α = α' ∧ β ∈ elts β'" (is "?lhs ⟷ ?rhs")
proof
assume L: ?lhs
show ?rhs
proof (cases "α ∈ elts α'")
case False
with assms have "α = α'"
then show ?thesis
using L less_V_def by auto
qed auto
next
assume R: ?rhs
then show ?lhs
proof
assume "α ∈ elts α'"
then obtain δ where "α' = α+δ"
by (metis OrdmemD assms(3) assms(4) le_Ord_diff less_V_def)
show ?lhs
using assms
next
assume "α = α' ∧ β ∈ elts β'"
then show ?lhs
using less_V_def by auto
qed
qed

lemma vcard_mult: "vcard (x * y) = vcard x ⊗ vcard y"
proof -
have 1: "elts (lift (x * u) x) ≈ elts x" if "u ∈ elts y" for u
by (metis cardinal_eqpoll eqpoll_sym eqpoll_trans card_lift)
have 2: "pairwise (λu u'. disjnt (elts (lift (x * u) x)) (elts (lift (x * u') x)))  (elts y)"
by (simp add: pairwise_def disjnt_def) (metis V_disjoint_iff lift_mult_disjoint)
have "x * y = (⨆u∈elts y. lift (x * u) x)"
using mult by blast
then have "elts (x * y) ≈ (⋃u∈elts y. elts (lift (x * u) x))"
by simp
also have "… ≈ elts y × elts x"
using Union_eqpoll_Times [OF 1 2] .
also have "… ≈ elts x × elts y"
also have "… ≈ elts (vcard x) × elts (vcard y)"
using cardinal_eqpoll eqpoll_sym times_eqpoll_cong by blast
also have "… ≈ elts (vcard x ⊗ vcard y)"
by (simp add: cmult_def elts_vcard_VSigma_eqpoll eqpoll_sym)
finally have "elts (x * y) ≈ elts (vcard x ⊗ vcard y)" .
then show ?thesis
qed

proposition TC_mult: "TC(x * y) = (⨆r ∈ elts (TC x). ⨆u ∈ elts (TC y). set{x * u + r})"
proof (cases "x = 0")
case False
have *: "TC(x * y) = (⨆u ∈ elts (TC y). lift (x * u) (TC x))" for y
proof (induction y rule: eps_induct)
case (step y)
have "TC(x * y) = (⨆u ∈ elts y. TC (lift (x * u) x))"
by (simp add: mult [of x y] TC_Sup_distrib image_image)
also have "… = (⨆u ∈ elts y. TC(x * u) ⊔ lift (x * u) (TC x))"
also have "… = (⨆u ∈ elts y. (⨆z ∈ elts (TC u). lift (x * z) (TC x)) ⊔ lift (x * u) (TC x))"
also have "… = (⨆u ∈ elts (TC y). lift (x * u) (TC x))"
by (auto simp: TC' [of y] image_Un Sup_Un_distrib TC_Sup_distrib cSUP_UNION SUP_sup_distrib)
finally show ?case .
qed
show ?thesis
by (force simp: * lift_def)
qed auto

corollary vcard_TC_mult: "vcard (TC(x * y)) = vcard (TC x) ⊗ vcard (TC y)"
proof -
have "(⋃u∈elts (TC x). ⋃v∈elts (TC y). {x * v + u}) = (⋃u∈elts (TC x). (λv. x * v + u) ` elts (TC y))"