move FuncSet back to HOL-Library (amending 493b818e8e10)
authorimmler
Tue May 15 11:33:43 2018 +0200 (12 months ago)
changeset 681882af1f142f855
parent 68187 48262e3a2bde
child 68189 6163c90694ef
move FuncSet back to HOL-Library (amending 493b818e8e10)
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Group.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/FuncSet.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Library.thy
src/HOL/Metis_Examples/Abstraction.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Number_Theory/Prime_Powers.thy
src/HOL/Vector_Spaces.thy
src/HOL/ex/Ballot.thy
src/HOL/ex/Birthday_Paradox.thy
src/HOL/ex/Tarski.thy
     1.1 --- a/src/HOL/Algebra/Congruence.thy	Tue May 15 06:23:12 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Congruence.thy	Tue May 15 11:33:43 2018 +0200
     1.3 @@ -5,7 +5,8 @@
     1.4  
     1.5  theory Congruence
     1.6    imports
     1.7 -    Main HOL.FuncSet
     1.8 +    Main
     1.9 +    "HOL-Library.FuncSet"
    1.10  begin
    1.11  
    1.12  section \<open>Objects\<close>
     2.1 --- a/src/HOL/Algebra/Group.thy	Tue May 15 06:23:12 2018 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Tue May 15 11:33:43 2018 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  *)
     2.5  
     2.6  theory Group
     2.7 -imports Complete_Lattice HOL.FuncSet
     2.8 +imports Complete_Lattice "HOL-Library.FuncSet"
     2.9  begin
    2.10  
    2.11  section \<open>Monoids and Groups\<close>
     3.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue May 15 06:23:12 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue May 15 11:33:43 2018 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    L2_Norm
     3.5    "HOL-Library.Numeral_Type"
     3.6    "HOL-Library.Countable_Set"
     3.7 +  "HOL-Library.FuncSet"
     3.8  begin
     3.9  
    3.10  subsection \<open>Finite Cartesian products, with indexing and lambdas\<close>
     4.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Tue May 15 06:23:12 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue May 15 11:33:43 2018 +0200
     4.3 @@ -11,6 +11,7 @@
     4.4  imports
     4.5    Complex_Main
     4.6    "HOL-Library.Countable_Set"
     4.7 +  "HOL-Library.FuncSet"
     4.8    "HOL-Library.Indicator_Function"
     4.9    "HOL-Library.Extended_Nonnegative_Real"
    4.10    "HOL-Library.Disjoint_Sets"
     5.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue May 15 06:23:12 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue May 15 11:33:43 2018 +0200
     5.3 @@ -10,6 +10,7 @@
     5.4  imports
     5.5    "HOL-Library.Indicator_Function"
     5.6    "HOL-Library.Countable_Set"
     5.7 +  "HOL-Library.FuncSet"
     5.8    Linear_Algebra
     5.9    Norm_Arith
    5.10  begin
     6.1 --- a/src/HOL/FuncSet.thy	Tue May 15 06:23:12 2018 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,568 +0,0 @@
     6.4 -(*  Title:      HOL/FuncSet.thy
     6.5 -    Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
     6.6 -*)
     6.7 -
     6.8 -section \<open>Pi and Function Sets\<close>
     6.9 -
    6.10 -theory FuncSet
    6.11 -  imports Main
    6.12 -  abbrevs PiE = "Pi\<^sub>E"
    6.13 -    and PIE = "\<Pi>\<^sub>E"
    6.14 -begin
    6.15 -
    6.16 -definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
    6.17 -  where "Pi A B = {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x}"
    6.18 -
    6.19 -definition extensional :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) set"
    6.20 -  where "extensional A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = undefined}"
    6.21 -
    6.22 -definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
    6.23 -  where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)"
    6.24 -
    6.25 -abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
    6.26 -  where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
    6.27 -
    6.28 -syntax
    6.29 -  "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    6.30 -  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    6.31 -translations
    6.32 -  "\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
    6.33 -  "\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
    6.34 -
    6.35 -definition "compose" :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c)"
    6.36 -  where "compose A g f = (\<lambda>x\<in>A. g (f x))"
    6.37 -
    6.38 -
    6.39 -subsection \<open>Basic Properties of @{term Pi}\<close>
    6.40 -
    6.41 -lemma Pi_I[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B"
    6.42 -  by (simp add: Pi_def)
    6.43 -
    6.44 -lemma Pi_I'[simp]: "(\<And>x. x \<in> A \<longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B"
    6.45 -  by (simp add:Pi_def)
    6.46 -
    6.47 -lemma funcsetI: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f \<in> A \<rightarrow> B"
    6.48 -  by (simp add: Pi_def)
    6.49 -
    6.50 -lemma Pi_mem: "f \<in> Pi A B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B x"
    6.51 -  by (simp add: Pi_def)
    6.52 -
    6.53 -lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
    6.54 -  unfolding Pi_def by auto
    6.55 -
    6.56 -lemma PiE [elim]: "f \<in> Pi A B \<Longrightarrow> (f x \<in> B x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> Q"
    6.57 -  by (auto simp: Pi_def)
    6.58 -
    6.59 -lemma Pi_cong: "(\<And>w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B"
    6.60 -  by (auto simp: Pi_def)
    6.61 -
    6.62 -lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
    6.63 -  by auto
    6.64 -
    6.65 -lemma funcset_mem: "f \<in> A \<rightarrow> B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B"
    6.66 -  by (simp add: Pi_def)
    6.67 -
    6.68 -lemma funcset_image: "f \<in> A \<rightarrow> B \<Longrightarrow> f ` A \<subseteq> B"
    6.69 -  by auto
    6.70 -
    6.71 -lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
    6.72 -  by auto
    6.73 -
    6.74 -lemma Pi_eq_empty[simp]: "(\<Pi> x \<in> A. B x) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})"
    6.75 -  apply (simp add: Pi_def)
    6.76 -  apply auto
    6.77 -  txt \<open>Converse direction requires Axiom of Choice to exhibit a function
    6.78 -  picking an element from each non-empty @{term "B x"}\<close>
    6.79 -  apply (drule_tac x = "\<lambda>u. SOME y. y \<in> B u" in spec)
    6.80 -  apply auto
    6.81 -  apply (cut_tac P = "\<lambda>y. y \<in> B x" in some_eq_ex)
    6.82 -  apply auto
    6.83 -  done
    6.84 -
    6.85 -lemma Pi_empty [simp]: "Pi {} B = UNIV"
    6.86 -  by (simp add: Pi_def)
    6.87 -
    6.88 -lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
    6.89 -  by auto
    6.90 -
    6.91 -lemma Pi_UN:
    6.92 -  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
    6.93 -  assumes "finite I"
    6.94 -    and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
    6.95 -  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
    6.96 -proof (intro set_eqI iffI)
    6.97 -  fix f
    6.98 -  assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
    6.99 -  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
   6.100 -    by auto
   6.101 -  from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
   6.102 -    by auto
   6.103 -  obtain k where k: "n i \<le> k" if "i \<in> I" for i
   6.104 -    using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
   6.105 -  have "f \<in> Pi I (A k)"
   6.106 -  proof (intro Pi_I)
   6.107 -    fix i
   6.108 -    assume "i \<in> I"
   6.109 -    from mono[OF this, of "n i" k] k[OF this] n[OF this]
   6.110 -    show "f i \<in> A k i" by auto
   6.111 -  qed
   6.112 -  then show "f \<in> (\<Union>n. Pi I (A n))"
   6.113 -    by auto
   6.114 -qed auto
   6.115 -
   6.116 -lemma Pi_UNIV [simp]: "A \<rightarrow> UNIV = UNIV"
   6.117 -  by (simp add: Pi_def)
   6.118 -
   6.119 -text \<open>Covariance of Pi-sets in their second argument\<close>
   6.120 -lemma Pi_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi A B \<subseteq> Pi A C"
   6.121 -  by auto
   6.122 -
   6.123 -text \<open>Contravariance of Pi-sets in their first argument\<close>
   6.124 -lemma Pi_anti_mono: "A' \<subseteq> A \<Longrightarrow> Pi A B \<subseteq> Pi A' B"
   6.125 -  by auto
   6.126 -
   6.127 -lemma prod_final:
   6.128 -  assumes 1: "fst \<circ> f \<in> Pi A B"
   6.129 -    and 2: "snd \<circ> f \<in> Pi A C"
   6.130 -  shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
   6.131 -proof (rule Pi_I)
   6.132 -  fix z
   6.133 -  assume z: "z \<in> A"
   6.134 -  have "f z = (fst (f z), snd (f z))"
   6.135 -    by simp
   6.136 -  also have "\<dots> \<in> B z \<times> C z"
   6.137 -    by (metis SigmaI PiE o_apply 1 2 z)
   6.138 -  finally show "f z \<in> B z \<times> C z" .
   6.139 -qed
   6.140 -
   6.141 -lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
   6.142 -  by (auto simp: Pi_def)
   6.143 -
   6.144 -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"
   6.145 -  by (auto simp: Pi_def)
   6.146 -
   6.147 -lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
   6.148 -  by (auto simp: Pi_def)
   6.149 -
   6.150 -lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
   6.151 -  by (auto simp: Pi_def)
   6.152 -
   6.153 -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"
   6.154 -  apply auto
   6.155 -  apply (drule_tac x=x in Pi_mem)
   6.156 -  apply (simp_all split: if_split_asm)
   6.157 -  apply (drule_tac x=i in Pi_mem)
   6.158 -  apply (auto dest!: Pi_mem)
   6.159 -  done
   6.160 -
   6.161 -
   6.162 -subsection \<open>Composition With a Restricted Domain: @{term compose}\<close>
   6.163 -
   6.164 -lemma funcset_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> g \<in> B \<rightarrow> C \<Longrightarrow> compose A g f \<in> A \<rightarrow> C"
   6.165 -  by (simp add: Pi_def compose_def restrict_def)
   6.166 -
   6.167 -lemma compose_assoc:
   6.168 -  assumes "f \<in> A \<rightarrow> B"
   6.169 -    and "g \<in> B \<rightarrow> C"
   6.170 -    and "h \<in> C \<rightarrow> D"
   6.171 -  shows "compose A h (compose A g f) = compose A (compose B h g) f"
   6.172 -  using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)
   6.173 -
   6.174 -lemma compose_eq: "x \<in> A \<Longrightarrow> compose A g f x = g (f x)"
   6.175 -  by (simp add: compose_def restrict_def)
   6.176 -
   6.177 -lemma surj_compose: "f ` A = B \<Longrightarrow> g ` B = C \<Longrightarrow> compose A g f ` A = C"
   6.178 -  by (auto simp add: image_def compose_eq)
   6.179 -
   6.180 -
   6.181 -subsection \<open>Bounded Abstraction: @{term restrict}\<close>
   6.182 -
   6.183 -lemma restrict_cong: "I = J \<Longrightarrow> (\<And>i. i \<in> J =simp=> f i = g i) \<Longrightarrow> restrict f I = restrict g J"
   6.184 -  by (auto simp: restrict_def fun_eq_iff simp_implies_def)
   6.185 -
   6.186 -lemma restrict_in_funcset: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> A \<rightarrow> B"
   6.187 -  by (simp add: Pi_def restrict_def)
   6.188 -
   6.189 -lemma restrictI[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> Pi A B"
   6.190 -  by (simp add: Pi_def restrict_def)
   6.191 -
   6.192 -lemma restrict_apply[simp]: "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
   6.193 -  by (simp add: restrict_def)
   6.194 -
   6.195 -lemma restrict_apply': "x \<in> A \<Longrightarrow> (\<lambda>y\<in>A. f y) x = f x"
   6.196 -  by simp
   6.197 -
   6.198 -lemma restrict_ext: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
   6.199 -  by (simp add: fun_eq_iff Pi_def restrict_def)
   6.200 -
   6.201 -lemma restrict_UNIV: "restrict f UNIV = f"
   6.202 -  by (simp add: restrict_def)
   6.203 -
   6.204 -lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
   6.205 -  by (simp add: inj_on_def restrict_def)
   6.206 -
   6.207 -lemma Id_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> f \<in> extensional A \<Longrightarrow> compose A (\<lambda>y\<in>B. y) f = f"
   6.208 -  by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)
   6.209 -
   6.210 -lemma compose_Id: "g \<in> A \<rightarrow> B \<Longrightarrow> g \<in> extensional A \<Longrightarrow> compose A g (\<lambda>x\<in>A. x) = g"
   6.211 -  by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)
   6.212 -
   6.213 -lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
   6.214 -  by (auto simp add: restrict_def)
   6.215 -
   6.216 -lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
   6.217 -  unfolding restrict_def by (simp add: fun_eq_iff)
   6.218 -
   6.219 -lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
   6.220 -  by (auto simp: restrict_def)
   6.221 -
   6.222 -lemma restrict_upd[simp]: "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
   6.223 -  by (auto simp: fun_eq_iff)
   6.224 -
   6.225 -lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
   6.226 -  by (auto simp: restrict_def Pi_def)
   6.227 -
   6.228 -
   6.229 -subsection \<open>Bijections Between Sets\<close>
   6.230 -
   6.231 -text \<open>The definition of @{const bij_betw} is in \<open>Fun.thy\<close>, but most of
   6.232 -the theorems belong here, or need at least @{term Hilbert_Choice}.\<close>
   6.233 -
   6.234 -lemma bij_betwI:
   6.235 -  assumes "f \<in> A \<rightarrow> B"
   6.236 -    and "g \<in> B \<rightarrow> A"
   6.237 -    and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x"
   6.238 -    and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y"
   6.239 -  shows "bij_betw f A B"
   6.240 -  unfolding bij_betw_def
   6.241 -proof
   6.242 -  show "inj_on f A"
   6.243 -    by (metis g_f inj_on_def)
   6.244 -  have "f ` A \<subseteq> B"
   6.245 -    using \<open>f \<in> A \<rightarrow> B\<close> by auto
   6.246 -  moreover
   6.247 -  have "B \<subseteq> f ` A"
   6.248 -    by auto (metis Pi_mem \<open>g \<in> B \<rightarrow> A\<close> f_g image_iff)
   6.249 -  ultimately show "f ` A = B"
   6.250 -    by blast
   6.251 -qed
   6.252 -
   6.253 -lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
   6.254 -  by (auto simp add: bij_betw_def)
   6.255 -
   6.256 -lemma inj_on_compose: "bij_betw f A B \<Longrightarrow> inj_on g B \<Longrightarrow> inj_on (compose A g f) A"
   6.257 -  by (auto simp add: bij_betw_def inj_on_def compose_eq)
   6.258 -
   6.259 -lemma bij_betw_compose: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (compose A g f) A C"
   6.260 -  apply (simp add: bij_betw_def compose_eq inj_on_compose)
   6.261 -  apply (auto simp add: compose_def image_def)
   6.262 -  done
   6.263 -
   6.264 -lemma bij_betw_restrict_eq [simp]: "bij_betw (restrict f A) A B = bij_betw f A B"
   6.265 -  by (simp add: bij_betw_def)
   6.266 -
   6.267 -
   6.268 -subsection \<open>Extensionality\<close>
   6.269 -
   6.270 -lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
   6.271 -  unfolding extensional_def by auto
   6.272 -
   6.273 -lemma extensional_arb: "f \<in> extensional A \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = undefined"
   6.274 -  by (simp add: extensional_def)
   6.275 -
   6.276 -lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
   6.277 -  by (simp add: restrict_def extensional_def)
   6.278 -
   6.279 -lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
   6.280 -  by (simp add: compose_def)
   6.281 -
   6.282 -lemma extensionalityI:
   6.283 -  assumes "f \<in> extensional A"
   6.284 -    and "g \<in> extensional A"
   6.285 -    and "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
   6.286 -  shows "f = g"
   6.287 -  using assms by (force simp add: fun_eq_iff extensional_def)
   6.288 -
   6.289 -lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
   6.290 -  by (rule extensionalityI[OF restrict_extensional]) auto
   6.291 -
   6.292 -lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B"
   6.293 -  unfolding extensional_def by auto
   6.294 -
   6.295 -lemma inv_into_funcset: "f ` A = B \<Longrightarrow> (\<lambda>x\<in>B. inv_into A f x) \<in> B \<rightarrow> A"
   6.296 -  by (unfold inv_into_def) (fast intro: someI2)
   6.297 -
   6.298 -lemma compose_inv_into_id: "bij_betw f A B \<Longrightarrow> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
   6.299 -  apply (simp add: bij_betw_def compose_def)
   6.300 -  apply (rule restrict_ext, auto)
   6.301 -  done
   6.302 -
   6.303 -lemma compose_id_inv_into: "f ` A = B \<Longrightarrow> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
   6.304 -  apply (simp add: compose_def)
   6.305 -  apply (rule restrict_ext)
   6.306 -  apply (simp add: f_inv_into_f)
   6.307 -  done
   6.308 -
   6.309 -lemma extensional_insert[intro, simp]:
   6.310 -  assumes "a \<in> extensional (insert i I)"
   6.311 -  shows "a(i := b) \<in> extensional (insert i I)"
   6.312 -  using assms unfolding extensional_def by auto
   6.313 -
   6.314 -lemma extensional_Int[simp]: "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
   6.315 -  unfolding extensional_def by auto
   6.316 -
   6.317 -lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
   6.318 -  by (auto simp: extensional_def)
   6.319 -
   6.320 -lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
   6.321 -  unfolding restrict_def extensional_def by auto
   6.322 -
   6.323 -lemma extensional_insert_undefined[intro, simp]:
   6.324 -  "a \<in> extensional (insert i I) \<Longrightarrow> a(i := undefined) \<in> extensional I"
   6.325 -  unfolding extensional_def by auto
   6.326 -
   6.327 -lemma extensional_insert_cancel[intro, simp]:
   6.328 -  "a \<in> extensional I \<Longrightarrow> a \<in> extensional (insert i I)"
   6.329 -  unfolding extensional_def by auto
   6.330 -
   6.331 -
   6.332 -subsection \<open>Cardinality\<close>
   6.333 -
   6.334 -lemma card_inj: "f \<in> A \<rightarrow> B \<Longrightarrow> inj_on f A \<Longrightarrow> finite B \<Longrightarrow> card A \<le> card B"
   6.335 -  by (rule card_inj_on_le) auto
   6.336 -
   6.337 -lemma card_bij:
   6.338 -  assumes "f \<in> A \<rightarrow> B" "inj_on f A"
   6.339 -    and "g \<in> B \<rightarrow> A" "inj_on g B"
   6.340 -    and "finite A" "finite B"
   6.341 -  shows "card A = card B"
   6.342 -  using assms by (blast intro: card_inj order_antisym)
   6.343 -
   6.344 -
   6.345 -subsection \<open>Extensional Function Spaces\<close>
   6.346 -
   6.347 -definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
   6.348 -  where "PiE S T = Pi S T \<inter> extensional S"
   6.349 -
   6.350 -abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
   6.351 -
   6.352 -syntax
   6.353 -  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
   6.354 -translations
   6.355 -  "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
   6.356 -
   6.357 -abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
   6.358 -  where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
   6.359 -
   6.360 -lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
   6.361 -  by (simp add: PiE_def)
   6.362 -
   6.363 -lemma PiE_empty_domain[simp]: "Pi\<^sub>E {} T = {\<lambda>x. undefined}"
   6.364 -  unfolding PiE_def by simp
   6.365 -
   6.366 -lemma PiE_UNIV_domain: "Pi\<^sub>E UNIV T = Pi UNIV T"
   6.367 -  unfolding PiE_def by simp
   6.368 -
   6.369 -lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (\<Pi>\<^sub>E i\<in>I. F i) = {}"
   6.370 -  unfolding PiE_def by auto
   6.371 -
   6.372 -lemma PiE_eq_empty_iff: "Pi\<^sub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
   6.373 -proof
   6.374 -  assume "Pi\<^sub>E I F = {}"
   6.375 -  show "\<exists>i\<in>I. F i = {}"
   6.376 -  proof (rule ccontr)
   6.377 -    assume "\<not> ?thesis"
   6.378 -    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)"
   6.379 -      by auto
   6.380 -    from choice[OF this]
   6.381 -    obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" ..
   6.382 -    then have "f \<in> Pi\<^sub>E I F"
   6.383 -      by (auto simp: extensional_def PiE_def)
   6.384 -    with \<open>Pi\<^sub>E I F = {}\<close> show False
   6.385 -      by auto
   6.386 -  qed
   6.387 -qed (auto simp: PiE_def)
   6.388 -
   6.389 -lemma PiE_arb: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
   6.390 -  unfolding PiE_def by auto (auto dest!: extensional_arb)
   6.391 -
   6.392 -lemma PiE_mem: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
   6.393 -  unfolding PiE_def by auto
   6.394 -
   6.395 -lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> Pi\<^sub>E S T \<Longrightarrow> f(x := y) \<in> Pi\<^sub>E (insert x S) T"
   6.396 -  unfolding PiE_def extensional_def by auto
   6.397 -
   6.398 -lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> Pi\<^sub>E (insert x S) T \<Longrightarrow> f(x := undefined) \<in> Pi\<^sub>E S T"
   6.399 -  unfolding PiE_def extensional_def by auto
   6.400 -
   6.401 -lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
   6.402 -proof -
   6.403 -  {
   6.404 -    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<notin> S"
   6.405 -    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
   6.406 -      by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   6.407 -  }
   6.408 -  moreover
   6.409 -  {
   6.410 -    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<in> S"
   6.411 -    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
   6.412 -      by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
   6.413 -  }
   6.414 -  ultimately show ?thesis
   6.415 -    by (auto intro: PiE_fun_upd)
   6.416 -qed
   6.417 -
   6.418 -lemma PiE_Int: "Pi\<^sub>E I A \<inter> Pi\<^sub>E I B = Pi\<^sub>E I (\<lambda>x. A x \<inter> B x)"
   6.419 -  by (auto simp: PiE_def)
   6.420 -
   6.421 -lemma PiE_cong: "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^sub>E I A = Pi\<^sub>E I B"
   6.422 -  unfolding PiE_def by (auto simp: Pi_cong)
   6.423 -
   6.424 -lemma PiE_E [elim]:
   6.425 -  assumes "f \<in> Pi\<^sub>E A B"
   6.426 -  obtains "x \<in> A" and "f x \<in> B x"
   6.427 -    | "x \<notin> A" and "f x = undefined"
   6.428 -  using assms by (auto simp: Pi_def PiE_def extensional_def)
   6.429 -
   6.430 -lemma PiE_I[intro!]:
   6.431 -  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> Pi\<^sub>E A B"
   6.432 -  by (simp add: PiE_def extensional_def)
   6.433 -
   6.434 -lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi\<^sub>E A B \<subseteq> Pi\<^sub>E A C"
   6.435 -  by auto
   6.436 -
   6.437 -lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
   6.438 -  by (simp add: PiE_def Pi_iff)
   6.439 -
   6.440 -lemma PiE_restrict[simp]:  "f \<in> Pi\<^sub>E A B \<Longrightarrow> restrict f A = f"
   6.441 -  by (simp add: extensional_restrict PiE_def)
   6.442 -
   6.443 -lemma restrict_PiE[simp]: "restrict f I \<in> Pi\<^sub>E I S \<longleftrightarrow> f \<in> Pi I S"
   6.444 -  by (auto simp: PiE_iff)
   6.445 -
   6.446 -lemma PiE_eq_subset:
   6.447 -  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   6.448 -    and eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   6.449 -    and "i \<in> I"
   6.450 -  shows "F i \<subseteq> F' i"
   6.451 -proof
   6.452 -  fix x
   6.453 -  assume "x \<in> F i"
   6.454 -  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)"
   6.455 -    by auto
   6.456 -  from choice[OF this] obtain f
   6.457 -    where f: " \<forall>j. (j \<in> I \<longrightarrow> f j \<in> F j \<and> (i = j \<longrightarrow> x = f j)) \<and> (j \<notin> I \<longrightarrow> f j = undefined)" ..
   6.458 -  then have "f \<in> Pi\<^sub>E I F"
   6.459 -    by (auto simp: extensional_def PiE_def)
   6.460 -  then have "f \<in> Pi\<^sub>E I F'"
   6.461 -    using assms by simp
   6.462 -  then show "x \<in> F' i"
   6.463 -    using f \<open>i \<in> I\<close> by (auto simp: PiE_def)
   6.464 -qed
   6.465 -
   6.466 -lemma PiE_eq_iff_not_empty:
   6.467 -  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   6.468 -  shows "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
   6.469 -proof (intro iffI ballI)
   6.470 -  fix i
   6.471 -  assume eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   6.472 -  assume i: "i \<in> I"
   6.473 -  show "F i = F' i"
   6.474 -    using PiE_eq_subset[of I F F', OF ne eq i]
   6.475 -    using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
   6.476 -    by auto
   6.477 -qed (auto simp: PiE_def)
   6.478 -
   6.479 -lemma PiE_eq_iff:
   6.480 -  "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   6.481 -proof (intro iffI disjCI)
   6.482 -  assume eq[simp]: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   6.483 -  assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   6.484 -  then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
   6.485 -    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
   6.486 -  with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i"
   6.487 -    by auto
   6.488 -next
   6.489 -  assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
   6.490 -  then show "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   6.491 -    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
   6.492 -qed
   6.493 -
   6.494 -lemma extensional_funcset_fun_upd_restricts_rangeI:
   6.495 -  "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f \<in> (insert x S) \<rightarrow>\<^sub>E T \<Longrightarrow> f(x := undefined) \<in> S \<rightarrow>\<^sub>E (T - {f x})"
   6.496 -  unfolding extensional_funcset_def extensional_def
   6.497 -  apply auto
   6.498 -  apply (case_tac "x = xa")
   6.499 -  apply auto
   6.500 -  done
   6.501 -
   6.502 -lemma extensional_funcset_fun_upd_extends_rangeI:
   6.503 -  assumes "a \<in> T" "f \<in> S \<rightarrow>\<^sub>E (T - {a})"
   6.504 -  shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E  T"
   6.505 -  using assms unfolding extensional_funcset_def extensional_def by auto
   6.506 -
   6.507 -
   6.508 -subsubsection \<open>Injective Extensional Function Spaces\<close>
   6.509 -
   6.510 -lemma extensional_funcset_fun_upd_inj_onI:
   6.511 -  assumes "f \<in> S \<rightarrow>\<^sub>E (T - {a})"
   6.512 -    and "inj_on f S"
   6.513 -  shows "inj_on (f(x := a)) S"
   6.514 -  using assms
   6.515 -  unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
   6.516 -
   6.517 -lemma extensional_funcset_extend_domain_inj_on_eq:
   6.518 -  assumes "x \<notin> S"
   6.519 -  shows "{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} =
   6.520 -    (\<lambda>(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
   6.521 -  using assms
   6.522 -  apply (auto del: PiE_I PiE_E)
   6.523 -  apply (auto intro: extensional_funcset_fun_upd_inj_onI
   6.524 -    extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
   6.525 -  apply (auto simp add: image_iff inj_on_def)
   6.526 -  apply (rule_tac x="xa x" in exI)
   6.527 -  apply (auto intro: PiE_mem del: PiE_I PiE_E)
   6.528 -  apply (rule_tac x="xa(x := undefined)" in exI)
   6.529 -  apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
   6.530 -  apply (auto dest!: PiE_mem split: if_split_asm)
   6.531 -  done
   6.532 -
   6.533 -lemma extensional_funcset_extend_domain_inj_onI:
   6.534 -  assumes "x \<notin> S"
   6.535 -  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
   6.536 -  using assms
   6.537 -  apply (auto intro!: inj_onI)
   6.538 -  apply (metis fun_upd_same)
   6.539 -  apply (metis assms PiE_arb fun_upd_triv fun_upd_upd)
   6.540 -  done
   6.541 -
   6.542 -
   6.543 -subsubsection \<open>Cardinality\<close>
   6.544 -
   6.545 -lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (\<Pi>\<^sub>E i \<in> S. T i)"
   6.546 -  by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
   6.547 -
   6.548 -lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^sub>E S T)"
   6.549 -proof (safe intro!: inj_onI ext)
   6.550 -  fix f y g z
   6.551 -  assume "x \<notin> S"
   6.552 -  assume fg: "f \<in> Pi\<^sub>E S T" "g \<in> Pi\<^sub>E S T"
   6.553 -  assume "f(x := y) = g(x := z)"
   6.554 -  then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
   6.555 -    unfolding fun_eq_iff by auto
   6.556 -  from this[of x] show "y = z" by simp
   6.557 -  fix i from *[of i] \<open>x \<notin> S\<close> fg show "f i = g i"
   6.558 -    by (auto split: if_split_asm simp: PiE_def extensional_def)
   6.559 -qed
   6.560 -
   6.561 -lemma card_PiE: "finite S \<Longrightarrow> card (\<Pi>\<^sub>E i \<in> S. T i) = (\<Prod> i\<in>S. card (T i))"
   6.562 -proof (induct rule: finite_induct)
   6.563 -  case empty
   6.564 -  then show ?case by auto
   6.565 -next
   6.566 -  case (insert x S)
   6.567 -  then show ?case
   6.568 -    by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
   6.569 -qed
   6.570 -
   6.571 -end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/FuncSet.thy	Tue May 15 11:33:43 2018 +0200
     7.3 @@ -0,0 +1,568 @@
     7.4 +(*  Title:      HOL/FuncSet.thy
     7.5 +    Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
     7.6 +*)
     7.7 +
     7.8 +section \<open>Pi and Function Sets\<close>
     7.9 +
    7.10 +theory FuncSet
    7.11 +  imports Main
    7.12 +  abbrevs PiE = "Pi\<^sub>E"
    7.13 +    and PIE = "\<Pi>\<^sub>E"
    7.14 +begin
    7.15 +
    7.16 +definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
    7.17 +  where "Pi A B = {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x}"
    7.18 +
    7.19 +definition extensional :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) set"
    7.20 +  where "extensional A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = undefined}"
    7.21 +
    7.22 +definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
    7.23 +  where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)"
    7.24 +
    7.25 +abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
    7.26 +  where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
    7.27 +
    7.28 +syntax
    7.29 +  "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    7.30 +  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    7.31 +translations
    7.32 +  "\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
    7.33 +  "\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
    7.34 +
    7.35 +definition "compose" :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c)"
    7.36 +  where "compose A g f = (\<lambda>x\<in>A. g (f x))"
    7.37 +
    7.38 +
    7.39 +subsection \<open>Basic Properties of @{term Pi}\<close>
    7.40 +
    7.41 +lemma Pi_I[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B"
    7.42 +  by (simp add: Pi_def)
    7.43 +
    7.44 +lemma Pi_I'[simp]: "(\<And>x. x \<in> A \<longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B"
    7.45 +  by (simp add:Pi_def)
    7.46 +
    7.47 +lemma funcsetI: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f \<in> A \<rightarrow> B"
    7.48 +  by (simp add: Pi_def)
    7.49 +
    7.50 +lemma Pi_mem: "f \<in> Pi A B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B x"
    7.51 +  by (simp add: Pi_def)
    7.52 +
    7.53 +lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
    7.54 +  unfolding Pi_def by auto
    7.55 +
    7.56 +lemma PiE [elim]: "f \<in> Pi A B \<Longrightarrow> (f x \<in> B x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> Q"
    7.57 +  by (auto simp: Pi_def)
    7.58 +
    7.59 +lemma Pi_cong: "(\<And>w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B"
    7.60 +  by (auto simp: Pi_def)
    7.61 +
    7.62 +lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
    7.63 +  by auto
    7.64 +
    7.65 +lemma funcset_mem: "f \<in> A \<rightarrow> B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B"
    7.66 +  by (simp add: Pi_def)
    7.67 +
    7.68 +lemma funcset_image: "f \<in> A \<rightarrow> B \<Longrightarrow> f ` A \<subseteq> B"
    7.69 +  by auto
    7.70 +
    7.71 +lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
    7.72 +  by auto
    7.73 +
    7.74 +lemma Pi_eq_empty[simp]: "(\<Pi> x \<in> A. B x) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})"
    7.75 +  apply (simp add: Pi_def)
    7.76 +  apply auto
    7.77 +  txt \<open>Converse direction requires Axiom of Choice to exhibit a function
    7.78 +  picking an element from each non-empty @{term "B x"}\<close>
    7.79 +  apply (drule_tac x = "\<lambda>u. SOME y. y \<in> B u" in spec)
    7.80 +  apply auto
    7.81 +  apply (cut_tac P = "\<lambda>y. y \<in> B x" in some_eq_ex)
    7.82 +  apply auto
    7.83 +  done
    7.84 +
    7.85 +lemma Pi_empty [simp]: "Pi {} B = UNIV"
    7.86 +  by (simp add: Pi_def)
    7.87 +
    7.88 +lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
    7.89 +  by auto
    7.90 +
    7.91 +lemma Pi_UN:
    7.92 +  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
    7.93 +  assumes "finite I"
    7.94 +    and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
    7.95 +  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
    7.96 +proof (intro set_eqI iffI)
    7.97 +  fix f
    7.98 +  assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
    7.99 +  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
   7.100 +    by auto
   7.101 +  from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
   7.102 +    by auto
   7.103 +  obtain k where k: "n i \<le> k" if "i \<in> I" for i
   7.104 +    using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
   7.105 +  have "f \<in> Pi I (A k)"
   7.106 +  proof (intro Pi_I)
   7.107 +    fix i
   7.108 +    assume "i \<in> I"
   7.109 +    from mono[OF this, of "n i" k] k[OF this] n[OF this]
   7.110 +    show "f i \<in> A k i" by auto
   7.111 +  qed
   7.112 +  then show "f \<in> (\<Union>n. Pi I (A n))"
   7.113 +    by auto
   7.114 +qed auto
   7.115 +
   7.116 +lemma Pi_UNIV [simp]: "A \<rightarrow> UNIV = UNIV"
   7.117 +  by (simp add: Pi_def)
   7.118 +
   7.119 +text \<open>Covariance of Pi-sets in their second argument\<close>
   7.120 +lemma Pi_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi A B \<subseteq> Pi A C"
   7.121 +  by auto
   7.122 +
   7.123 +text \<open>Contravariance of Pi-sets in their first argument\<close>
   7.124 +lemma Pi_anti_mono: "A' \<subseteq> A \<Longrightarrow> Pi A B \<subseteq> Pi A' B"
   7.125 +  by auto
   7.126 +
   7.127 +lemma prod_final:
   7.128 +  assumes 1: "fst \<circ> f \<in> Pi A B"
   7.129 +    and 2: "snd \<circ> f \<in> Pi A C"
   7.130 +  shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
   7.131 +proof (rule Pi_I)
   7.132 +  fix z
   7.133 +  assume z: "z \<in> A"
   7.134 +  have "f z = (fst (f z), snd (f z))"
   7.135 +    by simp
   7.136 +  also have "\<dots> \<in> B z \<times> C z"
   7.137 +    by (metis SigmaI PiE o_apply 1 2 z)
   7.138 +  finally show "f z \<in> B z \<times> C z" .
   7.139 +qed
   7.140 +
   7.141 +lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
   7.142 +  by (auto simp: Pi_def)
   7.143 +
   7.144 +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"
   7.145 +  by (auto simp: Pi_def)
   7.146 +
   7.147 +lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
   7.148 +  by (auto simp: Pi_def)
   7.149 +
   7.150 +lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
   7.151 +  by (auto simp: Pi_def)
   7.152 +
   7.153 +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"
   7.154 +  apply auto
   7.155 +  apply (drule_tac x=x in Pi_mem)
   7.156 +  apply (simp_all split: if_split_asm)
   7.157 +  apply (drule_tac x=i in Pi_mem)
   7.158 +  apply (auto dest!: Pi_mem)
   7.159 +  done
   7.160 +
   7.161 +
   7.162 +subsection \<open>Composition With a Restricted Domain: @{term compose}\<close>
   7.163 +
   7.164 +lemma funcset_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> g \<in> B \<rightarrow> C \<Longrightarrow> compose A g f \<in> A \<rightarrow> C"
   7.165 +  by (simp add: Pi_def compose_def restrict_def)
   7.166 +
   7.167 +lemma compose_assoc:
   7.168 +  assumes "f \<in> A \<rightarrow> B"
   7.169 +    and "g \<in> B \<rightarrow> C"
   7.170 +    and "h \<in> C \<rightarrow> D"
   7.171 +  shows "compose A h (compose A g f) = compose A (compose B h g) f"
   7.172 +  using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)
   7.173 +
   7.174 +lemma compose_eq: "x \<in> A \<Longrightarrow> compose A g f x = g (f x)"
   7.175 +  by (simp add: compose_def restrict_def)
   7.176 +
   7.177 +lemma surj_compose: "f ` A = B \<Longrightarrow> g ` B = C \<Longrightarrow> compose A g f ` A = C"
   7.178 +  by (auto simp add: image_def compose_eq)
   7.179 +
   7.180 +
   7.181 +subsection \<open>Bounded Abstraction: @{term restrict}\<close>
   7.182 +
   7.183 +lemma restrict_cong: "I = J \<Longrightarrow> (\<And>i. i \<in> J =simp=> f i = g i) \<Longrightarrow> restrict f I = restrict g J"
   7.184 +  by (auto simp: restrict_def fun_eq_iff simp_implies_def)
   7.185 +
   7.186 +lemma restrict_in_funcset: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> A \<rightarrow> B"
   7.187 +  by (simp add: Pi_def restrict_def)
   7.188 +
   7.189 +lemma restrictI[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> Pi A B"
   7.190 +  by (simp add: Pi_def restrict_def)
   7.191 +
   7.192 +lemma restrict_apply[simp]: "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
   7.193 +  by (simp add: restrict_def)
   7.194 +
   7.195 +lemma restrict_apply': "x \<in> A \<Longrightarrow> (\<lambda>y\<in>A. f y) x = f x"
   7.196 +  by simp
   7.197 +
   7.198 +lemma restrict_ext: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
   7.199 +  by (simp add: fun_eq_iff Pi_def restrict_def)
   7.200 +
   7.201 +lemma restrict_UNIV: "restrict f UNIV = f"
   7.202 +  by (simp add: restrict_def)
   7.203 +
   7.204 +lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
   7.205 +  by (simp add: inj_on_def restrict_def)
   7.206 +
   7.207 +lemma Id_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> f \<in> extensional A \<Longrightarrow> compose A (\<lambda>y\<in>B. y) f = f"
   7.208 +  by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)
   7.209 +
   7.210 +lemma compose_Id: "g \<in> A \<rightarrow> B \<Longrightarrow> g \<in> extensional A \<Longrightarrow> compose A g (\<lambda>x\<in>A. x) = g"
   7.211 +  by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)
   7.212 +
   7.213 +lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
   7.214 +  by (auto simp add: restrict_def)
   7.215 +
   7.216 +lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
   7.217 +  unfolding restrict_def by (simp add: fun_eq_iff)
   7.218 +
   7.219 +lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
   7.220 +  by (auto simp: restrict_def)
   7.221 +
   7.222 +lemma restrict_upd[simp]: "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
   7.223 +  by (auto simp: fun_eq_iff)
   7.224 +
   7.225 +lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
   7.226 +  by (auto simp: restrict_def Pi_def)
   7.227 +
   7.228 +
   7.229 +subsection \<open>Bijections Between Sets\<close>
   7.230 +
   7.231 +text \<open>The definition of @{const bij_betw} is in \<open>Fun.thy\<close>, but most of
   7.232 +the theorems belong here, or need at least @{term Hilbert_Choice}.\<close>
   7.233 +
   7.234 +lemma bij_betwI:
   7.235 +  assumes "f \<in> A \<rightarrow> B"
   7.236 +    and "g \<in> B \<rightarrow> A"
   7.237 +    and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x"
   7.238 +    and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y"
   7.239 +  shows "bij_betw f A B"
   7.240 +  unfolding bij_betw_def
   7.241 +proof
   7.242 +  show "inj_on f A"
   7.243 +    by (metis g_f inj_on_def)
   7.244 +  have "f ` A \<subseteq> B"
   7.245 +    using \<open>f \<in> A \<rightarrow> B\<close> by auto
   7.246 +  moreover
   7.247 +  have "B \<subseteq> f ` A"
   7.248 +    by auto (metis Pi_mem \<open>g \<in> B \<rightarrow> A\<close> f_g image_iff)
   7.249 +  ultimately show "f ` A = B"
   7.250 +    by blast
   7.251 +qed
   7.252 +
   7.253 +lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
   7.254 +  by (auto simp add: bij_betw_def)
   7.255 +
   7.256 +lemma inj_on_compose: "bij_betw f A B \<Longrightarrow> inj_on g B \<Longrightarrow> inj_on (compose A g f) A"
   7.257 +  by (auto simp add: bij_betw_def inj_on_def compose_eq)
   7.258 +
   7.259 +lemma bij_betw_compose: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (compose A g f) A C"
   7.260 +  apply (simp add: bij_betw_def compose_eq inj_on_compose)
   7.261 +  apply (auto simp add: compose_def image_def)
   7.262 +  done
   7.263 +
   7.264 +lemma bij_betw_restrict_eq [simp]: "bij_betw (restrict f A) A B = bij_betw f A B"
   7.265 +  by (simp add: bij_betw_def)
   7.266 +
   7.267 +
   7.268 +subsection \<open>Extensionality\<close>
   7.269 +
   7.270 +lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
   7.271 +  unfolding extensional_def by auto
   7.272 +
   7.273 +lemma extensional_arb: "f \<in> extensional A \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = undefined"
   7.274 +  by (simp add: extensional_def)
   7.275 +
   7.276 +lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
   7.277 +  by (simp add: restrict_def extensional_def)
   7.278 +
   7.279 +lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
   7.280 +  by (simp add: compose_def)
   7.281 +
   7.282 +lemma extensionalityI:
   7.283 +  assumes "f \<in> extensional A"
   7.284 +    and "g \<in> extensional A"
   7.285 +    and "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
   7.286 +  shows "f = g"
   7.287 +  using assms by (force simp add: fun_eq_iff extensional_def)
   7.288 +
   7.289 +lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
   7.290 +  by (rule extensionalityI[OF restrict_extensional]) auto
   7.291 +
   7.292 +lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B"
   7.293 +  unfolding extensional_def by auto
   7.294 +
   7.295 +lemma inv_into_funcset: "f ` A = B \<Longrightarrow> (\<lambda>x\<in>B. inv_into A f x) \<in> B \<rightarrow> A"
   7.296 +  by (unfold inv_into_def) (fast intro: someI2)
   7.297 +
   7.298 +lemma compose_inv_into_id: "bij_betw f A B \<Longrightarrow> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
   7.299 +  apply (simp add: bij_betw_def compose_def)
   7.300 +  apply (rule restrict_ext, auto)
   7.301 +  done
   7.302 +
   7.303 +lemma compose_id_inv_into: "f ` A = B \<Longrightarrow> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
   7.304 +  apply (simp add: compose_def)
   7.305 +  apply (rule restrict_ext)
   7.306 +  apply (simp add: f_inv_into_f)
   7.307 +  done
   7.308 +
   7.309 +lemma extensional_insert[intro, simp]:
   7.310 +  assumes "a \<in> extensional (insert i I)"
   7.311 +  shows "a(i := b) \<in> extensional (insert i I)"
   7.312 +  using assms unfolding extensional_def by auto
   7.313 +
   7.314 +lemma extensional_Int[simp]: "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
   7.315 +  unfolding extensional_def by auto
   7.316 +
   7.317 +lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
   7.318 +  by (auto simp: extensional_def)
   7.319 +
   7.320 +lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
   7.321 +  unfolding restrict_def extensional_def by auto
   7.322 +
   7.323 +lemma extensional_insert_undefined[intro, simp]:
   7.324 +  "a \<in> extensional (insert i I) \<Longrightarrow> a(i := undefined) \<in> extensional I"
   7.325 +  unfolding extensional_def by auto
   7.326 +
   7.327 +lemma extensional_insert_cancel[intro, simp]:
   7.328 +  "a \<in> extensional I \<Longrightarrow> a \<in> extensional (insert i I)"
   7.329 +  unfolding extensional_def by auto
   7.330 +
   7.331 +
   7.332 +subsection \<open>Cardinality\<close>
   7.333 +
   7.334 +lemma card_inj: "f \<in> A \<rightarrow> B \<Longrightarrow> inj_on f A \<Longrightarrow> finite B \<Longrightarrow> card A \<le> card B"
   7.335 +  by (rule card_inj_on_le) auto
   7.336 +
   7.337 +lemma card_bij:
   7.338 +  assumes "f \<in> A \<rightarrow> B" "inj_on f A"
   7.339 +    and "g \<in> B \<rightarrow> A" "inj_on g B"
   7.340 +    and "finite A" "finite B"
   7.341 +  shows "card A = card B"
   7.342 +  using assms by (blast intro: card_inj order_antisym)
   7.343 +
   7.344 +
   7.345 +subsection \<open>Extensional Function Spaces\<close>
   7.346 +
   7.347 +definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
   7.348 +  where "PiE S T = Pi S T \<inter> extensional S"
   7.349 +
   7.350 +abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
   7.351 +
   7.352 +syntax
   7.353 +  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
   7.354 +translations
   7.355 +  "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
   7.356 +
   7.357 +abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
   7.358 +  where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
   7.359 +
   7.360 +lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
   7.361 +  by (simp add: PiE_def)
   7.362 +
   7.363 +lemma PiE_empty_domain[simp]: "Pi\<^sub>E {} T = {\<lambda>x. undefined}"
   7.364 +  unfolding PiE_def by simp
   7.365 +
   7.366 +lemma PiE_UNIV_domain: "Pi\<^sub>E UNIV T = Pi UNIV T"
   7.367 +  unfolding PiE_def by simp
   7.368 +
   7.369 +lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (\<Pi>\<^sub>E i\<in>I. F i) = {}"
   7.370 +  unfolding PiE_def by auto
   7.371 +
   7.372 +lemma PiE_eq_empty_iff: "Pi\<^sub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
   7.373 +proof
   7.374 +  assume "Pi\<^sub>E I F = {}"
   7.375 +  show "\<exists>i\<in>I. F i = {}"
   7.376 +  proof (rule ccontr)
   7.377 +    assume "\<not> ?thesis"
   7.378 +    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)"
   7.379 +      by auto
   7.380 +    from choice[OF this]
   7.381 +    obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" ..
   7.382 +    then have "f \<in> Pi\<^sub>E I F"
   7.383 +      by (auto simp: extensional_def PiE_def)
   7.384 +    with \<open>Pi\<^sub>E I F = {}\<close> show False
   7.385 +      by auto
   7.386 +  qed
   7.387 +qed (auto simp: PiE_def)
   7.388 +
   7.389 +lemma PiE_arb: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
   7.390 +  unfolding PiE_def by auto (auto dest!: extensional_arb)
   7.391 +
   7.392 +lemma PiE_mem: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
   7.393 +  unfolding PiE_def by auto
   7.394 +
   7.395 +lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> Pi\<^sub>E S T \<Longrightarrow> f(x := y) \<in> Pi\<^sub>E (insert x S) T"
   7.396 +  unfolding PiE_def extensional_def by auto
   7.397 +
   7.398 +lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> Pi\<^sub>E (insert x S) T \<Longrightarrow> f(x := undefined) \<in> Pi\<^sub>E S T"
   7.399 +  unfolding PiE_def extensional_def by auto
   7.400 +
   7.401 +lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
   7.402 +proof -
   7.403 +  {
   7.404 +    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<notin> S"
   7.405 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
   7.406 +      by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   7.407 +  }
   7.408 +  moreover
   7.409 +  {
   7.410 +    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<in> S"
   7.411 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
   7.412 +      by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
   7.413 +  }
   7.414 +  ultimately show ?thesis
   7.415 +    by (auto intro: PiE_fun_upd)
   7.416 +qed
   7.417 +
   7.418 +lemma PiE_Int: "Pi\<^sub>E I A \<inter> Pi\<^sub>E I B = Pi\<^sub>E I (\<lambda>x. A x \<inter> B x)"
   7.419 +  by (auto simp: PiE_def)
   7.420 +
   7.421 +lemma PiE_cong: "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^sub>E I A = Pi\<^sub>E I B"
   7.422 +  unfolding PiE_def by (auto simp: Pi_cong)
   7.423 +
   7.424 +lemma PiE_E [elim]:
   7.425 +  assumes "f \<in> Pi\<^sub>E A B"
   7.426 +  obtains "x \<in> A" and "f x \<in> B x"
   7.427 +    | "x \<notin> A" and "f x = undefined"
   7.428 +  using assms by (auto simp: Pi_def PiE_def extensional_def)
   7.429 +
   7.430 +lemma PiE_I[intro!]:
   7.431 +  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> Pi\<^sub>E A B"
   7.432 +  by (simp add: PiE_def extensional_def)
   7.433 +
   7.434 +lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi\<^sub>E A B \<subseteq> Pi\<^sub>E A C"
   7.435 +  by auto
   7.436 +
   7.437 +lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
   7.438 +  by (simp add: PiE_def Pi_iff)
   7.439 +
   7.440 +lemma PiE_restrict[simp]:  "f \<in> Pi\<^sub>E A B \<Longrightarrow> restrict f A = f"
   7.441 +  by (simp add: extensional_restrict PiE_def)
   7.442 +
   7.443 +lemma restrict_PiE[simp]: "restrict f I \<in> Pi\<^sub>E I S \<longleftrightarrow> f \<in> Pi I S"
   7.444 +  by (auto simp: PiE_iff)
   7.445 +
   7.446 +lemma PiE_eq_subset:
   7.447 +  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   7.448 +    and eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   7.449 +    and "i \<in> I"
   7.450 +  shows "F i \<subseteq> F' i"
   7.451 +proof
   7.452 +  fix x
   7.453 +  assume "x \<in> F i"
   7.454 +  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)"
   7.455 +    by auto
   7.456 +  from choice[OF this] obtain f
   7.457 +    where f: " \<forall>j. (j \<in> I \<longrightarrow> f j \<in> F j \<and> (i = j \<longrightarrow> x = f j)) \<and> (j \<notin> I \<longrightarrow> f j = undefined)" ..
   7.458 +  then have "f \<in> Pi\<^sub>E I F"
   7.459 +    by (auto simp: extensional_def PiE_def)
   7.460 +  then have "f \<in> Pi\<^sub>E I F'"
   7.461 +    using assms by simp
   7.462 +  then show "x \<in> F' i"
   7.463 +    using f \<open>i \<in> I\<close> by (auto simp: PiE_def)
   7.464 +qed
   7.465 +
   7.466 +lemma PiE_eq_iff_not_empty:
   7.467 +  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   7.468 +  shows "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
   7.469 +proof (intro iffI ballI)
   7.470 +  fix i
   7.471 +  assume eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   7.472 +  assume i: "i \<in> I"
   7.473 +  show "F i = F' i"
   7.474 +    using PiE_eq_subset[of I F F', OF ne eq i]
   7.475 +    using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
   7.476 +    by auto
   7.477 +qed (auto simp: PiE_def)
   7.478 +
   7.479 +lemma PiE_eq_iff:
   7.480 +  "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   7.481 +proof (intro iffI disjCI)
   7.482 +  assume eq[simp]: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   7.483 +  assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   7.484 +  then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
   7.485 +    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
   7.486 +  with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i"
   7.487 +    by auto
   7.488 +next
   7.489 +  assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
   7.490 +  then show "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   7.491 +    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
   7.492 +qed
   7.493 +
   7.494 +lemma extensional_funcset_fun_upd_restricts_rangeI:
   7.495 +  "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f \<in> (insert x S) \<rightarrow>\<^sub>E T \<Longrightarrow> f(x := undefined) \<in> S \<rightarrow>\<^sub>E (T - {f x})"
   7.496 +  unfolding extensional_funcset_def extensional_def
   7.497 +  apply auto
   7.498 +  apply (case_tac "x = xa")
   7.499 +  apply auto
   7.500 +  done
   7.501 +
   7.502 +lemma extensional_funcset_fun_upd_extends_rangeI:
   7.503 +  assumes "a \<in> T" "f \<in> S \<rightarrow>\<^sub>E (T - {a})"
   7.504 +  shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E  T"
   7.505 +  using assms unfolding extensional_funcset_def extensional_def by auto
   7.506 +
   7.507 +
   7.508 +subsubsection \<open>Injective Extensional Function Spaces\<close>
   7.509 +
   7.510 +lemma extensional_funcset_fun_upd_inj_onI:
   7.511 +  assumes "f \<in> S \<rightarrow>\<^sub>E (T - {a})"
   7.512 +    and "inj_on f S"
   7.513 +  shows "inj_on (f(x := a)) S"
   7.514 +  using assms
   7.515 +  unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
   7.516 +
   7.517 +lemma extensional_funcset_extend_domain_inj_on_eq:
   7.518 +  assumes "x \<notin> S"
   7.519 +  shows "{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} =
   7.520 +    (\<lambda>(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
   7.521 +  using assms
   7.522 +  apply (auto del: PiE_I PiE_E)
   7.523 +  apply (auto intro: extensional_funcset_fun_upd_inj_onI
   7.524 +    extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
   7.525 +  apply (auto simp add: image_iff inj_on_def)
   7.526 +  apply (rule_tac x="xa x" in exI)
   7.527 +  apply (auto intro: PiE_mem del: PiE_I PiE_E)
   7.528 +  apply (rule_tac x="xa(x := undefined)" in exI)
   7.529 +  apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
   7.530 +  apply (auto dest!: PiE_mem split: if_split_asm)
   7.531 +  done
   7.532 +
   7.533 +lemma extensional_funcset_extend_domain_inj_onI:
   7.534 +  assumes "x \<notin> S"
   7.535 +  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
   7.536 +  using assms
   7.537 +  apply (auto intro!: inj_onI)
   7.538 +  apply (metis fun_upd_same)
   7.539 +  apply (metis assms PiE_arb fun_upd_triv fun_upd_upd)
   7.540 +  done
   7.541 +
   7.542 +
   7.543 +subsubsection \<open>Cardinality\<close>
   7.544 +
   7.545 +lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (\<Pi>\<^sub>E i \<in> S. T i)"
   7.546 +  by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
   7.547 +
   7.548 +lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^sub>E S T)"
   7.549 +proof (safe intro!: inj_onI ext)
   7.550 +  fix f y g z
   7.551 +  assume "x \<notin> S"
   7.552 +  assume fg: "f \<in> Pi\<^sub>E S T" "g \<in> Pi\<^sub>E S T"
   7.553 +  assume "f(x := y) = g(x := z)"
   7.554 +  then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
   7.555 +    unfolding fun_eq_iff by auto
   7.556 +  from this[of x] show "y = z" by simp
   7.557 +  fix i from *[of i] \<open>x \<notin> S\<close> fg show "f i = g i"
   7.558 +    by (auto split: if_split_asm simp: PiE_def extensional_def)
   7.559 +qed
   7.560 +
   7.561 +lemma card_PiE: "finite S \<Longrightarrow> card (\<Pi>\<^sub>E i \<in> S. T i) = (\<Prod> i\<in>S. card (T i))"
   7.562 +proof (induct rule: finite_induct)
   7.563 +  case empty
   7.564 +  then show ?case by auto
   7.565 +next
   7.566 +  case (insert x S)
   7.567 +  then show ?case
   7.568 +    by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
   7.569 +qed
   7.570 +
   7.571 +end
     8.1 --- a/src/HOL/Library/Library.thy	Tue May 15 06:23:12 2018 +0200
     8.2 +++ b/src/HOL/Library/Library.thy	Tue May 15 11:33:43 2018 +0200
     8.3 @@ -30,6 +30,7 @@
     8.4    Finite_Map
     8.5    Float
     8.6    FSet
     8.7 +  FuncSet
     8.8    Function_Division
     8.9    Fun_Lexorder
    8.10    Going_To_Filter
     9.1 --- a/src/HOL/Metis_Examples/Abstraction.thy	Tue May 15 06:23:12 2018 +0200
     9.2 +++ b/src/HOL/Metis_Examples/Abstraction.thy	Tue May 15 11:33:43 2018 +0200
     9.3 @@ -8,7 +8,7 @@
     9.4  section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close>
     9.5  
     9.6  theory Abstraction
     9.7 -imports HOL.FuncSet
     9.8 +imports "HOL-Library.FuncSet"
     9.9  begin
    9.10  
    9.11  (* For Christoph Benzm├╝ller *)
    10.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Tue May 15 06:23:12 2018 +0200
    10.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Tue May 15 11:33:43 2018 +0200
    10.3 @@ -8,7 +8,7 @@
    10.4  section \<open>Metis Example Featuring the Full Theorem of Tarski\<close>
    10.5  
    10.6  theory Tarski
    10.7 -imports Main HOL.FuncSet
    10.8 +imports Main "HOL-Library.FuncSet"
    10.9  begin
   10.10  
   10.11  declare [[metis_new_skolem]]
    11.1 --- a/src/HOL/Number_Theory/Prime_Powers.thy	Tue May 15 06:23:12 2018 +0200
    11.2 +++ b/src/HOL/Number_Theory/Prime_Powers.thy	Tue May 15 11:33:43 2018 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  *)
    11.5  section \<open>Prime powers\<close>
    11.6  theory Prime_Powers
    11.7 -  imports Complex_Main "HOL-Computational_Algebra.Primes"
    11.8 +  imports Complex_Main "HOL-Computational_Algebra.Primes" "HOL-Library.FuncSet"
    11.9  begin
   11.10  
   11.11  definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where
    12.1 --- a/src/HOL/Vector_Spaces.thy	Tue May 15 06:23:12 2018 +0200
    12.2 +++ b/src/HOL/Vector_Spaces.thy	Tue May 15 11:33:43 2018 +0200
    12.3 @@ -9,7 +9,7 @@
    12.4  section \<open>Vector Spaces\<close>
    12.5  
    12.6  theory Vector_Spaces
    12.7 -  imports Modules FuncSet
    12.8 +  imports Modules
    12.9  begin
   12.10  
   12.11  lemma isomorphism_expand:
   12.12 @@ -847,7 +847,7 @@
   12.13  lemma linear_exists_left_inverse_on:
   12.14    assumes lf: "linear s1 s2 f"
   12.15    assumes V: "vs1.subspace V" and f: "inj_on f V"
   12.16 -  shows "\<exists>g\<in>UNIV \<rightarrow> V. linear s2 s1 g \<and> (\<forall>v\<in>V. g (f v) = v)"
   12.17 +  shows "\<exists>g. g ` UNIV \<subseteq> V \<and> linear s2 s1 g \<and> (\<forall>v\<in>V. g (f v) = v)"
   12.18  proof -
   12.19    interpret linear s1 s2 f by fact
   12.20    obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
   12.21 @@ -856,7 +856,7 @@
   12.22    have f: "inj_on f (vs1.span B)"
   12.23      using f unfolding V_eq .
   12.24    show ?thesis
   12.25 -  proof (intro bexI ballI conjI)
   12.26 +  proof (intro exI ballI conjI)
   12.27      interpret p: vector_space_pair s2 s1 by unfold_locales
   12.28      have fB: "vs2.independent (f ` B)"
   12.29        using independent_injective_image[OF B f] .
   12.30 @@ -868,7 +868,7 @@
   12.31      moreover have "the_inv_into B f ` f ` B = B"
   12.32        by (auto simp: image_comp comp_def the_inv_into_f_f inj_on_subset[OF f vs1.span_superset]
   12.33            cong: image_cong)
   12.34 -    ultimately show "?g \<in> UNIV \<rightarrow> V"
   12.35 +    ultimately show "?g ` UNIV \<subseteq> V"
   12.36        by (auto simp: V_eq)
   12.37      have "(?g \<circ> f) v = id v" if "v \<in> vs1.span B" for v
   12.38      proof (rule vector_space_pair.linear_eq_on[where x=v])
   12.39 @@ -890,7 +890,7 @@
   12.40  lemma linear_exists_right_inverse_on:
   12.41    assumes lf: "linear s1 s2 f"
   12.42    assumes "vs1.subspace V"
   12.43 -  shows "\<exists>g\<in>UNIV \<rightarrow> V. linear s2 s1 g \<and> (\<forall>v\<in>f ` V. f (g v) = v)"
   12.44 +  shows "\<exists>g. g ` UNIV \<subseteq> V \<and> linear s2 s1 g \<and> (\<forall>v\<in>f ` V. f (g v) = v)"
   12.45  proof -
   12.46    obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
   12.47      using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>]
   12.48 @@ -900,7 +900,7 @@
   12.49    then have "\<forall>v\<in>C. \<exists>b\<in>B. v = f b" by auto
   12.50    then obtain g where g: "\<And>v. v \<in> C \<Longrightarrow> g v \<in> B" "\<And>v. v \<in> C \<Longrightarrow> f (g v) = v" by metis
   12.51    show ?thesis
   12.52 -  proof (intro bexI ballI conjI)
   12.53 +  proof (intro exI ballI conjI)
   12.54      interpret p: vector_space_pair s2 s1 by unfold_locales
   12.55      let ?g = "p.construct C g"
   12.56      show "linear ( *b) ( *a) ?g"
   12.57 @@ -908,7 +908,7 @@
   12.58      have "?g v \<in> vs1.span (g ` C)" for v
   12.59        by (rule p.construct_in_span[OF C])
   12.60      also have "\<dots> \<subseteq> V" unfolding V_eq using g by (intro vs1.span_mono) auto
   12.61 -    finally show "?g \<in> UNIV \<rightarrow> V" by auto
   12.62 +    finally show "?g ` UNIV \<subseteq> V" by auto
   12.63      have "(f \<circ> ?g) v = id v" if v: "v \<in> f ` V" for v
   12.64      proof (rule vector_space_pair.linear_eq_on[where x=v])
   12.65        show "vector_space_pair ( *b) ( *b)" by unfold_locales
   12.66 @@ -946,7 +946,7 @@
   12.67    assumes sf: "vs2.span T \<subseteq> f`vs1.span S"
   12.68    shows "\<exists>g. range g \<subseteq> vs1.span S \<and> linear s2 s1 g \<and> (\<forall>x\<in>vs2.span T. f (g x) = x)"
   12.69    using linear_exists_right_inverse_on[OF lf vs1.subspace_span, of S] sf
   12.70 -  by (auto simp: linear_iff_module_hom)
   12.71 +  by (force simp: linear_iff_module_hom)
   12.72  
   12.73  lemma linear_surjective_right_inverse: "linear s1 s2 f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear s2 s1 g \<and> f \<circ> g = id"
   12.74    using linear_surj_right_inverse[of f UNIV UNIV]
    13.1 --- a/src/HOL/ex/Ballot.thy	Tue May 15 06:23:12 2018 +0200
    13.2 +++ b/src/HOL/ex/Ballot.thy	Tue May 15 11:33:43 2018 +0200
    13.3 @@ -8,6 +8,7 @@
    13.4  theory Ballot
    13.5  imports
    13.6    Complex_Main
    13.7 +  "HOL-Library.FuncSet"
    13.8  begin
    13.9  
   13.10  subsection \<open>Preliminaries\<close>
    14.1 --- a/src/HOL/ex/Birthday_Paradox.thy	Tue May 15 06:23:12 2018 +0200
    14.2 +++ b/src/HOL/ex/Birthday_Paradox.thy	Tue May 15 11:33:43 2018 +0200
    14.3 @@ -5,7 +5,7 @@
    14.4  section \<open>A Formulation of the Birthday Paradox\<close>
    14.5  
    14.6  theory Birthday_Paradox
    14.7 -imports Main HOL.FuncSet
    14.8 +imports Main "HOL-Library.FuncSet"
    14.9  begin
   14.10  
   14.11  section \<open>Cardinality\<close>
    15.1 --- a/src/HOL/ex/Tarski.thy	Tue May 15 06:23:12 2018 +0200
    15.2 +++ b/src/HOL/ex/Tarski.thy	Tue May 15 11:33:43 2018 +0200
    15.3 @@ -5,7 +5,7 @@
    15.4  section \<open>The Full Theorem of Tarski\<close>
    15.5  
    15.6  theory Tarski
    15.7 -imports Main HOL.FuncSet
    15.8 +imports Main "HOL-Library.FuncSet"
    15.9  begin
   15.10  
   15.11  text \<open>