theory Dpolicy

lemma transform_asid_rev [simp]:
  "asid \<le> 2 ^ ARM_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid" apply (clarsimp simp:transform_asid_def transform_asid_rev_def
                       asid_high_bits_of_def ARM_A.asid_low_bits_def) apply (subgoal_tac "asid >> 10 < 2 ^ asid_high_bits") apply (simp add:ARM_A.asid_high_bits_def ARM_A.asid_bits_def) apply (subst ucast_ucast_len) apply simp apply (subst shiftr_shiftl1) apply simp apply (subst ucast_ucast_mask) apply (simp add:mask_out_sub_mask) apply (simp add:ARM_A.asid_high_bits_def) apply (rule shiftr_less_t2n[where m=7, simplified]) apply (simp add:ARM_A.asid_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid \<le> 2 ^ local.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid proof (prove)
goal (1 subgoal):
 1. asid < 2 ^ local.asid_bits \<Longrightarrow> (UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (asid >> 10)) << 10) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = asid proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid < 2 ^ local.asid_bits; asid >> 10 < 2 ^ local.asid_high_bits\<rbrakk> \<Longrightarrow> (UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (asid >> 10)) << 10) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = asid
 2. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> (UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (asid >> 10)) << 10) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = asid
 2. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> asid >> 10 < 2 ^ LENGTH(7)
 2. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> (asid >> 10 << 10) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = asid
 3. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> (asid >> 10 << 10) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = asid
 2. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> 10 \<le> 10
 2. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> ((asid >> 10 - 10) && ~~ mask 10) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = asid
 3. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> ((asid >> 10 - 10) && ~~ mask 10) + UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = asid
 2. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid < 0x20000; asid >> 10 < 0x80\<rbrakk> \<Longrightarrow> ((asid >> 10 - 10) && ~~ mask 10) + (asid && mask LENGTH(10)) = asid
 2. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 2 ^ local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. asid < 2 ^ local.asid_bits \<Longrightarrow> asid >> 10 < 0x80 proof (prove)
goal (1 subgoal):
 1. asid < 2 ^ local.asid_bits \<Longrightarrow> asid < 2 ^ (10 + 7) proof (prove)
goal:
No subgoals!