theory Untyped_AI

lemma mapME_validE_nth_induct:
  "\<lbrakk> \<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>;
        \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i \<rbrakk>
    \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>" proof (induct xs rule: rev_induct) case Nil show ?case by (wp | simp add: mapME_Nil)+ next case (snoc x xs) from snoc.prems have x: "x = zs ! length xs" by simp from snoc.prems have zs: "\<And>i. i < length xs \<Longrightarrow> xs ! i = zs ! i" by (metis length_append_singleton less_SucI nth_append) show ?case apply (simp add: mapME_append mapME_Cons mapME_Nil bindE_assoc x) apply (wp snoc.hyps snoc.prems | simp add: zs)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>i ys. i < length [] \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length [] \<Longrightarrow> zs ! i = [] ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f [] \<lbrace>\<lambda>ys. P (length []) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i ys. i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length (xs @ [x]) \<Longrightarrow> zs ! i = (xs @ [x]) ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
?i < length [] \<Longrightarrow> \<lbrace>P ?i ?ys\<rbrace> f (zs ! ?i) \<lbrace>\<lambda>y. P (Suc ?i) (y # ?ys)\<rbrace>, \<lbrace>E\<rbrace>
?i < length [] \<Longrightarrow> zs ! ?i = [] ! ?i

goal (2 subgoals):
 1. \<lbrakk>\<And>i ys. i < length [] \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length [] \<Longrightarrow> zs ! i = [] ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f [] \<lbrace>\<lambda>ys. P (length []) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i ys. i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length (xs @ [x]) \<Longrightarrow> zs ! i = (xs @ [x]) ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P 0 []\<rbrace> mapME f [] \<lbrace>\<lambda>ys. P (length []) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
\<lbrace>P 0 []\<rbrace> mapME f [] \<lbrace>\<lambda>ys. P (length []) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i ys. i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length (xs @ [x]) \<Longrightarrow> zs ! i = (xs @ [x]) ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i ys. i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length (xs @ [x]) \<Longrightarrow> zs ! i = (xs @ [x]) ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>
?i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P ?i ?ys\<rbrace> f (zs ! ?i) \<lbrace>\<lambda>y. P (Suc ?i) (y # ?ys)\<rbrace>, \<lbrace>E\<rbrace>
?i < length (xs @ [x]) \<Longrightarrow> zs ! ?i = (xs @ [x]) ! ?i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i ys. i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length (xs @ [x]) \<Longrightarrow> zs ! i = (xs @ [x]) ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (chain)
picking this:
?i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P ?i ?ys\<rbrace> f (zs ! ?i) \<lbrace>\<lambda>y. P (Suc ?i) (y # ?ys)\<rbrace>, \<lbrace>E\<rbrace>
?i < length (xs @ [x]) \<Longrightarrow> zs ! ?i = (xs @ [x]) ! ?i proof (prove)
using this:
?i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P ?i ?ys\<rbrace> f (zs ! ?i) \<lbrace>\<lambda>y. P (Suc ?i) (y # ?ys)\<rbrace>, \<lbrace>E\<rbrace>
?i < length (xs @ [x]) \<Longrightarrow> zs ! ?i = (xs @ [x]) ! ?i

goal (1 subgoal):
 1. x = zs ! length xs proof (state)
this:
x = zs ! length xs

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i ys. i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length (xs @ [x]) \<Longrightarrow> zs ! i = (xs @ [x]) ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (chain)
picking this:
?i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P ?i ?ys\<rbrace> f (zs ! ?i) \<lbrace>\<lambda>y. P (Suc ?i) (y # ?ys)\<rbrace>, \<lbrace>E\<rbrace>
?i < length (xs @ [x]) \<Longrightarrow> zs ! ?i = (xs @ [x]) ! ?i proof (prove)
using this:
?i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P ?i ?ys\<rbrace> f (zs ! ?i) \<lbrace>\<lambda>y. P (Suc ?i) (y # ?ys)\<rbrace>, \<lbrace>E\<rbrace>
?i < length (xs @ [x]) \<Longrightarrow> zs ! ?i = (xs @ [x]) ! ?i

goal (1 subgoal):
 1. \<And>i. i < length xs \<Longrightarrow> xs ! i = zs ! i proof (state)
this:
?i < length xs \<Longrightarrow> xs ! ?i = zs ! ?i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>\<And>i ys. i < length xs \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length xs \<Longrightarrow> zs ! i = xs ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f xs \<lbrace>\<lambda>ys. P (length xs) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i ys. i < length (xs @ [x]) \<Longrightarrow> \<lbrace>P i ys\<rbrace> f (zs ! i) \<lbrace>\<lambda>y. P (Suc i) (y # ys)\<rbrace>, \<lbrace>E\<rbrace>; \<And>i. i < length (xs @ [x]) \<Longrightarrow> zs ! i = (xs @ [x]) ! i\<rbrakk> \<Longrightarrow> \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P 0 []\<rbrace> doE xs_r <- mapME f xs;
x <- f (zs ! length xs);
returnOk (xs_r @ [x])
odE \<lbrace>\<lambda>ys. P (Suc (length xs)) (rev ys)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P 0 []\<rbrace> mapME f (xs @ [x]) \<lbrace>\<lambda>ys. P (length (xs @ [x])) (rev ys)\<rbrace>, \<lbrace>E\<rbrace>

goal:
No subgoals!