Theory k_coloring
theory k_coloring
imports PropCompactness
begin
section ‹de Bruijn-Erdös k-coloring theorem for countable infinite graphs›
text‹This section formalizes de Bruijn-Erdös k-coloring theorem for countable infinite graphs.
The construction applies the compactness theorem for propositional logic directly. ›
section ‹de Bruijn-Erdös k-coloring theorem for countable infinite graphs›
type_synonym 'v digraph = "('v set) × (('v × 'v) set)"
abbreviation vert :: "'v digraph ⇒ 'v set" ("V[_]" [80] 80) where
"V[G] ≡ fst G"
abbreviation edge :: "'v digraph ⇒ ('v × 'v) set" ("E[_]" [80] 80) where
"E[G] ≡ snd G"
definition is_graph :: "'v digraph ⇒ bool" where
"is_graph G ≡ ∀ u v. (u,v) ∈ E[G] ⟶ u ∈ V[G] ∧ v ∈ V[G] ∧ u ≠ v"
definition is_subgraph :: "'v digraph ⇒'v digraph ⇒ bool" where
"is_subgraph H G ≡
(V[H] ⊆ V[G]) ∧ E[H] ⊆ E[G] ∩ ((V[H]) × (V[H]))"
definition is_induced_subgraph :: "'v digraph ⇒'v digraph ⇒ bool" where
"is_induced_subgraph H G ≡
(V[H] ⊆ V[G]) ∧ E[H] = E[G] ∩ ((V[H]) × (V[H]))"
definition induced_subgraph_from_vert :: "'v digraph ⇒ 'v set ⇒ 'v digraph" where
"induced_subgraph_from_vert G V ≡ (V, E[G] ∩ (V×V))"
lemma is_induced_subgraph_from_vert_is_induced_subgraph:
assumes "V ⊆ V[G]"
shows "is_induced_subgraph (induced_subgraph_from_vert G V) G"
proof-
let ?indH = "induced_subgraph_from_vert G V"
have 1: "V[?indH] ⊆ V[G]" using induced_subgraph_from_vert_def assms
by (metis fst_conv)
have 2: "E[?indH] = E[G] ∩ ((V[?indH]) × (V[?indH]))"
using induced_subgraph_from_vert_def
by (metis fst_conv snd_conv)
show ?thesis using 1 2 is_induced_subgraph_def
by blast
qed
lemma induced_subgraph_is_subgraph:
shows "is_induced_subgraph H G ⟶ is_subgraph H G"
by(simp add: is_induced_subgraph_def is_subgraph_def)
corollary induced_subraph_from_vert_is_subgraph:
assumes "V ⊆ V[G]"
shows "is_subgraph (induced_subgraph_from_vert G V) G"
using assms induced_subgraph_is_subgraph is_induced_subgraph_from_vert_is_induced_subgraph
by blast
lemma subgraph_is_subgraph_ind_subgraph_vert:
assumes "is_subgraph H G"
shows "is_subgraph H (induced_subgraph_from_vert G (V[H]))"
proof-
let ?indH = "(induced_subgraph_from_vert G (V[H]))"
have 1: "V[H] ⊆ V[?indH]"
using induced_subgraph_from_vert_def[of G "V[H]"] assms by auto
have 2: "E[H] ⊆ E[?indH] ∩ ((V[H])×(V[H]))"
using is_subgraph_def induced_subgraph_from_vert_def[of G "V[H]"] assms snd_conv
by (metis inf_right_idem)
show ?thesis using 1 2 is_subgraph_def by blast
qed
lemma
assumes "is_graph G" and "is_induced_subgraph H G"
shows "is_graph H"
proof(unfold is_graph_def)
show "∀u v. (u, v) ∈ E[H] ⟶ u ∈ V[H] ∧ v ∈ V[H] ∧ u ≠ v"
proof((rule allI)+, rule impI)
fix u v
assume "(u, v) ∈ E[H]"
show "u ∈ V[H] ∧ v ∈ V[H] ∧ u ≠ v"
proof-
have "(u, v) ∈ E[G] ∩ (V[H]) × (V[H])" using `(u, v) ∈ E[H]` assms(2)
by(unfold is_induced_subgraph_def,auto)
hence 1: "(u, v) ∈ E[G]" and 2: "u ∈ V[H] ∧ v ∈ V[H]" by auto
have "u ≠ v" using 1 `is_graph G` by(unfold is_graph_def,auto)
thus "u ∈ V[H] ∧ v ∈ V[H] ∧ u ≠ v" using 2 by auto
qed
qed
qed
definition finite_graph :: "'v digraph ⇒ bool" where
"finite_graph G ≡ finite (V[G])"
definition coloring :: "('v ⇒ nat) ⇒ nat ⇒ 'v digraph ⇒ bool" where
"coloring c k G ≡
(∀u. u∈V[G]⟶ c(u) < k) ∧ (∀u v.(u,v)∈E[G] ⟶ c(u)≠c(v))"
definition colorable :: "'v digraph ⇒ nat ⇒ bool" where
"colorable G k ≡ ∃c. coloring c k G"
lemma coloring_emptygraph:
assumes "V[G]={}"
shows "colorable ({},{}) 0 " using colorable_def
using colorable_def coloring_def by fastforce
lemma coloring_nonemptygraph:
assumes "V[G]≠{}" and "colorable G k"
shows "0<k"
by (metis assms(1,2) colorable_def coloring_def empty_subsetI less_nat_zero_code not_gr_zero
subsetI subset_antisym)
lemma colorable_subgraph :
assumes "is_subgraph H G" and "colorable G k"
shows "colorable H k"
proof-
have "∃c. coloring c k G" using colorable_def assms(2) by blast
then obtain c where "coloring c k G" by auto
hence "coloring c k H" using coloring_def
by (smt (verit, best) assms(1) is_subgraph_def le_inf_iff subset_eq)
thus ?thesis using colorable_def
by blast
qed
lemma coloring_card_image:
assumes "coloring c k G"
shows "card (c ` (V[G])) ≤ k"
proof -
have img_subset: "c ` (V[G]) ⊆ {0..k-1}"
using assms unfolding coloring_def by auto
have fin_img: "finite (c ` (V[G]))"
using img_subset finite_atLeastAtMost by (rule finite_subset)
have "card (c ` (V[G])) ≤ card {0..k-1}"
using card_mono[OF finite_atLeastAtMost img_subset] fin_img
by simp
thus ?thesis
by (metis all_not_in_conv assms bot_nat_0.extremum_strict card.empty card_atLeastAtMost
coloring_def diff_Suc_1 diff_is_0_eq diff_zero gr0_conv_Suc image_empty not_gr_zero)
qed
primrec atomic_disjunctions :: "'v ⇒ nat ⇒ ('v × nat)formula" where
"atomic_disjunctions v 0 = atom (v, 0)"
| "atomic_disjunctions v (Suc k) = (atom (v, Suc k)) ∨. (atomic_disjunctions v k)"
definition ℱ :: "'v digraph ⇒ nat ⇒ (('v × nat)formula) set" where
"ℱ G k ≡ (⋃v∈V[G]. {atomic_disjunctions v (k-1)})"
definition 𝒢 :: "'v digraph ⇒ nat ⇒ ('v × nat)formula set" where
"𝒢 G k ≡ {¬.(atom (v, i) ∧. atom(v,j))
| v i j. (v∈V[G]) ∧ (0≤i ∧ 0≤j ∧ i<k ∧ j<k ∧ i≠j)}"
definition ℋ :: "'v digraph ⇒ nat ⇒ ('v × nat)formula set" where
"ℋ G k ≡ {¬.(atom (u, i) ∧. atom(v,i))
|u v i . (u∈V[G] ∧ v∈V[G] ∧ (u,v)∈E[G]) ∧ (0≤i ∧ i < k)} "
definition 𝒯 :: "'v digraph ⇒ nat ⇒ ('v × nat)formula set" where
"𝒯 G k ≡ (ℱ G k) ∪ (𝒢 G k) ∪ (ℋ G k)"
primrec vertices_formula :: "('v × nat)formula ⇒ 'v set" where
"vertices_formula ⊥. = {}"
| "vertices_formula ⊤. = {}"
| "vertices_formula (atom P) = {fst P}"
| "vertices_formula (¬. F) = vertices_formula F"
| "vertices_formula (F ∧. G) = vertices_formula F ∪ vertices_formula G"
| "vertices_formula (F ∨. G) = vertices_formula F ∪ vertices_formula G"
| "vertices_formula (F →.G) = vertices_formula F ∪ vertices_formula G"
definition vertices_set_formulas :: "('v × nat)formula set ⇒ 'v set" where
"vertices_set_formulas S = (⋃F∈ S. vertices_formula F)"
lemma finite_vertices:
shows "finite (vertices_formula F)"
by(induct F, auto)
lemma vertices_disjunction:
assumes "F = atomic_disjunctions v k" shows "vertices_formula F = {v}"
proof-
have "F = atomic_disjunctions v k ⟹ vertices_formula F = {v}"
proof(induct k arbitrary: F)
case 0
assume "F = atomic_disjunctions v 0"
hence "F = atom (v, 0 )" by auto
thus "vertices_formula F = {v}" by auto
next
case(Suc k)
have "F =(atom (v, Suc k )) ∨. (atomic_disjunctions v k)"
using Suc(2) by auto
hence "vertices_formula F = vertices_formula (atom (v, Suc k ))
∪ vertices_formula (atomic_disjunctions v k)"
by auto
hence "vertices_formula F = {v} ∪ vertices_formula (atomic_disjunctions v k)"
by auto
hence "vertices_formula F = {v} ∪ {v}" using Suc(1) by auto
thus "vertices_formula F = {v}" by auto
qed
thus ?thesis using assms by auto
qed
lemma all_vertices_colored:
shows "vertices_set_formulas (ℱ G k) ⊆ V[G]"
proof
fix x
assume hip: "x ∈ vertices_set_formulas (ℱ G k)" show "x ∈ V[G]"
proof-
have "x ∈ (⋃F∈(ℱ G k). vertices_formula F)" using hip
by(unfold vertices_set_formulas_def,auto)
hence "∃F∈(ℱ G k). x ∈ vertices_formula F" by auto
then obtain F where "F∈(ℱ G k)" and x: "x ∈ vertices_formula F" by auto
hence "∃ v∈V[G]. F∈{atomic_disjunctions v (k-1)}" by (unfold ℱ_def, auto)
then obtain v where v: "v∈V[G]" and "F∈{atomic_disjunctions v (k-1)}" by auto
hence "F = atomic_disjunctions v (k-1)" by auto
hence "vertices_formula F = {v}"
using vertices_disjunction[OF `F = atomic_disjunctions v (k-1)`] by auto
hence "x = v" using x by auto
thus ?thesis using v by auto
qed
qed
lemma vertices_maximumC:
shows "vertices_set_formulas(𝒢 G k) ⊆ V[G]"
proof
fix x
assume hip: "x ∈ vertices_set_formulas (𝒢 G k)" show "x ∈ V[G]"
proof-
have "x ∈ (⋃F∈(𝒢 G k). vertices_formula F)" using hip
by(unfold vertices_set_formulas_def,auto)
hence "∃F∈(𝒢 G k). x ∈ vertices_formula F" by auto
then obtain F where "F∈(𝒢 G k)" and x: "x ∈ vertices_formula F"
by auto
hence "∃v i j. v∈V[G] ∧ F = ¬.(atom (v, i) ∧. atom(v,j))"
by (unfold 𝒢_def, auto)
then obtain v i j where "v∈V[G]" and "F = ¬.(atom (v, i) ∧. atom(v,j))"
by auto
hence v: "v∈V[G]" and "F = ¬.(atom (v, i) ∧. atom(v,j))" by auto
hence v: "v∈V[G]" and "vertices_formula F = {v}" by auto
thus "x ∈ V[G]" using x by auto
qed
qed
lemma distinct_verticesC:
shows "vertices_set_formulas(ℋ G k)⊆ V[G]"
proof
fix x
assume hip: "x ∈ vertices_set_formulas (ℋ G k)" show "x ∈ V[G]"
proof-
have "x ∈ (⋃F∈(ℋ G k). vertices_formula F)" using hip
by(unfold vertices_set_formulas_def,auto)
hence "∃F∈(ℋ G k) . x ∈ vertices_formula F" by auto
then obtain F where "F∈(ℋ G k)" and x: "x ∈ vertices_formula F"
by auto
hence "∃u v i . u∈V[G] ∧ v∈V[G] ∧ F = ¬.(atom (u, i) ∧. atom(v,i))"
by (unfold ℋ_def, auto)
then obtain u v i
where "u∈V[G]" and "v∈V[G]" and "F = ¬.(atom (u, i) ∧. atom(v,i))"
by auto
hence "u∈V[G]" and "v∈V[G]" and "F = ¬.(atom (u, i) ∧. atom(v,i))"
by auto
hence u: "u∈V[G]" and v: "v∈V[G]" and "vertices_formula F = {u, v}"
by auto
hence "x=u ∨ x=v" using x by auto
thus "x ∈ V[G]" using u v by auto
qed
qed
lemma vv:
shows "vertices_set_formulas (A ∪ B) = (vertices_set_formulas A) ∪ (vertices_set_formulas B)"
by(unfold vertices_set_formulas_def, auto)
lemma vv1:
assumes "F∈(ℱ G k)"
shows "(vertices_formula F) ⊆ (vertices_set_formulas (ℱ G k))"
proof
fix x
assume hip: "x ∈ vertices_formula F"
show "x ∈ vertices_set_formulas (ℱ G k)"
proof-
have "∃F. F∈(ℱ G k) ∧ x ∈ vertices_formula F" using assms hip by auto
thus ?thesis by(unfold vertices_set_formulas_def, auto)
qed
qed
lemma vv2:
assumes "F∈(𝒢 G k)"
shows "(vertices_formula F) ⊆ (vertices_set_formulas (𝒢 G k))"
proof
fix x
assume hip: "x ∈ vertices_formula F"
show "x ∈ vertices_set_formulas (𝒢 G k)"
proof-
have "∃F. F∈(𝒢 G k) ∧ x ∈ vertices_formula F" using assms hip by auto
thus ?thesis by(unfold vertices_set_formulas_def, auto)
qed
qed
lemma vv3:
assumes "F∈(ℋ G k)"
shows "(vertices_formula F) ⊆ (vertices_set_formulas (ℋ G k))"
proof
fix x
assume hip: "x ∈ vertices_formula F"
show "x ∈ vertices_set_formulas (ℋ G k)"
proof-
have "∃F. F∈(ℋ G k) ∧ x ∈ vertices_formula F" using assms hip by auto
thus ?thesis by(unfold vertices_set_formulas_def, auto)
qed
qed
lemma vertex_set_inclusion:
shows "vertices_set_formulas (𝒯 G k) ⊆ V[G]"
proof
fix x
assume hip: "x ∈ vertices_set_formulas (𝒯 G k)" show "x ∈ V[G]"
proof-
have "x ∈ vertices_set_formulas ((ℱ G k) ∪ (𝒢 G k) ∪ (ℋ G k))"
using hip by (unfold 𝒯_def,auto)
hence "x ∈ vertices_set_formulas ((ℱ G k) ∪ (𝒢 G k)) ∪
vertices_set_formulas(ℋ G k)"
using vv[of "(ℱ G k) ∪ (𝒢 G k)"] by auto
hence "x ∈ vertices_set_formulas ((ℱ G k) ∪ (𝒢 G k)) ∨
x ∈ vertices_set_formulas(ℋ G k)"
by auto
thus ?thesis
proof(rule disjE)
assume hip: "x ∈ vertices_set_formulas (ℱ G k ∪ 𝒢 G k)"
hence "x ∈ (⋃F∈ (ℱ G k) ∪ (𝒢 G k). vertices_formula F)"
by(unfold vertices_set_formulas_def, auto)
then obtain F
where F: "F∈(ℱ G k) ∪ (𝒢 G k)" and x: "x ∈ vertices_formula F" by auto
from F have "(vertices_formula F) ⊆ (vertices_set_formulas (ℱ G k))
∨ vertices_formula F ⊆ (vertices_set_formulas (𝒢 G k))"
using vv1 vv2 by blast
hence "x ∈ vertices_set_formulas (ℱ G k) ∨ x ∈ vertices_set_formulas (𝒢 G k)"
using x by auto
thus "x ∈ V[G]"
using all_vertices_colored[of "G" "k"] vertices_maximumC[of "G" "k"] by auto
next
assume "x ∈ vertices_set_formulas (ℋ G k)"
hence
"x ∈ (⋃F∈(ℋ G k). vertices_formula F)"
by(unfold vertices_set_formulas_def, auto)
then obtain F where F: "F∈(ℋ G k)" and x: "x ∈ vertices_formula F"
by auto
from F have "(vertices_formula F) ⊆ (vertices_set_formulas (ℋ G k))"
using vv3 by blast
hence "x ∈ vertices_set_formulas (ℋ G k)" using x by auto
thus "x ∈ V[G]" using distinct_verticesC[of "G" "k"]
by auto
qed
qed
qed
lemma vsf:
assumes "G ⊆ H"
shows "vertices_set_formulas G ⊆ vertices_set_formulas H"
using assms by(unfold vertices_set_formulas_def, auto)
lemma vertices_subset_formulas:
assumes "S ⊆ (𝒯 G k)"
shows "vertices_set_formulas S ⊆ V[G]"
proof-
have "vertices_set_formulas S ⊆ vertices_set_formulas (𝒯 G k)"
using assms vsf by auto
thus ?thesis using vertex_set_inclusion[of "G"] by auto
qed
lemma induced_subgraph:
assumes "is_graph G" and "S ⊆ (𝒯 G k)"
shows "is_induced_subgraph (induced_subgraph_from_vert G (vertices_set_formulas S)) G"
proof-
let ?V = "vertices_set_formulas S"
let ?H = "(?V, E[G] ∩ (?V × ?V))"
have 1: "E[?H] = E[G] ∩ (?V × ?V)" and 2: "V[?H]= ?V" by auto
have "(V[?H] ⊆ V[G])" using 2 assms(2) vertices_subset_formulas[of S G ] by auto
moreover
have "E[?H] = (E[G] ∩ ((V[?H]) × (V[?H])))" using 1 2 by auto
ultimately
have "is_induced_subgraph ?H G" by(unfold is_induced_subgraph_def, auto)
thus ?thesis by(unfold induced_subgraph_from_vert_def, auto)
qed
lemma finite_subgraph:
assumes "is_graph G" and "S ⊆ (𝒯 G k)" and "finite S"
shows "finite_graph (induced_subgraph_from_vert G (vertices_set_formulas S))"
proof-
let ?V = "vertices_set_formulas S"
let ?H = "(?V, E[G] ∩ (?V × ?V))"
have 1: "E[?H] = E[G] ∩ (?V × ?V)" and 2: "V[?H]= ?V" by auto
have 3: "finite ?V" using `finite S` finite_vertices
by(unfold vertices_set_formulas_def, auto)
hence "finite (V[?H])" using 2 by auto
thus ?thesis
by (unfold finite_graph_def, unfold induced_subgraph_from_vert_def, auto)
qed
fun graph_interpretation :: "'v digraph ⇒ ('v ⇒ nat) ⇒ (('v × nat) ⇒ bool)" where
"graph_interpretation G f = (λ(v,i).(if v ∈ V[G] ∧ f(v) = i then True else False))"
lemma value1:
assumes "v ∈ V[G]" and "f(v)< k" and "F = atomic_disjunctions v k"
shows "t_v_evaluation (graph_interpretation G f) F"
proof-
let ?i = "f(v)"
have "0 ≤ ?i" by auto
{have "v ∈ V[G] ⟹ 0 ≤ ?i ⟹ ?i≤k ⟹ F = atomic_disjunctions v k ⟹
t_v_evaluation (graph_interpretation G f) F"
proof(induct k arbitrary: F)
case 0
have "?i = 0" using "0" (2-3) by auto
hence "t_v_evaluation (graph_interpretation G f) (atom (v, 0))"
using `v ∈ V[G]` by auto
thus ?case
using "0" (4) by auto
next
case(Suc k)
from Suc(1) Suc(2) Suc(3) Suc(4) Suc(5) show ?case
proof(cases)
assume "(Suc k) = ?i"
hence "t_v_evaluation (graph_interpretation G f) (atom (v,Suc k ))"
using Suc(2) Suc(3) Suc(5) by auto
hence
"t_v_evaluation (graph_interpretation G f) (atom (v, Suc k)
∨.atomic_disjunctions v k)"
by auto
thus ?case using Suc(5) by auto
next
assume 1: "(Suc k) ≠ ?i"
hence "¬ t_v_evaluation (graph_interpretation G f) (atom (v, Suc k))"
using Suc(5) by auto
moreover
have "?i < (Suc k)" using Suc(4) 1 by auto
hence "?i ≤ k" by auto
hence "t_v_evaluation (graph_interpretation G f) (atomic_disjunctions v k)"
using Suc(1) Suc(2) Suc(3) Suc(5) by auto
thus ?case using Suc(5) by auto
qed
qed
}
thus ?thesis using assms by auto
qed
lemma t_value_vertex:
assumes "t_v_evaluation (graph_interpretation G f) (atom (v, i))"
shows "f(v)=i"
proof(rule ccontr)
assume "f v ≠ i" hence "¬ t_v_evaluation (graph_interpretation G f) (atom (v, i))" by auto
hence "¬ t_v_evaluation (graph_interpretation G f) (atom (v, i))"
by auto
thus False using assms by simp
qed
lemma value2:
assumes "i≠j" and "F =¬.(atom (v, i) ∧. atom (v, j))"
shows "t_v_evaluation (graph_interpretation G f) F"
proof(rule ccontr)
assume "¬ t_v_evaluation (graph_interpretation G f) F"
hence "¬ t_v_evaluation (graph_interpretation G f) (¬.(atom (v, i) ∧. atom (v, j)))"
using assms(2) by auto
hence "t_v_evaluation (graph_interpretation G f) ((atom (v, i) ∧. atom (v, j)))"
by auto
hence "t_v_evaluation (graph_interpretation G f) (atom (v, i)) ∧
t_v_evaluation (graph_interpretation G f) (atom (v, j))"
by simp
hence "f(v)=i" and "f(v)=j" using t_value_vertex by auto
hence "i=j" by auto
thus False using assms(1) by auto
qed
lemma value3:
assumes "f(u)≠f(v)" and "F =¬.(atom (u, i) ∧. atom (v, i))"
shows "t_v_evaluation (graph_interpretation G f) F"
proof(rule ccontr)
assume "¬ t_v_evaluation (graph_interpretation G f) F"
hence
"¬ t_v_evaluation (graph_interpretation G f) (¬.(atom (u, i) ∧. atom (v, i)))"
using assms(2) by auto
hence "t_v_evaluation (graph_interpretation G f) ((atom (u, i) ∧. atom (v, i)))"
by auto
hence "t_v_evaluation (graph_interpretation G f) (atom (u, i)) ∧
t_v_evaluation (graph_interpretation G f) (atom (v, i))"
by auto
hence "f(u)=i" and "f(v)=i" using t_value_vertex by auto
hence "f(u)=f(v)" by auto
thus False using assms(1) by auto
qed
theorem coloring_satisfiable:
assumes "is_graph G" and "S ⊆ (𝒯 G k)" and
"coloring f k (induced_subgraph_from_vert G (vertices_set_formulas S))"
shows "satisfiable S"
proof-
let ?V = "vertices_set_formulas S"
let ?H = "induced_subgraph_from_vert G ?V"
have "(graph_interpretation ?H f) model S"
proof(unfold model_def)
show "∀ F ∈ S. t_v_evaluation (graph_interpretation ?H f) F"
proof
fix F assume "F ∈ S"
show "t_v_evaluation (graph_interpretation ?H f) F"
proof-
have 1: "vertices_formula F ⊆ ?V"
proof
fix v
assume "v ∈ (vertices_formula F)" thus "v ∈ ?V"
using `F ∈ S` by(unfold vertices_set_formulas_def,auto)
qed
have "F ∈ (ℱ G k) ∪ (𝒢 G k) ∪ (ℋ G k)"
using `F ∈ S` assms(2) by(unfold 𝒯_def,auto)
hence "F ∈ (ℱ G k) ∨ F ∈ (𝒢 G k) ∨ F ∈ (ℋ G k)" by auto
thus ?thesis
proof(rule disjE)
assume "F ∈ (ℱ G k)"
hence "∃v∈V[G]. F = atomic_disjunctions v (k-1)" by(unfold ℱ_def,auto)
then obtain v
where v: "v∈V[G]" and F: "F = atomic_disjunctions v (k-1)"
by auto
have "v∈?V" using F vertices_disjunction[of "F"] 1 by auto
hence "v∈ V[?H]" by(unfold induced_subgraph_from_vert_def, auto)
hence "f(v) < k" using coloring_def[of "f" "k" "?H"] assms(3)
by (simp add: coloring_def order_less_imp_le)
thus ?thesis using F value1[of v G f k F]
by (metis One_nat_def Suc_pred ‹v ∈ V[induced_subgraph_from_vert G (vertices_set_formulas S)]›
atomic_disjunctions.simps(2) bot_nat_0.extremum_strict
bot_nat_0.not_eq_extremum nat_less_le t_v_evaluation.simps(6) t_value_vertex value1)
next
assume "F ∈ (𝒢 G k) ∨ F ∈ (ℋ G k)"
thus ?thesis
proof(rule disjE)
assume "F ∈ (𝒢 G k)"
hence "∃v.∃i.∃j. F = ¬.(atom (v, i) ∧. atom(v,j)) ∧ ( i≠j)"
by(unfold 𝒢_def, auto)
then obtain v i j
where "F = ¬.(atom (v, i) ∧. atom(v,j))" and "(i≠j)"
by auto
thus "t_v_evaluation (graph_interpretation ?H f) F"
using value2[OF `i≠j` `F = ¬.(atom (v, i) ∧. atom(v,j))`]
by auto
next
assume " F ∈ (ℋ G k)"
hence "∃u.∃v.∃i.(F = ¬.(atom (u, i) ∧. atom(v,i)) ∧ (u,v)∈E[G])"
by(unfold ℋ_def, auto)
then obtain u v i
where F: "F = ¬.(atom (u, i) ∧. atom(v,i))" and uv: "(u,v)∈E[G]"
by auto
have "vertices_formula F = {u,v}" using F by auto
hence "{u,v} ⊆ ?V" using 1 by auto
hence "(u,v)∈E[?H]" using uv by(unfold induced_subgraph_from_vert_def, auto)
hence "f(u) ≠f(v)" using coloring_def[of "f" "k" "?H"] assms(3)
by auto
show ?thesis
using value3[OF `f(u) ≠f(v)` `F = ¬.(atom (u, i) ∧. atom(v,i))`]
by auto
qed
qed
qed
qed
qed
thus "satisfiable S" by(unfold satisfiable_def, auto)
qed
fun graph_coloring :: "(('v × nat) ⇒ bool) ⇒ nat ⇒ ('v ⇒ nat)"
where
"graph_coloring I k = (λv.(THE i. (t_v_evaluation I (atom (v,i))) ∧ 0 ≤i ∧ i<k))"
lemma unicity:
assumes "(t_v_evaluation I (atom (v, i)) ∧ 0 ≤ i ∧ i < k)"
and "∀j. (0≤j ∧ j<k ∧ i≠j) ⟶ (t_v_evaluation I (¬.(atom (v, i) ∧. atom(v,j))))"
shows "∀j. (0≤j ∧ j<k ∧ i≠j) ⟶ ¬ t_v_evaluation I (atom (v, j))"
proof(rule allI, rule impI)
fix j
assume hip: "0≤j ∧ j<k ∧ i≠j"
show "¬t_v_evaluation I (atom (v, j))"
using assms(1,2) hip by auto
qed
lemma existence:
assumes "(t_v_evaluation I (atom (v, i)) = Ttrue ∧ 0≤i ∧ i < k)"
and "∀j. (0≤j ∧ j<k ∧ i≠j) ⟶ ¬ t_v_evaluation I (atom (v, j))"
shows "(∀x. (t_v_evaluation I (atom (v, x)) ∧ 0≤x ∧ x < k) ⟶ x = i)"
proof(rule allI)
fix x
show "t_v_evaluation I (atom (v, x)) ∧ 0 ≤ x ∧ x < k ⟶ x = i"
proof(rule impI)
assume hip: "t_v_evaluation I (atom (v, x)) ∧ 0 ≤x ∧ x < k" show "x = i"
proof(rule ccontr)
assume 1: "x ≠ i"
have "0≤x ∧ x < k" using hip by auto
hence "¬ t_v_evaluation I (atom (v, x))" using 1 assms(2) by auto
thus False using hip by auto
qed
qed
qed
lemma exist_unicity1:
assumes "(t_v_evaluation I (atom (v, i)) ∧ 0≤i ∧ i < k)"
and "∀j. (0≤j ∧ j<k ∧ i≠j) ⟶ (t_v_evaluation I (¬.(atom (v, i) ∧. atom(v,j))))"
shows "(∀x. (t_v_evaluation I (atom (v, x)) ∧ 0≤x ∧ x < k) ⟶ x = i)"
using assms(1,2) by auto
lemma exist_unicity2:
assumes "(t_v_evaluation I (atom (v, i)) ∧ 0≤i ∧ i < k )" and
"(⋀x. (t_v_evaluation I (atom (v, x)) ∧ 0≤x ∧ x < k) ⟹ x = i)"
shows "(THE a. (t_v_evaluation I (atom (v,a)) ∧ 0≤a ∧ a < k )) = i"
using assms by (rule the_equality)
lemma exist_unicity:
assumes "(t_v_evaluation I (atom (v, i)) ∧ 0≤i ∧ i<k )" and
"∀j. (0≤j ∧ j<k ∧ i≠j) ⟶ (t_v_evaluation I (¬.(atom (v, i) ∧. atom(v,j))))"
shows "(THE a. (t_v_evaluation I (atom (v,a)) ∧ 0≤a ∧ a < k )) = i"
using assms exist_unicity1[of "I" "v" "i" "k" ] exist_unicity2[of "I" "v" "i" "k"]
by fastforce
lemma unique_color:
assumes "v ∈ V[G]"
shows "∀i j.(0≤i ∧ 0≤j ∧ i<k ∧ j<k ∧ i≠j) ⟶ (¬.(atom (v, i) ∧. atom(v,j))∈ (𝒢 G k))"
proof(rule allI )+
fix i j
show "0 ≤ i ∧ 0 ≤ j ∧ i < k ∧ j< k ∧ i ≠ j ⟶ ¬.(atom (v, i) ∧. atom (v, j)) ∈ (𝒢 G k)"
proof(rule impI)
assume "0 ≤ i ∧ 0 ≤ j ∧ i < k ∧ j < k ∧ i ≠ j"
thus "¬.(atom (v, i) ∧. atom (v, j)) ∈ (𝒢 G k)"
using `v ∈ V[G]` by(unfold 𝒢_def, auto)
qed
qed
lemma different_colors:
assumes "u ∈ V[G]" and "v∈V[G]" and "(u,v)∈E[G]"
shows "∀i.(0≤i ∧ i<k) ⟶ (¬.(atom (u, i) ∧. atom(v,i))∈ (ℋ G k))"
proof(rule allI)
fix i
show "0≤i ∧ i<k ⟶ (¬.(atom (u, i) ∧. atom(v,i))∈ (ℋ G k))"
proof(rule impI)
assume "0≤i ∧ i<k"
thus "¬.(atom (u, i) ∧. atom(v,i))∈ (ℋ G k)"
using assms by(unfold ℋ_def, auto)
qed
qed
lemma atom_value:
assumes "(t_v_evaluation I (atomic_disjunctions u k))"
shows "∃i.(t_v_evaluation I (atom (u,i))) ∧ 0 ≤ i ∧ i≤k"
proof-
have "(t_v_evaluation I (atomic_disjunctions u k)) ⟹
∃i.(t_v_evaluation I (atom (u,i))) ∧ 0≤i ∧ i≤k"
proof(induct k)
case(0)
assume "(t_v_evaluation I (atomic_disjunctions u 0))"
thus "∃i. t_v_evaluation I (atom (u, i)) ∧ 0≤i ∧ i ≤ 0" by auto
next
case(Suc k)
from Suc(1) Suc(2) show ?case
proof-
have "t_v_evaluation I (atom (u, (Suc k)) ∨. (atomic_disjunctions u k))"
using Suc(2) by auto
hence "t_v_evaluation I (atom (u, (Suc k))) ∨
(t_v_evaluation I (atomic_disjunctions u k))"
by auto
thus ?case
proof(rule disjE)
assume "t_v_evaluation I (atom (u, (Suc k)))"
thus ?case by(rule_tac x= "Suc k" in exI, auto)
next
assume "t_v_evaluation I (atomic_disjunctions u k)"
thus ?case using Suc(1) by auto
qed
qed
qed
thus ?thesis using assms by auto
qed
lemma coloring_function:
assumes "u ∈ V[G]" and "I model (𝒯 G k)" and "0 < k"
shows "∃!i. (t_v_evaluation I (atom (u,i)) ∧ 0 ≤ i ∧ i < k)
∧ graph_coloring I k u = i"
proof-
have F_subset: "ℱ G k ⊆ 𝒯 G k"
unfolding 𝒯_def by blast
have u_disj_in_F: "atomic_disjunctions u (k-1) ∈ ℱ G k"
using assms(1) unfolding ℱ_def by blast
have u_disj_sat: "t_v_evaluation I (atomic_disjunctions u (k-1))"
using assms(2) u_disj_in_F F_subset
unfolding model_def by blast
obtain i where
i_atom: "t_v_evaluation I (atom (u, i))" and
i_bound: "0 ≤ i" "i ≤ k - 1"
using atom_value[OF u_disj_sat] by auto
have i_lt_k: "i < k" using i_bound assms(3)
by simp
have G_subset: "𝒢 G k ⊆ 𝒯 G k"
unfolding 𝒯_def by blast
have uniq_formulas:
"∀j. 0 ≤ j ∧ j < k ∧ i ≠ j ⟶
t_v_evaluation I (¬.(atom (u, i) ∧. atom(u, j)))"
proof (intro allI impI)
fix j
assume jh: "0 ≤ j ∧ j < k ∧ i ≠ j"
have "¬.(atom (u, i) ∧. atom(u, j)) ∈ 𝒢 G k"
using unique_color[OF assms(1)] jh i_lt_k by blast
thus "t_v_evaluation I (¬.(atom (u, i) ∧. atom(u, j)))"
using assms(2) G_subset unfolding model_def by blast
qed
have no_other: "∀j. 0 ≤ j ∧ j < k ∧ i ≠ j ⟶
¬ t_v_evaluation I (atom (u, j))"
using unicity[OF _ uniq_formulas] i_atom i_lt_k by blast
have the_eq: "graph_coloring I k u = i"
proof -
have "(THE a. t_v_evaluation I (atom (u, a)) ∧ 0 ≤ a ∧ a < k) = i"
proof (rule the_equality)
show "t_v_evaluation I (atom (u, i)) ∧ 0 ≤ i ∧ i < k"
using i_atom i_bound i_lt_k by blast
next
fix x
assume "t_v_evaluation I (atom (u, x)) ∧ 0 ≤ x ∧ x < k"
hence "t_v_evaluation I (atom (u, x))" "0 ≤ x" "x < k" by auto
show "x = i"
proof (rule ccontr)
assume "x ≠ i"
hence "¬ t_v_evaluation I (atom (u, x))"
using no_other ‹0 ≤ x› ‹x < k› by blast
thus False using ‹t_v_evaluation I (atom (u, x))› by contradiction
qed
qed
thus ?thesis by simp
qed
show ?thesis
proof (rule ex1I)
show "(t_v_evaluation I (atom (u, i)) ∧ 0 ≤ i ∧ i < k)
∧ graph_coloring I k u = i"
using i_atom i_bound i_lt_k the_eq by blast
next
fix j
assume "(t_v_evaluation I (atom (u, j)) ∧ 0 ≤ j ∧ j < k)
∧ graph_coloring I k u = j"
hence j_atom: "t_v_evaluation I (atom (u, j))" and
j_lt_k: "j < k" and j_nn: "0 ≤ j" by auto
show "j = i"
proof (rule ccontr)
assume "j ≠ i"
hence "¬ t_v_evaluation I (atom (u, j))"
using no_other j_lt_k j_nn by blast
thus False using j_atom by contradiction
qed
qed
qed
lemma ℋ1:
assumes "(t_v_evaluation I (atom (u, a)) ∧ 0≤a ∧ a≤k )" and
"(t_v_evaluation I (atom (v, b)) ∧ 0≤b ∧ b≤k )" and
"∀i.(0≤i ∧ i≤k) ⟶ (t_v_evaluation I (¬.(atom (u, i) ∧. atom(v,i))))"
shows "a≠b"
proof(rule ccontr)
assume "¬ a ≠ b"
hence "a=b" by auto
hence "t_v_evaluation I (atom (u, a))" and "t_v_evaluation I (atom (v, a))" using assms by auto
hence "t_v_evaluation I (atom (u, a) ∧. atom(v,a))" by auto
hence "¬t_v_evaluation I (¬.(atom (u, a) ∧. atom(v,a)))" by auto
moreover
have "0≤a ∧ a≤k" using assms(1) by auto
hence "t_v_evaluation I (¬.(atom (u, a) ∧. atom(v,a)))" using assms(3) by auto
ultimately show False by auto
qed
lemma distinct_colors:
assumes "is_graph G" and "(u,v) ∈ E[G]" and I: "I model (𝒯 G k)" and "0 < k"
shows "graph_coloring I k u ≠ graph_coloring I k v"
proof-
have "u ≠ v" and "u ∈ V[G]" and "v ∈ V[G]" using `(u,v) ∈ E[G]` `is_graph G`
by(unfold is_graph_def, auto)
have "∃!i. (t_v_evaluation I (atom (u,i)) ∧ 0≤i ∧ i<k) ∧ graph_coloring I k u = i"
using coloring_function[OF `u ∈ V[G]` I]
using assms(4) by fastforce
then obtain i where i1: "(t_v_evaluation I (atom (u,i)) ∧ 0≤i ∧ i≤k)" and i2: "graph_coloring I k u = i"
by auto
have "∃!j. (t_v_evaluation I (atom (v,j)) ∧ 0≤j ∧ j<k) ∧ graph_coloring I k v = j"
using coloring_function[OF `v ∈ V[G]` I] using assms(4) by fastforce
then obtain j where j1: "(t_v_evaluation I (atom (v,j)) ∧ 0≤j ∧ j≤k)" and
j2: "graph_coloring I k v = j" by auto
have "∀i.(0≤i ∧ i<k) ⟶ (¬.(atom (u, i) ∧. atom(v,i))∈ ℋ G k)"
using `u ∈ V[G]` `v ∈ V[G]` `(u,v) ∈ E[G]` by(unfold ℋ_def, auto)
hence "∀i. (0≤i ∧ i<k) ⟶ ¬.(atom (u, i) ∧. atom(v,i)) ∈ 𝒯 G k"
by(unfold 𝒯_def, auto)
hence "∀i. (0≤i ∧ i<k) ⟶ (t_v_evaluation I (¬.(atom (u, i) ∧. atom(v,i))))"
using assms(2) I model_def[of I "𝒯 G k"] by blast
hence "i ≠ j" using i1 j1 ℋ1[of "I" "u" "i" "k" "v" "j"]
using
‹∃!i. (t_v_evaluation I (atom (u, i)) ∧ 0 ≤ i ∧ i < k) ∧ graph_coloring I k u = i›
i2 by auto
thus ?thesis using i2 j2 by auto
qed
theorem satisfiable_coloring:
assumes "is_graph G" and "satisfiable (𝒯 G k)" and "0 < k"
shows "colorable G k"
proof(unfold colorable_def)
show "∃f. coloring f k G"
proof-
from assms(2) have "∃I. I model (𝒯 G k)" by(unfold satisfiable_def)
then obtain I where I: "I model (𝒯 G k)" by auto
hence "coloring (graph_coloring I k) k G"
proof(unfold coloring_def)
show
"(∀u. u ∈ V[G] ⟶ (graph_coloring I k u) < k) ∧ (∀u v. (u, v) ∈ E[G]
⟶ graph_coloring I k u ≠ graph_coloring I k v)"
proof(rule conjI)
show "∀u. u ∈ V[G] ⟶ graph_coloring I k u < k"
proof(rule allI, rule impI)
fix u
assume "u ∈ V[G]"
hence "∃!i. (t_v_evaluation I (atom (u, i)) ∧ 0 ≤ i ∧ i < k) ∧ graph_coloring I k u = i"
using I coloring_function[of u G I "k"]
using assms(3) by linarith
then obtain i
where i: "(t_v_evaluation I (atom (u, i)) ∧ 0 ≤ i ∧ i < k) ∧ graph_coloring I k u = i"
by auto
thus "graph_coloring I k u < k"
by blast
qed
next
show
"∀u v. (u, v) ∈ E[G] ⟶
graph_coloring I k u ≠ graph_coloring I k v"
proof(rule allI,rule allI,rule impI)
fix u v
assume "(u,v) ∈ E[G]"
thus "graph_coloring I k u ≠ graph_coloring I k v"
using distinct_colors[OF `is_graph G` `(u,v) ∈ E[G]` I]
using assms(3) by blast
qed
qed
qed
thus "∃f. coloring f k G" by auto
qed
qed
lemma deBruijn_Erdos_coloring_for_finite_induced_subgraphs_aux:
assumes "is_graph (G::('vertices:: countable) set × ('vertices × 'vertices) set)"
and "∀H. (is_induced_subgraph H G ∧ finite_graph H ⟶ colorable H k)" and "0 < k"
shows "colorable G k"
proof-
have "∀ S. S ⊆ (𝒯 G k) ∧ (finite S) ⟶ satisfiable S"
proof(rule allI, rule impI)
fix S assume "S ⊆ (𝒯 G k) ∧ (finite S)"
hence hip1: "S ⊆ (𝒯 G k)" and hip2: "finite S" by auto
show "satisfiable S"
proof -
let ?V = "vertices_set_formulas S"
let ?H = "(?V, E[G] ∩ (?V × ?V))"
have "is_induced_subgraph ?H G"
using assms(1) hip1 induced_subgraph[of G S k]
by(unfold induced_subgraph_from_vert_def, auto)
moreover
have "finite_graph ?H"
using assms(1) hip1 hip2 finite_subgraph[of G S k]
by(unfold induced_subgraph_from_vert_def, auto)
ultimately
have "colorable ?H k"
using assms by auto
hence "∃f. coloring f k ?H " by(unfold colorable_def, auto)
then obtain f where "coloring f k ?H" by auto
thus "satisfiable S" using coloring_satisfiable[OF assms(1) hip1]
by(unfold induced_subgraph_from_vert_def, auto)
qed
qed
hence "satisfiable (𝒯 G k)" using
Compactness_Theorem by auto
thus ?thesis using assms(1) satisfiable_coloring
using assms(3) by blast
qed
lemma coloring_induced_subgraphs_and_subgraphs1:
assumes "is_graph (G::('vertices:: countable) set × ('vertices × 'vertices) set)"
shows "(∀H. (is_induced_subgraph H G ⟶ colorable H k)) ⟷
(∀H. (is_subgraph H G ⟶ colorable H k))"
proof
show "∀H. is_induced_subgraph H G ⟶ colorable H k ⟹
∀H. is_subgraph H G ⟶ colorable H k"
proof-
assume "∀H. is_induced_subgraph H G ⟶ colorable H k"
show " ∀H. is_subgraph H G ⟶ colorable H k "
proof
fix H
show "is_subgraph H G ⟶ colorable H k"
proof(rule impI)
assume hip: "is_subgraph H G"
let ?indH = "induced_subgraph_from_vert G (V[H])"
have "is_induced_subgraph ?indH G"
by (meson hip is_induced_subgraph_from_vert_is_induced_subgraph is_subgraph_def)
have "colorable ?indH k"
by (simp add: ‹∀H. is_induced_subgraph H G ⟶ colorable H k›
‹is_induced_subgraph (induced_subgraph_from_vert G (V[H])) G›)
have "is_subgraph H ?indH"
by (simp add: ‹is_subgraph H G› subgraph_is_subgraph_ind_subgraph_vert)
thus "colorable H k" using "colorable_subgraph"
using ‹colorable (induced_subgraph_from_vert G (V[H])) k›
‹is_subgraph H (induced_subgraph_from_vert G (V[H]))› by blast
qed
qed
qed
next
show "∀H. is_subgraph H G ⟶ colorable H k ⟹ ∀H. is_induced_subgraph H G ⟶ colorable H k"
by (simp add: induced_subgraph_is_subgraph)
qed
theorem deBruijn_Erdos_coloring:
assumes "is_graph (G::('vertices:: countable) set × ('vertices × 'vertices) set)"
and "∀H. (is_subgraph H G ∧ finite_graph H ⟶ colorable H k)"
shows "colorable G k"
proof(rule disjE)
show "k = 0 ∨ k ≠ 0" by auto
next
assume "k = 0"
have *: "∀H. is_subgraph H G ∧ finite_graph H ⟶ V[H] = {}"
by (metis ‹k = 0› assms(2) coloring_nonemptygraph less_imp_neq)
have **: "V[G] = {}"
proof(rule ccontr)
assume "V[G] ≠ {}"
hence "∃v. v∈V[G]" by auto
then obtain v where "v∈V[G]" by auto
hence "is_subgraph ({v}, {(v,v)}) G ∧ finite_graph ({v}, {(v,v)})"
by (metis "*" empty_not_insert empty_subsetI finite.emptyI finite.insertI finite_graph_def
fst_conv induced_subgraph_from_vert_def induced_subraph_from_vert_is_subgraph insert_subset)
thus False using * by auto
qed
thus ?thesis using assms
by (simp add: colorable_def coloring_def is_graph_def)
next
assume "k≠0"
hence "k > 0" by auto
thus ?thesis
using assms(1,2) coloring_induced_subgraphs_and_subgraphs1
induced_subgraph_is_subgraph deBruijn_Erdos_coloring_for_finite_induced_subgraphs_aux
by blast
qed
corollary deBruijn_Erdos_coloring_for_finite_induced_subgraphs:
assumes "is_graph (G::('vertices:: countable) set × ('vertices × 'vertices) set)"
and "∀H. (is_induced_subgraph H G ∧ finite_graph H ⟶ colorable H k)"
shows "colorable G k" using assms deBruijn_Erdos_coloring
by (metis colorable_subgraph finite_graph_def induced_subgraph_from_vert_def
is_induced_subgraph_from_vert_is_induced_subgraph is_subgraph_def
prod.sel(1) subgraph_is_subgraph_ind_subgraph_vert)
end