Quelle FuncSet.thy Sprache: 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"
  where "funcset A B \ Pi A (\_. B)"

open_bundle funcset_syntax
begin
notation funcset  (infixr \<open>\<rightarrow>\<close> 60)
end

syntax
  "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set"
    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<in>\<close>\<close>\<Pi> _\<in>_./ _)\<close> 10)
  "_lam" :: "pttrn \ 'a set \ ('a \ 'b) \ ('a \ 'b)"
    (\<open>(\<open>indent=3 notation=\<open>binder \<lambda>\<in>\<close>\<close>\<lambda>_\<in>_./ _)\<close> [0, 0, 3] 3)
syntax_consts
  "_Pi" \<rightleftharpoons> Pi and
  "_lam" \<rightleftharpoons> restrict
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"
  using mk_disjoint_insert by fastforce

lemma fst_Pi: "fst \ A \ B \ A" and snd_Pi: "snd \ A \ B \ B"
  by auto

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 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 inj_on_restrict_iff: "A \ B \ inj_on (restrict f B) A \ inj_on f A"
  by (metis inj_on_cong restrict_def subset_iff)

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"
  by (simp add: bij_betw_def inj_on_compose surj_compose)

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)"
  by (smt (verit, best) bij_betwE bij_betw_inv_into_left compose_def restrict_apply' restrict_ext)

lemma compose_id_inv_into: "f ` A = B \ compose B f (\y\B. inv_into A f y) = (\x\B. x)"
  by (smt (verit, best) compose_def f_inv_into_f restrict_apply' restrict_ext)

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"
    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>E\<in>\<close>\<close>\<Pi>\<^sub>E _\<in>_./ _)\<close> 10)
syntax_consts
  "_PiE" \<rightleftharpoons> Pi\<^sub>E
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 -
  have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)" if "f \ Pi\<^sub>E (insert x S) T" "x \ S" for f
    using that
    by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
  moreover
  have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)" if "f \ Pi\<^sub>E (insert x S) T" "x \ S" for f
    using that
    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 restrict_PiE_iff: "restrict f I \ Pi\<^sub>E I X \ (\i \ I. f i \ X i)"
  by (simp add: PiE_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
  by (auto split: if_split_asm)

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
  proof -
    have "x \ S i \ \f\Pi\<^sub>E I S. x = f i" for x
      using that
      by (force intro: bexI [where x="\k. if k=i then x else f k"])
    then show ?thesis
      using that by force
  qed
  then show ?thesis
    by (smt (verit) PiE_arb equals0I image_cong image_constant image_empty)
qed

lemma PiE_singleton:
  assumes "f \ extensional A"
  shows "PiE A (\x. {f x}) = {f}"
proof -
  have "g = f" if "g \ PiE A (\x. {f x})" for g
  proof -
    from that have "g x = f x" for x
      using assms by (cases "x \ A") (auto simp: extensional_def)
    then show ?thesis by (simp add: fun_eq_iff)
  qed
  with assms show ?thesis
    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})"
proof -
  have "\xa\B a. x = (\x\{a}. xa)" if "x a \ B a" and "x \ extensional {a}" for x
    using that PiE_singleton by fastforce
  then show ?thesis
    by (auto simp: PiE_iff split: if_split_asm)
qed

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 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}"
proof -
  have False if "f \ S \\<^sub>E T - {a}" and "a = (if y = x then a else f y)" and "y \ S" for a f y
    using assms that by (auto dest!: PiE_mem split: if_split_asm)
  moreover
  have "\b. b \ S \\<^sub>E T - {f x} \ inj_on b S \ f = b(x := f x)"
    if "f \ insert x S \\<^sub>E T" and "inj_on f S" and "\xb\S. f x \ f xb" for f
    using that
    unfolding inj_on_def
    by (smt (verit, ccfv_threshold) PiE_restrict fun_upd_apply fun_upd_triv insert_Diff insert_iff
        restrict_PiE_iff restrict_upd)
  ultimately show ?thesis
    using assms
    apply (auto simp: image_iff  intro: extensional_funcset_fun_upd_inj_onI
        extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
    apply (smt (verit, best) PiE_cong PiE_mem inj_on_def insertCI)
    apply blast
    done
qed

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
  by (simp add: inj_on_def) (metis PiE_restrict fun_upd_apply restrict_fupd)

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, opaque_lifting) 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

lemma card_funcsetE: "finite A \ card (A \\<^sub>E B) = card B ^ card A"
  by (subst card_PiE) auto

lemma card_inj_on_subset_funcset:
  assumes finB: "finite B"
    and finC: "finite C"
    and AB: "A \ B"
  shows "card {f \ B \\<^sub>E C. inj_on f A} =
    card C^(card B - card A) * prod ((-) (card C)) {0 ..< card A}"
