# HG changeset patch
# User obua
# Date 1091455573 -7200
# Node ID d027515e2aa61b4767afe4993df703142bcb4101
# Parent  dfb4e23923e044d02ea57f8250a7a6b38d7a3b95
zdiv_int, zmod_int

diff -r dfb4e23923e0 -r d027515e2aa6 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Mon Aug 02 11:20:37 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Mon Aug 02 16:06:13 2004 +0200
@@ -1200,6 +1200,19 @@
 apply (auto simp add: zero_le_mult_iff)
 done
 
+lemma zdiv_int: "int (a div b) = (int a) div (int b)"
+apply (subst split_div, auto)
+apply (subst split_zdiv, auto)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
+apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
+done
+
+lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
+apply (subst split_mod, auto)
+apply (subst split_zmod, auto)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder)
+apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
+done
 
 ML
 {*