[STATEMENT]
lemma weakenStatImpWeakStatImp:
  fixes \<Psi>  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"
  and     cExt: "\<And>\<Psi>' R S \<Psi>''. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> (\<Psi>' \<otimes> \<Psi>'', R, S) \<in> Rel"

  shows "\<Psi> \<rhd> P \<lessapprox><Rel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox><Rel> Q
[PROOF STEP]
proof(induct rule: weakStatImpI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
case(cStatImp \<Psi>')
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
obtain Q' where QChain: "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
              and PImpQ': "insertAssertion(extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame Q') \<Psi>"
              and "(\<Psi>, P, Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'; insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>; (\<Psi>, P, Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakenStatImpE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>
(\<Psi>, P, Q') \<in> Rel

goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
note QChain PImpQ'
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>

goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>

goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
have "\<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'

goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'

goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
from \<open>(\<Psi>, P, Q') \<in> Rel\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q') \<in> Rel
[PROOF STEP]
have "(\<Psi> \<otimes> \<Psi>', P, Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q') \<in> Rel

goal (1 subgoal):
 1. (\<Psi> \<otimes> \<Psi>', P, Q') \<in> Rel
[PROOF STEP]
by(rule cExt)
[PROOF STATE]
proof (state)
this:
(\<Psi> \<otimes> \<Psi>', P, Q') \<in> Rel

goal (1 subgoal):
 1. \<And>\<Psi>'. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>
\<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi> \<otimes> \<Psi>', P, Q') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>
\<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi> \<otimes> \<Psi>', P, Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q' Q''. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi> \<and> \<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'' \<and> (\<Psi> \<otimes> \<Psi>', P, Q'') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma justified_alt:
  "justified C M = (\<forall>t. 0 < zcount M t \<longrightarrow> supported_strong M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified C M = (\<forall>t. 0 < zcount M t \<longrightarrow> supported_strong M t \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t)
[PROOF STEP]
unfolding justified_def supported_def supported_strong_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t) = (\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t; 0 < zcount M t; \<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
apply (drule order_zmset_exists_foundation')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t; \<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u<s. zcount M u \<le> 0)\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t s. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t; \<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
subgoal for t s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t; \<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
[PROOF STEP]
apply (drule spec[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; 0 < zcount M s \<longrightarrow> (\<exists>sa<s. zcount M sa < 0) \<or> (\<exists>t'<s. 0 < zcount C t') \<or> zcount M s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; sa < s; zcount M sa < 0\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
 2. \<And>t'. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; t' < s; 0 < zcount C t'\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
 3. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
[PROOF STEP]
apply (meson le_less_trans less_le_trans nonpos_upto_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t'. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; t' < s; 0 < zcount C t'\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
 2. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
[PROOF STEP]
using order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (2 subgoals):
 1. \<And>t'. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; t' < s; 0 < zcount C t'\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
 2. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
[PROOF STEP]
using order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
(?a \<le> ?b) = (?a < ?b \<or> ?a = ?b)

goal (1 subgoal):
 1. \<lbrakk>\<forall>s. zcount M s < 0 \<longrightarrow> s < t \<longrightarrow> \<not> nonpos_upto M s; \<not> zcount M t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>t'<t. 0 < zcount C t'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<and> nonpos_upto M s) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0) \<or> (\<exists>t'<t. 0 < zcount C t') \<or> zcount M t < zcount C t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma justified_with_alt: "justified_with C M N =
  (\<forall>t. 0 < zcount M t \<longrightarrow>
    (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or>
    (\<exists>s<t. 0 < zcount C s) \<or>
    zcount (M+N) t < zcount C t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified_with C M N = (\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t)
[PROOF STEP]
unfolding justified_with_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t) = (\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount M t + zcount N t < zcount C t; 0 < zcount M t; \<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply (drule order_zmset_exists_foundation')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount M t + zcount N t < zcount C t; \<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u<s. zcount M u \<le> 0)\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t s. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount M t + zcount N t < zcount C t; \<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 2. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
subgoal for t s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount M t + zcount N t < zcount C t; \<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply (drule spec[of _ s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; 0 < zcount M s \<longrightarrow> (\<exists>sa<s. zcount M sa < 0 \<or> zcount N sa < 0) \<or> (\<exists>sa<s. 0 < zcount C sa) \<or> zcount M s + zcount N s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>sa. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; sa < s; zcount M sa < 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 2. \<And>sa. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; sa < s; zcount N sa < 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 3. \<And>sa. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; sa < s; 0 < zcount C sa\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 4. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s + zcount N s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
using order.strict_trans order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < ?b; ?b < ?c\<rbrakk> \<Longrightarrow> ?a < ?c
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (4 subgoals):
 1. \<And>sa. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; sa < s; zcount M sa < 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 2. \<And>sa. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; sa < s; zcount N sa < 0\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 3. \<And>sa. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; sa < s; 0 < zcount C sa\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
 4. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s + zcount N s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. \<not> zcount M s < 0 \<and> \<not> zcount N s < 0 \<or> (\<exists>s'<s. \<not> zcount M s' \<le> 0); \<not> zcount M t + zcount N t < zcount C t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s + zcount N s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply (simp add: not_less not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s<t. 0 \<le> zcount M s \<and> 0 \<le> zcount N s \<or> (\<exists>s'<s. 0 < zcount M s'); zcount C t \<le> zcount M t + zcount N t; s \<le> t; 0 < zcount M s; \<forall>u<s. zcount M u \<le> 0; zcount M s + zcount N s < zcount C s\<rbrakk> \<Longrightarrow> \<exists>s<t. 0 < zcount C s
[PROOF STEP]
apply (smt (verit, best) antisym_conv2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. (zcount M s < 0 \<or> zcount N s < 0) \<and> (\<forall>s'<s. zcount M s' \<le> 0)) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t \<Longrightarrow> \<forall>t. 0 < zcount M t \<longrightarrow> (\<exists>s<t. zcount M s < 0 \<or> zcount N s < 0) \<or> (\<exists>s<t. 0 < zcount C s) \<or> zcount (M + N) t < zcount C t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_induct_select [consumes 1, case_names empty select]:
  assumes "finite S"
    and empty: "P {}"
    and select: "\<And>T. finite T \<Longrightarrow> T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)"
  shows "P S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P S
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
finite S
[PROOF STEP]
have "P S \<and> finite S"
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. P S \<and> finite S
[PROOF STEP]
by (induct S rule: finite_induct_select) (auto intro: empty select)
[PROOF STATE]
proof (state)
this:
P S \<and> finite S

goal (1 subgoal):
 1. P S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P S \<and> finite S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P S \<and> finite S

goal (1 subgoal):
 1. P S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_induct_decompose_sum:
  fixes f :: "'c \<Rightarrow> ('b :: comm_monoid_add)"
  assumes "finite X"
    and     "x\<in>X"
    and     "A (f x)"
    and     "\<forall>Z. B (sum f Z)"
    and     "\<And>x Z. A (f x) \<Longrightarrow> B (sum f Z) \<Longrightarrow> A (f x + sum f Z)"
    and     "\<And>x Z. B (f x) \<Longrightarrow> A (sum f Z) \<Longrightarrow> A (f x + sum f Z)"
  shows "A (\<Sum>x\<in>X. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A (sum f X)
[PROOF STEP]
using assms(1,2,3)
[PROOF STATE]
proof (prove)
using this:
finite X
x \<in> X
A (f x)

goal (1 subgoal):
 1. A (sum f X)
[PROOF STEP]
apply (induct X rule: finite_induct_select)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> {}; A (f x)\<rbrakk> \<Longrightarrow> A (sum f {})
 2. \<And>T. \<lbrakk>finite T; T \<subset> X; \<lbrakk>x \<in> T; A (f x)\<rbrakk> \<Longrightarrow> A (sum f T)\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. x \<in> insert s T \<longrightarrow> A (f x) \<longrightarrow> A (sum f (insert s T))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. \<lbrakk>finite T; T \<subset> X; \<lbrakk>x \<in> T; A (f x)\<rbrakk> \<Longrightarrow> A (sum f T)\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. x \<in> insert s T \<longrightarrow> A (f x) \<longrightarrow> A (sum f (insert s T))
[PROOF STEP]
apply (simp add: sum.insert_remove)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. \<lbrakk>finite T; T \<subset> X; \<lbrakk>x \<in> T; A (f x)\<rbrakk> \<Longrightarrow> A (sum f T)\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. (x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)) \<and> (x \<in> T \<longrightarrow> A (f x) \<longrightarrow> A (f s + sum f T))
[PROOF STEP]
subgoal for T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite T; T \<subset> X; \<lbrakk>x \<in> T; A (f x)\<rbrakk> \<Longrightarrow> A (sum f T)\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. (x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)) \<and> (x \<in> T \<longrightarrow> A (f x) \<longrightarrow> A (f s + sum f T))
[PROOF STEP]
apply (cases "x \<in> T"; simp add: assms(3))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite T; T \<subset> X; A (sum f T); x \<in> T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. (x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)) \<and> A (f s + sum f T)
 2. \<lbrakk>finite T; T \<subset> X; x \<notin> T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)
[PROOF STEP]
apply (drule psubset_imp_ex_mem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; \<exists>b. b \<in> X - T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. (x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)) \<and> A (f s + sum f T)
 2. \<lbrakk>finite T; T \<subset> X; x \<notin> T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>finite T; A (sum f T); x \<in> T; b \<in> X; b \<notin> T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. (x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)) \<and> A (f s + sum f T)
 2. \<lbrakk>finite T; T \<subset> X; x \<notin> T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)
[PROOF STEP]
subgoal for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. (x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)) \<and> A (f s + sum f T)
[PROOF STEP]
apply (rule bexI[of _ z])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> (x = z \<longrightarrow> A (f z) \<longrightarrow> A (f z + sum f T)) \<and> A (f z + sum f T)
 2. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> z \<in> X - T
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> x = z \<longrightarrow> A (f z) \<longrightarrow> A (f z + sum f T)
 2. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> A (f z + sum f T)
 3. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> z \<in> X - T
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> A (f z + sum f T)
 2. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> z \<in> X - T
[PROOF STEP]
apply (rule assms(6)[of z T])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> B (f z)
 2. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> A (sum f T)
 3. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> z \<in> X - T
[PROOF STEP]
apply (rule assms(4)[THEN spec, of "{z}", simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> A (sum f T)
 2. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> z \<in> X - T
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite T; A (sum f T); x \<in> T; z \<in> X; z \<notin> T\<rbrakk> \<Longrightarrow> z \<in> X - T
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite T; T \<subset> X; x \<notin> T\<rbrakk> \<Longrightarrow> \<exists>s\<in>X - T. x = s \<longrightarrow> A (f s) \<longrightarrow> A (f s + sum f T)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>finite T; x \<notin> T; T \<subseteq> X; \<forall>s\<in>X - T. x = s \<and> A (f s) \<and> \<not> A (f s + sum f T); xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> T
[PROOF STEP]
apply (drule bspec[of _ _ x])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>finite T; x \<notin> T; T \<subseteq> X; xa \<in> X\<rbrakk> \<Longrightarrow> x \<in> X - T
 2. \<And>xa. \<lbrakk>finite T; x \<notin> T; T \<subseteq> X; xa \<in> X; x = x \<and> A (f x) \<and> \<not> A (f x + sum f T)\<rbrakk> \<Longrightarrow> xa \<in> T
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>finite T; x \<notin> T; T \<subseteq> X; xa \<in> X\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>xa. \<lbrakk>finite T; x \<notin> T; T \<subseteq> X; xa \<in> X; A (f x); \<not> A (f x + sum f T)\<rbrakk> \<Longrightarrow> xa \<in> T
[PROOF STEP]
apply (rule assms(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>finite T; x \<notin> T; T \<subseteq> X; xa \<in> X; A (f x); \<not> A (f x + sum f T)\<rbrakk> \<Longrightarrow> xa \<in> T
[PROOF STEP]
using assms(4) assms(5)
[PROOF STATE]
proof (prove)
using this:
\<forall>Z. B (sum f Z)
\<lbrakk>A (f ?x); B (sum f ?Z)\<rbrakk> \<Longrightarrow> A (f ?x + sum f ?Z)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>finite T; x \<notin> T; T \<subseteq> X; xa \<in> X; A (f x); \<not> A (f x + sum f T)\<rbrakk> \<Longrightarrow> xa \<in> T
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma minting_msg_add_records: "minting_msg C1 M \<Longrightarrow> \<forall>t. 0 \<le> zcount C2 t \<Longrightarrow> minting_msg (C1+C2) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>minting_msg C1 M; \<forall>t. 0 \<le> zcount C2 t\<rbrakk> \<Longrightarrow> minting_msg (C1 + C2) M
[PROOF STEP]
by (auto simp: minting_msg_def intro: add_strict_increasing dest!: bspec)


[STATEMENT]
lemma add_less: "(a::int) < c \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < c; b \<le> 0\<rbrakk> \<Longrightarrow> a + b < c
[PROOF STEP]
by linarith


[STATEMENT]
lemma disj3_split: "P \<or> Q \<or> R \<Longrightarrow> (P \<Longrightarrow> thesis) \<Longrightarrow> (\<not> P \<and> Q \<Longrightarrow> thesis) \<Longrightarrow> (\<not> P \<Longrightarrow> \<not> Q \<Longrightarrow> R \<Longrightarrow> thesis) \<Longrightarrow> thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q \<or> R; P \<Longrightarrow> thesis; \<not> P \<and> Q \<Longrightarrow> thesis; \<lbrakk>\<not> P; \<not> Q; R\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma filter_zmset_conclude_predicate: "0 < zcount {# x \<in>#\<^sub>z M. P x #} x \<Longrightarrow> 0 < zcount M x \<Longrightarrow> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < zcount (filter_zmset P M) x; 0 < zcount M x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma alw_holds2: "alw (holds P) ss = (P (shd ss) \<and> alw (holds P) (stl ss))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (holds P) ss = (P (shd ss) \<and> alw (holds P) (stl ss))
[PROOF STEP]
by (meson alw.simps holds.elims(2) holds.elims(3))


[STATEMENT]
lemma zmset_of_remove1_mset: "x \<in># M \<Longrightarrow> zmset_of (remove1_mset x M) = zmset_of M - {#x#}\<^sub>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in># M \<Longrightarrow> zmset_of (remove1_mset x M) = zmset_of M - {#x#}\<^sub>z
[PROOF STEP]
by (induct M) auto


[STATEMENT]
lemma timestamps_zmset_of_pair_image[simp]: "timestamps (zmset_of {# (c,t). t \<in># M #}) = zmset_of M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. timestamps (zmset_of (image_mset (Pair c) M)) = zmset_of M
[PROOF STEP]
by (induct M) auto


[STATEMENT]
lemma timestamps_image_zmset_fst[simp]: "timestamps {# (f x, t). (x, t) \<in>#\<^sub>z M #} = timestamps M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. timestamps {#(f x, t). (x, t) \<in>#\<^sub>z M#} = timestamps M
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f M. equiv_zmset (case case M of (M, N) \<Rightarrow> ({#(f x, y). (x, y) \<in># M#}, {#(f x, y). (x, y) \<in># N#}) of (M, N) \<Rightarrow> ({#t. (x, t) \<in># M#}, {#t. (x, t) \<in># N#})) (case M of (M, N) \<Rightarrow> ({#t. (x, t) \<in># M#}, {#t. (x, t) \<in># N#}))
[PROOF STEP]
apply (clarsimp simp: equiv_zmset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f a b. {#case case x of (x, xa) \<Rightarrow> (f x, xa) of (x, t) \<Rightarrow> t. x \<in># a#} + {#case x of (x, t) \<Rightarrow> t. x \<in># b#} = {#case x of (x, t) \<Rightarrow> t. x \<in># a#} + {#case case x of (x, xa) \<Rightarrow> (f x, xa) of (x, t) \<Rightarrow> t. x \<in># b#}
[PROOF STEP]
apply (metis (no_types, lifting) case_prod_unfold image_mset_cong prod.collapse prod.inject)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lift_invariant_to_spec:
  assumes "(\<And>c. init_config c \<Longrightarrow> P c)"
    and   "(\<And>s. holds P s \<Longrightarrow> next s \<Longrightarrow> nxt (holds P) s)"
  shows   "spec s \<Longrightarrow> alw (holds P) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec s \<Longrightarrow> alw (holds P) s
[PROOF STEP]
unfolding spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds init_config s \<and> alw next s \<Longrightarrow> alw (holds P) s
[PROOF STEP]
apply (elim conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds init_config s; alw next s\<rbrakk> \<Longrightarrow> alw (holds P) s
[PROOF STEP]
apply (coinduction arbitrary: s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>holds init_config s; alw next s\<rbrakk> \<Longrightarrow> \<exists>xs. s = xs \<and> holds P xs \<and> ((\<exists>s. stl xs = s \<and> holds init_config s \<and> alw next s) \<or> alw (holds P) (stl xs))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>init_config (shd s); alw next s\<rbrakk> \<Longrightarrow> P (shd s) \<and> (init_config (shd (stl s)) \<and> alw next (stl s) \<or> alw (holds P) (stl s))
[PROOF STEP]
apply (intro conjI assms(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>init_config (shd s); alw next s\<rbrakk> \<Longrightarrow> init_config (shd s)
 2. \<And>s. \<lbrakk>init_config (shd s); alw next s\<rbrakk> \<Longrightarrow> init_config (shd (stl s)) \<and> alw next (stl s) \<or> alw (holds P) (stl s)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>init_config (shd s); alw next s; \<not> alw (holds P) (stl s)\<rbrakk> \<Longrightarrow> init_config (shd (stl s))
 2. \<And>s. \<lbrakk>init_config (shd s); alw next s; \<not> alw (holds P) (stl s)\<rbrakk> \<Longrightarrow> alw next (stl s)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>init_config (shd s_); alw next s_; \<not> alw (holds P) (stl s_)\<rbrakk> \<Longrightarrow> init_config (shd (stl s_))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>init_config (shd s_); alw next s_; \<not> alw (holds P) (stl s_)\<rbrakk> \<Longrightarrow> init_config (shd (stl s_))
[PROOF STEP]
fix sa :: "('b, 'a) configuration stream"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>init_config (shd s_); alw next s_; \<not> alw (holds P) (stl s_)\<rbrakk> \<Longrightarrow> init_config (shd (stl s_))
[PROOF STEP]
assume a1: "init_config (shd sa)"
[PROOF STATE]
proof (state)
this:
init_config (shd sa)

goal (1 subgoal):
 1. \<lbrakk>init_config (shd s_); alw next s_; \<not> alw (holds P) (stl s_)\<rbrakk> \<Longrightarrow> init_config (shd (stl s_))
[PROOF STEP]
assume a2: "alw next sa"
[PROOF STATE]
proof (state)
this:
alw next sa

goal (1 subgoal):
 1. \<lbrakk>init_config (shd s_); alw next s_; \<not> alw (holds P) (stl s_)\<rbrakk> \<Longrightarrow> init_config (shd (stl s_))
[PROOF STEP]
assume "\<not> alw (holds P) (stl sa)"
[PROOF STATE]
proof (state)
this:
\<not> alw (holds P) (stl sa)

goal (1 subgoal):
 1. \<lbrakk>init_config (shd s_); alw next s_; \<not> alw (holds P) (stl s_)\<rbrakk> \<Longrightarrow> init_config (shd (stl s_))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> alw (holds P) (stl sa)
[PROOF STEP]
have "\<not> alw (\<lambda>s. holds P s \<longrightarrow> nxt (holds P) s) sa"
[PROOF STATE]
proof (prove)
using this:
\<not> alw (holds P) (stl sa)

goal (1 subgoal):
 1. \<not> alw (\<lambda>s. holds P s \<longrightarrow> nxt (holds P) s) sa
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
\<not> alw (holds P) (stl sa)
init_config (shd sa)

goal (1 subgoal):
 1. \<not> alw (\<lambda>s. holds P s \<longrightarrow> nxt (holds P) s) sa
[PROOF STEP]
by (metis (no_types) alw.cases alw_invar assms(1) holds.elims(3))
[PROOF STATE]
proof (state)
this:
\<not> alw (\<lambda>s. holds P s \<longrightarrow> nxt (holds P) s) sa

goal (1 subgoal):
 1. \<lbrakk>init_config (shd s_); alw next s_; \<not> alw (holds P) (stl s_)\<rbrakk> \<Longrightarrow> init_config (shd (stl s_))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> alw (\<lambda>s. holds P s \<longrightarrow> nxt (holds P) s) sa
[PROOF STEP]
show "init_config (shd (stl sa))"
[PROOF STATE]
proof (prove)
using this:
\<not> alw (\<lambda>s. holds P s \<longrightarrow> nxt (holds P) s) sa

goal (1 subgoal):
 1. init_config (shd (stl sa))
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
\<not> alw (\<lambda>s. holds P s \<longrightarrow> nxt (holds P) s) sa
alw next sa

goal (1 subgoal):
 1. init_config (shd (stl sa))
[PROOF STEP]
by (metis (lifting) alw_iff_sdrop assms(2))
[PROOF STATE]
proof (state)
this:
init_config (shd (stl sa))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>init_config (shd s); alw next s; \<not> alw (holds P) (stl s)\<rbrakk> \<Longrightarrow> alw next (stl s)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma timestamps_sum_distrib[simp]: "(\<Sum>p \<in> A. timestamps (f p)) = timestamps (\<Sum>p \<in> A. f p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p\<in>A. timestamps (f p)) = timestamps (sum f A)
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma timestamps_zmset_of[simp]: "timestamps (zmset_of M) = zmset_of {# t. (p,t) \<in># M #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. timestamps (zmset_of M) = zmset_of {#t. (p, t) \<in># M#}
[PROOF STEP]
by (induct M) auto


[STATEMENT]
lemma vacant_upto_add: "vacant_upto a t \<Longrightarrow> vacant_upto b t \<Longrightarrow> vacant_upto (a+b) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vacant_upto a t; vacant_upto b t\<rbrakk> \<Longrightarrow> vacant_upto (a + b) t
[PROOF STEP]
by (simp add: vacant_upto_def)


[STATEMENT]
lemma nonpos_upto_add: "nonpos_upto a t \<Longrightarrow> nonpos_upto b t \<Longrightarrow> nonpos_upto (a+b) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nonpos_upto a t; nonpos_upto b t\<rbrakk> \<Longrightarrow> nonpos_upto (a + b) t
[PROOF STEP]
by (auto intro: add_nonpos_nonpos simp: nonpos_upto_def)


[STATEMENT]
lemma nonzero_lt_gtD: "(n::_::linorder) \<noteq> 0 \<Longrightarrow> 0 < n \<or> n < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> (0::'b) \<Longrightarrow> (0::'b) < n \<or> n < (0::'b)
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_lt_diff: "(0::int) < a - b \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < a - b; 0 \<le> b\<rbrakk> \<Longrightarrow> 0 < a
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_lt_add_disj: "0 < (a::int) + b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a \<or> 0 < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < a + b; 0 \<le> a; 0 \<le> b\<rbrakk> \<Longrightarrow> 0 < a \<or> 0 < b
[PROOF STEP]
by auto


[STATEMENT]
lemma next_performopD:
  assumes "next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
  shows
    "\<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z"
    "\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t"
    "minting_self (c_caps c0 p) \<Delta>mint_self"
    "minting_msg (c_caps c0 p) \<Delta>mint_msg"
    "c_temp c1 = (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))"
    "c_msg c1  = c_msg c0"
    "c_glob c1 = c_glob c0"
    "c_data_msg c1 = c_data_msg c0 + \<Delta>mint_msg"
    "c_caps c1 = (c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z &&& \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t) &&& minting_self (c_caps c0 p) \<Delta>mint_self &&& minting_msg (c_caps c0 p) \<Delta>mint_msg) &&& (c_temp c1 = (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) &&& c_msg c1 = c_msg c0) &&& c_glob c1 = c_glob c0 &&& c_data_msg c1 = c_data_msg c0 + \<Delta>mint_msg &&& c_caps c1 = (c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self

goal (1 subgoal):
 1. ((\<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z &&& \<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t) &&& minting_self (c_caps c0 p) \<Delta>mint_self &&& minting_msg (c_caps c0 p) \<Delta>mint_msg) &&& (c_temp c1 = (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) &&& c_msg c1 = c_msg c0) &&& c_glob c1 = c_glob c0 &&& c_data_msg c1 = c_data_msg c0 + \<Delta>mint_msg &&& c_caps c1 = (c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
by (simp_all add: next_performop'_def Let_def algebra_simps)


[STATEMENT]
lemma next_performop_complexD:
  assumes "next_performop' c0 c1 p \<Delta>neg \<Delta>mint_msg \<Delta>mint_self"
  shows
    "records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)"
    "GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)"
    "IncomingInfo c1 k p' q = (if p' = p
      then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
      else IncomingInfo c0 k p' q)"
    "\<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0"
    "InfoAt c1 k p' q = InfoAt c0 k p' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) &&& GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)) &&& IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 k p' q) &&& (\<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0) &&& InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 2. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 3. IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 k p' q)
 4. \<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0
 5. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
let ?\<Delta> = "timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 2. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 3. IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 k p' q)
 4. \<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0
 5. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
note change = next_performopD[OF assms(1)]
[PROOF STATE]
proof (state)
this:
\<Delta>mint_msg \<noteq> {#} \<or> zmset_of \<Delta>mint_self - zmset_of \<Delta>neg \<noteq> {#}\<^sub>z
\<forall>t. int (count \<Delta>neg t) \<le> zcount (c_caps c0 p) t
minting_self (c_caps c0 p) \<Delta>mint_self
minting_msg (c_caps c0 p) \<Delta>mint_msg
c_temp c1 = (c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
c_msg c1 = c_msg c0
c_glob c1 = c_glob c0
c_data_msg c1 = c_data_msg c0 + \<Delta>mint_msg
c_caps c1 = (c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))

goal (5 subgoals):
 1. records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 2. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 3. IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 k p' q)
 4. \<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0
 5. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "records c1 = records c0 + ?\<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
[PROOF STEP]
unfolding records_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((c_caps c0)(p := c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) UNIV + timestamps (zmset_of (c_data_msg c0 + \<Delta>mint_msg)) = sum (c_caps c0) UNIV + timestamps (zmset_of (c_data_msg c0)) + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV. if x = p then c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else c_caps c0 x) + zmset_of ({#case x of (p, t) \<Rightarrow> t. x \<in># c_data_msg c0#} + {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>mint_msg#}) = sum (c_caps c0) UNIV + zmset_of {#case x of (p, t) \<Rightarrow> t. x \<in># c_data_msg c0#} + (zmset_of {#case x of (p, t) \<Rightarrow> t. x \<in># \<Delta>mint_msg#} + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
[PROOF STEP]
apply (subst add_diff_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV. if x = p then c_caps c0 p + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else c_caps c0 x) + zmset_of ({#t. (p, t) \<in># c_data_msg c0#} + {#t. (p, t) \<in># \<Delta>mint_msg#}) = sum (c_caps c0) UNIV + zmset_of {#t. (p, t) \<in># c_data_msg c0#} + (zmset_of {#t. (p, t) \<in># \<Delta>mint_msg#} + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
apply (subst sum_if_distrib_add)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite UNIV
 2. p \<in> UNIV
 3. sum (c_caps c0) UNIV + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) + zmset_of ({#t. (p, t) \<in># c_data_msg c0#} + {#t. (p, t) \<in># \<Delta>mint_msg#}) = sum (c_caps c0) UNIV + zmset_of {#t. (p, t) \<in># c_data_msg c0#} + (zmset_of {#t. (p, t) \<in># \<Delta>mint_msg#} + (zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))
[PROOF STEP]
apply (simp_all add: algebra_simps zmset_of_plus)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
records c1 = records c0 + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)

goal (4 subgoals):
 1. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 2. IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 k p' q)
 3. \<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0
 4. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "IncomingInfo c1 k p' q = (if p' = p
      then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
      else IncomingInfo c0 k p' q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 k p' q)
[PROOF STEP]
unfolding IncomingInfo_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (drop k (c_msg c0 p' q)) + ((c_temp c0)(p := c_temp c0 p + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg))) p' = (if p' = p then sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p' + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else sum_list (drop k (c_msg c0 p' q)) + c_temp c0 p')
[PROOF STEP]
by (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg) else IncomingInfo c0 k p' q)

goal (3 subgoals):
 1. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
 2. \<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0
 3. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + ?\<Delta>" for q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
[PROOF STEP]
unfolding GlobalIncomingInfo_def IncomingInfo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p'\<in>UNIV. sum_list (drop (if p' = q then 0 else 0) (c_msg c1 p' q)) + c_temp c1 p') = (\<Sum>p'\<in>UNIV. sum_list (drop (if p' = q then 0 else 0) (c_msg c0 p' q)) + c_temp c0 p') + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)
[PROOF STEP]
by (rule Sum_eq_pick_changed_elem[where m = p]) (simp_all add: change algebra_simps)
[PROOF STATE]
proof (state)
this:
GlobalIncomingInfoAt c1 ?q = GlobalIncomingInfoAt c0 ?q + (timestamps (zmset_of \<Delta>mint_msg) + zmset_of \<Delta>mint_self - zmset_of \<Delta>neg)

goal (2 subgoals):
 1. \<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0
 2. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "\<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t'<t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) t = 0
[PROOF STEP]
by (rule ccontr) (clarsimp dest!: image_zmset_pre change(4)[unfolded minting_msg_def, rule_format])
[PROOF STATE]
proof (state)
this:
\<forall>t'<?t. zcount (c_caps c0 p) t' = 0 \<Longrightarrow> zcount (timestamps (zmset_of \<Delta>mint_msg)) ?t = 0

goal (1 subgoal):
 1. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "InfoAt c1 k p' q = InfoAt c0 k p' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
unfolding InfoAt_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 \<le> k \<and> k < length (c_msg c0 p' q) then c_msg c0 p' q ! k else {#}\<^sub>z) = (if 0 \<le> k \<and> k < length (c_msg c0 p' q) then c_msg c0 p' q ! k else {#}\<^sub>z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
InfoAt c1 k p' q = InfoAt c0 k p' q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_sendupdD:
  assumes "next_sendupd' c0 c1 p tt"
  shows
    "{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} \<noteq> {#}\<^sub>z"
    "justified (c_caps c0 p) (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#})"
    "c_temp c1 p' = (if p' = p then c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else c_temp c0 p')"
    "c_msg c1 = (\<lambda>p' q. if p' = p then c_msg c0 p q @ [{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}] else c_msg c0 p' q)"
    "c_glob c1 = c_glob c0"
    "c_caps c1 = c_caps c0"
    "c_data_msg c1 = c_data_msg c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} \<noteq> {#}\<^sub>z &&& justified (c_caps c0 p) (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) &&& c_temp c1 p' = (if p' = p then c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else c_temp c0 p')) &&& (c_msg c1 = (\<lambda>p' q. if p' = p then c_msg c0 p q @ [{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}] else c_msg c0 p' q) &&& c_glob c1 = c_glob c0) &&& c_caps c1 = c_caps c0 &&& c_data_msg c1 = c_data_msg c0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_sendupd' c0 c1 p tt

goal (1 subgoal):
 1. ({#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} \<noteq> {#}\<^sub>z &&& justified (c_caps c0 p) (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}) &&& c_temp c1 p' = (if p' = p then c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else c_temp c0 p')) &&& (c_msg c1 = (\<lambda>p' q. if p' = p then c_msg c0 p q @ [{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}] else c_msg c0 p' q) &&& c_glob c1 = c_glob c0) &&& c_caps c1 = c_caps c0 &&& c_data_msg c1 = c_data_msg c0
[PROOF STEP]
by (simp_all add: next_sendupd'_def Let_def fun_eq_iff)


[STATEMENT]
lemma next_sendupd_complexD:
  assumes "next_sendupd' c0 c1 p tt"
  shows
    "records c1 = records c0"
    "IncomingInfo c1 0 = IncomingInfo c0 0"
    "IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k
                               then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}
                               else IncomingInfo c0 k p' q)"
    "k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q"
    "length (c_msg c0 p q) < k \<Longrightarrow>
     IncomingInfo c1 k p' q = (if p' = p
                               then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}
                               else IncomingInfo c0 k p' q)"
    "GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q"
    "InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (records c1 = records c0 &&& IncomingInfo c1 0 = IncomingInfo c0 0 &&& IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)) &&& ((k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q) &&& (length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q))) &&& GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q &&& InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. records c1 = records c0
 2. IncomingInfo c1 0 = IncomingInfo c0 0
 3. IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 4. k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q
 5. length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 6. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 7. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
note change = next_sendupdD[OF assms]
[PROOF STATE]
proof (state)
this:
{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} \<noteq> {#}\<^sub>z
justified (c_caps c0 p) (c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#})
c_temp c1 ?p' = (if ?p' = p then c_temp c0 p - {#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#} else c_temp c0 ?p')
c_msg c1 = (\<lambda>p' q. if p' = p then c_msg c0 p q @ [{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}] else c_msg c0 p' q)
c_glob c1 = c_glob c0
c_caps c1 = c_caps c0
c_data_msg c1 = c_data_msg c0

goal (7 subgoals):
 1. records c1 = records c0
 2. IncomingInfo c1 0 = IncomingInfo c0 0
 3. IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 4. k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q
 5. length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 6. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 7. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
show "records c1 = records c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. records c1 = records c0
[PROOF STEP]
by (simp add: records_def change)
[PROOF STATE]
proof (state)
this:
records c1 = records c0

goal (6 subgoals):
 1. IncomingInfo c1 0 = IncomingInfo c0 0
 2. IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 3. k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q
 4. length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 5. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 6. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
show ii: "IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k
                                      then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}
                                      else IncomingInfo c0 k p' q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
[PROOF STEP]
by (simp add: algebra_simps IncomingInfo_def change)
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)

goal (5 subgoals):
 1. IncomingInfo c1 0 = IncomingInfo c0 0
 2. k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q
 3. length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 4. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 5. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
[PROOF STEP]
show "k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q"
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)

goal (1 subgoal):
 1. k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<le> length (c_msg c0 p q) \<Longrightarrow> IncomingInfo c1 k p' q = IncomingInfo c0 k p' q

goal (4 subgoals):
 1. IncomingInfo c1 0 = IncomingInfo c0 0
 2. length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
 3. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 4. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
from ii
[PROOF STATE]
proof (chain)
picking this:
IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
[PROOF STEP]
show "length (c_msg c0 p q) < k \<Longrightarrow>
     IncomingInfo c1 k p' q = (if p' = p
                               then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#}
                               else IncomingInfo c0 k p' q)"
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 k p' q = (if p' = p \<and> length (c_msg c0 p q) < k then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)

goal (1 subgoal):
 1. length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (c_msg c0 p q) < k \<Longrightarrow> IncomingInfo c1 k p' q = (if p' = p then IncomingInfo c0 k p' q - {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else IncomingInfo c0 k p' q)

goal (3 subgoals):
 1. IncomingInfo c1 0 = IncomingInfo c0 0
 2. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 3. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
have "IncomingInfo c1 0 p q = IncomingInfo c0 0 p q" for p q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 0 p q = IncomingInfo c0 0 p q
[PROOF STEP]
by (simp add: algebra_simps IncomingInfo_def change)
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 0 ?p ?q = IncomingInfo c0 0 ?p ?q

goal (3 subgoals):
 1. IncomingInfo c1 0 = IncomingInfo c0 0
 2. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 3. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IncomingInfo c1 0 ?p ?q = IncomingInfo c0 0 ?p ?q
[PROOF STEP]
show "IncomingInfo c1 0 = IncomingInfo c0 0"
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 0 ?p ?q = IncomingInfo c0 0 ?p ?q

goal (1 subgoal):
 1. IncomingInfo c1 0 = IncomingInfo c0 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 0 = IncomingInfo c0 0

goal (2 subgoals):
 1. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
 2. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IncomingInfo c1 0 = IncomingInfo c0 0
[PROOF STEP]
show "GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q"
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 0 = IncomingInfo c0 0

goal (1 subgoal):
 1. GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q
[PROOF STEP]
unfolding GlobalIncomingInfo_def
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 0 = IncomingInfo c0 0

goal (1 subgoal):
 1. (\<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = q then 0 else 0) p' q) = (\<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q then 0 else 0) p' q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
GlobalIncomingInfoAt c1 q = GlobalIncomingInfoAt c0 q

goal (1 subgoal):
 1. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
show "InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)
[PROOF STEP]
unfolding InfoAt_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 \<le> k \<and> k < length (if p' = p then c_msg c0 p q @ [{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}] else c_msg c0 p' q) then (if p' = p then c_msg c0 p q @ [{#t \<in>#\<^sub>z c_temp c0 p. t \<in> tt#}] else c_msg c0 p' q) ! k else {#}\<^sub>z) = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else if 0 \<le> k \<and> k < length (c_msg c0 p' q) then c_msg c0 p' q ! k else {#}\<^sub>z)
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
InfoAt c1 k p' q = (if p' = p \<and> k = length (c_msg c0 p q) then {#t \<in>#\<^sub>z c_temp c0 p'. t \<in> tt#} else InfoAt c0 k p' q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_recvupdD:
  assumes "next_recvupd' c0 c1 p q"
  shows
    "c_msg c0 p q \<noteq> []"
    "c_temp c1 = c_temp c0"
    "c_msg c1 = (\<lambda>p' q'. if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q')"
    "c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))"
    "c_caps c1 = c_caps c0"
    "c_data_msg c1 = c_data_msg c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c_msg c0 p q \<noteq> [] &&& c_temp c1 = c_temp c0 &&& c_msg c1 = (\<lambda>p' q'. if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q')) &&& c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q)) &&& c_caps c1 = c_caps c0 &&& c_data_msg c1 = c_data_msg c0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_recvupd' c0 c1 p q

goal (1 subgoal):
 1. (c_msg c0 p q \<noteq> [] &&& c_temp c1 = c_temp c0 &&& c_msg c1 = (\<lambda>p' q'. if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q')) &&& c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q)) &&& c_caps c1 = c_caps c0 &&& c_data_msg c1 = c_data_msg c0
[PROOF STEP]
by (simp_all add: next_recvupd'_def fun_eq_iff)


[STATEMENT]
lemma next_recvupd_complexD:
  assumes "next_recvupd' c0 c1 p q"
  shows
    "records c1 = records c0"
    "IncomingInfo c1 0 p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 0 p' q' - hd (c_msg c0 p q) else IncomingInfo c0 0 p' q')"
    "IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q
                                then IncomingInfo c0 (k+1) p' q'
                                else IncomingInfo c0 k p' q')"
    "GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')"
    "InfoAt c1 k p q = InfoAt c0 (k+1) p q"
    "InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k+1) p q else InfoAt c0 k p' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (records c1 = records c0 &&& IncomingInfo c1 0 p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 0 p' q' - hd (c_msg c0 p q) else IncomingInfo c0 0 p' q') &&& IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 (k + 1) p' q' else IncomingInfo c0 k p' q')) &&& GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q') &&& InfoAt c1 k p q = InfoAt c0 (k + 1) p q &&& InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. records c1 = records c0
 2. IncomingInfo c1 0 p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 0 p' q' - hd (c_msg c0 p q) else IncomingInfo c0 0 p' q')
 3. IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 (k + 1) p' q' else IncomingInfo c0 k p' q')
 4. GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')
 5. InfoAt c1 k p q = InfoAt c0 (k + 1) p q
 6. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
note change = next_recvupdD[OF assms]
[PROOF STATE]
proof (state)
this:
c_msg c0 p q \<noteq> []
c_temp c1 = c_temp c0
c_msg c1 = (\<lambda>p' q'. if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q')
c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))
c_caps c1 = c_caps c0
c_data_msg c1 = c_data_msg c0

goal (6 subgoals):
 1. records c1 = records c0
 2. IncomingInfo c1 0 p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 0 p' q' - hd (c_msg c0 p q) else IncomingInfo c0 0 p' q')
 3. IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 (k + 1) p' q' else IncomingInfo c0 k p' q')
 4. GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')
 5. InfoAt c1 k p q = InfoAt c0 (k + 1) p q
 6. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
show "records c1 = records c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. records c1 = records c0
[PROOF STEP]
by (simp add: records_def change)
[PROOF STATE]
proof (state)
this:
records c1 = records c0

goal (5 subgoals):
 1. IncomingInfo c1 0 p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 0 p' q' - hd (c_msg c0 p q) else IncomingInfo c0 0 p' q')
 2. IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 (k + 1) p' q' else IncomingInfo c0 k p' q')
 3. GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')
 4. InfoAt c1 k p q = InfoAt c0 (k + 1) p q
 5. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
show ii: "IncomingInfo c1 0 p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 0 p' q' - hd (c_msg c0 p q) else IncomingInfo c0 0 p' q')" for p' q'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 0 p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 0 p' q' - hd (c_msg c0 p q) else IncomingInfo c0 0 p' q')
[PROOF STEP]
by (auto simp: IncomingInfo_def change algebra_simps sum_list_hd_tl)
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 0 ?p' ?q' = (if ?p' = p \<and> ?q' = q then IncomingInfo c0 0 ?p' ?q' - hd (c_msg c0 p q) else IncomingInfo c0 0 ?p' ?q')

goal (4 subgoals):
 1. IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 (k + 1) p' q' else IncomingInfo c0 k p' q')
 2. GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')
 3. InfoAt c1 k p q = InfoAt c0 (k + 1) p q
 4. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
show "IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q
                                   then IncomingInfo c0 (k+1) p' q'
                                   else IncomingInfo c0 k p' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 (k + 1) p' q' else IncomingInfo c0 k p' q')
[PROOF STEP]
by (auto simp:  IncomingInfo_def change algebra_simps sum_list_hd_tl drop_Suc)
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 k p' q' = (if p' = p \<and> q' = q then IncomingInfo c0 (k + 1) p' q' else IncomingInfo c0 k p' q')

goal (3 subgoals):
 1. GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')
 2. InfoAt c1 k p q = InfoAt c0 (k + 1) p q
 3. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
show "GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')
[PROOF STEP]
unfolding GlobalIncomingInfo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = q' then 0 else 0) p' q') = (if q' = q then (\<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q') - hd (c_msg c0 p q) else \<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q')
[PROOF STEP]
apply (cases "q'=q")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. q' = q \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = q' then 0 else 0) p' q') = (if q' = q then (\<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q') - hd (c_msg c0 p q) else \<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q')
 2. q' \<noteq> q \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = q' then 0 else 0) p' q') = (if q' = q then (\<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q') - hd (c_msg c0 p q) else \<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. q' = q \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c1 0 p' q) = (\<Sum>p'\<in>UNIV. IncomingInfo c0 0 p' q) - hd (c_msg c0 p q)
 2. q' \<noteq> q \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = q' then 0 else 0) p' q') = (if q' = q then (\<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q') - hd (c_msg c0 p q) else \<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q')
[PROOF STEP]
apply (subst diff_conv_add_uminus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. q' = q \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c1 0 p' q) = (\<Sum>p'\<in>UNIV. IncomingInfo c0 0 p' q) + - hd (c_msg c0 p q)
 2. q' \<noteq> q \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = q' then 0 else 0) p' q') = (if q' = q then (\<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q') - hd (c_msg c0 p q) else \<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q')
[PROOF STEP]
apply (intro Sum_eq_pick_changed_elem[where m = p])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. q' = q \<Longrightarrow> finite UNIV
 2. q' = q \<Longrightarrow> p \<in> UNIV
 3. q' = q \<Longrightarrow> IncomingInfo c1 0 p q = IncomingInfo c0 0 p q + - hd (c_msg c0 p q)
 4. \<And>n. \<lbrakk>q' = q; n \<noteq> p \<and> n \<in> UNIV\<rbrakk> \<Longrightarrow> IncomingInfo c1 0 n q = IncomingInfo c0 0 n q
 5. q' \<noteq> q \<Longrightarrow> (\<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = q' then 0 else 0) p' q') = (if q' = q then (\<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q') - hd (c_msg c0 p q) else \<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = q' then 0 else 0) p' q')
[PROOF STEP]
apply (simp_all add: ii)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
GlobalIncomingInfoAt c1 q' = (if q' = q then GlobalIncomingInfoAt c0 q' - hd (c_msg c0 p q) else GlobalIncomingInfoAt c0 q')

goal (2 subgoals):
 1. InfoAt c1 k p q = InfoAt c0 (k + 1) p q
 2. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
show "InfoAt c1 k p q = InfoAt c0 (k+1) p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfoAt c1 k p q = InfoAt c0 (k + 1) p q
[PROOF STEP]
unfolding InfoAt_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 \<le> k \<and> k < length (if p = p \<and> q = q then tl (c_msg c0 p q) else c_msg c0 p q) then (if p = p \<and> q = q then tl (c_msg c0 p q) else c_msg c0 p q) ! k else {#}\<^sub>z) = (if 0 \<le> k + 1 \<and> k + 1 < length (c_msg c0 p q) then c_msg c0 p q ! (k + 1) else {#}\<^sub>z)
[PROOF STEP]
by (auto simp: nth_tl)
[PROOF STATE]
proof (state)
this:
InfoAt c1 k p q = InfoAt c0 (k + 1) p q

goal (1 subgoal):
 1. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
show "InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k+1) p q else InfoAt c0 k p' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')
[PROOF STEP]
unfolding InfoAt_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 \<le> k \<and> k < length (if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q') then (if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q') ! k else {#}\<^sub>z) = (if p' = p \<and> q' = q then if 0 \<le> k + 1 \<and> k + 1 < length (c_msg c0 p q) then c_msg c0 p q ! (k + 1) else {#}\<^sub>z else if 0 \<le> k \<and> k < length (c_msg c0 p' q') then c_msg c0 p' q' ! k else {#}\<^sub>z)
[PROOF STEP]
by (auto simp: nth_tl)
[PROOF STATE]
proof (state)
this:
InfoAt c1 k p' q' = (if p' = p \<and> q' = q then InfoAt c0 (k + 1) p q else InfoAt c0 k p' q')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_recvcapD:
  assumes "next_recvcap' c0 c1 p t"
  shows
    "(p,t) \<in># c_data_msg c0"
    "c_temp c1 = c_temp c0"
    "c_msg c1 = c_msg c0"
    "c_glob c1 = c_glob c0"
    "c_caps c1 = (c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z)"
    "c_data_msg c1 = c_data_msg c0 - {#(p,t)#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p, t) \<in># c_data_msg c0 &&& c_temp c1 = c_temp c0 &&& c_msg c1 = c_msg c0) &&& c_glob c1 = c_glob c0 &&& c_caps c1 = (c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z) &&& c_data_msg c1 = remove1_mset (p, t) (c_data_msg c0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_recvcap' c0 c1 p t

goal (1 subgoal):
 1. ((p, t) \<in># c_data_msg c0 &&& c_temp c1 = c_temp c0 &&& c_msg c1 = c_msg c0) &&& c_glob c1 = c_glob c0 &&& c_caps c1 = (c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z) &&& c_data_msg c1 = remove1_mset (p, t) (c_data_msg c0)
[PROOF STEP]
by (simp_all add: next_recvcap'_def)


[STATEMENT]
lemma next_recvcap_complexD:
  assumes "next_recvcap' c0 c1 p t"
  shows
    "records c1 = records c0"
    "IncomingInfo c1 = IncomingInfo c0"
    "GlobalIncomingInfo c1 = GlobalIncomingInfo c0"
    "InfoAt c1 k p' q = InfoAt c0 k p' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (records c1 = records c0 &&& IncomingInfo c1 = IncomingInfo c0) &&& GlobalIncomingInfo c1 = GlobalIncomingInfo c0 &&& InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. records c1 = records c0
 2. IncomingInfo c1 = IncomingInfo c0
 3. GlobalIncomingInfo c1 = GlobalIncomingInfo c0
 4. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
note change = next_recvcapD[OF assms]
[PROOF STATE]
proof (state)
this:
(p, t) \<in># c_data_msg c0
c_temp c1 = c_temp c0
c_msg c1 = c_msg c0
c_glob c1 = c_glob c0
c_caps c1 = (c_caps c0)(p := c_caps c0 p + {#t#}\<^sub>z)
c_data_msg c1 = remove1_mset (p, t) (c_data_msg c0)

goal (4 subgoals):
 1. records c1 = records c0
 2. IncomingInfo c1 = IncomingInfo c0
 3. GlobalIncomingInfo c1 = GlobalIncomingInfo c0
 4. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "records c1 = records c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. records c1 = records c0
[PROOF STEP]
unfolding records_def change fun_upd_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>z\<in>UNIV. if z = p then c_caps c0 p + {#t#}\<^sub>z else c_caps c0 z) + timestamps (zmset_of (remove1_mset (p, t) (c_data_msg c0))) = sum (c_caps c0) UNIV + timestamps (zmset_of (c_data_msg c0))
[PROOF STEP]
apply (subst sum_if_distrib_add)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite UNIV
 2. p \<in> UNIV
 3. sum (c_caps c0) UNIV + {#t#}\<^sub>z + timestamps (zmset_of (remove1_mset (p, t) (c_data_msg c0))) = sum (c_caps c0) UNIV + timestamps (zmset_of (c_data_msg c0))
[PROOF STEP]
using change(1)
[PROOF STATE]
proof (prove)
using this:
(p, t) \<in># c_data_msg c0

goal (3 subgoals):
 1. finite UNIV
 2. p \<in> UNIV
 3. sum (c_caps c0) UNIV + {#t#}\<^sub>z + timestamps (zmset_of (remove1_mset (p, t) (c_data_msg c0))) = sum (c_caps c0) UNIV + timestamps (zmset_of (c_data_msg c0))
[PROOF STEP]
apply (simp_all add: zmset_of_remove1_mset algebra_simps records_def change)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
records c1 = records c0

goal (3 subgoals):
 1. IncomingInfo c1 = IncomingInfo c0
 2. GlobalIncomingInfo c1 = GlobalIncomingInfo c0
 3. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "IncomingInfo c1 = IncomingInfo c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IncomingInfo c1 = IncomingInfo c0
[PROOF STEP]
unfolding IncomingInfo_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k p q. sum_list (drop k (c_msg c0 p q)) + c_temp c0 p) = (\<lambda>k p q. sum_list (drop k (c_msg c0 p q)) + c_temp c0 p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
IncomingInfo c1 = IncomingInfo c0

goal (2 subgoals):
 1. GlobalIncomingInfo c1 = GlobalIncomingInfo c0
 2. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IncomingInfo c1 = IncomingInfo c0
[PROOF STEP]
show "GlobalIncomingInfo c1 = GlobalIncomingInfo c0"
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 = IncomingInfo c0

goal (1 subgoal):
 1. GlobalIncomingInfo c1 = GlobalIncomingInfo c0
[PROOF STEP]
unfolding GlobalIncomingInfo_def
[PROOF STATE]
proof (prove)
using this:
IncomingInfo c1 = IncomingInfo c0

goal (1 subgoal):
 1. (\<lambda>k p q. \<Sum>p'\<in>UNIV. IncomingInfo c1 (if p' = p then k else 0) p' q) = (\<lambda>k p q. \<Sum>p'\<in>UNIV. IncomingInfo c0 (if p' = p then k else 0) p' q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
GlobalIncomingInfo c1 = GlobalIncomingInfo c0

goal (1 subgoal):
 1. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
show "InfoAt c1 k p' q = InfoAt c0 k p' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfoAt c1 k p' q = InfoAt c0 k p' q
[PROOF STEP]
unfolding InfoAt_def change
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 \<le> k \<and> k < length (c_msg c0 p' q) then c_msg c0 p' q ! k else {#}\<^sub>z) = (if 0 \<le> k \<and> k < length (c_msg c0 p' q) then c_msg c0 p' q ! k else {#}\<^sub>z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
InfoAt c1 k p' q = InfoAt c0 k p' q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_next_recvupd:
  assumes "c_msg c0 p q \<noteq> []"
  shows   "\<exists>c1. next_recvupd' c0 c1 p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c1. next_recvupd' c0 c1 p q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c_msg c0 p q \<noteq> []

goal (1 subgoal):
 1. \<exists>c1. next_recvupd' c0 c1 p q
[PROOF STEP]
unfolding next_recvupd'_def
[PROOF STATE]
proof (prove)
using this:
c_msg c0 p q \<noteq> []

goal (1 subgoal):
 1. \<exists>c1. c_msg c0 p q \<noteq> [] \<and> c1 = c0\<lparr>c_msg := (c_msg c0)(p := (c_msg c0 p)(q := tl (c_msg c0 p q))), c_glob := (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))\<rparr>
[PROOF STEP]
by (intro
      exI[of _ "c0\<lparr>c_msg := (\<lambda>p' q'. if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q'),
                   c_glob := (\<lambda>q'. if q' = q then c_glob c0 q + hd (c_msg c0 p q) else c_glob c0 q')\<rparr>"])
        (auto simp: fun_eq_iff)


[STATEMENT]
lemma justified_empty[simp]: "justified {#}\<^sub>z {#}\<^sub>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justified {#}\<^sub>z {#}\<^sub>z
[PROOF STEP]
by (simp add: justified_def)