theory Tcb_DR

lemma corres_mapM_x_rhs_induct:
  "\<lbrakk> corres_underlying sr nf nf' dc P P' g (return ());
     \<And>a. corres_underlying sr nf nf' dc P P' g (g' a);
     g = do g; g od;
     \<lbrace> P \<rbrace> g \<lbrace> \<lambda>_. P \<rbrace>;
     \<And>a. \<lbrace> P' \<rbrace> g' a \<lbrace> \<lambda>_. P'\<rbrace> \<rbrakk> \<Longrightarrow>
  corres_underlying sr nf nf' dc P P' g (mapM_x g' l)" apply (induct_tac l) apply (clarsimp simp: mapM_x_def sequence_x_def dc_def) apply (clarsimp simp: mapM_x_def sequence_x_def dc_def) apply (erule ssubst) apply (rule corres_guard_imp) apply (rule corres_split) apply assumption apply assumption apply assumption apply assumption apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' dc P P' g (return ()); \<And>a. corres_underlying sr nf nf' dc P P' g (g' a); g = do g;
g
od; \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' dc P P' g (mapM_x g' l) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>corres_underlying sr nf nf' dc P P' g (return ()); \<And>a. corres_underlying sr nf nf' dc P P' g (g' a); g = do g;
g
od; \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' dc P P' g (mapM_x g' [])
 2. \<And>a list. \<lbrakk>corres_underlying sr nf nf' dc P P' g (return ()); \<And>a. corres_underlying sr nf nf' dc P P' g (g' a); g = do g;
g
od; \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' dc P P' g (mapM_x g' list)\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' dc P P' g (mapM_x g' (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>corres_underlying sr nf nf' dc P P' g (return ()); \<And>a. corres_underlying sr nf nf' dc P P' g (g' a); g = do g;
g
od; \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' dc P P' g (mapM_x g' list)\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' dc P P' g (mapM_x g' (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); g = do y <- g;
g
od; \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (do _ <- g' a;
foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())
od) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>a b. True) P P' (do y <- g;
g
od) (do _ <- g' a;
foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())
od) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>a b. True) (?Q6 a list) (?Q'6 a list) (do y <- g;
g
od) (do _ <- g' a;
foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())
od)
 2. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P s\<rbrakk> \<Longrightarrow> ?Q6 a list s
 3. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P' s\<rbrakk> \<Longrightarrow> ?Q'6 a list s proof (prove)
goal (6 subgoals):
 1. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (?r'10 a list) (?P10 a list) (?P'10 a list) g (g' a)
 2. \<And>a list rv rv'. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); ?r'10 a list rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>a b. True) (?R10 a list rv) (?R'10 a list rv') g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))
 3. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list\<rbrace> g \<lbrace>?R10 a list\<rbrace>
 4. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list\<rbrace> g' a \<lbrace>?R'10 a list\<rbrace>
 5. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P s\<rbrakk> \<Longrightarrow> (?P10 a list and ?Q10 a list) s
 6. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P' s\<rbrakk> \<Longrightarrow> (?P'10 a list and ?Q'10 a list) s proof (prove)
goal (5 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); True\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>a b. True) (?R10 a list rv) (?R'10 a list rv') g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))
 2. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list\<rbrace> g \<lbrace>?R10 a list\<rbrace>
 3. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list\<rbrace> g' a \<lbrace>?R'10 a list\<rbrace>
 4. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P s\<rbrakk> \<Longrightarrow> (P and ?Q10 a list) s
 5. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'10 a list) s proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 a list\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list\<rbrace> g' a \<lbrace>\<lambda>rv'. P'\<rbrace>
 3. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P s\<rbrakk> \<Longrightarrow> (P and ?Q10 a list) s
 4. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'10 a list) s proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ()))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 a list\<rbrace> g' a \<lbrace>\<lambda>rv'. P'\<rbrace>
 2. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P s\<rbrakk> \<Longrightarrow> (P and P) s
 3. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'10 a list) s proof (prove)
goal (2 subgoals):
 1. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P s\<rbrakk> \<Longrightarrow> (P and P) s
 2. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P' s\<rbrakk> \<Longrightarrow> (P' and P') s proof (prove)
goal (1 subgoal):
 1. \<And>a list s. \<lbrakk>corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (return ()); \<And>a. corres_underlying sr nf nf' (\<lambda>rv rv'. True) P P' g (g' a); \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; \<And>a. \<lbrace>P'\<rbrace> g' a \<lbrace>\<lambda>_. P'\<rbrace>; corres_underlying sr nf nf' (\<lambda>a b. True) P P' g (foldr (\<lambda>x y. do _ <- x;
y
od) (map g' list) (return ())); P' s\<rbrakk> \<Longrightarrow> (P' and P') s proof (prove)
goal:
No subgoals!