[STATEMENT]
lemma eqvtChainI[eqvt]:
  fixes P    :: pi
  and   P'   :: pi
  and   perm :: "name prm"

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"

  shows "(perm \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (perm \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'

goal (1 subgoal):
 1. perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
case(ih P'' P''')
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''
perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
have "P \<Longrightarrow>\<^sub>\<tau> P''" and "P'' \<longmapsto> \<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'' &&& P'' \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
hence "(perm \<bullet> P'') \<longmapsto>\<tau> \<prec> (perm \<bullet> P''')"
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. perm \<bullet> P'' \<longmapsto> \<tau> \<prec> perm \<bullet> P'''
[PROOF STEP]
by(force dest: transitions.eqvt)
[PROOF STATE]
proof (state)
this:
perm \<bullet> P'' \<longmapsto> \<tau> \<prec> perm \<bullet> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
perm \<bullet> P'' \<longmapsto> \<tau> \<prec> perm \<bullet> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
have "(perm \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (perm \<bullet> P'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'\<rbrakk> \<Longrightarrow> perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
perm \<bullet> P'' \<longmapsto> \<tau> \<prec> perm \<bullet> P'''
perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
perm \<bullet> P'' \<longmapsto> \<tau> \<prec> perm \<bullet> P'''
perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P''

goal (1 subgoal):
 1. perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvtChainE:
  fixes perm :: "name prm"
  and   P    :: pi
  and   P'   :: pi

  assumes Trans: "(perm \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (perm \<bullet> P')"

  shows   "P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
have "rev perm \<bullet> (perm \<bullet> P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev perm \<bullet> perm \<bullet> P = P
[PROOF STEP]
by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
rev perm \<bullet> perm \<bullet> P = P

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rev perm \<bullet> perm \<bullet> P = P

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
have "rev perm \<bullet> (perm \<bullet> P') = P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev perm \<bullet> perm \<bullet> P' = P'
[PROOF STEP]
by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
rev perm \<bullet> perm \<bullet> P' = P'

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rev perm \<bullet> perm \<bullet> P = P
rev perm \<bullet> perm \<bullet> P' = P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rev perm \<bullet> perm \<bullet> P = P
rev perm \<bullet> perm \<bullet> P' = P'

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rev perm \<bullet> perm \<bullet> P = P
rev perm \<bullet> perm \<bullet> P' = P'
perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by(drule_tac perm="rev perm" in eqvtChainI, simp)
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvtChainEq:
  fixes P    :: pi
  and   P'   :: pi
  and   perm :: "name prm"

  shows   "P \<Longrightarrow>\<^sub>\<tau> P' = (perm \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (perm \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P' = perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'
[PROOF STEP]
by(blast intro: eqvtChainE eqvtChainI)


[STATEMENT]
lemma freshChain:
  fixes P  :: pi
  and   P' :: pi
  and   x  :: name

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "x \<sharp> P"

  shows   "x \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'
x \<sharp> P

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<sharp> P \<Longrightarrow> x \<sharp> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:
x \<sharp> P

goal (2 subgoals):
 1. x \<sharp> P \<Longrightarrow> x \<sharp> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P

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

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
case(ih P' P'')
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P'
P' \<longmapsto> \<tau> \<prec> P''
x \<sharp> P \<Longrightarrow> x \<sharp> P'
x \<sharp> P

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
have "x \<sharp> P" and "x \<sharp> P \<Longrightarrow> x \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P &&& (x \<sharp> P \<Longrightarrow> x \<sharp> P')
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
x \<sharp> P
x \<sharp> P \<Longrightarrow> x \<sharp> P'

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
hence "x \<sharp> P'"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P
x \<sharp> P \<Longrightarrow> x \<sharp> P'

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> P'

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<sharp> P'

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
have "P' \<longmapsto> \<tau> \<prec> P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' \<longmapsto> \<tau> \<prec> P''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P' \<longmapsto> \<tau> \<prec> P''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; x \<sharp> P \<Longrightarrow> x \<sharp> P'; x \<sharp> P\<rbrakk> \<Longrightarrow> x \<sharp> P''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> P'
P' \<longmapsto> \<tau> \<prec> P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P'
P' \<longmapsto> \<tau> \<prec> P''

goal (1 subgoal):
 1. x \<sharp> P''
[PROOF STEP]
by(force intro: freshFreeDerivative)
[PROOF STATE]
proof (state)
this:
x \<sharp> P''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matchChain:
  fixes b :: name
  and   P :: pi
  and   P' :: pi

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "P \<noteq> P'"

  shows "[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'
P \<noteq> P'

goal (1 subgoal):
 1. [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<noteq> P \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:
P \<noteq> P

goal (2 subgoals):
 1. P \<noteq> P \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P

goal (1 subgoal):
 1. [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case(ih P'' P''')
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''
P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
P \<noteq> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
have P''TransP''':  "P'' \<longmapsto>\<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P'' \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show "[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
proof(cases "P = P''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
assume "P=P''"
[PROOF STATE]
proof (state)
this:
P = P''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P = P''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
with P''TransP'''
[PROOF STATE]
proof (chain)
picking this:
P'' \<longmapsto> \<tau> \<prec> P'''
P = P''
[PROOF STEP]
have "[b\<frown>b]P \<longmapsto>\<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
using this:
P'' \<longmapsto> \<tau> \<prec> P'''
P = P''

