theory Finalise_IF

lemma cancel_ipc_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at t and
                          (K (is_subject aag t))) (cancel_ipc t)" unfolding cancel_ipc_def apply (wp reads_respects_f[OF blocked_cancel_ipc_reads_respects, where st=st and Q="\<top>"]
            reply_cancel_ipc_reads_respects_f[where st=st]
            reads_respects_f[OF cancel_signal_owned_reads_respects, where st=st and Q="\<top>"]
            reads_respects_f[OF get_thread_state_rev, where st=st and Q="\<top>"] gts_wp
         | wpc | simp add: blocked_cancel_ipc_def | erule conjE)+ apply (clarsimp simp: st_tcb_at_def obj_at_def) apply (rule owns_thread_blocked_reads_endpoint) apply (simp add: st_tcb_at_def obj_at_def | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at t and K (is_subject aag t)) (cancel_ipc t) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at t and K (is_subject aag t)) (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) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; tcb_at t s; is_subject aag t\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> st_tcb_at ((=) (BlockedOnReceive x xa)) t s) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> st_tcb_at ((=) (BlockedOnSend x xa)) t s) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> aag_can_read aag x \<or> aag_can_affect aag l x) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; is_subject aag t; is_tcb (TCB tcb); kheap s t = Some (TCB tcb); tcb_state tcb = BlockedOnNotification x; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> aag_can_read aag x proof (prove)
goal (5 subgoals):
 1. \<And>s tcb x. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; is_subject aag t; is_tcb (TCB tcb); kheap s t = Some (TCB tcb); tcb_state tcb = BlockedOnNotification x; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> pas_refined aag (?s116 s tcb x)
 2. \<And>s tcb x. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; is_subject aag t; is_tcb (TCB tcb); kheap s t = Some (TCB tcb); tcb_state tcb = BlockedOnNotification x; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> invs (?s116 s tcb x)
 3. \<And>s tcb x. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; is_subject aag t; is_tcb (TCB tcb); kheap s t = Some (TCB tcb); tcb_state tcb = BlockedOnNotification x; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>y. y = ?state116 s tcb x) (?tptr116 s tcb x) (?s116 s tcb x)
 4. \<And>s tcb x. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; is_subject aag t; is_tcb (TCB tcb); kheap s t = Some (TCB tcb); tcb_state tcb = BlockedOnNotification x; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> is_subject aag (?tptr116 s tcb x)
 5. \<And>s tcb x. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; is_subject aag t; is_tcb (TCB tcb); kheap s t = Some (TCB tcb); tcb_state tcb = BlockedOnNotification x; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag x \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> ?state116 s tcb x = BlockedOnReceive x (?pl116 s tcb x) \<or> ?state116 s tcb x = BlockedOnSend x (?xb116 s tcb x) \<or> ?state116 s tcb x = BlockedOnNotification x proof (prove)
goal:
No subgoals!