src/HOL/Library/FuncSet.thy
 changeset 50123 69b35a75caf3 parent 50104 de19856feb54 child 53015 a1119cf551e8
1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Nov 19 16:14:18 2012 +0100
1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Nov 19 12:29:02 2012 +0100
1.3 @@ -86,7 +86,7 @@
1.4  lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
1.5    by auto
1.7 -lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
1.8 +lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B x = {})"
1.9  apply (simp add: Pi_def, auto)
1.10  txt{*Converse direction requires Axiom of Choice to exhibit a function
1.11  picking an element from each non-empty @{term "B x"}*}
1.12 @@ -97,12 +97,31 @@
1.13  lemma Pi_empty [simp]: "Pi {} B = UNIV"
1.16 +lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
1.17 +  by auto
1.18 +
1.19 +lemma Pi_UN:
1.20 +  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
1.21 +  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
1.22 +  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
1.23 +proof (intro set_eqI iffI)
1.24 +  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
1.25 +  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
1.26 +  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
1.27 +  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
1.28 +    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
1.29 +  have "f \<in> Pi I (A k)"
1.30 +  proof (intro Pi_I)
1.31 +    fix i assume "i \<in> I"
1.32 +    from mono[OF this, of "n i" k] k[OF this] n[OF this]
1.33 +    show "f i \<in> A k i" by auto
1.34 +  qed
1.35 +  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
1.36 +qed auto
1.37 +
1.38  lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
1.40 -(*
1.41 -lemma funcset_id [simp]: "(%x. x): A -> A"
1.42 -  by (simp add: Pi_def)
1.43 -*)
1.44 +
1.45  text{*Covariance of Pi-sets in their second argument*}
1.46  lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
1.47  by auto
1.48 @@ -124,6 +143,25 @@
1.49    finally show "f z \<in> B z \<times> C z" .
1.50  qed
1.52 +lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
1.53 +  by (auto simp: Pi_def)
1.54 +
1.55 +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"
1.56 +  by (auto simp: Pi_def)
1.57 +
1.58 +lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
1.59 +  by (auto simp: Pi_def)
1.60 +
1.61 +lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
1.62 +  by (auto simp: Pi_def)
1.63 +
1.64 +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"
1.65 +  apply auto
1.66 +  apply (drule_tac x=x in Pi_mem)
1.67 +  apply (simp_all split: split_if_asm)
1.68 +  apply (drule_tac x=i in Pi_mem)
1.69 +  apply (auto dest!: Pi_mem)
1.70 +  done
1.72  subsection{*Composition With a Restricted Domain: @{term compose}*}
1.74 @@ -173,6 +211,19 @@
1.75  lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
1.76    by (auto simp add: restrict_def)
1.78 +lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
1.79 +  unfolding restrict_def by (simp add: fun_eq_iff)
1.80 +
1.81 +lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
1.82 +  by (auto simp: restrict_def)
1.83 +
1.84 +lemma restrict_upd[simp]:
1.85 +  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
1.86 +  by (auto simp: fun_eq_iff)
1.87 +
1.88 +lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
1.89 +  by (auto simp: restrict_def Pi_def)
1.90 +
1.92  subsection{*Bijections Between Sets*}
1.94 @@ -213,6 +264,9 @@
1.96  subsection{*Extensionality*}
1.98 +lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
1.99 +  unfolding extensional_def by auto
1.101  lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
1.104 @@ -230,6 +284,9 @@
1.105  lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
1.106  by(rule extensionalityI[OF restrict_extensional]) auto
1.108 +lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B"
1.109 +  unfolding extensional_def by auto
1.111  lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
1.112  by (unfold inv_into_def) (fast intro: someI2)
1.114 @@ -246,6 +303,29 @@
1.116  done
1.118 +lemma extensional_insert[intro, simp]:
1.119 +  assumes "a \<in> extensional (insert i I)"
1.120 +  shows "a(i := b) \<in> extensional (insert i I)"
1.121 +  using assms unfolding extensional_def by auto
1.123 +lemma extensional_Int[simp]:
1.124 +  "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
1.125 +  unfolding extensional_def by auto
1.127 +lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
1.128 +  by (auto simp: extensional_def)
1.130 +lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
1.131 +  unfolding restrict_def extensional_def by auto
1.133 +lemma extensional_insert_undefined[intro, simp]:
1.134 +  "a \<in> extensional (insert i I) \<Longrightarrow> a(i := undefined) \<in> extensional I"
1.135 +  unfolding extensional_def by auto
1.137 +lemma extensional_insert_cancel[intro, simp]:
1.138 +  "a \<in> extensional I \<Longrightarrow> a \<in> extensional (insert i I)"
1.139 +  unfolding extensional_def by auto
1.142  subsection{*Cardinality*}
1.144 @@ -259,156 +339,207 @@
1.146  subsection {* Extensional Function Spaces *}
1.148 -definition extensional_funcset
1.149 -where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
1.150 +definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" where
1.151 +  "PiE S T = Pi S T \<inter> extensional S"
1.153 +abbreviation "Pi\<^isub>E A B \<equiv> PiE A B"
1.155 -lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
1.156 -unfolding extensional_def by auto
1.157 +syntax "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
1.159 +syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
1.161 +syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
1.163 +translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
1.165 -lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
1.166 -unfolding extensional_funcset_def by simp
1.167 +abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^isub>E" 60) where
1.168 +  "A ->\<^isub>E B \<equiv> (\<Pi>\<^isub>E i\<in>A. B)"
1.170 +notation (xsymbols)
1.171 +  extensional_funcset  (infixr "\<rightarrow>\<^isub>E" 60)
1.173 -lemma extensional_funcset_empty_range:
1.174 -  assumes "S \<noteq> {}"
1.175 -  shows "extensional_funcset S {} = {}"
1.176 -using assms unfolding extensional_funcset_def by auto
1.177 +lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) \<inter> extensional S"
1.178 +  by (simp add: PiE_def)
1.180 +lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
1.181 +  unfolding PiE_def by simp
1.183 +lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}"
1.184 +  unfolding PiE_def by auto
1.186 -lemma extensional_funcset_arb:
1.187 -  assumes "f \<in> extensional_funcset S T" "x \<notin> S"
1.188 -  shows "f x = undefined"
1.189 -using assms
1.190 -unfolding extensional_funcset_def by auto (auto dest!: extensional_arb)
1.192 -lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T"
1.193 -unfolding extensional_funcset_def by auto
1.195 -lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B"
1.196 -unfolding extensional_def by auto
1.197 +lemma PiE_eq_empty_iff:
1.198 +  "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
1.199 +proof
1.200 +  assume "Pi\<^isub>E I F = {}"
1.201 +  show "\<exists>i\<in>I. F i = {}"
1.202 +  proof (rule ccontr)
1.203 +    assume "\<not> ?thesis"
1.204 +    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
1.205 +    from choice[OF this] guess f ..
1.206 +    then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
1.207 +    with `Pi\<^isub>E I F = {}` show False by auto
1.208 +  qed
1.209 +qed (auto simp: PiE_def)
1.211 -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"
1.212 -unfolding extensional_funcset_def extensional_def by auto
1.213 +lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
1.214 +  unfolding PiE_def by auto (auto dest!: extensional_arb)
1.216 +lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
1.217 +  unfolding PiE_def by auto
1.219 -lemma extensional_funcset_restrict_domain:
1.220 -  "x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T"
1.221 -unfolding extensional_funcset_def extensional_def by auto
1.222 +lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T"
1.223 +  unfolding PiE_def extensional_def by auto
1.225 -lemma extensional_funcset_extend_domain_eq:
1.226 +lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
1.227 +  unfolding PiE_def extensional_def by auto
1.229 +lemma PiE_insert_eq:
1.230    assumes "x \<notin> S"
1.231 -  shows
1.232 -    "extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}"
1.233 -  using assms
1.234 +  shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.235  proof -
1.237 -    fix f
1.238 -    assume "f : extensional_funcset (insert x S) T"
1.239 -    from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
1.240 -      unfolding image_iff
1.241 -      apply (rule_tac x="(f x, f(x := undefined))" in bexI)
1.242 -    apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done
1.243 +    fix f assume "f \<in> PiE (insert x S) T"
1.244 +    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.245 +      by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
1.247 -  moreover
1.248 -  {
1.249 -    fix f
1.250 -    assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
1.251 -    from this assms have "f : extensional_funcset (insert x S) T"
1.252 -      by (auto intro: extensional_funcset_extend_domainI)
1.253 -  }
1.254 -  ultimately show ?thesis by auto
1.255 +  then show ?thesis using assms by (auto intro: PiE_fun_upd)
1.256  qed
1.258 -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})"
1.259 -unfolding extensional_funcset_def extensional_def
1.260 -apply auto
1.261 -apply (case_tac "x = xa")
1.262 -apply auto done
1.263 +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)"
1.264 +  by (auto simp: PiE_def)
1.266 +lemma PiE_cong:
1.267 +  "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^isub>E I A = Pi\<^isub>E I B"
1.268 +  unfolding PiE_def by (auto simp: Pi_cong)
1.270 +lemma PiE_E [elim]:
1.271 +  "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"
1.272 +by(auto simp: Pi_def PiE_def extensional_def)
1.274 +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"
1.275 +  by (simp add: PiE_def extensional_def)
1.277 +lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
1.278 +  by auto
1.280 +lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
1.281 +  by (simp add: PiE_def Pi_iff)
1.283 +lemma PiE_restrict[simp]:  "f \<in> PiE A B \<Longrightarrow> restrict f A = f"
1.284 +  by (simp add: extensional_restrict PiE_def)
1.286 +lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S"
1.287 +  by (auto simp: PiE_iff)
1.289 +lemma PiE_eq_subset:
1.290 +  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
1.291 +  assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
1.292 +  shows "F i \<subseteq> F' i"
1.293 +proof
1.294 +  fix x assume "x \<in> F i"
1.295 +  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
1.296 +  from choice[OF this] guess f .. note f = this
1.297 +  then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
1.298 +  then have "f \<in> Pi\<^isub>E I F'" using assms by simp
1.299 +  then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
1.300 +qed
1.302 +lemma PiE_eq_iff_not_empty:
1.303 +  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
1.304 +  shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
1.305 +proof (intro iffI ballI)
1.306 +  fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
1.307 +  show "F i = F' i"
1.308 +    using PiE_eq_subset[of I F F', OF ne eq i]
1.309 +    using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
1.310 +    by auto
1.311 +qed (auto simp: PiE_def)
1.313 +lemma PiE_eq_iff:
1.314 +  "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 = {}))"
1.315 +proof (intro iffI disjCI)
1.316 +  assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
1.317 +  assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
1.318 +  then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
1.319 +    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
1.320 +  with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
1.321 +next
1.322 +  assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
1.323 +  then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
1.324 +    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
1.325 +qed
1.327 +lemma extensional_funcset_fun_upd_restricts_rangeI:
1.328 +  "\<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})"
1.329 +  unfolding extensional_funcset_def extensional_def
1.330 +  apply auto
1.331 +  apply (case_tac "x = xa")
1.332 +  apply auto
1.333 +  done
1.335  lemma extensional_funcset_fun_upd_extends_rangeI:
1.336 -  assumes "a \<in> T" "f : extensional_funcset S (T - {a})"
1.337 -  shows "f(x := a) : extensional_funcset (insert x S) T"
1.338 +  assumes "a \<in> T" "f \<in> S \<rightarrow>\<^isub>E (T - {a})"
1.339 +  shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^isub>E  T"
1.340    using assms unfolding extensional_funcset_def extensional_def by auto
1.342  subsubsection {* Injective Extensional Function Spaces *}
1.344  lemma extensional_funcset_fun_upd_inj_onI:
1.345 -  assumes "f \<in> extensional_funcset S (T - {a})" "inj_on f S"
1.346 +  assumes "f \<in> S \<rightarrow>\<^isub>E (T - {a})" "inj_on f S"
1.347    shows "inj_on (f(x := a)) S"
1.348    using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
1.350  lemma extensional_funcset_extend_domain_inj_on_eq:
1.351    assumes "x \<notin> S"
1.352 -  shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} =
1.353 -    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
1.354 +  shows"{f. f \<in> (insert x S) \<rightarrow>\<^isub>E T \<and> inj_on f (insert x S)} =
1.355 +    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
1.356  proof -
1.357    from assms show ?thesis
1.358 -    apply auto
1.359 -    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI)
1.360 +    apply (auto del: PiE_I PiE_E)
1.361 +    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
1.362      apply (auto simp add: image_iff inj_on_def)
1.363      apply (rule_tac x="xa x" in exI)
1.364 -    apply (auto intro: extensional_funcset_mem)
1.365 +    apply (auto intro: PiE_mem del: PiE_I PiE_E)
1.366      apply (rule_tac x="xa(x := undefined)" in exI)
1.367      apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
1.368 -    apply (auto dest!: extensional_funcset_mem split: split_if_asm)
1.369 +    apply (auto dest!: PiE_mem split: split_if_asm)
1.370      done
1.371  qed
1.373  lemma extensional_funcset_extend_domain_inj_onI:
1.374    assumes "x \<notin> S"
1.375 -  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}"
1.376 +  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}"
1.377  proof -
1.378    from assms show ?thesis
1.379      apply (auto intro!: inj_onI)
1.380      apply (metis fun_upd_same)
1.381 -    by (metis assms extensional_funcset_arb fun_upd_triv fun_upd_upd)
1.382 +    by (metis assms PiE_arb fun_upd_triv fun_upd_upd)
1.383  qed
1.386  subsubsection {* Cardinality *}
1.388 -lemma card_extensional_funcset:
1.389 -  assumes "finite S"
1.390 -  shows "card (extensional_funcset S T) = (card T) ^ (card S)"
1.391 -using assms
1.392 -proof (induct rule: finite_induct)
1.393 -  case empty
1.394 -  show ?case
1.395 -    by (auto simp add: extensional_funcset_empty_domain)
1.396 -next
1.397 -  case (insert x S)
1.398 -  {
1.399 -    fix g g' y y'
1.400 -    assume assms: "g \<in> extensional_funcset S T"
1.401 -      "g' \<in> extensional_funcset S T"
1.402 -      "y \<in> T" "y' \<in> T"
1.403 -      "g(x := y) = g'(x := y')"
1.404 -    from this have "y = y'"
1.405 -      by (metis fun_upd_same)
1.406 -    have "g = g'"
1.407 -      by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2))
1.408 -  from `y = y'` `g = g'` have "y = y' & g = g'" by simp
1.409 -  }
1.410 -  from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)"
1.411 -    by (auto intro: inj_onI)
1.412 -  from this insert.hyps show ?case
1.413 -    by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product)
1.414 +lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (PIE i : S. T i)"
1.415 +  by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
1.417 +lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^isub>E S T)"
1.418 +proof (safe intro!: inj_onI ext)
1.419 +  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"
1.420 +  assume "f(x := y) = g(x := z)"
1.421 +  then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
1.422 +    unfolding fun_eq_iff by auto
1.423 +  from this[of x] show "y = z" by simp
1.424 +  fix i from *[of i] `x \<notin> S` fg show "f i = g i"
1.425 +    by (auto split: split_if_asm simp: PiE_def extensional_def)
1.426  qed
1.428 -lemma finite_extensional_funcset:
1.429 -  assumes "finite S" "finite T"
1.430 -  shows "finite (extensional_funcset S T)"
1.431 -proof -
1.432 -  from card_extensional_funcset[OF assms(1), of T] assms(2)
1.433 -  have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})"
1.434 -    by auto
1.435 -  from this show ?thesis
1.436 -  proof
1.437 -    assume "card (extensional_funcset S T) \<noteq> 0"
1.438 -    from this show ?thesis
1.439 -      by (auto intro: card_ge_0_finite)
1.440 -  next
1.441 -    assume "S \<noteq> {} \<and> T = {}"
1.442 -    from this show ?thesis
1.443 -      by (auto simp add: extensional_funcset_empty_range)
1.444 -  qed
1.445 +lemma card_PiE:
1.446 +  "finite S \<Longrightarrow> card (PIE i : S. T i) = (\<Prod> i\<in>S. card (T i))"
1.447 +proof (induct rule: finite_induct)
1.448 +  case empty then show ?case by auto
1.449 +next
1.450 +  case (insert x S) then show ?case
1.451 +    by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
1.452  qed
1.454  end