src/HOL/Divides.thy
changeset 13517 42efec18f5b2
parent 13189 81ed5c6de890
child 13882 2266550ab316
     1.1 --- a/src/HOL/Divides.thy	Fri Aug 23 07:34:20 2002 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Aug 23 07:41:05 2002 +0200
     1.3 @@ -44,11 +44,6 @@
     1.4  
     1.5  use "Divides_lemmas.ML"
     1.6  
     1.7 -lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
     1.8 -apply(insert mod_div_equality[of m n])
     1.9 -apply(simp only:mult_ac)
    1.10 -done
    1.11 -
    1.12  lemma split_div:
    1.13   "P(n div k :: nat) =
    1.14   ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
    1.15 @@ -85,7 +80,7 @@
    1.16      assume not0: "k \<noteq> 0"
    1.17      with Q have R: ?R by simp
    1.18      from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
    1.19 -    show ?P by(simp add:mod_div_equality2)
    1.20 +    show ?P by simp
    1.21    qed
    1.22  qed
    1.23  
    1.24 @@ -118,7 +113,7 @@
    1.25      assume not0: "k \<noteq> 0"
    1.26      with Q have R: ?R by simp
    1.27      from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
    1.28 -    show ?P by(simp add:mod_div_equality2)
    1.29 +    show ?P by simp
    1.30    qed
    1.31  qed
    1.32  
    1.33 @@ -145,7 +140,7 @@
    1.34  next
    1.35    assume Q: ?Q
    1.36    from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
    1.37 -  show ?P by(simp add:mod_div_equality2)
    1.38 +  show ?P by simp
    1.39  qed
    1.40  
    1.41  lemma split_mod:
    1.42 @@ -163,7 +158,7 @@
    1.43  next
    1.44    assume Q: ?Q
    1.45    from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
    1.46 -  show ?P by(simp add:mod_div_equality2)
    1.47 +  show ?P by simp
    1.48  qed
    1.49  *)
    1.50  end