# HG changeset patch
# User paulson
# Date 891595241 -7200
# Node ID b4760a8334809430eb14e860ce14728e39cb6fb1
# Parent  b6729feb8a5d47b01a84e946f17bcd62c28c354c
Tidied proofs by getting rid of case_tac

diff -r b6729feb8a5d -r b4760a833480 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Apr 03 09:54:48 1998 +0200
+++ b/src/HOL/Divides.ML	Fri Apr 03 11:20:41 1998 +0200
@@ -37,6 +37,11 @@
 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "mod_geq";
 
+(*NOT suitable for rewriting: loops*)
+goal thy "!!m. 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);
+qed "mod_if";
+
 goal thy "m mod 1 = 0";
 by (induct_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq])));
@@ -55,22 +60,18 @@
 
 goal thy "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
 by (res_inst_tac [("n","m")] less_induct 1);
-by (case_tac "na<n" 1);
-(*case na<n*)
-by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
-(*case n<=na*)
-by (asm_simp_tac (simpset() addsimps [mod_geq, diff_less, zero_less_mult_iff, 
-				     diff_mult_distrib]) 1);
+by (stac mod_if 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 
+				      diff_less, diff_mult_distrib]) 1);
 qed "mod_mult_distrib";
 
 goal thy "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
 by (res_inst_tac [("n","m")] less_induct 1);
-by (case_tac "na<n" 1);
-(*case na<n*)
-by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
-(*case n<=na*)
-by (asm_simp_tac (simpset() addsimps [mod_geq, diff_less, zero_less_mult_iff, 
-				     diff_mult_distrib2]) 1);
+by (stac mod_if 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 
+				      diff_less, diff_mult_distrib2]) 1);
 qed "mod_mult_distrib2";
 
 goal thy "!!n. 0<n ==> m*n mod n = 0";
@@ -98,14 +99,19 @@
 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "div_geq";
 
+(*NOT suitable for rewriting: loops*)
+goal thy "!!m. 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);
+qed "div_if";
+
 (*Main Result about quotient and remainder.*)
 goal thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
 by (res_inst_tac [("n","m")] less_induct 1);
-by (rename_tac "k" 1);    (*Variable name used in line below*)
-by (case_tac "k<n" 1);
-by (ALLGOALS (asm_simp_tac(simpset() addsimps ([add_assoc] @
-                       [mod_less, mod_geq, div_less, div_geq,
-                        add_diff_inverse, diff_less]))));
+by (stac mod_if 1);
+by (ALLGOALS (asm_simp_tac 
+	      (simpset() addsimps ([add_assoc] @
+				   [div_less, div_geq,
+				    add_diff_inverse, diff_less]))));
 qed "mod_div_equality";
 
 (* a simple rearrangement of mod_div_equality: *)