(* TODO CL: ask whether jEdit's Isabelle mode disables word wrapping *)
(* TODO CL: report Isabelle/jEdit bug: no auto-indentation *)
(* TODO CL: report Isabelle/jEdit bug: when I set long lines to wrap at window boundary, wrapped part behaves badly: not editable *)
(* TODO CL: report Isabelle/jEdit bug: can't copy goal in output pane to clipboard *)
header {* Vickrey's Theorem:
Second price auctions support an equilibrium in weakly dominant strategies, and are efficient, if each participant bids their valuation of the good. *}
(*
Authors:
* Manfred Kerber
* Christoph Lange
* Colin Rowat
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)
*)
theory Vickrey
imports Main Real
begin
section{* Introduction *}
text{*
In second price (or Vickrey) auctions, bidders submit sealed bids; the highest bidder wins, and pays the highest bid of the \emph{remaining} bids; the losers pay nothing. (See \url{http://en.wikipedia.org/wiki/Vickrey_auction} for more information, including a discussion of variants used by eBay, Google and Yahoo!.) Vickrey proved that 'truth-telling' (i.e. submitting a bid equal to one's actual valuation of the good) was a weakly dominant strategy. This means that no bidder could do strictly better by bidding above or below its valuation \emph{whatever} the other bidders did. Thus, the auction is also efficient, awarding the item to the bidder with the highest valuation.
Vickrey was awarded Economics' Nobel prize in 1996 for his work. High level versions of his theorem, and 12 others, were collected in Eric Maskin's 2004 review of Paul Milgrom's influential book on auction theory ("The unity of auction theory: Milgrom's master class", Journal of Economic Literature, 42(4), pp. 1102--1115). Maskin himself won the Nobel in 2007.
*}
section{* Preliminaries *}
text{* some types defined for our convenience *}
type_synonym bool_vector = "nat \ bool"
type_synonym real_vector = "nat \ real"
type_synonym participant = "nat" (* ordinal number *)
type_synonym participants = "nat" (* cardinal number *)
text{* TODO CL: discuss whether it's intuitive to name some types as in the following lines.
However, being of one such type does not yet imply well-formedness; e.g. we could have an x::allocation, which, for some given n and b does not satisfy "allocation n b x". *}
type_synonym allocation = "real_vector \ participants \ bool"
type_synonym payments = "real_vector \ participants \ real" (* a payment vector is a function of a real_vector of bids *)
subsection{* some range checks for vectors *}
text{* To ease writing, we introduce a predicate for the range of participants. *}
definition in_range ::
"nat \ nat \ bool" where
"in_range n i \ 1 \ i \ i \ n"
text{* we could also, in a higher-order style, generally define a vector whose components satisfy a predicate, and then parameterize this predicate with $\geq 0$ and $> 0$*}
definition non_negative_real_vector ::
"nat \ real_vector \ bool" where
"non_negative_real_vector n v \ \ i::nat . in_range n i \ v i \ 0"
definition positive_real_vector ::
"nat \ real_vector \ bool" where
"positive_real_vector n v \ \ i::nat . in_range n i \ v i > 0"
section{* Deviation from a vector *}
text{* We define a function that modifies a vector by using an alternative value for a given component. *}
definition deviation ::
"nat \ real_vector \ real \ nat \ nat \ real" where
"deviation n bid alternative_value index j \ if j = index then alternative_value else bid j"
text{* We define a function that,
given one vector and an alternative one (in practice these will be strategy profiles), and a participant index i,
returns a vector that
has component i changed to the alternative value (i.e. in practice: the bid of participant i changed), whereas the others keep their original values.
Actually this definition doesn't check whether its arguments are non-negative real vectors (i.e. well-formed strategy profiles). *}
(* NOTE CL: I changed the order of arguments compared to our original Theorema attempts, as I think this one is more intuitive.
TODO CL: ask whether there a way of writing the alternative as b_hat, as it looks in the paper version?
TODO CL: discuss whether there any useful way we could use n for range-checking? Or don't we need n at all? *)
definition deviation_vec ::
"nat \ real_vector \ real_vector \ nat \ nat \ real" where
"deviation_vec n bid alternative_vec index \ deviation n bid (alternative_vec index) index"
(* the old component-wise definition had an error actually:
"deviation_vec n bid alternative_vec index j \ deviation n bid (alternative_vec j) index j"
^^ should have been index
so actually a component-wise definition was not necessary
the error didn't cause trouble because of the "j = index" condition in deviation_def,
but it prevented us from rewriting deviation_def into deviation without providing a component index, i.e. in curried form.
The latter was desired after introducing remaining_maximum_invariant
(which uses the more general "deviation" form instead of "deviation_vec") *)
section{* Strategy (bids) *}
text{*
Strategy and strategy profile (the vector of the strategies of all participants) are not fully defined below. We ignore the distribu-
tion and density function, as they do not play a role in the proof of the theorem.
So, for now, we do not model the random mapping from a participant's valuation to its bid, but simply consider its bid as a non-
negative number that doesn't depend on anything.
*}
definition bids ::
"participants \ real_vector \ bool" where
"bids n b \ non_negative_real_vector n b"
subsection{* Deviation from a bid *}
text{* A deviation from a bid is still a well-formed bid. *}
lemma deviated_bid_well_formed :
fixes n::participants and bid::real_vector and alternative_vec::real_vector and i::participant
assumes bids_original: "bids n bid" and bids_alternative: "bids n alternative_vec"
shows "bids n (deviation_vec n bid alternative_vec i)"
proof -
let ?dev = "deviation_vec n bid alternative_vec i"
have "\ k::participant . in_range n k \ ?dev k \ 0"
proof
fix k::participant
show "in_range n k \ ?dev k \ 0"
proof
assume k_range: "in_range n k"
show "?dev k \ 0"
proof (cases "?dev k = bid k")
case True
with k_range and bids_original show ?thesis unfolding deviation_def by (simp add: bids_def non_negative_real_vector_def)
next
case False
then have "?dev k = alternative_vec k" by (auto simp add: deviation_vec_def deviation_def)
(* "then" \ "from this", where "this" is the most recently established fact;
note that in line with https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-October/msg00057.html
and for easier general comprehensibility
we are not using the abbreviations "hence" \ "then have" and "thus" \ "then show" here. *)
with k_range and bids_alternative show ?thesis unfolding deviation_def by (simp add: bids_def non_negative_real_vector_def)
qed
qed
qed
then show ?thesis unfolding bids_def non_negative_real_vector_def .
qed
text{* A single-good auction is a mechanism specified by a function that maps a strategy profile to an outcome. *}
section{* Allocation *}
text{* A function x, which takes a vector of n bids, is an allocation if it returns True for one bidder and False for the others. *}
(* TODO CL: discuss whether we should use different names for "definition allocation" and "type_synonym allocation", as they denote two different things *)
(* TODO CL: record in our notes that the order of arguments of a function matters.
Note that I, CL, reordered the arguments on 2012-08-24.
When using the function x in a curried way, we can speak of (x b) as a vector of booleans, in a very straightforward way;
with a different order of arguments we'd have to use (\ index::nat . x index b).
*)
definition allocation :: "participants \ real_vector \ allocation \ bool" where
"allocation n b x \ bids n b \
(\k:: participant. in_range n k \ x b k \ (\j:: participant. j\k \ \x b j))"
text{* An allocation function uniquely determines the winner. *}
lemma allocation_unique :
fixes n::participants and x::allocation and b::real_vector and winner::participant
assumes allocation: "allocation n b x"
and winner: "x b winner"
shows "\j::participant. x b j \ j = winner"
by (metis allocation allocation_def winner)
subsection{* 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"
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 first_wins_def)
apply(blast)
done
*)
(* TODO CL: note that 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 and in_range_def and first_wins_def using bid_all_bid_1
by blast
section{* Payment *}
text{* Each participant pays some amount. *}
definition vickrey_payment ::
"participants \ real_vector \ payments \ bool" where
"vickrey_payment n b p \ \i:: participant. in_range n i \ p b i \ 0"
section{* Outcome *}
text{* The outcome of an auction is specified an allocation $\{0, 1\}^n$ and a vector of payments $R^n$
made by each participant; we don't introduce a dedicated definition for this. *}
section{* Valuation *}
text{* Each participant has a positive valuation of the good. *}
definition valuation ::
"participants \ real_vector \ bool" where
"valuation n v \ \i:: participant. in_range n i \ v i > 0"
text{* Any well-formed valuation vector is a well-formed bid vector *}
lemma valuation_is_bid :
fixes n::participants and v::real_vector
assumes "valuation n v"
shows "bids n v"
(* Sledgehammer finds a proof
by (metis assms bids_def non_negative_real_vector_def order_less_imp_le valuation_def)
but we prefer manual Isar style here. *)
proof -
have bids_def_unfolded: "\i:: participant. in_range n i \ v i \ 0"
proof
fix i::participant
show "in_range n i \ v i \ 0"
proof
assume "in_range n i"
with assms have "v i > 0" unfolding valuation_def by simp
then show "v i \ 0" by simp
(* If we had been searching the library for an applicable theorem, we could have used
find_theorems (200) "_ > _ \ _ \ _" where 200 is some upper search bound,
and would have found less_imp_le *)
qed
qed
show ?thesis using bids_def_unfolded unfolding bids_def non_negative_real_vector_def by simp
qed
section{* Payoff *}
text{* The payoff of the winner $(x_i=1)$, determined by a utility function u, is the difference between its valuation and the actual
payment. For the losers, it is the negative payment. *}
(* TODO CL: ask whether there is a built-in function that converts bool to {0,1} *)
definition payoff ::
"real \ bool \ real \ real" where
"payoff Valuation Allocation Payment \ Valuation * (if Allocation then 1 else 0) - Payment"
(* for testing *)
value "payoff 5 True 2" (* I ascribed the value 5 to the good, won the auction, and had to pay 2. *)
text{* For convenience in the subsequent formalisation, we also define the payoff as a vector, component-wise. *}
definition payoff_vector ::
"real_vector \ bool_vector \ real_vector \ participant \ real" where
"payoff_vector v concrete_x concrete_p i \ payoff (v i) (concrete_x i) (concrete_p i)"
section{* Maximum and related functions *}
text{*
The maximum component value of a vector y of non-negative reals is equal to the value of one of the components, and it is greater or equal than the values of all [other] components.
We implement this as a computable function, whereas in Theorema we had two axioms:
1. The maximum component value is equal to the value of one of the components
2. maximum\_is\_greater\_or\_equal
Here, we derive those two statements as lemmas from the definition of the computable function.
*}
primrec maximum ::
"nat \ real_vector \ real" where
"maximum 0 _ = 0" |
"maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" (* we don't enforce that y is non-negative, but this computation only makes sense for a non-negative y *)
text{* If two vectors are equal, their maximum components are equal too *}
lemma maximum_equal :
fixes n::nat and y::real_vector and z::real_vector
shows "(\i::nat . in_range n i \ y i = z i) \ maximum n y = maximum n z"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
show ?case
proof
assume assms: "\i::nat . in_range (Suc n) i \ y i = z i"
then have equal_so_far: "maximum n y = maximum n z" by (simp add: Suc.hyps le_SucI in_range_def)
from assms have equal_here: "y (Suc n) = z (Suc n)" using Suc.hyps by (metis Suc_eq_plus1 le_add2 le_refl in_range_def)
with equal_so_far show "maximum (Suc n) y = maximum (Suc n) z" unfolding maximum_def by (simp add: Suc.hyps)
qed
qed
text{* The maximum component, as defined above, is non-negative *}
lemma maximum_non_negative :
fixes n::nat and y::real_vector
shows "maximum n y \ 0"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" unfolding maximum_def by simp
also have "\ \ 0" by auto
finally show ?case .
qed
text{* The maximum component value is greater or equal than the values of all [other] components *}
lemma maximum_is_greater_or_equal :
fixes n::nat and y::real_vector
shows "\ i::nat . in_range n i \ maximum n y \ y i"
proof (induct n)
case 0
show ?case by (simp add: in_range_def)
next
case (Suc n)
show ?case
(* This is a shorter alternative to first proving
have "\ i::nat . in_range (Suc n) i \ maximum (Suc n) y \ y i"
and then trivially showing ?case *)
proof
fix i::nat
show "in_range (Suc n) i \ maximum (Suc n) y \ y i"
proof
assume 1: "in_range (Suc n) i"
have "max (maximum n y) (y (Suc n)) \ y i" (* TODO CL: ask whether there is a way of automatically decomposing the initial goal until we arrive at this expression *)
proof (cases "i = Suc n")
case True
then show ?thesis by (simp add: le_max_iff_disj)
next
case False
with 1 (* TODO CL: ask whether there is a nicer way to write this, without having to number assumption 1 *)
have "in_range n i" by (simp add: less_eq_Suc_le in_range_def)
then have "maximum n y \ y i" by (simp add: Suc.hyps)
then show ?thesis by (simp add: le_max_iff_disj)
qed
then show "maximum (Suc n) y \ y i" unfolding maximum_def by simp
qed
qed
qed
text{* The maximum component is one component *}
lemma maximum_is_component :
fixes n::nat and y::real_vector
shows "n > 0 \ non_negative_real_vector n y \ (\ i::nat . in_range n i \ maximum n y = y i)" (* reuse for "Suc n" inside proof didn't work when declaring premise with "assumes" *)
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
show ?case
proof
assume non_negative: "(Suc n) > 0 \ non_negative_real_vector (Suc n) y"
show "\ i::nat . in_range (Suc n) i \ maximum (Suc n) y = y i"
proof (cases "y (Suc n) \ maximum n y")
case True
from non_negative have "y (Suc n) \ 0" unfolding in_range_def non_negative_real_vector_def by simp
with True have "y (Suc n) = max 0 (max (maximum n y) (y (Suc n)))" by simp
also have "\ = maximum (Suc n) y" unfolding maximum_def by simp
finally have "y (Suc n) = maximum (Suc n) y" .
then show ?thesis using in_range_def by auto
next
case False
have hyp: "n > 0 \ non_negative_real_vector n y \ (\ i::nat . in_range n i \ maximum n y = y i)" by (rule Suc.hyps)
have non_empty: "n > 0"
proof - (* by contradiction *)
{
assume "n = 0"
with False and non_negative have "y (Suc n) = maximum n y"
unfolding non_negative_real_vector_def maximum_def in_range_def
by simp
with False have "False" by simp
}
then show "n > 0" by blast
qed
from non_negative have pred_non_negative: "non_negative_real_vector n y"
unfolding non_negative_real_vector_def in_range_def
by simp
with non_empty and hyp obtain i::nat where pred_max: "in_range n i \ maximum n y = y i" by auto
with non_negative have y_i_non_negative: "0 \ y i" unfolding non_negative_real_vector_def in_range_def by simp
have "y i = maximum n y" using pred_max by simp
also have "\ = max (maximum n y) (y (Suc n))" using False by simp
(* TODO CL: ask for the difference between "from" and "using" (before/after goal).
In any case I got the impression that "with \ also have" breaks the chain of calculational reasoning. *)
also have "\ = max 0 (max (maximum n y) (y (Suc n)))" using non_negative and y_i_non_negative by (auto simp add: calculation min_max.le_iff_sup)
also have "\ = maximum (Suc n) y" unfolding maximum_def using non_empty by simp
finally have max: "y i = maximum (Suc n) y" .
from pred_max have "in_range (Suc n) i" by (simp add: in_range_def)
with max show ?thesis by auto
qed
qed
qed
text{* Being a component of a non-negative vector and being greater or equal than all other components uniquely defines a maximum component. *}
lemma maximum_sufficient :
fixes n::nat and y::real_vector and m::real
shows "non_negative_real_vector n y \ n > 0 \ (\ i::nat . in_range n i \ m \ y i) \ (\ i::nat . in_range n i \ m = y i) \ m = maximum n y"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
show ?case
proof
assume assms: "non_negative_real_vector (Suc n) y \ Suc n > 0 \ (\ i::nat . in_range (Suc n) i \ m \ y i) \ (\ i::nat . in_range (Suc n) i \ m = y i)"
(* now break this down into its conjunctives *)
from assms have non_negative: "non_negative_real_vector (Suc n) y" ..
(* ".." means: apply a canonical rule for the current context *)
from assms have non_empty: "Suc n > 0" by simp
from assms have greater_or_equal: "\ i::nat . in_range (Suc n) i \ m \ y i" by simp
from assms have is_component: "\ i::nat . in_range (Suc n) i \ m = y i" by simp
(* further preliminaries *)
from non_negative have pred_non_negative: "non_negative_real_vector n y"
unfolding non_negative_real_vector_def in_range_def by simp
(* then go on *)
from non_empty have max_def: "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" unfolding maximum_def by simp
also have "\ = m"
proof (cases "n = 0")
case True
with is_component have m_is_only_component: "m = y 1" unfolding in_range_def by auto
with non_negative have "m \ 0" unfolding non_negative_real_vector_def in_range_def by simp
(* we could break this down into further textbook-style steps, but their proofs turn out to be ugly as well, so we leave it at this high level *)
then have "max 0 (max (maximum 0 y) (y 1)) = m" by (auto simp add: m_is_only_component)
with True show ?thesis by auto (* this was (metis One_nat_def), but auto has access to simplification rules by default *)
next
case False
show ?thesis
proof cases
assume last_is_max: "y (Suc n) = m"
have "\ \ maximum n y"
proof -
from False and pred_non_negative and maximum_is_component have "\ k::nat . in_range n k \ maximum n y = y k" by auto
then obtain k::nat where "in_range n k \ maximum n y = y k" by auto
with greater_or_equal show ?thesis unfolding in_range_def by (simp add: le_Suc_eq)
(* TODO CL: ask whether we should have kept using metis here. Sledgehammer always suggests metis.
When auto or simp also works (which is the case here, but not always), is is more efficient? *)
qed
then show ?thesis using last_is_max by (metis less_max_iff_disj linorder_not_le maximum_non_negative min_max.sup_absorb1 min_max.sup_commute)
next
assume "y (Suc n) \ m"
with is_component have pred_is_component: "\k::nat . in_range n k \ m = y k"
unfolding in_range_def by (metis le_antisym not_less_eq_eq)
from greater_or_equal have "\k::nat . in_range n k \ m \ y k" unfolding in_range_def by simp
(* these, plus pred_non_negative, form the left hand side of the induction hypothesis *)
then have "m = maximum n y" by (metis False Suc gr0I pred_is_component pred_non_negative)
then show ?thesis
using in_range_def by (metis Suc_eq_plus1 greater_or_equal le_refl maximum_non_negative min_max.sup_absorb1 min_max.sup_absorb2 not_add_less2 not_leE)
qed
qed
finally show "m = maximum (Suc n) y" ..
qed
qed
(* TODO CL: discuss whether it makes sense to keep this lemma --- it's not used for "theorem vickreyA" but might still be useful for the toolbox *)
text{* Increasing the (actually: a) maximum component value keeps it the maximum. *}
lemma increment_keeps_maximum :
fixes n::nat and y::real_vector and y'::real_vector and max_index::nat and max::real and max'::real
shows "non_negative_real_vector n y
\ n > 0
\ in_range n max_index
\ maximum n y = y max_index
\ y max_index < max'
\ y' = (\ i::nat . if i = max_index then max' else y i)
\ maximum n y' = y' max_index"
proof
assume assms: "non_negative_real_vector n y
\ n > 0
\ in_range n max_index
\ maximum n y = y max_index
\ y max_index < max'
\ y' = (\ i::nat . if i = max_index then max' else y i)"
(* now break this down into its conjunctives *)
from assms have non_negative: "non_negative_real_vector n y" by simp
from assms have non_empty: "n > 0" by simp
from assms have index_range: "in_range n max_index" by simp
from assms have old_maximum: "maximum n y = y max_index" by simp
from assms have new_lt: "y max_index < max'" by simp
from assms have increment: "y' = (\ i::nat . if i = max_index then max' else y i)" by simp
(* now go on *)
then have new_component: "y' max_index = max'" by simp
from non_negative and index_range and new_lt have "\ \ 0" unfolding non_negative_real_vector_def by (auto simp add: linorder_not_less order_less_trans)
with non_negative and increment have new_non_negative: "non_negative_real_vector n y'" unfolding non_negative_real_vector_def by simp
from old_maximum and new_lt and increment
have greater_or_equal: "\ i::nat . in_range n i \ max' \ y' i"
by (metis linorder_not_less maximum_is_greater_or_equal order_less_trans order_refl)
from increment have "max' = y' max_index" by simp
(* now we have all prerequisites for applying maximum_sufficient *)
with new_non_negative and non_empty and greater_or_equal and index_range
show "maximum n y' = y' max_index" using maximum_sufficient by metis
qed
text{* a test vector whose maximum component value we determine *}
value "maximum 2 (\ x::nat . 1)"
value "maximum 5 (\ x::nat . x)"
text{* We define the set of maximal components of a vector y: *}
(* TODO CL: discuss whether we should define this in a computable way. If so, how? *)
(* TODO CL: discuss whether this function should return a set, or a vector. How to construct such a vector? Or should we define it as a predicate? *)
definition arg_max_set ::
"nat \ real_vector \ (nat set)" where
"arg_max_set n b \ {i. in_range n i \ maximum n b = b i}"
(* for testing *)
lemma test_arg_max_set:
shows "{1,2} \ arg_max_set 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_set_def in_range_def)
apply(simp add: maximum_def)
done
text{* an alternative proof of the same lemma --- still too trivial to test how declarative proofs \emph{actually} work *}
lemma test_arg_max_set_declarative:
shows "{1,2} \ arg_max_set 3 (\x. if x < 3 then 100 else 0)" (* the 1st and 2nd elements in a vector [100,100,\] are maximal. *)
unfolding arg_max_set_def in_range_def
by (simp add: maximum_def)
text{* constructing a new vector from a given one, by skipping one component *}
definition skip_index ::
"(nat \ 'a) \ nat \ (nat \ 'a)" where
"skip_index vector index = (\ i::nat . vector (if i < index then i else Suc i))"
text{* skipping one component in a non-negative vector keeps it non-negative *}
(* TODO CL: discuss whether we should actually prove the more general lemma that
skipping one component in a vector whose components each satisfy p still satisfies p (for a suitable p) *)
lemma skip_index_keeps_non_negativity :
fixes n::nat and v::real_vector
assumes non_empty: "n > 0"
and non_negative: "non_negative_real_vector n v"
shows "\i::nat . in_range n i \ non_negative_real_vector (n-(1::nat)) (skip_index v i)"
proof
fix i::nat
show "in_range n i \ non_negative_real_vector (n-(1::nat)) (skip_index v i)"
proof
assume "in_range n i"
have "\j::nat. in_range (n-(1::nat)) j \ (skip_index v i) j \ 0"
proof
fix j::nat
show "in_range (n-(1::nat)) j \ (skip_index v i) j \ 0"
proof
assume j_range: "in_range (n-(1::nat)) j"
show "(skip_index v i) j \ 0"
proof (cases "j < i")
case True
then have "(skip_index v i) j = v j" unfolding skip_index_def by simp
with j_range and non_negative show ?thesis
unfolding non_negative_real_vector_def in_range_def
by (auto simp add: leD less_imp_diff_less not_leE)
next
case False
then have "(skip_index v i) j = v (Suc j)" unfolding skip_index_def by simp
with j_range and non_negative show ?thesis
unfolding non_negative_real_vector_def in_range_def
by (auto simp add: leD less_imp_diff_less not_leE)
qed
qed
qed
then show "non_negative_real_vector (n-(1::nat)) (skip_index v i)" unfolding non_negative_real_vector_def by simp
qed
qed
text{* when two vectors differ in one component, skipping that component makes the vectors equal *}
lemma equal_by_skipping :
fixes n::nat and v::real_vector and w::real_vector and j::nat
assumes non_empty: "n > 0"
and j_range: "in_range n j"
and equal_except: "\i::nat . in_range n i \ i \ j \ v i = w i"
shows "\k::nat . in_range (n-(1::nat)) k \ (skip_index v j) k = (skip_index w j) k"
proof
fix k::nat
show "in_range (n-(1::nat)) k \ (skip_index v j) k = (skip_index w j) k"
proof
assume k_range: "in_range (n-(1::nat)) k"
show "(skip_index v j) k = (skip_index w j) k"
proof (cases "k < j")
case True
then have "(skip_index v j) k = v k"
and "(skip_index w j) k = w k"
unfolding skip_index_def by auto
with equal_except and k_range and True show ?thesis
using in_range_def by (metis diff_le_self le_trans less_not_refl)
next
case False
then have "(skip_index v j) k = v (Suc k)"
and "(skip_index w j) k = w (Suc k)"
unfolding skip_index_def by auto
with equal_except and k_range and False show ?thesis
using in_range_def
by (metis One_nat_def diff_0_eq_0 diff_Suc_Suc diff_less le_neq_implies_less lessI less_imp_diff_less linorder_not_less not_less_eq_eq)
qed
qed
qed
text{* We define the maximum component value that remains after removing the i-th component from the non-negative real vector y: *}
(* TODO CL: discuss whether we can, or should, enforce that j is \ n *)
(* TODO CL: ask whether there is an easier or more efficient way of stating this *)
primrec maximum_except ::
"nat \ real_vector \ nat \ real" where
"maximum_except 0 _ _ = 0" |
"maximum_except (Suc n) y j =
maximum n (skip_index y j)" (* we take y but skip its j-th component *)
(* for testing *)
value "maximum_except 3 (\ x::nat . 4-x) 1" (* the maximum component value of the vector [3,2,1], except the first element, is 2 *)
text{* The maximum component that remains after removing one component from a vector is greater or equal than the values of all remaining components *}
lemma maximum_except_is_greater_or_equal :
fixes n::nat and y::real_vector and j::nat
shows "n \ 1 \ in_range n j \ (\ i::nat . in_range n i \ i \ j \ maximum_except n y j \ y i)"
proof
assume j_range: "n \ 1 \ in_range n j"
show "\i::nat. in_range n i \ i \ j \ maximum_except n y j \ y i"
proof
fix i::nat
show "in_range n i \ i \ j \ maximum_except n y j \ y i"
proof
let ?y_with_j_skipped = "skip_index y j"
from j_range obtain pred_n where pred_n: "n = Suc pred_n"
by (metis not0_implies_Suc not_one_le_zero)
(* wouldn't work with simp or rule alone *)
assume i_range: "in_range n i \ i \ j"
then show "maximum_except n y j \ y i"
proof (cases "i < j")
case True
then have can_skip_j: "y i = ?y_with_j_skipped i" unfolding skip_index_def by simp
from True and j_range and i_range and pred_n have "in_range pred_n i" unfolding in_range_def by simp
then have "maximum pred_n ?y_with_j_skipped \ ?y_with_j_skipped i" by (simp add: maximum_is_greater_or_equal)
with can_skip_j and pred_n show ?thesis by simp
next
case False
with i_range have case_False_nice: "i > j" by simp
then obtain pred_i where pred_i: "i = Suc pred_i" by (rule lessE) (* TODO CL: ask why this works. I do not really understand what lessE does. *)
from case_False_nice and pred_i (* wouldn't work with "from False" *)
have can_skip_j_and_shift_left: "y i = ?y_with_j_skipped pred_i" unfolding skip_index_def by simp
from case_False_nice and i_range and j_range and pred_i and pred_n
have (* actually 2 \ i, but we don't need this *) "in_range pred_n pred_i" unfolding in_range_def by simp
then have "maximum pred_n ?y_with_j_skipped \