[STATEMENT]
lemma rank_of_indep_in_le:
  assumes "indep_in \<E> X"
  shows "card X \<le> rank_of \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
assume "basis_in \<E> B"
[PROOF STATE]
proof (state)
this:
basis_in \<E> B

goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
basis_in \<E> B

goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
obtain B' where "basis_in \<E> B'" "X \<subseteq> B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B'. \<lbrakk>basis_in \<E> B'; X \<subseteq> B'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms indep_in_imp_subset_basis_in[OF *]
[PROOF STATE]
proof (prove)
using this:
indep_in \<E> X
indep_in \<E> ?X \<Longrightarrow> \<exists>B. basis_in \<E> B \<and> ?X \<subseteq> B

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

goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
basis_in \<E> B
basis_in \<E> B'
X \<subseteq> B'
[PROOF STEP]
have "card X \<le> card B"
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> B
basis_in \<E> B'
X \<subseteq> B'

goal (1 subgoal):
 1. card X \<le> card B
[PROOF STEP]
using card_mono[OF basis_in_finite[OF *]] basis_in_card[OF *, of B B']
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> B
basis_in \<E> B'
X \<subseteq> B'
\<lbrakk>basis_in \<E> ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
\<lbrakk>basis_in \<E> B; basis_in \<E> B'\<rbrakk> \<Longrightarrow> card B = card B'

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

goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
basis_in \<E> ?B2 \<Longrightarrow> card X \<le> card ?B2

goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
basis_in \<E> ?B2 \<Longrightarrow> card X \<le> card ?B2

goal (1 subgoal):
 1. card X \<le> rank_of \<E>
[PROOF STEP]
have "finite {card B | B. basis_in \<E> B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {card B |B. basis_in \<E> B}
[PROOF STEP]
using collect_basis_in_finite[OF *]
[PROOF STATE]
proof (prove)
using this:
finite (Collect (basis_in \<E>))

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

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

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

goal (1 subgoal):
 1. card X \<le> Min {card B |B. basis_in \<E> B}
[PROOF STEP]
using basis_in_ex[OF *]
[PROOF STATE]
proof (prove)
using this:
basis_in \<E> ?B2 \<Longrightarrow> card X \<le> card ?B2
finite {card B |B. basis_in \<E> B}
\<exists>B. basis_in \<E> B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_of_mono:
  assumes "X \<subseteq> Y"
  assumes "Y \<subseteq> carrier"
  shows "rank_of X \<le> rank_of Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
obtain B\<^sub>X where B\<^sub>X: "basis_in X  B\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B\<^sub>X. basis_in X B\<^sub>X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms basis_in_ex[of X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
X \<subseteq> carrier \<Longrightarrow> \<exists>B. basis_in X B

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

goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
basis_in X B\<^sub>X

goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
obtain B\<^sub>Y where B\<^sub>Y: "basis_in Y B\<^sub>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B\<^sub>Y. basis_in Y B\<^sub>Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms basis_in_ex[of Y]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
Y \<subseteq> carrier \<Longrightarrow> \<exists>B. basis_in Y B

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

goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
basis_in Y B\<^sub>Y

goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
have "card B\<^sub>X \<le> card B\<^sub>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card B\<^sub>X \<le> card B\<^sub>Y
[PROOF STEP]
using assms basis_in_indep_in_card[OF _ _ B\<^sub>Y] basis_in_indep_in[OF _ B\<^sub>X] indep_in_subI_subset
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
\<lbrakk>Y \<subseteq> carrier; indep_in Y ?X\<rbrakk> \<Longrightarrow> card ?X \<le> card B\<^sub>Y
X \<subseteq> carrier \<Longrightarrow> indep_in X B\<^sub>X
\<lbrakk>?\<E>' \<subseteq> ?\<E>; indep_in ?\<E>' ?X\<rbrakk> \<Longrightarrow> indep_in ?\<E> ?X

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

goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
basis_in X B\<^sub>X
basis_in Y B\<^sub>Y
card B\<^sub>X \<le> card B\<^sub>Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_in X B\<^sub>X
basis_in Y B\<^sub>Y
card B\<^sub>X \<le> card B\<^sub>Y

goal (1 subgoal):
 1. rank_of X \<le> rank_of Y
[PROOF STEP]
using assms rank_of_eq_card_basis_in
[PROOF STATE]
proof (prove)
using this:
basis_in X B\<^sub>X
basis_in Y B\<^sub>Y
card B\<^sub>X \<le> card B\<^sub>Y
X \<subseteq> Y
Y \<subseteq> carrier
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?B\<rbrakk> \<Longrightarrow> rank_of ?\<E> = card ?B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_of_insert_le:
  assumes "X \<subseteq> carrier"
  assumes "x \<in> carrier"
  shows "rank_of (insert x X) \<le> Suc (rank_of X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
obtain B where B: "basis_in X B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. basis_in X B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms basis_in_ex[of X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
X \<subseteq> carrier \<Longrightarrow> \<exists>B. basis_in X B

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

goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
have "basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
obtain B' where B': "B' \<subseteq> insert x X - X" "basis_in (insert x X) (B \<union> B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B'. \<lbrakk>B' \<subseteq> insert x X - X; basis_in (insert x X) (B \<union> B')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms B basis_in_subI[of "insert x X" X B]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
basis_in X B
\<lbrakk>insert x X \<subseteq> carrier; X \<subseteq> insert x X; insert x X \<subseteq> carrier; basis_in X B\<rbrakk> \<Longrightarrow> \<exists>B'\<subseteq>insert x X - X. basis_in (insert x X) (B \<union> B')

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

goal (1 subgoal):
 1. basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B' \<subseteq> insert x X - X
