
diff -r 9963bb965a0e -r 4fdc9f681479 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/Nat.thy	Wed Jul 11 01:04:23 2018 +0200
@@ -1582,6 +1582,28 @@
   qed
 qed
 
+lemma inj_fn[simp]:
+  fixes f::"'a \<Rightarrow> 'a"
+  assumes "inj f"
+  shows "inj (f^^n)"
+proof (induction n)
+  case Suc thus ?case using inj_comp[OF assms Suc.IH] by (simp del: comp_apply)
+qed simp
+
+lemma surj_fn[simp]:
+  fixes f::"'a \<Rightarrow> 'a"
+  assumes "surj f"
+  shows "surj (f^^n)"
+proof (induction n)
+  case Suc thus ?case by (simp add: comp_surj[OF Suc.IH assms] del: comp_apply)
+qed simp
+
+lemma bij_fn[simp]:
+  fixes f::"'a \<Rightarrow> 'a"
+  assumes "bij f"
+  shows "bij (f^^n)"
+by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])
+
 
 subsection \<open>Kleene iteration\<close>
 




