CentraleSupélec LMF, UMR CNRS 9021
Département informatique Laboratoire Méthodes Formelles
Bât Breguet, 3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
91190 Gif-sur-Yvette, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
Preuves de certains théorèmes des TDs du cours d'algorithmique en 1re année

Table des matières

Preuves sur les graphes

text ‹
  CentraleSupélec Algorithms course: Proofs of the theorems of the first practical session
  frederic.boulanger@centralesupelec.fr, November 2018
›
(*<*)
theory AlgoST2_TD1
imports Main
begin
(*>*)

section‹Graph type›
text‹
  We define here graphs as a set of vertices and a set of edges, an edge being a pair
  of vertices. We add the constraint that the extremities of the edges must belong to 
  the set of vertices. Vertices are represented with natural integers.

  These types allow the representation of directed or not directed graphs, the
  directedness depends on how we interpret the set of edges. Loops (edges from a vertex 
  to the same vertex) are allowed, as well as infinite graphs. Multigraphs (with more
  than one edge between two given vertices) are not supported.
›
type_synonym vertex = ‹nat›
type_synonym edge = ‹vertex × vertex›
typedef graph = ‹{(V::vertex set, E::edge set). E ⊆ V×V}› by blast

text‹
  The constraint in the type definition makes the graph type distinct from its support.
  We obtain the representation of a graph as a pair (E,V) using \<^term>‹Rep_graph›, and 
  we can obtain a graph from an \<^term>‹(E,V)› pair that satisfies the constraint 
  using \<^term>‹Abs_graph›.
  We define here two abbreviations for accessing the set of vertices and the set of edges 
  of a graph:
›

abbreviation ‹vertices g ≡ (fst (Rep_graph g))›
abbreviation ‹edges g ≡ (snd (Rep_graph g))›

text‹An example of a graph:›
(*
 1 -- 2 -- 3 -- 4
 | \  | \/ |    |
 |  \ | /\ |    |
 5    6 -- 7 -- 8
*)
definition ‹g1::graph ≡ Abs_graph (
                          {1,2,3,4,5,6,7,8},
                          {(1,2),(1,5),(1,6),
                            (2,3),(2,6),(2,7),
                            (3,4),(3,6),(3,8),
                            (4,8),
                            (6,3),
                            (7,2),(7,3),(7,8)
                          })›


text‹
  Neighbours of a node, in a graph as well as in a directed graph:
›
definition neighbours :: ‹graph ⇒ vertex ⇒ vertex set›
where
  ‹neighbours g v ≡ {w ∈ vertices g. ∃ e ∈ edges g. e = (v, w) ∨ e = (w, v)}›

definition directedNeighbours :: ‹graph ⇒ vertex ⇒ vertex set›
where
  ‹directedNeighbours g v ≡ {w ∈ vertices g. ∃ e ∈ edges g. e = (v, w)}›


subsection‹Some basic lemmas about edges and vertices›
text‹
  The set of edges of a graph is included in the cartesian product 
  of the set of its vertices:
›
lemma edges_in_vertprod:‹edges g ⊆ vertices g × vertices g›
proof -
  { fix e assume h:‹e ∈ edges g›
    from Rep_graph have ‹Rep_graph g ∈ {(V, E). E ⊆ V×V}› .
    hence ‹∃V E. Rep_graph g = (V, E) ∧ E ⊆ V×V› by blast
    from this obtain V and E where rep:‹Rep_graph g = (V, E) ∧ E ⊆ V×V› by blast
    with h have ‹e ∈ V×V› by auto
    with rep have ‹e ∈ vertices g × vertices g› by auto
  } thus ?thesis by (simp add: subsetI)
qed

text‹
  The extremities of an edge are vertices:
›
lemma edges_link_vertices:
  assumes ‹e ∈ edges g›
  shows   ‹(fst e) ∈ vertices g›
  and     ‹(snd e) ∈ vertices g›
  using assms edges_in_vertprod by fastforce+

section‹Paths and cycles›
text‹
  A directed path is a list of vertices such that each pair formed of consecutive nodes
  is an edge.
›
definition isDirectedPath
where
  ‹isDirectedPath l g ≡ length l > 1
                      ∧ (∀i. Suc i < length l ⟶ (l!i, l!Suc i) ∈ edges g)›

text‹
  All elements in a directed path are vertices.
›
lemma dpath_in_vertices:
  assumes ‹isDirectedPath l g›
    shows ‹set l ⊆ vertices g›
proof
  fix v assume ‹v ∈ set l›
  hence ‹∃i < length l. l!i = v› by (simp add: in_set_conv_nth)
  from this obtain i where i_def:‹i < length l ∧ l!i = v› by blast
  show ‹v ∈ vertices g›
  proof (cases ‹i = 0›)
    case True
      with assms have ‹Suc i < length l› unfolding isDirectedPath_def by simp
      with assms have ‹(l!i, l!(Suc i)) ∈ edges g› unfolding isDirectedPath_def by simp
      thus ?thesis using edges_link_vertices i_def by fastforce
  next
    case False
      from this obtain k where ‹i = Suc k› using gr0_implies_Suc by blast
      with i_def assms have ‹(l!k, l!i) ∈ edges g› unfolding isDirectedPath_def by blast
      thus ?thesis using edges_link_vertices i_def by fastforce
  qed
qed

text‹
  A directed path in a subgraph is a directed path of the graph.
