equal
deleted
inserted
replaced
42 a = b*q + r & |
42 a = b*q + r & |
43 (if 0<b then 0<=r & r<b else b<r & r <=0)" |
43 (if 0<b then 0<=r & r<b else b<r & r <=0)" |
44 |
44 |
45 use "Divides_lemmas.ML" |
45 use "Divides_lemmas.ML" |
46 |
46 |
47 lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)" |
|
48 apply(insert mod_div_equality[of m n]) |
|
49 apply(simp only:mult_ac) |
|
50 done |
|
51 |
|
52 lemma split_div: |
47 lemma split_div: |
53 "P(n div k :: nat) = |
48 "P(n div k :: nat) = |
54 ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))" |
49 ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))" |
55 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))") |
50 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))") |
56 proof |
51 proof |
83 with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV) |
78 with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV) |
84 next |
79 next |
85 assume not0: "k \<noteq> 0" |
80 assume not0: "k \<noteq> 0" |
86 with Q have R: ?R by simp |
81 with Q have R: ?R by simp |
87 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"] |
88 show ?P by(simp add:mod_div_equality2) |
83 show ?P by simp |
89 qed |
84 qed |
90 qed |
85 qed |
91 |
86 |
92 lemma split_mod: |
87 lemma split_mod: |
93 "P(n mod k :: nat) = |
88 "P(n mod k :: nat) = |
116 with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD) |
111 with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD) |
117 next |
112 next |
118 assume not0: "k \<noteq> 0" |
113 assume not0: "k \<noteq> 0" |
119 with Q have R: ?R by simp |
114 with Q have R: ?R by simp |
120 from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] |
115 from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"] |
121 show ?P by(simp add:mod_div_equality2) |
116 show ?P by simp |
122 qed |
117 qed |
123 qed |
118 qed |
124 |
119 |
125 (* |
120 (* |
126 lemma split_div: |
121 lemma split_div: |
143 qed |
138 qed |
144 qed |
139 qed |
145 next |
140 next |
146 assume Q: ?Q |
141 assume Q: ?Q |
147 from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] |
142 from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] |
148 show ?P by(simp add:mod_div_equality2) |
143 show ?P by simp |
149 qed |
144 qed |
150 |
145 |
151 lemma split_mod: |
146 lemma split_mod: |
152 assumes m: "m \<noteq> 0" |
147 assumes m: "m \<noteq> 0" |
153 shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)" |
148 shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)" |
161 thus "P j" using m P by(simp add:add_ac mult_ac) |
156 thus "P j" using m P by(simp add:add_ac mult_ac) |
162 qed |
157 qed |
163 next |
158 next |
164 assume Q: ?Q |
159 assume Q: ?Q |
165 from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] |
160 from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"] |
166 show ?P by(simp add:mod_div_equality2) |
161 show ?P by simp |
167 qed |
162 qed |
168 *) |
163 *) |
169 end |
164 end |