Theory Dijkstra_Shortest_Path.Dijkstra_Misc

section ‹Miscellaneous Lemmas›
theory Dijkstra_Misc
imports Main
begin
  inductive_set least_map for f S where
    "⟦ x∈S; ∀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 "y∈S"
    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 "∀y∈S. 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: 
    "⟦ x∈least_map f S; f x ≤ f a ⟧ ⟹ x∈least_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