theory VSpace_C

lemma generic_frame_cap_get_capFMappedAddress_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or>
                cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace>
       Call generic_frame_cap_get_capFMappedAddress_'proc
       \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFMappedAddress_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply vcg apply (clarsimp simp: generic_frame_cap_get_capFMappedAddress_CL_def) apply (auto simp: cap_lift_small_frame_cap cap_small_frame_cap_lift_def
                    cap_lift_frame_cap cap_frame_cap_lift_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> Call generic_frame_cap_get_capFMappedAddress_'proc \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFMappedAddress_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) = cap_small_frame_cap \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<and> (\<forall>ret__unsigned. ret__unsigned = cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap)) = generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap))) \<and> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<noteq> cap_small_frame_cap \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>ret__unsigned. ret__unsigned = cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap)) = generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap))) proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFMappedAddress_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFMappedAddress_CL xa | Some _ \<Rightarrow> 0)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFMappedAddress_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFMappedAddress_CL xa | Some _ \<Rightarrow> 0)) proof (prove)
goal:
No subgoals!