src/HOL/Nat.thy
changeset 45833 033cb3a668b9
parent 45696 476ad865f125
child 45931 99cf6e470816
     1.1 --- a/src/HOL/Nat.thy	Tue Dec 13 15:19:30 2011 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Dec 13 16:14:41 2011 +0100
     1.3 @@ -1261,6 +1261,30 @@
     1.4    by (induct n) simp_all
     1.5  
     1.6  
     1.7 +subsection {* Kleene iteration *}
     1.8 +
     1.9 +lemma Kleene_iter_lpfp: assumes "mono f" and "f p \<le> p" shows "(f^^k) bot \<le> p"
    1.10 +proof(induction k)
    1.11 +  case 0 show ?case by simp
    1.12 +next
    1.13 +  case Suc
    1.14 +  from monoD[OF assms(1) Suc] assms(2)
    1.15 +  show ?case by simp
    1.16 +qed
    1.17 +
    1.18 +lemma lfp_Kleene_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"
    1.19 +shows "lfp f = (f^^k) bot"
    1.20 +proof(rule antisym)
    1.21 +  show "lfp f \<le> (f^^k) bot"
    1.22 +  proof(rule lfp_lowerbound)
    1.23 +    show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp
    1.24 +  qed
    1.25 +next
    1.26 +  show "(f^^k) bot \<le> lfp f"
    1.27 +    using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
    1.28 +qed
    1.29 +
    1.30 +
    1.31  subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
    1.32  
    1.33  context semiring_1