[STATEMENT]
lemma fair_aux2:
    assumes RUN: "A.is_run s"
    assumes ACQ: "t<N" "tts (s i) t=INIT" "tts (s (Suc i)) t=WAIT k"
    assumes HOLD: "i<j" "tts (s j) t = HOLD k"
    assumes WAIT: "t'<N" "tts (s i) t' = WAIT k'"
    obtains l where "i<l" "l<j" "tts (s l) t' = HOLD k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret A: run as\<^sub>0 alstep s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DF_System.run as\<^sub>0 alstep s
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from ACQ WAIT
[PROOF STATE]
proof (chain)
picking this:
t < N
tts (s i) t = INIT
tts (s (Suc i)) t = WAIT k
t' < N
tts (s i) t' = WAIT k'
[PROOF STEP]
have [simp]: "t\<noteq>t'" "t'\<noteq>t"
[PROOF STATE]
proof (prove)
using this:
t < N
tts (s i) t = INIT
tts (s (Suc i)) t = WAIT k
t' < N
tts (s i) t' = WAIT k'

goal (1 subgoal):
 1. t \<noteq> t' &&& t' \<noteq> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<noteq> t'
t' \<noteq> t

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from ACQ
[PROOF STATE]
proof (chain)
picking this:
t < N
tts (s i) t = INIT
tts (s (Suc i)) t = WAIT k
[PROOF STEP]
have [simp]:
      "nn (s i) = k \<and> nn (s (Suc i)) = Suc k
    \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t:=WAIT k)"
[PROOF STATE]
proof (prove)
using this:
t < N
tts (s i) t = INIT
tts (s (Suc i)) t = WAIT k

goal (1 subgoal):
 1. nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