proof -
  define D where "D = B - A"
  from AB have B: "B = A \ D" and disj: "A \ D = {}"
    unfolding D_def by auto
  have sub: "card B - card A = card D"
    unfolding D_def using finB AB
    by (metis card_Diff_subset finite_subset)
  from finB B have "finite A" "finite D" by auto
  then show ?thesis
    unfolding sub unfolding B using disj
  proof (induct A rule: finite_induct)
    case empty
    from card_funcsetE[OF this(1), of C] show ?case
      by auto
  next
    case (insert a A)
    have "{f. f \ insert a A \ D \\<^sub>E C \ inj_on f (insert a A)} =
      {f(a := c) | f c. f \<in> A \<union> D \<rightarrow>\<^sub>E C \<and> inj_on f A \<and> c \<in> C - f ` A}"
      (is "?l = ?r")
    proof
      show "?r \ ?l"
        by (auto intro: inj_on_fun_updI split: if_splits)
      have "f \ ?r" if f: "f \ ?l" for f
      proof -
        let ?g = "f(a := undefined)"
        let ?h = "?g(a := f a)"
        have mem: "f a \ C - ?g ` A" using insert(1,2,4,5) f by auto
        from f have f: "f \ insert a A \ D \\<^sub>E C" "inj_on f (insert a A)" by auto
        hence "?g \ A \ D \\<^sub>E C" "inj_on ?g A" using \a \ A\ \insert a A \ D = {}\
          by (auto split: if_splits simp: inj_on_def)
        with mem have "?h \ ?r" by blast
        also have "?h = f" by auto
        finally show ?thesis .
      qed
      then show "?l \ ?r" by auto
    qed
    also have "\ = (\ (f, c). f (a := c)) `
         (Sigma {f . f \<in> A \<union> D \<rightarrow>\<^sub>E C \<and> inj_on f A} (\<lambda> f. C - f ` A))"
      by auto
    also have "card (...) = card (Sigma {f . f \ A \ D \\<^sub>E C \ inj_on f A} (\ f. C - f ` A))"
    proof (rule card_image, intro inj_onI, clarsimp, goal_cases)
      case (1 f c g d)
      let ?f = "f(a := c, a := undefined)"
      let ?g = "g(a := d, a := undefined)"
      from 1 have id: "f(a := c) = g(a := d)"
        by auto
      from fun_upd_eqD[OF id]
      have cd: "c = d"
        by auto
      from id have "?f = ?g"
        by auto
      also have "?f = f" using `f \<in> A \<union> D \<rightarrow>\<^sub>E C` insert(1,2,4,5)
        by (intro ext, auto)
      also have "?g = g" using `g \<in> A \<union> D \<rightarrow>\<^sub>E C` insert(1,2,4,5)
        by (intro ext, auto)
      finally show "f = g \ c = d"
        using cd by auto
    qed
    also have "\ = (\f\{f \ A \ D \\<^sub>E C. inj_on f A}. card (C - f ` A))"
      by (rule card_SigmaI, rule finite_subset[of _ "A \ D \\<^sub>E C"],
          insert \<open>finite C\<close> \<open>finite D\<close> \<open>finite A\<close>, auto intro!: finite_PiE)
    also have "\ = (\f\{f \ A \ D \\<^sub>E C. inj_on f A}. card C - card A)"
      by (rule sum.cong[OF refl], subst card_Diff_subset, insert \<open>finite A\<close>, auto simp: card_image)
    also have "\ = (card C - card A) * card {f \ A \ D \\<^sub>E C. inj_on f A}"
      by simp
    also have "\ = card C ^ card D * ((card C - card A) * prod ((-) (card C)) {0..
      using insert by (auto simp: ac_simps)
    also have "(card C - card A) * prod ((-) (card C)) {0..
      prod ((-) (card C)) {0..<Suc (card A)}" by simp
    also have "Suc (card A) = card (insert a A)" using insert by auto
    finally show ?case .
  qed
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)
  from assms have "M \ (\y. card (f -` {y} \ A)) ` B"
    unfolding M_def by (intro Max_in) auto
  with * show ?thesis
    by blast
qed

subsection \<open>Products of sums\<close>

lemma prod_sum_PiE:
  fixes f :: "'a \ 'b \ 'c :: comm_semiring_1"
  assumes finite: "finite A" and finite: "\x. x \ A \ finite (B x)"
  shows   "(\x\A. \y\B x. f x y) = (\g\PiE A B. \x\A. f x (g x))"
  using assms
proof (induction A rule: finite_induct)
  case empty
  thus ?case by auto
next
  case (insert x A)
  have "(\g\Pi\<^sub>E (insert x A) B. \x\insert x A. f x (g x)) =
          (\<Sum>g\<in>Pi\<^sub>E (insert x A) B. f x (g x) * (\<Prod>x'\<in>A. f x' (g x')))"
    using insert by simp
  also have "(\g. \x'\A. f x' (g x')) = (\g. \x'\A. f x' (if x' = x then undefined else g x'))"
    using insert by (intro ext prod.cong) auto
  also have "(\g\Pi\<^sub>E (insert x A) B. f x (g x) * \ g) =
               (\<Sum>(y,g)\<in>B x \<times> Pi\<^sub>E A B. f x y * (\<Prod>x'\<in>A. f x' (g x')))"
    using insert.prems insert.hyps
    by (intro sum.reindex_bij_witness[of _ "\(y,g). g(x := y)" "\g. (g x, g(x := undefined))"])
       (auto simp: PiE_def extensional_def)
  also have "\ = (\y\B x. \g\Pi\<^sub>E A B. f x y * (\x'\A. f x' (g x')))"
    by (subst sum.cartesian_product) auto
  also have "\ = (\y\B x. f x y) * (\g\Pi\<^sub>E A B. \x'\A. f x' (g x'))"
    using insert by (subst sum.swap) (simp add: sum_distrib_left sum_distrib_right)
  also have "(\g\Pi\<^sub>E A B. \x'\A. f x' (g x')) = (\x\A. \y\B x. f x y)"
    using insert.prems by (intro insert.IH [symmetric]) auto
  also have "(\y\B x. f x y) * \ = (\x\insert x A. \y\B x. f x y)"
    using insert.hyps by simp
  finally show ?case ..
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

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.