[STATEMENT]
theorem (in v0_v1_Digraph) menger_trivial:
  assumes "DisjointPaths G v0 v1 paths" "card paths = n"
  shows "\<And>S. Separation G v0 v1 S \<Longrightarrow> card S \<ge> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
interpret DisjointPaths G v0 v1 paths
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DisjointPaths G v0 v1 paths
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
DisjointPaths G v0 v1 paths

goal (1 subgoal):
 1. DisjointPaths G v0 v1 paths
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
assume "Separation G v0 v1 S"
[PROOF STATE]
proof (state)
this:
Separation G v0 v1 S

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Separation G v0 v1 S
[PROOF STEP]
interpret S: Separation G v0 v1 S
[PROOF STATE]
proof (prove)
using this:
Separation G v0 v1 S

goal (1 subgoal):
 1. Separation G v0 v1 S
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
text \<open>
    Our plan is to show @{term "card S \<ge> n"} by defining an injective function from @{term paths}
    into @{term S}.  Because we have @{term "card paths = n"}, the result follows.

    For the injective function, we simply use the observation stated above: Every path needs to
    be separated by @{term S} at some vertex, so we can choose such a vertex.
\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
define f where "f \<equiv> \<lambda>xs. SOME v. v \<in> S \<and> v \<in> set xs"
[PROOF STATE]
proof (state)
this:
f \<equiv> \<lambda>xs. SOME v. v \<in> S \<and> v \<in> set xs

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
have f_good: "\<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
assume "xs \<in> paths"
[PROOF STATE]
proof (state)
this:
xs \<in> paths

goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> paths
[PROOF STEP]
obtain v where "v \<in> set xs \<inter> S"
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths

goal (1 subgoal):
 1. (\<And>v. v \<in> set xs \<inter> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using S.S_separates paths
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths
v0 \<leadsto>?xs\<leadsto> v1 \<Longrightarrow> set ?xs \<inter> S \<noteq> {}
?xs \<in> paths \<Longrightarrow> v0 \<leadsto>?xs\<leadsto> v1

goal (1 subgoal):
 1. (\<And>v. v \<in> set xs \<inter> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
v \<in> set xs \<inter> S

goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set xs \<inter> S
[PROOF STEP]
show "f xs \<in> S \<and> f xs \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
v \<in> set xs \<inter> S

goal (1 subgoal):
 1. f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
v \<in> set xs \<inter> S

goal (1 subgoal):
 1. (SOME v. v \<in> S \<and> v \<in> set xs) \<in> S \<and> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> set xs
[PROOF STEP]
using someI[of "\<lambda>v. v \<in> S \<and> v \<in> set xs" v]
[PROOF STATE]
proof (prove)
using this:
v \<in> set xs \<inter> S
v \<in> S \<and> v \<in> set xs \<Longrightarrow> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> S \<and> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> set xs

goal (1 subgoal):
 1. (SOME v. v \<in> S \<and> v \<in> set xs) \<in> S \<and> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> set xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f xs \<in> S \<and> f xs \<in> set xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
text \<open>This @{term f} is injective because no two paths intersect in the same vertex.\<close>
[PROOF STATE]
proof (state)
this:
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
have "inj_on f paths"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f paths
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix xs ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume *: "xs \<in> paths" "ys \<in> paths" "f xs = f ys"
[PROOF STATE]
proof (state)
this:
xs \<in> paths
ys \<in> paths
f xs = f ys

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> paths
ys \<in> paths
f xs = f ys
[PROOF STEP]
obtain v where "v \<in> S" "v \<in> set xs" "v \<in> set ys"
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths
ys \<in> paths
f xs = f ys

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> S; v \<in> set xs; v \<in> set ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f_good
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths
ys \<in> paths
f xs = f ys
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> S; v \<in> set xs; v \<in> set ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
v \<in> S
v \<in> set xs
v \<in> set ys

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> S
v \<in> set xs
v \<in> set ys
[PROOF STEP]
show "xs = ys"
[PROOF STATE]
proof (prove)
using this:
v \<in> S
v \<in> set xs
v \<in> set ys

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
using *(1,2) paths_disjoint S.v0_notin_S S.v1_notin_S
[PROOF STATE]
proof (prove)
using this:
v \<in> S
v \<in> set xs
v \<in> set ys
xs \<in> paths
ys \<in> paths
\<lbrakk>?xs \<in> paths; ?ys \<in> paths; ?xs \<noteq> ?ys; ?v \<in> set ?xs; ?v \<in> set ?ys\<rbrakk> \<Longrightarrow> ?v = v0 \<or> ?v = v1
v0 \<notin> S
v1 \<notin> S

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs = ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on f paths

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on f paths
[PROOF STEP]
show "card S \<ge> n"
[PROOF STATE]
proof (prove)
using this:
inj_on f paths

goal (1 subgoal):
 1. n \<le> card S
[PROOF STEP]
using assms(2) f_good
[PROOF STATE]
proof (prove)
using this:
inj_on f paths
card paths = n
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. n \<le> card S
[PROOF STEP]
by (metis S.finite_S finite_paths image_subsetI inj_on_iff_card_le)
[PROOF STATE]
proof (state)
this:
n \<le> card S

goal:
No subgoals!
[PROOF STEP]
qed