theory Intent_DR

lemma update_tcb_cxt_eq_dupdate_tcb_intent:
  "\<lbrakk>
    cdl_objects (transform b) y = Some (Tcb t);
    kheap b y = Some (TCB obj);
    \<exists>etcb'. ekheap b y = Some etcb';
    obj' = tcb_arch_update (arch_tcb_context_set cxt) obj;
    not_idle_thread y b;
    intent = transform_full_intent (machine_state (update_kheap ((kheap b)(y\<mapsto>(TCB obj'))) b)) y obj'
   \<rbrakk>
    \<Longrightarrow> dupdate_cdl_object y (Tcb (dupdate_tcb_intent intent t)) (transform b)
    = transform (update_kheap ((kheap b)(y\<mapsto> (TCB obj'))) b)" apply (clarsimp simp:transform_def transform_current_thread_def
                       not_idle_thread_def transform_objects_def) apply (rule ext, clarsimp) apply (rule conjI) apply (clarsimp simp:restrict_map_Some_iff) apply (clarsimp simp:transform_tcb_def restrict_map_def map_add_def) apply (clarsimp simp:transform_tcb_def restrict_map_def map_add_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl_objects (transform b) y = Some (Tcb t); kheap b y = Some (TCB obj); \<exists>etcb'. ekheap b y = Some etcb'; obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; not_idle_thread y b; intent = transform_full_intent (machine_state (update_kheap ((kheap b)(y \<mapsto> TCB obj')) b)) y obj'\<rbrakk> \<Longrightarrow> dupdate_cdl_object y (Tcb (dupdate_tcb_intent intent t)) (transform b) = transform (update_kheap ((kheap b)(y \<mapsto> TCB obj')) b) proof (prove)
goal (1 subgoal):
 1. \<And>etcb'. \<lbrakk>transform_tcb (machine_state b) y obj etcb' = Tcb t; kheap b y = Some (TCB obj); obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; y \<noteq> idle_thread b; intent = transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj); ekheap b y = Some etcb'\<rbrakk> \<Longrightarrow> ((\<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)))(y \<mapsto> Tcb (dupdate_tcb_intent (transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj)) t)) = (\<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)) (if ptr = y then Some (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj)) else (kheap b |` (- {idle_thread b} - {y})) ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>etcb' x. \<lbrakk>transform_tcb (machine_state b) y obj etcb' = Tcb t; kheap b y = Some (TCB obj); obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; y \<noteq> idle_thread b; intent = transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj); ekheap b y = Some etcb'\<rbrakk> \<Longrightarrow> (x = y \<longrightarrow> Tcb (dupdate_tcb_intent (transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj)) t) = transform_tcb (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj) etcb') \<and> (x \<noteq> y \<longrightarrow> ((\<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))) x = ((\<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)) (if ptr = y then Some (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj)) else (kheap b |` (- {idle_thread b} - {y})) ptr))) x) proof (prove)
goal (2 subgoals):
 1. \<And>etcb' x. \<lbrakk>transform_tcb (machine_state b) y obj etcb' = Tcb t; kheap b y = Some (TCB obj); obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; y \<noteq> idle_thread b; intent = transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj); ekheap b y = Some etcb'\<rbrakk> \<Longrightarrow> x = y \<longrightarrow> Tcb (dupdate_tcb_intent (transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj)) t) = transform_tcb (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj) etcb'
 2. \<And>etcb' x. \<lbrakk>transform_tcb (machine_state b) y obj etcb' = Tcb t; kheap b y = Some (TCB obj); obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; y \<noteq> idle_thread b; intent = transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj); ekheap b y = Some etcb'\<rbrakk> \<Longrightarrow> x \<noteq> y \<longrightarrow> ((\<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))) x = ((\<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)) (if ptr = y then Some (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj)) else (kheap b |` (- {idle_thread b} - {y})) ptr))) x proof (prove)
goal (2 subgoals):
 1. \<And>etcb'. \<lbrakk>transform_tcb (machine_state b) y obj etcb' = Tcb t; kheap b y = Some (TCB obj); obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; y \<noteq> idle_thread b; intent = transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj); ekheap b y = Some etcb'\<rbrakk> \<Longrightarrow> Tcb (dupdate_tcb_intent (transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj)) t) = transform_tcb (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj) etcb'
 2. \<And>etcb' x. \<lbrakk>transform_tcb (machine_state b) y obj etcb' = Tcb t; kheap b y = Some (TCB obj); obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; y \<noteq> idle_thread b; intent = transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj); ekheap b y = Some etcb'\<rbrakk> \<Longrightarrow> x \<noteq> y \<longrightarrow> ((\<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))) x = ((\<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)) (if ptr = y then Some (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj)) else (kheap b |` (- {idle_thread b} - {y})) ptr))) x proof (prove)
goal (1 subgoal):
 1. \<And>etcb' x. \<lbrakk>transform_tcb (machine_state b) y obj etcb' = Tcb t; kheap b y = Some (TCB obj); obj' = tcb_arch_update (arch_tcb_context_set cxt) obj; y \<noteq> idle_thread b; intent = transform_full_intent (machine_state b) y (tcb_arch_update (arch_tcb_context_set cxt) obj); ekheap b y = Some etcb'\<rbrakk> \<Longrightarrow> x \<noteq> y \<longrightarrow> ((\<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))) x = ((\<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)) (if ptr = y then Some (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj)) else (kheap b |` (- {idle_thread b} - {y})) ptr))) x proof (prove)
goal:
No subgoals!