Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: BNF_Wellorder_Embedding.thy Sprache: Isabelle

Original von: Isabelle^©

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

Cardinal arithmetic as needed by bounded natural functors.
*)

section \<open>Cardinal Arithmetic as Needed by Bounded Natural Functors\<close>

theory BNF_Cardinal_Arithmetic
imports BNF_Cardinal_Order_Relation
begin

lemma dir_image: "\\x y. (f x = f y) = (x = y); Card_order r\ \ r =o dir_image r f"
by (rule dir_image_ordIso) (auto simp add: inj_on_def card_order_on_def)

lemma card_order_dir_image:
  assumes bij: "bij f" and co: "card_order r"
  shows "card_order (dir_image r f)"
proof -
  from assms have "Field (dir_image r f) = UNIV"
    using card_order_on_Card_order[of UNIV r] unfolding bij_def dir_image_Field by auto
  moreover from bij have "\x y. (f x = f y) = (x = y)" unfolding bij_def inj_on_def by auto
  with co have "Card_order (dir_image r f)"
    using card_order_on_Card_order[of UNIV r] Card_order_ordIso2[OF _ dir_image] by blast
  ultimately show ?thesis by auto
qed

lemma ordIso_refl: "Card_order r \ r =o r"
by (rule card_order_on_ordIso)

lemma ordLeq_refl: "Card_order r \ r \o r"
by (rule ordIso_imp_ordLeq, rule card_order_on_ordIso)

lemma card_of_ordIso_subst: "A = B \ |A| =o |B|"
by (simp only: ordIso_refl card_of_Card_order)

lemma Field_card_order: "card_order r \ Field r = UNIV"
using card_order_on_Card_order[of UNIV r] by simp

subsection \<open>Zero\<close>

definition czero where
  "czero = card_of {}"

lemma czero_ordIso:
  "czero =o czero"
using card_of_empty_ordIso by (simp add: czero_def)

lemma card_of_ordIso_czero_iff_empty:
  "|A| =o (czero :: 'b rel) \ A = ({} :: 'a set)"
unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl card_of_empty_ordIso)

(* A "not czero" Cardinal predicate *)
abbreviation Cnotzero where
  "Cnotzero (r :: 'a rel) \ \(r =o (czero :: 'a rel)) \ Card_order r"

(*helper*)
lemma Cnotzero_imp_not_empty: "Cnotzero r \ Field r \ {}"
  unfolding Card_order_iff_ordIso_card_of czero_def by force

lemma czeroI:
  "\Card_order r; Field r = {}\ \ r =o czero"
using Cnotzero_imp_not_empty ordIso_transitive[OF _ czero_ordIso] by blast

lemma czeroE:
  "r =o czero \ Field r = {}"
unfolding czero_def
by (drule card_of_cong) (simp only: Field_card_of card_of_empty2)

lemma Cnotzero_mono:
  "\Cnotzero r; Card_order q; r \o q\ \ Cnotzero q"
apply (rule ccontr)
apply auto
apply (drule czeroE)
apply (erule notE)
apply (erule czeroI)
apply (drule card_of_mono2)
apply (simp only: card_of_empty3)
done

subsection \<open>(In)finite cardinals\<close>

definition cinfinite where
  "cinfinite r = (\ finite (Field r))"

abbreviation Cinfinite where
  "Cinfinite r \ cinfinite r \ Card_order r"

definition cfinite where
  "cfinite r = finite (Field r)"

abbreviation Cfinite where
  "Cfinite r \ cfinite r \ Card_order r"

lemma Cfinite_ordLess_Cinfinite: "\Cfinite r; Cinfinite s\ \ r
  unfolding cfinite_def cinfinite_def
  by (blast intro: finite_ordLess_infinite card_order_on_well_order_on)

lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]

lemma natLeq_cinfinite: "cinfinite natLeq"
unfolding cinfinite_def Field_natLeq by (rule infinite_UNIV_nat)

lemma natLeq_ordLeq_cinfinite:
  assumes inf: "Cinfinite r"
  shows "natLeq \o r"
