[STATEMENT]
lemma smooth_on_Taylor2E:
  fixes f::"'a::euclidean_space \<Rightarrow> real"
  assumes hd: "\<infinity>-smooth_on UNIV f"
  obtains g where "\<And>Y.
    f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. ((Y - X) \<bullet> j) * ((Y - X) \<bullet> i) * g i j Y))"
    "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> \<infinity>-smooth_on UNIV (g i j)"
    \<comment>\<open>TODO: generalize\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define S::"'a set" where "S = UNIV"
[PROOF STATE]
proof (state)
this:
S = UNIV

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "open S" and "convex S" "X \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open S &&& convex S &&& X \<in> S
[PROOF STEP]
by (auto simp: S_def)
[PROOF STATE]
proof (state)
this:
open S
convex S
X \<in> S

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have hd: "\<infinity>-smooth_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smooth_on S f
[PROOF STEP]
using hd
[PROOF STATE]
proof (prove)
using this:
smooth_on UNIV f

goal (1 subgoal):
 1. smooth_on S f
[PROOF STEP]
by (auto simp: S_def)
[PROOF STATE]
proof (state)
this:
smooth_on S f

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define i where "i H x = ((1 - x)) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H" for x H
[PROOF STATE]
proof (state)
this:
i ?H ?x = (1 - ?x) *\<^sub>R nth_derivative 2 f (X + ?x *\<^sub>R ?H) ?H

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define d2 where "d2 v v' = (\<lambda>x. frechet_derivative (\<lambda>x. frechet_derivative f (at x) v') (at x) v)" for v v'
[PROOF STATE]
proof (state)
this:
d2 ?v ?v' = (\<lambda>x. frechet_derivative (\<lambda>x. frechet_derivative f (at x) ?v') (at x) ?v)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define g where "g H x i j = d2 i j (X + x *\<^sub>R H)" for i j x H
[PROOF STATE]
proof (state)
this:
g ?H ?x ?i ?j = d2 ?i ?j (X + ?x *\<^sub>R ?H)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define g' where  "g' i j H = integral {0 .. 1} (\<lambda>x. (1 - x) * g H x i j)" for i j H
[PROOF STATE]
proof (state)
this:
g' ?i ?j ?H = integral {0..1} (\<lambda>x. (1 - x) * g ?H x ?i ?j)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "higher_differentiable_on S f 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f 2
[PROOF STEP]
using hd(1)
[PROOF STATE]
proof (prove)
using this:
smooth_on S f

goal (1 subgoal):
 1. higher_differentiable_on S f 2
[PROOF STEP]
by (auto simp: smooth_on_def dest!: spec[where x=2])
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 2

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note hd2 = this \<open>open S\<close>
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 2
open S

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have d2_cont: "continuous_on S (d2 i j)" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S (d2 i j)
[PROOF STEP]
using hd2(1)
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 2

goal (1 subgoal):
 1. continuous_on S (d2 i j)
[PROOF STEP]
by (auto simp: g_def numeral_2_eq_2 higher_differentiable_on.simps d2_def)
[PROOF STATE]
proof (state)
this:
continuous_on S (d2 ?i ?j)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note [continuous_intros] = continuous_on_compose2[OF d2_cont]
[PROOF STATE]
proof (state)
this:
\<lbrakk>continuous_on ?s ?f; ?f ` ?s \<subseteq> S\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. d2 ?i1 ?j1 (?f x))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have hdiff2: "\<infinity>-smooth_on S (d2 v v')" for v v'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smooth_on S (d2 v v')
[PROOF STEP]
apply (auto simp: d2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smooth_on S (\<lambda>x. frechet_derivative (\<lambda>x. frechet_derivative f (at x) v') (at x) v)
[PROOF STEP]
apply (rule smooth_on_frechet_derivivative_comp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. smooth_on UNIV (\<lambda>x. frechet_derivative f (at x) v')
 2. smooth_on ?S (\<lambda>x. x)
 3. open S
 4. open UNIV
 5. (\<lambda>x. x) ` S \<subseteq> UNIV
 6. S \<subseteq> ?S
