Theory Precomputation

subsection Precomputation

text ‹This theory contains precomputation functions, which take another function $f$ and a 
  finite set of inputs, and provide the same function $f$ as output, except that now all
  values $f\ i$ are precomputed if $i$ is contained in the set of finite inputs.›

theory Precomputation
imports 
  Containers.RBT_Set2
  "HOL-Library.RBT_Mapping"
begin
  
lemma lookup_tabulate: "x ∈ set xs ⟹ Mapping.lookup (Mapping.tabulate xs f) x = Some (f x)"
  by (transfer, simp add: map_of_map_Pair_key)

lemma lookup_tabulate2: "Mapping.lookup (Mapping.tabulate xs f) x = Some y ⟹ y = f x"
  by transfer (metis map_of_map_Pair_key option.distinct(1) option.sel)

definition memo_int :: "int ⇒ int ⇒ (int ⇒ 'a) ⇒ (int ⇒ 'a)" where
  "memo_int low up f ≡ let m = Mapping.tabulate [low .. up] f
     in (λ x. if x ≥ low ∧ x ≤ up then the (Mapping.lookup m x) else f x)"

lemma memo_int[simp]: "memo_int low up f = f"
proof (intro ext)
  fix x
  show "memo_int low up f x = f x"
  proof (cases "x ≥ low ∧ x ≤ up")
    case False
    thus ?thesis unfolding memo_int_def by auto
  next
    case True
    from True have x: "x ∈ set [low .. up]" by auto
    with True lookup_tabulate[OF this, of f]
    show ?thesis unfolding memo_int_def by auto
  qed
qed

definition memo_nat :: "nat ⇒ nat ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)" where
  "memo_nat low up f ≡ let m = Mapping.tabulate [low ..< up] f
     in (λ x. if x ≥ low ∧ x < up then the (Mapping.lookup m x) else f x)"

lemma memo_nat[simp]: "memo_nat low up f = f"
proof (intro ext)
  fix x
  show "memo_nat low up f x = f x"
  proof (cases "x ≥ low ∧ x < up")
    case False
    thus ?thesis unfolding memo_nat_def by auto
  next
    case True
    from True have x: "x ∈ set [low ..< up]" by auto
    with True lookup_tabulate[OF this, of f]
    show ?thesis unfolding memo_nat_def by auto
  qed
qed

definition memo :: "'a list ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b)" where
  "memo xs f ≡ let m = Mapping.tabulate xs f
     in (λ x. case Mapping.lookup m x of None ⇒ f x | Some y ⇒ y)"

lemma memo[simp]: "memo xs f = f"
proof (intro ext)
  fix x
  show "memo xs f x = f x"
  proof (cases "Mapping.lookup (Mapping.tabulate xs f) x")
    case None
    thus ?thesis unfolding memo_def by auto
  next
    case (Some y)
    with lookup_tabulate2[OF this]
    show ?thesis unfolding memo_def by auto
  qed
qed


end