(*
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 SingleGoodAuction *}
theory SingleGoodAuctionTest
imports SingleGoodAuction
begin
subsection {* Allocation *}
subsubsection {* Sample lemma: The allocation, in which the first participant wins (whatever the bids) is an allocation. *}
definition all_bid_1 :: "real vector" where
"all_bid_1 = (\x. 1)"
(* In contrast to Theorema, Isabelle can't _compute_ universal quantification in the finite case.
value "bids 1 all_bid_1"
*)
(*
lemma bid_all_bid_1:
shows "bids 1 all_bid_1"
apply(unfold bids_def all_bid_1_def)
apply(unfold non_negative_real_vector_def)
apply(auto)
done
*)
(*
definition first_wins :: "allocation"
where
"first_wins _ i \ i = 1" (* whatever the bids, the first participant wins *)
*)
(* for testing
lemma only_wins_is_allocation:
shows "allocation 1 all_bid_1 first_wins"
apply(unfold allocation_def)
apply(unfold true_for_exactly_one_member_def)
apply(unfold first_wins_def)
apply(auto)
apply(rule bid_all_bid_1)
apply(blast)
done
*)
(* This is a more tactic-free syntax; I think here it doesn't really make sense to write down explicit proof steps.
lemma only_wins_is_allocation_declarative:
shows "allocation 1 all_bid_1 first_wins"
unfolding allocation_def true_for_exactly_one_member_def first_wins_def using bid_all_bid_1
by auto *)
(*
subsection {* Payoff *}
(* for testing *)
value "payoff 5 True 2" (* I ascribed the value 5 to the good, won the auction, and had to pay 2. *)
*)
end