[PROOF STEP]
apply (rule smooth_on_frechet_derivivative_comp)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. smooth_on UNIV f
 2. smooth_on ?S7 (\<lambda>x. x)
 3. open UNIV
 4. open UNIV
 5. range (\<lambda>x. x) \<subseteq> UNIV
 6. UNIV \<subseteq> ?S7
 7. smooth_on ?S (\<lambda>x. x)
 8. open S
 9. open UNIV
 10. (\<lambda>x. x) ` S \<subseteq> UNIV
A total of 11 subgoals...
[PROOF STEP]
by (auto simp: S_def assms)
[PROOF STATE]
proof (state)
this:
smooth_on S (d2 ?v ?v')

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
smooth_on S (d2 ?v ?v')

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume "Y \<in> S"
[PROOF STATE]
proof (state)
this:
Y \<in> S

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define H where "H = Y - X"
[PROOF STATE]
proof (state)
this:
H = Y - X

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>Y \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
Y \<in> S
[PROOF STEP]
have "X + H \<in> S"
[PROOF STATE]
proof (prove)
using this:
Y \<in> S

goal (1 subgoal):
 1. X + H \<in> S
[PROOF STEP]
by (simp add: H_def)
[PROOF STATE]
proof (state)
this:
X + H \<in> S

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>X \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
X \<in> S
X + H \<in> S
[PROOF STEP]
have cs: "closed_segment X (X + H) \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
X \<in> S
X + H \<in> S

goal (1 subgoal):
 1. closed_segment X (X + H) \<subseteq> S
[PROOF STEP]
using \<open>convex S\<close>
[PROOF STATE]
proof (prove)
using this:
X \<in> S
X + H \<in> S
convex S

goal (1 subgoal):
 1. closed_segment X (X + H) \<subseteq> S
[PROOF STEP]
by (rule closed_segment_subset)
[PROOF STATE]
proof (state)
this:
closed_segment X (X + H) \<subseteq> S

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have i: "(i H has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1}"
      "f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (i H)"
      "i H integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i H has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1} &&& f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (i H) &&& i H integrable_on {0..1}
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1} &&& f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) &&& (\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) integrable_on {0..1}
[PROOF STEP]
using higher_differentiable_Taylor1[OF hd2 cs]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1}
f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H)
(\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) integrable_on {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1} &&& f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) &&& (\<lambda>x. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H) integrable_on {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i H has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1}
f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (i H)
i H integrable_on {0..1}

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note i(2)
[PROOF STATE]
proof (state)
this:
f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (i H)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (i H)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have integrable: "(\<lambda>x. \<Sum>n\<in>Basis. (1 - x) * (g H x a n * (H \<bullet> n) * (H \<bullet> a))) integrable_on {0..1}"
      "(\<lambda>x. (1 - x) * (g H x n a * (H \<bullet> a) * (H \<bullet> n))) integrable_on {0..1}"
      for a n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n\<in>Basis. (1 - x) * (g H x a n * (H \<bullet> n) * (H \<bullet> a))) integrable_on {0..1} &&& (\<lambda>x. (1 - x) * (g H x n a * (H \<bullet> a) * (H \<bullet> n))) integrable_on {0..1}
[PROOF STEP]
by (auto intro!: integrable_continuous_interval continuous_intros closed_segment_subsetD
          cs simp: g_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>n\<in>Basis. (1 - x) * (g H x ?a n * (H \<bullet> n) * (H \<bullet> ?a))) integrable_on {0..1}
(\<lambda>x. (1 - x) * (g H x ?n ?a * (H \<bullet> ?a) * (H \<bullet> ?n))) integrable_on {0..1}

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have i_eq: "i H x = (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))"
      if "0 \<le> x" "x \<le> 1"
      for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i H x = (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - x) *\<^sub>R nth_derivative 2 f (X + x *\<^sub>R H) H = (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))
[PROOF STEP]
apply (subst second_derivative_componentwise[OF hd2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. X + x *\<^sub>R H \<in> S
 2. (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at (X + x *\<^sub>R H)) i * (H \<bullet> j)) * (H \<bullet> i)) = (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))
[PROOF STEP]
apply (rule closed_segment_subsetD, rule cs, rule that, rule that)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at (X + x *\<^sub>R H)) i * (H \<bullet> j)) * (H \<bullet> i)) = (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))
[PROOF STEP]
by (simp add: g_def d2_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?x; ?x \<le> 1\<rbrakk> \<Longrightarrow> i H ?x = (1 - ?x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H ?x i j * (H \<bullet> j)) * (H \<bullet> i))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "integral {0 .. 1} (i H) = integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (i H) = integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i)))
[PROOF STEP]
apply (subst integral_spike[OF negligible_empty])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {0..1} - {} \<Longrightarrow> ?g x = i H x
 2. integral {0..1} ?g = integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i)))
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {0..1} - {} \<Longrightarrow> i H x = ?g x
 2. integral {0..1} ?g = integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i)))
[PROOF STEP]
apply (rule i_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> {0..1} - {} \<Longrightarrow> 0 \<le> x
 2. \<And>x. x \<in> {0..1} - {} \<Longrightarrow> x \<le> 1
 3. integral {0..1} (\<lambda>x. (1 - x) *\<^sub>R (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))) = integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i)))
[PROOF STEP]
by (auto simp: that)
[PROOF STATE]
proof (state)
this:
integral {0..1} (i H) = integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i)))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {0..1} (i H) = integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i)))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. (H \<bullet> j) * (H \<bullet> i) * g' i j H))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))) = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * g' i j H)
[PROOF STEP]
apply (simp add: sum_distrib_left sum_distrib_right integral_sum integrable g'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n\<in>Basis. \<Sum>na\<in>Basis. integral {0..1} (\<lambda>x. (1 - x) * (g H x n na * (H \<bullet> na) * (H \<bullet> n)))) = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * integral {0..1} (\<lambda>x. (1 - x) * g H x i j))
[PROOF STEP]
apply (simp add: integral_mult_right[symmetric] del: integral_mult_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n\<in>Basis. \<Sum>na\<in>Basis. integral {0..1} (\<lambda>x. (1 - x) * (g H x n na * (H \<bullet> na) * (H \<bullet> n)))) = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. integral {0..1} (\<lambda>x. H \<bullet> j * (H \<bullet> i) * ((1 - x) * g H x i j)))
[PROOF STEP]
by (simp only: ac_simps)
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. (1 - x) * (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. g H x i j * (H \<bullet> j)) * (H \<bullet> i))) = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * g' i j H)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (X + H) = f X + nth_derivative 1 f X H + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * g' i j H)
[PROOF STEP]
have "f (X + H) = f X + nth_derivative 1 f X H + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * g' i j H)"
[PROOF STATE]
proof (prove)
using this:
f (X + H) = f X + nth_derivative 1 f X H + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * g' i j H)

goal (1 subgoal):
 1. f (X + H) = f X + nth_derivative 1 f X H + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * g' i j H)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f (X + H) = f X + nth_derivative 1 f X H + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. H \<bullet> j * (H \<bullet> i) * g' i j H)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Y2 \<in> S \<Longrightarrow> f (X + (?Y2 - X)) = f X + nth_derivative 1 f X (?Y2 - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (?Y2 - X) \<bullet> j * ((?Y2 - X) \<bullet> i) * g' i j (?Y2 - X))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
?Y2 \<in> S \<Longrightarrow> f (X + (?Y2 - X)) = f X + nth_derivative 1 f X (?Y2 - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (?Y2 - X) \<bullet> j * ((?Y2 - X) \<bullet> i) * g' i j (?Y2 - X))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g' i j (Y - X))"
    for Y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g' i j (Y - X))
[PROOF STEP]
using *[of Y]
[PROOF STATE]
proof (prove)
using this:
Y \<in> S \<Longrightarrow> f (X + (Y - X)) = f X + nth_derivative 1 f X (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g' i j (Y - X))

goal (1 subgoal):
 1. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g' i j (Y - X))
[PROOF STEP]
by (auto simp: S_def)
[PROOF STATE]
proof (state)
this:
f ?Y = f X + frechet_derivative f (at X) (?Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (?Y - X) \<bullet> j * ((?Y - X) \<bullet> i) * g' i j (?Y - X))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ?Y = f X + frechet_derivative f (at X) (?Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (?Y - X) \<bullet> j * ((?Y - X) \<bullet> i) * g' i j (?Y - X))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define T::"real set" where "T = {- 1<..<2}"
[PROOF STATE]
proof (state)
this:
T = {- 1<..<2}

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "open T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open T
[PROOF STEP]
by (auto simp: T_def)
[PROOF STATE]
proof (state)
this:
open T

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "{0 .. 1} \<subseteq> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..1} \<subseteq> T
[PROOF STEP]
by (auto simp: T_def)
[PROOF STATE]
proof (state)
this:
{0..1} \<subseteq> T

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have T_small: "a \<in> S \<Longrightarrow> b \<in> T \<Longrightarrow> X + b *\<^sub>R (a - X) \<in> S" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> X + b *\<^sub>R (a - X) \<in> S
[PROOF STEP]
by (auto simp: S_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> S; ?b \<in> T\<rbrakk> \<Longrightarrow> X + ?b *\<^sub>R (?a - X) \<in> S

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "open (S \<times> T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (S \<times> T)
[PROOF STEP]
by (auto intro: open_Times \<open>open S\<close> \<open>open T\<close>)
[PROOF STATE]
proof (state)
this:
open (S \<times> T)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "smooth_on S (\<lambda>Y. g' i j (Y - X))" if i: "i \<in> Basis" and j: "j \<in> Basis" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smooth_on S (\<lambda>Y. g' i j (Y - X))
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. enat n \<le> \<infinity> \<longrightarrow> higher_differentiable_on S (\<lambda>Y. g' i j (Y - X)) n
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. enat n \<le> \<infinity> \<Longrightarrow> higher_differentiable_on S (\<lambda>Y. g' i j (Y - X)) n
[PROOF STEP]
apply (simp add: g'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. higher_differentiable_on S (\<lambda>Y. integral {0..1} (\<lambda>x. (1 - x) * g (Y - X) x i j)) n
[PROOF STEP]
apply (rule leibniz_rule'_higher_interval)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. convex S
 2. \<And>n. open S
 3. \<And>n. higher_differentiable_on (S \<times> {0..1}) (\<lambda>(Y, t). (1 - t) * g (Y - X) t i j) n
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. open S
 2. \<And>n. higher_differentiable_on (S \<times> {0..1}) (\<lambda>(Y, t). (1 - t) * g (Y - X) t i j) n
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. higher_differentiable_on (S \<times> {0..1}) (\<lambda>(Y, t). (1 - t) * g (Y - X) t i j) n
[PROOF STEP]
apply (rule higher_differentiable_on_subset[where T="S \<times> T"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>(Y, t). (1 - t) * g (Y - X) t i j) n
 2. \<And>n. S \<times> {0..1} \<subseteq> S \<times> T
[PROOF STEP]
apply (auto intro!: higher_differentiable_on_mult simp: split_beta')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. 1 - snd x) n
 2. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 3. open (S \<times> T)
 4. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (subst diff_conv_add_uminus)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. 1 + - snd x) n
 2. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 3. open (S \<times> T)
 4. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule higher_differentiable_on_add)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. 1) n
 2. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. - snd x) n
 3. \<And>n. open (S \<times> T)
 4. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 5. open (S \<times> T)
 6. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule higher_differentiable_on_const)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. - snd x) n
 2. \<And>n. open (S \<times> T)
 3. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 4. open (S \<times> T)
 5. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (subst scaleR_minus1_left[symmetric])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. - 1 *\<^sub>R snd x) n
 2. \<And>n. open (S \<times> T)
 3. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 4. open (S \<times> T)
 5. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule higher_differentiable_on_scaleR)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. - 1) n
 2. \<And>n. higher_differentiable_on (S \<times> T) snd n
 3. \<And>n. open (S \<times> T)
 4. \<And>n. open (S \<times> T)
 5. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 6. open (S \<times> T)
 7. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule higher_differentiable_on_const)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) snd n
 2. \<And>n. open (S \<times> T)
 3. \<And>n. open (S \<times> T)
 4. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 5. open (S \<times> T)
 6. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule higher_differentiable_on_snd_comp)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. x) n
 2. \<And>n. open (S \<times> T)
 3. \<And>n. open (S \<times> T)
 4. \<And>n. open (S \<times> T)
 5. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 6. open (S \<times> T)
 7. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule higher_differentiable_on_id)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. open (S \<times> T)
 2. \<And>n. open (S \<times> T)
 3. \<And>n. open (S \<times> T)
 4. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 5. open (S \<times> T)
 6. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n. open (S \<times> T)
 2. \<And>n. open (S \<times> T)
 3. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 4. open (S \<times> T)
 5. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. open (S \<times> T)
 2. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 3. open (S \<times> T)
 4. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. g (fst x - X) (snd x) i j) n
 2. open (S \<times> T)
 3. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (auto simp: g_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. higher_differentiable_on (S \<times> T) (\<lambda>x. d2 i j (X + snd x *\<^sub>R (fst x - X))) n
 2. open (S \<times> T)
 3. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule smooth_onD)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. (?m46 n)-smooth_on (S \<times> T) (\<lambda>x. d2 i j (X + snd x *\<^sub>R (fst x - X)))
 2. \<And>n. enat n \<le> ?m46 n
 3. open (S \<times> T)
 4. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
apply (rule smooth_on_compose2[OF hdiff2, unfolded o_def])
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>n. smooth_on (?S49 n) (\<lambda>x. X + snd x *\<^sub>R (fst x - X))
 2. \<And>n. open (S \<times> T)
 3. \<And>n. open S
 4. \<And>n. (\<lambda>x. X + snd x *\<^sub>R (fst x - X)) ` (S \<times> T) \<subseteq> S
 5. \<And>n. S \<times> T \<subseteq> ?S49 n
 6. \<And>n. enat n \<le> \<infinity>
 7. open (S \<times> T)
 8. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
