src/HOL/Nat.thy
changeset 59000 6eb0725503fc
parent 58952 5d82cdef6c1b
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Nat.thy	Thu Nov 13 14:40:06 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Nov 13 17:19:52 2014 +0100
     1.3 @@ -1391,6 +1391,12 @@
     1.4  lemma id_funpow[simp]: "id ^^ n = id"
     1.5    by (induct n) simp_all
     1.6  
     1.7 +lemma funpow_mono:
     1.8 +  fixes f :: "'a \<Rightarrow> ('a::lattice)"
     1.9 +  shows "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
    1.10 +  by (induct n arbitrary: A B)
    1.11 +     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
    1.12 +
    1.13  subsection {* Kleene iteration *}
    1.14  
    1.15  lemma Kleene_iter_lpfp:
    1.16 @@ -1848,7 +1854,27 @@
    1.17  lemma dec_induct[consumes 1, case_names base step]:
    1.18    "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
    1.19    by (induct j arbitrary: i) (auto simp: le_Suc_eq)
    1.20 - 
    1.21 +
    1.22 +subsection \<open> Monotonicity of funpow \<close>
    1.23 +
    1.24 +lemma funpow_increasing:
    1.25 +  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_top})"
    1.26 +  shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
    1.27 +  by (induct rule: inc_induct)
    1.28 +     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
    1.29 +           intro: order_trans[OF _ funpow_mono])
    1.30 +
    1.31 +lemma funpow_decreasing:
    1.32 +  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_bot})"
    1.33 +  shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
    1.34 +  by (induct rule: dec_induct)
    1.35 +     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
    1.36 +           intro: order_trans[OF _ funpow_mono])
    1.37 +
    1.38 +lemma mono_funpow:
    1.39 +  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_bot}) \<Rightarrow> ('i \<Rightarrow> 'a)"
    1.40 +  shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
    1.41 +  by (auto intro!: funpow_decreasing simp: mono_def)
    1.42  
    1.43  subsection {* The divides relation on @{typ nat} *}
    1.44