[STATEMENT]
lemma f_nth_derivative_cases:
  "higher_differentiable_on UNIV f k \<and>
   (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and>
   (\<exists>p. real_polynomial_function p \<and>
      (\<forall>t>0. nth_derivative k f t 1 = p t / (t ^ (2 * k)) * exp(-inverse t)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)))
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. higher_differentiable_on UNIV f 0 \<and> (\<forall>t\<le>0. nth_derivative 0 f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))
 2. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. higher_differentiable_on UNIV f 0 \<and> (\<forall>t\<le>0. nth_derivative 0 f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))
 2. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on UNIV f 0 \<and> (\<forall>t\<le>0. nth_derivative 0 f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))
[PROOF STEP]
apply (auto simp: higher_differentiable_on.simps f_continuous)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. real_polynomial_function p \<and> (\<forall>t>0. f t = p t * exp (- inverse t))
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on UNIV f 0 \<and> (\<forall>t\<le>0. nth_derivative 0 f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)))

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
from Suc.IH
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)))
[PROOF STEP]
obtain pk where IH:
    "higher_differentiable_on UNIV f k"
    "\<And>t. t \<le> 0 \<Longrightarrow> nth_derivative k f t 1 = 0"
    "real_polynomial_function pk"
    "\<And>t. t > 0 \<Longrightarrow> nth_derivative k f t 1 = pk t / t ^ (2 * k) * exp (- inverse t)"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)))

