theory Tcb_DR

lemma set_mcpriority_transform:
  "\<lbrace>\<lambda>s. transform s = i \<and> valid_etcbs s\<rbrace> set_mcpriority t mcp \<lbrace>\<lambda>rv s. transform s = i\<rbrace>" apply (clarsimp simp: set_mcpriority_def thread_set_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: transform_def transform_current_thread_def transform_objects_def) apply (thin_tac "i = _") apply (rule_tac f="(++) ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}))" in arg_cong) apply (rule ext) apply (rename_tac s tcb ptr) apply (drule (1) valid_etcbs_get_tcb_get_etcb; clarsimp) apply (drule get_etcb_SomeD; drule get_tcb_SomeD) by (case_tac "ptr = idle_thread s";
      clarsimp simp: transform_tcb_def transform_full_intent_set_mcpriority)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. transform s = i \<and> valid_etcbs s\<rbrace> set_mcpriority t mcp \<lbrace>\<lambda>rv s. transform s = i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. transform s = i \<and> valid_etcbs s\<rbrace> do tcb <- gets_the (get_tcb t);
KHeap_A.set_object t (TCB (tcb\<lparr>tcb_mcpriority := mcp\<rparr>))
od \<lbrace>\<lambda>rv s. transform s = i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_etcbs s; i = transform s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s)(t \<mapsto> TCB (y\<lparr>tcb_mcpriority := mcp\<rparr>))) s) = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_etcbs s; i = \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)), cdl_cdt = transform_cdt s, cdl_current_thread = if cur_thread s \<noteq> idle_thread s then Some (cur_thread s) else None, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr>; get_tcb t s = Some y; t \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) (if ptr = t then Some (TCB (y\<lparr>tcb_mcpriority := mcp\<rparr>)) else (kheap s |` (- {idle_thread s} - {t})) ptr)) = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_etcbs s; get_tcb t s = Some y; t \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) (if ptr = t then Some (TCB (y\<lparr>tcb_mcpriority := mcp\<rparr>)) else (kheap s |` (- {idle_thread s} - {t})) ptr)) = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_etcbs s; get_tcb t s = Some y; t \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) (if ptr = t then Some (TCB (y\<lparr>tcb_mcpriority := mcp\<rparr>)) else (kheap s |` (- {idle_thread s} - {t})) ptr)) = (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s y ptr. \<lbrakk>valid_etcbs s; get_tcb t s = Some y; t \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) (if ptr = t then Some (TCB (y\<lparr>tcb_mcpriority := mcp\<rparr>)) else (kheap s |` (- {idle_thread s} - {t})) ptr) = map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb ptr. \<lbrakk>valid_etcbs s; get_tcb t s = Some tcb; t \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) (if ptr = t then Some (TCB (tcb\<lparr>tcb_mcpriority := mcp\<rparr>)) else (kheap s |` (- {idle_thread s} - {t})) ptr) = map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb ptr etcb. \<lbrakk>get_tcb t s = Some tcb; t \<noteq> idle_thread s; get_etcb t s = Some etcb\<rbrakk> \<Longrightarrow> (ptr = t \<longrightarrow> Some (case ekheap s t of Some etcb \<Rightarrow> transform_tcb (machine_state s) t (tcb\<lparr>tcb_mcpriority := mcp\<rparr>) etcb) = map_option (transform_object (machine_state s) t (ekheap s t)) (kheap s t)) \<and> (ptr \<noteq> t \<longrightarrow> map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s} - {t})) ptr) = map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb ptr etcb. \<lbrakk>t \<noteq> idle_thread s; ekheap s t = Some etcb; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (ptr = t \<longrightarrow> Some (case ekheap s t of Some etcb \<Rightarrow> transform_tcb (machine_state s) t (tcb\<lparr>tcb_mcpriority := mcp\<rparr>) etcb) = map_option (transform_object (machine_state s) t (ekheap s t)) (kheap s t)) \<and> (ptr \<noteq> t \<longrightarrow> map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s} - {t})) ptr) = map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))