# HG changeset patch
# User nipkow
# Date 1323789281 -3600
# Node ID 033cb3a668b9956b09927793c9443eb1c731544b
# Parent  d4502442452694c78f16a92ff848af5d961bdfc0
lemmas about Kleene iteration

diff -r d45024424526 -r 033cb3a668b9 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Dec 13 15:19:30 2011 +0100
+++ b/src/HOL/Nat.thy	Tue Dec 13 16:14:41 2011 +0100
@@ -1261,6 +1261,30 @@
   by (induct n) simp_all
 
 
+subsection {* Kleene iteration *}
+
+lemma Kleene_iter_lpfp: assumes "mono f" and "f p \<le> p" shows "(f^^k) bot \<le> p"
+proof(induction k)
+  case 0 show ?case by simp
+next
+  case Suc
+  from monoD[OF assms(1) Suc] assms(2)
+  show ?case by simp
+qed
+
+lemma lfp_Kleene_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"
+shows "lfp f = (f^^k) bot"
+proof(rule antisym)
+  show "lfp f \<le> (f^^k) bot"
+  proof(rule lfp_lowerbound)
+    show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp
+  qed
+next
+  show "(f^^k) bot \<le> lfp f"
+    using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
+qed
+
+
 subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
 
 context semiring_1