# Theory 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
```