basis_in (insert x X) (B \<union> B')
[PROOF STEP]
have "B' = {} \<or> B' = {x}"
[PROOF STATE]
proof (prove)
using this:
B' \<subseteq> insert x X - X
basis_in (insert x X) (B \<union> B')

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

goal (1 subgoal):
 1. basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B' = {} \<or> B' = {x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
B' = {} \<or> B' = {x}

goal (1 subgoal):
 1. basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. B' = {} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
 2. B' = {x} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
assume "B' = {}"
[PROOF STATE]
proof (state)
this:
B' = {}

goal (2 subgoals):
 1. B' = {} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
 2. B' = {x} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B' = {}
[PROOF STEP]
have "basis_in (insert x X) B"
[PROOF STATE]
proof (prove)
using this:
B' = {}

goal (1 subgoal):
 1. basis_in (insert x X) B
[PROOF STEP]
using B'
[PROOF STATE]
proof (prove)
using this:
B' = {}
B' \<subseteq> insert x X - X
basis_in (insert x X) (B \<union> B')

goal (1 subgoal):
 1. basis_in (insert x X) B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) B

goal (2 subgoals):
 1. B' = {} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
 2. B' = {x} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in (insert x X) B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) B

goal (1 subgoal):
 1. basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)

goal (1 subgoal):
 1. B' = {x} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B' = {x} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
assume "B' = {x}"
[PROOF STATE]
proof (state)
this:
B' = {x}

goal (1 subgoal):
 1. B' = {x} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B' = {x}
[PROOF STEP]
have "basis_in (insert x X) (insert x B)"
[PROOF STATE]
proof (prove)
using this:
B' = {x}

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B)
[PROOF STEP]
using B'
[PROOF STATE]
proof (prove)
using this:
B' = {x}
B' \<subseteq> insert x X - X
basis_in (insert x X) (B \<union> B')

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) (insert x B)

goal (1 subgoal):
 1. B' = {x} \<Longrightarrow> basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in (insert x X) (insert x B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) (insert x B)

goal (1 subgoal):
 1. basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)

goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)

goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. basis_in (insert x X) B \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
 2. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
assume "basis_in (insert x X) B"
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) B

goal (2 subgoals):
 1. basis_in (insert x X) B \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
 2. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in (insert x X) B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) B

goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
using assms B rank_of_eq_card_basis_in
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) B
X \<subseteq> carrier
x \<in> carrier
basis_in X B
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?B\<rbrakk> \<Longrightarrow> rank_of ?\<E> = card ?B

goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (insert x X) \<le> Suc (rank_of X)

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
assume "basis_in (insert x X) (insert x B)"
[PROOF STATE]
proof (state)
this:
basis_in (insert x X) (insert x B)

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in (insert x X) (insert x B)
[PROOF STEP]
have "rank_of (insert x X) = card (insert x B)"
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) (insert x B)

goal (1 subgoal):
 1. rank_of (insert x X) = card (insert x B)
[PROOF STEP]
using assms rank_of_eq_card_basis_in
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) (insert x B)
X \<subseteq> carrier
x \<in> carrier
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?B\<rbrakk> \<Longrightarrow> rank_of ?\<E> = card ?B

goal (1 subgoal):
 1. rank_of (insert x X) = card (insert x B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (insert x X) = card (insert x B)

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (insert x X) = card (insert x B)

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
have "\<dots> = Suc (card (B - {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert x B) = Suc (card (B - {x}))
[PROOF STEP]
using assms card.insert_remove[of B x]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
finite B \<Longrightarrow> card (insert x B) = Suc (card (B - {x}))

goal (1 subgoal):
 1. card (insert x B) = Suc (card (B - {x}))
[PROOF STEP]
using B basis_in_finite
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
finite B \<Longrightarrow> card (insert x B) = Suc (card (B - {x}))
basis_in X B
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?A\<rbrakk> \<Longrightarrow> finite ?A

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

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (insert x B) = Suc (card (B - {x}))

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
have "\<dots> \<le> Suc (card B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card (B - {x})) \<le> Suc (card B)
[PROOF STEP]
using assms B basis_in_finite card_Diff1_le[of B]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
basis_in X B
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?A\<rbrakk> \<Longrightarrow> finite ?A
card (B - {?x}) \<le> card B

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

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (card (B - {x})) \<le> Suc (card B)

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
have "\<dots> = Suc (rank_of X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card B) = Suc (rank_of X)
[PROOF STEP]
using assms B rank_of_eq_card_basis_in
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
basis_in X B
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?B\<rbrakk> \<Longrightarrow> rank_of ?\<E> = card ?B

goal (1 subgoal):
 1. Suc (card B) = Suc (rank_of X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (card B) = Suc (rank_of X)

goal (1 subgoal):
 1. basis_in (insert x X) (insert x B) \<Longrightarrow> rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of (insert x X) \<le> Suc (rank_of X)

goal (1 subgoal):
 1. rank_of (insert x X) \<le> Suc (rank_of X)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rank_of (insert x X) \<le> Suc (rank_of X)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (insert x X) \<le> Suc (rank_of X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_of_Un_Int_le:
  assumes "X \<subseteq> carrier"
  assumes "Y \<subseteq> carrier"
  shows "rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
obtain B_Int where B_Int: "basis_in (X \<inter> Y) B_Int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B_Int. basis_in (X \<inter> Y) B_Int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms basis_in_ex[of "X \<inter> Y"]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
X \<inter> Y \<subseteq> carrier \<Longrightarrow> \<exists>B. basis_in (X \<inter> Y) B

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

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in (X \<inter> Y) B_Int
[PROOF STEP]
have "indep_in (X \<union> Y) B_Int"
[PROOF STATE]
proof (prove)
using this:
basis_in (X \<inter> Y) B_Int

goal (1 subgoal):
 1. indep_in (X \<union> Y) B_Int
[PROOF STEP]
using assms indep_in_subI_subset[OF _ basis_in_indep_in[of "X \<inter> Y" B_Int], of "X \<union> Y"]
[PROOF STATE]
proof (prove)
using this:
basis_in (X \<inter> Y) B_Int
X \<subseteq> carrier
Y \<subseteq> carrier
\<lbrakk>X \<inter> Y \<subseteq> X \<union> Y; X \<inter> Y \<subseteq> carrier; basis_in (X \<inter> Y) B_Int\<rbrakk> \<Longrightarrow> indep_in (X \<union> Y) B_Int

goal (1 subgoal):
 1. indep_in (X \<union> Y) B_Int
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indep_in (X \<union> Y) B_Int

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in (X \<union> Y) B_Int
[PROOF STEP]
obtain B_Un where B_Un: "basis_in (X \<union> Y) B_Un" "B_Int \<subseteq> B_Un"
[PROOF STATE]
proof (prove)
using this:
indep_in (X \<union> Y) B_Int

goal (1 subgoal):
 1. (\<And>B_Un. \<lbrakk>basis_in (X \<union> Y) B_Un; B_Int \<subseteq> B_Un\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms indep_in_imp_subset_basis_in[of "X \<union> Y" B_Int]
[PROOF STATE]
proof (prove)
using this:
indep_in (X \<union> Y) B_Int
X \<subseteq> carrier
Y \<subseteq> carrier
\<lbrakk>X \<union> Y \<subseteq> carrier; indep_in (X \<union> Y) B_Int\<rbrakk> \<Longrightarrow> \<exists>B. basis_in (X \<union> Y) B \<and> B_Int \<subseteq> B

goal (1 subgoal):
 1. (\<And>B_Un. \<lbrakk>basis_in (X \<union> Y) B_Un; B_Int \<subseteq> B_Un\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_in (X \<union> Y) B_Un
B_Int \<subseteq> B_Un

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) = card ((B_Un \<inter> X) \<union> (B_Un \<inter> Y)) + card ((B_Un \<inter> X) \<inter> (B_Un \<inter> Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) = card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y))
[PROOF STEP]
by (simp add: inf_assoc inf_left_commute inf_sup_distrib1)
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) = card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y))

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) = card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y))

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "\<dots> = card (B_Un \<inter> X) + card (B_Un \<inter> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)
[PROOF STEP]
have "finite (B_Un \<inter> X)" "finite (B_Un \<inter> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (B_Un \<inter> X) &&& finite (B_Un \<inter> Y)
[PROOF STEP]
using assms finite_subset[OF _ carrier_finite]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
?A \<subseteq> carrier \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (B_Un \<inter> X) &&& finite (B_Un \<inter> Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (B_Un \<inter> X)
finite (B_Un \<inter> Y)

goal (1 subgoal):
 1. card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (B_Un \<inter> X)
finite (B_Un \<inter> Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (B_Un \<inter> X)
finite (B_Un \<inter> Y)

goal (1 subgoal):
 1. card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)
[PROOF STEP]
using card_Un_Int[of "B_Un \<inter> X" "B_Un \<inter> Y"]
[PROOF STATE]
proof (prove)
using this:
finite (B_Un \<inter> X)
finite (B_Un \<inter> Y)
\<lbrakk>finite (B_Un \<inter> X); finite (B_Un \<inter> Y)\<rbrakk> \<Longrightarrow> card (B_Un \<inter> X) + card (B_Un \<inter> Y) = card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y))

