src/HOL/Nat.thy
changeset 60175 831ddb69db9b
parent 59833 ab828c2c5d67
child 60353 838025c6e278
     1.1 --- a/src/HOL/Nat.thy	Mon May 04 18:49:51 2015 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue May 05 14:52:17 2015 +0200
     1.3 @@ -1877,6 +1877,11 @@
     1.4    shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
     1.5    by (auto intro!: funpow_decreasing simp: mono_def)
     1.6  
     1.7 +lemma antimono_funpow:
     1.8 +  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
     1.9 +  shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
    1.10 +  by (auto intro!: funpow_increasing simp: antimono_def)
    1.11 +
    1.12  subsection {* The divides relation on @{typ nat} *}
    1.13  
    1.14  lemma dvd_1_left [iff]: "Suc 0 dvd k"