crefine: remove obsolete corres wpc setup

This setup didn't actually work. Replaced by corres_cases. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4 · Jun 26, 2023 · 48a9a2f · 48a9a2f
1 parent 79c7f8d
commit 48a9a2f
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 16 deletions.
diff --git a/proof/crefine/RISCV64/VSpace_C.thy b/proof/crefine/RISCV64/VSpace_C.thy
@@ -254,7 +254,7 @@ lemma handleVMFault_ccorres:
    apply (rule corres_split[OF read_stval_ccorres[ac]])
       apply terminates_trivial
      apply (drule sym, clarsimp)
-     apply (wpc; simp add: vm_fault_type_from_H_def vm_fault_defs_C bind_assoc)
+     apply (corres_cases; simp add: vm_fault_type_from_H_def vm_fault_defs_C bind_assoc)
           apply (rule returnVMFault_corres;
                  clarsimp simp: exception_defs mask_twice lift_rv_def mask_def vmFaultTypeFSR_def)+
      apply wpsimp+

diff --git a/proof/crefine/X64/VSpace_C.thy b/proof/crefine/X64/VSpace_C.thy
@@ -288,8 +288,8 @@ lemma handleVMFault_ccorres:
          apply simp
         apply terminates_trivial
        apply (drule sym, clarsimp)
-       apply (wpc; simp add: vm_fault_type_from_H_def X86InstructionFault_def X86DataFault_def
-                             bind_assoc)
+       apply (corres_cases; simp add: vm_fault_type_from_H_def X86InstructionFault_def X86DataFault_def
+                                      bind_assoc)
         apply (rule returnVMFault_corres;
                clarsimp simp: exception_defs mask_twice lift_rv_def)+
       apply wpsimp+
@@ -610,7 +610,7 @@ lemma lookupPDPTSlot_ccorres:
    apply (rule corres_symb_exec_lookupPML4Slot'; rename_tac pml4e_ptr)
    apply (rule corres_symb_exec_unknown_r; rename_tac undefined)
    apply (rule corres_symb_exec_pml4e_ptr_get_present'; rename_tac present)
-   apply wpc
+   apply corres_cases
     apply (rule_tac F="present = 0" in corres_gen_asm2)
     apply (simp add: bind_assoc)
     apply (rule corres_symb_exec_lookup_fault_missing_capability_new'; rename_tac lookup_fault)

diff --git a/proof/crefine/lib/AutoCorres_C.thy b/proof/crefine/lib/AutoCorres_C.thy
@@ -805,18 +805,6 @@ section \<open>Additional infrastructure\<close>
 
 context kernel begin
 
-lemma wpc_helper_corres_final:
-  "corres_underlying sr nf nf' rv Q Q' f f'
-   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (corres_underlying sr nf nf' rv P P' f f')"
-  apply (clarsimp simp: wpc_helper_def)
-  apply (erule corres_guard_imp)
-   apply auto
-  done
-
-wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' m f'" wpc_helper_corres_final
-wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' (m >>= f) f'" wpc_helper_corres_final
-wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' (m >>=E f) f'" wpc_helper_corres_final
-
 lemma condition_const: "condition (\<lambda>_. P) L R = (if P then L else R)"
   by (simp add: condition_def split: if_splits)