Theory Weight

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

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›

class weight = ordered_ab_semigroup_add + comm_monoid_add + linorder

lemma add_nonneg_nonneg [simp]:
  assumes "0  a" and "0  b" shows "0  a + b"
proof -
  have "0 + 0  a + b" 
    using assms by (rule add_mono)
  then show ?thesis by simp

lemma add_nonpos_nonpos[simp]:
  assumes "a  0" and "b  0" shows "a + b  0"
proof -
  have "a + b  0 + 0"
    using assms by (rule add_mono)
  then show ?thesis by simp

lemma add_nonneg_eq_0_iff:
  assumes x: "0  x" and y: "0  y"
  shows "x + y = 0  x = 0  y = 0"
  by (metis local.add_0_left local.add_0_right local.add_left_mono local.antisym_conv x y)

lemma add_incr: "0b  a  a+b"
  by (metis add.comm_neutral add_left_mono)

lemma add_incr_left[simp, intro!]: "0b  a  b + a"
  by (metis add_incr add.commute)

lemma sum_not_less[simp, intro!]: 
  "0b  ¬ (a+b < a)"
  "0a  ¬ (a+b < b)"
  apply (metis add_incr less_le_not_le)
  apply (metis add_incr_left less_le_not_le)


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"

lemma inf_add_left[simp]: "top + a = top"
  by (metis add.commute inf_add_right)

lemmas [simp] = top_unique less_top[symmetric]
lemma not_less_inf[simp]:
  "¬ (a < top)  a=top"
  by simp

subsection ‹Adding Infinity›
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]: "eInfty  Num (val e) = e" by (cases e) auto

type_synonym NatB = "nat infty"

instantiation infty :: (weight) top_weight
  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)  ab"

  lemma [simp]: "Inftya  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

    apply (intro_classes)
    apply (case_tac [!] x) [4]
    apply simp_all
    apply (case_tac [!] y) [3]
    apply (simp_all add: less_le_not_le)
    apply (case_tac z)
    apply (simp_all add: top_infty_def zero_infty_def)
    apply (case_tac [!] a) [4]
    apply simp_all
    apply (case_tac [!] b) [3]
    apply (simp_all add: ac_simps)
    apply (case_tac [!] c) [2]
    apply (simp_all add: ac_simps add_right_mono)
    apply (case_tac "(x,y)" rule: less_eq_infty.cases)
    apply (simp_all add: linear)

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"
  by (auto simp add: top_infty_def)

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

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

lemma infty_neE: 
  "aInfty; d. a=Num d  P  P"
  "atop; d. a=Num d  P  P"
  by (case_tac [!] a) (auto simp add: infty_unbox)