Theory Mapping_Str

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

section ‹Mapping›

theory Mapping_Str
  imports "Auto2_HOL.Auto2_Main"
begin

text ‹
  Basic definitions of a mapping. Here, we enclose the mapping inside
  a structure, to make evaluation a first-order concept.
›

datatype ('a, 'b) map = Map "'a ⇒ 'b option"

fun meval :: "('a, 'b) map ⇒ 'a ⇒ 'b option" (‹_⟨_⟩› [90]) where
  "(Map f) ⟨h⟩ = f h"
setup ‹add_rewrite_rule @{thm meval.simps}›

lemma meval_ext: "∀x. M⟨x⟩ = N⟨x⟩ ⟹ M = N"
  apply (cases M) apply (cases N) by auto
setup ‹add_backward_prfstep_cond @{thm meval_ext} [with_filt (order_filter "M" "N")]›

definition empty_map :: "('a, 'b) map" where
  "empty_map = Map (λx. None)"
setup ‹add_rewrite_rule @{thm empty_map_def}›

definition update_map :: "('a, 'b) map ⇒ 'a ⇒ 'b ⇒ ('a ,'b) map" (‹ _ { _ → _ }› [89,90,90] 90) where
  "M {k → v} = Map (λx. if x = k then Some v else M⟨x⟩)"
setup ‹add_rewrite_rule @{thm update_map_def}›

definition delete_map :: "'a ⇒ ('a, 'b) map ⇒ ('a, 'b) map" where
  "delete_map k M = Map (λx. if x = k then None else M⟨x⟩)"
setup ‹add_rewrite_rule @{thm delete_map_def}›

subsection ‹Map from an AList›

fun map_of_alist :: "('a × 'b) list ⇒ ('a, 'b) map" where
  "map_of_alist [] = empty_map"
| "map_of_alist (x # xs) = (map_of_alist xs) {fst x → snd x}"
setup ‹fold add_rewrite_rule @{thms map_of_alist.simps}›

definition has_key_alist :: "('a × 'b) list ⇒ 'a ⇒ bool" where [rewrite]:
  "has_key_alist xs a ⟷ (∃p∈set xs. fst p = a)"

lemma map_of_alist_nil [rewrite_back]:
  "has_key_alist ys x ⟷ (map_of_alist ys)⟨x⟩ ≠ None"
@proof @induct ys @qed
setup ‹add_rewrite_rule_cond @{thm map_of_alist_nil} [with_term "(map_of_alist ?ys)⟨?x⟩"]›

lemma map_of_alist_some [forward]:
  "(map_of_alist xs)⟨k⟩ = Some v ⟹ (k, v) ∈ set xs"
@proof @induct xs @qed

lemma map_of_alist_nil':
  "x ∈ set (map fst ys) ⟷ (map_of_alist ys)⟨x⟩ ≠ None"
@proof @induct ys @qed
setup ‹add_rewrite_rule_cond @{thm map_of_alist_nil'} [with_term "(map_of_alist ?ys)⟨?x⟩"]›
    
subsection ‹Mapping defined by a set of key-value pairs›

definition unique_keys_set :: "('a × 'b) set ⇒ bool" where [rewrite]:
  "unique_keys_set S = (∀i x y. (i, x) ∈ S ⟶ (i, y) ∈ S ⟶ x = y)"

lemma unique_keys_setD [forward]: "unique_keys_set S ⟹ (i, x) ∈ S ⟹ (i, y) ∈ S ⟹ x = y" by auto2
setup ‹del_prfstep_thm_eqforward @{thm unique_keys_set_def}›

definition map_of_aset :: "('a × 'b) set ⇒ ('a, 'b) map" where
  "map_of_aset S = Map (λa. if ∃b. (a, b) ∈ S then Some (THE b. (a, b) ∈ S) else None)"
setup ‹add_rewrite_rule @{thm map_of_aset_def}›
setup ‹add_prfstep_check_req ("map_of_aset S", "unique_keys_set S")›

lemma map_of_asetI1 [rewrite]: "unique_keys_set S ⟹ (a, b) ∈ S ⟹ (map_of_aset S)⟨a⟩ = Some b"
@proof @have "∃b. (a, b) ∈ S" @have "∃!b. (a, b) ∈ S" @qed

lemma map_of_asetI2 [rewrite]: "∀b. (a, b) ∉ S ⟹ (map_of_aset S)⟨a⟩ = None" by auto2

lemma map_of_asetD1 [forward]: "(map_of_aset S)⟨a⟩ = None ⟹ ∀b. (a, b) ∉ S" by auto2

lemma map_of_asetD2 [forward]:
  "unique_keys_set S ⟹ (map_of_aset S)⟨a⟩ = Some b ⟹ (a, b) ∈ S" by auto2
setup ‹del_prfstep_thm @{thm map_of_aset_def}›

lemma map_of_aset_insert [rewrite]:
  "unique_keys_set (S ∪ {(k, v)}) ⟹ map_of_aset (S ∪ {(k, v)}) = (map_of_aset S) {k → v}"
@proof
  @let "M = map_of_aset S" "N = map_of_aset (S ∪ {(k, v)})"
  @have (@rule) "∀x. N⟨x⟩ = (M {k → v}) ⟨x⟩" @with @case "M⟨x⟩ = None" @end
@qed

lemma map_of_alist_to_aset [rewrite]:
  "unique_keys_set (set xs) ⟹ map_of_aset (set xs) = map_of_alist xs"
@proof @induct xs @with
  @subgoal "xs = x # xs'"
    @have "set (x # xs') = set xs' ∪ {x}"
  @endgoal @end
@qed

lemma map_of_aset_delete [rewrite]:
  "unique_keys_set S ⟹ (k, v) ∈ S ⟹ map_of_aset (S - {(k, v)}) = delete_map k (map_of_aset S)"
@proof
  @let "T = S - {(k, v)}"
  @let "M = map_of_aset S" "N = map_of_aset T"
  @have (@rule) "∀x. N⟨x⟩ = (delete_map k M) ⟨x⟩" @with
    @case "M⟨x⟩ = None" @case "x = k"
    @obtain y where "M⟨x⟩ = Some y" @have "(x, y) ∈ T"
  @end
@qed

lemma map_of_aset_update [rewrite]:
  "unique_keys_set S ⟹ (k, v) ∈ S ⟹
   map_of_aset (S - {(k, v)} ∪ {(k, v')}) = (map_of_aset S) {k → v'}" by auto2

lemma map_of_alist_delete [rewrite]:
  "set xs' = set xs - {x} ⟹ unique_keys_set (set xs) ⟹ x ∈ set xs ⟹
   map_of_alist xs' = delete_map (fst x) (map_of_alist xs)"
@proof @have "map_of_alist xs' = map_of_aset (set xs')" @qed

lemma map_of_alist_insert [rewrite]:
  "set xs' = set xs ∪ {x} ⟹ unique_keys_set (set xs') ⟹
   map_of_alist xs' = (map_of_alist xs) {fst x → snd x}"
@proof @have "map_of_alist xs' = map_of_aset (set xs')" @qed

lemma map_of_alist_update [rewrite]:
  "set xs' = set xs - {(k, v)} ∪ {(k, v')} ⟹ unique_keys_set (set xs) ⟹ (k, v) ∈ set xs ⟹
   map_of_alist xs' = (map_of_alist xs) {k → v'}"
@proof @have "map_of_alist xs' = map_of_aset (set xs')" @qed

subsection ‹Set of keys of a mapping›

definition keys_of :: "('a, 'b) map ⇒ 'a set" where [rewrite]:
  "keys_of M = {x. M⟨x⟩ ≠ None}"

lemma keys_of_iff [rewrite_bidir]: "x ∈ keys_of M ⟷ M⟨x⟩ ≠ None" by auto2
setup ‹del_prfstep_thm @{thm keys_of_def}›

lemma keys_of_empty [rewrite]: "keys_of empty_map = {}" by auto2

lemma keys_of_delete [rewrite]:
  "keys_of (delete_map x M) = keys_of M - {x}" by auto2

subsection ‹Minimum of a mapping, relevant for heaps (priority queues)›

definition is_heap_min :: "'a ⇒ ('a, 'b::linorder) map ⇒ bool" where [rewrite]:
  "is_heap_min x M ⟷ x ∈ keys_of M ∧ (∀k∈keys_of M. the (M⟨x⟩) ≤ the (M⟨k⟩))"

subsection ‹General construction and update of maps›

fun map_constr :: "(nat ⇒ bool) ⇒ (nat ⇒ 'a) ⇒ nat ⇒ (nat, 'a) map" where
  "map_constr S f 0 = empty_map"
| "map_constr S f (Suc k) = (let M = map_constr S f k in if S k then M {k → f k} else M)"
setup ‹fold add_rewrite_rule @{thms map_constr.simps}›

lemma map_constr_eval [rewrite]:
  "map_constr S f n = Map (λi. if i < n then if S i then Some (f i) else None else None)"
@proof @induct n @qed

lemma keys_of_map_constr [rewrite]:
  "i ∈ keys_of (map_constr S f n) ⟷ (S i ∧ i < n)" by auto2

definition map_update_all :: "(nat ⇒ 'a) ⇒ (nat, 'a) map ⇒ (nat, 'a) map" where [rewrite]:
  "map_update_all f M = Map (λi. if i ∈ keys_of M then Some (f i) else M⟨i⟩)"

fun map_update_all_impl :: "(nat ⇒ 'a) ⇒ (nat, 'a) map ⇒ nat ⇒ (nat, 'a) map" where
  "map_update_all_impl f M 0 = M"
| "map_update_all_impl f M (Suc k) =
   (let M' = map_update_all_impl f M k in if k ∈ keys_of M then M' {k → f k} else M')"
setup ‹fold add_rewrite_rule @{thms map_update_all_impl.simps}›

lemma map_update_all_impl_ind [rewrite]:
  "map_update_all_impl f M n = Map (λi. if i < n then if i ∈ keys_of M then Some (f i) else None else M⟨i⟩)"
@proof @induct n @qed

lemma map_update_all_impl_correct [rewrite]:
  "∀i∈keys_of M. i < n ⟹ map_update_all_impl f M n = map_update_all f M" by auto2

lemma keys_of_map_update_all [rewrite]:
  "keys_of (map_update_all f M) = keys_of M" by auto2

end