# Theory Distance

```section ‹Distance of Paths›

theory Distance imports CFG begin

context CFG begin

inductive distance :: "'node ⇒ 'node ⇒ nat ⇒ bool"
where distanceI:
"⟦n -as→⇩ι* n'; length as = x; ∀as'. n -as'→⇩ι* n' ⟶ x ≤ length as'⟧
⟹ distance n n' x"

lemma every_path_distance:
assumes "n -as→⇩ι* n'"
obtains x where "distance n n' x" and "x ≤ length as"
proof(atomize_elim)
show "∃x. distance n n' x ∧ x ≤ length as"
proof(cases "∃as'. n -as'→⇩ι* n' ∧
(∀asx. n -asx→⇩ι* n' ⟶ length as' ≤ length asx)")
case True
then obtain as'
where "n -as'→⇩ι* n' ∧ (∀asx. n -asx→⇩ι* n' ⟶ length as' ≤ length asx)"
by blast
hence "n -as'→⇩ι* n'" and all:"∀asx. n -asx→⇩ι* n' ⟶ length as' ≤ length asx"
by simp_all
hence "distance n n' (length as')" by(fastforce intro:distanceI)
from ‹n -as→⇩ι* n'› all have "length as' ≤ length as" by fastforce
with ‹distance n n' (length as')› show ?thesis by blast
next
case False
hence all:"∀as'. n -as'→⇩ι* n' ⟶ (∃asx. n -asx→⇩ι* n' ∧ length as' > length asx)"
by fastforce
have "wf (measure length)" by simp
from ‹n -as→⇩ι* n'› have "as ∈ {as. n -as→⇩ι* n'}" by simp
with ‹wf (measure length)› obtain as' where "as' ∈ {as. n -as→⇩ι* n'}"
and notin:"⋀as''. (as'',as') ∈ (measure length) ⟹ as'' ∉ {as. n -as→⇩ι* n'}"
by(erule wfE_min)
from ‹as' ∈ {as. n -as→⇩ι* n'}› have "n -as'→⇩ι* n'" by simp
with all obtain asx where "n -asx→⇩ι* n'"
and "length as' > length asx"
by blast
with notin have  "asx ∉ {as. n -as→⇩ι* n'}" by simp
hence "¬ n -asx→⇩ι* n'" by simp
with ‹n -asx→⇩ι* n'› have False by simp
thus ?thesis by simp
qed
qed

lemma distance_det:
"⟦distance n n' x; distance n n' x'⟧ ⟹ x = x'"
apply(erule distance.cases)+ apply clarsimp
apply(erule_tac x="asa" in allE) apply(erule_tac x="as" in allE)
by simp

lemma only_one_SOME_dist_edge:
assumes "valid_edge a" and "intra_kind(kind a)" and "distance (targetnode a) n' x"
shows "∃!a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') n' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
proof(rule ex_ex1I)
show "∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
proof -
have "(∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)) =
(∃nx. ∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') n' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧ targetnode a' = nx)"
apply(unfold some_eq_ex[of "λnx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx"])
by simp
also have "…"
using ‹valid_edge a› ‹intra_kind(kind a)› ‹distance (targetnode a) n' x›
by blast
finally show ?thesis .
qed
next
fix a' ax
assume "sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
and "sourcenode a = sourcenode ax ∧
distance (targetnode ax) n' x ∧ valid_edge ax ∧ intra_kind(kind ax) ∧
targetnode ax = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
thus "a' = ax" by(fastforce intro!:edge_det)
qed

lemma distance_successor_distance:
assumes "distance n n' x" and "x ≠ 0"
obtains a where "valid_edge a" and "n = sourcenode a" and "intra_kind(kind a)"
and "distance (targetnode a) n' (x - 1)"
and "targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
proof(atomize_elim)
show "∃a. valid_edge a ∧ n = sourcenode a ∧ intra_kind(kind a) ∧
distance (targetnode a) n' (x - 1) ∧
targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
proof(rule ccontr)
assume "¬ (∃a. valid_edge a ∧ n = sourcenode a ∧ intra_kind(kind a) ∧
distance (targetnode a) n' (x - 1) ∧
targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx))"
hence imp:"∀a. valid_edge a ∧ n = sourcenode a ∧ intra_kind(kind a) ∧
targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)
⟶ ¬ distance (targetnode a) n' (x - 1)" by blast
from ‹distance n n' x› obtain as where "n -as→⇩ι* n'" and "x = length as"
and all:"∀as'. n -as'→⇩ι* n' ⟶ x ≤ length as'"
by(auto elim:distance.cases)
from ‹n -as→⇩ι* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)"
from this ‹x = length as› all imp show False
proof(induct rule:path.induct)
case (empty_path n)
from ‹x = length []› ‹x ≠ 0› show False by simp
next
case (Cons_path n'' as n' a n)
note imp = ‹∀a. valid_edge a ∧ n = sourcenode a ∧ intra_kind (kind a) ∧
targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)
⟶ ¬ distance (targetnode a) n' (x - 1)›
note all = ‹∀as'. n -as'→⇩ι* n' ⟶ x ≤ length as'›
from ‹∀a∈set (a#as). intra_kind (kind a)›
have "intra_kind (kind a)" and "∀a∈set as. intra_kind (kind a)"
by simp_all
from ‹n'' -as→* n'› ‹∀a∈set as. intra_kind (kind a)›
have "n'' -as→⇩ι* n'" by(simp add:intra_path_def)
then obtain y where "distance n'' n' y"
and "y ≤ length as" by(erule every_path_distance)
from ‹distance n'' n' y› obtain as' where "n'' -as'→⇩ι* n'"
and "y = length as'" by(auto elim:distance.cases)
hence "n'' -as'→* n'" and "∀a∈set as'. intra_kind (kind a)"
show False
proof(cases "y < length as")
case True
from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹n'' -as'→* n'›
have "n -a#as'→* n'" by -(rule path.Cons_path)
with ‹∀a∈set as'. intra_kind (kind a)› ‹intra_kind (kind a)›
have "n -a#as'→⇩ι* n'" by(simp add:intra_path_def)
with all have "x ≤ length (a#as')" by blast
with ‹x = length (a#as)› True ‹y = length as'› show False by simp
next
case False
with ‹y ≤ length as› ‹x = length (a#as)› have "y = x - 1" by simp
from ‹targetnode a = n''› ‹distance n'' n' y›
have "distance (targetnode a) n' y" by simp
with ‹valid_edge a› ‹intra_kind(kind a)›
obtain a' where "sourcenode a = sourcenode a'"
and "distance (targetnode a') n' y" and "valid_edge a'"
and "intra_kind(kind a')"
and "targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' y ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
by(auto dest:only_one_SOME_dist_edge)
with imp ‹sourcenode a = n› ‹y = x - 1› show False by fastforce
qed
qed
qed
qed

end

end
```