Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Cardinal_Arithmetic.thy Sprache: Isabelle

Original von: 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 (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])

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|"
unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)

lemma Cnotzero_cexp:
  assumes "Cnotzero q" "Card_order r"
  shows "Cnotzero (q ^c r)"
proof (cases "r =o czero")
  case False thus ?thesis
    apply -
    apply (rule Cnotzero_mono)
    apply (rule assms(1))
    apply (rule Card_order_cexp)
    apply (rule ordLeq_cexp1)
    apply (rule conjI)
    apply (rule notI)
    apply (erule notE)
    apply (rule ordIso_transitive)
    apply assumption
    apply (rule czero_ordIso)
    apply (rule assms(2))
    apply (rule conjunct2)
    apply (rule assms(1))
  done
next
  case True thus ?thesis
    apply -
    apply (rule Cnotzero_mono)
    apply (rule cone_Cnotzero)
    apply (rule Card_order_cexp)
    apply (rule ordIso_imp_ordLeq)
    apply (rule ordIso_symmetric)
    apply (rule ordIso_transitive)
    apply (rule cexp_cong2)
    apply assumption
    apply (rule conjunct2)
    apply (rule assms(1))
    apply (rule assms(2))
    apply (rule cexp_czero)
  done
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 \ {}"
proof (rule ccontr)
  assume "\ Field r \ {}"
  hence "Field r = {}" by simp
  thus False using card_of_empty3
    card_of_mono2[OF assms] Cnotzero_imp_not_empty[OF cone_Cnotzero] by auto
qed

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 (rule cexp_mono2)
apply (rule ordLeq_csum1)
apply (erule conjunct2)
apply assumption
apply (rule notE)
apply (rule cinfinite_not_czero[of r1])
apply (erule conjunct1)
apply assumption
apply (erule conjunct2)
apply (rule cexp_mono2)
apply (rule ordLeq_csum2)
apply (erule conjunct2)
apply assumption
apply (rule notE)
apply (rule cinfinite_not_czero[of r2])
apply (erule conjunct1)
apply assumption
apply (erule conjunct2)
apply (rule Card_order_cexp)
apply (rule Card_order_cexp)
apply (rule Cinfinite_cexp)
apply assumption
apply (rule Cinfinite_csum)
by (rule disjI1)

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 card_order_cexp:
  assumes "card_order r1" "card_order r2"
  shows "card_order (r1 ^c r2)"
proof -
  have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto
  thus ?thesis unfolding cexp_def Func_def by simp
qed

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 (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso)

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 (metis Field_card_of card_of_Card_order infinite_Pow)

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)

lemma csum_absorb2: "Cinfinite r2 \ r1 \o r2 \ r1 +c r2 =o r2"
  by (metis csum_absorb2')

lemma cprod_infinite2': "\Cnotzero r1; Cinfinite r2; r1 \o r2\ \ r1 *c r2 =o r2"
  unfolding ordIso_iff_ordLeq
  by (intro conjI cprod_cinfinite_bound ordLeq_cprod2 ordLeq_refl)
    (auto dest!: ordIso_imp_ordLeq not_ordLeq_ordLess simp: czero_def Card_order_empty)

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

lemma cmax_csum: "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 True csum_absorb2 ordIso_symmetric 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 \<open>s \<le>o r\<close> csum_absorb1 ordIso_symmetric r)
  finally show ?thesis .
qed

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"
proof-
  {assume "r \o s"
   hence ?thesis by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
  }
  moreover
  {assume "s \o r"
   hence ?thesis using cmax_com by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
  }
  ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
qed

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)"
proof-
  {assume "r \o s"
   hence ?thesis by (metis cmax2 ordIso_finite_Field ordLeq_finite_Field r s)
  }
  moreover
  {assume "s \o r"
   hence ?thesis by (metis cmax1 ordIso_finite_Field ordLeq_finite_Field r s)
  }
  ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
qed

end

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.