(* 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 {* Some examples for testing Maximum *} theory MaximumTest imports Maximum begin text{* a test vector whose maximum component value we determine *} value "maximum {1..2} (\ x::nat . 1)" value "maximum {1..5} (\ x::nat . x)" (* for testing *) lemma test_arg_max: shows "{1,2} \ arg_max {1..3} (\x. if x < 3 then 100 else 0)" (* the 1st and 2nd elements in a vector [100,100,\] are maximal. *) apply(unfold arg_max_def) apply(simp add: maximum_def) oops (* broken since I've changed "primrec maximum" to "fun maximum" *) text{* an alternative proof of the same lemma -- still too trivial to test how declarative proofs \emph{actually} work *} lemma test_arg_max_declarative: shows "{1,2} \ arg_max {1..3} (\x. if x < 3 then 100 else 0)" (* the 1st and 2nd elements in a vector [100,100,\] are maximal. *) oops (* broken since I've changed "primrec maximum" to "fun maximum" *) (* unfolding arg_max_def by (simp add: maximum_def) *) end