author paulson Wed Feb 09 18:32:28 2005 +0100 (2005-02-09) changeset 15510 9de204d7b699 parent 15509 c54970704285 child 15511 8c1910887be3
new foldSet proofs
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Fun.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 09 12:08:46 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 09 18:32:28 2005 +0100
1.3 @@ -100,18 +100,23 @@
1.4
1.5  text{* Finite sets are the images of initial segments of natural numbers: *}
1.6
1.7 -lemma finite_imp_nat_seg_image:
1.8 -assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}"
1.9 +lemma finite_imp_nat_seg_image_inj_on:
1.10 +  assumes fin: "finite A"
1.11 +  shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
1.12  using fin
1.13  proof induct
1.14    case empty
1.15 -  show ?case
1.16 -  proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed
1.17 +  show ?case
1.18 +  proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp
1.19 +  qed
1.20  next
1.21    case (insert a A)
1.22 -  from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast
1.23 -  hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}"
1.24 -    by (auto simp add:image_def Ball_def)
1.25 +  have notinA: "a \<notin> A" .
1.26 +  from insert.hyps obtain n f
1.27 +    where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
1.28 +  hence "insert a A = f(n:=a) ` {i. i < Suc n}"
1.29 +        "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
1.30 +    by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
1.31    thus ?case by blast
1.32  qed
1.33
1.34 @@ -137,7 +142,7 @@
1.35
1.36  lemma finite_conv_nat_seg_image:
1.37    "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
1.38 -by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite)
1.39 +by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
1.40
1.41  subsubsection{* Finiteness and set theoretic constructions *}
1.42
1.43 @@ -522,207 +527,142 @@
1.44
1.45  subsubsection{*From @{term foldSet} to @{term fold}*}
1.46
1.47 -(* only used in the next lemma, but in there twice *)
1.48 -lemma card_lemma: assumes A1: "A = insert b B" and notinB: "b \<notin> B" and
1.49 -  card: "A = h`{i. i<Suc n}" and new: "\<not>(EX k<n. h n = h k)"
1.50 -shows "EX h. B = h`{i. i<n}" (is "EX h. ?P h")
1.51 -proof
1.52 -  let ?h = "%i. if h i = b then h n else h i"
1.53 -  show "B = ?h`{i. i<n}" (is "_ = ?r")
1.54 -  proof
1.55 -    show "B \<subseteq> ?r"
1.56 -    proof
1.57 -      fix u assume "u \<in> B"
1.58 -      hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
1.59 -      then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
1.60 -	using card by(auto simp:image_def)
1.61 -      show "u \<in> ?r"
1.62 -      proof cases
1.63 -	assume "i\<^isub>u < n"
1.64 -	thus ?thesis using unotb by fastsimp
1.65 -      next
1.66 -	assume "\<not> i\<^isub>u < n"
1.67 -	with below have [simp]: "i\<^isub>u = n" by arith
1.68 -	obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
1.69 -	  using A1 card by blast
1.70 -	have "i\<^isub>k < n"
1.71 -	proof (rule ccontr)
1.72 -	  assume "\<not> i\<^isub>k < n"
1.73 -	  hence "i\<^isub>k = n" using i\<^isub>k by arith
1.74 -	  thus False using unotb by simp
1.75 -	qed
1.76 -	thus ?thesis by(auto simp add:image_def)
1.77 -      qed
1.78 +lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
1.79 +by (auto simp add: less_Suc_eq)
1.80 +
1.81 +lemma insert_image_inj_on_eq:
1.82 +     "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A;
1.83 +        inj_on h {i. i < Suc m}|]
1.84 +      ==> A = h ` {i. i < m}"
1.85 +apply (auto simp add: image_less_Suc inj_on_def)
1.86 +apply (blast intro: less_trans)
1.87 +done
1.88 +
1.89 +lemma insert_inj_onE:
1.90 +  assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A"
1.91 +      and inj_on: "inj_on h {i::nat. i<n}"
1.92 +  shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
1.93 +proof (cases n)
1.94 +  case 0 thus ?thesis using aA by auto
1.95 +next
1.96 +  case (Suc m)
1.97 +  have nSuc: "n = Suc m" .
1.98 +  have mlessn: "m<n" by (simp add: nSuc)
1.99 +  have "a \<in> h ` {i. i < n}" using aA by blast
1.100 +  then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast
1.101 +  show ?thesis
1.102 +  proof cases
1.103 +    assume eq: "k=m"
1.104 +    show ?thesis
1.105 +    proof (intro exI conjI)
1.106 +      show "inj_on h {i::nat. i<m}" using inj_on
1.107 +	by (simp add: nSuc inj_on_def)
1.108 +      show "m<n" by (rule mlessn)
1.109 +      show "A = h ` {i. i < m}" using aA anot nSuc hkeq eq inj_on
1.110 +	by (rules intro: insert_image_inj_on_eq)
1.111      qed
1.112    next
1.113 -    show "?r \<subseteq> B"
1.114 -    proof
1.115 -      fix u assume "u \<in> ?r"
1.116 -      then obtain i\<^isub>u where below: "i\<^isub>u < n" and
1.117 -        or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
1.118 -	by(auto simp:image_def)
1.119 -      from or show "u \<in> B"
1.120 -      proof
1.121 -	assume [simp]: "b = h i\<^isub>u \<and> u = h n"
1.122 -	have "u \<in> A" using card by auto
1.123 -        moreover have "u \<noteq> b" using new below by auto
1.124 -	ultimately show "u \<in> B" using A1 by blast
1.125 -      next
1.126 -	assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
1.127 -	moreover hence "u \<in> A" using card below by auto
1.128 -	ultimately show "u \<in> B" using A1 by blast
1.129 +    assume diff: "k~=m"
1.130 +    hence klessm: "k<m" using nSuc klessn by arith
1.131 +    have hdiff: "h k ~= h m" using diff inj_on klessn mlessn
1.132 +	by (auto simp add: inj_on_def)
1.133 +    let ?hm = "swap k m h"
1.134 +    have inj_onhm_n: "inj_on ?hm {i. i < n}" using klessn mlessn
1.135 +      by (simp add: inj_on_swap_iff inj_on)
1.136 +    hence inj_onhm_m: "inj_on ?hm {i. i < m}"
1.137 +      by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
1.138 +    show ?thesis
1.139 +    proof (intro exI conjI)
1.140 +      show "inj_on ?hm {i. i < m}" by (rule inj_onhm_m)
1.141 +      show "m<n" by (simp add: nSuc)
1.142 +      show "A = ?hm ` {i. i < m}"
1.143 +      proof (rule insert_image_inj_on_eq)
1.144 +	show "inj_on (swap k m h) {i. i < Suc m}" using inj_onhm_n
1.145 +	  by (simp add: nSuc)
1.146 +        show "?hm m \<notin> A" by (simp add: swap_def hkeq anot)
1.147 +        show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
1.148 +          using aA hkeq diff hdiff nSuc
1.149 +	  by (auto simp add: swap_def image_less_Suc fun_upd_image klessm
1.150 +                             inj_on_image_set_diff [OF inj_on])
1.151        qed
1.152      qed
1.153    qed
1.154  qed
1.155
1.156  lemma (in ACf) foldSet_determ_aux:
1.157 -  "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
1.158 +  "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n};
1.159 +                (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
1.160     \<Longrightarrow> x' = x"
1.161 -proof (induct n)
1.162 -  case 0 thus ?case by auto
1.163 -next
1.164 -  case (Suc n)
1.165 -  have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g z; (A,x') \<in> foldSet f g z\<rbrakk>
1.166 -           \<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}"
1.167 -  and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" .
1.168 -  show ?case
1.169 -  proof cases
1.170 -    assume "EX k<n. h n = h k"
1.171 -      --{*@{term h} is not injective, so the cardinality has not increased*}
1.172 -    hence card': "A = h ` {i. i < n}"
1.173 -      using card by (auto simp:image_def less_Suc_eq)
1.174 -    show ?thesis by(rule IH[OF card' Afoldx Afoldy])
1.175 -  next
1.176 -    assume new: "\<not>(EX k<n. h n = h k)"
1.177 -    show ?thesis
1.178 -    proof (rule foldSet.cases[OF Afoldx])
1.179 -      assume "(A, x) = ({}, z)"  --{*fold of a singleton set*}
1.180 -      thus "x' = x" using Afoldy by auto
1.181 +proof (induct n rule: less_induct)
1.182 +  case (less n)
1.183 +    have IH: "!!m h A x x'.
1.184 +               \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m};
1.185 +                (A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" .
1.186 +    have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z"
1.187 +     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
1.188 +    show ?case
1.189 +    proof (rule foldSet.cases [OF Afoldx])
1.190 +      assume "(A, x) = ({}, z)"
1.191 +      with Afoldx' show "x' = x" by blast
1.192      next
1.193 -      fix B b y
1.194 -      assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
1.195 -	and y: "(B,y) \<in> foldSet f g z" and notinB: "b \<notin> B"
1.196 -      hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
1.197 -      show ?thesis
1.198 -      proof (rule foldSet.cases[OF Afoldy])
1.199 -	assume "(A,x') = ({}, z)"
1.200 -	thus ?thesis using A1 by auto
1.201 +      fix B b u
1.202 +      assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B"
1.203 +         and Bu: "(B,u) \<in> foldSet f g z"
1.204 +      hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto
1.205 +      show "x'=x"
1.206 +      proof (rule foldSet.cases [OF Afoldx'])
1.207 +        assume "(A, x') = ({}, z)"
1.208 +        with AbB show "x' = x" by blast
1.209        next
1.210 -	fix C c r
1.211 -	assume eq2: "(A,x') = (insert c C, g c \<cdot> r)"
1.212 -	  and r: "(C,r) \<in> foldSet f g z" and notinC: "c \<notin> C"
1.213 -	hence A2: "A = insert c C" and x': "x' = g c \<cdot> r" by auto
1.214 -	obtain hB where lessB: "B = hB ` {i. i<n}"
1.215 -	  using card_lemma[OF A1 notinB card new] by auto
1.216 -	obtain hC where lessC: "C = hC ` {i. i<n}"
1.217 -	  using card_lemma[OF A2 notinC card new] by auto
1.218 -	show ?thesis
1.219 +	fix C c v
1.220 +	assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C"
1.221 +	   and Cv: "(C,v) \<in> foldSet f g z"
1.222 +	hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto
1.223 +	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
1.224 +        from insert_inj_onE [OF Beq notinB injh]
1.225 +        obtain hB mB where inj_onB: "inj_on hB {i. i < mB}"
1.226 +                     and Beq: "B = hB ` {i. i < mB}"
1.227 +                     and lessB: "mB < n" by auto
1.228 +	from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
1.229 +        from insert_inj_onE [OF Ceq notinC injh]
1.230 +        obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
1.231 +                       and Ceq: "C = hC ` {i. i < mC}"
1.232 +                       and lessC: "mC < n" by auto
1.233 +	show "x'=x"
1.234  	proof cases
1.235 -	  assume "b = c"
1.236 -	  then moreover have "B = C" using A1 A2 notinB notinC by auto
1.237 -	  ultimately show ?thesis using IH[OF lessB] y r x x' by auto
1.238 +          assume "b=c"
1.239 +	  then moreover have "B = C" using AbB AcC notinB notinC by auto
1.240 +	  ultimately show ?thesis  using Bu Cv x x' IH[OF lessC Ceq inj_onC]
1.241 +            by auto
1.242  	next
1.243  	  assume diff: "b \<noteq> c"
1.244  	  let ?D = "B - {c}"
1.245  	  have B: "B = insert c ?D" and C: "C = insert b ?D"
1.246 -	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
1.247 +	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
1.248  	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
1.249 -	  with A1 have "finite ?D" by simp
1.250 +	  with AbB have "finite ?D" by simp
1.251  	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
1.252  	    using finite_imp_foldSet by rules
1.253  	  moreover have cinB: "c \<in> B" using B by auto
1.254  	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
1.255  	    by(rule Diff1_foldSet)
1.256 -	  hence "g c \<cdot> d = y" by(rule IH[OF lessB y])
1.257 -          moreover have "g b \<cdot> d = r"
1.258 -	  proof (rule IH[OF lessC r])
1.259 -	    show "(C,g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
1.260 +	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu])
1.261 +          moreover have "g b \<cdot> d = v"
1.262 +	  proof (rule IH[OF lessC Ceq inj_onC Cv])
1.263 +	    show "(C, g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
1.264  	      by fastsimp
1.265  	  qed
1.266 -	  ultimately show ?thesis using x x' by(auto simp:AC)
1.267 +	  ultimately show ?thesis using x x' by (auto simp: AC)
1.268  	qed
1.269        qed
1.270      qed
1.271    qed
1.272 -qed
1.273
1.274 -(* The same proof, but using card
1.275 -lemma (in ACf) foldSet_determ_aux:
1.276 -  "!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
1.277 -   \<Longrightarrow> x' = x"
1.278 -proof (induct n)
1.279 -  case 0 thus ?case by simp
1.280 -next
1.281 -  case (Suc n)
1.282 -  have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
1.283 -           \<Longrightarrow> x' = x" and card: "card A < Suc n"
1.284 -  and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
1.285 -  from card have "card A < n \<or> card A = n" by arith
1.286 -  thus ?case
1.287 -  proof
1.288 -    assume less: "card A < n"
1.289 -    show ?thesis by(rule IH[OF less Afoldx Afoldy])
1.290 -  next
1.291 -    assume cardA: "card A = n"
1.292 -    show ?thesis
1.293 -    proof (rule foldSet.cases[OF Afoldx])
1.294 -      assume "(A, x) = ({}, e)"
1.295 -      thus "x' = x" using Afoldy by auto
1.296 -    next
1.297 -      fix B b y
1.298 -      assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
1.299 -	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
1.300 -      hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
1.301 -      show ?thesis
1.302 -      proof (rule foldSet.cases[OF Afoldy])
1.303 -	assume "(A,x') = ({}, e)"
1.304 -	thus ?thesis using A1 by auto
1.305 -      next
1.306 -	fix C c z
1.307 -	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
1.308 -	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
1.309 -	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
1.310 -	have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
1.311 -	with cardA A1 notinB have less: "card B < n" by simp
1.312 -	show ?thesis
1.313 -	proof cases
1.314 -	  assume "b = c"
1.315 -	  then moreover have "B = C" using A1 A2 notinB notinC by auto
1.316 -	  ultimately show ?thesis using IH[OF less] y z x x' by auto
1.317 -	next
1.318 -	  assume diff: "b \<noteq> c"
1.319 -	  let ?D = "B - {c}"
1.320 -	  have B: "B = insert c ?D" and C: "C = insert b ?D"
1.321 -	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
1.322 -	  have "finite ?D" using finA A1 by simp
1.323 -	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
1.324 -	    using finite_imp_foldSet by rules
1.325 -	  moreover have cinB: "c \<in> B" using B by auto
1.326 -	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
1.327 -	    by(rule Diff1_foldSet)
1.328 -	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
1.329 -          moreover have "g b \<cdot> d = z"
1.330 -	  proof (rule IH[OF _ z])
1.331 -	    show "card C < n" using C cardA A1 notinB finA cinB
1.332 -	      by(auto simp:card_Diff1_less)
1.333 -	  next
1.334 -	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
1.335 -	      by fastsimp
1.336 -	  qed
1.337 -	  ultimately show ?thesis using x x' by(auto simp:AC)
1.338 -	qed
1.339 -      qed
1.340 -    qed
1.341 -  qed
1.342 -qed
1.343 -*)
1.344
1.345  lemma (in ACf) foldSet_determ:
1.346 -  "(A, x) : foldSet f g z ==> (A, y) : foldSet f g z ==> y = x"
1.347 -apply(frule foldSet_imp_finite)
1.349 -apply(blast intro: foldSet_determ_aux [rule_format])
1.350 +  "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x"
1.351 +apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on])
1.352 +apply (blast intro: foldSet_determ_aux [rule_format])
1.353  done
1.354
1.355  lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
```
```     2.1 --- a/src/HOL/Fun.thy	Wed Feb 09 12:08:46 2005 +0100
2.2 +++ b/src/HOL/Fun.thy	Wed Feb 09 18:32:28 2005 +0100
2.3 @@ -6,7 +6,7 @@
2.5  *)
2.6
2.7 -theory Fun
2.8 +theory Fun
2.9  imports Typedef
2.10  begin
2.11
2.12 @@ -93,6 +93,16 @@
2.13  lemma id_apply [simp]: "id x = x"
2.15
2.16 +lemma inj_on_id: "inj_on id A"
2.18 +
2.19 +lemma surj_id: "surj id"
2.21 +
2.22 +lemma bij_id: "bij id"
2.23 +by (simp add: bij_def inj_on_id surj_id)
2.24 +
2.25 +
2.26
2.27  subsection{*The Composition Operator: @{term "f \<circ> g"}*}
2.28
2.29 @@ -378,6 +388,10 @@
2.30  lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
2.31  by(fastsimp simp:inj_on_def image_def)
2.32
2.33 +lemma fun_upd_image:
2.34 +     "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
2.35 +by auto
2.36 +
2.37  subsection{* overwrite *}
2.38
2.39  lemma overwrite_emptyset[simp]: "f(g|{}) = f"
2.40 @@ -389,6 +403,58 @@
2.41  lemma overwrite_apply_in[simp]: "a : A ==> (f(g|A)) a = g a"
2.43
2.44 +subsection{* swap *}
2.45 +
2.46 +constdefs
2.47 +  swap :: "['a, 'a, 'a => 'b] => ('a => 'b)"
2.48 +   "swap a b f == f(a := f b, b:= f a)"
2.49 +
2.50 +lemma swap_self: "swap a a f = f"
2.52 +
2.53 +lemma swap_commute: "swap a b f = swap b a f"
2.54 +by (rule ext, simp add: fun_upd_def swap_def)
2.55 +
2.56 +lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
2.57 +by (rule ext, simp add: fun_upd_def swap_def)
2.58 +
2.59 +lemma inj_on_imp_inj_on_swap:
2.60 +     "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
2.61 +by (simp add: inj_on_def swap_def, blast)
2.62 +
2.63 +lemma inj_on_swap_iff [simp]:
2.64 +  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
2.65 +proof
2.66 +  assume "inj_on (swap a b f) A"
2.67 +  with A have "inj_on (swap a b (swap a b f)) A"
2.68 +    by (rules intro: inj_on_imp_inj_on_swap)
2.69 +  thus "inj_on f A" by simp
2.70 +next
2.71 +  assume "inj_on f A"
2.72 +  with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
2.73 +qed
2.74 +
2.75 +lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
2.76 +apply (simp add: surj_def swap_def, clarify)
2.77 +apply (rule_tac P = "y = f b" in case_split_thm, blast)
2.78 +apply (rule_tac P = "y = f a" in case_split_thm, auto)
2.79 +  --{*We don't yet have @{text case_tac}*}
2.80 +done
2.81 +
2.82 +lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
2.83 +proof
2.84 +  assume "surj (swap a b f)"
2.85 +  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
2.86 +  thus "surj f" by simp
2.87 +next
2.88 +  assume "surj f"
2.89 +  thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
2.90 +qed
2.91 +
2.92 +lemma bij_swap_iff: "bij (swap a b f) = bij f"