goal (1 subgoal):
 1. card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X \<union> B_Un \<inter> Y) + card (B_Un \<inter> X \<inter> (B_Un \<inter> Y)) = card (B_Un \<inter> X) + card (B_Un \<inter> Y)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "\<dots> \<le> rank_of X + rank_of Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "card (B_Un \<inter> X) \<le> rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (B_Un \<inter> X) \<le> rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (B_Un \<inter> X) \<le> rank_of X
[PROOF STEP]
have "indep_in X (B_Un \<inter> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in X (B_Un \<inter> X)
[PROOF STEP]
using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
X \<union> Y \<subseteq> carrier \<Longrightarrow> indep_in (X \<union> Y) B_Un
indep_in ?\<E> ?X \<Longrightarrow> indep_in ?\<E>' (?X \<inter> ?\<E>')

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

goal (1 subgoal):
 1. card (B_Un \<inter> X) \<le> rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in X (B_Un \<inter> X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
indep_in X (B_Un \<inter> X)

goal (1 subgoal):
 1. card (B_Un \<inter> X) \<le> rank_of X
[PROOF STEP]
using assms rank_of_indep_in_le
[PROOF STATE]
proof (prove)
using this:
indep_in X (B_Un \<inter> X)
X \<subseteq> carrier
Y \<subseteq> carrier
\<lbrakk>?\<E> \<subseteq> carrier; indep_in ?\<E> ?X\<rbrakk> \<Longrightarrow> card ?X \<le> rank_of ?\<E>

goal (1 subgoal):
 1. card (B_Un \<inter> X) \<le> rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X) \<le> rank_of X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X) \<le> rank_of X

goal (1 subgoal):
 1. card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X) \<le> rank_of X

goal (1 subgoal):
 1. card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "card (B_Un \<inter> Y) \<le> rank_of Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (B_Un \<inter> Y) \<le> rank_of Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (B_Un \<inter> Y) \<le> rank_of Y
[PROOF STEP]
have "indep_in Y (B_Un \<inter> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in Y (B_Un \<inter> Y)
[PROOF STEP]
using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
X \<union> Y \<subseteq> carrier \<Longrightarrow> indep_in (X \<union> Y) B_Un
indep_in ?\<E> ?X \<Longrightarrow> indep_in ?\<E>' (?X \<inter> ?\<E>')

goal (1 subgoal):
 1. indep_in Y (B_Un \<inter> Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indep_in Y (B_Un \<inter> Y)

goal (1 subgoal):
 1. card (B_Un \<inter> Y) \<le> rank_of Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in Y (B_Un \<inter> Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
indep_in Y (B_Un \<inter> Y)

goal (1 subgoal):
 1. card (B_Un \<inter> Y) \<le> rank_of Y
[PROOF STEP]
using assms rank_of_indep_in_le
[PROOF STATE]
proof (prove)
using this:
indep_in Y (B_Un \<inter> Y)
X \<subseteq> carrier
Y \<subseteq> carrier
\<lbrakk>?\<E> \<subseteq> carrier; indep_in ?\<E> ?X\<rbrakk> \<Longrightarrow> card ?X \<le> rank_of ?\<E>

goal (1 subgoal):
 1. card (B_Un \<inter> Y) \<le> rank_of Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> Y) \<le> rank_of Y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> Y) \<le> rank_of Y

goal (1 subgoal):
 1. card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (B_Un \<inter> X) \<le> rank_of X
card (B_Un \<inter> Y) \<le> rank_of Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (B_Un \<inter> X) \<le> rank_of X
card (B_Un \<inter> Y) \<le> rank_of Y

goal (1 subgoal):
 1. card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> X) + card (B_Un \<inter> Y) \<le> rank_of X + rank_of Y

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "rank_of X + rank_of Y \<ge> card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y))"
[PROOF STATE]
proof (prove)
using this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) \<le> rank_of X + rank_of Y

goal (1 subgoal):
 1. card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) \<le> rank_of X + rank_of Y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) \<le> rank_of X + rank_of Y

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) \<le> rank_of X + rank_of Y

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "B_Un \<inter> (X \<union> Y) = B_Un"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B_Un \<inter> (X \<union> Y) = B_Un
[PROOF STEP]
using assms basis_in_subset_carrier[OF _ B_Un(1)]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
X \<union> Y \<subseteq> carrier \<Longrightarrow> B_Un \<subseteq> X \<union> Y

goal (1 subgoal):
 1. B_Un \<inter> (X \<union> Y) = B_Un
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B_Un \<inter> (X \<union> Y) = B_Un

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B_Un \<inter> (X \<union> Y) = B_Un

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "B_Un \<inter> (X \<inter> Y) = B_Int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
have "card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
[PROOF STEP]
have "indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))
[PROOF STEP]
using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
X \<union> Y \<subseteq> carrier \<Longrightarrow> indep_in (X \<union> Y) B_Un
indep_in ?\<E> ?X \<Longrightarrow> indep_in ?\<E>' (?X \<inter> ?\<E>')

goal (1 subgoal):
 1. indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))

goal (1 subgoal):
 1. card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))

goal (1 subgoal):
 1. card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
[PROOF STEP]
using assms basis_in_indep_in_card[of "X \<inter> Y" _ B_Int] B_Int
[PROOF STATE]
proof (prove)
using this:
indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))
X \<subseteq> carrier
Y \<subseteq> carrier
\<lbrakk>X \<inter> Y \<subseteq> carrier; indep_in (X \<inter> Y) ?X; basis_in (X \<inter> Y) B_Int\<rbrakk> \<Longrightarrow> card ?X \<le> card B_Int
basis_in (X \<inter> Y) B_Int

goal (1 subgoal):
 1. card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int

goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int

goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
have "finite (B_Un \<inter> (X \<inter> Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (B_Un \<inter> (X \<inter> Y))
[PROOF STEP]
using assms carrier_finite finite_subset[of "B_Un \<inter> (X \<inter> Y)"]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
finite carrier
\<lbrakk>B_Un \<inter> (X \<inter> Y) \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite (B_Un \<inter> (X \<inter> Y))

goal (1 subgoal):
 1. finite (B_Un \<inter> (X \<inter> Y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (B_Un \<inter> (X \<inter> Y))

goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (B_Un \<inter> (X \<inter> Y))

goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
have "B_Int \<subseteq> B_Un \<inter> (X \<inter> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B_Int \<subseteq> B_Un \<inter> (X \<inter> Y)
[PROOF STEP]
using assms B_Un B_Int basis_in_subset_carrier[of "X \<inter> Y" B_Int]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
basis_in (X \<union> Y) B_Un
B_Int \<subseteq> B_Un
basis_in (X \<inter> Y) B_Int
\<lbrakk>X \<inter> Y \<subseteq> carrier; basis_in (X \<inter> Y) B_Int\<rbrakk> \<Longrightarrow> B_Int \<subseteq> X \<inter> Y

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

goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
finite (B_Un \<inter> (X \<inter> Y))
B_Int \<subseteq> B_Un \<inter> (X \<inter> Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
finite (B_Un \<inter> (X \<inter> Y))
B_Int \<subseteq> B_Un \<inter> (X \<inter> Y)

goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
using card_seteq
[PROOF STATE]
proof (prove)
using this:
card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int
finite (B_Un \<inter> (X \<inter> Y))
B_Int \<subseteq> B_Un \<inter> (X \<inter> Y)
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?B \<le> card ?A\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B_Un \<inter> (X \<inter> Y) = B_Int

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
B_Un \<inter> (X \<inter> Y) = B_Int

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) \<le> rank_of X + rank_of Y
B_Un \<inter> (X \<union> Y) = B_Un
B_Un \<inter> (X \<inter> Y) = B_Int
[PROOF STEP]
have "rank_of X + rank_of Y \<ge> card B_Un + card B_Int"
[PROOF STATE]
proof (prove)
using this:
card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) \<le> rank_of X + rank_of Y
B_Un \<inter> (X \<union> Y) = B_Un
B_Un \<inter> (X \<inter> Y) = B_Int

goal (1 subgoal):
 1. card B_Un + card B_Int \<le> rank_of X + rank_of Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card B_Un + card B_Int \<le> rank_of X + rank_of Y

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card B_Un + card B_Int \<le> rank_of X + rank_of Y

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "card B_Un = rank_of (X \<union> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card B_Un = rank_of (X \<union> Y)
[PROOF STEP]
using assms rank_of_eq_card_basis_in[OF _ B_Un(1)]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
X \<union> Y \<subseteq> carrier \<Longrightarrow> rank_of (X \<union> Y) = card B_Un

goal (1 subgoal):
 1. card B_Un = rank_of (X \<union> Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card B_Un = rank_of (X \<union> Y)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card B_Un = rank_of (X \<union> Y)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
have "card B_Int = rank_of (X \<inter> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card B_Int = rank_of (X \<inter> Y)
[PROOF STEP]
using assms rank_of_eq_card_basis_in[OF _ B_Int]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
Y \<subseteq> carrier
X \<inter> Y \<subseteq> carrier \<Longrightarrow> rank_of (X \<inter> Y) = card B_Int

goal (1 subgoal):
 1. card B_Int = rank_of (X \<inter> Y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card B_Int = rank_of (X \<inter> Y)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card B_Un + card B_Int \<le> rank_of X + rank_of Y
card B_Un = rank_of (X \<union> Y)
card B_Int = rank_of (X \<inter> Y)
[PROOF STEP]
show "rank_of X + rank_of Y \<ge> rank_of (X \<union> Y) + rank_of (X \<inter> Y)"
[PROOF STATE]
proof (prove)
using this:
card B_Un + card B_Int \<le> rank_of X + rank_of Y
card B_Un = rank_of (X \<union> Y)
card B_Int = rank_of (X \<inter> Y)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_of_Un_absorbI:
  assumes "X \<subseteq> carrier" "Y \<subseteq> carrier"
  assumes "\<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X"
  shows "rank_of (X \<union> Y) = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
have "finite (Y - X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Y - X)
[PROOF STEP]
using finite_subset[OF \<open>Y \<subseteq> carrier\<close>] carrier_finite
[PROOF STATE]
proof (prove)
using this:
finite carrier \<Longrightarrow> finite Y
finite carrier

goal (1 subgoal):
 1. finite (Y - X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (Y - X)

goal (1 subgoal):
 1. rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (Y - X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (Y - X)

goal (1 subgoal):
 1. rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite (Y - X)
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
proof (induction "Y - X" arbitrary: Y rule: finite_induct )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Y. \<lbrakk>{} = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
 2. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

goal (2 subgoals):
 1. \<And>Y. \<lbrakk>{} = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
 2. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X
[PROOF STEP]
have "X \<union> Y = X"
[PROOF STATE]
proof (prove)
using this:
{} = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

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

goal (2 subgoals):
 1. \<And>Y. \<lbrakk>{} = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
 2. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<union> Y = X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
X \<union> Y = X

goal (1 subgoal):
 1. rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) = rank_of X

goal (1 subgoal):
 1. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
case (insert y F)
[PROOF STATE]
proof (state)
this:
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

goal (1 subgoal):
 1. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
have "rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
have "rank_of (X \<union> Y) + rank_of X = rank_of ((X \<union> (Y - {y})) \<union> (insert y X)) + rank_of ((X \<union> (Y - {y})) \<inter> (insert y X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X = rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X = rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X)
[PROOF STEP]
have "X \<union> Y = (X \<union> (Y - {y})) \<union> (insert y X)" "X = (X \<union> (Y - {y})) \<inter> (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<union> Y = X \<union> (Y - {y}) \<union> insert y X &&& X = (X \<union> (Y - {y})) \<inter> insert y X
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

goal (1 subgoal):
 1. X \<union> Y = X \<union> (Y - {y}) \<union> insert y X &&& X = (X \<union> (Y - {y})) \<inter> insert y X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<union> Y = X \<union> (Y - {y}) \<union> insert y X
X = (X \<union> (Y - {y})) \<inter> insert y X

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X = rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<union> Y = X \<union> (Y - {y}) \<union> insert y X
X = (X \<union> (Y - {y})) \<inter> insert y X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X \<union> Y = X \<union> (Y - {y}) \<union> insert y X
X = (X \<union> (Y - {y})) \<inter> insert y X

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X = rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) + rank_of X = rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) + rank_of X = rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) + rank_of X = rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
have "\<dots> \<le> rank_of (X \<union> (Y - {y})) +  rank_of (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X) \<le> rank_of (X \<union> (Y - {y})) + rank_of (insert y X)
[PROOF STEP]
proof (rule rank_of_Un_Int_le)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X \<union> (Y - {y}) \<subseteq> carrier
 2. insert y X \<subseteq> carrier
[PROOF STEP]
show "X \<union> (Y - {y}) \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<union> (Y - {y}) \<subseteq> carrier
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

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

goal (1 subgoal):
 1. insert y X \<subseteq> carrier
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert y X \<subseteq> carrier
[PROOF STEP]
show "insert y X \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert y X \<subseteq> carrier
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X) \<le> rank_of (X \<union> (Y - {y})) + rank_of (insert y X)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> (Y - {y}) \<union> insert y X) + rank_of ((X \<union> (Y - {y})) \<inter> insert y X) \<le> rank_of (X \<union> (Y - {y})) + rank_of (insert y X)

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
have "\<dots> = rank_of (X \<union> (Y - {y})) + rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X
[PROOF STEP]
have "y \<in> Y - X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> Y - X
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

