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