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)"
      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