[STATEMENT]
lemma vdw_lemma_imp_vdw:
  assumes "vdw_lemma k k l N"
  shows   "vdw k (Suc l) N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdw k (Suc l) N
[PROOF STEP]
unfolding vdw_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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b})
[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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
text \<open>Idea: Proof uses pigeonhole principle to guarantee the existence of an arithmetic
            progression of length $l+1$ with the same colour. \<close>
[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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
obtain start steps where prog:
    "\<And>i. i < k \<Longrightarrow> steps i > 0"
    "is_multi_arith_prog_on (l+1) k start steps a b"
    "let f = multi_arith_prog k start steps
     in  \<forall>c \<in> {0..<k} \<rightarrow> {0..l}. \<forall>s<k. (\<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 STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>steps start. \<lbrakk>\<And>i. i < k \<Longrightarrow> 0 < steps i; is_multi_arith_prog_on (l + 1) k start steps a b; let f = multi_arith_prog k start steps in \<forall>c\<in>{0..<k} \<rightarrow> {0..l}. \<forall>s<k. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms 1
[PROOF STATE]
proof (prove)
using this:
vdw_lemma k k l N
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. (\<And>steps start. \<lbrakk>\<And>i. i < k \<Longrightarrow> 0 < steps i; is_multi_arith_prog_on (l + 1) k start steps a b; let f = multi_arith_prog k start steps in \<forall>c\<in>{0..<k} \<rightarrow> {0..l}. \<forall>s<k. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim vdw_lemmaE[where a=a and b=b and col=col and m=k
          and k=k and l=l and n=N]) auto
[PROOF STATE]
proof (state)
this:
?i < k \<Longrightarrow> 0 < steps ?i
is_multi_arith_prog_on (l + 1) k start steps a b
let f = multi_arith_prog k start steps in \<forall>c\<in>{0..<k} \<rightarrow> {0..l}. \<forall>s<k. (\<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 (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
text \<open> Obtain a $k$-fold arithmetic progression $f$ of length $l$ from assumptions. \<close>
[PROOF STATE]
proof (state)
this:
?i < k \<Longrightarrow> 0 < steps ?i
is_multi_arith_prog_on (l + 1) k start steps a b
let f = multi_arith_prog k start steps in \<forall>c\<in>{0..<k} \<rightarrow> {0..l}. \<forall>s<k. (\<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 (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define f where "f = multi_arith_prog k start steps"
[PROOF STATE]
proof (state)
this:
f = multi_arith_prog k 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have rel_propE: "col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))"
    if "c \<in> {0..<k} \<rightarrow> {0..l}" "s<k" "\<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]
using prog(3) that
[PROOF STATE]
proof (prove)
using this:
let f = multi_arith_prog k start steps in \<forall>c\<in>{0..<k} \<rightarrow> {0..l}. \<forall>s<k. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
c \<in> {0..<k} \<rightarrow> {0..l}
s < k
\<forall>j\<le>s. c j < l

goal (1 subgoal):
 1. col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
unfolding f_def Let_def
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>{0..<k} \<rightarrow> {0..l}. \<forall>s<k. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (multi_arith_prog k start steps c) = col (multi_arith_prog k start steps (\<lambda>i. if i \<le> s then 0 else c i))
c \<in> {0..<k} \<rightarrow> {0..l}
s < k
\<forall>j\<le>s. c j < l

goal (1 subgoal):
 1. col (multi_arith_prog k start steps c) = col (multi_arith_prog k start steps (\<lambda>i. if i \<le> s then 0 else c i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> {0..<k} \<rightarrow> {0..l}; ?s < k; \<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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
text \<open>There are $k+1$ values $a_r = f(0,\dots,0,l,\dots,l)$ with $0\leq r\leq k$ zeros.\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> {0..<k} \<rightarrow> {0..l}; ?s < k; \<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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define a_r where "a_r = (\<lambda>r. f (\<lambda>i. (if i<r then 0 else l)))"
[PROOF STATE]
proof (state)
this:
a_r = (\<lambda>r. f (\<lambda>i. if i < r then 0 else 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have range_col_a_r: "col (a_r x) < k" if "x < k+1" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (a_r x) < k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. col (a_r x) < k
[PROOF STEP]
have "a_r x \<in> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_r x \<in> {a..b}
[PROOF STEP]
unfolding a_r_def f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multi_arith_prog k start steps (\<lambda>i. if i < x then 0 else l) \<in> {a..b}
[PROOF STEP]
by (intro is_multi_arith_prog_onD[OF prog(2)]) auto
[PROOF STATE]
proof (state)
this:
a_r x \<in> {a..b}

goal (1 subgoal):
 1. col (a_r x) < k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a_r x \<in> {a..b}

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

goal (1 subgoal):
 1. col (a_r x) < k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
col (a_r x) < k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x < k + 1 \<Longrightarrow> col (a_r ?x) < 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x < k + 1 \<Longrightarrow> col (a_r ?x) < k
[PROOF STEP]
have "(col \<circ> a_r) ` {..<k + 1} \<subseteq> {..<k}"
[PROOF STATE]
proof (prove)
using this:
?x < k + 1 \<Longrightarrow> col (a_r ?x) < k

goal (1 subgoal):
 1. (col \<circ> a_r) ` {..<k + 1} \<subseteq> {..<k}
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
?x < k + 1 \<Longrightarrow> col (a_r ?x) < k
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. (col \<circ> a_r) ` {..<k + 1} \<subseteq> {..<k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(col \<circ> a_r) ` {..<k + 1} \<subseteq> {..<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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(col \<circ> a_r) ` {..<k + 1} \<subseteq> {..<k}
[PROOF STEP]
have "card ((col \<circ> a_r) ` {..<k + 1}) \<le> card {..<k}"
[PROOF STATE]
proof (prove)
using this:
(col \<circ> a_r) ` {..<k + 1} \<subseteq> {..<k}

goal (1 subgoal):
 1. card ((col \<circ> a_r) ` {..<k + 1}) \<le> card {..<k}
[PROOF STEP]
by (intro card_mono) auto
[PROOF STATE]
proof (state)
this:
card ((col \<circ> a_r) ` {..<k + 1}) \<le> card {..<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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card ((col \<circ> a_r) ` {..<k + 1}) \<le> card {..<k}
[PROOF STEP]
have "\<not> inj_on (col \<circ> a_r) {..<k+1}"
[PROOF STATE]
proof (prove)
using this:
card ((col \<circ> a_r) ` {..<k + 1}) \<le> card {..<k}

goal (1 subgoal):
 1. \<not> inj_on (col \<circ> a_r) {..<k + 1}
[PROOF STEP]
using pigeonhole[of "col \<circ> a_r" "{..<k+1}"]
[PROOF STATE]
proof (prove)
using this:
card ((col \<circ> a_r) ` {..<k + 1}) \<le> card {..<k}
card ((col \<circ> a_r) ` {..<k + 1}) < card {..<k + 1} \<Longrightarrow> \<not> inj_on (col \<circ> a_r) {..<k + 1}

goal (1 subgoal):
 1. \<not> inj_on (col \<circ> a_r) {..<k + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> inj_on (col \<circ> a_r) {..<k + 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
text \<open>Using the pigeonhole principle get $r_1$ and $r_2$ where $a_{r_1}$ and $a_{r_2}$ have the
    same colour.\<close>
[PROOF STATE]
proof (state)
this:
\<not> inj_on (col \<circ> a_r) {..<k + 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on (col \<circ> a_r) {..<k + 1}
[PROOF STEP]
obtain r1 r2 where pigeon_cols:
      "r1\<in>{..<k+1}"
      "r2\<in>{..<k+1}"
      "r1 < r2"
      "(col \<circ> a_r) r1 = (col \<circ> a_r) r2"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on (col \<circ> a_r) {..<k + 1}

goal (1 subgoal):
 1. (\<And>r1 r2. \<lbrakk>r1 \<in> {..<k + 1}; r2 \<in> {..<k + 1}; r1 < r2; (col \<circ> a_r) r1 = (col \<circ> a_r) r2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, lifting) linear linorder_inj_onI)
[PROOF STATE]
proof (state)
this:
r1 \<in> {..<k + 1}
r2 \<in> {..<k + 1}
r1 < r2
(col \<circ> a_r) r1 = (col \<circ> a_r) r2

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
text \<open> Show that the following function $h$ is an arithmetic progression which fulfills all
         properties for Van der Waerden's Theorem. \<close>
[PROOF STATE]
proof (state)
this:
r1 \<in> {..<k + 1}
r2 \<in> {..<k + 1}
r1 < r2
(col \<circ> a_r) r1 = (col \<circ> a_r) r2

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define h where
    "h = (\<lambda>x. f (\<lambda>i. (if i<r1 then 0 else (if i<r2 then x else l))))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>x. f (\<lambda>i. if i < r1 then 0 else if i < r2 then x else 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "h 0 = a_r r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h 0 = a_r r2
[PROOF STEP]
unfolding h_def a_r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<lambda>i. if i < r1 then 0 else if i < r2 then 0 else l) = f (\<lambda>i. if i < r2 then 0 else l)
[PROOF STEP]
using \<open>r1<r2\<close>
[PROOF STATE]
proof (prove)
using this:
r1 < r2

goal (1 subgoal):
 1. f (\<lambda>i. if i < r1 then 0 else if i < r2 then 0 else l) = f (\<lambda>i. if i < r2 then 0 else l)
[PROOF STEP]
by (intro arg_cong[where f = f]) auto
[PROOF STATE]
proof (state)
this:
h 0 = a_r r2

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
h 0 = a_r r2

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "h l = a_r r1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h l = a_r r1
[PROOF STEP]
unfolding h_def a_r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<lambda>i. if i < r1 then 0 else if i < r2 then l else l) = f (\<lambda>i. if i < r1 then 0 else l)
[PROOF STEP]
using \<open>r1<r2\<close>
[PROOF STATE]
proof (prove)
using this:
r1 < r2

goal (1 subgoal):
 1. f (\<lambda>i. if i < r1 then 0 else if i < r2 then l else l) = f (\<lambda>i. if i < r1 then 0 else l)
[PROOF STEP]
by (metis le_eq_less_or_eq less_le_trans)
[PROOF STATE]
proof (state)
this:
h l = a_r r1

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
h 0 = a_r r2
h l = a_r r1
[PROOF STEP]
have "col (h 0) = col (h l)"
[PROOF STATE]
proof (prove)
using this:
h 0 = a_r r2
h l = a_r r1

goal (1 subgoal):
 1. col (h 0) = col (h l)
[PROOF STEP]
using pigeon_cols(4)
[PROOF STATE]
proof (prove)
using this:
h 0 = a_r r2
h l = a_r r1
(col \<circ> a_r) r1 = (col \<circ> a_r) r2

goal (1 subgoal):
 1. col (h 0) = col (h l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (h 0) = col (h 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have h_col: "col (h 0) = col (h i)" if "i\<in>{..<l+1}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (h 0) = col (h i)
[PROOF STEP]
proof (cases "i=l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = l \<Longrightarrow> col (h 0) = col (h i)
 2. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = l

goal (2 subgoals):
 1. i = l \<Longrightarrow> col (h 0) = col (h i)
 2. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[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. col (h 0) = col (h i)
[PROOF STEP]
using \<open>col (h 0) = col (h l)\<close>
[PROOF STATE]
proof (prove)
using this:
i = l
col (h 0) = col (h l)

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

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> l

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[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 \<in> {..<l + 1}

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

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
let ?c = "(\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
have "?c\<in>{0..<k} \<rightarrow> {0..l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<in> {..<l + 1}

goal (1 subgoal):
 1. (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
have "(\<forall>j\<le>r2-1. ?c j < l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<le>r2 - 1. (if j < r1 then 0 else if j < r2 then i else l) < l
[PROOF STEP]
using \<open>i<l\<close> pigeon_cols(3)
[PROOF STATE]
proof (prove)
using this:
i < l
r1 < r2

goal (1 subgoal):
 1. \<forall>j\<le>r2 - 1. (if j < r1 then 0 else if j < r2 then i else l) < l
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>j\<le>r2 - 1. (if j < r1 then 0 else if j < r2 then i else l) < l

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}
\<forall>j\<le>r2 - 1. (if j < r1 then 0 else if j < r2 then i else l) < l
[PROOF STEP]
have "col (f ?c) =
      col (f (\<lambda>i. if i \<le> r2-1 then 0 else ?c i))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}
\<forall>j\<le>r2 - 1. (if j < r1 then 0 else if j < r2 then i else l) < l

goal (1 subgoal):
 1. col (f (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)) = col (f (\<lambda>ia. if ia \<le> r2 - 1 then 0 else if ia < r1 then 0 else if ia < r2 then i else l))
[PROOF STEP]
using rel_propE[of ?c "r2-1"] pigeon_cols
[PROOF STATE]
proof (prove)
using this:
(\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}
\<forall>j\<le>r2 - 1. (if j < r1 then 0 else if j < r2 then i else l) < l
\<lbrakk>(\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l) \<in> {0..<k} \<rightarrow> {0..l}; r2 - 1 < k; \<forall>j\<le>r2 - 1. (if j < r1 then 0 else if j < r2 then i else l) < l\<rbrakk> \<Longrightarrow> col (f (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)) = col (f (\<lambda>ia. if ia \<le> r2 - 1 then 0 else if ia < r1 then 0 else if ia < r2 then i else l))
r1 \<in> {..<k + 1}
r2 \<in> {..<k + 1}
r1 < r2
(col \<circ> a_r) r1 = (col \<circ> a_r) r2

goal (1 subgoal):
 1. col (f (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)) = col (f (\<lambda>ia. if ia \<le> r2 - 1 then 0 else if ia < r1 then 0 else if ia < r2 then i else l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
col (f (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)) = col (f (\<lambda>ia. if ia \<le> r2 - 1 then 0 else if ia < r1 then 0 else if ia < r2 then i else l))

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> col (h 0) = col (h i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
col (f (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)) = col (f (\<lambda>ia. if ia \<le> r2 - 1 then 0 else if ia < r1 then 0 else if ia < r2 then i else l))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
col (f (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)) = col (f (\<lambda>ia. if ia \<le> r2 - 1 then 0 else if ia < r1 then 0 else if ia < r2 then i else l))

goal (1 subgoal):
 1. col (h 0) = col (h i)
[PROOF STEP]
unfolding h_def f_def
[PROOF STATE]
proof (prove)
using this:
col (multi_arith_prog k start steps (\<lambda>idx. if idx < r1 then 0 else if idx < r2 then i else l)) = col (multi_arith_prog k start steps (\<lambda>ia. if ia \<le> r2 - 1 then 0 else if ia < r1 then 0 else if ia < r2 then i else l))

goal (1 subgoal):
 1. col (multi_arith_prog k start steps (\<lambda>i. if i < r1 then 0 else if i < r2 then 0 else l)) = col (multi_arith_prog k start steps (\<lambda>ia. if ia < r1 then 0 else if ia < r2 then i else l))
[PROOF STEP]
by (smt (z3) Nat.lessE One_nat_def add_diff_cancel_left'
          le_less less_Suc_eq_le multi_arith_prog_mono plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
col (h 0) = col (h i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {..<l + 1} \<Longrightarrow> col (h 0) = col (h ?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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define h_start where "h_start = start + l*(\<Sum>i\<in>{r2..<k}. steps i)"
[PROOF STATE]
proof (state)
this:
h_start = start + int (l * sum steps {r2..<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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define h_step where "h_step = (\<Sum>i\<in>{r1..<r2}. steps i)"
[PROOF STATE]
proof (state)
this:
h_step = sum steps {r1..<r2}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int N \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have h_arith_prog: "h = arith_prog h_start h_step"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = arith_prog h_start h_step
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h = arith_prog h_start h_step
[PROOF STEP]
have "(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l)
        * int (steps x)) =
      int l * (\<Sum>x = r2..<k. int (steps x)) +
        int y * (\<Sum>x = r1..<r2. int (steps x))"
      for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
proof (cases "r2 = k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r2 = k

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r2 = k
[PROOF STEP]
have "r1<k"
[PROOF STATE]
proof (prove)
using this:
r2 = k

goal (1 subgoal):
 1. r1 < k
[PROOF STEP]
using pigeon_cols
[PROOF STATE]
proof (prove)
using this:
r2 = k
r1 \<in> {..<k + 1}
r2 \<in> {..<k + 1}
r1 < r2
(col \<circ> a_r) r1 = (col \<circ> a_r) r2

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

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
r2 = k
r1 < k
[PROOF STEP]
have
        "(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l)
           * int (steps x)) =
         (\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x))"
[PROOF STATE]
proof (prove)
using this:
r2 = k
r1 < k

goal (1 subgoal):
 1. (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = (\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x))
[PROOF STEP]
by (intro sum.cong) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = (\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x))

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = (\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x))

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "\<dots> = (\<Sum>x<r1. int (if x < r1 then 0 else y) *
          int (steps x)) + (\<Sum>x=r1..<k. int (if x < r1 then 0 else y)
          * int (steps x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x)) = (\<Sum>x<r1. int (if x < r1 then 0 else y) * int (steps x)) + (\<Sum>x = r1..<k. int (if x < r1 then 0 else y) * int (steps x))
[PROOF STEP]
using split_sum_mid_less[of r1 k
            "(\<lambda>x. int (if x < r1 then 0 else y) * int (steps x))"]
            \<open>r1<k\<close>
[PROOF STATE]
proof (prove)
using this:
r1 < k \<Longrightarrow> (\<Sum>j<k. int (if j < r1 then 0 else y) * int (steps j)) = (\<Sum>j<r1. int (if j < r1 then 0 else y) * int (steps j)) + (\<Sum>j = r1..<k. int (if j < r1 then 0 else y) * int (steps j))
r1 < k

goal (1 subgoal):
 1. (\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x)) = (\<Sum>x<r1. int (if x < r1 then 0 else y) * int (steps x)) + (\<Sum>x = r1..<k. int (if x < r1 then 0 else y) * int (steps x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x)) = (\<Sum>x<r1. int (if x < r1 then 0 else y) * int (steps x)) + (\<Sum>x = r1..<k. int (if x < r1 then 0 else y) * int (steps x))

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x<k. int (if x < r1 then 0 else y) * int (steps x)) = (\<Sum>x<r1. int (if x < r1 then 0 else y) * int (steps x)) + (\<Sum>x = r1..<k. int (if x < r1 then 0 else y) * int (steps x))

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "\<dots> = (\<Sum>x=r1..<k. int y * int (steps x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x<r1. int (if x < r1 then 0 else y) * int (steps x)) + (\<Sum>x = r1..<k. int (if x < r1 then 0 else y) * int (steps x)) = (\<Sum>x = r1..<k. int y * int (steps x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x<r1. int (if x < r1 then 0 else y) * int (steps x)) + (\<Sum>x = r1..<k. int (if x < r1 then 0 else y) * int (steps x)) = (\<Sum>x = r1..<k. int y * int (steps x))

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x<r1. int (if x < r1 then 0 else y) * int (steps x)) + (\<Sum>x = r1..<k. int (if x < r1 then 0 else y) * int (steps x)) = (\<Sum>x = r1..<k. int y * int (steps x))

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "\<dots> = int y * (\<Sum>x=r1..<k. int (steps x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = r1..<k. int y * int (steps x)) = int y * (\<Sum>x = r1..<k. int (steps x))
[PROOF STEP]
by (auto simp: sum_distrib_left[of "int y"])
[PROOF STATE]
proof (state)
this:
(\<Sum>x = r1..<k. int y * int (steps x)) = int y * (\<Sum>x = r1..<k. int (steps x))

goal (2 subgoals):
 1. r2 = k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
 2. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int y * (\<Sum>x = r1..<k. int (steps x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int y * (\<Sum>x = r1..<k. int (steps x))

goal (1 subgoal):
 1. (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int y * (\<Sum>x = r1..<k. int (steps x))
r2 = k

goal (1 subgoal):
 1. (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r2 \<noteq> k

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r2 \<noteq> k
[PROOF STEP]
have "r2<k"
[PROOF STATE]
proof (prove)
using this:
r2 \<noteq> k

goal (1 subgoal):
 1. r2 < k
[PROOF STEP]
using pigeon_cols
[PROOF STATE]
proof (prove)
using this:
r2 \<noteq> k
r1 \<in> {..<k + 1}
r2 \<in> {..<k + 1}
r1 < r2
(col \<circ> a_r) r1 = (col \<circ> a_r) r2

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

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
define aux_left where "aux_left =
        (\<lambda>x. int (if x < r1 then 0 else if x < r2 then y else l)
          * int (steps x))"
[PROOF STATE]
proof (state)
this:
aux_left = (\<lambda>x. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x))

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "(\<Sum>x<k. aux_left x) = (\<Sum>x=r1..<k. aux_left x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum aux_left {..<k} = sum aux_left {r1..<k}
[PROOF STEP]
by (intro sum.mono_neutral_right) (auto simp: aux_left_def)
[PROOF STATE]
proof (state)
this:
sum aux_left {..<k} = sum aux_left {r1..<k}

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum aux_left {..<k} = sum aux_left {r1..<k}

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "{r1..<k} = {r1..<r2} \<union> {r2..<k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {r1..<k} = {r1..<r2} \<union> {r2..<k}
[PROOF STEP]
using \<open>r1 < r2\<close> \<open>r2 < k\<close>
[PROOF STATE]
proof (prove)
using this:
r1 < r2
r2 < k

goal (1 subgoal):
 1. {r1..<k} = {r1..<r2} \<union> {r2..<k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{r1..<k} = {r1..<r2} \<union> {r2..<k}

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{r1..<k} = {r1..<r2} \<union> {r2..<k}

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "(\<Sum>x\<in>\<dots>. aux_left x) = (\<Sum>x=r1..<r2. aux_left x) +
        (\<Sum>x=r2..<k. aux_left x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum aux_left ({r1..<r2} \<union> {r2..<k}) = sum aux_left {r1..<r2} + sum aux_left {r2..<k}
[PROOF STEP]
by (intro sum.union_disjoint) auto
[PROOF STATE]
proof (state)
this:
sum aux_left ({r1..<r2} \<union> {r2..<k}) = sum aux_left {r1..<r2} + sum aux_left {r2..<k}

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum aux_left ({r1..<r2} \<union> {r2..<k}) = sum aux_left {r1..<r2} + sum aux_left {r2..<k}

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "(\<Sum>x=r1..<r2. aux_left x) =
        (\<Sum>x=r1..<r2. int y * int (steps x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum aux_left {r1..<r2} = (\<Sum>x = r1..<r2. int y * int (steps x))
[PROOF STEP]
by (intro sum.cong) (auto simp: aux_left_def)
[PROOF STATE]
proof (state)
this:
sum aux_left {r1..<r2} = (\<Sum>x = r1..<r2. int y * int (steps x))

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum aux_left {r1..<r2} = (\<Sum>x = r1..<r2. int y * int (steps x))

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
have "(\<Sum>x=r2..<k. aux_left x) =
        (\<Sum>x=r2..<k. int l * int (steps x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum aux_left {r2..<k} = (\<Sum>x = r2..<k. int l * int (steps x))
[PROOF STEP]
using \<open>r1 < r2\<close>
[PROOF STATE]
proof (prove)
using this:
r1 < r2

goal (1 subgoal):
 1. sum aux_left {r2..<k} = (\<Sum>x = r2..<k. int l * int (steps x))
[PROOF STEP]
by (intro sum.cong) (auto simp: aux_left_def)
[PROOF STATE]
proof (state)
this:
sum aux_left {r2..<k} = (\<Sum>x = r2..<k. int l * int (steps x))

goal (1 subgoal):
 1. r2 \<noteq> k \<Longrightarrow> (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum aux_left {..<k} = (\<Sum>x = r1..<r2. int y * int (steps x)) + (\<Sum>x = r2..<k. int l * int (steps x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum aux_left {..<k} = (\<Sum>x = r1..<r2. int y * int (steps x)) + (\<Sum>x = r2..<k. int l * int (steps x))

goal (1 subgoal):
 1. (\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
by (simp add: aux_left_def sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int y * (\<Sum>x = r1..<r2. int (steps x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then ?y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int ?y * (\<Sum>x = r1..<r2. int (steps x))

goal (1 subgoal):
 1. h = arith_prog h_start h_step
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then ?y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int ?y * (\<Sum>x = r1..<r2. int (steps x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then ?y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int ?y * (\<Sum>x = r1..<r2. int (steps x))

goal (1 subgoal):
 1. h = arith_prog h_start h_step
[PROOF STEP]
unfolding arith_prog_def h_start_def h_step_def h_def f_def
        multi_arith_prog_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x<k. int (if x < r1 then 0 else if x < r2 then ?y else l) * int (steps x)) = int l * (\<Sum>x = r2..<k. int (steps x)) + int ?y * (\<Sum>x = r1..<r2. int (steps x))

goal (1 subgoal):
 1. (\<lambda>x. start + int (\<Sum>i<k. (if i < r1 then 0 else if i < r2 then x else l) * steps i)) = (\<lambda>i. start + int (l * sum steps {r2..<k}) + int (i * sum steps {r1..<r2}))
[PROOF STEP]
by (auto split:if_splits)
[PROOF STATE]
proof (state)
this:
h = arith_prog h_start h_step

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
h = arith_prog h_start h_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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define j where "j = col (h 0)"
[PROOF STATE]
proof (state)
this:
j = col (h 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have case_j: "j<k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < k
[PROOF STEP]
using 1 range_col_a_r \<open>col (h 0) = col (h l)\<close>
      \<open>h l = a_r r1\<close> j_def pigeon_cols(1)
[PROOF STATE]
proof (prove)
using this:
a + int N \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
?x < k + 1 \<Longrightarrow> col (a_r ?x) < k
col (h 0) = col (h l)
h l = a_r r1
j = col (h 0)
r1 \<in> {..<k + 1}

goal (1 subgoal):
 1. j < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have case_step: "h_step > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < h_step
[PROOF STEP]
unfolding h_step_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < sum steps {r1..<r2}
[PROOF STEP]
using pigeon_cols
[PROOF STATE]
proof (prove)
using this:
r1 \<in> {..<k + 1}
r2 \<in> {..<k + 1}
r1 < r2
(col \<circ> a_r) r1 = (col \<circ> a_r) r2

goal (1 subgoal):
 1. 0 < sum steps {r1..<r2}
[PROOF STEP]
by (intro sum_pos prog(1)) auto
[PROOF STATE]
proof (state)
this:
0 < h_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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have range_h: "h i \<in> {a..b}" if "i < l + 1" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h i \<in> {a..b}
[PROOF STEP]
unfolding h_def f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multi_arith_prog k start steps (\<lambda>ia. if ia < r1 then 0 else if ia < r2 then i else l) \<in> {a..b}
[PROOF STEP]
by (rule is_multi_arith_prog_onD[OF prog(2)])
      (use that in auto)
[PROOF STATE]
proof (state)
this:
?i < l + 1 \<Longrightarrow> h ?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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have case_on: "is_arith_prog_on (l+1) h_start h_step a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arith_prog_on (l + 1) h_start h_step a b
[PROOF STEP]
unfolding is_arith_prog_on_def h_arith_prog
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> h_start \<and> arith_prog h_start h_step (l + 1 - 1) \<le> b
[PROOF STEP]
using range_h[of 0] range_h[of l]
[PROOF STATE]
proof (prove)
using this:
0 < l + 1 \<Longrightarrow> h 0 \<in> {a..b}
l < l + 1 \<Longrightarrow> h l \<in> {a..b}

goal (1 subgoal):
 1. a \<le> h_start \<and> arith_prog h_start h_step (l + 1 - 1) \<le> b
[PROOF STEP]
by (auto simp: Max_ge[of "{a..b}"] Min_le[of "{a..b}"]
        h_arith_prog arith_prog_def)
[PROOF STATE]
proof (state)
this:
is_arith_prog_on (l + 1) h_start h_step 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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have case_col: "h ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
using h_col range_h
[PROOF STATE]
proof (prove)
using this:
?i \<in> {..<l + 1} \<Longrightarrow> col (h 0) = col (h ?i)
?i < l + 1 \<Longrightarrow> h ?i \<in> {a..b}

goal (1 subgoal):
 1. h ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
unfolding j_def
[PROOF STATE]
proof (prove)
using this:
?i \<in> {..<l + 1} \<Longrightarrow> col (h 0) = col (h ?i)
?i < l + 1 \<Longrightarrow> h ?i \<in> {a..b}

goal (1 subgoal):
 1. h ` {..<Suc l} \<subseteq> col -` {col (h 0)} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h ` {..<Suc l} \<subseteq> col -` {j} \<inter> {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>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
using case_j case_step case_on case_col
[PROOF STATE]
proof (prove)
using this:
j < k
0 < h_step
is_arith_prog_on (l + 1) h_start h_step a b
h ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}

goal (1 subgoal):
 1. \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
by (auto simp: h_arith_prog)
[PROOF STATE]
proof (state)
this:
\<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on (Suc l) start step a b \<and> arith_prog start step ` {..<Suc l} \<subseteq> col -` {j} \<inter> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem van_der_Waerden: assumes "l>0" "k>0" shows "\<exists>n. vdw k l n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. vdw k l n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < l
0 < k

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

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

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

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

goal (1 subgoal):
 1. \<exists>a. vdw k l a
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. l = 1 \<Longrightarrow> \<exists>a. vdw k l a
 2. l = 2 \<Longrightarrow> \<exists>a. vdw k l a
 3. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
assume "l=1"
[PROOF STATE]
proof (state)
this:
l = 1

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

goal (1 subgoal):
 1. \<exists>a. vdw k l a
[PROOF STEP]
using vdw_1_right
[PROOF STATE]
proof (prove)
using this:
l = 1
vdw ?k 1 1

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

goal (2 subgoals):
 1. l = 2 \<Longrightarrow> \<exists>a. vdw k l a
 2. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = 2 \<Longrightarrow> \<exists>a. vdw k l a
 2. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
assume "l=2"
[PROOF STATE]
proof (state)
this:
l = 2

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

goal (1 subgoal):
 1. \<exists>a. vdw k l a
[PROOF STEP]
using vdw_2_right
[PROOF STATE]
proof (prove)
using this:
l = 2
vdw ?k 2 (?k + 1)

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

goal (1 subgoal):
 1. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
assume "l > 2"
[PROOF STATE]
proof (state)
this:
2 < l

goal (1 subgoal):
 1. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 < l
[PROOF STEP]
have "2\<le>l-1"
[PROOF STATE]
proof (prove)
using this:
2 < l

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

goal (1 subgoal):
 1. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
from less.IH[of "l-1"] \<open>l>2\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>l - 1 < l; 0 < l - 1; 0 < ?k\<rbrakk> \<Longrightarrow> \<exists>a. vdw ?k (l - 1) a
2 < l
[PROOF STEP]
have "\<And>k'. k'>0 \<Longrightarrow> \<exists>n. vdw k' (l-1) n"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>l - 1 < l; 0 < l - 1; 0 < ?k\<rbrakk> \<Longrightarrow> \<exists>a. vdw ?k (l - 1) a
2 < l

goal (1 subgoal):
 1. \<And>k'. 0 < k' \<Longrightarrow> \<exists>n. vdw k' (l - 1) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ?k' \<Longrightarrow> \<exists>n. vdw ?k' (l - 1) n

goal (1 subgoal):
 1. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
with vdw_imp_vdw_lemma[of "l-1" k k] \<open>l-1\<ge>2\<close> \<open>k>0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>k'. 0 < k' \<Longrightarrow> \<exists>n_k'. vdw k' (l - 1) n_k'; 2 \<le> l - 1; 0 < k; 0 < k\<rbrakk> \<Longrightarrow> \<exists>N. vdw_lemma k k (l - 1) N
2 \<le> l - 1
0 < k
0 < ?k' \<Longrightarrow> \<exists>n. vdw ?k' (l - 1) n
[PROOF STEP]
obtain N where "vdw_lemma k k (l-1) N"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k'. 0 < k' \<Longrightarrow> \<exists>n_k'. vdw k' (l - 1) n_k'; 2 \<le> l - 1; 0 < k; 0 < k\<rbrakk> \<Longrightarrow> \<exists>N. vdw_lemma k k (l - 1) N
2 \<le> l - 1
0 < k
0 < ?k' \<Longrightarrow> \<exists>n. vdw ?k' (l - 1) n

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

goal (1 subgoal):
 1. 2 < l \<Longrightarrow> \<exists>a. vdw k l a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vdw_lemma k k (l - 1) N
[PROOF STEP]
have "vdw k l N"
[PROOF STATE]
proof (prove)
using this:
vdw_lemma k k (l - 1) N

goal (1 subgoal):
 1. vdw k l N
[PROOF STEP]
using vdw_lemma_imp_vdw[of k "l-1" N]
[PROOF STATE]
proof (prove)
using this:
vdw_lemma k k (l - 1) N
vdw_lemma k k (l - 1) N \<Longrightarrow> vdw k (Suc (l - 1)) N

goal (1 subgoal):
 1. vdw k l N
[PROOF STEP]
by (simp add: less.prems(1))
[PROOF STATE]
proof (state)
this:
vdw k l N

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ext_mono[mono]: "gt \<le> gt' \<Longrightarrow> ext gt \<le> ext gt'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gt \<le> gt' \<Longrightarrow> ext gt \<le> ext gt'
[PROOF STEP]
by (simp add: ext.mono ext_ext_compat_list[unfolded ext_compat_list_def, THEN conjunct1])


[STATEMENT]
lemma prod_qbs_MxI:
  assumes "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) \<in> qbs_Mx (M i)"
      and "\<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) = (\<lambda>r. undefined)"
    shows "\<alpha> \<in> prod_qbs_Mx I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<in> prod_qbs_Mx I M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i \<in> I \<Longrightarrow> (\<lambda>r. \<alpha> r ?i) \<in> qbs_Mx (M ?i)
?i \<notin> I \<Longrightarrow> (\<lambda>r. \<alpha> r ?i) = (\<lambda>r. undefined)

goal (1 subgoal):
 1. \<alpha> \<in> prod_qbs_Mx I M
[PROOF STEP]
by(auto simp: prod_qbs_Mx_def)


[STATEMENT]
lemma prod_qbs_MxE:
  assumes "\<alpha> \<in> prod_qbs_Mx I M"
  shows "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) \<in> qbs_Mx (M i)"
    and "\<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) = (\<lambda>r. undefined)"
    and "\<And>i r. i \<notin> I \<Longrightarrow> \<alpha> r i = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) \<in> qbs_Mx (M i)) &&& (\<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) = (\<lambda>r. undefined)) &&& (\<And>i r. i \<notin> I \<Longrightarrow> \<alpha> r i = undefined)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> prod_qbs_Mx I M

goal (1 subgoal):
 1. (\<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) \<in> qbs_Mx (M i)) &&& (\<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. \<alpha> r i) = (\<lambda>r. undefined)) &&& (\<And>i r. i \<notin> I \<Longrightarrow> \<alpha> r i = undefined)
[PROOF STEP]
by(auto simp: prod_qbs_Mx_def dest: fun_cong[where g="(\<lambda>r. undefined)"])


[STATEMENT]
lemma PiQ_f: "prod_qbs_Mx I M \<subseteq> UNIV \<rightarrow> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_qbs_Mx I M \<subseteq> UNIV \<rightarrow> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))
[PROOF STEP]
using prod_qbs_MxE
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<alpha> \<in> prod_qbs_Mx ?I ?M; ?i \<in> ?I\<rbrakk> \<Longrightarrow> (\<lambda>r. ?\<alpha> r ?i) \<in> qbs_Mx (?M ?i)
\<lbrakk>?\<alpha> \<in> prod_qbs_Mx ?I ?M; ?i \<notin> ?I\<rbrakk> \<Longrightarrow> (\<lambda>r. ?\<alpha> r ?i) = (\<lambda>r. undefined)
\<lbrakk>?\<alpha> \<in> prod_qbs_Mx ?I ?M; ?i \<notin> ?I\<rbrakk> \<Longrightarrow> ?\<alpha> ?r ?i = undefined

goal (1 subgoal):
 1. prod_qbs_Mx I M \<subseteq> UNIV \<rightarrow> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma PiQ_closed1: "qbs_closed1 (prod_qbs_Mx I M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_closed1 (prod_qbs_Mx I M)
[PROOF STEP]
proof(rule qbs_closed1I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha> f. \<lbrakk>\<alpha> \<in> prod_qbs_Mx I M; f \<in> borel_measurable real_borel\<rbrakk> \<Longrightarrow> \<alpha> \<circ> f \<in> prod_qbs_Mx I M
[PROOF STEP]
fix \<alpha> f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha> f. \<lbrakk>\<alpha> \<in> prod_qbs_Mx I M; f \<in> borel_measurable real_borel\<rbrakk> \<Longrightarrow> \<alpha> \<circ> f \<in> prod_qbs_Mx I M
[PROOF STEP]
assume h:"\<alpha> \<in> prod_qbs_Mx I M "
           "f \<in> real_borel \<rightarrow>\<^sub>M real_borel"
[PROOF STATE]
proof (state)
this:
\<alpha> \<in> prod_qbs_Mx I M
f \<in> borel_measurable real_borel

goal (1 subgoal):
 1. \<And>\<alpha> f. \<lbrakk>\<alpha> \<in> prod_qbs_Mx I M; f \<in> borel_measurable real_borel\<rbrakk> \<Longrightarrow> \<alpha> \<circ> f \<in> prod_qbs_Mx I M
[PROOF STEP]
show "\<alpha> \<circ> f \<in> prod_qbs_Mx I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<circ> f \<in> prod_qbs_Mx I M
[PROOF STEP]
proof(rule prod_qbs_MxI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
assume "i \<in> I"
[PROOF STATE]
proof (state)
this:
i \<in> I

goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
from prod_qbs_MxE(1)[OF h(1) this]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>r. \<alpha> r i) \<in> qbs_Mx (M i)
[PROOF STEP]
have "(\<lambda>r. \<alpha> r i) \<circ> f \<in> qbs_Mx (M i)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>r. \<alpha> r i) \<in> qbs_Mx (M i)

goal (1 subgoal):
 1. (\<lambda>r. \<alpha> r i) \<circ> f \<in> qbs_Mx (M i)
[PROOF STEP]
using h(2)
[PROOF STATE]
proof (prove)
using this:
(\<lambda>r. \<alpha> r i) \<in> qbs_Mx (M i)
f \<in> borel_measurable real_borel

goal (1 subgoal):
 1. (\<lambda>r. \<alpha> r i) \<circ> f \<in> qbs_Mx (M i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>r. \<alpha> r i) \<circ> f \<in> qbs_Mx (M i)

goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
thus "(\<lambda>r. (\<alpha> \<circ> f) r i) \<in> qbs_Mx (M i)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>r. \<alpha> r i) \<circ> f \<in> qbs_Mx (M i)

goal (1 subgoal):
 1. (\<lambda>r. (\<alpha> \<circ> f) r i) \<in> qbs_Mx (M i)
[PROOF STEP]
by(simp add: comp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>r. (\<alpha> \<circ> f) r i) \<in> qbs_Mx (M i)

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
assume "i \<notin> I"
[PROOF STATE]
proof (state)
this:
i \<notin> I

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
from prod_qbs_MxE(3)[OF h(1) this]
[PROOF STATE]
proof (chain)
picking this:
\<alpha> ?r i = undefined
[PROOF STEP]
show "(\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)"
[PROOF STATE]
proof (prove)
using this:
\<alpha> ?r i = undefined

goal (1 subgoal):
 1. (\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>r. (\<alpha> \<circ> f) r i) = (\<lambda>r. undefined)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<alpha> \<circ> f \<in> prod_qbs_Mx I M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PiQ_closed2: "qbs_closed2 (\<Pi>\<^sub>E i\<in>I. qbs_space (M i)) (prod_qbs_Mx I M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_closed2 (\<Pi>\<^sub>E i\<in>I. qbs_space (M i)) (prod_qbs_Mx I M)
[PROOF STEP]
proof(rule qbs_closed2I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i)) \<Longrightarrow> (\<lambda>r. x) \<in> prod_qbs_Mx I M
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i)) \<Longrightarrow> (\<lambda>r. x) \<in> prod_qbs_Mx I M
[PROOF STEP]
assume h:"x \<in> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))"
[PROOF STATE]
proof (state)
this:
x \<in> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i)) \<Longrightarrow> (\<lambda>r. x) \<in> prod_qbs_Mx I M
[PROOF STEP]
show "(\<lambda>r. x) \<in> prod_qbs_Mx I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. x) \<in> prod_qbs_Mx I M
[PROOF STEP]
proof(rule prod_qbs_MxI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. x i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. x i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
assume hi:"i \<in> I"
[PROOF STATE]
proof (state)
this:
i \<in> I

goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. x i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> I
[PROOF STEP]
have "x i \<in> qbs_space (M i)"
[PROOF STATE]
proof (prove)
using this:
i \<in> I

goal (1 subgoal):
 1. x i \<in> qbs_space (M i)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
i \<in> I
x \<in> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))

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

goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. x i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
thus "(\<lambda>r. x i) \<in> qbs_Mx (M i)"
[PROOF STATE]
proof (prove)
using this:
x i \<in> qbs_space (M i)

goal (1 subgoal):
 1. (\<lambda>r. x i) \<in> qbs_Mx (M i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>r. x i) \<in> qbs_Mx (M i)

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
show "\<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. x i) = (\<lambda>r. undefined)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<notin> I \<Longrightarrow> (\<lambda>r. x ?i) = (\<lambda>r. undefined)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>r. x) \<in> prod_qbs_Mx I M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PiQ_closed3: "qbs_closed3 (prod_qbs_Mx I M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_closed3 (prod_qbs_Mx I M)
[PROOF STEP]
proof(rule qbs_closed3I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Fi. \<lbrakk>\<And>i. P -` {i} \<in> sets real_borel; \<And>i. Fi i \<in> prod_qbs_Mx I M\<rbrakk> \<Longrightarrow> (\<lambda>r. Fi (P r) r) \<in> prod_qbs_Mx I M
[PROOF STEP]
fix P Fi
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Fi. \<lbrakk>\<And>i. P -` {i} \<in> sets real_borel; \<And>i. Fi i \<in> prod_qbs_Mx I M\<rbrakk> \<Longrightarrow> (\<lambda>r. Fi (P r) r) \<in> prod_qbs_Mx I M
[PROOF STEP]
assume h:"\<And>i::nat. P -` {i} \<in> sets real_borel"
           "\<And>i::nat. Fi i \<in> prod_qbs_Mx I M"
[PROOF STATE]
proof (state)
this:
P -` {?i} \<in> sets real_borel
Fi ?i \<in> prod_qbs_Mx I M

goal (1 subgoal):
 1. \<And>P Fi. \<lbrakk>\<And>i. P -` {i} \<in> sets real_borel; \<And>i. Fi i \<in> prod_qbs_Mx I M\<rbrakk> \<Longrightarrow> (\<lambda>r. Fi (P r) r) \<in> prod_qbs_Mx I M
[PROOF STEP]
show "(\<lambda>r. Fi (P r) r) \<in> prod_qbs_Mx I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. Fi (P r) r) \<in> prod_qbs_Mx I M
[PROOF STEP]
proof(rule prod_qbs_MxI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)
[PROOF STEP]
assume hi:"i \<in> I"
[PROOF STATE]
proof (state)
this:
i \<in> I

goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)
[PROOF STEP]
show "(\<lambda>r. Fi (P r) r i) \<in> qbs_Mx (M i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. Fi (P r) r i) \<in> qbs_Mx (M i)
[PROOF STEP]
using prod_qbs_MxE(1)[OF h(2) hi] qbs_closed3_dest[OF h(1),of "\<lambda>j r. Fi j r i"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>r. Fi ?i1 r i) \<in> qbs_Mx (M i)
(\<And>ia. (\<lambda>r. Fi ia r i) \<in> qbs_Mx ?X) \<Longrightarrow> (\<lambda>r. Fi (P r) r i) \<in> qbs_Mx ?X

goal (1 subgoal):
 1. (\<lambda>r. Fi (P r) r i) \<in> qbs_Mx (M i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>r. Fi (P r) r i) \<in> qbs_Mx (M i)

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)
[PROOF STEP]
show "\<And>i. i \<notin> I \<Longrightarrow>
         (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)
[PROOF STEP]
using prod_qbs_MxE[OF h(2)]
[PROOF STATE]
proof (prove)
using this:
?i \<in> I \<Longrightarrow> (\<lambda>r. Fi ?i1 r ?i) \<in> qbs_Mx (M ?i)
?i \<notin> I \<Longrightarrow> (\<lambda>r. Fi ?i1 r ?i) = (\<lambda>r. undefined)
?i \<notin> I \<Longrightarrow> Fi ?i1 ?r ?i = undefined

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r i) = (\<lambda>r. undefined)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<notin> I \<Longrightarrow> (\<lambda>r. Fi (P r) r ?i) = (\<lambda>r. undefined)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>r. Fi (P r) r) \<in> prod_qbs_Mx I M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PiQ_correct: "Rep_quasi_borel (PiQ I M) = (\<Pi>\<^sub>E i\<in>I. qbs_space (M i), prod_qbs_Mx I M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_quasi_borel (PiQ I M) = (\<Pi>\<^sub>E i\<in>I. qbs_space (M i), prod_qbs_Mx I M)
[PROOF STEP]
by(auto intro!: Abs_quasi_borel_inverse PiQ_f is_quasi_borel_intro simp: PiQ_def PiQ_closed1 PiQ_closed2 PiQ_closed3)


[STATEMENT]
lemma PiQ_space[simp]: "qbs_space (PiQ I M) = (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_space (PiQ I M) = (\<Pi>\<^sub>E i\<in>I. qbs_space (M i))
[PROOF STEP]
by(simp add: qbs_space_def PiQ_correct)


[STATEMENT]
lemma PiQ_Mx[simp]: "qbs_Mx (PiQ I M) = prod_qbs_Mx I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_Mx (PiQ I M) = prod_qbs_Mx I M
[PROOF STEP]
by(simp add: qbs_Mx_def PiQ_correct)


[STATEMENT]
lemma qbs_morphism_component_singleton:
  assumes "i \<in> I"
  shows "(\<lambda>x. x i) \<in> (\<Pi>\<^sub>Q i\<in>I. (M i)) \<rightarrow>\<^sub>Q M i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x i) \<in> PiQ I M \<rightarrow>\<^sub>Q M i
[PROOF STEP]
by(auto intro!: qbs_morphismI simp: prod_qbs_Mx_def comp_def assms)


[STATEMENT]
lemma product_qbs_canonical1:
  assumes "\<And>i. i \<in> I \<Longrightarrow> f i \<in> Y \<rightarrow>\<^sub>Q X i"
      and "\<And>i. i \<notin> I \<Longrightarrow> f i = (\<lambda>y. undefined)"
    shows "(\<lambda>y i. f i y) \<in> Y \<rightarrow>\<^sub>Q (\<Pi>\<^sub>Q i\<in>I. X i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>y i. f i y) \<in> Y \<rightarrow>\<^sub>Q PiQ I X
[PROOF STEP]
using qbs_morphismE(3)[simplified comp_def,OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 \<in> I; ?\<alpha> \<in> qbs_Mx Y\<rbrakk> \<Longrightarrow> (\<lambda>x. f ?i1 (?\<alpha> x)) \<in> qbs_Mx (X ?i1)
?i \<notin> I \<Longrightarrow> f ?i = (\<lambda>y. undefined)

goal (1 subgoal):
 1. (\<lambda>y i. f i y) \<in> Y \<rightarrow>\<^sub>Q PiQ I X
[PROOF STEP]
by(auto intro!: qbs_morphismI prod_qbs_MxI)


[STATEMENT]
lemma product_qbs_canonical2:
  assumes "\<And>i. i \<in> I \<Longrightarrow> f i \<in> Y \<rightarrow>\<^sub>Q X i"
          "\<And>i. i \<notin> I \<Longrightarrow> f i = (\<lambda>y. undefined)"
          "g \<in> Y \<rightarrow>\<^sub>Q (\<Pi>\<^sub>Q i\<in>I. X i)"
          "\<And>i. i \<in> I \<Longrightarrow> f i = (\<lambda>x. x i) \<circ> g"
      and "y \<in> qbs_space Y"
    shows "g y = (\<lambda>i. f i y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g y = (\<lambda>i. f i y)
[PROOF STEP]
proof(rule ext)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. g y i = f i y
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. g y i = f i y
[PROOF STEP]
show "g y i = f i y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g y i = f i y
[PROOF STEP]
proof(cases "i \<in> I")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> I \<Longrightarrow> g y i = f i y
 2. i \<notin> I \<Longrightarrow> g y i = f i y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> I

goal (2 subgoals):
 1. i \<in> I \<Longrightarrow> g y i = f i y
 2. i \<notin> I \<Longrightarrow> g y i = f i y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> I

goal (1 subgoal):
 1. g y i = f i y
[PROOF STEP]
using assms(4)[of i]
[PROOF STATE]
proof (prove)
using this:
i \<in> I
i \<in> I \<Longrightarrow> f i = (\<lambda>x. x i) \<circ> g

goal (1 subgoal):
 1. g y i = f i y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g y i = f i y

goal (1 subgoal):
 1. i \<notin> I \<Longrightarrow> g y i = f i y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<notin> I \<Longrightarrow> g y i = f i y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> I

goal (1 subgoal):
 1. i \<notin> I \<Longrightarrow> g y i = f i y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<notin> I

goal (1 subgoal):
 1. i \<notin> I \<Longrightarrow> g y i = f i y
[PROOF STEP]
have "(\<lambda>r. y) \<in> qbs_Mx Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. y) \<in> qbs_Mx Y
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
y \<in> qbs_space Y

goal (1 subgoal):
 1. (\<lambda>r. y) \<in> qbs_Mx Y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>r. y) \<in> qbs_Mx Y

goal (1 subgoal):
 1. i \<notin> I \<Longrightarrow> g y i = f i y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<notin> I
(\<lambda>r. y) \<in> qbs_Mx Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<notin> I
(\<lambda>r. y) \<in> qbs_Mx Y

goal (1 subgoal):
 1. g y i = f i y
[PROOF STEP]
using assms(2,3) qbs_morphismE(3)[OF assms(3) _]
[PROOF STATE]
proof (prove)
using this:
i \<notin> I
(\<lambda>r. y) \<in> qbs_Mx Y
?i \<notin> I \<Longrightarrow> f ?i = (\<lambda>y. undefined)
g \<in> Y \<rightarrow>\<^sub>Q PiQ I X
?\<alpha> \<in> qbs_Mx Y \<Longrightarrow> g \<circ> ?\<alpha> \<in> qbs_Mx (PiQ I X)

goal (1 subgoal):
 1. g y i = f i y
[PROOF STEP]
by(fastforce simp: prod_qbs_Mx_def)
[PROOF STATE]
proof (state)
this:
g y i = f i y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g y i = f i y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma merge_qbs_morphism:
 "merge I J \<in> (\<Pi>\<^sub>Q i\<in>I. (M i)) \<Otimes>\<^sub>Q (\<Pi>\<^sub>Q j\<in>J. (M j)) \<rightarrow>\<^sub>Q (\<Pi>\<^sub>Q i\<in>I\<union>J. (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge I J \<in> PiQ I M \<Otimes>\<^sub>Q PiQ J M \<rightarrow>\<^sub>Q PiQ (I \<union> J) M
[PROOF STEP]
proof(rule qbs_morphismI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> qbs_Mx (PiQ I M \<Otimes>\<^sub>Q PiQ J M) \<Longrightarrow> merge I J \<circ> \<alpha> \<in> qbs_Mx (PiQ (I \<union> J) M)
[PROOF STEP]
fix \<alpha>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> qbs_Mx (PiQ I M \<Otimes>\<^sub>Q PiQ J M) \<Longrightarrow> merge I J \<circ> \<alpha> \<in> qbs_Mx (PiQ (I \<union> J) M)
[PROOF STEP]
assume h:"\<alpha> \<in> qbs_Mx ((\<Pi>\<^sub>Q i\<in>I. (M i)) \<Otimes>\<^sub>Q (\<Pi>\<^sub>Q j\<in>J. (M j)))"
[PROOF STATE]
proof (state)
this:
\<alpha> \<in> qbs_Mx (PiQ I M \<Otimes>\<^sub>Q PiQ J M)

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> qbs_Mx (PiQ I M \<Otimes>\<^sub>Q PiQ J M) \<Longrightarrow> merge I J \<circ> \<alpha> \<in> qbs_Mx (PiQ (I \<union> J) M)
[PROOF STEP]
show "merge I J \<circ> \<alpha> \<in> qbs_Mx (\<Pi>\<^sub>Q i\<in>I\<union>J. (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge I J \<circ> \<alpha> \<in> qbs_Mx (PiQ (I \<union> J) M)
[PROOF STEP]
proof(simp, rule prod_qbs_MxI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
assume "i \<in> I \<union> J"
[PROOF STATE]
proof (state)
this:
i \<in> I \<union> J

goal (2 subgoals):
 1. \<And>i. i \<in> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> I \<union> J
[PROOF STEP]
consider "i \<in> I" | "i \<in> I \<and> i \<in> J" | "i \<notin> I \<and> i \<in> J"
[PROOF STATE]
proof (prove)
using this:
i \<in> I \<union> J

goal (1 subgoal):
 1. \<lbrakk>i \<in> I \<Longrightarrow> thesis; i \<in> I \<and> i \<in> J \<Longrightarrow> thesis; i \<notin> I \<and> i \<in> J \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<in> I \<Longrightarrow> ?thesis; i \<in> I \<and> i \<in> J \<Longrightarrow> ?thesis; i \<notin> I \<and> i \<in> J \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. \<And>i. i \<in> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 2. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<in> I \<Longrightarrow> ?thesis; i \<in> I \<and> i \<in> J \<Longrightarrow> ?thesis; i \<notin> I \<and> i \<in> J \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "(\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in> I \<Longrightarrow> ?thesis; i \<in> I \<and> i \<in> J \<Longrightarrow> ?thesis; i \<notin> I \<and> i \<in> J \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i \<in> I \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 2. i \<in> I \<and> i \<in> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 3. i \<notin> I \<and> i \<in> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> qbs_Mx (PiQ I M \<Otimes>\<^sub>Q PiQ J M)

goal (3 subgoals):
 1. i \<in> I \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 2. i \<in> I \<and> i \<in> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
 3. i \<notin> I \<and> i \<in> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)
[PROOF STEP]
by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE)
[PROOF STATE]
proof (state)
this:
(\<lambda>r. (merge I J \<circ> \<alpha>) r i) \<in> qbs_Mx (M i)

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
assume "i \<notin> I \<union> J"
[PROOF STATE]
proof (state)
this:
i \<notin> I \<union> J

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<union> J \<Longrightarrow> (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<notin> I \<union> J
[PROOF STEP]
show "(\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)"
[PROOF STATE]
proof (prove)
using this:
i \<notin> I \<union> J

goal (1 subgoal):
 1. (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
i \<notin> I \<union> J
\<alpha> \<in> qbs_Mx (PiQ I M \<Otimes>\<^sub>Q PiQ J M)

goal (1 subgoal):
 1. (\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)
[PROOF STEP]
by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE )
[PROOF STATE]
proof (state)
this:
(\<lambda>r. (merge I J \<circ> \<alpha>) r i) = (\<lambda>r. undefined)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
merge I J \<circ> \<alpha> \<in> qbs_Mx (PiQ (I \<union> J) M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_preserves_product':
  "measure_to_qbs (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>Q i\<in>I. measure_to_qbs (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_to_qbs (Pi\<^sub>M I M) = (\<Pi>\<^sub>Q i\<in>I. measure_to_qbs (M i))
[PROOF STEP]
proof(rule qbs_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qbs_Mx (measure_to_qbs (Pi\<^sub>M I M)) = qbs_Mx (\<Pi>\<^sub>Q i\<in>I. measure_to_qbs (M i))
[PROOF STEP]
show "qbs_Mx (measure_to_qbs (Pi\<^sub>M I M)) = qbs_Mx (\<Pi>\<^sub>Q i\<in>I. measure_to_qbs (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qbs_Mx (measure_to_qbs (Pi\<^sub>M I M)) = qbs_Mx (\<Pi>\<^sub>Q i\<in>I. measure_to_qbs (M i))
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M \<Longrightarrow> x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))
 2. \<And>x. x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i)) \<Longrightarrow> x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M \<Longrightarrow> x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))
 2. \<And>x. x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i)) \<Longrightarrow> x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
assume h:"f \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M"
[PROOF STATE]
proof (state)
this:
f \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M

goal (2 subgoals):
 1. \<And>x. x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M \<Longrightarrow> x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))
 2. \<And>x. x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i)) \<Longrightarrow> x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