using \<open>open S\<close> \<open>open T\<close>
[PROOF STATE]
proof (prove)
using this:
open S
open T

goal (8 subgoals):
 1. \<And>n. smooth_on (?S49 n) (\<lambda>x. X + snd x *\<^sub>R (fst x - X))
 2. \<And>n. open (S \<times> T)
 3. \<And>n. open S
 4. \<And>n. (\<lambda>x. X + snd x *\<^sub>R (fst x - X)) ` (S \<times> T) \<subseteq> S
 5. \<And>n. S \<times> T \<subseteq> ?S49 n
 6. \<And>n. enat n \<le> \<infinity>
 7. open (S \<times> T)
 8. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
using T_small \<open>_ \<subseteq> T\<close>
[PROOF STATE]
proof (prove)
using this:
open S
open T
\<lbrakk>?a \<in> S; ?b \<in> T\<rbrakk> \<Longrightarrow> X + ?b *\<^sub>R (?a - X) \<in> S
{0..1} \<subseteq> T

goal (8 subgoals):
 1. \<And>n. smooth_on (?S49 n) (\<lambda>x. X + snd x *\<^sub>R (fst x - X))
 2. \<And>n. open (S \<times> T)
 3. \<And>n. open S
 4. \<And>n. (\<lambda>x. X + snd x *\<^sub>R (fst x - X)) ` (S \<times> T) \<subseteq> S
 5. \<And>n. S \<times> T \<subseteq> ?S49 n
 6. \<And>n. enat n \<le> \<infinity>
 7. open (S \<times> T)
 8. \<And>a b. \<lbrakk>a \<in> S; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> b \<in> T
