--- a/src/HOL/Algebra/CRing.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy Thu Apr 22 11:01:34 2004 +0200
@@ -16,12 +16,12 @@
text {* Derived operations. *}
-constdefs
- a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
+constdefs (structure R)
+ a_inv :: "[_, '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)"
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
locale abelian_monoid = struct G +
assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
@@ -183,10 +183,22 @@
*}
constdefs
- finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
+ finsum :: "[_, 'a => 'b, 'a set] => 'b"
"finsum G f A == finprod (| carrier = carrier G,
mult = add G, one = zero G |) f A"
+syntax
+ "_finsum" :: "index => idt => 'a set => 'b => 'b"
+ ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
+syntax (xsymbols)
+ "_finsum" :: "index => idt => 'a set => 'b => 'b"
+ ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+syntax (HTML output)
+ "_finsum" :: "index => idt => 'a set => 'b => 'b"
+ ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+translations
+ "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A" -- {* Beware of argument permutation! *}
+
(*
lemmas (in abelian_monoid) finsum_empty [simp] =
comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
@@ -214,7 +226,7 @@
folded finsum_def, simplified monoid_record_simps])
lemma (in abelian_monoid) finsum_zero [simp]:
- "finite A ==> finsum G (%i. \<zero>) A = \<zero>"
+ "finite A ==> (\<Oplus>i: A. \<zero>) = \<zero>"
by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
simplified monoid_record_simps])
--- a/src/HOL/Algebra/Coset.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy Thu Apr 22 11:01:34 2004 +0200
@@ -9,23 +9,23 @@
declare (in group) l_inv [simp] r_inv [simp]
-constdefs
- r_coset :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"
- "r_coset G H a == (% x. (mult G) x a) ` H"
+constdefs (structure G)
+ r_coset :: "[_,'a set, 'a] => 'a set"
+ "r_coset G H a == (% x. x \<otimes> a) ` H"
- l_coset :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
- "l_coset G a H == (% x. (mult G) a x) ` H"
+ l_coset :: "[_, 'a, 'a set] => 'a set"
+ "l_coset G a H == (% x. a \<otimes> x) ` H"
- rcosets :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
+ rcosets :: "[_, 'a set] => ('a set)set"
"rcosets G H == r_coset G H ` (carrier G)"
- 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_mult :: "[_, 'a set ,'a set] => 'a set"
+ "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
- set_inv :: "[('a,'b) monoid_scheme,'a set] => 'a set"
- "set_inv G H == (m_inv G) ` H"
+ set_inv :: "[_,'a set] => 'a set"
+ "set_inv G H == m_inv G ` H"
- normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "<|" 60)
+ normal :: "['a set, _] => bool" (infixl "<|" 60)
"normal H G == subgroup H G &
(\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
--- a/src/HOL/Algebra/FiniteProduct.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Thu Apr 22 11:01:34 2004 +0200
@@ -9,9 +9,10 @@
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 *)
+text {* Instantiation of @{text LC} from theory @{text Finite_Set} is not
+ possible, because here we have explicit typing rules like @{text "x
+ : carrier G"}. We introduce an explicit argument for the domain
+ @{text D}. *}
consts
foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
@@ -281,14 +282,23 @@
subsection {* Products over Finite Sets *}
-constdefs
- finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
+constdefs (structure G)
+ finprod :: "[_, 'a => 'b, 'a set] => 'b"
"finprod G f A == if finite A
- then foldD (carrier G) (mult G o f) (one G) A
+ then foldD (carrier G) (mult G 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 *)
+syntax
+ "_finprod" :: "index => idt => 'a set => 'b => 'b"
+ ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
+syntax (xsymbols)
+ "_finprod" :: "index => idt => 'a set => 'b => 'b"
+ ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+syntax (HTML output)
+ "_finprod" :: "index => idt => 'a set => 'b => 'b"
+ ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+translations
+ "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A" -- {* Beware of argument permutation! *}
ML_setup {*
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
@@ -324,7 +334,7 @@
done
lemma (in comm_monoid) finprod_one [simp]:
- "finite A ==> finprod G (%i. \<one>) A = \<one>"
+ "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
proof (induct set: Finites)
case empty show ?case by simp
next
--- a/src/HOL/Algebra/Group.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Group.thy Thu Apr 22 11:01:34 2004 +0200
@@ -31,14 +31,12 @@
record 'a monoid = "'a semigroup" +
one :: 'a ("\<one>\<index>")
-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)"
+constdefs (structure G)
+ m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
+ "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
- 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)}"
+ Units :: "_ => 'a set"
+ "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
consts
pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
@@ -492,20 +490,13 @@
subsection {* Direct Products *}
-constdefs
- DirProdSemigroup ::
- "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
- => ('a \<times> 'b) semigroup"
- (infixr "\<times>\<^sub>s" 80)
+constdefs (structure G and H)
+ DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup" (infixr "\<times>\<^sub>s" 80)
"G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
- mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
+ mult = (%(xg, xh) (yg, yh). (xg \<otimes> yg, xh \<otimes>\<^sub>2 yh)) |)"
- DirProdGroup ::
- "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
- (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 \<times> 'b) monoid" (infixr "\<times>\<^sub>g" 80)
+ "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>, \<one>\<^sub>2) |)"
lemma DirProdSemigroup_magma:
includes magma G + magma H
@@ -529,13 +520,13 @@
includes magma G + magma H
shows "magma (G \<times>\<^sub>g H)"
by (rule magma.intro)
- (auto simp add: DirProdGroup_def DirProdSemigroup_def)
+ (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
lemma DirProdGroup_semigroup_axioms:
includes semigroup G + semigroup H
shows "semigroup_axioms (G \<times>\<^sub>g H)"
by (rule semigroup_axioms.intro)
- (auto simp add: DirProdGroup_def DirProdSemigroup_def
+ (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
G.m_assoc H.m_assoc)
lemma DirProdGroup_semigroup:
@@ -545,26 +536,26 @@
by (fast intro: semigroup.intro
DirProdGroup_magma DirProdGroup_semigroup_axioms)
-(* ... and further lemmas for group ... *)
+text {* \dots\ and further lemmas for group \dots *}
lemma DirProdGroup_group:
includes group G + group H
shows "group (G \<times>\<^sub>g H)"
by (rule groupI)
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
- simp add: DirProdGroup_def DirProdSemigroup_def)
+ simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
lemma carrier_DirProdGroup [simp]:
"carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
- by (simp add: DirProdGroup_def DirProdSemigroup_def)
+ by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
lemma one_DirProdGroup [simp]:
"one (G \<times>\<^sub>g H) = (one G, one H)"
- by (simp add: DirProdGroup_def DirProdSemigroup_def);
+ by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
lemma mult_DirProdGroup [simp]:
"mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
- by (simp add: DirProdGroup_def DirProdSemigroup_def)
+ by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
lemma inv_DirProdGroup [simp]:
includes group G + group H
@@ -577,12 +568,11 @@
subsection {* Homomorphisms *}
-constdefs
- hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
- => ('a => 'b)set"
+constdefs (structure G and H)
+ hom :: "_ => _ => ('a => 'b) set"
"hom G H ==
{h. h \<in> carrier G -> carrier H &
- (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
+ (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^sub>2 h y)}"
lemma (in semigroup) hom:
includes semigroup G
--- a/src/HOL/Algebra/Lattice.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy Thu Apr 22 11:01:34 2004 +0200
@@ -25,40 +25,41 @@
"[| x \<sqsubseteq> y; y \<sqsubseteq> z;
x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
-constdefs
- less :: "[('a, 'm) order_scheme, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
- "less L x y == le L x y & x ~= y"
+constdefs (structure L)
+ less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
+ "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
- (* Upper and lower bounds of a set. *)
- Upper :: "[('a, 'm) order_scheme, 'a set] => 'a set"
+ -- {* Upper and lower bounds of a set. *}
+ Upper :: "[_, 'a set] => 'a set"
"Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> le L x u)} \<inter>
carrier L"
- Lower :: "[('a, 'm) order_scheme, 'a set] => 'a set"
+ Lower :: "[_, 'a set] => 'a set"
"Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> le L l x)} \<inter>
carrier L"
- (* Least and greatest, as predicate. *)
- least :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"
+ -- {* Least and greatest, as predicate. *}
+ least :: "[_, 'a, 'a set] => bool"
"least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. le L l x)"
- greatest :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"
+ greatest :: "[_, 'a, 'a set] => bool"
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. le L x g)"
- (* Supremum and infimum *)
- sup :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
- "sup L A == THE x. least L x (Upper L A)"
+ -- {* Supremum and infimum *}
+ sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
+ "\<Squnion>A == THE x. least L x (Upper L A)"
- inf :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
- "inf L A == THE x. greatest L x (Lower L A)"
+ inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
+ "\<Sqinter>A == THE x. greatest L x (Lower L A)"
- join :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
- "join L x y == sup L {x, y}"
+ join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
+ "x \<squnion> y == sup L {x, y}"
- meet :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
- "meet L x y == inf L {x, y}"
+ meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
+ "x \<sqinter> y == inf L {x, y}"
-(* Upper *)
+
+subsubsection {* Upper *}
lemma Upper_closed [intro, simp]:
"Upper L A \<subseteq> carrier L"
@@ -78,7 +79,8 @@
"A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
by (unfold Upper_def) blast
-(* Lower *)
+
+subsubsection {* Lower *}
lemma Lower_closed [intro, simp]:
"Lower L A \<subseteq> carrier L"
@@ -98,7 +100,8 @@
"A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
by (unfold Lower_def) blast
-(* least *)
+
+subsubsection {* least *}
lemma least_carrier [intro, simp]:
shows "least L l A ==> l \<in> carrier L"
@@ -131,7 +134,8 @@
from below show "ALL x : Upper L A. s \<sqsubseteq> x" by fast
qed
-(* greatest *)
+
+subsubsection {* greatest *}
lemma greatest_carrier [intro, simp]:
shows "greatest L l A ==> l \<in> carrier L"
@@ -199,8 +203,7 @@
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
by (rule joinI) (rule least_carrier)
-lemma (in partial_order) sup_of_singletonI:
- (* only reflexivity needed ? *)
+lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *)
"x \<in> carrier L ==> least L x (Upper L {x})"
by (rule least_UpperI) fast+
@@ -404,7 +407,7 @@
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
shows "x \<squnion> (y \<squnion> z) = \<Squnion> {x, y, z}"
proof (rule finite_sup_insertI)
- (* The textbook argument in Jacobson I, p 457 *)
+ -- {* The textbook argument in Jacobson I, p 457 *}
fix s
assume sup: "least L s (Upper L {x, y, z})"
show "x \<squnion> (y \<squnion> z) = s"
@@ -452,8 +455,7 @@
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
by (rule meetI) (rule greatest_carrier)
-lemma (in partial_order) inf_of_singletonI:
- (* only reflexivity needed ? *)
+lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *)
"x \<in> carrier L ==> greatest L x (Lower L {x})"
by (rule greatest_LowerI) fast+
@@ -765,17 +767,17 @@
by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
qed (assumption | rule complete_lattice_axioms.intro)+
-constdefs
- top :: "('a, 'm) order_scheme => 'a" ("\<top>\<index>")
- "top L == sup L (carrier L)"
+constdefs (structure L)
+ top :: "_ => 'a" ("\<top>\<index>")
+ "\<top> == sup L (carrier L)"
- bottom :: "('a, 'm) order_scheme => 'a" ("\<bottom>\<index>")
- "bottom L == inf L (carrier L)"
+ bottom :: "_ => 'a" ("\<bottom>\<index>")
+ "\<bottom> == inf L (carrier L)"
lemma (in complete_lattice) supI:
"[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
- ==> P (\<Squnion> A)"
+ ==> P (\<Squnion>A)"
proof (unfold sup_def)
assume L: "A \<subseteq> carrier L"
and P: "!!l. least L l (Upper L A) ==> P l"
--- a/src/HOL/Algebra/Module.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Module.thy Thu Apr 22 11:01:34 2004 +0200
@@ -32,61 +32,64 @@
(a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
lemma moduleI:
+ includes struct R + struct M
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"
+ "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 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)"
+ (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 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)"
+ 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 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)"
+ (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
and smult_one:
- "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+ "!!x. x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
shows "module R M"
by (auto intro: module.intro cring.axioms abelian_group.axioms
module_axioms.intro prems)
lemma algebraI:
+ includes struct R + struct M
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"
+ "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 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)"
+ (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 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)"
+ 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 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)"
+ (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
and smult_one:
- "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+ "!!x. x \<in> carrier M ==> (one R) \<odot>\<^sub>2 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)"
+ (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 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+
+ by (rule cring.intro)
lemma (in algebra) M_cring:
"cring M"
- by (rule cring.intro) assumption+
+ by (rule cring.intro)
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]:
--- a/src/HOL/Algebra/Sylow.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy Thu Apr 22 11:01:34 2004 +0200
@@ -15,8 +15,8 @@
subsection {*Order of a Group and Lagrange's Theorem*}
constdefs
- order :: "(('a,'b) semigroup_scheme) => nat"
- "order(S) == card(carrier S)"
+ order :: "('a,'b) semigroup_scheme => nat"
+ "order S == card (carrier S)"
theorem (in coset) lagrange:
"[| finite(carrier G); subgroup H G |]
--- a/src/HOL/Algebra/UnivPoly.thy Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Apr 22 11:01:34 2004 +0200
@@ -58,18 +58,18 @@
monom :: "['a, nat] => 'p"
coeff :: "['p, nat] => 'a"
-constdefs
- up :: "('a, 'm) ring_scheme => (nat => 'a) set"
- "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound (zero R) n f)}"
- UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
+constdefs (structure R)
+ up :: "_ => (nat => 'a) set"
+ "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero> n f)}"
+ UP :: "_ => ('a, nat => 'a) up_ring"
"UP R == (|
carrier = up R,
- mult = (%p:up R. %q:up R. %n. finsum R (%i. mult R (p i) (q (n-i))) {..n}),
- one = (%i. if i=0 then one R else zero R),
- zero = (%i. zero R),
- add = (%p:up R. %q:up R. %i. add R (p i) (q i)),
- smult = (%a:carrier R. %p:up R. %i. mult R a (p i)),
- monom = (%a:carrier R. %n i. if i=n then a else zero R),
+ mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)),
+ one = (%i. if i=0 then \<one> else \<zero>),
+ zero = (%i. \<zero>),
+ add = (%p:up R. %q:up R. %i. p i \<oplus> q i),
+ smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i),
+ monom = (%a:carrier R. %n i. if i=n then a else \<zero>),
coeff = (%p:up R. %n. p n) |)"
text {*
@@ -179,9 +179,8 @@
locale UP_domain = UP_cring + "domain" R
text {*
- Temporarily declare UP.P\_def as simp rule.
-*}
-(* TODO: use antiquotation once text (in locale) is supported. *)
+ Temporarily declare @{text UP.P_def} as simp rule.
+*} (* TODO: use antiquotation once text (in locale) is supported. *)
declare (in UP) P_def [simp]
@@ -785,9 +784,9 @@
subsection {* The degree function *}
-constdefs
- deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
- "deg R p == LEAST n. bound (zero R) n (coeff (UP R) p)"
+constdefs (structure R)
+ deg :: "[_, nat => 'a] => nat"
+ "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
lemma (in UP_cring) deg_aboveI:
"[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
@@ -1248,11 +1247,10 @@
"(%a. monom P a 0) \<in> ring_hom R P"
by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
-constdefs
- eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
- 'a => 'b, 'b, nat => 'a] => 'b"
- "eval R S phi s == (\<lambda>p \<in> carrier (UP R).
- finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p})"
+constdefs (structure S)
+ eval :: "[_, _, 'a => 'b, 'b, nat => 'a] => 'b"
+ "eval R S phi s == \<lambda>p \<in> carrier (UP R).
+ \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> pow S s i"
(*
"eval R S phi s p == if p \<in> carrier (UP R)
then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
@@ -1566,5 +1564,4 @@
-- {* Calculates @{term "x = 500"} *}
-
end