Theory k_coloring

(* De Bruijn-Erdős  k-coloring theorem 
   Fabian Fernando Serrano Suárez  UNAL Manizales
   Thaynara Arielly de Lima        Universidade Federal de Goiáis 
   Mauricio Ayala-Rincón           Universidade de Brasília
*)


(*<*)
theory k_coloring
imports PropCompactness
begin
(*>*)

section ‹de Bruijn-Erd\H{o}s k-coloring theorem for countable infinite graphs›

text‹This section formalizes de Bruijn-Erd\H{o}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_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]))"

lemma  (* Well-definedness of the above definition *)
  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"


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 FF = {}"
| "vertices_formula TT = {}"
| "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


(*>*)


definition subgraph_aux :: "'v digraph ⇒ 'v set ⇒'v digraph" where
  "subgraph_aux G V ≡  (V, E[G] ∩ (V × V))"

lemma induced_subgraph: 
 assumes "is_graph G" and "S ⊆(𝒯 G k)"
 shows "is_induced_subgraph (subgraph_aux 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 (simp add: subgraph_aux_def)
qed

lemma finite_subgraph:
  assumes "is_graph G" and "S ⊆ (𝒯 G k)" and "finite S"
  shows "finite_graph (subgraph_aux 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 (simp add: finite_graph_def subgraph_aux_def) 
qed 

(*>*)


fun graph_interpretation :: "'v digraph ⇒ ('v ⇒ nat) ⇒ (('v × nat) ⇒ v_truth)"  where
"graph_interpretation G f = (λ(v,i).(if v ∈ V[G] ∧ f(v) = i  then Ttrue else Ffalse))"

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 = Ttrue" 
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 = Ttrue"
  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)) =  Ttrue"
      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 )) =  Ttrue"
      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) = Ttrue"
      using v_disjunction_def 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)) =  Ffalse"
        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) = Ttrue" 
      using  Suc(1) Suc(2) Suc(3)  Suc(5)  by auto
      thus ?case using  Suc(5)  v_disjunction_def 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)) = Ttrue"
  shows  "f(v)=i"
proof(rule ccontr)
  assume  "f v ≠ i" hence "t_v_evaluation (graph_interpretation G f) (atom (v, i)) ≠ Ttrue" by auto
  hence "t_v_evaluation (graph_interpretation G f) (atom (v, i)) = Ffalse" 
  using non_Ttrue[of "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 = Ttrue"
proof(rule ccontr)
  assume "t_v_evaluation (graph_interpretation G f) F ≠ Ttrue"
  hence  "t_v_evaluation (graph_interpretation G f) (¬.(atom (v, i) ∧. atom (v, j))) ≠ Ttrue"
    using assms(2) by auto
  hence "t_v_evaluation (graph_interpretation G f) (¬.(atom (v, i) ∧. atom (v, j))) = Ffalse" using
  non_Ttrue[of "graph_interpretation G f" "¬.(atom (v, i) ∧. atom (v, j))" ]
    by auto     
  hence  "t_v_evaluation (graph_interpretation G f) ((atom (v, i) ∧. atom (v, j))) = Ttrue" 
  using  NegationValues1[of "graph_interpretation G f" "(atom (v, i) ∧. atom (v, j))"] by auto
  hence "t_v_evaluation (graph_interpretation G f) (atom (v, i)) = Ttrue" and
  "t_v_evaluation (graph_interpretation G f) (atom (v, j)) = Ttrue"
  using ConjunctionValues[of "graph_interpretation G f" "atom (v, i)" "atom (v, j)"] by auto
  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 = Ttrue"
proof(rule ccontr)
  assume "t_v_evaluation (graph_interpretation G f) F ≠ Ttrue"
  hence(*and "finite S"*)
  "t_v_evaluation (graph_interpretation G f) (¬.(atom (u, i) ∧. atom (v, i))) ≠ Ttrue" 
    using assms(2) by auto
  hence "t_v_evaluation (graph_interpretation G f) (¬.(atom (u, i) ∧. atom (v, i))) = Ffalse"
    using
  non_Ttrue[of "graph_interpretation G f" "¬.(atom (u, i) ∧. atom (v, i))"]
    by auto     
  hence  "t_v_evaluation (graph_interpretation G f) ((atom (u, i) ∧. atom (v, i))) = Ttrue" 
    using  NegationValues1[of "graph_interpretation G f" "(atom (u, i) ∧. atom (v, i))"]
    by auto
  hence "t_v_evaluation (graph_interpretation G f) (atom (u, i)) = Ttrue" and
  "t_v_evaluation (graph_interpretation G f) (atom (v, i)) = Ttrue"
    using ConjunctionValues[of "graph_interpretation G f" "atom (u, i)" "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 (subgraph_aux G (vertices_set_formulas S))" 
  shows "satisfiable S"
proof- 
  let ?V = "vertices_set_formulas S"
  let ?H = "subgraph_aux G ?V"
  have "(graph_interpretation ?H f) model S"
  proof(unfold model_def) 
    show "∀ F ∈ S. t_v_evaluation (graph_interpretation ?H f) F  = Ttrue"
    proof 
      fix F assume "F ∈ S"
      show  "t_v_evaluation (graph_interpretation ?H f) F  = Ttrue"
      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 subgraph_aux_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 = Ttrue"
            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 subgraph_aux_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) ⇒ v_truth) ⇒ nat  ⇒ ('v ⇒ nat)"
  where
"graph_coloring I k = (λv.(THE i. (t_v_evaluation I (atom (v,i)) = Ttrue) ∧ 0≤i ∧ i≤k))" 

lemma unicity:
  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, i) ∧. atom(v,j))) = Ttrue)"
  shows "∀j. (0≤j ∧ j≤k ∧ i≠j) ⟶  t_v_evaluation I (atom (v, j)) = Ffalse"
