equal
deleted
inserted
replaced
194 |
194 |
195 text{*This simplifies expressions of the form @{term "int n = z"} where |
195 text{*This simplifies expressions of the form @{term "int n = z"} where |
196 z is an integer literal.*} |
196 z is an integer literal.*} |
197 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard] |
197 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard] |
198 |
198 |
|
199 lemmas int_of_nat_eq_iff_number_of [simp] = |
|
200 int_of_nat_eq_iff [of _ "number_of v", standard] |
|
201 |
|
202 lemma split_nat': |
|
203 "P(nat(i::int)) = ((\<forall>n. i = int_of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" |
|
204 (is "?P = (?L & ?R)") |
|
205 proof (cases "i < 0") |
|
206 case True thus ?thesis by simp |
|
207 next |
|
208 case False |
|
209 have "?P = ?L" |
|
210 proof |
|
211 assume ?P thus ?L using False by clarsimp |
|
212 next |
|
213 assume ?L thus ?P using False by simp |
|
214 qed |
|
215 with False show ?thesis by simp |
|
216 qed |
199 |
217 |
200 lemma split_nat [arith_split]: |
218 lemma split_nat [arith_split]: |
201 "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" |
219 "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" |
202 (is "?P = (?L & ?R)") |
220 (is "?P = (?L & ?R)") |
203 proof (cases "i < 0") |
221 proof (cases "i < 0") |