Theory Kirby

section ‹Addition and Multiplication of Sets›

theory Kirby
  imports ZFC_Cardinals

begin

subsection ‹Generalised Addition›

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

subsubsection ‹Addition is a monoid›

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)

lemma add_Sup_distrib:
  fixes x::V shows "y  0  x + (zelts y. f z) = (zelts y. x + f z)"
  by (auto simp: plus_eq_lift SUP_sup_distrib lift_Sup_distrib image_image)

lemma Limit_add_Sup_distrib:
  fixes x::V shows "Limit α  x + (zelts α. f z) = (zelts α. x + f z)"
  using add_Sup_distrib by force

text‹Proposition 3.3(ii)›
instantiation V :: monoid_add
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
        by (simp add: sup_assoc)
    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"
  by (simp add: lift_def)

lemma lift_by0 [simp]: "lift x 0 = 0"
  by (simp add: lift_def)

lemma lift_by1 [simp]: "lift x 1 = set{x}"
  by (simp add: lift_def)

lemma add_eq_0_iff [simp]:
  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"
  by (simp add: plus_V_succ_right one_V_def)

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

lemma omega_closed_add [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)"
    using ord_of_nat_add by auto
  then show ?thesis
    by (simp add: ω_def)
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)

subsubsection ‹Deeper properties of addition›

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)

corollary add_right_cancel [iff]:
  fixes x y z::V shows "x+y = x+z  y=z"
  by (metis lift_eq_lift plus_eq_lift sup_lift_eq_lift)

corollary add_mem_right_cancel [iff]:
  fixes x y z::V shows "x+y  elts (x+z)  y  elts z"
  apply safe
   apply (metis mem_plus_V_E not_add_mem_right add_right_cancel)
  by (metis ZFC_in_HOL.ext dual_order.antisym elts_vinsert insert_subset order_refl plus_vinsert)

corollary add_le_cancel_left [iff]:
  fixes x y z::V shows "x+y  x+z  yz"
  by auto (metis add_mem_right_cancel mem_plus_V_E plus sup_ge1 vsubsetD)

corollary add_less_cancel_left [iff]:
  fixes x y z::V shows "x+y < x+z  y<z"
  by (simp add: less_le_not_le)

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 < ω"
  by (metis add_le_cancel_left add.right_neutral le_0 le_less_trans succ_eq_add1)

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
    by (simp add: inj_on_def lift_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]
  by (simp add: plus_eq_lift vcard_disjoint_sup)

lemma countable_add:
  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"
    unfolding vcard_add
    by (metis Aleph_0 Card_ω InfCard_cdouble_eq InfCard_def cadd_le_mono order_refl)
  then show ?thesis
    by (simp add: countable_iff_le_Aleph0)
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  (uelts 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)"
      by (simp add: step.IH)
    then have : "TC x  (welts 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)"
    by (simp add: sup_aci step.IH)
  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)"
  by (simp add: TC_add TC_sup_lift card_lift vcard_disjoint_sup)

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  (uelts y. TC x  lift x (TC u))"
    by (simp add: TC_add)
  also have " = lift x y  TC x  (uelts 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) = (uelts (x  ZFC_in_HOL.set ((+) x ` elts y)). succ (rank u))"
      by (metis plus rank_Sup)
    also have " = (xelts x. succ (rank x))  (zelts 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  (zelts 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))"
      by (simp add: add_Sup_distrib False)
    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
    by (metis Ord_rank rank_add_distrib rank_of_Ord)
qed

lemma add_Sup_distrib_id: "A  0  x + (elts A) = (zelts A. x + z)"
  by (metis add_Sup_distrib image_ident image_image)

lemma add_Limit: "Limit α  x + α = (zelts α. x + z)"
  by (metis Limit_add_Sup_distrib Limit_eq_Sup_self image_ident image_image)

lemma add_le_left:
  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 μ. β)"
    by (simp add: Limit_eq_Sup_self)
  also have "   (β  elts μ. α + β)"
    using Limit.IH by auto
  also have " = α + (β  elts μ. β)"
    using Limit.hyps Limit_add_Sup_distrib by presburger
  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 "ω  α + ω"
    by (simp add: add_le_left assms)
qed