goal (1 subgoal):
 1. y \<in> Y - X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Y - X

goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> Y - X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> Y - X

goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
y \<in> Y - X
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> (Y - {y})) + rank_of (insert y X) = rank_of (X \<union> (Y - {y})) + rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
have "\<dots> = rank_of X + rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of X = rank_of X + rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of X = rank_of X + rank_of X
[PROOF STEP]
have "F = (Y - {y}) - X" "Y - {y} \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = Y - {y} - X &&& Y - {y} \<subseteq> carrier
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X

goal (1 subgoal):
 1. F = Y - {y} - X &&& Y - {y} \<subseteq> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = Y - {y} - X
Y - {y} \<subseteq> carrier

goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of X = rank_of X + rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F = Y - {y} - X
Y - {y} \<subseteq> carrier
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F = Y - {y} - X
Y - {y} \<subseteq> carrier

goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of X = rank_of X + rank_of X
[PROOF STEP]
using insert insert(3)[of "Y - {y}"]
[PROOF STATE]
proof (prove)
using this:
F = Y - {y} - X
Y - {y} \<subseteq> carrier
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X
\<lbrakk>F = Y - {y} - X; X \<subseteq> carrier; Y - {y} \<subseteq> carrier; \<And>ya. ya \<in> Y - {y} - X \<Longrightarrow> rank_of (insert ya X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> (Y - {y})) = rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> (Y - {y})) + rank_of X = rank_of X + rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> (Y - {y})) + rank_of X = rank_of X + rank_of X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> (Y - {y})) + rank_of X = rank_of X + rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X

goal (1 subgoal):
 1. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X

goal (1 subgoal):
 1. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
have "rank_of (X \<union> Y) + rank_of X \<ge> rank_of X + rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of X + rank_of X \<le> rank_of (X \<union> Y) + rank_of X
[PROOF STEP]
using insert rank_of_mono
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
\<lbrakk>F = ?Y - X; X \<subseteq> carrier; ?Y \<subseteq> carrier; \<And>y. y \<in> ?Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> ?Y) = rank_of X
insert y F = Y - X
X \<subseteq> carrier
Y \<subseteq> carrier
?y \<in> Y - X \<Longrightarrow> rank_of (insert ?y X) = rank_of X
\<lbrakk>?X \<subseteq> ?Y; ?Y \<subseteq> carrier\<rbrakk> \<Longrightarrow> rank_of ?X \<le> rank_of ?Y

goal (1 subgoal):
 1. rank_of X + rank_of X \<le> rank_of (X \<union> Y) + rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of X + rank_of X \<le> rank_of (X \<union> Y) + rank_of X

goal (1 subgoal):
 1. \<And>x F Y. \<lbrakk>finite F; x \<notin> F; \<And>Y. \<lbrakk>F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X; insert x F = Y - X; X \<subseteq> carrier; Y \<subseteq> carrier; \<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X\<rbrakk> \<Longrightarrow> rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
