[STATEMENT]
lemma of_nat_ge_zero[intro!]: "of_nat n \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> of_nat n
[PROOF STEP]
using add_right_mono[of _ _ 1]
[PROOF STATE]
proof (prove)
using this:
?a \<le> ?b \<Longrightarrow> ?a + (1::'a) \<le> ?b + (1::'a)

goal (1 subgoal):
 1. (0::'a) \<le> of_nat n
[PROOF STEP]
by (induct n, auto)


[STATEMENT]
lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> a \<Longrightarrow> (0::'a) \<le> a ^ n
[PROOF STEP]
by (induct n) simp_all


[STATEMENT]
lemma power_mono: "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; (0::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> b ^ n
[PROOF STEP]
by (induct n) (auto intro: mult_mono order_trans [of 0 a b])


[STATEMENT]
lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> a \<Longrightarrow> (1::'a) \<le> a ^ n
[PROOF STEP]
using power_mono [of 1 a n]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(1::'a) \<le> a; (0::'a) \<le> (1::'a)\<rbrakk> \<Longrightarrow> (1::'a) ^ n \<le> a ^ n

goal (1 subgoal):
 1. (1::'a) \<le> a \<Longrightarrow> (1::'a) \<le> a ^ n
[PROOF STEP]
by simp


[STATEMENT]
lemma power_le_one: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ n \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ n \<le> (1::'a)
[PROOF STEP]
using power_mono [of a 1 n]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> (1::'a); (0::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> (1::'a) ^ n

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ n \<le> (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma power_gt1_lemma:
  assumes gt1: "1 < a"
  shows "1 < a * a ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) < a * a ^ n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a * a ^ n
[PROOF STEP]
from gt1
[PROOF STATE]
proof (chain)
picking this:
(1::'a) < a
[PROOF STEP]
have "0 \<le> a"
[PROOF STATE]
proof (prove)
using this:
(1::'a) < a

goal (1 subgoal):
 1. (0::'a) \<le> a
[PROOF STEP]
by (fact order_trans [OF zero_le_one less_imp_le])
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a

goal (1 subgoal):
 1. (1::'a) < a * a ^ n
[PROOF STEP]
from gt1
[PROOF STATE]
proof (chain)
picking this:
(1::'a) < a
[PROOF STEP]
have "1 * 1 < a * 1"
[PROOF STATE]
proof (prove)
using this:
(1::'a) < a

goal (1 subgoal):
 1. (1::'a) * (1::'a) < a * (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1::'a) * (1::'a) < a * (1::'a)

goal (1 subgoal):
 1. (1::'a) < a * a ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::'a) * (1::'a) < a * (1::'a)

goal (1 subgoal):
 1. (1::'a) < a * a ^ n
[PROOF STEP]
from gt1
[PROOF STATE]
proof (chain)
picking this:
(1::'a) < a
[PROOF STEP]
have "\<dots> \<le> a * a ^ n"
[PROOF STATE]
proof (prove)
using this:
(1::'a) < a

goal (1 subgoal):
 1. a * (1::'a) \<le> a * a ^ n
[PROOF STEP]
by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le zero_le_one order_refl)
[PROOF STATE]
proof (state)
this:
a * (1::'a) \<le> a * a ^ n

goal (1 subgoal):
 1. (1::'a) < a * a ^ n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1::'a) * (1::'a) < a * a ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(1::'a) * (1::'a) < a * a ^ n

goal (1 subgoal):
 1. (1::'a) < a * a ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1::'a) < a * a ^ n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_gt1: "1 < a \<Longrightarrow> 1 < a ^ Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) < a \<Longrightarrow> (1::'a) < a ^ Suc n
[PROOF STEP]
by (simp add: power_gt1_lemma)


[STATEMENT]
lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(1::'a) < a; 0 < n\<rbrakk> \<Longrightarrow> (1::'a) < a ^ n
[PROOF STEP]
by (cases n) (simp_all add: power_gt1_lemma)


[STATEMENT]
lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N
[PROOF STEP]
proof (induction N)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n \<le> 0; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ 0
 2. \<And>N. \<lbrakk>\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N; n \<le> Suc N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ Suc N
[PROOF STEP]
case (Suc N)
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N
n \<le> Suc N
(1::'a) \<le> a

goal (2 subgoals):
 1. \<lbrakk>n \<le> 0; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ 0
 2. \<And>N. \<lbrakk>\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N; n \<le> Suc N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ Suc N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N
n \<le> Suc N
(1::'a) \<le> a
[PROOF STEP]
have "1 * a^n \<le> a * a^N" if "n \<le> N"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N
n \<le> Suc N
(1::'a) \<le> a

goal (1 subgoal):
 1. (1::'a) * a ^ n \<le> a * a ^ N
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N
n \<le> Suc N
(1::'a) \<le> a
n \<le> N

goal (1 subgoal):
 1. (1::'a) * a ^ n \<le> a * a ^ N
[PROOF STEP]
by (intro mult_mono) (auto simp add: order_trans[OF zero_le_one])
[PROOF STATE]
proof (state)
this:
n \<le> N \<Longrightarrow> (1::'a) * a ^ n \<le> a * a ^ N

goal (2 subgoals):
 1. \<lbrakk>n \<le> 0; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ 0
 2. \<And>N. \<lbrakk>\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N; n \<le> Suc N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ Suc N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> N \<Longrightarrow> (1::'a) * a ^ n \<le> a * a ^ N
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> N \<Longrightarrow> (1::'a) * a ^ n \<le> a * a ^ N

goal (1 subgoal):
 1. a ^ n \<le> a ^ Suc N
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
n \<le> N \<Longrightarrow> (1::'a) * a ^ n \<le> a * a ^ N
\<lbrakk>n \<le> N; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ N
n \<le> Suc N
(1::'a) \<le> a

goal (1 subgoal):
 1. a ^ n \<le> a ^ Suc N
[PROOF STEP]
by (auto simp add: le_Suc_eq)
[PROOF STATE]
proof (state)
this:
a ^ n \<le> a ^ Suc N

goal (1 subgoal):
 1. \<lbrakk>n \<le> 0; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> a ^ 0
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ Suc n \<le> a
[PROOF STEP]
using power_decreasing [of 1 "Suc n" a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 \<le> Suc n; (0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ Suc n \<le> a ^ 1

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> a ^ Suc n \<le> a
[PROOF STEP]
by simp


[STATEMENT]
lemma prod_list_nonneg: "(\<And> x. (x :: 'a :: ordered_semiring_1) \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> prod_list xs \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> set xs \<Longrightarrow> (0::'a) \<le> x) \<Longrightarrow> (0::'a) \<le> prod_list xs
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma log_prod: assumes "0 < a" "a \<noteq> 1" "\<And> x. x \<in> X \<Longrightarrow> 0 < f x"
  shows "log a (prod f X) = sum (log a o f) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log a (prod f X) = sum (log a \<circ> f) X
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
?x \<in> X \<Longrightarrow> 0 < f ?x

goal (1 subgoal):
 1. log a (prod f X) = sum (log a \<circ> f) X
[PROOF STEP]
proof (induct X rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> 0 < f x\<rbrakk> \<Longrightarrow> log a (prod f A) = sum (log a \<circ> f) A
 2. (\<And>x. x \<in> {} \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f {}) = sum (log a \<circ> f) {}
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F; \<And>xa. xa \<in> insert x F \<Longrightarrow> 0 < f xa\<rbrakk> \<Longrightarrow> log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F
?x \<in> insert x F \<Longrightarrow> 0 < f ?x

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> 0 < f x\<rbrakk> \<Longrightarrow> log a (prod f A) = sum (log a \<circ> f) A
 2. (\<And>x. x \<in> {} \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f {}) = sum (log a \<circ> f) {}
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F; \<And>xa. xa \<in> insert x F \<Longrightarrow> 0 < f xa\<rbrakk> \<Longrightarrow> log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)
[PROOF STEP]
have "log a (prod f (insert x F)) = log a (f x * prod f F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log a (prod f (insert x F)) = log a (f x * prod f F)
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F
?x \<in> insert x F \<Longrightarrow> 0 < f ?x

goal (1 subgoal):
 1. log a (prod f (insert x F)) = log a (f x * prod f F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
log a (prod f (insert x F)) = log a (f x * prod f F)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> 0 < f x\<rbrakk> \<Longrightarrow> log a (prod f A) = sum (log a \<circ> f) A
 2. (\<And>x. x \<in> {} \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f {}) = sum (log a \<circ> f) {}
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F; \<And>xa. xa \<in> insert x F \<Longrightarrow> 0 < f xa\<rbrakk> \<Longrightarrow> log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
log a (prod f (insert x F)) = log a (f x * prod f F)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> 0 < f x\<rbrakk> \<Longrightarrow> log a (prod f A) = sum (log a \<circ> f) A
 2. (\<And>x. x \<in> {} \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f {}) = sum (log a \<circ> f) {}
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F; \<And>xa. xa \<in> insert x F \<Longrightarrow> 0 < f xa\<rbrakk> \<Longrightarrow> log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)
[PROOF STEP]
have "\<dots> = log a (f x) + log a (prod f F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log a (f x * prod f F) = log a (f x) + log a (prod f F)
[PROOF STEP]
by (rule log_mult[OF assms(1-2) insert(4) prod_pos], insert insert, auto)
[PROOF STATE]
proof (state)
this:
log a (f x * prod f F) = log a (f x) + log a (prod f F)

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> 0 < f x\<rbrakk> \<Longrightarrow> log a (prod f A) = sum (log a \<circ> f) A
 2. (\<And>x. x \<in> {} \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f {}) = sum (log a \<circ> f) {}
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F; \<And>xa. xa \<in> insert x F \<Longrightarrow> 0 < f xa\<rbrakk> \<Longrightarrow> log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
log a (prod f (insert x F)) = log a (f x) + log a (prod f F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
log a (prod f (insert x F)) = log a (f x) + log a (prod f F)

goal (1 subgoal):
 1. log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
log a (prod f (insert x F)) = log a (f x) + log a (prod f F)
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f F) = sum (log a \<circ> f) F
?x \<in> insert x F \<Longrightarrow> 0 < f ?x

goal (1 subgoal):
 1. log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
log a (prod f (insert x F)) = sum (log a \<circ> f) (insert x F)

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> 0 < f x\<rbrakk> \<Longrightarrow> log a (prod f A) = sum (log a \<circ> f) A
 2. (\<And>x. x \<in> {} \<Longrightarrow> 0 < f x) \<Longrightarrow> log a (prod f {}) = sum (log a \<circ> f) {}
[PROOF STEP]
qed auto


[STATEMENT]
lemma less_1_mult':
  fixes a::"'a::linordered_semidom"
  shows "1 < a \<Longrightarrow> 1 \<le> b \<Longrightarrow> 1 < a * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(1::'a) < a; (1::'a) \<le> b\<rbrakk> \<Longrightarrow> (1::'a) < a * b
[PROOF STEP]
by (metis le_less less_1_mult mult.right_neutral)


[STATEMENT]
lemma upt_minus_eq_append: "i\<le>j \<Longrightarrow> i\<le>j-k \<Longrightarrow> [i..<j] = [i..<j-k] @ [j-k..<j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; i \<le> j - k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - k] @ [j - k..<j]
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<le> j; i \<le> j - 0\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - 0] @ [j - 0..<j]
 2. \<And>k. \<lbrakk>\<lbrakk>i \<le> j; i \<le> j - k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - k] @ [j - k..<j]; i \<le> j; i \<le> j - Suc k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - Suc k] @ [j - Suc k..<j]
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<le> j; i \<le> j - k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - k] @ [j - k..<j]
i \<le> j
i \<le> j - Suc k

goal (2 subgoals):
 1. \<lbrakk>i \<le> j; i \<le> j - 0\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - 0] @ [j - 0..<j]
 2. \<And>k. \<lbrakk>\<lbrakk>i \<le> j; i \<le> j - k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - k] @ [j - k..<j]; i \<le> j; i \<le> j - Suc k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - Suc k] @ [j - Suc k..<j]
[PROOF STEP]
have hyp: "[i..<j] = [i..<j - k] @ [j - k..<j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i..<j] = [i..<j - k] @ [j - k..<j]
[PROOF STEP]
using Suc.hyps Suc.prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<le> j; i \<le> j - k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - k] @ [j - k..<j]
i \<le> j
i \<le> j - Suc k

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

goal (2 subgoals):
 1. \<lbrakk>i \<le> j; i \<le> j - 0\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - 0] @ [j - 0..<j]
 2. \<And>k. \<lbrakk>\<lbrakk>i \<le> j; i \<le> j - k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - k] @ [j - k..<j]; i \<le> j; i \<le> j - Suc k\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - Suc k] @ [j - Suc k..<j]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[i..<j] = [i..<j - k] @ [j - k..<j]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[i..<j] = [i..<j - k] @ [j - k..<j]

goal (1 subgoal):
 1. [i..<j] = [i..<j - Suc k] @ [j - Suc k..<j]
[PROOF STEP]
by (metis Suc.prems(2) append.simps(1) diff_Suc_less nat_less_le neq0_conv upt_append upt_rec zero_diff)
[PROOF STATE]
proof (state)
this:
[i..<j] = [i..<j - Suc k] @ [j - Suc k..<j]

goal (1 subgoal):
 1. \<lbrakk>i \<le> j; i \<le> j - 0\<rbrakk> \<Longrightarrow> [i..<j] = [i..<j - 0] @ [j - 0..<j]
[PROOF STEP]
qed auto


[STATEMENT]
lemma list_trisect: "x < length lst \<Longrightarrow> [0..<length lst] = [0..<x]@x#[Suc x..<length lst]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < length lst \<Longrightarrow> [0..<length lst] = [0..<x] @ x # [Suc x..<length lst]
[PROOF STEP]
by (induct lst, force, rename_tac a lst, case_tac "x = length lst", auto)


[STATEMENT]
lemma id_imp_bij_betw:
  assumes f: "f : A \<rightarrow> A"
      and ff: "\<And>a. a \<in> A \<Longrightarrow> f (f a) = a"
  shows "bij_betw f A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A A
[PROOF STEP]
by (intro bij_betwI[OF f f], simp_all add: ff)


[STATEMENT]
lemma range_subsetI:
  assumes "\<And>x. f x = g (h x)" shows "range f \<subseteq> range g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> range g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f ?x = g (h ?x)

goal (1 subgoal):
 1. range f \<subseteq> range g
[PROOF STEP]
by auto


[STATEMENT]
lemma Gcd_uminus:
  fixes A::"int set"
  assumes "finite A"
  shows "Gcd A = Gcd (uminus ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gcd A = Gcd (uminus ` A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. Gcd A = Gcd (uminus ` A)
[PROOF STEP]
by (induct A, auto)


[STATEMENT]
lemma aux_abs_int: fixes c :: int
  assumes "c \<noteq> 0"
  shows "\<bar>x\<bar> \<le> \<bar>x * c\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<le> \<bar>x * c\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>x\<bar> \<le> \<bar>x * c\<bar>
[PROOF STEP]
have "abs x = abs x * 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> = \<bar>x\<bar> * 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> = \<bar>x\<bar> * 1

goal (1 subgoal):
 1. \<bar>x\<bar> \<le> \<bar>x * c\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> = \<bar>x\<bar> * 1

goal (1 subgoal):
 1. \<bar>x\<bar> \<le> \<bar>x * c\<bar>
[PROOF STEP]
have "\<dots> \<le> abs x * abs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> * 1 \<le> \<bar>x\<bar> * \<bar>c\<bar>
[PROOF STEP]
by (rule mult_left_mono, insert assms, auto)
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> * 1 \<le> \<bar>x\<bar> * \<bar>c\<bar>

goal (1 subgoal):
 1. \<bar>x\<bar> \<le> \<bar>x * c\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> \<le> \<bar>x\<bar> * \<bar>c\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> \<le> \<bar>x\<bar> * \<bar>c\<bar>

goal (1 subgoal):
 1. \<bar>x\<bar> \<le> \<bar>x * c\<bar>
[PROOF STEP]
unfolding abs_mult
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> \<le> \<bar>x\<bar> * \<bar>c\<bar>

goal (1 subgoal):
 1. \<bar>x\<bar> \<le> \<bar>x\<bar> * \<bar>c\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> \<le> \<bar>x * c\<bar>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mod_0_abs_less_imp_0:
  fixes a::int
  assumes a1: "[a = 0] (mod m)"
  and a2: "abs(a)<m"
  shows "a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = 0
[PROOF STEP]
have "m\<ge>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> m
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[a = 0] (mod m)
\<bar>a\<bar> < m

goal (1 subgoal):
 1. 0 \<le> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> m

goal (1 subgoal):
 1. a = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> m

goal (1 subgoal):
 1. a = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> m
[a = 0] (mod m)
\<bar>a\<bar> < m

goal (1 subgoal):
 1. a = 0
[PROOF STEP]
unfolding cong_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> m
a mod m = 0 mod m
\<bar>a\<bar> < m

goal (1 subgoal):
 1. a = 0
[PROOF STEP]
using int_mod_pos_eq large_mod_0 zless_imp_add1_zle
[PROOF STATE]
proof (prove)
using this:
0 \<le> m
a mod m = 0 mod m
\<bar>a\<bar> < m
\<lbrakk>?a = ?b * ?q + ?r; 0 \<le> ?r; ?r < ?b\<rbrakk> \<Longrightarrow> ?a mod ?b = ?r
\<lbrakk>1 < ?n; \<bar>?k\<bar> < ?n; ?k mod ?n = 0\<rbrakk> \<Longrightarrow> ?k = 0
?w < ?z \<Longrightarrow> ?w + 1 \<le> ?z

goal (1 subgoal):
 1. a = 0
[PROOF STEP]
by (metis abs_of_nonneg le_less not_less zabs_less_one_iff zmod_trivial_iff)
[PROOF STATE]
proof (state)
this:
a = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_list_zero:
  assumes "set xs \<subseteq> {0}" shows "sum_list xs = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list xs = (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> {0::'a}

goal (1 subgoal):
 1. sum_list xs = (0::'a)
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma max_idem [simp]: shows "max a a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max a a = a
[PROOF STEP]
by (simp add: max_def)


[STATEMENT]
lemma hom_max:
  assumes "a \<le> b \<longleftrightarrow> f a \<le> f b"
  shows "f (max a b) = max (f a) (f b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (max a b) = max (f a) (f b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(a \<le> b) = (f a \<le> f b)

goal (1 subgoal):
 1. f (max a b) = max (f a) (f b)
[PROOF STEP]
by (auto simp: max_def)


[STATEMENT]
lemma le_max_self:
  fixes a b :: "'a :: preorder"
  assumes "a \<le> b \<or> b \<le> a" shows "a \<le> max a b" and "b \<le> max a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> max a b &&& b \<le> max a b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<le> b \<or> b \<le> a

goal (1 subgoal):
 1. a \<le> max a b &&& b \<le> max a b
[PROOF STEP]
by (auto simp: max_def)


[STATEMENT]
lemma le_max:
  fixes a b :: "'a :: preorder"
  assumes "c \<le> a \<or> c \<le> b" and "a \<le> b \<or> b \<le> a" shows "c \<le> max a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<le> max a b
[PROOF STEP]
using assms(1) le_max_self[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
c \<le> a \<or> c \<le> b
a \<le> max a b
b \<le> max a b

goal (1 subgoal):
 1. c \<le> max a b
[PROOF STEP]
by (auto dest: order_trans)


[STATEMENT]
lemma max_list_Cons: "max_list (x#xs) = (if xs = [] then x else max x (max_list xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Missing_Lemmas.max_list (x # xs) = (if xs = [] then x else max x (Missing_Lemmas.max_list xs))
[PROOF STEP]
by (cases xs, auto)


[STATEMENT]
lemma max_list_mem: "xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs \<in> set xs
[PROOF STEP]
by (induct xs, auto simp: max_list_Cons max_def)


[STATEMENT]
lemma mem_set_imp_le_max_list:
  fixes xs :: "'a :: preorder list"
  assumes "\<And>a b. a \<in> set xs \<Longrightarrow> b \<in> set xs \<Longrightarrow> a \<le> b \<or> b \<le> a"
      and "a \<in> set xs"
  shows "a \<le> max_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
proof (insert assms, induct xs arbitrary:a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>a b. \<lbrakk>a \<in> set []; b \<in> set []\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; a \<in> set []\<rbrakk> \<Longrightarrow> a \<le> Missing_Lemmas.max_list []
 2. \<And>a xs aa. \<lbrakk>\<And>a. \<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; a \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> Missing_Lemmas.max_list xs; \<And>aa b. \<lbrakk>aa \<in> set (a # xs); b \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> b \<or> b \<le> aa; aa \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> Missing_Lemmas.max_list (a # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> set []; ?b \<in> set []\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set []

goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>a b. \<lbrakk>a \<in> set []; b \<in> set []\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; a \<in> set []\<rbrakk> \<Longrightarrow> a \<le> Missing_Lemmas.max_list []
 2. \<And>a xs aa. \<lbrakk>\<And>a. \<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; a \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> Missing_Lemmas.max_list xs; \<And>aa b. \<lbrakk>aa \<in> set (a # xs); b \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> b \<or> b \<le> aa; aa \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> Missing_Lemmas.max_list (a # xs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a \<in> set xs; ?b \<in> set xs\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set xs
\<lbrakk>?a \<in> set []; ?b \<in> set []\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> set xs; ?b \<in> set xs\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set xs
\<lbrakk>?a \<in> set []; ?b \<in> set []\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set []

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> Missing_Lemmas.max_list []

goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. \<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; a \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> Missing_Lemmas.max_list xs; \<And>aa b. \<lbrakk>aa \<in> set (a # xs); b \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> b \<or> b \<le> aa; aa \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> Missing_Lemmas.max_list (a # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. \<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; a \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> Missing_Lemmas.max_list xs; \<And>aa b. \<lbrakk>aa \<in> set (a # xs); b \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> b \<or> b \<le> aa; aa \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> Missing_Lemmas.max_list (a # xs)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; ?a \<in> set xs\<rbrakk> \<Longrightarrow> ?a \<le> Missing_Lemmas.max_list xs
\<lbrakk>?a \<in> set (x # xs); ?b \<in> set (x # xs)\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set (x # xs)

goal (1 subgoal):
 1. \<And>a xs aa. \<lbrakk>\<And>a. \<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; a \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> Missing_Lemmas.max_list xs; \<And>aa b. \<lbrakk>aa \<in> set (a # xs); b \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> b \<or> b \<le> aa; aa \<in> set (a # xs)\<rbrakk> \<Longrightarrow> aa \<le> Missing_Lemmas.max_list (a # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
proof (cases "xs = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
 2. xs \<noteq> [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
 2. xs \<noteq> [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
have "x \<le> max_list xs \<or> max_list xs \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> Missing_Lemmas.max_list xs \<or> Missing_Lemmas.max_list xs \<le> x
[PROOF STEP]
apply (rule Cons(2))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> set (x # xs)
 2. Missing_Lemmas.max_list xs \<in> set (x # xs)
[PROOF STEP]
using max_list_mem[of xs] False
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs \<in> set xs
xs \<noteq> []

goal (2 subgoals):
 1. x \<in> set (x # xs)
 2. Missing_Lemmas.max_list xs \<in> set (x # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<le> Missing_Lemmas.max_list xs \<or> Missing_Lemmas.max_list xs \<le> x

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
 2. xs \<noteq> [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
note 1 = le_max_self[OF this]
[PROOF STATE]
proof (state)
this:
x \<le> max x (Missing_Lemmas.max_list xs)
Missing_Lemmas.max_list xs \<le> max x (Missing_Lemmas.max_list xs)

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
 2. xs \<noteq> [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; ?a \<in> set xs\<rbrakk> \<Longrightarrow> ?a \<le> Missing_Lemmas.max_list xs
\<lbrakk>?a \<in> set (x # xs); ?b \<in> set (x # xs)\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set (x # xs)
[PROOF STEP]
have "a = x \<or> a \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>a b. \<lbrakk>a \<in> set xs; b \<in> set xs\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a; ?a \<in> set xs\<rbrakk> \<Longrightarrow> ?a \<le> Missing_Lemmas.max_list xs
\<lbrakk>?a \<in> set (x # xs); ?b \<in> set (x # xs)\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
a \<in> set (x # xs)

goal (1 subgoal):
 1. a = x \<or> a \<in> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = x \<or> a \<in> set xs

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
 2. xs \<noteq> [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = x \<or> a \<in> set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = x \<or> a \<in> set xs

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = x \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
 2. a \<in> set xs \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
assume a: "a = x"
[PROOF STATE]
proof (state)
this:
a = x

goal (2 subgoals):
 1. a = x \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
 2. a \<in> set xs \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
by (unfold a max_list_Cons, auto simp: False intro!: 1)
[PROOF STATE]
proof (state)
this:
a \<le> Missing_Lemmas.max_list (x # xs)

goal (1 subgoal):
 1. a \<in> set xs \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> set xs \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
assume "a \<in> set xs"
[PROOF STATE]
proof (state)
this:
a \<in> set xs

goal (1 subgoal):
 1. a \<in> set xs \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set xs
[PROOF STEP]
have "a \<le> max_list xs"
[PROOF STATE]
proof (prove)
using this:
a \<in> set xs

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
by (intro Cons, auto)
[PROOF STATE]
proof (state)
this:
a \<le> Missing_Lemmas.max_list xs

goal (1 subgoal):
 1. a \<in> set xs \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
x \<le> max x (Missing_Lemmas.max_list xs)
Missing_Lemmas.max_list xs \<le> max x (Missing_Lemmas.max_list xs)
a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
have "a \<le> max x (max_list xs)"
[PROOF STATE]
proof (prove)
using this:
x \<le> max x (Missing_Lemmas.max_list xs)
Missing_Lemmas.max_list xs \<le> max x (Missing_Lemmas.max_list xs)
a \<le> Missing_Lemmas.max_list xs

goal (1 subgoal):
 1. a \<le> max x (Missing_Lemmas.max_list xs)
[PROOF STEP]
by (auto dest: order_trans)
[PROOF STATE]
proof (state)
this:
a \<le> max x (Missing_Lemmas.max_list xs)

goal (1 subgoal):
 1. a \<in> set xs \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<le> max x (Missing_Lemmas.max_list xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> max x (Missing_Lemmas.max_list xs)

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
by (unfold max_list_Cons, auto simp: False)
[PROOF STATE]
proof (state)
this:
a \<le> Missing_Lemmas.max_list (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a \<le> Missing_Lemmas.max_list (x # xs)

goal (1 subgoal):
 1. xs = [] \<Longrightarrow> a \<le> Missing_Lemmas.max_list (x # xs)
[PROOF STEP]
qed (insert Cons, auto)
[PROOF STATE]
proof (state)
this:
a \<le> Missing_Lemmas.max_list (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_max_list:
  fixes xs :: "'a :: preorder list"
  assumes ord: "\<And>a b. a \<in> set xs \<Longrightarrow> b \<in> set xs \<Longrightarrow> a \<le> b \<or> b \<le> a"
      and ab: "a \<le> b"
      and b: "b \<in> set xs"
  shows "a \<le> max_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
note ab
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
have "b \<le> max_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
by (rule mem_set_imp_le_max_list, fact ord, fact b)
[PROOF STATE]
proof (state)
this:
b \<le> Missing_Lemmas.max_list xs

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> Missing_Lemmas.max_list xs

goal (1 subgoal):
 1. a \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a \<le> Missing_Lemmas.max_list xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_list_le:
  fixes xs :: "'a :: preorder list"
  assumes a: "\<And>x. x \<in> set xs \<Longrightarrow> x \<le> a"
      and xs: "xs \<noteq> []"
  shows "max_list xs \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Missing_Lemmas.max_list xs \<le> a
[PROOF STEP]
using max_list_mem[OF xs] a
[PROOF STATE]
proof (prove)
using this:
Missing_Lemmas.max_list xs \<in> set xs
?x \<in> set xs \<Longrightarrow> ?x \<le> a

goal (1 subgoal):
 1. Missing_Lemmas.max_list xs \<le> a
[PROOF STEP]
by auto


[STATEMENT]
lemma max_list_as_Greatest:
  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> x \<le> y \<or> y \<le> x"
  shows "max_list xs = (GREATEST a. a \<in> set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
proof (cases "xs = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
 2. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
 2. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
by (unfold Greatest_def, auto simp: max_list.simps(1))
[PROOF STATE]
proof (state)
this:
Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> set xs; ?y \<in> set xs\<rbrakk> \<Longrightarrow> ?x \<le> ?y \<or> ?y \<le> ?x
[PROOF STEP]
have 1: "x \<in> set xs \<Longrightarrow> x \<le> max_list xs" for x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set xs; ?y \<in> set xs\<rbrakk> \<Longrightarrow> ?x \<le> ?y \<or> ?y \<le> ?x

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> x \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
by (auto intro: le_max_list)
[PROOF STATE]
proof (state)
this:
?x \<in> set xs \<Longrightarrow> ?x \<le> Missing_Lemmas.max_list xs

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
have 2: "max_list xs \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Missing_Lemmas.max_list xs \<in> set xs
[PROOF STEP]
by (fact max_list_mem[OF False])
[PROOF STATE]
proof (state)
this:
Missing_Lemmas.max_list xs \<in> set xs

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
have "\<exists>!x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)" (is "\<exists>!x. ?P x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)
[PROOF STEP]
proof (intro ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?a \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> ?a)
 2. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = ?a
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set xs \<Longrightarrow> ?x \<le> Missing_Lemmas.max_list xs
Missing_Lemmas.max_list xs \<in> set xs
[PROOF STEP]
show "?P (max_list xs)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> ?x \<le> Missing_Lemmas.max_list xs
Missing_Lemmas.max_list xs \<in> set xs

goal (1 subgoal):
 1. Missing_Lemmas.max_list xs \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> Missing_Lemmas.max_list xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Missing_Lemmas.max_list xs \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> Missing_Lemmas.max_list xs)

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = Missing_Lemmas.max_list xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = Missing_Lemmas.max_list xs
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = Missing_Lemmas.max_list xs
[PROOF STEP]
assume 3: "?P x"
[PROOF STATE]
proof (state)
this:
x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = Missing_Lemmas.max_list xs
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set xs \<Longrightarrow> ?x \<le> Missing_Lemmas.max_list xs
x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)
[PROOF STEP]
have "x \<le> max_list xs"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> ?x \<le> Missing_Lemmas.max_list xs
x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)

goal (1 subgoal):
 1. x \<le> Missing_Lemmas.max_list xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<le> Missing_Lemmas.max_list xs

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = Missing_Lemmas.max_list xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<le> Missing_Lemmas.max_list xs

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = Missing_Lemmas.max_list xs
[PROOF STEP]
from 2 3
[PROOF STATE]
proof (chain)
picking this:
Missing_Lemmas.max_list xs \<in> set xs
x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)
[PROOF STEP]
have "max_list xs \<le> x"
[PROOF STATE]
proof (prove)
using this:
Missing_Lemmas.max_list xs \<in> set xs
x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)

goal (1 subgoal):
 1. Missing_Lemmas.max_list xs \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Missing_Lemmas.max_list xs \<le> x

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x) \<Longrightarrow> x = Missing_Lemmas.max_list xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<le> Missing_Lemmas.max_list xs
Missing_Lemmas.max_list xs \<le> x
[PROOF STEP]
show "x = max_list xs"
[PROOF STATE]
proof (prove)
using this:
x \<le> Missing_Lemmas.max_list xs
Missing_Lemmas.max_list xs \<le> x

goal (1 subgoal):
 1. x = Missing_Lemmas.max_list xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = Missing_Lemmas.max_list xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
note 3 = theI_unique[OF this,symmetric]
[PROOF STATE]
proof (state)
this:
(?x = (THE x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x))) = (?x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> ?x))

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set xs \<Longrightarrow> ?x \<le> Missing_Lemmas.max_list xs
Missing_Lemmas.max_list xs \<in> set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> ?x \<le> Missing_Lemmas.max_list xs
Missing_Lemmas.max_list xs \<in> set xs

goal (1 subgoal):
 1. Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)
[PROOF STEP]
by (unfold Greatest_def Cons 3, auto)
[PROOF STATE]
proof (state)
this:
Missing_Lemmas.max_list xs = (GREATEST a. a \<in> set xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hom_max_list_commute:
  assumes "xs \<noteq> []"
      and "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> h (max x y) = max (h x) (h y)"
  shows "h (max_list xs) = max_list (map h xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h (Missing_Lemmas.max_list xs) = Missing_Lemmas.max_list (map h xs)
[PROOF STEP]
by (insert assms, induct xs, auto simp: max_list_Cons max_list_mem)


[STATEMENT]
lemma upt_aux_rec [code]:
  "rev_upt_aux i j js = (if j\<ge>i then js else rev_upt_aux i (Suc j) (j#js))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev_upt_aux i j js = (if i \<le> j then js else rev_upt_aux i (Suc j) (j # js))
[PROOF STEP]
by (induct j, auto simp add: rev_upt_aux_def rev_upt_rec)


[STATEMENT]
lemma rev_upt_code[code]: "[i>..j] = rev_upt_aux i j []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i>..j] = rev_upt_aux i j []
[PROOF STEP]
by(simp add: rev_upt_aux_def)


[STATEMENT]
lemma upt_rev_upt:
  "rev [j>..i] = [i..<j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [j>..i] = [i..<j]
[PROOF STEP]
by (induct j, auto)


[STATEMENT]
lemma rev_upt_upt:
  "rev [i..<j] = [j>..i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [i..<j] = [j>..i]
[PROOF STEP]
by (induct j, auto)


[STATEMENT]
lemma length_rev_upt [simp]: "length [i>..j] = i - j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [i>..j] = i - j
[PROOF STEP]
by (induct i) (auto simp add: Suc_diff_le)


[STATEMENT]
lemma nth_rev_upt [simp]: "j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
assume jk_i: "j + k < i"
[PROOF STATE]
proof (state)
this:
j + k < i

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
have "[i>..j] = rev [j..<i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i>..j] = rev [j..<i]
[PROOF STEP]
using rev_upt_upt
[PROOF STATE]
proof (prove)
using this:
rev [?i..<?j] = [?j>..?i]

goal (1 subgoal):
 1. [i>..j] = rev [j..<i]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[i>..j] = rev [j..<i]

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[i>..j] = rev [j..<i]

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
have "... ! k = [j..<i] ! (length [j..<i] - 1 - k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [j..<i] ! k = [j..<i] ! (length [j..<i] - 1 - k)
[PROOF STEP]
using jk_i
[PROOF STATE]
proof (prove)
using this:
j + k < i

goal (1 subgoal):
 1. rev [j..<i] ! k = [j..<i] ! (length [j..<i] - 1 - k)
[PROOF STEP]
by (simp add: rev_nth)
[PROOF STATE]
proof (state)
this:
rev [j..<i] ! k = [j..<i] ! (length [j..<i] - 1 - k)

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rev [j..<i] ! k = [j..<i] ! (length [j..<i] - 1 - k)

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
have "... = [j..<i] ! (i - j - 1 - k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [j..<i] ! (length [j..<i] - 1 - k) = [j..<i] ! (i - j - 1 - k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[j..<i] ! (length [j..<i] - 1 - k) = [j..<i] ! (i - j - 1 - k)

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[j..<i] ! (length [j..<i] - 1 - k) = [j..<i] ! (i - j - 1 - k)

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
have "... = j + (i - j - 1 - k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [j..<i] ! (i - j - 1 - k) = j + (i - j - 1 - k)
[PROOF STEP]
by (rule nth_upt, insert jk_i, auto)
[PROOF STATE]
proof (state)
this:
[j..<i] ! (i - j - 1 - k) = j + (i - j - 1 - k)

goal (1 subgoal):
 1. j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[i>..j] ! k = j + (i - j - 1 - k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[i>..j] ! k = j + (i - j - 1 - k)

goal (1 subgoal):
 1. [i>..j] ! k = i - 1 - k
[PROOF STEP]
using jk_i
[PROOF STATE]
proof (prove)
using this:
[i>..j] ! k = j + (i - j - 1 - k)
j + k < i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_map_rev_upt:
  assumes i: "i < m-n"
  shows "(map f [m>..n]) ! i = f (m - 1 - i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f [m>..n] ! i = f (m - 1 - i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map f [m>..n] ! i = f (m - 1 - i)
[PROOF STEP]
have "(map f [m>..n]) ! i = f ([m>..n] ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f [m>..n] ! i = f ([m>..n] ! i)
[PROOF STEP]
by (rule nth_map, auto simp add: i)
[PROOF STATE]
proof (state)
this:
map f [m>..n] ! i = f ([m>..n] ! i)

goal (1 subgoal):
 1. map f [m>..n] ! i = f (m - 1 - i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map f [m>..n] ! i = f ([m>..n] ! i)

goal (1 subgoal):
 1. map f [m>..n] ! i = f (m - 1 - i)
[PROOF STEP]
have "... = f (m - 1 - i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ([m>..n] ! i) = f (m - 1 - i)
[PROOF STEP]
proof (rule arg_cong[of _ _ f], rule nth_rev_upt)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n + i < m
[PROOF STEP]
show "n + i < m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n + i < m
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m - n

goal (1 subgoal):
 1. n + i < m
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
n + i < m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ([m>..n] ! i) = f (m - 1 - i)

goal (1 subgoal):
 1. map f [m>..n] ! i = f (m - 1 - i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map f [m>..n] ! i = f (m - 1 - i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map f [m>..n] ! i = f (m - 1 - i)

goal (1 subgoal):
 1. map f [m>..n] ! i = f (m - 1 - i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map f [m>..n] ! i = f (m - 1 - i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_mult_monom:
 "coeff (p * monom a d) i = (if d \<le> i then a * coeff p (i - d) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * monom a d) i = (if d \<le> i then a * coeff p (i - d) else (0::'a))
[PROOF STEP]
using coeff_monom_mult[of a d p]
[PROOF STATE]
proof (prove)
using this:
coeff (monom a d * p) ?i = (if d \<le> ?i then a * coeff p (?i - d) else (0::'a))

goal (1 subgoal):
 1. coeff (p * monom a d) i = (if d \<le> i then a * coeff p (i - d) else (0::'a))
[PROOF STEP]
by (simp add: ac_simps)


[STATEMENT]
lemma vec_of_poly_0 [simp]: "vec_of_poly 0 = 0\<^sub>v 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly 0 = 0\<^sub>v 1
[PROOF STEP]
by (auto simp: vec_of_poly_def)


[STATEMENT]
lemma vec_index_vec_of_poly [simp]: "i \<le> degree p \<Longrightarrow> vec_of_poly p $ i = coeff p (degree p - i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> degree p \<Longrightarrow> vec_of_poly p $ i = coeff p (degree p - i)
[PROOF STEP]
by (simp add: vec_of_poly_def Let_def)


[STATEMENT]
lemma poly_of_vec_vec: "poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))
[PROOF STEP]
proof (induct n arbitrary:f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. poly_of_vec (vec 0 f) = Poly (rev (map f [0..<0]))
 2. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>f. poly_of_vec (vec 0 f) = Poly (rev (map f [0..<0]))
 2. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (vec 0 f) = Poly (rev (map f [0..<0]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly_of_vec (vec 0 f) = Poly (rev (map f [0..<0]))

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
poly_of_vec (vec n ?f) = Poly (rev (map ?f [0..<n]))

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
have "map f [0..<Suc n] = f 0 # map (f \<circ> Suc) [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f [0..<Suc n] = f 0 # map (f \<circ> Suc) [0..<n]
[PROOF STEP]
by (simp add: map_upt_Suc del: upt_Suc)
[PROOF STATE]
proof (state)
this:
map f [0..<Suc n] = f 0 # map (f \<circ> Suc) [0..<n]

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map f [0..<Suc n] = f 0 # map (f \<circ> Suc) [0..<n]

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
have "Poly (rev \<dots>) = Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Poly (rev (f 0 # map (f \<circ> Suc) [0..<n])) = Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n
[PROOF STEP]
by (simp add: Poly_snoc smult_monom)
[PROOF STATE]
proof (state)
this:
Poly (rev (f 0 # map (f \<circ> Suc) [0..<n])) = Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Poly (rev (f 0 # map (f \<circ> Suc) [0..<n])) = Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
have "\<dots> = poly_of_vec (vec n (f \<circ> Suc)) + monom (f 0) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n = poly_of_vec (vec n (f \<circ> Suc)) + monom (f 0) n
[PROOF STEP]
by (fold Suc, simp)
[PROOF STATE]
proof (state)
this:
Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n = poly_of_vec (vec n (f \<circ> Suc)) + monom (f 0) n

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n = poly_of_vec (vec n (f \<circ> Suc)) + monom (f 0) n

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
have "\<dots> = poly_of_vec (vec (Suc n) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (vec n (f \<circ> Suc)) + monom (f 0) n = poly_of_vec (vec (Suc n) f)
[PROOF STEP]
apply (unfold poly_of_vec_def Let_def dim_vec sum.lessThan_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. monom (vec n (f \<circ> Suc) $ (n - Suc i)) i) + monom (f 0) n = (\<Sum>i<n. monom (vec (Suc n) f $ (Suc n - Suc i)) i) + monom (vec (Suc n) f $ (Suc n - Suc n)) n
[PROOF STEP]
by (auto simp add: Suc_diff_Suc)
[PROOF STATE]
proof (state)
this:
poly_of_vec (vec n (f \<circ> Suc)) + monom (f 0) n = poly_of_vec (vec (Suc n) f)

goal (1 subgoal):
 1. \<And>n f. (\<And>f. poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))) \<Longrightarrow> poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Poly (rev (map f [0..<Suc n])) = poly_of_vec (vec (Suc n) f)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Poly (rev (map f [0..<Suc n])) = poly_of_vec (vec (Suc n) f)

goal (1 subgoal):
 1. poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
poly_of_vec (vec (Suc n) f) = Poly (rev (map f [0..<Suc n]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_list_map_dropWhile0:
  assumes f0: "f 0 = 0"
  shows "sum_list (map f (dropWhile ((=) 0) xs)) = sum_list (map f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map f (dropWhile ((=) (0::'b)) xs)) = sum_list (map f xs)
[PROOF STEP]
by (induct xs, auto simp add: f0)


[STATEMENT]
lemma coeffs_poly_of_vec:
  "coeffs (poly_of_vec v) = rev (dropWhile ((=) 0) (list_of_vec v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeffs (poly_of_vec v) = rev (dropWhile ((=) (0::'a)) (list_of_vec v))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coeffs (poly_of_vec v) = rev (dropWhile ((=) (0::'a)) (list_of_vec v))
[PROOF STEP]
obtain n f where v: "v = vec n f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n f. v = vec n f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by transfer auto
[PROOF STATE]
proof (state)
this:
v = vec n f

goal (1 subgoal):
 1. coeffs (poly_of_vec v) = rev (dropWhile ((=) (0::'a)) (list_of_vec v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeffs (poly_of_vec v) = rev (dropWhile ((=) (0::'a)) (list_of_vec v))
[PROOF STEP]
by (simp add: v poly_of_vec_vec)
[PROOF STATE]
proof (state)
this:
coeffs (poly_of_vec v) = rev (dropWhile ((=) (0::'a)) (list_of_vec v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_of_vec_vCons:
 "poly_of_vec (vCons a v) = monom a (dim_vec v) + poly_of_vec v" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (vCons a v) = monom a (dim_vec v) + poly_of_vec v
[PROOF STEP]
by (auto intro: poly_eqI simp: coeff_poly_of_vec vec_index_vCons)


[STATEMENT]
lemma poly_of_vec_as_Poly: "poly_of_vec v = Poly (rev (list_of_vec v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec v = Poly (rev (list_of_vec v))
[PROOF STEP]
by (induct v, auto simp:poly_of_vec_vCons Poly_snoc ac_simps)


[STATEMENT]
lemma poly_of_vec_add:
  assumes "dim_vec a = dim_vec b"
  shows "poly_of_vec (a + b) = poly_of_vec a + poly_of_vec b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (a + b) = poly_of_vec a + poly_of_vec b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dim_vec a = dim_vec b

goal (1 subgoal):
 1. poly_of_vec (a + b) = poly_of_vec a + poly_of_vec b
[PROOF STEP]
by (auto simp add: poly_eq_iff coeff_poly_of_vec)


[STATEMENT]
lemma degree_poly_of_vec_less:
  assumes "0 < dim_vec v" and "dim_vec v \<le> n" shows "degree (poly_of_vec v) < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (poly_of_vec v) < n
[PROOF STEP]
using degree_poly_of_vec_less assms
[PROOF STATE]
proof (prove)
using this:
0 < dim_vec ?v \<Longrightarrow> degree (poly_of_vec ?v) < dim_vec ?v
0 < dim_vec v
dim_vec v \<le> n

goal (1 subgoal):
 1. degree (poly_of_vec v) < n
[PROOF STEP]
by (auto dest: less_le_trans)


[STATEMENT]
lemma (in vec_module) poly_of_vec_finsum:
  assumes "f \<in> X \<rightarrow> carrier_vec n"
  shows "poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
proof (cases "finite X")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite X \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
 2. infinite X \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite X

goal (2 subgoals):
 1. finite X \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
 2. infinite X \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite X

goal (1 subgoal):
 1. poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))

goal (1 subgoal):
 1. finite X \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite X \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite X

goal (1 subgoal):
 1. finite X \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
[PROOF STEP]
proof (insert True assms, induct X rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f {}) = (\<Sum>i\<in>{}. poly_of_vec (f i))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f F) = (\<Sum>i\<in>F. poly_of_vec (f i)); f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> poly_of_vec (finsum V f (insert x F)) = (\<Sum>i\<in>insert x F. poly_of_vec (f i))
[PROOF STEP]
case IH: (insert a X)
[PROOF STATE]
proof (state)
this:
finite X
a \<notin> X
f \<in> X \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
f \<in> insert a X \<rightarrow> carrier_vec n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f {}) = (\<Sum>i\<in>{}. poly_of_vec (f i))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f F) = (\<Sum>i\<in>F. poly_of_vec (f i)); f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> poly_of_vec (finsum V f (insert x F)) = (\<Sum>i\<in>insert x F. poly_of_vec (f i))
[PROOF STEP]
have [simp]: "f x \<in> carrier_vec n" if x: "x \<in> X" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<in> carrier_vec n
[PROOF STEP]
using x IH.prems
[PROOF STATE]
proof (prove)
using this:
x \<in> X
f \<in> insert a X \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. f x \<in> carrier_vec n
[PROOF STEP]
unfolding Pi_def
[PROOF STATE]
proof (prove)
using this:
x \<in> X
f \<in> {f. \<forall>x. x \<in> insert a X \<longrightarrow> f x \<in> carrier_vec n}

goal (1 subgoal):
 1. f x \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> X \<Longrightarrow> f ?x1 \<in> carrier_vec n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f {}) = (\<Sum>i\<in>{}. poly_of_vec (f i))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f F) = (\<Sum>i\<in>F. poly_of_vec (f i)); f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> poly_of_vec (finsum V f (insert x F)) = (\<Sum>i\<in>insert x F. poly_of_vec (f i))
[PROOF STEP]
have [simp]: "f a \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<in> carrier_vec n
[PROOF STEP]
using IH.prems
[PROOF STATE]
proof (prove)
using this:
f \<in> insert a X \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. f a \<in> carrier_vec n
[PROOF STEP]
unfolding Pi_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f. \<forall>x. x \<in> insert a X \<longrightarrow> f x \<in> carrier_vec n}

goal (1 subgoal):
 1. f a \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<in> carrier_vec n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f {}) = (\<Sum>i\<in>{}. poly_of_vec (f i))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f F) = (\<Sum>i\<in>F. poly_of_vec (f i)); f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> poly_of_vec (finsum V f (insert x F)) = (\<Sum>i\<in>insert x F. poly_of_vec (f i))
[PROOF STEP]
have [simp]: "dim_vec (finsum V f X) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (finsum V f X) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (finsum V f X) = n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f {}) = (\<Sum>i\<in>{}. poly_of_vec (f i))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f F) = (\<Sum>i\<in>F. poly_of_vec (f i)); f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> poly_of_vec (finsum V f (insert x F)) = (\<Sum>i\<in>insert x F. poly_of_vec (f i))
[PROOF STEP]
have [simp]: "dim_vec (f a) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (f a) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (f a) = n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f {}) = (\<Sum>i\<in>{}. poly_of_vec (f i))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f F) = (\<Sum>i\<in>F. poly_of_vec (f i)); f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> poly_of_vec (finsum V f (insert x F)) = (\<Sum>i\<in>insert x F. poly_of_vec (f i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
proof (cases "a \<in> X")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
 2. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> X

goal (2 subgoals):
 1. a \<in> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
 2. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in> X

goal (1 subgoal):
 1. poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
by (auto simp: insert_absorb IH)
[PROOF STATE]
proof (state)
this:
poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))

goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> X

goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<notin> X
[PROOF STEP]
have "(finsum V f (insert a X)) = f a + (finsum V f X)"
[PROOF STATE]
proof (prove)
using this:
a \<notin> X

goal (1 subgoal):
 1. finsum V f (insert a X) = f a + finsum V f X
[PROOF STEP]
by (auto intro: finsum_insert IH)
[PROOF STATE]
proof (state)
this:
finsum V f (insert a X) = f a + finsum V f X

goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
finsum V f (insert a X) = f a + finsum V f X

goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
have "poly_of_vec ... = poly_of_vec (f a) + poly_of_vec (finsum V f X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (f a + finsum V f X) = poly_of_vec (f a) + poly_of_vec (finsum V f X)
[PROOF STEP]
by (rule poly_of_vec_add, simp)
[PROOF STATE]
proof (state)
this:
poly_of_vec (f a + finsum V f X) = poly_of_vec (f a) + poly_of_vec (finsum V f X)

goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly_of_vec (f a + finsum V f X) = poly_of_vec (f a) + poly_of_vec (finsum V f X)

goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
have "... = (\<Sum>i\<in>insert a X. poly_of_vec (f i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (f a) + poly_of_vec (finsum V f X) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
using IH False
[PROOF STATE]
proof (prove)
using this:
finite X
a \<notin> X
f \<in> X \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))
f \<in> insert a X \<rightarrow> carrier_vec n
a \<notin> X

goal (1 subgoal):
 1. poly_of_vec (f a) + poly_of_vec (finsum V f X) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
by (subst sum.insert, auto)
[PROOF STATE]
proof (state)
this:
poly_of_vec (f a) + poly_of_vec (finsum V f X) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))

goal (1 subgoal):
 1. a \<notin> X \<Longrightarrow> poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))

goal (1 subgoal):
 1. poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly_of_vec (finsum V f (insert a X)) = (\<Sum>i\<in>insert a X. poly_of_vec (f i))

goal (1 subgoal):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> poly_of_vec (finsum V f {}) = (\<Sum>i\<in>{}. poly_of_vec (f i))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_poly_as: "vec_of_poly_n p (Suc (degree p)) = vec_of_poly p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n p (Suc (degree p)) = vec_of_poly p
[PROOF STEP]
by (induct p, auto simp: vec_of_poly_def vec_of_poly_n_def)


[STATEMENT]
lemma vec_of_poly_n_0 [simp]: "vec_of_poly_n p 0 = vNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n p 0 = vNil
[PROOF STEP]
by (auto simp: vec_of_poly_n_def)


[STATEMENT]
lemma vec_dim_vec_of_poly_n [simp]:
  "dim_vec (vec_of_poly_n p n) = n"
  "vec_of_poly_n p n \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_poly_n p n) = n &&& vec_of_poly_n p n \<in> carrier_vec n
[PROOF STEP]
unfolding vec_of_poly_n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec n (\<lambda>i. if i < n - degree p - 1 then 0::'a else coeff p (n - i - 1))) = n &&& vec n (\<lambda>i. if i < n - degree p - 1 then 0::'a else coeff p (n - i - 1)) \<in> carrier_vec n
[PROOF STEP]
by auto


[STATEMENT]
lemma dim_vec_of_poly [simp]: "dim_vec (vec_of_poly f) = degree f + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_poly f) = degree f + 1
[PROOF STEP]
by (simp add: vec_of_poly_as[symmetric])


[STATEMENT]
lemma vec_index_of_poly_n:
  assumes "i < n"
  shows "vec_of_poly_n p n $ i =
    (if i < n - Suc (degree p) then 0 else coeff p (n - i - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n p n $ i = (if i < n - Suc (degree p) then 0::'a else coeff p (n - i - 1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. vec_of_poly_n p n $ i = (if i < n - Suc (degree p) then 0::'a else coeff p (n - i - 1))
[PROOF STEP]
by (auto simp: vec_of_poly_n_def Let_def)


[STATEMENT]
lemma vec_of_poly_n_pCons[simp]:
  shows "vec_of_poly_n (pCons a p) (Suc n) = vec_of_poly_n p n @\<^sub>v vec_of_list [a]" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n (pCons a p) (Suc n) = vec_of_poly_n p n @\<^sub>v vec_of_list [a]
[PROOF STEP]
proof (unfold vec_eq_iff, intro conjI allI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dim_vec (vec_of_poly_n (pCons a p) (Suc n)) = dim_vec (vec_of_poly_n p n @\<^sub>v vec_of_list [a])
 2. \<And>i. i < dim_vec (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) \<Longrightarrow> vec_of_poly_n (pCons a p) (Suc n) $ i = (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) $ i
[PROOF STEP]
show "dim_vec ?l = dim_vec ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_poly_n (pCons a p) (Suc n)) = dim_vec (vec_of_poly_n p n @\<^sub>v vec_of_list [a])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (vec_of_poly_n (pCons a p) (Suc n)) = dim_vec (vec_of_poly_n p n @\<^sub>v vec_of_list [a])

goal (1 subgoal):
 1. \<And>i. i < dim_vec (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) \<Longrightarrow> vec_of_poly_n (pCons a p) (Suc n) $ i = (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) $ i
[PROOF STEP]
show "i < dim_vec ?r \<Longrightarrow> ?l $ i = ?r $ i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_vec (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) \<Longrightarrow> vec_of_poly_n (pCons a p) (Suc n) $ i = (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) $ i
[PROOF STEP]
by (cases "n - i", auto simp: coeff_pCons less_Suc_eq_le vec_index_of_poly_n)
[PROOF STATE]
proof (state)
this:
?i < dim_vec (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) \<Longrightarrow> vec_of_poly_n (pCons a p) (Suc n) $ ?i = (vec_of_poly_n p n @\<^sub>v vec_of_list [a]) $ ?i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_poly_pCons:
  shows "vec_of_poly (pCons a p) =
   (if p = 0 then vec_of_list [a] else vec_of_poly p @\<^sub>v vec_of_list [a])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly (pCons a p) = (if p = 0 then vec_of_list [a] else vec_of_poly p @\<^sub>v vec_of_list [a])
[PROOF STEP]
by (cases "degree p", auto simp: vec_of_poly_as[symmetric])


[STATEMENT]
lemma list_of_vec_of_poly [simp]:
  "list_of_vec (vec_of_poly p) = (if p = 0 then [0] else rev (coeffs p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_vec (vec_of_poly p) = (if p = 0 then [0::'a] else rev (coeffs p))
[PROOF STEP]
by (induct p, auto simp: vec_of_poly_pCons)


[STATEMENT]
lemma poly_of_vec_of_poly_n:
  assumes p: "degree p<n"
  shows "poly_of_vec (vec_of_poly_n p n) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (vec_of_poly_n p n) = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly_of_vec (vec_of_poly_n p n) = p
[PROOF STEP]
have "vec_of_poly_n p n $ (n - Suc i) = coeff p i" if i: "i < n" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
have n: "n - Suc i < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - Suc i < n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. n - Suc i < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - Suc i < n

goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
have "vec_of_poly_n p n $ (n - Suc i) =
      (if n - Suc i < n - Suc (degree p) then 0 else coeff p (n - (n - Suc i) - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = (if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1))
[PROOF STEP]
using vec_index_of_poly_n[OF n, of p]
[PROOF STATE]
proof (prove)
using this:
vec_of_poly_n p n $ (n - Suc i) = (if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1))

goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = (if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vec_of_poly_n p n $ (n - Suc i) = (if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1))

goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_poly_n p n $ (n - Suc i) = (if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1))

goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
have "... = coeff p i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1)) = coeff p i
[PROOF STEP]
using i n le_degree
[PROOF STATE]
proof (prove)
using this:
i < n
n - Suc i < n
coeff ?p ?n \<noteq> (0::?'a) \<Longrightarrow> ?n \<le> degree ?p

goal (1 subgoal):
 1. (if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1)) = coeff p i
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(if n - Suc i < n - Suc (degree p) then 0::'a else coeff p (n - (n - Suc i) - 1)) = coeff p i

goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_of_poly_n p n $ (n - Suc i) = coeff p i

goal (1 subgoal):
 1. vec_of_poly_n p n $ (n - Suc i) = coeff p i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vec_of_poly_n p n $ (n - Suc i) = coeff p i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> vec_of_poly_n p n $ (n - Suc ?i) = coeff p ?i

goal (1 subgoal):
 1. poly_of_vec (vec_of_poly_n p n) = p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> vec_of_poly_n p n $ (n - Suc ?i) = coeff p ?i

goal (1 subgoal):
 1. poly_of_vec (vec_of_poly_n p n) = p
[PROOF STEP]
have "coeff p i = 0" if i2: "i \<ge> n" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff p i = (0::'a)
[PROOF STEP]
by (rule coeff_eq_0, insert i2 p, simp)
[PROOF STATE]
proof (state)
this:
n \<le> ?i \<Longrightarrow> coeff p ?i = (0::'a)

goal (1 subgoal):
 1. poly_of_vec (vec_of_poly_n p n) = p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i < n \<Longrightarrow> vec_of_poly_n p n $ (n - Suc ?i) = coeff p ?i
n \<le> ?i \<Longrightarrow> coeff p ?i = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i < n \<Longrightarrow> vec_of_poly_n p n $ (n - Suc ?i) = coeff p ?i
n \<le> ?i \<Longrightarrow> coeff p ?i = (0::'a)

goal (1 subgoal):
 1. poly_of_vec (vec_of_poly_n p n) = p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < n \<Longrightarrow> vec_of_poly_n p n $ (n - Suc ?i) = coeff p ?i
n \<le> ?i \<Longrightarrow> coeff p ?i = (0::'a)
degree p < n

goal (1 subgoal):
 1. poly_of_vec (vec_of_poly_n p n) = p
[PROOF STEP]
unfolding poly_eq_iff
[PROOF STATE]
proof (prove)
using this:
?i < n \<Longrightarrow> vec_of_poly_n p n $ (n - Suc ?i) = coeff p ?i
n \<le> ?i \<Longrightarrow> coeff p ?i = (0::'a)
degree p < n

goal (1 subgoal):
 1. \<forall>na. coeff (poly_of_vec (vec_of_poly_n p n)) na = coeff p na
[PROOF STEP]
unfolding coeff_poly_of_vec
[PROOF STATE]
proof (prove)
using this:
?i < n \<Longrightarrow> vec_of_poly_n p n $ (n - Suc ?i) = coeff p ?i
n \<le> ?i \<Longrightarrow> coeff p ?i = (0::'a)
degree p < n

goal (1 subgoal):
 1. \<forall>na. (if na < dim_vec (vec_of_poly_n p n) then vec_of_poly_n p n $ (dim_vec (vec_of_poly_n p n) - Suc na) else (0::'a)) = coeff p na
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly_of_vec (vec_of_poly_n p n) = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_poly_n0[simp]: "vec_of_poly_n 0 n = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n 0 n = 0\<^sub>v n
[PROOF STEP]
unfolding vec_of_poly_n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec n (\<lambda>i. if i < n - degree 0 - 1 then 0::'a else coeff 0 (n - i - 1)) = 0\<^sub>v n
[PROOF STEP]
by auto


[STATEMENT]
lemma vec_of_poly_n_add: "vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n
[PROOF STEP]
proof (induct n arbitrary: a b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. vec_of_poly_n (a + b) 0 = vec_of_poly_n a 0 + vec_of_poly_n b 0
 2. \<And>n a b. (\<And>a b. vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n) \<Longrightarrow> vec_of_poly_n (a + b) (Suc n) = vec_of_poly_n a (Suc n) + vec_of_poly_n b (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>a b. vec_of_poly_n (a + b) 0 = vec_of_poly_n a 0 + vec_of_poly_n b 0
 2. \<And>n a b. (\<And>a b. vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n) \<Longrightarrow> vec_of_poly_n (a + b) (Suc n) = vec_of_poly_n a (Suc n) + vec_of_poly_n b (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n (a + b) 0 = vec_of_poly_n a 0 + vec_of_poly_n b 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_poly_n (a + b) 0 = vec_of_poly_n a 0 + vec_of_poly_n b 0

goal (1 subgoal):
 1. \<And>n a b. (\<And>a b. vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n) \<Longrightarrow> vec_of_poly_n (a + b) (Suc n) = vec_of_poly_n a (Suc n) + vec_of_poly_n b (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n a b. (\<And>a b. vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n) \<Longrightarrow> vec_of_poly_n (a + b) (Suc n) = vec_of_poly_n a (Suc n) + vec_of_poly_n b (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
vec_of_poly_n (?a + ?b) n = vec_of_poly_n ?a n + vec_of_poly_n ?b n

goal (1 subgoal):
 1. \<And>n a b. (\<And>a b. vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n) \<Longrightarrow> vec_of_poly_n (a + b) (Suc n) = vec_of_poly_n a (Suc n) + vec_of_poly_n b (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vec_of_poly_n (?a + ?b) n = vec_of_poly_n ?a n + vec_of_poly_n ?b n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vec_of_poly_n (?a + ?b) n = vec_of_poly_n ?a n + vec_of_poly_n ?b n

goal (1 subgoal):
 1. vec_of_poly_n (a + b) (Suc n) = vec_of_poly_n a (Suc n) + vec_of_poly_n b (Suc n)
[PROOF STEP]
by (cases a, cases b, auto)
[PROOF STATE]
proof (state)
this:
vec_of_poly_n (a + b) (Suc n) = vec_of_poly_n a (Suc n) + vec_of_poly_n b (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_poly_n_poly_of_vec:
  assumes n: "dim_vec g = n"
  shows "vec_of_poly_n (poly_of_vec g) n = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly_n (poly_of_vec g) n = g
[PROOF STEP]
proof (auto simp add: poly_of_vec_def vec_of_poly_n_def assms vec_eq_iff Let_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> g $ i = (0::'a)
 2. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
have d: "degree (\<Sum>i<n. monom (g $ (n - Suc i)) i) = degree (poly_of_vec g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Sum>i<n. monom (g $ (n - Suc i)) i) = degree (poly_of_vec g)
[PROOF STEP]
unfolding poly_of_vec_def Let_def n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Sum>i<n. monom (g $ (n - Suc i)) i) = degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (\<Sum>i<n. monom (g $ (n - Suc i)) i) = degree (poly_of_vec g)

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> g $ i = (0::'a)
 2. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> g $ i = (0::'a)
 2. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
assume i1: "i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i))"
    and i2: "i < n"
[PROOF STATE]
proof (state)
this:
i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i))
i < n

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> g $ i = (0::'a)
 2. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
have i3: "i < n - Suc (degree (poly_of_vec g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n - Suc (degree (poly_of_vec g))
[PROOF STEP]
using i1
[PROOF STATE]
proof (prove)
using this:
i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i))

goal (1 subgoal):
 1. i < n - Suc (degree (poly_of_vec g))
[PROOF STEP]
unfolding d
[PROOF STATE]
proof (prove)
using this:
i < n - Suc (degree (poly_of_vec g))

goal (1 subgoal):
 1. i < n - Suc (degree (poly_of_vec g))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n - Suc (degree (poly_of_vec g))

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> g $ i = (0::'a)
 2. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
hence "dim_vec g - Suc i > degree (poly_of_vec g)"
[PROOF STATE]
proof (prove)
using this:
i < n - Suc (degree (poly_of_vec g))

goal (1 subgoal):
 1. degree (poly_of_vec g) < dim_vec g - Suc i
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
i < n - Suc (degree (poly_of_vec g))
dim_vec g = n

goal (1 subgoal):
 1. degree (poly_of_vec g) < dim_vec g - Suc i
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
degree (poly_of_vec g) < dim_vec g - Suc i

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> g $ i = (0::'a)
 2. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree (poly_of_vec g) < dim_vec g - Suc i
[PROOF STEP]
show "g $ i = 0"
[PROOF STATE]
proof (prove)
using this:
degree (poly_of_vec g) < dim_vec g - Suc i

goal (1 subgoal):
 1. g $ i = (0::'a)
[PROOF STEP]
using i1 i2 i3
[PROOF STATE]
proof (prove)
using this:
degree (poly_of_vec g) < dim_vec g - Suc i
i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i))
i < n
i < n - Suc (degree (poly_of_vec g))

goal (1 subgoal):
 1. g $ i = (0::'a)
[PROOF STEP]
by (metis (no_types, lifting) Suc_diff_Suc coeff_poly_of_vec diff_Suc_less
        diff_diff_cancel leD le_degree less_imp_le_nat n neq0_conv)
[PROOF STATE]
proof (state)
this:
g $ i = (0::'a)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
assume "i < n"
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<not> i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i)); i < n\<rbrakk> \<Longrightarrow> coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
thus "coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i"
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i
[PROOF STEP]
by (metis (no_types) Suc_diff_Suc coeff_poly_of_vec diff_diff_cancel
        diff_less_Suc less_imp_le_nat n not_less_eq poly_of_vec_def)
[PROOF STATE]
proof (state)
this:
coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_of_vec_scalar_mult:
  assumes "degree b<n"
  shows "poly_of_vec (a \<cdot>\<^sub>v (vec_of_poly_n b n)) = smult a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec (a \<cdot>\<^sub>v vec_of_poly_n b n) = smult a b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
degree b < n

goal (1 subgoal):
 1. poly_of_vec (a \<cdot>\<^sub>v vec_of_poly_n b n) = smult a b
[PROOF STEP]
by (auto simp add: poly_eq_iff coeff_poly_of_vec vec_of_poly_n_def coeff_eq_0)


[STATEMENT]
lemma vec_of_poly_rev_shifted_dim[simp]: "dim_vec (vec_of_poly_rev_shifted p n s j) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n s j) = n
[PROOF STEP]
unfolding vec_of_poly_rev_shifted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec n (\<lambda>i. if i \<le> j \<and> j \<le> s + i then coeff p (s + i - j) else (0::'a))) = n
[PROOF STEP]
by auto