(*
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