src/HOL/Fun.thy
 changeset 49905 a81f95693c68 parent 49739 13aa6d8268ec child 51598 5dbe537087aa
```     1.1 --- a/src/HOL/Fun.thy	Thu Oct 18 09:17:00 2012 +0200
1.2 +++ b/src/HOL/Fun.thy	Thu Oct 18 09:19:37 2012 +0200
1.3 @@ -188,25 +188,30 @@
1.4    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
1.5           INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
1.6    shows "inj_on f (\<Union> i \<in> I. A i)"
1.7 -proof(unfold inj_on_def UNION_eq, auto)
1.8 -  fix i j x y
1.9 -  assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
1.10 -         and ***: "f x = f y"
1.11 -  show "x = y"
1.12 -  proof-
1.13 -    {assume "A i \<le> A j"
1.14 -     with ** have "x \<in> A j" by auto
1.15 -     with INJ * ** *** have ?thesis
1.16 -     by(auto simp add: inj_on_def)
1.17 -    }
1.18 -    moreover
1.19 -    {assume "A j \<le> A i"
1.20 -     with ** have "y \<in> A i" by auto
1.21 -     with INJ * ** *** have ?thesis
1.22 -     by(auto simp add: inj_on_def)
1.23 -    }
1.24 -    ultimately show ?thesis using  CH * by blast
1.25 -  qed
1.26 +proof -
1.27 +  {
1.28 +    fix i j x y
1.29 +    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
1.30 +      and ***: "f x = f y"
1.31 +    have "x = y"
1.32 +    proof -
1.33 +      {
1.34 +        assume "A i \<le> A j"
1.35 +        with ** have "x \<in> A j" by auto
1.36 +        with INJ * ** *** have ?thesis
1.37 +        by(auto simp add: inj_on_def)
1.38 +      }
1.39 +      moreover
1.40 +      {
1.41 +        assume "A j \<le> A i"
1.42 +        with ** have "y \<in> A i" by auto
1.43 +        with INJ * ** *** have ?thesis
1.44 +        by(auto simp add: inj_on_def)
1.45 +      }
1.46 +      ultimately show ?thesis using CH * by blast
1.47 +    qed
1.48 +  }
1.49 +  then show ?thesis by (unfold inj_on_def UNION_eq) auto
1.50  qed
1.51
1.52  lemma surj_id: "surj id"
1.53 @@ -416,7 +421,7 @@
1.54    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
1.55           BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
1.56    shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
1.57 -proof(unfold bij_betw_def, auto simp add: image_def)
1.58 +proof (unfold bij_betw_def, auto)
1.59    have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
1.60    using BIJ bij_betw_def[of f] by auto
1.61    thus "inj_on f (\<Union> i \<in> I. A i)"
1.62 @@ -430,8 +435,9 @@
1.63    fix i x'
1.64    assume *: "i \<in> I" "x' \<in> A' i"
1.65    hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
1.66 -  thus "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
1.67 -  using * by blast
1.68 +  then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
1.69 +    using * by blast
1.70 +  then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by (simp add: image_def)
1.71  qed
1.72
1.73  lemma bij_betw_subset:
```