[STATEMENT]
lemma prime_is_sum4sq: "prime p \<Longrightarrow> is_sum4sq_nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> is_sum4sq_nat p
[PROOF STEP]
using zprime_is_sum4sq is_sum4sq_int_nat_eq
[PROOF STATE]
proof (prove)
using this:
prime (nat ?p) \<Longrightarrow> is_sum4sq_int ?p
is_sum4sq_nat ?n = is_sum4sq_int (int ?n)

goal (1 subgoal):
 1. prime p \<Longrightarrow> is_sum4sq_nat p
[PROOF STEP]
by simp


[STATEMENT]
theorem sum_of_four_squares: "is_sum4sq_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum4sq_nat n
[PROOF STEP]
proof (induction n rule: nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>m<n. is_sum4sq_nat m \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. is_sum4sq_nat m

goal (1 subgoal):
 1. \<And>n. \<forall>m<n. is_sum4sq_nat m \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum4sq_nat n
[PROOF STEP]
proof (cases "n>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
 2. \<not> 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 1 < n

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
 2. \<not> 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
hence "n = 0 \<or> n = 1"
[PROOF STATE]
proof (prove)
using this:
\<not> 1 < n

goal (1 subgoal):
 1. n = 0 \<or> n = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 0 \<or> n = 1

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
 2. \<not> 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = 0 \<or> n = 1

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
 2. \<not> 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
have "0 = sum4sq_nat 0 0 0 0" "1 = sum4sq_nat 1 0 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = sum4sq_nat 0 0 0 0 &&& 1 = sum4sq_nat 1 0 0 0
[PROOF STEP]
unfolding sum4sq_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0\<^sup>2 + 0\<^sup>2 + 0\<^sup>2 + 0\<^sup>2 &&& 1 = 1\<^sup>2 + 0\<^sup>2 + 0\<^sup>2 + 0\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = sum4sq_nat 0 0 0 0
1 = sum4sq_nat 1 0 0 0

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
 2. \<not> 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n = 0 \<or> n = 1
0 = sum4sq_nat 0 0 0 0
1 = sum4sq_nat 1 0 0 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0 \<or> n = 1
0 = sum4sq_nat 0 0 0 0
1 = sum4sq_nat 1 0 0 0

goal (1 subgoal):
 1. is_sum4sq_nat n
[PROOF STEP]
unfolding is_sum4sq_nat_def
[PROOF STATE]
proof (prove)
using this:
n = 0 \<or> n = 1
0 = sum4sq_nat 0 0 0 0
1 = sum4sq_nat 1 0 0 0

goal (1 subgoal):
 1. \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_sum4sq_nat n

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
1 < n

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
obtain p m where dec: "prime p \<and> n = p * m"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. (\<And>p m. prime p \<and> n = p * m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_factor_nat[of n]
[PROOF STATE]
proof (prove)
using this:
1 < n
n \<noteq> 1 \<Longrightarrow> \<exists>p. prime p \<and> p dvd n

goal (1 subgoal):
 1. (\<And>p m. prime p \<and> n = p * m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: dvdE)
[PROOF STATE]
proof (state)
this:
prime p \<and> n = p * m

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prime p \<and> n = p * m

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
hence "m<n"
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m

goal (1 subgoal):
 1. m < n
[PROOF STEP]
using n_less_m_mult_n[of m p] prime_gt_Suc_0_nat[of p] True
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
\<lbrakk>0 < m; Suc 0 < p\<rbrakk> \<Longrightarrow> m < p * m
prime p \<Longrightarrow> Suc 0 < p
1 < n

goal (1 subgoal):
 1. m < n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
m < n

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prime p \<and> n = p * m
m < n
[PROOF STEP]
have "is_sum4sq_nat m" "is_sum4sq_nat p"
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
m < n

goal (1 subgoal):
 1. is_sum4sq_nat m &&& is_sum4sq_nat p
[PROOF STEP]
using 1 prime_is_sum4sq
[PROOF STATE]
proof (prove)
using this:
prime p \<and> n = p * m
m < n
\<forall>m<n. is_sum4sq_nat m
prime ?p \<Longrightarrow> is_sum4sq_nat ?p

goal (1 subgoal):
 1. is_sum4sq_nat m &&& is_sum4sq_nat p
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
is_sum4sq_nat m
is_sum4sq_nat p

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> is_sum4sq_nat n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_sum4sq_nat m
is_sum4sq_nat p

goal (1 subgoal):
 1. is_sum4sq_nat n
[PROOF STEP]
using dec is_mult_sum4sq_nat
[PROOF STATE]
proof (prove)
using this:
is_sum4sq_nat m
is_sum4sq_nat p
prime p \<and> n = p * m
\<lbrakk>is_sum4sq_nat ?x; is_sum4sq_nat ?y\<rbrakk> \<Longrightarrow> is_sum4sq_nat (?x * ?y)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_sum4sq_nat n

goal:
No subgoals!
[PROOF STEP]
qed


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

  shows "\<Psi> \<rhd> P \<parallel> Q \<doteq> Q \<parallel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<doteq> Q \<parallel> P
[PROOF STEP]
by(metis bisimParComm strongBisimWeakPsiCong)


[STATEMENT]
lemma weakPsiCongResComm:
  fixes x :: name
  and   \<Psi> :: 'b
  and   y :: name
  and   P :: "('a, 'b, 'c) psi"

  assumes "x \<sharp> \<Psi>"
  and     "y \<sharp> \<Psi>"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>P) \<doteq> \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>P) \<doteq> \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>
y \<sharp> \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>P) \<doteq> \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>P)
[PROOF STEP]
by(metis bisimResComm strongBisimWeakPsiCong)


[STATEMENT]
lemma weakPsiCongResComm':
  fixes x    :: name
  and   \<Psi>   :: 'b
  and   xvec :: "name list"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "x \<sharp> \<Psi>"
  and     "xvec \<sharp>* \<Psi>"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>P) \<doteq> \<lparr>\<nu>*xvec\<rparr>(\<lparr>\<nu>x\<rparr>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>P) \<doteq> \<lparr>\<nu>*xvec\<rparr>\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>
