[STATEMENT]
lemma bulk_update_account_mono:
  assumes "0 \<le> i"
  and "\<forall> n . \<rho> n < 1"
  and "\<forall> n m . n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m"
  and "\<alpha> \<le> \<beta>"
  shows "bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account 0 \<rho> i \<alpha> \<le> bulk_update_account 0 \<rho> i \<beta>
 2. \<And>n. \<lbrakk>\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>; 0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>

goal (2 subgoals):
 1. \<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account 0 \<rho> i \<alpha> \<le> bulk_update_account 0 \<rho> i \<beta>
 2. \<And>n. \<lbrakk>\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>; 0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>

goal (1 subgoal):
 1. bulk_update_account 0 \<rho> i \<alpha> \<le> bulk_update_account 0 \<rho> i \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bulk_update_account 0 \<rho> i \<alpha> \<le> bulk_update_account 0 \<rho> i \<beta>

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>; 0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>; 0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>; 0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
using bulk_update_account.simps(2) update_account_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> i; \<forall>n. \<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m; \<alpha> \<le> \<beta>\<rbrakk> \<Longrightarrow> bulk_update_account n \<rho> i \<alpha> \<le> bulk_update_account n \<rho> i \<beta>
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
\<alpha> \<le> \<beta>
bulk_update_account (Suc ?n) ?\<rho> ?i ?\<alpha> = update_account ?\<rho> ?i (bulk_update_account ?n ?\<rho> ?i ?\<alpha>)
\<lbrakk>0 \<le> ?i; \<forall>n. ?\<rho> n < 1; \<forall>n m. n \<le> m \<longrightarrow> ?\<rho> n \<le> ?\<rho> m; ?\<alpha> \<le> ?\<beta>\<rbrakk> \<Longrightarrow> update_account ?\<rho> ?i ?\<alpha> \<le> update_account ?\<rho> ?i ?\<beta>

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
bulk_update_account (Suc n) \<rho> i \<alpha> \<le> bulk_update_account (Suc n) \<rho> i \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem bulk_update_safety:
  assumes "0 \<le> i"
  and "\<forall> n . \<rho> n < 1"
  and "\<forall> n m . n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m"
  and "strictly_solvent \<alpha>"
  shows "0 \<le> net_asset_value (bulk_update_account n \<rho> i \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> net_asset_value (bulk_update_account n \<rho> i \<alpha>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n \<le> m \<longrightarrow> \<rho> n \<le> \<rho> m
strictly_solvent \<alpha>

goal (1 subgoal):
 1. 0 \<le> net_asset_value (bulk_update_account n \<rho> i \<alpha>)
[PROOF STEP]
by (metis
        bulk_update_account_mono
        bulk_update_account_zero
        strictly_solvent_alt_def
        strictly_solvent_net_asset_value)


[STATEMENT]
lemma loan_just_cash: "\<delta> 0 c = just_cash c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> 0 c = just_cash c
[PROOF STEP]
unfolding just_cash_def loan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> (\<lambda>m. if 0 = m then c else 0) = \<iota> (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
by force


[STATEMENT]
lemma Rep_account_loan [simp]:
  "\<pi> (\<delta> n x) = (\<lambda> m . if n = m then x else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<delta> n x) = (\<lambda>m. if n = m then x else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> (\<delta> n x) = (\<lambda>m. if n = m then x else 0)
[PROOF STEP]
have "(\<lambda> m . if n = m then x else 0) \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. if n = m then x else 0) \<in> fin_support 0 UNIV
[PROOF STEP]
unfolding fin_support_def support_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. if n = m then x else 0) \<in> {f. finite {x \<in> UNIV. f x \<noteq> 0}}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>m. if n = m then x else 0) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. \<pi> (\<delta> n x) = (\<lambda>m. if n = m then x else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>m. if n = m then x else 0) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. \<pi> (\<delta> n x) = (\<lambda>m. if n = m then x else 0)
[PROOF STEP]
unfolding loan_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>m. if n = m then x else 0) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. \<pi> (\<iota> (\<lambda>m. if n = m then x else 0)) = (\<lambda>m. if n = m then x else 0)
[PROOF STEP]
using Abs_account_inverse
[PROOF STATE]
proof (prove)
using this:
(\<lambda>m. if n = m then x else 0) \<in> fin_support 0 UNIV
?y \<in> fin_support 0 UNIV \<Longrightarrow> \<pi> (\<iota> ?y) = ?y

