Impressum Cardinal_Arithmetic.thy Sprache: Isabelle

(*  Title:      HOL/Cardinals/Cardinal_Arithmetic.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Copyright   2012

Cardinal arithmetic.
*)

section \<open>Cardinal Arithmetic\<close>

theory Cardinal_Arithmetic
  imports Cardinal_Order_Relation
begin

subsection \<open>Binary sum\<close>

lemma csum_Cnotzero2:
  "Cnotzero r2 \ Cnotzero (r1 +c r2)"
  unfolding csum_def
  by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE)

lemma single_cone:
  "|{x}| =o cone"
proof -
  let ?f = "\x. ()"
  have "bij_betw ?f {x} {()}" unfolding bij_betw_def by auto
  thus ?thesis unfolding cone_def using card_of_ordIso by blast
qed

lemma cone_Cnotzero: "Cnotzero cone"
  by (simp add: cone_not_czero Card_order_cone)

lemma cone_ordLeq_ctwo: "cone \o ctwo"
  unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto

lemma csum_czero1: "Card_order r \ r +c czero =o r"
  unfolding czero_def csum_def Field_card_of
  by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty1] card_of_Field_ordIso])

lemma csum_czero2: "Card_order r \ czero +c r =o r"
  unfolding czero_def csum_def Field_card_of
  by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty2] card_of_Field_ordIso])

subsection \<open>Product\<close>

lemma Times_cprod: "|A \ B| =o |A| *c |B|"
  by (simp only: cprod_def Field_card_of card_of_refl)

lemma card_of_Times_singleton:
  fixes A :: "'a set"
  shows "|A \ {x}| =o |A|"
proof -
  define f :: "'a \ 'b \ 'a" where "f = (\(a, b). a)"
  have "A \ f ` (A \ {x})" unfolding f_def by (auto simp: image_iff)
  hence "bij_betw f (A \ {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce
  thus ?thesis using card_of_ordIso by blast
qed

lemma cprod_assoc: "(r *c s) *c t =o r *c s *c t"
  unfolding cprod_def Field_card_of by (rule card_of_Times_assoc)

lemma cprod_czero: "r *c czero =o czero"
  unfolding cprod_def czero_def Field_card_of by (simp add: card_of_empty_ordIso)

lemma cprod_cone: "Card_order r \ r *c cone =o r"
  unfolding cprod_def cone_def Field_card_of
  by (metis (no_types) card_of_Field_ordIso card_of_Times_singleton ordIso_transitive)

lemma ordLeq_cprod1: "\Card_order p1; Cnotzero p2\ \ p1 \o p1 *c p2"
  unfolding cprod_def by (metis Card_order_Times1 czeroI)

subsection \<open>Exponentiation\<close>

lemma cexp_czero: "r ^c czero =o cone"
  unfolding cexp_def czero_def Field_card_of Func_empty by (rule single_cone)

lemma Pow_cexp_ctwo:
  "|Pow A| =o ctwo ^c |A|"
  by (simp add: card_of_Pow_Func cexp_def ctwo_def)

lemma Cnotzero_cexp:
  assumes "Cnotzero q"
  shows "Cnotzero (q ^c r)"
proof -
  have "Field q \ {}"
    by (metis Card_order_iff_ordIso_card_of assms(1) czero_def)
  then show ?thesis
    by (simp add: card_of_ordIso_czero_iff_empty cexp_def)
qed

lemma Cinfinite_ctwo_cexp:
  "Cinfinite r \ Cinfinite (ctwo ^c r)"
  unfolding ctwo_def cexp_def cinfinite_def Field_card_of
  by (rule conjI, rule infinite_Func, auto)

lemma cone_ordLeq_iff_Field:
  assumes "cone \o r"
  shows "Field r \ {}"
  by (metis assms card_of_empty3 card_of_mono2 cone_Cnotzero czeroI)

lemma cone_ordLeq_cexp: "cone \o r1 \ cone \o r1 ^c r2"
  by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field)

lemma Card_order_czero: "Card_order czero"
  by (simp only: card_of_Card_order czero_def)

lemma cexp_mono2'':
  assumes 2: "p2 \o r2"
    and n1: "Cnotzero q"
    and n2: "Card_order p2"
  shows "q ^c p2 \o q ^c r2"
proof (cases "p2 =o (czero :: 'a rel)")
  case True
  hence "q ^c p2 =o q ^c (czero :: 'a rel)" using n1 n2 cexp_cong2 Card_order_czero by blast
  also have "q ^c (czero :: 'a rel) =o cone" using cexp_czero by blast
  also have "cone \o q ^c r2" using cone_ordLeq_cexp cone_ordLeq_Cnotzero n1 by blast
  finally show ?thesis .
next
  case False thus ?thesis using assms cexp_mono2' czeroI by metis
qed