proof -
  from inf have "natLeq \o |Field r|" unfolding cinfinite_def
    using infinite_iff_natLeq_ordLeq by blast
  also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
  finally show ?thesis .
qed

lemma cinfinite_not_czero: "cinfinite r \ \ (r =o (czero :: 'a rel))"
unfolding cinfinite_def by (cases "Field r = {}") (auto dest: czeroE)

lemma Cinfinite_Cnotzero: "Cinfinite r \ Cnotzero r"
by (rule conjI[OF cinfinite_not_czero]) simp_all

lemma Cinfinite_cong: "\r1 =o r2; Cinfinite r1\ \ Cinfinite r2"
using Card_order_ordIso2[of r1 r2] unfolding cinfinite_def ordIso_iff_ordLeq
by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])

lemma cinfinite_mono: "\r1 \o r2; cinfinite r1\ \ cinfinite r2"
unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])

subsection \<open>Binary sum\<close>

definition csum (infixr "+c" 65) where
  "r1 +c r2 \ |Field r1 <+> Field r2|"

lemma Field_csum: "Field (r +c s) = Inl ` Field r \ Inr ` Field s"
  unfolding csum_def Field_card_of by auto

lemma Card_order_csum:
  "Card_order (r1 +c r2)"
unfolding csum_def by (simp add: card_of_Card_order)

lemma csum_Cnotzero1:
  "Cnotzero r1 \ Cnotzero (r1 +c r2)"
unfolding csum_def using Cnotzero_imp_not_empty[of r1] Plus_eq_empty_conv[of "Field r1" "Field r2"]
   card_of_ordIso_czero_iff_empty[of "Field r1 <+> Field r2"] by (auto intro: card_of_Card_order)

lemma card_order_csum:
  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 csum_def by (auto simp: card_of_card_order_on)
qed

lemma cinfinite_csum:
  "cinfinite r1 \ cinfinite r2 \ cinfinite (r1 +c r2)"
unfolding cinfinite_def csum_def by (auto simp: Field_card_of)

lemma Cinfinite_csum1:
  "Cinfinite r1 \ Cinfinite (r1 +c r2)"
unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)

lemma Cinfinite_csum:
  "Cinfinite r1 \ Cinfinite r2 \ Cinfinite (r1 +c r2)"
unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)

lemma Cinfinite_csum_weak:
  "\Cinfinite r1; Cinfinite r2\ \ Cinfinite (r1 +c r2)"
by (erule Cinfinite_csum1)

lemma csum_cong: "\p1 =o r1; p2 =o r2\ \ p1 +c p2 =o r1 +c r2"
by (simp only: csum_def ordIso_Plus_cong)

lemma csum_cong1: "p1 =o r1 \ p1 +c q =o r1 +c q"
by (simp only: csum_def ordIso_Plus_cong1)

lemma csum_cong2: "p2 =o r2 \ q +c p2 =o q +c r2"
by (simp only: csum_def ordIso_Plus_cong2)

lemma csum_mono: "\p1 \o r1; p2 \o r2\ \ p1 +c p2 \o r1 +c r2"
by (simp only: csum_def ordLeq_Plus_mono)

lemma csum_mono1: "p1 \o r1 \ p1 +c q \o r1 +c q"
by (simp only: csum_def ordLeq_Plus_mono1)

lemma csum_mono2: "p2 \o r2 \ q +c p2 \o q +c r2"
by (simp only: csum_def ordLeq_Plus_mono2)

lemma ordLeq_csum1: "Card_order p1 \ p1 \o p1 +c p2"
by (simp only: csum_def Card_order_Plus1)

lemma ordLeq_csum2: "Card_order p2 \ p2 \o p1 +c p2"
by (simp only: csum_def Card_order_Plus2)

lemma csum_com: "p1 +c p2 =o p2 +c p1"
by (simp only: csum_def card_of_Plus_commute)

lemma csum_assoc: "(p1 +c p2) +c p3 =o p1 +c p2 +c p3"
by (simp only: csum_def Field_card_of card_of_Plus_assoc)

lemma Cfinite_csum: "\Cfinite r; Cfinite s\ \ Cfinite (r +c s)"
  unfolding cfinite_def csum_def Field_card_of using card_of_card_order_on by simp

