\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{Duality of Linear Programming}
\author{René Thiemann}

\maketitle

\begin{abstract}
We formalize the weak and strong duality theorems of linear programming.
For the strong duality theorem we provide three sufficient 
preconditions: both the primal problem and the dual problem are satisfiable, 
the primal problem is satisfiable and bounded, or the dual problem
is satisfiable and bounded. The proofs are based on an existing formalization
of Farkas' Lemma.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

\section{Introduction}
The proofs are taken from a textbook on linear programming~\cite{schrijver1998theory}.
There clearly is already an related AFP entry on linear programming 
\cite{Linear_Programming-AFP} and we briefly explain the relationship
between that entry and this one.
\begin{itemize}
\item The other AFP entry provides an algorithm for solving linear programs based
on an existing simplex implementation. Since the simplex implementation is
formulated only for rational numbers, several results are only available for
rational numbers. Moreover, the simplex algorithm internally works on sets
of inequalities that are represented by linear polynomials, and there are 
conversions between matrix-vector inequalities and linear polynomial inequalities. 
Finally, that AFP entry does not contain the strong duality theorem,
which is the essential result in this AFP entry.
\item This AFP entry has completely been formalized 
  in the matrix-vector representation. It mainly consists of
  the strong duality theorems without any algorithms.
  The proof of these theorems are based on Farkas' Lemma which 
  is provided in \cite{Linear_Inequalities-AFP} for arbitrary linearly ordered fields. Therefore, also the duality theorems are 
proven in that generality without the restriction to rational numbers. 
\end{itemize}

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
