Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: FuncSet.thy Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/Library/FuncSet.thy
    Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
*)

section \<open>Pi and Function Sets\<close>

theory FuncSet
  imports Main
  abbrevs PiE = "Pi\<^sub>E"
    and PIE = "\\<^sub>E"
begin

definition Pi :: "'a set \ ('a \ 'b set) \ ('a \ 'b) set"
  where "Pi A B = {f. \x. x \ A \ f x \ B x}"

definition extensional :: "'a set \ ('a \ 'b) set"
  where "extensional A = {f. \x. x \ A \ f x = undefined}"

definition "restrict" :: "('a \ 'b) \ 'a set \ 'a \ 'b"
  where "restrict f A = (\x. if x \ A then f x else undefined)"

abbreviation funcset :: "'a set \ 'b set \ ('a \ 'b) set" (infixr "\" 60)
  where "A \ B \ Pi A (\_. B)"

syntax
  "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\ _\_./ _)" 10)
  "_lam" :: "pttrn \ 'a set \ ('a \ 'b) \ ('a \ 'b)" ("(3\_\_./ _)" [0,0,3] 3)
translations
  "\ x\A. B" \ "CONST Pi A (\x. B)"
  "\x\A. f" \ "CONST restrict (\x. f) A"

definition "compose" :: "'a set \ ('b \ 'c) \ ('a \ 'b) \ ('a \ 'c)"
  where "compose A g f = (\x\A. g (f x))"

subsection \<open>Basic Properties of \<^term>\<open>Pi\<close>\<close>

lemma Pi_I[intro!]: "(\x. x \ A \ f x \ B x) \ f \ Pi A B"
  by (simp add: Pi_def)

lemma Pi_I'[simp]: "(\x. x \ A \ f x \ B x) \ f \ Pi A B"
  by (simp add:Pi_def)

lemma funcsetI: "(\x. x \ A \ f x \ B) \ f \ A \ B"
  by (simp add: Pi_def)

lemma Pi_mem: "f \ Pi A B \ x \ A \ f x \ B x"
  by (simp add: Pi_def)

lemma Pi_iff: "f \ Pi I X \ (\i\I. f i \ X i)"
  unfolding Pi_def by auto

lemma PiE [elim]: "f \ Pi A B \ (f x \ B x \ Q) \ (x \ A \ Q) \ Q"
  by (auto simp: Pi_def)

lemma Pi_cong: "(\w. w \ A \ f w = g w) \ f \ Pi A B \ g \ Pi A B"
  by (auto simp: Pi_def)

lemma funcset_id [simp]: "(\x. x) \ A \ A"
  by auto

lemma funcset_mem: "f \ A \ B \ x \ A \ f x \ B"
  by (simp add: Pi_def)

lemma funcset_image: "f \ A \ B \ f ` A \ B"
  by auto

lemma image_subset_iff_funcset: "F ` A \ B \ F \ A \ B"
  by auto

lemma funcset_to_empty_iff: "A \ {} = (if A={} then UNIV else {})"
  by auto

lemma Pi_eq_empty[simp]: "(\ x \ A. B x) = {} \ (\x\A. B x = {})"
proof -
  have "\x\A. B x = {}" if "\f. \y. y \ A \ f y \ B y"
    using that [of "\u. SOME y. y \ B u"] some_in_eq by blast
  then show ?thesis
    by force
qed

lemma Pi_empty [simp]: "Pi {} B = UNIV"
  by (simp add: Pi_def)

lemma Pi_Int: "Pi I E \ Pi I F = (\ i\I. E i \ F i)"
  by auto

lemma Pi_UN:
  fixes A :: "nat \ 'i \ 'a set"
  assumes "finite I"
    and mono: "\i n m. i \ I \ n \ m \ A n i \ A m i"
  shows "(\n. Pi I (A n)) = (\ i\I. \n. A n i)"
proof (intro set_eqI iffI)
  fix f
  assume "f \ (\ i\I. \n. A n i)"
  then have "\i\I. \n. f i \ A n i"
    by auto
  from bchoice[OF this] obtain n where n: "f i \ A (n i) i" if "i \ I" for i
    by auto
  obtain k where k: "n i \ k" if "i \ I" for i
    using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
  have "f \ Pi I (A k)"
  proof (intro Pi_I)
    fix i
    assume "i \ I"
    from mono[OF this, of "n i" k] k[OF this] n[OF this]
    show "f i \ A k i" by auto
  qed
  then show "f \ (\n. Pi I (A n))"
    by auto
qed auto

lemma Pi_UNIV [simp]: "A \ UNIV = UNIV"
  by (simp add: Pi_def)

text \<open>Covariance of Pi-sets in their second argument\<close>
lemma Pi_mono: "(\x. x \ A \ B x \ C x) \ Pi A B \ Pi A C"
  by auto

text \<open>Contravariance of Pi-sets in their first argument\<close>
lemma Pi_anti_mono: "A' \ A \ Pi A B \ Pi A' B"
  by auto

lemma prod_final:
  assumes 1: "fst \ f \ Pi A B"
    and 2: "snd \ f \ Pi A C"
  shows "f \ (\ z \ A. B z \ C z)"
proof (rule Pi_I)
  fix z
  assume z: "z \ A"
  have "f z = (fst (f z), snd (f z))"
    by simp
  also have "\ \ B z \ C z"
    by (metis SigmaI PiE o_apply 1 2 z)
  finally show "f z \ B z \ C z" .
qed

lemma Pi_split_domain[simp]: "x \ Pi (I \ J) X \ x \ Pi I X \ x \ Pi J X"
  by (auto simp: Pi_def)

lemma Pi_split_insert_domain[simp]: "x \ Pi (insert i I) X \ x \ Pi I X \ x i \ X i"
  by (auto simp: Pi_def)

lemma Pi_cancel_fupd_range[simp]: "i \ I \ x \ Pi I (B(i := b)) \ x \ Pi I B"
  by (auto simp: Pi_def)

lemma Pi_cancel_fupd[simp]: "i \ I \ x(i := a) \ Pi I B \ x \ Pi I B"
  by (auto simp: Pi_def)

lemma Pi_fupd_iff: "i \ I \ f \ Pi I (B(i := A)) \ f \ Pi (I - {i}) B \ f i \ A"
  apply auto
  apply (metis PiE fun_upd_apply)
  by force

subsection \<open>Composition With a Restricted Domain: \<^term>\<open>compose\<close>\<close>

lemma funcset_compose: "f \ A \ B \ g \ B \ C \ compose A g f \ A \ C"
  by (simp add: Pi_def compose_def restrict_def)

lemma compose_assoc:
  assumes "f \ A \ B"
  shows "compose A h (compose A g f) = compose A (compose B h g) f"
  using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)

lemma compose_eq: "x \ A \ compose A g f x = g (f x)"
  by (simp add: compose_def restrict_def)

lemma surj_compose: "f ` A = B \ g ` B = C \ compose A g f ` A = C"
  by (auto simp add: image_def compose_eq)

subsection \<open>Bounded Abstraction: \<^term>\<open>restrict\<close>\<close>

lemma restrict_cong: "I = J \ (\i. i \ J =simp=> f i = g i) \ restrict f I = restrict g J"
  by (auto simp: restrict_def fun_eq_iff simp_implies_def)

lemma restrict_in_funcset: "(\x. x \ A \ f x \ B) \ (\x\A. f x) \ A \ B"
  by (simp add: Pi_def restrict_def)

lemma restrictI[intro!]: "(\x. x \ A \ f x \ B x) \ (\x\A. f x) \ Pi A B"
  by (simp add: Pi_def restrict_def)

lemma restrict_apply[simp]: "(\y\A. f y) x = (if x \ A then f x else undefined)"
  by (simp add: restrict_def)

lemma restrict_apply': "x \ A \ (\y\A. f y) x = f x"
  by simp

lemma restrict_ext: "(\x. x \ A \ f x = g x) \ (\x\A. f x) = (\x\A. g x)"
  by (simp add: fun_eq_iff Pi_def restrict_def)

lemma restrict_UNIV: "restrict f UNIV = f"
  by (simp add: restrict_def)

lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
  by (simp add: inj_on_def restrict_def)

lemma Id_compose: "f \ A \ B \ f \ extensional A \ compose A (\y\B. y) f = f"
  by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)

lemma compose_Id: "g \ A \ B \ g \ extensional A \ compose A g (\x\A. x) = g"
  by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)

lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
  by (auto simp add: restrict_def)

lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \ B)"
  unfolding restrict_def by (simp add: fun_eq_iff)

lemma restrict_fupd[simp]: "i \ I \ restrict (f (i := x)) I = restrict f I"
  by (auto simp: restrict_def)

lemma restrict_upd[simp]: "i \ I \ (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
  by (auto simp: fun_eq_iff)

lemma restrict_Pi_cancel: "restrict x I \ Pi I A \ x \ Pi I A"
  by (auto simp: restrict_def Pi_def)

lemma sum_restrict' [simp]: "sum' (\<lambda>i\<in>I. g i) I = sum' (\<lambda>i. g i) I"
  by (simp add: sum.G_def conj_commute cong: conj_cong)

lemma prod_restrict' [simp]: "prod' (\<lambda>i\<in>I. g i) I = prod' (\<lambda>i. g i) I"
  by (simp add: prod.G_def conj_commute cong: conj_cong)

subsection \<open>Bijections Between Sets\<close>

text \<open>The definition of \<^const>\<open>bij_betw\<close> is in \<open>Fun.thy\<close>, but most of
the theorems belong here, or need at least \<^term>\<open>Hilbert_Choice\<close>.\<close>

lemma bij_betwI:
  assumes "f \ A \ B"
    and "g \ B \ A"
    and g_f: "\x. x\A \ g (f x) = x"
    and f_g: "\y. y\B \ f (g y) = y"
  shows "bij_betw f A B"
  unfolding bij_betw_def
proof
  show "inj_on f A"
    by (metis g_f inj_on_def)
  have "f ` A \ B"
    using \<open>f \<in> A \<rightarrow> B\<close> by auto
  moreover
  have "B \ f ` A"
    by auto (metis Pi_mem \<open>g \<in> B \<rightarrow> A\<close> f_g image_iff)
  ultimately show "f ` A = B"
    by blast
qed

lemma bij_betw_imp_funcset: "bij_betw f A B \ f \ A \ B"
  by (auto simp add: bij_betw_def)

lemma inj_on_compose: "bij_betw f A B \ inj_on g B \ inj_on (compose A g f) A"
  by (auto simp add: bij_betw_def inj_on_def compose_eq)

lemma bij_betw_compose: "bij_betw f A B \ bij_betw g B C \ bij_betw (compose A g f) A C"
  apply (simp add: bij_betw_def compose_eq inj_on_compose)
  apply (auto simp add: compose_def image_def)
  done

lemma bij_betw_restrict_eq [simp]: "bij_betw (restrict f A) A B = bij_betw f A B"
  by (simp add: bij_betw_def)

subsection \<open>Extensionality\<close>

lemma extensional_empty[simp]: "extensional {} = {\x. undefined}"
  unfolding extensional_def by auto

lemma extensional_arb: "f \ extensional A \ x \ A \ f x = undefined"
  by (simp add: extensional_def)

lemma restrict_extensional [simp]: "restrict f A \ extensional A"
  by (simp add: restrict_def extensional_def)

lemma compose_extensional [simp]: "compose A f g \ extensional A"
  by (simp add: compose_def)

lemma extensionalityI:
  assumes "f \ extensional A"
    and "g \ extensional A"
    and "\x. x \ A \ f x = g x"
  shows "f = g"
  using assms by (force simp add: fun_eq_iff extensional_def)

lemma extensional_restrict:  "f \ extensional A \ restrict f A = f"
  by (rule extensionalityI[OF restrict_extensional]) auto

lemma extensional_subset: "f \ extensional A \ A \ B \ f \ extensional B"
  unfolding extensional_def by auto

lemma inv_into_funcset: "f ` A = B \ (\x\B. inv_into A f x) \ B \ A"
  by (unfold inv_into_def) (fast intro: someI2)

lemma compose_inv_into_id: "bij_betw f A B \ compose A (\y\B. inv_into A f y) f = (\x\A. x)"
  apply (simp add: bij_betw_def compose_def)
  apply (rule restrict_ext, auto)
  done

lemma compose_id_inv_into: "f ` A = B \ compose B f (\y\B. inv_into A f y) = (\x\B. x)"
  apply (simp add: compose_def)
  apply (rule restrict_ext)
  apply (simp add: f_inv_into_f)
  done

lemma extensional_insert[intro, simp]:
  assumes "a \ extensional (insert i I)"
  shows "a(i := b) \ extensional (insert i I)"
  using assms unfolding extensional_def by auto

lemma extensional_Int[simp]: "extensional I \ extensional I' = extensional (I \ I')"
  unfolding extensional_def by auto

lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
  by (auto simp: extensional_def)

lemma restrict_extensional_sub[intro]: "A \ B \ restrict f A \ extensional B"
  unfolding restrict_def extensional_def by auto

lemma extensional_insert_undefined[intro, simp]:
  "a \ extensional (insert i I) \ a(i := undefined) \ extensional I"
  unfolding extensional_def by auto

lemma extensional_insert_cancel[intro, simp]:
  "a \ extensional I \ a \ extensional (insert i I)"
  unfolding extensional_def by auto

subsection \<open>Cardinality\<close>

lemma card_inj: "f \ A \ B \ inj_on f A \ finite B \ card A \ card B"
  by (rule card_inj_on_le) auto

lemma card_bij:
  assumes "f \ A \ B" "inj_on f A"
    and "g \ B \ A" "inj_on g B"
    and "finite A" "finite B"
  shows "card A = card B"
  using assms by (blast intro: card_inj order_antisym)

subsection \<open>Extensional Function Spaces\<close>

definition PiE :: "'a set \ ('a \ 'b set) \ ('a \ 'b) set"
  where "PiE S T = Pi S T \ extensional S"

abbreviation "Pi\<^sub>E A B \ PiE A B"

syntax
  "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\\<^sub>E _\_./ _)" 10)
translations
  "\\<^sub>E x\A. B" \ "CONST Pi\<^sub>E A (\x. B)"

abbreviation extensional_funcset :: "'a set \ 'b set \ ('a \ 'b) set" (infixr "\\<^sub>E" 60)
  where "A \\<^sub>E B \ (\\<^sub>E i\A. B)"

lemma extensional_funcset_def: "extensional_funcset S T = (S \ T) \ extensional S"
  by (simp add: PiE_def)

lemma PiE_empty_domain[simp]: "Pi\<^sub>E {} T = {\x. undefined}"
  unfolding PiE_def by simp

lemma PiE_UNIV_domain: "Pi\<^sub>E UNIV T = Pi UNIV T"
  unfolding PiE_def by simp

lemma PiE_empty_range[simp]: "i \ I \ F i = {} \ (\\<^sub>E i\I. F i) = {}"
  unfolding PiE_def by auto

lemma PiE_eq_empty_iff: "Pi\<^sub>E I F = {} \ (\i\I. F i = {})"
proof
  assume "Pi\<^sub>E I F = {}"
  show "\i\I. F i = {}"
  proof (rule ccontr)
    assume "\ ?thesis"
    then have "\i. \y. (i \ I \ y \ F i) \ (i \ I \ y = undefined)"
      by auto
    from choice[OF this]
    obtain f where " \x. (x \ I \ f x \ F x) \ (x \ I \ f x = undefined)" ..
    then have "f \ Pi\<^sub>E I F"
      by (auto simp: extensional_def PiE_def)
    with \<open>Pi\<^sub>E I F = {}\<close> show False
      by auto
  qed
qed (auto simp: PiE_def)

lemma PiE_arb: "f \ Pi\<^sub>E S T \ x \ S \ f x = undefined"
  unfolding PiE_def by auto (auto dest!: extensional_arb)

lemma PiE_mem: "f \ Pi\<^sub>E S T \ x \ S \ f x \ T x"
  unfolding PiE_def by auto

lemma PiE_fun_upd: "y \ T x \ f \ Pi\<^sub>E S T \ f(x := y) \ Pi\<^sub>E (insert x S) T"
  unfolding PiE_def extensional_def by auto

lemma fun_upd_in_PiE: "x \ S \ f \ Pi\<^sub>E (insert x S) T \ f(x := undefined) \ Pi\<^sub>E S T"
  unfolding PiE_def extensional_def by auto

lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)"
proof -
  {
    fix f assume "f \ Pi\<^sub>E (insert x S) T" "x \ S"
    then have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)"
      by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
  }
  moreover
  {
    fix f assume "f \ Pi\<^sub>E (insert x S) T" "x \ S"
    then have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)"
      by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
  }
  ultimately show ?thesis
    by (auto intro: PiE_fun_upd)
qed

lemma PiE_Int: "Pi\<^sub>E I A \ Pi\<^sub>E I B = Pi\<^sub>E I (\x. A x \ B x)"
  by (auto simp: PiE_def)

lemma PiE_cong: "(\i. i\I \ A i = B i) \ Pi\<^sub>E I A = Pi\<^sub>E I B"
  unfolding PiE_def by (auto simp: Pi_cong)

