[STATEMENT]
lemma multivariate_Taylor_integral:
  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::banach"
    and Df::"'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b"
  assumes "n > 0"
  assumes Df_Nil: "\<And>a x. Df a 0 H = f a"
  assumes Df_Cons: "\<And>a i d. a \<in> closed_segment X (X + H) \<Longrightarrow> i < n \<Longrightarrow>
      ((\<lambda>a. Df a i H) has_derivative (Df a (Suc i))) (at a within G)"
  assumes cs: "closed_segment X (X + H) \<subseteq> G"
  defines "i \<equiv> \<lambda>x.
      ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H"
  shows multivariate_Taylor_has_integral:
    "(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}"
  and multivariate_Taylor:
    "f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i"
  and multivariate_Taylor_integrable:
    "i integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1} &&& f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i &&& i integrable_on {0..1}
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
let ?G = "closed_segment X (X + H)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
define line where "line t = X + t *\<^sub>R H" for t
[PROOF STATE]
proof (state)
this:
line ?t = X + ?t *\<^sub>R H

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
have segment_eq: "closed_segment X (X + H) = line ` {0 .. 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment X (X + H) = line ` {0..1}
[PROOF STEP]
by (auto simp: line_def closed_segment_def algebra_simps)
[PROOF STATE]
proof (state)
this:
closed_segment X (X + H) = line ` {0..1}

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
have line_deriv: "\<And>x. (line has_derivative (\<lambda>t. t *\<^sub>R H)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (line has_derivative (\<lambda>t. t *\<^sub>R H)) (at x)
[PROOF STEP]
by (auto intro!: derivative_eq_intros simp: line_def [abs_def])
[PROOF STATE]
proof (state)
this:
(line has_derivative (\<lambda>t. t *\<^sub>R H)) (at ?x)

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
define g where "g = f o line"
[PROOF STATE]
proof (state)
this:
g = f \<circ> line

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
define Dg where "Dg n t = Df (line t) n H" for n :: nat and t :: real
[PROOF STATE]
proof (state)
this:
Dg ?n ?t = Df (line ?t) ?n H

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
note \<open>n > 0\<close>
[PROOF STATE]
proof (state)
this:
0 < n

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < n

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
have Dg0: "Dg 0 = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dg 0 = g
[PROOF STEP]
by (auto simp add: Dg_def Df_Nil g_def)
[PROOF STATE]
proof (state)
this:
Dg 0 = g

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Dg 0 = g

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
have DgSuc: "(Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})"
    if "m < n" "0 \<le> t" "t \<le> 1" for m::nat and t::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
m < n
0 \<le> t
t \<le> 1
[PROOF STEP]
have [intro]: "line t \<in> ?G"
[PROOF STATE]
proof (prove)
using this:
m < n
0 \<le> t
t \<le> 1

goal (1 subgoal):
 1. line t \<in> closed_segment X (X + H)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m < n
0 \<le> t
t \<le> 1
0 < n
Df ?a 0 H = f ?a
\<lbrakk>?a \<in> closed_segment X (X + H); ?i < n\<rbrakk> \<Longrightarrow> ((\<lambda>a. Df a ?i H) has_derivative Df ?a (Suc ?i)) (at ?a within G)
closed_segment X (X + H) \<subseteq> G
i \<equiv> \<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H

goal (1 subgoal):
 1. line t \<in> closed_segment X (X + H)
[PROOF STEP]
by (auto simp: segment_eq)
[PROOF STATE]
proof (state)
this:
line t \<in> closed_segment X (X + H)

goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
note [derivative_intros] = has_derivative_in_compose[OF _ has_derivative_subset[OF Df_Cons]]
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?f has_derivative ?f') (at ?x within ?s); ?f ?x \<in> closed_segment X (X + H); ?i2 < n; ?f ` ?s \<subseteq> G\<rbrakk> \<Longrightarrow> ((\<lambda>x. Df (?f x) ?i2 H) has_derivative (\<lambda>x. Df (?f ?x) (Suc ?i2) (?f' x))) (at ?x within ?s)

goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
interpret Df: linear "(\<lambda>d. Df (line t) (Suc m) d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear (Df (line t) (Suc m))
[PROOF STEP]
by (auto intro!: has_derivative_linear derivative_intros \<open>m < n\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
note [derivative_intros] =
      has_derivative_compose[OF _ line_deriv]
[PROOF STATE]
proof (state)
this:
(?f has_derivative ?f') (at ?x within ?s) \<Longrightarrow> ((\<lambda>x. line (?f x)) has_derivative (\<lambda>x. ?f' x *\<^sub>R H)) (at ?x within ?s)

goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
using Df.scaleR \<open>m < n\<close>
[PROOF STATE]
proof (prove)
using this:
Df (line t) (Suc m) (?r *\<^sub>R ?b) = ?r *\<^sub>R Df (line t) (Suc m) ?b
m < n

goal (1 subgoal):
 1. (Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})
[PROOF STEP]
by (auto simp: Dg_def [abs_def] has_vector_derivative_def g_def segment_eq
         intro!: derivative_eq_intros subsetD[OF cs])
[PROOF STATE]
proof (state)
this:
(Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m < n; 0 \<le> ?t; ?t \<le> 1\<rbrakk> \<Longrightarrow> (Dg ?m has_vector_derivative Dg (Suc ?m) ?t) (at ?t within {0..1})

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < n
Dg 0 = g
\<lbrakk>?m < n; 0 \<le> ?t; ?t \<le> 1\<rbrakk> \<Longrightarrow> (Dg ?m has_vector_derivative Dg (Suc ?m) ?t) (at ?t within {0..1})
[PROOF STEP]
have g_Taylor: "(i has_integral g 1 - (\<Sum>i<n. ((1 - 0) ^ i / fact i) *\<^sub>R Dg i 0)) {0 .. 1}"
[PROOF STATE]
proof (prove)
using this:
0 < n
Dg 0 = g
\<lbrakk>?m < n; 0 \<le> ?t; ?t \<le> 1\<rbrakk> \<Longrightarrow> (Dg ?m has_vector_derivative Dg (Suc ?m) ?t) (at ?t within {0..1})

goal (1 subgoal):
 1. (i has_integral g 1 - (\<Sum>i<n. ((1 - 0) ^ i / fact i) *\<^sub>R Dg i 0)) {0..1}
[PROOF STEP]
unfolding i_def Dg_def [abs_def] line_def
[PROOF STATE]
proof (prove)
using this:
0 < n
(\<lambda>t. Df (X + t *\<^sub>R H) 0 H) = g
\<lbrakk>?m < n; 0 \<le> ?t; ?t \<le> 1\<rbrakk> \<Longrightarrow> ((\<lambda>t. Df (X + t *\<^sub>R H) ?m H) has_vector_derivative Df (X + ?t *\<^sub>R H) (Suc ?m) H) (at ?t within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. ((1 - x) ^ (n - 1) / fact (n - 1)) *\<^sub>R Df (X + x *\<^sub>R H) n H) has_integral g 1 - (\<Sum>i<n. ((1 - 0) ^ i / fact i) *\<^sub>R Df (X + 0 *\<^sub>R H) i H)) {0..1}
[PROOF STEP]
by (rule Taylor_has_integral) auto
[PROOF STATE]
proof (state)
this:
(i has_integral g 1 - (\<Sum>i<n. ((1 - 0) ^ i / fact i) *\<^sub>R Dg i 0)) {0..1}

goal (3 subgoals):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
 2. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 3. i integrable_on {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(i has_integral g 1 - (\<Sum>i<n. ((1 - 0) ^ i / fact i) *\<^sub>R Dg i 0)) {0..1}
[PROOF STEP]
show c: ?case
[PROOF STATE]
proof (prove)
using this:
(i has_integral g 1 - (\<Sum>i<n. ((1 - 0) ^ i / fact i) *\<^sub>R Dg i 0)) {0..1}

goal (1 subgoal):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(i has_integral g 1 - (\<Sum>i<n. ((1 - 0) ^ i / fact i) *\<^sub>R Dg i 0)) {0..1}
0 < n

goal (1 subgoal):
 1. (i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}
[PROOF STEP]
by (auto simp: g_def line_def Dg_def)
[PROOF STATE]
proof (state)
this:
(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}

goal (2 subgoals):
 1. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 2. i integrable_on {0..1}
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
 2. i integrable_on {0..1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}

goal (1 subgoal):
 1. f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i
[PROOF STEP]
by (simp add: integral_unique add.commute)
[PROOF STATE]
proof (state)
this:
f (X + H) = (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H) + integral {0..1} i

goal (1 subgoal):
 1. i integrable_on {0..1}
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. i integrable_on {0..1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i integrable_on {0..1}
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
(i has_integral f (X + H) - (\<Sum>i<n. (1 / fact i) *\<^sub>R Df X i H)) {0..1}

goal (1 subgoal):
 1. i integrable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i integrable_on {0..1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma second_derivative_componentwise:
  "nth_derivative 2 f a v =
    (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))"
  if "higher_differentiable_on S f 2" and S: "open S" "a \<in> S"
  for f::"'a::euclidean_space \<Rightarrow> real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_derivative 2 f a v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nth_derivative 2 f a v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
have diff: "(\<lambda>x. frechet_derivative f (at x) v) differentiable at a" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. frechet_derivative f (at x) v) differentiable at a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 2
open S
a \<in> S

goal (1 subgoal):
 1. (\<lambda>x. frechet_derivative f (at x) v) differentiable at a
[PROOF STEP]
by (auto simp: numeral_2_eq_2 higher_differentiable_on.simps differentiable_on_openD
        dest!: spec[where x=v])
[PROOF STATE]
proof (state)
this:
(\<lambda>x. frechet_derivative f (at x) ?v) differentiable at a

goal (1 subgoal):
 1. nth_derivative 2 f a v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
have d1: "x \<in> S \<Longrightarrow> f differentiable at x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> f differentiable at x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 2
open S
a \<in> S

goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> f differentiable at x
[PROOF STEP]
by (auto simp: numeral_2_eq_2 higher_differentiable_on.simps dest!: differentiable_on_openD)
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> f differentiable at ?x

goal (1 subgoal):
 1. nth_derivative 2 f a v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
have eq: "\<And>x. x \<in> Basis \<Longrightarrow>
         frechet_derivative
          (\<lambda>x. \<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at x) i) (at a) x =
         (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Basis \<Longrightarrow> frechet_derivative (\<lambda>x. \<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at x) i) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (subst frechet_derivative_sum)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>x \<in> Basis; i \<in> Basis\<rbrakk> \<Longrightarrow> (\<lambda>x. v \<bullet> i * frechet_derivative f (at x) i) differentiable at a
 2. \<And>x. x \<in> Basis \<Longrightarrow> (\<Sum>i\<in>Basis. frechet_derivative (\<lambda>x. v \<bullet> i * frechet_derivative f (at x) i) (at a) x) = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ \<in> Basis; i_ \<in> Basis\<rbrakk> \<Longrightarrow> (\<lambda>x. v \<bullet> i_ * frechet_derivative f (at x) i_) differentiable at a
[PROOF STEP]
by (auto intro!: differentiable_mult diff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Basis \<Longrightarrow> (\<Sum>i\<in>Basis. frechet_derivative (\<lambda>x. v \<bullet> i * frechet_derivative f (at x) i) (at a) x) = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> Basis \<Longrightarrow> Basis = Basis
 2. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> frechet_derivative (\<lambda>x. v \<bullet> xa * frechet_derivative f (at x) xa) (at a) x = frechet_derivative (\<lambda>a. frechet_derivative f (at a) xa) (at a) x * (v \<bullet> xa)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> frechet_derivative (\<lambda>x. v \<bullet> xa * frechet_derivative f (at x) xa) (at a) x = frechet_derivative (\<lambda>a. frechet_derivative f (at a) xa) (at a) x * (v \<bullet> xa)
[PROOF STEP]
apply (subst frechet_derivative_times)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> (\<lambda>x. v \<bullet> xa) differentiable at a
 2. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> (\<lambda>x. frechet_derivative f (at x) xa) differentiable at a
 3. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> v \<bullet> xa * frechet_derivative (\<lambda>x. frechet_derivative f (at x) xa) (at a) x + frechet_derivative (\<lambda>x. v \<bullet> xa) (at a) x * frechet_derivative f (at a) xa = frechet_derivative (\<lambda>a. frechet_derivative f (at a) xa) (at a) x * (v \<bullet> xa)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ \<in> Basis; xa_ \<in> Basis\<rbrakk> \<Longrightarrow> (\<lambda>x. v \<bullet> xa_) differentiable at a
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> (\<lambda>x. frechet_derivative f (at x) xa) differentiable at a
 2. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> v \<bullet> xa * frechet_derivative (\<lambda>x. frechet_derivative f (at x) xa) (at a) x + frechet_derivative (\<lambda>x. v \<bullet> xa) (at a) x * frechet_derivative f (at a) xa = frechet_derivative (\<lambda>a. frechet_derivative f (at a) xa) (at a) x * (v \<bullet> xa)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ \<in> Basis; xa_ \<in> Basis\<rbrakk> \<Longrightarrow> (\<lambda>x. frechet_derivative f (at x) xa_) differentiable at a
[PROOF STEP]
by (rule diff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> Basis\<rbrakk> \<Longrightarrow> v \<bullet> xa * frechet_derivative (\<lambda>x. frechet_derivative f (at x) xa) (at a) x + frechet_derivative (\<lambda>x. v \<bullet> xa) (at a) x * frechet_derivative f (at a) xa = frechet_derivative (\<lambda>a. frechet_derivative f (at a) xa) (at a) x * (v \<bullet> xa)
[PROOF STEP]
by (simp add: frechet_derivative_const)
[PROOF STATE]
proof (state)
this:
?x \<in> Basis \<Longrightarrow> frechet_derivative (\<lambda>x. \<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at x) i) (at a) ?x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) ?x * (v \<bullet> j))

goal (1 subgoal):
 1. nth_derivative 2 f a v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_derivative 2 f a v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
apply (simp add: numeral_2_eq_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. frechet_derivative f (at x) v) (at a) v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
apply (subst frechet_derivative_componentwise[OF diff])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative (\<lambda>x. frechet_derivative f (at x) v) (at a) i) = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))
[PROOF STEP]
apply (rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Basis = Basis
 2. \<And>x. x \<in> Basis \<Longrightarrow> v \<bullet> x * frechet_derivative (\<lambda>x. frechet_derivative f (at x) v) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j)) * (v \<bullet> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Basis \<Longrightarrow> v \<bullet> x * frechet_derivative (\<lambda>x. frechet_derivative f (at x) v) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j)) * (v \<bullet> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Basis \<Longrightarrow> v \<bullet> x = 0 \<or> frechet_derivative (\<lambda>x. frechet_derivative f (at x) v) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Basis \<Longrightarrow> frechet_derivative (\<lambda>x. frechet_derivative f (at x) v) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (rule trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> Basis \<Longrightarrow> frechet_derivative (\<lambda>x. frechet_derivative f (at x) v) (at a) x = ?s6 x
 2. \<And>x. x \<in> Basis \<Longrightarrow> ?s6 x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (rule frechet_derivative_transform_within_open_ext [OF _ S frechet_derivative_componentwise])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> Basis \<Longrightarrow> (\<lambda>x. frechet_derivative f (at x) v) differentiable at a
 2. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> S\<rbrakk> \<Longrightarrow> f differentiable at xa
 3. \<And>x. x \<in> Basis \<Longrightarrow> frechet_derivative (\<lambda>x. \<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at x) i) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (simp add: diff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> Basis; xa \<in> S\<rbrakk> \<Longrightarrow> f differentiable at xa
 2. \<And>x. x \<in> Basis \<Longrightarrow> frechet_derivative (\<lambda>x. \<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at x) i) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (rule d1, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Basis \<Longrightarrow> frechet_derivative (\<lambda>x. \<Sum>i\<in>Basis. v \<bullet> i * frechet_derivative f (at x) i) (at a) x = (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) x * (v \<bullet> j))
[PROOF STEP]
apply (simp add: eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nth_derivative 2 f a v = (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative (\<lambda>a. frechet_derivative f (at a) j) (at a) i * (v \<bullet> j)) * (v \<bullet> i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAll_sym:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs"
shows
"(\<forall> X'. X #= X' \<longrightarrow> X' #= X) \<and> (\<forall> A'. A $= A' \<longrightarrow> A' $= A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>X'. X #= X' \<longrightarrow> X' #= X) \<and> (\<forall>A'. A $= A' \<longrightarrow> A' $= A)
[PROOF STEP]
proof(induction rule: qTerm_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs x. \<forall>X'. qVar xs x #= X' \<longrightarrow> X' #= qVar xs x
 2. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> X' #= a) inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> A' $= a) binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> X' #= qOp delta inp binp
 3. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
case (Var xs x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>xs x. \<forall>X'. qVar xs x #= X' \<longrightarrow> X' #= qVar xs x
 2. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> X' #= a) inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> A' $= a) binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> X' #= qOp delta inp binp
 3. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X'. qVar xs x #= X' \<longrightarrow> X' #= qVar xs x
[PROOF STEP]
unfolding qVar_alpha_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X'. X' = qVar xs x \<longrightarrow> X' #= qVar xs x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>X'. qVar xs x #= X' \<longrightarrow> X' #= qVar xs x

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> X' #= a) inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> A' $= a) binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> X' #= qOp delta inp binp
 2. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> X' #= a) inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> A' $= a) binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> X' #= qOp delta inp binp
 2. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
case (Op delta inp binp)
[PROOF STATE]
proof (state)
this:
liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> X' #= a) inp
liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> A' $= a) binp

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> X' #= a) inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> A' $= a) binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> X' #= qOp delta inp binp
 2. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> X' #= qOp delta inp binp
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. qOp delta inp binp #= X' \<Longrightarrow> X' #= qOp delta inp binp
[PROOF STEP]
fix X'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. qOp delta inp binp #= X' \<Longrightarrow> X' #= qOp delta inp binp
[PROOF STEP]
assume "qOp delta inp binp #= X'"
[PROOF STATE]
proof (state)
this:
qOp delta inp binp #= X'

