Theory Approx_VC_Hoare

section "Vertex Cover"

theory Approx_VC_Hoare
imports "HOL-Hoare.Hoare_Logic"
begin

text ‹The algorithm is classical, the proof is based on and augments the one
by Berghammer and M\"uller-Olm \<^cite>‹"BerghammerM03"›.›

subsection "Graph"

text ‹A graph is simply a set of edges, where an edge is a 2-element set.›

definition vertex_cover :: "'a set set ⇒ 'a set ⇒ bool" where
"vertex_cover E C = (∀e ∈ E. e ∩ C ≠ {})"

abbreviation matching :: "'a set set ⇒ bool" where
"matching M ≡ pairwise disjnt M"

lemma card_matching_vertex_cover:
  "⟦ finite C;  matching M;  M ⊆ E;  vertex_cover E C ⟧ ⟹ card M ≤ card C"
apply(erule card_le_if_inj_on_rel[where r = "λe v. v ∈ e"])
 apply (meson disjnt_def disjnt_iff vertex_cover_def subsetCE)
by (meson disjnt_iff pairwise_def)


subsection "The Approximation Algorithm"

text ‹Formulated using a simple(!) predefined Hoare-logic.
This leads to a streamlined proof based on standard invariant reasoning.

The nondeterministic selection of an element from a set ‹F› is simulated by @{term "SOME x. x ∈ F"}.
The ‹SOME› operator is built into HOL: @{term "SOME x. P x"} denotes some ‹x› that satisfies ‹P›
if such an ‹x› exists; otherwise it denotes an arbitrary element. Note that there is no
actual nondeterminism involved: @{term "SOME x. P x"} is some fixed element
but in general we don't know which one. Proofs about ‹SOME› are notoriously tedious.
Typically it involves showing first that @{prop "∃x. P x"}. Then @{thm someI_ex} implies
@{prop"P (SOME x. P x)"}. There are a number of (more) useful related theorems:
just click on @{thm someI_ex} to be taken there.›

text ‹Convenient notation for choosing an arbitrary element from a set:›
abbreviation "some A ≡ SOME x. x ∈ A"

locale Edges =
  fixes E :: "'a set set"
  assumes finE: "finite E"
  assumes edges2: "e ∈ E ⟹ card e = 2"
begin

text ‹The invariant:›

definition "inv_matching C F M =
  (matching M ∧ M ⊆ E ∧ card C ≤ 2 * card M ∧ (∀e ∈ M. ∀f ∈ F. e ∩ f = {}))"

definition invar :: "'a set ⇒ 'a set set ⇒ bool" where
"invar C F = (F ⊆ E ∧ vertex_cover (E-F) C ∧ finite C ∧ (∃M. inv_matching C F M))"

text ‹Preservation of the invariant by the loop body:›

lemma invar_step:
  assumes "F ≠ {}" "invar C F"
  shows "invar (C ∪ some F) (F - {e' ∈ F. some F ∩ e' ≠ {}})"
proof -
  from assms(2) obtain M where "F ⊆ E" and vc: "vertex_cover (E-F) C" and fC: "finite C"
    and m: "matching M" "M ⊆ E" and card: "card C ≤ 2 * card M"
    and disj: "∀e ∈ M. ∀f ∈ F. e ∩ f = {}"
  by (auto simp: invar_def inv_matching_def)
  let ?e = "SOME e. e ∈ F"
  have "?e ∈ F" using ‹F ≠ {}› by (simp add: some_in_eq)
  hence fe': "finite ?e" using ‹F ⊆ E› edges2 by(intro card_ge_0_finite) auto
  have "?e ∉ M" using edges2 ‹?e ∈ F› disj ‹F ⊆ E› by fastforce
  have card': "card (C ∪ ?e) ≤ 2 * card (insert ?e M)"
    using ‹?e ∈ F› ‹?e ∉ M› card_Un_le[of C ?e] ‹F ⊆ E› edges2 card finite_subset[OF m(2) finE]
    by fastforce
  let ?M = "M ∪ {?e}"
  have vc': "vertex_cover (E - (F - {e' ∈ F. ?e ∩ e' ≠ {}})) (C ∪ ?e)"
    using vc by(auto simp: vertex_cover_def)
  have m': "inv_matching (C ∪ ?e) (F - {e' ∈ F. ?e ∩ e' ≠ {}}) ?M"
    using m card' ‹F ⊆ E› ‹?e ∈ F› disj
    by(auto simp: inv_matching_def Int_commute disjnt_def pairwise_insert)
  show ?thesis using ‹F ⊆ E› vc' fC fe' m' by(auto simp add: invar_def Let_def)
qed


lemma approx_vertex_cover:
"VARS C F
  {True}
  C := {};
  F := E;
  WHILE F ≠ {}
  INV {invar C F}
  DO C := C ∪ some F;
     F := F - {e' ∈ F. some F ∩ e' ≠ {}}
  OD
  {vertex_cover E C ∧ (∀C'. finite C' ∧ vertex_cover E C' ⟶ card C ≤ 2 * card C')}"
proof (vcg, goal_cases)
  case (1 C F)
  have "inv_matching {} E {}" by (auto simp add: inv_matching_def)
  with 1 show ?case by (auto simp add: invar_def vertex_cover_def)
next
  case (2 C F)
  thus ?case using invar_step[of F C] by(auto simp: Let_def)
next
  case (3 C F)
  then obtain M :: "'a set set" where
    post: "vertex_cover E C" "matching M" "M ⊆ E" "card C ≤ 2 * card M"
    by(auto simp: invar_def inv_matching_def)

  have opt: "card C ≤ 2 * card C'" if C': "finite C'" "vertex_cover E C'" for C'
  proof -
    note post(4)
    also have "2 * card M ≤ 2 * card C'"
    using card_matching_vertex_cover[OF C'(1) post(2,3) C'(2)] by simp
    finally show "card C ≤ 2 * card C'" .
  qed

  show ?case using post(1) opt by auto
qed

end (* locale Graph *)

subsection "Version for Hypergraphs"

text ‹Almost the same. We assume that the degree of every edge is bounded.›

locale Bounded_Hypergraph =
  fixes E :: "'a set set"
  fixes k :: nat
  assumes finE: "finite E"
  assumes edge_bnd: "e ∈ E ⟹ finite e ∧ card e ≤ k"
  assumes E1: "{} ∉ E"
begin

definition "inv_matching C F M =
  (matching M ∧ M ⊆ E ∧ card C ≤ k * card M ∧ (∀e ∈ M. ∀f ∈ F. e ∩ f = {}))"

definition invar :: "'a set ⇒ 'a set set ⇒ bool" where
"invar C F = (F ⊆ E ∧ vertex_cover (E-F) C ∧ finite C ∧ (∃M. inv_matching C F M))"

lemma invar_step:
  assumes "F ≠ {}" "invar C F"
  shows "invar (C ∪ some F) (F - {e' ∈ F. some F ∩ e' ≠ {}})"
proof -
  from assms(2) obtain M where "F ⊆ E" and vc: "vertex_cover (E-F) C" and fC: "finite C"
    and m: "matching M" "M ⊆ E" and card: "card C ≤ k * card M"
    and disj: "∀e ∈ M. ∀f ∈ F. e ∩ f = {}"
  by (auto simp: invar_def inv_matching_def)
  let ?e = "SOME e. e ∈ F"
  have "?e ∈ F" using ‹F ≠ {}› by (simp add: some_in_eq)
  hence fe': "finite ?e" using ‹F ⊆ E› assms(2) edge_bnd by blast
  have "?e ∉ M" using E1 ‹?e ∈ F› disj ‹F ⊆ E› by fastforce
  have card': "card (C ∪ ?e) ≤ k * card (insert ?e M)"
    using ‹?e ∈ F› ‹?e ∉ M› card_Un_le[of C ?e] ‹F ⊆ E› edge_bnd card finite_subset[OF m(2) finE]
    by fastforce
  let ?M = "M ∪ {?e}"
  have vc': "vertex_cover (E - (F - {e' ∈ F. ?e ∩ e' ≠ {}})) (C ∪ ?e)"
    using vc by(auto simp: vertex_cover_def)
  have m': "inv_matching (C ∪ ?e) (F - {e' ∈ F. ?e ∩ e' ≠ {}}) ?M"
    using m card' ‹F ⊆ E› ‹?e ∈ F› disj
    by(auto simp: inv_matching_def Int_commute disjnt_def pairwise_insert)
  show ?thesis using ‹F ⊆ E› vc' fC fe' m' by(auto simp add: invar_def Let_def)
qed


lemma approx_vertex_cover_bnd:
"VARS C F
  {True}
  C := {};
  F := E;
  WHILE F ≠ {}
  INV {invar C F}
  DO C := C ∪ some F;
     F := F - {e' ∈ F. some F ∩ e' ≠ {}}
  OD
  {vertex_cover E C ∧ (∀C'. finite C' ∧ vertex_cover E C' ⟶ card C ≤ k * card C')}"
proof (vcg, goal_cases)
  case (1 C F)
  have "inv_matching {} E {}" by (auto simp add: inv_matching_def)
  with 1 show ?case by (auto simp add: invar_def vertex_cover_def)
next
  case (2 C F)
  thus ?case using invar_step[of F C] by(auto simp: Let_def)
next
  case (3 C F)
  then obtain M :: "'a set set" where
    post: "vertex_cover E C" "matching M" "M ⊆ E" "card C ≤ k * card M"
    by(auto simp: invar_def inv_matching_def)

  have opt: "card C ≤ k * card C'" if C': "finite C'" "vertex_cover E C'" for C'
  proof -
    note post(4)
    also have "k * card M ≤ k * card C'"
    using card_matching_vertex_cover[OF C'(1) post(2,3) C'(2)] by simp
    finally show "card C ≤ k * card C'" .
  qed

  show ?case using post(1) opt by auto
qed

end (* locale Bounded_Hypergraph *)

end