[STATEMENT]
theorem bulk_update_closed_form:
  assumes "0 \<le> i"
  and "\<forall> n . \<rho> n < 1"
  and "\<forall> n m . n < m \<longrightarrow> \<rho> n < \<rho> m"
  and "\<rho> 0 = 0"
  shows "bulk_update_account n \<rho> i \<alpha>
           = \<iota> ( \<lambda> k .
                if k = 0 then
                  (1 + i) ^ n * (cash_reserve \<alpha>)
                  + (\<Sum> j = 1..shortest_period \<alpha>.
                        (\<pi> \<alpha> j) * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n)
                           / (i + \<rho> j))
                else
                  (1 - \<rho> k) ^ n * \<pi> \<alpha> k
               )"
  (is "_ = \<iota> ?\<nu>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
obtain \<nu> where X: "\<nu> = ?\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<nu>. \<nu> = (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<nu> = (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nu> = (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
obtain \<nu>' where Y:
    "\<nu>' = \<pi> ( just_cash (
                (1 + i) ^ n * (cash_reserve \<alpha>)
                + (\<Sum> j = 1..shortest_period \<alpha>.
                      (\<pi> \<alpha> j) * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n)
                         / (i + \<rho> j))
              )
              + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<nu>'. \<nu>' = \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<nu>' = \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nu>' = \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<nu>' = \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
have "\<forall> k > shortest_period \<alpha> . \<nu> k = \<nu>' k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k>shortest_period \<alpha>. \<nu> k = \<nu>' k
[PROOF STEP]
proof (rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. shortest_period \<alpha> < k \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. shortest_period \<alpha> < k \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
assume "shortest_period \<alpha> < k"
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> < k

goal (1 subgoal):
 1. \<And>k. shortest_period \<alpha> < k \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
hence "\<nu> k = 0"
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> < k

goal (1 subgoal):
 1. \<nu> k = 0
[PROOF STEP]
unfolding X
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> < k

goal (1 subgoal):
 1. (if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k) = 0
[PROOF STEP]
by (simp add: greater_than_shortest_period_zero)
[PROOF STATE]
proof (state)
this:
\<nu> k = 0

goal (1 subgoal):
 1. \<And>k. shortest_period \<alpha> < k \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nu> k = 0

goal (1 subgoal):
 1. \<And>k. shortest_period \<alpha> < k \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
have "\<nu>' k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>' k = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nu>' k = 0
[PROOF STEP]
have "\<forall> c. \<pi> (just_cash c) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. \<pi> (just_cash c) k = 0
[PROOF STEP]
using
            Rep_account_just_cash
            \<open>shortest_period \<alpha> < k\<close>
            just_cash_def
[PROOF STATE]
proof (prove)
using this:
\<pi> (just_cash ?c) = (\<lambda>n. if n = 0 then ?c else 0)
shortest_period \<alpha> < k
just_cash ?c = \<iota> (\<lambda>n. if n = 0 then ?c else 0)

goal (1 subgoal):
 1. \<forall>c. \<pi> (just_cash c) k = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>c. \<pi> (just_cash c) k = 0

goal (1 subgoal):
 1. \<nu>' k = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>c. \<pi> (just_cash c) k = 0

goal (1 subgoal):
 1. \<nu>' k = 0
[PROOF STEP]
have "\<forall> m < k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m<k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
proof (rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m < k \<Longrightarrow> \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m < k \<Longrightarrow> \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
assume "m < k"
[PROOF STATE]
proof (state)
this:
m < k

goal (1 subgoal):
 1. \<And>m. m < k \<Longrightarrow> \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
let ?\<pi>\<Sigma>\<delta> = "\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m < k \<Longrightarrow> \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
have "?\<pi>\<Sigma>\<delta> k = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)
[PROOF STEP]
by (induct m, auto)
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)

goal (1 subgoal):
 1. \<And>m. m < k \<Longrightarrow> \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)

goal (1 subgoal):
 1. \<And>m. m < k \<Longrightarrow> \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
have "\<dots> = (\<Sum>j = 1..m. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (\<Sum>j = 1..m. 0)
[PROOF STEP]
using \<open>m < k\<close>
[PROOF STATE]
proof (prove)
using this:
m < k

goal (1 subgoal):
 1. (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (\<Sum>j = 1..m. 0)
[PROOF STEP]
by (induct m, simp+)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (\<Sum>j = 1..m. 0)

goal (1 subgoal):
 1. \<And>m. m < k \<Longrightarrow> \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. 0)
[PROOF STEP]
show "?\<pi>\<Sigma>\<delta> k = 0"
[PROOF STATE]
proof (prove)
using this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. 0)

goal (1 subgoal):
 1. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m<k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0

goal (1 subgoal):
 1. \<nu>' k = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m<k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m<k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0

goal (1 subgoal):
 1. \<nu>' k = 0
[PROOF STEP]
unfolding Y
[PROOF STATE]
proof (prove)
using this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m<k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0

goal (1 subgoal):
 1. \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j))) k = 0
[PROOF STEP]
using \<open>shortest_period \<alpha> < k\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m<k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = 0
shortest_period \<alpha> < k

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nu>' k = 0

goal (1 subgoal):
 1. \<And>k. shortest_period \<alpha> < k \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nu> k = 0
\<nu>' k = 0
[PROOF STEP]
show "\<nu> k = \<nu>' k"
[PROOF STATE]
proof (prove)
using this:
\<nu> k = 0
\<nu>' k = 0

