lib: reorder assumptions of no_fail_bind
In order to aid wp-style reasoning Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
parent
ea943b5a6d
commit
b94a78c88c
|
@ -130,7 +130,7 @@ lemma no_fail_returnOK[simp, wp]:
|
|||
by (simp add: returnOk_def)
|
||||
|
||||
lemma no_fail_bind[wp]:
|
||||
"\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
|
||||
"\<lbrakk> \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
|
||||
unfolding no_fail_def bind_def
|
||||
using post_by_hoare by fastforce
|
||||
|
||||
|
|
|
@ -934,10 +934,10 @@ lemma terminates_spec_no_fail:
|
|||
using normal by auto
|
||||
show ?thesis
|
||||
apply (clarsimp simp: ac AC_call_L1_def L2_call_L1_def)
|
||||
apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select
|
||||
wp_del: select_f_wp)
|
||||
apply (wpsimp wp_del: select_f_wp)
|
||||
apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce)
|
||||
apply (wpsimp wp: nf_pre)+
|
||||
apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select)+
|
||||
apply (fastforce simp: nf_pre)
|
||||
done
|
||||
qed
|
||||
|
||||
|
|
|
@ -193,7 +193,6 @@ lemma handleInterrupt_no_fail:
|
|||
|
||||
lemma handleEvent_Interrupt_no_fail: "no_fail (invs' and ex_abs einvs) (handleEvent Interrupt)"
|
||||
apply (simp add: handleEvent_def)
|
||||
apply (rule no_fail_pre)
|
||||
apply wp
|
||||
apply (rule handleInterrupt_no_fail)
|
||||
apply (simp add: crunch_simps)
|
||||
|
@ -204,12 +203,10 @@ lemma handleEvent_Interrupt_no_fail: "no_fail (invs' and ex_abs einvs) (handleEv
|
|||
apply (rule hoare_vcg_conj_lift)
|
||||
apply (rule corres_ex_abs_lift)
|
||||
apply (rule dmo_getActiveIRQ_corres)
|
||||
apply wp
|
||||
apply simp
|
||||
apply wp
|
||||
apply simp
|
||||
apply (rule doMachineOp_getActiveIRQ_IRQ_active)
|
||||
apply wpsimp
|
||||
apply (wpsimp wp: doMachineOp_getActiveIRQ_IRQ_active)
|
||||
apply clarsimp
|
||||
apply wpsimp
|
||||
apply (clarsimp simp: invs'_def valid_state'_def)
|
||||
done
|
||||
|
||||
|
|
|
@ -271,8 +271,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]:
|
|||
lemma no_fail_invalidateCacheRange_RAM[simp, wp]:
|
||||
"no_fail \<top> (invalidateCacheRange_RAM s e p)"
|
||||
apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def)
|
||||
apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp)
|
||||
apply (auto intro: hoare_post_taut)
|
||||
apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb)
|
||||
done
|
||||
|
||||
lemma no_fail_branchFlushRange[simp, wp]:
|
||||
|
|
|
@ -280,8 +280,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]:
|
|||
lemma no_fail_invalidateCacheRange_RAM[simp, wp]:
|
||||
"no_fail \<top> (invalidateCacheRange_RAM s e p)"
|
||||
apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def)
|
||||
apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp)
|
||||
apply (auto intro: hoare_post_taut)
|
||||
apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb)
|
||||
done
|
||||
|
||||
lemma no_fail_branchFlushRange[simp, wp]:
|
||||
|
|
|
@ -1600,8 +1600,7 @@ lemma no_fail_asUser [wp]:
|
|||
apply (simp add: asUser_def split_def)
|
||||
apply wp
|
||||
apply (simp add: no_fail_def)
|
||||
apply (wp hoare_drop_imps)
|
||||
apply simp
|
||||
apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
|
||||
done
|
||||
|
||||
lemma asUser_setRegister_corres:
|
||||
|
|
|
@ -1535,8 +1535,7 @@ lemma no_fail_asUser [wp]:
|
|||
apply (simp add: asUser_def split_def)
|
||||
apply wp
|
||||
apply (simp add: no_fail_def)
|
||||
apply (wp hoare_drop_imps)
|
||||
apply simp
|
||||
apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
|
||||
done
|
||||
|
||||
lemma asUser_setRegister_corres:
|
||||
|
|
|
@ -341,9 +341,7 @@ lemma invokeTCB_WriteRegisters_corres:
|
|||
apply (rule asUser_corres)
|
||||
apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def)
|
||||
apply (rule corres_Id, simp+)
|
||||
apply (rule no_fail_pre, wp no_fail_mapM)
|
||||
apply clarsimp
|
||||
apply (wp no_fail_setRegister | simp)+
|
||||
apply (wpsimp wp: no_fail_mapM no_fail_setRegister)+
|
||||
apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
|
||||
apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]])
|
||||
apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]])
|
||||
|
|
|
@ -1582,8 +1582,7 @@ lemma no_fail_asUser [wp]:
|
|||
apply (simp add: asUser_def split_def)
|
||||
apply wp
|
||||
apply (simp add: no_fail_def)
|
||||
apply (wp hoare_drop_imps)
|
||||
apply simp
|
||||
apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
|
||||
done
|
||||
|
||||
lemma asUser_setRegister_corres:
|
||||
|
|
|
@ -1569,8 +1569,7 @@ lemma no_fail_asUser [wp]:
|
|||
apply (simp add: asUser_def split_def)
|
||||
apply wp
|
||||
apply (simp add: no_fail_def)
|
||||
apply (wp hoare_drop_imps)
|
||||
apply simp
|
||||
apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
|
||||
done
|
||||
|
||||
lemma asUser_setRegister_corres:
|
||||
|
|
|
@ -329,8 +329,8 @@ lemma invokeTCB_WriteRegisters_corres:
|
|||
apply (clarsimp simp: mask_def user_vtop_def
|
||||
cong: if_cong)
|
||||
apply simp
|
||||
apply (rule no_fail_pre, wp no_fail_mapM)
|
||||
apply (clarsimp, (wp no_fail_setRegister | simp)+)
|
||||
apply (wpsimp wp: no_fail_mapM no_fail_setRegister)
|
||||
apply simp
|
||||
apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
|
||||
apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]])
|
||||
apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]])
|
||||
|
|
|
@ -1448,10 +1448,7 @@ lemma no_fail_nativeThreadUsingFPU[wp]:
|
|||
"no_fail (\<top> and \<top>) (X64.nativeThreadUsingFPU thread)"
|
||||
supply Collect_const[simp del]
|
||||
apply (simp only: X64.nativeThreadUsingFPU_def)
|
||||
apply (rule no_fail_bind)
|
||||
apply (simp add: Arch.no_fail_machine_op_lift)
|
||||
apply simp
|
||||
apply wp
|
||||
apply (wpsimp wp: Arch.no_fail_machine_op_lift)
|
||||
done
|
||||
|
||||
lemma (in delete_one) prepareThreadDelete_corres:
|
||||
|
|
|
@ -1562,8 +1562,7 @@ lemma no_fail_asUser [wp]:
|
|||
apply (simp add: asUser_def split_def)
|
||||
apply wp
|
||||
apply (simp add: no_fail_def)
|
||||
apply (wp hoare_drop_imps)
|
||||
apply simp
|
||||
apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
|
||||
done
|
||||
|
||||
lemma asUser_setRegister_corres:
|
||||
|
|
|
@ -344,7 +344,7 @@ lemma invokeTCB_WriteRegisters_corres:
|
|||
mask_def user_vtop_def
|
||||
cong: if_cong)
|
||||
apply simp
|
||||
apply (rule no_fail_pre, wp no_fail_mapM)
|
||||
apply (wpsimp wp: no_fail_mapM no_fail_setRegister)
|
||||
apply (clarsimp simp: sanitiseOrFlags_def sanitiseAndFlags_def)
|
||||
apply ((safe)[1], (wp no_fail_setRegister | simp)+)
|
||||
apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
|
||||
|
|
|
@ -47,7 +47,7 @@ proof (induct n arbitrary: m rule: less_induct)
|
|||
|
||||
show "no_ofail (\<lambda>_. unat x < m) (factorial' m x)"
|
||||
apply (subst factorial'.simps)
|
||||
apply (wp induct_asm ovalid_post_triv)
|
||||
apply (wpsimp wp: induct_asm ovalid_post_triv)
|
||||
apply unat_arith
|
||||
done
|
||||
qed
|
||||
|
|
Loading…
Reference in New Issue