theory IpcCancel_C

lemma cbitmap_L2_relation_bit_clear:
  fixes p :: priority
  fixes d :: domain
  shows "\<lbrakk> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>) ;
           d \<le> maxDomain \<rbrakk>
         \<Longrightarrow>
         cbitmap_L2_relation
          (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d)
            (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d])
              (invertL1Index (prioToL1Index p))
              (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] &&
                ~~ 2 ^ unat (p && 0x1F))))
          ((ksReadyQueuesL2Bitmap \<sigma>)
           ((d, invertL1Index (prioToL1Index p)) :=
              ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) &&
                ~~ 2 ^ unat (p && mask wordRadix)))" unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def' apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def
                        invertL1Index_def l2BitmapSize_def'
                        le_maxDomain_eq_less_numDomains word_le_nat_alt) apply (case_tac "da = d" ; clarsimp simp: num_domains_index_updates) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>); d \<le> maxDomain\<rbrakk> \<Longrightarrow> cbitmap_L2_relation (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d) (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d]) (invertL1Index (prioToL1Index p)) (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] && ~~ 2 ^ unat (p && 0x1F)))) ((ksReadyQueuesL2Bitmap \<sigma>)((d, invertL1Index (prioToL1Index p)) := ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d i. (d \<le> maxDomain \<and> i < 8 \<longrightarrow> ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[i] = ksReadyQueuesL2Bitmap \<sigma> (d, i)) \<and> (\<not> (d \<le> maxDomain \<and> i < 8) \<longrightarrow> ksReadyQueuesL2Bitmap \<sigma> (d, i) = 0); d \<le> maxDomain\<rbrakk> \<Longrightarrow> \<forall>da i. (da \<le> maxDomain \<and> i < 8 \<longrightarrow> Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d) (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d]) (invertL1Index (prioToL1Index p)) (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] && ~~ 2 ^ unat (p && 0x1F))).[unat da].[i] = ((ksReadyQueuesL2Bitmap \<sigma>)((d, invertL1Index (prioToL1Index p)) := ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))) (da, i)) \<and> (\<not> (da \<le> maxDomain \<and> i < 8) \<longrightarrow> ((ksReadyQueuesL2Bitmap \<sigma>)((d, invertL1Index (prioToL1Index p)) := ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) && ~~ 2 ^ unat (p && mask wordRadix))) (da, i) = 0) proof (prove)
goal (1 subgoal):
 1. \<And>da i. \<lbrakk>\<forall>d i. (unat d < numDomains \<and> i < 8 \<longrightarrow> ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[i] = ksReadyQueuesL2Bitmap \<sigma> (d, i)) \<and> ((unat d < numDomains \<longrightarrow> \<not> i < 8) \<longrightarrow> ksReadyQueuesL2Bitmap \<sigma> (d, i) = 0); unat d < numDomains\<rbrakk> \<Longrightarrow> (da = d \<and> i = 7 - unat (p >> 5) \<longrightarrow> 7 - unat (p >> 5) < 8 \<longrightarrow> Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d) (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d]) (7 - unat (p >> 5)) (ksReadyQueuesL2Bitmap \<sigma> (d, 7 - unat (p >> 5)) && ~~ 2 ^ unat (p && 0x1F))).[unat d].[7 - unat (p >> 5)] = ksReadyQueuesL2Bitmap \<sigma> (d, 7 - unat (p >> 5)) && ~~ 2 ^ unat (p && 0x1F)) \<and> ((da = d \<longrightarrow> i \<noteq> 7 - unat (p >> 5)) \<longrightarrow> unat da < numDomains \<and> i < 8 \<longrightarrow> Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d) (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d]) (7 - unat (p >> 5)) (ksReadyQueuesL2Bitmap \<sigma> (d, 7 - unat (p >> 5)) && ~~ 2 ^ unat (p && 0x1F))).[unat da].[i] = ksReadyQueuesL2Bitmap \<sigma> (da, i)) proof (prove)
goal:
No subgoals!