# HG changeset patch
# User berghofe
# Date 1048582561 -3600
# Node ID 2266550ab31627bafbe1b3284fbaba4fdd0adc83
# Parent  f63e2a057fd4baf68a89c2a37e39057e42108f84
New theorems split_div' and mod_div_equality'.

diff -r f63e2a057fd4 -r 2266550ab316 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 25 09:52:21 2003 +0100
+++ b/src/HOL/Divides.thy	Tue Mar 25 09:56:01 2003 +0100
@@ -84,6 +84,31 @@
   qed
 qed
 
+lemma split_div_lemma:
+  "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
+  apply (rule iffI)
+  apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
+  apply (simp_all add: quorem_def)
+  apply arith
+  apply (rule conjI)
+  apply (rule_tac P="%x. n * (m div n) \<le> x" in
+    subst [OF mod_div_equality [of _ n]])
+  apply (simp only: add: mult_ac)
+  apply (rule_tac P="%x. x < n + n * (m div n)" in
+    subst [OF mod_div_equality [of _ n]])
+  apply (simp only: add: mult_ac add_ac)
+  apply (rule add_less_mono1)
+  apply simp
+  done
+
+theorem split_div':
+  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
+   (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"
+  apply (case_tac "0 < n")
+  apply (simp only: add: split_div_lemma)
+  apply (simp_all add: DIVISION_BY_ZERO_DIV)
+  done
+
 lemma split_mod:
  "P(n mod k :: nat) =
  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
@@ -117,6 +142,12 @@
   qed
 qed
 
+theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
+  apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
+    subst [OF mod_div_equality [of _ n]])
+  apply arith
+  done
+
 (*
 lemma split_div:
 assumes m: "m \<noteq> 0"