theory Finalise_IF

lemma finalise_cap_globals_equiv:
  "\<lbrace>globals_equiv st and invs and valid_cap cap
                     and (\<lambda>s. \<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)\<rbrace>
   finalise_cap cap b
   \<lbrace>\<lambda> _. globals_equiv st\<rbrace>" apply (induct cap; simp) by (wp cancel_all_ipc_globals_equiv cancel_all_ipc_valid_global_objs
         cancel_all_signals_globals_equiv cancel_all_signals_valid_global_objs
         arch_finalise_cap_globals_equiv unbind_maybe_notification_globals_equiv
         unbind_notification_globals_equiv liftM_wp when_def
      | clarsimp simp: valid_cap_def | intro impI conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and valid_cap cap and (\<lambda>s. \<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)\<rbrace> finalise_cap cap b \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>x1 x2 x3 x4. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> UntypedCap x1 x2 x3 x4\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>x1 x2 x3. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> EndpointCap x1 x2 x3\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when b (cancel_all_ipc x1)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>x1 x2 x3. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> NotificationCap x1 x2 x3\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when b (do y <- unbind_maybe_notification x1;
cancel_all_signals x1
od)) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>x1 x2 x3. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> ReplyCap x1 x2 x3\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>x1 x2 x3. (b \<longrightarrow> \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> CNodeCap x1 x2 x3\<rbrace> return (Zombie x1 (Some x2) (2 ^ x2), NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<and> (\<not> b \<longrightarrow> \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> CNodeCap x1 x2 x3\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>)
 7. \<And>x. (b \<longrightarrow> \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> ThreadCap x \<and> x \<noteq> idle_thread a\<rbrace> do y <- unbind_notification x;
y <- suspend x;
y <- prepare_thread_delete x;
return (Zombie x None 5, NullCap)
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<and> (\<not> b \<longrightarrow> \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> ThreadCap x \<and> x \<noteq> idle_thread a\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>)
 8. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> DomainCap\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 9. \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> IRQControlCap\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 10. \<And>x. (b \<longrightarrow> \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> IRQHandlerCap x\<rbrace> do y <- deleting_irq_handler x;
return (NullCap, IRQHandlerCap x)
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<and> (\<not> b \<longrightarrow> \<lbrace>\<lambda>a. globals_equiv st a \<and> invs a \<and> a \<turnstile> IRQHandlerCap x\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>)
A total of 12 subgoals...