[STATEMENT]
lemma vdw_imp_vdw_lemma:
  fixes l
  assumes vdw_assms: "\<And>k'. k'>0 \<Longrightarrow> \<exists>n_k'. vdw k' l n_k'"
    and "l \<ge> 2"
    and "m > 0"
    and "k > 0"
  shows   "\<exists>N. vdw_lemma k m l N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. vdw_lemma k m l N
[PROOF STEP]
using \<open>m>0\<close> \<open>k>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < m
0 < k

goal (1 subgoal):
 1. \<exists>N. vdw_lemma k m l N
[PROOF STEP]
proof (induction m rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; 0 < y; 0 < k\<rbrakk> \<Longrightarrow> Ex (vdw_lemma k y l); 0 < x; 0 < k\<rbrakk> \<Longrightarrow> Ex (vdw_lemma k x l)
[PROOF STEP]
case (less m)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y < m; 0 < ?y; 0 < k\<rbrakk> \<Longrightarrow> \<exists>a. vdw_lemma k ?y l a
0 < m
0 < k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; 0 < y; 0 < k\<rbrakk> \<Longrightarrow> Ex (vdw_lemma k y l); 0 < x; 0 < k\<rbrakk> \<Longrightarrow> Ex (vdw_lemma k x l)
[PROOF STEP]
consider  "m=1" | "m>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = 1 \<Longrightarrow> thesis; 1 < m \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
0 < m
0 < k

goal (1 subgoal):
 1. \<lbrakk>m = 1 \<Longrightarrow> thesis; 1 < m \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>m = 1 \<Longrightarrow> ?thesis; 1 < m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; 0 < y; 0 < k\<rbrakk> \<Longrightarrow> Ex (vdw_lemma k y l); 0 < x; 0 < k\<rbrakk> \<Longrightarrow> Ex (vdw_lemma k x l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>m = 1 \<Longrightarrow> ?thesis; 1 < m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>m = 1 \<Longrightarrow> ?thesis; 1 < m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>a. vdw_lemma k m l a
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = 1 \<Longrightarrow> \<exists>a. vdw_lemma k m l a
 2. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
text \<open> Case $m=1$: Show \<open>vdw_lemma\<close> for arithmetic progression, Induction start. \<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = 1 \<Longrightarrow> \<exists>a. vdw_lemma k m l a
 2. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
assume "m = 1"
[PROOF STATE]
proof (state)
this:
m = 1

goal (2 subgoals):
 1. m = 1 \<Longrightarrow> \<exists>a. vdw_lemma k m l a
 2. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
obtain n where vdw: "vdw k l n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. vdw k l n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vdw_assms \<open>k>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < ?k' \<Longrightarrow> \<exists>n_k'. vdw ?k' l n_k'
0 < k

goal (1 subgoal):
 1. (\<And>n. vdw k l n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vdw k l n

goal (2 subgoals):
 1. m = 1 \<Longrightarrow> \<exists>a. vdw_lemma k m l a
 2. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
define N where "N = 2*n"
[PROOF STATE]
proof (state)
this:
N = 2 * n

goal (2 subgoals):
 1. m = 1 \<Longrightarrow> \<exists>a. vdw_lemma k m l a
 2. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
have "l>0" and "l>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < l &&& 1 < l
[PROOF STEP]
using \<open>l\<ge>2\<close>
[PROOF STATE]
proof (prove)
using this:
2 \<le> l

goal (1 subgoal):
 1. 0 < l &&& 1 < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < l
1 < l

goal (2 subgoals):
 1. m = 1 \<Longrightarrow> \<exists>a. vdw_lemma k m l a
 2. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
have "vdw_lemma k m l N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdw_lemma k m l N
[PROOF STEP]
unfolding vdw_lemma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b col. a + int N \<le> b + 1 \<and> col \<in> {a..b} \<rightarrow> {..<k} \<longrightarrow> (\<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))))
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
case (1 a b col)
[PROOF STATE]
proof (state)
this:
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
text \<open> Divide $[a..b]$ in two intervals $I_1$, $I_2$ of same length and obtain arithmetic
        progression of length $l$ in $I_1$. \<close>
