Theory Hilbert_Function
section ‹Direct Decompositions and Hilbert Functions›
theory Hilbert_Function
imports
"HOL-Combinatorics.Permutations"
Dube_Prelims
Degree_Section
begin
subsection ‹Direct Decompositions›
text ‹The main reason for defining ‹direct_decomp› in terms of lists rather than sets is that
lemma ‹direct_decomp_direct_decomp› can be proved easier. At some point one could invest the time
to re-define ‹direct_decomp› in terms of sets (possibly adding a couple of further assumptions to
‹direct_decomp_direct_decomp›).›
definition direct_decomp :: "'a set ⇒ 'a::comm_monoid_add set list ⇒ bool"
where "direct_decomp A ss ⟷ bij_betw sum_list (listset ss) A"
lemma direct_decompI:
"inj_on sum_list (listset ss) ⟹ sum_list ` listset ss = A ⟹ direct_decomp A ss"
by (simp add: direct_decomp_def bij_betw_def)
lemma direct_decompI_alt:
"(⋀qs. qs ∈ listset ss ⟹ sum_list qs ∈ A) ⟹ (⋀a. a ∈ A ⟹ ∃!qs∈listset ss. a = sum_list qs) ⟹
direct_decomp A ss"
by (auto simp: direct_decomp_def intro!: bij_betwI') blast
lemma direct_decompD:
assumes "direct_decomp A ss"
shows "qs ∈ listset ss ⟹ sum_list qs ∈ A" and "inj_on sum_list (listset ss)"
and "sum_list ` listset ss = A"
using assms by (auto simp: direct_decomp_def bij_betw_def)
lemma direct_decompE:
assumes "direct_decomp A ss" and "a ∈ A"
obtains qs where "qs ∈ listset ss" and "a = sum_list qs"
using assms by (auto simp: direct_decomp_def bij_betw_def)
lemma direct_decomp_unique:
"direct_decomp A ss ⟹ qs ∈ listset ss ⟹ qs' ∈ listset ss ⟹ sum_list qs = sum_list qs' ⟹
qs = qs'"
by (auto dest: direct_decompD simp: inj_on_def)
lemma direct_decomp_singleton: "direct_decomp A [A]"
proof (rule direct_decompI_alt)
fix qs
assume "qs ∈ listset [A]"
then obtain q where "q ∈ A" and "qs = [q]" by (rule listset_singletonE)
thus "sum_list qs ∈ A" by simp
next
fix a
assume "a ∈ A"
show "∃!qs∈listset [A]. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from ‹a ∈ A› refl show "[a] ∈ listset [A]" by (rule listset_singletonI)
next
fix qs
assume "qs ∈ listset [A] ∧ a = sum_list qs"
hence a: "a = sum_list qs" and "qs ∈ listset [A]" by simp_all
from this(2) obtain b where qs: "qs = [b]" by (rule listset_singletonE)
with a show "qs = [a]" by simp
qed simp_all
qed
lemma mset_bij:
assumes "bij_betw f {..<length xs} {..<length ys}" and "⋀i. i < length xs ⟹ xs ! i = ys ! f i"
shows "mset xs = mset ys"
proof -
from assms(1) have 1: "inj_on f {0..<length xs}" and 2: "f ` {0..<length xs} = {0..<length ys}"
by (simp_all add: bij_betw_def lessThan_atLeast0)
let ?f = "(!) ys ∘ f"
have "xs = map ?f [0..<length xs]" unfolding list_eq_iff_nth_eq
proof (intro conjI allI impI)
fix i
assume "i < length xs"
hence "xs ! i = ys ! f i" by (rule assms(2))
also from ‹i < length xs› have "… = map ((!) ys ∘ f) [0..<length xs] ! i" by simp
finally show "xs ! i = map ((!) ys ∘ f) [0..<length xs] ! i" .
qed simp
hence "mset xs = mset (map ?f [0..<length xs])" by (rule arg_cong)
also have "… = image_mset ((!) ys) (image_mset f (mset_set {0..<length xs}))"
by (simp flip: image_mset.comp)
also from 1 have "… = image_mset ((!) ys) (mset_set {0..<length ys})"
by (simp add: image_mset_mset_set 2)
also have "… = mset (map ((!) ys) [0..<length ys])" by simp
finally show "mset xs = mset ys" by (simp only: map_nth)
qed
lemma direct_decomp_perm:
assumes "direct_decomp A ss1" and "mset ss1 = mset ss2"
shows "direct_decomp A ss2"
proof -
from assms(2) have len_ss1: "length ss1 = length ss2"
using mset_eq_length by blast
from assms(2) obtain f where ‹f permutes {..<length ss2}›
‹permute_list f ss2 = ss1›
by (rule mset_eq_permutation)
then have f_bij: "bij_betw f {..<length ss2} {..<length ss1}"
and f: "⋀i. i < length ss2 ⟹ ss1 ! i = ss2 ! f i"
by (auto simp add: permutes_imp_bij permute_list_nth)
define g where "g = inv_into {..<length ss2} f"
from f_bij have g_bij: "bij_betw g {..<length ss1} {..<length ss2}"
unfolding g_def len_ss1 by (rule bij_betw_inv_into)
have f_g: "f (g i) = i" if "i < length ss1" for i
proof -
from that f_bij have "i ∈ f ` {..<length ss2}" by (simp add: bij_betw_def len_ss1)
thus ?thesis by (simp only: f_inv_into_f g_def)
qed
have g_f: "g (f i) = i" if "i < length ss2" for i
proof -
from f_bij have "inj_on f {..<length ss2}" by (simp only: bij_betw_def)
moreover from that have "i ∈ {..<length ss2}" by simp
ultimately show ?thesis by (simp add: g_def)
qed
have g: "ss2 ! i = ss1 ! g i" if "i < length ss1" for i
proof -
from that have "i ∈ {..<length ss2}" by (simp add: len_ss1)
hence "g i ∈ g ` {..<length ss2}" by (rule imageI)
also from g_bij have "… = {..<length ss2}" by (simp only: len_ss1 bij_betw_def)
finally have "g i < length ss2" by simp
hence "ss1 ! g i = ss2 ! f (g i)" by (rule f)
with that show ?thesis by (simp only: f_g)
qed
show ?thesis
proof (rule direct_decompI_alt)
fix qs2
assume "qs2 ∈ listset ss2"
then obtain qs1 where qs1_in: "qs1 ∈ listset ss1" and len_qs1: "length qs1 = length qs2"
and *: "⋀i. i < length qs2 ⟹ qs1 ! i = qs2 ! f i" using f_bij f by (rule listset_permE) blast+
from ‹qs2 ∈ listset ss2› have "length qs2 = length ss2" by (rule listsetD)
with f_bij have "bij_betw f {..<length qs1} {..<length qs2}" by (simp only: len_qs1 len_ss1)
hence "mset qs1 = mset qs2" using * by (rule mset_bij) (simp only: len_qs1)
hence "sum_list qs2 = sum_list qs1" by (simp flip: sum_mset_sum_list)
also from assms(1) qs1_in have "… ∈ A" by (rule direct_decompD)
finally show "sum_list qs2 ∈ A" .
next
fix a
assume "a ∈ A"
with assms(1) obtain qs where a: "a = sum_list qs" and qs_in: "qs ∈ listset ss1"
by (rule direct_decompE)
from qs_in obtain qs2 where qs2_in: "qs2 ∈ listset ss2" and len_qs2: "length qs2 = length qs"
and 1: "⋀i. i < length qs ⟹ qs2 ! i = qs ! g i" using g_bij g by (rule listset_permE) blast+
show "∃!qs∈listset ss2. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from qs_in have len_qs: "length qs = length ss1" by (rule listsetD)
with g_bij have g_bij2: "bij_betw g {..<length qs2} {..<length qs}" by (simp only: len_qs2 len_ss1)
hence "mset qs2 = mset qs" using 1 by (rule mset_bij) (simp only: len_qs2)
thus a2: "a = sum_list qs2" by (simp only: a flip: sum_mset_sum_list)
fix qs'
assume "qs' ∈ listset ss2 ∧ a = sum_list qs'"
hence qs'_in: "qs' ∈ listset ss2" and a': "a = sum_list qs'" by simp_all
from this(1) obtain qs1 where qs1_in: "qs1 ∈ listset ss1" and len_qs1: "length qs1 = length qs'"
and 2: "⋀i. i < length qs' ⟹ qs1 ! i = qs' ! f i" using f_bij f by (rule listset_permE) blast+
from ‹qs' ∈ listset ss2› have "length qs' = length ss2" by (rule listsetD)
with f_bij have "bij_betw f {..<length qs1} {..<length qs'}" by (simp only: len_qs1 len_ss1)
hence "mset qs1 = mset qs'" using 2 by (rule mset_bij) (simp only: len_qs1)
hence "sum_list qs1 = sum_list qs'" by (simp flip: sum_mset_sum_list)
hence "sum_list qs1 = sum_list qs" by (simp only: a flip: a')
with assms(1) qs1_in qs_in have "qs1 = qs" by (rule direct_decomp_unique)
show "qs' = qs2" unfolding list_eq_iff_nth_eq
proof (intro conjI allI impI)
from qs'_in have "length qs' = length ss2" by (rule listsetD)
thus eq: "length qs' = length qs2" by (simp only: len_qs2 len_qs len_ss1)
fix i
assume "i < length qs'"
hence "i < length qs2" by (simp only: eq)
hence "i ∈ {..<length qs2}" and "i < length qs" and "i < length ss1"
by (simp_all add: len_qs2 len_qs)
from this(1) have "g i ∈ g ` {..<length qs2}" by (rule imageI)
also from g_bij2 have "… = {..<length qs}" by (simp only: bij_betw_def)
finally have "g i < length qs'" by (simp add: eq len_qs2)
from ‹i < length qs› have "qs2 ! i = qs ! g i" by (rule 1)
also have "… = qs1 ! g i" by (simp only: ‹qs1 = qs›)
also from ‹g i < length qs'› have "… = qs' ! f (g i)" by (rule 2)
also from ‹i < length ss1› have "… = qs' ! i" by (simp only: f_g)
finally show "qs' ! i = qs2 ! i" by (rule sym)
qed
qed fact
qed
qed
lemma direct_decomp_split_map:
"direct_decomp A (map f ss) ⟹ direct_decomp A (map f (filter P ss) @ map f (filter (- P) ss))"
proof (rule direct_decomp_perm)
show "mset (map f ss) = mset (map f (filter P ss) @ map f (filter (- P) ss))"
by simp (metis image_mset_union multiset_partition)
qed
lemmas direct_decomp_split = direct_decomp_split_map[where f=id, simplified]
lemma direct_decomp_direct_decomp:
assumes "direct_decomp A (s # ss)" and "direct_decomp s rs"
shows "direct_decomp A (ss @ rs)" (is "direct_decomp A ?ss")
proof (rule direct_decompI_alt)
fix qs
assume "qs ∈ listset ?ss"
then obtain qs1 qs2 where qs1: "qs1 ∈ listset ss" and qs2: "qs2 ∈ listset rs" and qs: "qs = qs1 @ qs2"
by (rule listset_appendE)
have "sum_list qs = sum_list ((sum_list qs2) # qs1)" by (simp add: qs add.commute)
also from assms(1) have "… ∈ A"
proof (rule direct_decompD)
from assms(2) qs2 have "sum_list qs2 ∈ s" by (rule direct_decompD)
thus "sum_list qs2 # qs1 ∈ listset (s # ss)" using qs1 refl by (rule listset_ConsI)
qed
finally show "sum_list qs ∈ A" .
next
fix a
assume "a ∈ A"
with assms(1) obtain qs1 where qs1_in: "qs1 ∈ listset (s # ss)" and a: "a = sum_list qs1"
by (rule direct_decompE)
from qs1_in obtain qs11 qs12 where "qs11 ∈ s" and qs12_in: "qs12 ∈ listset ss"
and qs1: "qs1 = qs11 # qs12" by (rule listset_ConsE)
from assms(2) this(1) obtain qs2 where qs2_in: "qs2 ∈ listset rs" and qs11: "qs11 = sum_list qs2"
by (rule direct_decompE)
let ?qs = "qs12 @ qs2"
show "∃!qs∈listset ?ss. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from qs12_in qs2_in refl show "?qs ∈ listset ?ss" by (rule listset_appendI)
show "a = sum_list ?qs" by (simp add: a qs1 qs11 add.commute)
fix qs0
assume "qs0 ∈ listset ?ss ∧ a = sum_list qs0"
hence qs0_in: "qs0 ∈ listset ?ss" and a2: "a = sum_list qs0" by simp_all
from this(1) obtain qs01 qs02 where qs01_in: "qs01 ∈ listset ss" and qs02_in: "qs02 ∈ listset rs"
and qs0: "qs0 = qs01 @ qs02" by (rule listset_appendE)
note assms(1)
moreover from _ qs01_in refl have "(sum_list qs02) # qs01 ∈ listset (s # ss)" (is "?qs' ∈ _")
proof (rule listset_ConsI)
from assms(2) qs02_in show "sum_list qs02 ∈ s" by (rule direct_decompD)
qed
moreover note qs1_in
moreover from a2 have "sum_list ?qs' = sum_list qs1" by (simp add: qs0 a add.commute)
ultimately have "?qs' = qs11 # qs12" unfolding qs1 by (rule direct_decomp_unique)
hence "qs11 = sum_list qs02" and 1: "qs01 = qs12" by simp_all
from this(1) have "sum_list qs02 = sum_list qs2" by (simp only: qs11)
with assms(2) qs02_in qs2_in have "qs02 = qs2" by (rule direct_decomp_unique)
thus "qs0 = qs12 @ qs2" by (simp only: 1 qs0)
qed
qed
lemma sum_list_map_times: "sum_list (map ((*) x) xs) = (x::'a::semiring_0) * sum_list xs"
by (induct xs) (simp_all add: algebra_simps)
lemma direct_decomp_image_times:
assumes "direct_decomp (A::'a::semiring_0 set) ss" and "⋀a b. x * a = x * b ⟹ x ≠ 0 ⟹ a = b"
shows "direct_decomp ((*) x ` A) (map ((`) ((*) x)) ss)" (is "direct_decomp ?A ?ss")
proof (rule direct_decompI_alt)
fix qs
assume "qs ∈ listset ?ss"
then obtain qs0 where qs0_in: "qs0 ∈ listset ss" and qs: "qs = map ((*) x) qs0"
by (rule listset_map_imageE)
have "sum_list qs = x * sum_list qs0" by (simp only: qs sum_list_map_times)
moreover from assms(1) qs0_in have "sum_list qs0 ∈ A" by (rule direct_decompD)
ultimately show "sum_list qs ∈ (*) x ` A" by (rule image_eqI)
next
fix a
assume "a ∈ ?A"
then obtain a' where "a' ∈ A" and a: "a = x * a'" ..
from assms(1) this(1) obtain qs' where qs'_in: "qs' ∈ listset ss" and a': "a' = sum_list qs'"
by (rule direct_decompE)
define qs where "qs = map ((*) x) qs'"
show "∃!qs∈listset ?ss. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from qs'_in qs_def show "qs ∈ listset ?ss" by (rule listset_map_imageI)
fix qs0
assume "qs0 ∈ listset ?ss ∧ a = sum_list qs0"
hence "qs0 ∈ listset ?ss" and a0: "a = sum_list qs0" by simp_all
from this(1) obtain qs1 where qs1_in: "qs1 ∈ listset ss" and qs0: "qs0 = map ((*) x) qs1"
by (rule listset_map_imageE)
show "qs0 = qs"
proof (cases "x = 0")
case True
from qs1_in have "length qs1 = length ss" by (rule listsetD)
moreover from qs'_in have "length qs' = length ss" by (rule listsetD)
ultimately show ?thesis by (simp add: qs_def qs0 list_eq_iff_nth_eq True)
next
case False
have "x * sum_list qs1 = a" by (simp only: a0 qs0 sum_list_map_times)
also have "… = x * sum_list qs'" by (simp only: a' a)
finally have "sum_list qs1 = sum_list qs'" using False by (rule assms(2))
with assms(1) qs1_in qs'_in have "qs1 = qs'" by (rule direct_decomp_unique)
thus ?thesis by (simp only: qs0 qs_def)
qed
qed (simp only: a a' qs_def sum_list_map_times)
qed
lemma direct_decomp_appendD:
assumes "direct_decomp A (ss1 @ ss2)"
shows "{} ∉ set ss2 ⟹ direct_decomp (sum_list ` listset ss1) ss1" (is "_ ⟹ ?thesis1")
and "{} ∉ set ss1 ⟹ direct_decomp (sum_list ` listset ss2) ss2" (is "_ ⟹ ?thesis2")
and "direct_decomp A [sum_list ` listset ss1, sum_list ` listset ss2]" (is "direct_decomp _ ?ss")
proof -
have rl: "direct_decomp (sum_list ` listset ts1) ts1"
if "direct_decomp A (ts1 @ ts2)" and "{} ∉ set ts2" for ts1 ts2
proof (intro direct_decompI inj_onI refl)
fix qs1 qs2
assume qs1: "qs1 ∈ listset ts1" and qs2: "qs2 ∈ listset ts1"
assume eq: "sum_list qs1 = sum_list qs2"
from that(2) have "listset ts2 ≠ {}" by (simp add: listset_empty_iff)
then obtain qs3 where qs3: "qs3 ∈ listset ts2" by blast
note that(1)
moreover from qs1 qs3 refl have "qs1 @ qs3 ∈ listset (ts1 @ ts2)" by (rule listset_appendI)
moreover from qs2 qs3 refl have "qs2 @ qs3 ∈ listset (ts1 @ ts2)" by (rule listset_appendI)
moreover have "sum_list (qs1 @ qs3) = sum_list (qs2 @ qs3)" by (simp add: eq)
ultimately have "qs1 @ qs3 = qs2 @ qs3" by (rule direct_decomp_unique)
thus "qs1 = qs2" by simp
qed
{
assume "{} ∉ set ss2"
with assms show ?thesis1 by (rule rl)
}
{
from assms have "direct_decomp A (ss2 @ ss1)"
by (rule direct_decomp_perm) simp
moreover assume "{} ∉ set ss1"
ultimately show ?thesis2 by (rule rl)
}
show "direct_decomp A ?ss"
proof (rule direct_decompI_alt)
fix qs
assume "qs ∈ listset ?ss"
then obtain q1 q2 where q1: "q1 ∈ sum_list ` listset ss1" and q2: "q2 ∈ sum_list ` listset ss2"
and qs: "qs = [q1, q2]" by (rule listset_doubletonE)
from q1 obtain qs1 where qs1: "qs1 ∈ listset ss1" and q1: "q1 = sum_list qs1" ..
from q2 obtain qs2 where qs2: "qs2 ∈ listset ss2" and q2: "q2 = sum_list qs2" ..
from qs1 qs2 refl have "qs1 @ qs2 ∈ listset (ss1 @ ss2)" by (rule listset_appendI)
with assms have "sum_list (qs1 @ qs2) ∈ A" by (rule direct_decompD)
thus "sum_list qs ∈ A" by (simp add: qs q1 q2)
next
fix a
assume "a ∈ A"
with assms obtain qs0 where qs0_in: "qs0 ∈ listset (ss1 @ ss2)" and a: "a = sum_list qs0"
by (rule direct_decompE)
from this(1) obtain qs1 qs2 where qs1: "qs1 ∈ listset ss1" and qs2: "qs2 ∈ listset ss2"
and qs0: "qs0 = qs1 @ qs2" by (rule listset_appendE)
from qs1 have len_qs1: "length qs1 = length ss1" by (rule listsetD)
define qs where "qs = [sum_list qs1, sum_list qs2]"
show "∃!qs∈listset ?ss. a = sum_list qs"
proof (intro ex1I conjI)
from qs1 have "sum_list qs1 ∈ sum_list ` listset ss1" by (rule imageI)
moreover from qs2 have "sum_list qs2 ∈ sum_list ` listset ss2" by (rule imageI)
ultimately show "qs ∈ listset ?ss" using qs_def by (rule listset_doubletonI)
fix qs'
assume "qs' ∈ listset ?ss ∧ a = sum_list qs'"
hence "qs' ∈ listset ?ss" and a': "a = sum_list qs'" by simp_all
from this(1) obtain q1 q2 where q1: "q1 ∈ sum_list ` listset ss1"
and q2: "q2 ∈ sum_list ` listset ss2" and qs': "qs' = [q1, q2]" by (rule listset_doubletonE)
from q1 obtain qs1' where qs1': "qs1' ∈ listset ss1" and q1: "q1 = sum_list qs1'" ..
from q2 obtain qs2' where qs2': "qs2' ∈ listset ss2" and q2: "q2 = sum_list qs2'" ..
from qs1' have len_qs1': "length qs1' = length ss1" by (rule listsetD)
note assms
moreover from qs1' qs2' refl have "qs1' @ qs2' ∈ listset (ss1 @ ss2)" by (rule listset_appendI)
moreover note qs0_in
moreover have "sum_list (qs1' @ qs2') = sum_list qs0" by (simp add: a' qs' flip: a q1 q2)
ultimately have "qs1' @ qs2' = qs0" by (rule direct_decomp_unique)
also have "… = qs1 @ qs2" by fact
finally show "qs' = qs" by (simp add: qs_def qs' q1 q2 len_qs1 len_qs1')
qed (simp add: qs_def a qs0)
qed
qed
lemma direct_decomp_Cons_zeroI:
assumes "direct_decomp A ss"
shows "direct_decomp A ({0} # ss)"
proof (rule direct_decompI_alt)
fix qs
assume "qs ∈ listset ({0} # ss)"
then obtain q qs' where "q ∈ {0}" and "qs' ∈ listset ss" and "qs = q # qs'"
by (rule listset_ConsE)
from this(1, 3) have "sum_list qs = sum_list qs'" by simp
also from assms ‹qs' ∈ listset ss› have "… ∈ A" by (rule direct_decompD)
finally show "sum_list qs ∈ A" .
next
fix a
assume "a ∈ A"
with assms obtain qs' where qs': "qs' ∈ listset ss" and a: "a = sum_list qs'"
by (rule direct_decompE)
define qs where "qs = 0 # qs'"
show "∃!qs. qs ∈ listset ({0} # ss) ∧ a = sum_list qs"
proof (intro ex1I conjI)
from _ qs' qs_def show "qs ∈ listset ({0} # ss)" by (rule listset_ConsI) simp
next
fix qs0
assume "qs0 ∈ listset ({0} # ss) ∧ a = sum_list qs0"
hence "qs0 ∈ listset ({0} # ss)" and a0: "a = sum_list qs0" by simp_all
from this(1) obtain q0 qs0' where "q0 ∈ {0}" and qs0': "qs0' ∈ listset ss"
and qs0: "qs0 = q0 # qs0'" by (rule listset_ConsE)
from this(1, 3) have "sum_list qs0' = sum_list qs'" by (simp add: a0 flip: a)
with assms qs0' qs' have "qs0' = qs'" by (rule direct_decomp_unique)
with ‹q0 ∈ {0}› show "qs0 = qs" by (simp add: qs_def qs0)
qed (simp add: qs_def a)
qed
lemma direct_decomp_Cons_zeroD:
assumes "direct_decomp A ({0} # ss)"
shows "direct_decomp A ss"
proof -
have "direct_decomp {0} []" by (simp add: direct_decomp_def bij_betw_def)
with assms have "direct_decomp A (ss @ [])" by (rule direct_decomp_direct_decomp)
thus ?thesis by simp
qed
lemma direct_decomp_Cons_subsetI:
assumes "direct_decomp A (s # ss)" and "⋀s0. s0 ∈ set ss ⟹ 0 ∈ s0"
shows "s ⊆ A"
proof
fix x
assume "x ∈ s"
moreover from assms(2) have "map (λ_. 0) ss ∈ listset ss"
by (induct ss, auto simp del: listset.simps(2) intro: listset_ConsI)
ultimately have "x # (map (λ_. 0) ss) ∈ listset (s # ss)" using refl by (rule listset_ConsI)
with assms(1) have "sum_list (x # (map (λ_. 0) ss)) ∈ A" by (rule direct_decompD)
thus "x ∈ A" by simp
qed
lemma direct_decomp_Int_zero:
assumes "direct_decomp A ss" and "i < j" and "j < length ss" and "⋀s. s ∈ set ss ⟹ 0 ∈ s"
shows "ss ! i ∩ ss ! j = {0}"
proof -
from assms(2, 3) have "i < length ss" by (rule less_trans)
hence i_in: "ss ! i ∈ set ss" by simp
from assms(3) have j_in: "ss ! j ∈ set ss" by simp
show ?thesis
proof
show "ss ! i ∩ ss ! j ⊆ {0}"
proof
fix x
assume "x ∈ ss ! i ∩ ss ! j"
hence x_i: "x ∈ ss ! i" and x_j: "x ∈ ss ! j" by simp_all
have 1: "(map (λ_. 0) ss)[k := y] ∈ listset ss" if "k < length ss" and "y ∈ ss ! k" for k y
using assms(4) that
proof (induct ss arbitrary: k)
case Nil
from Nil(2) show ?case by simp
next
case (Cons s ss)
have *: "⋀s'. s' ∈ set ss ⟹ 0 ∈ s'" by (rule Cons.prems) simp
show ?case
proof (cases k)
case k: 0
with Cons.prems(3) have "y ∈ s" by simp
moreover from * have "map (λ_. 0) ss ∈ listset ss"
by (induct ss) (auto simp del: listset.simps(2) intro: listset_ConsI)
moreover have "(map (λ_. 0) (s # ss))[k := y] = y # map (λ_. 0) ss" by (simp add: k)
ultimately show ?thesis by (rule listset_ConsI)
next
case k: (Suc k')
have "0 ∈ s" by (rule Cons.prems) simp
moreover from * have "(map (λ_. 0) ss)[k' := y] ∈ listset ss"
proof (rule Cons.hyps)
from Cons.prems(2) show "k' < length ss" by (simp add: k)
next
from Cons.prems(3) show "y ∈ ss ! k'" by (simp add: k)
qed
moreover have "(map (λ_. 0) (s # ss))[k := y] = 0 # (map (λ_. 0) ss)[k' := y]"
by (simp add: k)
ultimately show ?thesis by (rule listset_ConsI)
qed
qed
have 2: "sum_list ((map (λ_. 0) ss)[k := y]) = y" if "k < length ss" for k and y::'a
using that by (induct ss arbitrary: k) (auto simp: add_ac split: nat.split)
define qs1 where "qs1 = (map (λ_. 0) ss)[i := x]"
define qs2 where "qs2 = (map (λ_. 0) ss)[j := x]"
note assms(1)
moreover from ‹i < length ss› x_i have "qs1 ∈ listset ss" unfolding qs1_def by (rule 1)
moreover from assms(3) x_j have "qs2 ∈ listset ss" unfolding qs2_def by (rule 1)
thm sum_list_update
moreover from ‹i < length ss› assms(3) have "sum_list qs1 = sum_list qs2"
by (simp add: qs1_def qs2_def 2)
ultimately have "qs1 = qs2" by (rule direct_decomp_unique)
hence "qs1 ! i = qs2 ! i" by simp
with ‹i < length ss› assms(2, 3) show "x ∈ {0}" by (simp add: qs1_def qs2_def)
qed
next
from i_in have "0 ∈ ss ! i" by (rule assms(4))
moreover from j_in have "0 ∈ ss ! j" by (rule assms(4))
ultimately show "{0} ⊆ ss ! i ∩ ss ! j" by simp
qed
qed
corollary direct_decomp_pairwise_zero:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ 0 ∈ s"
shows "pairwise (λs1 s2. s1 ∩ s2 = {0}) (set ss)"
proof (rule pairwiseI)
fix s1 s2
assume "s1 ∈ set ss"
then obtain i where "i < length ss" and s1: "s1 = ss ! i" by (metis in_set_conv_nth)
assume "s2 ∈ set ss"
then obtain j where "j < length ss" and s2: "s2 = ss ! j" by (metis in_set_conv_nth)
assume "s1 ≠ s2"
hence "i < j ∨ j < i" by (auto simp: s1 s2)
thus "s1 ∩ s2 = {0}"
proof
assume "i < j"
with assms(1) show ?thesis unfolding s1 s2 using ‹j < length ss› assms(2)
by (rule direct_decomp_Int_zero)
next
assume "j < i"
with assms(1) have "s2 ∩ s1 = {0}" unfolding s1 s2 using ‹i < length ss› assms(2)
by (rule direct_decomp_Int_zero)
thus ?thesis by (simp only: Int_commute)
qed
qed
corollary direct_decomp_repeated_eq_zero:
assumes "direct_decomp A ss" and "1 < count_list ss X" and "⋀s. s ∈ set ss ⟹ 0 ∈ s"
shows "X = {0}"
proof -
from assms(2) obtain i j where "i < j" and "j < length ss" and 1: "ss ! i = X" and 2: "ss ! j = X"
by (rule count_list_gr_1_E)
from assms(1) this(1, 2) assms(3) have "ss ! i ∩ ss ! j = {0}" by (rule direct_decomp_Int_zero)
thus ?thesis by (simp add: 1 2)
qed
corollary direct_decomp_map_Int_zero:
assumes "direct_decomp A (map f ss)" and "s1 ∈ set ss" and "s2 ∈ set ss" and "s1 ≠ s2"
and "⋀s. s ∈ set ss ⟹ 0 ∈ f s"
shows "f s1 ∩ f s2 = {0}"
proof -
from assms(2) obtain i where "i < length ss" and s1: "s1 = ss ! i" by (metis in_set_conv_nth)
from this(1) have i: "i < length (map f ss)" by simp
from assms(3) obtain j where "j < length ss" and s2: "s2 = ss ! j" by (metis in_set_conv_nth)
from this(1) have j: "j < length (map f ss)" by simp
have *: "0 ∈ s" if "s ∈ set (map f ss)" for s
proof -
from that obtain s' where "s' ∈ set ss" and s: "s = f s'" unfolding set_map ..
from this(1) show "0 ∈ s" unfolding s by (rule assms(5))
qed
show ?thesis
proof (rule linorder_cases)
assume "i < j"
with assms(1) have "(map f ss) ! i ∩ (map f ss) ! j = {0}"
using j * by (rule direct_decomp_Int_zero)
with i j show ?thesis by (simp add: s1 s2)
next
assume "j < i"
with assms(1) have "(map f ss) ! j ∩ (map f ss) ! i = {0}"
using i * by (rule direct_decomp_Int_zero)
with i j show ?thesis by (simp add: s1 s2 Int_commute)
next
assume "i = j"
with assms(4) show ?thesis by (simp add: s1 s2)
qed
qed
subsection ‹Direct Decompositions and Vector Spaces›
definition (in vector_space) is_basis :: "'b set ⇒ 'b set ⇒ bool"
where "is_basis V B ⟷ (B ⊆ V ∧ independent B ∧ V ⊆ span B ∧ card B = dim V)"
definition (in vector_space) some_basis :: "'b set ⇒ 'b set"
where "some_basis V = Eps (local.is_basis V)"
hide_const (open) real_vector.is_basis real_vector.some_basis
context vector_space
begin
lemma dim_empty [simp]: "dim {} = 0"
using dim_span_eq_card_independent independent_empty by fastforce
lemma dim_zero [simp]: "dim {0} = 0"
using dim_span_eq_card_independent independent_empty by fastforce
lemma independent_UnI:
assumes "independent A" and "independent B" and "span A ∩ span B = {0}"
shows "independent (A ∪ B)"
proof
from span_superset have "A ∩ B ⊆ span A ∩ span B" by blast
hence "A ∩ B = {}" unfolding assms(3) using assms(1, 2) dependent_zero by blast
assume "dependent (A ∪ B)"
then obtain T u v where "finite T" and "T ⊆ A ∪ B" and eq: "(∑v∈T. u v *s v) = 0"
and "v ∈ T" and "u v ≠ 0" unfolding dependent_explicit by blast
define TA where "TA = T ∩ A"
define TB where "TB = T ∩ B"
from ‹T ⊆ A ∪ B› have T: "T = TA ∪ TB" by (auto simp: TA_def TB_def)
from ‹finite T› have "finite TA" and "TA ⊆ A" by (simp_all add: TA_def)
from ‹finite T› have "finite TB" and "TB ⊆ B" by (simp_all add: TB_def)
from ‹A ∩ B = {}› ‹TA ⊆ A› this(2) have "TA ∩ TB = {}" by blast
have "0 = (∑v∈TA ∪ TB. u v *s v)" by (simp only: eq flip: T)
also have "… = (∑v∈TA. u v *s v) + (∑v∈TB. u v *s v)" by (rule sum.union_disjoint) fact+
finally have "(∑v∈TA. u v *s v) = (∑v∈TB. (- u) v *s v)" (is "?x = ?y")
by (simp add: sum_negf eq_neg_iff_add_eq_0)
from ‹finite TB› ‹TB ⊆ B› have "?y ∈ span B" by (auto simp: span_explicit simp del: uminus_apply)
moreover from ‹finite TA› ‹TA ⊆ A› have "?x ∈ span A" by (auto simp: span_explicit)
ultimately have "?y ∈ span A ∩ span B" by (simp add: ‹?x = ?y›)
hence "?x = 0" and "?y = 0" by (simp_all add: ‹?x = ?y› assms(3))
from ‹v ∈ T› have "v ∈ TA ∪ TB" by (simp only: T)
hence "u v = 0"
proof
assume "v ∈ TA"
with assms(1) ‹finite TA› ‹TA ⊆ A› ‹?x = 0› show "u v = 0" by (rule independentD)
next
assume "v ∈ TB"
with assms(2) ‹finite TB› ‹TB ⊆ B› ‹?y = 0› have "(- u) v = 0" by (rule independentD)
thus "u v = 0" by simp
qed
with ‹u v ≠ 0› show False ..
qed
lemma subspace_direct_decomp:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ subspace s"
shows "subspace A"
proof (rule subspaceI)
let ?qs = "map (λ_. 0) ss"
from assms(2) have "?qs ∈ listset ss"
by (induct ss) (auto simp del: listset.simps(2) dest: subspace_0 intro: listset_ConsI)
with assms(1) have "sum_list ?qs ∈ A" by (rule direct_decompD)
thus "0 ∈ A" by simp
next
fix p q
assume "p ∈ A"
with assms(1) obtain ps where ps: "ps ∈ listset ss" and p: "p = sum_list ps" by (rule direct_decompE)
assume "q ∈ A"
with assms(1) obtain qs where qs: "qs ∈ listset ss" and q: "q = sum_list qs" by (rule direct_decompE)
from ps qs have l: "length ps = length qs" by (simp only: listsetD)
from ps qs have "map2 (+) ps qs ∈ listset ss" (is "?qs ∈ _")
by (rule listset_closed_map2) (auto dest: assms(2) subspace_add)
with assms(1) have "sum_list ?qs ∈ A" by (rule direct_decompD)
thus "p + q ∈ A" using l by (simp only: p q sum_list_map2_plus)
next
fix c p
assume "p ∈ A"
with assms(1) obtain ps where "ps ∈ listset ss" and p: "p = sum_list ps" by (rule direct_decompE)
from this(1) have "map ((*s) c) ps ∈ listset ss" (is "?qs ∈ _")
by (rule listset_closed_map) (auto dest: assms(2) subspace_scale)
with assms(1) have "sum_list ?qs ∈ A" by (rule direct_decompD)
also have "sum_list ?qs = c *s sum_list ps" by (induct ps) (simp_all add: scale_right_distrib)
finally show "c *s p ∈ A" by (simp only: p)
qed
lemma is_basis_alt: "subspace V ⟹ is_basis V B ⟷ (independent B ∧ span B = V)"
by (metis (full_types) is_basis_def dim_eq_card span_eq span_eq_iff)
lemma is_basis_finite: "is_basis V A ⟹ is_basis V B ⟹ finite A ⟷ finite B"
unfolding is_basis_def using independent_span_bound by auto
lemma some_basis_is_basis: "is_basis V (some_basis V)"
proof -
obtain B where "B ⊆ V" and "independent B" and "V ⊆ span B" and "card B = dim V"
by (rule basis_exists)
hence "is_basis V B" by (simp add: is_basis_def)
thus ?thesis unfolding some_basis_def by (rule someI)
qed
corollary
shows some_basis_subset: "some_basis V ⊆ V"
and independent_some_basis: "independent (some_basis V)"
and span_some_basis_supset: "V ⊆ span (some_basis V)"
and card_some_basis: "card (some_basis V) = dim V"
using some_basis_is_basis[of V] by (simp_all add: is_basis_def)
lemma some_basis_not_zero: "0 ∉ some_basis V"
using independent_some_basis dependent_zero by blast
lemma span_some_basis: "subspace V ⟹ span (some_basis V) = V"
by (simp add: span_subspace some_basis_subset span_some_basis_supset)
lemma direct_decomp_some_basis_pairwise_disjnt:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ subspace s"
shows "pairwise (λs1 s2. disjnt (some_basis s1) (some_basis s2)) (set ss)"
proof (rule pairwiseI)
fix s1 s2
assume "s1 ∈ set ss" and "s2 ∈ set ss" and "s1 ≠ s2"
have "some_basis s1 ∩ some_basis s2 ⊆ s1 ∩ s2" using some_basis_subset by blast
also from direct_decomp_pairwise_zero have "… = {0}"
proof (rule pairwiseD)
fix s
assume "s ∈ set ss"
hence "subspace s" by (rule assms(2))
thus "0 ∈ s" by (rule subspace_0)
qed fact+
finally have "some_basis s1 ∩ some_basis s2 ⊆ {0}" .
with some_basis_not_zero show "disjnt (some_basis s1) (some_basis s2)"
unfolding disjnt_def by blast
qed
lemma direct_decomp_span_some_basis:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ subspace s"
shows "span (⋃(some_basis ` set ss)) = A"
proof -
from assms(1) have eq0[symmetric]: "sum_list ` listset ss = A" by (rule direct_decompD)
show ?thesis unfolding eq0 using assms(2)
proof (induct ss)
case Nil
show ?case by simp
next
case (Cons s ss)
have "subspace s" by (rule Cons.prems) simp
hence eq1: "span (some_basis s) = s" by (rule span_some_basis)
have "⋀s'. s' ∈ set ss ⟹ subspace s'" by (rule Cons.prems) simp
hence eq2: "span (⋃ (some_basis ` set ss)) = sum_list ` listset ss" by (rule Cons.hyps)
have "span (⋃ (some_basis ` set (s # ss))) = {x + y |x y. x ∈ s ∧ y ∈ sum_list ` listset ss}"
by (simp add: span_Un eq1 eq2)
also have "… = sum_list ` listset (s # ss)" (is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix a
assume "a ∈ ?A"
then obtain x y where "x ∈ s" and "y ∈ sum_list ` listset ss" and a: "a = x + y" by blast
from this(2) obtain qs where "qs ∈ listset ss" and y: "y = sum_list qs" ..
from ‹x ∈ s› this(1) refl have "x # qs ∈ listset (s # ss)" by (rule listset_ConsI)
hence "sum_list (x # qs) ∈ ?B" by (rule imageI)
also have "sum_list (x # qs) = a" by (simp add: a y)
finally show "a ∈ ?B" .
qed
next
show "?B ⊆ ?A"
proof
fix a
assume "a ∈ ?B"
then obtain qs' where "qs' ∈ listset (s # ss)" and a: "a = sum_list qs'" ..
from this(1) obtain x qs where "x ∈ s" and "qs ∈ listset ss" and qs': "qs' = x # qs"
by (rule listset_ConsE)
from this(2) have "sum_list qs ∈ sum_list ` listset ss" by (rule imageI)
moreover have "a = x + sum_list qs" by (simp add: a qs')
ultimately show "a ∈ ?A" using ‹x ∈ s› by blast
qed
qed
finally show ?case .
qed
qed
lemma direct_decomp_independent_some_basis:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ subspace s"
shows "independent (⋃(some_basis ` set ss))"
using assms
proof (induct ss arbitrary: A)
case Nil
from independent_empty show ?case by simp
next
case (Cons s ss)
have 1: "⋀s'. s' ∈ set ss ⟹ subspace s'" by (rule Cons.prems) simp
have "subspace s" by (rule Cons.prems) simp
hence "0 ∈ s" and eq1: "span (some_basis s) = s" by (rule subspace_0, rule span_some_basis)
from Cons.prems(1) have *: "direct_decomp A ([s] @ ss)" by simp
moreover from ‹0 ∈ s› have "{} ∉ set [s]" by auto
ultimately have 2: "direct_decomp (sum_list ` listset ss) ss" by (rule direct_decomp_appendD)
hence eq2: "span (⋃ (some_basis ` set ss)) = sum_list ` listset ss" using 1
by (rule direct_decomp_span_some_basis)
note independent_some_basis[of s]
moreover from 2 1 have "independent (⋃ (some_basis ` set ss))" by (rule Cons.hyps)
moreover have "span (some_basis s) ∩ span (⋃ (some_basis ` set ss)) = {0}"
proof -
from * have "direct_decomp A [sum_list ` listset [s], sum_list ` listset ss]"
by (rule direct_decomp_appendD)
hence "direct_decomp A [s, sum_list ` listset ss]" by (simp add: image_image)
moreover have "0 < (1::nat)" by simp
moreover have "1 < length [s, sum_list ` listset ss]" by simp
ultimately have "[s, sum_list ` listset ss] ! 0 ∩ [s, sum_list ` listset ss] ! 1 = {0}"
by (rule direct_decomp_Int_zero) (auto simp: ‹0 ∈ s› eq2[symmetric] span_zero)
thus ?thesis by (simp add: eq1 eq2)
qed
ultimately have "independent (some_basis s ∪ (⋃ (some_basis ` set ss)))"
by (rule independent_UnI)
thus ?case by simp
qed
corollary direct_decomp_is_basis:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ subspace s"
shows "is_basis A (⋃(some_basis ` set ss))"
proof -
from assms have "subspace A" by (rule subspace_direct_decomp)
moreover from assms have "span (⋃(some_basis ` set ss)) = A"
by (rule direct_decomp_span_some_basis)
moreover from assms have "independent (⋃(some_basis ` set ss))"
by (rule direct_decomp_independent_some_basis)
ultimately show ?thesis by (simp add: is_basis_alt)
qed
lemma dim_direct_decomp:
assumes "direct_decomp A ss" and "finite B" and "A ⊆ span B" and "⋀s. s ∈ set ss ⟹ subspace s"
shows "dim A = (∑s∈set ss. dim s)"
proof -
from assms(1, 4) have "is_basis A (⋃(some_basis ` set ss))"
(is "is_basis A ?B") by (rule direct_decomp_is_basis)
hence "dim A = card ?B" and "independent ?B" and "?B ⊆ A" by (simp_all add: is_basis_def)
from this(3) assms(3) have "?B ⊆ span B" by (rule subset_trans)
with assms(2) ‹independent ?B› have "finite ?B" using independent_span_bound by blast
note ‹dim A = card ?B›
also from finite_set have "card ?B = (∑s∈set ss. card (some_basis s))"
proof (intro card_UN_disjoint ballI impI)
fix s
assume "s ∈ set ss"
with ‹finite ?B› show "finite (some_basis s)" by auto
next
fix s1 s2
have "pairwise (λs t. disjnt (some_basis s) (some_basis t)) (set ss)"
using assms(1, 4) by (rule direct_decomp_some_basis_pairwise_disjnt)
moreover assume "s1 ∈ set ss" and "s2 ∈ set ss" and "s1 ≠ s2"
thm pairwiseD
ultimately have "disjnt (some_basis s1) (some_basis s2)" by (rule pairwiseD)
thus "some_basis s1 ∩ some_basis s2 = {}" by (simp only: disjnt_def)
qed
also from refl card_some_basis have "… = (∑s∈set ss. dim s)" by (rule sum.cong)
finally show ?thesis .
qed
end
subsection ‹Homogeneous Sets of Polynomials with Fixed Degree›
lemma homogeneous_set_direct_decomp:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ homogeneous_set s"
shows "homogeneous_set A"
proof (rule homogeneous_setI)
fix a n
assume "a ∈ A"
with assms(1) obtain qs where "qs ∈ listset ss" and a: "a = sum_list qs" by (rule direct_decompE)
have "hom_component a n = hom_component (sum_list qs) n" by (simp only: a)
also have "… = sum_list (map (λq. hom_component q n) qs)"
by (induct qs) (simp_all add: hom_component_plus)
also from assms(1) have "… ∈ A"
proof (rule direct_decompD)
show "map (λq. hom_component q n) qs ∈ listset ss"
proof (rule listset_closed_map)
fix s q
assume "s ∈ set ss"
hence "homogeneous_set s" by (rule assms(2))
moreover assume "q ∈ s"
ultimately show "hom_component q n ∈ s" by (rule homogeneous_setD)
qed fact
qed
finally show "hom_component a n ∈ A" .
qed
definition hom_deg_set :: "nat ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) set ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::zero) set"
where "hom_deg_set z A = (λa. hom_component a z) ` A"
lemma hom_deg_setD:
assumes "p ∈ hom_deg_set z A"
shows "homogeneous p" and "p ≠ 0 ⟹ poly_deg p = z"
proof -
from assms obtain a where "a ∈ A" and p: "p = hom_component a z" unfolding hom_deg_set_def ..
show *: "homogeneous p" by (simp only: p homogeneous_hom_component)
assume "p ≠ 0"
hence "keys p ≠ {}" by simp
then obtain t where "t ∈ keys p" by blast
with * have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
moreover from ‹t ∈ keys p› have "deg_pm t = z" unfolding p by (rule keys_hom_componentD)
ultimately show "poly_deg p = z" by simp
qed
lemma zero_in_hom_deg_set:
assumes "0 ∈ A"
shows "0 ∈ hom_deg_set z A"
proof -
have "0 = hom_component 0 z" by simp
also from assms have "… ∈ hom_deg_set z A" unfolding hom_deg_set_def by (rule imageI)
finally show ?thesis .
qed
lemma hom_deg_set_closed_uminus:
assumes "⋀a. a ∈ A ⟹ - a ∈ A" and "p ∈ hom_deg_set z A"
shows "- p ∈ hom_deg_set z A"
proof -
from assms(2) obtain a where "a ∈ A" and p: "p = hom_component a z" unfolding hom_deg_set_def ..
from this(1) have "- a ∈ A" by (rule assms(1))
moreover have "- p = hom_component (- a) z" by (simp add: p)
ultimately show ?thesis unfolding hom_deg_set_def by (rule rev_image_eqI)
qed
lemma hom_deg_set_closed_plus:
assumes "⋀a1 a2. a1 ∈ A ⟹ a2 ∈ A ⟹ a1 + a2 ∈ A"
and "p ∈ hom_deg_set z A" and "q ∈ hom_deg_set z A"
shows "p + q ∈ hom_deg_set z A"
proof -
from assms(2) obtain a1 where "a1 ∈ A" and p: "p = hom_component a1 z" unfolding hom_deg_set_def ..
from assms(3) obtain a2 where "a2 ∈ A" and q: "q = hom_component a2 z" unfolding hom_deg_set_def ..
from ‹a1 ∈ A› this(1) have "a1 + a2 ∈ A" by (rule assms(1))
moreover have "p + q = hom_component (a1 + a2) z" by (simp only: p q hom_component_plus)
ultimately show ?thesis unfolding hom_deg_set_def by (rule rev_image_eqI)
qed
lemma hom_deg_set_closed_minus:
assumes "⋀a1 a2. a1 ∈ A ⟹ a2 ∈ A ⟹ a1 - a2 ∈ A"
and "p ∈ hom_deg_set z A" and "q ∈ hom_deg_set z A"
shows "p - q ∈ hom_deg_set z A"
proof -
from assms(2) obtain a1 where "a1 ∈ A" and p: "p = hom_component a1 z" unfolding hom_deg_set_def ..
from assms(3) obtain a2 where "a2 ∈ A" and q: "q = hom_component a2 z" unfolding hom_deg_set_def ..
from ‹a1 ∈ A› this(1) have "a1 - a2 ∈ A" by (rule assms(1))
moreover have "p - q = hom_component (a1 - a2) z" by (simp only: p q hom_component_minus)
ultimately show ?thesis unfolding hom_deg_set_def by (rule rev_image_eqI)
qed
lemma hom_deg_set_closed_scalar:
assumes "⋀a. a ∈ A ⟹ c ⋅ a ∈ A" and "p ∈ hom_deg_set z A"
shows "(c::'a::semiring_0) ⋅ p ∈ hom_deg_set z A"
proof -
from assms(2) obtain a where "a ∈ A" and p: "p = hom_component a z" unfolding hom_deg_set_def ..
from this(1) have "c ⋅ a ∈ A" by (rule assms(1))
moreover have "c ⋅ p = hom_component (c ⋅ a) z"
by (simp add: p punit.map_scale_eq_monom_mult hom_component_monom_mult)
ultimately show ?thesis unfolding hom_deg_set_def by (rule rev_image_eqI)
qed
lemma hom_deg_set_closed_sum:
assumes "0 ∈ A" and "⋀a1 a2. a1 ∈ A ⟹ a2 ∈ A ⟹ a1 + a2 ∈ A"
and "⋀i. i ∈ I ⟹ f i ∈ hom_deg_set z A"
shows "sum f I ∈ hom_deg_set z A"
using assms(3)
proof (induct I rule: infinite_finite_induct)
case (infinite I)
with assms(1) show ?case by (simp add: zero_in_hom_deg_set)
next
case empty
with assms(1) show ?case by (simp add: zero_in_hom_deg_set)
next
case (insert j I)
from insert.hyps(1, 2) have "sum f (insert j I) = f j + sum f I" by simp
also from assms(2) have "… ∈ hom_deg_set z A"
proof (intro hom_deg_set_closed_plus insert.hyps)
show "f j ∈ hom_deg_set z A" by (rule insert.prems) simp
next
fix i
assume "i ∈ I"
hence "i ∈ insert j I" by simp
thus "f i ∈ hom_deg_set z A" by (rule insert.prems)
qed
finally show ?case .
qed
lemma hom_deg_set_subset: "homogeneous_set A ⟹ hom_deg_set z A ⊆ A"
by (auto dest: homogeneous_setD simp: hom_deg_set_def)
lemma Polys_closed_hom_deg_set:
assumes "A ⊆ P[X]"
shows "hom_deg_set z A ⊆ P[X]"
proof
fix p
assume "p ∈ hom_deg_set z A"
then obtain p' where "p' ∈ A" and p: "p = hom_component p' z" unfolding hom_deg_set_def ..
from this(1) assms have "p' ∈ P[X]" ..
have "keys p ⊆ keys p'" by (simp add: p keys_hom_component)
also from ‹p' ∈ P[X]› have "… ⊆ .[X]" by (rule PolysD)
finally show "p ∈ P[X]" by (rule PolysI)
qed
lemma hom_deg_set_alt_homogeneous_set:
assumes "homogeneous_set A"
shows "hom_deg_set z A = {p ∈ A. homogeneous p ∧ (p = 0 ∨ poly_deg p = z)}" (is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix h
assume "h ∈ ?A"
also from assms have "… ⊆ A" by (rule hom_deg_set_subset)
finally show "h ∈ ?B" using ‹h ∈ ?A› by (auto dest: hom_deg_setD)
qed
next
show "?B ⊆ ?A"
proof
fix h
assume "h ∈ ?B"
hence "h ∈ A" and "homogeneous h" and "h = 0 ∨ poly_deg h = z" by simp_all
from this(3) show "h ∈ ?A"
proof
assume "h = 0"
with ‹h ∈ A› have "0 ∈ A" by simp
thus ?thesis unfolding ‹h = 0› by (rule zero_in_hom_deg_set)
next
assume "poly_deg h = z"
with ‹homogeneous h› have "h = hom_component h z" by (simp add: hom_component_of_homogeneous)
with ‹h ∈ A› show ?thesis unfolding hom_deg_set_def by (rule rev_image_eqI)
qed
qed
qed
lemma hom_deg_set_sum_list_listset:
assumes "A = sum_list ` listset ss"
shows "hom_deg_set z A = sum_list ` listset (map (hom_deg_set z) ss)" (is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix h
assume "h ∈ ?A"
then obtain a where "a ∈ A" and h: "h = hom_component a z" unfolding hom_deg_set_def ..
from this(1) obtain qs where "qs ∈ listset ss" and a: "a = sum_list qs" unfolding assms ..
have "h = hom_component (sum_list qs) z" by (simp only: a h)
also have "… = sum_list (map (λq. hom_component q z) qs)"
by (induct qs) (simp_all add: hom_component_plus)
also have "… ∈ ?B"
proof (rule imageI)
show "map (λq. hom_component q z) qs ∈ listset (map (hom_deg_set z) ss)"
unfolding hom_deg_set_def using ‹qs ∈ listset ss› refl by (rule listset_map_imageI)
qed
finally show "h ∈ ?B" .
qed
next
show "?B ⊆ ?A"
proof
fix h
assume "h ∈ ?B"
then obtain qs where "qs ∈ listset (map (hom_deg_set z) ss)" and h: "h = sum_list qs" ..
from this(1) obtain qs' where "qs' ∈ listset ss" and qs: "qs = map (λq. hom_component q z) qs'"
unfolding hom_deg_set_def by (rule listset_map_imageE)
have "h = sum_list (map (λq. hom_component q z) qs')" by (simp only: h qs)
also have "… = hom_component (sum_list qs') z" by (induct qs') (simp_all add: hom_component_plus)
finally have "h = hom_component (sum_list qs') z" .
moreover have "sum_list qs' ∈ A" unfolding assms using ‹qs' ∈ listset ss› by (rule imageI)
ultimately show "h ∈ ?A" unfolding hom_deg_set_def by (rule image_eqI)
qed
qed
lemma direct_decomp_hom_deg_set:
assumes "direct_decomp A ss" and "⋀s. s ∈ set ss ⟹ homogeneous_set s"
shows "direct_decomp (hom_deg_set z A) (map (hom_deg_set z) ss)"
proof (rule direct_decompI)
from assms(1) have "sum_list ` listset ss = A" by (rule direct_decompD)
from this[symmetric] show "sum_list ` listset (map (hom_deg_set z) ss) = hom_deg_set z A"
by (simp only: hom_deg_set_sum_list_listset)
next
from assms(1) have "inj_on sum_list (listset ss)" by (rule direct_decompD)
moreover have "listset (map (hom_deg_set z) ss) ⊆ listset ss"
proof (rule listset_mono)
fix i
assume "i < length ss"
hence "map (hom_deg_set z) ss ! i = hom_deg_set z (ss ! i)" by simp
also from ‹i < length ss› have "… ⊆ ss ! i" by (intro hom_deg_set_subset assms(2) nth_mem)
finally show "map (hom_deg_set z) ss ! i ⊆ ss ! i" .
qed simp
ultimately show "inj_on sum_list (listset (map (hom_deg_set z) ss))" by (rule inj_on_subset)
qed
subsection ‹Interpreting Polynomial Rings as Vector Spaces over the Coefficient Field›
text ‹There is no need to set up any further interpretation, since interpretation ‹phull› is exactly
what we need.›
lemma subspace_ideal: "phull.subspace (ideal (F::('b::comm_powerprod ⇒⇩0 'a::field) set))"
using ideal.span_zero ideal.span_add
proof (rule phull.subspaceI)
fix c p
assume "p ∈ ideal F"
thus "c ⋅ p ∈ ideal F" unfolding map_scale_eq_times by (rule ideal.span_scale)
qed
lemma subspace_Polys: "phull.subspace (P[X]::(('x ⇒⇩0 nat) ⇒⇩0 'a::field) set)"
using zero_in_Polys Polys_closed_plus Polys_closed_map_scale by (rule phull.subspaceI)
lemma subspace_hom_deg_set:
assumes "phull.subspace A"
shows "phull.subspace (hom_deg_set z A)" (is "phull.subspace ?A")
proof (rule phull.subspaceI)
from assms have "0 ∈ A" by (rule phull.subspace_0)
thus "0 ∈ ?A" by (rule zero_in_hom_deg_set)
next
fix p q
assume "p ∈ ?A" and "q ∈ ?A"
with phull.subspace_add show "p + q ∈ ?A" by (rule hom_deg_set_closed_plus) (rule assms)
next
fix c p
assume "p ∈ ?A"
with phull.subspace_scale show "c ⋅ p ∈ ?A" by (rule hom_deg_set_closed_scalar) (rule assms)
qed
lemma hom_deg_set_Polys_eq_span:
"hom_deg_set z P[X] = phull.span (monomial (1::'a::field) ` deg_sect X z)" (is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix p
assume "p ∈ ?A"
also from this have "… = {p ∈ P[X]. homogeneous p ∧ (p = 0 ∨ poly_deg p = z)}"
by (simp only: hom_deg_set_alt_homogeneous_set[OF homogeneous_set_Polys])
finally have "p ∈ P[X]" and "homogeneous p" and "p ≠ 0 ⟹ poly_deg p = z" by simp_all
thus "p ∈ ?B"
proof (induct p rule: poly_mapping_plus_induct)
case 1
from phull.span_zero show ?case .
next
case (2 p c t)
let ?m = "monomial c t"
from 2(1) have "t ∈ keys ?m" by simp
hence "t ∈ keys (?m + p)" using 2(2) by (rule in_keys_plusI1)
hence "?m + p ≠ 0" by auto
hence "poly_deg (monomial c t + p) = z" by (rule 2)
from 2(4) have "keys (?m + p) ⊆ .[X]" by (rule PolysD)
with ‹t ∈ keys (?m + p)› have "t ∈ .[X]" ..
hence "?m ∈ P[X]" by (rule Polys_closed_monomial)
have "t ∈ deg_sect X z"
proof (rule deg_sectI)
from 2(5) ‹t ∈ keys (?m + p)› have "deg_pm t = poly_deg (?m + p)"
by (rule homogeneousD_poly_deg)
also have "… = z" by fact
finally show "deg_pm t = z" .
qed fact
hence "monomial 1 t ∈ monomial 1 ` deg_sect X z" by (rule imageI)
hence "monomial 1 t ∈ ?B" by (rule phull.span_base)
hence "c ⋅ monomial 1 t ∈ ?B" by (rule phull.span_scale)
hence "?m ∈ ?B" by simp
moreover have "p ∈ ?B"
proof (rule 2)
from 2(4) ‹?m ∈ P[X]› have "(?m + p) - ?m ∈ P[X]" by (rule Polys_closed_minus)
thus "p ∈ P[X]" by simp
next
have 1: "deg_pm s = z" if "s ∈ keys p" for s
proof -
from that 2(2) have "s ≠ t" by blast
hence "s ∉ keys ?m" by simp
with that have "s ∈ keys (?m + p)" by (rule in_keys_plusI2)
with 2(5) have "deg_pm s = poly_deg (?m + p)" by (rule homogeneousD_poly_deg)
also have "… = z" by fact
finally show ?thesis .
qed
show "homogeneous p" by (rule homogeneousI) (simp add: 1)
assume "p ≠ 0"
show "poly_deg p = z"
proof (rule antisym)
show "poly_deg p ≤ z" by (rule poly_deg_leI) (simp add: 1)
next
from ‹p ≠ 0› have "keys p ≠ {}" by simp
then obtain s where "s ∈ keys p" by blast
hence "z = deg_pm s" by (simp only: 1)
also from ‹s ∈ keys p› have "… ≤ poly_deg p" by (rule poly_deg_max_keys)
finally show "z ≤ poly_deg p" .
qed
qed
ultimately show ?case by (rule phull.span_add)
qed
qed
next
show "?B ⊆ ?A"
proof
fix p
assume "p ∈ ?B"
then obtain M u where "M ⊆ monomial 1 ` deg_sect X z" and "finite M" and p: "p = (∑m∈M. u m ⋅ m)"
by (auto simp: phull.span_explicit)
from this(1) obtain T where "T ⊆ deg_sect X z" and M: "M = monomial 1 ` T"
and inj: "inj_on (monomial (1::'a)) T" by (rule subset_imageE_inj)
define c where "c = (λt. u (monomial 1 t))"
from inj have "p = (∑t∈T. monomial (c t) t)" by (simp add: p M sum.reindex c_def)
also have "… ∈ ?A"
proof (intro hom_deg_set_closed_sum zero_in_Polys Polys_closed_plus)
fix t
assume "t ∈ T"
hence "t ∈ deg_sect X z" using ‹T ⊆ deg_sect X z› ..
hence "t ∈ .[X]" and eq: "deg_pm t = z" by (rule deg_sectD)+
from this(1) have "monomial (c t) t ∈ P[X]" (is "?m ∈ _") by (rule Polys_closed_monomial)
thus "?m ∈ ?A"
by (simp add: hom_deg_set_alt_homogeneous_set[OF homogeneous_set_Polys] poly_deg_monomial
monomial_0_iff eq)
qed
finally show "p ∈ ?A" .
qed
qed
subsection ‹(Projective) Hilbert Function›
interpretation phull: vector_space map_scale
apply standard
subgoal by (fact map_scale_distrib_left)
subgoal by (fact map_scale_distrib_right)
subgoal by (fact map_scale_assoc)
subgoal by (fact map_scale_one_left)
done
definition Hilbert_fun :: "(('x ⇒⇩0 nat) ⇒⇩0 'a::field) set ⇒ nat ⇒ nat"
where "Hilbert_fun A z = phull.dim (hom_deg_set z A)"
lemma Hilbert_fun_empty [simp]: "Hilbert_fun {} = 0"
by (rule ext) (simp add: Hilbert_fun_def hom_deg_set_def)
lemma Hilbert_fun_zero [simp]: "Hilbert_fun {0} = 0"
by (rule ext) (simp add: Hilbert_fun_def hom_deg_set_def)
lemma Hilbert_fun_direct_decomp:
assumes "finite X" and "A ⊆ P[X]" and "direct_decomp (A::(('x::countable ⇒⇩0 nat) ⇒⇩0 'a::field) set) ps"
and "⋀s. s ∈ set ps ⟹ homogeneous_set s" and "⋀s. s ∈ set ps ⟹ phull.subspace s"
shows "Hilbert_fun A z = (∑p∈set ps. Hilbert_fun p z)"
proof -
from assms(3, 4) have dd: "direct_decomp (hom_deg_set z A) (map (hom_deg_set z) ps)"
by (rule direct_decomp_hom_deg_set)
have "Hilbert_fun A z = phull.dim (hom_deg_set z A)" by (fact Hilbert_fun_def)
also from dd have "… = sum phull.dim (set (map (hom_deg_set z) ps))"
proof (rule phull.dim_direct_decomp)
from assms(1) have "finite (deg_sect X z)" by (rule finite_deg_sect)
thus "finite (monomial (1::'a) ` deg_sect X z)" by (rule finite_imageI)
next
from assms(2) have "hom_deg_set z A ⊆ hom_deg_set z P[X]"
unfolding hom_deg_set_def by (rule image_mono)
thus "hom_deg_set z A ⊆ phull.span (monomial 1 ` deg_sect X z)"
by (simp only: hom_deg_set_Polys_eq_span)
next
fix s
assume "s ∈ set (map (hom_deg_set z) ps)"
then obtain s' where "s' ∈ set ps" and s: "s = hom_deg_set z s'" unfolding set_map ..
from this(1) have "phull.subspace s'" by (rule assms(5))
thus "phull.subspace s" unfolding s by (rule subspace_hom_deg_set)
qed
also have "… = sum (phull.dim ∘ hom_deg_set z) (set ps)" unfolding set_map using finite_set
proof (rule sum.reindex_nontrivial)
fix s1 s2
note dd
moreover assume "s1 ∈ set ps" and "s2 ∈ set ps" and "s1 ≠ s2"
moreover have "0 ∈ hom_deg_set z s" if "s ∈ set ps" for s
proof (rule zero_in_hom_deg_set)
from that have "phull.subspace s" by (rule assms(5))
thus "0 ∈ s" by (rule phull.subspace_0)
qed
ultimately have "hom_deg_set z s1 ∩ hom_deg_set z s2 = {0}" by (rule direct_decomp_map_Int_zero)
moreover assume "hom_deg_set z s1 = hom_deg_set z s2"
ultimately show "phull.dim (hom_deg_set z s1) = 0" by simp
qed
also have "… = (∑p∈set ps. Hilbert_fun p z)" by (simp only: o_def Hilbert_fun_def)
finally show ?thesis .
qed
context pm_powerprod
begin
lemma image_lt_hom_deg_set:
assumes "homogeneous_set A"
shows "lpp ` (hom_deg_set z A - {0}) = {t ∈ lpp ` (A - {0}). deg_pm t = z}" (is "?B = ?A")
proof (intro set_eqI iffI)
fix t
assume "t ∈ ?A"
hence "t ∈ lpp ` (A - {0})" and deg_t[symmetric]: "deg_pm t = z" by simp_all
from this(1) obtain p where "p ∈ A - {0}" and t: "t = lpp p" ..
from this(1) have "p ∈ A" and "p ≠ 0" by simp_all
from this(1) have 1: "hom_component p z ∈ hom_deg_set z A" (is "?p ∈ _")
unfolding hom_deg_set_def by (rule imageI)
from ‹p ≠ 0› have "?p ≠ 0" and "lpp ?p = t" unfolding t deg_t by (rule hom_component_lpp)+
note this(2)[symmetric]
moreover from 1 ‹?p ≠ 0› have "?p ∈ hom_deg_set z A - {0}" by simp
ultimately show "t ∈ ?B" by (rule image_eqI)
next
fix t
assume "t ∈ ?B"
then obtain p where "p ∈ hom_deg_set z A - {0}" and t: "t = lpp p" ..
from this(1) have "p ∈ hom_deg_set z A" and "p ≠ 0" by simp_all
with assms have "p ∈ A" and "homogeneous p" and "poly_deg p = z"
by (simp_all add: hom_deg_set_alt_homogeneous_set)
from this(1) ‹p ≠ 0› have "p ∈ A - {0}" by simp
hence 1: "t ∈ lpp ` (A - {0})" using t by (rule rev_image_eqI)
from ‹p ≠ 0› have "t ∈ keys p" unfolding t by (rule punit.lt_in_keys)
with ‹homogeneous p› have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
with 1 show "t ∈ ?A" by (simp add: ‹poly_deg p = z›)
qed
lemma Hilbert_fun_alt:
assumes "finite X" and "A ⊆ P[X]" and "phull.subspace A"
shows "Hilbert_fun A z = card (lpp ` (hom_deg_set z A - {0}))" (is "_ = card ?A")
proof -
have "?A ⊆ lpp ` (hom_deg_set z A - {0})" by simp
then obtain B where sub: "B ⊆ hom_deg_set z A - {0}" and eq1: "?A = lpp ` B"
and inj: "inj_on lpp B" by (rule subset_imageE_inj)
have "Hilbert_fun A z = phull.dim (hom_deg_set z A)" by (fact Hilbert_fun_def)
also have "… = card B"
proof (rule phull.dim_eq_card)
show "phull.span B = phull.span (hom_deg_set z A)"
proof
from sub have "B ⊆ hom_deg_set z A" by blast
thus "phull.span B ⊆ phull.span (hom_deg_set z A)" by (rule phull.span_mono)
next
from assms(3) have "phull.subspace (hom_deg_set z A)" by (rule subspace_hom_deg_set)
hence "phull.span (hom_deg_set z A) = hom_deg_set z A" by (simp only: phull.span_eq_iff)
also have "… ⊆ phull.span B"
proof (rule ccontr)
assume "¬ hom_deg_set z A ⊆ phull.span B"
then obtain p0 where "p0 ∈ hom_deg_set z A - phull.span B" (is "_ ∈ ?B") by blast
note assms(1) this
moreover have "?B ⊆ P[X]"
proof (rule subset_trans)
from assms(2) show "hom_deg_set z A ⊆ P[X]" by (rule Polys_closed_hom_deg_set)
qed blast
ultimately obtain p where "p ∈ ?B" and p_min: "⋀q. punit.ord_strict_p q p ⟹ q ∉ ?B"
by (rule punit.ord_p_minimum_dgrad_p_set[OF dickson_grading_varnum, where m=0,
simplified dgrad_p_set_varnum]) blast
from this(1) have "p ∈ hom_deg_set z A" and "p ∉ phull.span B" by simp_all
from phull.span_zero this(2) have "p ≠ 0" by blast
with ‹p ∈ hom_deg_set z A› have "p ∈ hom_deg_set z A - {0}" by simp
hence "lpp p ∈ lpp ` (hom_deg_set z A - {0})" by (rule imageI)
also have "… = lpp ` B" by (simp only: eq1)
finally obtain b where "b ∈ B" and eq2: "lpp p = lpp b" ..
from this(1) sub have "b ∈ hom_deg_set z A - {0}" ..
hence "b ∈ hom_deg_set z A" and "b ≠ 0" by simp_all
from this(2) have lcb: "punit.lc b ≠ 0" by (rule punit.lc_not_0)
from ‹p ≠ 0› have lcp: "punit.lc p ≠ 0" by (rule punit.lc_not_0)
from ‹b ∈ B› have "b ∈ phull.span B" by (rule phull.span_base)
hence "(punit.lc p / punit.lc b) ⋅ b ∈ phull.span B" (is "?b ∈ _") by (rule phull.span_scale)
with ‹p ∉ phull.span B› have "p - ?b ≠ 0" by auto
moreover from lcb lcp ‹b ≠ 0› have "lpp ?b = lpp p"
by (simp add: punit.map_scale_eq_monom_mult punit.lt_monom_mult eq2)
moreover from lcb have "punit.lc ?b = punit.lc p" by (simp add: punit.map_scale_eq_monom_mult)
ultimately have "lpp (p - ?b) ≺ lpp p" by (rule punit.lt_minus_lessI)
hence "punit.ord_strict_p (p - ?b) p" by (rule punit.lt_ord_p)
hence "p - ?b ∉ ?B" by (rule p_min)
hence "p - ?b ∉ hom_deg_set z A ∨ p - ?b ∈ phull.span B" by simp
thus False
proof
assume *: "p - ?b ∉ hom_deg_set z A"
from phull.subspace_scale have "?b ∈ hom_deg_set z A"
proof (rule hom_deg_set_closed_scalar)
show "phull.subspace A" by fact
next
show "b ∈ hom_deg_set z A" by fact
qed
with phull.subspace_diff ‹p ∈ hom_deg_set z A› have "p - ?b ∈ hom_deg_set z A"
by (rule hom_deg_set_closed_minus) (rule assms(3))
with * show ?thesis ..
next
assume "p - ?b ∈ phull.span B"
hence "p - ?b + ?b ∈ phull.span B" using ‹?b ∈ phull.span B› by (rule phull.span_add)
hence "p ∈ phull.span B" by simp
with ‹p ∉ phull.span B› show ?thesis ..
qed
qed
finally show "phull.span (hom_deg_set z A) ⊆ phull.span B" .
qed
next
show "phull.independent B"
proof
assume "phull.dependent B"
then obtain B' u b' where "finite B'" and "B' ⊆ B" and "(∑b∈B'. u b ⋅ b) = 0"
and "b' ∈ B'" and "u b' ≠ 0" unfolding phull.dependent_explicit by blast
define B0 where "B0 = {b ∈ B'. u b ≠ 0}"
have "B0 ⊆ B'" by (simp add: B0_def)
with ‹finite B'› have "(∑b∈B0. u b ⋅ b) = (∑b∈B'. u b ⋅ b)"
by (rule sum.mono_neutral_left) (simp add: B0_def)
also have "… = 0" by fact
finally have eq: "(∑b∈B0. u b ⋅ b) = 0" .
define t where "t = ordered_powerprod_lin.Max (lpp ` B0)"
from ‹b' ∈ B'› ‹u b' ≠ 0› have "b' ∈ B0" by (simp add: B0_def)
hence "lpp b' ∈ lpp ` B0" by (rule imageI)
hence "lpp ` B0 ≠ {}" by blast
from ‹B0 ⊆ B'› ‹finite B'› have "finite B0" by (rule finite_subset)
hence "finite (lpp ` B0)" by (rule finite_imageI)
hence "t ∈ lpp ` B0" unfolding t_def using ‹lpp ` B0 ≠ {}›
by (rule ordered_powerprod_lin.Max_in)
then obtain b0 where "b0 ∈ B0" and t: "t = lpp b0" ..
note this(1)
moreover from ‹B0 ⊆ B'› ‹B' ⊆ B› have "B0 ⊆ B" by (rule subset_trans)
also have "… ⊆ hom_deg_set z A - {0}" by fact
finally have "b0 ∈ hom_deg_set z A - {0}" .
hence "b0 ≠ 0" by simp
hence "t ∈ keys b0" unfolding t by (rule punit.lt_in_keys)
have "lookup (∑b∈B0. u b ⋅ b) t = (∑b∈B0. u b * lookup b t)" by (simp add: lookup_sum)
also from ‹finite B0› have "… = (∑b∈{b0}. u b * lookup b t)"
proof (rule sum.mono_neutral_right)
from ‹b0 ∈ B0› show "{b0} ⊆ B0" by simp
next
show "∀b∈B0 - {b0}. u b * lookup b t = 0"
proof
fix b
assume "b ∈ B0 - {b0}"
hence "b ∈ B0" and "b ≠ b0" by simp_all
from this(1) have "lpp b ∈ lpp ` B0" by (rule imageI)
with ‹finite (lpp ` B0)› have "lpp b ≼ t" unfolding t_def
by (rule ordered_powerprod_lin.Max_ge)
have "t ∉ keys b"
proof
assume "t ∈ keys b"
hence "t ≼ lpp b" by (rule punit.lt_max_keys)
with ‹lpp b ≼ t› have "lpp b = lpp b0"
unfolding t by simp
from inj ‹B0 ⊆ B› have "inj_on lpp B0" by (rule inj_on_subset)
hence "b = b0" using ‹lpp b = lpp b0› ‹b ∈ B0› ‹b0 ∈ B0› by (rule inj_onD)
with ‹b ≠ b0› show False ..
qed
thus "u b * lookup b t = 0" by (simp add: in_keys_iff)
qed
qed
also from ‹t ∈ keys b0› ‹b0 ∈ B0› have "… ≠ 0" by (simp add: B0_def in_keys_iff)
finally show False by (simp add: eq)
qed
qed
also have "… = card ?A" unfolding eq1 using inj by (rule card_image[symmetric])
finally show ?thesis .
qed
end
end