diff --git a/thys/Monad_Memo_DP/example/Bellman_Ford.thy b/thys/Monad_Memo_DP/example/Bellman_Ford.thy --- a/thys/Monad_Memo_DP/example/Bellman_Ford.thy +++ b/thys/Monad_Memo_DP/example/Bellman_Ford.thy @@ -1,425 +1,1188 @@ subsection \The Bellman-Ford Algorithm\ theory Bellman_Ford imports "HOL-Library.Extended" "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\ +lemma nat_le_cases: + fixes n :: nat + assumes "i \ n" + obtains "i < n" | "i = n" + using assms by (cases "i = n") auto + +bundle app_syntax begin + +notation App (infixl "$" 999) +notation Wrap ("\_\") + +end + +context dp_consistency_iterator +begin + +lemma crel_vs_iterate_state: + "crel_vs (=) () (iter_state f x)" if "((=) ===>\<^sub>T R) g f" + by (metis crel_vs_iterate_state iter_state_iterate_state that) + +lemma consistent_crel_vs_iterate_state: + "crel_vs (=) () (iter_state f x)" if "consistentDP f" + using consistentDP_def crel_vs_iterate_state that by simp + +end + instance extended :: (countable) countable proof standard obtain to_nat :: "'a \ nat" where "inj to_nat" by auto let ?f = "\ x. case x of Fin n \ to_nat n + 2 | Pinf \ 0 | Minf \ 1" from \inj _ \ have "inj ?f" by (auto simp: inj_def split: extended.split) then show "\to_nat :: 'a extended \ nat. inj to_nat" by auto qed instance extended :: (heap) heap .. +instantiation "extended" :: (conditionally_complete_lattice) complete_lattice +begin + +definition + "Inf A = ( + if A = {} \ A = {\} then \ + else if -\ \ A \ \ bdd_below (Fin -` A) then -\ + else Fin (Inf (Fin -` A)))" + +definition + "Sup A = ( + if A = {} \ A = {-\} then -\ + else if \ \ A \ \ bdd_above (Fin -` A) then \ + else Fin (Sup (Fin -` A)))" + +instance +proof standard + have [dest]: "Inf (Fin -` A) \ x" if "Fin x \ A" "bdd_below (Fin -` A)" for A and x :: 'a + using that by (intro cInf_lower) auto + have *: False if "\ z \ Inf (Fin -` A)" "\x. x \ A \ Fin z \ x" "Fin x \ A" for A and x z :: 'a + using cInf_greatest[of "Fin -` A" z] that vimage_eq by force + show "Inf A \ x" if "x \ A" for x :: "'a extended" and A + using that unfolding Inf_extended_def by (cases x) auto + show "z \ Inf A" if "\x. x \ A \ z \ x" for z :: "'a extended" and A + using that + unfolding Inf_extended_def + apply (clarsimp; safe) + apply force + apply force + subgoal + by (cases z; force simp: bdd_below_def) + subgoal + by (cases z; force simp: bdd_below_def) + subgoal for x y + by (cases z; cases y) (auto elim: *) + subgoal for x y + by (cases z; cases y; simp; metis * less_eq_extended.elims(2)) + done + have [dest]: "x \ Sup (Fin -` A)" if "Fin x \ A" "bdd_above (Fin -` A)" for A and x :: 'a + using that by (intro cSup_upper) auto + have *: False if "\ Sup (Fin -` A) \ z" "\x. x \ A \ x \ Fin z" "Fin x \ A" for A and x z :: 'a + using cSup_least[of "Fin -` A" z] that vimage_eq by force + show "x \ Sup A" if "x \ A" for x :: "'a extended" and A + using that unfolding Sup_extended_def by (cases x) auto + show "Sup A \ z" if "\x. x \ A \ x \ z" for z :: "'a extended" and A + using that + unfolding Sup_extended_def + apply (clarsimp; safe) + apply force + apply force + subgoal + by (cases z; force) + subgoal + by (cases z; force) + subgoal for x y + by (cases z; cases y) (auto elim: *) + subgoal for x y + by (cases z; cases y; simp; metis * extended.exhaust) + done + show "Inf {} = (top::'a extended)" + unfolding Inf_extended_def top_extended_def by simp + show "Sup {} = (bot::'a extended)" + unfolding Sup_extended_def bot_extended_def by simp +qed + +end + +instance "extended" :: ("{conditionally_complete_lattice,linorder}") complete_linorder .. + + +lemma Minf_eq_zero[simp]: "-\ = 0 \ False" and Pinf_eq_zero[simp]: "\ = 0 \ False" + unfolding zero_extended_def by auto + +lemma Sup_int: + fixes x :: int and X :: "int set" + assumes "X \ {}" "bdd_above X" + shows "Sup X \ X \ (\y\X. y \ Sup X)" +proof - + from assms obtain x y where "X \ {..y}" "x \ X" + by (auto simp: bdd_above_def) + then have *: "finite (X \ {x..y})" "X \ {x..y} \ {}" and "x \ y" + by (auto simp: subset_eq) + have "\!x\X. (\y\X. y \ x)" + proof + { fix z assume "z \ X" + have "z \ Max (X \ {x..y})" + proof cases + assume "x \ z" with \z \ X\ \X \ {..y}\ *(1) show ?thesis + by (auto intro!: Max_ge) + next + assume "\ x \ z" + then have "z < x" by simp + also have "x \ Max (X \ {x..y})" + using \x \ X\ *(1) \x \ y\ by (intro Max_ge) auto + finally show ?thesis by simp + qed } + note le = this + with Max_in[OF *] show ex: "Max (X \ {x..y}) \ X \ (\z\X. z \ Max (X \ {x..y}))" by auto + + fix z assume *: "z \ X \ (\y\X. y \ z)" + with le have "z \ Max (X \ {x..y})" + by auto + moreover have "Max (X \ {x..y}) \ z" + using * ex by auto + ultimately show "z = Max (X \ {x..y})" + by auto + qed + then show "Sup X \ X \ (\y\X. y \ Sup X)" + unfolding Sup_int_def by (rule theI') +qed + +lemmas Sup_int_in = Sup_int[THEN conjunct1] + +lemma Inf_int_in: + fixes S :: "int set" + assumes "S \ {}" "bdd_below S" + shows "Inf S \ S" + using assms unfolding Inf_int_def by (smt Sup_int_in bdd_above_uminus image_iff image_is_empty) + + lemma fold_acc_preserv: assumes "\ x acc. P acc \ P (f x acc)" "P acc" shows "P (fold f xs acc)" using assms(2) by (induction xs arbitrary: acc) (auto intro: assms(1)) + +lemma finite_setcompr_eq_image: "finite {f x |x. P x} \ finite (f ` {x. P x})" + by (simp add: setcompr_eq_image) + +lemma finite_lists_length_le1: "finite {xs. length xs \ i \ set xs \ {0..(n::nat)}}" for i + by (auto intro: finite_subset[OF _ finite_lists_length_le[OF finite_atLeastAtMost]]) + +lemma finite_lists_length_le2: "finite {xs. length xs + 1 \ i \ set xs \ {0..(n::nat)}}" for i + by (auto intro: finite_subset[OF _ finite_lists_length_le1[of "i"]]) + +lemmas [simp] = + finite_setcompr_eq_image finite_lists_length_le2[simplified] finite_lists_length_le1 + + lemma get_return: "run_state (State_Monad.bind State_Monad.get (\ m. State_Monad.return (f m))) m = (f m, m)" by (simp add: State_Monad.bind_def State_Monad.get_def) +lemma list_pidgeonhole: + assumes "set xs \ S" "card S < length xs" "finite S" + obtains as a bs cs where "xs = as @ a # bs @ a # cs" +proof - + from assms have "\ distinct xs" + by (metis card_mono distinct_card not_le) + then show ?thesis + by (metis append.assoc append_Cons not_distinct_conv_prefix split_list that) +qed + +lemma path_eq_cycleE: + assumes "v # ys @ [t] = as @ a # bs @ a # cs" + obtains (Nil_Nil) "as = []" "cs = []" "v = a" "a = t" "ys = bs" + | (Nil_Cons) cs' where "as = []" "v = a" "ys = bs @ a # cs'" "cs = cs' @ [t]" + | (Cons_Nil) as' where "as = v # as'" "cs = []" "a = t" "ys = as' @ a # bs" + | (Cons_Cons) as' cs' where "as = v # as'" "cs = cs' @ [t]" "ys = as' @ a # bs @ a # cs'" + using assms by (auto simp: Cons_eq_append_conv append_eq_Cons_conv append_eq_append_conv2) + +lemma le_add_same_cancel1: + "a + b \ a \ b \ 0" if "a < \" "-\ < a" for a b :: "int extended" + using that by (cases a; cases b) (auto simp add: zero_extended_def) + +lemma add_gt_minfI: + assumes "-\ < a" "-\ < b" + shows "-\ < a + b" + using assms by (cases a; cases b) auto + +lemma add_lt_infI: + assumes "a < \" "b < \" + shows "a + b < \" + using assms by (cases a; cases b) auto + +lemma sum_list_not_infI: + "sum_list xs < \" if "\ x \ set xs. x < \" for xs :: "int extended list" + using that + apply (induction xs) + apply (simp add: zero_extended_def)+ + by (smt less_extended_simps(2) plus_extended.elims) + +lemma sum_list_not_minfI: + "sum_list xs > -\" if "\ x \ set xs. x > -\" for xs :: "int extended list" + using that by (induction xs) (auto intro: add_gt_minfI simp: zero_extended_def) + + + subsubsection \Single-Sink Shortest Path Problem\ datatype bf_result = Path "nat list" int | No_Path | Computation_Error context fixes n :: nat and W :: "nat \ nat \ int extended" begin context fixes t :: nat \ \Final node\ begin text \ The correctness proof closely follows Kleinberg \&\ Tardos: "Algorithm Design", chapter "Dynamic Programming" @{cite "Kleinberg-Tardos"} \ -definition weight :: "nat list \ int extended" where - "weight xs = snd (fold (\ i (j, x). (i, W i j + x)) (rev xs) (t, 0))" +fun weight :: "nat list \ int extended" where + "weight [s] = 0" +| "weight (i # j # xs) = W i j + weight (j # xs)" definition "OPT i v = ( Min ( - {weight (v # xs) | xs. length xs + 1 \ i \ set xs \ {0..n}} \ + {weight (v # xs @ [t]) | xs. length xs + 1 \ i \ set xs \ {0..n}} \ {if t = v then 0 else \} ) )" -lemma weight_Cons [simp]: - "weight (v # w # xs) = W v w + weight (w # xs)" - by (simp add: case_prod_beta' weight_def) +lemma weight_alt_def': + "weight (s # xs) + w = snd (fold (\j (i, x). (j, W i j + x)) xs (s, w))" + by (induction xs arbitrary: s w; simp; smt add.commute add.left_commute) -lemma weight_single [simp]: - "weight [v] = W v t" - by (simp add: weight_def) +lemma weight_alt_def: + "weight (s # xs) = snd (fold (\j (i, x). (j, W i j + x)) xs (s, 0))" + by (rule weight_alt_def'[of s xs 0, simplified]) + +lemma weight_append: + "weight (xs @ a # ys) = weight (xs @ [a]) + weight (a # ys)" + by (induction xs rule: weight.induct; simp add: add.assoc) + + (* XXX Generalize to the right type class *) lemma Min_add_right: - "Min S + (x :: int extended) = Min ((\ y. y + x) ` S)" (is "?A = ?B") if "finite S" "S \ {}" + "Min S + x = Min ((\y. y + x) ` S)" (is "?A = ?B") + if "finite S" "S \ {}" for x :: "('a :: linordered_ab_semigroup_add) extended" proof - have "?A \ ?B" using that by (force intro: Min.boundedI add_right_mono) moreover have "?B \ ?A" using that by (force intro: Min.boundedI) ultimately show ?thesis by simp qed lemma OPT_0: "OPT 0 v = (if t = v then 0 else \)" unfolding OPT_def by simp (* TODO: Move to distribution! *) lemma Pinf_add_right[simp]: "\ + x = \" by (cases x; simp) subsubsection \Functional Correctness\ +lemma OPT_cases: + obtains (path) xs where "OPT i v = weight (v # xs @ [t])" "length xs + 1 \ i" "set xs \ {0..n}" + | (sink) "v = t" "OPT i v = 0" + | (unreachable) "v \ t" "OPT i v = \" + unfolding OPT_def + using Min_in[of "{weight (v # xs @ [t]) |xs. length xs + 1 \ i \ set xs \ {0..n}} + \ {if t = v then 0 else \}"] + by (auto simp: finite_lists_length_le2[simplified] split: if_split_asm) + lemma OPT_Suc: "OPT (Suc i) v = min (OPT i v) (Min {OPT i w + W v w | w. w \ n})" (is "?lhs = ?rhs") if "t \ n" proof - - have fin': "finite {xs. length xs \ i \ set xs \ {0..n}}" for i - by (auto intro: finite_subset[OF _ finite_lists_length_le[OF finite_atLeastAtMost]]) - have fin: "finite {weight (v # xs) |xs. length xs \ i \ set xs \ {0..n}}" - for v i using [[simproc add: finite_Collect]] by (auto intro: finite_subset[OF _ fin']) - have OPT_in: "OPT i v \ - {weight (v # xs) | xs. length xs + 1 \ i \ set xs \ {0..n}} \ - {if t = v then 0 else \}" - if "i > 0" for i v - using that unfolding OPT_def - by - (rule Min_in, auto 4 3 intro: finite_subset[OF _ fin, of _ v "Suc i"]) - - have "OPT i v \ OPT (Suc i) v" - unfolding OPT_def using fin by (auto 4 3 intro: Min_antimono) - have subs: - "(\y. y + W v w) ` {weight (w # xs) |xs. length xs + 1 \ i \ set xs \ {0..n}} - \ {weight (v # xs) |xs. length xs + 1 \ Suc i \ set xs \ {0..n}}" if \w \ n\ for v w - using \w \ n\ apply clarify - subgoal for _ _ xs - by (rule exI[where x = "w # xs"]) (auto simp: algebra_simps) - done - have "OPT i t + W v t \ OPT (Suc i) v" - unfolding OPT_def using subs[OF \t \ n\, of v] that - by (subst Min_add_right) - (auto 4 3 - simp: Bellman_Ford.weight_single - intro: exI[where x = "[]"] finite_subset[OF _ fin[of _ "Suc i"]] intro!: Min_antimono - ) - moreover have "OPT i w + W v w \ OPT (Suc i) v" if "w \ n" \w \ t\ \t \ v\ for w - unfolding OPT_def using subs[OF \w \ n\, of v] that - by (subst Min_add_right) - (auto 4 3 intro: finite_subset[OF _ fin[of _ "Suc i"]] intro!: Min_antimono) - moreover have "OPT i w + W t w \ OPT (Suc i) t" if "w \ n" \w \ t\ for w - unfolding OPT_def - apply (subst Min_add_right) - prefer 3 - using \w \ t\ - apply simp - apply (cases "i = 0") - apply (simp; fail) - using subs[OF \w \ n\, of t] - by (subst (2) Min_insert) - (auto 4 4 - intro: finite_subset[OF _ fin[of _ "Suc i"]] exI[where x = "[]"] intro!: Min_antimono - ) - ultimately have "Min {local.OPT i w + W v w |w. w \ n} \ OPT (Suc i) v" + have "OPT i w + W v w \ OPT (Suc i) v" if "w \ n" for w + using OPT_cases[of i w] + proof cases + case (path xs) + with \w \ n\ show ?thesis + by (subst OPT_def) (auto intro!: Min_le exI[where x = "w # xs"] simp: add.commute) + next + case sink + then show ?thesis + by (subst OPT_def) (auto intro!: Min_le exI[where x = "[]"]) + next + case unreachable + then show ?thesis + by simp + qed + then have "Min {OPT i w + W v w |w. w \ n} \ OPT (Suc i) v" by (auto intro!: Min.boundedI) - with \OPT i v \ _\ have "?lhs \ ?rhs" + moreover have "OPT i v \ OPT (Suc i) v" + unfolding OPT_def by (rule Min_antimono) auto + ultimately have "?lhs \ ?rhs" by simp - from OPT_in[of "Suc i" v] consider - "OPT (Suc i) v = \" | "t = v" "OPT (Suc i) v = 0" | - xs where "OPT (Suc i) v = weight (v # xs)" "length xs \ i" "set xs \ {0..n}" - by (auto split: if_split_asm) - then have "?lhs \ ?rhs" + from OPT_cases[of "Suc i" v] have "?lhs \ ?rhs" proof cases - case 1 + case (path xs) + note [simp] = path(1) + from path consider + (zero) "i = 0" "length xs = 0" | (new) "i > 0" "length xs = i" | (old) "length xs < i" + by (cases "length xs = i") auto + then show ?thesis + proof cases + case zero + with path have "OPT (Suc i) v = W v t" + by simp + also have "W v t = OPT i t + W v t" + unfolding OPT_def using \i = 0\ by auto + also have "\ \ Min {OPT i w + W v w |w. w \ n}" + using \t \ n\ by (auto intro: Min_le) + finally show ?thesis + by (rule min.coboundedI2) + next + case new + with \_ = i\ obtain u ys where [simp]: "xs = u # ys" + by (cases xs) auto + from path have "OPT i u \ weight (u # ys @ [t])" + unfolding OPT_def by (intro Min_le) auto + from path have "Min {OPT i w + W v w |w. w \ n} \ W v u + OPT i u" + by (intro Min_le) (auto simp: add.commute) + also from \OPT i u \ _\ have "\ \ OPT (Suc i) v" + by (simp add: add_left_mono) + finally show ?thesis + by (rule min.coboundedI2) + next + case old + with path have "OPT i v \ OPT (Suc i) v" + by (auto 4 3 intro: Min_le simp: OPT_def) + then show ?thesis + by (rule min.coboundedI1) + qed + next + case unreachable then show ?thesis by simp next - case 2 + case sink then have "OPT i v \ OPT (Suc i) v" - unfolding OPT_def using [[simproc add: finite_Collect]] - by (auto 4 4 intro: finite_subset[OF _ fin', of _ "Suc i"] intro!: Min_le) + unfolding OPT_def by auto then show ?thesis by (rule min.coboundedI1) - next - case xs: 3 - note [simp] = xs(1) - show ?thesis - proof (cases "length xs = i") - case True - show ?thesis - proof (cases "i = 0") - case True - with xs have "OPT (Suc i) v = W v t" - by simp - also have "W v t = OPT i t + W v t" - unfolding OPT_def using \i = 0\ by auto - also have "\ \ Min {OPT i w + W v w |w. w \ n}" - using \t \ n\ by (auto intro: Min_le) - finally show ?thesis - by (rule min.coboundedI2) - next - case False - with \_ = i\ have "xs \ []" - by auto - with xs have "weight xs \ OPT i (hd xs)" - unfolding OPT_def - by (intro Min_le[rotated] UnI1 CollectI exI[where x = "tl xs"]) - (auto 4 3 intro: finite_subset[OF _ fin, of _ "hd xs" "Suc i"] dest: list.set_sel(2)) - have "Min {OPT i w + W v w |w. w \ n} \ W v (hd xs) + OPT i (hd xs)" - using \set xs \ _\ \xs \ []\ by (force simp: add.commute intro: Min_le) - also have "\ \ W v (hd xs) + weight xs" - using \_ \ OPT i (hd xs)\ by (metis add_left_mono) - also from \xs \ []\ have "\ = OPT (Suc i) v" - by (cases xs) auto - finally show ?thesis - by (rule min.coboundedI2) - qed - next - case False - with xs have "OPT i v \ OPT (Suc i) v" - by (auto 4 4 intro: Min_le finite_subset[OF _ fin, of _ v "Suc i"] simp: OPT_def) - then show ?thesis - by (rule min.coboundedI1) - qed qed + with \?lhs \ ?rhs\ show ?thesis by (rule order.antisym) qed fun bf :: "nat \ nat \ int extended" where "bf 0 j = (if t = j then 0 else \)" | "bf (Suc k) j = min_list (bf k j # [W j i + bf k i . i \ [0 ..< Suc n]])" lemmas [simp del] = bf.simps -lemmas [simp] = bf.simps[unfolded min_list_fold] -thm bf.simps -thm bf.induct +lemmas bf_simps[simp] = bf.simps[unfolded min_list_fold] lemma bf_correct: "OPT i j = bf i j" if \t \ n\ proof (induction i arbitrary: j) case 0 then show ?case by (simp add: OPT_0) next case (Suc i) have *: "{bf i w + W j w |w. w \ n} = set (map (\w. W j w + bf i w) [0..t \ n\ show ?case by (simp add: OPT_Suc del: upt_Suc, subst Min.set_eq_fold[symmetric], auto simp: *) qed subsubsection \Functional Memoization\ memoize_fun bf\<^sub>m: bf with_memory dp_consistency_mapping monadifies (state) bf.simps text \Generated Definitions\ context includes state_monad_syntax begin thm bf\<^sub>m'.simps bf\<^sub>m_def end text \Correspondence Proof\ memoize_correct by memoize_prover print_theorems lemmas [code] = bf\<^sub>m.memoized_correct interpretation iterator "\ (x, y). x \ n \ y \ n" "\ (x, y). if y < n then (x, y + 1) else (x + 1, 0)" "\ (x, y). x * (n + 1) + y" by (rule table_iterator_up) interpretation bottom_up: dp_consistency_iterator_empty "\ (_::(nat \ nat, int extended) mapping). True" "\ (x, y). bf x y" "\ k. do {m \ State_Monad.get; State_Monad.return (Mapping.lookup m k :: int extended option)}" "\ k v. do {m \ State_Monad.get; State_Monad.set (Mapping.update k v m)}" "\ (x, y). x \ n \ y \ n" "\ (x, y). if y < n then (x, y + 1) else (x + 1, 0)" "\ (x, y). x * (n + 1) + y" Mapping.empty .. definition "iter_bf = iter_state (\ (x, y). bf\<^sub>m' x y)" lemma iter_bf_unfold[code]: "iter_bf = (\ (i, j). (if i \ n \ j \ n then do { bf\<^sub>m' i j; iter_bf (if j < n then (i, j + 1) else (i + 1, 0)) } else State_Monad.return ()))" unfolding iter_bf_def by (rule ext) (safe, clarsimp simp: iter_state_unfold) lemmas bf_memoized = bf\<^sub>m.memoized[OF bf\<^sub>m.crel] lemmas bf_bottom_up = bottom_up.memoized[OF bf\<^sub>m.crel, folded iter_bf_def] -thm bf\<^sub>m'.simps bf_memoized +definition + "bellman_ford \ + do { + _ \ iter_bf (n, n); + xs \ State_Main.map\<^sub>T' (\i. bf\<^sub>m' n i) [0.. State_Main.map\<^sub>T' (\i. bf\<^sub>m' (n + 1) i) [0.. + do { + _ \ iter_bf (n, n); + (\\xs. \\ys. State_Monad.return (if xs = ys then Some xs else None)\ + . (State_Main.map\<^sub>T . \\i. bf\<^sub>m' (n + 1) i\ . \[0..)\) + . (State_Main.map\<^sub>T . \\i. bf\<^sub>m' n i\ . \[0..) + }" + unfolding + State_Monad_Ext.fun_app_lifted_def bellman_ford_def State_Main.map\<^sub>T_def bind_left_identity + . + +end + subsubsection \Imperative Memoization\ context fixes mem :: "nat ref \ nat ref \ int extended option array ref \ int extended option array ref" assumes mem_is_init: "mem = result_of (init_state (n + 1) 1 0) Heap.empty" begin lemma [intro]: "dp_consistency_heap_array_pair' (n + 1) fst snd id 1 0 mem" by (standard; simp add: mem_is_init injective_def) interpretation iterator "\ (x, y). x \ n \ y \ n" "\ (x, y). if y < n then (x, y + 1) else (x + 1, 0)" "\ (x, y). x * (n + 1) + y" by (rule table_iterator_up) lemma [intro]: "dp_consistency_heap_array_pair_iterator (n + 1) fst snd id 1 0 mem (\ (x, y). if y < n then (x, y + 1) else (x + 1, 0)) (\ (x, y). x * (n + 1) + y) (\ (x, y). x \ n \ y \ n)" by (standard; simp add: mem_is_init injective_def) memoize_fun bf\<^sub>h: bf with_memory (default_proof) dp_consistency_heap_array_pair_iterator where size = "n + 1" - and key1="fst :: nat \ nat \ nat" and key2="snd :: nat \ nat \ nat" - and k1="1 :: nat" and k2="0 :: nat" + and key1 = "fst :: nat \ nat \ nat" and key2 = "snd :: nat \ nat \ nat" + and k1 = "1 :: nat" and k2 = "0 :: nat" and to_index = "id :: nat \ nat" and mem = mem and cnt = "\ (x, y). x \ n \ y \ n" and nxt = "\ (x :: nat, y). if y < n then (x, y + 1) else (x + 1, 0)" and sizef = "\ (x, y). x * (n + 1) + y" monadifies (heap) bf.simps memoize_correct by memoize_prover lemmas memoized_empty = bf\<^sub>h.memoized_empty[OF bf\<^sub>h.consistent_DP_iter_and_compute[OF bf\<^sub>h.crel]] lemmas iter_heap_unfold = iter_heap_unfold end (* Fixed Memory *) + +subsubsection \Detecting Negative Cycles\ + +definition + "shortest v = ( + Inf ( + {weight (v # xs @ [t]) | xs. set xs \ {0..n}} \ + {if t = v then 0 else \} + ) + )" + +definition + "is_path xs \ weight (xs @ [t]) < \" + +definition + "has_negative_cycle \ + \xs a ys. set (a # xs @ ys) \ {0..n} \ weight (a # xs @ [a]) < 0 \ is_path (a # ys)" + +definition + "reaches a \ \xs. is_path (a # xs) \ a \ n \ set xs \ {0..n}" + +lemma fold_sum_aux': + assumes "\u \ set (a # xs). \v \ set (xs @ [b]). f v + W u v \ f u" + shows "sum_list (map f (a # xs)) \ sum_list (map f (xs @ [b])) + weight (a # xs @ [b])" + using assms + by (induction xs arbitrary: a; simp) + (smt ab_semigroup_add_class.add_ac(1) add.left_commute add_mono) + +lemma fold_sum_aux: + assumes "\u \ set (a # xs). \v \ set (a # xs). f v + W u v \ f u" + shows "sum_list (map f (a # xs @ [a])) \ sum_list (map f (a # xs @ [a])) + weight (a # xs @ [a])" + using fold_sum_aux'[of a xs a f] assms + by auto (metis (no_types, hide_lams) add.assoc add.commute add_left_mono) + +context +begin + +private definition "is_path2 xs \ weight xs < \" + +private lemma is_path2_remove_cycle: + assumes "is_path2 (as @ a # bs @ a # cs)" + shows "is_path2 (as @ a # cs)" +proof - + have "weight (as @ a # bs @ a # cs) = + weight (as @ [a]) + weight (a # bs @ [a]) + weight (a # cs)" + by (metis Bellman_Ford.weight_append append_Cons append_assoc) + with assms have "weight (as @ [a]) < \" "weight (a # cs) < \" + unfolding is_path2_def + by (simp, metis Pinf_add_right antisym less_extended_simps(4) not_less add.commute)+ + then show ?thesis + unfolding is_path2_def by (subst weight_append) (rule add_lt_infI) +qed + +private lemma is_path_eq: + "is_path xs \ is_path2 (xs @ [t])" + unfolding is_path_def is_path2_def .. + +lemma is_path_remove_cycle: + assumes "is_path (as @ a # bs @ a # cs)" + shows "is_path (as @ a # cs)" + using assms unfolding is_path_eq by (simp add: is_path2_remove_cycle) + +lemma is_path_remove_cycle2: + assumes "is_path (as @ t # cs)" + shows "is_path as" + using assms unfolding is_path_eq by (simp add: is_path2_remove_cycle) + +end (* private lemmas *) + +lemma is_path_shorten: + assumes "is_path (i # xs)" "i \ n" "set xs \ {0..n}" "t \ n" "t \ i" + obtains xs where "is_path (i # xs)" "i \ n" "set xs \ {0..n}" "length xs < n" +proof (cases "length xs < n") + case True + with assms show ?thesis + by (auto intro: that) +next + case False + then have "length xs \ n" + by auto + with assms(1,3) show ?thesis + proof (induction "length xs" arbitrary: xs rule: less_induct) + case less + then have "length (i # xs @ [t]) > card ({0..n})" + by auto + moreover from less.prems \i \ n\ \t \ n\ have "set (i # xs @ [t]) \ {0..n}" + by auto + ultimately obtain a as bs cs where *: "i # xs @ [t] = as @ a # bs @ a # cs" + by (elim list_pidgeonhole) auto + obtain ys where ys: "is_path (i # ys)" "length ys < length xs" "set (i # ys) \ {0..n}" + apply atomize_elim + using * + proof (cases rule: path_eq_cycleE) + case Nil_Nil + with \t \ i\ show "\ys. is_path (i # ys) \ length ys < length xs \ set (i # ys) \ {0..n}" + by auto + next + case (Nil_Cons cs') + then show "\ys. is_path (i # ys) \ length ys < length xs \ set (i # ys) \ {0..n}" + using \set (i # xs @ [t]) \ {0..n}\ \is_path (i # xs)\ is_path_remove_cycle[of "[]"] + by - (rule exI[where x = cs'], simp) + next + case (Cons_Nil as') + then show "\ys. is_path (i # ys) \ length ys < length xs \ set (i # ys) \ {0..n}" + using \set (i # xs @ [t]) \ {0..n}\ \is_path (i # xs)\ + by - (rule exI[where x = as'], auto intro: is_path_remove_cycle2) + next + case (Cons_Cons as' cs') + then show "\ys. is_path (i # ys) \ length ys < length xs \ set (i # ys) \ {0..n}" + using \set (i # xs @ [t]) \ {0..n}\ \is_path (i # xs)\ is_path_remove_cycle[of "i # as'"] + by - (rule exI[where x = "as' @ a # cs'"], auto) + qed + then show ?thesis + by (cases "n \ length ys") (auto intro: that less) + qed +qed + +lemma reaches_non_inf_path: + assumes "reaches i" "i \ n" "t \ n" + shows "OPT n i < \" +proof (cases "t = i") + case True + with \i \ n\ \t \ n\ have "OPT n i \ 0" + unfolding OPT_def + by (auto intro: Min_le simp: finite_lists_length_le2[simplified]) + then show ?thesis + using less_linear by (fastforce simp: zero_extended_def) +next + case False + from assms(1) obtain xs where "is_path (i # xs)" "i \ n" "set xs \ {0..n}" + unfolding reaches_def by safe + then obtain xs where xs: "is_path (i # xs)" "i \ n" "set xs \ {0..n}" "length xs < n" + using \t \ i\ \t \ n\ by (auto intro: is_path_shorten) + then have "weight (i # xs @ [t]) < \" + unfolding is_path_def by auto + with xs(2-) show ?thesis + unfolding OPT_def + by (elim order.strict_trans1[rotated]) + (auto simp: setcompr_eq_image finite_lists_length_le2[simplified]) +qed + +lemma OPT_sink_le_0: + "OPT i t \ 0" + unfolding OPT_def by (auto simp: finite_lists_length_le2[simplified]) + +lemma is_path_appendD: + assumes "is_path (as @ a # bs)" + shows "is_path (a # bs)" + using assms weight_append[of as a "bs @ [t]"] unfolding is_path_def + by simp (metis Pinf_add_right add.commute less_extended_simps(4) not_less_iff_gr_or_eq) + +lemma has_negative_cycleI: + assumes "set (a # xs @ ys) \ {0..n}" "weight (a # xs @ [a]) < 0" "is_path (a # ys)" + shows has_negative_cycle + using assms unfolding has_negative_cycle_def by auto + +lemma OPT_cases2: + obtains (path) xs where + "v \ t" "OPT i v \ \" "OPT i v = weight (v # xs @ [t])" "length xs + 1 \ i" "set xs \ {0..n}" + | (unreachable) "v \ t" "OPT i v = \" + | (sink) "v = t" "OPT i v \ 0" + unfolding OPT_def + using Min_in[of "{weight (v # xs @ [t]) |xs. length xs + 1 \ i \ set xs \ {0..n}} + \ {if t = v then 0 else \}"] + by (cases "v = t"; force simp: finite_lists_length_le2[simplified] split: if_split_asm) + +lemma shortest_le_OPT: + assumes "v \ n" + shows "shortest v \ OPT i v" + unfolding OPT_def shortest_def + apply (subst Min_Inf) + apply (simp add: setcompr_eq_image finite_lists_length_le2[simplified]; fail)+ + apply (rule Inf_superset_mono) + apply auto + done + + +context + assumes W_wellformed: "\i \ n. \j \ n. W i j > -\" + assumes "t \ n" +begin + +lemma weight_not_minfI: + "-\ < weight xs" if "set xs \ {0..n}" "xs \ []" + using that using W_wellformed \t \ n\ + by (induction xs rule: induct_list012) (auto intro: add_gt_minfI simp: zero_extended_def) + +lemma OPT_not_minfI: + "OPT n i > -\" if "i \ n" +proof - + have "OPT n i \ + {weight (i # xs @ [t]) |xs. length xs + 1 \ n \ set xs \ {0..n}} \ {if t = i then 0 else \}" + unfolding OPT_def + by (rule Min_in) (auto simp: setcompr_eq_image finite_lists_length_le2[simplified]) + with that \t \ n\ show ?thesis + by (auto 4 3 intro!: weight_not_minfI simp: zero_extended_def) +qed + +theorem detects_cycle: + assumes has_negative_cycle + shows "\i \ n. OPT (n + 1) i < OPT n i" +proof - + from assms \t \ n\ obtain xs a ys where cycle: + "a \ n" "set xs \ {0..n}" "set ys \ {0..n}" + "weight (a # xs @ [a]) < 0" "is_path (a # ys)" + unfolding has_negative_cycle_def by clarsimp + then have "reaches a" + unfolding reaches_def by auto + have reaches: "reaches x" if "x \ set xs" for x + proof - + from that obtain as bs where "xs = as @ x # bs" + by atomize_elim (rule split_list) + with cycle have "weight (x # bs @ [a]) < \" + using weight_append[of "a # as" x "bs @ [a]"] + by simp (metis Pinf_add_right Pinf_le add.commute less_eq_extended.simps(2) not_less) + with \reaches a\ show ?thesis + unfolding reaches_def is_path_def + apply clarsimp + subgoal for cs + using weight_append[of "x # bs" a "cs @ [t]"] cycle(2) \xs = _\ + by - (rule exI[where x = "bs @ [a] @ cs"], auto intro: add_lt_infI) + done + qed + let ?S = "sum_list (map (OPT n) (a # xs @ [a]))" + obtain u v where "u \ n" "v \ n" "OPT n v + W u v < OPT n u" + proof (atomize_elim, rule ccontr) + assume "\u v. u \ n \ v \ n \ OPT n v + W u v < OPT n u" + then have "?S \ ?S + weight (a # xs @ [a])" + using cycle(1-3) by (subst fold_sum_aux; fastforce simp: subset_eq) + moreover have "?S > -\" + using cycle(1-4) by (intro sum_list_not_minfI, auto intro!: OPT_not_minfI) + moreover have "?S < \" + using reaches \t \ n\ cycle(1,2) + by (intro sum_list_not_infI) (auto intro: reaches_non_inf_path \reaches a\ simp: subset_eq) + ultimately have "weight (a # xs @ [a]) \ 0" + by (simp add: le_add_same_cancel1) + with \weight _ < 0\ show False + by simp + qed + then show ?thesis + by - + (rule exI[where x = u], + auto 4 4 intro: Min.coboundedI min.strict_coboundedI2 elim: order.strict_trans1[rotated] + simp: OPT_Suc[OF \t \ n\]) +qed + +corollary bf_detects_cycle: + assumes has_negative_cycle + shows "\i \ n. bf (n + 1) i < bf n i" + using detects_cycle[OF assms] unfolding bf_correct[OF \t \ n\] . + +lemma shortest_cases: + assumes "v \ n" + obtains (path) xs where "shortest v = weight (v # xs @ [t])" "set xs \ {0..n}" + | (sink) "v = t" "shortest v = 0" + | (unreachable) "v \ t" "shortest v = \" + | (negative_cycle) "shortest v = -\" "\x. \xs. set xs \ {0..n} \ weight (v # xs @ [t]) < Fin x" +proof - + let ?S = "{weight (v # xs @ [t]) | xs. set xs \ {0..n}} \ {if t = v then 0 else \}" + have "?S \ {}" + by auto + have Minf_lowest: False if "-\ < a" "-\ = a" for a :: "int extended" + using that by auto + show ?thesis + proof (cases "shortest v") + case (Fin x) + then have "-\ \ ?S" "bdd_below (Fin -` ?S)" "?S \ {\}" "x = Inf (Fin -` ?S)" + unfolding shortest_def Inf_extended_def by (auto split: if_split_asm) + from this(1-3) have "x \ Fin -` ?S" + unfolding \x = _\ + by (intro Inf_int_in, auto simp: zero_extended_def) + (smt empty_iff extended.exhaust insertI2 mem_Collect_eq vimage_eq) + with \shortest v = _\ show ?thesis + unfolding vimage_eq by (auto split: if_split_asm intro: that) + next + case Pinf + with \?S \ {}\ have "t \ v" + unfolding shortest_def Inf_extended_def by (auto split: if_split_asm) + with \_ = \\ show ?thesis + by (auto intro: that) + next + case Minf + then have "?S \ {}" "?S \ {\}" "-\ \ ?S \ \ bdd_below (Fin -` ?S)" + unfolding shortest_def Inf_extended_def by (auto split: if_split_asm) + from this(3) have "\x. \xs. set xs \ {0..n} \ weight (v # xs @ [t]) < Fin x" + proof + assume "-\ \ ?S" + with weight_not_minfI have False + using \v \ n\ \t \ n\ by (auto split: if_split_asm elim: Minf_lowest[rotated]) + then show ?thesis .. + next + assume "\ bdd_below (Fin -` ?S)" + show ?thesis + proof + fix x :: int + let ?m = "min x (-1)" + from \\ bdd_below _\ obtain m where "Fin m \ ?S" "m < ?m" + unfolding bdd_below_def by - (simp, drule spec[of _ "?m"], force) + then show "\xs. set xs \ {0..n} \ weight (v # xs @ [t]) < Fin x" + by (auto split: if_split_asm simp: zero_extended_def) (metis less_extended_simps(1))+ + qed + qed + with \shortest v = _\ show ?thesis + by (auto intro: that) + qed +qed + +lemma simple_paths: + assumes "\ has_negative_cycle" "weight (v # xs @ [t]) < \" "set xs \ {0..n}" "v \ n" + obtains ys where + "weight (v # ys @ [t]) \ weight (v # xs @ [t])" "set ys \ {0..n}" "length ys < n" | "v = t" + using assms(2-) +proof (atomize_elim, induction "length xs" arbitrary: xs rule: less_induct) + case (less ys) + note ys = less.prems(1,2) + note IH = less.hyps + have path: "is_path (v # ys)" + using is_path_def not_less_iff_gr_or_eq ys(1) by fastforce + show ?case + proof (cases "length ys \ n") + case True + with ys \v \ n\ \t \ n\ obtain a as bs cs where "v # ys @ [t] = as @ a # bs @ a # cs" + by - (rule list_pidgeonhole[of "v # ys @ [t]" "{0..n}"], auto) + then show ?thesis + proof (cases rule: path_eq_cycleE) + case Nil_Nil + then show ?thesis + by simp + next + case (Nil_Cons cs') + then have *: "weight (v # ys @ [t]) = weight (a # bs @ [a]) + weight (a # cs' @ [t])" + by (simp add: weight_append[of "a # bs" a "cs' @ [t]", simplified]) + show ?thesis + proof (cases "weight (a # bs @ [a]) < 0") + case True + with Nil_Cons \set ys \ _\ path show ?thesis + using assms(1) by (force intro: has_negative_cycleI[of a bs ys]) + next + case False + then have "weight (a # bs @ [a]) \ 0" + by auto + with * ys have "weight (a # cs' @ [t]) \ weight (v # ys @ [t])" + using add_mono not_le by fastforce + with Nil_Cons \length ys \ n\ ys show ?thesis + using IH[of cs'] by simp (meson le_less_trans order_trans) + qed + next + case (Cons_Nil as') + with ys have *: "weight (v # ys @ [t]) = weight (v # as' @ [t]) + weight (a # bs @ [a])" + using weight_append[of "v # as'" t "bs @ [t]"] by simp + show ?thesis + proof (cases "weight (a # bs @ [a]) < 0") + case True + with Cons_Nil \set ys \ _\ path assms(1) show ?thesis + using is_path_appendD[of "v # as'"] by (force intro: has_negative_cycleI[of a bs bs]) + next + case False + then have "weight (a # bs @ [a]) \ 0" + by auto + with * ys(1) have "weight (v # as' @ [t]) \ weight (v # ys @ [t])" + using add_left_mono by fastforce + with Cons_Nil \length ys \ n\ \v \ n\ ys show ?thesis + using IH[of as'] by simp (meson le_less_trans order_trans) + qed + next + case (Cons_Cons as' cs') + with ys have *: "weight (v # ys @ [t]) = weight (v # as' @ a # cs' @ [t]) + weight (a # bs @ [a])" + using + weight_append[of "v # as'" a "bs @ a # cs' @ [t]"] + weight_append[of "a # bs" a "cs' @ [t]"] + weight_append[of "v # as'" a "cs' @ [t]"] + by (simp add: algebra_simps) + show ?thesis + proof (cases "weight (a # bs @ [a]) < 0") + case True + with Cons_Cons \set ys \ _\ path assms(1) show ?thesis + using is_path_appendD[of "v # as'"] + by (force intro: has_negative_cycleI[of a bs "bs @ a # cs'"]) + next + case False + then have "weight (a # bs @ [a]) \ 0" + by auto + with * ys have "weight (v # as' @ a # cs' @ [t]) \ weight (v # ys @ [t])" + using add_left_mono by fastforce + with Cons_Cons \v \ n\ ys show ?thesis + using is_path_remove_cycle2 IH[of "as' @ a # cs'"] + by simp (meson le_less_trans order_trans) + qed + qed + next + case False + with \set ys \ _\ show ?thesis + by auto + qed +qed + +theorem shorter_than_OPT_n_has_negative_cycle: + assumes "shortest v < OPT n v" "v \ n" + shows has_negative_cycle +proof - + from assms obtain ys where ys: + "weight (v # ys @ [t]) < OPT n v" "set ys \ {0..n}" + apply (cases rule: OPT_cases2[of v n]; cases rule: shortest_cases[OF \v \ n\]; simp) + apply (metis uminus_extended.cases) + using less_extended_simps(2) less_trans apply blast + apply (metis less_eq_extended.elims(2) less_extended_def zero_extended_def) + done + show ?thesis + proof (cases "v = t") + case True + with ys \t \ n\ show ?thesis + using OPT_sink_le_0[of n] unfolding has_negative_cycle_def is_path_def + using less_extended_def by force + next + case False + show ?thesis + proof (rule ccontr) + assume "\ has_negative_cycle" + with False False ys \v \ n\ obtain xs where + "weight (v # xs @ [t]) \ weight (v # ys @ [t])" "set xs \ {0..n}" "length xs < n" + using less_extended_def by (fastforce elim!: simple_paths[of v ys]) + then have "OPT n v \ weight (v # xs @ [t])" + unfolding OPT_def by (intro Min_le) auto + with \_ \ weight (v # ys @ [t])\ \weight (v # ys @ [t]) < OPT n v\ show False + by simp + qed + qed +qed + +corollary detects_cycle_has_negative_cycle: + assumes "OPT (n + 1) v < OPT n v" "v \ n" + shows has_negative_cycle + using assms shortest_le_OPT[of v "n + 1"] shorter_than_OPT_n_has_negative_cycle[of v] by auto + +corollary bellman_ford_detects_cycle: + "has_negative_cycle \ (\v \ n. OPT (n + 1) v < OPT n v)" + using detects_cycle_has_negative_cycle detects_cycle by blast + +corollary bellman_ford_shortest_paths: + assumes "\ has_negative_cycle" + shows "\v \ n. bf n v = shortest v" +proof - + have "OPT n v \ shortest v" if "v \ n" for v + using that assms shorter_than_OPT_n_has_negative_cycle[of v] by force + then show ?thesis + unfolding bf_correct[OF \t \ n\, symmetric] + by (safe, rule order.antisym) (auto elim: shortest_le_OPT) +qed + +lemma OPT_mono: + "OPT m v \ OPT n v" if \v \ n\ \n \ m\ + using that unfolding OPT_def by (intro Min_antimono) auto + +corollary bf_fix: + assumes "\ has_negative_cycle" "m \ n" + shows "\v \ n. bf m v = bf n v" +proof (intro allI impI) + fix v assume "v \ n" + from \v \ n\ \n \ m\ have "shortest v \ OPT m v" + by (simp add: shortest_le_OPT) + moreover from \v \ n\ \n \ m\ have "OPT m v \ OPT n v" + by (rule OPT_mono) + moreover from \v \ n\ assms have "OPT n v \ shortest v" + using shorter_than_OPT_n_has_negative_cycle[of v] by force + ultimately show "bf m v = bf n v" + unfolding bf_correct[OF \t \ n\, symmetric] by simp +qed + +lemma bellman_ford_correct': + "bf\<^sub>m.crel_vs (=) (if has_negative_cycle then None else Some (map shortest [0..m' = bf\<^sub>m.crel[unfolded bf\<^sub>m.consistentDP_def, THEN rel_funD, + of "(m, x)" "(m, y)" for m x y, unfolded prod.case] + have "?l = ?r" + unfolding Wrap_def App_def Let_def + supply [simp del] = bf_simps + apply (simp; safe) + using bf_detects_cycle apply (auto elim: nat_le_cases; fail) + apply (simp add: bellman_ford_shortest_paths; fail)+ + apply (simp add: bf_fix[rule_format, symmetric])+ + done + show ?thesis + unfolding bellman_ford_alt_def \?l = ?r\ + apply (rule bf\<^sub>m.crel_vs_bind_ignore[rotated]) + apply (rule bottom_up.consistent_crel_vs_iterate_state[OF bf\<^sub>m.crel, folded iter_bf_def]) + apply (subst Transfer.Rel_def[symmetric]) + apply (rule bf\<^sub>m.crel_vs_fun_app[of "list_all2 (=)"]) + defer + apply (rule bf\<^sub>m.crel_vs_return_ext) + apply (rule bf\<^sub>m.rel_fun2) + defer + apply (rule bf\<^sub>m.crel_vs_fun_app[of "list_all2 (=)"]) + defer + apply (rule bf\<^sub>m.crel_vs_return_ext) + apply (rule bf\<^sub>m.rel_fun2) + defer + apply (rule bf\<^sub>m.crel_vs_return_ext) + apply (rule transfer_raw) + apply (rule is_equality_eq) + apply (rule bf\<^sub>m.crel_vs_fun_app[of "list_all2 (=)"]) + apply (rule bf\<^sub>m.crel_vs_return) + defer + apply (rule bf\<^sub>m.crel_vs_fun_app) + prefer 2 + apply (subst Transfer.Rel_def) + apply (rule bf\<^sub>m.map\<^sub>T_transfer) + prefer 3 + + apply (rule bf\<^sub>m.crel_vs_fun_app[of "list_all2 (=)"]) + apply (rule bf\<^sub>m.crel_vs_return) + defer + apply (rule bf\<^sub>m.crel_vs_fun_app) + prefer 2 + apply (subst Transfer.Rel_def) + apply (rule bf\<^sub>m.map\<^sub>T_transfer) + + subgoal + by (intro bf\<^sub>m.crel_vs_return Rel_abs; (unfold Transfer.Rel_def)?; rule crel_bf\<^sub>m')+ simp + + subgoal + apply (rule bf\<^sub>m.crel_vs_return) + apply (rule Rel_abs) + unfolding Transfer.Rel_def + apply (rule crel_bf\<^sub>m') + apply simp + done + unfolding Rel_def list.rel_eq by (rule is_equality_eq HOL.refl)+ +qed + +theorem bellman_ford_correct: + "fst (run_state bellman_ford Mapping.empty) = + (if has_negative_cycle then None else Some (map shortest [0..m.cmem_empty bellman_ford_correct'[unfolded bf\<^sub>m.crel_vs_def, rule_format, of Mapping.empty] + unfolding bf\<^sub>m.crel_vs_def by auto + +end (* Wellformedness *) + end (* Final Node *) end (* Bellman Ford *) subsubsection \Extracting an Executable Constant for the Imperative Implementation\ ground_function (prove_termination) bf\<^sub>h'_impl: bf\<^sub>h'.simps lemma bf\<^sub>h'_impl_def: fixes n :: nat fixes mem :: "nat ref \ nat ref \ int extended option array ref \ int extended option array ref" assumes mem_is_init: "mem = result_of (init_state (n + 1) 1 0) Heap.empty" shows "bf\<^sub>h'_impl n w t mem = bf\<^sub>h' n w t mem" proof - have "bf\<^sub>h'_impl n w t mem i j = bf\<^sub>h' n w t mem i j" for i j by (induction rule: bf\<^sub>h'.induct[OF mem_is_init]; simp add: bf\<^sub>h'.simps[OF mem_is_init]; solve_cong simp ) then show ?thesis by auto qed definition "iter_bf_heap n w t mem = iterator_defs.iter_heap (\(x, y). x \ n \ y \ n) (\(x, y). if y < n then (x, y + 1) else (x + 1, 0)) (\(x, y). bf\<^sub>h'_impl n w t mem x y)" lemma iter_bf_heap_unfold[code]: "iter_bf_heap n w t mem = (\ (i, j). (if i \ n \ j \ n then do { bf\<^sub>h'_impl n w t mem i j; iter_bf_heap n w t mem (if j < n then (i, j + 1) else (i + 1, 0)) } else Heap_Monad.return ()))" unfolding iter_bf_heap_def by (rule ext) (safe, simp add: iter_heap_unfold) definition "bf_impl n w t i j = do { mem \ (init_state (n + 1) (1::nat) (0::nat) :: (nat ref \ nat ref \ int extended option array ref \ int extended option array ref) Heap); iter_bf_heap n w t mem (0, 0); bf\<^sub>h'_impl n w t mem i j }" lemma bf_impl_correct: "bf n w t i j = result_of (bf_impl n w t i j) Heap.empty" using memoized_empty[OF HOL.refl, of n w t "(i, j)"] by (simp add: execute_bind_success[OF succes_init_state] bf_impl_def bf\<^sub>h'_impl_def iter_bf_heap_def ) subsubsection \Test Cases\ definition "G\<^sub>1_list = [[(1 :: nat,-6 :: int), (2,4), (3,5)], [(3,10)], [(3,2)], []]" definition + "G\<^sub>2_list = [[(1 :: nat,-6 :: int), (2,4), (3,5)], [(3,10)], [(3,2)], [(0, -5)]]" + +definition + "G\<^sub>3_list = [[(1 :: nat,-1 :: int), (2,2)], [(2,5), (3,4)], [(3,2), (4,3)], [(2,-2), (4,2)], []]" + +definition "graph_of a i j = case_option \ (Fin o snd) (List.find (\ p. fst p = j) (a !! i))" definition "test_bf = bf_impl 3 (graph_of (IArray G\<^sub>1_list)) 3 3 0" code_reflect Test functions test_bf text \One can see a trace of the calls to the memory in the output\ ML \Test.test_bf ()\ lemma bottom_up_alt[code]: "bf n W t i j = fst (run_state (iter_bf n W t (0, 0) \ (\_. bf\<^sub>m' n W t i j)) Mapping.empty)" using bf_bottom_up by auto definition "bf_ia n W t i j = (let W' = graph_of (IArray W) in fst (run_state (iter_bf n W' t (i, j) \ (\_. bf\<^sub>m' n W' t i j)) Mapping.empty) )" value "fst (run_state (bf\<^sub>m' 3 (graph_of (IArray G\<^sub>1_list)) 3 3 0) Mapping.empty)" +value "fst (run_state (bellman_ford 3 (graph_of (IArray G\<^sub>1_list)) 3) Mapping.empty)" + +value "fst (run_state (bellman_ford 3 (graph_of (IArray G\<^sub>2_list)) 3) Mapping.empty)" + +value "fst (run_state (bellman_ford 4 (graph_of (IArray G\<^sub>3_list)) 4) Mapping.empty)" + value "bf 3 (graph_of (IArray G\<^sub>1_list)) 3 3 0" -end (* Theory *) +end (* Theory *) \ No newline at end of file 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 \Misc\ lemma append_iff_take_drop: "w = u@v \ (\k \ {0..length w}. u = take k w \ 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 \ [] \ v \ [] \ w = u@v \ (\k \ {1..length w - 1}. u = take k w \ v = drop k w)" by(auto simp: append_iff_take_drop) subsubsection \Definitions\ datatype ('n, 't) rhs = NN 'n 'n | T 't type_synonym ('n, 't) prods = "('n \ ('n, 't) rhs) list" context fixes P :: "('n :: heap, 't) prods" begin inductive yield :: "'n \ 't list \ bool" where "(A, T a) \ set P \ yield A [a]" | "\ (A, NN B C) \ set P; yield B u; yield C v \ \ yield A (u@v)" lemma yield_not_Nil: "yield A w \ w \ []" by (induction rule: yield.induct) auto lemma yield_eq1: "yield A [a] \ (A, T a) \ 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 \ (\B u C v. yield B u \ yield C v \ w = u@v \ (A, NN B C) \ 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 \ 'n list" where "cyk [] = []" | "cyk [a] = [A . (A, T a') <- P, a'= a]" | "cyk w = [A. k <- [1.. 2 \ set(cyk w) = (\k \ {1..length w - 1}. \B \ set(cyk (take k w)). \C \ set(cyk (drop k w)). {A. (A, NN B C) \ 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) = (\k\{1..length ?w-1}. {N. \A B. (N, NN A B) \ set P \ yield A (take k ?w) \ yield B (drop k ?w)})" by(auto simp add:"3.IH" simp del:upt_Suc) also have "... = {N. \A B. (N, NN A B) \ set P \ (\u v. yield A u \ yield B v \ ?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 \ nat * nat \ '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..xb\set P. {A. (A, NN B C) = xb}) = {A. (A, NN B C) \ set P}" by auto lemma cyk2_eq_cyk: "i+n \ length w \ 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 \ 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 \ 't" begin fun cyk_ix :: "nat * nat \ '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..Correctness Proof\ lemma cyk_ix_simp2: "set(cyk_ix (i,Suc(Suc n))) = (\k \ {1..Suc n}. \B \ set(cyk_ix (i,k)). \C \ set(cyk_ix (i+k,n+2-k)). {A. (A, NN B C) \ set P})" by(simp add: atLeastLessThanSuc_atLeastAtMost set_aux del: upt_Suc) declare cyk_ix.simps(3)[simp del] -abbreviation "slice f i j \ map f [i.. map f [i.. [] \ v \ [] \ slice w i j = u @ v \ (\k. 1 \ k \ k \ j-i-1 \ slice w i (i + k) = u \ 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)) = (\k\{1..Suc m}. {N. \A B. (N, NN A B) \ set P \ yield A (slice w i (i+k)) \ yield B (slice w (i+k) (i+?n))})" by(auto simp add: 3 cyk_ix_simp2 simp del: upt_Suc) also have "... = {N. \A B. (N, NN A B) \ set P \ (\u v. yield A u \ yield B v \ 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 \Functional Memoization\ 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 \Imperative Memoization\ 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 \ 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 \ 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 (\i. w ! i) (0,length w)" definition "CYK_ix_impl S w n = do {R \ cyk_ix_impl w n 0 n; return (S \ 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 \Functional Test Case\ 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 (\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 (\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 \Imperative Test Case\ definition "cyk_ia' P w = (let a = IArray w in cyk_ix_impl P (\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 \List.map (fn f => f ()) Test.test\ 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,409 +1,409 @@ 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 \ 'b::order) \ 'a list \ 'a" where "argmin f [a] = a" | "argmin f (a#as) = (let m = argmin f as in if f a \ f m then a else m)" (* end rm *) (* Ex: Optimization of argmin *) fun argmin2 :: "('a \ 'b::order) \ 'a list \ '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 \ m then (a, fa) else (am,m))" subsubsection "Edit Distance" datatype 'a ed = Copy | Repl 'a | Ins 'a | Del fun edit :: "'a ed list \ 'a list \ '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 \ length [e <- es. e \ Copy]" subsubsection "Minimum Edit Sequence" fun min_eds :: "'a list \ 'a list \ '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 = [] \ xs = [] \ 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 \ length ys \ cost es" apply(induction es "[]::'a list" arbitrary: ys rule: edit.induct) apply auto done lemma if_edit_eq_Nil: "edit es xs = [] \ length xs \ cost es" by (induction es xs rule: edit.induct) auto lemma min_eds_minimal: "edit es xs = ys \ cost(min_eds xs ys) \ 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 \ 'a list \ 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 \ 'a list \ '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) \ 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) \ 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 \ nat" where "min_ed_ix' (i,j) = (if i \ m then if j \ n then 0 else 1 + min_ed_ix' (i,j+1) else if j \ 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(\(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 \ 'a" fixes m n :: nat begin function (sequential) min_ed_ix :: "nat \ nat \ nat" where "min_ed_ix (i, j) = (if i \ m then if j \ n then 0 else n-j else if j \ 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(\(i,j). (m - i) + (n - j))") auto subsubsection \Functional Memoization\ 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 \Imperative Memoization\ context fixes mem :: "nat ref \ nat ref \ nat option array ref \ nat option array ref" assumes mem_is_init: "mem = result_of (init_state (n + 1) m (m + 1)) Heap.empty" begin interpretation iterator "\ (x, y). x \ m \ y \ n \ x > 0" "\ (x, y). if y > 0 then (x, y - 1) else (x - 1, n)" "\ (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 (\ (x, y). if y > 0 then (x, y - 1) else (x - 1, n)) (\ (x, y). (m - x) * (n + 1) + (n - y)) (\ (x, y). x \ m \ y \ n \ 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 \ nat \ nat" and key2="snd :: nat \ nat \ nat" and k1="m :: nat" and k2="m + 1 :: nat" and to_index = "id :: nat \ nat" and mem = mem and cnt = "\ (x, y). x \ m \ y \ n \ x > 0" and nxt = "\ (x::nat, y). if y > 0 then (x, y - 1) else (x - 1, n)" and sizef = "\ (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 \Test Cases\ -abbreviation "slice xs i j \ map xs [i.. map xs [i..Functional Test Cases\ definition "min_ed_list xs ys = min_ed_ix (\i. xs!i) (\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 (\i. a!!i) (\i. b!!i) (length xs) (length ys) (0,0))" lemma "min_ed_ia ''madagascar'' ''bananas'' = 6" by eval text \Extracting an Executable Constant for the Imperative Implementation\ ground_function min_ed_ix\<^sub>h'_impl: min_ed_ix\<^sub>h'.simps termination by(relation "measure(\(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 \ nat ref \ nat option array ref \ 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 (\ (x, y). x \ m \ y \ n \ x > 0) (\ (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 = (\ (i, j). (if i > 0 \ i \ m \ j \ 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 \ (init_state (n + 1) (m::nat) (m + 1) :: (nat ref \ nat ref \ nat option array ref \ 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)" "\ _. (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 \Imperative Test Case\ definition "min_ed_ia\<^sub>h xs ys = (let a = IArray xs; b = IArray ys in min_ed_ix_impl (\i. a!!i) (\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 \One can see a trace of the calls to the memory in the output\ ML \Test.test_case ()\ end diff --git a/thys/Monad_Memo_DP/example/OptBST.thy b/thys/Monad_Memo_DP/example/OptBST.thy --- a/thys/Monad_Memo_DP/example/OptBST.thy +++ b/thys/Monad_Memo_DP/example/OptBST.thy @@ -1,219 +1,208 @@ subsection \Optimal Binary Search Trees\ theory OptBST imports "HOL-Library.Tree" "HOL-Library.Code_Target_Numeral" "../state_monad/State_Main" "../heap_monad/Heap_Default" Example_Misc + "HOL-Library.Product_Lexorder" + "HOL-Library.RBT_Mapping" begin subsubsection \Misc\ -(* FIXME mv List *) -lemma induct_list012: - "\P []; \x. P [x]; \x y zs. P (y # zs) \ P (x # y # zs)\ \ P xs" -by induction_schema (pat_completeness, lexicographic_order) - -lemma upto_split1: - "i \ j \ j \ k \ [i..k] = [i..j-1] @ [j..k]" -proof (induction j rule: int_ge_induct) - case base thus ?case by (simp add: upto_rec1) -next - case step thus ?case using upto_rec1 upto_rec2 by simp -qed - -lemma upto_split2: - "i \ j \ j \ k \ [i..k] = [i..j] @ [j+1..k]" -using upto_rec1 upto_rec2 upto_split1 by auto - -lemma upto_Nil: "[i..j] = [] \ j < i" -by (simp add: upto.simps) - -lemma upto_Nil2: "[] = [i..j] \ j < i" -by (simp add: upto.simps) - -lemma upto_join3: "\ i \ j; j \ k \ \ [i..j-1] @ j # [j+1..k] = [i..k]" -using upto_rec1 upto_split1 by auto - -fun arg_min_list :: "('a \ ('b::linorder)) \ 'a list \ 'a" where -"arg_min_list f [x] = x" | -"arg_min_list f (x#y#zs) = (let m = arg_min_list f (y#zs) in if f x \ f m then x else m)" - -lemma f_arg_min_list_f: "xs \ [] \ f (arg_min_list f xs) = Min (f ` (set xs))" -by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym) -(* end mv *) - +lemma upto_join: "\ i \ j; j \ k \ \ [i..j-1] @ j # [j+1..k] = [i..k]" + using upto_rec1 upto_split1 by auto subsubsection \Definitions\ context fixes W :: "int \ int \ nat" begin fun wpl :: "int \ int \ int tree \ nat" where "wpl i j Leaf = 0" | "wpl i j (Node l k r) = wpl i (k-1) l + wpl (k+1) j r + W i j" function min_wpl :: "int \ int \ nat" where "min_wpl i j = (if i > j then 0 else min_list (map (\k. min_wpl i (k-1) + min_wpl (k+1) j + W i j) [i..j]))" -by auto + by auto termination by (relation "measure (\(i,j) . nat(j-i+1))") auto declare min_wpl.simps[simp del] function opt_bst :: "int * int \ int tree" where "opt_bst (i,j) = (if i > j then Leaf else arg_min_list (wpl i j) [\opt_bst (i,k-1), k, opt_bst (k+1,j)\. k \ [i..j]])" -by auto + by auto termination by (relation "measure (\(i,j) . nat(j-i+1))") auto declare opt_bst.simps[simp del] subsubsection \Functional Memoization\ context fixes n :: nat begin context fixes mem :: "nat option array" begin memoize_fun min_wpl\<^sub>T: min_wpl with_memory dp_consistency_heap_default where bound = "Bound (0, 0) (int n, int n)" and mem="mem" monadifies (heap) min_wpl.simps context includes heap_monad_syntax begin thm min_wpl\<^sub>T'.simps min_wpl\<^sub>T_def end memoize_correct by memoize_prover lemmas memoized_empty = min_wpl\<^sub>T.memoized_empty end (* Fixed array *) context includes heap_monad_syntax notes [simp del] = min_wpl\<^sub>T'.simps begin definition "min_wpl\<^sub>h \ \ i j. Heap_Monad.bind (mem_empty (n * n)) (\ mem. min_wpl\<^sub>T' mem i j)" lemma min_wpl_heap: "min_wpl i j = result_of (min_wpl\<^sub>h i j) Heap.empty" unfolding min_wpl\<^sub>h_def using memoized_empty[of _ "\ m. \ (a, b). min_wpl\<^sub>T' m a b" "(i, j)", OF min_wpl\<^sub>T.crel] by (simp add: index_size_defs) end end (* Bound *) -context begin +context includes state_monad_syntax begin + memoize_fun min_wpl\<^sub>m: min_wpl with_memory dp_consistency_mapping monadifies (state) min_wpl.simps thm min_wpl\<^sub>m'.simps memoize_correct by memoize_prover print_theorems lemmas [code] = min_wpl\<^sub>m.memoized_correct +memoize_fun opt_bst\<^sub>m: opt_bst with_memory dp_consistency_mapping monadifies (state) opt_bst.simps +thm opt_bst\<^sub>m'.simps + +memoize_correct + by memoize_prover +print_theorems +lemmas [code] = opt_bst\<^sub>m.memoized_correct + end subsubsection \Correctness Proof\ lemma min_wpl_minimal: "inorder t = [i..j] \ min_wpl i j \ wpl i j t" proof(induction i j t rule: wpl.induct) case (1 i j) - then show ?case by (simp add: min_wpl.simps upto_Nil2) + then show ?case by (simp add: min_wpl.simps) next case (2 i j l k r) then show ?case proof cases assume "i > j" thus ?thesis by(simp add: min_wpl.simps) next assume [arith]: "\ i > j" have kk_ij: "k\set[i..j]" using 2 by (metis set_inorder tree.set_intros(2)) let ?M = "((\k. min_wpl i (k-1) + min_wpl (k+1) j + W i j) ` {i..j})" let ?w = "min_wpl i (k-1) + min_wpl (k+1) j + W i j" have aux_min:"Min ?M \ ?w" proof (rule Min_le) show "finite ?M" by simp show "?w \ ?M" using kk_ij by auto qed have"inorder \l,k,r\ = inorder l @k#inorder r" by auto from this have C:"[i..j] = inorder l @ k#inorder r" using 2 by auto have D: "[i..j] = [i..k-1]@k#[k+1..j]" using kk_ij upto_rec1 upto_split1 by (metis atLeastAtMost_iff set_upto) have l_inorder: "inorder l = [i..k-1]" by (smt C D append_Cons_eq_iff atLeastAtMost_iff set_upto) have r_inorder: "inorder r = [k+1..j]" by (smt C D append_Cons_eq_iff atLeastAtMost_iff set_upto) - have "min_wpl i j = Min ?M" by (simp add: min_wpl.simps min_list_Min upto_Nil) + have "min_wpl i j = Min ?M" by (simp add: min_wpl.simps min_list_Min) also have "... \ ?w" by (rule aux_min) also have "... \ wpl i (k-1) l + wpl (k+1) j r + W i j" using l_inorder r_inorder "2.IH" by simp also have "... = wpl i j \l,k,r\" by simp finally show ?thesis . qed qed lemma P_arg_min_list: "(\x. x \ set xs \ P x) \ xs \ [] \ P(arg_min_list f xs)" -by(induction f xs rule: arg_min_list.induct) (auto simp: Let_def) + by (induction f xs rule: arg_min_list.induct) (auto simp: Let_def) lemma opt_bst_correct: "inorder (opt_bst (i,j)) = [i..j]" -apply(induction "(i,j)" arbitrary: i j rule: opt_bst.induct) -by (force simp: opt_bst.simps upto_Nil upto_join3 intro: P_arg_min_list) + by (induction "(i,j)" arbitrary: i j rule: opt_bst.induct) + (force simp: opt_bst.simps upto_join intro: P_arg_min_list) lemma wpl_opt_bst: "wpl i j (opt_bst (i,j)) = min_wpl i j" proof(induction i j rule: min_wpl.induct) case (1 i j) show ?case proof cases assume "i > j" thus ?thesis by(simp add: min_wpl.simps opt_bst.simps) next assume *[arith]: "\ i > j" let ?ts = "[\opt_bst (i,k-1), k, opt_bst (k+1,j)\. k <- [i..j]]" let ?M = "((\k. min_wpl i (k-1) + min_wpl (k+1) j + W i j) ` {i..j})" have "?ts \ []" by (auto simp add: upto.simps) have "wpl i j (opt_bst (i,j)) = wpl i j (arg_min_list (wpl i j) ?ts)" by (simp add: opt_bst.simps) also have "\ = Min (wpl i j ` (set ?ts))" by(rule f_arg_min_list_f[OF \?ts \ []\]) also have "\ = Min ?M" proof (rule arg_cong[where f=Min]) show "wpl i j ` (set ?ts) = ?M" by (fastforce simp: Bex_def image_iff 1[OF *]) qed - also have "\ = min_wpl i j" by (simp add: min_wpl.simps min_list_Min upto_Nil) + also have "\ = min_wpl i j" by (simp add: min_wpl.simps min_list_Min) finally show ?thesis . qed qed lemma opt_bst_is_optimal: "inorder t = [i..j] \ wpl i j (opt_bst (i,j)) \ wpl i j t" -by (simp add: min_wpl_minimal wpl_opt_bst) + by (simp add: min_wpl_minimal wpl_opt_bst) -end +end (* Weight function *) + subsubsection \Test Case\ +text \Functional Implementations\ + +value "min_wpl (\i j. nat(i+j)) 0 4" + +value "opt_bst (\i j. nat(i+j)) (0, 4)" + + +text \Imperative Implementation\ + code_thms min_wpl -definition "min_wpl_test = min_wpl\<^sub>h (\i j. nat(i+j)) 2 3 3" +definition "min_wpl_test = min_wpl\<^sub>h (\i j. nat(i+j)) 4 0 4" code_reflect Test functions min_wpl_test ML \Test.min_wpl_test ()\ -end +end \ No newline at end of file