[STATEMENT]
lemma self_finance_init:
  assumes "\<forall>w. prices Mkt asset 0 w \<noteq> 0"
  and "portfolio pf"
shows "val_process Mkt (self_finance Mkt v pf asset) 0 w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
define scp where "scp = qty_single asset (remaining_qty Mkt v pf asset)"
[PROOF STATE]
proof (state)
this:
scp = qty_single asset (remaining_qty Mkt v pf asset)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "val_process Mkt (self_finance Mkt v pf asset) 0 w =
    val_process Mkt pf 0 w +
    val_process Mkt scp 0 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt scp 0 w
[PROOF STEP]
unfolding scp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) 0 w
[PROOF STEP]
using assms single_comp_portfolio[of asset]
    sum_val_process[of pf "qty_single asset (remaining_qty Mkt v pf asset)" Mkt]
[PROOF STATE]
proof (prove)
using this:
\<forall>w. prices Mkt asset 0 w \<noteq> 0
portfolio pf
portfolio (qty_single asset ?qty)
\<lbrakk>portfolio pf; portfolio (qty_single asset (remaining_qty Mkt v pf asset))\<rbrakk> \<Longrightarrow> \<forall>n w. val_process Mkt (qty_sum pf (qty_single asset (remaining_qty Mkt v pf asset))) n w = val_process Mkt pf n w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) n w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) 0 w
[PROOF STEP]
by (simp add: \<open>\<And>qty. portfolio (qty_single asset qty)\<close> self_finance_def)
[PROOF STATE]
proof (state)
this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt scp 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = val_process Mkt pf 0 w + val_process Mkt scp 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w +
    (sum (\<lambda>x. ((prices Mkt) x 0 w) * (scp x (Suc 0) w)) {asset})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)
[PROOF STEP]
using subset_val_process'[of "{asset}" scp]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {asset}; support_set scp \<subseteq> {asset}\<rbrakk> \<Longrightarrow> val_process ?Mkt scp ?n ?w = (\<Sum>x\<in>{asset}. prices ?Mkt x ?n ?w * scp x (Suc ?n) ?w)

goal (1 subgoal):
 1. val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)
[PROOF STEP]
unfolding scp_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {asset}; support_set (qty_single asset (remaining_qty Mkt v pf asset)) \<subseteq> {asset}\<rbrakk> \<Longrightarrow> val_process ?Mkt (qty_single asset (remaining_qty Mkt v pf asset)) ?n ?w = (\<Sum>x\<in>{asset}. prices ?Mkt x ?n ?w * qty_single asset (remaining_qty Mkt v pf asset) x (Suc ?n) ?w)

goal (1 subgoal):
 1. val_process Mkt pf 0 w + val_process Mkt (qty_single asset (remaining_qty Mkt v pf asset)) 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * qty_single asset (remaining_qty Mkt v pf asset) x (Suc 0) w)
[PROOF STEP]
by (auto simp add:  single_comp_support)
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + val_process Mkt scp 0 w = val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w) = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w) = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + (\<Sum>x\<in>{asset}. prices Mkt x 0 w * scp x (Suc 0) w) = val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + prices Mkt asset 0 w * (remaining_qty Mkt v pf asset) (Suc 0) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w
[PROOF STEP]
unfolding scp_def qty_single_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * (qty_empty(asset := remaining_qty Mkt v pf asset)) asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * scp asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w)/(prices Mkt asset 0 w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * remaining_qty Mkt v pf asset (Suc 0) w = val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>w. prices Mkt asset 0 w \<noteq> 0
portfolio pf

goal (1 subgoal):
 1. val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + prices Mkt asset 0 w * (v - val_process Mkt pf 0 w) / prices Mkt asset 0 w = val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w)

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
have "... = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w) = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_process Mkt pf 0 w + (v - val_process Mkt pf 0 w) = v

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = v

goal (1 subgoal):
 1. val_process Mkt (self_finance Mkt v pf asset) 0 w = v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
val_process Mkt (self_finance Mkt v pf asset) 0 w = v

goal:
No subgoals!
[PROOF STEP]
qed