xvec \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>P) \<doteq> \<lparr>\<nu>*xvec\<rparr>\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
by(metis bisimResComm' strongBisimWeakPsiCong)


[STATEMENT]
lemma weakPsiCongScopeExt:
  fixes x :: name
  and   \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "x \<sharp> \<Psi>"
  and     "x \<sharp> P"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<doteq> P \<parallel> \<lparr>\<nu>x\<rparr>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<doteq> P \<parallel> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>
x \<sharp> P

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<doteq> P \<parallel> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
by(metis bisimScopeExt strongBisimWeakPsiCong)


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

  assumes "xvec \<sharp>* \<Psi>"
  and     "xvec \<sharp>* P"

  shows "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>(P \<parallel> Q) \<doteq> P \<parallel> (\<lparr>\<nu>*xvec\<rparr>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<doteq> P \<parallel> (\<lparr>\<nu>*xvec\<rparr>Q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi>
xvec \<sharp>* P

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<doteq> P \<parallel> (\<lparr>\<nu>*xvec\<rparr>Q)
[PROOF STEP]
by(metis bisimScopeExtChain strongBisimWeakPsiCong)


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

  shows "\<Psi> \<rhd> (P \<parallel> Q) \<parallel> R \<doteq> P \<parallel> (Q \<parallel> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<parallel> R \<doteq> P \<parallel> (Q \<parallel> R)
[PROOF STEP]
by(metis bisimParAssoc strongBisimWeakPsiCong)


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

  shows "\<Psi> \<rhd> P \<parallel> \<zero> \<doteq> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> \<zero> \<doteq> P
[PROOF STEP]
by(metis bisimParNil strongBisimWeakPsiCong)


[STATEMENT]
lemma weakPsiCongResNil:
  fixes x :: name
  and   \<Psi> :: 'b

  assumes "x \<sharp> \<Psi>"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero> \<doteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero> \<doteq> \<zero>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>\<zero> \<doteq> \<zero>
[PROOF STEP]
by(metis bisimResNil strongBisimWeakPsiCong)


[STATEMENT]
lemma weakPsiCongOutputPushRes:
  fixes x :: name
  and   \<Psi> :: 'b
  and   M :: 'a
  and   N :: 'a
  and   P :: "('a, 'b, 'c) psi"

  assumes "x \<sharp> \<Psi>"
  and     "x \<sharp> M"
  and     "x \<sharp> N"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(M\<langle>N\<rangle>.P) \<doteq> M\<langle>N\<rangle>.\<lparr>\<nu>x\<rparr>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(M\<langle>N\<rangle>.P) \<doteq> M\<langle>N\<rangle>.\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>
x \<sharp> M
x \<sharp> N

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(M\<langle>N\<rangle>.P) \<doteq> M\<langle>N\<rangle>.\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
by(metis bisimOutputPushRes strongBisimWeakPsiCong)


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

  assumes "x \<sharp> \<Psi>"
  and     "x \<sharp> M"
  and     "x \<sharp> xvec"
  and     "x \<sharp> N"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(M\<lparr>\<lambda>*xvec N\<rparr>.P) \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.\<lparr>\<nu>x\<rparr>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(M\<lparr>\<lambda>*xvec N\<rparr>.P) \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>
x \<sharp> M
x \<sharp> xvec
x \<sharp> N

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(M\<lparr>\<lambda>*xvec N\<rparr>.P) \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
by(metis bisimInputPushRes strongBisimWeakPsiCong)


[STATEMENT]
lemma weakPsiCongCasePushRes:
  fixes x  :: name
  and   \<Psi>  :: 'b
  and   Cs :: "('c \<times> ('a, 'b, 'c) psi) list"

  assumes "x \<sharp> \<Psi>"
  and     "x \<sharp> (map fst Cs)"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(Cases Cs) \<doteq> Cases(map (\<lambda>(\<phi>, P). (\<phi>, \<lparr>\<nu>x\<rparr>P)) Cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(Cases Cs) \<doteq> Cases map (\<lambda>(\<phi>, P). (\<phi>, \<lparr>\<nu>x\<rparr>P)) Cs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>
x \<sharp> map fst Cs

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(Cases Cs) \<doteq> Cases map (\<lambda>(\<phi>, P). (\<phi>, \<lparr>\<nu>x\<rparr>P)) Cs
[PROOF STEP]
by(metis bisimCasePushRes strongBisimWeakPsiCong)


[STATEMENT]
lemma weakBangExt:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"

  assumes "guarded P"

  shows "\<Psi> \<rhd> !P \<doteq> P \<parallel> !P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<doteq> P \<parallel> !P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
guarded P

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<doteq> P \<parallel> !P
[PROOF STEP]
by(metis bangExt strongBisimWeakPsiCong)


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

  assumes "\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q"

  shows "\<Psi> \<rhd> R \<parallel> P \<doteq> R \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> R \<parallel> P \<doteq> R \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> R \<parallel> P \<doteq> R \<parallel> Q
[PROOF STEP]
by(metis weakPsiCongParComm weakPsiCongParPres weakPsiCongTransitive)


[STATEMENT]
lemma weakPsiCongScopeExtSym:
  fixes x :: name
  and   Q :: "('a, 'b, 'c) psi"
  and   P :: "('a, 'b, 'c) psi"

  assumes "x \<sharp> \<Psi>"
  and     "x \<sharp> Q"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<doteq> (\<lparr>\<nu>x\<rparr>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<doteq> \<lparr>\<nu>x\<rparr>P \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<Psi>
x \<sharp> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<doteq> \<lparr>\<nu>x\<rparr>P \<parallel> Q
[PROOF STEP]
by(metis weakPsiCongScopeExt weakPsiCongTransitive weakPsiCongParComm weakPsiCongE weakPsiCongResPres)


[STATEMENT]
lemma weakPsiCongScopeExtChainSym:
  fixes xvec :: "name list"
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "xvec \<sharp>* \<Psi>"
  and     "xvec \<sharp>* Q"

  shows "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>(P \<parallel> Q) \<doteq> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<doteq> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi>
xvec \<sharp>* Q

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<doteq> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q
[PROOF STEP]
by(induct xvec) (auto intro: weakPsiCongScopeExtSym weakPsiCongReflexive weakPsiCongTransitive weakPsiCongResPres)


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

  assumes "\<And>\<Psi>. \<Psi> \<rhd> P \<doteq> Q"

  shows "\<Psi> \<rhd> R \<parallel> P \<doteq> R \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> R \<parallel> P \<doteq> R \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?\<Psi> \<rhd> P \<doteq> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> R \<parallel> P \<doteq> R \<parallel> Q
[PROOF STEP]
by(metis weakPsiCongParComm weakPsiCongParPres weakPsiCongTransitive)


[STATEMENT]
lemma tauCongChainBangI:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "guarded P"

  obtains Q where "\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q" and "\<Psi> \<rhd> Q \<sim> P' \<parallel> !P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q; \<Psi> \<rhd> Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q; \<Psi> \<rhd> Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume "\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q; \<Psi> \<rhd> Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> ?Q; \<Psi> \<rhd> ?Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q; \<Psi> \<rhd> Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> ?Q; \<Psi> \<rhd> ?Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q; \<Psi> \<rhd> Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> P'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
have "\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> P' \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> P' \<parallel> !P
[PROOF STEP]
proof(induct x1=="P \<parallel> P" P' rule: tauStepChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. \<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> b \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P
 2. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
case(TauBase R')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> R'

goal (2 subgoals):
 1. \<And>b. \<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> b \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P
 2. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<parallel> P \<longmapsto>\<tau> \<prec> R'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> R'
[PROOF STEP]
obtain Q where "\<Psi> \<rhd> !P \<longmapsto>\<tau> \<prec> Q" and "Q \<sim> R' \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> R'

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<longmapsto> \<tau> \<prec> Q; Q \<sim> R' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>guarded P\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> R'
guarded P

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<longmapsto> \<tau> \<prec> Q; Q \<sim> R' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule tauBangI)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<longmapsto> \<tau> \<prec> Q
Q \<sim> R' \<parallel> !P

goal (2 subgoals):
 1. \<And>b. \<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> b \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P
 2. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
from \<open>\<Psi> \<rhd> !P \<longmapsto>\<tau> \<prec> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> !P \<longmapsto> \<tau> \<prec> Q
[PROOF STEP]
have "\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> !P \<longmapsto> \<tau> \<prec> Q

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

goal (2 subgoals):
 1. \<And>b. \<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> b \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P
 2. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q

goal (2 subgoals):
 1. \<And>b. \<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> b \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P
 2. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
from \<open>Q \<sim> R' \<parallel> !P\<close>
[PROOF STATE]
proof (chain)
picking this:
Q \<sim> R' \<parallel> !P
[PROOF STEP]
have "\<Psi> \<rhd> Q \<sim> R' \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
Q \<sim> R' \<parallel> !P

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<sim> R' \<parallel> !P
[PROOF STEP]
apply(drule_tac bisimE(3)[where \<Psi>'=\<Psi>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one> \<otimes> \<Psi> \<rhd> Q \<sim> R' \<parallel> !P \<Longrightarrow> \<Psi> \<rhd> Q \<sim> R' \<parallel> !P
[PROOF STEP]
by(rule_tac statEqBisim, assumption) (metis Identity AssertionStatEqSym AssertionStatEqTrans Commutativity)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<sim> R' \<parallel> !P

goal (2 subgoals):
 1. \<And>b. \<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> b \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P
 2. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q
\<Psi> \<rhd> Q \<sim> R' \<parallel> !P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q
\<Psi> \<rhd> Q \<sim> R' \<parallel> !P

goal (1 subgoal):
 1. \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> R' \<parallel> !P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> R' \<parallel> !P

goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
case(TauStep R' R'')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> R'
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> R' \<parallel> !P
\<Psi> \<rhd> R' \<longmapsto> \<tau> \<prec> R''

goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> R'
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> R' \<parallel> !P
\<Psi> \<rhd> R' \<longmapsto> \<tau> \<prec> R''
[PROOF STEP]
obtain Q where PChain: "\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q" and "\<Psi> \<rhd> Q \<sim> R' \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> R'
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> R' \<parallel> !P
\<Psi> \<rhd> R' \<longmapsto> \<tau> \<prec> R''

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q; \<Psi> \<rhd> Q \<sim> R' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q
\<Psi> \<rhd> Q \<sim> R' \<parallel> !P

goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
from \<open>\<Psi> \<rhd> R' \<longmapsto>\<tau> \<prec> R''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> R' \<longmapsto> \<tau> \<prec> R''
[PROOF STEP]
have "\<Psi> \<otimes> \<one> \<rhd> R' \<longmapsto>\<tau> \<prec> R''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> R' \<longmapsto> \<tau> \<prec> R''

goal (1 subgoal):
 1. \<Psi> \<otimes> \<one> \<rhd> R' \<longmapsto> \<tau> \<prec> R''
[PROOF STEP]
by(rule statEqTransition) (metis Identity AssertionStatEqSym)
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<one> \<rhd> R' \<longmapsto> \<tau> \<prec> R''

goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
hence "\<Psi> \<rhd> R' \<parallel> !P \<longmapsto>\<tau> \<prec> R'' \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<one> \<rhd> R' \<longmapsto> \<tau> \<prec> R''

goal (1 subgoal):
 1. \<Psi> \<rhd> R' \<parallel> !P \<longmapsto> \<tau> \<prec> R'' \<parallel> !P
[PROOF STEP]
by(rule_tac Par1) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> R' \<parallel> !P \<longmapsto> \<tau> \<prec> R'' \<parallel> !P

goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
with \<open>\<Psi> \<rhd> Q \<sim> R' \<parallel> !P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<sim> R' \<parallel> !P
\<Psi> \<rhd> R' \<parallel> !P \<longmapsto> \<tau> \<prec> R'' \<parallel> !P
[PROOF STEP]
obtain Q' where QTrans: "\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'" and "\<Psi> \<rhd> Q' \<sim> R'' \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<sim> R' \<parallel> !P
\<Psi> \<rhd> R' \<parallel> !P \<longmapsto> \<tau> \<prec> R'' \<parallel> !P

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; \<Psi> \<rhd> Q' \<sim> R'' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force dest: bisimE(2) simE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
\<Psi> \<rhd> Q' \<sim> R'' \<parallel> !P

goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
from PChain QTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
have "\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

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

goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> b; \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> b \<parallel> !P; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> c \<parallel> !P
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q'

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

goal (1 subgoal):
 1. \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> R'' \<parallel> !P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> R'' \<parallel> !P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> P' \<parallel> !P

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q; \<Psi> \<rhd> Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> ?Q; \<Psi> \<rhd> ?Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> P' \<parallel> !P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> ?Q; \<Psi> \<rhd> ?Q \<sim> P' \<parallel> !P\<rbrakk> \<Longrightarrow> thesis
\<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> P' \<parallel> !P

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

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes PeqQ: "\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q"
  and     "guarded P"
  and     "guarded Q"

  shows   "\<Psi> \<rhd> !P \<doteq> !Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<doteq> !Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<doteq> !Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q
guarded P
guarded Q
[PROOF STEP]
have "(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q
guarded P
guarded Q

goal (1 subgoal):
 1. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<doteq> !Q
[PROOF STEP]
hence "\<Psi> \<rhd> \<zero> \<parallel> !P \<doteq> \<zero> \<parallel> !Q"
[PROOF STATE]
proof (prove)
using this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (1 subgoal):
 1. \<Psi> \<rhd> \<zero> \<parallel> !P \<doteq> \<zero> \<parallel> !Q
[PROOF STEP]
proof(induct rule: weakPsiCongSymI[where C="\<lambda>P. \<zero> \<parallel> !P"])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> (\<forall>\<Psi>. \<Psi> \<rhd> Q \<doteq> P) \<and> guarded Q \<and> guarded P
 2. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<approx> \<zero> \<parallel> !Q
 3. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
case(cSym P Q)
[PROOF STATE]
proof (state)
this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (3 subgoals):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> (\<forall>\<Psi>. \<Psi> \<rhd> Q \<doteq> P) \<and> guarded Q \<and> guarded P
 2. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<approx> \<zero> \<parallel> !Q
 3. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (1 subgoal):
 1. (\<forall>\<Psi>. \<Psi> \<rhd> Q \<doteq> P) \<and> guarded Q \<and> guarded P
[PROOF STEP]
by(auto dest: weakPsiCongSym)
[PROOF STATE]
proof (state)
this:
(\<forall>\<Psi>. \<Psi> \<rhd> Q \<doteq> P) \<and> guarded Q \<and> guarded P

goal (2 subgoals):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<approx> \<zero> \<parallel> !Q
 2. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<approx> \<zero> \<parallel> !Q
 2. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
case(cWeakBisim P Q)
[PROOF STATE]
proof (state)
this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (2 subgoals):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<approx> \<zero> \<parallel> !Q
 2. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (1 subgoal):
 1. \<Psi> \<rhd> \<zero> \<parallel> !P \<approx> \<zero> \<parallel> !Q
[PROOF STEP]
by(metis weakPsiCongE weakBisimBangPresAux)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<zero> \<parallel> !P \<approx> \<zero> \<parallel> !Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
case(cSim P Q)
[PROOF STATE]
proof (state)
this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q
[PROOF STEP]
have "\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q" and "guarded P" and "guarded Q"
[PROOF STATE]
proof (prove)
using this:
(\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q

goal (1 subgoal):
 1. \<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q &&& guarded P &&& guarded Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q
guarded P
guarded Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q
guarded P
guarded Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
hence "\<Psi> \<rhd> P \<approx> Q"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q
guarded P
guarded Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<approx> Q
[PROOF STEP]
by(metis weakPsiCongE weakBisimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<approx> Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<approx> Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
have "\<And>\<Psi> P Q. (\<forall>\<Psi>. (\<Psi> \<rhd> P \<doteq> Q)) \<Longrightarrow> \<Psi> \<rhd> P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<Psi> P Q. \<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q \<Longrightarrow> \<Psi> \<rhd> P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> Q
[PROOF STEP]
by(blast dest: weakPsiCongE)
[PROOF STATE]
proof (state)
this:
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
note weakBisimClosed bisimClosed weakBisimE(3) bisimE(3) weakBisimE(2)
                  weakBisimE(4) bisimE(4) statEqWeakBisim statEqBisim weakBisimTransitive bisimTransitive weakBisimParAssoc[THEN weakBisimE(4)]
                  bisimParAssoc[THEN bisimE(4)] weakBisimParPres
[PROOF STATE]
proof (state)
this:
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<approx> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<sim> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<approx> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<sim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto><weakBisim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<approx> ?P
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<sim> ?P
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<approx> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<sim> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<rhd> ?Q \<approx> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?R
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<rhd> ?Q \<sim> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<sim> ?R
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<approx> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<sim> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<parallel> ?R \<approx> ?Q \<parallel> ?R

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<approx> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<sim> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<approx> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<sim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto><weakBisim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<approx> ?P
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<sim> ?P
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<approx> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<sim> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<rhd> ?Q \<approx> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?R
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<rhd> ?Q \<sim> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<sim> ?R
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<approx> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<sim> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<parallel> ?R \<approx> ?Q \<parallel> ?R

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
have "\<And>P Q. \<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q \<Longrightarrow> \<forall>\<Psi>. \<Psi> \<rhd> P \<parallel> P \<doteq> Q \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q. \<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q \<Longrightarrow> \<forall>\<Psi>. \<Psi> \<rhd> P \<parallel> P \<doteq> Q \<parallel> Q
[PROOF STEP]
by(metis weakPsiCongParPres weakPsiCongParComm weakPsiCongSym weakPsiCongTransitive)
[PROOF STATE]
proof (state)
this:
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> \<forall>\<Psi>. \<Psi> \<rhd> ?P \<parallel> ?P \<doteq> ?Q \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> \<forall>\<Psi>. \<Psi> \<rhd> ?P \<parallel> ?P \<doteq> ?Q \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
note bisimParPresSym
[PROOF STATE]
proof (state)
this:
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<sim> ?R \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<sim> ?R \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
from strongBisimWeakBisim
[PROOF STATE]
proof (chain)
picking this:
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?Q
[PROOF STEP]
have "bisim \<subseteq> weakBisim"
[PROOF STATE]
proof (prove)
using this:
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?Q

goal (1 subgoal):
 1. bisim \<subseteq> weakBisim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bisim \<subseteq> weakBisim

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim \<subseteq> weakBisim

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
have "\<And>\<Psi> \<Psi>\<^sub>R P Q R A\<^sub>R. \<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> P \<approx> Q; extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>; A\<^sub>R \<sharp>* \<Psi>; A\<^sub>R \<sharp>* P; A\<^sub>R \<sharp>* Q\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> R \<parallel> P \<approx> R \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<Psi> \<Psi>\<^sub>R P Q R A\<^sub>R. \<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> P \<approx> Q; extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>; A\<^sub>R \<sharp>* \<Psi>; A\<^sub>R \<sharp>* P; A\<^sub>R \<sharp>* Q\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> R \<parallel> P \<approx> R \<parallel> Q
[PROOF STEP]
by(metis weakBisimParComm weakBisimTransitive weakBisimParPresAux)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<otimes> ?\<Psi>\<^sub>R \<rhd> ?P \<approx> ?Q; extractFrame ?R = \<langle>?A\<^sub>R, ?\<Psi>\<^sub>R\<rangle>; ?A\<^sub>R \<sharp>* ?\<Psi>; ?A\<^sub>R \<sharp>* ?P; ?A\<^sub>R \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<approx> ?R \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<otimes> ?\<Psi>\<^sub>R \<rhd> ?P \<approx> ?Q; extractFrame ?R = \<langle>?A\<^sub>R, ?\<Psi>\<^sub>R\<rangle>; ?A\<^sub>R \<sharp>* ?\<Psi>; ?A\<^sub>R \<sharp>* ?P; ?A\<^sub>R \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<approx> ?R \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
note weakBisimResChainPres bisimResChainPres weakBisimScopeExtChainSym bisimScopeExtChainSym
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<approx> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<sim> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<approx> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<sim> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<approx> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<sim> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<approx> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<sim> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
have "\<And>\<Psi> P R S Q. \<lbrakk>\<Psi> \<rhd> P \<approx> R; \<Psi> \<rhd> R \<approx> S; \<Psi> \<rhd> S \<sim> Q\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> P \<approx> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<Psi> P R S Q. \<lbrakk>\<Psi> \<rhd> P \<approx> R; \<Psi> \<rhd> R \<approx> S; \<Psi> \<rhd> S \<sim> Q\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> P \<approx> Q
[PROOF STEP]
by(blast dest: weakBisimTransitive strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?R; ?\<Psi> \<rhd> ?R \<approx> ?S; ?\<Psi> \<rhd> ?S \<sim> ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?R; ?\<Psi> \<rhd> ?R \<approx> ?S; ?\<Psi> \<rhd> ?S \<sim> ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
note weakBisimBangPresAux
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; guarded ?P; guarded ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> !?P \<approx> ?R \<parallel> !?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; guarded ?P; guarded ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> !?P \<approx> ?R \<parallel> !?Q

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
from bangActE
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> ?\<alpha> \<prec> ?P'; bn ?\<alpha> \<sharp>* subject ?\<alpha>; guarded ?P; ?\<alpha> \<noteq> \<tau>; bn ?\<alpha> \<sharp>* ?P; \<And>Q. \<lbrakk>?\<Psi> \<rhd> ?P \<longmapsto> ?\<alpha> \<prec> Q; ?P' \<sim> Q \<parallel> !?P\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "\<And>\<Psi> P \<alpha> P'. \<lbrakk>\<Psi> \<rhd> !P \<longmapsto>\<alpha> \<prec> P'; bn \<alpha> \<sharp>* P; guarded P; \<alpha> \<noteq> \<tau>; bn \<alpha> \<sharp>* subject \<alpha>\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> Q \<and> P' \<sim> Q \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> ?\<alpha> \<prec> ?P'; bn ?\<alpha> \<sharp>* subject ?\<alpha>; guarded ?P; ?\<alpha> \<noteq> \<tau>; bn ?\<alpha> \<sharp>* ?P; \<And>Q. \<lbrakk>?\<Psi> \<rhd> ?P \<longmapsto> ?\<alpha> \<prec> Q; ?P' \<sim> Q \<parallel> !?P\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>\<Psi> P \<alpha> P'. \<lbrakk>\<Psi> \<rhd> !P \<longmapsto> \<alpha> \<prec> P'; bn \<alpha> \<sharp>* P; guarded P; \<alpha> \<noteq> \<tau>; bn \<alpha> \<sharp>* subject \<alpha>\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q \<and> P' \<sim> Q \<parallel> !P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> ?\<alpha> \<prec> ?P'; bn ?\<alpha> \<sharp>* ?P; guarded ?P; ?\<alpha> \<noteq> \<tau>; bn ?\<alpha> \<sharp>* subject ?\<alpha>\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<longmapsto> ?\<alpha> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> ?\<alpha> \<prec> ?P'; bn ?\<alpha> \<sharp>* ?P; guarded ?P; ?\<alpha> \<noteq> \<tau>; bn ?\<alpha> \<sharp>* subject ?\<alpha>\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<longmapsto> ?\<alpha> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
from bangTauE
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> \<tau> \<prec> ?P'; guarded ?P; \<And>Q. \<lbrakk>?\<Psi> \<rhd> ?P \<parallel> ?P \<longmapsto> \<tau> \<prec> Q; ?P' \<sim> Q \<parallel> !?P\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "\<And>\<Psi> P P'. \<lbrakk>\<Psi> \<rhd> !P \<longmapsto>\<tau> \<prec> P'; guarded P\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> P \<parallel> P \<longmapsto>\<tau> \<prec> Q \<and> P' \<sim> Q \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> \<tau> \<prec> ?P'; guarded ?P; \<And>Q. \<lbrakk>?\<Psi> \<rhd> ?P \<parallel> ?P \<longmapsto> \<tau> \<prec> Q; ?P' \<sim> Q \<parallel> !?P\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>\<Psi> P P'. \<lbrakk>\<Psi> \<rhd> !P \<longmapsto> \<tau> \<prec> P'; guarded P\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> P \<parallel> P \<longmapsto> \<tau> \<prec> Q \<and> P' \<sim> Q \<parallel> !P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> \<tau> \<prec> ?P'; guarded ?P\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<parallel> ?P \<longmapsto> \<tau> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> \<tau> \<prec> ?P'; guarded ?P\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<parallel> ?P \<longmapsto> \<tau> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
from tauCongChainBangI
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<Psi> \<rhd> ?P \<parallel> ?P \<Longrightarrow>\<^sub>\<tau> ?P'; guarded ?P; \<And>Q. \<lbrakk>?\<Psi> \<rhd> !?P \<Longrightarrow>\<^sub>\<tau> Q; ?\<Psi> \<rhd> Q \<sim> ?P' \<parallel> !?P\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "\<And>\<Psi> P P'. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> P'; guarded P\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> P' \<parallel> !P"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Psi> \<rhd> ?P \<parallel> ?P \<Longrightarrow>\<^sub>\<tau> ?P'; guarded ?P; \<And>Q. \<lbrakk>?\<Psi> \<rhd> !?P \<Longrightarrow>\<^sub>\<tau> Q; ?\<Psi> \<rhd> Q \<sim> ?P' \<parallel> !?P\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>\<Psi> P P'. \<lbrakk>\<Psi> \<rhd> P \<parallel> P \<Longrightarrow>\<^sub>\<tau> P'; guarded P\<rbrakk> \<Longrightarrow> \<exists>Q. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> Q \<and> \<Psi> \<rhd> Q \<sim> P' \<parallel> !P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<Psi> \<rhd> ?P \<parallel> ?P \<Longrightarrow>\<^sub>\<tau> ?P'; guarded ?P\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> !?P \<Longrightarrow>\<^sub>\<tau> Q \<and> ?\<Psi> \<rhd> Q \<sim> ?P' \<parallel> !?P

goal (1 subgoal):
 1. \<And>P Q. (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q) \<and> guarded P \<and> guarded Q \<Longrightarrow> \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q
guarded P
guarded Q
\<Psi> \<rhd> P \<approx> Q
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<approx> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<sim> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<approx> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<sim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto><weakBisim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<approx> ?P
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<sim> ?P
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<approx> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<sim> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<rhd> ?Q \<approx> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?R
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<rhd> ?Q \<sim> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<sim> ?R
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<approx> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<sim> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<parallel> ?R \<approx> ?Q \<parallel> ?R
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> \<forall>\<Psi>. \<Psi> \<rhd> ?P \<parallel> ?P \<doteq> ?Q \<parallel> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<sim> ?R \<parallel> ?Q
bisim \<subseteq> weakBisim
\<lbrakk>?\<Psi> \<otimes> ?\<Psi>\<^sub>R \<rhd> ?P \<approx> ?Q; extractFrame ?R = \<langle>?A\<^sub>R, ?\<Psi>\<^sub>R\<rangle>; ?A\<^sub>R \<sharp>* ?\<Psi>; ?A\<^sub>R \<sharp>* ?P; ?A\<^sub>R \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<approx> ?R \<parallel> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<approx> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<sim> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<approx> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<sim> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?R; ?\<Psi> \<rhd> ?R \<approx> ?S; ?\<Psi> \<rhd> ?S \<sim> ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; guarded ?P; guarded ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> !?P \<approx> ?R \<parallel> !?Q
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> ?\<alpha> \<prec> ?P'; bn ?\<alpha> \<sharp>* ?P; guarded ?P; ?\<alpha> \<noteq> \<tau>; bn ?\<alpha> \<sharp>* subject ?\<alpha>\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<longmapsto> ?\<alpha> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> \<tau> \<prec> ?P'; guarded ?P\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<parallel> ?P \<longmapsto> \<tau> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P
\<lbrakk>?\<Psi> \<rhd> ?P \<parallel> ?P \<Longrightarrow>\<^sub>\<tau> ?P'; guarded ?P\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> !?P \<Longrightarrow>\<^sub>\<tau> Q \<and> ?\<Psi> \<rhd> Q \<sim> ?P' \<parallel> !?P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q
guarded P
guarded Q
\<Psi> \<rhd> P \<approx> Q
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<approx> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?p \<bullet> ?\<Psi> \<rhd> ?p \<bullet> ?P \<sim> ?p \<bullet> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<approx> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<otimes> ?\<Psi>' \<rhd> ?P \<sim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<leadsto><weakBisim> ?Q
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<approx> ?P
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?Q \<sim> ?P
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<approx> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<simeq> ?\<Psi>'\<rbrakk> \<Longrightarrow> ?\<Psi>' \<rhd> ?P \<sim> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?\<Psi> \<rhd> ?Q \<approx> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?R
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?\<Psi> \<rhd> ?Q \<sim> ?R\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<sim> ?R
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<approx> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P1 \<parallel> (?Q1 \<parallel> ?R1) \<sim> ?P1 \<parallel> ?Q1 \<parallel> ?R1
?\<Psi> \<rhd> ?P \<approx> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?P \<parallel> ?R \<approx> ?Q \<parallel> ?R
\<forall>\<Psi>. \<Psi> \<rhd> ?P \<doteq> ?Q \<Longrightarrow> \<forall>\<Psi>. \<Psi> \<rhd> ?P \<parallel> ?P \<doteq> ?Q \<parallel> ?Q
?\<Psi> \<rhd> ?P \<sim> ?Q \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<sim> ?R \<parallel> ?Q
bisim \<subseteq> weakBisim
\<lbrakk>?\<Psi> \<otimes> ?\<Psi>\<^sub>R \<rhd> ?P \<approx> ?Q; extractFrame ?R = \<langle>?A\<^sub>R, ?\<Psi>\<^sub>R\<rangle>; ?A\<^sub>R \<sharp>* ?\<Psi>; ?A\<^sub>R \<sharp>* ?P; ?A\<^sub>R \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> ?P \<approx> ?R \<parallel> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<approx> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<sim> ?Q; ?xvec \<sharp>* ?\<Psi>\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<sim> \<lparr>\<nu>*?xvec\<rparr>?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<approx> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> \<lparr>\<nu>*?xvec\<rparr>?P \<parallel> ?Q \<sim> (\<lparr>\<nu>*?xvec\<rparr>?P) \<parallel> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?R; ?\<Psi> \<rhd> ?R \<approx> ?S; ?\<Psi> \<rhd> ?S \<sim> ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?P \<approx> ?Q
\<lbrakk>?\<Psi> \<rhd> ?P \<approx> ?Q; guarded ?P; guarded ?Q\<rbrakk> \<Longrightarrow> ?\<Psi> \<rhd> ?R \<parallel> !?P \<approx> ?R \<parallel> !?Q
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> ?\<alpha> \<prec> ?P'; bn ?\<alpha> \<sharp>* ?P; guarded ?P; ?\<alpha> \<noteq> \<tau>; bn ?\<alpha> \<sharp>* subject ?\<alpha>\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<longmapsto> ?\<alpha> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P
\<lbrakk>?\<Psi> \<rhd> !?P \<longmapsto> \<tau> \<prec> ?P'; guarded ?P\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> ?P \<parallel> ?P \<longmapsto> \<tau> \<prec> Q \<and> ?P' \<sim> Q \<parallel> !?P
\<lbrakk>?\<Psi> \<rhd> ?P \<parallel> ?P \<Longrightarrow>\<^sub>\<tau> ?P'; guarded ?P\<rbrakk> \<Longrightarrow> \<exists>Q. ?\<Psi> \<rhd> !?P \<Longrightarrow>\<^sub>\<tau> Q \<and> ?\<Psi> \<rhd> Q \<sim> ?P' \<parallel> !?P

goal (1 subgoal):
 1. \<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q
[PROOF STEP]
by(rule_tac weakCongSimBangPres[where Rel=weakBisim and Rel'=bisim and Rel''=weakBisim and Eq="\<lambda>P Q. \<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q"])
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<zero> \<parallel> !P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<zero> \<parallel> !Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<zero> \<parallel> !P \<doteq> \<zero> \<parallel> !Q

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<doteq> !Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> \<zero> \<parallel> !P \<doteq> \<zero> \<parallel> !Q

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<doteq> !Q
[PROOF STEP]
by(metis weakPsiCongParNil weakPsiCongParComm weakPsiCongTransitive weakPsiCongSym)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> !P \<doteq> !Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma class_wf:
  "\<lbrakk>class P C = Some c; wf_prog wf_md P\<rbrakk> \<Longrightarrow> wf_cdecl wf_md P (C,c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class P C = \<lfloor>c\<rfloor>; wf_prog wf_md P\<rbrakk> \<Longrightarrow> wf_cdecl wf_md P (C, c)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class P C = \<lfloor>c\<rfloor>; wf_prog wf_md P\<rbrakk> \<Longrightarrow> wf_cdecl wf_md P (C, c)
[PROOF STEP]
by (unfold wf_prog_def class_def) (fast dest: map_of_SomeD)


[STATEMENT]
lemma class_Object [simp]:
  "wf_prog wf_md P \<Longrightarrow> \<exists>C fs ms. class P Object = Some (C,fs,ms)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> \<exists>C fs ms. class P Object = \<lfloor>(C, fs, ms)\<rfloor>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> \<exists>C fs ms. class P Object = \<lfloor>(C, fs, ms)\<rfloor>
[PROOF STEP]
by (unfold wf_prog_def wf_syscls_def class_def)
        (auto simp: map_of_SomeI)


[STATEMENT]
lemma is_class_Object [simp]:
  "wf_prog wf_md P \<Longrightarrow> is_class P Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> is_class P Object
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> is_class P Object
[PROOF STEP]
by (simp add: is_class_def)


[STATEMENT]
lemma is_class_supclass:
assumes wf: "wf_prog wf_md P" and sub: "P \<turnstile> C \<preceq>\<^sup>* D"
shows "is_class P C \<Longrightarrow> is_class P D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> is_class P D
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> is_class P D
[PROOF STEP]
using sub
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C \<preceq>\<^sup>* D

goal (1 subgoal):
 1. is_class P C \<Longrightarrow> is_class P D
[PROOF STEP]
proof(induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_class P C \<Longrightarrow> is_class P C
 2. \<And>y z. \<lbrakk>P \<turnstile> C \<preceq>\<^sup>* y; P \<turnstile> y \<prec>\<^sup>1 z; is_class P C \<Longrightarrow> is_class P y; is_class P C\<rbrakk> \<Longrightarrow> is_class P z
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
P \<turnstile> C \<preceq>\<^sup>* y_
P \<turnstile> y_ \<prec>\<^sup>1 z_
is_class P C \<Longrightarrow> is_class P y_
is_class P C

goal (2 subgoals):
 1. is_class P C \<Longrightarrow> is_class P C
 2. \<And>y z. \<lbrakk>P \<turnstile> C \<preceq>\<^sup>* y; P \<turnstile> y \<prec>\<^sup>1 z; is_class P C \<Longrightarrow> is_class P y; is_class P C\<rbrakk> \<Longrightarrow> is_class P z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C \<preceq>\<^sup>* y_
P \<turnstile> y_ \<prec>\<^sup>1 z_
is_class P C \<Longrightarrow> is_class P y_
is_class P C
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C \<preceq>\<^sup>* y_
P \<turnstile> y_ \<prec>\<^sup>1 z_
is_class P C \<Longrightarrow> is_class P y_
is_class P C

goal (1 subgoal):
 1. is_class P z_
[PROOF STEP]
by(auto simp:wf_cdecl_def is_class_def dest!:class_wf[OF _ wf] subcls1D)
[PROOF STATE]
proof (state)
this:
is_class P z_

goal (1 subgoal):
 1. is_class P C \<Longrightarrow> is_class P C
[PROOF STEP]
qed simp


[STATEMENT]
lemma is_class_xcpt:
  "\<lbrakk> C \<in> sys_xcpts; wf_prog wf_md P \<rbrakk> \<Longrightarrow> is_class P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<in> sys_xcpts; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_class P C
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<in> sys_xcpts; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_class P C
[PROOF STEP]
by (fastforce intro!: map_of_SomeI
              simp add: wf_prog_def wf_syscls_def is_class_def class_def)


[STATEMENT]
lemma subcls1_wfD:
assumes sub1: "P \<turnstile> C \<prec>\<^sup>1 D" and wf: "wf_prog wf_md P"
shows "D \<noteq> C \<and> (D,C) \<notin> (subcls1 P)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
obtain fs ms where "C \<noteq> Object" and cls: "class P C = \<lfloor>(D, fs, ms)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>fs ms. \<lbrakk>C \<noteq> Object; class P C = \<lfloor>(D, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subcls1D[OF sub1]
[PROOF STATE]
proof (prove)
using this:
C \<noteq> Object \<and> (\<exists>fs ms. class P C = \<lfloor>(D, fs, ms)\<rfloor>)

goal (1 subgoal):
 1. (\<And>fs ms. \<lbrakk>C \<noteq> Object; class P C = \<lfloor>(D, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarify
[PROOF STATE]
proof (state)
this:
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
using wf class_wf[OF cls wf] r_into_trancl[OF sub1]
[PROOF STATE]
proof (prove)
using this:
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>
wf_prog wf_md P
wf_cdecl wf_md P (C, D, fs, ms)
(C, D) \<in> (subcls1 P)\<^sup>+

goal (1 subgoal):
 1. D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
by(force simp add: wf_cdecl_def reflcl_trancl [THEN sym]
             simp del: reflcl_trancl)
[PROOF STATE]
proof (state)
this:
D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_cdecl_supD:
  "\<lbrakk>wf_cdecl wf_md P (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class P D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_cdecl wf_md P (C, D, r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class P D
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_cdecl wf_md P (C, D, r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class P D
[PROOF STEP]
by (auto simp: wf_cdecl_def)


[STATEMENT]
lemma subcls_asym:
  "\<lbrakk> wf_prog wf_md P; (C,D) \<in> (subcls1 P)\<^sup>+ \<rbrakk> \<Longrightarrow> (D,C) \<notin> (subcls1 P)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; (C, D) \<in> (subcls1 P)\<^sup>+\<rbrakk> \<Longrightarrow> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; (C, D) \<in> (subcls1 P)\<^sup>+\<rbrakk> \<Longrightarrow> (D, C) \<notin> (subcls1 P)\<^sup>+
[PROOF STEP]
by(erule tranclE; fast dest!: subcls1_wfD intro: trancl_trans)


[STATEMENT]
lemma subcls_irrefl:
  "\<lbrakk> wf_prog wf_md P; (C,D) \<in> (subcls1 P)\<^sup>+ \<rbrakk> \<Longrightarrow> C \<noteq> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; (C, D) \<in> (subcls1 P)\<^sup>+\<rbrakk> \<Longrightarrow> C \<noteq> D
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; (C, D) \<in> (subcls1 P)\<^sup>+\<rbrakk> \<Longrightarrow> C \<noteq> D
[PROOF STEP]
by (erule trancl_trans_induct) (auto dest: subcls1_wfD subcls_asym)


[STATEMENT]
lemma acyclic_subcls1:
  "wf_prog wf_md P \<Longrightarrow> acyclic (subcls1 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> acyclic (subcls1 P)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> acyclic (subcls1 P)
[PROOF STEP]
by (unfold acyclic_def) (fast dest: subcls_irrefl)


[STATEMENT]
lemma wf_subcls1:
  "wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
assume wf: "wf_prog wf_md P"
[PROOF STATE]
proof (state)
this:
wf_prog wf_md P

goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
have "finite (subcls1 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (subcls1 P)
[PROOF STEP]
by(rule finite_subcls1)
[PROOF STATE]
proof (state)
this:
finite (subcls1 P)

goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (subcls1 P)
[PROOF STEP]
have fin': "finite ((subcls1 P)\<inverse>)"
[PROOF STATE]
proof (prove)
using this:
finite (subcls1 P)

goal (1 subgoal):
 1. finite ((subcls1 P)\<inverse>)
[PROOF STEP]
by(subst finite_converse)
[PROOF STATE]
proof (state)
this:
finite ((subcls1 P)\<inverse>)

goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
[PROOF STEP]
have "acyclic (subcls1 P)"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P

goal (1 subgoal):
 1. acyclic (subcls1 P)
[PROOF STEP]
by(rule acyclic_subcls1)
[PROOF STATE]
proof (state)
this:
acyclic (subcls1 P)

goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
acyclic (subcls1 P)
[PROOF STEP]
have acyc': "acyclic ((subcls1 P)\<inverse>)"
[PROOF STATE]
proof (prove)
using this:
acyclic (subcls1 P)

goal (1 subgoal):
 1. acyclic ((subcls1 P)\<inverse>)
[PROOF STEP]
by (subst acyclic_converse)
[PROOF STATE]
proof (state)
this:
acyclic ((subcls1 P)\<inverse>)

goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)
[PROOF STEP]
from fin' acyc'
[PROOF STATE]
proof (chain)
picking this:
finite ((subcls1 P)\<inverse>)
acyclic ((subcls1 P)\<inverse>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite ((subcls1 P)\<inverse>)
acyclic ((subcls1 P)\<inverse>)

goal (1 subgoal):
 1. wf ((subcls1 P)\<inverse>)
[PROOF STEP]
by (rule finite_acyclic_wf)
[PROOF STATE]
proof (state)
this:
wf ((subcls1 P)\<inverse>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma single_valued_subcls1:
  "wf_prog wf_md G \<Longrightarrow> single_valued (subcls1 G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md G \<Longrightarrow> single_valued (subcls1 G)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md G \<Longrightarrow> single_valued (subcls1 G)
[PROOF STEP]
by(auto simp:wf_prog_def distinct_fst_def single_valued_def dest!:subcls1D)


[STATEMENT]
lemma subcls_induct:
  "\<lbrakk> wf_prog wf_md P; \<And>C. \<forall>D. (C,D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C \<rbrakk> \<Longrightarrow> Q C"
(*<*)
  (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
assume p: "PROP ?P"
[PROOF STATE]
proof (state)
this:
\<forall>D. (?C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q ?C

goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
assume ?A
[PROOF STATE]
proof (state)
this:
wf_prog wf_md P

goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
[PROOF STEP]
have wf: "wf_prog wf_md P"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P

goal (1 subgoal):
 1. wf_prog wf_md P
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
wf_prog wf_md P

goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
have wf':"wf (((subcls1 P)\<^sup>+)\<inverse>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (((subcls1 P)\<^sup>+)\<inverse>)
[PROOF STEP]
using wf_trancl[OF wf_subcls1[OF wf]]
[PROOF STATE]
proof (prove)
using this:
wf (((subcls1 P)\<inverse>)\<^sup>+)

goal (1 subgoal):
 1. wf (((subcls1 P)\<^sup>+)\<inverse>)
[PROOF STEP]
by(simp only: trancl_converse)
[PROOF STATE]
proof (state)
this:
wf (((subcls1 P)\<^sup>+)\<inverse>)

goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q C
[PROOF STEP]
using wf_induct[where a = C and P = Q, OF wf' p]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. \<forall>y. (y, x) \<in> ((subcls1 P)\<^sup>+)\<inverse> \<longrightarrow> Q y \<Longrightarrow> \<forall>D. (x, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D) \<Longrightarrow> Q C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subcls1_induct_aux:
assumes "is_class P C" and wf: "wf_prog wf_md P" and QObj: "Q Object"
shows
 "\<lbrakk> \<And>C D fs ms.
    \<lbrakk> C \<noteq> Object; is_class P C; class P C = Some (D,fs,ms) \<and>
      wf_cdecl wf_md P (C,D,fs,ms) \<and> P \<turnstile> C \<prec>\<^sup>1 D \<and> is_class P D \<and> Q D\<rbrakk> \<Longrightarrow> Q C \<rbrakk>
  \<Longrightarrow> Q C"
(*<*)
  (is "PROP ?P \<Longrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C D fs ms. \<lbrakk>C \<noteq> Object; is_class P C; class P C = \<lfloor>(D, fs, ms)\<rfloor> \<and> wf_cdecl wf_md P (C, D, fs, ms) \<and> P \<turnstile> C \<prec>\<^sup>1 D \<and> is_class P D \<and> Q D\<rbrakk> \<Longrightarrow> Q C) \<Longrightarrow> Q C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>C D fs ms. \<lbrakk>C \<noteq> Object; is_class P C; class P C = \<lfloor>(D, fs, ms)\<rfloor> \<and> wf_cdecl wf_md P (C, D, fs, ms) \<and> P \<turnstile> C \<prec>\<^sup>1 D \<and> is_class P D \<and> Q D\<rbrakk> \<Longrightarrow> Q C) \<Longrightarrow> Q C
[PROOF STEP]
assume p: "PROP ?P"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?C \<noteq> Object; is_class P ?C; class P ?C = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<and> wf_cdecl wf_md P (?C, ?D, ?fs, ?ms) \<and> P \<turnstile> ?C \<prec>\<^sup>1 ?D \<and> is_class P ?D \<and> Q ?D\<rbrakk> \<Longrightarrow> Q ?C

goal (1 subgoal):
 1. (\<And>C D fs ms. \<lbrakk>C \<noteq> Object; is_class P C; class P C = \<lfloor>(D, fs, ms)\<rfloor> \<and> wf_cdecl wf_md P (C, D, fs, ms) \<and> P \<turnstile> C \<prec>\<^sup>1 D \<and> is_class P D \<and> Q D\<rbrakk> \<Longrightarrow> Q C) \<Longrightarrow> Q C
[PROOF STEP]
have "class P C \<noteq> None \<longrightarrow> Q C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class P C \<noteq> None \<longrightarrow> Q C
[PROOF STEP]
proof(induct rule: subcls_induct[OF wf])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> class P D \<noteq> None \<longrightarrow> Q D \<Longrightarrow> class P C \<noteq> None \<longrightarrow> Q C
[PROOF STEP]
case (1 C)
[PROOF STATE]
proof (state)
this:
\<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> class P D \<noteq> None \<longrightarrow> Q D

goal (1 subgoal):
 1. \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> class P D \<noteq> None \<longrightarrow> Q D \<Longrightarrow> class P C \<noteq> None \<longrightarrow> Q C
[PROOF STEP]
have "class P C \<noteq> None \<Longrightarrow> Q C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class P C \<noteq> None \<Longrightarrow> Q C
[PROOF STEP]
proof(cases "C = Object")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>class P C \<noteq> None; C = Object\<rbrakk> \<Longrightarrow> Q C
 2. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C = Object

goal (2 subgoals):
 1. \<lbrakk>class P C \<noteq> None; C = Object\<rbrakk> \<Longrightarrow> Q C
 2. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C = Object
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C = Object

goal (1 subgoal):
 1. Q C
[PROOF STEP]
using QObj
[PROOF STATE]
proof (prove)
using this:
C = Object
Q Object

goal (1 subgoal):
 1. Q C
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Q C

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<noteq> Object

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
assume nNone: "class P C \<noteq> None"
[PROOF STATE]
proof (state)
this:
class P C \<noteq> None

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
class P C \<noteq> None
[PROOF STEP]
have is_cls: "is_class P C"
[PROOF STATE]
proof (prove)
using this:
class P C \<noteq> None

goal (1 subgoal):
 1. is_class P C
[PROOF STEP]
by(simp add: is_class_def)
[PROOF STATE]
proof (state)
this:
is_class P C

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
obtain D fs ms where cls: "class P C = \<lfloor>(D, fs, ms)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D fs ms. class P C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nNone
[PROOF STATE]
proof (prove)
using this:
class P C \<noteq> None

goal (1 subgoal):
 1. (\<And>D fs ms. class P C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by safe
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
have wfC: "wf_cdecl wf_md P (C, D, fs, ms)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl wf_md P (C, D, fs, ms)
[PROOF STEP]
by(rule class_wf[OF cls wf])
[PROOF STATE]
proof (state)
this:
wf_cdecl wf_md P (C, D, fs, ms)

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_cdecl wf_md P (C, D, fs, ms)

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
have D: "is_class P D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P D
[PROOF STEP]
by(rule wf_cdecl_supD[OF wfC False])
[PROOF STATE]
proof (state)
this:
is_class P D

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_class P D

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
have "P \<turnstile> C \<prec>\<^sup>1 D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C \<prec>\<^sup>1 D
[PROOF STEP]
by(rule subcls1I[OF cls False])
[PROOF STATE]
proof (state)
this:
P \<turnstile> C \<prec>\<^sup>1 D

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<turnstile> C \<prec>\<^sup>1 D

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
have "class P D \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class P D \<noteq> None
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
is_class P D

goal (1 subgoal):
 1. class P D \<noteq> None
[PROOF STEP]
by(simp add: is_class_def)
[PROOF STATE]
proof (state)
this:
class P D \<noteq> None

goal (1 subgoal):
 1. \<lbrakk>class P C \<noteq> None; C \<noteq> Object\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>
wf_cdecl wf_md P (C, D, fs, ms)
is_class P D
P \<turnstile> C \<prec>\<^sup>1 D
class P D \<noteq> None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>
wf_cdecl wf_md P (C, D, fs, ms)
is_class P D
P \<turnstile> C \<prec>\<^sup>1 D
class P D \<noteq> None

goal (1 subgoal):
 1. Q C
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>
wf_cdecl wf_md P (C, D, fs, ms)
is_class P D
P \<turnstile> C \<prec>\<^sup>1 D
class P D \<noteq> None
\<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> class P D \<noteq> None \<longrightarrow> Q D

goal (1 subgoal):
 1. Q C
[PROOF STEP]
by (auto intro: p[OF False is_cls])
[PROOF STATE]
proof (state)
this:
Q C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
class P C \<noteq> None \<Longrightarrow> Q C

goal (1 subgoal):
 1. \<And>C. \<forall>D. (C, D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> class P D \<noteq> None \<longrightarrow> Q D \<Longrightarrow> class P C \<noteq> None \<longrightarrow> Q C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
class P C \<noteq> None \<Longrightarrow> Q C
[PROOF STEP]
show "class P C \<noteq> None \<longrightarrow> Q C"
[PROOF STATE]
proof (prove)
using this:
class P C \<noteq> None \<Longrightarrow> Q C

goal (1 subgoal):
 1. class P C \<noteq> None \<longrightarrow> Q C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
class P C \<noteq> None \<longrightarrow> Q C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
class P C \<noteq> None \<longrightarrow> Q C

goal (1 subgoal):
 1. (\<And>C D fs ms. \<lbrakk>C \<noteq> Object; is_class P C; class P C = \<lfloor>(D, fs, ms)\<rfloor> \<and> wf_cdecl wf_md P (C, D, fs, ms) \<and> P \<turnstile> C \<prec>\<^sup>1 D \<and> is_class P D \<and> Q D\<rbrakk> \<Longrightarrow> Q C) \<Longrightarrow> Q C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
class P C \<noteq> None \<longrightarrow> Q C

goal (1 subgoal):
 1. Q C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
class P C \<noteq> None \<longrightarrow> Q C
is_class P C
wf_prog wf_md P
Q Object

goal (1 subgoal):
 1. Q C
[PROOF STEP]
by(unfold is_class_def) simp
[PROOF STATE]
proof (state)
this:
Q C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subcls1_induct [consumes 2, case_names Object Subcls]:
  "\<lbrakk> wf_prog wf_md P; is_class P C; Q Object;
    \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; Q D\<rbrakk> \<Longrightarrow> Q C \<rbrakk>
  \<Longrightarrow> Q C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; is_class P C; Q Object; \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; Q D\<rbrakk> \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; is_class P C; Q Object; \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; Q D\<rbrakk> \<Longrightarrow> Q C\<rbrakk> \<Longrightarrow> Q C
[PROOF STEP]
by (erule (2) subcls1_induct_aux) blast