theory KHeap_DR

lemma thread_set_fault_corres:
  assumes r: "\<And>t. f (tcb_has_fault (t::Structures_A.tcb)) = (case (ft (tcb_fault t)) of None \<Rightarrow> False | _ \<Rightarrow> True)"
  shows "dcorres dc \<top> (tcb_at thread and not_idle_thread thread and valid_etcbs) (update_thread_fault thread f )
    (thread_set (tcb_fault_update ft) thread)" apply (clarsimp simp:thread_set_def update_thread_fault_def) apply (rule dcorres_gets_the) apply (simp_all) apply (clarsimp, drule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:opt_object_tcb not_idle_thread_def transform_tcb_def) apply (rule dcorres_set_object_tcb) apply (clarsimp simp: transform_tcb_def tcb_at_def cong: transform_full_intent_cong
                      dest!: get_tcb_SomeD get_etcb_SomeD ) apply (cut_tac t = obj' in r) apply (clarsimp split:option.splits) apply ((clarsimp simp:opt_object_tcb tcb_at_def get_etcb_def dest!:get_tcb_SomeD get_etcb_SomeD)+)[3] apply (clarsimp, drule(1) valid_etcbs_get_tcb_get_etcb, clarsimp simp:opt_object_tcb not_idle_thread_def get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at thread and not_idle_thread thread and valid_etcbs) (update_thread_fault thread f) (thread_set (tcb_fault_update ft) thread) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at thread and not_idle_thread thread and valid_etcbs) (do t <- KHeap_D.get_object thread;
case t of Tcb tcb \<Rightarrow> KHeap_D.set_object thread (Tcb (tcb\<lparr>cdl_tcb_has_fault := f (cdl_tcb_has_fault tcb)\<rparr>)) | _ \<Rightarrow> fail
od) (do tcb <- gets_the (get_tcb thread);
KHeap_A.set_object thread (TCB (tcb_fault_update ft tcb))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>s = transform s'; True; (tcb_at thread and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; cdl_objects s thread = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object thread (Tcb (tcb\<lparr>cdl_tcb_has_fault := f (cdl_tcb_has_fault tcb)\<rparr>)) | _ \<Rightarrow> fail) (KHeap_A.set_object thread (TCB (tcb_fault_update ft obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (tcb_at thread and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; get_tcb thread s' = Some obj'; cdl_objects (transform s') thread = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object thread (Tcb (tcb\<lparr>cdl_tcb_has_fault := f (cdl_tcb_has_fault tcb)\<rparr>)) | _ \<Rightarrow> fail) (KHeap_A.set_object thread (TCB (tcb_fault_update ft obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>get_tcb thread s' = Some obj'; cdl_objects (transform s') thread = Some obj; tcb_at thread s'; not_idle_thread thread s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object thread (Tcb (tcb\<lparr>cdl_tcb_has_fault := f (cdl_tcb_has_fault tcb)\<rparr>)) | _ \<Rightarrow> fail) (KHeap_A.set_object thread (TCB (tcb_fault_update ft obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_object thread (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') thread obj', cdl_tcb_has_fault = f (\<exists>y. tcb_fault obj' = Some y), cdl_tcb_domain = tcb_domain etcb\<rparr>)) (KHeap_A.set_object thread (TCB (tcb_fault_update ft obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb'. transform_tcb (machine_state s') thread (tcb_fault_update ft obj') etcb' = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') thread obj', cdl_tcb_has_fault = f (\<exists>y. tcb_fault obj' = Some y), cdl_tcb_domain = tcb_domain etcb\<rparr> \<and> ekheap s' thread = Some etcb'
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' thread \<noteq> None
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' thread \<noteq> None
 5. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>thread \<noteq> idle_thread s'; ekheap s' thread = Some etcb; kheap s' thread = Some (TCB obj')\<rbrakk> \<Longrightarrow> (\<exists>y. ft (tcb_fault obj') = Some y) = f (\<exists>y. tcb_fault obj' = Some y)
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' thread \<noteq> None
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' thread \<noteq> None
 5. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>thread \<noteq> idle_thread s'; ekheap s' thread = Some etcb; kheap s' thread = Some (TCB obj'); f (tcb_has_fault obj') = (case ft (tcb_fault obj') of None \<Rightarrow> False | Some a \<Rightarrow> True)\<rbrakk> \<Longrightarrow> (\<exists>y. ft (tcb_fault obj') = Some y) = f (\<exists>y. tcb_fault obj' = Some y)
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' thread \<noteq> None
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' thread \<noteq> None
 5. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' thread \<noteq> None
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; tcb_at thread s'; thread \<noteq> idle_thread s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' thread \<noteq> None
 4. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; tcb_at thread s' \<and> not_idle_thread thread s' \<and> valid_etcbs s'; \<exists>y. get_tcb thread s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal:
No subgoals!