Greatly extended CRing. Added Module.
--- a/src/HOL/Algebra/CRing.thy Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/CRing.thy Wed Apr 30 10:01:35 2003 +0200
@@ -5,41 +5,294 @@
Copyright: Clemens Ballarin
*)
-theory CRing = Summation
+theory CRing = FiniteProduct
files ("ringsimp.ML"):
+section {* Abelian Groups *}
+
+record 'a ring = "'a monoid" +
+ zero :: 'a ("\<zero>\<index>")
+ add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
+
+text {* Derived operations. *}
+
+constdefs
+ a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
+ "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+
+ minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
+
+locale abelian_monoid = struct G +
+ assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
+ mult = add G, one = zero G |)"
+
+text {*
+ The following definition is redundant but simple to use.
+*}
+
+locale abelian_group = abelian_monoid +
+ assumes a_comm_group: "comm_group (| carrier = carrier G,
+ mult = add G, one = zero G |)"
+
+subsection {* Basic Properties *}
+
+lemma abelian_monoidI:
+ assumes a_closed:
+ "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
+ and zero_closed: "zero R \<in> carrier R"
+ and a_assoc:
+ "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
+ add R (add R x y) z = add R x (add R y z)"
+ and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
+ and a_comm:
+ "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
+ shows "abelian_monoid R"
+ by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
+
+lemma abelian_groupI:
+ assumes a_closed:
+ "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
+ and zero_closed: "zero R \<in> carrier R"
+ and a_assoc:
+ "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
+ add R (add R x y) z = add R x (add R y z)"
+ and a_comm:
+ "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
+ and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
+ and l_inv_ex: "!!x. x \<in> carrier R ==> EX y : carrier R. add R y x = zero R"
+ shows "abelian_group R"
+ by (auto intro!: abelian_group.intro abelian_monoidI
+ abelian_group_axioms.intro comm_monoidI comm_groupI
+ intro: prems)
+
+(* TODO: The following thms are probably unnecessary. *)
+
+lemma (in abelian_monoid) a_magma:
+ "magma (| carrier = carrier G, mult = add G, one = zero G |)"
+ by (rule comm_monoid.axioms) (rule a_comm_monoid)
+
+lemma (in abelian_monoid) a_semigroup:
+ "semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
+ by (unfold semigroup_def) (fast intro: comm_monoid.axioms a_comm_monoid)
+
+lemma (in abelian_monoid) a_monoid:
+ "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
+ by (unfold monoid_def) (fast intro: a_comm_monoid comm_monoid.axioms)
+
+lemma (in abelian_group) a_group:
+ "group (| carrier = carrier G, mult = add G, one = zero G |)"
+ by (unfold group_def semigroup_def)
+ (fast intro: comm_group.axioms a_comm_group)
+
+lemma (in abelian_monoid) a_comm_semigroup:
+ "comm_semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
+ by (unfold comm_semigroup_def semigroup_def)
+ (fast intro: comm_monoid.axioms a_comm_monoid)
+
+lemmas monoid_record_simps = semigroup.simps monoid.simps
+
+lemma (in abelian_monoid) a_closed [intro, simp]:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
+ by (rule magma.m_closed [OF a_magma, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) zero_closed [intro, simp]:
+ "\<zero> \<in> carrier G"
+ by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps])
+
+lemma (in abelian_group) a_inv_closed [intro, simp]:
+ "x \<in> carrier G ==> \<ominus> x \<in> carrier G"
+ by (simp add: a_inv_def
+ group.inv_closed [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_group) minus_closed [intro, simp]:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
+ by (simp add: minus_def)
+
+lemma (in abelian_group) a_l_cancel [simp]:
+ "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ (x \<oplus> y = x \<oplus> z) = (y = z)"
+ by (rule group.l_cancel [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_group) a_r_cancel [simp]:
+ "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ (y \<oplus> x = z \<oplus> x) = (y = z)"
+ by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) a_assoc:
+ "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
+ by (rule semigroup.m_assoc [OF a_semigroup, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) l_zero [simp]:
+ "x \<in> carrier G ==> \<zero> \<oplus> x = x"
+ by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps])
+
+lemma (in abelian_group) l_neg:
+ "x \<in> carrier G ==> \<ominus> x \<oplus> x = \<zero>"
+ by (simp add: a_inv_def
+ group.l_inv [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) a_comm:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y = y \<oplus> x"
+ by (rule comm_semigroup.m_comm [OF a_comm_semigroup,
+ simplified monoid_record_simps])
+
+lemma (in abelian_monoid) a_lcomm:
+ "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
+ by (rule comm_semigroup.m_lcomm [OF a_comm_semigroup,
+ simplified monoid_record_simps])
+
+lemma (in abelian_monoid) r_zero [simp]:
+ "x \<in> carrier G ==> x \<oplus> \<zero> = x"
+ using monoid.r_one [OF a_monoid]
+ by simp
+
+lemma (in abelian_group) r_neg:
+ "x \<in> carrier G ==> x \<oplus> (\<ominus> x) = \<zero>"
+ using group.r_inv [OF a_group]
+ by (simp add: a_inv_def)
+
+lemma (in abelian_group) minus_zero [simp]:
+ "\<ominus> \<zero> = \<zero>"
+ by (simp add: a_inv_def
+ group.inv_one [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_group) minus_minus [simp]:
+ "x \<in> carrier G ==> \<ominus> (\<ominus> x) = x"
+ using group.inv_inv [OF a_group, simplified monoid_record_simps]
+ by (simp add: a_inv_def)
+
+lemma (in abelian_group) a_inv_inj:
+ "inj_on (a_inv G) (carrier G)"
+ using group.inv_inj [OF a_group, simplified monoid_record_simps]
+ by (simp add: a_inv_def)
+
+lemma (in abelian_group) minus_add:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
+ using comm_group.inv_mult [OF a_comm_group]
+ by (simp add: a_inv_def)
+
+lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
+
+subsection {* Sums over Finite Sets *}
+
+text {*
+ This definition makes it easy to lift lemmas from @{term finprod}.
+*}
+
+constdefs
+ finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
+ "finsum G f A == finprod (| carrier = carrier G,
+ mult = add G, one = zero G |) f A"
+
+(*
+ lemmas (in abelian_monoid) finsum_empty [simp] =
+ comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
+ is dangeous, because attributes (like simplified) are applied upon opening
+ the locale, simplified refers to the simpset at that time!!!
+
+ lemmas (in abelian_monoid) finsum_empty [simp] =
+ abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
+ simplified monoid_record_simps]
+makes the locale slow, because proofs are repeated for every
+"lemma (in abelian_monoid)" command.
+When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down
+from 110 secs to 60 secs.
+*)
+
+lemma (in abelian_monoid) finsum_empty [simp]:
+ "finsum G f {} = \<zero>"
+ by (rule comm_monoid.finprod_empty [OF a_comm_monoid,
+ folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_insert [simp]:
+ "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |]
+ ==> finsum G f (insert a F) = f a \<oplus> finsum G f F"
+ by (rule comm_monoid.finprod_insert [OF a_comm_monoid,
+ folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_zero [simp]:
+ "finite A ==> finsum G (%i. \<zero>) A = \<zero>"
+ by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
+ simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_closed [simp]:
+ fixes A
+ assumes fin: "finite A" and f: "f \<in> A -> carrier G"
+ shows "finsum G f A \<in> carrier G"
+ by (rule comm_monoid.finprod_closed [OF a_comm_monoid,
+ folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Un_Int:
+ "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
+ finsum G g (A Un B) \<oplus> finsum G g (A Int B) =
+ finsum G g A \<oplus> finsum G g B"
+ by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid,
+ folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Un_disjoint:
+ "[| finite A; finite B; A Int B = {};
+ g \<in> A -> carrier G; g \<in> B -> carrier G |]
+ ==> finsum G g (A Un B) = finsum G g A \<oplus> finsum G g B"
+ by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid,
+ folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_addf:
+ "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+ finsum G (%x. f x \<oplus> g x) A = (finsum G f A \<oplus> finsum G g A)"
+ by (rule comm_monoid.finprod_multf [OF a_comm_monoid,
+ folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_cong':
+ "[| A = B; g : B -> carrier G;
+ !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
+ by (rule comm_monoid.finprod_cong' [OF a_comm_monoid,
+ folded finsum_def, simplified monoid_record_simps]) auto
+
+lemma (in abelian_monoid) finsum_0 [simp]:
+ "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0"
+ by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def,
+ simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Suc [simp]:
+ "f : {..Suc n} -> carrier G ==>
+ finsum G f {..Suc n} = (f (Suc n) \<oplus> finsum G f {..n})"
+ by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def,
+ simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Suc2:
+ "f : {..Suc n} -> carrier G ==>
+ finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \<oplus> f 0)"
+ by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def,
+ simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_add [simp]:
+ "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
+ finsum G (%i. f i \<oplus> g i) {..n::nat} =
+ finsum G f {..n} \<oplus> finsum G g {..n}"
+ by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def,
+ simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_cong:
+ "[| A = B; !!i. i : B ==> f i = g i;
+ g : B -> carrier G = True |] ==> finsum G f A = finsum G g B"
+ by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
+ simplified monoid_record_simps]) auto
+
+text {*Usually, if this rule causes a failed congruence proof error,
+ the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
+ Adding @{thm [source] Pi_def} to the simpset is often useful. *}
+
section {* The Algebraic Hierarchy of Rings *}
subsection {* Basic Definitions *}
-record 'a ring = "'a group" +
- zero :: 'a ("\<zero>\<index>")
- add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
- a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
-
-locale cring = abelian_monoid R +
- assumes a_abelian_group: "abelian_group (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
- ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
- and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+locale cring = abelian_group R + comm_monoid R +
+ assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
-text {* Derived operation. *}
-
-constdefs
- minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
- "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
-
-(*
- -- {* Definition of derived operations *}
-
- minus_def: "a - b = a + (-b)"
- inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
- divide_def: "a / b = a * inverse b"
- power_def: "a ^ n = nat_rec 1 (%u b. b * a) n"
-*)
-
locale "domain" = cring +
assumes one_not_zero [simp]: "\<one> ~= \<zero>"
and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
@@ -47,117 +300,41 @@
subsection {* Basic Facts of Rings *}
-lemma (in cring) a_magma [simp, intro]:
- "magma (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- using a_abelian_group by (simp only: abelian_group_def)
-
-lemma (in cring) a_l_one [simp, intro]:
- "l_one (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- using a_abelian_group by (simp only: abelian_group_def)
-
-lemma (in cring) a_abelian_group_parts [simp, intro]:
- "semigroup_axioms (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- "group_axioms (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- "abelian_semigroup_axioms (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- using a_abelian_group by (simp_all only: abelian_group_def)
-
-lemma (in cring) a_semigroup:
- "semigroup (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- by (simp add: semigroup_def)
-
-lemma (in cring) a_group:
- "group (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- by (simp add: group_def)
-
-lemma (in cring) a_abelian_semigroup:
- "abelian_semigroup (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- by (simp add: abelian_semigroup_def)
-
-lemmas group_record_simps = semigroup.simps monoid.simps group.simps
-
-lemmas (in cring) a_closed [intro, simp] =
- magma.m_closed [OF a_magma, simplified group_record_simps]
-
-lemmas (in cring) zero_closed [intro, simp] =
- l_one.one_closed [OF a_l_one, simplified group_record_simps]
-
-lemmas (in cring) a_inv_closed [intro, simp] =
- group.inv_closed [OF a_group, simplified group_record_simps]
+lemma cringI:
+ assumes abelian_group: "abelian_group R"
+ and comm_monoid: "comm_monoid R"
+ and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+ ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
+ shows "cring R"
+ by (auto intro: cring.intro
+ abelian_group.axioms comm_monoid.axioms cring_axioms.intro prems)
-lemma (in cring) minus_closed [intro, simp]:
- "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
- by (simp add: minus_def)
-
-lemmas (in cring) a_l_cancel [simp] =
- group.l_cancel [OF a_group, simplified group_record_simps]
-
-lemmas (in cring) a_r_cancel [simp] =
- group.r_cancel [OF a_group, simplified group_record_simps]
-
-lemmas (in cring) a_assoc =
- semigroup.m_assoc [OF a_semigroup, simplified group_record_simps]
-
-lemmas (in cring) l_zero [simp] =
- l_one.l_one [OF a_l_one, simplified group_record_simps]
-
-lemmas (in cring) l_neg =
- group.l_inv [OF a_group, simplified group_record_simps]
-
-lemmas (in cring) a_comm =
- abelian_semigroup.m_comm [OF a_abelian_semigroup,
- simplified group_record_simps]
+lemma (in cring) is_abelian_group:
+ "abelian_group R"
+ by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
-lemmas (in cring) a_lcomm =
- abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified group_record_simps]
-
-lemma (in cring) r_zero [simp]:
- "x \<in> carrier R ==> x \<oplus> \<zero> = x"
- using group.r_one [OF a_group]
- by simp
-
-lemma (in cring) r_neg:
- "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
- using group.r_inv [OF a_group]
- by simp
-
-lemmas (in cring) minus_zero [simp] =
- group.inv_one [OF a_group, simplified group_record_simps]
-
-lemma (in cring) minus_minus [simp]:
- "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
- using group.inv_inv [OF a_group, simplified group_record_simps]
- by simp
-
-lemma (in cring) minus_add:
- "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
- using abelian_group.inv_mult [OF a_abelian_group]
- by simp
-
-lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
+lemma (in cring) is_comm_monoid:
+ "comm_monoid R"
+ by (auto intro!: comm_monoidI m_assoc m_comm)
subsection {* Normaliser for Commutative Rings *}
-lemma (in cring) r_neg2:
- "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
+lemma (in abelian_group) r_neg2:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
proof -
- assume G: "x \<in> carrier R" "y \<in> carrier R"
- then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
- with G show ?thesis by (simp add: a_ac)
+ assume G: "x \<in> carrier G" "y \<in> carrier G"
+ then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
+ by (simp only: r_neg l_zero)
+ with G show ?thesis
+ by (simp add: a_ac)
qed
-lemma (in cring) r_neg1:
- "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
+lemma (in abelian_group) r_neg1:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
proof -
- assume G: "x \<in> carrier R" "y \<in> carrier R"
- then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
+ assume G: "x \<in> carrier G" "y \<in> carrier G"
+ then have "(\<ominus> x \<oplus> x) \<oplus> y = y"
+ by (simp only: l_neg l_zero)
with G show ?thesis by (simp add: a_ac)
qed
@@ -165,10 +342,10 @@
"[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
proof -
- assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+ assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
- also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
- also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
+ also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
+ also from R have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
finally show ?thesis .
qed
@@ -191,7 +368,7 @@
"x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
proof -
assume R: "x \<in> carrier R"
- then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
+ then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: m_ac)
also from R have "... = \<zero>" by simp
finally show ?thesis .
qed
@@ -211,15 +388,19 @@
"[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
proof -
assume R: "x \<in> carrier R" "y \<in> carrier R"
- then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
+ then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: m_ac)
also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
- also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
+ also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: m_ac)
finally show ?thesis .
qed
+lemma (in cring) minus_eq:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
+ by (simp only: minus_def)
+
lemmas (in cring) cring_simprules =
a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
- a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
+ a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
@@ -227,7 +408,11 @@
method_setup algebra =
{* Method.ctxt_args cring_normalise *}
- {* computes distributive normal form in commutative rings (locales version) *}
+ {* computes distributive normal form in locale context cring *}
+
+lemma (in cring) nat_pow_zero:
+ "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
+ by (induct n) simp_all
text {* Two examples for use of method algebra *}
@@ -244,83 +429,6 @@
subsection {* Sums over Finite Sets *}
-text {*
- This definition makes it easy to lift lemmas from @{term finprod}.
-*}
-
-constdefs
- finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
- "finsum R f A == finprod (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |) f A"
-
-lemma (in cring) a_abelian_monoid:
- "abelian_monoid (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- by (simp add: abelian_monoid_def)
-
-(*
- lemmas (in cring) finsum_empty [simp] =
- abelian_monoid.finprod_empty [OF a_abelian_monoid, simplified]
- is dangeous, because attributes (like simplified) are applied upon opening
- the locale, simplified refers to the simpset at that time!!!
-*)
-
-lemmas (in cring) finsum_empty [simp] =
- abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_insert [simp] =
- abelian_monoid.finprod_insert [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_zero =
- abelian_monoid.finprod_one [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_closed [simp] =
- abelian_monoid.finprod_closed [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_Un_Int =
- abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_Un_disjoint =
- abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_addf =
- abelian_monoid.finprod_multf [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_cong' =
- abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_0 [simp] =
- abelian_monoid.finprod_0 [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_Suc [simp] =
- abelian_monoid.finprod_Suc [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_Suc2 =
- abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_add [simp] =
- abelian_monoid.finprod_mult [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-lemmas (in cring) finsum_cong =
- abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def,
- simplified group_record_simps]
-
-text {*Usually, if this rule causes a failed congruence proof error,
- the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
- Adding @{thm [source] Pi_def} to the simpset is often useful. *}
-
lemma (in cring) finsum_ldistr:
"[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
@@ -380,4 +488,90 @@
with R show ?thesis by algebra
qed
+subsection {* Morphisms *}
+
+constdefs
+ ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
+ "ring_hom R S == {h. h \<in> carrier R -> carrier S &
+ (ALL x y. x \<in> carrier R & y \<in> carrier R -->
+ h (mult R x y) = mult S (h x) (h y) &
+ h (add R x y) = add S (h x) (h y)) &
+ h (one R) = one S}"
+
+lemma ring_hom_memI:
+ assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
+ and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
+ h (mult R x y) = mult S (h x) (h y)"
+ and hom_add: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
+ h (add R x y) = add S (h x) (h y)"
+ and hom_one: "h (one R) = one S"
+ shows "h \<in> ring_hom R S"
+ by (auto simp add: ring_hom_def prems Pi_def)
+
+lemma ring_hom_closed:
+ "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
+ by (auto simp add: ring_hom_def funcset_mem)
+
+lemma ring_hom_mult:
+ "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
+ h (mult R x y) = mult S (h x) (h y)"
+ by (simp add: ring_hom_def)
+
+lemma ring_hom_add:
+ "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
+ h (add R x y) = add S (h x) (h y)"
+ by (simp add: ring_hom_def)
+
+lemma ring_hom_one:
+ "h \<in> ring_hom R S ==> h (one R) = one S"
+ by (simp add: ring_hom_def)
+
+locale ring_hom_cring = cring R + cring S + var h +
+ assumes homh [simp, intro]: "h \<in> ring_hom R S"
+ notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
+ and hom_mult [simp] = ring_hom_mult [OF homh]
+ and hom_add [simp] = ring_hom_add [OF homh]
+ and hom_one [simp] = ring_hom_one [OF homh]
+
+lemma (in ring_hom_cring) hom_zero [simp]:
+ "h \<zero> = \<zero>\<^sub>2"
+proof -
+ have "h \<zero> \<oplus>\<^sub>2 h \<zero> = h \<zero> \<oplus>\<^sub>2 \<zero>\<^sub>2"
+ by (simp add: hom_add [symmetric] del: hom_add)
+ then show ?thesis by (simp del: S.r_zero)
+qed
+
+lemma (in ring_hom_cring) hom_a_inv [simp]:
+ "x \<in> carrier R ==> h (\<ominus> x) = \<ominus>\<^sub>2 h x"
+proof -
+ assume R: "x \<in> carrier R"
+ then have "h x \<oplus>\<^sub>2 h (\<ominus> x) = h x \<oplus>\<^sub>2 (\<ominus>\<^sub>2 h x)"
+ by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
+ with R show ?thesis by simp
+qed
+
+lemma (in ring_hom_cring) hom_finsum [simp]:
+ "[| finite A; f \<in> A -> carrier R |] ==>
+ h (finsum R f A) = finsum S (h o f) A"
+proof (induct set: Finites)
+ case empty then show ?case by simp
+next
+ case insert then show ?case by (simp add: Pi_def)
+qed
+
+lemma (in ring_hom_cring) hom_finprod:
+ "[| finite A; f \<in> A -> carrier R |] ==>
+ h (finprod R f A) = finprod S (h o f) A"
+proof (induct set: Finites)
+ case empty then show ?case by simp
+next
+ case insert then show ?case by (simp add: Pi_def)
+qed
+
+declare ring_hom_cring.hom_finprod [simp]
+
+lemma id_ring_hom [simp]:
+ "id \<in> ring_hom R R"
+ by (auto intro!: ring_hom_memI)
+
end
--- a/src/HOL/Algebra/Coset.thy Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/Coset.thy Wed Apr 30 10:01:35 2003 +0200
@@ -10,27 +10,27 @@
declare (in group) l_inv [simp] r_inv [simp]
constdefs
- r_coset :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"
+ r_coset :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"
"r_coset G H a == (% x. (mult G) x a) ` H"
- l_coset :: "[('a,'b) group_scheme, 'a, 'a set] => 'a set"
+ l_coset :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
"l_coset G a H == (% x. (mult G) a x) ` H"
- rcosets :: "[('a,'b) group_scheme,'a set] => ('a set)set"
+ rcosets :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
"rcosets G H == r_coset G H ` (carrier G)"
- set_mult :: "[('a,'b) group_scheme,'a set,'a set] => 'a set"
+ set_mult :: "[('a,'b) monoid_scheme,'a set,'a set] => 'a set"
"set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
- set_inv :: "[('a,'b) group_scheme,'a set] => 'a set"
+ set_inv :: "[('a,'b) monoid_scheme,'a set] => 'a set"
"set_inv G H == (m_inv G) ` H"
- normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "<|" 60)
+ normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "<|" 60)
"normal H G == subgroup H G &
(\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
syntax (xsymbols)
- normal :: "['a set, ('a,'b) group_scheme] => bool" (infixl "\<lhd>" 60)
+ normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
locale coset = group G +
fixes rcos :: "['a set, 'a] => 'a set" (infixl "#>" 60)
@@ -153,7 +153,7 @@
subsection{*normal subgroups*}
(*????????????????
-text{*Allows use of theorems proved in the locale coset*}
+text "Allows use of theorems proved in the locale coset"
lemma subgroup_imp_coset: "subgroup H G ==> coset G"
apply (drule subgroup_imp_group)
apply (simp add: group_def coset_def)
@@ -406,13 +406,13 @@
subsection {*Factorization of a Group*}
constdefs
- FactGroup :: "[('a,'b) group_scheme, 'a set] => ('a set) group"
+ FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
(infixl "Mod" 60)
"FactGroup G H ==
(| carrier = rcosets G H,
mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
- one = H,
- m_inv = (%X: rcosets G H. set_inv G X) |)"
+ one = H (*,
+ m_inv = (%X: rcosets G H. set_inv G X) *) |)"
lemma (in coset) setmult_closed:
"[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
@@ -482,18 +482,13 @@
"H <| G ==> group (G Mod H)"
apply (insert is_coset)
apply (simp add: FactGroup_def)
-apply (rule group.intro)
- apply (rule magma.intro)
- apply (simp add: coset.setmult_closed)
- apply (rule semigroup_axioms.intro)
+apply (rule groupI)
+ apply (simp add: coset.setmult_closed)
+ apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc)
- apply (rule l_one.intro)
- apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
apply (simp add: normal_imp_subgroup
subgroup_in_rcosets coset.setrcos_mult_eq)
-apply (rule group_axioms.intro)
- apply (simp add: restrictI setinv_closed)
-apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq)
+apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
done
(*????????????????
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/FiniteProduct.thy Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,483 @@
+(* Title: Product Operator for Commutative Monoids
+ ID: $Id$
+ Author: Clemens Ballarin, started 19 November 2002
+
+This file is largely based on HOL/Finite_Set.thy.
+*)
+
+header {* Product Operator *}
+
+theory FiniteProduct = Group:
+
+(* Instantiation of LC from Finite_Set.thy is not possible,
+ because here we have explicit typing rules like x : carrier G.
+ We introduce an explicit argument for the domain D *)
+
+consts
+ foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
+
+inductive "foldSetD D f e"
+ intros
+ emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
+ insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
+ (insert x A, f x y) : foldSetD D f e"
+
+inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
+
+constdefs
+ foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
+ "foldD D f e A == THE x. (A, x) : foldSetD D f e"
+
+lemma foldSetD_closed:
+ "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D
+ |] ==> z : D";
+ by (erule foldSetD.elims) auto
+
+lemma Diff1_foldSetD:
+ "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
+ (A, f x y) : foldSetD D f e"
+ apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
+ apply auto
+ done
+
+lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
+ by (induct set: foldSetD) auto
+
+lemma finite_imp_foldSetD:
+ "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
+ EX x. (A, x) : foldSetD D f e"
+proof (induct set: Finites)
+ case empty then show ?case by auto
+next
+ case (insert F x)
+ then obtain y where y: "(F, y) : foldSetD D f e" by auto
+ with insert have "y : D" by (auto dest: foldSetD_closed)
+ with y and insert have "(insert x F, f x y) : foldSetD D f e"
+ by (intro foldSetD.intros) auto
+ then show ?case ..
+qed
+
+subsection {* Left-commutative operations *}
+
+locale LCD =
+ fixes B :: "'b set"
+ and D :: "'a set"
+ and f :: "'b => 'a => 'a" (infixl "\<cdot>" 70)
+ assumes left_commute:
+ "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+ and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
+
+lemma (in LCD) foldSetD_closed [dest]:
+ "(A, z) : foldSetD D f e ==> z : D";
+ by (erule foldSetD.elims) auto
+
+lemma (in LCD) Diff1_foldSetD:
+ "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
+ (A, f x y) : foldSetD D f e"
+ apply (subgoal_tac "x : B")
+ prefer 2 apply fast
+ apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
+ apply auto
+ done
+
+lemma (in LCD) foldSetD_imp_finite [simp]:
+ "(A, x) : foldSetD D f e ==> finite A"
+ by (induct set: foldSetD) auto
+
+lemma (in LCD) finite_imp_foldSetD:
+ "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
+proof (induct set: Finites)
+ case empty then show ?case by auto
+next
+ case (insert F x)
+ then obtain y where y: "(F, y) : foldSetD D f e" by auto
+ with insert have "y : D" by auto
+ with y and insert have "(insert x F, f x y) : foldSetD D f e"
+ by (intro foldSetD.intros) auto
+ then show ?case ..
+qed
+
+lemma (in LCD) foldSetD_determ_aux:
+ "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
+ (ALL y. (A, y) : foldSetD D f e --> y = x)"
+ apply (induct n)
+ apply (auto simp add: less_Suc_eq) (* slow *)
+ apply (erule foldSetD.cases)
+ apply blast
+ apply (erule foldSetD.cases)
+ apply blast
+ apply clarify
+ txt {* force simplification of @{text "card A < card (insert ...)"}. *}
+ apply (erule rev_mp)
+ apply (simp add: less_Suc_eq_le)
+ apply (rule impI)
+ apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
+ apply (subgoal_tac "Aa = Ab")
+ prefer 2 apply (blast elim!: equalityE)
+ apply blast
+ txt {* case @{prop "xa \<notin> xb"}. *}
+ apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
+ prefer 2 apply (blast elim!: equalityE)
+ apply clarify
+ apply (subgoal_tac "Aa = insert xb Ab - {xa}")
+ prefer 2 apply blast
+ apply (subgoal_tac "card Aa <= card Ab")
+ prefer 2
+ apply (rule Suc_le_mono [THEN subst])
+ apply (simp add: card_Suc_Diff1)
+ apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
+ apply (blast intro: foldSetD_imp_finite finite_Diff)
+ apply best
+ apply assumption
+ apply (frule (1) Diff1_foldSetD)
+ apply best
+ apply (subgoal_tac "ya = f xb x")
+ prefer 2
+ apply (subgoal_tac "Aa <= B")
+ prefer 2 apply best (* slow *)
+ apply (blast del: equalityCE)
+ apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
+ prefer 2 apply simp
+ apply (subgoal_tac "yb = f xa x")
+ prefer 2
+ apply (blast del: equalityCE dest: Diff1_foldSetD)
+ apply (simp (no_asm_simp))
+ apply (rule left_commute)
+ apply assumption
+ apply best (* slow *)
+ apply best
+ done
+
+lemma (in LCD) foldSetD_determ:
+ "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
+ ==> y = x"
+ by (blast intro: foldSetD_determ_aux [rule_format])
+
+lemma (in LCD) foldD_equality:
+ "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
+ by (unfold foldD_def) (blast intro: foldSetD_determ)
+
+lemma foldD_empty [simp]:
+ "e : D ==> foldD D f e {} = e"
+ by (unfold foldD_def) blast
+
+lemma (in LCD) foldD_insert_aux:
+ "[| x ~: A; x : B; e : D; A <= B |] ==>
+ ((insert x A, v) : foldSetD D f e) =
+ (EX y. (A, y) : foldSetD D f e & v = f x y)"
+ apply auto
+ apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
+ apply (fastsimp dest: foldSetD_imp_finite)
+ apply assumption
+ apply assumption
+ apply (blast intro: foldSetD_determ)
+ done
+
+lemma (in LCD) foldD_insert:
+ "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
+ foldD D f e (insert x A) = f x (foldD D f e A)"
+ apply (unfold foldD_def)
+ apply (simp add: foldD_insert_aux)
+ apply (rule the_equality)
+ apply (auto intro: finite_imp_foldSetD
+ cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
+ done
+
+lemma (in LCD) foldD_closed [simp]:
+ "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
+proof (induct set: Finites)
+ case empty then show ?case by (simp add: foldD_empty)
+next
+ case insert then show ?case by (simp add: foldD_insert)
+qed
+
+lemma (in LCD) foldD_commute:
+ "[| finite A; x : B; e : D; A <= B |] ==>
+ f x (foldD D f e A) = foldD D f (f x e) A"
+ apply (induct set: Finites)
+ apply simp
+ apply (auto simp add: left_commute foldD_insert)
+ done
+
+lemma Int_mono2:
+ "[| A <= C; B <= C |] ==> A Int B <= C"
+ by blast
+
+lemma (in LCD) foldD_nest_Un_Int:
+ "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
+ foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
+ apply (induct set: Finites)
+ apply simp
+ apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
+ Int_mono2 Un_subset_iff)
+ done
+
+lemma (in LCD) foldD_nest_Un_disjoint:
+ "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
+ ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
+ by (simp add: foldD_nest_Un_Int)
+
+-- {* Delete rules to do with @{text foldSetD} relation. *}
+
+declare foldSetD_imp_finite [simp del]
+ empty_foldSetDE [rule del]
+ foldSetD.intros [rule del]
+declare (in LCD)
+ foldSetD_closed [rule del]
+
+subsection {* Commutative monoids *}
+
+text {*
+ We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
+ instead of @{text "'b => 'a => 'a"}.
+*}
+
+locale ACeD =
+ fixes D :: "'a set"
+ and f :: "'a => 'a => 'a" (infixl "\<cdot>" 70)
+ and e :: 'a
+ assumes ident [simp]: "x : D ==> x \<cdot> e = x"
+ and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
+ and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+ and e_closed [simp]: "e : D"
+ and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
+
+lemma (in ACeD) left_commute:
+ "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+proof -
+ assume D: "x : D" "y : D" "z : D"
+ then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
+ also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
+ also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
+ finally show ?thesis .
+qed
+
+lemmas (in ACeD) AC = assoc commute left_commute
+
+lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
+proof -
+ assume D: "x : D"
+ have "x \<cdot> e = x" by (rule ident)
+ with D show ?thesis by (simp add: commute)
+qed
+
+lemma (in ACeD) foldD_Un_Int:
+ "[| finite A; finite B; A <= D; B <= D |] ==>
+ foldD D f e A \<cdot> foldD D f e B =
+ foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
+ apply (induct set: Finites)
+ apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
+ apply (simp add: AC insert_absorb Int_insert_left
+ LCD.foldD_insert [OF LCD.intro [of D]]
+ LCD.foldD_closed [OF LCD.intro [of D]]
+ Int_mono2 Un_subset_iff)
+ done
+
+lemma (in ACeD) foldD_Un_disjoint:
+ "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
+ foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
+ by (simp add: foldD_Un_Int
+ left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
+
+subsection {* Products over Finite Sets *}
+
+constdefs
+ finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
+ "finprod G f A == if finite A
+ then foldD (carrier G) (mult G o f) (one G) A
+ else arbitrary"
+
+(* TODO: nice syntax for the summation operator inside the locale
+ like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
+
+ML_setup {*
+ Context.>> (fn thy => (simpset_ref_of thy :=
+ simpset_of thy setsubgoaler asm_full_simp_tac; thy))
+*}
+
+lemma (in comm_monoid) finprod_empty [simp]:
+ "finprod G f {} = \<one>"
+ by (simp add: finprod_def)
+
+ML_setup {*
+ Context.>> (fn thy => (simpset_ref_of thy :=
+ simpset_of thy setsubgoaler asm_simp_tac; thy))
+*}
+
+declare funcsetI [intro]
+ funcset_mem [dest]
+
+lemma (in comm_monoid) finprod_insert [simp]:
+ "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
+ finprod G f (insert a F) = f a \<otimes> finprod G f F"
+ apply (rule trans)
+ apply (simp add: finprod_def)
+ apply (rule trans)
+ apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
+ apply simp
+ apply (rule m_lcomm)
+ apply fast
+ apply fast
+ apply assumption
+ apply (fastsimp intro: m_closed)
+ apply simp+
+ apply fast
+ apply (auto simp add: finprod_def)
+ done
+
+lemma (in comm_monoid) finprod_one [simp]:
+ "finite A ==> finprod G (%i. \<one>) A = \<one>"
+proof (induct set: Finites)
+ case empty show ?case by simp
+next
+ case (insert A a)
+ have "(%i. \<one>) \<in> A -> carrier G" by auto
+ with insert show ?case by simp
+qed
+
+lemma (in comm_monoid) finprod_closed [simp]:
+ fixes A
+ assumes fin: "finite A" and f: "f \<in> A -> carrier G"
+ shows "finprod G f A \<in> carrier G"
+using fin f
+proof induct
+ case empty show ?case by simp
+next
+ case (insert A a)
+ then have a: "f a \<in> carrier G" by fast
+ from insert have A: "f \<in> A -> carrier G" by fast
+ from insert A a show ?case by simp
+qed
+
+lemma funcset_Int_left [simp, intro]:
+ "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
+ by fast
+
+lemma funcset_Un_left [iff]:
+ "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
+ by fast
+
+lemma (in comm_monoid) finprod_Un_Int:
+ "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
+ finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
+ finprod G g A \<otimes> finprod G g B"
+-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
+proof (induct set: Finites)
+ case empty then show ?case by (simp add: finprod_closed)
+next
+ case (insert A a)
+ then have a: "g a \<in> carrier G" by fast
+ from insert have A: "g \<in> A -> carrier G" by fast
+ from insert A a show ?case
+ by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
+ Int_mono2 Un_subset_iff)
+qed
+
+lemma (in comm_monoid) finprod_Un_disjoint:
+ "[| finite A; finite B; A Int B = {};
+ g \<in> A -> carrier G; g \<in> B -> carrier G |]
+ ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
+ apply (subst finprod_Un_Int [symmetric])
+ apply (auto simp add: finprod_closed)
+ done
+
+lemma (in comm_monoid) finprod_multf:
+ "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+ finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
+proof (induct set: Finites)
+ case empty show ?case by simp
+next
+ case (insert A a) then
+ have fA: "f : A -> carrier G" by fast
+ from insert have fa: "f a : carrier G" by fast
+ from insert have gA: "g : A -> carrier G" by fast
+ from insert have ga: "g a : carrier G" by fast
+ from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
+ by (simp add: Pi_def)
+ show ?case (* check if all simps are really necessary *)
+ by (simp add: insert fA fa gA ga fgA m_ac Int_insert_left insert_absorb
+ Int_mono2 Un_subset_iff)
+qed
+
+lemma (in comm_monoid) finprod_cong':
+ "[| A = B; g : B -> carrier G;
+ !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+proof -
+ assume prems: "A = B" "g : B -> carrier G"
+ "!!i. i : B ==> f i = g i"
+ show ?thesis
+ proof (cases "finite B")
+ case True
+ then have "!!A. [| A = B; g : B -> carrier G;
+ !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+ proof induct
+ case empty thus ?case by simp
+ next
+ case (insert B x)
+ then have "finprod G f A = finprod G f (insert x B)" by simp
+ also from insert have "... = f x \<otimes> finprod G f B"
+ proof (intro finprod_insert)
+ show "finite B" .
+ next
+ show "x ~: B" .
+ next
+ assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+ "g \<in> insert x B \<rightarrow> carrier G"
+ thus "f : B -> carrier G" by fastsimp
+ next
+ assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+ "g \<in> insert x B \<rightarrow> carrier G"
+ thus "f x \<in> carrier G" by fastsimp
+ qed
+ also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
+ also from insert have "... = finprod G g (insert x B)"
+ by (intro finprod_insert [THEN sym]) auto
+ finally show ?case .
+ qed
+ with prems show ?thesis by simp
+ next
+ case False with prems show ?thesis by (simp add: finprod_def)
+ qed
+qed
+
+lemma (in comm_monoid) finprod_cong:
+ "[| A = B; !!i. i : B ==> f i = g i;
+ g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
+ by (rule finprod_cong') fast+
+
+text {*Usually, if this rule causes a failed congruence proof error,
+ the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
+ Adding @{thm [source] Pi_def} to the simpset is often useful.
+ For this reason, @{thm [source] comm_monoid.finprod_cong}
+ is not added to the simpset by default.
+*}
+
+declare funcsetI [rule del]
+ funcset_mem [rule del]
+
+lemma (in comm_monoid) finprod_0 [simp]:
+ "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
+by (simp add: Pi_def)
+
+lemma (in comm_monoid) finprod_Suc [simp]:
+ "f : {..Suc n} -> carrier G ==>
+ finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
+by (simp add: Pi_def atMost_Suc)
+
+lemma (in comm_monoid) finprod_Suc2:
+ "f : {..Suc n} -> carrier G ==>
+ finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
+proof (induct n)
+ case 0 thus ?case by (simp add: Pi_def)
+next
+ case Suc thus ?case by (simp add: m_assoc Pi_def)
+qed
+
+lemma (in comm_monoid) finprod_mult [simp]:
+ "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
+ finprod G (%i. f i \<otimes> g i) {..n::nat} =
+ finprod G f {..n} \<otimes> finprod G g {..n}"
+ by (induct n) (simp_all add: m_ac Pi_def)
+
+end
+
--- a/src/HOL/Algebra/Group.thy Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/Group.thy Wed Apr 30 10:01:35 2003 +0200
@@ -6,18 +6,23 @@
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
*)
-header {* Algebraic Structures up to Abelian Groups *}
+header {* Algebraic Structures up to Commutative Groups *}
theory Group = FuncSet:
+axclass number < type
+
+instance nat :: number ..
+instance int :: number ..
+
+section {* From Magmas to Groups *}
+
text {*
Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
the exception of \emph{magma} which, following Bourbaki, is a set
together with a binary, closed operation.
*}
-section {* From Magmas to Groups *}
-
subsection {* Definitions *}
record 'a semigroup =
@@ -27,8 +32,23 @@
record 'a monoid = "'a semigroup" +
one :: 'a ("\<one>\<index>")
-record 'a group = "'a monoid" +
- m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
+constdefs
+ m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80)
+ "m_inv G x == (THE y. y \<in> carrier G &
+ mult G x y = one G & mult G y x = one G)"
+
+ Units :: "('a, 'm) monoid_scheme => 'a set"
+ "Units G == {y. y \<in> carrier G &
+ (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"
+
+consts
+ pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
+
+defs (overloaded)
+ nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n"
+ int_pow_def: "pow G a z ==
+ let p = nat_rec (one G) (%u b. mult G b a)
+ in if neg z then m_inv G (p (nat (-z))) else p (nat z)"
locale magma = struct G +
assumes m_closed [intro, simp]:
@@ -37,32 +57,237 @@
locale semigroup = magma +
assumes m_assoc:
"[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
- (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+ (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-locale l_one = struct G +
+locale monoid = semigroup +
assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
+ and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
-locale group = semigroup + l_one +
- assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
- and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
+lemma monoidI:
+ assumes m_closed:
+ "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+ and one_closed: "one G \<in> carrier G"
+ and m_assoc:
+ "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ mult G (mult G x y) z = mult G x (mult G y z)"
+ and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+ and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x"
+ shows "monoid G"
+ by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
+ semigroup.intro monoid_axioms.intro
+ intro: prems)
+
+lemma (in monoid) Units_closed [dest]:
+ "x \<in> Units G ==> x \<in> carrier G"
+ by (unfold Units_def) fast
+
+lemma (in monoid) inv_unique:
+ assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
+ and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
+ shows "y = y'"
+proof -
+ from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
+ also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc)
+ also from G eq have "... = y'" by simp
+ finally show ?thesis .
+qed
+
+lemma (in monoid) Units_inv_closed [intro, simp]:
+ "x \<in> Units G ==> inv x \<in> carrier G"
+ apply (unfold Units_def m_inv_def)
+ apply auto
+ apply (rule theI2, fast)
+ apply (fast intro: inv_unique)
+ apply fast
+ done
+
+lemma (in monoid) Units_l_inv:
+ "x \<in> Units G ==> inv x \<otimes> x = \<one>"
+ apply (unfold Units_def m_inv_def)
+ apply auto
+ apply (rule theI2, fast)
+ apply (fast intro: inv_unique)
+ apply fast
+ done
+
+lemma (in monoid) Units_r_inv:
+ "x \<in> Units G ==> x \<otimes> inv x = \<one>"
+ apply (unfold Units_def m_inv_def)
+ apply auto
+ apply (rule theI2, fast)
+ apply (fast intro: inv_unique)
+ apply fast
+ done
+
+lemma (in monoid) Units_inv_Units [intro, simp]:
+ "x \<in> Units G ==> inv x \<in> Units G"
+proof -
+ assume x: "x \<in> Units G"
+ show "inv x \<in> Units G"
+ by (auto simp add: Units_def
+ intro: Units_l_inv Units_r_inv x Units_closed [OF x])
+qed
+
+lemma (in monoid) Units_l_cancel [simp]:
+ "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==>
+ (x \<otimes> y = x \<otimes> z) = (y = z)"
+proof
+ assume eq: "x \<otimes> y = x \<otimes> z"
+ and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
+ then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
+ by (simp add: m_assoc Units_closed)
+ with G show "y = z" by (simp add: Units_l_inv)
+next
+ assume eq: "y = z"
+ and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
+ then show "x \<otimes> y = x \<otimes> z" by simp
+qed
+
+lemma (in monoid) Units_inv_inv [simp]:
+ "x \<in> Units G ==> inv (inv x) = x"
+proof -
+ assume x: "x \<in> Units G"
+ then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
+ by (simp add: Units_l_inv Units_r_inv)
+ with x show ?thesis by (simp add: Units_closed)
+qed
+
+lemma (in monoid) inv_inj_on_Units:
+ "inj_on (m_inv G) (Units G)"
+proof (rule inj_onI)
+ fix x y
+ assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y"
+ then have "inv (inv x) = inv (inv y)" by simp
+ with G show "x = y" by simp
+qed
+
+text {* Power *}
+
+lemma (in monoid) nat_pow_closed [intro, simp]:
+ "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
+ by (induct n) (simp_all add: nat_pow_def)
+
+lemma (in monoid) nat_pow_0 [simp]:
+ "x (^) (0::nat) = \<one>"
+ by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_Suc [simp]:
+ "x (^) (Suc n) = x (^) n \<otimes> x"
+ by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_one [simp]:
+ "\<one> (^) (n::nat) = \<one>"
+ by (induct n) simp_all
+
+lemma (in monoid) nat_pow_mult:
+ "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
+ by (induct m) (simp_all add: m_assoc [THEN sym])
+
+lemma (in monoid) nat_pow_pow:
+ "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
+ by (induct m) (simp, simp add: nat_pow_mult add_commute)
+
+text {*
+ A group is a monoid all of whose elements are invertible.
+*}
+
+locale group = monoid +
+ assumes Units: "carrier G <= Units G"
+
+theorem groupI:
+ assumes m_closed [simp]:
+ "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+ and one_closed [simp]: "one G \<in> carrier G"
+ and m_assoc:
+ "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ mult G (mult G x y) z = mult G x (mult G y z)"
+ and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+ and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
+ shows "group G"
+proof -
+ have l_cancel [simp]:
+ "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ (mult G x y = mult G x z) = (y = z)"
+ proof
+ fix x y z
+ assume eq: "mult G x y = mult G x z"
+ and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
+ with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
+ and l_inv: "mult G x_inv x = one G" by fast
+ from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z"
+ by (simp add: m_assoc)
+ with G show "y = z" by (simp add: l_inv)
+ next
+ fix x y z
+ assume eq: "y = z"
+ and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
+ then show "mult G x y = mult G x z" by simp
+ qed
+ have r_one:
+ "!!x. x \<in> carrier G ==> mult G x (one G) = x"
+ proof -
+ fix x
+ assume x: "x \<in> carrier G"
+ with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
+ and l_inv: "mult G x_inv x = one G" by fast
+ from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x"
+ by (simp add: m_assoc [symmetric] l_inv)
+ with x xG show "mult G x (one G) = x" by simp
+ qed
+ have inv_ex:
+ "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G &
+ mult G x y = one G"
+ proof -
+ fix x
+ assume x: "x \<in> carrier G"
+ with l_inv_ex obtain y where y: "y \<in> carrier G"
+ and l_inv: "mult G y x = one G" by fast
+ from x y have "mult G y (mult G x y) = mult G y (one G)"
+ by (simp add: m_assoc [symmetric] l_inv r_one)
+ with x y have r_inv: "mult G x y = one G"
+ by simp
+ from x y show "EX y : carrier G. mult G y x = one G &
+ mult G x y = one G"
+ by (fast intro: l_inv r_inv)
+ qed
+ then have carrier_subset_Units: "carrier G <= Units G"
+ by (unfold Units_def) fast
+ show ?thesis
+ by (fast intro!: group.intro magma.intro semigroup_axioms.intro
+ semigroup.intro monoid_axioms.intro group_axioms.intro
+ carrier_subset_Units intro: prems r_one)
+qed
+
+lemma (in monoid) monoid_groupI:
+ assumes l_inv_ex:
+ "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
+ shows "group G"
+ by (rule groupI) (auto intro: m_assoc l_inv_ex)
+
+lemma (in group) Units_eq [simp]:
+ "Units G = carrier G"
+proof
+ show "Units G <= carrier G" by fast
+next
+ show "carrier G <= Units G" by (rule Units)
+qed
+
+lemma (in group) inv_closed [intro, simp]:
+ "x \<in> carrier G ==> inv x \<in> carrier G"
+ using Units_inv_closed by simp
+
+lemma (in group) l_inv:
+ "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
+ using Units_l_inv by simp
subsection {* Cancellation Laws and Basic Properties *}
lemma (in group) l_cancel [simp]:
"[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
(x \<otimes> y = x \<otimes> z) = (y = z)"
-proof
- assume eq: "x \<otimes> y = x \<otimes> z"
- and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
- then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc)
- with G show "y = z" by (simp add: l_inv)
-next
- assume eq: "y = z"
- and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
- then show "x \<otimes> y = x \<otimes> z" by simp
-qed
-
+ using Units_l_inv by simp
+(*
lemma (in group) r_one [simp]:
"x \<in> carrier G ==> x \<otimes> \<one> = x"
proof -
@@ -71,7 +296,7 @@
by (simp add: m_assoc [symmetric] l_inv)
with x show ?thesis by simp
qed
-
+*)
lemma (in group) r_inv:
"x \<in> carrier G ==> x \<otimes> inv x = \<one>"
proof -
@@ -106,11 +331,11 @@
lemma (in group) inv_inv [simp]:
"x \<in> carrier G ==> inv (inv x) = x"
-proof -
- assume x: "x \<in> carrier G"
- then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by (simp add: l_inv r_inv)
- with x show ?thesis by simp
-qed
+ using Units_inv_inv by simp
+
+lemma (in group) inv_inj:
+ "inj_on (m_inv G) (carrier G)"
+ using inv_inj_on_Units by simp
lemma (in group) inv_mult_group:
"[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
@@ -121,6 +346,20 @@
with G show ?thesis by simp
qed
+text {* Power *}
+
+lemma (in group) int_pow_def2:
+ "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
+ by (simp add: int_pow_def nat_pow_def Let_def)
+
+lemma (in group) int_pow_0 [simp]:
+ "x (^) (0::int) = \<one>"
+ by (simp add: int_pow_def2)
+
+lemma (in group) int_pow_one [simp]:
+ "\<one> (^) (z::int) = \<one>"
+ by (simp add: int_pow_def2)
+
subsection {* Substructures *}
locale submagma = var H + struct G +
@@ -128,7 +367,7 @@
and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
declare (in submagma) magma.intro [intro] semigroup.intro [intro]
-
+ semigroup_axioms.intro [intro]
(*
alternative definition of submagma
@@ -167,21 +406,21 @@
and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
declare (in subgroup) group.intro [intro]
-
+(*
lemma (in subgroup) l_oneI [intro]:
includes l_one G
shows "l_one (G(| carrier := H |))"
by rule simp_all
-
+*)
lemma (in subgroup) group_axiomsI [intro]:
includes group G
shows "group_axioms (G(| carrier := H |))"
- by rule (simp_all add: l_inv)
+ by rule (auto intro: l_inv r_inv simp add: Units_def)
lemma (in subgroup) groupI [intro]:
includes group G
shows "group (G(| carrier := H |))"
- using prems by fast
+ by (rule groupI) (auto intro: m_assoc l_inv)
text {*
Since @{term H} is nonempty, it contains some element @{term x}. Since
@@ -223,8 +462,8 @@
declare magma.m_closed [simp]
-declare l_one.one_closed [iff] group.inv_closed [simp]
- l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]
+declare monoid.one_closed [iff] group.inv_closed [simp]
+ monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
lemma subgroup_nonempty:
"~ subgroup {} G"
@@ -241,6 +480,11 @@
with subgroup_nonempty show ?thesis by contradiction
qed
+(*
+lemma (in monoid) Units_subgroup:
+ "subgroup (Units G) G"
+*)
+
subsection {* Direct Products *}
constdefs
@@ -251,13 +495,13 @@
"G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
- DirProdMonoid ::
+ DirProdGroup ::
"[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
- (infixr "\<times>\<^sub>m" 80)
- "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
+ (infixr "\<times>\<^sub>g" 80)
+ "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
mult = mult (G \<times>\<^sub>s H),
one = (one G, one H) |)"
-
+(*
DirProdGroup ::
"[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
(infixr "\<times>\<^sub>g" 80)
@@ -265,6 +509,7 @@
mult = mult (G \<times>\<^sub>m H),
one = one (G \<times>\<^sub>m H),
m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
+*)
lemma DirProdSemigroup_magma:
includes magma G + magma H
@@ -287,13 +532,13 @@
includes magma G + magma H
shows "magma (G \<times>\<^sub>g H)"
by rule
- (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)
+ (auto simp add: DirProdGroup_def DirProdSemigroup_def)
lemma DirProdGroup_semigroup_axioms:
includes semigroup G + semigroup H
shows "semigroup_axioms (G \<times>\<^sub>g H)"
by rule
- (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
+ (auto simp add: DirProdGroup_def DirProdSemigroup_def
G.m_assoc H.m_assoc)
lemma DirProdGroup_semigroup:
@@ -308,11 +553,9 @@
lemma DirProdGroup_group:
includes group G + group H
shows "group (G \<times>\<^sub>g H)"
-by rule
- (auto intro: magma.intro l_one.intro
- semigroup_axioms.intro group_axioms.intro
- simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
- G.m_assoc H.m_assoc G.l_inv H.l_inv)
+ by (rule groupI)
+ (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
+ simp add: DirProdGroup_def DirProdSemigroup_def)
subsection {* Homomorphisms *}
@@ -376,14 +619,20 @@
with x show ?thesis by simp
qed
-section {* Abelian Structures *}
+section {* Commutative Structures *}
+
+text {*
+ Naming convention: multiplicative structures that are commutative
+ are called \emph{commutative}, additive structures are called
+ \emph{Abelian}.
+*}
subsection {* Definition *}
-locale abelian_semigroup = semigroup +
+locale comm_semigroup = semigroup +
assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
-lemma (in abelian_semigroup) m_lcomm:
+lemma (in comm_semigroup) m_lcomm:
"[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
proof -
@@ -394,11 +643,33 @@
finally show ?thesis .
qed
-lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
+lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
+
+locale comm_monoid = comm_semigroup + monoid
-locale abelian_monoid = abelian_semigroup + l_one
+lemma comm_monoidI:
+ assumes m_closed:
+ "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+ and one_closed: "one G \<in> carrier G"
+ and m_assoc:
+ "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ mult G (mult G x y) z = mult G x (mult G y z)"
+ and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+ and m_comm:
+ "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
+ shows "comm_monoid G"
+ using l_one
+ by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
+ comm_semigroup_axioms.intro monoid_axioms.intro
+ intro: prems simp: m_closed one_closed m_comm)
-lemma (in abelian_monoid) l_one [simp]:
+lemma (in monoid) monoid_comm_monoidI:
+ assumes m_comm:
+ "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
+ shows "comm_monoid G"
+ by (rule comm_monoidI) (auto intro: m_assoc m_comm)
+(*
+lemma (in comm_monoid) r_one [simp]:
"x \<in> carrier G ==> x \<otimes> \<one> = x"
proof -
assume G: "x \<in> carrier G"
@@ -406,11 +677,38 @@
also from G have "... = x" by simp
finally show ?thesis .
qed
+*)
-locale abelian_group = abelian_monoid + group
+lemma (in comm_monoid) nat_pow_distr:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==>
+ (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
+ by (induct n) (simp, simp add: m_ac)
+
+locale comm_group = comm_monoid + group
+
+lemma (in group) group_comm_groupI:
+ assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
+ mult G x y = mult G y x"
+ shows "comm_group G"
+ by (fast intro: comm_group.intro comm_semigroup_axioms.intro
+ group.axioms prems)
-lemma (in abelian_group) inv_mult:
+lemma comm_groupI:
+ assumes m_closed:
+ "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+ and one_closed: "one G \<in> carrier G"
+ and m_assoc:
+ "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+ mult G (mult G x y) z = mult G x (mult G y z)"
+ and m_comm:
+ "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
+ and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+ and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
+ shows "comm_group G"
+ by (fast intro: group.group_comm_groupI groupI prems)
+
+lemma (in comm_group) inv_mult:
"[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
- by (simp add: ac inv_mult_group)
+ by (simp add: m_ac inv_mult_group)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Module.thy Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,161 @@
+(* Title: HOL/Algebra/Module
+ ID: $Id$
+ Author: Clemens Ballarin, started 15 April 2003
+ Copyright: Clemens Ballarin
+*)
+
+theory Module = CRing:
+
+section {* Modules over an Abelian Group *}
+
+record ('a, 'b) module = "'b ring" +
+ smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
+
+locale module = cring R + abelian_group M +
+ assumes smult_closed [simp, intro]:
+ "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
+ and smult_l_distr:
+ "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+ (a \<oplus> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 b \<odot>\<^sub>2 x"
+ and smult_r_distr:
+ "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+ a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 y"
+ and smult_assoc1:
+ "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+ (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
+ and smult_one [simp]:
+ "x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
+
+locale algebra = module R M + cring M +
+ assumes smult_assoc2:
+ "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+ (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
+
+lemma moduleI:
+ assumes cring: "cring R"
+ and abelian_group: "abelian_group M"
+ and smult_closed:
+ "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
+ and smult_l_distr:
+ "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+ smult M (add R a b) x = add M (smult M a x) (smult M b x)"
+ and smult_r_distr:
+ "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+ smult M a (add M x y) = add M (smult M a x) (smult M a y)"
+ and smult_assoc1:
+ "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+ smult M (mult R a b) x = smult M a (smult M b x)"
+ and smult_one:
+ "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+ shows "module R M"
+ by (auto intro: module.intro cring.axioms abelian_group.axioms
+ module_axioms.intro prems)
+
+lemma algebraI:
+ assumes R_cring: "cring R"
+ and M_cring: "cring M"
+ and smult_closed:
+ "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
+ and smult_l_distr:
+ "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+ smult M (add R a b) x = add M (smult M a x) (smult M b x)"
+ and smult_r_distr:
+ "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+ smult M a (add M x y) = add M (smult M a x) (smult M a y)"
+ and smult_assoc1:
+ "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+ smult M (mult R a b) x = smult M a (smult M b x)"
+ and smult_one:
+ "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+ and smult_assoc2:
+ "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+ mult M (smult M a x) y = smult M a (mult M x y)"
+ shows "algebra R M"
+ by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms
+ module_axioms.intro prems)
+
+lemma (in algebra) R_cring:
+ "cring R"
+ by (rule cring.intro) assumption+
+
+lemma (in algebra) M_cring:
+ "cring M"
+ by (rule cring.intro) assumption+
+
+lemma (in algebra) module:
+ "module R M"
+ by (auto intro: moduleI R_cring is_abelian_group
+ smult_l_distr smult_r_distr smult_assoc1)
+
+subsection {* Basic Properties of Algebras *}
+
+lemma (in algebra) smult_l_null [simp]:
+ "x \<in> carrier M ==> \<zero> \<odot>\<^sub>2 x = \<zero>\<^sub>2"
+proof -
+ assume M: "x \<in> carrier M"
+ note facts = M smult_closed
+ from facts have "\<zero> \<odot>\<^sub>2 x = (\<zero> \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<zero> \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)" by algebra
+ also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)"
+ by (simp add: smult_l_distr del: R.l_zero R.r_zero)
+ also from facts have "... = \<zero>\<^sub>2" by algebra
+ finally show ?thesis .
+qed
+
+lemma (in algebra) smult_r_null [simp]:
+ "a \<in> carrier R ==> a \<odot>\<^sub>2 \<zero>\<^sub>2 = \<zero>\<^sub>2";
+proof -
+ assume R: "a \<in> carrier R"
+ note facts = R smult_closed
+ from facts have "a \<odot>\<^sub>2 \<zero>\<^sub>2 = (a \<odot>\<^sub>2 \<zero>\<^sub>2 \<oplus>\<^sub>2 a \<odot>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
+ by algebra
+ also from R have "... = a \<odot>\<^sub>2 (\<zero>\<^sub>2 \<oplus>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
+ by (simp add: smult_r_distr del: M.l_zero M.r_zero)
+ also from facts have "... = \<zero>\<^sub>2" by algebra
+ finally show ?thesis .
+qed
+
+lemma (in algebra) smult_l_minus:
+ "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^sub>2 x = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
+proof -
+ assume RM: "a \<in> carrier R" "x \<in> carrier M"
+ note facts = RM smult_closed
+ from facts have "(\<ominus>a) \<odot>\<^sub>2 x = (\<ominus>a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
+ also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
+ by (simp add: smult_l_distr)
+ also from facts smult_l_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
+ finally show ?thesis .
+qed
+
+lemma (in algebra) smult_r_minus:
+ "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
+proof -
+ assume RM: "a \<in> carrier R" "x \<in> carrier M"
+ note facts = RM smult_closed
+ from facts have "a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = (a \<odot>\<^sub>2 \<ominus>\<^sub>2x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
+ by algebra
+ also from RM have "... = a \<odot>\<^sub>2 (\<ominus>\<^sub>2x \<oplus>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
+ by (simp add: smult_r_distr)
+ also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
+ finally show ?thesis .
+qed
+
+subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
+
+text {* Not finished. *}
+
+constdefs
+ INTEG :: "int ring"
+ "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+
+(*
+ INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module"
+ "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R,
+ zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)"
+*)
+
+lemma cring_INTEG:
+ "cring INTEG"
+ by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
+ zadd_zminus_inverse2 zadd_zmult_distrib)
+
+end
--- a/src/HOL/Algebra/ROOT.ML Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/ROOT.ML Wed Apr 30 10:01:35 2003 +0200
@@ -1,9 +1,16 @@
(*
- Polynomials
+ The Isabelle Algebraic Library
$Id$
Author: Clemens Ballarin, started 24 September 1999
*)
+(* New development, based on explicit structures *)
+
+use_thy "Sylow"; (* Groups *)
+(* use_thy "UnivPoly"; *) (* Rings and polynomials *)
+
+(* Old development, based on axiomatic type classes.
+ Will be withdrawn in future. *)
+
with_path "abstract" time_use_thy "Abstract"; (*The ring theory*)
with_path "poly" time_use_thy "Polynomial"; (*The full theory*)
-use_thy "Sylow";
--- a/src/HOL/Algebra/Summation.thy Tue Apr 29 12:36:49 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,500 +0,0 @@
-(* Title: Summation Operator for Abelian Groups
- ID: $Id$
- Author: Clemens Ballarin, started 19 November 2002
-
-This file is largely based on HOL/Finite_Set.thy.
-*)
-
-header {* Summation Operator *}
-
-theory Summation = Group:
-
-(* Instantiation of LC from Finite_Set.thy is not possible,
- because here we have explicit typing rules like x : carrier G.
- We introduce an explicit argument for the domain D *)
-
-consts
- foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
-
-inductive "foldSetD D f e"
- intros
- emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
- insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
- (insert x A, f x y) : foldSetD D f e"
-
-inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
-
-constdefs
- foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
- "foldD D f e A == THE x. (A, x) : foldSetD D f e"
-
-lemma foldSetD_closed:
- "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D
- |] ==> z : D";
- by (erule foldSetD.elims) auto
-
-lemma Diff1_foldSetD:
- "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
- (A, f x y) : foldSetD D f e"
- apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
- apply auto
- done
-
-lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
- by (induct set: foldSetD) auto
-
-lemma finite_imp_foldSetD:
- "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
- EX x. (A, x) : foldSetD D f e"
-proof (induct set: Finites)
- case empty then show ?case by auto
-next
- case (insert F x)
- then obtain y where y: "(F, y) : foldSetD D f e" by auto
- with insert have "y : D" by (auto dest: foldSetD_closed)
- with y and insert have "(insert x F, f x y) : foldSetD D f e"
- by (intro foldSetD.intros) auto
- then show ?case ..
-qed
-
-subsection {* Left-commutative operations *}
-
-locale LCD =
- fixes B :: "'b set"
- and D :: "'a set"
- and f :: "'b => 'a => 'a" (infixl "\<cdot>" 70)
- assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
- and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
-
-lemma (in LCD) foldSetD_closed [dest]:
- "(A, z) : foldSetD D f e ==> z : D";
- by (erule foldSetD.elims) auto
-
-lemma (in LCD) Diff1_foldSetD:
- "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
- (A, f x y) : foldSetD D f e"
- apply (subgoal_tac "x : B")
- prefer 2 apply fast
- apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
- apply auto
- done
-
-lemma (in LCD) foldSetD_imp_finite [simp]:
- "(A, x) : foldSetD D f e ==> finite A"
- by (induct set: foldSetD) auto
-
-lemma (in LCD) finite_imp_foldSetD:
- "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
-proof (induct set: Finites)
- case empty then show ?case by auto
-next
- case (insert F x)
- then obtain y where y: "(F, y) : foldSetD D f e" by auto
- with insert have "y : D" by auto
- with y and insert have "(insert x F, f x y) : foldSetD D f e"
- by (intro foldSetD.intros) auto
- then show ?case ..
-qed
-
-lemma (in LCD) foldSetD_determ_aux:
- "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
- (ALL y. (A, y) : foldSetD D f e --> y = x)"
- apply (induct n)
- apply (auto simp add: less_Suc_eq)
- apply (erule foldSetD.cases)
- apply blast
- apply (erule foldSetD.cases)
- apply blast
- apply clarify
- txt {* force simplification of @{text "card A < card (insert ...)"}. *}
- apply (erule rev_mp)
- apply (simp add: less_Suc_eq_le)
- apply (rule impI)
- apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
- apply (subgoal_tac "Aa = Ab")
- prefer 2 apply (blast elim!: equalityE)
- apply blast
- txt {* case @{prop "xa \<notin> xb"}. *}
- apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
- prefer 2 apply (blast elim!: equalityE)
- apply clarify
- apply (subgoal_tac "Aa = insert xb Ab - {xa}")
- prefer 2 apply blast
- apply (subgoal_tac "card Aa <= card Ab")
- prefer 2
- apply (rule Suc_le_mono [THEN subst])
- apply (simp add: card_Suc_Diff1)
- apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
- apply (blast intro: foldSetD_imp_finite finite_Diff)
-(* new subgoal from finite_imp_foldSetD *)
- apply best (* blast doesn't seem to solve this *)
- apply assumption
- apply (frule (1) Diff1_foldSetD)
-(* new subgoal from Diff1_foldSetD *)
- apply best
-(*
-apply (best del: foldSetD_closed elim: foldSetD_closed)
- apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
- prefer 3 apply assumption apply (rule e_closed)
- apply (rule f_closed) apply force apply assumption
-*)
- apply (subgoal_tac "ya = f xb x")
- prefer 2
-(* new subgoal to make IH applicable *)
- apply (subgoal_tac "Aa <= B")
- prefer 2 apply best
- apply (blast del: equalityCE)
- apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
- prefer 2 apply simp
- apply (subgoal_tac "yb = f xa x")
- prefer 2
-(* apply (drule_tac x = xa in Diff1_foldSetD)
- apply assumption
- apply (rule f_closed) apply best apply (rule foldSetD_closed)
- prefer 3 apply assumption apply (rule e_closed)
- apply (rule f_closed) apply best apply assumption
-*)
- apply (blast del: equalityCE dest: Diff1_foldSetD)
- apply (simp (no_asm_simp))
- apply (rule left_commute)
- apply assumption apply best apply best
- done
-
-lemma (in LCD) foldSetD_determ:
- "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
- ==> y = x"
- by (blast intro: foldSetD_determ_aux [rule_format])
-
-lemma (in LCD) foldD_equality:
- "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
- by (unfold foldD_def) (blast intro: foldSetD_determ)
-
-lemma foldD_empty [simp]:
- "e : D ==> foldD D f e {} = e"
- by (unfold foldD_def) blast
-
-lemma (in LCD) foldD_insert_aux:
- "[| x ~: A; x : B; e : D; A <= B |] ==>
- ((insert x A, v) : foldSetD D f e) =
- (EX y. (A, y) : foldSetD D f e & v = f x y)"
- apply auto
- apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
- apply (fastsimp dest: foldSetD_imp_finite)
-(* new subgoal by finite_imp_foldSetD *)
- apply assumption
- apply assumption
- apply (blast intro: foldSetD_determ)
- done
-
-lemma (in LCD) foldD_insert:
- "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
- foldD D f e (insert x A) = f x (foldD D f e A)"
- apply (unfold foldD_def)
- apply (simp add: foldD_insert_aux)
- apply (rule the_equality)
- apply (auto intro: finite_imp_foldSetD
- cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
- done
-
-lemma (in LCD) foldD_closed [simp]:
- "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
-proof (induct set: Finites)
- case empty then show ?case by (simp add: foldD_empty)
-next
- case insert then show ?case by (simp add: foldD_insert)
-qed
-
-lemma (in LCD) foldD_commute:
- "[| finite A; x : B; e : D; A <= B |] ==>
- f x (foldD D f e A) = foldD D f (f x e) A"
- apply (induct set: Finites)
- apply simp
- apply (auto simp add: left_commute foldD_insert)
- done
-
-lemma Int_mono2:
- "[| A <= C; B <= C |] ==> A Int B <= C"
- by blast
-
-lemma (in LCD) foldD_nest_Un_Int:
- "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
- foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
- apply (induct set: Finites)
- apply simp
- apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
- Int_mono2 Un_subset_iff)
- done
-
-lemma (in LCD) foldD_nest_Un_disjoint:
- "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
- ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
- by (simp add: foldD_nest_Un_Int)
-
--- {* Delete rules to do with @{text foldSetD} relation. *}
-
-declare foldSetD_imp_finite [simp del]
- empty_foldSetDE [rule del]
- foldSetD.intros [rule del]
-declare (in LCD)
- foldSetD_closed [rule del]
-
-subsection {* Commutative monoids *}
-
-text {*
- We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
- instead of @{text "'b => 'a => 'a"}.
-*}
-
-locale ACeD =
- fixes D :: "'a set"
- and f :: "'a => 'a => 'a" (infixl "\<cdot>" 70)
- and e :: 'a
- assumes ident [simp]: "x : D ==> x \<cdot> e = x"
- and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
- and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
- and e_closed [simp]: "e : D"
- and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
-
-lemma (in ACeD) left_commute:
- "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-proof -
- assume D: "x : D" "y : D" "z : D"
- then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
- also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
- also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
- finally show ?thesis .
-qed
-
-lemmas (in ACeD) AC = assoc commute left_commute
-
-lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
-proof -
- assume D: "x : D"
- have "x \<cdot> e = x" by (rule ident)
- with D show ?thesis by (simp add: commute)
-qed
-
-lemma (in ACeD) foldD_Un_Int:
- "[| finite A; finite B; A <= D; B <= D |] ==>
- foldD D f e A \<cdot> foldD D f e B =
- foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
- apply (induct set: Finites)
- apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
-(* left_commute is required to show premise of LCD.intro *)
- apply (simp add: AC insert_absorb Int_insert_left
- LCD.foldD_insert [OF LCD.intro [of D]]
- LCD.foldD_closed [OF LCD.intro [of D]]
- Int_mono2 Un_subset_iff)
- done
-
-lemma (in ACeD) foldD_Un_disjoint:
- "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
- foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
- by (simp add: foldD_Un_Int
- left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
-
-subsection {* Products over Finite Sets *}
-
-constdefs
- finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
- "finprod G f A == if finite A
- then foldD (carrier G) (mult G o f) (one G) A
- else arbitrary"
-
-(*
-locale finite_prod = abelian_monoid + var prod +
- defines "prod == (%f A. if finite A
- then foldD (carrier G) (op \<otimes> o f) \<one> A
- else arbitrary)"
-*)
-(* TODO: nice syntax for the summation operator inside the locale
- like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
-
-ML_setup {*
-
-Context.>> (fn thy => (simpset_ref_of thy :=
- simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
-
-lemma (in abelian_monoid) finprod_empty [simp]:
- "finprod G f {} = \<one>"
- by (simp add: finprod_def)
-
-ML_setup {*
-
-Context.>> (fn thy => (simpset_ref_of thy :=
- simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
-
-declare funcsetI [intro]
- funcset_mem [dest]
-
-lemma (in abelian_monoid) finprod_insert [simp]:
- "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
- finprod G f (insert a F) = f a \<otimes> finprod G f F"
- apply (rule trans)
- apply (simp add: finprod_def)
- apply (rule trans)
- apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
- apply simp
- apply (rule m_lcomm)
- apply fast apply fast apply assumption
- apply (fastsimp intro: m_closed)
- apply simp+ apply fast
- apply (auto simp add: finprod_def)
- done
-
-lemma (in abelian_monoid) finprod_one:
- "finite A ==> finprod G (%i. \<one>) A = \<one>"
-proof (induct set: Finites)
- case empty show ?case by simp
-next
- case (insert A a)
- have "(%i. \<one>) \<in> A -> carrier G" by auto
- with insert show ?case by simp
-qed
-
-lemma (in abelian_monoid) finprod_closed [simp]:
- fixes A
- assumes fin: "finite A" and f: "f \<in> A -> carrier G"
- shows "finprod G f A \<in> carrier G"
-using fin f
-proof induct
- case empty show ?case by simp
-next
- case (insert A a)
- then have a: "f a \<in> carrier G" by fast
- from insert have A: "f \<in> A -> carrier G" by fast
- from insert A a show ?case by simp
-qed
-
-lemma funcset_Int_left [simp, intro]:
- "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
- by fast
-
-lemma funcset_Un_left [iff]:
- "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
- by fast
-
-lemma (in abelian_monoid) finprod_Un_Int:
- "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
- finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
- finprod G g A \<otimes> finprod G g B"
- -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-proof (induct set: Finites)
- case empty then show ?case by (simp add: finprod_closed)
-next
- case (insert A a)
- then have a: "g a \<in> carrier G" by fast
- from insert have A: "g \<in> A -> carrier G" by fast
- from insert A a show ?case
- by (simp add: ac Int_insert_left insert_absorb finprod_closed
- Int_mono2 Un_subset_iff)
-qed
-
-lemma (in abelian_monoid) finprod_Un_disjoint:
- "[| finite A; finite B; A Int B = {};
- g \<in> A -> carrier G; g \<in> B -> carrier G |]
- ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
- apply (subst finprod_Un_Int [symmetric])
- apply (auto simp add: finprod_closed)
- done
-
-lemma (in abelian_monoid) finprod_multf:
- "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
- finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
-proof (induct set: Finites)
- case empty show ?case by simp
-next
- case (insert A a) then
- have fA: "f : A -> carrier G" by fast
- from insert have fa: "f a : carrier G" by fast
- from insert have gA: "g : A -> carrier G" by fast
- from insert have ga: "g a : carrier G" by fast
- from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
- from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
- by (simp add: Pi_def)
- show ?case (* check if all simps are really necessary *)
- by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
-qed
-
-lemma (in abelian_monoid) finprod_cong':
- "[| A = B; g : B -> carrier G;
- !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
-proof -
- assume prems: "A = B" "g : B -> carrier G"
- "!!i. i : B ==> f i = g i"
- show ?thesis
- proof (cases "finite B")
- case True
- then have "!!A. [| A = B; g : B -> carrier G;
- !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
- proof induct
- case empty thus ?case by simp
- next
- case (insert B x)
- then have "finprod G f A = finprod G f (insert x B)" by simp
- also from insert have "... = f x \<otimes> finprod G f B"
- proof (intro finprod_insert)
- show "finite B" .
- next
- show "x ~: B" .
- next
- assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
- "g \<in> insert x B \<rightarrow> carrier G"
- thus "f : B -> carrier G" by fastsimp
- next
- assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
- "g \<in> insert x B \<rightarrow> carrier G"
- thus "f x \<in> carrier G" by fastsimp
- qed
- also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
- also from insert have "... = finprod G g (insert x B)"
- by (intro finprod_insert [THEN sym]) auto
- finally show ?case .
- qed
- with prems show ?thesis by simp
- next
- case False with prems show ?thesis by (simp add: finprod_def)
- qed
-qed
-
-lemma (in abelian_monoid) finprod_cong:
- "[| A = B; !!i. i : B ==> f i = g i;
- g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
- by (rule finprod_cong') fast+
-
-text {*Usually, if this rule causes a failed congruence proof error,
- the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
- Adding @{thm [source] Pi_def} to the simpset is often useful.
- For this reason, @{thm [source] abelian_monoid.finprod_cong}
- is not added to the simpset by default.
-*}
-
-declare funcsetI [rule del]
- funcset_mem [rule del]
-
-lemma (in abelian_monoid) finprod_0 [simp]:
- "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
-by (simp add: Pi_def)
-
-lemma (in abelian_monoid) finprod_Suc [simp]:
- "f : {..Suc n} -> carrier G ==>
- finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
-by (simp add: Pi_def atMost_Suc)
-
-lemma (in abelian_monoid) finprod_Suc2:
- "f : {..Suc n} -> carrier G ==>
- finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
-proof (induct n)
- case 0 thus ?case by (simp add: Pi_def)
-next
- case Suc thus ?case by (simp add: m_assoc Pi_def finprod_closed)
-qed
-
-lemma (in abelian_monoid) finprod_mult [simp]:
- "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
- finprod G (%i. f i \<otimes> g i) {..n::nat} =
- finprod G f {..n} \<otimes> finprod G g {..n}"
- by (induct n) (simp_all add: ac Pi_def finprod_closed)
-
-end
-
--- a/src/HOL/Algebra/poly/PolyHomo.thy Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.thy Wed Apr 30 10:01:35 2003 +0200
@@ -4,7 +4,7 @@
Author: Clemens Ballarin, started 15 April 1997
*)
-PolyHomo = UnivPoly +
+PolyHomo = UnivPoly2 +
consts
EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
--- a/src/HOL/Algebra/poly/UnivPoly.ML Tue Apr 29 12:36:49 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,359 +0,0 @@
-(*
- Degree of polynomials
- $Id$
- written by Clemens Ballarin, started 22 January 1997
-*)
-
-(*
-(* Relating degree and bound *)
-
-Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
-by (force_tac (claset() addDs [inst "m" "n" boundD],
- simpset()) 1);
-qed "below_bound";
-
-goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
-by (rtac exE 1);
-by (rtac LeastI 2);
-by (assume_tac 2);
-by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
-by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
-qed "Least_is_bound";
-
-Goalw [coeff_def, deg_def]
- "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
-by (rtac Least_le 1);
-by (Fast_tac 1);
-qed "deg_aboveI";
-
-Goalw [coeff_def, deg_def]
- "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
-by (case_tac "n = 0" 1);
-(* Case n=0 *)
-by (Asm_simp_tac 1);
-(* Case n~=0 *)
-by (rotate_tac 1 1);
-by (Asm_full_simp_tac 1);
-by (rtac below_bound 1);
-by (assume_tac 2);
-by (rtac Least_is_bound 1);
-qed "deg_belowI";
-
-Goalw [coeff_def, deg_def]
- "deg p < m ==> coeff m p = 0";
-by (rtac exE 1); (* create !! x. *)
-by (rtac boundD 2);
-by (assume_tac 3);
-by (rtac LeastI 2);
-by (assume_tac 2);
-by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
-by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
-qed "deg_aboveD";
-
-Goalw [deg_def]
- "deg p = Suc y ==> ~ bound y (Rep_UP p)";
-by (rtac not_less_Least 1);
-by (Asm_simp_tac 1);
-val lemma1 = result();
-
-Goalw [deg_def, coeff_def]
- "deg p = Suc y ==> coeff (deg p) p ~= 0";
-by (rtac ccontr 1);
-by (dtac notnotD 1);
-by (cut_inst_tac [("p", "p")] Least_is_bound 1);
-by (subgoal_tac "bound y (Rep_UP p)" 1);
-(* prove subgoal *)
-by (rtac boundI 2);
-by (case_tac "Suc y < m" 2);
-(* first case *)
-by (rtac boundD 2);
-by (assume_tac 2);
-by (Asm_simp_tac 2);
-(* second case *)
-by (dtac leI 2);
-by (dtac Suc_leI 2);
-by (dtac le_anti_sym 2);
-by (assume_tac 2);
-by (Asm_full_simp_tac 2);
-(* end prove subgoal *)
-by (fold_goals_tac [deg_def]);
-by (dtac lemma1 1);
-by (etac notE 1);
-by (assume_tac 1);
-val lemma2 = result();
-
-Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
-by (rtac lemma2 1);
-by (Full_simp_tac 1);
-by (dtac Suc_pred 1);
-by (rtac sym 1);
-by (Asm_simp_tac 1);
-qed "deg_lcoeff";
-
-Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
-by (etac contrapos_np 1);
-by (case_tac "deg p = 0" 1);
-by (blast_tac (claset() addSDs [deg_lcoeff]) 2);
-by (rtac up_eqI 1);
-by (case_tac "n=0" 1);
-by (rotate_tac ~2 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-qed "nonzero_lcoeff";
-
-Goal "(deg p <= n) = bound n (Rep_UP p)";
-by (rtac iffI 1);
-(* ==> *)
-by (rtac boundI 1);
-by (fold_goals_tac [coeff_def]);
-by (rtac deg_aboveD 1);
-by (fast_arith_tac 1);
-(* <== *)
-by (rtac deg_aboveI 1);
-by (rewtac coeff_def);
-by (Fast_tac 1);
-qed "deg_above_is_bound";
-
-(* Lemmas on the degree function *)
-
-Goalw [max_def]
- "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
-by (case_tac "deg p <= deg q" 1);
-(* case deg p <= deg q *)
-by (rtac deg_aboveI 1);
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (dtac le_less_trans 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-(* case deg p > deg q *)
-by (rtac deg_aboveI 1);
-by (Asm_simp_tac 1);
-by (dtac not_leE 1);
-by (strip_tac 1);
-by (dtac less_trans 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-qed "deg_add";
-
-Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
-by (rtac order_antisym 1);
-by (rtac le_trans 1);
-by (rtac deg_add 1);
-by (Asm_simp_tac 1);
-by (rtac deg_belowI 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
-qed "deg_add_equal";
-
-Goal "deg (monom m::'a::ring up) <= m";
-by (asm_simp_tac
- (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
-qed "deg_monom_ring";
-
-Goal "deg (monom m::'a::domain up) = m";
-by (rtac le_anti_sym 1);
-(* <= *)
-by (rtac deg_monom_ring 1);
-(* >= *)
-by (asm_simp_tac
- (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
-qed "deg_monom";
-
-Goal "!! a::'a::ring. deg (const a) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-by (rtac deg_belowI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-qed "deg_const";
-
-Goal "deg (0::'a::ringS up) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (Simp_tac 1);
-by (rtac deg_belowI 1);
-by (Simp_tac 1);
-qed "deg_zero";
-
-Goal "deg (<1>::'a::ring up) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-by (rtac deg_belowI 1);
-by (Simp_tac 1);
-qed "deg_one";
-
-Goal "!!p::('a::ring) up. deg (-p) = deg p";
-by (rtac le_anti_sym 1);
-(* <= *)
-by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
-by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
-qed "deg_uminus";
-
-Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
-
-Goal
- "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
-by (case_tac "a = 0" 1);
-by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
-qed "deg_smult_ring";
-
-Goal
- "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
-by (rtac le_anti_sym 1);
-by (rtac deg_smult_ring 1);
-by (case_tac "a = 0" 1);
-by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
-qed "deg_smult";
-
-Goal
- "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
-\ coeff i p * coeff (k - i) q = 0";
-by (simp_tac (simpset() addsimps [coeff_def]) 1);
-by (rtac bound_mult_zero 1);
-by (assume_tac 3);
-by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
-by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
-qed "deg_above_mult_zero";
-
-Goal
- "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
-by (rtac deg_aboveI 1);
-by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
-qed "deg_mult_ring";
-
-goal Main.thy
- "!!k::nat. k < n ==> m < n + m - k";
-by (arith_tac 1);
-qed "less_add_diff";
-
-Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
-(* More general than deg_belowI, and simplifies the next proof! *)
-by (rtac deg_belowI 1);
-by (Fast_tac 1);
-qed "deg_below2I";
-
-Goal
- "!! p::'a::domain up. \
-\ [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
-by (rtac le_anti_sym 1);
-by (rtac deg_mult_ring 1);
-(* deg p + deg q <= deg (p * q) *)
-by (rtac deg_below2I 1);
-by (Simp_tac 1);
-(*
-by (rtac conjI 1);
-by (rtac impI 1);
-*)
-by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
-by (rtac le_add1 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
-by (rtac le_refl 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
-(*
-by (rtac impI 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
-by (rtac le_add1 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
-by (rtac le_refl 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
-*)
-qed "deg_mult";
-
-Addsimps [deg_smult, deg_mult];
-
-(* Representation theorems about polynomials *)
-
-goal PolyRing.thy
- "!! p::nat=>'a::ring up. \
-\ coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "coeff_SUM";
-
-goal UnivPoly.thy
- "!! f::(nat=>'a::ring). \
-\ bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
-by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
-by (auto_tac
- (claset() addDs [not_leE],
- simpset()));
-qed "bound_SUM_if";
-
-Goal
- "!! p::'a::ring up. deg p <= n ==> \
-\ setsum (%i. coeff i p *s monom i) {..n} = p";
-by (rtac up_eqI 1);
-by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
-by (rtac trans 1);
-by (res_inst_tac [("x", "na")] bound_SUM_if 2);
-by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
-by (rtac SUM_cong 1);
-by (rtac refl 1);
-by (Asm_simp_tac 1);
-qed "up_repr";
-
-Goal
- "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
-\ P (setsum (%i. coeff i p *s monom i) {..n})";
-by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
-qed "up_reprD";
-
-Goal
- "!! p::'a::ring up. \
-\ [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
-\ ==> P p";
-by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
-qed "up_repr2D";
-
-(*
-Goal
- "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
-\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
-\ = (coeff k f = coeff k g)
-...
-qed "up_unique";
-*)
-
-(* Polynomials over integral domains are again integral domains *)
-
-Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
-by (rtac classical 1);
-by (subgoal_tac "deg p = 0 & deg q = 0" 1);
-by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
-by (Asm_simp_tac 1);
-by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
-by (force_tac (claset() addIs [up_eqI], simpset()) 1);
-by (rtac integral 1);
-by (subgoal_tac "coeff 0 (p * q) = 0" 1);
-by (Asm_simp_tac 2);
-by (Full_simp_tac 1);
-by (dres_inst_tac [("f", "deg")] arg_cong 1);
-by (Asm_full_simp_tac 1);
-qed "up_integral";
-
-Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
-by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
-by (dtac up_integral 1);
-by Auto_tac;
-by (rtac (const_inj RS injD) 1);
-by (Simp_tac 1);
-qed "smult_integral";
-*)
-
-(* Divisibility and degree *)
-
-Goalw [dvd_def]
- "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
-by (etac exE 1);
-by (hyp_subst_tac 1);
-by (case_tac "p = 0" 1);
-by (case_tac "k = 0" 2);
-by Auto_tac;
-qed "dvd_imp_deg";
--- a/src/HOL/Algebra/poly/UnivPoly.thy Tue Apr 29 12:36:49 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,779 +0,0 @@
-(*
- Title: Univariate Polynomials
- Id: $Id$
- Author: Clemens Ballarin, started 9 December 1996
- Copyright: Clemens Ballarin
-*)
-
-header {* Univariate Polynomials *}
-
-theory UnivPoly = Abstract:
-
-(* already proved in Finite_Set.thy
-
-lemma setsum_cong:
- "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
-proof -
- assume prems: "A = B" "!!i. i : B ==> f i = g i"
- show ?thesis
- proof (cases "finite B")
- case True
- then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
- setsum f A = setsum g B"
- proof induct
- case empty thus ?case by simp
- next
- case insert thus ?case by simp
- qed
- with prems show ?thesis by simp
- next
- case False with prems show ?thesis by (simp add: setsum_def)
- qed
-qed
-*)
-
-(* Instruct simplifier to simplify assumptions introduced by congs.
- This makes setsum_cong more convenient to use, because assumptions
- like i:{m..n} get simplified (to m <= i & i <= n). *)
-
-ML_setup {*
-
-Addcongs [thm "setsum_cong"];
-Context.>> (fn thy => (simpset_ref_of thy :=
- simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
-
-section {* Definition of type up *}
-
-constdefs
- bound :: "[nat, nat => 'a::zero] => bool"
- "bound n f == (ALL i. n < i --> f i = 0)"
-
-lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
-proof (unfold bound_def)
-qed fast
-
-lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
-proof (unfold bound_def)
-qed fast
-
-lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
-proof (unfold bound_def)
-qed fast
-
-lemma bound_below:
- assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
-proof (rule classical)
- assume "~ ?thesis"
- then have "m < n" by arith
- with bound have "f n = 0" ..
- with nonzero show ?thesis by contradiction
-qed
-
-typedef (UP)
- ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
-by (rule+) (* Question: what does trace_rule show??? *)
-
-section {* Constants *}
-
-consts
- coeff :: "['a up, nat] => ('a::zero)"
- monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70)
- "*s" :: "['a::{zero, times}, 'a up] => 'a up" (infixl 70)
-
-defs
- coeff_def: "coeff p n == Rep_UP p n"
- monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
- smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
-
-lemma coeff_bound_ex: "EX n. bound n (coeff p)"
-proof -
- have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
- then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
- then show ?thesis ..
-qed
-
-lemma bound_coeff_obtain:
- assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
-proof -
- have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
- then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
- with prem show P .
-qed
-
-text {* Ring operations *}
-
-instance up :: (zero) zero ..
-instance up :: (one) one ..
-instance up :: (plus) plus ..
-instance up :: (minus) minus ..
-instance up :: (times) times ..
-instance up :: (inverse) inverse ..
-instance up :: (power) power ..
-
-defs
- up_add_def: "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
- up_mult_def: "p * q == Abs_UP (%n::nat. setsum
- (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
- up_zero_def: "0 == monom 0 0"
- up_one_def: "1 == monom 1 0"
- up_uminus_def:"- p == (- 1) *s p"
- (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
- (* note: - 1 is different from -1; latter is of class number *)
-
- up_minus_def: "(a::'a::{plus, minus} up) - b == a + (-b)"
- up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) ==
- (if a dvd 1 then THE x. a*x = 1 else 0)"
- up_divide_def: "(a::'a::{times, inverse} up) / b == a * inverse b"
- up_power_def: "(a::'a::{one, times, power} up) ^ n ==
- nat_rec 1 (%u b. b * a) n"
-
-subsection {* Effect of operations on coefficients *}
-
-lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
-proof -
- have "(%n. if n = m then a else 0) : UP"
- using UP_def by force
- from this show ?thesis
- by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_zero [simp]: "coeff 0 n = 0"
-proof (unfold up_zero_def)
-qed simp
-
-lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
-proof (unfold up_one_def)
-qed simp
-
-(* term order
-lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
-proof -
- have "!!f. f : UP ==> (%n. a * f n) : UP"
- by (unfold UP_def) (force simp add: ring_simps)
-*) (* this force step is slow *)
-(* then show ?thesis
- apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
-qed
-*)
-lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
-proof -
- have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
- by (unfold UP_def) (force simp add: ring_simps)
- (* this force step is slow *)
- then show ?thesis
- by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
-proof -
- {
- fix f g
- assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
- have "(%i. f i + g i) : UP"
- proof -
- from fup obtain n where boundn: "bound n f"
- by (unfold UP_def) fast
- from gup obtain m where boundm: "bound m g"
- by (unfold UP_def) fast
- have "bound (max n m) (%i. (f i + g i))"
- proof
- fix i
- assume "max n m < i"
- with boundn and boundm show "f i + g i = 0"
- by (fastsimp simp add: ring_simps)
- qed
- then show "(%i. (f i + g i)) : UP"
- by (unfold UP_def) fast
- qed
- }
- then show ?thesis
- by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_mult [simp]:
- "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
-proof -
- {
- fix f g
- assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
- have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
- proof -
- from fup obtain n where "bound n f"
- by (unfold UP_def) fast
- from gup obtain m where "bound m g"
- by (unfold UP_def) fast
- have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
- proof
- fix k
- assume bound: "n + m < k"
- {
- fix i
- have "f i * g (k-i) = 0"
- proof cases
- assume "n < i"
- show ?thesis by (auto! simp add: ring_simps)
- next
- assume "~ (n < i)"
- with bound have "m < k-i" by arith
- then show ?thesis by (auto! simp add: ring_simps)
- qed
- }
- then show "setsum (%i. f i * g (k-i)) {..k} = 0"
- by (simp add: ring_simps)
- qed
- then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
- by (unfold UP_def) fast
- qed
- }
- then show ?thesis
- by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
-by (unfold up_uminus_def) (simp add: ring_simps)
-
-(* Other lemmas *)
-
-lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
-proof -
- have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
- also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
- also have "... = q" by (simp add: Rep_UP_inverse)
- finally show ?thesis .
-qed
-
-(* ML_setup {* Addsimprocs [ring_simproc] *} *)
-
-instance up :: (ring) ring
-proof
- fix p q r :: "'a::ring up"
- fix n
- show "(p + q) + r = p + (q + r)"
- by (rule up_eqI) simp
- show "0 + p = p"
- by (rule up_eqI) simp
- show "(-p) + p = 0"
- by (rule up_eqI) simp
- show "p + q = q + p"
- by (rule up_eqI) simp
- show "(p * q) * r = p * (q * r)"
- proof (rule up_eqI)
- fix n
- {
- fix k and a b c :: "nat=>'a::ring"
- have "k <= n ==>
- setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} =
- setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}"
- (is "_ ==> ?eq k")
- proof (induct k)
- case 0 show ?case by simp
- next
- case (Suc k)
- then have "k <= n" by arith
- then have "?eq k" by (rule Suc)
- then show ?case
- by (simp add: Suc_diff_le natsum_ldistr)
- qed
- }
- then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
- by simp
- qed
- show "1 * p = p"
- proof (rule up_eqI)
- fix n
- show "coeff (1 * p) n = coeff p n"
- proof (cases n)
- case 0 then show ?thesis by simp
- next
- case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
- qed
- qed
- show "(p + q) * r = p * r + q * r"
- by (rule up_eqI) simp
- show "p * q = q * p"
- proof (rule up_eqI)
- fix n
- {
- fix k
- fix a b :: "nat=>'a::ring"
- have "k <= n ==>
- setsum (%i. a i * b (n-i)) {..k} =
- setsum (%i. a (k-i) * b (i+n-k)) {..k}"
- (is "_ ==> ?eq k")
- proof (induct k)
- case 0 show ?case by simp
- next
- case (Suc k) then show ?case by (subst natsum_Suc2) simp
- qed
- }
- then show "coeff (p * q) n = coeff (q * p) n"
- by simp
- qed
-
- show "p - q = p + (-q)"
- by (simp add: up_minus_def)
- show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
- by (simp add: up_inverse_def)
- show "p / q = p * inverse q"
- by (simp add: up_divide_def)
- show "p ^ n = nat_rec 1 (%u b. b * p) n"
- by (simp add: up_power_def)
- qed
-
-(* Further properties of monom *)
-
-lemma monom_zero [simp]:
- "monom 0 n = 0"
- by (simp add: monom_def up_zero_def)
-(* term order: application of coeff_mult goes wrong: rule not symmetric
-lemma monom_mult_is_smult:
- "monom (a::'a::ring) 0 * p = a *s p"
-proof (rule up_eqI)
- fix k
- show "coeff (monom a 0 * p) k = coeff (a *s p) k"
- proof (cases k)
- case 0 then show ?thesis by simp
- next
- case Suc then show ?thesis by simp
- qed
-qed
-*)
-ML_setup {* Delsimprocs [ring_simproc] *}
-
-lemma monom_mult_is_smult:
- "monom (a::'a::ring) 0 * p = a *s p"
-proof (rule up_eqI)
- fix k
- have "coeff (p * monom a 0) k = coeff (a *s p) k"
- proof (cases k)
- case 0 then show ?thesis by simp ring
- next
- case Suc then show ?thesis by (simp add: ring_simps) ring
- qed
- then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
-qed
-
-ML_setup {* Addsimprocs [ring_simproc] *}
-
-lemma monom_add [simp]:
- "monom (a + b) n = monom (a::'a::ring) n + monom b n"
-by (rule up_eqI) simp
-
-lemma monom_mult_smult:
- "monom (a * b) n = a *s monom (b::'a::ring) n"
-by (rule up_eqI) simp
-
-lemma monom_uminus [simp]:
- "monom (-a) n = - monom (a::'a::ring) n"
-by (rule up_eqI) simp
-
-lemma monom_one [simp]:
- "monom 1 0 = 1"
-by (simp add: up_one_def)
-
-lemma monom_inj:
- "(monom a n = monom b n) = (a = b)"
-proof
- assume "monom a n = monom b n"
- then have "coeff (monom a n) n = coeff (monom b n) n" by simp
- then show "a = b" by simp
-next
- assume "a = b" then show "monom a n = monom b n" by simp
-qed
-
-(* Properties of *s:
- Polynomials form a module *)
-
-lemma smult_l_distr:
- "(a + b::'a::ring) *s p = a *s p + b *s p"
-by (rule up_eqI) simp
-
-lemma smult_r_distr:
- "(a::'a::ring) *s (p + q) = a *s p + a *s q"
-by (rule up_eqI) simp
-
-lemma smult_assoc1:
- "(a * b::'a::ring) *s p = a *s (b *s p)"
-by (rule up_eqI) simp
-
-lemma smult_one [simp]:
- "(1::'a::ring) *s p = p"
-by (rule up_eqI) simp
-
-(* Polynomials form an algebra *)
-
-ML_setup {* Delsimprocs [ring_simproc] *}
-
-lemma smult_assoc2:
- "(a *s p) * q = (a::'a::ring) *s (p * q)"
-by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
-(* Simproc fails. *)
-
-ML_setup {* Addsimprocs [ring_simproc] *}
-
-(* the following can be derived from the above ones,
- for generality reasons, it is therefore done *)
-
-lemma smult_l_null [simp]:
- "(0::'a::ring) *s p = 0"
-proof -
- fix a
- have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
- also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
- also have "... = 0" by simp
- finally show ?thesis .
-qed
-
-lemma smult_r_null [simp]:
- "(a::'a::ring) *s 0 = 0";
-proof -
- fix p
- have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
- also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
- also have "... = 0" by simp
- finally show ?thesis .
-qed
-
-lemma smult_l_minus:
- "(-a::'a::ring) *s p = - (a *s p)"
-proof -
- have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp
- also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
- also have "... = -(a *s p)" by simp
- finally show ?thesis .
-qed
-
-lemma smult_r_minus:
- "(a::'a::ring) *s (-p) = - (a *s p)"
-proof -
- have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
- also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
- also have "... = -(a *s p)" by simp
- finally show ?thesis .
-qed
-
-section {* The degree function *}
-
-constdefs
- deg :: "('a::zero) up => nat"
- "deg p == LEAST n. bound n (coeff p)"
-
-lemma deg_aboveI:
- "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
-by (unfold deg_def) (fast intro: Least_le)
-
-lemma deg_aboveD:
- assumes prem: "deg p < m" shows "coeff p m = 0"
-proof -
- obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
- then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
- then show "coeff p m = 0" by (rule boundD)
-qed
-
-lemma deg_belowI:
- assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
-(* logically, this is a slightly stronger version of deg_aboveD *)
-proof (cases "n=0")
- case True then show ?thesis by simp
-next
- case False then have "coeff p n ~= 0" by (rule prem)
- then have "~ deg p < n" by (fast dest: deg_aboveD)
- then show ?thesis by arith
-qed
-
-lemma lcoeff_nonzero_deg:
- assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
-proof -
- obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
- proof -
- have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
- by arith (* make public?, why does proof not work with "1" *)
- from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
- by (unfold deg_def) arith
- then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
- then have "EX m. deg p - 1 < m & coeff p m ~= 0"
- by (unfold bound_def) fast
- then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
- then show ?thesis by auto
- qed
- with deg_belowI have "deg p = m" by fastsimp
- with m_coeff show ?thesis by simp
-qed
-
-lemma lcoeff_nonzero_nonzero:
- assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
-proof -
- have "EX m. coeff p m ~= 0"
- proof (rule classical)
- assume "~ ?thesis"
- then have "p = 0" by (auto intro: up_eqI)
- with nonzero show ?thesis by contradiction
- qed
- then obtain m where coeff: "coeff p m ~= 0" ..
- then have "m <= deg p" by (rule deg_belowI)
- then have "m = 0" by (simp add: deg)
- with coeff show ?thesis by simp
-qed
-
-lemma lcoeff_nonzero:
- "p ~= 0 ==> coeff p (deg p) ~= 0"
-proof (cases "deg p = 0")
- case True
- assume "p ~= 0"
- with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
-next
- case False
- assume "p ~= 0"
- with False show ?thesis by (simp add: lcoeff_nonzero_deg)
-qed
-
-lemma deg_eqI:
- "[| !!m. n < m ==> coeff p m = 0;
- !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
-by (fast intro: le_anti_sym deg_aboveI deg_belowI)
-
-(* Degree and polynomial operations *)
-
-lemma deg_add [simp]:
- "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
-proof (cases "deg p <= deg q")
- case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD)
-next
- case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
-qed
-
-lemma deg_monom_ring:
- "deg (monom a n::'a::ring up) <= n"
-by (rule deg_aboveI) simp
-
-lemma deg_monom [simp]:
- "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
-by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
-
-lemma deg_const [simp]:
- "deg (monom (a::'a::ring) 0) = 0"
-proof (rule le_anti_sym)
- show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
-next
- show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
-qed
-
-lemma deg_zero [simp]:
- "deg 0 = 0"
-proof (rule le_anti_sym)
- show "deg 0 <= 0" by (rule deg_aboveI) simp
-next
- show "0 <= deg 0" by (rule deg_belowI) simp
-qed
-
-lemma deg_one [simp]:
- "deg 1 = 0"
-proof (rule le_anti_sym)
- show "deg 1 <= 0" by (rule deg_aboveI) simp
-next
- show "0 <= deg 1" by (rule deg_belowI) simp
-qed
-
-lemma uminus_monom:
- "!!a::'a::ring. (-a = 0) = (a = 0)"
-proof
- fix a::"'a::ring"
- assume "a = 0"
- then show "-a = 0" by simp
-next
- fix a::"'a::ring"
- assume "- a = 0"
- then have "-(- a) = 0" by simp
- then show "a = 0" by simp
-qed
-
-lemma deg_uminus [simp]:
- "deg (-p::('a::ring) up) = deg p"
-proof (rule le_anti_sym)
- show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
-next
- show "deg p <= deg (- p)"
- by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
-qed
-
-lemma deg_smult_ring:
- "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
-proof (cases "a = 0")
-qed (simp add: deg_aboveI deg_aboveD)+
-
-lemma deg_smult [simp]:
- "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
-proof (rule le_anti_sym)
- show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
-next
- show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
- proof (cases "a = 0")
- qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
-qed
-
-lemma deg_mult_ring:
- "deg (p * q::'a::ring up) <= deg p + deg q"
-proof (rule deg_aboveI)
- fix m
- assume boundm: "deg p + deg q < m"
- {
- fix k i
- assume boundk: "deg p + deg q < k"
- then have "coeff p i * coeff q (k - i) = 0"
- proof (cases "deg p < i")
- case True then show ?thesis by (simp add: deg_aboveD)
- next
- case False with boundk have "deg q < k - i" by arith
- then show ?thesis by (simp add: deg_aboveD)
- qed
- }
- (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
- proofs. *)
- with boundm show "coeff (p * q) m = 0" by simp
-qed
-
-lemma deg_mult [simp]:
- "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
-proof (rule le_anti_sym)
- show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
-next
- let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
- assume nz: "p ~= 0" "q ~= 0"
- have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
- show "deg p + deg q <= deg (p * q)"
- proof (rule deg_belowI, simp)
- have "setsum ?s {.. deg p + deg q}
- = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
- by (simp only: ivl_disj_un_one)
- also have "... = setsum ?s {deg p .. deg p + deg q}"
- by (simp add: setsum_Un_disjoint ivl_disj_int_one
- setsum_0 deg_aboveD less_add_diff)
- also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
- by (simp only: ivl_disj_un_singleton)
- also have "... = coeff p (deg p) * coeff q (deg q)"
- by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
- setsum_0 deg_aboveD)
- finally have "setsum ?s {.. deg p + deg q}
- = coeff p (deg p) * coeff q (deg q)" .
- with nz show "setsum ?s {.. deg p + deg q} ~= 0"
- by (simp add: integral_iff lcoeff_nonzero)
- qed
- qed
-
-lemma coeff_natsum:
- "((coeff (setsum p A) k)::'a::ring) =
- setsum (%i. coeff (p i) k) A"
-proof (cases "finite A")
- case True then show ?thesis by induct auto
-next
- case False then show ?thesis by (simp add: setsum_def)
-qed
-(* Instance of a more general result!!! *)
-
-(*
-lemma coeff_natsum:
- "((coeff (setsum p {..n::nat}) k)::'a::ring) =
- setsum (%i. coeff (p i) k) {..n}"
-by (induct n) auto
-*)
-
-lemma up_repr:
- "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
-proof (rule up_eqI)
- let ?s = "(%i. monom (coeff p i) i)"
- fix k
- show "coeff (setsum ?s {..deg p}) k = coeff p k"
- proof (cases "k <= deg p")
- case True
- hence "coeff (setsum ?s {..deg p}) k =
- coeff (setsum ?s ({..k} Un {)k..deg p})) k"
- by (simp only: ivl_disj_un_one)
- also from True
- have "... = coeff (setsum ?s {..k}) k"
- by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
- setsum_0 coeff_natsum )
- also
- have "... = coeff (setsum ?s ({..k(} Un {k})) k"
- by (simp only: ivl_disj_un_singleton)
- also have "... = coeff p k"
- by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
- setsum_0 coeff_natsum deg_aboveD)
- finally show ?thesis .
- next
- case False
- hence "coeff (setsum ?s {..deg p}) k =
- coeff (setsum ?s ({..deg p(} Un {deg p})) k"
- by (simp only: ivl_disj_un_singleton)
- also from False have "... = coeff p k"
- by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
- setsum_0 coeff_natsum deg_aboveD)
- finally show ?thesis .
- qed
-qed
-
-lemma up_repr_le:
- "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
-proof -
- let ?s = "(%i. monom (coeff p i) i)"
- assume "deg p <= n"
- then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
- by (simp only: ivl_disj_un_one)
- also have "... = setsum ?s {..deg p}"
- by (simp add: setsum_Un_disjoint ivl_disj_int_one
- setsum_0 deg_aboveD)
- also have "... = p" by (rule up_repr)
- finally show ?thesis .
-qed
-
-instance up :: ("domain") "domain"
-proof
- show "1 ~= (0::'a up)"
- proof (* notI is applied here *)
- assume "1 = (0::'a up)"
- hence "coeff 1 0 = (coeff 0 0::'a)" by simp
- hence "1 = (0::'a)" by simp
- with one_not_zero show "False" by contradiction
- qed
-next
- fix p q :: "'a::domain up"
- assume pq: "p * q = 0"
- show "p = 0 | q = 0"
- proof (rule classical)
- assume c: "~ (p = 0 | q = 0)"
- then have "deg p + deg q = deg (p * q)" by simp
- also from pq have "... = 0" by simp
- finally have "deg p + deg q = 0" .
- then have f1: "deg p = 0 & deg q = 0" by simp
- from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
- by (simp only: up_repr_le)
- also have "... = monom (coeff p 0) 0" by simp
- finally have p: "p = monom (coeff p 0) 0" .
- from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
- by (simp only: up_repr_le)
- also have "... = monom (coeff q 0) 0" by simp
- finally have q: "q = monom (coeff q 0) 0" .
- have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
- also from pq have "... = 0" by simp
- finally have "coeff p 0 * coeff q 0 = 0" .
- then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
- with p q show "p = 0 | q = 0" by fastsimp
- qed
-qed
-
-lemma monom_inj_zero:
- "(monom a n = 0) = (a = 0)"
-proof -
- have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
- also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
- finally show ?thesis .
-qed
-(* term order: makes this simpler!!!
-lemma smult_integral:
- "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
-by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
-*)
-lemma smult_integral:
- "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
-by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
-
-end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/UnivPoly2.ML Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,359 @@
+(*
+ Degree of polynomials
+ $Id$
+ written by Clemens Ballarin, started 22 January 1997
+*)
+
+(*
+(* Relating degree and bound *)
+
+Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
+by (force_tac (claset() addDs [inst "m" "n" boundD],
+ simpset()) 1);
+qed "below_bound";
+
+goal UnivPoly2.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
+by (rtac exE 1);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "Least_is_bound";
+
+Goalw [coeff_def, deg_def]
+ "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
+by (rtac Least_le 1);
+by (Fast_tac 1);
+qed "deg_aboveI";
+
+Goalw [coeff_def, deg_def]
+ "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
+by (case_tac "n = 0" 1);
+(* Case n=0 *)
+by (Asm_simp_tac 1);
+(* Case n~=0 *)
+by (rotate_tac 1 1);
+by (Asm_full_simp_tac 1);
+by (rtac below_bound 1);
+by (assume_tac 2);
+by (rtac Least_is_bound 1);
+qed "deg_belowI";
+
+Goalw [coeff_def, deg_def]
+ "deg p < m ==> coeff m p = 0";
+by (rtac exE 1); (* create !! x. *)
+by (rtac boundD 2);
+by (assume_tac 3);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "deg_aboveD";
+
+Goalw [deg_def]
+ "deg p = Suc y ==> ~ bound y (Rep_UP p)";
+by (rtac not_less_Least 1);
+by (Asm_simp_tac 1);
+val lemma1 = result();
+
+Goalw [deg_def, coeff_def]
+ "deg p = Suc y ==> coeff (deg p) p ~= 0";
+by (rtac ccontr 1);
+by (dtac notnotD 1);
+by (cut_inst_tac [("p", "p")] Least_is_bound 1);
+by (subgoal_tac "bound y (Rep_UP p)" 1);
+(* prove subgoal *)
+by (rtac boundI 2);
+by (case_tac "Suc y < m" 2);
+(* first case *)
+by (rtac boundD 2);
+by (assume_tac 2);
+by (Asm_simp_tac 2);
+(* second case *)
+by (dtac leI 2);
+by (dtac Suc_leI 2);
+by (dtac le_anti_sym 2);
+by (assume_tac 2);
+by (Asm_full_simp_tac 2);
+(* end prove subgoal *)
+by (fold_goals_tac [deg_def]);
+by (dtac lemma1 1);
+by (etac notE 1);
+by (assume_tac 1);
+val lemma2 = result();
+
+Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
+by (rtac lemma2 1);
+by (Full_simp_tac 1);
+by (dtac Suc_pred 1);
+by (rtac sym 1);
+by (Asm_simp_tac 1);
+qed "deg_lcoeff";
+
+Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
+by (etac contrapos_np 1);
+by (case_tac "deg p = 0" 1);
+by (blast_tac (claset() addSDs [deg_lcoeff]) 2);
+by (rtac up_eqI 1);
+by (case_tac "n=0" 1);
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "nonzero_lcoeff";
+
+Goal "(deg p <= n) = bound n (Rep_UP p)";
+by (rtac iffI 1);
+(* ==> *)
+by (rtac boundI 1);
+by (fold_goals_tac [coeff_def]);
+by (rtac deg_aboveD 1);
+by (fast_arith_tac 1);
+(* <== *)
+by (rtac deg_aboveI 1);
+by (rewtac coeff_def);
+by (Fast_tac 1);
+qed "deg_above_is_bound";
+
+(* Lemmas on the degree function *)
+
+Goalw [max_def]
+ "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
+by (case_tac "deg p <= deg q" 1);
+(* case deg p <= deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (dtac le_less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+(* case deg p > deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (dtac not_leE 1);
+by (strip_tac 1);
+by (dtac less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "deg_add";
+
+Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
+by (rtac order_antisym 1);
+by (rtac le_trans 1);
+by (rtac deg_add 1);
+by (Asm_simp_tac 1);
+by (rtac deg_belowI 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
+qed "deg_add_equal";
+
+Goal "deg (monom m::'a::ring up) <= m";
+by (asm_simp_tac
+ (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
+qed "deg_monom_ring";
+
+Goal "deg (monom m::'a::domain up) = m";
+by (rtac le_anti_sym 1);
+(* <= *)
+by (rtac deg_monom_ring 1);
+(* >= *)
+by (asm_simp_tac
+ (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
+qed "deg_monom";
+
+Goal "!! a::'a::ring. deg (const a) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+qed "deg_const";
+
+Goal "deg (0::'a::ringS up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (Simp_tac 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_zero";
+
+Goal "deg (<1>::'a::ring up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_one";
+
+Goal "!!p::('a::ring) up. deg (-p) = deg p";
+by (rtac le_anti_sym 1);
+(* <= *)
+by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
+by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
+qed "deg_uminus";
+
+Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
+
+Goal
+ "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
+by (case_tac "a = 0" 1);
+by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
+qed "deg_smult_ring";
+
+Goal
+ "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
+by (rtac le_anti_sym 1);
+by (rtac deg_smult_ring 1);
+by (case_tac "a = 0" 1);
+by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
+qed "deg_smult";
+
+Goal
+ "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
+\ coeff i p * coeff (k - i) q = 0";
+by (simp_tac (simpset() addsimps [coeff_def]) 1);
+by (rtac bound_mult_zero 1);
+by (assume_tac 3);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+qed "deg_above_mult_zero";
+
+Goal
+ "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
+by (rtac deg_aboveI 1);
+by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
+qed "deg_mult_ring";
+
+goal Main.thy
+ "!!k::nat. k < n ==> m < n + m - k";
+by (arith_tac 1);
+qed "less_add_diff";
+
+Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
+(* More general than deg_belowI, and simplifies the next proof! *)
+by (rtac deg_belowI 1);
+by (Fast_tac 1);
+qed "deg_below2I";
+
+Goal
+ "!! p::'a::domain up. \
+\ [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
+by (rtac le_anti_sym 1);
+by (rtac deg_mult_ring 1);
+(* deg p + deg q <= deg (p * q) *)
+by (rtac deg_below2I 1);
+by (Simp_tac 1);
+(*
+by (rtac conjI 1);
+by (rtac impI 1);
+*)
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+(*
+by (rtac impI 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+*)
+qed "deg_mult";
+
+Addsimps [deg_smult, deg_mult];
+
+(* Representation theorems about polynomials *)
+
+goal PolyRing.thy
+ "!! p::nat=>'a::ring up. \
+\ coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "coeff_SUM";
+
+goal UnivPoly2.thy
+ "!! f::(nat=>'a::ring). \
+\ bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
+by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
+by (auto_tac
+ (claset() addDs [not_leE],
+ simpset()));
+qed "bound_SUM_if";
+
+Goal
+ "!! p::'a::ring up. deg p <= n ==> \
+\ setsum (%i. coeff i p *s monom i) {..n} = p";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
+by (rtac trans 1);
+by (res_inst_tac [("x", "na")] bound_SUM_if 2);
+by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
+by (rtac SUM_cong 1);
+by (rtac refl 1);
+by (Asm_simp_tac 1);
+qed "up_repr";
+
+Goal
+ "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
+\ P (setsum (%i. coeff i p *s monom i) {..n})";
+by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
+qed "up_reprD";
+
+Goal
+ "!! p::'a::ring up. \
+\ [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
+\ ==> P p";
+by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
+qed "up_repr2D";
+
+(*
+Goal
+ "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
+\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
+\ = (coeff k f = coeff k g)
+...
+qed "up_unique";
+*)
+
+(* Polynomials over integral domains are again integral domains *)
+
+Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
+by (rtac classical 1);
+by (subgoal_tac "deg p = 0 & deg q = 0" 1);
+by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
+by (force_tac (claset() addIs [up_eqI], simpset()) 1);
+by (rtac integral 1);
+by (subgoal_tac "coeff 0 (p * q) = 0" 1);
+by (Asm_simp_tac 2);
+by (Full_simp_tac 1);
+by (dres_inst_tac [("f", "deg")] arg_cong 1);
+by (Asm_full_simp_tac 1);
+qed "up_integral";
+
+Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
+by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
+by (dtac up_integral 1);
+by Auto_tac;
+by (rtac (const_inj RS injD) 1);
+by (Simp_tac 1);
+qed "smult_integral";
+*)
+
+(* Divisibility and degree *)
+
+Goalw [dvd_def]
+ "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (case_tac "p = 0" 1);
+by (case_tac "k = 0" 2);
+by Auto_tac;
+qed "dvd_imp_deg";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,779 @@
+(*
+ Title: Univariate Polynomials
+ Id: $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+ Copyright: Clemens Ballarin
+*)
+
+header {* Univariate Polynomials *}
+
+theory UnivPoly2 = Abstract:
+
+(* already proved in Finite_Set.thy
+
+lemma setsum_cong:
+ "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
+proof -
+ assume prems: "A = B" "!!i. i : B ==> f i = g i"
+ show ?thesis
+ proof (cases "finite B")
+ case True
+ then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
+ setsum f A = setsum g B"
+ proof induct
+ case empty thus ?case by simp
+ next
+ case insert thus ?case by simp
+ qed
+ with prems show ?thesis by simp
+ next
+ case False with prems show ?thesis by (simp add: setsum_def)
+ qed
+qed
+*)
+
+(* Instruct simplifier to simplify assumptions introduced by congs.
+ This makes setsum_cong more convenient to use, because assumptions
+ like i:{m..n} get simplified (to m <= i & i <= n). *)
+
+ML_setup {*
+
+Addcongs [thm "setsum_cong"];
+Context.>> (fn thy => (simpset_ref_of thy :=
+ simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+
+section {* Definition of type up *}
+
+constdefs
+ bound :: "[nat, nat => 'a::zero] => bool"
+ "bound n f == (ALL i. n < i --> f i = 0)"
+
+lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
+proof (unfold bound_def)
+qed fast
+
+lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
+proof (unfold bound_def)
+qed fast
+
+lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
+proof (unfold bound_def)
+qed fast
+
+lemma bound_below:
+ assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
+proof (rule classical)
+ assume "~ ?thesis"
+ then have "m < n" by arith
+ with bound have "f n = 0" ..
+ with nonzero show ?thesis by contradiction
+qed
+
+typedef (UP)
+ ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
+by (rule+) (* Question: what does trace_rule show??? *)
+
+section {* Constants *}
+
+consts
+ coeff :: "['a up, nat] => ('a::zero)"
+ monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70)
+ "*s" :: "['a::{zero, times}, 'a up] => 'a up" (infixl 70)
+
+defs
+ coeff_def: "coeff p n == Rep_UP p n"
+ monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
+ smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
+
+lemma coeff_bound_ex: "EX n. bound n (coeff p)"
+proof -
+ have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+ then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
+ then show ?thesis ..
+qed
+
+lemma bound_coeff_obtain:
+ assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
+proof -
+ have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+ then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
+ with prem show P .
+qed
+
+text {* Ring operations *}
+
+instance up :: (zero) zero ..
+instance up :: (one) one ..
+instance up :: (plus) plus ..
+instance up :: (minus) minus ..
+instance up :: (times) times ..
+instance up :: (inverse) inverse ..
+instance up :: (power) power ..
+
+defs
+ up_add_def: "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
+ up_mult_def: "p * q == Abs_UP (%n::nat. setsum
+ (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
+ up_zero_def: "0 == monom 0 0"
+ up_one_def: "1 == monom 1 0"
+ up_uminus_def:"- p == (- 1) *s p"
+ (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
+ (* note: - 1 is different from -1; latter is of class number *)
+
+ up_minus_def: "(a::'a::{plus, minus} up) - b == a + (-b)"
+ up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) ==
+ (if a dvd 1 then THE x. a*x = 1 else 0)"
+ up_divide_def: "(a::'a::{times, inverse} up) / b == a * inverse b"
+ up_power_def: "(a::'a::{one, times, power} up) ^ n ==
+ nat_rec 1 (%u b. b * a) n"
+
+subsection {* Effect of operations on coefficients *}
+
+lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
+proof -
+ have "(%n. if n = m then a else 0) : UP"
+ using UP_def by force
+ from this show ?thesis
+ by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_zero [simp]: "coeff 0 n = 0"
+proof (unfold up_zero_def)
+qed simp
+
+lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
+proof (unfold up_one_def)
+qed simp
+
+(* term order
+lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
+proof -
+ have "!!f. f : UP ==> (%n. a * f n) : UP"
+ by (unfold UP_def) (force simp add: ring_simps)
+*) (* this force step is slow *)
+(* then show ?thesis
+ apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
+qed
+*)
+lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
+proof -
+ have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
+ by (unfold UP_def) (force simp add: ring_simps)
+ (* this force step is slow *)
+ then show ?thesis
+ by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
+proof -
+ {
+ fix f g
+ assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
+ have "(%i. f i + g i) : UP"
+ proof -
+ from fup obtain n where boundn: "bound n f"
+ by (unfold UP_def) fast
+ from gup obtain m where boundm: "bound m g"
+ by (unfold UP_def) fast
+ have "bound (max n m) (%i. (f i + g i))"
+ proof
+ fix i
+ assume "max n m < i"
+ with boundn and boundm show "f i + g i = 0"
+ by (fastsimp simp add: ring_simps)
+ qed
+ then show "(%i. (f i + g i)) : UP"
+ by (unfold UP_def) fast
+ qed
+ }
+ then show ?thesis
+ by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_mult [simp]:
+ "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
+proof -
+ {
+ fix f g
+ assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
+ have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
+ proof -
+ from fup obtain n where "bound n f"
+ by (unfold UP_def) fast
+ from gup obtain m where "bound m g"
+ by (unfold UP_def) fast
+ have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
+ proof
+ fix k
+ assume bound: "n + m < k"
+ {
+ fix i
+ have "f i * g (k-i) = 0"
+ proof cases
+ assume "n < i"
+ show ?thesis by (auto! simp add: ring_simps)
+ next
+ assume "~ (n < i)"
+ with bound have "m < k-i" by arith
+ then show ?thesis by (auto! simp add: ring_simps)
+ qed
+ }
+ then show "setsum (%i. f i * g (k-i)) {..k} = 0"
+ by (simp add: ring_simps)
+ qed
+ then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
+ by (unfold UP_def) fast
+ qed
+ }
+ then show ?thesis
+ by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
+by (unfold up_uminus_def) (simp add: ring_simps)
+
+(* Other lemmas *)
+
+lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
+proof -
+ have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
+ also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
+ also have "... = q" by (simp add: Rep_UP_inverse)
+ finally show ?thesis .
+qed
+
+(* ML_setup {* Addsimprocs [ring_simproc] *} *)
+
+instance up :: (ring) ring
+proof
+ fix p q r :: "'a::ring up"
+ fix n
+ show "(p + q) + r = p + (q + r)"
+ by (rule up_eqI) simp
+ show "0 + p = p"
+ by (rule up_eqI) simp
+ show "(-p) + p = 0"
+ by (rule up_eqI) simp
+ show "p + q = q + p"
+ by (rule up_eqI) simp
+ show "(p * q) * r = p * (q * r)"
+ proof (rule up_eqI)
+ fix n
+ {
+ fix k and a b c :: "nat=>'a::ring"
+ have "k <= n ==>
+ setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} =
+ setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}"
+ (is "_ ==> ?eq k")
+ proof (induct k)
+ case 0 show ?case by simp
+ next
+ case (Suc k)
+ then have "k <= n" by arith
+ then have "?eq k" by (rule Suc)
+ then show ?case
+ by (simp add: Suc_diff_le natsum_ldistr)
+ qed
+ }
+ then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
+ by simp
+ qed
+ show "1 * p = p"
+ proof (rule up_eqI)
+ fix n
+ show "coeff (1 * p) n = coeff p n"
+ proof (cases n)
+ case 0 then show ?thesis by simp
+ next
+ case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
+ qed
+ qed
+ show "(p + q) * r = p * r + q * r"
+ by (rule up_eqI) simp
+ show "p * q = q * p"
+ proof (rule up_eqI)
+ fix n
+ {
+ fix k
+ fix a b :: "nat=>'a::ring"
+ have "k <= n ==>
+ setsum (%i. a i * b (n-i)) {..k} =
+ setsum (%i. a (k-i) * b (i+n-k)) {..k}"
+ (is "_ ==> ?eq k")
+ proof (induct k)
+ case 0 show ?case by simp
+ next
+ case (Suc k) then show ?case by (subst natsum_Suc2) simp
+ qed
+ }
+ then show "coeff (p * q) n = coeff (q * p) n"
+ by simp
+ qed
+
+ show "p - q = p + (-q)"
+ by (simp add: up_minus_def)
+ show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
+ by (simp add: up_inverse_def)
+ show "p / q = p * inverse q"
+ by (simp add: up_divide_def)
+ show "p ^ n = nat_rec 1 (%u b. b * p) n"
+ by (simp add: up_power_def)
+ qed
+
+(* Further properties of monom *)
+
+lemma monom_zero [simp]:
+ "monom 0 n = 0"
+ by (simp add: monom_def up_zero_def)
+(* term order: application of coeff_mult goes wrong: rule not symmetric
+lemma monom_mult_is_smult:
+ "monom (a::'a::ring) 0 * p = a *s p"
+proof (rule up_eqI)
+ fix k
+ show "coeff (monom a 0 * p) k = coeff (a *s p) k"
+ proof (cases k)
+ case 0 then show ?thesis by simp
+ next
+ case Suc then show ?thesis by simp
+ qed
+qed
+*)
+ML_setup {* Delsimprocs [ring_simproc] *}
+
+lemma monom_mult_is_smult:
+ "monom (a::'a::ring) 0 * p = a *s p"
+proof (rule up_eqI)
+ fix k
+ have "coeff (p * monom a 0) k = coeff (a *s p) k"
+ proof (cases k)
+ case 0 then show ?thesis by simp ring
+ next
+ case Suc then show ?thesis by (simp add: ring_simps) ring
+ qed
+ then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
+qed
+
+ML_setup {* Addsimprocs [ring_simproc] *}
+
+lemma monom_add [simp]:
+ "monom (a + b) n = monom (a::'a::ring) n + monom b n"
+by (rule up_eqI) simp
+
+lemma monom_mult_smult:
+ "monom (a * b) n = a *s monom (b::'a::ring) n"
+by (rule up_eqI) simp
+
+lemma monom_uminus [simp]:
+ "monom (-a) n = - monom (a::'a::ring) n"
+by (rule up_eqI) simp
+
+lemma monom_one [simp]:
+ "monom 1 0 = 1"
+by (simp add: up_one_def)
+
+lemma monom_inj:
+ "(monom a n = monom b n) = (a = b)"
+proof
+ assume "monom a n = monom b n"
+ then have "coeff (monom a n) n = coeff (monom b n) n" by simp
+ then show "a = b" by simp
+next
+ assume "a = b" then show "monom a n = monom b n" by simp
+qed
+
+(* Properties of *s:
+ Polynomials form a module *)
+
+lemma smult_l_distr:
+ "(a + b::'a::ring) *s p = a *s p + b *s p"
+by (rule up_eqI) simp
+
+lemma smult_r_distr:
+ "(a::'a::ring) *s (p + q) = a *s p + a *s q"
+by (rule up_eqI) simp
+
+lemma smult_assoc1:
+ "(a * b::'a::ring) *s p = a *s (b *s p)"
+by (rule up_eqI) simp
+
+lemma smult_one [simp]:
+ "(1::'a::ring) *s p = p"
+by (rule up_eqI) simp
+
+(* Polynomials form an algebra *)
+
+ML_setup {* Delsimprocs [ring_simproc] *}
+
+lemma smult_assoc2:
+ "(a *s p) * q = (a::'a::ring) *s (p * q)"
+by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
+(* Simproc fails. *)
+
+ML_setup {* Addsimprocs [ring_simproc] *}
+
+(* the following can be derived from the above ones,
+ for generality reasons, it is therefore done *)
+
+lemma smult_l_null [simp]:
+ "(0::'a::ring) *s p = 0"
+proof -
+ fix a
+ have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
+ also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
+ also have "... = 0" by simp
+ finally show ?thesis .
+qed
+
+lemma smult_r_null [simp]:
+ "(a::'a::ring) *s 0 = 0";
+proof -
+ fix p
+ have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
+ also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
+ also have "... = 0" by simp
+ finally show ?thesis .
+qed
+
+lemma smult_l_minus:
+ "(-a::'a::ring) *s p = - (a *s p)"
+proof -
+ have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp
+ also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
+ also have "... = -(a *s p)" by simp
+ finally show ?thesis .
+qed
+
+lemma smult_r_minus:
+ "(a::'a::ring) *s (-p) = - (a *s p)"
+proof -
+ have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
+ also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
+ also have "... = -(a *s p)" by simp
+ finally show ?thesis .
+qed
+
+section {* The degree function *}
+
+constdefs
+ deg :: "('a::zero) up => nat"
+ "deg p == LEAST n. bound n (coeff p)"
+
+lemma deg_aboveI:
+ "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
+by (unfold deg_def) (fast intro: Least_le)
+
+lemma deg_aboveD:
+ assumes prem: "deg p < m" shows "coeff p m = 0"
+proof -
+ obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
+ then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
+ then show "coeff p m = 0" by (rule boundD)
+qed
+
+lemma deg_belowI:
+ assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
+(* logically, this is a slightly stronger version of deg_aboveD *)
+proof (cases "n=0")
+ case True then show ?thesis by simp
+next
+ case False then have "coeff p n ~= 0" by (rule prem)
+ then have "~ deg p < n" by (fast dest: deg_aboveD)
+ then show ?thesis by arith
+qed
+
+lemma lcoeff_nonzero_deg:
+ assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
+proof -
+ obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
+ proof -
+ have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
+ by arith (* make public?, why does proof not work with "1" *)
+ from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
+ by (unfold deg_def) arith
+ then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
+ then have "EX m. deg p - 1 < m & coeff p m ~= 0"
+ by (unfold bound_def) fast
+ then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
+ then show ?thesis by auto
+ qed
+ with deg_belowI have "deg p = m" by fastsimp
+ with m_coeff show ?thesis by simp
+qed
+
+lemma lcoeff_nonzero_nonzero:
+ assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
+proof -
+ have "EX m. coeff p m ~= 0"
+ proof (rule classical)
+ assume "~ ?thesis"
+ then have "p = 0" by (auto intro: up_eqI)
+ with nonzero show ?thesis by contradiction
+ qed
+ then obtain m where coeff: "coeff p m ~= 0" ..
+ then have "m <= deg p" by (rule deg_belowI)
+ then have "m = 0" by (simp add: deg)
+ with coeff show ?thesis by simp
+qed
+
+lemma lcoeff_nonzero:
+ "p ~= 0 ==> coeff p (deg p) ~= 0"
+proof (cases "deg p = 0")
+ case True
+ assume "p ~= 0"
+ with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
+next
+ case False
+ assume "p ~= 0"
+ with False show ?thesis by (simp add: lcoeff_nonzero_deg)
+qed
+
+lemma deg_eqI:
+ "[| !!m. n < m ==> coeff p m = 0;
+ !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
+by (fast intro: le_anti_sym deg_aboveI deg_belowI)
+
+(* Degree and polynomial operations *)
+
+lemma deg_add [simp]:
+ "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
+proof (cases "deg p <= deg q")
+ case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD)
+next
+ case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
+qed
+
+lemma deg_monom_ring:
+ "deg (monom a n::'a::ring up) <= n"
+by (rule deg_aboveI) simp
+
+lemma deg_monom [simp]:
+ "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
+by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
+
+lemma deg_const [simp]:
+ "deg (monom (a::'a::ring) 0) = 0"
+proof (rule le_anti_sym)
+ show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
+next
+ show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
+qed
+
+lemma deg_zero [simp]:
+ "deg 0 = 0"
+proof (rule le_anti_sym)
+ show "deg 0 <= 0" by (rule deg_aboveI) simp
+next
+ show "0 <= deg 0" by (rule deg_belowI) simp
+qed
+
+lemma deg_one [simp]:
+ "deg 1 = 0"
+proof (rule le_anti_sym)
+ show "deg 1 <= 0" by (rule deg_aboveI) simp
+next
+ show "0 <= deg 1" by (rule deg_belowI) simp
+qed
+
+lemma uminus_monom:
+ "!!a::'a::ring. (-a = 0) = (a = 0)"
+proof
+ fix a::"'a::ring"
+ assume "a = 0"
+ then show "-a = 0" by simp
+next
+ fix a::"'a::ring"
+ assume "- a = 0"
+ then have "-(- a) = 0" by simp
+ then show "a = 0" by simp
+qed
+
+lemma deg_uminus [simp]:
+ "deg (-p::('a::ring) up) = deg p"
+proof (rule le_anti_sym)
+ show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
+next
+ show "deg p <= deg (- p)"
+ by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
+qed
+
+lemma deg_smult_ring:
+ "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
+proof (cases "a = 0")
+qed (simp add: deg_aboveI deg_aboveD)+
+
+lemma deg_smult [simp]:
+ "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
+proof (rule le_anti_sym)
+ show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
+next
+ show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
+ proof (cases "a = 0")
+ qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
+qed
+
+lemma deg_mult_ring:
+ "deg (p * q::'a::ring up) <= deg p + deg q"
+proof (rule deg_aboveI)
+ fix m
+ assume boundm: "deg p + deg q < m"
+ {
+ fix k i
+ assume boundk: "deg p + deg q < k"
+ then have "coeff p i * coeff q (k - i) = 0"
+ proof (cases "deg p < i")
+ case True then show ?thesis by (simp add: deg_aboveD)
+ next
+ case False with boundk have "deg q < k - i" by arith
+ then show ?thesis by (simp add: deg_aboveD)
+ qed
+ }
+ (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
+ proofs. *)
+ with boundm show "coeff (p * q) m = 0" by simp
+qed
+
+lemma deg_mult [simp]:
+ "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
+proof (rule le_anti_sym)
+ show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
+next
+ let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
+ assume nz: "p ~= 0" "q ~= 0"
+ have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
+ show "deg p + deg q <= deg (p * q)"
+ proof (rule deg_belowI, simp)
+ have "setsum ?s {.. deg p + deg q}
+ = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
+ by (simp only: ivl_disj_un_one)
+ also have "... = setsum ?s {deg p .. deg p + deg q}"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_one
+ setsum_0 deg_aboveD less_add_diff)
+ also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
+ by (simp only: ivl_disj_un_singleton)
+ also have "... = coeff p (deg p) * coeff q (deg q)"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
+ setsum_0 deg_aboveD)
+ finally have "setsum ?s {.. deg p + deg q}
+ = coeff p (deg p) * coeff q (deg q)" .
+ with nz show "setsum ?s {.. deg p + deg q} ~= 0"
+ by (simp add: integral_iff lcoeff_nonzero)
+ qed
+ qed
+
+lemma coeff_natsum:
+ "((coeff (setsum p A) k)::'a::ring) =
+ setsum (%i. coeff (p i) k) A"
+proof (cases "finite A")
+ case True then show ?thesis by induct auto
+next
+ case False then show ?thesis by (simp add: setsum_def)
+qed
+(* Instance of a more general result!!! *)
+
+(*
+lemma coeff_natsum:
+ "((coeff (setsum p {..n::nat}) k)::'a::ring) =
+ setsum (%i. coeff (p i) k) {..n}"
+by (induct n) auto
+*)
+
+lemma up_repr:
+ "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
+proof (rule up_eqI)
+ let ?s = "(%i. monom (coeff p i) i)"
+ fix k
+ show "coeff (setsum ?s {..deg p}) k = coeff p k"
+ proof (cases "k <= deg p")
+ case True
+ hence "coeff (setsum ?s {..deg p}) k =
+ coeff (setsum ?s ({..k} Un {)k..deg p})) k"
+ by (simp only: ivl_disj_un_one)
+ also from True
+ have "... = coeff (setsum ?s {..k}) k"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
+ setsum_0 coeff_natsum )
+ also
+ have "... = coeff (setsum ?s ({..k(} Un {k})) k"
+ by (simp only: ivl_disj_un_singleton)
+ also have "... = coeff p k"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
+ setsum_0 coeff_natsum deg_aboveD)
+ finally show ?thesis .
+ next
+ case False
+ hence "coeff (setsum ?s {..deg p}) k =
+ coeff (setsum ?s ({..deg p(} Un {deg p})) k"
+ by (simp only: ivl_disj_un_singleton)
+ also from False have "... = coeff p k"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
+ setsum_0 coeff_natsum deg_aboveD)
+ finally show ?thesis .
+ qed
+qed
+
+lemma up_repr_le:
+ "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
+proof -
+ let ?s = "(%i. monom (coeff p i) i)"
+ assume "deg p <= n"
+ then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
+ by (simp only: ivl_disj_un_one)
+ also have "... = setsum ?s {..deg p}"
+ by (simp add: setsum_Un_disjoint ivl_disj_int_one
+ setsum_0 deg_aboveD)
+ also have "... = p" by (rule up_repr)
+ finally show ?thesis .
+qed
+
+instance up :: ("domain") "domain"
+proof
+ show "1 ~= (0::'a up)"
+ proof (* notI is applied here *)
+ assume "1 = (0::'a up)"
+ hence "coeff 1 0 = (coeff 0 0::'a)" by simp
+ hence "1 = (0::'a)" by simp
+ with one_not_zero show "False" by contradiction
+ qed
+next
+ fix p q :: "'a::domain up"
+ assume pq: "p * q = 0"
+ show "p = 0 | q = 0"
+ proof (rule classical)
+ assume c: "~ (p = 0 | q = 0)"
+ then have "deg p + deg q = deg (p * q)" by simp
+ also from pq have "... = 0" by simp
+ finally have "deg p + deg q = 0" .
+ then have f1: "deg p = 0 & deg q = 0" by simp
+ from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
+ by (simp only: up_repr_le)
+ also have "... = monom (coeff p 0) 0" by simp
+ finally have p: "p = monom (coeff p 0) 0" .
+ from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
+ by (simp only: up_repr_le)
+ also have "... = monom (coeff q 0) 0" by simp
+ finally have q: "q = monom (coeff q 0) 0" .
+ have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
+ also from pq have "... = 0" by simp
+ finally have "coeff p 0 * coeff q 0 = 0" .
+ then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
+ with p q show "p = 0 | q = 0" by fastsimp
+ qed
+qed
+
+lemma monom_inj_zero:
+ "(monom a n = 0) = (a = 0)"
+proof -
+ have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
+ also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
+ finally show ?thesis .
+qed
+(* term order: makes this simpler!!!
+lemma smult_integral:
+ "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
+by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
+*)
+lemma smult_integral:
+ "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
+by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
+
+end
\ No newline at end of file
--- a/src/HOL/Algebra/ringsimp.ML Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Wed Apr 30 10:01:35 2003 +0200
@@ -56,8 +56,8 @@
(*** Term order for commutative rings ***)
fun ring_ord a =
- find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
- "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
+ find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
+ "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"];
fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);