goal (1 subgoal):
 1. (\<And>pk. \<lbrakk>higher_differentiable_on UNIV f k; \<And>t. t \<le> 0 \<Longrightarrow> nth_derivative k f t 1 = 0; real_polynomial_function pk; \<And>t. 0 < t \<Longrightarrow> nth_derivative k f t 1 = pk t / t ^ (2 * k) * exp (- inverse t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on UNIV f k
?t \<le> 0 \<Longrightarrow> nth_derivative k f ?t 1 = 0
real_polynomial_function pk
0 < ?t \<Longrightarrow> nth_derivative k f ?t 1 = pk ?t / ?t ^ (2 * k) * exp (- inverse ?t)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
from f_nth_derivative_lt_0[of "Suc k"]
    local.f_nth_derivative_is_poly[of "Suc k"]
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
obtain p where neg: "higher_differentiable_on {..<0} f (Suc k)"
    and neg0: "(\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)"
    and pos: "higher_differentiable_on {0<..} f (Suc k)"
    and p: "real_polynomial_function p"
    "\<And>t. t > 0 \<Longrightarrow> nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>higher_differentiable_on {..<0} f (Suc k); \<forall>t<0. nth_derivative (Suc k) f t 1 = 0; higher_differentiable_on {0<..} f (Suc k); real_polynomial_function p; \<And>t. 0 < t \<Longrightarrow> nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {..<0} f (Suc k)
\<forall>t<0. nth_derivative (Suc k) f t 1 = 0
higher_differentiable_on {0<..} f (Suc k)
real_polynomial_function p
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = p ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {..<0} f (Suc k)
\<forall>t<0. nth_derivative (Suc k) f t 1 = 0
higher_differentiable_on {0<..} f (Suc k)
real_polynomial_function p
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = p ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have at_within_eq_at_right: "(at 0 within {0..}) = at_right (0::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at 0 within {0..} = at_right 0
[PROOF STEP]
apply (auto simp: filter_eq_iff eventually_at_filter )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> 0 \<le> x \<longrightarrow> P x \<Longrightarrow> \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> 0 < x \<longrightarrow> P x
 2. \<And>P. \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> 0 < x \<longrightarrow> P x \<Longrightarrow> \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> 0 \<le> x \<longrightarrow> P x
[PROOF STEP]
apply (simp add: eventually_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> 0 < x \<longrightarrow> P x \<Longrightarrow> \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> 0 \<le> x \<longrightarrow> P x
[PROOF STEP]
apply (simp add: eventually_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
at 0 within {0..} = at_right 0

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have [simp]: "{0..} - {0} = {0::real<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..} - {0} = {0<..}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..} - {0} = {0<..}

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have [simp]: "(at (0::real) within {0..}) \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at 0 within {0..} \<noteq> bot
[PROOF STEP]
by (auto simp: at_within_eq_bot_iff)
[PROOF STATE]
proof (state)
this:
at 0 within {0..} \<noteq> bot

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have k_th_has_derivative_at_left:
    "((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {..0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {..0})
[PROOF STEP]
apply (rule has_derivative_transform_within[OF _ zero_less_one])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (?f has_derivative (\<lambda>x. 0)) (at 0 within {..0})
 2. 0 \<in> {..0}
 3. \<And>x'. \<lbrakk>x' \<in> {..0}; dist x' 0 < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative k f x' 1
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 \<in> {..0}
 2. (?f has_derivative (\<lambda>x. 0)) (at 0 within {..0})
 3. \<And>x'. \<lbrakk>x' \<in> {..0}; dist x' 0 < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative k f x' 1
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (?f has_derivative (\<lambda>x. 0)) (at 0 within {..0})
 2. \<And>x'. \<lbrakk>x' \<in> {..0}; dist x' 0 < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative k f x' 1
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x'. \<lbrakk>x' \<in> {..0}; dist x' 0 < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative k f x' 1
 2. (?f has_derivative (\<lambda>x. 0)) (at 0 within {..0})
[PROOF STEP]
apply (simp add: IH)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x'. 0) has_derivative (\<lambda>x. 0)) (at 0 within {..0})
[PROOF STEP]
by (rule derivative_intros)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {..0})

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have k_th_has_derivative_at_right:
    "((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {0..})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {0..})
[PROOF STEP]
apply (rule has_derivative_transform_within[where
          f="\<lambda>x'. if x' = 0 then 0 else pk x' / x' ^ (2 * k) * exp (- inverse x')", OF _ zero_less_one])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ((\<lambda>x'. if x' = 0 then 0 else pk x' / x' ^ (2 * k) * exp (- inverse x')) has_derivative (\<lambda>x. 0)) (at 0 within {0..})
 2. 0 \<in> {0..}
 3. \<And>x'. \<lbrakk>x' \<in> {0..}; dist x' 0 < 1\<rbrakk> \<Longrightarrow> (if x' = 0 then 0 else pk x' / x' ^ (2 * k) * exp (- inverse x')) = nth_derivative k f x' 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x'. if x' = 0 then 0 else pk x' / x' ^ (2 * k) * exp (- inverse x')) has_derivative (\<lambda>x. 0)) (at 0 within {0..})
[PROOF STEP]
unfolding has_derivative_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>x. 0) \<and> ((\<lambda>y. ((if y = 0 then 0 else pk y / y ^ (2 * k) * exp (- inverse y)) - (if netlimit (at 0 within {0..}) = 0 then 0 else pk (netlimit (at 0 within {0..})) / netlimit (at 0 within {0..}) ^ (2 * k) * exp (- inverse (netlimit (at 0 within {0..})))) - 0) /\<^sub>R norm (y - netlimit (at 0 within {0..}))) \<longlongrightarrow> 0) (at 0 within {0..})
[PROOF STEP]
apply (auto simp: Lim_ident_at)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>y. inverse \<bar>y\<bar> * (if y = 0 then 0 else pk y / y ^ (2 * k) * exp (- inverse y))) \<longlongrightarrow> 0) (at 0 within {0..})
[PROOF STEP]
apply (rule Lim_transform_eventually[where f="\<lambda>x. (pk x * (exp (- inverse x) / x ^ (2 * k + 1)))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>x. pk x * (exp (- inverse x) / x ^ (2 * k + 1))) \<longlongrightarrow> 0) (at 0 within {0..})
 2. \<forall>\<^sub>F x in at 0 within {0..}. pk x * (exp (- inverse x) / x ^ (2 * k + 1)) = inverse \<bar>x\<bar> * (if x = 0 then 0 else pk x / x ^ (2 * k) * exp (- inverse x))
[PROOF STEP]
apply (rule tendsto_eq_intros)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (pk \<longlongrightarrow> ?a6) (at 0 within {0..})
 2. ((\<lambda>x. exp (- inverse x) / x ^ (2 * k + 1)) \<longlongrightarrow> ?b6) (at 0 within {0..})
 3. ?a6 * ?b6 = 0
 4. \<forall>\<^sub>F x in at 0 within {0..}. pk x * (exp (- inverse x) / x ^ (2 * k + 1)) = inverse \<bar>x\<bar> * (if x = 0 then 0 else pk x / x ^ (2 * k) * exp (- inverse x))
[PROOF STEP]
apply (rule real_polynomial_function_tendsto[THEN tendsto_eq_rhs])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. real_polynomial_function pk
 2. pk 0 = ?a6
 3. ((\<lambda>x. exp (- inverse x) / x ^ (2 * k + 1)) \<longlongrightarrow> ?b6) (at 0 within {0..})
 4. ?a6 * ?b6 = 0
 5. \<forall>\<^sub>F x in at 0 within {0..}. pk x * (exp (- inverse x) / x ^ (2 * k + 1)) = inverse \<bar>x\<bar> * (if x = 0 then 0 else pk x / x ^ (2 * k) * exp (- inverse x))
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. pk 0 = ?a6
 2. ((\<lambda>x. exp (- inverse x) / x ^ (2 * k + 1)) \<longlongrightarrow> ?b6) (at 0 within {0..})
 3. ?a6 * ?b6 = 0
 4. \<forall>\<^sub>F x in at 0 within {0..}. pk x * (exp (- inverse x) / x ^ (2 * k + 1)) = inverse \<bar>x\<bar> * (if x = 0 then 0 else pk x / x ^ (2 * k) * exp (- inverse x))
[PROOF STEP]
apply (rule refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ((\<lambda>x. exp (- inverse x) / x ^ (2 * k + 1)) \<longlongrightarrow> ?b6) (at 0 within {0..})
 2. pk 0 * ?b6 = 0
 3. \<forall>\<^sub>F x in at 0 within {0..}. pk x * (exp (- inverse x) / x ^ (2 * k + 1)) = inverse \<bar>x\<bar> * (if x = 0 then 0 else pk x / x ^ (2 * k) * exp (- inverse x))
[PROOF STEP]
apply (subst at_within_eq_at_right)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ((\<lambda>x. exp (- inverse x) / x ^ (2 * k + 1)) \<longlongrightarrow> ?b6) (at_right 0)
 2. pk 0 * ?b6 = 0
 3. \<forall>\<^sub>F x in at 0 within {0..}. pk x * (exp (- inverse x) / x ^ (2 * k + 1)) = inverse \<bar>x\<bar> * (if x = 0 then 0 else pk x / x ^ (2 * k) * exp (- inverse x))
[PROOF STEP]
apply (rule exp_inv_limit_0_right_gen)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pk 0 * 0 = 0
 2. \<forall>\<^sub>F x in at 0 within {0..}. pk x * (exp (- inverse x) / x ^ (2 * k + 1)) = inverse \<bar>x\<bar> * (if x = 0 then 0 else pk x / x ^ (2 * k) * exp (- inverse x))
[PROOF STEP]
apply (auto simp add: eventually_at_filter divide_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<in> {0..}
 2. \<And>x'. \<lbrakk>x' \<in> {0..}; dist x' 0 < 1\<rbrakk> \<Longrightarrow> (if x' = 0 then 0 else pk x' / x' ^ (2 * k) * exp (- inverse x')) = nth_derivative k f x' 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> {0..}
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x'. \<lbrakk>x' \<in> {0..}; dist x' 0 < 1\<rbrakk> \<Longrightarrow> (if x' = 0 then 0 else pk x' / x' ^ (2 * k) * exp (- inverse x')) = nth_derivative k f x' 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x'_ \<in> {0..}; dist x'_ 0 < 1\<rbrakk> \<Longrightarrow> (if x'_ = 0 then 0 else pk x'_ / x'_ ^ (2 * k) * exp (- inverse x'_)) = nth_derivative k f x'_ 1
[PROOF STEP]
by (auto simp: IH(2) IH(4))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {0..})

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have k_th_has_derivative: "((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0)
[PROOF STEP]
apply (rule has_derivative_at_left_at_right')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {..0})
 2. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {0..})
[PROOF STEP]
apply (rule k_th_has_derivative_at_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0 within {0..})
[PROOF STEP]
apply (rule k_th_has_derivative_at_right)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have nth_Suc_zero: "nth_derivative (Suc k) f 0 1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_derivative (Suc k) f 0 1 = 0
[PROOF STEP]
apply (auto simp: frechet_derivative_nth_derivative_commute[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at 0) 1 = 0
[PROOF STEP]
apply (subst frechet_derivative_at')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative ?y) (at 0)
 2. ?y 1 = 0
[PROOF STEP]
apply (rule k_th_has_derivative)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_derivative (Suc k) f 0 1 = 0

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nth_derivative (Suc k) f 0 1 = 0

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have "higher_differentiable_on UNIV f (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
have "continuous_on UNIV (\<lambda>x. nth_derivative (Suc k) f x 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. nth_derivative (Suc k) f x 1)
[PROOF STEP]
unfolding continuous_on_eq_continuous_within
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
fix x::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
consider "x < 0" | "x > 0" | "x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 0 \<Longrightarrow> thesis; 0 < x \<Longrightarrow> thesis; x = 0 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<lbrakk>x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis; x = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis; x = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis; x = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x < 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 2. 0 < x \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 3. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x < 0

goal (3 subgoals):
 1. x < 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 2. 0 < x \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 3. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < 0
[PROOF STEP]
have at_eq: "at x = at x within {..<0}"
[PROOF STATE]
proof (prove)
using this:
x < 0

goal (1 subgoal):
 1. at x = at x within {..<0}
[PROOF STEP]
using at_within_open[of x "{..<0}"]
[PROOF STATE]
proof (prove)
using this:
x < 0
\<lbrakk>x \<in> {..<0}; open {..<0}\<rbrakk> \<Longrightarrow> at x within {..<0} = at x

goal (1 subgoal):
 1. at x = at x within {..<0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
at x = at x within {..<0}

goal (3 subgoals):
 1. x < 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 2. 0 < x \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 3. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
unfolding at_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at x within {..<0}) (\<lambda>x. nth_derivative (Suc k) f x 1)
[PROOF STEP]
apply (rule continuous_transform_within[OF _ zero_less_one])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous (at x within {..<0}) ?f
 2. x \<in> {..<0}
 3. \<And>x'. \<lbrakk>x' \<in> {..<0}; dist x' x < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative (Suc k) f x' 1
[PROOF STEP]
using neg0 1
[PROOF STATE]
proof (prove)
using this:
\<forall>t<0. nth_derivative (Suc k) f t 1 = 0
x < 0

goal (3 subgoals):
 1. continuous (at x within {..<0}) ?f
 2. x \<in> {..<0}
 3. \<And>x'. \<lbrakk>x' \<in> {..<0}; dist x' x < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative (Suc k) f x' 1
[PROOF STEP]
by (auto simp: at_eq)
[PROOF STATE]
proof (state)
this:
isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x

goal (2 subgoals):
 1. 0 < x \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 2. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < x \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 2. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < x

goal (2 subgoals):
 1. 0 < x \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 2. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < x
[PROOF STEP]
have at_eq: "at x = at x within {0<..}"
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. at x = at x within {0<..}
[PROOF STEP]
using at_within_open[of x "{0<..}"]
[PROOF STATE]
proof (prove)
using this:
0 < x
\<lbrakk>x \<in> {0<..}; open {0<..}\<rbrakk> \<Longrightarrow> at x within {0<..} = at x

goal (1 subgoal):
 1. at x = at x within {0<..}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
at x = at x within {0<..}

goal (2 subgoals):
 1. 0 < x \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
 2. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
unfolding at_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at x within {0<..}) (\<lambda>x. nth_derivative (Suc k) f x 1)
[PROOF STEP]
apply (rule continuous_transform_within[OF _ zero_less_one])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous (at x within {0<..}) ?f
 2. x \<in> {0<..}
 3. \<And>x'. \<lbrakk>x' \<in> {0<..}; dist x' x < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative (Suc k) f x' 1
[PROOF STEP]
using p 2
[PROOF STATE]
proof (prove)
using this:
real_polynomial_function p
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = p ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)
0 < x

goal (3 subgoals):
 1. continuous (at x within {0<..}) ?f
 2. x \<in> {0<..}
 3. \<And>x'. \<lbrakk>x' \<in> {0<..}; dist x' x < 1\<rbrakk> \<Longrightarrow> ?f x' = nth_derivative (Suc k) f x' 1
[PROOF STEP]
by (auto intro!: continuous_intros
              intro: continuous_real_polymonial_function continuous_at_imp_continuous_within)
[PROOF STATE]
proof (state)
this:
isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
x = 0

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
have "((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)
[PROOF STEP]
have "\<forall>\<^sub>F x in at_left 0. 0 = nth_derivative (Suc k) f x 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_left 0. 0 = nth_derivative (Suc k) f x 1
[PROOF STEP]
using neg0
[PROOF STATE]
proof (prove)
using this:
\<forall>t<0. nth_derivative (Suc k) f t 1 = 0

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_left 0. 0 = nth_derivative (Suc k) f x 1
[PROOF STEP]
by (auto simp: eventually_at_filter)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_left 0. 0 = nth_derivative (Suc k) f x 1

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at_left 0. 0 = nth_derivative (Suc k) f x 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_left 0. 0 = nth_derivative (Suc k) f x 1

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)
[PROOF STEP]
by (blast intro: Lim_transform_eventually)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
have "((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
have "((\<lambda>x. p x * (exp (- inverse x) / x ^ (2 * Suc k))) \<longlongrightarrow> 0) (at_right 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. p x * (exp (- inverse x) / x ^ (2 * Suc k))) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
apply (rule tendsto_eq_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (p \<longlongrightarrow> ?a1) (at_right 0)
 2. ((\<lambda>x. exp (- inverse x) / x ^ (2 * Suc k)) \<longlongrightarrow> ?b1) (at_right 0)
 3. ?a1 * ?b1 = 0
[PROOF STEP]
apply (rule real_polynomial_function_tendsto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. real_polynomial_function p
 2. ((\<lambda>x. exp (- inverse x) / x ^ (2 * Suc k)) \<longlongrightarrow> ?b1) (at_right 0)
 3. p 0 * ?b1 = 0
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>x. exp (- inverse x) / x ^ (2 * Suc k)) \<longlongrightarrow> ?b1) (at_right 0)
 2. p 0 * ?b1 = 0
[PROOF STEP]
apply (rule exp_inv_limit_0_right_gen)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p 0 * 0 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>x. p x * (exp (- inverse x) / x ^ (2 * Suc k))) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((\<lambda>x. p x * (exp (- inverse x) / x ^ (2 * Suc k))) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
have "\<forall>\<^sub>F x in at_right 0. p x * (exp (- inverse x) / x ^ (2 * Suc k)) =
            nth_derivative (Suc k) f x 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_right 0. p x * (exp (- inverse x) / x ^ (2 * Suc k)) = nth_derivative (Suc k) f x 1
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
real_polynomial_function p
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = p ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_right 0. p x * (exp (- inverse x) / x ^ (2 * Suc k)) = nth_derivative (Suc k) f x 1
[PROOF STEP]
by (auto simp: eventually_at_filter)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_right 0. p x * (exp (- inverse x) / x ^ (2 * Suc k)) = nth_derivative (Suc k) f x 1

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. p x * (exp (- inverse x) / x ^ (2 * Suc k))) \<longlongrightarrow> 0) (at_right 0)
\<forall>\<^sub>F x in at_right 0. p x * (exp (- inverse x) / x ^ (2 * Suc k)) = nth_derivative (Suc k) f x 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. p x * (exp (- inverse x) / x ^ (2 * Suc k))) \<longlongrightarrow> 0) (at_right 0)
\<forall>\<^sub>F x in at_right 0. p x * (exp (- inverse x) / x ^ (2 * Suc k)) = nth_derivative (Suc k) f x 1

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
by (rule Lim_transform_eventually)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_left 0)
((\<lambda>x. nth_derivative (Suc k) f x 1) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x
[PROOF STEP]
by (auto simp: continuous_def nth_Suc_zero 3 filterlim_split_at
              simp del: nth_derivative.simps)
[PROOF STATE]
proof (state)
this:
isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
isCont (\<lambda>x. nth_derivative (Suc k) f x 1) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. nth_derivative (Suc k) f x 1)

goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. nth_derivative (Suc k) f x 1)

goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
have "(\<lambda>x. nth_derivative k f x 1) differentiable at x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
consider  "x = 0" | "x < 0" | "x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 0 \<Longrightarrow> thesis; x < 0 \<Longrightarrow> thesis; 0 < x \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = 0 \<Longrightarrow> ?thesis; x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = 0 \<Longrightarrow> ?thesis; x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = 0 \<Longrightarrow> ?thesis; x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x = 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
 2. x < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
 3. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x = 0

goal (3 subgoals):
 1. x = 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
 2. x < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
 3. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
using k_th_has_derivative
[PROOF STATE]
proof (prove)
using this:
x = 0
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>x. 0)) (at 0)

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
by (auto simp: differentiable_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. nth_derivative k f x 1) differentiable at x

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
 2. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
 2. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x < 0

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
 2. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
