Theory Simplex.Simplex
section ‹The Simplex Algorithm›
theory Simplex
  imports
    Linear_Poly_Maps
    QDelta
    Rel_Chain
    Simplex_Algebra
    "HOL-Library.Multiset"
    "HOL-Library.RBT_Mapping"
    "HOL-Library.Code_Target_Numeral"
begin
text‹Linear constraints are of the form ‹p ⨝ c›, where ‹p› is
a homogenenous linear polynomial, ‹c› is a rational constant and ‹⨝ ∈
{<, >, ≤, ≥, =}›. Their abstract syntax is given by the ‹constraint› type, and semantics is given by the relation ‹⊨⇩c›, defined straightforwardly by primitive recursion over the
‹constraint› type. A set of constraints is satisfied,
denoted by ‹⊨⇩c⇩s›, if all constraints are. There is also an indexed
version ‹⊨⇩i⇩c⇩s› which takes an explicit set of indices and then only
demands that these constraints are satisfied.›