append

formal source

  93}
  94
  95/-- Append a transaction to a ledger. -/
  96def append (L : Ledger) (t : Transaction) : Ledger := {
  97  transactions := L.transactions ++ [t],
  98  total_debit := L.total_debit + t.debit,
  99  total_credit := L.total_credit + t.credit,
 100  global_balance := by
 101    have hL := L.global_balance
 102    have ht := t.balanced
 103    omega
 104}
 105
 106/-- The net balance of a ledger (should always be 0). -/
 107def net (L : Ledger) : ℤ := L.total_debit + L.total_credit
 108
 109/-- Ledger net is always zero. -/
 110theorem net_zero (L : Ledger) : L.net = 0 := L.global_balance
 111
 112/-- Concatenate two ledgers. -/
 113def concat (L₁ L₂ : Ledger) : Ledger := {
 114  transactions := L₁.transactions ++ L₂.transactions,
 115  total_debit := L₁.total_debit + L₂.total_debit,
 116  total_credit := L₁.total_credit + L₂.total_credit,
 117  global_balance := by
 118    have h₁ := L₁.global_balance
 119    have h₂ := L₂.global_balance
 120    omega
 121}
 122
 123theorem concat_preserves_balance (L₁ L₂ : Ledger) :
 124    (concat L₁ L₂).net = 0 := (concat L₁ L₂).global_balance
 125
 126end Ledger