tuned proofs
authornipkow
Fri Aug 28 19:15:59 2009 +0200 (2009-08-28)
changeset 3243766f1a0dfe7d9
parent 32436 10cd49e0c067
child 32438 620a5d8cfa78
tuned proofs
src/HOL/Finite_Set.thy
src/HOL/Int.thy
src/HOL/Nat.thy
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Aug 28 18:52:41 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Aug 28 19:15:59 2009 +0200
     1.3 @@ -2966,11 +2966,11 @@
     1.4  
     1.5  lemma dual_max:
     1.6    "ord.max (op \<ge>) = min"
     1.7 -  by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
     1.8 +  by (auto simp add: ord.max_def_raw expand_fun_eq)
     1.9  
    1.10  lemma dual_min:
    1.11    "ord.min (op \<ge>) = max"
    1.12 -  by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
    1.13 +  by (auto simp add: ord.min_def_raw expand_fun_eq)
    1.14  
    1.15  lemma strict_below_fold1_iff:
    1.16    assumes "finite A" and "A \<noteq> {}"
     2.1 --- a/src/HOL/Int.thy	Fri Aug 28 18:52:41 2009 +0200
     2.2 +++ b/src/HOL/Int.thy	Fri Aug 28 19:15:59 2009 +0200
     2.3 @@ -266,7 +266,7 @@
     2.4  proof  
     2.5    fix k :: int
     2.6    show "abs k = sup k (- k)"
     2.7 -    by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
     2.8 +    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
     2.9  qed
    2.10  
    2.11  lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
    2.12 @@ -1487,21 +1487,6 @@
    2.13         add_special diff_special eq_special less_special le_special
    2.14  
    2.15  
    2.16 -lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
    2.17 -                   max (0::int) 1 = 1 & max (1::int) 0 = 1"
    2.18 -by(simp add:min_def max_def)
    2.19 -
    2.20 -lemmas min_max_special[simp] =
    2.21 - min_max_01
    2.22 - max_def[of "0::int" "number_of v", standard, simp]
    2.23 - min_def[of "0::int" "number_of v", standard, simp]
    2.24 - max_def[of "number_of u" "0::int", standard, simp]
    2.25 - min_def[of "number_of u" "0::int", standard, simp]
    2.26 - max_def[of "1::int" "number_of v", standard, simp]
    2.27 - min_def[of "1::int" "number_of v", standard, simp]
    2.28 - max_def[of "number_of u" "1::int", standard, simp]
    2.29 - min_def[of "number_of u" "1::int", standard, simp]
    2.30 -
    2.31  text {* Legacy theorems *}
    2.32  
    2.33  lemmas zle_int = of_nat_le_iff [where 'a=int]
     3.1 --- a/src/HOL/Nat.thy	Fri Aug 28 18:52:41 2009 +0200
     3.2 +++ b/src/HOL/Nat.thy	Fri Aug 28 19:15:59 2009 +0200
     3.3 @@ -1512,7 +1512,7 @@
     3.4  by (simp split add: nat_diff_split)
     3.5  
     3.6  lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
     3.7 -unfolding min_def by auto
     3.8 +by auto
     3.9  
    3.10  lemma inj_on_diff_nat: 
    3.11    assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
     4.1 --- a/src/HOL/OrderedGroup.thy	Fri Aug 28 18:52:41 2009 +0200
     4.2 +++ b/src/HOL/OrderedGroup.thy	Fri Aug 28 19:15:59 2009 +0200
     4.3 @@ -1275,7 +1275,7 @@
     4.4  proof -
     4.5    note add_le_cancel_right [of a a "- a", symmetric, simplified]
     4.6    moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
     4.7 -  then show ?thesis by (auto simp: sup_max max_def)
     4.8 +  then show ?thesis by (auto simp: sup_max)
     4.9  qed
    4.10  
    4.11  lemma abs_if_lattice: