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.6  
     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.14  by (simp add: Pi_def)
    1.15  
    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.39  by (simp add: Pi_def)
    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.51  
    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.71  
    1.72  subsection{*Composition With a Restricted Domain: @{term compose}*}
    1.73  
    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.77  
    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.91  
    1.92  subsection{*Bijections Between Sets*}
    1.93  
    1.94 @@ -213,6 +264,9 @@
    1.95  
    1.96  subsection{*Extensionality*}
    1.97  
    1.98 +lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
    1.99 +  unfolding extensional_def by auto
   1.100 +
   1.101  lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
   1.102  by (simp add: extensional_def)
   1.103  
   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.107  
   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.110 +
   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.113  
   1.114 @@ -246,6 +303,29 @@
   1.115  apply (simp add: f_inv_into_f)
   1.116  done
   1.117  
   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.122 +
   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.126 +
   1.127 +lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
   1.128 +  by (auto simp: extensional_def)
   1.129 +
   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.132 +
   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.136 +
   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.140 +
   1.141  
   1.142  subsection{*Cardinality*}
   1.143  
   1.144 @@ -259,156 +339,207 @@
   1.145  
   1.146  subsection {* Extensional Function Spaces *} 
   1.147  
   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.152 +
   1.153 +abbreviation "Pi\<^isub>E A B \<equiv> PiE A B"
   1.154  
   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.158 +
   1.159 +syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
   1.160 +
   1.161 +syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
   1.162 +
   1.163 +translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
   1.164  
   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.169 +
   1.170 +notation (xsymbols)
   1.171 +  extensional_funcset  (infixr "\<rightarrow>\<^isub>E" 60)
   1.172  
   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.179 +
   1.180 +lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
   1.181 +  unfolding PiE_def by simp
   1.182 +
   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.185  
   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.191 -
   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.194 -
   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.210  
   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.215 +
   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.218  
   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.224  
   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.228 +
   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.236    {
   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.246    }
   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.257  
   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.265 +
   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.269 +
   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.273 +
   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.276 +
   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.279 +
   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.282 +
   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.285 +
   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.288 +
   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.301 +
   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.312 +
   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.326 +
   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.334  
   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.341  
   1.342  subsubsection {* Injective Extensional Function Spaces *}
   1.343  
   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.349  
   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.372  
   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.384    
   1.385  
   1.386  subsubsection {* Cardinality *}
   1.387  
   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.416 +
   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.427  
   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.453  
   1.454  end