author  bulwahn 
Mon, 22 Nov 2010 10:41:51 +0100  
changeset 40631  b3f85ba3dae4 
parent 39595  9f86e46779e4 
child 44382  9afa4a0e6f3c 
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 

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

69 

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

72 
by (auto simp: Pi_def) 

73 

31769  74 
lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" 
75 
by (auto intro: Pi_I) 

76 

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

14762  80 
lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B" 
31754  81 
by auto 
14762  82 

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

13593  87 
apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto) 
14706  88 
apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto) 
13586  89 
done 
90 

13593  91 
lemma Pi_empty [simp]: "Pi {} B = UNIV" 
31754  92 
by (simp add: Pi_def) 
13593  93 

94 
lemma Pi_UNIV [simp]: "A > UNIV = UNIV" 

31754  95 
by (simp add: Pi_def) 
31727  96 
(* 
97 
lemma funcset_id [simp]: "(%x. x): A > A" 

98 
by (simp add: Pi_def) 

99 
*) 

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

31754  102 
by auto 
13586  103 

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

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

31754  106 
by auto 
13586  107 

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

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

109 
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

110 
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

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

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

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

114 
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

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

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

117 
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

118 
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

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

120 

13586  121 

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

123 

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

13586  127 

128 
lemma compose_assoc: 

14706  129 
"[ f \<in> A > B; g \<in> B > C; h \<in> C > D ] 
13586  130 
==> 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

131 
by (simp add: fun_eq_iff Pi_def compose_def restrict_def) 
13586  132 

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

31754  134 
by (simp add: compose_def restrict_def) 
13586  135 

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

14706  137 
by (auto simp add: image_def compose_eq) 
13586  138 

139 

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

141 

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

14706  143 
by (simp add: Pi_def restrict_def) 
13586  144 

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

148 
lemma restrict_apply [simp]: 

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

14706  152 
lemma restrict_ext: 
13586  153 
"(!!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

154 
by (simp add: fun_eq_iff Pi_def restrict_def) 
13586  155 

14853  156 
lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A" 
14706  157 
by (simp add: inj_on_def restrict_def) 
13586  158 

159 
lemma Id_compose: 

14706  160 
"[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

161 
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def) 
13586  162 

163 
lemma compose_Id: 

14706  164 
"[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

165 
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def) 
13586  166 

14853  167 
lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A" 
19736  168 
by (auto simp add: restrict_def) 
13586  169 

14745  170 

14762  171 
subsection{*Bijections Between Sets*} 
172 

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

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

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

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

179 
shows "bij_betw f A B" 

180 
unfolding bij_betw_def 

181 
proof 

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

183 
next 

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

185 
moreover 

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

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

188 
qed 

189 

14762  190 
lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B" 
32988  191 
by (auto simp add: bij_betw_def) 
14762  192 

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

14853  196 

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

200 
apply (auto simp add: compose_def image_def) 

201 
done 

14762  202 

14853  203 
lemma bij_betw_restrict_eq [simp]: 
31754  204 
"bij_betw (restrict f A) A B = bij_betw f A B" 
205 
by (simp add: bij_betw_def) 

14853  206 

207 

208 
subsection{*Extensionality*} 

209 

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

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

31754  214 
by (simp add: restrict_def extensional_def) 
14853  215 

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

31754  217 
by (simp add: compose_def) 
14853  218 

219 
lemma extensionalityI: 

31754  220 
"[ f \<in> extensional A; g \<in> extensional A; 
14853  221 
!!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

222 
by (force simp add: fun_eq_iff extensional_def) 
14853  223 

39595  224 
lemma extensional_restrict: "f \<in> extensional A \<Longrightarrow> restrict f A = f" 
225 
by(rule extensionalityI[OF restrict_extensional]) auto 

226 

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

14853  229 

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

31754  232 
apply (simp add: bij_betw_def compose_def) 
233 
apply (rule restrict_ext, auto) 

234 
done 

14853  235 

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

31754  238 
apply (simp add: compose_def) 
239 
apply (rule restrict_ext) 

33057  240 
apply (simp add: f_inv_into_f) 
31754  241 
done 
14853  242 

14762  243 

14745  244 
subsection{*Cardinality*} 
245 

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

31754  247 
by (rule card_inj_on_le) auto 
14745  248 

