theory structures_proofs

lemma (in kernel_all_substitute) pde_pde_coarse_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_pde_C :== PROC pde_pde_coarse_new(\<acute>address, \<acute>P, \<acute>Domain)
       \<lbrace>pde_pde_coarse_lift \<acute>ret__struct_pde_C = \<lparr>
          pde_pde_coarse_CL.address_CL = (\<^bsup>s\<^esup>address___unsigned AND NOT (mask 10)),
          pde_pde_coarse_CL.P_CL = (\<^bsup>s\<^esup>P___unsigned AND mask 1),
          pde_pde_coarse_CL.Domain_CL = (\<^bsup>s\<^esup>Domain___unsigned AND mask 4) \<rparr> \<and>
        pde_get_tag \<acute>ret__struct_pde_C = scast pde_pde_coarse\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps o_def mask_def shift_over_ao_dists) apply (rule context_conjI[THEN iffD1[OF conj_commute]],
         fastforce simp: pde_get_tag_eq_x pde_pde_coarse_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: pde_pde_coarse_lift_def) apply (erule pde_lift_pde_coarse[THEN subst[OF sym]]; simp?) apply ((intro conjI sign_extend_eq)?;
         (simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
                    word_ao_dist word_bw_assocs word_and_max_simps pde_pde_coarse_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pde_pde_coarse_new_'proc \<lbrace>pde_pde_coarse_lift \<acute>ret__struct_pde_C = \<lparr>pde_pde_coarse_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 10, P_CL = \<^bsup>s\<^esup>P && mask 1, Domain_CL = \<^bsup>s\<^esup>Domain && mask 4\<rparr> \<and> pde_get_tag \<acute>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> 0 \<le>s 9 \<and> 9 <s 0x20 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> pde_pde_coarse_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address && 0xFFFFFC00 >> unat 0)) || (\<acute>P && 1 << unat 9)) || (\<acute>Domain && 0xF << unat 5)) || (SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3 << unat 0))) v) = \<lparr>pde_pde_coarse_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 10, P_CL = \<^bsup>s\<^esup>P && mask 1, Domain_CL = \<^bsup>s\<^esup>Domain && mask 4\<rparr> \<and> pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address && 0xFFFFFC00 >> unat 0)) || (\<acute>P && 1 << unat 9)) || (\<acute>Domain && 0xF << unat 5)) || (SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3 << unat 0))) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_pde_coarse_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3)) v) = \<lparr>pde_pde_coarse_CL.address_CL = address_' s && 0xFFFFFC00, P_CL = P_' s && 1, Domain_CL = Domain_' s && 0xF\<rparr> \<and> pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<Longrightarrow> pde_pde_coarse_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3)) v) = \<lparr>pde_pde_coarse_CL.address_CL = address_' s && 0xFFFFFC00, P_CL = P_' s && 1, Domain_CL = Domain_' s && 0xF\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<Longrightarrow> (case pde_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3)) v) of Some (Pde_pde_coarse rec) \<Rightarrow> rec) = \<lparr>pde_pde_coarse_CL.address_CL = address_' s && 0xFFFFFC00, P_CL = P_' s && 1, Domain_CL = Domain_' s && 0xF\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3) && ~~ mask 10 = address_' s && 0xFFFFFC00 \<and> (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3 >> 9) && 1 = P_' s && 1 \<and> (((address_' s && 0xFFFFFC00 || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || SCAST(32 signed \<rightarrow> 32) pde_pde_coarse && 3 >> 5) && mask 4 = Domain_' s && 0xF proof (prove)
goal:
No subgoals!