[STATEMENT]
lemma circuit_in_iff_rank_of:
  assumes "X \<subseteq> \<E>"
  shows "circuit_in \<E> 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_in \<E> 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 -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. circuit_in \<E> X = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
have "circuit_in \<E> X \<longleftrightarrow> \<E>.circuit X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circuit_in \<E> X = \<E>.circuit X
[PROOF STEP]
unfolding circuit_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.circuit X = \<E>.circuit X
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
circuit_in \<E> X = \<E>.circuit X

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

goal (1 subgoal):
 1. circuit_in \<E> X = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
have "\<dots> \<longleftrightarrow>  X \<noteq> {} \<and> (\<forall>x \<in> X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.circuit X = (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X))
[PROOF STEP]
using \<E>.circuit_iff_rank_of[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<E>.circuit X = (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X))

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

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

goal (1 subgoal):
 1. circuit_in \<E> X = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
have "\<dots> \<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. (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of 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 -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of 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 STATE]
proof (state)
goal (1 subgoal):
 1. (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)) = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)) = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
have "\<E>.rank_of (X - {x}) = rank_of (X - {x})" "\<E>.rank_of X = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of (X - {x}) = rank_of (X - {x}) &&& \<E>.rank_of X = rank_of X
[PROOF STEP]
using assms rank_of_sub_cong[OF *, of "X - {x}"] rank_of_sub_cong[OF *, of X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
X - {x} \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of (X - {x}) = rank_of (X - {x})
X \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of X = rank_of X

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

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

goal (1 subgoal):
 1. (\<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X) = (rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of 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. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of 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 STATE]
proof (state)
this:
(\<E>.rank_of (X - {?x2}) = card (X - {?x2}) \<and> card (X - {?x2}) = \<E>.rank_of X) = (rank_of (X - {?x2}) = card (X - {?x2}) \<and> card (X - {?x2}) = rank_of X)

goal (1 subgoal):
 1. (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)) = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<E>.rank_of (X - {?x2}) = card (X - {?x2}) \<and> card (X - {?x2}) = \<E>.rank_of X) = (rank_of (X - {?x2}) = card (X - {?x2}) \<and> card (X - {?x2}) = rank_of X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<E>.rank_of (X - {?x2}) = card (X - {?x2}) \<and> card (X - {?x2}) = \<E>.rank_of X) = (rank_of (X - {?x2}) = card (X - {?x2}) \<and> card (X - {?x2}) = rank_of X)

goal (1 subgoal):
 1. (X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)) = (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 simp: simp del: card_Diff_insert)
[PROOF STATE]
proof (state)
this:
(X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)) = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(X \<noteq> {} \<and> (\<forall>x\<in>X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)) = (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. circuit_in \<E> X = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
circuit_in \<E> X = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
circuit_in \<E> X = (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. circuit_in \<E> 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 STATE]
proof (state)
this:
circuit_in \<E> X = (X \<noteq> {} \<and> (\<forall>x\<in>X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clI:
  assumes "x \<in> carrier"
  assumes "rank_of (insert x X) = rank_of X"
  shows "x \<in> cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {x \<in> carrier. rank_of (insert x X) = rank_of X}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. x \<in> {x \<in> carrier. rank_of (insert x X) = rank_of X}
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_altdef:
  assumes "X \<subseteq> carrier"
  shows "cl X = \<Union>{Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
assume *: "x \<in> cl X"
[PROOF STATE]
proof (state)
this:
x \<in> cl X

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
have "x \<in> \<Union>{Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?X \<in> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
 2. x \<in> ?X
[PROOF STEP]
show "insert x X \<in> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x X \<in> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> cl X

goal (1 subgoal):
 1. insert x X \<in> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> {x \<in> carrier. rank_of (insert x X) = rank_of X}

goal (1 subgoal):
 1. insert x X \<in> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x X \<in> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. x \<in> insert x X
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> cl X \<Longrightarrow> ?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x2 \<in> cl X \<Longrightarrow> ?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x2 \<in> cl X \<Longrightarrow> ?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
assume *: "x \<in> \<Union>{Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
obtain Y where Y: "x \<in> Y" "Y \<subseteq> carrier" "X \<subseteq> Y" "rank_of Y = rank_of X"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>x \<in> Y; Y \<subseteq> carrier; X \<subseteq> Y; rank_of Y = rank_of X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> Y
Y \<subseteq> carrier
X \<subseteq> Y
rank_of Y = rank_of X

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
have "rank_of (insert x X) = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "rank_of (insert x X) \<le> rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
have "insert x X \<subseteq> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x X \<subseteq> Y
[PROOF STEP]
using Y
[PROOF STATE]
proof (prove)
using this:
x \<in> Y
Y \<subseteq> carrier
X \<subseteq> Y
rank_of Y = rank_of X

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

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

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

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

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

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "rank_of X \<le> rank_of (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of X \<le> rank_of (insert x X)
[PROOF STEP]
using Y
[PROOF STATE]
proof (prove)
using this:
x \<in> Y
Y \<subseteq> carrier
X \<subseteq> Y
rank_of Y = rank_of X

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert x X) = rank_of X
[PROOF STEP]
have "x \<in> cl X"
[PROOF STATE]
proof (prove)
using this:
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
rank_of (insert x X) = rank_of X
x \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
using this:
rank_of (insert x X) = rank_of X
x \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. x \<in> {x \<in> carrier. rank_of (insert x X) = rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> cl X

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X} \<Longrightarrow> ?x2 \<in> cl X

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> cl X \<Longrightarrow> ?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X} \<Longrightarrow> ?x2 \<in> cl X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> cl X \<Longrightarrow> ?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
?x2 \<in> \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X} \<Longrightarrow> ?x2 \<in> cl X

goal (1 subgoal):
 1. cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cl X = \<Union> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_rank_of: "x \<in> cl X \<Longrightarrow> rank_of (insert x X) = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl X \<Longrightarrow> rank_of (insert x X) = rank_of X
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {x \<in> carrier. rank_of (insert x X) = rank_of X} \<Longrightarrow> rank_of (insert x X) = rank_of X
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_subset_carrier: "cl X \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X \<subseteq> carrier
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier. rank_of (insert x X) = rank_of X} \<subseteq> carrier
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_subset:
  assumes "X \<subseteq> carrier"
  shows "X \<subseteq> cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> cl X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier

goal (1 subgoal):
 1. X \<subseteq> cl X
[PROOF STEP]
using insert_absorb[of _ X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
?a \<in> X \<Longrightarrow> insert ?a X = X

goal (1 subgoal):
 1. X \<subseteq> cl X
[PROOF STEP]
by (auto intro!: clI)


[STATEMENT]
lemma cl_mono:
  assumes "X \<subseteq> Y"
  assumes "Y \<subseteq> carrier"
  shows "cl X \<subseteq> cl Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X \<subseteq> cl Y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
assume "x \<in> cl X"
[PROOF STATE]
proof (state)
this:
x \<in> cl X

goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> cl X
[PROOF STEP]
have "x \<in> carrier"
[PROOF STATE]
proof (prove)
using this:
x \<in> cl X

goal (1 subgoal):
 1. x \<in> carrier
[PROOF STEP]
using cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
x \<in> cl X
cl ?X \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
have "insert x X \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x X \<subseteq> carrier
[PROOF STEP]
using assms \<open>x \<in> cl X\<close> cl_subset_carrier[of X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> cl X
cl X \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert x X \<subseteq> carrier
[PROOF STEP]
interpret X_insert: matroid "insert x X" "indep_in (insert x X)"
[PROOF STATE]
proof (prove)
using this:
insert x X \<subseteq> carrier

goal (1 subgoal):
 1. matroid (insert x X) (indep_in (insert x X))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
have "insert x Y \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x Y \<subseteq> carrier
[PROOF STEP]
using assms \<open>x \<in> cl X\<close> cl_subset_carrier[of X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> cl X
cl X \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert x Y \<subseteq> carrier
[PROOF STEP]
interpret Y_insert: matroid "insert x Y" "indep_in (insert x Y)"
[PROOF STATE]
proof (prove)
using this:
insert x Y \<subseteq> carrier

goal (1 subgoal):
 1. matroid (insert x Y) (indep_in (insert x Y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl X \<Longrightarrow> x \<in> cl Y
[PROOF STEP]
show "x \<in> cl Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl Y
[PROOF STEP]
using \<open>x \<in> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier

goal (1 subgoal):
 1. x \<in> cl Y
[PROOF STEP]
proof (rule clI, cases "x \<in> X")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier; x \<in> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
 2. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier; x \<in> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
 2. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
show "rank_of (insert x Y) = rank_of Y"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. rank_of (insert x Y) = rank_of Y
[PROOF STEP]
using assms insert_absorb[of x Y]
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> Y \<Longrightarrow> insert x Y = Y

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> X

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = 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. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
have "basis_in (insert x X) B\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_in (insert x X) B\<^sub>X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_in (insert x X) B\<^sub>X
[PROOF STEP]
have "rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)
[PROOF STEP]
have "rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of X
[PROOF STEP]
using assms B\<^sub>X
            basis_in_subset_carrier[where \<E> = X and X = B\<^sub>X]
            basis_in_iff_rank_of[where \<E> = X and X = B\<^sub>X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
basis_in X B\<^sub>X
\<lbrakk>X \<subseteq> carrier; basis_in X B\<^sub>X\<rbrakk> \<Longrightarrow> B\<^sub>X \<subseteq> X
\<lbrakk>X \<subseteq> carrier; B\<^sub>X \<subseteq> X\<rbrakk> \<Longrightarrow> basis_in X B\<^sub>X = (rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of X)

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

goal (1 subgoal):
 1. rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of X

goal (1 subgoal):
 1. rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)
[PROOF STEP]
using cl_rank_of[OF \<open>x \<in> cl X\<close>]
[PROOF STATE]
proof (prove)
using this:
rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of X
rank_of (insert x X) = rank_of X

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)

goal (1 subgoal):
 1. basis_in (insert x X) B\<^sub>X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)

goal (1 subgoal):
 1. basis_in (insert x X) B\<^sub>X
[PROOF STEP]
using assms basis_in_subset_carrier[OF _ B\<^sub>X] \<open>x \<in> carrier\<close> basis_in_iff_rank_of[of "insert x X" B\<^sub>X]
[PROOF STATE]
proof (prove)
using this:
rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)
X \<subseteq> Y
Y \<subseteq> carrier
X \<subseteq> carrier \<Longrightarrow> B\<^sub>X \<subseteq> X
x \<in> carrier
\<lbrakk>insert x X \<subseteq> carrier; B\<^sub>X \<subseteq> insert x X\<rbrakk> \<Longrightarrow> basis_in (insert x X) B\<^sub>X = (rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X))

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

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
have "indep_in (insert x Y) B\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in (insert x Y) B\<^sub>X
[PROOF STEP]
using assms basis_in_indep_in[OF _ B\<^sub>X] indep_in_subI_subset[of X "insert x Y"]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
X \<subseteq> carrier \<Longrightarrow> indep_in X B\<^sub>X
\<lbrakk>X \<subseteq> insert x Y; indep_in X ?X\<rbrakk> \<Longrightarrow> indep_in (insert x Y) ?X

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in (insert x Y) B\<^sub>X
[PROOF STEP]
obtain B\<^sub>Y where B\<^sub>Y: "basis_in (insert x Y) B\<^sub>Y" "B\<^sub>X \<subseteq> B\<^sub>Y"
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x Y) B\<^sub>X

goal (1 subgoal):
 1. (\<And>B\<^sub>Y. \<lbrakk>basis_in (insert x Y) B\<^sub>Y; B\<^sub>X \<subseteq> B\<^sub>Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms \<open>x \<in> carrier\<close> indep_in_iff_subset_basis_in[of "insert x Y" B\<^sub>X]
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x Y) B\<^sub>X
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> carrier
insert x Y \<subseteq> carrier \<Longrightarrow> indep_in (insert x Y) B\<^sub>X = (\<exists>B. basis_in (insert x Y) B \<and> B\<^sub>X \<subseteq> B)

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
have "basis_in Y B\<^sub>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_in Y B\<^sub>Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_in Y B\<^sub>Y
[PROOF STEP]
have "x \<notin> B\<^sub>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> B\<^sub>Y
[PROOF STEP]
proof (rule ccontr, goal_cases False)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<notin> B\<^sub>Y \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x \<notin> B\<^sub>Y

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

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

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

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

goal (1 subgoal):
 1. indep_in (insert x Y) (insert x B\<^sub>X)
[PROOF STEP]
using assms \<open>x \<in> carrier\<close>
            B\<^sub>Y basis_in_indep_in[where \<E> = "insert x Y" and X = B\<^sub>Y]
            indep_in_subset[where \<E> = "insert x Y" and X = B\<^sub>Y and Y = "insert x B\<^sub>X"]
[PROOF STATE]
proof (prove)
using this:
insert x B\<^sub>X \<subseteq> B\<^sub>Y
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> carrier
basis_in (insert x Y) B\<^sub>Y
B\<^sub>X \<subseteq> B\<^sub>Y
\<lbrakk>insert x Y \<subseteq> carrier; basis_in (insert x Y) B\<^sub>Y\<rbrakk> \<Longrightarrow> indep_in (insert x Y) B\<^sub>Y
\<lbrakk>insert x Y \<subseteq> carrier; indep_in (insert x Y) B\<^sub>Y; insert x B\<^sub>X \<subseteq> B\<^sub>Y\<rbrakk> \<Longrightarrow> indep_in (insert x Y) (insert x B\<^sub>X)

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

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

goal (1 subgoal):
 1. indep_in (insert x X) (insert x B\<^sub>X)
[PROOF STEP]
using assms B\<^sub>X
            basis_in_subset_carrier[where \<E> = X and X = B\<^sub>X]
            indep_in_supI[where \<E> = "insert x Y" and \<E>' = "insert x X" and X = "insert x B\<^sub>X"]
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x Y) (insert x B\<^sub>X)
X \<subseteq> Y
Y \<subseteq> carrier
basis_in X B\<^sub>X
\<lbrakk>X \<subseteq> carrier; basis_in X B\<^sub>X\<rbrakk> \<Longrightarrow> B\<^sub>X \<subseteq> X
\<lbrakk>insert x B\<^sub>X \<subseteq> insert x X; insert x X \<subseteq> insert x Y; indep_in (insert x Y) (insert x B\<^sub>X)\<rbrakk> \<Longrightarrow> indep_in (insert x X) (insert x B\<^sub>X)

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

goal (1 subgoal):
 1. \<not> x \<notin> B\<^sub>Y \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
indep_in (insert x X) (insert x B\<^sub>X)

goal (1 subgoal):
 1. \<not> x \<notin> B\<^sub>Y \<Longrightarrow> False
[PROOF STEP]
have "x \<in> insert x X - B\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> insert x X - B\<^sub>X
[PROOF STEP]
using assms \<open>x \<notin> X\<close> B\<^sub>X basis_in_subset_carrier[where \<E> = X and X = B\<^sub>X]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
x \<notin> X
basis_in X B\<^sub>X
\<lbrakk>X \<subseteq> carrier; basis_in X B\<^sub>X\<rbrakk> \<Longrightarrow> B\<^sub>X \<subseteq> X

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

goal (1 subgoal):
 1. \<not> x \<notin> B\<^sub>Y \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
indep_in (insert x X) (insert x B\<^sub>X)
x \<in> insert x X - B\<^sub>X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x X) (insert x B\<^sub>X)
x \<in> insert x X - B\<^sub>X

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms \<open>x \<in> carrier\<close> \<open>basis_in (insert x X) B\<^sub>X\<close>
            basis_in_max_indep_in[where \<E> = "insert x X" and X = B\<^sub>X and x = x]
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x X) (insert x B\<^sub>X)
x \<in> insert x X - B\<^sub>X
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> carrier
basis_in (insert x X) B\<^sub>X
\<lbrakk>insert x X \<subseteq> carrier; basis_in (insert x X) B\<^sub>X; x \<in> insert x X - B\<^sub>X\<rbrakk> \<Longrightarrow> \<not> indep_in (insert x X) (insert x B\<^sub>X)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<notin> B\<^sub>Y

goal (1 subgoal):
 1. basis_in Y B\<^sub>Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> B\<^sub>Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> B\<^sub>Y

goal (1 subgoal):
 1. basis_in Y B\<^sub>Y
[PROOF STEP]
using assms \<open>x \<in> carrier\<close> B\<^sub>Y basis_in_subset_carrier[of "insert x Y" B\<^sub>Y]
        basis_in_supI[where \<E> = "insert x Y" and \<E>' = Y and B = B\<^sub>Y]
[PROOF STATE]
proof (prove)
using this:
x \<notin> B\<^sub>Y
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> carrier
basis_in (insert x Y) B\<^sub>Y
B\<^sub>X \<subseteq> B\<^sub>Y
\<lbrakk>insert x Y \<subseteq> carrier; basis_in (insert x Y) B\<^sub>Y\<rbrakk> \<Longrightarrow> B\<^sub>Y \<subseteq> insert x Y
\<lbrakk>insert x Y \<subseteq> carrier; B\<^sub>Y \<subseteq> Y; Y \<subseteq> insert x Y; insert x Y \<subseteq> carrier; basis_in (insert x Y) B\<^sub>Y\<rbrakk> \<Longrightarrow> basis_in Y B\<^sub>Y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
basis_in Y B\<^sub>Y

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; x \<notin> X\<rbrakk> \<Longrightarrow> rank_of (insert x Y) = rank_of Y
[PROOF STEP]
show "rank_of (insert x Y) = rank_of Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x Y) = rank_of Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x Y) = rank_of Y
[PROOF STEP]
have "rank_of (insert x Y) = card B\<^sub>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x Y) = card B\<^sub>Y
[PROOF STEP]
using assms \<open>x \<in> carrier\<close> \<open>basis_in (insert x Y) B\<^sub>Y\<close> basis_in_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
Y \<subseteq> carrier
x \<in> carrier
basis_in (insert x Y) B\<^sub>Y
\<lbrakk>?\<E> \<subseteq> carrier; basis_in ?\<E> ?X\<rbrakk> \<Longrightarrow> ?X \<subseteq> ?\<E>

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

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

goal (1 subgoal):
 1. rank_of (insert x Y) = rank_of Y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (insert x Y) = card B\<^sub>Y

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

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

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

goal (1 subgoal):
 1. rank_of (insert x Y) = rank_of Y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert x Y) = rank_of Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of (insert x Y) = rank_of Y

