src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -1676,6 +1676,10 @@
     by (simp add: add.commute)
 qed
 
+lemma of_nat_of_bool [simp]:
+  "of_nat (of_bool P) = of_bool P"
+  by auto
+
 end
 
 declare of_nat_code [code]
@@ -1764,6 +1768,10 @@
 lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
   unfolding abs_if by auto
 
+lemma sgn_of_nat [simp]:
+  "sgn (of_nat n) = of_bool (n > 0)"
+  by simp
+
 end
 
 lemma of_nat_id [simp]: "of_nat n = n"