# Theory Optimal_BST_Memo

theory Optimal_BST_Memo
imports Optimal_BST State_Main Product_Lexorder RBT_Mapping Optimal_BST_Examples
section ‹Memoization\label{sec:memo}›

theory Optimal_BST_Memo
imports
Optimal_BST
"HOL-Library.Product_Lexorder"
"HOL-Library.RBT_Mapping"
Optimal_BST_Examples
begin

text ‹This theory memoizes the recursive algorithms with the help of our generic memoization
framework. Note that currently only the tree building (function @{const Optimal_BST.opt_bst}) is memoized but not the computation of ‹w›.›

global_interpretation Wpl
where a = a and b = b for a b
defines w_ab = w and wpl_ab = "wpl.wpl w_ab" .

text ‹First we express @{const argmin} via @{const fold}.
At the same time we improve efficiency.›

lemma fold_argmin: "fold (λx (m,fm). let fx = f x in if fx ≤ fm then (x,fx) else (m,fm)) xs (x,f x)
= (argmin f (x#xs), f(argmin f (x#xs)))"
by (induction xs arbitrary: x) (auto simp: Let_def split: prod.split)

lemma argmin_fold: "argmin f xs = (case xs of [] ⇒ undefined |
x#xs ⇒ fst(fold (λx (m,fm). let fx = f x in if fx ≤ fm then (x,fx) else (m,fm)) xs (x,f x)))"
apply(auto simp:fold_argmin split: list.split)
apply (meson argmin.elims list.distinct(1))
done

text ‹The actual memoization of the cubic algorithm:›

context Optimal_BST
begin

memoize_fun opt_bst⇩m: opt_bst with_memory dp_consistency_mapping
(* FIXME why not argmin_argmin2? memoize_prover breaks!
*)
thm opt_bst⇩m'.simps

memoize_correct
by memoize_prover

lemmas [code] = opt_bst⇩m.memoized_correct

end

text ‹Code generation:›

global_interpretation Optimal_BST
where w = "w_ab a b"
rewrites "wpl.wpl (w_ab a b) = wpl_ab a b" for a b
defines opt_bst_ab = opt_bst and opt_bst_ab' = opt_bst⇩m'