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. ›
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 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
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})"
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}" by (unfold ℱ_def, auto)
then obtain v where v: "v∈V[G]" and "F∈{atomic_disjunctions v k}" by auto
hence "F = atomic_disjunctions v k" by auto
hence "vertices_formula F = {v}"
using vertices_disjunction[OF `F = atomic_disjunctions v k`] 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" by(unfold ℱ_def,auto)
then obtain v
where v: "v∈V[G]" and F: "F = atomic_disjunctions v k"
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 auto
thus ?thesis using F value1[OF `v∈V[?H]`] by auto
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)"
shows "∃!i. (t_v_evaluation I (atom (u,i)) ∧ 0≤i ∧ i≤k) ∧ graph_coloring I k u = i"
proof-
from `u ∈ V[G]`
have "atomic_disjunctions u k ∈ ℱ G k" by(induct, unfold ℱ_def, auto)
hence "atomic_disjunctions u k ∈ 𝒯 G k" by(unfold 𝒯_def, auto)
hence "(t_v_evaluation I (atomic_disjunctions u k))"
using assms(2) model_def[of I "𝒯 G k"] by auto
hence "∃i.(t_v_evaluation I (atom (u,i)) ∧ 0≤i ∧ i≤k)"
using atom_value by auto
then obtain i where i: "(t_v_evaluation I (atom (u,i))) ∧ 0≤i ∧ i≤k"
by auto
moreover
have "∀i j.(0≤i ∧ 0≤j ∧ i≤k ∧ j≤k ∧ i≠j)⟶
(¬.(atom (u, i) ∧.atom(u,j))∈ (𝒢 G k))"
using `u ∈ V[G]` unique_color[of "u"] by auto
hence "∀j.(0≤j ∧ j≤k ∧ i≠j) ⟶ (¬.(atom (u, i) ∧. atom(u,j))∈ 𝒯 G k)"
using i by(unfold 𝒯_def, auto)
hence
"∀j. (0≤j ∧ j≤k ∧ i≠j) ⟶ (t_v_evaluation I (¬.(atom (u, i) ∧. atom(u,j))))"
using assms(2) model_def[of I "𝒯 G k"] by blast
hence "(THE a. (t_v_evaluation I (atom (u,a)) ∧ 0≤a ∧ a ≤ k ))= i"
using i exist_unicity[of "I" "u"] by blast
hence "graph_coloring I k u = i" by auto
hence
"(t_v_evaluation I (atom (u,i)) ∧ 0≤i ∧ i≤k) ∧
graph_coloring I k u = i"
using i by auto
thus ?thesis by auto
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)"
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] by blast
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] by blast
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"] by blast
thus ?thesis using i2 j2 by auto
qed
theorem satisfiable_coloring:
assumes "is_graph G" and "satisfiable (𝒯 G 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]"
show "graph_coloring I k u ≤ k"
using coloring_function[OF `u ∈ V[G]` I] 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] by blast
qed
qed
qed
thus "∃f. coloring f k G" by auto
qed
qed
lemma 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"
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 by blast
qed
lemma coloring_induced_subgraphs_and_subgraphs:
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"
using assms(1,2) coloring_induced_subgraphs_and_subgraphs
induced_subgraph_is_subgraph deBruijn_Erdos_coloring_for_finite_induced_subgraphs
by blast
end