Theory invariant

(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn)
School of Computer Science & Engineering, Beihang University, China
*)

theory invariant
imports mem_spec "HOL-Eisbach.Eisbach_Tools" (*"~~/src/HOL/Word/Word"*)
begin

text‹
this theory defines the invariant and its lemmas.
›

section ‹invariants›

subsection ‹defs of invariants›
text‹
we consider multi-threaded execution on mono-core.
A thread is the currently executing thread iff it is in RUNNING state.
›
definition inv_cur :: "State ⇒ bool"
where "inv_cur s ≡ ∀t. cur s = Some t ⟷ thd_state s t = RUNNING"

(******************************
Function dist_list is only used on ``inv_thd_waitq'', which could be replaced by distinct of List.
have proved many things, so now just leave it here.
later lets do replacement!
********************************)
abbreviation dist_list :: "'a list ⇒ bool"
where "dist_list l ≡ ∀i j. i < length l ∧ j < length l ∧ i ≠ j ⟶ l!i ≠ l!j"

text‹
the relation of thread state and wait queue.
here we dont consider other modules of zephyr, so blocked thread is in wait que of mem pools.
›
definition inv_thd_waitq :: "State ⇒ bool"
where "inv_thd_waitq s ≡
  (∀p∈mem_pools s. ∀t∈ set (wait_q (mem_pool_info s p)). thd_state s t = BLOCKED)
  ⌦‹(* thread in waitq is BLOCKED *)›
 ∧ (∀t. thd_state s t = BLOCKED ⟶ (∃p∈mem_pools s. t ∈ set (wait_q (mem_pool_info s p))))
    ⌦‹(* BLOCKED thread is in a waitq *)›
 ∧ (∀p∈mem_pools s. dist_list (wait_q (mem_pool_info s p)))
    ⌦‹(* threads in a waitq are different with each other, which means a thread could not waiting for the same pool two times *)›
 ∧ (∀p q. p∈mem_pools s ∧ q∈mem_pools s ∧ p ≠ q ⟶ (∄t. t ∈ set (wait_q (mem_pool_info s p))
                                                  ∧ t∈ set (wait_q (mem_pool_info s q))))"
    (* threads of two waitqs are different, which means a thread could not waiting for two pools *)

text‹
invariant of configuration of memory pools.
its actually a well-formed property for memory configuration.
(1) the max size (the size of top-level (level 0) block) is $4 ^ {n\_levels}$ times of block size of the lowest level.
4 * n means that the block size of the lowest level is alignd with 4.
(2) the block number at level 0 (n\_max) > 0, and the max number of levels is n\_levels > 0
(3) n\_level is equal to the length of levels list.
(4) the length of bitmap list at each level is equal to the block number at the same level.
Thus, bitmap saves a complete quad-tree with height of n\_levels.
A real memory pool is a top subtree of the complete tree.
bits of subnodes of a leaf node (ALLOCATED, FREE, ALLOCATING, FREEING) is NOEXIST.
›
abbreviation inv_mempool_info_mp :: "State ⇒ mempool_ref ⇒ bool"
where "inv_mempool_info_mp s p ≡
   let mp = mem_pool_info s p in
       buf mp ≠ NULL ∧ (∃n>0. max_sz mp = (4 * n) * (4 ^ n_levels mp))
      ∧ n_max mp > 0 ∧ n_levels mp > 0
      ∧ n_levels mp = length (levels mp)
      ∧ (∀i<length (levels mp). length (bits (levels mp ! i)) = (n_max mp) * 4 ^ i)"
      (* length of bits list in each level = the blocks in each level *)

definition inv_mempool_info :: "State ⇒ bool"
where "inv_mempool_info s ≡ ∀p∈mem_pools s. inv_mempool_info_mp s p"

lemma inv_max_sz_gt0: "inv_mempool_info s ⟹ ∀p∈mem_pools s. let mp = mem_pool_info s p in max_sz mp > 0"
  unfolding inv_mempool_info_def using neq0_conv by fastforce

text ‹
invariant between bitmap and free block list at each level.
(1) bit of a block is FREE, iff its start address is in free list.
the start address is buf mp + j * (max\_sz mp div ($4 ^ i$)), the start address of the mempool + block size at this level * block index
(2) start address of blocks in free list is valid,
i.e. it is the start address of some block (index n), where n is in the range of block index at the level
(3) start address of blocks in free list are different with each other.
›
(* invariant between bitmap and free_list *)
abbreviation inv_bitmap_freelist_mp :: "State ⇒ mempool_ref ⇒ bool"
where "inv_bitmap_freelist_mp s p ≡
          let mp = mem_pool_info s p in
            ∀i < length (levels mp).
              let bts = bits (levels mp ! i);
                  fl = free_list (levels mp ! i) in
              (∀j < length bts. bts ! j = FREE ⟷ buf mp + j * (max_sz mp div (4 ^ i)) ∈ set fl)
              ⌦‹(* the block corresponding to a free bit iff it is in freelist *)›
              ∧ (∀j < length fl. (∃n. n < n_max mp * (4 ^ i) ∧ fl ! j = buf mp + n * (max_sz mp div (4 ^ i))))
              ⌦‹(* pointers in freelist are head address of blocks *)›
              ∧ distinct fl ⌦‹(*(∀k j. k < length fl ∧ j < length fl ⟶ fl!k = fl!j ⟶ k = j) *)›
              ⌦‹(* pointers in freelist are different with each other *)›"

definition inv_bitmap_freelist :: "State ⇒ bool"
where "inv_bitmap_freelist s ≡
        ∀p∈mem_pools s. inv_bitmap_freelist_mp s p"

text‹
this invariant represents that a memory pools is forest of valid quad-trees of blocks.
parent node of a leaf node (ALLOCATED, FREE, ALLOCATING, FREEING) is an inner node (DIVIDED).
parent node of an inner node (DIVIDED) is also a DIVIDED node.
child nodes of a NOEXIST node is also NOEXIST nodes.
parent node of a NOEXIST node should not be DIVIDE nodes (may be NOEXIST, ALLOCATED, FREE, ALLOCATING, FREEING)
›
(* invariant that bits is a valid tree *)
abbreviation inv_bitmap_mp :: "State ⇒ mempool_ref ⇒ bool"
where "inv_bitmap_mp s p ≡
          let mp = mem_pool_info s p in
            ∀i < length (levels mp).
              let bts = bits (levels mp ! i) in
              (∀j < length bts.
                  (bts ! j = FREE ∨ bts ! j = FREEING ∨ bts ! j = ALLOCATED ∨ bts ! j = ALLOCATING ⟶
                        (i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED)
                        ∧ (i < length (levels mp) - 1 ⟶ noexist_bits mp (i+1) (j*4) ))
                ∧ (bts ! j = DIVIDED ⟶ i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED)
                ∧ (bts ! j = NOEXIST ⟶ i < length (levels mp) - 1
                      ⟶ noexist_bits mp (i+1) (j*4))
                ∧ (bts ! j = NOEXIST ∧ i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) ≠ DIVIDED) )"

definition inv_bitmap :: "State ⇒ bool"
where "inv_bitmap s ≡
        ∀p∈mem_pools s. inv_bitmap_mp s p"

text‹
due to the rule of merge as possible, there should not exist a node with 4 FREE child blocks.
In free syscall, 4 free child blocks should be merged to a bigger block.
›
abbreviation inv_bitmap_not4free_mp :: "State ⇒ mempool_ref ⇒ bool"
where "inv_bitmap_not4free_mp s p ≡
          let mp = mem_pool_info s p in
            ∀i < length (levels mp).
              let bts = bits (levels mp ! i) in
              (∀j < length bts. i > 0 ⟶ ¬ partner_bits mp i j) "  (* there is not 4 free blocks. level 0 is allowed *)

definition inv_bitmap_not4free :: "State ⇒ bool"
where "inv_bitmap_not4free s ≡
        ∀p∈mem_pools s. inv_bitmap_not4free_mp s p"

text‹
blocks at level 0 should not be NOEXIST. If so, the memory pool does not exist.
We only allow real memory pools.

›
definition inv_bitmap0 :: "State ⇒ bool"
where "inv_bitmap0 s ≡
  ∀p∈mem_pools s. let bits0 = bits (levels (mem_pool_info s p) ! 0) in ∀i<length bits0. bits0 ! i ≠ NOEXIST"

text‹
blocks at last level (n\_level - 1) should not be split again, thus should not be DIVIDED
›
definition inv_bitmapn :: "State ⇒ bool"
where "inv_bitmapn s ≡
  ∀p∈mem_pools s. let bitsn = bits ((levels (mem_pool_info s p) ! (length (levels (mem_pool_info s p)) - 1)))
                  in ∀i<length bitsn. bitsn ! i ≠ DIVIDED"

definition mem_block_addr_valid :: "State ⇒ Mem_block ⇒ bool"
where "mem_block_addr_valid s b ≡
        data b = buf (mem_pool_info s (pool b)) + (block b) * ((max_sz (mem_pool_info s (pool b))) div (4 ^ (level b)))"

text‹
invariants between FREEING/ALLOCATING blocks and freeing/allocating\_node variables.
›
definition inv_aux_vars :: "State ⇒ bool"
where "inv_aux_vars s ≡
        (∀t n. freeing_node s t = Some n ⟶ get_bit (mem_pool_info s) (pool n) (level n) (block n) = FREEING)
        ⌦‹(* freeing node is state of FREEING *)›
      ∧ (∀n. get_bit (mem_pool_info s) (pool n) (level n) (block n) = FREEING ∧ mem_block_addr_valid s n
                ⟶ (∃t. freeing_node s t = Some n))
        ⌦‹(* node of state of FREEING is freeing *)›
      ∧ (∀t n. allocating_node s t = Some n ⟶ get_bit (mem_pool_info s) (pool n) (level n) (block n) = ALLOCATING)
        ⌦‹(* freeing node is state of FREEING *)›
      ∧ (∀n. get_bit (mem_pool_info s) (pool n) (level n) (block n) = ALLOCATING ∧ mem_block_addr_valid s n
                ⟶ (∃t. allocating_node s t = Some n))
        ⌦‹(* node of state of FREEING is freeing *)›
      ∧ (∀t1 t2 n1 n2. t1 ≠ t2 ∧ freeing_node s t1 = Some n1 ∧ freeing_node s t2 = Some n2
                        ⟶ ¬(pool n1 = pool n2 ∧ level n1 = level n2 ∧ block n1 = block n2))
        ⌦‹(*here we only consider the pool, level, and block, not the first addr of the block *)›
        ⌦‹(* freeing nodes are different each other *)›
      ∧ (∀t1 t2 n1 n2. t1 ≠ t2 ∧ allocating_node s t1 = Some n1 ∧ allocating_node s t2 = Some n2
                        ⟶ ¬(pool n1 = pool n2 ∧ level n1 = level n2 ∧ block n1 = block n2))
        ⌦‹(* allocating node are different each other *)›
      ∧ (∀t1 t2 n1 n2. allocating_node s t1 = Some n1 ∧ freeing_node s t2 = Some n2
                        ⟶ ¬(pool n1 = pool n2 ∧ level n1 = level n2 ∧ block n1 = block n2))"
        (* allocating and freeing nodes are different each other *)

