tuned whitespace;
authorwenzelm
Sat Oct 25 21:16:32 2014 +0200 (2014-10-25)
changeset 58783c6348a062131
parent 58782 7305bad408b5
child 58784 11d726ce599e
tuned whitespace;
more symbols;
src/HOL/Library/FuncSet.thy
     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.81 -by(simp add:Pi_def)
    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