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