definition inv :: "State ⇒ bool"
where "inv s ≡ inv_cur s ∧ inv_thd_waitq s ∧ inv_mempool_info s
              ∧ inv_bitmap_freelist s ∧ inv_bitmap s ∧ inv_aux_vars s
              ∧ inv_bitmap0 s ∧ inv_bitmapn s ∧ inv_bitmap_not4free s"

(*declare inv_def[simp] and inv_bitmap_def[simp] and inv_bitmap_freelist_def[simp]
        and inv_mempool_info_def[simp] and inv_thd_waitq_def[simp] and inv_cur_def[simp]*)
method simp_inv = (simp add:inv_def inv_bitmap_def inv_bitmap_freelist_def
                    inv_mempool_info_def inv_thd_waitq_def inv_cur_def inv_aux_vars_def
                    inv_bitmap0_def inv_bitmapn_def
                    inv_bitmap_not4free_def mem_block_addr_valid_def)

method unfold_inv = (unfold inv_def inv_bitmap_def inv_bitmap_freelist_def
                    inv_mempool_info_def inv_thd_waitq_def inv_cur_def inv_aux_vars_def
                    inv_bitmap0_def inv_bitmapn_def
                    inv_bitmap_not4free_def mem_block_addr_valid_def)[1]

lemma inv_imp_fl_lt0:
  "inv Va ⟹
    ∀p∈mem_pools Va.
          let mp = mem_pool_info Va p in
            ∀i < length (levels mp).
              ∀j < length (free_list (levels mp ! i)). free_list (levels mp ! i) ! j > 0"
  apply(simp add:inv_def inv_mempool_info_def inv_bitmap_freelist_def)
  apply(simp add:Let_def) apply clarsimp
  by fastforce

subsection ‹initial state $s_0$›

text‹
we dont consider mem\_pool\_init, only define $s0$ to show the state after memory pool initialization.
›
axiomatization s0::State where
  s0a1: "cur s0 = None" and
  s0a2: "tick s0 = 0" and
  s0a3: "thd_state s0 = (λt. READY)" and
  s0a5: "mem_pools s0 ≠ {}" and
  s0a7: "∀p∈mem_pools s0. wait_q (mem_pool_info s0 p) = []" and
  s0a6: "∀p∈mem_pools s0. let mp = mem_pool_info s0 p in
                         buf mp > 0 ∧ (∃n>0. max_sz mp = (4 * n) * (4 ^ n_levels mp))
                        ∧ n_max mp > 0 ∧ n_levels mp > 1
                        ∧ n_levels mp = length (levels mp)" and
  s0a8: "∀p∈mem_pools s0. ⌦‹(* defines level 1 to n *)›
          let mp = mem_pool_info s0 p in
            ∀i. i > 0 ∧ i < length (levels mp) ⟶
                   length (bits (levels mp ! i)) = n_max mp * 4 ^ i
                  ∧ (∀j<length (bits (levels mp ! i)). bits (levels mp ! i) ! j = NOEXIST)
                  ∧ free_list (levels mp ! i) = []" and
  s0a9: "∀p∈mem_pools s0. ⌦‹(* defines the level0 *)›
          let mp = mem_pool_info s0 p;
              lv0 = (levels mp)!0 in
            length (bits lv0) = n_max mp
           ∧ length (free_list lv0) = n_max mp
           ∧ (∀i<length (bits lv0). (bits lv0)!i = FREE)
           ∧ (∀i<length (free_list lv0). (free_list lv0) ! i = (buf mp) + i * max_sz mp)
           ∧ distinct (free_list lv0)" and
  s0a4: "freeing_node s0 = Map.empty" and
  s0a10: "allocating_node s0 = Map.empty" and
  s0a11: "∄n. get_bit_s s0 (pool n) (level n) (block n) = FREEING" and
  s0a12: "∄n. get_bit_s s0 (pool n) (level n) (block n) = ALLOCATING"


lemma s0_max_sz_gt0: "∀p∈mem_pools s0. let mp = mem_pool_info s0 p in max_sz mp > 0"
  using s0a6 zero_less_power by fastforce

lemma s0_inv_cur: "inv_cur s0"
  by (simp add:inv_cur_def s0a1 s0a3)

lemma s0_inv_thdwaitq: "inv_thd_waitq s0"
  by (simp add: inv_thd_waitq_def s0a7 s0a3)

lemma s0_inv_mempool_info: "inv_mempool_info s0"
  apply (simp add: inv_mempool_info_def Let_def) apply clarsimp
  apply(rule conjI) apply (metis neq0_conv s0a6)
  apply(rule conjI) apply (meson s0a6)
  apply(rule conjI) apply (meson s0a6)
  apply(rule conjI) using neq0_conv s0a6 apply fastforce
  apply(rule conjI) apply (meson s0a6)
  by (metis One_nat_def mult_numeral_1_right neq0_conv numeral_1_eq_Suc_0 power.simps(1) s0a8 s0a9)