lemma PiE_E [elim]:
  assumes "f \ Pi\<^sub>E A B"
  obtains "x \ A" and "f x \ B x"
    | "x \ A" and "f x = undefined"
  using assms by (auto simp: Pi_def PiE_def extensional_def)

lemma PiE_I[intro!]:
  "(\x. x \ A \ f x \ B x) \ (\x. x \ A \ f x = undefined) \ f \ Pi\<^sub>E A B"
  by (simp add: PiE_def extensional_def)

lemma PiE_mono: "(\x. x \ A \ B x \ C x) \ Pi\<^sub>E A B \ Pi\<^sub>E A C"
  by auto

lemma PiE_iff: "f \ Pi\<^sub>E I X \ (\i\I. f i \ X i) \ f \ extensional I"
  by (simp add: PiE_def Pi_iff)

lemma ext_funcset_to_sing_iff [simp]: "A \\<^sub>E {a} = {\x\A. a}"
  by (auto simp: PiE_def Pi_iff extensionalityI)

lemma PiE_restrict[simp]:  "f \ Pi\<^sub>E A B \ restrict f A = f"
  by (simp add: extensional_restrict PiE_def)

lemma restrict_PiE[simp]: "restrict f I \ Pi\<^sub>E I S \ f \ Pi I S"
  by (auto simp: PiE_iff)

lemma PiE_eq_subset:
  assumes ne: "\i. i \ I \ F i \ {}" "\i. i \ I \ F' i \ {}"
    and eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
    and "i \ I"
  shows "F i \ F' i"
proof
  fix x
  assume "x \ F i"
  with ne have "\j. \y. (j \ I \ y \ F j \ (i = j \ x = y)) \ (j \ I \ y = undefined)"
    by auto
  from choice[OF this] obtain f
    where f: " \j. (j \ I \ f j \ F j \ (i = j \ x = f j)) \ (j \ I \ f j = undefined)" ..
  then have "f \ Pi\<^sub>E I F"
    by (auto simp: extensional_def PiE_def)
  then have "f \ Pi\<^sub>E I F'"
    using assms by simp
  then show "x \ F' i"
    using f \<open>i \<in> I\<close> by (auto simp: PiE_def)
qed

lemma PiE_eq_iff_not_empty:
  assumes ne: "\i. i \ I \ F i \ {}" "\i. i \ I \ F' i \ {}"
  shows "Pi\<^sub>E I F = Pi\<^sub>E I F' \ (\i\I. F i = F' i)"
