Simplified the new proofs about division
authorpaulson
Fri Jul 04 12:31:20 1997 +0200 (1997-07-04)
changeset 349632e7edc609fd
parent 3495 04739732b13e
child 3497 122e80826c95
Simplified the new proofs about division
src/HOL/Divides.ML
     1.1 --- a/src/HOL/Divides.ML	Fri Jul 04 11:57:33 1997 +0200
     1.2 +++ b/src/HOL/Divides.ML	Fri Jul 04 12:31:20 1997 +0200
     1.3 @@ -126,39 +126,31 @@
     1.4  (* 1  case n<k *)
     1.5  by (subgoal_tac "m<k" 1);
     1.6  by (asm_simp_tac (!simpset addsimps [div_less]) 1);
     1.7 -by (etac le_less_trans 1);
     1.8 -by (atac 1);
     1.9 +by (trans_tac 1);
    1.10  (* 2  case n >= k *)
    1.11  by (case_tac "m<k" 1);
    1.12  (* 2.1  case m<k *)
    1.13  by (asm_simp_tac (!simpset addsimps [div_less]) 1);
    1.14  (* 2.2  case m>=k *)
    1.15 -by (asm_simp_tac (!simpset addsimps [div_geq]) 1);
    1.16 -by (REPEAT (eresolve_tac [allE,impE] 1));
    1.17 -by (REPEAT (eresolve_tac [allE,impE] 2));
    1.18 -by (atac 3);
    1.19 -by (asm_simp_tac (!simpset addsimps [diff_less]) 1);
    1.20 -by (etac diff_le_mono 1);
    1.21 +by (asm_simp_tac (!simpset addsimps [div_geq, diff_less, diff_le_mono]) 1);
    1.22  qed_spec_mp "div_le_mono";
    1.23  
    1.24  
    1.25  (* Antimonotonicity of div in second argument *)
    1.26  goal thy "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
    1.27  by (subgoal_tac "0<n" 1);
    1.28 - by(trans_tac 2);
    1.29 + by (trans_tac 2);
    1.30  by (res_inst_tac [("n","k")] less_induct 1);
    1.31 -by(Simp_tac 1);
    1.32 -by(rename_tac "k" 1);
    1.33 +by (Simp_tac 1);
    1.34 +by (rename_tac "k" 1);
    1.35  by (case_tac "k<n" 1);
    1.36   by (asm_simp_tac (!simpset addsimps [div_less]) 1);
    1.37  by (subgoal_tac "~(k<m)" 1);
    1.38 - by(trans_tac 2);
    1.39 + by (trans_tac 2);
    1.40  by (asm_simp_tac (!simpset addsimps [div_geq]) 1);
    1.41  by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
    1.42 - by (etac le_trans 1);
    1.43 - by (REPEAT (eresolve_tac [allE,impE] 1));
    1.44 -  by (atac 2);
    1.45 - by (asm_simp_tac (!simpset addsimps [diff_less]) 1);
    1.46 + by (best_tac (!claset addIs [le_trans] 
    1.47 +                       addss (!simpset addsimps [diff_less])) 1);
    1.48  by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
    1.49  qed "div_le_mono2";
    1.50  
    1.51 @@ -173,12 +165,12 @@
    1.52  (* Similar for "less than" *)
    1.53  goal thy "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
    1.54  by (res_inst_tac [("n","m")] less_induct 1);
    1.55 -by(Simp_tac 1);
    1.56 -by(rename_tac "m" 1);
    1.57 +by (Simp_tac 1);
    1.58 +by (rename_tac "m" 1);
    1.59  by (case_tac "m<n" 1);
    1.60   by (asm_full_simp_tac (!simpset addsimps [div_less]) 1);
    1.61  by (subgoal_tac "0<n" 1);
    1.62 - by(trans_tac 2);
    1.63 + by (trans_tac 2);
    1.64  by (asm_full_simp_tac (!simpset addsimps [div_geq]) 1);
    1.65  by (case_tac "n<m" 1);
    1.66   by (subgoal_tac "(m-n) div n < (m-n)" 1);
    1.67 @@ -188,7 +180,7 @@
    1.68   by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1);
    1.69  (* case n=m *)
    1.70  by (subgoal_tac "m=n" 1);
    1.71 - by(trans_tac 2);
    1.72 + by (trans_tac 2);
    1.73  by (asm_simp_tac (!simpset addsimps [div_less]) 1);
    1.74  qed_spec_mp "div_less_dividend";
    1.75  Addsimps [div_less_dividend];