goal (1 subgoal):
 1. \<And>X'. qOp delta inp binp #= X' \<Longrightarrow> X' #= qOp delta inp binp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qOp delta inp binp #= X'
[PROOF STEP]
obtain inp' binp' where X': "X' = qOp delta inp' binp'" and
    1: "sameDom inp inp' \<and> sameDom binp binp'"
    and 2: "liftAll2 (\<lambda>Y Y'. Y #= Y') inp inp' \<and>
          liftAll2 (\<lambda>A A'. A $= A') binp binp'"
[PROOF STATE]
proof (prove)
using this:
qOp delta inp binp #= X'

goal (1 subgoal):
 1. (\<And>inp' binp'. \<lbrakk>X' = qOp delta inp' binp'; sameDom inp inp' \<and> sameDom binp binp'; liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding qOp_alpha_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>inp' binp'. X' = qOp delta inp' binp' \<and> sameDom inp inp' \<and> sameDom binp binp' \<and> liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. (\<And>inp' binp'. \<lbrakk>X' = qOp delta inp' binp'; sameDom inp inp' \<and> sameDom binp binp'; liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. \<And>X'. qOp delta inp binp #= X' \<Longrightarrow> X' #= qOp delta inp binp
[PROOF STEP]
thus "X' #= qOp delta inp binp"
[PROOF STATE]
proof (prove)
using this:
X' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. X' #= qOp delta inp binp
[PROOF STEP]
unfolding X'
[PROOF STATE]
proof (prove)
using this:
qOp delta inp' binp' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. qOp delta inp' binp' #= qOp delta inp binp
[PROOF STEP]
using Op.IH 1 2
[PROOF STATE]
proof (prove)
using this:
qOp delta inp' binp' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'
liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> X' #= a) inp
liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> A' $= a) binp
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. qOp delta inp' binp' #= qOp delta inp binp
[PROOF STEP]
by (auto simp add: fun_eq_iff option.case_eq_if
        lift_def liftAll_def sameDom_def liftAll2_def)
[PROOF STATE]
proof (state)
this:
X' #= qOp delta inp binp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>X'. qOp delta inp binp #= X' \<longrightarrow> X' #= qOp delta inp binp

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
case (Abs xs x X)
[PROOF STATE]
proof (state)
this:
(X, ?Y11) \<in> qSwapped \<Longrightarrow> \<forall>X'. ?Y11 #= X' \<longrightarrow> X' #= ?Y11
qSkel ?Y11 = qSkel X \<Longrightarrow> \<forall>X'. ?Y11 #= X' \<longrightarrow> X' #= ?Y11

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> X' #= Y\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
fix A'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
assume "qAbs xs x X $= A'"
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= A'

goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= A'
[PROOF STEP]
obtain x' y X' where
    1: "A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'" and
    "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= A'

goal (1 subgoal):
 1. (\<And>x' X' y. \<lbrakk>A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'; X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding qAbs_alphaAbs_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>x' y X'. A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. (\<And>x' X' y. \<lbrakk>A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'; X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
have "(X, X #[[y \<and> x]]_xs) \<in> qSwapped"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X, X #[[y \<and> x]]_xs) \<in> qSwapped
[PROOF STEP]
by (simp add: qSwap_qSwapped)
[PROOF STATE]
proof (state)
this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped

goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
(X, X #[[y \<and> x]]_xs) \<in> qSwapped
[PROOF STEP]
have "(X' #[[y \<and> x']]_xs) #= (X #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
using this:
A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
(X, X #[[y \<and> x]]_xs) \<in> qSwapped

goal (1 subgoal):
 1. X' #[[y \<and> x']]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
using Abs.IH
[PROOF STATE]
proof (prove)
using this:
A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
(X, X #[[y \<and> x]]_xs) \<in> qSwapped
(X, ?Y11) \<in> qSwapped \<Longrightarrow> \<forall>X'. ?Y11 #= X' \<longrightarrow> X' #= ?Y11
qSkel ?Y11 = qSkel X \<Longrightarrow> \<forall>X'. ?Y11 #= X' \<longrightarrow> X' #= ?Y11

goal (1 subgoal):
 1. X' #[[y \<and> x']]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X' #[[y \<and> x']]_xs #= X #[[y \<and> x]]_xs

goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> A' $= qAbs xs x X
[PROOF STEP]
thus "A' $= qAbs xs x X"
[PROOF STATE]
proof (prove)
using this:
X' #[[y \<and> x']]_xs #= X #[[y \<and> x]]_xs

goal (1 subgoal):
 1. A' $= qAbs xs x X
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
X' #[[y \<and> x']]_xs #= X #[[y \<and> x]]_xs
A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. A' $= qAbs xs x X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' $= qAbs xs x X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>A'. qAbs xs x X $= A' \<longrightarrow> A' $= qAbs xs x X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_vdiff_vunion_Obj_in_Obj:
  assumes "J \<subseteq>\<^sub>\<circ> I"
    and "b \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gk\<in>\<^sub>\<circ>I -\<^sub>\<circ> J. \<AA> k)\<lparr>Obj\<rparr>"
    and "c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>J. \<AA> j)\<lparr>Obj\<rparr>"
  shows "b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by
    (
      vdiff_of_vunion
        rule: dg_prod_vunion_Obj_in_Obj assms: assms(2,3) subset: assms(1)
    )


[STATEMENT]
lemma dghm_proj_snd_is_dghm'[dg_cs_intros]:
  assumes "i \<in>\<^sub>\<circ> I" and "\<CC> = \<AA> \<times>\<^sub>D\<^sub>G \<BB>" and "\
 = \<BB>"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB> : \<AA> \<times>\<^sub>D\<^sub>G \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule dghm_proj_snd_is_dghm)


