author  hoelzl 
Mon, 19 Nov 2012 12:29:02 +0100  
changeset 50123  69b35a75caf3 
parent 50104  de19856feb54 
child 53015  a1119cf551e8 
permissions  rwrr 
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 

14706  5 
header {* Pi and Function Sets *} 
13586  6 

15131  7 
theory FuncSet 
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
28524
diff
changeset

8 
imports Hilbert_Choice Main 
15131  9 
begin 
13586  10 

19736  11 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

12 
Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where 
19736  13 
"Pi A B = {f. \<forall>x. x \<in> A > f x \<in> B x}" 
13586  14 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

15 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

16 
extensional :: "'a set => ('a => 'b) set" where 
28524  17 
"extensional A = {f. \<forall>x. x~:A > f x = undefined}" 
13586  18 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

19 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

20 
"restrict" :: "['a => 'b, 'a set] => ('a => 'b)" where 
28524  21 
"restrict f A = (%x. if x \<in> A then f x else undefined)" 
13586  22 

19536  23 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

24 
funcset :: "['a set, 'b set] => ('a => 'b) set" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

25 
(infixr ">" 60) where 
19536  26 
"A > B == Pi A (%_. B)" 
27 

21210  28 
notation (xsymbols) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19536
diff
changeset

29 
funcset (infixr "\<rightarrow>" 60) 
19536  30 

13586  31 
syntax 
19736  32 
"_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10) 
33 
"_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3) 

13586  34 

35 
syntax (xsymbols) 

19736  36 
"_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10) 
37 
"_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3) 

13586  38 

14565  39 
syntax (HTML output) 
19736  40 
"_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10) 
41 
"_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3) 

14565  42 

13586  43 
translations 
20770  44 
"PI x:A. B" == "CONST Pi A (%x. B)" 
45 
"%x:A. f" == "CONST restrict (%x. f) A" 

13586  46 

19736  47 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

48 
"compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" where 
19736  49 
"compose A g f = (\<lambda>x\<in>A. g (f x))" 
13586  50 

51 

52 
subsection{*Basic Properties of @{term Pi}*} 

53 

31754  54 
lemma Pi_I[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B" 
14706  55 
by (simp add: Pi_def) 
13586  56 

31731  57 
lemma Pi_I'[simp]: "(!!x. x : A > f x : B x) ==> f : Pi A B" 
58 
by(simp add:Pi_def) 

59 

13586  60 
lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A > B" 
14706  61 
by (simp add: Pi_def) 
13586  62 

63 
lemma Pi_mem: "[f: Pi A B; x \<in> A] ==> f x \<in> B x" 

14706  64 
by (simp add: Pi_def) 
13586  65 

47761  66 
lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)" 
67 
unfolding Pi_def by auto 

68 

31759  69 
lemma PiE [elim]: 
31754  70 
"f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q" 
71 
by(auto simp: Pi_def) 

72 

38656  73 
lemma Pi_cong: 
74 
"(\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B" 

75 
by (auto simp: Pi_def) 

76 

31769  77 
lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" 
44382  78 
by auto 
31769  79 

13586  80 
lemma funcset_mem: "[f \<in> A > B; x \<in> A] ==> f x \<in> B" 
14706  81 
by (simp add: Pi_def) 
13586  82 

14762  83 
lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B" 
50104  84 
by auto 
85 

86 
lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B" 

87 
by auto 

14762  88 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

89 
lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B x = {})" 
13593  90 
apply (simp add: Pi_def, auto) 
13586  91 
txt{*Converse direction requires Axiom of Choice to exhibit a function 
92 
picking an element from each nonempty @{term "B x"}*} 

13593  93 
apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto) 
14706  94 
apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto) 
13586  95 
done 
96 

13593  97 
lemma Pi_empty [simp]: "Pi {} B = UNIV" 
31754  98 
by (simp add: Pi_def) 
13593  99 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

100 
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

101 
by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

