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>