theory Monad_Lists

lemma mapM_x_inv_wp3:
  fixes m :: "'b \<Rightarrow> ('a, unit) nondet_monad"
  assumes hr: "\<And>a as bs. xs = as @ [a] @ bs \<Longrightarrow>
     \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>"
  shows   "\<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>" using hr proof (induct xs rule: rev_induct) case Nil thus ?case by (simp add: mapM_x_Nil) next case (snoc x xs) show ?case apply (simp add: mapM_append_single) apply (wp snoc.prems) apply simp apply (rule snoc.hyps [OF snoc.prems]) apply simp apply assumption done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace> proof (prove)
using this:
xs = ?as @ [?a] @ ?bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V ?as s\<rbrace> m ?a \<lbrace>\<lambda>r s. I s \<and> V (?as @ [?a]) s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace> proof (state)
goal (2 subgoals):
 1. (\<And>as a bs. [] = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m [] \<lbrace>\<lambda>rv s. I s \<and> V [] s\<rbrace>
 2. \<And>x xs. \<lbrakk>(\<And>as a bs. xs = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>; \<And>as a bs. xs @ [x] = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m (xs @ [x]) \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace> proof (state)
this:
[] = ?as @ [?a] @ ?bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V ?as s\<rbrace> m ?a \<lbrace>\<lambda>r s. I s \<and> V (?as @ [?a]) s\<rbrace>

goal (2 subgoals):
 1. (\<And>as a bs. [] = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m [] \<lbrace>\<lambda>rv s. I s \<and> V [] s\<rbrace>
 2. \<And>x xs. \<lbrakk>(\<And>as a bs. xs = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>; \<And>as a bs. xs @ [x] = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m (xs @ [x]) \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace> proof (prove)
using this:
[] = ?as @ [?a] @ ?bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V ?as s\<rbrace> m ?a \<lbrace>\<lambda>r s. I s \<and> V (?as @ [?a]) s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m [] \<lbrace>\<lambda>rv s. I s \<and> V [] s\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m [] \<lbrace>\<lambda>rv s. I s \<and> V [] s\<rbrace>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>(\<And>as a bs. xs = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>; \<And>as a bs. xs @ [x] = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m (xs @ [x]) \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>(\<And>as a bs. xs = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>; \<And>as a bs. xs @ [x] = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m (xs @ [x]) \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace> proof (state)
this:
(\<And>as a bs. xs = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>
xs @ [x] = ?as @ [?a] @ ?bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V ?as s\<rbrace> m ?a \<lbrace>\<lambda>r s. I s \<and> V (?as @ [?a]) s\<rbrace>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>(\<And>as a bs. xs = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>; \<And>as a bs. xs @ [x] = as @ [a] @ bs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m (xs @ [x]) \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m (xs @ [x]) \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> do _ <- mapM_x m xs;
m x
od \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa. xs @ [x] = xs @ [x] @ ?bs2 xa
 2. \<lbrace>?Q\<rbrace> mapM_x m xs \<lbrace>\<lambda>x s. I s \<and> V xs s\<rbrace>
 3. \<And>s. I s \<and> V [] s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> mapM_x m xs \<lbrace>\<lambda>x s. I s \<and> V xs s\<rbrace>
 2. \<And>s. I s \<and> V [] s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>as a bs. xs = as @ [a] @ bs \<Longrightarrow> xs @ [x] = as @ [a] @ ?bs4 as a bs
 2. \<And>s. I s \<and> V [] s \<Longrightarrow> I s \<and> V [] s proof (prove)
goal (1 subgoal):
 1. \<And>s. I s \<and> V [] s \<Longrightarrow> I s \<and> V [] s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m (xs @ [x]) \<lbrace>\<lambda>rv s. I s \<and> V (xs @ [x]) s\<rbrace>

goal:
No subgoals!