proof (intro iffI ballI)
  fix i
  assume eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
  assume i: "i \ I"
  show "F i = F' i"
    using PiE_eq_subset[of I F F', OF ne eq i]
    using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
    by auto
qed (auto simp: PiE_def)

lemma PiE_eq_iff:
  "Pi\<^sub>E I F = Pi\<^sub>E I F' \ (\i\I. F i = F' i) \ ((\i\I. F i = {}) \ (\i\I. F' i = {}))"
proof (intro iffI disjCI)
  assume eq[simp]: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
  assume "\ ((\i\I. F i = {}) \ (\i\I. F' i = {}))"
  then have "(\i\I. F i \ {}) \ (\i\I. F' i \ {})"
    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
  with PiE_eq_iff_not_empty[of I F F'] show "\i\I. F i = F' i"
    by auto
next
  assume "(\i\I. F i = F' i) \ (\i\I. F i = {}) \ (\i\I. F' i = {})"
  then show "Pi\<^sub>E I F = Pi\<^sub>E I F'"
    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
qed

lemma extensional_funcset_fun_upd_restricts_rangeI:
  "\y \ S. f x \ f y \ f \ (insert x S) \\<^sub>E T \ f(x := undefined) \ S \\<^sub>E (T - {f x})"
  unfolding extensional_funcset_def extensional_def
  apply auto
  apply (case_tac "x = xa")
  apply auto
  done

lemma extensional_funcset_fun_upd_extends_rangeI:
  assumes "a \ T" "f \ S \\<^sub>E (T - {a})"
  shows "f(x := a) \ insert x S \\<^sub>E T"
  using assms unfolding extensional_funcset_def extensional_def by auto

lemma subset_PiE:
   "PiE I S \ PiE I T \ PiE I S = {} \ (\i \ I. S i \ T i)" (is "?lhs \ _ \ ?rhs")
proof (cases "PiE I S = {}")
  case False
  moreover have "?lhs = ?rhs"
  proof
    assume L: ?lhs
    have "\i. i\I \ S i \ {}"
      using False PiE_eq_empty_iff by blast
    with L show ?rhs
      by (simp add: PiE_Int PiE_eq_iff inf.absorb_iff2)
  qed auto
  ultimately show ?thesis
    by simp
qed simp

lemma PiE_eq:
   "PiE I S = PiE I T \ PiE I S = {} \ PiE I T = {} \ (\i \ I. S i = T i)"
  by (auto simp: PiE_eq_iff PiE_eq_empty_iff)

lemma PiE_UNIV [simp]: "PiE UNIV (\i. UNIV) = UNIV"
  by blast

lemma image_projection_PiE:
  "(\f. f i) ` (PiE I S) = (if PiE I S = {} then {} else if i \ I then S i else {undefined})"
proof -
  have "(\f. f i) ` Pi\<^sub>E I S = S i" if "i \ I" "f \ PiE I S" for f
    using that apply auto
    by (rule_tac x="(\k. if k=i then x else f k)" in image_eqI) auto
  moreover have "(\f. f i) ` Pi\<^sub>E I S = {undefined}" if "f \ PiE I S" "i \ I" for f
    using that by (blast intro: PiE_arb [OF that, symmetric])
  ultimately show ?thesis
    by auto
qed

lemma PiE_singleton:
  assumes "f \ extensional A"
  shows   "PiE A (\x. {f x}) = {f}"
proof -
  {
    fix g assume "g \ PiE A (\x. {f x})"
    hence "g x = f x" for x
      using assms by (cases "x \ A") (auto simp: extensional_def)
    hence "g = f" by (simp add: fun_eq_iff)
  }
  thus ?thesis using assms by (auto simp: extensional_def)
qed

lemma PiE_eq_singleton: "(\\<^sub>E i\I. S i) = {\i\I. f i} \ (\i\I. S i = {f i})"
  by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)

lemma PiE_over_singleton_iff: "(\\<^sub>E x\{a}. B x) = (\b \ B a. {\x \ {a}. b})"
  apply (auto simp: PiE_iff split: if_split_asm)
  apply (metis (no_types, lifting) extensionalityI restrict_apply' restrict_extensional singletonD)
  done

lemma all_PiE_elements:
   "(\z \ PiE I S. \i \ I. P i (z i)) \ PiE I S = {} \ (\i \ I. \x \ S i. P i x)" (is "?lhs = ?rhs")
proof (cases "PiE I S = {}")
  case False
  then obtain f where f: "\i. i \ I \ f i \ S i"
    by fastforce
  show ?thesis
  proof
    assume L: ?lhs
    have "P i x"
      if "i \ I" "x \ S i" for i x
    proof -
      have "(\j \ I. if j=i then x else f j) \ PiE I S"
        by (simp add: f that(2))
      then have "P i ((\j \ I. if j=i then x else f j) i)"
        using L that(1) by blast
      with that show ?thesis
        by simp
    qed
    then show ?rhs
      by (simp add: False)
  qed fastforce
qed simp

lemma PiE_ext: "\x \ PiE k s; y \ PiE k s; \i. i \ k \ x i = y i\ \ x = y"
  by (metis ext PiE_E)

subsubsection \<open>Injective Extensional Function Spaces\<close>

lemma extensional_funcset_fun_upd_inj_onI:
  assumes "f \ S \\<^sub>E (T - {a})"
    and "inj_on f S"
  shows "inj_on (f(x := a)) S"
  using assms
  unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)

lemma extensional_funcset_extend_domain_inj_on_eq:
  assumes "x \ S"
  shows "{f. f \ (insert x S) \\<^sub>E T \ inj_on f (insert x S)} =
    (\<lambda>(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
  using assms
  apply (auto del: PiE_I PiE_E)
  apply (auto intro: extensional_funcset_fun_upd_inj_onI
    extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
  apply (auto simp add: image_iff inj_on_def)
  apply (rule_tac x="xa x" in exI)
  apply (auto intro: PiE_mem del: PiE_I PiE_E)
  apply (rule_tac x="xa(x := undefined)" in exI)
  apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
  apply (auto dest!: PiE_mem split: if_split_asm)
  done

lemma extensional_funcset_extend_domain_inj_onI:
  assumes "x \ S"
  shows "inj_on (\(y, g). g(x := y)) {(y, g). y \ T \ g \ S \\<^sub>E (T - {y}) \ inj_on g S}"
  using assms
  apply (auto intro!: inj_onI)
  apply (metis fun_upd_same)
  apply (metis assms PiE_arb fun_upd_triv fun_upd_upd)
  done

subsubsection \<open>Misc properties of functions, composition and restriction from HOL Light\<close>

lemma function_factors_left_gen:
  "(\x y. P x \ P y \ g x = g y \ f x = f y) \ (\h. \x. P x \ f x = h(g x))"
  (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then show ?rhs
    apply (rule_tac x="f \ inv_into (Collect P) g" in exI)
    unfolding o_def
    by (metis (mono_tags, hide_lams) f_inv_into_f imageI inv_into_into mem_Collect_eq)
qed auto

lemma function_factors_left:
  "(\x y. (g x = g y) \ (f x = f y)) \ (\h. f = h \ g)"
  using function_factors_left_gen [of "\x. True" g f] unfolding o_def by blast

lemma function_factors_right_gen:
  "(\x. P x \ (\y. g y = f x)) \ (\h. \x. P x \ f x = g(h x))"
  by metis

lemma function_factors_right:
  "(\x. \y. g y = f x) \ (\h. f = g \ h)"
  unfolding o_def by metis

lemma restrict_compose_right:
   "restrict (g \ restrict f S) S = restrict (g \ f) S"
  by auto

lemma restrict_compose_left:
   "f ` S \ T \ restrict (restrict g T \ f) S = restrict (g \ f) S"
  by fastforce

subsubsection \<open>Cardinality\<close>

lemma finite_PiE: "finite S \ (\i. i \ S \ finite (T i)) \ finite (\\<^sub>E i \ S. T i)"
  by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)

lemma inj_combinator: "x \ S \ inj_on (\(y, g). g(x := y)) (T x \ Pi\<^sub>E S T)"
proof (safe intro!: inj_onI ext)
  fix f y g z
  assume "x \ S"
  assume fg: "f \ Pi\<^sub>E S T" "g \ Pi\<^sub>E S T"
  assume "f(x := y) = g(x := z)"
  then have *: "\i. (f(x := y)) i = (g(x := z)) i"
    unfolding fun_eq_iff by auto
  from this[of x] show "y = z" by simp
  fix i from *[of i] \<open>x \<notin> S\<close> fg show "f i = g i"
    by (auto split: if_split_asm simp: PiE_def extensional_def)
qed

lemma card_PiE: "finite S \ card (\\<^sub>E i \ S. T i) = (\ i\S. card (T i))"
proof (induct rule: finite_induct)
  case empty
  then show ?case by auto
next
  case (insert x S)
  then show ?case
    by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
qed

subsection \<open>The pigeonhole principle\<close>

text \<open>
  An alternative formulation of this is that for a function mapping a finite set \<open>A\<close> of
  cardinality \<open>m\<close> to a finite set \<open>B\<close> of cardinality \<open>n\<close>, there exists an element \<open>y \<in> B\<close> that
  is hit at least $\lceil \frac{m}{n}\rceil$ times. However, since we do not have real numbers
  or rounding yet, we state it in the following equivalent form:
\<close>
lemma pigeonhole_card:
  assumes "f \ A \ B" "finite A" "finite B" "B \ {}"
  shows   "\y\B. card (f -` {y} \ A) * card B \ card A"
proof -
  from assms have "card B > 0"
    by auto
  define M where "M = Max ((\y. card (f -` {y} \ A)) ` B)"
  have "A = (\y\B. f -` {y} \ A)"
    using assms by auto
  also have "card \ = (\i\B. card (f -` {i} \ A))"
    using assms by (subst card_UN_disjoint) auto
  also have "\ \ (\i\B. M)"
    unfolding M_def using assms by (intro sum_mono Max.coboundedI) auto
  also have "\ = card B * M"
    by simp
  finally have "M * card B \ card A"
    by (simp add: mult_ac)
  moreover have "M \ (\y. card (f -` {y} \ A)) ` B"
    unfolding M_def using assms \<open>B \<noteq> {}\<close> by (intro Max_in) auto
  ultimately show ?thesis
    by blast
qed

end

¤ Dauer der Verarbeitung: 0.31 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.