›
lemma dpath_subgraph:
  assumes ‹edges sg ⊆ edges g›
      and ‹isDirectedPath l sg›
    shows ‹isDirectedPath l g›
proof -
  from assms(2) have 
    len:‹length l > 1› and
    edge:‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges sg›
    unfolding isDirectedPath_def by simp+
  from edge and assms(1) have ‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges g› by blast
  with len show ?thesis unfolding isDirectedPath_def by simp
qed

text‹
  A path is similar but does not take the orientation of the edges into account.
›
definition isPath
where
  ‹isPath l g ≡ length l > 1
              ∧ (∀i. Suc i < length l ⟶ (l!i, l!Suc i) ∈ edges g
                                        ∨ (l!Suc i, l!i) ∈ edges g)›

text‹
  All elements in a path are vertices.
›
lemma path_in_vertices:
  assumes ‹isPath l g›
    shows ‹set l ⊆ vertices g›
proof
  fix v assume ‹v ∈ set l›
  hence ‹∃i < length l. l!i = v› by (simp add: in_set_conv_nth)
  from this obtain i where i_def:‹i < length l ∧ l!i = v› by blast
  show ‹v ∈ vertices g›
  proof (cases ‹i = 0›)
    case True
      with assms have ‹Suc i < length l› unfolding isPath_def by simp
      with assms have ‹(l!i, l!(Suc i)) ∈ edges g ∨ (l!(Suc i), l!i) ∈ edges g›
        unfolding isPath_def by simp
      thus ?thesis using edges_link_vertices i_def by fastforce
  next
    case False
      from this obtain k where ‹i = Suc k› using gr0_implies_Suc by blast
      with i_def assms have ‹(l!k, l!i) ∈ edges g ∨ (l!i, l!k) ∈ edges g›
        unfolding isPath_def by blast
      thus ?thesis using edges_link_vertices i_def by fastforce
  qed
qed

text‹
  A path in a subgraph is a path of the graph.
›
lemma path_subgraph:
  assumes ‹edges sg ⊆ edges g›
      and ‹isPath l sg›
    shows ‹isPath l g›
proof -
  from assms(2) have 
    len:‹length l > 1› and
    edge:‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges sg ∨ (l!(Suc i), l!i) ∈ edges sg›
    unfolding isPath_def by simp+
  from edge and assms(1) have
    ‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges g ∨ (l!(Suc i), l!i) ∈ edges g› by blast
  with len show ?thesis unfolding isPath_def by simp
qed

text‹
  A directed cycle is a directed path which ends where it starts and contains at 
  least two nodes.
›
definition isDirectedCycle
  where ‹isDirectedCycle l g ≡ l!0 = l!(length l - 1)
                             ∧ isDirectedPath l g
  ›

text‹
  A cycle is a path which ends where it starts and contains at least two nodes.
›
definition isCycle
  where ‹isCycle l g ≡ length l > 1
                   ∧ l!0 = l!(length l - 1)
                   ∧ isPath l g
  ›

section‹Properties of graphs›
text‹
  A bipartite graph has a partition of its vertices into two sets, such that all
  edges have an extremity in one set of the partition and the other extremity 
  in the other set.
›
abbreviation ‹twoParts g V1 V2 ≡
    V1 ∪ V2 = vertices g
  ∧ V1 ∩ V2 = {}
  ∧ (∀ e ∈ edges g. ((fst e) ∈ V1 ∧ (snd e) ∈ V2)
                  ∨ ((fst e) ∈ V2 ∧ (snd e) ∈ V1))›

definition isBipartite
  where ‹isBipartite g ≡ (∃V1 V2. twoParts g V1 V2)›

text‹
  A 2-colorable graph is a graph in which it is possible, using only two colors,
  to assign a color to each node without having two adjacent nodes with the same color.
  Here, we choose \<^term>‹True› and \<^term>‹False› as colors :
›
definition isTwoColorable
where
  ‹isTwoColorable g ≡ ∃f::nat ⇒ bool. ∀ e ∈ edges g. f (fst e) ≠ f (snd e)›

text‹
  A directed acyclic graph is a directed graph with no cycle.
›
definition isDAG
where
  ‹isDAG g ≡ (∀l::vertex list. ¬isDirectedCycle l g)›

text‹
  Subgraphs of a DAG are DAGs.
›
lemma dag_subgraph:
  assumes ‹isDAG g›
      and ‹edges sg ⊆ edges g›
    shows ‹isDAG sg›
  unfolding isDAG_def isDirectedCycle_def
  using assms(1) dpath_subgraph[OF assms(2)] isDAG_def isDirectedCycle_def by blast 