102 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

103 
lemma Pi_UN: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

104 
fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

105 
assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

106 
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

107 
proof (intro set_eqI iffI) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

108 
fix f assume "f \<in> (\<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

109 
then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

110 
from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

111 
obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

112 
using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

113 
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

114 
proof (intro Pi_I) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

115 
fix i assume "i \<in> I" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

116 
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

117 
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

118 
qed 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

119 
then show "f \<in> (\<Union>n. Pi I (A n))" by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

120 
qed auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

121 

13593  122 
lemma Pi_UNIV [simp]: "A > UNIV = UNIV" 
31754  123 
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

124 

13586  125 
text{*Covariance of Pisets in their second argument*} 
126 
lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C" 

31754  127 
by auto 
13586  128 

129 
text{*Contravariance of Pisets in their first argument*} 

130 
lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" 

31754  131 
by auto 
13586  132 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

133 
lemma prod_final: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

134 
assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

135 
shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

136 
proof (rule Pi_I) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

137 
fix z 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

138 
assume z: "z \<in> A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

139 
have "f z = (fst (f z), snd (f z))" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

140 
by simp 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

141 
also have "... \<in> B z \<times> C z" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

142 
by (metis SigmaI PiE o_apply 1 2 z) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

143 
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

144 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33057
diff
changeset

145 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

146 
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

147 
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

148 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

149 
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

150 
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

151 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

152 
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

153 
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

154 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

155 
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

156 
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

157 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

158 
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

159 
apply auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

160 
apply (drule_tac x=x in Pi_mem) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

161 
apply (simp_all split: split_if_asm) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

162 
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

163 
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

164 
done 
13586  165 

166 
subsection{*Composition With a Restricted Domain: @{term compose}*} 

167 

14706  168 
lemma funcset_compose: 
31754  169 
"[ f \<in> A > B; g \<in> B > C ]==> compose A g f \<in> A > C" 
170 
by (simp add: Pi_def compose_def restrict_def) 

13586  171 

172 
lemma compose_assoc: 

14706  173 
"[ f \<in> A > B; g \<in> B > C; h \<in> C > D ] 
13586  174 
==> compose A h (compose A g f) = compose A (compose B h g) 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

175 
by (simp add: fun_eq_iff Pi_def compose_def restrict_def) 
13586  176 

177 
lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))" 

31754  178 
by (simp add: compose_def restrict_def) 
13586  179 

180 
lemma surj_compose: "[ f ` A = B; g ` B = C ] ==> compose A g f ` A = C" 

14706  181 
by (auto simp add: image_def compose_eq) 
13586  182 

183 

184 
subsection{*Bounded Abstraction: @{term restrict}*} 

185 

186 
lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A > B" 

14706  187 
by (simp add: Pi_def restrict_def) 
13586  188 

31754  189 
lemma restrictI[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B" 
14706  190 
by (simp add: Pi_def restrict_def) 
13586  191 

192 
lemma restrict_apply [simp]: 

28524  193 
"(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)" 
14706  194 
by (simp add: restrict_def) 
13586  195 

14706  196 
lemma restrict_ext: 
13586  197 
"(!!x. x \<in> A ==> f x = g x) ==> (\<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

198 
by (simp add: fun_eq_iff Pi_def restrict_def) 
13586  199 

14853  200 
lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A" 
14706  201 
by (simp add: inj_on_def restrict_def) 
13586  202 

203 
lemma Id_compose: 

14706  204 
"[f \<in> A > B; f \<in> extensional A] ==> 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

205 
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def) 
13586  206 

207 
lemma compose_Id: 

14706  208 
"[g \<in> A > B; g \<in> extensional A] ==> 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

209 
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def) 
13586  210 

14853  211 
lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A" 
19736  212 
by (auto simp add: restrict_def) 
13586  213 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

214 
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

215 
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

216 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

217 
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

218 
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

219 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

220 
lemma restrict_upd[simp]: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

