zdiv_int, zmod_int
authorobua
Mon Aug 02 16:06:13 2004 +0200 (2004-08-02)
changeset 15101d027515e2aa6
parent 15100 dfb4e23923e0
child 15102 04b0e943fcc9
zdiv_int, zmod_int
src/HOL/Integ/IntDiv.thy
     1.1 --- a/src/HOL/Integ/IntDiv.thy	Mon Aug 02 11:20:37 2004 +0200
     1.2 +++ b/src/HOL/Integ/IntDiv.thy	Mon Aug 02 16:06:13 2004 +0200
     1.3 @@ -1200,6 +1200,19 @@
     1.4  apply (auto simp add: zero_le_mult_iff)
     1.5  done
     1.6  
     1.7 +lemma zdiv_int: "int (a div b) = (int a) div (int b)"
     1.8 +apply (subst split_div, auto)
     1.9 +apply (subst split_zdiv, auto)
    1.10 +apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
    1.11 +apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
    1.12 +done
    1.13 +
    1.14 +lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
    1.15 +apply (subst split_mod, auto)
    1.16 +apply (subst split_zmod, auto)
    1.17 +apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder)
    1.18 +apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
    1.19 +done
    1.20  
    1.21  ML
    1.22  {*