Simplified arithmetic.

--- a/src/HOL/Arith.ML	Tue Jan 12 17:19:53 1999 +0100
+++ b/src/HOL/Arith.ML	Wed Jan 13 08:41:28 1999 +0100
@@ -852,6 +852,7 @@
 val neqE = linorder_neqE;
 val notI = notI;
 val sym = sym;
+val not_lessD = linorder_not_less RS iffD1;
 
 val mk_Eq = mk_eq;
 val mk_Trueprop = HOLogic.mk_Trueprop;
@@ -870,7 +871,6 @@
 
 val lessD = Suc_leI;
 val not_leD = not_leE RS Suc_leI;
-val not_lessD = leI;
 
 (* Turn term into list of summand * multiplicity plus a constant *)
 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))

--- a/src/HOL/Integ/Bin.ML	Tue Jan 12 17:19:53 1999 +0100
+++ b/src/HOL/Integ/Bin.ML	Wed Jan 13 08:41:28 1999 +0100
@@ -404,7 +404,6 @@
 
 val lessD = add1_zle_eq RS iffD2;
 val not_leD = not_zleE RS lessD;
-val not_lessD = zleI;
 
 val intT = Type("IntDef.int",[]);
 

--- a/src/HOL/Nat.ML	Tue Jan 12 17:19:53 1999 +0100
+++ b/src/HOL/Nat.ML	Wed Jan 13 08:41:28 1999 +0100
@@ -52,13 +52,13 @@
  by (etac swap 1);
  by (ALLGOALS Asm_full_simp_tac);
 qed "not_gr0";
-Addsimps [not_gr0];
+AddIffs [not_gr0];
 
-Goal "m<n ==> 0 < n";
+(*Goal "m<n ==> 0 < n";
 by (dtac gr_implies_not0 1);
 by (Asm_full_simp_tac 1);
 qed "gr_implies_gr0";
-Addsimps [gr_implies_gr0];
+Addsimps [gr_implies_gr0];*)
 
 qed_goalw "Least_Suc" thy [Least_nat_def]
  "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"

--- a/src/HOL/NatDef.ML	Tue Jan 12 17:19:53 1999 +0100
+++ b/src/HOL/NatDef.ML	Wed Jan 13 08:41:28 1999 +0100
@@ -280,10 +280,10 @@
 qed "Suc_less_eq";
 Addsimps [Suc_less_eq];
 
-Goal "~(Suc(n) < n)";
+(*Goal "~(Suc(n) < n)";
 by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1);
 qed "not_Suc_n_less_n";
-(*Addsimps [not_Suc_n_less_n];*)
+Addsimps [not_Suc_n_less_n];*)
 
 Goal "i<j ==> j<k --> Suc i < k";
 by (nat_ind_tac "k" 1);
@@ -385,7 +385,7 @@
 qed "le_SucI";
 Addsimps[le_SucI];
 
-bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
+(*bind_thm ("le_Suc", not_Suc_n_less_n RS leI);*)
 
 Goalw [le_def] "m < n ==> m <= (n::nat)";
 by (blast_tac (claset() addEs [less_asym]) 1);
@@ -473,32 +473,6 @@
   Not suitable as default simprules because they often lead to looping*)
 val not_less_simps = [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq];
 
-(** max
-
-Goalw [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
-by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
-by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
-qed "le_max_iff_disj";
-
-Goalw [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)";
-by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
-by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
-qed "max_le_iff_conj";
-
-
-(** min **)
-
-Goalw [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)";
-by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
-by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
-qed "le_min_iff_conj";
-
-Goalw [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits) 1);
-by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
-qed "min_le_iff_disj";
- **)
-
 (** LEAST -- the least number operator **)
 
 Goal "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";

--- a/src/HOL/Ord.ML	Tue Jan 12 17:19:53 1999 +0100
+++ b/src/HOL/Ord.ML	Wed Jan 13 08:41:28 1999 +0100
@@ -144,3 +144,9 @@
 
 (*** eliminates ~= in premises ***)
 bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
+
+Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
+by (simp_tac (simpset() addsimps [order_less_le]) 1);
+by (cut_facts_tac [linorder_linear] 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
+qed "linorder_not_less";