src/HOL/ex/Function_Growth.thy
 changeset 66936 cf8d8fc23891 parent 66797 9c9baae29217 child 69597 ff784d5a5bfb
```     1.1 --- a/src/HOL/ex/Function_Growth.thy	Sun Oct 29 19:39:03 2017 +0100
1.2 +++ b/src/HOL/ex/Function_Growth.thy	Mon Oct 30 13:18:41 2017 +0000
1.3 @@ -10,40 +10,6 @@
1.4    "HOL-Library.Discrete"
1.5  begin
1.6
1.7 -(* FIXME move *)
1.8 -
1.9 -context linorder
1.10 -begin
1.11 -
1.12 -lemma mono_invE:
1.13 -  fixes f :: "'a \<Rightarrow> 'b::order"
1.14 -  assumes "mono f"
1.15 -  assumes "f x < f y"
1.16 -  obtains "x < y"
1.17 -proof
1.18 -  show "x < y"
1.19 -  proof (rule ccontr)
1.20 -    assume "\<not> x < y"
1.21 -    then have "y \<le> x" by simp
1.22 -    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
1.23 -    with \<open>f x < f y\<close> show False by simp
1.24 -  qed
1.25 -qed
1.26 -
1.27 -end
1.28 -
1.29 -lemma (in semidom_divide) power_diff:
1.30 -  fixes a :: 'a
1.31 -  assumes "a \<noteq> 0"
1.32 -  assumes "m \<ge> n"
1.33 -  shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
1.34 -proof -
1.35 -  define q where "q = m - n"
1.36 -  with assms have "m = q + n" by (simp add: q_def)
1.37 -  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
1.38 -qed
1.39 -
1.40 -
1.41  subsection \<open>Motivation\<close>
1.42
1.43  text \<open>
```