[STATEMENT]
lemma ipt_tcp_flags_assume_flag: assumes "match_tcp_flags flg (p_tcp_flags p)"
    shows "matches (common_matcher, \<alpha>) (ipt_tcp_flags_assume_flag flg m) a p \<longleftrightarrow> matches (common_matcher, \<alpha>) m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (common_matcher, \<alpha>) (ipt_tcp_flags_assume_flag flg m) a p = matches (common_matcher, \<alpha>) m a p
[PROOF STEP]
proof(rule matches_iff_apply_f)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg m)) = ternary_ternary_eval (map_match_tac common_matcher p m)
[PROOF STEP]
show "ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg m)) = ternary_ternary_eval (map_match_tac common_matcher p m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg m)) = ternary_ternary_eval (map_match_tac common_matcher p m)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match_tcp_flags flg (p_tcp_flags p)

goal (1 subgoal):
 1. ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg m)) = ternary_ternary_eval (map_match_tac common_matcher p m)
[PROOF STEP]
proof(induction m rule: ipt_tcp_flags_assume_flag.induct)
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>flg x. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (L4_Flags x)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (L4_Flags x)))
 2. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Src v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Src v)))
 3. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Dst v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Dst v)))
 4. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (IIface v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (IIface v)))
 5. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (OIface v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (OIface v)))
 6. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Prot v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Prot v)))
 7. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Src_Ports v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Src_Ports v)))
 8. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Dst_Ports v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Dst_Ports v)))
 9. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (MultiportPorts v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (MultiportPorts v)))
 10. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (CT_State v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (CT_State v)))
A total of 14 subgoals...
[PROOF STEP]
case (1 flg x)
[PROOF STATE]
proof (state)
this:
match_tcp_flags flg (p_tcp_flags p)

goal (14 subgoals):
 1. \<And>flg x. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (L4_Flags x)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (L4_Flags x)))
 2. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Src v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Src v)))
 3. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Dst v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Dst v)))
 4. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (IIface v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (IIface v)))
 5. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (OIface v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (OIface v)))
 6. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Prot v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Prot v)))
 7. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Src_Ports v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Src_Ports v)))
 8. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Dst_Ports v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Dst_Ports v)))
 9. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (MultiportPorts v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (MultiportPorts v)))
 10. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (CT_State v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (CT_State v)))
A total of 14 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
match_tcp_flags flg (p_tcp_flags p)

goal (1 subgoal):
 1. ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (L4_Flags x)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (L4_Flags x)))
[PROOF STEP]
apply(simp add: ipt_tcp_flags_equal del: match_tcp_flags.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (case match_tcp_flags_conjunct_option x flg of None \<Rightarrow> MatchNot MatchAny | Some f3 \<Rightarrow> Match (L4_Flags f3))) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
[PROOF STEP]
apply(cases "match_tcp_flags_conjunct_option x flg")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = None\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (case match_tcp_flags_conjunct_option x flg of None \<Rightarrow> MatchNot MatchAny | Some f3 \<Rightarrow> Match (L4_Flags f3))) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
 2. \<And>a. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = Some a\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (case match_tcp_flags_conjunct_option x flg of None \<Rightarrow> MatchNot MatchAny | Some f3 \<Rightarrow> Match (L4_Flags f3))) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = None\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> TernaryFalse = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
 2. \<And>a. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = Some a\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (case match_tcp_flags_conjunct_option x flg of None \<Rightarrow> MatchNot MatchAny | Some f3 \<Rightarrow> Match (L4_Flags f3))) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
[PROOF STEP]
using match_tcp_flags_conjunct_option_None bool_to_ternary_simps(2)
[PROOF STATE]
proof (prove)
using this:
match_tcp_flags_conjunct_option ?f1.0 ?f2.0 = None \<Longrightarrow> \<not> (match_tcp_flags ?f1.0 ?pkt \<and> match_tcp_flags ?f2.0 ?pkt)
(bool_to_ternary ?Y = TernaryFalse) = (\<not> ?Y)

goal (2 subgoals):
 1. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = None\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> TernaryFalse = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
 2. \<And>a. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = Some a\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (case match_tcp_flags_conjunct_option x flg of None \<Rightarrow> MatchNot MatchAny | Some f3 \<Rightarrow> Match (L4_Flags f3))) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = Some a\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (case match_tcp_flags_conjunct_option x flg of None \<Rightarrow> MatchNot MatchAny | Some f3 \<Rightarrow> Match (L4_Flags f3))) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); match_tcp_flags_conjunct_option x flg = Some a\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> bool_to_ternary (match_tcp_flags a (p_tcp_flags p)) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
[PROOF STEP]
apply(drule_tac pkt="(p_tcp_flags p)" in match_tcp_flags_conjunct_option_Some)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>match_tcp_flags flg (p_tcp_flags p); (match_tcp_flags x (p_tcp_flags p) \<and> match_tcp_flags flg (p_tcp_flags p)) = match_tcp_flags a (p_tcp_flags p)\<rbrakk> \<Longrightarrow> (\<exists>pkt. match_tcp_flags x pkt = (\<not> match_tcp_flags flg pkt)) \<longrightarrow> bool_to_ternary (match_tcp_flags a (p_tcp_flags p)) = bool_to_ternary (match_tcp_flags x (p_tcp_flags p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (L4_Flags x)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (L4_Flags x)))

goal (13 subgoals):
 1. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Src v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Src v)))
 2. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Dst v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Dst v)))
 3. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (IIface v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (IIface v)))
 4. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (OIface v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (OIface v)))
 5. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Prot v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Prot v)))
 6. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Src_Ports v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Src_Ports v)))
 7. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Dst_Ports v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Dst_Ports v)))
 8. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (MultiportPorts v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (MultiportPorts v)))
 9. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (CT_State v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (CT_State v)))
 10. \<And>flg v. match_tcp_flags flg (p_tcp_flags p) \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg (Match (Extra v)))) = ternary_ternary_eval (map_match_tac common_matcher p (Match (Extra v)))
A total of 13 subgoals...
[PROOF STEP]
qed(simp_all del: match_tcp_flags.simps)
[PROOF STATE]
proof (state)
this:
ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg m)) = ternary_ternary_eval (map_match_tac common_matcher p m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipt_tcp_flags_assume_syn_simple_ruleset: "simple_ruleset rs \<Longrightarrow> simple_ruleset (ipt_tcp_flags_assume_syn rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_ruleset rs \<Longrightarrow> simple_ruleset (ipt_tcp_flags_assume_syn rs)
[PROOF STEP]
by (simp add: ipt_tcp_flags_assume_syn_def optimize_matches_simple_ruleset)


[STATEMENT]
lemma packet_assume_new_simple_ruleset: "simple_ruleset rs \<Longrightarrow> simple_ruleset (packet_assume_new rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_ruleset rs \<Longrightarrow> simple_ruleset (packet_assume_new rs)
[PROOF STEP]
by (simp add: packet_assume_new_def ipt_tcp_flags_assume_syn_simple_ruleset ctstate_assume_new_simple_ruleset)


[STATEMENT]
lemma fv_transform: "fv (transform a e) \<subseteq> fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (transform a e) \<subseteq> fv e
[PROOF STEP]
unfolding fv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v. atom v \<in> supp (transform a e)} \<subseteq> {v. atom v \<in> supp e}
[PROOF STEP]
by (auto dest: subsetD[OF supp_transform])


