380 shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" |
380 shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" |
381 using not0 by (simp add: dvd_def) |
381 using not0 by (simp add: dvd_def) |
382 |
382 |
383 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)" |
383 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)" |
384 by simp_all |
384 by simp_all |
|
385 |
385 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} |
386 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} |
386 lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))" |
387 |
|
388 lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))" |
387 by (simp split add: split_nat) |
389 by (simp split add: split_nat) |
388 |
390 |
389 lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))" |
391 lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))" |
390 apply (auto split add: split_nat) |
392 proof |
391 apply (rule_tac x="int x" in exI, simp) |
393 assume "\<exists>x. P x" |
392 apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp) |
394 then obtain x where "P x" .. |
393 done |
395 then have "int x \<ge> 0 \<and> P (nat (int x))" by simp |
|
396 then show "\<exists>x\<ge>0. P (nat x)" .. |
|
397 next |
|
398 assume "\<exists>x\<ge>0. P (nat x)" |
|
399 then show "\<exists>x. P x" by auto |
|
400 qed |
394 |
401 |
395 lemma zdiff_int_split: "P (int (x - y)) = |
402 lemma zdiff_int_split: "P (int (x - y)) = |
396 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
403 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
397 by (case_tac "y \<le> x", simp_all add: zdiff_int) |
404 by (case_tac "y \<le> x", simp_all add: zdiff_int) |
398 |
405 |