221 
"i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

222 
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

223 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

224 
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

225 
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

226 

14745  227 

14762  228 
subsection{*Bijections Between Sets*} 
229 

26106
be52145f482d
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas
nipkow
parents:
21404
diff
changeset

230 
text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of 
14762  231 
the theorems belong here, or need at least @{term Hilbert_Choice}.*} 
232 

39595  233 
lemma bij_betwI: 
234 
assumes "f \<in> A \<rightarrow> B" and "g \<in> B \<rightarrow> A" 

235 
and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x" and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y" 

236 
shows "bij_betw f A B" 

237 
unfolding bij_betw_def 

238 
proof 

239 
show "inj_on f A" by (metis g_f inj_on_def) 

240 
next 

241 
have "f ` A \<subseteq> B" using `f \<in> A \<rightarrow> B` by auto 

242 
moreover 

243 
have "B \<subseteq> f ` A" by auto (metis Pi_mem `g \<in> B \<rightarrow> A` f_g image_iff) 

244 
ultimately show "f ` A = B" by blast 

245 
qed 

246 

14762  247 
lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B" 
32988  248 
by (auto simp add: bij_betw_def) 
14762  249 

14853  250 
lemma inj_on_compose: 
31754  251 
"[ bij_betw f A B; inj_on g B ] ==> inj_on (compose A g f) A" 
252 
by (auto simp add: bij_betw_def inj_on_def compose_eq) 

14853  253 

14762  254 
lemma bij_betw_compose: 
31754  255 
"[ bij_betw f A B; bij_betw g B C ] ==> bij_betw (compose A g f) A C" 
256 
apply (simp add: bij_betw_def compose_eq inj_on_compose) 

257 
apply (auto simp add: compose_def image_def) 

258 
done 

14762  259 

14853  260 
lemma bij_betw_restrict_eq [simp]: 
31754  261 
"bij_betw (restrict f A) A B = bij_betw f A B" 
262 
by (simp add: bij_betw_def) 

14853  263 

264 

265 
subsection{*Extensionality*} 

266 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

267 
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

268 
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

269 

28524  270 
lemma extensional_arb: "[f \<in> extensional A; x\<notin> A] ==> f x = undefined" 
31754  271 
by (simp add: extensional_def) 
14853  272 

273 
lemma restrict_extensional [simp]: "restrict f A \<in> extensional A" 

31754  274 
by (simp add: restrict_def extensional_def) 
14853  275 

276 
lemma compose_extensional [simp]: "compose A f g \<in> extensional A" 

31754  277 
by (simp add: compose_def) 
14853  278 

279 
lemma extensionalityI: 

31754  280 
"[ f \<in> extensional A; g \<in> extensional A; 
14853  281 
!!x. x\<in>A ==> f x = g x ] ==> f = 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

282 
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" 
285 
by(rule extensionalityI[OF restrict_extensional]) auto 

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 

33057  290 
lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B > A" 
291 
by (unfold inv_into_def) (fast intro: someI2) 

14853  292 

33057  293 
lemma compose_inv_into_id: 
294 
"bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)" 

31754  295 
apply (simp add: bij_betw_def compose_def) 
296 
apply (rule restrict_ext, auto) 

297 
done 

14853  298 

33057  299 
lemma compose_id_inv_into: 
300 
"f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)" 

31754  301 
apply (simp add: compose_def) 
302 
apply (rule restrict_ext) 

33057  303 
apply (simp add: f_inv_into_f) 
31754  304 
done 
14853  305 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

306 
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

307 
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

308 
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

309 
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

310 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

311 
lemma extensional_Int[simp]: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

312 
"extensional I \<inter> extensional I' = extensional (I \<inter> I')" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

313 
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

314 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

315 
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

316 
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

317 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

318 
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

319 
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

320 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

321 
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

322 
"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

323 
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

324 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

325 
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

326 
"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

327 
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

328 

14762  329 