goal (1 subgoal):
 1. [b\<frown>b]P \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by(force intro: Match)
[PROOF STATE]
proof (state)
this:
[b\<frown>b]P \<longmapsto> \<tau> \<prec> P'''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
thus "[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
using this:
[b\<frown>b]P \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
by(rule singleTauChain)
[PROOF STATE]
proof (state)
this:
[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
assume "P \<noteq> P''"
[PROOF STATE]
proof (state)
this:
P \<noteq> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<noteq> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
have "P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show "[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
using P''TransP'''
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. [b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[b\<frown>b]P \<Longrightarrow>\<^sub>\<tau> P'''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mismatchChain:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   P' :: pi

  assumes PChain: "P \<Longrightarrow>\<^sub>\<tau> P'"
  and     aineqb: "a \<noteq> b"
  and     PineqP': "P \<noteq> P'"

  shows "[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using PChain PineqP'
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'
P \<noteq> P'

goal (1 subgoal):
 1. [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<noteq> P \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:
P \<noteq> P

goal (2 subgoals):
 1. P \<noteq> P \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P

goal (1 subgoal):
 1. [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case(ih P'' P''')
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''
P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
P \<noteq> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
have P''TransP''':  "P'' \<longmapsto>\<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P'' \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show "[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
proof(cases "P = P''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
assume "P=P''"
[PROOF STATE]
proof (state)
this:
P = P''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P = P''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
with aineqb P''TransP'''
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> b
P'' \<longmapsto> \<tau> \<prec> P'''
P = P''
[PROOF STEP]
have "[a\<noteq>b]P \<longmapsto>\<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b
P'' \<longmapsto> \<tau> \<prec> P'''
P = P''

goal (1 subgoal):
 1. [a\<noteq>b]P \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by(force intro: Mismatch)
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<longmapsto> \<tau> \<prec> P'''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
thus "[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
using this:
[a\<noteq>b]P \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
by(rule singleTauChain)
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
assume "P \<noteq> P''"
[PROOF STATE]
proof (state)
this:
P \<noteq> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<noteq> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
have "P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show "[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
using P''TransP'''
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. [a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<Longrightarrow>\<^sub>\<tau> P'''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum1Chain[rule_format]:
  fixes P  :: pi
  and   P' :: pi
  and   Q  :: pi

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "P \<noteq> P'"

  shows "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'
P \<noteq> P'

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<noteq> P \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:
P \<noteq> P

goal (2 subgoals):
 1. P \<noteq> P \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P

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

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case(ih P'' P''')
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''
P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
P \<noteq> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
have P''TransP''':  "P'' \<longmapsto>\<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P'' \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; P \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
proof(cases "P = P''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
assume "P=P''"
[PROOF STATE]
proof (state)
this:
P = P''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P = P''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
with P''TransP'''
[PROOF STATE]
proof (chain)
picking this:
P'' \<longmapsto> \<tau> \<prec> P'''
P = P''
[PROOF STEP]
have "P \<oplus> Q \<longmapsto>\<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
using this:
P'' \<longmapsto> \<tau> \<prec> P'''
P = P''

goal (1 subgoal):
 1. P \<oplus> Q \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by(force intro: Sum1)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<longmapsto> \<tau> \<prec> P'''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
 2. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
thus "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
using this:
P \<oplus> Q \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
by(force intro: singleTauChain)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
assume "P \<noteq> P''"
[PROOF STATE]
proof (state)
this:
P \<noteq> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<noteq> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
have "P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''"
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
using P''TransP'''
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P''
P \<noteq> P'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''
[PROOF STEP]
by(force)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum2Chain[rule_format]:
  fixes P  :: pi
  and   Q :: pi
  and   Q'  :: pi

  assumes "Q \<Longrightarrow>\<^sub>\<tau> Q'"
  and     "Q \<noteq> Q'"

  shows "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Q \<Longrightarrow>\<^sub>\<tau> Q'
Q \<noteq> Q'

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q \<noteq> Q \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q
 2. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; Q \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; Q \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:
Q \<noteq> Q

goal (2 subgoals):
 1. Q \<noteq> Q \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q
 2. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; Q \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; Q \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Q \<noteq> Q

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

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; Q \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; Q \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; Q \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; Q \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case(ih Q'' Q''')
[PROOF STATE]
proof (state)
this:
Q \<Longrightarrow>\<^sub>\<tau> Q''
Q'' \<longmapsto> \<tau> \<prec> Q'''
Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q''
Q \<noteq> Q'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; Q \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; Q \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
have Q''TransQ''':  "Q'' \<longmapsto>\<tau> \<prec> Q'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q'' \<longmapsto> \<tau> \<prec> Q'''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q'' \<longmapsto> \<tau> \<prec> Q'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; Q \<noteq> P' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P'; Q \<noteq> P''\<rbrakk> \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
proof(cases "Q = Q''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q = Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
 2. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
assume "Q=Q''"
[PROOF STATE]
proof (state)
this:
Q = Q''

goal (2 subgoals):
 1. Q = Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
 2. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Q = Q''

goal (2 subgoals):
 1. Q = Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
 2. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
with Q''TransQ'''
[PROOF STATE]
proof (chain)
picking this:
Q'' \<longmapsto> \<tau> \<prec> Q'''
Q = Q''
[PROOF STEP]
have "P \<oplus> Q \<longmapsto>\<tau> \<prec> Q'''"
[PROOF STATE]
proof (prove)
using this:
Q'' \<longmapsto> \<tau> \<prec> Q'''
Q = Q''

goal (1 subgoal):
 1. P \<oplus> Q \<longmapsto> \<tau> \<prec> Q'''
[PROOF STEP]
by(force intro: Sum2)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<longmapsto> \<tau> \<prec> Q'''

goal (2 subgoals):
 1. Q = Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
 2. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
thus "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''"
[PROOF STATE]
proof (prove)
using this:
P \<oplus> Q \<longmapsto> \<tau> \<prec> Q'''

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
by(force intro: singleTauChain)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''

goal (1 subgoal):
 1. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
assume "Q \<noteq> Q''"
[PROOF STATE]
proof (state)
this:
Q \<noteq> Q''

goal (1 subgoal):
 1. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Q \<noteq> Q''

goal (1 subgoal):
 1. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
have "Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q''

goal (1 subgoal):
 1. Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Q \<noteq> Q''
Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q''
[PROOF STEP]
show "P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''"
[PROOF STATE]
proof (prove)
using this:
Q \<noteq> Q''
Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q''

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
using Q''TransQ'''
[PROOF STATE]
proof (prove)
using this:
Q \<noteq> Q''
Q \<noteq> Q'' \<Longrightarrow> P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q''
Q'' \<longmapsto> \<tau> \<prec> Q'''

goal (1 subgoal):
 1. P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<Longrightarrow>\<^sub>\<tau> Q'''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Par1Chain:
  fixes P  :: pi
  and   P' :: pi
  and   Q  :: pi

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"

  shows "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
case(ih P'' P')
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
have P''TransP':  "P'' \<longmapsto>\<tau> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P'' \<longmapsto> \<tau> \<prec> P'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P'' \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
have IH: "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
have "P'' \<parallel> Q \<longmapsto>\<tau> \<prec> P' \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P'' \<parallel> Q \<longmapsto> \<tau> \<prec> P' \<parallel> Q
[PROOF STEP]
using P''TransP'
[PROOF STATE]
proof (prove)
using this:
P'' \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. P'' \<parallel> Q \<longmapsto> \<tau> \<prec> P' \<parallel> Q
[PROOF STEP]
by(force intro: Par1F)
[PROOF STATE]
proof (state)
this:
P'' \<parallel> Q \<longmapsto> \<tau> \<prec> P' \<parallel> Q

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
thus "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
P'' \<parallel> Q \<longmapsto> \<tau> \<prec> P' \<parallel> Q

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
P'' \<parallel> Q \<longmapsto> \<tau> \<prec> P' \<parallel> Q
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P'' \<parallel> Q

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
by(force)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Par2Chain:
  fixes P  :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes "Q \<Longrightarrow>\<^sub>\<tau> Q'"

  shows "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Q \<Longrightarrow>\<^sub>\<tau> Q'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q
 2. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q
 2. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
case(ih Q'' Q')
[PROOF STATE]
proof (state)
this:
Q \<Longrightarrow>\<^sub>\<tau> Q''
Q'' \<longmapsto> \<tau> \<prec> Q'
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
have Q''TransQ':  "Q'' \<longmapsto>\<tau> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q'' \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q'' \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
have IH: "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
have "P \<parallel> Q'' \<longmapsto>\<tau> \<prec> P \<parallel> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q'' \<longmapsto> \<tau> \<prec> P \<parallel> Q'
[PROOF STEP]
using Q''TransQ'
[PROOF STATE]
proof (prove)
using this:
Q'' \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. P \<parallel> Q'' \<longmapsto> \<tau> \<prec> P \<parallel> Q'
[PROOF STEP]
by(force intro: Par2F)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q'' \<longmapsto> \<tau> \<prec> P \<parallel> Q'

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>Q \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P'\<rbrakk> \<Longrightarrow> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> P''
[PROOF STEP]
thus "P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'"
[PROOF STATE]
proof (prove)
using this:
P \<parallel> Q'' \<longmapsto> \<tau> \<prec> P \<parallel> Q'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
P \<parallel> Q'' \<longmapsto> \<tau> \<prec> P \<parallel> Q'
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q''

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
by(force)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ResChain:
  fixes P  :: pi
  and   P' :: pi
  and   a  :: name

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"

  shows "<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'

goal (1 subgoal):
 1. <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P
 2. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
case(ih P'' P''')
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>\<tau> P''
P'' \<longmapsto> \<tau> \<prec> P'''
<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
have "P'' \<longmapsto>\<tau> \<prec> P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P'' \<longmapsto> \<tau> \<prec> P'''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
hence "<\<nu>a>P'' \<longmapsto>\<tau> \<prec> <\<nu>a>P'''"
[PROOF STATE]
proof (prove)
using this:
P'' \<longmapsto> \<tau> \<prec> P'''

goal (1 subgoal):
 1. <\<nu>a>P'' \<longmapsto> \<tau> \<prec> <\<nu>a>P'''
[PROOF STEP]
by(force intro: ResF)
[PROOF STATE]
proof (state)
this:
<\<nu>a>P'' \<longmapsto> \<tau> \<prec> <\<nu>a>P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
<\<nu>a>P'' \<longmapsto> \<tau> \<prec> <\<nu>a>P'''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
have "<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'\<rbrakk> \<Longrightarrow> <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
<\<nu>a>P'' \<longmapsto> \<tau> \<prec> <\<nu>a>P'''
<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
<\<nu>a>P'' \<longmapsto> \<tau> \<prec> <\<nu>a>P'''
<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P''

goal (1 subgoal):
 1. <\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'''
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<Longrightarrow>\<^sub>\<tau> <\<nu>a>P'''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma substChain:
  fixes P  :: pi
  and   x  :: name
  and   b  :: name
  and   P' :: pi

  assumes PTrans: "P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'"

  shows "P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
proof(cases "x=b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
 2. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
assume "x = b"
[PROOF STATE]
proof (state)
this:
x = b

goal (2 subgoals):
 1. x = b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
 2. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'
x = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'
x = b

goal (1 subgoal):
 1. P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
assume "x \<noteq> b"
[PROOF STATE]
proof (state)
this:
x \<noteq> b

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
hence "x \<sharp> P[x::=b]"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> b

goal (1 subgoal):
 1. x \<sharp> P[x::=b]
[PROOF STEP]
by(simp add: fresh_fact2)
[PROOF STATE]
proof (state)
this:
x \<sharp> P[x::=b]

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'
x \<sharp> P[x::=b]
[PROOF STEP]
have "x \<sharp> P'"
[PROOF STATE]
proof (prove)
using this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'
x \<sharp> P[x::=b]

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
by(force intro: freshChain)
[PROOF STATE]
proof (state)
this:
x \<sharp> P'

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
hence "P' = P'[x::=b]"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P'

goal (1 subgoal):
 1. P' = P'[x::=b]
[PROOF STEP]
by(simp add: forget)
[PROOF STATE]
proof (state)
this:
P' = P'[x::=b]

goal (1 subgoal):
 1. x \<noteq> b \<Longrightarrow> P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'
P' = P'[x::=b]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'
P' = P'[x::=b]

goal (1 subgoal):
 1. P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P[x::=b] \<Longrightarrow>\<^sub>\<tau> P'[x::=b]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bangChain:
  fixes P  :: pi
  and   P' :: pi

  assumes PTrans: "P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'"
  and     P'ineq: "P' \<noteq> P \<parallel> !P"

  shows "!P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'
P' \<noteq> P \<parallel> !P

goal (1 subgoal):
 1. !P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
proof(induct rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<parallel> !P \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P \<parallel> !P
 2. \<And>P' P''. \<lbrakk>P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P'; P'' \<noteq> P \<parallel> !P\<rbrakk> \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case id
[PROOF STATE]
proof (state)
this:
P \<parallel> !P \<noteq> P \<parallel> !P

goal (2 subgoals):
 1. P \<parallel> !P \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P \<parallel> !P
 2. \<And>P' P''. \<lbrakk>P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P'; P'' \<noteq> P \<parallel> !P\<rbrakk> \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> !P \<noteq> P \<parallel> !P

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

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P'; P'' \<noteq> P \<parallel> !P\<rbrakk> \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P'; P'' \<noteq> P \<parallel> !P\<rbrakk> \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case(ih P' P'')
[PROOF STATE]
proof (state)
this:
P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'
P' \<longmapsto> \<tau> \<prec> P''
P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P'
P'' \<noteq> P \<parallel> !P

goal (1 subgoal):
 1. \<And>P' P''. \<lbrakk>P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''; P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P'; P'' \<noteq> P \<parallel> !P\<rbrakk> \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
proof(cases "P' = P \<parallel> !P")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P' = P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
 2. P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
P' = P \<parallel> !P

goal (2 subgoals):
 1. P' = P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
 2. P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
from \<open>P' \<longmapsto>\<tau> \<prec> P''\<close> \<open>P' = P \<parallel> !P\<close>
[PROOF STATE]
proof (chain)
picking this:
P' \<longmapsto> \<tau> \<prec> P''
P' = P \<parallel> !P
[PROOF STEP]
have "!P \<longmapsto>\<tau> \<prec> P''"
[PROOF STATE]
proof (prove)
using this:
P' \<longmapsto> \<tau> \<prec> P''
P' = P \<parallel> !P

goal (1 subgoal):
 1. !P \<longmapsto> \<tau> \<prec> P''
[PROOF STEP]
by(blast intro: Bang)
[PROOF STATE]
proof (state)
this:
!P \<longmapsto> \<tau> \<prec> P''

goal (2 subgoals):
 1. P' = P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
 2. P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
!P \<longmapsto> \<tau> \<prec> P''

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

goal (1 subgoal):
 1. P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
P' \<noteq> P \<parallel> !P

goal (1 subgoal):
 1. P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
from \<open>P' \<noteq> P \<parallel> !P\<close>
[PROOF STATE]
proof (chain)
picking this:
P' \<noteq> P \<parallel> !P
[PROOF STEP]
have "!P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
using this:
P' \<noteq> P \<parallel> !P

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

goal (1 subgoal):
 1. P' \<noteq> P \<parallel> !P \<Longrightarrow> !P \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
with \<open>P' \<longmapsto>\<tau> \<prec> P''\<close>
[PROOF STATE]
proof (chain)
picking this:
P' \<longmapsto> \<tau> \<prec> P''
!P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P' \<longmapsto> \<tau> \<prec> P''
!P \<Longrightarrow>\<^sub>\<tau> P'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
!P \<Longrightarrow>\<^sub>\<tau> P''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [mono]:"
         (!! x. f x --> g x) ==> list_all (%b. b) (map f foo_list)-->
                    list_all (%b. b) (map g foo_list) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x \<longrightarrow> g x) \<Longrightarrow> list_all (\<lambda>b. b) (map f foo_list) \<longrightarrow> list_all (\<lambda>b. b) (map g foo_list)
[PROOF STEP]
apply(induct_tac foo_list, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [mono]: "case_prod f p = f (fst p) (snd p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case p of (x, xa) \<Rightarrow> f x xa) = f (fst p) (snd p)
[PROOF STEP]
by (simp add: split_def)


[STATEMENT]
lemma (in ergodic_qmpt) AE_equal_preimage_then_null_or_conull:
  assumes [measurable]: "A \<in> sets M" and "A \<Delta> T--`A \<in> null_sets M"
  shows "A \<in> null_sets M \<or> space M - A \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
obtain B where B: "B \<in> sets Invariants" "A \<Delta> B \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<in> sets Invariants; A \<Delta> B \<in> null_sets M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Un_commute Invariants_quasi_Invariants_sets[OF assms(1)] assms(2))
[PROOF STATE]
proof (state)
this:
B \<in> sets Invariants
A \<Delta> B \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
have [measurable]: "B \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> sets M
[PROOF STEP]
using B(1)
[PROOF STATE]
proof (prove)
using this:
B \<in> sets Invariants

goal (1 subgoal):
 1. B \<in> sets M
[PROOF STEP]
using Invariants_in_sets
[PROOF STATE]
proof (prove)
using this:
B \<in> sets Invariants
?A \<in> sets Invariants \<Longrightarrow> ?A \<in> sets M

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

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
have *: "B \<in> null_sets M \<or> space M - B \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> null_sets M \<or> space M - B \<in> null_sets M
[PROOF STEP]
using ergodic B(1)
[PROOF STATE]
proof (prove)
using this:
?A \<in> sets Invariants \<Longrightarrow> ?A \<in> null_sets M \<or> space M - ?A \<in> null_sets M
B \<in> sets Invariants

goal (1 subgoal):
 1. B \<in> null_sets M \<or> space M - B \<in> null_sets M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B \<in> null_sets M \<or> space M - B \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
 2. \<not> ?P \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
assume "B \<in> null_sets M"
[PROOF STATE]
proof (state)
this:
B \<in> null_sets M

goal (2 subgoals):
 1. ?P \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
 2. \<not> ?P \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> null_sets M
[PROOF STEP]
have "A \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
B \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M
[PROOF STEP]
by (metis Un_commute B(2) Delta_null_of_null_is_null[OF assms(1), where ?A = B])
[PROOF STATE]
proof (state)
this:
A \<in> null_sets M

goal (2 subgoals):
 1. ?P \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
 2. \<not> ?P \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> null_sets M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<in> null_sets M \<or> space M - A \<in> null_sets M

goal (1 subgoal):
 1. B \<notin> null_sets M \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B \<notin> null_sets M \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
assume "\<not>(B \<in> null_sets M)"
[PROOF STATE]
proof (state)
this:
B \<notin> null_sets M

goal (1 subgoal):
 1. B \<notin> null_sets M \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<notin> null_sets M
[PROOF STEP]
have i: "space M - B \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
B \<notin> null_sets M

goal (1 subgoal):
 1. space M - B \<in> null_sets M
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
B \<notin> null_sets M
B \<in> null_sets M \<or> space M - B \<in> null_sets M

goal (1 subgoal):
 1. space M - B \<in> null_sets M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
space M - B \<in> null_sets M

goal (1 subgoal):
 1. B \<notin> null_sets M \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
have "(space M - B) \<Delta> (space M - A) = A \<Delta> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (space M - B) \<Delta> (space M - A) = A \<Delta> B
[PROOF STEP]
using sets.sets_into_space[OF \<open>A \<in> sets M\<close>] sets.sets_into_space[OF \<open>B \<in> sets M\<close>]
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> space M
B \<subseteq> space M

goal (1 subgoal):
 1. (space M - B) \<Delta> (space M - A) = A \<Delta> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(space M - B) \<Delta> (space M - A) = A \<Delta> B

goal (1 subgoal):
 1. B \<notin> null_sets M \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(space M - B) \<Delta> (space M - A) = A \<Delta> B
[PROOF STEP]
have "(space M - B) \<Delta> (space M - A) \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
(space M - B) \<Delta> (space M - A) = A \<Delta> B

goal (1 subgoal):
 1. (space M - B) \<Delta> (space M - A) \<in> null_sets M
[PROOF STEP]
using B(2)
[PROOF STATE]
proof (prove)
using this:
(space M - B) \<Delta> (space M - A) = A \<Delta> B
A \<Delta> B \<in> null_sets M

goal (1 subgoal):
 1. (space M - B) \<Delta> (space M - A) \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(space M - B) \<Delta> (space M - A) \<in> null_sets M

goal (1 subgoal):
 1. B \<notin> null_sets M \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(space M - B) \<Delta> (space M - A) \<in> null_sets M
[PROOF STEP]
have "space M - A \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
(space M - B) \<Delta> (space M - A) \<in> null_sets M

goal (1 subgoal):
 1. space M - A \<in> null_sets M
[PROOF STEP]
using Delta_null_of_null_is_null[where ?A = "space M - B" and ?B = "space M - A"] i
[PROOF STATE]
proof (prove)
using this:
(space M - B) \<Delta> (space M - A) \<in> null_sets M
\<lbrakk>space M - A \<in> sets ?M; (space M - B) \<Delta> (space M - A) \<in> null_sets ?M; space M - B \<in> null_sets ?M\<rbrakk> \<Longrightarrow> space M - A \<in> null_sets ?M
space M - B \<in> null_sets M

goal (1 subgoal):
 1. space M - A \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space M - A \<in> null_sets M

goal (1 subgoal):
 1. B \<notin> null_sets M \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
space M - A \<in> null_sets M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
space M - A \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<in> null_sets M \<or> space M - A \<in> null_sets M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<in> null_sets M \<or> space M - A \<in> null_sets M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_qmpt) ergodic_Tinv:
  assumes "invertible_qmpt"
  shows "ergodic_qmpt M Tinv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ergodic_qmpt M Tinv
[PROOF STEP]
unfolding ergodic_qmpt_def ergodic_qmpt_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmpt M Tinv \<and> (\<forall>A. A \<in> sets (qmpt.Invariants M Tinv) \<longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. qmpt M Tinv
 2. \<forall>A. A \<in> sets (qmpt.Invariants M Tinv) \<longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
show "qmpt M Tinv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmpt M Tinv
[PROOF STEP]
using Tinv_qmpt[OF assms]
[PROOF STATE]
proof (prove)
using this:
qmpt M Tinv

goal (1 subgoal):
 1. qmpt M Tinv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qmpt M Tinv

goal (1 subgoal):
 1. \<forall>A. A \<in> sets (qmpt.Invariants M Tinv) \<longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
show "\<forall>A. A \<in> sets (qmpt.Invariants M Tinv) \<longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. A \<in> sets (qmpt.Invariants M Tinv) \<longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. A \<in> sets (qmpt.Invariants M Tinv) \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. A \<in> sets (qmpt.Invariants M Tinv) \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
assume "A \<in> sets (qmpt.Invariants M Tinv)"
[PROOF STATE]
proof (state)
this:
A \<in> sets (qmpt.Invariants M Tinv)

goal (1 subgoal):
 1. \<And>A. A \<in> sets (qmpt.Invariants M Tinv) \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> sets (qmpt.Invariants M Tinv)
[PROOF STEP]
have "A \<in> sets Invariants"
[PROOF STATE]
proof (prove)
using this:
A \<in> sets (qmpt.Invariants M Tinv)

goal (1 subgoal):
 1. A \<in> sets Invariants
[PROOF STEP]
using Invariants_Tinv[OF assms]
[PROOF STATE]
proof (prove)
using this:
A \<in> sets (qmpt.Invariants M Tinv)
qmpt.Invariants M Tinv = Invariants

goal (1 subgoal):
 1. A \<in> sets Invariants
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<in> sets Invariants

goal (1 subgoal):
 1. \<And>A. A \<in> sets (qmpt.Invariants M Tinv) \<Longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> sets Invariants
[PROOF STEP]
show "A \<in> null_sets M \<or> space M - A \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
A \<in> sets Invariants

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
using ergodic
[PROOF STATE]
proof (prove)
using this:
A \<in> sets Invariants
?A \<in> sets Invariants \<Longrightarrow> ?A \<in> null_sets M \<or> space M - ?A \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> null_sets M \<or> space M - A \<in> null_sets M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>A. A \<in> sets (qmpt.Invariants M Tinv) \<longrightarrow> A \<in> null_sets M \<or> space M - A \<in> null_sets M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_conservative) preimage_included_then_null_or_conull:
  assumes "A \<in> sets M" "T--`A \<subseteq> A"
  shows "A \<in> null_sets M \<or> space M - A \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
have "A \<Delta> T--`A \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Delta> T --` A \<in> null_sets M
[PROOF STEP]
using preimage_included_then_almost_invariant[OF assms]
[PROOF STATE]
proof (prove)
using this:
A \<Delta> T --` A \<in> null_sets M

goal (1 subgoal):
 1. A \<Delta> T --` A \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<Delta> T --` A \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<Delta> T --` A \<in> null_sets M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<Delta> T --` A \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
using AE_equal_preimage_then_null_or_conull assms(1)
[PROOF STATE]
proof (prove)
using this:
A \<Delta> T --` A \<in> null_sets M
\<lbrakk>?A \<in> sets M; ?A \<Delta> T --` ?A \<in> null_sets M\<rbrakk> \<Longrightarrow> ?A \<in> null_sets M \<or> space M - ?A \<in> null_sets M
A \<in> sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> null_sets M \<or> space M - A \<in> null_sets M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_conservative) preimage_includes_then_null_or_conull:
  assumes "A \<in> sets M" "T--`A \<supseteq> A"
  shows "A \<in> null_sets M \<or> space M - A \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
have "A \<Delta> T--`A \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<Delta> T --` A \<in> null_sets M
[PROOF STEP]
using preimage_includes_then_almost_invariant[OF assms]
[PROOF STATE]
proof (prove)
using this:
A \<Delta> T --` A \<in> null_sets M

goal (1 subgoal):
 1. A \<Delta> T --` A \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<Delta> T --` A \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<Delta> T --` A \<in> null_sets M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<Delta> T --` A \<in> null_sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
using AE_equal_preimage_then_null_or_conull assms(1)
[PROOF STATE]
proof (prove)
using this:
A \<Delta> T --` A \<in> null_sets M
\<lbrakk>?A \<in> sets M; ?A \<Delta> T --` ?A \<in> null_sets M\<rbrakk> \<Longrightarrow> ?A \<in> null_sets M \<or> space M - ?A \<in> null_sets M
A \<in> sets M

goal (1 subgoal):
 1. A \<in> null_sets M \<or> space M - A \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> null_sets M \<or> space M - A \<in> null_sets M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_conservative) preimages_conull:
  assumes [measurable]: "A \<in> sets M" and "emeasure M A > 0"
  shows "space M - (\<Union>n. (T^^n)--`A) \<in> null_sets M"
        "space M \<Delta> (\<Union>n. (T^^n)--`A) \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M &&& space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
define B where "B = (\<Union>n. (T^^n)--`A)"
[PROOF STATE]
proof (state)
this:
B = (\<Union>n. (T ^^ n) --` A)

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B = (\<Union>n. (T ^^ n) --` A)
[PROOF STEP]
have [measurable]: "B \<in> sets M"
[PROOF STATE]
proof (prove)
using this:
B = (\<Union>n. (T ^^ n) --` A)

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

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
have "T--`B = (\<Union>n. (T^^(n+1))--`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T --` B = (\<Union>n. (T ^^ (n + 1)) --` A)
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T --` (\<Union>n. (T ^^ n) --` A) = (\<Union>n. (T ^^ (n + 1)) --` A)
[PROOF STEP]
using T_vrestr_composed(2)
[PROOF STATE]
proof (prove)
using this:
?A \<in> sets M \<Longrightarrow> T --` (T ^^ ?m) --` ?A = (T ^^ (?m + 1)) --` ?A

goal (1 subgoal):
 1. T --` (\<Union>n. (T ^^ n) --` A) = (\<Union>n. (T ^^ (n + 1)) --` A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T --` B = (\<Union>n. (T ^^ (n + 1)) --` A)

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T --` B = (\<Union>n. (T ^^ (n + 1)) --` A)
[PROOF STEP]
have "T--`B \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
T --` B = (\<Union>n. (T ^^ (n + 1)) --` A)

goal (1 subgoal):
 1. T --` B \<subseteq> B
[PROOF STEP]
using B_def
[PROOF STATE]
proof (prove)
using this:
T --` B = (\<Union>n. (T ^^ (n + 1)) --` A)
B = (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. T --` B \<subseteq> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T --` B \<subseteq> B

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T --` B \<subseteq> B
[PROOF STEP]
have *: "B \<in> null_sets M \<or> space M - B \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
T --` B \<subseteq> B

goal (1 subgoal):
 1. B \<in> null_sets M \<or> space M - B \<in> null_sets M
[PROOF STEP]
using preimage_included_then_null_or_conull
[PROOF STATE]
proof (prove)
using this:
T --` B \<subseteq> B
\<lbrakk>?A \<in> sets M; T --` ?A \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?A \<in> null_sets M \<or> space M - ?A \<in> null_sets M

goal (1 subgoal):
 1. B \<in> null_sets M \<or> space M - B \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<in> null_sets M \<or> space M - B \<in> null_sets M

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
have "A \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> (\<Union>n. (T ^^ n) --` A)
[PROOF STEP]
using T_vrestr_0 assms(1)
[PROOF STATE]
proof (prove)
using this:
?A \<in> sets M \<Longrightarrow> (T ^^ 0) --` ?A = ?A
?A \<in> sets M \<Longrightarrow> id --` ?A = ?A
A \<in> sets M

goal (1 subgoal):
 1. A \<subseteq> (\<Union>n. (T ^^ n) --` A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<subseteq> B

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> B
[PROOF STEP]
have "emeasure M B > 0"
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B

goal (1 subgoal):
 1. 0 < emeasure M B
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B
0 < emeasure M A

goal (1 subgoal):
 1. 0 < emeasure M B
[PROOF STEP]
by (metis \<open>B \<in> sets M\<close> emeasure_eq_0 zero_less_iff_neq_zero)
[PROOF STATE]
proof (state)
this:
0 < emeasure M B

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < emeasure M B
[PROOF STEP]
have "B \<notin> null_sets M"
[PROOF STATE]
proof (prove)
using this:
0 < emeasure M B

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

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<notin> null_sets M
[PROOF STEP]
have i: "space M - B \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
B \<notin> null_sets M

goal (1 subgoal):
 1. space M - B \<in> null_sets M
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
B \<notin> null_sets M
B \<in> null_sets M \<or> space M - B \<in> null_sets M

goal (1 subgoal):
 1. space M - B \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space M - B \<in> null_sets M

goal (2 subgoals):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
 2. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
space M - B \<in> null_sets M
[PROOF STEP]
show "space M - (\<Union>n. (T^^n)--`A) \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
space M - B \<in> null_sets M

goal (1 subgoal):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
using B_def
[PROOF STATE]
proof (prove)
using this:
space M - B \<in> null_sets M
B = (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space M - (\<Union>n. (T ^^ n) --` A) \<in> null_sets M

goal (1 subgoal):
 1. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
have "B \<subseteq> space M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> space M
[PROOF STEP]
using sets.sets_into_space[OF \<open>B \<in> sets M\<close>]
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> space M

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

goal (1 subgoal):
 1. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<subseteq> space M
[PROOF STEP]
have "space M \<Delta> B \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> space M

goal (1 subgoal):
 1. space M \<Delta> B \<in> null_sets M
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> space M
space M - B \<in> null_sets M

goal (1 subgoal):
 1. space M \<Delta> B \<in> null_sets M
[PROOF STEP]
by (simp add: Diff_mono sup.absorb1)
[PROOF STATE]
proof (state)
this:
space M \<Delta> B \<in> null_sets M

goal (1 subgoal):
 1. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
space M \<Delta> B \<in> null_sets M
[PROOF STEP]
show "space M \<Delta> (\<Union>n. (T^^n)--`A) \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
space M \<Delta> B \<in> null_sets M

goal (1 subgoal):
 1. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
using B_def
[PROOF STATE]
proof (prove)
using this:
space M \<Delta> B \<in> null_sets M
B = (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M

goal:
No subgoals!
[PROOF STEP]
qed