Theory Hales_Jewett
theory "Hales_Jewett"
imports Main "HOL-Library.Disjoint_Sets" "HOL-Library.FuncSet"
begin
section ‹Preliminaries›
text ‹
The Hales--Jewett Theorem is at its core a statement about sets of tuples called the
$n$-dimensional cube over $t$ elements (denoted by $C^n_t$); i.e.\ the set $\{0,\ldots,t - 1\}^n$, where
$\{0,\ldots,t - 1\}$ is called the base.
We represent tuples by functions $f : \{0,\ldots,n - 1\} \rightarrow \{0,\ldots,t - 1\}$ because
they're easier to deal with. The set of tuples then becomes the function space
$\{0,\ldots,t - 1\}^{\{0,\ldots,n - 1\}}$.
Furthermore, $r$-colourings of the cube are represented by mappings from the function space to the
set $\{0,\ldots, r-1\}$.
›
subsection ‹The $n$-dimensional cube over $t$ elements›
text ‹
Function spaces in Isabelle are supported by the library component FuncSet.
In essence, \<^prop>‹f ∈ A →⇩E B› means \<^prop>‹a ∈ A ⟹ f a ∈ B› and \<^prop>‹a ∉ A ⟹ f a = undefined›
›
text ‹The (canonical) $n$-dimensional cube over $t$ elements is defined in the following using the variables:
\begin{tabular}{lcp{8cm}}
$n$:& \<^typ>‹nat›& dimension\\
$t$:& \<^typ>‹nat›& number of elements\\
\end{tabular}›
definition cube :: "nat ⇒ nat ⇒ (nat ⇒ nat) set"
where "cube n t ≡ {..<n} →⇩E {..<t}"
text ‹
For any function $f$ whose image under a set $A$ is a subset of another set $B$, there's
a unique function $g$ in the function space $B^A$ that equals $f$ everywhere in $A$.
The function $g$ is usually written as $f|_A$ in the mathematical literature.
›
lemma PiE_uniqueness: "f ` A ⊆ B ⟹ ∃!g ∈ A
→⇩E B. ∀a∈A. g a = f a"
using exI[of "λx. x ∈ A →⇩E B ∧ (∀a∈A. x a = f a)"
"restrict f A"] PiE_ext PiE_iff by fastforce
text ‹Any prefix of length $j$ of an $n$-tuple (i.e.\ element of $C^n_t$) is a $j$-tuple
(i.e.\ element of $C^j_t$).›
lemma cube_restrict:
assumes "j < n"
and "y ∈ cube n t"
shows "(λg ∈ {..<j}. y g) ∈ cube j t" using assms unfolding cube_def by force
text ‹Narrowing down the obvious fact $B^A \subseteq C^A$ if $B \subseteq C$ to a specific case for cubes. ›
lemma cube_subset: "cube n t ⊆ cube n (t + 1)"
unfolding cube_def using PiE_mono[of "{..<n}" "λx. {..<t}" "λx. {..<t+1}"]
by simp
text ‹A simplifying definition for the 0-dimensional cube.›
lemma cube0_alt_def: "cube 0 t = {λx. undefined}"
unfolding cube_def by simp
text ‹
The cardinality of the ‹n›-dimensional over ‹t› elements is simply a consequence of the overarching
definition of the cardinality of function spaces (over finite sets).›
lemma cube_card: "card ({..<n::nat} →⇩E {..<t::nat}) = t ^ n"
by (simp add: card_PiE)
text ‹A simplifying definition for the ‹n›-dimensional cube over
a single element, i.e.\ the single ‹n›-dimensional point ‹(0, …, 0)›.›
lemma cube1_alt_def: "cube n 1 = {λx∈{..<n}. 0}" unfolding cube_def by (simp add: lessThan_Suc)
subsection ‹Lines›
text ‹The property of being a line in $C^n_t$ is defined in the following using the variables:
\begin{tabular}{llp{8cm}}
$L$:& \<^typ>‹nat ⇒ (nat ⇒ nat)›& line\\
$n$:& \<^typ>‹nat›& dimension of cube\\
$t$:& \<^typ>‹nat›& the size of the cube's base\\
\end{tabular}›
definition is_line :: "(nat ⇒ (nat ⇒ nat)) ⇒ nat ⇒
nat ⇒ bool"
where "is_line L n t ≡ (L ∈ {..<t} →⇩E cube n t ∧
((∀j<n. (∀x<t. ∀y<t. L x j = L y j) ∨ (∀s<t. L s j = s))
∧ (∃j < n. (∀s < t. L s j = s))))"
text ‹We introduce an elimination rule to relate lines with the more general definition of a
subspace (see below). ›
lemma is_line_elim_t_1:
assumes "is_line L n t" and "t = 1"
obtains B⇩0 B⇩1
where "B⇩0 ∪ B⇩1 = {..<n} ∧ B⇩0 ∩ B⇩1 = {} ∧
B⇩0 ≠ {} ∧ (∀j ∈ B⇩1. (∀x<t. ∀y<t. L x j = L y
j)) ∧ (∀j ∈ B⇩0. (∀s<t. L s j = s))"
proof -
define B0 where "B0 = {..<n}"
define B1 where "B1 = ({}::nat set)"
have "B0 ∪ B1 = {..<n}" unfolding B0_def B1_def by simp
moreover have "B0 ∩ B1 = {}" unfolding B0_def B1_def by simp
moreover have "B0 ≠ {}" using assms unfolding B0_def is_line_def by auto
moreover have "(∀j ∈ B1. (∀x<t. ∀y<t. L x j = L y j))" unfolding B1_def by simp
moreover have "(∀j ∈ B0. (∀s<t. L s j = s))" using assms(1, 2) cube1_alt_def
unfolding B0_def is_line_def by auto
ultimately show ?thesis using that by simp
qed
text ‹The next two lemmas are used to simplify proofs by enabling us to use the resulting
facts directly. This avoids having to unfold the definition of \<^const>‹is_line› each
time.›
lemma line_points_in_cube:
assumes "is_line L n t"
and "s < t"
shows "L s ∈ cube n t"
using assms unfolding cube_def is_line_def
by auto
lemma line_points_in_cube_unfolded:
assumes "is_line L n t"
and "s < t"
and "j < n"
shows "L s j ∈ {..<t}"
using assms line_points_in_cube unfolding cube_def by blast
text ‹The incrementation of all elements of a set is defined in the following using the variables:
\begin{tabular}{llp{8cm}}
$n$:& \<^typ>‹nat›& increment size\\
$S$:& \<^typ>‹nat set›& set\\
\end{tabular}›
definition set_incr :: "nat ⇒ nat set ⇒ nat set"
where
"set_incr n S ≡ (λa. a + n) ` S"
lemma set_incr_disjnt:
assumes "disjnt A B"
shows "disjnt (set_incr n A) (set_incr n B)"
using assms unfolding disjnt_def set_incr_def by force
lemma set_incr_disjoint_family:
assumes "disjoint_family_on B {..k}"
shows " disjoint_family_on (λi. set_incr n (B i)) {..k}"
using assms set_incr_disjnt unfolding disjoint_family_on_def by (meson disjnt_def)
lemma set_incr_altdef: "set_incr n S = (+) n ` S"
by (auto simp: set_incr_def)
lemma set_incr_image:
assumes "(⋃i∈{..k}. B i) = {..<n}"
shows "(⋃i∈{..k}. set_incr m (B i)) = {m..<m+n}"
using assms by (simp add: set_incr_altdef add.commute flip: image_UN atLeast0LessThan)
text ‹Each tuple of dimension $k+1$ can be split into a tuple of dimension $1$ (the first
entry) and a tuple of dimension $k$ (the remaining entries).›
lemma split_cube:
assumes "x ∈ cube (k+1) t"
shows "(λy ∈ {..<1}. x y) ∈ cube 1 t"
and "(λy ∈ {..<k}. x (y + 1)) ∈ cube k t"
using assms unfolding cube_def by auto
subsection ‹Subspaces›
text ‹The property of being a $k$-dimensional subspace of $C^n_t$ is defined in the following using the variables:
\begin{tabular}{llp{8cm}}
$S$:& \<^typ>‹(nat ⇒ nat) ⇒ (nat ⇒ nat)›& the subspace\\
$k$:& \<^typ>‹nat›& the dimension of the subspace\\
$n$:& \<^typ>‹nat›& the dimension of the cube\\
$t$:& \<^typ>‹nat›& the size of the cube's base
\end{tabular}›
definition is_subspace
where "is_subspace S k n t ≡ (∃B f. disjoint_family_on B {..k} ∧ ⋃(B `
{..k}) = {..<n} ∧ ({} ∉ B ` {..<k}) ∧ f ∈ (B k) →⇩E {..<t}
∧ S ∈ (cube k t) →⇩E (cube n t) ∧ (∀y ∈ cube k t.
(∀i ∈ B k. S y i = f i) ∧ (∀j<k. ∀i ∈ B j. (S y) i = y j)))"
text ‹A $k$-dimensional subspace of $C^n_t$ can be thought of as an embedding of the $C^k_t$
into $C^n_t$, akin to how a $k$-dimensional vector subspace of $\mathbf{R}^n$ may be thought of as
an embedding of $\mathbf{R}^k$ into $\mathbf{R}^n$.›
lemma subspace_inj_on_cube:
assumes "is_subspace S k n t"
shows "inj_on S (cube k t)"
proof
fix x y
assume a: "x ∈ cube k t" "y ∈ cube k t" "S x = S y"
from assms obtain B f where Bf_props: "disjoint_family_on B {..k} ∧ ⋃(B ` {..k}) =
{..<n} ∧ ({} ∉ B ` {..<k}) ∧ f ∈ (B k) →⇩E {..<t} ∧
S ∈ (cube k t) →⇩E (cube n t) ∧ (∀y ∈ cube k t.
(∀i ∈ B k. S y i = f i) ∧ (∀j<k. ∀i ∈ B j. (S y) i = y j))"
unfolding is_subspace_def by auto
have "∀i<k. x i = y i"
proof (intro allI impI)
fix j assume "j < k"
then have "B j ≠ {}" using Bf_props by auto
then obtain i where i_prop: "i ∈ B j" by blast
then have "y j = S y i" using Bf_props a(2) ‹j < k› by auto
also have " ... = S x i" using a by simp
also have " ... = x j" using Bf_props a(1) ‹j < k› i_prop by blast
finally show "x j = y j" by simp
qed
then show "x = y" using a(1,2) unfolding cube_def by (meson PiE_ext lessThan_iff)
qed
text ‹The following is required to handle base cases in the key lemmas.›
lemma dim0_subspace_ex:
assumes "t > 0"
shows "∃S. is_subspace S 0 n t"
proof-
define B where "B ≡ (λx::nat. undefined)(0:={..<n})"
have "{..<t} ≠ {}" using assms by auto
then have "∃f. f ∈ (B 0) →⇩E {..<t}"
by (meson PiE_eq_empty_iff all_not_in_conv)
then obtain f where f_prop: "f ∈ (B 0) →⇩E {..<t}" by blast
define S where "S ≡ (λx::(nat ⇒ nat). undefined)((λx. undefined):=f)"
have "disjoint_family_on B {..0}" unfolding disjoint_family_on_def by simp
moreover have "⋃(B ` {..0}) = {..<n}" unfolding B_def by simp
moreover have "({} ∉ B ` {..<0})" by simp
moreover have "S ∈ (cube 0 t) →⇩E (cube n t)"
using f_prop PiE_I unfolding B_def cube_def S_def by auto
moreover have "(∀y ∈ cube 0 t. (∀i ∈ B 0. S y i = f i) ∧
(∀j<0. ∀i ∈ B j. (S y) i = y j))" unfolding cube_def S_def by force
ultimately have "is_subspace S 0 n t" using f_prop unfolding is_subspace_def by blast
then show "∃S. is_subspace S 0 n t" by auto
qed
subsection ‹Equivalence classes›
text ‹Defining the equivalence classes of \<^term>‹cube n (t + 1)›:
‹{classes n t 0, …, classes n t n}››
definition classes
where "classes n t ≡ (λi. {x . x ∈ (cube n (t + 1)) ∧ (∀u ∈
{(n-i)..<n}. x u = t) ∧ t ∉ x ` {..<(n - i)}})"
lemma classes_subset_cube: "classes n t i ⊆ cube n (t+1)" unfolding classes_def by blast
definition layered_subspace
where "layered_subspace S k n t r χ ≡ (is_subspace S k n (t + 1) ∧ (∀i
∈ {..k}. ∃c<r. ∀x ∈ classes k t i. χ (S x) = c)) ∧ χ ∈
cube n (t + 1) →⇩E {..<r}"
lemma layered_eq_classes:
assumes "layered_subspace S k n t r χ"
shows "∀i ∈ {..k}. ∀x ∈ classes k t i. ∀y ∈ classes k t i.
χ (S x) = χ (S y)"
proof (safe)
fix i x y
assume a: "i ≤ k" "x ∈ classes k t i" "y ∈ classes k t i"
then obtain c where "c < r ∧ χ (S x) = c ∧ χ (S y) = c" using assms unfolding
layered_subspace_def by fast
then show "χ (S x) = χ (S y)" by simp
qed
lemma dim0_layered_subspace_ex:
assumes "χ ∈ (cube n (t + 1)) →⇩E {..<r::nat}"
shows "∃S. layered_subspace S (0::nat) n t r χ"
proof-
obtain S where S_prop: "is_subspace S (0::nat) n (t+1)" using dim0_subspace_ex by auto
have "classes (0::nat) t 0 = cube 0 (t+1)" unfolding classes_def by simp
moreover have "(∀i ∈ {..0::nat}. ∃c<r. ∀x ∈ classes (0::nat) t i. χ (S x) = c)"
proof(safe)
fix i
have "∀x ∈ classes 0 t 0. χ (S x) = χ (S (λx. undefined))" using cube0_alt_def
using ‹classes 0 t 0 = cube 0 (t + 1)› by auto
moreover have "S (λx. undefined) ∈ cube n (t+1)" using S_prop cube0_alt_def
unfolding is_subspace_def by auto
moreover have "χ (S (λx. undefined)) < r" using assms calculation by auto
ultimately show "∃c<r. ∀x∈classes 0 t 0. χ (S x) = c" by auto
qed
ultimately have "layered_subspace S 0 n t r χ" using S_prop assms unfolding layered_subspace_def by blast
then show "∃S. layered_subspace S (0::nat) n t r χ" by auto
qed
lemma disjoint_family_onI [intro]:
assumes "⋀m n. m ∈ S ⟹ n ∈ S ⟹ m ≠ n
⟹ A m ∩ A n = {}"
shows "disjoint_family_on A S"
using assms by (auto simp: disjoint_family_on_def)
lemma fun_ex: "a ∈ A ⟹ b ∈ B ⟹ ∃f ∈ A
→⇩E B. f a = b"
proof-
assume assms: "a ∈ A" "b ∈ B"
then obtain g where g_def: "g ∈ A → B ∧ g a = b" by fast
then have "restrict g A ∈ A →⇩E B ∧ (restrict g A) a = b" using assms(1) by auto
then show ?thesis by blast
qed
lemma ex_bij_betw_nat_finite_2:
assumes "card A = n"
and "n > 0"
shows "∃f. bij_betw f A {..<n}"
using assms ex_bij_betw_finite_nat[of A] atLeast0LessThan card_ge_0_finite by auto
lemma one_dim_cube_eq_nat_set: "bij_betw (λf. f 0) (cube 1 k) {..<k}"
proof (unfold bij_betw_def)
have *: "(λf. f 0) ` cube 1 k = {..<k}"
proof(safe)
fix x f
assume "f ∈ cube 1 k"
then show "f 0 < k" unfolding cube_def by blast
next
fix x
assume "x < k"
then have "x ∈ {..<k}" by simp
moreover have "0 ∈ {..<1::nat}" by simp
ultimately have "∃y ∈ {..<1::nat} →⇩E {..<k}. y 0 = x" using
fun_ex[of "0" "{..<1::nat}" "x" "{..<k}"] by auto
then show "x ∈ (λf. f 0) ` cube 1 k" unfolding cube_def by blast
qed
moreover
{
have "card (cube 1 k) = k" using cube_card by (simp add: cube_def)
moreover have "card {..<k} = k" by simp
ultimately have "inj_on (λf. f 0) (cube 1 k)" using * eq_card_imp_inj_on[of "cube 1 k" "λf. f 0"]
by force
}
ultimately show "inj_on (λf. f 0) (cube 1 k) ∧ (λf. f 0) ` cube 1 k = {..<k}" by simp
qed
text ‹An alternative introduction rule for the $\exists!x$ quantifier, which means "there
exists exactly one $x$".›
lemma ex1I_alt: "(∃x. P x ∧ (∀y. P y ⟶ x = y)) ⟹ (∃!x. P x)"
by auto
lemma nat_set_eq_one_dim_cube: "bij_betw (λx. λy∈{..<1::nat}. x) {..<k::nat} (cube 1 k)"
proof (unfold bij_betw_def)
have *: "(λx. λy∈{..<1::nat}. x) ` {..<k} = cube 1 k"
proof (safe)
fix x y
assume "y < k"
then show "(λz∈{..<1}. y) ∈ cube 1 k" unfolding cube_def by simp
next
fix x
assume "x ∈ cube 1 k"
have "x = (λz. λy∈{..<1::nat}. z) (x 0::nat)"
proof
fix j
consider "j ∈ {..<1}" | "j ∉ {..<1::nat}" by linarith
then show "x j = (λz. λy∈{..<1::nat}. z) (x 0::nat) j" using ‹x
∈ cube 1 k› unfolding cube_def by auto
qed
moreover have "x 0 ∈ {..<k}" using ‹x ∈ cube 1 k› by (auto simp add: cube_def)
ultimately show "x ∈ (λz. λy∈{..<1}. z) ` {..<k}" by blast
qed
moreover
{
have "card (cube 1 k) = k" using cube_card by (simp add: cube_def)
moreover have "card {..<k} = k" by simp
ultimately have "inj_on (λx. λy∈{..<1::nat}. x) {..<k}" using *
eq_card_imp_inj_on[of "{..<k}" "λx. λy∈{..<1::nat}. x"] by force
}
ultimately show "inj_on (λx. λy∈{..<1::nat}. x) {..<k} ∧ (λx.
λy∈{..<1::nat}. x) ` {..<k} = cube 1 k" by blast
qed
text ‹A bijection $f$ between domains $A_1$ and $A_2$ creates a correspondence between
functions in $A_1 \rightarrow B$ and $A_2 \rightarrow B$.›
lemma bij_domain_PiE:
assumes "bij_betw f A1 A2"
and "g ∈ A2 →⇩E B"
shows "(restrict (g ∘ f) A1) ∈ A1 →⇩E B"
using bij_betwE assms by fastforce
text ‹The following three lemmas relate lines to $1$-dimensional subspaces (in the natural
way). This is a direct consequence of the elimination rule ‹is_line_elim› introduced
above.›
lemma line_is_dim1_subspace_t_1:
assumes "n > 0"
and "is_line L n 1"
shows "is_subspace (restrict (λy. L (y 0)) (cube 1 1)) 1 n 1"
proof -
obtain B⇩0 B⇩1 where B_props: "B⇩0 ∪ B⇩1 = {..<n} ∧ B⇩0
∩ B⇩1 = {} ∧ B⇩0 ≠ {} ∧ (∀j ∈ B⇩1.
(∀x<1. ∀y<1. L x j = L y j)) ∧ (∀j ∈ B⇩0. (∀s<1. L
s j = s))" using is_line_elim_t_1[of L n 1] assms by auto
define B where "B ≡ (λi::nat. {}::nat set)(0:=B⇩0, 1:=B⇩1)"
define f where "f ≡ (λi ∈ B 1. L 0 i)"
have *: "L 0 ∈ {..<n} →⇩E {..<1}" using assms(2) unfolding cube_def is_line_def by auto
have "disjoint_family_on B {..1}" unfolding B_def using B_props
by (simp add: Int_commute disjoint_family_onI)
moreover have "⋃ (B ` {..1}) = {..<n}" unfolding B_def using B_props by auto
moreover have "{} ∉ B ` {..<1}" unfolding B_def using B_props by auto
moreover have " f ∈ B 1 →⇩E {..<1}" using * calculation(2) unfolding f_def by auto
moreover have "(restrict (λy. L (y 0)) (cube 1 1)) ∈ cube 1 1 →⇩E cube n 1"
using assms(2) cube1_alt_def unfolding is_line_def by auto
moreover have "(∀y∈cube 1 1. (∀i∈B 1. (restrict (λy. L (y 0)) (cube 1 1)) y i = f i)
∧ (∀j<1. ∀i∈B j. (restrict (λy. L (y 0)) (cube 1 1)) y i = y j))"
using cube1_alt_def B_props * unfolding B_def f_def by auto
ultimately show ?thesis unfolding is_subspace_def by blast
qed
lemma line_is_dim1_subspace_t_ge_1:
assumes "n > 0"
and "t > 1"
and "is_line L n t"
shows "is_subspace (restrict (λy. L (y 0)) (cube 1 t)) 1 n t"
proof -
let ?B1 = "{i::nat . i < n ∧ (∀x<t. ∀y<t. L x i = L y i)}"
let ?B0 = "{i::nat . i < n ∧ (∀s < t. L s i = s)}"
define B where "B ≡ (λi::nat. {}::nat set)(0:=?B0, 1:=?B1)"
let ?L = "(λy ∈ cube 1 t. L (y 0))"
have "?B0 ≠ {}" using assms(3) unfolding is_line_def by simp
have L1: "?B0 ∪ ?B1 = {..<n}" using assms(3) unfolding is_line_def by auto
{
have "(∀s < t. L s i = s) ⟶ ¬(∀x<t. ∀y<t. L x i =
L y i)" if "i < n" for i using assms(2) less_trans by auto
then have *:"i ∉ ?B0" if "i ∈ ?B1" for i using that by blast
}
moreover
{
have "(∀x<t. ∀y<t. L x i = L y i) ⟶ ¬(∀s < t. L s i = s)"
if "i < n" for i using that calculation by blast
then have **: "∀i ∈ ?B0. i ∉ ?B1"
by blast
}
ultimately have L2: "?B0 ∩ ?B1 = {}" by blast
let ?f = "(λi. if i ∈ B 1 then L 0 i else undefined)"
{
have "{..1::nat} = {0, 1}" by auto
then have "⋃(B ` {..1::nat}) = B 0 ∪ B 1" by simp
then have "⋃(B ` {..1::nat}) = ?B0 ∪ ?B1" unfolding B_def by simp
then have A1: "disjoint_family_on B {..1::nat}" using L2
by (simp add: B_def Int_commute disjoint_family_onI)
}
moreover
{
have "⋃(B ` {..1::nat}) = B 0 ∪ B 1" unfolding B_def by auto
then have "⋃(B ` {..1::nat}) = {..<n}" using L1 unfolding B_def by simp
}
moreover
{
have "∀i ∈ {..<1::nat}. B i ≠ {}"
using ‹{i. i < n ∧ (∀s<t. L s i = s)} ≠ {}› fun_upd_same lessThan_iff less_one
unfolding B_def by auto
then have "{} ∉ B ` {..<1::nat}" by blast
}
moreover
{
have "?f ∈ (B 1) →⇩E {..<t}"
proof
fix i
assume asm: "i ∈ (B 1)"
have "L a b ∈ {..<t}" if "a < t" and "b < n" for a b using assms(3) that unfolding is_line_def cube_def by auto
then have "L 0 i ∈ {..<t}" using assms(2) asm calculation(2) by blast
then show "?f i ∈ {..<t}" using asm by presburger
qed (auto)
}
moreover
{
have "L ∈ {..<t} →⇩E (cube n t)" using assms(3) by (simp add: is_line_def)
then have "?L ∈ (cube 1 t) →⇩E (cube n t)"
using bij_domain_PiE[of "(λf. f 0)" "(cube 1 t)" "{..<t}" "L" "cube n t"] one_dim_cube_eq_nat_set[of "t"]
by auto
}
moreover
{
have "∀y ∈ cube 1 t. (∀i ∈ B 1. ?L y i = ?f i) ∧ (∀j < 1.
∀i ∈ B j. (?L y) i = y j)"
proof
fix y
assume "y ∈ cube 1 t"
then have "y 0 ∈ {..<t}" unfolding cube_def by blast
have "(∀i ∈ B 1. ?L y i = ?f i)"
proof
fix i
assume "i ∈ B 1"
then have "?f i = L 0 i"
by meson
moreover have "?L y i = L (y 0) i" using ‹y ∈ cube 1 t› by simp
moreover have "L (y 0) i = L 0 i"
proof -
have "i ∈ ?B1" using ‹i ∈ B 1› unfolding B_def fun_upd_def by presburger
then have "(∀x<t. ∀y<t. L x i = L y i)" by blast
then show "L (y 0) i = L 0 i" using ‹y 0 ∈ {..<t}› by blast
qed
ultimately show "?L y i = ?f i" by simp
qed
moreover have "(?L y) i = y j" if "j < 1" and "i ∈ B j" for i j
proof-
have "i ∈ B 0" using that by blast
then have "i ∈ ?B0" unfolding B_def by auto
then have "(∀s < t. L s i = s)" by blast
moreover have "y 0 < t" using ‹y ∈ cube 1 t› unfolding cube_def by auto
ultimately have "L (y 0) i = y 0" by simp
then show "?L y i = y j" using that using ‹y ∈ cube 1 t› by force
qed
ultimately show "(∀i ∈ B 1. ?L y i = ?f i) ∧ (∀j < 1. ∀i
∈ B j. (?L y) i = y j)"
by blast
qed
}
ultimately show "is_subspace ?L 1 n t" unfolding is_subspace_def by blast
qed
lemma line_is_dim1_subspace:
assumes "n > 0"
and "t > 0"
and "is_line L n t"
shows "is_subspace (restrict (λy. L (y 0)) (cube 1 t)) 1 n t"
using line_is_dim1_subspace_t_1[of n L] line_is_dim1_subspace_t_ge_1[of n t L] assms not_less_iff_gr_or_eq by blast
text ‹The key property of the existence of a minimal dimension $N$, such that for any
$r$-colouring in $C^{N'}_t$ (for $N' \geq N$) there exists a monochromatic line is defined in the
following using the variables:
\begin{tabular}{llp{8cm}}
$r$:& \<^typ>‹nat›& the number of colours\\
$t$:& \<^typ>‹nat›& the size of of the base
\end{tabular}›
definition hj
where "hj r t ≡ (∃N>0. ∀N' ≥ N. ∀χ. χ ∈ (cube N'
t) →⇩E {..<r::nat} ⟶ (∃L. ∃c<r. is_line L N' t
∧ (∀y ∈ L ` {..<t}. χ y = c)))"
text ‹The key property of the existence of a minimal dimension $N$, such that for any
$r$-colouring in $C^{N'}_t$ (for $N' \geq N$) there exists a layered subspace of dimension $k$ is
defined in the following using the variables:
\begin{tabular}{llp{8cm}}
$r$:& \<^typ>‹nat›& the number of colours\\
$t$:& \<^typ>‹nat›& the size of of the base\\
$k$:& \<^typ>‹nat›& the dimension of the subspace
\end{tabular}›
definition lhj
where "lhj r t k ≡ (∃N > 0. ∀N' ≥ N. ∀χ. χ ∈
(cube N' (t + 1)) →⇩E {..<r::nat} ⟶ (∃S.
layered_subspace S k N' t r χ))"
text ‹We state some useful facts about $1$-dimensional subspaces.›
lemma dim1_subspace_elims:
assumes "disjoint_family_on B {..1::nat}" and "⋃(B ` {..1::nat}) = {..<n}" and "({}
∉ B ` {..<1::nat})" and "f ∈ (B 1) →⇩E {..<t}" and "S ∈ (cube 1
t) →⇩E (cube n t)" and "(∀y ∈ cube 1 t. (∀i ∈ B 1. S y i
= f i) ∧ (∀j<1. ∀i ∈ B j. (S y) i = y j))"
shows "B 0 ∪ B 1 = {..<n}"
and "B 0 ∩ B 1 = {}"
and "(∀y ∈ cube 1 t. (∀i ∈ B 1. S y i = f i) ∧ (∀i ∈ B 0. (S y) i = y 0))"
and "B 0 ≠ {}"
proof -
have "{..1} = {0::nat, 1}" by auto
then show "B 0 ∪ B 1 = {..<n}" using assms(2) by simp
next
show "B 0 ∩ B 1 = {}" using assms(1) unfolding disjoint_family_on_def by simp
next
show "(∀y ∈ cube 1 t. (∀i ∈ B 1. S y i = f i) ∧ (∀i ∈ B 0. (S y) i = y 0))"
using assms(6) by simp
next
show "B 0 ≠ {}" using assms(3) by auto
qed
text ‹We state some properties of cubes.›
lemma cube_props:
assumes "s < t"
shows "∃p ∈ cube 1 t. p 0 = s"
and "(SOME p. p ∈ cube 1 t ∧ p 0 = s) 0 = s"
and "(λs∈{..<t}. S (SOME p. p∈cube 1 t ∧ p 0 = s)) s =
(λs∈{..<t}. S (SOME p. p∈cube 1 t ∧ p 0 = s)) ((SOME p. p ∈ cube 1 t
∧ p 0 = s) 0)"
and "(SOME p. p ∈ cube 1 t ∧ p 0 = s) ∈ cube 1 t"
proof -
show 1: "∃p ∈ cube 1 t. p 0 = s" using assms unfolding cube_def by (simp add: fun_ex)
show 2: "(SOME p. p ∈ cube 1 t ∧ p 0 = s) 0 = s" using assms 1 someI_ex[of "λx. x
∈ cube 1 t ∧ x 0 = s"] by blast
show 3: "(λs∈{..<t}. S (SOME p. p∈cube 1 t ∧ p 0 = s)) s =
(λs∈{..<t}. S (SOME p. p∈cube 1 t ∧ p 0 = s)) ((SOME p. p ∈ cube 1 t
∧ p 0 = s) 0)" using 2 by simp
show 4: "(SOME p. p ∈ cube 1 t ∧ p 0 = s) ∈ cube 1 t" using 1 someI_ex[of
"λp. p ∈ cube 1 t ∧ p 0 = s"] assms by blast
qed
text ‹The following lemma relates $1$-dimensional subspaces to lines, thus establishing a
bidirectional correspondence between the two together with
‹line_is_dim1_subspace›.›
lemma dim1_subspace_is_line:
assumes "t > 0"
and "is_subspace S 1 n t"
shows "is_line (λs∈{..<t}. S (SOME p. p∈cube 1 t ∧ p 0 = s)) n t"
proof-
define L where "L ≡ (λs∈{..<t}. S (SOME p. p∈cube 1 t ∧ p 0 = s))"
have "{..1} = {0::nat, 1}" by auto
obtain B f where Bf_props: "disjoint_family_on B {..1::nat} ∧ ⋃(B ` {..1::nat}) =
{..<n} ∧ ({} ∉ B ` {..<1::nat}) ∧ f ∈ (B 1) →⇩E {..<t}
∧ S ∈ (cube 1 t) →⇩E (cube n t) ∧ (∀y ∈ cube 1 t.
(∀i ∈ B 1. S y i = f i) ∧ (∀j<1. ∀i ∈ B j. (S y) i = y j))"
using assms(2) unfolding is_subspace_def by auto
then have 1: "B 0 ∪ B 1 = {..<n} ∧ B 0 ∩ B 1 = {}" using dim1_subspace_elims(1,
2)[of B n f t S] by simp
have "L ∈ {..<t} →⇩E cube n t"
proof
fix s assume a: "s ∈ {..<t}"
then have "L s = S (SOME p. p∈cube 1 t ∧ p 0 = s)" unfolding L_def by simp
moreover have "(SOME p. p∈cube 1 t ∧ p 0 = s) ∈ cube 1 t" using cube_props(1) a
someI_ex[of "λp. p ∈ cube 1 t ∧ p 0 = s"] by blast
moreover have "S (SOME p. p∈cube 1 t ∧ p 0 = s) ∈ cube n t"
using assms(2) calculation(2) is_subspace_def by auto
ultimately show "L s ∈ cube n t" by simp
next
fix s assume a: "s ∉ {..<t}"
then show "L s = undefined" unfolding L_def by simp
qed
moreover have "(∀x<t. ∀y<t. L x j = L y j) ∨ (∀s<t. L s j = s)" if "j < n" for j
proof-
consider "j ∈ B 0" | "j ∈ B 1" using ‹j < n› 1 by blast
then show "(∀x<t. ∀y<t. L x j = L y j) ∨ (∀s<t. L s j = s)"
proof (cases)
case 1
have "L s j = s" if "s < t" for s
proof-
have "∀y ∈ cube 1 t. (S y) j = y 0" using Bf_props 1 by simp
then show "L s j = s" using that cube_props(2,4) unfolding L_def by auto
qed
then show ?thesis by blast
next
case 2
have "L x j = L y j" if "x < t" and "y < t" for x y
proof-
have *: "S y j = f j" if "y ∈ cube 1 t" for y using 2 that Bf_props by simp
then have "L y j = f j" using that(2) cube_props(2,4) lessThan_iff restrict_apply unfolding L_def by fastforce
moreover from * have "L x j = f j" using that(1) cube_props(2,4) lessThan_iff restrict_apply unfolding L_def
by fastforce
ultimately show "L x j = L y j" by simp
qed
then show ?thesis by blast
qed
qed
moreover have "(∃j<n. ∀s<t. (L s j = s))"
proof -
obtain j where j_prop: "j ∈ B 0 ∧ j < n" using Bf_props by blast
then have "(S y) j = y 0" if "y ∈ cube 1 t" for y using that Bf_props by auto
then have "L s j = s" if "s < t" for s using that cube_props(2,4) unfolding L_def by auto
then show "∃j<n. ∀s<t. (L s j = s)" using j_prop by blast
qed
ultimately show "is_line (λs∈{..<t}. S (SOME p. p∈cube 1 t ∧ p 0 = s)) n t"
unfolding L_def is_line_def by auto
qed
lemma bij_unique_inv:
assumes "bij_betw f A B"
and "x ∈ B"
shows "∃!y ∈ A. (the_inv_into A f) x = y"
using assms unfolding bij_betw_def inj_on_def the_inv_into_def
by blast
lemma inv_into_cube_props:
assumes "s < t"
shows "the_inv_into (cube 1 t) (λf. f 0) s ∈ cube 1 t"
and "the_inv_into (cube 1 t) (λf. f 0) s 0 = s"
using assms bij_unique_inv one_dim_cube_eq_nat_set f_the_inv_into_f_bij_betw
by fastforce+
lemma some_inv_into:
assumes "s < t"
shows "(SOME p. p∈cube 1 t ∧ p 0 = s) = (the_inv_into (cube 1 t) (λf. f 0) s)"
using inv_into_cube_props[of s t] one_dim_cube_eq_nat_set[of t] assms unfolding bij_betw_def inj_on_def by auto
lemma some_inv_into_2:
assumes "s < t"
shows "(SOME p. p∈cube 1 (t+1) ∧ p 0 = s) = (the_inv_into (cube 1 t) (λf. f 0) s)"
proof-
have *: "(SOME p. p∈cube 1 (t+1) ∧ p 0 = s) ∈ cube 1 (t+1)" using cube_props assms by simp
then have "(SOME p. p∈cube 1 (t+1) ∧ p 0 = s) 0 = s" using cube_props assms by simp
moreover
{
have "(SOME p. p∈cube 1 (t+1) ∧ p 0 = s) ` {..<1} ⊆ {..<t}" using calculation assms by force
then have "(SOME p. p∈cube 1 (t+1) ∧ p 0 = s) ∈ cube 1 t" using * unfolding cube_def by auto
}
moreover have "inj_on (λf. f 0) (cube 1 t)" using one_dim_cube_eq_nat_set[of t]
unfolding bij_betw_def inj_on_def by auto
ultimately show "(SOME p. p∈cube 1 (t+1) ∧ p 0 = s) = (the_inv_into (cube 1 t) (λf. f 0) s)"
using the_inv_into_f_eq [of "λf. f 0" "cube 1 t" "(SOME p. p∈cube 1 (t+1) ∧ p 0 = s)" s] by auto
qed
lemma dim1_layered_subspace_as_line:
assumes "t > 0"
and "layered_subspace S 1 n t r χ"
shows "∃c1 c2. c1<r ∧ c2<r ∧ (∀s<t. χ (S (SOME p. p∈cube 1
(t+1) ∧ p 0 = s)) = c1) ∧ χ (S (SOME p. p∈cube 1 (t+1) ∧ p 0 = t)) = c2"
proof -
have "x u < t" if "x ∈ classes 1 t 0" and "u < 1" for x u
proof -
have "x ∈ cube 1 (t+1)" using that unfolding classes_def by blast
then have "x u ∈ {..<t+1}" using that unfolding cube_def by blast
then have "x u ∈ {..<t}" using that
using that less_Suc_eq unfolding classes_def by auto
then show "x u < t" by simp
qed
then have "classes 1 t 0 ⊆ cube 1 t" unfolding cube_def classes_def by auto
moreover have "cube 1 t ⊆ classes 1 t 0" using cube_subset[of 1 t] unfolding cube_def classes_def by auto
ultimately have X: "classes 1 t 0 = cube 1 t" by blast
obtain c1 where c1_prop: "c1 < r ∧ (∀x∈classes 1 t 0. χ (S x) = c1)" using assms(2)
unfolding layered_subspace_def by blast
then have "(χ (S x) = c1)" if "x ∈ cube 1 t" for x using X that by blast
then have "χ (S (the_inv_into (cube 1 t) (λf. f 0) s)) = c1" if "s < t" for s
using one_dim_cube_eq_nat_set[of t] by (meson that bij_betwE bij_betw_the_inv_into lessThan_iff)
then have K1: "χ (S (SOME p. p∈cube 1 (t+1) ∧ p 0 = s)) = c1" if "s < t" for s
using that some_inv_into_2 by simp
have *: "∃c<r. ∀x ∈ classes 1 t 1. χ (S x) = c"
using assms(2) unfolding layered_subspace_def by blast
have "x 0 = t" if "x ∈ classes 1 t 1" for x using that unfolding classes_def by simp
moreover have "∃!x ∈ cube 1 (t+1). x 0 = t" using one_dim_cube_eq_nat_set[of "t+1"]
unfolding bij_betw_def inj_on_def using inv_into_cube_props(1) inv_into_cube_props(2) by force
moreover have **: "∃!x. x ∈ classes 1 t 1" unfolding classes_def using calculation(2) by simp
ultimately have "the_inv_into (cube 1 (t+1)) (λf. f 0) t ∈ classes 1 t 1"
using inv_into_cube_props[of t "t+1"] unfolding classes_def by simp
then have "∃c2. c2 < r ∧ χ (S (the_inv_into (cube 1 (t+1)) (λf. f 0) t)) = c2"
using * ** by blast
then have K2: "∃c2. c2 < r ∧ χ (S (SOME p. p∈cube 1 (t+1) ∧ p 0 = t)) = c2"
using some_inv_into by simp
from K1 K2 show ?thesis
using c1_prop by blast
qed
lemma dim1_layered_subspace_mono_line:
assumes "t > 0"
and "layered_subspace S 1 n t r χ"
shows "∀s<t. ∀l<t. χ (S (SOME p. p∈cube 1 (t+1) ∧ p 0 = s)) =
χ (S (SOME p. p∈cube 1 (t+1) ∧ p 0 = l)) ∧ χ (S (SOME p. p∈cube 1
(t+1) ∧ p 0 = s)) < r"
using dim1_layered_subspace_as_line[of t S n r χ] assms by auto
definition join :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ nat
⇒ nat ⇒ (nat ⇒ 'a)"
where
"join f g n m ≡ (λx. if x ∈ {..<n} then f x else (if x ∈ {n..<n+m} then g
(x - n) else undefined))"
lemma join_cubes:
assumes "f ∈ cube n (t+1)"
and "g ∈ cube m (t+1)"
shows "join f g n m ∈ cube (n+m) (t+1)"
proof (unfold cube_def; intro PiE_I)
fix i
assume "i ∈ {..<n+m}"
then consider "i < n" | "i ≥ n ∧ i < n+m" by fastforce
then show "join f g n m i ∈ {..<t + 1}"
proof (cases)
case 1
then have "join f g n m i = f i" unfolding join_def by simp
moreover have "f i ∈ {..<t+1}" using assms(1) 1 unfolding cube_def by blast
ultimately show ?thesis by simp
next
case 2
then have "join f g n m i = g (i - n)" unfolding join_def by simp
moreover have "i - n ∈ {..<m}" using 2 by auto
moreover have "g (i - n) ∈ {..<t+1}" using calculation(2) assms(2) unfolding cube_def by blast
ultimately show ?thesis by simp
qed
next
fix i
assume "i ∉ {..<n+m}"
then show "join f g n m i = undefined" unfolding join_def by simp
qed
lemma subspace_elems_embed:
assumes "is_subspace S k n t"
shows "S ` (cube k t) ⊆ cube n t"
using assms unfolding cube_def is_subspace_def by blast
section ‹Core proofs›
text‹The numbering of the theorems has been borrowed from the textbook~\<^cite>‹"thebook"›.›
subsection ‹Theorem 4›
subsubsection ‹Base case of Theorem 4›
lemma hj_imp_lhj_base:
fixes r t
assumes "t > 0"
and "⋀r'. hj r' t"
shows "lhj r t 1"
proof-
from assms(2) obtain N where N_def: "N > 0 ∧ (∀N' ≥ N. ∀χ. χ
∈ (cube N' t) →⇩E {..<r::nat} ⟶ (∃L. ∃c<r.
is_line L N' t ∧ (∀y ∈ L ` {..<t}. χ y = c)))" unfolding hj_def by blast
have "(∃S. is_subspace S 1 N' (t + 1) ∧ (∀i ∈ {..1}. ∃c < r.
(∀x ∈ classes 1 t i. χ (S x) = c)))" if asm: "N' ≥ N" "χ ∈ (cube N'
(t + 1)) →⇩E {..<r::nat}" for N' χ
proof-
have N'_props: "N' > 0 ∧ (∀χ. χ ∈ (cube N' t) →⇩E
{..<r::nat} ⟶ (∃L. ∃c<r. is_line L N' t ∧ (∀y ∈
L ` {..<t}. χ y = c)))" using asm N_def by simp
let ?chi_t = "λx ∈ cube N' t. χ x"
have "?chi_t ∈ cube N' t →⇩E {..<r::nat}" using cube_subset asm by auto
then obtain L where L_def: "is_line L N' t ∧ (∃c<r. (∀y ∈ L ` {..<t}. ?chi_t y = c))"
using N'_props by blast
have "is_subspace (restrict (λy. L (y 0)) (cube 1 t)) 1 N' t" using line_is_dim1_subspace N'_props L_def
using assms(1) by auto
then obtain B f where Bf_defs: "disjoint_family_on B {..1} ∧ ⋃(B ` {..1}) = {..<N'}
∧ ({} ∉ B ` {..<1}) ∧ f ∈ (B 1) →⇩E {..<t} ∧
(restrict (λy. L (y 0)) (cube 1 t)) ∈ (cube 1 t) →⇩E (cube N' t)
∧ (∀y ∈ cube 1 t. (∀i ∈ B 1. (restrict (λy. L (y 0)) (cube
1 t)) y i = f i) ∧ (∀j<1. ∀i ∈ B j. ((restrict (λy. L (y 0))
(cube 1 t)) y) i = y j))" unfolding is_subspace_def by auto
have "{..1::nat} = {0, 1}" by auto
then have B_props: "B 0 ∪ B 1 = {..<N'} ∧ (B 0 ∩ B 1 = {})"
using Bf_defs unfolding disjoint_family_on_def by auto
define L' where "L' ≡ L(t:=(λj. if j ∈ B 1 then L (t - 1) j else (if j ∈
B 0 then t else undefined)))"
text ‹‹S1› is the corresponding $1$-dimensional subspace of ‹L'›.›
define S1 where "S1 ≡ restrict (λy. L' (y (0::nat))) (cube 1 (t+1))"
have line_prop: "is_line L' N' (t + 1)"
proof-
have A1: "L' ∈ {..<t+1} →⇩E cube N' (t + 1)"
proof
fix x
assume asm: "x ∈ {..<t + 1}"
then show "L' x ∈ cube N' (t + 1)"
proof (cases "x < t")
case True
then have "L' x = L x" by (simp add: L'_def)
then have "L' x ∈ cube N' t" using L_def True unfolding is_line_def by auto
then show "L' x ∈ cube N' (t + 1)" using cube_subset by blast
next
case False
then have "x = t" using asm by simp
show "L' x ∈ cube N' (t + 1)"
proof(unfold cube_def, intro PiE_I)
fix j
assume "j ∈ {..<N'}"
have "j ∈ B 1 ∨ j ∈ B 0 ∨ j ∉ (B 0 ∪ B 1)" by blast
then show "L' x j ∈ {..<t + 1}"
proof (elim disjE)
assume "j ∈ B 1"
then have "L' x j = L (t - 1) j"
by (simp add: ‹x = t› L'_def)
have "L (t - 1) ∈ cube N' t" using line_points_in_cube L_def
by (meson assms(1) diff_less less_numeral_extra(1))
then have "L (t - 1) j < t" using ‹j ∈ {..<N'}› unfolding cube_def by auto
then show "L' x j ∈ {..<t + 1}" using ‹L' x j = L (t - 1) j› by simp
next
assume "j ∈ B 0"
then have "j ∉ B 1" using Bf_defs unfolding disjoint_family_on_def by auto
then have "L' x j = t" by (simp add: ‹j ∈ B 0› ‹x = t› L'_def)
then show "L' x j ∈ {..<t + 1}" by simp
next
assume a: "j ∉ (B 0 ∪ B 1)"
have "{..1::nat} = {0, 1}" by auto
then have "B 0 ∪ B 1 = (⋃(B ` {..1::nat}))" by simp
then have "B 0 ∪ B 1 = {..<N'}" using Bf_defs unfolding partition_on_def by simp
then have "¬(j ∈ {..<N'})" using a by simp
then have False using ‹j ∈ {..<N'}› by simp
then show ?thesis by simp
qed
next
fix j
assume "j ∉ {..<N'}"
then have "j ∉ (B 0) ∧ j ∉ B 1" using Bf_defs unfolding partition_on_def by auto
then show "L' x j = undefined" using ‹x = t› by (simp add: L'_def)
qed
qed
next
fix x
assume asm: "x ∉ {..<t+1}"
then have "x ∉ {..<t} ∧ x ≠ t" by simp
then show "L' x = undefined" using L_def unfolding L'_def is_line_def by auto
qed
have A2: "(∃j<N'. (∀s < (t + 1). L' s j = s))"
proof (cases "t = 1")
case True
obtain j where j_prop: "j ∈ B 0 ∧ j < N'" using Bf_defs by blast
then have "L' s j = L s j" if "s < t" for s using that by (auto simp: L'_def)
moreover have "L s j = 0" if "s < t" for s using that True L_def j_prop line_points_in_cube_unfolded[of L N' t]
by simp
moreover have "L' s j = s" if "s < t" for s using True calculation that by simp
moreover have "L' t j = t" using j_prop B_props by (auto simp: L'_def)
ultimately show ?thesis unfolding L'_def using j_prop by auto
next
case False
then show ?thesis
proof-
have "(∃j<N'. (∀s < t. L' s j = s))" using L_def unfolding is_line_def by (auto simp: L'_def)
then obtain j where j_def: "j < N' ∧ (∀s < t. L' s j = s)" by blast
have "j ∉ B 1"
proof
assume a:"j ∈ B 1"
then have "(restrict (λy. L (y 0)) (cube 1 t)) y j = f j" if "y ∈ cube 1 t" for y
using Bf_defs that by simp
then have "L (y 0) j = f j" if "y ∈ cube 1 t" for y using that by simp
moreover have "∃!i. i < t ∧ y 0 = i" if "y ∈ cube 1 t" for y
using that one_dim_cube_eq_nat_set[of "t"] unfolding bij_betw_def by blast
moreover have "∃!y. y ∈ cube 1 t ∧ y 0 = i" if "i < t" for i
proof (intro ex1I_alt)
define y where "y ≡ (λx::nat. λy∈{..<1::nat}. x)"
have "y i ∈ (cube 1 t)" using that unfolding cube_def y_def by simp
moreover have "y i 0 = i" unfolding y_def by simp
moreover have "z = y i" if "z ∈ cube 1 t" and "z 0 = i" for z
proof (rule ccontr)
assume "z ≠ y i"
then obtain l where l_prop: "z l ≠ y i l" by blast
consider "l ∈ {..<1::nat}" | "l ∉ {..<1::nat}" by blast
then show False
proof cases
case 1
then show ?thesis using l_prop that(2) unfolding y_def by auto
next
case 2
then have "z l = undefined" using that unfolding cube_def by blast
moreover have "y i l = undefined" unfolding y_def using 2 by auto
ultimately show ?thesis using l_prop by presburger
qed
qed
ultimately show "∃y. (y ∈ cube 1 t ∧ y 0 = i) ∧ (∀ya. ya
∈ cube 1 t ∧ ya 0 = i ⟶ y = ya)" by blast
qed
moreover have "L i j = f j" if "i < t" for i using that calculation by blast
moreover have "(∃j<N'. (∀s < t. L s j = s))" using
‹(∃j<N'. (∀s < t. L' s j = s))› by (auto simp: L'_def)
ultimately show False using False
by (metis (no_types, lifting) L'_def assms(1) fun_upd_apply j_def less_one nat_neq_iff)
qed
then have "j ∈ B 0" using ‹j ∉ B 1› j_def B_props by auto
then have "L' t j = t" using ‹j ∉ B 1› by (auto simp: L'_def)
then have "L' s j = s" if "s < t + 1" for s using j_def that by (auto simp: L'_def)
then show ?thesis using j_def by blast
qed
qed
have A3: "(∀x<t+1. ∀y<t+1. L' x j = L' y j) ∨ (∀s<t+1. L' s j = s)" if "j < N'" for j
proof-
consider "j ∈ B 1" | "j ∈ B 0" using ‹j < N'› B_props by auto
then show "(∀x<t+1. ∀y<t+1. L' x j = L' y j) ∨ (∀s<t+1. L' s j = s)"
proof (cases)
case 1
then have "(restrict (λy. L (y 0)) (cube 1 t)) y j = f j" if "y ∈ cube 1 t" for y
using that Bf_defs by simp
moreover have "∃!i. i < t ∧ y 0 = i" if "y ∈ cube 1 t" for y
using that one_dim_cube_eq_nat_set[of "t"] unfolding bij_betw_def by blast
moreover have "∃!y. y ∈ cube 1 t ∧ y 0 = i" if "i < t" for i
proof (intro ex1I_alt)
define y where "y ≡ (λx::nat. λy∈{..<1::nat}. x)"
have "y i ∈ (cube 1 t)" using that unfolding cube_def y_def by simp
moreover have "y i 0 = i" unfolding y_def by auto
moreover have "z = y i" if "z ∈ cube 1 t" and "z 0 = i" for z
proof (rule ccontr)
assume "z ≠ y i"
then obtain l where l_prop: "z l ≠ y i l" by blast
consider "l ∈ {..<1::nat}" | "l ∉ {..<1::nat}" by blast
then show False
proof cases
case 1
then show ?thesis using l_prop that(2) unfolding y_def by auto
next
case 2
then have "z l = undefined" using that unfolding cube_def by blast
moreover have "y i l = undefined" unfolding y_def using 2 by auto
ultimately show ?thesis using l_prop by presburger
qed
qed
ultimately show "∃y. (y ∈ cube 1 t ∧ y 0 = i) ∧ (∀ya. ya
∈ cube 1 t ∧ ya 0 = i ⟶ y = ya)" by blast
qed
moreover have "L i j = f j" if "i < t" for i using calculation that by force
moreover have "L i j = L x j" if "x < t" "i < t" for x i using that calculation by simp
moreover have "L' x j = L x j" if "x < t" for x using that fun_upd_other[of x t L
"λj. if j ∈ B 1 then L (t - 1) j else if j ∈ B 0 then t else undefined"]
unfolding L'_def by simp
ultimately have *: "L' x j = L' y j" if "x < t" "y < t" for x y using that by presburger
have "L' t j = L' (t - 1) j" using ‹j ∈ B 1› by (auto simp: L'_def)
also have "... = L' x j" if "x < t" for x using * by (simp add: assms(1) that)
finally have **: "L' t j = L' x j" if "x < t" for x using that by auto
have "L' x j = L' y j" if "x < t + 1" "y < t + 1" for x y
proof-
consider "x < t ∧ y = t" | "y < t ∧ x = t" | "x = t ∧ y = t" | "x < t ∧ y < t"
using ‹x < t + 1› ‹y < t + 1› by linarith
then show "L' x j = L' y j"
proof cases
case 1
then show ?thesis using ** by auto
next
case 2
then show ?thesis using ** by auto
next
case 3
then show ?thesis by simp
next
case 4
then show ?thesis using * by auto
qed
qed
then show ?thesis by blast
next
case 2
then have "∀y ∈ cube 1 t. ((restrict (λy. L (y 0)) (cube 1 t)) y) j = y 0"
using ‹j ∈ B 0› Bf_defs by auto
then have "∀y ∈ cube 1 t. L (y 0) j = y 0" by auto
moreover have "∃!y. y ∈ cube 1 t ∧ y 0 = i" if "i < t" for i
proof (intro ex1I_alt)
define y where "y ≡ (λx::nat. λy∈{..<1::nat}. x)"
have "y i ∈ (cube 1 t)" using that unfolding cube_def y_def by simp
moreover have "y i 0 = i" unfolding y_def by auto
moreover have "z = y i" if "z ∈ cube 1 t" and "z 0 = i" for z
proof (rule ccontr)
assume "z ≠ y i"
then obtain l where l_prop: "z l ≠ y i l" by blast
consider "l ∈ {..<1::nat}" | "l ∉ {..<1::nat}" by blast
then show False
proof cases
case 1
then show ?thesis using l_prop that(2) unfolding y_def by auto
next
case 2
then have "z l = undefined" using that unfolding cube_def by blast
moreover have "y i l = undefined" unfolding y_def using 2 by auto
ultimately show ?thesis using l_prop by presburger
qed
qed
ultimately show "∃y. (y ∈ cube 1 t ∧ y 0 = i) ∧ (∀ya. ya
∈ cube 1 t ∧ ya 0 = i ⟶ y = ya)" by blast
qed
ultimately have "L s j = s" if "s < t" for s using that by blast
then have "L' s j = s" if "s < t" for s using that by (auto simp: L'_def)
moreover have "L' t j = t" using 2 B_props by (auto simp: L'_def)
ultimately have "L' s j = s" if "s < t+1" for s using that by (auto simp: L'_def)
then show ?thesis by blast
qed
qed
from A1 A2 A3 show ?thesis unfolding is_line_def by simp
qed
then have F1: "is_subspace S1 1 N' (t + 1)" unfolding S1_def
using line_is_dim1_subspace[of "N'" "t+1"] N'_props assms(1) by force
moreover have F2: "∃c < r. (∀x ∈ classes 1 t i. χ (S1 x) = c)" if "i ≤ 1" for i
proof-
have "∃c < r. (∀y ∈ L' ` {..<t}. ?chi_t y = c)" unfolding L'_def using L_def by fastforce
have "∀x ∈ (L ` {..<t}). x ∈ cube N' t" using L_def
using line_points_in_cube by blast
then have "∀x ∈ (L' ` {..<t}). x ∈ cube N' t" by (auto simp: L'_def)
then have *:"∀x ∈ (L' ` {..<t}). χ x = ?chi_t x" by simp
then have "?chi_t ` (L' ` {..<t}) = χ ` (L' ` {..<t})" by force
then have "∃c < r. (∀y ∈ L' ` {..<t}. χ y = c)" using
‹∃c < r. (∀y ∈ L' ` {..<t}. ?chi_t y = c)› by fastforce
then obtain linecol where lc_def: "linecol < r ∧ (∀y ∈ L' ` {..<t}. χ y = linecol)" by blast
consider "i = 0" | "i = 1" using ‹i ≤ 1› by linarith
then show "∃c < r. (∀x ∈ classes 1 t i. χ (S1 x) = c)"
proof (cases)
case 1
assume "i = 0"
have *: "∀a t. a ∈ {..<t+1} ∧ a ≠ t ⟷ a ∈ {..<(t::nat)}" by auto
from ‹i = 0› have "classes 1 t 0 = {x . x ∈ (cube 1 (t + 1)) ∧
(∀u ∈ {((1::nat) - 0)..<1}. x u = t) ∧ t ∉ x ` {..<(1 - (0::nat))}}"
using classes_def by simp
also have "... = {x . x ∈ cube 1 (t+1) ∧ t ∉ x ` {..<(1::nat)}}" by simp
also have "... = {x . x ∈ cube 1 (t+1) ∧ (x 0 ≠ t)}" by blast
also have " ... = {x . x ∈ cube 1 (t+1) ∧ (x 0 ∈ {..<t+1} ∧ x 0 ≠ t)}"
unfolding cube_def by blast
also have " ... = {x . x ∈ cube 1 (t+1) ∧ (x 0 ∈ {..<t})}" using * by simp
finally have redef: "classes 1 t 0 = {x . x ∈ cube 1 (t+1) ∧ (x 0 ∈ {..<t})}" by simp
have "{x 0 | x . x ∈ classes 1 t 0} ⊆ {..<t}" using redef by auto
moreover have "{..<t} ⊆ {x 0 | x . x ∈ classes 1 t 0}"
proof
fix x assume x: "x ∈ {..<t}"
hence "∃a∈cube 1 t. a 0 = x"
unfolding cube_def by (intro fun_ex) auto
then show "x ∈ {x 0 |x. x ∈ classes 1 t 0}"
using x cube_subset unfolding redef by auto
qed
ultimately have **: "{x 0 | x . x ∈ classes 1 t 0} = {..<t}" by blast
have "χ (S1 x) = linecol" if "x ∈ classes 1 t 0" for x
proof-
have "x ∈ cube 1 (t+1)" unfolding classes_def using that redef by blast
then have "S1 x = L' (x 0)" unfolding S1_def by simp
moreover have "x 0 ∈ {..<t}" using ** using ‹x ∈ classes 1 t 0› by blast
ultimately show "χ (S1 x) = linecol" using lc_def using fun_upd_triv image_eqI by blast
qed
then show ?thesis using lc_def ‹i = 0› by auto
next
case 2
assume "i = 1"
have "classes 1 t 1 = {x . x ∈ (cube 1 (t + 1)) ∧ (∀u ∈ {0::nat..<1}. x
u = t) ∧ t ∉ x ` {..<0}}" unfolding classes_def by simp
also have " ... = {x . x ∈ cube 1 (t+1) ∧ (∀u ∈ {0}. x u = t)}" by simp
finally have redef: "classes 1 t 1 = {x . x ∈ cube 1 (t+1) ∧ (x 0 = t)}" by auto
have "∀s ∈ {..<t+1}. ∃!x ∈ cube 1 (t+1). (λp.
λy∈{..<1::nat}. p) s = x" using nat_set_eq_one_dim_cube[of "t+1"]
unfolding bij_betw_def by blast
then have "∃!x ∈cube 1 (t+1). (λp. λy∈{..<1::nat}. p) t = x" by auto
then obtain x where x_prop: "x ∈ cube 1 (t+1)" and "(λp.
λy∈{..<1::nat}. p) t = x" and "∀z ∈ cube 1 (t+1). (λp.
λy∈{..<1::nat}. p) t = z ⟶ z = x" by blast
then have "(λp. λy∈{0}. p) t = x ∧ (∀z ∈ cube 1
(t+1). (λp. λy∈{0}. p) t = z ⟶ z = x)" by force
then have *:"((λp. λy∈{0}. p) t) 0 = x 0 ∧ (∀z ∈ cube
1 (t+1). (λp. λy∈{0}. p) t = z ⟶ z = x)"
using x_prop by force
then have "∃!y ∈ cube 1 (t + 1). y 0 = t"
proof (intro ex1I_alt)
define y where "y ≡ (λx::nat. λy∈{..<1::nat}. x)"
have "y t ∈ (cube 1 (t + 1))" unfolding cube_def y_def by simp
moreover have "y t 0 = t" unfolding y_def by auto
moreover have "z = y t" if "z ∈ cube 1 (t + 1)" and "z 0 = t" for z
proof (rule ccontr)
assume "z ≠ y t"
then obtain l where l_prop: "z l ≠ y t l" by blast
consider "l ∈ {..<1::nat}" | "l ∉ {..<1::nat}" by blast
then show False
proof cases
case 1
then show ?thesis using l_prop that(2) unfolding y_def by auto
next
case 2
then have "z l = undefined" using that unfolding cube_def by blast
moreover have "y t l = undefined" unfolding y_def using 2 by auto
ultimately show ?thesis using l_prop by presburger
qed
qed
ultimately show "∃y. (y ∈ cube 1 (t + 1) ∧ y 0 = t) ∧ (∀ya.
ya ∈ cube 1 (t + 1) ∧ ya 0 = t ⟶ y = ya)" by blast
qed
then have "∃!x ∈ classes 1 t 1. True" using redef by simp
then obtain x where x_def: "x ∈ classes 1 t 1 ∧ (∀y ∈ classes 1 t 1. x = y)" by auto
have "χ (S1 y) < r" if "y ∈ classes 1 t 1" for y
proof-
have "y = x" using x_def that by auto
then have "χ (S1 y) = χ (S1 x)" by auto
moreover have "S1 x ∈ cube N' (t+1)" unfolding S1_def is_line_def
using line_prop line_points_in_cube redef x_def by fastforce
ultimately show "χ (S1 y) < r" using asm unfolding cube_def by auto
qed
then show ?thesis using lc_def ‹i = 1› using x_def by fast
qed
qed
ultimately show "(∃S. is_subspace S 1 N' (t + 1) ∧ (∀i ∈ {..1}.
∃c < r. (∀x ∈ classes 1 t i. χ (S x) = c)))" by blast
qed
then show ?thesis using N_def unfolding layered_subspace_def lhj_def by auto
qed
subsubsection ‹Induction step of theorem 4›
text ‹The proof has four parts:
\begin{enumerate}
\item We obtain two layered subspaces of dimension 1 and k (respectively), whose existence is
guaranteed by the assumption \<^const>‹lhj› (i.e.\ the induction hypothesis).
Additionally, we prove some useful facts about these.
\item We construct a ‹k+1›-dimensional subspace with the goal of showing that it is layered.
\item We prove that our construction is a subspace in the first place.
\item We prove that it is a layered subspace.
\end{enumerate}›
lemma hj_imp_lhj_step:
fixes r k
assumes "t > 0"
and "k ≥ 1"
and "True"
and "(⋀r k'. k' ≤ k ⟹ lhj r t k')"
and "r > 0"
shows "lhj r t (k+1)"
proof-
obtain m where m_props: "(m > 0 ∧ (∀M' ≥ m. ∀χ. χ ∈ (cube
M' (t + 1)) →⇩E {..<r::nat} ⟶ (∃S. layered_subspace S k
M' t r χ)))" using assms(4)[of "k" "r"] unfolding lhj_def by blast
define s where "s ≡ r^((t + 1)^m)"
obtain n' where n'_props: "(n' > 0 ∧ (∀N ≥ n'. ∀χ. χ ∈
(cube N (t + 1)) →⇩E {..<s::nat} ⟶ (∃S. layered_subspace
S 1 N t s χ)))" using assms(2) assms(4)[of "1" "s"] unfolding lhj_def by auto
have "(∃T. layered_subspace T (k + 1) (M') t r χ)" if χ_prop: "χ ∈ cube
M' (t + 1) →⇩E {..<r}" and M'_prop: "M' ≥ n' + m" for χ M'
proof -
define d where "d ≡ M' - (n' + m)"
define n where "n ≡ n' + d"
have "n ≥ n'" unfolding n_def d_def by simp
have "n + m = M'" unfolding n_def d_def using M'_prop by simp
have line_subspace_s: "∃S. layered_subspace S 1 n t s χ ∧ is_line
(λs∈{..<t+1}. S (SOME p. p∈cube 1 (t+1) ∧ p 0 = s)) n (t+1)" if "χ
∈ (cube n (t + 1)) →⇩E {..<s::nat}" for χ
proof-
have "∃S. layered_subspace S 1 n t s χ" using that n'_props ‹n ≥ n'› by blast
then obtain L where "layered_subspace L 1 n t s χ" by blast
then have "is_subspace L 1 n (t+1)" unfolding layered_subspace_def by simp
then have "is_line (λs∈{..<t+1}. L (SOME p. p∈cube 1 (t+1) ∧ p 0 = s)) n (t + 1)"
using dim1_subspace_is_line[of "t+1" "L" "n"] assms(1) by simp
then show "∃S. layered_subspace S 1 n t s χ ∧ is_line (λs∈{..<t
+ 1}. S (SOME p. p ∈ cube 1 (t+1) ∧ p 0 = s)) n (t + 1)" using
‹layered_subspace L 1 n t s χ› by auto
qed
paragraph ‹Part 1: Obtaining the subspaces ‹L› and ‹S›\\›
text ‹Recall that @{term lhj} claims the existence of a layered subspace for any colouring
(of a fixed size, where the size of a colouring refers to the number of colours). Therefore, the
colourings have to be defined first, before the layered subspaces can be obtained. The colouring
‹χL› here is $\chi^*$ in the book~\<^cite>‹"thebook"›, an
‹s›-colouring; see the fact ‹s_coloured› a couple of lines
below.›
define χL where "χL ≡ (λx ∈ cube n (t+1). (λy ∈ cube m
(t + 1). χ (join x y n m)))"
have A: "∀x ∈ cube n (t+1). ∀y ∈ cube m (t+1). χ (join x y n m) ∈ {..<r}"
proof(safe)
fix x y
assume "x ∈ cube n (t+1)" "y ∈ cube m (t+1)"
then have "join x y n m ∈ cube (n+m) (t+1)" using join_cubes[of x n t y m] by simp
then show "χ (join x y n m) < r" using χ_prop ‹n + m = M'› by blast
qed
have χL_prop: "χL ∈ cube n (t+1) →⇩E cube m (t+1) →⇩E {..<r}"
using A by (auto simp: χL_def)
have "card (cube m (t+1) →⇩E {..<r}) = (card {..<r}) ^ (card (cube m (t+1)))"
using card_PiE[of "cube m (t + 1)" "λ_. {..<r}"] by (simp add: cube_def finite_PiE)
also have "... = r ^ (card (cube m (t+1)))" by simp
also have "... = r ^ ((t+1)^m)" using cube_card unfolding cube_def by simp
finally have "card (cube m (t+1) →⇩E {..<r}) = r ^ ((t+1)^m)" .
then have s_coloured: "card (cube m (t+1) →⇩E {..<r}) = s" unfolding s_def by simp
have "s > 0" using assms(5) unfolding s_def by simp
then obtain φ where φ_prop: "bij_betw φ (cube m (t+1) →⇩E {..<r}) {..<s}"
using assms(5) ex_bij_betw_nat_finite_2[of "cube m (t+1) →⇩E {..<r}" "s"] s_coloured by blast
define χL_s where "χL_s ≡ (λx∈cube n (t+1). φ (χL x))"
have "χL_s ∈ cube n (t+1) →⇩E {..<s}"
proof
fix x assume a: "x ∈ cube n (t+1)"
then have "χL_s x = φ (χL x)" unfolding χL_s_def by simp
moreover have "χL x ∈ (cube m (t+1) →⇩E {..<r})"
using a χL_def χL_prop unfolding χL_def by blast
moreover have "φ (χL x) ∈ {..<s}" using φ_prop calculation(2) unfolding bij_betw_def by blast
ultimately show "χL_s x ∈ {..<s}" by auto
qed (auto simp: χL_s_def)
text ‹L is the layered line which we obtain from the monochromatic line guaranteed to
exist by the assumption ‹hj s t›.›
then obtain L where L_prop: "layered_subspace L 1 n t s χL_s" using line_subspace_s by blast
define L_line where "L_line ≡ (λs∈{..<t+1}. L (SOME p. p∈cube 1 (t+1) ∧ p 0 = s))"
have L_line_base_prop: "∀s ∈ {..<t+1}. L_line s ∈ cube n (t+1)"
using assms(1) dim1_subspace_is_line[of "t+1" "L" "n"] L_prop line_points_in_cube[of L_line n "t+1"]
unfolding layered_subspace_def L_line_def by auto
text ‹Here, ‹χS› is $\chi^{**}$ in the book~\<^cite>‹"thebook"›, an r-colouring.›
define χS where "χS ≡ (λy∈cube m (t+1). χ (join (L_line 0) y n m))"
have "χS ∈ (cube m (t + 1)) →⇩E {..<r::nat}"
proof
fix x assume a: "x ∈ cube m (t+1)"
then have "χS x = χ (join (L_line 0) x n m)" unfolding χS_def by simp
moreover have "L_line 0 = L (SOME p. p∈cube 1 (t+1) ∧ p 0 = 0)"
using L_prop assms(1) unfolding L_line_def by simp
moreover have "(SOME p. p∈cube 1 (t+1) ∧ p 0 = 0) ∈ cube 1 (t+1)" using cube_props(4)[of 0 "t+1"]
using assms(1) by auto
moreover have "L ∈ cube 1 (t+1) →⇩E cube n (t+1)"
using L_prop unfolding layered_subspace_def is_subspace_def by blast
moreover have "L (SOME p. p∈cube 1 (t+1) ∧ p 0 = 0) ∈ cube n (t+1)"
using calculation (3,4) unfolding cube_def by auto
moreover have "join (L_line 0) x n m ∈ cube (n + m) (t+1)" using join_cubes a calculation(2, 5) by auto
ultimately show "χS x ∈ {..<r}" using A a by fastforce
qed (auto simp: χS_def)
text ‹‹S› is the $k$-dimensional layered subspace that arises as a
consequence of the induction hypothesis. Note that the colouring is ‹χS›, an
‹r›-colouring.›
then obtain S where S_prop: "layered_subspace S k m t r χS" using assms(4) m_props by blast
text ‹Remark: ‹L_Line i› returns the i-th point of the line.›
paragraph ‹Part 2: Constructing the $(k+1)$-dimensional subspace ‹T›\\›
text ‹Below, ‹Tset› is the set as defined in the book~\<^cite>‹"thebook"›. It
represents the $(k+1)$-dimensional subspace. In this construction, subspaces (e.g.
‹T›) are functions whose image is a set. See the fact ‹im_T_eq_Tset›
below.›
text‹Having obtained our subspaces ‹S› and ‹L›, we define the
$(k+1)$-dimensional subspace very straightforwardly Namely, T = L \times S. Since we represent
tuples by function sets, we need an appropriate operator that mirrors the Cartesian product
$\times$ for these. We call this ‹join› and define it for elements of a function
set.›
define Tset where "Tset ≡ {join (L_line i) s n m | i s . i ∈ {..<t+1} ∧ s ∈ S ` (cube k (t+1))}"
define T' where "T' ≡ (λx ∈ cube 1 (t+1). λy ∈ cube k (t+1). join
(L_line (x 0)) (S y) n m)"
have T'_prop: "T' ∈ cube 1 (t+1) →⇩E cube k (t+1) →⇩E cube (n + m) (t+1)"
proof
fix x assume a: "x ∈ cube 1 (t+1)"
show "T' x ∈ cube k (t + 1) →⇩E cube (n + m) (t + 1)"
proof
fix y assume b: "y ∈ cube k (t+1)"
then have "T' x y = join (L_line (x 0)) (S y) n m" using a unfolding T'_def by simp
moreover have "L_line (x 0) ∈ cube n (t+1)" using a L_line_base_prop unfolding cube_def by blast
moreover have "S y ∈ cube m (t+1)"
using subspace_elems_embed[of "S" "k" "m" "t+1"] S_prop b unfolding layered_subspace_def by blast
ultimately show "T' x y ∈ cube (n + m) (t + 1)" using join_cubes by presburger
next
qed (unfold T'_def; use a in simp)
qed (auto simp: T'_def)
define T where "T ≡ (λx ∈ cube (k + 1) (t+1). T' (λy ∈ {..<1}. x
y) (λy ∈ {..<k}. x (y + 1)))"
have T_prop: "T ∈ cube (k+1) (t+1) →⇩E cube (n+m) (t+1)"
proof
fix x assume a: "x ∈ cube (k+1) (t+1)"
then have "T x = T' (λy ∈ {..<1}. x y) (λy ∈ {..<k}. x (y + 1))" unfolding T_def by auto
moreover have "(λy ∈ {..<1}. x y) ∈ cube 1 (t+1)" using a unfolding cube_def by auto
moreover have "(λy ∈ {..<k}. x (y + 1)) ∈ cube k (t+1)" using a unfolding cube_def by auto
moreover have "T' (λy ∈ {..<1}. x y) (λy ∈ {..<k}. x (y + 1)) ∈ cube (n + m) (t+1)"
using T'_prop calculation unfolding T'_def by blast
ultimately show "T x ∈ cube (n + m) (t+1)" by argo
qed (auto simp: T_def)
have im_T_eq_Tset: "T ` cube (k+1) (t+1) = Tset"
proof
show "T ` cube (k + 1) (t + 1) ⊆ Tset"
proof
fix x assume "x ∈ T ` cube (k+1) (t+1)"
then obtain y where y_prop: "y ∈ cube (k+1) (t+1) ∧ x = T y" by blast
then have "T y = T' (λi ∈ {..<1}. y i) (λi ∈ {..<k}. y (i + 1))" unfolding T_def by simp
moreover have "(λi ∈ {..<1}. y i) ∈ cube 1 (t+1)" using y_prop unfolding cube_def by auto
moreover have "(λi ∈ {..<k}. y (i + 1)) ∈ cube k (t+1)" using y_prop unfolding cube_def by auto
moreover have " T' (λi ∈ {..<1}. y i) (λi ∈ {..<k}. y (i + 1)) =
join (L_line ((λi ∈ {..<1}. y i) 0)) (S (λi ∈ {..<k}. y (i + 1))) n m"
using calculation unfolding T'_def by auto
ultimately have *: "T y = join (L_line ((λi ∈ {..<1}. y i) 0))
(S (λi ∈ {..<k}. y (i + 1))) n m" by simp
have "(λi ∈ {..<1}. y i) 0 ∈ {..<t+1}" using y_prop unfolding cube_def by auto
moreover have "S (λi ∈ {..<k}. y (i + 1)) ∈ S ` (cube k (t+1))"
using ‹(λi∈{..<k}. y (i + 1)) ∈ cube k (t + 1)› by blast
ultimately have "T y ∈ Tset" using * unfolding Tset_def by blast
then show "x ∈ Tset" using y_prop by simp
qed
show "Tset ⊆ T ` cube (k + 1) (t + 1)"
proof
fix x assume "x ∈ Tset"
then obtain i sx sxinv where isx_prop: "x = join (L_line i) sx n m ∧ i ∈ {..<t+1}
∧ sx ∈ S ` (cube k (t+1)) ∧ sxinv ∈ cube k (t+1) ∧ S sxinv = sx"
unfolding Tset_def by blast
let ?f1 = "(λj ∈ {..<1::nat}. i)"
let ?f2 = "sxinv"
have "?f1 ∈ cube 1 (t+1)" using isx_prop unfolding cube_def by simp
moreover have "?f2 ∈ cube k (t+1)" using isx_prop by blast
moreover have "x = join (L_line (?f1 0)) (S ?f2) n m" by (simp add: isx_prop)
ultimately have *: "x = T' ?f1 ?f2" unfolding T'_def by simp
define f where "f ≡ (λj ∈ {1..<k+1}. ?f2 (j - 1))(0:=i)"
have "f ∈ cube (k+1) (t+1)"
proof (unfold cube_def; intro PiE_I)
fix j assume "j ∈ {..<k+1}"
then consider "j = 0" | "j ∈ {1..<k+1}" by fastforce
then show "f j ∈ {..<t+1}"
proof (cases)
case 1
then have "f j = i" unfolding f_def by simp
then show ?thesis using isx_prop by simp
next
case 2
then have "j - 1 ∈ {..<k}" by auto
moreover have "f j = ?f2 (j - 1)" using 2 unfolding f_def by simp
moreover have "?f2 (j - 1) ∈ {..<t+1}" using calculation(1) isx_prop unfolding cube_def by blast
ultimately show ?thesis by simp
qed
qed (auto simp: f_def)
have "?f1 = (λj ∈ {..<1}. f j)" unfolding f_def using isx_prop by auto
moreover have "?f2 = (λj∈{..<k}. f (j+1))"
using calculation isx_prop unfolding cube_def f_def by fastforce
ultimately have "T' ?f1 ?f2 = T f" using ‹f ∈ cube (k+1) (t+1)› unfolding T_def by simp
then show "x ∈ T ` cube (k + 1) (t + 1)" using *
using ‹f ∈ cube (k + 1) (t + 1)› by blast
qed
qed
have "Tset ⊆ cube (n + m) (t+1)"
proof
fix x assume a: "x∈Tset"
then obtain i sx where isx_props: "x = join (L_line i) sx n m ∧ i ∈ {..<t+1} ∧
sx ∈ S ` (cube k (t+1))" unfolding Tset_def by blast
then have "L_line i ∈ cube n (t+1)" using L_line_base_prop by blast
moreover have "sx ∈ cube m (t+1)"
using subspace_elems_embed[of "S" "k" "m" "t+1"] S_prop isx_props unfolding layered_subspace_def by blast
ultimately show "x ∈ cube (n + m) (t+1)" using join_cubes[of "L_line i" "n" "t" sx m] isx_props by simp
qed
paragraph ‹Part 3: Proving that ‹T› is a subspace\\›
text ‹To prove something is a subspace, we have to provide the ‹B› and ‹f›
satisfying the subspace properties.
We construct ‹BT› and ‹fT› from ‹BS›, ‹fS› and
‹BL›, ‹fL›, which correspond to the $k$-dimensional subspace ‹S›
and the $1$-dimensional subspace (i.e.\ line) ‹L›, respectively.›
obtain BS fS where BfS_props: "disjoint_family_on BS {..k}" "⋃(BS ` {..k}) = {..<m}" "({}
∉ BS ` {..<k})" " fS ∈ (BS k) →⇩E {..<t+1}" "S ∈ (cube k (t+1))
→⇩E (cube m (t+1)) " "(∀y ∈ cube k (t+1). (∀i ∈ BS k.
S y i = fS i) ∧ (∀j<k. ∀i ∈ BS j. (S y) i = y j))" using S_prop
unfolding layered_subspace_def is_subspace_def by auto
obtain BL fL where BfL_props: "disjoint_family_on BL {..1}" "⋃(BL ` {..1}) = {..<n}"
"({} ∉ BL ` {..<1})" "fL ∈ (BL 1) →⇩E {..<t+1}" "L ∈ (cube 1
(t+1)) →⇩E (cube n (t+1))" "(∀y ∈ cube 1 (t+1). (∀i ∈
BL 1. L y i = fL i) ∧ (∀j<1. ∀i ∈ BL j. (L y) i = y j))" using L_prop
unfolding layered_subspace_def is_subspace_def by auto
define Bstat where "Bstat ≡ set_incr n (BS k) ∪ BL 1"
define Bvar where "Bvar ≡ (λi::nat. (if i = 0 then BL 0 else set_incr n (BS (i - 1))))"
define BT where "BT ≡ (λi ∈ {..<k+1}. Bvar i)((k+1):=Bstat)"
define fT where "fT ≡ (λx. (if x ∈ BL 1 then fL x else (if x ∈ set_incr n
(BS k) then fS (x - n) else undefined)))"
have fact1: "set_incr n (BS k) ∩ BL 1 = {}" using BfL_props BfS_props unfolding set_incr_def by auto
have fact2: "BL 0 ∩ (⋃i∈{..<k}. set_incr n (BS i)) = {}"
using BfL_props BfS_props unfolding set_incr_def by auto
have fact3: "∀i ∈ {..<k}. BL 0 ∩ set_incr n (BS i) = {}"
using BfL_props BfS_props unfolding set_incr_def by auto
have fact4: "∀i ∈ {..<k+1}. ∀j ∈ {..<k+1}. i ≠ j
⟶ set_incr n (BS i) ∩ set_incr n (BS j) = {}"
using set_incr_disjoint_family[of BS k] BfS_props unfolding disjoint_family_on_def by simp
have fact5: "∀i ∈ {..<k+1}. Bvar i ∩ Bstat = {}"
proof
fix i assume a: "i ∈ {..<k+1}"
show "Bvar i ∩ Bstat = {}"
proof (cases i)
case 0
then have "Bvar i = BL 0" unfolding Bvar_def by simp
moreover have "BL 0 ∩ BL 1 = {}" using BfL_props unfolding disjoint_family_on_def by simp
moreover have "set_incr n (BS k) ∩ BL 0 = {}" using BfL_props BfS_props unfolding set_incr_def by auto
ultimately show ?thesis unfolding Bstat_def by blast
next
case (Suc nat)
then have "Bvar i = set_incr n (BS nat)" unfolding Bvar_def by simp
moreover have "set_incr n (BS nat) ∩ BL 1 = {}" using BfS_props BfL_props a Suc unfolding set_incr_def
by auto
moreover have "set_incr n (BS nat) ∩ set_incr n (BS k) = {}" using a Suc fact4 by simp
ultimately show ?thesis unfolding Bstat_def by blast
qed
qed
text ‹The facts ‹F1›, ..., ‹F5› are the disjuncts in the subspace definition.›
have "Bvar ` {..<k+1} = BL ` {..<1} ∪ Bvar ` {1..<k+1}" unfolding Bvar_def by force
also have " ... = BL ` {..<1} ∪ {set_incr n (BS i) | i . i ∈ {..<k}} " unfolding Bvar_def by fastforce
moreover have "{} ∉ BL ` {..<1}" using BfL_props by auto
moreover have "{} ∉ {set_incr n (BS i) | i . i ∈ {..<k}}" using BfS_props(2, 3) set_incr_def by fastforce
ultimately have "{} ∉ Bvar ` {..<k+1}" by simp
then have F1: "{} ∉ BT ` {..<k+1}" unfolding BT_def by simp
moreover
{
have F2_aux: "disjoint_family_on Bvar {..<k+1}"
proof (unfold disjoint_family_on_def; safe)
fix m n x assume a: "m < k + 1" "n < k + 1" "m ≠ n" "x ∈ Bvar m" "x ∈ Bvar n"
show "x ∈ {}"
proof (cases "n")
case 0
then show ?thesis using a fact3 unfolding Bvar_def by auto
next
case (Suc nnat)
then have *: "n = Suc nnat" by simp
then show ?thesis
proof (cases m)
case 0
then show ?thesis using a fact3 unfolding Bvar_def by auto
next
case (Suc mnat)
then show ?thesis using a fact4 * unfolding Bvar_def by fastforce
qed
qed
qed
have F2: "disjoint_family_on BT {..k+1}"
proof
fix m n assume a: "m∈{..k+1}" "n∈{..k+1}" "m ≠ n"
have "∀x. x ∈ BT m ∩ BT n ⟶ x ∈ {}"
proof (intro allI impI)
fix x assume b: "x ∈ BT m ∩ BT n"
have "m < k + 1 ∧ n < k + 1 ∨ m = k + 1 ∧ n = k + 1 ∨ m < k + 1
∧ n = k + 1 ∨ m = k + 1 ∧ n < k + 1" using a le_eq_less_or_eq by auto
then show "x ∈ {}"
proof (elim disjE)
assume c: "m < k + 1 ∧ n < k + 1"
then have "BT m = Bvar m ∧ BT n = Bvar n" unfolding BT_def by simp
then show "x ∈ {}" using a b c fact4 F2_aux unfolding Bvar_def disjoint_family_on_def by auto
qed (use a b fact5 in ‹auto simp: BT_def›)
qed
then show "BT m ∩ BT n = {}" by auto
qed
}
moreover have F3: "⋃(BT ` {..k+1}) = {..<n + m}"
proof
show "⋃ (BT ` {..k + 1}) ⊆ {..<n + m}"
proof
fix x assume "x ∈ ⋃ (BT ` {..k + 1})"
then obtain i where i_prop: "i ∈ {..k+1} ∧ x ∈ BT i" by blast
then consider "i = k +1" | "i ∈ {..<k+1}" by fastforce
then show "x ∈ {..<n + m}"
proof (cases)
case 1
then have "x ∈ Bstat" using i_prop unfolding BT_def by simp
then have "x ∈ BL 1 ∨ x ∈ set_incr n (BS k)" unfolding Bstat_def by blast
then have "x ∈ {..<n} ∨ x ∈ {n..<n+m}" using BfL_props BfS_props(2) set_incr_image[of BS k m n]
by blast
then show ?thesis by auto
next
case 2
then have "x ∈ Bvar i" using i_prop unfolding BT_def by simp
then have "x ∈ BL 0 ∨ x ∈ set_incr n (BS (i - 1))" unfolding Bvar_def by presburger
then show ?thesis
proof (elim disjE)
assume "x ∈ BL 0"
then have "x ∈ {..<n}" using BfL_props by auto
then show "x ∈ {..<n + m}" by simp
next
assume a: "x ∈ set_incr n (BS (i - 1))"
then have "i - 1 ≤ k"
by (meson atMost_iff i_prop le_diff_conv)
then have "set_incr n (BS (i - 1)) ⊆ {n..<n+m}" using set_incr_image[of BS k m n] BfS_props
by auto
then show "x ∈ {..<n+m}" using a by auto
qed
qed
qed
next
show "{..<n + m} ⊆ ⋃ (BT ` {..k + 1})"
proof
fix x assume "x ∈ {..<n + m}"
then consider "x ∈ {..<n}" | "x ∈ {n..<n+m}" by fastforce
then show "x ∈ ⋃ (BT ` {..k + 1})"
proof (cases)
case 1
have *: "{..1::nat} = {0, 1::nat}" by auto
from 1 have "x ∈ ⋃ (BL ` {..1::nat})" using BfL_props by simp
then have "x ∈ BL 0 ∨ x ∈ BL 1" using * by simp
then show ?thesis
proof (elim disjE)
assume "x ∈ BL 0"
then have "x ∈ Bvar 0" unfolding Bvar_def by simp
then have "x ∈ BT 0" unfolding BT_def by simp
then show "x ∈ ⋃ (BT ` {..k + 1})" by auto
next
assume "x ∈ BL 1"
then have "x ∈ Bstat" unfolding Bstat_def by simp
then have "x ∈ BT (k+1)" unfolding BT_def by simp
then show "x ∈ ⋃ (BT ` {..k + 1})" by auto
qed
next
case 2
then have "x ∈ (⋃i≤k. set_incr n (BS i))" using set_incr_image[of BS k m n] BfS_props by simp
then obtain i where i_prop: "i ≤ k ∧ x ∈ set_incr n (BS i)" by blast
then consider "i = k" | "i < k" by fastforce
then show ?thesis
proof (cases)
case 1
then have "x ∈ Bstat" unfolding Bstat_def using i_prop by auto
then have "x ∈ BT (k+1)" unfolding BT_def by simp
then show ?thesis by auto
next
case 2
then have "x ∈ Bvar (i + 1)" unfolding Bvar_def using i_prop by simp
then have "x ∈ BT (i + 1)" unfolding BT_def using 2 by force
then show ?thesis using 2 by auto
qed
qed
qed
qed
moreover have F4: "fT ∈ (BT (k+1)) →⇩E {..<t+1}"
proof
fix x assume "x ∈ BT (k+1)"
then have "x ∈ Bstat" unfolding BT_def by simp
then have "x ∈ BL 1 ∨ x ∈ set_incr n (BS k)" unfolding Bstat_def by auto
then show "fT x ∈ {..<t + 1}"
proof (elim disjE)
assume "x ∈ BL 1"
then have "fT x = fL x" unfolding fT_def by simp
then show "fT x ∈ {..<t+1}" using BfL_props ‹x ∈ BL 1› by auto
next
assume a: "x ∈ set_incr n (BS k)"
then have "fT x = fS (x - n)" using fact1 unfolding fT_def by auto
moreover have "x - n ∈ BS k" using a unfolding set_incr_def by auto
ultimately show "fT x ∈ {..<t+1}" using BfS_props by auto
qed
qed(auto simp: BT_def Bstat_def fT_def)
moreover have F5: "((∀i ∈ BT (k + 1). T y i = fT i) ∧ (∀j<k+1.
∀i ∈ BT j. (T y) i = y j))" if "y ∈ cube (k + 1) (t + 1)" for y
proof(intro conjI allI impI ballI)
fix i assume "i ∈ BT (k + 1)"
then have "i ∈ Bstat" unfolding BT_def by simp
then consider "i ∈ set_incr n (BS k)" | "i ∈ BL 1" unfolding Bstat_def by blast
then show "T y i = fT i"
proof (cases)
case 1
then have "∃s<m. i = n + s" unfolding set_incr_def using BfS_props(2) by auto
then obtain s where s_prop: "s < m ∧ i = n + s" by blast
then have *: " i ∈ {n..<n+m}" by simp
have "i ∉ BL 1" using 1 fact1 by auto
then have "fT i = fS (i - n)" using 1 unfolding fT_def by simp
then have **: "fT i = fS s" using s_prop by simp
have XX: "(λz ∈ {..<k}. y (z + 1)) ∈ cube k (t+1)" using split_cube that by simp
have XY: "s ∈ BS k" using s_prop 1 unfolding set_incr_def by auto
from that have "T y i = (T' (λz ∈ {..<1}. y z) (λz ∈ {..<k}. y (z + 1))) i"
unfolding T_def by auto
also have "... = (join (L_line ((λz ∈ {..<1}. y z) 0)) (S (λz ∈
{..<k}. y (z + 1))) n m) i" using split_cube that unfolding T'_def by simp
also have "... = (join (L_line (y 0)) (S (λz ∈ {..<k}. y (z + 1))) n m) i" by simp
also have "... = (S (λz ∈ {..<k}. y (z + 1))) s" using * s_prop unfolding join_def by simp
also have "... = fS s" using XX XY BfS_props(6) by blast
finally show ?thesis using ** by simp
next
case 2
have XZ: "y 0 ∈ {..<t+1}" using that unfolding cube_def by auto
have XY: "i ∈ {..<n}" using 2 BfL_props(2) by blast
have XX: "(λz ∈ {..<1}. y z) ∈ cube 1 (t+1)" using that split_cube by simp
have some_eq_restrict: "(SOME p. p∈cube 1 (t+1) ∧ p 0 = ((λz ∈ {..<1}.
y z) 0)) = (λz ∈ {..<1}. y z)"
proof
show "restrict y {..<1} ∈ cube 1 (t + 1) ∧ restrict y {..<1} 0 = restrict y {..<1} 0"
using XX by simp
next
fix p
assume "p ∈ cube 1 (t+1) ∧ p 0 = restrict y {..<1} 0"
moreover have "p u = restrict y {..<1} u" if "u ∉ {..<1}" for u
using that calculation XX unfolding cube_def
using PiE_arb[of "restrict y {..<1}" "{..<1}" "λx. {..<t + 1}" u]
PiE_arb[of p "{..<1}" "λx. {..<t + 1}" u] by simp
ultimately show "p = restrict y {..<1}" by auto
qed
from that have "T y i = (T' (λz ∈ {..<1}. y z) (λz ∈ {..<k}. y (z + 1))) i"
unfolding T_def by auto
also have "... = (join (L_line ((λz ∈ {..<1}. y z) 0)) (S (λz ∈ {..<k}. y (z + 1))) n m) i"
using split_cube that unfolding T'_def by simp
also have "... = (L_line ((λz ∈ {..<1}. y z) 0)) i" using XY unfolding join_def by simp
also have "... = L (SOME p. p∈cube 1 (t+1) ∧ p 0 = ((λz ∈ {..<1}. y z) 0)) i"
using XZ unfolding L_line_def by auto
also have "... = L (λz ∈ {..<1}. y z) i" using some_eq_restrict by simp
also have "... = fL i" using BfL_props(6) XX 2 by blast
also have "... = fT i" using 2 unfolding fT_def by simp
finally show ?thesis .
qed
next
fix j i assume "j < k + 1" "i ∈ BT j"
then have i_prop: "i ∈ Bvar j" unfolding BT_def by auto
consider "j = 0" | "j > 0" by auto
then show "T y i = y j"
proof cases
case 1
then have "i ∈ BL 0" using i_prop unfolding Bvar_def by auto
then have XY: "i ∈ {..<n}" using 1 BfL_props(2) by blast
have XX: "(λz ∈ {..<1}. y z) ∈ cube 1 (t+1)" using that split_cube by simp
have XZ: "y 0 ∈ {..<t+1}" using that unfolding cube_def by auto
have some_eq_restrict: "(SOME p. p∈cube 1 (t+1) ∧ p 0 = ((λz ∈ {..<1}.
y z) 0)) = (λz ∈ {..<1}. y z)"
proof
show "restrict y {..<1} ∈ cube 1 (t + 1) ∧ restrict y {..<1} 0 = restrict y {..<1} 0" using XX by simp
next
fix p
assume "p ∈ cube 1 (t+1) ∧ p 0 = restrict y {..<1} 0"
moreover have "p u = restrict y {..<1} u" if "u ∉ {..<1}" for u
using that calculation XX unfolding cube_def
using PiE_arb[of "restrict y {..<1}" "{..<1}" "λx. {..<t + 1}" u]
PiE_arb[of p "{..<1}" "λx. {..<t + 1}" u] by simp
ultimately show "p = restrict y {..<1}" by auto
qed
from that have "T y i = (T' (λz ∈ {..<1}. y z) (λz ∈ {..<k}. y (z + 1))) i"
unfolding T_def by auto
also have "... = (join (L_line ((λz ∈ {..<1}. y z) 0)) (S (λz ∈ {..<k}. y (z + 1))) n m) i"
using split_cube that unfolding T'_def by simp
also have "... = (L_line ((λz ∈ {..<1}. y z) 0)) i" using XY unfolding join_def by simp
also have "... = L (SOME p. p∈cube 1 (t+1) ∧ p 0 = ((λz ∈ {..<1}. y z) 0)) i"
using XZ unfolding L_line_def by auto
also have "... = L (λz ∈ {..<1}. y z) i" using some_eq_restrict by simp
also have "... = (λz ∈ {..<1}. y z) j" using BfL_props(6) XX 1 ‹i ∈ BL 0› by blast
also have "... = (λz ∈ {..<1}. y z) 0" using 1 by blast
also have "... = y 0" by simp
also have "... = y j" using 1 by simp
finally show ?thesis .
next
case 2
then have "i ∈ set_incr n (BS (j - 1))" using i_prop unfolding Bvar_def by simp
then have "∃s<m. n + s = i" using BfS_props(2) ‹j < k + 1› unfolding set_incr_def by force
then obtain s where s_prop: "s < m" "i = s + n" by auto
then have *: " i ∈ {n..<n+m}" by simp
have XX: "(λz ∈ {..<k}. y (z + 1)) ∈ cube k (t+1)" using split_cube that by simp
have XY: "s ∈ BS (j - 1)" using s_prop 2 ‹i ∈ set_incr n (BS (j - 1))›
unfolding set_incr_def by force
from that have "T y i = (T' (λz ∈ {..<1}. y z) (λz ∈ {..<k}. y (z + 1))) i"
unfolding T_def by auto
also have "... = (join (L_line ((λz ∈ {..<1}. y z) 0)) (S (λz ∈ {..<k}. y (z + 1))) n m) i"
using split_cube that unfolding T'_def by simp
also have "... = (join (L_line (y 0)) (S (λz ∈ {..<k}. y (z + 1))) n m) i" by simp
also have "... = (S (λz ∈ {..<k}. y (z + 1))) s" using * s_prop unfolding join_def by simp
also have "... = (λz ∈ {..<k}. y (z + 1)) (j-1)"
using XX XY BfS_props(6) 2 ‹j < k + 1› by auto
also have "... = y j" using 2 ‹j < k + 1› by force
finally show ?thesis .
qed
qed
ultimately have subspace_T: "is_subspace T (k+1) (n+m) (t+1)" unfolding is_subspace_def using T_prop by metis
paragraph ‹Part 4: Proving ‹T› is layered\\›
text ‹The following redefinition of the classes makes proving the layered property easier.›
define T_class where "T_class ≡ (λj∈{..k}. {join (L_line i) s n m | i s . i
∈ {..<t} ∧ s ∈ S ` (classes k t j)})(k+1:= {join (L_line t) (SOME s. s ∈ S `
(cube m (t+1))) n m})"
have classprop: "T_class j = T ` classes (k + 1) t j" if j_prop: "j ≤ k" for j
proof
show "T_class j ⊆ T ` classes (k + 1) t j"
proof
fix x assume "x ∈ T_class j"
from that have "T_class j = {join (L_line i) s n m | i s . i ∈ {..<t} ∧ s ∈ S ` (classes k t j)}"
unfolding T_class_def by simp
then obtain i s where is_defs: "x = join (L_line i) s n m ∧ i < t ∧ s ∈ S ` (classes k t j)"
using ‹x ∈ T_class j› unfolding T_class_def by auto
moreover have *:"classes k t j ⊆ cube k (t+1)" unfolding classes_def by simp
moreover have "∃!y. y ∈ classes k t j ∧ s = S y"
using subspace_inj_on_cube[of S k m "t+1"] S_prop inj_onD[of S "cube k (t+1)"] calculation
unfolding layered_subspace_def inj_on_def by blast
ultimately obtain y where y_prop: "y ∈ classes k t j ∧ s = S y ∧
(∀z∈classes k t j. s = S z ⟶ y = z)" by auto
define p where "p ≡ join (λg∈{..<1}. i) y 1 k"
have "(λg∈{..<1}. i) ∈ cube 1 (t+1)" using is_defs unfolding cube_def by simp
then have p_in_cube: "p ∈ cube (k + 1) (t+1)"
using join_cubes[of "(λg∈{..<1}. i)" 1 t y k] y_prop * unfolding p_def by auto
then have **: "p 0 = i ∧ (∀l < k. p (l + 1) = y l)" unfolding p_def join_def by simp
have "t ∉ y ` {..<(k - j)}" using y_prop unfolding classes_def by simp
then have "∀u < k - j. y u ≠ t" by auto
then have "∀u < k - j. p (u + 1) ≠ t" using ** by simp
moreover have "p 0 ≠ t" using is_defs ** by simp
moreover have "∀u < k - j + 1. p u ≠ t"
using calculation by (auto simp: algebra_simps less_Suc_eq_0_disj)
ultimately have "∀u < (k + 1) - j. p u ≠ t" using that by auto
then have A1: "t ∉ p ` {..<((k+1) - j)}" by blast
have "p u = t" if "u ∈ {k - j + 1..<k+1}" for u
proof -
from that have "u - 1 ∈ {k - j..<k}" by auto
then have "y (u - 1) = t" using y_prop unfolding classes_def by blast
then show "p u = t" using ** that ‹u - 1 ∈ {k - j..<k}› by auto
qed
then have A2: "∀u∈{(k+1) - j..<k+1}. p u = t" using that by auto
from A1 A2 p_in_cube have "p ∈ classes (k+1) t j" unfolding classes_def by blast
moreover have "x = T p"
proof-
have loc_useful:"(λy ∈ {..<k}. p (y + 1)) = (λz ∈ {..<k}. y z)" using ** by auto
have "T p = T' (λy ∈ {..<1}. p y) (λy ∈ {..<k}. p (y + 1))"
using p_in_cube unfolding T_def by auto
have "T' (λy ∈ {..<1}. p y) (λy ∈ {..<k}. p (y + 1))
= join (L_line ((λy ∈ {..<1}. p y) 0)) (S (λy ∈ {..<k}. p (y + 1))) n m"
using split_cube p_in_cube unfolding T'_def by simp
also have "... = join (L_line (p 0)) (S (λy ∈ {..<k}. p (y + 1))) n m" by simp
also have "... = join (L_line i) (S (λy ∈ {..<k}. p (y + 1))) n m" by (simp add: **)
also have "... = join (L_line i) (S (λz ∈ {..<k}. y z)) n m" using loc_useful by simp
also have "... = join (L_line i) (S y) n m" using y_prop * unfolding cube_def by auto
also have "... = x" using is_defs y_prop by simp
finally show "x = T p"
using ‹T p = T' (restrict p {..<1}) (λy∈{..<k}. p (y + 1))› by presburger
qed
ultimately show "x ∈ T ` classes (k + 1) t j" by blast
qed
next
show "T ` classes (k + 1) t j ⊆ T_class j"
proof
fix x assume "x ∈ T ` classes (k+1) t j"
then obtain y where y_prop: "y ∈ classes (k+1) t j ∧ T y = x" by blast
then have y_props: "(∀u ∈ {((k+1)-j)..<k+1}. y u = t) ∧ t ∉ y ` {..<(k+1) - j }"
unfolding classes_def by blast
define z where "z ≡ (λv ∈ {..<k}. y (v+1))"
have "z ∈ cube k (t+1)" using y_prop classes_subset_cube[of "k+1" t j] unfolding z_def cube_def by auto
moreover
{
have "z ` {..<k - j} = y ` ((+) 1 ` {..<k-j}) " unfolding z_def by fastforce
also have "... = y ` {1..<k-j+1}" by (simp add: atLeastLessThanSuc_atLeastAtMost image_Suc_lessThan)
also have "... = y ` {1..<(k+1)-j}" using j_prop by auto
finally have "z ` {..<k - j} ⊆ y ` {..<(k+1)-j}" by auto
then have "t ∉ z ` {..<k - j}" using y_props by blast
}
moreover have "∀u ∈ {k-j..<k}. z u = t" unfolding z_def using y_props by auto
ultimately have z_in_classes: "z ∈ classes k t j" unfolding classes_def by blast
have "y 0 ≠ t"
proof-
from that have "0 ∈ {..<k + 1 - j}" by simp
then show "y 0 ≠ t" using y_props by blast
qed
then have tr: "y 0 < t" using y_prop classes_subset_cube[of "k+1" t j] unfolding cube_def by fastforce
have "(λg ∈ {..<1}. y g) ∈ cube 1 (t+1)"
using y_prop classes_subset_cube[of "k+1" t j] cube_restrict[of 1 "(k+1)" y "t+1"] assms(2) by auto
then have "T y = T' (λg ∈ {..<1}. y g) z" using y_prop classes_subset_cube[of "k+1" t j]
unfolding T_def z_def by auto
also have " ... = join (L_line ((λg ∈ {..<1}. y g) 0)) (S z) n m"
unfolding T'_def
using ‹(λg ∈ {..<1}. y g) ∈ cube 1 (t+1)› ‹z ∈ cube k (t+1)›
by auto
also have " ... = join (L_line (y 0)) (S z) n m" by simp
also have " ... ∈ T_class j" using tr z_in_classes that unfolding T_class_def by force
finally show "x ∈ T_class j" using y_prop by simp
qed
qed
text ‹The core case $i \leq k$. The case $i = k+1$ is trivial since $k+1$ has only one point.›
have "χ x = χ y ∧ χ x < r" if a: "i ≤ k" "x ∈ T ` classes (k+1) t i"
"y ∈ T ` classes (k+1) t i" for i x y
proof-
from a have *: "T ` classes (k+1) t i = T_class i" by (simp add: classprop)
then have "x ∈ T_class i " using that by simp
moreover have **: "T_class i = {join (L_line l) s n m | l s . l ∈ {..<t} ∧ s ∈ S ` (classes k t i)}"
using a unfolding T_class_def by simp
ultimately obtain xs xi where xdefs: "x = join (L_line xi) xs n m ∧ xi < t ∧ xs ∈ S ` (classes k t i)"
by blast
from * ** obtain ys yi where ydefs: "y = join (L_line yi) ys n m ∧ yi < t ∧ ys ∈ S ` (classes k t i)"
using a by auto
have "(L_line xi) ∈ cube n (t+1)" using L_line_base_prop xdefs by simp
moreover have "xs ∈ cube m (t+1)"
using xdefs S_prop subspace_elems_embed imageE image_subset_iff mem_Collect_eq
unfolding layered_subspace_def classes_def by blast
ultimately have AA1: "χ x = χL (L_line xi) xs" using xdefs unfolding χL_def by simp
have "(L_line yi) ∈ cube n (t+1)" using L_line_base_prop ydefs by simp
moreover have "ys ∈ cube m (t+1)"
using ydefs S_prop subspace_elems_embed imageE image_subset_iff mem_Collect_eq
unfolding layered_subspace_def classes_def by blast
ultimately have AA2: "χ y = χL (L_line yi) ys" using ydefs unfolding χL_def by simp
have "∀s<t. ∀l < t. χL_s (L (SOME p. p∈cube 1 (t+1) ∧ p 0 = s))
= χL_s (L (SOME p. p∈cube 1 (t+1) ∧ p 0 = l))" using
dim1_layered_subspace_mono_line[of t L n s χL_s] L_prop assms(1) by blast
then have key_aux: "χL_s (L_line s) = χL_s (L_line l)" if "s ∈ {..<t}" "l ∈ {..<t}" for s l
using that unfolding L_line_def
by (metis (no_types, lifting) add.commute
lessThan_iff less_Suc_eq plus_1_eq_Suc restrict_apply)
have key: "χL (L_line s) = χL (L_line l)" if "s < t" "l < t" for s l
proof-
have L1: "χL (L_line s) ∈ cube m (t + 1) →⇩E {..<r}" unfolding χL_def
using A L_line_base_prop ‹s < t› by simp
have L2: "χL (L_line l) ∈ cube m (t + 1) →⇩E {..<r}" unfolding χL_def
using A L_line_base_prop ‹l < t› by simp
have "φ (χL (L_line s)) = χL_s (L_line s)" unfolding χL_s_def
using ‹s < t› L_line_base_prop by simp
also have " ... = χL_s (L_line l)" using key_aux ‹s <t› ‹l < t› by blast
also have " ... = φ (χL (L_line l))" unfolding χL_s_def using L_line_base_prop ‹l<t›
by simp
finally have "φ (χL (L_line s)) = φ (χL (L_line l))" by simp
then show "χL (L_line s) = χL (L_line l)"
using φ_prop L_line_base_prop L1 L2 unfolding bij_betw_def inj_on_def by blast
qed
then have "χL (L_line xi) xs = χL (L_line 0) xs" using xdefs assms(1) by metis
also have " ... = χS xs" unfolding χS_def χL_def using xdefs L_line_base_prop by auto
also have " ... = χS ys" using xdefs ydefs layered_eq_classes[of S k m t r χS] S_prop a by blast
also have " ... = χL (L_line 0) ys" unfolding χS_def χL_def using xdefs L_line_base_prop
by auto
also have " ... = χL (L_line yi) ys" using ydefs key assms(1) by metis
finally have core_prop: "χL (L_line xi) xs = χL (L_line yi) ys" by simp
then have "χ x = χ y" using AA1 AA2 by simp
then show " χ x = χ y ∧ χ x < r"
using xdefs AA1 key assms(1) A
‹L_line xi ∈ cube n (t + 1)› ‹xs ∈ cube m (t + 1)› by blast
qed
then have "∃c<r. ∀x ∈ T ` classes (k+1) t i. χ x = c" if "i ≤ k" for i
using that assms(5) by blast
moreover have "∃c<r. ∀x ∈ T ` classes (k+1) t (k+1). χ x = c"
proof -
have "∀x ∈ classes (k+1) t (k+1). ∀u < k + 1. x u = t" unfolding classes_def by auto
have "(λu. t) ` {..<k + 1} ⊆ {..<t + 1}" by auto
then have "∃!y ∈ cube (k+1) (t+1). (∀u < k + 1. y u = t)"
using PiE_uniqueness[of "(λu. t)" "{..<k+1}" "{..<t+1}"] unfolding cube_def by auto
then have "∃!y ∈ classes (k+1) t (k+1). (∀u < k + 1. y u = t)"
unfolding classes_def using classes_subset_cube[of "k+1" t "k+1"] by auto
then have "∃!y. y ∈ classes (k+1) t (k+1)"
using ‹∀x ∈ classes (k+1) t (k+1). ∀u < k + 1. x u = t› by auto
have "∃c<r. ∀y ∈ classes (k+1) t (k+1). χ (T y) = c"
proof -
have "∀y ∈ classes (k+1) t (k+1). T y ∈ cube (n+m) (t+1)" using T_prop classes_subset_cube
by blast
then have "∀y ∈ classes (k+1) t (k+1). χ (T y) < r" using χ_prop
unfolding n_def d_def using M'_prop by auto
then show "∃c<r. ∀y ∈ classes (k+1) t (k+1). χ (T y) = c"
using ‹∃!y. y ∈ classes (k+1) t (k+1)› by blast
qed
then show "∃c<r. ∀x ∈ T ` classes (k+1) t (k+1). χ x = c" by blast
qed
ultimately have "∃c<r. ∀x ∈ T ` classes (k+1) t i. χ x = c" if "i ≤ k + 1" for i
using that by (metis Suc_eq_plus1 le_Suc_eq)
then have "∃c<r. ∀x ∈ classes (k+1) t i. χ (T x) = c" if "i ≤ k + 1" for i
using that by simp
then have "layered_subspace T (k+1) (n + m) t r χ" using subspace_T that(1) ‹n + m = M'›
unfolding layered_subspace_def by blast
then show ?thesis using ‹n + m = M'› by blast
qed
then show ?thesis unfolding lhj_def
using m_props
exI[of "λM. ∀M'≥M. ∀χ. χ ∈ cube M' (t + 1)
→⇩E {..<r} ⟶ (∃S. layered_subspace S (k + 1) M' t r
χ)" m]
by blast
qed
theorem hj_imp_lhj:
fixes k
assumes "⋀r'. hj r' t"
shows "lhj r t k"
proof (induction k arbitrary: r rule: less_induct)
case (less k)
consider "k = 0" | "k = 1" | "k ≥ 2" by linarith
then show ?case
proof (cases)
case 1
then show ?thesis using dim0_layered_subspace_ex unfolding lhj_def by auto
next
case 2
then show ?thesis
proof (cases "t > 0")
case True
then show ?thesis using hj_imp_lhj_base[of "t"] assms 2 by blast
next
case False
then show ?thesis using assms unfolding hj_def lhj_def cube_def by fastforce
qed
next
case 3
note less
then show ?thesis
proof (cases "t > 0 ∧ r > 0")
case True
then show ?thesis using hj_imp_lhj_step[of t "k-1" r]
using assms less.IH 3 One_nat_def Suc_pred by fastforce
next
case False
then consider "t = 0" | "t > 0 ∧ r = 0" | "t = 0 ∧ r = 0" by fastforce
then show ?thesis
proof cases
case 1
then show ?thesis using assms unfolding hj_def lhj_def cube_def by fastforce
next
case 2
then obtain N where N_props: "N > 0" "∀N'≥N. ∀χ ∈ cube N' t
→⇩E {..<r}. (∃L c. c < r ∧ is_line L N' t ∧ (∀y
∈ L ` {..<t}. χ y = c))" using assms[of r] unfolding hj_def by force
have "cube N' (t + 1) →⇩E {..<r} = {}" if "N' ≥ N" for N'
proof-
have "cube N' t ≠ {}" using N_props(2) that 2 by fastforce
then have "cube N' (t + 1) ≠ {}" using cube_subset[of N' t] by blast
then show ?thesis using 2 by blast
qed
then show ?thesis unfolding lhj_def using N_props(1) by blast
next
case 3
then have "(∃L c. c < r ∧ is_line L N' t ∧ (∀y ∈ L ` {..<t}. χ y = c))
⟹ False" for N' χ by blast
then have False using assms 3 unfolding hj_def cube_def by fastforce
then show ?thesis by blast
qed
qed
qed
qed
subsection ‹Theorem 5›
text ‹We provide a way to construct a monochromatic line in $C^n_{t + 1}$ from a $k$-dimensional $k$-coloured
layered subspace ‹S› in $C^n_{t + 1}$.
The idea is to rely on the fact that there are $k+1$ classes in ‹S›, but only $k$ colours. It thus follows
from the Pigeonhole Principle that two classes must share the same colour. The way classes are defined allows for a
straightforward construction of a line with points only from those two classes. Thus we have our monochromatic
line.›
theorem layered_subspace_to_mono_line:
assumes "layered_subspace S k n t k χ"
and "t > 0"
shows "(∃L. ∃c<k. is_line L n (t+1) ∧ (∀y ∈ L ` {..<t+1}. χ y = c))"
proof-
define x where "x ≡ (λi∈{..k}. λj∈{..<k}. (if j < k - i then 0 else t))"
have A: "x i ∈ cube k (t + 1)" if "i ≤ k" for i using that unfolding cube_def x_def by simp
then have "S (x i) ∈ cube n (t+1)" if "i ≤ k" for i using that assms(1)
unfolding layered_subspace_def is_subspace_def by fast
have "χ ∈ cube n (t + 1) →⇩E {..<k}" using assms unfolding layered_subspace_def by linarith
then have "χ ` (cube n (t+1)) ⊆ {..<k}" by blast
then have "card (χ ` (cube n (t+1))) ≤ card {..<k}"
by (meson card_mono finite_lessThan)
then have *: "card (χ ` (cube n (t+1))) ≤ k" by auto
have "k > 0" using assms(1) unfolding layered_subspace_def by auto
have "inj_on x {..k}"
proof -
have *:"x i1 (k - i2) ≠ x i2 (k - i2)" if "i1 ≤ k" "i2 ≤ k" "i1 ≠ i2" "i1 < i2" for i1 i2
using that assms(2) unfolding x_def by auto
have "∃j<k. x i1 j ≠ x i2 j" if "i1 ≤ k" "i2 ≤ k" "i1 ≠ i2" for i1 i2
proof (cases "i1 ≤ i2")
case True
then have "k - i2 < k"
using ‹0 < k› that(3) by linarith
then show ?thesis using that *
by (meson True nat_less_le)
next
case False
then have "i2 < i1" by simp
then show ?thesis using that *[of i2 i1] ‹k > 0›
by (metis diff_less gr_implies_not0 le0 nat_less_le)
qed
then have "x i1 ≠ x i2" if "i1 ≤ k" "i2 ≤ k" "i1 ≠ i2" "i1 < i2" for i1 i2 using that
by fastforce
then show ?thesis unfolding inj_on_def by (metis atMost_iff linorder_cases)
qed
then have "card (x ` {..k}) = card {..k}" using card_image by blast
then have B: "card (x ` {..k}) = k+1" by simp
have "x ` {..k} ⊆ cube k (t+1)" using A by blast
then have "S ` x ` {..k} ⊆ S ` cube k (t+1)" by fast
also have "... ⊆ cube n (t+1)"
by (meson assms(1) layered_subspace_def subspace_elems_embed)
finally have "S ` x ` {..k} ⊆ cube n (t+1)" by blast
then have "χ ` S ` x ` {..k} ⊆ χ ` cube n (t+1)" by auto
then have "card (χ ` S ` x ` {..k}) ≤ card (χ ` cube n (t+1))"
by (simp add: card_mono cube_def finite_PiE)
also have " ... ≤ k" using * by blast
also have " ... < k + 1" by auto
also have " ... = card {..k}" by simp
also have " ... = card (x ` {..k})" using B by auto
also have " ... = card (S ` x ` {..k})"
using subspace_inj_on_cube[of S k n "t+1"] card_image[of S "x ` {..k}"]
inj_on_subset[of S "cube k (t+1)" "x ` {..k}"] assms(1) ‹x ` {..k} ⊆ cube k (t + 1)›
unfolding layered_subspace_def by simp
finally have "card (χ ` S ` x ` {..k}) < card (S ` x ` {..k})" by blast
then have "¬inj_on χ (S ` x ` {..k})" using pigeonhole[of χ "S ` x ` {..k}"] by blast
then have "∃a b. a ∈ S ` x ` {..k} ∧ b ∈ S ` x ` {..k} ∧ a ≠ b ∧ χ a =
χ b" unfolding inj_on_def by auto
then obtain ax bx where ab_props: "ax ∈ S ` x ` {..k} ∧ bx ∈ S ` x ` {..k} ∧ ax ≠ bx ∧
χ ax = χ bx" by blast
then have "∃u v. u ∈ {..k} ∧ v ∈ {..k} ∧ u ≠ v ∧ χ (S (x u)) = χ (S (x
v))" by blast
then obtain u v where uv_props: "u ∈ {..k} ∧ v ∈ {..k} ∧ u < v ∧ χ (S (x u))
= χ (S (x v))" by (metis linorder_cases)
let ?f = "λs. (λi ∈ {..<k}. if i < k - v then 0 else (if i < k - u then s else t))"
define y where "y ≡ (λs ∈ {..t}. S (?f s))"
have line1: "?f s ∈ cube k (t+1)" if "s ≤ t" for s unfolding cube_def using that by auto
have f_cube: "?f j ∈ cube k (t+1)" if "j < t+1" for j using line1 that by simp
have f_classes_u: "?f j ∈ classes k t u" if j_prop: "j < t" for j
using that j_prop uv_props f_cube unfolding classes_def by auto
have f_classes_v: "?f j ∈ classes k t v" if j_prop: "j = t" for j
using that j_prop uv_props assms(2) f_cube unfolding classes_def by auto
obtain B f where Bf_props: "disjoint_family_on B {..k}" "⋃(B ` {..k}) = {..<n}" "({} ∉ B ` {..<k})"
"f ∈ (B k) →⇩E {..<t+1}" "S ∈ (cube k (t+1)) →⇩E (cube n (t+1))"
"(∀y ∈ cube k (t+1). (∀i ∈ B k. S y i = f i) ∧ (∀j<k. ∀i ∈ B j.
(S y) i = y j))"
using assms(1) unfolding layered_subspace_def is_subspace_def by auto
have "y ∈ {..<t+1} →⇩E cube n (t+1)" unfolding y_def using line1 ‹S ` cube k (t + 1)
⊆ cube n (t + 1)› by auto
moreover have "(∀u<t+1. ∀v<t+1. y u j = y v j) ∨ (∀s<t+1. y s j = s)"
if j_prop: "j<n" for j
proof-
show "(∀u<t+1. ∀v<t+1. y u j = y v j) ∨ (∀s<t+1. y s j = s)"
proof -
consider "j ∈ B k" | "∃ii<k. j ∈ B ii" using Bf_props(2) j_prop
by (metis UN_E atMost_iff le_neq_implies_less lessThan_iff)
then have "y a j = y b j ∨ y s j = s" if "a < t + 1" "b < t +1" "s < t +1" for a b s
proof cases
case 1
then have "y a j = S (?f a) j" using that(1) unfolding y_def by auto
also have " ... = f j" using Bf_props(6) f_cube 1 that(1) by auto
also have " ... = S (?f b) j" using Bf_props(6) f_cube 1 that(2) by auto
also have " ... = y b j" using that(2) unfolding y_def by simp
finally show ?thesis by simp
next
case 2
then obtain ii where ii_prop:" ii < k ∧ j ∈ B ii" by blast
then consider "ii < k - v" | "ii ≥ k - v ∧ ii < k - u" | "ii ≥ k - u ∧ ii < k" using not_less
by blast
then show ?thesis
proof cases
case 1
then have "y a j = S (?f a) j" using that(1) unfolding y_def by auto
also have " ... = (?f a) ii" using Bf_props(6) f_cube that(1) ii_prop by auto
also have " ... = 0" using 1 by (simp add: ii_prop)
also have " ... = (?f b) ii" using 1 by (simp add: ii_prop)
also have " ... = S (?f b) j" using Bf_props(6) f_cube that(2) ii_prop by auto
also have " ... = y b j" using that(2) unfolding y_def by auto
finally show ?thesis by simp
next
case 2
then have "y s j = S (?f s) j" using that(3) unfolding y_def by auto
also have " ... = (?f s) ii" using Bf_props(6) f_cube that(3) ii_prop by auto
also have " ... = s" using 2 by (simp add: ii_prop)
finally show ?thesis by simp
next
case 3
then have "y a j = S (?f a) j" using that(1) unfolding y_def by auto
also have " ... = (?f a) ii" using Bf_props(6) f_cube that(1) ii_prop by auto
also have " ... = t" using 3 uv_props by auto
also have " ... = (?f b) ii" using 3 uv_props by auto
also have " ... = S (?f b) j" using Bf_props(6) f_cube that(2) ii_prop by auto
also have " ... = y b j" using that(2) unfolding y_def by auto
finally show ?thesis by simp
qed
qed
then show ?thesis by blast
qed
qed
moreover have "∃j < n. ∀s<t+1. y s j = s"
proof -
have "k > 0" using uv_props by simp
have "k - v < k" using uv_props by auto
have "k - v < k - u" using uv_props by auto
then have "B (k - v) ≠ {}" using Bf_props(3) uv_props by auto
then obtain j where j_prop: "j ∈ B (k - v) ∧ j < n" using Bf_props(2) uv_props by force
then have "y s j = s" if "s<t+1" for s
proof
have "y s j = S (?f s) j" using that unfolding y_def by auto
also have " ... = (?f s) (k - v)" using Bf_props(6) f_cube that j_prop ‹k - v < k› by fast
also have " ... = s" using that j_prop ‹k - v < k - u› by simp
finally show ?thesis .
qed
then show "∃j < n. ∀s<t+1. y s j = s" using j_prop by blast
qed
ultimately have Z1: "is_line y n (t+1)" unfolding is_line_def by blast
moreover
{
have k_colour: "χ e < k" if "e ∈ y ` {..<t+1}" for e
using ‹y ∈ {..<t+1} →⇩E cube n (t + 1)› ‹χ ∈ cube n (t + 1)
→⇩E {..<k}› that by auto
have "χ e1 = χ e2 ∧ χ e1 < k" if "e1 ∈ y ` {..<t+1}" "e2 ∈ y ` {..<t+1}" for e1 e2
proof
from that obtain i1 i2 where i_props: "i1 < t + 1" "i2 < t + 1" "e1 = y i1" "e2 = y i2" by blast
from i_props(1,2) have "χ (y i1) = χ (y i2)"
proof (induction i1 i2 rule: linorder_wlog)
case (le a b)
then show ?case
proof (cases "a = b")
case True
then show ?thesis by blast
next
case False
then have "a < b" using le by linarith
then consider "b = t" | "b < t" using le.prems(2) by linarith
then show ?thesis
proof cases
case 1
then have "y b ∈ S ` classes k t v"
proof -
have "y b = S (?f b)" unfolding y_def using ‹b = t› by auto
moreover have "?f b ∈ classes k t v" using ‹b = t› f_classes_v by blast
ultimately show "y b ∈ S ` classes k t v" by blast
qed
moreover have "x u ∈ classes k t u"
proof -
have "x u cord = t" if "cord ∈ {k - u..<k}" for cord using uv_props that unfolding x_def by simp
moreover
{
have "x u cord ≠ t" if "cord ∈ {..<k - u}" for cord
using uv_props that assms(2) unfolding x_def by auto
then have "t ∉ x u ` {..<k - u}" by blast
}
ultimately show "x u ∈ classes k t u" unfolding classes_def
using ‹x ` {..k} ⊆ cube k (t + 1)› uv_props by blast
qed
moreover have "x v ∈ classes k t v"
proof -
have "x v cord = t" if "cord ∈ {k - v..<k}" for cord using uv_props that unfolding x_def by simp
moreover
{
have "x v cord ≠ t" if "cord ∈ {..<k - v}" for cord
using uv_props that assms(2) unfolding x_def by auto
then have "t ∉ x v ` {..<k - v}" by blast
}
ultimately show "x v ∈ classes k t v" unfolding classes_def
using ‹x ` {..k} ⊆ cube k (t + 1)› uv_props by blast
qed
moreover have "χ (y b) = χ (S (x v))"
using assms(1) calculation(1, 3) unfolding layered_subspace_def by (metis imageE uv_props)
moreover have "y a ∈ S ` classes k t u"
proof -
have "y a = S (?f a)" unfolding y_def using ‹a < b› 1 by simp
moreover have "?f a ∈ classes k t u" using ‹a < b› 1 f_classes_u by blast
ultimately show "y a ∈ S ` classes k t u" by blast
qed
moreover have "χ (y a) = χ (S (x u))" using assms(1) calculation(2, 5)
unfolding layered_subspace_def by (metis imageE uv_props)
ultimately have "χ (y a) = χ (y b)" using uv_props by simp
then show ?thesis by blast
next
case 2
then have "a < t" using ‹a < b› less_trans by blast
then have "y a ∈ S ` classes k t u"
proof -
have "y a = S (?f a)" unfolding y_def using ‹a < t› by auto
moreover have "?f a ∈ classes k t u" using ‹a < t› f_classes_u by blast
ultimately show "y a ∈ S ` classes k t u" by blast
qed
moreover have "y b ∈ S ` classes k t u"
proof -
have "y b = S (?f b)" unfolding y_def using ‹b < t› by auto
moreover have "?f b ∈ classes k t u" using ‹b < t› f_classes_u by blast
ultimately show "y b ∈ S ` classes k t u" by blast
qed
ultimately have "χ (y a) = χ (y b)" using assms(1) uv_props unfolding layered_subspace_def
by (metis imageE)
then show ?thesis by blast
qed
qed
next
case (sym a b)
then show ?case by presburger
qed
then show "χ e1 = χ e2" using i_props(3,4) by blast
qed (use that(1) k_colour in blast)
then have Z2: "∃c < k. ∀e ∈ y ` {..<t+1}. χ e = c"
by (meson image_eqI lessThan_iff less_add_one)
}
ultimately show "∃L c. c < k ∧ is_line L n (t + 1) ∧ (∀y∈L ` {..<t + 1}. χ y = c)"
by blast
qed
subsection ‹Corollary 6›
corollary lhj_imp_hj:
assumes "(⋀r k. lhj r t k)"
and "t>0"
shows "(hj r (t+1))"
using assms(1)[of r r] assms(2) unfolding lhj_def hj_def using layered_subspace_to_mono_line[of _ r _ t] by metis
subsection ‹Main result›
subsubsection ‹Edge cases and auxiliary lemmas›
lemma single_point_line:
assumes "N > 0"
shows "is_line (λs∈{..<1}. λa∈{..<N}. 0) N 1"
using assms unfolding is_line_def cube_def by auto
lemma single_point_line_is_monochromatic:
assumes "χ ∈ cube N 1 →⇩E {..<r}" "N > 0"
shows "(∃c < r. is_line (λs∈{..<1}. λa∈{..<N}. 0) N 1 ∧ (∀i ∈
(λs∈{..<1}. λa∈{..<N}. 0) ` {..<1}. χ i = c))"
proof -
have "is_line (λs∈{..<1}. λa∈{..<N}. 0) N 1" using assms(2) single_point_line by blast
moreover have "∃c < r. χ ((λs∈{..<1}. λa∈{..<N}. 0) j) = c"
if "(j::nat) < 1" for j using assms line_points_in_cube calculation that unfolding cube_def by blast
ultimately show ?thesis by auto
qed
lemma hj_r_nonzero_t_0:
assumes "r > 0"
shows "hj r 0"
proof-
have "(∃L c. c < r ∧ is_line L N' 0 ∧ (∀y ∈ L ` {..<0::nat}. χ y = c))"
if "N' ≥ 1" "χ ∈ cube N' 0 →⇩E {..<r}" for N' χ using assms is_line_def that(1) by fastforce
then show ?thesis unfolding hj_def by auto
qed
text ‹Any cube over 1 element always has a single point, which also forms the only line in the cube. Since it's a
single point line, it's trivially monochromatic. We show the result for dimension 1.›
lemma hj_t_1: "hj r 1"
unfolding hj_def
proof-
let ?N = 1
have "∃L c. c < r ∧ is_line L N' 1 ∧ (∀y∈L ` {..<1}. χ y = c)" if "N' ≥ ?N" "χ ∈ cube N' 1 →⇩E {..<r}" for N' χ
using single_point_line_is_monochromatic[of χ N' r] that by force
then show "∃N>0. ∀N'≥N. ∀χ. χ ∈ cube N' 1 →⇩E {..<r} ⟶ (∃L c. c < r ∧ is_line L N' 1 ∧ (∀y∈L ` {..<1}. χ y = c))"
by blast
qed
subsubsection ‹Main theorem›
text ‹We state the main result \<^prop>‹hj r t›. The explanation for the choice of assumption is
offered subsequently.›
theorem hales_jewett:
assumes "¬(r = 0 ∧ t = 0)"
shows "hj r t"
using assms
proof (induction t arbitrary: r)
case 0
then show ?case using hj_r_nonzero_t_0[of r] by blast
next
case (Suc t)
then show ?case using hj_t_1[of r] hj_imp_lhj[of t] lhj_imp_hj[of t r] by auto
qed
text ‹We offer a justification for having excluded the special case $r = t = 0$ from the statement of the main
theorem ‹hales_jewett›. The exclusion is a consequence of the fact that colourings are defined as members
of the function set ‹cube n t →⇩E {..<r}›, which for $r = t = 0$ means there's a dummy
colouring \<^term>‹λx. undefined›, even though \<^prop>‹cube n 0 = {}› for $n > 0$.
Hence, in this case, no line exists at all (let alone one monochromatic under the aforementioned colouring). This means
\<^prop>‹hj 0 0 ⟹ False›---but only because of the quirky behaviour of the FuncSet
‹cube n t →⇩E {..<r}›. This could have been circumvented by letting colourings $\chi$ be
arbitrary functions constraint only by \<^prop>‹χ ` cube n t ⊆ {..<r}›. We avoided this in
order to have consistency with the cube's definition, for which FuncSets were crucial because the proof heavily relies
on arguments about the cardinality of the cube. he constraint \<^prop>‹x ` {..<n} ⊆ {..<t}› for
elements ‹x› of $C^n_t$ would not have sufficed there, as there are infinitely many functions over the
naturals satisfying it.›
end