rank_of X + rank_of X \<le> rank_of (X \<union> Y) + rank_of X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X
rank_of X + rank_of X \<le> rank_of (X \<union> Y) + rank_of X

goal (1 subgoal):
 1. rank_of (X \<union> Y) = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) = rank_of X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (X \<union> Y) = rank_of X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma indep_iff_rank_of:
  assumes "X \<subseteq> carrier"
  shows "indep X \<longleftrightarrow> rank_of X = card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep X = (rank_of X = card X)
[PROOF STEP]
proof (standard, goal_cases LTR RTL)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. indep X \<Longrightarrow> rank_of X = card X
 2. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
case LTR
[PROOF STATE]
proof (state)
this:
indep X

goal (2 subgoals):
 1. indep X \<Longrightarrow> rank_of X = card X
 2. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep X
[PROOF STEP]
have "indep_in X X"
[PROOF STATE]
proof (prove)
using this:
indep X

goal (1 subgoal):
 1. indep_in X X
[PROOF STEP]
by (auto intro: indep_inI)
[PROOF STATE]
proof (state)
this:
indep_in X X

goal (2 subgoals):
 1. indep X \<Longrightarrow> rank_of X = card X
 2. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in X X
[PROOF STEP]
have "basis_in X X"
[PROOF STATE]
proof (prove)
using this:
indep_in X X

goal (1 subgoal):
 1. basis_in X X
[PROOF STEP]
by (auto intro: basis_inI[OF assms])
[PROOF STATE]
proof (state)
this:
basis_in X X

goal (2 subgoals):
 1. indep X \<Longrightarrow> rank_of X = card X
 2. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in X X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
basis_in X X

goal (1 subgoal):
 1. rank_of X = card X
[PROOF STEP]
using rank_of_eq_card_basis_in[OF assms]
[PROOF STATE]
proof (prove)
using this:
basis_in X X
basis_in X ?B \<Longrightarrow> rank_of X = card ?B

goal (1 subgoal):
 1. rank_of X = card X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of X = card X

goal (1 subgoal):
 1. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
case RTL
[PROOF STATE]
proof (state)
this:
rank_of X = card X

goal (1 subgoal):
 1. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
obtain B where B: "basis_in X B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. basis_in X B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using basis_in_ex[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>B. basis_in X B

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

goal (1 subgoal):
 1. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in X B
[PROOF STEP]
have "card B = card X"
[PROOF STATE]
proof (prove)
using this:
basis_in X B

goal (1 subgoal):
 1. card B = card X
[PROOF STEP]
using RTL rank_of_eq_card_basis_in[OF assms]
[PROOF STATE]
proof (prove)
using this:
basis_in X B
rank_of X = card X
basis_in X ?B \<Longrightarrow> rank_of X = card ?B

goal (1 subgoal):
 1. card B = card X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card B = card X

goal (1 subgoal):
 1. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card B = card X
[PROOF STEP]
have "B = X"
[PROOF STATE]
proof (prove)
using this:
card B = card X

goal (1 subgoal):
 1. B = X
[PROOF STEP]
using basis_in_subset_carrier[OF assms B] card_seteq[OF finite_subset[OF assms carrier_finite]]
[PROOF STATE]
proof (prove)
using this:
card B = card X
B \<subseteq> X
\<lbrakk>?A \<subseteq> X; card X \<le> card ?A\<rbrakk> \<Longrightarrow> ?A = X

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

goal (1 subgoal):
 1. rank_of X = card X \<Longrightarrow> indep X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B = X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
B = X

goal (1 subgoal):
 1. indep X
[PROOF STEP]
using basis_in_indep_in[OF assms B] indep_in_indep
[PROOF STATE]
proof (prove)
using this:
B = X
indep_in X B
indep_in ?\<E> ?X \<Longrightarrow> indep ?X

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_iff_rank_of:
  assumes "X \<subseteq> carrier"
  shows "basis X \<longleftrightarrow> rank_of X = card X \<and> rank_of X = rank_of carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis X = (rank_of X = card X \<and> rank_of X = rank_of carrier)
[PROOF STEP]
proof (standard, goal_cases LTR RTL)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. basis X \<Longrightarrow> rank_of X = card X \<and> rank_of X = rank_of carrier
 2. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
case LTR
[PROOF STATE]
proof (state)
this:
basis X

goal (2 subgoals):
 1. basis X \<Longrightarrow> rank_of X = card X \<and> rank_of X = rank_of carrier
 2. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis X
[PROOF STEP]
have "rank_of X = card X"
[PROOF STATE]
proof (prove)
using this:
basis X

goal (1 subgoal):
 1. rank_of X = card X
[PROOF STEP]
using assms indep_iff_rank_of basis_indep
[PROOF STATE]
proof (prove)
using this:
basis X
X \<subseteq> carrier
?X \<subseteq> carrier \<Longrightarrow> indep ?X = (rank_of ?X = card ?X)
basis ?X \<Longrightarrow> indep ?X

goal (1 subgoal):
 1. rank_of X = card X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of X = card X

goal (2 subgoals):
 1. basis X \<Longrightarrow> rank_of X = card X \<and> rank_of X = rank_of carrier
 2. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rank_of X = card X

goal (2 subgoals):
 1. basis X \<Longrightarrow> rank_of X = card X \<and> rank_of X = rank_of carrier
 2. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
have "\<dots> = rank_of carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card X = rank_of carrier
[PROOF STEP]
using LTR rank_of_eq_card_basis_in[of carrier X] basis_iff_basis_in
[PROOF STATE]
proof (prove)
using this:
basis X
\<lbrakk>carrier \<subseteq> carrier; basis_in carrier X\<rbrakk> \<Longrightarrow> rank_of carrier = card X
basis ?B = basis_in carrier ?B

goal (1 subgoal):
 1. card X = rank_of carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card X = rank_of carrier

goal (2 subgoals):
 1. basis X \<Longrightarrow> rank_of X = card X \<and> rank_of X = rank_of carrier
 2. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank_of X = card X
card X = rank_of carrier
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rank_of X = card X
card X = rank_of carrier

goal (1 subgoal):
 1. rank_of X = card X \<and> rank_of X = rank_of carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of X = card X \<and> rank_of X = rank_of carrier

goal (1 subgoal):
 1. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
