theory ArchArch_IF

lemma arm_asid_table_delete_ev2:
  "equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) \<top>\<top>
     (\<lambda>s. rv = arm_asid_table (arch_state s)) (\<lambda>s. rv' = arm_asid_table (arch_state s))
     (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base
                                                                     then None
                                                                     else rv a\<rparr>\<rparr>))
     (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base
                                                                     then None
                                                                     else rv' a\<rparr>\<rparr>))" apply (rule modify_ev2) 
  (* slow 15s *)
   by (auto simp: reads_equiv_def2 affects_equiv_def2
         intro!: states_equiv_forI equiv_forI equiv_asids_arm_asid_table_delete
          elim!: states_equiv_forE equiv_forE
           elim: is_subject_kheap_eq[simplified reads_equiv_def2 states_equiv_for_def, rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (\<lambda>s. rv = asid_table s) (\<lambda>s. rv' = asid_table s) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; rv = asid_table s; rv' = asid_table t\<rbrakk> \<Longrightarrow> True \<and> reads_equiv aag (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; rv = asid_table s; rv' = asid_table t\<rbrakk> \<Longrightarrow> True \<and> reads_equiv aag (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>) (t\<lparr>arch_state := arch_state t\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>)