Theory Graph

section‹Multigraphs with Partially Ordered Weights›

(*<*)
theory Graph
  imports "HOL-Library.Sublist" Antichain
begin
(*>*)

abbreviation (input) FROM where
  "FROM ≡ λ(s, l, t). s"

abbreviation (input) LBL where
  "LBL ≡ λ(s, l, t). l"

abbreviation (input) TO where
  "TO ≡ λ(s, l, t). t"

notation subseq (infix "≼" 50)

locale graph =
  fixes weights :: "'vtx :: finite ⇒ 'vtx ⇒ 'lbl :: {order, monoid_add} antichain"
  assumes zero_le[simp]: "0 ≤ (s::'lbl)"
    and plus_mono: "(s1::'lbl) ≤ s2 ⟹ s3 ≤ s4 ⟹ s1 + s3 ≤ s2 + s4"
    and summary_self: "weights loc loc = {}⇩A"
begin

lemma le_plus: "(s::'lbl) ≤ s + s'" "(s'::'lbl) ≤ s + s'"
  by (intro plus_mono[of s s 0 s', simplified] plus_mono[of 0 s s' s', simplified])+

subsection‹Paths›

inductive path :: "'vtx ⇒ 'vtx ⇒ ('vtx × 'lbl × 'vtx) list ⇒ bool" where
  path0: "l1 = l2 ⟹ path l1 l2 []"
| path: "path l1 l2 xs ⟹ lbl ∈⇩A weights l2 l3 ⟹ path l1 l3 (xs @ [(l2, lbl, l3)])"

inductive_cases path0E: "path l1 l2 []"
inductive_cases path_AppendE: "path l1 l3 (xs @ [(l2,s,l2')])"

lemma path_trans: "path l1 l2 xs ⟹ path l2 l3 ys ⟹ path l1 l3 (xs @ ys)"
  by (rotate_tac, induct l2 l3 ys rule: path.induct)
    (auto intro: path.path simp flip: append_assoc)

lemma path_take_from: "path l1 l2 xs ⟹ m < length xs ⟹ FROM (xs ! m) = l2' ⟹ path l1 l2' (take m xs)"
proof (induct l1 l2 xs rule: path.induct)
  case (path l1 l2 xs lbl l3)
  then show ?case
    apply (unfold take_append)
    apply simp
    apply (cases "l2=l2'")
     apply (metis linorder_not_less nth_append take_all)
    apply (metis case_prod_conv less_Suc_eq nth_append nth_append_length)
    done
qed simp

lemma path_take_to: "path l1 l2 xs ⟹ m < length xs ⟹ TO (xs ! m) = l2' ⟹ path l1 l2' (take (m+1) xs)"
proof (induct l1 l2 xs rule: path.induct)
  case (path l1 l2 xs lbl l3)
  then show ?case
    apply (cases "m < length xs")
     apply (simp add: nth_append)
    apply clarsimp
    apply (metis case_prod_conv less_antisym nth_append_length path.path)
    done
qed simp

lemma path_determines_loc: "path l1 l2 xs ⟹ path l1 l3 xs ⟹ l2 = l3"
  by (induct l1 l2 xs rule: path.induct) (auto elim: path.cases)

lemma path_first_loc: "path loc loc' xs ⟹ xs ≠ [] ⟹ FROM (xs ! 0) = loc"
proof (induct rule: path.induct)
  case (path l1 l2 xs lbl l3)
  then show ?case
    by (auto elim: path0E simp: nth_append)
qed simp

lemma path_to_eq_from: "path loc1 loc2 xs ⟹ i + 1 < length xs ⟹ FROM (xs ! (i+1)) = TO (xs ! i)"
proof (induct rule: path.induct)
  case (path l1 l2 xs lbl l3)
  then show ?case
    apply (cases "i + 1 < length xs")
     apply (simp add: nth_append)
    apply (simp add: nth_append)
    apply (metis add.commute drop_eq_Nil hd_drop_conv_nth id_take_nth_drop linorder_not_less path_determines_loc path_take_to plus_1_eq_Suc take_hd_drop)
    done
qed simp

lemma path_singleton[intro, simp]: "s ∈⇩A weights l1 l2 ⟹ path l1 l2 [(l1,s,l2)]"
  by (subst path.simps) (auto simp: path.intros)

lemma path_appendE: "path l1 l3 (xs @ ys) ⟹ ∃l2. path l2 l3 ys ∧ path l1 l2 xs"
proof (induct l1 l3 "xs@ys" arbitrary: xs ys rule: path.induct)
  case (path0 l1 l2)
  then show ?case by (auto intro: path.intros)
next
  case (path l1 l2 xs lbl l3 xs' ys')
  from path(1,3-) show ?case
    apply -
    apply (subst (asm) append_eq_append_conv2[of xs "[(l2,lbl,l3)]" xs' ys'])
    apply (elim exE conjE disjE)
    subgoal for us
      using path(2)[of xs' us]
      by (auto intro: path.intros)
    subgoal for us
      by (cases "us=[]") (auto intro: path.intros simp: Cons_eq_append_conv)
    done
qed

lemma path_replace_prefix:
  "path l1 l3 (xs @ zs) ⟹ path l1 l2 ys ⟹ path l1 l2 xs ⟹ path l1 l3 (ys @ zs)"
  by (drule path_appendE) (auto elim!: path_trans dest: path_determines_loc)

lemma drop_subseq: "n ≤ length xs ⟹ drop n xs ≼ xs"
  by (auto simp: suffix_def intro!: exI[of _ "take n xs"])

lemma take_subseq[simp, intro]: "take n xs ≼ xs"
  by (induct xs) auto

lemma map_take_subseq[simp, intro]: "map f (take n xs) ≼ map f xs"
  by (rule subseq_map, induct xs) auto

lemma path_distinct:
  "path l1 l2 xs ⟹ ∃xs'. distinct xs' ∧ path l1 l2 xs' ∧ map LBL xs' ≼ map LBL xs"
proof (induct rule: path.induct)
  case (path0 l1 l2)
  then show ?case
    by (intro exI[of _ "[]"]) (auto intro: path.intros)
next
  case (path l1 l2 xs lbl l3)
  then obtain xs' where ih: "path l1 l2 xs'" "distinct xs'" "map LBL xs' ≼ map LBL xs"
    by blast
  then show ?case
  proof (cases "(l2, lbl, l3) ∈ set xs'")
    case True
    then obtain m where m: "m < length xs'" "xs' ! m = (l2, lbl, l3)"
      unfolding in_set_conv_nth by blast
    from m ih have "path l1 l2 (take m xs')"
      by (auto intro: path_take_from)
    with m ih path show ?thesis
      apply (intro exI[of _ "take m xs' @ [(l2, lbl, l3)]"])
      apply (rule conjI)
       apply (metis distinct_take take_Suc_conv_app_nth)
      apply (rule conjI)
       apply (rule path.intros)
        apply simp
       apply simp
      apply simp
      apply (metis ih(3) subseq_order.trans take_map take_subseq)
      done
  next
    case False
    with ih path(3) show ?thesis
      by (auto intro!: exI[of _ "xs' @ [(l2, lbl, l3)]"] intro: path.intros)
  qed
qed

lemma path_edge: "(l1', lbl, l2') ∈ set xs ⟹ path l1 l2 xs ⟹ lbl ∈⇩A weights l1' l2'"
  by (rotate_tac, induct rule: path.induct) auto

subsection‹Path Weights›

abbreviation sum_weights :: "'lbl list ⇒ 'lbl" where
  "sum_weights xs ≡ foldr (+) xs 0"
abbreviation "sum_path_weights xs ≡ sum_weights (map LBL xs)"

definition "path_weightp l1 l2 s ≡ (∃xs. path l1 l2 xs ∧ s = sum_path_weights xs)"

lemma sum_not_less_zero[simp, dest]: "(s::'lbl) < 0 ⟹ False"
  by (simp add: less_le_not_le)

lemma sum_le_zero[simp]: "(s::'lbl) ≤ 0 ⟷ s = 0"
  by (simp add: eq_iff)

lemma sum_le_zeroD[dest]: "(x::'lbl) ≤ 0 ⟹ x = 0"
  by simp

lemma foldr_plus_mono: "(n::'lbl) ≤ m ⟹ foldr (+) xs n ≤ foldr (+) xs m"
  by (induct xs) (auto simp: plus_mono)

lemma sum_weights_append:
  "sum_weights (ys @ xs) = sum_weights ys + sum_weights xs"
  by (induct ys) (auto simp: add.assoc)

lemma sum_summary_prepend_le: "sum_path_weights ys ≤ sum_path_weights xs ⟹ sum_path_weights (zs @ ys) ≤ sum_path_weights (zs @ xs)"
  by (induct zs arbitrary: xs ys) (auto intro: plus_mono)

lemma sum_summary_append_le: "sum_path_weights ys ≤ sum_path_weights xs ⟹ sum_path_weights (ys @ zs) ≤ sum_path_weights (xs @ zs)"
proof (induct zs arbitrary: xs ys)
  case (Cons a zs)
  then show ?case
    by (metis plus_mono map_append order_refl sum_weights_append)
qed simp

lemma foldr_plus_zero_le: "foldr (+) xs (0::'lbl) ≤ foldr (+) xs a"
  by (induct xs) (simp_all add: plus_mono)

lemma subseq_sum_weights_le:
  assumes "xs ≼ ys"
  shows "sum_weights xs ≤ sum_weights ys"
  using assms
proof (induct rule: list_emb.induct)
  case (list_emb_Nil ys)
  then show ?case by auto
next
  case (list_emb_Cons xs ys y)
  then show ?case by (auto elim!: order_trans simp: le_plus)
next
  case (list_emb_Cons2 x y xs ys)
  then show ?case by (auto elim!: order_trans simp: plus_mono)
qed

lemma subseq_sum_path_weights_le:
  "map LBL xs ≼ map LBL ys ⟹ sum_path_weights xs ≤ sum_path_weights ys"
  by (rule subseq_sum_weights_le)

lemma sum_path_weights_take_le[simp, intro]: "sum_path_weights (take i xs) ≤ sum_path_weights xs"
  by (auto intro!: subseq_sum_path_weights_le)

lemma sum_weights_append_singleton:
  "sum_weights (xs @ [x]) = sum_weights xs + x"
  by (induct xs) (simp_all add: add.assoc)

lemma sum_path_weights_append_singleton:
  "sum_path_weights (xs @ [(l,x,l')]) = sum_path_weights xs + x"
  by (induct xs) (simp_all add: add.assoc)

lemma path_weightp_ex_path:
  "path_weightp l1 l2 s ⟹ ∃xs.
  (let s' = sum_path_weights xs in s' ≤ s ∧ path_weightp l1 l2 s' ∧ distinct xs ∧
  (∀(l1,s,l2) ∈ set xs. s ∈⇩A weights l1 l2))"
  unfolding path_weightp_def
  apply (erule exE conjE)+
  apply (drule path_distinct)
  apply (erule exE conjE)+
  subgoal for xs xs'
    apply (rule exI[of _ xs'])
    apply (auto simp: Let_def dest!: path_edge intro: subseq_sum_path_weights_le)
    done
  done

lemma finite_set_summaries:
  "finite ((λ((l1,l2),s). (l1,s,l2)) ` (Sigma UNIV (λ(l1,l2). set_antichain (weights l1 l2))))"
  by force

lemma finite_summaries: "finite {xs. distinct xs ∧ (∀(l1, s, l2) ∈ set xs. s ∈⇩A weights l1 l2)}"
  apply (rule finite_subset[OF _ finite_distinct_bounded[of "((λ((l1,l2),s). (l1,s,l2)) ` (Sigma UNIV (λ(l1,l2). set_antichain (weights l1 l2))))"]])
   apply (force simp: finite_set_summaries)+
  done

lemma finite_minimal_antichain_path_weightp:
  "finite (minimal_antichain {x. path_weightp l1 l2 x})"
  apply (rule finite_surj[OF finite_summaries, where f = sum_path_weights])
  apply (clarsimp simp: minimal_antichain_def image_iff dest!: path_weightp_ex_path)
  apply (fastforce simp: Let_def)
  done

(* antichain of summaries along cycles-less paths (cycle-less = no edge repeated) *)
lift_definition path_weight :: "'vtx ⇒ 'vtx ⇒ 'lbl antichain"
  is "λl1 l2. minimal_antichain {x. path_weightp l1 l2 x}"
  using finite_minimal_antichain_path_weightp
  by auto

definition "reachable l1 l2 ≡ path_weight l1 l2 ≠ {}⇩A"

lemma in_path_weight: "s ∈⇩A path_weight loc1 loc2 ⟷ s ∈ minimal_antichain {s. path_weightp loc1 loc2 s}"
  by transfer simp

lemma path_weight_refl[simp]: "0 ∈⇩A path_weight loc loc"
proof -
  have *: "path loc loc []"
    by (simp add: path0)
  then have "0 = sum_path_weights []" by auto
  with * have "path_weightp loc loc 0"
    using path_weightp_def by blast
  then show ?thesis
    by (auto simp: in_path_weight in_minimal_antichain)
qed

lemma zero_in_minimal_antichain[simp]: "(0::'lbl) ∈ S ⟹ 0 ∈ minimal_antichain S"
  by (auto simp: in_minimal_antichain intro: sum_not_less_zero)

definition "path_weightp_distinct l1 l2 s ≡ (∃xs. distinct xs ∧ path l1 l2 xs ∧ s = sum_path_weights xs)"

lemma minimal_antichain_path_weightp_distinct:
  "minimal_antichain {xs. path_weightp l1 l2 xs} = minimal_antichain {xs. path_weightp_distinct l1 l2 xs}"
  unfolding path_weightp_def path_weightp_distinct_def minimal_antichain_def
  apply safe
     apply clarsimp
     apply (metis path_distinct order.strict_iff_order subseq_sum_path_weights_le)
    apply (blast+) [2]
  apply clarsimp
  apply (metis (no_types, lifting) le_less_trans path_distinct subseq_sum_weights_le)
  done

lemma finite_path_weightp_distinct[simp, intro]: "finite {xs. path_weightp_distinct l1 l2 xs}"
  unfolding path_weightp_distinct_def
  apply (rule finite_subset[where B = "sum_path_weights ` {xs. distinct xs ∧ path l1 l2 xs}"])
   apply clarsimp
  apply (rule finite_imageI)
  apply (rule finite_subset[OF _ finite_summaries])
  apply (clarsimp simp: path_edge)
  done

lemma path_weightp_distinct_nonempty:
  "{xs. path_weightp l1 l2 xs} ≠ {} ⟷ {xs. path_weightp_distinct l1 l2 xs} ≠ {}"
  by (auto dest: path_distinct simp: path_weightp_def path_weightp_distinct_def)

lemma path_weightp_distinct_member:
  "s ∈ {s. path_weightp l1 l2 s} ⟹ ∃u. u ∈ {s. path_weightp_distinct l1 l2 s} ∧ u ≤ s"
  apply (clarsimp simp: path_weightp_def path_weightp_distinct_def)
  apply (drule path_distinct)
  apply (auto dest: subseq_sum_path_weights_le)
  done

lemma minimal_antichain_path_weightp_member:
  "s ∈ {xs. path_weightp l1 l2 xs} ⟹ ∃u. u ∈ minimal_antichain {xs. path_weightp l1 l2 xs} ∧ u ≤ s"
proof -
  assume "s ∈ {xs. path_weightp l1 l2 xs}"
  then obtain u where u: "u ∈ {s. path_weightp_distinct l1 l2 s} ∧ u ≤ s"
    using path_weightp_distinct_member by blast
  have finite: "finite {xs. path_weightp_distinct l1 l2 xs}" ..
  from u finite obtain v where "v ∈ minimal_antichain {xs. path_weightp_distinct l1 l2 xs} ∧ v ≤ u"
    by atomize_elim (auto intro: minimal_antichain_member)
  with u show ?thesis
    by (auto simp: minimal_antichain_path_weightp_distinct)
qed

lemma path_path_weight: "path l1 l2 xs ⟹ ∃s. s ∈⇩A path_weight l1 l2 ∧ s ≤ sum_path_weights xs"
proof -
  assume "path l1 l2 xs"
  then have "sum_path_weights xs ∈ {x. path_weightp l1 l2 x}"
    by (auto simp: path_weightp_def)
  then obtain u where "u ∈ minimal_antichain {x. path_weightp l1 l2 x} ∧ u ≤ sum_path_weights xs"
    apply atomize_elim
    apply (drule minimal_antichain_path_weightp_member)
    apply auto
    done
  then show ?thesis
    by transfer auto
qed

lemma path_weight_conv_path:
  "s ∈⇩A path_weight l1 l2 ⟹ ∃xs. path l1 l2 xs ∧ s = sum_path_weights xs ∧ (∀ys. path l1 l2 ys ⟶ ¬ sum_path_weights ys < sum_path_weights xs)"
  by transfer (auto simp: in_minimal_antichain path_weightp_def)

abbreviation "optimal_path loc1 loc2 xs ≡ path loc1 loc2 xs ∧
   (∀ys. path loc1 loc2 ys ⟶ ¬ sum_path_weights ys < sum_path_weights xs)"

lemma path_weight_path: "s ∈⇩A path_weight loc1 loc2 ⟹
  (⋀xs. optimal_path loc1 loc2 xs ⟹ distinct xs ⟹ sum_path_weights xs = s ⟹ P) ⟹ P"
  apply atomize_elim
  apply transfer
  apply (clarsimp simp: in_minimal_antichain path_weightp_def)
  apply (drule path_distinct)
  apply (erule exE)
  subgoal for loc1 loc2 xs xs'
    apply (rule exI[of _ xs'])
    apply safe
    using order.strict_iff_order subseq_sum_path_weights_le apply metis
    using less_le subseq_sum_path_weights_le apply fastforce
    done
  done

lemma path_weight_elem_trans:
  "s ∈⇩A path_weight l1 l2 ⟹ s' ∈⇩A path_weight l2 l3 ⟹ ∃u. u ∈⇩A path_weight l1 l3 ∧ u ≤ s + s'"
proof -
  assume ps1: "s  ∈⇩A path_weight l1 l2"
  assume ps2: "s' ∈⇩A path_weight l2 l3"
  from ps1 obtain xs where path1: "path l1 l2 xs" "s = sum_path_weights xs"
    by (auto intro: path_weight_path)
  from ps2 obtain ys where path2: "path l2 l3 ys" "s' = sum_path_weights ys"
    by (auto intro: path_weight_path)
  from path1(1) path2(1) have "path l1 l3 (xs @ ys)"
    by (rule path_trans)
  with path1(2) path2(2) have "s + s' ∈ {s. path_weightp l1 l3 s}"
    by (auto simp: path_weightp_def sum_weights_append[symmetric])
  then show "∃u. u ∈⇩A path_weight l1 l3 ∧ u ≤ s + s'"
    by transfer (simp add: minimal_antichain_path_weightp_member)
qed

end

(*<*)
end
(*>*)