lemma csum_csum: "(r1 +c r2) +c (r3 +c r4) =o (r1 +c r3) +c (r2 +c r4)"
proof -
  have "(r1 +c r2) +c (r3 +c r4) =o r1 +c r2 +c (r3 +c r4)"
    by (rule csum_assoc)
  also have "r1 +c r2 +c (r3 +c r4) =o r1 +c (r2 +c r3) +c r4"
    by (intro csum_assoc csum_cong2 ordIso_symmetric)
  also have "r1 +c (r2 +c r3) +c r4 =o r1 +c (r3 +c r2) +c r4"
    by (intro csum_com csum_cong1 csum_cong2)
  also have "r1 +c (r3 +c r2) +c r4 =o r1 +c r3 +c r2 +c r4"
    by (intro csum_assoc csum_cong2 ordIso_symmetric)
  also have "r1 +c r3 +c r2 +c r4 =o (r1 +c r3) +c (r2 +c r4)"
    by (intro csum_assoc ordIso_symmetric)
  finally show ?thesis .
qed

lemma Plus_csum: "|A <+> B| =o |A| +c |B|"
by (simp only: csum_def Field_card_of card_of_refl)

lemma Un_csum: "|A \ B| \o |A| +c |B|"
using ordLeq_ordIso_trans[OF card_of_Un_Plus_ordLeq Plus_csum] by blast

subsection \<open>One\<close>

definition cone where
  "cone = card_of {()}"

lemma Card_order_cone: "Card_order cone"
unfolding cone_def by (rule card_of_Card_order)

lemma Cfinite_cone: "Cfinite cone"
  unfolding cfinite_def by (simp add: Card_order_cone)

lemma cone_not_czero: "\ (cone =o czero)"
unfolding czero_def cone_def ordIso_iff_ordLeq using card_of_empty3 empty_not_insert by blast

lemma cone_ordLeq_Cnotzero: "Cnotzero r \ cone \o r"
unfolding cone_def by (rule Card_order_singl_ordLeq) (auto intro: czeroI)

subsection \<open>Two\<close>

definition ctwo where
  "ctwo = |UNIV :: bool set|"

lemma Card_order_ctwo: "Card_order ctwo"
unfolding ctwo_def by (rule card_of_Card_order)

lemma ctwo_not_czero: "\ (ctwo =o czero)"
using card_of_empty3[of "UNIV :: bool set"] ordIso_iff_ordLeq
unfolding czero_def ctwo_def using UNIV_not_empty by auto

lemma ctwo_Cnotzero: "Cnotzero ctwo"
by (simp add: ctwo_not_czero Card_order_ctwo)

subsection \<open>Family sum\<close>

definition Csum where
  "Csum r rs \ |SIGMA i : Field r. Field (rs i)|"

(* Similar setup to the one for SIGMA from theory Big_Operators: *)
syntax "_Csum" ::
  "pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set"
  ("(3CSUM _:_. _)" [0, 51, 10] 10)

translations
  "CSUM i:r. rs" == "CONST Csum r (%i. rs)"

lemma SIGMA_CSUM: "|SIGMA i : I. As i| = (CSUM i : |I|. |As i| )"
by (auto simp: Csum_def Field_card_of)

(* NB: Always, under the cardinal operator,
operations on sets are reduced automatically to operations on cardinals.
This should make cardinal reasoning more direct and natural.  *)

subsection \<open>Product\<close>

definition cprod (infixr "*c" 80) where
  "r1 *c r2 = |Field r1 \ Field r2|"

lemma card_order_cprod:
  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 by (auto simp: cprod_def card_of_card_order_on)
qed

lemma Card_order_cprod: "Card_order (r1 *c r2)"
by (simp only: cprod_def Field_card_of card_of_card_order_on)

lemma cprod_mono1: "p1 \o r1 \ p1 *c q \o r1 *c q"
by (simp only: cprod_def ordLeq_Times_mono1)

lemma cprod_mono2: "p2 \o r2 \ q *c p2 \o q *c r2"
by (simp only: cprod_def ordLeq_Times_mono2)