14745  330 
subsection{*Cardinality*} 
331 

332 
lemma card_inj: "[f \<in> A\<rightarrow>B; inj_on f A; finite B] ==> card(A) \<le> card(B)" 

31754  333 
by (rule card_inj_on_le) auto 
14745  334 

335 
lemma card_bij: 

31754  336 
"[f \<in> A\<rightarrow>B; inj_on f A; 
337 
g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B] ==> card(A) = card(B)" 

338 
by (blast intro: card_inj order_antisym) 

14745  339 

40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

340 
subsection {* Extensional Function Spaces *} 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

341 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

342 
definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" where 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

343 
"PiE S T = Pi S T \<inter> extensional S" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

344 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

345 
abbreviation "Pi\<^isub>E A B \<equiv> PiE A B" 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

346 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

347 
syntax "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

348 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

349 
syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

350 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

351 
syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

352 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

353 
translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)" 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

354 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

355 
abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr ">\<^isub>E" 60) where 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

356 
"A >\<^isub>E B \<equiv> (\<Pi>\<^isub>E i\<in>A. B)" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

357 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

358 
notation (xsymbols) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

359 
extensional_funcset (infixr "\<rightarrow>\<^isub>E" 60) 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

360 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

361 
lemma extensional_funcset_def: "extensional_funcset S T = (S > T) \<inter> extensional S" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

362 
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

363 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

364 
lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}" 
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 simp 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

366 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

367 
lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

368 
unfolding PiE_def by auto 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

369 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

370 
lemma PiE_eq_empty_iff: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

371 
"Pi\<^isub>E I F = {} \<longleftrightarrow> (\<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

372 
proof 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

373 
assume "Pi\<^isub>E I F = {}" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

374 
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

375 
proof (rule ccontr) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

376 
assume "\<not> ?thesis" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

377 
then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

378 
from choice[OF this] guess f .. 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

379 
then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

380 
with `Pi\<^isub>E I F = {}` show False by auto 
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 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

384 
lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined" 
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 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

387 
lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x" 
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 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

390 
lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T" 
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 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

393 
lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T" 
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 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

396 
lemma PiE_insert_eq: 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

397 
assumes "x \<notin> S" 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

398 
shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)" 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

399 
proof  
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

400 
{ 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

401 
fix f assume "f \<in> PiE (insert x S) T" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

402 
with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

403 
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

404 
} 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

405 
then show ?thesis using assms by (auto intro: PiE_fun_upd) 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

406 
qed 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

407 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

408 
lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

409 
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

410 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

411 
lemma PiE_cong: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

412 
"(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^isub>E I A = Pi\<^isub>E I B" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

413 
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

414 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

415 
lemma PiE_E [elim]: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

416 
"f \<in> PiE A B \<Longrightarrow> (x \<in> A \<Longrightarrow> f x \<in> B x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> f x = undefined \<Longrightarrow> Q) \<Longrightarrow> Q" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

417 
by(auto simp: Pi_def PiE_def extensional_def) 
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_I[intro!]: "(\<And>x. x \<in> A ==> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> PiE A B" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

420 
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

421 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

422 
lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

423 
by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

424 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

425 
lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

426 
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

427 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

428 
lemma PiE_restrict[simp]: "f \<in> PiE A B \<Longrightarrow> restrict f A = f" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

429 
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

430 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

431 
lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

432 
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

433 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

434 
lemma PiE_eq_subset: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

435 
assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

436 
assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

437 
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

438 
proof 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

439 
fix x assume "x \<in> F i" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

440 
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))" by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

441 
from choice[OF this] guess f .. note f = this 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

442 
then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

443 
then have "f \<in> Pi\<^isub>E I F'" using assms by simp 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

444 
then show "x \<in> F' i" using f `i \<in> I` 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

445 
qed 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

446 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

447 
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

448 
assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

449 
shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

450 
proof (intro iffI ballI) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

451 
fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

