header {* \isaheader{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)"
by(simp_all add:intra_path_def)
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)"
by(simp_all add:intra_path_def)
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