Session Timed_Automata

Theory Floyd_Warshall

theory Floyd_Warshall
  imports Main
begin

chapter ‹Floyd-Warshall Algorithm for the All-Pairs Shortest Paths Problem›

subsubsection ‹Auxiliary›

lemma distinct_list_single_elem_decomp: "{xs. set xs  {0}  distinct xs} = {[], [0]}"
proof (standard, goal_cases)
  case 1
  { fix xs :: "'a list" assume xs: "xs  {xs. set xs  {0}  distinct xs}"
    have "xs  {[], [0]}"
    proof (cases xs)
      case (Cons y ys)
      hence y: "y = 0" using xs by auto
      with Cons xs have "ys = []" by (cases ys, auto)
      thus ?thesis using y Cons by simp
    qed simp
  }
  thus ?case by blast
qed simp


section ‹Cycles in Lists›

abbreviation "cnt x xs  length (filter (λy. x = y) xs)"

fun remove_cycles :: "'a list  'a  'a list  'a list"
where
  "remove_cycles [] _ acc = rev acc" |
  "remove_cycles (x#xs) y acc =
    (if x = y then remove_cycles xs y [x] else remove_cycles xs y (x#acc))"

lemma cnt_rev: "cnt x (rev xs) = cnt x xs" by (metis length_rev rev_filter)

value "as @ [x] @ bs @ [x] @ cs @ [x] @ ds"

lemma remove_cycles_removes: "cnt x (remove_cycles xs x ys)  max 1 (cnt x ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case
  by (simp, cases "x  set ys", (auto simp: cnt_rev[of x ys]))
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True
    thus ?thesis using Cons[of "[y]"] True by auto
  next
    case False
    thus ?thesis using Cons[of "y # ys"] by auto
  qed
qed

lemma remove_cycles_id: "x  set xs  remove_cycles xs x ys = rev ys @ xs"
by (induction xs arbitrary: ys) auto

lemma remove_cycles_cnt_id:
  "x  y  cnt y (remove_cycles xs x ys)  cnt y ys + cnt y xs"
proof (induction xs arbitrary: ys x)
  case Nil thus ?case by (simp add: cnt_rev)
next
  case (Cons z xs)
  thus ?case
  proof (cases "x = z")
    case True thus ?thesis using Cons.IH[of z "[z]"] Cons.prems by auto
  next
    case False
    thus ?thesis using Cons.IH[of x "z # ys"] Cons.prems False by auto
  qed
qed

lemma remove_cycles_ends_cycle: "remove_cycles xs x ys  rev ys @ xs  x  set xs"
using remove_cycles_id by fastforce

lemma remove_cycles_begins_with: "x  set xs   zs. remove_cycles xs x ys = x # zs  x  set zs"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True thus ?thesis
    proof (cases "x  set xs", goal_cases)
      case 1 with Cons show ?case by auto
    next
      case 2 with remove_cycles_id[of x xs "[y]"] show ?case by auto
    qed
  next
    case False
    with Cons show ?thesis by auto
  qed
qed

lemma remove_cycles_self:
  "x  set xs  remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys"
proof -
  assume x:"x  set xs"
  then obtain ws where ws: "remove_cycles xs x ys = x # ws" "x  set ws"
  using remove_cycles_begins_with[OF x, of ys] by blast
  from remove_cycles_id[OF this(2)] have "remove_cycles ws x [x] = x # ws" by auto
  with ws(1) show "remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys" by simp
qed

lemma remove_cycles_one: "remove_cycles (as @ x # xs) x ys = remove_cycles (x#xs) x ys"
by (induction as arbitrary: ys) auto

lemma remove_cycles_cycles:
  "x  set xs   xxs as. as @ concat (map (λ xs. x # xs) xxs) @ remove_cycles xs x ys = xs  x  set as"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True thus ?thesis
    proof (cases "x  set xs", goal_cases)
      case 1
      then obtain as xxs where "as @ concat (map (λxs. y#xs) xxs) @ remove_cycles xs y [y] = xs"
      using Cons.IH[of "[y]"] by auto
      hence "[] @ concat (map (λxs. x#xs) (as#xxs)) @ remove_cycles (y#xs) x ys = y # xs"
      by (simp add: x = y)
      thus ?thesis by fastforce
    next
      case 2
      hence "remove_cycles (y # xs) x ys = y # xs" using remove_cycles_id[of x xs "[y]"] by auto
      hence "[] @ concat (map (λxs. x # xs) []) @ remove_cycles (y#xs) x ys = y # xs" by auto
      thus ?thesis by fastforce
    qed
  next
    case False
    then obtain as xxs where as:
      "as @ concat (map (λxs. x # xs) xxs) @ remove_cycles xs x (y#ys) = xs" "x  set as"
    using Cons.IH[of "y # ys"] Cons.prems by auto
    hence "(y # as) @ concat (map (λxs. x # xs) xxs) @ remove_cycles (y#xs) x ys = y # xs"
    using x  y by auto
    thus ?thesis using as(2) x  y by fastforce
  qed
qed

fun start_remove :: "'a list  'a  'a list  'a list"
where
  "start_remove [] _ acc = rev acc" |
  "start_remove (x#xs) y acc =
    (if x = y then rev acc @ remove_cycles xs y [y] else start_remove xs y (x # acc))"

lemma start_remove_decomp:
  "x  set xs   as bs. xs = as @ x # bs  start_remove xs x ys = rev ys @ as @ remove_cycles bs x [x]"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  proof (auto, goal_cases)
    case 1
    from 1(1)[of "y # ys"]
    obtain as bs where 
      "xs = as @ x # bs" "start_remove xs x (y # ys) = rev (y # ys) @ as @ remove_cycles bs x [x]"
    by blast
    hence "y # xs = (y # as) @ x # bs"
          "start_remove xs x (y # ys) = rev ys @ (y # as) @ remove_cycles bs x [x]" by simp+
    thus ?case by blast
  qed
qed

lemma start_remove_removes: "cnt x (start_remove xs x ys)  Suc (cnt x ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case using cnt_rev[of x ys] by auto
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True
    thus ?thesis using remove_cycles_removes[of y xs "[y]"] cnt_rev[of y ys] by auto
  next
    case False
    thus ?thesis using Cons[of "y # ys"] by auto
  qed
qed

lemma start_remove_id[simp]: "x  set xs  start_remove xs x ys = rev ys @ xs"
by (induction xs arbitrary: ys) auto

lemma start_remove_cnt_id:
  "x  y  cnt y (start_remove xs x ys)  cnt y ys + cnt y xs"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by (simp add: cnt_rev)
next
  case (Cons z xs)
  thus ?case
  proof (cases "x = z", goal_cases)
    case 1 thus ?case using remove_cycles_cnt_id[of x y xs "[x]"] by (simp add: cnt_rev)
  next
    case 2 from this(1)[of "(z # ys)"] this(2,3) show ?case by auto
  qed
qed

fun remove_all_cycles :: "'a list  'a list  'a list"
where
  "remove_all_cycles [] xs = xs" |
  "remove_all_cycles (x # xs) ys = remove_all_cycles xs (start_remove ys x [])"

lemma cnt_remove_all_mono:"cnt y (remove_all_cycles xs ys)  max 1 (cnt y ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  thus ?case
  proof (cases "x = y")
    case True thus ?thesis using start_remove_removes[of y ys "[]"] Cons[of "start_remove ys y []"]
    by auto
  next
    case False
    hence "cnt y (start_remove ys x [])  cnt y ys"
    using start_remove_cnt_id[of x y ys "[]"] by auto
    thus ?thesis using Cons[of "start_remove ys x []"] by auto
  qed
qed


lemma cnt_remove_all_cycles: "x  set xs  cnt x (remove_all_cycles xs ys)  1"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  using start_remove_removes[of x ys "[]"] cnt_remove_all_mono[of y xs "start_remove ys y []"]
  by auto
qed

lemma cnt_mono:
  "cnt a (b # xs)  cnt a (b # c # xs)"
by (induction xs) auto
  
lemma cnt_distinct_intro: " x  set xs. cnt x xs  1  distinct xs"
proof (induction xs)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  from this(2) have " x  set xs. cnt x xs  1"
  by (metis filter.simps(2) impossible_Cons linorder_class.linear list.set_intros(2)
      preorder_class.order_trans)
  with Cons.IH have "distinct xs" by auto
  moreover have "x  set xs" using Cons.prems
  proof (induction xs)
    case Nil then show ?case by auto
  next
    case (Cons a xs)
    from this(2) have "xaset (x # xs). cnt xa (x # a # xs)  1"
    by auto
    then have *: "xaset (x # xs). cnt xa (x # xs)  1"
    proof (safe, goal_cases)
      case (1 b)
      then have "cnt b (x # a # xs)  1" by auto
      with cnt_mono[of b x xs a] show ?case by fastforce
    qed
    with Cons(1) have "x  set xs" by auto
    moreover have "x  a"
    by (metis (full_types) Cons.prems One_nat_def * empty_iff filter.simps(2) impossible_Cons
                           le_0_eq le_Suc_eq length_0_conv list.set(1) list.set_intros(1)) 
    ultimately show ?case by auto
  qed
  ultimately show ?case by auto
qed

lemma remove_cycles_subs:
  "set (remove_cycles xs x ys)  set xs  set ys"
by (induction xs arbitrary: ys; auto; fastforce)

lemma start_remove_subs:
  "set (start_remove xs x ys)  set xs  set ys"
using remove_cycles_subs by (induction xs arbitrary: ys; auto; fastforce)

lemma remove_all_cycles_subs:
  "set (remove_all_cycles xs ys)  set ys"
using start_remove_subs by (induction xs arbitrary: ys, auto) (fastforce+)

lemma remove_all_cycles_distinct: "set ys  set xs  distinct (remove_all_cycles xs ys)"
proof -
  assume "set ys  set xs"
  hence " x  set ys. cnt x (remove_all_cycles xs ys)  1" using cnt_remove_all_cycles by fastforce
  hence " x  set (remove_all_cycles xs ys). cnt x (remove_all_cycles xs ys)  1"
  using remove_all_cycles_subs by fastforce
  thus "distinct (remove_all_cycles xs ys)" using cnt_distinct_intro by auto
qed

lemma distinct_remove_cycles_inv: "distinct (xs @ ys)  distinct (remove_cycles xs x ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case by auto
qed

definition "remove_all x xs = (if x  set xs then tl (remove_cycles xs x []) else xs)"

definition "remove_all_rev x xs = (if x  set xs then rev (tl (remove_cycles (rev xs) x [])) else xs)"

lemma remove_all_distinct:
  "distinct xs  distinct (x # remove_all x xs)"
proof (cases "x  set xs", goal_cases)
  case 1
  from remove_cycles_begins_with[OF 1(2), of "[]"] obtain zs
  where "remove_cycles xs x [] = x # zs" "x  set zs" by auto
  thus ?thesis using 1(1) distinct_remove_cycles_inv[of "xs" "[]" x] by (simp add: remove_all_def)
next
  case 2 thus ?thesis by (simp add: remove_all_def)
qed

lemma remove_all_removes:
  "x  set (remove_all x xs)"
by (metis list.sel(3) remove_all_def remove_cycles_begins_with)

lemma remove_all_subs:
  "set (remove_all x xs)  set xs"
using remove_cycles_subs remove_all_def
by (metis (no_types, lifting) append_Nil2 list.sel(2) list.set_sel(2) set_append subsetCE subsetI)

lemma remove_all_rev_distinct: "distinct xs  distinct (x # remove_all_rev x xs)"
proof (cases "x  set xs", goal_cases)
  case 1
  then have "x  set (rev xs)" by auto
  from remove_cycles_begins_with[OF this, of "[]"] obtain zs
  where "remove_cycles (rev xs) x [] = x # zs" "x  set zs" by auto
  thus ?thesis using 1(1) distinct_remove_cycles_inv[of "rev xs" "[]" x] by (simp add: remove_all_rev_def)
next
  case 2 thus ?thesis by (simp add: remove_all_rev_def)
qed

lemma remove_all_rev_removes: "x  set (remove_all_rev x xs)"
by (metis remove_all_def remove_all_removes remove_all_rev_def set_rev)

lemma remove_all_rev_subs: "set (remove_all_rev x xs)  set xs"
by (metis remove_all_def remove_all_subs set_rev remove_all_rev_def)

abbreviation "rem_cycles i j xs  remove_all i (remove_all_rev j (remove_all_cycles xs xs))"

lemma rem_cycles_distinct': "i  j  distinct (i # j # rem_cycles i j xs)"
proof -
  assume "i  j"
  have "distinct (remove_all_cycles xs xs)" by (simp add: remove_all_cycles_distinct)
  from remove_all_rev_distinct[OF this] have
    "distinct (remove_all_rev j (remove_all_cycles xs xs))"
  by simp
  from remove_all_distinct[OF this] have "distinct (i # rem_cycles i j xs)" by simp
  moreover have
    "j  set (rem_cycles i j xs)"
  using remove_all_subs remove_all_rev_removes remove_all_removes by fastforce
  ultimately show ?thesis by (simp add: i  j)
qed

lemma rem_cycles_removes_last: "j  set (rem_cycles i j xs)"
by (meson remove_all_rev_removes remove_all_subs rev_subsetD)

lemma rem_cycles_distinct: "distinct (rem_cycles i j xs)"
by (meson distinct.simps(2) order_refl remove_all_cycles_distinct
          remove_all_distinct remove_all_rev_distinct) 

lemma rem_cycles_subs: "set (rem_cycles i j xs)  set xs"
by (meson order_trans remove_all_cycles_subs remove_all_subs remove_all_rev_subs)

section ‹Definition of the Algorithm›

text ‹
  We formalize the Floyd-Warshall algorithm on a linearly ordered abelian semigroup.
  However, we would not need an abelian› monoid if we had the right type class.
›

class linordered_ab_monoid_add = linordered_ab_semigroup_add +
  fixes neutral :: 'a ("𝟭")
    assumes neutl[simp]: "𝟭 + x = x"
    assumes neutr[simp]: "x + 𝟭 = x"
begin

lemmas assoc = add.assoc

type_synonym 'c mat = "nat  nat  'c"

definition (in -) upd :: "'c mat  nat  nat  'c  'c mat"
where
  "upd m x y v = m (x := (m x) (y := v))"

definition fw_upd :: "'a mat  nat  nat  nat  'a mat" where
  "fw_upd m k i j  upd m i j (min (m i j) (m i k + m k j))"

lemma fw_upd_mono:
  "fw_upd m k i j i' j'  m i' j'" 
by (cases "i = i'", cases "j = j'") (auto simp: fw_upd_def upd_def)

fun fw :: "'a mat  nat  nat  nat  nat  'a mat" where
  "fw m n 0       0       0        = fw_upd m 0 0 0" |
  "fw m n (Suc k) 0       0        = fw_upd (fw m n k n n) (Suc k) 0 0" |
  "fw m n k       (Suc i) 0        = fw_upd (fw m n k i n) k (Suc i) 0" |
  "fw m n k       i       (Suc j)  = fw_upd (fw m n k i j) k i (Suc j)"

lemma fw_invariant_aux_1:
  "j''  j  i  n  j  n  k  n  fw m n k i j i' j'  fw m n k i j'' i' j'"
proof (induction j)
  case 0 thus ?case by simp
next
  case (Suc j) thus ?case
  proof (cases "j'' = Suc j")
    case True thus ?thesis by simp
  next
    case False
    have "fw_upd (fw m n k i j) k i (Suc j) i' j'  fw m n k i j i' j'" by (simp add: fw_upd_mono)
    thus ?thesis using Suc False by simp
  qed
qed

lemma fw_invariant_aux_2:
  "i  n  j  n  k  n  i''  i  j''  j
    fw m n k i j i' j'  fw m n k i'' j'' i' j'"
proof (induction i)
  case 0 thus ?case using fw_invariant_aux_1 by auto
next
  case (Suc i) thus ?case
  proof (cases "i'' = Suc i")
    case True thus ?thesis using Suc fw_invariant_aux_1 by simp
  next
    case False
    have "fw m n k (Suc i) j i' j'  fw m n k (Suc i) 0 i' j'"
    using fw_invariant_aux_1[of 0 j "Suc i" n k] Suc(2-) by simp
    also have "  fw m n k i n i' j'" by (simp add: fw_upd_mono)
    also have "  fw m n k i j i' j'" using fw_invariant_aux_1[of j n i n k] False Suc by simp
    also have "  fw m n k i'' j'' i' j'" using Suc False by simp
    finally show ?thesis by simp
  qed
qed

lemma fw_invariant:
  "k'  k  i  n  j  n  k  n  j''  j  i''  i
    fw m n k i j i' j'  fw m n k' i'' j'' i' j'"
proof (induction k)
  case 0 thus ?case using fw_invariant_aux_2 by auto
next
  case (Suc k) thus ?case
  proof (cases "k' = Suc k")
    case True thus ?thesis using Suc fw_invariant_aux_2 by simp
  next
    case False
    have "fw m n (Suc k) i j i' j'  fw m n (Suc k) 0 0 i' j'"
    using fw_invariant_aux_2[of i n j "Suc k" 0 0] Suc(2-) by simp
    also have "  fw m n k n n i' j'" by (simp add: fw_upd_mono)
    also have "  fw m n k i j i' j'" using fw_invariant_aux_2[of n n n k] False Suc by simp
    also have "  fw m n k' i'' j'' i' j'" using Suc False by simp
    finally show ?thesis by simp
  qed
qed

lemma single_row_inv:
  "j' < j  j  n  i'  n  fw m n k i' j i' j' = fw m n k i' j' i' j'"
proof (induction j)
  case 0 thus ?case by simp
next
  case (Suc j) thus ?case by (cases "j' = j") (simp add: fw_upd_def upd_def)+
qed

lemma single_iteration_inv':
  "i' < i  j'  n  j  n  i  n  fw m n k i j i' j' = fw m n k i' j' i' j'"
proof (induction i arbitrary: j)
  case 0 thus ?case by simp
next
  case (Suc i) thus ?case
  proof (induction j)
    case 0 thus ?case
    proof (cases "i = i'", goal_cases)
      case 2 thus ?case by (simp add: fw_upd_def upd_def)
    next
      case 1 thus ?case using single_row_inv[of j' n n i' m k] 
      by (cases "j' = n") (fastforce simp add: fw_upd_def upd_def)+
    qed
  next
    case (Suc j) thus ?case by (simp add: fw_upd_def upd_def)
  qed
qed

lemma single_iteration_inv:
  "i'  i  j'  j  i  n  j  n fw m n k i j i' j' = fw m n k i' j' i' j'"
proof (induction i arbitrary: j)
  case 0 thus ?case
  proof (induction j)
    case 0 thus ?case by simp
  next
    case (Suc j) thus ?case using 0 by (cases "j' = Suc j") (simp add: fw_upd_def upd_def)+
  qed
next
  case (Suc i) thus ?case
  proof (induction j)
    case 0 thus ?case by (cases "i' = Suc i") (simp add: fw_upd_def upd_def)+
  next
    case (Suc j) thus ?case
    proof (cases "i' = Suc i", goal_cases)
      case 1 thus ?case
      proof (cases "j' = Suc j", goal_cases)
        case 1 thus ?case by simp
      next
        case 2 thus ?case by (simp add: fw_upd_def upd_def)
      qed
    next
      case 2 thus ?case
      proof (cases "j' = Suc j", goal_cases)
        case 1 thus ?case using single_iteration_inv'[of i' "Suc i" j' n "Suc j" m k] by simp
      next
        case 2 thus ?case by (simp add: fw_upd_def upd_def)
      qed
    qed
  qed
qed

lemma fw_innermost_id:
  "i  n  j  n  j'  n  i' < i  fw m n 0 i' j' i j = m i j"
proof (induction i' arbitrary: j')
  case 0 thus ?case
  proof (induction j')
    case 0 thus ?case by (simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def)
  qed
next
  case (Suc i') thus ?case
  proof (induction j')
    case 0 thus ?case by (auto simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def)
  qed
qed

lemma fw_middle_id:
  "i  n  j  n  j' < j  i'  i  fw m n 0 i' j' i j = m i j"
proof (induction i' arbitrary: j')
  case 0 thus ?case
  proof (induction j')
    case 0 thus ?case by (simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def)
  qed
next
  case (Suc i') thus ?case
  proof (induction j')
    case 0 thus ?case using fw_innermost_id by (auto simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def)
  qed
qed

lemma fw_outermost_mono:
  "i  n  j  n  fw m n 0 i j i j  m i j"
proof (cases j)
  case 0
  assume "i  n"
  thus ?thesis
  proof (cases i)
    case 0 thus ?thesis using j = 0 by (simp add: fw_upd_def upd_def)
  next
    case (Suc i')
    hence "fw m n 0 i' n (Suc i') 0 = m (Suc i') 0" using fw_innermost_id[of "Suc i'" n 0 n i' m]
    using i  n by simp
    thus ?thesis using j = 0 Suc by (simp add: fw_upd_def upd_def)
  qed
next
  case (Suc j')
  assume "i  n" "j  n"
  hence "fw m n 0 i j' i (Suc j') = m i (Suc j')"
  using fw_middle_id[of i n "Suc j'" j' i m] Suc by simp
  thus ?thesis using Suc by (simp add: fw_upd_def upd_def)
qed

lemma Suc_innermost_id1:
  "i  n  j  n  j'  n  i' < i  fw m n (Suc k) i' j' i j = fw m n k i j i j"
proof (induction i' arbitrary: j')
  case 0 thus ?case
  proof (induction j')
    case 0
    hence "fw m n k n n i j = fw m n k i j i j" using single_iteration_inv[of i n j n n m k] by simp
    thus ?case using 0 by (simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def)
  qed
next
  case (Suc i') thus ?case
  proof (induction j')
    case 0 thus ?case by (auto simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def)
  qed
qed

lemma Suc_innermost_id2:
  "i  n  j  n  j' < j  i'  i  fw m n (Suc k) i' j' i j = fw m n k i j i j"
proof (induction i' arbitrary: j')
  case 0
  hence "fw m n k n n i j = fw m n k i j i j" using single_iteration_inv[of i n j n n m k] by simp
  with 0 show ?case
  proof (induction j')
    case 0
    thus ?case by (auto simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def)
  qed
next
  case (Suc i') thus ?case
  proof (induction j')
    case 0 thus ?case using Suc_innermost_id1 by (auto simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def)
  qed
qed

lemma Suc_innermost_id1':
  "i  n  j  n  j'  n  i' < i  fw m n (Suc k) i' j' i j = fw m n k n n i j"
proof goal_cases
  case 1
  hence "fw m n (Suc k) i' j' i j = fw m n k i j i j" using Suc_innermost_id1 by simp
  thus ?thesis using 1 single_iteration_inv[of i n] by simp
qed

lemma Suc_innermost_id2':
  "i  n  j  n  j' < j  i'  i  fw m n (Suc k) i' j' i j = fw m n k n n i j"
proof goal_cases
  case 1
  hence "fw m n (Suc k) i' j' i j = fw m n k i j i j" using Suc_innermost_id2 by simp
  thus ?thesis using 1 single_iteration_inv[of i n] by simp
qed

lemma Suc_innermost_mono:
  "i  n  j  n  fw m n (Suc k) i j i j  fw m n k i j i j"
proof (cases j)
  case 0
  assume "i  n"
  thus ?thesis
  proof (cases i)
    case 0 thus ?thesis using j = 0 single_iteration_inv[of 0 n 0 n n m k]
    by (simp add: fw_upd_def upd_def)
  next
    case (Suc i')
    thus ?thesis using Suc_innermost_id1 i  n j = 0
    by (auto simp: fw_upd_def upd_def local.min.coboundedI1)
  qed
next
  case (Suc j')
  assume "i  n" "j  n"
  thus ?thesis using Suc Suc_innermost_id2 by (auto simp: fw_upd_def upd_def local.min.coboundedI1)
qed

lemma fw_mono':
  "i  n  j  n  fw m n k i j i j  m i j"
proof (induction k)
  case 0 thus ?case using fw_outermost_mono by simp
next
  case (Suc k) thus ?case using Suc_innermost_mono[OF Suc.prems, of m k] by simp
qed

lemma fw_mono:
  "i  n  j  n  i'  n  j'  n  fw m n k i j i' j'  m i' j'"
proof (cases k)
  case 0
  assume 0: "i  n" "j  n" "i'  n" "j'  n" "k = 0"
  thus ?thesis
  proof (cases "i'  i")
    case False thus ?thesis using 0 fw_innermost_id by simp
  next
    case True thus ?thesis
    proof (cases "j'  j")
      case True
      have "fw m n 0 i j i' j'  fw m n 0 i' j' i' j'" using fw_invariant True i'  i 0 by simp
      also have "fw m n 0 i' j' i' j'  m i' j'" using 0 fw_outermost_mono by blast
      finally show ?thesis by (simp add: k = 0)
    next
      case False thus ?thesis
      proof (cases "i = i'", goal_cases)
        case 1 then show ?thesis using fw_middle_id[of i' n j' j i' m] 0 by simp
      next
        case 2
        then show ?case
        using single_iteration_inv'[of i' i j' n j m 0] i'  i fw_middle_id[of i' n j' j i' m]
              fw_outermost_mono[of i' n j' m] 0
        by simp
      qed
    qed
  qed
next
  case (Suc k)
  assume prems: "i  n" "j  n" "i'  n" "j'  n"
  thus ?thesis
  proof (cases "i'  i  j'  j")
    case True
    hence "fw m n (Suc k) i j i' j' = fw m n (Suc k) i' j' i' j'"
    using prems single_iteration_inv by blast
    thus ?thesis using Suc prems fw_mono' by auto
  next
    case False thus ?thesis
    proof auto
      assume "¬ i'  i"
      thus ?thesis using Suc prems fw_mono' Suc_innermost_id1 by auto
    next
      assume "¬ j'  j"
      hence "j < j'" by simp
      show ?thesis
      proof (cases "i  i'")
        case True
        thus ?thesis using Suc prems Suc_innermost_id2 j < j' fw_mono' by auto
      next
        case False
        thus ?thesis using single_iteration_inv' Suc prems fw_mono' by auto
      qed
    qed
  qed
qed

lemma add_mono_neutr:
  assumes "𝟭  b"
  shows "a  a + b"
using neutr add_mono assms by force

lemma add_mono_neutl:
  assumes "𝟭  b"
  shows "a  b + a"
using neutr add_mono assms by force

lemma fw_step_0:
  "m 0 0  𝟭  i  n  j  n  fw m n 0 i j i j = min (m i j) (m i 0 + m 0 j)"
proof (induction i)
  case 0 thus ?case
  proof (cases j)
    case 0 thus ?thesis by (simp add: fw_upd_def upd_def)
  next
    case (Suc j)
    hence "fw m n 0 0 j 0 (Suc j) = m 0 (Suc j)" using 0 fw_middle_id[of 0 n "Suc j" j 0 m] by fast
    moreover have "fw m n 0 0 j 0 0 = m 0 0" using single_iteration_inv[of 0 0 0 j n m 0] Suc 0
    by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl)
    ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def)
  qed
next
  case (Suc i)
  note A = this
  show ?case
  proof (cases j)
    case 0
    have "fw m n 0 i n (Suc i) 0 = m (Suc i) 0" using fw_innermost_id[of "Suc i" n 0 n i m] Suc by simp
    moreover have "fw m n 0 i n 0 0 = m 0 0" using Suc single_iteration_inv[of 0 i 0 n n m 0]
    by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl)
    ultimately show ?thesis using 0 by (simp add: fw_upd_def upd_def)
  next
    case (Suc j)
    have *: "fw m n 0 0 j 0 0 = m 0 0" using single_iteration_inv[ of 0 0 0 j n m 0] A Suc
    by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl)
    have **: "fw m n 0 i n 0 0 = m 0 0" using single_iteration_inv[of 0 i 0 n n m 0] A
    by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl)
    have "m 0 (Suc j) = fw_upd m 0 0 (Suc j) 0 (Suc j)" using m 0 0 >= 𝟭
    by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl)
    also have " = fw m n 0 0 (Suc j) 0 (Suc j)" using fw_middle_id[of 0 n "Suc j" j 0 m] Suc A(4)
    by (simp add: fw_upd_def upd_def *)
    finally have ***: "fw m n 0 (Suc i) j 0 (Suc j) = m 0 (Suc j)"
    using single_iteration_inv'[of 0 "Suc i" "Suc j" n j m 0] A Suc by simp
    have "m (Suc i) 0 = fw_upd m 0 (Suc i) 0 (Suc i) 0" using m 0 0 >= 𝟭
    by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutr)
    also have " = fw m n 0 (Suc i) 0 (Suc i) 0"
    using fw_innermost_id[of "Suc i" n 0 n i m] ‹Suc i  n ** by (simp add: fw_upd_def upd_def)
    finally have "fw m n 0 (Suc i) j (Suc i) 0 = m (Suc i) 0"
    using single_iteration_inv A Suc by auto
    moreover have "fw m n 0 (Suc i) j (Suc i) (Suc j) = m (Suc i) (Suc j)"
    using fw_middle_id A Suc by simp
    ultimately show ?thesis using Suc *** by (simp add: fw_upd_def upd_def)
  qed
qed

lemma fw_step_Suc:
  " k'n. fw m n k n n k' k'  𝟭  i  n  j  n  Suc k  n
     fw m n (Suc k) i j i j = min (fw m n k n n i j) (fw m n k n n i (Suc k) + fw m n k n n (Suc k) j)"
proof (induction i)
  case 0 thus ?case
  proof (cases j)
    case 0 thus ?thesis by (simp add: fw_upd_def upd_def)
  next
    case (Suc j)
    then have
      "fw m n k n n 0 (Suc j) = fw m n (Suc k) 0 j 0 (Suc j)"
    using 0(2-) Suc_innermost_id2' by simp
    moreover have "fw m n (Suc k) 0 j 0 (Suc k) = fw m n k n n 0 (Suc k)"
    proof (cases "j < Suc k")
      case True thus ?thesis using 0 Suc_innermost_id2' by simp
    next
      case False
      hence
        "fw m n (Suc k) 0 k 0 (Suc k) = fw m n k n n 0 (Suc k)"
      using 0(2-) Suc Suc_innermost_id2' by simp
      moreover have "fw m n (Suc k) 0 k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
      using 0(2-) Suc Suc_innermost_id2' by simp
      moreover have "fw m n (Suc k) 0 j 0 (Suc k) = fw m n (Suc k) 0 (Suc k) 0 (Suc k)"
      using False single_iteration_inv 0(2-) Suc by force
      ultimately show ?thesis using 0(1)
      by (auto simp add: fw_upd_def upd_def ‹Suc k  n min_def intro: add_mono_neutr)
    qed
    moreover have "fw m n k n n (Suc k) (Suc j) = fw m n (Suc k) 0 j (Suc k) (Suc j)"
    using 0(2-) Suc Suc_innermost_id2' by simp
    ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def)
  qed
next
  case (Suc i)
  note A = this
  show ?case
  proof (cases j)
    case 0
    hence
      "fw m n (Suc k) i n (Suc i) 0 = fw m n k n n (Suc i) 0"
    using Suc_innermost_id1' ‹Suc i  n by simp
    moreover have "fw m n (Suc k) i n (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)"
    using Suc_innermost_id1' A(3,5) by simp
    moreover have "fw m n (Suc k) i n (Suc k) 0 = fw m n k n n (Suc k) 0"
    proof (cases "i < Suc k")
      case True thus ?thesis using Suc_innermost_id1' A(3,5) by simp
    next
      case False
      have "fw m n (Suc k) k n (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
      using Suc_innermost_id1' ‹Suc i  n False by simp
      moreover have "fw m n (Suc k) k n (Suc k) 0 = fw m n k n n (Suc k) 0"
      using Suc_innermost_id1' ‹Suc i  n False by simp
      moreover have "fw m n (Suc k) i n (Suc k) 0 = fw m n (Suc k) (Suc k) 0 (Suc k) 0"
      using single_iteration_inv ‹Suc i  n False by simp
      ultimately show ?thesis using Suc(2)
      by (auto simp add: fw_upd_def upd_def ‹Suc k  n min_def intro: add_mono_neutl)
    qed
    ultimately show ?thesis using 0 by (simp add: fw_upd_def upd_def)
  next
    case (Suc j)
    hence "fw m n (Suc k) (Suc i) j (Suc i) (Suc j) = fw m n k n n (Suc i) (Suc j)"
    using Suc_innermost_id2' A(3,4) by simp
    moreover have "fw m n (Suc k) (Suc i) j (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)"
    proof (cases "j < Suc k")
      case True thus ?thesis using Suc A(3-) Suc_innermost_id2' by simp
    next
      case False
      have *:"fw m n (Suc k) (Suc i) k (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)"
      using Suc_innermost_id2' A(3,5) by simp
      have **:"fw m n (Suc k) (Suc i) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
      proof (cases "Suc i  Suc k")
        case True thus ?thesis using Suc_innermost_id2' A(5) by simp
      next
        case False
        hence "fw m n (Suc k) (Suc i) k (Suc k) (Suc k) = fw m n (Suc k) (Suc k) (Suc k) (Suc k) (Suc k)"
        using single_iteration_inv'[of "Suc k" "Suc i" "Suc k" n k m "Suc k"] A(3) by simp
        moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
        using Suc_innermost_id2' A(5) by simp
        ultimately show ?thesis using A(2)
        by (auto simp add: fw_upd_def upd_def ‹Suc k  n min_def intro: add_mono_neutl)
      qed
      have "fw m n (Suc k) (Suc i) j (Suc i) (Suc k) = fw m n (Suc k) (Suc i) (Suc k) (Suc i) (Suc k)"
      using False single_iteration_inv[of "Suc i" "Suc i" "Suc k" j n m "Suc k"] A(3-) Suc by simp
      also have " = fw m n k n n (Suc i) (Suc k)" using * ** A(2)
      by (auto simp add: fw_upd_def upd_def ‹Suc k  n min_def intro: add_mono_neutr)
      finally show ?thesis by simp
    qed
    moreover have "fw m n (Suc k) (Suc i) j (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)"
    proof (cases "Suc i  Suc k")
      case True thus ?thesis using Suc_innermost_id2' Suc A(3-5) by simp
    next
      case False
      have "fw m n (Suc k) (Suc k) j (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
      proof (cases "j < Suc k")
        case True thus ?thesis using Suc_innermost_id2' A(5) by simp
      next
        case False
        hence "fw m n (Suc k) (Suc k) j (Suc k) (Suc k) = fw m n (Suc k) (Suc k) (Suc k) (Suc k) (Suc k)"
        using single_iteration_inv A(3,4) Suc by simp
        moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
        using Suc_innermost_id2' A(5) by simp
        ultimately show ?thesis using A(2)
        by (auto simp add: fw_upd_def upd_def ‹Suc k  n min_def intro: add_mono_neutl)
      qed
      moreover have "fw m n (Suc k) (Suc k) j (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)"
      using Suc_innermost_id2' Suc A(3-5) by simp
      ultimately have "fw m n (Suc k) (Suc k) (Suc j) (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)"
      using A(2) by (auto simp add: fw_upd_def upd_def ‹Suc k  n min_def intro: add_mono_neutl)
      moreover have "fw m n (Suc k) (Suc i) j (Suc k) (Suc j) = fw m n (Suc k) (Suc k) (Suc j) (Suc k) (Suc j)"
      using single_iteration_inv'[of "Suc k" "Suc i" "Suc j" n j m "Suc k"] Suc A(3-) False  by simp
      moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
      using Suc_innermost_id2' A(5) by simp
      ultimately show ?thesis using A(2) by (simp add: fw_upd_def upd_def)
    qed
    ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def)
  qed
qed


subsection ‹Length of Paths›

fun len :: "'a mat  nat  nat  nat list  'a" where
  "len m u v [] = m u v" |
  "len m u v (w#ws) = m u w + len m w v ws"

lemma len_decomp: "xs = ys @ y # zs  len m x z xs = len m x y ys + len m y z zs"
by (induction ys arbitrary: x xs) (simp add: assoc)+

lemma len_comp: "len m a c (xs @ b # ys) = len m a b xs + len m b c ys"
by (induction xs arbitrary: a) (auto simp: assoc)


subsection ‹Shortening Negative Cycles›

lemma remove_cycles_neg_cycles_aux:
  fixes i xs ys
  defines "xs'  i # ys"
  assumes "i  set ys"
  assumes "i  set xs"
  assumes "xs = as @ concat (map ((#) i) xss) @ xs'"
  assumes "len m i j ys > len m i j xs"
  shows " ys. set ys  set xs  len m i i ys < 𝟭" using assms
proof (induction xss arbitrary: xs as)
  case Nil
  with Nil show ?case
  proof (cases "len m i i as  𝟭", goal_cases)
    case 1
    from this(4,6) len_decomp[of xs as i ys m i j]
    have "len m i j xs = len m i i as + len m i j ys" by simp
    with 1(11)
    have "len m i j ys  len m i j xs" using add_mono by fastforce
    thus ?thesis using Nil(5) by auto
  next
    case 2 thus ?case by auto
  qed
next
  case (Cons zs xss)
  let ?xs = "zs @ concat (map ((#) i) xss) @ xs'"
  from Cons show ?case
  proof (cases "len m i i as  𝟭", goal_cases)
    case 1
    from this(5,7) len_decomp add_mono
    have "len m i j ?xs  len m i j xs" by fastforce
    hence 4:"len m i j ?xs < len m i j ys" using 1(6) by simp
    have 2:"i  set ?xs" using Cons(2) by auto
    have "set ?xs  set xs" using Cons(5) by auto
    moreover from Cons(1)[OF 1(2,3) 2 _ 4] have "ys. set ys  set ?xs  len m i i ys < 𝟭" by auto
    ultimately show ?case by blast
  next
    case 2
    from this(5,7) show ?case by auto
  qed
qed

lemma add_lt_neutral: "a + b < b  a < 𝟭"
proof (rule ccontr)
  assume "a + b < b" "¬ a < 𝟭"
  hence "a  𝟭" by auto
  from add_mono[OF this, of b b] a + b < b show False by auto
qed

lemma remove_cycles_neg_cycles_aux':
  fixes j xs ys
  assumes "j  set ys"
  assumes "j  set xs"
  assumes "xs = ys @ j # concat (map (λ xs. xs @ [j]) xss) @ as"
  assumes "len m i j ys > len m i j xs"
  shows " ys. set ys  set xs  len m j j ys < 𝟭" using assms
proof (induction xss arbitrary: xs as)
  case Nil
  show ?case
  proof (cases "len m j j as  𝟭")
    case True
    from Nil(3) len_decomp[of xs ys j as m i j]
    have "len m i j xs = len m i j ys + len m j j as" by simp
    with True
    have "len m i j ys  len m i j xs" using add_mono by fastforce
    with Nil show ?thesis by auto
  next
    case False with Nil show ?thesis by auto
  qed
next
  case (Cons zs xss)
  let ?xs = "ys @ j # concat (map (λxs. xs @ [j]) xss) @ as"
  let ?t = "concat (map (λxs. xs @ [j]) xss) @ as"
  show ?case
  proof (cases "len m i j ?xs  len m i j xs")
    case True
    hence 4:"len m i j ?xs < len m i j ys" using Cons(5) by simp
    have 2:"j  set ?xs" using Cons(2) by auto
    have "set ?xs  set xs" using Cons(4) by auto
    moreover from Cons(1)[OF Cons(2) 2 _ 4] have "ys. set ys  set ?xs  len m j j ys < 𝟭" by blast
    ultimately show ?thesis by blast
  next
    case False
    hence "len m i j xs < len m i j ?xs" by auto
    from this len_decomp Cons(4) add_mono
    have "len m j j (concat (map (λxs. xs @ [j]) (zs # xss)) @ as) < len m j j ?t"
    using False local.leI by fastforce 
    hence "len m j j (zs @ j # ?t) < len m j j ?t" by simp
    with len_decomp[of "zs @ j # ?t" zs j ?t m j j]
    have "len m j j zs + len m j j ?t < len m j j ?t" by auto
    hence "len m j j zs < 𝟭" using add_lt_neutral by auto
    thus ?thesis using Cons.prems(3) by auto
  qed
qed

lemma add_le_impl: "a + b < a + c  b < c"
proof (rule ccontr)
  assume "a + b < a + c" "¬ b < c"
  hence "b  c" by auto
  from add_mono[OF _ this, of a a] a + b < a + c show False by auto
qed

lemma start_remove_neg_cycles:
  "len m i j (start_remove xs k []) > len m i j xs   ys. set ys  set xs  len m k k ys < 𝟭"
proof-
  let ?xs = "start_remove xs k []"
  assume len_lt:"len m i j ?xs > len m i j xs"
  hence "k  set xs" using start_remove_id by fastforce
  from start_remove_decomp[OF this, of "[]"] obtain as bs where as_bs:
    "xs = as @ k # bs" "?xs = as @ remove_cycles bs k [k]"
  by fastforce
  let ?xs' = "remove_cycles bs k [k]"
  have "k  set bs" using as_bs len_lt remove_cycles_id by fastforce
  then obtain ys where ys: "?xs = as @ k # ys" "?xs' = k # ys" "k  set ys"
  using as_bs(2) remove_cycles_begins_with[OF k  set bs] by auto
  have len_lt': "len m k j bs < len m k j ys"
  using len_decomp[OF as_bs(1), of m i j] len_decomp[OF ys(1), of m i j] len_lt add_le_impl by metis
  from remove_cycles_cycles[OF k  set bs] obtain xss as'
  where "as' @ concat (map ((#) k) xss) @ ?xs' = bs" by fastforce
  hence "as' @ concat (map ((#) k) xss) @ k # ys = bs" using ys(2) by simp
  from remove_cycles_neg_cycles_aux[OF k  set ys k  set bs this[symmetric] len_lt']
  show ?thesis using as_bs(1) by auto
qed

lemma remove_all_cycles_neg_cycles:
  "len m i j (remove_all_cycles ys xs) > len m i j xs
    ys k. set ys  set xs  k  set xs  len m k k ys < 𝟭"
proof (induction ys arbitrary: xs)
  case Nil thus ?case by auto
next
  case (Cons y ys)
  let ?xs = "start_remove xs y []"
  show ?case
  proof (cases "len m i j xs < len m i j ?xs")
    case True
    with start_remove_id have "y  set xs" by fastforce
    with start_remove_neg_cycles[OF True] show ?thesis by blast
  next
    case False
    with Cons(2) have "len m i j ?xs < len m i j (remove_all_cycles (y # ys) xs)" by auto
    hence "len m i j ?xs < len m i j (remove_all_cycles ys ?xs)" by auto
    from Cons(1)[OF this] show ?thesis using start_remove_subs[of xs y "[]"] by auto
  qed
qed

lemma (in -) concat_map_cons_rev:
  "rev (concat (map ((#) j) xss)) = concat (map (λ xs. xs @ [j]) (rev (map rev xss)))"
by (induction xss) auto

lemma negative_cycle_dest: "len m i j (rem_cycles i j xs) > len m i j xs
         i' ys. len m i' i' ys < 𝟭  set ys  set xs  i'  set (i # j # xs)"
proof -
  let ?xsij = "rem_cycles i j xs"
  let ?xsj  = "remove_all_rev j (remove_all_cycles xs xs)"
  let ?xs   = "remove_all_cycles xs xs"
  assume len_lt: "len m i j ?xsij > len m i j xs"
  show ?thesis
  proof (cases "len m i j ?xsij  len m i j ?xsj")
    case True
    hence len_lt: "len m i j ?xsj > len m i j xs" using len_lt by simp
    show ?thesis
    proof (cases "len m i j ?xsj  len m i j ?xs")
      case True
      hence "len m i j ?xs > len m i j xs" using len_lt by simp
      with remove_all_cycles_neg_cycles[OF this] show ?thesis by auto
    next
      case False
      then have len_lt': "len m i j ?xsj > len m i j ?xs" by simp
      show ?thesis
      proof (cases "j  set ?xs")
        case False
        thus ?thesis using len_lt' by (simp add: remove_all_rev_def)
      next
        case True
          from remove_all_rev_removes[of j] have 1: "j  set ?xsj" by simp
          from True have "j  set (rev ?xs)" by auto
          from remove_cycles_cycles[OF this] obtain xss as where as:
          "as @ concat (map ((#) j) xss) @ remove_cycles (rev ?xs) j [] = rev ?xs" "j  set as"
          by blast
          from True have "?xsj = rev (tl (remove_cycles (rev ?xs) j []))" by (simp add: remove_all_rev_def)
          with remove_cycles_begins_with[OF j  set (rev ?xs), of "[]"]
          have "remove_cycles (rev ?xs) j [] = j # rev ?xsj" "j  set ?xsj"
          by auto
          with as(1) have xss: "as @ concat (map ((#) j) xss) @ j # rev ?xsj = rev ?xs" by simp
          hence "rev (as @ concat (map ((#) j) xss) @ j # rev ?xsj) = ?xs" by simp
          hence "?xsj @ j # rev (concat (map ((#) j) xss)) @ rev as = ?xs" by simp
          hence "?xsj @ j # concat (map (λ xs. xs @ [j]) (rev (map rev xss))) @ rev as = ?xs"
          by (simp add: concat_map_cons_rev)
          from remove_cycles_neg_cycles_aux'[OF 1 True this[symmetric] len_lt']
          show ?thesis using remove_all_cycles_subs by fastforce
      qed
    qed
  next
    case False
    hence len_lt': "len m i j ?xsij > len m i j ?xsj" by simp
    show ?thesis
    proof (cases "i  set ?xsj")
      case False
      thus ?thesis using len_lt' by (simp add: remove_all_def)
    next
      case True
      from remove_all_removes[of i] have 1: "i  set ?xsij" by (simp add: remove_all_def)
      from remove_cycles_cycles[OF True] obtain xss as where as:
      "as @ concat (map ((#) i) xss) @ remove_cycles ?xsj i [] = ?xsj" "i  set as" by blast
      from True have "?xsij = tl (remove_cycles ?xsj i [])" by (simp add: remove_all_def)
      with remove_cycles_begins_with[OF True, of "[]"]
      have "remove_cycles ?xsj i [] = i # ?xsij" "i  set ?xsij"
      by auto
      with as(1) have xss: "as @ concat (map ((#) i) xss) @ i # ?xsij = ?xsj" by simp
      from remove_cycles_neg_cycles_aux[OF 1 True this[symmetric] len_lt']
      show ?thesis using remove_all_rev_subs remove_all_cycles_subs by fastforce
    qed
  qed
qed

section ‹Definition of Shortest Paths›

definition D :: "'a mat  nat  nat  nat  'a" where
  "D m i j k  Min {len m i j xs | xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"

lemma (in -) distinct_length_le:"finite s  set xs  s  distinct xs  length xs  card s"
by (metis card_mono distinct_card) 

lemma (in -) finite_distinct: "finite s  finite {xs . set xs  s  distinct xs}"
proof -
  assume "finite s"
  hence "{xs . set xs  s  distinct xs}  {xs. set xs  s  length xs  card s}"
  using distinct_length_le by auto
  moreover have "finite {xs. set xs  s  length xs  card s}"
  using finite_lists_length_le[OF ‹finite s] by auto
  ultimately show ?thesis by (rule finite_subset)
qed

lemma D_base_finite:
  "finite {len m i j xs | xs. set xs  {0..k}  distinct xs}"
using finite_distinct finite_image_set by blast

lemma D_base_finite':
  "finite {len m i j xs | xs. set xs  {0..k}  distinct (i # j # xs)}"
proof -
  have "{len m i j xs | xs. set xs  {0..k}  distinct (i # j # xs)}
         {len m i j xs | xs. set xs  {0..k}  distinct xs}" by auto
  with D_base_finite[of m i j k] show ?thesis by (rule rev_finite_subset)
qed

lemma D_base_finite'':
  "finite {len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"
using D_base_finite[of m i j k] by - (rule finite_subset, auto)

definition cycle_free :: "'a mat  nat  bool" where
  "cycle_free m n   i xs. i  n  set xs  {0..n} 
  ( j. j  n  len m i j (rem_cycles i j xs)  len m i j xs)  len m i i xs  𝟭"

lemma D_eqI:
  fixes m n i j k
  defines "A  {len m i j xs | xs. set xs  {0..k}}"
  defines "A_distinct  {len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"
  assumes "cycle_free m n" "i  n" "j  n" "k  n" "(y. y  A_distinct  x  y)" "x  A"
  shows "D m i j k = x" using assms
proof -
  let ?S = "{len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"
  show ?thesis unfolding D_def
  proof (rule Min_eqI)
    have "?S  {len m i j xs |xs. set xs  {0..k}  distinct xs}" by auto
    thus "finite {len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"
    using D_base_finite[of m i j k] by (rule finite_subset)
  next
    fix y assume "y  ?S"
    hence "y  A_distinct" using assms(2,7) by fastforce
    thus "x  y" using assms by meson
  next
    from assms obtain xs where xs: "x = len m i j xs" "set xs  {0..k}" by auto
    let ?ys = "rem_cycles i j xs"
    let ?y = "len m i j ?ys"
    from assms(3-6) xs have *:"?y  x" by (fastforce simp add: cycle_free_def)
    have distinct: "i  set ?ys" "j  set ?ys" "distinct ?ys"
    using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+
    with xs(2) have "?y  A_distinct" unfolding A_distinct_def using rem_cycles_subs by fastforce
    hence "x  ?y" using assms by meson
    moreover have "?y  x" using assms(3-6) xs by (fastforce simp add: cycle_free_def)
    ultimately have "x = ?y" by simp
    thus "x  ?S" using distinct xs(2) rem_cycles_subs[of i j xs] by fastforce
  qed
qed

lemma D_base_not_empty:
   "{len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}  {}"
proof -
  have "len m i j []  {len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"
  by fastforce
  thus ?thesis by auto
qed

lemma Min_elem_dest: "finite A  A  {}  x = Min A  x  A" by simp

lemma D_dest: "x = D m i j k 
  x  {len m i j xs |xs. set xs  {0..Suc k}  i  set xs  j  set xs  distinct xs}"
using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def)

lemma D_dest': "x = D m i j k  x  {len m i j xs |xs. set xs  {0..Suc k}}"
using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def)

lemma D_dest'': "x = D m i j k  x  {len m i j xs |xs. set xs  {0..k}}"
using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def)

lemma cycle_free_loop_dest: "i  n  set xs  {0..n}  cycle_free m n  len m i i xs  𝟭"
unfolding cycle_free_def by auto

lemma cycle_free_dest:
  "cycle_free m n  i  n  j  n  set xs  {0..n}
     len m i j (rem_cycles i j xs)  len m i j xs"
by (auto simp add: cycle_free_def)

definition cycle_free_up_to :: "'a mat  nat  nat  bool" where
  "cycle_free_up_to m k n   i xs. i  n  set xs  {0..k} 
  ( j. j  n  len m i j (rem_cycles i j xs)  len m i j xs)  len m i i xs  𝟭"

lemma cycle_free_up_to_loop_dest:
  "i  n  set xs  {0..k}  cycle_free_up_to m k n  len m i i xs  𝟭"
unfolding cycle_free_up_to_def by auto

lemma cycle_free_up_to_diag:
  assumes "cycle_free_up_to m k n" "i  n"
  shows "m i i  𝟭"
using cycle_free_up_to_loop_dest[OF assms(2) _ assms(1), of "[]"] by auto

lemma D_eqI2:
  fixes m n i j k
  defines "A  {len m i j xs | xs. set xs  {0..k}}"
  defines "A_distinct  {len m i j xs | xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"
  assumes "cycle_free_up_to m k n" "i  n" "j  n" "k  n"
          "(y. y  A_distinct  x  y)" "x  A"
  shows "D m i j k = x" using assms
proof -
  show ?thesis
  proof (simp add: D_def A_distinct_def[symmetric], rule Min_eqI)
    show "finite A_distinct" using D_base_finite''[of m i j k] unfolding A_distinct_def by auto
  next
    fix y assume "y  A_distinct"
    thus "x  y" using assms by meson
  next
    from assms obtain xs where xs: "x = len m i j xs" "set xs  {0..k}" by auto
    let ?ys = "rem_cycles i j xs"
    let ?y = "len m i j ?ys"
    from assms(3-6) xs have *:"?y  x" by (fastforce simp add: cycle_free_up_to_def)
    have distinct: "i  set ?ys" "j  set ?ys" "distinct ?ys"
    using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+
    with xs(2) have "?y  A_distinct" unfolding A_distinct_def using rem_cycles_subs by fastforce 
    hence "x  ?y" using assms by meson
    moreover have "?y  x" using assms(3-6) xs by (fastforce simp add: cycle_free_up_to_def)
    ultimately have "x = ?y" by simp
    then show "x  A_distinct" using distinct xs(2) rem_cycles_subs[of i j xs]
    unfolding A_distinct_def by fastforce
  qed
qed


section ‹Result Under The Absence of Negative Cycles›

text ‹
  This proves that the algorithm correctly computes shortest paths under the absence of negative
  cycles by a standard argument.
›

theorem fw_shortest_path_up_to:
  "cycle_free_up_to m k n  i'  i  j'  j  i  n  j  n  k  n
         D m i' j' k = fw m n k i j i' j'"
proof (induction k arbitrary: i j i' j')
  case 0
  from cycle_free_up_to_diag[OF 0(1)] have diag: " k  n. m k k  𝟭" by auto
  then have m_diag: "m 0 0  𝟭" by simp
  let ?S = "{len m i' j' xs |xs. set xs  {0}  i'  set xs  j'  set xs  distinct xs}"
  show ?case unfolding D_def
  proof (simp, rule Min_eqI)
    have "?S  {len m i' j' xs |xs. set xs  {0..0}  distinct xs}" by auto
    thus "finite ?S" using D_base_finite[of m i' j' 0] by (rule finite_subset)
  next
    fix l assume "l  ?S"
    then obtain xs where l: "l = len m i' j' xs" and xs: "xs = []  xs = [0]"
    using distinct_list_single_elem_decomp by auto
    { assume "xs = []"
      have "fw m n 0 i j i' j'  fw m n 0 0 0 i' j'" using fw_invariant 0 by blast
      also have "  m i' j'" by (cases "i' = 0  j' = 0") (simp add: fw_upd_def upd_def)+
      finally have "fw m n 0 i j i' j'  l" using xs = [] l by simp
    }
    moreover
    { assume "xs = [0]"
      have "fw m n 0 i j i' j'  fw m n 0 i' j' i' j'" using fw_invariant 0 by blast
      also have "  m i' 0 + m 0 j'"
      proof (cases j')
        assume "j' = 0"
        show ?thesis
        proof (cases i')
          assume "i' = 0"
          thus ?thesis using j' = 0 by (simp add: fw_upd_def upd_def)
        next
          fix i'' assume i'': "i' = Suc i''"
          have "fw_upd (fw m n 0 i'' n) 0 (Suc i'') 0 (Suc i'') 0  fw m n 0 i'' n (Suc i'') 0"
          by (simp add: fw_upd_mono)
          also have "  m (Suc i'') 0" using fw_mono 0 i'' by simp
          finally show ?thesis using j' = 0 m_diag i'' neutr add_mono by fastforce
        qed
      next
        fix j'' assume j'': "j' = Suc j''"
        have "fw_upd (fw m n 0 i' j'') 0 i' (Suc j'') i' (Suc j'')
               fw m n 0 i' j'' i' 0 + fw m n 0 i' j'' 0 (Suc j'') "
        by (simp add: fw_upd_def upd_def)
        also have "  m i' 0 + m 0 (Suc j'')"
        using fw_mono[of i' n j'' i' 0 m 0] fw_mono[of i' n j'' 0 "Suc j''" m 0 ] j'' 0
        by (simp add: add_mono)
        finally show ?thesis using j'' by simp
      qed
      finally have "fw m n 0 i j i' j'  l" using xs = [0] l by simp
    }
    ultimately show "fw m n 0 i j i' j'  l" using xs by auto
  next
    have A: "fw m n 0 i j i' j' = fw m n 0 i' j' i' j'" using single_iteration_inv 0 by blast
    have "fw m n 0 i' j' i' j' = min (m i' j') (m i' 0 + m 0 j')"
    using 0 by (simp add: fw_step_0[of m, OF m_diag])
    hence
      "fw m n 0 i' j' i' j' = m i' j'
       (fw m n 0 i' j' i' j' = m i' 0 + m 0 j' m i' 0 + m 0 j'  m i' j')"
    by (auto simp add: ord.min_def) 
    thus "fw m n 0 i j i' j'  ?S"
    proof (standard, goal_cases)
      case 1
      hence "fw m n 0 i j i' j' = len m i' j' []" using A by auto
      thus ?case by fastforce
    next
      case 2
      hence *:"fw m n 0 i j i' j' = len m i' j' [0]" using A by auto
      thus ?case
      proof (cases "i' = 0  j' = 0")
        case False thus ?thesis using * by fastforce
      next
        case True
        { assume "i' = 0"
          from diag have "m 0 0 + m 0 j'  m 0 j'" by (auto intro: add_mono_neutl)
          with i' = 0 have "fw m n 0 i j i' j' = len m 0 j' []" using 0 A 2 by auto
        } moreover
        { assume "j' = 0"
          from diag have "m i' 0 + m 0 0  m i' 0" by (auto intro: add_mono_neutr)
          with j' = 0 have "fw m n 0 i j i' j' = len m i' 0 []" using 0 A 2 by auto
        }
        ultimately have "fw m n 0 i j i' j' = len m i' j' []" using True by auto
        then show ?thesis by fastforce
      qed
    qed
  qed
next
  case (Suc k)
  from cycle_free_up_to_diag[OF Suc.prems(1)] have diag: " k  n. m k k  𝟭" by auto
  from Suc.prems have cycle_free_to_k:
    "cycle_free_up_to m k n" by (fastforce simp add: cycle_free_up_to_def)
  { fix k' assume "k'  n"
    with Suc cycle_free_to_k have "D m k' k' k = fw m n k n n k' k'" by auto
    from D_dest''[OF this[symmetric]] obtain xs where
      "set xs  {0..k}" "fw m n k n n k' k'= len m k' k' xs"
    by auto
    with Suc(2) ‹Suc k  n k'  n have "fw m n k n n k' k'  𝟭"
    unfolding cycle_free_up_to_def by force
  }
  hence K: "k'n. fw m n k n n k' k'  𝟭" by simp
  let ?S = "λ k i j. {len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}"
  show ?case
  proof (rule D_eqI2)
    show "cycle_free_up_to m (Suc k) n" using Suc.prems(1) .
  next
    show "i'  n" using Suc.prems by simp
  next
    show "j'  n" using Suc.prems by simp
  next
    show "Suc k  n" using Suc.prems by simp
  next
    fix l assume "l  {len m i' j' xs | xs. set xs  {0..Suc k}  i'  set xs  j'  set xs  distinct xs}"
    then obtain xs where xs:
      "l = len m i' j' xs" "set xs  {0..Suc k}" "i'  set xs" "j'  set xs" "distinct xs"
    by auto
    have IH: "D m i' j' k = fw m n k i j i' j'" using cycle_free_to_k Suc by auto
    have fin:
      "finite {len m i' j' xs |xs. set xs  {0..k}  i'  set xs  j'  set xs  distinct xs}"
    using D_base_finite'' by simp
    show "fw m n (Suc k) i j i' j'  l"
    proof (cases "Suc k  set xs")
      case False
      hence "set xs  {0..k}" using xs(2) using atLeastAtMostSuc_conv by auto
      hence
        "l  {len m i' j' xs | xs. set xs  {0..k}  i'  set xs  j'  set xs  distinct xs}"
      using xs by auto
      with Min_le[OF fin this] have "fw m n k i j i' j'  l" using IH by (simp add: D_def)
      thus ?thesis using fw_invariant[of k "Suc k" i n j j i m i' j'] Suc.prems by simp
    next
      case True
      then obtain ys zs where ys_zs_id: "xs = ys @ Suc k # zs" by (meson split_list)
      with xs(5) have ys_zs: "distinct ys" "distinct zs" "Suc k  set ys" "Suc k  set zs"
      "set ys  set zs = {}" by auto
      have "i'  Suc k" "j'  Suc k" using xs(3,4) True by auto

      have "set ys  {0..k}" using ys_zs(3) xs(2) ys_zs_id using atLeastAtMostSuc_conv by auto
      hence "len m i' (Suc k) ys  ?S k i' (Suc k)" using ys_zs_id ys_zs xs(3) by fastforce
      with Min_le[OF _ this] have "Min (?S k i' (Suc k))  len m i' (Suc k) ys"
      using D_base_finite'[of m i' "Suc k" k] i'  Suc k by fastforce
      moreover have "fw m n k n n i' (Suc k)  =  D m i' (Suc k) k"
      using Suc.IH[OF cycle_free_to_k, of i' n] Suc.prems by auto
      ultimately have *:"fw m n k n n i' (Suc k)  len m i' (Suc k) ys" using i'  Suc k
      by (auto simp: D_def)

      have "set zs  {0..k}" using ys_zs(4) xs(2) ys_zs_id using atLeastAtMostSuc_conv by auto
      hence "len m (Suc k) j' zs  ?S k (Suc k) j'" using ys_zs_id ys_zs xs(3,4,5) by fastforce
      with Min_le[OF _ this] have "Min (?S k (Suc k) j')  len m (Suc k) j' zs"
      using D_base_finite'[of m "Suc k" j' k] j'  Suc k by fastforce
      moreover have "fw m n k n n (Suc k) j'  =  D m (Suc k) j' k"
      using Suc.IH[OF cycle_free_to_k, of "Suc k" n j' n] Suc.prems by auto
      ultimately have **:"fw m n k n n (Suc k) j'  len m (Suc k) j' zs" using j'  Suc k
      by (auto simp: D_def)

      have len_eq: "l = len m i' (Suc k) ys + len m (Suc k) j' zs"
      by (simp add: xs(1) len_decomp[OF ys_zs_id, symmetric] ys_zs_id)
      have "fw m n (Suc k) i' j' i' j'  fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j'"
      using fw_step_Suc[of n m k i' j', OF K] Suc.prems(2-) by simp
      hence "fw m n (Suc k) i' j' i' j'  l"
      using fw_step_Suc[of n m k i j] Suc.prems(3-) * ** len_eq add_mono by fastforce
      thus ?thesis using fw_invariant[of "Suc k" "Suc k" i n j j' i' m i' j'] Suc.prems(2-) by simp
    qed
  next
    have "fw m n (Suc k) i j i' j' = fw m n (Suc k) i' j' i' j'"
    using single_iteration_inv[OF Suc.prems(2-5)] .
    also have " = min (fw m n k n n i' j') (fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j')"
    using fw_step_Suc[OF K] Suc.prems(2-) by simp
    finally show "fw m n (Suc k) i j i' j'  {len m i' j' xs | xs. set xs  {0..Suc k}}"
    proof (cases "fw m n (Suc k) i j i' j' = fw m n k n n i' j'", goal_cases)
      case True
      have "fw m n (Suc k) i j i' j' = D m i' j' k"
      using Suc.IH[OF cycle_free_to_k, of i' n j' n] Suc.prems(2-) True by simp
      from D_dest'[OF this] show ?thesis by blast
    next
      case 2
      hence A:"fw m n (Suc k) i j i' j' = fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j'"
      by (metis ord.min_def)
      have "fw m n k n n i' j' = D m i' j' k"
      using Suc.IH[OF cycle_free_to_k, of i' n j' n] Suc.prems by simp
      from D_dest[OF this] have B:"fw m n k n n i' j'  ?S (Suc k) i' j'"
      by blast
      have "fw m n k n n i' (Suc k) = D m i' (Suc k) k"
      using Suc.IH[OF cycle_free_to_k, of i' n "Suc k" n] Suc.prems by simp
      from D_dest'[OF this] obtain xs where xs:
        "fw m n k n n i' (Suc k) = len m i' (Suc k) xs" "set xs  {0..Suc k}" by blast
      have "fw m n k n n (Suc k) j' = D m (Suc k) j' k"
      using Suc.IH[OF cycle_free_to_k, of "Suc k" n j' n] Suc.prems by simp
      from D_dest'[OF this] obtain ys where ys:
        "fw m n k n n (Suc k) j' = len m (Suc k) j' ys" "set ys  {0..Suc k}" by blast
      from A xs(1) ys(1) len_comp
      have "fw m n (Suc k) i j i' j' = len m i' j' (xs @ Suc k # ys)" by simp
      moreover have "set (xs @ Suc k # ys)  {0..Suc k}" using xs(2) ys(2) by auto
      ultimately show ?thesis by blast
    qed
  qed
qed

lemma cycle_free_cycle_free_up_to:
  "cycle_free m n  k  n  cycle_free_up_to m k n"
unfolding cycle_free_def cycle_free_up_to_def by force

lemma cycle_free_diag:
  "cycle_free m n  i  n  𝟭  m i i"
using cycle_free_up_to_diag[OF cycle_free_cycle_free_up_to] by blast

corollary fw_shortest_path:
  "cycle_free m n  i'  i  j'  j  i  n  j  n  k  n
         D m i' j' k = fw m n k i j i' j'"
using fw_shortest_path_up_to[OF cycle_free_cycle_free_up_to] by auto

corollary fw_shortest:
  assumes "cycle_free m n" "i  n" "j  n" "k  n"
  shows "fw m n n n n i j  fw m n n n n i k + fw m n n n n k j"
proof (rule ccontr, goal_cases)
  case 1
  let ?S = "λ i j. {len m i j xs |xs. set xs  {0..n}}"
  let ?FW = "fw m n n n n"
  from assms fw_shortest_path
  have FW: "?FW i j = D m i j n" "?FW i k = D m i k n" "?FW k j = D m k j n" by auto
  with D_dest'' FW have "?FW i k  ?S i k" "?FW k j  ?S k j" by auto
  then obtain xs ys where xs_ys:
    "?FW i k = len m i k xs" "set xs  {0..n}" "?FW k j = len m k j ys" "set ys  {0..n}" by auto
  let ?zs = "rem_cycles i j (xs @ k # ys)"
  have *:"?FW i j = Min {len m i j xs |xs. set xs  {0..n}  i  set xs  j  set xs  distinct xs}"
  using FW(1) unfolding D_def .
  have "set (xs @ k # ys)  {0..n}" using assms xs_ys by fastforce
  from cycle_free_dest [OF ‹cycle_free m n i  n j  n this]
  have **:"len m i j ?zs  len m i j (xs @ k # ys)" by auto
  moreover have "i  set ?zs" "j  set ?zs" "distinct ?zs"
  using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+
  moreover have "set ?zs  {0..n}" using rem_cycles_subs[of i j"xs @ k # ys"] xs_ys assms by fastforce
  ultimately have
    "len m i j ?zs  {len m i j xs |xs. set xs  {0..n}  i  set xs  j  set xs  distinct xs}"
  by blast
  with * have "?FW i j  len m i j ?zs" using D_base_finite'' by auto
  with ** xs_ys len_comp 1 show ?case by auto
qed


section ‹Result Under the Presence of Negative Cycles›

lemma not_cylce_free_dest: "¬ cycle_free m n   k  n. ¬ cycle_free_up_to m k n"
by (auto simp add: cycle_free_def cycle_free_up_to_def)

lemma D_not_diag_le:
  "(x :: 'a)  {len m i j xs |xs. set xs  {0..k}  i  set xs  j  set xs  distinct xs}
   D m i j k  x" using Min_le[OF D_base_finite''] by (auto simp add: D_def)

lemma D_not_diag_le': "set xs  {0..k}  i  set xs  j  set xs  distinct xs
   D m i j k  len m i j xs" using Min_le[OF D_base_finite''] by (fastforce simp add: D_def)

lemma (in -) nat_upto_subs_top_removal':
  "S  {0..Suc n}  Suc n  S  S  {0..n}"
apply (induction n)
 apply safe
 apply (rename_tac x)
 apply (case_tac "x = Suc 0"; fastforce)
apply (rename_tac n x)
apply (case_tac "x = Suc (Suc n)"; fastforce)
done

lemma (in -) nat_upto_subs_top_removal:
  "S  {0..n::nat}  n  S  S  {0..n - 1}"
using nat_upto_subs_top_removal' by (cases n; simp)

lemma fw_Suc:
  "i  n  j  n  i'  n  j'  n  fw m n (Suc k) i' j' i j  fw m n k n n i j"
by (metis Suc_innermost_id1' Suc_innermost_id2 Suc_innermost_mono linorder_class.not_le order.eq_iff
          preorder_class.order_refl single_iteration_inv single_iteration_inv')

lemma negative_len_shortest:
  "length xs = n  len m i i xs < 𝟭
      j ys. distinct (j # ys)  len m j j ys < 𝟭  j  set (i # xs)  set ys  set xs"
proof (induction n arbitrary: xs i rule: less_induct)
  case (less n)
  show ?case
  proof (cases xs)
    case Nil
    thus ?thesis using less.prems by auto
  next
    case (Cons y ys)
    then have "length xs  1" by auto
    show ?thesis
    proof (cases "i  set xs")
      assume i: "i  set xs"
      then obtain as bs where xs: "xs = as @ i # bs" by (meson split_list)
      show ?thesis
      proof (cases "len m i i as < 𝟭")
        case True
        from xs less.prems have "length as < n" by auto
        from less.IH[OF this _ True] xs show ?thesis by auto
      next
        case False
        from len_decomp[OF xs] have "len m i i xs = len m i i as + len m i i bs" by auto
        with False less.prems have *: "len m i i bs < 𝟭"
        by (metis add_lt_neutral local.dual_order.strict_trans local.neqE)
        from xs less.prems have "length bs < n" by auto
        from less.IH[OF this _ *] xs show ?thesis by auto
      qed
    next
      assume i: "i  set xs"
      show ?thesis
      proof (cases "distinct xs")
        case True
        with i less.prems show ?thesis by auto
      next
        case False
        from not_distinct_decomp[OF this] obtain a as bs cs where xs:
          "xs = as @ a # bs @ a # cs"
        by auto
        show ?thesis
        proof (cases "len m a a bs < 𝟭")
          case True
          from xs less.prems have "length bs < n" by auto
          from less.IH[OF this _ True] xs show ?thesis by auto
        next
          case False
          from len_decomp[OF xs, of m  i i] len_decomp[of "bs @ a # cs" bs a cs m a i]
          have *:"len m i i xs = len m i a as + (len m a a bs + len m a i cs)" by auto
          from False have "len m a a bs  𝟭" by auto
          with add_mono have "len m a a bs + len m a i cs  len m a i cs" by fastforce
          with * have "len m i i xs  len m i a as + len m a i cs" by (simp add: add_mono)
          with less.prems(2) have "len m i a as + len m a i cs < 𝟭" by auto
          with len_comp have "len m i i (as @ a # cs) < 𝟭" by auto
          from less.IH[OF _ _ this, of "length (as @ a # cs)"] xs less.prems
          show ?thesis by auto
        qed
      qed
    qed
  qed
qed

theorem FW_neg_cycle_detect:
  "¬ cycle_free m n   i  n. fw m n n n n i i < 𝟭"
proof -
  assume A: "¬ cycle_free m n"
  let ?K = "{k. k  n  ¬ cycle_free_up_to m k n}"
  let ?k = "Min ?K"
  have not_empty_K: "?K  {}" using not_cylce_free_dest[OF A(1)] by auto
  have "finite ?K" by auto
  with not_empty_K have *:
    " k' < ?k. cycle_free_up_to m k' n"
  by (auto, metis le_trans less_or_eq_imp_le preorder_class.less_irrefl)
  from linorder_class.Min_in[OF ‹finite ?K ?K  {}] have
    "¬ cycle_free_up_to m ?k n" "?k  n"
  by auto
  then have " xs j. j  n  len m j j xs < 𝟭  set xs  {0..?k}" unfolding cycle_free_up_to_def
  proof (auto, goal_cases)
    case (2 i xs) then have "len m i i xs < 𝟭" by auto
    with 2 show ?case by auto
  next
    case (1 i xs j)
    then have "len m i j (rem_cycles i j xs) > len m i j xs" by auto
    from negative_cycle_dest[OF this]
    obtain i' ys where ys: "i'  set (i # j # xs)" "len m i' i' ys < 𝟭" "set ys  set xs" by blast
    from ys(1) 1(2-4) show ?case
    proof (auto, goal_cases)
      case 1
      with ys(2,3) show ?case by auto
    next
      case 2
      with ys(2,3) show ?case by auto
    next
      case 3
      with ?k  n have "i'  n" unfolding cycle_free_up_to_def by auto
      with 3 ys(2,3) show ?case by auto
    qed
  qed
  then obtain a as where a_as: "a  n  len m a a as < 𝟭  set as  {0..?k}" by auto
  with negative_len_shortest[of as "length as" m a] obtain j xs where j_xs:
  "distinct (j # xs)  len m j j xs < 𝟭  j  set (a # as)  set xs  set as" by auto
  with a_as ?k  n have cyc: "j  n" "set xs  {0..?k}" "len m j j xs < 𝟭" "distinct (j # xs)"
  by auto
  { assume "?k > 0"
    then have "?k - 1 < ?k" by simp
    with * have **:"cycle_free_up_to m (?k - 1) n" by blast
    have "?k  set xs"
    proof (rule ccontr, goal_cases)
      case 1
      with ‹set xs  {0..?k} nat_upto_subs_top_removal have "set xs  {0..?k-1}" by auto
      from cycle_free_up_to_loop_dest[OF j  n this ‹cycle_free_up_to m (?k - 1) n] cyc(3)
      show ?case by auto
    qed
    with cyc(4) have "j  ?k" by auto
    from ?k  set xs obtain ys zs where "xs = ys @ ?k # zs" by (meson split_list)
    with ‹distinct (j # xs)
    have xs: "xs = ys @ ?k # zs" "distinct ys" "distinct zs" "?k  set ys" "?k  set zs"
             "j  set ys" "j  set zs" by auto
    from xs(1,4) ‹set xs  {0..?k} nat_upto_subs_top_removal have ys: "set ys  {0..?k-1}" by auto
    from xs(1,5) ‹set xs  {0..?k} nat_upto_subs_top_removal have zs: "set zs  {0..?k-1}" by auto
    have "D m j ?k (?k - 1) = fw m n (?k - 1) n n j ?k"
    using ?k  n j  n fw_shortest_path_up_to[OF **, of j n ?k n] by auto
    moreover have "D m ?k j (?k - 1) = fw m n (?k - 1) n n ?k j"
    using ?k  n j  n fw_shortest_path_up_to[OF **, of ?k n j n] by auto
    ultimately have "fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j  len m j ?k ys + len m ?k j zs"
    using D_not_diag_le'[OF zs(1) xs(5,7,3), of m]
          D_not_diag_le'[OF ys(1) xs(6,4,2), of m] by (auto simp: add_mono)
    then have neg: "fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j < 𝟭"
    using xs(1) ‹len m j j xs < 𝟭 len_comp by auto
    have "fw m n ?k j j j j  fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j"
    proof (cases "j = 0")
      case True
      with?k > 0 fw.simps(2)[of m n "?k - 1"]
      have "fw m n ?k j j = fw_upd (fw m n (?k - 1) n n) ?k j j" by auto
      then have "fw m n ?k j j j j  fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j"
      by (simp add: fw_upd_def upd_def)
      then show ?thesis by auto
    next
      case False
      with fw.simps(4)[of m n ?k j "j - 1"]
      have "fw m n ?k j j = fw_upd (fw m n ?k j (j -1)) ?k j j" by simp
      then have *: "fw m n ?k j j j j  fw m n ?k j (j -1) j ?k + fw m n ?k j (j -1) ?k j"
      by (simp add: fw_upd_def upd_def)
      have "j - 1 < n" using j  n False by auto
      then have "fw m n ?k j (j -1) j ?k  fw m n (?k - 1) n n j ?k"
      using fw_Suc[of j n ?k j "j - 1" m "?k - 1"] j  n ?k  n ?k > 0 by auto
      moreover have "fw m n ?k j (j -1) ?k j  fw m n (?k - 1) n n ?k j"
      using fw_Suc[of ?k n j j "j - 1" m "?k - 1"] j  n ?k  n ?k > 0 by auto
      ultimately have "fw m n ?k j j j j  fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j"
      using * add_mono by fastforce
      then show ?thesis by auto
    qed
    with neg have "fw m n ?k j j j j < 𝟭" by auto
    moreover have "fw m n n n n j j  fw m n ?k j j j j" using fw_invariant jn ?k  n by auto
    ultimately have "fw m n n n n j j < 𝟭" using neg by auto
    with jn have ?thesis by auto
  }
  moreover
  { assume "?k = 0"
    with cyc(2,4) have "xs = []  xs = [0]"
      apply safe
      apply (case_tac xs)
       apply fastforce
      apply (rename_tac ys)
      apply (case_tac ys)
       apply auto
    done
    then have ?thesis
    proof
      assume "xs = []"
      with cyc have "m j j < 𝟭" by auto
      with fw_mono[of n n n j j m n] j  n have "fw m n n n n j j < 𝟭" by auto
      with j  n show ?thesis by auto
    next
      assume xs: "xs = [0]"
      with cyc have "m j 0 + m 0 j < 𝟭" by auto
      then have "fw m n 0 j j j j < 𝟭"
      proof (cases "j = 0", goal_cases)
        case 1
        have "m j j < 𝟭"
        proof (rule ccontr)
          assume "¬ m j j < 𝟭"
          with 1 have "m 0 0  𝟭" by simp
          with add_mono have "m 0 0 + m 0 0  𝟭" by fastforce
          with 1 show False by simp
        qed
        with fw_mono[of j n j j j m 0] j  n show ?thesis by auto
      next
        case 2
        with fw.simps(4)[of m n 0 j "j - 1"]
        have "fw m n 0 j j = fw_upd (fw m n 0 j (j - 1)) 0 j j" by simp
        then have "fw m n 0 j j j j  fw m n 0 j (j - 1) j 0 + fw m n 0 j (j - 1) 0 j"
        by (simp add: fw_upd_def upd_def)
        also have "  m j 0 + m 0 j" using j  n add_mono fw_mono by auto
        finally show ?thesis using 2 by auto
      qed
      then have "fw m n 0 n n j j < 𝟭" by (metis cyc(1) less_or_eq_imp_le single_iteration_inv) 
      with fw_invariant[of 0 n n n n n n m j j] j  n have "fw m n n n n j j < 𝟭" by auto
      with j  n show ?thesis by blast
    qed
  }
  ultimately show ?thesis by auto
qed

end (* End of local class context *)
end (* End of theory *)

Theory Timed_Automata

theory Timed_Automata
  imports Main
begin

chapter ‹Basic Definitions and Semantics›

section ‹Time›

class time = linordered_ab_group_add +
  assumes dense: "x < y  z. x < z  z < y"
  assumes non_trivial: " x. x  0"

begin

lemma non_trivial_neg: " x. x < 0"
proof -
  from non_trivial obtain x where "x  0" by auto
  then show ?thesis
  proof (cases "x < 0", auto, goal_cases)
    case 1
    then have "x > 0" by auto
    then have "(-x) < 0" by auto
    then show ?case by blast
  qed
qed

end

datatype ('c, 't :: time) cconstraint =
  AND "('c, 't) cconstraint" "('c, 't) cconstraint" |
  LT 'c 't |
  LE 'c 't |
  EQ 'c 't |
  GT 'c 't |
  GE 'c 't

section ‹Syntactic Definition›

text ‹
  For an informal description of timed automata we refer to Bengtsson and Yi \cite{BengtssonY03}.
  We define a timed automaton A›

type_synonym
  ('c, 'time, 's) invassn = "'s  ('c, 'time) cconstraint"

type_synonym
  ('a, 'c, 'time, 's) transition = "'s * ('c, 'time) cconstraint * 'a * 'c list * 's"

type_synonym
  ('a, 'c, 'time, 's) ta = "('a, 'c, 'time, 's) transition set * ('c, 'time, 's) invassn"

definition trans_of :: "('a, 'c, 'time, 's) ta  ('a, 'c, 'time, 's) transition set" where
  "trans_of  fst"
definition inv_of  :: "('a, 'c, 'time, 's) ta  ('c, 'time, 's) invassn" where
  "inv_of  snd"

abbreviation transition ::
  "('a, 'c, 'time, 's) ta  's  ('c, 'time) cconstraint  'a  'c list  's  bool"
("_  _ ⟶⇗_,_,_ _" [61,61,61,61,61,61] 61) where
  "(A  lg,a,r l')  (l,g,a,r,l')  trans_of A"

subsection ‹Collecting Information About Clocks›

fun collect_clks :: "('c, 't :: time) cconstraint  'c set"
where
  "collect_clks (AND cc1 cc2) = collect_clks cc1  collect_clks cc2" |
  "collect_clks (LT c _) = {c}" |
  "collect_clks (LE c _) = {c}" |
  "collect_clks (EQ c _) = {c}" |
  "collect_clks (GE c _) = {c}" |
  "collect_clks (GT c _) = {c}"

fun collect_clock_pairs :: "('c, 't :: time) cconstraint  ('c * 't) set"
where
  "collect_clock_pairs (LT x m) = {(x, m)}" |
  "collect_clock_pairs (LE x m) = {(x, m)}" |
  "collect_clock_pairs (EQ x m) = {(x, m)}" |
  "collect_clock_pairs (GE x m) = {(x, m)}" |
  "collect_clock_pairs (GT x m) = {(x, m)}" |
  "collect_clock_pairs (AND cc1 cc2) = (collect_clock_pairs cc1  collect_clock_pairs cc2)"

definition collect_clkt :: "('a, 'c, 't::time, 's) transition set  ('c *'t) set"
where
  "collect_clkt S =  {collect_clock_pairs (fst (snd t)) | t . t  S}"

definition collect_clki :: "('c, 't :: time, 's) invassn  ('c *'t) set"
where
  "collect_clki I =  {collect_clock_pairs (I x) | x. True}"

definition clkp_set :: "('a, 'c, 't :: time, 's) ta  ('c *'t) set"
where
  "clkp_set A = collect_clki (inv_of A)  collect_clkt (trans_of A)"

definition collect_clkvt :: "('a, 'c, 't::time, 's) transition set  'c set"
where
  "collect_clkvt S =  {set ((fst o snd o snd o snd) t) | t . t  S}"

abbreviation clk_set where "clk_set A  fst ` clkp_set A  collect_clkvt (trans_of A)"

(* We don not need this here but most other theories will make use of this predicate *)
inductive valid_abstraction
where
  "(x,m)  clkp_set A. m  k x  x  X  m  ; collect_clkvt (trans_of A)  X; finite X
   valid_abstraction A X k"

section ‹Operational Semantics›

type_synonym ('c, 't) cval = "'c  't"

definition cval_add :: "('c,'t) cval  't::time  ('c,'t) cval" (infixr "" 64)
where
  "u  d = (λ x. u x + d)"

inductive clock_val :: "('c, 't) cval  ('c, 't::time) cconstraint  bool" ("_  _" [62, 62] 62)
where
  "u  cc1; u  cc2  u  AND cc1 cc2" |
  "u c < d  u  LT c d" |
  "u c  d  u  LE c d" |
  "u c = d  u  EQ c d" |
  "u c  d  u  GE c d" |
  "u c > d  u  GT c d"

declare clock_val.intros[intro]

inductive_cases[elim!]: "u  AND cc1 cc2"
inductive_cases[elim!]: "u  LT c d"
inductive_cases[elim!]: "u  LE c d"
inductive_cases[elim!]: "u  EQ c d"
inductive_cases[elim!]: "u  GE c d"
inductive_cases[elim!]: "u  GT c d"

fun clock_set :: "'c list  't::time  ('c,'t) cval  ('c,'t) cval"
where
  "clock_set [] _ u = u" |
  "clock_set (c#cs) t u = (clock_set cs t u)(c:=t)"

abbreviation clock_set_abbrv :: "'c list  't::time  ('c,'t) cval  ('c,'t) cval"
("[__]_" [65,65,65] 65)
where
  "[r  t]u  clock_set r t u"

inductive step_t ::
  "('a, 'c, 't, 's) ta  's  ('c, 't) cval  ('t::time)  's  ('c, 't) cval  bool"
("_  _, _ →⇗_ _, _" [61,61,61] 61)                      
where
  "u  inv_of A l; u  d  inv_of A l; d  0  A  l, ud l, u  d"

declare step_t.intros[intro!]

inductive_cases[elim!]: "A  l, ud l',u'"

lemma step_t_determinacy1:
  "A  l, ud l',u'   A  l, ud l'',u''  l' = l''"
by auto

lemma step_t_determinacy2:
  "A  l, ud l',u'   A  l, ud l'',u''  u' = u''"
by auto

lemma step_t_cont1:
  "d  0  e  0  A  l, ud l',u'  A  l', u'e l'',u''
   A  l, ud+e l'',u''"
proof -
  assume A: "d  0" "e  0" "A  l, ud l',u'" "A  l', u'e l'',u''"
  hence "u' = (u  d)" "u'' = (u'  e)" by auto
  hence "u'' = (u  (d + e))" unfolding cval_add_def by auto
  with A show ?thesis by auto
qed

inductive step_a ::
  "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) cval  'a  's  ('c, 't) cval  bool"
("_  _, _ →⇘_ _, _" [61,61,61] 61)
where
  "A  lg,a,r l'; u  g; u'  inv_of A l'; u' = [r  0]u  (A  l, ua l', u')"

inductive step ::
  "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) cval  's  ('c, 't) cval  bool"
("_  _, _  _,_" [61,61,61] 61)
where
  step_a: "A  l, ua l',u'  (A  l, u  l',u')" |
  step_t: "A  l, ud l',u'  (A  l, u  l',u')"

inductive_cases[elim!]: "A  l, u  l',u'"

declare step.intros[intro]

inductive
  steps :: "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) cval  's  ('c, 't) cval  bool"
("_  _, _ →* _, _" [61,61,61] 61)
where
  refl: "A  l, u →* l, u" |
  step: "A  l, u  l', u'  A  l', u' →* l'', u''  A  l, u →* l'', u''"

declare steps.intros[intro]

section ‹Zone Semantics›

type_synonym ('c, 't) zone = "('c, 't) cval set"

definition zone_delay :: "('c, ('t::time)) zone  ('c, 't) zone"
("_" [71] 71)
where
  "Z = {u  d|u d. u  Z  d  (0::'t)}"

definition zone_set :: "('c, 't::time) zone  'c list  ('c, 't) zone"
("__  0⇙" [71] 71)
where
  "zone_set Z r = {[r  (0::'t)]u | u . u  Z}"

inductive step_z ::
  "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) zone  's  ('c, 't) zone  bool"
("_  _, _  _, _" [61,61,61] 61)
where
  step_t_z: "A  l, Z  l, (Z  {u. u  inv_of A l})  {u. u  inv_of A l}" |
  step_a_z: "A  lg,a,r l'
               (A  l, Z  l', zone_set (Z  {u. u  g}) r  {u. u  inv_of A l'} )"

inductive_cases[elim!]: "A  l, u  l', u'"

declare step_z.intros[intro]

lemma step_z_sound:
  "A  l, Z  l',Z'  ( u'  Z'.  u  Z.  A  l, u  l',u')"
proof (induction rule: step_z.induct, goal_cases)
  case 1 thus ?case unfolding zone_delay_def by blast
next
  case (2 A l g a r l' Z)
  show ?case
  proof
    fix u' assume "u'  zone_set (Z  {u. u  g}) r  {u. u  inv_of A l'}"
    then obtain u where
      "u  g" "u'  inv_of A l'" "u' = [r0]u" "u  Z"
    unfolding zone_set_def by auto
    with step_a.intros[OF 2 this(1-3)] show "uZ. A  l, u  l',u'" by fast
  qed
qed

lemma step_z_complete:
  "A  l, u  l', u'  u  Z   Z'. A  l, Z  l', Z'  u'  Z'"
proof (induction rule: step.induct, goal_cases)
  case (1 A l u a l' u')
  then obtain g r
  where u': "u' = [r0]u" "A  lg,a,r l'" "u  g" "[r0]u  inv_of A l'"
  by (cases rule: step_a.cases) auto
  hence "u'  zone_set (Z  {u. u  g}) r  {u. u  inv_of A l'}"
  unfolding zone_set_def using u  Z by blast
  with u'(1,2) show ?case by blast
next
  case (2 A l u d l' u')
  hence u': "u' = (u  d)" "u  inv_of A l" "u  d  inv_of A l" "0  d" and "l = l'" by auto
  with u' u  Z have
    "u'  {u''  d |u'' d. u''  Z  {u. u  inv_of A l}  0  d}  {u. u  inv_of A l}"
  by fastforce
  thus ?case using l = l'  step_t_z[unfolded zone_delay_def, of A l] by blast
qed

text ‹
  Corresponds to version in old papers --
  not strong enough for inductive proof over transitive closure relation.
›
lemma step_z_complete1:
  "A  l, u  l', u'   Z. A  l, {u}  l', Z  u'  Z"
proof (induction rule: step.induct, goal_cases)
  case (1 A l u a l' u')
  then obtain g r
  where u': "u' = [r0]u" "A  lg,a,r l'" "u  g" "[r0]u  inv_of A l'"
  by (cases rule: step_a.cases) auto
  hence "{[r0]u} = zone_set ({u}  {u. u  g}) r  {u. u  inv_of A l'}"
  unfolding zone_set_def by blast
  with u'(1,2) show ?case by auto 
next
  case (2 A l u d l' u')
  hence u': "u' = (u  d)" "u  inv_of A l" "u  d  inv_of A l" "0  d" and "l = l'" by auto
  hence "{u} = {u}  {u''. u''  inv_of A l}" by fastforce 
  with u'(1) have "{u'} = {u''  d |u''. u''  {u}  {u''. u''  inv_of A l}}" by fastforce
  with u' have
    "u'  {u''  d |u'' d. u''  {u}  {u. u  inv_of A l}  0  d}  {u. u  inv_of A l}"
  by fastforce
  thus ?case using l = l' step_t_z[unfolded zone_delay_def, of A l "{u}"] by blast
qed

text ‹
  Easier proof.
›
lemma step_z_complete2:
  "A  l, u  l', u'   Z. A  l, {u}  l', Z  u'  Z"
using step_z_complete by fast

inductive
  steps_z :: "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) zone  's  ('c, 't) zone  bool"
("_  _, _ ↝* _, _" [61,61,61] 61)
where
  refl: "A  l, Z ↝* l, Z" |
  step: "A  l, Z  l', Z'  A  l', Z' ↝* l'', Z''  A  l, Z ↝* l'', Z''"

declare steps_z.intros[intro]

lemma steps_z_sound:
  "A  l, Z ↝* l', Z'  u'  Z'   u  Z. A  l, u →* l', u'"
proof (induction A l _ l' _ arbitrary: rule: steps_z.induct, goal_cases)
  case refl thus ?case by fast
next
  case (step A l Z l' Z' l'' Z'')
  then obtain u'' where u'': "A  l', u'' →* l'',u'" "u''  Z'" by auto
  then obtain u where "u  Z" "A  l, u  l',u''" using step_z_sound[OF step(1)] by blast
  with u'' show ?case by blast
qed

lemma steps_z_complete:
  "A  l, u →* l', u'  u  Z   Z'. A  l, Z ↝* l', Z'  u'  Z'"
proof (induction arbitrary: Z rule: steps.induct)
  case refl thus ?case by auto
next
  case (step A l u l' u' l'' u'' Z)
  from step_z_complete[OF this(1,4)] obtain Z' where Z': "A  l, Z  l',Z'" "u'  Z'" by auto
  then obtain Z'' where "A  l', Z' ↝* l'',Z''" "u''  Z''" using step by metis
  with Z' show ?case by blast
qed

end

Theory DBM

theory DBM
  imports Floyd_Warshall Timed_Automata
begin

chapter ‹Difference Bound Matrices›

section ‹Definitions›

text ‹
  Difference Bound Matrices (DBMs) constrain differences of clocks
  (or more precisely, the difference of values assigned to individual clocks by a valuation).
  The possible constraints are given by the following datatype:
›

datatype ('t::time) DBMEntry = Le 't | Lt 't | INF ("")

text ‹\noindent This yields a simple definition of DBMs:›

type_synonym 't DBM = "nat  nat  't DBMEntry"

text ‹\noindent
  To relate clocks with rows and columns of
  a DBM, we use a clock numbering v› of type @{typ "'c  nat"} to map clocks to indices.
  DBMs will regularly be  accompanied by a natural number $n$,
  which designates the number of clocks constrained by the matrix.
  To be able to represent the full set of clock constraints with DBMs, we add an imaginary
  clock 𝟬›, which shall be assigned to 0 in every valuation.
  In the following predicate we explicitly keep track of 𝟬›.
›

inductive dbm_entry_val :: "('c, 't) cval  'c option  'c option  ('t::time) DBMEntry  bool"
where
  "u r  d  dbm_entry_val u (Some r) None (Le d)" |
  "-u c  d  dbm_entry_val u None (Some c) (Le d)" |
  "u r < d  dbm_entry_val u (Some r) None (Lt d)" |
  "-u c < d  dbm_entry_val u None (Some c) (Lt d)" |
  "u r - u c  d  dbm_entry_val u (Some r) (Some c) (Le d)" |
  "u r - u c < d  dbm_entry_val u (Some r) (Some c) (Lt d)" |
  "dbm_entry_val _ _ _ "

declare dbm_entry_val.intros[intro]
inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Le d)"
inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Le d)"
inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Lt d)"
inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Lt d)"
inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Le d)"
inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Lt d)"

fun dbm_entry_bound :: "('t::time) DBMEntry  't"
where
  "dbm_entry_bound (Le t) = t" |
  "dbm_entry_bound (Lt t) = t" |
  "dbm_entry_bound  = 0"

inductive dbm_lt :: "('t::time) DBMEntry  't DBMEntry  bool"
("_  _" [51, 51] 50)
where
  "dbm_lt (Lt _) " |
  "dbm_lt (Le _) " |
  "a < b   dbm_lt (Le a) (Le b)" |
  "a < b   dbm_lt (Le a) (Lt b)" |
  "a  b   dbm_lt (Lt a) (Le b)" |
  "a < b   dbm_lt (Lt a) (Lt b)"

declare dbm_lt.intros[intro]

definition dbm_le :: "('t::time) DBMEntry  't DBMEntry  bool"
("_  _" [51, 51] 50)
where
  "dbm_le a b  (a  b)  a = b"

text ‹
  Now a valuation is contained in the zone represented by a DBM if it fulfills all individual
  constraints:
›

definition DBM_val_bounded :: "('c  nat)  ('c, 't) cval  ('t::time) DBM  nat  bool"
where
  "DBM_val_bounded v u m n  Le 0  m 0 0 
    ( c. v c  n  (dbm_entry_val u None (Some c) (m 0 (v c))
                       dbm_entry_val u (Some c) None (m (v c) 0)))
     ( c1 c2. v c1  n  v c2  n  dbm_entry_val u (Some c1) (Some c2) (m (v c1) (v c2)))"

abbreviation DBM_val_bounded_abbrev ::
  "('c, 't) cval  ('c  nat)  nat  ('t::time) DBM  bool"
("_ ⊢⇘_,_ _")
where
  "uv,n M  DBM_val_bounded v u M n"

abbreviation
  "dmin a b  if a  b then a else b"

lemma dbm_le_dbm_min:
  "a  b  a = dmin a b" unfolding dbm_le_def
by auto

lemma dbm_lt_asym:
  assumes "e  f"
  shows "~ f  e"
using assms
proof (safe, cases e f rule: dbm_lt.cases, goal_cases)
  case 1 from this(2) show ?case using 1(3-) by (cases f e rule: dbm_lt.cases) auto
next
  case 2 from this(2) show ?case using 2(3-) by (cases f e rule: dbm_lt.cases) auto
next
  case 3 from this(2) show ?case using 3(3-) by (cases f e rule: dbm_lt.cases) auto
next
  case 4 from this(2) show ?case using 4(3-) by (cases f e rule: dbm_lt.cases) auto
next
  case 5 from this(2) show ?case using 5(3-) by (cases f e rule: dbm_lt.cases) auto
next
  case 6 from this(2) show ?case using 6(3-) by (cases f e rule: dbm_lt.cases) auto
qed

lemma dbm_le_dbm_min2:
  "a  b  a = dmin b a"
using dbm_lt_asym by (auto simp: dbm_le_def)

lemma dmb_le_dbm_entry_bound_inf:
  "a  b  a =   b = "
apply (auto simp: dbm_le_def)
  apply (cases rule: dbm_lt.cases)
by auto

lemma dbm_not_lt_eq: "¬ a  b  ¬ b  a  a = b"
apply (cases a)
  apply (cases b, fastforce+)+
done

lemma dbm_not_lt_impl: "¬ a  b  b  a  a = b" using dbm_not_lt_eq by auto

lemma "dmin a b = dmin b a"
proof (cases "a  b")
  case True thus ?thesis by (simp add: dbm_lt_asym)
next
  case False thus ?thesis by (simp add: dbm_not_lt_eq)
qed

lemma dbm_lt_trans: "a  b  b  c  a  c"
proof (cases a b rule: dbm_lt.cases, goal_cases)
  case 1 thus ?case by simp
next
  case 2 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+
next
  case 3 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+
next
  case 4 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
  case 5 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
  case 6 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
  case 7 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
qed

lemma aux_3: "¬ a  b  ¬ b  c  a  c  c = a"
proof goal_cases
  case 1 thus ?case
  proof (cases "c  b")
    case True
    with a  c have "a  b" by (rule dbm_lt_trans)
    thus ?thesis using 1 by auto
  next
    case False thus ?thesis using dbm_not_lt_eq 1 by auto
  qed
qed

inductive_cases[elim!]: "  x"

lemma dbm_lt_asymmetric[simp]: "x  y  y  x  False"
by (cases x y rule: dbm_lt.cases) (auto elim: dbm_lt.cases)

lemma le_dbm_le: "Le a  Le b  a  b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma le_dbm_lt: "Le a  Lt b  a < b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma lt_dbm_le: "Lt a  Le b  a  b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma lt_dbm_lt: "Lt a  Lt b  a  b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma not_dbm_le_le_impl: "¬ Le a  Le b  a  b" by (metis dbm_lt.intros(3) not_less)

lemma not_dbm_lt_le_impl: "¬ Lt a  Le b  a > b" by (metis dbm_lt.intros(5) not_less)

lemma not_dbm_lt_lt_impl: "¬ Lt a  Lt b  a  b" by (metis dbm_lt.intros(6) not_less)

lemma not_dbm_le_lt_impl: "¬ Le a  Lt b  a  b" by (metis dbm_lt.intros(4) not_less)

(*>*)

(*<*)

fun dbm_add :: "('t::time) DBMEntry  't DBMEntry  't DBMEntry" (infixl "" 70)
where
  "dbm_add      _      = " |
  "dbm_add _           = " |
  "dbm_add (Le a) (Le b) = (Le (a+b))" |
  "dbm_add (Le a) (Lt b) = (Lt (a+b))" |
  "dbm_add (Lt a) (Le b) = (Lt (a+b))" |
  "dbm_add (Lt a) (Lt b) = (Lt (a+b))"

thm dbm_add.simps

lemma aux_4: "x  y  ¬ dbm_add x z  dbm_add y z  dbm_add x z = dbm_add y z"
by (cases x y rule: dbm_lt.cases) ((cases z), auto)+

lemma aux_5: "¬ x  y  dbm_add x z  dbm_add y z  dbm_add y z = dbm_add x z"
proof -
  assume lt: "dbm_add x z  dbm_add y z" "¬ x  y"
  hence "x = y  y  x" by (auto simp: dbm_not_lt_eq)
  thus ?thesis
  proof
    assume "x = y" thus ?thesis by simp
  next
    assume "y  x"
    thus ?thesis
    proof (cases y x rule: dbm_lt.cases, goal_cases)
      case 1 thus ?case using lt by auto
    next
      case 2 thus ?case using lt by auto
    next
      case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    next
      case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    next
      case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    next
      case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    qed
  qed
qed

lemma aux_42: "x  y  ¬ dbm_add z x  dbm_add z y  dbm_add z x = dbm_add z y"
by (cases x y rule: dbm_lt.cases) ((cases z), auto)+

lemma aux_52: "¬ x  y  dbm_add z x  dbm_add z y  dbm_add z y = dbm_add z x"
proof -
  assume lt: "dbm_add z x  dbm_add z y" "¬ x  y"
  hence "x = y  y  x" by (auto simp: dbm_not_lt_eq)
  thus ?thesis
  proof
    assume "x = y" thus ?thesis by simp
  next
    assume "y  x"
    thus ?thesis
    proof (cases y x rule: dbm_lt.cases, goal_cases)
      case 1 thus ?case using lt by (cases z) fastforce+
    next
      case 2 thus ?case using lt by (cases z) fastforce+
    next
      case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    next
      case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    next
      case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    next
      case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
    qed
  qed
qed

lemma dbm_add_not_inf:
  "a    b    dbm_add a b  "
by (cases a, auto, cases b, auto, cases b, auto)

lemma dbm_le_not_inf:
  "a  b  b    a  "
by (cases "a = b") (auto simp: dbm_le_def)

section ‹DBM Entries Form a Linearly Ordered Abelian Monoid›

instantiation DBMEntry :: (time) linorder
begin
  definition less_eq: "(≤)  dbm_le"
  definition less: "(<) = dbm_lt"
  instance
  proof ((standard; unfold less less_eq), goal_cases)
    case 1 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto
  next
    case 2 thus ?case by (simp add: dbm_le_def)
  next
    case 3 thus ?case unfolding dbm_le_def using dbm_lt_trans by auto
  next
    case 4 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto
  next
    case 5 thus ?case unfolding dbm_le_def using dbm_not_lt_eq by auto
  qed
end

instantiation DBMEntry :: (time) linordered_ab_monoid_add
begin
  definition mult: "(+) = dbm_add"
  definition neutral: "neutral = Le 0"
  instance proof ((standard; unfold mult neutral less less_eq), goal_cases)
    case (1 a b c) thus ?case by (cases a; cases b; cases c; auto)
  next
    case (2 a b) thus ?case by (cases a; cases b) auto
  next
    case (3 a b c)
    thus ?case unfolding dbm_le_def
    apply safe
     apply (rule dbm_lt.cases)
          apply assumption
    by (cases c; fastforce)+
  next
    case (4 x) thus ?case by (cases x) auto
  next
    case (5 x) thus ?case by (cases x) auto
  qed
end

interpretation linordered_monoid: linordered_ab_monoid_add dbm_add dbm_le dbm_lt "Le 0"
  apply (standard, fold neutral mult less_eq less)
using add.commute add.commute add_left_mono assoc by auto

lemma Le_Le_dbm_lt_D[dest]: "Le a  Lt b  a < b" by (cases rule: dbm_lt.cases) auto
lemma Le_Lt_dbm_lt_D[dest]: "Le a  Le b  a < b" by (cases rule: dbm_lt.cases) auto
lemma Lt_Le_dbm_lt_D[dest]: "Lt a  Le b  a  b" by (cases rule: dbm_lt.cases) auto
lemma Lt_Lt_dbm_lt_D[dest]: "Lt a  Lt b  a < b" by (cases rule: dbm_lt.cases) auto

lemma Le_le_LeI[intro]: "a  b  Le a  Le b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LeI[intro]: "a  b  Lt a  Le b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LtI[intro]: "a  b  Lt a  Lt b" unfolding less_eq dbm_le_def by auto
lemma Le_le_LtI[intro]: "a < b  Le a  Lt b" unfolding less_eq dbm_le_def by auto
lemma Lt_lt_LeI: "x  y  Lt x < Le y" unfolding less by auto

lemma Le_le_LeD[dest]: "Le a  Le b  a  b" unfolding dbm_le_def less_eq by auto
lemma Le_le_LtD[dest]: "Le a  Lt b  a < b" unfolding dbm_le_def less_eq by auto
lemma Lt_le_LeD[dest]: "Lt a  Le b  a  b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LtD[dest]: "Lt a  Lt b  a  b" unfolding less_eq dbm_le_def by auto

lemma inf_not_le_Le[simp]: "  Le x = False" unfolding less_eq dbm_le_def by auto
lemma inf_not_le_Lt[simp]: "  Lt x = False" unfolding less_eq dbm_le_def by auto
lemma inf_not_lt[simp]: "  x = False" by auto

lemma any_le_inf: "x  " by (metis less_eq dmb_le_dbm_entry_bound_inf le_cases)


section ‹Basic Properties of DBMs›

subsection ‹DBMs and Length of Paths›

lemma dbm_entry_val_add_1: "dbm_entry_val u (Some c) (Some d) a   dbm_entry_val u (Some d) None b
        dbm_entry_val u (Some c) None (dbm_add a b)"
proof (cases a, goal_cases)
  case 1 thus ?thesis
  apply (cases b)
    apply auto
   using add_mono_thms_linordered_semiring(1) apply fastforce
  using add_le_less_mono by fastforce
next
  case 2 thus ?thesis
  apply (cases b)
    apply auto
   apply (simp add: dbm_entry_val.intros(3) diff_less_eq less_le_trans)
  by (metis add_le_less_mono dbm_entry_val.intros(3) diff_add_cancel less_imp_le)
next
  case 3 thus ?thesis by (cases b) auto
qed

lemma dbm_entry_val_add_2: "dbm_entry_val u None (Some c) a  dbm_entry_val u (Some c) (Some d) b
        dbm_entry_val u None (Some d) (dbm_add a b)"
proof (cases a, goal_cases)
  case 1 thus ?thesis
  apply (cases b)
    apply auto
   using add_mono_thms_linordered_semiring(1) apply fastforce
  using add_le_less_mono by fastforce
next
  case 2 thus ?thesis
  apply (cases b)
    apply auto
   using add_mono_thms_linordered_field(3) apply fastforce
  using add_strict_mono by fastforce
next
  case 3 thus ?thesis by (cases b) auto
qed

lemma dbm_entry_val_add_3:
  "dbm_entry_val u (Some c) (Some d) a   dbm_entry_val u (Some d) (Some e) b
    dbm_entry_val u (Some c) (Some e) (dbm_add a b)"
proof (cases a, goal_cases)
  case 1 thus ?thesis
  apply (cases b)
    apply auto
   using add_mono_thms_linordered_semiring(1) apply fastforce
  using add_le_less_mono by fastforce
next
  case 2 thus ?thesis
  apply (cases b)
    apply auto
   using add_mono_thms_linordered_field(3) apply fastforce
  using add_strict_mono by fastforce
next
  case 3 thus ?thesis by (cases b) auto
qed

lemma dbm_entry_val_add_4:
  "dbm_entry_val u (Some c) None a  dbm_entry_val u None (Some d) b
    dbm_entry_val u (Some c) (Some d) (dbm_add a b)"
proof (cases a, goal_cases)
  case 1 thus ?thesis
  apply (cases b)
    apply auto
   using add_mono_thms_linordered_semiring(1) apply fastforce
  using add_le_less_mono by fastforce
next
  case 2 thus ?thesis
  apply (cases b)
    apply auto
   using add_mono_thms_linordered_field(3) apply fastforce
  using add_strict_mono by fastforce
next
  case 3 thus ?thesis by (cases b) auto
qed

no_notation dbm_add (infixl "" 70)

lemma DBM_val_bounded_len_1'_aux:
  assumes "DBM_val_bounded v u m n" "v c  n" " k  set vs. k > 0  k  n  ( c. v c = k)"
  shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)" using assms
proof (induction vs arbitrary: c)
  case Nil then show ?case unfolding DBM_val_bounded_def by auto
next
  case (Cons k vs)
  then obtain c' where c': "k > 0" "k  n" "v c' = k" by auto
  with Cons have "dbm_entry_val u (Some c') None (len m (v c') 0 vs)" by auto
  moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c'
  by (auto simp add: DBM_val_bounded_def)
  ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 vs)"
  using dbm_entry_val_add_1 unfolding mult by fastforce
  with c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_3'_aux:
  "DBM_val_bounded v u m n  v c  n  v d  n   k  set vs. k > 0  k  n  ( c. v c = k)
    dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) vs)"
proof (induction vs arbitrary: c)
  case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
  case (Cons k vs)
  then obtain c' where c': "k > 0" "k  n" "v c' = k" by auto
  with Cons have "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) vs)" by auto
  moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c'
  by (auto simp add: DBM_val_bounded_def)
  ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) vs)"
  using dbm_entry_val_add_3 unfolding mult by fastforce
  with c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_2'_aux:
  "DBM_val_bounded v u m n  v c  n   k  set vs. k > 0  k  n  ( c. v c = k)
   dbm_entry_val u None (Some c) (len m 0 (v c) vs)"
proof (cases vs, goal_cases)
  case 1 then show ?thesis unfolding DBM_val_bounded_def by auto
next
  case (2 k vs)
  then obtain c' where c': "k > 0" "k  n" "v c' = k" by auto
  with 2 have "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) vs)"
  using DBM_val_bounded_len_3'_aux by auto
  moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))"
  using 2 c' by (auto simp add: DBM_val_bounded_def)
  ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) vs)"
  using dbm_entry_val_add_2 unfolding mult by fastforce
  with 2(4) c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma cnt_0_D:
  "cnt x xs = 0  x  set xs"
apply (induction xs)
 apply simp
apply (rename_tac a xs)
apply (case_tac "x = a")
by simp+

lemma cnt_at_most_1_D:
  "cnt x (xs @ x # ys)  1  x  set xs  x  set ys"
apply (induction xs)
  apply auto[]
  using cnt_0_D apply force
 apply (rename_tac a xs)
 apply (case_tac "a = x")
  apply simp
 apply simp
done

lemma nat_list_0 [intro]:
  "x  set xs  0  set (xs :: nat list)  x > 0"
by (induction xs) auto

lemma DBM_val_bounded_len':
  fixes v
  defines "vo  λ k. if k = 0 then None else Some (SOME c. v c = k)"
  assumes "DBM_val_bounded v u m n" "cnt 0 (i # j # vs)  1"
          " k  set (i # j # vs). k > 0  k  n  ( c. v c = k)"
  shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)"
proof -
  show ?thesis
  proof (cases " k  set vs. k > 0")
    case True
    with assms have *: " k  set vs. k > 0  k  n  ( c. v c = k)" by auto
    show ?thesis
    proof (cases "i = 0")
      case True
      then have i: "vo i = None" by (simp add: vo_def)
      show ?thesis
      proof (cases "j = 0")
        case True with assms i = 0 show ?thesis by auto
      next
        case False
        with assms obtain c2 where c2: "j  n" "v c2 = j" "vo j = Some c2"
        unfolding vo_def by (fastforce intro: someI)
        with i = 0 i DBM_val_bounded_len_2'_aux[OF assms(2) _ *] show ?thesis by auto
      qed
    next
      case False
      with assms(4) obtain c1 where c1: "i  n" "v c1 = i" "vo i = Some c1"
      unfolding vo_def by (fastforce intro: someI)
      show ?thesis
      proof (cases "j = 0")
        case True
        with DBM_val_bounded_len_1'_aux[OF assms(2) _ *] c1 show ?thesis by (auto simp: vo_def)
      next
        case False
        with assms obtain c2 where c2: "j  n" "v c2 = j" "vo j = Some c2"
        unfolding vo_def by (fastforce intro: someI)
        with c1 DBM_val_bounded_len_3'_aux[OF assms(2) _ _ *] show ?thesis by auto
      qed
    qed
  next
    case False
    then have " k  set vs. k = 0" by auto
    then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last) 
    with cnt_at_most_1_D[of 0 "i # j # us"] assms(3) have
      "0  set us" "0  set ws" "i  0" "j  0"
    by auto
    with vs have vs: "vs = us @ 0 # ws" " k  set us. k > 0" " k  set ws. k > 0" by auto
    with assms(4) have v:
      "kset us. 0 < k  k  n  (c. v c = k)" "kset ws. 0 < k  k  n  (c. v c = k)"
    by auto
    from i  0 j  0 assms obtain c1 c2 where
      c1: "i  n" "v c1 = i" "vo i = Some c1" and c2: "j  n" "v c2 = j" "vo j = Some c2"
    unfolding vo_def by (fastforce intro: someI)
    with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(2) _ v(1)] DBM_val_bounded_len_2'_aux[OF assms(2) _ v(2)]]
    have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto
    moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)"
    by (simp add: len_comp mult)
    ultimately show ?thesis using c1 c2 by auto
  qed
qed

lemma DBM_val_bounded_len'1:
  fixes v
  assumes "DBM_val_bounded v u m n" "0  set vs" "v c  n"
          " k  set vs. k > 0  k  n  ( c. v c = k)"
  shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)"
using DBM_val_bounded_len_1'_aux[OF assms(1,3)] assms(2,4) by fastforce

lemma DBM_val_bounded_len'2:
  fixes v
  assumes "DBM_val_bounded v u m n" "0  set vs" "v c  n"
          " k  set vs. k > 0  k  n  ( c. v c = k)"
  shows "dbm_entry_val u None (Some c) (len m 0 (v c) vs)"
using DBM_val_bounded_len_2'_aux[OF assms(1,3)] assms(2,4) by fastforce

lemma DBM_val_bounded_len'3:
  fixes v
  assumes "DBM_val_bounded v u m n" "cnt 0 vs  1" "v c1  n" "v c2  n"
          " k  set vs. k > 0  k  n  ( c. v c = k)"
  shows "dbm_entry_val u (Some c1) (Some c2) (len m (v c1) (v c2) vs)"
proof -
  show ?thesis
  proof (cases " k  set vs. k > 0")
    case True
    with assms have " k  set vs. k > 0  k  n  ( c. v c = k)" by auto
    with DBM_val_bounded_len_3'_aux[OF assms(1,3,4)] show ?thesis by auto
  next
    case False
    then have " k  set vs. k = 0" by auto
    then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last) 
    with cnt_at_most_1_D[of 0 "us"] assms(2) have
      "0  set us" "0  set ws"
    by auto
    with vs have vs: "vs = us @ 0 # ws" " k  set us. k > 0" " k  set ws. k > 0" by auto
    with assms(5) have v:
      "kset us. 0 < k  k  n  (c. v c = k)" "kset ws. 0 < k  k  n  (c. v c = k)"
    by auto
    with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(1,3) v(1)] DBM_val_bounded_len_2'_aux[OF assms(1,4) v(2)]]
    have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto
    moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)"
    by (simp add: len_comp mult)
    ultimately show ?thesis by auto
  qed
qed

lemma DBM_val_bounded_len'':
  fixes v
  defines "vo  λ k. if k = 0 then None else Some (SOME c. v c = k)"
  assumes "DBM_val_bounded v u m n" "i  0  j  0"
          " k  set (i # j # vs). k > 0  k  n  ( c. v c = k)"
  shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)" using assms
proof (induction "length vs" arbitrary: i vs rule: less_induct)
  case less
  show ?case
  proof (cases " k  set vs. k > 0")
    case True
    with less.prems have *: " k  set vs. k > 0  k  n  ( c. v c = k)" by auto
    show ?thesis
    proof (cases "i = 0")
      case True
      then have i: "vo i = None" by (simp add: vo_def)
      show ?thesis
      proof (cases "j = 0")
        case True with less.prems i = 0 show ?thesis by auto
      next
        case False
        with less.prems obtain c2 where c2: "j  n" "v c2 = j" "vo j = Some c2"
        unfolding vo_def by (fastforce intro: someI)
        with i = 0 i DBM_val_bounded_len_2'_aux[OF less.prems(1) _ *] show ?thesis by auto
      qed
    next
      case False
      with less.prems obtain c1 where c1: "i  n" "v c1 = i" "vo i = Some c1"
      unfolding vo_def by (fastforce intro: someI)
      show ?thesis
      proof (cases "j = 0")
        case True
        with DBM_val_bounded_len_1'_aux[OF less.prems(1) _ *] c1 show ?thesis by (auto simp: vo_def)
      next
        case False
        with less.prems obtain c2 where c2: "j  n" "v c2 = j" "vo j = Some c2"
        unfolding vo_def by (fastforce intro: someI)
        with c1 DBM_val_bounded_len_3'_aux[OF less.prems(1) _ _ *] show ?thesis by auto
      qed
    qed
  next
    case False
    then have " us ws. vs = us @ 0 # ws  ( k  set us. k > 0)"
    proof (induction vs)
      case Nil then show ?case by auto
    next
      case (Cons x vs)
      show ?case
      proof (cases "x = 0")
        case True then show ?thesis by fastforce
      next
        case False
        with Cons.prems have "¬ (aset vs. 0 < a)" by auto
        from Cons.IH[OF this] obtain us ws where "vs = us @ 0 # ws" "aset us. 0 < a" by auto
        with False have "x # vs = (x # us) @ 0 # ws" "aset (x # us). 0 < a" by auto
        then show ?thesis by blast
      qed
    qed
    then obtain us ws where vs: "vs = us @ 0 # ws" " k  set us. k > 0" by blast
    then show ?thesis
oops

lemma DBM_val_bounded_len_1: "DBM_val_bounded v u m n  v c  n   c  set cs. v c  n
       dbm_entry_val u (Some c) None (len m (v c) 0 (map v cs))"
proof (induction cs arbitrary: c)
  case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
  case (Cons c' cs)
  hence "dbm_entry_val u (Some c') None (len m (v c') 0 (map v cs))" by auto
  moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems
  by (simp add: DBM_val_bounded_def)
  ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 (map v cs))"
  using dbm_entry_val_add_1 unfolding mult by fastforce
  thus ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_3: "DBM_val_bounded v u m n  v c  n  v d  n   c  set cs. v c  n
       dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) (map v cs))"
