[STATEMENT]
lemma neville_aitken_main: assumes dist: "\<And> i j. i < j \<Longrightarrow> j \<le> n \<Longrightarrow> x i \<noteq> x j"
  shows "i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> j \<le> n \<Longrightarrow> poly (neville_aitken_main i j) (x k) = (f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
proof (induct i j arbitrary: k rule: neville_aitken_main.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<And>k. \<lbrakk>i < j; i + 1 \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main (i + 1) j) (x k) = f k; \<And>k. \<lbrakk>i < j; i \<le> k; k \<le> j - 1; j - 1 \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i (j - 1)) (x k) = f k; i \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
case (1 i j k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < j; i + 1 \<le> ?k; ?k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main (i + 1) j) (x ?k) = f ?k
\<lbrakk>i < j; i \<le> ?k; ?k \<le> j - 1; j - 1 \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i (j - 1)) (x ?k) = f ?k
i \<le> k
k \<le> j
j \<le> n

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<And>k. \<lbrakk>i < j; i + 1 \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main (i + 1) j) (x k) = f k; \<And>k. \<lbrakk>i < j; i \<le> k; k \<le> j - 1; j - 1 \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i (j - 1)) (x k) = f k; i \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
note neville_aitken_main.simps[of i j, simp]
[PROOF STATE]
proof (state)
this:
local.neville_aitken_main i j = (if i < j then smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) else [:f i:])

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<And>k. \<lbrakk>i < j; i + 1 \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main (i + 1) j) (x k) = f k; \<And>k. \<lbrakk>i < j; i \<le> k; k \<le> j - 1; j - 1 \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i (j - 1)) (x k) = f k; i \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
proof (cases "i < j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
 2. \<not> i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (2 subgoals):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
 2. \<not> i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
with 1(3-)
[PROOF STATE]
proof (chain)
picking this:
i \<le> k
k \<le> j
j \<le> n
\<not> i < j
[PROOF STEP]
have "k = i"
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<le> j
j \<le> n
\<not> i < j

goal (1 subgoal):
 1. k = i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = i

goal (2 subgoals):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
 2. \<not> i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> i < j
k = i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> i < j
k = i

goal (1 subgoal):
 1. poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly (local.neville_aitken_main i j) (x k) = f k

goal (1 subgoal):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
note ij = this
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
from dist[OF True 1(5)]
[PROOF STATE]
proof (chain)
picking this:
x i \<noteq> x j
[PROOF STEP]
have diff: "x i \<noteq> x j"
[PROOF STATE]
proof (prove)
using this:
x i \<noteq> x j

goal (1 subgoal):
 1. x i \<noteq> x j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x i \<noteq> x j

goal (1 subgoal):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
i < j
[PROOF STEP]
have id: "neville_aitken_main i j =
      (smult (inverse (x j - x i)) (X i * neville_aitken_main (i + 1) j - X j
        * neville_aitken_main i (j - 1)))"
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. local.neville_aitken_main i j = smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.neville_aitken_main i j = smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))

goal (1 subgoal):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
note IH = 1(1-2)[OF True]
[PROOF STATE]
proof (state)
this:
\<lbrakk>i + 1 \<le> ?k; ?k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main (i + 1) j) (x ?k) = f ?k
\<lbrakk>i \<le> ?k; ?k \<le> j - 1; j - 1 \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i (j - 1)) (x ?k) = f ?k

goal (1 subgoal):
 1. i < j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
proof (cases "k = i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
 2. k \<noteq> i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = i

goal (2 subgoals):
 1. k = i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
 2. k \<noteq> i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
unfolding id True poly_smult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (x j - x i) * poly (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) (x i) = f i
[PROOF STEP]
using IH(2)[of i] ij 1(3-) diff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<le> i; i \<le> j - 1; j - 1 \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i (j - 1)) (x i) = f i
i < j
i \<le> k
k \<le> j
j \<le> n
x i \<noteq> x j

goal (1 subgoal):
 1. inverse (x j - x i) * poly (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) (x i) = f i
[PROOF STEP]
by (simp add: X_def field_simps)
[PROOF STATE]
proof (state)
this:
poly (local.neville_aitken_main i j) (x k) = f k

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> i

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
note ki = this
[PROOF STATE]
proof (state)
this:
k \<noteq> i

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
proof (cases "k = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
 2. k \<noteq> j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = j

goal (2 subgoals):
 1. k = j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
 2. k \<noteq> j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
unfolding id True poly_smult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (x j - x i) * poly (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) (x j) = f j
[PROOF STEP]
using IH(1)[of j] ij 1(3-) diff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i + 1 \<le> j; j \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main (i + 1) j) (x j) = f j
i < j
i \<le> k
k \<le> j
j \<le> n
x i \<noteq> x j

goal (1 subgoal):
 1. inverse (x j - x i) * poly (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) (x j) = f j
