[STATEMENT]
lemma matroid_subset [simp, intro]:
  assumes "\<E> \<subseteq> carrier"
  shows "matroid \<E> (indep_in \<E>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matroid \<E> (indep_in \<E>)
[PROOF STEP]
unfolding matroid_def matroid_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_system \<E> (indep_in \<E>) \<and> (\<forall>X Y. indep_in \<E> X \<longrightarrow> indep_in \<E> Y \<longrightarrow> card X = Suc (card Y) \<longrightarrow> (\<exists>x\<in>X - Y. indep_in \<E> (insert x Y)))
[PROOF STEP]
proof (safe, goal_cases indep_system augment)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. indep_system \<E> (indep_in \<E>)
 2. \<And>X Y. \<lbrakk>indep_in \<E> X; indep_in \<E> Y; card X = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X - Y. indep_in \<E> (insert x Y)
[PROOF STEP]
case indep_system
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. indep_system \<E> (indep_in \<E>)
 2. \<And>X Y. \<lbrakk>indep_in \<E> X; indep_in \<E> Y; card X = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X - Y. indep_in \<E> (insert x Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_system \<E> (indep_in \<E>)
[PROOF STEP]
using indep_system_subset[OF assms]
[PROOF STATE]
proof (prove)
using this:
indep_system \<E> (indep_in \<E>)

goal (1 subgoal):
 1. indep_system \<E> (indep_in \<E>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
indep_system \<E> (indep_in \<E>)

goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>indep_in \<E> X; indep_in \<E> Y; card X = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X - Y. indep_in \<E> (insert x Y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>indep_in \<E> X; indep_in \<E> Y; card X = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X - Y. indep_in \<E> (insert x Y)
[PROOF STEP]
case (augment X Y)
[PROOF STATE]
proof (state)
this:
indep_in \<E> X
indep_in \<E> Y
card X = Suc (card Y)

goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>indep_in \<E> X; indep_in \<E> Y; card X = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X - Y. indep_in \<E> (insert x Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in \<E> X
indep_in \<E> Y
card X = Suc (card Y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
indep_in \<E> X
indep_in \<E> Y
card X = Suc (card Y)

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep_in \<E> (insert x Y)
[PROOF STEP]
using augment_aux[of X Y]
[PROOF STATE]
proof (prove)
using this:
indep_in \<E> X
indep_in \<E> Y
card X = Suc (card Y)
\<lbrakk>indep X; indep Y; card X = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X - Y. indep (insert x Y)

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep_in \<E> (insert x Y)
[PROOF STEP]
unfolding indep_in_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E> \<and> indep X
Y \<subseteq> \<E> \<and> indep Y
card X = Suc (card Y)
\<lbrakk>indep X; indep Y; card X = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X - Y. indep (insert x Y)

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. insert x Y \<subseteq> \<E> \<and> indep (insert x Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>X - Y. indep_in \<E> (insert x Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_card:
  assumes "basis B\<^sub>1"
  assumes "basis B\<^sub>2"
  shows "card B\<^sub>1 = card B\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card B\<^sub>1 = card B\<^sub>2
[PROOF STEP]
proof (rule ccontr, goal_cases False)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
card B\<^sub>1 \<noteq> card B\<^sub>2

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card B\<^sub>1 \<noteq> card B\<^sub>2
[PROOF STEP]
have "card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
card B\<^sub>1 \<noteq> card B\<^sub>2

goal (1 subgoal):
 1. card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
fix B\<^sub>1 B\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
assume "basis B\<^sub>1" "basis B\<^sub>2" "card B\<^sub>1 < card B\<^sub>2"
[PROOF STATE]
proof (state)
this:
basis B\<^sub>1
basis B\<^sub>2
card B\<^sub>1 < card B\<^sub>2

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis B\<^sub>1
basis B\<^sub>2
card B\<^sub>1 < card B\<^sub>2
[PROOF STEP]
obtain x where "x \<in> B\<^sub>2 - B\<^sub>1" "indep (insert x B\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
basis B\<^sub>1
basis B\<^sub>2
card B\<^sub>1 < card B\<^sub>2

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> B\<^sub>2 - B\<^sub>1; indep (insert x B\<^sub>1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using augment basisD
[PROOF STATE]
proof (prove)
using this:
basis B\<^sub>1
basis B\<^sub>2
card B\<^sub>1 < card B\<^sub>2
\<lbrakk>indep ?X; indep ?Y; card ?Y < card ?X\<rbrakk> \<Longrightarrow> \<exists>x\<in>?X - ?Y. indep (insert x ?Y)
basis ?X \<Longrightarrow> indep ?X
\<lbrakk>basis ?X; ?x \<in> carrier - ?X\<rbrakk> \<Longrightarrow> \<not> indep (insert ?x ?X)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> B\<^sub>2 - B\<^sub>1; indep (insert x B\<^sub>1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> B\<^sub>2 - B\<^sub>1
indep (insert x B\<^sub>1)

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> B\<^sub>2 - B\<^sub>1
indep (insert x B\<^sub>1)
[PROOF STEP]
have "x \<in> carrier - B\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
x \<in> B\<^sub>2 - B\<^sub>1
indep (insert x B\<^sub>1)

goal (1 subgoal):
 1. x \<in> carrier - B\<^sub>1
[PROOF STEP]
using \<open>basis B\<^sub>1\<close> basisD indep_subset_carrier
[PROOF STATE]
proof (prove)
using this:
x \<in> B\<^sub>2 - B\<^sub>1
indep (insert x B\<^sub>1)
basis B\<^sub>1
basis ?X \<Longrightarrow> indep ?X
\<lbrakk>basis ?X; ?x \<in> carrier - ?X\<rbrakk> \<Longrightarrow> \<not> indep (insert ?x ?X)
indep ?X \<Longrightarrow> ?X \<subseteq> carrier

goal (1 subgoal):
 1. x \<in> carrier - B\<^sub>1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> carrier - B\<^sub>1

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier - B\<^sub>1
[PROOF STEP]
have "\<not> indep (insert x B\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier - B\<^sub>1

goal (1 subgoal):
 1. \<not> indep (insert x B\<^sub>1)
[PROOF STEP]
using \<open>basis B\<^sub>1\<close> basisD
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier - B\<^sub>1
basis B\<^sub>1
basis ?X \<Longrightarrow> indep ?X
\<lbrakk>basis ?X; ?x \<in> carrier - ?X\<rbrakk> \<Longrightarrow> \<not> indep (insert ?x ?X)

goal (1 subgoal):
 1. \<not> indep (insert x B\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> indep (insert x B\<^sub>1)

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> indep (insert x B\<^sub>1)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<not> indep (insert x B\<^sub>1)

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>indep (insert x B\<^sub>1)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> indep (insert x B\<^sub>1)
indep (insert x B\<^sub>1)

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

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>basis ?B\<^sub>1'2; basis ?B\<^sub>2'2; card ?B\<^sub>1'2 < card ?B\<^sub>2'2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. card B\<^sub>1 \<noteq> card B\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1
\<lbrakk>basis ?B\<^sub>1'2; basis ?B\<^sub>2'2; card ?B\<^sub>1'2 < card ?B\<^sub>2'2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1
\<lbrakk>basis ?B\<^sub>1'2; basis ?B\<^sub>2'2; card ?B\<^sub>1'2 < card ?B\<^sub>2'2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1
\<lbrakk>basis ?B\<^sub>1'2; basis ?B\<^sub>2'2; card ?B\<^sub>1'2 < card ?B\<^sub>2'2\<rbrakk> \<Longrightarrow> False
basis B\<^sub>1
basis B\<^sub>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_indep_card:
  assumes "indep X"
  assumes "basis B"
  shows "card X \<le> card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card X \<le> card B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card X \<le> card B
[PROOF STEP]
obtain B' where "basis B'" "X \<subseteq> B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B'. \<lbrakk>basis B'; X \<subseteq> B'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms indep_imp_subset_basis
[PROOF STATE]
proof (prove)
using this:
indep X
basis B
indep ?X \<Longrightarrow> \<exists>B. basis B \<and> ?X \<subseteq> B

goal (1 subgoal):
 1. (\<And>B'. \<lbrakk>basis B'; X \<subseteq> B'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis B'
X \<subseteq> B'

goal (1 subgoal):
 1. card X \<le> card B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis B'
X \<subseteq> B'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis B'
X \<subseteq> B'

goal (1 subgoal):
 1. card X \<le> card B
[PROOF STEP]
using assms basis_finite basis_card[of B B']
[PROOF STATE]
proof (prove)
using this:
basis B'
X \<subseteq> B'
indep X
basis B
basis ?A \<Longrightarrow> finite ?A
\<lbrakk>basis B; basis B'\<rbrakk> \<Longrightarrow> card B = card B'

goal (1 subgoal):
 1. card X \<le> card B
[PROOF STEP]
by (auto intro: card_mono)
[PROOF STATE]
proof (state)
this:
card X \<le> card B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_augment:
  assumes "basis B\<^sub>1" "basis B\<^sub>2" "x \<in> B\<^sub>1 - B\<^sub>2"
  shows "\<exists>y \<in> B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
let ?B\<^sub>1 = "B\<^sub>1 - {x}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
have "card ?B\<^sub>1 < card B\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (B\<^sub>1 - {x}) < card B\<^sub>2
[PROOF STEP]
using assms basis_card[of B\<^sub>1 B\<^sub>2] card_Diff1_less[OF basis_finite, of B\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
basis B\<^sub>1
basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
\<lbrakk>basis B\<^sub>1; basis B\<^sub>2\<rbrakk> \<Longrightarrow> card B\<^sub>1 = card B\<^sub>2
\<lbrakk>basis B\<^sub>1; ?x \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> card (B\<^sub>1 - {?x}) < card B\<^sub>1

goal (1 subgoal):
 1. card (B\<^sub>1 - {x}) < card B\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (B\<^sub>1 - {x}) < card B\<^sub>2

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (B\<^sub>1 - {x}) < card B\<^sub>2

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
have "indep ?B\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep (B\<^sub>1 - {x})
[PROOF STEP]
using assms basis_indep[of B\<^sub>1] indep_subset[of B\<^sub>1 ?B\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
basis B\<^sub>1
basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
basis B\<^sub>1 \<Longrightarrow> indep B\<^sub>1
\<lbrakk>indep B\<^sub>1; B\<^sub>1 - {x} \<subseteq> B\<^sub>1\<rbrakk> \<Longrightarrow> indep (B\<^sub>1 - {x})

goal (1 subgoal):
 1. indep (B\<^sub>1 - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indep (B\<^sub>1 - {x})

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (B\<^sub>1 - {x}) < card B\<^sub>2
indep (B\<^sub>1 - {x})
[PROOF STEP]
obtain y where y: "y \<in> B\<^sub>2 - ?B\<^sub>1" "indep (insert y ?B\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
card (B\<^sub>1 - {x}) < card B\<^sub>2
indep (B\<^sub>1 - {x})

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> B\<^sub>2 - (B\<^sub>1 - {x}); indep (insert y (B\<^sub>1 - {x}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms augment[of B\<^sub>2 ?B\<^sub>1] basis_indep
[PROOF STATE]
proof (prove)
using this:
card (B\<^sub>1 - {x}) < card B\<^sub>2
indep (B\<^sub>1 - {x})
basis B\<^sub>1
basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
\<lbrakk>indep B\<^sub>2; indep (B\<^sub>1 - {x}); card (B\<^sub>1 - {x}) < card B\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>xa\<in>B\<^sub>2 - (B\<^sub>1 - {x}). indep (insert xa (B\<^sub>1 - {x}))
basis ?X \<Longrightarrow> indep ?X

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> B\<^sub>2 - (B\<^sub>1 - {x}); indep (insert y (B\<^sub>1 - {x}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> B\<^sub>2 - (B\<^sub>1 - {x})
indep (insert y (B\<^sub>1 - {x}))

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
let ?B\<^sub>1' = "insert y ?B\<^sub>1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
have "basis ?B\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
using \<open>indep ?B\<^sub>1'\<close>
[PROOF STATE]
proof (prove)
using this:
indep (insert y (B\<^sub>1 - {x}))

goal (1 subgoal):
 1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
proof (rule basisI, goal_cases "insert")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> carrier - insert y (B\<^sub>1 - {x}) \<Longrightarrow> \<not> indep (insert xa (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
case (insert x)
[PROOF STATE]
proof (state)
this:
x \<in> carrier - insert y (B\<^sub>1 - {x})

goal (1 subgoal):
 1. \<And>xa. xa \<in> carrier - insert y (B\<^sub>1 - {x}) \<Longrightarrow> \<not> indep (insert xa (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
have "card (insert x ?B\<^sub>1') > card B\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
have "card (insert x ?B\<^sub>1') = Suc (card ?B\<^sub>1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert x (insert y (B\<^sub>1 - {x}))) = Suc (card (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
using insert card.insert_remove[OF indep_finite, of ?B\<^sub>1'] y
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier - insert y (B\<^sub>1 - {x})
indep (insert y (B\<^sub>1 - {x})) \<Longrightarrow> card (insert ?x (insert y (B\<^sub>1 - {x}))) = Suc (card (insert y (B\<^sub>1 - {x}) - {?x}))
y \<in> B\<^sub>2 - (B\<^sub>1 - {x})
indep (insert y (B\<^sub>1 - {x}))

goal (1 subgoal):
 1. card (insert x (insert y (B\<^sub>1 - {x}))) = Suc (card (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (insert x (insert y (B\<^sub>1 - {x}))) = Suc (card (insert y (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (insert x (insert y (B\<^sub>1 - {x}))) = Suc (card (insert y (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
have "\<dots> = Suc (Suc (card ?B\<^sub>1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card (insert y (B\<^sub>1 - {x}))) = Suc (Suc (card (B\<^sub>1 - {x})))
[PROOF STEP]
using card.insert_remove[OF indep_finite, of ?B\<^sub>1] \<open>indep ?B\<^sub>1\<close> y
[PROOF STATE]
proof (prove)
using this:
indep (B\<^sub>1 - {x}) \<Longrightarrow> card (insert ?x (B\<^sub>1 - {x})) = Suc (card (B\<^sub>1 - {x} - {?x}))
indep (B\<^sub>1 - {x})
y \<in> B\<^sub>2 - (B\<^sub>1 - {x})
indep (insert y (B\<^sub>1 - {x}))

goal (1 subgoal):
 1. Suc (card (insert y (B\<^sub>1 - {x}))) = Suc (Suc (card (B\<^sub>1 - {x})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (card (insert y (B\<^sub>1 - {x}))) = Suc (Suc (card (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (card (insert y (B\<^sub>1 - {x}))) = Suc (Suc (card (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
have "\<dots> = Suc (card B\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Suc (card (B\<^sub>1 - {x}))) = Suc (card B\<^sub>1)
[PROOF STEP]
using assms basis_finite[of B\<^sub>1] card.remove[of B\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
basis B\<^sub>1
basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
basis B\<^sub>1 \<Longrightarrow> finite B\<^sub>1
\<lbrakk>finite B\<^sub>1; ?x \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> card B\<^sub>1 = Suc (card (B\<^sub>1 - {?x}))

goal (1 subgoal):
 1. Suc (Suc (card (B\<^sub>1 - {x}))) = Suc (card B\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (Suc (card (B\<^sub>1 - {x}))) = Suc (card B\<^sub>1)

goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (insert x (insert y (B\<^sub>1 - {x}))) = Suc (card B\<^sub>1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (insert x (insert y (B\<^sub>1 - {x}))) = Suc (card B\<^sub>1)

goal (1 subgoal):
 1. card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. \<And>xa. xa \<in> carrier - insert y (B\<^sub>1 - {x}) \<Longrightarrow> \<not> indep (insert xa (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
have "\<not>indep (insert x (insert y ?B\<^sub>1))"
[PROOF STATE]
proof (prove)
using this:
card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. \<not> indep (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
using assms basis_indep_card[of "insert x (insert y ?B\<^sub>1)" B\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
card B\<^sub>1 < card (insert x (insert y (B\<^sub>1 - {x})))
basis B\<^sub>1
basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
\<lbrakk>indep (insert x (insert y (B\<^sub>1 - {x}))); basis B\<^sub>1\<rbrakk> \<Longrightarrow> card (insert x (insert y (B\<^sub>1 - {x}))) \<le> card B\<^sub>1

goal (1 subgoal):
 1. \<not> indep (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> indep (insert x (insert y (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. \<And>xa. xa \<in> carrier - insert y (B\<^sub>1 - {x}) \<Longrightarrow> \<not> indep (insert xa (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> indep (insert x (insert y (B\<^sub>1 - {x})))

goal (1 subgoal):
 1. \<And>xa. xa \<in> carrier - insert y (B\<^sub>1 - {x}) \<Longrightarrow> \<not> indep (insert xa (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
have "insert x (insert y ?B\<^sub>1) \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x (insert y (B\<^sub>1 - {x})) \<subseteq> carrier
[PROOF STEP]
using assms insert y basis_finite indep_subset_carrier
[PROOF STATE]
proof (prove)
using this:
basis B\<^sub>1
basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
x \<in> carrier - insert y (B\<^sub>1 - {x})
y \<in> B\<^sub>2 - (B\<^sub>1 - {x})
indep (insert y (B\<^sub>1 - {x}))
basis ?A \<Longrightarrow> finite ?A
indep ?X \<Longrightarrow> ?X \<subseteq> carrier

goal (1 subgoal):
 1. insert x (insert y (B\<^sub>1 - {x})) \<subseteq> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x (insert y (B\<^sub>1 - {x})) \<subseteq> carrier

goal (1 subgoal):
 1. \<And>xa. xa \<in> carrier - insert y (B\<^sub>1 - {x}) \<Longrightarrow> \<not> indep (insert xa (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> indep (insert x (insert y (B\<^sub>1 - {x})))
insert x (insert y (B\<^sub>1 - {x})) \<subseteq> carrier
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> indep (insert x (insert y (B\<^sub>1 - {x})))
insert x (insert y (B\<^sub>1 - {x})) \<subseteq> carrier

goal (1 subgoal):
 1. \<not> indep (insert x (insert y (B\<^sub>1 - {x})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> indep (insert x (insert y (B\<^sub>1 - {x})))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
basis (insert y (B\<^sub>1 - {x}))

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis (insert y (B\<^sub>1 - {x}))

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
using assms y
[PROOF STATE]
proof (prove)
using this:
basis (insert y (B\<^sub>1 - {x}))
basis B\<^sub>1
basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
y \<in> B\<^sub>2 - (B\<^sub>1 - {x})
indep (insert y (B\<^sub>1 - {x}))

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_in_augment:
  assumes "basis_in \<E> B\<^sub>1" "basis_in \<E> B\<^sub>2" "x \<in> B\<^sub>1 - B\<^sub>2"
  shows "\<exists>y \<in> B\<^sub>2 - B\<^sub>1. basis_in \<E> (insert y (B\<^sub>1 - {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis_in \<E> (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
using assms \<E>.basis_augment
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> B\<^sub>1
basis_in \<E> B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
\<lbrakk>\<E>.basis ?B\<^sub>1; \<E>.basis ?B\<^sub>2; ?x \<in> ?B\<^sub>1 - ?B\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>y\<in>?B\<^sub>2 - ?B\<^sub>1. \<E>.basis (insert y (?B\<^sub>1 - {?x}))

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. basis_in \<E> (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
unfolding basis_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.basis B\<^sub>1
\<E>.basis B\<^sub>2
x \<in> B\<^sub>1 - B\<^sub>2
\<lbrakk>\<E>.basis ?B\<^sub>1; \<E>.basis ?B\<^sub>2; ?x \<in> ?B\<^sub>1 - ?B\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>y\<in>?B\<^sub>2 - ?B\<^sub>1. \<E>.basis (insert y (?B\<^sub>1 - {?x}))

goal (1 subgoal):
 1. \<exists>y\<in>B\<^sub>2 - B\<^sub>1. \<E>.basis (insert y (B\<^sub>1 - {x}))
[PROOF STEP]
by auto


[STATEMENT]
lemma circuit_elim:
  assumes "circuit C\<^sub>1" "circuit C\<^sub>2" "C\<^sub>1 \<noteq> C\<^sub>2" "x \<in> C\<^sub>1 \<inter> C\<^sub>2"
  shows "\<exists>C\<^sub>3 \<subseteq> (C\<^sub>1 \<union> C\<^sub>2) - {x}. circuit C\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
let ?C = "(C\<^sub>1 \<union> C\<^sub>2) - {x}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
let ?carrier = "C\<^sub>1 \<union> C\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have assms': "circuit_in carrier C\<^sub>1" "circuit_in carrier C\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circuit_in carrier C\<^sub>1 &&& circuit_in carrier C\<^sub>2
[PROOF STEP]
using assms circuit_imp_circuit_in
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
circuit ?C \<Longrightarrow> circuit_in carrier ?C

goal (1 subgoal):
 1. circuit_in carrier C\<^sub>1 &&& circuit_in carrier C\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
circuit_in carrier C\<^sub>1
circuit_in carrier C\<^sub>2

goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "?C \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>1 \<union> C\<^sub>2 - {x} \<subseteq> carrier
[PROOF STEP]
using assms circuit_subset_carrier
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
circuit ?X \<Longrightarrow> ?X \<subseteq> carrier

goal (1 subgoal):
 1. C\<^sub>1 \<union> C\<^sub>2 - {x} \<subseteq> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 \<union> C\<^sub>2 - {x} \<subseteq> carrier

goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
proof (cases "indep ?C")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
 2. \<not> indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> indep (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (2 subgoals):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
 2. \<not> indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> indep (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> indep (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
using dep_iff_supset_circuit \<open>?C \<subseteq> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> indep (C\<^sub>1 \<union> C\<^sub>2 - {x})
?X \<subseteq> carrier \<Longrightarrow> (\<not> indep ?X) = (\<exists>C. circuit C \<and> C \<subseteq> ?X)
C\<^sub>1 \<union> C\<^sub>2 - {x} \<subseteq> carrier

goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
indep (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
have "indep_in ?carrier ?C"
[PROOF STATE]
proof (prove)
using this:
indep (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
using \<open>?C \<subseteq> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
indep (C\<^sub>1 \<union> C\<^sub>2 - {x})
C\<^sub>1 \<union> C\<^sub>2 - {x} \<subseteq> carrier

goal (1 subgoal):
 1. indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
by (auto intro: indep_inI)
[PROOF STATE]
proof (state)
this:
indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have *: "?carrier \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>1 \<union> C\<^sub>2 \<subseteq> carrier
[PROOF STEP]
using assms circuit_subset_carrier
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
circuit ?X \<Longrightarrow> ?X \<subseteq> carrier

goal (1 subgoal):
 1. C\<^sub>1 \<union> C\<^sub>2 \<subseteq> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 \<union> C\<^sub>2 \<subseteq> carrier

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
obtain y where y: "y \<in> C\<^sub>2" "y \<notin> C\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> C\<^sub>2; y \<notin> C\<^sub>1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms circuit_subset_eq
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
\<lbrakk>circuit ?C\<^sub>1; circuit ?C\<^sub>2; ?C\<^sub>1 \<subseteq> ?C\<^sub>2\<rbrakk> \<Longrightarrow> ?C\<^sub>1 = ?C\<^sub>2

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> C\<^sub>2; y \<notin> C\<^sub>1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> C\<^sub>2
y \<notin> C\<^sub>1

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> C\<^sub>2
y \<notin> C\<^sub>1
[PROOF STEP]
have "indep_in ?carrier (C\<^sub>2 - {y})"
[PROOF STATE]
proof (prove)
using this:
y \<in> C\<^sub>2
y \<notin> C\<^sub>1

goal (1 subgoal):
 1. indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {y})
[PROOF STEP]
using assms' circuit_in_min_dep_in[OF * circuit_in_supI[OF *, of C\<^sub>2]]
[PROOF STATE]
proof (prove)
using this:
y \<in> C\<^sub>2
y \<notin> C\<^sub>1
circuit_in carrier C\<^sub>1
circuit_in carrier C\<^sub>2
\<lbrakk>carrier \<subseteq> carrier; C\<^sub>2 \<subseteq> C\<^sub>1 \<union> C\<^sub>2; circuit_in carrier C\<^sub>2; ?x \<in> C\<^sub>2\<rbrakk> \<Longrightarrow> indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {?x})

goal (1 subgoal):
 1. indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {y})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {y})

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {y})
[PROOF STEP]
obtain B where B: "basis_in ?carrier B" "C\<^sub>2 - {y} \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {y})

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>basis_in (C\<^sub>1 \<union> C\<^sub>2) B; C\<^sub>2 - {y} \<subseteq> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using * assms indep_in_imp_subset_basis_in[of ?carrier "C\<^sub>2 - {y}"]
[PROOF STATE]
proof (prove)
using this:
indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {y})
C\<^sub>1 \<union> C\<^sub>2 \<subseteq> carrier
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
\<lbrakk>C\<^sub>1 \<union> C\<^sub>2 \<subseteq> carrier; indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>2 - {y})\<rbrakk> \<Longrightarrow> \<exists>B. basis_in (C\<^sub>1 \<union> C\<^sub>2) B \<and> C\<^sub>2 - {y} \<subseteq> B

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>basis_in (C\<^sub>1 \<union> C\<^sub>2) B; C\<^sub>2 - {y} \<subseteq> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_in (C\<^sub>1 \<union> C\<^sub>2) B
C\<^sub>2 - {y} \<subseteq> B

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "y \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> B
[PROOF STEP]
proof (rule ccontr, goal_cases False)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y \<notin> B \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> y \<notin> B

goal (1 subgoal):
 1. \<not> y \<notin> B \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> y \<notin> B
[PROOF STEP]
have "C\<^sub>2 \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
\<not> y \<notin> B

goal (1 subgoal):
 1. C\<^sub>2 \<subseteq> B
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
\<not> y \<notin> B
basis_in (C\<^sub>1 \<union> C\<^sub>2) B
C\<^sub>2 - {y} \<subseteq> B

goal (1 subgoal):
 1. C\<^sub>2 \<subseteq> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>2 \<subseteq> B

goal (1 subgoal):
 1. \<not> y \<notin> B \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>2 \<subseteq> B

goal (1 subgoal):
 1. \<not> y \<notin> B \<Longrightarrow> False
[PROOF STEP]
have "circuit_in ?carrier C\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circuit_in (C\<^sub>1 \<union> C\<^sub>2) C\<^sub>2
[PROOF STEP]
using * assms' circuit_in_supI
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<union> C\<^sub>2 \<subseteq> carrier
circuit_in carrier C\<^sub>1
circuit_in carrier C\<^sub>2
\<lbrakk>?\<E>' \<subseteq> ?\<E>; ?\<E> \<subseteq> carrier; ?C \<subseteq> ?\<E>'; circuit_in ?\<E> ?C\<rbrakk> \<Longrightarrow> circuit_in ?\<E>' ?C

goal (1 subgoal):
 1. circuit_in (C\<^sub>1 \<union> C\<^sub>2) C\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
circuit_in (C\<^sub>1 \<union> C\<^sub>2) C\<^sub>2

goal (1 subgoal):
 1. \<not> y \<notin> B \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>2 \<subseteq> B
circuit_in (C\<^sub>1 \<union> C\<^sub>2) C\<^sub>2
[PROOF STEP]
have "\<not> indep_in ?carrier B"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>2 \<subseteq> B
circuit_in (C\<^sub>1 \<union> C\<^sub>2) C\<^sub>2

goal (1 subgoal):
 1. \<not> indep_in (C\<^sub>1 \<union> C\<^sub>2) B
[PROOF STEP]
using B basis_in_subset_carrier[OF *] supset_circuit_in_imp_dep_in[OF *]
[PROOF STATE]
proof (prove)
using this:
C\<^sub>2 \<subseteq> B
circuit_in (C\<^sub>1 \<union> C\<^sub>2) C\<^sub>2
basis_in (C\<^sub>1 \<union> C\<^sub>2) B
C\<^sub>2 - {y} \<subseteq> B
basis_in (C\<^sub>1 \<union> C\<^sub>2) ?X \<Longrightarrow> ?X \<subseteq> C\<^sub>1 \<union> C\<^sub>2
circuit_in (C\<^sub>1 \<union> C\<^sub>2) ?C \<and> ?C \<subseteq> ?X \<Longrightarrow> \<not> indep_in (C\<^sub>1 \<union> C\<^sub>2) ?X

goal (1 subgoal):
 1. \<not> indep_in (C\<^sub>1 \<union> C\<^sub>2) B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> indep_in (C\<^sub>1 \<union> C\<^sub>2) B

goal (1 subgoal):
 1. \<not> y \<notin> B \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> indep_in (C\<^sub>1 \<union> C\<^sub>2) B
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> indep_in (C\<^sub>1 \<union> C\<^sub>2) B

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms B basis_in_indep_in[OF *]
[PROOF STATE]
proof (prove)
using this:
\<not> indep_in (C\<^sub>1 \<union> C\<^sub>2) B
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
basis_in (C\<^sub>1 \<union> C\<^sub>2) B
C\<^sub>2 - {y} \<subseteq> B
basis_in (C\<^sub>1 \<union> C\<^sub>2) ?X \<Longrightarrow> indep_in (C\<^sub>1 \<union> C\<^sub>2) ?X

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:
y \<notin> B

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "C\<^sub>1 - B \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>1 - B \<noteq> {}
[PROOF STEP]
proof (rule ccontr, goal_cases False)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> C\<^sub>1 - B \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> C\<^sub>1 - B \<noteq> {}

goal (1 subgoal):
 1. \<not> C\<^sub>1 - B \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> C\<^sub>1 - B \<noteq> {}
[PROOF STEP]
have "C\<^sub>1 - (C\<^sub>1 \<inter> B) = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> C\<^sub>1 - B \<noteq> {}

goal (1 subgoal):
 1. C\<^sub>1 - C\<^sub>1 \<inter> B = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 - C\<^sub>1 \<inter> B = {}

goal (1 subgoal):
 1. \<not> C\<^sub>1 - B \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 - C\<^sub>1 \<inter> B = {}
[PROOF STEP]
have "C\<^sub>1 = C\<^sub>1 \<inter> B"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 - C\<^sub>1 \<inter> B = {}

goal (1 subgoal):
 1. C\<^sub>1 = C\<^sub>1 \<inter> B
[PROOF STEP]
using assms circuit_subset_eq
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 - C\<^sub>1 \<inter> B = {}
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
\<lbrakk>circuit ?C\<^sub>1; circuit ?C\<^sub>2; ?C\<^sub>1 \<subseteq> ?C\<^sub>2\<rbrakk> \<Longrightarrow> ?C\<^sub>1 = ?C\<^sub>2

goal (1 subgoal):
 1. C\<^sub>1 = C\<^sub>1 \<inter> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 = C\<^sub>1 \<inter> B

goal (1 subgoal):
 1. \<not> C\<^sub>1 - B \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>1 = C\<^sub>1 \<inter> B

goal (1 subgoal):
 1. \<not> C\<^sub>1 - B \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
have "indep (C\<^sub>1 \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep (C\<^sub>1 \<inter> B)
[PROOF STEP]
using assms B basis_in_indep_in[OF *] indep_in_subset[OF *, of B "C\<^sub>1 \<inter> B"] indep_in_indep
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
basis_in (C\<^sub>1 \<union> C\<^sub>2) B
C\<^sub>2 - {y} \<subseteq> B
basis_in (C\<^sub>1 \<union> C\<^sub>2) ?X \<Longrightarrow> indep_in (C\<^sub>1 \<union> C\<^sub>2) ?X
\<lbrakk>indep_in (C\<^sub>1 \<union> C\<^sub>2) B; C\<^sub>1 \<inter> B \<subseteq> B\<rbrakk> \<Longrightarrow> indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>1 \<inter> B)
indep_in ?\<E> ?X \<Longrightarrow> indep ?X

goal (1 subgoal):
 1. indep (C\<^sub>1 \<inter> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indep (C\<^sub>1 \<inter> B)

goal (1 subgoal):
 1. \<not> C\<^sub>1 - B \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 = C\<^sub>1 \<inter> B
indep (C\<^sub>1 \<inter> B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 = C\<^sub>1 \<inter> B
indep (C\<^sub>1 \<inter> B)

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms circuitD
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 = C\<^sub>1 \<inter> B
indep (C\<^sub>1 \<inter> B)
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
circuit ?X \<Longrightarrow> ?X \<subseteq> carrier
circuit ?X \<Longrightarrow> \<not> indep ?X
\<lbrakk>circuit ?X; ?x \<in> ?X\<rbrakk> \<Longrightarrow> indep (?X - {?x})

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:
C\<^sub>1 - B \<noteq> {}

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 - B \<noteq> {}
[PROOF STEP]
obtain z where z: "z \<in> C\<^sub>1" "z \<notin> B"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 - B \<noteq> {}

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> C\<^sub>1; z \<notin> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> C\<^sub>1
z \<notin> B

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "y \<noteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<noteq> z
[PROOF STEP]
using y z
[PROOF STATE]
proof (prove)
using this:
y \<in> C\<^sub>2
y \<notin> C\<^sub>1
z \<in> C\<^sub>1
z \<notin> B

goal (1 subgoal):
 1. y \<noteq> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<noteq> z

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "x \<in> C\<^sub>1" "x \<in> C\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> C\<^sub>1 &&& x \<in> C\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2

goal (1 subgoal):
 1. x \<in> C\<^sub>1 &&& x \<in> C\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> C\<^sub>1
x \<in> C\<^sub>2

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "finite ?carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (C\<^sub>1 \<union> C\<^sub>2)
[PROOF STEP]
using assms carrier_finite finite_subset
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
finite carrier
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (C\<^sub>1 \<union> C\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (C\<^sub>1 \<union> C\<^sub>2)

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "card B \<le> card (?carrier - {y, z})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card B \<le> card (C\<^sub>1 \<union> C\<^sub>2 - {y, z})
[PROOF STEP]
proof (rule card_mono)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (C\<^sub>1 \<union> C\<^sub>2 - {y, z})
 2. B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}
[PROOF STEP]
show "finite (C\<^sub>1 \<union> C\<^sub>2 - {y, z})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (C\<^sub>1 \<union> C\<^sub>2 - {y, z})
[PROOF STEP]
using \<open>finite ?carrier\<close>
[PROOF STATE]
proof (prove)
using this:
finite (C\<^sub>1 \<union> C\<^sub>2)

goal (1 subgoal):
 1. finite (C\<^sub>1 \<union> C\<^sub>2 - {y, z})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (C\<^sub>1 \<union> C\<^sub>2 - {y, z})

goal (1 subgoal):
 1. B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}
[PROOF STEP]
show "B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}
[PROOF STEP]
using B basis_in_subset_carrier[OF *, of B] \<open>y \<notin> B\<close> \<open>z \<notin> B\<close>
[PROOF STATE]
proof (prove)
using this:
basis_in (C\<^sub>1 \<union> C\<^sub>2) B
C\<^sub>2 - {y} \<subseteq> B
basis_in (C\<^sub>1 \<union> C\<^sub>2) B \<Longrightarrow> B \<subseteq> C\<^sub>1 \<union> C\<^sub>2
y \<notin> B
z \<notin> B

goal (1 subgoal):
 1. B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card B \<le> card (C\<^sub>1 \<union> C\<^sub>2 - {y, z})

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card B \<le> card (C\<^sub>1 \<union> C\<^sub>2 - {y, z})

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "\<dots> = card ?carrier - 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2 - {y, z}) = card (C\<^sub>1 \<union> C\<^sub>2) - 2
[PROOF STEP]
using \<open>finite ?carrier\<close> \<open>y \<in> C\<^sub>2\<close> \<open>z \<in> C\<^sub>1\<close> \<open>y \<noteq> z\<close> card_Diff_subset_Int
[PROOF STATE]
proof (prove)
using this:
finite (C\<^sub>1 \<union> C\<^sub>2)
y \<in> C\<^sub>2
z \<in> C\<^sub>1
y \<noteq> z
finite (?A \<inter> ?B) \<Longrightarrow> card (?A - ?B) = card ?A - card (?A \<inter> ?B)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2 - {y, z}) = card (C\<^sub>1 \<union> C\<^sub>2) - 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2 - {y, z}) = card (C\<^sub>1 \<union> C\<^sub>2) - 2

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2 - {y, z}) = card (C\<^sub>1 \<union> C\<^sub>2) - 2

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "\<dots> < card ?carrier - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
have "card ?carrier = card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)
[PROOF STEP]
using assms \<open>finite ?carrier\<close> card_Un_Int[of C\<^sub>1 C\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
finite (C\<^sub>1 \<union> C\<^sub>2)
\<lbrakk>finite C\<^sub>1; finite C\<^sub>2\<rbrakk> \<Longrightarrow> card C\<^sub>1 + card C\<^sub>2 = card (C\<^sub>1 \<union> C\<^sub>2) + card (C\<^sub>1 \<inter> C\<^sub>2)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
have "\<dots> = card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2) = card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2))
[PROOF STEP]
using assms \<open>finite ?carrier\<close> card_mono[of C\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
finite (C\<^sub>1 \<union> C\<^sub>2)
\<lbrakk>finite C\<^sub>2; ?A \<subseteq> C\<^sub>2\<rbrakk> \<Longrightarrow> card ?A \<le> card C\<^sub>2

goal (1 subgoal):
 1. card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2) = card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2) = card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2))

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2) = card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2))

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
have "\<dots> = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
have "card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1)
[PROOF STEP]
using assms \<open>finite ?carrier\<close> card_Diff_subset_Int[of C\<^sub>2 C\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
finite (C\<^sub>1 \<union> C\<^sub>2)
finite (C\<^sub>2 \<inter> C\<^sub>1) \<Longrightarrow> card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1)

goal (1 subgoal):
 1. card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1)

goal (1 subgoal):
 1. card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1)

goal (1 subgoal):
 1. card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
have "\<dots> = card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)
[PROOF STEP]
by (simp add: inf_commute)
[PROOF STATE]
proof (state)
this:
card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)

goal (1 subgoal):
 1. card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)

goal (1 subgoal):
 1. card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
have "card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
have "card C\<^sub>1 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < card C\<^sub>1
[PROOF STEP]
using assms circuit_nonempty \<open>finite ?carrier\<close>
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
circuit ?X \<Longrightarrow> ?X \<noteq> {}
finite (C\<^sub>1 \<union> C\<^sub>2)

goal (1 subgoal):
 1. 0 < card C\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < card C\<^sub>1

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < card C\<^sub>1

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
have "card (C\<^sub>2 - C\<^sub>1) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
using assms \<open>finite ?carrier\<close> \<open>y \<in> C\<^sub>2\<close> \<open>y \<notin> C\<^sub>1\<close>
[PROOF STATE]
proof (prove)
using this:
circuit C\<^sub>1
circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
finite (C\<^sub>1 \<union> C\<^sub>2)
y \<in> C\<^sub>2
y \<notin> C\<^sub>1

goal (1 subgoal):
 1. 0 < card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < card (C\<^sub>2 - C\<^sub>1)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
0 < card C\<^sub>1
0 < card (C\<^sub>2 - C\<^sub>1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)
0 < card C\<^sub>1
0 < card (C\<^sub>2 - C\<^sub>1)

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) - 2 < card (C\<^sub>1 \<union> C\<^sub>2) - 1

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
have "\<dots> = card ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 1 = card (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
using \<open>finite ?carrier\<close> card_Diff_singleton \<open>x \<in> C\<^sub>1\<close> \<open>x \<in> C\<^sub>2\<close>
[PROOF STATE]
proof (prove)
using this:
finite (C\<^sub>1 \<union> C\<^sub>2)
?x \<in> ?A \<Longrightarrow> card (?A - {?x}) = card ?A - 1
x \<in> C\<^sub>1
x \<in> C\<^sub>2

goal (1 subgoal):
 1. card (C\<^sub>1 \<union> C\<^sub>2) - 1 = card (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (C\<^sub>1 \<union> C\<^sub>2) - 1 = card (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card B < card (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
have "card B < card ?C"
[PROOF STATE]
proof (prove)
using this:
card B < card (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. card B < card (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card B < card (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card B < card (C\<^sub>1 \<union> C\<^sub>2 - {x})
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
card B < card (C\<^sub>1 \<union> C\<^sub>2 - {x})

goal (1 subgoal):
 1. False
[PROOF STEP]
using basis_in_indep_in_card[OF *, of ?C B] B \<open>indep_in ?carrier ?C\<close>
[PROOF STATE]
proof (prove)
using this:
card B < card (C\<^sub>1 \<union> C\<^sub>2 - {x})
\<lbrakk>indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>1 \<union> C\<^sub>2 - {x}); basis_in (C\<^sub>1 \<union> C\<^sub>2) B\<rbrakk> \<Longrightarrow> card (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<le> card B
basis_in (C\<^sub>1 \<union> C\<^sub>2) B
C\<^sub>2 - {y} \<subseteq> B
indep_in (C\<^sub>1 \<union> C\<^sub>2) (C\<^sub>1 \<union> C\<^sub>2 - {x})

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

goal (1 subgoal):
 1. indep (C\<^sub>1 \<union> C\<^sub>2 - {x}) \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit C\<^sub>3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_dep_imp_supset_circuit:
  assumes "indep X"
  assumes "circuit C"
  assumes "C \<subseteq> insert x X"
  shows "x \<in> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> C \<Longrightarrow> False
[PROOF STEP]
assume "x \<notin> C"
[PROOF STATE]
proof (state)
this:
x \<notin> C

goal (1 subgoal):
 1. x \<notin> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> C
[PROOF STEP]
have "C \<subseteq> X"
[PROOF STATE]
proof (prove)
using this:
x \<notin> C

goal (1 subgoal):
 1. C \<subseteq> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<notin> C
indep X
circuit C
C \<subseteq> insert x X

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

goal (1 subgoal):
 1. x \<notin> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<subseteq> X
[PROOF STEP]
have "indep C"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> X

goal (1 subgoal):
 1. indep C
[PROOF STEP]
using assms indep_subset
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> X
indep X
circuit C
C \<subseteq> insert x X
\<lbrakk>indep ?X; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> indep ?Y

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

goal (1 subgoal):
 1. x \<notin> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
indep C

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms circuitD
[PROOF STATE]
proof (prove)
using this:
indep C
indep X
circuit C
C \<subseteq> insert x X
circuit ?X \<Longrightarrow> ?X \<subseteq> carrier
circuit ?X \<Longrightarrow> \<not> indep ?X
\<lbrakk>circuit ?X; ?x \<in> ?X\<rbrakk> \<Longrightarrow> indep (?X - {?x})

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_dep_imp_ex1_supset_circuit:
  assumes "x \<in> carrier"
  assumes "indep X"
  assumes "\<not> indep (insert x X)"
  shows "\<exists>!C. circuit C \<and> C \<subseteq> insert x X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x X
[PROOF STEP]
obtain C where C: "circuit C" "C \<subseteq> insert x X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>circuit C; C \<subseteq> insert x X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms indep_subset_carrier dep_iff_supset_circuit
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
indep X
\<not> indep (insert x X)
indep ?X \<Longrightarrow> ?X \<subseteq> carrier
?X \<subseteq> carrier \<Longrightarrow> (\<not> indep ?X) = (\<exists>C. circuit C \<and> C \<subseteq> ?X)

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>circuit C; C \<subseteq> insert x X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
circuit C
C \<subseteq> insert x X

goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x X
[PROOF STEP]
proof (rule ex1I, goal_cases ex unique)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. circuit ?a \<and> ?a \<subseteq> insert x X
 2. \<And>C. circuit C \<and> C \<subseteq> insert x X \<Longrightarrow> C = ?a
[PROOF STEP]
show "circuit C \<and> C \<subseteq> insert x X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circuit C \<and> C \<subseteq> insert x X
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
circuit C
C \<subseteq> insert x X

goal (1 subgoal):
 1. circuit C \<and> C \<subseteq> insert x X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
circuit C \<and> C \<subseteq> insert x X

goal (1 subgoal):
 1. \<And>Ca. circuit Ca \<and> Ca \<subseteq> insert x X \<Longrightarrow> Ca = C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ca. circuit Ca \<and> Ca \<subseteq> insert x X \<Longrightarrow> Ca = C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ca. circuit Ca \<and> Ca \<subseteq> insert x X \<Longrightarrow> Ca = C
[PROOF STEP]
fix C'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ca. circuit Ca \<and> Ca \<subseteq> insert x X \<Longrightarrow> Ca = C
[PROOF STEP]
assume C': "circuit C'" "C' \<subseteq> insert x X"
[PROOF STATE]
proof (state)
this:
circuit C'
C' \<subseteq> insert x X

goal (1 subgoal):
 1. \<And>Ca. circuit Ca \<and> Ca \<subseteq> insert x X \<Longrightarrow> Ca = C
[PROOF STEP]
have "C' = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C' = C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C' \<noteq> C \<Longrightarrow> False
[PROOF STEP]
assume "C' \<noteq> C"
[PROOF STATE]
proof (state)
this:
C' \<noteq> C

goal (1 subgoal):
 1. C' \<noteq> C \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C' \<noteq> C

goal (1 subgoal):
 1. C' \<noteq> C \<Longrightarrow> False
[PROOF STEP]
have "x \<in> C' \<inter> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> C' \<inter> C
[PROOF STEP]
using C C' assms min_dep_imp_supset_circuit
[PROOF STATE]
proof (prove)
using this:
circuit C
C \<subseteq> insert x X
circuit C'
C' \<subseteq> insert x X
x \<in> carrier
indep X
\<not> indep (insert x X)
\<lbrakk>indep ?X; circuit ?C; ?C \<subseteq> insert ?x ?X\<rbrakk> \<Longrightarrow> ?x \<in> ?C

goal (1 subgoal):
 1. x \<in> C' \<inter> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> C' \<inter> C

goal (1 subgoal):
 1. C' \<noteq> C \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C' \<noteq> C
x \<in> C' \<inter> C
[PROOF STEP]
have "\<not> indep (C' \<union> C - {x})"
[PROOF STATE]
proof (prove)
using this:
C' \<noteq> C
x \<in> C' \<inter> C

goal (1 subgoal):
 1. \<not> indep (C' \<union> C - {x})
[PROOF STEP]
using circuit_elim[OF C(1) C'(1), of x] supset_circuit_imp_dep[of _ "C' \<union> C - {x}"]
[PROOF STATE]
proof (prove)
using this:
C' \<noteq> C
x \<in> C' \<inter> C
\<lbrakk>C \<noteq> C'; x \<in> C \<inter> C'\<rbrakk> \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>C \<union> C' - {x}. circuit C\<^sub>3
circuit ?C \<and> ?C \<subseteq> C' \<union> C - {x} \<Longrightarrow> \<not> indep (C' \<union> C - {x})

goal (1 subgoal):
 1. \<not> indep (C' \<union> C - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> indep (C' \<union> C - {x})

goal (1 subgoal):
 1. C' \<noteq> C \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> indep (C' \<union> C - {x})

goal (1 subgoal):
 1. C' \<noteq> C \<Longrightarrow> False
[PROOF STEP]
have "C' \<union> C - {x} \<subseteq> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C' \<union> C - {x} \<subseteq> X
[PROOF STEP]
using C C'
[PROOF STATE]
proof (prove)
using this:
circuit C
C \<subseteq> insert x X
circuit C'
C' \<subseteq> insert x X

goal (1 subgoal):
 1. C' \<union> C - {x} \<subseteq> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C' \<union> C - {x} \<subseteq> X

goal (1 subgoal):
 1. C' \<noteq> C \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> indep (C' \<union> C - {x})
C' \<union> C - {x} \<subseteq> X
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> indep (C' \<union> C - {x})
C' \<union> C - {x} \<subseteq> X

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms indep_subset
[PROOF STATE]
proof (prove)
using this:
\<not> indep (C' \<union> C - {x})
C' \<union> C - {x} \<subseteq> X
x \<in> carrier
indep X
\<not> indep (insert x X)
\<lbrakk>indep ?X; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> indep ?Y

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:
C' = C

goal (1 subgoal):
 1. \<And>Ca. circuit Ca \<and> Ca \<subseteq> insert x X \<Longrightarrow> Ca = C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>circuit ?C'2; ?C'2 \<subseteq> insert x X\<rbrakk> \<Longrightarrow> ?C'2 = C

goal (1 subgoal):
 1. \<And>Ca. circuit Ca \<and> Ca \<subseteq> insert x X \<Longrightarrow> Ca = C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>circuit ?C'2; ?C'2 \<subseteq> insert x X\<rbrakk> \<Longrightarrow> ?C'2 = C
[PROOF STEP]
show "\<And>C'. circuit C' \<and> C' \<subseteq> insert x X \<Longrightarrow> C' = C"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>circuit ?C'2; ?C'2 \<subseteq> insert x X\<rbrakk> \<Longrightarrow> ?C'2 = C

goal (1 subgoal):
 1. \<And>C'. circuit C' \<and> C' \<subseteq> insert x X \<Longrightarrow> C' = C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
circuit ?C' \<and> ?C' \<subseteq> insert x X \<Longrightarrow> ?C' = C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!C. circuit C \<and> C \<subseteq> insert x X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_ex1_supset_circuit:
  assumes "basis B"
  assumes "x \<in> carrier - B"
  shows "\<exists>!C. circuit C \<and> C \<subseteq> insert x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x B
[PROOF STEP]
using assms min_dep_imp_ex1_supset_circuit basisD
[PROOF STATE]
proof (prove)
using this:
basis B
x \<in> carrier - B
\<lbrakk>?x \<in> carrier; indep ?X; \<not> indep (insert ?x ?X)\<rbrakk> \<Longrightarrow> \<exists>!C. circuit C \<and> C \<subseteq> insert ?x ?X
basis ?X \<Longrightarrow> indep ?X
\<lbrakk>basis ?X; ?x \<in> carrier - ?X\<rbrakk> \<Longrightarrow> \<not> indep (insert ?x ?X)

goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x B
[PROOF STEP]
by auto


[STATEMENT]
lemma circuit_iff_fund_circuit:
  "circuit C \<longleftrightarrow> (\<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circuit C = (\<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B)
[PROOF STEP]
proof (safe, goal_cases LTR RTL)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
case LTR
[PROOF STATE]
proof (state)
this:
circuit C

goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
circuit C
[PROOF STEP]
obtain x where "x \<in> C"
[PROOF STATE]
proof (prove)
using this:
circuit C

goal (1 subgoal):
 1. (\<And>x. x \<in> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using circuit_nonempty
[PROOF STATE]
proof (prove)
using this:
circuit C
circuit ?X \<Longrightarrow> ?X \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> C

goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> C
[PROOF STEP]
have "indep (C - {x})"
[PROOF STATE]
proof (prove)
using this:
x \<in> C

goal (1 subgoal):
 1. indep (C - {x})
[PROOF STEP]
using LTR
[PROOF STATE]
proof (prove)
using this:
x \<in> C
circuit C

goal (1 subgoal):
 1. indep (C - {x})
[PROOF STEP]
unfolding circuit_def
[PROOF STATE]
proof (prove)
using this:
x \<in> C
C \<subseteq> carrier \<and> \<not> indep C \<and> (\<forall>x\<in>C. indep (C - {x}))

goal (1 subgoal):
 1. indep (C - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indep (C - {x})

goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep (C - {x})
[PROOF STEP]
obtain B where B: "basis B" "C - {x} \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
indep (C - {x})

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>basis B; C - {x} \<subseteq> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using indep_imp_subset_basis
[PROOF STATE]
proof (prove)
using this:
indep (C - {x})
indep ?X \<Longrightarrow> \<exists>B. basis B \<and> ?X \<subseteq> B

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>basis B; C - {x} \<subseteq> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis B
C - {x} \<subseteq> B

goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis B
C - {x} \<subseteq> B
[PROOF STEP]
have "x \<in> carrier"
[PROOF STATE]
proof (prove)
using this:
basis B
C - {x} \<subseteq> B

goal (1 subgoal):
 1. x \<in> carrier
[PROOF STEP]
using LTR circuit_subset_carrier \<open>x \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
basis B
C - {x} \<subseteq> B
circuit C
circuit ?X \<Longrightarrow> ?X \<subseteq> carrier
x \<in> C

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

goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> carrier

goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
have "x \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> B
[PROOF STEP]
proof (rule ccontr, goal_cases False)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<notin> B \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x \<notin> B

goal (1 subgoal):
 1. \<not> x \<notin> B \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> x \<notin> B
[PROOF STEP]
have "C \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<notin> B

goal (1 subgoal):
 1. C \<subseteq> B
[PROOF STEP]
using \<open>C - {x} \<subseteq> B\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> x \<notin> B
C - {x} \<subseteq> B

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

goal (1 subgoal):
 1. \<not> x \<notin> B \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<subseteq> B
[PROOF STEP]
have "\<not> indep B"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> B

goal (1 subgoal):
 1. \<not> indep B
[PROOF STEP]
using LTR B basis_subset_carrier supset_circuit_imp_dep
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> B
circuit C
basis B
C - {x} \<subseteq> B
basis ?X \<Longrightarrow> ?X \<subseteq> carrier
circuit ?C \<and> ?C \<subseteq> ?X \<Longrightarrow> \<not> indep ?X

goal (1 subgoal):
 1. \<not> indep B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> indep B

goal (1 subgoal):
 1. \<not> x \<notin> B \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> indep B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> indep B

goal (1 subgoal):
 1. False
[PROOF STEP]
using B basis_indep
[PROOF STATE]
proof (prove)
using this:
\<not> indep B
basis B
C - {x} \<subseteq> B
basis ?X \<Longrightarrow> indep ?X

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:
x \<notin> B

goal (2 subgoals):
 1. circuit C \<Longrightarrow> \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
 2. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier
x \<notin> B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
x \<notin> B

goal (1 subgoal):
 1. \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B
[PROOF STEP]
unfolding fund_circuit_def
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
x \<notin> B

goal (1 subgoal):
 1. \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = (THE C. circuit C \<and> C \<subseteq> insert x B)
[PROOF STEP]
using LTR B theI_unique[OF basis_ex1_supset_circuit[of B x], of C]
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
x \<notin> B
circuit C
basis B
C - {x} \<subseteq> B
\<lbrakk>basis B; x \<in> carrier - B\<rbrakk> \<Longrightarrow> (circuit C \<and> C \<subseteq> insert x B) = (C = (THE C. circuit C \<and> C \<subseteq> insert x B))

goal (1 subgoal):
 1. \<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = (THE C. circuit C \<and> C \<subseteq> insert x B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B

goal (1 subgoal):
 1. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
case (RTL x B)
[PROOF STATE]
proof (state)
this:
x \<in> carrier
x \<notin> B
basis B
C = fund_circuit x B

goal (1 subgoal):
 1. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier
x \<notin> B
basis B
C = fund_circuit x B
[PROOF STEP]
have "\<exists>!C. circuit C \<and> C \<subseteq> insert x B"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
x \<notin> B
basis B
C = fund_circuit x B

goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x B
[PROOF STEP]
using min_dep_imp_ex1_supset_circuit basisD[of B]
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
x \<notin> B
basis B
C = fund_circuit x B
\<lbrakk>?x \<in> carrier; indep ?X; \<not> indep (insert ?x ?X)\<rbrakk> \<Longrightarrow> \<exists>!C. circuit C \<and> C \<subseteq> insert ?x ?X
basis B \<Longrightarrow> indep B
\<lbrakk>basis B; ?x \<in> carrier - B\<rbrakk> \<Longrightarrow> \<not> indep (insert ?x B)

goal (1 subgoal):
 1. \<exists>!C. circuit C \<and> C \<subseteq> insert x B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>!C. circuit C \<and> C \<subseteq> insert x B

goal (1 subgoal):
 1. \<And>x B. \<lbrakk>x \<in> carrier; x \<notin> B; basis B; C = fund_circuit x B\<rbrakk> \<Longrightarrow> circuit (fund_circuit x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>!C. circuit C \<and> C \<subseteq> insert x B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>!C. circuit C \<and> C \<subseteq> insert x B

goal (1 subgoal):
 1. circuit (fund_circuit x B)
[PROOF STEP]
unfolding fund_circuit_def
[PROOF STATE]
proof (prove)
using this:
\<exists>!C. circuit C \<and> C \<subseteq> insert x B

goal (1 subgoal):
 1. circuit (THE C. circuit C \<and> C \<subseteq> insert x B)
[PROOF STEP]
using theI[of "\<lambda>C. circuit C \<and> C \<subseteq> insert x B"]
[PROOF STATE]
proof (prove)
using this:
\<exists>!C. circuit C \<and> C \<subseteq> insert x B
\<lbrakk>circuit ?a \<and> ?a \<subseteq> insert x B; \<And>xa. circuit xa \<and> xa \<subseteq> insert x B \<Longrightarrow> xa = ?a\<rbrakk> \<Longrightarrow> circuit (THE xa. circuit xa \<and> xa \<subseteq> insert x B) \<and> (THE xa. circuit xa \<and> xa \<subseteq> insert x B) \<subseteq> insert x B

goal (1 subgoal):
 1. circuit (THE C. circuit C \<and> C \<subseteq> insert x B)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
circuit (fund_circuit x B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_circuitI:
  assumes "basis B"
  assumes "x \<in> carrier - B"
  assumes "circuit C"
  assumes "C \<subseteq> insert x B"
  shows "fund_circuit x B = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fund_circuit x B = C
[PROOF STEP]
unfolding fund_circuit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE C. circuit C \<and> C \<subseteq> insert x B) = C
[PROOF STEP]
using assms theI_unique[OF basis_ex1_supset_circuit, of B x C]
[PROOF STATE]
proof (prove)
using this:
basis B
x \<in> carrier - B
circuit C
C \<subseteq> insert x B
\<lbrakk>basis B; x \<in> carrier - B\<rbrakk> \<Longrightarrow> (circuit C \<and> C \<subseteq> insert x B) = (C = (THE C. circuit C \<and> C \<subseteq> insert x B))

goal (1 subgoal):
 1. (THE C. circuit C \<and> C \<subseteq> insert x B) = C
[PROOF STEP]
by auto


[STATEMENT]
lemma fund_circuit_inI_aux: "\<E>.fund_circuit x B = fund_circuit_in \<E> x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.fund_circuit x B = fund_circuit_in \<E> x B
[PROOF STEP]
unfolding fund_circuit_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.fund_circuit x B = \<E>.fund_circuit x B
[PROOF STEP]
by auto


[STATEMENT]
lemma circuit_in_elim:
  assumes "circuit_in \<E> C\<^sub>1" "circuit_in \<E> C\<^sub>2" "C\<^sub>1 \<noteq> C\<^sub>2" "x \<in> C\<^sub>1 \<inter> C\<^sub>2"
  shows "\<exists>C\<^sub>3 \<subseteq> (C\<^sub>1 \<union> C\<^sub>2) - {x}. circuit_in \<E> C\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit_in \<E> C\<^sub>3
[PROOF STEP]
using assms \<E>.circuit_elim
[PROOF STATE]
proof (prove)
using this:
circuit_in \<E> C\<^sub>1
circuit_in \<E> C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
\<lbrakk>\<E>.circuit ?C\<^sub>1; \<E>.circuit ?C\<^sub>2; ?C\<^sub>1 \<noteq> ?C\<^sub>2; ?x \<in> ?C\<^sub>1 \<inter> ?C\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>?C\<^sub>1 \<union> ?C\<^sub>2 - {?x}. \<E>.circuit C\<^sub>3

goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. circuit_in \<E> C\<^sub>3
[PROOF STEP]
unfolding circuit_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.circuit C\<^sub>1
\<E>.circuit C\<^sub>2
C\<^sub>1 \<noteq> C\<^sub>2
x \<in> C\<^sub>1 \<inter> C\<^sub>2
\<lbrakk>\<E>.circuit ?C\<^sub>1; \<E>.circuit ?C\<^sub>2; ?C\<^sub>1 \<noteq> ?C\<^sub>2; ?x \<in> ?C\<^sub>1 \<inter> ?C\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>C\<^sub>3\<subseteq>?C\<^sub>1 \<union> ?C\<^sub>2 - {?x}. \<E>.circuit C\<^sub>3

goal (1 subgoal):
 1. \<exists>C\<^sub>3\<subseteq>C\<^sub>1 \<union> C\<^sub>2 - {x}. \<E>.circuit C\<^sub>3
[PROOF STEP]
by auto


[STATEMENT]
lemma min_dep_in_imp_ex1_supset_circuit_in:
  assumes "x \<in> \<E>"
  assumes "indep_in \<E> X"
  assumes "\<not> indep_in \<E> (insert x X)"
  shows "\<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x X
[PROOF STEP]
using assms \<E>.min_dep_imp_ex1_supset_circuit
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>
indep_in \<E> X
\<not> indep_in \<E> (insert x X)
\<lbrakk>?x \<in> \<E>; indep_in \<E> ?X; \<not> indep_in \<E> (insert ?x ?X)\<rbrakk> \<Longrightarrow> \<exists>!C. \<E>.circuit C \<and> C \<subseteq> insert ?x ?X

goal (1 subgoal):
 1. \<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x X
[PROOF STEP]
unfolding circuit_in_def
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>
indep_in \<E> X
\<not> indep_in \<E> (insert x X)
\<lbrakk>?x \<in> \<E>; indep_in \<E> ?X; \<not> indep_in \<E> (insert ?x ?X)\<rbrakk> \<Longrightarrow> \<exists>!C. \<E>.circuit C \<and> C \<subseteq> insert ?x ?X

goal (1 subgoal):
 1. \<exists>!C. \<E>.circuit C \<and> C \<subseteq> insert x X
[PROOF STEP]
by auto


[STATEMENT]
lemma basis_in_ex1_supset_circuit_in:
  assumes "basis_in \<E> B"
  assumes "x \<in> \<E> - B"
  shows "\<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x B
[PROOF STEP]
using assms \<E>.basis_ex1_supset_circuit
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> B
x \<in> \<E> - B
\<lbrakk>\<E>.basis ?B; ?x \<in> \<E> - ?B\<rbrakk> \<Longrightarrow> \<exists>!C. \<E>.circuit C \<and> C \<subseteq> insert ?x ?B

goal (1 subgoal):
 1. \<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x B
[PROOF STEP]
unfolding circuit_in_def basis_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.basis B
x \<in> \<E> - B
\<lbrakk>\<E>.basis ?B; ?x \<in> \<E> - ?B\<rbrakk> \<Longrightarrow> \<exists>!C. \<E>.circuit C \<and> C \<subseteq> insert ?x ?B

goal (1 subgoal):
 1. \<exists>!C. \<E>.circuit C \<and> C \<subseteq> insert x B
[PROOF STEP]
by auto


[STATEMENT]
lemma fund_circuit_inI:
  assumes "basis_in \<E> B"
  assumes "x \<in> \<E> - B"
  assumes "circuit_in \<E> C"
  assumes "C \<subseteq> insert x B"
  shows "fund_circuit_in \<E> x B = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fund_circuit_in \<E> x B = C
[PROOF STEP]
using assms \<E>.fund_circuitI
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> B
x \<in> \<E> - B
circuit_in \<E> C
C \<subseteq> insert x B
\<lbrakk>\<E>.basis ?B; ?x \<in> \<E> - ?B; \<E>.circuit ?C; ?C \<subseteq> insert ?x ?B\<rbrakk> \<Longrightarrow> \<E>.fund_circuit ?x ?B = ?C

goal (1 subgoal):
 1. fund_circuit_in \<E> x B = C
[PROOF STEP]
unfolding basis_in_def circuit_in_def fund_circuit_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.basis B
x \<in> \<E> - B
\<E>.circuit C
C \<subseteq> insert x B
\<lbrakk>\<E>.basis ?B; ?x \<in> \<E> - ?B; \<E>.circuit ?C; ?C \<subseteq> insert ?x ?B\<rbrakk> \<Longrightarrow> \<E>.fund_circuit ?x ?B = ?C

goal (1 subgoal):
 1. \<E>.fund_circuit x B = C
[PROOF STEP]
by auto


[STATEMENT]
lemma fund_circuit_in_sub_cong:
  assumes "\<E>' \<subseteq> \<E>"
  assumes "x \<in> \<E>' - B"
  assumes "basis_in \<E>' B"
  shows "\<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B
[PROOF STEP]
obtain C where C: "circuit_in \<E>' C" "C \<subseteq> insert x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>circuit_in \<E>' C; C \<subseteq> insert x B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using * assms basis_in_ex1_supset_circuit_in[of \<E>' B x]
[PROOF STATE]
proof (prove)
using this:
\<E> \<subseteq> carrier
\<E>' \<subseteq> \<E>
x \<in> \<E>' - B
basis_in \<E>' B
\<lbrakk>\<E>' \<subseteq> carrier; basis_in \<E>' B; x \<in> \<E>' - B\<rbrakk> \<Longrightarrow> \<exists>!C. circuit_in \<E>' C \<and> C \<subseteq> insert x B

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>circuit_in \<E>' C; C \<subseteq> insert x B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
circuit_in \<E>' C
C \<subseteq> insert x B

goal (1 subgoal):
 1. \<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
circuit_in \<E>' C
C \<subseteq> insert x B
[PROOF STEP]
have "fund_circuit_in \<E>' x B = C"
[PROOF STATE]
proof (prove)
using this:
circuit_in \<E>' C
C \<subseteq> insert x B

goal (1 subgoal):
 1. fund_circuit_in \<E>' x B = C
[PROOF STEP]
using * assms fund_circuit_inI
[PROOF STATE]
proof (prove)
using this:
circuit_in \<E>' C
C \<subseteq> insert x B
\<E> \<subseteq> carrier
\<E>' \<subseteq> \<E>
x \<in> \<E>' - B
basis_in \<E>' B
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?B; ?x \<in> ?\<E> - ?B; circuit_in ?\<E> ?C; ?C \<subseteq> insert ?x ?B\<rbrakk> \<Longrightarrow> fund_circuit_in ?\<E> ?x ?B = ?C

goal (1 subgoal):
 1. fund_circuit_in \<E>' x B = C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fund_circuit_in \<E>' x B = C

goal (1 subgoal):
 1. \<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fund_circuit_in \<E>' x B = C

goal (1 subgoal):
 1. \<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B
[PROOF STEP]
have "\<dots> = \<E>.fund_circuit_in \<E>' x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = \<E>.fund_circuit_in \<E>' x B
[PROOF STEP]
using * assms C \<E>.fund_circuit_inI basis_in_sub_cong[of \<E>] circuit_in_sub_cong[of \<E>]
[PROOF STATE]
proof (prove)
using this:
\<E> \<subseteq> carrier
\<E>' \<subseteq> \<E>
x \<in> \<E>' - B
basis_in \<E>' B
circuit_in \<E>' C
C \<subseteq> insert x B
\<lbrakk>?\<E> \<subseteq> \<E>; \<E>.basis_in ?\<E> ?B; ?x \<in> ?\<E> - ?B; \<E>.circuit_in ?\<E> ?C; ?C \<subseteq> insert ?x ?B\<rbrakk> \<Longrightarrow> \<E>.fund_circuit_in ?\<E> ?x ?B = ?C
\<lbrakk>\<E> \<subseteq> carrier; ?\<E>' \<subseteq> \<E>\<rbrakk> \<Longrightarrow> \<E>.basis_in ?\<E>' ?B = basis_in ?\<E>' ?B
\<lbrakk>\<E> \<subseteq> carrier; ?\<E>' \<subseteq> \<E>\<rbrakk> \<Longrightarrow> \<E>.circuit_in ?\<E>' ?C = circuit_in ?\<E>' ?C

goal (1 subgoal):
 1. C = \<E>.fund_circuit_in \<E>' x B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = \<E>.fund_circuit_in \<E>' x B

goal (1 subgoal):
 1. \<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fund_circuit_in \<E>' x B = \<E>.fund_circuit_in \<E>' x B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fund_circuit_in \<E>' x B = \<E>.fund_circuit_in \<E>' x B

goal (1 subgoal):
 1. \<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_rank_of_eq_upper_rank_of: "lower_rank_of \<E> = upper_rank_of \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of \<E> = upper_rank_of \<E>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of \<E> = upper_rank_of \<E>
[PROOF STEP]
obtain B where "basis_in \<E> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. basis_in \<E> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using basis_in_ex[OF *]
[PROOF STATE]
proof (prove)
using this:
\<exists>B. basis_in \<E> B

goal (1 subgoal):
 1. (\<And>B. basis_in \<E> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_in \<E> B

goal (1 subgoal):
 1. rank_of \<E> = upper_rank_of \<E>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in \<E> B
[PROOF STEP]
have "{card B | B. basis_in \<E> B} = {card B}"
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> B

goal (1 subgoal):
 1. {card B |B. basis_in \<E> B} = {card B}
[PROOF STEP]
by safe (auto dest: basis_in_card[OF *])
[PROOF STATE]
proof (state)
this:
{card B |B. basis_in \<E> B} = {card B}

goal (1 subgoal):
 1. rank_of \<E> = upper_rank_of \<E>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{card B |B. basis_in \<E> B} = {card B}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{card B |B. basis_in \<E> B} = {card B}

goal (1 subgoal):
 1. rank_of \<E> = upper_rank_of \<E>
[PROOF STEP]
unfolding lower_rank_of_def upper_rank_of_def
[PROOF STATE]
proof (prove)
using this:
{card B |B. basis_in \<E> B} = {card B}

goal (1 subgoal):
 1. Min {card B |B. basis_in \<E> B} = Max {card B |B. basis_in \<E> B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of \<E> = upper_rank_of \<E>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_of_eq_card_basis_in:
  assumes "basis_in \<E> B"
  shows "rank_of \<E> = card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of \<E> = card B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of \<E> = card B
[PROOF STEP]
have "{card B | B. basis_in \<E> B} = {card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {card B |B. basis_in \<E> B} = {card B}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> B

goal (1 subgoal):
 1. {card B |B. basis_in \<E> B} = {card B}
[PROOF STEP]
by safe (auto dest: basis_in_card[OF *])
[PROOF STATE]
proof (state)
this:
{card B |B. basis_in \<E> B} = {card B}

goal (1 subgoal):
 1. rank_of \<E> = card B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{card B |B. basis_in \<E> B} = {card B}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{card B |B. basis_in \<E> B} = {card B}

goal (1 subgoal):
 1. rank_of \<E> = card B
[PROOF STEP]
unfolding rank_of_def
[PROOF STATE]
proof (prove)
using this:
{card B |B. basis_in \<E> B} = {card B}

goal (1 subgoal):
 1. Min {card B |B. basis_in \<E> B} = card B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of \<E> = card B

goal:
No subgoals!
[PROOF STEP]
qed