theory Retype_R

lemma curDomain_mapM_x_futz:
  "curDomain >>= (\<lambda>cdom. mapM_x (threadSet (F cdom)) addrs)
 = mapM_x (\<lambda>addr. curDomain >>= (\<lambda>cdom. threadSet (F cdom) addr)) addrs" proof(induct addrs) case Nil thus ?case by (simp add: curDomain_def mapM_x_def sequence_x_def bind_def gets_def get_def return_def) next case (Cons addr addrs) have H: "\<And>G. do cdom \<leftarrow> curDomain;
                   _ \<leftarrow> threadSet (F cdom) addr;
                   G cdom
                od
              = do cdom \<leftarrow> curDomain;
                   threadSet (F cdom) addr;
                   cdom \<leftarrow> curDomain;
                   G cdom
                od" by (simp add: bind_assoc curDomain_def threadSet_def setObject_tcb_gets_ksCurDomain
                  getObject_tcb_gets double_gets_drop_regets) from Cons.hyps show ?case apply (simp add: mapM_x_def sequence_x_def) apply (simp add: bind_assoc foldr_map o_def) apply (subst H) apply (simp add: mapM_x_def sequence_x_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs proof (state)
goal (2 subgoals):
 1. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) []
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) []
 2. \<And>a addrs. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs \<Longrightarrow> do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (a # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (a # addrs) proof (state)
this:


goal (2 subgoals):
 1. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) []
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) []
 2. \<And>a addrs. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs \<Longrightarrow> do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (a # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (a # addrs) proof (prove)
goal (1 subgoal):
 1. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) []
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) [] proof (state)
this:
do cdom <- curDomain;
mapM_x (threadSet (F cdom)) []
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) []

goal (1 subgoal):
 1. \<And>a addrs. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs \<Longrightarrow> do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (a # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (a # addrs) proof (state)
goal (1 subgoal):
 1. \<And>a addrs. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs \<Longrightarrow> do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (a # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (a # addrs) proof (state)
this:
do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs

goal (1 subgoal):
 1. \<And>a addrs. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs \<Longrightarrow> do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (a # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (a # addrs) proof (prove)
goal (1 subgoal):
 1. \<And>G. do cdom <- curDomain;
_ <- threadSet (F cdom) addr;
G cdom
od = do cdom <- curDomain;
threadSet (F cdom) addr;
curDomain >>= G
od proof (state)
this:
do cdom <- curDomain;
_ <- threadSet (F cdom) addr;
?G cdom
od = do cdom <- curDomain;
threadSet (F cdom) addr;
curDomain >>= ?G
od

goal (1 subgoal):
 1. \<And>a addrs. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs \<Longrightarrow> do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (a # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (a # addrs) proof (chain)
picking this:
do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs proof (prove)
using this:
do cdom <- curDomain;
mapM_x (threadSet (F cdom)) addrs
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs

goal (1 subgoal):
 1. do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (addr # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (addr # addrs) proof (prove)
goal (1 subgoal):
 1. do cdom <- curDomain;
foldr (\<lambda>x y. do _ <- x;
y
od) (map (threadSet (F cdom)) addrs) (return ())
od = foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs) (return ()) \<Longrightarrow> do cdom <- curDomain;
_ <- threadSet (F cdom) addr;
foldr (\<lambda>x y. do _ <- x;
y
od) (map (threadSet (F cdom)) addrs) (return ())
od = do _ <- do cdom <- curDomain;
threadSet (F cdom) addr
od;
foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) addrs) (return ())
od proof (prove)
goal (1 subgoal):
 1. do cdom <- curDomain;
foldr (\<lambda>x y. do _ <- threadSet (F cdom) x;
y
od) addrs (return ())
od = foldr (\<lambda>x y. do xa <- curDomain;
_ <- threadSet (F xa) x;
y
od) addrs (return ()) \<Longrightarrow> do cdom <- curDomain;
_ <- threadSet (F cdom) addr;
foldr (\<lambda>x y. do _ <- threadSet (F cdom) x;
y
od) addrs (return ())
od = do x <- curDomain;
_ <- threadSet (F x) addr;
foldr (\<lambda>x y. do xa <- curDomain;
_ <- threadSet (F xa) x;
y
od) addrs (return ())
od proof (prove)
goal (1 subgoal):
 1. do cdom <- curDomain;
foldr (\<lambda>x y. do _ <- threadSet (F cdom) x;
y
od) addrs (return ())
od = foldr (\<lambda>x y. do xa <- curDomain;
_ <- threadSet (F xa) x;
y
od) addrs (return ()) \<Longrightarrow> do cdom <- curDomain;
threadSet (F cdom) addr;
cdom <- curDomain;
foldr (\<lambda>x y. do _ <- threadSet (F cdom) x;
y
od) addrs (return ())
od = do x <- curDomain;
_ <- threadSet (F x) addr;
foldr (\<lambda>x y. do xa <- curDomain;
_ <- threadSet (F xa) x;
y
od) addrs (return ())
od proof (prove)
goal:
No subgoals! proof (state)
this:
do cdom <- curDomain;
mapM_x (threadSet (F cdom)) (addr # addrs)
od = mapM_x (\<lambda>addr. do cdom <- curDomain;
threadSet (F cdom) addr
od) (addr # addrs)

goal:
No subgoals!