theory SyscallArgs_C

lemma ccorres_pre_loadWordUser:
  "(\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow>
   ccorres r xf (valid_pspace' and K (is_aligned ptr 2) and
                 (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s))
     {s. \<forall>v. cslift s (Ptr ptr :: word32 ptr) = Some v \<longrightarrow>
               s \<in> Q v} hs
     (loadWordUser ptr >>= a) c" apply (rule ccorres_guard_imp) apply (rule_tac Q="\<lambda>rv. P rv and user_word_at rv ptr" and Q'=Q in
          ccorres_symb_exec_l [OF _ loadWordUser_inv loadWordUser_wp]) apply (fastforce intro: ccorres_guard_imp) apply simp apply simp apply clarsimp apply (drule(1) user_word_at_cross_over, simp) apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow> ccorres r xf (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s)) {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v} hs (loadWordUser ptr >>= a) c proof (prove)
goal (3 subgoals):
 1. (\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow> ccorres r xf ?Q ?Q' hs (loadWordUser ptr >>= a) c
 2. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s)) s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; s \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v}\<rbrakk> \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. \<And>rv. (\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow> ccorres r xf (P rv and user_word_at rv ptr) (Q rv) hs (a rv) c
 2. (\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow> empty_fail (loadWordUser ptr)
 3. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s)) s\<rbrakk> \<Longrightarrow> is_aligned ptr 2 \<and> (\<forall>v. user_word_at v ptr s \<longrightarrow> (P v and user_word_at v ptr) s)
 4. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; s \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v}\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (P rv and user_word_at rv ptr) s \<longrightarrow> s' \<in> Q rv} proof (prove)
goal (3 subgoals):
 1. (\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow> empty_fail (loadWordUser ptr)
 2. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s)) s\<rbrakk> \<Longrightarrow> is_aligned ptr 2 \<and> (\<forall>v. user_word_at v ptr s \<longrightarrow> (P v and user_word_at v ptr) s)
 3. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; s \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v}\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (P rv and user_word_at rv ptr) s \<longrightarrow> s' \<in> Q rv} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; (valid_pspace' and K (is_aligned ptr 2) and (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s)) s\<rbrakk> \<Longrightarrow> is_aligned ptr 2 \<and> (\<forall>v. user_word_at v ptr s \<longrightarrow> (P v and user_word_at v ptr) s)
 2. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; s \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v}\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (P rv and user_word_at rv ptr) s \<longrightarrow> s' \<in> Q rv} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; s \<in> {s. \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v}\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (P rv and user_word_at rv ptr) s \<longrightarrow> s' \<in> Q rv} proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v; (sa, s) \<in> rf_sr; P rv sa; user_word_at rv ptr sa\<rbrakk> \<Longrightarrow> s \<in> Q rv proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c; \<forall>v. cslift s (PTR(32 word) ptr) = Some v \<longrightarrow> s \<in> Q v; (sa, s) \<in> rf_sr; P rv sa; c_guard (PTR(32 word) ptr) \<and> s \<Turnstile>\<^sub>c PTR(32 word) ptr \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word) ptr) = rv\<rbrakk> \<Longrightarrow> s \<in> Q rv proof (prove)
goal:
No subgoals!