theory CNode_AC

lemma set_cdt_empty_slot_ext_comm:
  "(do set_cdt c; empty_slot_ext slot slot_p od) =
   (do empty_slot_ext slot slot_p; set_cdt c od)" supply K_bind_def[simp del] apply (clarsimp simp: set_cdt_def empty_slot_ext_def
                        update_cdt_list_def set_cdt_list_def) apply (simp only: modify_def[symmetric]) apply (rule monad_commuteI2) apply monad_commute_default apply monad_eq done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do set_cdt c;
empty_slot_ext slot slot_p
od = do empty_slot_ext slot slot_p;
set_cdt c
od proof (prove)
goal (1 subgoal):
 1. do set_cdt c;
empty_slot_ext slot slot_p
od = do empty_slot_ext slot slot_p;
set_cdt c
od proof (prove)
goal (1 subgoal):
 1. do do s <- get;
put (s\<lparr>cdt := c\<rparr>)
od;
t <- gets cdt_list;
s <- get;
put (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> t(slot := []) | Some p \<Rightarrow> if p = slot then t(slot := list_remove (t slot) slot) else t(p := list_replace_list (t p) slot (t slot), slot := [])) s)
od = do do t <- gets cdt_list;
s <- get;
put (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> t(slot := []) | Some p \<Rightarrow> if p = slot then t(slot := list_remove (t slot) slot) else t(p := list_replace_list (t p) slot (t slot), slot := [])) s)
od;
s <- get;
put (s\<lparr>cdt := c\<rparr>)
od proof (prove)
goal (1 subgoal):
 1. do modify (cdt_update (\<lambda>_. c));
t <- gets cdt_list;
modify (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> t(slot := []) | Some p \<Rightarrow> if p = slot then t(slot := list_remove (t slot) slot) else t(p := list_replace_list (t p) slot (t slot), slot := [])))
od = do do t <- gets cdt_list;
modify (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> t(slot := []) | Some p \<Rightarrow> if p = slot then t(slot := list_remove (t slot) slot) else t(p := list_replace_list (t p) slot (t slot), slot := [])))
od;
modify (cdt_update (\<lambda>_. c))
od proof (prove)
goal (2 subgoals):
 1. monad_commute ?P6 (modify (cdt_update (\<lambda>_. c))) (do t <- gets cdt_list;
modify (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> t(slot := []) | Some p \<Rightarrow> if p = slot then t(slot := list_remove (t slot) slot) else t(p := list_replace_list (t p) slot (t slot), slot := [])))
od)
 2. \<And>s. ?P6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. (\<forall>x. (\<exists>xa. xa \<in> fst (gets cdt_list (s\<lparr>cdt := c\<rparr>)) \<and> x = fst xa) = (\<exists>xa. xa \<in> fst (gets cdt_list s) \<and> x = fst xa)) \<and> snd (gets cdt_list (s\<lparr>cdt := c\<rparr>)) = snd (gets cdt_list s)) and (\<lambda>s. s\<lparr>cdt_list := case slot_p of None \<Rightarrow> (cdt_list s)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list s)(slot := list_remove (cdt_list s slot) slot) else (cdt_list s)(p := list_replace_list (cdt_list s p) slot (cdt_list s slot), slot := []), cdt := c\<rparr> = cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> (cdt_list s)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list s)(slot := list_remove (cdt_list s slot) slot) else (cdt_list s)(p := list_replace_list (cdt_list s p) slot (cdt_list s slot), slot := [])) (s\<lparr>cdt := c\<rparr>))) s proof (prove)
goal:
No subgoals!