Theory Lists_Ex

(*
  File: Lists_Ex.thy
  Author: Bohua Zhan
*)

section ‹Lists›

theory Lists_Ex
  imports Mapping_Str
begin

text ‹
  Examples on lists. The itrev example comes from
  \<^cite>‹‹Section 2.4› in "prog-prove"›.

  The development here of insertion and deletion on lists is
  essential for verifying functional binary search trees and
  red-black trees. The idea, following Nipkow~\<^cite>‹"nipkow16"›,
  is that showing sorted-ness and preservation of multisets for trees
  should be done on the in-order traversal of the tree.
›

subsection ‹Linear time version of rev›

fun itrev :: "'a list ⇒ 'a list ⇒ 'a list" where
  "itrev []       ys = ys"
| "itrev (x # xs) ys = itrev xs (x # ys)"
setup ‹fold add_rewrite_rule @{thms itrev.simps}›

lemma itrev_eq_rev: "itrev x [] = rev x"
@proof
  @induct x for "∀y. itrev x y = rev x @ y" arbitrary y
@qed

subsection ‹Strict sorted›

fun strict_sorted :: "'a::linorder list ⇒ bool" where
  "strict_sorted [] = True"
| "strict_sorted (x # ys) = ((∀y∈set ys. x < y) ∧ strict_sorted ys)"
setup ‹fold add_rewrite_rule @{thms strict_sorted.simps}›

lemma strict_sorted_appendI [backward]:
  "strict_sorted xs ∧ strict_sorted ys ∧ (∀x∈set xs. ∀y∈set ys. x < y) ⟹ strict_sorted (xs @ ys)"
@proof @induct xs @qed

lemma strict_sorted_appendE1 [forward]:
  "strict_sorted (xs @ ys) ⟹ strict_sorted xs ∧ strict_sorted ys"
@proof @induct xs @qed

lemma strict_sorted_appendE2 [forward]:
  "strict_sorted (xs @ ys) ⟹ x ∈ set xs ⟹ ∀y∈set ys. x < y"
@proof @induct xs @qed

lemma strict_sorted_distinct [forward]: "strict_sorted l ⟹ distinct l"
@proof @induct l @qed

subsection ‹Ordered insert›

fun ordered_insert :: "'a::ord ⇒ 'a list ⇒ 'a list" where
  "ordered_insert x [] = [x]"
