diff --git a/thys/Monad_Memo_DP/example/CYK.thy b/thys/Monad_Memo_DP/example/CYK.thy
--- a/thys/Monad_Memo_DP/example/CYK.thy
+++ b/thys/Monad_Memo_DP/example/CYK.thy
@@ -1,295 +1,295 @@
 subsection "The CYK Algorithm"
 
 theory CYK
 imports
   "HOL-Library.IArray"
   "HOL-Library.Code_Target_Numeral"
   "HOL-Library.Product_Lexorder"
   "HOL-Library.RBT_Mapping"
   "../state_monad/State_Main"
   "../heap_monad/Heap_Default"
   Example_Misc
 begin
 
 subsubsection \<open>Misc\<close>
 
 lemma append_iff_take_drop:
   "w = u@v \<longleftrightarrow> (\<exists>k \<in> {0..length w}. u = take k w \<and> v = drop k w)"
 by (metis (full_types) append_eq_conv_conj append_take_drop_id atLeastAtMost_iff le0 le_add1 length_append) 
 
 lemma append_iff_take_drop1: "u \<noteq> [] \<Longrightarrow> v \<noteq> [] \<Longrightarrow>
   w = u@v \<longleftrightarrow> (\<exists>k \<in> {1..length w - 1}. u = take k w \<and> v = drop k w)"
 by(auto simp: append_iff_take_drop)
 
 subsubsection \<open>Definitions\<close>
 
 datatype ('n, 't) rhs = NN 'n 'n | T 't 
 
 type_synonym ('n, 't) prods = "('n \<times> ('n, 't) rhs) list"
 
 context
 fixes P :: "('n :: heap, 't) prods"
 begin
 
 inductive yield :: "'n \<Rightarrow> 't list \<Rightarrow> bool" where
 "(A, T a) \<in> set P \<Longrightarrow> yield A [a]" |
 "\<lbrakk> (A, NN B C) \<in> set P; yield B u; yield C v \<rbrakk> \<Longrightarrow> yield A (u@v)"
 
 lemma yield_not_Nil: "yield A w \<Longrightarrow> w \<noteq> []"
 by (induction rule: yield.induct) auto
 
 lemma yield_eq1:
   "yield A [a] \<longleftrightarrow> (A, T a) \<in> set P" (is "?L = ?R")
 proof
   assume ?L thus ?R 
     by(induction A "[a]" arbitrary: a rule: yield.induct)
       (auto simp add: yield_not_Nil append_eq_Cons_conv)
 qed (simp add: yield.intros)
 
 lemma yield_eq2: assumes "length w > 1"
 shows "yield A w \<longleftrightarrow> (\<exists>B u C v. yield B u \<and> yield C v \<and> w = u@v \<and> (A, NN B C) \<in> set P)"
        (is "?L = ?R")
 proof
   assume ?L from this assms show ?R
     by(induction rule: yield.induct) (auto)
 next
   assume ?R with assms show ?L
     by (auto simp add: yield.intros)
 qed
 
 
 subsubsection "CYK on Lists"
 
 fun cyk :: "'t list \<Rightarrow> 'n list" where
 "cyk [] = []" |
 "cyk [a] = [A . (A, T a') <- P, a'= a]" |
 "cyk w =
   [A. k <- [1..<length w], B <- cyk (take k w), C <- cyk (drop k w), (A, NN B' C') <- P, B' = B, C' = C]"
 
 lemma set_cyk_simp2[simp]: "length w \<ge> 2 \<Longrightarrow> set(cyk w) =
   (\<Union>k \<in> {1..length w - 1}. \<Union>B \<in> set(cyk (take k w)). \<Union>C \<in> set(cyk (drop k w)). {A. (A, NN B C) \<in> set P})"
 apply(cases w)
  apply simp
 subgoal for _ w'
 apply(case_tac w')
  apply auto
     apply force
    apply force
   apply force
  using le_Suc_eq le_simps(3) apply auto[1]
 by (metis drop_Suc_Cons le_Suc_eq le_antisym not_le take_Suc_Cons)
 done
 
 declare cyk.simps(3)[simp del]
 
 lemma cyk_correct: "set(cyk w) = {N. yield N w}"
 proof (induction w rule: cyk.induct)
   case 1 thus ?case by (auto dest: yield_not_Nil)
 next
   case 2 thus ?case by (auto simp add: yield_eq1)
 next
   case (3 v vb vc)
   let ?w = "v # vb # vc"
   have "set(cyk ?w) = (\<Union>k\<in>{1..length ?w-1}. {N. \<exists>A B. (N, NN A B) \<in> set P \<and>
              yield A (take k ?w) \<and> yield B (drop k ?w)})"
     by(auto simp add:"3.IH" simp del:upt_Suc)
   also have "... = {N. \<exists>A B. (N, NN A B) \<in> set P \<and>
               (\<exists>u v. yield A u \<and> yield B v \<and> ?w = u@v)}"
     by(fastforce simp add: append_iff_take_drop1 yield_not_Nil)
   also have "... = {N. yield N ?w}" using yield_eq2[of ?w] by(auto)
   finally show ?case .
 qed
 
 subsubsection "CYK on Lists and Index"
 
 fun cyk2 :: "'t list \<Rightarrow> nat * nat \<Rightarrow> 'n list" where
 "cyk2 w (i,0) = []" |
 "cyk2 w (i,Suc 0) = [A . (A, T a) <- P, a = w!i]" |
 "cyk2 w (i,n) =
 [A. k <- [1..<n], B <- cyk2 w (i,k), C <- cyk2 w (i+k,n-k), (A, NN B' C') <- P, B' = B, C' = C]"
 
 lemma set_aux: "(\<Union>xb\<in>set P. {A. (A, NN B C) = xb}) = {A. (A, NN B C) \<in> set P}"
 by auto
 
 lemma cyk2_eq_cyk: "i+n \<le> length w \<Longrightarrow> set(cyk2 w (i,n)) = set(cyk (take n (drop i w)))"
 proof(induction w "(i,n)" arbitrary: i n rule: cyk2.induct)
   case 1 show ?case by(simp)
 next
   case 2 show ?case using "2.prems"
     by(auto simp: hd_drop_conv_nth take_Suc)
 next
   case (3 w i m)
   show ?case using "3.prems"
     by(simp add: 3(1,2) min.absorb1 min.absorb2 drop_take atLeastLessThanSuc_atLeastAtMost set_aux
          del:upt_Suc cong: SUP_cong_simp)
       (simp add: add.commute)
 qed
 
 definition "CYK S w =  (S \<in> set(cyk2 w (0, length w)))"
 
 theorem CYK_correct: "CYK S w = yield S w"
 by(simp add: CYK_def cyk2_eq_cyk cyk_correct)
 
 
 subsubsection "CYK With Index Function"
 
 context
 fixes w :: "nat \<Rightarrow> 't"
 begin
 
 fun cyk_ix :: "nat * nat \<Rightarrow> 'n list" where
 "cyk_ix (i,0) = []" |
 "cyk_ix (i,Suc 0) = [A . (A, T a) <- P, a = w i]" |
 "cyk_ix (i,n) =
   [A. k <- [1..<n], B <- cyk_ix (i,k), C <- cyk_ix (i+k,n-k), (A, NN B' C') <- P, B' = B, C' = C]"
 
 subsubsection \<open>Correctness Proof\<close>
 
 lemma cyk_ix_simp2: "set(cyk_ix (i,Suc(Suc n))) =
   (\<Union>k \<in> {1..Suc n}. \<Union>B \<in> set(cyk_ix (i,k)). \<Union>C \<in> set(cyk_ix (i+k,n+2-k)). {A. (A, NN B C) \<in> set P})"
 by(simp add: atLeastLessThanSuc_atLeastAtMost set_aux del: upt_Suc)
 
 declare cyk_ix.simps(3)[simp del]
 
