--- a/src/HOL/Divides.thy Mon Oct 03 14:34:31 2016 +0200
+++ b/src/HOL/Divides.thy Mon Oct 03 14:34:32 2016 +0200
@@ -542,6 +542,10 @@
"even a \<longleftrightarrow> a mod 2 = 0"
by (fact dvd_eq_mod_eq_0)
+lemma odd_iff_mod_2_eq_one:
+ "odd a \<longleftrightarrow> a mod 2 = 1"
+ by (auto simp add: even_iff_mod_2_eq_zero)
+
lemma even_succ_div_two [simp]:
"even a \<Longrightarrow> (a + 1) div 2 = a div 2"
by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
--- a/src/HOL/Int.thy Mon Oct 03 14:34:31 2016 +0200
+++ b/src/HOL/Int.thy Mon Oct 03 14:34:32 2016 +0200
@@ -983,6 +983,20 @@
end
+lemma transfer_rule_of_int:
+ fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool"
+ assumes [transfer_rule]: "R 0 0" "R 1 1"
+ "rel_fun R (rel_fun R R) plus plus"
+ "rel_fun R R uminus uminus"
+ shows "rel_fun HOL.eq R of_int of_int"
+proof -
+ note transfer_rule_of_nat [transfer_rule]
+ have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat"
+ by transfer_prover
+ show ?thesis
+ by (unfold of_int_of_nat [abs_def]) transfer_prover
+qed
+
lemma nat_mult_distrib:
fixes z z' :: int
assumes "0 \<le> z"
--- a/src/HOL/Transfer.thy Mon Oct 03 14:34:31 2016 +0200
+++ b/src/HOL/Transfer.thy Mon Oct 03 14:34:32 2016 +0200
@@ -602,4 +602,14 @@
end
+
+subsection \<open>@{const of_nat}\<close>
+
+lemma transfer_rule_of_nat:
+ fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
+ assumes [transfer_rule]: "R 0 0" "R 1 1"
+ "rel_fun R (rel_fun R R) plus plus"
+ shows "rel_fun HOL.eq R of_nat of_nat"
+ by (unfold of_nat_def [abs_def]) transfer_prover
+
end