# HG changeset patch
# User haftmann
# Date 1475498072 -7200
# Node ID ca1239a3277b346535c8eb33598c3bed93192b76
# Parent  048b7dbfdfa36d7c0d03fbd46e02903781d0be3c
more lemmas

diff -r 048b7dbfdfa3 -r ca1239a3277b src/HOL/Divides.thy
--- 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)
diff -r 048b7dbfdfa3 -r ca1239a3277b src/HOL/Int.thy
--- 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"
diff -r 048b7dbfdfa3 -r ca1239a3277b src/HOL/Transfer.thy
--- 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