lemma cprod_mono: "\p1 \o r1; p2 \o r2\ \ p1 *c p2 \o r1 *c r2"
by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])

lemma ordLeq_cprod2: "\Cnotzero p1; Card_order p2\ \ p2 \o p1 *c p2"
unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)

lemma cinfinite_cprod: "\cinfinite r1; cinfinite r2\ \ cinfinite (r1 *c r2)"
by (simp add: cinfinite_def cprod_def Field_card_of infinite_cartesian_product)

lemma cinfinite_cprod2: "\Cnotzero r1; Cinfinite r2\ \ cinfinite (r1 *c r2)"
by (rule cinfinite_mono) (auto intro: ordLeq_cprod2)

lemma Cinfinite_cprod2: "\Cnotzero r1; Cinfinite r2\ \ Cinfinite (r1 *c r2)"
by (blast intro: cinfinite_cprod2 Card_order_cprod)

lemma cprod_cong: "\p1 =o r1; p2 =o r2\ \ p1 *c p2 =o r1 *c r2"
unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono)

lemma cprod_cong1: "\p1 =o r1\ \ p1 *c p2 =o r1 *c p2"
unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1)

lemma cprod_cong2: "p2 =o r2 \ q *c p2 =o q *c r2"
unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono2)

lemma cprod_com: "p1 *c p2 =o p2 *c p1"
by (simp only: cprod_def card_of_Times_commute)

lemma card_of_Csum_Times:
  "\i \ I. |A i| \o |B| \ (CSUM i : |I|. |A i| ) \o |I| *c |B|"
by (simp only: Csum_def cprod_def Field_card_of card_of_Sigma_mono1)

lemma card_of_Csum_Times':
  assumes "Card_order r" "\i \ I. |A i| \o r"
  shows "(CSUM i : |I|. |A i| ) \o |I| *c r"
proof -
  from assms(1) have *: "r =o |Field r|" by (simp add: card_of_unique)
  with assms(2) have "\i \ I. |A i| \o |Field r|" by (blast intro: ordLeq_ordIso_trans)
  hence "(CSUM i : |I|. |A i| ) \o |I| *c |Field r|" by (simp only: card_of_Csum_Times)
  also from * have "|I| *c |Field r| \o |I| *c r"
    by (simp only: Field_card_of card_of_refl cprod_def ordIso_imp_ordLeq)
  finally show ?thesis .
qed

lemma cprod_csum_distrib1: "r1 *c r2 +c r1 *c r3 =o r1 *c (r2 +c r3)"
unfolding csum_def cprod_def by (simp add: Field_card_of card_of_Times_Plus_distrib ordIso_symmetric)

lemma csum_absorb2': "\Card_order r2; r1 \o r2; cinfinite r1 \ cinfinite r2\ \ r1 +c r2 =o r2"
unfolding csum_def by (rule conjunct2[OF Card_order_Plus_infinite])
  (auto simp: cinfinite_def dest: cinfinite_mono)

lemma csum_absorb1':
  assumes card: "Card_order r2"
  and r12: "r1 \o r2" and cr12: "cinfinite r1 \ cinfinite r2"
  shows "r2 +c r1 =o r2"
