theory SyscallArgs_C

lemma mapM_loadWordUser_user_words_at:
  "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s)
              \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace>
    mapM loadWordUser xs \<lbrace>Q\<rbrace>" apply (induct xs arbitrary: Q) apply (simp add: mapM_def sequence_def) apply wp apply (simp add: mapM_Cons) apply wp apply assumption apply (wp loadWordUser_user_word_at) apply clarsimp apply (drule spec, erule mp) apply clarsimp apply (case_tac x) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length []. user_word_at (rv ! x) ([] ! x) s) \<and> length rv = length [] \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser [] \<lbrace>Q\<rbrace>
 2. \<And>x1 xs Q. (\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length (x1 # xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = length (x1 # xs) \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser (x1 # xs) \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q. \<lbrace>Q []\<rbrace> return [] \<lbrace>Q\<rbrace>
 2. \<And>x1 xs Q. (\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length (x1 # xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = length (x1 # xs) \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser (x1 # xs) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs Q. (\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length (x1 # xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = length (x1 # xs) \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser (x1 # xs) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs Q. (\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<Suc (length xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = Suc (length xs) \<longrightarrow> Q rv s\<rbrace> do y <- loadWordUser x1;
ys <- mapM loadWordUser xs;
return (y # ys)
od \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1 xs Q y. (\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>?B13 x1 xs Q y\<rbrace> mapM loadWordUser xs \<lbrace>\<lambda>ys. Q (y # ys)\<rbrace>
 2. \<And>x1 xs Q. (\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>?Q12 x1 xs Q\<rbrace> loadWordUser x1 \<lbrace>?B13 x1 xs Q\<rbrace>
 3. \<And>x1 xs Q s. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; \<forall>rv. (\<forall>x<Suc (length xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = Suc (length xs) \<longrightarrow> Q rv s\<rbrakk> \<Longrightarrow> ?Q12 x1 xs Q s proof (prove)
goal (2 subgoals):
 1. \<And>x1 xs Q. (\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>?Q12 x1 xs Q\<rbrace> loadWordUser x1 \<lbrace>\<lambda>y s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q (y # rv) s\<rbrace>
 2. \<And>x1 xs Q s. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; \<forall>rv. (\<forall>x<Suc (length xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = Suc (length xs) \<longrightarrow> Q rv s\<rbrakk> \<Longrightarrow> ?Q12 x1 xs Q s proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs Q s. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; \<forall>rv. (\<forall>x<Suc (length xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = Suc (length xs) \<longrightarrow> Q rv s\<rbrakk> \<Longrightarrow> \<forall>rv. user_word_at rv x1 s \<longrightarrow> (\<forall>rva. (\<forall>x<length xs. user_word_at (rva ! x) (xs ! x) s) \<and> length rva = length xs \<longrightarrow> Q (rv # rva) s) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs Q s rv rva. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; \<forall>rv. (\<forall>x<Suc (length xs). user_word_at (rv ! x) ((x1 # xs) ! x) s) \<and> length rv = Suc (length xs) \<longrightarrow> Q rv s; user_word_at rv x1 s; \<forall>x<length xs. user_word_at (rva ! x) (xs ! x) s; length rva = length xs\<rbrakk> \<Longrightarrow> Q (rv # rva) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs Q s rv rva. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; user_word_at rv x1 s; \<forall>x<length xs. user_word_at (rva ! x) (xs ! x) s; length rva = length xs\<rbrakk> \<Longrightarrow> (\<forall>x<Suc (length xs). user_word_at ((rv # rva) ! x) ((x1 # xs) ! x) s) \<and> length (rv # rva) = Suc (length xs) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs s rv rva x. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; user_word_at rv x1 s; \<forall>x<length xs. user_word_at (rva ! x) (xs ! x) s; length rva = length xs; x < Suc (length xs)\<rbrakk> \<Longrightarrow> user_word_at ((rv # rva) ! x) ((x1 # xs) ! x) s proof (prove)
goal (2 subgoals):
 1. \<And>x1 xs s rv rva x. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; user_word_at rv x1 s; \<forall>x<length xs. user_word_at (rva ! x) (xs ! x) s; length rva = length xs; x < Suc (length xs); x = 0\<rbrakk> \<Longrightarrow> user_word_at ((rv # rva) ! x) ((x1 # xs) ! x) s
 2. \<And>x1 xs s rv rva x nat. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; user_word_at rv x1 s; \<forall>x<length xs. user_word_at (rva ! x) (xs ! x) s; length rva = length xs; x < Suc (length xs); x = Suc nat\<rbrakk> \<Longrightarrow> user_word_at ((rv # rva) ! x) ((x1 # xs) ! x) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs s rv rva x nat. \<lbrakk>\<And>Q. \<lbrace>\<lambda>s. \<forall>rv. (\<forall>x<length xs. user_word_at (rv ! x) (xs ! x) s) \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> mapM loadWordUser xs \<lbrace>Q\<rbrace>; user_word_at rv x1 s; \<forall>x<length xs. user_word_at (rva ! x) (xs ! x) s; length rva = length xs; x < Suc (length xs); x = Suc nat\<rbrakk> \<Longrightarrow> user_word_at ((rv # rva) ! x) ((x1 # xs) ! x) s proof (prove)
goal:
No subgoals!