[STATEMENT]
lemma prec_after_EV_WAIT_step:
assumes prec: "rprecondition s (rcurrent s) (aseq ! n)"
    and n_bound: "Suc n < length aseq"
    and IPC: "is_SK_EV_WAIT aseq"
    and not_aborting: "\<not>raborting s (rcurrent s) (aseq ! n)"
    and not_waiting: "\<not>rwaiting s (rcurrent s) (aseq ! n)"
shows "rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
fix consume
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume WAIT: "aseq = [SK_EV_WAIT EV_PREP consume,
                        SK_EV_WAIT EV_WAIT consume,
                        SK_EV_WAIT EV_FINISH consume]"
[PROOF STATE]
proof (state)
this:
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume 0: "n=0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from 0 WAIT prec not_aborting
[PROOF STATE]
proof (chain)
picking this:
n = 0
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
rprecondition s (rcurrent s) (aseq ! n)
\<not> raborting s (rcurrent s) (aseq ! n)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
rprecondition s (rcurrent s) (aseq ! n)
\<not> raborting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding rprecondition_def atomic_step_precondition_def
[PROOF STATE]
proof (prove)
using this:
n = 0
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
case aseq ! n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (rcurrent s) partner \<down> s | NONE \<Rightarrow> True
\<not> raborting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. case aseq ! Suc n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> rstep s (aseq ! n) | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> rstep s (aseq ! n) \<and> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) page' \<down> rstep s (aseq ! n) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (rcurrent s) partner \<down> rstep s (aseq ! n) | NONE \<Rightarrow> True
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume 1: "n=1"
[PROOF STATE]
proof (state)
this:
n = 1

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from 1 WAIT prec not_waiting
[PROOF STATE]
proof (chain)
picking this:
n = 1
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
rprecondition s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 1
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
rprecondition s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding rprecondition_def atomic_step_precondition_def
[PROOF STATE]
proof (prove)
using this:
n = 1
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
case aseq ! n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (rcurrent s) partner \<down> s | NONE \<Rightarrow> True
\<not> rwaiting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. case aseq ! Suc n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> rstep s (aseq ! n) | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> rstep s (aseq ! n) \<and> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) page' \<down> rstep s (aseq ! n) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> ev_signal_precondition (rcurrent s) partner \<down> rstep s (aseq ! n) | NONE \<Rightarrow> True
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from WAIT
[PROOF STATE]
proof (chain)
picking this:
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
[PROOF STEP]
have "length aseq = 3"
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]

goal (1 subgoal):
 1. length aseq = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length aseq = 3

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 3
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 3

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
using n_bound
[PROOF STATE]
proof (prove)
using this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
n = 1 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 3
Suc n < length aseq

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
aseq = [SK_EV_WAIT EV_PREP ?consume2, SK_EV_WAIT EV_WAIT ?consume2, SK_EV_WAIT EV_FINISH ?consume2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_WAIT EV_PREP ?consume2, SK_EV_WAIT EV_WAIT ?consume2, SK_EV_WAIT EV_FINISH ?consume2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_WAIT EV_PREP ?consume2, SK_EV_WAIT EV_WAIT ?consume2, SK_EV_WAIT EV_FINISH ?consume2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
rprecondition s (rcurrent s) (aseq ! n)
Suc n < length aseq
is_SK_EV_WAIT aseq
\<not> raborting s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding is_SK_EV_WAIT_def
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_WAIT EV_PREP ?consume2, SK_EV_WAIT EV_WAIT ?consume2, SK_EV_WAIT EV_FINISH ?consume2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
rprecondition s (rcurrent s) (aseq ! n)
Suc n < length aseq
\<exists>consume. aseq = [SK_EV_WAIT EV_PREP consume, SK_EV_WAIT EV_WAIT consume, SK_EV_WAIT EV_FINISH consume]
\<not> raborting s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prec_after_EV_SIGNAL_step:
assumes prec: "rprecondition s (rcurrent s) (aseq ! n)"
    and n_bound: "Suc n < length aseq"
    and SIGNAL: "is_SK_EV_SIGNAL aseq"
    and not_aborting: "\<not>raborting s (rcurrent s) (aseq ! n)"
    and not_waiting: "\<not>rwaiting s (rcurrent s) (aseq ! n)"
shows "rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
fix partner
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume SIGNAL1: "aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner,
                            SK_EV_SIGNAL EV_SIGNAL_FINISH partner]"
[PROOF STATE]
proof (state)
this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
assume 0: "n=0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from 0 SIGNAL1 prec not_aborting
[PROOF STATE]
proof (chain)
picking this:
n = 0
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]
rprecondition s (rcurrent s) (aseq ! n)
\<not> raborting s (rcurrent s) (aseq ! n)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]
rprecondition s (rcurrent s) (aseq ! n)
\<not> raborting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding rprecondition_def atomic_step_precondition_def ev_signal_precondition_def
                aborting_def rstep_def atomic_step_def
[PROOF STATE]
proof (prove)
using this:
n = 0
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]
case aseq ! n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj \<down> s (Step.partition (rcurrent s)) (Step.partition partner) | NONE \<Rightarrow> True
\<not> (case aseq ! n of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition (rcurrent s) dir partner page \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> sp_impl_subj_subj \<down> s (Step.partition (rcurrent s)) (Step.partition partner) | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False)

goal (1 subgoal):
 1. case aseq ! Suc n of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> \<up> case aseq ! n of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current \<down> s) dir stage partner page \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (rcurrent s) dir partner page \<down> \<up> case aseq ! n of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current \<down> s) dir stage partner page \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) page' \<down> \<up> case aseq ! n of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current \<down> s) dir stage partner page \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj \<down> \<up> case aseq ! n of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current \<down> s) dir stage partner page \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s (Step.partition (rcurrent s)) (Step.partition partner) | NONE \<Rightarrow> True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
from SIGNAL1
[PROOF STATE]
proof (chain)
picking this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]
[PROOF STEP]
have "length aseq = 2"
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]

goal (1 subgoal):
 1. length aseq = 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length aseq = 2

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 2
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 2

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
using n_bound
[PROOF STATE]
proof (prove)
using this:
n = 0 \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
length aseq = 2
Suc n < length aseq

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP ?partner2, SK_EV_SIGNAL EV_SIGNAL_FINISH ?partner2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP ?partner2, SK_EV_SIGNAL EV_SIGNAL_FINISH ?partner2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP ?partner2, SK_EV_SIGNAL EV_SIGNAL_FINISH ?partner2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
rprecondition s (rcurrent s) (aseq ! n)
Suc n < length aseq
is_SK_EV_SIGNAL aseq
\<not> raborting s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
unfolding is_SK_EV_SIGNAL_def
[PROOF STATE]
proof (prove)
using this:
aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP ?partner2, SK_EV_SIGNAL EV_SIGNAL_FINISH ?partner2] \<Longrightarrow> rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
rprecondition s (rcurrent s) (aseq ! n)
Suc n < length aseq
\<exists>partner. aseq = [SK_EV_SIGNAL EV_SIGNAL_PREP partner, SK_EV_SIGNAL EV_SIGNAL_FINISH partner]
\<not> raborting s (rcurrent s) (aseq ! n)
\<not> rwaiting s (rcurrent s) (aseq ! n)

goal (1 subgoal):
 1. rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rprecondition (rstep s (aseq ! n)) (rcurrent s) (aseq ! Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma on_set_object_value:
  shows "sp_impl_subj_subj (set_object_value ob val s) = sp_impl_subj_subj s"
    and "sp_impl_subj_obj (set_object_value ob val s) = sp_impl_subj_obj s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sp_impl_subj_subj (set_object_value ob val s) = sp_impl_subj_subj s &&& sp_impl_subj_obj (set_object_value ob val s) = sp_impl_subj_obj s
[PROOF STEP]
unfolding set_object_value_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sp_impl_subj_subj (s\<lparr>obj := (obj s)(ob := val)\<rparr>) = sp_impl_subj_subj s &&& sp_impl_subj_obj (s\<lparr>obj := (obj s)(ob := val)\<rparr>) = sp_impl_subj_obj s
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prec_IPC_dom_independent:
assumes "current s \<noteq> d"
    and "atomic_step_invariant s"
    and "atomic_step_precondition s d a"
shows "atomic_step_precondition (atomic_step_ipc (current s) dir stage partner page s) d a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ipc (current s) dir stage partner page s) d a
[PROOF STEP]
using assms on_set_object_value
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
atomic_step_precondition s d a
sp_impl_subj_subj (set_object_value ?ob ?val ?s) = sp_impl_subj_subj ?s
sp_impl_subj_obj (set_object_value ?ob ?val ?s) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ipc (current s) dir stage partner page s) d a
[PROOF STEP]
unfolding atomic_step_precondition_def atomic_step_ipc_def ipc_precondition_def
          ev_signal_precondition_def set_object_value_def
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode | SK_IPC dir (BUF page') partner page \<Rightarrow> (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode) \<and> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition partner) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj s (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
sp_impl_subj_subj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_subj ?s
sp_impl_subj_obj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. case a of SK_IPC dira PREP partner pagea \<Rightarrow> True | SK_IPC dira WAIT partner pagea \<Rightarrow> let sender = case dira of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dira of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dira of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition d) (PAGE pagea) local_access_mode | SK_IPC dira (BUF page') partner pagea \<Rightarrow> (let sender = case dira of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dira of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dira of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition d) (PAGE pagea) local_access_mode) \<and> (let sender = case opposite_ipc_direction dira of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dira of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dira of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition partner) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
[PROOF STEP]
by (auto split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
                   ev_consume_t.splits ev_wait_stage_t.splits ev_signal_stage_t.splits)


[STATEMENT]
lemma prec_ev_signal_dom_independent:
assumes "current s \<noteq> d"
    and "atomic_step_invariant s"
    and "atomic_step_precondition s d a"
shows "atomic_step_precondition (atomic_step_ev_signal (current s) partner s) d a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ev_signal (current s) partner s) d a
[PROOF STEP]
using assms on_set_object_value
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
atomic_step_precondition s d a
sp_impl_subj_subj (set_object_value ?ob ?val ?s) = sp_impl_subj_subj ?s
sp_impl_subj_obj (set_object_value ?ob ?val ?s) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ev_signal (current s) partner s) d a
[PROOF STEP]
unfolding atomic_step_precondition_def atomic_step_ev_signal_def ipc_precondition_def
          ev_signal_precondition_def set_object_value_def
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode | SK_IPC dir (BUF page') partner page \<Rightarrow> (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode) \<and> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition partner) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj s (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
sp_impl_subj_subj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_subj ?s
sp_impl_subj_obj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. case a of SK_IPC dir PREP partnera page \<Rightarrow> True | SK_IPC dir WAIT partnera page \<Rightarrow> let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partnera; receiver = case dir of SEND \<Rightarrow> partnera | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) (Step.partition d) (PAGE page) local_access_mode | SK_IPC dir (BUF page') partnera page \<Rightarrow> (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partnera; receiver = case dir of SEND \<Rightarrow> partnera | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) (Step.partition d) (PAGE page) local_access_mode) \<and> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partnera | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partnera; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) (Step.partition partnera) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partnera \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partnera \<Rightarrow> sp_impl_subj_subj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) (Step.partition d) (Step.partition partnera) | NONE \<Rightarrow> True
[PROOF STEP]
by (auto split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
                   ev_consume_t.splits ev_wait_stage_t.splits ev_signal_stage_t.splits)


[STATEMENT]
lemma prec_ev_wait_one_dom_independent:
assumes "current s \<noteq> d"
    and "atomic_step_invariant s"
    and "atomic_step_precondition s d a"
shows "atomic_step_precondition (atomic_step_ev_wait_one (current s) s) d a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ev_wait_one (current s) s) d a
[PROOF STEP]
using assms on_set_object_value
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
atomic_step_precondition s d a
sp_impl_subj_subj (set_object_value ?ob ?val ?s) = sp_impl_subj_subj ?s
sp_impl_subj_obj (set_object_value ?ob ?val ?s) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ev_wait_one (current s) s) d a
[PROOF STEP]
unfolding atomic_step_precondition_def atomic_step_ev_wait_one_def ipc_precondition_def
          ev_signal_precondition_def set_object_value_def
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode | SK_IPC dir (BUF page') partner page \<Rightarrow> (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode) \<and> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition partner) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj s (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
sp_impl_subj_subj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_subj ?s
sp_impl_subj_obj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr>) (Step.partition d) (PAGE page) local_access_mode | SK_IPC dir (BUF page') partner page \<Rightarrow> (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr>) (Step.partition d) (PAGE page) local_access_mode) \<and> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr>) (Step.partition partner) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr>) (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
[PROOF STEP]
by (auto split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
                   ev_consume_t.splits ev_wait_stage_t.splits ev_signal_stage_t.splits)


[STATEMENT]
lemma prec_ev_wait_all_dom_independent:
assumes "current s \<noteq> d"
    and "atomic_step_invariant s"
    and "atomic_step_precondition s d a"
shows "atomic_step_precondition (atomic_step_ev_wait_all (current s) s) d a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ev_wait_all (current s) s) d a
[PROOF STEP]
using assms on_set_object_value
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
atomic_step_precondition s d a
sp_impl_subj_subj (set_object_value ?ob ?val ?s) = sp_impl_subj_subj ?s
sp_impl_subj_obj (set_object_value ?ob ?val ?s) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. atomic_step_precondition (atomic_step_ev_wait_all (current s) s) d a
[PROOF STEP]
unfolding atomic_step_precondition_def atomic_step_ev_wait_all_def ipc_precondition_def
          ev_signal_precondition_def set_object_value_def
[PROOF STATE]
proof (prove)
using this:
current s \<noteq> d
atomic_step_invariant s
case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode | SK_IPC dir (BUF page') partner page \<Rightarrow> (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d) (PAGE page) local_access_mode) \<and> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition partner) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj s (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
sp_impl_subj_subj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_subj ?s
sp_impl_subj_obj (?s\<lparr>obj := (obj ?s)(?ob := ?val)\<rparr>) = sp_impl_subj_obj ?s

goal (1 subgoal):
 1. case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr>) (Step.partition d) (PAGE page) local_access_mode | SK_IPC dir (BUF page') partner page \<Rightarrow> (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr>) (Step.partition d) (PAGE page) local_access_mode) \<and> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr>) (Step.partition partner) (PAGE page') local_access_mode) | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj (s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr>) (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True
[PROOF STEP]
by (auto split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
                   ev_consume_t.splits ev_wait_stage_t.splits ev_signal_stage_t.splits)


[STATEMENT]
lemma prec_dom_independent:
shows "\<forall> s d a a' . rcurrent s \<noteq> d \<and> rprecondition s d a \<longrightarrow> rprecondition (rstep s a') d a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s d a a'. rcurrent s \<noteq> d \<and> rprecondition s d a \<longrightarrow> rprecondition (rstep s a') d a
[PROOF STEP]
using atomic_step_preserves_invariants
rstate_invariant prec_IPC_dom_independent prec_ev_signal_dom_independent
prec_ev_wait_all_dom_independent prec_ev_wait_one_dom_independent
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step ?s ?a)
atomic_step_invariant \<down> ?s
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ipc (current ?s) ?dir ?stage ?partner ?page ?s) ?d ?a
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ev_signal (current ?s) ?partner ?s) ?d ?a
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ev_wait_all (current ?s) ?s) ?d ?a
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ev_wait_one (current ?s) ?s) ?d ?a

goal (1 subgoal):
 1. \<forall>s d a a'. rcurrent s \<noteq> d \<and> rprecondition s d a \<longrightarrow> rprecondition (rstep s a') d a
[PROOF STEP]
unfolding rcurrent_def rprecondition_def rstep_def atomic_step_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (case ?a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current ?s) dir stage partner page ?s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current ?s) ?s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current ?s) ?s | SK_EV_WAIT _ consume \<Rightarrow> ?s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> ?s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current ?s) partner ?s | NONE \<Rightarrow> ?s)
atomic_step_invariant \<down> ?s
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ipc (current ?s) ?dir ?stage ?partner ?page ?s) ?d ?a
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ev_signal (current ?s) ?partner ?s) ?d ?a
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ev_wait_all (current ?s) ?s) ?d ?a
\<lbrakk>current ?s \<noteq> ?d; atomic_step_invariant ?s; atomic_step_precondition ?s ?d ?a\<rbrakk> \<Longrightarrow> atomic_step_precondition (atomic_step_ev_wait_one (current ?s) ?s) ?d ?a

goal (1 subgoal):
 1. \<forall>s d a a'. current \<down> s \<noteq> d \<and> atomic_step_precondition \<down> s d a \<longrightarrow> atomic_step_precondition \<down> \<up> case a' of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current \<down> s) dir stage partner page \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current \<down> s) \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current \<down> s) \<down> s | SK_EV_WAIT _ consume \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current \<down> s) partner \<down> s | NONE \<Rightarrow> \<down> s d a
[PROOF STEP]
by(auto split: int_point_t.splits  ev_consume_t.splits ev_wait_stage_t.splits ev_signal_stage_t.splits)


[STATEMENT]
lemma ipc_precondition_after_cswitch[simp]:
shows "ipc_precondition d dir partner page ((\<down> s)\<lparr>current := new_current\<rparr>)
          = ipc_precondition d dir partner page (\<down> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipc_precondition d dir partner page (\<down> s\<lparr>current := new_current\<rparr>) = ipc_precondition d dir partner page \<down> s
[PROOF STEP]
unfolding ipc_precondition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (\<down> s\<lparr>current := new_current\<rparr>) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (\<down> s\<lparr>current := new_current\<rparr>) (Step.partition d) (PAGE page) local_access_mode) = (let sender = case dir of SEND \<Rightarrow> d | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj \<down> s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj \<down> s (Step.partition d) (PAGE page) local_access_mode)
[PROOF STEP]
by(auto split: ipc_direction_t.splits)


[STATEMENT]
lemma precondition_after_cswitch:
shows "\<forall>s d n a. rprecondition s d a \<longrightarrow> rprecondition (rcswitch n s) d a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s d n a. rprecondition s d a \<longrightarrow> rprecondition (rcswitch n s) d a
[PROOF STEP]
using cswitch_preserves_invariants rstate_invariant
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. \<forall>s d n a. rprecondition s d a \<longrightarrow> rprecondition (rcswitch n s) d a
[PROOF STEP]
unfolding rprecondition_def rcswitch_def atomic_step_precondition_def
          ev_signal_precondition_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. \<forall>s d n a. (case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition d dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) d page' \<down> s | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj \<down> s (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True) \<longrightarrow> (case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition d dir partner page \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition d dir partner page \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> \<and> ipc_precondition partner (opposite_ipc_direction dir) d page' \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> | SK_EV_WAIT ev_wait_stage_t x \<Rightarrow> rinvariant x | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> True | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> sp_impl_subj_subj \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> (Step.partition d) (Step.partition partner) | NONE \<Rightarrow> True)
[PROOF STEP]
by (auto split: int_point_t.splits ipc_stage_t.splits  ev_signal_stage_t.splits)


[STATEMENT]
lemma aborting_switch_independent:
shows "\<forall>n s. raborting (rcswitch n s) = raborting s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
fix n s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
fix tid a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
have "raborting (rcswitch n s) tid a = raborting s tid a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. raborting (rcswitch n s) tid a = raborting s tid a
[PROOF STEP]
using rstate_invariant cswitch_preserves_invariants ev_signal_precondition_weakly_step_consistent
            cswitch_consistency_and_respect
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ev_signal_precondition ?tid ?partner ?s1.0 = ev_signal_precondition ?tid ?partner ?s2.0
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. raborting (rcswitch n s) tid a = raborting s tid a
[PROOF STEP]
unfolding aborting_def rcswitch_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ev_signal_precondition ?tid ?partner ?s1.0 = ev_signal_precondition ?tid ?partner ?s2.0
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. (case a of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition tid dir partner page \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> ev_signal_precondition tid partner \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False) = (case a of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition tid dir partner page \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> ev_signal_precondition tid partner \<down> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
apply (auto split: int_point_t.splits ipc_stage_t.splits
                         ev_wait_stage_t.splits ev_signal_stage_t.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x32. \<lbrakk>\<And>s. atomic_step_invariant \<down> s; \<And>s new_current. atomic_step_invariant s \<Longrightarrow> atomic_step_invariant (s\<lparr>current := new_current\<rparr>); \<And>tid s1 s2 partner. \<lbrakk>vpeq (Step.partition tid) s1 s2; atomic_step_invariant s1; atomic_step_invariant s2\<rbrakk> \<Longrightarrow> ev_signal_precondition tid partner s1 = ev_signal_precondition tid partner s2; \<And>s u new_current. atomic_step_invariant s \<Longrightarrow> vpeq u s (s\<lparr>current := new_current\<rparr>); a = SK_EV_SIGNAL EV_SIGNAL_PREP x32; ev_signal_precondition tid x32 (\<down> s\<lparr>current := Eps rinvariant\<rparr>)\<rbrakk> \<Longrightarrow> ev_signal_precondition tid x32 \<down> s
 2. \<And>x32. \<lbrakk>\<And>s. atomic_step_invariant \<down> s; \<And>s new_current. atomic_step_invariant s \<Longrightarrow> atomic_step_invariant (s\<lparr>current := new_current\<rparr>); \<And>tid s1 s2 partner. \<lbrakk>vpeq (Step.partition tid) s1 s2; atomic_step_invariant s1; atomic_step_invariant s2\<rbrakk> \<Longrightarrow> ev_signal_precondition tid partner s1 = ev_signal_precondition tid partner s2; \<And>s u new_current. atomic_step_invariant s \<Longrightarrow> vpeq u s (s\<lparr>current := new_current\<rparr>); a = SK_EV_SIGNAL EV_SIGNAL_PREP x32; ev_signal_precondition tid x32 \<down> s\<rbrakk> \<Longrightarrow> ev_signal_precondition tid x32 (\<down> s\<lparr>current := Eps rinvariant\<rparr>)
[PROOF STEP]
apply (metis (full_types))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x32. \<lbrakk>\<And>s. atomic_step_invariant \<down> s; \<And>s new_current. atomic_step_invariant s \<Longrightarrow> atomic_step_invariant (s\<lparr>current := new_current\<rparr>); \<And>tid s1 s2 partner. \<lbrakk>vpeq (Step.partition tid) s1 s2; atomic_step_invariant s1; atomic_step_invariant s2\<rbrakk> \<Longrightarrow> ev_signal_precondition tid partner s1 = ev_signal_precondition tid partner s2; \<And>s u new_current. atomic_step_invariant s \<Longrightarrow> vpeq u s (s\<lparr>current := new_current\<rparr>); a = SK_EV_SIGNAL EV_SIGNAL_PREP x32; ev_signal_precondition tid x32 \<down> s\<rbrakk> \<Longrightarrow> ev_signal_precondition tid x32 (\<down> s\<lparr>current := Eps rinvariant\<rparr>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
raborting (rcswitch n s) tid a = raborting s tid a

goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
raborting (rcswitch n s) ?tid2 ?a2 = raborting s ?tid2 ?a2

goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
hence "raborting (rcswitch n s) = raborting s"
[PROOF STATE]
proof (prove)
using this:
raborting (rcswitch n s) ?tid2 ?a2 = raborting s ?tid2 ?a2

goal (1 subgoal):
 1. raborting (rcswitch n s) = raborting s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
raborting (rcswitch n s) = raborting s

goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
raborting (rcswitch ?n2 ?s2) = raborting ?s2

goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
raborting (rcswitch ?n2 ?s2) = raborting ?s2

goal (1 subgoal):
 1. \<forall>n s. raborting (rcswitch n s) = raborting s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n s. raborting (rcswitch n s) = raborting s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma waiting_switch_independent:
shows "\<forall>n s. rwaiting (rcswitch n s) = rwaiting s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
fix n s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
fix tid a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
have "rwaiting (rcswitch n s) tid a = rwaiting s tid a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rwaiting (rcswitch n s) tid a = rwaiting s tid a
[PROOF STEP]
using rstate_invariant cswitch_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. rwaiting (rcswitch n s) tid a = rwaiting s tid a
[PROOF STEP]
unfolding waiting_def rcswitch_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. (case a of SK_IPC dir WAIT partner page \<Rightarrow> \<not> ipc_precondition partner (opposite_ipc_direction dir) tid (Eps rinvariant) \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr> tid) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False) = (case a of SK_IPC dir WAIT partner page \<Rightarrow> \<not> ipc_precondition partner (opposite_ipc_direction dir) tid (Eps rinvariant) \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> s tid) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
by(auto split: int_point_t.splits ipc_stage_t.splits ev_wait_stage_t.splits)
[PROOF STATE]
proof (state)
this:
rwaiting (rcswitch n s) tid a = rwaiting s tid a

goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rwaiting (rcswitch n s) ?tid2 ?a2 = rwaiting s ?tid2 ?a2

goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
hence "rwaiting (rcswitch n s) = rwaiting s"
[PROOF STATE]
proof (prove)
using this:
rwaiting (rcswitch n s) ?tid2 ?a2 = rwaiting s ?tid2 ?a2

goal (1 subgoal):
 1. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rwaiting (rcswitch n s) = rwaiting s

goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rwaiting (rcswitch ?n2 ?s2) = rwaiting ?s2

goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
rwaiting (rcswitch ?n2 ?s2) = rwaiting ?s2

goal (1 subgoal):
 1. \<forall>n s. rwaiting (rcswitch n s) = rwaiting s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n s. rwaiting (rcswitch n s) = rwaiting s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aborting_after_IPC_step:
assumes "d1 \<noteq> d2"
shows "aborting (atomic_step_ipc d1 dir stage partner page s) d2 a = aborting s d2 a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aborting (atomic_step_ipc d1 dir stage partner page s) d2 a = aborting s d2 a
[PROOF STEP]
unfolding atomic_step_ipc_def aborting_def set_object_value_def ipc_precondition_def
          ev_signal_precondition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case a of SK_IPC dira PREP partner pagea \<Rightarrow> \<not> (let sender = case dira of SEND \<Rightarrow> d2 | RECV \<Rightarrow> partner; receiver = case dira of SEND \<Rightarrow> partner | RECV \<Rightarrow> d2; local_access_mode = case dira of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition d2) (PAGE pagea) local_access_mode) | SK_IPC dira _ partner pagea \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> sp_impl_subj_subj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition d2) (Step.partition partner) | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False) = (case a of SK_IPC dir PREP partner page \<Rightarrow> \<not> (let sender = case dir of SEND \<Rightarrow> d2 | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d2; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition d2) (PAGE page) local_access_mode) | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> sp_impl_subj_subj s (Step.partition d2) (Step.partition partner) | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
by(auto split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
                   ev_signal_stage_t.splits)


[STATEMENT]
lemma waiting_after_IPC_step:
assumes "d1 \<noteq> d2"
shows "waiting (atomic_step_ipc d1 dir stage partner page s) d2 a = waiting s d2 a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. waiting (atomic_step_ipc d1 dir stage partner page s) d2 a = waiting s d2 a
[PROOF STEP]
unfolding atomic_step_ipc_def waiting_def set_object_value_def ipc_precondition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case a of SK_IPC dira WAIT partner pagea \<Rightarrow> \<not> (let sender = case opposite_ipc_direction dira of SEND \<Rightarrow> partner | RECV \<Rightarrow> d2; receiver = case opposite_ipc_direction dira of SEND \<Rightarrow> d2 | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dira of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) (Step.partition partner) (PAGE (Eps rinvariant)) local_access_mode) | SK_IPC dira _ partner pagea \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | RECV \<Rightarrow> s | _ \<Rightarrow> s) d2) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False) = (case a of SK_IPC dir WAIT partner page \<Rightarrow> \<not> (let sender = case opposite_ipc_direction dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> d2; receiver = case opposite_ipc_direction dir of SEND \<Rightarrow> d2 | RECV \<Rightarrow> partner; local_access_mode = case opposite_ipc_direction dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition partner) (PAGE (Eps rinvariant)) local_access_mode) | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread s d2) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
by(auto split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
                   ev_wait_stage_t.splits)


[STATEMENT]
lemma raborting_consistent:
shows "\<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
fix s t u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
assume vpeq: "rvpeq u s t"
[PROOF STATE]
proof (state)
this:
rvpeq u s t

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rvpeq u s t

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
from vpeq ipc_precondition_weakly_step_consistent rstate_invariant
[PROOF STATE]
proof (chain)
picking this:
rvpeq u s t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ipc_precondition ?tid ?dir ?partner ?page ?s1.0 = ipc_precondition ?tid ?dir ?partner ?page ?s2.0
atomic_step_invariant \<down> ?s
[PROOF STEP]
have "\<And> tid dir partner page . ipc_precondition u dir partner page (\<down>s)
                                    = ipc_precondition u dir partner page (\<down>t)"
[PROOF STATE]
proof (prove)
using this:
rvpeq u s t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ipc_precondition ?tid ?dir ?partner ?page ?s1.0 = ipc_precondition ?tid ?dir ?partner ?page ?s2.0
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. \<And>tid dir partner page. ipc_precondition u dir partner page \<down> s = ipc_precondition u dir partner page \<down> t
[PROOF STEP]
unfolding rvpeq_def
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ipc_precondition ?tid ?dir ?partner ?page ?s1.0 = ipc_precondition ?tid ?dir ?partner ?page ?s2.0
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. \<And>tid dir partner page. ipc_precondition u dir partner page \<down> s = ipc_precondition u dir partner page \<down> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ipc_precondition u ?dir ?partner ?page \<down> s = ipc_precondition u ?dir ?partner ?page \<down> t

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
with vpeq rstate_invariant
[PROOF STATE]
proof (chain)
picking this:
rvpeq u s t
atomic_step_invariant \<down> ?s
ipc_precondition u ?dir ?partner ?page \<down> s = ipc_precondition u ?dir ?partner ?page \<down> t
[PROOF STEP]
have "raborting s u a = raborting t u a"
[PROOF STATE]
proof (prove)
using this:
rvpeq u s t
atomic_step_invariant \<down> ?s
ipc_precondition u ?dir ?partner ?page \<down> s = ipc_precondition u ?dir ?partner ?page \<down> t

goal (1 subgoal):
 1. raborting s u a = raborting t u a
[PROOF STEP]
unfolding aborting_def rvpeq_def vpeq_def vpeq_local_def ev_signal_precondition_def
               vpeq_subj_subj_def atomic_step_invariant_def sp_subset_def rep_def
[PROOF STATE]
proof (prove)
using this:
vpeq_obj (Step.partition u) (Rep_rstate_t s) (Rep_rstate_t t) \<and> (\<forall>v. (Policy.sp_spec_subj_subj (Step.partition u) v \<longrightarrow> sp_impl_subj_subj (Rep_rstate_t s) (Step.partition u) v = sp_impl_subj_subj (Rep_rstate_t t) (Step.partition u) v) \<and> (Policy.sp_spec_subj_subj v (Step.partition u) \<longrightarrow> sp_impl_subj_subj (Rep_rstate_t s) v (Step.partition u) = sp_impl_subj_subj (Rep_rstate_t t) v (Step.partition u))) \<and> vpeq_subj_obj (Step.partition u) (Rep_rstate_t s) (Rep_rstate_t t) \<and> (\<forall>tid. Step.partition tid = Step.partition u \<longrightarrow> thread (Rep_rstate_t s) tid = thread (Rep_rstate_t t) tid)
(\<forall>p1 p2. sp_impl_subj_subj (Rep_rstate_t ?s) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (Rep_rstate_t ?s) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)
ipc_precondition u ?dir ?partner ?page (Rep_rstate_t s) = ipc_precondition u ?dir ?partner ?page (Rep_rstate_t t)

goal (1 subgoal):
 1. (case a of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition u dir partner page (Rep_rstate_t s) | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> sp_impl_subj_subj (Rep_rstate_t s) (Step.partition u) (Step.partition partner) | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False) = (case a of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition u dir partner page (Rep_rstate_t t) | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> sp_impl_subj_subj (Rep_rstate_t t) (Step.partition u) (Step.partition partner) | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
apply (auto split: int_point_t.splits ipc_stage_t.splits ev_signal_stage_t.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x32. \<lbrakk>\<And>s. (\<forall>p1 p2. sp_impl_subj_subj (Rep_rstate_t s) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (Rep_rstate_t s) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m); \<And>dir partner page. ipc_precondition u dir partner page (Rep_rstate_t s) = ipc_precondition u dir partner page (Rep_rstate_t t); vpeq_obj (Step.partition u) (Rep_rstate_t s) (Rep_rstate_t t); \<forall>v. (Policy.sp_spec_subj_subj (Step.partition u) v \<longrightarrow> sp_impl_subj_subj (Rep_rstate_t s) (Step.partition u) v = sp_impl_subj_subj (Rep_rstate_t t) (Step.partition u) v) \<and> (Policy.sp_spec_subj_subj v (Step.partition u) \<longrightarrow> sp_impl_subj_subj (Rep_rstate_t s) v (Step.partition u) = sp_impl_subj_subj (Rep_rstate_t t) v (Step.partition u)); vpeq_subj_obj (Step.partition u) (Rep_rstate_t s) (Rep_rstate_t t); \<forall>tid. Step.partition tid = Step.partition u \<longrightarrow> thread (Rep_rstate_t s) tid = thread (Rep_rstate_t t) tid; a = SK_EV_SIGNAL EV_SIGNAL_PREP x32; sp_impl_subj_subj (Rep_rstate_t s) (Step.partition u) (Step.partition x32)\<rbrakk> \<Longrightarrow> sp_impl_subj_subj (Rep_rstate_t t) (Step.partition u) (Step.partition x32)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
raborting s u a = raborting t u a

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
raborting s u ?a2 = raborting t u ?a2

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
hence "raborting s u = raborting t u"
[PROOF STATE]
proof (prove)
using this:
raborting s u ?a2 = raborting t u ?a2

goal (1 subgoal):
 1. raborting s u = raborting t u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
raborting s u = raborting t u

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rvpeq ?u2 ?s2 ?t2 \<Longrightarrow> raborting ?s2 ?u2 = raborting ?t2 ?u2

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
rvpeq ?u2 ?s2 ?t2 \<Longrightarrow> raborting ?s2 ?u2 = raborting ?t2 ?u2

goal (1 subgoal):
 1. \<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s t u. rvpeq u s t \<longrightarrow> raborting s u = raborting t u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aborting_dom_independent:
  assumes "rcurrent s \<noteq> d"
    shows "raborting (rstep s a) d a' = raborting s d a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. raborting (rstep s a) d a' = raborting s d a'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. raborting (rstep s a) d a' = raborting s d a'
[PROOF STEP]
have "\<And> tid dir partner page s . ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a)
                                   \<and> ev_signal_precondition tid partner  s = ev_signal_precondition tid partner (atomic_step s a)
       "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tid dir partner page s. ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a) \<and> ev_signal_precondition tid partner s = ev_signal_precondition tid partner (atomic_step s a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tid dir partner page s. ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a) \<and> ev_signal_precondition tid partner s = ev_signal_precondition tid partner (atomic_step s a)
[PROOF STEP]
fix tid dir partner page s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tid dir partner page s. ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a) \<and> ev_signal_precondition tid partner s = ev_signal_precondition tid partner (atomic_step s a)
[PROOF STEP]
let ?s = "atomic_step s a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tid dir partner page s. ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a) \<and> ev_signal_precondition tid partner s = ev_signal_precondition tid partner (atomic_step s a)
[PROOF STEP]
have "(\<forall> p q . sp_impl_subj_subj s p q = sp_impl_subj_subj ?s p q)
       \<and> (\<forall> p x m . sp_impl_subj_obj s p x m = sp_impl_subj_obj ?s p x m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p q. sp_impl_subj_subj s p q = sp_impl_subj_subj (atomic_step s a) p q) \<and> (\<forall>p x m. sp_impl_subj_obj s p x m = sp_impl_subj_obj (atomic_step s a) p x m)
[PROOF STEP]
unfolding atomic_step_def atomic_step_ipc_def
               atomic_step_ev_wait_all_def atomic_step_ev_wait_one_def
               atomic_step_ev_signal_def set_object_value_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p q. sp_impl_subj_subj s p q = sp_impl_subj_subj (case a of SK_IPC SEND (BUF page') partner page \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | SK_IPC RECV (BUF page') partner page \<Rightarrow> s | SK_IPC dir _ partner page \<Rightarrow> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr> | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr> | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr> | NONE \<Rightarrow> s) p q) \<and> (\<forall>p x m. sp_impl_subj_obj s p x m = sp_impl_subj_obj (case a of SK_IPC SEND (BUF page') partner page \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | SK_IPC RECV (BUF page') partner page \<Rightarrow> s | SK_IPC dir _ partner page \<Rightarrow> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr> | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr> | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr> | NONE \<Rightarrow> s) p x m)
[PROOF STEP]
by (auto split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
          ev_wait_stage_t.splits ev_consume_t.splits  ev_signal_stage_t.splits)
[PROOF STATE]
proof (state)
this:
(\<forall>p q. sp_impl_subj_subj s p q = sp_impl_subj_subj (atomic_step s a) p q) \<and> (\<forall>p x m. sp_impl_subj_obj s p x m = sp_impl_subj_obj (atomic_step s a) p x m)

goal (1 subgoal):
 1. \<And>tid dir partner page s. ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a) \<and> ev_signal_precondition tid partner s = ev_signal_precondition tid partner (atomic_step s a)
[PROOF STEP]
thus "ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a)
         \<and> ev_signal_precondition tid partner  s = ev_signal_precondition tid partner (atomic_step s a)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>p q. sp_impl_subj_subj s p q = sp_impl_subj_subj (atomic_step s a) p q) \<and> (\<forall>p x m. sp_impl_subj_obj s p x m = sp_impl_subj_obj (atomic_step s a) p x m)

goal (1 subgoal):
 1. ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a) \<and> ev_signal_precondition tid partner s = ev_signal_precondition tid partner (atomic_step s a)
[PROOF STEP]
unfolding ipc_precondition_def ev_signal_precondition_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>p q. sp_impl_subj_subj s p q = sp_impl_subj_subj (atomic_step s a) p q) \<and> (\<forall>p x m. sp_impl_subj_obj s p x m = sp_impl_subj_obj (atomic_step s a) p x m)

goal (1 subgoal):
 1. (let sender = case dir of SEND \<Rightarrow> tid | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> tid; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj s (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj s (Step.partition tid) (PAGE page) local_access_mode) = (let sender = case dir of SEND \<Rightarrow> tid | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> tid; local_access_mode = case dir of SEND \<Rightarrow> READ | RECV \<Rightarrow> WRITE in sp_impl_subj_subj (atomic_step s a) (Step.partition sender) (Step.partition receiver) \<and> sp_impl_subj_obj (atomic_step s a) (Step.partition tid) (PAGE page) local_access_mode) \<and> sp_impl_subj_subj s (Step.partition tid) (Step.partition partner) = sp_impl_subj_subj (atomic_step s a) (Step.partition tid) (Step.partition partner)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ipc_precondition tid dir partner page s = ipc_precondition tid dir partner page (atomic_step s a) \<and> ev_signal_precondition tid partner s = ev_signal_precondition tid partner (atomic_step s a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ipc_precondition ?tid ?dir ?partner ?page ?s = ipc_precondition ?tid ?dir ?partner ?page (atomic_step ?s a) \<and> ev_signal_precondition ?tid ?partner ?s = ev_signal_precondition ?tid ?partner (atomic_step ?s a)

goal (1 subgoal):
 1. raborting (rstep s a) d a' = raborting s d a'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ipc_precondition ?tid ?dir ?partner ?page ?s = ipc_precondition ?tid ?dir ?partner ?page (atomic_step ?s a) \<and> ev_signal_precondition ?tid ?partner ?s = ev_signal_precondition ?tid ?partner (atomic_step ?s a)

goal (1 subgoal):
 1. raborting (rstep s a) d a' = raborting s d a'
[PROOF STEP]
have "\<And> b . (\<down>(\<up>(atomic_step (\<down>s) b))) = atomic_step (\<down>s) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<down> \<up> atomic_step \<down> s b = atomic_step \<down> s b
[PROOF STEP]
using rstate_invariant atomic_step_preserves_invariants rstate_up_down
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step ?s ?a)
atomic_step_invariant ?s \<Longrightarrow> \<down> \<up> ?s = ?s

goal (1 subgoal):
 1. \<And>b. \<down> \<up> atomic_step \<down> s b = atomic_step \<down> s b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<down> \<up> atomic_step \<down> s ?b = atomic_step \<down> s ?b

goal (1 subgoal):
 1. raborting (rstep s a) d a' = raborting s d a'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ipc_precondition ?tid ?dir ?partner ?page ?s = ipc_precondition ?tid ?dir ?partner ?page (atomic_step ?s a) \<and> ev_signal_precondition ?tid ?partner ?s = ev_signal_precondition ?tid ?partner (atomic_step ?s a)
\<down> \<up> atomic_step \<down> s ?b = atomic_step \<down> s ?b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ipc_precondition ?tid ?dir ?partner ?page ?s = ipc_precondition ?tid ?dir ?partner ?page (atomic_step ?s a) \<and> ev_signal_precondition ?tid ?partner ?s = ev_signal_precondition ?tid ?partner (atomic_step ?s a)
\<down> \<up> atomic_step \<down> s ?b = atomic_step \<down> s ?b

goal (1 subgoal):
 1. raborting (rstep s a) d a' = raborting s d a'
[PROOF STEP]
unfolding aborting_def rstep_def ev_signal_precondition_def
[PROOF STATE]
proof (prove)
using this:
ipc_precondition ?tid ?dir ?partner ?page ?s = ipc_precondition ?tid ?dir ?partner ?page (atomic_step ?s a) \<and> sp_impl_subj_subj ?s (Step.partition ?tid) (Step.partition ?partner) = sp_impl_subj_subj (atomic_step ?s a) (Step.partition ?tid) (Step.partition ?partner)
\<down> \<up> atomic_step \<down> s ?b = atomic_step \<down> s ?b

goal (1 subgoal):
 1. (case a' of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition d dir partner page \<down> \<up> atomic_step \<down> s a | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> sp_impl_subj_subj \<down> \<up> atomic_step \<down> s a (Step.partition d) (Step.partition partner) | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False) = (case a' of SK_IPC dir PREP partner page \<Rightarrow> \<not> ipc_precondition d dir partner page \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> \<not> sp_impl_subj_subj \<down> s (Step.partition d) (Step.partition partner) | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
by (simp split: int_point_t.splits ipc_stage_t.splits ev_wait_stage_t.splits
                        ev_signal_stage_t.splits)
[PROOF STATE]
proof (state)
this:
raborting (rstep s a) d a' = raborting s d a'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipc_precondition_of_partner_consistent:
assumes vpeq: "\<forall> d \<in> rkinvolved (SK_IPC dir WAIT partner page) . rvpeq d s t"
shows "ipc_precondition partner dir' u page' (\<down> s) =  ipc_precondition partner dir' u page' \<down> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipc_precondition partner dir' u page' \<down> s = ipc_precondition partner dir' u page' \<down> t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ipc_precondition partner dir' u page' \<down> s = ipc_precondition partner dir' u page' \<down> t
[PROOF STEP]
from assms ipc_precondition_weakly_step_consistent rstate_invariant
[PROOF STATE]
proof (chain)
picking this:
\<forall>d\<in>rkinvolved (SK_IPC dir WAIT partner page). rvpeq d s t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ipc_precondition ?tid ?dir ?partner ?page ?s1.0 = ipc_precondition ?tid ?dir ?partner ?page ?s2.0
atomic_step_invariant \<down> ?s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>rkinvolved (SK_IPC dir WAIT partner page). rvpeq d s t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ipc_precondition ?tid ?dir ?partner ?page ?s1.0 = ipc_precondition ?tid ?dir ?partner ?page ?s2.0
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. ipc_precondition partner dir' u page' \<down> s = ipc_precondition partner dir' u page' \<down> t
[PROOF STEP]
unfolding rvpeq_def rkinvolved_def
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>case SK_IPC dir WAIT partner page of SK_IPC dir WAIT partner page \<Rightarrow> {partner} | SK_IPC dir _ partner page \<Rightarrow> {} | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> {} | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> {partner} | _ \<Rightarrow> {}. vpeq (Step.partition d) \<down> s \<down> t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ipc_precondition ?tid ?dir ?partner ?page ?s1.0 = ipc_precondition ?tid ?dir ?partner ?page ?s2.0
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. ipc_precondition partner dir' u page' \<down> s = ipc_precondition partner dir' u page' \<down> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ipc_precondition partner dir' u page' \<down> s = ipc_precondition partner dir' u page' \<down> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ev_signal_precondition_of_partner_consistent:
assumes vpeq: "\<forall> d \<in> rkinvolved (SK_EV_SIGNAL EV_SIGNAL_FINISH partner) . rvpeq d s t"
shows "ev_signal_precondition partner u (\<down> s) =  ev_signal_precondition partner u (\<down> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ev_signal_precondition partner u \<down> s = ev_signal_precondition partner u \<down> t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ev_signal_precondition partner u \<down> s = ev_signal_precondition partner u \<down> t
[PROOF STEP]
from assms ev_signal_precondition_weakly_step_consistent rstate_invariant
[PROOF STATE]
proof (chain)
picking this:
\<forall>d\<in>rkinvolved (SK_EV_SIGNAL EV_SIGNAL_FINISH partner). rvpeq d s t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ev_signal_precondition ?tid ?partner ?s1.0 = ev_signal_precondition ?tid ?partner ?s2.0
atomic_step_invariant \<down> ?s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>rkinvolved (SK_EV_SIGNAL EV_SIGNAL_FINISH partner). rvpeq d s t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ev_signal_precondition ?tid ?partner ?s1.0 = ev_signal_precondition ?tid ?partner ?s2.0
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. ev_signal_precondition partner u \<down> s = ev_signal_precondition partner u \<down> t
[PROOF STEP]
unfolding rvpeq_def rkinvolved_def
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>case SK_EV_SIGNAL EV_SIGNAL_FINISH partner of SK_IPC dir WAIT partner page \<Rightarrow> {partner} | SK_IPC dir _ partner page \<Rightarrow> {} | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> {} | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> {partner} | _ \<Rightarrow> {}. vpeq (Step.partition d) \<down> s \<down> t
\<lbrakk>vpeq (Step.partition ?tid) ?s1.0 ?s2.0; atomic_step_invariant ?s1.0; atomic_step_invariant ?s2.0\<rbrakk> \<Longrightarrow> ev_signal_precondition ?tid ?partner ?s1.0 = ev_signal_precondition ?tid ?partner ?s2.0
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. ev_signal_precondition partner u \<down> s = ev_signal_precondition partner u \<down> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ev_signal_precondition partner u \<down> s = ev_signal_precondition partner u \<down> t

goal:
No subgoals!
[PROOF STEP]
qed