section‹First theorem about bipartite graphs›
text‹
  All cycles in a bipartite graph have an even length (number of edges).

  We first show that for a list \<^term>‹l› of vertices and a partition
  \<^term>‹(V, V')› of graph, if the first node of the list is in \<^term>‹V›, then:
  ▪ after following an even number of edges, we have a node in \<^term>‹V›
  ▪ after following an odd number of edges, we have a node in \<^term>‹V'›
›
lemma step2V:
  assumes ‹∀i. Suc (Suc i) < length l ∧ l!i ∈ V ⟶ l!(Suc(Suc i)) ∈ V›
      and ‹∀i. Suc i < length l ∧ l!i ∈ V ⟶ l!(Suc i) ∈ V'›
      and ‹l!0 ∈ V›
    shows ‹((Suc^^(2*k)) 0 < length l ⟶ l!((Suc^^(2*k)) 0) ∈ V)
         ∧ ((Suc^^(2*k+1)) 0 < length l ⟶ l!((Suc^^(2*k+1)) 0) ∈ V')›
proof (induction k)
  case 0
    text‹
      The case \<^term>‹k=0› is easy because \<^term>‹Suc^^0 = id› and \<^term>‹Suc^^1 = Suc›.
    ›
    thus ?case using assms(2,3) by simp
next
  case (Suc k')
    text‹First, if \<^term>‹2+2*k' < length l› then \<^term>‹2*k' < length l››
    have ‹Suc (Suc ((Suc^^(2 * k')) 0)) < length l ⟶ (Suc^^(2 * k')) 0 < length l› by auto
    text‹With the induction hypothesis, we know that after \<^term>‹2*k'› edges, we have a node in V.›
    with Suc.IH have ‹Suc (Suc ((Suc^^(2 * k')) 0)) < length l ⟶ l!(Suc^^(2 * k')) 0 ∈ V›
      by blast
    text‹With the first assumption, we know that after \<^term>‹2+2*k'› edges, we have a node in V.›
    with assms(1)
      have ‹Suc (Suc ((Suc^^(2 * k')) 0)) < length l ⟶ l!(Suc (Suc ((Suc^^(2 * k')) 0))) ∈ V›
      by blast
    text‹With some massaging of the powers of Suc, we get the first part of our theorem.›
    moreover have ‹Suc^^(2*(Suc k')) = Suc^^(2*k') ∘ Suc ∘ Suc› by auto
    ultimately have 1:‹(Suc^^(2*(Suc k'))) 0 < length l ⟶ l!(Suc^^(2 * (Suc k'))) 0 ∈ V› by auto

    text‹With the second assumption, we get the second part of our theorem.›
    with assms(2) have
      ‹Suc ((Suc^^(2*(Suc k'))) 0) < length l ⟶ l!(Suc ((Suc^^(2 * (Suc k'))) 0)) ∈ V'›
      using Suc_lessD by blast
    hence 2:‹(Suc^^(2*(Suc k')+1)) 0 < length l ⟶ l!((Suc^^(2 * (Suc k') + 1)) 0) ∈ V'› by simp

    from 1 2 show ?case ..
qed

text‹Some lemmas about even and odd numbers.›
lemma even_sucpow_even:‹even n = (∃k. n = (Suc^^(2*k)) 0)› by (simp add: dvd_def)
lemma odd_sucpow_odd:‹odd n = (∃k. n = Suc ((Suc^^(2*k)) 0))› using oddE by fastforce

text‹
  The main part of our proof: if V and V' are a bipartition of g, and if l is a cycle 
  in g which starts in V, then the length of the cycle is even. The length of the cycle
  is the number of edges, but the cycle is a list of edges, so we have to subtract 1
  to obtain it.
›
lemma twoParts_all_cycles_even:
  assumes ‹twoParts g V V'›
      and ‹isCycle l g›
      and ‹l!0 ∈ V›
    shows ‹even (length l - 1)›
proof -
  text‹Edges connect nodes from distinct subsets of the partition›
  have alt:‹∀ e ∈ edges g. ((fst e) ∈ V ⟶ (snd e) ∈ V') ∧ ((fst e) ∈ V' ⟶ (snd e) ∈ V)›
    using assms(1) by blast
  text‹The vertices of the cycle alternate between the two subsets of the partition›
  have alt1:‹∀ i. Suc i < length l ∧ l!i ∈ V ⟶ l!(Suc i) ∈ V'›
    using assms(1,2) unfolding isCycle_def isPath_def by fastforce
  have alt1':‹∀ i. Suc i < length l ∧ l!i ∈ V' ⟶ l!(Suc i) ∈ V›
    using assms(1,2) unfolding isCycle_def isPath_def by fastforce
  text‹So we stay in the same subset when skipping a node.›
  have alt2:‹∀ i. Suc (Suc i) < length l ∧ l!i ∈ V ⟶ l!(Suc (Suc i)) ∈ V›
    using alt1 alt1' by auto
  text‹After an even number of steps in the cycle, we get into the starting subset›
  have evenV:‹∀k::nat. (Suc^^(2*k)) 0 < length l ⟶ l!((Suc^^(2*k)) 0) ∈ V›
        using assms(3) step2V alt2 by blast
  text‹And after an odd number of steps in the cycle, we get into the other subset›
  hence oddV':‹∀k::nat. Suc ((Suc^^(2*k)) 0) < length l ⟶ l!(Suc ((Suc^^(2*k)) 0)) ∈ V'›
        using assms(3) step2V alt1 by auto
  text‹A cycle starts and ends at the same vertex›
  from assms(2) have c:‹l!0 = l!(length l - 1)› unfolding isCycle_def by simp
  text‹So the lastnode of the cycle is in V›
  with assms(3) have lastInV:‹l!(length l - 1) ∈ V› by simp
  text‹We can now prove our theorem:›
  show ?thesis
  proof -
    text‹The proof is by contradiction: assume the length of the cycle is not even›
    { assume ‹¬even (length l - 1)›
      text‹So the length is odd and we get \<^term>‹k› such that the length is \<^term>‹2*k+1››
      with odd_sucpow_odd obtain k where ‹(length l - 1) = Suc ((Suc^^(2*k)) 0)› by blast
      text‹But we know that following an odd number of edges leads to a  node in V'... ›
      with oddV' have ‹l!(length l - 1) ∈ V'› by simp
      text‹Which is therefore not in V ›
      with assms(1) have ‹l!(length l - 1) ∉ V› by blast
      text‹Which contradicts the fact that the last node is in V›
      with lastInV have False by simp
    }
    text‹So, the assumption is false, and the theorem is proved.›
    thus ?thesis by blast
  qed
qed

text‹Now, the real theorem: All cycles in a bipartite graph have an even length (number of edges).›
lemma bipartite_all_cycles_even:
  assumes ‹isBipartite g›
      and ‹isCycle l g›
    shows ‹even ((length l) - 1)› (* the number of edges is the number of vertices minus 1 *)
proof -
  text‹From the first assumption, get a bipartition of g›
  from assms(1) obtain V1 and V2 where bip:‹twoParts g V1 V2› unfolding isBipartite_def by blast
  hence bip':‹twoParts g V2 V1› by blast
  show ?thesis
    text‹We have two cases: the first node of the cycle may be in V1 or in V2.›
  proof (cases ‹l!0 ∈ V1›)
    case True
    text‹This case reduces to our previous lemma›
      from twoParts_all_cycles_even[OF bip assms(2) this] show ?thesis .
  next
    case False
      text‹\<^term>‹l!0› is not in V1, but we have to prove that it is in V2!›
      from assms(2) have ‹l!0 ∈ vertices g› unfolding isCycle_def 
        using path_in_vertices by fastforce
      with `l ! 0 ∉ V1` bip have ‹l!0 ∈ V2› by blast
      text‹And we can now reuse the previous lemma›
      from twoParts_all_cycles_even[OF bip' assms(2) this]  show ?thesis .
  qed
qed

section‹Second theorem about bipartite graph›
text‹
  Bipartite graphs are exactly 2-colorable graphs.
›
lemma ‹isTwoColorable g = isBipartite g›
proof
  text‹First, we show \<^term>‹isTwoColorable g ⟹ isBipartite g››
  { assume ‹isTwoColorable g›
    text‹Get the coloring function \<^term>‹f››
    from isTwoColorable_def this obtain f::‹nat ⇒ bool›
      where h:‹∀ e ∈ edges g. f (fst e) ≠ f (snd e)› by blast
    text‹Define the subsets V1 and V2 of same color nodes.›
    define V1 V2 where ‹V1 = {v. f v} ∩ vertices g› and  ‹V2 = {v. ¬f v} ∩ vertices g›
    text‹And show that they form a bipartition of g.›
    have ‹twoParts g V1 V2›
      using edges_link_vertices h V1_def V2_def by auto
    hence ‹isBipartite g› using isBipartite_def by blast
  } thus ‹isTwoColorable g ⟹ isBipartite g› using isBipartite_def by simp

  text‹First, we show \<^term>‹isBipartite g ⟹ isTwoColorable g››
  { assume ‹isBipartite g›
    text‹Get the bipartition of g›
    from isBipartite_def this obtain V1 and V2 where h:‹twoParts g V1 V2› by auto
    text‹Then define a bicoloring function based on V1 and V2.›
    define f where ‹f = (λn. n ∈ V1)›
    text‹and show that the graph is 2-colorable.›
    from h have ‹∀e ∈ edges g. f (fst e) ≠ f (snd e)› using f_def by blast
    hence ‹∃f::nat ⇒ bool. ∀e ∈ edges g. f (fst e) ≠ f (snd e)› by blast
  } thus ‹isBipartite g ⟹ isTwoColorable g› using isTwoColorable_def by simp
qed

section‹A property of DAGs›
text‹
  We want to show that in any directed acyclic graph, there is at least one vertex 
  that has no incoming edge.

  First, we prove by induction that in a non-empty graph where all vertices have at least
  an incoming edge, there are directed paths of arbitrary length.
›
lemma arbitrary_length_chain_suc:
  assumes ‹∀v ∈ vertices g. ∃e ∈ edges g. v = snd e›
      and ‹vertices g ≠ {}›
    shows ‹∃l. length l = Suc (Suc n) ∧ isDirectedPath l g›
proof (induction n)
  case 0
    text‹Build a path of length one (two vertyices).›
    from assms(2) obtain node where node_def:‹node ∈ vertices g› by blast
    with assms(1) obtain edge where edge_def:‹edge ∈ edges g ∧ node = snd edge› by blast
    define prev where ‹prev = fst edge›
    have ‹prev ∈ vertices g› using prev_def edge_def by (simp add: edges_link_vertices)
    hence ‹isDirectedPath [prev, node] g› unfolding isDirectedPath_def
      using node_def edge_def prev_def by auto
    thus ?case by force 
next
  case (Suc k)
    text‹Here, we have to extend a directed path using the first assumption›
    from Suc.IH obtain ll
      where llprop:‹length ll = Suc (Suc k) ∧ isDirectedPath ll g› by blast
    text‹
      For this, we consider the first vertex of the path, get an incoming edge to this
      vertex, and extend the path with the first extremity of this edge.
    ›
    hence ‹ll!0 ∈ vertices g› using dpath_in_vertices by fastforce
    with assms(1) obtain e where exarc:‹e ∈ edges g ∧ ll!0 = snd e› by blast
    define lll where ‹lll = (fst e)#ll›
    with llprop have ‹length lll = Suc (Suc (Suc k)) ∧ isDirectedPath lll g›
      using Suc isDirectedPath_def edges_link_vertices exarc less_Suc_eq_0_disj by auto
    thus ?case by blast
qed

corollary arbitrary_length_chain:
  assumes ‹∀v ∈ vertices g. ∃e ∈ edges g. v = snd e›
      and ‹vertices g ≠ {}›
      and ‹n > 1›
    shows ‹∃l. length l = n ∧ isDirectedPath l g›
proof -
  from assms(3) have ‹∃k. n = Suc (Suc k)› using less_imp_Suc_add by fastforce
  thus ?thesis using arbitrary_length_chain_suc using assms(1,2) by blast
qed

subsection‹Some theorems about lists and finite sets›
text‹
  A list of items from a finite set which is longer that the cardinal
  of the set has repeated elements.
›
lemma biglist_from_set_repeat:
  assumes ‹finite s›
      and ‹set l ⊆ s›
      and ‹length l > card s›
    shows ‹∃i j. i < length l ∧ j < length l ∧ i ≠ j ∧ l!i = l!j›
  by (metis assms antisym_conv2 card_length card_mono distinct_card distinct_conv_nth le_less_trans)

text‹
  A list of items from a finite set which is longer that the cardinal 
  of the set has an element that appears again later in the list.
›
corollary biglist_from_set_repeat_later:
  assumes ‹finite s›
      and ‹set l ⊆ s›
      and ‹length l > card s›
    shows ‹∃i j. i < length l ∧ j < length l ∧ i < j ∧ l!i = l!j›
  by (metis assms biglist_from_set_repeat not_less_iff_gr_or_eq)

subsection‹Sublists and their properties›
text‹
  The sublist of l composed of item i through j included.
›
definition ‹sublist l i j ≡ drop i (take (Suc j) l)›

text‹Examples›

value ‹sublist [0::nat,1,2,3,4,5] 0 2›
value ‹sublist [0::nat,1,2,3,4,5] 3 5›

text‹The length of a sublist:›
lemma sublist_length:
  assumes ‹i < j›
      and ‹j < length l›
    shows ‹length (sublist l i j) = (Suc j) - i›
  unfolding sublist_def by (simp add: Suc_leI assms(2) min.absorb2)

text‹Position of the items of a sublist in the original list:›
lemma sublist_idx:
  assumes ‹i < j›
      and ‹j < length l›
    shows ‹k < (Suc j) - i ⟹ (sublist l i j)!k = l!(k+i)›
  unfolding sublist_def
  by (metis (no_types, hide_lams) add.commute assms length_take lessI less_diff_conv
            less_le min.absorb2 min_less_iff_conj nth_drop nth_take)

text‹A sublist does not contain items that are not in the original list:›
lemma sublist_subset:
  ‹set (sublist l i j) ⊆ set l›
  unfolding sublist_def by (metis dual_order.trans set_drop_subset set_take_subset)

subsection‹The theorem›
text‹
  In a non-empty directed acyclic graph, there is at least one vertex without incoming edge.
›
lemma dag_root_vertex:
  assumes ‹isDAG g›
      and ‹vertices g ≠ {}›
      and ‹finite (vertices g)›
    shows ‹∃v ∈ vertices g. ∀e ∈ edges g. v ≠ (snd e)›
proof -
  text‹Assume all vertices have at least an incoming edge.›
  { assume contr:‹∀v ∈ vertices g. ∃e ∈ edges g. v = snd e›
    text‹Then, build a list of vertices longer that the number of vertices in the graph.›
    define n where ‹n = Suc (card (vertices g))›
    hence ‹n > 1› by (simp add: assms(2,3) card_gt_0_iff)
    from arbitrary_length_chain[OF contr assms(2) this] obtain l where
      lp:‹length l = n ∧ isDirectedPath l g› by blast
    text‹This list necessarily contains the same vertex twice.›
    hence ‹∃i j. i < length l ∧ j < length l ∧ i < j ∧ l!i = l!j›
      using biglist_from_set_repeat_later[OF assms(3)] n_def by (metis dpath_in_vertices lessI lp)
    from this obtain i and j where ij:‹i < length l ∧ j < length l ∧ i < j ∧ l!i = l!j› by blast
    hence iltj:‹i < j› and jltlen:‹j < length l› and ijsame:‹l!i = l!j› by simp+
    text‹The sublist starting and ending at this repeated vertex is a cycle.›
    define cy where cyp:‹cy = sublist l i j›
    from cyp iltj have lcy:‹length cy - 1 + i = j› using sublist_length[OF iltj jltlen] by auto
    from cyp sublist_idx[OF iltj jltlen] have cy_offet:‹∀k < (Suc j) - i. cy!k = l!(k+i)› by blast
    from sublist_length[OF iltj jltlen] iltj cyp have ‹length cy > 1› by simp
    moreover from cyp ijsame sublist_idx[OF iltj jltlen] sublist_length[OF iltj jltlen] iltj
      have ‹cy!0 = cy!(length cy -1)› by auto
    moreover from lp cyp have ‹set cy ⊆ vertices g›
      using sublist_subset dpath_in_vertices by fastforce
    moreover from lp have ‹∀i. Suc i < length l ⟶ (l ! i, l ! Suc i) ∈ edges g›
      unfolding isDirectedPath_def by blast
    with cyp sublist_idx[OF iltj jltlen]
      have ‹∀k. Suc k < length cy ⟶ (cy ! k, cy ! Suc k) ∈ edges g›
      by (simp add: add.commute sublist_def)
    ultimately have ‹isDirectedCycle cy g›
      using ij lp unfolding isDirectedCycle_def isDirectedPath_def by simp
    text‹But DAGs have by definition no cycle.›
    with assms(1) have False unfolding isDAG_def by simp
    text‹So the initial assumption is false, and the theorem is proved.›
  } thus ?thesis by blast
qed

section‹Topoligical orders and DAGs›
text‹DAGs are exactly graphs that have a topological order›

subsection‹Some lemmas about minimal elements›

text‹A non empty set of natural numbers has a minimal element.›
lemma not_empty_set_min:
  assumes ‹(S::(nat set)) ≠ {}›
    shows ‹∃m::nat ∈ S. ∀x ∈ S. m ≤ x›
by (metis (full_types) Collect_empty_eq Collect_mem_eq assms exists_least_iff le_less_linear)

text‹A non empty list of natural numbers has a minimal element.›
lemma not_empty_list_min:
  assumes ‹l ≠ []›
    shows ‹∃i < length (l::'a list). ∀j < length l. (f::('a⇒nat)) (l!i) ≤ f (l!j)›
proof -
  have ‹∃x ∈ f ` (set l). ∀y ∈ f ` (set l). x ≤ y› 
    by (metis assms not_empty_set_min empty_is_image set_empty)
  thus ?thesis
    by (metis (full_types) image_iff in_set_conv_nth)
qed

subsection‹Topological orders›
text‹
  A topological order is compatible with the directed edges of a graph.
›
definition isTopologicalOrder :: ‹(vertex ⇒ nat) ⇒ graph ⇒ bool›
where
  ‹isTopologicalOrder f g ≡ inj f
                      ∧ (∀e ∈ edges g. f (fst e) < f (snd e))›

definition hasTopoOrder
where
  ‹hasTopoOrder g ≡ (∃f. isTopologicalOrder f g)›


subsection‹A DAG has a topological order›

text‹
  The proof is by induction on the number of vertices in the graph. Since the cardinal of
  an infinite set in Isabelle/HOL is 0, we have to add the assumption that our graphs 
  have a finite number of vertices in order to handle the base case.
›
lemma DAG_n_thus_topoOrder:
  ‹⟦finite (vertices g); isDAG g; card (vertices g) = n⟧ ⟹ hasTopoOrder g›
proof (induction n arbitrary: g)
  case 0
  text‹An empty graph has no vertex, so any injective function is a topological order.›
  thus ?case unfolding hasTopoOrder_def isTopologicalOrder_def
    by (metis card_0_eq edges_link_vertices(1) ex_in_conv inj_of_nat)
next
  case (Suc n) thus ?case
    proof (cases ‹n = 0›)
      case True
        text‹Induction step for a graph with one vertex.›
        with Suc have card_1:‹card (vertices g) = 1› by linarith
        text‹The only possible edge is a loop on the unique vertex.›
        hence edge_loop:‹∀ e ∈ edges g. fst e = snd e›  by (metis card_1_singletonE edges_link_vertices singletonD)
        text‹Which is not possible in a DAG.›
        have ‹edges g = {}›
        proof -
          { assume ‹∃e. e ∈ edges g›
            from this obtain e where e_edge:‹e ∈ edges g› by blast
            with edge_loop have loop_e:‹fst e = snd e› by simp
            define ll where ‹ll = [fst e, snd e]›
            hence ‹length ll > 1› by simp
            moreover from ll_def have ‹ll!0 = ll!(length ll - 1)› using loop_e by simp
            moreover have ‹set ll ⊆ vertices g› using ll_def e_edge edges_link_vertices by simp
            moreover have ‹(∀i. Suc i < length ll ⟶ (ll ! i, ll ! Suc i) ∈ edges g)›
              by (simp add: e_edge ll_def)
            ultimately have ‹∃l. isDirectedCycle l g›
              unfolding isDirectedCycle_def isDirectedPath_def by blast
            hence False using Suc.prems(2) unfolding isDAG_def by simp
          }
          thus ?thesis by blast
        qed
        thus ?thesis unfolding hasTopoOrder_def isTopologicalOrder_def using inj_of_nat by blast
    next
      case False
        text‹Induction step for a graph with more than one vertex.›
        text‹Assume we have a DAG with \<^term>‹Suc n› vertices.›
      { fix gg assume gg_dag:‹isDAG gg› and gg_card:‹card (vertices gg) = Suc n›
        from gg_card ‹n ≠ 0› have gg_not_empty:‹vertices gg ≠ {}› by auto
        from gg_card have gg_finite:‹finite (vertices gg)› using ‹n ≠ 0› card_infinite by force
        text‹From a previous theorem, we have a vertex without incoming edge.›
        from dag_root_vertex[OF gg_dag gg_not_empty gg_finite]
          obtain root where root_def:‹root ∈ vertices gg ∧ (∀e ∈ edges gg. root ≠ snd e)› by blast
        text‹We now define a subgraph by removing this root vertex›
        define sv::‹vertex set› where ‹sv = vertices gg - {root}›
        define se::‹edge set› where ‹se = {e. e ∈ edges gg ∧ (fst e) ≠ root}›
        hence subgraph:‹se ⊆ edges gg› by blast
        have ‹se ⊆ sv × sv› using root_def sv_def se_def
          using edges_link_vertices by fastforce
        hence sg_rep:‹(sv, se) ∈ {(V, E). E ⊆ V × V}› by simp
        define sg::‹graph› where ‹sg = Abs_graph (sv, se)›
        have sg_vert:‹vertices sg = sv› using sg_def Abs_graph_inverse[OF sg_rep] by simp
        have sg_edge:‹edges sg = se› using sg_def Abs_graph_inverse[OF sg_rep] by simp
        text‹This subgraph is also a DAG.›
        have sg_dag:‹isDAG sg› using dag_subgraph[OF gg_dag] subgraph sg_edge by simp
        have sg_card:‹card (vertices sg) = n› using gg_card sg_vert sv_def root_def
          by (simp add: gg_finite)
        with ‹n ≠ 0› have ‹finite (vertices sg)› using card_infinite by fastforce
        text‹With the induction hypothesis, we have a topological order on this subgraph.›
        from Suc.IH[OF this sg_dag sg_card] obtain f where f_def:‹isTopologicalOrder f sg›
          unfolding hasTopoOrder_def by blast
        text‹
          We use this order to build an order on the original graph by shifting the rank
          of all vertices of the subgraph by one, and by setting the root as the minimal element.
        ›
        define f' where ‹f' = (Suc ∘ f)(root:=0)›
        have ‹inj f› using f_def isTopologicalOrder_def by simp
        hence ‹inj f'› using f'_def
          by (metis (no_types, lifting) comp_apply fun_upd_apply injD injI inj_Suc nat.distinct(1))
        moreover have ‹(∀e ∈ edges gg. f' (fst e) < f' (snd e))›
          using isTopologicalOrder_def f'_def f_def root_def se_def sg_edge by auto
        ultimately have ‹isTopologicalOrder f' gg› unfolding isTopologicalOrder_def by simp
        hence ‹hasTopoOrder gg› using hasTopoOrder_def by blast
      } thus ?thesis using Suc.prems(2,3) by blast
    qed
qed

text‹
  This corollary removes the assumption on the size of the graph,
  which was used only for the induction.
›
corollary DAG_thus_topoOrder:
  ‹⟦finite (vertices g); isDAG g⟧ ⟹ hasTopoOrder g›
  using DAG_n_thus_topoOrder by blast

text‹
  We can now show that (finite) graphs with a topological order are exactly (finite) DAGs.
›
lemma topo_order_dag:
  assumes ‹finite (vertices g)›
    shows ‹hasTopoOrder g = isDAG g›
proof
  text‹First, show that if a graph admits a topological order, it is a DAG.›
  { assume ‹hasTopoOrder g›
    from this obtain f::‹vertex⇒nat› where topo:‹isTopologicalOrder f g›
      unfolding hasTopoOrder_def by blast
    have ‹isDAG g›
    proof -
      text‹The proof is by contradiction: we assume it is not a DAG and derive False.›
      { assume contr:‹¬isDAG g›
        text‹If the graph is not a DAG, it has a directed cycle.›
        hence ‹∃l. isDirectedCycle l g› unfolding isDAG_def by simp
        from this obtain l where cycle:‹isDirectedCycle l g› by blast
        text‹This cycle has a minimal element according to the topological order›
        with not_empty_list_min have ‹∃i < length l. ∀j < length l. f (l!i) ≤ f (l!j)›
          by (metis cycle isDirectedCycle_def isDirectedPath_def less_numeral_extra(2) list.size(3))
        from this obtain i where i_def:‹i < length l ∧ (∀j < length l. f (l!i) ≤ f (l!j))› by blast
        have False
        proof (cases ‹i = 0›)
          case True
            text‹If the minimal element is the first one in the cycle, it is also the last one›
            define i' where ‹i' = (length l -1)›
            with cycle have cycle_loop:‹l!i' = l!i› unfolding isDirectedCycle_def by (simp add:‹i= 0›)
            from i'_def cycle have ‹i' > 0› unfolding isDirectedCycle_def isDirectedPath_def by simp
            text‹So the two last vertices in the cycle form an edge›
            from this obtain k where k_def:‹i' = Suc k› using old.nat.exhaust by auto
            with cycle have ‹(l!k, l!i') ∈ edges g› 
              unfolding isDirectedCycle_def isDirectedPath_def by (simp add: i'_def)
            text‹According to the topological order, the last element is larger that the previous one›
            hence fk_less:‹f (l!k) < f (l!i')› using topo unfolding isTopologicalOrder_def by auto
            text‹Which contradicts the fact that it is the minimal element in the cycle.›
            moreover from cycle_loop i_def have ‹∀j < length l. f (l!i') ≤ f (l!j)› by simp
            moreover have ‹k < length l› using i'_def k_def by linarith
            ultimately have False using leD by blast
            thus ?thesis .
        next
          case False
            text‹If the minimal element is not the first one in the cycle, we consider the previous one›
            from this obtain k where k_def:‹i = Suc k› using old.nat.exhaust by auto
            with cycle have ‹(l!k, l!i) ∈ edges g› 
              using i_def unfolding isDirectedCycle_def isDirectedPath_def by blast
            text‹Which is therefore smaller than the minimal element, hence the contradiction.›
            hence ‹f (l!k) < f (l!i)› using topo unfolding isTopologicalOrder_def by auto
            with i_def k_def have False using Suc_lessD leD by blast
            thus ?thesis .
        qed
      } thus ?thesis by blast
    qed
  } thus ‹hasTopoOrder g ⟹ isDAG g› .
  text‹For the other implication, we use the lemma proved by induction.›
  { assume ‹isDAG g›
    from DAG_thus_topoOrder[OF assms(1) this] have ‹hasTopoOrder g› .
  } thus ‹isDAG g ⟹ hasTopoOrder g› .
qed

section ‹k-stable and k-vertex cover›

definition is_k_stable
  where  ‹is_k_stable g s k ≡
    card s ≥ k
  ∧ s ⊆ vertices g 
  ∧ (∀ e ∈ edges g. ¬((fst e) ∈ s ∧ (snd e) ∈ s))›

definition is_k_vertexcover
where ‹is_k_vertexcover g c k ≡
    card c ≤ k
  ∧ c ⊆ vertices g 
  ∧ (∀ e ∈ edges g. ((fst e) ∈ c ∨ (snd e) ∈ c))›

lemma stable_vcover_duality:
  assumes ‹finite (vertices g)›
      and ‹s ⊆ vertices g›
      and ‹k ≤ card (vertices g)›
  shows   ‹is_k_stable g s k = is_k_vertexcover g (vertices g - s) (card (vertices g) - k)›
proof
  { assume h:‹is_k_stable g s k›
    let ?c = ‹(vertices g) - s›
    from h have ‹card s ≥ k› using is_k_stable_def by simp
    hence ‹card ?c ≤ card (vertices g) - k› using assms h is_k_stable_def
      by (metis card_Diff_subset diff_le_mono2 rev_finite_subset)
    moreover from h have ‹s ⊆ vertices g› using is_k_stable_def by simp
    hence ‹?c ⊆ vertices g› by simp
    moreover from h have ‹∀ e ∈ edges g. ¬((fst e) ∈ s ∧ (snd e) ∈ s)› using is_k_stable_def by simp
    hence ‹∀ e ∈ edges g. ((fst e) ∈ ?c ∨ (snd e) ∈ ?c)› using edges_link_vertices by auto
    ultimately have ‹is_k_vertexcover g ?c (card (vertices g) - k)› using is_k_vertexcover_def by simp
  } thus ‹is_k_stable g s k ⟹ is_k_vertexcover g (vertices g - s) (card (vertices g) - k)› .

  { assume h:‹is_k_vertexcover g (vertices g - s) (card (vertices g) - k)›
    from h have ‹card (vertices g - s) ≤ card (vertices g) - k› using is_k_vertexcover_def by simp
    hence ‹card (vertices g) - card s ≤ card (vertices g) - k› using assms
      by (simp add: card_Diff_subset finite_subset)
    hence ‹card s ≥ k› using assms by simp
    moreover from h have ‹s ⊆ vertices g› using is_k_vertexcover_def  using assms(2) by blast
    moreover from h have ‹∀ e ∈ edges g. (fst e) ∈ ((vertices g) - s) ∨ (snd e) ∈ ((vertices g) - s)›
      using is_k_vertexcover_def by simp
    hence ‹∀ e ∈ edges g. ((fst e) ∉ s ∨ (snd e) ∉ s)› by blast
    ultimately have ‹is_k_stable g s k› using is_k_stable_def by simp
  } thus ‹is_k_vertexcover g (vertices g - s) (card (vertices g) - k) ⟹ is_k_stable g s k› .
qed

(*<*)
end
(*>*)

Réduction du problème SubsetSum au Knapsack Réduction SubsetSum

theory knapsack
imports Main

begin
text ‹
  Reducing the subset sum problem to the knapsack problem.
›

text ‹
  The subset sum problem: find a subset of [1..n] of sum t
›
definition isSubsetSum where
  ‹isSubsetSum n (a::nat⇒int) s t ≡ s ⊆ {i. 1 ≤ i ∧ i ≤ n} ∧ (∑i∈s. a i) = t›

text ‹
  The knapsack problem: find k items among n with total weight ≤ B and value at least V
›
definition isKnapsack
where ‹isKnapsack (n::nat) (v::nat⇒int) (w::nat⇒int) (B::int) (V::int) (k::nat set) ≡ 
    (k ⊆ {i. 1 ≤ i ∧ i ≤ n})
  ∧ (∑i∈k. w i) ≤ B
  ∧ (∑i∈k. v i) ≥ V›

text ‹
  Solving a particular form of the knapsack problem solves the subset sum problem.
›
lemma ‹isSubsetSum n a s t = isKnapsack n a a t t s›
proof
  { assume h:‹isSubsetSum n a s t›
    hence ‹(∑i∈s. a i) = t› using isSubsetSum_def by simp
    hence ‹(∑i∈s. a i) ≤ t› and ‹(∑i∈s. a i) ≥ t› by simp+
    moreover from h have ‹s ⊆ {i. 1 ≤ i ∧ i ≤ n}› using isSubsetSum_def by simp
    ultimately have ‹isKnapsack n a a t t s› using isKnapsack_def by simp
  } thus ‹isSubsetSum n a s t ⟹ isKnapsack n a a t t s› .

  { assume h:‹isKnapsack n a a t t s›
    hence ‹(∑i∈s. a i) ≤ t› and ‹(∑i∈s. a i) ≥ t› using isKnapsack_def by simp+
    moreover from h have ‹s ⊆ {i. 1 ≤ i ∧ i ≤ n}› using isKnapsack_def by simp
    ultimately have ‹isSubsetSum n a s t› using isSubsetSum_def by simp
  } thus ‹isKnapsack n a a t t s ⟹ isSubsetSum n a s t› .
qed

end