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 [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 : 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 (α - δ<