show "f \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))
[PROOF STEP]
proof(rule prod_qbs_MxI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. f r i) \<in> qbs_Mx (measure_to_qbs (M i))
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. f r i) \<in> qbs_Mx (measure_to_qbs (M i))
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
assume 1:"i \<in> I"
[PROOF STATE]
proof (state)
this:
i \<in> I

goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>r. f r i) \<in> qbs_Mx (measure_to_qbs (M i))
 2. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
show "(\<lambda>r. f r i) \<in> qbs_Mx (measure_to_qbs (M i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. f r i) \<in> qbs_Mx (measure_to_qbs (M i))
[PROOF STEP]
using measurable_comp[OF h measurable_component_singleton[OF 1,of M]]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x i) \<circ> f \<in> real_borel \<rightarrow>\<^sub>M M i

goal (1 subgoal):
 1. (\<lambda>r. f r i) \<in> qbs_Mx (measure_to_qbs (M i))
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>r. f r i) \<in> qbs_Mx (measure_to_qbs (M i))

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
assume 1:"i \<notin> I"
[PROOF STATE]
proof (state)
this:
i \<notin> I

goal (1 subgoal):
 1. \<And>i. i \<notin> I \<Longrightarrow> (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<notin> I
[PROOF STEP]
show "(\<lambda>r. f r i) = (\<lambda>r. undefined)"
[PROOF STATE]
proof (prove)
using this:
i \<notin> I

goal (1 subgoal):
 1. (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
using measurable_space[OF h] 1
[PROOF STATE]
proof (prove)
using this:
i \<notin> I
?x \<in> space real_borel \<Longrightarrow> f ?x \<in> space (Pi\<^sub>M I M)
i \<notin> I

goal (1 subgoal):
 1. (\<lambda>r. f r i) = (\<lambda>r. undefined)
[PROOF STEP]
by(auto simp: space_PiM PiE_def extensional_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>r. f r i) = (\<lambda>r. undefined)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))

