theory Interrupt_AI

lemma cancel_ipc_noreply_interrupt_states:
  "\<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) t s \<and> P (interrupt_states s) \<rbrace> cancel_ipc t \<lbrace> \<lambda>_ s. P (interrupt_states s) \<rbrace>" apply (simp add: cancel_ipc_def) apply wpsimp apply (rule hoare_pre_cont) apply (wp) apply (wp gts_wp)+ apply (auto simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) t s \<and> P (interrupt_states s)\<rbrace> cancel_ipc t \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) t s \<and> P (interrupt_states s)\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>?R16 (ds_id BlockedOnReply)\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 2. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R15 state x7\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 3. \<And>state. idle state \<Longrightarrow> \<lbrace>?R13 state\<rbrace> return () \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 4. \<lbrace>?Q1\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (interrupt_states s)) \<and> (inactive state \<longrightarrow> P (interrupt_states s)) \<and> (state = Restart \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (interrupt_states s)) \<and> (awaiting_reply state \<longrightarrow> ?R16 state s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R15 state x s) \<and> (idle state \<longrightarrow> ?R13 state s)\<rbrace>
 5. \<And>s. st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) t s \<and> P (interrupt_states s) \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R15 state x7\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 2. \<And>state. idle state \<Longrightarrow> \<lbrace>?R13 state\<rbrace> return () \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 3. \<lbrace>?Q1\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (interrupt_states s)) \<and> (inactive state \<longrightarrow> P (interrupt_states s)) \<and> (state = Restart \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (interrupt_states s)) \<and> (awaiting_reply state \<longrightarrow> False) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R15 state x s) \<and> (idle state \<longrightarrow> ?R13 state s)\<rbrace>
 4. \<And>s. st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) t s \<and> P (interrupt_states s) \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>state. idle state \<Longrightarrow> \<lbrace>?R13 state\<rbrace> return () \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 2. \<lbrace>?Q1\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (interrupt_states s)) \<and> (inactive state \<longrightarrow> P (interrupt_states s)) \<and> (state = Restart \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (interrupt_states s)) \<and> (awaiting_reply state \<longrightarrow> False) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> P (interrupt_states s)) \<and> (idle state \<longrightarrow> ?R13 state s)\<rbrace>
 3. \<And>s. st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) t s \<and> P (interrupt_states s) \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) t s \<and> P (interrupt_states s) \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> (st = Running \<longrightarrow> P (interrupt_states s)) \<and> (inactive st \<longrightarrow> P (interrupt_states s)) \<and> (st = Restart \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> P (interrupt_states s)) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> P (interrupt_states s)) \<and> (awaiting_reply st \<longrightarrow> False) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> P (interrupt_states s)) \<and> (idle st \<longrightarrow> P (interrupt_states s)) proof (prove)
goal:
No subgoals!