Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Product_Plus.thy Sprache: Isabelle

Original von: Isabelle^©

section \<open>Equipollence and Other Relations Connected with Cardinality\<close>

theory "Equipollence"
  imports FuncSet
begin

subsection\<open>Eqpoll\<close>

definition eqpoll :: "'a set \ 'b set \ bool" (infixl "\" 50)
  where "eqpoll A B \ \f. bij_betw f A B"

definition lepoll :: "'a set \ 'b set \ bool" (infixl "\" 50)
  where "lepoll A B \ \f. inj_on f A \ f ` A \ B"

definition lesspoll :: "'a set \ 'b set \ bool" (infixl \\\ 50)
  where "A \ B == A \ B \ ~(A \ B)"

lemma lepoll_empty_iff_empty [simp]: "A \ {} \ A = {}"
  by (auto simp: lepoll_def)

lemma eqpoll_iff_card_of_ordIso: "A \ B \ ordIso2 (card_of A) (card_of B)"
  by (simp add: card_of_ordIso eqpoll_def)

lemma eqpoll_refl [iff]: "A \ A"
  by (simp add: card_of_refl eqpoll_iff_card_of_ordIso)

lemma eqpoll_finite_iff: "A \ B \ finite A \ finite B"
  by (meson bij_betw_finite eqpoll_def)

lemma eqpoll_iff_card:
  assumes "finite A" "finite B"
  shows  "A \ B \ card A = card B"
  using assms by (auto simp: bij_betw_iff_card eqpoll_def)

lemma lepoll_antisym:
  assumes "A \ B" "B \ A" shows "A \ B"
  using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)

lemma lepoll_trans [trans]: "\A \ B; B \ C\ \ A \ C"
  apply (clarsimp simp: lepoll_def)
  apply (rename_tac f g)
  apply (rule_tac x="g \ f" in exI)
  apply (auto simp: image_subset_iff inj_on_def)
  done

lemma lepoll_trans1 [trans]: "\A \ B; B \ C\ \ A \ C"
  by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)

lemma lepoll_trans2 [trans]: "\A \ B; B \ C\ \ A \ C"
  apply (clarsimp simp: eqpoll_def lepoll_def bij_betw_def)
  apply (rename_tac f g)
  apply (rule_tac x="g \ f" in exI)
  apply (auto simp: image_subset_iff inj_on_def)
  done

lemma eqpoll_sym: "A \ B \ B \ A"
  unfolding eqpoll_def
  using bij_betw_the_inv_into by auto

lemma eqpoll_trans [trans]: "\A \ B; B \ C\ \ A \ C"
  unfolding eqpoll_def using bij_betw_trans by blast

lemma eqpoll_imp_lepoll: "A \ B \ A \ B"
  unfolding eqpoll_def lepoll_def by (metis bij_betw_def order_refl)

lemma subset_imp_lepoll: "A \ B \ A \ B"
  by (force simp: lepoll_def)

lemma lepoll_refl [iff]: "A \ A"
  by (simp add: subset_imp_lepoll)

lemma lepoll_iff: "A \ B \ (\g. A \ g ` B)"
  unfolding lepoll_def
proof safe
  fix g assume "A \ g ` B"
  then show "\f. inj_on f A \ f ` A \ B"
    by (rule_tac x="inv_into B g" in exI) (auto simp: inv_into_into inj_on_inv_into)
qed (metis image_mono the_inv_into_onto)

lemma empty_lepoll [iff]: "{} \ A"
  by (simp add: lepoll_iff)

lemma subset_image_lepoll: "B \ f ` A \ B \ A"
  by (auto simp: lepoll_iff)

lemma image_lepoll: "f ` A \ A"
  by (auto simp: lepoll_iff)

lemma infinite_le_lepoll: "infinite A \ (UNIV::nat set) \ A"
apply (auto simp: lepoll_def)
  apply (simp add: infinite_countable_subset)
  using infinite_iff_countable_subset by blast

lemma lepoll_Pow_self: "A \ Pow A"
  unfolding lepoll_def inj_def
  proof (intro exI conjI)
    show "inj_on (\x. {x}) A"
      by (auto simp: inj_on_def)
qed auto

lemma eqpoll_iff_bijections:
   "A \ B \ (\f g. (\x \ A. f x \ B \ g(f x) = x) \ (\y \ B. g y \ A \ f(g y) = y))"
    by (auto simp: eqpoll_def bij_betw_iff_bijections)

