theory Arch_IF

lemma mol_states_equiv_for:
  "machine_op_lift mop \<lbrace>\<lambda>ms. states_equiv_for P Q R S st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>" unfolding machine_op_lift_def apply (simp add: machine_rest_lift_def split_def) apply (wp modify_wp) apply (clarsimp simp: states_equiv_for_def equiv_asids_def) apply (fastforce elim!: equiv_forE intro!: equiv_forI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. states_equiv_for P Q R S st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. states_equiv_for P Q R S st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. states_equiv_for P Q R S st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> (machine_rest_lift \<circ> ignore_failure) mop \<lbrace>\<lambda>_ ms. states_equiv_for P Q R S st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. states_equiv_for P Q R S st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> do mr <- gets machine_state_rest;
p <- select_f (ignore_failure mop mr);
modify (machine_state_rest_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_ ms. states_equiv_for P Q R S st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. states_equiv_for P Q R S st (s\<lparr>machine_state := sa\<rparr>) \<Longrightarrow> \<forall>x\<in>fst (ignore_failure mop (machine_state_rest sa)). states_equiv_for P Q R S st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := snd x\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa b. \<lbrakk>((), b) \<in> fst (ignore_failure mop (machine_state_rest sa)); equiv_for P kheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for P underlying_memory (machine_state st) sa; equiv_for P device_state (machine_state st) sa; equiv_for (P \<circ> fst) cdt st (s\<lparr>machine_state := sa\<rparr>); equiv_for P ekheap st (s\<lparr>machine_state := sa\<rparr>); equiv_for (P \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<rparr>); equiv_for (P \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<rparr>); equiv_for Q interrupt_states st (s\<lparr>machine_state := sa\<rparr>); equiv_for Q interrupt_irq_node st (s\<lparr>machine_state := sa\<rparr>); equiv_for S ready_queues st (s\<lparr>machine_state := sa\<rparr>); \<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> equiv_asid asid st s\<rbrakk> \<Longrightarrow> equiv_for P kheap st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) \<and> equiv_for P underlying_memory (machine_state st) (sa\<lparr>machine_state_rest := b\<rparr>) \<and> equiv_for P device_state (machine_state st) (sa\<lparr>machine_state_rest := b\<rparr>) \<and> equiv_for (P \<circ> fst) cdt st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) \<and> equiv_for P ekheap st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) \<and> equiv_for (P \<circ> fst) cdt_list st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) \<and> equiv_for (P \<circ> fst) is_original_cap st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) \<and> equiv_for Q interrupt_states st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) \<and> equiv_for Q interrupt_irq_node st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) \<and> equiv_for S ready_queues st (s\<lparr>machine_state := sa\<lparr>machine_state_rest := b\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!