by (rule ordIso_transitive, rule csum_com, rule csum_absorb2', (simp only: assms)+)

lemma csum_absorb1: "\Cinfinite r2; r1 \o r2\ \ r2 +c r1 =o r2"
by (rule csum_absorb1') auto

subsection \<open>Exponentiation\<close>

definition cexp (infixr "^c" 90) where
  "r1 ^c r2 \ |Func (Field r2) (Field r1)|"

lemma Card_order_cexp: "Card_order (r1 ^c r2)"
unfolding cexp_def by (rule card_of_Card_order)

lemma cexp_mono':
  assumes 1: "p1 \o r1" and 2: "p2 \o r2"
  and n: "Field p2 = {} \ Field r2 = {}"
  shows "p1 ^c p2 \o r1 ^c r2"
proof(cases "Field p1 = {}")
  case True
  hence "Field p2 \ {} \ Func (Field p2) {} = {}" unfolding Func_is_emp by simp
  with True have "|Field |Func (Field p2) (Field p1)|| \o cone"
    unfolding cone_def Field_card_of
    by (cases "Field p2 = {}", auto intro: surj_imp_ordLeq simp: Func_empty)
  hence "|Func (Field p2) (Field p1)| \o cone" by (simp add: Field_card_of cexp_def)
  hence "p1 ^c p2 \o cone" unfolding cexp_def .
  thus ?thesis
  proof (cases "Field p2 = {}")
    case True
    with n have "Field r2 = {}" .
    hence "cone \o r1 ^c r2" unfolding cone_def cexp_def Func_def
      by (auto intro: card_of_ordLeqI[where f="\_ _. undefined"])
    thus ?thesis using \<open>p1 ^c p2 \<le>o cone\<close> ordLeq_transitive by auto
  next
    case False with True have "|Field (p1 ^c p2)| =o czero"
      unfolding card_of_ordIso_czero_iff_empty cexp_def Field_card_of Func_def by auto
    thus ?thesis unfolding cexp_def card_of_ordIso_czero_iff_empty Field_card_of
      by (simp add: card_of_empty)
  qed
next
  case False
  have 1: "|Field p1| \o |Field r1|" and 2: "|Field p2| \o |Field r2|"
    using 1 2 by (auto simp: card_of_mono2)
  obtain f1 where f1: "f1 ` Field r1 = Field p1"
    using 1 unfolding card_of_ordLeq2[OF False, symmetric] by auto
  obtain f2 where f2: "inj_on f2 (Field p2)" "f2 ` Field p2 \ Field r2"
    using 2 unfolding card_of_ordLeq[symmetric] by blast
  have 0: "Func_map (Field p2) f1 f2 ` (Field (r1 ^c r2)) = Field (p1 ^c p2)"
    unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n, symmetric] .
  have 00: "Field (p1 ^c p2) \ {}" unfolding cexp_def Field_card_of Func_is_emp
    using False by simp
  show ?thesis
    using 0 card_of_ordLeq2[OF 00] unfolding cexp_def Field_card_of by blast
qed

lemma cexp_mono:
  assumes 1: "p1 \o r1" and 2: "p2 \o r2"
  and n: "p2 =o czero \ r2 =o czero" and card: "Card_order p2"
  shows "p1 ^c p2 \o r1 ^c r2"
  by (rule cexp_mono'[OF 1 2 czeroE[OF n[OF czeroI[OF card]]]])

lemma cexp_mono1:
  assumes 1: "p1 \o r1" and q: "Card_order q"
  shows "p1 ^c q \o r1 ^c q"
using ordLeq_refl[OF q] by (rule cexp_mono[OF 1]) (auto simp: q)

lemma cexp_mono2':
  assumes 2: "p2 \o r2" and q: "Card_order q"
  and n: "Field p2 = {} \ Field r2 = {}"
  shows "q ^c p2 \o q ^c r2"
using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n]) auto

lemma cexp_mono2:
  assumes 2: "p2 \o r2" and q: "Card_order q"
  and n: "p2 =o czero \ r2 =o czero" and card: "Card_order p2"
  shows "q ^c p2 \o q ^c r2"
using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n card]) auto

lemma cexp_mono2_Cnotzero:
  assumes "p2 \o r2" "Card_order q" "Cnotzero p2"
  shows "q ^c p2 \o q ^c r2"
using assms(3) czeroI by (blast intro: cexp_mono2'[OF assms(1,2)])

lemma cexp_cong:
  assumes 1: "p1 =o r1" and 2: "p2 =o r2"
  and Cr: "Card_order r2"
  and Cp: "Card_order p2"
  shows "p1 ^c p2 =o r1 ^c r2"
proof -
  obtain f where "bij_betw f (Field p2) (Field r2)"
    using 2 card_of_ordIso[of "Field p2" "Field r2"] card_of_cong by auto
  hence 0: "Field p2 = {} \ Field r2 = {}" unfolding bij_betw_def by auto
  have r: "p2 =o czero \ r2 =o czero"
    and p: "r2 =o czero \ p2 =o czero"
     using 0 Cr Cp czeroE czeroI by auto
  show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq
    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast
qed

lemma cexp_cong1:
  assumes 1: "p1 =o r1" and q: "Card_order q"
  shows "p1 ^c q =o r1 ^c q"
by (rule cexp_cong[OF 1 _ q q]) (rule ordIso_refl[OF q])

lemma cexp_cong2:
  assumes 2: "p2 =o r2" and q: "Card_order q" and p: "Card_order p2"
  shows "q ^c p2 =o q ^c r2"
by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl Card_order_ordIso2[OF p 2] q p)

