theory Untyped_DR

lemma set_cap_set_parent_swap:
  "do _ \<leftarrow> KHeap_D.set_cap ptr cap; set_parent ptr2 ptr3 od
   = do _ \<leftarrow> set_parent ptr2 ptr3; KHeap_D.set_cap ptr cap od" apply (rule bind_return_eq) apply (subst bind_assoc)+ apply (rule ext) apply (subst monad_commute_simple) apply (simp add:set_parent_def) apply (rule monad_commute_split)+ apply (rule monad_commute_set_cap_cdt) apply (rule monad_commute_set_cap_assert) apply wp apply (rule monad_commute_set_cap_gets_cdt) apply clarsimp apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- KHeap_D.set_cap ptr cap;
set_parent ptr2 ptr3
od = do _ <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap
od proof (prove)
goal (1 subgoal):
 1. do _ <- KHeap_D.set_cap ptr cap;
set_parent ptr2 ptr3
od >>= return = do _ <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap
od >>= return proof (prove)
goal (1 subgoal):
 1. do x <- KHeap_D.set_cap ptr cap;
set_parent ptr2 ptr3 >>= return
od = do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- KHeap_D.set_cap ptr cap;
set_parent ptr2 ptr3 >>= return
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (3 subgoals):
 1. \<And>x. monad_commute (?P4 x) (KHeap_D.set_cap ptr cap) (set_parent ptr2 ptr3)
 2. \<And>x. ?P4 x x
 3. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (3 subgoals):
 1. \<And>x. monad_commute (?P4 x) (KHeap_D.set_cap ptr cap) (do cdt <- gets cdl_cdt;
y <- assert (cdt ptr2 = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>)
od)
 2. \<And>x. ?P4 x x
 3. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (7 subgoals):
 1. \<And>x r ra. monad_commute (?Q9 x r ra) (KHeap_D.set_cap ptr cap) (modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>))
 2. \<And>x r. monad_commute (?P9 x r) (KHeap_D.set_cap ptr cap) (assert (r ptr2 = None))
 3. \<And>x r. \<lbrace>?P'9 x r\<rbrace> assert (r ptr2 = None) \<lbrace>?Q9 x r\<rbrace>
 4. \<And>x. monad_commute (?P5 x) (KHeap_D.set_cap ptr cap) (gets cdl_cdt)
 5. \<And>x. \<lbrace>?P'5 x\<rbrace> gets cdl_cdt \<lbrace>\<lambda>r. ?P9 x r and ?P'9 x r\<rbrace>
 6. \<And>x. (?P5 x and ?P'5 x) x
 7. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (6 subgoals):
 1. \<And>x r. monad_commute (?P9 x r) (KHeap_D.set_cap ptr cap) (assert (r ptr2 = None))
 2. \<And>x r. \<lbrace>?P'9 x r\<rbrace> assert (r ptr2 = None) \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>x. monad_commute (?P5 x) (KHeap_D.set_cap ptr cap) (gets cdl_cdt)
 4. \<And>x. \<lbrace>?P'5 x\<rbrace> gets cdl_cdt \<lbrace>\<lambda>r. ?P9 x r and ?P'9 x r\<rbrace>
 5. \<And>x. (?P5 x and ?P'5 x) x
 6. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (5 subgoals):
 1. \<And>x r. \<lbrace>?P'9 x r\<rbrace> assert (r ptr2 = None) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>x. monad_commute (?P5 x) (KHeap_D.set_cap ptr cap) (gets cdl_cdt)
 3. \<And>x. \<lbrace>?P'5 x\<rbrace> gets cdl_cdt \<lbrace>\<lambda>r. (\<lambda>_. True) and ?P'9 x r\<rbrace>
 4. \<And>x. (?P5 x and ?P'5 x) x
 5. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (4 subgoals):
 1. \<And>x. monad_commute (?P5 x) (KHeap_D.set_cap ptr cap) (gets cdl_cdt)
 2. \<And>x. \<lbrace>?P'5 x\<rbrace> gets cdl_cdt \<lbrace>\<lambda>r. (\<lambda>_. True) and (\<lambda>s. r ptr2 = None \<longrightarrow> True)\<rbrace>
 3. \<And>x. (?P5 x and ?P'5 x) x
 4. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?P'5 x\<rbrace> gets cdl_cdt \<lbrace>\<lambda>r. (\<lambda>_. True) and (\<lambda>s. r ptr2 = None \<longrightarrow> True)\<rbrace>
 2. \<And>x. ((\<lambda>_. True) and ?P'5 x) x
 3. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. ((\<lambda>_. True) and ?P'5 x) x
 2. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (do y <- set_parent ptr2 ptr3;
x <- KHeap_D.set_cap ptr cap;
return y
od) x = (do x <- set_parent ptr2 ptr3;
KHeap_D.set_cap ptr cap >>= return
od) x proof (prove)
goal:
No subgoals!