author berghofe Tue, 25 Mar 2003 09:56:01 +0100 changeset 13882 2266550ab316 parent 13881 f63e2a057fd4 child 13883 0451e0fb3f22
New theorems split_div' and mod_div_equality'.
 src/HOL/Divides.thy file | annotate | diff | comparison | revisions
```--- 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 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
+  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)
+  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"```