lemma cexp_cone:
  assumes "Card_order r"
  shows "r ^c cone =o r"
proof -
  have "r ^c cone =o |Field r|"
    unfolding cexp_def cone_def Field_card_of Func_empty
      card_of_ordIso[symmetric] bij_betw_def Func_def inj_on_def image_def
    by (rule exI[of _ "\f. f ()"]) auto
  also have "|Field r| =o r" by (rule card_of_Field_ordIso[OF assms])
  finally show ?thesis .
qed

lemma cexp_cprod:
  assumes r1: "Card_order r1"
  shows "(r1 ^c r2) ^c r3 =o r1 ^c (r2 *c r3)" (is "?L =o ?R")
proof -
  have "?L =o r1 ^c (r3 *c r2)"
    unfolding cprod_def cexp_def Field_card_of
    using card_of_Func_Times by(rule ordIso_symmetric)
  also have "r1 ^c (r3 *c r2) =o ?R"
    apply(rule cexp_cong2) using cprod_com r1 by (auto simp: Card_order_cprod)
  finally show ?thesis .
qed

lemma cprod_infinite1': "\Cinfinite r; Cnotzero p; p \o r\ \ r *c p =o r"
unfolding cinfinite_def cprod_def
by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+

lemma cprod_infinite: "Cinfinite r \ r *c r =o r"
using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast

lemma cexp_cprod_ordLeq:
  assumes r1: "Card_order r1" and r2: "Cinfinite r2"
  and r3: "Cnotzero r3" "r3 \o r2"
  shows "(r1 ^c r2) ^c r3 =o r1 ^c r2" (is "?L =o ?R")
proof-
  have "?L =o r1 ^c (r2 *c r3)" using cexp_cprod[OF r1] .
  also have "r1 ^c (r2 *c r3) =o ?R"
  apply(rule cexp_cong2)
  apply(rule cprod_infinite1'[OF r2 r3]) using r1 r2 by (fastforce simp: Card_order_cprod)+
  finally show ?thesis .
qed

lemma Cnotzero_UNIV: "Cnotzero |UNIV|"
by (auto simp: card_of_Card_order card_of_ordIso_czero_iff_empty)

lemma ordLess_ctwo_cexp:
  assumes "Card_order r"
  shows "r
proof -
  have "r using assms by (rule Card_order_Pow)
  also have "|Pow (Field r)| =o ctwo ^c r"
    unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
  finally show ?thesis .
qed

lemma ordLeq_cexp1:
  assumes "Cnotzero r" "Card_order q"
  shows "q \o q ^c r"
proof (cases "q =o (czero :: 'a rel)")
  case True thus ?thesis by (simp only: card_of_empty cexp_def czero_def ordIso_ordLeq_trans)
next
  case False
  thus ?thesis
    apply -
    apply (rule ordIso_ordLeq_trans)
    apply (rule ordIso_symmetric)
    apply (rule cexp_cone)
    apply (rule assms(2))
    apply (rule cexp_mono2)
    apply (rule cone_ordLeq_Cnotzero)
    apply (rule assms(1))
    apply (rule assms(2))
    apply (rule notE)
    apply (rule cone_not_czero)
    apply assumption
    apply (rule Card_order_cone)
  done
qed

lemma ordLeq_cexp2:
  assumes "ctwo \o q" "Card_order r"
  shows "r \o q ^c r"
proof (cases "r =o (czero :: 'a rel)")
  case True thus ?thesis by (simp only: card_of_empty cexp_def czero_def ordIso_ordLeq_trans)
next
  case False thus ?thesis
    apply -
    apply (rule ordLess_imp_ordLeq)
    apply (rule ordLess_ordLeq_trans)
    apply (rule ordLess_ctwo_cexp)
    apply (rule assms(2))
    apply (rule cexp_mono1)
    apply (rule assms(1))
    apply (rule assms(2))
  done
qed

lemma cinfinite_cexp: "\ctwo \o q; Cinfinite r\ \ cinfinite (q ^c r)"
by (rule cinfinite_mono[OF ordLeq_cexp2]) simp_all

lemma Cinfinite_cexp:
  "\ctwo \o q; Cinfinite r\ \ Cinfinite (q ^c r)"
by (simp add: cinfinite_cexp Card_order_cexp)

lemma ctwo_ordLess_natLeq: "ctwo
unfolding ctwo_def using finite_UNIV natLeq_cinfinite natLeq_Card_order
by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)

