Theory Code_Word_Dist

(*
  Author: Maximilian Spitz
*)


section ‹A Generalised Distance Measure›

theory Code_Word_Dist
  imports Encoding_Nat
begin

text ‹
In the case of the reflected binary code (RBC) it is sufficient
  to use the Hamming distance to express the property, because there are
  only two distinct digits so that one bitflip naturally always corresponds
  to a distance of 1.
›


subsection ‹Distance of Digits›

text ‹
We can interpret a bitflip as an increment modulo 2, which is why for the
  distance of digits it appears as a natural generalisation to choose the
  amount of required increments.
Mathematically, the distance $d(x,y)$ should be $y-x$ (mod $b$).
For example we have $d(0,1) = d(1,0) = 1$ in the binary numeral system.
›

definition dist1 :: "base ⇒ nat ⇒ nat ⇒ nat" where
  "dist1 b x y ≡ if x≤y then y-x else b+y-x"

text ‹
Note that the distance of digits is in general asymmetric, so that it is
  in paticular not a metric. However, this is not an issue and in fact the
  most appropriate generalisation, partly due to the next lemma:
›

lemma dist1_eq:
  "⟦x < b; y < b; dist1 b x y = 0⟧ ⟹ x = y"
  by (auto simp add: dist1_def split: if_splits)

lemma dist1_0:
  "dist1 b x x = 0"
  by (auto simp add: dist1_def)

lemma dist1_ge1:
  "⟦x < b; y < b; x≠y⟧ ⟹ dist1 b x y ≥ 1"
  using dist1_eq by fastforce

lemma dist1_elim_1:
  "⟦x < b; y < b⟧ ⟹ (dist1 b x y + x) mod b = y"
  by (auto simp add: dist1_def)

lemma dist1_elim_2:
  "⟦x < b; y < b⟧ ⟹ dist1 b x (x+y) = y"
  by (auto simp add: dist1_def)

lemma dist1_mod_Suc:
  "⟦x < b; y < b⟧ ⟹ dist1 b x (Suc y mod b) = Suc (dist1 b x y) mod b"
  by (auto simp add: dist1_def mod_Suc)

lemma dist1_Suc:
  "⟦2 ≤ b; x < b⟧ ⟹ dist1 b x (Suc x mod b) = 1"
  by (simp add: dist1_0 dist1_mod_Suc)

lemma dist1_asym:
  "⟦x < b; y < b⟧ ⟹ (dist1 b x y + dist1 b y x) mod b = 0"
  by (auto simp add: dist1_def)

lemma dist1_valid:
  "⟦x < b; y < b⟧ ⟹ dist1 b x y < b"
  by (auto simp add: dist1_def)

(* linarith_split_limit exceeded *)
lemma dist1_distr:
  "⟦x < b; y < b; z < b⟧ ⟹ dist1 b (dist1 b x y) (dist1 b x z) = dist1 b y z"
  by (auto simp add: dist1_def)

lemma dist1_distr2:
  "⟦x < b; y < b; z < b⟧ ⟹ dist1 b (dist1 b x z) (dist1 b y z) = dist1 b y x"
  by (auto simp add: dist1_def)


subsection ‹(Hamming-) Distance between Words›

text ‹
The total distance between two words of equal length is then defined as
  the sum of component-wise distances.
Note that the Hamming distance is equivalent to this definition for $b=2$
  and is in general a lower bound.
›

fun hamming :: "word ⇒ word ⇒ nat" where
  "hamming [] [] = 0"
| "hamming (a#v) (b#w) = (if a≠b then 1 else 0) + hamming v w"

text ‹
The Hamming distance is only defined in the case of equal word length.
In the following definition of a distance we assume leading zeroes
  if the word length is not equal:
›

fun dist :: "base ⇒ word ⇒ word ⇒ nat" where
  "dist _ [] [] = 0"
| "dist b (x#xs) [] = dist1 b x 0 + dist b xs []"
| "dist b [] (y#ys) = dist1 b 0 y + dist b [] ys"
| "dist b (x#xs) (y#ys) = dist1 b x y + dist b xs ys"

lemma dist_0:
  "dist b w w = 0"
  apply (induction w)
  by (auto simp add: dist1_0)

lemma dist_eq:
  "⟦valid b v; valid b w; length v=length w; dist b v w = 0⟧ ⟹ v = w"
  apply (induction b v w rule: dist.induct)
  by (auto simp add: dist1_eq)

lemma dist_posd:
  "⟦valid b v; valid b w; length v=length w⟧ ⟹ (dist b v w = 0) = (v = w)"
  using dist_0 dist_eq by auto

lemma hamming_posd:
  "length v=length w ⟹ (hamming v w = 0) = (v = w)"
  by (induction v w rule: hamming.induct) auto

lemma hamming_symm:
  "length v=length w ⟹ hamming v w = hamming w v"
  by (induction v w rule: hamming.induct) auto

theorem hamming_dist:
  "⟦valid b v; valid b w; length v=length w⟧ ⟹ hamming v w ≤ dist b v w"
  apply (induction b v w rule: dist.induct)
     apply auto
  using dist1_ge1 by fastforce

end