goal (1 subgoal):
 1. rank_of (insert x Y) = rank_of Y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rank_of (insert x Y) = rank_of Y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (insert x Y) = rank_of Y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> cl Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_insert_absorb:
  assumes "X \<subseteq> carrier"
  assumes "x \<in> cl X"
  shows "cl (insert x X) = cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl (insert x X) = cl X
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cl (insert x X) \<subseteq> cl X
 2. cl X \<subseteq> cl (insert x X)
[PROOF STEP]
show "cl (insert x X) \<subseteq> cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl (insert x X) \<subseteq> cl X
[PROOF STEP]
proof (standard, goal_cases elem)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
case (elem y)
[PROOF STATE]
proof (state)
this:
y \<in> cl (insert x X)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> cl (insert x X)
[PROOF STEP]
have *: "x \<in> carrier" "y \<in> carrier"
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x X)

goal (1 subgoal):
 1. x \<in> carrier &&& y \<in> carrier
[PROOF STEP]
using assms cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x X)
X \<subseteq> carrier
x \<in> cl X
cl ?X \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
have "rank_of (insert y X) = rank_of (insert y (insert x X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y X) = rank_of (insert y (insert x X))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert y X) = rank_of (insert y (insert x X))
[PROOF STEP]
have "rank_of (insert y X) \<le> rank_of (insert y (insert x X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y X) \<le> rank_of (insert y (insert x X))
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> cl X
x \<in> carrier
y \<in> carrier

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

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

goal (1 subgoal):
 1. rank_of (insert y X) = rank_of (insert y (insert x X))
[PROOF STEP]
have "rank_of (insert y (insert x X)) = rank_of (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
have "insert y (insert x X) = insert x (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert y (insert x X) = insert x (insert y X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert y (insert x X) = insert x (insert y X)

goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert y (insert x X) = insert x (insert y X)
[PROOF STEP]
have "rank_of (insert y (insert x X)) = rank_of (insert x (insert y X))"
[PROOF STATE]
proof (prove)
using this:
insert y (insert x X) = insert x (insert y X)

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

goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (insert y (insert x X)) = rank_of (insert x (insert y X))

goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
have "\<dots> = rank_of (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
have "cl X \<subseteq> cl (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X \<subseteq> cl (insert y X)
[PROOF STEP]
by (rule cl_mono) (auto simp add: assms \<open>y \<in> carrier\<close>)
[PROOF STATE]
proof (state)
this:
cl X \<subseteq> cl (insert y X)

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cl X \<subseteq> cl (insert y X)
[PROOF STEP]
have "x \<in> cl (insert y X)"
[PROOF STATE]
proof (prove)
using this:
cl X \<subseteq> cl (insert y X)

goal (1 subgoal):
 1. x \<in> cl (insert y X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cl X \<subseteq> cl (insert y X)
X \<subseteq> carrier
x \<in> cl X

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

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> cl (insert y X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> cl (insert y X)

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> carrier. rank_of (insert x (insert y X)) = rank_of (insert y X)}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (insert x (insert y X)) = rank_of (insert y X)

goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of (insert y (insert x X)) = rank_of (insert y X)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (insert y (insert x X)) = rank_of (insert y X)

goal (1 subgoal):
 1. rank_of (insert y X) = rank_of (insert y (insert x X))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert y X) \<le> rank_of (insert y (insert x X))
rank_of (insert y (insert x X)) = rank_of (insert y X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of (insert y X) \<le> rank_of (insert y (insert x X))
rank_of (insert y (insert x X)) = rank_of (insert y X)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (insert y X) = rank_of (insert y (insert x X))

goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (insert y X) = rank_of (insert y (insert x X))

goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
have "\<dots> = rank_of (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert x X)
[PROOF STEP]
using elem
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x X)

goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert x X)
[PROOF STEP]
using cl_rank_of
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x X)
?x \<in> cl ?X \<Longrightarrow> rank_of (insert ?x ?X) = rank_of ?X

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (insert y (insert x X)) = rank_of (insert x X)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
have "\<dots> = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
using assms cl_rank_of
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> cl X
?x \<in> cl ?X \<Longrightarrow> rank_of (insert ?x ?X) = rank_of ?X

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> cl (insert x X) \<Longrightarrow> xa \<in> cl X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert y X) = rank_of X
[PROOF STEP]
show "y \<in> cl X"
[PROOF STATE]
proof (prove)
using this:
rank_of (insert y X) = rank_of X

goal (1 subgoal):
 1. y \<in> cl X
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
rank_of (insert y X) = rank_of X
x \<in> carrier
y \<in> carrier

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

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