lemma s0_inv_bitmap_freelist: "inv_bitmap_freelist s0"
  apply(simp add:inv_bitmap_freelist_def)
  apply(simp add: Let_def) apply clarsimp
    apply(case_tac "i = 0")
    apply(rule conjI) apply clarsimp apply (metis nth_mem s0a9)
    apply(rule conjI) apply clarsimp apply (metis s0a9)
    apply (meson s0a9)

    apply(rule conjI) apply clarsimp
      apply(subgoal_tac "n_levels (mem_pool_info s0 p) = length (levels (mem_pool_info s0 p))")
        prefer 2 apply (meson s0a6)
      apply(subgoal_tac "get_bit_s s0 p i j ≠ FREE")
        prefer 2 apply (metis BlockState.distinct(13) s0a8)
      apply(subgoal_tac "set (free_list (levels (mem_pool_info s0 p) ! i)) = {}")
        prefer 2 apply (metis all_not_in_conv in_set_conv_nth length_greater_0_conv neq0_conv not_less_zero s0a8)
      apply simp

    apply(rule conjI) apply clarsimp
      apply (metis length_greater_0_conv neq0_conv not_less_zero s0a8)
    apply (metis distinct_conv_nth length_0_conv neq0_conv not_less_zero s0a8)
done

lemma s0_inv_bitmap: "inv_bitmap s0"
  apply(simp add: inv_bitmap_def)
  apply(simp add: Let_def) apply clarsimp
    apply(case_tac "i = 0")
      apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def partner_bits_def)

      apply(rule conjI) apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def)
      apply(rule conjI) apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def)
      apply(rule conjI) apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def)
      apply(rule conjI) apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def)
      apply(rule conjI) apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def)
      apply(rule conjI) apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def)

        apply(case_tac "i = 1") apply clarsimp using s0a6 s0a8 s0a9 apply(simp add:Let_def)
          apply(subgoal_tac "i > 1") prefer 2 apply simp
          apply(subgoal_tac "get_bit_s s0 p (i - Suc NULL) (j div 4) = NOEXIST")
            prefer 2 using s0a8 apply(simp add: Let_def)
            apply(subgoal_tac "j div 4 < length (bits (levels (mem_pool_info s0 p) ! (i - 1)))")
              prefer 2 using s0a6 apply(simp add:Let_def)
                apply(subgoal_tac "n_max (mem_pool_info s0 p) > 0")
                  prefer 2 using s0a6 apply(simp add:Let_def)
                apply(simp add: power_eq_if)
            apply auto[1]
          apply simp

done

lemma s0_inv_bitmap_not4free: "inv_bitmap_not4free s0"
  apply(simp add: inv_bitmap_not4free_def)
  apply(simp add: Let_def) apply clarsimp
  using s0a6 s0a8 s0a9 apply(simp add:Let_def partner_bits_def)
done

lemma s0_inv_aux_vars: "inv_aux_vars s0"
  apply(simp add: inv_aux_vars_def Let_def)
  apply(rule conjI) apply (simp add: s0a4)
  apply(rule conjI) apply clarify using s0a11 apply auto[1]
  apply(rule conjI) apply (simp add: s0a10)
  apply(rule conjI) apply clarify using s0a12 apply auto[1]
  apply(rule conjI) apply (simp add: s0a4)
  apply(rule conjI) apply (simp add: s0a10)
  apply (simp add: s0a4 s0a10)
done

lemma s0_inv_bitmap_freelist0: "inv_bitmap0 s0"
  apply(simp add: inv_bitmap0_def Let_def)
  using s0a9 apply(simp add:Let_def)
done

lemma s0_inv_bitmap_freelistn: "inv_bitmapn s0"
  apply(simp add: inv_bitmapn_def Let_def)
  using s0a8 apply(simp add:Let_def) apply clarify
  apply(subgoal_tac "get_bit_s s0 p (length (levels (mem_pool_info s0 p)) - Suc 0) i = NOEXIST")
    prefer 2 apply(subgoal_tac "length (levels (mem_pool_info s0 p)) > 0")
               prefer 2 using s0a6 apply(simp add:Let_def) apply auto[1]
    using s0a6 apply(simp add:Let_def) apply auto[1]
 apply simp
done

lemma s0_inv: "inv s0"
  apply(unfold inv_def)
  apply(rule conjI) using s0_inv_cur apply fast
  apply(rule conjI) using s0_inv_thdwaitq apply fast
  apply(rule conjI) using s0_inv_mempool_info apply fast
  apply(rule conjI) using s0_inv_bitmap_freelist apply fast
  apply(rule conjI) using s0_inv_bitmap apply fast
  apply(rule conjI) using s0_inv_aux_vars apply fast
  apply(rule conjI) using s0_inv_bitmap_freelist0 apply fast
  apply(rule conjI) using s0_inv_bitmap_freelistn apply fast
  using s0_inv_bitmap_not4free apply fast
done

subsection ‹lemmas of invariants›

lemma inv_bitmap_presv_setbit_0:
"¬ (x = l ∧ y = b) ⟹
      Vb = Va⦇mem_pool_info := (mem_pool_info Va)
                (p := mem_pool_info Va p
                   ⦇levels := (levels (mem_pool_info Va p))
                      [l := (levels (mem_pool_info Va p) ! l)⦇bits := (bits (levels (mem_pool_info Va p) ! l))[b := st]⦈]⦈)⦈ ⟹
      get_bit_s Va p x y= get_bit_s Vb p x y"
apply simp by (metis (no_types, lifting) Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4)
                Mem_pool_lvl.surjective list_update_beyond not_less nth_list_update_eq nth_list_update_neq)

lemma inv_bitmap_presv_setbit:
"inv_bitmap Va ⟹
  get_bit_s Va p l b = FREE ∨ get_bit_s Va p l b = FREEING ∨ get_bit_s Va p l b = ALLOCATED
     ∨ get_bit_s Va p l b = ALLOCATING ⟹
  st = FREE ∨ st = FREEING ∨ st = ALLOCATED ∨ st = ALLOCATING ⟹
  Vb = set_bit_s Va p l b st ⟹
  inv_bitmap Vb"
apply(simp add:inv_bitmap_def) apply(simp add:set_bit_s_def set_bit_def)

apply(simp add:Let_def) apply clarify apply(rename_tac ii jj)
apply(subgoal_tac "p∈mem_pools Va") prefer 2 apply(simp add:set_bit_s_def set_bit_def)
apply(subgoal_tac "jj < length (bits (levels (mem_pool_info Va p) ! ii))")
  prefer 2 apply(simp add:set_bit_s_def set_bit_def)
  apply (metis (no_types, lifting) Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4)
    Mem_pool_lvl.surjective list_updt_samelen nth_list_update_eq nth_list_update_neq)

(* (bts ! j = FREE ∨ bts ! j = FREEING ∨ bts ! j = ALLOCATED ∨ bts ! j = ALLOCATING ⟶
      (i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED)
      ∧ (i < length (levels mp) - 1 ⟶ (bits (levels mp ! (i + 1))) ! (j * 4) = NOEXIST
                                      ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 1) = NOEXIST
                                      ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 2) = NOEXIST
                                      ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 3) = NOEXIST) )*)
(* FREE ⟶  **************************************************************** *)
apply(rule conjI) apply clarify apply(rule conjI) apply clarify
(* (i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4) = DIVIDED")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    One_nat_def nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4)
                      = (bits (levels (mem_pool_info Vb p) ! (ii - 1))) ! (jj div 4)")
  prefer 2 apply(case_tac "ii - 1 = l ∧ jj div 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply clarify apply(rule conjI)
(* (i < length (levels mp) - 1 ⟶ (bits (levels mp ! (i + 1))) ! (j * 4) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 1) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 2) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 3) = NOEXIST) ) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                      nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
      Nat.add_0_right One_nat_def add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 1)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 1 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 2)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 2 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 3)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 3 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

(* FREEING ⟶  **************************************************************** *)
apply(rule conjI) apply clarify apply(rule conjI) apply clarify
(* (i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4) = DIVIDED")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    One_nat_def nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4)
                      = (bits (levels (mem_pool_info Vb p) ! (ii - 1))) ! (jj div 4)")
  prefer 2 apply(case_tac "ii - 1 = l ∧ jj div 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply clarify apply(rule conjI)
(* (i < length (levels mp) - 1 ⟶ (bits (levels mp ! (i + 1))) ! (j * 4) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 1) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 2) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 3) = NOEXIST) ) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                        nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
      Nat.add_0_right One_nat_def add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 1)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 1 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 2)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 2 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 3)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 3 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

(* ALLOCATED ⟶  **************************************************************** *)
apply(rule conjI) apply clarify apply(rule conjI) apply clarify
(* (i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4) = DIVIDED")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    One_nat_def nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4)
                      = (bits (levels (mem_pool_info Vb p) ! (ii - 1))) ! (jj div 4)")
  prefer 2 apply(case_tac "ii - 1 = l ∧ jj div 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply clarify apply(rule conjI)
(* (i < length (levels mp) - 1 ⟶ (bits (levels mp ! (i + 1))) ! (j * 4) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 1) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 2) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 3) = NOEXIST) ) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                        nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
      Nat.add_0_right One_nat_def add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 1)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 1 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 2)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 2 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 3)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 3 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

(* ALLOCATING ⟶  **************************************************************** *)
apply(rule conjI) apply clarify apply(rule conjI) apply clarify
(* (i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4) = DIVIDED")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    One_nat_def nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4)
                      = (bits (levels (mem_pool_info Vb p) ! (ii - 1))) ! (jj div 4)")
  prefer 2 apply(case_tac "ii - 1 = l ∧ jj div 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply clarify apply(rule conjI)
(* (i < length (levels mp) - 1 ⟶ (bits (levels mp ! (i + 1))) ! (j * 4) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 1) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 2) = NOEXIST
                                  ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 3) = NOEXIST) ) *)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
      Nat.add_0_right One_nat_def add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 1)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 1)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 1 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 2)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 2)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 2 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp

apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3) = NOEXIST")
  prefer 2
  apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
          add_2_eq_Suc' nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! Suc ii)) ! (jj * 4 + 3)
                      = (bits (levels (mem_pool_info Vb p) ! Suc ii)) ! (jj * 4 + 3)")
  prefer 2 apply(case_tac "Suc ii = l ∧ jj * 4 + 3 = b") apply simp using inv_bitmap_presv_setbit_0 apply metis
apply simp


apply(rule conjI)
(* (bts ! j = DIVIDED ⟶ i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) = DIVIDED) *)
apply clarify
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4) = DIVIDED")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    One_nat_def nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4)
                      = (bits (levels (mem_pool_info Vb p) ! (ii - 1))) ! (jj div 4)")
  prefer 2 apply(case_tac "ii - 1 = l ∧ jj div 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(rule conjI)
(* (bts ! j = NOEXIST ⟶ i < length (levels mp) - 1
      ⟶ (bits (levels mp ! (i + 1))) ! (j * 4) = NOEXIST
          ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 1) = NOEXIST
          ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 2) = NOEXIST
          ∧ (bits (levels mp ! (i + 1))) ! (j * 4 + 3) = NOEXIST) *)