lemma lepoll_restricted_funspace:
   "{f. f ` A \ B \ {x. f x \ k x} \ A \ finite {x. f x \ k x}} \ Fpow (A \ B)"
proof -
  have *: "\U \ Fpow (A \ B). f = (\x. if \y. (x, y) \ U then SOME y. (x,y) \ U else k x)"
    if "f ` A \ B" "{x. f x \ k x} \ A" "finite {x. f x \ k x}" for f
    apply (rule_tac x="(\x. (x, f x)) ` {x. f x \ k x}" in bexI)
    using that by (auto simp: image_def Fpow_def)
  show ?thesis
    apply (rule subset_image_lepoll [where f = "\U x. if \y. (x,y) \ U then @y. (x,y) \ U else k x"])
    using * by (auto simp: image_def)
qed

lemma singleton_lepoll: "{x} \ insert y A"
  by (force simp: lepoll_def)

lemma singleton_eqpoll: "{x} \ {y}"
  by (blast intro: lepoll_antisym singleton_lepoll)

lemma subset_singleton_iff_lepoll: "(\x. S \ {x}) \ S \ {()}"
proof safe
  show "S \ {()}" if "S \ {x}" for x
    using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
  show "\x. S \ {x}" if "S \ {()}"
  by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
qed

lemma infinite_insert_lepoll:
  assumes "infinite A" shows "insert a A \ A"
proof -
  obtain f :: "nat \ 'a" where "inj f" and f: "range f \ A"
    using assms infinite_countable_subset by blast
  let ?g = "(\z. if z=a then f 0 else if z \ range f then f (Suc (inv f z)) else z)"
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ?g (insert a A)"
      using inj_on_eq_iff [OF \<open>inj f\<close>]
      by (auto simp: inj_on_def)
    show "?g ` insert a A \ A"
      using f by auto
  qed
qed

lemma infinite_insert_eqpoll: "infinite A \ insert a A \ A"
  by (simp add: lepoll_antisym infinite_insert_lepoll subset_imp_lepoll subset_insertI)

lemma finite_lepoll_infinite:
  assumes "infinite A" "finite B" shows "B \ A"
proof -
  have "B \ (UNIV::nat set)"
    unfolding lepoll_def
    using finite_imp_inj_to_nat_seg [OF \<open>finite B\<close>] by blast
  then show ?thesis
    using \<open>infinite A\<close> infinite_le_lepoll lepoll_trans by auto
qed

subsection\<open>The strict relation\<close>

lemma lesspoll_not_refl [iff]: "~ (i \ i)"
  by (simp add: lepoll_antisym lesspoll_def)

lemma lesspoll_imp_lepoll: "A \ B ==> A \ B"
by (unfold lesspoll_def, blast)

lemma lepoll_iff_leqpoll: "A \ B \ A \ B | A \ B"
  using eqpoll_imp_lepoll lesspoll_def by blast

lemma lesspoll_trans [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)

lemma lesspoll_trans1 [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)

lemma lesspoll_trans2 [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym lepoll_trans lesspoll_def)

lemma eq_lesspoll_trans [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  using eqpoll_imp_lepoll lesspoll_trans1 by blast

lemma lesspoll_eq_trans [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  using eqpoll_imp_lepoll lesspoll_trans2 by blast

lemma lesspoll_Pow_self: "A \ Pow A"
  unfolding lesspoll_def bij_betw_def eqpoll_def
  by (meson lepoll_Pow_self Cantors_paradox)

lemma finite_lesspoll_infinite:
  assumes "infinite A" "finite B" shows "B \ A"
  by (meson assms eqpoll_finite_iff finite_lepoll_infinite lesspoll_def)

subsection\<open>Mapping by an injection\<close>

lemma inj_on_image_eqpoll_self: "inj_on f A \ f ` A \ A"
  by (meson bij_betw_def eqpoll_def eqpoll_sym)

lemma inj_on_image_lepoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A \ B \ A \ B"
  by (meson assms image_lepoll lepoll_def lepoll_trans order_refl)

lemma inj_on_image_lepoll_2 [simp]:
  assumes "inj_on f B" shows "A \ f ` B \ A \ B"
  by (meson assms eq_iff image_lepoll lepoll_def lepoll_trans)

lemma inj_on_image_lesspoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A \ B \ A \ B"
  by (meson assms image_lepoll le_less lepoll_def lesspoll_trans1)

lemma inj_on_image_lesspoll_2 [simp]:
  assumes "inj_on f B" shows "A \ f ` B \ A \ B"
  by (meson assms eqpoll_sym inj_on_image_eqpoll_self lesspoll_eq_trans)

lemma inj_on_image_eqpoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A \ B \ A \ B"
  by (metis assms eqpoll_trans inj_on_image_eqpoll_self eqpoll_sym)

lemma inj_on_image_eqpoll_2 [simp]:
  assumes "inj_on f B" shows "A \ f ` B \ A \ B"
  by (metis assms inj_on_image_eqpoll_1 eqpoll_sym)

subsection \<open>Inserting elements into sets\<close>

lemma insert_lepoll_insertD:
  assumes "insert u A \ insert v B" "u \ A" "v \ B" shows "A \ B"
proof -
  obtain f where inj: "inj_on f (insert u A)" and fim: "f ` (insert u A) \ insert v B"
    by (meson assms lepoll_def)
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    let ?g = "\x\A. if f x = v then f u else f x"
    show "inj_on ?g A"
      using inj \<open>u \<notin> A\<close> by (auto simp: inj_on_def)
    show "?g ` A \ B"
      using fim \<open>u \<notin> A\<close> image_subset_iff inj inj_on_image_mem_iff by fastforce
  qed
qed

lemma insert_eqpoll_insertD: "\insert u A \ insert v B; u \ A; v \ B\ \ A \ B"
  by (meson insert_lepoll_insertD eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)

lemma insert_lepoll_cong:
  assumes "A \ B" "b \ B" shows "insert a A \ insert b B"
proof -
  obtain f where f: "inj_on f A" "f ` A \ B"
    by (meson assms lepoll_def)
  let ?f = "\u \ insert a A. if u=a then b else f u"
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ?f (insert a A)"
      using f \<open>b \<notin> B\<close> by (auto simp: inj_on_def)
    show "?f ` insert a A \ insert b B"
      using f \<open>b \<notin> B\<close> by auto
  qed
qed

lemma insert_eqpoll_cong:
     "\A \ B; a \ A; b \ B\ \ insert a A \ insert b B"
  apply (rule lepoll_antisym)
  apply (simp add: eqpoll_imp_lepoll insert_lepoll_cong)+
  by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong)

lemma insert_eqpoll_insert_iff:
     "\a \ A; b \ B\ \ insert a A \ insert b B \ A \ B"
  by (meson insert_eqpoll_insertD insert_eqpoll_cong)

lemma insert_lepoll_insert_iff:
     " \a \ A; b \ B\ \ (insert a A \ insert b B) \ (A \ B)"
  by (meson insert_lepoll_insertD insert_lepoll_cong)

lemma less_imp_insert_lepoll:
  assumes "A \ B" shows "insert a A \ B"
proof -
  obtain f where "inj_on f A" "f ` A \ B"
    using assms by (metis bij_betw_def eqpoll_def lepoll_def lesspoll_def psubset_eq)
  then obtain b where b: "b \ B" "b \ f ` A"
    by auto
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on (f(a:=b)) (insert a A)"
      using b \<open>inj_on f A\<close> by (auto simp: inj_on_def)
    show "(f(a:=b)) ` insert a A \ B"
      using \<open>f ` A \<subset> B\<close>  by (auto simp: b)
  qed
qed

lemma finite_insert_lepoll: "finite A \ (insert a A \ A) \ (a \ A)"
proof (induction A rule: finite_induct)
  case (insert x A)
  then show ?case
    apply (auto simp: insert_absorb)
    by (metis insert_commute insert_iff insert_lepoll_insertD)
qed auto

subsection\<open>Binary sums and unions\<close>

lemma Un_lepoll_mono:
  assumes "A \ C" "B \ D" "disjnt C D" shows "A \ B \ C \ D"
proof -
  obtain f g where inj: "inj_on f A" "inj_on g B" and fg: "f ` A \ C" "g ` B \ D"
    by (meson assms lepoll_def)
  have "inj_on (\x. if x \ A then f x else g x) (A \ B)"
    using inj \<open>disjnt C D\<close> fg unfolding disjnt_iff
    by (fastforce intro: inj_onI dest: inj_on_contraD split: if_split_asm)
  with fg show ?thesis
    unfolding lepoll_def
    by (rule_tac x="\x. if x \ A then f x else g x" in exI) auto
qed

lemma Un_eqpoll_cong: "\A \ C; B \ D; disjnt A B; disjnt C D\ \ A \ B \ C \ D"
  by (meson Un_lepoll_mono eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)

lemma sum_lepoll_mono:
  assumes "A \ C" "B \ D" shows "A <+> B \ C <+> D"
proof -
  obtain f g where "inj_on f A" "f ` A \ C" "inj_on g B" "g ` B \ D"
    by (meson assms lepoll_def)
  then show ?thesis
    unfolding lepoll_def
    by (rule_tac x="case_sum (Inl \ f) (Inr \ g)" in exI) (force simp: inj_on_def)
qed

lemma sum_eqpoll_cong: "\A \ C; B \ D\ \ A <+> B \ C <+> D"
  by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym sum_lepoll_mono)

subsection\<open>Binary Cartesian products\<close>

lemma times_square_lepoll: "A \ A \ A"
  unfolding lepoll_def inj_def
proof (intro exI conjI)
  show "inj_on (\x. (x,x)) A"
    by (auto simp: inj_on_def)
qed auto

lemma times_commute_eqpoll: "A \ B \ B \ A"
  unfolding eqpoll_def
  by (force intro: bij_betw_byWitness [where f = "\(x,y). (y,x)" and f' = "\(x,y). (y,x)"])

lemma times_assoc_eqpoll: "(A \ B) \ C \ A \ (B \ C)"
  unfolding eqpoll_def
  by (force intro: bij_betw_byWitness [where f = "\((x,y),z). (x,(y,z))" and f' = "\(x,(y,z)). ((x,y),z)"])

lemma times_singleton_eqpoll: "{a} \ A \ A"
proof -
  have "{a} \ A = (\x. (a,x)) ` A"
    by auto
  also have "\ \ A"
    proof (rule inj_on_image_eqpoll_self)
      show "inj_on (Pair a) A"
        by (auto simp: inj_on_def)
    qed
    finally show ?thesis .
qed

lemma times_lepoll_mono:
  assumes "A \ C" "B \ D" shows "A \ B \ C \ D"
proof -
  obtain f g where "inj_on f A" "f ` A \ C" "inj_on g B" "g ` B \ D"
    by (meson assms lepoll_def)
  then show ?thesis
    unfolding lepoll_def
    by (rule_tac x="\(x,y). (f x, g y)" in exI) (auto simp: inj_on_def)
qed

lemma times_eqpoll_cong: "\A \ C; B \ D\ \ A \ B \ C \ D"
  by (metis eqpoll_imp_lepoll eqpoll_sym lepoll_antisym times_lepoll_mono)

lemma
  assumes "B \ {}" shows lepoll_times1: "A \ A \ B" and lepoll_times2: "A \ B \ A"
  using assms lepoll_iff by fastforce+

lemma times_0_eqpoll: "{} \ A \ {}"
  by (simp add: eqpoll_iff_bijections)

lemma Sigma_lepoll_mono:
  assumes "A \ C" "\x. x \ A \ B x \ D x" shows "Sigma A B \ Sigma C D"
proof -
  have "\x. x \ A \ \f. inj_on f (B x) \ f ` (B x) \ D x"
    by (meson assms lepoll_def)
  then obtain f where  "\x. x \ A \ inj_on (f x) (B x) \ f x ` B x \ D x"
    by metis
  with \<open>A \<subseteq> C\<close> show ?thesis
    unfolding lepoll_def inj_on_def
    by (rule_tac x="\(x,y). (x, f x y)" in exI) force
qed

lemma sum_times_distrib_eqpoll: "(A <+> B) \ C \ (A \ C) <+> (B \ C)"
  unfolding eqpoll_def
proof
  show "bij_betw (\(x,z). case_sum(\y. Inl(y,z)) (\y. Inr(y,z)) x) ((A <+> B) \ C) (A \ C <+> B \ C)"
    by (rule bij_betw_byWitness [where f' = "case_sum (\(x,z). (Inl x, z)) (\(y,z). (Inr y, z))"]) auto
qed

lemma prod_insert_eqpoll:
  assumes "a \ A" shows "insert a A \ B \ B <+> A \ B"
  unfolding eqpoll_def
  proof
  show "bij_betw (\(x,y). if x=a then Inl y else Inr (x,y)) (insert a A \ B) (B <+> A \ B)"
    by (rule bij_betw_byWitness [where f' = "case_sum (\y. (a,y)) id"]) (auto simp: assms)
qed

subsection\<open>General Unions\<close>

lemma Union_eqpoll_Times:
  assumes B: "\x. x \ A \ F x \ B" and disj: "pairwise (\x y. disjnt (F x) (F y)) A"
  shows "(\x\A. F x) \ A \ B"
proof (rule lepoll_antisym)
  obtain b where b: "\x. x \ A \ bij_betw (b x) (F x) B"
    using B unfolding eqpoll_def by metis
  show "\(F ` A) \ A \ B"
    unfolding lepoll_def
  proof (intro exI conjI)
    define \<chi> where "\<chi> \<equiv> \<lambda>z. THE x. x \<in> A \<and> z \<in> F x"
    have \<chi>: "\<chi> z = x" if "x \<in> A" "z \<in> F x" for x z
      unfolding \<chi>_def
      apply (rule the_equality)
      apply (simp add: that)
      by (metis disj disjnt_iff pairwiseD that)
    let ?f = "\z. (\ z, b (\ z) z)"
    show "inj_on ?f (\(F ` A))"
      unfolding inj_on_def
      by clarify (metis \<chi> b bij_betw_inv_into_left)
    show "?f ` \(F ` A) \ A \ B"
      using \<chi> b bij_betwE by blast
  qed
  show "A \ B \ \(F ` A)"
    unfolding lepoll_def
  proof (intro exI conjI)
    let ?f = "\(x,y). inv_into (F x) (b x) y"
    have *: "inv_into (F x) (b x) y \ F x" if "x \ A" "y \ B" for x y
      by (metis b bij_betw_imp_surj_on inv_into_into that)
    then show "inj_on ?f (A \ B)"
      unfolding inj_on_def
      by clarsimp (metis (mono_tags, lifting) b bij_betw_inv_into_right disj disjnt_iff pairwiseD)
    show "?f ` (A \ B) \ \ (F ` A)"
      by clarsimp (metis b bij_betw_imp_surj_on inv_into_into)
  qed
qed

lemma UN_lepoll_UN:
  assumes A: "\x. x \ A \ B x \ C x"
    and disj: "pairwise (\x y. disjnt (C x) (C y)) A"
  shows "\ (B`A) \ \ (C`A)"
proof -
  obtain f where f: "\x. x \ A \ inj_on (f x) (B x) \ f x ` (B x) \ (C x)"
    using A unfolding lepoll_def by metis
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    define \<chi> where "\<chi> \<equiv> \<lambda>z. @x. x \<in> A \<and> z \<in> B x"
    have \<chi>: "\<chi> z \<in> A \<and> z \<in> B (\<chi> z)" if "x \<in> A" "z \<in> B x" for x z
      unfolding \<chi>_def by (metis (mono_tags, lifting) someI_ex that)
    let ?f = "\z. (f (\ z) z)"
    show "inj_on ?f (\(B ` A))"
      using disj f unfolding inj_on_def disjnt_iff pairwise_def image_subset_iff
      by (metis UN_iff \<chi>)
    show "?f ` \ (B ` A) \ \ (C ` A)"
      using \<chi> f unfolding image_subset_iff by blast
  qed
qed

lemma UN_eqpoll_UN:
  assumes A: "\x. x \ A \ B x \ C x"
    and B: "pairwise (\x y. disjnt (B x) (B y)) A"
    and C: "pairwise (\x y. disjnt (C x) (C y)) A"
  shows "(\x\A. B x) \ (\x\A. C x)"
proof (rule lepoll_antisym)
  show "\ (B ` A) \ \ (C ` A)"
    by (meson A C UN_lepoll_UN eqpoll_imp_lepoll)
  show "\ (C ` A) \ \ (B ` A)"
    by (simp add: A B UN_lepoll_UN eqpoll_imp_lepoll eqpoll_sym)
qed

subsection\<open>General Cartesian products (Pi)\<close>

lemma PiE_sing_eqpoll_self: "({a} \\<^sub>E B) \ B"
proof -
  have 1: "x = y"
    if "x \ {a} \\<^sub>E B" "y \ {a} \\<^sub>E B" "x a = y a" for x y
    by (metis IntD2 PiE_def extensionalityI singletonD that)
  have 2: "x \ (\h. h a) ` ({a} \\<^sub>E B)" if "x \ B" for x
    using that by (rule_tac x="\z\{a}. x" in image_eqI) auto
  show ?thesis
  unfolding eqpoll_def bij_betw_def inj_on_def
  by (force intro: 1 2)
qed

lemma lepoll_funcset_right:
   "B \ B' \ A \\<^sub>E B \ A \\<^sub>E B'"
  apply (auto simp: lepoll_def inj_on_def)
  apply (rule_tac x = "\g. \z \ A. f(g z)" in exI)
  apply (auto simp: fun_eq_iff)
  apply (metis PiE_E)
  by blast

lemma lepoll_funcset_left:
  assumes "B \ {}" "A \ A'"
  shows "A \\<^sub>E B \ A' \\<^sub>E B"
proof -
  obtain b where "b \ B"
    using assms by blast
  obtain f where "inj_on f A" and fim: "f ` A \ A'"
    using assms by (auto simp: lepoll_def)
  then obtain h where h: "\x. x \ A \ h (f x) = x"
    using the_inv_into_f_f by fastforce
  let ?F = "\g. \u \ A'. if h u \ A then g(h u) else b"
  show ?thesis
    unfolding lepoll_def inj_on_def
  proof (intro exI conjI ballI impI ext)
    fix k l x
    assume k: "k \ A \\<^sub>E B" and l: "l \ A \\<^sub>E B" and "?F k = ?F l"
    then have "?F k (f x) = ?F l (f x)"
      by simp
    then show "k x = l x"
      apply (auto simp: h split: if_split_asm)
      apply (metis PiE_arb h k l)
      apply (metis (full_types) PiE_E h k l)
      using fim k l by fastforce
  next
    show "?F ` (A \\<^sub>E B) \ A' \\<^sub>E B"
      using \<open>b \<in> B\<close> by force
  qed
qed

lemma lepoll_funcset:
   "\B \ {}; A \ A'; B \ B'\ \ A \\<^sub>E B \ A' \\<^sub>E B'"
  by (rule lepoll_trans [OF lepoll_funcset_right lepoll_funcset_left]) auto

lemma lepoll_PiE:
  assumes "\i. i \ A \ B i \ C i"
  shows "PiE A B \ PiE A C"
proof -
  obtain f where f: "\i. i \ A \ inj_on (f i) (B i) \ (f i) ` B i \ C i"
    using assms unfolding lepoll_def by metis
  then show ?thesis
    unfolding lepoll_def
    apply (rule_tac x = "\g. \i \ A. f i (g i)" in exI)
    apply (auto simp: inj_on_def)
     apply (rule PiE_ext, auto)
     apply (metis (full_types) PiE_mem restrict_apply')
    by blast
qed

lemma card_le_PiE_subindex:
  assumes "A \ A'" "Pi\<^sub>E A' B \ {}"
  shows "PiE A B \ PiE A' B"
proof -
  have "\x. x \ A' \ \y. y \ B x"
    using assms by blast
  then obtain g where g: "\x. x \ A' \ g x \ B x"
    by metis
  let ?F = "\f x. if x \ A then f x else if x \ A' then g x else undefined"
  have "Pi\<^sub>E A B \ (\f. restrict f A) ` Pi\<^sub>E A' B"
  proof
    show "f \ Pi\<^sub>E A B \ f \ (\f. restrict f A) ` Pi\<^sub>E A' B" for f
      using \<open>A \<subseteq> A'\<close>
      by (rule_tac x="?F f" in image_eqI) (auto simp: g fun_eq_iff)
  qed
  then have "Pi\<^sub>E A B \ (\f. \i \ A. f i) ` Pi\<^sub>E A' B"
    by (simp add: subset_imp_lepoll)
  also have "\ \ PiE A' B"
    by (rule image_lepoll)
  finally show ?thesis .
qed

lemma finite_restricted_funspace:
  assumes "finite A" "finite B"
  shows "finite {f. f ` A \ B \ {x. f x \ k x} \ A}" (is "finite ?F")
proof (rule finite_subset)
  show "finite ((\U x. if \y. (x,y) \ U then @y. (x,y) \ U else k x) ` Pow(A \ B))" (is "finite ?G")
    using assms by auto
  show "?F \ ?G"
  proof
    fix f
    assume "f \ ?F"
    then show "f \ ?G"
      by (rule_tac x="(\x. (x,f x)) ` {x. f x \ k x}" in image_eqI) (auto simp: fun_eq_iff image_def)
  qed
qed

proposition finite_PiE_iff:
   "finite(PiE I S) \ PiE I S = {} \ finite {i \ I. ~(\a. S i \ {a})} \ (\i \ I. finite(S i))"
(is "?lhs = ?rhs")
proof (cases "PiE I S = {}")
  case False
  define J where "J \ {i \ I. \a. S i \ {a}}"
  show ?thesis
  proof
    assume L: ?lhs
    have "infinite (Pi\<^sub>E I S)" if "infinite J"
    proof -
      have "(UNIV::nat set) \ (UNIV::(nat\bool) set)"
      proof -
        have "\N::nat set. inj_on (=) N"
          by (simp add: inj_on_def)
        then show ?thesis
          by (meson infinite_iff_countable_subset infinite_le_lepoll top.extremum)
      qed
      also have "\ = (UNIV::nat set) \\<^sub>E (UNIV::bool set)"
        by auto
      also have "\ \ J \\<^sub>E (UNIV::bool set)"
        apply (rule lepoll_funcset_left)
        using infinite_le_lepoll that by auto
      also have "\ \ Pi\<^sub>E J S"
      proof -
        have *: "(UNIV::bool set) \ S i" if "i \ I" and "\a. \ S i \ {a}" for i
        proof -
          obtain a b where "{a,b} \ S i" "a \ b"
            by (metis \<open>\<forall>a. \<not> S i \<subseteq> {a}\<close> all_not_in_conv empty_subsetI insertCI insert_subset set_eq_subset subsetI)
          then show ?thesis
            apply (clarsimp simp: lepoll_def inj_on_def)
            apply (rule_tac x="\x. if x then a else b" in exI, auto)
            done
        qed
        show ?thesis
          by (auto simp: * J_def intro: lepoll_PiE)
      qed
      also have "\ \ Pi\<^sub>E I S"
        using False by (auto simp: J_def intro: card_le_PiE_subindex)
      finally have "(UNIV::nat set) \ Pi\<^sub>E I S" .
      then show ?thesis
        by (simp add: infinite_le_lepoll)
    qed
    moreover have "finite (S i)" if "i \ I" for i
    proof (rule finite_subset)
      obtain f where f: "f \ PiE I S"
        using False by blast
      show "S i \ (\f. f i) ` Pi\<^sub>E I S"
      proof
        show "s \ (\f. f i) ` Pi\<^sub>E I S" if "s \ S i" for s
          using that f \<open>i \<in> I\<close>
          by (rule_tac x="\j. if j = i then s else f j" in image_eqI) auto
      qed
    next
      show "finite ((\x. x i) ` Pi\<^sub>E I S)"
        using L by blast
    qed
    ultimately show ?rhs
      using L
      by (auto simp: J_def False)
  next
    assume R: ?rhs
    have "\i \ I - J. \a. S i = {a}"
      using False J_def by blast
    then obtain a where a: "\i \ I - J. S i = {a i}"
      by metis
    let ?F = "{f. f ` J \ (\i \ J. S i) \ {i. f i \ (if i \ I then a i else undefined)} \ J}"
    have *: "finite (Pi\<^sub>E I S)"
      if "finite J" and "\i\I. finite (S i)"
    proof (rule finite_subset)
      show "Pi\<^sub>E I S \ ?F"
        apply safe
        using J_def apply blast
        by (metis DiffI PiE_E a singletonD)
      show "finite ?F"
      proof (rule finite_restricted_funspace [OF \<open>finite J\<close>])
        show "finite (\ (S ` J))"
          using that J_def by blast
      qed
  qed
  show ?lhs
      using R by (auto simp: * J_def)
  qed
qed auto

corollary finite_funcset_iff:
  "finite(I \\<^sub>E S) \ (\a. S \ {a}) \ I = {} \ finite I \ finite S"
  apply (auto simp: finite_PiE_iff PiE_eq_empty_iff dest: not_finite_existsD)
  using finite.simps by auto

lemma lists_lepoll_mono:
  assumes "A \ B" shows "lists A \ lists B"
proof -
  obtain f where f: "inj_on f A" "f ` A \ B"
    by (meson assms lepoll_def)
  moreover have "inj_on (map f) (lists A)"
    using f unfolding inj_on_def
    by clarsimp (metis list.inj_map_strong)
  ultimately show ?thesis
    unfolding lepoll_def by force
qed

lemma lepoll_lists: "A \ lists A"
  unfolding lepoll_def inj_on_def by(rule_tac x="\x. [x]" in exI) auto

end

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.