author | wenzelm |
Tue, 17 Jan 2017 11:26:21 +0100 | |
changeset 64910 | 6108dddad9f0 |
parent 63092 | a949b2a5f51d |
child 64917 | 5db5b8cf6dc6 |
permissions | -rw-r--r-- |
13586 | 1 |
(* Title: HOL/Library/FuncSet.thy |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
2 |
Author: Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn |
13586 | 3 |
*) |
4 |
||
58881 | 5 |
section \<open>Pi and Function Sets\<close> |
13586 | 6 |
|
15131 | 7 |
theory FuncSet |
64910 | 8 |
imports Hilbert_Choice Main |
9 |
abbrevs PiE = "Pi\<^sub>E" |
|
10 |
PIE = "\<Pi>\<^sub>E" |
|
15131 | 11 |
begin |
13586 | 12 |
|
58783 | 13 |
definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
14 |
where "Pi A B = {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x}" |
|
13586 | 15 |
|
58783 | 16 |
definition extensional :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" |
17 |
where "extensional A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = undefined}" |
|
13586 | 18 |
|
58783 | 19 |
definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" |
20 |
where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)" |
|
13586 | 21 |
|
61384 | 22 |
abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>" 60) |
23 |
where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)" |
|
19536 | 24 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
25 |
syntax (ASCII) |
58783 | 26 |
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PI _:_./ _)" 10) |
27 |
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3%_:_./ _)" [0,0,3] 3) |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
28 |
syntax |
58783 | 29 |
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi> _\<in>_./ _)" 10) |
30 |
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3) |
|
13586 | 31 |
translations |
58783 | 32 |
"\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)" |
33 |
"\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A" |
|
13586 | 34 |
|
58783 | 35 |
definition "compose" :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c)" |
36 |
where "compose A g f = (\<lambda>x\<in>A. g (f x))" |
|
13586 | 37 |
|
38 |
||
58783 | 39 |
subsection \<open>Basic Properties of @{term Pi}\<close> |
13586 | 40 |
|
58783 | 41 |
lemma Pi_I[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B" |
14706 | 42 |
by (simp add: Pi_def) |
13586 | 43 |
|
58783 | 44 |
lemma Pi_I'[simp]: "(\<And>x. x \<in> A \<longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B" |
45 |
by (simp add:Pi_def) |
|
31731 | 46 |
|
58783 | 47 |
lemma funcsetI: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f \<in> A \<rightarrow> B" |
14706 | 48 |
by (simp add: Pi_def) |
13586 | 49 |
|
58783 | 50 |
lemma Pi_mem: "f \<in> Pi A B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B x" |
14706 | 51 |
by (simp add: Pi_def) |
13586 | 52 |
|
47761 | 53 |
lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)" |
54 |
unfolding Pi_def by auto |
|
55 |
||
58783 | 56 |
lemma PiE [elim]: "f \<in> Pi A B \<Longrightarrow> (f x \<in> B x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> Q" |
57 |
by (auto simp: Pi_def) |
|
31754 | 58 |
|
58783 | 59 |
lemma Pi_cong: "(\<And>w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B" |
38656 | 60 |
by (auto simp: Pi_def) |
61 |
||
31769 | 62 |
lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" |
44382 | 63 |
by auto |
31769 | 64 |
|
58783 | 65 |
lemma funcset_mem: "f \<in> A \<rightarrow> B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B" |
14706 | 66 |
by (simp add: Pi_def) |
13586 | 67 |
|
58783 | 68 |
lemma funcset_image: "f \<in> A \<rightarrow> B \<Longrightarrow> f ` A \<subseteq> B" |
50104 | 69 |
by auto |
70 |
||
71 |
lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B" |
|
72 |
by auto |
|
14762 | 73 |
|
58783 | 74 |
lemma Pi_eq_empty[simp]: "(\<Pi> x \<in> A. B x) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})" |
75 |
apply (simp add: Pi_def) |
|
76 |
apply auto |
|
77 |
txt \<open>Converse direction requires Axiom of Choice to exhibit a function |
|
78 |
picking an element from each non-empty @{term "B x"}\<close> |
|
79 |
apply (drule_tac x = "\<lambda>u. SOME y. y \<in> B u" in spec) |
|
80 |
apply auto |
|
81 |
apply (cut_tac P = "\<lambda>y. y \<in> B x" in some_eq_ex) |
|
82 |
apply auto |
|
83 |
done |
|
13586 | 84 |
|
13593 | 85 |
lemma Pi_empty [simp]: "Pi {} B = UNIV" |
58783 | 86 |
by (simp add: Pi_def) |
13593 | 87 |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
88 |
lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
89 |
by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
90 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
91 |
lemma Pi_UN: |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
92 |
fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set" |
58783 | 93 |
assumes "finite I" |
94 |
and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
95 |
shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
96 |
proof (intro set_eqI iffI) |
58783 | 97 |
fix f |
98 |
assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)" |
|
99 |
then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" |
|
100 |
by auto |
|
63060 | 101 |
from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i |
58783 | 102 |
by auto |
63060 | 103 |
obtain k where k: "n i \<le> k" if "i \<in> I" for i |
58783 | 104 |
using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
105 |
have "f \<in> Pi I (A k)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
106 |
proof (intro Pi_I) |
58783 | 107 |
fix i |
108 |
assume "i \<in> I" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
109 |
from mono[OF this, of "n i" k] k[OF this] n[OF this] |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
110 |
show "f i \<in> A k i" by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
111 |
qed |
58783 | 112 |
then show "f \<in> (\<Union>n. Pi I (A n))" |
113 |
by auto |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
114 |
qed auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
115 |
|
58783 | 116 |
lemma Pi_UNIV [simp]: "A \<rightarrow> UNIV = UNIV" |
117 |
by (simp add: Pi_def) |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
118 |
|
58783 | 119 |
text \<open>Covariance of Pi-sets in their second argument\<close> |
120 |
lemma Pi_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi A B \<subseteq> Pi A C" |
|
121 |
by auto |
|
13586 | 122 |
|
58783 | 123 |
text \<open>Contravariance of Pi-sets in their first argument\<close> |
124 |
lemma Pi_anti_mono: "A' \<subseteq> A \<Longrightarrow> Pi A B \<subseteq> Pi A' B" |
|
125 |
by auto |
|
13586 | 126 |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset
|
127 |
lemma prod_final: |
58783 | 128 |
assumes 1: "fst \<circ> f \<in> Pi A B" |
129 |
and 2: "snd \<circ> f \<in> Pi A C" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset
|
130 |
shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)" |
58783 | 131 |
proof (rule Pi_I) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset
|
132 |
fix z |
58783 | 133 |
assume z: "z \<in> A" |
134 |
have "f z = (fst (f z), snd (f z))" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset
|
135 |
by simp |
58783 | 136 |
also have "\<dots> \<in> B z \<times> C z" |
137 |
by (metis SigmaI PiE o_apply 1 2 z) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset
|
138 |
finally show "f z \<in> B z \<times> C z" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset
|
139 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset
|
140 |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
141 |
lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
142 |
by (auto simp: Pi_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
143 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
144 |
lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
145 |
by (auto simp: Pi_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
146 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
147 |
lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
148 |
by (auto simp: Pi_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
149 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
150 |
lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
151 |
by (auto simp: Pi_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
152 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
153 |
lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
154 |
apply auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
155 |
apply (drule_tac x=x in Pi_mem) |
62390 | 156 |
apply (simp_all split: if_split_asm) |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
157 |
apply (drule_tac x=i in Pi_mem) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
158 |
apply (auto dest!: Pi_mem) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
159 |
done |
13586 | 160 |
|
58783 | 161 |
|
162 |
subsection \<open>Composition With a Restricted Domain: @{term compose}\<close> |
|
13586 | 163 |
|
58783 | 164 |
lemma funcset_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> g \<in> B \<rightarrow> C \<Longrightarrow> compose A g f \<in> A \<rightarrow> C" |
165 |
by (simp add: Pi_def compose_def restrict_def) |
|
13586 | 166 |
|
167 |
lemma compose_assoc: |
|
58783 | 168 |
assumes "f \<in> A \<rightarrow> B" |
169 |
and "g \<in> B \<rightarrow> C" |
|
170 |
and "h \<in> C \<rightarrow> D" |
|
171 |
shows "compose A h (compose A g f) = compose A (compose B h g) f" |
|
172 |
using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def) |
|
13586 | 173 |
|
58783 | 174 |
lemma compose_eq: "x \<in> A \<Longrightarrow> compose A g f x = g (f x)" |
175 |
by (simp add: compose_def restrict_def) |
|
13586 | 176 |
|
58783 | 177 |
lemma surj_compose: "f ` A = B \<Longrightarrow> g ` B = C \<Longrightarrow> compose A g f ` A = C" |
14706 | 178 |
by (auto simp add: image_def compose_eq) |
13586 | 179 |
|
180 |
||
58783 | 181 |
subsection \<open>Bounded Abstraction: @{term restrict}\<close> |
13586 | 182 |
|
61359
e985b52c3eb3
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
hoelzl
parents:
59425
diff
changeset
|
183 |
lemma restrict_cong: "I = J \<Longrightarrow> (\<And>i. i \<in> J =simp=> f i = g i) \<Longrightarrow> restrict f I = restrict g J" |
e985b52c3eb3
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
hoelzl
parents:
59425
diff
changeset
|
184 |
by (auto simp: restrict_def fun_eq_iff simp_implies_def) |
e985b52c3eb3
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
hoelzl
parents:
59425
diff
changeset
|
185 |
|
54417 | 186 |
lemma restrict_in_funcset: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> A \<rightarrow> B" |
14706 | 187 |
by (simp add: Pi_def restrict_def) |
13586 | 188 |
|
54417 | 189 |
lemma restrictI[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> Pi A B" |
14706 | 190 |
by (simp add: Pi_def restrict_def) |
13586 | 191 |
|
54417 | 192 |
lemma restrict_apply[simp]: "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)" |
14706 | 193 |
by (simp add: restrict_def) |
13586 | 194 |
|
54417 | 195 |
lemma restrict_apply': "x \<in> A \<Longrightarrow> (\<lambda>y\<in>A. f y) x = f x" |
196 |
by simp |
|
197 |
||
58783 | 198 |
lemma restrict_ext: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
199 |
by (simp add: fun_eq_iff Pi_def restrict_def) |
13586 | 200 |
|
58606 | 201 |
lemma restrict_UNIV: "restrict f UNIV = f" |
202 |
by (simp add: restrict_def) |
|
203 |
||
14853 | 204 |
lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A" |
14706 | 205 |
by (simp add: inj_on_def restrict_def) |
13586 | 206 |
|
58783 | 207 |
lemma Id_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> f \<in> extensional A \<Longrightarrow> compose A (\<lambda>y\<in>B. y) f = f" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
208 |
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def) |
13586 | 209 |
|
58783 | 210 |
lemma compose_Id: "g \<in> A \<rightarrow> B \<Longrightarrow> g \<in> extensional A \<Longrightarrow> compose A g (\<lambda>x\<in>A. x) = g" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
211 |
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def) |
13586 | 212 |
|
14853 | 213 |
lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A" |
19736 | 214 |
by (auto simp add: restrict_def) |
13586 | 215 |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
216 |
lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
217 |
unfolding restrict_def by (simp add: fun_eq_iff) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
218 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
219 |
lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
220 |
by (auto simp: restrict_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
221 |
|
58783 | 222 |
lemma restrict_upd[simp]: "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
223 |
by (auto simp: fun_eq_iff) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
224 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
225 |
lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
226 |
by (auto simp: restrict_def Pi_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
227 |
|
14745 | 228 |
|
58783 | 229 |
subsection \<open>Bijections Between Sets\<close> |
14762 | 230 |
|
61585 | 231 |
text \<open>The definition of @{const bij_betw} is in \<open>Fun.thy\<close>, but most of |
58783 | 232 |
the theorems belong here, or need at least @{term Hilbert_Choice}.\<close> |
14762 | 233 |
|
39595 | 234 |
lemma bij_betwI: |
58783 | 235 |
assumes "f \<in> A \<rightarrow> B" |
236 |
and "g \<in> B \<rightarrow> A" |
|
237 |
and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x" |
|
238 |
and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y" |
|
239 |
shows "bij_betw f A B" |
|
240 |
unfolding bij_betw_def |
|
39595 | 241 |
proof |
58783 | 242 |
show "inj_on f A" |
243 |
by (metis g_f inj_on_def) |
|
244 |
have "f ` A \<subseteq> B" |
|
245 |
using \<open>f \<in> A \<rightarrow> B\<close> by auto |
|
39595 | 246 |
moreover |
58783 | 247 |
have "B \<subseteq> f ` A" |
248 |
by auto (metis Pi_mem \<open>g \<in> B \<rightarrow> A\<close> f_g image_iff) |
|
249 |
ultimately show "f ` A = B" |
|
250 |
by blast |
|
39595 | 251 |
qed |
252 |
||
14762 | 253 |
lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B" |
58783 | 254 |
by (auto simp add: bij_betw_def) |
14762 | 255 |
|
58783 | 256 |
lemma inj_on_compose: "bij_betw f A B \<Longrightarrow> inj_on g B \<Longrightarrow> inj_on (compose A g f) A" |
257 |
by (auto simp add: bij_betw_def inj_on_def compose_eq) |
|
14853 | 258 |
|
58783 | 259 |
lemma bij_betw_compose: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (compose A g f) A C" |
260 |
apply (simp add: bij_betw_def compose_eq inj_on_compose) |
|
261 |
apply (auto simp add: compose_def image_def) |
|
262 |
done |
|
14762 | 263 |
|
58783 | 264 |
lemma bij_betw_restrict_eq [simp]: "bij_betw (restrict f A) A B = bij_betw f A B" |
265 |
by (simp add: bij_betw_def) |
|
14853 | 266 |
|
267 |
||
58783 | 268 |
subsection \<open>Extensionality\<close> |
14853 | 269 |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
270 |
lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
271 |
unfolding extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
272 |
|
58783 | 273 |
lemma extensional_arb: "f \<in> extensional A \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = undefined" |
274 |
by (simp add: extensional_def) |
|
14853 | 275 |
|
276 |
lemma restrict_extensional [simp]: "restrict f A \<in> extensional A" |
|
58783 | 277 |
by (simp add: restrict_def extensional_def) |
14853 | 278 |
|
279 |
lemma compose_extensional [simp]: "compose A f g \<in> extensional A" |
|
58783 | 280 |
by (simp add: compose_def) |
14853 | 281 |
|
282 |
lemma extensionalityI: |
|
58783 | 283 |
assumes "f \<in> extensional A" |
284 |
and "g \<in> extensional A" |
|
285 |
and "\<And>x. x \<in> A \<Longrightarrow> f x = g x" |
|
286 |
shows "f = g" |
|
287 |
using assms by (force simp add: fun_eq_iff extensional_def) |
|
14853 | 288 |
|
39595 | 289 |
lemma extensional_restrict: "f \<in> extensional A \<Longrightarrow> restrict f A = f" |
58783 | 290 |
by (rule extensionalityI[OF restrict_extensional]) auto |
39595 | 291 |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
292 |
lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
293 |
unfolding extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
294 |
|
58783 | 295 |
lemma inv_into_funcset: "f ` A = B \<Longrightarrow> (\<lambda>x\<in>B. inv_into A f x) \<in> B \<rightarrow> A" |
296 |
by (unfold inv_into_def) (fast intro: someI2) |
|
14853 | 297 |
|
58783 | 298 |
lemma compose_inv_into_id: "bij_betw f A B \<Longrightarrow> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)" |
299 |
apply (simp add: bij_betw_def compose_def) |
|
300 |
apply (rule restrict_ext, auto) |
|
301 |
done |
|
14853 | 302 |
|
58783 | 303 |
lemma compose_id_inv_into: "f ` A = B \<Longrightarrow> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)" |
304 |
apply (simp add: compose_def) |
|
305 |
apply (rule restrict_ext) |
|
306 |
apply (simp add: f_inv_into_f) |
|
307 |
done |
|
14853 | 308 |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
309 |
lemma extensional_insert[intro, simp]: |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
310 |
assumes "a \<in> extensional (insert i I)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
311 |
shows "a(i := b) \<in> extensional (insert i I)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
312 |
using assms unfolding extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
313 |
|
58783 | 314 |
lemma extensional_Int[simp]: "extensional I \<inter> extensional I' = extensional (I \<inter> I')" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
315 |
unfolding extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
316 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
317 |
lemma extensional_UNIV[simp]: "extensional UNIV = UNIV" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
318 |
by (auto simp: extensional_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
319 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
320 |
lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
321 |
unfolding restrict_def extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
322 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
323 |
lemma extensional_insert_undefined[intro, simp]: |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
324 |
"a \<in> extensional (insert i I) \<Longrightarrow> a(i := undefined) \<in> extensional I" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
325 |
unfolding extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
326 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
327 |
lemma extensional_insert_cancel[intro, simp]: |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
328 |
"a \<in> extensional I \<Longrightarrow> a \<in> extensional (insert i I)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
329 |
unfolding extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
330 |
|
14762 | 331 |
|
58783 | 332 |
subsection \<open>Cardinality\<close> |
14745 | 333 |
|
58783 | 334 |
lemma card_inj: "f \<in> A \<rightarrow> B \<Longrightarrow> inj_on f A \<Longrightarrow> finite B \<Longrightarrow> card A \<le> card B" |
335 |
by (rule card_inj_on_le) auto |
|
14745 | 336 |
|
337 |
lemma card_bij: |
|
58783 | 338 |
assumes "f \<in> A \<rightarrow> B" "inj_on f A" |
339 |
and "g \<in> B \<rightarrow> A" "inj_on g B" |
|
340 |
and "finite A" "finite B" |
|
341 |
shows "card A = card B" |
|
342 |
using assms by (blast intro: card_inj order_antisym) |
|
14745 | 343 |
|
58783 | 344 |
|
345 |
subsection \<open>Extensional Function Spaces\<close> |
|
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
346 |
|
58783 | 347 |
definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" |
348 |
where "PiE S T = Pi S T \<inter> extensional S" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
349 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
350 |
abbreviation "Pi\<^sub>E A B \<equiv> PiE A B" |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
351 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
352 |
syntax (ASCII) |
58783 | 353 |
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10) |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
354 |
syntax |
58783 | 355 |
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10) |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
356 |
translations |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
357 |
"\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
358 |
|
61384 | 359 |
abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60) |
360 |
where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)" |
|
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
361 |
|
58783 | 362 |
lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
363 |
by (simp add: PiE_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
364 |
|
64910 | 365 |
lemma PiE_empty_domain[simp]: "Pi\<^sub>E {} T = {\<lambda>x. undefined}" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
366 |
unfolding PiE_def by simp |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
367 |
|
64910 | 368 |
lemma PiE_UNIV_domain: "Pi\<^sub>E UNIV T = Pi UNIV T" |
54417 | 369 |
unfolding PiE_def by simp |
370 |
||
58783 | 371 |
lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (\<Pi>\<^sub>E i\<in>I. F i) = {}" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
372 |
unfolding PiE_def by auto |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
373 |
|
58783 | 374 |
lemma PiE_eq_empty_iff: "Pi\<^sub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
375 |
proof |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
376 |
assume "Pi\<^sub>E I F = {}" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
377 |
show "\<exists>i\<in>I. F i = {}" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
378 |
proof (rule ccontr) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
379 |
assume "\<not> ?thesis" |
58783 | 380 |
then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" |
381 |
by auto |
|
53381 | 382 |
from choice[OF this] |
383 |
obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" .. |
|
58783 | 384 |
then have "f \<in> Pi\<^sub>E I F" |
385 |
by (auto simp: extensional_def PiE_def) |
|
386 |
with \<open>Pi\<^sub>E I F = {}\<close> show False |
|
387 |
by auto |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
388 |
qed |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
389 |
qed (auto simp: PiE_def) |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
390 |
|
64910 | 391 |
lemma PiE_arb: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
392 |
unfolding PiE_def by auto (auto dest!: extensional_arb) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
393 |
|
64910 | 394 |
lemma PiE_mem: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
395 |
unfolding PiE_def by auto |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
396 |
|
64910 | 397 |
lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> Pi\<^sub>E S T \<Longrightarrow> f(x := y) \<in> Pi\<^sub>E (insert x S) T" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
398 |
unfolding PiE_def extensional_def by auto |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
399 |
|
64910 | 400 |
lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> Pi\<^sub>E (insert x S) T \<Longrightarrow> f(x := undefined) \<in> Pi\<^sub>E S T" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
401 |
unfolding PiE_def extensional_def by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
402 |
|
64910 | 403 |
lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)" |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
404 |
proof - |
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
405 |
{ |
64910 | 406 |
fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<notin> S" |
407 |
then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
408 |
by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem) |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
409 |
} |
59425 | 410 |
moreover |
411 |
{ |
|
64910 | 412 |
fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<in> S" |
413 |
then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)" |
|
59425 | 414 |
by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb) |
415 |
} |
|
416 |
ultimately show ?thesis |
|
63092 | 417 |
by (auto intro: PiE_fun_upd) |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
418 |
qed |
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
419 |
|
58783 | 420 |
lemma PiE_Int: "Pi\<^sub>E I A \<inter> Pi\<^sub>E I B = Pi\<^sub>E I (\<lambda>x. A x \<inter> B x)" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
421 |
by (auto simp: PiE_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
422 |
|
58783 | 423 |
lemma PiE_cong: "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^sub>E I A = Pi\<^sub>E I B" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
424 |
unfolding PiE_def by (auto simp: Pi_cong) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
425 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
426 |
lemma PiE_E [elim]: |
64910 | 427 |
assumes "f \<in> Pi\<^sub>E A B" |
58783 | 428 |
obtains "x \<in> A" and "f x \<in> B x" |
429 |
| "x \<notin> A" and "f x = undefined" |
|
430 |
using assms by (auto simp: Pi_def PiE_def extensional_def) |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
431 |
|
58783 | 432 |
lemma PiE_I[intro!]: |
64910 | 433 |
"(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> Pi\<^sub>E A B" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
434 |
by (simp add: PiE_def extensional_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
435 |
|
64910 | 436 |
lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi\<^sub>E A B \<subseteq> Pi\<^sub>E A C" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
437 |
by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
438 |
|
64910 | 439 |
lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
440 |
by (simp add: PiE_def Pi_iff) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
441 |
|
64910 | 442 |
lemma PiE_restrict[simp]: "f \<in> Pi\<^sub>E A B \<Longrightarrow> restrict f A = f" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
443 |
by (simp add: extensional_restrict PiE_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
444 |
|
64910 | 445 |
lemma restrict_PiE[simp]: "restrict f I \<in> Pi\<^sub>E I S \<longleftrightarrow> f \<in> Pi I S" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
446 |
by (auto simp: PiE_iff) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
447 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
448 |
lemma PiE_eq_subset: |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
449 |
assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}" |
58783 | 450 |
and eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'" |
451 |
and "i \<in> I" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
452 |
shows "F i \<subseteq> F' i" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
453 |
proof |
58783 | 454 |
fix x |
455 |
assume "x \<in> F i" |
|
456 |
with ne have "\<forall>j. \<exists>y. (j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined)" |
|
53381 | 457 |
by auto |
458 |
from choice[OF this] obtain f |
|
459 |
where f: " \<forall>j. (j \<in> I \<longrightarrow> f j \<in> F j \<and> (i = j \<longrightarrow> x = f j)) \<and> (j \<notin> I \<longrightarrow> f j = undefined)" .. |
|
58783 | 460 |
then have "f \<in> Pi\<^sub>E I F" |
461 |
by (auto simp: extensional_def PiE_def) |
|
462 |
then have "f \<in> Pi\<^sub>E I F'" |
|
463 |
using assms by simp |
|
464 |
then show "x \<in> F' i" |
|
465 |
using f \<open>i \<in> I\<close> by (auto simp: PiE_def) |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
466 |
qed |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
467 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
468 |
lemma PiE_eq_iff_not_empty: |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
469 |
assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
470 |
shows "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
471 |
proof (intro iffI ballI) |
58783 | 472 |
fix i |
473 |
assume eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'" |
|
474 |
assume i: "i \<in> I" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
475 |
show "F i = F' i" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
476 |
using PiE_eq_subset[of I F F', OF ne eq i] |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
477 |
using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i] |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
478 |
by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
479 |
qed (auto simp: PiE_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
480 |
|
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
481 |
lemma PiE_eq_iff: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
482 |
"Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
483 |
proof (intro iffI disjCI) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
484 |
assume eq[simp]: "Pi\<^sub>E I F = Pi\<^sub>E I F'" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
485 |
assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
486 |
then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
487 |
using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto |
58783 | 488 |
with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" |
489 |
by auto |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
490 |
next |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
491 |
assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
492 |
then show "Pi\<^sub>E I F = Pi\<^sub>E I F'" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
493 |
using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
494 |
qed |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
495 |
|
58783 | 496 |
lemma extensional_funcset_fun_upd_restricts_rangeI: |
497 |
"\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f \<in> (insert x S) \<rightarrow>\<^sub>E T \<Longrightarrow> f(x := undefined) \<in> S \<rightarrow>\<^sub>E (T - {f x})" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
498 |
unfolding extensional_funcset_def extensional_def |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
499 |
apply auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
500 |
apply (case_tac "x = xa") |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
501 |
apply auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
502 |
done |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
503 |
|
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
504 |
lemma extensional_funcset_fun_upd_extends_rangeI: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
505 |
assumes "a \<in> T" "f \<in> S \<rightarrow>\<^sub>E (T - {a})" |
58783 | 506 |
shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E T" |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
507 |
using assms unfolding extensional_funcset_def extensional_def by auto |
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
508 |
|
58783 | 509 |
|
510 |
subsubsection \<open>Injective Extensional Function Spaces\<close> |
|
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
511 |
|
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
512 |
lemma extensional_funcset_fun_upd_inj_onI: |
58783 | 513 |
assumes "f \<in> S \<rightarrow>\<^sub>E (T - {a})" |
514 |
and "inj_on f S" |
|
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
515 |
shows "inj_on (f(x := a)) S" |
58783 | 516 |
using assms |
517 |
unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI) |
|
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
518 |
|
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
519 |
lemma extensional_funcset_extend_domain_inj_on_eq: |
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
520 |
assumes "x \<notin> S" |
58783 | 521 |
shows "{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} = |
522 |
(\<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}" |
|
523 |
using assms |
|
524 |
apply (auto del: PiE_I PiE_E) |
|
525 |
apply (auto intro: extensional_funcset_fun_upd_inj_onI |
|
526 |
extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E) |
|
527 |
apply (auto simp add: image_iff inj_on_def) |
|
528 |
apply (rule_tac x="xa x" in exI) |
|
529 |
apply (auto intro: PiE_mem del: PiE_I PiE_E) |
|
530 |
apply (rule_tac x="xa(x := undefined)" in exI) |
|
531 |
apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI) |
|
62390 | 532 |
apply (auto dest!: PiE_mem split: if_split_asm) |
58783 | 533 |
done |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
534 |
|
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
535 |
lemma extensional_funcset_extend_domain_inj_onI: |
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
536 |
assumes "x \<notin> S" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
537 |
shows "inj_on (\<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}" |
58783 | 538 |
using assms |
539 |
apply (auto intro!: inj_onI) |
|
540 |
apply (metis fun_upd_same) |
|
541 |
apply (metis assms PiE_arb fun_upd_triv fun_upd_upd) |
|
542 |
done |
|
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
543 |
|
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
544 |
|
58783 | 545 |
subsubsection \<open>Cardinality\<close> |
546 |
||
547 |
lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (\<Pi>\<^sub>E i \<in> S. T i)" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
548 |
by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq) |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
549 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50123
diff
changeset
|
550 |
lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^sub>E S T)" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
551 |
proof (safe intro!: inj_onI ext) |
58783 | 552 |
fix f y g z |
553 |
assume "x \<notin> S" |
|
554 |
assume fg: "f \<in> Pi\<^sub>E S T" "g \<in> Pi\<^sub>E S T" |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
555 |
assume "f(x := y) = g(x := z)" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
556 |
then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i" |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
557 |
unfolding fun_eq_iff by auto |
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
558 |
from this[of x] show "y = z" by simp |
58783 | 559 |
fix i from *[of i] \<open>x \<notin> S\<close> fg show "f i = g i" |
62390 | 560 |
by (auto split: if_split_asm simp: PiE_def extensional_def) |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
561 |
qed |
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
562 |
|
58783 | 563 |
lemma card_PiE: "finite S \<Longrightarrow> card (\<Pi>\<^sub>E i \<in> S. T i) = (\<Prod> i\<in>S. card (T i))" |
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
564 |
proof (induct rule: finite_induct) |
58783 | 565 |
case empty |
566 |
then show ?case by auto |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
567 |
next |
58783 | 568 |
case (insert x S) |
569 |
then show ?case |
|
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset
|
570 |
by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product) |
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
571 |
qed |
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset
|
572 |
|
13586 | 573 |
end |