Theory Risk_Free_Lending
theory Risk_Free_Lending
imports
Complex_Main
"HOL-Cardinals.Cardinals"
begin
section ‹Accounts \label{sec:accounts}›
text ‹We model accounts as functions from \<^typ>‹nat› to \<^typ>‹real› with
∗‹finite support›.›
text ‹Index @{term [show_types] "0 :: nat"} corresponds to an account's
∗‹cash› reserve (see \S\ref{sec:cash} for details).›
text ‹An index greater than \<^term>‹0::nat› may be regarded as corresponding to
a financial product. Such financial products are similar to ∗‹notes›.
Our notes are intended to be as easy to use for exchange as cash.
Positive values are debited. Negative values are credited.›
text ‹We refer to our new financial products as ∗‹risk-free loans›, because
they may be regarded as 0\% APY loans that bear interest for the debtor.
They are ∗‹risk-free› because we prove a ∗‹safety› theorem for them.
Our safety theorem proves no account will ``be in the red'', with more
credited loans than debited loans, provided an invariant is maintained.
We call this invariant ∗‹strictly solvent›. See \S\ref{sec:bulk-update}
for details on our safety proof.›
text ‹Each risk-free loan index corresponds to a progressively shorter
∗‹loan period›. Informally, a loan period is the time it takes for 99\%
of a loan to be returned given a ∗‹rate function› \<^term>‹ρ›. Rate
functions are introduced in \S\ref{sec:update}.›
text ‹It is unnecessary to track counter-party obligations so we do not.
See \S\ref{subsec:balanced-ledgers} and \S\ref{subsec:transfers} for
details.›
typedef account = "(fin_support 0 UNIV) :: (nat ⇒ real) set"
proof -
have "(λ _ . 0) ∈ fin_support 0 UNIV"
unfolding fin_support_def support_def
by simp
thus "∃x :: nat ⇒ real. x ∈ fin_support 0 UNIV" by fastforce
qed
text ‹The type definition for \<^typ>‹account› automatically generates two
functions: @{term [show_types] "Rep_account"} and
@{term [show_types] "Rep_account"}. \<^term>‹Rep_account› is a left inverse
of \<^term>‹Abs_account›. For convenience we introduce the following
shorthand notation:›
notation Rep_account ("π")
notation Abs_account ("ι")
text ‹Accounts form an Abelian group. ∗‹Summing› accounts will be helpful in
expressing how all credited and debited loans can cancel across a
ledger. This is done in \S\ref{subsec:balanced-ledgers}.›
text ‹It is also helpful to think of an account as a transferable quantity.
Transferring subtracts values under indexes from one account and adds
them to another. Transfers are presented in \S\ref{subsec:transfers}.›
instantiation account :: ab_group_add
begin
definition "0 = ι (λ _ . 0)"
definition "- α = ι (λ n . - π α n)"
definition "α⇩1 + α⇩2 = ι (λ n. π α⇩1 n + π α⇩2 n)"
definition "(α⇩1 :: account) - α⇩2 = α⇩1 + - α⇩2"
lemma Rep_account_zero [simp]: "π 0 = (λ _ . 0)"
proof -
have "(λ _ . 0) ∈ fin_support 0 UNIV"
unfolding fin_support_def support_def
by simp
thus ?thesis
unfolding zero_account_def
using Abs_account_inverse by blast
qed
lemma Rep_account_uminus [simp]:
"π (- α) = (λ n . - π α n)"
proof -
have "π α ∈ fin_support 0 UNIV"
using Rep_account by blast
hence "(λx. - π α x) ∈ fin_support 0 UNIV"
unfolding fin_support_def support_def
by force
thus ?thesis
unfolding uminus_account_def
using Abs_account_inverse by blast
qed
lemma fin_support_closed_under_addition:
fixes f g :: "'a ⇒ real"
assumes "f ∈ fin_support 0 A"
and "g ∈ fin_support 0 A"
shows "(λ x . f x + g x) ∈ fin_support 0 A"
using assms
unfolding fin_support_def support_def
by (metis (mono_tags) mem_Collect_eq sum.finite_Collect_op)
lemma Rep_account_plus [simp]:
"π (α⇩1 + α⇩2) = (λ n. π α⇩1 n + π α⇩2 n)"
unfolding plus_account_def
by (metis (full_types)
Abs_account_cases
Abs_account_inverse
fin_support_closed_under_addition)
instance
proof(standard)
fix a b c :: account
have "∀n. π (a + b) n + π c n = π a n + π (b + c) n"
using Rep_account_plus plus_account_def
by auto
thus "a + b + c = a + (b + c)"
unfolding plus_account_def
by force
next
fix a b :: account
show "a + b = b + a"
unfolding plus_account_def
by (simp add: add.commute)
next
fix a :: account
show "0 + a = a"
unfolding plus_account_def Rep_account_zero
by (simp add: Rep_account_inverse)
next
fix a :: account
show "- a + a = 0"
unfolding plus_account_def zero_account_def Rep_account_uminus
by (simp add: Abs_account_inverse)
next
fix a b :: account
show "a - b = a + - b"
using minus_account_def by blast
qed
end
section ‹Strictly Solvent›
text ‹An account is ∗‹strictly solvent› when, for every loan period, the sum of
all the debited and credited loans for longer periods is positive.
This implies that the ∗‹net asset value› for the account is positive.
The net asset value is the sum of all of the credit and debit in the
account. We prove ‹strictly_solvent α ⟹ 0 ≤ net_asset_value α› in
\S\ref{subsubsec:net-asset-value-properties}.›
definition strictly_solvent :: "account ⇒ bool" where
"strictly_solvent α ≡ ∀ n . 0 ≤ (∑ i≤n . π α i)"
lemma additive_strictly_solvent:
assumes "strictly_solvent α⇩1" and "strictly_solvent α⇩2"
shows "strictly_solvent (α⇩1 + α⇩2)"
using assms Rep_account_plus
unfolding strictly_solvent_def plus_account_def
by (simp add: Abs_account_inverse sum.distrib)
text ‹The notion of strictly solvent generalizes to a partial order, making
\<^typ>‹account› an ordered Abelian group.›
instantiation account :: ordered_ab_group_add
begin
definition less_eq_account :: "account ⇒ account ⇒ bool" where
"less_eq_account α⇩1 α⇩2 ≡ ∀ n . (∑ i≤n . π α⇩1 i) ≤ (∑ i≤n . π α⇩2 i)"
definition less_account :: "account ⇒ account ⇒ bool" where
"less_account α⇩1 α⇩2 ≡ (α⇩1 ≤ α⇩2 ∧ ¬ α⇩2 ≤ α⇩1)"
instance
proof(standard)
fix x y :: account
show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
unfolding less_account_def ..
next
fix x :: account
show "x ≤ x"
unfolding less_eq_account_def by auto
next
fix x y z :: account
assume "x ≤ y" and "y ≤ z"
thus "x ≤ z"
unfolding less_eq_account_def
by (meson order_trans)
next
fix x y :: account
assume "x ≤ y" and "y ≤ x"
hence ⋆: "∀ n . (∑ i≤n . π x i) = (∑ i≤n . π y i)"
unfolding less_eq_account_def
using dual_order.antisym by blast
{
fix n
have "π x n = π y n"
proof (cases "n = 0")
case True
then show ?thesis using ⋆
by (metis
atMost_0
empty_iff
finite.intros(1)
group_cancel.rule0
sum.empty sum.insert)
next
case False
from this obtain m where
"n = m + 1"
by (metis Nat.add_0_right Suc_eq_plus1 add_eq_if)
have "(∑ i≤n . π x i) = (∑ i≤n . π y i)"
using ⋆ by auto
hence
"(∑ i≤m . π x i) + π x n =
(∑ i≤m . π y i) + π y n"
using ‹n = m + 1›
by simp
moreover have "(∑ i≤m . π x i) = (∑ i≤m . π y i)"
using ⋆ by auto
ultimately show ?thesis by linarith
qed
}
hence "π x = π y" by auto
thus "x = y"
by (metis Rep_account_inverse)
next
fix x y z :: account
assume "x ≤ y"
{
fix n :: nat
have
"(∑ i≤n . π (z + x) i) =
(∑ i≤n . π z i) + (∑ i≤n . π x i)"
and
"(∑ i≤n . π (z + y) i) =
(∑ i≤n . π z i) + (∑ i≤n . π y i)"
unfolding Rep_account_plus
by (simp add: sum.distrib)+
moreover have "(∑ i≤n . π x i) ≤ (∑ i≤n . π y i)"
using ‹x ≤ y›
unfolding less_eq_account_def by blast
ultimately have
"(∑ i≤n . π (z + x) i) ≤ (∑ i≤n . π (z + y) i)"
by linarith
}
thus "z + x ≤ z + y"
unfolding
less_eq_account_def by auto
qed
end
text ‹An account is strictly solvent exactly when it is
∗‹greater than or equal to› @{term [show_types] "0 :: account"},
according to the partial order just defined.›
lemma strictly_solvent_alt_def: "strictly_solvent α = (0 ≤ α)"
unfolding
strictly_solvent_def
less_eq_account_def
using zero_account_def
by force
section ‹Cash \label{sec:cash}›
text ‹The ∗‹cash reserve› in an account is the value under index 0.›
text ‹Cash is treated with distinction. For instance it grows with interest
(see \S\ref{sec:interest}). When we turn to balanced ledgers in
\S\ref{subsec:balanced-ledgers}, we will see that cash is the only
quantity that does not cancel out.›
definition cash_reserve :: "account ⇒ real" where
"cash_reserve α = π α 0"
text ‹If ‹α› is strictly solvent then it has non-negative cash reserves.›
lemma strictly_solvent_non_negative_cash:
assumes "strictly_solvent α"
shows "0 ≤ cash_reserve α"
using assms
unfolding strictly_solvent_def cash_reserve_def
by (metis
atMost_0
empty_iff
finite.emptyI
group_cancel.rule0
sum.empty
sum.insert)
text ‹An account consists of ∗‹just cash› when it has no other credit or debit
other than under the first index.›
definition just_cash :: "real ⇒ account" where
"just_cash c = ι (λ n . if n = 0 then c else 0)"
lemma Rep_account_just_cash [simp]:
"π (just_cash c) = (λ n . if n = 0 then c else 0)"
proof(cases "c = 0")
case True
hence "just_cash c = 0"
unfolding just_cash_def zero_account_def
by force
then show ?thesis
using Rep_account_zero True by force
next
case False
hence "finite (support 0 UNIV (λ n :: nat . if n = 0 then c else 0))"
unfolding support_def
by auto
hence "(λ n :: nat . if n = 0 then c else 0) ∈ fin_support 0 UNIV"
unfolding fin_support_def
by blast
then show ?thesis
unfolding just_cash_def
using Abs_account_inverse by auto
qed
section ‹Ledgers›
text ‹We model a ∗‹ledger› as a function from an index type \<^typ>‹'a› to
an \<^typ>‹account›. A ledger could be thought of as an ∗‹indexed set› of
accounts.›
type_synonym 'a ledger = "'a ⇒ account"
subsection ‹Balanced Ledgers \label{subsec:balanced-ledgers}›
text ‹We say a ledger is ∗‹balanced› when all of the debited and credited
loans cancel, and all that is left is just cash.›
text ‹Conceptually, given a balanced ledger we are justified in not tracking
counter-party obligations.›
definition (in finite) balanced :: "'a ledger ⇒ real ⇒ bool" where
"balanced ℒ c ≡ (∑ a ∈ UNIV. ℒ a) = just_cash c"
text ‹Provided the total cash is non-negative, a balanced ledger is a special
case of a ledger which is globally strictly solvent.›
lemma balanced_strictly_solvent:
assumes "0 ≤ c" and "balanced ℒ c"
shows "strictly_solvent (∑ a ∈ UNIV. ℒ a)"
using assms
unfolding balanced_def strictly_solvent_def
by simp
lemma (in finite) finite_Rep_account_ledger [simp]:
"π (∑ a ∈ (A :: 'a set). ℒ a) n = (∑ a ∈ A. π (ℒ a) n)"
using finite
by (induct A rule: finite_induct, auto)
text ‹An alternate definition of balanced is that the \<^term>‹cash_reserve›
for each account sums to ‹c›, and all of the other credited and debited
assets cancels out.›
lemma (in finite) balanced_alt_def:
"balanced ℒ c =
((∑ a ∈ UNIV. cash_reserve (ℒ a)) = c
∧ (∀ n > 0. (∑ a ∈ UNIV. π (ℒ a) n) = 0))"
(is "?lhs = ?rhs")
proof (rule iffI)
assume ?lhs
hence "(∑ a ∈ UNIV. cash_reserve (ℒ a)) = c"
unfolding balanced_def cash_reserve_def
by (metis Rep_account_just_cash finite_Rep_account_ledger)
moreover
{
fix n :: "nat"
assume "n > 0"
with ‹?lhs› have "(∑ a ∈ UNIV. π (ℒ a) n) = 0"
unfolding balanced_def
by (metis
Rep_account_just_cash
less_nat_zero_code
finite_Rep_account_ledger)
}
ultimately show ?rhs by auto
next
assume ?rhs
have "cash_reserve (just_cash c) = c"
unfolding cash_reserve_def
using Rep_account_just_cash
by presburger
also have "... = (∑a∈UNIV. cash_reserve (ℒ a))" using ‹?rhs› by auto
finally have
"cash_reserve (∑ a ∈ UNIV. ℒ a) = cash_reserve (just_cash c)"
unfolding cash_reserve_def
by auto
moreover
{
fix n :: "nat"
assume "n > 0"
hence "π (∑ a ∈ UNIV. ℒ a) n = 0" using ‹?rhs› by auto
hence "π (∑ a ∈ UNIV. ℒ a) n = π (just_cash c) n"
unfolding Rep_account_just_cash using ‹n > 0› by auto
}
ultimately have
"∀ n . π (∑ a ∈ UNIV. ℒ a) n = π (just_cash c) n"
unfolding cash_reserve_def
by (metis gr_zeroI)
hence "π (∑ a ∈ UNIV. ℒ a) = π (just_cash c)"
by auto
thus ?lhs
unfolding balanced_def
using Rep_account_inject
by blast
qed
subsection ‹Transfers \label{subsec:transfers}›
text ‹A ∗‹transfer amount› is the same as an \<^typ>‹account›. It is just a
function from \<^typ>‹nat› to \<^typ>‹real› with finite support.›
type_synonym transfer_amount = "account"
text ‹When transferring between accounts in a ledger we make use of the
Abelian group operations defined in \S\ref{sec:accounts}.›
definition transfer :: "'a ledger ⇒ transfer_amount ⇒ 'a ⇒ 'a ⇒ 'a ledger" where
"transfer ℒ τ a b x = (if a = b then ℒ x
else if x = a then ℒ a - τ
else if x = b then ℒ b + τ
else ℒ x)"
text ‹Transferring from an account to itself is a no-op.›
lemma transfer_collapse:
"transfer ℒ τ a a = ℒ"
unfolding transfer_def by auto
text ‹After a transfer, the sum totals of all credited and debited assets are
preserved.›
lemma (in finite) sum_transfer_equiv:
fixes x y :: "'a"
shows "(∑ a ∈ UNIV. ℒ a) = (∑ a ∈ UNIV. transfer ℒ τ x y a)"
(is "_ = (∑ a ∈ UNIV. ?ℒ' a)")
proof (cases "x = y")
case True
show ?thesis
unfolding ‹x = y› transfer_collapse ..
next
case False
let ?sum_ℒ = "(∑ a ∈ UNIV - {x,y}. ℒ a)"
let ?sum_ℒ' = "(∑ a ∈ UNIV - {x,y}. ?ℒ' a)"
have "∀ a ∈ UNIV - {x,y}. ?ℒ' a = ℒ a "
by (simp add: transfer_def)
hence "?sum_ℒ' = ?sum_ℒ"
by (meson sum.cong)
have "{x,y} ⊆ UNIV" by auto
have "(∑ a ∈ UNIV. ?ℒ' a) = ?sum_ℒ' + (∑ a ∈ {x,y}. ?ℒ' a)"
using finite_UNIV sum.subset_diff [OF ‹{x,y} ⊆ UNIV›]
by fastforce
also have "... = ?sum_ℒ' + ?ℒ' x + ?ℒ' y"
using
‹x ≠ y›
finite
Diff_empty
Diff_insert_absorb
Diff_subset
group_cancel.add1
insert_absorb
sum.subset_diff
by (simp add: insert_Diff_if)
also have "... = ?sum_ℒ' + ℒ x - τ + ℒ y + τ"
unfolding transfer_def
using ‹x ≠ y›
by auto
also have "... = ?sum_ℒ' + ℒ x + ℒ y"
by simp
also have "... = ?sum_ℒ + ℒ x + ℒ y"
unfolding ‹?sum_ℒ' = ?sum_ℒ› ..
also have "... = ?sum_ℒ + (∑ a ∈ {x,y}. ℒ a)"
using
‹x ≠ y›
finite
Diff_empty
Diff_insert_absorb
Diff_subset
group_cancel.add1
insert_absorb
sum.subset_diff
by (simp add: insert_Diff_if)
ultimately show ?thesis
by (metis local.finite sum.subset_diff top_greatest)
qed
text ‹Since the sum totals of all credited and debited assets are preserved
after transfer, a ledger is balanced if and only if it is balanced after
transfer.›
lemma (in finite) balanced_transfer:
"balanced ℒ c = balanced (transfer ℒ τ a b) c"
unfolding balanced_def
using sum_transfer_equiv
by force
text ‹Similarly, the sum total of a ledger is strictly solvent if and only if
it is strictly solvent after transfer.›
lemma (in finite) strictly_solvent_transfer:
fixes x y :: "'a"
shows "strictly_solvent (∑ a ∈ UNIV. ℒ a) =
strictly_solvent (∑ a ∈ UNIV. transfer ℒ τ x y a)"
using sum_transfer_equiv
by presburger
subsection ‹The Valid Transfers Protocol›
text ‹In this section we give a ∗‹protocol› for safely transferring value
from one account to another.›
text ‹We enforce that every transfer is ∗‹valid›. Valid transfers are
intended to be intuitive. For instance one cannot transfer negative
cash. Nor is it possible for an account that only has \$50 to loan out
\$5,000,000.›
text ‹A transfer is valid just in case the \<^typ>‹transfer_amount› is strictly
solvent and the account being credited the transfer will be strictly
solvent afterwards.›
definition valid_transfer :: "account ⇒ transfer_amount ⇒ bool" where
"valid_transfer α τ = (strictly_solvent τ ∧ strictly_solvent (α - τ))"
lemma valid_transfer_alt_def: "valid_transfer α τ = (0 ≤ τ ∧ τ ≤ α)"
unfolding valid_transfer_def strictly_solvent_alt_def
by simp
text ‹Only strictly solvent accounts can make valid transfers to begin with.›
lemma only_strictly_solvent_accounts_can_transfer:
assumes "valid_transfer α τ"
shows "strictly_solvent α"
using assms
unfolding strictly_solvent_alt_def valid_transfer_alt_def
by auto
text ‹We may now give a key result: accounts remain strictly solvent given a
valid transfer.›
theorem strictly_solvent_still_strictly_solvent_after_valid_transfer:
assumes "valid_transfer (ℒ a) τ"
and "strictly_solvent (ℒ b)"
shows
"strictly_solvent ((transfer ℒ τ a b) a)"
"strictly_solvent ((transfer ℒ τ a b) b)"
using assms
unfolding
strictly_solvent_alt_def
valid_transfer_alt_def
transfer_def
by (cases "a = b", auto)
subsection ‹Embedding Conventional Cash-Only Ledgers›
text ‹We show that in a sense the ledgers presented generalize conventional
ledgers which only track cash.›
text ‹An account consisting of just cash is strictly solvent if and only if
it consists of a non-negative amount of cash.›
lemma strictly_solvent_just_cash_equiv:
"strictly_solvent (just_cash c) = (0 ≤ c)"
unfolding strictly_solvent_def
using Rep_account_just_cash just_cash_def by force
text ‹An empty account corresponds to @{term [show_types] "0 :: account"};
the account with no cash or debit or credit.›
lemma zero_account_alt_def: "just_cash 0 = 0"
unfolding zero_account_def just_cash_def
by simp
text ‹Building on @{thm zero_account_alt_def}, we have that \<^term>‹just_cash›
is an embedding into an ordered subgroup. This means that \<^term>‹just_cash›
is an order-preserving group homomorphism from the reals to the universe
of accounts.›
lemma just_cash_embed: "(a = b) = (just_cash a = just_cash b)"
proof (rule iffI)
assume "a = b"
thus "just_cash a = just_cash b"
by force
next
assume "just_cash a = just_cash b"
hence "cash_reserve (just_cash a) = cash_reserve (just_cash b)"
by presburger
thus "a = b"
unfolding Rep_account_just_cash cash_reserve_def
by auto
qed
lemma partial_nav_just_cash [simp]:
"(∑ i≤n . π (just_cash a) i) = a"
unfolding Rep_account_just_cash
by (induct n, auto)
lemma just_cash_order_embed: "(a ≤ b) = (just_cash a ≤ just_cash b)"
unfolding less_eq_account_def
by simp
lemma just_cash_plus [simp]: "just_cash a + just_cash b = just_cash (a + b)"
proof -
{
fix x
have "π (just_cash a + just_cash b) x = π (just_cash (a + b)) x"
proof (cases "x = 0")
case True
then show ?thesis
using Rep_account_just_cash just_cash_def by force
next
case False
then show ?thesis by simp
qed
}
hence "π (just_cash a + just_cash b) = π (just_cash (a + b))"
by auto
thus ?thesis
by (metis Rep_account_inverse)
qed
lemma just_cash_uminus [simp]: "- just_cash a = just_cash (- a)"
proof -
{
fix x
have "π (- just_cash a) x = π (just_cash (- a)) x"
proof (cases "x = 0")
case True
then show ?thesis
using Rep_account_just_cash just_cash_def by force
next
case False
then show ?thesis by simp
qed
}
hence "π (- just_cash a) = π (just_cash (- a))"
by auto
thus ?thesis
by (metis Rep_account_inverse)
qed
lemma just_cash_subtract [simp]:
"just_cash a - just_cash b = just_cash (a - b)"
by (simp add: minus_account_def)
text ‹Valid transfers as per @{thm valid_transfer_alt_def} collapse into
inequalities over the real numbers.›
lemma just_cash_valid_transfer:
"valid_transfer (just_cash c) (just_cash t) = ((0 :: real) ≤ t ∧ t ≤ c)"
unfolding valid_transfer_alt_def
by (simp add: less_eq_account_def)
text ‹Finally a ledger consisting of accounts with only cash is trivially
\<^term>‹balanced›.›
lemma (in finite) just_cash_summation:
fixes A :: "'a set"
assumes "∀ a ∈ A. ∃ c . ℒ a = just_cash c"
shows "∃ c . (∑ a ∈ A . ℒ a) = just_cash c"
using finite assms
by (induct A rule: finite_induct, auto, metis zero_account_alt_def)
lemma (in finite) just_cash_UNIV_is_balanced:
assumes "∀ a . ∃ c . ℒ a = just_cash c"
shows "∃ c . balanced ℒ c"
unfolding balanced_def
using
assms
just_cash_summation [where A=UNIV]
by simp
section ‹Interest \label{sec:interest}›
text ‹In this section we discuss how to calculate the interest accrued by
an account for a period. This is done by looking at the sum of all of
the credit and debit in an account. This sum is called the
∗‹net asset value› of an account.›
subsection ‹Net Asset Value \label{subsec:net-asset-value}›
text ‹The net asset value of an account is the sum of all of the non-zero
entries. Since accounts have finite support this sum is always well
defined.›
definition net_asset_value :: "account ⇒ real" where
"net_asset_value α = (∑ i | π α i ≠ 0 . π α i)"
subsubsection ‹The Shortest Period for Credited \& Debited Assets in an
Account›
text ‹Higher indexes for an account correspond to shorter loan periods.
Since accounts only have a finite number of entries, it makes sense to
talk about the ∗‹shortest› period an account has an entry for. The net
asset value for an account has a simpler expression in terms of that
account's shortest period.›
definition shortest_period :: "account ⇒ nat" where
"shortest_period α =
(if (∀ i. π α i = 0)
then 0
else Max {i . π α i ≠ 0})"
lemma shortest_period_uminus:
"shortest_period (- α) = shortest_period α"
unfolding shortest_period_def
using Rep_account_uminus uminus_account_def
by force
lemma finite_account_support:
"finite {i . π α i ≠ 0}"
proof -
have "π α ∈ fin_support 0 UNIV"
by (simp add: Rep_account)
thus ?thesis
unfolding fin_support_def support_def
by fastforce
qed
lemma shortest_period_plus:
"shortest_period (α + β) ≤ max (shortest_period α) (shortest_period β)"
(is "_ ≤ ?MAX")
proof (cases "∀ i . π (α + β) i = 0")
case True
then show ?thesis unfolding shortest_period_def by auto
next
case False
have "shortest_period α ≤ ?MAX" and "shortest_period β ≤ ?MAX"
by auto
moreover
have "∀ i > shortest_period α . π α i = 0"
and "∀ i > shortest_period β . π β i = 0"
unfolding shortest_period_def
using finite_account_support Max.coboundedI leD Collect_cong
by auto
ultimately
have "∀ i > ?MAX . π α i = 0"
and "∀ i > ?MAX . π β i = 0"
by simp+
hence "∀ i > ?MAX . π (α + β) i = 0"
by simp
hence "∀ i . π (α + β) i ≠ 0 ⟶ i ≤ ?MAX"
by (meson not_le)
thus ?thesis
unfolding shortest_period_def
using
finite_account_support [where α = "α + β"]
False
by simp
qed
lemma shortest_period_π:
assumes "π α i ≠ 0"
shows "π α (shortest_period α) ≠ 0"
proof -
let ?support = "{i . π α i ≠ 0}"
have A: "finite ?support"
using finite_account_support by blast
have B: "?support ≠ {}" using assms by auto
have "shortest_period α = Max ?support"
using assms
unfolding shortest_period_def
by auto
have "shortest_period α ∈ ?support"
unfolding ‹shortest_period α = Max ?support›
using Max_in [OF A B] by auto
thus ?thesis
by auto
qed
lemma shortest_period_bound:
assumes "π α i ≠ 0"
shows "i ≤ shortest_period α"
proof -
let ?support = "{i . π α i ≠ 0}"
have "shortest_period α = Max ?support"
using assms
unfolding shortest_period_def
by auto
have "shortest_period α ∈ ?support"
using assms shortest_period_π by force
thus ?thesis
unfolding ‹shortest_period α = Max ?support›
by (simp add: assms finite_account_support)
qed
text ‹Using \<^term>‹shortest_period› we may give an alternate definition for
\<^term>‹net_asset_value›.›
lemma net_asset_value_alt_def:
"net_asset_value α = (∑ i ≤ shortest_period α. π α i)"
proof -
let ?support = "{i . π α i ≠ 0}"
{
fix k
have "(∑ i | i ≤ k ∧ π α i ≠ 0 . π α i) = (∑ i ≤ k. π α i)"
proof (induct k)
case 0
thus ?case
proof (cases "π α 0 = 0")
case True
then show ?thesis
by fastforce
next
case False
{
fix i
have "(i ≤ 0 ∧ π α i ≠ 0) = (i ≤ 0)"
using False
by blast
}
hence "(∑ i | i ≤ 0 ∧ π α i ≠ 0. π α i) =
(∑i | i ≤ 0. π α i)"
by presburger
also have "... = (∑i ≤ 0. π α i)"
by simp
ultimately show ?thesis
by simp
qed
next
case (Suc k)
then show ?case
proof (cases "π α (Suc k) = 0")
case True
{
fix i
have "(i ≤ Suc k ∧ π α i ≠ 0) =
(i ≤ k ∧ π α i ≠ 0)"
using True le_Suc_eq by blast
}
hence "(∑i | i ≤ Suc k ∧ π α i ≠ 0. π α i) =
(∑i | i ≤ k ∧ π α i ≠ 0. π α i)"
by presburger
also have "... = (∑ i ≤ k. π α i)"
using Suc by blast
ultimately show ?thesis using True
by simp
next
let ?A = "{i . i ≤ Suc k ∧ π α i ≠ 0}"
let ?A' = "{i . i ≤ k ∧ π α i ≠ 0}"
case False
hence "?A = {i . (i ≤ k ∧ π α i ≠ 0) ∨ i = Suc k}"
by auto
hence "?A = ?A' ∪ {i . i = Suc k}"
by (simp add: Collect_disj_eq)
hence ⋆: "?A = ?A' ∪ {Suc k}"
by simp
hence ♡: "finite (?A' ∪ {Suc k})"
using finite_nat_set_iff_bounded_le
by blast
hence
"(∑i | i ≤ Suc k ∧ π α i ≠ 0. π α i) =
(∑ i ∈ ?A' ∪ {Suc k}. π α i)"
unfolding ⋆
by auto
also have "... = (∑ i ∈ ?A'. π α i) + (∑ i ∈ {Suc k}. π α i)"
using ♡
by force
also have "... = (∑ i ∈ ?A'. π α i) + π α (Suc k)"
by simp
ultimately show ?thesis
by (simp add: Suc)
qed
qed
}
hence †:
"(∑i | i ≤ shortest_period α ∧ π α i ≠ 0. π α i) =
(∑ i ≤ shortest_period α. π α i)"
by auto
{
fix i
have "(i ≤ shortest_period α ∧ π α i ≠ 0) = (π α i ≠ 0)"
using shortest_period_bound by blast
}
note ∙ = this
show ?thesis
using †
unfolding ∙ net_asset_value_def
by blast
qed
lemma greater_than_shortest_period_zero:
assumes "shortest_period α < m"
shows "π α m = 0"
proof -
let ?support = "{i . π α i ≠ 0}"
have "∀ i ∈ ?support . i ≤ shortest_period α"
by (simp add: finite_account_support shortest_period_def)
then show ?thesis
using assms
by (meson CollectI leD)
qed
text ‹An account's \<^term>‹net_asset_value› does not change when summing beyond
its \<^term>‹shortest_period›. This is helpful when computing aggregate
net asset values across multiple accounts.›
lemma net_asset_value_shortest_period_ge:
assumes "shortest_period α ≤ n"
shows "net_asset_value α = (∑ i ≤ n. π α i)"
proof (cases "shortest_period α = n")
case True
then show ?thesis
unfolding net_asset_value_alt_def by auto
next
case False
hence "shortest_period α < n" using assms by auto
hence "(∑ i=shortest_period α + 1.. n. π α i) = 0"
(is "?Σextra = 0")
using greater_than_shortest_period_zero
by auto
moreover have "(∑ i ≤ n. π α i) =
(∑ i ≤ shortest_period α. π α i) + ?Σextra"
(is "?lhs = ?Σshortest_period + _")
by (metis
‹shortest_period α < n›
Suc_eq_plus1
less_imp_add_positive
sum_up_index_split)
ultimately have "?lhs = ?Σshortest_period"
by linarith
then show ?thesis
unfolding net_asset_value_alt_def by auto
qed
subsubsection ‹Net Asset Value Properties \label{subsubsec:net-asset-value-properties}›
text ‹In this section we explore how \<^term>‹net_asset_value› forms an
order-preserving group homomorphism from the universe of accounts to the
real numbers.›
text ‹We first observe that \<^term>‹strictly_solvent› implies the more
conventional notion of solvent, where an account's net asset value is
non-negative.›
lemma strictly_solvent_net_asset_value:
assumes "strictly_solvent α"
shows "0 ≤ net_asset_value α"
using assms strictly_solvent_def net_asset_value_alt_def by auto
text ‹Next we observe that \<^term>‹net_asset_value› is a order preserving
group homomorphism from the universe of accounts to \<^term>‹real›.›
lemma net_asset_value_zero [simp]: "net_asset_value 0 = 0"
unfolding net_asset_value_alt_def
using zero_account_def by force
lemma net_asset_value_mono:
assumes "α ≤ β"
shows "net_asset_value α ≤ net_asset_value β"
proof -
let ?r = "max (shortest_period α) (shortest_period β)"
have "shortest_period α ≤ ?r" and "shortest_period β ≤ ?r" by auto
hence "net_asset_value α = (∑ i ≤ ?r. π α i)"
and "net_asset_value β = (∑ i ≤ ?r. π β i)"
using net_asset_value_shortest_period_ge by presburger+
thus ?thesis using assms unfolding less_eq_account_def by auto
qed
lemma net_asset_value_uminus: "net_asset_value (- α) = - net_asset_value α"
unfolding
net_asset_value_alt_def
shortest_period_uminus
Rep_account_uminus
by (simp add: sum_negf)
lemma net_asset_value_plus:
"net_asset_value (α + β) = net_asset_value α + net_asset_value β"
(is "?lhs = ?Σα + ?Σβ")
proof -
let ?r = "max (shortest_period α) (shortest_period β)"
have A: "shortest_period (α + β) ≤ ?r"
and B: "shortest_period α ≤ ?r"
and C: "shortest_period β ≤ ?r"
using shortest_period_plus by presburger+
have "?lhs = (∑ i ≤ ?r. π (α + β) i)"
using net_asset_value_shortest_period_ge [OF A] .
also have "… = (∑ i ≤ ?r. π α i + π β i)"
using Rep_account_plus by presburger
ultimately show ?thesis
using
net_asset_value_shortest_period_ge [OF B]
net_asset_value_shortest_period_ge [OF C]
by (simp add: sum.distrib)
qed
lemma net_asset_value_minus:
"net_asset_value (α - β) = net_asset_value α - net_asset_value β"
using additive.diff additive.intro net_asset_value_plus by blast
text ‹Finally we observe that \<^term>‹just_cash› is the right inverse of
\<^term>‹net_asset_value›.›
lemma net_asset_value_just_cash_left_inverse:
"net_asset_value (just_cash c) = c"
using net_asset_value_alt_def partial_nav_just_cash by presburger
subsection ‹Distributing Interest›
text ‹We next show that the total interest accrued for a ledger at
distribution does not change when one account makes a transfer to
another.›
definition (in finite) total_interest :: "'a ledger ⇒ real ⇒ real"
where "total_interest ℒ i = (∑ a ∈ UNIV. i * net_asset_value (ℒ a))"
lemma (in finite) total_interest_transfer:
"total_interest (transfer ℒ τ a b) i = total_interest ℒ i"
(is "total_interest ?ℒ' i = _")
proof (cases "a = b")
case True
show ?thesis
unfolding ‹a = b› transfer_collapse ..
next
case False
have "total_interest ?ℒ' i = (∑ a ∈ UNIV . i * net_asset_value (?ℒ' a))"
unfolding total_interest_def ..
also have "… = (∑ a ∈ UNIV - {a, b} ∪ {a,b}. i * net_asset_value (?ℒ' a))"
by (metis Un_Diff_cancel2 Un_UNIV_left)
also have "… = (∑ a ∈ UNIV - {a, b}. i * net_asset_value (?ℒ' a)) +
i * net_asset_value (?ℒ' a) + i * net_asset_value (?ℒ' b)"
(is "_ = ?Σ + _ + _")
using ‹a ≠ b›
by simp
also have "… = ?Σ +
i * net_asset_value (ℒ a - τ) +
i * net_asset_value (ℒ b + τ)"
unfolding transfer_def
using ‹a ≠ b›
by auto
also have "… = ?Σ +
i * net_asset_value (ℒ a) +
i * net_asset_value (- τ) +
i * net_asset_value (ℒ b) +
i * net_asset_value τ"
unfolding minus_account_def net_asset_value_plus
by (simp add: distrib_left)
also have "… = ?Σ +
i * net_asset_value (ℒ a) +
i * net_asset_value (ℒ b)"
unfolding net_asset_value_uminus
by linarith
also have "… = (∑ a ∈ UNIV - {a, b}. i * net_asset_value (ℒ a)) +
i * net_asset_value (ℒ a) +
i * net_asset_value (ℒ b)"
unfolding transfer_def
using ‹a ≠ b›
by force
also have "… = (∑ a ∈ UNIV - {a, b} ∪ {a,b}. i * net_asset_value (ℒ a))"
using ‹a ≠ b› by force
ultimately show ?thesis
unfolding total_interest_def
by (metis Diff_partition Un_commute top_greatest)
qed
section ‹Update \label{sec:update}›
text ‹Periodically the ledger is ∗‹updated›. When this happens interest is
distributed and loans are returned. Each time loans are returned, a
fixed fraction of each loan for each period is returned.›
text ‹The fixed fraction for returned loans is given by a ∗‹rate function›.
We denote rate functions with @{term [show_types] "ρ :: nat ⇒ real"}.
In principle this function obeys the rules:
▪ \<^term>‹ρ (0::nat) = (0 ::real)› -- Cash is not returned.
▪ \<^term>‹∀n ::nat . ρ n < (1 :: real)› -- The fraction of a loan
returned never exceeds 1.
▪ \<^term>‹∀n m :: nat. n < m ⟶ ((ρ n) :: real) < ρ m› -- Higher indexes
correspond to shorter loan periods. This in turn corresponds to
a higher fraction of loans returned at update for higher indexes.
›
text ‹In practice, rate functions determine the time it takes for 99\%
of the loan to be returned. However, the presentation here abstracts
away from time. In \S\ref{subsec:bulk-update-closed-form} we establish
a closed form for updating. This permits for a production implementation
to efficiently (albeit ∗‹lazily›) update ever ∗‹millisecond› if so
desired.›
definition return_loans :: "(nat ⇒ real) ⇒ account ⇒ account" where
"return_loans ρ α = ι (λ n . (1 - ρ n) * π α n)"
lemma Rep_account_return_loans [simp]:
"π (return_loans ρ α) = (λ n . (1 - ρ n) * π α n)"
proof -
have "(support 0 UNIV (λ n . (1 - ρ n) * π α n)) ⊆
(support 0 UNIV (π α))"
unfolding support_def
by (simp add: Collect_mono)
moreover have "finite (support 0 UNIV (π α))"
using Rep_account
unfolding fin_support_def by auto
ultimately have "finite (support 0 UNIV (λ n . (1 - ρ n) * π α n))"
using infinite_super by blast
hence "(λ n . (1 - ρ n) * π α n) ∈ fin_support 0 UNIV"
unfolding fin_support_def by auto
thus ?thesis
using
Rep_account
Abs_account_inject
Rep_account_inverse
return_loans_def
by auto
qed
text ‹As discussed, updating an account involves distributing interest and
returning its credited and debited loans.›
definition update_account :: "(nat ⇒ real) ⇒ real ⇒ account ⇒ account" where
"update_account ρ i α = just_cash (i * net_asset_value α) + return_loans ρ α"
definition update_ledger :: "(nat ⇒ real) ⇒ real ⇒ 'a ledger ⇒ 'a ledger"
where
"update_ledger ρ i ℒ a = update_account ρ i (ℒ a)"
subsection ‹Update Preserves Ledger Balance›
text ‹A key theorem is that if all credit and debit in a ledger cancel,
they will continue to cancel after update. In this sense the monetary
supply grows with the interest rate, but is otherwise conserved.›
text ‹A consequence of this theorem is that while counter-party obligations
are not explicitly tracked by the ledger, these obligations are fulfilled
as funds are returned by the protocol.›
definition shortest_ledger_period :: "'a ledger ⇒ nat" where
"shortest_ledger_period ℒ = Max (image shortest_period (range ℒ))"
lemma (in finite) shortest_ledger_period_bound:
fixes ℒ :: "'a ledger"
shows "shortest_period (ℒ a) ≤ shortest_ledger_period ℒ"
proof -
{
fix α :: account
fix S :: "account set"
assume "finite S" and "α ∈ S"
hence "shortest_period α ≤ Max (shortest_period ` S)"
proof (induct S rule: finite_induct)
case empty
then show ?case by auto
next
case (insert β S)
then show ?case
proof (cases "α = β")
case True
then show ?thesis
by (simp add: insert.hyps(1))
next
case False
hence "α ∈ S"
using insert.prems by fastforce
then show ?thesis
by (meson
Max_ge
finite_imageI
finite_insert
imageI
insert.hyps(1)
insert.prems)
qed
qed
}
moreover
have "finite (range ℒ)"
by force
ultimately show ?thesis
by (simp add: shortest_ledger_period_def)
qed
theorem (in finite) update_balanced:
assumes "ρ 0 = 0" and "∀n. ρ n < 1" and "0 ≤ i"
shows "balanced ℒ c = balanced (update_ledger ρ i ℒ) ((1 + i) * c)"
(is "_ = balanced ?ℒ' ((1 + i) * c)")
proof
assume "balanced ℒ c"
have "∀n>0. (∑a∈UNIV. π (?ℒ' a) n) = 0"
proof (rule allI, rule impI)
fix n :: nat
assume "n > 0"
{
fix a
let ?α' = "λn. (1 - ρ n) * π (ℒ a) n"
have "π (?ℒ' a) n = ?α' n"
unfolding
update_ledger_def
update_account_def
Rep_account_plus
Rep_account_just_cash
Rep_account_return_loans
using plus_account_def ‹n > 0›
by simp
}
hence "(∑a∈UNIV. π (?ℒ' a) n) =
(1 - ρ n) * (∑a∈UNIV. π (ℒ a) n)"
using finite_UNIV
by (metis (mono_tags, lifting) sum.cong sum_distrib_left)
thus "(∑a∈UNIV. π (?ℒ' a) n) = 0"
using ‹0 < n› ‹balanced ℒ c› local.balanced_alt_def by force
qed
moreover
{
fix S :: "'a set"
let ?ω = "shortest_ledger_period ℒ"
assume "(∑a∈S. cash_reserve (ℒ a)) = c"
and "∀n>0. (∑a∈S. π (ℒ a) n) = 0"
have "(∑a∈S. cash_reserve (?ℒ' a)) =
(∑a∈S. i * (∑ n ≤ ?ω. π (ℒ a) n) +
cash_reserve (ℒ a))"
using finite
proof (induct S arbitrary: c rule: finite_induct)
case empty
then show ?case
by auto
next
case (insert x S)
have "(∑a∈insert x S. cash_reserve (?ℒ' a)) =
(∑a∈insert x S. i * (∑ n ≤ ?ω. π (ℒ a) n) +
cash_reserve (ℒ a))"
unfolding update_ledger_def update_account_def cash_reserve_def
by (simp add: ‹ρ 0 = 0›,
metis (no_types)
shortest_ledger_period_bound
net_asset_value_shortest_period_ge)
thus ?case .
qed
also have "... = (∑a∈S. i * (∑ n = 1 .. ?ω. π (ℒ a) n) +
i * cash_reserve (ℒ a) + cash_reserve (ℒ a))"
unfolding cash_reserve_def
by (simp add:
add.commute
distrib_left
sum.atMost_shift
sum_bounds_lt_plus1)
also have "... = (∑a∈S. i * (∑ n = 1 .. ?ω. π (ℒ a) n) +
(1 + i) * cash_reserve (ℒ a))"
using finite
by (induct S rule: finite_induct, auto, simp add: distrib_right)
also have "... = i * (∑a∈S. (∑ n = 1 .. ?ω. π (ℒ a) n)) +
(1 + i) * (∑a∈S. cash_reserve (ℒ a))"
by (simp add: sum.distrib sum_distrib_left)
also have "... = i * (∑ n = 1 .. ?ω. (∑a∈S. π (ℒ a) n)) +
(1 + i) * c"
using ‹(∑a∈S. cash_reserve (ℒ a)) = c› sum.swap by force
finally have "(∑a∈S. cash_reserve (?ℒ' a)) = c * (1 + i)"
using ‹∀n>0. (∑a∈S. π (ℒ a) n) = 0›
by simp
}
hence "(∑a∈UNIV. cash_reserve (?ℒ' a)) = c * (1 + i)"
using ‹balanced ℒ c›
unfolding balanced_alt_def
by fastforce
ultimately show "balanced ?ℒ' ((1 + i) * c)"
unfolding balanced_alt_def
by auto
next
assume "balanced ?ℒ' ((1 + i) * c)"
have ⋆: "∀n>0. (∑a∈UNIV. π (ℒ a) n) = 0"
proof (rule allI, rule impI)
fix n :: nat
assume "n > 0"
hence "0 = (∑a∈UNIV. π (?ℒ' a) n)"
using ‹balanced ?ℒ' ((1 + i) * c)›
unfolding balanced_alt_def
by auto
also have "… = (∑a∈UNIV. (1 - ρ n) * π (ℒ a) n)"
unfolding
update_ledger_def
update_account_def
Rep_account_return_loans
Rep_account_just_cash
using ‹n > 0›
by auto
also have "… = (1 - ρ n) * (∑a∈UNIV. π (ℒ a) n)"
by (simp add: sum_distrib_left)
finally show "(∑a∈UNIV. π (ℒ a) n) = 0"
by (metis
‹∀ r . ρ r < 1›
diff_gt_0_iff_gt
less_numeral_extra(3)
mult_eq_0_iff)
qed
moreover
{
fix S :: "'a set"
let ?ω = "shortest_ledger_period ℒ"
assume "(∑a∈S. cash_reserve (?ℒ' a)) = (1 + i) * c"
and "∀n>0. (∑a∈S. π (ℒ a) n) = 0"
hence "(1 + i) * c = (∑a∈S. cash_reserve (?ℒ' a))"
by auto
also have "… = (∑a∈S. i * (∑ n ≤ ?ω. π (ℒ a) n) +
cash_reserve (ℒ a))"
using finite
proof (induct S rule: finite_induct)
case empty
then show ?case
by auto
next
case (insert x S)
have "(∑a∈insert x S. cash_reserve (?ℒ' a)) =
(∑a∈insert x S.
i * (∑ n ≤ ?ω. π (ℒ a) n) + cash_reserve (ℒ a))"
unfolding update_ledger_def update_account_def cash_reserve_def
by (simp add: ‹ρ 0 = 0›,
metis (no_types)
shortest_ledger_period_bound
net_asset_value_shortest_period_ge)
thus ?case .
qed
also have "… = (∑a∈S. i * (∑ n = 1 .. ?ω. π (ℒ a) n) +
i * cash_reserve (ℒ a) + cash_reserve (ℒ a))"
unfolding cash_reserve_def
by (simp add:
add.commute
distrib_left
sum.atMost_shift
sum_bounds_lt_plus1)
also have "… = (∑a∈S. i * (∑ n = 1 .. ?ω. π (ℒ a) n) +
(1 + i) * cash_reserve (ℒ a))"
using finite
by (induct S rule: finite_induct, auto, simp add: distrib_right)
also have "… = i * (∑a∈S. (∑ n = 1 .. ?ω. π (ℒ a) n)) +
(1 + i) * (∑a∈S. cash_reserve (ℒ a))"
by (simp add: sum.distrib sum_distrib_left)
also have "… = i * (∑ n = 1 .. ?ω. (∑a∈S. π (ℒ a) n)) +
(1 + i) * (∑a∈S. cash_reserve (ℒ a))"
using sum.swap by force
also have "… = (1 + i) * (∑a∈S. cash_reserve (ℒ a))"
using ‹∀n>0. (∑a∈S. π (ℒ a) n) = 0›
by simp
finally have "c = (∑a∈S. cash_reserve (ℒ a))"
using ‹0 ≤ i›
by force
}
hence "(∑a∈UNIV. cash_reserve (ℒ a)) = c"
unfolding cash_reserve_def
by (metis
Rep_account_just_cash
‹balanced ?ℒ' ((1 + i) * c)›
⋆
balanced_def
finite_Rep_account_ledger)
ultimately show "balanced ℒ c"
unfolding balanced_alt_def
by auto
qed
subsection ‹Strictly Solvent is Forever Strictly Solvent›
text ‹The final theorem presented in this section is that if an account is
strictly solvent, it will still be strictly solvent after update.›
text ‹This theorem is the key to how the system avoids counter party risk.
Provided the system enforces that all accounts are strictly solvent and
transfers are ∗‹valid› (as discussed in \S\ref{subsec:transfers}),
all accounts will remain strictly solvent forever.›
text ‹We first prove that \<^term>‹return_loans› is a group homomorphism.›
text ‹It is order preserving given certain assumptions.›
lemma return_loans_plus:
"return_loans ρ (α + β) = return_loans ρ α + return_loans ρ β"
proof -
let ?α = "π α"
let ?β = "π β"
let ?ραβ = "λn. (1 - ρ n) * (?α n + ?β n)"
let ?ρα = "λn. (1 - ρ n) * ?α n"
let ?ρβ = "λn. (1 - ρ n) * ?β n"
have "support 0 UNIV ?ρα ⊆ support 0 UNIV ?α"
"support 0 UNIV ?ρβ ⊆ support 0 UNIV ?β"
"support 0 UNIV ?ραβ ⊆ support 0 UNIV ?α ∪ support 0 UNIV ?β"
unfolding support_def
by auto
moreover have
"?α ∈ fin_support 0 UNIV"
"?β ∈ fin_support 0 UNIV"
using Rep_account by force+
ultimately have ⋆:
"?ρα ∈ fin_support 0 UNIV"
"?ρβ ∈ fin_support 0 UNIV"
"?ραβ ∈ fin_support 0 UNIV"
unfolding fin_support_def
using finite_subset by auto+
{
fix n
have "π (return_loans ρ (α + β)) n =
π (return_loans ρ α + return_loans ρ β) n"
unfolding return_loans_def Rep_account_plus
using ⋆ Abs_account_inverse distrib_left by auto
}
hence "π (return_loans ρ (α + β)) =
π (return_loans ρ α + return_loans ρ β)"
by auto
thus ?thesis
by (metis Rep_account_inverse)
qed
lemma return_loans_zero [simp]: "return_loans ρ 0 = 0"
proof -
have "(λn. (1 - ρ n) * 0) = (λ_. 0)"
by force
hence "ι (λn. (1 - ρ n) * 0) = 0"
unfolding zero_account_def
by presburger
thus ?thesis
unfolding return_loans_def Rep_account_zero .
qed
lemma return_loans_uminus: "return_loans ρ (- α) = - return_loans ρ α"
by (metis
add.left_cancel
diff_self
minus_account_def
return_loans_plus
return_loans_zero)
lemma return_loans_subtract:
"return_loans ρ (α - β) = return_loans ρ α - return_loans ρ β"
by (simp add: additive.diff additive_def return_loans_plus)
text ‹As presented in \S\ref{sec:accounts}, each index corresponds to a
progressively shorter loan period. This is captured by a monotonicity
assumption on the rate function @{term [show_types] "ρ :: nat ⇒ real"}.
In particular, provided \<^term>‹∀ n . ρ n < (1 :: real)› and
\<^term>‹∀ n m :: nat . n < m ⟶ ρ n < (ρ m :: real)› then we know that
all outstanding credit is going away faster than loans debited for
longer periods.›
text ‹Given the monotonicity assumptions for a rate function
@{term [show_types] "ρ :: nat ⇒ real"}, we may in turn prove monotonicity
for \<^term>‹return_loans› over ‹(≤)::account ⇒ account ⇒ bool›.›
lemma return_loans_mono:
assumes "∀ n . ρ n < 1"
and "∀ n m . n ≤ m ⟶ ρ n ≤ ρ m"
and "α ≤ β"
shows "return_loans ρ α ≤ return_loans ρ β"
proof -
{
fix α :: account
assume "0 ≤ α"
{
fix n :: nat
let ?α = "π α"
let ?ρα = "λn. (1 - ρ n) * ?α n"
have "∀ n . 0 ≤ (∑ i≤n . ?α i)"
using ‹0 ≤ α›
unfolding less_eq_account_def Rep_account_zero
by simp
hence "0 ≤ (∑ i≤n . ?α i)" by auto
moreover have "(1 - ρ n) * (∑ i≤n . ?α i) ≤ (∑ i≤n . ?ρα i)"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
have "0 ≤ (1 - ρ (Suc n))"
by (simp add: ‹∀ n . ρ n < 1› less_eq_real_def)
moreover have "(1 - ρ (Suc n)) ≤ (1 - ρ n)"
using ‹∀ n m . n ≤ m ⟶ ρ n ≤ ρ m›
by simp
ultimately have
"(1 - ρ (Suc n)) * (∑ i≤n . ?α i) ≤ (1 - ρ n) * (∑ i≤n . ?α i)"
using ‹∀ n . 0 ≤ (∑ i≤n . ?α i)›
by (meson le_less mult_mono')
hence
"(1 - ρ (Suc n)) * (∑ i≤ Suc n . ?α i) ≤
(1 - ρ n) * (∑ i≤n . ?α i) + (1 - ρ (Suc n)) * (?α (Suc n))"
(is "_ ≤ ?X")
by (simp add: distrib_left)
moreover have
"?X ≤ (∑ i≤ Suc n . ?ρα i)"
using Suc.hyps by fastforce
ultimately show ?case by auto
qed
moreover have "0 < 1 - ρ n"
by (simp add: ‹∀ n . ρ n < 1›)
ultimately have "0 ≤ (∑ i≤n . ?ρα i)"
using dual_order.trans by fastforce
}
hence "strictly_solvent (return_loans ρ α)"
unfolding strictly_solvent_def Rep_account_return_loans
by auto
}
hence "0 ≤ return_loans ρ (β - α)"
using ‹α ≤ β›
by (simp add: strictly_solvent_alt_def)
thus ?thesis
by (metis
add_diff_cancel_left'
diff_ge_0_iff_ge
minus_account_def
return_loans_plus)
qed
lemma return_loans_just_cash:
assumes "ρ 0 = 0"
shows "return_loans ρ (just_cash c) = just_cash c"
proof -
have "(λn. (1 - ρ n) * π (ι (λn. if n = 0 then c else 0)) n)
= (λn. if n = 0 then (1 - ρ n) * c else 0)"
using Rep_account_just_cash just_cash_def by force
also have "… = (λn. if n = 0 then c else 0)"
using ‹ρ 0 = 0›
by force
finally show ?thesis
unfolding return_loans_def just_cash_def
by presburger
qed
lemma distribute_interest_plus:
"just_cash (i * net_asset_value (α + β)) =
just_cash (i * net_asset_value α) +
just_cash (i * net_asset_value β)"
unfolding just_cash_def net_asset_value_plus
by (metis
distrib_left
just_cash_plus
just_cash_def)
text ‹We now prove that \<^term>‹update_account› is an order-preserving group
homomorphism just as \<^term>‹just_cash›, \<^term>‹net_asset_value›, and
\<^term>‹return_loans› are.›
lemma update_account_plus:
"update_account ρ i (α + β) =
update_account ρ i α + update_account ρ i β"
unfolding
update_account_def
return_loans_plus
distribute_interest_plus
by simp
lemma update_account_zero [simp]: "update_account ρ i 0 = 0"
by (metis add_cancel_right_left update_account_plus)
lemma update_account_uminus:
"update_account ρ i (-α) = - update_account ρ i α"
unfolding update_account_def
by (simp add: net_asset_value_uminus return_loans_uminus)
lemma update_account_subtract:
"update_account ρ i (α - β) =
update_account ρ i α - update_account ρ i β"
by (simp add: additive.diff additive.intro update_account_plus)
lemma update_account_mono:
assumes "0 ≤ i"
and "∀ n . ρ n < 1"
and "∀ n m . n ≤ m ⟶ ρ n ≤ ρ m"
and "α ≤ β"
shows "update_account ρ i α ≤ update_account ρ i β"
proof -
have "net_asset_value α ≤ net_asset_value β"
using ‹α ≤ β› net_asset_value_mono by presburger
hence "i * net_asset_value α ≤ i * net_asset_value β"
by (simp add: ‹0 ≤ i› mult_left_mono)
hence "just_cash (i * net_asset_value α) ≤
just_cash (i * net_asset_value β)"
by (simp add: just_cash_order_embed)
moreover
have "return_loans ρ α ≤ return_loans ρ β"
using assms return_loans_mono by presburger
ultimately show ?thesis unfolding update_account_def
by (simp add: add_mono)
qed
text ‹It follows from monotonicity and @{thm update_account_zero [no_vars]} that
strictly solvent accounts remain strictly solvent after update.›
lemma update_preserves_strictly_solvent:
assumes "0 ≤ i"
and "∀ n . ρ n < 1"
and "∀ n m . n ≤ m ⟶ ρ n ≤ ρ m"
and "strictly_solvent α"
shows "strictly_solvent (update_account ρ i α)"
using assms
unfolding strictly_solvent_alt_def
by (metis update_account_mono update_account_zero)
section ‹Bulk Update \label{sec:bulk-update}›
text ‹In this section we demonstrate there exists a closed form for
bulk-updating an account.›
primrec bulk_update_account ::
"nat ⇒ (nat ⇒ real) ⇒ real ⇒ account ⇒ account"
where
"bulk_update_account 0 _ _ α = α"
| "bulk_update_account (Suc n) ρ i α =
update_account ρ i (bulk_update_account n ρ i α)"
text ‹As with \<^term>‹update_account›, \<^term>‹bulk_update_account› is an
order-preserving group homomorphism.›
text ‹We now prove that \<^term>‹update_account› is an order-preserving group
homomorphism just as \<^term>‹just_cash›, \<^term>‹net_asset_value›, and
\<^term>‹return_loans› are.›
lemma bulk_update_account_plus:
"bulk_update_account n ρ i (α + β) =
bulk_update_account n ρ i α + bulk_update_account n ρ i β"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case
using bulk_update_account.simps(2) update_account_plus by presburger
qed
lemma bulk_update_account_zero [simp]: "bulk_update_account n ρ i 0 = 0"
by (metis add_cancel_right_left bulk_update_account_plus)
lemma bulk_update_account_uminus:
"bulk_update_account n ρ i (-α) = - bulk_update_account n ρ i α"
by (metis add_eq_0_iff bulk_update_account_plus bulk_update_account_zero)
lemma bulk_update_account_subtract:
"bulk_update_account n ρ i (α - β) =
bulk_update_account n ρ i α - bulk_update_account n ρ i β"
by (simp add: additive.diff additive_def bulk_update_account_plus)
lemma bulk_update_account_mono:
assumes "0 ≤ i"
and "∀ n . ρ n < 1"
and "∀ n m . n ≤ m ⟶ ρ n ≤ ρ m"
and "α ≤ β"
shows "bulk_update_account n ρ i α ≤ bulk_update_account n ρ i β"
using assms
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case
using bulk_update_account.simps(2) update_account_mono by presburger
qed
text ‹In follows from the fact that \<^term>‹bulk_update_account› is an
order-preserving group homomorphism that the update protocol is ∗‹safe›.
Informally this means that provided we enforce every account is strictly
solvent then no account will ever have negative net asset value
(ie, be in the red).›
theorem bulk_update_safety:
assumes "0 ≤ i"
and "∀ n . ρ n < 1"
and "∀ n m . n ≤ m ⟶ ρ n ≤ ρ m"
and "strictly_solvent α"
shows "0 ≤ net_asset_value (bulk_update_account n ρ i α)"
using assms
by (metis
bulk_update_account_mono
bulk_update_account_zero
strictly_solvent_alt_def
strictly_solvent_net_asset_value)
subsection ‹Decomposition›
text ‹In order to express \<^term>‹bulk_update_account› using a closed
formulation, we first demonstrate how to ∗‹decompose› an account
into a summation of credited and debited loans for different periods.›
definition loan :: "nat ⇒ real ⇒ account" ("δ")
where
"δ n x = ι (λ m . if n = m then x else 0)"
lemma loan_just_cash: "δ 0 c = just_cash c"
unfolding just_cash_def loan_def
by force
lemma Rep_account_loan [simp]:
"π (δ n x) = (λ m . if n = m then x else 0)"
proof -
have "(λ m . if n = m then x else 0) ∈ fin_support 0 UNIV"
unfolding fin_support_def support_def
by force
thus ?thesis
unfolding loan_def
using Abs_account_inverse by blast
qed
lemma loan_zero [simp]: "δ n 0 = 0"
unfolding loan_def
using zero_account_def by fastforce
lemma shortest_period_loan:
assumes "c ≠ 0"
shows "shortest_period (δ n c) = n"
using assms
unfolding shortest_period_def Rep_account_loan
by simp
lemma net_asset_value_loan [simp]: "net_asset_value (δ n c) = c"
proof (cases "c = 0")
case True
then show ?thesis by simp
next
case False
hence "shortest_period (δ n c) = n" using shortest_period_loan by blast
then show ?thesis unfolding net_asset_value_alt_def by simp
qed
lemma return_loans_loan [simp]: "return_loans ρ (δ n c) = δ n ((1 - ρ n) * c)"
proof -
have "return_loans ρ (δ n c) =
ι (λna. (if n = na then (1 - ρ n) * c else 0))"
unfolding return_loans_def
by (metis Rep_account_loan mult.commute mult_zero_left)
thus ?thesis
by (simp add: loan_def)
qed
lemma account_decomposition:
"α = (∑ i ≤ shortest_period α. δ i (π α i))"
proof -
let ?p = "shortest_period α"
let ?πα = "π α"
let ?Σδ = "∑ i ≤ ?p. δ i (?πα i)"
{
fix n m :: nat
fix f :: "nat ⇒ real"
assume "n > m"
hence "π (∑ i ≤ m. δ i (f i)) n = 0"
by (induct m, simp+)
}
note ∙ = this
{
fix n :: nat
have "π ?Σδ n = ?πα n"
proof (cases "n ≤ ?p")
case True
{
fix n m :: nat
fix f :: "nat ⇒ real"
assume "n ≤ m"
hence "π (∑ i ≤ m. δ i (f i)) n = f n"
proof (induct m)
case 0
then show ?case by simp
next
case (Suc m)
then show ?case
proof (cases "n = Suc m")
case True
then show ?thesis using ∙ by auto
next
case False
hence "n ≤ m"
using Suc.prems le_Suc_eq by blast
then show ?thesis
by (simp add: Suc.hyps)
qed
qed
}
then show ?thesis using True by auto
next
case False
have "?πα n = 0"
unfolding shortest_period_def
using False shortest_period_bound by blast
thus ?thesis using False ∙ by auto
qed
}
thus ?thesis
by (metis Rep_account_inject ext)
qed
subsection ‹Simple Transfers›
text ‹Building on our decomposition, we can understand the necessary and
sufficient conditions to transfer a loan of \<^term>‹δ n c›.›
text ‹We first give a notion of the ∗‹reserves for a period ‹n››. This
characterizes the available funds for a loan of period ‹n› that an
account ‹α› possesses.›
definition reserves_for_period :: "account ⇒ nat ⇒ real" where
"reserves_for_period α n =
fold
min
[(∑ i≤k . π α i) . k ← [n..<shortest_period α+1]]
(∑ i≤n . π α i)"
lemma nav_reserves_for_period:
assumes "shortest_period α ≤ n"
shows "reserves_for_period α n = net_asset_value α"
proof cases
assume "shortest_period α = n"
hence "[n..<shortest_period α+1] = [n]"
by simp
hence "[(∑ i≤k . π α i) . k ← [n..<shortest_period α+1]] =
[(∑ i≤n . π α i)]"
by simp
then show ?thesis
unfolding reserves_for_period_def
by (simp add: ‹shortest_period α = n› net_asset_value_alt_def)
next
assume "shortest_period α ≠ n"
hence "shortest_period α < n"
using assms order_le_imp_less_or_eq by blast
hence "[(∑ i≤k . π α k) . k ← [n..<shortest_period α+1]] = []"
by force
hence "reserves_for_period α n = (∑ i≤n . π α i)"
unfolding reserves_for_period_def by auto
then show ?thesis
using assms net_asset_value_shortest_period_ge by presburger
qed
lemma reserves_for_period_exists:
"∃m≥n. reserves_for_period α n = (∑ i≤m . π α i)
∧ (∀u≥n. (∑ i≤m . π α i) ≤ (∑ i≤u . π α i))"
proof -
{
fix j
have "∃m≥n. (∑ i≤m . π α i) =
fold
min
[(∑ i≤k . π α i) . k ← [n..<j]]
(∑ i≤n . π α i)
∧ (∀u≥n. u < j ⟶ (∑ i≤m . π α i) ≤ (∑ i≤u . π α i))"
proof (induct j)
case 0
then show ?case by auto
next
case (Suc j)
then show ?case
proof cases
assume "j ≤ n"
thus ?thesis
by (simp, metis dual_order.refl le_less_Suc_eq)
next
assume "¬(j ≤ n)"
hence "n < j" by auto
obtain m where
"m ≥ n"
"∀u≥n. u < j ⟶ (∑ i≤m . π α i) ≤ (∑ i≤u . π α i)"
"(∑ i≤m . π α i) =
fold
min
[(∑ i≤k . π α i) . k ← [n..<j]]
(∑ i≤n . π α i)"
using Suc by blast
note ♡ = this
hence †: "min (∑ i≤m . π α i) (∑ i≤j . π α i) =
fold
min
[(∑ i≤k . π α i) . k ← [n..<Suc j]]
(∑ i≤n . π α i)"
(is "_ = ?fold")
using ‹n < j› by simp
show ?thesis
proof cases
assume "(∑ i≤m . π α i) < (∑ i≤j . π α i)"
hence
"∀u≥n. u < Suc j ⟶ (∑ i≤m . π α i) ≤ (∑ i≤u . π α i)"
by (metis
♡(2)
dual_order.order_iff_strict
less_Suc_eq)
thus ?thesis
using † ‹m ≥ n› by auto
next
assume ⋆: "¬ ((∑ i≤m . π α i) < (∑ i≤j . π α i))"
hence
"∀u≥n. u < j ⟶ (∑ i≤j . π α i) ≤ (∑ i≤u . π α i)"
using ♡(2)
by auto
hence
"∀u≥n. u < Suc j ⟶ (∑ i≤j . π α i) ≤ (∑ i≤u . π α i)"
by (simp add: less_Suc_eq)
also have "?fold = (∑ i≤j . π α i)"
using † ⋆ by linarith
ultimately show ?thesis
by (metis ‹n < j› less_or_eq_imp_le)
qed
qed
qed
}
from this obtain m where
"m ≥ n"
"(∑ i≤m . π α i) = reserves_for_period α n"
"∀u≥n. u < shortest_period α + 1
⟶ (∑ i≤m . π α i) ≤ (∑ i≤u . π α i)"
unfolding reserves_for_period_def
by blast
note ♢ = this
hence "(∑ i≤m . π α i) ≤ (∑ i≤shortest_period α . π α i)"
by (metis
less_add_one
nav_reserves_for_period
net_asset_value_alt_def
nle_le)
hence "∀u≥shortest_period α. (∑ i≤m . π α i) ≤ (∑ i≤u . π α i)"
by (metis
net_asset_value_alt_def
net_asset_value_shortest_period_ge)
hence "∀u≥n. (∑ i≤m . π α i) ≤ (∑ i≤u . π α i)"
by (metis ♢(3) Suc_eq_plus1 less_Suc_eq linorder_not_le)
thus ?thesis
using ♢(1) ♢(2)
by metis
qed
lemma permissible_loan_converse:
assumes "strictly_solvent (α - δ n c)"
shows "c ≤ reserves_for_period α n"
proof -
obtain m where
"n ≤ m"
"reserves_for_period α n = (∑ i≤m . π α i)"
using reserves_for_period_exists by blast
have "(∑ i≤m . π (α - δ n c) i) = (∑ i≤m . π α i) - c"
using ‹n ≤ m›
proof (induct m)
case 0
hence "n = 0" by auto
have "π (α - δ n c + δ n c) 0 = π (α - δ n c) 0 + π (δ n c) 0"
using Rep_account_plus by presburger
thus ?case
unfolding ‹n = 0›
by simp
next
case (Suc m)
then show ?case
proof cases
assume "n = Suc m"
hence "m < n" by auto
hence "(∑ i≤m . π (α - δ n c) i) = (∑ i≤m . π α i)"
proof(induct m)
case 0
then show ?case
by (metis
(no_types, opaque_lifting)
Rep_account_loan
Rep_account_plus
atMost_0 bot_nat_0.not_eq_extremum
diff_0_right
diff_add_cancel
empty_iff
finite.intros(1)
sum.empty
sum.insert)
next
case (Suc m)
hence "m < n" and "n ≠ Suc m"
using Suc_lessD by blast+
moreover have
"π (α - δ n c + δ n c) (Suc m) =
π (α - δ n c) (Suc m) + π (δ n c) (Suc m)"
using Rep_account_plus by presburger
ultimately show ?case by (simp add: Suc.hyps)
qed
moreover
have "π (α - δ (Suc m) c + δ (Suc m) c) (Suc m) =
π (α - δ (Suc m) c) (Suc m) + π (δ (Suc m) c) (Suc m)"
by (meson Rep_account_plus)
ultimately show ?thesis
unfolding ‹n = Suc m›
by simp
next
assume "n ≠ Suc m"
hence "n ≤ m"
using Suc.prems le_SucE by blast
have "π (α - δ n c + δ n c) (Suc m) =
π (α - δ n c) (Suc m) + π (δ n c) (Suc m)"
by (meson Rep_account_plus)
moreover have "0 = (if n = Suc m then c else 0)"
using ‹n ≠ Suc m› by presburger
ultimately show ?thesis
by (simp add: Suc.hyps ‹n ≤ m›)
qed
qed
hence "0 ≤ (∑ i≤m . π α i) - c"
by (metis assms strictly_solvent_def)
thus ?thesis
by (simp add: ‹reserves_for_period α n = sum (π α) {..m}›)
qed
lemma permissible_loan:
assumes "strictly_solvent α"
shows "strictly_solvent (α - δ n c) = (c ≤ reserves_for_period α n)"
proof
assume "strictly_solvent (α - δ n c)"
thus "c ≤ reserves_for_period α n"
using permissible_loan_converse by blast
next
assume "c ≤ reserves_for_period α n"
{
fix j
have "0 ≤ (∑ i≤j . π (α - δ n c) i)"
proof cases
assume "j < n"
hence "(∑ i≤j . π (α - δ n c) i) = (∑ i≤j . π α i)"
proof (induct j)
case 0
then show ?case
by (simp,
metis
Rep_account_loan
Rep_account_plus
‹j < n›
add.commute
add_0
diff_add_cancel
gr_implies_not_zero)
next
case (Suc j)
moreover have "π (α - δ n c + δ n c) (Suc j) =
π (α - δ n c) (Suc j) + π (δ n c) (Suc j)"
using Rep_account_plus by presburger
ultimately show ?case by simp
qed
thus ?thesis
by (metis assms strictly_solvent_def)
next
assume "¬ (j < n)"
hence "n ≤ j" by auto
obtain m where
"reserves_for_period α n = (∑ i≤m . π α i)"
"∀u≥n. (∑ i≤m . π α i) ≤ (∑ i≤u . π α i)"
using reserves_for_period_exists by blast
hence "∀u≥n. c ≤ (∑ i≤u . π α i)"
using ‹c ≤ reserves_for_period α n›
by auto
hence "c ≤ (∑ i≤j . π α i)"
using ‹n ≤ j› by presburger
hence "0 ≤ (∑ i≤j . π α i) - c"
by force
moreover have "(∑ i≤j . π α i) - c = (∑ i≤j . π (α - δ n c) i)"
using ‹n ≤ j›
proof (induct j)
case 0
hence "n = 0" by auto
have "π (α - δ 0 c + δ 0 c) 0 = π (α - δ 0 c) 0 + π (δ 0 c) 0"
using Rep_account_plus by presburger
thus ?case unfolding ‹n = 0› by simp
next
case (Suc j)
then show ?case
proof cases
assume "n = Suc j"
hence "j < n"
by blast
hence "(∑ i≤j . π (α - δ n c) i) = (∑ i≤j . π α i)"
proof (induct j)
case 0
then show ?case
by (simp,
metis
Rep_account_loan
Rep_account_plus
‹j < n›
add.commute
add_0
diff_add_cancel
gr_implies_not_zero)
next
case (Suc j)
moreover have "π (α - δ n c + δ n c) (Suc j) =
π (α - δ n c) (Suc j) + π (δ n c) (Suc j)"
using Rep_account_plus by presburger
ultimately show ?case by simp
qed
moreover have
"π (α - δ (Suc j) c + δ (Suc j) c) (Suc j) =
π (α - δ (Suc j) c) (Suc j) + π (δ (Suc j) c) (Suc j)"
using Rep_account_plus by presburger
ultimately show ?thesis
unfolding ‹n = Suc j›
by simp
next
assume "n ≠ Suc j"
hence "n ≤ j"
using Suc.prems le_SucE by blast
hence "(∑ i≤j . π α i) - c = (∑ i≤j . π (α - δ n c) i)"
using Suc.hyps by blast
moreover have "π (α - δ n c + δ n c) (Suc j) =
π (α - δ n c) (Suc j) + π (δ n c) (Suc j)"
using Rep_account_plus by presburger
ultimately show ?thesis
by (simp add: ‹n ≠ Suc j›)
qed
qed
ultimately show ?thesis by auto
qed
}
thus "strictly_solvent (α - δ n c)"
unfolding strictly_solvent_def
by auto
qed
subsection ‹Closed Forms \label{subsec:bulk-update-closed-form}›
text ‹We first give closed forms for loans \<^term>‹δ n c›. The simplest closed
form is for \<^term>‹just_cash›. Here the closed form is just the compound
interest accrued from each update.›
lemma bulk_update_just_cash_closed_form:
assumes "ρ 0 = 0"
shows "bulk_update_account n ρ i (just_cash c) =
just_cash ((1 + i) ^ n * c)"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
have "return_loans ρ (just_cash ((1 + i) ^ n * c)) =
just_cash ((1 + i) ^ n * c)"
using assms return_loans_just_cash by blast
thus ?case
using Suc net_asset_value_just_cash_left_inverse
by (simp add: update_account_def,
metis
add.commute
mult.commute
mult.left_commute
mult_1
ring_class.ring_distribs(2))
qed
lemma bulk_update_loan_closed_form:
assumes "ρ k ≠ 1"
and "ρ k > 0"
and "ρ 0 = 0"
and "i ≥ 0"
shows "bulk_update_account n ρ i (δ k c) =
just_cash (c * i * ((1 + i) ^ n - (1 - ρ k) ^ n) / (i + ρ k))
+ δ k ((1 - ρ k) ^ n * c)"
proof (induct n)
case 0
then show ?case
by (simp add: zero_account_alt_def)
next
case (Suc n)
have "i + ρ k > 0"
using assms(2) assms(4) by force
hence "(i + ρ k) / (i + ρ k) = 1"
by force
hence "bulk_update_account (Suc n) ρ i (δ k c) =
just_cash
((c * i) / (i + ρ k) * (1 + i) * ((1 + i) ^ n - (1 - ρ k) ^ n) +
c * i * (1 - ρ k) ^ n * ((i + ρ k) / (i + ρ k)))
+ δ k ((1 - ρ k) ^ (n + 1) * c)"
using Suc
by (simp add:
return_loans_plus
‹ρ 0 = 0›
return_loans_just_cash
update_account_def
net_asset_value_plus
net_asset_value_just_cash_left_inverse
add.commute
add.left_commute
distrib_left
mult.assoc
add_divide_distrib
distrib_right
mult.commute
mult.left_commute)
also have
"… =
just_cash
((c * i) / (i + ρ k) * (1 + i) * ((1 + i) ^ n - (1 - ρ k) ^ n) +
(c * i) / (i + ρ k) * (1 - ρ k) ^ n * (i + ρ k))
+ δ k ((1 - ρ k) ^ (n + 1) * c)"
by (metis (no_types, lifting) times_divide_eq_left times_divide_eq_right)
also have
"… =
just_cash
((c * i) / (i + ρ k) * (
(1 + i) * ((1 + i) ^ n - (1 - ρ k) ^ n)
+ (1 - ρ k) ^ n * (i + ρ k)))
+ δ k ((1 - ρ k) ^ (n + 1) * c)"
by (metis (no_types, lifting) mult.assoc ring_class.ring_distribs(1))
also have
"… =
just_cash
((c * i) / (i + ρ k) * ((1 + i) ^ (n + 1) - (1 - ρ k) ^ (n + 1)))
+ δ k ((1 - ρ k) ^ (n + 1) * c)"
by (simp add: mult.commute mult_diff_mult)
ultimately show ?case by simp
qed
text ‹We next give an ∗‹algebraic› closed form. This uses the ordered
abelian group that \<^typ>‹account›s form.›
lemma bulk_update_algebraic_closed_form:
assumes "0 ≤ i"
and "∀ n . ρ n < 1"
and "∀ n m . n < m ⟶ ρ n < ρ m"
and "ρ 0 = 0"
shows "bulk_update_account n ρ i α
= just_cash (
(1 + i) ^ n * (cash_reserve α)
+ (∑ k = 1..shortest_period α.
(π α k) * i * ((1 + i) ^ n - (1 - ρ k) ^ n)
/ (i + ρ k))
)
+ (∑k = 1..shortest_period α. δ k ((1 - ρ k) ^ n * π α k))"
proof -
{
fix m
have "∀ k ∈ {1..m}. ρ k ≠ 1 ∧ ρ k > 0"
by (metis
assms(2)
assms(3)
assms(4)
atLeastAtMost_iff
dual_order.refl
less_numeral_extra(1)
linorder_not_less
not_gr_zero)
hence ⋆: "∀ k ∈ {1..m}.
bulk_update_account n ρ i (δ k (π α k))
= just_cash ((π α k) * i * ((1 + i) ^ n - (1 - ρ k) ^ n)
/ (i + ρ k))
+ δ k ((1 - ρ k) ^ n * (π α k))"
using assms(1) assms(4) bulk_update_loan_closed_form by blast
have "bulk_update_account n ρ i (∑ k ≤ m. δ k (π α k))
= (∑ k ≤ m. bulk_update_account n ρ i (δ k (π α k)))"
by (induct m, simp, simp add: bulk_update_account_plus)
also have
"… = bulk_update_account n ρ i (δ 0 (π α 0))
+ (∑ k = 1..m. bulk_update_account n ρ i (δ k (π α k)))"
by (simp add: atMost_atLeast0 sum.atLeast_Suc_atMost)
also have
"… = just_cash ((1 + i) ^ n * cash_reserve α)
+ (∑ k = 1..m. bulk_update_account n ρ i (δ k (π α k)))"
using
‹ρ 0 = 0›
bulk_update_just_cash_closed_form
loan_just_cash
cash_reserve_def
by presburger
also have
"… = just_cash ((1 + i) ^ n * cash_reserve α)
+ (∑ k = 1..m.
just_cash ((π α k) * i * ((1 + i) ^ n - (1 - ρ k) ^ n)
/ (i + ρ k))
+ δ k ((1 - ρ k) ^ n * (π α k)))"
using ⋆ by auto
also have
"… = just_cash ((1 + i) ^ n * cash_reserve α)
+ (∑ k = 1..m.
just_cash ((π α k) * i * ((1 + i) ^ n - (1 - ρ k) ^ n)
/ (i + ρ k)))
+ (∑ k = 1..m. δ k ((1 - ρ k) ^ n * (π α k)))"
by (induct m, auto)
also have
"… = just_cash ((1 + i) ^ n * cash_reserve α)
+ just_cash
(∑ k = 1..m.
(π α k) * i * ((1 + i) ^ n - (1 - ρ k) ^ n) / (i + ρ k))
+ (∑ k = 1..m. δ k ((1 - ρ k) ^ n * (π α k)))"
by (induct m, auto, metis (no_types, lifting) add.assoc just_cash_plus)
ultimately have
"bulk_update_account n ρ i (∑ k ≤ m. δ k (π α k)) =
just_cash (
(1 + i) ^ n * cash_reserve α
+ (∑ k = 1..m.
(π α k) * i * ((1 + i) ^ n - (1 - ρ k) ^ n) / (i + ρ k)))
+ (∑ k = 1..m. δ k ((1 - ρ k) ^ n * (π α k)))"
by simp
}
note ∙ = this
have
"bulk_update_account n ρ i α
= bulk_update_account n ρ i (∑ k ≤ shortest_period α. δ k (π α k))"
using account_decomposition by presburger
thus ?thesis unfolding ∙ .
qed
text ‹We finally give a ∗‹functional› closed form for bulk updating an
account. Since the form is in terms of exponentiation, we may
efficiently compute the bulk update output using
∗‹exponentiation-by-squaring›.›
theorem bulk_update_closed_form:
assumes "0 ≤ i"
and "∀ n . ρ n < 1"
and "∀ n m . n < m ⟶ ρ n < ρ m"
and "ρ 0 = 0"
shows "bulk_update_account n ρ i α
= ι ( λ k .
if k = 0 then
(1 + i) ^ n * (cash_reserve α)
+ (∑ j = 1..shortest_period α.
(π α j) * i * ((1 + i) ^ n - (1 - ρ j) ^ n)
/ (i + ρ j))
else
(1 - ρ k) ^ n * π α k
)"
(is "_ = ι ?ν")
proof -
obtain ν where X: "ν = ?ν" by blast
moreover obtain ν' where Y:
"ν' = π ( just_cash (
(1 + i) ^ n * (cash_reserve α)
+ (∑ j = 1..shortest_period α.
(π α j) * i * ((1 + i) ^ n - (1 - ρ j) ^ n)
/ (i + ρ j))
)
+ (∑j = 1..shortest_period α. δ j ((1 - ρ j) ^ n * π α j)))"
by blast
moreover
{
fix k
have "∀ k > shortest_period α . ν k = ν' k"
proof (rule allI, rule impI)
fix k
assume "shortest_period α < k"
hence "ν k = 0"
unfolding X
by (simp add: greater_than_shortest_period_zero)
moreover have "ν' k = 0"
proof -
have "∀ c. π (just_cash c) k = 0"
using
Rep_account_just_cash
‹shortest_period α < k›
just_cash_def
by auto
moreover
have "∀ m < k. π (∑j = 1..m. δ j ((1 - ρ j) ^ n * π α j)) k = 0"
proof (rule allI, rule impI)
fix m
assume "m < k"
let ?πΣδ = "π (∑j = 1..m. δ j ((1 - ρ j) ^ n * π α j))"
have "?πΣδ k = (∑j = 1..m. π (δ j ((1 - ρ j) ^ n * π α j)) k)"
by (induct m, auto)
also have "… = (∑j = 1..m. 0)"
using ‹m < k›
by (induct m, simp+)
finally show "?πΣδ k = 0"
by force
qed
ultimately show ?thesis unfolding Y
using ‹shortest_period α < k› by force
qed
ultimately show "ν k = ν' k" by auto
qed
moreover have "∀ k . 0 < k ⟶ k ≤ shortest_period α ⟶ ν k = ν' k"
proof (rule allI, (rule impI)+)
fix k
assume "0 < k"
and "k ≤ shortest_period α"
have "ν k = (1 - ρ k) ^ n * π α k"
unfolding X
using ‹0 < k› by fastforce
moreover have "ν' k = (1 - ρ k) ^ n * π α k"
proof -
have "∀ c. π (just_cash c) k = 0"
using ‹0 < k› by auto
moreover
{
fix m
assume "k ≤ m"
have " π (∑j = 1..m. δ j ((1 - ρ j) ^ n * π α j)) k
= (∑j = 1..m. π (δ j ((1 - ρ j) ^ n * π α j)) k)"
by (induct m, auto)
also
have "… = (1 - ρ k) ^ n * π α k"
using ‹0 < k› ‹k ≤ m›
proof (induct m)
case 0
then show ?case by simp
next
case (Suc m)
then show ?case
proof (cases "k = Suc m")
case True
hence "k > m" by auto
hence "(∑j = 1..m. π (δ j ((1 - ρ j) ^ n * π α j)) k) = 0"
by (induct m, auto)
then show ?thesis
using ‹k > m› ‹k = Suc m›
by simp
next
case False
hence "(∑j = 1..m. π (δ j ((1 - ρ j) ^ n * π α j)) k)
= (1 - ρ k) ^ n * π α k"
using Suc.hyps Suc.prems(1) Suc.prems(2) le_Suc_eq by blast
moreover have "k ≤ m"
using False Suc.prems(2) le_Suc_eq by blast
ultimately show ?thesis using ‹0 < k› by simp
qed
qed
finally have
"π (∑j = 1..m. δ j ((1 - ρ j) ^ n * π α j)) k
= (1 - ρ k) ^ n * π α k" .
}
hence
"∀ m ≥ k.
π (∑j = 1..m. δ j ((1 - ρ j) ^ n * π α j)) k
= (1 - ρ k) ^ n * π α k" by auto
ultimately show ?thesis
unfolding Y
using ‹k ≤ shortest_period α›
by force
qed
ultimately show "ν k = ν' k"
by fastforce
qed
moreover have "ν 0 = ν' 0"
proof -
have "ν 0 = (1 + i) ^ n * (cash_reserve α)
+ (∑ j = 1..shortest_period α.
(π α j) * i * ((1 + i) ^ n - (1 - ρ j) ^ n)
/ (i + ρ j))"
using X by presburger
moreover
have "ν' 0 = (1 + i) ^ n * (cash_reserve α)
+ (∑ j = 1..shortest_period α.
(π α j) * i * ((1 + i) ^ n - (1 - ρ j) ^ n)
/ (i + ρ j))"
proof -
{
fix m
have "π (∑j = 1..m. δ j ((1 - ρ j) ^ n * π α j)) 0 = 0"
by (induct m, simp+)
}
thus ?thesis unfolding Y
by simp
qed
ultimately show ?thesis by auto
qed
ultimately have "ν k = ν' k"
by (metis linorder_not_less not_gr0)
}
hence "ι ν = ι ν'"
by presburger
ultimately show ?thesis
using
Rep_account_inverse
assms
bulk_update_algebraic_closed_form
by presburger
qed
end