--- a/src/HOL/NatDef.ML Thu Feb 05 10:38:34 1998 +0100
+++ b/src/HOL/NatDef.ML Thu Feb 05 10:46:31 1998 +0100
@@ -489,6 +489,10 @@
by (Blast_tac 1);
qed "not_leE";
+goalw thy [le_def] "(~n<=m) = (m<(n::nat))";
+by (Simp_tac 1);
+qed "not_le_iff_less";
+
goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1);
@@ -577,6 +581,32 @@
by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
qed "nat_less_le";
+(** max **)
+
+goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
+by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
+qed "le_max_iff_disj";
+
+goalw thy [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)";
+by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
+qed "max_le_iff_conj";
+
+
+(** min **)
+
+goalw thy [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)";
+by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
+qed "le_min_iff_conj";
+
+goalw thy [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)";
+by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
+qed "min_le_iff_disj";
+
+
(** LEAST -- the least number operator **)
goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";