src/HOL/IntDiv.thy
changeset 23853 2c69bb1374b8
parent 23684 8c508c4dc53b
child 23969 ef782bbf2d09
     1.1 --- a/src/HOL/IntDiv.thy	Thu Jul 19 21:47:37 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Jul 19 21:47:38 2007 +0200
     1.3 @@ -1398,7 +1398,32 @@
     1.4   apply simp_all
     1.5  done
     1.6  
     1.7 -text {* code serializer setup *}
     1.8 +text {* by Brian Huffman *}
     1.9 +lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
    1.10 +by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
    1.11 +
    1.12 +lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
    1.13 +by (simp only: diff_def zmod_zadd_left_eq [symmetric])
    1.14 +
    1.15 +lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
    1.16 +proof -
    1.17 +  have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
    1.18 +    by (simp only: zminus_zmod)
    1.19 +  hence "(x + - (y mod m)) mod m = (x + - y) mod m"
    1.20 +    by (simp only: zmod_zadd_right_eq [symmetric])
    1.21 +  thus "(x - y mod m) mod m = (x - y) mod m"
    1.22 +    by (simp only: diff_def)
    1.23 +qed
    1.24 +
    1.25 +lemmas zmod_simps =
    1.26 +  IntDiv.zmod_zadd_left_eq  [symmetric]
    1.27 +  IntDiv.zmod_zadd_right_eq [symmetric]
    1.28 +  IntDiv.zmod_zmult1_eq     [symmetric]
    1.29 +  IntDiv.zmod_zmult1_eq'    [symmetric]
    1.30 +  IntDiv.zpower_zmod
    1.31 +  zminus_zmod zdiff_zmod_left zdiff_zmod_right
    1.32 +
    1.33 +text {* code generator setup *}
    1.34  
    1.35  code_modulename SML
    1.36    IntDiv Integer