[PROOF STEP]
by (auto intro!: open_Times smooth_on_add smooth_on_scaleR smooth_on_snd
        smooth_on_minus smooth_on_fst)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i \<in> Basis; ?j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on S (\<lambda>Y. g' ?i ?j (Y - X))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>Y. f Y = f X + frechet_derivative f (at X) (Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (Y - X) \<bullet> j * ((Y - X) \<bullet> i) * g i j Y); \<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (g i j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f ?Y = f X + frechet_derivative f (at X) (?Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (?Y - X) \<bullet> j * ((?Y - X) \<bullet> i) * g' i j (?Y - X))
\<lbrakk>?i \<in> Basis; ?j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on S (\<lambda>Y. g' ?i ?j (Y - X))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ?Y = f X + frechet_derivative f (at X) (?Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (?Y - X) \<bullet> j * ((?Y - X) \<bullet> i) * g' i j (?Y - X))
\<lbrakk>?i \<in> Basis; ?j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on S (\<lambda>Y. g' ?i ?j (Y - X))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
using this:
f ?Y = f X + frechet_derivative f (at X) (?Y - X) + (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. (?Y - X) \<bullet> j * ((?Y - X) \<bullet> i) * g' i j (?Y - X))
\<lbrakk>?i \<in> Basis; ?j \<in> Basis\<rbrakk> \<Longrightarrow> smooth_on UNIV (\<lambda>Y. g' ?i ?j (Y - X))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smooth_on_Pair:
  "k-smooth_on S (\<lambda>x. (f x, g x))"
  if "open S" "k-smooth_on S f" "k-smooth_on S g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on S (\<lambda>x. (f x, g x))
[PROOF STEP]
proof (auto simp: smooth_on_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) n
[PROOF STEP]
assume n: "enat n \<le> k"
[PROOF STATE]
proof (state)
this:
enat n \<le> k

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) n
[PROOF STEP]
have 1: "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using that(2) n
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S f
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on S f n
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) n
[PROOF STEP]
have 2: "higher_differentiable_on S g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S g n
[PROOF STEP]
using that(3) n
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S g
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on S g n
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on S g n
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on S g n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S g n

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on S (\<lambda>x. (f x, g x)) n
[PROOF STEP]
show "higher_differentiable_on S (\<lambda>x. (f x, g x)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. (f x, g x)) n
[PROOF STEP]
by (rule higher_differentiable_on_Pair [OF that(1) 1 2])
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. (f x, g x)) n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smooth_on_Pair':
  "k-smooth_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x)))"
  if "open S" "open T" "k-smooth_on S f" "k-smooth_on T g"
  for f::"_::euclidean_space\<Rightarrow>_" and g::"_::euclidean_space\<Rightarrow>_"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x)))