lemma csum_cexp: "\Cinfinite r1; Cinfinite r2; Card_order q; ctwo \o q\ \
  q ^c r1 +c q ^c r2 \<le>o q ^c (r1 +c r2)"
  apply (rule csum_cinfinite_bound)
      apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum1)
     apply (metis cexp_mono2' cinfinite_def finite.emptyI ordLeq_csum2)
  by (simp_all add: Card_order_cexp Cinfinite_csum1 Cinfinite_cexp cinfinite_cexp)

lemma csum_cexp': "\Cinfinite r; Card_order q; ctwo \o q\ \ q +c r \o q ^c r"
  apply (rule csum_cinfinite_bound)
      apply (metis Cinfinite_Cnotzero ordLeq_cexp1)
     apply (metis ordLeq_cexp2)
    apply blast+
  by (metis Cinfinite_cexp)

lemma card_of_Sigma_ordLeq_Cinfinite:
  "\Cinfinite r; |I| \o r; \i \ I. |A i| \o r\ \ |SIGMA i : I. A i| \o r"
  unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)

lemma Cinfinite_ordLess_cexp:
  assumes r: "Cinfinite r"
  shows "r
proof -
  have "r using r by (simp only: ordLess_ctwo_cexp)
  also have "ctwo ^c r \o r ^c r"
    by (rule cexp_mono1[OF ctwo_ordLeq_Cinfinite]) (auto simp: r ctwo_not_czero Card_order_ctwo)
  finally show ?thesis .
qed

lemma infinite_ordLeq_cexp:
  assumes "Cinfinite r"
  shows "r \o r ^c r"
  by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])

lemma czero_cexp: "Cnotzero r \ czero ^c r =o czero"
  by (metis Cnotzero_imp_not_empty cexp_def czero_def card_of_empty_ordIso Field_card_of Func_is_emp)

lemma Func_singleton:
  fixes x :: 'b and A :: "'a set"
  shows "|Func A {x}| =o |{x}|"
proof (rule ordIso_symmetric)
  define f where [abs_def]: "f y a = (if y = x \ a \ A then x else undefined)" for y a
  have "Func A {x} \ f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff)
  hence "bij_betw f {x} (Func A {x})"
    unfolding bij_betw_def inj_on_def f_def Func_def by (auto split: if_split_asm)
  thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast
qed

lemma cone_cexp: "cone ^c r =o cone"
  unfolding cexp_def cone_def Field_card_of by (rule Func_singleton)

lemma card_of_Func_squared:
  fixes A :: "'a set"
  shows "|Func (UNIV :: bool set) A| =o |A \ A|"
proof (rule ordIso_symmetric)
  define f where "f = (\(x::'a,y) b. if A = {} then undefined else if b then x else y)"
  have "Func (UNIV :: bool set) A \ f ` (A \ A)" unfolding f_def Func_def
    by (auto simp: image_iff fun_eq_iff split: option.splits if_split_asm) blast
  hence "bij_betw f (A \ A) (Func (UNIV :: bool set) A)"
    unfolding bij_betw_def inj_on_def f_def Func_def by (auto simp: fun_eq_iff)
  thus "|A \ A| =o |Func (UNIV :: bool set) A|" using card_of_ordIso by blast
qed

lemma cexp_ctwo: "r ^c ctwo =o r *c r"
  unfolding cexp_def ctwo_def cprod_def Field_card_of by (rule card_of_Func_squared)

lemma card_of_Func_Plus:
  fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
  shows "|Func (A <+> B) C| =o |Func A C \ Func B C|"
proof (rule ordIso_symmetric)
  define f where "f = (\(g :: 'a => 'c, h::'b \ 'c) ab. case ab of Inl a \ g a | Inr b \ h b)"
  define f' where "f' = (\<lambda>(f :: ('a + 'b) \<Rightarrow> 'c). (\<lambda>a. f (Inl a), \<lambda>b. f (Inr b)))"
  have "f ` (Func A C \ Func B C) \ Func (A <+> B) C"
    unfolding Func_def f_def by (force split: sum.splits)
  moreover have "f' ` Func (A <+> B) C \ Func A C \ Func B C" unfolding Func_def f'_def by force
  moreover have "\a \ Func A C \ Func B C. f' (f a) = a" unfolding f'_def f_def Func_def by auto
  moreover have "\a' \ Func (A <+> B) C. f (f' a') = a'" unfolding f'_def f_def Func_def
    by (auto split: sum.splits)
  ultimately have "bij_betw f (Func A C \ Func B C) (Func (A <+> B) C)"
    by (intro bij_betw_byWitness[of _ f' f])
  thus "|Func A C \ Func B C| =o |Func (A <+> B) C|" using card_of_ordIso by blast
qed

lemma cexp_csum: "r ^c (s +c t) =o r ^c s *c r ^c t"
  unfolding cexp_def cprod_def csum_def Field_card_of by (rule card_of_Func_Plus)

subsection \<open>Powerset\<close>

definition cpow where "cpow r = |Pow (Field r)|"

lemma card_order_cpow: "card_order r \ card_order (cpow r)"
  by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on)

lemma cpow_greater_eq: "Card_order r \ r \o cpow r"
  by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow)

lemma Cinfinite_cpow: "Cinfinite r \ Cinfinite (cpow r)"
  unfolding cpow_def cinfinite_def by simp

lemma Card_order_cpow: "Card_order (cpow r)"
  unfolding cpow_def by (rule card_of_Card_order)

lemma cardSuc_ordLeq_cpow: "Card_order r \ cardSuc r \o cpow r"
  unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order)

lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
  unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)

