Theory TSP_Dyn_Prog

(* License: LGPL *)

theory TSP_Dyn_Prog
imports Main
begin


section ‹The Bellman–-Held–-Karp approach to TSP›


subsection ‹Hamiltonian paths›

text ‹A Hamiltonian path from a vertex $s$ to a vertex $t$ via a (finite) set $V$ has to pass 
      through each vertex in $V$ exactly once.
      This can be captured by a list that starts with $s$, ends with $t$ and has a distinct list
      containing all vertices from $V$ (i.e. essentially the same as a permutation on $V$) in-between.

      In particular, with $s = t$ one gets a representation of a Hamiltonian cycle from $s$ via $V$.

      Also note that $s$ or $t$ might in principle occur in $V$ as well.›

definition
"Hamiltonian_paths s V t = {s#vs@[t] |vs. distinct vs ∧ set vs = V}"


text ‹By the above definition, a Hamiltonian path exists only for a finite $V$:›
lemma Hamiltonian_paths_not_empty :
"finite V = (∃p. p ∈ Hamiltonian_paths s V t)"
  using Hamiltonian_paths_def finite_distinct_list by fastforce


lemma Hamiltonian_paths_finite :
"finite(Hamiltonian_paths s V t)"
proof(cases "finite V")
  case a:True
  show ?thesis
  proof(rule_tac B="(λvs. s#vs@[t]) ` {vs. set vs ⊆ V ∧ distinct vs}" in finite_subset)
    show "Hamiltonian_paths s V t ⊆ (λvs. s # vs @ [t]) ` {vs. set vs ⊆ V ∧ distinct vs}"
      by(clarsimp simp: Hamiltonian_paths_def)
  next
    from a show "finite ((λvs. s#vs@[t]) ` {vs. set vs ⊆ V ∧ distinct vs})"
      by (simp add: finite_subset_distinct)
  qed
next
  case False
  then show ?thesis
    by (metis Hamiltonian_paths_not_empty equals0I finite.emptyI)
qed



lemma Hamiltonian_paths0 :
"Hamiltonian_paths s {} t = {[s, t]}"
  by(clarsimp simp: Hamiltonian_paths_def)


text ‹If $V$ is not empty then the tail of any Hamiltonian path from $s$ to $t$ via $V$ 
      is in turn a Hamiltonian path starting with a vertex in $V$:›
lemma Hamiltonian_pathsD :
  assumes "p ∈ Hamiltonian_paths s V t"
      and "V ≠ {}"
    shows "∃v∈V. ∃p'∈ Hamiltonian_paths v (V - {v}) t. p = s#p'"
  using assms Hamiltonian_paths_def hd_Cons_tl set_empty
proof(clarsimp simp: Hamiltonian_paths_def) 
qed(case_tac vs; clarsimp+)


lemma Hamiltonian_pathsI :
  assumes "p ∈ Hamiltonian_paths v (V - {v}) t"
      and "v ∈ V"
    shows "s#p ∈ Hamiltonian_paths s V t"
  using assms
  by(clarsimp simp: Hamiltonian_paths_def insert_absorb)




subsection ‹Optimal Hamiltonian paths›


text ‹Extending an edge distance function $\delta$ to paths:›
fun path_distance where
"path_distance δ [] = (0 :: 'a :: linordered_ab_group_add)" |
"path_distance δ [v] = 0" |
"path_distance δ (v1#v2#vs) = δ v1 v2 + path_distance δ (v2#vs)"



lemma Hamiltonian_path_distance_Cons_le :
  assumes "p ∈ Hamiltonian_paths s V t"
      and "p' ∈ Hamiltonian_paths s V t"
    shows "(path_distance δ p ≤ path_distance δ p') = 
           (path_distance δ (v#p) ≤ path_distance δ (v#p'))"
  using assms by(clarsimp simp: Hamiltonian_paths_def)



text ‹A Hamiltonian path is optimal with respect to the given edge distance function $\delta$ 
      if its @{term path_distance} is minimal:›
definition 
"opt_Hamiltonian_paths δ s V t = {p. p ∈ Hamiltonian_paths s V t ∧ 
  (∀p'∈Hamiltonian_paths s V t. path_distance δ p ≤ path_distance δ p')}"


lemma opt_Hamiltonian_paths0 :
"opt_Hamiltonian_paths δ s {} t = {[s, t]}"
  by(fastforce simp: opt_Hamiltonian_paths_def Hamiltonian_paths0)
 

lemma opt_Hamiltonian_pathsD :
"opt_Hamiltonian_paths δ s V t ⊆ Hamiltonian_paths s V t"
  by(clarsimp simp: opt_Hamiltonian_paths_def)


lemma opt_Hamiltonian_paths_same_distance :
  assumes "p ∈ opt_Hamiltonian_paths δ s V t"
      and "p' ∈ opt_Hamiltonian_paths δ s V t"
    shows "path_distance δ p = path_distance δ p'"
  using assms
  by (simp add: Orderings.order_eq_iff opt_Hamiltonian_paths_def)



lemma opt_Hamiltonian_paths_not_empty :
  assumes "finite V"
  shows "∃p. p ∈ opt_Hamiltonian_paths δ s V t"
proof -
  have "Hamiltonian_paths s V t ≠ {}"
    by (metis Hamiltonian_paths_not_empty assms empty_iff)
  with obtains_MIN[where f="path_distance δ"] show ?thesis
    by (smt (verit, best) Hamiltonian_paths_finite Min.bounded_iff empty_iff finite_imageI image_eqI
        mem_Collect_eq nle_le opt_Hamiltonian_paths_def)
qed



lemma opt_Hamiltonian_pathsI :
  assumes "p ∈ Hamiltonian_paths s V t"
  and "∀p'∈opt_Hamiltonian_paths δ s V t. path_distance δ p ≤ path_distance δ p'"
  shows "p ∈ opt_Hamiltonian_paths δ s V t"
  by (smt (z3) Hamiltonian_paths_not_empty assms mem_Collect_eq opt_Hamiltonian_paths_def
      opt_Hamiltonian_paths_not_empty order_trans)



subsection ‹Minimal distance extensions›

definition Min_distance_ext where 
"Min_distance_ext δ v S = {v#p |p. p ∈ S ∧ 
 (∀p'∈S. path_distance δ (v#p) ≤ path_distance δ (v#p'))}"