-abbreviation "slice f i j \<equiv> map f [i..<j]"
+abbreviation (input) "slice f i j \<equiv> map f [i..<j]"
 
 lemma slice_append_iff_take_drop1: "u \<noteq> [] \<Longrightarrow> v \<noteq> [] \<Longrightarrow>
   slice w i j = u @ v \<longleftrightarrow> (\<exists>k. 1 \<le> k \<and> k \<le> j-i-1 \<and> slice w i (i + k) = u \<and> slice w (i + k) j = v)"
 by(subst append_iff_take_drop1) (auto simp: take_map drop_map Bex_def)
 
 lemma cyk_ix_correct:
   "set(cyk_ix (i,n)) = {N. yield N (slice w i (i+n))}"
 proof (induction "(i,n)" arbitrary: i n rule: cyk_ix.induct)
   case 1 thus ?case by (auto simp: dest: yield_not_Nil)
 next
   case 2 thus ?case by (auto simp add: yield_eq1)
 next
   case (3 i m)
   let ?n = "Suc(Suc m)" let ?w = "slice w i (i+?n)"
   have "set(cyk_ix (i,?n)) = (\<Union>k\<in>{1..Suc m}. {N. \<exists>A B. (N, NN A B) \<in> set P \<and>
              yield A (slice w i (i+k)) \<and> yield B (slice w (i+k) (i+?n))})"
     by(auto simp add: 3 cyk_ix_simp2 simp del: upt_Suc)
   also have "... = {N. \<exists>A B. (N, NN A B) \<in> set P \<and>
               (\<exists>u v. yield A u \<and> yield B v \<and> slice w i (i+?n) = u@v)}"
     by(fastforce simp del: upt_Suc simp: slice_append_iff_take_drop1 yield_not_Nil cong: conj_cong)
   also have "... = {N. yield N ?w}" using yield_eq2[of ?w] by(auto)
   finally show ?case .
 qed
 
 subsubsection \<open>Functional Memoization\<close>
 
 memoize_fun cyk_ix\<^sub>m: cyk_ix with_memory dp_consistency_mapping monadifies (state) cyk_ix.simps
 thm cyk_ix\<^sub>m'.simps
 
 memoize_correct
   by memoize_prover
 print_theorems
 
 lemmas [code] = cyk_ix\<^sub>m.memoized_correct
 
 
 subsubsection \<open>Imperative Memoization\<close>
 
 context
   fixes n :: nat
 begin
 
 context
   fixes mem :: "'n list option array"
 begin
 
 memoize_fun cyk_ix\<^sub>h: cyk_ix
   with_memory dp_consistency_heap_default where bound = "Bound (0, 0) (n, n)" and mem="mem"
   monadifies (heap) cyk_ix.simps
 
 context includes heap_monad_syntax begin
 thm cyk_ix\<^sub>h'.simps cyk_ix\<^sub>h_def
 end
 
 memoize_correct
   by memoize_prover
 
 lemmas memoized_empty = cyk_ix\<^sub>h.memoized_empty
 
 lemmas init_success = cyk_ix\<^sub>h.init_success
 
 end (* Fixed array *)
 
 definition "cyk_ix_impl i j = do {mem \<leftarrow> mem_empty (n * n); cyk_ix\<^sub>h' mem (i, j)}"
 
 lemma cyk_ix_impl_success:
   "success (cyk_ix_impl i j) Heap.empty"
   using init_success[of _ cyk_ix\<^sub>h' "(i, j)", OF cyk_ix\<^sub>h.crel]
   by (simp add: cyk_ix_impl_def index_size_defs)
 
 lemma min_wpl_heap:
   "cyk_ix (i, j) = result_of (cyk_ix_impl i j) Heap.empty"
   unfolding cyk_ix_impl_def
   using memoized_empty[of _ cyk_ix\<^sub>h' "(i, j)", OF cyk_ix\<^sub>h.crel]
   by (simp add: index_size_defs)
 
 end (* Bound *)
 
 end (* Index *)
 
 definition "CYK_ix S w n =  (S \<in> set(cyk_ix w (0,n)))"
 
 theorem CYK_ix_correct: "CYK_ix S w n = yield S (slice w 0 n)"
 by(simp add: CYK_ix_def cyk_ix_correct)
 
 definition "cyk_list w = cyk_ix (\<lambda>i. w ! i) (0,length w)"
 
 definition
   "CYK_ix_impl S w n = do {R \<leftarrow> cyk_ix_impl w n 0 n; return (S \<in> set R)}"
 
 lemma CYK_ix_impl_correct:
   "result_of (CYK_ix_impl S w n) Heap.empty = yield S (slice w 0 n)"
   unfolding CYK_ix_impl_def
   by (simp add: execute_bind_success[OF cyk_ix_impl_success]
         min_wpl_heap[symmetric] CYK_ix_correct CYK_ix_def[symmetric]
      )
 
 end (* Fixed Productions *)
 
 
 subsubsection \<open>Functional Test Case\<close>
 
 value
   "(let P = [(0::int, NN 1 2), (0, NN 2 3),
             (1, NN 2 1), (1, T (CHR ''a'')),
             (2, NN 3 3), (2, T (CHR ''b'')),
             (3, NN 1 2), (3, T (CHR ''a''))]
   in map (\<lambda>w. cyk2 P w (0,length w)) [''baaba'', ''baba''])"
 
 value
   "(let P = [(0::int, NN 1 2), (0, NN 2 3),
             (1, NN 2 1), (1, T (CHR ''a'')),
             (2, NN 3 3), (2, T (CHR ''b'')),
             (3, NN 1 2), (3, T (CHR ''a''))]
   in map (cyk_list P) [''baaba'', ''baba''])"
 
 definition "cyk_ia P w = (let a = IArray w in cyk_ix P (\<lambda>i. a !! i) (0,length w))"
 
 value
   "(let P = [(0::int, NN 1 2), (0, NN 2 3),
             (1, NN 2 1), (1, T (CHR ''a'')),
             (2, NN 3 3), (2, T (CHR ''b'')),
             (3, NN 1 2), (3, T (CHR ''a''))]
   in map (cyk_ia P) [''baaba'', ''baba''])"
 
 subsubsection \<open>Imperative Test Case\<close>
 
 definition "cyk_ia' P w = (let a = IArray w in cyk_ix_impl P (\<lambda>i. a !! i) (length w) 0 (length w))"
 
 definition
   "test = (let P = [(0::int, NN 1 2), (0, NN 2 3),
             (1, NN 2 1), (1, T (CHR ''a'')),
             (2, NN 3 3), (2, T (CHR ''b'')),
             (3, NN 1 2), (3, T (CHR ''a''))]
   in map (cyk_ia' P) [''baaba'', ''baba''])"
 
 code_reflect Test functions test
 
 ML \<open>List.map (fn f => f ()) Test.test\<close>
 
 end
diff --git a/thys/Monad_Memo_DP/example/Min_Ed_Dist0.thy b/thys/Monad_Memo_DP/example/Min_Ed_Dist0.thy
--- a/thys/Monad_Memo_DP/example/Min_Ed_Dist0.thy
+++ b/thys/Monad_Memo_DP/example/Min_Ed_Dist0.thy
@@ -1,411 +1,411 @@
 subsection "Minimum Edit Distance"
 
 theory Min_Ed_Dist0
 imports
   "HOL-Library.IArray"
   "HOL-Library.Code_Target_Numeral"
   "HOL-Library.Product_Lexorder"
   "HOL-Library.RBT_Mapping"
   "../state_monad/State_Main"
   "../heap_monad/Heap_Main"
   Example_Misc
   "../util/Tracing"
   "../util/Ground_Function"
 begin
 
 subsubsection "Misc"
 
 text "Executable argmin"
 
 fun argmin :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'a list \<Rightarrow> 'a" where
 "argmin f [a] = a" |
 "argmin f (a#as) = (let m = argmin f as in if f a \<le> f m then a else m)"
 (* end rm *)
 
 (* Ex: Optimization of argmin *)
 fun argmin2 :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'a list \<Rightarrow> 'a * 'b" where
 "argmin2 f [a] = (a, f a)" |
 "argmin2 f (a#as) = (let fa = f a; (am,m) = argmin2 f as in if fa \<le> m then (a, fa) else (am,m))"
 
 
 subsubsection "Edit Distance"
 
 datatype 'a ed = Copy | Repl 'a | Ins 'a | Del
 
 fun edit :: "'a ed list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "edit (Copy # es) (x # xs) = x # edit es xs" |
 "edit (Repl a # es) (x # xs) = a # edit es xs" |
 "edit (Ins a # es) xs = a # edit es xs" |
 "edit (Del # es) (x # xs) = edit es xs" |
 "edit (Copy # es) [] = edit es []" |
 "edit (Repl a # es) [] = edit es []" |
 "edit (Del # es) [] = edit es []" |
 "edit [] xs = xs"
 
 abbreviation cost where
 "cost es \<equiv> length [e <- es. e \<noteq> Copy]"
 
 
 subsubsection "Minimum Edit Sequence"
 
 fun min_eds :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a ed list" where
 "min_eds [] [] = []" |
 "min_eds [] (y#ys) = Ins y # min_eds [] ys" |
 "min_eds (x#xs) [] = Del # min_eds xs []" |
 "min_eds (x#xs) (y#ys) =
   argmin cost [Ins y # min_eds (x#xs) ys, Del # min_eds xs (y#ys),
      (if x=y then Copy else Repl y) # min_eds xs ys]"
 
 lemma "min_eds ''vintner'' ''writers'' =
   [Ins CHR ''w'', Repl CHR ''r'', Copy, Del, Copy, Del, Copy, Copy, Ins CHR ''s'']"
 by eval
 (*
 value "min_eds ''madagascar'' ''bananas''"
 
 value "min_eds ''madagascaram'' ''banananas''"
 *)
 lemma min_eds_correct: "edit (min_eds xs ys) xs = ys"
 by (induction xs ys rule: min_eds.induct) auto
 
 lemma min_eds_same: "min_eds xs xs = replicate (length xs) Copy"
 by (induction xs) auto
 
 lemma min_eds_eq_Nil_iff: "min_eds xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
 by (induction xs ys rule: min_eds.induct) auto
 
 lemma min_eds_Nil: "min_eds [] ys = map Ins ys"
 by (induction ys) auto
 
 lemma min_eds_Nil2: "min_eds xs [] = replicate (length xs) Del"
 by (induction xs) auto
 
 lemma if_edit_Nil2: "edit es ([]::'a list) = ys \<Longrightarrow> length ys \<le> cost es"
 apply(induction es "[]::'a list" arbitrary: ys rule: edit.induct)
 apply auto
  apply fastforce
 apply fastforce
 done
 
 lemma if_edit_eq_Nil: "edit es xs = [] \<Longrightarrow> length xs \<le> cost es"
 by (induction es xs rule: edit.induct) auto
 
 lemma min_eds_minimal: "edit es xs = ys \<Longrightarrow> cost(min_eds xs ys) \<le> cost es"
 proof(induction xs ys arbitrary: es rule: min_eds.induct)
   case 1 thus ?case by simp
 next
   case 2 thus ?case by (auto simp add: min_eds_Nil dest: if_edit_Nil2)
 next
   case 3
   thus ?case by(auto simp add: min_eds_Nil2 dest: if_edit_eq_Nil)
 next
   case 4
   show ?case
   proof (cases "es")
     case Nil then show ?thesis using "4.prems" by (auto simp: min_eds_same)
   next
     case [simp]: (Cons e es')
     show ?thesis
     proof (cases e)
       case Copy
       thus ?thesis using "4.prems" "4.IH"(3)[of es'] by simp
     next
       case (Repl a)
       thus ?thesis using "4.prems" "4.IH"(3)[of es']
         using [[simp_depth_limit=1]] by simp
     next
       case (Ins a)
       thus ?thesis using "4.prems" "4.IH"(1)[of es']
         using [[simp_depth_limit=1]] by auto
     next
       case Del
       thus ?thesis using "4.prems" "4.IH"(2)[of es']
         using [[simp_depth_limit=1]] by auto
     qed
   qed
 qed
 
 
 subsubsection "Computing the Minimum Edit Distance"
 
 fun min_ed :: "'a list \<Rightarrow> 'a list \<Rightarrow> nat" where
 "min_ed [] [] = 0" |
 "min_ed [] (y#ys) = 1 + min_ed [] ys" |
 "min_ed (x#xs) [] = 1 + min_ed xs []" |
 "min_ed (x#xs) (y#ys) =
   Min {1 + min_ed (x#xs) ys, 1 + min_ed xs (y#ys), (if x=y then 0 else 1) + min_ed xs ys}"
 
 lemma min_ed_min_eds: "min_ed xs ys = cost(min_eds xs ys)"
 apply(induction xs ys rule: min_ed.induct)
 apply (auto split!: if_splits)
 done
 
 lemma "min_ed ''madagascar'' ''bananas'' = 6"
 by eval
 (*
 value "min_ed ''madagascaram'' ''banananas''"
 *)
 
 text "Exercise: Optimization of the Copy case"
 
 fun min_eds2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a ed list" where
 "min_eds2 [] [] = []" |
 "min_eds2 [] (y#ys) = Ins y # min_eds2 [] ys" |
 "min_eds2 (x#xs) [] = Del # min_eds2 xs []" |
 "min_eds2 (x#xs) (y#ys) =
   (if x=y then Copy # min_eds2 xs ys
    else argmin cost
      [Ins y # min_eds2 (x#xs) ys, Del # min_eds2 xs (y#ys), Repl y # min_eds2 xs ys])"
 
 value "min_eds2 ''madagascar'' ''bananas''"
 
 lemma cost_Copy_Del: "cost(min_eds xs ys) \<le> cost (min_eds xs (x#ys)) + 1"
 apply(induction xs ys rule: min_eds.induct)
 apply(auto simp del: filter_True filter_False split!: if_splits)
 done
 
 lemma cost_Copy_Ins: "cost(min_eds xs ys) \<le> cost (min_eds (x#xs) ys) + 1"
 apply(induction xs ys rule: min_eds.induct)
 apply(auto simp del: filter_True filter_False split!: if_splits)
 done
 
 lemma "cost(min_eds2 xs ys) = cost(min_eds xs ys)"
 proof(induction xs ys rule: min_eds2.induct)
   case (4 x xs y ys) thus ?case
     apply (auto split!: if_split)
       apply (metis (mono_tags, lifting) Suc_eq_plus1 Suc_leI cost_Copy_Del cost_Copy_Ins le_imp_less_Suc le_neq_implies_less not_less)
      apply (metis Suc_eq_plus1 cost_Copy_Del le_antisym)
     by (metis Suc_eq_plus1 cost_Copy_Ins le_antisym)
 qed simp_all
 
 lemma "min_eds2 xs ys = min_eds xs ys"
 oops
 (* Not proveable because Copy comes last in min_eds but first in min_eds2.
    Can reorder, but the proof still requires the same two lemmas cost_*_* above.
 *)
 
 
 subsubsection "Indexing"
 
 text "Indexing lists"
 
 context
 fixes xs ys :: "'a list"
 fixes m n :: nat
 begin
 
 function (sequential)
   min_ed_ix' :: "nat * nat \<Rightarrow> nat" where
 "min_ed_ix' (i,j) =
   (if i \<ge> m then
      if j \<ge> n then 0 else 1 + min_ed_ix' (i,j+1) else
    if j \<ge> n then 1 + min_ed_ix' (i+1, j)
    else
    Min {1 + min_ed_ix' (i,j+1), 1 + min_ed_ix' (i+1, j),
        (if xs!i = ys!j then 0 else 1) + min_ed_ix' (i+1,j+1)})"
 by pat_completeness auto
 termination by(relation "measure(\<lambda>(i,j). (m - i) + (n - j))") auto
 
 
 declare min_ed_ix'.simps[simp del]
 
 end
 
 lemma min_ed_ix'_min_ed:
   "min_ed_ix' xs ys (length xs) (length ys) (i, j) = min_ed (drop i xs) (drop j ys)"
 apply(induction "(i,j)" arbitrary: i j rule: min_ed_ix'.induct[of "length xs" "length ys"])
 apply(subst min_ed_ix'.simps)
 apply(simp add: Cons_nth_drop_Suc[symmetric])
 done
 
 
 text "Indexing functions"
 
 context
 fixes xs ys :: "nat \<Rightarrow> 'a"
 fixes m n :: nat
 begin
 
 function (sequential)
   min_ed_ix :: "nat \<times> nat \<Rightarrow> nat" where
 "min_ed_ix (i, j) =
   (if i \<ge> m then
      if j \<ge> n then 0 else n-j else
    if j \<ge> n then m-i
    else
    min_list [1 + min_ed_ix (i, j+1), 1 + min_ed_ix (i+1, j),
        (if xs i = ys j then 0 else 1) + min_ed_ix (i+1, j+1)])"
 by pat_completeness auto
 termination by(relation "measure(\<lambda>(i,j). (m - i) + (n - j))") auto
 
 
 subsubsection \<open>Functional Memoization\<close>
 
 memoize_fun min_ed_ix\<^sub>m: min_ed_ix with_memory dp_consistency_mapping monadifies (state) min_ed_ix.simps
 thm min_ed_ix\<^sub>m'.simps
 
 memoize_correct
   by memoize_prover
 print_theorems
 
 lemmas [code] = min_ed_ix\<^sub>m.memoized_correct
 
 declare min_ed_ix.simps[simp del]
 
 
 subsubsection \<open>Imperative Memoization\<close>
 
 context
   fixes mem :: "nat ref \<times> nat ref \<times> nat option array ref \<times> nat option array ref"
   assumes mem_is_init: "mem = result_of (init_state (n + 1) m (m + 1)) Heap.empty"
 begin
 
 interpretation iterator
   "\<lambda> (x, y). x \<le> m \<and> y \<le> n \<and> x > 0"
   "\<lambda> (x, y). if y > 0 then (x, y - 1) else (x - 1, n)"
   "\<lambda> (x, y). (m - x) * (n + 1) + (n - y)"
   by (rule table_iterator_down)
 
 lemma [intro]:
   "dp_consistency_heap_array_pair' (n + 1) fst snd id m (m + 1) mem"
   by (standard; simp add: mem_is_init injective_def)
 
 lemma [intro]:
   "dp_consistency_heap_array_pair_iterator (n + 1) fst snd id m (m + 1) mem
    (\<lambda> (x, y). if y > 0 then (x, y - 1) else (x - 1, n))
    (\<lambda> (x, y). (m - x) * (n + 1) + (n - y))
    (\<lambda> (x, y). x \<le> m \<and> y \<le> n \<and> x > 0)
   "
   by (standard; simp add: mem_is_init injective_def)
 
 memoize_fun min_ed_ix\<^sub>h: min_ed_ix
   with_memory (default_proof) dp_consistency_heap_array_pair_iterator
   where size = "n + 1"
     and key1="fst :: nat \<times> nat \<Rightarrow> nat" and key2="snd :: nat \<times> nat \<Rightarrow> nat"
     and k1="m :: nat" and k2="m + 1 :: nat"
     and to_index = "id :: nat \<Rightarrow> nat"
     and mem = mem
     and cnt = "\<lambda> (x, y). x \<le> m \<and> y \<le> n \<and> x > 0"
     and nxt = "\<lambda> (x::nat, y). if y > 0 then (x, y - 1) else (x - 1, n)"
     and sizef = "\<lambda> (x, y). (m - x) * (n + 1) + (n - y)"
 monadifies (heap) min_ed_ix.simps
 
 memoize_correct
   by memoize_prover
 
 lemmas memoized_empty =
   min_ed_ix\<^sub>h.memoized_empty[OF min_ed_ix\<^sub>h.consistent_DP_iter_and_compute[OF min_ed_ix\<^sub>h.crel]]
 lemmas iter_heap_unfold = iter_heap_unfold
 
 end (* Fixed Memory *)
 
 end
 
 
 subsubsection \<open>Test Cases\<close>
 
-abbreviation "slice xs i j \<equiv> map xs [i..<j]"
+abbreviation (input) "slice xs i j \<equiv> map xs [i..<j]"
 
 lemma min_ed_Nil1: "min_ed [] ys = length ys"
 by (induction ys) auto
 
 lemma min_ed_Nil2: "min_ed xs [] = length xs"
 by (induction xs) auto
 
 (* prove correctness of min_ed_ix directly ? *)
 lemma min_ed_ix_min_ed: "min_ed_ix xs ys m n (i,j) = min_ed (slice xs i m) (slice ys j n)"
 apply(induction "(i,j)" arbitrary: i j rule: min_ed_ix.induct[of m n])
 apply(simp add: min_ed_ix.simps upt_conv_Cons min_ed_Nil1 min_ed_Nil2 Suc_diff_Suc)
 done
 
 
 text \<open>Functional Test Cases\<close>
 
 definition "min_ed_list xs ys = min_ed_ix (\<lambda>i. xs!i) (\<lambda>i. ys!i) (length xs) (length ys) (0,0)"
 
 lemma "min_ed_list ''madagascar'' ''bananas'' = 6"
 by eval
 
 definition "min_ed_ia xs ys = (let a = IArray xs; b = IArray ys
   in min_ed_ix (\<lambda>i. a!!i) (\<lambda>i. b!!i) (length xs) (length ys) (0,0))"
 
 lemma "min_ed_ia ''madagascar'' ''bananas'' = 6"
 by eval
 
 
 
 text \<open>Extracting an Executable Constant for the Imperative Implementation\<close>
 
 ground_function min_ed_ix\<^sub>h'_impl: min_ed_ix\<^sub>h'.simps
 termination
   by(relation "measure(\<lambda>(xs, ys, m, n, mem, i, j). (m - i) + (n - j))") auto
 
 lemmas [simp del] = min_ed_ix\<^sub>h'_impl.simps min_ed_ix\<^sub>h'.simps
 
 lemma min_ed_ix\<^sub>h'_impl_def:
   includes heap_monad_syntax
   fixes m n :: nat
   fixes mem :: "nat ref \<times> nat ref \<times> nat option array ref \<times> nat option array ref"
   assumes mem_is_init: "mem = result_of (init_state (n + 1) m (m + 1)) Heap.empty"
   shows "min_ed_ix\<^sub>h'_impl xs ys m n mem = min_ed_ix\<^sub>h' xs ys m n mem"
 proof -
   have "min_ed_ix\<^sub>h'_impl xs ys m n mem (i, j) = min_ed_ix\<^sub>h' xs ys m n mem (i, j)" for i j
     apply (induction rule: min_ed_ix\<^sub>h'.induct[OF mem_is_init])
     apply (subst min_ed_ix\<^sub>h'_impl.simps)
     apply (subst min_ed_ix\<^sub>h'.simps[OF mem_is_init])
     apply (solve_cong simp)
     done
   then show ?thesis
     by auto
 qed
 
 definition
   "iter_min_ed_ix xs ys m n mem = iterator_defs.iter_heap
     (\<lambda> (x, y). x \<le> m \<and> y \<le> n \<and> x > 0)
     (\<lambda> (x, y). if y > 0 then (x, y - 1) else (x - 1, n))
     (min_ed_ix\<^sub>h'_impl xs ys m n mem)
   "
 
 lemma iter_min_ed_ix_unfold[code]:
   "iter_min_ed_ix xs ys m n mem = (\<lambda> (i, j).
     (if i > 0 \<and> i \<le> m \<and> j \<le> n
      then do {
             min_ed_ix\<^sub>h'_impl xs ys m n mem (i, j);
             iter_min_ed_ix xs ys m n mem (if j > 0 then (i, j - 1) else (i - 1, n))
           }
      else Heap_Monad.return ()))"
   unfolding iter_min_ed_ix_def by (rule ext) (safe, simp add: iter_heap_unfold)
 
 definition
   "min_ed_ix_impl xs ys m n i j = do {
     mem \<leftarrow> (init_state (n + 1) (m::nat) (m + 1) ::
       (nat ref \<times> nat ref \<times> nat option array ref \<times> nat option array ref) Heap);
     iter_min_ed_ix xs ys m n mem (m, n);
     min_ed_ix\<^sub>h'_impl xs ys m n mem (i, j)
   }"
 
 lemma bf_impl_correct:
   "min_ed_ix xs ys m n (i, j) = result_of (min_ed_ix_impl xs ys m n i j) Heap.empty"
   using memoized_empty[OF HOL.refl, of xs ys m n "(i, j)" "\<lambda> _. (m, n)"]
   by (simp add:
       execute_bind_success[OF succes_init_state] min_ed_ix_impl_def min_ed_ix\<^sub>h'_impl_def
       iter_min_ed_ix_def
      )
 
 
 text \<open>Imperative Test Case\<close>
 
 definition
   "min_ed_ia\<^sub>h xs ys = (let a = IArray xs; b = IArray ys
   in min_ed_ix_impl (\<lambda>i. a!!i) (\<lambda>i. b!!i) (length xs) (length ys) 0 0)"
 
 definition
   "test_case = min_ed_ia\<^sub>h ''madagascar'' ''bananas''"
 
 export_code min_ed_ix in SML module_name Test
 
 code_reflect Test functions test_case
 
 text \<open>One can see a trace of the calls to the memory in the output\<close>
 ML \<open>Test.test_case ()\<close>
 
 end