[PROOF STEP]
apply (rule_tac A.stepE[of i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>t < N; tts (s i) t = INIT; tts (s (Suc i)) t = WAIT k; alstep l (s i) (s (Suc i))\<rbrakk> \<Longrightarrow> nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
[PROOF STEP]
apply (erule alstep.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l c n ts c' n' s'. \<lbrakk>t < N; tts (s i) t = INIT; tts (s (Suc i)) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(l := s')); l < N; astep_sng (c, n, ts l) (c', n', s')\<rbrakk> \<Longrightarrow> nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
[PROOF STEP]
apply (erule astep_sng.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>l c n ts c' n' s' ca na. \<lbrakk>t < N; tts (s i) t = INIT; tts (s (Suc i)) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(l := s')); l < N; (c, n, ts l) = (ca, na, INIT); (c', n', s') = (ca, na + 1, WAIT na)\<rbrakk> \<Longrightarrow> nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
 2. \<And>l c n ts c' n' s' ca ka na. \<lbrakk>t < N; tts (s i) t = INIT; tts (s (Suc i)) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(l := s')); l < N; (c, n, ts l) = (ca, na, WAIT ka); (c', n', s') = (ca, na, WAIT ka); ca \<noteq> ka\<rbrakk> \<Longrightarrow> nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
 3. \<And>l c n ts c' n' s' ca na. \<lbrakk>t < N; tts (s i) t = INIT; tts (s (Suc i)) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(l := s')); l < N; (c, n, ts l) = (ca, na, WAIT ca); (c', n', s') = (ca, na, HOLD ca)\<rbrakk> \<Longrightarrow> nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
 4. \<And>l c n ts c' n' s' ca na ka. \<lbrakk>t < N; tts (s i) t = INIT; tts (s (Suc i)) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(l := s')); l < N; (c, n, ts l) = (ca, na, HOLD ka); (c', n', s') = (ca, na, REL ka)\<rbrakk> \<Longrightarrow> nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
 5. \<And>l c n ts c' n' s' ca na ka. \<lbrakk>t < N; tts (s i) t = INIT; tts (s (Suc i)) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(l := s')); l < N; (c, n, ts l) = (ca, na, REL ka); (c', n', s') = (ka + 1, na, INIT)\<rbrakk> \<Longrightarrow> nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)
[PROOF STEP]
by (auto simp: nth_list_update split: if_splits)
[PROOF STATE]
proof (state)
this:
nn (s i) = k \<and> nn (s (Suc i)) = Suc k \<and> cc (s (Suc i)) = cc (s i) \<and> tts (s (Suc i)) = (tts (s i))(t := WAIT k)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from A.run_invar[OF is_invar1, of i]
[PROOF STATE]
proof (chain)
picking this:
invar1 (s i)
[PROOF STEP]
have "invar1 (s i)"
[PROOF STATE]
proof (prove)
using this:
invar1 (s i)

goal (1 subgoal):
 1. invar1 (s i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar1 (s i)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note I1 = this[unfolded invar1_def, unfolded s_case_expand, simplified]
[PROOF STATE]
proof (state)
this:
cc (s i) \<le> k \<and> (\<forall>t ka. t < N \<and> has_ticket (tts (s i) t) ka \<longrightarrow> cc (s i) \<le> ka \<and> ka < k \<and> (\<forall>t' k'. t' < N \<and> has_ticket (tts (s i) t') k' \<and> t \<noteq> t' \<longrightarrow> ka \<noteq> k') \<and> (\<forall>k. k \<noteq> cc (s i) \<longrightarrow> \<not> locks_ticket (tts (s i) t) k))

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from WAIT I1
[PROOF STATE]
proof (chain)
picking this:
t' < N
tts (s i) t' = WAIT k'
cc (s i) \<le> k \<and> (\<forall>t ka. t < N \<and> has_ticket (tts (s i) t) ka \<longrightarrow> cc (s i) \<le> ka \<and> ka < k \<and> (\<forall>t' k'. t' < N \<and> has_ticket (tts (s i) t') k' \<and> t \<noteq> t' \<longrightarrow> ka \<noteq> k') \<and> (\<forall>k. k \<noteq> cc (s i) \<longrightarrow> \<not> locks_ticket (tts (s i) t) k))
[PROOF STEP]
have "k' < k"
[PROOF STATE]
proof (prove)
using this:
t' < N
tts (s i) t' = WAIT k'
cc (s i) \<le> k \<and> (\<forall>t ka. t < N \<and> has_ticket (tts (s i) t) ka \<longrightarrow> cc (s i) \<le> ka \<and> ka < k \<and> (\<forall>t' k'. t' < N \<and> has_ticket (tts (s i) t') k' \<and> t \<noteq> t' \<longrightarrow> ka \<noteq> k') \<and> (\<forall>k. k \<noteq> cc (s i) \<longrightarrow> \<not> locks_ticket (tts (s i) t) k))

goal (1 subgoal):
 1. k' < k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
k' < k

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from ACQ HOLD
[PROOF STATE]
proof (chain)
picking this:
t < N
tts (s i) t = INIT
tts (s (Suc i)) t = WAIT k
i < j
tts (s j) t = HOLD k
[PROOF STEP]
have "Suc i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
t < N
tts (s i) t = INIT
tts (s (Suc i)) t = WAIT k
i < j
tts (s j) t = HOLD k

goal (1 subgoal):
 1. Suc i \<noteq> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i \<noteq> j

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with HOLD
[PROOF STATE]
proof (chain)
picking this:
i < j
tts (s j) t = HOLD k
Suc i \<noteq> j
[PROOF STEP]
have "Suc i < j"
[PROOF STATE]
proof (prove)
using this:
i < j
tts (s j) t = HOLD k
Suc i \<noteq> j

goal (1 subgoal):
 1. Suc i < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i < j

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have X1: "cc (s i) \<le> k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cc (s i) \<le> k'
[PROOF STEP]
using I1 WAIT
[PROOF STATE]
proof (prove)
using this:
cc (s i) \<le> k \<and> (\<forall>t ka. t < N \<and> has_ticket (tts (s i) t) ka \<longrightarrow> cc (s i) \<le> ka \<and> ka < k \<and> (\<forall>t' k'. t' < N \<and> has_ticket (tts (s i) t') k' \<and> t \<noteq> t' \<longrightarrow> ka \<noteq> k') \<and> (\<forall>k. k \<noteq> cc (s i) \<longrightarrow> \<not> locks_ticket (tts (s i) t) k))
t' < N
tts (s i) t' = WAIT k'

goal (1 subgoal):
 1. cc (s i) \<le> k'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
cc (s i) \<le> k'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have X2: "k' < cc (s j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < cc (s j)
[PROOF STEP]
using A.run_invar[OF is_invar1, of j, unfolded invar1_def s_case_expand]
[PROOF STATE]
proof (prove)
using this:
cc (s j) \<le> nn (s j) \<and> (\<forall>t k. t < N \<and> has_ticket (tts (s j) t) k \<longrightarrow> cc (s j) \<le> k \<and> k < nn (s j) \<and> (\<forall>t' k'. t' < N \<and> has_ticket (tts (s j) t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> cc (s j) \<longrightarrow> \<not> locks_ticket (tts (s j) t) k))

goal (1 subgoal):
 1. k' < cc (s j)
[PROOF STEP]
using \<open>k' < k\<close> \<open>t<N\<close> HOLD(2)
[PROOF STATE]
proof (prove)
using this:
cc (s j) \<le> nn (s j) \<and> (\<forall>t k. t < N \<and> has_ticket (tts (s j) t) k \<longrightarrow> cc (s j) \<le> k \<and> k < nn (s j) \<and> (\<forall>t' k'. t' < N \<and> has_ticket (tts (s j) t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> cc (s j) \<longrightarrow> \<not> locks_ticket (tts (s j) t) k))
k' < k
t < N
tts (s j) t = HOLD k

goal (1 subgoal):
 1. k' < cc (s j)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k' < k; t < N; tts (s j) t = HOLD k; cc (s j) \<le> nn (s j); \<forall>t k. t < N \<and> has_ticket (tts (s j) t) k \<longrightarrow> cc (s j) \<le> k \<and> k < nn (s j) \<and> (\<forall>t' k'. t' < N \<and> has_ticket (tts (s j) t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> cc (s j) \<longrightarrow> \<not> locks_ticket (tts (s j) t) k)\<rbrakk> \<Longrightarrow> k' < cc (s j)
[PROOF STEP]
by (metis locks_ticket_simps(3) has_ticket_simps(3))
[PROOF STATE]
proof (state)
this:
k' < cc (s j)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from fair_aux[OF RUN \<open>Suc i < j\<close>, of k' t', simplified]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>cc (s i) \<le> k'; k' < cc (s j); t' < N; tts (s i) t' = WAIT k'\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t' = HOLD k'
[PROOF STEP]
obtain l where
      "l\<ge>Suc i" "l<j" "tts (s l) t' = HOLD k'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cc (s i) \<le> k'; k' < cc (s j); t' < N; tts (s i) t' = WAIT k'\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t' = HOLD k'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>Suc i \<le> l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using WAIT X1 X2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cc (s i) \<le> k'; k' < cc (s j); t' < N; tts (s i) t' = WAIT k'\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t' = HOLD k'
t' < N
tts (s i) t' = WAIT k'
cc (s i) \<le> k'
k' < cc (s j)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>Suc i \<le> l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i \<le> l
l < j
tts (s l) t' = HOLD k'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc i \<le> l
l < j
tts (s l) t' = HOLD k'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (rule_tac that[of l])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Suc i \<le> l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> i < l
 2. \<lbrakk>Suc i \<le> l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> l < j
 3. \<lbrakk>Suc i \<le> l; l < j; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> tts (s l) t' = HOLD k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_hold_position:
    assumes RUN: "A.is_run s"
    assumes WAIT: "t<N" "tts (s i) t = WAIT tk"
    assumes NWAIT: "i<j" "tts (s j) t \<noteq> WAIT tk"
    obtains l where "i<l" "l\<le>j" "tts (s l) t = HOLD tk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l \<le> j; tts (s l) t = HOLD tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l \<le> j; tts (s l) t = HOLD tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret A: run as\<^sub>0 alstep s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DF_System.run as\<^sub>0 alstep s
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l \<le> j; tts (s l) t = HOLD tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from WAIT(2) NWAIT
[PROOF STATE]
proof (chain)
picking this:
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk
[PROOF STEP]
have "\<exists>l. i<l \<and> l\<le>j \<and> tts (s l) t = HOLD tk"
[PROOF STATE]
proof (prove)
using this:
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk

goal (1 subgoal):
 1. \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
proof (induction "j-i" arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 2. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = j - i
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk

goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 2. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = j - i
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 = j - i
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk

goal (1 subgoal):
 1. \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
case (Suc i')
[PROOF STATE]
proof (state)
this:
\<lbrakk>i' = j - ?i; tts (s ?i) t = WAIT tk; ?i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>?i. l \<le> j \<and> tts (s l) t = HOLD tk
Suc i' = j - i
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
hence [simp]: "i'=j - Suc i"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i' = j - ?i; tts (s ?i) t = WAIT tk; ?i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>?i. l \<le> j \<and> tts (s l) t = HOLD tk
Suc i' = j - i
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk

goal (1 subgoal):
 1. i' = j - Suc i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' = j - Suc i

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
note IH=Suc.hyps(1)[OF this]
[PROOF STATE]
proof (state)
this:
\<lbrakk>tts (s (Suc i)) t = WAIT tk; Suc i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
obtain t' where "alstep t' (s i) (s (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t'. alstep t' (s i) (s (Suc i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule A.stepE)
[PROOF STATE]
proof (state)
this:
alstep t' (s i) (s (Suc i))

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk; Suc x = j - i; tts (s i) t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alstep t' (s i) (s (Suc i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
alstep t' (s i) (s (Suc i))

goal (1 subgoal):
 1. \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alstep t' (s i) (s (Suc i)) \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (cases "t=t'";erule alstep.cases; erule astep_sng.cases)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>c n ts c' n' s' ca na. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, INIT); (c', n', s') = (ca, na + 1, WAIT na)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 2. \<And>c n ts c' n' s' ca k na. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, WAIT k); (c', n', s') = (ca, na, WAIT k); ca \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 3. \<And>c n ts c' n' s' ca na. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, WAIT ca); (c', n', s') = (ca, na, HOLD ca)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 4. \<And>c n ts c' n' s' ca na k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, HOLD k); (c', n', s') = (ca, na, REL k)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 5. \<And>c n ts c' n' s' ca na k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, REL k); (c', n', s') = (k + 1, na, INIT)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 6. \<And>c n ts c' n' s' ca na. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, INIT); (c', n', s') = (ca, na + 1, WAIT na)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 7. \<And>c n ts c' n' s' ca k na. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, WAIT k); (c', n', s') = (ca, na, WAIT k); ca \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 8. \<And>c n ts c' n' s' ca na. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, WAIT ca); (c', n', s') = (ca, na, HOLD ca)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 9. \<And>c n ts c' n' s' ca na k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, HOLD k); (c', n', s') = (ca, na, REL k)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 10. \<And>c n ts c' n' s' ca na k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; (c, n, ts t') = (ca, na, REL k); (c', n', s') = (k + 1, na, INIT)\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>c n ts. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, Suc n, ts(t' := WAIT n)); t' < N; ts t' = INIT\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 2. \<And>c n ts k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT k)); t' < N; ts t' = WAIT k; c \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 3. \<And>c n ts. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 4. \<And>c n ts k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 5. \<And>c n ts k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 6. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, Suc n, ts(t' := WAIT n)); t' < N; ts t' = INIT\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 7. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT k)); t' < N; ts t' = WAIT k; c \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 8. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 9. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 10. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
using IH Suc.prems Suc.hyps(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tts (s (Suc i)) t = WAIT tk; Suc i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk
tts (s i) t = WAIT tk
i < j
tts (s j) t \<noteq> WAIT tk
Suc i' = j - i

goal (10 subgoals):
 1. \<And>c n ts. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, Suc n, ts(t' := WAIT n)); t' < N; ts t' = INIT\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 2. \<And>c n ts k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT k)); t' < N; ts t' = WAIT k; c \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 3. \<And>c n ts. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 4. \<And>c n ts k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 5. \<And>c n ts k. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 6. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, Suc n, ts(t' := WAIT n)); t' < N; ts t' = INIT\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 7. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT k)); t' < N; ts t' = WAIT k; c \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 8. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 9. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 10. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>c n ts. \<lbrakk>t = t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT tk)); t' < N; ts t' = WAIT tk; c \<noteq> tk; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t' = HOLD tk; i < j; tts (s j) t' \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t' = HOLD tk
 2. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, Suc n, ts(t' := WAIT n)); t' < N; ts t' = INIT; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 3. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT k)); t' < N; ts t' = WAIT k; c \<noteq> k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 4. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 5. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 6. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (metis Suc_lessD Suc_lessI fun_upd_same snd_conv)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, Suc n, ts(t' := WAIT n)); t' < N; ts t' = INIT; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 2. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT k)); t' < N; ts t' = WAIT k; c \<noteq> k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 3. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 4. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 5. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (metis Suc_lessD Suc_lessI fun_upd_other snd_conv)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := WAIT k)); t' < N; ts t' = WAIT k; c \<noteq> k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 2. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 3. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 4. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (metis Suc.prems(1) Suc_lessD Suc_lessI fun_upd_triv)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c n ts. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := HOLD c)); t' < N; ts t' = WAIT c; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 2. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 3. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (metis Suc_lessD Suc_lessI fun_upd_other snd_conv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (c, n, ts(t' := REL k)); t' < N; ts t' = HOLD k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
 2. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (metis Suc_lessD Suc_lessI fun_upd_other snd_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c n ts k. \<lbrakk>t \<noteq> t'; s i = (c, n, ts); s (Suc i) = (Suc k, n, ts(t' := INIT)); t' < N; ts t' = REL k; Suc i < j \<Longrightarrow> \<exists>l>Suc i. l \<le> j \<and> tts (s l) t = HOLD tk; ts t = WAIT tk; i < j; tts (s j) t \<noteq> WAIT tk\<rbrakk> \<Longrightarrow> \<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
[PROOF STEP]
apply (metis Suc_lessD Suc_lessI fun_upd_other snd_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l \<le> j; tts (s l) t = HOLD tk\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<exists>l>i. l \<le> j \<and> tts (s l) t = HOLD tk
\<lbrakk>i < ?l; ?l \<le> j; tts (s ?l) t = HOLD tk\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem fair:
    assumes RUN: "A.is_run s"
    assumes ACQ: "t<N" "tts (s i) t=INIT" "is_WAIT (tts (s (Suc i)) t)"
      \<comment> \<open>Thread \<open>t\<close> calls \<open>acquire\<close> in step \<open>i\<close>\<close>
    assumes HOLD: "i<j" "is_HOLD (tts (s j) t)"
      \<comment> \<open>Thread \<open>t\<close> holds lock in step \<open>j\<close>\<close>
    assumes WAIT: "t'<N" "is_WAIT (tts (s i) t')"
      \<comment> \<open>Thread \<open>t'\<close> waits for lock at step \<open>i\<close>\<close>
    obtains l where "i<l" "l<j" "is_HOLD (tts (s l) t')"
      \<comment> \<open>Then, \<open>t'\<close> gets lock earlier\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain k where Wk: "tts (s (Suc i)) t = WAIT k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. tts (s (Suc i)) t = WAIT k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ACQ
[PROOF STATE]
proof (prove)
using this:
t < N
tts (s i) t = INIT
is_WAIT (tts (s (Suc i)) t)

goal (1 subgoal):
 1. (\<And>k. tts (s (Suc i)) t = WAIT k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "tts (s (Suc i)) t") auto
[PROOF STATE]
proof (state)
this:
tts (s (Suc i)) t = WAIT k

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain k' where Wk': "tts (s i) t' = WAIT k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. tts (s i) t' = WAIT k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using WAIT
[PROOF STATE]
proof (prove)
using this:
t' < N
is_WAIT (tts (s i) t')

goal (1 subgoal):
 1. (\<And>k'. tts (s i) t' = WAIT k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "tts (s i) t'") auto
[PROOF STATE]
proof (state)
this:
tts (s i) t' = WAIT k'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from ACQ HOLD
[PROOF STATE]
proof (chain)
picking this:
t < N
tts (s i) t = INIT
is_WAIT (tts (s (Suc i)) t)
i < j
is_HOLD (tts (s j) t)
[PROOF STEP]
have "Suc i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
t < N
tts (s i) t = INIT
is_WAIT (tts (s (Suc i)) t)
i < j
is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. Suc i \<noteq> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i \<noteq> j

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with HOLD
[PROOF STATE]
proof (chain)
picking this:
i < j
is_HOLD (tts (s j) t)
Suc i \<noteq> j
[PROOF STEP]
have "Suc i < j"
[PROOF STATE]
proof (prove)
using this:
i < j
is_HOLD (tts (s j) t)
Suc i \<noteq> j

goal (1 subgoal):
 1. Suc i < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i < j

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain j' where H': "Suc i < j'" "j' \<le> j" "tts (s j') t = HOLD k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>Suc i < j'; j' \<le> j; tts (s j') t = HOLD k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule find_hold_position[OF RUN \<open>t<N\<close> Wk \<open>Suc i < j\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>j'. \<lbrakk>Suc i < j'; j' \<le> j; tts (s j') t = HOLD k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> tts (s j) t \<noteq> WAIT k
 2. \<And>l. \<lbrakk>\<And>j'. \<lbrakk>Suc i < j'; j' \<le> j; tts (s j') t = HOLD k\<rbrakk> \<Longrightarrow> thesis; Suc i < l; l \<le> j; tts (s l) t = HOLD k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using HOLD(2)
[PROOF STATE]
proof (prove)
using this:
is_HOLD (tts (s j) t)

goal (2 subgoals):
 1. (\<And>j'. \<lbrakk>Suc i < j'; j' \<le> j; tts (s j') t = HOLD k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> tts (s j) t \<noteq> WAIT k
 2. \<And>l. \<lbrakk>\<And>j'. \<lbrakk>Suc i < j'; j' \<le> j; tts (s j') t = HOLD k\<rbrakk> \<Longrightarrow> thesis; Suc i < l; l \<le> j; tts (s l) t = HOLD k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i < j'
j' \<le> j
tts (s j') t = HOLD k

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>i < l; l < j; is_HOLD (tts (s l) t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (rule fair_aux2[OF RUN ACQ(1,2) Wk _ H'(3) WAIT(1) Wk'])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < j'
 2. \<And>l. \<lbrakk>i < l; l < j'; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j'
[PROOF STEP]
using H'(1)
[PROOF STATE]
proof (prove)
using this:
Suc i < j'

goal (1 subgoal):
 1. i < j'
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>i < l; l < j'; tts (s l) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < l_; l_ < j'; tts (s l_) t' = HOLD k'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule that)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>l_ < j'; tts (s l_) t' = HOLD k'\<rbrakk> \<Longrightarrow> l_ < j
 2. \<lbrakk>l_ < j'; tts (s l_) t' = HOLD k'\<rbrakk> \<Longrightarrow> is_HOLD (tts (s l_) t')
[PROOF STEP]
using H'(2)
[PROOF STATE]
proof (prove)
using this:
j' \<le> j

goal (2 subgoals):
 1. \<lbrakk>l_ < j'; tts (s l_) t' = HOLD k'\<rbrakk> \<Longrightarrow> l_ < j
 2. \<lbrakk>l_ < j'; tts (s l_) t' = HOLD k'\<rbrakk> \<Longrightarrow> is_HOLD (tts (s l_) t')
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_invar2: "A.is_invar invar2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.is_invar invar2
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invar2 as\<^sub>0
 2. \<And>s s'. \<lbrakk>A.reachable s; invar2 s; A.step s s'\<rbrakk> \<Longrightarrow> invar2 s'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2 as\<^sub>0
[PROOF STEP]
by (auto simp: invar2_def as\<^sub>0_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>A.reachable s; invar2 s; A.step s s'\<rbrakk> \<Longrightarrow> invar2 s'
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable s; invar2 s; A.step s s'\<rbrakk> \<Longrightarrow> invar2 s'
[PROOF STEP]
apply (clarsimp simp: invar2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a b x aa ba l k. \<lbrakk>A.reachable (x, aa, ba); s' = (c, a, b); \<forall>k. x \<le> k \<and> k < aa \<longrightarrow> (\<exists>t<N. has_ticket (ba t) k); s = (x, aa, ba); alstep l (x, aa, ba) (c, a, b); c \<le> k; k < a\<rbrakk> \<Longrightarrow> \<exists>t<N. has_ticket (b t) k
[PROOF STEP]
apply (erule alstep.cases; erule astep_sng.cases; clarsimp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c aa l k ts. \<lbrakk>A.reachable (c, aa, ts); s' = (c, Suc aa, ts(l := WAIT aa)); \<forall>k. c \<le> k \<and> k < aa \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, aa, ts); c \<le> k; k < Suc aa; l < N; ts l = INIT\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = aa) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 2. \<And>c a l k ts ka. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := WAIT ka)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = WAIT ka; c \<noteq> ka\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = ka) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 3. \<And>c a l k ts. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := HOLD c)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = WAIT c\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = c) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 4. \<And>c a l k ts ka. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := REL ka)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = HOLD ka\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = ka) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 5. \<And>a x l k ts ka. \<lbrakk>A.reachable (x, a, ts); s' = (Suc ka, a, ts(l := INIT)); \<forall>k. x \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (x, a, ts); Suc ka \<le> k; k < a; l < N; ts l = REL ka\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l \<and> t < N \<and> has_ticket (ts t) k
[PROOF STEP]
apply (metis less_antisym has_ticket_simps(1))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c a l k ts ka. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := WAIT ka)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = WAIT ka; c \<noteq> ka\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = ka) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 2. \<And>c a l k ts. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := HOLD c)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = WAIT c\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = c) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 3. \<And>c a l k ts ka. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := REL ka)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = HOLD ka\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = ka) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 4. \<And>a x l k ts ka. \<lbrakk>A.reachable (x, a, ts); s' = (Suc ka, a, ts(l := INIT)); \<forall>k. x \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (x, a, ts); Suc ka \<le> k; k < a; l < N; ts l = REL ka\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l \<and> t < N \<and> has_ticket (ts t) k
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (c_, a_, ts_); s' = (c_, a_, ts_(l_ := WAIT ka_)); \<forall>k. c_ \<le> k \<and> k < a_ \<longrightarrow> (\<exists>t<N. has_ticket (ts_ t) k); s = (c_, a_, ts_); c_ \<le> k_; k_ < a_; l_ < N; ts_ l_ = WAIT ka_; c_ \<noteq> ka_\<rbrakk> \<Longrightarrow> \<exists>t. (t = l_ \<longrightarrow> k_ = ka_) \<and> (t \<noteq> l_ \<longrightarrow> t < N \<and> has_ticket (ts_ t) k_)
[PROOF STEP]
by (metis has_ticket_simps(2))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c a l k ts. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := HOLD c)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = WAIT c\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = c) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 2. \<And>c a l k ts ka. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := REL ka)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = HOLD ka\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = ka) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 3. \<And>a x l k ts ka. \<lbrakk>A.reachable (x, a, ts); s' = (Suc ka, a, ts(l := INIT)); \<forall>k. x \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (x, a, ts); Suc ka \<le> k; k < a; l < N; ts l = REL ka\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l \<and> t < N \<and> has_ticket (ts t) k
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (c_, a_, ts_); s' = (c_, a_, ts_(l_ := HOLD c_)); \<forall>k. c_ \<le> k \<and> k < a_ \<longrightarrow> (\<exists>t<N. has_ticket (ts_ t) k); s = (c_, a_, ts_); c_ \<le> k_; k_ < a_; l_ < N; ts_ l_ = WAIT c_\<rbrakk> \<Longrightarrow> \<exists>t. (t = l_ \<longrightarrow> k_ = c_) \<and> (t \<noteq> l_ \<longrightarrow> t < N \<and> has_ticket (ts_ t) k_)
[PROOF STEP]
by (metis has_ticket_simps(2))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c a l k ts ka. \<lbrakk>A.reachable (c, a, ts); s' = (c, a, ts(l := REL ka)); \<forall>k. c \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (c, a, ts); c \<le> k; k < a; l < N; ts l = HOLD ka\<rbrakk> \<Longrightarrow> \<exists>t. (t = l \<longrightarrow> k = ka) \<and> (t \<noteq> l \<longrightarrow> t < N \<and> has_ticket (ts t) k)
 2. \<And>a x l k ts ka. \<lbrakk>A.reachable (x, a, ts); s' = (Suc ka, a, ts(l := INIT)); \<forall>k. x \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (x, a, ts); Suc ka \<le> k; k < a; l < N; ts l = REL ka\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l \<and> t < N \<and> has_ticket (ts t) k
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (c_, a_, ts_); s' = (c_, a_, ts_(l_ := REL ka_)); \<forall>k. c_ \<le> k \<and> k < a_ \<longrightarrow> (\<exists>t<N. has_ticket (ts_ t) k); s = (c_, a_, ts_); c_ \<le> k_; k_ < a_; l_ < N; ts_ l_ = HOLD ka_\<rbrakk> \<Longrightarrow> \<exists>t. (t = l_ \<longrightarrow> k_ = ka_) \<and> (t \<noteq> l_ \<longrightarrow> t < N \<and> has_ticket (ts_ t) k_)
[PROOF STEP]
by (metis has_ticket_simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x l k ts ka. \<lbrakk>A.reachable (x, a, ts); s' = (Suc ka, a, ts(l := INIT)); \<forall>k. x \<le> k \<and> k < a \<longrightarrow> (\<exists>t<N. has_ticket (ts t) k); s = (x, a, ts); Suc ka \<le> k; k < a; l < N; ts l = REL ka\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l \<and> t < N \<and> has_ticket (ts t) k
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (x_, a_, ts_); s' = (Suc ka_, a_, ts_(l_ := INIT)); \<forall>k. x_ \<le> k \<and> k < a_ \<longrightarrow> (\<exists>t<N. has_ticket (ts_ t) k); s = (x_, a_, ts_); Suc ka_ \<le> k_; k_ < a_; l_ < N; ts_ l_ = REL ka_\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l_ \<and> t < N \<and> has_ticket (ts_ t) k_
[PROOF STEP]
apply (frule A.invar_reachable[OF is_invar1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (x_, a_, ts_); s' = (Suc ka_, a_, ts_(l_ := INIT)); \<forall>k. x_ \<le> k \<and> k < a_ \<longrightarrow> (\<exists>t<N. has_ticket (ts_ t) k); s = (x_, a_, ts_); Suc ka_ \<le> k_; k_ < a_; l_ < N; ts_ l_ = REL ka_; invar1 (x_, a_, ts_)\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l_ \<and> t < N \<and> has_ticket (ts_ t) k_
[PROOF STEP]
unfolding invar1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (x_, a_, ts_); s' = (Suc ka_, a_, ts_(l_ := INIT)); \<forall>k. x_ \<le> k \<and> k < a_ \<longrightarrow> (\<exists>t<N. has_ticket (ts_ t) k); s = (x_, a_, ts_); Suc ka_ \<le> k_; k_ < a_; l_ < N; ts_ l_ = REL ka_; case (x_, a_, ts_) of (c, n, ts) \<Rightarrow> c \<le> n \<and> (\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k))\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l_ \<and> t < N \<and> has_ticket (ts_ t) k_
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (x_, a_, ts_); s' = (Suc ka_, a_, ts_(l_ := INIT)); \<forall>k. x_ \<le> k \<and> k < a_ \<longrightarrow> (\<exists>t<N. has_ticket (ts_ t) k); s = (x_, a_, ts_); Suc ka_ \<le> k_; k_ < a_; l_ < N; ts_ l_ = REL ka_; x_ \<le> a_; \<forall>t k. t < N \<and> has_ticket (ts_ t) k \<longrightarrow> x_ \<le> k \<and> k < a_ \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts_ t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x_ \<longrightarrow> \<not> locks_ticket (ts_ t) k)\<rbrakk> \<Longrightarrow> \<exists>t. t \<noteq> l_ \<and> t < N \<and> has_ticket (ts_ t) k_
[PROOF STEP]
by (metis Suc_leD locks_ticket_simps(4)
          not_less_eq_eq has_ticket_simps(4))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma has_ticket_unique: "\<lbrakk>A.reachable (c,n,ts);
      t<N; has_ticket (ts t) k; t'<N; has_ticket (ts t') k
    \<rbrakk> \<Longrightarrow> t'=t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable (c, n, ts); t < N; has_ticket (ts t) k; t' < N; has_ticket (ts t') k\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
apply (drule A.invar_reachable[OF is_invar1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t < N; has_ticket (ts t) k; t' < N; has_ticket (ts t') k; invar1 (c, n, ts)\<rbrakk> \<Longrightarrow> t' = t
[PROOF STEP]
by (auto simp: invar1_def)


[STATEMENT]
lemma holds_only_current:
    assumes R: "A.reachable (c,n,ts)"
    assumes A: "t<N" "locks_ticket (ts t) k"
    shows "k=c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = c
[PROOF STEP]
using A.invar_reachable[OF is_invar1 R] A
[PROOF STATE]
proof (prove)
using this:
invar1 (c, n, ts)
t < N
locks_ticket (ts t) k

goal (1 subgoal):
 1. k = c
[PROOF STEP]
unfolding invar1_def
[PROOF STATE]
proof (prove)
using this:
case (c, n, ts) of (c, n, ts) \<Rightarrow> c \<le> n \<and> (\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k))
t < N
locks_ticket (ts t) k

goal (1 subgoal):
 1. k = c
[PROOF STEP]
using holds_imp_uses
[PROOF STATE]
proof (prove)
using this:
case (c, n, ts) of (c, n, ts) \<Rightarrow> c \<le> n \<and> (\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k))
t < N
locks_ticket (ts t) k
locks_ticket ?s ?k \<Longrightarrow> has_ticket ?s ?k

goal (1 subgoal):
 1. k = c
[PROOF STEP]
by blast


[STATEMENT]
theorem progress:
    assumes FRUN: "A.is_fair_run s"
    assumes A: "t<N" "is_WAIT (tts (s i) t)"
    shows "\<exists>j>i. is_HOLD (tts (s j) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
interpret A: fair_run as\<^sub>0 alstep s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fair_run as\<^sub>0 alstep s
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
t < N
is_WAIT (tts (s i) t)
[PROOF STEP]
obtain k where Wk: "tts (s i) t = WAIT k"
[PROOF STATE]
proof (prove)
using this:
t < N
is_WAIT (tts (s i) t)

goal (1 subgoal):
 1. (\<And>k. tts (s i) t = WAIT k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "tts (s i) t") auto
[PROOF STATE]
proof (state)
this:
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>We use the following induction scheme:
      \<^item> Either the current thread increases (if we reach \<open>k\<close>, we are done)
      \<^item> (lex) the thread using the current ticket makes a step
      \<^item> (lex) another thread makes a step
    \<close>
[PROOF STATE]
proof (state)
this:
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
define lrel where "lrel \<equiv>
      inv_image (measure id <*lex*> measure id <*lex*> measure id) (\<lambda>i. (
        k-cc (s i),
        tweight (tts (s i) (tkt_thread (tts (s i)) (cc (s i)))),
        A.dist_step (tkt_thread (tts (s i)) (cc (s i))) i
      ))"
[PROOF STATE]
proof (state)
this:
lrel \<equiv> inv_image (measure id <*lex*> measure id <*lex*> measure id) (\<lambda>i. (k - cc (s i), tweight (tts (s i) (tkt_thread (tts (s i)) (cc (s i)))), A.dist_step (tkt_thread (tts (s i)) (cc (s i))) i))

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
have "wf lrel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf lrel
[PROOF STEP]
unfolding lrel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (inv_image (measure id <*lex*> measure id <*lex*> measure id) (\<lambda>i. (k - cc (s i), tweight (tts (s i) (tkt_thread (tts (s i)) (cc (s i)))), A.dist_step (tkt_thread (tts (s i)) (cc (s i))) i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf lrel

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf lrel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf lrel

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
using A(1) Wk
[PROOF STATE]
proof (prove)
using this:
wf lrel
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
proof (induction i)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
case (less i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?y, i) \<in> lrel; t < N; tts (s ?y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>?y. is_HOLD (tts (s j) t)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>We name the components of this and the next state\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?y, i) \<in> lrel; t < N; tts (s ?y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>?y. is_HOLD (tts (s j) t)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
obtain c n ts where [simp]: "s i = (c,n,ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c n ts. s i = (c, n, ts) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "s i")
[PROOF STATE]
proof (state)
this:
s i = (c, n, ts)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
from A.run_reachable[of i]
[PROOF STATE]
proof (chain)
picking this:
A.reachable (s i)
[PROOF STEP]
have R: "A.reachable (c,n,ts)"
[PROOF STATE]
proof (prove)
using this:
A.reachable (s i)

goal (1 subgoal):
 1. A.reachable (c, n, ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A.reachable (c, n, ts)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
obtain c' n' ts' where [simp]: "s (Suc i) = (c',n',ts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c' n' ts'. s (Suc i) = (c', n', ts') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "s (Suc i)")
[PROOF STATE]
proof (state)
this:
s (Suc i) = (c', n', ts')

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
from A.run_reachable[of "Suc i"]
[PROOF STATE]
proof (chain)
picking this:
A.reachable (s (Suc i))
[PROOF STEP]
have R': "A.reachable (c',n',ts')"
[PROOF STATE]
proof (prove)
using this:
A.reachable (s (Suc i))

goal (1 subgoal):
 1. A.reachable (c', n', ts')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A.reachable (c', n', ts')

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
from less.prems
[PROOF STATE]
proof (chain)
picking this:
t < N
tts (s i) t = WAIT k
[PROOF STEP]
have WAIT[simp]: "ts t = WAIT k"
[PROOF STATE]
proof (prove)
using this:
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. ts t = WAIT k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ts t = WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ts t = WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>If thread \<open>t\<close> left waiting state, we are done\<close>
[PROOF STATE]
proof (state)
this:
ts t = WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
assume "ts' t \<noteq> WAIT k"
[PROOF STATE]
proof (state)
this:
ts' t \<noteq> WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
hence "ts' t = HOLD k"
[PROOF STATE]
proof (prove)
using this:
ts' t \<noteq> WAIT k

goal (1 subgoal):
 1. ts' t = HOLD k
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
ts' t \<noteq> WAIT k
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. ts' t = HOLD k
[PROOF STEP]
apply (rule_tac A.stepE[of i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>ts' t \<noteq> WAIT k; t < N; tts (s i) t = WAIT k; alstep l (s i) (s (Suc i))\<rbrakk> \<Longrightarrow> ts' t = HOLD k
[PROOF STEP]
apply (auto elim!: alstep.cases astep_sng.cases split: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ts' t = HOLD k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
hence ?case
[PROOF STATE]
proof (prove)
using this:
ts' t = HOLD k

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ts' t \<noteq> WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ts' t \<noteq> WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ts' t \<noteq> WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
assume [simp]: "ts' t = WAIT k"
[PROOF STATE]
proof (state)
this:
ts' t = WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>Otherwise, we obtain the thread \<open>tt\<close> that holds the current lock\<close>
[PROOF STATE]
proof (state)
this:
ts' t = WAIT k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
obtain tt where UTT: "tt<N" "has_ticket (ts tt) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tt. \<lbrakk>tt < N; has_ticket (ts tt) c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using current_lock_used[of c n ts t k]
            and less.prems A.run_reachable[of i]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>A.reachable (c, n, ts); t < N; ts t = WAIT k; \<And>t'. \<lbrakk>t' < N; has_ticket (ts t') c\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
t < N
tts (s i) t = WAIT k
A.reachable (s i)

goal (1 subgoal):
 1. (\<And>tt. \<lbrakk>tt < N; has_ticket (ts tt) c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tt < N
has_ticket (ts tt) c

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
have [simp]: "tkt_thread ts c = tt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tkt_thread ts c = tt
[PROOF STEP]
using tkt_thread_eq[OF R UTT]
[PROOF STATE]
proof (prove)
using this:
tkt_thread ts c = tt

goal (1 subgoal):
 1. tkt_thread ts c = tt
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
tkt_thread ts c = tt

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
note [simp] = \<open>tt<N\<close>
[PROOF STATE]
proof (state)
this:
tt < N

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
have "A.can_step tt (s i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.can_step tt (s i)
[PROOF STEP]
by (simp add: never_blocked)
[PROOF STATE]
proof (state)
this:
A.can_step tt (s i)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
hence ?case
[PROOF STATE]
proof (prove)
using this:
A.can_step tt (s i)

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
proof (cases rule: A.rstep_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
case (other t') \<comment> \<open>Another thread than \<open>tt\<close> makes a step.\<close>
[PROOF STATE]
proof (state)
this:
tt \<noteq> t'
\<not> A.rstep tt s i
A.rstep t' s i
A.dist_step tt (Suc i) < A.dist_step tt i

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>The current ticket and \<open>tt\<close>'s state remain the same\<close>
[PROOF STATE]
proof (state)
this:
tt \<noteq> t'
\<not> A.rstep tt s i
A.rstep t' s i
A.dist_step tt (Suc i) < A.dist_step tt i

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
hence [simp]: "c' = c \<and> ts' tt = ts tt"
[PROOF STATE]
proof (prove)
using this:
tt \<noteq> t'
\<not> A.rstep tt s i
A.rstep t' s i
A.dist_step tt (Suc i) < A.dist_step tt i

goal (1 subgoal):
 1. c' = c \<and> ts' tt = ts tt
[PROOF STEP]
using has_ticket_unique[OF R UTT, of t']
[PROOF STATE]
proof (prove)
using this:
tt \<noteq> t'
\<not> A.rstep tt s i
A.rstep t' s i
A.dist_step tt (Suc i) < A.dist_step tt i
\<lbrakk>t' < N; has_ticket (ts t') c\<rbrakk> \<Longrightarrow> t' = tt

goal (1 subgoal):
 1. c' = c \<and> ts' tt = ts tt
[PROOF STEP]
unfolding A.rstep_def
[PROOF STATE]
proof (prove)
using this:
tt \<noteq> t'
\<not> alstep tt (s i) (s (Suc i))
alstep t' (s i) (s (Suc i))
A.dist_step tt (Suc i) < A.dist_step tt i
\<lbrakk>t' < N; has_ticket (ts t') c\<rbrakk> \<Longrightarrow> t' = tt

goal (1 subgoal):
 1. c' = c \<and> ts' tt = ts tt
[PROOF STEP]
using holds_only_current[OF R, of t']
[PROOF STATE]
proof (prove)
using this:
tt \<noteq> t'
\<not> alstep tt (s i) (s (Suc i))
alstep t' (s i) (s (Suc i))
A.dist_step tt (Suc i) < A.dist_step tt i
\<lbrakk>t' < N; has_ticket (ts t') c\<rbrakk> \<Longrightarrow> t' = tt
\<lbrakk>t' < N; locks_ticket (ts t') ?k\<rbrakk> \<Longrightarrow> ?k = c

goal (1 subgoal):
 1. c' = c \<and> ts' tt = ts tt
[PROOF STEP]
by (force elim!: alstep.cases astep_sng.cases)
[PROOF STATE]
proof (state)
this:
c' = c \<and> ts' tt = ts tt

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>Thus, \<open>tt\<close> is still using the current ticket\<close>
[PROOF STATE]
proof (state)
this:
c' = c \<and> ts' tt = ts tt

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
have [simp]: "tkt_thread ts' c = tt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tkt_thread ts' c = tt
[PROOF STEP]
using UTT tkt_thread_eq[OF R', of tt c]
[PROOF STATE]
proof (prove)
using this:
tt < N
has_ticket (ts tt) c
\<lbrakk>tt < N; has_ticket (ts' tt) c\<rbrakk> \<Longrightarrow> tkt_thread ts' c = tt

goal (1 subgoal):
 1. tkt_thread ts' c = tt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tkt_thread ts' c = tt

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>Only the distance to \<open>tt\<close>'s next step has decreased\<close>
[PROOF STATE]
proof (state)
this:
tkt_thread ts' c = tt

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
have "(Suc i, i) \<in> lrel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc i, i) \<in> lrel
[PROOF STEP]
unfolding lrel_def tweight_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc i, i) \<in> inv_image (measure id <*lex*> measure id <*lex*> measure id) (\<lambda>i. (k - cc (s i), case tts (s i) (tkt_thread (tts (s i)) (cc (s i))) of INIT \<Rightarrow> 0 | WAIT x \<Rightarrow> 3 | HOLD x \<Rightarrow> 2 | REL x \<Rightarrow> 1, A.dist_step (tkt_thread (tts (s i)) (cc (s i))) i))
[PROOF STEP]
by (simp add: other)
[PROOF STATE]
proof (state)
this:
(Suc i, i) \<in> lrel

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>And we can apply the induction hypothesis\<close>
[PROOF STATE]
proof (state)
this:
(Suc i, i) \<in> lrel

goal (2 subgoals):
 1. \<And>l'. \<lbrakk>tt \<noteq> l'; \<not> A.rstep tt s i; A.rstep l' s i; A.dist_step tt (Suc i) < A.dist_step tt i\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
with less.IH[of "Suc i"] \<open>t<N\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(Suc i, i) \<in> lrel; t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>Suc i. is_HOLD (tts (s j) t)
t < N
(Suc i, i) \<in> lrel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(Suc i, i) \<in> lrel; t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>Suc i. is_HOLD (tts (s j) t)
t < N
(Suc i, i) \<in> lrel

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>t < N; (Suc i, i) \<in> lrel; Suc i < j; is_HOLD (tts (s j) t)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
using Suc_lessD
[PROOF STATE]
proof (prove)
using this:
Suc ?m < ?n \<Longrightarrow> ?m < ?n

goal (1 subgoal):
 1. \<And>j. \<lbrakk>t < N; (Suc i, i) \<in> lrel; Suc i < j; is_HOLD (tts (s j) t)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
case THIS: this \<comment> \<open>The thread \<open>tt\<close> that uses the current ticket makes a step\<close>
[PROOF STATE]
proof (state)
this:
A.rstep tt s i

goal (1 subgoal):
 1. A.rstep tt s i \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
proof (cases "\<exists>k'. ts tt = REL k'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
case True \<comment> \<open>\<open>tt\<close> has finished releasing the lock \<close>
[PROOF STATE]
proof (state)
this:
\<exists>k'. ts tt = REL k'

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'. ts tt = REL k'
[PROOF STEP]
have [simp]: "ts tt = REL c"
[PROOF STATE]
proof (prove)
using this:
\<exists>k'. ts tt = REL k'

goal (1 subgoal):
 1. ts tt = REL c
[PROOF STEP]
using UTT
[PROOF STATE]
proof (prove)
using this:
\<exists>k'. ts tt = REL k'
tt < N
has_ticket (ts tt) c

goal (1 subgoal):
 1. ts tt = REL c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ts tt = REL c

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>Thus, current increases\<close>
[PROOF STATE]
proof (state)
this:
ts tt = REL c

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
have [simp]: "c' = Suc c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c' = Suc c
[PROOF STEP]
using THIS
[PROOF STATE]
proof (prove)
using this:
A.rstep tt s i

goal (1 subgoal):
 1. c' = Suc c
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.rstep tt s i \<Longrightarrow> c' = Suc c
[PROOF STEP]
unfolding A.rstep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alstep tt (s i) (s (Suc i)) \<Longrightarrow> c' = Suc c
[PROOF STEP]
apply (erule alstep.cases, erule astep_sng.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ca n ts c'a n' s' caa na. \<lbrakk>s i = (ca, n, ts); s (Suc i) = (c'a, n', ts(tt := s')); tt < N; (ca, n, ts tt) = (caa, na, INIT); (c'a, n', s') = (caa, na + 1, WAIT na)\<rbrakk> \<Longrightarrow> c' = Suc c
 2. \<And>ca n ts c'a n' s' caa k na. \<lbrakk>s i = (ca, n, ts); s (Suc i) = (c'a, n', ts(tt := s')); tt < N; (ca, n, ts tt) = (caa, na, WAIT k); (c'a, n', s') = (caa, na, WAIT k); caa \<noteq> k\<rbrakk> \<Longrightarrow> c' = Suc c
 3. \<And>ca n ts c'a n' s' caa na. \<lbrakk>s i = (ca, n, ts); s (Suc i) = (c'a, n', ts(tt := s')); tt < N; (ca, n, ts tt) = (caa, na, WAIT caa); (c'a, n', s') = (caa, na, HOLD caa)\<rbrakk> \<Longrightarrow> c' = Suc c
 4. \<And>ca n ts c'a n' s' caa na k. \<lbrakk>s i = (ca, n, ts); s (Suc i) = (c'a, n', ts(tt := s')); tt < N; (ca, n, ts tt) = (caa, na, HOLD k); (c'a, n', s') = (caa, na, REL k)\<rbrakk> \<Longrightarrow> c' = Suc c
 5. \<And>ca n ts c'a n' s' caa na k. \<lbrakk>s i = (ca, n, ts); s (Suc i) = (c'a, n', ts(tt := s')); tt < N; (ca, n, ts tt) = (caa, na, REL k); (c'a, n', s') = (k + 1, na, INIT)\<rbrakk> \<Longrightarrow> c' = Suc c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c' = Suc c

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>But is still less than \<open>k\<close>\<close>
[PROOF STATE]
proof (state)
this:
c' = Suc c

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
from A.invar_reachable[OF is_invar1 R]
[PROOF STATE]
proof (chain)
picking this:
invar1 (c, n, ts)
[PROOF STEP]
have "k>c"
[PROOF STATE]
proof (prove)
using this:
invar1 (c, n, ts)

goal (1 subgoal):
 1. c < k
[PROOF STEP]
apply (auto simp: invar1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> c < k
[PROOF STEP]
by (metis UTT WAIT \<open>ts tt = REL c\<close> le_neq_implies_less
                less.prems(1) thread.distinct(9) has_ticket_simps(2))
[PROOF STATE]
proof (state)
this:
c < k

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>And we can apply the induction hypothesis\<close>
[PROOF STATE]
proof (state)
this:
c < k

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
hence "(Suc i, i) \<in> lrel"
[PROOF STATE]
proof (prove)
using this:
c < k

goal (1 subgoal):
 1. (Suc i, i) \<in> lrel
[PROOF STEP]
unfolding lrel_def
[PROOF STATE]
proof (prove)
using this:
c < k

goal (1 subgoal):
 1. (Suc i, i) \<in> inv_image (measure id <*lex*> measure id <*lex*> measure id) (\<lambda>i. (k - cc (s i), tweight (tts (s i) (tkt_thread (tts (s i)) (cc (s i)))), A.dist_step (tkt_thread (tts (s i)) (cc (s i))) i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Suc i, i) \<in> lrel

goal (2 subgoals):
 1. \<exists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
 2. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
with less.IH[of "Suc i"] \<open>t<N\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(Suc i, i) \<in> lrel; t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>Suc i. is_HOLD (tts (s j) t)
t < N
(Suc i, i) \<in> lrel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(Suc i, i) \<in> lrel; t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>Suc i. is_HOLD (tts (s j) t)
t < N
(Suc i, i) \<in> lrel

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>t < N; (Suc i, i) \<in> lrel; Suc i < j; is_HOLD (tts (s j) t)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
using Suc_lessD
[PROOF STATE]
proof (prove)
using this:
Suc ?m < ?n \<Longrightarrow> ?m < ?n

goal (1 subgoal):
 1. \<And>j. \<lbrakk>t < N; (Suc i, i) \<in> lrel; Suc i < j; is_HOLD (tts (s j) t)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
case False \<comment> \<open>\<open>tt\<close> has acquired the lock, or started releasing it\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>k'. ts tt = REL k'

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>Hence, current remains the same, but the weight of \<open>tt\<close> decreases\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>k'. ts tt = REL k'

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
hence [simp]: "
              c' = c
            \<and> tweight (ts tt) > tweight (ts' tt)
            \<and> has_ticket (ts' tt) c"
[PROOF STATE]
proof (prove)
using this:
\<nexists>k'. ts tt = REL k'

goal (1 subgoal):
 1. c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
[PROOF STEP]
using THIS UTT
[PROOF STATE]
proof (prove)
using this:
\<nexists>k'. ts tt = REL k'
A.rstep tt s i
tt < N
has_ticket (ts tt) c

goal (1 subgoal):
 1. c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nexists>k'. ts tt = REL k'; A.rstep tt s i; tt < N; has_ticket (ts tt) c\<rbrakk> \<Longrightarrow> c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
[PROOF STEP]
unfolding A.rstep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nexists>k'. ts tt = REL k'; alstep tt (s i) (s (Suc i)); tt < N; has_ticket (ts tt) c\<rbrakk> \<Longrightarrow> c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
[PROOF STEP]
apply (erule alstep.cases, erule astep_sng.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ca n tsa c'a n' s' caa na. \<lbrakk>\<nexists>k'. ts tt = REL k'; tt < N; has_ticket (ts tt) c; s i = (ca, n, tsa); s (Suc i) = (c'a, n', tsa(tt := s')); tt < N; (ca, n, tsa tt) = (caa, na, INIT); (c'a, n', s') = (caa, na + 1, WAIT na)\<rbrakk> \<Longrightarrow> c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
 2. \<And>ca n tsa c'a n' s' caa k na. \<lbrakk>\<nexists>k'. ts tt = REL k'; tt < N; has_ticket (ts tt) c; s i = (ca, n, tsa); s (Suc i) = (c'a, n', tsa(tt := s')); tt < N; (ca, n, tsa tt) = (caa, na, WAIT k); (c'a, n', s') = (caa, na, WAIT k); caa \<noteq> k\<rbrakk> \<Longrightarrow> c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
 3. \<And>ca n tsa c'a n' s' caa na. \<lbrakk>\<nexists>k'. ts tt = REL k'; tt < N; has_ticket (ts tt) c; s i = (ca, n, tsa); s (Suc i) = (c'a, n', tsa(tt := s')); tt < N; (ca, n, tsa tt) = (caa, na, WAIT caa); (c'a, n', s') = (caa, na, HOLD caa)\<rbrakk> \<Longrightarrow> c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
 4. \<And>ca n tsa c'a n' s' caa na k. \<lbrakk>\<nexists>k'. ts tt = REL k'; tt < N; has_ticket (ts tt) c; s i = (ca, n, tsa); s (Suc i) = (c'a, n', tsa(tt := s')); tt < N; (ca, n, tsa tt) = (caa, na, HOLD k); (c'a, n', s') = (caa, na, REL k)\<rbrakk> \<Longrightarrow> c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
 5. \<And>ca n tsa c'a n' s' caa na k. \<lbrakk>\<nexists>k'. ts tt = REL k'; tt < N; has_ticket (ts tt) c; s i = (ca, n, tsa); s (Suc i) = (c'a, n', tsa(tt := s')); tt < N; (ca, n, tsa tt) = (caa, na, REL k); (c'a, n', s') = (k + 1, na, INIT)\<rbrakk> \<Longrightarrow> c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c
[PROOF STEP]
by (auto simp: has_ticket_def tweight_def)
[PROOF STATE]
proof (state)
this:
c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>\<open>tt\<close> still holds the current lock\<close>
[PROOF STATE]
proof (state)
this:
c' = c \<and> tweight (ts' tt) < tweight (ts tt) \<and> has_ticket (ts' tt) c

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
have [simp]: "tkt_thread ts' c = tt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tkt_thread ts' c = tt
[PROOF STEP]
using tkt_thread_eq[OF R' \<open>tt<N\<close>, of c]
[PROOF STATE]
proof (prove)
using this:
has_ticket (ts' tt) c \<Longrightarrow> tkt_thread ts' c = tt

goal (1 subgoal):
 1. tkt_thread ts' c = tt
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tkt_thread ts' c = tt

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
text \<open>And we can apply the IH\<close>
[PROOF STATE]
proof (state)
this:
tkt_thread ts' c = tt

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
have "(Suc i, i) \<in> lrel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc i, i) \<in> lrel
[PROOF STEP]
unfolding lrel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc i, i) \<in> inv_image (measure id <*lex*> measure id <*lex*> measure id) (\<lambda>i. (k - cc (s i), tweight (tts (s i) (tkt_thread (tts (s i)) (cc (s i)))), A.dist_step (tkt_thread (tts (s i)) (cc (s i))) i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Suc i, i) \<in> lrel

goal (1 subgoal):
 1. \<nexists>k'. ts tt = REL k' \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
with less.IH[of "Suc i"] \<open>t<N\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(Suc i, i) \<in> lrel; t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>Suc i. is_HOLD (tts (s j) t)
t < N
(Suc i, i) \<in> lrel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(Suc i, i) \<in> lrel; t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>Suc i. is_HOLD (tts (s j) t)
t < N
(Suc i, i) \<in> lrel

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>t < N; (Suc i, i) \<in> lrel; Suc i < j; is_HOLD (tts (s j) t)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
using Suc_lessD
[PROOF STATE]
proof (prove)
using this:
Suc ?m < ?n \<Longrightarrow> ?m < ?n

goal (1 subgoal):
 1. \<And>j. \<lbrakk>t < N; (Suc i, i) \<in> lrel; Suc i < j; is_HOLD (tts (s j) t)\<rbrakk> \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ts' t = WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> lrel; t < N; tts (s y) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>y. is_HOLD (tts (s j) t); t < N; tts (s x) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>j>x. is_HOLD (tts (s j) t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ts' t \<noteq> WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
ts' t = WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts' t \<noteq> WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)
ts' t = WAIT k \<Longrightarrow> \<exists>j>i. is_HOLD (tts (s j) t)

goal (1 subgoal):
 1. \<exists>j>i. is_HOLD (tts (s j) t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j>i. is_HOLD (tts (s j) t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma k_gt0[simp]: "0<k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
by (cases k) auto


[STATEMENT]
lemma b_never_blocked: "B.can_step l s \<longleftrightarrow> l<N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B.can_step l s = (l < N)
[PROOF STEP]
apply (cases s; cases "tts s l"; simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>s = (a, b, c); c l = INIT\<rbrakk> \<Longrightarrow> B.can_step l (a, b, c) = (l < N)
 2. \<And>a b c x2. \<lbrakk>s = (a, b, c); c l = WAIT x2\<rbrakk> \<Longrightarrow> B.can_step l (a, b, c) = (l < N)
 3. \<And>a b c x3. \<lbrakk>s = (a, b, c); c l = HOLD x3\<rbrakk> \<Longrightarrow> B.can_step l (a, b, c) = (l < N)
 4. \<And>a b c x4. \<lbrakk>s = (a, b, c); c l = REL x4\<rbrakk> \<Longrightarrow> B.can_step l (a, b, c) = (l < N)
[PROOF STEP]
unfolding B.can_step_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>s = (a, b, c); c l = INIT\<rbrakk> \<Longrightarrow> (\<exists>s'. blstep l (a, b, c) s') = (l < N)
 2. \<And>a b c x2. \<lbrakk>s = (a, b, c); c l = WAIT x2\<rbrakk> \<Longrightarrow> (\<exists>s'. blstep l (a, b, c) s') = (l < N)
 3. \<And>a b c x3. \<lbrakk>s = (a, b, c); c l = HOLD x3\<rbrakk> \<Longrightarrow> (\<exists>s'. blstep l (a, b, c) s') = (l < N)
 4. \<And>a b c x4. \<lbrakk>s = (a, b, c); c l = REL x4\<rbrakk> \<Longrightarrow> (\<exists>s'. blstep l (a, b, c) s') = (l < N)
[PROOF STEP]
apply (clarsimp simp: blstep.simps bstep_sng.simps; blast)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nat_sum_gtZ_iff[simp]:
    "finite s \<Longrightarrow> sum f s \<noteq> (0::nat) \<longleftrightarrow> (\<exists>x\<in>s. f x \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s \<Longrightarrow> (sum f s \<noteq> 0) = (\<exists>x\<in>s. f x \<noteq> 0)
[PROOF STEP]
by simp


[STATEMENT]
lemma n_eq_Suc_sub1_conv[simp]: "n = Suc (n - Suc 0) \<longleftrightarrow> n\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n = Suc (n - Suc 0)) = (n \<noteq> 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma mod_mult_mod_eq[mod_simps]: "x mod (k * N) mod N = x mod N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mod (k * N) mod N = x mod N
[PROOF STEP]
by (meson dvd_eq_mod_eq_0 mod_mod_cancel mod_mult_self2_is_0)


[STATEMENT]
lemma mod_eq_imp_eq_aux: "b mod N = (a::nat) mod N \<Longrightarrow> a\<le>b \<Longrightarrow> b<a+N \<Longrightarrow> b=a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b mod N = a mod N; a \<le> b; b < a + N\<rbrakk> \<Longrightarrow> b = a
[PROOF STEP]
by (auto simp add: mod_eq_dvd_iff_nat le_imp_diff_is_add)


[STATEMENT]
lemma mod_eq_imp_eq:
    "\<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N \<rbrakk> \<Longrightarrow> x=y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume a1: "b \<le> y"
[PROOF STATE]
proof (state)
this:
b \<le> y

goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume a2: "y < b + N"
[PROOF STATE]
proof (state)
this:
y < b + N

goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume a3: "b \<le> x"
[PROOF STATE]
proof (state)
this:
b \<le> x

goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume a4: "x < b + N"
[PROOF STATE]
proof (state)
this:
x < b + N

goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume a5: "x mod N = y mod N"
[PROOF STATE]
proof (state)
this:
x mod N = y mod N

goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have f6: "x < y + N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y + N
[PROOF STEP]
using a4 a1
[PROOF STATE]
proof (prove)
using this:
x < b + N
b \<le> y

goal (1 subgoal):
 1. x < y + N
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
x < y + N

goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "y < x + N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y < x + N
[PROOF STEP]
using a3 a2
[PROOF STATE]
proof (prove)
using this:
b \<le> x
y < b + N

goal (1 subgoal):
 1. y < x + N
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
y < x + N

goal (1 subgoal):
 1. \<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y < x + N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y < x + N

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using f6 a5
[PROOF STATE]
proof (prove)
using this:
y < x + N
x < y + N
x mod N = y mod N

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis (no_types) mod_eq_imp_eq_aux nat_le_linear)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_ticket_addsimps[simp]:
    "map_ticket f t = INIT \<longleftrightarrow> t=INIT"
    "map_ticket f t = WAIT tk \<longleftrightarrow> (\<exists>tk'. tk=f tk' \<and> t=WAIT tk')"
    "map_ticket f t = HOLD tk \<longleftrightarrow> (\<exists>tk'. tk=f tk' \<and> t=HOLD tk')"
    "map_ticket f t = REL tk \<longleftrightarrow> (\<exists>tk'. tk=f tk' \<and> t=REL tk')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((map_ticket f t = INIT) = (t = INIT) &&& (map_ticket f t = WAIT tk) = (\<exists>tk'. tk = f tk' \<and> t = WAIT tk')) &&& (map_ticket f t = HOLD tk) = (\<exists>tk'. tk = f tk' \<and> t = HOLD tk') &&& (map_ticket f t = REL tk) = (\<exists>tk'. tk = f tk' \<and> t = REL tk')
[PROOF STEP]
by (cases t; auto)+


[STATEMENT]
lemma ni_weight_le1[simp]: "ni_weight s \<le> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni_weight s \<le> Suc 0
[PROOF STEP]
by (cases s) auto


[STATEMENT]
lemma num_ni_init[simp]: "num_ni (\<lambda>_. INIT) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_ni (\<lambda>_. INIT) = 0
[PROOF STEP]
by (auto simp: num_ni_def)


[STATEMENT]
lemma num_ni_upd:
    "t<N \<Longrightarrow> num_ni (ts(t:=s)) = num_ni ts - ni_weight (ts t) + ni_weight s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t < N \<Longrightarrow> num_ni (ts(t := s)) = num_ni ts - ni_weight (ts t) + ni_weight s
[PROOF STEP]
by (auto
      simp: num_ni_def if_distrib[of ni_weight] sum.If_cases algebra_simps
      simp: sum_diff1_nat
      )