Theory Dijkstra_Shortest_Path.Dijkstra_Misc

section ‹Miscellaneous Lemmas›
theory Dijkstra_Misc
imports Main
begin
  inductive_set least_map for f S where
    " xS; x'S. f x  f x'   x  least_map f S"

  lemma least_map_subset: "least_map f S  S"
    by (auto elim: least_map.cases)

  lemmas least_map_elemD = subsetD[OF least_map_subset]

  lemma least_map_leD:
    assumes "x  least_map f S"
    assumes "yS"
    shows "f x  f y"
    using assms
    by (auto elim: least_map.cases)

  lemma least_map_empty[simp]: "least_map f {} = {}"
    by (auto elim: least_map.cases)

  lemma least_map_singleton[simp]: "least_map (f::'a'b::order) {x} = {x}"
    by (auto elim: least_map.cases intro!: least_map.intros simp: refl)

  lemma least_map_insert_min:
    fixes f::"'a'b::order"
    assumes "yS. f x  f y"
    shows "x  least_map f (insert x S)"
    using assms by (auto intro: least_map.intros)

  lemma least_map_insert_nmin: 
    " xleast_map f S; f x  f a   xleast_map f (insert a S)"
    by (auto elim: least_map.cases intro: least_map.intros)


context semilattice_inf
begin
  lemmas [simp] = inf_absorb1 inf_absorb2

  lemma inf_absorb_less[simp]:
    "a < b  inf a b = a"
    "a < b  inf b a = a"
    apply (metis le_iff_inf less_imp_le)
    by (metis inf_commute le_iff_inf less_imp_le)
end







end