# HG changeset patch # User wenzelm # Date 1414264592 -7200 # Node ID c6348a0621311e1cf9ec5c30b422cf3e98594f0f # Parent 7305bad408b5132261388b8fbf690cab487c4de7 tuned whitespace; more symbols; diff -r 7305bad408b5 -r c6348a062131 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Sat Oct 25 11:53:35 2014 +0200 +++ b/src/HOL/Library/FuncSet.thy Sat Oct 25 21:16:32 2014 +0200 @@ -2,144 +2,143 @@ Author: Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn *) -header {* Pi and Function Sets *} +header \Pi and Function Sets\ theory FuncSet imports Hilbert_Choice Main begin -definition - Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where - "Pi A B = {f. \x. x \ A --> f x \ B x}" +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 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)" +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)" +abbreviation funcset :: "'a set \ 'b set \ ('a \ 'b) set" (infixr "->" 60) + where "A -> B \ Pi A (\_. B)" notation (xsymbols) funcset (infixr "\" 60) syntax - "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10) - "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3) - + "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PI _:_./ _)" 10) + "_lam" :: "pttrn \ 'a set \ 'a \ 'b \ ('a \ 'b)" ("(3%_:_./ _)" [0,0,3] 3) syntax (xsymbols) - "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\ _\_./ _)" 10) - "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\_\_./ _)" [0,0,3] 3) - + "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\ _\_./ _)" 10) + "_lam" :: "pttrn \ 'a set \ ('a \ 'b) \ ('a \ 'b)" ("(3\_\_./ _)" [0,0,3] 3) syntax (HTML output) - "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\ _\_./ _)" 10) - "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\_\_./ _)" [0,0,3] 3) - + "_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 - "PI x:A. B" \ "CONST Pi A (%x. B)" - "%x:A. f" \ "CONST restrict (%x. f) A" + "\ 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))" +definition "compose" :: "'a set \ ('b \ 'c) \ ('a \ 'b) \ ('a \ 'c)" + where "compose A g f = (\x\A. g (f x))" -subsection{*Basic Properties of @{term Pi}*} +subsection \Basic Properties of @{term Pi}\ -lemma Pi_I[intro!]: "(!!x. x \ A ==> f x \ B x) ==> f \ Pi A B" +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 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" +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" +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 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" +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" +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" +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 Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\x\A. B x = {})" -apply (simp add: Pi_def, auto) -txt{*Converse direction requires Axiom of Choice to exhibit a function -picking an element from each non-empty @{term "B x"}*} -apply (drule_tac x = "%u. SOME y. y \ B u" in spec, auto) -apply (cut_tac P= "%y. y \ B x" in some_eq_ex, auto) -done +lemma Pi_eq_empty[simp]: "(\ x \ A. B x) = {} \ (\x\A. B x = {})" + apply (simp add: Pi_def) + apply auto + txt \Converse direction requires Axiom of Choice to exhibit a function + picking an element from each non-empty @{term "B x"}\ + apply (drule_tac x = "\u. SOME y. y \ B u" in spec) + apply auto + apply (cut_tac P = "\y. y \ B x" in some_eq_ex) + apply auto + done lemma Pi_empty [simp]: "Pi {} B = UNIV" -by (simp add: Pi_def) + 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" + 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: "\i. i \ I \ f i \ (A (n i) i)" by auto + 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: "\i. i \ I \ f i \ (A (n i) i)" + by auto obtain k where k: "\i. i \ I \ n i \ k" - using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto + using \finite I\ 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" + 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 + then show "f \ (\n. Pi I (A n))" + by auto qed auto -lemma Pi_UNIV [simp]: "A -> UNIV = UNIV" -by (simp add: Pi_def) +lemma Pi_UNIV [simp]: "A \ UNIV = UNIV" + by (simp add: Pi_def) -text{*Covariance of Pi-sets in their second argument*} -lemma Pi_mono: "(!!x. x \ A ==> B x <= C x) ==> Pi A B <= Pi A C" -by auto +text \Covariance of Pi-sets in their second argument\ +lemma Pi_mono: "(\x. x \ A \ B x \ C x) \ Pi A B \ Pi A C" + by auto -text{*Contravariance of Pi-sets in their first argument*} -lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" -by auto +text \Contravariance of Pi-sets in their first argument\ +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" + 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) +proof (rule Pi_I) fix z - assume z: "z \ A" - have "f z = (fst (f z), snd (f 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) + also have "\ \ B z \ C z" + by (metis SigmaI PiE o_apply 1 2 z) finally show "f z \ B z \ C z" . qed @@ -163,25 +162,27 @@ apply (auto dest!: Pi_mem) done -subsection{*Composition With a Restricted Domain: @{term compose}*} + +subsection \Composition With a Restricted Domain: @{term compose}\ -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 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: - "[| f \ A -> B; g \ B -> C; h \ C -> D |] - ==> compose A h (compose A g f) = compose A (compose B h g) f" -by (simp add: fun_eq_iff Pi_def compose_def restrict_def) + assumes "f \ A \ B" + and "g \ B \ C" + and "h \ C \ D" + 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 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" +lemma surj_compose: "f ` A = B \ g ` B = C \ compose A g f ` A = C" by (auto simp add: image_def compose_eq) -subsection{*Bounded Abstraction: @{term restrict}*} +subsection \Bounded Abstraction: @{term restrict}\ lemma restrict_in_funcset: "(\x. x \ A \ f x \ B) \ (\x\A. f x) \ A \ B" by (simp add: Pi_def restrict_def) @@ -195,8 +196,7 @@ 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)" +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" @@ -205,12 +205,10 @@ 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" +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" +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" @@ -222,99 +220,99 @@ 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)" +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) -subsection{*Bijections Between Sets*} +subsection \Bijections Between Sets\ -text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of -the theorems belong here, or need at least @{term Hilbert_Choice}.*} +text \The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of +the theorems belong here, or need at least @{term Hilbert_Choice}.\ 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 + 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) -next - have "f ` A \ B" using `f \ A \ B` by auto + show "inj_on f A" + by (metis g_f inj_on_def) + have "f ` A \ B" + using \f \ A \ B\ by auto moreover - have "B \ f ` A" by auto (metis Pi_mem `g \ B \ A` f_g image_iff) - ultimately show "f ` A = B" by blast + have "B \ f ` A" + by auto (metis Pi_mem \g \ B \ A\ 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) + 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 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_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) +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{*Extensionality*} +subsection \Extensionality\ 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 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) + by (simp add: restrict_def extensional_def) lemma compose_extensional [simp]: "compose A f g \ extensional A" -by (simp add: compose_def) + by (simp add: compose_def) lemma extensionalityI: - "[| f \ extensional A; g \ extensional A; - !!x. x\A ==> f x = g x |] ==> f = g" -by (force simp add: fun_eq_iff extensional_def) + 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 + 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 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_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 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')" +lemma extensional_Int[simp]: "extensional I \ extensional I' = extensional (I \ I')" unfolding extensional_def by auto lemma extensional_UNIV[simp]: "extensional UNIV = UNIV" @@ -332,61 +330,66 @@ unfolding extensional_def by auto -subsection{*Cardinality*} +subsection \Cardinality\ -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_inj: "f \ A \ B \ inj_on f A \ finite B \ card A \ card B" + by (rule card_inj_on_le) auto lemma card_bij: - "[|f \ A\B; inj_on f A; - g \ B\A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)" -by (blast intro: card_inj order_antisym) + 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 {* Extensional Function Spaces *} + +subsection \Extensional Function Spaces\ -definition PiE :: "'a set \ ('a \ 'b set) \ ('a \ 'b) set" where - "PiE S T = Pi S T \ extensional S" +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" ("(3PIE _:_./ _)" 10) - -syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^sub>E _\_./ _)" 10) +syntax + "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PIE _:_./ _)" 10) +syntax (xsymbols) + "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\\<^sub>E _\_./ _)" 10) +syntax (HTML output) + "_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)" -syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^sub>E _\_./ _)" 10) - -translations "PIE 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)" +abbreviation extensional_funcset :: "'a set \ 'b set \ ('a \ 'b) set" (infixr "->\<^sub>E" 60) + where "A ->\<^sub>E B \ (\\<^sub>E i\A. B)" notation (xsymbols) extensional_funcset (infixr "\\<^sub>E" 60) -lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) \ extensional S" +lemma extensional_funcset_def: "extensional_funcset S T = (S \ T) \ extensional S" by (simp add: PiE_def) -lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}" +lemma PiE_empty_domain[simp]: "PiE {} T = {\x. undefined}" unfolding PiE_def by simp lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T" unfolding PiE_def by simp -lemma PiE_empty_range[simp]: "i \ I \ F i = {} \ (PIE i:I. F i) = {}" +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 = {})" +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 + 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 `Pi\<^sub>E I F = {}` show False by auto + then have "f \ Pi\<^sub>E I F" + by (auto simp: extensional_def PiE_def) + with \Pi\<^sub>E I F = {}\ show False + by auto qed qed (auto simp: PiE_def) @@ -411,21 +414,24 @@ with assms have "f \ (\(y, g). g(x := y)) ` (T x \ PiE S T)" by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem) } - then show ?thesis using assms by (auto intro: PiE_fun_upd) + then show ?thesis + using assms 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)" +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" +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]: - "f \ PiE A B \ (x \ A \ f x \ B x \ Q) \ (x \ A \ f x = undefined \ Q) \ Q" -by(auto simp: Pi_def PiE_def extensional_def) + assumes "f \ PiE 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 \ PiE A B" +lemma PiE_I[intro!]: + "(\x. x \ A \ f x \ B x) \ (\x. x \ A \ f x = undefined) \ f \ PiE A B" by (simp add: PiE_def extensional_def) lemma PiE_mono: "(\x. x \ A \ B x \ C x) \ PiE A B \ PiE A C" @@ -442,24 +448,31 @@ lemma PiE_eq_subset: assumes ne: "\i. i \ I \ F i \ {}" "\i. i \ I \ F' i \ {}" - assumes eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'" and "i \ 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))" + 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 `i \ I` by (auto simp: PiE_def) + 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 \i \ I\ 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'" and i: "i \ I" + 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] @@ -473,15 +486,16 @@ 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 + 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})" +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") @@ -490,66 +504,70 @@ 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" + shows "f(x := a) \ insert x S \\<^sub>E T" using assms unfolding extensional_funcset_def extensional_def by auto -subsubsection {* Injective Extensional Function Spaces *} + +subsubsection \Injective Extensional Function Spaces\ lemma extensional_funcset_fun_upd_inj_onI: - assumes "f \ S \\<^sub>E (T - {a})" "inj_on f S" + 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) + 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)} = - (%(y, g). g(x:=y)) ` {(y, g). y \ T \ g \ S \\<^sub>E (T - {y}) \ inj_on g S}" -proof - - from assms show ?thesis - 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: split_if_asm) - done -qed + shows "{f. f \ (insert x S) \\<^sub>E T \ inj_on f (insert x S)} = + (\(y, g). g(x:=y)) ` {(y, g). y \ T \ g \ S \\<^sub>E (T - {y}) \ 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: split_if_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}" -proof - - from assms show ?thesis - apply (auto intro!: inj_onI) - apply (metis fun_upd_same) - by (metis assms PiE_arb fun_upd_triv fun_upd_upd) -qed - + 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 {* Cardinality *} -lemma finite_PiE: "finite S \ (\i. i \ S \ finite (T i)) \ finite (PIE i : S. T i)" +subsubsection \Cardinality\ + +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" and fg: "f \ Pi\<^sub>E S T" "g \ Pi\<^sub>E S T" + 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] `x \ S` fg show "f i = g i" + fix i from *[of i] \x \ S\ fg show "f i = g i" by (auto split: split_if_asm simp: PiE_def extensional_def) qed -lemma card_PiE: - "finite S \ card (PIE i : S. T i) = (\ i\S. card (T i))" +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 + case empty + then show ?case by auto next - case (insert x S) then show ?case + case (insert x S) + then show ?case by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product) qed