[STATEMENT]
lemma contradiction': "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using Q_weight_smaller DisjointPaths_Q' card_Q' Q_min
[PROOF STATE]
proof (prove)
using this:
Q_weight Q' < Q_weight Q
DisjointPaths H_x v0 v1 Q'
card Q' = sep_size
DisjointPaths H_x v0 v1 ?Q' \<and> card ?Q' = sep_size \<Longrightarrow> Q_weight Q \<le> Q_weight ?Q'

goal (1 subgoal):
 1. False
[PROOF STEP]
using Suc_leI not_less_eq_eq
[PROOF STATE]
proof (prove)
using this:
Q_weight Q' < Q_weight Q
DisjointPaths H_x v0 v1 Q'
card Q' = sep_size
DisjointPaths H_x v0 v1 ?Q' \<and> card ?Q' = sep_size \<Longrightarrow> Q_weight Q \<le> Q_weight ?Q'
?m < ?n \<Longrightarrow> Suc ?m \<le> ?n
(\<not> ?m \<le> ?n) = (Suc ?n \<le> ?m)

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast


[STATEMENT]
lemma deg_sectI: "t \<in> .[X] \<Longrightarrow> deg_pm t = d \<Longrightarrow> t \<in> deg_sect X d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> .[X]; deg_pm t = d\<rbrakk> \<Longrightarrow> t \<in> deg_sect X d
[PROOF STEP]
by (simp add: deg_sect_def)


[STATEMENT]
lemma deg_sectD:
  assumes "t \<in> deg_sect X d"
  shows "t \<in> .[X]" and "deg_pm t = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> .[X] &&& deg_pm t = d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> deg_sect X d

goal (1 subgoal):
 1. t \<in> .[X] &&& deg_pm t = d
[PROOF STEP]
by (simp_all add: deg_sect_def)


[STATEMENT]
lemma deg_le_sect_alt: "deg_le_sect X d = .[X] \<inter> {t. deg_pm t \<le> d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_le_sect X d = .[X] \<inter> {t. deg_pm t \<le> d}
[PROOF STEP]
by (auto simp: deg_le_sect_def deg_sect_def)


[STATEMENT]
lemma deg_le_sectI: "t \<in> .[X] \<Longrightarrow> deg_pm t \<le> d \<Longrightarrow> t \<in> deg_le_sect X d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> .[X]; deg_pm t \<le> d\<rbrakk> \<Longrightarrow> t \<in> deg_le_sect X d
[PROOF STEP]
by (simp add: deg_le_sect_alt)


[STATEMENT]
lemma deg_le_sectD:
  assumes "t \<in> deg_le_sect X d"
  shows "t \<in> .[X]" and "deg_pm t \<le> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> .[X] &&& deg_pm t \<le> d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> deg_le_sect X d

goal (1 subgoal):
 1. t \<in> .[X] &&& deg_pm t \<le> d
[PROOF STEP]
by (simp_all add: deg_le_sect_alt)


[STATEMENT]
lemma deg_sect_zero [simp]: "deg_sect X 0 = {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_sect X 0 = {0}
[PROOF STEP]
by (auto simp: deg_sect_def zero_in_PPs)


[STATEMENT]
lemma deg_sect_empty: "deg_sect {} d = (if d = 0 then {0} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_sect {} d = (if d = 0 then {0} else {})
[PROOF STEP]
by (auto simp: deg_sect_def)


[STATEMENT]
lemma deg_sect_singleton [simp]: "deg_sect {x} d = {Poly_Mapping.single x d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_sect {x} d = {monomial d x}
[PROOF STEP]
by (auto simp: deg_sect_def deg_pm_single PPs_singleton)


[STATEMENT]
lemma deg_le_sect_zero [simp]: "deg_le_sect X 0 = {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_le_sect X 0 = {0}
[PROOF STEP]
by (auto simp: deg_le_sect_def)


[STATEMENT]
lemma deg_le_sect_empty [simp]: "deg_le_sect {} d = {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_le_sect {} d = {0}
[PROOF STEP]
by (auto simp: deg_le_sect_alt varnum_eq_zero_iff)


[STATEMENT]
lemma deg_le_sect_singleton: "deg_le_sect {x} d = Poly_Mapping.single x ` {..d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_le_sect {x} d = Poly_Mapping.single x ` {..d}
[PROOF STEP]
by (auto simp: deg_le_sect_alt deg_pm_single PPs_singleton)


[STATEMENT]
lemma deg_sect_mono: "X \<subseteq> Y \<Longrightarrow> deg_sect X d \<subseteq> deg_sect Y d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> Y \<Longrightarrow> deg_sect X d \<subseteq> deg_sect Y d
[PROOF STEP]
by (auto simp: deg_sect_def dest: PPs_mono)


[STATEMENT]
lemma deg_le_sect_mono_1: "X \<subseteq> Y \<Longrightarrow> deg_le_sect X d \<subseteq> deg_le_sect Y d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> Y \<Longrightarrow> deg_le_sect X d \<subseteq> deg_le_sect Y d
[PROOF STEP]
by (auto simp: deg_le_sect_alt dest: PPs_mono)


[STATEMENT]
lemma deg_le_sect_mono_2: "d1 \<le> d2 \<Longrightarrow> deg_le_sect X d1 \<subseteq> deg_le_sect X d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d1 \<le> d2 \<Longrightarrow> deg_le_sect X d1 \<subseteq> deg_le_sect X d2
[PROOF STEP]
by (auto simp: deg_le_sect_alt)


[STATEMENT]
lemma zero_in_deg_le_sect: "0 \<in> deg_le_sect n d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> deg_le_sect n d
[PROOF STEP]
by (simp add: deg_le_sect_alt zero_in_PPs)


[STATEMENT]
lemma deg_sect_disjoint: "d1 \<noteq> d2 \<Longrightarrow> deg_sect X d1 \<inter> deg_sect Y d2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d1 \<noteq> d2 \<Longrightarrow> deg_sect X d1 \<inter> deg_sect Y d2 = {}
[PROOF STEP]
by (auto simp: deg_sect_def)


[STATEMENT]
lemma deg_le_sect_deg_sect_disjoint: "d1 < d2 \<Longrightarrow> deg_le_sect Y d1 \<inter> deg_sect X d2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d1 < d2 \<Longrightarrow> deg_le_sect Y d1 \<inter> deg_sect X d2 = {}
[PROOF STEP]
by (auto simp: deg_sect_def deg_le_sect_alt)


[STATEMENT]
lemma deg_sect_Suc:
  "deg_sect X (Suc d) = (\<Union>x\<in>X. (+) (Poly_Mapping.single x 1) ` deg_sect X d)" (is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_sect X (Suc d) = (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
[PROOF STEP]
proof (rule set_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> deg_sect X (Suc d)) = (x \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d))
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> deg_sect X (Suc d)) = (x \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d))
[PROOF STEP]
show "t \<in> ?A \<longleftrightarrow> t \<in> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<in> deg_sect X (Suc d)) = (t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
assume "t \<in> ?A"
[PROOF STATE]
proof (state)
this:
t \<in> deg_sect X (Suc d)

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
hence "t \<in> .[X]" and "deg_pm t = Suc d"
[PROOF STATE]
proof (prove)
using this:
t \<in> deg_sect X (Suc d)

goal (1 subgoal):
 1. t \<in> .[X] &&& deg_pm t = Suc d
[PROOF STEP]
by (rule deg_sectD)+
[PROOF STATE]
proof (state)
this:
t \<in> .[X]
deg_pm t = Suc d

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
deg_pm t = Suc d
[PROOF STEP]
have "keys t \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
deg_pm t = Suc d

goal (1 subgoal):
 1. keys t \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
keys t \<noteq> {}

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
keys t \<noteq> {}
[PROOF STEP]
obtain x where "x \<in> keys t"
[PROOF STATE]
proof (prove)
using this:
keys t \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> keys t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> keys t

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
hence "1 \<le> lookup t x"
[PROOF STATE]
proof (prove)
using this:
x \<in> keys t

goal (1 subgoal):
 1. 1 \<le> lookup t x
[PROOF STEP]
by (simp add: in_keys_iff)
[PROOF STATE]
proof (state)
this:
1 \<le> lookup t x

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
from \<open>t \<in> .[X]\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> .[X]
[PROOF STEP]
have "keys t \<subseteq> X"
[PROOF STATE]
proof (prove)
using this:
t \<in> .[X]

goal (1 subgoal):
 1. keys t \<subseteq> X
[PROOF STEP]
by (rule PPsD)
[PROOF STATE]
proof (state)
this:
keys t \<subseteq> X

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
with \<open>x \<in> keys t\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> keys t
keys t \<subseteq> X
[PROOF STEP]
have "x \<in> X"
[PROOF STATE]
proof (prove)
using this:
x \<in> keys t
keys t \<subseteq> X

goal (1 subgoal):
 1. x \<in> X
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
let ?s = "Poly_Mapping.single x (1::nat)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
from \<open>1 \<le> lookup t x\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> lookup t x
[PROOF STEP]
have "?s adds t"
[PROOF STATE]
proof (prove)
using this:
1 \<le> lookup t x

goal (1 subgoal):
 1. monomial 1 x adds t
