killed a few warnings
authorkrauss
Wed Dec 30 10:24:53 2009 +0100 (2009-12-30)
changeset 34209c7f621786035
parent 34208 a7acd6c68d9b
child 34210 f040cd999794
killed a few warnings
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Lattices.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Fun.thy	Wed Dec 30 01:08:33 2009 +0100
     1.2 +++ b/src/HOL/Fun.thy	Wed Dec 30 10:24:53 2009 +0100
     1.3 @@ -171,7 +171,7 @@
     1.4  by (simp add: surj_def) 
     1.5  
     1.6  lemma bij_id[simp]: "bij id"
     1.7 -by (simp add: bij_def inj_on_id surj_id) 
     1.8 +by (simp add: bij_def)
     1.9  
    1.10  lemma inj_onI:
    1.11      "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
    1.12 @@ -432,14 +432,14 @@
    1.13  by (rule ext, auto)
    1.14  
    1.15  lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
    1.16 -by(fastsimp simp:inj_on_def image_def)
    1.17 +by (fastsimp simp:inj_on_def image_def)
    1.18  
    1.19  lemma fun_upd_image:
    1.20       "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
    1.21  by auto
    1.22  
    1.23  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
    1.24 -by(auto intro: ext)
    1.25 +by (auto intro: ext)
    1.26  
    1.27  
    1.28  subsection {* @{text override_on} *}
    1.29 @@ -496,7 +496,7 @@
    1.30    thus "inj_on f A" by simp 
    1.31  next
    1.32    assume "inj_on f A"
    1.33 -  with A show "inj_on (swap a b f) A" by(iprover intro: inj_on_imp_inj_on_swap)
    1.34 +  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
    1.35  qed
    1.36  
    1.37  lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
    1.38 @@ -529,7 +529,7 @@
    1.39  lemma the_inv_into_f_f:
    1.40    "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
    1.41  apply (simp add: the_inv_into_def inj_on_def)
    1.42 -apply (blast intro: the_equality)
    1.43 +apply blast
    1.44  done
    1.45  
    1.46  lemma f_the_inv_into_f:
     2.1 --- a/src/HOL/HOL.thy	Wed Dec 30 01:08:33 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Wed Dec 30 10:24:53 2009 +0100
     2.3 @@ -869,7 +869,6 @@
     2.4    and impCE [elim!]
     2.5    and disjE [elim!]
     2.6    and conjE [elim!]
     2.7 -  and conjE [elim!]
     2.8  
     2.9  declare ex_ex1I [intro!]
    2.10    and allI [intro!]
     3.1 --- a/src/HOL/Lattices.thy	Wed Dec 30 01:08:33 2009 +0100
     3.2 +++ b/src/HOL/Lattices.thy	Wed Dec 30 10:24:53 2009 +0100
     3.3 @@ -201,7 +201,7 @@
     3.4  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
     3.5  proof-
     3.6    have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
     3.7 -  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1)
     3.8 +  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
     3.9    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    3.10      by(simp add:inf_sup_absorb inf_commute)
    3.11    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    3.12 @@ -213,7 +213,7 @@
    3.13  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    3.14  proof-
    3.15    have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
    3.16 -  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1)
    3.17 +  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
    3.18    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    3.19      by(simp add:sup_inf_absorb sup_commute)
    3.20    also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
    3.21 @@ -404,7 +404,7 @@
    3.22      by (simp add: inf_sup_distrib1)
    3.23    then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
    3.24      using sup_compl_top assms(2) by simp
    3.25 -  then show "- x = y" by (simp add: inf_top_right)
    3.26 +  then show "- x = y" by simp
    3.27  qed
    3.28  
    3.29  lemma double_compl [simp]:
     4.1 --- a/src/HOL/Set.thy	Wed Dec 30 01:08:33 2009 +0100
     4.2 +++ b/src/HOL/Set.thy	Wed Dec 30 10:24:53 2009 +0100
     4.3 @@ -517,10 +517,10 @@
     4.4  *}
     4.5  
     4.6  lemma equalityD1: "A = B ==> A \<subseteq> B"
     4.7 -  by (simp add: subset_refl)
     4.8 +  by simp
     4.9  
    4.10  lemma equalityD2: "A = B ==> B \<subseteq> A"
    4.11 -  by (simp add: subset_refl)
    4.12 +  by simp
    4.13  
    4.14  text {*
    4.15    \medskip Be careful when adding this to the claset as @{text
    4.16 @@ -529,7 +529,7 @@
    4.17  *}
    4.18  
    4.19  lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
    4.20 -  by (simp add: subset_refl)
    4.21 +  by simp
    4.22  
    4.23  lemma equalityCE [elim]:
    4.24      "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
    4.25 @@ -629,7 +629,7 @@
    4.26    by simp
    4.27  
    4.28  lemma Pow_top: "A \<in> Pow A"
    4.29 -  by (simp add: subset_refl)
    4.30 +  by simp
    4.31  
    4.32  
    4.33  subsubsection {* Set complement *}