proof(rule allI, rule impI)
  fix j
  assume hip: "0≤j ∧ j≤k ∧ i≠j"
  show "t_v_evaluation I (atom (v, j)) = Ffalse"
  proof(rule ccontr)
    assume "t_v_evaluation I (atom (v, j)) ≠ Ffalse" 
    hence "t_v_evaluation I (atom (v, j)) = Ttrue" using Bivaluation by blast
    hence 1: "t_v_evaluation I (atom (v, i) ∧. atom(v,j))  = Ttrue"
      using assms(1) v_conjunction_def by auto
    have "t_v_evaluation I (¬.(atom (v, i) ∧. atom(v,j))) = Ttrue"
      using hip assms(2)  by auto
    hence "t_v_evaluation I (atom (v, i) ∧. atom(v,j)) = Ffalse" 
      using NegationValues2  by blast
    thus False using 1  by auto
  qed      
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)) = Ffalse"
shows  "(∀x. (t_v_evaluation I (atom (v, x)) = Ttrue ∧ 0≤x ∧ x ≤ k) ⟶ x = i)"
proof(rule allI)
  fix x 
  show "t_v_evaluation I (atom (v, x)) = Ttrue ∧ 0 ≤ x ∧ x ≤ k ⟶ x = i"
  proof(rule impI)
    assume hip: "t_v_evaluation I (atom (v, x)) = Ttrue ∧ 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)) = Ffalse" 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)) = Ttrue ∧ 0≤i ∧ i ≤ k)"
  and "∀j. (0≤j ∧ j≤k ∧ i≠j) ⟶ (t_v_evaluation I (¬.(atom (v, i) ∧. atom(v,j))) = Ttrue)"
shows "(∀x. (t_v_evaluation I (atom (v, x)) = Ttrue ∧ 0≤x ∧ x ≤ k) ⟶ x = i)"
using assms  unicity[of "I" "v" "i" "k" ] existence[of "I" "v" "i" "k"]  by blast

lemma exist_unicity2:
  assumes "(t_v_evaluation I (atom (v, i)) = Ttrue ∧ 0≤i ∧ i ≤ k )" and
  "(⋀x. (t_v_evaluation I (atom (v, x)) = Ttrue ∧ 0≤x ∧ x ≤ k) ⟹ x = i)"
shows "(THE a. (t_v_evaluation I (atom (v,a)) = Ttrue ∧ 0≤a ∧ a ≤ k )) = i" 
  using assms by (rule the_equality)