[STATEMENT]
lemma subst_transform: "(transform a e)[x ::= y] = transform a e[x ::= y]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (transform a e)[x::=y] = transform a e[x::=y]
[PROOF STEP]
proof (nominal_induct e avoiding: x y arbitrary: a  rule: exp_strong_induct_set)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>var x y a. (transform a (Var var))[x::=y] = transform a (Var var)[x::=y]
 2. \<And>exp var x y a. (\<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]) \<Longrightarrow> (transform a (App exp var))[x::=y] = transform a (App exp var)[x::=y]
 3. \<And>\<Gamma> exp x y a. \<lbrakk>atom ` domA \<Gamma> \<sharp>* x; atom ` domA \<Gamma> \<sharp>* y; \<And>b ba x e a. (x, e) \<in> set \<Gamma> \<Longrightarrow> (transform a e)[b::=ba] = transform a e[b::=ba]; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Terms.Let \<Gamma> exp))[x::=y] = transform a (Terms.Let \<Gamma> exp)[x::=y]
 4. \<And>var exp x y a. \<lbrakk>atom var \<sharp> x; atom var \<sharp> y; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Lam [var]. exp))[x::=y] = transform a (Lam [var]. exp)[x::=y]
 5. \<And>b x y a. (transform a (Bool b))[x::=y] = transform a (Bool b)[x::=y]
 6. \<And>scrut e1 e2 x y a. \<lbrakk>\<And>b ba a. (transform a scrut)[b::=ba] = transform a scrut[b::=ba]; \<And>b ba a. (transform a e1)[b::=ba] = transform a e1[b::=ba]; \<And>b ba a. (transform a e2)[b::=ba] = transform a e2[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (scrut ? e1 : e2))[x::=y] = transform a (scrut ? e1 : e2)[x::=y]
[PROOF STEP]
case (Let \<Delta> body x y)
[PROOF STATE]
proof (state)
this:
atom ` domA \<Delta> \<sharp>* x
atom ` domA \<Delta> \<sharp>* y
(?x, ?e) \<in> set \<Delta> \<Longrightarrow> (transform ?a ?e)[?b::=?ba] = transform ?a ?e[?b::=?ba]
(transform ?a body)[?b::=?ba] = transform ?a body[?b::=?ba]

goal (6 subgoals):
 1. \<And>var x y a. (transform a (Var var))[x::=y] = transform a (Var var)[x::=y]
 2. \<And>exp var x y a. (\<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]) \<Longrightarrow> (transform a (App exp var))[x::=y] = transform a (App exp var)[x::=y]
 3. \<And>\<Gamma> exp x y a. \<lbrakk>atom ` domA \<Gamma> \<sharp>* x; atom ` domA \<Gamma> \<sharp>* y; \<And>b ba x e a. (x, e) \<in> set \<Gamma> \<Longrightarrow> (transform a e)[b::=ba] = transform a e[b::=ba]; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Terms.Let \<Gamma> exp))[x::=y] = transform a (Terms.Let \<Gamma> exp)[x::=y]
 4. \<And>var exp x y a. \<lbrakk>atom var \<sharp> x; atom var \<sharp> y; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Lam [var]. exp))[x::=y] = transform a (Lam [var]. exp)[x::=y]
 5. \<And>b x y a. (transform a (Bool b))[x::=y] = transform a (Bool b)[x::=y]
 6. \<And>scrut e1 e2 x y a. \<lbrakk>\<And>b ba a. (transform a scrut)[b::=ba] = transform a scrut[b::=ba]; \<And>b ba a. (transform a e1)[b::=ba] = transform a e1[b::=ba]; \<And>b ba a. (transform a e2)[b::=ba] = transform a e2[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (scrut ? e1 : e2))[x::=y] = transform a (scrut ? e1 : e2)[x::=y]
[PROOF STEP]
hence *: "x \<notin> domA \<Delta>" "y \<notin> domA \<Delta>"
[PROOF STATE]
proof (prove)
using this:
atom ` domA \<Delta> \<sharp>* x
atom ` domA \<Delta> \<sharp>* y
(?x, ?e) \<in> set \<Delta> \<Longrightarrow> (transform ?a ?e)[?b::=?ba] = transform ?a ?e[?b::=?ba]
(transform ?a body)[?b::=?ba] = transform ?a body[?b::=?ba]

goal (1 subgoal):
 1. x \<notin> domA \<Delta> &&& y \<notin> domA \<Delta>
[PROOF STEP]
by (auto simp add: fresh_star_def fresh_at_base)
[PROOF STATE]
proof (state)
this:
x \<notin> domA \<Delta>
y \<notin> domA \<Delta>

goal (6 subgoals):
 1. \<And>var x y a. (transform a (Var var))[x::=y] = transform a (Var var)[x::=y]
 2. \<And>exp var x y a. (\<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]) \<Longrightarrow> (transform a (App exp var))[x::=y] = transform a (App exp var)[x::=y]
 3. \<And>\<Gamma> exp x y a. \<lbrakk>atom ` domA \<Gamma> \<sharp>* x; atom ` domA \<Gamma> \<sharp>* y; \<And>b ba x e a. (x, e) \<in> set \<Gamma> \<Longrightarrow> (transform a e)[b::=ba] = transform a e[b::=ba]; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Terms.Let \<Gamma> exp))[x::=y] = transform a (Terms.Let \<Gamma> exp)[x::=y]
 4. \<And>var exp x y a. \<lbrakk>atom var \<sharp> x; atom var \<sharp> y; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Lam [var]. exp))[x::=y] = transform a (Lam [var]. exp)[x::=y]
 5. \<And>b x y a. (transform a (Bool b))[x::=y] = transform a (Bool b)[x::=y]
 6. \<And>scrut e1 e2 x y a. \<lbrakk>\<And>b ba a. (transform a scrut)[b::=ba] = transform a scrut[b::=ba]; \<And>b ba a. (transform a e1)[b::=ba] = transform a e1[b::=ba]; \<And>b ba a. (transform a e2)[b::=ba] = transform a e2[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (scrut ? e1 : e2))[x::=y] = transform a (scrut ? e1 : e2)[x::=y]
[PROOF STEP]
hence "AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a"
[PROOF STATE]
proof (prove)
using this:
x \<notin> domA \<Delta>
y \<notin> domA \<Delta>

goal (1 subgoal):
 1. AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a
[PROOF STEP]
by (rule AnalLet_subst)
[PROOF STATE]
proof (state)
this:
AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a

goal (6 subgoals):
 1. \<And>var x y a. (transform a (Var var))[x::=y] = transform a (Var var)[x::=y]
 2. \<And>exp var x y a. (\<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]) \<Longrightarrow> (transform a (App exp var))[x::=y] = transform a (App exp var)[x::=y]
 3. \<And>\<Gamma> exp x y a. \<lbrakk>atom ` domA \<Gamma> \<sharp>* x; atom ` domA \<Gamma> \<sharp>* y; \<And>b ba x e a. (x, e) \<in> set \<Gamma> \<Longrightarrow> (transform a e)[b::=ba] = transform a e[b::=ba]; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Terms.Let \<Gamma> exp))[x::=y] = transform a (Terms.Let \<Gamma> exp)[x::=y]
 4. \<And>var exp x y a. \<lbrakk>atom var \<sharp> x; atom var \<sharp> y; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Lam [var]. exp))[x::=y] = transform a (Lam [var]. exp)[x::=y]
 5. \<And>b x y a. (transform a (Bool b))[x::=y] = transform a (Bool b)[x::=y]
 6. \<And>scrut e1 e2 x y a. \<lbrakk>\<And>b ba a. (transform a scrut)[b::=ba] = transform a scrut[b::=ba]; \<And>b ba a. (transform a e1)[b::=ba] = transform a e1[b::=ba]; \<And>b ba a. (transform a e2)[b::=ba] = transform a e2[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (scrut ? e1 : e2))[x::=y] = transform a (scrut ? e1 : e2)[x::=y]
[PROOF STEP]
with Let
[PROOF STATE]
proof (chain)
picking this:
atom ` domA \<Delta> \<sharp>* x
atom ` domA \<Delta> \<sharp>* y
(?x, ?e) \<in> set \<Delta> \<Longrightarrow> (transform ?a ?e)[?b::=?ba] = transform ?a ?e[?b::=?ba]
(transform ?a body)[?b::=?ba] = transform ?a body[?b::=?ba]
AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom ` domA \<Delta> \<sharp>* x
atom ` domA \<Delta> \<sharp>* y
(?x, ?e) \<in> set \<Delta> \<Longrightarrow> (transform ?a ?e)[?b::=?ba] = transform ?a ?e[?b::=?ba]
(transform ?a body)[?b::=?ba] = transform ?a body[?b::=?ba]
AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a

goal (1 subgoal):
 1. (transform a (Terms.Let \<Delta> body))[x::=y] = transform a (Terms.Let \<Delta> body)[x::=y]
