theory Detype_R

lemma modify_mapM_x:
  "(modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) list))) =
   (mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x\<mapsto> obj)))) (rev list))" apply (induct list) apply (clarsimp simp:mapM_x_Nil) apply (rule ext) apply (simp add:simpler_modify_def return_def) apply (clarsimp simp:mapM_x_append mapM_x_singleton simpler_modify_def) apply (drule sym) apply (rule ext) apply (simp add:Fun.comp_def bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) list)) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev list) proof (prove)
goal (2 subgoals):
 1. modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) [])) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev [])
 2. \<And>a list. modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) list)) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev list) \<Longrightarrow> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) (a # list))) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev (a # list)) proof (prove)
goal (2 subgoals):
 1. modify (ksPSpace_update (\<lambda>a. a)) = return ()
 2. \<And>a list. modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) list)) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev list) \<Longrightarrow> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) (a # list))) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev (a # list)) proof (prove)
goal (2 subgoals):
 1. \<And>x. modify (ksPSpace_update (\<lambda>a. a)) x = return () x
 2. \<And>a list. modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) list)) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev list) \<Longrightarrow> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) (a # list))) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) list)) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev list) \<Longrightarrow> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> obj)) (a # list))) = mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> obj)))) (rev (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. (\<lambda>a. ({((), ksPSpace_update (foldr (\<lambda>addr map a. if a = addr then Some obj else map a) list) a)}, False)) = mapM_x (\<lambda>x a. ({((), ksPSpace_update (\<lambda>m a. if a = x then Some obj else m a) a)}, False)) (rev list) \<Longrightarrow> (\<lambda>b. ({((), ksPSpace_update (\<lambda>b c. if c = a then Some obj else foldr (\<lambda>addr map a. if a = addr then Some obj else map a) list b c) b)}, False)) = do x <- mapM_x (\<lambda>x a. ({((), ksPSpace_update (\<lambda>m a. if a = x then Some obj else m a) a)}, False)) (rev list);
\<lambda>b. ({((), ksPSpace_update (\<lambda>m b. if b = a then Some obj else m b) b)}, False)
od proof (prove)
goal (1 subgoal):
 1. \<And>a list. mapM_x (\<lambda>x a. ({((), ksPSpace_update (\<lambda>m a. if a = x then Some obj else m a) a)}, False)) (rev list) = (\<lambda>a. ({((), ksPSpace_update (foldr (\<lambda>addr map a. if a = addr then Some obj else map a) list) a)}, False)) \<Longrightarrow> (\<lambda>b. ({((), ksPSpace_update (\<lambda>b c. if c = a then Some obj else foldr (\<lambda>addr map a. if a = addr then Some obj else map a) list b c) b)}, False)) = do x <- mapM_x (\<lambda>x a. ({((), ksPSpace_update (\<lambda>m a. if a = x then Some obj else m a) a)}, False)) (rev list);
\<lambda>b. ({((), ksPSpace_update (\<lambda>m b. if b = a then Some obj else m b) b)}, False)
od proof (prove)
goal (1 subgoal):
 1. \<And>a list x. mapM_x (\<lambda>x a. ({((), ksPSpace_update (\<lambda>m a. if a = x then Some obj else m a) a)}, False)) (rev list) = (\<lambda>a. ({((), ksPSpace_update (foldr (\<lambda>addr map a. if a = addr then Some obj else map a) list) a)}, False)) \<Longrightarrow> ({((), ksPSpace_update (\<lambda>b c. if c = a then Some obj else foldr (\<lambda>addr map a. if a = addr then Some obj else map a) list b c) x)}, False) = (do x <- mapM_x (\<lambda>x a. ({((), ksPSpace_update (\<lambda>m a. if a = x then Some obj else m a) a)}, False)) (rev list);
\<lambda>b. ({((), ksPSpace_update (\<lambda>m b. if b = a then Some obj else m b) b)}, False)
od) x proof (prove)
goal:
No subgoals!