Theory FW_More

theory FW_More
  imports 
    DBM_Basics 
    Floyd_Warshall.FW_Code
begin

section ‹Partial Floyd-Warshall Preserves Zones›

lemma fwi_len_distinct:
  "∃ ys. set ys ⊆ {k} ∧ fwi m n k n n i j = len m i j ys ∧ i ∉ set ys ∧ j ∉ set ys ∧ distinct ys"
  if "i ≤ n" "j ≤ n" "k ≤ n" "m k k ≥ 0"
  using fwi_step'[of m, OF that(4), of n n n i j] that
  apply (clarsimp split: if_splits simp: min_def)
  by (rule exI[where x = "[]"] exI[where x = "[k]"]; auto simp: add_increasing add_increasing2)+

lemma FWI_mono:
  "i ≤ n ⟹ j ≤ n ⟹ FWI M n k i j ≤ M i j"
  using fwi_mono[of _ n _ M k n n, folded FWI_def, rule_format] .

lemma FWI_zone_equiv:
  "[M]⇘v,n⇙ = [FWI M n k]⇘v,n⇙" if surj_on: "∀ k ≤ n. k > 0 ⟶ (∃ c. v c = k)" and "k ≤ n"
proof safe
  fix u assume A: "u ∈ [FWI M n k]⇘v,n⇙"
  { fix i j assume "i ≤ n" "j ≤ n"
    then have "FWI M n k i j ≤ M i j" by (rule FWI_mono)
    hence "FWI M n k i j ≼ M i j" by (simp add: less_eq)
  }
  with DBM_le_subset[of n "FWI M n k" M] A show "u ∈ [M]⇘v,n⇙" by auto
next
  fix u assume u:"u ∈ [M]⇘v,n⇙"
  hence *:"DBM_val_bounded v u M n" by (simp add: DBM_zone_repr_def)
  note ** = DBM_val_bounded_neg_cycle[OF this _ _ _ surj_on]
  have cyc_free: "cyc_free M n" using ** by fastforce
  from cyc_free_diag[OF this] ‹k ≤ n› have "M k k ≥ 0" by auto

  have "DBM_val_bounded v u (FWI M n k) n" unfolding DBM_val_bounded_def
  proof (safe, goal_cases)
    case 1
    with ‹k ≤ n› ‹M k k ≥ 0› cyc_free show ?case
      unfolding FWI_def neutral[symmetric] less_eq[symmetric]
      by - (rule fwi_cyc_free_diag[where I = "{0..n}"]; auto)
  next
    case (2 c)
    with ‹k ≤ n› ‹M k k ≥ 0› fwi_len_distinct[of 0 n "v c" k M] obtain xs where xs:
      "FWI M n k 0 (v c) = len M 0 (v c) xs" "set xs ⊆ {0..n}" "0 ∉ set xs"
      unfolding FWI_def by force
    with surj_on ‹v c ≤ n› show ?case unfolding xs(1)
      by - (rule DBM_val_bounded_len'2[OF *]; auto)
  next
    case (3 c)
    with ‹k ≤ n› ‹M k k ≥ 0› fwi_len_distinct[of "v c" n 0 k M] obtain xs where xs:
      "FWI M n k (v c) 0 = len M (v c) 0 xs" "set xs ⊆ {0..n}"
      "0 ∉ set xs" "v c ∉ set xs"
      unfolding FWI_def by force
    with surj_on ‹v c ≤ n› show ?case unfolding xs(1)
      by - (rule DBM_val_bounded_len'1[OF *]; auto)
  next
    case (4 c1 c2)
    with ‹k ≤ n› ‹M k k ≥ 0› fwi_len_distinct[of "v c1" n "v c2" k M] obtain xs where xs:
      "FWI M n k (v c1) (v c2) = len M (v c1) (v c2) xs" "set xs ⊆ {0..n}"
      "v c1 ∉ set xs" "v c2 ∉ set xs" "distinct xs"
      unfolding FWI_def by force
    with surj_on ‹v c1 ≤ n› ‹v c2 ≤ n› show ?case
      unfolding xs(1) by - (rule DBM_val_bounded_len'3[OF *]; auto dest: distinct_cnt[of _ 0])
  qed
  then show "u ∈ [FWI M n k]⇘v,n⇙" unfolding DBM_zone_repr_def by simp
qed

end