goal (1 subgoal):
 1. \<And>x. x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i)) \<Longrightarrow> x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i)) \<Longrightarrow> x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i)) \<Longrightarrow> x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
assume h:"f \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))"
[PROOF STATE]
proof (state)
this:
f \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))

goal (1 subgoal):
 1. \<And>x. x \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i)) \<Longrightarrow> x \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
show "f \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M
[PROOF STEP]
apply(rule measurable_PiM_single')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>\<omega>. f \<omega> i) \<in> real_borel \<rightarrow>\<^sub>M M i
 2. f \<in> space real_borel \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))
[PROOF STEP]
using prod_qbs_MxE(1)[OF h]
[PROOF STATE]
proof (prove)
using this:
?i \<in> I \<Longrightarrow> (\<lambda>r. f r ?i) \<in> qbs_Mx (measure_to_qbs (M ?i))

goal (2 subgoals):
 1. \<And>i. i \<in> I \<Longrightarrow> (\<lambda>\<omega>. f \<omega> i) \<in> real_borel \<rightarrow>\<^sub>M M i
 2. f \<in> space real_borel \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space real_borel \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))
[PROOF STEP]
using PiQ_f[of I M] h
[PROOF STATE]
proof (prove)
using this:
prod_qbs_Mx I (\<lambda>x. measure_to_qbs (M x)) \<subseteq> UNIV \<rightarrow> (\<Pi>\<^sub>E i\<in>I. qbs_space (measure_to_qbs (M i)))
f \<in> prod_qbs_Mx I (\<lambda>i. measure_to_qbs (M i))

