# HG changeset patch
# User nipkow
# Date 1169804775 -3600
# Node ID 834c4604de7b23b1c09d05a56d978cb803b984d2
# Parent  9c07aab3a6539368de59962691877396e2bdcce1
more fixes of arithmetic for min/max.

diff -r 9c07aab3a653 -r 834c4604de7b src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Fri Jan 26 10:24:33 2007 +0100
+++ b/src/HOL/Integ/IntArith.thy	Fri Jan 26 10:46:15 2007 +0100
@@ -91,10 +91,26 @@
     binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
     binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
 
-lemmas arith_special = 
+lemmas arith_special[simp] = 
        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]
+
+
 use "int_arith1.ML"
 setup int_arith_setup
 
diff -r 9c07aab3a653 -r 834c4604de7b src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Fri Jan 26 10:24:33 2007 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Fri Jan 26 10:46:15 2007 +0100
@@ -132,7 +132,6 @@
   end;
 
 
-Addsimps arith_special;
 Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];