lemma one_plus_ω_equals_ω [simp]: "1 + ω = ω"
  by (simp add: one_V_def plus_ω_equals_ω)

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"
  by (metis (no_types) add.right_neutral vle_def)

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"
  by (metis add.assoc vle_def)

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"
        using trad_foundation by blast
      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)"
              by (simp add: lift_def)
            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"
  by (metis (full_types) TC_add' add.right_neutral le_TC_def vle_def nonzero_less_TC)

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
      by (metis Ord_add Ord_linear add_le_left mem_not_refl mem_plus_V_E vsubsetD)
  qed
qed

lemma add_le_cancel_left0 [iff]:
  fixes x::V shows "x  x+z"
  by (simp add: vle1 vle_def)

lemma add_less_cancel_left0 [iff]:
  fixes x::V shows "x < x+z  0<z"
  by (metis add_less_cancel_left add.right_neutral)

lemma le_Ord_diff:
  assumes "α  β" "Ord α" "Ord β"
  obtains γ where "α+γ = β" "γ  β" "Ord γ"
proof -
  obtain γ where γ: "α+γ = β" "γ  β"
    by (metis add_le_cancel_left add_le_left assms vle_def vle_iff_le_Ord)
  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 "α+β = β+α"
    by (auto simp: elts_ω add.commute ord_of_nat_add [symmetric])
  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 "α+β = β"
    by (metis add.assoc assms(1) plus_ω_equals_ω)
  then show ?thesis
    by simp
qed

lemma add_right_mono: "α  β; Ord α; Ord β; Ord γ  α+γ  β+γ"
  by (metis add_le_cancel_left add.assoc add_le_left le_Ord_diff)

lemma add_strict_mono: "α < β; γ < δ; Ord α; Ord β; Ord γ; Ord δ  α+γ < β+δ"
  by (metis order.strict_implies_order add_less_cancel_left add_right_mono le_less_trans)

lemma add_right_strict_mono: "α  β; γ < δ; Ord α; Ord β; Ord γ; Ord δ  α+γ < β+δ"
  using add_strict_mono le_imp_less_or_eq by blast

lemma Limit_add_Limit [simp]:
  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
      by (metis Kirby.add_strict_mono Limit_def Ord_add Ord_in_Ord Ord_mem_iff_lt assms one_V_def succ_eq_add1)
  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
    by (simp add: odiff_def vle_def)
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 
    by (simp add: odiff_def vle_def)
qed


lemma odiff_0_right [simp]: "odiff x 0 = x"
  by (metis add.left_neutral vle_def vle_imp_odiff_eq)

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"
  by (simp add: odiff_le_iff vle_iff_le_Ord)

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
    by (simp add: not_vle_imp_odiff_0)
qed

lemma Ord_odiff_le_odiff: "x  y; Ord x; Ord y  odiff x α  odiff y α"
  by (simp add: odiff_le_odiff vle_iff_le_Ord)

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"
  by (simp add: odiff_eq_iff vle_def)

lemma odiff_add_cancel_0 [simp]: "odiff x x = 0"
  by (simp add: odiff_eq_iff)

lemma odiff_add_cancel_both [simp]: "odiff (x + y) (x + z) = odiff y z"
  by (simp add: add.assoc odiff_def vle_def)


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 = (uelts 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
    by (simp add: add.commute [of m]) (simp add: ord_of_nat_add mult_succ)
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)"
    by (simp add: ord_of_nat_mult)
  then show ?thesis
    by (simp add: ω_def)
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]
  by (simp add: Sup_Un_distrib image_Un)

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"
  by (simp add: mult_sup_distrib plus_eq_lift)

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 = (uelts (lift y z). lift (x * u) x)"
    using mult by blast
  also have " = (velts z. lift (x * (y + v)) x)"
    using lift_def by auto
  also have " = (velts z. lift (x * y + x * v) x)"
    using mult_lift_imp_distrib step.IH by auto
  also have " = (velts z. lift (x * y) (lift (x * v) x))"
    by (simp add: lift_lift)
  also have " = lift (x * y) (velts z. lift (x * v) x)"
    by (simp add: image_image lift_Sup_distrib)
  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
  by (simp add: mult_lift mult_lift_imp_distrib)

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 = (uelts z. lift (x * y * u) (x * y))"
      using mult by blast
    also have " = (uelts z. lift (x * (y * u)) (x * y))"
      using step.IH by auto
    also have " = (uelts z. x * lift (y * u) y)"
      using mult_lift by auto
    also have " = x * (uelts z. lift (y * u) y)"
      by (simp add: image_image mult_Sup_distrib)
    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
    by (simp add: Limit.hyps mult_Limit)
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
    by (simp add: mult_succ)
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) = (yelts (uelts y. lift (x * u) x). succ (rank y))"
    by (metis rank_Sup mult)
  also have " = (uelts y. relts x. succ (rank (x * u + r)))"
    apply (simp add: lift_def image_image image_UN)
    apply (simp add: Sup_V_def)
    done
  also have " = (uelts y. relts x. succ (rank (x * u) + rank r))"
    using rank_add_distrib by auto
  also have " = (uelts y. relts x. succ (rank x * rank u + rank r))"
    using step arg_cong [where f = Sup] by auto
  also have " = (uelts y. rank x * rank u + rank x)"
  proof (rule SUP_cong)
    show "(relts 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 "(relts x. succ (rank x * rank u + rank r)) = rank x * rank u + (yelts x. succ (rank y))"
      proof (rule order_antisym)
        show "(relts x. succ (rank x * rank u + rank r))  rank x * rank u + (yelts x. succ (rank y))"
          by (auto simp: Sup_le_iff simp flip: plus_V_succ_right)
        have "rank x * rank u + (yelts x. succ (rank y)) = (yelts x. rank x * rank u + succ (rank y))"
          by (simp add: add_Sup_distrib False)
        also have "  (relts x. succ (rank x * rank u + rank r))"
          using plus_V_succ_right by auto
        finally show "rank x * rank u + (yelts x. succ (rank y))  (relts 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)"
        by (simp add: lift_def r)
      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"
        by (metis TC_add' V_equalityI add.right_neutral eps_induct le_TC_refl less_TC_iff less_imp_le_TC)
      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
    apply (simp add: mult_Limit elts_ω)
    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 "a0" "x0"
    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'"
            by (simp add: eq plus_eq_lift)
          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"
            by (metis add.right_neutral noteq vle_def)
          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
            ―‹contradicts minimality of @{term x'}
            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"
            by (metis add.right_neutral noteq vle_def)
          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'"
                by (simp add: eq plus_eq_lift)
              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"
              by (metis add.right_neutral noteq vle_def)
            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"
              by (metis add.right_neutral noteq vle_def)
            moreover have "e + d = c"
              by (metis add_right_cancel add.assoc d e)
            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)"
        by (simp add: plus_eq_lift)
      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'"
            by (metis add_right_cancel add.assoc t)
          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"
            by (metis add_right_cancel add.assoc 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"
        by (simp add: Limit.prems)
    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

lemma mult_add_mem:
  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
    by (metis mult_eq_0_iff add.right_neutral mult_add_mem(2) nonzero_less_TC)
qed

lemma zero_mem_mult_iff: "0  elts (x*y)  0  elts x  0  elts y" 
  by (metis Kirby.mult_zero_right mult_add_mem_0)

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) + β"
  apply (simp add: mult_succ add.assoc)
  by (meson Ord_add Ord_linear2 le_less_trans not_add_less_right)

lemma mult_nat_less_add_less:
  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) + β"
    using assms mult_Suc_add_less by blast
  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

lemma add_mult_less_add_mult:
  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
    apply (simp add: add_mult_distrib add.assoc)
    by (meson OrdmemD add_le_cancel_left0 μ  elts α Ord α less_le_trans zero_imp_le_mult)
qed

lemma add_mult_less:
  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

lemma Ord_add_mult_iff:
  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 "α = α'"
      by (meson L Ord_linear Ord_mult Ord_trans add_mult_less not_add_mem_right)
    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
      by (meson α  elts α' add_le_cancel_left0 add_mult_less vsubsetD)
  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 = (uelts y. lift (x * u) x)"
    using mult by blast
  then have "elts (x * y)  (uelts 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"
    by (simp add: times_commute_eqpoll)
  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
    by (metis cadd_cmult_distrib cadd_def cardinal_cong cardinal_idem vsum_0_eqpoll)
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))"
      by (simp add: TC_lift False)
    also have " = (u  elts y. (z  elts (TC u). lift (x * z) (TC x))  lift (x * u) (TC x))"
      by (simp add: step)
    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 "(uelts (TC x). velts (TC y). {x * v + u}) = (uelts (TC x). (λv. x * v + u) ` elts (TC y))"
    by (simp add: UNION_singleton_eq_range)
  also have "  (xelts (TC x). elts (lift (TC y * x) (TC y)))"
  proof (rule UN_eqpoll_UN)
    show "(λv. x * v + u) ` elts (TC y)  elts (lift (TC y * u) (TC y))"
      if "u  elts (TC x)" for u
    proof -
      have "inj_on (λv.