with neg
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on {..<0} f (Suc k)
x < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on {..<0} f (Suc k)
x < 0

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
by (subst (asm) higher_differentiable_on_real_Suc') auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. nth_derivative k f x 1) differentiable at x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
0 < x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
with pos
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on {0<..} f (Suc k)
0 < x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on {0<..} f (Suc k)
0 < x

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at x
[PROOF STEP]
by (subst (asm) higher_differentiable_on_real_Suc') auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. nth_derivative k f x 1) differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. nth_derivative k f x 1) differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. nth_derivative k f x 1) differentiable at ?x

goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. nth_derivative k f x 1) differentiable at ?x

goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
have "higher_differentiable_on UNIV f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on UNIV f k
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
higher_differentiable_on UNIV f k

goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
continuous_on UNIV (\<lambda>x. nth_derivative (Suc k) f x 1)
(\<lambda>x. nth_derivative k f x 1) differentiable at ?x
higher_differentiable_on UNIV f k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. nth_derivative (Suc k) f x 1)
(\<lambda>x. nth_derivative k f x 1) differentiable at ?x
higher_differentiable_on UNIV f k

goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
by (subst higher_differentiable_on_real_Suc'[OF open_UNIV]) auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on UNIV f (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
higher_differentiable_on UNIV f (Suc k)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on UNIV f k \<and> (\<forall>t\<le>0. nth_derivative k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on {..<0} f (Suc k)
\<forall>t<0. nth_derivative (Suc k) f t 1 = 0
higher_differentiable_on {0<..} f (Suc k)
real_polynomial_function p
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = p ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)
nth_derivative (Suc k) f 0 1 = 0
higher_differentiable_on UNIV f (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on {..<0} f (Suc k)
\<forall>t<0. nth_derivative (Suc k) f t 1 = 0
higher_differentiable_on {0<..} f (Suc k)
real_polynomial_function p
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = p ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)
nth_derivative (Suc k) f 0 1 = 0
higher_differentiable_on UNIV f (Suc k)

goal (1 subgoal):
 1. higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
by (auto simp: less_eq_real_def)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on UNIV f (Suc k) \<and> (\<forall>t\<le>0. nth_derivative (Suc k) f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_smooth_on: "k-smooth_on S f"
  and f_higher_differentiable_on: "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S f &&& higher_differentiable_on S f n
[PROOF STEP]
using f_nth_derivative_cases
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on UNIV f ?k \<and> (\<forall>t\<le>0. nth_derivative ?k f t 1 = 0) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative ?k f t 1 = p t / t ^ (2 * ?k) * exp (- inverse t)))

