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