goal (1 subgoal):
 1. \<pi> (\<iota> (\<lambda>m. if n = m then x else 0)) = (\<lambda>m. if n = m then x else 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi> (\<delta> n x) = (\<lambda>m. if n = m then x else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loan_zero [simp]: "\<delta> n 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> n 0 = 0
[PROOF STEP]
unfolding loan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> (\<lambda>m. if n = m then 0 else 0) = 0
[PROOF STEP]
using zero_account_def
[PROOF STATE]
proof (prove)
using this:
0 = \<iota> (\<lambda>_. 0)

goal (1 subgoal):
 1. \<iota> (\<lambda>m. if n = m then 0 else 0) = 0
[PROOF STEP]
by fastforce


[STATEMENT]
lemma shortest_period_loan:
  assumes "c \<noteq> 0"
  shows "shortest_period (\<delta> n c) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period (\<delta> n c) = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. shortest_period (\<delta> n c) = n
[PROOF STEP]
unfolding shortest_period_def Rep_account_loan
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. (if \<forall>i. (if n = i then c else 0) = 0 then 0 else Max {i. (if n = i then c else 0) \<noteq> 0}) = n
[PROOF STEP]
by simp


[STATEMENT]
lemma net_asset_value_loan [simp]: "net_asset_value (\<delta> n c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value (\<delta> n c) = c
[PROOF STEP]
proof (cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
 2. c \<noteq> 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
 2. c \<noteq> 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. net_asset_value (\<delta> n c) = c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
net_asset_value (\<delta> n c) = c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
[PROOF STEP]
hence "shortest_period (\<delta> n c) = n"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. shortest_period (\<delta> n c) = n
[PROOF STEP]
using shortest_period_loan
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
?c \<noteq> 0 \<Longrightarrow> shortest_period (\<delta> ?n ?c) = ?n

goal (1 subgoal):
 1. shortest_period (\<delta> n c) = n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
shortest_period (\<delta> n c) = n

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> net_asset_value (\<delta> n c) = c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
shortest_period (\<delta> n c) = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
shortest_period (\<delta> n c) = n

goal (1 subgoal):
 1. net_asset_value (\<delta> n c) = c
[PROOF STEP]
unfolding net_asset_value_alt_def
[PROOF STATE]
proof (prove)
using this:
shortest_period (\<delta> n c) = n

goal (1 subgoal):
 1. sum (\<pi> (\<delta> n c)) {..shortest_period (\<delta> n c)} = c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
net_asset_value (\<delta> n c) = c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_loans_loan [simp]: "return_loans \<rho> (\<delta> n c) = \<delta> n ((1 - \<rho> n) * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> (\<delta> n c) = \<delta> n ((1 - \<rho> n) * c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. return_loans \<rho> (\<delta> n c) = \<delta> n ((1 - \<rho> n) * c)
[PROOF STEP]
have "return_loans \<rho> (\<delta> n c) =
          \<iota> (\<lambda>na. (if n = na then (1 - \<rho> n) * c else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> (\<delta> n c) = \<iota> (\<lambda>na. if n = na then (1 - \<rho> n) * c else 0)
[PROOF STEP]
unfolding return_loans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> (\<lambda>na. (1 - \<rho> na) * \<pi> (\<delta> n c) na) = \<iota> (\<lambda>na. if n = na then (1 - \<rho> n) * c else 0)
[PROOF STEP]
by (metis Rep_account_loan mult.commute mult_zero_left)
[PROOF STATE]
proof (state)
this:
return_loans \<rho> (\<delta> n c) = \<iota> (\<lambda>na. if n = na then (1 - \<rho> n) * c else 0)

goal (1 subgoal):
 1. return_loans \<rho> (\<delta> n c) = \<delta> n ((1 - \<rho> n) * c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
return_loans \<rho> (\<delta> n c) = \<iota> (\<lambda>na. if n = na then (1 - \<rho> n) * c else 0)

goal (1 subgoal):
 1. return_loans \<rho> (\<delta> n c) = \<delta> n ((1 - \<rho> n) * c)
[PROOF STEP]
by (simp add: loan_def)
[PROOF STATE]
proof (state)
this:
return_loans \<rho> (\<delta> n c) = \<delta> n ((1 - \<rho> n) * c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma account_decomposition:
  "\<alpha> = (\<Sum> i \<le> shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
let ?p = "shortest_period \<alpha>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
let ?\<pi>\<alpha> = "\<pi> \<alpha>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
let ?\<Sigma>\<delta> = "\<Sum> i \<le> ?p. \<delta> i (?\<pi>\<alpha> i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
fix n m :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
fix f :: "nat \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
assume "n > m"
[PROOF STATE]
proof (state)
this:
m < n

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
hence "\<pi> (\<Sum> i \<le> m. \<delta> i (f i)) n = 0"
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = 0
[PROOF STEP]
by (induct m, simp+)
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = 0

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?m2 < ?n2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?n2 = 0

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
note \<bullet> = this
[PROOF STATE]
proof (state)
this:
?m2 < ?n2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?n2 = 0

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?m2 < ?n2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?n2 = 0

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
have "\<pi> ?\<Sigma>\<delta> n = ?\<pi>\<alpha> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
proof (cases "n \<le> ?p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
 2. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n \<le> shortest_period \<alpha>

goal (2 subgoals):
 1. n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
 2. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n \<le> shortest_period \<alpha>

goal (2 subgoals):
 1. n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
 2. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
fix n m :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
 2. \<not> n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
[PROOF STEP]
fix f :: "nat \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
 2. \<not> n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
[PROOF STEP]
assume "n \<le> m"
[PROOF STATE]
proof (state)
this:
n \<le> m

goal (2 subgoals):
 1. n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
 2. \<not> n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
[PROOF STEP]
hence "\<pi> (\<Sum> i \<le> m. \<delta> i (f i)) n = f n"
[PROOF STATE]
proof (prove)
using this:
n \<le> m

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n
[PROOF STEP]
proof (induct m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<le> 0 \<Longrightarrow> \<pi> (\<Sum>i\<le>0. \<delta> i (f i)) n = f n
 2. \<And>m. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n \<le> 0

goal (2 subgoals):
 1. n \<le> 0 \<Longrightarrow> \<pi> (\<Sum>i\<le>0. \<delta> i (f i)) n = f n
 2. \<And>m. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> 0

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>0. \<delta> i (f i)) n = f n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>0. \<delta> i (f i)) n = f n

goal (1 subgoal):
 1. \<And>m. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n
n \<le> Suc m

goal (1 subgoal):
 1. \<And>m. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n
n \<le> Suc m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n
n \<le> Suc m

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
proof (cases "n = Suc m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n = Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
 2. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n \<noteq> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = Suc m

goal (2 subgoals):
 1. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n = Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
 2. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n \<noteq> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = Suc m

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
using \<bullet>
[PROOF STATE]
proof (prove)
using this:
n = Suc m
?m2 < ?n2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?n2 = 0

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n

goal (1 subgoal):
 1. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n \<noteq> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n \<noteq> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> Suc m

goal (1 subgoal):
 1. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n \<noteq> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
hence "n \<le> m"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> Suc m

goal (1 subgoal):
 1. n \<le> m
[PROOF STEP]
using Suc.prems le_Suc_eq
[PROOF STATE]
proof (prove)
using this:
n \<noteq> Suc m
n \<le> Suc m
(?m \<le> Suc ?n) = (?m \<le> ?n \<or> ?m = Suc ?n)

goal (1 subgoal):
 1. n \<le> m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<le> m

goal (1 subgoal):
 1. \<lbrakk>n \<le> m \<Longrightarrow> \<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n; n \<le> Suc m; n \<noteq> Suc m\<rbrakk> \<Longrightarrow> \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> m

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n
[PROOF STEP]
by (simp add: Suc.hyps)
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>Suc m. \<delta> i (f i)) n = f n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>m. \<delta> i (f i)) n = f n

goal (2 subgoals):
 1. n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
 2. \<not> n__ \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n__ = \<pi> \<alpha> n__
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?na2 \<le> ?m2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?na2 = ?f2 ?na2

goal (2 subgoals):
 1. n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
 2. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?na2 \<le> ?m2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?na2 = ?f2 ?na2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?na2 \<le> ?m2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?na2 = ?f2 ?na2

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
?na2 \<le> ?m2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?na2 = ?f2 ?na2
n \<le> shortest_period \<alpha>

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n

goal (1 subgoal):
 1. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n \<le> shortest_period \<alpha>

goal (1 subgoal):
 1. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
have "?\<pi>\<alpha> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<alpha> n = 0
[PROOF STEP]
unfolding shortest_period_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<alpha> n = 0
[PROOF STEP]
using False shortest_period_bound
[PROOF STATE]
proof (prove)
using this:
\<not> n \<le> shortest_period \<alpha>
\<pi> ?\<alpha> ?i \<noteq> 0 \<Longrightarrow> ?i \<le> shortest_period ?\<alpha>

goal (1 subgoal):
 1. \<pi> \<alpha> n = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> n = 0

goal (1 subgoal):
 1. \<not> n \<le> shortest_period \<alpha> \<Longrightarrow> \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> n = 0

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
using False \<bullet>
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> n = 0
\<not> n \<le> shortest_period \<alpha>
?m2 < ?n2 \<Longrightarrow> \<pi> (\<Sum>i\<le>?m2. \<delta> i (?f2 i)) ?n2 = 0

goal (1 subgoal):
 1. \<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) n = \<pi> \<alpha> n

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) ?n2 = \<pi> \<alpha> ?n2

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i)) ?n2 = \<pi> \<alpha> ?n2

goal (1 subgoal):
 1. \<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))