lemma ctwo_ordLess_Cinfinite: "Cinfinite r \ ctwo
by (rule ordLess_ordLeq_trans[OF ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite])

lemma ctwo_ordLeq_Cinfinite:
  assumes "Cinfinite r"
  shows "ctwo \o r"
by (rule ordLess_imp_ordLeq[OF ctwo_ordLess_Cinfinite[OF assms]])

lemma Un_Cinfinite_bound: "\|A| \o r; |B| \o r; Cinfinite r\ \ |A \ B| \o r"
by (auto simp add: cinfinite_def card_of_Un_ordLeq_infinite_Field)

lemma UNION_Cinfinite_bound: "\|I| \o r; \i \ I. |A i| \o r; Cinfinite r\ \ |\i \ I. A i| \o r"
by (auto simp add: card_of_UNION_ordLeq_infinite_Field cinfinite_def)

lemma csum_cinfinite_bound:
  assumes "p \o r" "q \o r" "Card_order p" "Card_order q" "Cinfinite r"
  shows "p +c q \o r"
proof -
  from assms(1-4) have "|Field p| \o r" "|Field q| \o r"
    unfolding card_order_on_def using card_of_least ordLeq_transitive by blast+
  with assms show ?thesis unfolding cinfinite_def csum_def
    by (blast intro: card_of_Plus_ordLeq_infinite_Field)
qed

lemma cprod_cinfinite_bound:
  assumes "p \o r" "q \o r" "Card_order p" "Card_order q" "Cinfinite r"
  shows "p *c q \o r"
proof -
  from assms(1-4) have "|Field p| \o r" "|Field q| \o r"
    unfolding card_order_on_def using card_of_least ordLeq_transitive by blast+
  with assms show ?thesis unfolding cinfinite_def cprod_def
    by (blast intro: card_of_Times_ordLeq_infinite_Field)
qed

lemma cprod_csum_cexp:
  "r1 *c r2 \o (r1 +c r2) ^c ctwo"
unfolding cprod_def csum_def cexp_def ctwo_def Field_card_of
proof -
  let ?f = "\(a, b). %x. if x then Inl a else Inr b"
  have "inj_on ?f (Field r1 \ Field r2)" (is "inj_on _ ?LHS")
    by (auto simp: inj_on_def fun_eq_iff split: bool.split)
  moreover
  have "?f ` ?LHS \ Func (UNIV :: bool set) (Field r1 <+> Field r2)" (is "_ \ ?RHS")
    by (auto simp: Func_def)
  ultimately show "|?LHS| \o |?RHS|" using card_of_ordLeq by blast
qed

lemma Cfinite_cprod_Cinfinite: "\Cfinite r; Cinfinite s\ \ r *c s \o s"
by (intro cprod_cinfinite_bound)
  (auto intro: ordLeq_refl ordLess_imp_ordLeq[OF Cfinite_ordLess_Cinfinite])

lemma cprod_cexp: "(r *c s) ^c t =o r ^c t *c s ^c t"
  unfolding cprod_def cexp_def Field_card_of by (rule Func_Times_Range)

lemma cprod_cexp_csum_cexp_Cinfinite:
  assumes t: "Cinfinite t"
  shows "(r *c s) ^c t \o (r +c s) ^c t"
