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