goal (1 subgoal):
 1. f \<in> space real_borel \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> real_borel \<rightarrow>\<^sub>M Pi\<^sub>M I M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
qbs_Mx (measure_to_qbs (Pi\<^sub>M I M)) = qbs_Mx (\<Pi>\<^sub>Q i\<in>I. measure_to_qbs (M i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_binary_product:
 "\<exists>f g. f \<in> (\<Pi>\<^sub>Q i\<in>UNIV. if i then X else Y) \<rightarrow>\<^sub>Q X \<Otimes>\<^sub>Q Y \<and> g \<in> X \<Otimes>\<^sub>Q Y \<rightarrow>\<^sub>Q (\<Pi>\<^sub>Q i\<in>UNIV. if i then X else Y) \<and>
        g \<circ> f = id \<and> f \<circ> g = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f g. f \<in> (\<Pi>\<^sub>Q i\<in>UNIV. if i then X else Y) \<rightarrow>\<^sub>Q X \<Otimes>\<^sub>Q Y \<and> g \<in> X \<Otimes>\<^sub>Q Y \<rightarrow>\<^sub>Q (\<Pi>\<^sub>Q i\<in>UNIV. if i then X else Y) \<and> g \<circ> f = id \<and> f \<circ> g = id
[PROOF STEP]
by(auto intro!: exI[where x="\<lambda>f. (f True, f False)"] exI[where x="\<lambda>xy b. if b then fst xy else snd xy"] qbs_morphismI
            simp: prod_qbs_Mx_def pair_qbs_Mx_def comp_def all_bool_eq ext)


[STATEMENT]
lemma \<delta>: assumes "(q,a,q',b,d) \<in> \<delta>"
  shows "q \<in> Q" "a k \<in> \<Gamma>" "q' \<in> Q" "b k \<in> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q \<in> Q &&& a k \<in> \<Gamma>) &&& q' \<in> Q &&& b k \<in> \<Gamma>
[PROOF STEP]
using assms \<delta>_set
[PROOF STATE]
proof (prove)
using this:
(q, a, q', b, d) \<in> \<delta>
\<delta> \<subseteq> (Q - {t, r}) \<times> (UNIV \<rightarrow> \<Gamma>) \<times> Q \<times> (UNIV \<rightarrow> \<Gamma>) \<times> (UNIV \<rightarrow> UNIV)

goal (1 subgoal):
 1. (q \<in> Q &&& a k \<in> \<Gamma>) &&& q' \<in> Q &&& b k \<in> \<Gamma>
[PROOF STEP]
by auto


[STATEMENT]
lemma fin_\<Sigma>: "finite \<Sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Sigma>
[PROOF STEP]
using fin_\<Gamma> \<Sigma>_sub_\<Gamma>
[PROOF STATE]
proof (prove)
using this:
finite \<Gamma>
\<Sigma> \<subseteq> \<Gamma>

goal (1 subgoal):
 1. finite \<Sigma>
[PROOF STEP]
by (metis finite_subset)


[STATEMENT]
lemma fin_\<delta>: "finite \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<delta>
[PROOF STEP]
by (intro finite_subset[OF \<delta>_set] finite_cartesian_product fin_funcsetI, insert fin_Q fin_\<Gamma>, auto)


[STATEMENT]
lemma valid_init_config: "set w \<subseteq> \<Sigma> \<Longrightarrow> valid_config (init_config w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set w \<subseteq> \<Sigma> \<Longrightarrow> valid_config (init_config w)
[PROOF STEP]
unfolding init_config_def valid_config.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set w \<subseteq> \<Sigma> \<Longrightarrow> s \<in> Q \<and> (\<forall>k. range (\<lambda>n. if n = 0 then LE else if k = (0::'k) \<and> n \<le> length w then w ! (n - 1) else blank) \<subseteq> \<Gamma>) \<and> (\<forall>k. (if 0 = 0 then LE else if k = (0::'k) \<and> 0 \<le> length w then w ! (0 - 1) else blank) = LE)
[PROOF STEP]
using tm
[PROOF STATE]
proof (prove)
using this:
s \<in> Q
\<Sigma> \<subseteq> \<Gamma>
blank \<in> \<Gamma>
LE \<in> \<Gamma>

goal (1 subgoal):
 1. set w \<subseteq> \<Sigma> \<Longrightarrow> s \<in> Q \<and> (\<forall>k. range (\<lambda>n. if n = 0 then LE else if k = (0::'k) \<and> n \<le> length w then w ! (n - 1) else blank) \<subseteq> \<Gamma>) \<and> (\<forall>k. (if 0 = 0 then LE else if k = (0::'k) \<and> 0 \<le> length w then w ! (0 - 1) else blank) = LE)
[PROOF STEP]
by (force simp: set_conv_nth)


[STATEMENT]
lemma valid_step: assumes step: "(\<alpha>,\<beta>) \<in> step"
  and val: "valid_config \<alpha>"
shows "valid_config \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_config \<beta>
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
(\<alpha>, \<beta>) \<in> step

goal (1 subgoal):
 1. valid_config \<beta>
[PROOF STEP]
proof (cases rule: step.cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q ts n q' a dir. \<lbrakk>\<alpha> = Config\<^sub>M q ts n; \<beta> = Config\<^sub>M q' (\<lambda>k. (ts k)(n k := a k)) (\<lambda>k. go_dir (dir k) (n k)); (q, \<lambda>k. ts k (n k), q', a, dir) \<in> \<delta>\<rbrakk> \<Longrightarrow> valid_config \<beta>
[PROOF STEP]
case (step q ts n q' a dir)
[PROOF STATE]
proof (state)
this:
\<alpha> = Config\<^sub>M q ts n
\<beta> = Config\<^sub>M q' (\<lambda>k. (ts k)(n k := a k)) (\<lambda>k. go_dir (dir k) (n k))
(q, \<lambda>k. ts k (n k), q', a, dir) \<in> \<delta>

goal (1 subgoal):
 1. \<And>q ts n q' a dir. \<lbrakk>\<alpha> = Config\<^sub>M q ts n; \<beta> = Config\<^sub>M q' (\<lambda>k. (ts k)(n k := a k)) (\<lambda>k. go_dir (dir k) (n k)); (q, \<lambda>k. ts k (n k), q', a, dir) \<in> \<delta>\<rbrakk> \<Longrightarrow> valid_config \<beta>
[PROOF STEP]
from \<delta>[OF step(3)] val \<delta>LE step(3)
[PROOF STATE]
proof (chain)
picking this:
q \<in> Q
ts ?k (n ?k) \<in> \<Gamma>
q' \<in> Q
a ?k \<in> \<Gamma>
valid_config \<alpha>
\<lbrakk>(?q, ?a, ?q', ?a', ?d) \<in> \<delta>; ?a ?k = LE\<rbrakk> \<Longrightarrow> ?a' ?k = LE \<and> ?d ?k \<in> {dir.N, dir.R}
(q, \<lambda>k. ts k (n k), q', a, dir) \<in> \<delta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> Q
ts ?k (n ?k) \<in> \<Gamma>
q' \<in> Q
a ?k \<in> \<Gamma>
valid_config \<alpha>
\<lbrakk>(?q, ?a, ?q', ?a', ?d) \<in> \<delta>; ?a ?k = LE\<rbrakk> \<Longrightarrow> ?a' ?k = LE \<and> ?d ?k \<in> {dir.N, dir.R}
(q, \<lambda>k. ts k (n k), q', a, dir) \<in> \<delta>

goal (1 subgoal):
 1. valid_config \<beta>
[PROOF STEP]
unfolding step(1-2)
[PROOF STATE]
proof (prove)
using this:
q \<in> Q
ts ?k (n ?k) \<in> \<Gamma>
q' \<in> Q
a ?k \<in> \<Gamma>
valid_config (Config\<^sub>M q ts n)
\<lbrakk>(?q, ?a, ?q', ?a', ?d) \<in> \<delta>; ?a ?k = LE\<rbrakk> \<Longrightarrow> ?a' ?k = LE \<and> ?d ?k \<in> {dir.N, dir.R}
(q, \<lambda>k. ts k (n k), q', a, dir) \<in> \<delta>

goal (1 subgoal):
 1. valid_config (Config\<^sub>M q' (\<lambda>k. (ts k)(n k := a k)) (\<lambda>k. go_dir (dir k) (n k)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_config \<beta>

goal:
No subgoals!
[PROOF STEP]
qed