[STATEMENT]
lemma isShortestPath_alt: 
  "isShortestPath u p v \<longleftrightarrow> isSimplePath u p v \<and> length p = min_dist u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isShortestPath u p v = (isSimplePath u p v \<and> length p = min_dist u v)
[PROOF STEP]
using shortestPath_is_simple isShortestPath_min_dist_def
[PROOF STATE]
proof (prove)
using this:
isShortestPath ?s ?p ?t \<Longrightarrow> isSimplePath ?s ?p ?t
isShortestPath ?u ?p ?v = (isPath ?u ?p ?v \<and> length ?p = min_dist ?u ?v)

goal (1 subgoal):
 1. isShortestPath u p v = (isSimplePath u p v \<and> length p = min_dist u v)
[PROOF STEP]
unfolding isSimplePath_def
[PROOF STATE]
proof (prove)
using this:
isShortestPath ?s ?p ?t \<Longrightarrow> isPath ?s ?p ?t \<and> distinct (pathVertices ?s ?p)
isShortestPath ?u ?p ?v = (isPath ?u ?p ?v \<and> length ?p = min_dist ?u ?v)

goal (1 subgoal):
 1. isShortestPath u p v = ((isPath u p v \<and> distinct (pathVertices u p)) \<and> length p = min_dist u v)
[PROOF STEP]
by auto