goal (1 subgoal):
 1. cl X \<subseteq> cl (insert x X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X \<subseteq> cl (insert x X)
[PROOF STEP]
have "insert x X \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x X \<subseteq> carrier
[PROOF STEP]
using assms cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> cl X
cl ?X \<subseteq> carrier

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

goal (1 subgoal):
 1. cl X \<subseteq> cl (insert x X)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert x X \<subseteq> carrier

goal (1 subgoal):
 1. cl X \<subseteq> cl (insert x X)
[PROOF STEP]
have "X \<subseteq> insert x X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> insert x X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> cl X

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

goal (1 subgoal):
 1. cl X \<subseteq> cl (insert x X)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert x X \<subseteq> carrier
X \<subseteq> insert x X
[PROOF STEP]
show "cl X \<subseteq> cl (insert x X)"
[PROOF STATE]
proof (prove)
using this:
insert x X \<subseteq> carrier
X \<subseteq> insert x X

goal (1 subgoal):
 1. cl X \<subseteq> cl (insert x X)
[PROOF STEP]
using assms cl_subset_carrier cl_mono
[PROOF STATE]
proof (prove)
using this:
insert x X \<subseteq> carrier
X \<subseteq> insert x X
X \<subseteq> carrier
x \<in> cl X
cl ?X \<subseteq> carrier
\<lbrakk>?X \<subseteq> ?Y; ?Y \<subseteq> carrier\<rbrakk> \<Longrightarrow> cl ?X \<subseteq> cl ?Y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_cl_absorb:
  assumes "X \<subseteq> carrier"
  shows "cl (cl X) = cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl (cl X) = cl X
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cl (cl X) \<subseteq> cl X
 2. cl X \<subseteq> cl (cl X)
[PROOF STEP]
show "cl (cl X) \<subseteq> cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl (cl X) \<subseteq> cl X
[PROOF STEP]
proof (standard, goal_cases elem)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl (cl X) \<Longrightarrow> x \<in> cl X
[PROOF STEP]
case (elem x)
[PROOF STATE]
proof (state)
this:
x \<in> cl (cl X)

goal (1 subgoal):
 1. \<And>x. x \<in> cl (cl X) \<Longrightarrow> x \<in> cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> cl (cl X)
[PROOF STEP]
have "x \<in> carrier"
[PROOF STATE]
proof (prove)
using this:
x \<in> cl (cl X)

goal (1 subgoal):
 1. x \<in> carrier
[PROOF STEP]
using cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
x \<in> cl (cl X)
cl ?X \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>x. x \<in> cl (cl X) \<Longrightarrow> x \<in> cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier

goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
proof (rule clI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "rank_of (insert x X) \<ge> rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of X \<le> rank_of (insert x X)
[PROOF STEP]
using assms \<open>x \<in> carrier\<close> rank_of_mono[of X "insert x X"]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
\<lbrakk>X \<subseteq> insert x X; insert x X \<subseteq> carrier\<rbrakk> \<Longrightarrow> rank_of X \<le> rank_of (insert x X)

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

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "rank_of (insert x X) \<le> rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
have "rank_of (insert x X) \<le> rank_of (insert x (cl X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of (insert x (cl X))
[PROOF STEP]
using assms \<open>x \<in> carrier\<close> cl_subset_carrier cl_subset[of X]
                rank_of_mono[of "insert x X" "insert x (cl X)"]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
cl ?X \<subseteq> carrier
X \<subseteq> carrier \<Longrightarrow> X \<subseteq> cl X
\<lbrakk>insert x X \<subseteq> insert x (cl X); insert x (cl X) \<subseteq> carrier\<rbrakk> \<Longrightarrow> rank_of (insert x X) \<le> rank_of (insert x (cl X))

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

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

goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
have "\<dots> = rank_of (cl X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x (cl X)) = rank_of (cl X)
[PROOF STEP]
using elem cl_rank_of
[PROOF STATE]
proof (prove)
using this:
x \<in> cl (cl X)
?x \<in> cl ?X \<Longrightarrow> rank_of (insert ?x ?X) = rank_of ?X

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

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

goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
have "\<dots> = rank_of (X \<union> (cl X - X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (cl X) = rank_of (X \<union> (cl X - X))
[PROOF STEP]
using Diff_partition[OF cl_subset[OF assms]]
[PROOF STATE]
proof (prove)
using this:
X \<union> (cl X - X) = cl X

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

goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank_of (cl X) = rank_of (X \<union> (cl X - X))

goal (1 subgoal):
 1. rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
have "\<dots> = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (X \<union> (cl X - X)) = rank_of X
[PROOF STEP]
using \<open>X \<subseteq> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier

goal (1 subgoal):
 1. rank_of (X \<union> (cl X - X)) = rank_of X
[PROOF STEP]
proof (rule rank_of_Un_absorbI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cl X - X \<subseteq> carrier
 2. \<And>y. y \<in> cl X - X - X \<Longrightarrow> rank_of (insert y X) = rank_of X
[PROOF STEP]
show "cl X - X \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X - X \<subseteq> carrier
[PROOF STEP]
using assms cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
cl ?X \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>y. y \<in> cl X - X - X \<Longrightarrow> rank_of (insert y X) = rank_of X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> cl X - X - X \<Longrightarrow> rank_of (insert y X) = rank_of X
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> cl X - X - X \<Longrightarrow> rank_of (insert y X) = rank_of X
[PROOF STEP]
assume "y \<in> cl X - X - X"
[PROOF STATE]
proof (state)
this:
y \<in> cl X - X - X

goal (1 subgoal):
 1. \<And>y. y \<in> cl X - X - X \<Longrightarrow> rank_of (insert y X) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> cl X - X - X
[PROOF STEP]
show "rank_of (insert y X) = rank_of X"
[PROOF STATE]
proof (prove)
using this:
y \<in> cl X - X - X

goal (1 subgoal):
 1. rank_of (insert y X) = rank_of X
[PROOF STEP]
unfolding cl_def
[PROOF STATE]
proof (prove)
using this:
y \<in> {x \<in> carrier. rank_of (insert x X) = rank_of X} - X - X

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

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

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

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

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank_of X \<le> rank_of (insert x X)
rank_of (insert x X) \<le> rank_of X
[PROOF STEP]
show "rank_of (insert x X) = rank_of X"
[PROOF STATE]
proof (prove)
using this:
rank_of X \<le> rank_of (insert x X)
rank_of (insert x X) \<le> rank_of X

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> cl X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cl (cl X) \<subseteq> cl X

goal (1 subgoal):
 1. cl X \<subseteq> cl (cl X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl X \<subseteq> cl (cl X)
[PROOF STEP]
show "cl X \<subseteq> cl (cl X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl X \<subseteq> cl (cl X)
[PROOF STEP]
using cl_subset[OF cl_subset_carrier]
[PROOF STATE]
proof (prove)
using this:
cl ?X1 \<subseteq> cl (cl ?X1)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_augment:
  assumes "X \<subseteq> carrier"
  assumes "x \<in> carrier"
  assumes "y \<in> cl (insert x X) - cl X"
  shows "x \<in> cl (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl (insert y X)
[PROOF STEP]
using \<open>x \<in> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier

goal (1 subgoal):
 1. x \<in> cl (insert y X)
[PROOF STEP]
proof (rule clI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
have "rank_of (insert y X) \<le> rank_of (insert x (insert y X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y X) \<le> rank_of (insert x (insert y X))
[PROOF STEP]
using assms cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
y \<in> cl (insert x X) - cl X
cl ?X \<subseteq> carrier

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

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

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
have "rank_of (insert x (insert y X)) \<le> rank_of (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x (insert y X)) \<le> rank_of (insert y X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x (insert y X)) \<le> rank_of (insert y X)
[PROOF STEP]
have "rank_of (insert x (insert y X)) = rank_of (insert y (insert x X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y (insert x X))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y (insert x X))
[PROOF STEP]
have "insert x (insert y X) = insert y (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x (insert y X) = insert y (insert x X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x (insert y X) = insert y (insert x X)

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y (insert x X))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert x (insert y X) = insert y (insert x X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insert x (insert y X) = insert y (insert x X)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rank_of (insert x (insert y X)) = rank_of (insert y (insert x X))

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

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) \<le> rank_of (insert y X)
[PROOF STEP]
have "rank_of (insert y (insert x X)) = rank_of (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y (insert x X)) = rank_of (insert x X)
[PROOF STEP]
using assms cl_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
y \<in> cl (insert x X) - cl X
cl ?X \<equiv> {x \<in> carrier. rank_of (insert x ?X) = rank_of ?X}

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

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

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) \<le> rank_of (insert y X)
[PROOF STEP]
have "\<dots> \<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]
using assms cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
y \<in> cl (insert x X) - cl X
cl ?X \<subseteq> carrier

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

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

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) \<le> rank_of (insert y X)
[PROOF STEP]
have "\<dots> = rank_of (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (rank_of X) = rank_of (insert y X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc (rank_of X) = rank_of (insert y X)
[PROOF STEP]
have "rank_of (insert y X) \<le> Suc (rank_of X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y X) \<le> Suc (rank_of X)
[PROOF STEP]
using assms cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
y \<in> cl (insert x X) - cl X
cl ?X \<subseteq> carrier

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

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

goal (1 subgoal):
 1. Suc (rank_of X) = rank_of (insert y X)
[PROOF STEP]
have "rank_of (insert y X) \<noteq> rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert y X) \<noteq> rank_of X
[PROOF STEP]
using assms cl_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
y \<in> cl (insert x X) - cl X
cl ?X \<equiv> {x \<in> carrier. rank_of (insert x ?X) = rank_of ?X}

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

goal (1 subgoal):
 1. Suc (rank_of X) = rank_of (insert y X)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rank_of (insert y X) \<noteq> rank_of X

goal (1 subgoal):
 1. Suc (rank_of X) = rank_of (insert y X)
[PROOF STEP]
have "rank_of X \<le> rank_of (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of X \<le> rank_of (insert y X)
[PROOF STEP]
using assms cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier
x \<in> carrier
y \<in> cl (insert x X) - cl X
cl ?X \<subseteq> carrier

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

goal (1 subgoal):
 1. Suc (rank_of X) = rank_of (insert y X)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert y X) \<le> Suc (rank_of X)
rank_of (insert y X) \<noteq> rank_of X
rank_of X \<le> rank_of (insert y X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank_of (insert y X) \<le> Suc (rank_of X)
rank_of (insert y X) \<noteq> rank_of X
rank_of X \<le> rank_of (insert y X)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc (rank_of X) = rank_of (insert y X)

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

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

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

goal (1 subgoal):
 1. rank_of (insert x (insert y X)) = rank_of (insert y X)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank_of (insert y X) \<le> rank_of (insert x (insert y X))
rank_of (insert x (insert y X)) \<le> rank_of (insert y X)
[PROOF STEP]
show "rank_of (insert x (insert y X)) = rank_of (insert y X)"
[PROOF STATE]
proof (prove)
using this:
rank_of (insert y X) \<le> rank_of (insert x (insert y X))
rank_of (insert x (insert y X)) \<le> rank_of (insert y X)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clI_insert:
  assumes "x \<in> carrier"
  assumes "indep X"
  assumes "\<not> indep (insert x X)"
  shows "x \<in> cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
using \<open>x \<in> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier

goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
proof (rule clI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have *: "X \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> carrier
[PROOF STEP]
using assms indep_subset_carrier
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
indep X
\<not> indep (insert x X)
indep ?X \<Longrightarrow> ?X \<subseteq> carrier

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> carrier
[PROOF STEP]
have **: "insert x X \<subseteq> carrier"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier

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

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "indep_in (insert x X) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in (insert x X) X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier
indep X
\<not> indep (insert x X)

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indep_in (insert x X) X
[PROOF STEP]
obtain B where B: "basis_in (insert x X) B" "X \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x X) X

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>basis_in (insert x X) B; X \<subseteq> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms indep_in_iff_subset_basis_in[OF **]
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x X) X
x \<in> carrier
indep X
\<not> indep (insert x X)
indep_in (insert x X) ?X = (\<exists>B. basis_in (insert x X) B \<and> ?X \<subseteq> B)

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "x \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> B
[PROOF STEP]
proof (rule ccontr, goal_cases False)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<notin> B \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x \<notin> B

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

goal (1 subgoal):
 1. indep_in (insert x X) (insert x X)
[PROOF STEP]
using B indep_in_subset[OF ** basis_in_indep_in[OF **]]
[PROOF STATE]
proof (prove)
using this:
\<not> x \<notin> B
basis_in (insert x X) B
X \<subseteq> B
\<lbrakk>basis_in (insert x X) ?X; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> indep_in (insert x X) ?Y

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms indep_in_indep
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x X) (insert x X)
x \<in> carrier
indep X
\<not> indep (insert x X)
indep_in ?\<E> ?X \<Longrightarrow> indep ?X

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

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "basis_in X B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_in X B
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier

goal (1 subgoal):
 1. basis_in X B
[PROOF STEP]
proof (rule basis_inI, goal_cases indep max_indep)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. indep_in X B
 2. \<And>x. x \<in> X - B \<Longrightarrow> \<not> indep_in X (insert x B)
[PROOF STEP]
case indep
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. indep_in X B
 2. \<And>x. x \<in> X - B \<Longrightarrow> \<not> indep_in X (insert x B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in X B
[PROOF STEP]
proof (rule indep_in_supI[where \<E> = "insert x X"])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. B \<subseteq> X
 2. X \<subseteq> insert x X
 3. indep_in (insert x X) B
[PROOF STEP]
show "B \<subseteq> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> X
[PROOF STEP]
using B basis_in_subset_carrier[OF **] \<open>x \<notin> B\<close>
[PROOF STATE]
proof (prove)
using this:
basis_in (insert x X) B
X \<subseteq> B
basis_in (insert x X) ?X \<Longrightarrow> ?X \<subseteq> insert x X
x \<notin> B

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

goal (2 subgoals):
 1. X \<subseteq> insert x X
 2. indep_in (insert x X) B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X \<subseteq> insert x X
 2. indep_in (insert x X) B
[PROOF STEP]
show "indep_in (insert x X) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in (insert x X) B
[PROOF STEP]
using basis_in_indep_in[OF ** B(1)]
[PROOF STATE]
proof (prove)
using this:
indep_in (insert x X) B

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

goal (1 subgoal):
 1. X \<subseteq> insert x X
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
indep_in X B

goal (1 subgoal):
 1. \<And>x. x \<in> X - B \<Longrightarrow> \<not> indep_in X (insert x B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X - B \<Longrightarrow> \<not> indep_in X (insert x B)
[PROOF STEP]
case (max_indep y)
[PROOF STATE]
proof (state)
this:
y \<in> X - B

goal (1 subgoal):
 1. \<And>x. x \<in> X - B \<Longrightarrow> \<not> indep_in X (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> X - B
[PROOF STEP]
have "\<not> indep_in (insert x X) (insert y B)"
[PROOF STATE]
proof (prove)
using this:
y \<in> X - B

goal (1 subgoal):
 1. \<not> indep_in (insert x X) (insert y B)
[PROOF STEP]
using B basis_in_max_indep_in[OF **]
[PROOF STATE]
proof (prove)
using this:
y \<in> X - B
basis_in (insert x X) B
X \<subseteq> B
\<lbrakk>basis_in (insert x X) ?X; ?x \<in> insert x X - ?X\<rbrakk> \<Longrightarrow> \<not> indep_in (insert x X) (insert ?x ?X)

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

goal (1 subgoal):
 1. \<And>x. x \<in> X - B \<Longrightarrow> \<not> indep_in X (insert x B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> indep_in (insert x X) (insert y B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> indep_in (insert x X) (insert y B)

goal (1 subgoal):
 1. \<not> indep_in X (insert y B)
[PROOF STEP]
by (auto intro: indep_in_subI_subset)
[PROOF STATE]
proof (state)
this:
\<not> indep_in X (insert y B)

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

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
basis_in X B
[PROOF STEP]
show "rank_of (insert x X) = rank_of X"
[PROOF STATE]
proof (prove)
using this:
basis_in X B

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma indep_in_carrier [simp]: "indep_in carrier = indep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_in carrier = indep
[PROOF STEP]
using indep_subset_carrier
[PROOF STATE]
proof (prove)
using this:
indep ?X \<Longrightarrow> ?X \<subseteq> carrier

goal (1 subgoal):
 1. indep_in carrier = indep
[PROOF STEP]
by (auto simp: indep_in_def fun_eq_iff)


[STATEMENT]
lemma I_mono: "I Y" if "Y \<subseteq> X" "I X" for X Y :: "'a set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I Y
[PROOF STEP]
have "\<forall>x\<in>Y. x \<notin> cl (Y - {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>Y. x \<notin> cl (Y - {x})
[PROOF STEP]
proof (intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<notin> cl (Y - {x})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<notin> cl (Y - {x})
[PROOF STEP]
assume x: "x \<in> Y"
[PROOF STATE]
proof (state)
this:
x \<in> Y

goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<notin> cl (Y - {x})
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> X
I X
x \<in> Y
[PROOF STEP]
have "cl (Y - {x}) \<subseteq> cl (X - {x})"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> X
I X
x \<in> Y

goal (1 subgoal):
 1. cl (Y - {x}) \<subseteq> cl (X - {x})
[PROOF STEP]
by (intro cl_mono) (auto simp: I_def)
[PROOF STATE]
proof (state)
this:
cl (Y - {x}) \<subseteq> cl (X - {x})

goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<notin> cl (Y - {x})
[PROOF STEP]
with that and x
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> X
I X
x \<in> Y
cl (Y - {x}) \<subseteq> cl (X - {x})
[PROOF STEP]
show "x \<notin> cl (Y - {x})"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> X
I X
x \<in> Y
cl (Y - {x}) \<subseteq> cl (X - {x})

goal (1 subgoal):
 1. x \<notin> cl (Y - {x})
[PROOF STEP]
by (auto simp: I_def)
[PROOF STATE]
proof (state)
this:
x \<notin> cl (Y - {x})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>Y. x \<notin> cl (Y - {x})

goal (1 subgoal):
 1. I Y
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> X
I X
\<forall>x\<in>Y. x \<notin> cl (Y - {x})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> X
I X
\<forall>x\<in>Y. x \<notin> cl (Y - {x})

goal (1 subgoal):
 1. I Y
[PROOF STEP]
by (auto simp: I_def)
[PROOF STATE]
proof (state)
this:
I Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clI':
  assumes "I X" "x \<in> carrier" "\<not>I (insert x X)"
  shows   "x \<in> cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
I X
x \<in> carrier
\<not> I (insert x X)
[PROOF STEP]
have x: "x \<notin> X"
[PROOF STATE]
proof (prove)
using this:
I X
x \<in> carrier
\<not> I (insert x X)

goal (1 subgoal):
 1. x \<notin> X
[PROOF STEP]
by (auto simp: insert_absorb)
[PROOF STATE]
proof (state)
this:
x \<notin> X

goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
I X
x \<in> carrier
\<not> I (insert x X)
[PROOF STEP]
obtain y where y: "y \<in> insert x X" "y \<in> cl (insert x X - {y})"
[PROOF STATE]
proof (prove)
using this:
I X
x \<in> carrier
\<not> I (insert x X)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> insert x X; y \<in> cl (insert x X - {y})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp: I_def)
[PROOF STATE]
proof (state)
this:
y \<in> insert x X
y \<in> cl (insert x X - {y})

goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
show "x \<in> cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> x \<in> cl X
 2. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> x \<in> cl X
 2. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. x \<in> cl X
[PROOF STEP]
using assms x y
[PROOF STATE]
proof (prove)
using this:
x = y
I X
x \<in> carrier
\<not> I (insert x X)
x \<notin> X
y \<in> insert x X
y \<in> cl (insert x X - {y})

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

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
have "y \<in> cl (insert x X - {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> cl (insert x X - {y})
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
y \<in> cl (insert x X - {y})

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<in> cl (insert x X - {y})

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
[PROOF STEP]
have "insert x X - {y} = insert x (X - {y})"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

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

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y \<in> cl (insert x (X - {y}))
[PROOF STEP]
have "y \<in> cl (insert x (X - {y})) - cl (X - {y})"
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x (X - {y}))

goal (1 subgoal):
 1. y \<in> cl (insert x (X - {y})) - cl (X - {y})
[PROOF STEP]
using assms False y
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x (X - {y}))
I X
x \<in> carrier
\<not> I (insert x X)
x \<noteq> y
y \<in> insert x X
y \<in> cl (insert x X - {y})

goal (1 subgoal):
 1. y \<in> cl (insert x (X - {y})) - cl (X - {y})
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x (X - {y}))
X \<subseteq> carrier \<and> (\<forall>x\<in>X. x \<notin> cl (X - {x}))
x \<in> carrier
\<not> (insert x X \<subseteq> carrier \<and> (\<forall>xa\<in>insert x X. xa \<notin> cl (insert x X - {xa})))
x \<noteq> y
y \<in> insert x X
y \<in> cl (insert x X - {y})

goal (1 subgoal):
 1. y \<in> cl (insert x (X - {y})) - cl (X - {y})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> cl (insert x (X - {y})) - cl (X - {y})

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
hence "x \<in> cl (insert y (X - {y}))"
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x (X - {y})) - cl (X - {y})

goal (1 subgoal):
 1. x \<in> cl (insert y (X - {y}))
[PROOF STEP]
using cl_augment[of "X - {y}" x y] assms False y
[PROOF STATE]
proof (prove)
using this:
y \<in> cl (insert x (X - {y})) - cl (X - {y})
\<lbrakk>X - {y} \<subseteq> carrier; x \<in> carrier; y \<in> cl (insert x (X - {y})) - cl (X - {y})\<rbrakk> \<Longrightarrow> x \<in> cl (insert y (X - {y}))
I X
x \<in> carrier
\<not> I (insert x X)
x \<noteq> y
y \<in> insert x X
y \<in> cl (insert x X - {y})

goal (1 subgoal):
 1. x \<in> cl (insert y (X - {y}))
[PROOF STEP]
by (auto simp: I_def)
[PROOF STATE]
proof (state)
this:
x \<in> cl (insert y (X - {y}))

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<in> cl (insert y (X - {y}))

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
from y and False
[PROOF STATE]
proof (chain)
picking this:
y \<in> insert x X
y \<in> cl (insert x X - {y})
x \<noteq> y
[PROOF STEP]
have "insert y (X - {y}) = X"
[PROOF STATE]
proof (prove)
using this:
y \<in> insert x X
y \<in> cl (insert x X - {y})
x \<noteq> y

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

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> x \<in> cl X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> cl X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> cl X

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> cl X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_inI_aux: "x \<in> \<E>.cl X \<Longrightarrow> x \<in> cl_in \<E> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<E>.cl X \<Longrightarrow> x \<in> cl_in \<E> X
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<E>.cl X \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_inD_aux: "x \<in> cl_in \<E> X \<Longrightarrow> x \<in> \<E>.cl X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl_in \<E> X \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<E>.cl X \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_inI:
  assumes "X \<subseteq> \<E>"
  assumes "x \<in> \<E>"
  assumes "rank_of (insert x X) = rank_of X"
  shows "x \<in> cl_in \<E> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl_in \<E> X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> cl_in \<E> X
[PROOF STEP]
have "\<E>.rank_of (insert x X) = rank_of (insert x X)" "\<E>.rank_of X = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = rank_of (insert x X) &&& \<E>.rank_of X = rank_of X
[PROOF STEP]
using assms rank_of_sub_cong[OF *]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> \<E>
rank_of (insert x X) = rank_of X
?\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'

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

goal (1 subgoal):
 1. x \<in> cl_in \<E> X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<E>.rank_of (insert x X) = rank_of (insert x X)
\<E>.rank_of X = rank_of X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<E>.rank_of (insert x X) = rank_of (insert x X)
\<E>.rank_of X = rank_of X

goal (1 subgoal):
 1. x \<in> cl_in \<E> X
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.rank_of (insert x X) = rank_of (insert x X)
\<E>.rank_of X = rank_of X

goal (1 subgoal):
 1. x \<in> \<E>.cl X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<E>.rank_of (insert x X) = rank_of (insert x X)
\<E>.rank_of X = rank_of X
X \<subseteq> \<E>
x \<in> \<E>
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. x \<in> \<E>.cl X
[PROOF STEP]
by (auto intro: \<E>.clI)
[PROOF STATE]
proof (state)
this:
x \<in> cl_in \<E> X

goal:
No subgoals!
[PROOF STEP]
qed