proof -
  have "(r *c s) ^c t \o ((r +c s) ^c ctwo) ^c t"
    by (rule cexp_mono1[OF cprod_csum_cexp conjunct2[OF t]])
  also have "((r +c s) ^c ctwo) ^c t =o (r +c s) ^c (ctwo *c t)"
    by (rule cexp_cprod[OF Card_order_csum])
  also have "(r +c s) ^c (ctwo *c t) =o (r +c s) ^c (t *c ctwo)"
    by (rule cexp_cong2[OF cprod_com Card_order_csum Card_order_cprod])
  also have "(r +c s) ^c (t *c ctwo) =o ((r +c s) ^c t) ^c ctwo"
    by (rule ordIso_symmetric[OF cexp_cprod[OF Card_order_csum]])
  also have "((r +c s) ^c t) ^c ctwo =o (r +c s) ^c t"
    by (rule cexp_cprod_ordLeq[OF Card_order_csum t ctwo_Cnotzero ctwo_ordLeq_Cinfinite[OF t]])
  finally show ?thesis .
qed

lemma Cfinite_cexp_Cinfinite:
  assumes s: "Cfinite s" and t: "Cinfinite t"
  shows "s ^c t \o ctwo ^c t"
proof (cases "s \o ctwo")
  case True thus ?thesis using t by (blast intro: cexp_mono1)
next
  case False
  hence "ctwo \o s" using ordLeq_total[of s ctwo] Card_order_ctwo s
    by (auto intro: card_order_on_well_order_on)
  hence "Cnotzero s" using Cnotzero_mono[OF ctwo_Cnotzero] s by blast
  hence st: "Cnotzero (s *c t)" by (intro Cinfinite_Cnotzero[OF Cinfinite_cprod2]) (auto simp: t)
  have "s ^c t \o (ctwo ^c s) ^c t"
    using assms by (blast intro: cexp_mono1 ordLess_imp_ordLeq[OF ordLess_ctwo_cexp])
  also have "(ctwo ^c s) ^c t =o ctwo ^c (s *c t)"
    by (blast intro: Card_order_ctwo cexp_cprod)
  also have "ctwo ^c (s *c t) \o ctwo ^c t"
    using assms st by (intro cexp_mono2_Cnotzero Cfinite_cprod_Cinfinite Card_order_ctwo)
  finally show ?thesis .
qed

lemma csum_Cfinite_cexp_Cinfinite:
  assumes r: "Card_order r" and s: "Cfinite s" and t: "Cinfinite t"
  shows "(r +c s) ^c t \o (r +c ctwo) ^c t"
proof (cases "Cinfinite r")
  case True
  hence "r +c s =o r" by (intro csum_absorb1 ordLess_imp_ordLeq[OF Cfinite_ordLess_Cinfinite] s)
  hence "(r +c s) ^c t =o r ^c t" using t by (blast intro: cexp_cong1)
  also have "r ^c t \o (r +c ctwo) ^c t" using t by (blast intro: cexp_mono1 ordLeq_csum1 r)
  finally show ?thesis .
next
  case False
  with r have "Cfinite r" unfolding cinfinite_def cfinite_def by auto
  hence "Cfinite (r +c s)" by (intro Cfinite_csum s)
  hence "(r +c s) ^c t \o ctwo ^c t" by (intro Cfinite_cexp_Cinfinite t)
  also have "ctwo ^c t \o (r +c ctwo) ^c t" using t
    by (blast intro: cexp_mono1 ordLeq_csum2 Card_order_ctwo)
  finally show ?thesis .
qed

(* cardSuc *)

lemma Cinfinite_cardSuc: "Cinfinite r \ Cinfinite (cardSuc r)"
by (simp add: cinfinite_def cardSuc_Card_order cardSuc_finite)

lemma cardSuc_UNION_Cinfinite:
  assumes "Cinfinite r" "relChain (cardSuc r) As" "B \ (\i \ Field (cardSuc r). As i)" "|B| <=o r"
  shows "\i \ Field (cardSuc r). B \ As i"
using cardSuc_UNION assms unfolding cinfinite_def by blast

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.