apply clarify
apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    Nat.add_0_right One_nat_def add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4)
                      = (bits (levels (mem_pool_info Vb p) ! (ii + 1))) ! (jj * 4)")
  prefer 2 apply(case_tac "ii + 1 = l ∧ jj * 4 = b") apply simp using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4 + 1) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    Nat.add_0_right One_nat_def add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4 + 1)
                      = (bits (levels (mem_pool_info Vb p) ! (ii + 1))) ! (jj * 4 + 1)")
  prefer 2 apply(case_tac "ii + 1 = l ∧ jj * 4 + 1 = b") apply auto[1] using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(rule conjI)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4 + 2) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                  Nat.add_0_right One_nat_def add_2_eq_Suc' add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4 + 2)
                      = (bits (levels (mem_pool_info Vb p) ! (ii + 1))) ! (jj * 4 + 2)")
  prefer 2 apply(case_tac "ii + 1 = l ∧ jj * 4 + 2 = b") apply auto[1] using inv_bitmap_presv_setbit_0 apply simp
apply simp

apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4 + 3) = NOEXIST")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                  Nat.add_0_right One_nat_def add_2_eq_Suc' add_Suc_right nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii + 1))) ! (jj * 4 + 3)
                      = (bits (levels (mem_pool_info Vb p) ! (ii + 1))) ! (jj * 4 + 3)")
  prefer 2 apply(case_tac "ii + 1 = l ∧ jj * 4 + 3 = b") apply auto[1] using inv_bitmap_presv_setbit_0 apply simp
apply simp

(* (bts ! j = NOEXIST ∧ i > 0 ⟶ (bits (levels mp ! (i - 1))) ! (j div 4) ≠ DIVIDED) *)
apply clarify
(* apply(subgoal_tac "¬(ii = l ∧ jj = b)") prefer 2 apply clarsimp *)
apply(subgoal_tac "bits (levels (mem_pool_info Va p) ! ii) ! jj = NOEXIST")
  prefer 2 apply(case_tac "ii = l ∧ jj = b") apply auto[1] using inv_bitmap_presv_setbit_0 apply simp
apply(subgoal_tac "bits (levels (mem_pool_info Va p) ! (ii - 1)) ! (jj div 4) ≠ DIVIDED")
  prefer 2 apply (smt Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4) Mem_pool_lvl.surjective
                    One_nat_def nth_list_update_eq nth_list_update_neq)
apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - 1))) ! (jj div 4)
                      = (bits ((levels (mem_pool_info Va p))
                   [l := (levels (mem_pool_info Va p) ! l)⦇bits := (bits (levels (mem_pool_info Va p) ! l))[b := st]⦈] !
                   (ii - 1))) ! (jj div 4)") prefer 2
  apply(case_tac "ii - 1 = l ∧ jj div 4 = b") apply clarsimp
    apply(subgoal_tac "(bits (levels (mem_pool_info Va p) ! (ii - Suc NULL)))[jj div 4 := st] ! (jj div 4) = st")
      prefer 2 apply (metis list_update_beyond not_less nth_list_update_eq)
    apply simp
  using inv_bitmap_presv_setbit_0 apply simp
apply clarsimp

done


lemma inv_bitmap_freelist_fl_bnum_in:
"inv_bitmap_freelist Va ⟹
  inv_mempool_info Va ⟹
  p∈mem_pools Va ⟹
  ii < length (levels (mem_pool_info Va p)) ⟹
  jj < length (free_list ((levels (mem_pool_info Va p)) ! ii)) ⟹
  block_num (mem_pool_info Va p)
             ((free_list ((levels (mem_pool_info Va p)) ! ii)) ! jj)
             (max_sz (mem_pool_info Va p) div 4 ^ ii) < length (bits (levels (mem_pool_info Va p) ! ii))"
apply(simp add:inv_bitmap_freelist_def inv_mempool_info_def block_num_def Let_def)
apply(subgoal_tac "∃n. n < n_max (mem_pool_info Va p) * (4 ^ ii) ∧ free_list (levels (mem_pool_info Va p) ! ii) ! jj
        = buf (mem_pool_info Va p) + n * (max_sz (mem_pool_info Va p) div 4 ^ ii)")
  prefer 2 apply blast
apply(subgoal_tac "free_list (levels (mem_pool_info Va p) ! ii) ! jj ≥ buf (mem_pool_info Va p)")
  prefer 2 apply linarith
  using nonzero_mult_div_cancel_right by force

lemma inv_bitmap_freelist_fl_FREE:
"inv_bitmap_freelist Va ⟹
  inv_mempool_info Va ⟹
  p∈mem_pools Va ⟹
  ii < length (levels (mem_pool_info Va p)) ⟹
  jj < length (free_list ((levels (mem_pool_info Va p)) ! ii)) ⟹
  get_bit_s Va p ii (block_num (mem_pool_info Va p)
                               ((free_list ((levels (mem_pool_info Va p)) ! ii)) ! jj)
                               (max_sz (mem_pool_info Va p) div 4 ^ ii)) = FREE"
apply(simp add:inv_bitmap_freelist_def inv_mempool_info_def block_num_def Let_def)
apply(subgoal_tac "∃n. n < n_max (mem_pool_info Va p) * (4 ^ ii) ∧ free_list (levels (mem_pool_info Va p) ! ii) ! jj
        = buf (mem_pool_info Va p) + n * (max_sz (mem_pool_info Va p) div 4 ^ ii)")
  prefer 2 apply blast
  by (metis add_diff_cancel_left' div_0 mult_0_right neq0_conv nonzero_mult_div_cancel_right not_less_zero nth_mem)


lemma inv_buf_le_fl:
"inv_bitmap_freelist Va ⟹
  inv_mempool_info Va ⟹
  p∈mem_pools Va ⟹
  ii < length (levels (mem_pool_info Va p)) ⟹
  jj < length (free_list ((levels (mem_pool_info Va p)) ! ii)) ⟹
  buf (mem_pool_info Va p) ≤ (free_list ((levels (mem_pool_info Va p)) ! ii)) ! jj"
apply(simp add:inv_bitmap_freelist_def inv_mempool_info_def Let_def)
apply(subgoal_tac "∃n. free_list (levels (mem_pool_info Va p) ! ii) ! jj
        = buf (mem_pool_info Va p) + n * (max_sz (mem_pool_info Va p) div 4 ^ ii)")
  prefer 2 apply blast
by linarith

lemma inv_fl_mod_sz0:
"inv_bitmap_freelist Va ⟹
  inv_mempool_info Va ⟹
  p∈mem_pools Va ⟹
  ii < length (levels (mem_pool_info Va p)) ⟹
  jj < length (free_list ((levels (mem_pool_info Va p)) ! ii)) ⟹
  ((free_list ((levels (mem_pool_info Va p)) ! ii)) ! jj - buf (mem_pool_info Va p)) mod
         (max_sz (mem_pool_info Va p) div 4 ^ ii) = 0"
apply(simp add:inv_bitmap_freelist_def inv_mempool_info_def Let_def)
apply(subgoal_tac "∃n. free_list (levels (mem_pool_info Va p) ! ii) ! jj
        = buf (mem_pool_info Va p) + n * (max_sz (mem_pool_info Va p) div 4 ^ ii)")
  prefer 2 apply blast
by force


lemma sameinfo_inv_bitmap_mp:
"mem_pool_info Va p = mem_pool_info Vb p ⟹ inv_bitmap_mp Va p = inv_bitmap_mp Vb p"
apply(simp add: Let_def)
done

lemma sameinfo_inv_bitmap_freelist_mp:
"mem_pool_info Va p = mem_pool_info Vb p ⟹ inv_bitmap_freelist_mp Va p = inv_bitmap_freelist_mp Vb p"
apply(simp add: Let_def)
done


lemma inv_bitmap_presv_mpls_mpi:
  "mem_pools Va = mem_pools Vb ⟹
   mem_pool_info Va = mem_pool_info Vb ⟹
   inv_bitmap Va ⟹
   inv_bitmap Vb"
by(simp add:inv_bitmap_def Let_def)

lemma inv_bitmap_presv_mpls_mpi2:
  "mem_pools Va = mem_pools Vb ⟹
   (∀p. length (levels (mem_pool_info Va p)) = length (levels (mem_pool_info Vb p))) ⟹
   (∀p ii. ii < length (levels (mem_pool_info Va p))
        ⟶ bits (levels (mem_pool_info Va p) ! ii) = bits (levels (mem_pool_info Vb p) ! ii)) ⟹
   inv_bitmap Va ⟹
   inv_bitmap Vb"
by (simp add: inv_bitmap_def Let_def)


lemma inv_bitmap_freeing2free:
"inv_bitmap_mp V p ⟹
  ∃lv bl. bits (levels (mem_pool_info V p) ! lv) ! bl = FREEING
          ∧ bits (levels (mem_pool_info V2 p) ! lv) = (bits (levels (mem_pool_info V p) ! lv)) [bl := FREE]
          ∧ (∀lv'. lv ≠ lv' ⟶  bits (levels (mem_pool_info V2 p) ! lv') =  bits (levels (mem_pool_info V p) ! lv') ) ⟹
  length (levels (mem_pool_info V p)) = length (levels (mem_pool_info V2 p))
  ⟹ inv_bitmap_mp V2 p"
apply(simp add:Let_def) apply clarify
apply(subgoal_tac "length (bits (levels (mem_pool_info V p) ! i)) = length (bits (levels (mem_pool_info V2 p) ! i))")
  prefer 2 apply(case_tac "i = lv") apply auto[1] apply auto[1]
apply(rule conjI) apply clarify
  apply(rule conjI) apply clarify
    apply(case_tac "i = lv ∧ j = bl") apply clarsimp
      apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
        prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
    apply (metis BlockState.distinct(21) nth_list_update_neq)

  apply clarify
    apply(case_tac "i = lv ∧ j = bl") apply clarsimp
      apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
        prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(25) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(21) BlockState.distinct(25) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(21) BlockState.distinct(25) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(21) BlockState.distinct(25) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(21) BlockState.distinct(25) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(21) BlockState.distinct(25) nth_list_update_neq)

apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(11) list_update_beyond not_less nth_list_update_eq nth_list_update_neq)

done

lemma inv_bitmap_allocating2allocate:
"inv_bitmap_mp V p ⟹
  ∃lv bl. bits (levels (mem_pool_info V p) ! lv) ! bl = ALLOCATING
          ∧ bits (levels (mem_pool_info V2 p) ! lv) = (bits (levels (mem_pool_info V p) ! lv)) [bl := ALLOCATED]
          ∧ (∀lv'. lv ≠ lv' ⟶  bits (levels (mem_pool_info V2 p) ! lv') =  bits (levels (mem_pool_info V p) ! lv') )  ⟹
  length (levels (mem_pool_info V p)) = length (levels (mem_pool_info V2 p))
  ⟹ inv_bitmap_mp V2 p"
apply(simp add:Let_def) apply clarify
apply(subgoal_tac "length (bits (levels (mem_pool_info V p) ! i)) = length (bits (levels (mem_pool_info V2 p) ! i))")
  prefer 2 apply(case_tac "i = lv") apply auto[1] apply auto[1]
apply(rule conjI) apply clarify
  apply(rule conjI) apply clarify
    apply(case_tac "i = lv ∧ j = bl") apply clarsimp
      apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
        prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
    apply (metis BlockState.distinct(23) nth_list_update_neq)

  apply clarify
    apply(case_tac "i = lv ∧ j = bl") apply clarsimp
      apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
        prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(27) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(23) BlockState.distinct(27) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(23) BlockState.distinct(27) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(23) BlockState.distinct(27) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(23) BlockState.distinct(27) nth_list_update_neq)

apply(rule conjI) apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(23) BlockState.distinct(27) nth_list_update_neq)

apply clarify
  apply(case_tac "i = lv ∧ j = bl") apply clarsimp
    apply(subgoal_tac "get_bit_s V2 p i j = get_bit_s V p i j")
      prefer 2 apply(case_tac "i = lv") apply clarsimp apply presburger
  apply (smt BlockState.distinct(3) list_update_beyond not_less nth_list_update_eq nth_list_update_neq)
done


(************ move to invariant.thy **************)
lemma inv_bitmap_freelist_presv_setbit_notfree_h:
"¬ (x = lv ∧ y = bkn) ⟹
      Vb = set_bit_s V p lv bkn st ⟹
      get_bit_s V p x y= get_bit_s Vb p x y"
apply(simp add:set_bit_s_def set_bit_def)
by (metis (no_types, lifting) Mem_pool_lvl.simps(1) Mem_pool_lvl.simps(4)
                Mem_pool_lvl.surjective list_update_beyond not_less nth_list_update_eq nth_list_update_neq)

lemma inv_bitmap_freelist_presv_setbit_notfree:
"p ∈ mem_pools V ⟹
  inv_mempool_info V ∧ inv_aux_vars V ∧ inv_bitmap_freelist V ⟹
  st ≠ FREE ⟹
  get_bit_s V p lv bkn ≠ FREE ⟹
  inv_bitmap_freelist (set_bit_s V p lv bkn st)"
apply(simp add:inv_bitmap_freelist_def) apply(simp add:set_bit_s_def set_bit_def)
apply(simp add:Let_def)
apply clarsimp apply(rename_tac ii)
apply(rule conjI) (* ∀j < length bts. bts ! j = FREE ⟷ buf mp + j * (max_sz mp div (4 ^ i)) ∈ set fl *)
  apply clarsimp apply(rename_tac jj)
  apply(subgoal_tac "length (bits ((levels (mem_pool_info V p))
                       [lv := (levels (mem_pool_info V p) ! lv)⦇bits := (bits (levels (mem_pool_info V p) ! lv))[bkn := st]⦈] ! ii))
                     = length (bits (levels (mem_pool_info V p) ! ii))") prefer 2
    apply(case_tac "ii = lv") apply fastforce apply fastforce
  apply(case_tac "ii = lv ∧ jj = bkn")
    using inv_bitmap_freelist_presv_setbit_notfree_h apply force
    apply(subgoal_tac "(bits ((levels (mem_pool_info V p))[lv := (levels (mem_pool_info V p) ! lv)
                          ⦇bits := (bits (levels (mem_pool_info V p) ! lv))[bkn := st]⦈] ! ii)) ! jj =
                        (bits (levels (mem_pool_info V p) ! ii)) ! jj") prefer 2
      apply(case_tac "ii ≠ lv") apply fastforce
      apply(case_tac "jj ≠ bkn") apply fastforce
      apply fastforce
    apply(subgoal_tac "free_list ((levels (mem_pool_info V p))[lv := (levels (mem_pool_info V p) ! lv)
                          ⦇bits := (bits (levels (mem_pool_info V p) ! lv))[bkn := st]⦈] ! ii)
                    = free_list (levels (mem_pool_info V p) ! ii)") prefer 2
      apply(case_tac "ii ≠ lv") apply fastforce apply fastforce
    apply auto[1]