[PROOF STEP]
by (simp add: X_def field_simps)
[PROOF STATE]
proof (state)
this:
poly (local.neville_aitken_main i j) (x k) = f k

goal (1 subgoal):
 1. k \<noteq> j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> j

goal (1 subgoal):
 1. k \<noteq> j \<Longrightarrow> poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
with ki
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> i
k \<noteq> j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i
k \<noteq> j

goal (1 subgoal):
 1. poly (local.neville_aitken_main i j) (x k) = f k
[PROOF STEP]
unfolding id poly_smult
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i
k \<noteq> j

goal (1 subgoal):
 1. inverse (x j - x i) * poly (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) (x k) = f k
[PROOF STEP]
using IH(1-2)[of k] ij 1(3-) diff
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i
k \<noteq> j
\<lbrakk>i + 1 \<le> k; k \<le> j; j \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main (i + 1) j) (x k) = f k
\<lbrakk>i \<le> k; k \<le> j - 1; j - 1 \<le> n\<rbrakk> \<Longrightarrow> poly (local.neville_aitken_main i (j - 1)) (x k) = f k
i < j
i \<le> k
k \<le> j
j \<le> n
x i \<noteq> x j

goal (1 subgoal):
 1. inverse (x j - x i) * poly (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) (x k) = f k