proof (induction cs arbitrary: c)
  case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
  case (Cons c' cs)
  hence "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) (map v cs))" by auto
  moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems
  by (simp add: DBM_val_bounded_def)
  ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) (map v cs))"
  using dbm_entry_val_add_3 unfolding mult by fastforce
  thus ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_2: "DBM_val_bounded v u m n  v c  n   c  set cs. v c  n
       dbm_entry_val u None (Some c) (len m 0 (v c) (map v cs))"
proof (cases cs, goal_cases)
  case 1 thus ?thesis unfolding DBM_val_bounded_def by auto
next
  case (2 c' cs)
  hence "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) (map v cs))"
  using DBM_val_bounded_len_3 by auto
  moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))"
  using 2 by (simp add: DBM_val_bounded_def)
  ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) (map v cs))"
  using dbm_entry_val_add_2 unfolding mult by fastforce
  thus ?case using 2(4) unfolding DBM_val_bounded_def by simp 
qed

end

Theory Paths_Cycles

theory Paths_Cycles
  imports Floyd_Warshall Timed_Automata
begin

chapter ‹Library for Paths, Arcs and Lengths›

lemma length_eq_distinct:
  assumes "set xs = set ys" "distinct xs" "length xs = length ys"
  shows "distinct ys"
using assms card_distinct distinct_card by fastforce

