theory Finalise_AI

lemma emptyable_no_reply_cap:
  assumes e: "emptyable sl s"
  and   mdb: "reply_caps_mdb (mdb s) (caps_of_state s)"
  and    vr: "valid_reply_caps s"
  and    vm: "valid_reply_masters s"
  and    vo: "valid_objs s"
  and    rc: "\<exists> R. caps_of_state s sl' = Some (cap.ReplyCap t False R)"
  and    rp: "mdb s sl' = Some sl"
  shows      "False" proof - have rm:
    "\<exists> R. caps_of_state s sl = Some (cap.ReplyCap t True R)" using mdb rc rp unfolding reply_caps_mdb_def by fastforce have tcb_slot:
    "sl = (t, tcb_cnode_index 2)" using vm rm unfolding valid_reply_masters_def by (fastforce simp: cte_wp_at_caps_of_state is_master_reply_cap_to_def) have tcb_halted:
    "st_tcb_at halted t s" using vo rm tcb_slot e unfolding emptyable_def by (fastforce dest: caps_of_state_valid_cap simp: valid_cap_def) have tcb_not_halted:
    "st_tcb_at (Not \<circ> halted) t s" using vr rc unfolding valid_reply_caps_def by (fastforce simp add: has_reply_cap_def is_reply_cap_to_def cte_wp_at_caps_of_state
                 simp del: split_paired_Ex
                    elim!: pred_tcb_weakenE) show ?thesis using tcb_halted tcb_not_halted by (clarsimp simp: st_tcb_def2) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (state)
goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<exists>R. caps_of_state s sl = Some (ReplyCap t True R) proof (prove)
using this:
reply_caps_mdb (mdb s) (caps_of_state s)
\<exists>R. caps_of_state s sl' = Some (ReplyCap t False R)
mdb s sl' = Some sl

goal (1 subgoal):
 1. \<exists>R. caps_of_state s sl = Some (ReplyCap t True R) proof (prove)
using this:
\<forall>ptr t rights. caps_of_state s ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. mdb s ptr = Some ptr' \<and> caps_of_state s ptr' = Some (ReplyCap t True rights'))
\<exists>R. caps_of_state s sl' = Some (ReplyCap t False R)
mdb s sl' = Some sl

goal (1 subgoal):
 1. \<exists>R. caps_of_state s sl = Some (ReplyCap t True R) proof (state)
this:
\<exists>R. caps_of_state s sl = Some (ReplyCap t True R)

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. sl = (t, tcb_cnode_index 2) proof (prove)
using this:
valid_reply_masters s
\<exists>R. caps_of_state s sl = Some (ReplyCap t True R)

goal (1 subgoal):
 1. sl = (t, tcb_cnode_index 2) proof (prove)
using this:
\<forall>p t. cte_wp_at (is_master_reply_cap_to t) p s \<longrightarrow> p = (t, tcb_cnode_index 2)
\<exists>R. caps_of_state s sl = Some (ReplyCap t True R)

goal (1 subgoal):
 1. sl = (t, tcb_cnode_index 2) proof (state)
this:
sl = (t, tcb_cnode_index 2)

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. st_tcb_at halted t s proof (prove)
using this:
valid_objs s
\<exists>R. caps_of_state s sl = Some (ReplyCap t True R)
sl = (t, tcb_cnode_index 2)
emptyable sl s

goal (1 subgoal):
 1. st_tcb_at halted t s proof (prove)
using this:
valid_objs s
\<exists>R. caps_of_state s sl = Some (ReplyCap t True R)
sl = (t, tcb_cnode_index 2)
tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s

goal (1 subgoal):
 1. st_tcb_at halted t s proof (state)
this:
st_tcb_at halted t s

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. st_tcb_at (Not \<circ> halted) t s proof (prove)
using this:
valid_reply_caps s
\<exists>R. caps_of_state s sl' = Some (ReplyCap t False R)

goal (1 subgoal):
 1. st_tcb_at (Not \<circ> halted) t s proof (prove)
using this:
(\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)
\<exists>R. caps_of_state s sl' = Some (ReplyCap t False R)

goal (1 subgoal):
 1. st_tcb_at (Not \<circ> halted) t s proof (state)
this:
st_tcb_at (Not \<circ> halted) t s

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
st_tcb_at halted t s
st_tcb_at (Not \<circ> halted) t s

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!