Theory Cube_Dissection

theory Cube_Dissection
  imports Complex_Main "HOL-Library.Disjoint_Sets" "HOL-Library.Infinite_Set"
begin

text "Proof that a cube can't be dissected into a finite number of subcubes of different size
This formalization is heavily inspired by the Lean proof of the same fact,  \<^cite>‹leanproof›.
One goal of this project, is that by restricting to cubes of dimension 3 the logic will
be easier to follow"

section "Basic definitions"
subsection "point and cube definitions"
record point = px:: real py::real pz::real
record cube = point:: point width::real
datatype axis = x | y | z
abbreviation "coordinate ≡ case_axis px py pz"

abbreviation is_valid :: "cube ⇒ bool" where "is_valid c ≡ (width c > 0)"

text "Min value of cube along given axis"
hide_const (open) min
abbreviation min :: "axis ⇒ cube ⇒ real" where "min ax c ≡ coordinate ax (point c)"

text "Max value (supremum) along given axis"
hide_const (open) max
abbreviation max :: "axis ⇒ cube ⇒ real" where "max ax c ≡ min ax c  + width c"

text "Sides of a cube. Half-open intervals, so that a dissection both is a cover, and consists of disjoint cubes"
abbreviation side :: "axis ⇒ cube ⇒ real set" where
  "side ax c ≡ {min ax c ..< max ax c}"

text "Sets of points generated from cubes"
definition to_set :: "cube ⇒ point set" where
  "to_set c = {p. px p ∈ side x c ∧ py p ∈ side y c ∧ pz p ∈ side z c}"
definition bot :: "cube ⇒ point set" where
  "bot c = {p. px p ∈ side x c ∧ py p ∈ side y c ∧ pz p = min z c}"
definition top :: "cube ⇒ point set" where
  "top c = {p. px p ∈ side x c ∧ py p ∈ side y c ∧ pz p = max z c}"

text "Moves a cube its width down (so top face to bottom face)"
definition shift_down :: "cube ⇒ cube" where 
  "shift_down c = c ⦇ point := point c ⦇ pz := min z c - width c  ⦈ ⦈"


subsection "Calculations with sets from cubes"
text "A bunch of statements we need about how cubes can be compared by \<^term>‹side›"
lemma top_shift_down_eq_bot: "top (shift_down c) = bot c"
  unfolding top_def bot_def shift_down_def by simp

text "Sets not empty"
lemma non_empty: "is_valid c ⟹ to_set c ≠ {}"
  unfolding to_set_def by force
lemma top_non_empty: "is_valid c ⟹ top c ≠ {}"
  unfolding top_def by (auto intro!: exI[of _ "point c ⦇ pz := max z c ⦈"])

text "\<^term>‹min› of a cube is in corresponding \<^term>‹side›"
lemma min_in_side: "is_valid c ⟹ min ax c ∈ side ax c"
  by simp

lemma min_ne_max: "is_valid c ⟹ min ax c ≠ max ax c"
  by simp
lemma min_lt_max: "is_valid c ⟹ min ax c < max ax c"
  by simp

lemma bot_subset: "bot c ⊆ to_set c"
  unfolding bot_def to_set_def by(auto)


subsubsection "Point membership"
text "Points in a cube's set, by looking at membership of \<^term>‹side›"
lemma in_set_by_side: "p ∈ to_set c ⟷
  px p ∈ side x c ∧ py p ∈ side y c ∧ pz p ∈ side z c"
  by(cases p, simp add: to_set_def)
lemma in_set_by_side_2: "⦇px=x0, py=y0, pz=z0⦈ ∈ to_set c ⟷
  x0 ∈ side x c ∧ y0 ∈ side y c ∧ z0 ∈ side z c"
  by(simp add: to_set_def)

lemma in_bot_by_side: "p ∈ bot c ⟷
  px p ∈ side x c ∧ py p ∈ side y c ∧ pz p = min z c"
  by(simp add: bot_def)
lemma in_bot_by_side_2: "⦇px=x0, py=y0, pz=z0⦈ ∈ bot c ⟷
  x0 ∈ side x c ∧ y0 ∈ side y c ∧ z0 = min z c"
  by(simp add: in_bot_by_side)

lemma in_top_by_side: "p ∈ top c ⟷
  px p ∈ side x c ∧ py p ∈ side y c ∧ pz p = max z c"
  by(cases p, auto simp add: top_def)
lemma in_top_by_side_2: "⦇px=x0, py=y0, pz=z0⦈ ∈ top c ⟷
  x0 ∈ side x c ∧ y0 ∈ side y c ∧ z0 = max z c"
  by(simp add: top_def)

lemma all_point_iff: "(∀p. P p) ⟷ (∀x1 y1 z1. P ⦇px = x1, py = y1, pz = z1⦈)"
  by (metis point.cases)

text "Intersection by \<^term>‹side›"
lemma set_intersect_by_side: "to_set c1 ∩ to_set c2 ≠ {} ⟷
  side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {} ∧ side z c1 ∩ side z c2 ≠ {}"
  unfolding set_eq_iff all_point_iff using in_set_by_side_2 by blast

lemma bot_intersect_by_side: "bot c1 ∩ bot c2 ≠ {} 
  ⟷ side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {} ∧ min z c1 = min z c2"
proof(intro iffI)
  assume "bot c1 ∩ bot c2 ≠ {}"
  thus  "side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {} ∧ min z c1 = min z c2" 
    using in_bot_by_side by fastforce
next
  assume "side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {} ∧ min z c1 = min z c2" 
  thus "bot c1 ∩ bot c2 ≠ {}" using in_bot_by_side_2 by blast
qed

lemma bot_top_intersect_by_side: "bot c1 ∩ top c2 ≠ {} 
  ⟷ side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {} ∧ min z c1 = max z c2"
proof(intro iffI)
  assume "bot c1 ∩ top c2 ≠ {}"
  thus  "side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {} ∧ min z c1 = max z c2" 
    using in_bot_by_side in_top_by_side by fastforce
next
  assume "side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {} ∧ min z c1 = max z c2" 
  thus "bot c1 ∩ top c2 ≠ {}" using in_bot_by_side_2 in_top_by_side_2 by blast
qed


subsubsection "Cubes subset of each other, by \<^term>‹side›"
lemma set_subset_by_side: "to_set c1 ⊆ to_set c2 ⟷
  side x c1 ⊆ side x c2 ∧ side y c1 ⊆ side y c2 ∧ side z c1 ⊆ side z c2"
  unfolding subset_eq Ball_def all_point_iff in_set_by_side by fastforce
lemma set_eq_by_side: "to_set c1 = to_set c2 ⟷
  side x c1 = side x c2 ∧ side y c1 = side y c2 ∧ side z c1 = side z c2"
  using set_subset_by_side by fast

lemma bot_eq_by_side: "is_valid c1 ⟹ bot c1 = bot c2 ⟷
side x c1 = side x c2 ∧ side y c1 = side y c2 ∧ min z c1 = min z c2"
  unfolding bot_def set_eq_iff all_point_iff by fastforce


lemma bot_top_subset_by_side: "is_valid c1 ⟹ bot c1 ⊆ top c2 ⟷
side x c1 ⊆ side x c2 ∧ side y c1 ⊆ side y c2 ∧ min z c1 = max z c2"
  unfolding top_def bot_def subset_eq Ball_def all_point_iff by fastforce
lemma bot_top_eq_by_side: "is_valid c1 ⟹ bot c1 = top c2 ⟷
side x c1 = side x c2 ∧ side y c1 = side y c2 ∧ min z c1 = max z c2"
  unfolding top_def bot_def set_eq_iff Ball_def all_point_iff by fastforce

lemma width_eq_if_side_eq: "⟦is_valid c1; side ax c1 = side ax c2⟧ ⟹ width c1 = width c2"
  by(simp add:Ico_eq_Ico)

text "\<^term>‹to_set› is injective"
lemma to_set_inj: 
  assumes "is_valid c1" "to_set c1 = to_set c2" 
  shows "c1 = c2"
proof -
  from assms(2) have *: "side x c1 = side x c2" "side y c1 = side y c2" "side z c1 = side z c2" 
    by(metis set_eq_by_side)+
  hence "min x c1 = min x c2" "min y c1 = min y c2" "min z c1 = min z c2"
    by(meson assms(1) Ico_eq_Ico less_add_same_cancel1)+
  hence "point c1 = point c2" by simp
  moreover from * have "width c1 = width c2" by(metis assms(1) width_eq_if_side_eq)
  ultimately show "c1 = c2" by simp
qed

text "\<^term>‹bot› is also injective"
lemma bot_inj: assumes "is_valid c1" "bot c1 = bot c2" shows "c1 = c2"
proof -
  from assms have "width c1 = width c2" by(metis assms bot_eq_by_side width_eq_if_side_eq)
  hence "to_set c1 = to_set c2" using assms bot_eq_by_side set_eq_by_side by auto
  thus "c1 = c2" by(metis assms(1) to_set_inj)
qed


section "Cubing"
text "We in this section introduce a dissection C of the unit cube"

text "The cube we show there is no dissection of"
definition unit_cube where "unit_cube = ⦇ point=⦇px=0, py=0, pz=0⦈, width=1⦈"

lemma min_unit_cube_0: "min ax unit_cube = 0"
  by(metis unit_cube_def axis.exhaust axis.simps(7-9) cube.select_convs(1) point.select_convs(1-3))

lemma unit_cube_valid[simp]: "is_valid unit_cube"
  by(simp add: unit_cube_def)

text "What we want to show doesn't exist. \<^term>‹C› is a set of cubes which satisfy:
▸ All cubes are valid (width > 0)
▸ All cubes a disjoint
▸ The union of the cubes in \<^term>‹C› equal \<^term>‹unit_cube› (hence, all cubes are contained in \<^term>‹unit_cube›)
▸ All cubes in \<^term>‹C› have different width
▸ There are at least two cubes in \<^term>‹C›
▸ There are a finite number of cubes in \<^term>‹C›"
definition is_dissection :: "cube set ⇒ bool" where
  "is_dissection C ⟷ 
  (∀ c ∈ C. is_valid c)
  ∧ disjoint (image to_set C)
  ∧ ⋃(image to_set C) = to_set unit_cube
  ∧ inj_on width C ― ‹All cubes are of different size›
  ∧ card C ≥ 2  ― ‹At least two cubes›
  ∧ finite C"

text "From now on, C is some fixed dissection of \<^term>‹unit_cube›, and 'dissection' refers to this fact" 
context fixes C assumes dissection: "is_dissection C"
begin

subsection "Properties of \<^term>‹is_dissection›"
lemma valid_if_dissection[simp]: "c ∈ C ⟹ is_valid c"
  using dissection unfolding is_dissection_def by fast 

lemma side_unit_cube: 
  "side ax unit_cube = {0..<1}"
  by(metis add.commute add.right_neutral cube.select_convs(2) min_unit_cube_0 unit_cube_def)

lemma subset_unit_cube_if_dissection: "c ∈ C ⟹ to_set c ⊆ to_set unit_cube"
  using dissection unfolding is_dissection_def to_set_def by fast

lemma subset_unit_cube_by_side:
  "c ∈ C ⟹ side ax c ⊆ {0..<1}"
  by(metis(full_types)subset_unit_cube_if_dissection set_subset_by_side side_unit_cube axis.exhaust)

lemma eq_iff_intersect: "⟦c1 ∈ C; c2 ∈ C⟧ ⟹ c1 = c2 ⟷ to_set c1 ∩ to_set c2 ≠ {}"
  using dissection unfolding is_dissection_def disjoint_def
  by (metis image_eqI inf.idem non_empty to_set_inj)

text "Whenever we have a point in \<^term>‹unit_cube›, there exists a (unique) cube in \<^term>‹C› containing that
point"
lemma obtain_cube: "p ∈ to_set unit_cube ⟹ ∃ c ∈ C. p ∈ to_set c"
  using dissection unfolding is_dissection_def by blast

text "If the top of \<^term>‹c› doesn't touch the top of \<^term>‹unit_cube›, then top of \<^term>‹c› must 
be covered by bottoms of cubes in \<^term>‹C›"
lemma top_cover_by_bot:
  assumes "c ∈ C" "max z c < 1"
  shows "top c ⊆ ⋃(image bot C)"
