diff --git a/metadata/entries/Risk_Free_Lending.toml b/metadata/entries/Risk_Free_Lending.toml
--- a/metadata/entries/Risk_Free_Lending.toml
+++ b/metadata/entries/Risk_Free_Lending.toml
@@ -1,41 +1,42 @@
title = "Risk-Free Lending"
date = 2022-09-18
topics = [
"Mathematics/Games and economics",
]
abstract = """
We construct an abstract ledger supporting the risk-free
-lending protocol. The risk-free lending protocol is a
-system for issuing and exchanging novel financial products we call
-risk-free loan. The system allows one party to
-lend money at 0% APY to another party in exchange for a good
-or service. On every update of the ledger, accounts have interest
-distributed to them. Holders of lent assets keep interest accrued by
-those assets. After distributing interest, the system returns a fixed
-fraction of each loan. These fixed fractions determine loan
-periods. Loans for longer periods have a smaller fixed
-fraction returned. Loans may be re-lent or used as collateral for
-other loans. We give a sufficient criterion to enforce all accounts
-will forever be solvent. We give a protocol for maintaining this
-invariant when transferring or lending funds. We also show this
-invariant holds after update. Even though the system does not track
-counter-party obligations, we show that all credited and debited loans
-cancel and the monetary supply grows at a specified interest rate."""
+lending protocol. The risk-free lending protocol is a system for
+issuing and exchanging novel financial products we call risk-free
+loans. The system allows one party to lend money at 0% APY
+to another party in exchange for a good or service. On every update of
+the ledger, accounts have interest distributed to them. Holders of
+lent assets keep interest accrued by those assets. After distributing
+interest, the system returns a fixed fraction of each loan. These
+fixed fractions determine loan periods. Loans for longer
+periods have a smaller fixed fraction returned. Loans may be re-lent
+or used as collateral for other loans. We give a sufficient criterion
+to enforce that all accounts will forever be solvent. We give a
+protocol for maintaining this invariant when transferring or lending
+funds. We also show that this invariant holds after an update. Even
+though the system does not track counter-party obligations, we show
+that all credited and debited loans cancel, and the monetary supply
+grows at a specified interest rate."""
license = "bsd"
note = ""
[authors]
[authors.doty]
email = "doty_email"
[contributors]
[notify]
doty = "doty_email" # matt@w-d.org
[history]
[extra]
[related]
+dois = ["10.2139/ssrn.4254003"]
\ No newline at end of file
diff --git a/thys/Risk_Free_Lending/Risk_Free_Lending.thy b/thys/Risk_Free_Lending/Risk_Free_Lending.thy
--- a/thys/Risk_Free_Lending/Risk_Free_Lending.thy
+++ b/thys/Risk_Free_Lending/Risk_Free_Lending.thy
@@ -1,2119 +1,2444 @@
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
\<^emph>\finite support\.\
text \Index @{term [show_types] "0 :: nat"} corresponds to an account's
\<^emph>\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 \<^emph>\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 \<^emph>\risk-free loans\, because
they may be regarded as 0\% APY loans that bear interest for the debtor.
They are \<^emph>\risk-free\ because we prove a \<^emph>\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 \<^emph>\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
\<^emph>\loan period\. Informally, a loan period is the time it takes for 99\%
of a loan to be returned given a \<^emph>\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. \<^emph>\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 "\\<^sub>1 + \\<^sub>2 = \ (\ n. \ \\<^sub>1 n + \ \\<^sub>2 n)"
definition "(\\<^sub>1 :: account) - \\<^sub>2 = \\<^sub>1 + - \\<^sub>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]:
"\ (\\<^sub>1 + \\<^sub>2) = (\ n. \ \\<^sub>1 n + \ \\<^sub>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 \<^emph>\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 \<^emph>\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 \\<^sub>1" and "strictly_solvent \\<^sub>2"
shows "strictly_solvent (\\<^sub>1 + \\<^sub>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 \\<^sub>1 \\<^sub>2 \ \ n . (\ i\n . \ \\<^sub>1 i) \ (\ i\n . \ \\<^sub>2 i)"
definition less_account :: "account \ account \ bool" where
"less_account \\<^sub>1 \\<^sub>2 \ (\\<^sub>1 \ \\<^sub>2 \ \ \\<^sub>2 \ \\<^sub>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) \