theory KHeap_DR

lemma valid_idle_fast_finalise[wp]:
  "\<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>%r. valid_idle\<rbrace>" apply (case_tac p) apply simp_all 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_idle\<rbrace> proof (prove)
goal (12 subgoals):
 1. p = cap.NullCap \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 2. \<And>x21 x22 x23 x24. p = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>x31 x32 x33. p = cap.EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 4. \<And>x41 x42 x43. p = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 5. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 6. \<And>x61 x62 x63. p = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 7. \<And>x7. p = ThreadCap x7 \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 8. p = cap.DomainCap \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 9. p = IRQControlCap \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
 10. \<And>x10. p = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>\<lambda>r. valid_idle\<rbrace>
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. p = cap.NullCap \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_idle\<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_idle\<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_idle\<rbrace>
 4. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_idle\<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_idle\<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_idle\<rbrace>
 3. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_idle\<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_idle 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_idle\<rbrace>
 4. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_idle\<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_idle\<rbrace>
 3. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_idle\<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_idle\<rbrace>
 2. \<And>x51 x52 x53. p = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>r. valid_idle\<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_idle 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_idle\<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_idle\<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_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x51 x52 x53 s. \<lbrakk>p = cap.ReplyCap x51 x52 x53; invs s\<rbrakk> \<Longrightarrow> valid_idle s proof (prove)
goal:
No subgoals!