section ‹Arcs›

fun arcs :: "nat  nat  nat list  (nat * nat) list" where
  "arcs a b [] = [(a,b)]" |
  "arcs a b (x # xs) = (a, x) # arcs x b xs"

definition arcs' :: "nat list  (nat * nat) set" where
  "arcs' xs = set (arcs (hd xs) (last xs) (butlast (tl xs)))"

lemma arcs'_decomp:
  "length xs > 1  (i, j)  arcs' xs   zs ys. xs = zs @ i # j # ys"
proof (induction xs)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  then have "length xs > 0" by auto
  then obtain y ys where xs: "xs = y # ys" by (metis Suc_length_conv less_imp_Suc_add)
  show ?case
  proof (cases "(i, j) = (x, y)")
    case True
    with xs have "x # xs = [] @ i # j # ys" by simp
    then show ?thesis by auto
  next
    case False
    then show ?thesis
    proof (cases "length ys > 0", goal_cases)
      case 2
      then have "ys = []" by auto
      then have "arcs' (x#xs) = {(x,y)}" using xs by (auto simp add: arcs'_def)
      with Cons.prems(2) 2(1) show ?case by auto
    next
      case True
      with xs Cons.prems(2) False have "(i, j)  arcs' xs" by (auto simp add: arcs'_def)
      with Cons.IH[OF _ this] True xs obtain zs ys where "xs = zs @ i # j # ys" by auto
      then have "x # xs = (x # zs) @ i # j # ys" by simp
      then show ?thesis by blast
    qed
  qed
qed

lemma arcs_decomp_tail:
  "arcs j l (ys @ [i]) = arcs j i ys @ [(i, l)]"
by (induction ys arbitrary: j) auto

lemma arcs_decomp: "xs = ys @ y # zs  arcs x z xs = arcs x y ys @ arcs y z zs"
by (induction ys arbitrary: x xs) simp+

lemma distinct_arcs_ex:
  "distinct xs  i  set xs  xs  []   a b. a  x  (a,b)  set (arcs i j xs)"
 apply (induction xs arbitrary: i)
  apply simp
 apply (rename_tac a xs i)
 apply (case_tac xs)
  apply simp
  apply metis
by auto

lemma cycle_rotate_2_aux:
  "(i, j)  set (arcs a b (xs @ [c]))  (i,j)  (c,b)  (i, j)  set (arcs a c xs)"
by (induction xs arbitrary: a) auto

lemma arcs_set_elem1:
  assumes "j  k" "k  set (i # xs)"
  shows " l. (k, l)  set (arcs i j xs)" using assms
by (induction xs arbitrary: i) auto

lemma arcs_set_elem2:
  assumes "i  k" "k  set (j # xs)"
  shows " l. (l, k)  set (arcs i j xs)" using assms
proof (induction xs arbitrary: i)
  case Nil then show ?case by simp
next
  case (Cons x xs)
  then show ?case by (cases "k = x") auto
qed

section ‹Length of Paths›

lemmas (in linordered_ab_monoid_add) comm = add.commute

lemma len_add:
  fixes M :: "('a :: linordered_ab_monoid_add) mat"
  shows "len M i j xs + len M i j xs = len (λi j. M i j + M i j) i j xs"
proof (induction xs arbitrary: i j)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  have "M i x + len M x j xs + (M i x + len M x j xs) = M i x + (len M x j xs + M i x) + len M x j xs"
  by (simp add: assoc)
  also have " = M i x + (M i x + len M x j xs) + len M x j xs" by (simp add: comm)
  also have " = (M i x + M i x) + (len M x j xs + len M x j xs)" by (simp add: assoc)
  finally have "M i x + len M x j xs + (M i x + len M x j xs)
                = (M i x + M i x) + len (λi j. M i j + M i j) x j xs"
  using Cons by simp
  thus ?case by simp
qed

section ‹Canonical Matrices›

abbreviation
  "canonical M n   i j k. i  n  j  n  k  n  M i k  M i j + M j k"

lemma fw_canonical:
 "cycle_free m n  canonical (fw m n n n n) n"
proof (clarify, goal_cases)
  case 1
  with fw_shortest[OF ‹cycle_free m n] show ?case
  by auto
qed

lemma canonical_len:
  "canonical M n  i  n  j  n  set xs  {0..n}  M i j  len M i j xs"
proof (induction xs arbitrary: i)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  then have "M x j  len M x j xs" by auto
  from Cons.prems ‹canonical M n have "M i j  M i x + M x j" by simp
  also with Cons have "  M i x + len M x j xs" by (simp add: add_mono)
  finally show ?case by simp
qed

section ‹Cycle Rotation›

lemma cycle_rotate:
  fixes M :: "('a :: linordered_ab_monoid_add) mat"
  assumes "length xs > 1" "(i, j)  arcs' xs"
  shows " ys zs. len M a a xs = len M i i (j # ys @ a # zs)  xs = zs @ i # j # ys" using assms
proof -
  assume A: "length xs > 1" "(i, j)  arcs' xs"
  from arcs'_decomp[OF this] obtain ys zs where xs: "xs = zs @ i # j # ys" by blast
  from len_decomp[OF this, of M a a]
  have "len M a a xs = len M a i zs + len M i a (j # ys)" .
  also have " = len M i a (j # ys) + len M a i zs" by (simp add: comm)
  also from len_comp[of M i i "j # ys" a zs] have " = len M i i (j # ys @ a # zs)" by auto
  finally show ?thesis using xs by auto
qed

lemma cycle_rotate_2:
  fixes M :: "('a :: linordered_ab_monoid_add) mat"
  assumes "xs  []" "(i, j)  set (arcs a a xs)"
  shows " ys. len M a a xs = len M i i (j # ys)  set ys  set (a # xs)  length ys < length xs"
using assms proof -
  assume A:"xs  []" "(i, j)  set (arcs a a xs)"
  { fix ys assume A:"a = i" "xs = j # ys"
    then have ?thesis by auto
  } note * = this
  { fix b ys assume A:"a = j" "xs = ys @ [i]"
    then have ?thesis
    proof (auto, goal_cases)
      case 1
      have "len M j j (ys @ [i]) = M i j + len M j i ys"
      using len_decomp[of "ys @ [i]" ys i "[]" M j j] by (auto simp: comm)
      thus ?case by blast
    qed
  } note ** = this
  { assume "length xs = 1"
    then obtain b where xs: "xs = [b]" by (metis One_nat_def length_0_conv length_Suc_conv) 
    with A(2) have "a = i  b = j  a = j  b = i" by auto
    then have ?thesis using * ** xs by auto
  } note *** = this
  show ?thesis
  proof (cases "length xs = 0")
    case True with A show ?thesis by auto
  next
    case False
    thus ?thesis
    proof (cases "length xs = 1", goal_cases)
      case True with *** show ?thesis by auto
    next
      case 2
      hence "length xs > 1" by linarith
      then obtain b c ys where ys:"xs = b # ys @ [c]"
      by (metis One_nat_def assms(1) 2(2) length_0_conv length_Cons list.exhaust rev_exhaust) 
      thus ?thesis
      proof (cases "(i,j) = (a,b)", goal_cases)
        case True
        with ys * show ?thesis by auto
      next
        case False
        then show ?thesis
        proof (cases "(i,j) = (c,a)", goal_cases)
          case True
          with ys ** show ?thesis by auto
        next
          case 2
          with A(2) ys have "(i, j)  arcs' xs"
          using cycle_rotate_2_aux by (auto simp: arcs'_def) (* slow *)
          from cycle_rotate[OF ‹length xs > 1 this, of M a] show ?thesis by auto
        qed
      qed
    qed
  qed
qed

lemma cycle_rotate_len_arcs:
  fixes M :: "('a :: linordered_ab_monoid_add) mat"
  assumes "length xs > 1" "(i, j)  arcs' xs"
  shows " ys zs. len M a a xs = len M i i (j # ys @ a # zs)
                 set (arcs a a xs) = set (arcs i i (j # ys @ a # zs))  xs = zs @ i # j # ys"
using assms
proof -
  assume A: "length xs > 1" "(i, j)  arcs' xs"
  from arcs'_decomp[OF this] obtain ys zs where xs: "xs = zs @ i # j # ys" by blast
  from len_decomp[OF this, of M a a]
  have "len M a a xs = len M a i zs + len M i a (j # ys)" .
  also have " = len M i a (j # ys) + len M a i zs" by (simp add: comm)
  also from len_comp[of M i i "j # ys" a zs] have " = len M i i (j # ys @ a # zs)" by auto
  finally show ?thesis
  using xs arcs_decomp[OF xs, of a a] arcs_decomp[of "j # ys @ a # zs" "j # ys" a zs i i] by force
qed

lemma cycle_rotate_2':
  fixes M :: "('a :: linordered_ab_monoid_add) mat"
  assumes "xs  []" "(i, j)  set (arcs a a xs)"
  shows " ys. len M a a xs = len M i i (j # ys)  set (i # j # ys) = set (a # xs)
              1 + length ys = length xs  set (arcs a a xs) = set (arcs i i (j # ys))"
proof -
  note A = assms
  { fix ys assume A:"a = i" "xs = j # ys"
    then have ?thesis by auto
  } note * = this
  { fix b ys assume A:"a = j" "xs = ys @ [i]"
    then have ?thesis
    proof (auto, goal_cases)
      case 1
      have "len M j j (ys @ [i]) = M i j + len M j i ys"
      using len_decomp[of