diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,703 +1,704 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRYSTALS-Kyber CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs +Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Risk_Free_Lending/ROOT b/thys/Risk_Free_Lending/ROOT new file mode 100644 --- /dev/null +++ b/thys/Risk_Free_Lending/ROOT @@ -0,0 +1,8 @@ +chapter AFP + +session Risk_Free_Lending (AFP) = "HOL-Cardinals" + + options [timeout = 300] + theories + Risk_Free_Lending + document_files + "root.tex" diff --git a/thys/Risk_Free_Lending/Risk_Free_Lending.thy b/thys/Risk_Free_Lending/Risk_Free_Lending.thy new file mode 100644 --- /dev/null +++ b/thys/Risk_Free_Lending/Risk_Free_Lending.thy @@ -0,0 +1,2119 @@ +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) \ (\ 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 + \<^emph>\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 \<^emph>\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 \<^emph>\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 \<^emph>\ledger\ as a function from an index type \<^typ>\'a\ to + an \<^typ>\account\. A ledger could be thought of as an \<^emph>\indexed set\ of + accounts.\ + +type_synonym 'a ledger = "'a \ account" + +subsection \Balanced Ledgers \label{subsec:balanced-ledgers}\ + +text \We say a ledger is \<^emph>\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 \<^emph>\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 \<^emph>\protocol\ for safely transferring value + from one account to another.\ + +text \We enforce that every transfer is \<^emph>\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 + \<^emph>\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 \<^emph>\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 \<^emph>\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 \<^emph>\rate function\. + We denote rate functions with @{term [show_types] "\ :: nat \ real"}. + In principle this function obeys the rules: + \<^item> \<^term>\\ (0::nat) = (0 ::real)\ -- Cash is not returned. + \<^item> \<^term>\\n ::nat . \ n < (1 :: real)\ -- The fraction of a loan + returned never exceeds 1. + \<^item> \<^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 \<^emph>\lazily\) update ever \<^emph>\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 \<^emph>\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 \<^emph>\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 \<^emph>\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 \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 \<^emph>\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 \<^emph>\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 + \<^emph>\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 diff --git a/thys/Risk_Free_Lending/document/root.tex b/thys/Risk_Free_Lending/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Risk_Free_Lending/document/root.tex @@ -0,0 +1,80 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Risk-Free Lending} +\author{Matthew Doty} +\maketitle + +\begin{abstract} + We construct an abstract ledger supporting the \emph{risk-free + lending} protocol. The risk-free lending protocol is a system for + issuing and exchanging novel financial products we call + \emph{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 \emph{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. +\end{abstract} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: