theory KHeap_DR

lemma invs_mdb_fast_finalise[wp]:
  "\<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>%r. valid_mdb\<rbrace>" apply (case_tac p; simp) apply (wp,simp add:valid_state_def invs_def) apply (rule hoare_post_imp[where Q="%r. invs"]) apply (clarsimp simp:valid_state_def invs_def,wp cancel_all_ipc_invs) apply clarsimp apply (rule hoare_post_imp[where Q="%r. invs"]) apply (clarsimp simp:valid_state_def invs_def,wp unbind_maybe_notification_invs cancel_all_signals_invs) apply clarsimp apply wp apply (simp add:valid_state_def invs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (4 subgoals):
 1. p = cap.NullCap \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 2. \<And>x31 x32 x33. p = cap.EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (IpcCancel_A.cancel_all_ipc x31) \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 3. \<And>x41 x42 x43. p = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 4. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33. p = cap.EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (IpcCancel_A.cancel_all_ipc x31) \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 2. \<And>x41 x42 x43. p = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 3. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 rv s. \<lbrakk>p = cap.EndpointCap x31 x32 x33; invs s\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<And>x31 x32 x33. p = cap.EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (IpcCancel_A.cancel_all_ipc x31) \<lbrace>\<lambda>r. invs\<rbrace>
 3. \<And>x41 x42 x43. p = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 4. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 s. \<lbrakk>p = cap.EndpointCap x31 x32 x33; invs s\<rbrakk> \<Longrightarrow> (if q then invs else invs) s
 2. \<And>x41 x42 x43. p = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 3. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43. p = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>r. valid_mdb\<rbrace>
 2. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43 rv s. \<lbrakk>p = cap.NotificationCap x41 x42 x43; invs s\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<And>x41 x42 x43. p = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs\<rbrace> when q (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>r. invs\<rbrace>
 3. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 s. \<lbrakk>p = cap.NotificationCap x41 x42 x43; invs s\<rbrakk> \<Longrightarrow> (if q then invs else invs) s
 2. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x51 x52 x53 s. \<lbrakk>p = cap.ReplyCap x51 x52 x53; invs s\<rbrakk> \<Longrightarrow> valid_mdb s proof (prove)
goal:
No subgoals!