theory Intent_DR

lemma corres_corrupt_tcb_intent_return:
  "dcorres dc \<top> (tcb_at ptr and not_idle_thread ptr and valid_etcbs) (corrupt_tcb_intent ptr) (return x)" supply option.case_cong[cong] apply (clarsimp simp: corres_underlying_def return_def corrupt_tcb_intent_def update_thread_def
                        select_def gets_the_def fail_def gets_def get_def assert_opt_def bind_def
                        put_def modify_def KHeap_D.set_object_def) apply (clarsimp split: option.splits
                  simp: transform_def tcb_at_def transform_objects_def not_idle_thread_def
                  dest!: get_tcb_SomeD) apply (drule(1) valid_etcbs_tcb_etcb) apply (clarsimp) apply (force simp: transform_def transform_tcb_def transform_objects_def not_idle_thread_def
                     tcb_at_def obj_at_def
               split: cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at ptr and not_idle_thread ptr and valid_etcbs) (corrupt_tcb_intent ptr) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at ptr and not_idle_thread ptr and valid_etcbs) (corrupt_tcb_intent ptr) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>tcb_at ptr b; not_idle_thread ptr b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>y\<in>fst ((case cdl_objects (transform b) ptr of None \<Rightarrow> \<lambda>s. ({}, True) | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) (transform b)). \<exists>x\<in>fst (case y of (xa, xb) \<Rightarrow> (case xa of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object ptr (Tcb (dupdate_tcb_intent x tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) xb). case x of (r, x) \<Rightarrow> transform b = x proof (prove)
goal (2 subgoals):
 1. \<And>b tcb. \<lbrakk>ptr \<noteq> idle_thread b; valid_etcbs b; kheap b ptr = Some (TCB tcb); ekheap b ptr = None\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>x\<in>fst ((case undefined of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object ptr (Tcb (dupdate_tcb_intent x tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>). case x of (r, x) \<Rightarrow> \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr> = x
 2. \<And>b tcb x2 x2a. \<lbrakk>ptr \<noteq> idle_thread b; valid_etcbs b; kheap b ptr = Some (TCB tcb); ekheap b ptr = Some x2a; transform_tcb (machine_state b) ptr tcb x2a = x2\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>x\<in>fst ((case x2 of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object ptr (Tcb (dupdate_tcb_intent x tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>). case x of (r, x) \<Rightarrow> \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr> = x proof (prove)
goal (2 subgoals):
 1. \<And>b tcb. \<lbrakk>ptr \<noteq> idle_thread b; kheap b ptr = Some (TCB tcb); ekheap b ptr = None; \<exists>etcb. ekheap b ptr = Some etcb\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>x\<in>fst ((case undefined of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object ptr (Tcb (dupdate_tcb_intent x tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>). case x of (r, x) \<Rightarrow> \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr> = x
 2. \<And>b tcb x2 x2a. \<lbrakk>ptr \<noteq> idle_thread b; valid_etcbs b; kheap b ptr = Some (TCB tcb); ekheap b ptr = Some x2a; transform_tcb (machine_state b) ptr tcb x2a = x2\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>x\<in>fst ((case x2 of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object ptr (Tcb (dupdate_tcb_intent x tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>). case x of (r, x) \<Rightarrow> \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr> = x proof (prove)
goal (1 subgoal):
 1. \<And>b tcb x2 x2a. \<lbrakk>ptr \<noteq> idle_thread b; valid_etcbs b; kheap b ptr = Some (TCB tcb); ekheap b ptr = Some x2a; transform_tcb (machine_state b) ptr tcb x2a = x2\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>x\<in>fst ((case x2 of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object ptr (Tcb (dupdate_tcb_intent x tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr>). case x of (r, x) \<Rightarrow> \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr)), cdl_cdt = transform_cdt b, cdl_current_thread = transform_current_thread b, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = transform_asid_table b, cdl_current_domain = cur_domain b\<rparr> = x proof (prove)
goal:
No subgoals!