[STATEMENT]
lemma resPres:
  fixes P :: pi
  and   Q :: pi
  and   x :: name
  
  assumes "P \<approx> Q"

  shows "<\<nu>x>P \<approx> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
let ?X = "{(<\<nu>x>P, <\<nu>x>Q) | x P Q. P \<approx> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
from \<open>P \<approx> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<approx> Q
[PROOF STEP]
have "(<\<nu>x>P, <\<nu>x>Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<approx> Q

goal (1 subgoal):
 1. (<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
proof(coinduct rule: weakBisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
case(cSim xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
fix P Q x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
assume "P \<approx> Q"
[PROOF STATE]
proof (state)
this:
P \<approx> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
hence "P \<leadsto><weakBisim> Q"
[PROOF STATE]
proof (prove)
using this:
P \<approx> Q

goal (1 subgoal):
 1. P \<leadsto><weakBisim> Q
[PROOF STEP]
by(rule weakBisimE)
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "\<And>P Q x. P \<approx> Q \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> ?X \<union> weakBisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q x. P \<approx> Q \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "weakBisim \<subseteq> ?X \<union> weakBisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "eqvt weakBisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt weakBisim
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eqvt weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "eqvt (?X \<union> weakBisim)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)
[PROOF STEP]
by(auto simp add: eqvt_def dest: Weak_Early_Bisim.eqvtI)+
[PROOF STATE]
proof (state)
this:
eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto><weakBisim> Q
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
eqvt weakBisim
eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)
[PROOF STEP]
have "<\<nu>x>P \<leadsto><(?X \<union> weakBisim)> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><weakBisim> Q
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
eqvt weakBisim
eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)

goal (1 subgoal):
 1. <\<nu>x>P \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>x>Q
[PROOF STEP]
by(rule Weak_Early_Sim_Pres.resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>x>P \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>x>Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Pa2 \<approx> ?Qa2 \<Longrightarrow> <\<nu>?xa2>?Pa2 \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>?xa2>?Qa2

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
with \<open>(xP, xQ) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
?Pa2 \<approx> ?Qa2 \<Longrightarrow> <\<nu>?xa2>?Pa2 \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>?xa2>?Qa2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
?Pa2 \<approx> ?Qa2 \<Longrightarrow> <\<nu>?xa2>?Pa2 \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>?xa2>?Qa2

goal (1 subgoal):
 1. xP \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> xQ
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xP \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> xQ

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
case(cSym xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. (xQ, xP) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
by(blast dest: Weak_Early_Bisim.symetric)
[PROOF STATE]
proof (state)
this:
(xQ, xP) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
<\<nu>x>P \<approx> <\<nu>x>Q

goal:
No subgoals!
[PROOF STEP]
qed