lemma Min_distance_ext :
"(p ∈ Min_distance_ext δ v S) = 
 (∃p'∈S. p = v#p' ∧ (∀p''∈S. path_distance δ (v#p') ≤ path_distance δ (v#p'')))"
proof(rule iffI) 
qed(clarsimp simp: Min_distance_ext_def)+


lemma Min_distance_ext_eq' :
  assumes "S ⊆ T" 
      and "∀p'∈T - S. ∃p∈S. path_distance δ (v#p) < path_distance δ (v#p')"
    shows "(p ∈ Min_distance_ext δ v S) = (p ∈ Min_distance_ext δ v T)" 
  (is "?L = ?R")
proof
  assume ?L with assms show ?R
    by (smt (verit, del_insts) DiffI Min_distance_ext nless_le order.strict_trans1 subset_iff)
next
  assume ?R with assms show ?L
    by (smt (verit, del_insts) DiffI Min_distance_ext nle_le nless_le subset_iff)
qed


corollary Min_distance_ext_eq :
  assumes "S ⊆ T" 
      and "∀p'∈T - S. ∃p∈S. path_distance δ (v#p) < path_distance δ (v#p')"
    shows "Min_distance_ext δ v S = Min_distance_ext δ v T" 
proof(rule set_eqI)
qed(simp add: Min_distance_ext_eq' assms)



subsection ‹@{term opt_Hamiltonian_paths} as a fixed point›


theorem opt_Hamiltonian_paths_fix :
  assumes "V ≠ {}"
  shows "opt_Hamiltonian_paths δ s V t = 
         Min_distance_ext δ s (⋃v∈V. opt_Hamiltonian_paths δ v (V - {v}) t)"
(is "?L = ?R") 
proof
  show "?L ⊆ ?R"
  proof
    fix p assume a: "p ∈ opt_Hamiltonian_paths δ s V t"
    with assms obtain v p' where b: "v ∈ V" "p' ∈ Hamiltonian_paths v (V - {v}) t" "p = s#p'"
      by (meson Hamiltonian_pathsD opt_Hamiltonian_pathsD subsetD)
    have "p' ∈ opt_Hamiltonian_paths δ v (V - {v}) t"
    proof(rule opt_Hamiltonian_pathsI)
      show "p' ∈ Hamiltonian_paths v (V - {v}) t" by(rule b)
    next
      from a and b 
      show "∀p''∈opt_Hamiltonian_paths δ v (V - {v}) t. path_distance δ p' ≤ path_distance δ p''"
        by (metis (no_types, lifting) Hamiltonian_path_distance_Cons_le Hamiltonian_pathsI 
            mem_Collect_eq opt_Hamiltonian_paths_def)
    qed
    with a show "p ∈ Min_distance_ext δ s (⋃v∈V. opt_Hamiltonian_paths δ v (V - {v}) t)"
    proof(clarsimp simp: Min_distance_ext)
    qed(metis (no_types, lifting) Hamiltonian_pathsI b(1,3) mem_Collect_eq opt_Hamiltonian_paths_def)
  qed
next
  show "?R ⊆ ?L"
  proof(clarsimp simp: Min_distance_ext)
    fix v p
    assume 1: "v ∈ V"
       and 2: "p ∈ opt_Hamiltonian_paths δ v (V - {v}) t"
       and 3: "∀v∈V. ∀p'∈opt_Hamiltonian_paths δ v (V - {v}) t. 
                   path_distance δ (s#p) ≤ path_distance δ (s#p')" 
    show "s#p ∈ opt_Hamiltonian_paths δ s V t"
    proof(rule opt_Hamiltonian_pathsI)
      from 1 and 2 show "s#p ∈ Hamiltonian_paths s V t"
        by (meson Hamiltonian_pathsI opt_Hamiltonian_pathsD subsetD)
    next
      show "∀p'∈opt_Hamiltonian_paths δ s V t. path_distance δ (s#p) ≤ path_distance δ p'"
      proof
        fix p' assume a:"p' ∈ opt_Hamiltonian_paths δ s V t"
        with 1 obtain v' p'' where "p''∈ Hamiltonian_paths v' (V - {v'}) t" "v' ∈ V" "p' = s#p''"
          by (metis Hamiltonian_pathsD emptyE in_mono opt_Hamiltonian_pathsD)
        with 3 and a show "path_distance δ (s#p) ≤ path_distance δ p'"
          by (smt (verit) Hamiltonian_path_distance_Cons_le Hamiltonian_pathsI
              mem_Collect_eq opt_Hamiltonian_paths_def)
      qed
    qed
  qed
qed



section ‹An implementation using dynamic programming›


subsection ‹A few preparations›


text ‹Membership test for lists with a (strictly) descending order of elements:›
fun memS where
"memS a [] = False" |
"memS a (x#xs) = (a ≤ x ∧ (a = x ∨ memS a xs))"


lemma memS :
  assumes "sorted_wrt (>) xs"
  shows "memS (a :: 'a :: linorder) xs = (a ∈ set xs)"
  using assms
proof(induct xs) 
qed(fastforce+)


text ‹Removal from lists with a strictly descending order of elements:›
fun rem1S where
"rem1S (a :: 'a :: linorder) [] = []" |
"rem1S a (x#xs) = (if a = x then xs else (if a < x then x#rem1S a xs else x#xs))"

lemma rem1S :
  assumes "sorted_wrt (>) xs" 
  shows "set(rem1S a xs) = set xs - {a}"
  using assms
proof(induct xs)
qed(force+)


lemma rem1S_length :
  assumes "sorted_wrt (>) xs"
      and "a ∈ set xs"
    shows "length(rem1S a xs) + 1 = length xs"
  using assms
proof(induct xs)
qed(fastforce+)


corollary rem1S_length' :
  assumes "sorted_wrt (>) xs"
      and "a ∈ set xs"
    shows "length(rem1S a xs) < length xs"
  using assms rem1S_length by fastforce


lemma sorted_wrt_rem1S :
  assumes "sorted_wrt (>) xs" 
  shows "sorted_wrt (>) (rem1S a xs)"
  using assms
proof(induct xs) 
qed(clarsimp simp: rem1S)+



lemma sorted_lists_eq :
  assumes "sorted_wrt (>) (as :: 'a :: linorder list)"
      and "sorted_wrt (>) bs"
      and "set as ⊆ set bs" 
      and "length as = length bs"
    shows "as = bs"
  using assms
proof(induct bs arbitrary: as)
  case Nil
  then show ?case
    by simp 
next
  case 1:(Cons b bs)
  then show ?case 
  proof(cases as)
    case Nil
    then show ?thesis
      using 1(5) by fastforce 
  next
    case (Cons a as')
    with 1 show ?thesis
    proof(clarsimp)
    qed(metis not_less_iff_gr_or_eq subset_insert_iff)
  qed
qed



subsection ‹Indexing subsets of $\{0,\ldots,n\}$ represented by sorted lists›


fun nat2list :: "nat ⇒ nat ⇒ nat list" 
  where
"nat2list c ix = (if ix = 0 then []
                  else (if even ix then nat2list (c+1) (ix div 2)
                        else nat2list (c+1) (ix div 2) @ [c]))"


lemma nat2list_Nil :
"(nat2list c ix = []) = (ix = 0)"
proof(induct c ix rule: nat2list.induct)
  case (1 c ix)
  then show ?case
  proof(cases ix)
    case 0
    then show ?thesis
      by simp 
  next
    case (Suc n)
    with 1 show ?thesis 
    proof(subst nat2list.simps)
    qed(clarsimp simp del: nat2list.simps)
  qed
qed


abbreviation pow2 :: "nat ⇒ nat"  ("2⇗_⇖" 80)
  where "pow2 n ≡ 2^n"



lemma nat2list_ub :
  assumes "ix < 2⇗b⇖"
  shows "∀i∈set(nat2list c ix). i < b + c"
  using assms
proof(induct c ix arbitrary: b rule: nat2list.induct)
  case (1 c ix)
  show ?case
  proof(cases b)
    case 0
    with 1 show ?thesis by simp 
  next
    case (Suc n)
    with 1 show ?thesis 
    proof(subst nat2list.simps)
    qed(clarsimp simp del: nat2list.simps)
  qed
qed


lemma nat2list_lb :
"∀i∈set(nat2list c ix). c ≤ i"
proof(induct c ix rule: nat2list.induct)
  case (1 c ix)
  hence "ix > 0 ⟹ ∀i∈set (nat2list (c + 1) (ix div 2)). c ≤ i" by fastforce
  then show ?case
  proof(subst nat2list.simps)
  qed(simp del: nat2list.simps)
qed



lemma nat2list_sorted :
"sorted_wrt (>) (nat2list c ix)"
proof(induct c ix rule: nat2list.induct)
  case (1 c ix)
  have "ix > 0 ⟹ ∀i∈set (nat2list (c + 1) (ix div 2)). c < i"
    by (meson less_iff_succ_less_eq nat2list_lb)
  with 1 show ?case 
  proof(subst nat2list.simps)
  qed(simp add: sorted_wrt_append del: nat2list.simps)
qed


lemma nat2list_pow2[OF refl] :
  assumes "b = 2⇗n⇖"
  shows "nat2list c b = [c+n]"
  using assms
proof(induct c b arbitrary: n rule: nat2list.induct)
  case (1 c ix)
  then show ?case 
  proof(cases "n")
    case 0
    with 1(3) and nat2list_Nil show ?thesis
      by simp 
  next
    case (Suc m)
    with 1 show ?thesis 
    proof(subst nat2list.simps)
    qed(simp del: nat2list.simps)
  qed
qed



lemma pow2_div2 :
  assumes "n > 0"
  shows "(2⇗n⇖ + x) div 2 = 2⇗n-1⇖ + x div 2"
  by (metis assms add_self_div_2 div_plus_div_distrib_dvd_left dvd_power mult_2_right power_minus_mult)


lemma pow2pred_div2 :
"(2⇗n⇖ - 1) div 2 = 2⇗n-1⇖ - 1"
  by (metis mask_half mask_nat_def)


lemma nat2list_pred_pow2 :
  assumes "b = 2⇗n⇖ - 1" 
  shows "nat2list c b = rev [c..<n+c]"
  using assms
proof(induct c b arbitrary: n rule: nat2list.induct)
  case (1 c ix)
  then show ?case
  proof(cases "n = 0")
    case True
    with 1 show ?thesis by simp 
  next
    case a:False
    then show ?thesis
    proof(cases "n = 1")
      case True
      with 1 show ?thesis by simp 
    next
      from a have b : "2⇗n⇖ > 1" by (simp add: less_trans_Suc)
      case False
      with 1 and a and b and pow2pred_div2[of n] show ?thesis 
      proof(subst nat2list.simps)
      qed(simp add: bot_nat_0.not_eq_extremum upt_rec)
    qed
  qed
qed


corollary nat2list_pred_pow2' :
"nat2list 0 (2⇗n⇖ - 1) = rev [0..<n]"
  using nat2list_pred_pow2 by fastforce



lemma nat2list_shift :
  assumes "ix < 2⇗b⇖"
  shows "nat2list c (2⇗b⇖ + ix) = (c + b)#(nat2list c ix)"
  using assms
proof(induct c ix arbitrary: b rule: nat2list.induct)
  case (1 c ix)
  then show ?case 
  proof(cases "b = 0")
    case True
    with 1 show ?thesis by simp
  next
    case 2:False
    show ?thesis 
    proof(cases "even ix")
      case 3:True
      show ?thesis
      proof(cases "ix = 0")
        case True
        with 2 show ?thesis
          by (metis add.right_neutral nat2list_Nil nat2list_pow2)  
      next
        case 4:False
        note pow2_div2[where x=ix and n=b]
        with 1(1)[where b="b-1"] and 1(3) and 2 and 3 and 4 show ?thesis
          by (simp add: div_greater_zero_iff div_less_iff_less_mult dvd_add_left_iff power_eq_if)
      qed
    next
      case 3:False
      hence "ix > 0" by (meson odd_pos) 

      with 1(2)[where b="b-1"] and 1(3) and 2 and 3 
      have "nat2list (c+1) (2⇗b - 1⇖ + ix div 2) @ [c] = (c + b) # nat2list c ix"
      proof(subst nat2list.simps[where ix=ix])
      qed(smt (verit, best) One_nat_def Suc_pred append_Cons even_add even_power group_cancel.add1
          less_mult_imp_div_less mult_2_right plus_1_eq_Suc power_commutes power_eq_if)

      with 2 and 3 show ?thesis
        by (simp add: pow2_div2)
    qed
  qed
qed




lemma nat2list_inj :
  assumes "ix ≠ ix'"
  shows "nat2list c ix ≠ nat2list c ix'"
  using assms
proof(induct c ix arbitrary: ix' rule: nat2list.induct)
  case (1 c ix)
  then show ?case 
  proof(cases "even ix")
    case 2:True
    then show ?thesis 
    proof(cases "even ix'")
      case True
      with 1 and 2 show ?thesis
        by (metis dvd_div_eq_iff nat2list.simps nat2list_Nil) 
    next
      case False
      with 1 and 2 show ?thesis
        by (metis add_le_same_cancel1 in_set_conv_decomp nat2list.simps nat2list_lb not_one_le_zero)
    qed
  next
    case 2:False
    show ?thesis 
    proof(cases "even ix'")
      case True
      with 1 and 2 show ?thesis
        by (metis add_le_same_cancel1 even_zero in_set_conv_decomp nat2list.simps nat2list_lb not_one_le_zero)
    next
      have 3:"⋀n m. n ≠ m ⟹ odd n ⟹ odd m ⟹ n div 2 ≠ m div 2"
        by (metis mod2_eq_if mult_div_mod_eq) 
      case False
      with 1(2)[where ix'="ix' div 2"] and 1(3) and 2 show ?thesis 
        by(simp add: 3) 
    qed
  qed
qed




fun list2nat :: "nat ⇒ nat ⇒ nat list ⇒ nat"
  where
"list2nat r b [] = 2⇗b⇖ * r" |
"list2nat r b (e#l) = (if b > 0 then 
                        (if b-1 = e then list2nat (2*r + 1) (b-1) l 
                         else list2nat (2*r) (b-1) (e#l))
                       else r)"



lemma list2nat_eq :
"list2nat r b l = 2⇗b⇖*r + list2nat 0 b l"                            
proof(induct b arbitrary:l r rule: less_induct)
  case (less x)
  then show ?case
  proof(cases l)
    case Nil
    then show ?thesis by simp
  next
    case (Cons a xs)
    then show ?thesis
    proof(cases "x - 1 = a")
      case 1:True
      note less[of "x-1" "2*r+1" "xs"] and less[of "x-1" "1" "xs"]
      with Cons and 1 show ?thesis
        by (simp add: power_eq_if)
    next
      case 1:False
      note less[of "x-1" "2*r" "a#xs"]
      with Cons and 1 show ?thesis
        by (simp add: power_eq_if)
    qed
  qed
qed



lemma list2nat_gr0 :
  assumes "sorted_wrt (>) l"
      and "length l > 0"
      and "∀x∈set l. x < b"
    shows "list2nat r b l > 0"
  using assms
proof(induct r b l rule: list2nat.induct)
  case (1 r b)
  then show ?case by simp
next
  case (2 r b x l)
  then show ?case
  proof(cases "l = []")
    case True
    with 2(5) show ?thesis
    proof(clarsimp simp del: list2nat.simps)
      have "x < b ⟹ 0 < list2nat 0 b [x]"
      proof(induct b rule: less_induct)
        case (less v)
        then show ?case
        proof(subst list2nat.simps)
        qed(simp del: list2nat.simps(2))
      qed      
      thus "x < b ⟹ 0 < list2nat r b [x]"
        by (metis add_is_0 gr_zeroI list2nat_eq)
    qed
  next
    from 2 have a:"b - 1 ≠ x ⟹ 0 < list2nat (2 * r) (b - 1) (x # l)" by fastforce
    case False
    with 2 and a show ?thesis
    proof(subst list2nat.simps)
    qed(simp del: list2nat.simps)
  qed
qed



lemma list2nat_ub :
  assumes "∀x∈set l. x < b"
      and "sorted_wrt (>) l"
    shows "list2nat r b l < 2⇗b⇖ * r + 2⇗b⇖"
  using assms
proof(induct r b l rule: list2nat.induct)
  case (1 r b)
  then show ?case by simp
next
  case (2 r b x l)
  then show ?case 
  proof(cases "b - 1 = x")
    case True
    with 2 show ?thesis 
    proof(subst list2nat.simps)
    qed(clarsimp simp del: list2nat.simps simp add: power_eq_if)
  next
    case a:False
    with 2(4) have b:"∀x∈set (x # l). x < b - 1" using 2(3) by fastforce
    hence c:"b > 0"
      by (simp add: less_diff_conv)
    hence "list2nat (2 * r) (b - 1) (x # l) < 2 ^ (b - 1) * (2 * r) + 2 ^ (b - 1)"
      using 2 and a and b by blast
    with a and c show ?thesis
      by (smt (z3) ab_semigroup_mult_class.mult_ac(1) add.commute left_add_mult_distrib 
          list2nat.simps(2) mult_2_right mult_numeral_1_right power_minus_mult trans_less_add2)
  qed
qed


lemmas list2nat_ub0 = list2nat_ub[where r=0, simplified]


lemma list2nat_inj :
  assumes "∀x∈set l. x < b"
      and "sorted_wrt (>) l"
    shows "nat2list 0 (list2nat 0 b l) = l"
  using assms
proof(induct b arbitrary: l rule: less_induct)
  case (less b)
  then show ?case 
  proof(cases "l")
    case Nil
    then show ?thesis by simp
  next
    case (Cons y ls)
    with less(2) have a:"b > 0" by simp 
    show ?thesis
    proof(cases "b - 1 = y")
      case b:True
      with less(2, 3) and Cons and a have c:"∀x∈set ls. x < b-1 ∧ sorted_wrt (>) ls"
        by (meson sorted_wrt.simps(2))

      with Cons and a and b 
      have d:"nat2list 0 (list2nat 1 (b - 1) ls) = 
              (b - 1) # nat2list 0 (list2nat 0 (b - 1) ls)"
      proof(subst list2nat_eq)
      qed(metis add.commute add_0 lambda_one less.prems(2) list2nat_ub mult_0_right mult_Suc_right 
          nat2list_shift sorted_wrt.simps(2))

      note less(1)[where y="b-1" and l=ls]
      with a and b and c have "nat2list 0 (list2nat 0 (b - 1) ls) = ls"
        by (metis diff_less less_numeral_extra(1) nth_mem sorted_wrt_iff_nth_less)
      with a and b and d and Cons and list2nat.simps show ?thesis 
        by simp
    next
      case b:False
      have "nat2list 0 (list2nat 0 (b - 1) (y # ls)) = y # ls"
      proof(rule less(1))
        from a show "b - 1 < b" by simp
      next
        from less(2,3) and a and b and Cons show "∀x∈set (y # ls). x < b - 1" by fastforce
      next
        from less(3) Cons show "sorted_wrt (>) (y # ls)" by simp
      qed
      with a and b and Cons and list2nat.simps show ?thesis
        by simp 
    qed
  qed
qed


corollary list2nat_surj :
  assumes "ix < 2⇗b⇖"
  shows "list2nat 0 b (nat2list 0 ix) = ix"
  by (metis assms add.right_neutral list2nat_inj nat2list_inj nat2list_sorted nat2list_ub)



lemma list2nat_mono :
  assumes "∀x∈set l. x < b"
      and "sorted_wrt (>) l" 
      and "length l' < length l"
      and "set l' ⊆ set l"
      and "sorted_wrt (>) l'"
    shows "list2nat r b l' < list2nat r b l"
  using assms
proof(induct r b l arbitrary: l' rule: list2nat.induct)
  case (1 r b)
  then show ?case by simp
next
  case (2 r b x l)
  hence a:"b > 0" by simp
  show ?case
  proof(cases "b - 1 = x")
    case b:True
    with 2(3, 4) and a have c:"(∀x∈set l. x < b-1) ∧ sorted_wrt (>) l" by simp
    have "list2nat r b l' < list2nat (2 * r + 1) x l"
    proof(cases l')
      case Nil
      with 2 and a and b show ?thesis
      proof(subst list2nat_eq[where l=l])
      qed(smt (verit) ab_semigroup_mult_class.mult_ac(1) less_add_same_cancel1 list2nat.simps(1) mult.commute
          mult_less_mono1 power_minus_mult trans_less_add1 zero_less_numeral zero_less_one zero_less_power)
    next
      case (Cons a l'')
      show ?thesis
      proof(cases "b-1 = a")
        case d:True
        have "list2nat (2 * r + 1) (b - 1) l'' < list2nat (2 * r + 1) (b - 1) l"
        proof(rule 2(1))
          from a show "b > 0" .
        next
          from b show "b - 1 = x" .
        next
          from c show "∀x'∈set l. x' < b - 1" by simp
        next
          from c show "sorted_wrt (>) l" by simp
        next
          from 2(5) and Cons show "length l'' < length l" by simp
        next
          from 2(6, 7) and Cons and b and d show "set l'' ⊆ set l"
            using set_subset_Cons by fastforce
        next
          from 2(7) and Cons show "sorted_wrt (>) l''" by simp
        qed
        with a and b and d and Cons show ?thesis by simp
      next
        case d:False
        show ?thesis
        proof(cases "length l'' + 1 = length l")
          case e:True
          have "l' = l"
          proof(rule sorted_lists_eq)
            show "sorted_wrt (>) l" using 2(4) by fastforce
          next
            show "set l' ⊆ set l" using b c d Cons 2(6) 2(7) by fastforce
          next
            show "length l' = length l" using Cons e by fastforce
          qed(simp add: 2)
          with a and b and d and Cons show ?thesis
            by (smt (verit, del_insts) add.commute add_less_cancel_left less_add_same_cancel1 list2nat.simps(2)
                list2nat_eq mult.commute mult_less_mono1 zero_less_numeral zero_less_one zero_less_power)
        next
          case e:False
          have f:"list2nat (2 * r + 1) (b - 1) (a # l'') < list2nat (2 * r + 1) (b - 1) l"
          proof(rule 2(1))
            from a show "b > 0" .
          next
            from b show "b - 1 = x" .
          next
            from c show "∀x∈set l. x < b - 1" by simp
          next
            from c show "sorted_wrt (>) l" by simp
          next
            from Cons and e and 2(5) show "length (a # l'') < length l" by fastforce
          next
            from 2(6, 7) and Cons and b c d e  show "set (a # l'') ⊆ set l"
            proof(clarsimp)
            qed(metis less_imp_add_positive not_add_less1 subset_iff subset_insert)
          next
            from 2(7) and Cons show "sorted_wrt (>) (a # l'')" by simp
          qed

          have "list2nat (2 * r) (b - 1) (a # l'') < list2nat (2 * r + 1) (b - 1) l"
          proof(rule less_trans)
            from list2nat_eq show "list2nat (2 * r) (b - 1) (a # l'') < list2nat (2 * r + 1) (b - 1) (a # l'')"
              by (metis Suc_eq_plus1 add.commute add_less_cancel_left lessI mult.commute 
                  mult_less_mono1 zero_less_numeral zero_less_power)
          next
            from f show "list2nat (2 * r + 1) (b - 1) (a # l'') < list2nat (2 * r + 1) (b - 1) l"
              by simp
          qed

          with a and b and d and Cons show ?thesis by simp
        qed
      qed
    qed
    with a and b show ?thesis by simp
  next
    case b:False
    with 2(3, 4) and a have c:"∀x∈set(x#l). x < b - 1"
      using less_imp_diff_less by force

    have "list2nat r b l' < list2nat (2 * r) (b - 1) (x # l)" 
    proof(cases l')
      case Nil
      with 2 and a and b and c show ?thesis
        by (smt (verit, ccfv_threshold) One_nat_def Suc_le_eq ab_semigroup_mult_class.mult_ac(1) 
            le_add_diff_inverse2 list2nat.simps(1) power_Suc0_right power_add) 
    next
      case (Cons a l'')
      then show ?thesis 
      proof(cases "b-1 = a")
        case True
        with a and b and c and Cons and 2(6) show ?thesis
          by (metis less_not_refl list.set_intros(1) subset_iff)
      next
        case False
        with a and b and c and Cons and 2 show ?thesis
          by (metis list2nat.simps(2))
      qed
    qed
    with a b c and 2 show ?thesis
      by (metis list2nat.simps(2))
  qed
qed


declare list2nat.simps[simp del] nat2list.simps[simp del]



corollary list2nat_rem1S :
  assumes "sorted_wrt (>) l"
      and "∀x∈set l. x < b" 
      and "u ∈ set l"
 shows "list2nat r b (rem1S u l) < list2nat r b l"
proof(rule list2nat_mono)
qed(simp_all add: assms rem1S sorted_wrt_rem1S rem1S_length')


corollary list2nat_rem1S_not_in :
  assumes "u ∈ set (nat2list 0 ix)" 
      and "ix < 2⇗N⇖"
    shows "u ∉ set(nat2list 0 (list2nat 0 N (rem1S u (nat2list 0 ix))))"
  using assms nat2list_sorted[of 0 ix] nat2list_ub[of ix N 0] sorted_wrt_rem1S rem1S list2nat_inj
  by (metis Diff_iff add_cancel_right_right insert_iff)


corollary list2nat_rem1S_less :
  assumes "u ∈ set (nat2list 0 ix)" 
      and "ix < 2⇗N⇖"
    shows "list2nat 0 N (rem1S u (nat2list 0 ix)) < ix"
  by (metis assms add.right_neutral list2nat_rem1S list2nat_surj nat2list_sorted nat2list_ub) 




subsection ‹Computing minimal distance extensions›


fun min_distance_ext'
  where
"min_distance_ext' δ v (md :: 'a :: linordered_ab_group_add) mps [] = (md, mps)" |
"min_distance_ext' δ v md mps ((h, (d, ps))#xs) = 
(let dp = δ v h + d in
  if md < dp then min_distance_ext' δ v md mps xs
  else (if md = dp then min_distance_ext' δ v md ((map ((#) h) ps)@mps) xs
        else min_distance_ext' δ v dp (map ((#) h) ps) xs))"


definition "min_distance_ext δ v xs = 
 (case xs of 
   [] ⇒ (0, [])
 | (h, (d, ps))#xs' ⇒ min_distance_ext' δ v (δ v h + d) (map ((#) h) ps) xs')"


lemma min_distance_ext'1 :
  assumes "δ v h + d > md"
  shows "min_distance_ext' δ v md mps ((h, d, ps)#xs) = 
         min_distance_ext' δ v md mps xs"
  by(simp add: assms)

lemma min_distance_ext'2 :
  assumes "δ v h + d = md"
  shows "min_distance_ext' δ v md mps ((h, d, ps)#xs) = 
         min_distance_ext' δ v md (map ((#) h) ps@mps) xs"
  by(simp add: assms)


lemma min_distance_ext'3 :
  assumes "δ v h + d < md"
  shows "min_distance_ext' δ v md mps ((h, d, ps)#xs) = 
         min_distance_ext' δ v (δ v h + d) (map ((#) h) ps) xs"
  using assms by(fastforce simp add: Let_def)


declare min_distance_ext'.simps(2)[simp del]



definition 
"min_distance_ext_inv δ h = (λ(d, ps). length ps > 0 ∧ (∀p∈set ps. path_distance δ (h#p) = d))" 


lemma min_distance_ext_invD :
  assumes "min_distance_ext_inv δ h (d, ps)"  
  shows "∃p. p ∈ set ps" and "∀p∈set ps. path_distance δ (h#p) = d" 
  using assms last_in_set 
  unfolding min_distance_ext_inv_def
  by blast+


lemma min_distance_ext'_inv :
  assumes "min_distance_ext' δ v md mps xs = (d, ps)"
      and "min_distance_ext_inv δ v (md, mps)"
      and "∀(h, d, ps)∈set xs. min_distance_ext_inv δ h (d, ps)"
    shows "min_distance_ext_inv δ v (d, ps)"
  using assms
proof(induct xs arbitrary: md mps)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
  proof clarsimp
    fix h d' l
    assume a: "a = (h, d', l)"
       and b: "min_distance_ext_inv δ h (d', l)"
    show ?thesis
    proof(cases "δ v h + d' > md")
      case True
      with Cons and a and b show ?thesis
        by (metis list.set_intros(2) min_distance_ext'1) 
    next
      case c:False
      show ?thesis
      proof(cases "δ v h + d' < md")
        from Cons(4) and a have d: "min_distance_ext_inv δ v (δ v h + d', map ((#) h) l)" 
          by(clarsimp simp: min_distance_ext_inv_def)
        case True
        with Cons and a and d show ?thesis
          by (simp add: min_distance_ext'3)
      next
        case False
        with c have d:"δ v h + d' = md" by simp
        with Cons(3,4) and a have "min_distance_ext_inv δ v (md, map ((#) h) l @ mps)" 
        proof(clarsimp simp: min_distance_ext_inv_def)
        qed(fastforce)
        with Cons and a and d show ?thesis 
          by(clarsimp simp: min_distance_ext'2)
      qed
    qed
  qed
qed




lemma min_distance_ext'_eq :
  assumes "min_distance_ext' δ v md mps xs = (d, ps)"
      and "min_distance_ext_inv δ v (md, mps)"
      and "∀(h, d', l)∈set xs. min_distance_ext_inv δ h (d', l)"
    shows "(#) v ` set ps = Min_distance_ext δ v {p. p ∈ set mps ∨ (∃(h, d', l)∈set xs. p ∈ (#) h ` set l)}"
 (is "_ = Min_distance_ext δ v (?s mps xs)")
  using assms
proof(induct xs arbitrary: md mps)
  case Nil
  then show ?case 
  proof(clarsimp simp: min_distance_ext_inv_def Min_distance_ext_def)
  qed(fastforce)
next
  case (Cons a xs)
  then show ?case
  proof clarsimp
    fix h d' l
    assume a: "a = (h, d', l)"
       and b: "min_distance_ext_inv δ h (d', l)"
    show "(#) v ` set ps = Min_distance_ext δ v {p. p ∈ set mps ∨ p ∈ (#) h ` set l ∨ 
                                                 (∃(h, d', l)∈set xs. p ∈ (#) h ` set l)}"
    (is "_ = Min_distance_ext δ v ?t")
    proof(cases "δ v h + d' > md")
      case c:True
      with Cons a and b show ?thesis
      proof(clarsimp simp: min_distance_ext'1)
        show "Min_distance_ext δ v (?s mps xs) = Min_distance_ext δ v ?t"
        proof(rule Min_distance_ext_eq, fast)
          from Cons(3,4) and b and c 
          show "∀p'∈ ?t - ?s mps xs. ∃p∈?s mps xs. path_distance δ (v#p) < path_distance δ (v#p')"
          proof(clarsimp)
          qed(metis (mono_tags, opaque_lifting) min_distance_ext_invD)
        qed
      qed
    next
      case c:False
      show ?thesis
      proof(cases "δ v h + d' < md")
        case d:True
        with Cons and a and b show ?thesis
        proof(clarsimp simp: min_distance_ext'3 min_distance_ext_inv_def)
          show "Min_distance_ext δ v {p. p ∈ (#) h ` set l ∨ (∃(h, d', l)∈set xs. p ∈ (#) h ` set l)} =
                Min_distance_ext δ v ?t"  (is "Min_distance_ext δ v ?u = _")
          proof(rule Min_distance_ext_eq, fast)
            from Cons(3,4) and b and d
            show "∀p'∈ ?t - ?u. ∃p∈?u. path_distance δ (v#p) < path_distance δ (v#p')"
            proof(clarsimp)
            qed(metis (no_types, opaque_lifting) image_eqI min_distance_ext_invD path_distance.simps(3))
          qed
        qed
      next
        case False
        with c have d:"δ v h + d' = md" by simp
        with Cons(3,4) and a have "min_distance_ext_inv δ v (md, map ((#) h) l @ mps)" 
        proof(clarsimp simp: min_distance_ext_inv_def)
        qed(fastforce)
        with Cons(1,2,4) and a and d show ?thesis
        proof(clarsimp simp: min_distance_ext'2)
        qed(meson)
      qed
    qed
  qed
qed
            


lemma min_distance_ext :
  assumes "min_distance_ext δ v xs = (d, rs)" 
      and "∀(h, d', l)∈set xs. min_distance_ext_inv δ h (d', l)"
      and "length xs > 0"
    shows "min_distance_ext_inv δ v (d, rs) ∧ 
           (#) v ` set rs = Min_distance_ext δ v {p. ∃(h, d', l)∈set xs. p ∈ (#) h ` set l}"
    (is "?A ∧ ?B")
proof(cases xs)
  case Nil
  with assms(3) show ?thesis by simp 
next
  case (Cons a ls)
  show ?thesis 
  proof
    from assms(1, 2) and Cons show "?A"
    proof(clarsimp simp: min_distance_ext_def)
    qed(smt (verit) Collect_cong case_prodI2 case_prod_conv image_iff length_greater_0_conv list.distinct(1)
        list.map_disc_iff list.set_map min_distance_ext'_inv min_distance_ext_inv_def path_distance.simps(3))
  next
    from assms(1, 2) and Cons show "?B"
    proof(clarsimp simp: min_distance_ext_def)
    qed(smt (verit) Collect_cong case_prodI2 case_prod_conv image_iff length_greater_0_conv list.distinct(1)
        list.map_disc_iff list.set_map min_distance_ext'_eq min_distance_ext_inv_def path_distance.simps(3))
  qed
qed



subsection ‹Tables›

type_synonym vertex = nat

text ‹For simplicity distances shall be represented by integers below:› 
type_synonym distance = int 

type_synonym table = "vertex × nat ⇒ distance × (vertex list) list"


text ‹The table invariant condition:›
definition table_inv :: "(vertex ⇒ vertex ⇒ distance) ⇒ nat ⇒ vertex ⇒ table ⇒ nat ⇒ bool"
  where
"table_inv δ N t T ix = 
 (∀i≤ix. ∀v∈{0..<N} - set(nat2list 0 i). 
  min_distance_ext_inv δ v (T(v, i)) ∧
  (#) v ` set(snd(T(v, i))) = opt_Hamiltonian_paths δ v (set(nat2list 0 i)) t)"


text ‹Initialising a table with edge distances from each of $\{0,\ldots,N-1\}$ to
      the destination $t$:›
fun init_tab :: "(vertex ⇒ vertex ⇒ distance) ⇒ nat ⇒ vertex ⇒ table"
  where
"init_tab δ N t = (if N = 0 then (λx. (0, [])) 
                   else (init_tab δ (N-1) t)((N-1, 0) := (δ (N-1) t, [[t]])))"



lemma table_inv_init :
"table_inv δ N t (init_tab δ N t) 0"
proof(induct N)
qed(clarsimp simp: min_distance_ext_inv_def table_inv_def nat2list.simps opt_Hamiltonian_paths0)+


declare init_tab.simps[simp del]


text ‹Update a table along the column $ix$ using the values in the preceding columns:›
definition upd_tab :: "(vertex ⇒ vertex ⇒ distance) ⇒ nat ⇒ nat ⇒ table ⇒ table" 
  where
"upd_tab δ N ix =
(let vs = nat2list 0 ix in
 let V = [0..<N] in
foldr (λv T. T((v, ix) := min_distance_ext δ v (map (λw. (w, T(w, list2nat 0 N (rem1S w vs)))) vs)))
                   (filter (λv. ¬ memS v vs) V))" 


lemma foldr_upd1 :
  assumes "∀v∈set xs. f v ≠ x"
  shows "foldr (λv T. T(f v := g v T)) xs T x = T x"
  using assms
proof(induct xs)
qed(fastforce+)


lemma foldr_upd2 :
  assumes "x ∈ set xs"
      and "∀xs. m (foldr (λv T. T((v, vs) := g v (m T))) xs T) = m T"
    shows "foldr (λv T. T((v, vs) := g v (m T))) xs T (x, vs) = g x (m T)"
  using assms
proof(induct xs)
qed(clarsimp+)


lemma table_inv_upd :
  assumes "table_inv δ N t T ix"
      and "ix < ix'"
    shows "table_inv δ N t (upd_tab δ N ix' T) ix"
  using assms 
proof(clarsimp simp add: Let_def table_inv_def upd_tab_def)
qed(simp add: foldr_upd1[where f="λx. (x, ix')"])



lemma upd_tab_app :
  assumes "vs = nat2list 0 ix"
      and "v ∈ {0..<N} - set vs" 
      and "ix < 2⇗N⇖"
    shows "upd_tab δ N ix T (v, ix) = 
           min_distance_ext δ v (map (λw. (w, T(w, list2nat 0 N (rem1S w vs)))) vs)"
  using assms unfolding upd_tab_def Let_def
proof(subst foldr_upd2; clarsimp simp add: memS nat2list_sorted)
qed(rule foldr_upd1; metis Pair_inject list2nat_rem1S_not_in)



lemma table_inv_upd_ext :
  assumes "table_inv δ N t T ix"
      and "ix + 1 < 2⇗N⇖"
    shows "table_inv δ N t (upd_tab δ N (ix+1) T) (ix+1)"
proof(clarsimp simp: table_inv_def)
  fix v i
  define vs where "vs = nat2list 0 i"
  define pix where "pix = (λw. list2nat 0 N (rem1S w vs))"
 
  assume 1:"i ≤ Suc ix"
     and 2:"v < N"
     and 3:"v ∉ set vs"
  show "min_distance_ext_inv δ v (upd_tab δ N (Suc ix) T (v, i)) ∧
   (#) v ` set (snd (upd_tab δ N (Suc ix) T (v, i))) = opt_Hamiltonian_paths δ v (set vs) t"
  proof(cases "i < ix+1")
    case True
    with vs_def and table_inv_upd and assms(1) and 2 and 3 show ?thesis
      by (metis Diff_iff Suc_eq_plus1 atLeastLessThan_iff lessI less_Suc_eq_le less_eq_nat.simps(1)
          table_inv_def)
  next
    case False
    with 1 have 4: "i = ix+1" by simp
    show ?thesis
    proof(cases "upd_tab δ N i T (v, i)")
      case 5:(Pair d rs)
      with 4 show ?thesis 
      proof(clarsimp)
        note upd_tab_app[OF refl]
        with vs_def pix_def have a:"min_distance_ext δ v (map (λw. (w, T (w, pix w))) vs) = (d, rs)"
          using "2" "3" "4" "5" assms(2) by fastforce
        from 4 and assms(2)  
        have b:"∀x∈set vs. pix x < i ∧ pix x ≤ ix ∧ x ∉ set(nat2list 0 (pix x))"
          by (metis less_eq_iff_succ_less list2nat_rem1S_less list2nat_rem1S_not_in pix_def vs_def)

        with 4 and pix_def and vs_def have pix_set: "∀x. set vs - {x} = set(nat2list 0 (pix x))"
          by (metis Diff_iff add.right_neutral assms(2) list2nat_inj nat2list_sorted nat2list_ub rem1S
              sorted_wrt_rem1S)

        from b and 1 and 4 and assms have 
        c:"∀(h, d', l)∈set (map (λw. (w, T(w, pix w))) vs). min_distance_ext_inv δ h (d', l) "
        proof(clarsimp simp: table_inv_def pix_def vs_def)
        qed(metis DiffI add_cancel_right_right atLeastLessThan_iff bot_nat_0.extremum nat2list_ub)

        note min_distance_ext[OF a c]
        with nat2list_Nil and 4 have d:
        "min_distance_ext_inv δ v (d, rs) ∧ (#) v ` set rs = 
         Min_distance_ext δ v {p. ∃x∈set vs. case T(x, pix x) of (d', l) ⇒ p ∈ (#) x ` set l}" 
          by(simp add: pix_def vs_def)

        have "Min_distance_ext δ v {p. ∃x∈set vs. case T(x, pix x) of (d', l) ⇒ p ∈ (#) x ` set l} =
              Min_distance_ext δ v (⋃x∈set vs. opt_Hamiltonian_paths δ x (set vs - {x}) t)"
                    (is "Min_distance_ext δ v ?l = Min_distance_ext δ v ?r") 
        proof -
          have e: "∀x∈set vs. (#) x ` set(snd(T(x, pix x))) = 
                  opt_Hamiltonian_paths δ x (set(nat2list 0 (pix x))) t"
            by (metis "4" Diff_iff add.right_neutral assms(1,2) atLeastLessThan_iff b le0 nat2list_ub table_inv_def
                vs_def)
          have "∀p. (p ∈ ?l) = (p ∈ ?r)"
          proof(clarsimp)
          qed(metis (lifting) case_prodE case_prodI2 e pix_set snd_eqD) 
          thus ?thesis
            by (metis (mono_tags, lifting) Collect_cong Sup_set_def mem_Collect_eq)
        qed

        with 4 and d 
        show "min_distance_ext_inv δ v (d, rs) ∧ (#) v ` set rs = opt_Hamiltonian_paths δ v (set vs) t"
          by (simp add: SUP_cong Union_eq nat2list_Nil opt_Hamiltonian_paths_fix plus_1_eq_Suc vs_def)
      qed
    qed
  qed
qed


corollary table_inv_upd_ext' :
  assumes "table_inv δ N t T (ix-1)"
      and "ix < 2⇗N⇖"
      and "ix > 0" 
    shows "table_inv δ N t (upd_tab δ N ix T) ix"
  by (metis One_nat_def assms le_add_diff_inverse2 less_eq_Suc_le table_inv_upd_ext)


text ‹Successively update the columns up to $2^n-1$ using @{term "upd_tab"}:›
function fill_tab :: "(vertex ⇒ vertex ⇒ distance) ⇒ nat ⇒ table ⇒ nat ⇒ table" 
  where
"fill_tab δ N T ix = (if ix < 2⇗N⇖ - 1 then fill_tab δ N (upd_tab δ N ix T) (ix+1)
                      else T)"
  by pat_completeness auto
termination
  by(relation "measure (λ(a, b, c, d). 2⇗b⇖ - d)", fastforce+)

declare fill_tab.simps[simp del]


lemma fill_tab :
  assumes "N > 0"
      and "ix > 0"
      and "∀ix'<ix. table_inv δ N t T ix'"
    shows "table_inv δ N t (fill_tab δ N T ix) (2⇗N⇖-2)"
  using assms
proof(induct ix arbitrary: T rule: wf_induct[where r="measure(λx. 2⇗N⇖ - x)"])
  show "wf (measure ((-) (2⇗N⇖)))" by simp
next
  case h:(2 x)
  have "table_inv δ N t (fill_tab δ N (upd_tab δ N x T) (x+1)) (2⇗N⇖ - 2)"
           if a: "x < 2⇗N⇖ - 1"
  proof(rule h(1)[rule_format, simplified])
    show "2⇗N⇖ - (x+1) < 2⇗N⇖ - x"
      using a by linarith
    next
      show "0 < N" by(rule h(2))
    next
      show "0 < x+1" by simp
    next
      fix ix' assume "ix' < x+1"
      thus "table_inv δ N t (upd_tab δ N x T) ix'"
        by (metis One_nat_def Suc_eq_plus1 Suc_pred h.prems(2,3) less_imp_diff_less not_less_iff_gr_or_eq
            not_less_less_Suc_eq table_inv_upd table_inv_upd_ext' that)
    qed
    with h(3,4) show ?case by(simp add: fill_tab.simps)
qed




subsection ‹Summing up›

definition
"tsp δ N = 
 (if N = 0 then (δ N N, [[N, N]])
  else (let T = init_tab δ N N in
        let T' = fill_tab δ N T 1 in
        let vs = nat2list 0 (2⇗N⇖-1) in
        let (d, ps) = min_distance_ext δ N (map (λw. (w, T'(w, list2nat 0 N (rem1S w vs)))) vs) in
        (d, map ((#) N) ps)))"




text ‹Without loss of generality, the salesman is assumed to reside in the location/vertex $N$
      and has to visit each of the locations $0\ldots N-1$ returning subsequently to $N$.
      Now the list(s) forming the value @{term "tsp δ N"} represent all of such Hamiltonian cycles 
      that are minimal with respect to $\delta$ as the following theorem shows:›

theorem tsp :
  assumes "tsp δ N = (d, ps)"
  shows "set ps = opt_Hamiltonian_paths δ N {0..<N} N ∧
         (∀p∈set ps. path_distance δ p = d)"
proof(cases "N = 0")
  case True
  with assms and opt_Hamiltonian_paths0 show ?thesis
    by(fastforce simp: tsp_def)
next
  define vs where "vs = nat2list 0 (2⇗N⇖ - 1)"
  define pix where "pix = (λw. list2nat 0 N (rem1S w vs))"
  define T where "T = fill_tab δ N (init_tab δ N N) 1"
  have vs1:"vs = rev[0..<N]"
    using nat2list_pred_pow2' vs_def by blast
  have pix1:"∀x∈set vs. pix x < 2⇗N⇖ - 1 ∧ x ∉ set(nat2list 0 (pix x))"
    by (simp add: list2nat_rem1S_less list2nat_rem1S_not_in pix_def vs_def)
  with pix_def and vs_def have pix_set: "∀x. set vs - {x} = set(nat2list 0 (pix x))"
    by (metis Diff_iff add.right_neutral diff_less list2nat_inj nat2list_sorted nat2list_ub
        nat_zero_less_power_iff rem1S sorted_wrt_rem1S zero_less_numeral zero_less_one)
  have pix2:"∀x∈set vs. pix x ≤ 2⇗N⇖ - 2"
    using length_pos_if_in_set pix1 by fastforce 
  from pix1 vs1 pix_set have pix3: "∀x∈set vs. {0..<N} - set (nat2list 0 (pix x)) = {x}"
    by fastforce

  case a:False
  with T_def have inv:"table_inv δ N N T (2⇗N⇖ - 2)"
    by (simp add: fill_tab table_inv_init)

  note inv[simplified table_inv_def]
  with vs1 pix1 pix2 pix_set have 
  c:"∀(h, d', l)∈set (map (λv. (v, T(v, pix v))) vs). min_distance_ext_inv δ h (d', l)" 
    by clarsimp

  from a and assms obtain ps' where 
  d:"min_distance_ext δ N (map (λv. (v, T(v, pix v))) vs) = (d, ps') ∧ ps = map ((#) N) ps'"
    by(clarsimp simp: tsp_def Let_def split_def T_def pix_def vs_def)

  note min_distance_ext[OF d[THEN conjunct1]]
  with a and c and d and vs1 have e:"min_distance_ext_inv δ N (d, ps') ∧
  set ps = Min_distance_ext δ N {p. ∃(h, d', l)∈set (map (λv. (v, T(v, pix v))) vs). p ∈ (#) h ` set l}"
    by simp

  with d have 1:"∀p∈set ps. path_distance δ p = d"
    by (smt (verit) imageE image_set min_distance_ext_invD)

  from vs1 pix_set pix2 pix3 set_rev[of vs] inv[simplified table_inv_def]
  have f:"∀p. (∃v∈{0..<N}. case T(v, pix v) of (d', l) ⇒ p ∈ (#) v ` set l) =
            (∃v∈{0..<N}. p ∈ opt_Hamiltonian_paths δ v ({0..<N} - {v}) N)"
    by (smt (verit) atLeastLessThan_upt case_prodE case_prodI2 insertCI rev_rev_ident snd_eqD)

  have "{p. ∃x∈set vs. case T (x, pix x) of (d', l) ⇒ p ∈ (#) x ` set l} =
        (⋃v∈{0..<N}. opt_Hamiltonian_paths δ v ({0..<N} - {v}) N)"
  proof(rule set_eqI)
  qed(clarsimp simp: f vs1)

  with a and e and 1 show ?thesis
  proof(subst opt_Hamiltonian_paths_fix) 
  qed(simp+)

qed




subsection ‹An example›

text ‹An asymmetric edge distance function:›
definition "δ (u :: vertex) (v :: vertex) = 
(if u = 0 then (if v = 1 then 9
                else (if v = 2 then 10
                      else (if v = 3 then 5 else 0)))
 else (if u = 1 then (if v = 0 then 13
                      else (if v = 2 then 12
                            else (if v = 3 then 6 else 0)))
       else (if u = 2 then (if v = 0 then 8
                            else (if v = 1 then 9
                                  else (if v = 3 then 8 else 0)))
             else (if u = 3 then (if v = 0 then 10
                                  else (if v = 1 then 15
                                        else (if v = 2 then 20 else 0)))
                   else 0))))"

text ‹For this $\delta$ there is exactly one optimal Hamiltonian cycle that starts/ends in $3$ 
      passing through each of the vertices $0, 1, 2$ once:›
value "tsp δ 3"


end