theory ArchADT_IF_Refine

lemma valid_device_abs_state_eq[ADT_IF_Refine_assms]:
  "valid_machine_state s \<Longrightarrow> abs_state s = s" apply (simp add: abs_state_def observable_memory_def) apply (case_tac s) apply clarsimp apply (case_tac machine_state) apply clarsimp apply (rule ext) apply (fastforce simp: user_mem_def option_to_0_def valid_machine_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state s \<Longrightarrow> abs_state s = s proof (prove)
goal (1 subgoal):
 1. valid_machine_state s \<Longrightarrow> s\<lparr>machine_state := machine_state s\<lparr>underlying_memory := option_to_0 \<circ> user_mem s\<rparr>\<rparr> = s proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdt is_original_cap cur_thread idle_thread machine_statea interrupt_irq_node interrupt_states arch_state exst. \<lbrakk>valid_machine_state s; s = \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_statea, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>\<rbrakk> \<Longrightarrow> s\<lparr>machine_state := machine_state s\<lparr>underlying_memory := option_to_0 \<circ> user_mem s\<rparr>\<rparr> = s proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdt is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state exst. \<lbrakk>valid_machine_state \<lparr>kheap = kheap, cdt = cdt, 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>; s = \<lparr>kheap = kheap, cdt = cdt, 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>\<rbrakk> \<Longrightarrow> machine_state\<lparr>underlying_memory := option_to_0 \<circ> user_mem \<lparr>kheap = kheap, cdt = cdt, 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>\<rparr> = machine_state proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdt is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state exst irq_masks irq_state underlying_memory device_state exclusive_state machine_state_rest. \<lbrakk>valid_machine_state \<lparr>kheap = kheap, cdt = cdt, 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>; s = \<lparr>kheap = kheap, cdt = cdt, 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>; machine_state = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memory, device_state = device_state, exclusive_state = exclusive_state, machine_state_rest = machine_state_rest\<rparr>\<rbrakk> \<Longrightarrow> machine_state\<lparr>underlying_memory := option_to_0 \<circ> user_mem \<lparr>kheap = kheap, cdt = cdt, 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>\<rparr> = machine_state proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdt is_original_cap cur_thread idle_thread interrupt_irq_node interrupt_states arch_state exst irq_masks irq_state underlying_memory device_state a b machine_state_rest. \<lbrakk>valid_machine_state \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memory, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>; s = \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memory, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>\<rbrakk> \<Longrightarrow> option_to_0 \<circ> user_mem \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memory, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> = underlying_memory proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdt is_original_cap cur_thread idle_thread interrupt_irq_node interrupt_states arch_state exst irq_masks irq_state underlying_memory device_state a b machine_state_rest x. \<lbrakk>valid_machine_state \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memory, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>; s = \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memory, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>\<rbrakk> \<Longrightarrow> (option_to_0 \<circ> user_mem \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memory, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>) x = underlying_memory x proof (prove)
goal:
No subgoals!