case RTL
[PROOF STATE]
proof (state)
this:
rank_of X = card X \<and> rank_of X = rank_of carrier

goal (1 subgoal):
 1. rank_of X = card X \<and> rank_of X = rank_of carrier \<Longrightarrow> basis X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis X
[PROOF STEP]
proof (rule basisI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. indep X
 2. \<And>x. x \<in> carrier - X \<Longrightarrow> \<not> indep (insert x X)
[PROOF STEP]
show "indep X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep X
[PROOF STEP]
using assms RTL indep_iff_rank_of
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
rank_of X = card X \<and> rank_of X = rank_of carrier
?X \<subseteq> carrier \<Longrightarrow> indep ?X = (rank_of ?X = card ?X)

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

goal (1 subgoal):
 1. \<And>x. x \<in> carrier - X \<Longrightarrow> \<not> indep (insert x X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier - X \<Longrightarrow> \<not> indep (insert x X)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier - X \<Longrightarrow> \<not> indep (insert x X)
[PROOF STEP]
assume x: "x \<in> carrier - X"
[PROOF STATE]
proof (state)
this:
x \<in> carrier - X

goal (1 subgoal):
 1. \<And>x. x \<in> carrier - X \<Longrightarrow> \<not> indep (insert x X)
[PROOF STEP]
show "\<not> indep (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> indep (insert x X)
[PROOF STEP]
proof (rule ccontr, goal_cases False)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> indep (insert x X) \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<not> indep (insert x X)

goal (1 subgoal):
 1. \<not> \<not> indep (insert x X) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<not> indep (insert x X)
[PROOF STEP]
have "card (insert x X) \<le> rank_of carrier"
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> indep (insert x X)

goal (1 subgoal):
 1. card (insert x X) \<le> rank_of carrier
[PROOF STEP]
using assms x indep_inI rank_of_indep_in_le
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> indep (insert x X)
X \<subseteq> carrier
x \<in> carrier - X
\<lbrakk>?X \<subseteq> ?\<E>; indep ?X\<rbrakk> \<Longrightarrow> indep_in ?\<E> ?X
\<lbrakk>?\<E> \<subseteq> carrier; indep_in ?\<E> ?X\<rbrakk> \<Longrightarrow> card ?X \<le> rank_of ?\<E>

goal (1 subgoal):
 1. card (insert x X) \<le> rank_of carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (insert x X) \<le> rank_of carrier

goal (1 subgoal):
 1. \<not> \<not> indep (insert x X) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (insert x X) \<le> rank_of carrier

goal (1 subgoal):
 1. \<not> \<not> indep (insert x X) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of carrier = card X
[PROOF STEP]
using RTL
[PROOF STATE]
proof (prove)
using this:
rank_of X = card X \<and> rank_of X = rank_of carrier

goal (1 subgoal):
 1. rank_of carrier = card X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of carrier = card X

goal (1 subgoal):
 1. \<not> \<not> indep (insert x X) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (insert x X) \<le> card X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
card (insert x X) \<le> card X

goal (1 subgoal):
 1. False
[PROOF STEP]
using finite_subset[OF assms carrier_finite] x
[PROOF STATE]
proof (prove)
using this:
card (insert x X) \<le> card X
finite X
x \<in> carrier - 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:
\<not> indep (insert x X)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
basis X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma circuit_iff_rank_of:
  assumes "X \<subseteq> carrier"
  shows "circuit X \<longleftrightarrow> X \<noteq> {} \<and> (\<forall>x \<in> X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circuit X = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
proof (standard, goal_cases LTR RTL)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. circuit X \<Longrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
 2. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
case LTR
[PROOF STATE]
proof (state)
this:
circuit X

goal (2 subgoals):
 1. circuit X \<Longrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
 2. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
circuit X
[PROOF STEP]
have "X \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
circuit X

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

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

goal (2 subgoals):
 1. circuit X \<Longrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
 2. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X \<noteq> {}

goal (2 subgoals):
 1. circuit X \<Longrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
 2. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
have indep_remove: "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
assume "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
have "indep (X - {x})"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. indep (X - {x})
[PROOF STEP]
using circuit_min_dep[OF LTR]
[PROOF STATE]
proof (prove)
using this:
x \<in> X
?x \<in> X \<Longrightarrow> indep (X - {?x})

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

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
indep (X - {x})

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
have "X - {x} \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X - {x} \<subseteq> carrier
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
indep (X - {x})
X - {x} \<subseteq> carrier
[PROOF STEP]
show "rank_of (X - {x}) = card (X - {x})"
[PROOF STATE]
proof (prove)
using this:
indep (X - {x})
X - {x} \<subseteq> carrier

goal (1 subgoal):
 1. rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
using indep_iff_rank_of
[PROOF STATE]
proof (prove)
using this:
indep (X - {x})
X - {x} \<subseteq> carrier
?X \<subseteq> carrier \<Longrightarrow> indep ?X = (rank_of ?X = card ?X)

goal (1 subgoal):
 1. rank_of (X - {x}) = card (X - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (X - {x}) = card (X - {x})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = card (X - {?x})

goal (2 subgoals):
 1. circuit X \<Longrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
 2. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = card (X - {?x})

goal (2 subgoals):
 1. circuit X \<Longrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
 2. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
have "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
assume *: "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
have "rank_of X \<le> card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of X \<le> card X
[PROOF STEP]
using assms rank_of_le
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
?\<E> \<subseteq> carrier \<Longrightarrow> rank_of ?\<E> \<le> card ?\<E>

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

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rank_of X \<le> card X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
have "rank_of X \<noteq> card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of X \<noteq> card X
[PROOF STEP]
using assms LTR circuitD indep_iff_rank_of[of X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
circuit X
circuit ?X \<Longrightarrow> ?X \<subseteq> carrier
circuit ?X \<Longrightarrow> \<not> indep ?X
\<lbrakk>circuit ?X; ?x \<in> ?X\<rbrakk> \<Longrightarrow> indep (?X - {?x})
X \<subseteq> carrier \<Longrightarrow> indep X = (rank_of X = card X)

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

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank_of X \<le> card X
rank_of X \<noteq> card X
[PROOF STEP]
have "rank_of X < card X"
[PROOF STATE]
proof (prove)
using this:
rank_of X \<le> card X
rank_of X \<noteq> card X

goal (1 subgoal):
 1. rank_of X < card X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of X < card X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rank_of X < card X
[PROOF STEP]
have "rank_of X \<le> card (X - {x})"
[PROOF STATE]
proof (prove)
using this:
rank_of X < card X

goal (1 subgoal):
 1. rank_of X \<le> card (X - {x})
[PROOF STEP]
using * finite_subset[OF assms] carrier_finite
[PROOF STATE]
proof (prove)
using this:
rank_of X < card X
x \<in> X
finite carrier \<Longrightarrow> finite X
finite carrier

goal (1 subgoal):
 1. rank_of X \<le> card (X - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of X \<le> card (X - {x})

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of X \<le> card (X - {x})

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
have "\<dots> = rank_of (X - {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (X - {x}) = rank_of (X - {x})
[PROOF STEP]
using indep_remove \<open>x \<in> X\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = card (X - {?x})
x \<in> X

goal (1 subgoal):
 1. card (X - {x}) = rank_of (X - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (X - {x}) = rank_of (X - {x})

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank_of X \<le> rank_of (X - {x})
[PROOF STEP]
show "rank_of (X - {x}) = rank_of X"
[PROOF STATE]
proof (prove)
using this:
rank_of X \<le> rank_of (X - {x})

goal (1 subgoal):
 1. rank_of (X - {x}) = rank_of X
[PROOF STEP]
using assms rank_of_mono[of "X - {x}" X]
[PROOF STATE]
proof (prove)
using this:
rank_of X \<le> rank_of (X - {x})
X \<subseteq> carrier
\<lbrakk>X - {x} \<subseteq> X; X \<subseteq> carrier\<rbrakk> \<Longrightarrow> rank_of (X - {x}) \<le> rank_of X

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = rank_of X

goal (2 subgoals):
 1. circuit X \<Longrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
 2. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> {}
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = card (X - {?x})
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = rank_of X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {}
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = card (X - {?x})
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = rank_of X

goal (1 subgoal):
 1. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)

goal (1 subgoal):
 1. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
case RTL
[PROOF STATE]
proof (state)
this:
X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)

goal (1 subgoal):
 1. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
[PROOF STEP]
have "X \<noteq> {}"
    and indep_remove: "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})"
    and dep: "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X"
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)

goal (1 subgoal):
 1. X \<noteq> {} &&& (\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})) &&& (\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<noteq> {}
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = card (X - {?x})
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = rank_of X

goal (1 subgoal):
 1. X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X) \<Longrightarrow> circuit X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circuit X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier

goal (1 subgoal):
 1. circuit X
[PROOF STEP]
proof (rule circuitI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> indep X
 2. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
obtain x where x: "x \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>X \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {}

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

goal (2 subgoals):
 1. \<not> indep X
 2. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
have "rank_of X = card (X - {x})"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. rank_of X = card (X - {x})
[PROOF STEP]
using dep indep_remove
[PROOF STATE]
proof (prove)
using this:
x \<in> X
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = rank_of X
?x \<in> X \<Longrightarrow> rank_of (X - {?x}) = card (X - {?x})

goal (1 subgoal):
 1. rank_of X = card (X - {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of X = card (X - {x})

goal (2 subgoals):
 1. \<not> indep X
 2. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of X = card (X - {x})

goal (2 subgoals):
 1. \<not> indep X
 2. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
have "\<dots> < card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (X - {x}) < card X
[PROOF STEP]
using card_Diff1_less[OF finite_subset[OF assms carrier_finite] x]
[PROOF STATE]
proof (prove)
using this:
card (X - {x}) < card X

goal (1 subgoal):
 1. card (X - {x}) < card X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (X - {x}) < card X

goal (2 subgoals):
 1. \<not> indep X
 2. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank_of X < card X
[PROOF STEP]
show "\<not> indep X"
[PROOF STATE]
proof (prove)
using this:
rank_of X < card X

goal (1 subgoal):
 1. \<not> indep X
[PROOF STEP]
using indep_iff_rank_of[OF assms]
[PROOF STATE]
proof (prove)
using this:
rank_of X < card X
indep X = (rank_of X = card X)

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

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
assume "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> indep (X - {x})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
show "indep (X - {x})"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. indep (X - {x})
[PROOF STEP]
using assms indep_remove[of x] indep_iff_rank_of[of "X - {x}"]
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<subseteq> carrier
x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})
X - {x} \<subseteq> carrier \<Longrightarrow> indep (X - {x}) = (rank_of (X - {x}) = card (X - {x}))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
circuit X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma indep_in_iff_rank_of:
  assumes "X \<subseteq> \<E>"
  shows "indep_in \<E> X \<longleftrightarrow> rank_of X = card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in \<E> X = (rank_of X = card X)
[PROOF STEP]
using assms \<E>.indep_iff_rank_of rank_of_sub_cong[OF * assms]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
?X \<subseteq> \<E> \<Longrightarrow> indep_in \<E> ?X = (\<E>.rank_of ?X = card ?X)
\<E>.rank_of X = rank_of X

goal (1 subgoal):
 1. indep_in \<E> X = (rank_of X = card X)
[PROOF STEP]
by auto


[STATEMENT]
lemma basis_in_iff_rank_of:
  assumes "X \<subseteq> \<E>"
  shows "basis_in \<E> X \<longleftrightarrow> rank_of X = card X \<and> rank_of X = rank_of \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_in \<E> X = (rank_of X = card X \<and> rank_of X = rank_of \<E>)
[PROOF STEP]
using \<E>.basis_iff_rank_of[OF assms] rank_of_sub_cong[OF *] assms
[PROOF STATE]
proof (prove)
using this:
\<E>.basis X = (\<E>.rank_of X = card X \<and> \<E>.rank_of X = \<E>.rank_of \<E>)
?\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'
X \<subseteq> \<E>

goal (1 subgoal):
 1. basis_in \<E> X = (rank_of X = card X \<and> rank_of X = rank_of \<E>)
[PROOF STEP]
unfolding basis_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.basis X = (\<E>.rank_of X = card X \<and> \<E>.rank_of X = \<E>.rank_of \<E>)
?\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'
X \<subseteq> \<E>

goal (1 subgoal):
 1. \<E>.basis X = (rank_of X = card X \<and> rank_of X = rank_of \<E>)
[PROOF STEP]
by auto