theory Invoke_C

lemma APIType_capBits_low:
  "\<lbrakk> newType = APIObjectType apiobject_type.CapTableObject \<longrightarrow> 0 < us;
     newType = APIObjectType apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits\<rbrakk>
           \<Longrightarrow> 4 \<le> APIType_capBits newType us" apply (case_tac newType) apply (clarsimp simp: invokeUntyped_proofs_def APIType_capBits_def objBits_simps' untypedBits_defs
                 split: apiobject_type.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; newType = APIObjectType x1\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us
 2. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; newType = object_type.SmallPageObject\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us
 3. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; newType = object_type.LargePageObject\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us
 4. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; newType = object_type.SectionObject\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us
 5. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; newType = object_type.SuperSectionObject\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us
 6. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; newType = object_type.PageTableObject\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us
 7. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; newType = object_type.PageDirectoryObject\<rbrakk> \<Longrightarrow> 4 \<le> APIType_capBits newType us proof (prove)
goal:
No subgoals!