[PROOF STEP]
proof (auto simp: smooth_on_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n
[PROOF STEP]
assume n: "enat n \<le> k"
[PROOF STATE]
proof (state)
this:
enat n \<le> k

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n
[PROOF STEP]
have 1: "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using that(3) n
[PROOF STATE]
proof (prove)
using this:
k-smooth_on S f
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on S f n
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n
[PROOF STEP]
have 2: "higher_differentiable_on T g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on T g n
[PROOF STEP]
using that(4) n
[PROOF STATE]
proof (prove)
using this:
k-smooth_on T g
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on T g n
[PROOF STEP]
unfolding smooth_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. enat n \<le> k \<longrightarrow> higher_differentiable_on T g n
enat n \<le> k

goal (1 subgoal):
 1. higher_differentiable_on T g n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on T g n

goal (1 subgoal):
 1. \<And>n. enat n \<le> k \<Longrightarrow> higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n
[PROOF STEP]
show "higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n
[PROOF STEP]
by (rule higher_differentiable_on_Pair'[OF that(1,2) 1 2])
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (S \<times> T) (\<lambda>x. (f (fst x), g (snd x))) n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diffeomorphism_imp_homeomorphism:
  assumes "diffeomorphism k s t p p'"
  shows  "homeomorphism s t p p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism s t p p'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
diffeomorphism k s t p p'

goal (1 subgoal):
 1. homeomorphism s t p p'
[PROOF STEP]
by (auto simp: diffeomorphism_def)


[STATEMENT]
lemma diffeomorphismD:
  assumes "diffeomorphism k S T f g"
  shows diffeomorphism_smoothD: "k-smooth_on S f" "k-smooth_on T g"
    and diffeomorphism_inverseD: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x" "\<And>y. y \<in> T \<Longrightarrow> f (g y) = y"
    and diffeomorphism_image_eq: "(f ` S = T)" "(g ` T = S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k-smooth_on S f &&& k-smooth_on T g) &&& ((\<And>x. x \<in> S \<Longrightarrow> g (f x) = x) &&& (\<And>y. y \<in> T \<Longrightarrow> f (g y) = y)) &&& f ` S = T &&& g ` T = S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
diffeomorphism k S T f g

goal (1 subgoal):
 1. (k-smooth_on S f &&& k-smooth_on T g) &&& ((\<And>x. x \<in> S \<Longrightarrow> g (f x) = x) &&& (\<And>y. y \<in> T \<Longrightarrow> f (g y) = y)) &&& f ` S = T &&& g ` T = S
[PROOF STEP]
by (auto simp: diffeomorphism_def homeomorphism_def)


[STATEMENT]
lemma diffeomorphism_compose:
  "diffeomorphism n S T f g \<Longrightarrow> diffeomorphism n T U h k \<Longrightarrow> open S \<Longrightarrow> open T \<Longrightarrow> open U \<Longrightarrow>
    diffeomorphism n S U (h \<circ> f) (g \<circ> k)"
  for f::"_\<Rightarrow>_::euclidean_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>diffeomorphism n S T f g; diffeomorphism n T U h k; open S; open T; open U\<rbrakk> \<Longrightarrow> diffeomorphism n S U (h \<circ> f) (g \<circ> k)
[PROOF STEP]
by (auto simp: diffeomorphism_def intro!: smooth_on_compose homeomorphism_compose)
    (auto simp: homeomorphism_def)


[STATEMENT]
lemma diffeomorphism_add: "diffeomorphism k UNIV UNIV (\<lambda>x. x + c) (\<lambda>x. x - c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diffeomorphism k UNIV UNIV (\<lambda>x. x + c) (\<lambda>x. x - c)
[PROOF STEP]
by (auto simp: diffeomorphism_def homeomorphism_add intro!: smooth_on_minus smooth_on_add)


[STATEMENT]
lemma diffeomorphism_scaleR: "diffeomorphism k UNIV UNIV (\<lambda>x. c *\<^sub>R x) (\<lambda>x. x /\<^sub>R c)"
  if "c \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diffeomorphism k UNIV UNIV ((*\<^sub>R) c) (\<lambda>x. x /\<^sub>R c)
[PROOF STEP]
by (auto simp: that diffeomorphism_def homeomorphism_scaleR
      intro!: smooth_on_minus smooth_on_scaleR)


[STATEMENT]
lemma vars_of_conj :
  "vars (\<lambda> \<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<subseteq> vars e1 \<union> vars e2"
(is "vars ?e \<subseteq> vars e1 \<union> vars e2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<subseteq> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
unfolding subset_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<longrightarrow> t \<in> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<Longrightarrow> t \<in> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<Longrightarrow> t \<in> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
assume "v \<in> vars ?e"
[PROOF STATE]
proof (state)
this:
v \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>)

goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<Longrightarrow> t \<in> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>)
[PROOF STEP]
obtain \<sigma> val
  where "?e (\<sigma> (v := val)) \<noteq> ?e \<sigma>"
[PROOF STATE]
proof (prove)
using this:
v \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>)