[PROOF STEP]
apply (auto simp add: fresh_star_Pair TransLet_subst simp del: Let_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom ` domA \<Delta> \<sharp>* x; atom ` domA \<Delta> \<sharp>* y; \<And>x e a b ba. (x, e) \<in> set \<Delta> \<Longrightarrow> (transform a e)[b::=ba] = transform a e[b::=ba]; \<And>a b ba. (transform a body)[b::=ba] = transform a body[b::=ba]; AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a\<rbrakk> \<Longrightarrow> TransLet (AnalLet \<Delta> body a) (map_transform transform (PropLetHeap (AnalLet \<Delta> body a)) \<Delta>)[x::h=y] (transform (PropLetBody (AnalLet \<Delta> body a)) body[x::=y]) = TransLet (AnalLet \<Delta> body a) (map_transform transform (PropLetHeap (AnalLet \<Delta> body a)) \<Delta>[x::h=y]) (transform (PropLetBody (AnalLet \<Delta> body a)) body[x::=y])
[PROOF STEP]
apply (rule fun_cong[OF arg_cong[where f = "TransLet b" for b]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom ` domA \<Delta> \<sharp>* x; atom ` domA \<Delta> \<sharp>* y; \<And>x e a b ba. (x, e) \<in> set \<Delta> \<Longrightarrow> (transform a e)[b::=ba] = transform a e[b::=ba]; \<And>a b ba. (transform a body)[b::=ba] = transform a body[b::=ba]; AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a\<rbrakk> \<Longrightarrow> (map_transform transform (PropLetHeap (AnalLet \<Delta> body a)) \<Delta>)[x::h=y] = map_transform transform (PropLetHeap (AnalLet \<Delta> body a)) \<Delta>[x::h=y]
[PROOF STEP]
apply (rule subst_map_transform)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x' e a. \<lbrakk>atom ` domA \<Delta> \<sharp>* x; atom ` domA \<Delta> \<sharp>* y; \<And>x e a b ba. (x, e) \<in> set \<Delta> \<Longrightarrow> (transform a e)[b::=ba] = transform a e[b::=ba]; \<And>a b ba. (transform a body)[b::=ba] = transform a body[b::=ba]; AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a; (x', e) \<in> set \<Delta>\<rbrakk> \<Longrightarrow> (transform a e)[x::=y] = transform a e[x::=y]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(transform a (Terms.Let \<Delta> body))[x::=y] = transform a (Terms.Let \<Delta> body)[x::=y]

goal (5 subgoals):
 1. \<And>var x y a. (transform a (Var var))[x::=y] = transform a (Var var)[x::=y]
 2. \<And>exp var x y a. (\<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]) \<Longrightarrow> (transform a (App exp var))[x::=y] = transform a (App exp var)[x::=y]
 3. \<And>var exp x y a. \<lbrakk>atom var \<sharp> x; atom var \<sharp> y; \<And>b ba a. (transform a exp)[b::=ba] = transform a exp[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (Lam [var]. exp))[x::=y] = transform a (Lam [var]. exp)[x::=y]
 4. \<And>b x y a. (transform a (Bool b))[x::=y] = transform a (Bool b)[x::=y]
 5. \<And>scrut e1 e2 x y a. \<lbrakk>\<And>b ba a. (transform a scrut)[b::=ba] = transform a scrut[b::=ba]; \<And>b ba a. (transform a e1)[b::=ba] = transform a e1[b::=ba]; \<And>b ba a. (transform a e2)[b::=ba] = transform a e2[b::=ba]\<rbrakk> \<Longrightarrow> (transform a (scrut ? e1 : e2))[x::=y] = transform a (scrut ? e1 : e2)[x::=y]
[PROOF STEP]
qed (simp_all add: TransVar_subst TransApp_subst TransLam_subst)


[STATEMENT]
lemma isLam_transform[simp]:
    "isLam (transform a e) \<longleftrightarrow> isLam e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isLam (transform a e) = isLam e
[PROOF STEP]
by (induction e rule:isLam.induct) auto


[STATEMENT]
lemma isVal_transform[simp]:
    "isVal (transform a e) \<longleftrightarrow> isVal e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isVal (transform a e) = isVal e
[PROOF STEP]
by (induction e rule:isLam.induct) auto


[STATEMENT]
lemma Rep_account_zero [simp]: "\<pi> 0 = (\<lambda> _ . 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> 0 = (\<lambda>_. 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> 0 = (\<lambda>_. 0)
[PROOF STEP]
have "(\<lambda> _ . 0) \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. 0::'b) \<in> fin_support (0::'b) UNIV
[PROOF STEP]
unfolding fin_support_def support_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. 0::'b) \<in> {f. finite {x \<in> UNIV. f x \<noteq> (0::'b)}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>_. 0::?'b1) \<in> fin_support (0::?'b1) UNIV

goal (1 subgoal):
 1. \<pi> 0 = (\<lambda>_. 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>_. 0::?'b1) \<in> fin_support (0::?'b1) UNIV

goal (1 subgoal):
 1. \<pi> 0 = (\<lambda>_. 0)
[PROOF STEP]
unfolding zero_account_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>_. 0::?'b1) \<in> fin_support (0::?'b1) UNIV

goal (1 subgoal):
 1. \<pi> (\<iota> (\<lambda>_. 0)) = (\<lambda>_. 0)
[PROOF STEP]
using Abs_account_inverse
[PROOF STATE]
proof (prove)
using this:
(\<lambda>_. 0::?'b1) \<in> fin_support (0::?'b1) UNIV
?y \<in> fin_support 0 UNIV \<Longrightarrow> \<pi> (\<iota> ?y) = ?y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Rep_account_uminus [simp]:
  "\<pi> (- \<alpha>) = (\<lambda> n . - \<pi> \<alpha> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (- \<alpha>) = (\<lambda>n. - \<pi> \<alpha> n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> (- \<alpha>) = (\<lambda>n. - \<pi> \<alpha> n)
[PROOF STEP]
have "\<pi> \<alpha> \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<alpha> \<in> fin_support 0 UNIV
[PROOF STEP]
using Rep_account
[PROOF STATE]
proof (prove)
using this:
\<pi> ?x \<in> fin_support 0 UNIV

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

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

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

goal (1 subgoal):
 1. (\<lambda>x. - \<pi> \<alpha> x) \<in> {f. finite {x \<in> UNIV. f x \<noteq> 0}}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>x. - \<pi> \<alpha> x) \<in> fin_support 0 UNIV

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

goal (1 subgoal):
 1. \<pi> (- \<alpha>) = (\<lambda>n. - \<pi> \<alpha> n)
[PROOF STEP]
unfolding uminus_account_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. - \<pi> \<alpha> x) \<in> fin_support 0 UNIV

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fin_support_closed_under_addition:
  fixes f g :: "'a \<Rightarrow> real"
  assumes "f \<in> fin_support 0 A"
  and "g \<in> fin_support 0 A"
  shows "(\<lambda> x . f x + g x) \<in> fin_support 0 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x + g x) \<in> fin_support 0 A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> fin_support 0 A
g \<in> fin_support 0 A

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) \<in> fin_support 0 A
[PROOF STEP]
unfolding fin_support_def support_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f. finite {x \<in> A. f x \<noteq> 0}}
g \<in> {f. finite {x \<in> A. f x \<noteq> 0}}

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) \<in> {f. finite {x \<in> A. f x \<noteq> 0}}
[PROOF STEP]
by (metis (mono_tags) mem_Collect_eq sum.finite_Collect_op)


[STATEMENT]
lemma Rep_account_plus [simp]:
  "\<pi> (\<alpha>\<^sub>1 + \<alpha>\<^sub>2) = (\<lambda> n. \<pi> \<alpha>\<^sub>1 n + \<pi> \<alpha>\<^sub>2 n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<alpha>\<^sub>1 + \<alpha>\<^sub>2) = (\<lambda>n. \<pi> \<alpha>\<^sub>1 n + \<pi> \<alpha>\<^sub>2 n)
