theory ArchFinalise_IF

lemma requiv_arm_asid_table_asid_high_bits_of_asid_eq':
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x \<rbrakk>
     \<Longrightarrow> arm_asid_table (arch_state s) (asid_high_bits_of b) =
         arm_asid_table (arch_state t) (asid_high_bits_of b)" apply (subgoal_tac "asid_high_bits_of 0 = asid_high_bits_of 1") apply (case_tac "b = 0") apply (subgoal_tac "is_subject_asid aag 1") apply ((fastforce intro: requiv_arm_asid_table_asid_high_bits_of_asid_eq
                              aag_cap_auth_ASIDPoolCap_asid)+)[2] apply (auto intro: requiv_arm_asid_table_asid_high_bits_of_asid_eq
                      aag_cap_auth_ASIDPoolCap_asid)[1] apply (simp add: asid_high_bits_of_def asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of b) = asid_table t (asid_high_bits_of b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x; asid_high_bits_of 0 = asid_high_bits_of 1\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of b) = asid_table t (asid_high_bits_of b)
 2. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_high_bits_of 0 = asid_high_bits_of 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x; asid_high_bits_of 0 = asid_high_bits_of 1; b = 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of b) = asid_table t (asid_high_bits_of b)
 2. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x; asid_high_bits_of 0 = asid_high_bits_of 1; b \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of b) = asid_table t (asid_high_bits_of b)
 3. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_high_bits_of 0 = asid_high_bits_of 1 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x; asid_high_bits_of 0 = asid_high_bits_of 1; b = 0; is_subject_asid aag 1\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of b) = asid_table t (asid_high_bits_of b)
 2. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x; asid_high_bits_of 0 = asid_high_bits_of 1; b = 0\<rbrakk> \<Longrightarrow> is_subject_asid aag 1
 3. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x; asid_high_bits_of 0 = asid_high_bits_of 1; b \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of b) = asid_table t (asid_high_bits_of b)
 4. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_high_bits_of 0 = asid_high_bits_of 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x; asid_high_bits_of 0 = asid_high_bits_of 1; b \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of b) = asid_table t (asid_high_bits_of b)
 2. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_high_bits_of 0 = asid_high_bits_of 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap p b)); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_high_bits_of 0 = asid_high_bits_of 1 proof (prove)
goal:
No subgoals!