[PROOF STEP]
by (auto simp: lookup_single when_def intro!: adds_poly_mappingI le_funI)
[PROOF STATE]
proof (state)
this:
monomial 1 x adds t

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
hence t: "?s + (t - ?s) = t"
[PROOF STATE]
proof (prove)
using this:
monomial 1 x adds t

goal (1 subgoal):
 1. monomial 1 x + (t - monomial 1 x) = t
[PROOF STEP]
by (metis add.commute adds_minus)
[PROOF STATE]
proof (state)
this:
monomial 1 x + (t - monomial 1 x) = t

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
have "t - ?s \<in> deg_sect X d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t - monomial 1 x \<in> deg_sect X d
[PROOF STEP]
proof (rule deg_sectI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t - monomial 1 x \<in> .[X]
 2. deg_pm (t - monomial 1 x) = d
[PROOF STEP]
from \<open>t \<in> .[X]\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> .[X]
[PROOF STEP]
show "t - ?s \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
t \<in> .[X]

goal (1 subgoal):
 1. t - monomial 1 x \<in> .[X]
[PROOF STEP]
by (rule PPs_closed_minus)
[PROOF STATE]
proof (state)
this:
t - monomial 1 x \<in> .[X]

goal (1 subgoal):
 1. deg_pm (t - monomial 1 x) = d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deg_pm (t - monomial 1 x) = d
[PROOF STEP]
from deg_pm_plus[of ?s "t - ?s"]
[PROOF STATE]
proof (chain)
picking this:
deg_pm (monomial 1 x + (t - monomial 1 x)) = deg_pm (monomial 1 x) + deg_pm (t - monomial 1 x)
[PROOF STEP]
have "deg_pm t = Suc (deg_pm (t - ?s))"
[PROOF STATE]
proof (prove)
using this:
deg_pm (monomial 1 x + (t - monomial 1 x)) = deg_pm (monomial 1 x) + deg_pm (t - monomial 1 x)

goal (1 subgoal):
 1. deg_pm t = Suc (deg_pm (t - monomial 1 x))
[PROOF STEP]
by (simp only: t deg_pm_single)
[PROOF STATE]
proof (state)
this:
deg_pm t = Suc (deg_pm (t - monomial 1 x))

goal (1 subgoal):
 1. deg_pm (t - monomial 1 x) = d
[PROOF STEP]
thus "deg_pm (t - ?s) = d"
[PROOF STATE]
proof (prove)
using this:
deg_pm t = Suc (deg_pm (t - monomial 1 x))

goal (1 subgoal):
 1. deg_pm (t - monomial 1 x) = d
[PROOF STEP]
by (simp add: \<open>deg_pm t = Suc d\<close>)
[PROOF STATE]
proof (state)
this:
deg_pm (t - monomial 1 x) = d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t - monomial 1 x \<in> deg_sect X d

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
hence "?s + (t - ?s) \<in> (+) ?s ` deg_sect X d"
[PROOF STATE]
proof (prove)
using this:
t - monomial 1 x \<in> deg_sect X d

goal (1 subgoal):
 1. monomial 1 x + (t - monomial 1 x) \<in> (+) (monomial 1 x) ` deg_sect X d
[PROOF STEP]
by (rule imageI)
[PROOF STATE]
proof (state)
this:
monomial 1 x + (t - monomial 1 x) \<in> (+) (monomial 1 x) ` deg_sect X d

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
hence "t \<in> (+) ?s ` deg_sect X d"
[PROOF STATE]
proof (prove)
using this:
monomial 1 x + (t - monomial 1 x) \<in> (+) (monomial 1 x) ` deg_sect X d

goal (1 subgoal):
 1. t \<in> (+) (monomial 1 x) ` deg_sect X d
[PROOF STEP]
by (simp only: t)
[PROOF STATE]
proof (state)
this:
t \<in> (+) (monomial 1 x) ` deg_sect X d

goal (2 subgoals):
 1. t \<in> deg_sect X (Suc d) \<Longrightarrow> t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
 2. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
with \<open>x \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
t \<in> (+) (monomial 1 x) ` deg_sect X d
[PROOF STEP]
show "t \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
t \<in> (+) (monomial 1 x) ` deg_sect X d

goal (1 subgoal):
 1. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)

goal (1 subgoal):
 1. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
assume "t \<in> ?B"
[PROOF STATE]
proof (state)
this:
t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)

goal (1 subgoal):
 1. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)
[PROOF STEP]
obtain x where "x \<in> X" and "t \<in> (+) (Poly_Mapping.single x 1) ` deg_sect X d"
[PROOF STATE]
proof (prove)
using this:
t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> X; t \<in> (+) (monomial 1 x) ` deg_sect X d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<in> X
t \<in> (+) (monomial 1 x) ` deg_sect X d

goal (1 subgoal):
 1. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
t \<in> (+) (monomial 1 x) ` deg_sect X d
[PROOF STEP]
obtain s where s: "s \<in> deg_sect X d"
      and t: "t = Poly_Mapping.single x 1 + s" (is "t = ?s + s")
[PROOF STATE]
proof (prove)
using this:
t \<in> (+) (monomial 1 x) ` deg_sect X d

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> deg_sect X d; t = monomial 1 x + s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s \<in> deg_sect X d
t = monomial 1 x + s

goal (1 subgoal):
 1. t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d) \<Longrightarrow> t \<in> deg_sect X (Suc d)