[PROOF STEP]
unfolding plus_account_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (\<iota> (\<lambda>n. \<pi> \<alpha>\<^sub>1 n + \<pi> \<alpha>\<^sub>2 n)) = (\<lambda>n. \<pi> \<alpha>\<^sub>1 n + \<pi> \<alpha>\<^sub>2 n)
[PROOF STEP]
by (metis (full_types)
        Abs_account_cases
        Abs_account_inverse
        fin_support_closed_under_addition)


[STATEMENT]
lemma additive_strictly_solvent:
  assumes "strictly_solvent \<alpha>\<^sub>1" and "strictly_solvent \<alpha>\<^sub>2"
  shows "strictly_solvent (\<alpha>\<^sub>1 + \<alpha>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent (\<alpha>\<^sub>1 + \<alpha>\<^sub>2)
[PROOF STEP]
using assms Rep_account_plus
[PROOF STATE]
proof (prove)
using this:
strictly_solvent \<alpha>\<^sub>1
strictly_solvent \<alpha>\<^sub>2
\<pi> (?\<alpha>\<^sub>1 + ?\<alpha>\<^sub>2) = (\<lambda>n. \<pi> ?\<alpha>\<^sub>1 n + \<pi> ?\<alpha>\<^sub>2 n)

goal (1 subgoal):
 1. strictly_solvent (\<alpha>\<^sub>1 + \<alpha>\<^sub>2)
[PROOF STEP]
unfolding strictly_solvent_def plus_account_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 \<le> sum (\<pi> \<alpha>\<^sub>1) {..n}
\<forall>n. 0 \<le> sum (\<pi> \<alpha>\<^sub>2) {..n}
\<pi> (\<iota> (\<lambda>n. \<pi> ?\<alpha>\<^sub>1 n + \<pi> ?\<alpha>\<^sub>2 n)) = (\<lambda>n. \<pi> ?\<alpha>\<^sub>1 n + \<pi> ?\<alpha>\<^sub>2 n)

goal (1 subgoal):
 1. \<forall>n. 0 \<le> sum (\<pi> (\<iota> (\<lambda>n. \<pi> \<alpha>\<^sub>1 n + \<pi> \<alpha>\<^sub>2 n))) {..n}
[PROOF STEP]
by (simp add: Abs_account_inverse sum.distrib)


[STATEMENT]
lemma strictly_solvent_alt_def: "strictly_solvent \<alpha> = (0 \<le> \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent \<alpha> = (0 \<le> \<alpha>)
[PROOF STEP]
unfolding
    strictly_solvent_def
    less_eq_account_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}) = (\<forall>n. sum (\<pi> 0) {..n} \<le> sum (\<pi> \<alpha>) {..n})
[PROOF STEP]
using zero_account_def
[PROOF STATE]
proof (prove)
using this:
0 = \<iota> (\<lambda>_. 0)

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


[STATEMENT]
lemma strictly_solvent_non_negative_cash:
  assumes "strictly_solvent \<alpha>"
  shows "0 \<le> cash_reserve \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> cash_reserve \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
strictly_solvent \<alpha>

goal (1 subgoal):
 1. 0 \<le> cash_reserve \<alpha>
[PROOF STEP]
unfolding strictly_solvent_def cash_reserve_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 \<le> sum (\<pi> \<alpha>) {..n}

goal (1 subgoal):
 1. 0 \<le> \<pi> \<alpha> 0
[PROOF STEP]
by (metis
        atMost_0
        empty_iff
        finite.emptyI
        group_cancel.rule0
        sum.empty
        sum.insert)


[STATEMENT]
lemma Rep_account_just_cash [simp]:
  "\<pi> (just_cash c) = (\<lambda> n . if n = 0 then c else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
proof(cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
 2. c \<noteq> 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
 2. c \<noteq> 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
hence "just_cash c = 0"
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. just_cash c = 0
[PROOF STEP]
unfolding just_cash_def zero_account_def
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. \<iota> (\<lambda>n. if n = 0 then c else 0) = \<iota> (\<lambda>_. 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
just_cash c = 0

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

goal (1 subgoal):
 1. \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
using Rep_account_zero True
[PROOF STATE]
proof (prove)
using this:
just_cash c = 0
\<pi> 0 = (\<lambda>_. 0)
c = 0

goal (1 subgoal):
 1. \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
hence "finite (support 0 UNIV (\<lambda> n :: nat . if n = 0 then c else 0))"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. finite (support 0 UNIV (\<lambda>n. if n = 0 then c else 0))
[PROOF STEP]
unfolding support_def
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. finite {x \<in> UNIV. (if x = 0 then c else 0) \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (support 0 UNIV (\<lambda>n. if n = 0 then c else 0))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
hence "(\<lambda> n :: nat . if n = 0 then c else 0) \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
using this:
finite (support 0 UNIV (\<lambda>n. if n = 0 then c else 0))

goal (1 subgoal):
 1. (\<lambda>n. if n = 0 then c else 0) \<in> fin_support 0 UNIV
[PROOF STEP]
unfolding fin_support_def
[PROOF STATE]
proof (prove)
using this:
finite (support 0 UNIV (\<lambda>n. if n = 0 then c else 0))

goal (1 subgoal):
 1. (\<lambda>n. if n = 0 then c else 0) \<in> {f. finite (support 0 UNIV f)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. if n = 0 then c else 0) \<in> fin_support 0 UNIV

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<pi> (just_cash c) = (\<lambda>n. if n = 0 then c else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. if n = 0 then c else 0) \<in> fin_support 0 UNIV
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. if n = 0 then c else 0) \<in> fin_support 0 UNIV

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma balanced_strictly_solvent:
  assumes "0 \<le> c" and "balanced \<L> c"
  shows "strictly_solvent (\<Sum> a \<in> UNIV. \<L> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent (sum \<L> UNIV)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
balanced \<L> c

goal (1 subgoal):
 1. strictly_solvent (sum \<L> UNIV)
[PROOF STEP]
unfolding balanced_def strictly_solvent_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
sum \<L> UNIV = just_cash c

goal (1 subgoal):
 1. \<forall>n. 0 \<le> sum (\<pi> (sum \<L> UNIV)) {..n}
[PROOF STEP]
by simp


[STATEMENT]
lemma (in finite) finite_Rep_account_ledger [simp]:
  "\<pi> (\<Sum> a \<in> (A :: 'a set). \<L> a) n = (\<Sum> a \<in> A. \<pi> (\<L> a) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (sum \<L> A) n = (\<Sum>a\<in>A. \<pi> (\<L> a) n)
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
finite ?A

goal (1 subgoal):
 1. \<pi> (sum \<L> A) n = (\<Sum>a\<in>A. \<pi> (\<L> a) n)
[PROOF STEP]
by (induct A rule: finite_induct, auto)


[STATEMENT]
lemma (in finite) balanced_alt_def:
  "balanced \<L> c =
     ((\<Sum> a \<in> UNIV. cash_reserve (\<L> a)) = c
      \<and> (\<forall> n > 0. (\<Sum> a \<in> UNIV. \<pi> (\<L> a) n) = 0))"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. balanced \<L> c = ((\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0))
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
balanced \<L> c

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
hence "(\<Sum> a \<in> UNIV. cash_reserve (\<L> a)) = c"
[PROOF STATE]
proof (prove)
using this:
balanced \<L> c

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c
[PROOF STEP]
unfolding balanced_def cash_reserve_def
[PROOF STATE]
proof (prove)
using this:
sum \<L> UNIV = just_cash c

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) 0) = c
[PROOF STEP]
by (metis Rep_account_just_cash finite_Rep_account_ledger)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
fix n :: "nat"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume "n > 0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
with \<open>?lhs\<close>
[PROOF STATE]
proof (chain)
picking this:
balanced \<L> c
0 < n
[PROOF STEP]
have "(\<Sum> a \<in> UNIV. \<pi> (\<L> a) n) = 0"
[PROOF STATE]
proof (prove)
using this:
balanced \<L> c
0 < n

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
unfolding balanced_def
[PROOF STATE]
proof (prove)
using this:
sum \<L> UNIV = just_cash c
0 < n

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0
[PROOF STEP]
by (metis
            Rep_account_just_cash
            less_nat_zero_code
            finite_Rep_account_ledger)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < ?n2 \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) ?n2) = 0

