equal
deleted
inserted
replaced
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)" |