[STATEMENT]
theorem welltyped_aggressive_imp_defensive:
  "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P \<Longrightarrow> P,\<Phi> \<turnstile> \<sigma> \<surd> \<Longrightarrow> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'
  \<Longrightarrow> P \<turnstile> (Normal \<sigma>) -jvmd\<rightarrow> (Normal \<sigma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_jvm_prog\<^bsub>\<Phi>\<^esub> P; P,\<Phi> |- \<sigma> [ok]; P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_jvm_prog\<^bsub>\<Phi>\<^esub> P; P,\<Phi> |- \<sigma> [ok]; P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>wf_jvm_prog\<^bsub>\<Phi>\<^esub> P; P,\<Phi> |- \<sigma> [ok]; P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'
[PROOF STEP]
assume wf: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P" and cf: "P,\<Phi> \<turnstile> \<sigma> \<surd>" and exec: "P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'"
[PROOF STATE]
proof (state)
this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P
P,\<Phi> |- \<sigma> [ok]
P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'

goal (1 subgoal):
 1. \<lbrakk>wf_jvm_prog\<^bsub>\<Phi>\<^esub> P; P,\<Phi> |- \<sigma> [ok]; P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P
P,\<Phi> |- \<sigma> [ok]
P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'
[PROOF STEP]
have "(\<sigma>, \<sigma>') \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P
P,\<Phi> |- \<sigma> [ok]
P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'

goal (1 subgoal):
 1. (\<sigma>, \<sigma>') \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*
[PROOF STEP]
by(simp only: exec_all_def)
[PROOF STATE]
proof (state)
this:
(\<sigma>, \<sigma>') \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>wf_jvm_prog\<^bsub>\<Phi>\<^esub> P; P,\<Phi> |- \<sigma> [ok]; P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, \<sigma>') \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<sigma>') \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*

goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'
[PROOF STEP]
proof(induct rule: rtrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>
 2. \<And>y z. \<lbrakk>(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*; (y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}; P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>
 2. \<And>y z. \<lbrakk>(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*; (y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}; P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>
[PROOF STEP]
by (simp add: exec_all_d_def1)
[PROOF STATE]
proof (state)
this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*; (y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}; P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*; (y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}; P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*
(y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*; (y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}; P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*
(y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y
[PROOF STEP]
have \<sigma>y: "P \<turnstile> \<sigma> -jvm\<rightarrow> y"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*
(y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y

goal (1 subgoal):
 1. P \<turnstile> \<sigma> -jvm\<rightarrow> y
[PROOF STEP]
by (simp only: exec_all_def [symmetric])
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<sigma> -jvm\<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*; (y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}; P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
have exec_d: "exec_d P y = Normal \<lfloor>z\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_d P y = Normal \<lfloor>z\<rfloor>
[PROOF STEP]
using step
     no_type_error_commutes[OF no_type_error[OF wf BV_correct[OF wf \<sigma>y cf]]]
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*
(y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y
exec_d P y = Normal (exec (P, y))

goal (1 subgoal):
 1. exec_d P y = Normal \<lfloor>z\<rfloor>
[PROOF STEP]
by (simp add: exec_all_d_def1)
[PROOF STATE]
proof (state)
this:
exec_d P y = Normal \<lfloor>z\<rfloor>

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<sigma>, y) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*; (y, z) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}; P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
using step.hyps(3) exec_1_d_NormalI[OF exec_d]
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y
P \<turnstile> Normal y -jvmd\<rightarrow>\<^sub>1 Normal z

goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z
[PROOF STEP]
by (simp add: exec_all_d_def1)
[PROOF STATE]
proof (state)
this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_TypeError_eq [iff]:
  "x \<noteq> TypeError = (\<exists>t. x = Normal t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> TypeError) = (\<exists>t. x = Normal t)
[PROOF STEP]
by (cases x) auto


[STATEMENT]
theorem (in cnf) no_type_errors:
  "P \<turnstile> (Normal \<sigma>) -jvmd\<rightarrow> \<sigma>' \<Longrightarrow> \<sigma>' \<noteq> TypeError"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> \<sigma>' \<Longrightarrow> \<sigma>' \<noteq> TypeError
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> \<sigma>' \<Longrightarrow> \<sigma>' \<noteq> TypeError
[PROOF STEP]
assume "P \<turnstile> (Normal \<sigma>) -jvmd\<rightarrow> \<sigma>'"
[PROOF STATE]
proof (state)
this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> \<sigma>'

goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> \<sigma>' \<Longrightarrow> \<sigma>' \<noteq> TypeError
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> \<sigma>'
[PROOF STEP]
have "(Normal \<sigma>, \<sigma>') \<in> (exec_1_d P)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> \<sigma>'

goal (1 subgoal):
 1. (Normal \<sigma>, \<sigma>') \<in> (exec_1_d P)\<^sup>*
[PROOF STEP]
by (unfold exec_all_d_def1) simp
[PROOF STATE]
proof (state)
this:
(Normal \<sigma>, \<sigma>') \<in> (exec_1_d P)\<^sup>*

goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> \<sigma>' \<Longrightarrow> \<sigma>' \<noteq> TypeError
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Normal \<sigma>, \<sigma>') \<in> (exec_1_d P)\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Normal \<sigma>, \<sigma>') \<in> (exec_1_d P)\<^sup>*

goal (1 subgoal):
 1. \<sigma>' \<noteq> TypeError
[PROOF STEP]
proof(induct rule: rtrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Normal \<sigma> \<noteq> TypeError
 2. \<And>y z. \<lbrakk>(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*; P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z; y \<noteq> TypeError\<rbrakk> \<Longrightarrow> z \<noteq> TypeError
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*
P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z
y \<noteq> TypeError

goal (2 subgoals):
 1. Normal \<sigma> \<noteq> TypeError
 2. \<And>y z. \<lbrakk>(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*; P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z; y \<noteq> TypeError\<rbrakk> \<Longrightarrow> z \<noteq> TypeError
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*
P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z
y \<noteq> TypeError
[PROOF STEP]
obtain y\<^sub>n where [simp]: "y = Normal y\<^sub>n"
[PROOF STATE]
proof (prove)
using this:
(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*
P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z
y \<noteq> TypeError

goal (1 subgoal):
 1. (\<And>y\<^sub>n. y = Normal y\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
y = Normal y\<^sub>n

goal (2 subgoals):
 1. Normal \<sigma> \<noteq> TypeError
 2. \<And>y z. \<lbrakk>(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*; P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z; y \<noteq> TypeError\<rbrakk> \<Longrightarrow> z \<noteq> TypeError
[PROOF STEP]
have n\<sigma>y: "P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<^sub>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<^sub>n
[PROOF STEP]
using step.hyps(1)
[PROOF STATE]
proof (prove)
using this:
(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*

goal (1 subgoal):
 1. P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<^sub>n
[PROOF STEP]
by (fold exec_all_d_def1) simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal y\<^sub>n

goal (2 subgoals):
 1. Normal \<sigma> \<noteq> TypeError
 2. \<And>y z. \<lbrakk>(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*; P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z; y \<noteq> TypeError\<rbrakk> \<Longrightarrow> z \<noteq> TypeError
[PROOF STEP]
have \<sigma>y: "P \<turnstile> \<sigma> -jvm\<rightarrow> y\<^sub>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<sigma> -jvm\<rightarrow> y\<^sub>n
[PROOF STEP]
using defensive_imp_aggressive[OF n\<sigma>y]
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<sigma> -jvm\<rightarrow> y\<^sub>n

goal (1 subgoal):
 1. P \<turnstile> \<sigma> -jvm\<rightarrow> y\<^sub>n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<sigma> -jvm\<rightarrow> y\<^sub>n

goal (2 subgoals):
 1. Normal \<sigma> \<noteq> TypeError
 2. \<And>y z. \<lbrakk>(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*; P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z; y \<noteq> TypeError\<rbrakk> \<Longrightarrow> z \<noteq> TypeError
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<noteq> TypeError
[PROOF STEP]
using step no_type_error[OF wf BV_correct[OF wf \<sigma>y cnf]]
[PROOF STATE]
proof (prove)
using this:
(Normal \<sigma>, y) \<in> (exec_1_d P)\<^sup>*
P \<turnstile> y -jvmd\<rightarrow>\<^sub>1 z
y \<noteq> TypeError
exec_d P y\<^sub>n \<noteq> TypeError

goal (1 subgoal):
 1. z \<noteq> TypeError
[PROOF STEP]
by (auto simp add: exec_1_d_eq)
[PROOF STATE]
proof (state)
this:
z \<noteq> TypeError

goal (1 subgoal):
 1. Normal \<sigma> \<noteq> TypeError
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<sigma>' \<noteq> TypeError

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bind_cong [fundef_cong]:
  assumes "xs = ys" and "\<And>x. ys = Right x \<Longrightarrow> f x = g x"
  shows "bind xs f = bind ys g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Strict_Sum.bind xs f = Strict_Sum.bind ys g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = ys
ys = sum_bot.Right ?x \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. Strict_Sum.bind xs f = Strict_Sum.bind ys g
[PROOF STEP]
by (cases ys) simp_all


[STATEMENT]
lemma bind_mono [partial_function_mono]:
  assumes mf: "mono_sum_bot B" and mg: "\<And>y. mono_sum_bot (\<lambda>f. C y f)"
  shows "mono_sum_bot (\<lambda>f. bind (B f) (\<lambda>y. C y f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone sum_bot.le_fun sum_bot_ord (\<lambda>f. Strict_Sum.bind (B f) (\<lambda>y. C y f))
[PROOF STEP]
proof (rule monotoneI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
fix f g :: "'a \<Rightarrow> 'b +\<^sub>\<bottom> 'c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
assume fg: "fun_ord sum_bot_ord f g"
[PROOF STATE]
proof (state)
this:
sum_bot.le_fun f g

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
with mf
[PROOF STATE]
proof (chain)
picking this:
monotone sum_bot.le_fun sum_bot_ord B
sum_bot.le_fun f g
[PROOF STEP]
have "sum_bot_ord (B f) (B g)"
[PROOF STATE]
proof (prove)
using this:
monotone sum_bot.le_fun sum_bot_ord B
sum_bot.le_fun f g

goal (1 subgoal):
 1. sum_bot_ord (B f) (B g)
[PROOF STEP]
by (rule monotoneD [of _ _ _ f g])
[PROOF STATE]
proof (state)
this:
sum_bot_ord (B f) (B g)

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_bot_ord (B f) (B g)
[PROOF STEP]
have "sum_bot_ord (bind (B f) (\<lambda>y. C y f)) (bind (B g) (\<lambda>y. C y f))"
[PROOF STATE]
proof (prove)
using this:
sum_bot_ord (B f) (B g)

goal (1 subgoal):
 1. sum_bot_ord (Strict_Sum.bind (B f) (\<lambda>y. C y f)) (Strict_Sum.bind (B g) (\<lambda>y. C y f))
[PROOF STEP]
unfolding flat_ord_def
[PROOF STATE]
proof (prove)
using this:
B f = Bottom \<or> B f = B g

goal (1 subgoal):
 1. Strict_Sum.bind (B f) (\<lambda>y. C y f) = Bottom \<or> Strict_Sum.bind (B f) (\<lambda>y. C y f) = Strict_Sum.bind (B g) (\<lambda>y. C y f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum_bot_ord (Strict_Sum.bind (B f) (\<lambda>y. C y f)) (Strict_Sum.bind (B g) (\<lambda>y. C y f))

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_bot_ord (Strict_Sum.bind (B f) (\<lambda>y. C y f)) (Strict_Sum.bind (B g) (\<lambda>y. C y f))

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
from mg
[PROOF STATE]
proof (chain)
picking this:
monotone sum_bot.le_fun sum_bot_ord (C ?y)
[PROOF STEP]
have "\<And>y'. sum_bot_ord (C y' f) (C y' g)"
[PROOF STATE]
proof (prove)
using this:
monotone sum_bot.le_fun sum_bot_ord (C ?y)

goal (1 subgoal):
 1. \<And>y'. sum_bot_ord (C y' f) (C y' g)
[PROOF STEP]
by (rule monotoneD) (rule fg)
[PROOF STATE]
proof (state)
this:
sum_bot_ord (C ?y' f) (C ?y' g)

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_bot_ord (C ?y' f) (C ?y' g)
[PROOF STEP]
have "sum_bot_ord (bind (B g) (\<lambda>y'. C y' f)) (bind (B g) (\<lambda>y'. C y' g))"
[PROOF STATE]
proof (prove)
using this:
sum_bot_ord (C ?y' f) (C ?y' g)

goal (1 subgoal):
 1. sum_bot_ord (Strict_Sum.bind (B g) (\<lambda>y'. C y' f)) (Strict_Sum.bind (B g) (\<lambda>y'. C y' g))
[PROOF STEP]
unfolding flat_ord_def
[PROOF STATE]
proof (prove)
using this:
C ?y' f = Bottom \<or> C ?y' f = C ?y' g

goal (1 subgoal):
 1. Strict_Sum.bind (B g) (\<lambda>y'. C y' f) = Bottom \<or> Strict_Sum.bind (B g) (\<lambda>y'. C y' f) = Strict_Sum.bind (B g) (\<lambda>y'. C y' g)
[PROOF STEP]
by (cases "B g") auto
[PROOF STATE]
proof (state)
this:
sum_bot_ord (Strict_Sum.bind (B g) (\<lambda>y'. C y' f)) (Strict_Sum.bind (B g) (\<lambda>y'. C y' g))

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (Strict_Sum.bind (B x) (\<lambda>y. C y x)) (Strict_Sum.bind (B y) (\<lambda>ya. C ya y))
[PROOF STEP]
finally (sum_bot.leq_trans)
[PROOF STATE]
proof (chain)
picking this:
sum_bot_ord (Strict_Sum.bind (B f) (\<lambda>y. C y f)) (Strict_Sum.bind (B g) (\<lambda>y'. C y' g))
[PROOF STEP]
show "sum_bot_ord (bind (B f) (\<lambda>y. C y f)) (bind (B g) (\<lambda>y'. C y' g))"
[PROOF STATE]
proof (prove)
using this:
sum_bot_ord (Strict_Sum.bind (B f) (\<lambda>y. C y f)) (Strict_Sum.bind (B g) (\<lambda>y'. C y' g))

goal (1 subgoal):
 1. sum_bot_ord (Strict_Sum.bind (B f) (\<lambda>y. C y f)) (Strict_Sum.bind (B g) (\<lambda>y'. C y' g))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum_bot_ord (Strict_Sum.bind (B f) (\<lambda>y. C y f)) (Strict_Sum.bind (B g) (\<lambda>y'. C y' g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma catch_mono [partial_function_mono]:
  assumes mf: "mono_sum_bot B" and mg: "\<And>y. mono_sum_bot (\<lambda>f. C y f)"
  shows "mono_sum_bot (\<lambda>f. try (B f) catch (\<lambda>y. C y f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone sum_bot.le_fun sum_bot_ord (\<lambda>f. try B f catch (\<lambda>y. C y f))
[PROOF STEP]
proof (rule monotoneI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
fix f g :: "'a \<Rightarrow> 'b +\<^sub>\<bottom> 'c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
assume fg: "fun_ord sum_bot_ord f g"
[PROOF STATE]
proof (state)
this:
sum_bot.le_fun f g

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
with mf
[PROOF STATE]
proof (chain)
picking this:
monotone sum_bot.le_fun sum_bot_ord B
sum_bot.le_fun f g
[PROOF STEP]
have "sum_bot_ord (B f) (B g)"
[PROOF STATE]
proof (prove)
using this:
monotone sum_bot.le_fun sum_bot_ord B
sum_bot.le_fun f g

goal (1 subgoal):
 1. sum_bot_ord (B f) (B g)
[PROOF STEP]
by (rule monotoneD [of _ _ _ f g])
[PROOF STATE]
proof (state)
this:
sum_bot_ord (B f) (B g)

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_bot_ord (B f) (B g)
[PROOF STEP]
have "sum_bot_ord (try (B f) catch (\<lambda>y. C y f)) (try (B g) catch (\<lambda>y. C y f))"
[PROOF STATE]
proof (prove)
using this:
sum_bot_ord (B f) (B g)

goal (1 subgoal):
 1. sum_bot_ord (try B f catch (\<lambda>y. C y f)) (try B g catch (\<lambda>y. C y f))
[PROOF STEP]
unfolding flat_ord_def
[PROOF STATE]
proof (prove)
using this:
B f = Bottom \<or> B f = B g

goal (1 subgoal):
 1. (try B f catch (\<lambda>y. C y f)) = Bottom \<or> (try B f catch (\<lambda>y. C y f)) = (try B g catch (\<lambda>y. C y f))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum_bot_ord (try B f catch (\<lambda>y. C y f)) (try B g catch (\<lambda>y. C y f))

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_bot_ord (try B f catch (\<lambda>y. C y f)) (try B g catch (\<lambda>y. C y f))

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
from mg
[PROOF STATE]
proof (chain)
picking this:
monotone sum_bot.le_fun sum_bot_ord (C ?y)
[PROOF STEP]
have "\<And>y'. sum_bot_ord (C y' f) (C y' g)"
[PROOF STATE]
proof (prove)
using this:
monotone sum_bot.le_fun sum_bot_ord (C ?y)

goal (1 subgoal):
 1. \<And>y'. sum_bot_ord (C y' f) (C y' g)
[PROOF STEP]
by (rule monotoneD) (rule fg)
[PROOF STATE]
proof (state)
this:
sum_bot_ord (C ?y' f) (C ?y' g)

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_bot_ord (C ?y' f) (C ?y' g)
[PROOF STEP]
have "sum_bot_ord (try (B g) catch (\<lambda>y'. C y' f)) (try (B g) catch (\<lambda>y'. C y' g))"
[PROOF STATE]
proof (prove)
using this:
sum_bot_ord (C ?y' f) (C ?y' g)

goal (1 subgoal):
 1. sum_bot_ord (try B g catch (\<lambda>y'. C y' f)) (try B g catch (\<lambda>y'. C y' g))
[PROOF STEP]
unfolding flat_ord_def
[PROOF STATE]
proof (prove)
using this:
C ?y' f = Bottom \<or> C ?y' f = C ?y' g

goal (1 subgoal):
 1. (try B g catch (\<lambda>y'. C y' f)) = Bottom \<or> (try B g catch (\<lambda>y'. C y' f)) = (try B g catch (\<lambda>y'. C y' g))
[PROOF STEP]
by (cases "B g") auto
[PROOF STATE]
proof (state)
this:
sum_bot_ord (try B g catch (\<lambda>y'. C y' f)) (try B g catch (\<lambda>y'. C y' g))

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (try B x catch (\<lambda>y. C y x)) (try B y catch (\<lambda>ya. C ya y))
[PROOF STEP]
finally (sum_bot.leq_trans)
[PROOF STATE]
proof (chain)
picking this:
sum_bot_ord (try B f catch (\<lambda>y. C y f)) (try B g catch (\<lambda>y'. C y' g))
[PROOF STEP]
show "sum_bot_ord (try (B f) catch (\<lambda>y. C y f)) (try (B g) catch (\<lambda>y'. C y' g))"
[PROOF STATE]
proof (prove)
using this:
sum_bot_ord (try B f catch (\<lambda>y. C y f)) (try B g catch (\<lambda>y'. C y' g))

goal (1 subgoal):
 1. sum_bot_ord (try B f catch (\<lambda>y. C y f)) (try B g catch (\<lambda>y'. C y' g))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum_bot_ord (try B f catch (\<lambda>y. C y f)) (try B g catch (\<lambda>y'. C y' g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_sum_bot_cong [fundef_cong]:
  assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> f x = g x"
  shows "map_sum_bot f xs = map_sum_bot g ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_sum_bot f xs = map_sum_bot g ys
[PROOF STEP]
unfolding assms(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_sum_bot f ys = map_sum_bot g ys
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
?x \<in> set ys \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. map_sum_bot f ys = map_sum_bot g ys
[PROOF STEP]
by (induct ys) auto


[STATEMENT]
lemma map_sum_bot_mono [partial_function_mono]:
  fixes C :: "'a \<Rightarrow> ('b \<Rightarrow> ('e +\<^sub>\<bottom> 'c)) \<Rightarrow> 'e +\<^sub>\<bottom> 'd"
  assumes "\<And>y. y \<in> set B \<Longrightarrow> mono_sum_bot (C y)"
  shows "mono_sum_bot (\<lambda>f. map_sum_bot (\<lambda>y. C y f) B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone sum_bot.le_fun sum_bot_ord (\<lambda>f. map_sum_bot (\<lambda>y. C y f) B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?y \<in> set B \<Longrightarrow> monotone sum_bot.le_fun sum_bot_ord (C ?y)

goal (1 subgoal):
 1. monotone sum_bot.le_fun sum_bot_ord (\<lambda>f. map_sum_bot (\<lambda>y. C y f) B)
[PROOF STEP]
by (induct B) (auto intro!: partial_function_mono)


[STATEMENT]
lemma [code]:
  "bind (sumbot a) f = (case a of Inl b \<Rightarrow> sumbot (Inl b) | Inr a \<Rightarrow> f a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumbot a \<bind> f = (case a of Inl b \<Rightarrow> sumbot (Inl b) | Inr a \<Rightarrow> f a)
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma [code]:
  "(try (sumbot a) catch f) = (case a of Inl b \<Rightarrow> f b | Inr a \<Rightarrow> sumbot (Inr a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (try sumbot a catch f) = (case a of Inl b \<Rightarrow> f b | Inr a \<Rightarrow> sumbot (Inr a))
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma [code]: "Right x = sumbot (Inr x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_bot.Right x = sumbot (Inr x)
[PROOF STEP]
by simp


[STATEMENT]
lemma [code]: "Left x = sumbot (Inl x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_bot.Left x = sumbot (Inl x)
[PROOF STEP]
by simp


[STATEMENT]
lemma [code]: "return x = sumbot (Inr x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return x = sumbot (Inr x)
[PROOF STEP]
by simp


[STATEMENT]
lemma [code]: "error x = sumbot (Inl x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. error x = sumbot (Inl x)
[PROOF STEP]
by simp


[STATEMENT]
lemma [code]:
  "case_sum_bot f g h (sumbot p) = case_sum g h p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case sumbot p of Bottom \<Rightarrow> f | sum_bot.Left x \<Rightarrow> g x | sum_bot.Right x \<Rightarrow> h x) = (case p of Inl x \<Rightarrow> g x | Inr x \<Rightarrow> h x)
[PROOF STEP]
by (cases p) auto


[STATEMENT]
lemma sum_bot_map_mono [partial_function_mono]:
  assumes mf: "mono_sum_bot B"
  shows "mono_sum_bot (\<lambda>f. sum_bot_map h (B f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone sum_bot.le_fun sum_bot_ord (\<lambda>f. sum_bot_map h (B f))
[PROOF STEP]
proof (rule monotoneI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (sum_bot_map h (B x)) (sum_bot_map h (B y))
[PROOF STEP]
fix f g :: "'a \<Rightarrow> 'b +\<^sub>\<bottom> 'c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (sum_bot_map h (B x)) (sum_bot_map h (B y))
[PROOF STEP]
assume fg: "fun_ord sum_bot_ord f g"
[PROOF STATE]
proof (state)
this:
sum_bot.le_fun f g

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (sum_bot_map h (B x)) (sum_bot_map h (B y))
[PROOF STEP]
with mf
[PROOF STATE]
proof (chain)
picking this:
monotone sum_bot.le_fun sum_bot_ord B
sum_bot.le_fun f g
[PROOF STEP]
have "sum_bot_ord (B f) (B g)"
[PROOF STATE]
proof (prove)
using this:
monotone sum_bot.le_fun sum_bot_ord B
sum_bot.le_fun f g

goal (1 subgoal):
 1. sum_bot_ord (B f) (B g)
[PROOF STEP]
by (rule monotoneD [of _ _ _ f g])
[PROOF STATE]
proof (state)
this:
sum_bot_ord (B f) (B g)

goal (1 subgoal):
 1. \<And>x y. sum_bot.le_fun x y \<Longrightarrow> sum_bot_ord (sum_bot_map h (B x)) (sum_bot_map h (B y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_bot_ord (B f) (B g)
[PROOF STEP]
show "sum_bot_ord (sum_bot_map h (B f)) (sum_bot_map h (B g))"
[PROOF STATE]
proof (prove)
using this:
sum_bot_ord (B f) (B g)

goal (1 subgoal):
 1. sum_bot_ord (sum_bot_map h (B f)) (sum_bot_map h (B g))
[PROOF STEP]
unfolding flat_ord_def
[PROOF STATE]
proof (prove)
using this:
B f = Bottom \<or> B f = B g

goal (1 subgoal):
 1. sum_bot_map h (B f) = Bottom \<or> sum_bot_map h (B f) = sum_bot_map h (B g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum_bot_ord (sum_bot_map h (B f)) (sum_bot_map h (B g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma euclid2:
  "PRE (\<lambda>s::nat store. s ''x'' = x \<and> s ''y'' = y)
   (WHILE (\<lambda>s. s ''y'' \<noteq> 0) INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y)
    DO
     (''z'' ::= (\<lambda>s. s ''y''));
     (''y'' ::= (\<lambda>s. s ''x'' mod s ''y''));
     (''x'' ::= (\<lambda>s. s ''z''))
    OD)
   POST (\<lambda>s. s ''x'' = gcd x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. s ''x'' = x \<and> s ''y'' = y\<rceil> \<subseteq> wp (WHILE (\<lambda>s. s ''y'' \<noteq> 0) INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) DO (''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')) OD) \<lceil>\<lambda>s. s ''x'' = gcd x y\<rceil>
[PROOF STEP]
apply hoare
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. rdom \<lceil>\<lambda>s. s ''x'' = x \<and> s ''y'' = y\<rceil> \<subseteq> rdom \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil>
 2. rdom \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil> ; rel_ad \<lceil>\<lambda>s. s ''y'' \<noteq> 0\<rceil> \<subseteq> rdom \<lceil>\<lambda>s. s ''x'' = gcd x y\<rceil>
 3. rdom \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil> ; rdom \<lceil>\<lambda>s. s ''y'' \<noteq> 0\<rceil> \<subseteq> wp (''z'' ::= (\<lambda>s. s ''y'')) (wp (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) (wp (''x'' ::= (\<lambda>s. s ''z'')) \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil>))
[PROOF STEP]
using gcd_red_nat
[PROOF STATE]
proof (prove)
using this:
gcd ?x ?y = gcd ?y (?x mod ?y)

goal (3 subgoals):
 1. rdom \<lceil>\<lambda>s. s ''x'' = x \<and> s ''y'' = y\<rceil> \<subseteq> rdom \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil>
 2. rdom \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil> ; rel_ad \<lceil>\<lambda>s. s ''y'' \<noteq> 0\<rceil> \<subseteq> rdom \<lceil>\<lambda>s. s ''x'' = gcd x y\<rceil>
 3. rdom \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil> ; rdom \<lceil>\<lambda>s. s ''y'' \<noteq> 0\<rceil> \<subseteq> wp (''z'' ::= (\<lambda>s. s ''y'')) (wp (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) (wp (''x'' ::= (\<lambda>s. s ''z'')) \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil>))
[PROOF STEP]
by auto


[STATEMENT]
lemma euclid_diff2:
   "PRE (\<lambda>s::nat store. s ''x'' = x \<and> s ''y'' = y \<and> x > 0 \<and> y > 0)
    (WHILE (\<lambda>s. s ''x''\<noteq> s ''y'') INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y)
     DO
        (IF (\<lambda>s. s ''x'' >  s ''y'')
         THEN (''x'' ::= (\<lambda>s. s ''x'' - s ''y''))
         ELSE (''y'' ::= (\<lambda>s. s ''y'' - s ''x''))
         FI)
    OD)
    POST (\<lambda>s. s ''x'' = gcd x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. s ''x'' = x \<and> s ''y'' = y \<and> 0 < x \<and> 0 < y\<rceil> \<subseteq> wp (WHILE (\<lambda>s. s ''x'' \<noteq> s ''y'') INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) DO (IF (\<lambda>s. s ''y'' < s ''x'') THEN (''x'' ::= (\<lambda>s. s ''x'' - s ''y'')) ELSE (''y'' ::= (\<lambda>s. s ''y'' - s ''x'')) FI) OD) \<lceil>\<lambda>s. s ''x'' = gcd x y\<rceil>
[PROOF STEP]
apply (hoare, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>s. gcd (s ''x'') (s ''y'') = gcd x y \<and> s ''x'' = s ''y'' \<longrightarrow> s ''y'' = gcd x y
 2. \<forall>s. gcd (s ''x'') (s ''y'') = gcd x y \<and> s ''x'' \<noteq> s ''y'' \<longrightarrow> (s ''y'' < s ''x'' \<longrightarrow> gcd (s ''x'' - s ''y'') (s ''y'') = gcd x y) \<and> (s ''y'' < s ''x'' \<or> gcd (s ''x'') (s ''y'' - s ''x'') = gcd x y)
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. gcd (s ''x'') (s ''y'') = gcd x y \<and> s ''x'' \<noteq> s ''y'' \<longrightarrow> (s ''y'' < s ''x'' \<longrightarrow> gcd (s ''x'' - s ''y'') (s ''y'') = gcd x y) \<and> (s ''y'' < s ''x'' \<or> gcd (s ''x'') (s ''y'' - s ''x'') = gcd x y)
[PROOF STEP]
by (metis gcd.commute gcd_diff1_nat le_cases nat_less_le)


[STATEMENT]
lemma integer_division2:
  "PRE (\<lambda>s::nat store. x \<ge> 0)
    (''q'' ::= (\<lambda>s. 0));
    (''r'' ::= (\<lambda>s. x));
    (WHILE (\<lambda>s. y \<le> s ''r'') INV (\<lambda>s. x = s ''q'' * y + s ''r'' \<and> s ''r'' \<ge> 0)
     DO
      (''q'' ::= (\<lambda>s. s ''q'' + 1));
      (''r'' ::= (\<lambda>s. s ''r'' - y))
      OD)
   POST (\<lambda>s. x = s ''q'' * y + s ''r'' \<and> s ''r'' \<ge> 0 \<and> s ''r'' < y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. 0 \<le> x\<rceil> \<subseteq> wp ((''q'' ::= (\<lambda>s. 0)) ; (''r'' ::= (\<lambda>s. x)) ; (WHILE (\<lambda>s. y \<le> s ''r'') INV (\<lambda>s. x = s ''q'' \<cdot> y + s ''r'' \<and> 0 \<le> s ''r'') DO (''q'' ::= (\<lambda>s. s ''q'' + 1)) ; (''r'' ::= (\<lambda>s. s ''r'' - y)) OD)) \<lceil>\<lambda>s. x = s ''q'' \<cdot> y + s ''r'' \<and> 0 \<le> s ''r'' \<and> s ''r'' < y\<rceil>
[PROOF STEP]
by hoare simp_all


[STATEMENT]
lemma factorial2:
  "PRE (\<lambda>s::nat store. True)
   (''x'' ::= (\<lambda>s. 0));
   (''y'' ::= (\<lambda>s. 1));
   (WHILE (\<lambda>s. s ''x'' \<noteq> x0) INV (\<lambda>s. s ''y'' = fact (s ''x''))
   DO
     (''x'' ::= (\<lambda>s. s ''x'' + 1));
     (''y'' ::= (\<lambda>s. s ''y'' \<cdot> s ''x''))
   OD)
   POST (\<lambda>s. s ''y'' = fact x0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. True\<rceil> \<subseteq> wp ((''x'' ::= (\<lambda>s. 0)) ; (''y'' ::= (\<lambda>s. 1)) ; (WHILE (\<lambda>s. s ''x'' \<noteq> x0) INV (\<lambda>s. s ''y'' = fact (s ''x'')) DO (''x'' ::= (\<lambda>s. s ''x'' + 1)) ; (''y'' ::= (\<lambda>s. s ''y'' \<cdot> s ''x'')) OD)) \<lceil>\<lambda>s. s ''y'' = fact x0\<rceil>
[PROOF STEP]
by hoare simp_all


[STATEMENT]
lemma my_power2:
  "PRE (\<lambda>s::nat store. True)
   (''i'' ::= (\<lambda>s. 0));
   (''y'' ::= (\<lambda>s. 1));
   (WHILE (\<lambda>s. s ''i'' < n) INV (\<lambda>s. s ''y'' = x ^ (s ''i'') \<and> s ''i'' \<le> n)
     DO
       (''y'' ::= (\<lambda>s. (s ''y'') * x));
       (''i'' ::= (\<lambda>s. s ''i'' + 1))
     OD)
   POST (\<lambda>s. s ''y'' = x ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. True\<rceil> \<subseteq> wp ((''i'' ::= (\<lambda>s. 0)) ; (''y'' ::= (\<lambda>s. 1)) ; (WHILE (\<lambda>s. s ''i'' < n) INV (\<lambda>s. s ''y'' = x ^ s ''i'' \<and> s ''i'' \<le> n) DO (''y'' ::= (\<lambda>s. s ''y'' \<cdot> x)) ; (''i'' ::= (\<lambda>s. s ''i'' + 1)) OD)) \<lceil>\<lambda>s. s ''y'' = x ^ n\<rceil>
[PROOF STEP]
by hoare auto


[STATEMENT]
lemma imp_reverse2:
  "PRE (\<lambda>s:: 'a list store. s ''x'' = X)
   (''y'' ::= (\<lambda>s. []));
   (WHILE (\<lambda>s. s ''x'' \<noteq> []) INV (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
    DO
     (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y''));
     (''x'' ::= (\<lambda>s. tl (s ''x'')))
    OD)
   POST (\<lambda>s. s ''y''= rev X )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. s ''x'' = X\<rceil> \<subseteq> wp ((''y'' ::= (\<lambda>s. [])) ; (WHILE (\<lambda>s. s ''x'' \<noteq> []) INV (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X) DO (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y'')) ; (''x'' ::= (\<lambda>s. tl (s ''x''))) OD)) \<lceil>\<lambda>s. s ''y'' = rev X\<rceil>
[PROOF STEP]
apply (hoare, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>s. rev (s ''x'') @ s ''y'' = rev X \<and> s ''x'' = [] \<longrightarrow> s ''y'' = rev X
 2. \<forall>s. rev (s ''x'') @ s ''y'' = rev X \<and> s ''x'' \<noteq> [] \<longrightarrow> rev (tl (s ''x'')) @ hd (s ''x'') # s ''y'' = rev X
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. rev (s ''x'') @ s ''y'' = rev X \<and> s ''x'' \<noteq> [] \<longrightarrow> rev (tl (s ''x'')) @ hd (s ''x'') # s ''y'' = rev X
[PROOF STEP]
by (clarsimp, metis append.simps append_assoc hd_Cons_tl rev.simps(2))


[STATEMENT]
lemma sum_list_hd_tl:
  fixes xs :: "(_ :: group_add) list"
  shows "xs \<noteq> [] \<Longrightarrow> sum_list (tl xs) = (- hd xs) + sum_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> sum_list (tl xs) = - hd xs + sum_list xs
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma finite_distinct_bounded: "finite A \<Longrightarrow> finite {xs. distinct xs \<and> set xs \<subseteq> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> finite {xs. distinct xs \<and> set xs \<subseteq> A}
[PROOF STEP]
apply (rule finite_subset[of _ "\<Union>n \<in> {0 .. card A}. {xs.  length xs = n \<and> distinct xs \<and> set xs \<subseteq> A}"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite A \<Longrightarrow> {xs. distinct xs \<and> set xs \<subseteq> A} \<subseteq> (\<Union>n\<in>{0..card A}. {xs. length xs = n \<and> distinct xs \<and> set xs \<subseteq> A})
 2. finite A \<Longrightarrow> finite (\<Union>n\<in>{0..card A}. {xs. length xs = n \<and> distinct xs \<and> set xs \<subseteq> A})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> {xs. distinct xs \<and> set xs \<subseteq> A} \<subseteq> (\<Union>n\<in>{0..card A}. {xs. length xs = n \<and> distinct xs \<and> set xs \<subseteq> A})
[PROOF STEP]
by clarsimp (metis card_mono distinct_card)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> finite (\<Union>n\<in>{0..card A}. {xs. length xs = n \<and> distinct xs \<and> set xs \<subseteq> A})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> finite (\<Union>n\<in>{0..card A}. {xs. length xs = n \<and> distinct xs \<and> set xs \<subseteq> A})
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Sum_eq_pick_changed_elem:
  assumes "finite M"
    and "m \<in> M" "f m = g m + \<Delta>"
    and "\<And>n. n \<noteq> m \<and> n \<in> M \<Longrightarrow> f n = g n"
  shows "(\<Sum>x\<in>M. f x) = (\<Sum>x\<in>M. g x) + \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f M = sum g M + \<Delta>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite M
m \<in> M
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> M \<Longrightarrow> f ?n = g ?n

goal (1 subgoal):
 1. sum f M = sum g M + \<Delta>
[PROOF STEP]
proof (induct M arbitrary: m rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>m \<in> {}; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> {} \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f {} = sum g {} + \<Delta>
 2. \<And>x F m. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
m \<in> {}
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> {} \<Longrightarrow> f ?n = g ?n

goal (2 subgoals):
 1. \<And>m. \<lbrakk>m \<in> {}; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> {} \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f {} = sum g {} + \<Delta>
 2. \<And>x F m. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> {}
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> {} \<Longrightarrow> f ?n = g ?n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m \<in> {}
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> {} \<Longrightarrow> f ?n = g ?n

goal (1 subgoal):
 1. sum f {} = sum g {} + \<Delta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {} = sum g {} + \<Delta>

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n

goal (1 subgoal):
 1. sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
proof (cases "x=m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x = m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
 2. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x \<noteq> m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = m

goal (2 subgoals):
 1. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x = m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
 2. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x \<noteq> m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
with insert
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n
x = m
[PROOF STEP]
have "sum f F = sum g F"
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n
x = m

goal (1 subgoal):
 1. sum f F = sum g F
[PROOF STEP]
by (intro sum.cong[OF refl]) force
[PROOF STATE]
proof (state)
this:
sum f F = sum g F

goal (2 subgoals):
 1. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x = m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
 2. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x \<noteq> m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
with insert True
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n
x = m
sum f F = sum g F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n
x = m
sum f F = sum g F

goal (1 subgoal):
 1. sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
by (auto simp: add.commute add.left_commute)
[PROOF STATE]
proof (state)
this:
sum f (insert x F) = sum g (insert x F) + \<Delta>

goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x \<noteq> m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x \<noteq> m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> m

goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>; m \<in> insert x F; f m = g m + \<Delta>; \<And>n. n \<noteq> m \<and> n \<in> insert x F \<Longrightarrow> f n = g n; x \<noteq> m\<rbrakk> \<Longrightarrow> sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
with insert
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n
x \<noteq> m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>?m \<in> F; f ?m = g ?m + \<Delta>; \<And>n. n \<noteq> ?m \<and> n \<in> F \<Longrightarrow> f n = g n\<rbrakk> \<Longrightarrow> sum f F = sum g F + \<Delta>
m \<in> insert x F
f m = g m + \<Delta>
?n \<noteq> m \<and> ?n \<in> insert x F \<Longrightarrow> f ?n = g ?n
x \<noteq> m

goal (1 subgoal):
 1. sum f (insert x F) = sum g (insert x F) + \<Delta>
[PROOF STEP]
by (auto simp: add.assoc)
[PROOF STATE]
proof (state)
this:
sum f (insert x F) = sum g (insert x F) + \<Delta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum f (insert x F) = sum g (insert x F) + \<Delta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_pos_ex_elem_pos: "(0::int) < (\<Sum>m\<in>M. f m) \<Longrightarrow> \<exists>m\<in>M. 0 < f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < sum f M \<Longrightarrow> \<exists>m\<in>M. 0 < f m
[PROOF STEP]
by (meson not_le sum_nonpos)


[STATEMENT]
lemma sum_if_distrib_add: "finite A \<Longrightarrow> b \<in> A \<Longrightarrow> (\<Sum>a\<in>A. if a=b then X b + Y a else X a) = (\<Sum>a\<in>A. X a) + Y b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; b \<in> A\<rbrakk> \<Longrightarrow> (\<Sum>a\<in>A. if a = b then X b + Y a else X a) = sum X A + Y b
[PROOF STEP]
by (simp add: Sum_eq_pick_changed_elem)


[STATEMENT]
lemma (in order) order_finite_set_exists_foundation:
  fixes   t :: 'a
  assumes "finite M"
    and   "t \<in> M"
  shows   "\<exists>s\<in>M. s \<le> t \<and> (\<forall>u\<in>M. \<not> u < s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<in>M. s \<le> t \<and> (\<forall>u\<in>M. \<not> u < s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite M
t \<in> M

goal (1 subgoal):
 1. \<exists>s\<in>M. s \<le> t \<and> (\<forall>u\<in>M. \<not> u < s)
[PROOF STEP]
by (simp add: dual_order.strict_iff_order finite_has_minimal2)


[STATEMENT]
lemma order_finite_set_obtain_foundation:
  fixes   t :: "_ :: order"
  assumes "finite M"
    and   "t \<in> M"
  obtains s where "s \<in> M" "s \<le> t" "\<forall>u\<in>M. \<not> u < s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> M; s \<le> t; \<forall>u\<in>M. \<not> u < s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms order_finite_set_exists_foundation
[PROOF STATE]
proof (prove)
using this:
finite M
t \<in> M
\<lbrakk>finite ?M; ?t \<in> ?M\<rbrakk> \<Longrightarrow> \<exists>s\<in>?M. s \<le> ?t \<and> (\<forall>u\<in>?M. \<not> u < s)

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> M; s \<le> t; \<forall>u\<in>M. \<not> u < s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma finite_nonzero_count: "finite {t. count M t > 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. 0 < count M t}
[PROOF STEP]
using count
[PROOF STATE]
proof (prove)
using this:
count ?x \<in> {f. finite {x. 0 < f x}}

goal (1 subgoal):
 1. finite {t. 0 < count M t}
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_count[simp]: "finite {t. count M t > i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. i < count M t}
[PROOF STEP]
by (rule finite_subset[OF _ finite_nonzero_count[of M]]) (auto simp only: set_mset_def)


[STATEMENT]
lemma zcount_zmset_of_nonneg[simp]: "0 \<le> zcount (zmset_of M) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> zcount (zmset_of M) t
[PROOF STEP]
by simp


[STATEMENT]
lemma finite_zcount_pos[simp]: "finite {t. zcount M t > 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. 0 < zcount M t}
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. finite {t. 0 < (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t}
[PROOF STEP]
subgoal for M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. 0 < (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t}
[PROOF STEP]
apply (rule finite_subset[OF _ finite_Un[THEN iffD2, OF conjI[OF finite_nonzero_count finite_nonzero_count]], of _ "fst M" "snd M"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t. 0 < (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t} \<subseteq> {t. 0 < count (fst M) t} \<union> {t. 0 < count (snd M) t}
[PROOF STEP]
apply (auto simp only: set_mset_def fst_conv snd_conv split: prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_zcount_neg[simp]: "finite {t. zcount M t < 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. zcount M t < 0}
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. finite {t. (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t < 0}
[PROOF STEP]
subgoal for M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t < 0}
[PROOF STEP]
apply (rule finite_subset[OF _ finite_Un[THEN iffD2, OF conjI[OF finite_nonzero_count finite_nonzero_count]], of _ "fst M" "snd M"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t. (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t < 0} \<subseteq> {t. 0 < count (fst M) t} \<union> {t. 0 < count (snd M) t}
[PROOF STEP]
apply (auto simp only: set_mset_def fst_conv snd_conv split: prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pos_zcount_in_zmset: "0 < zcount M x \<Longrightarrow> x \<in>#\<^sub>z M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount M x \<Longrightarrow> x \<in>#\<^sub>z M
[PROOF STEP]
by (simp add: zcount_inI)


[STATEMENT]
lemma zmset_elem_nonneg: "x \<in>#\<^sub>z M \<Longrightarrow> (\<And>x. x \<in>#\<^sub>z M \<Longrightarrow> 0 \<le> zcount M x) \<Longrightarrow> 0 < zcount M x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in>#\<^sub>z M; \<And>x. x \<in>#\<^sub>z M \<Longrightarrow> 0 \<le> zcount M x\<rbrakk> \<Longrightarrow> 0 < zcount M x
[PROOF STEP]
by (simp add: order.order_iff_strict zcount_eq_zero_iff)


[STATEMENT]
lemma zero_le_sum_single: "0 \<le> zcount (\<Sum>x\<in>M. {#f x#}\<^sub>z) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> zcount (\<Sum>x\<in>M. {#f x#}\<^sub>z) t
[PROOF STEP]
by (induct M rule: infinite_finite_induct) auto


[STATEMENT]
lemma mem_zmset_of[simp]: "x \<in>#\<^sub>z zmset_of M \<longleftrightarrow> x \<in># M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in>#\<^sub>z zmset_of M) = (x \<in># M)
[PROOF STEP]
by (simp add: set_zmset_def)


[STATEMENT]
lemma mset_neg_minus: "mset_neg (abs_zmultiset (Mp,Mn)) = Mn-Mp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_neg (abs_zmultiset (Mp, Mn)) = Mn - Mp
[PROOF STEP]
by (simp add: mset_neg.abs_eq)


[STATEMENT]
lemma mset_pos_minus: "mset_pos (abs_zmultiset (Mp,Mn)) = Mp-Mn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_pos (abs_zmultiset (Mp, Mn)) = Mp - Mn
[PROOF STEP]
by (simp add: mset_pos.abs_eq)


[STATEMENT]
lemma mset_neg_sum_set: "(\<And>m. m \<in> M \<Longrightarrow> mset_neg (f m) = {#}) \<Longrightarrow> mset_neg (\<Sum>m\<in>M. f m) = {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> M \<Longrightarrow> mset_neg (f m) = {#}) \<Longrightarrow> mset_neg (sum f M) = {#}
[PROOF STEP]
by (induct M rule: infinite_finite_induct) auto


[STATEMENT]
lemma mset_neg_empty_iff: "mset_neg M = {#} \<longleftrightarrow> (\<forall>t. 0 \<le> zcount M t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mset_neg M = {#}) = (\<forall>t. 0 \<le> zcount M t)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mset_neg M = {#} \<Longrightarrow> \<forall>t. 0 \<le> zcount M t
 2. \<forall>t. 0 \<le> zcount M t \<Longrightarrow> mset_neg M = {#}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_neg M = {#} \<Longrightarrow> \<forall>t. 0 \<le> zcount M t
[PROOF STEP]
by (metis add.commute add.right_neutral mset_pos_as_neg zcount_zmset_of_nonneg zmset_of_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 \<le> zcount M t \<Longrightarrow> mset_neg M = {#}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 \<le> zcount M t \<Longrightarrow> mset_neg M = {#}
[PROOF STEP]
apply (induct rule: zmultiset.abs_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<forall>t. 0 \<le> zcount (abs_zmultiset y) t \<Longrightarrow> mset_neg (abs_zmultiset y) = {#}
[PROOF STEP]
subgoal for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. 0 \<le> zcount (abs_zmultiset y) t \<Longrightarrow> mset_neg (abs_zmultiset y) = {#}
[PROOF STEP]
apply (induct y)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<forall>t. 0 \<le> zcount (abs_zmultiset (a, b)) t \<Longrightarrow> mset_neg (abs_zmultiset (a, b)) = {#}
[PROOF STEP]
apply (subst mset_neg_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<forall>t. 0 \<le> zcount (abs_zmultiset (a, b)) t \<Longrightarrow> b - a = {#}
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<forall>t. 0 \<le> (case (a, b) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t \<Longrightarrow> b - a = {#}
[PROOF STEP]
apply (simp add: Diff_eq_empty_iff_mset mset_subset_eqI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mset_neg_zcount_nonneg: "mset_neg M = {#} \<Longrightarrow> 0 \<le> zcount M t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_neg M = {#} \<Longrightarrow> 0 \<le> zcount M t
[PROOF STEP]
by (subst (asm) mset_neg_empty_iff) simp


[STATEMENT]
lemma in_zmset_conv_pos_neg_disj: "x \<in>#\<^sub>z M \<longleftrightarrow> x \<in># mset_pos M \<or> x \<in># mset_neg M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in>#\<^sub>z M) = (x \<in># mset_pos M \<or> x \<in># mset_neg M)
[PROOF STEP]
by (metis count_mset_pos in_diff_zcount mem_zmset_of mset_pos_neg_partition nat_code(2) not_in_iff zcount_ne_zero_iff)


[STATEMENT]
lemma in_zmset_notin_mset_pos[simp]: "x \<in>#\<^sub>z M \<Longrightarrow> x \<notin># mset_pos M \<Longrightarrow> x \<in># mset_neg M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in>#\<^sub>z M; x \<notin># mset_pos M\<rbrakk> \<Longrightarrow> x \<in># mset_neg M
[PROOF STEP]
by (auto simp: in_zmset_conv_pos_neg_disj)


[STATEMENT]
lemma in_zmset_notin_mset_neg[simp]: "x \<in>#\<^sub>z M \<Longrightarrow> x \<notin># mset_neg M \<Longrightarrow> x \<in># mset_pos M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in>#\<^sub>z M; x \<notin># mset_neg M\<rbrakk> \<Longrightarrow> x \<in># mset_pos M
[PROOF STEP]
by (auto simp: in_zmset_conv_pos_neg_disj)


[STATEMENT]
lemma in_mset_pos_in_zmset: "x \<in># mset_pos M \<Longrightarrow> x \<in>#\<^sub>z M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in># mset_pos M \<Longrightarrow> x \<in>#\<^sub>z M
[PROOF STEP]
by (auto intro: iffD2[OF in_zmset_conv_pos_neg_disj])


[STATEMENT]
lemma in_mset_neg_in_zmset: "x \<in># mset_neg M \<Longrightarrow> x \<in>#\<^sub>z M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in># mset_neg M \<Longrightarrow> x \<in>#\<^sub>z M
[PROOF STEP]
by (auto intro: iffD2[OF in_zmset_conv_pos_neg_disj])


[STATEMENT]
lemma set_zmset_eq_set_mset_union: "set_zmset M = set_mset (mset_pos M) \<union> set_mset (mset_neg M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_zmset M = set_mset (mset_pos M) \<union> set_mset (mset_neg M)
[PROOF STEP]
by (auto dest: in_mset_pos_in_zmset in_mset_neg_in_zmset)


[STATEMENT]
lemma member_mset_pos_iff_zcount: "x \<in># mset_pos M \<longleftrightarrow> 0 < zcount M x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in># mset_pos M) = (0 < zcount M x)
[PROOF STEP]
using not_in_iff pos_zcount_in_zmset
[PROOF STATE]
proof (prove)
using this:
(?x \<notin># ?M) = (count ?M ?x = 0)
0 < zcount ?M ?x \<Longrightarrow> ?x \<in>#\<^sub>z ?M

goal (1 subgoal):
 1. (x \<in># mset_pos M) = (0 < zcount M x)
[PROOF STEP]
by force


[STATEMENT]
lemma member_mset_neg_iff_zcount: "x \<in># mset_neg M \<longleftrightarrow> zcount M x < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in># mset_neg M) = (zcount M x < 0)
[PROOF STEP]
by (metis member_mset_pos_iff_zcount mset_pos_uminus neg_le_0_iff_le not_le zcount_uminus)


[STATEMENT]
lemma mset_pos_mset_neg_disjoint[simp]: "set_mset (mset_pos \<Delta>) \<inter> set_mset (mset_neg \<Delta>) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset (mset_pos \<Delta>) \<inter> set_mset (mset_neg \<Delta>) = {}
[PROOF STEP]
by (auto simp: member_mset_pos_iff_zcount member_mset_neg_iff_zcount)


[STATEMENT]
lemma zcount_sum: "zcount (\<Sum>M\<in>MM. f M) t = (\<Sum>M\<in>MM. zcount (f M) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (sum f MM) t = (\<Sum>M\<in>MM. zcount (f M) t)
[PROOF STEP]
by (induct MM rule: infinite_finite_induct) auto


[STATEMENT]
lemma zcount_filter_invariant: "zcount {# t'\<in>#\<^sub>zM. t'=t #} t = zcount M t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount {#t' \<in>#\<^sub>z M. t' = t#} t = zcount M t
[PROOF STEP]
by auto


[STATEMENT]
lemma in_filter_zmset_in_zmset[simp]: "x \<in>#\<^sub>z filter_zmset P M \<Longrightarrow> x \<in>#\<^sub>z M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>#\<^sub>z filter_zmset P M \<Longrightarrow> x \<in>#\<^sub>z M
[PROOF STEP]
by (metis count_filter_zmset zcount_ne_zero_iff)


[STATEMENT]
lemma pos_filter_zmset_pos_zmset[simp]: "0 < zcount (filter_zmset P M) x \<Longrightarrow> 0 < zcount M x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < zcount (filter_zmset P M) x \<Longrightarrow> 0 < zcount M x
[PROOF STEP]
by (metis (full_types) count_filter_zmset less_irrefl)


[STATEMENT]
lemma neg_filter_zmset_neg_zmset[simp]: "0 > zcount (filter_zmset P M) x \<Longrightarrow> 0 > zcount M x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (filter_zmset P M) x < 0 \<Longrightarrow> zcount M x < 0
[PROOF STEP]
by (metis (full_types) count_filter_zmset less_irrefl)


[STATEMENT]
lemma zcount_update_zmultiset: "zcount (update_zmultiset M t n) t' = zcount M t' + (if t = t' then n else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (update_zmultiset M t n) t' = zcount M t' + (if t = t' then n else 0)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma (in order) order_zmset_exists_foundation:
  fixes   t :: 'a
  assumes "0 < zcount M t"
  shows   "\<exists>s. s \<le> t \<and> 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < zcount M t

goal (1 subgoal):
 1. \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < zcount M t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)
[PROOF STEP]
let ?M = "{t. 0 < zcount M t}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < zcount M t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < zcount M t
[PROOF STEP]
have "t \<in> ?M"
[PROOF STATE]
proof (prove)
using this:
0 < zcount M t

goal (1 subgoal):
 1. t \<in> {t. 0 < zcount M t}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<in> {t. 0 < zcount M t}

goal (1 subgoal):
 1. 0 < zcount M t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> {t. 0 < zcount M t}
[PROOF STEP]
have "\<exists>s\<in>?M. s \<le> t \<and> (\<forall>u\<in>?M. \<not> u < s)"
[PROOF STATE]
proof (prove)
using this:
t \<in> {t. 0 < zcount M t}

goal (1 subgoal):
 1. \<exists>s\<in>{t. 0 < zcount M t}. s \<le> t \<and> (\<forall>u\<in>{t. 0 < zcount M t}. \<not> u < s)
[PROOF STEP]
by - (drule order_finite_set_exists_foundation[rotated 1], auto)
[PROOF STATE]
proof (state)
this:
\<exists>s\<in>{t. 0 < zcount M t}. s \<le> t \<and> (\<forall>u\<in>{t. 0 < zcount M t}. \<not> u < s)

goal (1 subgoal):
 1. 0 < zcount M t \<Longrightarrow> \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s\<in>{t. 0 < zcount M t}. s \<le> t \<and> (\<forall>u\<in>{t. 0 < zcount M t}. \<not> u < s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s\<in>{t. 0 < zcount M t}. s \<le> t \<and> (\<forall>u\<in>{t. 0 < zcount M t}. \<not> u < s)

goal (1 subgoal):
 1. \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u. 0 < zcount M u \<longrightarrow> \<not> u < s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in order) order_zmset_exists_foundation':
  fixes   t :: 'a
  assumes "0 < zcount M t"
  shows   "\<exists>s. s \<le> t \<and> 0 < zcount M s \<and> (\<forall>u<s. zcount M u \<le> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u<s. zcount M u \<le> 0)
[PROOF STEP]
using assms order_zmset_exists_foundation
[PROOF STATE]
proof (prove)
using this:
0 < zcount M t
0 < zcount ?M ?t \<Longrightarrow> \<exists>s\<le>?t. 0 < zcount ?M s \<and> (\<forall>u. 0 < zcount ?M u \<longrightarrow> \<not> u < s)

goal (1 subgoal):
 1. \<exists>s\<le>t. 0 < zcount M s \<and> (\<forall>u<s. zcount M u \<le> 0)
[PROOF STEP]
by (meson le_less_linear)


[STATEMENT]
lemma (in order) order_zmset_exists_foundation_neg:
  fixes   t :: 'a
  assumes "zcount M t < 0"
  shows   "\<exists>s. s \<le> t \<and> zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
zcount M t < 0

goal (1 subgoal):
 1. \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount M t < 0 \<Longrightarrow> \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)
[PROOF STEP]
let ?M = "{t. zcount M t < 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount M t < 0 \<Longrightarrow> \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
zcount M t < 0
[PROOF STEP]
have "t \<in> ?M"
[PROOF STATE]
proof (prove)
using this:
zcount M t < 0

goal (1 subgoal):
 1. t \<in> {t. zcount M t < 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<in> {t. zcount M t < 0}

goal (1 subgoal):
 1. zcount M t < 0 \<Longrightarrow> \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> {t. zcount M t < 0}
[PROOF STEP]
have "\<exists>s\<in>?M. s \<le> t \<and> (\<forall>u\<in>?M. \<not> u < s)"
[PROOF STATE]
proof (prove)
using this:
t \<in> {t. zcount M t < 0}

goal (1 subgoal):
 1. \<exists>s\<in>{t. zcount M t < 0}. s \<le> t \<and> (\<forall>u\<in>{t. zcount M t < 0}. \<not> u < s)
[PROOF STEP]
by - (drule order_finite_set_exists_foundation[rotated 1], auto)
[PROOF STATE]
proof (state)
this:
\<exists>s\<in>{t. zcount M t < 0}. s \<le> t \<and> (\<forall>u\<in>{t. zcount M t < 0}. \<not> u < s)

goal (1 subgoal):
 1. zcount M t < 0 \<Longrightarrow> \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s\<in>{t. zcount M t < 0}. s \<le> t \<and> (\<forall>u\<in>{t. zcount M t < 0}. \<not> u < s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s\<in>{t. zcount M t < 0}. s \<le> t \<and> (\<forall>u\<in>{t. zcount M t < 0}. \<not> u < s)

goal (1 subgoal):
 1. \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u. zcount M u < 0 \<longrightarrow> \<not> u < s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in order) order_zmset_exists_foundation_neg':
  fixes   t :: 'a
  assumes "zcount M t < 0"
  shows   "\<exists>s. s \<le> t \<and> zcount M s < 0 \<and> (\<forall>u<s. 0 \<le> zcount M u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u<s. 0 \<le> zcount M u)
[PROOF STEP]
using assms order_zmset_exists_foundation_neg
[PROOF STATE]
proof (prove)
using this:
zcount M t < 0
zcount ?M ?t < 0 \<Longrightarrow> \<exists>s\<le>?t. zcount ?M s < 0 \<and> (\<forall>u. zcount ?M u < 0 \<longrightarrow> \<not> u < s)

goal (1 subgoal):
 1. \<exists>s\<le>t. zcount M s < 0 \<and> (\<forall>u<s. 0 \<le> zcount M u)
[PROOF STEP]
by (meson le_less_linear)


[STATEMENT]
lemma image_zmset_empty[simp]: "image_zmset f {#}\<^sub>z = {#}\<^sub>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auxiliary.image_zmset f {#}\<^sub>z = {#}\<^sub>z
[PROOF STEP]
by transfer (auto simp: equiv_zmset_def)


[STATEMENT]
lemma image_zmset_single[simp]: "image_zmset f {#x#}\<^sub>z = {#f x#}\<^sub>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auxiliary.image_zmset f {#x#}\<^sub>z = {#f x#}\<^sub>z
[PROOF STEP]
by transfer (simp add: equiv_zmset_def)


[STATEMENT]
lemma image_zmset_union[simp]: "image_zmset f (M + N) = image_zmset f M + image_zmset f N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auxiliary.image_zmset f (M + N) = Auxiliary.image_zmset f M + Auxiliary.image_zmset f N
[PROOF STEP]
by transfer (auto simp: equiv_zmset_def)


[STATEMENT]
lemma image_zmset_Diff[simp]: "image_zmset f (A - B) = image_zmset f A - image_zmset f B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auxiliary.image_zmset f (A - B) = Auxiliary.image_zmset f A - Auxiliary.image_zmset f B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Auxiliary.image_zmset f (A - B) = Auxiliary.image_zmset f A - Auxiliary.image_zmset f B
[PROOF STEP]
have "image_zmset f (A - B + B) = image_zmset f (A - B) + image_zmset f B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auxiliary.image_zmset f (A - B + B) = Auxiliary.image_zmset f (A - B) + Auxiliary.image_zmset f B
[PROOF STEP]
using image_zmset_union
[PROOF STATE]
proof (prove)
using this:
Auxiliary.image_zmset ?f (?M + ?N) = Auxiliary.image_zmset ?f ?M + Auxiliary.image_zmset ?f ?N

goal (1 subgoal):
 1. Auxiliary.image_zmset f (A - B + B) = Auxiliary.image_zmset f (A - B) + Auxiliary.image_zmset f B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Auxiliary.image_zmset f (A - B + B) = Auxiliary.image_zmset f (A - B) + Auxiliary.image_zmset f B

goal (1 subgoal):
 1. Auxiliary.image_zmset f (A - B) = Auxiliary.image_zmset f A - Auxiliary.image_zmset f B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Auxiliary.image_zmset f (A - B + B) = Auxiliary.image_zmset f (A - B) + Auxiliary.image_zmset f B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Auxiliary.image_zmset f (A - B + B) = Auxiliary.image_zmset f (A - B) + Auxiliary.image_zmset f B

goal (1 subgoal):
 1. Auxiliary.image_zmset f (A - B) = Auxiliary.image_zmset f A - Auxiliary.image_zmset f B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Auxiliary.image_zmset f (A - B) = Auxiliary.image_zmset f A - Auxiliary.image_zmset f B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_neg_image_zmset: "mset_neg M = {#} \<Longrightarrow> mset_neg (image_zmset f M) = {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_neg M = {#} \<Longrightarrow> mset_neg (Auxiliary.image_zmset f M) = {#}
[PROOF STEP]
unfolding multiset_eq_iff count_empty
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. count (mset_neg M) a = 0 \<Longrightarrow> \<forall>a. count (mset_neg (Auxiliary.image_zmset f M)) a = 0
[PROOF STEP]
by transfer (auto simp add: image_mset_subseteq_mono mset_subset_eqI mset_subset_eq_count)


[STATEMENT]
lemma nonneg_zcount_image_zmset[simp]: "(\<And>t. 0 \<le> zcount M t) \<Longrightarrow> 0 \<le> zcount (image_zmset f M) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. 0 \<le> zcount M t) \<Longrightarrow> 0 \<le> zcount (Auxiliary.image_zmset f M) t
[PROOF STEP]
by (meson mset_neg_empty_iff mset_neg_image_zmset)


[STATEMENT]
lemma image_zmset_add_zmset[simp]: "image_zmset f (add_zmset t M) = add_zmset (f t) (image_zmset f M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auxiliary.image_zmset f (add_zmset t M) = add_zmset (f t) (Auxiliary.image_zmset f M)
[PROOF STEP]
by transfer (auto simp: equiv_zmset_def)


[STATEMENT]
lemma pos_zcount_image_zmset[simp]: "(\<And>t. 0 \<le> zcount M t) \<Longrightarrow> 0 < zcount M t \<Longrightarrow> 0 < zcount (image_zmset f M) (f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount M t\<rbrakk> \<Longrightarrow> 0 < zcount (Auxiliary.image_zmset f M) (f t)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M t f. \<lbrakk>\<And>t. 0 \<le> (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t; 0 < (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t\<rbrakk> \<Longrightarrow> 0 < (case case M of (M, N) \<Rightarrow> (image_mset f M, image_mset f N) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) (f t)
[PROOF STEP]
subgoal for M t f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t; 0 < (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t\<rbrakk> \<Longrightarrow> 0 < (case case M of (M, N) \<Rightarrow> (image_mset f M, image_mset f N) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) (f t)
[PROOF STEP]
apply (induct M)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>t. 0 \<le> (case (a, b) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t; 0 < (case (a, b) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t\<rbrakk> \<Longrightarrow> 0 < (case case (a, b) of (M, N) \<Rightarrow> (image_mset f M, image_mset f N) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) (f t)
[PROOF STEP]
subgoal for Mp Mn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> (case (Mp, Mn) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t; 0 < (case (Mp, Mn) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) t\<rbrakk> \<Longrightarrow> 0 < (case case (Mp, Mn) of (M, N) \<Rightarrow> (image_mset f M, image_mset f N) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) (f t)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. count Mn t \<le> count Mp t; count Mn t < count Mp t\<rbrakk> \<Longrightarrow> count (image_mset f Mn) (f t) < count (image_mset f Mp) (f t)
[PROOF STEP]
apply (metis count_diff count_image_mset_ge_count image_mset_Diff less_le_trans subseteq_mset_def zero_less_diff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_zmset_transfer[transfer_rule]:
  "(rel_fun (pcr_zmultiset (=)) (rel_set (=)))
   (\<lambda>(Mp, Mn). set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}) set_zmset"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (pcr_zmultiset (=)) (rel_set (=)) (\<lambda>(Mp, Mn). set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}) set_zmset
[PROOF STEP]
by (auto simp: rel_fun_def pcr_zmultiset_def cr_zmultiset_def
      rel_set_eq multiset.rel_eq set_zmset_def zcount.abs_eq count_eq_zero_iff[symmetric]
      simp del: zcount_ne_zero_iff)


[STATEMENT]
lemma zcount_image_zmset:
  "zcount (image_zmset f M) x = (\<Sum>y \<in> f -` {x} \<inter> set_zmset M. zcount M y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (Auxiliary.image_zmset f M) x = sum (zcount M) (f -` {x} \<inter> set_zmset M)
[PROOF STEP]
apply (transfer fixing: f x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. (case case M of (M, N) \<Rightarrow> (image_mset f M, image_mset f N) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) x = sum (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) (f -` {x} \<inter> (case M of (Mp, Mn) \<Rightarrow> set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}))
[PROOF STEP]
subgoal for M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case M of (M, N) \<Rightarrow> (image_mset f M, image_mset f N) of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) x = sum (case M of (Mp, Mn) \<Rightarrow> \<lambda>x. int (count Mp x) - int (count Mn x)) (f -` {x} \<inter> (case M of (Mp, Mn) \<Rightarrow> set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}))
[PROOF STEP]
apply (cases M; clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. M = (a, b) \<Longrightarrow> int (count (image_mset f a) x) - int (count (image_mset f b) x) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset a \<union> set_mset b - {x. count a x = count b x}). int (count a x) - int (count b x))
[PROOF STEP]
subgoal for Mp Mn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> int (count (image_mset f Mp) x) - int (count (image_mset f Mn) x) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
unfolding count_image_mset int_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
have "(\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) =
        (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x))" (is "?S1 = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x))
[PROOF STEP]
by (subst sum.same_carrier[where C="f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn)"])
          (auto simp: count_eq_zero_iff)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x))

goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x))

goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
have "(\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) =
        (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mn x))"(is "?S2 = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mn x))
[PROOF STEP]
by (subst sum.same_carrier[where C="f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn)"])
          (auto simp: count_eq_zero_iff)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mn x))

goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mn x))

goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
have "(\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
        = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x) - int (count Mn x))"
        (is "?S = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x) - int (count Mn x))
[PROOF STEP]
by (subst sum.same_carrier[where C="f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn)"]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x) - int (count Mn x))

goal (1 subgoal):
 1. M = (Mp, Mn) \<Longrightarrow> (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x))
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mn x))
(\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x) - int (count Mn x))
[PROOF STEP]
show "?S1 - ?S2 = ?S"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x))
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mn x))
(\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn). int (count Mp x) - int (count Mn x))

goal (1 subgoal):
 1. (\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))
[PROOF STEP]
by (auto simp: sum_subtractf)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>f -` {x} \<inter> set_mset Mp. int (count Mp x)) - (\<Sum>x\<in>f -` {x} \<inter> set_mset Mn. int (count Mn x)) = (\<Sum>x\<in>f -` {x} \<inter> (set_mset Mp \<union> set_mset Mn - {x. count Mp x = count Mn x}). int (count Mp x) - int (count Mn x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma zmset_empty_image_zmset_empty: "(\<And>t. zcount M t = 0) \<Longrightarrow> zcount (image_zmset f M) t = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. zcount M t = 0) \<Longrightarrow> zcount (Auxiliary.image_zmset f M) t = 0
[PROOF STEP]
by (auto simp: zcount_image_zmset)


[STATEMENT]
lemma in_image_zmset_in_zmset: "t \<in>#\<^sub>z image_zmset f M \<Longrightarrow> \<exists>t. t \<in>#\<^sub>z M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in>#\<^sub>z Auxiliary.image_zmset f M \<Longrightarrow> \<exists>t. t \<in>#\<^sub>z M
[PROOF STEP]
by (rule ccontr) simp


[STATEMENT]
lemma zcount_image_zmset_zero: "(\<And>m. m \<in>#\<^sub>z M \<Longrightarrow> f m \<noteq> x) \<Longrightarrow> x \<notin>#\<^sub>z image_zmset f M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in>#\<^sub>z M \<Longrightarrow> f m \<noteq> x) \<Longrightarrow> x \<notin>#\<^sub>z Auxiliary.image_zmset f M
[PROOF STEP]
unfolding set_zmset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> {x. zcount M x \<noteq> 0} \<Longrightarrow> f m \<noteq> x) \<Longrightarrow> x \<notin> {x. zcount (Auxiliary.image_zmset f M) x \<noteq> 0}
[PROOF STEP]
by (simp add: zcount_image_zmset) (metis Int_emptyI sum.empty vimage_singleton_eq)


[STATEMENT]
lemma image_zmset_pre: "t \<in>#\<^sub>z image_zmset f M \<Longrightarrow> \<exists>m. m \<in>#\<^sub>z M \<and> f m = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in>#\<^sub>z Auxiliary.image_zmset f M \<Longrightarrow> \<exists>m. m \<in>#\<^sub>z M \<and> f m = t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>t \<in>#\<^sub>z Auxiliary.image_zmset f M; \<nexists>m. m \<in>#\<^sub>z M \<and> f m = t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume t: "t \<in>#\<^sub>z image_zmset f M"
[PROOF STATE]
proof (state)
this:
t \<in>#\<^sub>z Auxiliary.image_zmset f M

goal (1 subgoal):
 1. \<lbrakk>t \<in>#\<^sub>z Auxiliary.image_zmset f M; \<nexists>m. m \<in>#\<^sub>z M \<and> f m = t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<nexists>m. m \<in>#\<^sub>z M \<and> f m = t"
[PROOF STATE]
proof (state)
this:
\<nexists>m. m \<in>#\<^sub>z M \<and> f m = t

goal (1 subgoal):
 1. \<lbrakk>t \<in>#\<^sub>z Auxiliary.image_zmset f M; \<nexists>m. m \<in>#\<^sub>z M \<and> f m = t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>m. m \<in>#\<^sub>z M \<and> f m = t
[PROOF STEP]
have "m \<in>#\<^sub>z M \<Longrightarrow> \<not> f m = t" for m
[PROOF STATE]
proof (prove)
using this:
\<nexists>m. m \<in>#\<^sub>z M \<and> f m = t

goal (1 subgoal):
 1. m \<in>#\<^sub>z M \<Longrightarrow> f m \<noteq> t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?m \<in>#\<^sub>z M \<Longrightarrow> f ?m \<noteq> t

goal (1 subgoal):
 1. \<lbrakk>t \<in>#\<^sub>z Auxiliary.image_zmset f M; \<nexists>m. m \<in>#\<^sub>z M \<and> f m = t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?m \<in>#\<^sub>z M \<Longrightarrow> f ?m \<noteq> t
[PROOF STEP]
have "zcount (image_zmset f M) t = 0"
[PROOF STATE]
proof (prove)
using this:
?m \<in>#\<^sub>z M \<Longrightarrow> f ?m \<noteq> t

goal (1 subgoal):
 1. zcount (Auxiliary.image_zmset f M) t = 0
[PROOF STEP]
by (meson t zcount_image_zmset_zero)
[PROOF STATE]
proof (state)
this:
zcount (Auxiliary.image_zmset f M) t = 0

goal (1 subgoal):
 1. \<lbrakk>t \<in>#\<^sub>z Auxiliary.image_zmset f M; \<nexists>m. m \<in>#\<^sub>z M \<and> f m = t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with t
[PROOF STATE]
proof (chain)
picking this:
t \<in>#\<^sub>z Auxiliary.image_zmset f M
zcount (Auxiliary.image_zmset f M) t = 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
t \<in>#\<^sub>z Auxiliary.image_zmset f M
zcount (Auxiliary.image_zmset f M) t = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (meson zcount_ne_zero_iff)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pos_image_zmset_obtain_pre:
  "(\<And>t. 0 \<le> zcount M t) \<Longrightarrow> 0 < zcount (image_zmset f M) t \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount (Auxiliary.image_zmset f M) t\<rbrakk> \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount (Auxiliary.image_zmset f M) t\<rbrakk> \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
assume nonneg: "0 \<le> zcount M t" for t
[PROOF STATE]
proof (state)
this:
0 \<le> zcount M ?t

goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount (Auxiliary.image_zmset f M) t\<rbrakk> \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
assume "0 < zcount (image_zmset f M) t"
[PROOF STATE]
proof (state)
this:
0 < zcount (Auxiliary.image_zmset f M) t

goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount (Auxiliary.image_zmset f M) t\<rbrakk> \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (Auxiliary.image_zmset f M) t
[PROOF STEP]
have "t \<in>#\<^sub>z image_zmset f M"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (Auxiliary.image_zmset f M) t

goal (1 subgoal):
 1. t \<in>#\<^sub>z Auxiliary.image_zmset f M
[PROOF STEP]
by (simp add: pos_zcount_in_zmset)
[PROOF STATE]
proof (state)
this:
t \<in>#\<^sub>z Auxiliary.image_zmset f M

goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount (Auxiliary.image_zmset f M) t\<rbrakk> \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in>#\<^sub>z Auxiliary.image_zmset f M
[PROOF STEP]
obtain x where x: "x \<in>#\<^sub>z M" "f x = t"
[PROOF STATE]
proof (prove)
using this:
t \<in>#\<^sub>z Auxiliary.image_zmset f M

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>#\<^sub>z M; f x = t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: image_zmset_pre)
[PROOF STATE]
proof (state)
this:
x \<in>#\<^sub>z M
f x = t

goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount (Auxiliary.image_zmset f M) t\<rbrakk> \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
with nonneg
[PROOF STATE]
proof (chain)
picking this:
0 \<le> zcount M ?t
x \<in>#\<^sub>z M
f x = t
[PROOF STEP]
have "0 < zcount M x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> zcount M ?t
x \<in>#\<^sub>z M
f x = t

goal (1 subgoal):
 1. 0 < zcount M x
[PROOF STEP]
by (meson zmset_elem_nonneg)
[PROOF STATE]
proof (state)
this:
0 < zcount M x

goal (1 subgoal):
 1. \<lbrakk>\<And>t. 0 \<le> zcount M t; 0 < zcount (Auxiliary.image_zmset f M) t\<rbrakk> \<Longrightarrow> \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x \<in>#\<^sub>z M
f x = t
0 < zcount M x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in>#\<^sub>z M
f x = t
0 < zcount M x

goal (1 subgoal):
 1. \<exists>m. 0 < zcount M m \<and> f m = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m. 0 < zcount M m \<and> f m = t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relatesD[dest]: "relates P s \<Longrightarrow> P (shd s) (shd (stl s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relates P s \<Longrightarrow> P (shd s) (shd (stl s))
[PROOF STEP]
unfolding relates_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (shd s) (shd (stl s)) \<Longrightarrow> P (shd s) (shd (stl s))
[PROOF STEP]
by simp


[STATEMENT]
lemma alw_relatesD[dest]: "alw (relates P) s \<Longrightarrow> P (shd s) (shd (stl s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (relates P) s \<Longrightarrow> P (shd s) (shd (stl s))
[PROOF STEP]
by auto


[STATEMENT]
lemma relatesI[intro]: "P (shd s) (shd (stl s)) \<Longrightarrow> relates P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (shd s) (shd (stl s)) \<Longrightarrow> relates P s
[PROOF STEP]
by (auto simp: relates_def)