arm-hyp crefine: proof update for object_type enum reorder

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4 · Aug 11, 2023 · e2955fc · e2955fc
1 parent 8ba1b46
commit e2955fc
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy
@@ -2785,6 +2785,9 @@ lemma hoarep_Cond_UNIV:
   apply simp
   done
 
+(* always unfold StrictC'_mode_object_defs together with api_object_defs *)
+lemmas api_object_defs = api_object_defs StrictC'_mode_object_defs
+
 lemma object_type_from_H_toAPIType_simps:
   "(object_type_from_H tp = scast seL4_UntypedObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.Untyped)"
   "(object_type_from_H tp = scast seL4_TCBObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.TCBObject)"