goal (1 subgoal):
 1. \<nu> k = \<nu>' k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nu> k = \<nu>' k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k>shortest_period \<alpha>. \<nu> k = \<nu>' k

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k>shortest_period \<alpha>. \<nu> k = \<nu>' k

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
have "\<forall> k . 0 < k \<longrightarrow> k \<le> shortest_period \<alpha> \<longrightarrow> \<nu> k = \<nu>' k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k>0. k \<le> shortest_period \<alpha> \<longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
proof (rule allI, (rule impI)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < k; k \<le> shortest_period \<alpha>\<rbrakk> \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < k; k \<le> shortest_period \<alpha>\<rbrakk> \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
assume "0 < k"
      and "k \<le> shortest_period \<alpha>"
[PROOF STATE]
proof (state)
this:
0 < k
k \<le> shortest_period \<alpha>

goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < k; k \<le> shortest_period \<alpha>\<rbrakk> \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
have "\<nu> k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
unfolding X
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
using \<open>0 < k\<close>
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. (if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<nu> k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < k; k \<le> shortest_period \<alpha>\<rbrakk> \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nu> k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < k; k \<le> shortest_period \<alpha>\<rbrakk> \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
have "\<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
have "\<forall> c. \<pi> (just_cash c) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. \<pi> (just_cash c) k = 0
[PROOF STEP]
using \<open>0 < k\<close>
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. \<forall>c. \<pi> (just_cash c) k = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>c. \<pi> (just_cash c) k = 0

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>c. \<pi> (just_cash c) k = 0

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>c. \<pi> (just_cash c) k = 0

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
assume "k \<le> m"
[PROOF STATE]
proof (state)
this:
k \<le> m

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
have "  \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k
                = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)
[PROOF STEP]
by (induct m, auto)
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
have "\<dots> = (1 - \<rho> k) ^ n * \<pi> \<alpha> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
using \<open>0 < k\<close> \<open>k \<le> m\<close>
[PROOF STATE]
proof (prove)
using this:
0 < k
k \<le> m

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

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

goal (1 subgoal):
 1. (\<Sum>j = 1..0. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..0. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<And>m. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
0 < k
k \<le> Suc m

goal (1 subgoal):
 1. \<And>m. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
0 < k
k \<le> Suc m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
0 < k
k \<le> Suc m

goal (1 subgoal):
 1. (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
proof (cases "k = Suc m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k = Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
 2. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = Suc m

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k = Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
 2. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
hence "k > m"
[PROOF STATE]
proof (prove)
using this:
k = Suc m

goal (1 subgoal):
 1. m < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m < k

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k = Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
 2. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
hence "(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = 0"
[PROOF STATE]
proof (prove)
using this:
m < k

goal (1 subgoal):
 1. (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = 0
[PROOF STEP]
by (induct m, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = 0

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k = Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
 2. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = 0

goal (1 subgoal):
 1. (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
using \<open>k > m\<close> \<open>k = Suc m\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = 0
m < k
k = Suc m

goal (1 subgoal):
 1. (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> Suc m

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
hence "(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k)
                       = (1 - \<rho> k) ^ n * \<pi> \<alpha> k"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> Suc m

goal (1 subgoal):
 1. (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
using Suc.hyps Suc.prems(1) Suc.prems(2) le_Suc_eq
[PROOF STATE]
proof (prove)
using this:
k \<noteq> Suc m
\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
0 < k
k \<le> Suc m
(?m \<le> Suc ?n) = (?m \<le> ?n \<or> ?m = Suc ?n)

goal (1 subgoal):
 1. (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
have "k \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> m
[PROOF STEP]
using False Suc.prems(2) le_Suc_eq
[PROOF STATE]
proof (prove)
using this:
k \<noteq> Suc m
k \<le> Suc m
(?m \<le> Suc ?n) = (?m \<le> ?n \<or> ?m = Suc ?n)

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k; 0 < k; k \<le> Suc m; k \<noteq> Suc m\<rbrakk> \<Longrightarrow> (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
k \<le> m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
k \<le> m

goal (1 subgoal):
 1. (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
using \<open>0 < k\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
k \<le> m
0 < k

goal (1 subgoal):
 1. (\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..Suc m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..m. \<pi> (\<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k) = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
have
            "\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k
                 = (1 - \<rho> k) ^ n * \<pi> \<alpha> k"
[PROOF STATE]
proof (prove)
using this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
k \<le> ?m2 \<Longrightarrow> \<pi> (\<Sum>j = 1..?m2. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
hence
          "\<forall> m \<ge> k.
              \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k
            = (1 - \<rho> k) ^ n * \<pi> \<alpha> k"
[PROOF STATE]
proof (prove)
using this:
k \<le> ?m2 \<Longrightarrow> \<pi> (\<Sum>j = 1..?m2. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<forall>m\<ge>k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m\<ge>k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m\<ge>k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
unfolding Y
[PROOF STATE]
proof (prove)
using this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m\<ge>k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j))) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
using \<open>k \<le> shortest_period \<alpha>\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>c. \<pi> (just_cash c) k = 0
\<forall>m\<ge>k. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
k \<le> shortest_period \<alpha>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < k; k \<le> shortest_period \<alpha>\<rbrakk> \<Longrightarrow> \<nu> k = \<nu>' k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nu> k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
\<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
[PROOF STEP]
show "\<nu> k = \<nu>' k"
[PROOF STATE]
proof (prove)
using this:
\<nu> k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k
\<nu>' k = (1 - \<rho> k) ^ n * \<pi> \<alpha> k

goal (1 subgoal):
 1. \<nu> k = \<nu>' k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<nu> k = \<nu>' k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k>0. k \<le> shortest_period \<alpha> \<longrightarrow> \<nu> k = \<nu>' k

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k>0. k \<le> shortest_period \<alpha> \<longrightarrow> \<nu> k = \<nu>' k

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
have "\<nu> 0 = \<nu>' 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> 0 = \<nu>' 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nu> 0 = \<nu>' 0
[PROOF STEP]
have "\<nu> 0 = (1 + i) ^ n * (cash_reserve \<alpha>)
                  + (\<Sum> j = 1..shortest_period \<alpha>.
                        (\<pi> \<alpha> j) * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n)
                           / (i + \<rho> j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
\<nu> = (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)

goal (1 subgoal):
 1. \<nu> 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<nu> 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))

goal (1 subgoal):
 1. \<nu> 0 = \<nu>' 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nu> 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))

goal (1 subgoal):
 1. \<nu> 0 = \<nu>' 0
[PROOF STEP]
have "\<nu>' 0 = (1 + i) ^ n * (cash_reserve \<alpha>)
                   + (\<Sum> j = 1..shortest_period \<alpha>.
                         (\<pi> \<alpha> j) * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n)
                            / (i + \<rho> j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
have "\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) 0 = 0
[PROOF STEP]
by (induct m, simp+)
[PROOF STATE]
proof (state)
this:
\<pi> (\<Sum>j = 1..m. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) 0 = 0

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

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

goal (1 subgoal):
 1. \<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
unfolding Y
[PROOF STATE]
proof (prove)
using this:
\<pi> (\<Sum>j = 1..?m2. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)) 0 = 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))

goal (1 subgoal):
 1. \<nu> 0 = \<nu>' 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nu> 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
\<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nu> 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))
\<nu>' 0 = (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))

goal (1 subgoal):
 1. \<nu> 0 = \<nu>' 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nu> 0 = \<nu>' 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nu> 0 = \<nu>' 0

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>k>shortest_period \<alpha>. \<nu> k = \<nu>' k
\<forall>k>0. k \<le> shortest_period \<alpha> \<longrightarrow> \<nu> k = \<nu>' k
\<nu> 0 = \<nu>' 0
[PROOF STEP]
have "\<nu> k = \<nu>' k"
[PROOF STATE]
proof (prove)
using this:
\<forall>k>shortest_period \<alpha>. \<nu> k = \<nu>' k
\<forall>k>0. k \<le> shortest_period \<alpha> \<longrightarrow> \<nu> k = \<nu>' k
\<nu> 0 = \<nu>' 0

goal (1 subgoal):
 1. \<nu> k = \<nu>' k
[PROOF STEP]
by (metis linorder_not_less not_gr0)
[PROOF STATE]
proof (state)
this:
\<nu> k = \<nu>' k

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<nu> ?k2 = \<nu>' ?k2

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
hence "\<iota> \<nu> = \<iota> \<nu>'"
[PROOF STATE]
proof (prove)
using this:
\<nu> ?k2 = \<nu>' ?k2

goal (1 subgoal):
 1. \<iota> \<nu> = \<iota> \<nu>'
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<iota> \<nu> = \<iota> \<nu>'

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nu> = (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
\<nu>' = \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)))
\<iota> \<nu> = \<iota> \<nu>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nu> = (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
\<nu>' = \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)))
\<iota> \<nu> = \<iota> \<nu>'

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
using
      Rep_account_inverse
      assms
      bulk_update_algebraic_closed_form
[PROOF STATE]
proof (prove)
using this:
\<nu> = (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
\<nu>' = \<pi> (just_cash ((1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j))) + (\<Sum>j = 1..shortest_period \<alpha>. \<delta> j ((1 - \<rho> j) ^ n * \<pi> \<alpha> j)))
\<iota> \<nu> = \<iota> \<nu>'
\<iota> (\<pi> ?x) = ?x
0 \<le> i
\<forall>n. \<rho> n < 1
\<forall>n m. n < m \<longrightarrow> \<rho> n < \<rho> m
\<rho> 0 = 0
\<lbrakk>0 \<le> ?i; \<forall>n. ?\<rho> n < 1; \<forall>n m. n < m \<longrightarrow> ?\<rho> n < ?\<rho> m; ?\<rho> 0 = 0\<rbrakk> \<Longrightarrow> bulk_update_account ?n ?\<rho> ?i ?\<alpha> = just_cash ((1 + ?i) ^ ?n * cash_reserve ?\<alpha> + (\<Sum>k = 1..shortest_period ?\<alpha>. \<pi> ?\<alpha> k * ?i * ((1 + ?i) ^ ?n - (1 - ?\<rho> k) ^ ?n) / (?i + ?\<rho> k))) + (\<Sum>k = 1..shortest_period ?\<alpha>. \<delta> k ((1 - ?\<rho> k) ^ ?n * \<pi> ?\<alpha> k))

goal (1 subgoal):
 1. bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
bulk_update_account n \<rho> i \<alpha> = \<iota> (\<lambda>k. if k = 0 then (1 + i) ^ n * cash_reserve \<alpha> + (\<Sum>j = 1..shortest_period \<alpha>. \<pi> \<alpha> j * i * ((1 + i) ^ n - (1 - \<rho> j) ^ n) / (i + \<rho> j)) else (1 - \<rho> k) ^ n * \<pi> \<alpha> k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_on_subset:
  assumes "isometry_on X f"
          "Y \<subseteq> X"
  shows "isometry_on Y f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on Y f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry_on X f
Y \<subseteq> X

goal (1 subgoal):
 1. isometry_on Y f
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y
Y \<subseteq> X

goal (1 subgoal):
 1. \<forall>x\<in>Y. \<forall>y\<in>Y. dist (f x) (f y) = dist x y
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_onI [intro?]:
  assumes "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) = dist x y"
  shows "isometry_on X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on X f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) = dist ?x ?y

goal (1 subgoal):
 1. isometry_on X f
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) = dist ?x ?y

goal (1 subgoal):
 1. \<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_onD:
  assumes "isometry_on X f"
          "x \<in> X" "y \<in> X"
  shows "dist (f x) (f y) = dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) (f y) = dist x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry_on X f
x \<in> X
y \<in> X

goal (1 subgoal):
 1. dist (f x) (f y) = dist x y
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y
x \<in> X
y \<in> X

goal (1 subgoal):
 1. dist (f x) (f y) = dist x y
[PROOF STEP]
by auto


[STATEMENT]
lemma isometryI [intro?]:
  assumes "\<And>x y. dist (f x) (f y) = dist x y"
          "range f = UNIV"
  shows "isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry f
[PROOF STEP]
unfolding isometry_def isometry_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. dist (f x) (f y) = dist x y) \<and> surj f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dist (f ?x) (f ?y) = dist ?x ?y
surj f

goal (1 subgoal):
 1. (\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. dist (f x) (f y) = dist x y) \<and> surj f
[PROOF STEP]
by auto


[STATEMENT]
lemma isometryD:
  assumes "isometry f"
  shows "isometry_on UNIV f"
        "dist (f x) (f y) = dist x y"
        "range f = UNIV"
        "1-lipschitz_on UNIV f"
        "uniformly_continuous_on UNIV f"
        "continuous_on UNIV f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (isometry_on UNIV f &&& dist (f x) (f y) = dist x y &&& surj f) &&& 1-lipschitz_on UNIV f &&& isUCont f &&& continuous_on UNIV f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry f

goal (1 subgoal):
 1. (isometry_on UNIV f &&& dist (f x) (f y) = dist x y &&& surj f) &&& 1-lipschitz_on UNIV f &&& isUCont f &&& continuous_on UNIV f
[PROOF STEP]
unfolding isometry_def isometry_on_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. dist (f x) (f y) = dist x y) \<and> surj f

goal (1 subgoal):
 1. (\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. dist (f x) (f y) = dist x y &&& dist (f x) (f y) = dist x y &&& surj f) &&& 1-lipschitz_on UNIV f &&& isUCont f &&& continuous_on UNIV f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> 1-lipschitz_on UNIV f
 2. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> isUCont f
 3. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> continuous_on UNIV f
[PROOF STEP]
using isometry_on_lipschitz isometry_on_uniformly_continuous isometry_on_continuous assms
[PROOF STATE]
proof (prove)
using this:
isometry_on ?X ?f \<Longrightarrow> 1-lipschitz_on ?X ?f
isometry_on ?X ?f \<Longrightarrow> uniformly_continuous_on ?X ?f
isometry_on ?X ?f \<Longrightarrow> continuous_on ?X ?f
isometry f

goal (3 subgoals):
 1. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> 1-lipschitz_on UNIV f
 2. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> isUCont f
 3. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> continuous_on UNIV f
[PROOF STEP]
unfolding isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry_on ?X ?f \<Longrightarrow> 1-lipschitz_on ?X ?f
isometry_on ?X ?f \<Longrightarrow> uniformly_continuous_on ?X ?f
isometry_on ?X ?f \<Longrightarrow> continuous_on ?X ?f
isometry_on UNIV f \<and> surj f

goal (3 subgoals):
 1. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> 1-lipschitz_on UNIV f
 2. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> isUCont f
 3. \<lbrakk>\<forall>x y. dist (f x) (f y) = dist x y; surj f\<rbrakk> \<Longrightarrow> continuous_on UNIV f
[PROOF STEP]
by blast+


[STATEMENT]
lemma isometry_on_injective:
  assumes "isometry_on X f"
  shows "inj_on f X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f X
[PROOF STEP]
using assms inj_on_def isometry_on_def
[PROOF STATE]
proof (prove)
using this:
isometry_on X f
inj_on ?f ?A = (\<forall>x\<in>?A. \<forall>y\<in>?A. ?f x = ?f y \<longrightarrow> x = y)
isometry_on ?X ?f = (\<forall>x\<in>?X. \<forall>y\<in>?X. dist (?f x) (?f y) = dist x y)

goal (1 subgoal):
 1. inj_on f X
[PROOF STEP]
by force


[STATEMENT]
lemma isometry_on_compose:
  assumes "isometry_on X f"
          "isometry_on (f`X) g"
  shows "isometry_on X (\<lambda>x. g(f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on X (\<lambda>x. g (f x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry_on X f
isometry_on (f ` X) g

goal (1 subgoal):
 1. isometry_on X (\<lambda>x. g (f x))
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y
\<forall>x\<in>f ` X. \<forall>y\<in>f ` X. dist (g x) (g y) = dist x y

goal (1 subgoal):
 1. \<forall>x\<in>X. \<forall>y\<in>X. dist (g (f x)) (g (f y)) = dist x y
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_on_cong:
  assumes "isometry_on X f"
          "\<And>x. x \<in> X \<Longrightarrow> g x = f x"
  shows "isometry_on X g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on X g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry_on X f
?x \<in> X \<Longrightarrow> g ?x = f ?x

goal (1 subgoal):
 1. isometry_on X g
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y
?x \<in> X \<Longrightarrow> g ?x = f ?x

goal (1 subgoal):
 1. \<forall>x\<in>X. \<forall>y\<in>X. dist (g x) (g y) = dist x y
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_on_inverse:
  assumes "isometry_on X f"
  shows "isometry_on (f`X) (inv_into X f)"
        "\<And>x. x \<in> X \<Longrightarrow> (inv_into X f) (f x) = x"
        "\<And>y. y \<in> f`X \<Longrightarrow> f (inv_into X f y) = y"
        "bij_betw f X (f`X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (isometry_on (f ` X) (inv_into X f) &&& (\<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x)) &&& (\<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y) &&& bij_betw f X (f ` X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. isometry_on (f ` X) (inv_into X f)
 2. \<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x
 3. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
 4. bij_betw f X (f ` X)
[PROOF STEP]
show *: "bij_betw f X (f`X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f X (f ` X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry_on X f

goal (1 subgoal):
 1. bij_betw f X (f ` X)
[PROOF STEP]
unfolding bij_betw_def inj_on_def isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y

goal (1 subgoal):
 1. (\<forall>x\<in>X. \<forall>y\<in>X. f x = f y \<longrightarrow> x = y) \<and> f ` X = f ` X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
bij_betw f X (f ` X)

goal (3 subgoals):
 1. isometry_on (f ` X) (inv_into X f)
 2. \<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x
 3. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
show "isometry_on (f`X) (inv_into X f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on (f ` X) (inv_into X f)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry_on X f

goal (1 subgoal):
 1. isometry_on (f ` X) (inv_into X f)
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y

goal (1 subgoal):
 1. \<forall>x\<in>f ` X. \<forall>y\<in>f ` X. dist (inv_into X f x) (inv_into X f y) = dist x y
[PROOF STEP]
by (auto) (metis (mono_tags, lifting) dist_eq_0_iff inj_on_def inv_into_f_f)
[PROOF STATE]
proof (state)
this:
isometry_on (f ` X) (inv_into X f)

goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x
 2. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x
 2. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
assume "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x
 2. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
show "(inv_into X f) (f x) = x"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. inv_into X f (f x) = x
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
x \<in> X
bij_betw f X (f ` X)

goal (1 subgoal):
 1. inv_into X f (f x) = x
[PROOF STEP]
by (simp add: bij_betw_def)
[PROOF STATE]
proof (state)
this:
inv_into X f (f x) = x

goal (1 subgoal):
 1. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
assume "y \<in> f`X"
[PROOF STATE]
proof (state)
this:
y \<in> f ` X

goal (1 subgoal):
 1. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> f ` X
[PROOF STEP]
show "f (inv_into X f y) = y"
[PROOF STATE]
proof (prove)
using this:
y \<in> f ` X

goal (1 subgoal):
 1. f (inv_into X f y) = y
[PROOF STEP]
by (simp add: f_inv_into_f)
[PROOF STATE]
proof (state)
this:
f (inv_into X f y) = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_inverse:
  assumes "isometry f"
  shows "isometry (inv f)"
        "bij f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry (inv f) &&& bij f
[PROOF STEP]
using isometry_on_inverse[OF isometryD(1)[OF assms]] isometryD(3)[OF assms]
[PROOF STATE]
proof (prove)
using this:
isometry_on (range f) (inv f)
?x \<in> UNIV \<Longrightarrow> inv f (f ?x) = ?x
?y \<in> range f \<Longrightarrow> f (inv f ?y) = ?y
bij_betw f UNIV (range f)
surj f

goal (1 subgoal):
 1. isometry (inv f) &&& bij f
[PROOF STEP]
unfolding isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry_on (range f) (inv f)
?x \<in> UNIV \<Longrightarrow> inv f (f ?x) = ?x
?y \<in> range f \<Longrightarrow> f (inv f ?y) = ?y
bij_betw f UNIV (range f)
surj f

goal (1 subgoal):
 1. isometry_on UNIV (inv f) \<and> surj (inv f) &&& bij f
[PROOF STEP]
by (auto simp add: bij_imp_bij_inv bij_is_surj)


[STATEMENT]
lemma isometry_on_homeomorphism:
  assumes "isometry_on X f"
  shows "homeomorphism X (f`X) f (inv_into X f)"
        "homeomorphism_on X f"
        "X homeomorphic f`X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism X (f ` X) f (inv_into X f) &&& homeomorphism_on X f &&& X homeomorphic f ` X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. homeomorphism X (f ` X) f (inv_into X f)
 2. homeomorphism_on X f
 3. X homeomorphic f ` X
[PROOF STEP]
show *: "homeomorphism X (f`X) f (inv_into X f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism X (f ` X) f (inv_into X f)
[PROOF STEP]
apply (rule homeomorphismI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. continuous_on X f
 2. continuous_on (f ` X) (inv_into X f)
 3. f ` X \<subseteq> f ` X
 4. inv_into X f ` f ` X \<subseteq> X
 5. \<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x
 6. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
using uniformly_continuous_imp_continuous[OF isometry_on_uniformly_continuous]
    isometry_on_inverse[OF assms] assms
[PROOF STATE]
proof (prove)
using this:
isometry_on ?s ?f \<Longrightarrow> continuous_on ?s ?f
isometry_on (f ` X) (inv_into X f)
?x \<in> X \<Longrightarrow> inv_into X f (f ?x) = ?x
?y \<in> f ` X \<Longrightarrow> f (inv_into X f ?y) = ?y
bij_betw f X (f ` X)
isometry_on X f

goal (6 subgoals):
 1. continuous_on X f
 2. continuous_on (f ` X) (inv_into X f)
 3. f ` X \<subseteq> f ` X
 4. inv_into X f ` f ` X \<subseteq> X
 5. \<And>x. x \<in> X \<Longrightarrow> inv_into X f (f x) = x
 6. \<And>y. y \<in> f ` X \<Longrightarrow> f (inv_into X f y) = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
homeomorphism X (f ` X) f (inv_into X f)

goal (2 subgoals):
 1. homeomorphism_on X f
 2. X homeomorphic f ` X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
homeomorphism X (f ` X) f (inv_into X f)
[PROOF STEP]
show "X homeomorphic f`X"
[PROOF STATE]
proof (prove)
using this:
homeomorphism X (f ` X) f (inv_into X f)

goal (1 subgoal):
 1. X homeomorphic f ` X
[PROOF STEP]
unfolding homeomorphic_def
[PROOF STATE]
proof (prove)
using this:
homeomorphism X (f ` X) f (inv_into X f)

goal (1 subgoal):
 1. \<exists>fa g. homeomorphism X (f ` X) fa g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X homeomorphic f ` X

goal (1 subgoal):
 1. homeomorphism_on X f
[PROOF STEP]
show "homeomorphism_on X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism_on X f
[PROOF STEP]
unfolding homeomorphism_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ex (homeomorphism X (f ` X) f)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
homeomorphism X (f ` X) f (inv_into X f)

goal (1 subgoal):
 1. Ex (homeomorphism X (f ` X) f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
homeomorphism_on X f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_homeomorphism:
  fixes f::"('a::metric_space) \<Rightarrow> ('b::metric_space)"
  assumes "isometry f"
  shows "homeomorphism UNIV UNIV f (inv f)"
        "(UNIV::'a set) homeomorphic (UNIV::'b set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism UNIV UNIV f (inv f) &&& UNIV homeomorphic UNIV
[PROOF STEP]
using isometry_on_homeomorphism[OF isometryD(1)[OF assms]] isometryD(3)[OF assms]
[PROOF STATE]
proof (prove)
using this:
homeomorphism UNIV (range f) f (inv f)
homeomorphism_on UNIV f
UNIV homeomorphic range f
surj f

goal (1 subgoal):
 1. homeomorphism UNIV UNIV f (inv f) &&& UNIV homeomorphic UNIV
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_on_closure:
  assumes "isometry_on X f"
          "continuous_on (closure X) f"
  shows "isometry_on (closure X) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on (closure X) f
[PROOF STEP]
proof (rule isometry_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
assume "x \<in> closure X" "y \<in> closure X"
[PROOF STATE]
proof (state)
this:
x \<in> closure X
y \<in> closure X

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
obtain u v::"nat \<Rightarrow> 'a" where *: "\<And>n. u n \<in> X" "u \<longlonglongrightarrow> x"
                                   "\<And>n. v n \<in> X" "v \<longlonglongrightarrow> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u v. \<lbrakk>\<And>n. u n \<in> X; u \<longlonglongrightarrow> x; \<And>n. v n \<in> X; v \<longlonglongrightarrow> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x \<in> closure X\<close> \<open>y \<in> closure X\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> closure X
y \<in> closure X

goal (1 subgoal):
 1. (\<And>u v. \<lbrakk>\<And>n. u n \<in> X; u \<longlonglongrightarrow> x; \<And>n. v n \<in> X; v \<longlonglongrightarrow> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding closure_sequential
[PROOF STATE]
proof (prove)
using this:
\<exists>xa. (\<forall>n. xa n \<in> X) \<and> xa \<longlonglongrightarrow> x
\<exists>x. (\<forall>n. x n \<in> X) \<and> x \<longlonglongrightarrow> y

goal (1 subgoal):
 1. (\<And>u v. \<lbrakk>\<And>n. u n \<in> X; u \<longlonglongrightarrow> x; \<And>n. v n \<in> X; v \<longlonglongrightarrow> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u ?n \<in> X
u \<longlonglongrightarrow> x
v ?n \<in> X
v \<longlonglongrightarrow> y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
have "(\<lambda>n. f (u n)) \<longlonglongrightarrow> f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (u n)) \<longlonglongrightarrow> f x
[PROOF STEP]
using *(1) *(2) \<open>x \<in> closure X\<close> \<open>continuous_on (closure X) f\<close>
[PROOF STATE]
proof (prove)
using this:
u ?n \<in> X
u \<longlonglongrightarrow> x
x \<in> closure X
continuous_on (closure X) f

goal (1 subgoal):
 1. (\<lambda>n. f (u n)) \<longlonglongrightarrow> f x
[PROOF STEP]
unfolding comp_def continuous_on_closure_sequentially[of X f]
[PROOF STATE]
proof (prove)
using this:
u ?n \<in> X
u \<longlonglongrightarrow> x
x \<in> closure X
\<forall>x a. a \<in> closure X \<and> (\<forall>n. x n \<in> X) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>xa. f (x xa)) \<longlonglongrightarrow> f a

goal (1 subgoal):
 1. (\<lambda>n. f (u n)) \<longlonglongrightarrow> f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (u n)) \<longlonglongrightarrow> f x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (u n)) \<longlonglongrightarrow> f x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
have "(\<lambda>n. f (v n)) \<longlonglongrightarrow> f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (v n)) \<longlonglongrightarrow> f y
[PROOF STEP]
using *(3) *(4) \<open>y \<in> closure X\<close> \<open>continuous_on (closure X) f\<close>
[PROOF STATE]
proof (prove)
using this:
v ?n \<in> X
v \<longlonglongrightarrow> y
y \<in> closure X
continuous_on (closure X) f

goal (1 subgoal):
 1. (\<lambda>n. f (v n)) \<longlonglongrightarrow> f y
[PROOF STEP]
unfolding comp_def continuous_on_closure_sequentially[of X f]
[PROOF STATE]
proof (prove)
using this:
v ?n \<in> X
v \<longlonglongrightarrow> y
y \<in> closure X
\<forall>x a. a \<in> closure X \<and> (\<forall>n. x n \<in> X) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>xa. f (x xa)) \<longlonglongrightarrow> f a

goal (1 subgoal):
 1. (\<lambda>n. f (v n)) \<longlonglongrightarrow> f y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (v n)) \<longlonglongrightarrow> f y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. f (u n)) \<longlonglongrightarrow> f x
(\<lambda>n. f (v n)) \<longlonglongrightarrow> f y
[PROOF STEP]
have "(\<lambda>n. dist (f (u n)) (f (v n))) \<longlonglongrightarrow> dist (f x) (f y)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f (u n)) \<longlonglongrightarrow> f x
(\<lambda>n. f (v n)) \<longlonglongrightarrow> f y

goal (1 subgoal):
 1. (\<lambda>n. dist (f (u n)) (f (v n))) \<longlonglongrightarrow> dist (f x) (f y)
[PROOF STEP]
by (simp add: tendsto_dist)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist (f (u n)) (f (v n))) \<longlonglongrightarrow> dist (f x) (f y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. dist (f (u n)) (f (v n))) \<longlonglongrightarrow> dist (f x) (f y)
[PROOF STEP]
have "(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist (f (u n)) (f (v n))) \<longlonglongrightarrow> dist (f x) (f y)

goal (1 subgoal):
 1. (\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)
[PROOF STEP]
using assms(1) *(1) *(3)
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist (f (u n)) (f (v n))) \<longlonglongrightarrow> dist (f x) (f y)
isometry_on X f
u ?n \<in> X
v ?n \<in> X

goal (1 subgoal):
 1. (\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist (f (u n)) (f (v n))) \<longlonglongrightarrow> dist (f x) (f y)
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y
u ?n \<in> X
v ?n \<in> X

goal (1 subgoal):
 1. (\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
have "(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist x y
[PROOF STEP]
using *(2) *(4)
[PROOF STATE]
proof (prove)
using this:
u \<longlonglongrightarrow> x
v \<longlonglongrightarrow> y

goal (1 subgoal):
 1. (\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist x y
[PROOF STEP]
by (simp add: tendsto_dist)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist x y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> closure X; y \<in> closure X\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist x y
[PROOF STEP]
show "dist (f x) (f y) = dist x y"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist x y

goal (1 subgoal):
 1. dist (f x) (f y) = dist x y
[PROOF STEP]
using LIMSEQ_unique
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist (f x) (f y)
(\<lambda>n. dist (u n) (v n)) \<longlonglongrightarrow> dist x y
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. dist (f x) (f y) = dist x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f x) (f y) = dist x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_extend_closure:
  fixes f::"('a::metric_space) \<Rightarrow> ('b::complete_space)"
  assumes "isometry_on X f"
  shows "\<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)
[PROOF STEP]
obtain g where g: "\<And>x. x \<in> X \<Longrightarrow> g x = f x" "uniformly_continuous_on (closure X) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>x. x \<in> X \<Longrightarrow> g x = f x; uniformly_continuous_on (closure X) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using uniformly_continuous_on_extension_on_closure[OF isometry_on_uniformly_continuous[OF assms]]
[PROOF STATE]
proof (prove)
using this:
(\<And>g. \<lbrakk>uniformly_continuous_on (closure X) g; \<And>x. x \<in> X \<Longrightarrow> f x = g x; \<And>Y h x. \<lbrakk>X \<subseteq> Y; Y \<subseteq> closure X; continuous_on Y h; \<And>x. x \<in> X \<Longrightarrow> f x = h x; x \<in> Y\<rbrakk> \<Longrightarrow> h x = g x\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>x. x \<in> X \<Longrightarrow> g x = f x; uniformly_continuous_on (closure X) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> X \<Longrightarrow> g ?x = f ?x
uniformly_continuous_on (closure X) g

goal (1 subgoal):
 1. \<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)
[PROOF STEP]
have "isometry_on (closure X) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on (closure X) g
[PROOF STEP]
apply (rule isometry_on_closure, rule isometry_on_cong[OF assms])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> g x = f x
 2. continuous_on (closure X) g
[PROOF STEP]
using g uniformly_continuous_imp_continuous[OF g(2)]
[PROOF STATE]
proof (prove)
using this:
?x \<in> X \<Longrightarrow> g ?x = f ?x
uniformly_continuous_on (closure X) g
continuous_on (closure X) g

goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> g x = f x
 2. continuous_on (closure X) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isometry_on (closure X) g

goal (1 subgoal):
 1. \<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isometry_on (closure X) g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isometry_on (closure X) g

goal (1 subgoal):
 1. \<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)
[PROOF STEP]
using g(1)
[PROOF STATE]
proof (prove)
using this:
isometry_on (closure X) g
?x \<in> X \<Longrightarrow> g ?x = f ?x

goal (1 subgoal):
 1. \<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. isometry_on (closure X) g \<and> (\<forall>x\<in>X. g x = f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_on_complete_image:
  assumes "isometry_on X f"
          "complete X"
  shows "complete (f`X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete (f ` X)
[PROOF STEP]
proof (rule completeI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
fix u :: "nat \<Rightarrow> 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
assume u: "\<forall>n. u n \<in> f`X" "Cauchy u"
[PROOF STATE]
proof (state)
this:
\<forall>n. u n \<in> f ` X
Cauchy u

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
define v where "v = (\<lambda>n. inv_into X f (u n))"
[PROOF STATE]
proof (state)
this:
v = (\<lambda>n. inv_into X f (u n))

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
have "v n \<in> X" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v n \<in> X
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_into X f (u n) \<in> X
[PROOF STEP]
by (simp add: inv_into_into u(1))
[PROOF STATE]
proof (state)
this:
v ?n \<in> X

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
have "dist (v n) (v m) = dist (u n) (u m)" for m n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (v n) (v m) = dist (u n) (u m)
[PROOF STEP]
using u(1) isometry_on_inverse[OF \<open>isometry_on X f\<close>]
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> f ` X
isometry_on (f ` X) (inv_into X f)
?x \<in> X \<Longrightarrow> inv_into X f (f ?x) = ?x
?y \<in> f ` X \<Longrightarrow> f (inv_into X f ?y) = ?y
bij_betw f X (f ` X)

goal (1 subgoal):
 1. dist (v n) (v m) = dist (u n) (u m)
[PROOF STEP]
unfolding isometry_on_def v_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> f ` X
\<forall>x\<in>f ` X. \<forall>y\<in>f ` X. dist (inv_into X f x) (inv_into X f y) = dist x y
?x \<in> X \<Longrightarrow> inv_into X f (f ?x) = ?x
?y \<in> f ` X \<Longrightarrow> f (inv_into X f ?y) = ?y
bij_betw f X (f ` X)

goal (1 subgoal):
 1. dist (inv_into X f (u n)) (inv_into X f (u m)) = dist (u n) (u m)
[PROOF STEP]
by (auto simp add: inv_into_into)
[PROOF STATE]
proof (state)
this:
dist (v ?n) (v ?m) = dist (u ?n) (u ?m)

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (v ?n) (v ?m) = dist (u ?n) (u ?m)
[PROOF STEP]
have "Cauchy v"
[PROOF STATE]
proof (prove)
using this:
dist (v ?n) (v ?m) = dist (u ?n) (u ?m)

goal (1 subgoal):
 1. Cauchy v
[PROOF STEP]
using u(2)
[PROOF STATE]
proof (prove)
using this:
dist (v ?n) (v ?m) = dist (u ?n) (u ?m)
Cauchy u

goal (1 subgoal):
 1. Cauchy v
[PROOF STEP]
unfolding Cauchy_def
[PROOF STATE]
proof (prove)
using this:
dist (v ?n) (v ?m) = dist (u ?n) (u ?m)
\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (u m) (u n) < e

goal (1 subgoal):
 1. \<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (v m) (v n) < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Cauchy v

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
obtain l where "l \<in> X" "v \<longlonglongrightarrow> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l \<in> X; v \<longlonglongrightarrow> l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule completeE[OF \<open>complete X\<close> _ \<open>Cauchy v\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>l. \<lbrakk>l \<in> X; v \<longlonglongrightarrow> l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>n. v n \<in> X
 2. \<And>l. \<lbrakk>\<And>l. \<lbrakk>l \<in> X; v \<longlonglongrightarrow> l\<rbrakk> \<Longrightarrow> thesis; l \<in> X; v \<longlonglongrightarrow> l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<And>n. v n \<in> X\<close>
[PROOF STATE]
proof (prove)
using this:
v ?n \<in> X

goal (2 subgoals):
 1. (\<And>l. \<lbrakk>l \<in> X; v \<longlonglongrightarrow> l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>n. v n \<in> X
 2. \<And>l. \<lbrakk>\<And>l. \<lbrakk>l \<in> X; v \<longlonglongrightarrow> l\<rbrakk> \<Longrightarrow> thesis; l \<in> X; v \<longlonglongrightarrow> l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<in> X
v \<longlonglongrightarrow> l

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
have "(\<lambda>n. f (v n)) \<longlonglongrightarrow> f l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (v n)) \<longlonglongrightarrow> f l
[PROOF STEP]
apply (rule continuous_on_tendsto_compose[OF isometry_on_continuous[OF \<open>isometry_on X f\<close>]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. v \<longlonglongrightarrow> l
 2. l \<in> X
 3. \<forall>\<^sub>F n in sequentially. v n \<in> X
[PROOF STEP]
using \<open>\<And>n. v n \<in> X\<close> \<open>l \<in> X\<close> \<open>v \<longlonglongrightarrow> l\<close>
[PROOF STATE]
proof (prove)
using this:
v ?n \<in> X
l \<in> X
v \<longlonglongrightarrow> l

goal (3 subgoals):
 1. v \<longlonglongrightarrow> l
 2. l \<in> X
 3. \<forall>\<^sub>F n in sequentially. v n \<in> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (v n)) \<longlonglongrightarrow> f l

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (v n)) \<longlonglongrightarrow> f l

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
have "f(v n) = u n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (v n) = u n
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (inv_into X f (u n)) = u n
[PROOF STEP]
by (simp add: f_inv_into_f u(1))
[PROOF STATE]
proof (state)
this:
f (v ?n) = u ?n

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. f (v n)) \<longlonglongrightarrow> f l
f (v ?n) = u ?n
[PROOF STEP]
have "u \<longlonglongrightarrow> f l"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f (v n)) \<longlonglongrightarrow> f l
f (v ?n) = u ?n

goal (1 subgoal):
 1. u \<longlonglongrightarrow> f l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<longlonglongrightarrow> f l

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>n. fa n \<in> f ` X; Cauchy fa\<rbrakk> \<Longrightarrow> \<exists>l\<in>f ` X. fa \<longlonglongrightarrow> l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<longlonglongrightarrow> f l
[PROOF STEP]
show "\<exists>m \<in> f`X. u \<longlonglongrightarrow> m"
[PROOF STATE]
proof (prove)
using this:
u \<longlonglongrightarrow> f l

goal (1 subgoal):
 1. \<exists>m\<in>f ` X. u \<longlonglongrightarrow> m
[PROOF STEP]
using \<open>l \<in> X\<close>
[PROOF STATE]
proof (prove)
using this:
u \<longlonglongrightarrow> f l
l \<in> X

goal (1 subgoal):
 1. \<exists>m\<in>f ` X. u \<longlonglongrightarrow> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<in>f ` X. u \<longlonglongrightarrow> m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_on_id [simp]:
  "isometry_on A (\<lambda>x. x)"
  "isometry_on A id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on A (\<lambda>x. x) &&& isometry_on A id
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. dist x y = dist x y &&& \<forall>x\<in>A. \<forall>y\<in>A. dist (id x) (id y) = dist x y
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_on_add [simp]:
  "isometry_on A (\<lambda>x. x + (t::'a::real_normed_vector))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on A (\<lambda>x. x + t)
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. dist (x + t) (y + t) = dist x y
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_on_minus [simp]:
  "isometry_on A (\<lambda>(x::'a::real_normed_vector). -x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on A uminus
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. dist (- x) (- y) = dist x y
[PROOF STEP]
by (auto simp add: dist_minus)


[STATEMENT]
lemma isometry_on_diff [simp]:
  "isometry_on A (\<lambda>x. (t::'a::real_normed_vector) - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on A ((-) t)
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. dist (t - x) (t - y) = dist x y
[PROOF STEP]
by (auto, metis add_uminus_conv_diff dist_add_cancel dist_minus)


[STATEMENT]
lemma isometry_preserves_bounded:
  assumes "isometry_on X f"
          "A \<subseteq> X"
  shows "bounded (f`A) \<longleftrightarrow> bounded A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded (f ` A) = bounded A
[PROOF STEP]
unfolding bounded_two_points
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>e. \<forall>x\<in>f ` A. \<forall>y\<in>f ` A. dist x y \<le> e) = (\<exists>e. \<forall>x\<in>A. \<forall>y\<in>A. dist x y \<le> e)
[PROOF STEP]
using assms(2) isometry_onD[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> X
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) = dist ?x ?y

goal (1 subgoal):
 1. (\<exists>e. \<forall>x\<in>f ` A. \<forall>y\<in>f ` A. dist x y \<le> e) = (\<exists>e. \<forall>x\<in>A. \<forall>y\<in>A. dist x y \<le> e)
[PROOF STEP]
by auto (metis assms(2) rev_subsetD)+


[STATEMENT]
lemma isometry_preserves_infdist:
  "infdist (f x) (f`A) = infdist x A"
  if "isometry_on X f" "A \<subseteq> X" "x \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f x) (f ` A) = infdist x A
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
isometry_on X f
A \<subseteq> X
x \<in> X

goal (1 subgoal):
 1. infdist (f x) (f ` A) = infdist x A
[PROOF STEP]
by (simp add: infdist_def image_comp isometry_on_def subset_iff)


[STATEMENT]
lemma isometry_preserves_hausdorff_distance:
  "hausdorff_distance (f`A) (f`B) = hausdorff_distance A B"
  if "isometry_on X f" "A \<subseteq> X" "B \<subseteq> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` A) (f ` B) = hausdorff_distance A B
[PROOF STEP]
using that isometry_preserves_infdist [OF that(1) that(2)]
  isometry_preserves_infdist [OF that(1) that(3)]
  isometry_preserves_bounded [OF that(1) that(2)]
  isometry_preserves_bounded [OF that(1) that(3)]
[PROOF STATE]
proof (prove)
using this:
isometry_on X f
A \<subseteq> X
B \<subseteq> X
?x \<in> X \<Longrightarrow> infdist (f ?x) (f ` A) = infdist ?x A
?x \<in> X \<Longrightarrow> infdist (f ?x) (f ` B) = infdist ?x B
bounded (f ` A) = bounded A
bounded (f ` B) = bounded B

goal (1 subgoal):
 1. hausdorff_distance (f ` A) (f ` B) = hausdorff_distance A B
[PROOF STEP]
by (simp add: hausdorff_distance_def image_comp subset_eq)


[STATEMENT]
lemma isometry_on_UNIV_iterates:
  fixes f::"('a::metric_space) \<Rightarrow> 'a"
  assumes "isometry_on UNIV f"
  shows "isometry_on UNIV (f^^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on UNIV (f ^^ n)
[PROOF STEP]
by (induction n, auto, rule isometry_on_compose[of _ _ f], auto intro: isometry_on_subset[OF assms])


[STATEMENT]
lemma isometry_iterates:
  fixes f::"('a::metric_space) \<Rightarrow> 'a"
  assumes "isometry f"
  shows "isometry (f^^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry (f ^^ n)
[PROOF STEP]
using isometry_on_UNIV_iterates[OF isometryD(1)[OF assms], of n] bij_fn[OF isometry_inverse(2)[OF assms], of n]
[PROOF STATE]
proof (prove)
using this:
isometry_on UNIV (f ^^ n)
bij (f ^^ n)

goal (1 subgoal):
 1. isometry (f ^^ n)
[PROOF STEP]
unfolding isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry_on UNIV (f ^^ n)
bij (f ^^ n)

goal (1 subgoal):
 1. isometry_on UNIV (f ^^ n) \<and> surj (f ^^ n)
[PROOF STEP]
by (simp add: bij_is_surj)


[STATEMENT]
lemma geodesic_segment_betweenI:
  assumes "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}"
  shows "geodesic_segment_between G x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G x y
[PROOF STEP]
unfolding geodesic_segment_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. g 0 = x \<and> g (dist x y) = y \<and> isometry_on {0..dist x y} g \<and> G = g ` {0..dist x y}
[PROOF STEP]
apply (rule exI[of _ g])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g 0 = x \<and> g (dist x y) = y \<and> isometry_on {0..dist x y} g \<and> G = g ` {0..dist x y}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. g 0 = x \<and> g (dist x y) = y \<and> isometry_on {0..dist x y} g \<and> G = g ` {0..dist x y}
[PROOF STEP]
by auto


[STATEMENT]
lemma geodesic_segmentI [intro, simp]:
  assumes "geodesic_segment_between G x y"
  shows "geodesic_segment G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment G
[PROOF STEP]
unfolding geodesic_segment_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. Ex (geodesic_segment_between G x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y

goal (1 subgoal):
 1. \<exists>x. Ex (geodesic_segment_between G x)
[PROOF STEP]
by auto