[STATEMENT]
lemma \<tau>diverge_into_\<tau>mredT:
  assumes "\<tau>diverge t (x, shr s)"
  and "thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>" "wset s t = None"
  shows "mthr.\<tau>diverge s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mthr.\<tau>diverge s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>diverge t (x, shr s)
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None

goal (1 subgoal):
 1. mthr.\<tau>diverge s
[PROOF STEP]
proof(coinduction arbitrary: s x)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
case (\<tau>diverge s x)
[PROOF STATE]
proof (state)
this:
\<tau>diverge t (x, shr s)
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
note tst = \<open>thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>\<close>
[PROOF STATE]
proof (state)
this:
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
from \<open>\<tau>diverge t (x, shr s)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau>diverge t (x, shr s)
[PROOF STEP]
obtain x' m' where "silent_move t (x, shr s) (x', m')" 
    and "\<tau>diverge t (x', m')"
[PROOF STATE]
proof (prove)
using this:
\<tau>diverge t (x, shr s)

goal (1 subgoal):
 1. (\<And>x' m'. \<lbrakk>silent_move t (x, shr s) (x', m'); \<tau>diverge t (x', m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
silent_move t (x, shr s) (x', m')
\<tau>diverge t (x', m')

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
from \<open>silent_move t (x, shr s) (x', m')\<close> tst \<open>wset s t = None\<close>
[PROOF STATE]
proof (chain)
picking this:
silent_move t (x, shr s) (x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None
[PROOF STEP]
have "\<tau>mredT s (redT_upd_\<epsilon> s t x' m')"
[PROOF STATE]
proof (prove)
using this:
silent_move t (x, shr s) (x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None

goal (1 subgoal):
 1. \<tau>mredT s (redT_upd_\<epsilon> s t x' m')
[PROOF STEP]
by(rule silent_move_into_RedT_\<tau>_inv)
[PROOF STATE]
proof (state)
this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
have "thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
[PROOF STEP]
using tst
[PROOF STATE]
proof (prove)
using this:
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
[PROOF STEP]
by(auto simp add: redT_updLns_def)
[PROOF STATE]
proof (state)
this:
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
have "wset (redT_upd_\<epsilon> s t x' m') t = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wset (redT_upd_\<epsilon> s t x' m') t = None
[PROOF STEP]
using \<open>wset s t = None\<close>
[PROOF STATE]
proof (prove)
using this:
wset s t = None

goal (1 subgoal):
 1. wset (redT_upd_\<epsilon> s t x' m') t = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wset (redT_upd_\<epsilon> s t x' m') t = None

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wset (redT_upd_\<epsilon> s t x' m') t = None

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
from \<open>\<tau>diverge t (x', m')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau>diverge t (x', m')
[PROOF STEP]
have "\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))"
[PROOF STATE]
proof (prove)
using this:
\<tau>diverge t (x', m')

goal (1 subgoal):
 1. \<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
wset (redT_upd_\<epsilon> s t x' m') t = None
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
wset (redT_upd_\<epsilon> s t x' m') t = None
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))

goal (1 subgoal):
 1. \<exists>s s'. s = s \<and> \<tau>mredT s s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
using \<open>\<tau>diverge t (x', m')\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
wset (redT_upd_\<epsilon> s t x' m') t = None
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))
\<tau>diverge t (x', m')

goal (1 subgoal):
 1. \<exists>s s'. s = s \<and> \<tau>mredT s s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s s'. s = s \<and> \<tau>mredT s s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')

goal:
No subgoals!
[PROOF STEP]
qed