[PROOF STEP]
by (metis Rep_account_inject ext)
[PROOF STATE]
proof (state)
this:
\<alpha> = (\<Sum>i\<le>shortest_period \<alpha>. \<delta> i (\<pi> \<alpha> i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bulk_update_just_cash_closed_form:
  assumes "\<rho> 0 = 0"
  shows "bulk_update_account n \<rho> i (just_cash c) =
           just_cash ((1 + i) ^ n * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bulk_update_account 0 \<rho> i (just_cash c) = just_cash ((1 + i) ^ 0 * c)
 2. \<And>n. bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. bulk_update_account 0 \<rho> i (just_cash c) = just_cash ((1 + i) ^ 0 * c)
 2. \<And>n. bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account 0 \<rho> i (just_cash c) = just_cash ((1 + i) ^ 0 * c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bulk_update_account 0 \<rho> i (just_cash c) = just_cash ((1 + i) ^ 0 * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
have "return_loans \<rho> (just_cash ((1 + i) ^ n * c)) =
          just_cash ((1 + i) ^ n * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_loans \<rho> (just_cash ((1 + i) ^ n * c)) = just_cash ((1 + i) ^ n * c)
[PROOF STEP]
using assms return_loans_just_cash
[PROOF STATE]
proof (prove)
using this:
\<rho> 0 = 0
?\<rho> 0 = 0 \<Longrightarrow> return_loans ?\<rho> (just_cash ?c) = just_cash ?c

goal (1 subgoal):
 1. return_loans \<rho> (just_cash ((1 + i) ^ n * c)) = just_cash ((1 + i) ^ n * c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
return_loans \<rho> (just_cash ((1 + i) ^ n * c)) = just_cash ((1 + i) ^ n * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
return_loans \<rho> (just_cash ((1 + i) ^ n * c)) = just_cash ((1 + i) ^ n * c)

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
using Suc net_asset_value_just_cash_left_inverse
[PROOF STATE]
proof (prove)
using this:
return_loans \<rho> (just_cash ((1 + i) ^ n * c)) = just_cash ((1 + i) ^ n * c)
bulk_update_account n \<rho> i (just_cash c) = just_cash ((1 + i) ^ n * c)
net_asset_value (just_cash ?c) = ?c

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)
[PROOF STEP]
by (simp add: update_account_def,
        metis
          add.commute
          mult.commute
          mult.left_commute
          mult_1
          ring_class.ring_distribs(2))
[PROOF STATE]
proof (state)
this:
bulk_update_account (Suc n) \<rho> i (just_cash c) = just_cash ((1 + i) ^ Suc n * c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bulk_update_loan_closed_form:
  assumes "\<rho> k \<noteq> 1"
  and "\<rho> k > 0"
  and "\<rho> 0 = 0"
  and "i \<ge> 0"
  shows "bulk_update_account n \<rho> i (\<delta> k c) =
           just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))
           + \<delta> k ((1 - \<rho> k) ^ n * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bulk_update_account 0 \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ 0 - (1 - \<rho> k) ^ 0) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ 0 * c)
 2. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. bulk_update_account 0 \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ 0 - (1 - \<rho> k) ^ 0) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ 0 * c)
 2. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account 0 \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ 0 - (1 - \<rho> k) ^ 0) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ 0 * c)
[PROOF STEP]
by (simp add: zero_account_alt_def)
[PROOF STATE]
proof (state)
this:
bulk_update_account 0 \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ 0 - (1 - \<rho> k) ^ 0) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ 0 * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
have "i + \<rho> k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < i + \<rho> k
[PROOF STEP]
using assms(2) assms(4)
[PROOF STATE]
proof (prove)
using this:
0 < \<rho> k
0 \<le> i

goal (1 subgoal):
 1. 0 < i + \<rho> k
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 < i + \<rho> k

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
hence "(i + \<rho> k) / (i + \<rho> k) = 1"
[PROOF STATE]
proof (prove)
using this:
0 < i + \<rho> k

goal (1 subgoal):
 1. (i + \<rho> k) / (i + \<rho> k) = 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(i + \<rho> k) / (i + \<rho> k) = 1

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
hence "bulk_update_account (Suc n) \<rho> i (\<delta> k c) =
            just_cash
              ((c * i) / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) +
               c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k)))
            + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)"
[PROOF STATE]
proof (prove)
using this:
(i + \<rho> k) / (i + \<rho> k) = 1

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(i + \<rho> k) / (i + \<rho> k) = 1
bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c)

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
[PROOF STEP]
by (simp add:
            return_loans_plus
            \<open>\<rho> 0 = 0\<close>
            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)
[PROOF STATE]
proof (state)
this:
bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
have
    "\<dots> =
      just_cash
        ((c * i) / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) +
         (c * i) / (i + \<rho> k) * (1 - \<rho> k) ^ n * (i + \<rho> k))
      + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i / (i + \<rho> k) * (1 - \<rho> k) ^ n * (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
[PROOF STEP]
by (metis (no_types, lifting) times_divide_eq_left times_divide_eq_right)
[PROOF STATE]
proof (state)
this:
just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i / (i + \<rho> k) * (1 - \<rho> k) ^ n * (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i * (1 - \<rho> k) ^ n * ((i + \<rho> k) / (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i / (i + \<rho> k) * (1 - \<rho> k) ^ n * (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
have
    "\<dots> =
      just_cash
        ((c * i) / (i + \<rho> k) * (
              (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n)
            + (1 - \<rho> k) ^ n * (i + \<rho> k)))
      + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i / (i + \<rho> k) * (1 - \<rho> k) ^ n * (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
[PROOF STEP]
by (metis (no_types, lifting) mult.assoc ring_class.ring_distribs(1))
[PROOF STATE]
proof (state)
this:
just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i / (i + \<rho> k) * (1 - \<rho> k) ^ n * (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
just_cash (c * i / (i + \<rho> k) * (1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + c * i / (i + \<rho> k) * (1 - \<rho> k) ^ n * (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
have
    "\<dots> =
      just_cash
        ((c * i) / (i + \<rho> k) * ((1 + i) ^ (n + 1) - (1 - \<rho> k) ^ (n + 1)))
      + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) ^ (n + 1) - (1 - \<rho> k) ^ (n + 1))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
[PROOF STEP]
by (simp add: mult.commute mult_diff_mult)
[PROOF STATE]
proof (state)
this:
just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) ^ (n + 1) - (1 - \<rho> k) ^ (n + 1))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. \<And>n. bulk_update_account n \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * c) \<Longrightarrow> bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) ^ (n + 1) - (1 - \<rho> k) ^ (n + 1))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)
just_cash (c * i / (i + \<rho> k) * ((1 + i) * ((1 + i) ^ n - (1 - \<rho> k) ^ n) + (1 - \<rho> k) ^ n * (i + \<rho> k))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c) = just_cash (c * i / (i + \<rho> k) * ((1 + i) ^ (n + 1) - (1 - \<rho> k) ^ (n + 1))) + \<delta> k ((1 - \<rho> k) ^ (n + 1) * c)

goal (1 subgoal):
 1. bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bulk_update_account (Suc n) \<rho> i (\<delta> k c) = just_cash (c * i * ((1 + i) ^ Suc n - (1 - \<rho> k) ^ Suc n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ Suc n * c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bulk_update_algebraic_closed_form:
  assumes "0 \<le> i"
  and "\<forall> n . \<rho> n < 1"
  and "\<forall> n m . n < m \<longrightarrow> \<rho> n < \<rho> m"
  and "\<rho> 0 = 0"
  shows "bulk_update_account n \<rho> i \<alpha>
           = just_cash (
                (1 + i) ^ n * (cash_reserve \<alpha>)
                + (\<Sum> k = 1..shortest_period \<alpha>.
                      (\<pi> \<alpha> k) * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n)
                         / (i + \<rho> k))
             )
             + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have "\<forall> k \<in> {1..m}. \<rho> k \<noteq> 1 \<and> \<rho> k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>{1..m}. \<rho> k \<noteq> 1 \<and> 0 < \<rho> k
[PROOF STEP]
by (metis
            assms(2)
            assms(3)
            assms(4)
            atLeastAtMost_iff
            dual_order.refl
            less_numeral_extra(1)
            linorder_not_less
            not_gr_zero)
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>{1..m}. \<rho> k \<noteq> 1 \<and> 0 < \<rho> k

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
hence \<star>: "\<forall> k \<in> {1..m}.
                 bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))
               = just_cash ((\<pi> \<alpha> k) * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n)
                               / (i + \<rho> k))
                 + \<delta> k ((1 - \<rho> k) ^ n * (\<pi> \<alpha> k))"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{1..m}. \<rho> k \<noteq> 1 \<and> 0 < \<rho> k

goal (1 subgoal):
 1. \<forall>k\<in>{1..m}. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)) = just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
using assms(1) assms(4) bulk_update_loan_closed_form
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{1..m}. \<rho> k \<noteq> 1 \<and> 0 < \<rho> k
0 \<le> i
\<rho> 0 = 0
\<lbrakk>?\<rho> ?k \<noteq> 1; 0 < ?\<rho> ?k; ?\<rho> 0 = 0; 0 \<le> ?i\<rbrakk> \<Longrightarrow> bulk_update_account ?n ?\<rho> ?i (\<delta> ?k ?c) = just_cash (?c * ?i * ((1 + ?i) ^ ?n - (1 - ?\<rho> ?k) ^ ?n) / (?i + ?\<rho> ?k)) + \<delta> ?k ((1 - ?\<rho> ?k) ^ ?n * ?c)

goal (1 subgoal):
 1. \<forall>k\<in>{1..m}. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)) = just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>{1..m}. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)) = just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have "bulk_update_account n \<rho> i (\<Sum> k \<le> m. \<delta> k (\<pi> \<alpha> k))
            = (\<Sum> k \<le> m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i (\<Sum>k\<le>m. \<delta> k (\<pi> \<alpha> k)) = (\<Sum>k\<le>m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))
[PROOF STEP]
by (induct m, simp, simp add: bulk_update_account_plus)
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<Sum>k\<le>m. \<delta> k (\<pi> \<alpha> k)) = (\<Sum>k\<le>m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<Sum>k\<le>m. \<delta> k (\<pi> \<alpha> k)) = (\<Sum>k\<le>m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have
      "\<dots> =   bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0))
            + (\<Sum> k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<le>m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0)) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))
[PROOF STEP]
by (simp add: atMost_atLeast0 sum.atLeast_Suc_atMost)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<le>m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0)) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<le>m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0)) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have
      "\<dots> =   just_cash ((1 + i) ^ n * cash_reserve \<alpha>)
            + (\<Sum> k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0)) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))
[PROOF STEP]
using
        \<open>\<rho> 0 = 0\<close>
        bulk_update_just_cash_closed_form
        loan_just_cash
        cash_reserve_def
[PROOF STATE]
proof (prove)
using this:
\<rho> 0 = 0
?\<rho> 0 = 0 \<Longrightarrow> bulk_update_account ?n ?\<rho> ?i (just_cash ?c) = just_cash ((1 + ?i) ^ ?n * ?c)
\<delta> 0 ?c = just_cash ?c
cash_reserve ?\<alpha> = \<pi> ?\<alpha> 0

goal (1 subgoal):
 1. bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0)) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0)) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<delta> 0 (\<pi> \<alpha> 0)) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have
      "\<dots> =   just_cash ((1 + i) ^ n * cash_reserve \<alpha>)
            + (\<Sum> k = 1..m.
                  just_cash ((\<pi> \<alpha> k) * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n)
                                 / (i + \<rho> k))
                  + \<delta> k ((1 - \<rho> k) ^ n * (\<pi> \<alpha> k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
using \<star>
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{1..m}. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k)) = just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)

