Theory Approx_MIS_Hoare

section "Independent Set"

theory Approx_MIS_Hoare
imports
  "HOL-Hoare.Hoare_Logic"
  "HOL-Library.Disjoint_Sets"
begin


text ‹The algorithm is classical, the proofs are inspired by the ones
by Berghammer and M\"uller-Olm \<^cite>‹"BerghammerM03"›.
In particular the approximation ratio is improved from ‹Δ+1› to ‹Δ›.›


subsection "Graph"

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

definition independent_vertices :: "'a set set ⇒ 'a set ⇒ bool" where
"independent_vertices E S ⟷ S ⊆ ⋃E ∧ (∀v1 v2. v1 ∈ S ∧ v2 ∈ S ⟶ {v1, v2} ∉ E)"

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

fun vertices :: "'a set set ⇒ 'a set" where
"vertices G = ⋃G"

abbreviation V :: "'a set" where
"V ≡ vertices E"

definition approximation_miv :: "nat ⇒ 'a set ⇒ bool" where
"approximation_miv n S ⟷ independent_vertices E S ∧ (∀S'. independent_vertices E S' ⟶ card S' ≤ card S * n)"

fun neighbors :: "'a ⇒ 'a set" where
"neighbors v = {u. {u,v} ∈ E}"

fun degree_vertex :: "'a ⇒ nat" where
"degree_vertex v = card (neighbors v)"

abbreviation Δ :: nat where
"Δ ≡ Max{degree_vertex u|u. u ∈ V}"

lemma finite_edges: "e ∈ E ⟹ finite e"
  using card_ge_0_finite and edges2 by force

lemma finite_V: "finite V"
  using finite_edges and finite_E by auto

lemma finite_neighbors: "finite (neighbors u)"
  using finite_V and rev_finite_subset [of V "neighbors u"] by auto

lemma independent_vertices_finite: "independent_vertices E S ⟹ finite S"
  by (metis rev_finite_subset independent_vertices_def vertices.simps finite_V)

lemma edge_ex_vertices: "e ∈ E ⟹ ∃u v. u ≠ v ∧ e = {u, v}"
proof -
  assume "e ∈ E"
  then have "card e = Suc (Suc 0)" using edges2 by auto
  then show "∃u v. u ≠ v ∧ e = {u, v}"
    by (metis card_eq_SucD insertI1)
qed

lemma Δ_pos [simp]: "E = {} ∨ 0 < Δ"
proof cases
  assume "E = {}"
  then show "E = {} ∨ 0 < Δ" by auto
next
  assume 1: "E ≠ {}"
  then have "V ≠ {}" using edges2 by fastforce
  moreover have "finite {degree_vertex u |u. u ∈ V}"
    by (metis finite_V finite_imageI Setcompr_eq_image)
  ultimately have 2: "Δ ∈ {degree_vertex u |u. u ∈ V}" using Max_in by auto
  have "Δ ≠ 0"
  proof
    assume "Δ = 0"
    with 2 obtain u where 3: "u ∈ V" and 4: "degree_vertex u = 0" by auto
    from 3 obtain e where 5: "e ∈ E" and "u ∈ e" by auto
    moreover with 4 have "∀v. {u, v} ≠ e" using finite_neighbors insert_absorb by fastforce
    ultimately show False using edge_ex_vertices by auto
  qed
  then show "E = {} ∨ 0 < Δ" by auto
qed

lemma Δ_max_degree: "u ∈ V ⟹ degree_vertex u ≤ Δ"
proof -
  assume H: "u ∈ V"
  have "finite {degree_vertex u |u. u ∈ V}"
    by (metis finite_V finite_imageI Setcompr_eq_image)
  with H show "degree_vertex u ≤ Δ" using Max_ge by auto
qed

subsection ‹Wei's algorithm: ‹(Δ+1)›-approximation›

