src/HOL/BNF_Wellorder_Embedding.thy
changeset 60585 48fdff264eb2
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jun 26 00:14:10 2015 +0200
     1.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jun 26 10:20:33 2015 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  assumes WELL: "Well_order r" and
     1.5          OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
     1.6         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
     1.7 -shows "inj_on f (\<Union> i \<in> I. A i)"
     1.8 +shows "inj_on f (\<Union>i \<in> I. A i)"
     1.9  proof-
    1.10    have "wo_rel r" using WELL by (simp add: wo_rel_def)
    1.11    hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
    1.12 @@ -487,7 +487,7 @@
    1.13    have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
    1.14    have OF: "wo_rel.ofilter r (underS r a)"
    1.15    by (auto simp add: Well wo_rel.underS_ofilter)
    1.16 -  hence UN: "underS r a = (\<Union>  b \<in> underS r a. under r b)"
    1.17 +  hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)"
    1.18    using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
    1.19    (* Gather facts about elements of underS r a *)
    1.20    {fix b assume *: "b \<in> underS r a"
    1.21 @@ -520,13 +520,13 @@
    1.22    (*  *)
    1.23    have OF': "wo_rel.ofilter r' (f`(underS r a))"
    1.24    proof-
    1.25 -    have "f`(underS r a) = f`(\<Union>  b \<in> underS r a. under r b)"
    1.26 +    have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)"
    1.27      using UN by auto
    1.28 -    also have "\<dots> = (\<Union>  b \<in> underS r a. f`(under r b))" by blast
    1.29 -    also have "\<dots> = (\<Union>  b \<in> underS r a. (under r' (f b)))"
    1.30 +    also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast
    1.31 +    also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))"
    1.32      using bFact by auto
    1.33      finally
    1.34 -    have "f`(underS r a) = (\<Union>  b \<in> underS r a. (under r' (f b)))" .
    1.35 +    have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" .
    1.36      thus ?thesis
    1.37      using Well' bFact
    1.38            wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce