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 + (⨆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) lemma Limit_add_Sup_distrib: fixes x::V shows "Limit α ⟹ x + (⨆z∈elts α. f z) = (⨆z∈elts α. 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 ⟷ y≤z" 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 ⊔ (⨆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)" by (simp add: step.IH) 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)" 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 ⊔ (⨆u∈elts y. TC x ⊔ lift x (TC u))" by (simp add: TC_add) 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))" 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) = (⨆z∈elts A. x + z)" by (metis add_Sup_distrib image_ident image_image) lemma add_Limit: "Limit α ⟹ x + α = (⨆z∈elts α. 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 = (⨆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 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 = (⨆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))" by (simp add: lift_lift) also have "… = lift (x * y) (⨆v∈elts 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 = (⨆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)" 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) = (⨆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) apply (simp add: Sup_V_def) done also have "… = (⨆u∈elts y. ⨆r∈elts x. succ (rank (x * u) + rank r))" using rank_add_distrib by auto 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))" by (simp add: add_Sup_distrib False) 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)" 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 "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'" 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 = (⨆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" 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 "(⋃u∈elts (TC x). ⋃v∈elts (TC y). {x * v + u}) = (⋃u∈elts (TC x). (λv. x * v + u) ` elts (TC y))" by (simp add: UNION_singleton_eq_range) also have "… ≈ (⋃x∈elts (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.