452 
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

453 
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

454 
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

455 
by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

456 
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

457 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

458 
lemma PiE_eq_iff: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

459 
"Pi\<^isub>E I F = Pi\<^isub>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 = {}))" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

460 
proof (intro iffI disjCI) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

461 
assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

462 
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

463 
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

464 
using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

465 
with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

466 
next 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

467 
assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<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

468 
then show "Pi\<^isub>E I F = Pi\<^isub>E I F'" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

469 
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

470 
qed 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

471 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

472 
lemma extensional_funcset_fun_upd_restricts_rangeI: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

473 
"\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f : (insert x S) \<rightarrow>\<^isub>E T ==> f(x := undefined) : S \<rightarrow>\<^isub>E (T  {f x})" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

474 
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

475 
apply auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

476 
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

477 
apply auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

478 
done 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

479 

b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

480 
lemma extensional_funcset_fun_upd_extends_rangeI: 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

481 
assumes "a \<in> T" "f \<in> S \<rightarrow>\<^isub>E (T  {a})" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

482 
shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^isub>E T" 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

483 
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

484 

b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

485 
subsubsection {* Injective Extensional Function Spaces *} 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

486 

b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

487 
lemma extensional_funcset_fun_upd_inj_onI: 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

488 
assumes "f \<in> S \<rightarrow>\<^isub>E (T  {a})" "inj_on f S" 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

489 
shows "inj_on (f(x := a)) S" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

490 
using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

491 

b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

492 
lemma extensional_funcset_extend_domain_inj_on_eq: 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

493 
assumes "x \<notin> S" 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

494 
shows"{f. f \<in> (insert x S) \<rightarrow>\<^isub>E T \<and> inj_on f (insert x S)} = 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

495 
(%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T  {y}) \<and> inj_on g S}" 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

496 
proof  
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

497 
from assms show ?thesis 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

498 
apply (auto del: PiE_I PiE_E) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

499 
apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E) 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

500 
apply (auto simp add: image_iff inj_on_def) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

501 
apply (rule_tac x="xa x" in exI) 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

502 
apply (auto intro: PiE_mem del: PiE_I PiE_E) 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

503 
apply (rule_tac x="xa(x := undefined)" in exI) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

504 
apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI) 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

505 
apply (auto dest!: PiE_mem split: split_if_asm) 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

506 
done 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

507 
qed 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

508 

b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

509 
lemma extensional_funcset_extend_domain_inj_onI: 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

510 
assumes "x \<notin> S" 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

511 
shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T  {y}) \<and> inj_on g S}" 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

512 
proof  
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

513 
from assms show ?thesis 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

514 
apply (auto intro!: inj_onI) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

515 
apply (metis fun_upd_same) 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

516 
by (metis assms PiE_arb fun_upd_triv fun_upd_upd) 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

517 
qed 
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 

b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

520 
subsubsection {* Cardinality *} 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

521 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

522 
lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (PIE i : S. T i)" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

523 
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

524 

69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

525 
lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^isub>E S T)" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

526 
proof (safe intro!: inj_onI ext) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

527 
fix f y g z assume "x \<notin> S" and fg: "f \<in> Pi\<^isub>E S T" "g \<in> Pi\<^isub>E S T" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

528 
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

529 
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

530 
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

531 
from this[of x] show "y = z" by simp 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

532 
fix i from *[of i] `x \<notin> S` fg show "f i = g i" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

533 
by (auto split: split_if_asm simp: PiE_def extensional_def) 
40631
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

534 
qed 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

535 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

536 
lemma card_PiE: 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

537 
"finite S \<Longrightarrow> card (PIE i : S. T i) = (\<Prod> i\<in>S. card (T i))" 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

538 
proof (induct rule: finite_induct) 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

539 
case empty then show ?case by auto 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

540 
next 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

541 
case (insert x S) then show ?case 
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

542 
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

543 
qed 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

544 

13586  545 
end 