| "ordered_insert x (y # ys) = (
    if x = y then (y # ys)
    else if x < y then x # (y # ys)
    else y # ordered_insert x ys)"
setup ‹fold add_rewrite_rule @{thms ordered_insert.simps}›

lemma ordered_insert_set [rewrite]:
  "set (ordered_insert x ys) = {x} ∪ set ys"
@proof @induct ys @qed

lemma ordered_insert_sorted [forward]:
  "strict_sorted ys ⟹ strict_sorted (ordered_insert x ys)"
@proof @induct ys @qed

lemma ordered_insert_binary [rewrite]:
  "strict_sorted (xs @ a # ys) ⟹ ordered_insert x (xs @ a # ys) =
    (if x < a then ordered_insert x xs @ a # ys
     else if x > a then xs @ a # ordered_insert x ys
     else xs @ a # ys)"
@proof @induct xs @qed

subsection ‹Deleting an element›

fun remove_elt_list :: "'a ⇒ 'a list ⇒ 'a list" where
  "remove_elt_list x [] = []"
| "remove_elt_list x (y # ys) = (if y = x then remove_elt_list x ys else y # remove_elt_list x ys)"
setup ‹fold add_rewrite_rule @{thms remove_elt_list.simps}›

lemma remove_elt_list_set [rewrite]:
  "set (remove_elt_list x ys) = set ys - {x}"
@proof @induct ys @qed

lemma remove_elt_list_sorted [forward]:
  "strict_sorted ys ⟹ strict_sorted (remove_elt_list x ys)"
@proof @induct ys @qed

lemma remove_elt_idem [rewrite]:
  "x ∉ set ys ⟹ remove_elt_list x ys = ys"
@proof @induct ys @qed

lemma remove_elt_list_binary [rewrite]:
  "strict_sorted (xs @ a # ys) ⟹ remove_elt_list x (xs @ a # ys) =
    (if x < a then remove_elt_list x xs @ a # ys
     else if x > a then xs @ a # remove_elt_list x ys else xs @ ys)"
@proof @induct xs @with
  @subgoal "xs = []"
    @case "x < a" @with @have "x ∉ set ys" @end
  @endgoal @end
@qed

subsection ‹Ordered insertion into list of pairs›

fun ordered_insert_pairs :: "'a::ord ⇒ 'b ⇒ ('a × 'b) list ⇒ ('a × 'b) list" where
  "ordered_insert_pairs x v [] = [(x, v)]"
| "ordered_insert_pairs x v (y # ys) = (
    if x = fst y then ((x, v) # ys)
    else if x < fst y then (x, v) # (y # ys)
    else y # ordered_insert_pairs x v ys)"
setup ‹fold add_rewrite_rule @{thms ordered_insert_pairs.simps}›

lemma ordered_insert_pairs_map [rewrite]:
  "map_of_alist (ordered_insert_pairs x v ys) = update_map (map_of_alist ys) x v"
@proof @induct ys @qed

lemma ordered_insert_pairs_set [rewrite]:
  "set (map fst (ordered_insert_pairs x v ys)) = {x} ∪ set (map fst ys)"
@proof @induct ys @qed

lemma ordered_insert_pairs_sorted [backward]:
  "strict_sorted (map fst ys) ⟹ strict_sorted (map fst (ordered_insert_pairs x v ys))"
@proof @induct ys @qed

lemma ordered_insert_pairs_binary [rewrite]:
  "strict_sorted (map fst (xs @ a # ys)) ⟹ ordered_insert_pairs x v (xs @ a # ys) =
    (if x < fst a then ordered_insert_pairs x v xs @ a # ys
     else if x > fst a then xs @ a # ordered_insert_pairs x v ys
     else xs @ (x, v) # ys)"
@proof @induct xs @qed

subsection ‹Deleting from a list of pairs›

fun remove_elt_pairs :: "'a ⇒ ('a × 'b) list ⇒ ('a × 'b) list" where
  "remove_elt_pairs x [] = []"
| "remove_elt_pairs x (y # ys) = (if fst y = x then ys else y # remove_elt_pairs x ys)"
setup ‹fold add_rewrite_rule @{thms remove_elt_pairs.simps}›

lemma remove_elt_pairs_map [rewrite]:
  "strict_sorted (map fst ys) ⟹ map_of_alist (remove_elt_pairs x ys) = delete_map x (map_of_alist ys)"
@proof @induct ys @with
  @subgoal "ys = y # ys'"
    @case "fst y = x" @with @have "x ∉ set (map fst ys')" @end
  @endgoal @end
@qed

lemma remove_elt_pairs_on_set [rewrite]:
  "strict_sorted (map fst ys) ⟹ set (map fst (remove_elt_pairs x ys)) = set (map fst ys) - {x}"
@proof @induct ys @qed

lemma remove_elt_pairs_sorted [backward]:
  "strict_sorted (map fst ys) ⟹ strict_sorted (map fst (remove_elt_pairs x ys))"
@proof @induct ys @qed

lemma remove_elt_pairs_idem [rewrite]:
  "x ∉ set (map fst ys) ⟹ remove_elt_pairs x ys = ys"
@proof @induct ys @qed

lemma remove_elt_pairs_binary [rewrite]:
  "strict_sorted (map fst (xs @ a # ys)) ⟹ remove_elt_pairs x (xs @ a # ys) =
    (if x < fst a then remove_elt_pairs x xs @ a # ys
     else if x > fst a then xs @ a # remove_elt_pairs x ys else xs @ ys)"
@proof @induct xs @with
  @subgoal "xs = []"
    @case "x < fst a" @with @have "x ∉ set (map fst ys)" @end
  @endgoal @end
@qed

subsection ‹Search in a list of pairs›

lemma map_of_alist_binary [rewrite]:
  "strict_sorted (map fst (xs @ a # ys)) ⟹ (map_of_alist (xs @ a # ys))⟨x⟩ =
   (if x < fst a then (map_of_alist xs)⟨x⟩
    else if x > fst a then (map_of_alist ys)⟨x⟩ else Some (snd a))"
@proof @induct xs @with
  @subgoal "xs = []"
    @case "x ∉ set (map fst ys)"
  @endgoal @end
@qed

end