Merge pull request #167 in SEL4/l4v from hv_inv_ex to master

* commit '8a7d450f3a1c7b509e01eed107abdf64e7cc4618':
  ainvs + refine: remove hv_inv_ex

proof/invariant-abstract/ARM/ArchSyscall_AI.thy

@@ -70,14 +70,6 @@ lemma hv_invs[wp, Syscall_AI_assms]: "\<lbrace>invs\<rbrace> handle_vm_fault t'
   apply (wp|simp)+
   done
 
-lemma hv_inv_ex [Syscall_AI_assms]:
-  "\<lbrace>P\<rbrace> handle_vm_fault t vp \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>"
-  apply (cases vp, simp_all)
-  apply (wp dmo_inv getDFSR_inv getFAR_inv getIFSR_inv getRestartPC_inv 
-            det_getRestartPC as_user_inv
-         | wpcw | simp)+
-  done
-
 lemma handle_vm_fault_valid_fault[wp, Syscall_AI_assms]:
   "\<lbrace>\<top>\<rbrace> handle_vm_fault thread ft -,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>"
   apply (cases ft, simp_all)

proof/invariant-abstract/Syscall_AI.thy

@@ -417,8 +417,6 @@ locale Syscall_AI = Systemcall_AI_Pre:Systemcall_AI_Pre _ state_ext_t
         \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s"
   assumes hv_invs[wp]:
     "\<And>t' flt. \<lbrace>invs :: 'state_ext state \<Rightarrow> bool\<rbrace> handle_vm_fault t' flt \<lbrace>\<lambda>r. invs\<rbrace>"
-  assumes hv_inv_ex:
-    "\<And>P t vp. \<lbrace>P :: 'state_ext state \<Rightarrow> bool\<rbrace> handle_vm_fault t vp \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>"
   assumes handle_vm_fault_valid_fault[wp]:
     "\<And>thread ft.
       \<lbrace>\<top>::'state_ext state \<Rightarrow> bool\<rbrace> handle_vm_fault thread ft -,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>"

proof/refine/ARM/Syscall_R.thy

@@ -2310,7 +2310,7 @@ proof -
            apply (erule hf_corres)
           apply (rule hv_corres)
          apply (rule hoare_elim_pred_conjE2)
-         apply (rule hoare_vcg_E_conj, rule validE_validE_E[OF hv_inv_ex])
+         apply (rule hoare_vcg_E_conj, rule valid_validE_E, wp)
          apply (wp handle_vm_fault_valid_fault)
         apply (rule hv_inv_ex')
        apply wp