goal (1 subgoal):
 1. (\<And>\<sigma> val. (e1 (\<sigma>(v := val)) \<and> e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> \<and> e2 \<sigma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {v. \<exists>\<sigma> val. (e1 (\<sigma>(v := val)) \<and> e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> \<and> e2 \<sigma>)}

goal (1 subgoal):
 1. (\<And>\<sigma> val. (e1 (\<sigma>(v := val)) \<and> e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> \<and> e2 \<sigma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(e1 (\<sigma>(v := val)) \<and> e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> \<and> e2 \<sigma>)

goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<Longrightarrow> t \<in> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
hence "e1 (\<sigma> (v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma> (v := val)) \<noteq> e2 \<sigma>"
[PROOF STATE]
proof (prove)
using this:
(e1 (\<sigma>(v := val)) \<and> e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> \<and> e2 \<sigma>)

goal (1 subgoal):
 1. e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>

goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> \<and> e2 \<sigma>) \<Longrightarrow> t \<in> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
thus "v \<in> vars e1 \<union> vars e2"
[PROOF STATE]
proof (prove)
using this:
e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>

goal (1 subgoal):
 1. v \<in> Bexp.vars e1 \<union> Bexp.vars e2
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>

goal (1 subgoal):
 1. v \<in> {v. \<exists>\<sigma> val. e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma>} \<union> {v. \<exists>\<sigma> val. e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> Bexp.vars e1 \<union> Bexp.vars e2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_conj :
  assumes "finite E"
  assumes "\<forall> e \<in> E. finite (vars e)"
  shows   "finite (vars (conjunct E))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Bexp.vars (conjunct E))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite E
\<forall>e\<in>E. finite (Bexp.vars e)

goal (1 subgoal):
 1. finite (Bexp.vars (conjunct E))
[PROOF STEP]
proof (induct rule : finite_induct, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>e\<in>{}. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct {}))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>e\<in>F. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct F)); \<forall>e\<in>insert x F. finite (Bexp.vars e)\<rbrakk> \<Longrightarrow> finite (Bexp.vars (conjunct (insert x F)))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>{}. finite (Bexp.vars e)

goal (2 subgoals):
 1. \<forall>e\<in>{}. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct {}))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>e\<in>F. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct F)); \<forall>e\<in>insert x F. finite (Bexp.vars e)\<rbrakk> \<Longrightarrow> finite (Bexp.vars (conjunct (insert x F)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>{}. finite (Bexp.vars e)

goal (1 subgoal):
 1. finite (Bexp.vars (conjunct {}))
[PROOF STEP]
by (simp add : vars_def conjunct_def)
[PROOF STATE]
proof (state)
this:
finite (Bexp.vars (conjunct {}))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>e\<in>F. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct F)); \<forall>e\<in>insert x F. finite (Bexp.vars e)\<rbrakk> \<Longrightarrow> finite (Bexp.vars (conjunct (insert x F)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>e\<in>F. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct F)); \<forall>e\<in>insert x F. finite (Bexp.vars e)\<rbrakk> \<Longrightarrow> finite (Bexp.vars (conjunct (insert x F)))
[PROOF STEP]
case (2 e E)
[PROOF STATE]
proof (state)
this:
finite E
e \<notin> E
\<forall>e\<in>E. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct E))
\<forall>e\<in>insert e E. finite (Bexp.vars e)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>e\<in>F. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct F)); \<forall>e\<in>insert x F. finite (Bexp.vars e)\<rbrakk> \<Longrightarrow> finite (Bexp.vars (conjunct (insert x F)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite E
e \<notin> E
\<forall>e\<in>E. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct E))
\<forall>e\<in>insert e E. finite (Bexp.vars e)

goal (1 subgoal):
 1. finite (Bexp.vars (conjunct (insert e E)))
[PROOF STEP]
using vars_of_conj[of e "conjunct E"]
[PROOF STATE]
proof (prove)
using this:
finite E
e \<notin> E
\<forall>e\<in>E. finite (Bexp.vars e) \<Longrightarrow> finite (Bexp.vars (conjunct E))
\<forall>e\<in>insert e E. finite (Bexp.vars e)
Bexp.vars (\<lambda>\<sigma>. e \<sigma> \<and> conjunct E \<sigma>) \<subseteq> Bexp.vars e \<union> Bexp.vars (conjunct E)

goal (1 subgoal):
 1. finite (Bexp.vars (conjunct (insert e E)))
[PROOF STEP]
by (rule_tac rev_finite_subset, auto simp add : conjunct_def)
[PROOF STATE]
proof (state)
this:
finite (Bexp.vars (conjunct (insert e E)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_of_eq_a :
  shows  "vars (\<lambda> \<sigma>. e1 \<sigma> = e2 \<sigma>) \<subseteq> Aexp.vars e1 \<union> Aexp.vars e2"
(is "vars ?e \<subseteq> Aexp.vars e1 \<union> Aexp.vars e2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<subseteq> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
unfolding subset_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<longrightarrow> t \<in> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<Longrightarrow> t \<in> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<Longrightarrow> t \<in> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
assume "v \<in> vars ?e"
[PROOF STATE]
proof (state)
this:
v \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>)

goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<Longrightarrow> t \<in> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>)
[PROOF STEP]
obtain \<sigma> val where "?e (\<sigma> (v := val)) \<noteq> ?e \<sigma>"
[PROOF STATE]
proof (prove)
using this:
v \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>)

