src/HOL/Library/FuncSet.thy
 changeset 58783 c6348a062131 parent 58606 9c66f7c541fb child 58881 b9556a055632
```     1.1 --- a/src/HOL/Library/FuncSet.thy	Sat Oct 25 11:53:35 2014 +0200
1.2 +++ b/src/HOL/Library/FuncSet.thy	Sat Oct 25 21:16:32 2014 +0200
1.3 @@ -2,144 +2,143 @@
1.4      Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
1.5  *)
1.6
1.7 -header {* Pi and Function Sets *}
1.8 +header \<open>Pi and Function Sets\<close>
1.9
1.10  theory FuncSet
1.11  imports Hilbert_Choice Main
1.12  begin
1.13
1.14 -definition
1.15 -  Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where
1.16 -  "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}"
1.17 +definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
1.18 +  where "Pi A B = {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x}"
1.19
1.20 -definition
1.21 -  extensional :: "'a set => ('a => 'b) set" where
1.22 -  "extensional A = {f. \<forall>x. x~:A --> f x = undefined}"
1.23 +definition extensional :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) set"
1.24 +  where "extensional A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = undefined}"
1.25
1.26 -definition
1.27 -  "restrict" :: "['a => 'b, 'a set] => ('a => 'b)" where
1.28 -  "restrict f A = (%x. if x \<in> A then f x else undefined)"
1.29 +definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
1.30 +  where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)"
1.31
1.32 -abbreviation
1.33 -  funcset :: "['a set, 'b set] => ('a => 'b) set"
1.34 -    (infixr "->" 60) where
1.35 -  "A -> B \<equiv> Pi A (%_. B)"
1.36 +abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "->" 60)
1.37 +  where "A -> B \<equiv> Pi A (\<lambda>_. B)"
1.38
1.39  notation (xsymbols)
1.40    funcset  (infixr "\<rightarrow>" 60)
1.41
1.42  syntax
1.43 -  "_Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
1.44 -  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
1.45 -
1.46 +  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
1.47 +  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
1.48  syntax (xsymbols)
1.49 -  "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
1.50 -  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
1.51 -
1.52 +  "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
1.53 +  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
1.54  syntax (HTML output)
1.55 -  "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
1.56 -  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
1.57 -
1.58 +  "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
1.59 +  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
1.60  translations
1.61 -  "PI x:A. B" \<rightleftharpoons> "CONST Pi A (%x. B)"
1.62 -  "%x:A. f" \<rightleftharpoons> "CONST restrict (%x. f) A"
1.63 +  "\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
1.64 +  "\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
1.65
1.66 -definition
1.67 -  "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" where
1.68 -  "compose A g f = (\<lambda>x\<in>A. g (f x))"
1.69 +definition "compose" :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c)"
1.70 +  where "compose A g f = (\<lambda>x\<in>A. g (f x))"
1.71
1.72
1.73 -subsection{*Basic Properties of @{term Pi}*}
1.74 +subsection \<open>Basic Properties of @{term Pi}\<close>
1.75
1.76 -lemma Pi_I[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
1.77 +lemma Pi_I[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B"
1.78    by (simp add: Pi_def)
1.79
1.80 -lemma Pi_I'[simp]: "(!!x. x : A --> f x : B x) ==> f : Pi A B"
1.82 +lemma Pi_I'[simp]: "(\<And>x. x \<in> A \<longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi A B"
1.83 +  by (simp add:Pi_def)
1.84
1.85 -lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
1.86 +lemma funcsetI: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f \<in> A \<rightarrow> B"
1.87    by (simp add: Pi_def)
1.88
1.89 -lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
1.90 +lemma Pi_mem: "f \<in> Pi A B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B x"
1.91    by (simp add: Pi_def)
1.92
1.93  lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
1.94    unfolding Pi_def by auto
1.95
1.96 -lemma PiE [elim]:
1.97 -  "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
1.98 -by(auto simp: Pi_def)
1.99 +lemma PiE [elim]: "f \<in> Pi A B \<Longrightarrow> (f x \<in> B x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> Q"
1.100 +  by (auto simp: Pi_def)
1.101
1.102 -lemma Pi_cong:
1.103 -  "(\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B"
1.104 +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"
1.105    by (auto simp: Pi_def)
1.106
1.107  lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
1.108    by auto
1.109
1.110 -lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
1.111 +lemma funcset_mem: "f \<in> A \<rightarrow> B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B"
1.112    by (simp add: Pi_def)
1.113
1.114 -lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
1.115 +lemma funcset_image: "f \<in> A \<rightarrow> B \<Longrightarrow> f ` A \<subseteq> B"
1.116    by auto
1.117
1.118  lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
1.119    by auto
1.120
1.121 -lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B x = {})"
1.122 -apply (simp add: Pi_def, auto)
1.123 -txt{*Converse direction requires Axiom of Choice to exhibit a function
1.124 -picking an element from each non-empty @{term "B x"}*}
1.125 -apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto)
1.126 -apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
1.127 -done
1.128 +lemma Pi_eq_empty[simp]: "(\<Pi> x \<in> A. B x) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})"
1.129 +  apply (simp add: Pi_def)
1.130 +  apply auto
1.131 +  txt \<open>Converse direction requires Axiom of Choice to exhibit a function
1.132 +  picking an element from each non-empty @{term "B x"}\<close>
1.133 +  apply (drule_tac x = "\<lambda>u. SOME y. y \<in> B u" in spec)
1.134 +  apply auto
1.135 +  apply (cut_tac P = "\<lambda>y. y \<in> B x" in some_eq_ex)
1.136 +  apply auto
1.137 +  done
1.138
1.139  lemma Pi_empty [simp]: "Pi {} B = UNIV"
1.140 -by (simp add: Pi_def)
1.141 +  by (simp add: Pi_def)
1.142
1.143  lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
1.144    by auto
1.145
1.146  lemma Pi_UN:
1.147    fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
1.148 -  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.149 +  assumes "finite I"
1.150 +    and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
1.151    shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
1.152  proof (intro set_eqI iffI)
1.153 -  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
1.154 -  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
1.155 -  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
1.156 +  fix f
1.157 +  assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
1.158 +  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
1.159 +    by auto
1.160 +  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)"
1.161 +    by auto
1.162    obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
1.163 -    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
1.164 +    using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
1.165    have "f \<in> Pi I (A k)"
1.166    proof (intro Pi_I)
1.167 -    fix i assume "i \<in> I"
1.168 +    fix i
1.169 +    assume "i \<in> I"
1.170      from mono[OF this, of "n i" k] k[OF this] n[OF this]
1.171      show "f i \<in> A k i" by auto
1.172    qed
1.173 -  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
1.174 +  then show "f \<in> (\<Union>n. Pi I (A n))"
1.175 +    by auto
1.176  qed auto
1.177
1.178 -lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
1.179 -by (simp add: Pi_def)
1.180 +lemma Pi_UNIV [simp]: "A \<rightarrow> UNIV = UNIV"
1.181 +  by (simp add: Pi_def)
1.182
1.183 -text{*Covariance of Pi-sets in their second argument*}
1.184 -lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
1.185 -by auto
1.186 +text \<open>Covariance of Pi-sets in their second argument\<close>
1.187 +lemma Pi_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi A B \<subseteq> Pi A C"
1.188 +  by auto
1.189
1.190 -text{*Contravariance of Pi-sets in their first argument*}
1.191 -lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
1.192 -by auto
1.193 +text \<open>Contravariance of Pi-sets in their first argument\<close>
1.194 +lemma Pi_anti_mono: "A' \<subseteq> A \<Longrightarrow> Pi A B \<subseteq> Pi A' B"
1.195 +  by auto
1.196
1.197  lemma prod_final:
1.198 -  assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
1.199 +  assumes 1: "fst \<circ> f \<in> Pi A B"
1.200 +    and 2: "snd \<circ> f \<in> Pi A C"
1.201    shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
1.202 -proof (rule Pi_I)
1.203 +proof (rule Pi_I)
1.204    fix z
1.205 -  assume z: "z \<in> A"
1.206 -  have "f z = (fst (f z), snd (f z))"
1.207 +  assume z: "z \<in> A"
1.208 +  have "f z = (fst (f z), snd (f z))"
1.209      by simp
1.210 -  also have "...  \<in> B z \<times> C z"
1.211 -    by (metis SigmaI PiE o_apply 1 2 z)
1.212 +  also have "\<dots> \<in> B z \<times> C z"
1.213 +    by (metis SigmaI PiE o_apply 1 2 z)
1.214    finally show "f z \<in> B z \<times> C z" .
1.215  qed
1.216
1.217 @@ -163,25 +162,27 @@
1.218    apply (auto dest!: Pi_mem)
1.219    done
1.220
1.221 -subsection{*Composition With a Restricted Domain: @{term compose}*}
1.222 +
1.223 +subsection \<open>Composition With a Restricted Domain: @{term compose}\<close>
1.224
1.225 -lemma funcset_compose:
1.226 -  "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
1.227 -by (simp add: Pi_def compose_def restrict_def)
1.228 +lemma funcset_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> g \<in> B \<rightarrow> C \<Longrightarrow> compose A g f \<in> A \<rightarrow> C"
1.229 +  by (simp add: Pi_def compose_def restrict_def)
1.230
1.231  lemma compose_assoc:
1.232 -    "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
1.233 -      ==> compose A h (compose A g f) = compose A (compose B h g) f"
1.234 -by (simp add: fun_eq_iff Pi_def compose_def restrict_def)
1.235 +  assumes "f \<in> A \<rightarrow> B"
1.236 +    and "g \<in> B \<rightarrow> C"
1.237 +    and "h \<in> C \<rightarrow> D"
1.238 +  shows "compose A h (compose A g f) = compose A (compose B h g) f"
1.239 +  using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)
1.240
1.241 -lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
1.242 -by (simp add: compose_def restrict_def)
1.243 +lemma compose_eq: "x \<in> A \<Longrightarrow> compose A g f x = g (f x)"
1.244 +  by (simp add: compose_def restrict_def)
1.245
1.246 -lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
1.247 +lemma surj_compose: "f ` A = B \<Longrightarrow> g ` B = C \<Longrightarrow> compose A g f ` A = C"
1.248    by (auto simp add: image_def compose_eq)
1.249
1.250
1.251 -subsection{*Bounded Abstraction: @{term restrict}*}
1.252 +subsection \<open>Bounded Abstraction: @{term restrict}\<close>
1.253
1.254  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"
1.255    by (simp add: Pi_def restrict_def)
1.256 @@ -195,8 +196,7 @@
1.257  lemma restrict_apply': "x \<in> A \<Longrightarrow> (\<lambda>y\<in>A. f y) x = f x"
1.258    by simp
1.259
1.260 -lemma restrict_ext:
1.261 -    "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
1.262 +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)"
1.263    by (simp add: fun_eq_iff Pi_def restrict_def)
1.264
1.265  lemma restrict_UNIV: "restrict f UNIV = f"
1.266 @@ -205,12 +205,10 @@
1.267  lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
1.268    by (simp add: inj_on_def restrict_def)
1.269
1.270 -lemma Id_compose:
1.271 -    "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
1.272 +lemma Id_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> f \<in> extensional A \<Longrightarrow> compose A (\<lambda>y\<in>B. y) f = f"
1.273    by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)
1.274
1.275 -lemma compose_Id:
1.276 -    "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
1.277 +lemma compose_Id: "g \<in> A \<rightarrow> B \<Longrightarrow> g \<in> extensional A \<Longrightarrow> compose A g (\<lambda>x\<in>A. x) = g"
1.278    by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)
1.279
1.280  lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
1.281 @@ -222,99 +220,99 @@
1.282  lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
1.283    by (auto simp: restrict_def)
1.284
1.285 -lemma restrict_upd[simp]:
1.286 -  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
1.287 +lemma restrict_upd[simp]: "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
1.288    by (auto simp: fun_eq_iff)
1.289
1.290  lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
1.291    by (auto simp: restrict_def Pi_def)
1.292
1.293
1.294 -subsection{*Bijections Between Sets*}
1.295 +subsection \<open>Bijections Between Sets\<close>
1.296
1.297 -text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
1.298 -the theorems belong here, or need at least @{term Hilbert_Choice}.*}
1.299 +text \<open>The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
1.300 +the theorems belong here, or need at least @{term Hilbert_Choice}.\<close>
1.301
1.302  lemma bij_betwI:
1.303 -assumes "f \<in> A \<rightarrow> B" and "g \<in> B \<rightarrow> A"
1.304 -    and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x" and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y"
1.305 -shows "bij_betw f A B"
1.306 -unfolding bij_betw_def
1.307 +  assumes "f \<in> A \<rightarrow> B"
1.308 +    and "g \<in> B \<rightarrow> A"
1.309 +    and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x"
1.310 +    and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y"
1.311 +  shows "bij_betw f A B"
1.312 +  unfolding bij_betw_def
1.313  proof
1.314 -  show "inj_on f A" by (metis g_f inj_on_def)
1.315 -next
1.316 -  have "f ` A \<subseteq> B" using `f \<in> A \<rightarrow> B` by auto
1.317 +  show "inj_on f A"
1.318 +    by (metis g_f inj_on_def)
1.319 +  have "f ` A \<subseteq> B"
1.320 +    using \<open>f \<in> A \<rightarrow> B\<close> by auto
1.321    moreover
1.322 -  have "B \<subseteq> f ` A" by auto (metis Pi_mem `g \<in> B \<rightarrow> A` f_g image_iff)
1.323 -  ultimately show "f ` A = B" by blast
1.324 +  have "B \<subseteq> f ` A"
1.325 +    by auto (metis Pi_mem \<open>g \<in> B \<rightarrow> A\<close> f_g image_iff)
1.326 +  ultimately show "f ` A = B"
1.327 +    by blast
1.328  qed
1.329
1.330  lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
1.331 -by (auto simp add: bij_betw_def)
1.332 +  by (auto simp add: bij_betw_def)
1.333
1.334 -lemma inj_on_compose:
1.335 -  "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
1.336 -by (auto simp add: bij_betw_def inj_on_def compose_eq)
1.337 +lemma inj_on_compose: "bij_betw f A B \<Longrightarrow> inj_on g B \<Longrightarrow> inj_on (compose A g f) A"
1.338 +  by (auto simp add: bij_betw_def inj_on_def compose_eq)
1.339
1.340 -lemma bij_betw_compose:
1.341 -  "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
1.342 -apply (simp add: bij_betw_def compose_eq inj_on_compose)
1.343 -apply (auto simp add: compose_def image_def)
1.344 -done
1.345 +lemma bij_betw_compose: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (compose A g f) A C"
1.346 +  apply (simp add: bij_betw_def compose_eq inj_on_compose)
1.347 +  apply (auto simp add: compose_def image_def)
1.348 +  done
1.349
1.350 -lemma bij_betw_restrict_eq [simp]:
1.351 -  "bij_betw (restrict f A) A B = bij_betw f A B"
1.352 -by (simp add: bij_betw_def)
1.353 +lemma bij_betw_restrict_eq [simp]: "bij_betw (restrict f A) A B = bij_betw f A B"
1.354 +  by (simp add: bij_betw_def)
1.355
1.356
1.357 -subsection{*Extensionality*}
1.358 +subsection \<open>Extensionality\<close>
1.359
1.360  lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
1.361    unfolding extensional_def by auto
1.362
1.363 -lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
1.364 -by (simp add: extensional_def)
1.365 +lemma extensional_arb: "f \<in> extensional A \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = undefined"
1.366 +  by (simp add: extensional_def)
1.367
1.368  lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
1.369 -by (simp add: restrict_def extensional_def)
1.370 +  by (simp add: restrict_def extensional_def)
1.371
1.372  lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
1.373 -by (simp add: compose_def)
1.374 +  by (simp add: compose_def)
1.375
1.376  lemma extensionalityI:
1.377 -  "[| f \<in> extensional A; g \<in> extensional A;
1.378 -      !!x. x\<in>A ==> f x = g x |] ==> f = g"
1.379 -by (force simp add: fun_eq_iff extensional_def)
1.380 +  assumes "f \<in> extensional A"
1.381 +    and "g \<in> extensional A"
1.382 +    and "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
1.383 +  shows "f = g"
1.384 +  using assms by (force simp add: fun_eq_iff extensional_def)
1.385
1.386  lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
1.387 -by(rule extensionalityI[OF restrict_extensional]) auto
1.388 +  by (rule extensionalityI[OF restrict_extensional]) auto
1.389
1.390  lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B"
1.391    unfolding extensional_def by auto
1.392
1.393 -lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
1.394 -by (unfold inv_into_def) (fast intro: someI2)
1.395 +lemma inv_into_funcset: "f ` A = B \<Longrightarrow> (\<lambda>x\<in>B. inv_into A f x) \<in> B \<rightarrow> A"
1.396 +  by (unfold inv_into_def) (fast intro: someI2)
1.397
1.398 -lemma compose_inv_into_id:
1.399 -  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
1.400 -apply (simp add: bij_betw_def compose_def)
1.401 -apply (rule restrict_ext, auto)
1.402 -done
1.403 +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)"
1.404 +  apply (simp add: bij_betw_def compose_def)
1.405 +  apply (rule restrict_ext, auto)
1.406 +  done
1.407
1.408 -lemma compose_id_inv_into:
1.409 -  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
1.410 -apply (simp add: compose_def)
1.411 -apply (rule restrict_ext)
1.412 -apply (simp add: f_inv_into_f)
1.413 -done
1.414 +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)"
1.415 +  apply (simp add: compose_def)
1.416 +  apply (rule restrict_ext)
1.417 +  apply (simp add: f_inv_into_f)
1.418 +  done
1.419
1.420  lemma extensional_insert[intro, simp]:
1.421    assumes "a \<in> extensional (insert i I)"
1.422    shows "a(i := b) \<in> extensional (insert i I)"
1.423    using assms unfolding extensional_def by auto
1.424
1.425 -lemma extensional_Int[simp]:
1.426 -  "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
1.427 +lemma extensional_Int[simp]: "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
1.428    unfolding extensional_def by auto
1.429
1.430  lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
1.431 @@ -332,61 +330,66 @@
1.432    unfolding extensional_def by auto
1.433
1.434
1.435 -subsection{*Cardinality*}
1.436 +subsection \<open>Cardinality\<close>
1.437
1.438 -lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
1.439 -by (rule card_inj_on_le) auto
1.440 +lemma card_inj: "f \<in> A \<rightarrow> B \<Longrightarrow> inj_on f A \<Longrightarrow> finite B \<Longrightarrow> card A \<le> card B"
1.441 +  by (rule card_inj_on_le) auto
1.442
1.443  lemma card_bij:
1.444 -  "[|f \<in> A\<rightarrow>B; inj_on f A;
1.445 -     g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
1.446 -by (blast intro: card_inj order_antisym)
1.447 +  assumes "f \<in> A \<rightarrow> B" "inj_on f A"
1.448 +    and "g \<in> B \<rightarrow> A" "inj_on g B"
1.449 +    and "finite A" "finite B"
1.450 +  shows "card A = card B"
1.451 +  using assms by (blast intro: card_inj order_antisym)
1.452
1.453 -subsection {* Extensional Function Spaces *}
1.454 +
1.455 +subsection \<open>Extensional Function Spaces\<close>
1.456
1.457 -definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" where
1.458 -  "PiE S T = Pi S T \<inter> extensional S"
1.459 +definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
1.460 +  where "PiE S T = Pi S T \<inter> extensional S"
1.461
1.462  abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
1.463
1.464 -syntax "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
1.465 -
1.466 -syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
1.467 +syntax
1.468 +  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
1.469 +syntax (xsymbols)
1.470 +  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
1.471 +syntax (HTML output)
1.472 +  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
1.473 +translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
1.474
1.475 -syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
1.476 -
1.477 -translations "PIE x:A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (%x. B)"
1.478 -
1.479 -abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60) where
1.480 -  "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
1.481 +abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60)
1.482 +  where "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
1.483
1.484  notation (xsymbols)
1.485    extensional_funcset  (infixr "\<rightarrow>\<^sub>E" 60)
1.486
1.487 -lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) \<inter> extensional S"
1.488 +lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
1.489    by (simp add: PiE_def)
1.490
1.491 -lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
1.492 +lemma PiE_empty_domain[simp]: "PiE {} T = {\<lambda>x. undefined}"
1.493    unfolding PiE_def by simp
1.494
1.495  lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T"
1.496    unfolding PiE_def by simp
1.497
1.498 -lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}"
1.499 +lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (\<Pi>\<^sub>E i\<in>I. F i) = {}"
1.500    unfolding PiE_def by auto
1.501
1.502 -lemma PiE_eq_empty_iff:
1.503 -  "Pi\<^sub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
1.504 +lemma PiE_eq_empty_iff: "Pi\<^sub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
1.505  proof
1.506    assume "Pi\<^sub>E I F = {}"
1.507    show "\<exists>i\<in>I. F i = {}"
1.508    proof (rule ccontr)
1.509      assume "\<not> ?thesis"
1.510 -    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
1.511 +    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)"
1.512 +      by auto
1.513      from choice[OF this]
1.514      obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" ..
1.515 -    then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
1.516 -    with `Pi\<^sub>E I F = {}` show False by auto
1.517 +    then have "f \<in> Pi\<^sub>E I F"
1.518 +      by (auto simp: extensional_def PiE_def)
1.519 +    with \<open>Pi\<^sub>E I F = {}\<close> show False
1.520 +      by auto
1.521    qed
1.522  qed (auto simp: PiE_def)
1.523
1.524 @@ -411,21 +414,24 @@
1.525      with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.526        by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
1.527    }
1.528 -  then show ?thesis using assms by (auto intro: PiE_fun_upd)
1.529 +  then show ?thesis
1.530 +    using assms by (auto intro: PiE_fun_upd)
1.531  qed
1.532
1.533 -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)"
1.534 +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)"
1.535    by (auto simp: PiE_def)
1.536
1.537 -lemma PiE_cong:
1.538 -  "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^sub>E I A = Pi\<^sub>E I B"
1.539 +lemma PiE_cong: "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^sub>E I A = Pi\<^sub>E I B"
1.540    unfolding PiE_def by (auto simp: Pi_cong)
1.541
1.542  lemma PiE_E [elim]:
1.543 -  "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.544 -by(auto simp: Pi_def PiE_def extensional_def)
1.545 +  assumes "f \<in> PiE A B"
1.546 +  obtains "x \<in> A" and "f x \<in> B x"
1.547 +    | "x \<notin> A" and "f x = undefined"
1.548 +  using assms by (auto simp: Pi_def PiE_def extensional_def)
1.549
1.550 -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.551 +lemma PiE_I[intro!]:
1.552 +  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> PiE A B"
1.553    by (simp add: PiE_def extensional_def)
1.554
1.555  lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
1.556 @@ -442,24 +448,31 @@
1.557
1.558  lemma PiE_eq_subset:
1.559    assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
1.560 -  assumes eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'" and "i \<in> I"
1.561 +    and eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
1.562 +    and "i \<in> I"
1.563    shows "F i \<subseteq> F' i"
1.564  proof
1.565 -  fix x assume "x \<in> F i"
1.566 -  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))"
1.567 +  fix x
1.568 +  assume "x \<in> F i"
1.569 +  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)"
1.570      by auto
1.571    from choice[OF this] obtain f
1.572      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)" ..
1.573 -  then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
1.574 -  then have "f \<in> Pi\<^sub>E I F'" using assms by simp
1.575 -  then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
1.576 +  then have "f \<in> Pi\<^sub>E I F"
1.577 +    by (auto simp: extensional_def PiE_def)
1.578 +  then have "f \<in> Pi\<^sub>E I F'"
1.579 +    using assms by simp
1.580 +  then show "x \<in> F' i"
1.581 +    using f \<open>i \<in> I\<close> by (auto simp: PiE_def)
1.582  qed
1.583
1.584  lemma PiE_eq_iff_not_empty:
1.585    assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
1.586    shows "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
1.587  proof (intro iffI ballI)
1.588 -  fix i assume eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'" and i: "i \<in> I"
1.589 +  fix i
1.590 +  assume eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
1.591 +  assume i: "i \<in> I"
1.592    show "F i = F' i"
1.593      using PiE_eq_subset[of I F F', OF ne eq i]
1.594      using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
1.595 @@ -473,15 +486,16 @@
1.596    assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
1.597    then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
1.598      using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
1.599 -  with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
1.600 +  with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i"
1.601 +    by auto
1.602  next
1.603    assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
1.604    then show "Pi\<^sub>E I F = Pi\<^sub>E I F'"
1.605      using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
1.606  qed
1.607
1.608 -lemma extensional_funcset_fun_upd_restricts_rangeI:
1.609 -  "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f : (insert x S) \<rightarrow>\<^sub>E T ==> f(x := undefined) : S \<rightarrow>\<^sub>E (T - {f x})"
1.610 +lemma extensional_funcset_fun_upd_restricts_rangeI:
1.611 +  "\<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})"
1.612    unfolding extensional_funcset_def extensional_def
1.613    apply auto
1.614    apply (case_tac "x = xa")
1.615 @@ -490,66 +504,70 @@
1.616
1.617  lemma extensional_funcset_fun_upd_extends_rangeI:
1.618    assumes "a \<in> T" "f \<in> S \<rightarrow>\<^sub>E (T - {a})"
1.619 -  shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^sub>E  T"
1.620 +  shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E  T"
1.621    using assms unfolding extensional_funcset_def extensional_def by auto
1.622
1.623 -subsubsection {* Injective Extensional Function Spaces *}
1.624 +
1.625 +subsubsection \<open>Injective Extensional Function Spaces\<close>
1.626
1.627  lemma extensional_funcset_fun_upd_inj_onI:
1.628 -  assumes "f \<in> S \<rightarrow>\<^sub>E (T - {a})" "inj_on f S"
1.629 +  assumes "f \<in> S \<rightarrow>\<^sub>E (T - {a})"
1.630 +    and "inj_on f S"
1.631    shows "inj_on (f(x := a)) S"
1.632 -  using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
1.633 +  using assms
1.634 +  unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
1.635
1.636  lemma extensional_funcset_extend_domain_inj_on_eq:
1.637    assumes "x \<notin> S"
1.638 -  shows"{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} =
1.639 -    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
1.640 -proof -
1.641 -  from assms show ?thesis
1.642 -    apply (auto del: PiE_I PiE_E)
1.643 -    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
1.644 -    apply (auto simp add: image_iff inj_on_def)
1.645 -    apply (rule_tac x="xa x" in exI)
1.646 -    apply (auto intro: PiE_mem del: PiE_I PiE_E)
1.647 -    apply (rule_tac x="xa(x := undefined)" in exI)
1.648 -    apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
1.649 -    apply (auto dest!: PiE_mem split: split_if_asm)
1.650 -    done
1.651 -qed
1.652 +  shows "{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} =
1.653 +    (\<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}"
1.654 +  using assms
1.655 +  apply (auto del: PiE_I PiE_E)
1.656 +  apply (auto intro: extensional_funcset_fun_upd_inj_onI
1.657 +    extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
1.658 +  apply (auto simp add: image_iff inj_on_def)
1.659 +  apply (rule_tac x="xa x" in exI)
1.660 +  apply (auto intro: PiE_mem del: PiE_I PiE_E)
1.661 +  apply (rule_tac x="xa(x := undefined)" in exI)
1.662 +  apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
1.663 +  apply (auto dest!: PiE_mem split: split_if_asm)
1.664 +  done
1.665
1.666  lemma extensional_funcset_extend_domain_inj_onI:
1.667    assumes "x \<notin> S"
1.668    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}"
1.669 -proof -
1.670 -  from assms show ?thesis
1.671 -    apply (auto intro!: inj_onI)
1.672 -    apply (metis fun_upd_same)
1.673 -    by (metis assms PiE_arb fun_upd_triv fun_upd_upd)
1.674 -qed
1.675 -
1.676 +  using assms
1.677 +  apply (auto intro!: inj_onI)
1.678 +  apply (metis fun_upd_same)
1.679 +  apply (metis assms PiE_arb fun_upd_triv fun_upd_upd)
1.680 +  done
1.681
1.682 -subsubsection {* Cardinality *}
1.683
1.684 -lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (PIE i : S. T i)"
1.685 +subsubsection \<open>Cardinality\<close>
1.686 +
1.687 +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)"
1.688    by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
1.689
1.690  lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^sub>E S T)"
1.691  proof (safe intro!: inj_onI ext)
1.692 -  fix f y g z assume "x \<notin> S" and fg: "f \<in> Pi\<^sub>E S T" "g \<in> Pi\<^sub>E S T"
1.693 +  fix f y g z
1.694 +  assume "x \<notin> S"
1.695 +  assume fg: "f \<in> Pi\<^sub>E S T" "g \<in> Pi\<^sub>E S T"
1.696    assume "f(x := y) = g(x := z)"
1.697    then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
1.698      unfolding fun_eq_iff by auto
1.699    from this[of x] show "y = z" by simp
1.700 -  fix i from *[of i] `x \<notin> S` fg show "f i = g i"
1.701 +  fix i from *[of i] \<open>x \<notin> S\<close> fg show "f i = g i"
1.702      by (auto split: split_if_asm simp: PiE_def extensional_def)
1.703  qed
1.704
1.705 -lemma card_PiE:
1.706 -  "finite S \<Longrightarrow> card (PIE i : S. T i) = (\<Prod> i\<in>S. card (T i))"
1.707 +lemma card_PiE: "finite S \<Longrightarrow> card (\<Pi>\<^sub>E i \<in> S. T i) = (\<Prod> i\<in>S. card (T i))"
1.708  proof (induct rule: finite_induct)
1.709 -  case empty then show ?case by auto
1.710 +  case empty
1.711 +  then show ?case by auto
1.712  next
1.713 -  case (insert x S) then show ?case
1.714 +  case (insert x S)
1.715 +  then show ?case
1.716      by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
1.717  qed
1.718
```