theory Intent_DR

lemma corrupt_intents_dup: "corrupt_intents f bufp (corrupt_intents g bufp s) = corrupt_intents f bufp s" apply (clarsimp simp:corrupt_intents_def) apply (cases s) apply clarsimp apply (rule ext) apply (case_tac "cdl_objects x") apply (clarsimp simp:map_add_def)+ apply (clarsimp simp: tcb_ipcframe_id_def split:cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corrupt_intents f bufp (corrupt_intents g bufp s) = corrupt_intents f bufp s proof (prove)
goal (1 subgoal):
 1. s\<lparr>cdl_objects := cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None) ++ (\<lambda>ptr. case (cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None)) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = s\<lparr>cdl_objects := cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> \<Longrightarrow> s\<lparr>cdl_objects := cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None) ++ (\<lambda>ptr. case (cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None)) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = s\<lparr>cdl_objects := cdl_objects s ++ (\<lambda>ptr. case cdl_objects s ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> \<Longrightarrow> cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None) ++ (\<lambda>ptr. case (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None)) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None) = cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x. s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> \<Longrightarrow> (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None) ++ (\<lambda>ptr. case (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None)) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)) x = (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)) x proof (prove)
goal (2 subgoals):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; cdl_objects x = None\<rbrakk> \<Longrightarrow> (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None) ++ (\<lambda>ptr. case (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None)) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)) x = (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)) x
 2. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x a. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; cdl_objects x = Some a\<rbrakk> \<Longrightarrow> (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None) ++ (\<lambda>ptr. case (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g ptr) tcb)) else None | Some _ \<Rightarrow> None)) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)) x = (cdl_objects ++ (\<lambda>ptr. case cdl_objects ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f ptr) tcb)) else None | Some _ \<Rightarrow> None)) x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x a. \<lbrakk>s = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>; cdl_objects x = Some a\<rbrakk> \<Longrightarrow> (case case case case a of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g x) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> cdl_objects x | Some x \<Rightarrow> Some x of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f x) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> case case cdl_objects x of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (g x) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> cdl_objects x | Some x \<Rightarrow> Some x | Some x \<Rightarrow> Some x) = (case case a of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some bufp then Some (Tcb (dupdate_tcb_intent (f x) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> cdl_objects x | Some x \<Rightarrow> Some x) proof (prove)
goal:
No subgoals!