theory KHeap_DR

lemma abs_remove_parent_def':
 "(do a\<leftarrow> gets cdt;set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p) (slot := None)) od)= (modify (\<lambda>s. abs_cdt_single_remove(abs_cdt_set_update s {x. if cdt s x = Some slot then True else False} (\<lambda>x. cdt s slot)) slot))" apply (clarsimp simp:remove_parent_def simpler_modify_def bind_def set_cdt_def put_def get_def gets_def return_def) apply (rule ext) apply (clarsimp simp:abs_cdt_single_remove_def abs_cdt_set_update_def) apply (case_tac s) apply clarsimp apply (rule ext) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od = modify (\<lambda>s. abs_cdt_single_remove (abs_cdt_set_update s {x. if cdt s x = Some slot then True else False} (\<lambda>x. cdt s slot)) slot) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ({((), s\<lparr>cdt := (\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)\<rparr>)}, False)) = (\<lambda>s. ({((), abs_cdt_single_remove (abs_cdt_set_update s {x. cdt s x = Some slot} (\<lambda>x. cdt s slot)) slot)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s. ({((), s\<lparr>cdt := (\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)\<rparr>)}, False) = ({((), abs_cdt_single_remove (abs_cdt_set_update s {x. cdt s x = Some slot} (\<lambda>x. cdt s slot)) slot)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s. s\<lparr>cdt := (\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)\<rparr> = s\<lparr>cdt := \<lambda>x. if x = slot then None else cdt (s\<lparr>cdt := \<lambda>x. if cdt s x = Some slot then cdt s slot else cdt s x\<rparr>) x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s kheap cdta is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state exst. s = \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> \<Longrightarrow> s\<lparr>cdt := (\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)\<rparr> = s\<lparr>cdt := \<lambda>x. if x = slot then None else cdt (s\<lparr>cdt := \<lambda>x. if cdt s x = Some slot then cdt s slot else cdt s x\<rparr>) x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdta is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state exst. (\<lambda>p. if cdta p = Some slot then cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> slot else cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> p)(slot := None) = (\<lambda>x. if x = slot then None else cdt (\<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>\<lparr>cdt := \<lambda>x. if cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> x = Some slot then cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> slot else cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> x\<rparr>) x) proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdta is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state exst x. ((\<lambda>p. if cdta p = Some slot then cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> slot else cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> p)(slot := None)) x = (if x = slot then None else cdt (\<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>\<lparr>cdt := \<lambda>x. if cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> x = Some slot then cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> slot else cdt \<lparr>kheap = kheap, cdt = cdta, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> x\<rparr>) x) proof (prove)
goal:
No subgoals!