goal (1 subgoal):
 1. (\<And>\<sigma> val. (e1 (\<sigma>(v := val)) = e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> = e2 \<sigma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {v. \<exists>\<sigma> val. (e1 (\<sigma>(v := val)) = e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> = e2 \<sigma>)}

goal (1 subgoal):
 1. (\<And>\<sigma> val. (e1 (\<sigma>(v := val)) = e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> = e2 \<sigma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(e1 (\<sigma>(v := val)) = e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> = e2 \<sigma>)

goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<Longrightarrow> t \<in> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
hence "e1 (\<sigma> (v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma> (v := val)) \<noteq> e2 \<sigma>"
[PROOF STATE]
proof (prove)
using this:
(e1 (\<sigma>(v := val)) = e2 (\<sigma>(v := val))) \<noteq> (e1 \<sigma> = e2 \<sigma>)

goal (1 subgoal):
 1. e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>

goal (1 subgoal):
 1. \<And>t. t \<in> Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<Longrightarrow> t \<in> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
thus "v \<in> Aexp.vars e1 \<union> Aexp.vars e2"
[PROOF STATE]
proof (prove)
using this:
e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>

goal (1 subgoal):
 1. v \<in> Aexp.vars e1 \<union> Aexp.vars e2
[PROOF STEP]
unfolding Aexp.vars_def
[PROOF STATE]
proof (prove)
using this:
e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma> \<or> e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>

goal (1 subgoal):
 1. v \<in> {v. \<exists>\<sigma> val. e1 (\<sigma>(v := val)) \<noteq> e1 \<sigma>} \<union> {v. \<exists>\<sigma> val. e2 (\<sigma>(v := val)) \<noteq> e2 \<sigma>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> Aexp.vars e1 \<union> Aexp.vars e2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_vars_of_a_eq :
  assumes "finite (Aexp.vars e1)"
  assumes "finite (Aexp.vars e2)"
  shows   "finite (vars (\<lambda> \<sigma>. e1 \<sigma> = e2 \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>))
[PROOF STEP]
using assms vars_of_eq_a[of e1 e2]
[PROOF STATE]
proof (prove)
using this:
finite (Aexp.vars e1)
finite (Aexp.vars e2)
Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>) \<subseteq> Aexp.vars e1 \<union> Aexp.vars e2

goal (1 subgoal):
 1. finite (Bexp.vars (\<lambda>\<sigma>. e1 \<sigma> = e2 \<sigma>))
[PROOF STEP]
by (rule_tac rev_finite_subset, auto)


[STATEMENT]
lemma best_division_abs: "(n::int) > 0 \<Longrightarrow> \<exists> k. 2 * \<bar>a - k*n\<bar> \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
assume a: "n > 0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
define k where "k = a div n"
[PROOF STATE]
proof (state)
this:
k = a div n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
hence h: "a - k * n = a mod n"
[PROOF STATE]
proof (prove)
using this:
k = a div n

goal (1 subgoal):
 1. a - k * n = a mod n
[PROOF STEP]
by (simp add: mod_div_mult_eq algebra_simps)
[PROOF STATE]
proof (state)
this:
a - k * n = a mod n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a - k * n = a mod n

goal (1 subgoal):
 1. \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
proof (cases "2 * (a mod n) \<le> n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a - k * n = a mod n; 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
 2. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
2 * (a mod n) \<le> n

goal (2 subgoals):
 1. \<lbrakk>a - k * n = a mod n; 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
 2. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
hence "2 * \<bar>a - k*n\<bar> \<le> n"
[PROOF STATE]
proof (prove)
using this:
2 * (a mod n) \<le> n

goal (1 subgoal):
 1. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
using h pos_mod_sign a
[PROOF STATE]
proof (prove)
using this:
2 * (a mod n) \<le> n
a - k * n = a mod n
(0::?'a) < ?b \<Longrightarrow> (0::?'a) \<le> ?a mod ?b
0 < n

goal (1 subgoal):
 1. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * \<bar>a - k * n\<bar> \<le> n

goal (2 subgoals):
 1. \<lbrakk>a - k * n = a mod n; 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
 2. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * \<bar>a - k * n\<bar> \<le> n

goal (1 subgoal):
 1. \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 2 * (a mod n) \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
hence "2 * (n - a mod n) \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<not> 2 * (a mod n) \<le> n

goal (1 subgoal):
 1. 2 * (n - a mod n) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * (n - a mod n) \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
have "a - (k+1)*n = a mod n - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a - (k + 1) * n = a mod n - n
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
a - k * n = a mod n

goal (1 subgoal):
 1. a - (k + 1) * n = a mod n - n
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
a - (k + 1) * n = a mod n - n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
hence "2 * \<bar>a - (k+1)*n\<bar> \<le> n"
[PROOF STATE]
proof (prove)
using this:
a - (k + 1) * n = a mod n - n

goal (1 subgoal):
 1. 2 * \<bar>a - (k + 1) * n\<bar> \<le> n
[PROOF STEP]
using h pos_mod_bound[of n a] a False
[PROOF STATE]
proof (prove)
using this:
a - (k + 1) * n = a mod n - n
a - k * n = a mod n
0 < n \<Longrightarrow> a mod n < n
0 < n
\<not> 2 * (a mod n) \<le> n

goal (1 subgoal):
 1. 2 * \<bar>a - (k + 1) * n\<bar> \<le> n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
2 * \<bar>a - (k + 1) * n\<bar> \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * \<bar>a - (k + 1) * n\<bar> \<le> n

goal (1 subgoal):
 1. \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum2sq_int_nat_eq: "sum2sq_nat a b = sum2sq_int (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (sum2sq_nat a b) = sum2sq_int (int a, int b)
[PROOF STEP]
unfolding sum2sq_nat_def sum2sq_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (a\<^sup>2 + b\<^sup>2) = (case (int a, int b) of (a, b) \<Rightarrow> a\<^sup>2 + b\<^sup>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma is_sum2sq_int_nat_eq: "is_sum2sq_nat n = is_sum2sq_int (int n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum2sq_nat n = is_sum2sq_int (int n)
[PROOF STEP]
unfolding is_sum2sq_nat_def is_sum2sq_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>a b. n = sum2sq_nat a b) = (\<exists>a b. int n = sum2sq_int (a, b))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>a b. n = sum2sq_nat a b \<Longrightarrow> \<exists>a b. int n = sum2sq_int (a, b)
 2. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
assume "\<exists>a b. n = sum2sq_nat a b"
[PROOF STATE]
proof (state)
this:
\<exists>a b. n = sum2sq_nat a b

goal (2 subgoals):
 1. \<exists>a b. n = sum2sq_nat a b \<Longrightarrow> \<exists>a b. int n = sum2sq_int (a, b)
 2. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
thus "\<exists>a b. int n = sum2sq_int (a, b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. n = sum2sq_nat a b

goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b)
[PROOF STEP]
using sum2sq_int_nat_eq
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. n = sum2sq_nat a b
int (sum2sq_nat ?a ?b) = sum2sq_int (int ?a, int ?b)

goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>a b. int n = sum2sq_int (a, b)

goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
assume "\<exists>a b. int n = sum2sq_int (a, b)"
[PROOF STATE]
proof (state)
this:
\<exists>a b. int n = sum2sq_int (a, b)

goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. int n = sum2sq_int (a, b)
[PROOF STEP]
obtain a b where "int n = sum2sq_int (a, b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. int n = sum2sq_int (a, b)

goal (1 subgoal):
 1. (\<And>a b. int n = sum2sq_int (a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
int n = sum2sq_int (a, b)

goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
hence "int n = sum2sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>))"
[PROOF STATE]
proof (prove)
using this:
int n = sum2sq_int (a, b)

goal (1 subgoal):
 1. int n = sum2sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>))
[PROOF STEP]
unfolding sum2sq_int_def
[PROOF STATE]
proof (prove)
using this:
int n = (case (a, b) of (a, b) \<Rightarrow> a\<^sup>2 + b\<^sup>2)

goal (1 subgoal):
 1. int n = (case (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>)) of (a, b) \<Rightarrow> a\<^sup>2 + b\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int n = sum2sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>))

goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
hence "int n = int (sum2sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>))"
[PROOF STATE]
proof (prove)
using this:
int n = sum2sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>))

