Up to index of Isabelle/HOL/HOL-Algebra/Vector_Spaces
theory Dimensiontheory Dimension
imports Basis
begin
section{*Dimension*}
context finite_dimensional_vector_space
begin
text{*Now we are going to prove that every basis of a finite vector space has the same cardinality than any other
basis.*}
(*
definition funcion_intercambio :: "('c iset × 'c iset)
=> ('c iset × 'c iset)"
where "funcion_intercambio A = (remove_iset (fst A) 0, if ( ((snd(fst A) 0)) ∈ fst(snd A) ) then
insert_iset (remove_iset (snd A) (obtain_position ((snd(fst A) 0)) (snd A) )) (snd(fst A) 0) 0
else
remove_ld (insert_iset (snd A) ((snd(fst A) 0)) 0))"
*)
text{*First of all, we are going to define a function that remove the first element of an iset. We will use
the function @{term remove_iset}. Note that this redefinition is essential: we can not iterate @{term remove_iset}
because is @{text remove_iset}: $\colon iset \times \mathbb{N} \to iset$*}
definition remove_iset_0 :: "'e iset => 'e iset"
where "remove_iset_0 A = remove_iset A 0"
text{*A property about this function and the empty set: *}
lemma remove_iset_empty:
shows "fst (remove_iset_0 ({},f))={}"
unfolding remove_iset_0_def remove_iset_def
by simp
text{*Now the definition of the function by means of we are going to prove the theorem.*}
definition swap_function :: "('c iset × 'c iset)
=> ('c iset × 'c iset)"
where "swap_function A = (remove_iset_0 (fst A),
if (((snd(fst A) 0)) ∈ fst(snd A) ) then
insert_iset (remove_iset (snd A)
(obtain_position ((snd(fst A) 0)) (snd A))) (snd(fst A) 0) 0
else
remove_ld (insert_iset (snd A) ((snd(fst A) 0)) 0))"
text{*From this, we will prove some basic properties that @{term swap_function} satisfies.*}
text{*The set of the first component of the result is finite:*}
lemma finite_fst_swap_function:
assumes indexing_A: "indexing (A,f)"
shows "finite (iset_to_set(fst(swap_function ((A,f),(B,g)))))"
proof -
have finite_A: "finite A" using indexing_finite[OF indexing_A] .
thus ?thesis unfolding swap_function_def remove_iset_0_def remove_iset_def by simp
qed
text{*The set of the first component of the result is in the carrier:*}
lemma swap_function_fst_in_carrier:
assumes A_in_V: "A ⊆ carrier V"
shows "iset_to_set(fst(swap_function ((A,f),(B,g)))) ⊆ carrier V"
using A_in_V
unfolding swap_function_def remove_iset_0_def remove_iset_def by auto
text{*If the first set is not empty, then the set of the first component of the result is contained (strictly) in it.*}
lemma fst_swap_function_subset_fst:
assumes indexing_A: "indexing (A,f)"
and A_not_empty: "A≠{}" --"INDISPENSABLE: IF NOT THE EMPTY CASE WILL NOT BE STRICT"
shows "iset_to_set(fst(swap_function ((A,f),(B,g)))) ⊂ A"
proof -
have "0∈{..<card A}" using A_not_empty and indexing_finite[OF indexing_A]
by (metis card_gt_0_iff lessThan_iff)
hence "f 0 ∈ A" using indexing_A unfolding indexing_def bij_betw_def by auto
thus ?thesis
unfolding swap_function_def remove_iset_0_def remove_iset_def
by auto
qed
text{*If we not demand that content be strict, then the result is trivial.*}
lemma fst_swap_function_subseteq_fst:
shows "iset_to_set(fst(swap_function ((A,f),(B,g)))) ⊆ A"
unfolding swap_function_def remove_iset_0_def remove_iset_def
by auto
text{*We are goint to prove that the set of the second component of the result is
a @{text good_set}. To prove it we will make use of @{thm good_set_insert_remove[no_vars]}.*}
lemma swap_function_snd_good_set:
assumes B_in_V: "B ⊆ carrier V"
and A_in_V: "A ⊆ carrier V"
and A_not_empty: "A≠{}"
and indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
shows "good_set (iset_to_set(snd(swap_function ((A,f),(B,g)))))"
proof (unfold swap_function_def, simp, rule conjI)
have cb_A: "good_set A" using A_in_V indexing_finite[OF indexing_A] unfolding good_set_def by simp
have cb_B: "good_set B" using B_in_V indexing_finite[OF indexing_B] unfolding good_set_def by simp
show "f 0 ∈ B --> good_set (fst (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0))"
proof
assume f0_in_B: "f 0 ∈ B"
show "good_set (fst (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0))"
using good_set_insert_remove[OF B_in_V A_in_V A_not_empty indexing_A indexing_B f0_in_B] .
qed
show "f 0 ∉ B --> good_set (fst (remove_ld (insert_iset (B, g) (f 0) 0)))"
proof
assume f0_notin_B: "f 0 ∉ B"
have "good_set (fst (remove_ld ((fst(insert_iset (B, g) (f 0) 0)), snd (insert_iset (B, g) (f 0) 0))))"
proof (rule remove_ld_good_set)
show "good_set (fst (insert_iset (B, g) (f 0) 0))"
proof (rule insert_iset_good_set)
show "f 0 ∉ B" using f0_notin_B .
show "indexing (B, g)" using indexing_B .
show "f 0 ∈ carrier V" using f0_in_V[OF indexing_A A_in_V A_not_empty] .
show "good_set B" using cb_B .
qed
show "indexing (fst (insert_iset (B, g) (f 0) 0), snd (insert_iset (B, g) (f 0) 0))"
using insert_iset_indexing[OF indexing_B f0_notin_B _] by auto
qed
thus "good_set (fst (remove_ld (insert_iset (B, g) (f 0) 0)))" by simp
qed
qed
corollary swap_function_snd_in_carrier:
assumes B_in_V: "B ⊆ carrier V"
and A_in_V: "A ⊆ carrier V"
and A_not_empty: "A≠{}"
and indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
shows "(iset_to_set(snd(swap_function ((A,f),(B,g))))) ⊆ carrier V"
using swap_function_snd_good_set assms unfolding good_set_def by simp
text{*If the first set is independent, our function will preserve it.*}
lemma fst_swap_function_preserves_li:
assumes li_A: "linear_independent A"
shows "linear_independent (iset_to_set(fst(swap_function ((A,f),(B,g)))))"
unfolding swap_function_def remove_iset_0_def and remove_iset_def
using independent_set_implies_independent_subset[of "A-{f 0}",OF _ li_A] by auto
text{*If the first element of the iset (A,f) is in B, the function will preserve the second set (but it will have changed
the indexation, putting that element in first position of B).*}
lemma swap_function_preserves_B_if_fst_element_of_A_in_B:
assumes f0_in_B: "f 0 ∈B"
and indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
shows "iset_to_set(snd(swap_function ((A,f),(B,g))))=B"
unfolding swap_function_def using f0_in_B apply simp
unfolding insert_iset_def remove_iset_def obtain_position_def apply auto
proof -
assume gn_not_f0: "g (THE n. g n = f 0 ∧ n < card B) ≠ f 0"
let ?P = "(λn. g n = f 0 ∧ n < card B)"
have exK: "(∃!k. ?P k)" using exists_n_and_is_unique_obtain_position[OF f0_in_B indexing_B] .
have ex_THE: "?P (THE k. ?P k)"
using theI' [OF exK] .
def n≡"(THE k. ?P k)"
have "g n = f 0" unfolding n_def
by (metis ex_THE)
thus False using gn_not_f0 unfolding n_def by contradiction
qed
text{*This is an auxiliar lemma which says that if we insert an element into a spanning set, the result will be
a linearly dependent set. We will need this result to assure the existence of the element to remove of the second
set using the function @{term swap_function} through the theorem
@{thm linear_dependent_set_sorted_contains_linear_combination[no_vars]}*}
lemma linear_dependent_insert_spanning_set:
assumes f0_notin_B: "f 0 ∉ B"
and indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A ≠ {}" -- "Essential to cardinality"
and sg_B: "spanning_set B"
shows "linear_dependent (iset_to_set (insert_iset (B,g) (f 0) 0))"
proof (cases "linear_dependent B")
case True show ?thesis
proof (rule linear_dependent_subset_implies_linear_dependent_set)
show "B ⊆ iset_to_set (insert_iset (B, g) (f (0)) 0)" unfolding insert_iset_def iset_to_set_def by auto
show "good_set (iset_to_set (insert_iset (B, g) (f (0)) 0))"
unfolding insert_iset_def iset_to_set_def good_set_def
using A_in_V B_in_V indexing_finite[OF indexing_A] indexing_finite[OF indexing_B]
and f0_in_V[OF indexing_A A_in_V A_not_empty] by simp
show "linear_dependent B" using True .
qed
next
case False show ?thesis unfolding insert_iset_def apply simp
proof (rule lc1)
show li_B: "linear_independent B"
using not_dependent_implies_independent[OF _ False]
unfolding good_set_def
using B_in_V indexing_finite[OF indexing_B] by simp
show "f 0 ∈ carrier V" using f0_in_V[OF indexing_A A_in_V A_not_empty] .
show "f 0 ∉ B" using f0_notin_B .
show "∃fa. fa ∈ coefficients_function (carrier V) ∧ linear_combination fa B = f 0"
using sg_B and f0_in_V[OF indexing_A A_in_V A_not_empty]
unfolding spanning_set_def by blast
qed
qed
text{*This result is similar to @{text linear_dependent_insert_spanning_set} but using sets directly, not isets.*}
lemma spanning_set_insert:
assumes sg_B: "spanning_set B"
and finite_B: "finite B"
and B_in_V: "B ⊆ carrier V"
and a_in_V: "a ∈ carrier V"
shows "spanning_set (insert a B)"
proof (unfold spanning_set_def, auto)
show "good_set (insert a B)" using finite_B B_in_V a_in_V unfolding good_set_def by fast
next
fix x
assume x_in_V: "x ∈ carrier V"
from this obtain f where cf_f: "f ∈ coefficients_function (carrier V)" and lc_B: "linear_combination f B = x"
using sg_B unfolding spanning_set_def by blast
show "∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f (insert a B) = x"
proof -
def g≡"(λx. if x ∈ B then f x else \<zero>)"
have "linear_combination f B = linear_combination g (B ∪ {a})"
proof (unfold g_def, rule eq_lc_when_out_of_set_is_zero[symmetric])
show "good_set {a}" using a_in_V unfolding good_set_def by fast
show "good_set B" using finite_B B_in_V unfolding good_set_def by blast
show "f ∈ coefficients_function (carrier V)" using cf_f .
qed
also have "...=linear_combination g (insert a B)" using arg_cong2 by simp
finally have lc_Ba: "x=linear_combination g (insert a B)" using lc_B by simp
have "g ∈ coefficients_function (carrier V)" unfolding g_def using coefficients_function_g_f_null[of "f" "B"] cf_f by auto
thus ?thesis using lc_Ba by auto
qed
qed
text{*Our function will preserve that the second term is a @{text spanning_set}.*}
lemma swap_function_preserves_sg:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and B_in_V: "B⊆carrier V"
and A_not_empty: "A≠{}" -- "Essential to cardinality"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "spanning_set (iset_to_set(snd(swap_function ((A,f),(B,g)))))"
proof (cases "f 0 ∈ B")
case True show ?thesis
using swap_function_preserves_B_if_fst_element_of_A_in_B [OF True indexing_A indexing_B] sg_B
by simp
next
case False thus ?thesis
proof (unfold swap_function_def, simp)
have A_in_V: "A ⊆ carrier V"
by (metis good_set_def li_A linear_independent_def)
show "spanning_set (fst (remove_ld (insert_iset (B, g) (f 0) 0)))"
proof -
have "span (fst (remove_ld (insert_iset (B, g) (f 0) 0)))=span (iset_to_set (insert_iset (B, g) (f 0) 0))"
proof -
have 1: "linear_dependent (fst (insert_iset (B, g) (f 0) 0))"
using linear_dependent_insert_spanning_set[OF False indexing_A indexing_B A_in_V B_in_V A_not_empty sg_B]
by simp
have 2: "\<zero>\<^bsub>V\<^esub> ∉ fst (insert_iset (B, g) (f 0) 0)" using f0_not_zero[OF indexing_A li_A A_not_empty] zero_notin_B
unfolding insert_iset_def by simp
have 3:"indexing (fst (insert_iset (B, g) (f 0) 0), snd (insert_iset (B, g) (f 0) 0))"
unfolding insert_iset_def apply simp
using surjective_pairing
and insert_iset_indexing[OF indexing_B False _] unfolding insert_iset_def by auto
show ?thesis
using remove_ld_preserves_span[of "fst (insert_iset (B, g) (f 0) 0)" "snd (insert_iset (B, g) (f 0) 0)" ]
using surjective_pairing[of "insert_iset (B, g) (f 0) 0"] 1 2 3 by auto
qed
also have "...=carrier V"
proof (rule spanning_set_implies_span_basis)
show "spanning_set(iset_to_set (insert_iset (B, g) (f 0) 0))"
unfolding insert_iset_def
using spanning_set_insert[OF sg_B indexing_finite[OF indexing_B] B_in_V
f0_in_V[OF indexing_A A_in_V A_not_empty]] by simp
qed
finally have "span (fst (remove_ld (insert_iset (B, g) (f 0) 0)))=carrier V" .
thus ?thesis
proof (rule span_basis_implies_spanning_set)
show "good_set (fst (remove_ld (insert_iset (B, g) (f 0) 0)))"
by (metis A_in_V A_not_empty B_in_V f0_in_V finite.insertI finite_subset
fst_conv good_set_def indexing_A indexing_B indexing_finite insert_iset_def
insert_subset iset_to_set_def remove_ld_monotone remove_ld_preserves_carrier)
qed
qed
qed
qed
text{*@{text swap_function} preserves the cardinality of the second iset.*}
lemma snd_swap_function_preserves_card:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A ≠ {}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "card (iset_to_set (snd (swap_function ((A,f),(B,g))))) = card B"
proof (cases "f 0 ∈ B")
case True thus ?thesis
using swap_function_preserves_B_if_fst_element_of_A_in_B[OF True indexing_A indexing_B] by presburger
next
case False thus ?thesis
proof (unfold swap_function_def, simp)
have A_in_V: "A ⊆ carrier V"
by (metis good_set_in_carrier l_ind_good_set li_A)
have eq_card: "card (iset_to_set (insert_iset (B, g) (f 0) 0))= card B + 1"
using insert_iset_increase_card[OF indexing_B False] .
have zero_notin_insert: "\<zero>\<^bsub>V\<^esub> ∉ (iset_to_set (insert_iset (B, g) (f 0) 0))"
using f0_not_zero[OF indexing_A li_A A_not_empty] and zero_notin_B
unfolding insert_iset_def by simp
have "card (fst (remove_ld (insert_iset (B, g) (f 0) 0)))= card (iset_to_set (insert_iset (B, g) (f 0) 0)) - 1"
using surjective_pairing
using remove_ld_decr_card[OF linear_dependent_insert_spanning_set
[OF False indexing_A indexing_B A_in_V B_in_V A_not_empty sg_B] zero_notin_insert ]
by (metis eq_card False Suc_eq_plus1 diff_Suc_1 fst_conv
indexing_B insert_iset_def insert_iset_indexing iset_to_set_def le0)
also have "...= (card B + 1) - 1" using eq_card
by presburger
finally show "card (fst (remove_ld (insert_iset (B, g) (f 0) 0))) = card B" by simp
qed
qed
text{*Next lemmas shows us how our function decreases the cardinality of the first term.*}
lemma fst_swap_function_decr_card:
assumes indexing_A: "indexing (A,f)"
shows "card (iset_to_set(fst(swap_function ((A,f),(B,g))))) = card A - 1"
proof (cases "A={}")
case True show ?thesis unfolding swap_function_def remove_iset_0_def remove_iset_def using True by auto
next
case False note A_not_empty=False
show ?thesis
proof (unfold swap_function_def, unfold remove_iset_0_def, unfold remove_iset_def, simp)
have "card A > 0" using A_not_empty indexing_finite[OF indexing_A] card_gt_0_iff by metis
hence "0∈{..<card A}" by fast
hence "f 0 ∈ A" using indexing_A unfolding indexing_def bij_betw_def by auto
thus "card (A - {f 0}) = card A - Suc 0"
by (metis One_nat_def `0 < card A` card_Diff_singleton card_infinite less_zeroE)
qed
qed
text{*Now we are going to prove that exists an element of the second iset such that if we apply the @{text swap_function},
the second term will be able to be writen as the second set removing that element and adding the first element of
the first set.*}
text{*We will prove it by cases, first the case that B is not empty*}
lemma swap_function_exists_y_in_B_not_empty:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A ≠ {}"
and B_not_empty: "B ≠ {}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "∃y∈B. iset_to_set (snd(swap_function ((A,f),(B,g)))) = (insert (f 0) (B-{y}))"
unfolding swap_function_def
proof (simp,auto)
show "f 0 ∈ B ==> ∃y∈B. fst (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0)
= insert (f 0) (B - {y})"
using swap_function_preserves_B_if_fst_element_of_A_in_B[OF _ indexing_A indexing_B]
unfolding swap_function_def by auto
show "f 0 ∉ B ==> ∃y∈B. fst (remove_ld (insert_iset (B, g) (f 0) 0)) = insert (f 0) (B - {y})"
proof -
assume f0_notin_B: "f 0 ∉ B"
--"Usaré el teorema: " thm descomposicion_remove_ld
have finite_B: "finite B" using indexing_finite[OF indexing_B] .
have A_in_V: "A ⊆ carrier V"
by (metis good_set_in_carrier l_ind_good_set li_A)
have "insert_iset (B, g) (f 0) 0=(fst (insert_iset (B, g) (f 0) 0,snd (insert_iset (B, g) (f 0) 0)))"
using surjective_pairing by simp
also have "...=({f 0} ∪ B,snd (insert_iset (B, g) (f 0) 0))" unfolding insert_iset_def by simp
finally have eq_pairing: "insert_iset (B, g) (f 0) 0 = ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))" .
hence "fst (remove_ld (insert_iset (B, g) (f 0) 0))=fst(remove_ld ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0)))"
by simp
hence indexing_insert: "indexing ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))"
using insert_iset_indexing [OF indexing_B f0_notin_B _] using eq_pairing by auto
have "∃y. fst (remove_ld ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))) = {f 0} ∪ (B - {y}) ∧ y ∈ B ∧
snd (remove_ld ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))) ` ({..<card {f 0} + card (B - {y})} - {..<card {f 0}})
= B - {y} ∧ snd (remove_ld ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))) ` {..<card {f 0}} = {f 0}
∧ indexing ({f 0} ∪ (B - {y}), snd (remove_ld ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))))"
proof (rule descomposicion_remove_ld)
show "indexing ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))" using indexing_insert .
show "B ≠ {}" using B_not_empty .
show "snd (insert_iset (B, g) (f 0) 0) ` {..<card {f 0}} = {f 0}" unfolding insert_iset_def indexing_ext_def by auto
show "snd (insert_iset (B, g) (f 0) 0) ` ({..<card {f 0} + card B} - {..<card {f 0}}) = B"
unfolding insert_iset_def indexing_ext_def
unfolding image_def
proof (auto)
show "!!xa. [|xa < Suc (card B); g (xa - Suc 0) ∉ B|] ==> xa = 0"
proof (rule FalseE)
fix xa
assume xa_l_cardB1: "xa < Suc (card B)" and gx_notin_B: "g (xa - Suc 0) ∉ B"
have surj: "g `{..<card B}=B" using indexing_B unfolding indexing_def bij_betw_def by simp
have "(xa - Suc 0) ∈ {..< card B}" using xa_l_cardB1
by (metis B_not_empty card_eq_0_iff diff_Suc_less finite_B gr0I lessThan_iff less_antisym less_imp_diff_less)
hence "g (xa - Suc 0) ∈ B" using surj by fast
thus False using gx_notin_B by contradiction
qed
show "!!x. x ∈ B ==> ∃xa∈{..<Suc (card B)} - {..<Suc 0}. x = g (xa - Suc 0)"
proof -
fix x
assume x_in_B: "x∈B"
have surj: "g `{..<card B}=B" using indexing_B unfolding indexing_def bij_betw_def by simp
hence "∃y∈{..<card B}. g y = x" using x_in_B unfolding image_def by force
from this obtain y where y_l_card: "y ∈ {..<card B}" and gy_x: "g y = x" by fast
show "∃xa∈{..<Suc (card B)} - {..<Suc 0}. x = g (xa - Suc 0)"
proof (rule bexI[of _ "y + Suc 0"])
show "x = g (y + Suc 0 - Suc 0)" using gy_x by simp
show "y + Suc 0 ∈ {..<Suc (card B)} - {..<Suc 0}" using y_l_card by simp
qed
qed
qed
show "linear_independent {f 0}"
using unipuntual_is_li[OF f0_in_V[OF indexing_A A_in_V A_not_empty]
f0_not_zero[OF indexing_A li_A A_not_empty]] .
show "\<zero>\<^bsub>V\<^esub> ∉ {f 0} ∪ B" using f0_not_zero[OF indexing_A li_A A_not_empty] and zero_notin_B by simp
show "linear_dependent ({f 0} ∪ B)"
proof -
have eq_iset: "iset_to_set (insert_iset (B, g) (f 0) 0)= {f 0} ∪ B" apply simp
by (metis fst_conv insert_iset_def iset_to_set_def)
have "linear_dependent (iset_to_set (insert_iset (B, g) (f 0) 0))"
using linear_dependent_insert_spanning_set[OF f0_notin_B indexing_A indexing_B A_in_V B_in_V
A_not_empty sg_B] .
thus ?thesis using eq_iset by simp
qed
show "{f 0} ∩ B = {}" using f0_notin_B by fast
qed
from this obtain y where
eq_remove: "fst (remove_ld ({f 0} ∪ B, snd (insert_iset (B, g) (f 0) 0))) = {f 0} ∪ (B - {y})" and y_in_B: " y ∈ B"
by metis
show ?thesis using eq_remove and y_in_B eq_pairing by auto
qed
qed
text{*And now the case that B is empty. It is an inconsistent case: if @{term B} is empty and a spanning set, then the
vector space is @{text "{\<zero>\<^bsub>V\<^esub>}"}. A is not empty, so @{text "A={\<zero>\<^bsub>V\<^esub>}"}. However, we will have a contradiction: @{term A} will be dependent
(@{text "{\<zero>\<^bsub>V\<^esub>}"} is dependent) and also independent (by hypothesis).*}
lemma swap_function_exists_y_in_B_empty:
assumes indexing_A: "indexing (A,f)"
and A_not_empty: "A≠{}"
and B_empty: "B={}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
shows "∃y∈B. iset_to_set (snd(swap_function ((A,f),(B,g)) ))=(insert (f 0) (B-{y}))"
by (metis A_not_empty B_empty Un_absorb1 Un_empty_right good_set_in_carrier
empty_set_is_linearly_independent l_ind_good_set li_A sg_B span_V_eq_spanning_set
span_empty subset_insert zero_not_in_linear_independent_set)
lemma swap_function_exists_y_in_B:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "∃y∈B. iset_to_set (snd(swap_function ((A,f),(B,g)) ))=(insert (f 0) (B-{y}))"
proof (cases "B={}")
case True show ?thesis using swap_function_exists_y_in_B_empty[OF indexing_A A_not_empty True li_A sg_B] .
next
case False show ?thesis
using swap_function_exists_y_in_B_not_empty[OF indexing_A indexing_B B_in_V
A_not_empty False li_A sg_B zero_notin_B] .
qed
text{*From this we can obtain a corollary: @{term "\<zero>\<^bsub>V\<^esub>"} is not in the second term of the result of applying @{text "swap_function"}
to a @{text spanning_set}.*}
corollary zero_notin_snd_swap_function:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd(swap_function ((A,f),(B,g))))"
using swap_function_exists_y_in_B[OF indexing_A indexing_B B_in_V A_not_empty li_A sg_B zero_notin_B]
using f0_not_zero[OF indexing_A li_A A_not_empty] using zero_notin_B by force
text{*The first term of the result of applying @{text swap_function} is an indexing.*}
lemma fst_swap_function_indexing:
assumes indexing_A: "indexing (A,f)"
and A_in_V: "A ⊆ carrier V"
shows "indexing (fst(swap_function ((A,f),(B,g))))"
proof (cases "A={}")
case True show ?thesis using True unfolding swap_function_def remove_iset_0_def remove_iset_def
using indexing_empty by auto
next
case False note A_not_empty=False
show ?thesis
proof (unfold swap_function_def,unfold remove_iset_0_def, simp, rule indexing_remove_iset)
have finite_A: "finite A"using indexing_finite[OF indexing_A] .
show "indexing (A, f)" using indexing_A .
show "0 < card A" using finite_A A_not_empty by fastsimp
qed
qed
text{*Similarly with the second term: *}
lemma snd_swap_function_indexing:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "indexing (snd(swap_function ((A,f),(B,g))))"
proof (unfold swap_function_def, simp, rule conjI)
show "f 0 ∈ B --> indexing (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0)"
proof
assume f0_in_B: "f 0 ∈ B"
show "indexing (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0)"
proof -
have "indexing (insert_iset (fst (remove_iset (B, g) (obtain_position (f 0) (B, g))),
snd (remove_iset (B, g) (obtain_position (f 0) (B, g)))) (f 0) 0)"
proof (rule insert_iset_indexing)
have "indexing (remove_iset (B, g) (obtain_position (f 0) (B, g)))"
proof (rule indexing_remove_iset)
show "indexing (B, g)" using indexing_B .
show "obtain_position (f 0) (B, g) < card B" using obtain_position_less_card[OF f0_in_B indexing_B] .
qed
thus "indexing
(fst (remove_iset (B, g) (obtain_position (f 0) (B, g))),
snd (remove_iset (B, g) (obtain_position (f 0) (B, g))))" by simp
show "f 0 ∉ fst (remove_iset (B, g) (obtain_position (f 0) (B, g)))" unfolding remove_iset_def
using obtain_position_element[OF f0_in_B indexing_B] by simp
show "0 ≤ card (fst (remove_iset (B, g) (obtain_position (f 0) (B, g))))" by fast
qed
thus ?thesis by simp
qed
qed
show "f 0 ∉ B --> indexing (remove_ld (insert_iset (B, g) (f 0) 0))"
proof
assume f0_notin_B: "f 0 ∉ B"
show "indexing (remove_ld (insert_iset (B, g) (f 0) 0))"
proof -
have "indexing (remove_ld ((fst (insert_iset (B, g) (f 0) 0), snd (insert_iset (B, g) (f 0) 0)) ))"
proof (rule indexing_remove_ld)
show "linear_dependent (fst (insert_iset (B, g) (f 0) 0))"
using linear_dependent_insert_spanning_set[OF f0_notin_B indexing_A indexing_B A_in_V
B_in_V A_not_empty sg_B] by simp
show "indexing (fst (insert_iset (B, g) (f 0) 0), snd (insert_iset (B, g) (f 0) 0))"
using insert_iset_indexing[OF indexing_B f0_notin_B _] by auto
show "\<zero>\<^bsub>V\<^esub> ∉ fst (insert_iset (B, g) (f 0) 0)"
by (metis A_not_empty f0_not_zero fst_conv indexing_A insertE insert_iset_def iset_to_set_def li_A zero_notin_B)
qed
thus ?thesis by simp
qed
qed
qed
text{*If the first argument is an empty iset, then @{text swap_function} will also return the empty set (in first component).*}
lemma swap_function_empty:
shows "iset_to_set(fst(swap_function (({},f),(B,g))))={}"
unfolding swap_function_def
unfolding remove_iset_0_def
unfolding remove_iset_def by simp
lemma swap_function_empty2:
assumes A_empty: "A={}"
shows "iset_to_set(fst(swap_function ((A,f),(B,g))))={}"
using A_empty
unfolding swap_function_def
unfolding remove_iset_0_def
unfolding remove_iset_def by simp
end
text{*Up to now we have proved properties of @{text swap_function}. However, we want to iterate it a specific number of times
(compose with itself several times). We need to implement the power of a function because (surprisingly) it is not
in the library. We are interpreting the power of a function as a composition with itself.*}
text{*We will have to be careful with the types: we can not iterate (compose) every function: a function can be composed
with itself if the result and the arguments are of the same type (and the number of arguments is the same as the number
of arguments of the result). *}
text{*We can do the instantiation out of our context, since it is more general: *}
instantiation "fun" :: (type, type) power
begin
definition one_fun :: "'a => 'a"
where one_fun_def: "one_fun = id"
definition times_fun :: "('a => 'a) => ('a => 'a) => 'a => 'a"
where "times_fun f g = (%x. f (g x))"
instance
proof
qed
end
text{*Once we have finished the instatiation, we can prove some general properties about the power of a function. *}
text{*For example: the power of the identity function is also the identity.*}
lemma id_n: shows "id ^ n = id"
apply (induct n)
apply auto
unfolding one_fun_def times_fun_def
unfolding id_def
apply auto
done
text{*Any function power to zero is the identity.*}
lemma power_zero_id: "f^0=id"
by (metis one_fun_def power_0)
text{*A corollary of this lemma will be indispensable for the proofs by induction.*}
lemma fun_power_suc: shows "f^(Suc n)= f o (f^n)"
unfolding power.simps [of f]
apply (rule ext)
unfolding times_fun_def by simp
corollary fun_power_suc_eq:
shows "(f^(Suc n)) x = f ((f^n) x)"
using fun_power_suc by (metis id_o o_eq_id_dest)
context finite_dimensional_vector_space
begin
text{*Now we will begin with the proofs of properties that @{text swap_function} iterated several times satisfies.
In general, we have proved a property in the case $n=1$ and now we are going to generalize it for any n by induction.*}
text{*Most properties are invariants of the @{term swap_function}, so we will have proved a property in case $n=1$.
To generalize it we will apply induction: we suppose that a property is true for $f^n$ and we want to prove it
for $f^{(Suc (n)})$. By induction hypothesis, $f^n$ satisfies the property and thanks to @{text fun_power_suc_eq}
we can write @{term "(f^(Suc n)) x = f ((f^n) x)"}. As we have the property proved in case $n=1$,
we will obtain the result generalized.*}
text{*For example, we have proved @{text swap_function_empty}: @{thm swap_function_empty[no_vars]} and now we will generalize it.*}
lemma swap_function_power_empty:
shows "iset_to_set(fst((swap_function^n) (({},f),(B,g))))={}"
proof (induct n)
show " iset_to_set (fst ((swap_function ^ 0) (({}, f), B, g))) = {}" using id_apply power_zero_id
by (metis bot_nat_def fst_conv iset_to_set_def)
case Suc
fix n
assume hip_induct: "iset_to_set (fst ((swap_function ^ n) (({}, f), B, g))) = {}"
show "iset_to_set (fst ((swap_function ^ Suc n) (({}, f), B, g))) = {}"
proof -
have "iset_to_set(fst((swap_function ^ Suc n) (({}, f), B, g)))
=iset_to_set(fst((swap_function ((swap_function ^ n) (({}, f), B, g)))))"
using fun_power_suc_eq by metis
also have "...= iset_to_set
(fst (swap_function
((iset_to_set (fst ((swap_function ^ n) (({}, f), B, g))),
iset_to_index (fst ((swap_function ^ n) (({}, f), B, g)))),
iset_to_set (snd ((swap_function ^ n) (({}, f), B, g))),
iset_to_index (snd ((swap_function ^ n) (({}, f), B, g))))))" by auto
also have "...={}"
using hip_induct swap_function_empty2[of "iset_to_set (fst ((swap_function ^ n) (({}, f), B, g)))"
"(iset_to_index (fst ((swap_function ^ n) (({}, f), B, g))))"
"(iset_to_set (snd ((swap_function ^ n) (({}, f), B, g))))"
"(iset_to_index (snd ((swap_function ^ n) (({}, f), B, g))))"] by simp
finally show ?thesis .
qed
qed
lemma swap_function_power_empty2:
assumes A_empty: "A={}"
shows "iset_to_set(fst((swap_function^n) ((A,f),(B,g))))={}"
by (metis A_empty swap_function_power_empty)
text{*The generalized lemma for @{text swap_function_fst_in_carrier}.*}
lemma swap_function_power_fst_in_carrier:
assumes A_in_V: "A ⊆ carrier V"
shows "iset_to_set(fst((swap_function^n) ((A,f),(B,g)))) ⊆ carrier V"
proof (induct n)
show "iset_to_set (fst ((swap_function ^ 0) ((A, f), B, g))) ⊆ carrier V"
using power_zero_id id_apply A_in_V
by (metis iset_to_set_def fst_conv)
case Suc
fix n
assume hip_induct: "iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))) ⊆ carrier V"
show "iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g))) ⊆ carrier V"
proof -
have "(swap_function ^ Suc n) ((A, f), B, g)
=swap_function ((swap_function ^ n) ((A, f), B, g))" using fun_power_suc_eq by metis
thus ?thesis
using swap_function_fst_in_carrier[of "iset_to_set (fst ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_index (fst ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_index (snd ((swap_function ^ n) ((A, f), B, g)))"] hip_induct by simp
qed
qed
text{*Iterating the function the independence (in first argument) is preserved.*}
lemma fst_swap_function_power_preserves_li:
assumes li_A: "linear_independent A"
shows "linear_independent (iset_to_set(fst(((swap_function^(n))) ((A,f),(B,g)))))"
proof (induct "n")
case 0 show "linear_independent (iset_to_set (fst ((swap_function ^ 0) ((A, f), B, g))))"
proof -
have "iset_to_set (fst ((swap_function ^ 0) ((A, f), B, g)))=
iset_to_set (fst ((id) ((A, f), B, g)))"
using power_zero_id by metis
also have "...=A" using id_apply by simp
finally show ?thesis using li_A by presburger
qed
next
case Suc
fix n
assume hip_induct: "linear_independent (iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))))"
show "linear_independent (iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g))))"
proof -
have "(swap_function ^ Suc n) ((A, f), B, g)
= swap_function ((swap_function ^ n) ((A, f), B, g))" using fun_power_suc_eq by metis
thus ?thesis using fst_swap_function_preserves_li[OF hip_induct,
of "(iset_to_index (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))))"] by simp
qed
qed
text{*The first term is always an indexing. This is the generalization
of @{text fst_swap_function_indexing}.*}
lemma fst_swap_function_power_indexing:
assumes indexing_A: "indexing (A,f)"
and A_in_V: "A ⊆ carrier V"
shows "indexing (fst((swap_function^n) ((A,f),(B,g))))"
proof (induct n)
show "indexing(fst ((swap_function ^ 0) ((A, f), B, g)))"
using power_zero_id id_apply indexing_A
by (metis fst_conv)
case Suc
fix n
assume hip_induct: "indexing (fst ((swap_function ^ n) ((A, f), B, g)))"
show "indexing (fst ((swap_function ^ Suc n) ((A, f), B, g)))"
proof -
have "(swap_function ^ Suc n) ((A, f), B, g)
=swap_function ((swap_function ^ n) ((A, f), B, g))" using fun_power_suc_eq by metis
thus ?thesis
using fst_swap_function_indexing[of "iset_to_set (fst ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_index (fst ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_index (snd ((swap_function ^ n) ((A, f), B, g)))"]
swap_function_power_fst_in_carrier[OF A_in_V]
using hip_induct by simp
qed
qed
text{*Now we can prove that if we compose n-times @{text swap_function}, the cardinality of the set of the first term
will be decreased in n. Note that to use the induction hypothesis, we have to have proved previously
@{text fst_swap_function_power_indexing} (and obviously also @{text fst_swap_function_decr_card}).*}
lemma fst_swap_function_power_decr_card:
assumes indexing_A: "indexing (A, f)"
and A_in_V: "A ⊆ carrier V"
shows "card (iset_to_set (fst ((swap_function^n) ((A, f), B, g)))) = card A - n"
proof (induct n)
show "card (iset_to_set (fst ((swap_function ^ 0) ((A, f), B, g)))) = card A - 0" using power_zero_id id_apply
by (metis fst_conv iset_to_set_def minus_nat.diff_0)
case Suc
fix n
assume hip_induct: "card (iset_to_set (fst ((swap_function ^ n) ((A, f), B, g)))) = card A - n"
show "card (iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g)))) = card A - Suc n"
proof (cases "A={}")
case True show ?thesis
proof -
have "card (iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g))))=card {}"
using swap_function_power_empty2[OF True] by (metis True card.empty card_eq_0_iff)
thus ?thesis using True by simp
qed
next
case False note A_not_empty=False
show ?thesis
proof -
have "(swap_function ^ Suc n) ((A, f), B, g)
=swap_function ((swap_function ^ n) ((A, f), B, g))" using fun_power_suc_eq by metis
thus ?thesis
using fst_swap_function_power_indexing[OF indexing_A A_in_V]
using fst_swap_function_decr_card[of "(iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))))"] using hip_induct by simp
qed
qed
qed
text{*The generalization of @{text finite_fst_swap_function}: *}
lemma finite_fst_swap_function_power:
assumes indexing_A: "indexing (A,f)"
and A_in_V: "A ⊆ carrier V"
shows "finite (iset_to_set(fst((swap_function^n) ((A,f),(B,g)))))"
proof (induct n)
show "finite (iset_to_set (fst ((swap_function ^ 0) ((A, f), B, g))))"
using power_zero_id id_apply indexing_finite[OF indexing_A]
by (metis fst_conv iset_to_set_def)
case Suc
fix n
assume hip_induct: "finite (iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))))"
show "finite (iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g))))"
proof -
have indexing: "indexing
(iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))),
iset_to_index (fst ((swap_function ^ n) ((A, f), B, g))))"
using fst_swap_function_power_indexing[OF indexing_A A_in_V, of "n"] by auto
have finite: "finite (iset_to_set
(fst (swap_function
((iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))),
iset_to_index (fst ((swap_function ^ n) ((A, f), B, g)))),
iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))),
iset_to_index (snd ((swap_function ^ n) ((A, f), B, g)))))))"
using finite_fst_swap_function[of "iset_to_set (fst ((swap_function^n) ((A, f), B, g)))"
"iset_to_index (fst ((swap_function^n) ((A, f), B, g)))"
"iset_to_set (snd ((swap_function^ n) ((A, f), B, g)))"
"iset_to_index (snd ((swap_function^n) ((A, f), B, g)))"]
using indexing
using hip_induct
by simp
have "iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g)))
=iset_to_set (fst (swap_function ((swap_function ^ n) ((A, f), B, g))))" using fun_power_suc_eq by metis
also have "...=(iset_to_set
(fst (swap_function
((iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))),
iset_to_index (fst ((swap_function ^ n) ((A, f), B, g)))),
iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))),
iset_to_index (snd ((swap_function ^ n) ((A, f), B, g)))))))" by auto
finally have eq: "iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g))) =
iset_to_set(fst (swap_function ((iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))),
iset_to_index (fst ((swap_function ^ n) ((A, f), B, g)))),
iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))),
iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))))))" .
thus ?thesis using finite by presburger
qed
qed
text{*If we iterate cardinality of A times the function, where A is the set of the first argument, then the first
term of the result will be the empty set (we have removed card A elements in A).*}
corollary swap_function_power_card_fst_empty:
assumes indexing_A: "indexing (A,f)"
and A_in_V: "A ⊆ carrier V"
shows "iset_to_set(fst((swap_function^(card A)) ((A,f),(B,g))))={}"
proof -
have finite: "finite (iset_to_set(fst((swap_function^(card A)) ((A,f),(B,g)))))"
using finite_fst_swap_function_power[OF indexing_A A_in_V] by simp
have "card (iset_to_set (fst ((swap_function ^ (card A)) ((A, f), B, g)))) = card A - card A"
using fst_swap_function_power_decr_card[OF indexing_A A_in_V] .
also have "...= 0" by fastsimp
finally show ?thesis using finite
by (metis card_gt_0_iff le0 less_le_not_le)
qed
text{*And if we iterate a number of times less than card A, then the (first) result set will not be empty:*}
corollary swap_function_power_fst_not_empty_if_n_l_cardA:
assumes indexing_A: "indexing (A,f)"
and A_in_V: "A ⊆ carrier V"
and n_l_card: "n < card A"
shows "iset_to_set(fst((swap_function^n) ((A,f),(B,g))))≠{}"
proof -
have "card (iset_to_set (fst ((swap_function^n) ((A, f), B, g)))) = card A - n"
using fst_swap_function_power_decr_card[OF indexing_A A_in_V] .
thus ?thesis using n_l_card by auto
qed
(*lemma
assumes cardB_l_cardA: "card B < card A"
and indexing_A: "indexing (A,f)"
shows "f`({..<card B}∪{n. card B ≤ n ∧ n < card A})=A"
proof -
have "{..<card A}={..<card B}∪{n::nat. card B ≤ n ∧ n < card A}" using cardB_l_cardA by force
hence "f`({..<card B}∪{n::nat. card B ≤ n ∧ n < card A})=f`{..<card A}" by presburger
also have "...=A" using indexing_A unfolding indexing_def bij_betw_def by simp
finally show ?thesis .
qed*)
text{*This is a very important property which shows us how is the result of applying the function @{text remove_iset_0}
a specific number of times.*}
lemma remove_iset_0_eq:
assumes i: "indexing (A,f)"
and k_l_card: "k<card A"
shows "(remove_iset_0^k) (A,f)=(f`{k..<card A},λn. f(n+k))"
using k_l_card
proof (induct k)
case 0 show ?case unfolding power_zero_id unfolding id_apply using i unfolding indexing_def bij_betw_def
by fastsimp
next
case (Suc k)
hence k_l_card: "k<card A" and hyp: "(remove_iset_0 ^ k) (A, f) = (f ` {k..<card A}, λn. f (n + k))" by auto
show ?case
proof -
have "(remove_iset_0 ^ Suc k) (A, f) =remove_iset_0 ((remove_iset_0 ^ k) (A, f))" using fun_power_suc_eq by metis
also have "...=remove_iset_0 (f ` {k..<card A}, λn. f (n + k))" unfolding hyp ..
also have "...=(f ` {Suc k..<card A}, λn. f (n + Suc k))" unfolding remove_iset_0_def remove_iset_def
unfolding snd_conv fst_conv
proof (rule, rule conjI)
show "(λn. if n < 0 then f (n + k) else f (Suc n + k)) = (λn. f (n + Suc k))" by simp
next
show "f ` {k..<card A} - {f (0 + k)} = f ` {Suc k..<card A}"
proof (auto)
fix xa
assume fxa_notin: "f xa ∉ f ` {Suc k..<card A}" and k_le_xa: "k ≤ xa" and xa_l_card: "xa < card A"
have "xa < Suc k" using fxa_notin xa_l_card by fastsimp
hence "k=xa" using k_le_xa by presburger
thus "f xa = f k" by simp
next
fix xa
assume fxa_eq_fk: "f xa = f k" and suc_k_le_xa: "Suc k ≤ xa" and xa_l_cardA: "xa < card A"
have "f xa ≠ f k"
proof (rule inj_on_contraD[of f "{..<card A}"])
show "inj_on f {..<card A}" using i unfolding indexing_def bij_betw_def by simp
show "xa ≠ k" using suc_k_le_xa by fastsimp
show "xa ∈ {..<card A}" using xa_l_cardA by simp
show "k ∈ {..<card A}" using suc_k_le_xa xa_l_cardA by simp
qed
thus False using fxa_eq_fk by contradiction
qed
qed
finally show ?thesis .
qed
qed
corollary corollary_remove_iset_0_eq:
assumes i: "indexing (A,f)"
and n_l_card: "n < card A"
shows "snd ((remove_iset_0^n) (A,f)) 0 = f n"
using remove_iset_0_eq[OF i n_l_card] by simp
text{*In the next lemma we prove some properties at same the time. We have done like that
because in the induction case the properties need each others. We can not prove one separately: for example, to
prove that @{term "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function^(Suc n)) ((A, f), B, g)))"} we would write that
@{term "(swap_function ^ Suc n) ((A, f), B, g)=swap_function ((swap_function ^ n) ((A, f), B, g))"} and we would apply the
theorem @{text "zero_notin_snd_swap_function:"}*}
text{* @{thm zero_notin_snd_swap_function[no_vars]}*}
text{* However, to apply this theorem we need that
@{term "spanning_set (iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"}. To prove that we would need to use
@{text "swap_function_preserves_sg:"}*}
text{* @{thm swap_function_preserves_sg[no_vars]}*}
text{*And a premise would be that
@{term "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function^n) ((A, f), B, g)))"}...but this is what we want to prove.
Bringing all together in the same theorem we will have everything we need like induction hypothesis, so we can prove it.
Next we will separate the properties.*}
lemma zeronotin_sg_carrier_indexing:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and n_l_cardA: "n < card A"
shows "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function^n) ((A, f), B, g)))
∧ spanning_set(iset_to_set(snd((swap_function^n)((A,f),(B,g)))))
∧ (iset_to_set(snd((swap_function^n) ((A,f),(B,g)))))
⊆ carrier V
∧ indexing (snd((swap_function^n) ((A,f),(B,g))))"
using n_l_cardA
proof (induct n)
show "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function ^ 0) ((A, f), B, g))) ∧
spanning_set (iset_to_set (snd ((swap_function ^ 0) ((A, f), B, g)))) ∧
iset_to_set (snd ((swap_function^0) ((A, f), B, g))) ⊆ carrier V ∧
indexing (snd ((swap_function ^ 0) ((A, f), B, g)))"
proof (rule conjI4)
show "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function ^ 0) ((A, f), B, g)))" using power_zero_id id_apply
by (metis fst_conv iset_to_set_def one_fun_def snd_conv zero_notin_B)
show "spanning_set (iset_to_set (snd ((swap_function ^ 0) ((A, f), B, g))))" using power_zero_id id_apply
by (metis fst_conv iset_to_set_def one_fun_def sg_B snd_conv)
show "iset_to_set (snd ((swap_function^0) ((A, f), B, g))) ⊆ carrier V" using power_zero_id id_apply
by (metis fst_conv iset_to_set_def one_fun_def B_in_V snd_conv)
show "indexing (snd ((swap_function ^ 0) ((A, f), B, g)))"
using power_zero_id id_apply
by (metis fst_conv iset_to_set_def one_fun_def indexing_B snd_conv)
qed
case Suc
fix n
assume hip_induct: "n < card A ==> \<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))) ∧
spanning_set (iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))) ∧
iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))) ⊆ carrier V ∧
indexing (snd ((swap_function ^ n) ((A, f), B, g)))" and Suc_l_card: "Suc n < card A"
hence n_l_card: "n<card A"
by linarith
hence hi_zero: "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))"
and hi_sg: "spanning_set (iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"
and hi_carrier: "iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))) ⊆ carrier V"
and hi_indexing: "indexing (snd ((swap_function ^ n) ((A, f), B, g)))" using hip_induct by fast+
show "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function ^ Suc n) ((A, f), B, g))) ∧
spanning_set (iset_to_set (snd ((swap_function ^ Suc n) ((A, f), B, g)))) ∧
iset_to_set (snd ((swap_function ^ Suc n) ((A, f), B, g))) ⊆ carrier V ∧
indexing (snd ((swap_function ^ Suc n) ((A, f), B, g)))"
proof (rule conjI4)
have eq_fi: "(swap_function ^ Suc n) ((A, f), B, g)
=swap_function ((swap_function ^ n) ((A, f), B, g))" using fun_power_suc_eq by metis
show "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function ^ Suc n) ((A, f), B, g)))"
using fst_swap_function_power_indexing[OF indexing_A A_in_V, of n B g]
using hi_indexing
using hi_carrier
using hi_sg
using hi_zero
using fst_swap_function_power_preserves_li[OF li_A, of n f B g]
using swap_function_power_fst_not_empty_if_n_l_cardA[OF indexing_A A_in_V n_l_card, of B g]
using zero_notin_snd_swap_function[of "(iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))))"] using eq_fi by simp
show "spanning_set (iset_to_set (snd ((swap_function ^ Suc n) ((A, f), B, g))))"
using fst_swap_function_power_indexing[OF indexing_A A_in_V, of n B g]
using hi_indexing
using hi_carrier
using hi_sg
using hi_zero
using fst_swap_function_power_preserves_li[OF li_A, of n f B g]
using swap_function_power_fst_not_empty_if_n_l_cardA[OF indexing_A A_in_V n_l_card, of B g]
using swap_function_preserves_sg[of "(iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))))"] using eq_fi by simp
show "iset_to_set (snd ((swap_function ^ Suc n) ((A, f), B, g))) ⊆ carrier V"
using fst_swap_function_power_indexing[OF indexing_A A_in_V, of n B g]
using hi_indexing
using hi_carrier
using swap_function_power_fst_in_carrier[OF A_in_V, of n f B g]
using swap_function_power_fst_not_empty_if_n_l_cardA[OF indexing_A A_in_V n_l_card, of B g]
using swap_function_snd_in_carrier[of "(iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))))"] using eq_fi by simp
show "indexing (snd ((swap_function ^ Suc n) ((A, f), B, g)))"
using fst_swap_function_power_indexing[OF indexing_A A_in_V, of n B g]
using hi_indexing
using swap_function_power_fst_in_carrier[OF A_in_V, of n f B g]
using hi_carrier
using swap_function_power_fst_not_empty_if_n_l_cardA[OF indexing_A A_in_V n_l_card, of B g]
using fst_swap_function_power_preserves_li[OF li_A, of n f B g]
using hi_sg
using hi_zero
using snd_swap_function_indexing[of "(iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (fst ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_set (snd ((swap_function ^ n) ((A, f), B, g))))"
"(iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))))"] using eq_fi by simp
qed
qed
text{*Now we can obtain the properties separately as corollaries.*}
corollary zero_notin_snd_swap_function_power:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and n_l_cardA: "n<card A"
shows "\<zero>\<^bsub>V\<^esub> ∉ iset_to_set (snd ((swap_function^n) ((A, f), B, g)))"
using zeronotin_sg_carrier_indexing assms by simp
corollary swap_function_power_preserves_sg:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and n_l_cardA: "n<card A"
shows "spanning_set (iset_to_set (snd ((swap_function^n) ((A, f), B, g))))"
using zeronotin_sg_carrier_indexing assms by simp
corollary swap_function_power_snd_in_carrier:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and n_l_cardA: "n<card A"
shows "iset_to_set (snd ((swap_function^n) ((A, f), B, g))) ⊆ carrier V"
using zeronotin_sg_carrier_indexing assms by simp
corollary snd_swap_function_power_indexing:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and n_l_cardA: "n<card A"
shows "indexing (snd ((swap_function ^ n) ((A, f), B, g)))"
using zeronotin_sg_carrier_indexing assms by simp
text{*@{text Swap_function} preserves the cardinality of the second iset.*}
lemma snd_swap_function_power_preserves_card:
assumes indexing_A: "indexing (A, f)"
and indexing_B: "indexing (B, g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A ≠ {}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and n_l_card: "n<card A"
shows "card (iset_to_set (snd ((swap_function^n) ((A, f), B, g)))) = card B"
using n_l_card
proof (induct n)
show "card (iset_to_set (snd ((swap_function ^ 0) ((A, f), B, g)))) = card B"
using id_apply power_zero_id
by (metis fst_conv iset_to_set_def snd_conv)
case Suc
fix n
assume hip: "n < card A ==> card (iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))) = card B"
and suc_l_card: "Suc n < card A"
hence hip_induct: "card (iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))) = card B"
and n_l_card: "n<card A" by fastsimp+
show "card (iset_to_set (snd ((swap_function ^ Suc n) ((A, f), B, g)))) = card B"
proof -
have "(swap_function ^ Suc n) ((A, f), B, g)
=swap_function ((swap_function ^ n) ((A, f), B, g))" using fun_power_suc_eq by metis
thus ?thesis
using fst_swap_function_power_indexing[OF indexing_A A_in_V]
using snd_swap_function_power_indexing[OF indexing_A indexing_B
A_in_V B_in_V A_not_empty li_A sg_B zero_notin_B n_l_card]
using swap_function_power_snd_in_carrier[OF indexing_A indexing_B
A_in_V B_in_V A_not_empty li_A sg_B zero_notin_B n_l_card]
using fst_swap_function_power_preserves_li[OF li_A, of n f B g]
using swap_function_power_fst_not_empty_if_n_l_cardA[OF indexing_A A_in_V n_l_card, of B g]
using swap_function_power_preserves_sg[OF indexing_A indexing_B
A_in_V B_in_V A_not_empty li_A sg_B zero_notin_B n_l_card]
using zero_notin_snd_swap_function_power[OF indexing_A indexing_B
A_in_V B_in_V A_not_empty li_A sg_B zero_notin_B n_l_card]
using snd_swap_function_preserves_card [of "iset_to_set (fst ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_index (fst ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))"
"iset_to_index (snd ((swap_function ^ n) ((A, f), B, g)))"] hip_induct by simp
qed
qed
text{*The first term of @{text swap_function} iterated is the same than @{text remove_iset_0} iterated.*}
lemma fst_swap_function_power_eq:
"fst ((swap_function ^ n) ((A, f), B, g)) = (remove_iset_0 ^ n) (A, f)"
proof (induct n)
case 0 show ?case using power_zero_id id_apply fst_conv by metis
next
case (Suc n)
show ?case
proof -
have "fst((swap_function ^ Suc n) ((A, f), B, g))
=fst(swap_function ((swap_function ^ n) ((A, f), B, g)))" using fun_power_suc_eq by metis
also have "...=fst(swap_function (fst((swap_function ^ n) ((A, f), B, g)),
snd((swap_function ^ n) ((A, f), B, g))))" by simp
also have "...=fst(swap_function ((remove_iset_0 ^ n) (A, f), snd((swap_function ^ n) ((A, f), B, g))))"
using Suc.hyps by simp
also have "...=remove_iset_0 ((remove_iset_0 ^ n) (A, f))" unfolding swap_function_def fst_conv ..
also have "...=(remove_iset_0 ^ Suc n) (A, f)" using fun_power_suc_eq by metis
finally show ?thesis .
qed
qed
text{*The first element of the result of the first term in the nth iteration is f(n).*}
lemma snd_fst_swap_function_image_0:
assumes indexing_A: "indexing (A,f)"
and c: "n < card A"
shows "snd (fst ((swap_function ^ n) ((A, f), B, g))) 0 = f (n)"
proof -
have "fst ((swap_function ^ n) ((A, f), B, g)) = (remove_iset_0^n) (A,f)"
using fst_swap_function_power_eq[of n A f B g] .
hence "snd (fst ((swap_function ^ n) ((A, f), B, g))) 0 = snd ((remove_iset_0^n) (A,f)) 0"
by presburger
also have "...= f n" using corollary_remove_iset_0_eq[OF indexing_A c] .
finally show ?thesis .
qed
text{*If we compose n times the @{text swap_function}, the first term will be the first set minus the first n elements of it.*}
lemma swap_function_fst_image_until_n:
assumes indexing_A: "indexing (A,f)"
and A_not_empty: "A≠{}"
and n_l_cardA: "n<card A"
shows "iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))) = f ` {n..<card A}"
using n_l_cardA
proof (induct n)
show "iset_to_set (fst ((swap_function ^ 0) ((A, f), B, g))) = f ` {0..<card A}"
using id_apply power_zero_id
using indexing_A unfolding indexing_def bij_betw_def
by (metis atLeast0LessThan fst_conv iset_to_index_def iset_to_set_def snd_conv)
case Suc
fix n
assume "n < card A ==>iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))) = f ` {n..<card A}"
and "Suc n < card A"
hence hip_induct: "iset_to_set (fst ((swap_function ^ n) ((A, f), B, g))) = f ` {n..<card A}"
and n_l_card: "n < card A" by auto
show "iset_to_set (fst ((swap_function ^ Suc n) ((A, f), B, g))) = f ` {Suc n..<card A}"
proof -
have fn: "snd (fst ((swap_function ^ n) ((A, f), B, g))) 0 = f n"
using snd_fst_swap_function_image_0[OF indexing_A n_l_card] by simp
have "iset_to_set (fst((swap_function ^ Suc n) ((A, f), B, g)))
=iset_to_set (fst(swap_function ((swap_function ^ n) ((A, f), B, g))))"
using fun_power_suc_eq by metis
also have "...=iset_to_set (fst(swap_function (fst((swap_function ^ n) ((A, f), B, g)),
snd((swap_function ^ n) ((A, f), B, g)))))" by simp
also have "...=iset_to_set (fst(swap_function ((fst(fst((swap_function ^ n) ((A, f), B, g))),
snd(fst((swap_function ^ n) ((A, f), B, g)))), snd((swap_function ^ n) ((A, f), B, g)))))" by auto
also have "...=iset_to_set (fst(swap_function ((f ` {n..<card A},
snd(fst((swap_function ^ n) ((A, f), B, g)))), snd((swap_function ^ n) ((A, f), B, g)))))"
using hip_induct by simp
also have "...=f ` {n..<card A} - {f n}" unfolding swap_function_def remove_iset_0_def remove_iset_def
using fn by force
also have "...=f ` {n..<card A} - f` {n}" by fast
also have "...=f`({n..<card A} - {n})"
proof (rule inj_on_image_set_diff[symmetric])
show "inj_on f {..<card A}" using indexing_A unfolding indexing_def bij_betw_def by simp
show "{n..<card A} ⊆ {..<card A}"
by (metis Un_upper2 atLeastLessThan_empty ivl_disj_un(8)
lessThan_0 lessThan_subset_iff less_eq_nat.simps(1) nat_le_linear)
show "{n} ⊆ {..<card A}"
proof -
have "card A > 0" using A_not_empty indexing_finite[OF indexing_A] by fastsimp
thus ?thesis using n_l_card by fast
qed
qed
also have "...=f`{Suc n..<card A}"
by (metis atLeastLessThan_singleton ivl_diff le_Suc_eq le_refl)
finally show ?thesis .
qed
qed
text{*Now an auxiliar and ugly lemma which we will use to prove the swap theorem. It is very laborious and hard lemma,
similar that @{text swap_function_exists_y_in_B} but much more precisse and difficult (over 400 lines).
It represents properties that has the function during the process of iterating.*}
lemma aux_swap_theorem1:
assumes indexing_A: "indexing (A,f)" --"In this set are the elements that we have not included in second term yet."
and indexing_B: "indexing (B,g)"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and li_Z: "linear_independent Z" --"Z is the first independent set, the set over we would apply our function the first
time. A is the subset of Z where there are the elements of Z
that we have not added to B yet. The elements that we have added to B are in C."
and A_union_C: "A∪C=Z" --"Of course, the union of A and C is Z."
and disjoint: "A∩C={}" --"The sets are disjoints."
and surj_g_C: "g`{..<card C}= C" --"In first positions of B there are elements of Z that we have already included.
This set will be independent, so when we apply @{text remove_ld} we will delete an element of (B-C)"
shows "∃y∈B. iset_to_set (snd(swap_function ((A,f),(B,g))))
=(insert (f 0) (B-{y}))
∧ y ∉ C
∧ iset_to_index (snd(swap_function ((A,f),(B,g))))
` {..<card (C) + 1} = C ∪ {f 0}"
proof (unfold swap_function_def, auto)
have li_A: "linear_independent A" and li_C: "linear_independent C"
using independent_set_implies_independent_subset[OF _ li_Z] A_union_C by auto
show "f 0 ∈ B ==>
∃y∈B. fst (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) = insert (f 0) (B - {y}) ∧
y ∉ C ∧ snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {..<Suc (card C)} =
insert (f 0) C"
proof -
assume f0_in_B: "f 0 ∈ B"
show "∃y∈B. fst (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) = insert (f 0) (B - {y}) ∧
y ∉ C ∧
snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {..<Suc (card C)} =
insert (f 0) C"
proof (rule bexI[of _ "f 0"], rule conjI)
show "fst (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) = insert (f 0) (B - {f 0})"
unfolding insert_iset_def remove_iset_def
using f0_in_B indexing_B obtain_position_element by force
show "f 0 ∉ C ∧
snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {..<Suc (card C)}
= insert (f 0) C"
proof (rule conjI)
have "0 ∈ {..< card A}" using A_not_empty
by (metis card_gt_0_iff indexing_A indexing_finite lessThan_iff)
hence "f 0 ∈ A" using indexing_A unfolding indexing_def bij_betw_def by auto
thus f0_notin_C: "f 0 ∉ C" using disjoint by fast
show "snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {..<Suc (card C)}
= insert (f 0) C"
proof -
have "snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {..<Suc (card C)}=
snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {0} ∪
snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {0<..<Suc (card C)}"
proof -
have "{..<Suc (card C)}={0}∪{0<..<Suc (card C)}" by fastsimp
thus ?thesis by blast
qed
also have "...=snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {0} ∪ C"
proof -
have "snd (insert_iset (remove_iset (B, g) (obtain_position (f 0) (B, g))) (f 0) 0) ` {0<..<Suc (card C)} = C"
proof -
have cardC_le_obt_pos: "card C ≤ obtain_position (f 0) (B, g)"
by (metis f0_in_B f0_notin_C indexing_B insert_image insert_subset leI
lessThan_iff mem_def obtain_position_element subset_refl surj_g_C)
have image_C: "snd (remove_iset (B, g) (obtain_position (f 0) (B, g))) ` {..<(card C)} = C"
unfolding remove_iset_def
proof (auto)
show "!!k. [| k < card C; k < obtain_position (f 0) (B, g)|] ==> g k ∈ C"
by (metis imageI lessThan_iff surj_g_C)
show "!!k. [|k < card C; ¬ k < obtain_position (f 0) (B, g)|] ==> g (Suc k) ∈ C"
using cardC_le_obt_pos by simp
show "!!x. [|x ∈ C; x ∉ (λk. g (Suc k)) ` ({..<card C} ∩ {k. ¬ k < obtain_position (f 0) (B, g)})|]
==> x ∈ g ` ({..<card C} ∩ {k. k < obtain_position (f 0) (B, g)})"
using surj_g_C cardC_le_obt_pos by force
qed
show ?thesis unfolding insert_iset_def indexing_ext_def using image_C
proof (auto)
fix x
assume x_in_C: "x∈C"
show "x ∈ (λk. snd (remove_iset (B, g) (obtain_position (f 0) (B, g))) (k - Suc 0)) `
({0<..<Suc (card C)} ∩ Collect (op < 0))"
proof (unfold image_def, auto)
have "∃xa∈{..<card C}. x = snd (remove_iset (B, g) (obtain_position (f 0) (B, g))) xa"
using image_C x_in_C unfolding image_def by auto
from this obtain xa where xa_in_l_card: "xa∈{..<card C}"
and x_eq: "x = snd (remove_iset (B, g) (obtain_position (f 0) (B, g))) xa" by blast
show ex_xa: "∃xa∈{0<..<Suc (card C)} ∩ Collect (op < 0).
x = snd (remove_iset (B, g) (obtain_position (f 0) (B, g))) (xa - Suc 0)"
proof (rule bexI[of _ "xa + 1"])
show "x = snd (remove_iset (B, g) (obtain_position (f 0) (B, g))) (xa + 1 - Suc 0)"
using x_eq by auto
show "xa + 1 ∈ {0<..<Suc (card C)} ∩ Collect (op < 0)"
using xa_in_l_card by auto
qed
qed
qed
qed
thus ?thesis by presburger
qed
also have "...={f 0} ∪ C" unfolding insert_iset_def indexing_ext_def by fastsimp
also have "...=insert (f 0) C" by simp
finally show ?thesis .
qed
qed
show "f 0 ∈ B" using f0_in_B .
qed
qed
show "f 0 ∉ B ==>
∃y∈B. fst (remove_ld (insert_iset (B, g) (f 0) 0)) = insert (f 0) (B - {y}) ∧
y ∉ C ∧ snd (remove_ld (insert_iset (B, g) (f 0) 0)) ` {..<Suc (card C)} = insert (f 0) C"
proof -
assume f0_notin_B: "f 0 ∉ B"
show "∃y∈B. fst (remove_ld (insert_iset (B, g) (f 0) 0)) = insert (f 0) (B - {y}) ∧
y ∉ C ∧ snd (remove_ld (insert_iset (B, g) (f 0) 0)) ` {..<Suc (card C)} = insert (f 0) C"
proof -
have A_in_V: "A ⊆ carrier V" using l_ind_good_set[OF li_Z] A_union_C unfolding good_set_def by fast
def P'≡"iset_to_set (insert_iset (B, g) (f 0) 0)"
def h'≡"iset_to_index(insert_iset (B, g) (f 0) 0)"
have ld_P':"linear_dependent P'"
proof (unfold P'_def, rule linear_dependent_insert_spanning_set)
show "f 0 ∉ B" using f0_notin_B .
show "indexing (A, f)" using indexing_A .
show "indexing (B, g)" using indexing_B .
show "A ⊆ carrier V" using A_in_V .
show "B ⊆ carrier V" using B_in_V .
show "A ≠ {}" using A_not_empty .
show "spanning_set B" using sg_B .
qed
have indexing: "indexing (P',h')"
unfolding P'_def h'_def using insert_iset_indexing[OF indexing_B f0_notin_B _] by simp
have zero_not_in: "\<zero>\<^bsub>V\<^esub> ∉ P'"
using P'_def zero_notin_B f0_not_zero[OF indexing_A li_A A_not_empty]
unfolding insert_iset_def by simp
let ?P = "(λk. ∃y∈P'. ∃g. g∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧
k < card P' ∧ h' k = y ∧ y = linear_combination g (h' ` {i. i < k}))"
have exK: "(∃k. ?P k)"
using linear_dependent_set_sorted_contains_linear_combination[OF ld_P' zero_not_in indexing] by auto
have ex_LEAST: "?P (LEAST k. ?P k)"
using LeastI_ex [OF exK] .
let ?k = "(LEAST k. ?P k)"
have "∃y∈P'. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ ?k ∧
?k < card P' ∧ h' ?k = y ∧ y = linear_combination g (h' ` {i. i < ?k})"
using ex_LEAST by simp
then obtain y s
where one_le_k: "1 ≤ ?k" and k_l_card: "?k < card P'" and h'_k_eq_y: "h' ?k = y"
and cf_s: "s ∈ coefficients_function (carrier V)" and
combinacion_anteriores: "y = linear_combination s (h' ` {i. i < ?k})" by blast
have rem_eq: "fst (remove_ld (P', h')) = P' - {y}" and y_in_P': "y ∈ P'"
using indexing_equiv_img [OF indexing] one_le_k k_l_card h'_k_eq_y
unfolding Pi_def unfolding remove_ld_def' by auto
show ?thesis
proof (rule bexI[of _ y], rule conjI)
show y_in_B: "y∈B" --"WE HAVE TO PROVE THAT y is different to f 0"
using y_in_P' unfolding P'_def unfolding insert_iset_def
proof (simp)
assume y_f0_or_in_B: "y=f 0 ∨ y ∈ B"
show "y ∈ B"
proof (cases "y= f 0")
case False thus ?thesis using y_f0_or_in_B by fast
next
case True
have inj_on_h': "inj_on h' {..<card P'}" using indexing unfolding indexing_def bij_betw_def by simp
have "h' 0 = f 0" using h'_def unfolding insert_iset_def indexing_ext_def by simp
hence "h' 0 = y" using True by simp
hence "h' 0= h' ?k" using h'_k_eq_y by simp
hence "?k=0"
using inj_on_eq_iff[OF inj_on_h'] using k_l_card by simp
thus ?thesis using one_le_k by presburger --"CONTRADICTION, WE HAVE k=0 and k greater or equal to 1"
qed
qed
show "fst (remove_ld (insert_iset (B, g) (f 0) 0)) = insert (f 0) (B - {y})"
proof -
have "fst (remove_ld (insert_iset (B, g) (f 0) 0))
=fst (remove_ld (fst(insert_iset (B, g) (f 0) 0),snd(insert_iset (B, g) (f 0) 0)))" by simp
also have "...=(insert (f 0) B) - {y}" using rem_eq unfolding P'_def h'_def insert_iset_def by simp
also have "...=insert (f 0) (B - {y})" using f0_notin_B y_in_B by blast
finally show ?thesis .
qed
show "y ∉ C ∧ snd (remove_ld (insert_iset (B, g) (f 0) 0)) ` {..<Suc (card C)} = insert (f 0) C"
proof (rule conjI)
show "y ∉ C"
proof (cases "y∉C")
case True thus ?thesis .
next
case False note y_in_C=False show ?thesis
proof -
have image_h_C: "h'`{0<..< Suc (card C)} = C"
proof (unfold image_def, unfold h'_def,unfold insert_iset_def
, unfold indexing_ext_def, auto)
fix xa
assume "0 < xa" and "xa < Suc (card C)"
thus "g (xa - Suc 0) ∈ C" using surj_g_C by auto
next
fix x
assume x_in_C: "x ∈ C"
have "∃xa∈{..<(card C)}. x = g (xa)" using surj_g_C x_in_C unfolding image_def by auto
from this obtain xa where g_xa_x: "x = g (xa)" and xa_in_set: "xa∈{..<(card C)}" by auto
show "∃xb∈{0<..<Suc (card C)}. x = g (xb - Suc 0)" --"SerÃa xb=xa+1"
using g_xa_x xa_in_set by force
qed
have image_h_BC: "h'`{i. Suc (card C)≤i ∧ i<(card P')}=B-C"
proof (unfold image_def, unfold h'_def,unfold insert_iset_def
, unfold indexing_ext_def, auto)
fix xa
assume (*suc_card_le_xa: "Suc (card C) ≤ xa" and*) "xa < card P'"
hence xa_l_suc_cardB: "xa < Suc (card B)" unfolding P'_def
by (metis P'_def card_insert_if f0_notin_B fst_conv
indexing_B indexing_finite insert_iset_def iset_to_set_def)
have "card B > 0 " using y_in_B indexing_finite[OF indexing_B]
by (metis card_gt_0_iff equals0D)
thus "g (xa - Suc 0) ∈ B"
using indexing_B unfolding indexing_def bij_betw_def using xa_l_suc_cardB by auto
next
fix x
assume x_in_B: "x ∈ B" and x_notin_C: "x ∉ C"
show "∃xa≥Suc (card C). xa < card P' ∧ x = g (xa - Suc 0)" --"El testigo es a+1"
proof -
from x_in_B obtain a where x_eq_ga: "x=g a" and a_l_cardB:"a < card B"
using indexing_B unfolding indexing_def
bij_betw_def by auto
have a_ge_cardC: "a≥card C"
by (metis imageI lessThan_iff not_leE surj_g_C x_eq_ga x_notin_C)
hence a_plus_one_ge_suc_card_C: "a + 1 ≥ Suc (card C)" by simp
have x_eq:"x = g (a + 1 - Suc 0)" using x_eq_ga by simp
have "a + 1 < card P'" using P'_def
by (metis Suc_eq_plus1 Suc_n_not_n a_l_cardB f0_notin_B indexing_B
insert_iset_increase_card less_trans_Suc linorder_neqE_nat
nat_add_commute not_add_less2)
thus ?thesis using a_plus_one_ge_suc_card_C and x_eq by fast
qed
next
fix xa
assume suc_C_le_xa: "Suc (card C) ≤ xa" and xa_l_cardP: "xa < card P'"
and g_xa0_in_C:"g (xa - Suc 0) ∈ C" --"We will obtain a contradiction thanks to injectivity."
def b≡" g (xa - Suc 0)"
have xa0_l_B:"xa - Suc 0 < card B" using xa_l_cardP
by (metis One_nat_def P'_def Suc_less_SucD
Suc_pred add_Suc_shift f0_notin_B gr0I gr_implies_not0
indexing_B insert_iset_increase_card less_eq_Suc_le
nat_add_commute plus_nat.add_0 suc_C_le_xa)
have cardC_le_cardB: "card C ≤ card B"
by (metis One_nat_def P'_def Suc_diff_1 Suc_le_lessD
diff_add_inverse f0_notin_B indexing_B
insert_iset_increase_card le_add1 le_trans nat_add_commute
not_less_eq_eq order_less_not_sym suc_C_le_xa xa_l_cardP)
hence C_subset_B: "C⊆B" using indexing_B surj_g_C unfolding indexing_def bij_betw_def
unfolding image_def by fastsimp
have b_in_C: "b ∈ C" using b_def g_xa0_in_C by auto
from b_in_C obtain a where ga_eq_b: "g a = b" and a_l_cardC: "a < card C"
using surj_g_C unfolding image_def by force
hence "a ≠ xa - Suc 0" using suc_C_le_xa by auto
thus False using indexing_B ga_eq_b a_l_cardC xa_l_cardP xa0_l_B cardC_le_cardB
inj_on_eq_iff[of g "{..<card B}" "a" "xa - Suc 0"]
unfolding indexing_def bij_betw_def b_def
by fastsimp
qed
hence "y∉ h'`{i. Suc (card C)≤i ∧ i<(card P')}" using y_in_C by simp
hence k_l_cardC: "?k≤card C" using image_h_C h'_k_eq_y k_l_card by auto
have image_h_card_in_Z: "h' ` {..<card C} ⊆ Z"
proof -
have "{..< card C}={0} ∪ {0<..< card C}" using one_le_k k_l_cardC by force
hence "h' ` {..< card C}=h' `{0} ∪ h'`{0<..< card C}" by blast
also have "...= {f 0} ∪ h'`{0<..< card C}"
using h'_def unfolding insert_iset_def indexing_ext_def by auto
also have "...⊆ Z"
proof -
have "f 0 ∈ A"
using indexing_in_set[OF indexing_A _]
A_not_empty indexing_finite[OF indexing_A] by (metis card_eq_0_iff gr0I)
thus ?thesis using image_h_C A_union_C by auto
qed
finally show ?thesis .
qed
have ld_insert: "linear_dependent (insert y (h'`{i. i<?k}))"
proof (rule lc1)
show "linear_independent (h'`{i. i<?k})"
proof (rule independent_set_implies_independent_subset)
show "linear_independent Z" using li_Z .
next
show "h' ` {i. i < ?k} ⊆ Z" using image_h_card_in_Z k_l_cardC by auto
qed
show "y ∈ carrier V" by (metis B_in_V subsetD y_in_B)
show "y∉ h'`{i. i<?k}"
using y_in_C and h'_k_eq_y and k_l_card and indexing
unfolding indexing_def and bij_betw_def and inj_on_def
by force
show "∃f. f ∈ coefficients_function (carrier V) ∧
linear_combination f (h' `{i. i<?k})=y"
using cf_s and combinacion_anteriores by auto
qed
have "linear_dependent Z"
proof (rule linear_dependent_subset_implies_linear_dependent_set [of "insert y (h'`{i. i<?k})"])
show "insert y (h' ` {i. i<?k}) ⊆ Z"
proof -
have "y∈Z" using y_in_C A_union_C by auto
thus ?thesis using image_h_card_in_Z k_l_cardC by auto
qed
show "good_set Z"
by (metis l_ind_good_set li_Z)
show "linear_dependent (insert y (h' `{i. i<?k}))" using ld_insert .
qed
--"Contradiction: we have linear dependent Z and linear independent Z"
thus ?thesis using independent_implies_not_dependent[OF li_Z] by contradiction
qed
qed
show "snd (remove_ld (insert_iset (B, g) (f 0) 0)) ` {..<Suc (card C)} = insert (f 0) C"
proof -
have eq: "snd (remove_ld (insert_iset (B, g) (f 0) 0))=snd(remove_iset(insert_iset (B, g) (f 0) 0) ?k)"
unfolding remove_ld_def using snd_conv using remove_iset_def[of "(insert_iset (B, g) (f 0) 0)" "?k"]
unfolding P'_def h'_def by force
have "{..<Suc (card C)}={0}∪{0<..<Suc (card C)}" by auto
hence "snd (remove_ld (insert_iset (B, g) (f 0) 0)) ` {..<Suc (card C)}
=snd (remove_ld (insert_iset (B, g) (f 0) 0)) ` {0}
∪ snd (remove_ld (insert_iset (B, g) (f 0) 0)) `{0<..<Suc (card C)}" by blast
also have "...= {f 0} ∪ snd (remove_ld (insert_iset (B, g) (f 0) 0)) `{0<..<Suc (card C)}"
proof -
have "snd (insert_iset (B, g) (f 0) 0) ` {0}={f 0}" unfolding insert_iset_def indexing_ext_def by simp
hence "snd (remove_iset(insert_iset (B, g) (f 0) 0) ?k)`{0}={f 0}"
unfolding remove_iset_def using one_le_k by auto
thus ?thesis using eq by presburger
qed
also have "...= {f 0} ∪ C"
proof -
have k_g_cardC: "?k ≥ Suc (card C)" --"No puede ser menor porque C es independiente!"
proof (cases "?k ≥ Suc (card C)")
case True thus ?thesis .
next
case False note k_l_suc_cardC=False
have image_eq:"h'`{0<..<Suc (card C)}=g`{..<card C}"
unfolding h'_def insert_iset_def indexing_ext_def
unfolding image_def by force
have image_eq2: "h' 0 = f 0" unfolding h'_def insert_iset_def indexing_ext_def by simp
have ld_f0_C: "linear_dependent ({f 0} ∪ g`{..<card C})"
proof (rule linear_dependent_subset_implies_linear_dependent_set)
show "insert (h' ?k) (h' `{..<?k})⊆ {f 0} ∪ g`{..<card C}"
proof -
have igualdad_conjuntos: "{..<?k} ∪ {?k}={0} ∪ {0<..?k}" using one_le_k by auto
have "insert (h' ?k) (h'`{..<?k})= h'` {?k} ∪ h'`{..<?k} " by auto
also have "...=h'` ({..<?k} ∪ {?k})" by auto
also have "...=h'` ({0} ∪ {0<..?k})" using igualdad_conjuntos by auto
also have "...={h' 0} ∪ h'`{0<..?k}" by auto
also have "... ⊆ {f 0} ∪ g`{..<card C}" using image_eq image_eq2 k_l_suc_cardC by auto
finally show ?thesis .
qed
show "good_set ({f 0} ∪ g ` {..<card C})"
using f0_in_V[OF indexing_A A_in_V A_not_empty] surj_g_C l_ind_good_set[OF li_C]
unfolding good_set_def by simp
show "linear_dependent (insert (h' ?k) (h' `{..<?k}))"
proof (rule lc1)
show "linear_independent (h' `{..<?k})"
proof (rule independent_set_implies_independent_subset)
have "h' `{..<?k}⊆{f 0} ∪ g ` {..<card C}" using image_eq image_eq2 k_l_suc_cardC by force
also have "...⊆ Z"
using A_union_C A_not_empty surj_g_C
indexing_in_set[OF indexing_A] indexing_finite[OF indexing_A]
by force
finally show "h' `{..<?k} ⊆ Z" .
next
show "linear_independent Z" using li_Z .
qed
show "h' ?k ∈ carrier V"
proof -
have "h' ?k ∈ h'`{..<card P'}" using k_l_card by blast
also have "...=P'" using indexing unfolding indexing_def bij_betw_def by simp
also have "...⊆ carrier V" using P'_def B_in_V f0_in_V[OF indexing_A A_in_V A_not_empty]
unfolding insert_iset_def by simp
finally show ?thesis .
qed
show "h' ?k ∉ h'` {..<?k}"
proof (cases "h' ?k ∉ h'` {..<?k}")
case True thus ?thesis .
next case False
from this obtain s where hk_hs: "h' ?k = h' s" and s_in_set: "s∈{..<?k}" by auto
hence s_not_k: "s≠?k" and s_l_card: "s<card P'" using k_l_card by auto
have "inj_on h' {..<card P'}" using indexing unfolding indexing_def bij_betw_def by auto
hence "h' ?k ≠ h' s" using inj_on_eq_iff s_not_k s_l_card k_l_card by fastsimp
thus ?thesis
using hk_hs by contradiction
qed
next
show "∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f (h' ` {..<?k}) = h' (?k)"
proof -
have "{i. i<?k}={..<?k}" by fast
thus ?thesis
using cf_s and combinacion_anteriores h'_k_eq_y by auto
qed
qed
qed
have li_f0_C: "linear_independent ({f 0} ∪ g`{..<card C})"
proof (rule independent_set_implies_independent_subset)
show "{f 0} ∪ g ` {..<card C} ⊆ Z"
using A_union_C A_not_empty surj_g_C
indexing_in_set[OF indexing_A] indexing_finite[OF indexing_A]
by force
show "linear_independent Z " using li_Z .
qed
thus ?thesis using dependent_implies_not_independent[OF ld_f0_C] by contradiction
--"Contradiction"
qed
have "snd (remove_iset(insert_iset (B, g) (f 0) 0) ?k) ` {0<..<Suc (card C)}=
snd (insert_iset (B, g) (f 0) 0) `{0<..<Suc (card C)}"
unfolding remove_iset_def using k_g_cardC by auto
also have "...=C"
proof (unfold insert_iset_def, unfold indexing_ext_def, unfold image_def, auto)
fix xa
assume "0 < xa" and "xa < Suc (card C)"
thus "g (xa - Suc 0) ∈ C" using surj_g_C by force
next
fix x
assume x_in_C: "x ∈ C"
from this obtain a where "x = g a" and "a < card C" using surj_g_C by blast
thus "∃xa∈{0<..<Suc (card C)}. x = g (xa - Suc 0)" using bexI[of _ "a+1"] by force
qed
finally show ?thesis using eq by presburger
qed
also have "...=insert (f 0) C" by simp
finally show ?thesis .
qed
qed
qed
qed
qed
qed
text{*Another important auxiliary lemma. Applying the swap function $n$-times (with $n < card(A)$)
to @{term "((A,f),(B,g))"}, where $A$ is independent and $B$ a spanning set,
we will have that the first $n$ elements of $A$ will be in the first
positions of the second component of the result. Of course, these elements come from $A$ and thus they are independent.
We make use of @{text aux_swap_theorem1} to prove this lemma.*}
lemma aux_swap_theorem2:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
and n_l_cardA: "n < card A"
shows "f`{..<n}
= iset_to_index(snd((swap_function^(n)) ((A,f),(B,g))))`{..<n}
∧ iset_to_index(snd((swap_function^(n)) ((A,f),(B,g))))`{..<n}
⊂ A
∧ linear_independent
(iset_to_index(snd((swap_function^(n)) ((A,f),(B,g))))`{..<n})
∧ n = (card (iset_to_index(snd((swap_function^(n))
((A,f),(B,g))))`{..<n}))"
using n_l_cardA
proof (induct n)
show "f ` {..<0} = iset_to_index (snd ((swap_function ^ 0) ((A, f), B, g))) ` {..<0} ∧
iset_to_index (snd ((swap_function ^ 0) ((A, f), B, g))) ` {..<0} ⊂ A ∧
linear_independent (iset_to_index (snd ((swap_function ^ 0) ((A, f), B, g))) ` {..<0}) ∧
0 = card (iset_to_index (snd ((swap_function ^ 0) ((A, f), B, g))) ` {..<0})"
proof -
have "iset_to_index (snd ((swap_function ^ 0) ((A, f), B, g))) ` {..<0}={}" by simp
hence li: "linear_independent (iset_to_index (snd ((swap_function ^ 0) ((A, f), B, g))) ` {..<0})"
using empty_set_is_linearly_independent by presburger
show ?thesis using li and A_not_empty by auto
qed
case Suc
fix n
assume hip_induct: "n < card A ==>
f ` {..<n} = iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n} ∧
iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n} ⊂ A ∧
linear_independent (iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n}) ∧
n = card (iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n})"
and suc_n_l_card: "Suc n < card A"
have n_l_card: "n < card A" using suc_n_l_card by simp
hence hip: "f ` {..<n} = iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n} ∧
iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n} ⊂ A ∧
linear_independent (iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n}) ∧
n = card (iset_to_index (snd ((swap_function ^ n) ((A, f), B, g))) ` {..<n})"
using hip_induct by simp
show "f ` {..<Suc n} = iset_to_index (snd ((swap_function ^ Suc n) ((A, f), B, g))) ` {..<Suc n} ∧
iset_to_index (snd ((swap_function ^ Suc n) ((A, f), B, g))) ` {..<Suc n} ⊂ A ∧
linear_independent (iset_to_index (snd ((swap_function ^ Suc n) ((A, f), B, g))) ` {..<Suc n}) ∧
Suc n = card (iset_to_index (snd ((swap_function ^ Suc n) ((A, f), B, g))) ` {..<Suc n})"
proof (rule conjI4)
have A_in_V: "A ⊆ carrier V"
by (metis good_set_in_carrier l_ind_good_set li_A)
def C=="iset_to_index (snd ((swap_function ^ Suc n) ((A, f), B, g))) ` {..<Suc n}"
show image_C: "f ` {..<Suc n} = C"
proof -
def A'≡"iset_to_set (fst ((swap_function ^ n) ((A, f), B, g)))"
def f'≡"iset_to_index (fst ((swap_function ^ n) ((A, f), B, g)))"
def B'≡"iset_to_set (snd ((swap_function ^ n) ((A, f), B, g)))"
def g'≡"iset_to_index (snd ((swap_function ^ n) ((A, f), B, g)))"
def C'≡"f ` {..<n}"
have "snd ((swap_function ^ Suc n) ((A, f), B, g))
=snd (swap_function ((swap_function ^ n) ((A, f), B, g)))"
using fun_power_suc_eq by metis
also have "...=snd (swap_function ((A',f'),(B',g')))"
using A'_def B'_def f'_def g'_def by simp
finally have descomposicion: "snd ((swap_function ^ Suc n) ((A, f), B, g)) =
snd (swap_function ((A', f'), B', g'))" .
have "∃y∈B'. iset_to_set (snd (swap_function ((A',f'),(B',g'))))=(insert (f' 0) (B'-{y})) ∧ y ∉ C' ∧
iset_to_index (snd (swap_function ((A', f'), B', g')))` {..<card (C') + 1} = C'∪{f' 0}"
proof (rule aux_swap_theorem1)
show "indexing (A', f')"
using fst_swap_function_power_indexing[OF indexing_A A_in_V, of n B g]
unfolding A'_def f'_def by simp
show "indexing (B', g')"
using snd_swap_function_power_indexing
[OF indexing_A indexing_B A_in_V B_in_V A_not_empty li_A sg_B zero_notin_B n_l_card]
unfolding B'_def g'_def by simp
show "B' ⊆ carrier V" unfolding B'_def
using swap_function_power_snd_in_carrier[OF indexing_A indexing_B A_in_V B_in_V
A_not_empty li_A sg_B zero_notin_B n_l_card] .
show "A' ≠ {}"
unfolding A'_def
using swap_function_power_fst_not_empty_if_n_l_cardA[OF indexing_A A_in_V n_l_card]
by presburger
show "spanning_set B'"
unfolding B'_def
using swap_function_power_preserves_sg[OF indexing_A indexing_B A_in_V B_in_V
A_not_empty li_A sg_B zero_notin_B n_l_card] .
show "\<zero>\<^bsub>V\<^esub> ∉ B'"
unfolding B'_def using zero_notin_snd_swap_function_power[OF indexing_A indexing_B A_in_V B_in_V
A_not_empty li_A sg_B zero_notin_B n_l_card] .
show "g' ` {..<card C'} = C'"
unfolding g'_def C'_def using hip by presburger
show "A' ∪ C' = A"
proof -
have "A'=f`{n..<card A}" using swap_function_fst_image_until_n[OF indexing_A A_not_empty n_l_card]
unfolding A'_def by auto
hence "A' ∪ C'=f`{n..<card A} ∪ f`{..<n}" unfolding C'_def by fast
also have "...=f`{..<card A}"
by (metis C'_def Un_commute `A' = f \` {n..<card A}`
image_Un ivl_disj_un(8) n_l_card nat_less_le)
also have "...=A" using indexing_A unfolding indexing_def bij_betw_def by simp
finally show ?thesis .
qed
show "A' ∩ C' = {}"
proof -
have "A'=f`{n..<card A}"
using swap_function_fst_image_until_n[OF indexing_A A_not_empty n_l_card]
unfolding A'_def by auto
hence "A' ∩ C'=f`{n..<card A} ∩ C'" by simp
also have "...=f`{n..<card A} ∩ f`{..<n}" unfolding C'_def ..
also have "...=f`({n..<card A} ∩ {..<n})"
proof (rule inj_on_image_Int[symmetric])
show "inj_on f {..<card A}" using indexing_A unfolding indexing_def bij_betw_def by simp
show "{n..<card A} ⊆ {..<card A}" using n_l_card by fastsimp
show "{..<n} ⊆ {..<card A}" using n_l_card by simp
qed
also have "...=f`{}" by auto
also have "...={}" by simp
finally show ?thesis .
qed
show "linear_independent A" using li_A .
qed
hence image: "iset_to_index (snd (swap_function ((A', f'), B', g')))` {..<card (C') + 1} = C'∪{f' 0}"
by fast
have "f`{..<Suc n}=f ` {..<n}∪{f' 0}"
proof -
have f'0_fn:"f' 0=f n" unfolding f'_def
using snd_fst_swap_function_image_0[OF indexing_A n_l_card, of B g] by simp
have "f`{..<Suc n}=f ` {..<n}∪{f n}"
by (metis C'_def Un_empty_right Un_insert_right image_insert lessThan_Suc)
also have "...=f ` {..<n}∪{f' 0}" using f'0_fn by presburger
finally show ?thesis .
qed
also have "...=C'∪{f' 0}" using C'_def by simp
also have "...=iset_to_index (snd (swap_function ((A', f'), B', g')))` {..<card (C') + 1}"
using image by fast
also have "...=iset_to_index (snd (swap_function ((A', f'), B', g')))` {..<Suc n}"
proof -
have igualdad_conjuntos: "{..<card (C') + 1}={..<Suc n}"
proof -
have "card C'= card {..<n}"
proof (unfold C'_def, rule card_image)
show "inj_on f {..<n}"using subset_inj_on indexing_A _n_l_card
unfolding indexing_def bij_betw_def by fastsimp
qed
also have "...=n" by simp
finally show ?thesis by simp
qed
thus ?thesis by presburger
qed
also have "...=iset_to_index (snd ((swap_function ^ Suc n) ((A, f), B, g)))` {..<Suc n}"
using C_def A'_def B'_def f'_def g'_def descomposicion by presburger
finally show ?thesis using C_def by presburger
qed
show "linear_independent C"
proof -
have "f ` {..<Suc n}⊆ A" using indexing_A suc_n_l_card unfolding indexing_def bij_betw_def by fastsimp
thus ?thesis using independent_set_implies_independent_subset using image_C li_A unfolding C_def by force
qed
show "C ⊂ A"
proof -
have "f` {..<Suc n} ⊂ f` {..<card A}"
proof (rule inj_on_strict_subset)
show "inj_on f {..<card A}" using indexing_A unfolding indexing_def bij_betw_def by simp
show "{..<Suc n} ⊂ {..<card A}" using suc_n_l_card by fastsimp
qed
thus ?thesis using indexing_A image_C unfolding indexing_def bij_betw_def C_def by auto
qed
show "Suc n = card C"
proof -
have "card C = card (f ` {..<Suc n})" using image_C by fast
also have "...= card {..<Suc n}"
proof (rule card_image)
show "inj_on f {..<Suc n}"
using subset_inj_on indexing_A suc_n_l_card
unfolding indexing_def bij_betw_def
by fastsimp
qed
also have "...= Suc n" using card_lessThan by simp
finally show ?thesis by presburger
qed
qed
qed
text{*At last, we can prove the swap theorem. We separate it in cases, when A is empty and when it is not.
We use the auxiliar lemma @{text aux_swap_theorem2}.*}
theorem swap_theorem_not_empty:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and A_not_empty: "A≠{}"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "card A ≤ card B"
proof (cases "card A ≤ card B")
case True thus ?thesis .
next
case False
have cardB_l_cardA: "card A > card B" using False by linarith
def C≡"iset_to_index(snd((swap_function^(card B)) ((A,f),(B,g))))`{..<card B}"
have C_eq: "C=iset_to_set(snd((swap_function^(card B)) ((A,f),(B,g))))"
using snd_swap_function_power_indexing
[OF indexing_A indexing_B A_in_V B_in_V A_not_empty
li_A sg_B zero_notin_B cardB_l_cardA]
unfolding C_def indexing_def bij_betw_def
using snd_swap_function_power_preserves_card
[OF indexing_A indexing_B A_in_V B_in_V
A_not_empty li_A sg_B zero_notin_B cardB_l_cardA]
by simp
have surjf_B_C: "f`{..<card B}=C"
and C_subset_A:"C ⊂ A"
and li_C:"linear_independent C"
and cB_eq_cC:"card B=card C"
using aux_swap_theorem2 assms cardB_l_cardA
unfolding C_def by auto
have spanning_set_C: "spanning_set C"
using swap_function_power_preserves_sg
[OF indexing_A indexing_B A_in_V B_in_V A_not_empty
li_A sg_B zero_notin_B cardB_l_cardA] C_eq
unfolding C_def by presburger
have "linear_dependent A"
proof -
have "∃x. x∈A ∧ x∉C" using C_subset_A by fast
from this obtain x where x_in_A: "x∈A" and x_notin_C: "x∉C"
by blast
show ?thesis
proof (rule linear_dependent_subset_implies_linear_dependent_set
[of "insert x C"])
show "insert x C ⊆ A" using C_subset_A and x_in_A by simp
show "good_set A" using li_A linear_independent_def by blast
show "linear_dependent (insert x C)"
proof (rule lc1)
show "linear_independent C" using li_C .
show x_in_V: " x ∈ carrier V"
by (metis good_set_def li_A linear_independent_def
subsetD x_in_A)
show "x ∉ C" using x_notin_C .
show "∃f. f ∈ coefficients_function (carrier V)
∧ linear_combination f C = x"
using spanning_set_C x_in_V
unfolding spanning_set_def by blast
qed
qed
qed
hence "¬ linear_independent A"
using dependent_implies_not_independent by simp
thus ?thesis using li_A by contradiction
qed
text{*Finally the theorem (every independent set has cardinal less than or equal to every spanning set) and some corollaries:*}
theorem swap_theorem:
assumes indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and A_in_V: "A ⊆ carrier V"
and B_in_V: "B ⊆ carrier V"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "card A ≤ card B"
proof (cases "A={}")
case True show ?thesis by (metis True card_eq_0_iff le0)
next
case False show ?thesis using swap_theorem_not_empty assms False by force
qed
text{*The next corollary omits the need of indexing functions for $A$ and $B$ (these are obtained through auxiliary lemmas).*}
corollary swap_theorem2:
assumes finite_B: "finite B"
and B_in_V: "B ⊆ carrier V"
and A_in_V: "A ⊆ carrier V"
and li_A: "linear_independent A"
and sg_B: "spanning_set B"
and zero_notin_B: "\<zero>\<^bsub>V\<^esub> ∉ B"
shows "card A ≤ card B"
proof -
have "∃f. indexing (A,f)" using obtain_indexing
by (metis good_set_finite l_ind_good_set li_A)
from this obtain f where indexing_A: "indexing (A,f)" by fast
have "∃g. indexing (B,g)" using obtain_indexing[OF finite_B] .
from this obtain g where indexing_B: "indexing (B,g)" by fast
show ?thesis using swap_theorem
[OF indexing_A indexing_B A_in_V B_in_V
li_A sg_B zero_notin_B] .
qed
text{*Now we can prove that the number of elements in any (finite) basis (of a finite-dimensional vector space)
is the same as in any other (finite) basis.*}
theorem eq_cardinality_basis:
assumes basis_B: "basis B"
and finite_B: "finite B"
shows "card X = card B"
proof -
have "∃f. indexing (X,f)" using obtain_indexing[OF finite_X] .
from this obtain f where indexing_X: "indexing (X,f)" by fast
have "∃g. indexing (B,g)" using obtain_indexing[OF finite_B] .
from this obtain g where indexing_B: "indexing (B,g)" by fast
have li_X: "linear_independent X" and sg_X: "spanning_set X"
using linear_independent_X and spanning_set_X by fast+
have gs_B: "good_set B"
using finite_basis_implies_good_set[OF basis_B finite_B] .
have li_B: "linear_independent B" and sg_B: "spanning_set B"
using basis_B finite_B unfolding basis_def
using fin_ind_ext_impl_ind
gs_spanning_ext_imp_spanning gs_B by blast+
have cardX_le_cardB: "card X ≤ card B"
proof (rule swap_theorem)
show "indexing (X, f)" using indexing_X .
show "indexing (B, g)" using indexing_B .
show "X ⊆ carrier V"
using finite_basis_implies_good_set[OF basis_X finite_X]
unfolding good_set_def by simp
show "B ⊆ carrier V"
using finite_basis_implies_good_set[OF basis_B finite_B]
unfolding good_set_def by simp
show "linear_independent X" using li_X .
show "spanning_set B" using sg_B .
show "\<zero>\<^bsub>V\<^esub> ∉ B"
using zero_not_in_linear_independent_set[OF li_B] .
qed
have cardX_ge_cardB: "card X ≥ card B"
proof (rule swap_theorem)
show "indexing (B, g)" using indexing_B .
show "indexing (X, f)" using indexing_X .
show "X ⊆ carrier V"
using finite_basis_implies_good_set[OF basis_X finite_X]
unfolding good_set_def by simp
show "B ⊆ carrier V"
using finite_basis_implies_good_set[OF basis_B finite_B]
unfolding good_set_def by simp
show "linear_independent B" using li_B .
show "spanning_set X" using sg_X .
show "\<zero>\<^bsub>V\<^esub> ∉ X"
using zero_not_in_linear_independent_set[OF li_X] .
qed
show ?thesis
using cardX_le_cardB and cardX_ge_cardB by presburger
qed
corollary eq_cardinality_basis2:
assumes basis_A: "basis A"
and finite_A: "finite A"
and basis_B: "basis B"
and finite_B: "finite B"
shows "card A = card B"
by (metis basis_A basis_B eq_cardinality_basis finite_A finite_B)
text{*We can make the definicion of dimension of a vector space and relationate the concept with above theorems.*}
text{*The dimension of a vector space is the cardinality of one of its basis. We have fixed X as a basis, so the
definition is trivial:*}
definition dimension :: "nat"
where "dimension = card X"
text{*If we have another basis, the dimension is equal to its cardinality.*}
lemma eq_dimension_basis:
assumes basis_A: "basis A"
and finite_A: "finite A"
shows "dimension = card A"
by (metis basis_A dimension_def eq_cardinality_basis finite_A)
text{*Whenever we have an independent set, we will know that its cardinality is less than the dimension of the vector space.*}
lemma card_li_le_dim:
assumes li_A: "linear_independent A"
shows "card A ≤ dimension"
proof -
have "∃f. indexing (X,f)" using obtain_indexing[OF finite_X] .
from this obtain f where indexing_X: "indexing (X,f)" by fast
have finite_A: "finite A"
by (metis assms good_set_finite l_ind_good_set)
have "∃g. indexing (A,g)" using obtain_indexing[OF finite_A] .
from this obtain g where indexing_A: "indexing (A,g)" by fast
have li_X: "linear_independent X" and sg_X: "spanning_set X"
by auto
show ?thesis
proof (unfold dimension_def, rule swap_theorem)
show "indexing (A, g)" using indexing_A .
show "indexing (X, f)" using indexing_X .
show "A ⊆ carrier V"
by (metis assms good_set_in_carrier l_ind_good_set)
show "X ⊆ carrier V"
by (metis good_set_X good_set_in_carrier)
show "linear_independent A" using li_A .
show "spanning_set X" using sg_X .
show "\<zero>\<^bsub>V\<^esub> ∉ X"by (metis li_X zero_not_in_linear_independent_set)
qed
qed
text{*Whenever the cardinality of a set is greater (strictly) than the dimension of $V$ then the set is dependent.*}
corollary card_g_dim_implies_ld:
assumes card_g_dim: "card A > dimension"
and A_in_V: "A ⊆ carrier V"
shows "linear_dependent A"
proof -
have finite_A: "finite A"
using card_g_dim finite_X unfolding dimension_def
by (metis card.empty card_g_dim
card_infinite card_li_le_dim dimension_def
empty_set_is_linearly_independent linorder_not_le)
hence cb_A: "good_set A"
using A_in_V unfolding good_set_def by fast
thus ?thesis using card_li_le_dim
by (metis card_g_dim dependent_if_only_if_not_independent
dimension_def less_not_refl xt1(8))
qed
text{*The following lemma proves that the cardinality of any spanning set is greater than the dimension.
In the infinite case (when $A$ is not finite but is a @{text spanning_set_ext}) it would be trivial, but Isabelle assigns
0 as the cardinality of an infinite set.*}
text{*We will use @{text swap_theorem}, so @{text "\<zero>\<^bsub>V\<^esub>"} must not be in the @{text spanning_set} over we apply it.*}
lemma card_sg_ge_dim:
assumes sg_A: "spanning_set A"
shows "card A ≥ dimension"
proof -
have finite_A: "finite A" and A_in_V: "A ⊆ carrier V"
using sg_A unfolding spanning_set_def and good_set_def
by fast+
have "∃f. indexing (X,f)" using obtain_indexing[OF finite_X] .
from this obtain f where indexing_X: "indexing (X,f)" by fast
have "∃g. indexing (A-{\<zero>\<^bsub>V\<^esub>},g)" using obtain_indexing finite_A
by blast
from this obtain g where indexing_A: "indexing (A-{\<zero>\<^bsub>V\<^esub>},g)"
by fast
have li_X: "linear_independent X" and sg_X: "spanning_set X"
by auto
have "card (A-{\<zero>\<^bsub>V\<^esub>}) ≥ dimension"
proof (unfold dimension_def, rule swap_theorem)
show "indexing (A-{\<zero>\<^bsub>V\<^esub>}, g)" using indexing_A .
show "indexing (X, f)" using indexing_X .
show "(A-{\<zero>\<^bsub>V\<^esub>}) ⊆ carrier V" using A_in_V by blast
show "linear_independent X" by simp
show "X ⊆ carrier V"
by (metis good_set_X good_set_in_carrier)
show "spanning_set (A-{\<zero>\<^bsub>V\<^esub>})"
by (metis A_in_V finite_A sg_A spanning_set_minus_zero)
show "\<zero>\<^bsub>V\<^esub> ∉ (A-{\<zero>\<^bsub>V\<^esub>})" by fast
qed
thus ?thesis by (metis card_Diff1_le finite_A le_trans)
qed
text{*There not exists a @{text spanning_set} with cardinality less than the dimension.*}
corollary card_less_dim_implies_not_sg:
assumes cardA_l_dim: "card A < dimension"
shows "¬ spanning_set A"
by (metis assms card_sg_ge_dim dimension_def
less_not_refl3 xt1(8))
text{*If we have a set which cardinality is equal to the dimension of a finite vector space, then it is a finite set.
We have to assume that the basis is not empty: if $X$ is empty, then $card(X) = 0 = card(A)$.
However and due to the implementation of cardinality in Isabelle (giving $0$ as the cardinality of an infinite set),
we could only prove that either $A$ is infinite or empty.*}
lemma card_eq_not_empty_basis_implies_finite:
assumes cardA_dim: "card A = dimension"
and X_not_empty: "X≠{}"
shows "finite A"
by (metis X_not_empty cardA_dim card_eq_0_iff
card_infinite dimension_def finite_X)
text{*Assuming that $A$ is in $V$, the problem is solved.*}
lemma card_eq_basis_implies_finite:
assumes cardA_dim: "card A = dimension"
and A_in_V: "A ⊆ carrier V"
shows "finite A"
proof (cases "X={}")
case True show ?thesis
by (metis A_in_V True finite.insertI finite_X
finite_subset span_basis_is_V span_empty)
next
case False show ?thesis
using card_eq_not_empty_basis_implies_finite
[OF cardA_dim False] .
qed
text{*If a set has cardinality equal to the dimension, if it is a basis then is independent.*}
lemma card_eq_basis_imp_li:
assumes cardA_dim: "card A = dimension"
shows "basis A ==> linear_independent A"
proof -
assume basis_A: "basis A"
hence A_in_V: "A ⊆ carrier V" unfolding basis_def by fast
show "linear_independent A"
proof (cases "X={}")
case False show ?thesis
using card_eq_not_empty_basis_implies_finite
[OF cardA_dim False]
and basis_A
unfolding basis_def linear_independent_ext_def
by (metis subset_refl)
next
case True
have "A={}" using A_in_V True
unfolding basis_def spanning_set_def
by (metis all_not_in_conv assms card.empty
card_eq_0_iff dimension_def finite.emptyI
finite.insertI finite_subset mem_def
span_basis_is_V span_empty)
thus ?thesis
using empty_set_is_linearly_independent by simp
qed
qed
text{*If we have an independent set with cardinality equal to the dimension, then this set is a basis.*}
lemma card_li_set_eq_basis_imp_li:
assumes card_eq_dim: "card A = dimension"
shows "linear_independent A ==> basis A"
proof -
assume li_A: "linear_independent A"
have finite_A: "finite A"
by (metis good_set_finite l_ind_good_set li_A)
have cb_A: "good_set A" using l_ind_good_set[OF li_A] .
show ?thesis
proof (unfold basis_def, rule conjI3)
show "A ⊆ carrier V"
using cb_A unfolding good_set_def by fast
show "linear_independent_ext A"
using independent_imp_independent_ext[OF li_A] .
show "spanning_set_ext A"
proof (cases "spanning_set A")
case True thus ?thesis
using spanning_imp_spanning_ext by fast
next
case False
show ?thesis
proof -
have "∃y. y ∈ (carrier V - span A)"
using False cb_A
unfolding span_def spanning_set_def by fast
from this obtain y
where y_in_V_minus_span: "y ∈ (carrier V - span A)"
by fast
hence "linear_independent (insert y A)"
using insert_y_notin_span_li[OF _ _ li_A]
y_in_V_minus_span by fast
hence "card (insert y A) ≤ dimension"
using card_li_le_dim by simp
hence "card A + 1 ≤ dimension"
using y_in_V_minus_span card_insert_if[OF finite_A]
not_in_span_impl_not_in_set[OF _ cb_A]
by simp
thus ?thesis using card_eq_dim by linarith
--"Contradiction: we have proved that card(A+1)@{text ≤}dimension
and card(A)=dimension."
qed
qed
qed
qed
text{*If a spanning set has cardinality equal to the dimension, then is independent (so a basis). *}
lemma card_sg_set_eq_basis_imp_li:
assumes card_eq_dim: "card A = dimension"
shows "spanning_set A ==> linear_independent A"
proof-
assume sg_A: "spanning_set A"
hence A_in_V: "A ⊆ carrier V"
unfolding spanning_set_def good_set_def by fast
show ?thesis
proof (cases "linear_independent A")
case True thus ?thesis .
next
case False
show ?thesis
proof (cases "X={}")
case True
have "A={}"
by (metis A_in_V True bot_apply card_eq_0_iff card_eq_dim
dimension_def ext finite.emptyI finite.insertI
rev_finite_subset span_basis_is_V span_empty)
thus ?thesis using empty_set_is_linearly_independent by simp
next
case False
have finite_A: "finite A"
by (metis False card_eq_dim
card_eq_not_empty_basis_implies_finite dimension_def)
have ld_A: "linear_dependent A"
by (metis A_in_V `¬ linear_independent A` good_set_def
dependent_if_only_if_not_independent finite_A)
have "∃y∈A. ∃g. g ∈ coefficients_function (carrier V)
∧ y = linear_combination g (A - {y})"
using exists_x_linear_combination2[OF ld_A] .
from this obtain y g where y_in_A: "y∈A"
and cf_g: "g ∈ coefficients_function (carrier V)"
and y_lc_Ay: "y = linear_combination g (A - {y})" by blast
have "span A = span (A-{y})"
proof (rule span_minus)
show "good_set A"
by (metis l_dep_good_set ld_A)
show "y ∈ A" using y_in_A .
show "∃g. g ∈ coefficients_function (carrier V)
∧ y = linear_combination g (A - {y})"
by (metis cf_g y_lc_Ay)
qed
hence sg_Ay: "spanning_set (A-{y})" using sg_A
by (metis A_in_V Diff_subset finite_A finite_Diff
good_set_def span_V_eq_spanning_set
spanning_set_implies_span_basis subset_trans)
have "¬ spanning_set (A-{y})"
proof (rule card_less_dim_implies_not_sg)
show "card (A - {y}) < dimension"
by (metis False card_Diff_singleton_if card_eq_dim
card_gt_0_iff diff_less dimension_def finite_A
finite_X y_in_A zero_less_one)
qed
thus ?thesis using sg_Ay by contradiction
--"CONTRADICTION: we have proved that the set @{term A} minus the element @{term y} is a @{text spanning_set} and at the same time
that it is not."
qed
qed
qed
corollary card_sg_set_eq_basis_imp_basis:
assumes card_eq_dim: "card A = dimension"
shows "spanning_set A ==> basis A"
by (metis assms card_li_set_eq_basis_imp_li
card_sg_set_eq_basis_imp_li)
lemma basis_iff_linear_independent:
assumes card_eq: "card A = dimension"
shows "basis A <-> linear_independent A"
by (metis assms card_eq_basis_imp_li
card_li_set_eq_basis_imp_li)
text{*We can remove from @{text eq_cardinality_basis2} the premises about finiteness:
we can prove that in a finite dimensional vector space there not exist infinite bases.*}
lemma
not_finite_A_contains_empty_set:
assumes A: "¬ finite A"
shows "{} ⊆ A"
using empty_subsetI [of A] .
lemma not_finite_diff:
assumes A: "¬ finite A"
shows "¬ finite (A - {x})"
using A by auto
lemma not_finite_diff_set:
assumes A: "¬ finite A"
and B: "finite B"
shows "¬ finite (A - B)"
using A B by auto
text{*We can obtain a subset with the number of elements that we want from an infinite set:*}
lemma subset_card_n:
assumes A: "¬ finite A"
shows "∀k::nat. ∃B. B ⊆ A ∧ card B = k"
proof (rule allI)
fix k
show "∃B⊆A. card B = k"
proof (induct k)
let ?P = "(λk C. C ⊆ A ∧ card C = k)"
case 0
show ?case
by (rule exI [of "?P 0" "{}"], intro conjI)
(rule not_finite_A_contains_empty_set [OF A], simp)
next
case (Suc k)
show ?case
proof -
obtain B where b: "B ⊆ A" and card_b: "card B = k"
using Suc.hyps by auto
show ?thesis
using b and card_b
proof (cases "k = 0")
case True
obtain x where x: "x ∈ A"
using A by (metis ex_in_conv finite.emptyI)
hence "{x} ⊆ A" and "card {x} = Suc 0" by simp_all
thus ?thesis unfolding True by auto
next
case False
have fin_B: "finite B" using card_b False by (metis card_eq_0_iff)
hence nfin_A_B: "¬ finite (A - B)"
using A by auto
then obtain x where x: "x ∈ A - B" by (metis ex_in_conv finite.emptyI)
show ?thesis
apply (rule exI [of _ "insert x B"])
using x card_b b
by auto (metis card_b card_insert_disjoint fin_B)
qed
qed
qed
qed
text{*Every basis of a finite dimensional vector space is finite
(because each set of cardinality greater than the dimension is linearly dependent (@{text card_g_dim_implies_ld}), so we can not
have an infinite basis).*}
lemma basis_not_infinite:
assumes basis_A: "basis A"
shows "finite A"
proof (rule classical)
assume not_finite: "¬ finite A"
from not_finite obtain B where card: "card B = dimension + 1"
and B_in_A: "B ⊆ A" using subset_card_n by blast
have li_ext_A: "linear_independent_ext A" by (metis assms basis_def)
have "linear_dependent_ext A"
proof (unfold linear_dependent_ext_def, rule exI[of _ "B"], rule conjI)
show "linear_dependent B"
proof (rule card_g_dim_implies_ld)
show "dimension < card B" using card by simp
show "B ⊆ carrier V" using B_in_A basis_A unfolding basis_def by fast
qed
show "B⊆A" using B_in_A .
qed
thus ?thesis using independent_ext_implies_not_dependent_ext[OF li_ext_A] by contradiction
qed
text{*Finally the theorem:*}
lemma eq_cardinality_basis':
assumes A: "basis A" and B: "basis B"
shows "card A = card B"
by (metis A B basis_not_infinite eq_cardinality_basis)
end
end