theory Tcb_C

lemma mapM_upd_inv:
  assumes f: "\<And>x rv. (rv,s) \<in> fst (f x s) \<Longrightarrow> x \<in> set xs \<Longrightarrow> (rv, g s) \<in> fst (f x (g s))"
  assumes inv: "\<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>"
  shows "(rv,s) \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s))" using f inv proof (induct xs arbitrary: rv s) case Nil thus ?case by (simp add: mapM_Nil return_def) next case (Cons z zs) from Cons.prems show ?case apply (clarsimp simp: mapM_Cons in_monad) apply (frule use_valid, assumption, rule refl) apply clarsimp apply (drule Cons.prems, simp) apply (rule exI, erule conjI) apply (drule Cons.hyps) apply simp apply assumption apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s) \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s)) proof (prove)
using this:
\<lbrakk>(?rv1, s) \<in> fst (f ?x1 s); ?x1 \<in> set xs\<rbrakk> \<Longrightarrow> (?rv1, g s) \<in> fst (f ?x1 (g s))
\<lbrace>(=) s\<rbrace> f ?x1 \<lbrace>\<lambda>_. (=) s\<rbrace>

goal (1 subgoal):
 1. (rv, s) \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s)) proof (state)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>(rv, s) \<in> fst (mapM f [] s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set []\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f [] (g s))
 2. \<And>x1 xs rv s. \<lbrakk>\<And>rv s. \<lbrakk>(rv, s) \<in> fst (mapM f xs s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s)); (rv, s) \<in> fst (mapM f (x1 # xs) s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set (x1 # xs)\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f (x1 # xs) (g s)) proof (state)
this:
(rv, s) \<in> fst (mapM f [] s)
\<lbrakk>(?rv1, s) \<in> fst (f ?x1 s); ?x1 \<in> set []\<rbrakk> \<Longrightarrow> (?rv1, g s) \<in> fst (f ?x1 (g s))
\<lbrace>(=) s\<rbrace> f ?x1 \<lbrace>\<lambda>_. (=) s\<rbrace>

goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>(rv, s) \<in> fst (mapM f [] s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set []\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f [] (g s))
 2. \<And>x1 xs rv s. \<lbrakk>\<And>rv s. \<lbrakk>(rv, s) \<in> fst (mapM f xs s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s)); (rv, s) \<in> fst (mapM f (x1 # xs) s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set (x1 # xs)\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f (x1 # xs) (g s)) proof (prove)
using this:
(rv, s) \<in> fst (mapM f [] s)
\<lbrakk>(?rv1, s) \<in> fst (f ?x1 s); ?x1 \<in> set []\<rbrakk> \<Longrightarrow> (?rv1, g s) \<in> fst (f ?x1 (g s))
\<lbrace>(=) s\<rbrace> f ?x1 \<lbrace>\<lambda>_. (=) s\<rbrace>

goal (1 subgoal):
 1. (rv, g s) \<in> fst (mapM f [] (g s)) proof (state)
this:
(rv, g s) \<in> fst (mapM f [] (g s))

goal (1 subgoal):
 1. \<And>x1 xs rv s. \<lbrakk>\<And>rv s. \<lbrakk>(rv, s) \<in> fst (mapM f xs s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s)); (rv, s) \<in> fst (mapM f (x1 # xs) s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set (x1 # xs)\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f (x1 # xs) (g s)) proof (state)
goal (1 subgoal):
 1. \<And>x1 xs rv s. \<lbrakk>\<And>rv s. \<lbrakk>(rv, s) \<in> fst (mapM f xs s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s)); (rv, s) \<in> fst (mapM f (x1 # xs) s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set (x1 # xs)\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f (x1 # xs) (g s)) proof (state)
this:
\<lbrakk>(?rv1, ?s1) \<in> fst (mapM f zs ?s1); \<And>rv x. \<lbrakk>(rv, ?s1) \<in> fst (f x ?s1); x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g ?s1) \<in> fst (f x (g ?s1)); \<And>x. \<lbrace>(=) ?s1\<rbrace> f x \<lbrace>\<lambda>_. (=) ?s1\<rbrace>\<rbrakk> \<Longrightarrow> (?rv1, g ?s1) \<in> fst (mapM f zs (g ?s1))
(rv, s) \<in> fst (mapM f (z # zs) s)
\<lbrakk>(?rv1, s) \<in> fst (f ?x1 s); ?x1 \<in> set (z # zs)\<rbrakk> \<Longrightarrow> (?rv1, g s) \<in> fst (f ?x1 (g s))
\<lbrace>(=) s\<rbrace> f ?x1 \<lbrace>\<lambda>_. (=) s\<rbrace>

goal (1 subgoal):
 1. \<And>x1 xs rv s. \<lbrakk>\<And>rv s. \<lbrakk>(rv, s) \<in> fst (mapM f xs s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set xs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s)); (rv, s) \<in> fst (mapM f (x1 # xs) s); \<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x \<in> set (x1 # xs)\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (mapM f (x1 # xs) (g s)) proof (chain)
picking this:
(rv, s) \<in> fst (mapM f (z # zs) s)
\<lbrakk>(?rv1, s) \<in> fst (f ?x1 s); ?x1 \<in> set (z # zs)\<rbrakk> \<Longrightarrow> (?rv1, g s) \<in> fst (f ?x1 (g s))
\<lbrace>(=) s\<rbrace> f ?x1 \<lbrace>\<lambda>_. (=) s\<rbrace> proof (prove)
using this:
(rv, s) \<in> fst (mapM f (z # zs) s)
\<lbrakk>(?rv1, s) \<in> fst (f ?x1 s); ?x1 \<in> set (z # zs)\<rbrakk> \<Longrightarrow> (?rv1, g s) \<in> fst (f ?x1 (g s))
\<lbrace>(=) s\<rbrace> f ?x1 \<lbrace>\<lambda>_. (=) s\<rbrace>

goal (1 subgoal):
 1. (rv, g s) \<in> fst (mapM f (z # zs) (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s'' y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; (y, s'') \<in> fst (f z s); (ys, s) \<in> fst (mapM f zs s''); rv = y # ys\<rbrakk> \<Longrightarrow> \<exists>s''. (y, s'') \<in> fst (f z (g s)) \<and> (ys, g s) \<in> fst (mapM f zs s'') proof (prove)
goal (1 subgoal):
 1. \<And>s'' y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; (y, s'') \<in> fst (f z s); (ys, s) \<in> fst (mapM f zs s''); rv = y # ys; s = s''\<rbrakk> \<Longrightarrow> \<exists>s''. (y, s'') \<in> fst (f z (g s)) \<and> (ys, g s) \<in> fst (mapM f zs s'') proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; (y, s) \<in> fst (f z s); (ys, s) \<in> fst (mapM f zs s); rv = y # ys\<rbrakk> \<Longrightarrow> \<exists>s''. (y, s'') \<in> fst (f z (g s)) \<and> (ys, g s) \<in> fst (mapM f zs s'') proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; (ys, s) \<in> fst (mapM f zs s); rv = y # ys; (y, g s) \<in> fst (f z (g s))\<rbrakk> \<Longrightarrow> \<exists>s''. (y, s'') \<in> fst (f z (g s)) \<and> (ys, g s) \<in> fst (mapM f zs s'') proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; (ys, s) \<in> fst (mapM f zs s); rv = y # ys\<rbrakk> \<Longrightarrow> (ys, g s) \<in> fst (mapM f zs (g s)) proof (prove)
goal (3 subgoals):
 1. \<And>y ys rv x. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; rv = y # ys; (rv, s) \<in> fst (f x s); x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s))
 2. \<And>y ys x. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; rv = y # ys\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. \<And>y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; rv = y # ys; (ys, g s) \<in> fst (mapM f zs (g s))\<rbrakk> \<Longrightarrow> (ys, g s) \<in> fst (mapM f zs (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>y ys x. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; rv = y # ys\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. \<And>y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; rv = y # ys; (ys, g s) \<in> fst (mapM f zs (g s))\<rbrakk> \<Longrightarrow> (ys, g s) \<in> fst (mapM f zs (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>\<And>rv x. \<lbrakk>(rv, s) \<in> fst (f x s); x = z \<or> x \<in> set zs\<rbrakk> \<Longrightarrow> (rv, g s) \<in> fst (f x (g s)); \<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>; rv = y # ys; (ys, g s) \<in> fst (mapM f zs (g s))\<rbrakk> \<Longrightarrow> (ys, g s) \<in> fst (mapM f zs (g s)) proof (prove)
goal:
No subgoals! proof (state)
this:
(rv, g s) \<in> fst (mapM f (z # zs) (g s))

goal:
No subgoals!