[STATEMENT]
lemma weakBang:
  fixes \<Psi>   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"

  assumes PTrans: "\<Psi> : R \<rhd> P \<parallel> !P \<Longrightarrow>\<alpha> \<prec> P'"
  and     "guarded P"

  shows "\<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : R \<rhd> P \<parallel> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
                           and RImpP'': "insertAssertion(extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame P'') \<Psi>"
                           and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : R \<rhd> P \<parallel> !P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain A\<^sub>P \<Psi>\<^sub>P where FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>" and "A\<^sub>P \<sharp>* \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>P \<Psi>\<^sub>P. \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule freshFrame)
[PROOF STATE]
proof (state)
this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from \<open>guarded P\<close> FrP
[PROOF STATE]
proof (chain)
picking this:
guarded P
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
have "\<Psi>\<^sub>P \<simeq> \<one>"
[PROOF STATE]
proof (prove)
using this:
guarded P
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<Psi>\<^sub>P \<simeq> \<one>
[PROOF STEP]
by(blast dest: guardedStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>P \<simeq> \<one>

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>
\<Psi>\<^sub>P \<simeq> \<one>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>
\<Psi>\<^sub>P \<simeq> \<one>

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
proof(auto simp add: rtrancl_eq_or_trancl)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
have "\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> !P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> !P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> !P

goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> !P

goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
assume RimpP: "insertAssertion(extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>"
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>

goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
have "insertAssertion(extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame(!P)) \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
[PROOF STEP]
from \<open>\<Psi>\<^sub>P \<simeq> \<one>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>P \<simeq> \<one>
[PROOF STEP]
have "\<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>P \<simeq> \<one>

goal (1 subgoal):
 1. \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
by(metis frameIntCompositionSym frameIntAssociativity frameIntCommutativity frameIntIdentity FrameStatEqTrans FrameStatEqSym)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
[PROOF STEP]
from \<open>A\<^sub>P \<sharp>* \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>P \<sharp>* \<Psi>
[PROOF STEP]
have "\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>P \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
by(force intro: frameResFreshChain)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
[PROOF STEP]
using RimpP
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
[PROOF STEP]
by(auto simp add: FrameStatEq_def dest: FrameStatImpTrans)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>

goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>

goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
assume "\<Psi> \<rhd> P \<parallel> !P \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'

goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
hence "\<Psi> \<rhd> !P \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
using \<open>guarded P\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'
guarded P

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
by(rule Bang)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<longmapsto> \<alpha> \<prec> P'

goal (2 subgoals):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<one>\<rangle>; \<Psi> \<rhd> P \<parallel> !P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P'' = P \<parallel> !P\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
 2. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> !P
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
\<Psi> \<rhd> !P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> !P
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (!P)) \<Psi>
\<Psi> \<rhd> !P \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
fix P'''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
assume "\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau>  P''"
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
hence "\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
using \<open>guarded P\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''
guarded P

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
by(rule tauStepChainBang)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
hence "\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
assume "insertAssertion(extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame P'') \<Psi>"
                and "\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<lbrakk>insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* \<Psi>; \<Psi>\<^sub>P \<simeq> \<one>; P \<parallel> !P \<noteq> P''; \<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> !P \<Longrightarrow>\<alpha> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakTransitionFrameImp:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and             "insertAssertion(extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame Q) \<Psi>"

  shows "\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>

goal (1 subgoal):
 1. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(auto simp add: weakTransition_def intro: FrameStatImpTrans)


[STATEMENT]
lemma guardedFrameStatEq:
  fixes P :: "('a, 'b, 'c) psi"

  assumes "guarded P"

  shows "extractFrame P \<simeq>\<^sub>F \<langle>\<epsilon>, \<one>\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
obtain A\<^sub>P \<Psi>\<^sub>P where FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>P \<Psi>\<^sub>P. extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule freshFrame)
[PROOF STATE]
proof (state)
this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
from \<open>guarded P\<close> FrP
[PROOF STATE]
proof (chain)
picking this:
guarded P
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
have "\<Psi>\<^sub>P \<simeq> \<one>"
[PROOF STATE]
proof (prove)
using this:
guarded P
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<Psi>\<^sub>P \<simeq> \<one>
[PROOF STEP]
by(blast dest: guardedStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>P \<simeq> \<one>

goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
hence "\<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<one>\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>P \<simeq> \<one>

goal (1 subgoal):
 1. \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<one>\<rangle>
[PROOF STEP]
by(rule_tac frameResChainPres) auto
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<one>\<rangle>

goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<one>\<rangle>

goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
have "\<langle>A\<^sub>P, \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<one>\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>P, \<one>\<rangle> \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
by(rule_tac frameResFreshChain) auto
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P, \<one>\<rangle> \<simeq>\<^sub>F \<bottom>\<^sub>F

goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<one>\<rangle>
\<langle>A\<^sub>P, \<one>\<rangle> \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<one>\<rangle>
\<langle>A\<^sub>P, \<one>\<rangle> \<simeq>\<^sub>F \<bottom>\<^sub>F

goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
using FrP
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<one>\<rangle>
\<langle>A\<^sub>P, \<one>\<rangle> \<simeq>\<^sub>F \<bottom>\<^sub>F
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F
[PROOF STEP]
by(force intro: FrameStatEqTrans)
[PROOF STATE]
proof (state)
this:
extractFrame P \<simeq>\<^sub>F \<bottom>\<^sub>F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakGuardedTransition:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and    "guarded Q"

  shows "\<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain A\<^sub>Q \<Psi>\<^sub>Q where FrQ: "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>" and "A\<^sub>Q \<sharp>* \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>Q \<Psi>\<^sub>Q. \<lbrakk>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; A\<^sub>Q \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule freshFrame)
[PROOF STATE]
proof (state)
this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from \<open>guarded Q\<close> FrQ
[PROOF STATE]
proof (chain)
picking this:
guarded Q
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
have "\<Psi>\<^sub>Q \<simeq> \<one>"
[PROOF STATE]
proof (prove)
using this:
guarded Q
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<Psi>\<^sub>Q \<simeq> \<one>
[PROOF STEP]
by(blast dest: guardedStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>Q \<simeq> \<one>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
hence "\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>Q \<simeq> \<one>

goal (1 subgoal):
 1. \<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
by(metis frameIntCompositionSym)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from \<open>A\<^sub>Q \<sharp>* \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>Q \<sharp>* \<Psi>
[PROOF STEP]
have "\<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>Q \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
by(rule_tac frameResFreshChain) auto
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
have "insertAssertion(extractFrame Q) \<Psi> \<simeq>\<^sub>F insertAssertion (extractFrame (\<zero>)) \<Psi>"
[PROOF STATE]
proof (prove)
using this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame Q) \<Psi> \<simeq>\<^sub>F insertAssertion (extractFrame (\<zero>)) \<Psi>
[PROOF STEP]
using FrQ \<open>A\<^sub>Q \<sharp>* \<Psi>\<close>
[PROOF STATE]
proof (prove)
using this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>Q, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame Q) \<Psi> \<simeq>\<^sub>F insertAssertion (extractFrame (\<zero>)) \<Psi>
[PROOF STEP]
by simp (blast intro: FrameStatEqTrans)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q) \<Psi> \<simeq>\<^sub>F insertAssertion (extractFrame (\<zero>)) \<Psi>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
insertAssertion (extractFrame Q) \<Psi> \<simeq>\<^sub>F insertAssertion (extractFrame (\<zero>)) \<Psi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
insertAssertion (extractFrame Q) \<Psi> \<simeq>\<^sub>F insertAssertion (extractFrame (\<zero>)) \<Psi>

goal (1 subgoal):
 1. \<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(rule_tac weakTransitionFrameImp) (auto simp add: FrameStatEq_def)
[PROOF STATE]
proof (state)
this:
\<Psi> : \<zero> \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expandTauChainFrame:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   A\<^sub>P :: "name list"
  and   \<Psi>\<^sub>P :: 'b
  and   C   :: "'d::fs_name"

  assumes PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
  and     "distinct A\<^sub>P"
  and     "A\<^sub>P \<sharp>* P"
  and     "A\<^sub>P \<sharp>* C"

  obtains \<Psi>' A\<^sub>P' \<Psi>\<^sub>P' where "extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>" and "\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'" and "A\<^sub>P' \<sharp>* P'" and "A\<^sub>P' \<sharp>* C" and "distinct A\<^sub>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* P'; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using PChain FrP \<open>A\<^sub>P \<sharp>* P\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* P

goal (1 subgoal):
 1. (\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* P'; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(induct arbitrary: thesis rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame a = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* a; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case(TauBase P)
[PROOF STATE]
proof (state)
this:
\<lbrakk>extractFrame P = \<langle>?A\<^sub>P', ?\<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> ?\<Psi>' \<simeq> ?\<Psi>\<^sub>P'; ?A\<^sub>P' \<sharp>* P; ?A\<^sub>P' \<sharp>* C; distinct ?A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* P

goal (2 subgoals):
 1. \<And>a thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame a = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* a; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "\<Psi>\<^sub>P \<otimes> SBottom' \<simeq> \<Psi>\<^sub>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi>\<^sub>P \<otimes> \<one> \<simeq> \<Psi>\<^sub>P
[PROOF STEP]
by(rule Identity)
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>P \<otimes> \<one> \<simeq> \<Psi>\<^sub>P

goal (2 subgoals):
 1. \<And>a thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame a = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* a; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with \<open>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
\<Psi>\<^sub>P \<otimes> \<one> \<simeq> \<Psi>\<^sub>P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
\<Psi>\<^sub>P \<otimes> \<one> \<simeq> \<Psi>\<^sub>P

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* C\<close> \<open>distinct A\<^sub>P\<close>
[PROOF STATE]
proof (prove)
using this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
\<Psi>\<^sub>P \<otimes> \<one> \<simeq> \<Psi>\<^sub>P
A\<^sub>P \<sharp>* P
A\<^sub>P \<sharp>* C
distinct A\<^sub>P

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule TauBase)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case(TauStep P P' P'')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* P'; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> ?thesis; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> ?thesis
\<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''
\<lbrakk>extractFrame P'' = \<langle>?A\<^sub>P', ?\<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> ?\<Psi>' \<simeq> ?\<Psi>\<^sub>P'; ?A\<^sub>P' \<sharp>* P''; ?A\<^sub>P' \<sharp>* C; distinct ?A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* P

goal (1 subgoal):
 1. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from \<open>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>\<close> \<open>A\<^sub>P \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* P
[PROOF STEP]
obtain \<Psi>' A\<^sub>P' \<Psi>\<^sub>P' where FrP': "extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>" and "\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'"
                       and "A\<^sub>P' \<sharp>* P'" and "A\<^sub>P' \<sharp>* C" and "distinct A\<^sub>P'"
[PROOF STATE]
proof (prove)
using this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* P

goal (1 subgoal):
 1. (\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* P'; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac TauStep)
[PROOF STATE]
proof (state)
this:
extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>
\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'
A\<^sub>P' \<sharp>* P'
A\<^sub>P' \<sharp>* C
distinct A\<^sub>P'

goal (1 subgoal):
 1. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from \<open>\<Psi> \<rhd> P' \<longmapsto>\<tau> \<prec> P''\<close> FrP' \<open>distinct A\<^sub>P'\<close> \<open>A\<^sub>P' \<sharp>* P'\<close> \<open>A\<^sub>P' \<sharp>* C\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''
extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>
distinct A\<^sub>P'
A\<^sub>P' \<sharp>* P'
A\<^sub>P' \<sharp>* C
[PROOF STEP]
obtain \<Psi>'' A\<^sub>P'' \<Psi>\<^sub>P'' where FrP'': "extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>" and "\<Psi>\<^sub>P' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''"
                          and "A\<^sub>P'' \<sharp>* P''" and "A\<^sub>P'' \<sharp>* C" and "distinct A\<^sub>P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''
extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>
distinct A\<^sub>P'
A\<^sub>P' \<sharp>* P'
A\<^sub>P' \<sharp>* C

goal (1 subgoal):
 1. (\<And>A\<^sub>P'' \<Psi>\<^sub>P'' \<Psi>''. \<lbrakk>extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>; \<Psi>\<^sub>P' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''; A\<^sub>P'' \<sharp>* P''; A\<^sub>P'' \<sharp>* C; distinct A\<^sub>P''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule expandTauFrame)
[PROOF STATE]
proof (state)
this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi>\<^sub>P' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* C
distinct A\<^sub>P''

goal (1 subgoal):
 1. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from \<open>\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'
[PROOF STEP]
have "(\<Psi>\<^sub>P \<otimes> \<Psi>') \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P' \<otimes> \<Psi>''"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'

goal (1 subgoal):
 1. (\<Psi>\<^sub>P \<otimes> \<Psi>') \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P' \<otimes> \<Psi>''
[PROOF STEP]
by(rule Composition)
[PROOF STATE]
proof (state)
this:
(\<Psi>\<^sub>P \<otimes> \<Psi>') \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P' \<otimes> \<Psi>''

goal (1 subgoal):
 1. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with \<open>\<Psi>\<^sub>P' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>P' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''
(\<Psi>\<^sub>P \<otimes> \<Psi>') \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P' \<otimes> \<Psi>''
[PROOF STEP]
have "\<Psi>\<^sub>P \<otimes> \<Psi>' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>P' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''
(\<Psi>\<^sub>P \<otimes> \<Psi>') \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P' \<otimes> \<Psi>''

goal (1 subgoal):
 1. \<Psi>\<^sub>P \<otimes> \<Psi>' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''
[PROOF STEP]
by(metis AssertionStatEqTrans Associativity Commutativity)
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>P \<otimes> \<Psi>' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''

goal (1 subgoal):
 1. \<And>a b c thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>thesis. \<lbrakk>\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame b = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* b; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; \<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame c = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* c; A\<^sub>P' \<sharp>* C; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis; extractFrame a = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>P \<sharp>* a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with FrP''
[PROOF STATE]
proof (chain)
picking this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi>\<^sub>P \<otimes> \<Psi>' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi>\<^sub>P \<otimes> \<Psi>' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using \<open>A\<^sub>P'' \<sharp>* P''\<close> \<open>A\<^sub>P'' \<sharp>* C\<close> \<open>distinct A\<^sub>P''\<close>
[PROOF STATE]
proof (prove)
using this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi>\<^sub>P \<otimes> \<Psi>' \<otimes> \<Psi>'' \<simeq> \<Psi>\<^sub>P''
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* C
distinct A\<^sub>P''

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule TauStep)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frameIntImpComposition:
  fixes \<Psi>  :: 'b
  and   \<Psi>' :: 'b
  and   A\<^sub>F :: "name list"
  and   \<Psi>\<^sub>F :: 'b

  assumes "\<Psi> \<simeq> \<Psi>'"

  shows "\<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
using assms frameIntComposition
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<simeq> \<Psi>'
?\<Psi> \<simeq> ?\<Psi>' \<Longrightarrow> \<langle>?A\<^sub>F, ?\<Psi> \<otimes> ?\<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>?A\<^sub>F, ?\<Psi>' \<otimes> ?\<Psi>\<^sub>F\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
by(simp add: FrameStatEq_def)


[STATEMENT]
lemma tauChainInduct2[consumes 1, case_names TauBase TauStep]:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     cBase: "\<And>P. Prop P P"
  and     cStep: "\<And>P P' P''. \<lbrakk>\<Psi> \<rhd> P' \<longmapsto>\<tau> \<prec> P''; \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; Prop P P'\<rbrakk> \<Longrightarrow> Prop P P''"

  shows "Prop P P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prop P P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
Prop ?P ?P
\<lbrakk>\<Psi> \<rhd> ?P' \<longmapsto> \<tau> \<prec> ?P''; \<Psi> \<rhd> ?P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; Prop ?P ?P'\<rbrakk> \<Longrightarrow> Prop ?P ?P''

goal (1 subgoal):
 1. Prop P P'
[PROOF STEP]
by(rule tauChainInduct)


[STATEMENT]
lemma tauStepChainInduct2[consumes 1, case_names TauBase TauStep]:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     cBase: "\<And>P P'. \<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P' \<Longrightarrow> Prop P P'"
  and     cStep: "\<And>P P' P''. \<lbrakk>\<Psi> \<rhd> P' \<longmapsto>\<tau> \<prec> P''; \<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'; Prop P P'\<rbrakk> \<Longrightarrow> Prop P P''"

  shows "Prop P P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prop P P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
\<Psi> \<rhd> ?P \<longmapsto> \<tau> \<prec> ?P' \<Longrightarrow> Prop ?P ?P'
\<lbrakk>\<Psi> \<rhd> ?P' \<longmapsto> \<tau> \<prec> ?P''; \<Psi> \<rhd> ?P \<Longrightarrow>\<^sub>\<tau> ?P'; Prop ?P ?P'\<rbrakk> \<Longrightarrow> Prop ?P ?P''

goal (1 subgoal):
 1. Prop P P'
[PROOF STEP]
by(rule tauStepChainInduct)