proof(intro subsetI)
  fix p assume p_in_top: "p ∈ top c"
  from assms(1) have "side x c ⊆ {0..<1}" "side y c ⊆ {0..<1}" "side z c ⊆ {0..<1}" 
    using subset_unit_cube_by_side by blast+
  with assms(2) p_in_top have "px p ∈ {0..<1}" "py p ∈ {0..<1}" "pz p ∈ {0..<1}" 
    by(simp add: in_top_by_side)+
  hence "p ∈ to_set unit_cube" using in_set_by_side side_unit_cube by blast
  then obtain c' where "c' ∈ C" "p ∈ to_set c'" by(metis obtain_cube)
  moreover have "p ∉ to_set c" using p_in_top in_top_by_side in_set_by_side by simp
  ultimately have "c' ≠ c" by metis
  hence "to_set c' ∩ to_set c = {}" by(metis assms(1) ‹c' ∈ C›  eq_iff_intersect)
  have "p ∈ bot c'"
  proof(rule ccontr)
    assume "p ∉ bot c'"
    hence "min z c' < pz p" "pz p < max z c'" using ‹p ∈ to_set c'›
      by(simp_all add: in_set_by_side in_bot_by_side)
    hence "side z c' ∩ side z c ≠ {}" using ‹p ∈ top c› by(simp add: in_top_by_side)
    moreover have "side x c ∩ side x c' ≠ {}" "side y c ∩ side y c' ≠ {}"
      using ‹p ∈ top c› ‹p ∈ to_set c'› by(simp_all add: in_top_by_side in_set_by_side assms)
    ultimately have "to_set c' ∩ to_set c ≠ {}" using set_intersect_by_side by simp
    thus "False" using ‹to_set c' ∩ to_set c = {}› by metis
  qed
  thus "p ∈ ⋃(image bot C)" using ‹c' ∈ C› by blast
qed


section "Hole"
text "A hole \<^term>‹h› is a special kind of cube, where any cube whose bottom 'touches' the top of \<^term>‹v›
must in fact have its bottom contained in the top of \<^term>‹v›. If \<^term>‹h ∈ C›, then this happens because 
all the other cubes surrounding \<^term>‹h› go up taller, forming a hole on top of \<^term>‹v›.
Note that we don't require that \<^term>‹h ∈ C›, but this is only so we can prove that \<^term>‹unit_cube›
shifted down by 1 is a hole - all other holes will in fact lie in \<^term>‹C›. The concept of a hole is
inspired by the 'Valley' definition from \<^cite>‹leanproof›"
subsection "Definitions"
definition is_hole :: "cube ⇒ bool" where
  "is_hole h ⟷
    is_valid h
    ∧ top h ⊆ ⋃(image bot C)
    ∧ (∀ c ∈ C .  bot c ∩ top h ≠ {} ⟶ bot c ⊆ top h)
    ― ‹\<^term>‹v› could be a cube in \<^term>‹C› (and most often is), but any other cube must be different width.
        Also, this assumption is not actually needed (as it follows from \<^term>‹v›, \<^term>‹c ∈ C›), 
        but without it we have to do a special-case proof for the bottom of the \<^term>‹unit_cube››
    ∧ (∀ c ∈ C . c ≠ h ⟶ width c ≠ width h)"

text "Subset of \<^term>‹C› which are on a given hole h"
definition is_on_hole :: "cube ⇒ cube ⇒ bool" where
  "is_on_hole h c ⟷ bot c ⊆ top h"
definition filter_on_hole :: "cube ⇒ cube set" where
  "filter_on_hole h = Set.filter (is_on_hole h) C"


subsection "Properties of a hole"
text "Terminology: 
  'on hole' means cube \<^term>‹c› with:  \<^term>‹bot c ⊆ top h›. 
  'in hole' means point \<^term>‹p› with: \<^term>‹p ∈ top h› h"

text "\<^term>‹filter_on_hole h ⊆ C›"
lemma dissection_if_on_hole[simp]: "c ∈ filter_on_hole h ⟹ c ∈ C"
  unfolding filter_on_hole_def by simp

text "Holes, and cubes on them, are valid"
lemma valid_if_hole[simp]: "is_hole h ⟹ is_valid h"
  by(metis is_hole_def)
lemma valid_if_on_hole[simp]: "c ∈ filter_on_hole h ⟹ is_valid c"
  by simp

lemma on_hole_finite: "is_hole h ⟹ finite (filter_on_hole h)"
  by (metis dissection is_dissection_def filter_on_hole_def finite_filter )

lemma on_hole_if_in_filter_on_hole: "c ∈ filter_on_hole h ⟹ is_on_hole h c"
  unfolding filter_on_hole_def by simp

lemma on_hole_cover: assumes "is_hole h" shows "top h ⊆ ⋃(image bot (filter_on_hole h))"
proof
  fix p assume "p ∈ top h"
  then obtain "c" where "c ∈ C" "p ∈ bot c" using assms unfolding is_hole_def by blast
  with ‹p ∈ top h› have "bot c ⊆ top h" using assms unfolding is_hole_def by blast
  hence "c ∈ filter_on_hole h"
    by (metis  ‹c ∈ C› filter_on_hole_def is_on_hole_def member_filter)
  with ‹p ∈ bot c› show "p ∈ ⋃(image bot(filter_on_hole h))" by blast
qed

text "Whenever we have a point \<^term>‹p› in the top of a hole \<^term>‹h›, there exists a (unique) cube 
\<^term>‹c ∈ filter_on_hole h›, such that \<^term>‹p ∈ bot c›"
lemma obtain_cube_if_in_hole: "⟦is_hole h; p ∈ top h⟧ 
  ⟹ ∃c ∈ filter_on_hole h . p ∈ bot c"
  using on_hole_cover by blast

lemma on_hole_inj_on_width: "is_hole h ⟹ inj_on width (filter_on_hole h)"
  using dissection_if_on_hole inj_on_subset dissection
    is_dissection_def subset_iff by metis


subsection "Properties of cubes on a hole"
lemma neq_hole_if_on_hole: "c ∈ filter_on_hole h ⟹ c ≠ h"
  using valid_if_on_hole min_ne_max bot_top_subset_by_side is_on_hole_def 
    on_hole_if_in_filter_on_hole by blast

lemma subset_if_on_hole: "c ∈ filter_on_hole h ⟹ bot c ⊆ top h"
  unfolding is_hole_def filter_on_hole_def is_on_hole_def by simp

lemma side_subset_if_on_hole: "⟦c ∈ filter_on_hole h; ax ∈ {x,y}⟧ ⟹ side ax c ⊆ side ax h"
  using bot_top_subset_by_side subset_if_on_hole by auto

lemma min_z_eq_max_z_hole_if_on_hole:
  "c ∈ filter_on_hole h ⟹ min z c =  max z h"
  using subset_if_on_hole  by(simp add: bot_top_subset_by_side)

lemma z_eq_if_on_hole:
  "⟦c1 ∈ filter_on_hole h; c2 ∈ filter_on_hole h⟧ ⟹ min z c1 = min z c2"
  using min_z_eq_max_z_hole_if_on_hole by simp

text "Do not need to care about \<^term>‹z›-coordinate"
lemma eq_iff_side_eq_if_on_hole: "⟦c1 ∈ filter_on_hole h; c2 ∈ filter_on_hole h⟧ 
  ⟹ c1 = c2 ⟷ side x c1 = side x c2 ∧ side y c1 = side y c2"
  by(meson valid_if_on_hole z_eq_if_on_hole bot_eq_by_side bot_inj)

text "Disjointness-lemmas:"
lemma eq_iff_bot_intersect_if_on_hole: 
  assumes "c1 ∈ filter_on_hole h" "c2 ∈ filter_on_hole h"
  shows "c1 = c2 ⟷ bot c1 ∩ bot c2 ≠ {}"
proof -
  from assms have "c1 = c2 ⟷ to_set c1 ∩ to_set c2 ≠ {}" by(simp add: eq_iff_intersect)
  moreover have "min z c1 = min z c2" by(metis assms z_eq_if_on_hole)
  hence "to_set c1 ∩ to_set c2 ≠ {} ⟷ bot c1 ∩ bot c2 ≠ {}"
    using set_intersect_by_side bot_intersect_by_side bot_subset subsetD by blast
  ultimately show "c1 = c2 ⟷ bot c1 ∩ bot c2 ≠ {}" by blast
qed

lemma eq_iff_side_intersect_if_on_hole: 
  "⟦c1 ∈ filter_on_hole h; c2 ∈ filter_on_hole h⟧ 
  ⟹ c1 = c2 ⟷ side x c1 ∩ side x c2 ≠ {} ∧ side y c1 ∩ side y c2 ≠ {}"
  by(meson z_eq_if_on_hole eq_iff_bot_intersect_if_on_hole bot_intersect_by_side)

lemma width_on_hole_lt_width_hole: 
  assumes "is_hole h" "c ∈ filter_on_hole h" shows "width c < width h"
proof(rule ccontr)
  assume "¬width c < width h"
  hence "width c ≥ width h" by simp
  moreover have "c ≠ h" by (metis assms(2) neq_hole_if_on_hole)
  hence "width c ≠ width h" using assms unfolding is_hole_def by simp
  ultimately have "width c > width h" by simp
  hence "¬(side x c ⊆ side x h)" using assms less_le_not_le by fastforce 
  hence "¬(bot c ⊆ top h)" using assms by(auto simp add: bot_top_subset_by_side)
  moreover have "bot c ⊆ top h" by(metis assms(2) subset_if_on_hole)
  ultimately show "False" by metis
qed

lemma strict_subset_if_on_hole: assumes "is_hole h" "c ∈ filter_on_hole h"
  shows "bot c ⊂ top h"
proof
  show "bot c ⊆ top h" by(metis assms(2) subset_if_on_hole)
next
  have "width c ≠ width h" using assms width_on_hole_lt_width_hole by fastforce
  hence "side x c ≠ side x h" by(metis assms(1) valid_if_hole width_eq_if_side_eq)
  thus "bot c ≠ top h" using assms bot_top_eq_by_side by simp
qed

lemma on_hole_non_empty: "is_hole h ⟹ filter_on_hole h ≠ {}"
  using on_hole_cover
  by (metis Sup_empty image_empty subset_empty top_non_empty valid_if_hole)


section "Bottom of \<^term>‹unit_cube› is a hole"
lemma bot_unit_cube_cover_by_bot: "bot unit_cube ⊆ ⋃(image bot C)"
proof
  fix p
  assume "p ∈ bot unit_cube"
  hence "p ∈ to_set unit_cube" using bot_subset by auto
  then obtain "c" where "c ∈ C" "p ∈ to_set c" by(metis obtain_cube)
  from ‹p ∈ bot unit_cube› have "pz p = 0" by(metis min_unit_cube_0 in_bot_by_side)
  hence "min z c ≤ 0" using ‹p ∈ to_set c› by(simp add: in_set_by_side)
  moreover have "side z c ⊆ {0..<1}" by(metis ‹c ∈ C› subset_unit_cube_by_side)
  hence "min z c ≥ 0" using ‹c ∈ C› by fastforce
  ultimately have "min z c = 0" by simp
  hence "p ∈ bot c" using ‹p ∈ to_set c› ‹pz p = 0› by(simp add: in_set_by_side in_bot_by_side)
  thus "p ∈ ⋃ (image bot C)" using ‹c ∈ C› by auto
qed

lemma eq_if_width_eq_if_subset:
  assumes "width c1 = width c2" "to_set c1 ⊆ to_set c2"
  shows "to_set c1 = to_set c2"
proof-
  from assms(2) have "side x c1 ⊆ side x c2" "side y c1 ⊆ side y c2"  "side z c1 ⊆ side z c2" 
    using set_subset_by_side by blast+
  hence "side x c1 = side x c2" "side y c1 = side y c2" "side z c1 = side z c2"
    using assms(1) by fastforce+
  thus "to_set c1 = to_set c2" using set_eq_by_side by blast
qed

lemma width_ne_one:
  assumes "c ∈ C"
  shows "width c ≠ 1"
proof(rule ccontr)
  obtain "c'" where "c' ∈ C" "c ≠ c'" using assms dissection 
    unfolding is_dissection_def by(auto simp add: card_le_Suc_iff numeral_eq_Suc)
  hence "to_set c' ∩ to_set c = {}"  using assms by(metis eq_iff_intersect)
  assume "¬ width c ≠ 1"
  hence "width c = 1" by blast
  moreover have "to_set c ⊆ to_set unit_cube" by(metis assms subset_unit_cube_if_dissection)
  ultimately have "to_set c = to_set unit_cube" using eq_if_width_eq_if_subset 
    unfolding unit_cube_def by auto
  with ‹c' ∈ C› have "to_set c' ⊆ to_set c" by(metis subset_unit_cube_if_dissection)
  hence "to_set c' ∩ to_set c ≠ {}" using ‹c' ∈ C› by(simp add: non_empty Int_absorb2)
  moreover have "to_set c' ∩ to_set c = {}" by(metis assms ‹c' ∈ C› ‹c ≠ c'› eq_iff_intersect)
  ultimately show "False" by metis
qed

text "Combines the previous lemmas, to show that the bottom of \<^term>‹unit_cube› is a hole"
proposition hole_unit_cube: "is_hole (shift_down unit_cube)"
proof-
  let ?b = "shift_down unit_cube" ― ‹cube with \<^term>‹point› (0,0,-1) and \<^term>‹width› 1›
  show ?thesis unfolding is_hole_def
  proof(intro conjI subsetI ballI impI)
    show "is_valid ?b" by(simp add: shift_down_def)
  next
    fix p assume "p ∈ top ?b"
    hence "p ∈ bot unit_cube"  by(simp add: top_shift_down_eq_bot)
    thus "p ∈ ⋃(image bot C)" using bot_unit_cube_cover_by_bot by blast
  next
    fix c p assume "c ∈ C" "bot c ∩ top ?b ≠ {}" "p ∈ bot c"
    with ‹bot c ∩ top ?b ≠ {}› have "min z c = 0" 
      by(metis top_shift_down_eq_bot bot_intersect_by_side min_unit_cube_0)
    hence "pz p = 0" by(metis ‹p ∈ bot c› in_bot_by_side)
    moreover from ‹p ∈ bot c› have "px p ∈ {0..<1}" "py p ∈ {0..<1}" 
      using ‹c ∈ C› subset_unit_cube_by_side in_bot_by_side by blast+
    ultimately have "p ∈ bot unit_cube" by(metis min_unit_cube_0 in_bot_by_side side_unit_cube)
    thus "p ∈ top ?b" by(metis top_shift_down_eq_bot)
  next
    fix c assume "c ∈ C" "c ≠ ?b"
    hence "width c ≠ 1"  by(metis width_ne_one)
    thus "width c ≠ width ?b" by(simp add: unit_cube_def shift_down_def)
  qed
qed


section "Minimum cube on hole is interior"
context 
  fixes h assumes hole: "is_hole h"
begin

text "For this section, we fix a hole \<^term>‹h›, and define \<^term>‹cmin› to be the smallest cube 
on this hole. Theorem @{thm[source] hole} refers to this fact. The goal of this section is then to show that
\<^term>‹cmin› itself is a hole." 

subsection "Definition: Minimum cube on \<^term>‹h›"
text "\<^term>‹cmin› is the smallest cube on the hole \<^term>‹h›"
definition cmin:: "cube"
  where "cmin = (ARG_MIN width c . c ∈ filter_on_hole h)"

lemma arg_min_exist: "⟦finite C'; C' ≠ {}⟧ ⟹ (ARG_MIN width c . c ∈ C') ∈ C'"
  by(metis arg_min_on_def arg_min_if_finite(1))

text "This lemma also shows that \<^term>‹cmin› exists"
lemma cmin_on_h: "cmin ∈ filter_on_hole h"
  unfolding cmin_def by(metis hole arg_min_exist on_hole_finite on_hole_non_empty )

lemma cmin_valid[simp]: "is_valid cmin"
  by(metis cmin_on_h valid_if_on_hole)

lemma arg_min_minimal: "⟦finite C'; c ∈ C'⟧ ⟹ width (ARG_MIN width c . c ∈ C') ≤ width c"
  by(metis arg_min_least arg_min_on_def empty_iff)

lemma cmin_minimal: "c ∈ filter_on_hole h ⟹ width cmin ≤ width c"
  unfolding cmin_def by(metis hole arg_min_minimal on_hole_finite)

lemma cmin_minimal_strict:
  assumes "c ∈ filter_on_hole h" "c ≠ cmin"
  shows "width cmin < width c"              
proof -
  have "width cmin ≤ width c" using assms(1) by(rule cmin_minimal)
  moreover have "width cmin ≠ width c"
    by (metis assms on_hole_inj_on_width assms(2) cmin_on_h hole inj_on_contraD)
  ultimately show "width cmin < width c" by simp
qed

lemma cmin_max_z_neq_one: "max z cmin < 1"
proof -
  let ?On_h = "filter_on_hole h"
  have "bot cmin ⊂ top h" by(metis hole cmin_on_h strict_subset_if_on_hole)
  then obtain c where "c ∈ ?On_h" "c ≠ cmin" using hole obtain_cube_if_in_hole by blast 
  hence "min z cmin = min z c" by(metis cmin_on_h ‹c ∈ ?On_h› z_eq_if_on_hole)
  hence "max z cmin < max z c" by(simp add: ‹c ∈ ?On_h› ‹c ≠ cmin› cmin_minimal_strict)
  moreover have "side z c ⊆ {0..<1}" 
    by(metis ‹c ∈ ?On_h› dissection_if_on_hole  subset_unit_cube_by_side) 
  hence "max z c ≤ 1" using ‹c ∈ ?On_h› valid_if_on_hole by (simp add: less_le_not_le)
  ultimately show "max z cmin < 1" by simp
qed


subsection "Minimum cube on hole is interior"
text "All squares on the boundary of \<^term>‹h›"
definition is_on_boundary :: "axis ⇒ cube ⇒ bool" where
  "is_on_boundary ax c ⟷ min ax h  = min ax c ∨ max ax h  = max ax c"

text "Shows that IF \<^term>‹cmin› is on a boundary \<^term>‹ax›, then we find some \<^term>‹ax›-coordinate 
\<^term>‹r›, which is further from the boundary than the edge of \<^term>‹cmin›, but closer than the edge
 of any other cube sufficiently close to the boundary."
lemma cmin_on_boundary:
  assumes "is_on_boundary ax cmin"  "ax ∈ {x, y}"
  shows "∃r . 
    r ∈ (side ax h - (side ax cmin)) ∧ 
    (∀ c ∈ filter_on_hole h .  c ≠ cmin ⟶ side ax cmin ∩ side ax c ≠ {} ⟶ r ∈ side ax c)"
proof -
  let ?On_h = "filter_on_hole h"
  let ?c_2nd_min = "ARG_MIN width c . c ∈ (Set.remove cmin ?On_h)"
  have "bot cmin ⊂ top h" by(metis hole cmin_on_h strict_subset_if_on_hole)
  hence "Set.remove cmin ?On_h ≠ {}" using hole obtain_cube_if_in_hole by fastforce
  moreover have "finite (Set.remove cmin ?On_h)" 
    by (metis hole on_hole_finite remove_def finite_Diff)
  ultimately have "?c_2nd_min ∈ Set.remove cmin ?On_h" by(metis arg_min_exist)
  hence "?c_2nd_min ∈ ?On_h " and "width cmin < width ?c_2nd_min"
    by(simp, simp add: cmin_minimal_strict)
  then obtain "ε" where "ε > 0" "width cmin + ε < width ?c_2nd_min" 
    by(metis field_le_epsilon less_le_not_le nle_le)
  have ε_prop: "∀c ∈ ?On_h . cmin ≠ c ⟶ width cmin + ε < width c"
  proof(intro ballI impI)
    fix c assume "c ∈ ?On_h" "cmin ≠ c"
    hence "c ∈ Set.remove cmin ?On_h" by auto
    hence "width ?c_2nd_min ≤ width c" 
      using ‹Set.remove cmin ?On_h ≠ {}› ‹finite (Set.remove cmin ?On_h) › arg_min_minimal
      by blast
    thus "width cmin + ε < width c" using ‹width cmin + ε < width ?c_2nd_min› by simp
  qed
  then show ?thesis using assms(1) unfolding is_on_boundary_def
  proof(elim disjE)
    assume "min ax h = min ax cmin"
    let ?r = "max ax cmin + ε" 
    show ?thesis
    proof(intro exI conjI ballI impI)
      have "?r < min ax cmin + width ?c_2nd_min" using ‹width cmin + ε < width ?c_2nd_min› by auto
      also have "... = min ax h + width ?c_2nd_min" using ‹min ax h = min ax cmin› by simp
      finally have "?r < max ax h" 
        using ‹?c_2nd_min ∈ ?On_h› hole width_on_hole_lt_width_hole by fastforce
      moreover have "min ax cmin < max ax cmin" using assms(1) by(simp add: min_lt_max)
      hence "min ax h < ?r" using ‹ε > 0› ‹min ax h = min ax cmin›  by linarith
      ultimately have "?r ∈ side ax h" by simp
      moreover from ‹ε > 0› have "?r ∉ side ax cmin" by simp
      ultimately show  "?r ∈ side ax h - side ax cmin"  by simp
    next
      fix c assume "c ∈ ?On_h" "c ≠ cmin" "side ax cmin ∩ side ax c ≠ {}"
      from ‹side ax cmin ∩ side ax c ≠ {}› have "min ax c < max ax cmin" by auto
      also have "... < ?r" using ‹ε>0› by simp
      finally have "min ax c ≤ ?r" by simp
      moreover have "bot c ⊆ top h" by(metis ‹c ∈ ?On_h› subset_if_on_hole)
      hence "side ax c ⊆ side ax h" using ‹c ∈ ?On_h› assms(2) bot_top_subset_by_side by fastforce
      hence "min ax h ≤ min ax c" using ‹c ∈ ?On_h› by fastforce 
      hence "min ax cmin ≤ min ax c" using ‹min ax h = min ax cmin›  by simp
      hence "?r < max ax c" using ‹c ∈ ?On_h› ‹c ≠ cmin› ε_prop by auto
      ultimately show "?r ∈ side ax c" by simp
    qed
  next
    assume "max ax h = max ax cmin"
    let ?r = "min ax cmin - ε"
    show ?thesis
    proof(intro exI conjI ballI impI)
      have "min ax h = max ax h - width h" by simp
      also have "... < max ax h - width ?c_2nd_min" 
        using hole width_on_hole_lt_width_hole ‹?c_2nd_min ∈ ?On_h› by simp
      also have "... = max ax cmin - width ?c_2nd_min" using ‹max ax h = max ax cmin› by simp
      also have "... < ?r" using ‹width cmin + ε < width ?c_2nd_min› by argo
      finally have "min ax h < ?r" by simp
      moreover have "min ax cmin < max ax cmin" using assms(1) by(simp add: min_lt_max)
      hence "?r < max ax h" using ‹max ax h = max ax cmin› ‹ε > 0› by argo
      ultimately have "?r ∈ side ax h" by simp
      moreover have "?r ∉ side ax cmin" using ‹ε > 0› by simp
      ultimately show "?r ∈ side ax h - side ax cmin" by simp
    next
      fix c assume "c ∈ ?On_h" "c ≠ cmin" "side ax cmin ∩ side ax c ≠ {}"
      have "?r < min ax cmin" using ‹ε>0› by simp
      also have "... < max ax c" using ‹side ax cmin ∩ side ax c ≠ {}› by simp
      finally have "?r < max ax c" by simp
      moreover have "bot c ⊆ top h" by(metis ‹c ∈ ?On_h› subset_if_on_hole)
      hence "side ax c ⊆ side ax h" 
        using ‹c ∈ ?On_h› assms(2) bot_top_subset_by_side by fastforce
      hence "max ax c ≤ max ax h" using ‹c ∈ ?On_h› valid_if_on_hole by fastforce
      hence "max ax c ≤ max ax cmin" using ‹ max ax h = max ax cmin› by simp
      hence "min ax c≤ ?r" using ‹c ∈ ?On_h› ‹c ≠ cmin› ε_prop by auto
      ultimately show "?r ∈ side ax c" by simp
    qed
  qed
qed

text "Using the previous lemma, we show that \<^term>‹cmin› being on the boundary leads to a 
contradiction"
lemma cmin_not_on_boundary_by_axis: 
  assumes "ax ∈ {x, y}"
  shows "¬is_on_boundary ax cmin "
proof(rule ccontr, unfold not_not)
  let ?On_h = "filter_on_hole h"
  assume "is_on_boundary ax cmin"
  then obtain r where "r ∈ (side ax h - side ax cmin)" and
    r_prop: "(∀ c ∈ ?On_h .  c ≠ cmin ⟶ side ax cmin ∩ side ax c ≠ {} ⟶ r ∈ side ax c)"
    by(metis assms cmin_on_boundary)
  hence "r ∈ side ax h" and "r ∉ side ax cmin" by blast+
  let ?ax2 = "if ax = x then y else x"
  let ?p1 = "if ax = x then ⦇px=r, py=min y cmin, pz=max z h⦈ else ⦇px=min x cmin, py=r, pz=max z h⦈"
  have "side ?ax2 cmin ⊆ side ?ax2 h" using cmin_on_h side_subset_if_on_hole by simp
  hence "min ?ax2 cmin ∈ side ?ax2 h" using min_in_side by fastforce
  hence "?p1 ∈ top h" using ‹r ∈ side ax h› in_top_by_side assms by (simp split: if_splits)
  then obtain c1 where "?p1 ∈ bot c1" and c1_on_h: "c1 ∈ ?On_h" 
    using hole obtain_cube_if_in_hole by blast
  hence "cmin ≠ c1" using ‹r ∉ side ax cmin› assms in_bot_by_side by (auto split: if_splits)
  hence "width cmin < width c1" by(metis ‹c1 ∈ ?On_h› cmin_minimal_strict)
  hence "¬ side ?ax2 c1 ⊆ side ?ax2 cmin" using c1_on_h valid_if_on_hole by fastforce  
  then obtain s where "s ∈ side ?ax2 c1" "s ∉ side ?ax2 cmin" by blast
  let ?p2="if ax = x then ⦇px=min x cmin, py=s, pz=max z h⦈ else ⦇px=s, py=min y cmin, pz=max z h⦈"
  have "side ax cmin ⊆ side ax h" using assms cmin_on_h side_subset_if_on_hole by blast
  hence "min ax cmin ∈ side ax h" using min_in_side by fastforce
  moreover have "side ?ax2 c1 ⊆ side ?ax2 h" using ‹c1 ∈?On_h› side_subset_if_on_hole by simp
  hence "s ∈ side ?ax2 h" using ‹s ∈ side ?ax2 c1› by blast
  ultimately have "?p2 ∈ top h" using in_top_by_side assms by (simp split: if_splits)
  then obtain c2 where  "?p2 ∈ bot c2" and c2_on_h: "c2 ∈ ?On_h" 
    using hole obtain_cube_if_in_hole by blast
  let ?p3 = "if ax = x then ⦇px=r, py=s, pz=max z h⦈ else ⦇px=s, py=r, pz=max z h⦈"
    ― ‹We show that \<^term>‹?p3› is in the intersection of \<^term>‹c1› and \<^term>‹c2›, but \<^term>‹p2› is 
      only in \<^term>‹c2›, contradicting disjointness›
  have "?p2 ∉ bot cmin" using ‹s ∉ side ?ax2 cmin› in_bot_by_side by (auto split: if_splits)
  hence "cmin ≠ c2" using ‹?p2 ∈ bot c2› by blast
  hence "r ∈ side ax c2" using r_prop c2_on_h min_in_side ‹?p2 ∈ bot c2› in_bot_by_side assms
    by fastforce
  hence "?p3 ∈ bot c2" using ‹?p2 ∈ bot c2› in_bot_by_side assms by (simp split: if_splits)
  moreover have "?p3 ∈ bot c1" using ‹?p1 ∈ bot c1› ‹s ∈ side ?ax2 c1› in_bot_by_side by auto
  ultimately have "c1 = c2" using c1_on_h c2_on_h eq_iff_bot_intersect_if_on_hole
    by blast
  moreover from ‹s ∉ side ?ax2 cmin› have "?p2 ∉ to_set cmin" using in_set_by_side by auto
  hence "cmin ≠ c2" using eq_iff_side_eq_if_on_hole c2_on_h ‹?p2 ∈ bot c2› bot_subset 
    by blast
  hence "to_set cmin ∩ to_set c2 = {}" using cmin_on_h c2_on_h eq_iff_intersect by simp
  hence "side ?ax2 cmin ∩ side ?ax2 c2 = {}" using ‹?p2 ∈ bot c2› ‹cmin ≠ c2› 
      c2_on_h assms cmin_on_h in_bot_by_side eq_iff_side_intersect_if_on_hole by fastforce
  hence "min ?ax2 cmin ∉ side ?ax2 c2" using cmin_valid min_in_side by blast
  hence "?p1 ∉ bot c2" using assms in_bot_by_side by fastforce 
  hence "c1 ≠ c2" using ‹?p1 ∈ bot c1› by blast
  ultimately show "False" by blast
qed

text "Previous result, written as inequalities instead"
proposition cmin_not_on_boundary: 
  "min x h < min x cmin ∧ max x cmin < max x h 
        ∧ min y h < min y cmin ∧ max y cmin < max y h"
proof-
  have "side x cmin ⊆ side x h ∧ side y cmin ⊆ side y h"
    using cmin_on_h side_subset_if_on_hole by blast
  hence "min x h ≤ min x cmin ∧ max x cmin ≤ max x h ∧ 
    min y h ≤ min y cmin ∧ max y cmin ≤ max y h" using cmin_valid by auto
  thus "min x h < min x cmin ∧ max x cmin < max x h ∧
    min y h < min y cmin ∧ max y cmin < max y h" 
    using cmin_not_on_boundary_by_axis unfolding is_on_boundary_def by force
qed


section "Minimum cube of hole induces hole on top"
text "The main result of this proof - the minimum cube on a hole is itself a hole!"
proposition hole_cmin: 
  shows "is_hole cmin"
proof-
  let ?On_cmin = "filter_on_hole cmin"
  show ?thesis unfolding is_hole_def
  proof(intro conjI ballI impI)
    show "is_valid cmin" by simp
  next 
    show "top cmin ⊆ ⋃(image bot C)" 
      by(metis top_cover_by_bot cmin_max_z_neq_one cmin_on_h dissection_if_on_hole)
  next
    fix c assume "c ∈ C" "c ≠ cmin"
    thus "width c ≠ width cmin" 
      by(metis dissection dissection_if_on_hole cmin_on_h inj_onD is_dissection_def)
  next
    fix c assume "c ∈ C" "bot c ∩ top cmin ≠ {}"
    hence c_valid: "is_valid c" by simp
    show "bot c ⊆ top cmin"
    proof(rule ccontr)
      assume "¬ bot c ⊆ top cmin"
      from ‹bot c ∩ top cmin ≠ {}› have "min z c = max z cmin" using bot_top_intersect_by_side 
        by blast
      with ‹¬ bot c ⊆ top cmin› obtain ax where ax: "ax ∈{x,y}" "¬side ax c ⊆ side ax cmin" 
        using bot_top_subset_by_side c_valid by (meson insert_iff)
      let ?ax2 = "if ax=x then y else x"
      have "?ax2 ∈ {x,y}" by simp
      have "min ax h < min ax cmin" "max ax cmin < max ax h" 
        using ax(1) cmin_not_on_boundary by blast+
      moreover have "side ax c ∩ side ax cmin ≠ {}" 
        using ‹bot c ∩ top cmin ≠ {}› ax(1) bot_top_intersect_by_side  by blast
      ultimately have "side ax c ∩ side ax h - side ax cmin ≠ {}" using ax(2) by fastforce
      then obtain a where a_prop: "a ∈ side ax c ∩ side ax h" "a ∉ side ax cmin" by blast
      moreover from ‹bot c ∩ top cmin ≠ {}› have "side ?ax2 c ∩ side ?ax2 cmin ≠ {}"
        using bot_top_intersect_by_side ‹?ax2 ∈ {x,y}› by simp
      then obtain b where b_prop: "b ∈ side ?ax2 c ∩ side ?ax2 cmin" by blast
      hence b_prop_2: "b ∈ side ?ax2 c ∩ side ?ax2 h" 
        using ‹?ax2 ∈ {x,y}› cmin_on_h side_subset_if_on_hole by blast
      let ?x0 = "if ax=x then a else b" and ?y0 = "if ax=y then a else b"
      have xy0_props: "?x0 ∈ side x c ∩ side x h" "?y0 ∈ side y c ∩ side y h"
        "?x0 ∉ side x cmin ∨ ?y0 ∉ side y cmin"
      proof -
        show"?x0 ∈ side x c ∩ side x h" using a_prop b_prop ax(1) ‹?ax2 ∈ {x,y}›
          using b_prop_2 by presburger
        show  "?y0 ∈ side y c ∩ side y h" using a_prop b_prop_2 ax(1)  by fastforce
        show "?x0 ∉ side x cmin ∨ ?y0 ∉ side y cmin" using a_prop ax(1) by fastforce
      qed
      let ?pd = "⦇px=?x0, py=?y0, pz=max z h⦈"
      let ?pu = "⦇px=?x0, py=?y0, pz=min z c⦈"
      have "max z h = min z cmin" by(metis cmin_on_h min_z_eq_max_z_hole_if_on_hole)
      hence "?pd = ⦇px=?x0, py=?y0, pz=min z cmin⦈" by simp
      moreover have "min z cmin < min z c" using min_lt_max ‹min z c = max z cmin› by simp
      hence "min z cmin ∉ side z c" using in_set_by_side by simp
      ultimately have "?pd ∉ to_set c" by(simp add: in_set_by_side)
      have "?pu ∈ bot c" using c_valid xy0_props in_bot_by_side by simp
      hence "?pu ∈ to_set c" using bot_subset by blast
      have "?pd ∉ bot cmin" using ‹?x0 ∉ side x cmin ∨ ?y0 ∉ side y cmin› in_bot_by_side by auto
      have "?pd ∈ top h" using valid_if_hole xy0_props in_top_by_side by simp
      then obtain c' where "c' ∈ filter_on_hole h" "?pd ∈ bot c'" 
        using hole obtain_cube_if_in_hole by blast
      hence "c' ≠ cmin" using ‹?pd ∉ bot cmin› by blast
      hence "width cmin < width c'"
        using ‹c' ∈ filter_on_hole h› cmin_minimal_strict by simp
      moreover have "min z cmin = min z c'" 
        by(metis cmin_on_h ‹c' ∈ filter_on_hole h› z_eq_if_on_hole)
      ultimately have "max z cmin < max z c'" by simp 
      hence "min z c < max z c'" by(metis ‹min z c = max z cmin›)
      hence "min z c ∈ side z c'" using ‹min z cmin < min z c› ‹min z cmin = min z c'› by auto 
      hence "?pu ∈ to_set c'" using ‹c' ∈ filter_on_hole h› ‹?pd ∈ bot c'› 
          in_bot_by_side in_set_by_side ‹min z c = max z cmin› by simp
      hence "to_set c ∩ to_set c' ≠ {}" using ‹?pu ∈ to_set c› by blast
      hence "c = c'" using ‹c' ∈ filter_on_hole h›  ‹c ∈ C› eq_iff_intersect by auto
      moreover have "c ≠ c'" using ‹?pd ∉ to_set c› ‹?pd ∈ bot c'› using bot_subset by blast
      ultimately show "False" by blast
    qed
  qed
qed

text "The main purpose of the previous result: From the proposition, \<^term>‹hole_cmin› when given the
hole \<^term>‹h› induce another hole \<^term>‹h'› (i.e., \<^term>‹cmin›), which is in \<^term>‹C› and is strictly
smaller."
lemma recursive_step: "∃h'. h' ∈ C ∧ is_hole h' ∧ width h' < width h"
proof-
  show ?thesis
  proof(intro exI conjI)
    show "cmin ∈ C" using cmin_on_h by force
    show "is_hole cmin" by(simp add: hole_cmin)
    show "width cmin < width h" by(simp add: hole cmin_on_h width_on_hole_lt_width_hole)
  qed
qed
text "Here we end the context in which \<^term>‹h› is some fixed hole 
(and hence also the specific \<^term>‹cmin›)"
end

section "The main result"
text "We combine the previous lemmas inductively as follows:
  0: Start with the bottom of \<^term>‹unit_cube›, which we showed is a hole.
  n: For each hole, take the minimum cube on this hole, which is then a new hole, 
strictly smaller, and in \<^term>‹C›. Hence, \<^term>‹C› is infinite."
definition next_hole:: "cube ⇒ cube" where
  "next_hole h = (SOME h' . h' ∈ C ∧ is_hole h' ∧ width h' < width h)"

lemma next_hole_exist: "is_hole h 
  ⟹ next_hole h ∈ C ∧ is_hole (next_hole h) ∧ width (next_hole h) < width h"
  unfolding next_hole_def  by (rule someI_ex) (rule recursive_step)

text "For following proof, we want the image of \<^term>‹nth_hole› to be contained in \<^term>‹C›, 
hence we start at \<^term>‹1› (= \<^term>‹Suc 0›). \<^term>‹nth_hole› is a function from \<^term>‹ℕ› to \<^term>‹C›"
definition nth_hole :: "nat ⇒ cube" where
  "nth_hole n = (next_hole ^^ Suc n) (shift_down unit_cube)"

text "Each cube in the image of \<^term>‹nth_hole› is a hole"
lemma nth_hole_is_hole: "is_hole (nth_hole n)"
proof(induction n)
  case 0
  have "nth_hole 0 = next_hole (shift_down unit_cube)" by(simp add: nth_hole_def)
  moreover have "is_hole (shift_down unit_cube)" by(rule hole_unit_cube)
  ultimately show ?case by(simp add: next_hole_exist)
next
  case (Suc n)
  then show ?case by(simp add: nth_hole_def next_hole_exist)
qed

text "\<^term>‹uminus› is \<^term>‹(λ x. -x)›, and \<^term>‹strict_mono› means strictly increasing 
  (not strictly monotonous, as the name might suggest)"
lemma nth_hole_strict_decreasing: "strict_mono (uminus ∘ width ∘ nth_hole)"
proof(rule iffD2, rule strict_mono_Suc_iff, intro allI)
  fix n
  have "is_hole (nth_hole n)" by (rule nth_hole_is_hole)
  thus "(uminus ∘ width ∘ nth_hole) n < (uminus ∘ width ∘ nth_hole) (Suc n)" 
    by(simp add: nth_hole_def next_hole_exist)
qed

text "\<^term>‹nth_hole› is injective"
lemma nth_hole_inj : "inj nth_hole"
proof -
  have "strict_mono (uminus ∘ width ∘ nth_hole)" by(rule nth_hole_strict_decreasing)
  hence "inj (uminus ∘ width ∘ nth_hole)" by(simp add: strict_mono_imp_inj_on)
  thus "inj nth_hole" by(simp add:inj_on_imageI2)
qed

text "The image (range) of \<^term>‹nth_hole› is contained in \<^term>‹C›"
lemma nth_hole_in: "nth_hole n ∈ C"
proof(cases n)
  case 0
  then show ?thesis by(simp add: hole_unit_cube nth_hole_def next_hole_exist)
next
  case (Suc nat)
  then obtain m where "n = Suc m" by simp
  have "is_hole (nth_hole m)" by(simp add: nth_hole_is_hole)
  hence "next_hole (nth_hole m) ∈ C" by(simp add: next_hole_exist)
  thus "nth_hole n ∈ C"  by(simp add: nth_hole_def ‹n = Suc m›)
qed

text "Same as previous lemma, but written with a quantifier"
lemma nth_hole_in_forall: "∀n . nth_hole n ∈ C"
  by(simp add: nth_hole_in)

text "The assumption made in this context (\<^term>‹is_dissection C›) leads to \<^term>‹False› 
(since \<^term>‹nth_hole› generates an infinite subset of \<^term>‹C›)"
theorem false_if_dissection: "False"
proof-
  have "inj nth_hole" by(rule nth_hole_inj)
  moreover have "∀n . nth_hole n ∈ C" by(rule nth_hole_in_forall)
      ― ‹\<^term>‹nth_hole› injective, with infinite domain \<^term>‹ℕ›, and image contained in \<^term>‹C› 
  together implies that \<^term>‹C› is infinite›
  ultimately have "infinite C" by(metis finite_subset image_subset_iff range_inj_infinite)
  moreover have "finite C" using dissection unfolding is_dissection_def by metis
  ultimately show "False" by metis
qed
end ― ‹Here we end the \<^term>‹is_dissection C› context›


text "Main result (spelling out the definition of \<^term>‹is_dissection›)."
theorem dissection_does_not_exist:
  "∄ C. (∀ c ∈ C. is_valid c) 
  ∧ disjoint (image to_set C) 
  ∧ ⋃(image to_set C) = to_set unit_cube 
  ∧ inj_on width C 
  ∧ card C ≥ 2 
  ∧ finite C"
  by(metis is_dissection_def false_if_dissection)
end