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: