theory Retype_C

lemma createObject_IRQHandler:
  "\<lbrace>\<top>\<rbrace> createObject ty ptr us dev
    \<lbrace>\<lambda>rv s. rv = IRQHandlerCap x \<longrightarrow> P rv s x\<rbrace>" apply (simp add:createObject_def3) apply (rule hoare_pre) apply wp apply (rule_tac Q = "\<lambda>r s. r \<noteq> [] \<and> Q r s" for Q in hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule hoare_strengthen_post[OF createNewCaps_ret_len]) apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\<lambda>_ _. False"]]) apply assumption apply (rename_tac rv s) apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv s. rv = capability.IRQHandlerCap x \<longrightarrow> P rv s x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>m a. hd m = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) a x\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q3 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q3\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>r s. r \<noteq> [] \<and> ?Q15 r s\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q15 rv s \<Longrightarrow> hd rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x
 3. \<And>s. True \<Longrightarrow> ?Q3 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P16\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>rv s. rv \<noteq> []\<rbrace>
 2. \<lbrace>?P'16\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q15\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q15 rv s \<Longrightarrow> hd rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x
 4. \<And>s. True \<Longrightarrow> ?P16 s \<and> ?P'16 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. Suc 0 = length rv \<Longrightarrow> rv \<noteq> []
 2. \<lbrace>?P'16\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q15\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q15 rv s \<Longrightarrow> hd rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x
 4. \<And>s. True \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'16 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'16\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q15\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q15 rv s \<Longrightarrow> hd rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x
 3. \<And>s. True \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'16 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. capability.IRQHandlerCap x \<in> set rv \<longrightarrow> False \<Longrightarrow> ?Q15 rv s
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q15 rv s \<Longrightarrow> hd rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x
 3. \<And>s. True \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (capability.IRQHandlerCap x \<in> set rv \<longrightarrow> False) \<Longrightarrow> hd rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x
 2. \<And>s. True \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (capability.IRQHandlerCap x \<in> set rv \<longrightarrow> False) \<Longrightarrow> hd rv = capability.IRQHandlerCap x \<longrightarrow> P (capability.IRQHandlerCap x) s x
 2. \<And>s. True \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> True proof (prove)
goal:
No subgoals!