[STATEMENT]
lemma fixes V W :: "'a vec set"
  shows
    card_le_dim_span:
    "V \<subseteq> carrier_vec n \<Longrightarrow> V \<subseteq> span W \<Longrightarrow> lin_indpt V \<Longrightarrow> card V \<le> dim_span W" and
    card_eq_dim_span_imp_same_span:
    "W \<subseteq> carrier_vec n \<Longrightarrow> V \<subseteq> span W \<Longrightarrow> lin_indpt V \<Longrightarrow> card V = dim_span W \<Longrightarrow> span V = span W" and
    same_span_imp_card_eq_dim_span:
    "V \<subseteq> carrier_vec n \<Longrightarrow> W \<subseteq> carrier_vec n \<Longrightarrow> span V = span W \<Longrightarrow> lin_indpt V \<Longrightarrow> card V = dim_span W" and
    dim_span_cong:
    "span V = span W \<Longrightarrow> dim_span V = dim_span W" and
    ex_basis_span:
    "V \<subseteq> carrier_vec n \<Longrightarrow> \<exists> W. W \<subseteq> carrier_vec n \<and> lin_indpt W \<and> span V = span W \<and> dim_span V = card W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W) &&& (\<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W)) &&& (\<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W) &&& (local.span V = local.span W \<Longrightarrow> dim_span V = dim_span W) &&& (V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. local.span V = local.span W \<Longrightarrow> dim_span V = dim_span W
 5. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
show cong: "\<And> V W. span V = span W \<Longrightarrow> dim_span V = dim_span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V W. local.span V = local.span W \<Longrightarrow> dim_span V = dim_span W
[PROOF STEP]
unfolding dim_span_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V W. local.span V = local.span W \<Longrightarrow> Max (card ` {Va. Va \<subseteq> carrier_vec n \<and> Va \<subseteq> local.span V \<and> lin_indpt Va}) = Max (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span ?V1 = local.span ?W1 \<Longrightarrow> dim_span ?V1 = dim_span ?W1

goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
local.span ?V1 = local.span ?W1 \<Longrightarrow> dim_span ?V1 = dim_span ?W1

goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
fix W :: "'a vec set"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
let ?M = "{V. V \<subseteq> carrier_vec n \<and> V \<subseteq> span W \<and> lin_indpt V}"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
have "card ` ?M \<subseteq> {0 .. n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<subseteq> {0..n}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<Longrightarrow> x \<in> {0..n}
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<Longrightarrow> x \<in> {0..n}
[PROOF STEP]
assume "k \<in> card ` ?M"
[PROOF STATE]
proof (state)
this:
k \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (1 subgoal):
 1. \<And>x. x \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<Longrightarrow> x \<in> {0..n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}
[PROOF STEP]
obtain V where V: "V \<subseteq> carrier_vec n \<and> V \<subseteq> span W \<and> lin_indpt V"
        and k: "k = card V"
[PROOF STATE]
proof (prove)
using this:
k \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (1 subgoal):
 1. (\<And>V. \<lbrakk>V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V; k = card V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V
k = card V

goal (1 subgoal):
 1. \<And>x. x \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<Longrightarrow> x \<in> {0..n}
[PROOF STEP]
from V
[PROOF STATE]
proof (chain)
picking this:
V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V
[PROOF STEP]
have "card V \<le> n"
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V

goal (1 subgoal):
 1. card V \<le> n
[PROOF STEP]
using dim_is_n li_le_dim
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V
local.dim = n
\<lbrakk>fin_dim; ?A \<subseteq> carrier_vec n; lin_indpt ?A\<rbrakk> \<Longrightarrow> finite ?A
\<lbrakk>fin_dim; ?A \<subseteq> carrier_vec n; lin_indpt ?A\<rbrakk> \<Longrightarrow> card ?A \<le> local.dim

goal (1 subgoal):
 1. card V \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card V \<le> n

goal (1 subgoal):
 1. \<And>x. x \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<Longrightarrow> x \<in> {0..n}
[PROOF STEP]
with k
[PROOF STATE]
proof (chain)
picking this:
k = card V
card V \<le> n
[PROOF STEP]
show "k \<in> {0 .. n}"
[PROOF STATE]
proof (prove)
using this:
k = card V
card V \<le> n

goal (1 subgoal):
 1. k \<in> {0..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> {0..n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<subseteq> {0..n}

goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
from finite_subset[OF this]
[PROOF STATE]
proof (chain)
picking this:
finite {0..n} \<Longrightarrow> finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V})
[PROOF STEP]
have fin: "finite (card ` ?M)"
[PROOF STATE]
proof (prove)
using this:
finite {0..n} \<Longrightarrow> finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V})

goal (1 subgoal):
 1. finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V})

goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
have "{} \<in> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<in> {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}
[PROOF STEP]
by (auto simp: span_empty span_zero)
[PROOF STATE]
proof (state)
this:
{} \<in> {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
from imageI[OF this, of card]
[PROOF STATE]
proof (chain)
picking this:
card {} \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}
[PROOF STEP]
have "0 \<in> card ` ?M"
[PROOF STATE]
proof (prove)
using this:
card {} \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (1 subgoal):
 1. 0 \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