[PROOF STEP]
show "t \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> deg_sect X (Suc d)
[PROOF STEP]
proof (rule deg_sectI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<in> .[X]
 2. deg_pm t = Suc d
[PROOF STEP]
from \<open>x \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
have "?s \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. monomial 1 x \<in> .[X]
[PROOF STEP]
by (rule PPs_closed_single)
[PROOF STATE]
proof (state)
this:
monomial 1 x \<in> .[X]

goal (2 subgoals):
 1. t \<in> .[X]
 2. deg_pm t = Suc d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
monomial 1 x \<in> .[X]

goal (2 subgoals):
 1. t \<in> .[X]
 2. deg_pm t = Suc d
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> deg_sect X d
[PROOF STEP]
have "s \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
s \<in> deg_sect X d

goal (1 subgoal):
 1. s \<in> .[X]
[PROOF STEP]
by (rule deg_sectD)
[PROOF STATE]
proof (state)
this:
s \<in> .[X]

goal (2 subgoals):
 1. t \<in> .[X]
 2. deg_pm t = Suc d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
monomial 1 x \<in> .[X]
s \<in> .[X]
[PROOF STEP]
show "t \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
monomial 1 x \<in> .[X]
s \<in> .[X]

goal (1 subgoal):
 1. t \<in> .[X]
[PROOF STEP]
unfolding t
[PROOF STATE]
proof (prove)
using this:
monomial 1 x \<in> .[X]
s \<in> .[X]

goal (1 subgoal):
 1. monomial 1 x + s \<in> .[X]
[PROOF STEP]
by (rule PPs_closed_plus)
[PROOF STATE]
proof (state)
this:
t \<in> .[X]

goal (1 subgoal):
 1. deg_pm t = Suc d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deg_pm t = Suc d
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> deg_sect X d
[PROOF STEP]
have "deg_pm s = d"
[PROOF STATE]
proof (prove)
using this:
s \<in> deg_sect X d

goal (1 subgoal):
 1. deg_pm s = d
[PROOF STEP]
by (rule deg_sectD)
[PROOF STATE]
proof (state)
this:
deg_pm s = d

goal (1 subgoal):
 1. deg_pm t = Suc d
[PROOF STEP]
thus "deg_pm t = Suc d"
[PROOF STATE]
proof (prove)
using this:
deg_pm s = d

goal (1 subgoal):
 1. deg_pm t = Suc d
[PROOF STEP]
by (simp add: t deg_pm_single deg_pm_plus)
[PROOF STATE]
proof (state)
this:
deg_pm t = Suc d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<in> deg_sect X (Suc d)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(t \<in> deg_sect X (Suc d)) = (t \<in> (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deg_sect_insert:
  "deg_sect (insert x X) d = (\<Union>d0\<le>d. (+) (Poly_Mapping.single x (d - d0)) ` deg_sect X d0)"
    (is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_sect (insert x X) d = (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
[PROOF STEP]
proof (rule set_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. (xa \<in> deg_sect (insert x X) d) = (xa \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0))
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. (xa \<in> deg_sect (insert x X) d) = (xa \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0))
[PROOF STEP]
show "t \<in> ?A \<longleftrightarrow> t \<in> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<in> deg_sect (insert x X) d) = (t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
assume "t \<in> ?A"
[PROOF STATE]
proof (state)
this:
t \<in> deg_sect (insert x X) d

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
hence "t \<in> .[insert x X]" and "deg_pm t = d"
[PROOF STATE]
proof (prove)
using this:
t \<in> deg_sect (insert x X) d

goal (1 subgoal):
 1. t \<in> .[insert x X] &&& deg_pm t = d
[PROOF STEP]
by (rule deg_sectD)+
[PROOF STATE]
proof (state)
this:
t \<in> .[insert x X]
deg_pm t = d

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
t \<in> .[insert x X]
[PROOF STEP]
obtain e tx where "tx \<in> .[X]" and t: "t = Poly_Mapping.single x e + tx"
[PROOF STATE]
proof (prove)
using this:
t \<in> .[insert x X]

goal (1 subgoal):
 1. (\<And>tx e. \<lbrakk>tx \<in> .[X]; t = monomial e x + tx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule PPs_insertE)
[PROOF STATE]
proof (state)
this:
tx \<in> .[X]
t = monomial e x + tx

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
have "e + deg_pm tx = deg_pm t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e + deg_pm tx = deg_pm t
[PROOF STEP]
by (simp add: t deg_pm_plus deg_pm_single)
[PROOF STATE]
proof (state)
this:
e + deg_pm tx = deg_pm t

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
hence "e + deg_pm tx = d"
[PROOF STATE]
proof (prove)
using this:
e + deg_pm tx = deg_pm t

goal (1 subgoal):
 1. e + deg_pm tx = d
[PROOF STEP]
by (simp only: \<open>deg_pm t = d\<close>)
[PROOF STATE]
proof (state)
this:
e + deg_pm tx = d

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
hence "deg_pm tx \<in> {..d}" and e: "e = d - deg_pm tx"
[PROOF STATE]
proof (prove)
using this:
e + deg_pm tx = d

goal (1 subgoal):
 1. deg_pm tx \<in> {..d} &&& e = d - deg_pm tx
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
deg_pm tx \<in> {..d}
e = d - deg_pm tx

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
from \<open>tx \<in> .[X]\<close> refl
[PROOF STATE]
proof (chain)
picking this:
tx \<in> .[X]
?t = ?t
[PROOF STEP]
have "tx \<in> deg_sect X (deg_pm tx)"
[PROOF STATE]
proof (prove)
using this:
tx \<in> .[X]
?t = ?t

goal (1 subgoal):
 1. tx \<in> deg_sect X (deg_pm tx)
[PROOF STEP]
by (rule deg_sectI)
[PROOF STATE]
proof (state)
this:
tx \<in> deg_sect X (deg_pm tx)

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
hence "t \<in> (+) (Poly_Mapping.single x (d - deg_pm tx)) ` deg_sect X (deg_pm tx)"
[PROOF STATE]
proof (prove)
using this:
tx \<in> deg_sect X (deg_pm tx)

goal (1 subgoal):
 1. t \<in> (+) (monomial (d - deg_pm tx) x) ` deg_sect X (deg_pm tx)
[PROOF STEP]
unfolding t e
[PROOF STATE]
proof (prove)
using this:
tx \<in> deg_sect X (deg_pm tx)

goal (1 subgoal):
 1. monomial (d - deg_pm tx) x + tx \<in> (+) (monomial (d - deg_pm tx) x) ` deg_sect X (deg_pm tx)
[PROOF STEP]
by (rule imageI)
[PROOF STATE]
proof (state)
this:
t \<in> (+) (monomial (d - deg_pm tx) x) ` deg_sect X (deg_pm tx)

goal (2 subgoals):
 1. t \<in> deg_sect (insert x X) d \<Longrightarrow> t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
 2. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
with \<open>deg_pm tx \<in> {..d}\<close>
[PROOF STATE]
proof (chain)
picking this:
deg_pm tx \<in> {..d}
t \<in> (+) (monomial (d - deg_pm tx) x) ` deg_sect X (deg_pm tx)
[PROOF STEP]
show "t \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
deg_pm tx \<in> {..d}
t \<in> (+) (monomial (d - deg_pm tx) x) ` deg_sect X (deg_pm tx)

goal (1 subgoal):
 1. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)

goal (1 subgoal):
 1. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
assume "t \<in> ?B"
[PROOF STATE]
proof (state)
this:
t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)

goal (1 subgoal):
 1. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)
[PROOF STEP]
obtain d0 where "d0 \<in> {..d}" and "t \<in> (+) (Poly_Mapping.single x (d - d0)) ` deg_sect X d0"
[PROOF STATE]
proof (prove)
using this:
t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0)

goal (1 subgoal):
 1. (\<And>d0. \<lbrakk>d0 \<in> {..d}; t \<in> (+) (monomial (d - d0) x) ` deg_sect X d0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
d0 \<in> {..d}
t \<in> (+) (monomial (d - d0) x) ` deg_sect X d0

goal (1 subgoal):
 1. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
t \<in> (+) (monomial (d - d0) x) ` deg_sect X d0
[PROOF STEP]
obtain s where s: "s \<in> deg_sect X d0"
      and t: "t = Poly_Mapping.single x (d - d0) + s" (is "t = ?s + s")
[PROOF STATE]
proof (prove)
using this:
t \<in> (+) (monomial (d - d0) x) ` deg_sect X d0

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> deg_sect X d0; t = monomial (d - d0) x + s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s \<in> deg_sect X d0
t = monomial (d - d0) x + s

goal (1 subgoal):
 1. t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) \<Longrightarrow> t \<in> deg_sect (insert x X) d
[PROOF STEP]
show "t \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> deg_sect (insert x X) d
[PROOF STEP]
proof (rule deg_sectI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<in> .[insert x X]
 2. deg_pm t = d
[PROOF STEP]
have "?s \<in> .[insert x X]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomial (d - d0) x \<in> .[insert x X]
[PROOF STEP]
by (rule PPs_closed_single, simp)
[PROOF STATE]
proof (state)
this:
monomial (d - d0) x \<in> .[insert x X]

goal (2 subgoals):
 1. t \<in> .[insert x X]
 2. deg_pm t = d
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> deg_sect X d0
[PROOF STEP]
have "s \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
s \<in> deg_sect X d0

goal (1 subgoal):
 1. s \<in> .[X]
[PROOF STEP]
by (rule deg_sectD)
[PROOF STATE]
proof (state)
this:
s \<in> .[X]

goal (2 subgoals):
 1. t \<in> .[insert x X]
 2. deg_pm t = d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s \<in> .[X]

goal (2 subgoals):
 1. t \<in> .[insert x X]
 2. deg_pm t = d
[PROOF STEP]
have "... \<subseteq> .[insert x X]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. .[X] \<subseteq> .[insert x X]
[PROOF STEP]
by (rule PPs_mono, blast)
[PROOF STATE]
proof (state)
this:
.[X] \<subseteq> .[insert x X]

goal (2 subgoals):
 1. t \<in> .[insert x X]
 2. deg_pm t = d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
s \<in> .[insert x X]
[PROOF STEP]
have "s \<in> .[insert x X]"
[PROOF STATE]
proof (prove)
using this:
s \<in> .[insert x X]

goal (1 subgoal):
 1. s \<in> .[insert x X]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
s \<in> .[insert x X]

goal (2 subgoals):
 1. t \<in> .[insert x X]
 2. deg_pm t = d
[PROOF STEP]
with \<open>?s \<in> .[insert x X]\<close>
[PROOF STATE]
proof (chain)
picking this:
monomial (d - d0) x \<in> .[insert x X]
s \<in> .[insert x X]
[PROOF STEP]
show "t \<in> .[insert x X]"
[PROOF STATE]
proof (prove)
using this:
monomial (d - d0) x \<in> .[insert x X]
s \<in> .[insert x X]

goal (1 subgoal):
 1. t \<in> .[insert x X]
[PROOF STEP]
unfolding t
[PROOF STATE]
proof (prove)
using this:
monomial (d - d0) x \<in> .[insert x X]
s \<in> .[insert x X]

goal (1 subgoal):
 1. monomial (d - d0) x + s \<in> .[insert x X]
[PROOF STEP]
by (rule PPs_closed_plus)
[PROOF STATE]
proof (state)
this:
t \<in> .[insert x X]

goal (1 subgoal):
 1. deg_pm t = d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deg_pm t = d
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> deg_sect X d0
[PROOF STEP]
have "deg_pm s = d0"
[PROOF STATE]
proof (prove)
using this:
s \<in> deg_sect X d0

goal (1 subgoal):
 1. deg_pm s = d0
[PROOF STEP]
by (rule deg_sectD)
[PROOF STATE]
proof (state)
this:
deg_pm s = d0

goal (1 subgoal):
 1. deg_pm t = d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
deg_pm s = d0

goal (1 subgoal):
 1. deg_pm t = d
[PROOF STEP]
from \<open>d0 \<in> {..d}\<close>
[PROOF STATE]
proof (chain)
picking this:
d0 \<in> {..d}
[PROOF STEP]
have "d0 \<le> d"
[PROOF STATE]
proof (prove)
using this:
d0 \<in> {..d}

goal (1 subgoal):
 1. d0 \<le> d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d0 \<le> d

goal (1 subgoal):
 1. deg_pm t = d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
deg_pm s = d0
d0 \<le> d
[PROOF STEP]
show "deg_pm t = d"
[PROOF STATE]
proof (prove)
using this:
deg_pm s = d0
d0 \<le> d

goal (1 subgoal):
 1. deg_pm t = d
[PROOF STEP]
by (simp add: t deg_pm_single deg_pm_plus)
[PROOF STATE]
proof (state)
this:
deg_pm t = d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<in> deg_sect (insert x X) d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(t \<in> deg_sect (insert x X) d) = (t \<in> (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deg_le_sect_Suc: "deg_le_sect X (Suc d) = deg_le_sect X d \<union> deg_sect X (Suc d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_le_sect X (Suc d) = deg_le_sect X d \<union> deg_sect X (Suc d)
[PROOF STEP]
by (simp add: deg_le_sect_def atMost_Suc Un_commute)


[STATEMENT]
lemma deg_le_sect_Suc_2:
  "deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (Poly_Mapping.single x 1) ` deg_le_sect X d)"
    (is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
have eq1: "{Suc 0..Suc d} = Suc ` {..d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Suc 0..Suc d} = Suc ` {..d}
[PROOF STEP]
by (simp add: image_Suc_atMost)
[PROOF STATE]
proof (state)
this:
{Suc 0..Suc d} = Suc ` {..d}

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
have "insert 0 {1..Suc d} = {..Suc d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert 0 {1..Suc d} = {..Suc d}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
insert 0 {1..Suc d} = {..Suc d}

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
hence "?A = (\<Union>d0\<in>insert 0 {1..Suc d}. deg_sect X d0)"
[PROOF STATE]
proof (prove)
using this:
insert 0 {1..Suc d} = {..Suc d}

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = \<Union> (deg_sect X ` insert 0 {1..Suc d})
[PROOF STEP]
by (simp add: deg_le_sect_def)
[PROOF STATE]
proof (state)
this:
deg_le_sect X (Suc d) = \<Union> (deg_sect X ` insert 0 {1..Suc d})

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
deg_le_sect X (Suc d) = \<Union> (deg_sect X ` insert 0 {1..Suc d})

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
have "... = insert 0 (\<Union>d0\<le>d. deg_sect X (Suc d0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (deg_sect X ` insert 0 {1..Suc d}) = insert 0 (\<Union>d0\<le>d. deg_sect X (Suc d0))
[PROOF STEP]
by (simp add: eq1)
[PROOF STATE]
proof (state)
this:
\<Union> (deg_sect X ` insert 0 {1..Suc d}) = insert 0 (\<Union>d0\<le>d. deg_sect X (Suc d0))

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (deg_sect X ` insert 0 {1..Suc d}) = insert 0 (\<Union>d0\<le>d. deg_sect X (Suc d0))

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
have "... = insert 0 (\<Union>d0\<le>d. (\<Union>x\<in>X. (+) (Poly_Mapping.single x 1) ` deg_sect X d0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert 0 (\<Union>d0\<le>d. deg_sect X (Suc d0)) = insert 0 (\<Union>d0\<le>d. \<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d0)
[PROOF STEP]
by (simp only: deg_sect_Suc)
[PROOF STATE]
proof (state)
this:
insert 0 (\<Union>d0\<le>d. deg_sect X (Suc d0)) = insert 0 (\<Union>d0\<le>d. \<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d0)

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insert 0 (\<Union>d0\<le>d. deg_sect X (Suc d0)) = insert 0 (\<Union>d0\<le>d. \<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d0)

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
have "... = insert 0 (\<Union>x\<in>X. (+) (Poly_Mapping.single x 1) ` (\<Union>d0\<le>d. deg_sect X d0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert 0 (\<Union>d0\<le>d. \<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d0) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` \<Union> (deg_sect X ` {..d}))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
insert 0 (\<Union>d0\<le>d. \<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d0) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` \<Union> (deg_sect X ` {..d}))

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insert 0 (\<Union>d0\<le>d. \<Union>x\<in>X. (+) (monomial 1 x) ` deg_sect X d0) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` \<Union> (deg_sect X ` {..d}))

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
have "... = ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` \<Union> (deg_sect X ` {..d})) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
by (simp only: deg_le_sect_def)
[PROOF STATE]
proof (state)
this:
insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` \<Union> (deg_sect X ` {..d})) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)

goal (1 subgoal):
 1. deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
deg_le_sect X (Suc d) = insert 0 (\<Union>x\<in>X. (+) (monomial 1 x) ` deg_le_sect X d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_deg_sect:
  assumes "finite X"
  shows "finite ((deg_sect X d)::('x::countable \<Rightarrow>\<^sub>0 nat) set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (deg_sect X d)
[PROOF STEP]
proof (induct d)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (deg_sect X 0)
 2. \<And>d. finite (deg_sect X d) \<Longrightarrow> finite (deg_sect X (Suc d))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite (deg_sect X 0)
 2. \<And>d. finite (deg_sect X d) \<Longrightarrow> finite (deg_sect X (Suc d))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (deg_sect X 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (deg_sect X 0)

goal (1 subgoal):
 1. \<And>d. finite (deg_sect X d) \<Longrightarrow> finite (deg_sect X (Suc d))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. finite (deg_sect X d) \<Longrightarrow> finite (deg_sect X (Suc d))
[PROOF STEP]
case (Suc d)
[PROOF STATE]
proof (state)
this:
finite (deg_sect X d)

goal (1 subgoal):
 1. \<And>d. finite (deg_sect X d) \<Longrightarrow> finite (deg_sect X (Suc d))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite X
finite (deg_sect X d)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite X
finite (deg_sect X d)

goal (1 subgoal):
 1. finite (deg_sect X (Suc d))
[PROOF STEP]
by (simp add: deg_sect_Suc)
[PROOF STATE]
proof (state)
this:
finite (deg_sect X (Suc d))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma keys_subset_deg_le_sectI:
  assumes "p \<in> P[X]" and "poly_deg p \<le> d"
  shows "keys p \<subseteq> deg_le_sect X d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys p \<subseteq> deg_le_sect X d
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
assume "t \<in> keys p"
[PROOF STATE]
proof (state)
this:
t \<in> keys p

goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t \<in> keys p

goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
p \<in> P[X]
[PROOF STEP]
have "... \<subseteq> .[X]"
[PROOF STATE]
proof (prove)
using this:
p \<in> P[X]

goal (1 subgoal):
 1. keys p \<subseteq> .[X]
[PROOF STEP]
by (rule PolysD)
[PROOF STATE]
proof (state)
this:
keys p \<subseteq> .[X]

goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
t \<in> .[X]
[PROOF STEP]
have "t \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
t \<in> .[X]

goal (1 subgoal):
 1. t \<in> .[X]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
t \<in> .[X]

goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
from \<open>t \<in> keys p\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> keys p
[PROOF STEP]
have "deg_pm t \<le> poly_deg p"
[PROOF STATE]
proof (prove)
using this:
t \<in> keys p

goal (1 subgoal):
 1. deg_pm t \<le> poly_deg p
[PROOF STEP]
by (rule poly_deg_max_keys)
[PROOF STATE]
proof (state)
this:
deg_pm t \<le> poly_deg p

goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
from this assms(2)
[PROOF STATE]
proof (chain)
picking this:
deg_pm t \<le> poly_deg p
poly_deg p \<le> d
[PROOF STEP]
have "deg_pm t \<le> d"
[PROOF STATE]
proof (prove)
using this:
deg_pm t \<le> poly_deg p
poly_deg p \<le> d

goal (1 subgoal):
 1. deg_pm t \<le> d
[PROOF STEP]
by (rule le_trans)
[PROOF STATE]
proof (state)
this:
deg_pm t \<le> d

goal (1 subgoal):
 1. \<And>x. x \<in> keys p \<Longrightarrow> x \<in> deg_le_sect X d
[PROOF STEP]
with \<open>t \<in> .[X]\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> .[X]
deg_pm t \<le> d
[PROOF STEP]
show "t \<in> deg_le_sect X d"
[PROOF STATE]
proof (prove)
using this:
t \<in> .[X]
deg_pm t \<le> d

goal (1 subgoal):
 1. t \<in> deg_le_sect X d
[PROOF STEP]
by (rule deg_le_sectI)
[PROOF STATE]
proof (state)
this:
t \<in> deg_le_sect X d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma binomial_symmetric_plus: "(n + k) choose n = (n + k) choose k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n + k choose n = n + k choose k
[PROOF STEP]
by (metis add_diff_cancel_left' binomial_symmetric le_add1)


[STATEMENT]
lemma card_deg_sect:
  assumes "finite X" and "X \<noteq> {}"
  shows "card (deg_sect X d) = (d + (card X - 1)) choose (card X - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (deg_sect X d) = d + (card X - 1) choose (card X - 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
X \<noteq> {}

goal (1 subgoal):
 1. card (deg_sect X d) = d + (card X - 1) choose (card X - 1)
[PROOF STEP]
proof (induct X arbitrary: d)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>d. {} \<noteq> {} \<Longrightarrow> card (deg_sect {} d) = d + (card {} - 1) choose (card {} - 1)
 2. \<And>x F d. \<lbrakk>finite F; x \<notin> F; \<And>d. F \<noteq> {} \<Longrightarrow> card (deg_sect F d) = d + (card F - 1) choose (card F - 1); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> card (deg_sect (insert x F) d) = d + (card (insert x F) - 1) choose (card (insert x F) - 1)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<noteq> {}

goal (2 subgoals):
 1. \<And>d. {} \<noteq> {} \<Longrightarrow> card (deg_sect {} d) = d + (card {} - 1) choose (card {} - 1)
 2. \<And>x F d. \<lbrakk>finite F; x \<notin> F; \<And>d. F \<noteq> {} \<Longrightarrow> card (deg_sect F d) = d + (card F - 1) choose (card F - 1); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> card (deg_sect (insert x F) d) = d + (card (insert x F) - 1) choose (card (insert x F) - 1)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
{} \<noteq> {}

goal (1 subgoal):
 1. card (deg_sect {} d) = d + (card {} - 1) choose (card {} - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (deg_sect {} d) = d + (card {} - 1) choose (card {} - 1)

goal (1 subgoal):
 1. \<And>x F d. \<lbrakk>finite F; x \<notin> F; \<And>d. F \<noteq> {} \<Longrightarrow> card (deg_sect F d) = d + (card F - 1) choose (card F - 1); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> card (deg_sect (insert x F) d) = d + (card (insert x F) - 1) choose (card (insert x F) - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F d. \<lbrakk>finite F; x \<notin> F; \<And>d. F \<noteq> {} \<Longrightarrow> card (deg_sect F d) = d + (card F - 1) choose (card F - 1); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> card (deg_sect (insert x F) d) = d + (card (insert x F) - 1) choose (card (insert x F) - 1)
[PROOF STEP]
case (insert x X)
[PROOF STATE]
proof (state)
this:
finite X
x \<notin> X
X \<noteq> {} \<Longrightarrow> card (deg_sect X ?d) = ?d + (card X - 1) choose (card X - 1)
insert x X \<noteq> {}

goal (1 subgoal):
 1. \<And>x F d. \<lbrakk>finite F; x \<notin> F; \<And>d. F \<noteq> {} \<Longrightarrow> card (deg_sect F d) = d + (card F - 1) choose (card F - 1); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> card (deg_sect (insert x F) d) = d + (card (insert x F) - 1) choose (card (insert x F) - 1)
[PROOF STEP]
from insert(1, 2)
[PROOF STATE]
proof (chain)
picking this:
finite X
x \<notin> X
[PROOF STEP]
have eq1: "card (insert x X) = Suc (card X)"
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X

goal (1 subgoal):
 1. card (insert x X) = Suc (card X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (insert x X) = Suc (card X)

goal (1 subgoal):
 1. \<And>x F d. \<lbrakk>finite F; x \<notin> F; \<And>d. F \<noteq> {} \<Longrightarrow> card (deg_sect F d) = d + (card F - 1) choose (card F - 1); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> card (deg_sect (insert x F) d) = d + (card (insert x F) - 1) choose (card (insert x F) - 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
proof (cases "X = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X = {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
 2. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
X = {}

goal (2 subgoals):
 1. X = {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
 2. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X = {}

goal (1 subgoal):
 1. card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
X \<noteq> {}

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
with insert.hyps(1)
[PROOF STATE]
proof (chain)
picking this:
finite X
X \<noteq> {}
[PROOF STEP]
have "0 < card X"
[PROOF STATE]
proof (prove)
using this:
finite X
X \<noteq> {}

goal (1 subgoal):
 1. 0 < card X
[PROOF STEP]
by (simp add: card_gt_0_iff)
[PROOF STATE]
proof (state)
this:
0 < card X

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
let ?f = "\<lambda>d0. Poly_Mapping.single x (d - d0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> {}
[PROOF STEP]
have eq2: "card (deg_sect X d0) = d0 + (card X - 1) choose (card X - 1)" for d0
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {}

goal (1 subgoal):
 1. card (deg_sect X d0) = d0 + (card X - 1) choose (card X - 1)
[PROOF STEP]
by (rule insert.hyps)
[PROOF STATE]
proof (state)
this:
card (deg_sect X ?d0.0) = ?d0.0 + (card X - 1) choose (card X - 1)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
have "finite {..d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {..d}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {..d}

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {..d}

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
from insert.hyps(1)
[PROOF STATE]
proof (chain)
picking this:
finite X
[PROOF STEP]
have "\<forall>d0\<in>{..d}. finite ((+) (?f d0) ` deg_sect X d0)"
[PROOF STATE]
proof (prove)
using this:
finite X

goal (1 subgoal):
 1. \<forall>d0\<in>{..d}. finite ((+) (monomial (d - d0) x) ` deg_sect X d0)
[PROOF STEP]
by (simp add: finite_deg_sect)
[PROOF STATE]
proof (state)
this:
\<forall>d0\<in>{..d}. finite ((+) (monomial (d - d0) x) ` deg_sect X d0)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>d0\<in>{..d}. finite ((+) (monomial (d - d0) x) ` deg_sect X d0)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
have "\<forall>d0\<in>{..d}. \<forall>d1\<in>{..d}. d0 \<noteq> d1 \<longrightarrow>
                          ((+) (?f d0) ` deg_sect X d0) \<inter> ((+) (?f d1) ` deg_sect X d1) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d0\<in>{..d}. \<forall>d1\<in>{..d}. d0 \<noteq> d1 \<longrightarrow> (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 = {}
[PROOF STEP]
proof (intro ballI impI, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix d1 d2 :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "d1 \<noteq> d2"
[PROOF STATE]
proof (state)
this:
d1 \<noteq> d2

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "((+) (?f d1) ` deg_sect X d1) \<inter> ((+) (?f d2) ` deg_sect X d2) \<noteq> {}"
[PROOF STATE]
proof (state)
this:
(+) (monomial (d - d1) x) ` deg_sect X d1 \<inter> (+) (monomial (d - d2) x) ` deg_sect X d2 \<noteq> {}

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(+) (monomial (d - d1) x) ` deg_sect X d1 \<inter> (+) (monomial (d - d2) x) ` deg_sect X d2 \<noteq> {}
[PROOF STEP]
obtain t where "t \<in> ((+) (?f d1) ` deg_sect X d1) \<inter> ((+) (?f d2) ` deg_sect X d2)"
[PROOF STATE]
proof (prove)
using this:
(+) (monomial (d - d1) x) ` deg_sect X d1 \<inter> (+) (monomial (d - d2) x) ` deg_sect X d2 \<noteq> {}

goal (1 subgoal):
 1. (\<And>t. t \<in> (+) (monomial (d - d1) x) ` deg_sect X d1 \<inter> (+) (monomial (d - d2) x) ` deg_sect X d2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> (+) (monomial (d - d1) x) ` deg_sect X d1 \<inter> (+) (monomial (d - d2) x) ` deg_sect X d2

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence t1: "t \<in> (+) (?f d1) ` deg_sect X d1" and t2: "t \<in> (+) (?f d2) ` deg_sect X d2"
[PROOF STATE]
proof (prove)
using this:
t \<in> (+) (monomial (d - d1) x) ` deg_sect X d1 \<inter> (+) (monomial (d - d2) x) ` deg_sect X d2

goal (1 subgoal):
 1. t \<in> (+) (monomial (d - d1) x) ` deg_sect X d1 &&& t \<in> (+) (monomial (d - d2) x) ` deg_sect X d2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
t \<in> (+) (monomial (d - d1) x) ` deg_sect X d1
t \<in> (+) (monomial (d - d2) x) ` deg_sect X d2

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from t1
[PROOF STATE]
proof (chain)
picking this:
t \<in> (+) (monomial (d - d1) x) ` deg_sect X d1
[PROOF STEP]
obtain s1 where "s1 \<in> deg_sect X d1" and s1: "t = ?f d1 + s1"
[PROOF STATE]
proof (prove)
using this:
t \<in> (+) (monomial (d - d1) x) ` deg_sect X d1

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> deg_sect X d1; t = monomial (d - d1) x + s1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s1 \<in> deg_sect X d1
t = monomial (d - d1) x + s1

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
s1 \<in> deg_sect X d1
[PROOF STEP]
have "s1 \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
s1 \<in> deg_sect X d1

goal (1 subgoal):
 1. s1 \<in> .[X]
[PROOF STEP]
by (rule deg_sectD)
[PROOF STATE]
proof (state)
this:
s1 \<in> .[X]

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "keys s1 \<subseteq> X"
[PROOF STATE]
proof (prove)
using this:
s1 \<in> .[X]

goal (1 subgoal):
 1. keys s1 \<subseteq> X
[PROOF STEP]
by (rule PPsD)
[PROOF STATE]
proof (state)
this:
keys s1 \<subseteq> X

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with insert.hyps(2)
[PROOF STATE]
proof (chain)
picking this:
x \<notin> X
keys s1 \<subseteq> X
[PROOF STEP]
have eq3: "lookup s1 x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<notin> X
keys s1 \<subseteq> X

goal (1 subgoal):
 1. lookup s1 x = 0
[PROOF STEP]
by (auto simp: in_keys_iff)
[PROOF STATE]
proof (state)
this:
lookup s1 x = 0

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from t2
[PROOF STATE]
proof (chain)
picking this:
t \<in> (+) (monomial (d - d2) x) ` deg_sect X d2
[PROOF STEP]
obtain s2 where "s2 \<in> deg_sect X d2" and s2: "t = ?f d2 + s2"
[PROOF STATE]
proof (prove)
using this:
t \<in> (+) (monomial (d - d2) x) ` deg_sect X d2

goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>s2 \<in> deg_sect X d2; t = monomial (d - d2) x + s2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s2 \<in> deg_sect X d2
t = monomial (d - d2) x + s2

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
s2 \<in> deg_sect X d2
[PROOF STEP]
have "s2 \<in> .[X]"
[PROOF STATE]
proof (prove)
using this:
s2 \<in> deg_sect X d2

goal (1 subgoal):
 1. s2 \<in> .[X]
[PROOF STEP]
by (rule deg_sectD)
[PROOF STATE]
proof (state)
this:
s2 \<in> .[X]

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "keys s2 \<subseteq> X"
[PROOF STATE]
proof (prove)
using this:
s2 \<in> .[X]

goal (1 subgoal):
 1. keys s2 \<subseteq> X
[PROOF STEP]
by (rule PPsD)
[PROOF STATE]
proof (state)
this:
keys s2 \<subseteq> X

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with insert.hyps(2)
[PROOF STATE]
proof (chain)
picking this:
x \<notin> X
keys s2 \<subseteq> X
[PROOF STEP]
have eq4: "lookup s2 x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<notin> X
keys s2 \<subseteq> X

goal (1 subgoal):
 1. lookup s2 x = 0
[PROOF STEP]
by (auto simp: in_keys_iff)
[PROOF STATE]
proof (state)
this:
lookup s2 x = 0

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from s2
[PROOF STATE]
proof (chain)
picking this:
t = monomial (d - d2) x + s2
[PROOF STEP]
have "lookup (?f d1 + s1) x = lookup (?f d2 + s2) x"
[PROOF STATE]
proof (prove)
using this:
t = monomial (d - d2) x + s2

goal (1 subgoal):
 1. lookup (monomial (d - d1) x + s1) x = lookup (monomial (d - d2) x + s2) x
[PROOF STEP]
by (simp only: s1)
[PROOF STATE]
proof (state)
this:
lookup (monomial (d - d1) x + s1) x = lookup (monomial (d - d2) x + s2) x

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "d - d1 = d - d2"
[PROOF STATE]
proof (prove)
using this:
lookup (monomial (d - d1) x + s1) x = lookup (monomial (d - d2) x + s2) x

goal (1 subgoal):
 1. d - d1 = d - d2
[PROOF STEP]
by (simp add: lookup_add eq3 eq4)
[PROOF STATE]
proof (state)
this:
d - d1 = d - d2

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d - d1 = d - d2

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "d1 \<in> {..d}" and "d2 \<in> {..d}"
[PROOF STATE]
proof (state)
this:
d1 \<in> {..d}
d2 \<in> {..d}

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d - d1 = d - d2
d1 \<in> {..d}
d2 \<in> {..d}
[PROOF STEP]
have "d1 = d2"
[PROOF STATE]
proof (prove)
using this:
d - d1 = d - d2
d1 \<in> {..d}
d2 \<in> {..d}

goal (1 subgoal):
 1. d1 = d2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d1 = d2

goal (1 subgoal):
 1. \<And>d0 d1. \<lbrakk>d0 \<in> {..d}; d1 \<in> {..d}; d0 \<noteq> d1; (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>d1 \<noteq> d2\<close>
[PROOF STATE]
proof (chain)
picking this:
d1 \<noteq> d2
d1 = d2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
d1 \<noteq> d2
d1 = d2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>d0\<in>{..d}. \<forall>d1\<in>{..d}. d0 \<noteq> d1 \<longrightarrow> (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 = {}

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {..d}
\<forall>d0\<in>{..d}. finite ((+) (monomial (d - d0) x) ` deg_sect X d0)
\<forall>d0\<in>{..d}. \<forall>d1\<in>{..d}. d0 \<noteq> d1 \<longrightarrow> (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 = {}
[PROOF STEP]
have "card (deg_sect (insert x X) d) =
                       (\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0))"
[PROOF STATE]
proof (prove)
using this:
finite {..d}
\<forall>d0\<in>{..d}. finite ((+) (monomial (d - d0) x) ` deg_sect X d0)
\<forall>d0\<in>{..d}. \<forall>d1\<in>{..d}. d0 \<noteq> d1 \<longrightarrow> (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 = {}

goal (1 subgoal):
 1. card (deg_sect (insert x X) d) = (\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0))
[PROOF STEP]
unfolding deg_sect_insert
[PROOF STATE]
proof (prove)
using this:
finite {..d}
\<forall>d0\<in>{..d}. finite ((+) (monomial (d - d0) x) ` deg_sect X d0)
\<forall>d0\<in>{..d}. \<forall>d1\<in>{..d}. d0 \<noteq> d1 \<longrightarrow> (+) (monomial (d - d0) x) ` deg_sect X d0 \<inter> (+) (monomial (d - d1) x) ` deg_sect X d1 = {}

goal (1 subgoal):
 1. card (\<Union>d0\<le>d. (+) (monomial (d - d0) x) ` deg_sect X d0) = (\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0))
[PROOF STEP]
by (rule card_UN_disjoint)
[PROOF STATE]
proof (state)
this:
card (deg_sect (insert x X) d) = (\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0))

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (deg_sect (insert x X) d) = (\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0))

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
from refl
[PROOF STATE]
proof (chain)
picking this:
?t = ?t
[PROOF STEP]
have "... = (\<Sum>d0\<le>d. card (deg_sect X d0))"
[PROOF STATE]
proof (prove)
using this:
?t = ?t

goal (1 subgoal):
 1. (\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0)) = (\<Sum>d0\<le>d. card (deg_sect X d0))
[PROOF STEP]
proof (rule sum.cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..d} \<Longrightarrow> card ((+) (monomial (d - xa) x) ` deg_sect X xa) = card (deg_sect X xa)
[PROOF STEP]
fix d0
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..d} \<Longrightarrow> card ((+) (monomial (d - xa) x) ` deg_sect X xa) = card (deg_sect X xa)
[PROOF STEP]
have "inj_on ((+) (monomial (d - d0) x)) (deg_sect X d0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ((+) (monomial (d - d0) x)) (deg_sect X d0)
[PROOF STEP]
by (rule, rule add_left_imp_eq)
[PROOF STATE]
proof (state)
this:
inj_on ((+) (monomial (d - d0) x)) (deg_sect X d0)

goal (1 subgoal):
 1. \<And>xa. xa \<in> {..d} \<Longrightarrow> card ((+) (monomial (d - xa) x) ` deg_sect X xa) = card (deg_sect X xa)
[PROOF STEP]
thus "card ((+) (monomial (d - d0) x) ` deg_sect X d0) = card (deg_sect X d0)"
[PROOF STATE]
proof (prove)
using this:
inj_on ((+) (monomial (d - d0) x)) (deg_sect X d0)

goal (1 subgoal):
 1. card ((+) (monomial (d - d0) x) ` deg_sect X d0) = card (deg_sect X d0)
[PROOF STEP]
by (rule card_image)
[PROOF STATE]
proof (state)
this:
card ((+) (monomial (d - d0) x) ` deg_sect X d0) = card (deg_sect X d0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0)) = (\<Sum>d0\<le>d. card (deg_sect X d0))

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card ((+) (monomial (d - d0) x) ` deg_sect X d0)) = (\<Sum>d0\<le>d. card (deg_sect X d0))

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
have "... = (\<Sum>d0\<le>d. (card X - 1) + d0 choose (card X - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d0\<le>d. card (deg_sect X d0)) = (\<Sum>d0\<le>d. card X - 1 + d0 choose (card X - 1))
[PROOF STEP]
by (simp only: eq2 add.commute)
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card (deg_sect X d0)) = (\<Sum>d0\<le>d. card X - 1 + d0 choose (card X - 1))

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card (deg_sect X d0)) = (\<Sum>d0\<le>d. card X - 1 + d0 choose (card X - 1))

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
have "... = (\<Sum>d0\<le>d. (card X - 1) + d0 choose d0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d0\<le>d. card X - 1 + d0 choose (card X - 1)) = (\<Sum>d0\<le>d. card X - 1 + d0 choose d0)
[PROOF STEP]
by (simp only: binomial_symmetric_plus)
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card X - 1 + d0 choose (card X - 1)) = (\<Sum>d0\<le>d. card X - 1 + d0 choose d0)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card X - 1 + d0 choose (card X - 1)) = (\<Sum>d0\<le>d. card X - 1 + d0 choose d0)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
have "... = Suc ((card X - 1) + d) choose d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d0\<le>d. card X - 1 + d0 choose d0) = Suc (card X - 1 + d) choose d
[PROOF STEP]
by (rule sum_choose_lower)
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card X - 1 + d0 choose d0) = Suc (card X - 1 + d) choose d

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d0\<le>d. card X - 1 + d0 choose d0) = Suc (card X - 1 + d) choose d

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
from \<open>0 < card X\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < card X
[PROOF STEP]
have "... = d + (card (insert x X) - 1) choose d"
[PROOF STATE]
proof (prove)
using this:
0 < card X

goal (1 subgoal):
 1. Suc (card X - 1 + d) choose d = d + (card (insert x X) - 1) choose d
[PROOF STEP]
by (simp add: eq1 add.commute)
[PROOF STATE]
proof (state)
this:
Suc (card X - 1 + d) choose d = d + (card (insert x X) - 1) choose d

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (card X - 1 + d) choose d = d + (card (insert x X) - 1) choose d

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
have "... = d + (card (insert x X) - 1) choose (card (insert x X) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d + (card (insert x X) - 1) choose d = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
by (fact binomial_symmetric_plus)
[PROOF STATE]
proof (state)
this:
d + (card (insert x X) - 1) choose d = d + (card (insert x X) - 1) choose (card (insert x X) - 1)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)

goal (1 subgoal):
 1. card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (deg_sect (insert x X) d) = d + (card (insert x X) - 1) choose (card (insert x X) - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma span_code [code]:
  "span P [] = ([], [])"
  "span P (x # xs) =
    (if P x then let (ys, zs) = span P xs in (x # ys, zs) else ([], x # xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. span P [] = ([], []) &&& span P (x # xs) = (if P x then let (ys, zs) = span P xs in (x # ys, zs) else ([], x # xs))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma push_list [simp]: "list (push x stack) = x # list stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list (push x stack) = x # list stack
[PROOF STEP]
by(cases stack) auto


[STATEMENT]
lemma pop_list [simp]: "\<not> is_empty stack \<Longrightarrow> list (pop stack) = tl (list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_empty stack \<Longrightarrow> list (pop stack) = tl (list stack)
[PROOF STEP]
by(induction stack rule: pop.induct) auto


[STATEMENT]
lemma first_list [simp]: "\<not> is_empty stack \<Longrightarrow> first stack = hd (list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_empty stack \<Longrightarrow> first stack = hd (list stack)
[PROOF STEP]
by(induction stack rule: first.induct) auto


[STATEMENT]
lemma list_empty: "list stack = [] \<longleftrightarrow> is_empty stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list stack = []) = is_empty stack
[PROOF STEP]
by(induction stack rule: is_empty_stack.induct) auto


[STATEMENT]
lemma list_not_empty: "list stack  \<noteq> [] \<longleftrightarrow> \<not> is_empty stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list stack \<noteq> []) = (\<not> is_empty stack)
[PROOF STEP]
by(induction stack rule: is_empty_stack.induct) auto


[STATEMENT]
lemma list_empty_2 [simp]: "\<lbrakk>list stack \<noteq> []; is_empty stack\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list stack \<noteq> []; is_empty stack\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: list_empty)


[STATEMENT]
lemma list_not_empty_2 [simp]:"\<lbrakk>list stack = []; \<not> is_empty stack\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list stack = []; \<not> is_empty stack\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: list_empty)


[STATEMENT]
lemma list_empty_size: "list stack = [] \<longleftrightarrow> size stack = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list stack = []) = (size stack = 0)
[PROOF STEP]
by(induction stack) auto


[STATEMENT]
lemma list_not_empty_size:"list stack \<noteq> [] \<longleftrightarrow> 0 < size stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list stack \<noteq> []) = (0 < size stack)
[PROOF STEP]
by(induction stack) auto


[STATEMENT]
lemma list_empty_size_2 [simp]: "\<lbrakk>list stack \<noteq> []; size stack = 0\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list stack \<noteq> []; size stack = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: list_empty_size)


[STATEMENT]
lemma list_not_empty_size_2 [simp]:"\<lbrakk>list stack = []; 0 < size stack\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list stack = []; 0 < size stack\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: list_empty_size)


[STATEMENT]
lemma size_push [simp]: "size (push x stack) = Suc (size stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (push x stack) = Suc (size stack)
[PROOF STEP]
by(cases stack) auto


[STATEMENT]
lemma size_pop [simp]: "size (pop stack) = size stack - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (pop stack) = size stack - Suc 0
[PROOF STEP]
by(induction stack rule: pop.induct) auto


[STATEMENT]
lemma size_empty: "size (stack :: 'a stack) = 0 \<longleftrightarrow> is_empty stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (size stack = 0) = is_empty stack
[PROOF STEP]
by(induction stack rule: is_empty_stack.induct) auto


[STATEMENT]
lemma size_not_empty: "size (stack :: 'a stack) > 0 \<longleftrightarrow> \<not> is_empty stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < size stack) = (\<not> is_empty stack)
[PROOF STEP]
by(induction stack rule: is_empty_stack.induct) auto


[STATEMENT]
lemma size_empty_2[simp]: "\<lbrakk>size (stack :: 'a stack) = 0; \<not>is_empty stack\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size stack = 0; \<not> is_empty stack\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: size_empty)


[STATEMENT]
lemma size_not_empty_2[simp]: "\<lbrakk>0 < size (stack :: 'a stack); is_empty stack\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size stack; is_empty stack\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: size_not_empty)


[STATEMENT]
lemma size_list_length [simp]: "length (list stack) = size stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (list stack) = size stack
[PROOF STEP]
by(cases stack) auto


[STATEMENT]
lemma first_pop [simp]: "\<not> is_empty stack \<Longrightarrow> first stack # list (pop stack) = list stack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_empty stack \<Longrightarrow> first stack # list (pop stack) = list stack
[PROOF STEP]
by(induction stack rule: pop.induct) auto


[STATEMENT]
lemma push_not_empty [simp]: "\<lbrakk>\<not> is_empty stack; is_empty (push x stack)\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_empty stack; is_empty (push x stack)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(induction x stack rule: push.induct) auto


[STATEMENT]
lemma pop_list_length [simp]: "\<not> is_empty stack
   \<Longrightarrow> Suc (length (list (pop stack))) = length (list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_empty stack \<Longrightarrow> Suc (length (list (pop stack))) = length (list stack)
[PROOF STEP]
by(induction stack rule: pop.induct) auto


[STATEMENT]
lemma first_take: "\<not>is_empty stack \<Longrightarrow> [first stack] = take 1 (Stack.list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_empty stack \<Longrightarrow> [first stack] = take 1 (list stack)
[PROOF STEP]
by (simp add: list_empty)


[STATEMENT]
lemma first_take_tl [simp]: "0 < size big
   \<Longrightarrow> (first big # take count (tl (list big))) = take (Suc count) (list big)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < size big \<Longrightarrow> first big # take count (tl (list big)) = take (Suc count) (list big)
[PROOF STEP]
by(induction big rule: Stack.first.induct) auto


[STATEMENT]
lemma first_take_pop [simp]: "\<lbrakk>\<not>is_empty stack; 0 < x\<rbrakk>
   \<Longrightarrow> first stack # take (x - Suc 0) (list (pop stack)) = take x (list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_empty stack; 0 < x\<rbrakk> \<Longrightarrow> first stack # take (x - Suc 0) (list (pop stack)) = take x (list stack)
[PROOF STEP]
by(induction stack rule: pop.induct) (auto simp: take_Cons')


[STATEMENT]
lemma [simp]: "first (Stack [] []) = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. first (Stack [] []) = undefined
[PROOF STEP]
by (meson first.elims list.distinct(1) stack.inject)


[STATEMENT]
lemma first_hd: "Stack.first stack = hd (Stack.list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. first stack = hd (list stack)
[PROOF STEP]
by(induction stack rule: first.induct)(auto simp: hd_def)


[STATEMENT]
lemma pop_tl [simp]: "list (pop stack) = tl (list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list (pop stack) = tl (list stack)
[PROOF STEP]
by(induction stack rule: pop.induct) auto


[STATEMENT]
lemma pop_drop: "list (pop stack) = drop 1 (list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list (pop stack) = drop 1 (list stack)
[PROOF STEP]
by (simp add: drop_Suc)


[STATEMENT]
lemma popN_drop [simp]: "list ((pop ^^ n) stack) = drop n (list stack)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list ((pop ^^ n) stack) = drop n (list stack)
[PROOF STEP]
by(induction n)(auto simp: drop_Suc tl_drop)


[STATEMENT]
lemma popN_size [simp]: "size ((pop ^^ n) stack) = (size stack) - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size ((pop ^^ n) stack) = size stack - n
[PROOF STEP]
by(induction n) auto


[STATEMENT]
lemma take_first: "\<lbrakk>0 < size s1; 0 < size s2; take (size s1) (list s2) = take (size s2) (list s1)\<rbrakk>
    \<Longrightarrow> first s1 = first s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size s1; 0 < size s2; take (size s1) (list s2) = take (size s2) (list s1)\<rbrakk> \<Longrightarrow> first s1 = first s2
[PROOF STEP]
by(induction s1 rule: first.induct; induction s2 rule: first.induct) auto


[STATEMENT]
lemma length_mat_to_cols_list [simp]:
  "length (mat_to_cols_list A) = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mat_to_cols_list A) = dim_col A
[PROOF STEP]
by (simp add: mat_to_cols_list_def)


[STATEMENT]
lemma length_cols_mat_to_cols_list [simp]:
  assumes "j < dim_col A"
  shows "length [A $$ (i,j) . i <- [0..< dim_row A]] = dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. A $$ (i, j)) [0..<dim_row A]) = dim_row A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j < dim_col A

goal (1 subgoal):
 1. length (map (\<lambda>i. A $$ (i, j)) [0..<dim_row A]) = dim_row A
[PROOF STEP]
by simp


[STATEMENT]
lemma length_row_mat_to_cols_list [simp]:
  assumes "i < dim_row A"
  shows "length (row (mat_to_cols_list A) i) = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Matrix_Legacy.row (mat_to_cols_list A) i) = dim_col A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < dim_row A

goal (1 subgoal):
 1. length (Matrix_Legacy.row (mat_to_cols_list A) i) = dim_col A
[PROOF STEP]
by (simp add: row_def)


[STATEMENT]
lemma length_col_mat_to_cols_list [simp]:
  assumes "j < dim_col A"
  shows "length (col (mat_to_cols_list A) j) = dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Matrix_Legacy.col (mat_to_cols_list A) j) = dim_row A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j < dim_col A

goal (1 subgoal):
 1. length (Matrix_Legacy.col (mat_to_cols_list A) j) = dim_row A
[PROOF STEP]
by (simp add: col_def mat_to_cols_list_def)


[STATEMENT]
lemma mat_to_cols_list_is_not_Nil [simp]:
  assumes "dim_col A > 0"
  shows "mat_to_cols_list A \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list A \<noteq> []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < dim_col A

goal (1 subgoal):
 1. mat_to_cols_list A \<noteq> []
[PROOF STEP]
by (simp add: mat_to_cols_list_def)


[STATEMENT]
lemma row_length_mat_to_cols_list [simp]:
  assumes "dim_col A > 0"
  shows "mult.row_length (mat_to_cols_list A) = dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult.row_length (mat_to_cols_list A) = dim_row A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult.row_length (mat_to_cols_list A) = dim_row A
[PROOF STEP]
have "mat_to_cols_list A \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_to_cols_list A \<noteq> []
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
mat_to_cols_list A \<noteq> []

goal (1 subgoal):
 1. mult.row_length (mat_to_cols_list A) = dim_row A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat_to_cols_list A \<noteq> []
[PROOF STEP]
have "mult.row_length (mat_to_cols_list A) = length (hd (mat_to_cols_list A))"
[PROOF STATE]
proof (prove)
using this:
mat_to_cols_list A \<noteq> []

goal (1 subgoal):
 1. mult.row_length (mat_to_cols_list A) = length (hd (mat_to_cols_list A))
[PROOF STEP]
using mult.row_length_def[of "1" "(*)"]
[PROOF STATE]
proof (prove)
using this:
mat_to_cols_list A \<noteq> []
Matrix_Tensor.mult (1::?'a1) (*) \<Longrightarrow> mult.row_length ?xs \<equiv> if ?xs = [] then 0 else length (hd ?xs)

goal (1 subgoal):
 1. mult.row_length (mat_to_cols_list A) = length (hd (mat_to_cols_list A))
[PROOF STEP]
by (simp add: \<open>\<And>xs. Matrix_Tensor.mult 1 (*) \<Longrightarrow> mult.row_length xs \<equiv> if xs = [] then 0 else length (hd xs)\<close> mult.intro)
[PROOF STATE]
proof (state)
this:
mult.row_length (mat_to_cols_list A) = length (hd (mat_to_cols_list A))

goal (1 subgoal):
 1. mult.row_length (mat_to_cols_list A) = dim_row A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mult.row_length (mat_to_cols_list A) = length (hd (mat_to_cols_list A))

goal (1 subgoal):
 1. mult.row_length (mat_to_cols_list A) = dim_row A
[PROOF STEP]
by (simp add: assms mat_to_cols_list_def upt_conv_Cons)
[PROOF STATE]
proof (state)
this:
mult.row_length (mat_to_cols_list A) = dim_row A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_to_cols_list_is_mat [simp]:
  assumes "dim_col A > 0"
  shows "mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
[PROOF STEP]
have "Ball (set (mat_to_cols_list A)) (Matrix_Legacy.vec (mult.row_length (mat_to_cols_list A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (set (mat_to_cols_list A)) (Matrix_Legacy.vec (mult.row_length (mat_to_cols_list A)))
[PROOF STEP]
using assms row_length_mat_to_cols_list mat_to_cols_list_def Ball_def set_def vec_def
[PROOF STATE]
proof (prove)
using this:
0 < dim_col A
0 < dim_col ?A \<Longrightarrow> mult.row_length (mat_to_cols_list ?A) = dim_row ?A
mat_to_cols_list ?A = map (\<lambda>j. map (\<lambda>i. ?A $$ (i, j)) [0..<dim_row ?A]) [0..<dim_col ?A]
Ball ?A ?P = (\<forall>x. x \<in> ?A \<longrightarrow> ?P x)
set \<equiv> ctor_fold_list (\<lambda>z. set1_pre_list z \<union> \<Union> (set2_pre_list z))
Matrix_Legacy.vec ?n ?x = (length ?x = ?n)

goal (1 subgoal):
 1. Ball (set (mat_to_cols_list A)) (Matrix_Legacy.vec (mult.row_length (mat_to_cols_list A)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Ball (set (mat_to_cols_list A)) (Matrix_Legacy.vec (mult.row_length (mat_to_cols_list A)))

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Ball (set (mat_to_cols_list A)) (Matrix_Legacy.vec (mult.row_length (mat_to_cols_list A)))

goal (1 subgoal):
 1. Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)
[PROOF STEP]
by(auto simp: mat_def)
[PROOF STATE]
proof (state)
this:
Matrix_Legacy.mat (mult.row_length (mat_to_cols_list A)) (length (mat_to_cols_list A)) (mat_to_cols_list A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_mat_of_cols_list [simp]:
  assumes "i < nr" and "j < length cs"
  shows "mat_of_cols_list nr cs $$ (i,j) = cs ! j ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list nr cs $$ (i, j) = cs ! j ! i
[PROOF STEP]
by (simp add: assms mat_of_cols_list_def)


[STATEMENT]
lemma mat_to_cols_list_to_mat [simp]:
  "mat_of_cols_list (dim_row A) (mat_to_cols_list A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) = A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) $$ (i, j) = A $$ (i, j)
 2. dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_row A
 3. dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_col A
[PROOF STEP]
show f1:"dim_row (mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_row A
[PROOF STEP]
by (simp add: mat_of_cols_list_def)
[PROOF STATE]
proof (state)
this:
dim_row (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_row A

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) $$ (i, j) = A $$ (i, j)
 2. dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_col A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) $$ (i, j) = A $$ (i, j)
 2. dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_col A
[PROOF STEP]
show f2:"dim_col (mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_col A
[PROOF STEP]
by (simp add: Tensor.mat_of_cols_list_def)
[PROOF STATE]
proof (state)
this:
dim_col (Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A)) = dim_col A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) $$ (i, j) = A $$ (i, j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) $$ (i, j) = A $$ (i, j)
[PROOF STEP]
show "\<And>i j. i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow>
    (mat_of_cols_list (dim_row A) (mat_to_cols_list A)) $$ (i, j) = A $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) $$ (i, j) = A $$ (i, j)
[PROOF STEP]
by (simp add: mat_of_cols_list_def mat_to_cols_list_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim_row A; ?j < dim_col A\<rbrakk> \<Longrightarrow> Tensor.mat_of_cols_list (dim_row A) (mat_to_cols_list A) $$ (?i, ?j) = A $$ (?i, ?j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plus_mult_cpx [simp]:
  "plus_mult 1 (*) 0 (+) (a_inv cpx_rng)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plus_mult 1 (*) 0 (+) (a_inv cpx_rng)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>a b. a * b = b * a
 2. \<And>a b c. a * b * c = a * (b * c)
 3. \<And>x. 1 * x = x
 4. \<And>x. x * 1 = x
 5. \<And>a b. a + b = b + a
 6. \<And>a b c. a + b + c = a + (b + c)
 7. \<And>x. 0 + x = x
 8. \<And>x. x + 0 = x
 9. \<And>a b c. a * (b + c) = a * b + a * c
 10. \<And>a b c. (a + b) * c = a * c + b * c
A total of 12 subgoals...
[PROOF STEP]
apply (auto intro: cpx_cring_is_field simp: field_simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
 2. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
 2. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
[PROOF STEP]
show "\<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
[PROOF STEP]
using group.r_inv[of "cpx_rng"] cpx_cring_is_field field_def domain_def cpx_rng_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Group.group cpx_rng; ?x \<in> carrier cpx_rng\<rbrakk> \<Longrightarrow> ?x \<otimes>\<^bsub>cpx_rng\<^esub> inv\<^bsub>cpx_rng\<^esub> ?x = \<one>\<^bsub>cpx_rng\<^esub>
field cpx_rng
field ?R \<equiv> domain ?R \<and> field_axioms ?R
domain ?R \<equiv> cring ?R \<and> domain_axioms ?R
cpx_rng \<equiv> \<lparr>carrier = UNIV, monoid.mult = (*), one = 1, zero = 0, add = (+)\<rparr>

goal (1 subgoal):
 1. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
[PROOF STEP]
by (metis UNIV_I cring.cring_simprules(17) ordered_semiring_record_simps(1)
        ordered_semiring_record_simps(11) ordered_semiring_record_simps(12))
[PROOF STATE]
proof (state)
this:
?x + \<ominus>\<^bsub>cpx_rng\<^esub> ?x = 0

goal (1 subgoal):
 1. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
[PROOF STEP]
show "\<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
[PROOF STEP]
using group.r_inv[of "cpx_rng"] cpx_cring_is_field field_def domain_def cpx_rng_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Group.group cpx_rng; ?x \<in> carrier cpx_rng\<rbrakk> \<Longrightarrow> ?x \<otimes>\<^bsub>cpx_rng\<^esub> inv\<^bsub>cpx_rng\<^esub> ?x = \<one>\<^bsub>cpx_rng\<^esub>
field cpx_rng
field ?R \<equiv> domain ?R \<and> field_axioms ?R
domain ?R \<equiv> cring ?R \<and> domain_axioms ?R
cpx_rng \<equiv> \<lparr>carrier = UNIV, monoid.mult = (*), one = 1, zero = 0, add = (+)\<rparr>

goal (1 subgoal):
 1. \<And>x. x + \<ominus>\<^bsub>cpx_rng\<^esub> x = 0
[PROOF STEP]
by (metis UNIV_I cring.cring_simprules(17) ordered_semiring_record_simps(1)
        ordered_semiring_record_simps(11) ordered_semiring_record_simps(12))
[PROOF STATE]
proof (state)
this:
?x + \<ominus>\<^bsub>cpx_rng\<^esub> ?x = 0

goal:
No subgoals!
[PROOF STEP]
qed