src/HOL/Divides.thy
changeset 15439 71c0f98e31f1
parent 15251 bb6f072c8d10
child 16733 236dfafbeb63
     1.1 --- a/src/HOL/Divides.thy	Thu Jan 13 14:56:37 2005 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Jan 14 12:00:27 2005 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
     1.5  apply (case_tac "n=0", simp) 
     1.6  apply (rule mod_eq [THEN wf_less_trans])
     1.7 -apply (simp add: diff_less cut_apply less_eq)
     1.8 +apply (simp add: cut_apply less_eq)
     1.9  done
    1.10  
    1.11  (*Avoids the ugly ~m<n above*)
    1.12 @@ -119,7 +119,7 @@
    1.13  apply (case_tac "k=0", simp)
    1.14  apply (induct "m" rule: nat_less_induct)
    1.15  apply (subst mod_if, simp)
    1.16 -apply (simp add: mod_geq diff_less diff_mult_distrib)
    1.17 +apply (simp add: mod_geq diff_mult_distrib)
    1.18  done
    1.19  
    1.20  lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
    1.21 @@ -144,7 +144,7 @@
    1.22  
    1.23  lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
    1.24  apply (rule div_eq [THEN wf_less_trans])
    1.25 -apply (simp add: diff_less cut_apply less_eq)
    1.26 +apply (simp add: cut_apply less_eq)
    1.27  done
    1.28  
    1.29  (*Avoids the ugly ~m<n above*)
    1.30 @@ -160,7 +160,7 @@
    1.31  apply (case_tac "n=0", simp)
    1.32  apply (induct "m" rule: nat_less_induct)
    1.33  apply (subst mod_if)
    1.34 -apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
    1.35 +apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse)
    1.36  done
    1.37  
    1.38  lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
    1.39 @@ -222,7 +222,12 @@
    1.40  apply (induct "m" rule: nat_less_induct)
    1.41  apply (case_tac "na<n", simp) 
    1.42  txt{*case @{term "n \<le> na"}*}
    1.43 -apply (simp add: mod_geq diff_less)
    1.44 +apply (simp add: mod_geq)
    1.45 +done
    1.46 +
    1.47 +lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
    1.48 +apply(drule mod_less_divisor[where m = m])
    1.49 +apply simp
    1.50  done
    1.51  
    1.52  lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
    1.53 @@ -427,7 +432,7 @@
    1.54  (* 2.1  case m<k *)
    1.55  apply simp
    1.56  (* 2.2  case m>=k *)
    1.57 -apply (simp add: div_geq diff_less diff_le_mono)
    1.58 +apply (simp add: div_geq diff_le_mono)
    1.59  done
    1.60  
    1.61  (* Antimonotonicity of div in second argument *)
    1.62 @@ -444,7 +449,7 @@
    1.63   prefer 2
    1.64   apply (blast intro: div_le_mono diff_le_mono2)
    1.65  apply (rule le_trans, simp)
    1.66 -apply (simp add: diff_less)
    1.67 +apply (simp)
    1.68  done
    1.69  
    1.70  lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
    1.71 @@ -467,7 +472,7 @@
    1.72   apply (subgoal_tac "(m-n) div n < (m-n) ")
    1.73    apply (rule impI less_trans_Suc)+
    1.74  apply assumption
    1.75 -  apply (simp_all add: diff_less)
    1.76 +  apply (simp_all)
    1.77  done
    1.78  
    1.79  text{*A fact for the mutilated chess board*}
    1.80 @@ -479,7 +484,7 @@
    1.81  apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
    1.82  (* case n \<le> Suc(na) *)
    1.83  apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
    1.84 -apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
    1.85 +apply (auto simp add: Suc_diff_le le_mod_geq)
    1.86  done
    1.87  
    1.88  lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"