apply(rule conjI) (* ∀j < length fl. (∃n. n < n_max mp * (4 ^ i) ∧ fl ! j = buf mp + n * (max_sz mp div (4 ^ i))) *)
apply clarsimp apply(rename_tac jj)
  apply(subgoal_tac "length (bits ((levels (mem_pool_info V p))
                       [lv := (levels (mem_pool_info V p) ! lv)⦇bits := (bits (levels (mem_pool_info V p) ! lv))[bkn := st]⦈] ! ii))
                     = length (bits (levels (mem_pool_info V p) ! ii))") prefer 2
    apply(case_tac "ii = lv") apply fastforce apply fastforce
  apply(subgoal_tac "free_list ((levels (mem_pool_info V p))[lv := (levels (mem_pool_info V p) ! lv)
                          ⦇bits := (bits (levels (mem_pool_info V p) ! lv))[bkn := st]⦈] ! ii)
                    = free_list (levels (mem_pool_info V p) ! ii)") prefer 2
      apply(case_tac "ii ≠ lv") apply fastforce apply fastforce
  apply auto[1]

(* distinct fl *)
apply(subgoal_tac "free_list ((levels (mem_pool_info V p))[lv := (levels (mem_pool_info V p) ! lv)
                          ⦇bits := (bits (levels (mem_pool_info V p) ! lv))[bkn := st]⦈] ! ii)
                    = free_list (levels (mem_pool_info V p) ! ii)") prefer 2
      apply(case_tac "ii ≠ lv") apply fastforce apply fastforce
  apply auto[1]
done

end