author berghofe Tue Mar 25 09:56:01 2003 +0100 (2003-03-25) changeset 13882 2266550ab316 parent 13881 f63e2a057fd4 child 13883 0451e0fb3f22
New theorems split_div' and mod_div_equality'.
 src/HOL/Divides.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Divides.thy	Tue Mar 25 09:52:21 2003 +0100
1.2 +++ b/src/HOL/Divides.thy	Tue Mar 25 09:56:01 2003 +0100
1.3 @@ -84,6 +84,31 @@
1.4    qed
1.5  qed
1.6
1.7 +lemma split_div_lemma:
1.8 +  "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
1.9 +  apply (rule iffI)
1.10 +  apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
1.11 +  apply (simp_all add: quorem_def)
1.12 +  apply arith
1.13 +  apply (rule conjI)
1.14 +  apply (rule_tac P="%x. n * (m div n) \<le> x" in
1.15 +    subst [OF mod_div_equality [of _ n]])
1.16 +  apply (simp only: add: mult_ac)
1.17 +  apply (rule_tac P="%x. x < n + n * (m div n)" in
1.18 +    subst [OF mod_div_equality [of _ n]])
1.21 +  apply simp
1.22 +  done
1.23 +
1.24 +theorem split_div':
1.25 +  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
1.26 +   (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"
1.27 +  apply (case_tac "0 < n")
1.28 +  apply (simp only: add: split_div_lemma)
1.29 +  apply (simp_all add: DIVISION_BY_ZERO_DIV)
1.30 +  done
1.31 +
1.32  lemma split_mod:
1.33   "P(n mod k :: nat) =
1.34   ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
1.35 @@ -117,6 +142,12 @@
1.36    qed
1.37  qed
1.38
1.39 +theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
1.40 +  apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
1.41 +    subst [OF mod_div_equality [of _ n]])
1.42 +  apply arith
1.43 +  done
1.44 +
1.45  (*
1.46  lemma split_div:
1.47  assumes m: "m \<noteq> 0"
```