# HG changeset patch # User nipkow # Date 1251479759 -7200 # Node ID 66f1a0dfe7d904e21bcf6bbcb3be8b675bfbb9cc # Parent 10cd49e0c067a137feeaf6cd658817678ef8fecc tuned proofs diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Aug 28 18:52:41 2009 +0200 +++ b/src/HOL/Finite_Set.thy Fri Aug 28 19:15:59 2009 +0200 @@ -2966,11 +2966,11 @@ lemma dual_max: "ord.max (op \) = min" - by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq) + by (auto simp add: ord.max_def_raw expand_fun_eq) lemma dual_min: "ord.min (op \) = max" - by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq) + by (auto simp add: ord.min_def_raw expand_fun_eq) lemma strict_below_fold1_iff: assumes "finite A" and "A \ {}" diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/Int.thy --- a/src/HOL/Int.thy Fri Aug 28 18:52:41 2009 +0200 +++ b/src/HOL/Int.thy Fri Aug 28 19:15:59 2009 +0200 @@ -266,7 +266,7 @@ proof fix k :: int show "abs k = sup k (- k)" - by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric]) + by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric]) qed lemma zless_imp_add1_zle: "w < z \ w + (1\int) \ z" @@ -1487,21 +1487,6 @@ add_special diff_special eq_special less_special le_special -lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 & - max (0::int) 1 = 1 & max (1::int) 0 = 1" -by(simp add:min_def max_def) - -lemmas min_max_special[simp] = - min_max_01 - max_def[of "0::int" "number_of v", standard, simp] - min_def[of "0::int" "number_of v", standard, simp] - max_def[of "number_of u" "0::int", standard, simp] - min_def[of "number_of u" "0::int", standard, simp] - max_def[of "1::int" "number_of v", standard, simp] - min_def[of "1::int" "number_of v", standard, simp] - max_def[of "number_of u" "1::int", standard, simp] - min_def[of "number_of u" "1::int", standard, simp] - text {* Legacy theorems *} lemmas zle_int = of_nat_le_iff [where 'a=int] diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Aug 28 18:52:41 2009 +0200 +++ b/src/HOL/Nat.thy Fri Aug 28 19:15:59 2009 +0200 @@ -1512,7 +1512,7 @@ by (simp split add: nat_diff_split) lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i" -unfolding min_def by auto +by auto lemma inj_on_diff_nat: assumes k_le_n: "\n \ N. k \ (n::nat)" diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Fri Aug 28 18:52:41 2009 +0200 +++ b/src/HOL/OrderedGroup.thy Fri Aug 28 19:15:59 2009 +0200 @@ -1275,7 +1275,7 @@ proof - note add_le_cancel_right [of a a "- a", symmetric, simplified] moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified] - then show ?thesis by (auto simp: sup_max max_def) + then show ?thesis by (auto simp: sup_max) qed lemma abs_if_lattice: