[STATEMENT]
lemma shortest_period_\<pi>:
  assumes "\<pi> \<alpha> i \<noteq> 0"
  shows "\<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
let ?support = "{i . \<pi> \<alpha> i \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
have A: "finite ?support"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
using finite_account_support
[PROOF STATE]
proof (prove)
using this:
finite {i. \<pi> ?\<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. finite {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
have B: "?support \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. \<pi> \<alpha> i \<noteq> 0} \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> i \<noteq> 0

goal (1 subgoal):
 1. {i. \<pi> \<alpha> i \<noteq> 0} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. \<pi> \<alpha> i \<noteq> 0} \<noteq> {}

goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
have "shortest_period \<alpha> = Max ?support"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period \<alpha> = Max {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> i \<noteq> 0

goal (1 subgoal):
 1. shortest_period \<alpha> = Max {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
unfolding shortest_period_def
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> i \<noteq> 0

goal (1 subgoal):
 1. (if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0}) = Max {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> = Max {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
have "shortest_period \<alpha> \<in> ?support"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period \<alpha> \<in> {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
unfolding \<open>shortest_period \<alpha> = Max ?support\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max {i. \<pi> \<alpha> i \<noteq> 0} \<in> {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
using Max_in [OF A B]
[PROOF STATE]
proof (prove)
using this:
Max {i. \<pi> \<alpha> i \<noteq> 0} \<in> {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. Max {i. \<pi> \<alpha> i \<noteq> 0} \<in> {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<in> {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> \<in> {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. \<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> (shortest_period \<alpha>) \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shortest_period_bound:
  assumes "\<pi> \<alpha> i \<noteq> 0"
  shows "i \<le> shortest_period \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> shortest_period \<alpha>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<le> shortest_period \<alpha>
[PROOF STEP]
let ?support = "{i . \<pi> \<alpha> i \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<le> shortest_period \<alpha>
[PROOF STEP]
have "shortest_period \<alpha> = Max ?support"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period \<alpha> = Max {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> i \<noteq> 0

goal (1 subgoal):
 1. shortest_period \<alpha> = Max {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
unfolding shortest_period_def
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> i \<noteq> 0

goal (1 subgoal):
 1. (if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0}) = Max {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> = Max {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. i \<le> shortest_period \<alpha>
[PROOF STEP]
have "shortest_period \<alpha> \<in> ?support"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period \<alpha> \<in> {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
using assms shortest_period_\<pi>
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> i \<noteq> 0
\<pi> ?\<alpha> ?i \<noteq> 0 \<Longrightarrow> \<pi> ?\<alpha> (shortest_period ?\<alpha>) \<noteq> 0

goal (1 subgoal):
 1. shortest_period \<alpha> \<in> {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<in> {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. i \<le> shortest_period \<alpha>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> \<in> {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. i \<le> shortest_period \<alpha>
[PROOF STEP]
unfolding \<open>shortest_period \<alpha> = Max ?support\<close>
[PROOF STATE]
proof (prove)
using this:
Max {i. \<pi> \<alpha> i \<noteq> 0} \<in> {i. \<pi> \<alpha> i \<noteq> 0}

goal (1 subgoal):
 1. i \<le> Max {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
by (simp add: assms finite_account_support)
[PROOF STATE]
proof (state)
this:
i \<le> shortest_period \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma net_asset_value_alt_def:
  "net_asset_value \<alpha> = (\<Sum> i \<le> shortest_period \<alpha>. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
let ?support = "{i . \<pi> \<alpha> i \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
have "(\<Sum> i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0 . \<pi> \<alpha> i) = (\<Sum> i \<le> k. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
 2. \<And>k. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k} \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
 2. \<And>k. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k} \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
proof (cases "\<pi> \<alpha> 0 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<pi> \<alpha> 0 = 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
 2. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> 0 = 0

goal (2 subgoals):
 1. \<pi> \<alpha> 0 = 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
 2. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi> \<alpha> 0 = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> 0 = 0

goal (1 subgoal):
 1. (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> 0 \<noteq> 0

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> 0 \<noteq> 0

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
have "(i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0) = (i \<le> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0) = (i \<le> 0)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> 0 \<noteq> 0

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

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?i2 \<le> 0 \<and> \<pi> \<alpha> ?i2 \<noteq> 0) = (?i2 \<le> 0)

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
hence "(\<Sum> i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) =
                 (\<Sum>i | i \<le> 0. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
using this:
(?i2 \<le> 0 \<and> \<pi> \<alpha> ?i2 \<noteq> 0) = (?i2 \<le> 0)

goal (1 subgoal):
 1. (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> 0. \<pi> \<alpha> i)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> 0. \<pi> \<alpha> i)

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> 0. \<pi> \<alpha> i)

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
have "... = (\<Sum>i \<le> 0. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}

goal (1 subgoal):
 1. \<pi> \<alpha> 0 \<noteq> 0 \<Longrightarrow> (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> 0. \<pi> \<alpha> i)
(\<Sum>i | i \<le> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> 0. \<pi> \<alpha> i)
(\<Sum>i | i \<le> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}

goal (1 subgoal):
 1. (\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> 0 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..0}

goal (1 subgoal):
 1. \<And>k. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k} \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k} \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}

goal (1 subgoal):
 1. \<And>k. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k} \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}

goal (1 subgoal):
 1. (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
proof (cases "\<pi> \<alpha> (Suc k) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> (Suc k) = 0

goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> (Suc k) = 0

goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
have "(i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0) =
                  (i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0) = (i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0)
[PROOF STEP]
using True le_Suc_eq
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> (Suc k) = 0
(?m \<le> Suc ?n) = (?m \<le> ?n \<or> ?m = Suc ?n)

goal (1 subgoal):
 1. (i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0) = (i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0) = (i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0)

goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?i2 \<le> Suc k \<and> \<pi> \<alpha> ?i2 \<noteq> 0) = (?i2 \<le> k \<and> \<pi> \<alpha> ?i2 \<noteq> 0)

goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
hence "(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) =
                 (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
using this:
(?i2 \<le> Suc k \<and> \<pi> \<alpha> ?i2 \<noteq> 0) = (?i2 \<le> k \<and> \<pi> \<alpha> ?i2 \<noteq> 0)

goal (1 subgoal):
 1. (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i)

goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i)

goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
have "... = (\<Sum> i \<le> k. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}

goal (1 subgoal):
 1. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}

goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
 2. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i)
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i)
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}

goal (1 subgoal):
 1. (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i)
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}
\<pi> \<alpha> (Suc k) = 0

goal (1 subgoal):
 1. (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
let ?A = "{i . i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
let ?A' = "{i . i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> (Suc k) \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
hence "?A = {i . (i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0) \<or> i = Suc k}"
[PROOF STATE]
proof (prove)
using this:
\<pi> \<alpha> (Suc k) \<noteq> 0

goal (1 subgoal):
 1. {i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0 \<or> i = Suc k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0 \<or> i = Suc k}

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
hence "?A = ?A' \<union> {i . i = Suc k}"
[PROOF STATE]
proof (prove)
using this:
{i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0 \<or> i = Suc k}

goal (1 subgoal):
 1. {i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {i. i = Suc k}
[PROOF STEP]
by (simp add: Collect_disj_eq)
[PROOF STATE]
proof (state)
this:
{i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {i. i = Suc k}

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
hence \<star>: "?A = ?A' \<union> {Suc k}"
[PROOF STATE]
proof (prove)
using this:
{i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {i. i = Suc k}

goal (1 subgoal):
 1. {i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
hence \<heartsuit>: "finite (?A' \<union> {Suc k})"
[PROOF STATE]
proof (prove)
using this:
{i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}

goal (1 subgoal):
 1. finite ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})
[PROOF STEP]
using finite_nat_set_iff_bounded_le
[PROOF STATE]
proof (prove)
using this:
{i. i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0} = {i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}
finite ?N = (\<exists>m. \<forall>n\<in>?N. n \<le> m)

goal (1 subgoal):
 1. finite ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
hence
          "(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) =
             (\<Sum> i \<in> ?A' \<union> {Suc k}. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
using this:
finite ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})

goal (1 subgoal):
 1. (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})
[PROOF STEP]
unfolding \<star>
[PROOF STATE]
proof (prove)
using this:
finite ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})

goal (1 subgoal):
 1. sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}) = sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
have "... = (\<Sum> i \<in> ?A'. \<pi> \<alpha> i) + (\<Sum> i \<in> {Suc k}. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k}
[PROOF STEP]
using \<heartsuit>
[PROOF STATE]
proof (prove)
using this:
finite ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k})

goal (1 subgoal):
 1. sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k}

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (\<pi> \<alpha>) ({i. i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0} \<union> {Suc k}) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k}

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
have "... = (\<Sum> i \<in> ?A'. \<pi> \<alpha> i) + \<pi> \<alpha> (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k} = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + \<pi> \<alpha> (Suc k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k} = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + \<pi> \<alpha> (Suc k)

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}; \<pi> \<alpha> (Suc k) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k}
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k} = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + \<pi> \<alpha> (Suc k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k}
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + sum (\<pi> \<alpha>) {Suc k} = (\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) + \<pi> \<alpha> (Suc k)

goal (1 subgoal):
 1. (\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}
[PROOF STEP]
by (simp add: Suc)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> Suc k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..Suc k}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> k \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..k}

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> ?k2 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..?k2}

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
hence \<dagger>:
    "(\<Sum>i | i \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) =
            (\<Sum> i \<le> shortest_period \<alpha>. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> ?k2 \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..?k2}

goal (1 subgoal):
 1. (\<Sum>i | i \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
have "(i \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> i \<noteq> 0) = (\<pi> \<alpha> i \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> i \<noteq> 0) = (\<pi> \<alpha> i \<noteq> 0)
[PROOF STEP]
using shortest_period_bound
[PROOF STATE]
proof (prove)
using this:
\<pi> ?\<alpha> ?i \<noteq> 0 \<Longrightarrow> ?i \<le> shortest_period ?\<alpha>

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

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?i2 \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> ?i2 \<noteq> 0) = (\<pi> \<alpha> ?i2 \<noteq> 0)

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
note \<bullet> = this
[PROOF STATE]
proof (state)
this:
(?i2 \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> ?i2 \<noteq> 0) = (\<pi> \<alpha> ?i2 \<noteq> 0)

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
using \<dagger>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<le> shortest_period \<alpha> \<and> \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
unfolding \<bullet> net_asset_value_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | \<pi> \<alpha> i \<noteq> 0. \<pi> \<alpha> i) = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}

goal (1 subgoal):
 1. sum (\<pi> \<alpha>) {i. \<pi> \<alpha> i \<noteq> 0} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greater_than_shortest_period_zero:
  assumes "shortest_period \<alpha> < m"
  shows "\<pi> \<alpha> m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<alpha> m = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<alpha> m = 0
[PROOF STEP]
let ?support = "{i . \<pi> \<alpha> i \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<alpha> m = 0
[PROOF STEP]
have "\<forall> i \<in> ?support . i \<le> shortest_period \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{i. \<pi> \<alpha> i \<noteq> 0}. i \<le> shortest_period \<alpha>
[PROOF STEP]
by (simp add: finite_account_support shortest_period_def)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{i. \<pi> \<alpha> i \<noteq> 0}. i \<le> shortest_period \<alpha>

goal (1 subgoal):
 1. \<pi> \<alpha> m = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>{i. \<pi> \<alpha> i \<noteq> 0}. i \<le> shortest_period \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{i. \<pi> \<alpha> i \<noteq> 0}. i \<le> shortest_period \<alpha>

goal (1 subgoal):
 1. \<pi> \<alpha> m = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{i. \<pi> \<alpha> i \<noteq> 0}. i \<le> shortest_period \<alpha>
shortest_period \<alpha> < m

goal (1 subgoal):
 1. \<pi> \<alpha> m = 0
[PROOF STEP]
by (meson CollectI leD)
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> m = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma net_asset_value_shortest_period_ge:
  assumes "shortest_period \<alpha> \<le> n"
  shows "net_asset_value \<alpha> = (\<Sum> i \<le> n. \<pi> \<alpha> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
proof (cases "shortest_period \<alpha> = n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. shortest_period \<alpha> = n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
 2. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> = n

goal (2 subgoals):
 1. shortest_period \<alpha> = n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
 2. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
shortest_period \<alpha> = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> = n

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
unfolding net_asset_value_alt_def
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> = n

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

goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<noteq> n

goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
hence "shortest_period \<alpha> < n"
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> \<noteq> n

goal (1 subgoal):
 1. shortest_period \<alpha> < n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> \<noteq> n
shortest_period \<alpha> \<le> n

goal (1 subgoal):
 1. shortest_period \<alpha> < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> < n

goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
hence "(\<Sum> i=shortest_period \<alpha> + 1.. n. \<pi> \<alpha> i) = 0"
    (is "?\<Sigma>extra = 0")
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> < n

goal (1 subgoal):
 1. sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n} = 0
[PROOF STEP]
using greater_than_shortest_period_zero
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> < n
shortest_period ?\<alpha> < ?m \<Longrightarrow> \<pi> ?\<alpha> ?m = 0

goal (1 subgoal):
 1. sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n} = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n} = 0

goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n} = 0

goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
have "(\<Sum> i \<le> n. \<pi> \<alpha> i) =
                  (\<Sum> i \<le> shortest_period \<alpha>. \<pi> \<alpha> i) + ?\<Sigma>extra"
    (is "?lhs = ?\<Sigma>shortest_period + _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (\<pi> \<alpha>) {..n} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>} + sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n}
[PROOF STEP]
by (metis
          \<open>shortest_period \<alpha> < n\<close>
          Suc_eq_plus1
          less_imp_add_positive
          sum_up_index_split)
[PROOF STATE]
proof (state)
this:
sum (\<pi> \<alpha>) {..n} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>} + sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n}

goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n} = 0
sum (\<pi> \<alpha>) {..n} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>} + sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n}
[PROOF STEP]
have "?lhs = ?\<Sigma>shortest_period"
[PROOF STATE]
proof (prove)
using this:
sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n} = 0
sum (\<pi> \<alpha>) {..n} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>} + sum (\<pi> \<alpha>) {shortest_period \<alpha> + 1..n}

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

goal (1 subgoal):
 1. shortest_period \<alpha> \<noteq> n \<Longrightarrow> net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum (\<pi> \<alpha>) {..n} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (\<pi> \<alpha>) {..n} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..n}
[PROOF STEP]
unfolding net_asset_value_alt_def
[PROOF STATE]
proof (prove)
using this:
sum (\<pi> \<alpha>) {..n} = sum (\<pi> \<alpha>) {..shortest_period \<alpha>}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strictly_solvent_net_asset_value:
  assumes "strictly_solvent \<alpha>"
  shows "0 \<le> net_asset_value \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> net_asset_value \<alpha>
[PROOF STEP]
using assms strictly_solvent_def net_asset_value_alt_def
[PROOF STATE]
proof (prove)
using this:
strictly_solvent \<alpha>
strictly_solvent ?\<alpha> \<equiv> \<forall>n. 0 \<le> sum (\<pi> ?\<alpha>) {..n}
net_asset_value ?\<alpha> = sum (\<pi> ?\<alpha>) {..shortest_period ?\<alpha>}

goal (1 subgoal):
 1. 0 \<le> net_asset_value \<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma net_asset_value_zero [simp]: "net_asset_value 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value 0 = 0
[PROOF STEP]
unfolding net_asset_value_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (\<pi> 0) {..shortest_period 0} = 0
[PROOF STEP]
using zero_account_def
[PROOF STATE]
proof (prove)
using this:
0 = \<iota> (\<lambda>_. 0)

goal (1 subgoal):
 1. sum (\<pi> 0) {..shortest_period 0} = 0
[PROOF STEP]
by force


[STATEMENT]
lemma net_asset_value_mono:
  assumes "\<alpha> \<le> \<beta>"
  shows "net_asset_value \<alpha> \<le> net_asset_value \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
let ?r = "max (shortest_period \<alpha>) (shortest_period \<beta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
have "shortest_period \<alpha> \<le> ?r" and "shortest_period \<beta> \<le> ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>) &&& shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)

goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
hence "net_asset_value \<alpha> = (\<Sum> i \<le> ?r. \<pi> \<alpha> i)"
  and "net_asset_value \<beta> = (\<Sum> i \<le> ?r. \<pi> \<beta> i)"
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} &&& net_asset_value \<beta> = sum (\<pi> \<beta>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
[PROOF STEP]
using net_asset_value_shortest_period_ge
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period ?\<alpha> \<le> ?n \<Longrightarrow> net_asset_value ?\<alpha> = sum (\<pi> ?\<alpha>) {..?n}

goal (1 subgoal):
 1. net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} &&& net_asset_value \<beta> = sum (\<pi> \<beta>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
[PROOF STEP]
by presburger+
[PROOF STATE]
proof (state)
this:
net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
net_asset_value \<beta> = sum (\<pi> \<beta>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}

goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
net_asset_value \<beta> = sum (\<pi> \<beta>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}

goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
net_asset_value \<beta> = sum (\<pi> \<beta>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
\<alpha> \<le> \<beta>

goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
unfolding less_eq_account_def
[PROOF STATE]
proof (prove)
using this:
net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
net_asset_value \<beta> = sum (\<pi> \<beta>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
\<forall>n. sum (\<pi> \<alpha>) {..n} \<le> sum (\<pi> \<beta>) {..n}

goal (1 subgoal):
 1. net_asset_value \<alpha> \<le> net_asset_value \<beta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
net_asset_value \<alpha> \<le> net_asset_value \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma net_asset_value_uminus: "net_asset_value (- \<alpha>) = - net_asset_value \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value (- \<alpha>) = - net_asset_value \<alpha>
[PROOF STEP]
unfolding
    net_asset_value_alt_def
    shortest_period_uminus
    Rep_account_uminus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n\<le>shortest_period \<alpha>. - \<pi> \<alpha> n) = - sum (\<pi> \<alpha>) {..shortest_period \<alpha>}
[PROOF STEP]
by (simp add: sum_negf)


[STATEMENT]
lemma net_asset_value_plus:
  "net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>"
  (is "?lhs = ?\<Sigma>\<alpha> + ?\<Sigma>\<beta>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
let ?r = "max (shortest_period \<alpha>) (shortest_period \<beta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
have  A: "shortest_period (\<alpha> + \<beta>) \<le> ?r"
    and B: "shortest_period \<alpha> \<le> ?r"
    and C: "shortest_period \<beta> \<le> ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>) &&& shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>) &&& shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
using shortest_period_plus
[PROOF STATE]
proof (prove)
using this:
shortest_period (?\<alpha> + ?\<beta>) \<le> max (shortest_period ?\<alpha>) (shortest_period ?\<beta>)

goal (1 subgoal):
 1. shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>) &&& shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>) &&& shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
by presburger+
[PROOF STATE]
proof (state)
this:
shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)

goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
have "?lhs = (\<Sum> i \<le> ?r. \<pi> (\<alpha> + \<beta>) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
[PROOF STEP]
using net_asset_value_shortest_period_ge [OF A]
[PROOF STATE]
proof (prove)
using this:
net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}

goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}

goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}

goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
have "\<dots> = (\<Sum> i \<le> ?r. \<pi> \<alpha> i + \<pi> \<beta> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} = (\<Sum>i\<le>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i + \<pi> \<beta> i)
[PROOF STEP]
using Rep_account_plus
[PROOF STATE]
proof (prove)
using this:
\<pi> (?\<alpha>\<^sub>1 + ?\<alpha>\<^sub>2) = (\<lambda>n. \<pi> ?\<alpha>\<^sub>1 n + \<pi> ?\<alpha>\<^sub>2 n)

goal (1 subgoal):
 1. sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} = (\<Sum>i\<le>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i + \<pi> \<beta> i)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} = (\<Sum>i\<le>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i + \<pi> \<beta> i)

goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} = (\<Sum>i\<le>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i + \<pi> \<beta> i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} = (\<Sum>i\<le>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i + \<pi> \<beta> i)

goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
using
      net_asset_value_shortest_period_ge [OF B]
      net_asset_value_shortest_period_ge [OF C]
[PROOF STATE]
proof (prove)
using this:
net_asset_value (\<alpha> + \<beta>) = sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
sum (\<pi> (\<alpha> + \<beta>)) {..max (shortest_period \<alpha>) (shortest_period \<beta>)} = (\<Sum>i\<le>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i + \<pi> \<beta> i)
net_asset_value \<alpha> = sum (\<pi> \<alpha>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}
net_asset_value \<beta> = sum (\<pi> \<beta>) {..max (shortest_period \<alpha>) (shortest_period \<beta>)}

goal (1 subgoal):
 1. net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>
[PROOF STEP]
by (simp add: sum.distrib)
[PROOF STATE]
proof (state)
this:
net_asset_value (\<alpha> + \<beta>) = net_asset_value \<alpha> + net_asset_value \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma net_asset_value_minus:
  "net_asset_value (\<alpha> - \<beta>) = net_asset_value \<alpha> - net_asset_value \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value (\<alpha> - \<beta>) = net_asset_value \<alpha> - net_asset_value \<beta>
[PROOF STEP]
using additive.diff additive.intro net_asset_value_plus
[PROOF STATE]
proof (prove)
using this:
additive ?f \<Longrightarrow> ?f (?x - ?y) = ?f ?x - ?f ?y
(\<And>x y. ?f (x + y) = ?f x + ?f y) \<Longrightarrow> additive ?f
net_asset_value (?\<alpha> + ?\<beta>) = net_asset_value ?\<alpha> + net_asset_value ?\<beta>

goal (1 subgoal):
 1. net_asset_value (\<alpha> - \<beta>) = net_asset_value \<alpha> - net_asset_value \<beta>
[PROOF STEP]
by blast


[STATEMENT]
lemma net_asset_value_just_cash_left_inverse:
  "net_asset_value (just_cash c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. net_asset_value (just_cash c) = c
[PROOF STEP]
using net_asset_value_alt_def partial_nav_just_cash
[PROOF STATE]
proof (prove)
using this:
net_asset_value ?\<alpha> = sum (\<pi> ?\<alpha>) {..shortest_period ?\<alpha>}
sum (\<pi> (just_cash ?a)) {..?n} = ?a

goal (1 subgoal):
 1. net_asset_value (just_cash c) = c
[PROOF STEP]
by presburger


