theory Intent_DR

lemma duplicate_corrupt_tcb_intent:
  "do corrupt_tcb_intent epptr; corrupt_tcb_intent epptr od = corrupt_tcb_intent epptr" apply (clarsimp simp:bind_def) apply (rule ext) apply (clarsimp simp:split_def) apply (rule prod_eqI) apply (rule set_eqI) apply clarsimp apply (auto simp:corrupt_tcb_intent_def update_thread_def select_def gets_the_def
          return_def fail_def gets_def get_def assert_opt_def bind_def
          put_def modify_def KHeap_D.set_object_def split_def
          split:option.splits cdl_object.splits)[1] apply clarsimp apply (rule iffI) by (auto simp: corrupt_tcb_intent_def update_thread_def select_def gets_the_def
                  return_def fail_def gets_def get_def assert_opt_def bind_def
                  put_def modify_def KHeap_D.set_object_def split_def
           split: option.splits cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do corrupt_tcb_intent epptr;
corrupt_tcb_intent epptr
od = corrupt_tcb_intent epptr proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<Union>a\<in>fst (corrupt_tcb_intent epptr s). fst (case a of (y, x) \<Rightarrow> corrupt_tcb_intent epptr x), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (case x of (y, x) \<Rightarrow> corrupt_tcb_intent epptr x)) \<or> snd (corrupt_tcb_intent epptr s))) = corrupt_tcb_intent epptr proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>a\<in>fst (corrupt_tcb_intent epptr s). fst (case a of (y, x) \<Rightarrow> corrupt_tcb_intent epptr x), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (case x of (y, x) \<Rightarrow> corrupt_tcb_intent epptr x)) \<or> snd (corrupt_tcb_intent epptr s)) = corrupt_tcb_intent epptr s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>x\<in>fst (corrupt_tcb_intent epptr s). fst (corrupt_tcb_intent epptr (snd x)), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)) = corrupt_tcb_intent epptr s proof (prove)
goal (2 subgoals):
 1. \<And>s. fst (\<Union>x\<in>fst (corrupt_tcb_intent epptr s). fst (corrupt_tcb_intent epptr (snd x)), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)) = fst (corrupt_tcb_intent epptr s)
 2. \<And>s. snd (\<Union>x\<in>fst (corrupt_tcb_intent epptr s). fst (corrupt_tcb_intent epptr (snd x)), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)) = snd (corrupt_tcb_intent epptr s) proof (prove)
goal (2 subgoals):
 1. \<And>s x. (x \<in> fst (\<Union>x\<in>fst (corrupt_tcb_intent epptr s). fst (corrupt_tcb_intent epptr (snd x)), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s))) = (x \<in> fst (corrupt_tcb_intent epptr s))
 2. \<And>s. snd (\<Union>x\<in>fst (corrupt_tcb_intent epptr s). fst (corrupt_tcb_intent epptr (snd x)), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)) = snd (corrupt_tcb_intent epptr s) proof (prove)
goal (2 subgoals):
 1. \<And>s b. (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). ((), b) \<in> fst (corrupt_tcb_intent epptr (snd x))) = (((), b) \<in> fst (corrupt_tcb_intent epptr s))
 2. \<And>s. snd (\<Union>x\<in>fst (corrupt_tcb_intent epptr s). fst (corrupt_tcb_intent epptr (snd x)), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)) = snd (corrupt_tcb_intent epptr s) proof (prove)
goal (1 subgoal):
 1. \<And>s. snd (\<Union>x\<in>fst (corrupt_tcb_intent epptr s). fst (corrupt_tcb_intent epptr (snd x)), (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)) = snd (corrupt_tcb_intent epptr s) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)) = snd (corrupt_tcb_intent epptr s) proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s) \<Longrightarrow> snd (corrupt_tcb_intent epptr s)
 2. \<And>s. snd (corrupt_tcb_intent epptr s) \<Longrightarrow> (\<exists>x\<in>fst (corrupt_tcb_intent epptr s). snd (corrupt_tcb_intent epptr (snd x))) \<or> snd (corrupt_tcb_intent epptr s)