hence Mempty: "card ` ?M \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
0 \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (1 subgoal):
 1. card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<noteq> {}

goal (4 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
 2. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 3. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 4. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
from Max_ge[OF fin, folded dim_span_def]
[PROOF STATE]
proof (chain)
picking this:
?x \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<Longrightarrow> ?x \<le> dim_span W
[PROOF STEP]
show "\<And> V :: 'a vec set. V \<subseteq> carrier_vec n \<Longrightarrow> V \<subseteq> span W \<Longrightarrow> lin_indpt V \<Longrightarrow> card V \<le> dim_span W"
[PROOF STATE]
proof (prove)
using this:
?x \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<Longrightarrow> ?x \<le> dim_span W

goal (1 subgoal):
 1. \<And>V. \<lbrakk>V \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V \<le> dim_span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?V1 \<subseteq> carrier_vec n; ?V1 \<subseteq> local.span W; lin_indpt ?V1\<rbrakk> \<Longrightarrow> card ?V1 \<le> dim_span W

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
note this fin Mempty
[PROOF STATE]
proof (state)
this:
\<lbrakk>?V1 \<subseteq> carrier_vec n; ?V1 \<subseteq> local.span W; lin_indpt ?V1\<rbrakk> \<Longrightarrow> card ?V1 \<le> dim_span W
finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V})
card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V} \<noteq> {}

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?V1 \<subseteq> carrier_vec n; ?V1 \<subseteq> local.span ?Wa4; lin_indpt ?V1\<rbrakk> \<Longrightarrow> card ?V1 \<le> dim_span ?Wa4
finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span ?Wa4 \<and> lin_indpt V})
card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span ?Wa4 \<and> lin_indpt V} \<noteq> {}

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
note part1 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?V1 \<subseteq> carrier_vec n; ?V1 \<subseteq> local.span ?Wa4; lin_indpt ?V1\<rbrakk> \<Longrightarrow> card ?V1 \<le> dim_span ?Wa4
finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span ?Wa4 \<and> lin_indpt V})
card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span ?Wa4 \<and> lin_indpt V} \<noteq> {}

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?V1 \<subseteq> carrier_vec n; ?V1 \<subseteq> local.span ?Wa4; lin_indpt ?V1\<rbrakk> \<Longrightarrow> card ?V1 \<le> dim_span ?Wa4
finite (card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span ?Wa4 \<and> lin_indpt V})
card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span ?Wa4 \<and> lin_indpt V} \<noteq> {}

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
fix V W :: "'a vec set"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
assume  W: "W \<subseteq> carrier_vec n"
      and VsW: "V \<subseteq> span W" and linV: "lin_indpt V" and card: "card V = dim_span W"
[PROOF STATE]
proof (state)
this:
W \<subseteq> carrier_vec n
V \<subseteq> local.span W
lin_indpt V
card V = dim_span W

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
from W VsW
[PROOF STATE]
proof (chain)
picking this:
W \<subseteq> carrier_vec n
V \<subseteq> local.span W
[PROOF STEP]
have V: "V \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
V \<subseteq> local.span W

goal (1 subgoal):
 1. V \<subseteq> carrier_vec n
[PROOF STEP]
using span_mem[OF W]
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
V \<subseteq> local.span W
?u \<in> W \<Longrightarrow> ?u \<in> local.span W

goal (1 subgoal):
 1. V \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<subseteq> carrier_vec n

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
from Max_in[OF part1(2,3), folded dim_span_def, of W]
[PROOF STATE]
proof (chain)
picking this:
dim_span W \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}
[PROOF STEP]
obtain WW where WW: "WW \<subseteq> carrier_vec n" "WW \<subseteq> span W" "lin_indpt WW"
      and id: "dim_span W = card WW"
