theory Interrupt_DR

lemma thread_set_time_slice_transform: "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> thread_set_time_slice tptr time \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" apply (clarsimp simp: thread_set_time_slice_def ethread_set_def set_eobject_def | wp)+ apply (clarsimp simp: transform_def transform_objects_def transform_cdt_def transform_current_thread_def transform_asid_table_def) apply (rule_tac y="\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)" in arg_cong) apply (rule ext) apply (rule_tac y="transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)" in arg_cong) apply (rule ext) apply (clarsimp simp: transform_object_def transform_tcb_def restrict_map_def get_etcb_def split: option.splits Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> thread_set_time_slice tptr time \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>cs = transform s; get_etcb tptr s = Some y\<rbrakk> \<Longrightarrow> transform (ekheap_update (\<lambda>_ a. if a = tptr then Some (the (get_etcb tptr s)\<lparr>tcb_time_slice := time\<rparr>) else ekheap s a) s) = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>cs = \<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 = map_lift_over transform_cslot_ptr (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 = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s), cdl_current_domain = cur_domain s\<rparr>; get_etcb tptr s = Some y\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr (((\<lambda>a. if a = tptr then Some (the (get_etcb tptr s)\<lparr>tcb_time_slice := time\<rparr>) else ekheap s a) |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) 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>cs = \<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 = map_lift_over transform_cslot_ptr (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 = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s), cdl_current_domain = cur_domain s\<rparr>; get_etcb tptr s = Some y\<rbrakk> \<Longrightarrow> (\<lambda>a. map_option (transform_object (machine_state s) a (((\<lambda>a. if a = tptr then Some (the (get_etcb tptr s)\<lparr>tcb_time_slice := time\<rparr>) else ekheap s a) |` (- {idle_thread s})) a)) ((kheap s |` (- {idle_thread s})) a)) = (\<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>cs = \<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 = map_lift_over transform_cslot_ptr (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 = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s), cdl_current_domain = cur_domain s\<rparr>; get_etcb tptr s = Some y\<rbrakk> \<Longrightarrow> map_option (transform_object (machine_state s) ptr (((\<lambda>a. if a = tptr then Some (the (get_etcb tptr s)\<lparr>tcb_time_slice := time\<rparr>) else ekheap s a) |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) 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>cs = \<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 = map_lift_over transform_cslot_ptr (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 = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s), cdl_current_domain = cur_domain s\<rparr>; get_etcb tptr s = Some y\<rbrakk> \<Longrightarrow> transform_object (machine_state s) ptr (((\<lambda>a. if a = tptr then Some (the (get_etcb tptr s)\<lparr>tcb_time_slice := time\<rparr>) else ekheap s a) |` (- {idle_thread s})) ptr) = transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s y ptr x. \<lbrakk>cs = \<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 = map_lift_over transform_cslot_ptr (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 = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s), cdl_current_domain = cur_domain s\<rparr>; get_etcb tptr s = Some y\<rbrakk> \<Longrightarrow> transform_object (machine_state s) ptr (((\<lambda>a. if a = tptr then Some (the (get_etcb tptr s)\<lparr>tcb_time_slice := time\<rparr>) else ekheap s a) |` (- {idle_thread s})) ptr) x = transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr) x proof (prove)
goal:
No subgoals!