[STATEMENT]
lemma count_image_mset_le_imp_lt_raw:
  assumes
    "finite A" and
    "A = set_mset M \<union> set_mset N" and
    "count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a"
  shows "\<exists>b. f b = f a \<and> count M b < count N b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
A = set_mset M \<union> set_mset N
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
proof (induct A arbitrary: M N rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>F = set_mset ?M \<union> set_mset ?N; count (image_mset f ?M) (f a) + count ?N a < count (image_mset f ?N) (f a) + count ?M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count ?M b < count ?N b
insert x F = set_mset M \<union> set_mset N
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a

goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
    cnt_lt = this(5)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>F = set_mset ?M \<union> set_mset ?N; count (image_mset f ?M) (f a) + count ?N a < count (image_mset f ?N) (f a) + count ?M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count ?M b < count ?N b
insert x F = set_mset M \<union> set_mset N
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a

goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
let ?Ma = "{#y \<in># M. y \<noteq> x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
let ?Mb = "{#y \<in># M. y = x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
let ?Na = "{#y \<in># N. y \<noteq> x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
let ?Nb = "{#y \<in># N. y = x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M = {#y \<in># M. y = x#} + {#y \<in># M. y \<noteq> x#} &&& N = {#y \<in># N. y = x#} + {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
using multiset_partition
[PROOF STATE]
proof (prove)
using this:
?M = filter_mset ?P ?M + {#x \<in># ?M. \<not> ?P x#}

goal (1 subgoal):
 1. M = {#y \<in># M. y = x#} + {#y \<in># M. y \<noteq> x#} &&& N = {#y \<in># N. y = x#} + {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
M = {#y \<in># M. y = x#} + {#y \<in># M. y \<noteq> x#}
N = {#y \<in># N. y = x#} + {#y \<in># N. y \<noteq> x#}

goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = set_mset {#y \<in># M. y \<noteq> x#} \<union> set_mset {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
using x_f_eq_m_n x_ni_f
[PROOF STATE]
proof (prove)
using this:
insert x F = set_mset M \<union> set_mset N
x \<notin> F

goal (1 subgoal):
 1. F = set_mset {#y \<in># M. y \<noteq> x#} \<union> set_mset {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = set_mset {#y \<in># M. y \<noteq> x#} \<union> set_mset {#y \<in># N. y \<noteq> x#}

goal (2 subgoals):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<And>x F M N. \<lbrakk>finite F; x \<notin> F; \<And>M N. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
proof (cases "f x = f a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
case fx_ne_fa: False
[PROOF STATE]
proof (state)
this:
f x \<noteq> f a

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have cnt_fma_fa: "count (image_mset f ?Ma) (f a) = count (image_mset f M) (f a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) = count (image_mset f M) (f a)
[PROOF STEP]
using fx_ne_fa
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> f a

goal (1 subgoal):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) = count (image_mset f M) (f a)
[PROOF STEP]
by (subst (2) m_part) auto
[PROOF STATE]
proof (state)
this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) = count (image_mset f M) (f a)

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have cnt_fna_fa: "count (image_mset f ?Na) (f a) = count (image_mset f N) (f a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) = count (image_mset f N) (f a)
[PROOF STEP]
using fx_ne_fa
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> f a

goal (1 subgoal):
 1. count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) = count (image_mset f N) (f a)
[PROOF STEP]
by (subst (2) n_part) auto
[PROOF STATE]
proof (state)
this:
count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) = count (image_mset f N) (f a)

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have cnt_ma_a: "count ?Ma a = count M a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count {#y \<in># M. y \<noteq> x#} a = count M a
[PROOF STEP]
using fx_ne_fa
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> f a

goal (1 subgoal):
 1. count {#y \<in># M. y \<noteq> x#} a = count M a
[PROOF STEP]
by (subst (2) m_part) auto
[PROOF STATE]
proof (state)
this:
count {#y \<in># M. y \<noteq> x#} a = count M a

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have cnt_na_a: "count ?Na a = count N a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count {#y \<in># N. y \<noteq> x#} a = count N a
[PROOF STEP]
using fx_ne_fa
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> f a

goal (1 subgoal):
 1. count {#y \<in># N. y \<noteq> x#} a = count N a
[PROOF STEP]
by (subst (2) n_part) auto
[PROOF STATE]
proof (state)
this:
count {#y \<in># N. y \<noteq> x#} a = count N a

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
obtain b where fb_eq_fa: "f b = f a" and cnt_b: "count ?Ma b < count ?Na b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b. \<lbrakk>f b = f a; count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ih[OF f_eq_ma_na] cnt_lt
[PROOF STATE]
proof (prove)
using this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a \<Longrightarrow> \<exists>b. f b = f a \<and> count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>f b = f a; count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding cnt_fma_fa cnt_fna_fa cnt_ma_a cnt_na_a
[PROOF STATE]
proof (prove)
using this:
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a \<Longrightarrow> \<exists>b. f b = f a \<and> count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>f b = f a; count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f b = f a
count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have fx_ne_fb: "f x \<noteq> f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<noteq> f b
[PROOF STEP]
using fb_eq_fa fx_ne_fa
[PROOF STATE]
proof (prove)
using this:
f b = f a
f x \<noteq> f a

goal (1 subgoal):
 1. f x \<noteq> f b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f x \<noteq> f b

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have cnt_ma_b: "count ?Ma b = count M b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count {#y \<in># M. y \<noteq> x#} b = count M b
[PROOF STEP]
using fx_ne_fb
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> f b

goal (1 subgoal):
 1. count {#y \<in># M. y \<noteq> x#} b = count M b
[PROOF STEP]
by (subst (2) m_part) auto
[PROOF STATE]
proof (state)
this:
count {#y \<in># M. y \<noteq> x#} b = count M b

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have cnt_na_b: "count ?Na b = count N b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count {#y \<in># N. y \<noteq> x#} b = count N b
[PROOF STEP]
using fx_ne_fb
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> f b

goal (1 subgoal):
 1. count {#y \<in># N. y \<noteq> x#} b = count N b
[PROOF STEP]
by (subst (2) n_part) auto
[PROOF STATE]
proof (state)
this:
count {#y \<in># N. y \<noteq> x#} b = count N b

goal (2 subgoals):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. f x \<noteq> f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
using fb_eq_fa cnt_b
[PROOF STATE]
proof (prove)
using this:
f b = f a
count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
unfolding cnt_ma_b cnt_na_b
[PROOF STATE]
proof (prove)
using this:
f b = f a
count M b < count N b

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. f b = f a \<and> count M b < count N b

goal (1 subgoal):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
case fx_eq_fa: True
[PROOF STATE]
proof (state)
this:
f x = f a

goal (1 subgoal):
 1. f x = f a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
proof (cases "x = a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. x \<noteq> a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
case x_eq_a: True
[PROOF STATE]
proof (state)
this:
x = a

goal (2 subgoals):
 1. x = a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. x \<noteq> a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have "count (image_mset f ?Ma) (f a) + count ?Na a
        < count (image_mset f ?Na) (f a) + count ?Ma a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
[PROOF STEP]
using cnt_lt x_eq_a
[PROOF STATE]
proof (prove)
using this:
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a
x = a

goal (1 subgoal):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
[PROOF STEP]
by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part, auto)
[PROOF STATE]
proof (state)
this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a

goal (2 subgoals):
 1. x = a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. x \<noteq> a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
using ih[OF f_eq_ma_na]
[PROOF STATE]
proof (prove)
using this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a \<Longrightarrow> \<exists>b. f b = f a \<and> count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
by (metis count_filter_mset nat_neq_iff)
[PROOF STATE]
proof (state)
this:
\<exists>b. f b = f a \<and> count M b < count N b

goal (1 subgoal):
 1. x \<noteq> a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
case x_ne_a: False
[PROOF STATE]
proof (state)
this:
x \<noteq> a

goal (1 subgoal):
 1. x \<noteq> a \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
proof (cases "count M x < count N x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
count M x < count N x

goal (2 subgoals):
 1. count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
 2. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
count M x < count N x

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
using fx_eq_fa
[PROOF STATE]
proof (prove)
using this:
count M x < count N x
f x = f a

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. f b = f a \<and> count M b < count N b

goal (1 subgoal):
 1. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> count M x < count N x

goal (1 subgoal):
 1. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
hence cnt_x: "count M x \<ge> count N x"
[PROOF STATE]
proof (prove)
using this:
\<not> count M x < count N x

goal (1 subgoal):
 1. count N x \<le> count M x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
count N x \<le> count M x

goal (1 subgoal):
 1. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
have "count M x + count (image_mset f ?Ma) (f a) + count ?Na a
          < count N x + count (image_mset f ?Na) (f a) + count ?Ma a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count M x + count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count N x + count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
[PROOF STEP]
using cnt_lt x_ne_a fx_eq_fa
[PROOF STATE]
proof (prove)
using this:
count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a
x \<noteq> a
f x = f a

goal (1 subgoal):
 1. count M x + count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count N x + count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
[PROOF STEP]
by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part, auto)
[PROOF STATE]
proof (state)
this:
count M x + count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count N x + count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a

goal (1 subgoal):
 1. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
hence "count (image_mset f ?Ma) (f a) + count ?Na a
          < count (image_mset f ?Na) (f a) + count ?Ma a"
[PROOF STATE]
proof (prove)
using this:
count M x + count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count N x + count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a

goal (1 subgoal):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
[PROOF STEP]
using cnt_x
[PROOF STATE]
proof (prove)
using this:
count M x + count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count N x + count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
count N x \<le> count M x

goal (1 subgoal):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a

goal (1 subgoal):
 1. \<not> count M x < count N x \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
using ih[OF f_eq_ma_na]
[PROOF STATE]
proof (prove)
using this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a
count (image_mset f {#y \<in># M. y \<noteq> x#}) (f a) + count {#y \<in># N. y \<noteq> x#} a < count (image_mset f {#y \<in># N. y \<noteq> x#}) (f a) + count {#y \<in># M. y \<noteq> x#} a \<Longrightarrow> \<exists>b. f b = f a \<and> count {#y \<in># M. y \<noteq> x#} b < count {#y \<in># N. y \<noteq> x#} b

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
by (metis count_filter_mset nat_neq_iff)
[PROOF STATE]
proof (state)
this:
\<exists>b. f b = f a \<and> count M b < count N b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b. f b = f a \<and> count M b < count N b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b. f b = f a \<and> count M b < count N b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b. f b = f a \<and> count M b < count N b

goal (1 subgoal):
 1. \<And>M N. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a\<rbrakk> \<Longrightarrow> \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
qed auto


[STATEMENT]
lemma count_image_mset_le_imp_lt:
  assumes
    "count (image_mset f M) (f a) \<le> count (image_mset f N) (f a)" and
    "count M a > count N a"
  shows "\<exists>b. f b = f a \<and> count M b < count N b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
count (image_mset f M) (f a) \<le> count (image_mset f N) (f a)
count N a < count M a

goal (1 subgoal):
 1. \<exists>b. f b = f a \<and> count M b < count N b
[PROOF STEP]
by (auto intro: count_image_mset_le_imp_lt_raw[of "set_mset M \<union> set_mset N"])


[STATEMENT]
lemma Max_in_mset: "M \<noteq> {#} \<Longrightarrow> Max_mset M \<in># M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> {#} \<Longrightarrow> Max_mset M \<in># M
[PROOF STEP]
by simp


[STATEMENT]
lemma Max_lt_imp_lt_mset:
  assumes n_nemp: "N \<noteq> {#}" and max: "Max_mset M < Max_mset N" (is "?max_M < ?max_N")
  shows "M < N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M < N
[PROOF STEP]
proof (cases "M = {#}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
case m_nemp: False
[PROOF STATE]
proof (state)
this:
M \<noteq> {#}

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
have max_n_in_n: "?max_N \<in># N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max_mset N \<in># N
[PROOF STEP]
using n_nemp
[PROOF STATE]
proof (prove)
using this:
N \<noteq> {#}

goal (1 subgoal):
 1. Max_mset N \<in># N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Max_mset N \<in># N

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
have max_n_nin_m: "?max_N \<notin># M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max_mset N \<notin># M
[PROOF STEP]
using max Max_ge leD
[PROOF STATE]
proof (prove)
using this:
Max_mset M < Max_mset N
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<le> Max ?A
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (1 subgoal):
 1. Max_mset N \<notin># M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max_mset N \<notin># M

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
have "M \<noteq> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> N
[PROOF STEP]
using max
[PROOF STATE]
proof (prove)
using this:
Max_mset M < Max_mset N

goal (1 subgoal):
 1. M \<noteq> N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<noteq> N

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
M \<noteq> N

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
M \<noteq> N

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
assume "count N y < count M y"
[PROOF STATE]
proof (state)
this:
count N y < count M y

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
hence "y \<in># M"
[PROOF STATE]
proof (prove)
using this:
count N y < count M y

goal (1 subgoal):
 1. y \<in># M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in># M

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
hence "?max_M \<ge> y"
[PROOF STATE]
proof (prove)
using this:
y \<in># M

goal (1 subgoal):
 1. y \<le> Max_mset M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<le> Max_mset M

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
hence "?max_N > y"
[PROOF STATE]
proof (prove)
using this:
y \<le> Max_mset M

goal (1 subgoal):
 1. y < Max_mset N
[PROOF STEP]
using max
[PROOF STATE]
proof (prove)
using this:
y \<le> Max_mset M
Max_mset M < Max_mset N

goal (1 subgoal):
 1. y < Max_mset N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y < Max_mset N

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
hence "\<exists>x > y. count M x < count N x"
[PROOF STATE]
proof (prove)
using this:
y < Max_mset N

goal (1 subgoal):
 1. \<exists>x>y. count M x < count N x
[PROOF STEP]
using max_n_nin_m max_n_in_n
[PROOF STATE]
proof (prove)
using this:
y < Max_mset N
Max_mset N \<notin># M
Max_mset N \<in># N

goal (1 subgoal):
 1. \<exists>x>y. count M x < count N x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>x>y. count M x < count N x

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
count N ?y2 < count M ?y2 \<Longrightarrow> \<exists>x>?y2. count M x < count N x

goal (2 subgoals):
 1. M = {#} \<Longrightarrow> M < N
 2. M \<noteq> {#} \<Longrightarrow> M < N
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
M \<noteq> N
count N ?y2 < count M ?y2 \<Longrightarrow> \<exists>x>?y2. count M x < count N x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M \<noteq> N
count N ?y2 < count M ?y2 \<Longrightarrow> \<exists>x>?y2. count M x < count N x

goal (1 subgoal):
 1. M < N
[PROOF STEP]
unfolding less_multiset\<^sub>H\<^sub>O
[PROOF STATE]
proof (prove)
using this:
M \<noteq> N
count N ?y2 < count M ?y2 \<Longrightarrow> \<exists>x>?y2. count M x < count N x

goal (1 subgoal):
 1. M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x>y. count M x < count N x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
M < N

goal (1 subgoal):
 1. M = {#} \<Longrightarrow> M < N
[PROOF STEP]
qed (auto simp: n_nemp)


[STATEMENT]
lemma fold_mset_singleton[simp]: "fold_mset f z {#x#} = f x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_mset f z {#x#} = f x z
[PROOF STEP]
by (simp add: fold_mset_def)


[STATEMENT]
lemma UniqueReceiverOf:
fixes
  msg  :: "('p, 'v) message" and
  p q :: 'p
assumes
  "isReceiverOf q msg"
  "p \<noteq> q"
shows
  "\<not> isReceiverOf p msg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> isReceiverOf p msg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isReceiverOf q msg
p \<noteq> q

goal (1 subgoal):
 1. \<not> isReceiverOf p msg
[PROOF STEP]
by (cases msg, auto)


[STATEMENT]
lemma NoReceivingNoChange:
fixes
  cfg1 cfg2 :: "('p,'v,'s) configuration" and
  m :: "('p,'v) message" and
  p :: 'p
assumes
  Step: "cfg1 \<turnstile> m \<mapsto> cfg2" and
  Rec: "\<not> isReceiverOf p m"
shows
  "states cfg1 p = states cfg2 p "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. states cfg1 p = states cfg2 p
[PROOF STEP]
proof(cases m)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> states cfg1 p = states cfg2 p
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> states cfg1 p = states cfg2 p
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
case (OutMsg b')
[PROOF STATE]
proof (state)
this:
m = <\<bottom>, outM b'>

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> states cfg1 p = states cfg2 p
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> states cfg1 p = states cfg2 p
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m = <\<bottom>, outM b'>

goal (1 subgoal):
 1. states cfg1 p = states cfg2 p
[PROOF STEP]
using Step
[PROOF STATE]
proof (prove)
using this:
m = <\<bottom>, outM b'>
cfg1 \<turnstile> m \<mapsto> cfg2

goal (1 subgoal):
 1. states cfg1 p = states cfg2 p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
states cfg1 p = states cfg2 p

goal (2 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> states cfg1 p = states cfg2 p
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> states cfg1 p = states cfg2 p
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
case (InMsg q b')
[PROOF STATE]
proof (state)
this:
m = <q, inM b'>

goal (2 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> states cfg1 p = states cfg2 p
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
assume CaseM:  "m = <q, inM b'>"
[PROOF STATE]
proof (state)
this:
m = <q, inM b'>

goal (2 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> states cfg1 p = states cfg2 p
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m \<mapsto> cfg2
\<not> isReceiverOf p m
m = <q, inM b'>
[PROOF STEP]
have "p \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
\<not> isReceiverOf p m
m = <q, inM b'>

goal (1 subgoal):
 1. p \<noteq> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<noteq> q

goal (2 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> states cfg1 p = states cfg2 p
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
with Step CaseM
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <q, inM b'>
p \<noteq> q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <q, inM b'>
p \<noteq> q

goal (1 subgoal):
 1. states cfg1 p = states cfg2 p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
states cfg1 p = states cfg2 p

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
case (Msg q v')
[PROOF STATE]
proof (state)
this:
m = <q, v'>

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
assume CaseM:  "m = <q, v'>"
[PROOF STATE]
proof (state)
this:
m = <q, v'>

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m \<mapsto> cfg2
\<not> isReceiverOf p m
m = <q, v'>
[PROOF STEP]
have "p \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
\<not> isReceiverOf p m
m = <q, v'>

goal (1 subgoal):
 1. p \<noteq> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<noteq> q

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> states cfg1 p = states cfg2 p
[PROOF STEP]
with Step CaseM
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <q, v'>
p \<noteq> q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <q, v'>
p \<noteq> q

goal (1 subgoal):
 1. states cfg1 p = states cfg2 p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
states cfg1 p = states cfg2 p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ExistsMsg:
fixes
  cfg1 cfg2 :: "('p,'v,'s) configuration" and
  m :: "('p,'v) message"
assumes
  Step: "cfg1 \<turnstile> m \<mapsto> cfg2"
shows
  "m \<in># (msgs cfg1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in># msgs cfg1
[PROOF STEP]
using assms enabled_def
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
enabled ?cfg ?msg \<equiv> ?msg \<in># msgs ?cfg

goal (1 subgoal):
 1. m \<in># msgs cfg1
[PROOF STEP]
by (cases m, auto)


[STATEMENT]
lemma NoMessageLossStep:
fixes
  cfg1 :: "('p,'v,'s) configuration" and
  cfg2 :: "('p,'v,'s) configuration" and
  p :: 'p and
  m :: "('p,'v) message" and
  m' :: "('p,'v) message"
assumes
  Step: "cfg1 \<turnstile> m \<mapsto> cfg2" and
  Rec1: "isReceiverOf p m" and
  Rec2: "\<not>isReceiverOf p m'"
shows
  "msgs cfg1 m' \<le> msgs cfg2 m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
isReceiverOf p m
\<not> isReceiverOf p m'

goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
by (induct m, simp_all, auto)


[STATEMENT]
lemma OutOnlyGrowing:
fixes
  cfg1 cfg2 :: "('p,'v,'s) configuration" and
  b::bool and
  m::"('p, 'v) message" and
  p::'p
assumes
  "cfg1 \<turnstile> m \<mapsto> cfg2"
  "isReceiverOf p m"
shows
  "msgs cfg2 <\<bottom>, outM b>
  = (msgs cfg1 <\<bottom>, outM b>) +
    sends p (states cfg1 p) (unpackMessage m) <\<bottom>, outM b>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
proof(-)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
have "m = <\<bottom>, outM b> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = <\<bottom>, outM b> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
isReceiverOf p m

goal (1 subgoal):
 1. m = <\<bottom>, outM b> \<Longrightarrow> False
[PROOF STEP]
proof(auto)
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m = <\<bottom>, outM b> \<Longrightarrow> False

goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
hence MNotOut: "m \<noteq> <\<bottom>, outM b>"
[PROOF STATE]
proof (prove)
using this:
m = <\<bottom>, outM b> \<Longrightarrow> False

goal (1 subgoal):
 1. m \<noteq> <\<bottom>, outM b>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<noteq> <\<bottom>, outM b>

goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
have MsgFunction: "msgs cfg2
                    = ((sends p (states cfg1 p) (unpackMessage m))
                      \<union># ((msgs cfg1) -# m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
proof(cases m)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
case (InMsg pa bool)
[PROOF STATE]
proof (state)
this:
m = <pa, inM bool>

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = <pa, inM bool>
[PROOF STEP]
have PaIsP: "pa = p" "(unpackMessage m) = Bool bool"
[PROOF STATE]
proof (prove)
using this:
m = <pa, inM bool>

goal (1 subgoal):
 1. pa = p &&& unpackMessage m = Bool bool
[PROOF STEP]
using isReceiverOf_def assms(2)
[PROOF STATE]
proof (prove)
using this:
m = <pa, inM bool>
isReceiverOf \<equiv> \<lambda>uu uua. rec_message (\<lambda>p2 v p1. p1 = p2) (\<lambda>v p1. False) (\<lambda>p2 v p1. p1 = p2) uua uu
isReceiverOf p m

goal (1 subgoal):
 1. pa = p &&& unpackMessage m = Bool bool
[PROOF STEP]
by (auto simp add: UniqueReceiverOf)
[PROOF STATE]
proof (state)
this:
pa = p
unpackMessage m = Bool bool

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence "cfg1 \<turnstile> <p, inM bool> \<mapsto> cfg2"
[PROOF STATE]
proof (prove)
using this:
pa = p
unpackMessage m = Bool bool

goal (1 subgoal):
 1. cfg1 \<turnstile> <p, inM bool> \<mapsto> cfg2
[PROOF STEP]
using assms(1) InMsg
[PROOF STATE]
proof (prove)
using this:
pa = p
unpackMessage m = Bool bool
cfg1 \<turnstile> m \<mapsto> cfg2
m = <pa, inM bool>

goal (1 subgoal):
 1. cfg1 \<turnstile> <p, inM bool> \<mapsto> cfg2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> <p, inM bool> \<mapsto> cfg2

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence "msgs cfg2 = (sends p (states cfg1 p) (Bool bool)
                       \<union># (msgs cfg1 -# <p, inM bool>))"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> <p, inM bool> \<mapsto> cfg2

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence "msgs cfg2 = (sends p (states cfg1 p) (Bool bool)
                       \<union># (msgs cfg1 -# m))"
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# m
[PROOF STEP]
using PaIsP(1) InMsg
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>
pa = p
m = <pa, inM bool>

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# m

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# m

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
using StepInMsg assms PaIsP
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# m
?cfg1.0 \<turnstile> <?p, inM ?v> \<mapsto> ?cfg2.0 = ((\<forall>s. (s = ?p \<longrightarrow> states ?cfg2.0 ?p = trans ?p (states ?cfg1.0 ?p) (Bool ?v)) \<and> (s \<noteq> ?p \<longrightarrow> states ?cfg2.0 s = states ?cfg1.0 s)) \<and> enabled ?cfg1.0 <?p, inM ?v> \<and> msgs ?cfg2.0 = sends ?p (states ?cfg1.0 ?p) (Bool ?v) \<union># msgs ?cfg1.0 -# <?p, inM ?v>)
cfg1 \<turnstile> m \<mapsto> cfg2
isReceiverOf p m
pa = p
unpackMessage m = Bool bool

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m

goal (2 subgoals):
 1. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
case (OutMsg b)
[PROOF STATE]
proof (state)
this:
m = <\<bottom>, outM b>

goal (2 subgoals):
 1. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
m = <\<bottom>, outM b>

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m = <\<bottom>, outM b>
cfg1 \<turnstile> m \<mapsto> cfg2
isReceiverOf p m

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

goal (2 subgoals):
 1. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
case (Msg pa va)
[PROOF STATE]
proof (state)
this:
m = <pa, va>

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence PaIsP: "pa = p" "(unpackMessage m) = Value va"
[PROOF STATE]
proof (prove)
using this:
m = <pa, va>

goal (1 subgoal):
 1. pa = p &&& unpackMessage m = Value va
[PROOF STEP]
using isReceiverOf_def assms(2)
[PROOF STATE]
proof (prove)
using this:
m = <pa, va>
isReceiverOf \<equiv> \<lambda>uu uua. rec_message (\<lambda>p2 v p1. p1 = p2) (\<lambda>v p1. False) (\<lambda>p2 v p1. p1 = p2) uua uu
isReceiverOf p m

goal (1 subgoal):
 1. pa = p &&& unpackMessage m = Value va
[PROOF STEP]
by (auto simp add: UniqueReceiverOf)
[PROOF STATE]
proof (state)
this:
pa = p
unpackMessage m = Value va

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence "cfg1 \<turnstile> <p, va> \<mapsto> cfg2"
[PROOF STATE]
proof (prove)
using this:
pa = p
unpackMessage m = Value va

goal (1 subgoal):
 1. cfg1 \<turnstile> <p, va> \<mapsto> cfg2
[PROOF STEP]
using assms(1) Msg
[PROOF STATE]
proof (prove)
using this:
pa = p
unpackMessage m = Value va
cfg1 \<turnstile> m \<mapsto> cfg2
m = <pa, va>

goal (1 subgoal):
 1. cfg1 \<turnstile> <p, va> \<mapsto> cfg2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> <p, va> \<mapsto> cfg2

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence "msgs cfg2 = (sends p (states cfg1 p) (Value va)
                       \<union># (msgs cfg1 -# <p, va>))"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> <p, va> \<mapsto> cfg2

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# <p, va>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# <p, va>

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
hence "msgs cfg2 = (sends p (states cfg1 p) (Value va)
                       \<union># (msgs cfg1 -# m))"
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# <p, va>

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# m
[PROOF STEP]
using PaIsP(1) Msg
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# <p, va>
pa = p
m = <pa, va>

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# m

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# m

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
using StepInMsg assms PaIsP
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Value va) \<union># msgs cfg1 -# m
?cfg1.0 \<turnstile> <?p, inM ?v> \<mapsto> ?cfg2.0 = ((\<forall>s. (s = ?p \<longrightarrow> states ?cfg2.0 ?p = trans ?p (states ?cfg1.0 ?p) (Bool ?v)) \<and> (s \<noteq> ?p \<longrightarrow> states ?cfg2.0 s = states ?cfg1.0 s)) \<and> enabled ?cfg1.0 <?p, inM ?v> \<and> msgs ?cfg2.0 = sends ?p (states ?cfg1.0 ?p) (Bool ?v) \<union># msgs ?cfg1.0 -# <?p, inM ?v>)
cfg1 \<turnstile> m \<mapsto> cfg2
isReceiverOf p m
pa = p
unpackMessage m = Value va

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m

goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
have "((sends p (states cfg1 p) (unpackMessage m))
         \<union># ((msgs cfg1) -# m)) <\<bottom>, outM b>
       = ((sends p (states cfg1 p) (unpackMessage m))
         \<union># (msgs cfg1)) <\<bottom>, outM b>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m) <\<bottom>, outM b> = (sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1) <\<bottom>, outM b>
[PROOF STEP]
using MNotOut
[PROOF STATE]
proof (prove)
using this:
m \<noteq> <\<bottom>, outM b>

goal (1 subgoal):
 1. (sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m) <\<bottom>, outM b> = (sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1) <\<bottom>, outM b>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m) <\<bottom>, outM b> = (sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1) <\<bottom>, outM b>

goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
thus "msgs cfg2 <\<bottom>, outM b>
       = (msgs cfg1 <\<bottom>, outM b>) +
         sends p (states cfg1 p) (unpackMessage m) <\<bottom>, outM b>"
[PROOF STATE]
proof (prove)
using this:
(sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m) <\<bottom>, outM b> = (sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1) <\<bottom>, outM b>

goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
using MsgFunction
[PROOF STATE]
proof (prove)
using this:
(sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m) <\<bottom>, outM b> = (sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1) <\<bottom>, outM b>
msgs cfg2 = sends p (states cfg1 p) (unpackMessage m) \<union># msgs cfg1 -# m

goal (1 subgoal):
 1. msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2 <\<bottom>, outM b> = (msgs cfg1 \<union># sends p (states cfg1 p) (unpackMessage m)) <\<bottom>, outM b>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma OtherMessagesOnlyGrowing:
fixes
  cfg1 :: "('p,'v,'s) configuration" and
  cfg2 :: "('p,'v,'s) configuration" and
  p :: 'p and
  m :: "('p,'v) message" and
  m' :: "('p,'v) message"
assumes
  Step: "cfg1 \<turnstile> m \<mapsto> cfg2" and
  "m \<noteq> m'"
shows
  "msgs cfg1 m' \<le> msgs cfg2 m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
m \<noteq> m'

goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
by (cases m, auto)


[STATEMENT]
lemma OnlyOccurenceDisables:
fixes
  cfg1 :: "('p,'v,'s) configuration" and
  cfg2 :: "('p,'v,'s) configuration" and
  p :: 'p and
  m :: "('p,'v) message" and
  m' :: "('p,'v) message"
assumes
  Step: "cfg1 \<turnstile> m \<mapsto> cfg2" and
  En: "enabled cfg1 m'" and
  NotEn: "\<not> (enabled cfg2 m')"
shows
  "m = m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = m'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
enabled cfg1 m'
\<not> enabled cfg2 m'

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
proof (cases m)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x11, inM x12>\<rbrakk> \<Longrightarrow> m = m'
 2. \<And>x2. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> m = m'
 3. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
print_cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x11, inM x12>\<rbrakk> \<Longrightarrow> m = m'
 2. \<And>x2. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> m = m'
 3. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
case (InMsg p bool)
[PROOF STATE]
proof (state)
this:
m = <p, inM bool>

goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x11, inM x12>\<rbrakk> \<Longrightarrow> m = m'
 2. \<And>x2. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> m = m'
 3. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
with Step
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <p, inM bool>
[PROOF STEP]
have "msgs cfg2 = (sends p (states cfg1 p) (Bool bool)
                              \<union># (msgs cfg1 -# <p, inM bool>))"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <p, inM bool>

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>

goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x11, inM x12>\<rbrakk> \<Longrightarrow> m = m'
 2. \<And>x2. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> m = m'
 3. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
thus "m = m'"
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
using InMsg En NotEn
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Bool bool) \<union># msgs cfg1 -# <p, inM bool>
m = <p, inM bool>
enabled cfg1 m'
\<not> enabled cfg2 m'

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
by (auto simp add: enabled_def, metis less_nat_zero_code)
[PROOF STATE]
proof (state)
this:
m = m'

goal (2 subgoals):
 1. \<And>x2. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> m = m'
 2. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> m = m'
 2. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
case (OutMsg bool)
[PROOF STATE]
proof (state)
this:
m = <\<bottom>, outM bool>

goal (2 subgoals):
 1. \<And>x2. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> m = m'
 2. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
with Step
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <\<bottom>, outM bool>
[PROOF STEP]
show "m = m'"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <\<bottom>, outM bool>

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

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
case (Msg p v)
[PROOF STATE]
proof (state)
this:
m = <p, v>

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
with Step
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <p, v>
[PROOF STEP]
have "msgs cfg2 = (sends p (states cfg1 p) (Value v)
                              \<union># (msgs cfg1 -# <p, v>))"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m \<mapsto> cfg2
m = <p, v>

goal (1 subgoal):
 1. msgs cfg2 = sends p (states cfg1 p) (Value v) \<union># msgs cfg1 -# <p, v>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
msgs cfg2 = sends p (states cfg1 p) (Value v) \<union># msgs cfg1 -# <p, v>

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; enabled cfg1 m'; \<not> enabled cfg2 m'; m = <x31, x32>\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
thus "m = m'"
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Value v) \<union># msgs cfg1 -# <p, v>

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
using Msg En NotEn
[PROOF STATE]
proof (prove)
using this:
msgs cfg2 = sends p (states cfg1 p) (Value v) \<union># msgs cfg1 -# <p, v>
m = <p, v>
enabled cfg1 m'
\<not> enabled cfg2 m'

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
by (auto simp add: enabled_def, metis less_nat_zero_code)
[PROOF STATE]
proof (state)
this:
m = m'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ReachableStepFirst:
assumes
  "reachable cfg cfg'"
shows
  "cfg = cfg' \<or> (\<exists> cfg1 msg p . (cfg \<turnstile> msg \<mapsto> cfg1) \<and> enabled cfg msg
                    \<and> isReceiverOf p msg
                    \<and> reachable cfg1 cfg')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg = cfg' \<or> (\<exists>cfg1 msg p. cfg \<turnstile> msg \<mapsto> cfg1 \<and> enabled cfg msg \<and> isReceiverOf p msg \<and> reachable cfg1 cfg')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable cfg cfg'

goal (1 subgoal):
 1. cfg = cfg' \<or> (\<exists>cfg1 msg p. cfg \<turnstile> msg \<mapsto> cfg1 \<and> enabled cfg msg \<and> isReceiverOf p msg \<and> reachable cfg1 cfg')
[PROOF STEP]
by (induct rule: reachable.induct, auto,
    metis StepOutMsg ExistsMsg init enabled_def isReceiverOf.simps(1)
    isReceiverOf.simps(2) message.exhaust, metis asynchronousSystem.step)


[STATEMENT]
lemma ReachableTrans:
fixes
  cfg1 cfg2 cfg3 :: "('p, 'v, 's ) configuration" and
  Q :: " 'p set"
assumes
  "reachable cfg1 cfg2" and
  "reachable cfg2 cfg3"
shows "reachable cfg1 cfg3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable cfg1 cfg3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reachable cfg1 cfg3
[PROOF STEP]
have "reachable cfg2 cfg3 \<Longrightarrow> reachable cfg1 cfg2 \<Longrightarrow> reachable cfg1 cfg3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable cfg2 cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
proof (induct rule: reachable.induct, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>reachable cfg1a cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; reachable cfg1 cfg1a\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
fix cfg1' cfg2' msg cfg3'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>reachable cfg1a cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; reachable cfg1 cfg1a\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
assume
      "reachable cfg1 cfg2'"
      "cfg2' \<turnstile> msg \<mapsto> cfg3'"
[PROOF STATE]
proof (state)
this:
reachable cfg1 cfg2'
cfg2' \<turnstile> msg \<mapsto> cfg3'

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>reachable cfg1a cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; reachable cfg1 cfg1a\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
thus "reachable cfg1 cfg3'"
[PROOF STATE]
proof (prove)
using this:
reachable cfg1 cfg2'
cfg2' \<turnstile> msg \<mapsto> cfg3'

goal (1 subgoal):
 1. reachable cfg1 cfg3'
[PROOF STEP]
using reachable.simps
[PROOF STATE]
proof (prove)
using this:
reachable cfg1 cfg2'
cfg2' \<turnstile> msg \<mapsto> cfg3'
reachable ?a1.0 ?a2.0 = ((\<exists>cfg1. ?a1.0 = cfg1 \<and> ?a2.0 = cfg1) \<or> (\<exists>cfg1 cfg2 msg cfg3. ?a1.0 = cfg1 \<and> ?a2.0 = cfg3 \<and> reachable cfg1 cfg2 \<and> cfg2 \<turnstile> msg \<mapsto> cfg3))

goal (1 subgoal):
 1. reachable cfg1 cfg3'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
reachable cfg1 cfg3'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>reachable cfg2 cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3

goal (1 subgoal):
 1. reachable cfg1 cfg3
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reachable cfg2 cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3

goal (1 subgoal):
 1. reachable cfg1 cfg3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reachable cfg2 cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
reachable cfg1 cfg2
reachable cfg2 cfg3

goal (1 subgoal):
 1. reachable cfg1 cfg3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reachable cfg1 cfg3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma StepReachable:
fixes
  cfg cfg' :: "('p,'v,'s) configuration" and
  msg :: "('p, 'v) message"
assumes
  "reachable cfg cfg'" and
  "enabled cfg msg" and
  "\<not> (enabled cfg' msg)"
shows "stepReachable cfg msg cfg'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stepReachable cfg msg cfg'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable cfg cfg'
enabled cfg msg
\<not> enabled cfg' msg

goal (1 subgoal):
 1. stepReachable cfg msg cfg'
[PROOF STEP]
proof(induct rule: reachable.induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 cfg2 msga cfg3. \<lbrakk>reachable cfg1 cfg2; \<lbrakk>enabled cfg1 msg; \<not> enabled cfg2 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg2; cfg2 \<turnstile> msga \<mapsto> cfg3; enabled cfg1 msg; \<not> enabled cfg3 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
fix cfg1 cfg2 msga cfg3
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 cfg2 msga cfg3. \<lbrakk>reachable cfg1 cfg2; \<lbrakk>enabled cfg1 msg; \<not> enabled cfg2 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg2; cfg2 \<turnstile> msga \<mapsto> cfg3; enabled cfg1 msg; \<not> enabled cfg3 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
assume Step: "cfg2 \<turnstile> msga \<mapsto> cfg3" and
    ReachCfg1Cfg2: "reachable cfg1 cfg2" and
    IV: "(enabled cfg1 msg \<Longrightarrow> \<not> enabled cfg2 msg
        \<Longrightarrow> stepReachable cfg1 msg cfg2)" and
    AssumpInduct: "enabled cfg1 msg" "\<not> enabled cfg3 msg"
[PROOF STATE]
proof (state)
this:
cfg2 \<turnstile> msga \<mapsto> cfg3
reachable cfg1 cfg2
\<lbrakk>enabled cfg1 msg; \<not> enabled cfg2 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg2
enabled cfg1 msg
\<not> enabled cfg3 msg

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msga cfg3. \<lbrakk>reachable cfg1 cfg2; \<lbrakk>enabled cfg1 msg; \<not> enabled cfg2 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg2; cfg2 \<turnstile> msga \<mapsto> cfg3; enabled cfg1 msg; \<not> enabled cfg3 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
have ReachCfg2Cfg3: "reachable cfg2 cfg3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable cfg2 cfg3
[PROOF STEP]
using Step
[PROOF STATE]
proof (prove)
using this:
cfg2 \<turnstile> msga \<mapsto> cfg3

goal (1 subgoal):
 1. reachable cfg2 cfg3
[PROOF STEP]
by (metis reachable.init reachable.step)
[PROOF STATE]
proof (state)
this:
reachable cfg2 cfg3

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msga cfg3. \<lbrakk>reachable cfg1 cfg2; \<lbrakk>enabled cfg1 msg; \<not> enabled cfg2 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg2; cfg2 \<turnstile> msga \<mapsto> cfg3; enabled cfg1 msg; \<not> enabled cfg3 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
show "stepReachable cfg1 msg cfg3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stepReachable cfg1 msg cfg3
[PROOF STEP]
proof (cases "enabled cfg2 msg")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
 2. \<not> enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
assume AssumpEnabled: "enabled cfg2 msg"
[PROOF STATE]
proof (state)
this:
enabled cfg2 msg

goal (2 subgoals):
 1. enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
 2. \<not> enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
hence "msga = msg"
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 msg

goal (1 subgoal):
 1. msga = msg
[PROOF STEP]
using OnlyOccurenceDisables Step AssumpInduct(2)
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 msg
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; enabled ?cfg1.0 ?m'; \<not> enabled ?cfg2.0 ?m'\<rbrakk> \<Longrightarrow> ?m = ?m'
cfg2 \<turnstile> msga \<mapsto> cfg3
\<not> enabled cfg3 msg

goal (1 subgoal):
 1. msga = msg
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
msga = msg

goal (2 subgoals):
 1. enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
 2. \<not> enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
thus "stepReachable cfg1 msg cfg3"
[PROOF STATE]
proof (prove)
using this:
msga = msg

goal (1 subgoal):
 1. stepReachable cfg1 msg cfg3
[PROOF STEP]
using ReachCfg1Cfg2 Step
[PROOF STATE]
proof (prove)
using this:
msga = msg
reachable cfg1 cfg2
cfg2 \<turnstile> msga \<mapsto> cfg3

goal (1 subgoal):
 1. stepReachable cfg1 msg cfg3
[PROOF STEP]
unfolding stepReachable_def
[PROOF STATE]
proof (prove)
using this:
msga = msg
reachable cfg1 cfg2
cfg2 \<turnstile> msga \<mapsto> cfg3

goal (1 subgoal):
 1. \<exists>c' c''. reachable cfg1 c' \<and> c' \<turnstile> msg \<mapsto> c'' \<and> reachable c'' cfg3
[PROOF STEP]
by (metis init)
[PROOF STATE]
proof (state)
this:
stepReachable cfg1 msg cfg3

goal (1 subgoal):
 1. \<not> enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
assume AssumpNotEnabled: "\<not> enabled cfg2 msg"
[PROOF STATE]
proof (state)
this:
\<not> enabled cfg2 msg

goal (1 subgoal):
 1. \<not> enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
hence "stepReachable cfg1 msg cfg2"
[PROOF STATE]
proof (prove)
using this:
\<not> enabled cfg2 msg

goal (1 subgoal):
 1. stepReachable cfg1 msg cfg2
[PROOF STEP]
using IV AssumpInduct(1)
[PROOF STATE]
proof (prove)
using this:
\<not> enabled cfg2 msg
\<lbrakk>enabled cfg1 msg; \<not> enabled cfg2 msg\<rbrakk> \<Longrightarrow> stepReachable cfg1 msg cfg2
enabled cfg1 msg

goal (1 subgoal):
 1. stepReachable cfg1 msg cfg2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stepReachable cfg1 msg cfg2

goal (1 subgoal):
 1. \<not> enabled cfg2 msg \<Longrightarrow> stepReachable cfg1 msg cfg3
[PROOF STEP]
thus "stepReachable cfg1 msg cfg3"
[PROOF STATE]
proof (prove)
using this:
stepReachable cfg1 msg cfg2

goal (1 subgoal):
 1. stepReachable cfg1 msg cfg3
[PROOF STEP]
using ReachCfg2Cfg3 ReachableTrans asynchronousSystem.stepReachable_def
[PROOF STATE]
proof (prove)
using this:
stepReachable cfg1 msg cfg2
reachable cfg2 cfg3
\<lbrakk>reachable ?cfg1.0 ?cfg2.0; reachable ?cfg2.0 ?cfg3.0\<rbrakk> \<Longrightarrow> reachable ?cfg1.0 ?cfg3.0
asynchronousSystem.stepReachable ?trans ?sends ?c1.0 ?msg ?c2.0 \<equiv> \<exists>c' c''. asynchronousSystem.reachable ?trans ?sends ?c1.0 c' \<and> asynchronousSystem.steps ?trans ?sends c' ?msg c'' \<and> asynchronousSystem.reachable ?trans ?sends c'' ?c2.0

goal (1 subgoal):
 1. stepReachable cfg1 msg cfg3
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stepReachable cfg1 msg cfg3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stepReachable cfg1 msg cfg3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma QReachImplReach:
fixes
  cfg1 cfg2::  "('p, 'v, 's ) configuration" and
  Q :: " 'p set"
assumes
  "qReachable cfg1 Q cfg2"
shows
  "reachable cfg1 cfg2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable cfg1 cfg2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1 Q cfg2

goal (1 subgoal):
 1. reachable cfg1 cfg2
[PROOF STEP]
proof (induct rule: qReachable.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfg1 Q. reachable cfg1 cfg1
 2. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
case InitQ
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>cfg1 Q. reachable cfg1 cfg1
 2. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable cfg1_ cfg1_
[PROOF STEP]
using reachable.simps
[PROOF STATE]
proof (prove)
using this:
reachable ?a1.0 ?a2.0 = ((\<exists>cfg1. ?a1.0 = cfg1 \<and> ?a2.0 = cfg1) \<or> (\<exists>cfg1 cfg2 msg cfg3. ?a1.0 = cfg1 \<and> ?a2.0 = cfg3 \<and> reachable cfg1 cfg2 \<and> cfg2 \<turnstile> msg \<mapsto> cfg3))

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

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
case StepQ
[PROOF STATE]
proof (state)
this:
qReachable cfg1_ Q_ cfg2_
reachable cfg1_ cfg2_
cfg2_ \<turnstile> msg_ \<mapsto> cfg3_
\<exists>p\<in>Q_. isReceiverOf p msg_

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; reachable cfg1 cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> reachable cfg1 cfg3
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1_ Q_ cfg2_
reachable cfg1_ cfg2_
cfg2_ \<turnstile> msg_ \<mapsto> cfg3_
\<exists>p\<in>Q_. isReceiverOf p msg_

goal (1 subgoal):
 1. reachable cfg1_ cfg3_
[PROOF STEP]
using reachable.step
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1_ Q_ cfg2_
reachable cfg1_ cfg2_
cfg2_ \<turnstile> msg_ \<mapsto> cfg3_
\<exists>p\<in>Q_. isReceiverOf p msg_
\<lbrakk>reachable ?cfg1.0 ?cfg2.0; ?cfg2.0 \<turnstile> ?msg \<mapsto> ?cfg3.0\<rbrakk> \<Longrightarrow> reachable ?cfg1.0 ?cfg3.0

goal (1 subgoal):
 1. reachable cfg1_ cfg3_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reachable cfg1_ cfg3_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma QReachableTrans:
fixes cfg1 cfg2 cfg3 :: "('p, 'v, 's ) configuration" and
  Q :: " 'p set"
assumes "qReachable cfg2 Q cfg3" and
  "qReachable cfg1 Q cfg2"
shows "qReachable cfg1 Q cfg3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qReachable cfg1 Q cfg3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qReachable cfg2 Q cfg3
qReachable cfg1 Q cfg2

goal (1 subgoal):
 1. qReachable cfg1 Q cfg3
[PROOF STEP]
proof (induct rule: qReachable.induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1a Q cfg2; qReachable cfg1 Q cfg1a \<Longrightarrow> qReachable cfg1 Q cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg; qReachable cfg1 Q cfg1a\<rbrakk> \<Longrightarrow> qReachable cfg1 Q cfg3
[PROOF STEP]
case (StepQ)
[PROOF STATE]
proof (state)
this:
qReachable cfg1_ Q_ cfg2_
qReachable cfg1 Q_ cfg1_ \<Longrightarrow> qReachable cfg1 Q_ cfg2_
cfg2_ \<turnstile> msg_ \<mapsto> cfg3_
\<exists>p\<in>Q_. isReceiverOf p msg_
qReachable cfg1 Q_ cfg1_

goal (1 subgoal):
 1. \<And>cfg1a Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1a Q cfg2; qReachable cfg1 Q cfg1a \<Longrightarrow> qReachable cfg1 Q cfg2; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg; qReachable cfg1 Q cfg1a\<rbrakk> \<Longrightarrow> qReachable cfg1 Q cfg3
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1_ Q_ cfg2_
qReachable cfg1 Q_ cfg1_ \<Longrightarrow> qReachable cfg1 Q_ cfg2_
cfg2_ \<turnstile> msg_ \<mapsto> cfg3_
\<exists>p\<in>Q_. isReceiverOf p msg_
qReachable cfg1 Q_ cfg1_

goal (1 subgoal):
 1. qReachable cfg1 Q_ cfg3_
[PROOF STEP]
using qReachable.simps
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1_ Q_ cfg2_
qReachable cfg1 Q_ cfg1_ \<Longrightarrow> qReachable cfg1 Q_ cfg2_
cfg2_ \<turnstile> msg_ \<mapsto> cfg3_
\<exists>p\<in>Q_. isReceiverOf p msg_
qReachable cfg1 Q_ cfg1_
qReachable ?a1.0 ?a2.0 ?a3.0 = ((\<exists>cfg1 Q. ?a1.0 = cfg1 \<and> ?a2.0 = Q \<and> ?a3.0 = cfg1) \<or> (\<exists>cfg1 Q cfg2 msg cfg3. ?a1.0 = cfg1 \<and> ?a2.0 = Q \<and> ?a3.0 = cfg3 \<and> qReachable cfg1 Q cfg2 \<and> cfg2 \<turnstile> msg \<mapsto> cfg3 \<and> (\<exists>p\<in>Q. isReceiverOf p msg)))

goal (1 subgoal):
 1. qReachable cfg1 Q_ cfg3_
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
qReachable cfg1 Q_ cfg3_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma NotInQFrozenQReachability:
fixes
  cfg1 cfg2 :: "('p,'v,'s) configuration" and
  p :: 'p and
  Q :: "'p set"
assumes
  "qReachable cfg1 Q cfg2" and
  "p \<notin> Q"
shows
  "states cfg1 p = states cfg2 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. states cfg1 p = states cfg2 p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1 Q cfg2
p \<notin> Q

goal (1 subgoal):
 1. states cfg1 p = states cfg2 p
[PROOF STEP]
proof(induct rule: qReachable.induct, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
fix cfg1' Q' cfg2' msg cfg3 p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
assume "qReachable cfg1' Q' cfg2'"
[PROOF STATE]
proof (state)
this:
qReachable cfg1' Q' cfg2'

goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
assume Step: "cfg2' \<turnstile> msg \<mapsto> cfg3"
[PROOF STATE]
proof (state)
this:
cfg2' \<turnstile> msg \<mapsto> cfg3

goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
assume Rec: "isReceiverOf p' msg"
[PROOF STATE]
proof (state)
this:
isReceiverOf p' msg

goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
assume "p' \<in> Q'"  "p \<notin> Q'"
[PROOF STATE]
proof (state)
this:
p' \<in> Q'
p \<notin> Q'

goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
hence notEq: "p \<noteq> p'"
[PROOF STATE]
proof (prove)
using this:
p' \<in> Q'
p \<notin> Q'

goal (1 subgoal):
 1. p \<noteq> p'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<noteq> p'

goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
with Rec
[PROOF STATE]
proof (chain)
picking this:
isReceiverOf p' msg
p \<noteq> p'
[PROOF STEP]
have "\<not> (isReceiverOf p msg)"
[PROOF STATE]
proof (prove)
using this:
isReceiverOf p' msg
p \<noteq> p'

goal (1 subgoal):
 1. \<not> isReceiverOf p msg
[PROOF STEP]
by (cases msg, simp_all)
[PROOF STATE]
proof (state)
this:
\<not> isReceiverOf p msg

goal (1 subgoal):
 1. \<And>cfg1a Qa cfg2a msg cfg3 pa. \<lbrakk>qReachable cfg1a Qa cfg2a; states cfg1a p = states cfg2a p; cfg2a \<turnstile> msg \<mapsto> cfg3; p \<notin> Qa; qReachable cfg1 Q cfg2; p \<notin> Q; pa \<in> Qa; isReceiverOf pa msg\<rbrakk> \<Longrightarrow> states cfg2a p = states cfg3 p
[PROOF STEP]
thus "states cfg2' p = states cfg3 p"
[PROOF STATE]
proof (prove)
using this:
\<not> isReceiverOf p msg

goal (1 subgoal):
 1. states cfg2' p = states cfg3 p
[PROOF STEP]
using Step NoReceivingNoChange
[PROOF STATE]
proof (prove)
using this:
\<not> isReceiverOf p msg
cfg2' \<turnstile> msg \<mapsto> cfg3
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; \<not> isReceiverOf ?p ?m\<rbrakk> \<Longrightarrow> states ?cfg1.0 ?p = states ?cfg2.0 ?p

goal (1 subgoal):
 1. states cfg2' p = states cfg3 p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
states cfg2' p = states cfg3 p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma NoActivityNoMessageLoss :
fixes
  cfg1 cfg2 :: "('p,'v,'s) configuration" and
  p :: 'p and
  Q :: "'p set" and
  m' :: "('p, 'v) message"
assumes
  "qReachable cfg1 Q cfg2" and
  "p \<notin> Q" and
  "isReceiverOf p m'"
shows
  "(msgs cfg1 m') \<le> (msgs cfg2 m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1 Q cfg2
p \<notin> Q
isReceiverOf p m'

goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
proof (induct rule: qReachable.induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; \<lbrakk>p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg2 m'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg; p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg3 m'
[PROOF STEP]
case (StepQ cfg1' Q' cfg2' msg cfg3)
[PROOF STATE]
proof (state)
this:
qReachable cfg1' Q' cfg2'
\<lbrakk>p \<notin> Q'; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1' m' \<le> msgs cfg2' m'
cfg2' \<turnstile> msg \<mapsto> cfg3
\<exists>p\<in>Q'. isReceiverOf p msg
p \<notin> Q'
isReceiverOf p m'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; \<lbrakk>p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg2 m'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg; p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg3 m'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg1' Q' cfg2'
\<lbrakk>p \<notin> Q'; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1' m' \<le> msgs cfg2' m'
cfg2' \<turnstile> msg \<mapsto> cfg3
\<exists>p\<in>Q'. isReceiverOf p msg
p \<notin> Q'
isReceiverOf p m'
[PROOF STEP]
obtain p' where
    P': "p' \<in> Q'" "isReceiverOf p' msg" "p \<noteq> p'"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1' Q' cfg2'
\<lbrakk>p \<notin> Q'; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1' m' \<le> msgs cfg2' m'
cfg2' \<turnstile> msg \<mapsto> cfg3
\<exists>p\<in>Q'. isReceiverOf p msg
p \<notin> Q'
isReceiverOf p m'

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>p' \<in> Q'; isReceiverOf p' msg; p \<noteq> p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' \<in> Q'
isReceiverOf p' msg
p \<noteq> p'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; \<lbrakk>p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg2 m'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg; p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg3 m'
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
isReceiverOf p m'
p' \<in> Q'
isReceiverOf p' msg
p \<noteq> p'
[PROOF STEP]
have "\<not>(isReceiverOf p' m')"
[PROOF STATE]
proof (prove)
using this:
isReceiverOf p m'
p' \<in> Q'
isReceiverOf p' msg
p \<noteq> p'

goal (1 subgoal):
 1. \<not> isReceiverOf p' m'
[PROOF STEP]
by (cases m', simp_all)
[PROOF STATE]
proof (state)
this:
\<not> isReceiverOf p' m'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; \<lbrakk>p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg2 m'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg; p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg3 m'
[PROOF STEP]
with NoMessageLossStep StepQ(3) P'
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; isReceiverOf ?p ?m; \<not> isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'
cfg2' \<turnstile> msg \<mapsto> cfg3
p' \<in> Q'
isReceiverOf p' msg
p \<noteq> p'
\<not> isReceiverOf p' m'
[PROOF STEP]
have "msgs cfg2' m' \<le> msgs cfg3 m'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; isReceiverOf ?p ?m; \<not> isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'
cfg2' \<turnstile> msg \<mapsto> cfg3
p' \<in> Q'
isReceiverOf p' msg
p \<noteq> p'
\<not> isReceiverOf p' m'

goal (1 subgoal):
 1. msgs cfg2' m' \<le> msgs cfg3 m'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg2' m' \<le> msgs cfg3 m'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2 msg cfg3. \<lbrakk>qReachable cfg1 Q cfg2; \<lbrakk>p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg2 m'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msg; p \<notin> Q; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1 m' \<le> msgs cfg3 m'
[PROOF STEP]
with StepQ
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg1' Q' cfg2'
\<lbrakk>p \<notin> Q'; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1' m' \<le> msgs cfg2' m'
cfg2' \<turnstile> msg \<mapsto> cfg3
\<exists>p\<in>Q'. isReceiverOf p msg
p \<notin> Q'
isReceiverOf p m'
msgs cfg2' m' \<le> msgs cfg3 m'
[PROOF STEP]
show "msgs cfg1' m' \<le> msgs cfg3 m'"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1' Q' cfg2'
\<lbrakk>p \<notin> Q'; isReceiverOf p m'\<rbrakk> \<Longrightarrow> msgs cfg1' m' \<le> msgs cfg2' m'
cfg2' \<turnstile> msg \<mapsto> cfg3
\<exists>p\<in>Q'. isReceiverOf p msg
p \<notin> Q'
isReceiverOf p m'
msgs cfg2' m' \<le> msgs cfg3 m'

goal (1 subgoal):
 1. msgs cfg1' m' \<le> msgs cfg3 m'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msgs cfg1' m' \<le> msgs cfg3 m'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma NoMessageLoss:
fixes
  cfg1 cfg2 :: "('p,'v,'s) configuration" and
  p :: 'p and
  Q :: "'p set" and
  m' :: "('p, 'v) message"
assumes
  "withoutQReachable cfg1 Q cfg2" and
  "p \<in> Q" and
  "isReceiverOf p m'"
shows
  "(msgs cfg1 m') \<le> (msgs cfg2 m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
using assms NoActivityNoMessageLoss
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1 (Proc - Q) cfg2
p \<in> Q
isReceiverOf p m'
\<lbrakk>qReachable ?cfg1.0 ?Q ?cfg2.0; ?p \<notin> ?Q; isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'

goal (1 subgoal):
 1. msgs cfg1 m' \<le> msgs cfg2 m'
[PROOF STEP]
by simp


[STATEMENT]
lemma NoOutMessageLoss:
fixes
  cfg1 cfg2 :: "('p,'v,'s) configuration" and
  v :: bool
assumes
  "reachable cfg1 cfg2"
shows
  "(msgs cfg1 <\<bottom>, outM v>) \<le> (msgs cfg2 <\<bottom>, outM v>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable cfg1 cfg2

goal (1 subgoal):
 1. msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>
[PROOF STEP]
proof(induct rule: reachable.induct, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a cfg2a msg cfg3. \<lbrakk>reachable cfg1a cfg2a; msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg2a <\<bottom>, outM v>; cfg2a \<turnstile> msg \<mapsto> cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg3 <\<bottom>, outM v>
[PROOF STEP]
fix cfg1 cfg' msg cfg2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a cfg2a msg cfg3. \<lbrakk>reachable cfg1a cfg2a; msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg2a <\<bottom>, outM v>; cfg2a \<turnstile> msg \<mapsto> cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg3 <\<bottom>, outM v>
[PROOF STEP]
assume AssInduct:
    "reachable cfg1 cfg'"
    "msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg' <\<bottom>, outM v>"
    "cfg' \<turnstile> msg \<mapsto> cfg2"
[PROOF STATE]
proof (state)
this:
reachable cfg1 cfg'
msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg' <\<bottom>, outM v>
cfg' \<turnstile> msg \<mapsto> cfg2

goal (1 subgoal):
 1. \<And>cfg1a cfg2a msg cfg3. \<lbrakk>reachable cfg1a cfg2a; msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg2a <\<bottom>, outM v>; cfg2a \<turnstile> msg \<mapsto> cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg3 <\<bottom>, outM v>
[PROOF STEP]
from AssInduct(3)
[PROOF STATE]
proof (chain)
picking this:
cfg' \<turnstile> msg \<mapsto> cfg2
[PROOF STEP]
have "msgs cfg' <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>"
[PROOF STATE]
proof (prove)
using this:
cfg' \<turnstile> msg \<mapsto> cfg2

goal (1 subgoal):
 1. msgs cfg' <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>
[PROOF STEP]
by (cases msg, auto)
[PROOF STATE]
proof (state)
this:
msgs cfg' <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>

goal (1 subgoal):
 1. \<And>cfg1a cfg2a msg cfg3. \<lbrakk>reachable cfg1a cfg2a; msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg2a <\<bottom>, outM v>; cfg2a \<turnstile> msg \<mapsto> cfg3; reachable cfg1 cfg2\<rbrakk> \<Longrightarrow> msgs cfg1a <\<bottom>, outM v> \<le> msgs cfg3 <\<bottom>, outM v>
[PROOF STEP]
with AssInduct(2)
[PROOF STATE]
proof (chain)
picking this:
msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg' <\<bottom>, outM v>
msgs cfg' <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>
[PROOF STEP]
show " msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>"
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg' <\<bottom>, outM v>
msgs cfg' <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>

goal (1 subgoal):
 1. msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>
[PROOF STEP]
using le_trans
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg' <\<bottom>, outM v>
msgs cfg' <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>
\<lbrakk>?i \<le> ?j; ?j \<le> ?k\<rbrakk> \<Longrightarrow> ?i \<le> ?k

goal (1 subgoal):
 1. msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
msgs cfg1 <\<bottom>, outM v> \<le> msgs cfg2 <\<bottom>, outM v>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma StillEnabled:
fixes
  cfg1 cfg2:: "('p,'v,'s) configuration" and
  p :: 'p and
  msg :: "('p,'v) message" and
  Q :: "'p set"
assumes
  "withoutQReachable cfg1 Q cfg2" and
  "p \<in> Q" and
  "isReceiverOf p msg" and
  "enabled cfg1 msg"
shows
  "enabled cfg2 msg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enabled cfg2 msg
[PROOF STEP]
using assms enabled_def NoMessageLoss
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1 (Proc - Q) cfg2
p \<in> Q
isReceiverOf p msg
enabled cfg1 msg
enabled ?cfg ?msg \<equiv> ?msg \<in># msgs ?cfg
\<lbrakk>qReachable ?cfg1.0 (Proc - ?Q) ?cfg2.0; ?p \<in> ?Q; isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'

goal (1 subgoal):
 1. enabled cfg2 msg
[PROOF STEP]
by (metis le_0_eq neq0_conv)


[STATEMENT]
lemma InitialIsInitReachable :
assumes "initial c"
shows "initReachable c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. initReachable c
[PROOF STEP]
using assms reachable.init
[PROOF STATE]
proof (prove)
using this:
initial c
reachable ?cfg1.0 ?cfg1.0

goal (1 subgoal):
 1. initReachable c
[PROOF STEP]
unfolding initReachable_def
[PROOF STATE]
proof (prove)
using this:
initial c
reachable ?cfg1.0 ?cfg1.0

goal (1 subgoal):
 1. \<exists>cfg0. initial cfg0 \<and> reachable cfg0 c
[PROOF STEP]
by blast