text ‹The 'functional' part of the invariant, used to prove that the algorithm produces an independent set of vertices.›

definition inv_iv :: "'a set ⇒ 'a set ⇒ bool" where
"inv_iv S X ⟷ independent_vertices E S
            ∧ X ⊆ V
            ∧ (∀v1 ∈ (V - X). ∀v2 ∈ S. {v1, v2} ∉ E)
            ∧ S ⊆ X"

text ‹Strenghten the invariant with an approximation ratio ‹r›:›

definition inv_approx :: "'a set ⇒ 'a set ⇒ nat ⇒ bool" where
"inv_approx S X r ⟷ inv_iv S X ∧ card X ≤ card S * r"

text ‹Preservation of the functional invariant:›

lemma inv_preserv:
  fixes S :: "'a set"
    and X :: "'a set"
    and x :: "'a"
  assumes inv: "inv_iv S X"
      and x_def: "x ∈ V - X"
    shows "inv_iv (insert x S) (X ∪ neighbors x ∪ {x})"
proof -
  have inv1: "independent_vertices E S"
   and inv2: "X ⊆ V"
   and inv3: "S ⊆ X"
   and inv4: "∀v1 v2. v1 ∈ (V - X) ∧ v2 ∈ S ⟶ {v1, v2} ∉ E"
    using inv unfolding inv_iv_def by auto
  have finite_S: "finite S" using inv1 and independent_vertices_finite by auto
  have S1: "∀y ∈ S. {x, y} ∉ E" using inv4 and x_def by blast
  have S2: "∀x ∈ S. ∀y ∈ S. {x, y} ∉ E" using inv1 unfolding independent_vertices_def by metis
  have S3: "v1 ∈ insert x S ⟹ v2 ∈ insert x S ⟹ {v1, v2} ∉ E" for v1 v2
    proof -
      assume "v1 ∈ insert x S" and "v2 ∈ insert x S"
      then consider
          (a) "v1 = x" and "v2 = x"
        | (b) "v1 = x" and "v2 ∈ S"
        | (c) "v1 ∈ S" and "v2 = x"
        | (d) "v1 ∈ S" and "v2 ∈ S"
        by auto
      then show "{v1, v2} ∉ E"
      proof cases
        case a then show ?thesis using edges2 by force
      next
        case b then show ?thesis using S1 by auto
      next
        case c then show ?thesis using S1 by (metis doubleton_eq_iff)
      next
        case d then show ?thesis using S2 by auto
      qed
    qed
  (* invariant conjunct 1 *)
  have "independent_vertices E (insert x S)"
    using S3 and inv1 and x_def unfolding independent_vertices_def by auto
  (* invariant conjunct 2 *)
  moreover have "X ∪ neighbors x ∪ {x} ⊆ V"
  proof
    fix xa
    assume "xa ∈ X ∪ neighbors x ∪ {x}"
    then consider (a) "xa ∈ X" | (b) "xa ∈ neighbors x" | (c) "xa = x" by auto
    then show "xa ∈ V"
    proof cases
      case a
      then show ?thesis using inv2 by blast
    next
      case b
      then show ?thesis by auto
    next
      case c
      then show ?thesis using x_def by blast
    qed
  qed
  (* invariant conjunct 3 *)
  moreover have "insert x S ⊆ X ∪ neighbors x ∪ {x}" using inv3 by auto
  (* invariant conjunct 4 *)
  moreover have "v1 ∈ V - (X ∪ neighbors x ∪ {x}) ⟹ v2 ∈ insert x S ⟹ {v1, v2} ∉ E" for v1 v2
  proof -
    assume H: "v1 ∈ V - (X ∪ neighbors x ∪ {x})" and "v2 ∈ insert x S"
    then consider (a) "v2 = x" | (b) "v2 ∈ S" by auto
    then show "{v1, v2} ∉ E"
    proof cases
      case a
      with H have "v1 ∉ neighbors v2" by blast
      then show ?thesis by auto
    next
      case b
      from H have "v1 ∈ V - X" by blast
      with b and inv4 show ?thesis by blast
    qed
  qed
  (* conclusion *)
  ultimately show "inv_iv (insert x S) (X ∪ neighbors x ∪ {x})" unfolding inv_iv_def by blast
