New theorems split_div' and mod_div_equality'.
authorberghofe
Tue Mar 25 09:56:01 2003 +0100 (2003-03-25)
changeset 138822266550ab316
parent 13881 f63e2a057fd4
child 13883 0451e0fb3f22
New theorems split_div' and mod_div_equality'.
src/HOL/Divides.thy
     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.19 +  apply (simp only: add: mult_ac add_ac)
    1.20 +  apply (rule add_less_mono1)
    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"