[STATEMENT]
lemma Shuffle_Plus_ShuffleLR_One[simp]: "Times_Plus (ShuffleLR r One) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus (ShuffleLR r One) = r
[PROOF STEP]
by (coinduction arbitrary: r) simp


[STATEMENT]
lemma GodNecExists_v1: "\<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E \<^bold>\<down>G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
using GodExImpliesNecEx_v1 T3_deRe
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. \<P> xa w \<longrightarrow> xa x) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x))) w)\<rfloor>
serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa w \<longrightarrow> xa x)))

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v \<longrightarrow> xa x)))
[PROOF STEP]
by fastforce \<comment> \<open>corollary 11.28\<close>


[STATEMENT]
lemma (in order) elem_order_zmset_exists_foundation:
  fixes x :: 'a
  assumes "x \<in>#\<^sub>z M"
  shows   "\<exists>s\<in>#\<^sub>zM. s \<le> x \<and> (\<forall>u\<in>#\<^sub>zM. \<not> u < s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<in>#\<^sub>zM. s \<le> x \<and> (\<forall>u\<in>#\<^sub>zM. \<not> u < s)
[PROOF STEP]
by (rule order_finite_set_exists_foundation[OF finite_set_zmset, OF assms(1)])


[STATEMENT]
lemma return_pmf_card_equals_set:
  shows "card {return_pmf x |x. x \<in> S} = card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {return_pmf x |x. x \<in> S} = card S
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {return_pmf x |x. x \<in> S} = card S
[PROOF STEP]
have "{return_pmf x |x. x \<in> S} = return_pmf ` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {return_pmf x |x. x \<in> S} = return_pmf ` S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{return_pmf x |x. x \<in> S} = return_pmf ` S