qed

lemma inv_approx_preserv:
  assumes inv: "inv_approx S X (Δ + 1)"
      and x_def: "x ∈ V - X"
    shows "inv_approx (insert x S) (X ∪ neighbors x ∪ {x}) (Δ + 1)"
proof -
  have finite_S: "finite S" using inv and independent_vertices_finite
    unfolding inv_approx_def inv_iv_def by auto
  have Sx: "x ∉ S" using inv and x_def unfolding inv_approx_def inv_iv_def by blast
  (* main invariant is preserved *)
  from inv have "inv_iv S X" unfolding inv_approx_def by auto
  with x_def have "inv_iv (insert x S) (X ∪ neighbors x ∪ {x})"
  proof (intro inv_preserv, auto) qed
  (* the approximation ratio is preserved (at most Δ+1 vertices are removed in any iteration) *)
  moreover have "card (X ∪ neighbors x ∪ {x}) ≤ card (insert x S) * (Δ + 1)"
  proof -
    have "degree_vertex x ≤ Δ" using Δ_max_degree and x_def by auto
    then have "card (neighbors x ∪ {x}) ≤ Δ + 1" using card_Un_le [of "neighbors x" "{x}"] by auto
    then have "card (X ∪ neighbors x ∪ {x}) ≤ card X + Δ + 1" using card_Un_le [of X "neighbors x ∪ {x}"] by auto
    also have "... ≤ card S * (Δ + 1) + Δ + 1" using inv unfolding inv_approx_def by auto
    also have "... = card (insert x S) * (Δ + 1)" using finite_S and Sx by auto
    finally show ?thesis .
  qed
  (* conclusion *)
  ultimately show "inv_approx (insert x S) (X ∪ neighbors x ∪ {x}) (Δ + 1)"
    unfolding inv_approx_def by auto
qed

(* the antecedent combines inv_approx (for an arbitrary ratio r) and the negated post-condition *)
lemma inv_approx: "independent_vertices E S ⟹ card V ≤ card S * r ⟹ approximation_miv r S"
proof -
  assume 1: "independent_vertices E S" and 2: "card V ≤ card S * r"
  have "independent_vertices E S' ⟹ card S' ≤ card S * r" for S'
  proof -
    assume  "independent_vertices E S'"
    then have "S' ⊆ V" unfolding independent_vertices_def by auto
    then have "card S' ≤ card V" using finite_V and card_mono by auto
    also have "... ≤ card S * r" using 2 by auto
    finally show "card S' ≤ card S * r" .
  qed
  with 1 show "approximation_miv r S" unfolding approximation_miv_def by auto
qed

theorem wei_approx_Δ_plus_1:
"VARS (S :: 'a set) (X :: 'a set) (x :: 'a)
  { True }
  S := {};
  X := {};
  WHILE X ≠ V
  INV { inv_approx S X (Δ + 1) }
  DO x := (SOME x. x ∈ V - X);
     S := insert x S;
     X := X ∪ neighbors x ∪ {x}
  OD
  { approximation_miv (Δ + 1) S }"
proof (vcg, goal_cases)
  case (1 S X x) (* invariant initially true *)
  then show ?case unfolding inv_approx_def inv_iv_def independent_vertices_def by auto
next
  case (2 S X x) (* invariant preserved by loop *)
  (* definedness of assignment *)
  let ?x = "(SOME x. x ∈ V - X)"
  have "V - X ≠ {}" using 2 unfolding inv_approx_def inv_iv_def by blast
  then have "?x ∈ V - X" using some_in_eq by metis
  with 2 show ?case using inv_approx_preserv by auto
next
  case (3 S X x) (* invariant implies post-condition *)
  then show ?case using inv_approx unfolding inv_approx_def inv_iv_def by auto
qed


subsection ‹Wei's algorithm: ‹Δ›-approximation›

text ‹The previous approximation uses very little information about the optimal solution (it has at most as many vertices as the set itself). With some extra effort we can improve the ratio to ‹Δ› instead of ‹Δ+1›. In order to do that we must show that among the vertices removed in each iteration, at most ‹Δ› could belong to an optimal solution. This requires carrying around a set ‹P› (via a ghost variable) which records the vertices deleted in each iteration.›

definition inv_partition :: "'a set ⇒ 'a set ⇒ 'a set set ⇒ bool" where
"inv_partition S X P ⟷ inv_iv S X
                     ∧ ⋃P = X
                     ∧ (∀p ∈ P. ∃s ∈ V. p = {s} ∪ neighbors s)
                     ∧ card P = card S
                     ∧ finite P"

lemma inv_partition_preserv:
  assumes inv: "inv_partition S X P"
      and x_def: "x ∈ V - X"
    shows "inv_partition (insert x S) (X ∪ neighbors x ∪ {x}) (insert ({x} ∪ neighbors x) P)"
proof -
  have finite_S: "finite S" using inv and independent_vertices_finite
    unfolding inv_partition_def inv_iv_def by auto
  have Sx: "x ∉ S" using inv and x_def unfolding inv_partition_def inv_iv_def by blast
  (* main invariant is preserved *)
  from inv have "inv_iv S X" unfolding inv_partition_def by auto
  with x_def have "inv_iv (insert x S) (X ∪ neighbors x ∪ {x})"
  proof (intro inv_preserv, auto) qed
  (* conjunct 1 *)
  moreover have "⋃(insert ({x} ∪ neighbors x) P) = X ∪ neighbors x ∪ {x}"
    using inv unfolding inv_partition_def by auto
  (* conjunct 2 *)
  moreover have "(∀p∈insert ({x} ∪ neighbors x) P. ∃s ∈ V. p = {s} ∪ neighbors s)"
    using inv and x_def unfolding inv_partition_def by auto
  (* conjunct 3 *)
  moreover have "card (insert ({x} ∪ neighbors x) P) = card (insert x S)"
  proof -
    from x_def and inv have "x ∉ ⋃P" unfolding inv_partition_def by auto
    then have "{x} ∪ neighbors x ∉ P" by auto
    then have "card (insert ({x} ∪ neighbors x) P) = card P + 1" using inv unfolding inv_partition_def by auto
    moreover have "card (insert x S) = card S + 1" using Sx and finite_S by auto
    ultimately show ?thesis using inv unfolding inv_partition_def by auto
  qed
  (* conjunct 4 *)
  moreover have "finite (insert ({x} ∪ neighbors x) P)"
    using inv unfolding inv_partition_def by auto
  (* conclusion *)
  ultimately show "inv_partition (insert x S) (X ∪ neighbors x ∪ {x}) (insert ({x} ∪ neighbors x) P)"
    unfolding inv_partition_def by auto
qed

lemma card_Union_le_sum_card:
  fixes U :: "'a set set"
  assumes "∀u ∈ U. finite u"
  shows "card (⋃U) ≤ sum card U"
proof (cases "finite U")
  case False
  then show "card (⋃U) ≤ sum card U"
    using card_eq_0_iff finite_UnionD by auto
next
  case True
  then show "card (⋃U) ≤ sum card U"
  proof (induct U rule: finite_induct)
    case empty
    then show ?case by auto
  next
    case (insert x F)
    then have "card(⋃(insert x F)) ≤ card(x) + card (⋃F)" using card_Un_le by auto
    also have "... ≤ card(x) + sum card F" using insert.hyps by auto
    also have "... = sum card (insert x F)" using sum.insert_if and insert.hyps by auto
    finally show ?case .
  qed