goal (2 subgoals):
 1. balanced \<L> c \<Longrightarrow> (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
 2. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c
0 < ?n2 \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) ?n2) = 0
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c
0 < ?n2 \<Longrightarrow> (\<Sum>a\<in>UNIV. \<pi> (\<L> a) ?n2) = 0

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "cash_reserve (just_cash c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cash_reserve (just_cash c) = c
[PROOF STEP]
unfolding cash_reserve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (just_cash c) 0 = c
[PROOF STEP]
using Rep_account_just_cash
[PROOF STATE]
proof (prove)
using this:
\<pi> (just_cash ?c) = (\<lambda>n. if n = 0 then ?c else 0)

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

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cash_reserve (just_cash c) = c

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
have "... = (\<Sum>a\<in>UNIV. cash_reserve (\<L> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (\<Sum>a\<in>UNIV. cash_reserve (\<L> a))
[PROOF STEP]
using \<open>?rhs\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)

goal (1 subgoal):
 1. c = (\<Sum>a\<in>UNIV. cash_reserve (\<L> a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c = (\<Sum>a\<in>UNIV. cash_reserve (\<L> a))

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cash_reserve (just_cash c) = (\<Sum>a\<in>UNIV. cash_reserve (\<L> a))
[PROOF STEP]
have
    "cash_reserve (\<Sum> a \<in> UNIV. \<L> a) = cash_reserve (just_cash c)"
[PROOF STATE]
proof (prove)
using this:
cash_reserve (just_cash c) = (\<Sum>a\<in>UNIV. cash_reserve (\<L> a))

goal (1 subgoal):
 1. cash_reserve (sum \<L> UNIV) = cash_reserve (just_cash c)
[PROOF STEP]
unfolding cash_reserve_def
[PROOF STATE]
proof (prove)
using this:
\<pi> (just_cash c) 0 = (\<Sum>a\<in>UNIV. \<pi> (\<L> a) 0)

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

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cash_reserve (sum \<L> UNIV) = cash_reserve (just_cash c)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
cash_reserve (sum \<L> UNIV) = cash_reserve (just_cash c)

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
fix n :: "nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
assume "n > 0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
hence "\<pi> (\<Sum> a \<in> UNIV. \<L> a) n = 0"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. \<pi> (sum \<L> UNIV) n = 0
[PROOF STEP]
using \<open>?rhs\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n
(\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0)

goal (1 subgoal):
 1. \<pi> (sum \<L> UNIV) n = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (sum \<L> UNIV) n = 0

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
hence "\<pi> (\<Sum> a \<in> UNIV. \<L> a) n = \<pi> (just_cash c) n"
[PROOF STATE]
proof (prove)
using this:
\<pi> (sum \<L> UNIV) n = 0

goal (1 subgoal):
 1. \<pi> (sum \<L> UNIV) n = \<pi> (just_cash c) n
[PROOF STEP]
unfolding Rep_account_just_cash
[PROOF STATE]
proof (prove)
using this:
\<pi> (sum \<L> UNIV) n = 0

goal (1 subgoal):
 1. \<pi> (sum \<L> UNIV) n = (if n = 0 then c else 0)
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (sum \<L> UNIV) n = 0
0 < n

goal (1 subgoal):
 1. \<pi> (sum \<L> UNIV) n = (if n = 0 then c else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (sum \<L> UNIV) n = \<pi> (just_cash c) n

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < ?n2 \<Longrightarrow> \<pi> (sum \<L> UNIV) ?n2 = \<pi> (just_cash c) ?n2

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cash_reserve (sum \<L> UNIV) = cash_reserve (just_cash c)
0 < ?n2 \<Longrightarrow> \<pi> (sum \<L> UNIV) ?n2 = \<pi> (just_cash c) ?n2
[PROOF STEP]
have
    "\<forall> n . \<pi> (\<Sum> a \<in> UNIV. \<L> a) n = \<pi> (just_cash c) n"
[PROOF STATE]
proof (prove)
using this:
cash_reserve (sum \<L> UNIV) = cash_reserve (just_cash c)
0 < ?n2 \<Longrightarrow> \<pi> (sum \<L> UNIV) ?n2 = \<pi> (just_cash c) ?n2

goal (1 subgoal):
 1. \<forall>n. \<pi> (sum \<L> UNIV) n = \<pi> (just_cash c) n
[PROOF STEP]
unfolding cash_reserve_def
[PROOF STATE]
proof (prove)
using this:
\<pi> (sum \<L> UNIV) 0 = \<pi> (just_cash c) 0
0 < ?n2 \<Longrightarrow> \<pi> (sum \<L> UNIV) ?n2 = \<pi> (just_cash c) ?n2

goal (1 subgoal):
 1. \<forall>n. \<pi> (sum \<L> UNIV) n = \<pi> (just_cash c) n
[PROOF STEP]
by (metis gr_zeroI)
[PROOF STATE]
proof (state)
this:
\<forall>n. \<pi> (sum \<L> UNIV) n = \<pi> (just_cash c) n

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
hence "\<pi> (\<Sum> a \<in> UNIV. \<L> a) = \<pi> (just_cash c)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<pi> (sum \<L> UNIV) n = \<pi> (just_cash c) n

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

goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV. cash_reserve (\<L> a)) = c \<and> (\<forall>n>0. (\<Sum>a\<in>UNIV. \<pi> (\<L> a) n) = 0) \<Longrightarrow> balanced \<L> c
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
\<pi> (sum \<L> UNIV) = \<pi> (just_cash c)

goal (1 subgoal):
 1. balanced \<L> c
[PROOF STEP]
unfolding balanced_def
[PROOF STATE]
proof (prove)
using this:
\<pi> (sum \<L> UNIV) = \<pi> (just_cash c)

goal (1 subgoal):
 1. sum \<L> UNIV = just_cash c
[PROOF STEP]
using Rep_account_inject
[PROOF STATE]
proof (prove)
using this:
\<pi> (sum \<L> UNIV) = \<pi> (just_cash c)
(\<pi> ?x = \<pi> ?y) = (?x = ?y)

goal (1 subgoal):
 1. sum \<L> UNIV = just_cash c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
balanced \<L> c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_collapse:
  "transfer \<L> \<tau> a a = \<L>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transfer \<L> \<tau> a a = \<L>
[PROOF STEP]
unfolding transfer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if a = a then \<L> x else if x = a then \<L> a - \<tau> else if x = a then \<L> a + \<tau> else \<L> x) = \<L>
[PROOF STEP]
by auto


[STATEMENT]
lemma (in finite) sum_transfer_equiv:
  fixes x y :: "'a"
  shows "(\<Sum> a \<in> UNIV. \<L> a) = (\<Sum> a \<in> UNIV. transfer \<L> \<tau> x y a)"
  (is "_ = (\<Sum> a \<in> UNIV. ?\<L>' a)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
 2. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

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

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
let ?sum_\<L> = "(\<Sum> a \<in> UNIV - {x,y}. \<L> a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
let ?sum_\<L>' = "(\<Sum> a \<in> UNIV - {x,y}. ?\<L>' a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "\<forall> a \<in> UNIV - {x,y}. ?\<L>' a = \<L> a "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>UNIV - {x, y}. transfer \<L> \<tau> x y a = \<L> a
[PROOF STEP]
by (simp add: transfer_def)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>UNIV - {x, y}. transfer \<L> \<tau> x y a = \<L> a

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
hence "?sum_\<L>' = ?sum_\<L>"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>UNIV - {x, y}. transfer \<L> \<tau> x y a = \<L> a

goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) = sum \<L> (UNIV - {x, y})
[PROOF STEP]
by (meson sum.cong)
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) = sum \<L> (UNIV - {x, y})

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "{x,y} \<subseteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} \<subseteq> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x, y} \<subseteq> UNIV

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "(\<Sum> a \<in> UNIV. ?\<L>' a) = ?sum_\<L>' + (\<Sum> a \<in> {x,y}. ?\<L>' a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) UNIV = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y}
[PROOF STEP]
using finite_UNIV sum.subset_diff [OF \<open>{x,y} \<subseteq> UNIV\<close>]
[PROOF STATE]
proof (prove)
using this:
finite UNIV
finite UNIV \<Longrightarrow> sum ?g UNIV = sum ?g (UNIV - {x, y}) + sum ?g {x, y}

goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) UNIV = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) UNIV = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y}

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) UNIV = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y}

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "... = ?sum_\<L>' + ?\<L>' x + ?\<L>' y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y} = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + transfer \<L> \<tau> x y x + transfer \<L> \<tau> x y y
[PROOF STEP]
using
      \<open>x \<noteq> y\<close>
      finite
      Diff_empty
      Diff_insert_absorb
      Diff_subset
      group_cancel.add1
      insert_absorb
      sum.subset_diff
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
finite ?A
?A - {} = ?A
?x \<notin> ?A \<Longrightarrow> insert ?x ?A - {?x} = ?A
?A - ?B \<subseteq> ?A
?A \<equiv> ?k + ?a \<Longrightarrow> ?A + ?b \<equiv> ?k + (?a + ?b)
?a \<in> ?A \<Longrightarrow> insert ?a ?A = ?A
\<lbrakk>?B \<subseteq> ?A; finite ?A\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?g (?A - ?B) + sum ?g ?B

goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y} = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + transfer \<L> \<tau> x y x + transfer \<L> \<tau> x y y
[PROOF STEP]
by (simp add: insert_Diff_if)
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y} = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + transfer \<L> \<tau> x y x + transfer \<L> \<tau> x y y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + sum (transfer \<L> \<tau> x y) {x, y} = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + transfer \<L> \<tau> x y x + transfer \<L> \<tau> x y y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "... = ?sum_\<L>' + \<L> x - \<tau> + \<L> y + \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + transfer \<L> \<tau> x y x + transfer \<L> \<tau> x y y = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x - \<tau> + \<L> y + \<tau>
[PROOF STEP]
unfolding transfer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>UNIV - {x, y}. if x = y then \<L> a else if a = x then \<L> x - \<tau> else if a = y then \<L> y + \<tau> else \<L> a) + (if x = y then \<L> x else if x = x then \<L> x - \<tau> else if x = y then \<L> y + \<tau> else \<L> x) + (if x = y then \<L> y else if y = x then \<L> x - \<tau> else if y = y then \<L> y + \<tau> else \<L> y) = (\<Sum>a\<in>UNIV - {x, y}. if x = y then \<L> a else if a = x then \<L> x - \<tau> else if a = y then \<L> y + \<tau> else \<L> a) + \<L> x - \<tau> + \<L> y + \<tau>
[PROOF STEP]
using \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

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

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + transfer \<L> \<tau> x y x + transfer \<L> \<tau> x y y = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x - \<tau> + \<L> y + \<tau>

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "... = ?sum_\<L>' + \<L> x + \<L> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x - \<tau> + \<L> y + \<tau> = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x + \<L> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x - \<tau> + \<L> y + \<tau> = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x + \<L> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x - \<tau> + \<L> y + \<tau> = sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x + \<L> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "... = ?sum_\<L> + \<L> x + \<L> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y
[PROOF STEP]
unfolding \<open>?sum_\<L>' = ?sum_\<L>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (transfer \<L> \<tau> x y) (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
have "... = ?sum_\<L> + (\<Sum> a \<in> {x,y}. \<L> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + sum \<L> {x, y}
[PROOF STEP]
using
      \<open>x \<noteq> y\<close>
      finite
      Diff_empty
      Diff_insert_absorb
      Diff_subset
      group_cancel.add1
      insert_absorb
      sum.subset_diff
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
finite ?A
?A - {} = ?A
?x \<notin> ?A \<Longrightarrow> insert ?x ?A - {?x} = ?A
?A - ?B \<subseteq> ?A
?A \<equiv> ?k + ?a \<Longrightarrow> ?A + ?b \<equiv> ?k + (?a + ?b)
?a \<in> ?A \<Longrightarrow> insert ?a ?A = ?A
\<lbrakk>?B \<subseteq> ?A; finite ?A\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?g (?A - ?B) + sum ?g ?B

goal (1 subgoal):
 1. sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + sum \<L> {x, y}
[PROOF STEP]
by (simp add: insert_Diff_if)
[PROOF STATE]
proof (state)
this:
sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + sum \<L> {x, y}

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum (transfer \<L> \<tau> x y) UNIV = sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y
sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + sum \<L> {x, y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (transfer \<L> \<tau> x y) UNIV = sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y
sum \<L> (UNIV - {x, y}) + \<L> x + \<L> y = sum \<L> (UNIV - {x, y}) + sum \<L> {x, y}

goal (1 subgoal):
 1. sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV
[PROOF STEP]
by (metis local.finite sum.subset_diff top_greatest)
[PROOF STATE]
proof (state)
this:
sum \<L> UNIV = sum (transfer \<L> \<tau> x y) UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in finite) balanced_transfer:
  "balanced \<L> c = balanced (transfer \<L> \<tau> a b) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. balanced \<L> c = balanced (transfer \<L> \<tau> a b) c
[PROOF STEP]
unfolding balanced_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum \<L> UNIV = just_cash c) = (sum (transfer \<L> \<tau> a b) UNIV = just_cash c)
[PROOF STEP]
using sum_transfer_equiv
[PROOF STATE]
proof (prove)
using this:
sum ?\<L> UNIV = sum (transfer ?\<L> ?\<tau> ?x ?y) UNIV

goal (1 subgoal):
 1. (sum \<L> UNIV = just_cash c) = (sum (transfer \<L> \<tau> a b) UNIV = just_cash c)
[PROOF STEP]
by force


[STATEMENT]
lemma (in finite) strictly_solvent_transfer:
  fixes x y :: "'a"
  shows "strictly_solvent (\<Sum> a \<in> UNIV. \<L> a) =
           strictly_solvent (\<Sum> a \<in> UNIV. transfer \<L> \<tau> x y a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent (sum \<L> UNIV) = strictly_solvent (sum (transfer \<L> \<tau> x y) UNIV)
[PROOF STEP]
using sum_transfer_equiv
[PROOF STATE]
proof (prove)
using this:
sum ?\<L> UNIV = sum (transfer ?\<L> ?\<tau> ?x ?y) UNIV

goal (1 subgoal):
 1. strictly_solvent (sum \<L> UNIV) = strictly_solvent (sum (transfer \<L> \<tau> x y) UNIV)
[PROOF STEP]
by presburger


[STATEMENT]
lemma valid_transfer_alt_def: "valid_transfer \<alpha> \<tau> = (0 \<le> \<tau> \<and> \<tau> \<le> \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_transfer \<alpha> \<tau> = (0 \<le> \<tau> \<and> \<tau> \<le> \<alpha>)
[PROOF STEP]
unfolding valid_transfer_def strictly_solvent_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> \<tau> \<and> 0 \<le> \<alpha> - \<tau>) = (0 \<le> \<tau> \<and> \<tau> \<le> \<alpha>)
[PROOF STEP]
by simp


[STATEMENT]
lemma only_strictly_solvent_accounts_can_transfer:
  assumes "valid_transfer \<alpha> \<tau>"
  shows "strictly_solvent \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
valid_transfer \<alpha> \<tau>

goal (1 subgoal):
 1. strictly_solvent \<alpha>
[PROOF STEP]
unfolding strictly_solvent_alt_def valid_transfer_alt_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<tau> \<and> \<tau> \<le> \<alpha>

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


[STATEMENT]
theorem strictly_solvent_still_strictly_solvent_after_valid_transfer:
  assumes "valid_transfer (\<L> a) \<tau>"
  and "strictly_solvent (\<L> b)"
  shows
    "strictly_solvent ((transfer \<L> \<tau> a b) a)"
    "strictly_solvent ((transfer \<L> \<tau> a b) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent (transfer \<L> \<tau> a b a) &&& strictly_solvent (transfer \<L> \<tau> a b b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
valid_transfer (\<L> a) \<tau>
strictly_solvent (\<L> b)