goal (1 subgoal):
 1. k-smooth_on S f &&& higher_differentiable_on S f n
[PROOF STEP]
by (auto simp: smooth_on_def higher_differentiable_on_subset[OF _ subset_UNIV])


[STATEMENT]
lemma f_compose_smooth_on: "k-smooth_on S (\<lambda>x. f (g x))"
  if "k-smooth_on S g" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. f (g x))
[PROOF STEP]
using smooth_on_compose[OF f_smooth_on that open_UNIV subset_UNIV]
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S (f \<circ> g)

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. f (g x))
[PROOF STEP]
by (auto simp: o_def)


[STATEMENT]
lemma f_nonneg: "f x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> f x
[PROOF STEP]
by (auto simp: f_def)


[STATEMENT]
lemma f_pos_iff: "f x > 0 \<longleftrightarrow> x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < f x) = (0 < x)
[PROOF STEP]
by (auto simp: f_def)


[STATEMENT]
lemma f_eq_zero_iff: "f x = 0 \<longleftrightarrow> x \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f x = 0) = (x \<le> 0)
[PROOF STEP]
by (auto simp: f_def)


[STATEMENT]
lemma denominator_pos: "f (2 - t) + f (t - 1) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < f (2 - t) + f (t - 1)
[PROOF STEP]
by (auto simp: f_def add_pos_pos)


[STATEMENT]
lemma denominator_nonzero: "f (2 - t) + f (t - 1) = 0 \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f (2 - t) + f (t - 1) = 0) = False
[PROOF STEP]
using denominator_pos[of t]
[PROOF STATE]
proof (prove)
using this:
0 < f (2 - t) + f (t - 1)

goal (1 subgoal):
 1. (f (2 - t) + f (t - 1) = 0) = False
[PROOF STEP]
by auto


[STATEMENT]
lemma h_range: "0 \<le> h t" "h t \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> h t &&& h t \<le> 1
[PROOF STEP]
by (auto simp: h_def f_nonneg denominator_pos)


[STATEMENT]
lemma h_pos: "t < 2 \<Longrightarrow> 0 < h t"
  and h_less_one: "1 < t \<Longrightarrow> h t < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t < 2 \<Longrightarrow> 0 < h t) &&& (1 < t \<Longrightarrow> h t < 1)
[PROOF STEP]
by (auto simp: h_def f_pos_iff denominator_pos)


[STATEMENT]
lemma h_eq_0: "h t = 0" if "t \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h t = 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
2 \<le> t

goal (1 subgoal):
 1. h t = 0
[PROOF STEP]
by (auto simp: h_def)


[STATEMENT]
lemma h_eq_1: "h t = 1" if "t \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h t = 1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
t \<le> 1

goal (1 subgoal):
 1. h t = 1
[PROOF STEP]
by (auto simp: h_def f_eq_zero_iff)


[STATEMENT]
lemma h_compose_smooth_on: "k-smooth_on S (\<lambda>x. h (g x))"
  if "k-smooth_on S g" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. h (g x))
[PROOF STEP]
by (auto simp: h_def[abs_def] denominator_nonzero
      intro!: smooth_on_divide f_compose_smooth_on smooth_on_minus smooth_on_add
      that)


[STATEMENT]
lemma H_range: "0 \<le> H x" "H x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> H x &&& H x \<le> 1
[PROOF STEP]
by (auto simp: H_def h_range)


[STATEMENT]
lemma H_eq_one: "H x = 1" if "x \<in> cball 0 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H x = 1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> cball (0::'a) 1

goal (1 subgoal):
 1. H x = 1
[PROOF STEP]
by (auto simp: H_def h_eq_1)


[STATEMENT]
lemma H_pos: "H x > 0" if "x \<in> ball 0 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < H x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> ball (0::'a) 2

goal (1 subgoal):
 1. 0 < H x
[PROOF STEP]
by (auto simp: H_def h_pos)


[STATEMENT]
lemma H_eq_zero: "H x = 0" if "x \<notin> ball 0 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H x = 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<notin> ball (0::'a) 2

goal (1 subgoal):
 1. H x = 0
[PROOF STEP]
by (auto simp: H_def h_eq_0)