goal (1 subgoal):
 1. card {return_pmf x |x. x \<in> S} = card S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{return_pmf x |x. x \<in> S} = return_pmf ` S

goal (1 subgoal):
 1. card {return_pmf x |x. x \<in> S} = card S
[PROOF STEP]
have "card \<dots> = card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (return_pmf ` S) = card S
[PROOF STEP]
by (intro card_image) (auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
card (return_pmf ` S) = card S

goal (1 subgoal):
 1. card {return_pmf x |x. x \<in> S} = card S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {return_pmf x |x. x \<in> S} = card S
[PROOF STEP]
show "card {return_pmf x |x. x \<in> S} = card S"
[PROOF STATE]
proof (prove)
using this:
card {return_pmf x |x. x \<in> S} = card S

goal (1 subgoal):
 1. card {return_pmf x |x. x \<in> S} = card S
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card {return_pmf x |x. x \<in> S} = card S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fresh_fv_list[simp]:
  "a \<sharp> (fv_list e :: 'b::at_base list) \<longleftrightarrow> a \<sharp> (fv e :: 'b::at_base set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> fv_list e = a \<sharp> fv e
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> fv_list e = a \<sharp> fv e
[PROOF STEP]
have "a \<sharp> (fv_list e :: 'b::at_base list) \<longleftrightarrow> a \<sharp> set (fv_list e :: 'b::at_base list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> fv_list e = a \<sharp> set (fv_list e)
[PROOF STEP]
by (rule fresh_set[symmetric])
[PROOF STATE]
proof (state)
this:
a \<sharp> fv_list e = a \<sharp> set (fv_list e)

goal (1 subgoal):
 1. a \<sharp> fv_list e = a \<sharp> fv e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<sharp> fv_list e = a \<sharp> set (fv_list e)

goal (1 subgoal):
 1. a \<sharp> fv_list e = a \<sharp> fv e
[PROOF STEP]
have "\<dots> \<longleftrightarrow> a \<sharp> (fv e :: 'b::at_base set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> set (fv_list e) = a \<sharp> fv e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<sharp> set (fv_list e) = a \<sharp> fv e

goal (1 subgoal):
 1. a \<sharp> fv_list e = a \<sharp> fv e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a \<sharp> fv_list e = a \<sharp> fv e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<sharp> fv_list e = a \<sharp> fv e

goal (1 subgoal):
 1. a \<sharp> fv_list e = a \<sharp> fv e
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a \<sharp> fv_list e = a \<sharp> fv e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vfsequence_vcomp_vsv_vfsequence:
  assumes "vsv f" and "vfsequence xs" and "\<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> f"
  shows "vfsequence (f \<circ>\<^sub>\<circ> xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (f \<circ>\<^sub>\<circ> xs)
[PROOF STEP]
proof(intro vfsequenceI vsv_vcomp)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv f
 2. vsv xs
 3. \<D>\<^sub>\<circ> (f \<circ>\<^sub>\<circ> xs) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
interpret xs: vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv f
 2. vsv xs
 3. \<D>\<^sub>\<circ> (f \<circ>\<^sub>\<circ> xs) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (f \<circ>\<^sub>\<circ> xs) \<in>\<^sub>\<circ> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (f \<circ>\<^sub>\<circ> xs) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
unfolding vdomain_vcomp_vsubset[OF assms(3)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
by (force simp: xs.vfsequence_vdomain_in_omega)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (f \<circ>\<^sub>\<circ> xs) \<in>\<^sub>\<circ> \<omega>

goal (2 subgoals):
 1. vsv f
 2. vsv xs
[PROOF STEP]
qed (auto intro: assms)


[STATEMENT]
lemma cr_scalar_transfer_domain_rule[transfer_domain_rule]:
  "Domainp (cr_scalar R) = (\<lambda>x. \<exists>a. x = [a]\<^sub>\<circ> \<and> Domainp R a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domainp (cr_scalar R) = (\<lambda>x. \<exists>a. x = [a]\<^sub>\<circ> \<and> Domainp R a)
[PROOF STEP]
unfolding cr_scalar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domainp (\<lambda>x y. \<exists>a. x = [a]\<^sub>\<circ> \<and> R a y) = (\<lambda>x. \<exists>a. x = [a]\<^sub>\<circ> \<and> Domainp R a)
[PROOF STEP]
by auto


[STATEMENT]
lemma PRE_D2: "(Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> S x \<longrightarrow> P x y)) \<longrightarrow> comp_PRE S1 Q P S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> S x \<longrightarrow> P x y) \<longrightarrow> comp_PRE S1 Q P S x
[PROOF STEP]
by (auto simp: comp_PRE_def)


[STATEMENT]
lemma in_set_real_plus_interval[intro, simp]:
  "x + y \<in>\<^sub>r X + Y" if "x \<in>\<^sub>r X" "y \<in>\<^sub>r Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + y \<in>\<^sub>r X + Y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r X
y \<in>\<^sub>r Y

goal (1 subgoal):
 1. x + y \<in>\<^sub>r X + Y
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma tm_add_range:
  "x + y \<in>\<^sub>i range_tm e (tm_add t1 t2)"
  if "x \<in>\<^sub>i range_tm e t1"
    "y \<in>\<^sub>i range_tm e t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + y \<in>\<^sub>i range_tm e (tm_add t1 t2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x + y \<in>\<^sub>i range_tm e (tm_add t1 t2)
[PROOF STEP]
from range_tmD[OF that(1)] range_tmD[OF that(2)]
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1)
y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1)
y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2)

goal (1 subgoal):
 1. x + y \<in>\<^sub>i range_tm e (tm_add t1 t2)
[PROOF STEP]
apply (cases t1; cases t2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1); y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2); t1 = TaylorModel x1 x2; x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1); y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2); t2 = TaylorModel x1a x2a\<rbrakk> \<Longrightarrow> x + y \<in>\<^sub>i range_tm e (tm_add t1 t2)
[PROOF STEP]
apply (rule range_tmI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1); y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2); t1 = TaylorModel x1 x2; x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1); y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2); t2 = TaylorModel x1a x2a\<rbrakk> \<Longrightarrow> x + y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly (tm_add t1 t2)))) + real_interval (tm_bound (tm_add t1 t2))
[PROOF STEP]
by (auto simp: map_poly_homo_polyadd real_interval_plus ac_simps interval_of_add
        num_params_polyadd insertion_polyadd set_of_eq
        dest: less_le_trans[OF _ num_params_polyadd])
[PROOF STATE]
proof (state)
this:
x + y \<in>\<^sub>i range_tm e (tm_add t1 t2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma region_reset_not_Succ:
  (* XXX Declare globally? *)
  notes regions_closed'_spec[intro]
  assumes "R \<in> \<R>" "set r \<subseteq> X"
  shows "region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R" (is "?R = R \<or> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
from assms finite
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
set r \<subseteq> X
finite X
[PROOF STEP]
obtain u where "u \<in> R"
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>
set r \<subseteq> X
finite X

goal (1 subgoal):
 1. (\<And>u. u \<in> R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson Succ.cases succ_ex(2))
[PROOF STATE]
proof (state)
this:
u \<in> R

goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
with \<open>R \<in> \<R>\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
u \<in> R
[PROOF STEP]
have "u \<in> V" "[u]\<^sub>\<R> = R"
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>
u \<in> R

goal (1 subgoal):
 1. u \<in> V &&& [u]\<^sub>\<R> = R
[PROOF STEP]
by (auto simp: region_unique_spec dest: region_V)
[PROOF STATE]
proof (state)
this:
u \<in> V
[u]\<^sub>\<R> = R

goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
with region_set'_id[OF \<open>R \<in> \<R>\<close>[unfolded \<R>_def] \<open>u \<in> R\<close> finite] assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 \<le> ?c; \<forall>x\<in>set ?r. ?c \<le> k x; set ?r \<subseteq> X\<rbrakk> \<Longrightarrow> [[?r\<rightarrow>real ?c]u]\<^sub>{Regions.region X I r |I r. Regions.valid_region X k I r} = region_set' R ?r (real ?c) \<and> [[?r\<rightarrow>real ?c]u]\<^sub>{Regions.region X I r |I r. Regions.valid_region X k I r} \<in> {Regions.region X I r |I r. Regions.valid_region X k I r} \<and> [?r\<rightarrow>real ?c]u \<in> [[?r\<rightarrow>real ?c]u]\<^sub>{Regions.region X I r |I r. Regions.valid_region X k I r}
set r \<subseteq> X
u \<in> V
[u]\<^sub>\<R> = R
[PROOF STEP]
have
    "?R = [[r\<rightarrow>0]u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?c; \<forall>x\<in>set ?r. ?c \<le> k x; set ?r \<subseteq> X\<rbrakk> \<Longrightarrow> [[?r\<rightarrow>real ?c]u]\<^sub>{Regions.region X I r |I r. Regions.valid_region X k I r} = region_set' R ?r (real ?c) \<and> [[?r\<rightarrow>real ?c]u]\<^sub>{Regions.region X I r |I r. Regions.valid_region X k I r} \<in> {Regions.region X I r |I r. Regions.valid_region X k I r} \<and> [?r\<rightarrow>real ?c]u \<in> [[?r\<rightarrow>real ?c]u]\<^sub>{Regions.region X I r |I r. Regions.valid_region X k I r}
set r \<subseteq> X
u \<in> V
[u]\<^sub>\<R> = R

goal (1 subgoal):
 1. region_set' R r 0 = [[r\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
by (force simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
region_set' R r 0 = [[r\<rightarrow>0]u]\<^sub>\<R>

goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
proof (cases "\<forall> x \<in> set r. u x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>set r. u x = 0 \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
 2. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set r. u x = 0

goal (2 subgoals):
 1. \<forall>x\<in>set r. u x = 0 \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
 2. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set r. u x = 0
[PROOF STEP]
have "[r\<rightarrow>0]u = u"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set r. u x = 0

goal (1 subgoal):
 1. [r\<rightarrow>0]u = u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[r\<rightarrow>0]u = u

goal (2 subgoals):
 1. \<forall>x\<in>set r. u x = 0 \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
 2. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
with \<open>?R = _\<close> \<open>_ = R\<close>
[PROOF STATE]
proof (chain)
picking this:
region_set' R r 0 = [[r\<rightarrow>0]u]\<^sub>\<R>
[u]\<^sub>\<R> = R
[r\<rightarrow>0]u = u
[PROOF STEP]
have "?R = R"
[PROOF STATE]
proof (prove)
using this:
region_set' R r 0 = [[r\<rightarrow>0]u]\<^sub>\<R>
[u]\<^sub>\<R> = R
[r\<rightarrow>0]u = u

goal (1 subgoal):
 1. region_set' R r 0 = R
[PROOF STEP]
by (force simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
region_set' R r 0 = R

goal (2 subgoals):
 1. \<forall>x\<in>set r. u x = 0 \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
 2. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
region_set' R r 0 = R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
region_set' R r 0 = R

goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x\<in>set r. u x = 0)

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x\<in>set r. u x = 0)
[PROOF STEP]
obtain x where x: "x \<in> set r" "u x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>set r. u x = 0)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> set r; u x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set r
u x \<noteq> 0

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> set r
u x \<noteq> 0

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
assume "?R \<in> Succ \<R> R"
[PROOF STATE]
proof (state)
this:
region_set' R r 0 \<in> Succ \<R> R

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
with \<open>u \<in> R\<close> \<open>R \<in> \<R>\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> R
R \<in> \<R>
region_set' R r 0 \<in> Succ \<R> R
[PROOF STEP]
obtain t where
        "t \<ge> 0" "[u \<oplus> t]\<^sub>\<R> = ?R" "?R \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
u \<in> R
R \<in> \<R>
region_set' R r 0 \<in> Succ \<R> R

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; [u \<oplus> t]\<^sub>\<R> = region_set' R r 0; region_set' R r 0 \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson Succ.cases set_of_regions_spec)
[PROOF STATE]
proof (state)
this:
0 \<le> t
[u \<oplus> t]\<^sub>\<R> = region_set' R r 0
region_set' R r 0 \<in> \<R>

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
with \<open>u \<in> R\<close> assms(1)
[PROOF STATE]
proof (chain)
picking this:
u \<in> R
R \<in> \<R>
0 \<le> t
[u \<oplus> t]\<^sub>\<R> = region_set' R r 0
region_set' R r 0 \<in> \<R>
[PROOF STEP]
have "u \<oplus> t \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
u \<in> R
R \<in> \<R>
0 \<le> t
[u \<oplus> t]\<^sub>\<R> = region_set' R r 0
region_set' R r 0 \<in> \<R>

goal (1 subgoal):
 1. u \<oplus> t \<in> region_set' R r 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<oplus> t \<in> region_set' R r 0

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<oplus> t \<in> region_set' R r 0

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
from \<open>?R = _\<close> \<open>u \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
region_set' R r 0 = [[r\<rightarrow>0]u]\<^sub>\<R>
u \<in> R
[PROOF STEP]
have "[r\<rightarrow>0]u \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
region_set' R r 0 = [[r\<rightarrow>0]u]\<^sub>\<R>
u \<in> R

goal (1 subgoal):
 1. [r\<rightarrow>0]u \<in> region_set' R r 0
[PROOF STEP]
by (fastforce simp: region_set'_def)
[PROOF STATE]
proof (state)
this:
[r\<rightarrow>0]u \<in> region_set' R r 0

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[r\<rightarrow>0]u \<in> region_set' R r 0

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
from x \<open>t \<ge> 0\<close> \<open>u \<in> V\<close> assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> set r
u x \<noteq> 0
0 \<le> t
u \<in> V
R \<in> \<R>
set r \<subseteq> X
[PROOF STEP]
have "(u \<oplus> t) x > 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> set r
u x \<noteq> 0
0 \<le> t
u \<in> V
R \<in> \<R>
set r \<subseteq> X

goal (1 subgoal):
 1. 0 < (u \<oplus> t) x
[PROOF STEP]
by (force simp: cval_add_def V_def)
[PROOF STATE]
proof (state)
this:
0 < (u \<oplus> t) x

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < (u \<oplus> t) x

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> set r
u x \<noteq> 0
[PROOF STEP]
have "([r\<rightarrow>0]u) x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> set r
u x \<noteq> 0

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = 0

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<oplus> t \<in> region_set' R r 0
[r\<rightarrow>0]u \<in> region_set' R r 0
0 < (u \<oplus> t) x
([r\<rightarrow>0]u) x = 0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
u \<oplus> t \<in> region_set' R r 0
[r\<rightarrow>0]u \<in> region_set' R r 0
0 < (u \<oplus> t) x
([r\<rightarrow>0]u) x = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>?R \<in> \<R>\<close> x(1)
[PROOF STATE]
proof (prove)
using this:
u \<oplus> t \<in> region_set' R r 0
[r\<rightarrow>0]u \<in> region_set' R r 0
0 < (u \<oplus> t) x
([r\<rightarrow>0]u) x = 0
region_set' R r 0 \<in> \<R>
x \<in> set r

goal (1 subgoal):
 1. False
[PROOF STEP]
by (fastforce simp: region_set'_def)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
region_set' R r 0 \<in> Succ \<R> R \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>set r. u x = 0) \<Longrightarrow> region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
region_set' R r 0 \<in> Succ \<R> R \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
region_set' R r 0 \<in> Succ \<R> R \<Longrightarrow> False

goal (1 subgoal):
 1. region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
region_set' R r 0 = R \<or> region_set' R r 0 \<notin> Succ \<R> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R_G_K_cfg_valid_cfgD:
  assumes "cfg \<in> R_G.valid_cfg" "cfg' \<in> K_cfg cfg"
  shows "cfg' = cont cfg (state cfg')" "state cfg' \<in> action cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg' = cont cfg (state cfg') &&& state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cfg' = cont cfg (state cfg')
 2. state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
cfg' \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
obtain s where "s \<in> action cfg" "cfg' = cont cfg s"
[PROOF STATE]
proof (prove)
using this:
cfg' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> set_pmf (action cfg); cfg' = cont cfg s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: set_K_cfg)
[PROOF STATE]
proof (state)
this:
s \<in> set_pmf (action cfg)
cfg' = cont cfg s

goal (2 subgoals):
 1. cfg' = cont cfg (state cfg')
 2. state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
cfg' \<in> set_pmf (K_cfg cfg)
s \<in> set_pmf (action cfg)
cfg' = cont cfg s
[PROOF STEP]
show
    "cfg' = cont cfg (state cfg')" "state cfg' \<in> action cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
cfg' \<in> set_pmf (K_cfg cfg)
s \<in> set_pmf (action cfg)
cfg' = cont cfg s

goal (1 subgoal):
 1. cfg' = cont cfg (state cfg') &&& state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
by (auto intro: R_G.valid_cfg_state_in_S R_G.valid_cfgD)
[PROOF STATE]
proof (state)
this:
cfg' = cont cfg (state cfg')
state cfg' \<in> set_pmf (action cfg)

goal:
No subgoals!
[PROOF STEP]
qed