theory CSpace_C

lemma generic_frame_cap_get_capFIsDevice_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>
       \<acute>ret__unsigned_long :== PROC generic_frame_cap_get_capFIsDevice(\<acute>cap)
       \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFIsDevice_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: generic_frame_cap_get_capFIsDevice_CL_def) apply (intro conjI impI) apply (clarsimp simp: cap_lift_small_frame_cap cap_small_frame_cap_lift_def) apply (clarsimp simp: cap_lift_frame_cap cap_frame_cap_lift_def) apply (clarsimp simp: cap_lifts [THEN sym]) by (clarsimp simp: generic_frame_cap_get_capFIsDevice_CL_def
                        cap_lift_small_frame_cap cap_lift_frame_cap
                        cap_small_frame_cap_lift_def cap_frame_cap_lift_def)

(* 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_capFIsDevice_'proc \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFIsDevice_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<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> \<subseteq> \<lbrace>\<forall>v t. \<^bsup>t\<^esup>ret__unsigned = cap_get_tag \<acute>cap \<longrightarrow> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag \<acute>cap) = cap_small_frame_cap \<longrightarrow> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift \<acute>cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift \<acute>cap)) = generic_frame_cap_get_capFIsDevice_CL (cap_lift \<^bsup>s\<^esup>cap))) \<and> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag \<acute>cap) \<noteq> cap_small_frame_cap \<longrightarrow> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift \<acute>cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift \<acute>cap)) = generic_frame_cap_get_capFIsDevice_CL (cap_lift \<^bsup>s\<^esup>cap)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = cap_get_tag (cap_' x)\<rbrakk> \<Longrightarrow> (cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift (cap_' x))) \<longrightarrow> cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift (cap_' x)) = (case cap_lift (cap_' x) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFIsDevice_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFIsDevice_CL xa | Some _ \<Rightarrow> 0)) \<and> (cap_get_tag (cap_' x) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> ((\<exists>t. ret__unsigned_' t = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x))) \<longrightarrow> cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x)) = (case cap_lift (cap_' x) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFIsDevice_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFIsDevice_CL xa | Some _ \<Rightarrow> 0))) proof (prove)
goal (3 subgoals):
 1. \<And>x t. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = cap_get_tag (cap_' x); cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; \<exists>t. ret__unsigned_' t = cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift (cap_' x))\<rbrakk> \<Longrightarrow> cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift (cap_' x)) = (case cap_lift (cap_' x) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFIsDevice_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFIsDevice_CL xa | Some _ \<Rightarrow> 0)
 2. \<And>x t. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = cap_get_tag (cap_' x); cap_get_tag (cap_' x) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap
 3. \<And>x t. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = cap_get_tag (cap_' x); cap_get_tag (cap_' x) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; \<exists>t. ret__unsigned_' t = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x))\<rbrakk> \<Longrightarrow> cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x)) = (case cap_lift (cap_' x) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFIsDevice_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFIsDevice_CL xa | Some _ \<Rightarrow> 0) proof (prove)
goal (2 subgoals):
 1. \<And>x t. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = cap_get_tag (cap_' x); cap_get_tag (cap_' x) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap
 2. \<And>x t. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = cap_get_tag (cap_' x); cap_get_tag (cap_' x) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; \<exists>t. ret__unsigned_' t = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x))\<rbrakk> \<Longrightarrow> cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x)) = (case cap_lift (cap_' x) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFIsDevice_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFIsDevice_CL xa | Some _ \<Rightarrow> 0) proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = cap_get_tag (cap_' x); cap_get_tag (cap_' x) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; \<exists>t. ret__unsigned_' t = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x))\<rbrakk> \<Longrightarrow> cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x)) = (case cap_lift (cap_' x) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFIsDevice_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFIsDevice_CL xa | Some _ \<Rightarrow> 0) proof (prove)
goal (1 subgoal):
 1. \<And>x t ta. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_frame_cap \<noteq> cap_small_frame_cap; ret__unsigned_' ta = cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x))\<rbrakk> \<Longrightarrow> cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift (cap_' x)) = (case cap_lift (cap_' x) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFIsDevice_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFIsDevice_CL xa | Some _ \<Rightarrow> 0)