Theory DataStructures

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

theory DataStructures
imports Main
begin

(*
 * Proofs on abstract data structures that should be applicable
 * to concrete C proofs.
 *)


(*
 * Singly-linked list definitions and lemmas adapted from:
 *
 *   "Proving Pointer Programs in Higher-Order Logic"
 *   Farhad Mehta, Tobias Nipkow
 *)

locale linked_list =
  (* Fetch next pointer from object. *)
  fixes list_next :: "'a ⇒ 'p"
  (* Null pointer. *)
  and NULL :: "'p"

context linked_list begin

primrec
  list :: "('p ⇒ 'a option) ⇒ 'p list ⇒ 'p ⇒ bool"
where
  "list s [] i = (i = NULL)"
| "list s (x#xs) i =
    (i = x ∧ x ≠ NULL ∧ (∃a. s x = Some a ∧  list s xs (list_next a)))"



definition
  is_list :: "('p ⇒ 'a option) ⇒ 'p ⇒ bool"
where
  "is_list s p ≡ ∃xs. list s xs p"

definition
  the_list :: "('p ⇒ 'a option) ⇒ 'p ⇒ 'p list"
where
  "the_list s p ≡ (THE xs. list s xs p)"

lemma list_empty [simp]: "list s xs NULL = (xs = [])"
  by (case_tac "xs", auto)

lemma is_list_empty [simp]: "is_list s NULL"
  by (clarsimp simp: is_list_def)

lemma the_list_empty [simp]: "the_list s NULL = []"
  by (clarsimp simp: the_list_def)

lemma list_unique: "⟦ list s xs p; list s ys p ⟧ ⟹ xs = ys"
  apply (induct xs arbitrary: ys p)
   apply simp
  apply (case_tac ys, auto)
  done

lemma list_ptr_unique: "⟦ list s xs p; list s xs p' ⟧ ⟹ p = p'"
  by (metis linked_list.list.simps(1) linked_list.list.simps(2) neq_Nil_conv)

lemma list_non_NULL:
  "p ≠ NULL ⟹
    list s xs p = (∃ys. xs= p#ys ∧ (∃a. s p = Some a ∧ list s ys (list_next a)))"
  by (case_tac xs, auto)

lemma is_list_non_NULL:
  "p ≠ NULL ⟹
    is_list s p = (∃a. s p = Some a ∧ is_list s (list_next a))"
  apply (clarsimp simp: is_list_def list_non_NULL)
  apply force
  done

lemma the_list_non_NULL:
  "⟦ p ≠ NULL; is_list s p ⟧ ⟹
    the_list s p = (p # (the_list s (list_next (the (s p)))))"
  apply (clarsimp simp: the_list_def is_list_def list_non_NULL)
  apply (rule the_equality)
   apply (clarsimp simp: list_unique)
   apply (metis (lifting) list_unique the_equality)
  apply clarsimp
  apply (metis (lifting) list_unique the_equality)
  done

lemma list_is_list: "list s xs p ⟹ is_list s p"
  apply (clarsimp simp: is_list_def)
  apply force
  done

lemma list_the_list: "list s xs p ⟹ the_list s p = xs"
  apply (clarsimp simp: the_list_def)
  apply (metis (lifting) list_unique the_equality)
  done

lemma the_list_empty' [simp]:
    "is_list s p ⟹ (the_list s p = []) = (p = NULL)"
  by (metis is_list_def list_empty list_ptr_unique list_the_list)

lemma list_last_is_NULL:
    "⟦ is_list s p; the_list s p = l; p ≠ NULL ⟧ ⟹ list_next (the (s (last l))) = NULL"
  apply (induct l arbitrary: p)
   apply clarsimp
  apply (metis is_list_non_NULL last_ConsL last_ConsR linked_list.the_list_non_NULL option.sel the_list_empty' list.sel(3))
  done

lemma list_in_Some:
  "⟦ list s xs p; x ∈ set xs ⟧ ⟹ ∃a. s x = Some a"
  apply (induct xs arbitrary: p, auto)
  done

lemma list_mem: "⟦ list s xs p; p ≠ NULL ⟧ ⟹ p ∈ set xs"
  by (case_tac xs, auto)

lemma list_ign [iff]: "⟦ x ∉ set xs ⟧ ⟹ list (s(x := v)) xs p = list s xs p"
  apply (induct xs arbitrary: p)
   apply clarsimp
  apply atomize
  apply clarsimp
  done

lemma list_ign_ext' [intro, iff]:
    "⟦ ∀x ∈ set xs. (∃a. s x = Some a) = (∃a. s' x = Some a) ∧ (list_next (the (s x)) = list_next (the (s' x)))  ⟧ ⟹ list s xs p = list s' xs p"
  apply (induct xs arbitrary: p, auto)
  done

lemma list_ign_ext [iff?]: "⟦ ∀x ∈ set xs. s x = s' x ⟧ ⟹ list s xs p = list s' xs p"
  apply force
  done

lemma list_append_Ex:
  "list s (xs@ys) p ⟹ (∃q. list s ys q)"
  apply (induct xs arbitrary: ys p)
   apply force
  apply force
  done

lemma list_head_not_in_list: "⟦ list s xs (list_next a); s p = Some a ⟧ ⟹ p ∉ set xs"
  apply (rule ccontr)
  apply clarsimp
  apply (frule split_list)
  apply clarsimp
  apply (frule list_append_Ex)
  apply clarsimp
  apply (drule (1) list_unique)
  apply clarsimp
  done

lemma list_distinct: "list s xs x ⟹ distinct xs"
  apply (induct xs arbitrary: x)
   apply clarsimp
  apply clarsimp
  apply (drule (1) list_head_not_in_list)
  apply clarsimp
  done

lemma list_next: "⟦ list s xs x; s x = Some a; x ≠ NULL ⟧ ⟹ list s (tl xs) (list_next a)"
  apply (case_tac xs)
   apply clarsimp
  apply clarsimp
  done

primrec
  path :: "('p ⇒ 'a option) ⇒ 'p ⇒ 'p list ⇒ 'p ⇒ bool"
where
  "path s x [] y = (x = y)"
| "path s x (a#as) y = (x ≠ NULL ∧ x = a ∧ (∃v. s x = Some v ∧ path s (list_next v) as y))"

lemma path_null [simp]: "path s NULL as x = (as = [] ∧ x = NULL)"
  by (case_tac as, auto)

lemma path_no_null [simp]: "⟦ path s a xs b ⟧ ⟹ NULL ∉ set xs"
  apply (induct xs arbitrary: a)
   apply clarsimp
  apply clarsimp
  done

lemma path_next:
  "⟦ x ≠ NULL ⟧ ⟹ path s x as y = ((as = [] ∧ x = y)
    ∨ (∃bs. as = x # bs ∧ (∃a. s x = Some a ∧ path s (list_next a) bs y)))"
  apply (case_tac as, auto)
  done

lemma path_null_list: "path s a xs NULL = list s xs a"
  apply (induct xs arbitrary: a, auto)
  done

lemma path_ign [iff]: "u ∉ set as ⟹ path (s(u := v)) x as y = path s x as y"
  by (induct as arbitrary: x y, auto)

lemma path_split [simp]: "path s x (as @ bs) z = (∃y. path s x as y ∧ path s y bs z)"
  apply (induct as arbitrary: x, auto)
  done

lemma list_split [simp]: "list s (as @ bs) x = (∃y. path s x as y ∧ list s bs y)"
  by (induct as arbitrary: x, auto)

end

(*
 * Doubly-linked list, with NULL pointers.
 *)
locale dbl_linked_list =
  linked_list +
  constrains list_next :: "'a ⇒ 'p" and NULL :: "'p"
  (* Fetch prev pointer from object. *)
  fixes list_prev :: "'a ⇒ 'p"

context dbl_linked_list begin

primrec
  dbl_list_tail :: "('p ⇒ 'a option) ⇒ 'p ⇒ 'p list ⇒ 'p ⇒ bool"
where
  "dbl_list_tail s p [] h = (h = NULL)"
| "dbl_list_tail s p (x#xs) h =
    (h = x ∧ x ≠ NULL ∧ (∃a. s x = Some a ∧ list_prev a = p ∧ dbl_list_tail s x xs (list_next a)))"

abbreviation
  dbl_list :: "('p ⇒ 'a option) ⇒ 'p list ⇒ 'p ⇒ bool"
where
  "dbl_list s l h ≡ dbl_list_tail s NULL l h"

lemma dbl_list_null_empty [simp]: "dbl_list_tail s p [] NULL"
  by simp

lemma dbl_list_empty [simp]: "dbl_list_tail s p xs NULL = (xs = [])"
  by (case_tac xs, auto)

lemma dbl_list_single: "⟦ s x = Some y; list_prev y = NULL; list_next y = NULL; x ≠ NULL ⟧ ⟹ dbl_list s [x] x"
  by simp

lemma dbl_list_tail_non_NULL:
  "h ≠ NULL ⟹
    dbl_list_tail s p xs h =
      (∃ys. xs= h#ys ∧ (∃a. s h = Some a ∧ list_prev a = p ∧ dbl_list_tail s h ys (list_next a)))"
  apply (case_tac xs, auto)
  done

lemma dbl_list_tail_in_Some:
  "⟦ dbl_list_tail s p xs h; x ∈ set xs ⟧ ⟹ ∃a. s x = Some a"
  apply (induct xs arbitrary: p h, auto)
  done

lemma dbl_list_tail_mem: "⟦ dbl_list_tail s p xs h; h ≠ NULL ⟧ ⟹ h ∈ set xs"
  by (case_tac xs, auto)

lemma dbl_list_ign [iff]: "⟦ x ∉ set xs ⟧ ⟹ dbl_list_tail (s(x := v)) p xs h = dbl_list_tail s p xs h"
  apply (induct xs arbitrary: p h)
   apply clarsimp
  apply atomize
  apply clarsimp
  done

lemma dbl_list_ign_ext' [intro, iff]:
    "⟦ ∀x ∈ set xs.
        (∃a. s x = Some a) = (∃a. s' x = Some a)
        ∧ (list_next (the (s x)) = list_next (the (s' x)))
        ∧ (list_prev (the (s x)) = list_prev (the (s' x))) ⟧ ⟹
     dbl_list_tail s p xs h = dbl_list_tail s' p xs h"
  apply (induct xs arbitrary: p h, auto)
  done

lemma dbl_list_ign_ext [iff?]: "⟦ ∀x ∈ set xs. s x = s' x ⟧ ⟹ dbl_list_tail s p xs h = dbl_list_tail s' p xs h"
  apply force
  done

lemma dbl_list_unique: "⟦ dbl_list_tail s p xs h; dbl_list_tail s p' ys h ⟧ ⟹ xs = ys"
  apply (induct xs arbitrary: ys p p' h)
   apply simp
  apply (case_tac ys, auto)
  done

lemma dbl_list_append_Ex:
  "dbl_list_tail s p (xs@ys) h ⟹ (∃q. dbl_list_tail s (last (p#xs)) ys q)"
  apply (induct xs arbitrary: ys p h)
   apply force
  apply force
  done

lemma dbl_list_head_not_in_list: "⟦ dbl_list_tail s p xs (list_next a); s h = Some a ⟧ ⟹ h ∉ set xs"
  apply (rule ccontr)
  apply clarsimp
  apply (frule split_list)
  apply clarsimp
  apply (frule dbl_list_append_Ex)
  apply clarsimp
  apply (drule (1) dbl_list_unique)
  apply clarsimp
  done

lemma dbl_list_distinct: "dbl_list_tail s p xs x ⟹ distinct xs"
  apply (induct xs arbitrary: x p)
   apply clarsimp
  apply clarsimp
  apply (drule (1) dbl_list_head_not_in_list)
  apply clarsimp
  done

lemma dbl_list_next: "⟦ dbl_list_tail s p xs x; s x = Some a; x ≠ NULL ⟧ ⟹ dbl_list_tail s x (tl xs) (list_next a)"
  apply (case_tac xs)
   apply clarsimp
  apply clarsimp
  done

end

(*
 * Circular-linked list, with a head node.
 *)
locale circ_linked_list =
  (* Fetch next pointer from object. *)
  fixes list_next :: "'a ⇒ 'p"
  (* Fetch previous pointer from object. *)
  fixes list_prev :: "'a ⇒ 'p"

context circ_linked_list begin

fun
  circ_list_tail :: "('p ⇒ 'a option) ⇒ 'p ⇒ 'p ⇒ 'p list ⇒ 'p ⇒ bool"
where
  "circ_list_tail s head prev [] current = (current = head)"
| "circ_list_tail s head prev (x#xs) current =
        (current = x ∧ current ≠ head ∧
          (∃a. s x = Some a ∧ list_prev a = prev
            ∧ circ_list_tail s head x xs (list_next a)))"

lemma circ_list_defn_test: "
  ⟦ s head = Some headNode;
    s n1 = Some node1;
    s n2 = Some node2;
    list_next headNode = n1; list_next node1 = n2; list_next node2 = head;
    list_prev headNode = n2; list_prev node1 = head; list_prev node2 = n1;
    n1 ≠ head; n2 ≠ head ⟧ ⟹
   circ_list_tail s head head [n1, n2] n1"
  apply clarsimp
  done

definition
  circ_list :: "('p ⇒ 'a option) ⇒ 'p ⇒ 'p list ⇒ bool"
where
  "circ_list s head l ≡ (∃a. s head = Some a ∧ (list_prev a = (last (head # l))) ∧ (circ_list_tail s head head l (list_next a)))"

lemma circ_list_tail_empty [simp]: "circ_list_tail s head p xs head = (xs = [])"
  apply (case_tac xs)
   apply clarsimp
  apply clarsimp
  done

lemma circ_list_empty: "⟦ s head = Some a; list_next a = head; list_prev a = head ⟧ ⟹ circ_list s head []"
  apply (clarsimp simp: circ_list_def)
  done

lemma circ_list_single: "⟦
    x ≠ head;
    s x = Some a; list_next a = head; list_prev a = head;
    s head = Some b; list_next b = x; list_prev b = x
  ⟧ ⟹ circ_list s head [x]"
  apply (clarsimp simp: circ_list_def)
  done

lemma circ_list_tail_in_Some:
  "⟦ circ_list_tail s head p xs h; x ∈ set xs ⟧ ⟹ ∃a. s x = Some a"
  apply (induct xs arbitrary: p h, auto)
  done

lemma circ_list_tail_ign [iff]: "⟦ x ∉ set xs ⟧ ⟹ circ_list_tail (s(x := v)) head p xs h = circ_list_tail s head p xs h"
  apply (induct xs arbitrary: p h)
   apply clarsimp
  apply clarsimp
  done

lemma circ_list_ign [iff]: "⟦ x ∉ set xs; x ≠ head ⟧ ⟹ circ_list (s(x := v)) head xs = circ_list s head xs"
  apply (clarsimp simp: circ_list_def)
  done

lemmas circ_list_tail_ign' [iff] = circ_list_tail_ign [unfolded fun_upd_def]
lemmas circ_list_ign' [iff] = circ_list_ign [unfolded fun_upd_def]

lemma circ_list_tail_ign_ext' [intro?, iff?]:
    "⟦ ∀x ∈ set xs.
        (∃a. s x = Some a) = (∃a. s' x = Some a)
        ∧ (list_next (the (s x)) = list_next (the (s' x)))
        ∧ (list_prev (the (s x)) = list_prev (the (s' x))) ⟧ ⟹
     circ_list_tail s head p xs h = circ_list_tail s' head p xs h"
  apply (induct xs arbitrary: p h, auto)
  done

lemma circ_list_ign_ext' [intro?, iff?]:
    "⟦ ∀x ∈ set xs.
        (∃a. s x = Some a) = (∃a. s' x = Some a)
        ∧ (list_next (the (s x)) = list_next (the (s' x)))
        ∧ (list_prev (the (s x)) = list_prev (the (s' x)));
       (∃a. s head = Some a) = (∃a. s' head = Some a);
       (list_next (the (s head)) = list_next (the (s' head)));
       (list_prev (the (s head)) = list_prev (the (s' head))) ⟧ ⟹
     circ_list s head xs = circ_list s' head xs"
  apply (clarsimp simp: circ_list_def)
  apply (case_tac xs)
   apply force
  apply (clarsimp, safe, auto iff: circ_list_tail_ign_ext')
  done

lemma circ_list_tail_ign_ext [iff?]: "⟦ ∀x ∈ set xs. s x = s' x ⟧ ⟹ circ_list_tail s head p xs h = circ_list_tail s' head p xs h"
  apply (force iff: circ_list_tail_ign_ext')
  done

lemma circ_list_ign_ext [iff?]: "⟦ ∀x ∈ set xs. s x = s' x; s head = s' head ⟧ ⟹ circ_list s head xs = circ_list s' head xs"
  apply (force iff: circ_list_ign_ext')
  done

lemma circ_list_tail_unique: "⟦ circ_list_tail s head p xs h; circ_list_tail s head p' ys h ⟧ ⟹ xs = ys"
  apply (induct xs arbitrary: ys p p' h)
   apply clarsimp
  apply (case_tac ys, auto)
  done

lemma circ_list_unique: "⟦ circ_list s h xs; circ_list s h ys ⟧ ⟹ xs = ys"
  apply (clarsimp simp: circ_list_def)
  apply (erule (1) circ_list_tail_unique)
  done

lemma circ_list_tail_append_Ex:
  "circ_list_tail s head p (xs@ys) h ⟹ (∃q. circ_list_tail s head (last (p#xs)) ys q)"
  apply (induct xs arbitrary: ys p h)
   apply force
  apply force
  done

lemma circ_list_tail_head_not_in_list: "⟦ circ_list_tail s head p xs (list_next a); s h = Some a ⟧ ⟹ h ∉ set xs"
  apply (rule ccontr)
  apply clarsimp
  apply (frule split_list)
  apply clarsimp
  apply (frule circ_list_tail_append_Ex)
  apply clarsimp
  apply (drule (1) circ_list_tail_unique)
  apply clarsimp
  done

lemma circ_list_head_not_in_list: "⟦ circ_list s head xs ⟧ ⟹ head ∉ set xs"
  apply (clarsimp simp: circ_list_def)
  apply (drule (1) circ_list_tail_head_not_in_list)
  apply simp
  done

lemma circ_list_tail_distinct: "circ_list_tail s head p xs x ⟹ distinct xs"
  apply (induct xs arbitrary: x p)
   apply clarsimp
  apply clarsimp
  apply (drule (1) circ_list_tail_head_not_in_list)
  apply clarsimp
  done

lemma circ_list_distinct: "circ_list s head xs ⟹ distinct xs"
  by (metis circ_list_def circ_list_tail_distinct)

lemma circ_list_tail_prev':
  "⟦ circ_list_tail s h p a x; n ∈ set a; s n = Some m; list_prev m ≠ p ⟧ ⟹ list_prev m ∈ set a"
  apply (induct a arbitrary: p x)
   apply clarsimp
  apply force
  done

lemma circ_list_tail_prev:
  "⟦ circ_list_tail s h p a x; n ∈ set a; s n = Some m; list_prev m ∉ set a ⟧ ⟹ list_prev m = p"
  apply (induct a arbitrary: p x)
   apply clarsimp
  apply force
  done

lemma circ_list_tail_h_not_in_list:
  "⟦ circ_list_tail s h p a x ⟧ ⟹ h ∉ set a"
  by (induct a arbitrary: p x, auto)

lemma circ_list_tail_cong:
  "⟦ ⋀i. ⟦ i ∈ set a; i ≠ h ⟧ ⟹ s i = s' i; h = h'; p = p'; a = a'; x = x' ⟧
     ⟹ circ_list_tail s h p a x = circ_list_tail s' h' p' a' x'"
  apply clarsimp
  apply (case_tac "h' ∈ set a'")
   apply (metis circ_list_tail_h_not_in_list)
  apply (rule circ_list_tail_ign_ext')
  apply clarsimp
  apply metis
  done

end


end