[PROOF STEP]
by (simp add: X_def field_simps)
[PROOF STATE]
proof (state)
this:
poly (local.neville_aitken_main i j) (x k) = f k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly (local.neville_aitken_main i j) (x k) = f k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly (local.neville_aitken_main i j) (x k) = f k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly (local.neville_aitken_main i j) (x k) = f k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_neville_aitken_main: "degree (neville_aitken_main i j) \<le> j - i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
proof (induct i j rule: neville_aitken_main.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < j \<Longrightarrow> degree (local.neville_aitken_main (i + 1) j) \<le> j - (i + 1); i < j \<Longrightarrow> degree (local.neville_aitken_main i (j - 1)) \<le> j - 1 - i\<rbrakk> \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
case (1 i j)
[PROOF STATE]
proof (state)
this:
i < j \<Longrightarrow> degree (local.neville_aitken_main (i + 1) j) \<le> j - (i + 1)
i < j \<Longrightarrow> degree (local.neville_aitken_main i (j - 1)) \<le> j - 1 - i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < j \<Longrightarrow> degree (local.neville_aitken_main (i + 1) j) \<le> j - (i + 1); i < j \<Longrightarrow> degree (local.neville_aitken_main i (j - 1)) \<le> j - 1 - i\<rbrakk> \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
note simp = neville_aitken_main.simps[of i j]
[PROOF STATE]
proof (state)
this:
local.neville_aitken_main i j = (if i < j then smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) else [:f i:])

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < j \<Longrightarrow> degree (local.neville_aitken_main (i + 1) j) \<le> j - (i + 1); i < j \<Longrightarrow> degree (local.neville_aitken_main i (j - 1)) \<le> j - 1 - i\<rbrakk> \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
proof (cases "i < j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
 2. \<not> i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (2 subgoals):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
 2. \<not> i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> i < j

goal (1 subgoal):
 1. degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
unfolding simp
[PROOF STATE]
proof (prove)
using this:
\<not> i < j

goal (1 subgoal):
 1. degree (if i < j then smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) else [:f i:]) \<le> j - i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (local.neville_aitken_main i j) \<le> j - i

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
note IH = 1[OF this]
[PROOF STATE]
proof (state)
this:
degree (local.neville_aitken_main (i + 1) j) \<le> j - (i + 1)
degree (local.neville_aitken_main i (j - 1)) \<le> j - 1 - i

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
let ?n = neville_aitken_main
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have X: "\<And> i. degree (X i) = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. degree (X i) = Suc 0
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. degree [:- x i, 1::'a:] = Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (X ?i) = Suc 0

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have "degree (X i * ?n (i + 1) j) \<le> Suc (degree (?n (i+1) j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (X i * local.neville_aitken_main (i + 1) j) \<le> Suc (degree (local.neville_aitken_main (i + 1) j))
[PROOF STEP]
by (rule order.trans[OF degree_mult_le], simp add: X)
[PROOF STATE]
proof (state)
this:
degree (X i * local.neville_aitken_main (i + 1) j) \<le> Suc (degree (local.neville_aitken_main (i + 1) j))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (X i * local.neville_aitken_main (i + 1) j) \<le> Suc (degree (local.neville_aitken_main (i + 1) j))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have "\<dots> \<le> Suc (j - (i+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (degree (local.neville_aitken_main (i + 1) j)) \<le> Suc (j - (i + 1))
[PROOF STEP]
using IH(1)
[PROOF STATE]
proof (prove)
using this:
degree (local.neville_aitken_main (i + 1) j) \<le> j - (i + 1)

goal (1 subgoal):
 1. Suc (degree (local.neville_aitken_main (i + 1) j)) \<le> Suc (j - (i + 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (degree (local.neville_aitken_main (i + 1) j)) \<le> Suc (j - (i + 1))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (X i * local.neville_aitken_main (i + 1) j) \<le> Suc (j - (i + 1))
[PROOF STEP]
have 1: "degree (X i * ?n (i + 1) j) \<le> j - i"
[PROOF STATE]
proof (prove)
using this:
degree (X i * local.neville_aitken_main (i + 1) j) \<le> Suc (j - (i + 1))

goal (1 subgoal):
 1. degree (X i * local.neville_aitken_main (i + 1) j) \<le> j - i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
degree (X i * local.neville_aitken_main (i + 1) j) \<le> Suc (j - (i + 1))
i < j

goal (1 subgoal):
 1. degree (X i * local.neville_aitken_main (i + 1) j) \<le> j - i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (X i * local.neville_aitken_main (i + 1) j) \<le> j - i

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have "degree (X j * ?n i (j - 1)) \<le> Suc (degree (?n i (j - 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (X j * local.neville_aitken_main i (j - 1)) \<le> Suc (degree (local.neville_aitken_main i (j - 1)))
[PROOF STEP]
by (rule order.trans[OF degree_mult_le], simp add: X)
[PROOF STATE]
proof (state)
this:
degree (X j * local.neville_aitken_main i (j - 1)) \<le> Suc (degree (local.neville_aitken_main i (j - 1)))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (X j * local.neville_aitken_main i (j - 1)) \<le> Suc (degree (local.neville_aitken_main i (j - 1)))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have "\<dots> \<le> Suc ((j - 1) - i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (degree (local.neville_aitken_main i (j - 1))) \<le> Suc (j - 1 - i)
[PROOF STEP]
using IH(2)
[PROOF STATE]
proof (prove)
using this:
degree (local.neville_aitken_main i (j - 1)) \<le> j - 1 - i

goal (1 subgoal):
 1. Suc (degree (local.neville_aitken_main i (j - 1))) \<le> Suc (j - 1 - i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (degree (local.neville_aitken_main i (j - 1))) \<le> Suc (j - 1 - i)

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (X j * local.neville_aitken_main i (j - 1)) \<le> Suc (j - 1 - i)
[PROOF STEP]
have 2: "degree (X j * ?n i (j - 1)) \<le> j - i"
[PROOF STATE]
proof (prove)
using this:
degree (X j * local.neville_aitken_main i (j - 1)) \<le> Suc (j - 1 - i)

goal (1 subgoal):
 1. degree (X j * local.neville_aitken_main i (j - 1)) \<le> j - i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
degree (X j * local.neville_aitken_main i (j - 1)) \<le> Suc (j - 1 - i)
i < j

goal (1 subgoal):
 1. degree (X j * local.neville_aitken_main i (j - 1)) \<le> j - i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (X j * local.neville_aitken_main i (j - 1)) \<le> j - i

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have id: "?n i j = smult (inverse (x j - x i))
            (X i * ?n (i + 1) j - X j * ?n i (j - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.neville_aitken_main i j = smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))
[PROOF STEP]
unfolding simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < j then smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) else [:f i:]) = smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. (if i < j then smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) else [:f i:]) = smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.neville_aitken_main i j = smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have "degree (?n i j) \<le> degree (X i * ?n (i + 1) j - X j * ?n i (j - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (local.neville_aitken_main i j) \<le> degree (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (smult (inverse (x j - x i)) (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))) \<le> degree (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (local.neville_aitken_main i j) \<le> degree (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (local.neville_aitken_main i j) \<le> degree (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have "\<dots> \<le> max (degree (X i * ?n (i + 1) j)) (degree (X j * ?n i (j - 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) \<le> max (degree (X i * local.neville_aitken_main (i + 1) j)) (degree (X j * local.neville_aitken_main i (j - 1)))
[PROOF STEP]
by (rule degree_diff_le_max)
[PROOF STATE]
proof (state)
this:
degree (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) \<le> max (degree (X i * local.neville_aitken_main (i + 1) j)) (degree (X j * local.neville_aitken_main i (j - 1)))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (X i * local.neville_aitken_main (i + 1) j - X j * local.neville_aitken_main i (j - 1)) \<le> max (degree (X i * local.neville_aitken_main (i + 1) j)) (degree (X j * local.neville_aitken_main i (j - 1)))

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
have "\<dots> \<le> j - i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (degree (X i * local.neville_aitken_main (i + 1) j)) (degree (X j * local.neville_aitken_main i (j - 1))) \<le> j - i
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
degree (X i * local.neville_aitken_main (i + 1) j) \<le> j - i
degree (X j * local.neville_aitken_main i (j - 1)) \<le> j - i

goal (1 subgoal):
 1. max (degree (X i * local.neville_aitken_main (i + 1) j)) (degree (X j * local.neville_aitken_main i (j - 1))) \<le> j - i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (degree (X i * local.neville_aitken_main (i + 1) j)) (degree (X j * local.neville_aitken_main i (j - 1))) \<le> j - i

goal (1 subgoal):
 1. i < j \<Longrightarrow> degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree (local.neville_aitken_main i j) \<le> j - i

goal (1 subgoal):
 1. degree (local.neville_aitken_main i j) \<le> j - i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree (local.neville_aitken_main i j) \<le> j - i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
degree (local.neville_aitken_main i j) \<le> j - i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_neville_aitken: "degree (neville_aitken n) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (local.neville_aitken n) \<le> n
[PROOF STEP]
unfolding neville_aitken_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (local.neville_aitken_main 0 n) \<le> n
[PROOF STEP]
using degree_neville_aitken_main[of 0 n]
[PROOF STATE]
proof (prove)
using this:
degree (local.neville_aitken_main 0 n) \<le> n - 0

goal (1 subgoal):
 1. degree (local.neville_aitken_main 0 n) \<le> n
[PROOF STEP]
by simp


[STATEMENT]
lemma length_neville_aitken_merge[termination_simp]: "length (neville_aitken_merge xs) = length xs - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (local.neville_aitken_merge xs) = length xs - 1
[PROOF STEP]
by (induct xs rule: neville_aitken_merge.induct, auto)


[STATEMENT]
lemma neville_aitken_merge:
  "xs = map (\<lambda> i. (x i, x (i + j), neville_aitken_main i (i + j)))  [l ..< Suc (l + k)]
   \<Longrightarrow> neville_aitken_merge xs
       = (map (\<lambda> i. (x i, x (i + Suc j), neville_aitken_main i (i + Suc j))) [l ..< l + k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge xs = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
proof (induct xs arbitrary: l k rule: neville_aitken_merge.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
case (1 xi xj p_ij xsi xsj p_sisj rest l k)
[PROOF STATE]
proof (state)
this:
(xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [?l..<Suc (?l + ?k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [?l..<?l + ?k]
(xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
let ?n = neville_aitken_main
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
let ?f = "\<lambda> j i. (x i, x (i + j), ?n i (i + j))"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
define f where "f = ?f"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>j i. (x i, x (i + j), local.neville_aitken_main i (i + j)))

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
let ?map = "\<lambda> j. map (?f j)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
note res = 1(2)
[PROOF STATE]
proof (state)
this:
(xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
from arg_cong[OF res, of length]
[PROOF STATE]
proof (chain)
picking this:
length ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = length (map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)])
[PROOF STEP]
obtain kk where k: "k = Suc kk"
[PROOF STATE]
proof (prove)
using this:
length ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = length (map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)])

goal (1 subgoal):
 1. (\<And>kk. k = Suc kk \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases k, auto)
[PROOF STATE]
proof (state)
this:
k = Suc kk

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
hence id: "[l..<Suc (l + k)] = l # [Suc l ..< Suc (Suc l + kk)]"
[PROOF STATE]
proof (prove)
using this:
k = Suc kk

goal (1 subgoal):
 1. [l..<Suc (l + k)] = l # [Suc l..<Suc (Suc l + kk)]
[PROOF STEP]
by (simp add: upt_rec)
[PROOF STATE]
proof (state)
this:
[l..<Suc (l + k)] = l # [Suc l..<Suc (Suc l + kk)]

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
from res[unfolded id]
[PROOF STATE]
proof (chain)
picking this:
(xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) (l # [Suc l..<Suc (Suc l + kk)])
[PROOF STEP]
have id2: "(xsi, xsj, p_sisj) # rest =
    ?map j [Suc l..< Suc (Suc l + kk)]"
    and id3: "xi = x l" "xj = x (l + j)" "p_ij = ?n l (l + j)"
        "xsi = x (Suc l)" "xsj = x (Suc (l + j))" "p_sisj = ?n (Suc l) (Suc (l + j))"
[PROOF STATE]
proof (prove)
using this:
(xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) (l # [Suc l..<Suc (Suc l + kk)])

goal (1 subgoal):
 1. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [Suc l..<Suc (Suc l + kk)] &&& (xi = x l &&& xj = x (l + j) &&& p_ij = local.neville_aitken_main l (l + j)) &&& xsi = x (Suc l) &&& xsj = x (Suc (l + j)) &&& p_sisj = local.neville_aitken_main (Suc l) (Suc (l + j))
[PROOF STEP]
by (auto simp: upt_rec)
[PROOF STATE]
proof (state)
this:
(xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [Suc l..<Suc (Suc l + kk)]
xi = x l
xj = x (l + j)
p_ij = local.neville_aitken_main l (l + j)
xsi = x (Suc l)
xsj = x (Suc (l + j))
p_sisj = local.neville_aitken_main (Suc l) (Suc (l + j))

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
note IH = 1(1)[OF id2]
[PROOF STATE]
proof (state)
this:
local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [Suc l..<Suc l + kk]

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
have X: "[:x (Suc (l + j)), - 1:] = - X (Suc l + j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:x (Suc (l + j)), - (1::'a):] = - X (Suc l + j)
[PROOF STEP]
unfolding X_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:x (Suc (l + j)), - (1::'a):] = - [:- x (Suc l + j), 1::'a:]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[:x (Suc (l + j)), - (1::'a):] = - X (Suc l + j)

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
have id4: "(xi, xsj, smult (inverse (xsj - xi)) ([:- xi, 1:] * p_sisj +
     [:xsj, - 1:] * p_ij)) = (x l, x (l + Suc j), ?n l (l + Suc j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xi, xsj, smult (inverse (xsj - xi)) ([:- xi, 1::'a:] * p_sisj + [:xsj, - (1::'a):] * p_ij)) = (x l, x (l + Suc j), local.neville_aitken_main l (l + Suc j))
[PROOF STEP]
unfolding id3 neville_aitken_main.simps[of l "l + Suc j"]
      X_def[symmetric] X
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x l, x (Suc (l + j)), smult (inverse (x (Suc (l + j)) - x l)) (X l * local.neville_aitken_main (Suc l) (Suc (l + j)) + - X (Suc l + j) * local.neville_aitken_main l (l + j))) = (x l, x (l + Suc j), if l < l + Suc j then smult (inverse (x (l + Suc j) - x l)) (X l * local.neville_aitken_main (l + 1) (l + Suc j) - X (l + Suc j) * local.neville_aitken_main l (l + Suc j - 1)) else [:f l:])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(xi, xsj, smult (inverse (xsj - xi)) ([:- xi, 1::'a:] * p_sisj + [:xsj, - (1::'a):] * p_ij)) = (x l, x (l + Suc j), local.neville_aitken_main l (l + Suc j))

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
have id5: "[l..<l + k] = l # [Suc l ..< Suc l + kk]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [l..<l + k] = l # [Suc l..<Suc l + kk]
[PROOF STEP]
unfolding k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [l..<l + Suc kk] = l # [Suc l..<Suc l + kk]
[PROOF STEP]
by (simp add: upt_rec)
[PROOF STATE]
proof (state)
this:
[l..<l + k] = l # [Suc l..<Suc l + kk]

goal (3 subgoals):
 1. \<And>xi xj p_ij xsi xsj p_sisj rest l k. \<lbrakk>\<And>l k. (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge ((xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]; (xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 3. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
unfolding neville_aitken_merge.simps IH id4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x l, x (l + Suc j), local.neville_aitken_main l (l + Suc j)) # map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [Suc l..<Suc l + kk] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
unfolding id5
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x l, x (l + Suc j), local.neville_aitken_main l (l + Suc j)) # map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [Suc l..<Suc l + kk] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) (l # [Suc l..<Suc l + kk])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.neville_aitken_merge ((xi, xj, p_ij) # (xsi, xsj, p_sisj) # rest) = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]

goal (2 subgoals):
 1. \<And>uu_ l k. [uu_] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [uu_] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
 2. \<And>l k. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_merge [] = map (\<lambda>i. (x i, x (i + Suc j), local.neville_aitken_main i (i + Suc j))) [l..<l + k]
[PROOF STEP]
qed auto


[STATEMENT]
lemma neville_aitken_impl_main:
  "xs = map (\<lambda> i. (x i, x (i + j), neville_aitken_main i (i + j)))  [l ..< Suc (l + k)]
   \<Longrightarrow> neville_aitken_impl_main xs = neville_aitken_main l (l + j + k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main xs = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
proof (induct xs arbitrary: l k j rule: neville_aitken_impl_main.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e1 e2 es l k j. \<lbrakk>\<And>l k j. local.neville_aitken_merge (e1 # e2 # es) = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main (local.neville_aitken_merge (e1 # e2 # es)) = local.neville_aitken_main l (l + j + k); e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_impl_main (e1 # e2 # es) = local.neville_aitken_main l (l + j + k)
 2. \<And>uu_ uv_ p l k j. [(uu_, uv_, p)] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [(uu_, uv_, p)] = local.neville_aitken_main l (l + j + k)
 3. \<And>l k j. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [] = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
case (1 e1 e2 es l k j)
[PROOF STATE]
proof (state)
this:
local.neville_aitken_merge (e1 # e2 # es) = map (\<lambda>i. (x i, x (i + ?j), local.neville_aitken_main i (i + ?j))) [?l..<Suc (?l + ?k)] \<Longrightarrow> local.neville_aitken_impl_main (local.neville_aitken_merge (e1 # e2 # es)) = local.neville_aitken_main ?l (?l + ?j + ?k)
e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]

goal (3 subgoals):
 1. \<And>e1 e2 es l k j. \<lbrakk>\<And>l k j. local.neville_aitken_merge (e1 # e2 # es) = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main (local.neville_aitken_merge (e1 # e2 # es)) = local.neville_aitken_main l (l + j + k); e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_impl_main (e1 # e2 # es) = local.neville_aitken_main l (l + j + k)
 2. \<And>uu_ uv_ p l k j. [(uu_, uv_, p)] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [(uu_, uv_, p)] = local.neville_aitken_main l (l + j + k)
 3. \<And>l k j. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [] = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
note res = 1(2)
[PROOF STATE]
proof (state)
this:
e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]

goal (3 subgoals):
 1. \<And>e1 e2 es l k j. \<lbrakk>\<And>l k j. local.neville_aitken_merge (e1 # e2 # es) = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main (local.neville_aitken_merge (e1 # e2 # es)) = local.neville_aitken_main l (l + j + k); e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_impl_main (e1 # e2 # es) = local.neville_aitken_main l (l + j + k)
 2. \<And>uu_ uv_ p l k j. [(uu_, uv_, p)] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [(uu_, uv_, p)] = local.neville_aitken_main l (l + j + k)
 3. \<And>l k j. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [] = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
from res
[PROOF STATE]
proof (chain)
picking this:
e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]
[PROOF STEP]
obtain kk where k: "k = Suc kk"
[PROOF STATE]
proof (prove)
using this:
e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]

goal (1 subgoal):
 1. (\<And>kk. k = Suc kk \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases k, auto)
[PROOF STATE]
proof (state)
this:
k = Suc kk

goal (3 subgoals):
 1. \<And>e1 e2 es l k j. \<lbrakk>\<And>l k j. local.neville_aitken_merge (e1 # e2 # es) = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main (local.neville_aitken_merge (e1 # e2 # es)) = local.neville_aitken_main l (l + j + k); e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_impl_main (e1 # e2 # es) = local.neville_aitken_main l (l + j + k)
 2. \<And>uu_ uv_ p l k j. [(uu_, uv_, p)] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [(uu_, uv_, p)] = local.neville_aitken_main l (l + j + k)
 3. \<And>l k j. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [] = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
hence id1: "l + k = Suc (l + kk)"
[PROOF STATE]
proof (prove)
using this:
k = Suc kk

goal (1 subgoal):
 1. l + k = Suc (l + kk)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l + k = Suc (l + kk)

goal (3 subgoals):
 1. \<And>e1 e2 es l k j. \<lbrakk>\<And>l k j. local.neville_aitken_merge (e1 # e2 # es) = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main (local.neville_aitken_merge (e1 # e2 # es)) = local.neville_aitken_main l (l + j + k); e1 # e2 # es = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)]\<rbrakk> \<Longrightarrow> local.neville_aitken_impl_main (e1 # e2 # es) = local.neville_aitken_main l (l + j + k)
 2. \<And>uu_ uv_ p l k j. [(uu_, uv_, p)] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [(uu_, uv_, p)] = local.neville_aitken_main l (l + j + k)
 3. \<And>l k j. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [] = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.neville_aitken_impl_main (e1 # e2 # es) = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
unfolding neville_aitken_impl_main.simps 1(1)[OF neville_aitken_merge[OF 1(2), unfolded id1]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.neville_aitken_main l (l + Suc j + kk) = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
by (simp add: k)
[PROOF STATE]
proof (state)
this:
local.neville_aitken_impl_main (e1 # e2 # es) = local.neville_aitken_main l (l + j + k)

goal (2 subgoals):
 1. \<And>uu_ uv_ p l k j. [(uu_, uv_, p)] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [(uu_, uv_, p)] = local.neville_aitken_main l (l + j + k)
 2. \<And>l k j. [] = map (\<lambda>i. (x i, x (i + j), local.neville_aitken_main i (i + j))) [l..<Suc (l + k)] \<Longrightarrow> local.neville_aitken_impl_main [] = local.neville_aitken_main l (l + j + k)
[PROOF STEP]
qed auto


[STATEMENT]
lemma neville_aitken_impl:
  "xs = map (\<lambda> i. (x i, x i, [:f i:]))  [0 ..< Suc k]
   \<Longrightarrow> neville_aitken_impl_main xs = neville_aitken k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = map (\<lambda>i. (x i, x i, [:f i:])) [0..<Suc k] \<Longrightarrow> local.neville_aitken_impl_main xs = local.neville_aitken k
[PROOF STEP]
unfolding neville_aitken_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = map (\<lambda>i. (x i, x i, [:f i:])) [0..<Suc k] \<Longrightarrow> local.neville_aitken_impl_main xs = local.neville_aitken_main 0 k
[PROOF STEP]
using neville_aitken_impl_main[of xs 0 0 k]
[PROOF STATE]
proof (prove)
using this:
xs = map (\<lambda>i. (x i, x (i + 0), local.neville_aitken_main i (i + 0))) [0..<Suc (0 + k)] \<Longrightarrow> local.neville_aitken_impl_main xs = local.neville_aitken_main 0 (0 + 0 + k)

goal (1 subgoal):
 1. xs = map (\<lambda>i. (x i, x i, [:f i:])) [0..<Suc k] \<Longrightarrow> local.neville_aitken_impl_main xs = local.neville_aitken_main 0 k
[PROOF STEP]
by (simp add: neville_aitken_main.simps)


[STATEMENT]
lemma neville_aitken: assumes "\<And> i j. i < j \<Longrightarrow> j \<le> n \<Longrightarrow> x i \<noteq> x j"
  shows "j \<le> n \<Longrightarrow> poly (neville_aitken x f n) (x j) = (f j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> n \<Longrightarrow> poly (neville_aitken x f n) (x j) = f j
[PROOF STEP]
unfolding neville_aitken_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> n \<Longrightarrow> poly (neville_aitken_main x f 0 n) (x j) = f j
[PROOF STEP]
by (rule neville_aitken_main[OF assms, of n], auto)


[STATEMENT]
lemma neville_aitken_interpolation_impl: assumes "x_fs \<noteq> []"
  shows "neville_aitken_interpolation_poly x_fs =
  neville_aitken (\<lambda> i. fst (x_fs ! i)) (\<lambda> i. snd (x_fs ! i)) (length x_fs - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neville_aitken_interpolation_poly x_fs = neville_aitken (\<lambda>i. fst (x_fs ! i)) (\<lambda>i. snd (x_fs ! i)) (length x_fs - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. neville_aitken_interpolation_poly x_fs = neville_aitken (\<lambda>i. fst (x_fs ! i)) (\<lambda>i. snd (x_fs ! i)) (length x_fs - 1)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x_fs \<noteq> []
[PROOF STEP]
have id: "Suc (length x_fs - 1) = length x_fs"
[PROOF STATE]
proof (prove)
using this:
x_fs \<noteq> []

goal (1 subgoal):
 1. Suc (length x_fs - 1) = length x_fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (length x_fs - 1) = length x_fs

goal (1 subgoal):
 1. neville_aitken_interpolation_poly x_fs = neville_aitken (\<lambda>i. fst (x_fs ! i)) (\<lambda>i. snd (x_fs ! i)) (length x_fs - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neville_aitken_interpolation_poly x_fs = neville_aitken (\<lambda>i. fst (x_fs ! i)) (\<lambda>i. snd (x_fs ! i)) (length x_fs - 1)
[PROOF STEP]
unfolding neville_aitken_interpolation_poly_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neville_aitken_impl_main (map (\<lambda>(xi, fi). (xi, xi, [:fi:])) x_fs) = neville_aitken (\<lambda>i. fst (x_fs ! i)) (\<lambda>i. snd (x_fs ! i)) (length x_fs - 1)
[PROOF STEP]
by (rule neville_aitken_impl, unfold id, rule nth_equalityI, auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
neville_aitken_interpolation_poly x_fs = neville_aitken (\<lambda>i. fst (x_fs ! i)) (\<lambda>i. snd (x_fs ! i)) (length x_fs - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma neville_aitken_interpolation_poly: assumes dist: "distinct (map fst xs_ys)"
  and p: "p = neville_aitken_interpolation_poly xs_ys"
  and xy: "(x,y) \<in> set xs_ys"
  shows "poly p x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly p x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly p x = y
[PROOF STEP]
have p: "p = neville_aitken (\<lambda> i. fst (xs_ys ! i)) (\<lambda> i. snd (xs_ys ! i)) (length xs_ys - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = neville_aitken (\<lambda>i. fst (xs_ys ! i)) (\<lambda>i. snd (xs_ys ! i)) (length xs_ys - 1)
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neville_aitken_interpolation_poly xs_ys = neville_aitken (\<lambda>i. fst (xs_ys ! i)) (\<lambda>i. snd (xs_ys ! i)) (length xs_ys - 1)
[PROOF STEP]
by (rule neville_aitken_interpolation_impl, insert xy, auto)
[PROOF STATE]
proof (state)
this:
p = neville_aitken (\<lambda>i. fst (xs_ys ! i)) (\<lambda>i. snd (xs_ys ! i)) (length xs_ys - 1)

goal (1 subgoal):
 1. poly p x = y
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> set xs_ys
[PROOF STEP]
obtain i where i: "i < length xs_ys" and x: "x = fst (xs_ys ! i)" and y: "y = snd (xs_ys ! i)"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> set xs_ys

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length xs_ys; x = fst (xs_ys ! i); y = snd (xs_ys ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {xs_ys ! i |i. i < length xs_ys}

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length xs_ys; x = fst (xs_ys ! i); y = snd (xs_ys ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis fst_conv in_set_conv_nth snd_conv xy)
[PROOF STATE]
proof (state)
this:
i < length xs_ys
x = fst (xs_ys ! i)
y = snd (xs_ys ! i)

goal (1 subgoal):
 1. poly p x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly p x = y
[PROOF STEP]
unfolding p x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (neville_aitken (\<lambda>i. fst (xs_ys ! i)) (\<lambda>i. snd (xs_ys ! i)) (length xs_ys - 1)) (fst (xs_ys ! i)) = snd (xs_ys ! i)
[PROOF STEP]
proof (rule neville_aitken)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < j; j \<le> length xs_ys - 1\<rbrakk> \<Longrightarrow> fst (xs_ys ! i) \<noteq> fst (xs_ys ! j)
 2. i \<le> length xs_ys - 1
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < j; j \<le> length xs_ys - 1\<rbrakk> \<Longrightarrow> fst (xs_ys ! i) \<noteq> fst (xs_ys ! j)
 2. i__ \<le> length xs_ys - 1
[PROOF STEP]
show "i < j \<Longrightarrow> j \<le> length xs_ys - 1 \<Longrightarrow> fst (xs_ys ! i) \<noteq> fst (xs_ys ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j \<le> length xs_ys - 1\<rbrakk> \<Longrightarrow> fst (xs_ys ! i) \<noteq> fst (xs_ys ! j)
[PROOF STEP]
using dist
[PROOF STATE]
proof (prove)
using this:
distinct (map fst xs_ys)

goal (1 subgoal):
 1. \<lbrakk>i < j; j \<le> length xs_ys - 1\<rbrakk> \<Longrightarrow> fst (xs_ys ! i) \<noteq> fst (xs_ys ! j)
[PROOF STEP]
by (metis (mono_tags, lifting) One_nat_def diff_less dual_order.strict_trans2 length_map
        length_pos_if_in_set lessI less_or_eq_imp_le neq_iff nth_eq_iff_index_eq nth_map xy)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < j; j \<le> length xs_ys - 1\<rbrakk> \<Longrightarrow> fst (xs_ys ! i) \<noteq> fst (xs_ys ! j)

goal (1 subgoal):
 1. i__ \<le> length xs_ys - 1
[PROOF STEP]
qed (insert i, auto)
[PROOF STATE]
proof (state)
this:
poly p x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_neville_aitken_interpolation_poly:
  shows "degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
proof (cases "length xs_ys")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs_ys = 0 \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
 2. \<And>nat. length xs_ys = Suc nat \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
length xs_ys = 0

goal (2 subgoals):
 1. length xs_ys = 0 \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
 2. \<And>nat. length xs_ys = Suc nat \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
hence id: "xs_ys = []"
[PROOF STATE]
proof (prove)
using this:
length xs_ys = 0

goal (1 subgoal):
 1. xs_ys = []
[PROOF STEP]
by (cases xs_ys, auto)
[PROOF STATE]
proof (state)
this:
xs_ys = []

goal (2 subgoals):
 1. length xs_ys = 0 \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
 2. \<And>nat. length xs_ys = Suc nat \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
unfolding id neville_aitken_interpolation_poly_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (neville_aitken_impl_main (map (\<lambda>(xi, fi). (xi, xi, [:fi:])) [])) \<le> length [] - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1

goal (1 subgoal):
 1. \<And>nat. length xs_ys = Suc nat \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. length xs_ys = Suc nat \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
case (Suc nn)
[PROOF STATE]
proof (state)
this:
length xs_ys = Suc nn

goal (1 subgoal):
 1. \<And>nat. length xs_ys = Suc nat \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
have id: "neville_aitken_interpolation_poly xs_ys =
    neville_aitken (\<lambda> i. fst (xs_ys ! i)) (\<lambda> i. snd (xs_ys ! i)) (length xs_ys - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neville_aitken_interpolation_poly xs_ys = neville_aitken (\<lambda>i. fst (xs_ys ! i)) (\<lambda>i. snd (xs_ys ! i)) (length xs_ys - 1)
[PROOF STEP]
by (rule neville_aitken_interpolation_impl, insert Suc, auto)
[PROOF STATE]
proof (state)
this:
neville_aitken_interpolation_poly xs_ys = neville_aitken (\<lambda>i. fst (xs_ys ! i)) (\<lambda>i. snd (xs_ys ! i)) (length xs_ys - 1)

goal (1 subgoal):
 1. \<And>nat. length xs_ys = Suc nat \<Longrightarrow> degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (neville_aitken (\<lambda>i. fst (xs_ys ! i)) (\<lambda>i. snd (xs_ys ! i)) (length xs_ys - 1)) \<le> length xs_ys - 1
[PROOF STEP]
by (rule degree_neville_aitken)
[PROOF STATE]
proof (state)
this:
degree (neville_aitken_interpolation_poly xs_ys) \<le> length xs_ys - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_fst_append1:
  assumes "\<forall>i \<in> set (map fst xs). P i"
    and "P x"
  shows "\<forall>i \<in> set (map fst (xs @ [(x, y)])). P i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(x, y)])). P i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (map fst xs). P i
P x

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(x, y)])). P i
[PROOF STEP]
by (induction xs, auto)