Theory Weight

header "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 *}

class weight = ordered_ab_semigroup_add + comm_monoid_add + linorder
begin

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
qed

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
qed

lemma add_nonneg_eq_0_iff:
  assumes x: "0 ≤ x" and y: "0 ≤ y"
  shows "x + y = 0 <-> x = 0 ∧ y = 0"
  by (metis add.comm_neutral add.left_neutral add_left_mono antisym x y)

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

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

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

end

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

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

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
  
end

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]: "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 (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: add_ac)
    apply (case_tac [!] c) [2]
    apply (simp_all add: add_ac add_right_mono)
    apply (case_tac "(x,y)" rule: less_eq_infty.cases)
    apply (simp_all add: linear)
    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"
  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
  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