[PROOF STATE]
proof (prove)
using this:
dim_span W \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (1 subgoal):
 1. (\<And>WW. \<lbrakk>WW \<subseteq> carrier_vec n; WW \<subseteq> local.span W; lin_indpt WW; dim_span W = card WW\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
WW \<subseteq> carrier_vec n
WW \<subseteq> local.span W
lin_indpt WW
dim_span W = card WW

goal (3 subgoals):
 1. \<lbrakk>W \<subseteq> carrier_vec n; V \<subseteq> local.span W; lin_indpt V; card V = dim_span W\<rbrakk> \<Longrightarrow> local.span V = local.span W
 2. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 3. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
show "span V = span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span V = local.span W
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
from VsW V W
[PROOF STATE]
proof (chain)
picking this:
V \<subseteq> local.span W
V \<subseteq> carrier_vec n
W \<subseteq> carrier_vec n
[PROOF STEP]
have sub: "span V \<subseteq> span W"
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> local.span W
V \<subseteq> carrier_vec n
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. local.span V \<subseteq> local.span W
[PROOF STEP]
using span_subsetI
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> local.span W
V \<subseteq> carrier_vec n
W \<subseteq> carrier_vec n
\<lbrakk>?ws \<subseteq> carrier_vec n; ?us \<subseteq> local.span ?ws\<rbrakk> \<Longrightarrow> local.span ?us \<subseteq> local.span ?ws

goal (1 subgoal):
 1. local.span V \<subseteq> local.span W
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
local.span V \<subseteq> local.span W

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
assume "span V \<noteq> span W"
[PROOF STATE]
proof (state)
this:
local.span V \<noteq> local.span W

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
with sub
[PROOF STATE]
proof (chain)
picking this:
local.span V \<subseteq> local.span W
local.span V \<noteq> local.span W
[PROOF STEP]
obtain w where wW: "w \<in> span W" and wsV: "w \<notin> span V"
[PROOF STATE]
proof (prove)
using this:
local.span V \<subseteq> local.span W
local.span V \<noteq> local.span W

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w \<in> local.span W; w \<notin> local.span V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> local.span W
w \<notin> local.span V

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
from wW W
[PROOF STATE]
proof (chain)
picking this:
w \<in> local.span W
W \<subseteq> carrier_vec n
[PROOF STEP]
have w: "w \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
w \<in> local.span W
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. w \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec n

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
from linV V
[PROOF STATE]
proof (chain)
picking this:
lin_indpt V
V \<subseteq> carrier_vec n
[PROOF STEP]
have finV: "finite V"
[PROOF STATE]
proof (prove)
using this:
lin_indpt V
V \<subseteq> carrier_vec n

goal (1 subgoal):
 1. finite V
[PROOF STEP]
using fin_dim fin_dim_li_fin
[PROOF STATE]
proof (prove)
using this:
lin_indpt V
V \<subseteq> carrier_vec n
fin_dim
\<lbrakk>fin_dim; lin_indpt ?A; ?A \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite V

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
from wsV span_mem[OF V, of w]
[PROOF STATE]
proof (chain)
picking this:
w \<notin> local.span V
w \<in> V \<Longrightarrow> w \<in> local.span V
[PROOF STEP]
have wV: "w \<notin> V"
[PROOF STATE]
proof (prove)
using this:
w \<notin> local.span V
w \<in> V \<Longrightarrow> w \<in> local.span V

goal (1 subgoal):
 1. w \<notin> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<notin> V

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
let ?X = "insert w V"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
have "card ?X = Suc (card V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert w V) = Suc (card V)
[PROOF STEP]
using wV finV
[PROOF STATE]
proof (prove)
using this:
w \<notin> V
finite V

goal (1 subgoal):
 1. card (insert w V) = Suc (card V)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (insert w V) = Suc (card V)

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
hence gt: "card ?X > dim_span W"
[PROOF STATE]
proof (prove)
using this:
card (insert w V) = Suc (card V)

goal (1 subgoal):
 1. dim_span W < card (insert w V)
[PROOF STEP]
unfolding card
[PROOF STATE]
proof (prove)
using this:
card (insert w V) = Suc (dim_span W)

goal (1 subgoal):
 1. dim_span W < card (insert w V)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_span W < card (insert w V)

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
have linX: "lin_indpt ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (insert w V)
[PROOF STEP]
using lin_dep_iff_in_span[OF V linV w wV] wsV
[PROOF STATE]
proof (prove)
using this:
(w \<in> local.span V) = lin_dep (V \<union> {w})
w \<notin> local.span V

goal (1 subgoal):
 1. lin_indpt (insert w V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt (insert w V)

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
have XW: "?X \<subseteq> span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert w V \<subseteq> local.span W
[PROOF STEP]
using wW VsW
[PROOF STATE]
proof (prove)
using this:
w \<in> local.span W
V \<subseteq> local.span W

goal (1 subgoal):
 1. insert w V \<subseteq> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert w V \<subseteq> local.span W

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
from part1(1)[OF _ XW linX] w V
[PROOF STATE]
proof (chain)
picking this:
insert w V \<subseteq> carrier_vec n \<Longrightarrow> card (insert w V) \<le> dim_span W
w \<in> carrier_vec n
V \<subseteq> carrier_vec n
[PROOF STEP]
have "card ?X \<le> dim_span W"
[PROOF STATE]
proof (prove)
using this:
insert w V \<subseteq> carrier_vec n \<Longrightarrow> card (insert w V) \<le> dim_span W
w \<in> carrier_vec n
V \<subseteq> carrier_vec n

goal (1 subgoal):
 1. card (insert w V) \<le> dim_span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (insert w V) \<le> dim_span W

goal (1 subgoal):
 1. local.span V \<noteq> local.span W \<Longrightarrow> False
[PROOF STEP]
with gt
[PROOF STATE]
proof (chain)
picking this:
dim_span W < card (insert w V)
card (insert w V) \<le> dim_span W
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
dim_span W < card (insert w V)
card (insert w V) \<le> dim_span W

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.span V = local.span W

goal (2 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 2. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?Wa3 \<subseteq> carrier_vec n; ?Va3 \<subseteq> local.span ?Wa3; lin_indpt ?Va3; card ?Va3 = dim_span ?Wa3\<rbrakk> \<Longrightarrow> local.span ?Va3 = local.span ?Wa3

goal (2 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 2. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
note card_dim_span = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?Wa3 \<subseteq> carrier_vec n; ?Va3 \<subseteq> local.span ?Wa3; lin_indpt ?Va3; card ?Va3 = dim_span ?Wa3\<rbrakk> \<Longrightarrow> local.span ?Va3 = local.span ?Wa3

goal (2 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 2. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?Wa3 \<subseteq> carrier_vec n; ?Va3 \<subseteq> local.span ?Wa3; lin_indpt ?Va3; card ?Va3 = dim_span ?Wa3\<rbrakk> \<Longrightarrow> local.span ?Va3 = local.span ?Wa3

goal (2 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 2. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
fix V :: "'a vec set"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 2. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
assume V: "V \<subseteq> carrier_vec n"
[PROOF STATE]
proof (state)
this:
V \<subseteq> carrier_vec n

goal (2 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 2. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
from Max_in[OF part1(2,3), folded dim_span_def, of V]
[PROOF STATE]
proof (chain)
picking this:
dim_span V \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span V \<and> lin_indpt V}
[PROOF STEP]
obtain W where W: "W \<subseteq> carrier_vec n" "W \<subseteq> span V" "lin_indpt W"
      and idW: "card W = dim_span V"
[PROOF STATE]
proof (prove)
using this:
dim_span V \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span V \<and> lin_indpt V}

goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<subseteq> carrier_vec n; W \<subseteq> local.span V; lin_indpt W; card W = dim_span V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W \<subseteq> carrier_vec n
W \<subseteq> local.span V
lin_indpt W
card W = dim_span V

goal (2 subgoals):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
 2. V \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
show "\<exists> W. W \<subseteq> carrier_vec n \<and> lin_indpt W \<and> span V = span W \<and> dim_span V = card W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W
[PROOF STEP]
proof (intro exI[of _ W] conjI W idW[symmetric])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span V = local.span W
[PROOF STEP]
from card_dim_span[OF V(1) W(2-3) idW]
[PROOF STATE]
proof (chain)
picking this:
local.span W = local.span V
[PROOF STEP]
show "span V = span W"
[PROOF STATE]
proof (prove)
using this:
local.span W = local.span V

goal (1 subgoal):
 1. local.span V = local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span V = local.span W

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span V = local.span W \<and> dim_span V = card W

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Va3 \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span ?Va3 = local.span W \<and> dim_span ?Va3 = card W

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?Va3 \<subseteq> carrier_vec n \<Longrightarrow> \<exists>W\<subseteq>carrier_vec n. lin_indpt W \<and> local.span ?Va3 = local.span W \<and> dim_span ?Va3 = card W

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
fix V W
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
assume V: "V \<subseteq> carrier_vec n"
      and W: "W \<subseteq> carrier_vec n"
      and span: "span V = span W"
      and lin: "lin_indpt V"
[PROOF STATE]
proof (state)
this:
V \<subseteq> carrier_vec n
W \<subseteq> carrier_vec n
local.span V = local.span W
lin_indpt V

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
from Max_in[OF part1(2,3), folded dim_span_def, of W]
[PROOF STATE]
proof (chain)
picking this:
dim_span W \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}
[PROOF STEP]
obtain WW where WW: "WW \<subseteq> carrier_vec n" "WW \<subseteq> span W" "lin_indpt WW"
      and idWW: "card WW = dim_span W"
[PROOF STATE]
proof (prove)
using this:
dim_span W \<in> card ` {V. V \<subseteq> carrier_vec n \<and> V \<subseteq> local.span W \<and> lin_indpt V}

goal (1 subgoal):
 1. (\<And>WW. \<lbrakk>WW \<subseteq> carrier_vec n; WW \<subseteq> local.span W; lin_indpt WW; card WW = dim_span W\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
WW \<subseteq> carrier_vec n
WW \<subseteq> local.span W
lin_indpt WW
card WW = dim_span W

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
from card_dim_span[OF W WW(2-3) idWW] span
[PROOF STATE]
proof (chain)
picking this:
local.span WW = local.span W
local.span V = local.span W
[PROOF STEP]
have spanWW: "span WW = span V"
[PROOF STATE]
proof (prove)
using this:
local.span WW = local.span W
local.span V = local.span W

goal (1 subgoal):
 1. local.span WW = local.span V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span WW = local.span V

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
from span
[PROOF STATE]
proof (chain)
picking this:
local.span V = local.span W
[PROOF STEP]
have "V \<subseteq> span W"
[PROOF STATE]
proof (prove)
using this:
local.span V = local.span W

goal (1 subgoal):
 1. V \<subseteq> local.span W
[PROOF STEP]
using span_mem[OF V]
[PROOF STATE]
proof (prove)
using this:
local.span V = local.span W
?u \<in> V \<Longrightarrow> ?u \<in> local.span V

goal (1 subgoal):
 1. V \<subseteq> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<subseteq> local.span W

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
from part1(1)[OF V this lin]
[PROOF STATE]
proof (chain)
picking this:
card V \<le> dim_span W
[PROOF STEP]
have VW: "card V \<le> dim_span W"
[PROOF STATE]
proof (prove)
using this:
card V \<le> dim_span W

goal (1 subgoal):
 1. card V \<le> dim_span W
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card V \<le> dim_span W

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
have finWW: "finite WW"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite WW
[PROOF STEP]
using WW
[PROOF STATE]
proof (prove)
using this:
WW \<subseteq> carrier_vec n
WW \<subseteq> local.span W
lin_indpt WW

goal (1 subgoal):
 1. finite WW
[PROOF STEP]
by (simp add: fin_dim_li_fin)
[PROOF STATE]
proof (state)
this:
finite WW

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
have finV: "finite V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite V
[PROOF STEP]
using lin V
[PROOF STATE]
proof (prove)
using this:
lin_indpt V
V \<subseteq> carrier_vec n

goal (1 subgoal):
 1. finite V
[PROOF STEP]
by (simp add: fin_dim_li_fin)
[PROOF STATE]
proof (state)
this:
finite V

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
from replacement[OF finWW finV V WW(3) WW(2)[folded span], unfolded idWW]
[PROOF STATE]
proof (chain)
picking this:
\<exists>C. finite C \<and> C \<subseteq> carrier_vec n \<and> C \<subseteq> local.span V \<and> C \<inter> WW = {} \<and> int (card C) \<le> int (card V) - int (dim_span W) \<and> local.span (WW \<union> C) = local.span V
[PROOF STEP]
obtain C :: "'a vec set"
      where le: "int (card C) \<le> int (card V) - int (dim_span W)"
[PROOF STATE]
proof (prove)
using this:
\<exists>C. finite C \<and> C \<subseteq> carrier_vec n \<and> C \<subseteq> local.span V \<and> C \<inter> WW = {} \<and> int (card C) \<le> int (card V) - int (dim_span W) \<and> local.span (WW \<union> C) = local.span V

goal (1 subgoal):
 1. (\<And>C. int (card C) \<le> int (card V) - int (dim_span W) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (card C) \<le> int (card V) - int (dim_span W)

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
from le
[PROOF STATE]
proof (chain)
picking this:
int (card C) \<le> int (card V) - int (dim_span W)
[PROOF STEP]
have "int (dim_span W) + int (card C) \<le> int (card V)"
[PROOF STATE]
proof (prove)
using this:
int (card C) \<le> int (card V) - int (dim_span W)

goal (1 subgoal):
 1. int (dim_span W) + int (card C) \<le> int (card V)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
int (dim_span W) + int (card C) \<le> int (card V)

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
hence "dim_span W + card C \<le> card V"
[PROOF STATE]
proof (prove)
using this:
int (dim_span W) + int (card C) \<le> int (card V)

goal (1 subgoal):
 1. dim_span W + card C \<le> card V
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
dim_span W + card C \<le> card V

goal (1 subgoal):
 1. \<lbrakk>V \<subseteq> carrier_vec n; W \<subseteq> carrier_vec n; local.span V = local.span W; lin_indpt V\<rbrakk> \<Longrightarrow> card V = dim_span W
[PROOF STEP]
with VW
[PROOF STATE]
proof (chain)
picking this:
card V \<le> dim_span W
dim_span W + card C \<le> card V
[PROOF STEP]
show "card V = dim_span W"
[PROOF STATE]
proof (prove)
using this:
card V \<le> dim_span W
dim_span W + card C \<le> card V

goal (1 subgoal):
 1. card V = dim_span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card V = dim_span W

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?Va3 \<subseteq> carrier_vec n; ?Wa3 \<subseteq> carrier_vec n; local.span ?Va3 = local.span ?Wa3; lin_indpt ?Va3\<rbrakk> \<Longrightarrow> card ?Va3 = dim_span ?Wa3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_span_le_n: assumes W: "W \<subseteq> carrier_vec n" shows "dim_span W \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_span W \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim_span W \<le> n
[PROOF STEP]
from ex_basis_span[OF W]
[PROOF STATE]
proof (chain)
picking this:
\<exists>Wa\<subseteq>carrier_vec n. lin_indpt Wa \<and> local.span W = local.span Wa \<and> dim_span W = card Wa
[PROOF STEP]
obtain V where
    V: "V \<subseteq> carrier_vec n"
    and lin: "lin_indpt V"
    and dim: "dim_span W = card V"
[PROOF STATE]
proof (prove)
using this:
\<exists>Wa\<subseteq>carrier_vec n. lin_indpt Wa \<and> local.span W = local.span Wa \<and> dim_span W = card Wa

goal (1 subgoal):
 1. (\<And>V. \<lbrakk>V \<subseteq> carrier_vec n; lin_indpt V; dim_span W = card V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<subseteq> carrier_vec n
lin_indpt V
dim_span W = card V

goal (1 subgoal):
 1. dim_span W \<le> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_span W \<le> n
[PROOF STEP]
unfolding dim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card V \<le> n
[PROOF STEP]
using lin V
[PROOF STATE]
proof (prove)
using this:
lin_indpt V
V \<subseteq> carrier_vec n

goal (1 subgoal):
 1. card V \<le> n
[PROOF STEP]
using dim_is_n li_le_dim
[PROOF STATE]
proof (prove)
using this:
lin_indpt V
V \<subseteq> carrier_vec n
local.dim = n
\<lbrakk>fin_dim; ?A \<subseteq> carrier_vec n; lin_indpt ?A\<rbrakk> \<Longrightarrow> finite ?A
\<lbrakk>fin_dim; ?A \<subseteq> carrier_vec n; lin_indpt ?A\<rbrakk> \<Longrightarrow> card ?A \<le> local.dim

goal (1 subgoal):
 1. card V \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_span W \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_span_insert: assumes W: "W \<subseteq> carrier_vec n"
  and v: "v \<in> carrier_vec n" and vs: "v \<notin> span W"
shows "dim_span (insert v W) = Suc (dim_span W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
from ex_basis_span[OF W]
[PROOF STATE]
proof (chain)
picking this:
\<exists>Wa\<subseteq>carrier_vec n. lin_indpt Wa \<and> local.span W = local.span Wa \<and> dim_span W = card Wa
[PROOF STEP]
obtain V where
    V: "V \<subseteq> carrier_vec n"
    and lin: "lin_indpt V"
    and span: "span W = span V"
    and dim: "dim_span W = card V"
[PROOF STATE]
proof (prove)
using this:
\<exists>Wa\<subseteq>carrier_vec n. lin_indpt Wa \<and> local.span W = local.span Wa \<and> dim_span W = card Wa

goal (1 subgoal):
 1. (\<And>V. \<lbrakk>V \<subseteq> carrier_vec n; lin_indpt V; local.span W = local.span V; dim_span W = card V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<subseteq> carrier_vec n
lin_indpt V
local.span W = local.span V
dim_span W = card V

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
from V vs[unfolded span]
[PROOF STATE]
proof (chain)
picking this:
V \<subseteq> carrier_vec n
v \<notin> local.span V
[PROOF STEP]
have vV: "v \<notin> V"
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> carrier_vec n
v \<notin> local.span V

goal (1 subgoal):
 1. v \<notin> V
[PROOF STEP]
using span_mem[OF V]
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> carrier_vec n
v \<notin> local.span V
?u \<in> V \<Longrightarrow> ?u \<in> local.span V

goal (1 subgoal):
 1. v \<notin> V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<notin> V

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
from lin_dep_iff_in_span[OF V lin v vV] vs span
[PROOF STATE]
proof (chain)
picking this:
(v \<in> local.span V) = lin_dep (V \<union> {v})
v \<notin> local.span W
local.span W = local.span V
[PROOF STEP]
have lin': "lin_indpt (insert v V)"
[PROOF STATE]
proof (prove)
using this:
(v \<in> local.span V) = lin_dep (V \<union> {v})
v \<notin> local.span W
local.span W = local.span V

goal (1 subgoal):
 1. lin_indpt (insert v V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt (insert v V)

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
have finV: "finite V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite V
[PROOF STEP]
using lin V
[PROOF STATE]
proof (prove)
using this:
lin_indpt V
V \<subseteq> carrier_vec n

goal (1 subgoal):
 1. finite V
[PROOF STEP]
using fin_dim fin_dim_li_fin
[PROOF STATE]
proof (prove)
using this:
lin_indpt V
V \<subseteq> carrier_vec n
fin_dim
\<lbrakk>fin_dim; lin_indpt ?A; ?A \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite V

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
have "card (insert v V) = Suc (card V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert v V) = Suc (card V)
[PROOF STEP]
using finV vV
[PROOF STATE]
proof (prove)
using this:
finite V
v \<notin> V

goal (1 subgoal):
 1. card (insert v V) = Suc (card V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (insert v V) = Suc (card V)

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
hence cvV: "card (insert v V) = Suc (dim_span W)"
[PROOF STATE]
proof (prove)
using this:
card (insert v V) = Suc (card V)

goal (1 subgoal):
 1. card (insert v V) = Suc (dim_span W)
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
card (insert v V) = Suc (card V)
dim_span W = card V

goal (1 subgoal):
 1. card (insert v V) = Suc (dim_span W)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (insert v V) = Suc (dim_span W)

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
have "span (insert v V) = span (insert v W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (insert v V) = local.span (insert v W)
[PROOF STEP]
using span V W v
[PROOF STATE]
proof (prove)
using this:
local.span W = local.span V
V \<subseteq> carrier_vec n
W \<subseteq> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. local.span (insert v V) = local.span (insert v W)
[PROOF STEP]
by (metis bot_least insert_subset insert_union span_union_is_sum)
[PROOF STATE]
proof (state)
this:
local.span (insert v V) = local.span (insert v W)

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
from same_span_imp_card_eq_dim_span[OF _ _ this lin'] cvV v V W
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>insert v V \<subseteq> carrier_vec n; insert v W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> card (insert v V) = dim_span (insert v W)
card (insert v V) = Suc (dim_span W)
v \<in> carrier_vec n
V \<subseteq> carrier_vec n
W \<subseteq> carrier_vec n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert v V \<subseteq> carrier_vec n; insert v W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> card (insert v V) = dim_span (insert v W)
card (insert v V) = Suc (dim_span W)
v \<in> carrier_vec n
V \<subseteq> carrier_vec n
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. dim_span (insert v W) = Suc (dim_span W)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_span (insert v W) = Suc (dim_span W)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gen_valid: "l(u) \<le> l(x) + length p" if "cf.isPath u p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l u \<le> l x + length p
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cf.isPath u p x

goal (1 subgoal):
 1. l u \<le> l x + length p
[PROOF STEP]
by (induction p arbitrary: u; fastforce dest: valid)


[STATEMENT]
theorem no_augmenting_path: "\<not>isAugmentingPath p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> isAugmentingPath p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isAugmentingPath p \<Longrightarrow> False
[PROOF STEP]
assume "isAugmentingPath p"
[PROOF STATE]
proof (state)
this:
isAugmentingPath p

goal (1 subgoal):
 1. isAugmentingPath p \<Longrightarrow> False
[PROOF STEP]
hence SP: "cf.isSimplePath s p t"
[PROOF STATE]
proof (prove)
using this:
isAugmentingPath p

goal (1 subgoal):
 1. cf.isSimplePath s p t
[PROOF STEP]
unfolding isAugmentingPath_def
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath s p t

goal (1 subgoal):
 1. cf.isSimplePath s p t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cf.isSimplePath s p t

goal (1 subgoal):
 1. isAugmentingPath p \<Longrightarrow> False
[PROOF STEP]
hence "cf.isPath s p t"
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath s p t

goal (1 subgoal):
 1. cf.isPath s p t
[PROOF STEP]
unfolding cf.isSimplePath_def
[PROOF STATE]
proof (prove)
using this:
cf.isPath s p t \<and> distinct (cf.pathVertices s p)

goal (1 subgoal):
 1. cf.isPath s p t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cf.isPath s p t

goal (1 subgoal):
 1. isAugmentingPath p \<Longrightarrow> False
[PROOF STEP]
from gen_valid[OF this]
[PROOF STATE]
proof (chain)
picking this:
l s \<le> l t + length p
[PROOF STEP]
have "length p \<ge> card V"
[PROOF STATE]
proof (prove)
using this:
l s \<le> l t + length p

goal (1 subgoal):
 1. card V \<le> length p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card V \<le> length p

goal (1 subgoal):
 1. isAugmentingPath p \<Longrightarrow> False
[PROOF STEP]
with cf.simplePath_length_less_V[OF _ SP]
[PROOF STATE]
proof (chain)
picking this:
s \<in> cf.V \<Longrightarrow> length p < card cf.V
card V \<le> length p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
s \<in> cf.V \<Longrightarrow> length p < card cf.V
card V \<le> length p

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma augment_edge_zero[simp]: "augment_edge f e 0 = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. augment_edge f e (0::'capacity) = f
[PROOF STEP]
unfolding augment_edge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case e of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) (0::'capacity) = f
[PROOF STEP]
by (auto split: prod.split)


[STATEMENT]
lemma augment_edge_same[simp]: "e\<in>E \<Longrightarrow> augment_edge f e \<Delta> e = f e + \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> augment_edge f e \<Delta> e = f e + \<Delta>
[PROOF STEP]
unfolding augment_edge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> (case e of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> e = f e + \<Delta>
[PROOF STEP]
by (auto split!: prod.splits)


[STATEMENT]
lemma augment_edge_other[simp]:"\<lbrakk>e\<in>E; e'\<noteq>e \<rbrakk> \<Longrightarrow> augment_edge f e \<Delta> e' = f e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<in> E; e' \<noteq> e\<rbrakk> \<Longrightarrow> augment_edge f e \<Delta> e' = f e'
[PROOF STEP]
unfolding augment_edge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<in> E; e' \<noteq> e\<rbrakk> \<Longrightarrow> (case e of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> e' = f e'
[PROOF STEP]
by (auto split!: prod.splits)


[STATEMENT]
lemma augment_edge_rev_same[simp]:
  "(v,u)\<in>E \<Longrightarrow> augment_edge f (u,v) \<Delta> (v,u) = f (v,u) - \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, u) \<in> E \<Longrightarrow> augment_edge f (u, v) \<Delta> (v, u) = f (v, u) - \<Delta>
[PROOF STEP]
using no_parallel_edge
[PROOF STATE]
proof (prove)
using this:
\<forall>u v. (u, v) \<in> E \<longrightarrow> (v, u) \<notin> E

goal (1 subgoal):
 1. (v, u) \<in> E \<Longrightarrow> augment_edge f (u, v) \<Delta> (v, u) = f (v, u) - \<Delta>
[PROOF STEP]
unfolding augment_edge_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u v. (u, v) \<in> E \<longrightarrow> (v, u) \<notin> E

goal (1 subgoal):
 1. (v, u) \<in> E \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> (v, u) = f (v, u) - \<Delta>
[PROOF STEP]
by (auto split!: prod.splits)


[STATEMENT]
lemma augment_edge_rev_other[simp]:
  "\<lbrakk>(u,v)\<notin>E; e'\<noteq>(v,u)\<rbrakk> \<Longrightarrow> augment_edge f (u,v) \<Delta> e' = f e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<notin> E; e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> augment_edge f (u, v) \<Delta> e' = f e'
[PROOF STEP]
unfolding augment_edge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<notin> E; e' \<noteq> (v, u)\<rbrakk> \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> e' = f e'
[PROOF STEP]
by (auto split!: prod.splits)


[STATEMENT]
lemma augment_edge_cf': "(u,v)\<in>cfE_of f \<Longrightarrow>
    cf_of (augment_edge f (u,v) \<Delta>)
  = (cf_of f)( (u,v) := cf_of f (u,v) - \<Delta>, (v,u) := cf_of f (v,u) + \<Delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> cfE_of f \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) = (cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u, v) \<in> cfE_of f \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) = (cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)
[PROOF STEP]
assume "(u,v)\<in>cfE_of f"
[PROOF STATE]
proof (state)
this:
(u, v) \<in> cfE_of f

goal (1 subgoal):
 1. (u, v) \<in> cfE_of f \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) = (cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)
[PROOF STEP]
hence "(u,v)\<in>E\<union>E\<inverse>"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cfE_of f

goal (1 subgoal):
 1. (u, v) \<in> E \<union> E\<inverse>
[PROOF STEP]
using cfE_of_ss_invE
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cfE_of f
cfE_of ?cf \<subseteq> E \<union> E\<inverse>

goal (1 subgoal):
 1. (u, v) \<in> E \<union> E\<inverse>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(u, v) \<in> E \<union> E\<inverse>

goal (1 subgoal):
 1. (u, v) \<in> cfE_of f \<Longrightarrow> cf_of (augment_edge f (u, v) \<Delta>) = (cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> E \<union> E\<inverse>

goal (1 subgoal):
 1. cf_of (augment_edge f (u, v) \<Delta>) = (cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cf_of (augment_edge f (u, v) \<Delta>) = (cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cf_of_augment_edge:
  assumes A: "(u,v)\<in>cfE_of f"
  shows "cf_of (augment_edge f (u,v) \<Delta>) = augment_edge_cf (cf_of f) (u,v) \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_of (augment_edge f (u, v) \<Delta>) = augment_edge_cf (cf_of f) (u, v) \<Delta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_of (augment_edge f (u, v) \<Delta>) = augment_edge_cf (cf_of f) (u, v) \<Delta>
[PROOF STEP]
show "cf_of (augment_edge f (u, v) \<Delta>) = augment_edge_cf (cf_of f) (u, v) \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_of (augment_edge f (u, v) \<Delta>) = augment_edge_cf (cf_of f) (u, v) \<Delta>
[PROOF STEP]
by (simp add: augment_edge_cf_def A augment_edge_cf')
[PROOF STATE]
proof (state)
this:
cf_of (augment_edge f (u, v) \<Delta>) = augment_edge_cf (cf_of f) (u, v) \<Delta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cfE_augment_ss:
  assumes EDGE: "(u,v)\<in>cfE_of f"
  shows "cfE_of (augment_edge f (u,v) \<Delta>) \<subseteq> insert (v,u) (cfE_of f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfE_of (augment_edge f (u, v) \<Delta>) \<subseteq> insert (v, u) (cfE_of f)
[PROOF STEP]
using EDGE
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cfE_of f

goal (1 subgoal):
 1. cfE_of (augment_edge f (u, v) \<Delta>) \<subseteq> insert (v, u) (cfE_of f)
[PROOF STEP]
apply (clarsimp simp: augment_edge_cf')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(u, v) \<in> cfE_of f; (a, b) \<in> Graph.E ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)); (a, b) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> a = v \<and> b = u
[PROOF STEP]
unfolding Graph.E_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(u, v) \<in> {(u, v). cf_of f (u, v) \<noteq> (0::'capacity)}; (a, b) \<in> {(ua, va). ((cf_of f)((u, v) := cf_of f (u, v) - \<Delta>, (v, u) := cf_of f (v, u) + \<Delta>)) (ua, va) \<noteq> (0::'capacity)}; (a, b) \<notin> {(u, v). cf_of f (u, v) \<noteq> (0::'capacity)}\<rbrakk> \<Longrightarrow> a = v \<and> b = u
[PROOF STEP]
apply (auto split: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done