theory KHeap_DR

lemma tcb_filter_modify_decompose:
  "\<lbrakk> filter_set = setA \<union> setB; (setA \<inter> setB) = {}\<rbrakk>
    \<Longrightarrow> (do tcb_filter_modify setA f;tcb_filter_modify setB f od) = (tcb_filter_modify filter_set f)" apply (simp add:bind_def) apply (rule ext) apply (clarsimp simp:tcb_filter_modify_def bind_def simpler_modify_def) apply (case_tac s) apply (clarsimp simp:option_map_def) apply (rule ext) apply (clarsimp split:option.splits|rule conjI)+ apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}\<rbrakk> \<Longrightarrow> do tcb_filter_modify setA f;
tcb_filter_modify setB f
od = tcb_filter_modify filter_set f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}\<rbrakk> \<Longrightarrow> (\<lambda>s. (\<Union>a\<in>fst (tcb_filter_modify setA f s). fst (case a of (y, x) \<Rightarrow> tcb_filter_modify setB f x), (\<exists>x\<in>fst (tcb_filter_modify setA f s). snd (case x of (y, x) \<Rightarrow> tcb_filter_modify setB f x)) \<or> snd (tcb_filter_modify setA f s))) = tcb_filter_modify (setA \<union> setB) f proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (tcb_filter_modify setA f s). fst (case a of (y, x) \<Rightarrow> tcb_filter_modify setB f x), (\<exists>x\<in>fst (tcb_filter_modify setA f s). snd (case x of (y, x) \<Rightarrow> tcb_filter_modify setB f x)) \<or> snd (tcb_filter_modify setA f s)) = tcb_filter_modify (setA \<union> setB) f s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}\<rbrakk> \<Longrightarrow> s\<lparr>cdl_objects := \<lambda>x. if x \<in> setB then f (cdl_objects (s\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects s x) else cdl_objects s x\<rparr>) x) else cdl_objects (s\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects s x) else cdl_objects s x\<rparr>) x\<rparr> = s\<lparr>cdl_objects := \<lambda>x. if x \<in> setA \<or> x \<in> setB then f (cdl_objects s x) else cdl_objects s x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}; 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>\<rbrakk> \<Longrightarrow> s\<lparr>cdl_objects := \<lambda>x. if x \<in> setB then f (cdl_objects (s\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects s x) else cdl_objects s x\<rparr>) x) else cdl_objects (s\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects s x) else cdl_objects s x\<rparr>) x\<rparr> = s\<lparr>cdl_objects := \<lambda>x. if x \<in> setA \<or> x \<in> setB then f (cdl_objects s x) else cdl_objects s x\<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. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. if x \<in> setB then f (cdl_objects (\<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>\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects \<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> x) else cdl_objects \<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> x\<rparr>) x) else cdl_objects (\<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>\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects \<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> x) else cdl_objects \<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> x\<rparr>) x) = (\<lambda>x. if x \<in> setA \<or> x \<in> setB then f (cdl_objects \<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> x) else cdl_objects \<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> x) 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 x. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}\<rbrakk> \<Longrightarrow> (if x \<in> setB then f (cdl_objects (\<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>\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects \<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> x) else cdl_objects \<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> x\<rparr>) x) else cdl_objects (\<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>\<lparr>cdl_objects := \<lambda>x. if x \<in> setA then f (cdl_objects \<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> x) else cdl_objects \<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> x\<rparr>) x) = (if x \<in> setA \<or> x \<in> setB then f (cdl_objects \<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> x) else cdl_objects \<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> x) proof (prove)
goal (1 subgoal):
 1. \<And>cdl_objects x. \<lbrakk>filter_set = setA \<union> setB; setA \<inter> setB = {}; x \<in> setA; x \<in> setB\<rbrakk> \<Longrightarrow> f (f (cdl_objects x)) = f (cdl_objects x) proof (prove)
goal:
No subgoals!