249 
lemma card_bij: 

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

252 
by (blast intro: card_inj order_antisym) 

14745  253 

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

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

255 

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

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

257 
where "extensional_funcset S T = (S > T) \<inter> (extensional S)" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

258 

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

259 
lemma extensional_empty[simp]: "extensional {} = {%x. undefined}" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

260 
unfolding extensional_def by (auto intro: ext) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

261 

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

262 
lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

263 
unfolding extensional_funcset_def by simp 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

264 

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

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

266 
assumes "S \<noteq> {}" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

267 
shows "extensional_funcset S {} = {}" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

268 
using assms unfolding extensional_funcset_def by auto 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

269 

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

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

271 
assumes "f \<in> extensional_funcset S T" "x \<notin> S" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

272 
shows "f x = undefined" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

274 
unfolding extensional_funcset_def by auto (auto dest!: extensional_arb) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

275 

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

276 
lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

277 
unfolding extensional_funcset_def by auto 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

278 

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

279 
lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

280 
unfolding extensional_def by auto 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

281 

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

282 
lemma extensional_funcset_extend_domainI: "\<lbrakk> y \<in> T; f \<in> extensional_funcset S T\<rbrakk> \<Longrightarrow> f(x := y) \<in> extensional_funcset (insert x S) T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

283 
unfolding extensional_funcset_def extensional_def by auto 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

284 

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

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

286 
"x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

287 
unfolding extensional_funcset_def extensional_def by auto 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

288 

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

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

290 
assumes "x \<notin> S" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

292 
"extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

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

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

297 
assume "f : extensional_funcset (insert x S) T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

298 
from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

300 
apply (rule_tac x="(f x, f(x := undefined))" in bexI) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

301 
apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

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

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

306 
assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

307 
from this assms have "f : extensional_funcset (insert x S) T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

308 
by (auto intro: extensional_funcset_extend_domainI) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

310 
ultimately show ?thesis by auto 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

312 

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

313 
lemma extensional_funcset_fun_upd_restricts_rangeI: "\<forall> y \<in> S. f x \<noteq> f y ==> f : extensional_funcset (insert x S) T ==> f(x := undefined) : extensional_funcset S (T  {f x})" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

316 
apply (case_tac "x = xa") 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

318 

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

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

320 
assumes "a \<in> T" "f : extensional_funcset S (T  {a})" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

322 
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

323 

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

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

325 

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

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

327 
assumes "f \<in> extensional_funcset S (T  {a})" "inj_on f S" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

329 
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

330 

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

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

332 
assumes "x \<notin> S" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

333 
shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} = 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

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

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

338 
apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

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

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

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

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

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

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

347 

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

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

349 
assumes "x \<notin> S" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

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

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

354 
apply (metis fun_upd_same) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

357 

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

358 

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

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

360 

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

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

362 
assumes "finite S" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

363 
shows "card (extensional_funcset S T) = (card T) ^ (card S)" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

365 
proof (induct rule: finite_induct) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

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

368 
by (auto simp add: extensional_funcset_empty_domain) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

370 
case (insert x S) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

372 
fix g g' y y' 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

373 
assume assms: "g \<in> extensional_funcset S T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

374 
"g' \<in> extensional_funcset S T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

375 
"y \<in> T" "y' \<in> T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

376 
"g(x := y) = g'(x := y')" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

377 
from this have "y = y'" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

378 
by (metis fun_upd_same) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

379 
have "g = g'" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

380 
by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2)) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

381 
from `y = y'` `g = g'` have "y = y' & g = g'" by simp 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

383 
from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

385 
from this insert.hyps show ?case 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

386 
by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

388 

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

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

390 
assumes "finite S" "finite T" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

391 
shows "finite (extensional_funcset S T)" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

393 
from card_extensional_funcset[OF assms(1), of T] assms(2) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

394 
have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

396 
from this show ?thesis 
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 
assume "card (extensional_funcset S T) \<noteq> 0" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

400 
by (auto intro: card_ge_0_finite) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

402 
assume "S \<noteq> {} \<and> T = {}" 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

404 
by (auto simp add: extensional_funcset_empty_range) 
b3f85ba3dae4
adding extensional function spaces to the FuncSet library theory
bulwahn
parents:
39595
diff
changeset

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

13586  408 
end 