[STATEMENT]
lemma H_neq_zeroD: "H x \<noteq> 0 \<Longrightarrow> x \<in> ball 0 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H x \<noteq> 0 \<Longrightarrow> x \<in> ball (0::'a) 2
[PROOF STEP]
using H_eq_zero
[PROOF STATE]
proof (prove)
using this:
?x \<notin> ball (0::?'a) 2 \<Longrightarrow> H ?x = 0

goal (1 subgoal):
 1. H x \<noteq> 0 \<Longrightarrow> x \<in> ball (0::'a) 2
[PROOF STEP]
by blast


[STATEMENT]
lemma H_smooth_on: "k-smooth_on UNIV H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
have 1: "k-smooth_on (ball 0 1) H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (ball (0::'b) 1) H
[PROOF STEP]
by (rule smooth_on_cong[where g="\<lambda>x. 1"]) (auto simp: H_eq_one)
[PROOF STATE]
proof (state)
this:
k-smooth_on (ball (0::?'b1) 1) H

goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
have 2: "k-smooth_on (UNIV - cball 0 (1/2)) H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (UNIV - cball (0::'b) (1 / 2)) H
[PROOF STEP]
by (auto simp: H_def[abs_def]
        intro!: h_compose_smooth_on smooth_on_norm)
[PROOF STATE]
proof (state)
this:
k-smooth_on (UNIV - cball (0::?'b2) (1 / 2)) H

goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
have O: "open (ball 0 1)" "open (UNIV - cball 0 (1 / 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (ball (0::'b) 1) &&& open (UNIV - cball (0::'c) (1 / 2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open (ball (0::?'b3) 1)
open (UNIV - cball (0::?'c3) (1 / 2))

goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
have *: "ball 0 1 \<union> (UNIV - cball 0 (1 / 2)) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ball (0::'b) 1 \<union> (UNIV - cball (0::'b) (1 / 2)) = UNIV
[PROOF STEP]
by (auto simp: mem_ball)
[PROOF STATE]
proof (state)
this:
ball (0::?'b4) 1 \<union> (UNIV - cball (0::?'b4) (1 / 2)) = UNIV

goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
from smooth_on_open_Un[OF 1 2 O, unfolded *]
[PROOF STATE]
proof (chain)
picking this:
k-smooth_on UNIV H
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k-smooth_on UNIV H

goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
by (rule smooth_on_subset) auto
[PROOF STATE]
proof (state)
this:
k-smooth_on UNIV H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma H_compose_smooth_on: "k-smooth_on S (\<lambda>x. H (g x))" if "k-smooth_on S g" "open S"
  for g :: "_ \<Rightarrow> _::euclidean_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. H (g x))
[PROOF STEP]
using smooth_on_compose[OF H_smooth_on that]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>open UNIV; g ` S \<subseteq> UNIV\<rbrakk> \<Longrightarrow> k-smooth_on S (H \<circ> g)

goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. H (g x))
[PROOF STEP]
by (auto simp: o_def)


[STATEMENT]
lemma map_of_map_Pair_const:
  "map_of (map (\<lambda>x. (x, v)) xs) = (\<lambda>x. if x \<in> set xs then Some v else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>x. (x, v)) xs) = (\<lambda>x. if x \<in> set xs then Some v else None)
[PROOF STEP]
by(induct xs) auto


[STATEMENT]
lemma map_of_rev_unit [simp]:
  fixes xs :: "('a * unit) list"
  shows "map_of (rev xs) = map_of xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (rev xs) = map_of xs
[PROOF STEP]
by(induct xs rule: rev_induct)(auto simp add: map_add_def split: option.split)


[STATEMENT]
lemma fold_split_conv_map_fst: "fold (\<lambda>(x, y). f x) xs = fold f (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>(x, y). f x) xs = fold f (map fst xs)
[PROOF STEP]
by(simp add: fold_map o_def split_def)


[STATEMENT]
lemma foldr_split_conv_map_fst: "foldr (\<lambda>(x, y). f x) xs = foldr f (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>(x, y). f x) xs = foldr f (map fst xs)
[PROOF STEP]
by(simp add: foldr_map o_def split_def fun_eq_iff)


[STATEMENT]
lemma set_foldr_Cons:
  "set (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []) \<subseteq> set as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []) \<subseteq> set as
[PROOF STEP]
by(induct as) auto


[STATEMENT]
lemma distinct_fst_foldr_Cons:
  "distinct (map f as) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map f as) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
[PROOF STEP]
proof(induct as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct (map f []) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) [] []))
 2. \<And>a as. \<lbrakk>distinct (map f as) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as [])); distinct (map f (a # as))\<rbrakk> \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
distinct (map f as) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
distinct (map f (a # as))

goal (2 subgoals):
 1. distinct (map f []) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) [] []))
 2. \<And>a as. \<lbrakk>distinct (map f as) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as [])); distinct (map f (a # as))\<rbrakk> \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))
[PROOF STEP]
with set_foldr_Cons[of P as]
[PROOF STATE]
proof (chain)
picking this:
set (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []) \<subseteq> set as
distinct (map f as) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
distinct (map f (a # as))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []) \<subseteq> set as
distinct (map f as) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
distinct (map f (a # as))

goal (1 subgoal):
 1. distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))

goal (1 subgoal):
 1. distinct (map f []) \<Longrightarrow> distinct (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) [] []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma filter_conv_foldr:
  "filter P xs = foldr (\<lambda>x xs. if P x then x # xs else xs) xs []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P xs = foldr (\<lambda>x xs. if P x then x # xs else xs) xs []
[PROOF STEP]
by(induct xs) simp_all


[STATEMENT]
lemma map_of_filter: "map_of (filter (\<lambda>x. P (fst x)) xs) = map_of xs |` Collect P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (filter (\<lambda>x. P (fst x)) xs) = map_of xs |` Collect P
[PROOF STEP]
by(induct xs)(simp_all add: fun_eq_iff restrict_map_def)


[STATEMENT]
lemma map_of_map_Pair_key: "map_of (map (\<lambda>k. (k, f k)) xs) x = (if x \<in> set xs then Some (f x) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>k. (k, f k)) xs) x = (if x \<in> set xs then Some (f x) else None)
[PROOF STEP]
by(induct xs) simp_all


[STATEMENT]
lemma neq_Empty_conv: "t \<noteq> rbt.Empty \<longleftrightarrow> (\<exists>c l k v r. t = Branch c l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<noteq> rbt.Empty) = (\<exists>c l k v r. t = Branch c l k v r)
[PROOF STEP]
by(cases t) simp_all


[STATEMENT]
lemma is_rbt_RBT_fold_rbt_insert [simp]:
  "is_rbt t \<Longrightarrow> is_rbt (fold (\<lambda>(k, v). rbt_insert k v) xs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> is_rbt (fold (\<lambda>(k, v). rbt_insert k v) xs t)
[PROOF STEP]
by(induct xs arbitrary: t)(simp_all add: split_beta)


[STATEMENT]
lemma rbt_lookup_RBT_fold_rbt_insert [simp]:
  "is_rbt t \<Longrightarrow> rbt_lookup (fold (\<lambda>(k, v). rbt_insert k v) xs t) = rbt_lookup t ++ map_of (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> rbt_lookup (fold (\<lambda>(k, v). rbt_insert k v) xs t) = rbt_lookup t ++ map_of (rev xs)
[PROOF STEP]
apply(induct xs arbitrary: t rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. is_rbt t \<Longrightarrow> rbt_lookup (fold (\<lambda>(x, y). rbt_insert x y) [] t) = rbt_lookup t ++ map_of (rev [])
 2. \<And>x xs t. \<lbrakk>\<And>t. is_rbt t \<Longrightarrow> rbt_lookup (fold (\<lambda>(x, y). rbt_insert x y) xs t) = rbt_lookup t ++ map_of (rev xs); is_rbt t\<rbrakk> \<Longrightarrow> rbt_lookup (fold (\<lambda>(x, y). rbt_insert x y) (xs @ [x]) t) = rbt_lookup t ++ map_of (rev (xs @ [x]))
[PROOF STEP]
apply(simp_all add: split_beta fun_eq_iff rbt_lookup_rbt_insert)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_rbt_fold_rbt_delete [simp]:
  "is_rbt t \<Longrightarrow> is_rbt (fold rbt_delete xs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> is_rbt (fold rbt_delete xs t)
[PROOF STEP]
by(induct xs arbitrary: t)(simp_all)


[STATEMENT]
lemma rbt_lookup_fold_rbt_delete [simp]:
  "is_rbt t \<Longrightarrow> rbt_lookup (fold rbt_delete xs t) = rbt_lookup t |` (- set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> rbt_lookup (fold rbt_delete xs t) = rbt_lookup t |` (- set xs)
[PROOF STEP]
apply(induct xs rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_rbt t \<Longrightarrow> rbt_lookup (fold rbt_delete [] t) = rbt_lookup t |` (- set [])
 2. \<And>x xs. \<lbrakk>is_rbt t \<Longrightarrow> rbt_lookup (fold rbt_delete xs t) = rbt_lookup t |` (- set xs); is_rbt t\<rbrakk> \<Longrightarrow> rbt_lookup (fold rbt_delete (xs @ [x]) t) = rbt_lookup t |` (- set (xs @ [x]))
[PROOF STEP]
apply(simp_all add: rbt_lookup_rbt_delete ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>rbt_lookup (fold rbt_delete xs t) = rbt_lookup t |` (- set xs); is_rbt t\<rbrakk> \<Longrightarrow> rbt_lookup t |` (- set xs \<inter> - {x}) = rbt_lookup t |` (- insert x (set xs))
[PROOF STEP]
apply(metis Un_insert_right compl_sup sup_bot_right)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_rbt_fold_rbt_insert: "is_rbt t \<Longrightarrow> is_rbt (fold (\<lambda>k. rbt_insert k (f k)) xs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> is_rbt (fold (\<lambda>k. rbt_insert k (f k)) xs t)
[PROOF STEP]
by(induct xs rule: rev_induct) simp_all


[STATEMENT]
lemma rbt_lookup_fold_rbt_insert:
  "is_rbt t \<Longrightarrow>
  rbt_lookup (fold (\<lambda>k. rbt_insert k (f k)) xs t) =
  rbt_lookup t ++ map_of (map (\<lambda>k. (k, f k)) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> rbt_lookup (fold (\<lambda>k. rbt_insert k (f k)) xs t) = rbt_lookup t ++ map_of (map (\<lambda>k. (k, f k)) xs)
[PROOF STEP]
by(induct xs arbitrary: t)(auto simp add: rbt_lookup_rbt_insert map_add_def fun_eq_iff map_of_map_Pair_key split: option.splits)


[STATEMENT]
lemma fold_rev_simps [simp, code]:
  "fold_rev f RBT_Impl.Empty = id"
  "fold_rev f (Branch c l k v r) = fold_rev f l o f k v o fold_rev f r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_rev f rbt.Empty = id &&& fold_rev f (Branch c l k v r) = fold_rev f l \<circ> f k v \<circ> fold_rev f r
[PROOF STEP]
by(simp_all add: fold_rev_def fun_eq_iff)


[STATEMENT]
lemma sorted_fst_foldr_Cons:
  "sorted (map f as) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map f as) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
[PROOF STEP]
proof(induct as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sorted (map f []) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) [] []))
 2. \<And>a as. \<lbrakk>sorted (map f as) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as [])); sorted (map f (a # as))\<rbrakk> \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
sorted (map f as) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
sorted (map f (a # as))

goal (2 subgoals):
 1. sorted (map f []) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) [] []))
 2. \<And>a as. \<lbrakk>sorted (map f as) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as [])); sorted (map f (a # as))\<rbrakk> \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))
[PROOF STEP]
with set_foldr_Cons[of P as]
[PROOF STATE]
proof (chain)
picking this:
set (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []) \<subseteq> set as
sorted (map f as) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
sorted (map f (a # as))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []) \<subseteq> set as
sorted (map f as) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) as []))
sorted (map f (a # as))

goal (1 subgoal):
 1. sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) (a # as) []))

goal (1 subgoal):
 1. sorted (map f []) \<Longrightarrow> sorted (map f (foldr (\<lambda>x xs. if P x xs then x # xs else xs) [] []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma member_empty [simp]:
  "member empty = (\<lambda>_. False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member RBT_Set2.empty = (\<lambda>_. False)
[PROOF STEP]
by(simp add: member_def empty_def Mapping_RBT_inverse ord.Empty_is_rbt ord.rbt_lookup.simps fun_eq_iff)


[STATEMENT]
lemma fold_conv_fold_keys: "RBT_Set2.fold f rbt b = List.fold f (RBT_Set2.keys rbt) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RBT_Set2.fold f rbt b = List.fold f (keys rbt) b
[PROOF STEP]
by(simp add: RBT_Set2.fold_def RBT_Set2.keys_def RBT_Impl.fold_def RBT_Impl.keys_def fold_map o_def split_def)


[STATEMENT]
lemma fold_conv_fold_keys':
  "fold f t = List.fold f (RBT_Impl.keys (RBT_Mapping2.impl_of t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RBT_Set2.fold f t = List.fold f (RBT_Impl.keys (mapping_rbt.impl_of t))
[PROOF STEP]
by(simp add: fold.rep_eq RBT_Impl.fold_def RBT_Impl.keys_def fold_map o_def split_def)


[STATEMENT]
lemma member_lookup [code]: "member t x \<longleftrightarrow> RBT_Mapping2.lookup t x = Some ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member t x = (RBT_Mapping2.lookup t x = Some ())
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma unfoldr_rbt_keys_generator:
  "list.unfoldr rbt_keys_generator (init t) = keys t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.unfoldr rbt_keys_generator (init t) = keys t
[PROOF STEP]
by transfer(simp add: unfoldr_rbt_keys_generator)


[STATEMENT]
lemma keys_eq_Nil_iff [simp]: "keys rbt = [] \<longleftrightarrow> rbt = empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (keys rbt = []) = (rbt = RBT_Set2.empty)
[PROOF STEP]
by transfer(case_tac rbt, simp_all)


[STATEMENT]
lemma fold1_conv_fold: "fold1 f rbt = List.fold f (tl (keys rbt)) (hd (keys rbt))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold1 f rbt = List.fold f (tl (keys rbt)) (hd (keys rbt))
[PROOF STEP]
by transfer(simp add: RBT_Impl_fold1_def)


[STATEMENT]
lemma set_linorder: "class.linorder (cless_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool) cless"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
using ID_ccompare_neq_None
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
by(clarsimp)(rule ID_ccompare)


[STATEMENT]
lemma ccomp_comparator: "comparator (ccomp :: 'a comparator)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comparator ccomp
[PROOF STEP]
using ID_ccompare_neq_None
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. comparator ccomp
[PROOF STEP]
by(clarsimp)(rule ID_ccompare')


[STATEMENT]
lemma is_rbt_impl_of [simp, intro]:
  fixes t :: "'a set_rbt"
  shows "ord.is_rbt cless (RBT_Mapping2.impl_of t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord.is_rbt cless (mapping_rbt.impl_of t)
[PROOF STEP]
using ID_ccompare_neq_None impl_of [of t]
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None
mapping_rbt.impl_of t \<in> {t. ord.is_rbt cless t \<or> ID ccompare = None}

goal (1 subgoal):
 1. ord.is_rbt cless (mapping_rbt.impl_of t)
[PROOF STEP]
by auto


[STATEMENT]
lemma member_RBT:
  "ord.is_rbt cless t \<Longrightarrow> member (Set_RBT t) (x :: 'a) \<longleftrightarrow> ord.rbt_lookup cless t x = Some ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord.is_rbt cless t \<Longrightarrow> member (Mapping_RBT t) x = (ord.rbt_lookup cless t x = Some ())
[PROOF STEP]
by(auto simp add: member_def Mapping_RBT_inverse rbt_comps)


[STATEMENT]
lemma member_impl_of:
  "ord.rbt_lookup cless (RBT_Mapping2.impl_of t) (x :: 'a) = Some () \<longleftrightarrow> member t x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ord.rbt_lookup cless (mapping_rbt.impl_of t) x = Some ()) = member t x
[PROOF STEP]
by transfer (auto simp: rbt_comps)


[STATEMENT]
lemma member_insert [simp]:
  "member (insert x (t :: 'a set_rbt)) = (member t)(x := True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (RBT_Set2.insert x t) = (member t)(x := True)
[PROOF STEP]
by transfer (simp add: fun_eq_iff linorder.rbt_lookup_rbt_insert[OF set_linorder] ID_ccompare_neq_None)


[STATEMENT]
lemma member_fold_insert [simp]:
  "member (List.fold insert xs (t :: 'a set_rbt)) = (\<lambda>x. member t x \<or> x \<in> set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (List.fold RBT_Set2.insert xs t) = (\<lambda>x. member t x \<or> x \<in> set xs)
[PROOF STEP]
by(induct xs arbitrary: t) auto


[STATEMENT]
lemma member_remove [simp]:
  "member (remove (x :: 'a) t) = (member t)(x := False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (remove x t) = (member t)(x := False)
[PROOF STEP]
by transfer (simp add: linorder.rbt_lookup_rbt_delete[OF set_linorder] ID_ccompare_neq_None fun_eq_iff)


[STATEMENT]
lemma member_conv_keys: "member t = (\<lambda>x :: 'a. x \<in> set (keys t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member t = (\<lambda>x. x \<in> set (keys t))
[PROOF STEP]
by(transfer)(simp add: ID_ccompare_neq_None linorder.rbt_lookup_keys[OF set_linorder] ord.is_rbt_rbt_sorted)


[STATEMENT]
lemma is_empty_empty [simp]:
  "is_empty t \<longleftrightarrow> t = empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RBT_Set2.is_empty t = (t = RBT_Set2.empty)
[PROOF STEP]
by transfer (simp split: rbt.split)


[STATEMENT]
lemma RBT_lookup_empty [simp]:
  "ord.rbt_lookup cless (t :: ('a, unit) rbt) = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ord.rbt_lookup cless t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ord.rbt_lookup cless t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
interpret linorder "cless_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool" cless
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
by(rule set_linorder)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (local.rbt_lookup t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.rbt_lookup t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
by(cases t)(auto simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(local.rbt_lookup t = Map.empty) = (t = rbt.Empty)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma member_empty_empty [simp]:
  "member t = (\<lambda>_. False) \<longleftrightarrow> (t :: 'a set_rbt) = empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (member t = (\<lambda>_. False)) = (t = RBT_Set2.empty)
[PROOF STEP]
by transfer(simp add: ID_ccompare_neq_None fun_eq_iff RBT_lookup_empty[symmetric])


[STATEMENT]
lemma member_union [simp]:
  "member (union (t1 :: 'a set_rbt) t2) = (\<lambda>x. member t1 x \<or> member t2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (RBT_Set2.union t1 t2) = (\<lambda>x. member t1 x \<or> member t2 x)
[PROOF STEP]
by(auto simp add: member_lookup fun_eq_iff lookup_join[OF ID_ccompare_neq_None] split: option.split)


[STATEMENT]
lemma member_minus [simp]:
  "member (minus (t1 :: 'a set_rbt) t2) = (\<lambda>x. member t1 x \<and> \<not> member t2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (RBT_Set2.minus t1 t2) = (\<lambda>x. member t1 x \<and> \<not> member t2 x)
[PROOF STEP]
by(transfer)(auto simp add: ID_ccompare_neq_None fun_eq_iff rbt_comps linorder.rbt_lookup_rbt_minus[OF set_linorder] ord.is_rbt_rbt_sorted)


[STATEMENT]
lemma member_inter [simp]:
  "member (inter (t1 :: 'a set_rbt) t2) = (\<lambda>x. member t1 x \<and> member t2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (RBT_Set2.inter t1 t2) = (\<lambda>x. member t1 x \<and> member t2 x)
[PROOF STEP]
by(auto simp add: member_lookup fun_eq_iff lookup_meet[OF ID_ccompare_neq_None] split: option.split)


[STATEMENT]
lemma member_inter_list [simp]:
  "member (inter_list (t :: 'a set_rbt) xs) = (\<lambda>x. member t x \<and> x \<in> set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (inter_list t xs) = (\<lambda>x. member t x \<and> x \<in> set xs)
[PROOF STEP]
by transfer(auto simp add: ID_ccompare_neq_None fun_eq_iff linorder.rbt_lookup_fold_rbt_insert[OF set_linorder] ord.Empty_is_rbt map_of_map_Pair_key ord.rbt_lookup.simps rel_option_iff split: if_split_asm option.split_asm)


[STATEMENT]
lemma member_filter [simp]:
  "member (filter P (t :: 'a set_rbt)) = (\<lambda>x. member t x \<and> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (RBT_Set2.filter P t) = (\<lambda>x. member t x \<and> P x)
[PROOF STEP]
by(simp add: member_lookup fun_eq_iff lookup_filter[OF ID_ccompare_neq_None] split: option.split)


[STATEMENT]
lemma distinct_keys [simp]:
  "distinct (keys (rbt :: 'a set_rbt))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (keys rbt)
[PROOF STEP]
by transfer(simp add: ID_ccompare_neq_None RBT_Impl.keys_def ord.is_rbt_rbt_sorted linorder.distinct_entries[OF set_linorder])


[STATEMENT]
lemma all_conv_all_member:
  "all P t \<longleftrightarrow> (\<forall>x :: 'a. member t x \<longrightarrow> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all P t = (\<forall>x. member t x \<longrightarrow> P x)
[PROOF STEP]
by(simp add: member_lookup all_conv_all_lookup[OF ID_ccompare_neq_None])


[STATEMENT]
lemma ex_conv_ex_member:
  "ex P t \<longleftrightarrow> (\<exists>x :: 'a. member t x \<and> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ex P t = (\<exists>x. member t x \<and> P x)
[PROOF STEP]
by(simp add: member_lookup ex_conv_ex_lookup[OF ID_ccompare_neq_None])


[STATEMENT]
lemma finite_member: "finite (Collect (RBT_Set2.member (t :: 'a set_rbt)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Collect (member t))
[PROOF STEP]
by transfer (simp add: rbt_comps linorder.finite_dom_rbt_lookup[OF set_linorder])


[STATEMENT]
lemma member_Id_on: "member (Id_on t) = (\<lambda>(k :: 'a, k'). k = k' \<and> member t k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (RBT_Set2.Id_on t) = (\<lambda>(k, k'). k = k' \<and> member t k)
[PROOF STEP]
by(simp add: member_lookup[abs_def] diag_lookup[OF ID_ccompare_neq_None] fun_eq_iff)


[STATEMENT]
lemma set_linorder': "class.linorder (cless_eq :: 'b \<Rightarrow> 'b \<Rightarrow> bool) cless"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
using ID_ccompare_neq_None'
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
by(clarsimp)(rule ID_ccompare)


[STATEMENT]
lemma member_product:
  "member (product rbt1 rbt2) = (\<lambda>ab :: 'a \<times> 'b. ab \<in> Collect (member rbt1) \<times> Collect (member rbt2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (product rbt1 rbt2) = (\<lambda>ab. ab \<in> Collect (member rbt1) \<times> Collect (member rbt2))
[PROOF STEP]
by(auto simp add: fun_eq_iff member_lookup product_def RBT_Mapping2.lookup_product ID_ccompare_neq_None ID_ccompare_neq_None' split: option.splits)


[STATEMENT]
lemma sorted_RBT_Set_keys:
  "ID CCOMPARE('a :: ccompare) = Some c
  \<Longrightarrow> linorder.sorted (le_of_comp c) (RBT_Set2.keys rbt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ID ccompare = Some c \<Longrightarrow> sorted_wrt (le_of_comp c) (keys rbt)
[PROOF STEP]
by transfer(auto simp add: RBT_Set2.keys.rep_eq RBT_Impl.keys_def linorder.rbt_sorted_entries[OF ID_ccompare] ord.is_rbt_rbt_sorted)


[STATEMENT]
lemma set_linorder2: "class.linorder (cless_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool) cless"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
using ID_ccompare_neq_None
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
by(clarsimp)(rule ID_ccompare)


[STATEMENT]
lemma set_keys_Mapping_RBT: "set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
proof(cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = rbt.Empty \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
 2. \<And>x21 x22 x23 x24 x25. t = Branch x21 x22 x23 x24 x25 \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
case Empty
[PROOF STATE]
proof (state)
this:
t = rbt.Empty

goal (2 subgoals):
 1. t = rbt.Empty \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
 2. \<And>x21 x22 x23 x24 x25. t = Branch x21 x22 x23 x24 x25 \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = rbt.Empty

goal (1 subgoal):
 1. set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
by(clarsimp simp add: Mapping_RBT_def keys.rep_eq is_ccompare_def Mapping_RBT'_inverse ord.is_rbt_def ord.rbt_sorted.simps)
[PROOF STATE]
proof (state)
this:
set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)

goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. t = Branch x21 x22 x23 x24 x25 \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. t = Branch x21 x22 x23 x24 x25 \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
case (Branch c l k v r)
[PROOF STATE]
proof (state)
this:
t = Branch c l k v r

goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. t = Branch x21 x22 x23 x24 x25 \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
proof(cases "is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r) \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
 2. \<not> (is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r)) \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r))

goal (2 subgoals):
 1. is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r) \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
 2. \<not> (is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r)) \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r))

goal (1 subgoal):
 1. set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
using Branch
[PROOF STATE]
proof (prove)
using this:
\<not> (is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r))
t = Branch c l k v r

goal (1 subgoal):
 1. set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
by(auto simp add: Mapping_RBT_def keys.rep_eq is_ccompare_def Mapping_RBT'_inverse simp del: not_None_eq)
[PROOF STATE]
proof (state)
this:
set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)

goal (1 subgoal):
 1. is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r) \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r) \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r)

goal (1 subgoal):
 1. is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r) \<Longrightarrow> set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r)

goal (1 subgoal):
 1. set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
using Branch
[PROOF STATE]
proof (prove)
using this:
is_ccompare TYPE('a) \<and> \<not> ord.is_rbt cless (Branch c l k v r)
t = Branch c l k v r

goal (1 subgoal):
 1. set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)
[PROOF STEP]
by(clarsimp simp add: Mapping_RBT_def keys.rep_eq is_ccompare_def Mapping_RBT'_inverse RBT_ext.linorder.is_rbt_fold_rbt_insert_impl[OF ID_ccompare] linorder.rbt_insert_is_rbt[OF ID_ccompare] ord.Empty_is_rbt)(subst linorder.rbt_lookup_keys[OF ID_ccompare, symmetric], assumption, auto simp add: linorder.rbt_sorted_fold_insert[OF ID_ccompare] RBT_ext.linorder.rbt_lookup_fold_rbt_insert_impl[OF ID_ccompare] RBT_ext.linorder.rbt_lookup_rbt_insert'[OF ID_ccompare] linorder.rbt_insert_rbt_sorted[OF ID_ccompare] ord.is_rbt_rbt_sorted ord.Empty_is_rbt dom_map_of_conv_image_fst RBT_Impl.keys_def ord.rbt_lookup.simps)
[PROOF STATE]
proof (state)
this:
set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (keys (Mapping_RBT t)) = set (RBT_Impl.keys t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fin: "finite X" if "X \<subseteq> {n. real n \<le> x}" for X x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X
[PROOF STEP]
by (rule finite_subset[of _ "{..nat \<lfloor>x\<rfloor>}"]) (use that in \<open>auto simp: le_nat_iff le_floor_iff\<close>)


[STATEMENT]
lemma S_mono: "S x \<le> S y" if "x \<le> y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S x \<le> S y
[PROOF STEP]
unfolding S_def sum_upto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum a {i. 0 < i \<and> real i \<le> x} \<le> sum a {i. 0 < i \<and> real i \<le> y}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. sum a {i. 0 < i \<and> real i \<le> x} \<le> sum a {i. 0 < i \<and> real i \<le> y}
[PROOF STEP]
by (intro sum_mono2 fin[of _ y] a_nonneg) auto


[STATEMENT]
lemma split:
  fixes f :: "nat \<Rightarrow> real"
  assumes "\<alpha> \<in> {0..1}"
  shows   "sum_upto f x = sum_upto f (\<alpha>*x) + (\<Sum>n | n > 0 \<and> real n \<in> {\<alpha>*x<..x}. f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
proof (cases "x > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
 2. \<not> 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < x

goal (2 subgoals):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
 2. \<not> 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
hence *: "{n. n > 0 \<and> real n \<le> x} = {}" "{n. n > 0 \<and> real n \<in> {\<alpha>*x<..x}} = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < x

goal (1 subgoal):
 1. {n. 0 < n \<and> real n \<le> x} = {} &&& {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}} = {}
[PROOF STEP]
using mult_right_mono[of \<alpha> 1 x] assms
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < x
\<lbrakk>\<alpha> \<le> 1; 0 \<le> x\<rbrakk> \<Longrightarrow> \<alpha> * x \<le> 1 * x
\<alpha> \<in> {0..1}

goal (1 subgoal):
 1. {n. 0 < n \<and> real n \<le> x} = {} &&& {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. 0 < n \<and> real n \<le> x} = {}
{n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}} = {}

goal (2 subgoals):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
 2. \<not> 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
have "\<alpha> * x \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> * x \<le> 0
[PROOF STEP]
using False assms
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < x
\<alpha> \<in> {0..1}

goal (1 subgoal):
 1. \<alpha> * x \<le> 0
[PROOF STEP]
by (intro mult_nonneg_nonpos) auto
[PROOF STATE]
proof (state)
this:
\<alpha> * x \<le> 0

goal (2 subgoals):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
 2. \<not> 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
hence **: "{n. n > 0 \<and> real n \<le> \<alpha> * x} = {}"
[PROOF STATE]
proof (prove)
using this:
\<alpha> * x \<le> 0

goal (1 subgoal):
 1. {n. 0 < n \<and> real n \<le> \<alpha> * x} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. 0 < n \<and> real n \<le> \<alpha> * x} = {}

goal (2 subgoals):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
 2. \<not> 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
unfolding sum_upto_def * **
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {} = sum f {} + sum f {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
have "sum_upto f x = (\<Sum>n | n > 0 \<and> real n \<le> x. f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto f x = (\<Sum>n | 0 < n \<and> real n \<le> x. f n)
[PROOF STEP]
by (simp add: sum_upto_def)
[PROOF STATE]
proof (state)
this:
sum_upto f x = (\<Sum>n | 0 < n \<and> real n \<le> x. f n)

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_upto f x = (\<Sum>n | 0 < n \<and> real n \<le> x. f n)

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
have "{n. n > 0 \<and> real n \<le> x} =
                {n. n > 0 \<and> real n \<le> \<alpha>*x} \<union> {n. n > 0 \<and> real n \<in> {\<alpha>*x<..x}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {n. 0 < n \<and> real n \<le> x} = {n. 0 < n \<and> real n \<le> \<alpha> * x} \<union> {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}}
[PROOF STEP]
using assms True mult_right_mono[of \<alpha> 1 x]
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> {0..1}
0 < x
\<lbrakk>\<alpha> \<le> 1; 0 \<le> x\<rbrakk> \<Longrightarrow> \<alpha> * x \<le> 1 * x

goal (1 subgoal):
 1. {n. 0 < n \<and> real n \<le> x} = {n. 0 < n \<and> real n \<le> \<alpha> * x} \<union> {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}}
[PROOF STEP]
by (force intro: order_trans)
[PROOF STATE]
proof (state)
this:
{n. 0 < n \<and> real n \<le> x} = {n. 0 < n \<and> real n \<le> \<alpha> * x} \<union> {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}}

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{n. 0 < n \<and> real n \<le> x} = {n. 0 < n \<and> real n \<le> \<alpha> * x} \<union> {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}}

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
have "(\<Sum>n\<in>\<dots>. f n) = sum_upto f (\<alpha>*x) + (\<Sum>n | n > 0 \<and> real n \<in> {\<alpha>*x<..x}. f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f ({n. 0 < n \<and> real n \<le> \<alpha> * x} \<union> {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}}) = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
by (subst sum.union_disjoint) (auto intro: fin simp: sum_upto_def)
[PROOF STATE]
proof (state)
this:
sum f ({n. 0 < n \<and> real n \<le> \<alpha> * x} \<union> {n. 0 < n \<and> real n \<in> {\<alpha> * x<..x}}) = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)

goal (1 subgoal):
 1. sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum_upto f x = sum_upto f (\<alpha> * x) + (\<Sum>n | 0 < n \<and> real n \<in> {\<alpha> * x<..x}. f n)

goal:
No subgoals!
[PROOF STEP]
qed