goal (1 subgoal):
 1. int n = int (sum2sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>))
[PROOF STEP]
using sum2sq_int_nat_eq
[PROOF STATE]
proof (prove)
using this:
int n = sum2sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>))
int (sum2sq_nat ?a ?b) = sum2sq_int (int ?a, int ?b)

goal (1 subgoal):
 1. int n = int (sum2sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
int n = int (sum2sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>))

goal (1 subgoal):
 1. \<exists>a b. int n = sum2sq_int (a, b) \<Longrightarrow> \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
thus "\<exists>a b. n = sum2sq_nat a b"
[PROOF STATE]
proof (prove)
using this:
int n = int (sum2sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>))

goal (1 subgoal):
 1. \<exists>a b. n = sum2sq_nat a b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a b. n = sum2sq_nat a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_two_squares_aux: "sum2sq_int(a, b) * sum2sq_int(c, d) = sum2sq_int(a*c - b*d, a*d + b*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum2sq_int (a, b) * sum2sq_int (c, d) = sum2sq_int (a * c - b * d, a * d + b * c)
[PROOF STEP]
unfolding power2_eq_square sum2sq_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (a, b) of (a, b) \<Rightarrow> a * a + b * b) * (case (c, d) of (a, b) \<Rightarrow> a * a + b * b) = (case (a * c - b * d, a * d + b * c) of (a, b) \<Rightarrow> a * a + b * b)
[PROOF STEP]
by (simp add: algebra_simps)


[STATEMENT]
lemma product_two_squares_int: "is_sum2sq_int m \<Longrightarrow> is_sum2sq_int n \<Longrightarrow> is_sum2sq_int (m*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_sum2sq_int m; is_sum2sq_int n\<rbrakk> \<Longrightarrow> is_sum2sq_int (m * n)
[PROOF STEP]
by (unfold is_sum2sq_int_def, auto simp only: product_two_squares_aux, blast)


[STATEMENT]
lemma product_two_squares_nat: "is_sum2sq_nat m \<Longrightarrow> is_sum2sq_nat n \<Longrightarrow> is_sum2sq_nat (m*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_sum2sq_nat m; is_sum2sq_nat n\<rbrakk> \<Longrightarrow> is_sum2sq_nat (m * n)
[PROOF STEP]
using product_two_squares_int is_sum2sq_int_nat_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_sum2sq_int ?m; is_sum2sq_int ?n\<rbrakk> \<Longrightarrow> is_sum2sq_int (?m * ?n)
is_sum2sq_nat ?n = is_sum2sq_int (int ?n)

goal (1 subgoal):
 1. \<lbrakk>is_sum2sq_nat m; is_sum2sq_nat n\<rbrakk> \<Longrightarrow> is_sum2sq_nat (m * n)
[PROOF STEP]
by simp