(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Manfred Kerber * Christoph Lange * Colin Rowat * Makarius Wenzel Dually licenced under * Creative Commons Attribution (CC-BY) 3.0 * ISC License (1-clause BSD License) See LICENSE file for details (Rationale for this dual licence: http://arxiv.org/abs/1107.3212) *) header {* Vectors, implemented as functions from an index set to some other set *} theory Vectors imports Main begin subsection {* Preliminaries *} type_synonym index = "nat" type_synonym 'a vector = "index \ 'a" subsubsection {* Some component-wise operations for vectors *} definition zero :: "'a::zero vector" where "zero = (\ x. 0)" (* TODO CL: introduce infix notation as per https://github.com/formare/auctions/issues/24 *) definition le :: "index set \ ('a::ord) vector \ ('a::ord) vector \ bool" where "le N v w \ (\i \ N . v i \ w i)" (* TODO CL: introduce infix notation as per https://github.com/formare/auctions/issues/24 *) definition eq :: "index set \ 'a vector \ 'a vector \ bool" where "eq N v w \ (\i \ N . v i = w i)" text{* we could also, in a higher-order style, generally define a vector whose components satisfy a predicate, and then parameterise this predicate with \$\geq 0\$ and \$> 0\$ *} definition non_negative :: "index set \ 'a::{zero,ord} vector \ bool" where "non_negative N v \ le N zero v" definition positive :: "index set \ 'a::{zero,ord} vector \ bool" where "positive N v \ le N zero v \ \eq N zero v" end