Theory AutoCorres2.AbstractArrays

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory AbstractArrays
imports
  "TypHeapLib"
  "WordSetup"
begin

(*
 * Return a list of addresses that contain an element for an array at location
 * "p" of length "n".
 *)
primrec
  array_addrs :: "('a::mem_type) ptr ⇒ nat ⇒ 'a ptr list"
where
  "array_addrs _ 0 = []"
| "array_addrs p (Suc n) = p # (array_addrs (p +⇩p 1) n)"

declare array_addrs.simps(2) [simp del]

(* The first element is in the array if the array has non-zero length. *)
lemma hd_in_array_addrs [simp]:
  "(x ∈ set (array_addrs x n)) = (n > 0)"
  by (cases n, auto simp: array_addrs.simps(2))

lemma array_addrs_1 [simp]:
  "array_addrs p (Suc 0) = [p]"
  "array_addrs p 1 = [p]"
  by (auto simp: array_addrs.simps(2))

(* All array elements are aligned if the array itself is aligned. *)
lemma array_addrs_ptr_aligned:
     "⟦ x ∈ set (array_addrs p n); ptr_aligned p ⟧ ⟹ ptr_aligned x"
  apply (induct n arbitrary: x p)
  subgoal by clarsimp
  subgoal for n x p
    apply (clarsimp simp: array_addrs.simps(2))
    apply (erule disjE)
     apply clarsimp
    apply atomize
    apply (drule_tac x=x in spec)
    apply (drule_tac x="p +⇩p 1" in spec)
    apply (clarsimp simp: ptr_aligned_plus)
    done
  done

(* Split off the last element in an array. *)
lemma set_array_addrs_unfold_last:
  shows "set (array_addrs a (Suc n)) = set (array_addrs a n) ∪ {(a :: ('a::mem_type) ptr) +⇩p int n}"
    (is "?LHS a n = ?RHS a n")
proof (induct n arbitrary: a)
  fix a
  show "?LHS a 0 = ?RHS a 0"
    by clarsimp
next
  fix a n
  assume induct: "⋀a. ?LHS a n = ?RHS a n"
  show "?LHS a (Suc n) = ?RHS a (Suc n)"
  apply (subst array_addrs.simps(2))
  apply (subst set_simps)
  apply (subst induct [where a="a +⇩p 1"])
  apply (subst array_addrs.simps(2))
  apply (subst set_simps)
  apply (clarsimp simp: CTypesDefs.ptr_add_def field_simps insert_commute)
  done
qed

(* Alternative representation of the set of array elements. *)
lemma set_array_addrs:
  "set (array_addrs (p :: ('a::mem_type) ptr) n)
           = {x. ∃k. x = p +⇩p int k ∧ k < n }"
  apply (induct n arbitrary: p)
  subgoal by (clarsimp simp: not_less)
  subgoal for n p
    apply (subst set_array_addrs_unfold_last)
    apply atomize
    apply (drule_tac x=p in spec)
    apply (erule ssubst)
    apply (rule set_eqI)
    apply (rule iffI)
     apply clarsimp
     apply (erule disjE)
      apply clarsimp
      apply force
     apply force
    apply clarsimp
    apply (rename_tac k)
    apply (drule_tac x=k in spec)
    apply (clarsimp simp: not_less)
    apply (subgoal_tac "k = n")
     apply clarsimp
    apply clarsimp
    done
  done

end