src/HOL/Divides.thy
 changeset 13882 2266550ab316 parent 13517 42efec18f5b2 child 14131 a4fc8b1af5e7
equal inserted replaced
13881:f63e2a057fd4 13882:2266550ab316
`    82     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]`
`    82     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]`
`    83     show ?P by simp`
`    83     show ?P by simp`
`    84   qed`
`    84   qed`
`    85 qed`
`    85 qed`
`    86 `
`    86 `
`       `
`    87 lemma split_div_lemma:`
`       `
`    88   "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"`
`       `
`    89   apply (rule iffI)`
`       `
`    90   apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)`
`       `
`    91   apply (simp_all add: quorem_def)`
`       `
`    92   apply arith`
`       `
`    93   apply (rule conjI)`
`       `
`    94   apply (rule_tac P="%x. n * (m div n) \<le> x" in`
`       `
`    95     subst [OF mod_div_equality [of _ n]])`
`       `
`    96   apply (simp only: add: mult_ac)`
`       `
`    97   apply (rule_tac P="%x. x < n + n * (m div n)" in`
`       `
`    98     subst [OF mod_div_equality [of _ n]])`
`       `
`    99   apply (simp only: add: mult_ac add_ac)`
`       `
`   100   apply (rule add_less_mono1)`
`       `
`   101   apply simp`
`       `
`   102   done`
`       `
`   103 `
`       `
`   104 theorem split_div':`
`       `
`   105   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>`
`       `
`   106    (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"`
`       `
`   107   apply (case_tac "0 < n")`
`       `
`   108   apply (simp only: add: split_div_lemma)`
`       `
`   109   apply (simp_all add: DIVISION_BY_ZERO_DIV)`
`       `
`   110   done`
`       `
`   111 `
`    87 lemma split_mod:`
`   112 lemma split_mod:`
`    88  "P(n mod k :: nat) =`
`   113  "P(n mod k :: nat) =`
`    89  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"`
`   114  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"`
`    90  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")`
`   115  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")`
`    91 proof`
`   116 proof`
`   114     with Q have R: ?R by simp`
`   139     with Q have R: ?R by simp`
`   115     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]`
`   140     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]`
`   116     show ?P by simp`
`   141     show ?P by simp`
`   117   qed`
`   142   qed`
`   118 qed`
`   143 qed`
`       `
`   144 `
`       `
`   145 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"`
`       `
`   146   apply (rule_tac P="%x. m mod n = x - (m div n) * n" in`
`       `
`   147     subst [OF mod_div_equality [of _ n]])`
`       `
`   148   apply arith`
`       `
`   149   done`
`   119 `
`   150 `
`   120 (*`
`   151 (*`
`   121 lemma split_div:`
`   152 lemma split_div:`
`   122 assumes m: "m \<noteq> 0"`
`   153 assumes m: "m \<noteq> 0"`
`   123 shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"`
`   154 shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"`