subsection \<open>Inverse image\<close>

lemma vimage_ordLeq:
  assumes "|A| \o k" and "\ a \ A. |vimage f {a}| \o k" and "Cinfinite k"
  shows "|vimage f A| \o k"
proof-
  have "vimage f A = (\a \ A. vimage f {a})" by auto
  also have "|\a \ A. vimage f {a}| \o k"
    using UNION_Cinfinite_bound[OF assms] .
  finally show ?thesis .
qed

subsection \<open>Maximum\<close>

definition cmax where
  "cmax r s =
    (if cinfinite r \<or> cinfinite s then czero +c r +c s
     else natLeq_on (max (card (Field r)) (card (Field s))) +c czero)"

lemma cmax_com: "cmax r s =o cmax s r"
  unfolding cmax_def
  by (auto simp: max.commute intro: csum_cong2[OF csum_com] csum_cong2[OF czero_ordIso])

lemma cmax1:
  assumes "Card_order r" "Card_order s" "s \o r"
  shows "cmax r s =o r"
  unfolding cmax_def
proof (split if_splits, intro conjI impI)
  assume "cinfinite r \ cinfinite s"
  hence Cinf: "Cinfinite r" using assms(1,3) by (metis cinfinite_mono)
  have "czero +c r +c s =o r +c s" by (rule csum_czero2[OF Card_order_csum])
  also have "r +c s =o r" by (rule csum_absorb1[OF Cinf assms(3)])
  finally show "czero +c r +c s =o r" .
next
  assume "\ (cinfinite r \ cinfinite s)"
  hence fin: "finite (Field r)" and "finite (Field s)" unfolding cinfinite_def by simp_all
  moreover
  { from assms(2) have "|Field s| =o s" by (rule card_of_Field_ordIso)
    also from assms(3) have "s \o r" .
    also from assms(1) have "r =o |Field r|" by (rule ordIso_symmetric[OF card_of_Field_ordIso])
    finally have "|Field s| \o |Field r|" .
  }
  ultimately have "card (Field s) \ card (Field r)" by (subst sym[OF finite_card_of_iff_card2])
  hence "max (card (Field r)) (card (Field s)) = card (Field r)" by (rule max_absorb1)
  hence "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =
    natLeq_on (card (Field r)) +c czero" by simp
  also have "\ =o natLeq_on (card (Field r))" by (rule csum_czero1[OF natLeq_on_Card_order])
  also have "natLeq_on (card (Field r)) =o |Field r|"
    by (rule ordIso_symmetric[OF finite_imp_card_of_natLeq_on[OF fin]])
  also from assms(1) have "|Field r| =o r" by (rule card_of_Field_ordIso)
  finally show "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =o r" .
qed

lemma cmax2:
  assumes "Card_order r" "Card_order s" "r \o s"
  shows "cmax r s =o s"
  by (metis assms cmax1 cmax_com ordIso_transitive)

context
  fixes r s
  assumes r: "Cinfinite r"
    and     s: "Cinfinite s"
begin

lemma cmax_csum: "cmax r s =o r +c s"
  by (simp add: Card_order_csum cmax_def csum_czero2 r)

lemma cmax_cprod: "cmax r s =o r *c s"
proof (cases "r \o s")
  case True
  hence "cmax r s =o s" by (metis cmax2 r s)
  also have "s =o r *c s" by (metis Cinfinite_Cnotzero True cprod_infinite2' ordIso_symmetric r s)
  finally show ?thesis .
next
  case False
  hence "s \o r" by (metis ordLeq_total r s card_order_on_def)
  hence "cmax r s =o r" by (metis cmax1 r s)
  also have "r =o r *c s" by (metis Cinfinite_Cnotzero \<open>s \<le>o r\<close> cprod_infinite1' ordIso_symmetric r s)
  finally show ?thesis .
qed

end

lemma Card_order_cmax:
  assumes r: "Card_order r" and s: "Card_order s"
  shows "Card_order (cmax r s)"
  unfolding cmax_def by (auto simp: Card_order_csum)

lemma ordLeq_cmax:
  assumes r: "Card_order r" and s: "Card_order s"
  shows "r \o cmax r s \ s \o cmax r s"
  by (meson card_order_on_def cmax1 cmax2 ordIso_iff_ordLeq ordLeq_total ordLeq_transitive r s)

lemmas ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and
  ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2]

lemma finite_cmax:
  assumes r: "Card_order r" and s: "Card_order s"
  shows "finite (Field (cmax r s)) \ finite (Field r) \ finite (Field s)"
  by (meson card_order_on_def cmax1 cmax2 ordIso_finite_Field ordLeq_finite_Field ordLeq_total r s)

end

quality97%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.15Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.