[STATEMENT]
lemma par_qmsg_oreachable_statelessassm:
  assumes "(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
                               (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})"
      and ustutter: "\<And>\<xi>. U \<xi> \<xi>"
  shows "(\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})
         \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R)
         \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})
[PROOF STEP]
have "(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
                                (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)))
                                (other (\<lambda>_ _. True) {i})"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})

goal (1 subgoal):
 1. (\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
have "A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)),
                  other (\<lambda>_ _. True) {i} \<rightarrow>) globala (\<lambda>(\<sigma>, _, \<sigma>'). True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). True)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). True)

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})
A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). True)
[PROOF STEP]
obtain "(\<sigma>, fst \<zeta>) \<in> oreachable A
                           (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})"
         and  *: "snd \<zeta> \<in> reachable qmsg (recvmsg R)"
         and **: "(\<forall>m\<in>set (fst (snd \<zeta>)). R m)"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})
A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). True)

goal (1 subgoal):
 1. (\<lbrakk>(\<sigma>, fst \<zeta>) \<in> oreachable A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i}); snd \<zeta> \<in> reachable qmsg (recvmsg R); \<forall>m\<in>set (fst (snd \<zeta>)). R m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: par_qmsg_oreachable)
[PROOF STATE]
proof (state)
this:
(\<sigma>, fst \<zeta>) \<in> oreachable A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})
snd \<zeta> \<in> reachable qmsg (recvmsg R)
\<forall>m\<in>set (fst (snd \<zeta>)). R m

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, fst \<zeta>) \<in> oreachable A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})
[PROOF STEP]
have "(\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, fst \<zeta>) \<in> oreachable A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R))) (other (\<lambda>_ _. True) {i})

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})
[PROOF STEP]
by rule auto
[PROOF STATE]
proof (state)
this:
(\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i})
snd \<zeta> \<in> reachable qmsg (recvmsg R)
\<forall>m\<in>set (fst (snd \<zeta>)). R m

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<sigma>, fst \<zeta>) \<in> oreachable A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>) (other (\<lambda>_ _. True) {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg R) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_into_qmsg:
  assumes "A \<Turnstile> (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) global P"
      and "\<And>\<xi>. U \<xi> \<xi>"
      and "\<And>\<xi> \<xi>'. S \<xi> \<xi>' \<Longrightarrow> U \<xi> \<xi>'"
      and "\<And>\<sigma> \<sigma>' m. \<lbrakk> \<forall>j. U (\<sigma> j) (\<sigma>' j); R \<sigma> m \<rbrakk> \<Longrightarrow> R \<sigma>' m"
      and "A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>)
                 globala (\<lambda>(\<sigma>, _, \<sigma>'). U (\<sigma> i) (\<sigma>' i))"
    shows "A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile> (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) global P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile> (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) global P
[PROOF STEP]
proof (rule oinvariant_oreachableI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}) \<Longrightarrow> global P (\<sigma>, s)
[PROOF STEP]
fix \<sigma> \<zeta>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}) \<Longrightarrow> global P (\<sigma>, s)
[PROOF STEP]
assume "(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
[PROOF STATE]
proof (state)
this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}) \<Longrightarrow> global P (\<sigma>, s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
obtain s where "(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. (\<And>s. (\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: par_qmsg_oreachable [OF _ assms(5,2-4)])
[PROOF STATE]
proof (state)
this:
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. \<And>\<sigma> s. (\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}) \<Longrightarrow> global P (\<sigma>, s)
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
A \<Turnstile> (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) global P
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
show "global P (\<sigma>, \<zeta>)"
[PROOF STATE]
proof (prove)
using this:
A \<Turnstile> (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) global P
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. global P (\<sigma>, \<zeta>)
[PROOF STEP]
by (auto dest: oinvariant_weakenD [OF assms(1)])
[PROOF STATE]
proof (state)
this:
global P (\<sigma>, \<zeta>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_step_into_qmsg:
  assumes inv: "A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) globala P"
      and ustutter: "\<And>\<xi>. U \<xi> \<xi>"
      and sgivesu: "\<And>\<xi> \<xi>'. S \<xi> \<xi>' \<Longrightarrow> U \<xi> \<xi>'"
      and upreservesq: "\<And>\<sigma> \<sigma>' m. \<lbrakk> \<forall>j. U (\<sigma> j) (\<sigma>' j); R \<sigma> m \<rbrakk> \<Longrightarrow> R \<sigma>' m"
      and self_sync: "A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>)
                            globala (\<lambda>(\<sigma>, _, \<sigma>'). U (\<sigma> i) (\<sigma>' i))"

      and recv_stutter:  "\<And>\<sigma> \<sigma>' m. \<lbrakk> \<forall>j. U (\<sigma> j) (\<sigma>' j); \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P (\<sigma>, receive m, \<sigma>')"
      and receive_right: "\<And>\<sigma> \<sigma>' m.  P (\<sigma>, receive m, \<sigma>') \<Longrightarrow> P (\<sigma>, \<tau>, \<sigma>')"
    shows "A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) globala P"
      (is "_ \<Turnstile>\<^sub>A (?owS, ?U \<rightarrow>) _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) globala P
[PROOF STEP]
proof (rule ostep_invariantI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
fix \<sigma> \<zeta> a \<sigma>' \<zeta>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
assume or: "(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) ?owS ?U"
       and otr: "((\<sigma>, \<zeta>), a, (\<sigma>', \<zeta>')) \<in> trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)"
       and "?owS \<sigma> \<sigma>' a"
[PROOF STATE]
proof (state)
this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a

goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
[PROOF STEP]
have "((\<sigma>, \<zeta>), a, (\<sigma>', \<zeta>')) \<in> oparp_sos i (trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)

goal (1 subgoal):
 1. ((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)
[PROOF STEP]
obtain s msgs q s' msgs' q'
      where "\<zeta> = (s, (msgs, q))" "\<zeta>' = (s', (msgs', q'))"
        and "((\<sigma>, (s, (msgs, q))), a, (\<sigma>', (s', (msgs', q'))))
               \<in> oparp_sos i (trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. (\<And>s msgs q s' msgs' q'. \<lbrakk>\<zeta> = (s, msgs, q); \<zeta>' = (s', msgs', q'); ((\<sigma>, s, msgs, q), a, \<sigma>', s', msgs', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
\<zeta> = (s, msgs, q)
\<zeta>' = (s', msgs', q')
((\<sigma>, s, msgs, q), a, \<sigma>', s', msgs', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
from this(1-2) and or
[PROOF STATE]
proof (chain)
picking this:
\<zeta> = (s, msgs, q)
\<zeta>' = (s', msgs', q')
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
obtain "(\<sigma>, s) \<in> oreachable A ?owS ?U"
             "(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))"
             "(\<forall>m\<in>set msgs. R \<sigma> m)"
[PROOF STATE]
proof (prove)
using this:
\<zeta> = (s, msgs, q)
\<zeta>' = (s', msgs', q')
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. (\<lbrakk>(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}); (msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>)); \<forall>m\<in>set msgs. R \<sigma> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: par_qmsg_oreachable [OF _ self_sync ustutter sgivesu]
                elim!: upreservesq)
[PROOF STATE]
proof (state)
this:
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
\<forall>m\<in>set msgs. R \<sigma> m

goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
from otr \<open>\<zeta> = (s, (msgs, q))\<close> \<open>\<zeta>' = (s', (msgs', q'))\<close>
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
\<zeta> = (s, msgs, q)
\<zeta>' = (s', msgs', q')
[PROOF STEP]
have "((\<sigma>, (s, (msgs, q))), a, (\<sigma>', (s', (msgs', q'))))
              \<in> oparp_sos i (trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
\<zeta> = (s, msgs, q)
\<zeta>' = (s', msgs', q')

goal (1 subgoal):
 1. ((\<sigma>, s, msgs, q), a, \<sigma>', s', msgs', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<sigma>, s, msgs, q), a, \<sigma>', s', msgs', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
hence "globala P ((\<sigma>, s), a, (\<sigma>', s'))"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s, msgs, q), a, \<sigma>', s', msgs', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (msgs', q') = (msgs, q)\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
assume "((\<sigma>, s), a, (\<sigma>', s')) \<in> trans A"
[PROOF STATE]
proof (state)
this:
((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans A

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (msgs', q') = (msgs, q)\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
with \<open>(\<sigma>, s) \<in> oreachable A ?owS ?U\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans A
[PROOF STEP]
show "globala P ((\<sigma>, s), a, (\<sigma>', s'))"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans A

goal (1 subgoal):
 1. globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
using \<open>?owS \<sigma> \<sigma>' a\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a

goal (1 subgoal):
 1. globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
by (rule ostep_invariantD [OF inv])
[PROOF STATE]
proof (state)
this:
globala P ((\<sigma>, s), a, \<sigma>', s')

goal (2 subgoals):
 1. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
assume "((msgs, q), a, (msgs', q')) \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G"
         and "\<And>m. a \<noteq> send m"
         and "\<sigma>' i = \<sigma> i"
[PROOF STATE]
proof (state)
this:
((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
a \<noteq> send ?m
\<sigma>' i = \<sigma> i

goal (2 subgoals):
 1. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
from this(3) and ustutter
[PROOF STATE]
proof (chain)
picking this:
\<sigma>' i = \<sigma> i
U ?\<xi> ?\<xi>
[PROOF STEP]
have "U (\<sigma> i) (\<sigma>' i)"
[PROOF STATE]
proof (prove)
using this:
\<sigma>' i = \<sigma> i
U ?\<xi> ?\<xi>

goal (1 subgoal):
 1. U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U (\<sigma> i) (\<sigma>' i)

goal (2 subgoals):
 1. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
with \<open>?owS \<sigma> \<sigma>' a\<close> and sgivesu
[PROOF STATE]
proof (chain)
picking this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
S ?\<xi> ?\<xi>' \<Longrightarrow> U ?\<xi> ?\<xi>'
U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
have "\<forall>j. U (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
using this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
S ?\<xi> ?\<xi>' \<Longrightarrow> U ?\<xi> ?\<xi>'
U (\<sigma> i) (\<sigma>' i)

goal (1 subgoal):
 1. \<forall>j. U (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by (clarsimp dest!: otherwith_syncD) metis
[PROOF STATE]
proof (state)
this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (2 subgoals):
 1. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (2 subgoals):
 1. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
have "(\<exists>m. a = receive m) \<or> (a = \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
from \<open>(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
have "(msgs, q) \<in> reachable qmsg TT"
[PROOF STATE]
proof (prove)
using this:
(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (msgs, q) \<in> reachable qmsg TT
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(msgs, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. (\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(msgs, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. (\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
from \<open>((msgs, q), a, (msgs', q')) \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<close>
[PROOF STATE]
proof (chain)
picking this:
((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
[PROOF STEP]
have "((msgs, q), a, (msgs', q')) \<in> trans qmsg"
[PROOF STATE]
proof (prove)
using this:
((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G

goal (1 subgoal):
 1. ((msgs, q), a, msgs', q') \<in> automaton.trans qmsg
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((msgs, q), a, msgs', q') \<in> automaton.trans qmsg

goal (1 subgoal):
 1. (\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(msgs, q) \<in> reachable qmsg TT
((msgs, q), a, msgs', q') \<in> automaton.trans qmsg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(msgs, q) \<in> reachable qmsg TT
((msgs, q), a, msgs', q') \<in> automaton.trans qmsg

goal (1 subgoal):
 1. (\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
using \<open>\<And>m. a \<noteq> send m\<close>
[PROOF STATE]
proof (prove)
using this:
(msgs, q) \<in> reachable qmsg TT
((msgs, q), a, msgs', q') \<in> automaton.trans qmsg
a \<noteq> send ?m

goal (1 subgoal):
 1. (\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
by (auto dest!: step_invariantD [OF qmsg_send_receive_or_tau])
[PROOF STATE]
proof (state)
this:
(\<exists>m. a = receive m) \<or> a = \<tau>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>m. a = receive m) \<or> a = \<tau>

goal (2 subgoals):
 1. \<lbrakk>((msgs, q), a, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
(\<exists>m. a = receive m) \<or> a = \<tau>
[PROOF STEP]
show "globala P ((\<sigma>, s), a, (\<sigma>', s'))"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
(\<exists>m. a = receive m) \<or> a = \<tau>

goal (1 subgoal):
 1. globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
using \<open>\<sigma>' i = \<sigma> i\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
(\<exists>m. a = receive m) \<or> a = \<tau>
\<sigma>' i = \<sigma> i

goal (1 subgoal):
 1. globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
by simp (metis receive_right recv_stutter step_seq_tau)
[PROOF STATE]
proof (state)
this:
globala P ((\<sigma>, s), a, \<sigma>', s')

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
assume "a = \<tau>"
         and "((\<sigma>, s), receive m, (\<sigma>', s')) \<in> trans A"
         and "((msgs, q), send m, (msgs', q')) \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G"
[PROOF STATE]
proof (state)
this:
a = \<tau>
((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A
((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
from \<open>(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
have "(msgs, q) \<in> reachable qmsg TT"
[PROOF STATE]
proof (prove)
using this:
(msgs, q) \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (msgs, q) \<in> reachable qmsg TT
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(msgs, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(msgs, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
from \<open>((msgs, q), send m, (msgs', q')) \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<close>
[PROOF STATE]
proof (chain)
picking this:
((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
[PROOF STEP]
have "((msgs, q), send m, (msgs', q')) \<in> trans qmsg"
[PROOF STATE]
proof (prove)
using this:
((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G

goal (1 subgoal):
 1. ((msgs, q), send m, msgs', q') \<in> automaton.trans qmsg
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((msgs, q), send m, msgs', q') \<in> automaton.trans qmsg

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(msgs, q) \<in> reachable qmsg TT
((msgs, q), send m, msgs', q') \<in> automaton.trans qmsg
[PROOF STEP]
have "m\<in>set msgs"
[PROOF STATE]
proof (prove)
using this:
(msgs, q) \<in> reachable qmsg TT
((msgs, q), send m, msgs', q') \<in> automaton.trans qmsg

goal (1 subgoal):
 1. m \<in> set msgs
[PROOF STEP]
by (auto dest!: step_invariantD [OF qmsg_send_from_queue])
[PROOF STATE]
proof (state)
this:
m \<in> set msgs

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
with \<open>\<forall>m\<in>set msgs. R \<sigma> m\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set msgs. R \<sigma> m
m \<in> set msgs
[PROOF STEP]
have "R \<sigma> m"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set msgs. R \<sigma> m
m \<in> set msgs

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
R \<sigma> m

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
with \<open>?owS \<sigma> \<sigma>' a\<close>
[PROOF STATE]
proof (chain)
picking this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
R \<sigma> m
[PROOF STEP]
have "?owS \<sigma> \<sigma>' (receive m)"
[PROOF STATE]
proof (prove)
using this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
R \<sigma> m

goal (1 subgoal):
 1. otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)
[PROOF STEP]
by (auto dest!: otherwith_syncD)
[PROOF STATE]
proof (state)
this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
with \<open>((\<sigma>, s), receive m, (\<sigma>', s')) \<in> trans A\<close>
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)
[PROOF STEP]
have "globala P ((\<sigma>, s), receive m, (\<sigma>', s'))"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)

goal (1 subgoal):
 1. globala P ((\<sigma>, s), receive m, \<sigma>', s')
[PROOF STEP]
using \<open>(\<sigma>, s) \<in> oreachable A ?owS ?U\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)
(\<sigma>, s) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. globala P ((\<sigma>, s), receive m, \<sigma>', s')
[PROOF STEP]
by - (rule ostep_invariantD [OF inv])
[PROOF STATE]
proof (state)
this:
globala P ((\<sigma>, s), receive m, \<sigma>', s')

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
hence "P (\<sigma>, receive m, \<sigma>')"
[PROOF STATE]
proof (prove)
using this:
globala P ((\<sigma>, s), receive m, \<sigma>', s')

goal (1 subgoal):
 1. P (\<sigma>, receive m, \<sigma>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (\<sigma>, receive m, \<sigma>')

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
hence "P (\<sigma>, \<tau>, \<sigma>')"
[PROOF STATE]
proof (prove)
using this:
P (\<sigma>, receive m, \<sigma>')

goal (1 subgoal):
 1. P (\<sigma>, \<tau>, \<sigma>')
[PROOF STEP]
by (rule receive_right)
[PROOF STATE]
proof (state)
this:
P (\<sigma>, \<tau>, \<sigma>')

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, s), receive m, \<sigma>', s') \<in> automaton.trans A; ((msgs, q), send m, msgs', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
with \<open>a = \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
a = \<tau>
P (\<sigma>, \<tau>, \<sigma>')
[PROOF STEP]
show "globala P ((\<sigma>, s), a, (\<sigma>', s'))"
[PROOF STATE]
proof (prove)
using this:
a = \<tau>
P (\<sigma>, \<tau>, \<sigma>')

goal (1 subgoal):
 1. globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
globala P ((\<sigma>, s), a, \<sigma>', s')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
globala P ((\<sigma>, s), a, \<sigma>', s')

goal (1 subgoal):
 1. \<And>\<sigma> s a \<sigma>' s'. \<lbrakk>(\<sigma>, s) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); ((\<sigma>, s), a, \<sigma>', s') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
with \<open>\<zeta> = (s, (msgs, q))\<close> and \<open>\<zeta>' = (s', (msgs', q'))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<zeta> = (s, msgs, q)
\<zeta>' = (s', msgs', q')
globala P ((\<sigma>, s), a, \<sigma>', s')
[PROOF STEP]
show "globala P ((\<sigma>, \<zeta>), a, (\<sigma>', \<zeta>'))"
[PROOF STATE]
proof (prove)
using this:
\<zeta> = (s, msgs, q)
\<zeta>' = (s', msgs', q')
globala P ((\<sigma>, s), a, \<sigma>', s')

goal (1 subgoal):
 1. globala P ((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
globala P ((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_step_into_qmsg_statelessassm:
  assumes "A \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P"
      and "\<And>\<sigma> \<sigma>' m. \<sigma>' i = \<sigma> i \<Longrightarrow> P (\<sigma>, receive m, \<sigma>')"
      and "\<And>\<sigma> \<sigma>' m. P (\<sigma>, receive m, \<sigma>') \<Longrightarrow> P (\<sigma>, \<tau>, \<sigma>')"
    shows "A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
A \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
have *: "A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)),
                                 other (\<lambda>_ _. True) {i} \<rightarrow>) globala P"
[PROOF STATE]
proof (prove)
using this:
A \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P

goal (1 subgoal):
 1. A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
by rule auto
[PROOF STATE]
proof (state)
this:
A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala P

goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
hence "A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A
              (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala P"
[PROOF STATE]
proof (prove)
using this:
A \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala P

goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
by (rule lift_step_into_qmsg)
         (auto elim!: assms(2-3) simp del: step_seq_tau)
[PROOF STATE]
proof (state)
this:
A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala P

goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (otherwith (\<lambda>_ _. True) {i} (orecvmsg (\<lambda>_. R)), other (\<lambda>_ _. True) {i} \<rightarrow>) globala P

goal (1 subgoal):
 1. A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P
[PROOF STEP]
by rule auto
[PROOF STATE]
proof (state)
this:
A \<langle>\<langle>\<^bsub>i\<^esub> qmsg \<Turnstile>\<^sub>A (\<lambda>\<sigma> _. orecvmsg (\<lambda>_. R) \<sigma>, other (\<lambda>_ _. True) {i} \<rightarrow>) globala P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma external_WT_defs_is_type:
  assumes "wf_prog wf_md P" and "C\<bullet>M(Ts) :: T"
  shows "is_class P C" and "is_type P T" "set Ts \<subseteq> types P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C &&& is_type P T &&& set Ts \<subseteq> types P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
C\<bullet>M(Ts) :: T

goal (1 subgoal):
 1. is_class P C &&& is_type P T &&& set Ts \<subseteq> types P
[PROOF STEP]
by(auto elim: external_WT_defs.cases)


[STATEMENT]
lemma WT_red_external_aggr_imp_red_external:
  "\<lbrakk> wf_prog wf_md P; (ta, va, h') \<in> red_external_aggr P t a M vs h; P,h \<turnstile> a\<bullet>M(vs) : U; P,h \<turnstile> t \<surd>t \<rbrakk>
  \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs), h\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; (ta, va, h') \<in> red_external_aggr P t a M vs h; P,h \<turnstile> a\<bullet>M(vs) : U; P,h \<turnstile> t \<surd>t\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
[PROOF STEP]
apply(drule tconfD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; (ta, va, h') \<in> red_external_aggr P t a M vs h; P,h \<turnstile> a\<bullet>M(vs) : U; \<exists>C. typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor> \<and> P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
[PROOF STEP]
apply(erule external_WT'.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hT Ts Ts' D. \<lbrakk>wf_prog wf_md P; (ta, va, h') \<in> red_external_aggr P t a M vs h; \<exists>C. typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor> \<and> P \<turnstile> C \<preceq>\<^sup>* Thread; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hT Ts Ts' D C. \<lbrakk>wf_prog wf_md P; (ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
[PROOF STEP]
apply(drule (1) sees_wf_native)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D\<bullet>M(Ts') :: U\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
[PROOF STEP]
apply(erule external_WT_defs.cases)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = start; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 2. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = join; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 3. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = interrupt; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 4. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = isInterrupted; Ts' = []; U = Boolean\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 5. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = wait; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 6. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = notify; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 7. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = notifyAll; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 8. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = clone; Ts' = []; U = Class Object\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 9. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = hashcode; Ts' = []; U = Integer\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 10. \<And>hT Ts Ts' D C. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = print; Ts' = [Integer]; U = Void\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
A total of 13 subgoals...
[PROOF STEP]
apply(case_tac [!] hT)
[PROOF STATE]
proof (prove)
goal (26 subgoals):
 1. \<And>hT Ts Ts' D C x1. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = start; Ts' = []; U = Void; hT = Class_type x1\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 2. \<And>hT Ts Ts' D C x21 x22. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = start; Ts' = []; U = Void; hT = Array_type x21 x22\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 3. \<And>hT Ts Ts' D C x1. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = join; Ts' = []; U = Void; hT = Class_type x1\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 4. \<And>hT Ts Ts' D C x21 x22. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = join; Ts' = []; U = Void; hT = Array_type x21 x22\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 5. \<And>hT Ts Ts' D C x1. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = interrupt; Ts' = []; U = Void; hT = Class_type x1\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 6. \<And>hT Ts Ts' D C x21 x22. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = interrupt; Ts' = []; U = Void; hT = Array_type x21 x22\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 7. \<And>hT Ts Ts' D C x1. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = isInterrupted; Ts' = []; U = Boolean; hT = Class_type x1\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 8. \<And>hT Ts Ts' D C x21 x22. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Thread; M = isInterrupted; Ts' = []; U = Boolean; hT = Array_type x21 x22\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 9. \<And>hT Ts Ts' D C x1. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = wait; Ts' = []; U = Void; hT = Class_type x1\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 10. \<And>hT Ts Ts' D C x21 x22. \<lbrakk>(ta, va, h') \<in> red_external_aggr P t a M vs h; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; D = Object; M = wait; Ts' = []; U = Void; hT = Array_type x21 x22\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
A total of 26 subgoals...
[PROOF STEP]
apply(auto 4 4 simp add: red_external_aggr_def widen_Class intro: red_external.intros heap_base.red_external.intros[where addr2thread_id=addr2thread_id and thread_id2addr=thread_id2addr and spurious_wakeups=True and empty_heap=empty_heap and allocate=allocate and typeof_addr=typeof_addr and heap_read=heap_read and heap_write=heap_write] heap_base.red_external.intros[where addr2thread_id=addr2thread_id and thread_id2addr=thread_id2addr and spurious_wakeups=False and empty_heap=empty_heap and allocate=allocate and typeof_addr=typeof_addr and heap_read=heap_read and heap_write=heap_write] split: if_split_asm dest: sees_method_decl_above)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WT_red_external_list_conv:
  "\<lbrakk> wf_prog wf_md P; P,h \<turnstile> a\<bullet>M(vs) : U; P,h \<turnstile> t \<surd>t \<rbrakk>
  \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs), h\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle> \<longleftrightarrow> (ta, va, h') \<in> red_external_aggr P t a M vs h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; P,h \<turnstile> a\<bullet>M(vs) : U; P,h \<turnstile> t \<surd>t\<rbrakk> \<Longrightarrow> P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle> = ((ta, va, h') \<in> red_external_aggr P t a M vs h)
[PROOF STEP]
by(blast intro: WT_red_external_aggr_imp_red_external red_external_imp_red_external_aggr)


[STATEMENT]
lemma red_external_new_thread_sees:
  "\<lbrakk> wf_prog wf_md P; P,t \<turnstile> \<langle>a\<bullet>M(vs), h\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle>; NewThread t' (C, M', a') h'' \<in> set \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<rbrakk>
  \<Longrightarrow> typeof_addr h' a' = \<lfloor>Class_type C\<rfloor> \<and> (\<exists>T meth D. P \<turnstile> C sees M':[]\<rightarrow>T = \<lfloor>meth\<rfloor> in D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; NewThread t' (C, M', a') h'' \<in> set \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>\<rbrakk> \<Longrightarrow> typeof_addr h' a' = \<lfloor>Class_type C\<rfloor> \<and> (\<exists>T meth D. P \<turnstile> C sees M': []\<rightarrow>T = \<lfloor>meth\<rfloor> in D)
[PROOF STEP]
by(fastforce elim!: red_external.cases simp add: widen_Class ta_upd_simps dest: sub_Thread_sees_run)


[STATEMENT]
lemma hconf_heap_copy_loc_mono:
  assumes "heap_copy_loc a a' al h obs h'"
  and "hconf h"
  and "P,h \<turnstile> a@al : T" "P,h \<turnstile> a'@al : T"
  shows "hconf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
from \<open>heap_copy_loc a a' al h obs h'\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_copy_loc a a' al h obs h'
[PROOF STEP]
obtain v
    where read: "heap_read h a al v"
    and "write": "heap_write h a' al v h'"
[PROOF STATE]
proof (prove)
using this:
heap_copy_loc a a' al h obs h'

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>heap_read h a al v; heap_write h a' al v h'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
heap_read h a al v
heap_write h a' al v h'

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
from read \<open>P,h \<turnstile> a@al : T\<close> \<open>hconf h\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_read h a al v
P,h \<turnstile> a@al : T
hconf h
[PROOF STEP]
have "P,h \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
using this:
heap_read h a al v
P,h \<turnstile> a@al : T
hconf h

goal (1 subgoal):
 1. P,h \<turnstile> v :\<le> T
[PROOF STEP]
by(rule heap_read_conf)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> v :\<le> T

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
with "write" \<open>hconf h\<close> \<open>P,h \<turnstile> a'@al : T\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_write h a' al v h'
hconf h
P,h \<turnstile> a'@al : T
P,h \<turnstile> v :\<le> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
heap_write h a' al v h'
hconf h
P,h \<turnstile> a'@al : T
P,h \<turnstile> v :\<le> T

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by(rule hconf_heap_write_mono)
[PROOF STATE]
proof (state)
this:
hconf h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hconf_heap_copies_mono:
  assumes "heap_copies a a' als h obs h'"
  and "hconf h"
  and "list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) als Ts"
  and "list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) als Ts"
  shows "hconf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
heap_copies a a' als h obs h'
hconf h
list_all2 (addr_loc_type P h a) als Ts
list_all2 (addr_loc_type P h a') als Ts

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
proof(induct arbitrary: Ts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) [] Ts; list_all2 (addr_loc_type P h a') [] Ts\<rbrakk> \<Longrightarrow> hconf h
 2. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
hconf h_
list_all2 (addr_loc_type P h_ a) [] Ts
list_all2 (addr_loc_type P h_ a') [] Ts

goal (2 subgoals):
 1. \<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) [] Ts; list_all2 (addr_loc_type P h a') [] Ts\<rbrakk> \<Longrightarrow> hconf h
 2. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
hconf h_
list_all2 (addr_loc_type P h_ a) [] Ts
list_all2 (addr_loc_type P h_ a') [] Ts

goal (1 subgoal):
 1. hconf h_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hconf h_

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
case (Cons al h ob h' als obs h'')
[PROOF STATE]
proof (state)
this:
heap_copy_loc a a' al h ob h'
heap_copies a a' als h' obs h''
\<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als ?Ts14; list_all2 (addr_loc_type P h' a') als ?Ts14\<rbrakk> \<Longrightarrow> hconf h''
hconf h
list_all2 (addr_loc_type P h a) (al # als) Ts
list_all2 (addr_loc_type P h a') (al # als) Ts

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
note step = \<open>heap_copy_loc a a' al h ob h'\<close>
[PROOF STATE]
proof (state)
this:
heap_copy_loc a a' al h ob h'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) (al # als) Ts\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a) (al # als) Ts
[PROOF STEP]
obtain T Ts' where [simp]: "Ts = T # Ts'"
    and "P,h \<turnstile> a@al : T" "list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a) (al # als) Ts

goal (1 subgoal):
 1. (\<And>T Ts'. \<lbrakk>Ts = T # Ts'; P,h \<turnstile> a@al : T; list_all2 (addr_loc_type P h a) als Ts'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: list_all2_Cons1)
[PROOF STATE]
proof (state)
this:
Ts = T # Ts'
P,h \<turnstile> a@al : T
list_all2 (addr_loc_type P h a) als Ts'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) (al # als) Ts\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a') (al # als) Ts
[PROOF STEP]
have "P,h \<turnstile> a'@al : T" "list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a') (al # als) Ts

goal (1 subgoal):
 1. P,h \<turnstile> a'@al : T &&& list_all2 (addr_loc_type P h a') als Ts'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> a'@al : T
list_all2 (addr_loc_type P h a') als Ts'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
from step \<open>hconf h\<close> \<open>P,h \<turnstile> a@al : T\<close> \<open>P,h \<turnstile> a'@al : T\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_copy_loc a a' al h ob h'
hconf h
P,h \<turnstile> a@al : T
P,h \<turnstile> a'@al : T
[PROOF STEP]
have "hconf h'"
[PROOF STATE]
proof (prove)
using this:
heap_copy_loc a a' al h ob h'
hconf h
P,h \<turnstile> a@al : T
P,h \<turnstile> a'@al : T

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by(rule hconf_heap_copy_loc_mono)
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
from step
[PROOF STATE]
proof (chain)
picking this:
heap_copy_loc a a' al h ob h'
[PROOF STEP]
have "h \<unlhd> h'"
[PROOF STATE]
proof (prove)
using this:
heap_copy_loc a a' al h ob h'

goal (1 subgoal):
 1. h \<unlhd> h'
[PROOF STEP]
by(rule hext_heap_copy_loc)
[PROOF STATE]
proof (state)
this:
h \<unlhd> h'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) als Ts'\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a) als Ts'
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h' \<turnstile> a@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a) als Ts'

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a) als Ts'
[PROOF STEP]
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ \<open>h \<unlhd> h'\<close>])
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) als Ts'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) als Ts'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) als Ts'\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a') als Ts'
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h' \<turnstile> a'@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a') als Ts'

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a') als Ts'
[PROOF STEP]
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ \<open>h \<unlhd> h'\<close>])
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a') als Ts'

goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' Ts. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>Ts. \<lbrakk>hconf h'; list_all2 (addr_loc_type P h' a) als Ts; list_all2 (addr_loc_type P h' a') als Ts\<rbrakk> \<Longrightarrow> hconf h''; hconf h; list_all2 (addr_loc_type P h a) (al # als) Ts; list_all2 (addr_loc_type P h a') (al # als) Ts\<rbrakk> \<Longrightarrow> hconf h''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hconf h'
list_all2 (addr_loc_type P h' a) als Ts'
list_all2 (addr_loc_type P h' a') als Ts'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hconf h'
list_all2 (addr_loc_type P h' a) als Ts'
list_all2 (addr_loc_type P h' a') als Ts'

goal (1 subgoal):
 1. hconf h''
[PROOF STEP]
by(rule Cons)
[PROOF STATE]
proof (state)
this:
hconf h''

goal:
No subgoals!
[PROOF STEP]
qed