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";