goal (1 subgoal):
 1. just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. bulk_update_account n \<rho> i (\<delta> k (\<pi> \<alpha> k))) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have
      "\<dots> =   just_cash ((1 + i) ^ n * cash_reserve \<alpha>)
            + (\<Sum> k = 1..m.
                  just_cash ((\<pi> \<alpha> k) * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n)
                                 / (i + \<rho> k)))
            + (\<Sum> k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * (\<pi> \<alpha> k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
by (induct m, auto)
[PROOF STATE]
proof (state)
this:
just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have
      "\<dots> =   just_cash ((1 + i) ^ n * cash_reserve \<alpha>)
            + just_cash
                (\<Sum> k = 1..m.
                   (\<pi> \<alpha> k) * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))
            + (\<Sum> k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * (\<pi> \<alpha> k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + just_cash (\<Sum>k = 1..m. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
by (induct m, auto, metis (no_types, lifting) add.assoc just_cash_plus)
[PROOF STATE]
proof (state)
this:
just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + just_cash (\<Sum>k = 1..m. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bulk_update_account n \<rho> i (\<Sum>k\<le>m. \<delta> k (\<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + just_cash (\<Sum>k = 1..m. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have
      "bulk_update_account n \<rho> i (\<Sum> k \<le> m. \<delta> k (\<pi> \<alpha> k)) =
          just_cash (
              (1 + i) ^ n * cash_reserve \<alpha>
            + (\<Sum> k = 1..m.
                  (\<pi> \<alpha> k) * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)))
        + (\<Sum> k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * (\<pi> \<alpha> k)))"
[PROOF STATE]
proof (prove)
using this:
bulk_update_account n \<rho> i (\<Sum>k\<le>m. \<delta> k (\<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + (\<Sum>k = 1..m. just_cash (\<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha>) + just_cash (\<Sum>k = 1..m. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k)) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i (\<Sum>k\<le>m. \<delta> k (\<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..m. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<Sum>k\<le>m. \<delta> k (\<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..m. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..m. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<Sum>k\<le>?m2. \<delta> k (\<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..?m2. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..?m2. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
note \<bullet> = this
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i (\<Sum>k\<le>?m2. \<delta> k (\<pi> \<alpha> k)) = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..?m2. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..?m2. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
have
    "bulk_update_account n \<rho> i \<alpha>
       = bulk_update_account n \<rho> i (\<Sum> k \<le> shortest_period \<alpha>. \<delta> k (\<pi> \<alpha> k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = bulk_update_account n \<rho> i (\<Sum>k\<le>shortest_period \<alpha>. \<delta> k (\<pi> \<alpha> k))
[PROOF STEP]
using account_decomposition
[PROOF STATE]
proof (prove)
using this:
?\<alpha> = (\<Sum>i\<le>shortest_period ?\<alpha>. \<delta> i (\<pi> ?\<alpha> i))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = bulk_update_account n \<rho> i (\<Sum>k\<le>shortest_period \<alpha>. \<delta> k (\<pi> \<alpha> k))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i \<alpha> = bulk_update_account n \<rho> i (\<Sum>k\<le>shortest_period \<alpha>. \<delta> k (\<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bulk_update_account n \<rho> i \<alpha> = bulk_update_account n \<rho> i (\<Sum>k\<le>shortest_period \<alpha>. \<delta> k (\<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
unfolding \<bullet>
[PROOF STATE]
proof (prove)
using this:
bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i \<alpha> = just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>k = 1..shortest_period \<alpha>. \<pi> \<alpha> k * i * ((1 + i) ^ n - (1 - \<rho> k) ^ n) / (i + \<rho> k))) + (\<Sum>k = 1..shortest_period \<alpha>. \<delta> k ((1 - \<rho> k) ^ n * \<pi> \<alpha> k))

goal:
No subgoals!
[PROOF STEP]
qed