qed

(* this lemma could be more generally about U :: "nat set", but this makes its application more difficult later *)
lemma sum_card:
  fixes U :: "'a set set"
    and n :: nat
  assumes "∀S ∈ U. card S ≤ n"
  shows "sum card U ≤ card U * n"
proof cases
  assume "infinite U ∨ U = {}"
  then have "sum card U = 0" using sum.infinite by auto
  then show "sum card U ≤ card U * n" by auto
next
  assume "¬(infinite U ∨ U = {})"
  with assms have "finite U" and "U ≠ {}"and "∀S ∈ U. card S ≤ n" by auto
  then show "sum card U ≤ card U * n"
  proof (induct U rule: finite_ne_induct)
    case (singleton x)
    then show ?case by auto
  next
    case (insert x F)
    assume "∀S∈insert x F. card S ≤ n"
    then have 1:"card x ≤ n" and 2:"sum card F ≤ card F * n" using insert.hyps by auto
    then have "sum card (insert x F) = card x + sum card F" using sum.insert_if and insert.hyps by auto
    also have "... ≤ n + card F * n" using 1 and 2 by auto
    also have "... = card (insert x F) * n" using card_insert_if and insert.hyps by auto
    finally show ?case .
  qed
qed

(* among the vertices deleted in each iteration, at most Δ can belong to an independent set of
   vertices: the chosen vertex or (some of) its neighbors *)
lemma x_or_neighbors:
  fixes P :: "'a set set"
    and S :: "'a set"
  assumes inv: "∀p∈P. ∃s ∈ V. p = {s} ∪ neighbors s"
      and ivS: "independent_vertices E S"
    shows "∀p ∈ P. card (S ∩ p) ≤ Δ"
proof
  fix p
  assume "p ∈ P"
  then obtain s where 1: "s ∈ V ∧ p = {s} ∪ neighbors s" using inv by blast
  then show "card (S ∩ p) ≤ Δ"
  proof cases
    assume "s ∈ S"
    then have "S ∩ neighbors s = {}" using ivS unfolding independent_vertices_def by auto
    then have "S ∩ p ⊆ {s}" using 1 by auto
    then have 2: "card (S ∩ p) ≤ 1" using subset_singletonD by fastforce
    consider (a) "E = {}" | (b) "0 < Δ" using Δ_pos by auto
    then show "card (S ∩ p) ≤ Δ"
    proof cases
      case a
      then have "S = {}" using ivS unfolding independent_vertices_def by auto
      then show ?thesis by auto
    next
      case b
      then show ?thesis using 2 by auto
    qed  
  next
    assume "s ∉ S"
    with 1 have "S ∩ p ⊆ neighbors s" by auto
    then have "card (S ∩ p) ≤ degree_vertex s" using card_mono and finite_neighbors by auto
    then show "card (S ∩ p) ≤ Δ" using 1 and Δ_max_degree [of s] by auto
  qed
qed

