theory "Mono-Nat-Fun"
imports "Library/Infinite_Set"
begin
text {*
The following lemma proves that a monotonous function from and the natural numbers is either eventually
constant or unbounded.
*}
lemma nat_mono_characterization:
fixes f :: "nat \ nat"
assumes "mono f"
obtains n where "\m . n \ m \ f n = f m" | "\ m . \ n . m \ f n"
proof (cases "finite (range f)")
case True
from Max_in[OF True]
obtain n where Max: "f n = Max (range f)" by auto
show thesis
proof(rule that(1))
fix m
assume "n \ m"
hence "f n \ f m" using `mono f` by (metis monoD)
also
have "f m \ f n" unfolding Max by (rule Max_ge[OF True rangeI])
finally
show "f n = f m".
qed
next
case False
thus thesis by (fastforce intro: that(2) simp add: infinite_nat_iff_unbounded_le)
qed
end