[STATEMENT]
lemma waiting_consistent:
shows "\<forall>s t u a . rvpeq (rcurrent s) s t \<and> (\<forall> d \<in> rkinvolved a . rvpeq d s t)
        \<and> rvpeq u s t
        \<longrightarrow> rwaiting s u a = rwaiting t u a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
fix s t u a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
assume vpeq: "rvpeq (rcurrent s) s t"
[PROOF STATE]
proof (state)
this:
rvpeq (rcurrent s) s t

goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
assume vpeq_involved: "\<forall> d \<in> rkinvolved a . rvpeq d s t"
[PROOF STATE]
proof (state)
this:
\<forall>d\<in>rkinvolved a. rvpeq d s t

goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
assume vpeq_u: "rvpeq u s t"
[PROOF STATE]
proof (state)
this:
rvpeq u s t

goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
have "rwaiting s u a = rwaiting t u a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rwaiting s u a = rwaiting t u a
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. a = SK_IPC x11 x12 x13 x14 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 2. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 3. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 4. a = NONE \<Longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
case SK_IPC
[PROOF STATE]
proof (state)
this:
a = SK_IPC x11_ x12_ x13_ x14_

goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. a = SK_IPC x11 x12 x13 x14 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 2. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 3. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 4. a = NONE \<Longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
thus "rwaiting s u a = rwaiting t u a"
[PROOF STATE]
proof (prove)
using this:
a = SK_IPC x11_ x12_ x13_ x14_

goal (1 subgoal):
 1. rwaiting s u a = rwaiting t u a
[PROOF STEP]
using ipc_precondition_of_partner_consistent vpeq_involved
[PROOF STATE]
proof (prove)
using this:
a = SK_IPC x11_ x12_ x13_ x14_
\<forall>d\<in>rkinvolved (SK_IPC ?dir WAIT ?partner ?page). rvpeq d ?s ?t \<Longrightarrow> ipc_precondition ?partner ?dir' ?u ?page' \<down> ?s = ipc_precondition ?partner ?dir' ?u ?page' \<down> ?t
\<forall>d\<in>rkinvolved a. rvpeq d s t

goal (1 subgoal):
 1. rwaiting s u a = rwaiting t u a
[PROOF STEP]
unfolding waiting_def
[PROOF STATE]
proof (prove)
using this:
a = SK_IPC x11_ x12_ x13_ x14_
\<forall>d\<in>rkinvolved (SK_IPC ?dir WAIT ?partner ?page). rvpeq d ?s ?t \<Longrightarrow> ipc_precondition ?partner ?dir' ?u ?page' \<down> ?s = ipc_precondition ?partner ?dir' ?u ?page' \<down> ?t
\<forall>d\<in>rkinvolved a. rvpeq d s t

goal (1 subgoal):
 1. (case a of SK_IPC dir WAIT partner page \<Rightarrow> \<not> ipc_precondition partner (opposite_ipc_direction dir) u (Eps rinvariant) \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> s u) = 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) u (Eps rinvariant) \<down> t | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> t u) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
by (auto split: ipc_stage_t.splits)
[PROOF STATE]
proof (state)
this:
rwaiting s u a = rwaiting t u a

goal (3 subgoals):
 1. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 2. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 3. a = NONE \<Longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 2. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 3. a = NONE \<Longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
case SK_EV_WAIT
[PROOF STATE]
proof (state)
this:
a = SK_EV_WAIT x21_ x22_

goal (3 subgoals):
 1. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 2. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 3. a = NONE \<Longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
thus "rwaiting s u a = rwaiting t u a"
[PROOF STATE]
proof (prove)
using this:
a = SK_EV_WAIT x21_ x22_

goal (1 subgoal):
 1. rwaiting s u a = rwaiting t u a
[PROOF STEP]
using ev_signal_precondition_of_partner_consistent
        vpeq_involved vpeq vpeq_u
[PROOF STATE]
proof (prove)
using this:
a = SK_EV_WAIT x21_ x22_
\<forall>d\<in>rkinvolved (SK_EV_SIGNAL EV_SIGNAL_FINISH ?partner). rvpeq d ?s ?t \<Longrightarrow> ev_signal_precondition ?partner ?u \<down> ?s = ev_signal_precondition ?partner ?u \<down> ?t
\<forall>d\<in>rkinvolved a. rvpeq d s t
rvpeq (rcurrent s) s t
rvpeq u s t

goal (1 subgoal):
 1. rwaiting s u a = rwaiting t u a
[PROOF STEP]
unfolding waiting_def rkinvolved_def ev_signal_precondition_def
                  rvpeq_def vpeq_def vpeq_local_def
[PROOF STATE]
proof (prove)
using this:
a = SK_EV_WAIT x21_ x22_
\<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_obj (Step.partition d) \<down> ?s \<down> ?t \<and> vpeq_subj_subj (Step.partition d) \<down> ?s \<down> ?t \<and> vpeq_subj_obj (Step.partition d) \<down> ?s \<down> ?t \<and> (\<forall>tid. Step.partition tid = Step.partition d \<longrightarrow> thread \<down> ?s tid = thread \<down> ?t tid) \<Longrightarrow> sp_impl_subj_subj \<down> ?s (Step.partition ?partner) (Step.partition ?u) = sp_impl_subj_subj \<down> ?t (Step.partition ?partner) (Step.partition ?u)
\<forall>d\<in>case a 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_obj (Step.partition d) \<down> s \<down> t \<and> vpeq_subj_subj (Step.partition d) \<down> s \<down> t \<and> vpeq_subj_obj (Step.partition d) \<down> s \<down> t \<and> (\<forall>tid. Step.partition tid = Step.partition d \<longrightarrow> thread \<down> s tid = thread \<down> t tid)
vpeq_obj (Step.partition (rcurrent s)) \<down> s \<down> t \<and> vpeq_subj_subj (Step.partition (rcurrent s)) \<down> s \<down> t \<and> vpeq_subj_obj (Step.partition (rcurrent s)) \<down> s \<down> t \<and> (\<forall>tid. Step.partition tid = Step.partition (rcurrent s) \<longrightarrow> thread \<down> s tid = thread \<down> t tid)
vpeq_obj (Step.partition u) \<down> s \<down> t \<and> vpeq_subj_subj (Step.partition u) \<down> s \<down> t \<and> vpeq_subj_obj (Step.partition u) \<down> s \<down> t \<and> (\<forall>tid. Step.partition tid = Step.partition u \<longrightarrow> thread \<down> s tid = thread \<down> t tid)

goal (1 subgoal):
 1. (case a of SK_IPC dir WAIT partner page \<Rightarrow> \<not> ipc_precondition partner (opposite_ipc_direction dir) u (Eps rinvariant) \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> s u) = 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) u (Eps rinvariant) \<down> t | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> t u) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False)
[PROOF STEP]
by (auto split: ipc_stage_t.splits ev_wait_stage_t.splits ev_consume_t.splits)
[PROOF STATE]
proof (state)
this:
rwaiting s u a = rwaiting t u a

goal (2 subgoals):
 1. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> rwaiting s u a = rwaiting t u a
 2. a = NONE \<Longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
qed (simp add: waiting_def, simp add: waiting_def)
[PROOF STATE]
proof (state)
this:
rwaiting s u a = rwaiting t u a

goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>rvpeq (rcurrent ?s2) ?s2 ?t2; \<forall>d\<in>rkinvolved ?a2. rvpeq d ?s2 ?t2; rvpeq ?u2 ?s2 ?t2\<rbrakk> \<Longrightarrow> rwaiting ?s2 ?u2 ?a2 = rwaiting ?t2 ?u2 ?a2

goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rvpeq (rcurrent ?s2) ?s2 ?t2; \<forall>d\<in>rkinvolved ?a2. rvpeq d ?s2 ?t2; rvpeq ?u2 ?s2 ?t2\<rbrakk> \<Longrightarrow> rwaiting ?s2 ?u2 ?a2 = rwaiting ?t2 ?u2 ?a2

goal (1 subgoal):
 1. \<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s t u a. rvpeq (rcurrent s) s t \<and> (\<forall>d\<in>rkinvolved a. rvpeq d s t) \<and> rvpeq u s t \<longrightarrow> rwaiting s u a = rwaiting t u a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipc_precondition_ensures_ifp:
assumes "ipc_precondition (current s) dir partner page s"
    and "atomic_step_invariant s"
shows "rifp partner (current s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
let ?sp = "\<lambda> t1 t2 . Policy.sp_spec_subj_subj (partition t1) (partition t2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
have "?sp (current s) partner \<or> ?sp partner (current s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ipc_precondition (current s) dir partner page s
atomic_step_invariant s

goal (1 subgoal):
 1. Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
unfolding ipc_precondition_def atomic_step_invariant_def sp_subset_def
[PROOF STATE]
proof (prove)
using this:
let sender = case dir of SEND \<Rightarrow> current s | RECV \<Rightarrow> partner; receiver = case dir of SEND \<Rightarrow> partner | RECV \<Rightarrow> current s; 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 (current s)) (PAGE page) local_access_mode
(\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)

goal (1 subgoal):
 1. Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
by (cases dir, auto)
[PROOF STATE]
proof (state)
this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))

goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))

goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
unfolding rifp_def
[PROOF STATE]
proof (prove)
using this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))

goal (1 subgoal):
 1. Policy.ifp (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
using Policy_properties.ifp_compatible_with_sp_spec
[PROOF STATE]
proof (prove)
using this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
\<forall>a b. Policy.sp_spec_subj_subj a b \<longrightarrow> Policy.ifp a b \<and> Policy.ifp b a

goal (1 subgoal):
 1. Policy.ifp (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rifp partner (current s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ev_signal_precondition_ensures_ifp:
assumes "ev_signal_precondition (current s) partner s"
    and "atomic_step_invariant s"
shows "rifp partner (current s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
let ?sp = "\<lambda> t1 t2 . Policy.sp_spec_subj_subj (partition t1) (partition t2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
have "?sp (current s) partner \<or> ?sp partner (current s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ev_signal_precondition (current s) partner s
atomic_step_invariant s

goal (1 subgoal):
 1. Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
unfolding ev_signal_precondition_def atomic_step_invariant_def sp_subset_def
[PROOF STATE]
proof (prove)
using this:
sp_impl_subj_subj s (Step.partition (current s)) (Step.partition partner)
(\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)

goal (1 subgoal):
 1. Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))

goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))

goal (1 subgoal):
 1. rifp partner (current s)
[PROOF STEP]
unfolding rifp_def
[PROOF STATE]
proof (prove)
using this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))

goal (1 subgoal):
 1. Policy.ifp (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
using Policy_properties.ifp_compatible_with_sp_spec
[PROOF STATE]
proof (prove)
using this:
Policy.sp_spec_subj_subj (Step.partition (current s)) (Step.partition partner) \<or> Policy.sp_spec_subj_subj (Step.partition partner) (Step.partition (current s))
\<forall>a b. Policy.sp_spec_subj_subj a b \<longrightarrow> Policy.ifp a b \<and> Policy.ifp b a

goal (1 subgoal):
 1. Policy.ifp (Step.partition partner) (Step.partition (current s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rifp partner (current s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma involved_ifp:
shows "\<forall> s a . \<forall> d \<in> rkinvolved a . rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
fix s a d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
assume d_involved: "d \<in> rkinvolved a"
[PROOF STATE]
proof (state)
this:
d \<in> rkinvolved a

goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
assume prec: "rprecondition s (rcurrent s) a"
[PROOF STATE]
proof (state)
this:
rprecondition s (rcurrent s) a

goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
from d_involved prec
[PROOF STATE]
proof (chain)
picking this:
d \<in> rkinvolved a
rprecondition s (rcurrent s) a
[PROOF STEP]
have "rifp d (rcurrent s)"
[PROOF STATE]
proof (prove)
using this:
d \<in> rkinvolved a
rprecondition s (rcurrent s) a

goal (1 subgoal):
 1. rifp d (rcurrent s)
[PROOF STEP]
using ipc_precondition_ensures_ifp ev_signal_precondition_ensures_ifp rstate_invariant
[PROOF STATE]
proof (prove)
using this:
d \<in> rkinvolved a
rprecondition s (rcurrent s) a
\<lbrakk>ipc_precondition (current ?s) ?dir ?partner ?page ?s; atomic_step_invariant ?s\<rbrakk> \<Longrightarrow> rifp ?partner (current ?s)
\<lbrakk>ev_signal_precondition (current ?s) ?partner ?s; atomic_step_invariant ?s\<rbrakk> \<Longrightarrow> rifp ?partner (current ?s)
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. rifp d (rcurrent s)
[PROOF STEP]
unfolding rkinvolved_def rprecondition_def atomic_step_precondition_def rcurrent_def Kernel.involved_def
[PROOF STATE]
proof (prove)
using this:
d \<in> (case a 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> {})
case a of SK_IPC dir PREP partner page \<Rightarrow> True | SK_IPC dir WAIT partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> s | SK_IPC dir (BUF page') partner page \<Rightarrow> ipc_precondition (current \<down> s) dir partner page \<down> s \<and> ipc_precondition partner (opposite_ipc_direction dir) (current \<down> 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 (current \<down> s) partner \<down> s | NONE \<Rightarrow> True
\<lbrakk>ipc_precondition (current ?s) ?dir ?partner ?page ?s; atomic_step_invariant ?s\<rbrakk> \<Longrightarrow> rifp ?partner (current ?s)
\<lbrakk>ev_signal_precondition (current ?s) ?partner ?s; atomic_step_invariant ?s\<rbrakk> \<Longrightarrow> rifp ?partner (current ?s)
atomic_step_invariant \<down> ?s

goal (1 subgoal):
 1. rifp d (current \<down> s)
[PROOF STEP]
by(cases a,simp,auto split: int_point_t.splits ipc_stage_t.splits ev_signal_stage_t.splits)
[PROOF STATE]
proof (state)
this:
rifp d (rcurrent s)

goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?d2 \<in> rkinvolved ?a2; rprecondition ?s2 (rcurrent ?s2) ?a2\<rbrakk> \<Longrightarrow> rifp ?d2 (rcurrent ?s2)

goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?d2 \<in> rkinvolved ?a2; rprecondition ?s2 (rcurrent ?s2) ?a2\<rbrakk> \<Longrightarrow> rifp ?d2 (rcurrent ?s2)

goal (1 subgoal):
 1. \<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s a. \<forall>d\<in>rkinvolved a. rprecondition s (rcurrent s) a \<longrightarrow> rifp d (rcurrent s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_of_waiting_ev:
shows "\<forall>s a. rwaiting s (rcurrent s) (SK_EV_WAIT EV_FINISH EV_CONSUME_ALL)
               \<longrightarrow> rstep s a = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. rwaiting s (rcurrent s) (SK_EV_WAIT EV_FINISH EV_CONSUME_ALL) \<longrightarrow> rstep s a = s
[PROOF STEP]
unfolding waiting_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. (case SK_EV_WAIT EV_FINISH EV_CONSUME_ALL of SK_IPC dir WAIT partner page \<Rightarrow> \<not> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) (Eps rinvariant) \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> s (rcurrent s)) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False) \<longrightarrow> rstep s a = s
[PROOF STEP]
by auto


[STATEMENT]
lemma spec_of_waiting_ev_w:
shows "\<forall>s a. rwaiting s (rcurrent s) (SK_EV_WAIT EV_WAIT EV_CONSUME_ALL)
               \<longrightarrow> rstep s (SK_EV_WAIT EV_WAIT EV_CONSUME_ALL) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. rwaiting s (rcurrent s) (SK_EV_WAIT EV_WAIT EV_CONSUME_ALL) \<longrightarrow> rstep s (SK_EV_WAIT EV_WAIT EV_CONSUME_ALL) = s
[PROOF STEP]
unfolding rstep_def atomic_step_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. rwaiting s (rcurrent s) (SK_EV_WAIT EV_WAIT EV_CONSUME_ALL) \<longrightarrow> \<up> case SK_EV_WAIT EV_WAIT EV_CONSUME_ALL 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 = s
[PROOF STEP]
by (auto split: int_point_t.splits ipc_stage_t.splits ev_wait_stage_t.splits)


[STATEMENT]
lemma spec_of_waiting:
shows "\<forall>s a. rwaiting s (rcurrent s) a \<longrightarrow> rstep s a = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. rwaiting s (rcurrent s) a \<longrightarrow> rstep s a = s
[PROOF STEP]
unfolding waiting_def rstep_def atomic_step_def atomic_step_ipc_def
          atomic_step_ev_signal_def atomic_step_ev_wait_all_def
          atomic_step_ev_wait_one_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a. (case a of SK_IPC dir WAIT partner page \<Rightarrow> \<not> ipc_precondition partner (opposite_ipc_direction dir) (rcurrent s) (Eps rinvariant) \<down> s | SK_IPC dir _ partner page \<Rightarrow> False | SK_EV_WAIT EV_WAIT x \<Rightarrow> ev_counter (thread \<down> s (rcurrent s)) = 0 | SK_EV_WAIT _ x \<Rightarrow> False | _ \<Rightarrow> False) \<longrightarrow> \<up> case a of SK_IPC SEND (BUF page') partner page \<Rightarrow> set_object_value (PAGE page') (obj \<down> s (PAGE page)) \<down> s | SK_IPC RECV (BUF page') partner page \<Rightarrow> \<down> s | SK_IPC dir _ partner page \<Rightarrow> \<down> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> \<down> s\<lparr>thread := (thread \<down> s)(current \<down> s := thread \<down> s (current \<down> s)\<lparr>ev_counter := 0\<rparr>)\<rparr> | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> \<down> s\<lparr>thread := (thread \<down> s)(current \<down> s := thread \<down> s (current \<down> s)\<lparr>ev_counter := ev_counter (thread \<down> s (current \<down> s)) - 1\<rparr>)\<rparr> | 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> \<down> s\<lparr>thread := (thread \<down> s)(partner := thread \<down> s partner\<lparr>ev_counter := Suc (ev_counter (thread \<down> s partner))\<rparr>)\<rparr> | NONE \<Rightarrow> \<down> s = s
[PROOF STEP]
by(auto split: int_point_t.splits ipc_stage_t.splits ev_wait_stage_t.splits)


[STATEMENT]
lemma ty_def2 [simp]: "P,E \<turnstile>1 e :: T \<Longrightarrow> ty E e = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>1 e :: T \<Longrightarrow> ty E e = T
[PROOF STEP]
apply(unfold ty_def ty_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile>1 e :: T \<Longrightarrow> (THE T. P,E \<turnstile>1 e :: T) = T
[PROOF STEP]
apply(blast intro: the_equality WT1_unique[OF wf_prog])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ty\<^sub>i'_None [simp]: "ty\<^sub>i' ST E None = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>i' ST E None = None
[PROOF STEP]
by(simp add:ty\<^sub>i'_def)


[STATEMENT]
lemma ty\<^sub>l_app_diff[simp]:
 "ty\<^sub>l (E@[T]) (A - {size E}) = ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>l (E @ [T]) (A - {length E}) = ty\<^sub>l E A
[PROOF STEP]
by(auto simp add:ty\<^sub>l_def hyperset_defs)


[STATEMENT]
lemma ty\<^sub>i'_app_diff[simp]:
 "ty\<^sub>i' ST (E @ [T]) (A \<ominus> size E) = ty\<^sub>i' ST E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty\<^sub>i' ST (E @ [T]) (A \<ominus> length E) = ty\<^sub>i' ST E A
[PROOF STEP]
by(auto simp add:ty\<^sub>i'_def hyperset_defs)


[STATEMENT]
lemma ty\<^sub>l_antimono:
 "A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>l E A' [\<le>\<^sub>\<top>] ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>l E A' [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
by(auto simp:ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma ty\<^sub>i'_antimono:
 "A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma ty\<^sub>l_env_antimono:
 "P \<turnstile> ty\<^sub>l (E@[T]) A [\<le>\<^sub>\<top>] ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>l (E @ [T]) A [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
by(auto simp:ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma ty\<^sub>i'_env_antimono:
 "P \<turnstile> ty\<^sub>i' ST (E@[T]) A \<le>' ty\<^sub>i' ST E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>i' ST (E @ [T]) A \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma ty\<^sub>i'_incr:
 "P \<turnstile> ty\<^sub>i' ST (E @ [T]) \<lfloor>insert (size E) A\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>i' ST (E @ [T]) \<lfloor>insert (length E) A\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma ty\<^sub>l_incr:
 "P \<turnstile> ty\<^sub>l (E @ [T]) (insert (size E) A) [\<le>\<^sub>\<top>] ty\<^sub>l E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ty\<^sub>l (E @ [T]) (insert (length E) A) [\<le>\<^sub>\<top>] ty\<^sub>l E A
[PROOF STEP]
by(auto simp: hyperset_defs ty\<^sub>l_def list_all2_conv_all_nth)


[STATEMENT]
lemma ty\<^sub>l_in_types:
 "set E \<subseteq> types P \<Longrightarrow> ty\<^sub>l E A \<in> list mxl (err (types P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set E \<subseteq> types P \<Longrightarrow> ty\<^sub>l E A \<in> list mxl (err (types P))
[PROOF STEP]
by(auto simp add:ty\<^sub>l_def intro!:listI dest!: nth_mem)


[STATEMENT]
lemma compT_sizes[simp]:
  shows "size(compT E A ST e) = size(compE2 e) - 1"
  and "size(compTs E A ST es) = size(compEs2 es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (compT E A ST e) = length (compE2 e) - 1 &&& length (compTs E A ST es) = length (compEs2 es)
[PROOF STEP]
apply(induct E A ST e and E A ST es rule: compT_compTs_induct)
[PROOF STATE]
proof (prove)
goal (26 subgoals):
 1. \<And>E A ST C. length (compT E A ST (new C)) = length (compE2 (new C)) - 1
 2. \<And>E A ST T e. length (compT E A ST e) = length (compE2 e) - 1 \<Longrightarrow> length (compT E A ST (newA T\<lfloor>e\<rceil>)) = length (compE2 (newA T\<lfloor>e\<rceil>)) - 1
 3. \<And>E A ST C e. length (compT E A ST e) = length (compE2 e) - 1 \<Longrightarrow> length (compT E A ST (Cast C e)) = length (compE2 (Cast C e)) - 1
 4. \<And>E A ST e T. length (compT E A ST e) = length (compE2 e) - 1 \<Longrightarrow> length (compT E A ST (e instanceof T)) = length (compE2 (e instanceof T)) - 1
 5. \<And>E A ST v. length (compT E A ST (Val v)) = length (compE2 (Val v)) - 1
 6. \<And>E A ST e1 bop e2. \<lbrakk>length (compT E A ST e1) = length (compE2 e1) - 1; length (compT E (A \<squnion> \<A> e1) (ty E e1 # ST) e2) = length (compE2 e2) - 1\<rbrakk> \<Longrightarrow> length (compT E A ST (e1 \<guillemotleft>bop\<guillemotright> e2)) = length (compE2 (e1 \<guillemotleft>bop\<guillemotright> e2)) - 1
 7. \<And>E A ST i. length (compT E A ST (Var i)) = length (compE2 (Var i)) - 1
 8. \<And>E A ST i e. length (compT E A ST e) = length (compE2 e) - 1 \<Longrightarrow> length (compT E A ST (i:=e)) = length (compE2 (i:=e)) - 1
 9. \<And>E A ST a i. \<lbrakk>length (compT E A ST a) = length (compE2 a) - 1; length (compT E (A \<squnion> \<A> a) (ty E a # ST) i) = length (compE2 i) - 1\<rbrakk> \<Longrightarrow> length (compT E A ST (a\<lfloor>i\<rceil>)) = length (compE2 (a\<lfloor>i\<rceil>)) - 1
 10. \<And>E A ST a i e. \<lbrakk>length (compT E A ST a) = length (compE2 a) - 1; length (compT E (A \<squnion> \<A> a) (ty E a # ST) i) = length (compE2 i) - 1; length (compT E (A \<squnion> \<A> a \<squnion> \<A> i) (ty E i # ty E a # ST) e) = length (compE2 e) - 1\<rbrakk> \<Longrightarrow> length (compT E A ST (a\<lfloor>i\<rceil> := e)) = length (compE2 (a\<lfloor>i\<rceil> := e)) - 1
A total of 26 subgoals...
[PROOF STEP]
apply(auto split:nat_diff_split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compT_None_not_Some [simp]: "\<lfloor>\<tau>\<rfloor> \<notin> set (compT E None ST e)"
  and compTs_None_not_Some [simp]: "\<lfloor>\<tau>\<rfloor> \<notin> set (compTs E None ST es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<tau>\<rfloor> \<notin> set (compT E None ST e) &&& \<lfloor>\<tau>\<rfloor> \<notin> set (compTs E None ST es)
[PROOF STEP]
by(induct E A\<equiv>"None :: nat hyperset" ST e and E A\<equiv>"None :: nat hyperset" ST es rule: compT_compTs_induct) (simp_all add:after_def)


[STATEMENT]
lemma pair_eq_ty\<^sub>i'_conv:
  "(\<lfloor>(ST, LT)\<rfloor> = ty\<^sub>i' ST\<^sub>0 E A) = (case A of None \<Rightarrow> False | Some A \<Rightarrow> (ST = ST\<^sub>0 \<and> LT = ty\<^sub>l E A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lfloor>(ST, LT)\<rfloor> = ty\<^sub>i' ST\<^sub>0 E A) = (case A of None \<Rightarrow> False | \<lfloor>A\<rfloor> \<Rightarrow> ST = ST\<^sub>0 \<and> LT = ty\<^sub>l E A)
[PROOF STEP]
by(simp add:ty\<^sub>i'_def)


[STATEMENT]
lemma pair_conv_ty\<^sub>i': "\<lfloor>(ST, ty\<^sub>l E A)\<rfloor> = ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(ST, ty\<^sub>l E A)\<rfloor> = ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
by(simp add:ty\<^sub>i'_def)


[STATEMENT]
lemma ty\<^sub>i'_antimono2:
 "\<lbrakk> E \<le> E'; A \<subseteq> A' \<rbrakk> \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E' \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>E \<le> E'; A \<subseteq> A'\<rbrakk> \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E' \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth less_eq_list_def prefix_def)