theory CSpace_C

lemma generic_frame_cap_size[simp]:
  "cap_get_tag cap = scast cap_frame_cap \<or> cap_get_tag cap = scast cap_small_frame_cap
  \<Longrightarrow> generic_frame_cap_get_capFSize_CL (cap_lift cap) && mask 2 =
     generic_frame_cap_get_capFSize_CL (cap_lift cap)" apply (simp add: generic_frame_cap_get_capFSize_CL_def) apply (erule disjE) subgoal by (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs) by (simp add: cap_lift_def cap_tag_defs mask_def Kernel_C.ARMSmallPage_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> generic_frame_cap_get_capFSize_CL (cap_lift cap) && mask 2 = generic_frame_cap_get_capFSize_CL (cap_lift cap) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) && mask 2 = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) proof (prove)
goal (2 subgoals):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) && mask 2 = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0)
 2. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) && mask 2 = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) && mask 2 = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0) && mask 2 = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap c) \<Rightarrow> capFSize_CL c | Some _ \<Rightarrow> 0)