goal (1 subgoal):
 1. strictly_solvent (transfer \<L> \<tau> a b a) &&& strictly_solvent (transfer \<L> \<tau> a b b)
[PROOF STEP]
unfolding
    strictly_solvent_alt_def
    valid_transfer_alt_def
    transfer_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<tau> \<and> \<tau> \<le> \<L> a
0 \<le> \<L> b

goal (1 subgoal):
 1. 0 \<le> (if a = b then \<L> a else if a = a then \<L> a - \<tau> else if a = b then \<L> b + \<tau> else \<L> a) &&& 0 \<le> (if a = b then \<L> b else if b = a then \<L> a - \<tau> else if b = b then \<L> b + \<tau> else \<L> b)
[PROOF STEP]
by (cases "a = b", auto)


[STATEMENT]
lemma strictly_solvent_just_cash_equiv:
  "strictly_solvent (just_cash c) = (0 \<le> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_solvent (just_cash c) = (0 \<le> c)
[PROOF STEP]
unfolding strictly_solvent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n. 0 \<le> sum (\<pi> (just_cash c)) {..n}) = (0 \<le> c)
[PROOF STEP]
using Rep_account_just_cash just_cash_def
[PROOF STATE]
proof (prove)
using this:
\<pi> (just_cash ?c) = (\<lambda>n. if n = 0 then ?c else 0)
just_cash ?c = \<iota> (\<lambda>n. if n = 0 then ?c else 0)

goal (1 subgoal):
 1. (\<forall>n. 0 \<le> sum (\<pi> (just_cash c)) {..n}) = (0 \<le> c)
[PROOF STEP]
by force


[STATEMENT]
lemma zero_account_alt_def: "just_cash 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash 0 = 0
[PROOF STEP]
unfolding zero_account_def just_cash_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> (\<lambda>n. if n = 0 then 0 else 0) = \<iota> (\<lambda>_. 0)
[PROOF STEP]
by simp


[STATEMENT]
lemma just_cash_embed: "(a = b) = (just_cash a = just_cash b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a = b) = (just_cash a = just_cash b)
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = b \<Longrightarrow> just_cash a = just_cash b
 2. just_cash a = just_cash b \<Longrightarrow> a = b
[PROOF STEP]
assume "a = b"
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. a = b \<Longrightarrow> just_cash a = just_cash b
 2. just_cash a = just_cash b \<Longrightarrow> a = b
[PROOF STEP]
thus "just_cash a = just_cash b"
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. just_cash a = just_cash b
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
just_cash a = just_cash b

goal (1 subgoal):
 1. just_cash a = just_cash b \<Longrightarrow> a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. just_cash a = just_cash b \<Longrightarrow> a = b
[PROOF STEP]
assume "just_cash a = just_cash b"
[PROOF STATE]
proof (state)
this:
just_cash a = just_cash b

goal (1 subgoal):
 1. just_cash a = just_cash b \<Longrightarrow> a = b
[PROOF STEP]
hence "cash_reserve (just_cash a) = cash_reserve (just_cash b)"
[PROOF STATE]
proof (prove)
using this:
just_cash a = just_cash b

goal (1 subgoal):
 1. cash_reserve (just_cash a) = cash_reserve (just_cash b)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
cash_reserve (just_cash a) = cash_reserve (just_cash b)

goal (1 subgoal):
 1. just_cash a = just_cash b \<Longrightarrow> a = b
[PROOF STEP]
thus "a = b"
[PROOF STATE]
proof (prove)
using this:
cash_reserve (just_cash a) = cash_reserve (just_cash b)

goal (1 subgoal):
 1. a = b
[PROOF STEP]
unfolding Rep_account_just_cash cash_reserve_def
[PROOF STATE]
proof (prove)
using this:
(if 0 = 0 then a else 0) = (if 0 = 0 then b else 0)

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partial_nav_just_cash [simp]:
 "(\<Sum> i\<le>n . \<pi> (just_cash a) i) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (\<pi> (just_cash a)) {..n} = a
[PROOF STEP]
unfolding Rep_account_just_cash
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>n. if i = 0 then a else 0) = a
[PROOF STEP]
by (induct n, auto)


[STATEMENT]
lemma just_cash_order_embed: "(a \<le> b) = (just_cash a \<le> just_cash b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b) = (just_cash a \<le> just_cash b)
[PROOF STEP]
unfolding less_eq_account_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b) = (\<forall>n. sum (\<pi> (just_cash a)) {..n} \<le> sum (\<pi> (just_cash b)) {..n})
[PROOF STEP]
by simp


[STATEMENT]
lemma just_cash_plus [simp]: "just_cash a + just_cash b = just_cash (a + b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
have "\<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
 2. x \<noteq> 0 \<Longrightarrow> \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
 2. x \<noteq> 0 \<Longrightarrow> \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
using Rep_account_just_cash just_cash_def
[PROOF STATE]
proof (prove)
using this:
x = 0
\<pi> (just_cash ?c) = (\<lambda>n. if n = 0 then ?c else 0)
just_cash ?c = \<iota> (\<lambda>n. if n = 0 then ?c else 0)

goal (1 subgoal):
 1. \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. \<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> (just_cash a + just_cash b) x = \<pi> (just_cash (a + b)) x

goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<pi> (just_cash a + just_cash b) ?x2 = \<pi> (just_cash (a + b)) ?x2

goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
hence "\<pi> (just_cash a + just_cash b) = \<pi> (just_cash (a + b))"
[PROOF STATE]
proof (prove)
using this:
\<pi> (just_cash a + just_cash b) ?x2 = \<pi> (just_cash (a + b)) ?x2