[PROOF STATE]
proof (state)
this:
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have col_restr: "col \<in> {a..a + int n - 1} \<rightarrow> {..<k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col \<in> {a..a + int n - 1} \<rightarrow> {..<k}
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. col \<in> {a..a + int n - 1} \<rightarrow> {..<k}
[PROOF STEP]
by (auto simp: N_def)
[PROOF STATE]
proof (state)
this:
col \<in> {a..a + int n - 1} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
col \<in> {a..a + int n - 1} \<rightarrow> {..<k}
[PROOF STEP]
obtain j start step where prog:
        "j < k" "step > 0"
        "is_arith_prog_on l start step a (a + int n -1)"
        "arith_prog start step ` {..<l} \<subseteq>
          col -` {j} \<inter> {a..a + int n - 1}"
[PROOF STATE]
proof (prove)
using this:
col \<in> {a..a + int n - 1} \<rightarrow> {..<k}

goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k; 0 < step; is_arith_prog_on l start step a (a + int n - 1); arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..a + int n - 1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vdw 1
[PROOF STATE]
proof (prove)
using this:
col \<in> {a..a + int n - 1} \<rightarrow> {..<k}
vdw k l n
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k; 0 < step; is_arith_prog_on l start step a (a + int n - 1); arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..a + int n - 1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
col \<in> {a..a + int n - 1} \<rightarrow> {..<k}
vdw k l n
a + int (2 * n) \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k; 0 < step; is_arith_prog_on l start step a (a + int n - 1); arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..a + int n - 1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim vdwE)(auto simp:is_arith_prog_on_def)
[PROOF STATE]
proof (state)
this:
j < k
0 < step
is_arith_prog_on l start step a (a + int n - 1)
arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..a + int n - 1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have range_prog_lessThan_l:
        "arith_prog start step i \<in> {a..a + int n -1}" if "i < l" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + int n - 1}
[PROOF STEP]
using that prog
[PROOF STATE]
proof (prove)
using this:
i < l
j < k
0 < step
is_arith_prog_on l start step a (a + int n - 1)
arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..a + int n - 1}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + int n - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have "{a..a + int n-1}\<subseteq>{a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a..a + int n - 1} \<subseteq> {a..b}
[PROOF STEP]
using N_def "1"(1)
[PROOF STATE]
proof (prove)
using this:
N = 2 * n
a + int N \<le> b + 1

goal (1 subgoal):
 1. {a..a + int n - 1} \<subseteq> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a..a + int n - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{a..a + int n - 1} \<subseteq> {a..b}
[PROOF STEP]
have "a + 2* int n - 1 \<le> b"
[PROOF STATE]
proof (prove)
using this:
{a..a + int n - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. a + 2 * int n - 1 \<le> b
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
{a..a + int n - 1} \<subseteq> {a..b}
a + int N \<le> b + 1

goal (1 subgoal):
 1. a + 2 * int n - 1 \<le> b
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
{a..a + int n - 1} \<subseteq> {a..b}
a + int (2 * n) \<le> b + 1

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

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
text \<open> Show that \<open>arith_prog start step\<close> is an arithmetic progression of length $l+1$
         in $[a..b]$. \<close>
[PROOF STATE]
proof (state)
this:
a + 2 * int n - 1 \<le> b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have prog_in_ivl: "arith_prog start step i \<in> {a..b}"
        if "i \<le> l" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step i \<in> {a..b}
[PROOF STEP]
proof (cases "i=l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
 2. i \<noteq> l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> l

goal (2 subgoals):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
 2. i \<noteq> l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
have "i<l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < l
[PROOF STEP]
using that False
[PROOF STATE]
proof (prove)
using this:
i \<le> l
i \<noteq> l

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

goal (2 subgoals):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
 2. i \<noteq> l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < l

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..b}
[PROOF STEP]
using range_prog_lessThan_l \<open>{a..a + int n-1}\<subseteq>{a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
i < l
?i < l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + int n - 1}
{a..a + int n - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..b}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
arith_prog start step i \<in> {a..b}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = l

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
text \<open> Show $\<open>step\<close>\leq |I_1|$ then have \<open>arith_prog start step (l+1)\<in>[a..b]\<close> as
           \<open>arith_prog start step (l+1) = arith_prog start step l + step\<close> \<close>
[PROOF STATE]
proof (state)
this:
i = l

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
have "start \<in> {a..a + int n -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start \<in> {a..a + int n - 1}
[PROOF STEP]
using range_prog_lessThan_l[of 0]
[PROOF STATE]
proof (prove)
using this:
0 < l \<Longrightarrow> arith_prog start step 0 \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. start \<in> {a..a + int n - 1}
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
0 < l \<Longrightarrow> start + int (0 * step) \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. start \<in> {a..a + int n - 1}
[PROOF STEP]
by (simp add: \<open>0 < l\<close>)
[PROOF STATE]
proof (state)
this:
start \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
start \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
have "start + int step \<in> {a..a + int n -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int step \<in> {a..a + int n - 1}
[PROOF STEP]
using range_prog_lessThan_l[of 1]
[PROOF STATE]
proof (prove)
using this:
1 < l \<Longrightarrow> arith_prog start step 1 \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. start + int step \<in> {a..a + int n - 1}
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
1 < l \<Longrightarrow> start + int (1 * step) \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. start + int step \<in> {a..a + int n - 1}
[PROOF STEP]
by (metis \<open>1 < l\<close> mult.left_neutral)
[PROOF STATE]
proof (state)
this:
start + int step \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
start \<in> {a..a + int n - 1}
start + int step \<in> {a..a + int n - 1}
[PROOF STEP]
have "step \<le> n"
[PROOF STATE]
proof (prove)
using this:
start \<in> {a..a + int n - 1}
start + int step \<in> {a..a + int n - 1}

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

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
have "arith_prog start step (l-1) \<in> {a..a + int n -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step (l - 1) \<in> {a..a + int n - 1}
[PROOF STEP]
using range_prog_lessThan_l[of "l-1"]
[PROOF STATE]
proof (prove)
using this:
l - 1 < l \<Longrightarrow> arith_prog start step (l - 1) \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. arith_prog start step (l - 1) \<in> {a..a + int n - 1}
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
l - 1 < l \<Longrightarrow> start + int ((l - 1) * step) \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. start + int ((l - 1) * step) \<in> {a..a + int n - 1}
[PROOF STEP]
using \<open>0 < l\<close> diff_less less_numeral_extra(1)
[PROOF STATE]
proof (prove)
using this:
l - 1 < l \<Longrightarrow> start + int ((l - 1) * step) \<in> {a..a + int n - 1}
0 < l
\<lbrakk>0 < ?n; 0 < ?m\<rbrakk> \<Longrightarrow> ?m - ?n < ?m
(0::?'a) < (1::?'a)

goal (1 subgoal):
 1. start + int ((l - 1) * step) \<in> {a..a + int n - 1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
arith_prog start step (l - 1) \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arith_prog start step (l - 1) \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
have "arith_prog start step l =
                        arith_prog start step (l-1) + int step"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step l = arith_prog start step (l - 1) + int step
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int (l * step) = start + int ((l - 1) * step) + int step
[PROOF STEP]
using \<open>0 < l\<close> mult_eq_if
[PROOF STATE]
proof (prove)
using this:
0 < l
?m * ?n = (if ?m = 0 then 0 else ?n + (?m - 1) * ?n)

goal (1 subgoal):
 1. start + int (l * step) = start + int ((l - 1) * step) + int step
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
arith_prog start step l = arith_prog start step (l - 1) + int step

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arith_prog start step (l - 1) \<in> {a..a + int n - 1}
arith_prog start step l = arith_prog start step (l - 1) + int step
[PROOF STEP]
have "arith_prog start step l \<in> {a..b}"
[PROOF STATE]
proof (prove)
using this:
arith_prog start step (l - 1) \<in> {a..a + int n - 1}
arith_prog start step l = arith_prog start step (l - 1) + int step

goal (1 subgoal):
 1. arith_prog start step l \<in> {a..b}
[PROOF STEP]
using \<open>step\<le>n\<close> N_def \<open>a + 2* int n -1 \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
arith_prog start step (l - 1) \<in> {a..a + int n - 1}
arith_prog start step l = arith_prog start step (l - 1) + int step
step \<le> n
N = 2 * n
a + 2 * int n - 1 \<le> b

goal (1 subgoal):
 1. arith_prog start step l \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog start step l \<in> {a..b}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
arith_prog start step l \<in> {a..b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
arith_prog start step l \<in> {a..b}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..b}
[PROOF STEP]
using range_prog_lessThan_l
[PROOF STATE]
proof (prove)
using this:
arith_prog start step l \<in> {a..b}
?i < l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + int n - 1}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..b}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
arith_prog start step l \<in> {a..b}
?i < l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + int n - 1}
i = l

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..b}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
arith_prog start step i \<in> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<le> l \<Longrightarrow> arith_prog start step ?i \<in> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have col_prog_eq: "col (arith_prog start step k) = j"
        if "k < l" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (arith_prog start step k) = j
[PROOF STEP]
using prog that
[PROOF STATE]
proof (prove)
using this:
j < k
0 < step
is_arith_prog_on l start step a (a + int n - 1)
arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..a + int n - 1}
k < l

goal (1 subgoal):
 1. col (arith_prog start step k) = j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?k < l \<Longrightarrow> col (arith_prog start step ?k) = j

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
define steps :: "nat \<Rightarrow> nat" where steps_def: "steps = (\<lambda>i. step)"
[PROOF STATE]
proof (state)
this:
steps = (\<lambda>i. step)

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
define f where "f = multi_arith_prog 1 start steps"
[PROOF STATE]
proof (state)
this:
f = multi_arith_prog 1 start steps

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have rel_prop_1:
        "col (f c) = col (f (\<lambda>i. if i < s then 0 else c i))"
        if "c \<in> {0..<1} \<rightarrow> {0..l}" "s<1" "\<forall>j\<le>s. c j < l" for c s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (f c) = col (f (\<lambda>i. if i < s then 0 else c i))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {0..<1} \<rightarrow> {0..l}
s < 1
\<forall>j\<le>s. c j < l

goal (1 subgoal):
 1. col (f c) = col (f (\<lambda>i. if i < s then 0 else c i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> {0..<1} \<rightarrow> {0..l}; ?s < 1; \<forall>j\<le>?s. ?c j < l\<rbrakk> \<Longrightarrow> col (f ?c) = col (f (\<lambda>i. if i < ?s then 0 else ?c i))

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have arith_prog_on:
        "is_multi_arith_prog_on (l+1) m start steps a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start steps a b
[PROOF STEP]
using prog(3)
[PROOF STATE]
proof (prove)
using this:
is_arith_prog_on l start step a (a + int n - 1)

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start steps a b
[PROOF STEP]
unfolding is_arith_prog_on_def is_multi_arith_prog_on_def
[PROOF STATE]
proof (prove)
using this:
a \<le> start \<and> arith_prog start step (l - 1) \<le> a + int n - 1

goal (1 subgoal):
 1. a \<le> start \<and> multi_arith_prog m start steps (\<lambda>_. l + 1 - 1) \<le> b
[PROOF STEP]
using \<open>m=1\<close> arith_prog_to_multi steps_def prog_in_ivl
[PROOF STATE]
proof (prove)
using this:
a \<le> start \<and> arith_prog start step (l - 1) \<le> a + int n - 1
m = 1
arith_prog ?start ?step ?c = multi_arith_prog 1 ?start (\<lambda>_. ?step) (\<lambda>_. ?c)
steps = (\<lambda>i. step)
?i \<le> l \<Longrightarrow> arith_prog start step ?i \<in> {a..b}

goal (1 subgoal):
 1. a \<le> start \<and> multi_arith_prog m start steps (\<lambda>_. l + 1 - 1) \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_multi_arith_prog_on (l + 1) m start steps a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
by (rule exI[of _ start], rule exI[of _ steps])
           (use rel_prop_1 \<open>step > 0\<close> \<open>m = 1\<close> arith_prog_on col_prog_eq
             multi_to_arith_prog in \<open>auto simp: f_def Let_def steps_def\<close>)
[PROOF STATE]
proof (state)
this:
\<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vdw_lemma k m l N

goal (2 subgoals):
 1. m = 1 \<Longrightarrow> \<exists>a. vdw_lemma k m l a
 2. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vdw_lemma k m l N
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vdw_lemma k m l N

goal (1 subgoal):
 1. \<exists>a. vdw_lemma k m l a
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>a. vdw_lemma k m l a

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
text \<open> Case $m>1$: Show \<open>vdw_lemma\<close> for $m$-fold arithmetic progression,
          Induction step $(m-1) \longrightarrow m$. \<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
assume "m>1"
[PROOF STATE]
proof (state)
this:
1 < m

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
obtain q where vdw_lemma_IH:"vdw_lemma k (m-1) l q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. vdw_lemma k (m - 1) l q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>1 < m\<close> less
[PROOF STATE]
proof (prove)
using this:
1 < m
\<lbrakk>?y < m; 0 < ?y; 0 < k\<rbrakk> \<Longrightarrow> \<exists>a. vdw_lemma k ?y l a
0 < m
0 < k

goal (1 subgoal):
 1. (\<And>q. vdw_lemma k (m - 1) l q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vdw_lemma k (m - 1) l q

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
have "k^q>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k ^ q
[PROOF STEP]
using \<open>k>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. 0 < k ^ q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < k ^ q

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
obtain n_kq where vdw: "vdw (k^q) l n_kq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n_kq. vdw (k ^ q) l n_kq \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vdw_assms \<open>k^q>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < ?k' \<Longrightarrow> \<exists>n_k'. vdw ?k' l n_k'
0 < k ^ q

goal (1 subgoal):
 1. (\<And>n_kq. vdw (k ^ q) l n_kq \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vdw (k ^ q) l n_kq

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
define N where "N = q + 2 * n_kq"
[PROOF STATE]
proof (state)
this:
N = q + 2 * n_kq

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
text \<open>Idea: $[a..b] = I_1 \cup I_2$ where $|I_1| = 2*n_{k,q}$ and $|I_2| = q$.
                Divide $I_1$ into blocks of length $q$ and define a new colouring on the set of
                $q$-blocks where the colour of the block is the $k$-basis representation where
                the $i$-th digit corresponds to the colour of the $i$-th element in the block.
                Get an arithmetic progression of $q$-blocks of length $l+1$ in $I_1$, such that
                the first $l$ $q$-blocks have the same colour.
                The step of the block-arithmetic progression is going to be the additional
                step in the induction over $m$. \<close>
[PROOF STATE]
proof (state)
this:
N = q + 2 * n_kq

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
have "vdw_lemma k m l N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdw_lemma k m l N
[PROOF STEP]
unfolding vdw_lemma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b col. a + int N \<le> b + 1 \<and> col \<in> {a..b} \<rightarrow> {..<k} \<longrightarrow> (\<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))))
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
case (1 a b col)
[PROOF STATE]
proof (state)
this:
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have "n_kq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n_kq
[PROOF STEP]
using vdw_imp_pos vdw \<open>l\<ge>2\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vdw ?k ?l ?n; 0 < ?l\<rbrakk> \<Longrightarrow> 0 < ?n
vdw (k ^ q) l n_kq
2 \<le> l

goal (1 subgoal):
 1. 0 < n_kq
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n_kq

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < n_kq
[PROOF STEP]
have "N>0"
[PROOF STATE]
proof (prove)
using this:
0 < n_kq

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

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < N
[PROOF STEP]
have "a\<le>b"
[PROOF STATE]
proof (prove)
using this:
0 < N

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
0 < N
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

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

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
[PROOF STEP]
have "k>0"
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
a \<le> b
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
by (intro Nat.gr0I) force
[PROOF STATE]
proof (state)
this:
0 < k

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have "l>0" and "l>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < l &&& 1 < l
[PROOF STEP]
using \<open>l\<ge>2\<close>
[PROOF STATE]
proof (prove)
using this:
2 \<le> l

goal (1 subgoal):
 1. 0 < l &&& 1 < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < l
1 < l

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
interpret digits k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digits k
[PROOF STEP]
by (simp add: \<open>0 < k\<close> digits_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
define col1 where "col1 = (\<lambda> x. from_digits q (\<lambda>y. col (x + y)))"
[PROOF STATE]
proof (state)
this:
col1 = (\<lambda>x. from_digits q (\<lambda>xa. col (x + int xa)))

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have range_col1: "col1\<in>{a..a + int n_kq - 1} \<rightarrow> {..<k^q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col1 \<in> {a..a + int n_kq - 1} \<rightarrow> {..<k ^ q}
[PROOF STEP]
unfolding Pi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col1 \<in> {f. \<forall>x. x \<in> {a..a + int n_kq - 1} \<longrightarrow> f x \<in> {..<k ^ q}}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
assume "x\<in>{a..a + int n_kq - 1}"
[PROOF STATE]
proof (state)
this:
x \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {a..a + int n_kq - 1}
[PROOF STEP]
have col_xn:"col (x + int n)\<in>{..<k}" if "n<q" for n :: nat
[PROOF STATE]
proof (prove)
using this:
x \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. col (x + int n) \<in> {..<k}
[PROOF STEP]
using that 1 PiE N_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {a..a + int n_kq - 1}
n < q
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
\<lbrakk>?f \<in> Pi ?A ?B; ?f ?x \<in> ?B ?x \<Longrightarrow> ?Q; ?x \<notin> ?A \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> ?Q
N = q + 2 * n_kq

goal (1 subgoal):
 1. col (x + int n) \<in> {..<k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?n < q \<Longrightarrow> col (x + int ?n) \<in> {..<k}

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
have col_xn_upper_bound:"col (x + int n) \<le> k - 1"
          if "n<q" for n ::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (x + int n) \<le> k - 1
[PROOF STEP]
using that col_xn[of n] \<open>k>0\<close>
[PROOF STATE]
proof (prove)
using this:
n < q
n < q \<Longrightarrow> col (x + int n) \<in> {..<k}
0 < k

goal (1 subgoal):
 1. col (x + int n) \<le> k - 1
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
?n < q \<Longrightarrow> col (x + int ?n) \<le> k - 1

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
have "(\<Sum>n<q. col (x + int n) * k ^ n)\<le>
               (\<Sum>n<q. (k-1) *  k ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n<q. col (x + int n) * k ^ n) \<le> (\<Sum>n<q. (k - 1) * k ^ n)
[PROOF STEP]
using col_xn_upper_bound
[PROOF STATE]
proof (prove)
using this:
?n < q \<Longrightarrow> col (x + int ?n) \<le> k - 1

goal (1 subgoal):
 1. (\<Sum>n<q. col (x + int n) * k ^ n) \<le> (\<Sum>n<q. (k - 1) * k ^ n)
[PROOF STEP]
by (intro sum_mono mult_right_mono)
            auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n<q. col (x + int n) * k ^ n) \<le> (\<Sum>n<q. (k - 1) * k ^ n)

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n<q. col (x + int n) * k ^ n) \<le> (\<Sum>n<q. (k - 1) * k ^ n)

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
have "\<dots> = (k-1) * (\<Sum>n<q. k ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n<q. (k - 1) * k ^ n) = (k - 1) * sum ((^) k) {..<q}
[PROOF STEP]
by (rule sum_distrib_left[symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>n<q. (k - 1) * k ^ n) = (k - 1) * sum ((^) k) {..<q}

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n<q. (k - 1) * k ^ n) = (k - 1) * sum ((^) k) {..<q}

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
have "\<dots> < k^q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
using sum_mod_poly \<open>k>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < ?k \<Longrightarrow> (?k - 1) * sum ((^) ?k) {..<?q} < ?k ^ ?q
0 < k

goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(k - 1) * sum ((^) k) {..<q} < k ^ q

goal (1 subgoal):
 1. \<And>x. x \<in> {a..a + int n_kq - 1} \<Longrightarrow> col1 x < k ^ q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n<q. col (x + int n) * k ^ n) < k ^ q
[PROOF STEP]
show "col1 x <k^q"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n<q. col (x + int n) * k ^ n) < k ^ q

goal (1 subgoal):
 1. col1 x < k ^ q
[PROOF STEP]
unfolding col1_def from_digits_altdef
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n<q. col (x + int n) * k ^ n) < k ^ q

goal (1 subgoal):
 1. (\<Sum>i<q. col (x + int i) * k ^ i) < k ^ q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col1 x < k ^ q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
col1 \<in> {a..a + int n_kq - 1} \<rightarrow> {..<k ^ q}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
obtain j start step where prog:
        "j < k^q" "step > 0"
        "is_arith_prog_on l start step a (a + int n_kq - 1)"
        "arith_prog start step ` {..<l} \<subseteq>
          col1 -` {j} \<inter> {a..a + int n_kq -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k ^ q; 0 < step; is_arith_prog_on l start step a (a + int n_kq - 1); arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vdw range_col1
[PROOF STATE]
proof (prove)
using this:
vdw (k ^ q) l n_kq
col1 \<in> {a..a + int n_kq - 1} \<rightarrow> {..<k ^ q}

goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k ^ q; 0 < step; is_arith_prog_on l start step a (a + int n_kq - 1); arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim vdwE) (auto simp: \<open>k>0\<close>)
[PROOF STATE]
proof (state)
this:
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have range_prog_lessThan_l:
        "arith_prog start step i \<in> {a..a + int n_kq -1}"
        if "i < l" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + int n_kq - 1}
[PROOF STEP]
using that prog
[PROOF STATE]
proof (prove)
using this:
i < l
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + int n_kq - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have prog_in_ivl:
        "arith_prog start step i \<in> {a..a + 2 * int n_kq -1}"
        if "i \<le> l" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
proof (cases "i=l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
 2. i \<noteq> l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> l

goal (2 subgoals):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
 2. i \<noteq> l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> l
[PROOF STEP]
have "i<l"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> l

goal (1 subgoal):
 1. i < l
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<noteq> l
i \<le> l

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

goal (2 subgoals):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
 2. i \<noteq> l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < l

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
using prog
[PROOF STATE]
proof (prove)
using this:
i < l
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = l

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
have "start \<in> {a..a + int n_kq -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start \<in> {a..a + int n_kq - 1}
[PROOF STEP]
using range_prog_lessThan_l[of 0]
[PROOF STATE]
proof (prove)
using this:
0 < l \<Longrightarrow> arith_prog start step 0 \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. start \<in> {a..a + int n_kq - 1}
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
0 < l \<Longrightarrow> start + int (0 * step) \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. start \<in> {a..a + int n_kq - 1}
[PROOF STEP]
by (simp add: \<open>0 < l\<close>)
[PROOF STATE]
proof (state)
this:
start \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
start \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
have "start + step \<in> {a..a + int n_kq -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int step \<in> {a..a + int n_kq - 1}
[PROOF STEP]
using range_prog_lessThan_l[of 1]
[PROOF STATE]
proof (prove)
using this:
1 < l \<Longrightarrow> arith_prog start step 1 \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. start + int step \<in> {a..a + int n_kq - 1}
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
1 < l \<Longrightarrow> start + int (1 * step) \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. start + int step \<in> {a..a + int n_kq - 1}
[PROOF STEP]
by (metis \<open>1 < l\<close> mult.left_neutral)
[PROOF STATE]
proof (state)
this:
start + int step \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
start \<in> {a..a + int n_kq - 1}
start + int step \<in> {a..a + int n_kq - 1}
[PROOF STEP]
have "step \<le> n_kq"
[PROOF STATE]
proof (prove)
using this:
start \<in> {a..a + int n_kq - 1}
start + int step \<in> {a..a + int n_kq - 1}

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

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
have "arith_prog start step (l-1) \<in> {a..a + int n_kq -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}
[PROOF STEP]
using range_prog_lessThan_l[of "l-1"]
[PROOF STATE]
proof (prove)
using this:
l - 1 < l \<Longrightarrow> arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
l - 1 < l \<Longrightarrow> start + int ((l - 1) * step) \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. start + int ((l - 1) * step) \<in> {a..a + int n_kq - 1}
[PROOF STEP]
using \<open>0 < l\<close> diff_less less_numeral_extra(1)
[PROOF STATE]
proof (prove)
using this:
l - 1 < l \<Longrightarrow> start + int ((l - 1) * step) \<in> {a..a + int n_kq - 1}
0 < l
\<lbrakk>0 < ?n; 0 < ?m\<rbrakk> \<Longrightarrow> ?m - ?n < ?m
(0::?'a) < (1::?'a)

goal (1 subgoal):
 1. start + int ((l - 1) * step) \<in> {a..a + int n_kq - 1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
have "arith_prog start step l =
            arith_prog start step (l-1) + step"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step l = arith_prog start step (l - 1) + int step
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int (l * step) = start + int ((l - 1) * step) + int step
[PROOF STEP]
using \<open>0 < l\<close> mult_eq_if
[PROOF STATE]
proof (prove)
using this:
0 < l
?m * ?n = (if ?m = 0 then 0 else ?n + (?m - 1) * ?n)

goal (1 subgoal):
 1. start + int (l * step) = start + int ((l - 1) * step) + int step
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
arith_prog start step l = arith_prog start step (l - 1) + int step

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}
arith_prog start step l = arith_prog start step (l - 1) + int step
[PROOF STEP]
have "arith_prog start step l \<in>
            {a..a + 2 * int n_kq - 1}"
[PROOF STATE]
proof (prove)
using this:
arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}
arith_prog start step l = arith_prog start step (l - 1) + int step

goal (1 subgoal):
 1. arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
using \<open>step\<le>n_kq\<close>
[PROOF STATE]
proof (prove)
using this:
arith_prog start step (l - 1) \<in> {a..a + int n_kq - 1}
arith_prog start step l = arith_prog start step (l - 1) + int step
step \<le> n_kq

goal (1 subgoal):
 1. arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}

goal (1 subgoal):
 1. i = l \<Longrightarrow> arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
using range_prog_lessThan_l
[PROOF STATE]
proof (prove)
using this:
arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
?i < l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
?i < l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + int n_kq - 1}
i = l

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<le> l \<Longrightarrow> arith_prog start step ?i \<in> {a..a + 2 * int n_kq - 1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have col_prog_eq: "col1 (arith_prog start step k) = j"
        if "k < l" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col1 (arith_prog start step k) = j
[PROOF STEP]
using prog that
[PROOF STATE]
proof (prove)
using this:
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}
k < l

goal (1 subgoal):
 1. col1 (arith_prog start step k) = j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?k < l \<Longrightarrow> col1 (arith_prog start step ?k) = j

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have digit_col1:"digit (col1 x) y = col (x+int y)"
        if "x\<in>{a..<a + 2*int n_kq}" "y\<in>{..<q}"
        for x::int and y::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit (col1 x) y = col (x + int y)
[PROOF STEP]
unfolding col1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> {a..<a + 2 * int n_kq}
y \<in> {..<q}

goal (1 subgoal):
 1. digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {a..<a + 2 * int n_kq}; y \<in> {..<q}\<rbrakk> \<Longrightarrow> digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)
[PROOF STEP]
have "\<And>j'. j'<q \<Longrightarrow> x+j'\<in>{a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j'. j' < q \<Longrightarrow> x + int j' \<in> {a..b}
[PROOF STEP]
using "1"(1) N_def that(1)
[PROOF STATE]
proof (prove)
using this:
a + int N \<le> b + 1
N = q + 2 * n_kq
x \<in> {a..<a + 2 * int n_kq}

goal (1 subgoal):
 1. \<And>j'. j' < q \<Longrightarrow> x + int j' \<in> {a..b}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?j' < q \<Longrightarrow> x + int ?j' \<in> {a..b}

goal (1 subgoal):
 1. \<lbrakk>x \<in> {a..<a + 2 * int n_kq}; y \<in> {..<q}\<rbrakk> \<Longrightarrow> digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j' < q \<Longrightarrow> x + int ?j' \<in> {a..b}
[PROOF STEP]
have "\<And>j'. j'<q \<Longrightarrow> (\<lambda>y. col (x+int y)) j' < k"
[PROOF STATE]
proof (prove)
using this:
?j' < q \<Longrightarrow> x + int ?j' \<in> {a..b}

goal (1 subgoal):
 1. \<And>j'. j' < q \<Longrightarrow> col (x + int j') < k
[PROOF STEP]
using 1 that
[PROOF STATE]
proof (prove)
using this:
?j' < q \<Longrightarrow> x + int ?j' \<in> {a..b}
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
x \<in> {a..<a + 2 * int n_kq}
y \<in> {..<q}

goal (1 subgoal):
 1. \<And>j'. j' < q \<Longrightarrow> col (x + int j') < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?j' < q \<Longrightarrow> col (x + int ?j') < k

goal (1 subgoal):
 1. \<lbrakk>x \<in> {a..<a + 2 * int n_kq}; y \<in> {..<q}\<rbrakk> \<Longrightarrow> digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j' < q \<Longrightarrow> col (x + int ?j') < k
[PROOF STEP]
show "digit (from_digits q (\<lambda>xa. col (x + int xa))) y =
                    col (x + int y)"
[PROOF STATE]
proof (prove)
using this:
?j' < q \<Longrightarrow> col (x + int ?j') < k

goal (1 subgoal):
 1. digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)
[PROOF STEP]
using digit_from_digits that 1
[PROOF STATE]
proof (prove)
using this:
?j' < q \<Longrightarrow> col (x + int ?j') < k
\<lbrakk>\<And>j. j < ?n \<Longrightarrow> ?d j < k; 0 < ?n; ?i < ?n\<rbrakk> \<Longrightarrow> digit (from_digits ?n ?d) ?i = ?d ?i
x \<in> {a..<a + 2 * int n_kq}
y \<in> {..<q}
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
digit (from_digits q (\<lambda>xa. col (x + int xa))) y = col (x + int y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> {a..<a + 2 * int n_kq}; ?y \<in> {..<q}\<rbrakk> \<Longrightarrow> digit (col1 ?x) ?y = col (?x + int ?y)

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
text \<open> Impact on the colour when taking the block-step. \<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> {a..<a + 2 * int n_kq}; ?y \<in> {..<q}\<rbrakk> \<Longrightarrow> digit (col1 ?x) ?y = col (?x + int ?y)

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have one_step_more:
        "col (arith_prog start' step i) = digit j (nat (start'-start))"
        if "start'\<in>{start..<start+q}" "i\<in>{..<l}" for start' i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
have "start \<le> start'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start \<le> start'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
start' \<in> {start..<start + int q}
i \<in> {..<l}

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

goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
have shift_arith_prog:
          "arith_prog start step i + (start' - start) =
            arith_prog start' step i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step i + (start' - start) = arith_prog start' step i
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int (i * step) + (start' - start) = start' + int (i * step)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
arith_prog start step i + (start' - start) = arith_prog start' step i

goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
define diff where "diff = nat (start'-start)"
[PROOF STATE]
proof (state)
this:
diff = nat (start' - start)

goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
have "diff \<in>{..<q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff \<in> {..<q}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
start' \<in> {start..<start + int q}
i \<in> {..<l}

goal (1 subgoal):
 1. diff \<in> {..<q}
[PROOF STEP]
unfolding diff_def
[PROOF STATE]
proof (prove)
using this:
start' \<in> {start..<start + int q}
i \<in> {..<l}

goal (1 subgoal):
 1. nat (start' - start) \<in> {..<q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
diff \<in> {..<q}

goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
have "col (arith_prog start step i + int diff) = digit j diff"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
have "col1 (arith_prog start step i) = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col1 (arith_prog start step i) = j
[PROOF STEP]
using col1_def prog that
[PROOF STATE]
proof (prove)
using this:
col1 = (\<lambda>x. from_digits q (\<lambda>xa. col (x + int xa)))
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}
start' \<in> {start..<start + int q}
i \<in> {..<l}

goal (1 subgoal):
 1. col1 (arith_prog start step i) = j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
col1 (arith_prog start step i) = j

goal (1 subgoal):
 1. col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
col1 (arith_prog start step i) = j

goal (1 subgoal):
 1. col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
have " arith_prog start step i\<in>{a..a + 2 * int n_kq-1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
using prog(4) that
[PROOF STATE]
proof (prove)
using this:
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}
start' \<in> {start..<start + int q}
i \<in> {..<l}

goal (1 subgoal):
 1. arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}

goal (1 subgoal):
 1. col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
col1 (arith_prog start step i) = j
arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
col1 (arith_prog start step i) = j
arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}

goal (1 subgoal):
 1. col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
using digit_col1[where x = "arith_prog start step i"
                and y = "diff"]
              prog 1 \<open>diff \<in>{..<q}\<close>
[PROOF STATE]
proof (prove)
using this:
col1 (arith_prog start step i) = j
arith_prog start step i \<in> {a..a + 2 * int n_kq - 1}
\<lbrakk>arith_prog start step i \<in> {a..<a + 2 * int n_kq}; diff \<in> {..<q}\<rbrakk> \<Longrightarrow> digit (col1 (arith_prog start step i)) diff = col (arith_prog start step i + int diff)
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
diff \<in> {..<q}

goal (1 subgoal):
 1. col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (arith_prog start step i + int diff) = digit j diff

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
col (arith_prog start step i + int diff) = digit j diff

goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
col (arith_prog start step i + int diff) = digit j diff
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
col (arith_prog start step i + int diff) = digit j diff

goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
unfolding diff_def 1
[PROOF STATE]
proof (prove)
using this:
col (arith_prog start step i + int (nat (start' - start))) = digit j (nat (start' - start))

goal (1 subgoal):
 1. col (arith_prog start' step i) = digit j (nat (start' - start))
[PROOF STEP]
by (auto simp: \<open>start\<le>start'\<close> shift_arith_prog)
[PROOF STATE]
proof (state)
this:
col (arith_prog start' step i) = digit j (nat (start' - start))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?start' \<in> {start..<start + int q}; ?i \<in> {..<l}\<rbrakk> \<Longrightarrow> col (arith_prog ?start' step ?i) = digit j (nat (?start' - start))

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have one_step_more': "col (arith_prog start' step i) =
        col (arith_prog start' step 0)"
        if "start'\<in>{start..<start+q}" "i\<in>{..<l}" for start' i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (arith_prog start' step i) = col (arith_prog start' step 0)
[PROOF STEP]
using that one_step_more[of start' 0]
          one_step_more[of start' i]
[PROOF STATE]
proof (prove)
using this:
start' \<in> {start..<start + int q}
i \<in> {..<l}
\<lbrakk>start' \<in> {start..<start + int q}; 0 \<in> {..<l}\<rbrakk> \<Longrightarrow> col (arith_prog start' step 0) = digit j (nat (start' - start))
\<lbrakk>start' \<in> {start..<start + int q}; i \<in> {..<l}\<rbrakk> \<Longrightarrow> col (arith_prog start' step i) = digit j (nat (start' - start))

goal (1 subgoal):
 1. col (arith_prog start' step i) = col (arith_prog start' step 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?start' \<in> {start..<start + int q}; ?i \<in> {..<l}\<rbrakk> \<Longrightarrow> col (arith_prog ?start' step ?i) = col (arith_prog ?start' step 0)

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have start_q: "start + int q \<le> start + int q - 1 + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int q \<le> start + int q - 1 + 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
start + int q \<le> start + int q - 1 + 1

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have "{start..start + int q-1} \<subseteq> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {start..start + int q - 1} \<subseteq> {a..b}
[PROOF STEP]
using prog N_def 1(1)
[PROOF STATE]
proof (prove)
using this:
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}
N = q + 2 * n_kq
a + int N \<le> b + 1

goal (1 subgoal):
 1. {start..start + int q - 1} \<subseteq> {a..b}
[PROOF STEP]
by (force simp: arith_prog_def is_arith_prog_on_def)
[PROOF STATE]
proof (state)
this:
{start..start + int q - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{start..start + int q - 1} \<subseteq> {a..b}
[PROOF STEP]
have col': "col \<in> {start..start + int q-1} \<rightarrow> {..<k}"
[PROOF STATE]
proof (prove)
using this:
{start..start + int q - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. col \<in> {start..start + int q - 1} \<rightarrow> {..<k}
[PROOF STEP]
using 1 prog(4)
[PROOF STATE]
proof (prove)
using this:
{start..start + int q - 1} \<subseteq> {a..b}
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. col \<in> {start..start + int q - 1} \<rightarrow> {..<k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col \<in> {start..start + int q - 1} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
text \<open> Obtain an $(m-1)$-fold arithmetic progression in the starting $q$-bolck of the
             block arithmetic progression. \<close>
[PROOF STATE]
proof (state)
this:
col \<in> {start..start + int q - 1} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
obtain start_m steps_m where
        step_m_pos: "\<And>i. i < m - 1 \<Longrightarrow> 0 < steps_m i" and
        is_multi_arith_prog: "is_multi_arith_prog_on (l+1) (m - 1)
          start_m steps_m start (start + int q - 1)" and
        g_aux: "let g = multi_arith_prog (m - 1) start_m steps_m
          in  \<forall>c\<in>{0..<m - 1} \<rightarrow> {0..l}. \<forall>s<m - 1. (\<forall>j\<le>s. c j < l) \<longrightarrow>
          col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>steps_m start_m. \<lbrakk>\<And>i. i < m - 1 \<Longrightarrow> 0 < steps_m i; is_multi_arith_prog_on (l + 1) (m - 1) start_m steps_m start (start + int q - 1); let g = multi_arith_prog (m - 1) start_m steps_m in \<forall>c\<in>{0..<m - 1} \<rightarrow> {0..l}. \<forall>s<m - 1. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule vdw_lemmaE[OF vdw_lemma_IH start_q col']) blast
[PROOF STATE]
proof (state)
this:
?i < m - 1 \<Longrightarrow> 0 < steps_m ?i
is_multi_arith_prog_on (l + 1) (m - 1) start_m steps_m start (start + int q - 1)
let g = multi_arith_prog (m - 1) start_m steps_m in \<forall>c\<in>{0..<m - 1} \<rightarrow> {0..l}. \<forall>s<m - 1. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
define g where "g = multi_arith_prog (m-1) start_m steps_m"
[PROOF STATE]
proof (state)
this:
g = multi_arith_prog (m - 1) start_m steps_m

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have g: "col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))"
        if "c \<in> {0..<(m-1)} \<rightarrow> {0..l}" "s < m - 1" "\<forall>j \<le> s. c j < l"
        for c s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
using g_aux that
[PROOF STATE]
proof (prove)
using this:
let g = multi_arith_prog (m - 1) start_m steps_m in \<forall>c\<in>{0..<m - 1} \<rightarrow> {0..l}. \<forall>s<m - 1. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))
c \<in> {0..<m - 1} \<rightarrow> {0..l}
s < m - 1
\<forall>j\<le>s. c j < l

goal (1 subgoal):
 1. col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
unfolding g_def Let_def
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>{0..<m - 1} \<rightarrow> {0..l}. \<forall>s<m - 1. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (multi_arith_prog (m - 1) start_m steps_m c) = col (multi_arith_prog (m - 1) start_m steps_m (\<lambda>i. if i \<le> s then 0 else c i))
c \<in> {0..<m - 1} \<rightarrow> {0..l}
s < m - 1
\<forall>j\<le>s. c j < l

goal (1 subgoal):
 1. col (multi_arith_prog (m - 1) start_m steps_m c) = col (multi_arith_prog (m - 1) start_m steps_m (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> {0..<m - 1} \<rightarrow> {0..l}; ?s < m - 1; \<forall>j\<le>?s. ?c j < l\<rbrakk> \<Longrightarrow> col (g ?c) = col (g (\<lambda>i. if i \<le> ?s then 0 else ?c i))

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have range_g: "g c \<in> {start..start + int q - 1}"
        if "c \<in> {0..<m - 1} \<rightarrow> {0..<(l+1)}" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g c \<in> {start..start + int q - 1}
[PROOF STEP]
using is_multi_arith_prog_onD[OF is_multi_arith_prog that]
[PROOF STATE]
proof (prove)
using this:
multi_arith_prog (m - 1) start_m steps_m c \<in> {start..start + int q - 1}

goal (1 subgoal):
 1. g c \<in> {start..start + int q - 1}
[PROOF STEP]
by (auto simp: g_def)
[PROOF STATE]
proof (state)
this:
?c \<in> {0..<m - 1} \<rightarrow> {0..<l + 1} \<Longrightarrow> g ?c \<in> {start..start + int q - 1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
text \<open>Obtain an $m$-fold arithmetic progression by adding the block-step.\<close>
[PROOF STATE]
proof (state)
this:
?c \<in> {0..<m - 1} \<rightarrow> {0..<l + 1} \<Longrightarrow> g ?c \<in> {start..start + int q - 1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
define steps :: "nat \<Rightarrow> nat" where steps_def:
        "steps = (\<lambda>i.  (if i=0 then step else steps_m (i-1)))"
[PROOF STATE]
proof (state)
this:
steps = (\<lambda>i. if i = 0 then step else steps_m (i - 1))

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
define f where "f = multi_arith_prog m start_m steps"
[PROOF STATE]
proof (state)
this:
f = multi_arith_prog m start_m steps

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have f_step_g: "f c = int (c 0*step) + g (c \<circ> Suc)" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
have "f c = start_m + int (\<Sum>i<Suc (m-1). c i * steps i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f c = start_m + int (\<Sum>i<Suc (m - 1). c i * steps i)
[PROOF STEP]
using f_def
[PROOF STATE]
proof (prove)
using this:
f = multi_arith_prog m start_m steps

goal (1 subgoal):
 1. f c = start_m + int (\<Sum>i<Suc (m - 1). c i * steps i)
[PROOF STEP]
unfolding multi_arith_prog_def
[PROOF STATE]
proof (prove)
using this:
f = (\<lambda>c. start_m + int (\<Sum>i<m. c i * steps i))

goal (1 subgoal):
 1. f c = start_m + int (\<Sum>i<Suc (m - 1). c i * steps i)
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
f = (\<lambda>c. start_m + int (\<Sum>i<m. c i * steps i))
0 < m
0 < k

goal (1 subgoal):
 1. f c = start_m + int (\<Sum>i<Suc (m - 1). c i * steps i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f c = start_m + int (\<Sum>i<Suc (m - 1). c i * steps i)

goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f c = start_m + int (\<Sum>i<Suc (m - 1). c i * steps i)

goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
have "\<dots> = start_m + int (c 0 * steps 0) +
                       int (\<Sum>i<m-1. c (Suc i) * steps (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start_m + int (\<Sum>i<Suc (m - 1). c i * steps i) = start_m + int (c 0 * steps 0) + int (\<Sum>i<m - 1. c (Suc i) * steps (Suc i))
[PROOF STEP]
using sum.lessThan_Suc_shift[where n = "m-1"]
[PROOF STATE]
proof (prove)
using this:
sum ?g {..<Suc (m - 1)} = ?g 0 + (\<Sum>i<m - 1. ?g (Suc i))

goal (1 subgoal):
 1. start_m + int (\<Sum>i<Suc (m - 1). c i * steps i) = start_m + int (c 0 * steps 0) + int (\<Sum>i<m - 1. c (Suc i) * steps (Suc i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
start_m + int (\<Sum>i<Suc (m - 1). c i * steps i) = start_m + int (c 0 * steps 0) + int (\<Sum>i<m - 1. c (Suc i) * steps (Suc i))

goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
start_m + int (\<Sum>i<Suc (m - 1). c i * steps i) = start_m + int (c 0 * steps 0) + int (\<Sum>i<m - 1. c (Suc i) * steps (Suc i))

goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
have "\<dots> = start_m + int (c 0 * step) +
                       int (\<Sum>i<m-1. c (Suc i) * steps_m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start_m + int (c 0 * steps 0) + int (\<Sum>i<m - 1. c (Suc i) * steps (Suc i)) = start_m + int (c 0 * step) + int (\<Sum>i<m - 1. c (Suc i) * steps_m i)
[PROOF STEP]
using steps_def
[PROOF STATE]
proof (prove)
using this:
steps = (\<lambda>i. if i = 0 then step else steps_m (i - 1))

goal (1 subgoal):
 1. start_m + int (c 0 * steps 0) + int (\<Sum>i<m - 1. c (Suc i) * steps (Suc i)) = start_m + int (c 0 * step) + int (\<Sum>i<m - 1. c (Suc i) * steps_m i)
[PROOF STEP]
by (auto split:if_splits)
[PROOF STATE]
proof (state)
this:
start_m + int (c 0 * steps 0) + int (\<Sum>i<m - 1. c (Suc i) * steps (Suc i)) = start_m + int (c 0 * step) + int (\<Sum>i<m - 1. c (Suc i) * steps_m i)

goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f c = start_m + int (c 0 * step) + int (\<Sum>i<m - 1. c (Suc i) * steps_m i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f c = start_m + int (c 0 * step) + int (\<Sum>i<m - 1. c (Suc i) * steps_m i)

goal (1 subgoal):
 1. f c = int (c 0 * step) + g (c \<circ> Suc)
[PROOF STEP]
unfolding multi_arith_prog_def g_def
[PROOF STATE]
proof (prove)
using this:
f c = start_m + int (c 0 * step) + int (\<Sum>i<m - 1. c (Suc i) * steps_m i)

goal (1 subgoal):
 1. f c = int (c 0 * step) + (start_m + int (\<Sum>i<m - 1. (c \<circ> Suc) i * steps_m i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f c = int (c 0 * step) + g (c \<circ> Suc)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ?c = int (?c 0 * step) + g (?c \<circ> Suc)

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
text \<open> Show that this $m$-fold arithmetic progression fulfills all needed properties. \<close>
[PROOF STATE]
proof (state)
this:
f ?c = int (?c 0 * step) + g (?c \<circ> Suc)

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have steps_gr_0: "\<forall>i<m. 0 < steps i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<m. 0 < steps i
[PROOF STEP]
unfolding steps_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<m. 0 < (if i = 0 then step else steps_m (i - 1))
[PROOF STEP]
using step_m_pos prog
[PROOF STATE]
proof (prove)
using this:
?i < m - 1 \<Longrightarrow> 0 < steps_m ?i
j < k ^ q
0 < step
is_arith_prog_on l start step a (a + int n_kq - 1)
arith_prog start step ` {..<l} \<subseteq> col1 -` {j} \<inter> {a..a + int n_kq - 1}

goal (1 subgoal):
 1. \<forall>i<m. 0 < (if i = 0 then step else steps_m (i - 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<m. 0 < steps i

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have is_multi_on_f:
        "is_multi_arith_prog_on (l+1) m start_m steps a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
have "a \<le> start_m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> start_m
[PROOF STEP]
using is_multi_arith_prog
[PROOF STATE]
proof (prove)
using this:
is_multi_arith_prog_on (l + 1) (m - 1) start_m steps_m start (start + int q - 1)

goal (1 subgoal):
 1. a \<le> start_m
[PROOF STEP]
unfolding is_multi_arith_prog_on_def
[PROOF STATE]
proof (prove)
using this:
start \<le> start_m \<and> multi_arith_prog (m - 1) start_m steps_m (\<lambda>_. l + 1 - 1) \<le> start + int q - 1

goal (1 subgoal):
 1. a \<le> start_m
[PROOF STEP]
using is_arith_prog_on_def prog(3)
[PROOF STATE]
proof (prove)
using this:
start \<le> start_m \<and> multi_arith_prog (m - 1) start_m steps_m (\<lambda>_. l + 1 - 1) \<le> start + int q - 1
is_arith_prog_on ?l ?start ?step ?a ?b = (?a \<le> ?start \<and> arith_prog ?start ?step (?l - 1) \<le> ?b)
is_arith_prog_on l start step a (a + int n_kq - 1)

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

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<le> start_m

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a \<le> start_m

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
have "f (\<lambda>_. l) = arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<lambda>_. l) = arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l
[PROOF STEP]
using f_step_g
[PROOF STATE]
proof (prove)
using this:
f ?c = int (?c 0 * step) + g (?c \<circ> Suc)

goal (1 subgoal):
 1. f (\<lambda>_. l) = arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
f ?c = int (?c 0 * step) + g (?c \<circ> Suc)

goal (1 subgoal):
 1. f (\<lambda>_. l) = g ((\<lambda>_. l) \<circ> Suc) + int (l * step)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (\<lambda>_. l) = arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (\<lambda>_. l) = arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
have "g ((\<lambda>_. l) \<circ> Suc) \<le> start + q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ((\<lambda>_. l) \<circ> Suc) \<le> start + int q
[PROOF STEP]
using range_g[of "(\<lambda>_. l) \<circ> Suc"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>_. l) \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..<l + 1} \<Longrightarrow> g ((\<lambda>_. l) \<circ> Suc) \<in> {start..start + int q - 1}

goal (1 subgoal):
 1. g ((\<lambda>_. l) \<circ> Suc) \<le> start + int q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g ((\<lambda>_. l) \<circ> Suc) \<le> start + int q

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g ((\<lambda>_. l) \<circ> Suc) \<le> start + int q
[PROOF STEP]
have "arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l \<le>
            arith_prog start step l + q"
[PROOF STATE]
proof (prove)
using this:
g ((\<lambda>_. l) \<circ> Suc) \<le> start + int q

goal (1 subgoal):
 1. arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l \<le> arith_prog start step l + int q
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
g ((\<lambda>_. l) \<circ> Suc) \<le> start + int q

goal (1 subgoal):
 1. g ((\<lambda>_. l) \<circ> Suc) + int (l * step) \<le> start + int (l * step) + int q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l \<le> arith_prog start step l + int q

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
arith_prog (g ((\<lambda>_. l) \<circ> Suc)) step l \<le> arith_prog start step l + int q

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
have "\<dots>\<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step l + int q \<le> b
[PROOF STEP]
using prog_in_ivl[of l]
[PROOF STATE]
proof (prove)
using this:
l \<le> l \<Longrightarrow> arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}

goal (1 subgoal):
 1. arith_prog start step l + int q \<le> b
[PROOF STEP]
using is_multi_arith_prog
[PROOF STATE]
proof (prove)
using this:
l \<le> l \<Longrightarrow> arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
is_multi_arith_prog_on (l + 1) (m - 1) start_m steps_m start (start + int q - 1)

goal (1 subgoal):
 1. arith_prog start step l + int q \<le> b
[PROOF STEP]
unfolding is_multi_arith_prog_on_def
[PROOF STATE]
proof (prove)
using this:
l \<le> l \<Longrightarrow> arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
start \<le> start_m \<and> multi_arith_prog (m - 1) start_m steps_m (\<lambda>_. l + 1 - 1) \<le> start + int q - 1

goal (1 subgoal):
 1. arith_prog start step l + int q \<le> b
[PROOF STEP]
using "1"(1) N_def
[PROOF STATE]
proof (prove)
using this:
l \<le> l \<Longrightarrow> arith_prog start step l \<in> {a..a + 2 * int n_kq - 1}
start \<le> start_m \<and> multi_arith_prog (m - 1) start_m steps_m (\<lambda>_. l + 1 - 1) \<le> start + int q - 1
a + int N \<le> b + 1
N = q + 2 * n_kq

goal (1 subgoal):
 1. arith_prog start step l + int q \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog start step l + int q \<le> b

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (\<lambda>_. l) \<le> b
[PROOF STEP]
have "f (\<lambda>_. l) \<le> b"
[PROOF STATE]
proof (prove)
using this:
f (\<lambda>_. l) \<le> b

goal (1 subgoal):
 1. f (\<lambda>_. l) \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (\<lambda>_. l) \<le> b

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
f (\<lambda>_. l) \<le> b

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<le> start_m
f (\<lambda>_. l) \<le> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> start_m
f (\<lambda>_. l) \<le> b

goal (1 subgoal):
 1. is_multi_arith_prog_on (l + 1) m start_m steps a b
[PROOF STEP]
unfolding is_multi_arith_prog_on_def f_def
[PROOF STATE]
proof (prove)
using this:
a \<le> start_m
multi_arith_prog m start_m steps (\<lambda>_. l) \<le> b

goal (1 subgoal):
 1. a \<le> start_m \<and> multi_arith_prog m start_m steps (\<lambda>_. l + 1 - 1) \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_multi_arith_prog_on (l + 1) m start_m steps a b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_multi_arith_prog_on (l + 1) m start_m steps a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
text \<open> Show the relational property for all $s$. \<close>
[PROOF STATE]
proof (state)
this:
is_multi_arith_prog_on (l + 1) m start_m steps a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
have rel_prop_1:
        "col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))"
        if "c \<in> {0..<m} \<rightarrow> {0..l}" "s<m" "\<forall>j\<le>s. c j < l" for c s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
proof (cases "s = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s = 0

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "c 0 < l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c 0 < l
[PROOF STEP]
using that(3) True
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<le>s. c j < l
s = 0

goal (1 subgoal):
 1. c 0 < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c 0 < l

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have range_c_Suc: "c \<circ> Suc \<in> {0..<m-1} \<rightarrow> {0..l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
c \<in> {0..<m} \<rightarrow> {0..l}

goal (1 subgoal):
 1. c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "f c = arith_prog (g (c \<circ> Suc)) step (c 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f c = arith_prog (g (c \<circ> Suc)) step (c 0)
[PROOF STEP]
using f_step_g
[PROOF STATE]
proof (prove)
using this:
f ?c = int (?c 0 * step) + g (?c \<circ> Suc)

goal (1 subgoal):
 1. f c = arith_prog (g (c \<circ> Suc)) step (c 0)
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
f ?c = int (?c 0 * step) + g (?c \<circ> Suc)

goal (1 subgoal):
 1. f c = g (c \<circ> Suc) + int (c 0 * step)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f c = arith_prog (g (c \<circ> Suc)) step (c 0)

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f c = arith_prog (g (c \<circ> Suc)) step (c 0)
[PROOF STEP]
have "col (f c) = col (arith_prog (g (c \<circ> Suc)) step 0)"
[PROOF STATE]
proof (prove)
using this:
f c = arith_prog (g (c \<circ> Suc)) step (c 0)

goal (1 subgoal):
 1. col (f c) = col (arith_prog (g (c \<circ> Suc)) step 0)
[PROOF STEP]
using one_step_more'[of "g (c \<circ> Suc)" "c 0"] \<open>c 0 < l\<close>
            range_g[of "c \<circ> Suc"] range_c_Suc
            atLeastLessThanSuc_atLeastAtMost
[PROOF STATE]
proof (prove)
using this:
f c = arith_prog (g (c \<circ> Suc)) step (c 0)
\<lbrakk>g (c \<circ> Suc) \<in> {start..<start + int q}; c 0 \<in> {..<l}\<rbrakk> \<Longrightarrow> col (arith_prog (g (c \<circ> Suc)) step (c 0)) = col (arith_prog (g (c \<circ> Suc)) step 0)
c 0 < l
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..<l + 1} \<Longrightarrow> g (c \<circ> Suc) \<in> {start..start + int q - 1}
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
{?l..<Suc ?u} = {?l..?u}

goal (1 subgoal):
 1. col (f c) = col (arith_prog (g (c \<circ> Suc)) step 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (f c) = col (arith_prog (g (c \<circ> Suc)) step 0)

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
col (f c) = col (arith_prog (g (c \<circ> Suc)) step 0)

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
col (f c) = col (arith_prog (g (c \<circ> Suc)) step 0)

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "(\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) =
                   (\<Sum>x=1..<m. int(c x) * int (steps x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) = (\<Sum>x = 1..<m. int (c x) * int (steps x))
[PROOF STEP]
by(rule sum.reindex_bij_witness[of _ "(\<lambda>x. x-1)" "Suc"])
              (auto simp: steps_def split:if_splits)
[PROOF STATE]
proof (state)
this:
(\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) = (\<Sum>x = 1..<m. int (c x) * int (steps x))

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) = (\<Sum>x = 1..<m. int (c x) * int (steps x))

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "\<dots> = (\<Sum>x<m. int (if x = 0 then 0 else c x) *
            int (steps x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 1..<m. int (c x) * int (steps x)) = (\<Sum>x<m. int (if x = 0 then 0 else c x) * int (steps x))
[PROOF STEP]
by (rule sum.mono_neutral_cong_left) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 1..<m. int (c x) * int (steps x)) = (\<Sum>x<m. int (if x = 0 then 0 else c x) * int (steps x))

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) = (\<Sum>x<m. int (if x = 0 then 0 else c x) * int (steps x))
[PROOF STEP]
have "arith_prog (g (c \<circ> Suc)) step 0 =
            f (\<lambda>i. if i \<le> s then 0 else c i)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) = (\<Sum>x<m. int (if x = 0 then 0 else c x) * int (steps x))

goal (1 subgoal):
 1. arith_prog (g (c \<circ> Suc)) step 0 = f (\<lambda>i. if i \<le> s then 0 else c i)
[PROOF STEP]
unfolding f_def g_def multi_arith_prog_def arith_prog_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) = (\<Sum>x<m. int (if x = 0 then 0 else c x) * int (steps x))

goal (1 subgoal):
 1. start_m + int (\<Sum>i<m - 1. (c \<circ> Suc) i * steps_m i) + int (0 * step) = start_m + int (\<Sum>i<m. (if i \<le> s then 0 else c i) * steps i)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x<m - 1. int (c (Suc x)) * int (steps_m x)) = (\<Sum>x<m. int (if x = 0 then 0 else c x) * int (steps x))
s = 0

goal (1 subgoal):
 1. start_m + int (\<Sum>i<m - 1. (c \<circ> Suc) i * steps_m i) + int (0 * step) = start_m + int (\<Sum>i<m. (if i \<le> s then 0 else c i) * steps i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog (g (c \<circ> Suc)) step 0 = f (\<lambda>i. if i \<le> s then 0 else c i)

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
arith_prog (g (c \<circ> Suc)) step 0 = f (\<lambda>i. if i \<le> s then 0 else c i)

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
 2. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))

goal (1 subgoal):
 1. col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s \<noteq> 0

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
hence s_greater_0: "s > 0"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 0

goal (1 subgoal):
 1. 0 < s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < s

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have range_c_Suc: "c \<circ> Suc \<in> {0..<m-1} \<rightarrow> {0..l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
c \<in> {0..<m} \<rightarrow> {0..l}

goal (1 subgoal):
 1. c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "c 0 < l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c 0 < l
[PROOF STEP]
using \<open>s>0\<close> that
[PROOF STATE]
proof (prove)
using this:
0 < s
c \<in> {0..<m} \<rightarrow> {0..l}
s < m
\<forall>j\<le>s. c j < l

goal (1 subgoal):
 1. c 0 < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c 0 < l

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have g_IH:
          "col (g c') = col (g (\<lambda>i. if i \<le> s' then 0 else c' i))"
          if "c' \<in> {0..<m-1} \<rightarrow> {0..l}" "s'<m-1" "\<forall>j\<le>s'. c' j < l"
          for c' s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (g c') = col (g (\<lambda>i. if i \<le> s' then 0 else c' i))
[PROOF STEP]
using g_aux that
[PROOF STATE]
proof (prove)
using this:
let g = multi_arith_prog (m - 1) start_m steps_m in \<forall>c\<in>{0..<m - 1} \<rightarrow> {0..l}. \<forall>s<m - 1. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))
c' \<in> {0..<m - 1} \<rightarrow> {0..l}
s' < m - 1
\<forall>j\<le>s'. c' j < l

goal (1 subgoal):
 1. col (g c') = col (g (\<lambda>i. if i \<le> s' then 0 else c' i))
[PROOF STEP]
unfolding multi_arith_prog_def g_def
[PROOF STATE]
proof (prove)
using this:
let g = \<lambda>c. start_m + int (\<Sum>i<m - 1. c i * steps_m i) in \<forall>c\<in>{0..<m - 1} \<rightarrow> {0..l}. \<forall>s<m - 1. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (g c) = col (g (\<lambda>i. if i \<le> s then 0 else c i))
c' \<in> {0..<m - 1} \<rightarrow> {0..l}
s' < m - 1
\<forall>j\<le>s'. c' j < l

goal (1 subgoal):
 1. col (start_m + int (\<Sum>i<m - 1. c' i * steps_m i)) = col (start_m + int (\<Sum>i<m - 1. (if i \<le> s' then 0 else c' i) * steps_m i))
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c' \<in> {0..<m - 1} \<rightarrow> {0..l}; ?s' < m - 1; \<forall>j\<le>?s'. ?c' j < l\<rbrakk> \<Longrightarrow> col (g ?c') = col (g (\<lambda>i. if i \<le> ?s' then 0 else ?c' i))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have g_shift_IH: "col (g (c \<circ> Suc)) =
          col (g ((\<lambda>i. if i\<in>{1..t} then 0 else c i) \<circ> Suc))"
          if "c \<in> {1..<m} \<rightarrow> {0..l}" "t\<in>{1..<m}" "\<forall>j\<in>{1..t}. c j < l"
          for c t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
have "(\<lambda>i. (if i \<le> t - 1 then 0 else (c \<circ> Suc) i)) =
                (\<lambda>i. (if i \<in> {1..t} then 0 else c i)) \<circ> Suc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = (\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {1..<m} \<rightarrow> {0..l}
t \<in> {1..<m}
\<forall>j\<in>{1..t}. c j < l

goal (1 subgoal):
 1. (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = (\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc
[PROOF STEP]
by (auto split: if_splits simp:fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = (\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = (\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc
[PROOF STEP]
have right:
            "g (\<lambda>i. if i \<le> (t-1) then 0 else (c \<circ> Suc) i) =
             g ((\<lambda>i. if i\<in>{1..t} then 0 else c i) \<circ> Suc)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = (\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc

goal (1 subgoal):
 1. g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc)

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
have "(c \<circ> Suc)\<in> {0..<m-1} \<rightarrow> {0..l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
c \<in> {1..<m} \<rightarrow> {0..l}

goal (1 subgoal):
 1. c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
have "t-1<m-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t - 1 < m - 1
[PROOF STEP]
using that(2)
[PROOF STATE]
proof (prove)
using this:
t \<in> {1..<m}

goal (1 subgoal):
 1. t - 1 < m - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t - 1 < m - 1

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t - 1 < m - 1

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
have"\<forall>j\<le>t-1. (c \<circ> Suc) j < l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<le>t - 1. (c \<circ> Suc) j < l
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {1..<m} \<rightarrow> {0..l}
t \<in> {1..<m}
\<forall>j\<in>{1..t}. c j < l

goal (1 subgoal):
 1. \<forall>j\<le>t - 1. (c \<circ> Suc) j < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j\<le>t - 1. (c \<circ> Suc) j < l

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
t - 1 < m - 1
\<forall>j\<le>t - 1. (c \<circ> Suc) j < l
[PROOF STEP]
have "col (g (c \<circ> Suc)) =
            col (g (\<lambda>i. (if i \<le> t-1 then 0 else (c \<circ> Suc) i)))"
[PROOF STATE]
proof (prove)
using this:
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
t - 1 < m - 1
\<forall>j\<le>t - 1. (c \<circ> Suc) j < l

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i))
[PROOF STEP]
using g_IH[of "(c \<circ> Suc)" "t-1"]
[PROOF STATE]
proof (prove)
using this:
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
t - 1 < m - 1
\<forall>j\<le>t - 1. (c \<circ> Suc) j < l
\<lbrakk>c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}; t - 1 < m - 1; \<forall>j\<le>t - 1. (c \<circ> Suc) j < l\<rbrakk> \<Longrightarrow> col (g (c \<circ> Suc)) = col (g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i))

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (g (c \<circ> Suc)) = col (g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i))

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
with right
[PROOF STATE]
proof (chain)
picking this:
g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc)
col (g (c \<circ> Suc)) = col (g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i) = g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc)
col (g (c \<circ> Suc)) = col (g (\<lambda>i. if i \<le> t - 1 then 0 else (c \<circ> Suc) i))

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..t} then 0 else c i) \<circ> Suc))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> {1..<m} \<rightarrow> {0..l}; ?t \<in> {1..<m}; \<forall>j\<in>{1..?t}. ?c j < l\<rbrakk> \<Longrightarrow> col (g (?c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..?t} then 0 else ?c i) \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "col (f c) = col (int (c 0 * step) + g (c \<circ> Suc))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (f c) = col (int (c 0 * step) + g (c \<circ> Suc))
[PROOF STEP]
using f_step_g
[PROOF STATE]
proof (prove)
using this:
f ?c = int (?c 0 * step) + g (?c \<circ> Suc)

goal (1 subgoal):
 1. col (f c) = col (int (c 0 * step) + g (c \<circ> Suc))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
col (f c) = col (int (c 0 * step) + g (c \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
col (f c) = col (int (c 0 * step) + g (c \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "int (c 0 * step) + g (c \<circ> Suc) =
          arith_prog (g (c \<circ> Suc)) step (c 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (c 0 * step) + g (c \<circ> Suc) = arith_prog (g (c \<circ> Suc)) step (c 0)
[PROOF STEP]
by (simp add: arith_prog_def)
[PROOF STATE]
proof (state)
this:
int (c 0 * step) + g (c \<circ> Suc) = arith_prog (g (c \<circ> Suc)) step (c 0)

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (c 0 * step) + g (c \<circ> Suc) = arith_prog (g (c \<circ> Suc)) step (c 0)

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "col \<dots> = col (arith_prog (g (c \<circ> Suc)) step 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (arith_prog (g (c \<circ> Suc)) step (c 0)) = col (arith_prog (g (c \<circ> Suc)) step 0)
[PROOF STEP]
using one_step_more'[of "g (c \<circ> Suc)" "c 0"] \<open>c 0 < l\<close>
            range_g[of "c \<circ> Suc"] range_c_Suc
            atLeastLessThanSuc_atLeastAtMost
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g (c \<circ> Suc) \<in> {start..<start + int q}; c 0 \<in> {..<l}\<rbrakk> \<Longrightarrow> col (arith_prog (g (c \<circ> Suc)) step (c 0)) = col (arith_prog (g (c \<circ> Suc)) step 0)
c 0 < l
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..<l + 1} \<Longrightarrow> g (c \<circ> Suc) \<in> {start..start + int q - 1}
c \<circ> Suc \<in> {0..<m - 1} \<rightarrow> {0..l}
{?l..<Suc ?u} = {?l..?u}

goal (1 subgoal):
 1. col (arith_prog (g (c \<circ> Suc)) step (c 0)) = col (arith_prog (g (c \<circ> Suc)) step 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (arith_prog (g (c \<circ> Suc)) step (c 0)) = col (arith_prog (g (c \<circ> Suc)) step 0)

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
col (arith_prog (g (c \<circ> Suc)) step (c 0)) = col (arith_prog (g (c \<circ> Suc)) step 0)

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "\<dots> = col (g (c \<circ> Suc))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (arith_prog (g (c \<circ> Suc)) step 0) = col (g (c \<circ> Suc))
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (g (c \<circ> Suc) + int (0 * step)) = col (g (c \<circ> Suc))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (arith_prog (g (c \<circ> Suc)) step 0) = col (g (c \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
col (arith_prog (g (c \<circ> Suc)) step 0) = col (g (c \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "\<dots> = col (g ((\<lambda>i. if  i\<in>{1..s} then 0 else c i) \<circ>
          Suc))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc))
[PROOF STEP]
using g_shift_IH[of "c" s] \<open>s>0\<close> that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c \<in> {1..<m} \<rightarrow> {0..l}; s \<in> {1..<m}; \<forall>j\<in>{1..s}. c j < l\<rbrakk> \<Longrightarrow> col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc))
0 < s
c \<in> {0..<m} \<rightarrow> {0..l}
s < m
\<forall>j\<le>s. c j < l

goal (1 subgoal):
 1. col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
col (g (c \<circ> Suc)) = col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "\<dots> = col ((\<lambda>c. int (c 0 * step) +
          g (c \<circ> Suc))(\<lambda>i. if i\<le>s then 0 else c i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc)) = col (int ((if 0 \<le> s then 0 else c 0) * step) + g ((\<lambda>i. if i \<le> s then 0 else c i) \<circ> Suc))
[PROOF STEP]
by (auto simp: g_def multi_arith_prog_def)
[PROOF STATE]
proof (state)
this:
col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc)) = col (int ((if 0 \<le> s then 0 else c 0) * step) + g ((\<lambda>i. if i \<le> s then 0 else c i) \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
col (g ((\<lambda>i. if i \<in> {1..s} then 0 else c i) \<circ> Suc)) = col (int ((if 0 \<le> s then 0 else c 0) * step) + g ((\<lambda>i. if i \<le> s then 0 else c i) \<circ> Suc))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
have "\<dots> = col (f (\<lambda>i. if i \<le> s then 0 else c i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (int ((if 0 \<le> s then 0 else c 0) * step) + g ((\<lambda>i. if i \<le> s then 0 else c i) \<circ> Suc)) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
unfolding f_step_g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (int ((if 0 \<le> s then 0 else c 0) * step) + g ((\<lambda>i. if i \<le> s then 0 else c i) \<circ> Suc)) = col (int ((if 0 \<le> s then 0 else c 0) * step) + g ((\<lambda>i. if i \<le> s then 0 else c i) \<circ> Suc))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (int ((if 0 \<le> s then 0 else c 0) * step) + g ((\<lambda>i. if i \<le> s then 0 else c i) \<circ> Suc)) = col (f (\<lambda>i. if i \<le> s then 0 else c i))

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))

goal (1 subgoal):
 1. col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> {0..<m} \<rightarrow> {0..l}; ?s < m; \<forall>j\<le>?s. ?c j < l\<rbrakk> \<Longrightarrow> col (f ?c) = col (f (\<lambda>i. if i \<le> ?s then 0 else ?c i))

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))
[PROOF STEP]
by (rule exI[of _ start_m], rule exI[of _ steps])
           (use steps_gr_0 is_multi_on_f rel_prop_1 in
             \<open>auto simp: f_def Let_def steps_def\<close>)
[PROOF STATE]
proof (state)
this:
\<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vdw_lemma k m l N

goal (1 subgoal):
 1. 1 < m \<Longrightarrow> \<exists>a. vdw_lemma k m l a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vdw_lemma k m l N
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vdw_lemma k m l N

goal (1 subgoal):
 1. \<exists>a. vdw_lemma k m l a
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>a. vdw_lemma k m l a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. vdw_lemma k m l a

goal:
No subgoals!
[PROOF STEP]
qed