# HG changeset patch
# User paulson
# Date 904655023 -7200
# Node ID 13a199e94877d2083c1c3b98078e05f7a31f5093
# Parent  8a458866637c8f898591b89903802816a11f215e
tidying; moved diff_less to Arith.ML

diff -r 8a458866637c -r 13a199e94877 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Tue Sep 01 15:03:10 1998 +0200
+++ b/src/HOL/Divides.ML	Tue Sep 01 15:03:43 1998 +0200
@@ -9,21 +9,13 @@
 
 (** Less-then properties **)
 
-(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-Goal "[| 0<n; ~ m<n |] ==> m - n < m";
-by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
-by (Blast_tac 1);
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS(asm_simp_tac(simpset() addsimps [diff_less_Suc])));
-qed "diff_less";
-
 val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
                     def_wfrec RS trans;
 
 (*** Remainder ***)
 
 Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
-             \                      (%f j. if j<n then j else f (j-n))";
+\                           (%f j. if j<n then j else f (j-n))";
 by (simp_tac (simpset() addsimps [mod_def]) 1);
 qed "mod_eq";
 
@@ -37,6 +29,11 @@
 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "mod_geq";
 
+(*Avoids the ugly ~m<n above*)
+Goal "[| 0<n;  n<=m |] ==> m mod n = (m-n) mod n";
+by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
+qed "le_mod_geq";
+
 (*NOT suitable for rewriting: loops*)
 Goal "0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
@@ -114,6 +111,11 @@
 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "div_geq";
 
+(*Avoids the ugly ~m<n above*)
+Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
+by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
+qed "le_div_geq";
+
 (*NOT suitable for rewriting: loops*)
 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
@@ -245,12 +247,12 @@
 by (forward_tac [lessI RS less_trans] 2);
 by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
 (* case n <= Suc(na) *)
-by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, mod_geq]) 1);
-by (etac (le_imp_less_or_eq RS disjE) 1);
-by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1);
-by (asm_full_simp_tac (simpset() addsimps [not_less_eq RS sym, 
-                                          diff_less, mod_geq]) 1);
-by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
+by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
+					   mod_geq]) 1);
+by (etac disjE 1);
+ by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_diff_less, 
+				      le_mod_geq]) 1);
 qed "mod_Suc";
 
 Goal "0<n ==> m mod n < n";
@@ -325,7 +327,7 @@
 by (subgoal_tac "~ k*na < k*n" 1);
 by (asm_simp_tac
      (simpset() addsimps [zero_less_mult_iff, div_geq,
-                         diff_mult_distrib2 RS sym, diff_less]) 1);
+			  diff_mult_distrib2 RS sym, diff_less]) 1);
 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
                                           le_refl RS mult_le_mono]) 1);
 qed "div_cancel";