theory Invoke_C

lemma toEnum_object_type_to_H:
  "unat v \<le> (fromEnum::object_type \<Rightarrow> nat) maxBound
  \<Longrightarrow> toEnum (unat v) = (object_type_to_H (v::word32))" apply (simp add:enum_object_type enum_apiobject_type object_type_to_H_def toEnum_def
                  maxBound_less_length) apply (clarsimp simp: Kernel_C_defs split:if_splits) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat v \<le> fromEnum maxBound \<Longrightarrow> toEnum (unat v) = object_type_to_H v proof (prove)
goal (1 subgoal):
 1. unat v < Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<Longrightarrow> [APIObjectType ArchTypes_H.apiobject_type.Untyped, APIObjectType ArchTypes_H.apiobject_type.TCBObject, APIObjectType ArchTypes_H.apiobject_type.EndpointObject, APIObjectType ArchTypes_H.apiobject_type.NotificationObject, APIObjectType ArchTypes_H.apiobject_type.CapTableObject, object_type.PageDirectoryObject, object_type.SmallPageObject, object_type.LargePageObject, object_type.SectionObject, object_type.SuperSectionObject, object_type.PageTableObject] ! unat v = (if v = SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject then APIObjectType ArchTypes_H.apiobject_type.Untyped else if v = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject then APIObjectType ArchTypes_H.apiobject_type.TCBObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject then APIObjectType ArchTypes_H.apiobject_type.EndpointObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject then APIObjectType ArchTypes_H.apiobject_type.NotificationObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject then APIObjectType ArchTypes_H.apiobject_type.CapTableObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject then object_type.SmallPageObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject then object_type.LargePageObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject then object_type.SectionObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject then object_type.SuperSectionObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject then object_type.PageTableObject else if v = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject then object_type.PageDirectoryObject else undefined) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat v < Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))); v \<noteq> 5; v \<noteq> 0xA; v \<noteq> 9; v \<noteq> 8; v \<noteq> 7; v \<noteq> 6; v \<noteq> 4; v \<noteq> 3; v \<noteq> 2; v \<noteq> 1; v \<noteq> 0\<rbrakk> \<Longrightarrow> [APIObjectType ArchTypes_H.apiobject_type.Untyped, APIObjectType ArchTypes_H.apiobject_type.TCBObject, APIObjectType ArchTypes_H.apiobject_type.EndpointObject, APIObjectType ArchTypes_H.apiobject_type.NotificationObject, APIObjectType ArchTypes_H.apiobject_type.CapTableObject, object_type.PageDirectoryObject, object_type.SmallPageObject, object_type.LargePageObject, object_type.SectionObject, object_type.SuperSectionObject, object_type.PageTableObject] ! unat v = undefined proof (prove)
goal:
No subgoals!