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