lemma exist_unicity:
  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, i) ∧. atom(v,j))) = Ttrue)"
shows "(THE a. (t_v_evaluation I (atom (v,a)) = Ttrue ∧ 0≤a ∧ a ≤ k )) = i"  
 using assms  exist_unicity1[of "I" "v" "i" "k" ] exist_unicity2[of "I" "v" "i" "k"] by blast

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)) = Ttrue"  
  shows "∃i.(t_v_evaluation I (atom (u,i)) = Ttrue) ∧ 0≤i ∧ i≤k"
proof-
  have "(t_v_evaluation I (atomic_disjunctions u  k)) = Ttrue ⟹
  ∃i.(t_v_evaluation I (atom (u,i)) = Ttrue) ∧ 0≤i ∧ i≤k"
  proof(induct k)
    case(0)
    assume "(t_v_evaluation I (atomic_disjunctions u 0)) = Ttrue"
    thus "∃i. t_v_evaluation I (atom (u, i)) = Ttrue ∧ 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)) = Ttrue" 
        using Suc(2) by auto
      hence "t_v_evaluation I (atom (u, (Suc k))) = Ttrue ∨
      (t_v_evaluation I (atomic_disjunctions u k)) = Ttrue"
        using  DisjunctionValues[of I "(atom (u, (Suc k)))"] by auto
      thus ?case
        using Suc.hyps le_SucI by blast
    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)) = Ttrue ∧ 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)) = Ttrue"
    using assms(2) model_def[of I "𝒯 G k"] by auto
  hence "∃i.(t_v_evaluation I (atom (u,i)) = Ttrue ∧ 0≤i ∧ i≤k)"
    using atom_value by auto
  then obtain i where i: "(t_v_evaluation I (atom (u,i)) = Ttrue) ∧ 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)))  = Ttrue)" 
  using assms(2)  model_def[of I "𝒯 G k"] by blast
  hence "(THE a. (t_v_evaluation I (atom (u,a)) = Ttrue ∧ 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)) = Ttrue ∧ 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)) = Ttrue ∧ 0≤a ∧ a≤k )" and  "(t_v_evaluation I (atom (v, b)) = Ttrue ∧ 0≤b ∧ b≤k)"
  and "∀i.(0≤i ∧ i≤k) ⟶ (t_v_evaluation I (¬.(atom (u, i) ∧. atom(v,i))) = Ttrue)"
  shows "a≠b"  
proof(rule ccontr)
  assume  "¬ a ≠ b" 
  hence "a=b" by auto
  hence "t_v_evaluation I (atom (u, a)) = Ttrue" and  "t_v_evaluation I (atom (v, a)) = Ttrue" using assms by auto
  hence "t_v_evaluation I (atom (u, a) ∧. atom(v,a)) = Ttrue" using v_conjunction_def by auto
  hence "t_v_evaluation I (¬.(atom (u, a) ∧. atom(v,a))) = Ffalse" using v_negation_def by auto
  moreover
  have "0≤a ∧ a≤k" using assms(1) by auto
  hence "t_v_evaluation I (¬.(atom (u, a) ∧. atom(v,a))) = Ttrue" using assms(3) by auto
  finally show False by auto
qed

(* Include also in the document  *)
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)) = Ttrue ∧ 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)) = Ttrue ∧ 0≤i ∧ i≤k)" and i2: "graph_coloring I k u = i"
    by auto
  have  "∃!j. (t_v_evaluation I (atom (v,j)) = Ttrue ∧ 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)) = Ttrue ∧ 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))) = Ttrue)" 
  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


theorem deBruijn_Erdos_coloring:
  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 subgraph_aux_def, auto)         
      moreover      
      have "finite_graph ?H"
        using assms(1) hip1 hip2 finite_subgraph[of G S k]
        by(unfold subgraph_aux_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 subgraph_aux_def, auto)
    qed
  qed
  hence "satisfiable (𝒯 G k)" using 
   Compactness_Theorem by auto
  thus ?thesis using assms(1) satisfiable_coloring by blast
qed

end