goal (1 subgoal):
 1. \<pi> (just_cash a + just_cash b) = \<pi> (just_cash (a + b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (just_cash a + just_cash b) = \<pi> (just_cash (a + b))

goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> (just_cash a + just_cash b) = \<pi> (just_cash (a + b))

goal (1 subgoal):
 1. just_cash a + just_cash b = just_cash (a + b)
[PROOF STEP]
by (metis Rep_account_inverse)
[PROOF STATE]
proof (state)
this:
just_cash a + just_cash b = just_cash (a + b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma just_cash_uminus [simp]: "- just_cash a = just_cash (- a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
have "\<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
 2. x \<noteq> 0 \<Longrightarrow> \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
 2. x \<noteq> 0 \<Longrightarrow> \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
using Rep_account_just_cash just_cash_def
[PROOF STATE]
proof (prove)
using this:
x = 0
\<pi> (just_cash ?c) = (\<lambda>n. if n = 0 then ?c else 0)
just_cash ?c = \<iota> (\<lambda>n. if n = 0 then ?c else 0)

goal (1 subgoal):
 1. \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. \<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> (- just_cash a) x = \<pi> (just_cash (- a)) x

goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<pi> (- just_cash a) ?x2 = \<pi> (just_cash (- a)) ?x2

goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
hence "\<pi> (- just_cash a) = \<pi> (just_cash (- a))"
[PROOF STATE]
proof (prove)
using this:
\<pi> (- just_cash a) ?x2 = \<pi> (just_cash (- a)) ?x2

goal (1 subgoal):
 1. \<pi> (- just_cash a) = \<pi> (just_cash (- a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (- just_cash a) = \<pi> (just_cash (- a))

goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> (- just_cash a) = \<pi> (just_cash (- a))

goal (1 subgoal):
 1. - just_cash a = just_cash (- a)
[PROOF STEP]
by (metis Rep_account_inverse)
[PROOF STATE]
proof (state)
this:
- just_cash a = just_cash (- a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma just_cash_subtract [simp]:
  "just_cash a - just_cash b = just_cash (a - b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. just_cash a - just_cash b = just_cash (a - b)
[PROOF STEP]
by (simp add: minus_account_def)


[STATEMENT]
lemma just_cash_valid_transfer:
  "valid_transfer (just_cash c) (just_cash t) = ((0 :: real) \<le> t \<and> t \<le> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_transfer (just_cash c) (just_cash t) = (0 \<le> t \<and> t \<le> c)
[PROOF STEP]
unfolding valid_transfer_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> just_cash t \<and> just_cash t \<le> just_cash c) = (0 \<le> t \<and> t \<le> c)
[PROOF STEP]
by (simp add: less_eq_account_def)


[STATEMENT]
lemma (in finite) just_cash_summation:
  fixes A :: "'a set"
  assumes "\<forall> a \<in> A. \<exists> c . \<L> a = just_cash c"
  shows "\<exists> c . (\<Sum> a \<in> A . \<L> a) = just_cash c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. sum \<L> A = just_cash c
[PROOF STEP]
using finite assms
[PROOF STATE]
proof (prove)
using this:
finite ?A
\<forall>a\<in>A. \<exists>c. \<L> a = just_cash c

goal (1 subgoal):
 1. \<exists>c. sum \<L> A = just_cash c
[PROOF STEP]
by (induct A rule: finite_induct, auto, metis zero_account_alt_def)


[STATEMENT]
lemma (in finite) just_cash_UNIV_is_balanced:
  assumes "\<forall> a . \<exists> c . \<L> a = just_cash c"
  shows "\<exists> c . balanced \<L> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. balanced \<L> c
[PROOF STEP]
unfolding balanced_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. sum \<L> UNIV = just_cash c
[PROOF STEP]
using
      assms
      just_cash_summation [where A=UNIV]
[PROOF STATE]
proof (prove)
using this:
\<forall>a. \<exists>c. \<L> a = just_cash c
\<forall>a\<in>UNIV. \<exists>c. ?\<L> a = just_cash c \<Longrightarrow> \<exists>c. sum ?\<L> UNIV = just_cash c

goal (1 subgoal):
 1. \<exists>c. sum \<L> UNIV = just_cash c
[PROOF STEP]
by simp


[STATEMENT]
lemma shortest_period_uminus:
  "shortest_period (- \<alpha>) = shortest_period \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period (- \<alpha>) = shortest_period \<alpha>
[PROOF STEP]
unfolding shortest_period_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<forall>i. \<pi> (- \<alpha>) i = 0 then 0 else Max {i. \<pi> (- \<alpha>) i \<noteq> 0}) = (if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0})
[PROOF STEP]
using Rep_account_uminus uminus_account_def
[PROOF STATE]
proof (prove)
using this:
\<pi> (- ?\<alpha>) = (\<lambda>n. - \<pi> ?\<alpha> n)
- ?\<alpha> = \<iota> (\<lambda>n. - \<pi> ?\<alpha> n)

goal (1 subgoal):
 1. (if \<forall>i. \<pi> (- \<alpha>) i = 0 then 0 else Max {i. \<pi> (- \<alpha>) i \<noteq> 0}) = (if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0})
[PROOF STEP]
by force


[STATEMENT]
lemma finite_account_support:
  "finite {i . \<pi> \<alpha> i \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {i. \<pi> \<alpha> i \<noteq> 0}
[PROOF STEP]
have "\<pi> \<alpha> \<in> fin_support 0 UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<alpha> \<in> fin_support 0 UNIV
[PROOF STEP]
by (simp add: Rep_account)
[PROOF STATE]
proof (state)
this:
\<pi> \<alpha> \<in> fin_support 0 UNIV

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shortest_period_plus:
  "shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)"
  (is "_ \<le> ?MAX")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
proof (cases "\<forall> i . \<pi> (\<alpha> + \<beta>) i = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>i. \<pi> (\<alpha> + \<beta>) i = 0 \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
 2. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0

goal (2 subgoals):
 1. \<forall>i. \<pi> (\<alpha> + \<beta>) i = 0 \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
 2. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0

goal (1 subgoal):
 1. shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
unfolding shortest_period_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0

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

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0)

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
have "shortest_period \<alpha> \<le> ?MAX" and "shortest_period \<beta> \<le> ?MAX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>) &&& shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
have "\<forall> i > shortest_period \<alpha> . \<pi> \<alpha> i = 0"
  and "\<forall> i > shortest_period \<beta> . \<pi> \<beta> i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i>shortest_period \<alpha>. \<pi> \<alpha> i = 0 &&& \<forall>i>shortest_period \<beta>. \<pi> \<beta> i = 0
[PROOF STEP]
unfolding shortest_period_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i>if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0}. \<pi> \<alpha> i = 0 &&& \<forall>i>if \<forall>i. \<pi> \<beta> i = 0 then 0 else Max {i. \<pi> \<beta> i \<noteq> 0}. \<pi> \<beta> i = 0
[PROOF STEP]
using finite_account_support Max.coboundedI leD Collect_cong
[PROOF STATE]
proof (prove)
using this:
finite {i. \<pi> ?\<alpha> i \<noteq> 0}
\<lbrakk>finite ?A; ?a \<in> ?A\<rbrakk> \<Longrightarrow> ?a \<le> Max ?A
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y
(\<And>x. ?P x = ?Q x) \<Longrightarrow> {x. ?P x} = {x. ?Q x}

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

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
\<forall>i>shortest_period \<alpha>. \<pi> \<alpha> i = 0
\<forall>i>shortest_period \<beta>. \<pi> \<beta> i = 0
[PROOF STEP]
have "\<forall> i > ?MAX . \<pi> \<alpha> i = 0"
  and "\<forall> i > ?MAX . \<pi> \<beta> i = 0"
[PROOF STATE]
proof (prove)
using this:
shortest_period \<alpha> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
shortest_period \<beta> \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
\<forall>i>shortest_period \<alpha>. \<pi> \<alpha> i = 0
\<forall>i>shortest_period \<beta>. \<pi> \<beta> i = 0

goal (1 subgoal):
 1. \<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i = 0 &&& \<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<beta> i = 0
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
\<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i = 0
\<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<beta> i = 0

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
hence "\<forall> i > ?MAX . \<pi> (\<alpha> + \<beta>) i = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<alpha> i = 0
\<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> \<beta> i = 0

goal (1 subgoal):
 1. \<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> (\<alpha> + \<beta>) i = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> (\<alpha> + \<beta>) i = 0

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
hence "\<forall> i . \<pi> (\<alpha> + \<beta>) i \<noteq> 0 \<longrightarrow> i \<le> ?MAX"
[PROOF STATE]
proof (prove)
using this:
\<forall>i>max (shortest_period \<alpha>) (shortest_period \<beta>). \<pi> (\<alpha> + \<beta>) i = 0

goal (1 subgoal):
 1. \<forall>i. \<pi> (\<alpha> + \<beta>) i \<noteq> 0 \<longrightarrow> i \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
by (meson not_le)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i \<noteq> 0 \<longrightarrow> i \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)

goal (1 subgoal):
 1. \<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0) \<Longrightarrow> shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i \<noteq> 0 \<longrightarrow> i \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)

goal (1 subgoal):
 1. shortest_period (\<alpha> + \<beta>) \<le> max (shortest_period \<alpha>) (shortest_period \<beta>)
[PROOF STEP]
unfolding shortest_period_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i \<noteq> 0 \<longrightarrow> i \<le> max (if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0}) (if \<forall>i. \<pi> \<beta> i = 0 then 0 else Max {i. \<pi> \<beta> i \<noteq> 0})

goal (1 subgoal):
 1. (if \<forall>i. \<pi> (\<alpha> + \<beta>) i = 0 then 0 else Max {i. \<pi> (\<alpha> + \<beta>) i \<noteq> 0}) \<le> max (if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0}) (if \<forall>i. \<pi> \<beta> i = 0 then 0 else Max {i. \<pi> \<beta> i \<noteq> 0})
[PROOF STEP]
using
      finite_account_support [where \<alpha> = "\<alpha> + \<beta>"]
      False
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi> (\<alpha> + \<beta>) i \<noteq> 0 \<longrightarrow> i \<le> max (if \<forall>i. \<pi> \<alpha> i = 0 then 0 else Max {i. \<pi> \<alpha> i \<noteq> 0}) (if \<forall>i. \<pi> \<beta> i = 0 then 0 else Max {i. \<pi> \<beta> i \<noteq> 0})
finite {i. \<pi> (\<alpha> + \<beta>) i \<noteq> 0}
\<not> (\<forall>i. \<pi> (\<alpha> + \<beta>) i = 0)

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

goal:
No subgoals!
[PROOF STEP]
qed