Replace surj by abbreviation; remove surj_on.
authorhoelzl
Mon Nov 22 10:34:33 2010 +0100 (2010-11-22)
changeset 40702cf26dd7395e4
parent 40683 a3f37b3d303a
child 40703 d1fc454d6735
Replace surj by abbreviation; remove surj_on.
NEWS
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Countable.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Nominal/Examples/Support.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Product_Type.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Rename.thy
     1.1 --- a/NEWS	Wed Nov 24 10:52:02 2010 +0100
     1.2 +++ b/NEWS	Mon Nov 22 10:34:33 2010 +0100
     1.3 @@ -291,9 +291,10 @@
     1.4  derive instantiated and simplified equations for inductive predicates,
     1.5  similar to inductive_cases.
     1.6  
     1.7 -* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
     1.8 -generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
     1.9 -The theorems bij_def and surj_def are unchanged.
    1.10 +* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an
    1.11 +abbreviation of "range f = UIV". The theorems bij_def and surj_def are
    1.12 +unchanged.
    1.13 +INCOMPATIBILITY.
    1.14  
    1.15  * Function package: .psimps rules are no longer implicitly declared [simp].
    1.16  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Finite_Set.thy	Wed Nov 24 10:52:02 2010 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Mon Nov 22 10:34:33 2010 +0100
     2.3 @@ -2286,7 +2286,7 @@
     2.4  
     2.5  lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
     2.6  shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
     2.7 -by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
     2.8 +by (blast intro: finite_surj_inj subset_UNIV)
     2.9  
    2.10  lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
    2.11  shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
     3.1 --- a/src/HOL/Fun.thy	Wed Nov 24 10:52:02 2010 +0100
     3.2 +++ b/src/HOL/Fun.thy	Mon Nov 22 10:34:33 2010 +0100
     3.3 @@ -130,24 +130,22 @@
     3.4    by (simp_all add: fun_eq_iff)
     3.5  
     3.6  
     3.7 -subsection {* Injectivity, Surjectivity and Bijectivity *}
     3.8 +subsection {* Injectivity and Bijectivity *}
     3.9  
    3.10  definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
    3.11    "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
    3.12  
    3.13 -definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
    3.14 -  "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
    3.15 -
    3.16  definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
    3.17    "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
    3.18  
    3.19 -text{*A common special case: functions injective over the entire domain type.*}
    3.20 +text{*A common special case: functions injective, surjective or bijective over
    3.21 +the entire domain type.*}
    3.22  
    3.23  abbreviation
    3.24    "inj f \<equiv> inj_on f UNIV"
    3.25  
    3.26 -abbreviation
    3.27 -  "surj f \<equiv> surj_on f UNIV"
    3.28 +abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
    3.29 +  "surj f \<equiv> (range f = UNIV)"
    3.30  
    3.31  abbreviation
    3.32    "bij f \<equiv> bij_betw f UNIV UNIV"
    3.33 @@ -187,8 +185,8 @@
    3.34  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
    3.35  by (simp add: inj_on_def)
    3.36  
    3.37 -lemma surj_id[simp]: "surj_on id A"
    3.38 -by (simp add: surj_on_def)
    3.39 +lemma surj_id: "surj id"
    3.40 +by simp
    3.41  
    3.42  lemma bij_id[simp]: "bij id"
    3.43  by (simp add: bij_betw_def)
    3.44 @@ -251,20 +249,11 @@
    3.45  apply (blast)
    3.46  done
    3.47  
    3.48 -lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
    3.49 -  by (simp add: surj_on_def) (blast intro: sym)
    3.50 -
    3.51 -lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
    3.52 -  by (auto simp: surj_on_def)
    3.53 +lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    3.54 +  by auto
    3.55  
    3.56 -lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
    3.57 -  unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
    3.58 -
    3.59 -lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    3.60 -  by (simp add: surj_on_def subset_eq image_iff)
    3.61 -
    3.62 -lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
    3.63 -  by (blast intro: surj_onI)
    3.64 +lemma surjI: assumes *: "\<And> x. g (f x) = x" shows "surj g"
    3.65 +  using *[symmetric] by auto
    3.66  
    3.67  lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
    3.68    by (simp add: surj_def)
    3.69 @@ -278,17 +267,11 @@
    3.70  apply (drule_tac x = x in spec, blast)
    3.71  done
    3.72  
    3.73 -lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
    3.74 -  by (auto simp add: surj_on_def)
    3.75 -
    3.76 -lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
    3.77 -  unfolding surj_on_def by auto
    3.78 -
    3.79  lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
    3.80 -  unfolding bij_betw_def surj_range_iff by auto
    3.81 +  unfolding bij_betw_def by auto
    3.82  
    3.83  lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
    3.84 -  unfolding surj_range_iff bij_betw_def ..
    3.85 +  unfolding bij_betw_def ..
    3.86  
    3.87  lemma bijI: "[| inj f; surj f |] ==> bij f"
    3.88  by (simp add: bij_def)
    3.89 @@ -302,16 +285,13 @@
    3.90  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
    3.91  by (simp add: bij_betw_def)
    3.92  
    3.93 -lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
    3.94 -by (auto simp: bij_betw_def surj_on_range_iff)
    3.95 -
    3.96 -lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
    3.97 -by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
    3.98 -
    3.99  lemma bij_betw_trans:
   3.100    "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
   3.101  by(auto simp add:bij_betw_def comp_inj_on)
   3.102  
   3.103 +lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
   3.104 +  by (rule bij_betw_trans)
   3.105 +
   3.106  lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
   3.107  proof -
   3.108    have i: "inj_on f A" and s: "f ` A = B"
   3.109 @@ -349,15 +329,13 @@
   3.110    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
   3.111  
   3.112  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   3.113 -by (simp add: surj_range)
   3.114 +by simp
   3.115  
   3.116  lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   3.117  by (simp add: inj_on_def, blast)
   3.118  
   3.119  lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
   3.120 -apply (unfold surj_def)
   3.121 -apply (blast intro: sym)
   3.122 -done
   3.123 +by (blast intro: sym)
   3.124  
   3.125  lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
   3.126  by (unfold inj_on_def, blast)
   3.127 @@ -410,7 +388,7 @@
   3.128  done
   3.129  
   3.130  lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
   3.131 -by (auto simp add: surj_def)
   3.132 +by auto
   3.133  
   3.134  lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
   3.135  by (auto simp add: inj_on_def)
   3.136 @@ -559,10 +537,10 @@
   3.137  qed
   3.138  
   3.139  lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
   3.140 -  unfolding surj_range_iff by simp
   3.141 +  by simp
   3.142  
   3.143  lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
   3.144 -  unfolding surj_range_iff by simp
   3.145 +  by simp
   3.146  
   3.147  lemma bij_betw_swap_iff [simp]:
   3.148    "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Nov 24 10:52:02 2010 +0100
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Nov 22 10:34:33 2010 +0100
     4.3 @@ -151,10 +151,10 @@
     4.4  by(fastsimp simp: image_def)
     4.5  
     4.6  lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
     4.7 -by (blast intro: surjI inv_into_f_f)
     4.8 +by (blast intro!: surjI inv_into_f_f)
     4.9  
    4.10  lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
    4.11 -by (simp add: f_inv_into_f surj_range)
    4.12 +by (simp add: f_inv_into_f)
    4.13  
    4.14  lemma inv_into_injective:
    4.15    assumes eq: "inv_into A f x = inv_into A f y"
    4.16 @@ -173,12 +173,13 @@
    4.17  by (auto simp add: bij_betw_def inj_on_inv_into)
    4.18  
    4.19  lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
    4.20 -by (simp add: inj_on_inv_into surj_range)
    4.21 +by (simp add: inj_on_inv_into)
    4.22  
    4.23  lemma surj_iff: "(surj f) = (f o inv f = id)"
    4.24 -apply (simp add: o_def fun_eq_iff)
    4.25 -apply (blast intro: surjI surj_f_inv_f)
    4.26 -done
    4.27 +by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
    4.28 +
    4.29 +lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
    4.30 +  unfolding surj_iff by (simp add: o_def fun_eq_iff)
    4.31  
    4.32  lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
    4.33  apply (rule ext)
     5.1 --- a/src/HOL/Lattice/Orders.thy	Wed Nov 24 10:52:02 2010 +0100
     5.2 +++ b/src/HOL/Lattice/Orders.thy	Mon Nov 22 10:34:33 2010 +0100
     5.3 @@ -118,8 +118,8 @@
     5.4    qed
     5.5  qed
     5.6  
     5.7 -lemma range_dual [simp]: "dual ` UNIV = UNIV"
     5.8 -proof (rule surj_range)
     5.9 +lemma range_dual [simp]: "surj dual"
    5.10 +proof -
    5.11    have "\<And>x'. dual (undual x') = x'" by simp
    5.12    thus "surj dual" by (rule surjI)
    5.13  qed
     6.1 --- a/src/HOL/Library/ContNotDenum.thy	Wed Nov 24 10:52:02 2010 +0100
     6.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Nov 22 10:34:33 2010 +0100
     6.3 @@ -565,8 +565,7 @@
     6.4    shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
     6.5  proof -- "by contradiction"
     6.6    assume "\<exists>f::nat\<Rightarrow>real. surj f"
     6.7 -  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
     6.8 -  hence rangeF: "range f = UNIV" by (rule surj_range)
     6.9 +  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
    6.10    -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
    6.11    have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
    6.12    moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
     7.1 --- a/src/HOL/Library/Countable.thy	Wed Nov 24 10:52:02 2010 +0100
     7.2 +++ b/src/HOL/Library/Countable.thy	Mon Nov 22 10:34:33 2010 +0100
     7.3 @@ -165,7 +165,7 @@
     7.4  qed
     7.5  
     7.6  lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
     7.7 -by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
     7.8 +by (simp add: Rats_def surj_nat_to_rat_surj)
     7.9  
    7.10  context field_char_0
    7.11  begin
     8.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Nov 24 10:52:02 2010 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Nov 22 10:34:33 2010 +0100
     8.3 @@ -948,14 +948,12 @@
     8.4     assumes lf: "linear f" and gf: "f o g = id"
     8.5     shows "linear g"
     8.6   proof-
     8.7 -   from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def fun_eq_iff)
     8.8 -     by metis 
     8.9 +   from gf have fi: "surj f" by (auto simp add: surj_def o_def id_def) metis
    8.10     from linear_surjective_isomorphism[OF lf fi]
    8.11     obtain h:: "'a => 'a" where
    8.12       h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
    8.13     have "h = g" apply (rule ext) using gf h(2,3)
    8.14 -     apply (simp add: o_def id_def fun_eq_iff)
    8.15 -     by metis
    8.16 +     by (simp add: o_def id_def fun_eq_iff) metis
    8.17     with h(1) show ?thesis by blast
    8.18   qed
    8.19   
     9.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Nov 24 10:52:02 2010 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Nov 22 10:34:33 2010 +0100
     9.3 @@ -2843,7 +2843,7 @@
     9.4      h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
     9.5    from h(2)
     9.6    have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
     9.7 -    using sf by(auto simp add: surj_iff o_def fun_eq_iff)
     9.8 +    using sf by(auto simp add: surj_iff_all)
     9.9    from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
    9.10    have "f o h = id" .
    9.11    then show ?thesis using h(1) by blast
    9.12 @@ -2995,7 +2995,7 @@
    9.13    {fix f f':: "'a => 'a"
    9.14      assume lf: "linear f" "linear f'" and f: "f o f' = id"
    9.15      from f have sf: "surj f"
    9.16 -      apply (auto simp add: o_def fun_eq_iff id_def surj_def)
    9.17 +      apply (auto simp add: o_def id_def surj_def)
    9.18        by metis
    9.19      from linear_surjective_isomorphism[OF lf(1) sf] lf f
    9.20      have "f' o f = id" unfolding fun_eq_iff o_def id_def
    10.1 --- a/src/HOL/Nominal/Examples/Support.thy	Wed Nov 24 10:52:02 2010 +0100
    10.2 +++ b/src/HOL/Nominal/Examples/Support.thy	Mon Nov 22 10:34:33 2010 +0100
    10.3 @@ -47,7 +47,7 @@
    10.4    also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto
    10.5    also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
    10.6    also have "\<dots> = (UNIV::atom set)" using atom.exhaust
    10.7 -    by (rule_tac  surj_range) (auto simp add: surj_def)
    10.8 +    by (auto simp add: surj_def)
    10.9    finally show "EVEN \<union> ODD = UNIV" by simp
   10.10  qed
   10.11  
    11.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 24 10:52:02 2010 +0100
    11.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 22 10:34:33 2010 +0100
    11.3 @@ -132,7 +132,7 @@
    11.4        by (auto intro!: exI[of _ "from_nat i"])
    11.5    qed
    11.6    have **: "range ?A' = range A"
    11.7 -    using surj_range[OF surj_from_nat]
    11.8 +    using surj_from_nat
    11.9      by (auto simp: image_compose intro!: imageI)
   11.10    show ?thesis unfolding * ** ..
   11.11  qed
    12.1 --- a/src/HOL/Product_Type.thy	Wed Nov 24 10:52:02 2010 +0100
    12.2 +++ b/src/HOL/Product_Type.thy	Mon Nov 22 10:34:33 2010 +0100
    12.3 @@ -1135,6 +1135,7 @@
    12.4  qed
    12.5  
    12.6  lemma map_pair_surj:
    12.7 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
    12.8    assumes "surj f" and "surj g"
    12.9    shows "surj (map_pair f g)"
   12.10  unfolding surj_def
    13.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Wed Nov 24 10:52:02 2010 +0100
    13.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Nov 22 10:34:33 2010 +0100
    13.3 @@ -358,7 +358,7 @@
    13.4    done
    13.5  
    13.6  lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
    13.7 -  apply (simp add: surj_iff fun_eq_iff o_apply)
    13.8 +  apply (simp add: surj_iff_all)
    13.9    apply record_auto
   13.10    done
   13.11  
   13.12 @@ -386,7 +386,7 @@
   13.13    done
   13.14  
   13.15  lemma surj_sysOfClient [iff]: "surj sysOfClient"
   13.16 -  apply (simp add: surj_iff fun_eq_iff o_apply)
   13.17 +  apply (simp add: surj_iff_all)
   13.18    apply record_auto
   13.19    done
   13.20  
   13.21 @@ -410,7 +410,7 @@
   13.22    done
   13.23  
   13.24  lemma surj_client_map [iff]: "surj client_map"
   13.25 -  apply (simp add: surj_iff fun_eq_iff o_apply)
   13.26 +  apply (simp add: surj_iff_all)
   13.27    apply record_auto
   13.28    done
   13.29  
   13.30 @@ -682,7 +682,7 @@
   13.31  lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
   13.32  apply (insert fst_o_lift_map [of i])
   13.33  apply (drule fun_cong [where x=x])
   13.34 -apply (simp add: o_def);
   13.35 +apply (simp add: o_def)
   13.36  done
   13.37  
   13.38  lemma fst_o_lift_map' [simp]:
   13.39 @@ -702,7 +702,7 @@
   13.40    RS guarantees_PLam_I
   13.41    RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
   13.42    |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
   13.43 -                                   surj_rename RS surj_range])
   13.44 +                                   surj_rename])
   13.45  
   13.46  However, the "preserves" property remains to be discharged, and the unfolding
   13.47  of "o" and "sub" complicates subsequent reasoning.
   13.48 @@ -723,7 +723,7 @@
   13.49      asm_simp_tac
   13.50          (ss addsimps [@{thm lift_guarantees_eq_lift_inv},
   13.51                        @{thm rename_guarantees_eq_rename_inv},
   13.52 -                      @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
   13.53 +                      @{thm bij_imp_bij_inv}, @{thm surj_rename},
   13.54                        @{thm inv_inv_eq}]) 1,
   13.55      asm_simp_tac
   13.56          (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
   13.57 @@ -798,9 +798,9 @@
   13.58  lemmas rename_Alloc_Increasing =
   13.59    Alloc_Increasing
   13.60      [THEN rename_guarantees_sysOfAlloc_I,
   13.61 -     simplified surj_rename [THEN surj_range] o_def sub_apply
   13.62 +     simplified surj_rename o_def sub_apply
   13.63                  rename_image_Increasing bij_sysOfAlloc
   13.64 -                allocGiv_o_inv_sysOfAlloc_eq'];
   13.65 +                allocGiv_o_inv_sysOfAlloc_eq']
   13.66  
   13.67  lemma System_Increasing_allocGiv:
   13.68       "i < Nclients ==> System : Increasing (sub i o allocGiv)"
   13.69 @@ -879,7 +879,7 @@
   13.70              \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
   13.71    apply (simp add: o_apply)
   13.72    apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
   13.73 -  apply (simp add: o_def);
   13.74 +  apply (simp add: o_def)
   13.75    apply (erule component_guaranteesD)
   13.76    apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
   13.77    done
    14.1 --- a/src/HOL/UNITY/Extend.thy	Wed Nov 24 10:52:02 2010 +0100
    14.2 +++ b/src/HOL/UNITY/Extend.thy	Mon Nov 22 10:34:33 2010 +0100
    14.3 @@ -127,7 +127,7 @@
    14.4       assumes surj_h: "surj h"
    14.5           and prem:   "!! x y. g (h(x,y)) = x"
    14.6       shows "fst (inv h z) = g z"
    14.7 -by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
    14.8 +by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
    14.9  
   14.10  
   14.11  subsection{*Trivial properties of f, g, h*}
    15.1 --- a/src/HOL/UNITY/Rename.thy	Wed Nov 24 10:52:02 2010 +0100
    15.2 +++ b/src/HOL/UNITY/Rename.thy	Mon Nov 22 10:34:33 2010 +0100
    15.3 @@ -60,7 +60,8 @@
    15.4  lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
    15.5  apply (rule bijI)
    15.6  apply (rule Extend.inj_extend_act)
    15.7 -apply (auto simp add: bij_extend_act_eq_project_act)
    15.8 +apply simp
    15.9 +apply (simp add: bij_extend_act_eq_project_act)
   15.10  apply (rule surjI)
   15.11  apply (rule Extend.extend_act_inverse)
   15.12  apply (blast intro: bij_imp_bij_inv good_map_bij)
   15.13 @@ -75,7 +76,7 @@
   15.14                  project_act (%(x,u::'c). h x)"
   15.15  apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
   15.16  apply (rule surj_imp_inv_eq)
   15.17 -apply (blast intro: bij_extend_act bij_is_surj)
   15.18 +apply (blast intro!: bij_extend_act bij_is_surj)
   15.19  apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
   15.20  done
   15.21