theory ArchArch_IF

lemma requiv_arm_asid_table_asid_high_bits_of_asid_eq':
  "\<lbrakk> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base
              \<longrightarrow> is_subject_asid aag asid'); reads_equiv aag s t \<rbrakk>
     \<Longrightarrow> arm_asid_table (arch_state s) (asid_high_bits_of base) =
         arm_asid_table (arch_state t) (asid_high_bits_of base)" apply (insert asid_high_bits_0_eq_1) apply (case_tac "base = 0") apply (subgoal_tac "is_subject_asid aag 1") apply simp apply (rule requiv_arm_asid_table_asid_high_bits_of_asid_eq[where aag=aag]) apply (erule_tac x=1 in allE) apply simp+ apply (rule requiv_arm_asid_table_asid_high_bits_of_asid_eq[where aag=aag]) apply (erule_tac x=base in allE) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base)
 2. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0; is_subject_asid aag 1\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base)
 2. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> is_subject_asid aag 1
 3. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of 1 \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of 1) = asid_table t (asid_high_bits_of 1)
 2. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> is_subject_asid aag 1
 3. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of 1 \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> is_subject_asid aag 1
 2. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of 1 \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> reads_equiv aag s t
 3. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of 1 \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> 1 \<noteq> 0
 4. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> is_subject_asid aag 1
 5. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0; 1 \<noteq> 0 \<and> asid_high_bits_of 1 = asid_high_bits_of 1 \<longrightarrow> is_subject_asid aag 1\<rbrakk> \<Longrightarrow> is_subject_asid aag 1
 2. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of 1 \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> reads_equiv aag s t
 3. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of 1 \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> 1 \<noteq> 0
 4. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base = 0\<rbrakk> \<Longrightarrow> is_subject_asid aag 1
 5. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of base) = asid_table t (asid_high_bits_of base) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> is_subject_asid aag base
 2. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> reads_equiv aag s t
 3. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> base \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0; base \<noteq> 0 \<and> asid_high_bits_of base = asid_high_bits_of base \<longrightarrow> is_subject_asid aag base\<rbrakk> \<Longrightarrow> is_subject_asid aag base
 2. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> reads_equiv aag s t
 3. \<lbrakk>\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid'; reads_equiv aag s t; asid_high_bits_of 0 = asid_high_bits_of 1; base \<noteq> 0\<rbrakk> \<Longrightarrow> base \<noteq> 0 proof (prove)
goal:
No subgoals!