[STATEMENT]
lemma (in finite) total_interest_transfer:
  "total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i"
  (is "total_interest ?\<L>' i = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
proof (cases "a = b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
 2. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. a = b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
 2. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
unfolding \<open>a = b\<close> transfer_collapse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_interest \<L> i = total_interest \<L> i
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "total_interest ?\<L>' i = (\<Sum> a \<in> UNIV . i * net_asset_value (?\<L>' a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_interest (transfer \<L> \<tau> a b) i = (\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa))
[PROOF STEP]
unfolding total_interest_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
total_interest (transfer \<L> \<tau> a b) i = (\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa))

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
total_interest (transfer \<L> \<tau> a b) i = (\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa))

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "\<dots> = (\<Sum> a \<in> UNIV - {a, b} \<union> {a,b}. i * net_asset_value (?\<L>' a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa))
[PROOF STEP]
by (metis Un_Diff_cancel2 Un_UNIV_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa))

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa))

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "\<dots> = (\<Sum> a \<in> UNIV - {a, b}. i * net_asset_value (?\<L>' a)) +
                   i * net_asset_value (?\<L>' a) + i * net_asset_value (?\<L>' b)"
    (is "_ = ?\<Sigma> + _ + _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (transfer \<L> \<tau> a b a) + i * net_asset_value (transfer \<L> \<tau> a b b)
[PROOF STEP]
using \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (transfer \<L> \<tau> a b a) + i * net_asset_value (transfer \<L> \<tau> a b b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (transfer \<L> \<tau> a b a) + i * net_asset_value (transfer \<L> \<tau> a b b)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (transfer \<L> \<tau> a b a) + i * net_asset_value (transfer \<L> \<tau> a b b)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "\<dots> = ?\<Sigma> +
                    i * net_asset_value (\<L> a - \<tau>) +
                    i * net_asset_value (\<L> b + \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (transfer \<L> \<tau> a b a) + i * net_asset_value (transfer \<L> \<tau> a b b) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>)
[PROOF STEP]
unfolding transfer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (if a = b then \<L> aa else if aa = a then \<L> a - \<tau> else if aa = b then \<L> b + \<tau> else \<L> aa)) + i * net_asset_value (if a = b then \<L> a else if a = a then \<L> a - \<tau> else if a = b then \<L> b + \<tau> else \<L> a) + i * net_asset_value (if a = b then \<L> b else if b = a then \<L> a - \<tau> else if b = b then \<L> b + \<tau> else \<L> b) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (if a = b then \<L> aa else if aa = a then \<L> a - \<tau> else if aa = b then \<L> b + \<tau> else \<L> aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>)
[PROOF STEP]
using \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (if a = b then \<L> aa else if aa = a then \<L> a - \<tau> else if aa = b then \<L> b + \<tau> else \<L> aa)) + i * net_asset_value (if a = b then \<L> a else if a = a then \<L> a - \<tau> else if a = b then \<L> b + \<tau> else \<L> a) + i * net_asset_value (if a = b then \<L> b else if b = a then \<L> a - \<tau> else if b = b then \<L> b + \<tau> else \<L> b) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (if a = b then \<L> aa else if aa = a then \<L> a - \<tau> else if aa = b then \<L> b + \<tau> else \<L> aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (transfer \<L> \<tau> a b a) + i * net_asset_value (transfer \<L> \<tau> a b b) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (transfer \<L> \<tau> a b a) + i * net_asset_value (transfer \<L> \<tau> a b b) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "\<dots> = ?\<Sigma> +
                  i * net_asset_value (\<L> a) +
                  i * net_asset_value (- \<tau>) +
                  i * net_asset_value (\<L> b) +
                  i * net_asset_value \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (- \<tau>) + i * net_asset_value (\<L> b) + i * net_asset_value \<tau>
[PROOF STEP]
unfolding minus_account_def net_asset_value_plus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * (net_asset_value (\<L> a) + net_asset_value (- \<tau>)) + i * (net_asset_value (\<L> b) + net_asset_value \<tau>) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (- \<tau>) + i * net_asset_value (\<L> b) + i * net_asset_value \<tau>
[PROOF STEP]
by (simp add: distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (- \<tau>) + i * net_asset_value (\<L> b) + i * net_asset_value \<tau>

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a - \<tau>) + i * net_asset_value (\<L> b + \<tau>) = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (- \<tau>) + i * net_asset_value (\<L> b) + i * net_asset_value \<tau>

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "\<dots> = ?\<Sigma> +
                  i * net_asset_value (\<L> a) +
                  i * net_asset_value (\<L> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (- \<tau>) + i * net_asset_value (\<L> b) + i * net_asset_value \<tau> = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
[PROOF STEP]
unfolding net_asset_value_uminus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * - net_asset_value \<tau> + i * net_asset_value (\<L> b) + i * net_asset_value \<tau> = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (- \<tau>) + i * net_asset_value (\<L> b) + i * net_asset_value \<tau> = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (- \<tau>) + i * net_asset_value (\<L> b) + i * net_asset_value \<tau> = (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "\<dots> = (\<Sum> a \<in> UNIV - {a, b}. i * net_asset_value (\<L> a)) +
                  i * net_asset_value (\<L> a) +
                  i * net_asset_value (\<L> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
[PROOF STEP]
unfolding transfer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (if a = b then \<L> aa else if aa = a then \<L> a - \<tau> else if aa = b then \<L> b + \<tau> else \<L> aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
[PROOF STEP]
using \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (if a = b then \<L> aa else if aa = a then \<L> a - \<tau> else if aa = b then \<L> b + \<tau> else \<L> aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>aa\<in>UNIV - {a, b}. i * net_asset_value (transfer \<L> \<tau> a b aa)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
have "\<dots> = (\<Sum> a \<in> UNIV - {a, b} \<union> {a,b}. i * net_asset_value (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (\<L> a))
[PROOF STEP]
using \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (\<L> a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (\<L> a))

goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
total_interest (transfer \<L> \<tau> a b) i = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
(\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (\<L> a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
total_interest (transfer \<L> \<tau> a b) i = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
(\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (\<L> a))

goal (1 subgoal):
 1. total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i
[PROOF STEP]
unfolding total_interest_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b)
(\<Sum>a\<in>UNIV - {a, b}. i * net_asset_value (\<L> a)) + i * net_asset_value (\<L> a) + i * net_asset_value (\<L> b) = (\<Sum>a\<in>UNIV - {a, b} \<union> {a, b}. i * net_asset_value (\<L> a))

goal (1 subgoal):
 1. (\<Sum>aa\<in>UNIV. i * net_asset_value (transfer \<L> \<tau> a b aa)) = (\<Sum>a\<in>UNIV. i * net_asset_value (\<L> a))
[PROOF STEP]
by (metis Diff_partition Un_commute top_greatest)
[PROOF STATE]
proof (state)
this:
total_interest (transfer \<L> \<tau> a b) i = total_interest \<L> i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Rep_account_return_loans [simp]:
  "\<pi> (return_loans \<rho> \<alpha>) = (\<lambda> n . (1 - \<rho> n) * \<pi> \<alpha> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
have "(support 0 UNIV (\<lambda> n . (1 - \<rho> n) * \<pi> \<alpha> n)) \<subseteq>
          (support 0 UNIV (\<pi> \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
[PROOF STEP]
unfolding support_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> UNIV. (1 - \<rho> x) * \<pi> \<alpha> x \<noteq> 0} \<subseteq> {x \<in> UNIV. \<pi> \<alpha> x \<noteq> 0}
[PROOF STEP]
by (simp add: Collect_mono)
[PROOF STATE]
proof (state)
this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
have "finite (support 0 UNIV (\<pi> \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (support 0 UNIV (\<pi> \<alpha>))
[PROOF STEP]
using Rep_account
[PROOF STATE]
proof (prove)
using this:
\<pi> ?x \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. finite (support 0 UNIV (\<pi> \<alpha>))
[PROOF STEP]
unfolding fin_support_def
[PROOF STATE]
proof (prove)
using this:
\<pi> ?x \<in> {f. finite (support 0 UNIV f)}

goal (1 subgoal):
 1. finite (support 0 UNIV (\<pi> \<alpha>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (support 0 UNIV (\<pi> \<alpha>))

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
finite (support 0 UNIV (\<pi> \<alpha>))
[PROOF STEP]
have "finite (support 0 UNIV (\<lambda> n . (1 - \<rho> n) * \<pi> \<alpha> n))"
[PROOF STATE]
proof (prove)
using this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
finite (support 0 UNIV (\<pi> \<alpha>))

goal (1 subgoal):
 1. finite (support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n))
[PROOF STEP]
using infinite_super
[PROOF STATE]
proof (prove)
using this:
support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<subseteq> support 0 UNIV (\<pi> \<alpha>)
finite (support 0 UNIV (\<pi> \<alpha>))
\<lbrakk>?S \<subseteq> ?T; infinite ?S\<rbrakk> \<Longrightarrow> infinite ?T

goal (1 subgoal):
 1. finite (support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n))

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
hence "(\<lambda> n . (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
using this:
finite (support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n))

goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV
[PROOF STEP]
unfolding fin_support_def
[PROOF STATE]
proof (prove)
using this:
finite (support 0 UNIV (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n))

goal (1 subgoal):
 1. (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> {f. finite (support 0 UNIV f)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
using
      Rep_account
      Abs_account_inject
      Rep_account_inverse
      return_loans_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n) \<in> fin_support 0 UNIV
\<pi> ?x \<in> fin_support 0 UNIV
\<lbrakk>?x \<in> fin_support 0 UNIV; ?y \<in> fin_support 0 UNIV\<rbrakk> \<Longrightarrow> (\<iota> ?x = \<iota> ?y) = (?x = ?y)
\<iota> (\<pi> ?x) = ?x
return_loans ?\<rho> ?\<alpha> = \<iota> (\<lambda>n. (1 - ?\<rho> n) * \<pi> ?\<alpha> n)

goal (1 subgoal):
 1. \<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (return_loans \<rho> \<alpha>) = (\<lambda>n. (1 - \<rho> n) * \<pi> \<alpha> n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in finite) shortest_ledger_period_bound:
  fixes \<L> :: "'a ledger"
  shows "shortest_period (\<L> a) \<le> shortest_ledger_period \<L>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
fix \<alpha> :: account
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
fix S :: "account set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
assume "finite S" and "\<alpha> \<in> S"
[PROOF STATE]
proof (state)
this:
finite S
\<alpha> \<in> S

goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
hence "shortest_period \<alpha> \<le> Max (shortest_period ` S)"
[PROOF STATE]
proof (prove)
using this:
finite S
\<alpha> \<in> S

goal (1 subgoal):
 1. shortest_period \<alpha> \<le> Max (shortest_period ` S)
[PROOF STEP]
proof (induct S rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<alpha> \<in> {} \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` {})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<alpha> \<in> F \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` F); \<alpha> \<in> insert x F\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
\<alpha> \<in> {}

goal (2 subgoals):
 1. \<alpha> \<in> {} \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` {})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<alpha> \<in> F \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` F); \<alpha> \<in> insert x F\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in> {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> {}

goal (1 subgoal):
 1. shortest_period \<alpha> \<le> Max (shortest_period ` {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> Max (shortest_period ` {})

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<alpha> \<in> F \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` F); \<alpha> \<in> insert x F\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<alpha> \<in> F \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` F); \<alpha> \<in> insert x F\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert x F)
[PROOF STEP]
case (insert \<beta> S)
[PROOF STATE]
proof (state)
this:
finite S
\<beta> \<notin> S
\<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S)
\<alpha> \<in> insert \<beta> S

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<alpha> \<in> F \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` F); \<alpha> \<in> insert x F\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite S
\<beta> \<notin> S
\<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S)
\<alpha> \<in> insert \<beta> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite S
\<beta> \<notin> S
\<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S)
\<alpha> \<in> insert \<beta> S

goal (1 subgoal):
 1. shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
proof (cases "\<alpha> = \<beta>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> = \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
 2. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> \<noteq> \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<alpha> = \<beta>

goal (2 subgoals):
 1. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> = \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
 2. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> \<noteq> \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> = \<beta>

goal (1 subgoal):
 1. shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
by (simp add: insert.hyps(1))
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)

goal (1 subgoal):
 1. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> \<noteq> \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> \<noteq> \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<alpha> \<noteq> \<beta>

goal (1 subgoal):
 1. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> \<noteq> \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
hence "\<alpha> \<in> S"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<noteq> \<beta>

goal (1 subgoal):
 1. \<alpha> \<in> S
[PROOF STEP]
using insert.prems
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<noteq> \<beta>
\<alpha> \<in> insert \<beta> S

goal (1 subgoal):
 1. \<alpha> \<in> S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<alpha> \<in> S

goal (1 subgoal):
 1. \<lbrakk>finite S; \<beta> \<notin> S; \<alpha> \<in> S \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` S); \<alpha> \<in> insert \<beta> S; \<alpha> \<noteq> \<beta>\<rbrakk> \<Longrightarrow> shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> S

goal (1 subgoal):
 1. shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)
[PROOF STEP]
by (meson
                Max_ge
                finite_imageI
                finite_insert
                imageI
                insert.hyps(1)
                insert.prems)
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> Max (shortest_period ` insert \<beta> S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> Max (shortest_period ` S)

goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?S2; ?\<alpha>2 \<in> ?S2\<rbrakk> \<Longrightarrow> shortest_period ?\<alpha>2 \<le> Max (shortest_period ` ?S2)

goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?S2; ?\<alpha>2 \<in> ?S2\<rbrakk> \<Longrightarrow> shortest_period ?\<alpha>2 \<le> Max (shortest_period ` ?S2)

goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
have "finite (range \<L>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (range \<L>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite (range \<L>)

goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite ?S2; ?\<alpha>2 \<in> ?S2\<rbrakk> \<Longrightarrow> shortest_period ?\<alpha>2 \<le> Max (shortest_period ` ?S2)
finite (range \<L>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?S2; ?\<alpha>2 \<in> ?S2\<rbrakk> \<Longrightarrow> shortest_period ?\<alpha>2 \<le> Max (shortest_period ` ?S2)
finite (range \<L>)

goal (1 subgoal):
 1. shortest_period (\<L> a) \<le> shortest_ledger_period \<L>
[PROOF STEP]
by (simp add: shortest_ledger_period_def)
[PROOF STATE]
proof (state)
this:
shortest_period (\<L> a) \<le> shortest_ledger_period \<L>

goal:
No subgoals!
[PROOF STEP]
qed