(* the premise combines the invariant and the negated post-condition *)
lemma inv_partition_approx: "inv_partition S V P ⟹ approximation_miv Δ S"
proof -
  assume H1: "inv_partition S V P"
  then have "independent_vertices E S" unfolding inv_partition_def inv_iv_def by auto
  moreover have "independent_vertices E S' ⟹ card S' ≤ card S * Δ" for S'
  proof -
    let ?I = "{S' ∩ p | p. p ∈ P}"
    (* split the optimal solution among the sets of P, which cover V so no element is
       lost. We obtain a cover of S' and show the required bound on its cardinality *)
    assume H2: "independent_vertices E S'"
    then have "S' ⊆ V" unfolding independent_vertices_def using vertices.simps by blast
    with H1 have "S' = S' ∩ ⋃P" unfolding inv_partition_def by auto
    then have "S' = (⋃p ∈ P. S' ∩ p)" using Int_Union by auto
    then have "S' = ⋃?I" by blast
    moreover have "finite S'" using H2 and independent_vertices_finite by auto
    then have "p ∈ P ⟹ finite (S' ∩ p)" for p by auto
    ultimately have "card S' ≤ sum card ?I" using card_Union_le_sum_card [of ?I] by auto
    also have "... ≤ card ?I * Δ"
      using x_or_neighbors [of P S']
        and sum_card [of ?I Δ]
        and H1 and H2 unfolding inv_partition_def by auto
    also have "... ≤ card P * Δ"
    proof -
      have "finite P" using H1 unfolding inv_partition_def by auto
      then have "card ?I ≤ card P"
        using Setcompr_eq_image [of "λp. S' ∩ p" P]
          and card_image_le unfolding inv_partition_def by auto
      then show ?thesis by auto
    qed
    also have "... = card S * Δ" using H1 unfolding inv_partition_def by auto
    ultimately show "card S' ≤ card S * Δ" by auto
  qed
  ultimately show "approximation_miv Δ S" unfolding approximation_miv_def by auto
qed

theorem wei_approx_Δ:
"VARS (S :: 'a set) (X :: 'a set) (x :: 'a)
  { True }
  S := {};
  X := {};
  WHILE X ≠ V
  INV { ∃P. inv_partition S X P }
  DO x := (SOME x. x ∈ V - X);
     S := insert x S;
     X := X ∪ neighbors x ∪ {x}
  OD
  { approximation_miv Δ S }"
proof (vcg, goal_cases)
  case (1 S X x) (* invariant initially true *)
  (* the invariant is initially true with the ghost variable P := {} *)
  have "inv_partition {} {} {}" unfolding inv_partition_def inv_iv_def independent_vertices_def by auto
  then show ?case by auto
next
  case (2 S X x) (* invariant preserved by loop *)
  (* definedness of assignment *)
  let ?x = "(SOME x. x ∈ V - X)"
  from 2 obtain P where I: "inv_partition S X P" by auto 
  then have "V - X ≠ {}" using 2 unfolding inv_partition_def by auto
  then have "?x ∈ V - X" using some_in_eq by metis
  (* show that the invariant is true with the ghost variable P := insert ({?x} ∪ neighbors ?x) P *)
  with I have "inv_partition (insert ?x S) (X ∪ neighbors ?x ∪ {?x}) (insert ({?x} ∪ neighbors ?x) P)"
    using inv_partition_preserv by blast
  then show ?case by auto
next
  case (3 S X x) (* invariant implies post-condition *)
  then show ?case using inv_partition_approx unfolding inv_approx_def by auto
qed

subsection "Wei's algorithm with dynamically computed approximation ratio"

text ‹In this subsection, we augment the algorithm with a variable used to compute the effective approximation ratio of the solution. In addition, the vertex of smallest degree is picked. With this heuristic, the algorithm achieves an approximation ratio of ‹(Δ+2)/3›, but this is not proved here.›

definition vertex_heuristic :: "'a set ⇒ 'a ⇒ bool" where
"vertex_heuristic X v = (∀u ∈ V - X. card (neighbors v - X) ≤ card (neighbors u - X))"

(* this lemma is needed to show that there exist a vertex to be picked by the heuristic *)
lemma ex_min_finite_set:
  fixes S :: "'a set"
    and f :: "'a ⇒ nat"
    shows "finite S ⟹ S ≠ {} ⟹ ∃x. x ∈ S ∧ (∀y ∈ S. f x ≤ f y)"
          (is "?P1 ⟹ ?P2 ⟹ ∃x. ?minf S x")
proof (induct S rule: finite_ne_induct)
  case (singleton x)
  have "?minf {x} x" by auto
  then show ?case by auto
next
  case (insert x F)
  from insert(4) obtain y where Py: "?minf F y" by auto
  show "∃z. ?minf (insert x F) z"
  proof cases
    assume "f x < f y"
    then have "?minf (insert x F) x" using Py by auto
    then show ?case by auto
  next
    assume "¬f x < f y"
    then have "?minf (insert x F) y" using Py by auto
    then show ?case by auto
  qed
qed

lemma inv_approx_preserv2:
  fixes S :: "'a set"
    and X :: "'a set"
    and s :: nat
    and x :: "'a"
  assumes inv: "inv_approx S X s"
      and x_def: "x ∈ V - X"
    shows "inv_approx (insert x S) (X ∪ neighbors x ∪ {x}) (max (card (neighbors x ∪ {x} - X)) s)"
proof -
  have finite_S: "finite S" using inv and independent_vertices_finite unfolding inv_approx_def inv_iv_def by auto
  have Sx: "x ∉ S" using inv and x_def unfolding inv_approx_def inv_iv_def by blast
  (* main invariant is preserved *)
  from inv have "inv_iv S X" unfolding inv_approx_def by auto
  with x_def have "inv_iv (insert x S) (X ∪ neighbors x ∪ {x})"
  proof (intro inv_preserv, auto) qed
  (* the approximation ratio is preserved *)
  moreover have "card (X ∪ neighbors x ∪ {x}) ≤ card (insert x S) * max (card (neighbors x ∪ {x} - X)) s"
  proof -
    let ?N = "neighbors x ∪ {x} - X"
    have "card (X ∪ ?N) ≤ card X + card ?N" using card_Un_le [of X ?N] by auto
    also have "... ≤ card S * s + card ?N" using inv unfolding inv_approx_def by auto
    also have "... ≤ card S * max (card ?N) s + card ?N" by auto
    also have "... ≤ card S * max (card ?N) s + max (card ?N) s" by auto
    also have "... = card (insert x S) * max (card ?N) s" using Sx and finite_S by auto
    finally show ?thesis by auto
  qed
  (* conclusion *)
  ultimately show "inv_approx (insert x S) (X ∪ neighbors x ∪ {x}) (max (card (neighbors x ∪ {x} - X)) s)"
    unfolding inv_approx_def by auto
qed

theorem wei_approx_min_degree_heuristic:
"VARS (S :: 'a set) (X :: 'a set) (x :: 'a) (r :: nat)
  { True }
  S := {};
  X := {};
  r := 0;
  WHILE X ≠ V
  INV { inv_approx S X r }
  DO x := (SOME x. x ∈ V - X ∧ vertex_heuristic X x);
     S := insert x S;
     r := max (card (neighbors x ∪ {x} - X)) r;
     X := X ∪ neighbors x ∪ {x}
  OD
  { approximation_miv r S }"
proof (vcg, goal_cases)
  case (1 S X x r) (* invariant initially true *)
  then show ?case unfolding inv_approx_def inv_iv_def independent_vertices_def by auto
next
  case (2 S X x r) (* invariant preserved by loop *)
  (* definedness of assignment *)
  let ?x = "(SOME x. x ∈ V - X ∧ vertex_heuristic X x)"
  have "V - X ≠ {}" using 2 unfolding inv_approx_def inv_iv_def by blast
  moreover have "finite (V - X)" using 2 and finite_V by auto
  ultimately have "∃x. x ∈ V - X ∧ vertex_heuristic X x"
    using ex_min_finite_set [where ?f = "λx. card (neighbors x - X)"]
    unfolding vertex_heuristic_def by auto
  then have x_def: "?x ∈ V - X ∧ vertex_heuristic X ?x"
    using someI_ex [where ?P = "λx. x ∈ V - X ∧ vertex_heuristic X x"] by auto
  with 2 show ?case using inv_approx_preserv2 by auto
next
  case (3 S X x r)
  then show ?case using inv_approx unfolding inv_approx_def inv_iv_def by auto
qed

end
end