theory Untyped_DR

lemma monad_commute_set_cap_gets_cdt:
  "monad_commute \<top> (KHeap_D.set_cap ptr cap) (gets cdl_cdt)" apply (simp add: monad_commute_def gets_def get_def
     assert_def fail_def bind_def return_def) apply auto[1] apply (rule bexI[rotated]) apply simp apply simp apply (drule use_valid) apply (rule KHeap_D_set_cap_cdl_cdt) prefer 2 apply (fastforce +)[2] apply (rule bexI[rotated]) apply simp apply simp apply (drule use_valid) apply (rule KHeap_D_set_cap_cdl_cdt) prefer 2 apply (fastforce +)[2] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (KHeap_D.set_cap ptr cap) (gets cdl_cdt) proof (prove)
goal (1 subgoal):
 1. \<forall>s. (\<Union>a\<in>fst (KHeap_D.set_cap ptr cap s). fst (case a of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False))) = (\<Union>a\<in>fst (KHeap_D.set_cap ptr cap s). fst (case a of (x, sa) \<Rightarrow> ({(((), cdl_cdt s), sa)}, False))) \<and> ((\<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). snd (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False))) \<or> snd (KHeap_D.set_cap ptr cap s)) = ((\<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). snd (case x of (x, sa) \<Rightarrow> ({(((), cdl_cdt s), sa)}, False))) \<or> snd (KHeap_D.set_cap ptr cap s)) proof (prove)
goal (2 subgoals):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt ba), ba) \<in> fst (case x of (x, sa) \<Rightarrow> ({(((), cdl_cdt s), sa)}, False))
 2. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (3 subgoals):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> ?x42 s ba \<in> fst (KHeap_D.set_cap ptr cap s)
 2. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> (((), cdl_cdt ba), ba) \<in> fst (case ?x42 s ba of (x, sa) \<Rightarrow> ({(((), cdl_cdt s), sa)}, False))
 3. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (2 subgoals):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> (((), cdl_cdt ba), ba) \<in> fst (case ((), ba) of (x, sa) \<Rightarrow> ({(((), cdl_cdt s), sa)}, False))
 2. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (2 subgoals):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> cdl_cdt ba = cdl_cdt s
 2. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (4 subgoals):
 1. \<And>s ba. \<lbrace>?P45 s ba\<rbrace> KHeap_D.set_cap ptr cap \<lbrace>?Q45 s ba\<rbrace>
 2. \<And>s ba. ?P45 s ba s
 3. \<And>s ba. ?Q45 s ba () ba \<Longrightarrow> cdl_cdt ba = cdl_cdt s
 4. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (3 subgoals):
 1. \<And>s ba. ?P49 s ba (cdl_cdt s)
 2. \<And>s ba. ?P49 s ba (cdl_cdt ba) \<Longrightarrow> cdl_cdt ba = cdl_cdt s
 3. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (3 subgoals):
 1. \<And>s ba. ?P49 s ba (cdl_cdt ba) \<Longrightarrow> cdl_cdt ba = cdl_cdt s
 2. \<And>s ba. ?P49 s ba (cdl_cdt s)
 3. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap ptr cap s). (((), cdl_cdt s), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (2 subgoals):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> ?x57 s ba \<in> fst (KHeap_D.set_cap ptr cap s)
 2. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> (((), cdl_cdt s), ba) \<in> fst (case ?x57 s ba of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> (((), cdl_cdt s), ba) \<in> fst (case ((), ba) of (x, s) \<Rightarrow> ({(((), cdl_cdt s), s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s ba. ((), ba) \<in> fst (KHeap_D.set_cap ptr cap s) \<Longrightarrow> cdl_cdt s = cdl_cdt ba proof (prove)
goal (3 subgoals):
 1. \<And>s ba. \<lbrace>?P60 s ba\<rbrace> KHeap_D.set_cap ptr cap \<lbrace>?Q60 s ba\<rbrace>
 2. \<And>s ba. ?P60 s ba s
 3. \<And>s ba. ?Q60 s ba () ba \<Longrightarrow> cdl_cdt s = cdl_cdt ba proof (prove)
goal (2 subgoals):
 1. \<And>s ba. ?P64 s ba (cdl_cdt s)
 2. \<And>s ba. ?P64 s ba (cdl_cdt ba) \<Longrightarrow> cdl_cdt s = cdl_cdt ba proof (prove)
goal (2 subgoals):
 1. \<And>s ba. ?P64 s ba (cdl_cdt ba) \<Longrightarrow> cdl_cdt s = cdl_cdt ba
 2. \<And>s ba. ?P64 s ba (cdl_cdt s) proof (prove)
goal:
No subgoals!