# Theory Weight

```section "Weights for Dijkstra's Algorithm"
theory Weight
imports Complex_Main
begin

text ‹
In this theory, we set up a type class for weights, and
a typeclass for weights with an infinity element. The latter
one is used internally in Dijkstra's algorithm.

Moreover, we provide a datatype that adds an infinity element to a given
base type.
›

subsection ‹Type Classes Setup›

begin

assumes "0 ≤ a" and "0 ≤ b" shows "0 ≤ a + b"
proof -
have "0 + 0 ≤ a + b"
then show ?thesis by simp
qed

assumes "a ≤ 0" and "b ≤ 0" shows "a + b ≤ 0"
proof -
have "a + b ≤ 0 + 0"
then show ?thesis by simp
qed

assumes x: "0 ≤ x" and y: "0 ≤ y"
shows "x + y = 0 ⟷ x = 0 ∧ y = 0"

lemma add_incr: "0≤b ⟹ a ≤ a+b"

lemma add_incr_left[simp, intro!]: "0≤b ⟹ a ≤ b + a"

lemma sum_not_less[simp, intro!]:
"0≤b ⟹ ¬ (a+b < a)"
"0≤a ⟹ ¬ (a+b < b)"
done

end

instance nat :: weight ..
instance int :: weight ..
instance rat :: weight ..
instance real :: weight ..

term top

class top_weight = order_top + weight +
assumes inf_add_right[simp]: "a + top = top"
begin

lemma inf_add_left[simp]: "top + a = top"

lemmas [simp] = top_unique less_top[symmetric]

lemma not_less_inf[simp]:
"¬ (a < top) ⟷ a=top"
by simp

end

text ‹
We provide a standard way to add an infinity element to any type.
›

datatype 'a infty = Infty | Num 'a

primrec val where "val (Num d) = d"

lemma num_val_iff[simp]: "e≠Infty ⟹ Num (val e) = e" by (cases e) auto

type_synonym NatB = "nat infty"

instantiation infty :: (weight) top_weight
begin
definition "(0::'a infty) == Num 0"
definition "top ≡ Infty"

fun less_eq_infty where
"less_eq Infty (Num _) ⟷ False" |
"less_eq _ Infty ⟷ True" |
"less_eq (Num a) (Num b) ⟷ a≤b"

lemma [simp]: "Infty≤a ⟷ a=Infty"
by (cases a) auto

fun less_infty where
"less Infty _ ⟷ False" |
"less (Num _) Infty ⟷ True" |
"less (Num a) (Num b) ⟷ a<b"

lemma [simp]: "less a Infty ⟷ a ≠ Infty"
by (cases a) auto

fun plus_infty where
"plus _ Infty = Infty" |
"plus Infty _ = Infty" |
"plus (Num a) (Num b) = Num (a+b)"

lemma [simp]: "plus Infty a = Infty" by (cases a) simp_all

instance
apply (intro_classes)
apply (case_tac [!] x) [4]
apply simp_all
apply (case_tac [!] y) [3]
apply (case_tac z)
apply (case_tac [!] a) [4]
apply simp_all
apply (case_tac [!] b) [3]
apply (case_tac [!] c) [2]
apply (case_tac "(x,y)" rule: less_eq_infty.cases)
done
end

subsubsection ‹Unboxing›

text ‹Conversion between the constants defined by the
typeclass, and the concrete functions on the @{typ "'a infty"} type.
›
lemma infty_inf_unbox:
"Num a ≠ top"
"top ≠ Num a"
"Infty = top"

lemma infty_ord_unbox:
"Num a ≤ Num b ⟷ a ≤ b"
"Num a < Num b ⟷ a < b"
by auto

lemma infty_plus_unbox:
"Num a + Num b = Num (a+b)"
by (auto)

lemma infty_zero_unbox:
"Num a = 0 ⟷ a = 0"
"Num 0 = 0"
by (auto simp: zero_infty_def)

lemmas infty_unbox =
infty_inf_unbox infty_zero_unbox infty_ord_unbox infty_plus_unbox

lemma inf_not_zero[simp]:
"top≠(0::_ infty)" "(0::_ infty)≠top"
apply (unfold zero_infty_def top_infty_def)
apply auto
done

lemma num_val_iff'[simp]: "e≠top ⟹ Num (val e) = e"
by (cases e) (auto simp add: infty_unbox)

lemma infty_neE:
"⟦a≠Infty; ⋀d. a=Num d ⟹ P⟧ ⟹ P"
"⟦a≠top; ⋀d. a=Num d ⟹ P⟧ ⟹ P"
by (case_tac [!] a) (auto simp add: infty_unbox)

end
```