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:
›
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

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

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›
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›

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)›
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
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
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
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