improved notation;
authorwenzelm
Thu Apr 22 11:01:34 2004 +0200 (2004-04-22)
changeset 1465102b8f3bcf7fe
parent 14650 0390abdd1e62
child 14652 5ddbdbadba06
improved notation;
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
     1.1 --- a/src/HOL/Algebra/CRing.thy	Thu Apr 22 11:00:22 2004 +0200
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Thu Apr 22 11:01:34 2004 +0200
     1.3 @@ -16,12 +16,12 @@
     1.4  
     1.5  text {* Derived operations. *}
     1.6  
     1.7 -constdefs
     1.8 -  a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
     1.9 +constdefs (structure R)
    1.10 +  a_inv :: "[_, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
    1.11    "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
    1.12  
    1.13    minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
    1.14 -  "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
    1.15 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
    1.16  
    1.17  locale abelian_monoid = struct G +
    1.18    assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
    1.19 @@ -183,10 +183,22 @@
    1.20  *}
    1.21  
    1.22  constdefs
    1.23 -  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
    1.24 +  finsum :: "[_, 'a => 'b, 'a set] => 'b"
    1.25    "finsum G f A == finprod (| carrier = carrier G,
    1.26       mult = add G, one = zero G |) f A"
    1.27  
    1.28 +syntax
    1.29 +  "_finsum" :: "index => idt => 'a set => 'b => 'b"
    1.30 +      ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
    1.31 +syntax (xsymbols)
    1.32 +  "_finsum" :: "index => idt => 'a set => 'b => 'b"
    1.33 +      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
    1.34 +syntax (HTML output)
    1.35 +  "_finsum" :: "index => idt => 'a set => 'b => 'b"
    1.36 +      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
    1.37 +translations
    1.38 +  "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
    1.39 +
    1.40  (*
    1.41    lemmas (in abelian_monoid) finsum_empty [simp] =
    1.42      comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
    1.43 @@ -214,7 +226,7 @@
    1.44      folded finsum_def, simplified monoid_record_simps])
    1.45  
    1.46  lemma (in abelian_monoid) finsum_zero [simp]:
    1.47 -  "finite A ==> finsum G (%i. \<zero>) A = \<zero>"
    1.48 +  "finite A ==> (\<Oplus>i: A. \<zero>) = \<zero>"
    1.49    by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
    1.50      simplified monoid_record_simps])
    1.51  
     2.1 --- a/src/HOL/Algebra/Coset.thy	Thu Apr 22 11:00:22 2004 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Thu Apr 22 11:01:34 2004 +0200
     2.3 @@ -9,23 +9,23 @@
     2.4  
     2.5  declare (in group) l_inv [simp]  r_inv [simp] 
     2.6  
     2.7 -constdefs
     2.8 -  r_coset    :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"    
     2.9 -   "r_coset G H a == (% x. (mult G) x a) ` H"
    2.10 +constdefs (structure G)
    2.11 +  r_coset    :: "[_,'a set, 'a] => 'a set"    
    2.12 +   "r_coset G H a == (% x. x \<otimes> a) ` H"
    2.13  
    2.14 -  l_coset    :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
    2.15 -   "l_coset G a H == (% x. (mult G) a x) ` H"
    2.16 +  l_coset    :: "[_, 'a, 'a set] => 'a set"
    2.17 +   "l_coset G a H == (% x. a \<otimes> x) ` H"
    2.18  
    2.19 -  rcosets  :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
    2.20 +  rcosets  :: "[_, 'a set] => ('a set)set"
    2.21     "rcosets G H == r_coset G H ` (carrier G)"
    2.22  
    2.23 -  set_mult  :: "[('a,'b) monoid_scheme,'a set,'a set] => 'a set"
    2.24 -   "set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
    2.25 +  set_mult  :: "[_, 'a set ,'a set] => 'a set"
    2.26 +   "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
    2.27  
    2.28 -  set_inv   :: "[('a,'b) monoid_scheme,'a set] => 'a set"
    2.29 -   "set_inv G H == (m_inv G) ` H"
    2.30 +  set_inv   :: "[_,'a set] => 'a set"
    2.31 +   "set_inv G H == m_inv G ` H"
    2.32  
    2.33 -  normal     :: "['a set, ('a,'b) monoid_scheme] => bool"       (infixl "<|" 60)
    2.34 +  normal     :: "['a set, _] => bool"       (infixl "<|" 60)
    2.35     "normal H G == subgroup H G & 
    2.36                    (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
    2.37  
     3.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 22 11:00:22 2004 +0200
     3.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 22 11:01:34 2004 +0200
     3.3 @@ -9,9 +9,10 @@
     3.4  
     3.5  theory FiniteProduct = Group:
     3.6  
     3.7 -(* Instantiation of LC from Finite_Set.thy is not possible,
     3.8 -   because here we have explicit typing rules like x : carrier G.
     3.9 -   We introduce an explicit argument for the domain D *)
    3.10 +text {* Instantiation of @{text LC} from theory @{text Finite_Set} is not
    3.11 +  possible, because here we have explicit typing rules like @{text "x
    3.12 +  : carrier G"}.  We introduce an explicit argument for the domain
    3.13 +  @{text D}. *}
    3.14  
    3.15  consts
    3.16    foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    3.17 @@ -281,14 +282,23 @@
    3.18  
    3.19  subsection {* Products over Finite Sets *}
    3.20  
    3.21 -constdefs
    3.22 -  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
    3.23 +constdefs (structure G)
    3.24 +  finprod :: "[_, 'a => 'b, 'a set] => 'b"
    3.25    "finprod G f A == if finite A
    3.26 -      then foldD (carrier G) (mult G o f) (one G) A
    3.27 +      then foldD (carrier G) (mult G o f) \<one> A
    3.28        else arbitrary"
    3.29  
    3.30 -(* TODO: nice syntax for the summation operator inside the locale
    3.31 -   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
    3.32 +syntax
    3.33 +  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    3.34 +      ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
    3.35 +syntax (xsymbols)
    3.36 +  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    3.37 +      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
    3.38 +syntax (HTML output)
    3.39 +  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    3.40 +      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
    3.41 +translations
    3.42 +  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
    3.43  
    3.44  ML_setup {* 
    3.45    simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    3.46 @@ -324,7 +334,7 @@
    3.47    done
    3.48  
    3.49  lemma (in comm_monoid) finprod_one [simp]:
    3.50 -  "finite A ==> finprod G (%i. \<one>) A = \<one>"
    3.51 +  "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
    3.52  proof (induct set: Finites)
    3.53    case empty show ?case by simp
    3.54  next
     4.1 --- a/src/HOL/Algebra/Group.thy	Thu Apr 22 11:00:22 2004 +0200
     4.2 +++ b/src/HOL/Algebra/Group.thy	Thu Apr 22 11:01:34 2004 +0200
     4.3 @@ -31,14 +31,12 @@
     4.4  record 'a monoid = "'a semigroup" +
     4.5    one :: 'a ("\<one>\<index>")
     4.6  
     4.7 -constdefs
     4.8 -  m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80)
     4.9 -  "m_inv G x == (THE y. y \<in> carrier G &
    4.10 -                  mult G x y = one G & mult G y x = one G)"
    4.11 +constdefs (structure G)
    4.12 +  m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
    4.13 +  "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
    4.14  
    4.15 -  Units :: "('a, 'm) monoid_scheme => 'a set"
    4.16 -  "Units G == {y. y \<in> carrier G &
    4.17 -                  (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"
    4.18 +  Units :: "_ => 'a set"
    4.19 +  "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    4.20  
    4.21  consts
    4.22    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    4.23 @@ -492,20 +490,13 @@
    4.24  
    4.25  subsection {* Direct Products *}
    4.26  
    4.27 -constdefs
    4.28 -  DirProdSemigroup ::
    4.29 -    "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
    4.30 -    => ('a \<times> 'b) semigroup"
    4.31 -    (infixr "\<times>\<^sub>s" 80)
    4.32 +constdefs (structure G and H)
    4.33 +  DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
    4.34    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
    4.35 -    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    4.36 +    mult = (%(xg, xh) (yg, yh). (xg \<otimes> yg, xh \<otimes>\<^sub>2 yh)) |)"
    4.37  
    4.38 -  DirProdGroup ::
    4.39 -    "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
    4.40 -    (infixr "\<times>\<^sub>g" 80)
    4.41 -  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
    4.42 -    mult = mult (G \<times>\<^sub>s H),
    4.43 -    one = (one G, one H) |)"
    4.44 +  DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
    4.45 +  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>, \<one>\<^sub>2) |)"
    4.46  
    4.47  lemma DirProdSemigroup_magma:
    4.48    includes magma G + magma H
    4.49 @@ -529,13 +520,13 @@
    4.50    includes magma G + magma H
    4.51    shows "magma (G \<times>\<^sub>g H)"
    4.52    by (rule magma.intro)
    4.53 -    (auto simp add: DirProdGroup_def DirProdSemigroup_def)
    4.54 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    4.55  
    4.56  lemma DirProdGroup_semigroup_axioms:
    4.57    includes semigroup G + semigroup H
    4.58    shows "semigroup_axioms (G \<times>\<^sub>g H)"
    4.59    by (rule semigroup_axioms.intro)
    4.60 -    (auto simp add: DirProdGroup_def DirProdSemigroup_def
    4.61 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
    4.62        G.m_assoc H.m_assoc)
    4.63  
    4.64  lemma DirProdGroup_semigroup:
    4.65 @@ -545,26 +536,26 @@
    4.66    by (fast intro: semigroup.intro
    4.67      DirProdGroup_magma DirProdGroup_semigroup_axioms)
    4.68  
    4.69 -(* ... and further lemmas for group ... *)
    4.70 +text {* \dots\ and further lemmas for group \dots *}
    4.71  
    4.72  lemma DirProdGroup_group:
    4.73    includes group G + group H
    4.74    shows "group (G \<times>\<^sub>g H)"
    4.75    by (rule groupI)
    4.76      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    4.77 -      simp add: DirProdGroup_def DirProdSemigroup_def)
    4.78 +      simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    4.79  
    4.80  lemma carrier_DirProdGroup [simp]:
    4.81       "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
    4.82 -  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    4.83 +  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    4.84  
    4.85  lemma one_DirProdGroup [simp]:
    4.86       "one (G \<times>\<^sub>g H) = (one G, one H)"
    4.87 -  by (simp add: DirProdGroup_def DirProdSemigroup_def);
    4.88 +  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    4.89  
    4.90  lemma mult_DirProdGroup [simp]:
    4.91       "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
    4.92 -  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    4.93 +  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    4.94  
    4.95  lemma inv_DirProdGroup [simp]:
    4.96    includes group G + group H
    4.97 @@ -577,12 +568,11 @@
    4.98  
    4.99  subsection {* Homomorphisms *}
   4.100  
   4.101 -constdefs
   4.102 -  hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
   4.103 -    => ('a => 'b)set"
   4.104 +constdefs (structure G and H)
   4.105 +  hom :: "_ => _ => ('a => 'b) set"
   4.106    "hom G H ==
   4.107      {h. h \<in> carrier G -> carrier H &
   4.108 -      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
   4.109 +      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^sub>2 h y)}"
   4.110  
   4.111  lemma (in semigroup) hom:
   4.112    includes semigroup G
     5.1 --- a/src/HOL/Algebra/Lattice.thy	Thu Apr 22 11:00:22 2004 +0200
     5.2 +++ b/src/HOL/Algebra/Lattice.thy	Thu Apr 22 11:01:34 2004 +0200
     5.3 @@ -25,40 +25,41 @@
     5.4                    "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
     5.5                     x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
     5.6  
     5.7 -constdefs
     5.8 -  less :: "[('a, 'm) order_scheme, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
     5.9 -  "less L x y == le L x y & x ~= y"
    5.10 +constdefs (structure L)
    5.11 +  less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    5.12 +  "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
    5.13  
    5.14 -  (* Upper and lower bounds of a set. *)
    5.15 -  Upper :: "[('a, 'm) order_scheme, 'a set] => 'a set"
    5.16 +  -- {* Upper and lower bounds of a set. *}
    5.17 +  Upper :: "[_, 'a set] => 'a set"
    5.18    "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> le L x u)} \<inter>
    5.19                  carrier L"
    5.20  
    5.21 -  Lower :: "[('a, 'm) order_scheme, 'a set] => 'a set"
    5.22 +  Lower :: "[_, 'a set] => 'a set"
    5.23    "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> le L l x)} \<inter>
    5.24                  carrier L"
    5.25  
    5.26 -  (* Least and greatest, as predicate. *)
    5.27 -  least :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"
    5.28 +  -- {* Least and greatest, as predicate. *}
    5.29 +  least :: "[_, 'a, 'a set] => bool"
    5.30    "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. le L l x)"
    5.31  
    5.32 -  greatest :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"
    5.33 +  greatest :: "[_, 'a, 'a set] => bool"
    5.34    "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. le L x g)"
    5.35  
    5.36 -  (* Supremum and infimum *)
    5.37 -  sup :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
    5.38 -  "sup L A == THE x. least L x (Upper L A)"
    5.39 +  -- {* Supremum and infimum *}
    5.40 +  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
    5.41 +  "\<Squnion>A == THE x. least L x (Upper L A)"
    5.42  
    5.43 -  inf :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
    5.44 -  "inf L A == THE x. greatest L x (Lower L A)"
    5.45 +  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
    5.46 +  "\<Sqinter>A == THE x. greatest L x (Lower L A)"
    5.47  
    5.48 -  join :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
    5.49 -  "join L x y == sup L {x, y}"
    5.50 +  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
    5.51 +  "x \<squnion> y == sup L {x, y}"
    5.52  
    5.53 -  meet :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
    5.54 -  "meet L x y == inf L {x, y}"
    5.55 +  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
    5.56 +  "x \<sqinter> y == inf L {x, y}"
    5.57  
    5.58 -(* Upper *)
    5.59 +
    5.60 +subsubsection {* Upper *}
    5.61  
    5.62  lemma Upper_closed [intro, simp]:
    5.63    "Upper L A \<subseteq> carrier L"
    5.64 @@ -78,7 +79,8 @@
    5.65    "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
    5.66    by (unfold Upper_def) blast
    5.67  
    5.68 -(* Lower *)
    5.69 +
    5.70 +subsubsection {* Lower *}
    5.71  
    5.72  lemma Lower_closed [intro, simp]:
    5.73    "Lower L A \<subseteq> carrier L"
    5.74 @@ -98,7 +100,8 @@
    5.75    "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
    5.76    by (unfold Lower_def) blast
    5.77  
    5.78 -(* least *)
    5.79 +
    5.80 +subsubsection {* least *}
    5.81  
    5.82  lemma least_carrier [intro, simp]:
    5.83    shows "least L l A ==> l \<in> carrier L"
    5.84 @@ -131,7 +134,8 @@
    5.85    from below show "ALL x : Upper L A. s \<sqsubseteq> x" by fast
    5.86  qed
    5.87  
    5.88 -(* greatest *)
    5.89 +
    5.90 +subsubsection {* greatest *}
    5.91  
    5.92  lemma greatest_carrier [intro, simp]:
    5.93    shows "greatest L l A ==> l \<in> carrier L"
    5.94 @@ -199,8 +203,7 @@
    5.95    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
    5.96    by (rule joinI) (rule least_carrier)
    5.97  
    5.98 -lemma (in partial_order) sup_of_singletonI:
    5.99 -  (* only reflexivity needed ? *)
   5.100 +lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   5.101    "x \<in> carrier L ==> least L x (Upper L {x})"
   5.102    by (rule least_UpperI) fast+
   5.103  
   5.104 @@ -404,7 +407,7 @@
   5.105    assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   5.106    shows "x \<squnion> (y \<squnion> z) = \<Squnion> {x, y, z}"
   5.107  proof (rule finite_sup_insertI)
   5.108 -  (* The textbook argument in Jacobson I, p 457 *)
   5.109 +  -- {* The textbook argument in Jacobson I, p 457 *}
   5.110    fix s
   5.111    assume sup: "least L s (Upper L {x, y, z})"
   5.112    show "x \<squnion> (y \<squnion> z) = s"
   5.113 @@ -452,8 +455,7 @@
   5.114    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   5.115    by (rule meetI) (rule greatest_carrier)
   5.116  
   5.117 -lemma (in partial_order) inf_of_singletonI:
   5.118 -  (* only reflexivity needed ? *)
   5.119 +lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   5.120    "x \<in> carrier L ==> greatest L x (Lower L {x})"
   5.121    by (rule greatest_LowerI) fast+
   5.122  
   5.123 @@ -765,17 +767,17 @@
   5.124    by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
   5.125  qed (assumption | rule complete_lattice_axioms.intro)+
   5.126  
   5.127 -constdefs
   5.128 -  top :: "('a, 'm) order_scheme => 'a" ("\<top>\<index>")
   5.129 -  "top L == sup L (carrier L)"
   5.130 +constdefs (structure L)
   5.131 +  top :: "_ => 'a" ("\<top>\<index>")
   5.132 +  "\<top> == sup L (carrier L)"
   5.133  
   5.134 -  bottom :: "('a, 'm) order_scheme => 'a" ("\<bottom>\<index>")
   5.135 -  "bottom L == inf L (carrier L)"
   5.136 +  bottom :: "_ => 'a" ("\<bottom>\<index>")
   5.137 +  "\<bottom> == inf L (carrier L)"
   5.138  
   5.139  
   5.140  lemma (in complete_lattice) supI:
   5.141    "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   5.142 -  ==> P (\<Squnion> A)"
   5.143 +  ==> P (\<Squnion>A)"
   5.144  proof (unfold sup_def)
   5.145    assume L: "A \<subseteq> carrier L"
   5.146      and P: "!!l. least L l (Upper L A) ==> P l"
     6.1 --- a/src/HOL/Algebra/Module.thy	Thu Apr 22 11:00:22 2004 +0200
     6.2 +++ b/src/HOL/Algebra/Module.thy	Thu Apr 22 11:01:34 2004 +0200
     6.3 @@ -32,61 +32,64 @@
     6.4        (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
     6.5  
     6.6  lemma moduleI:
     6.7 +  includes struct R + struct M
     6.8    assumes cring: "cring R"
     6.9      and abelian_group: "abelian_group M"
    6.10      and smult_closed:
    6.11 -      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
    6.12 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
    6.13      and smult_l_distr:
    6.14        "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    6.15 -      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
    6.16 +      (a \<oplus> b) \<odot>\<^sub>2 x = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (b \<odot>\<^sub>2 x)"
    6.17      and smult_r_distr:
    6.18        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    6.19 -      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
    6.20 +      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (a \<odot>\<^sub>2 y)"
    6.21      and smult_assoc1:
    6.22        "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    6.23 -      smult M (mult R a b) x = smult M a (smult M b x)"
    6.24 +      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
    6.25      and smult_one:
    6.26 -      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
    6.27 +      "!!x. x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
    6.28    shows "module R M"
    6.29    by (auto intro: module.intro cring.axioms abelian_group.axioms
    6.30      module_axioms.intro prems)
    6.31  
    6.32  lemma algebraI:
    6.33 +  includes struct R + struct M
    6.34    assumes R_cring: "cring R"
    6.35      and M_cring: "cring M"
    6.36      and smult_closed:
    6.37 -      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
    6.38 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
    6.39      and smult_l_distr:
    6.40        "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    6.41 -      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
    6.42 +      (a \<oplus> b) \<odot>\<^sub>2 x = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (b \<odot>\<^sub>2 x)"
    6.43      and smult_r_distr:
    6.44        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    6.45 -      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
    6.46 +      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (a \<odot>\<^sub>2 y)"
    6.47      and smult_assoc1:
    6.48        "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    6.49 -      smult M (mult R a b) x = smult M a (smult M b x)"
    6.50 +      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
    6.51      and smult_one:
    6.52 -      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
    6.53 +      "!!x. x \<in> carrier M ==> (one R) \<odot>\<^sub>2 x = x"
    6.54      and smult_assoc2:
    6.55        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    6.56 -      mult M (smult M a x) y = smult M a (mult M x y)"
    6.57 +      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
    6.58    shows "algebra R M"
    6.59    by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
    6.60      module_axioms.intro prems)
    6.61  
    6.62  lemma (in algebra) R_cring:
    6.63    "cring R"
    6.64 -  by (rule cring.intro) assumption+
    6.65 +  by (rule cring.intro)
    6.66  
    6.67  lemma (in algebra) M_cring:
    6.68    "cring M"
    6.69 -  by (rule cring.intro) assumption+
    6.70 +  by (rule cring.intro)
    6.71  
    6.72  lemma (in algebra) module:
    6.73    "module R M"
    6.74    by (auto intro: moduleI R_cring is_abelian_group
    6.75      smult_l_distr smult_r_distr smult_assoc1)
    6.76  
    6.77 +
    6.78  subsection {* Basic Properties of Algebras *}
    6.79  
    6.80  lemma (in algebra) smult_l_null [simp]:
     7.1 --- a/src/HOL/Algebra/Sylow.thy	Thu Apr 22 11:00:22 2004 +0200
     7.2 +++ b/src/HOL/Algebra/Sylow.thy	Thu Apr 22 11:01:34 2004 +0200
     7.3 @@ -15,8 +15,8 @@
     7.4  subsection {*Order of a Group and Lagrange's Theorem*}
     7.5  
     7.6  constdefs
     7.7 -  order     :: "(('a,'b) semigroup_scheme) => nat"
     7.8 -   "order(S) == card(carrier S)"
     7.9 +  order     :: "('a,'b) semigroup_scheme => nat"
    7.10 +  "order S == card (carrier S)"
    7.11  
    7.12  theorem (in coset) lagrange:
    7.13       "[| finite(carrier G); subgroup H G |] 
     8.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Apr 22 11:00:22 2004 +0200
     8.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Apr 22 11:01:34 2004 +0200
     8.3 @@ -58,18 +58,18 @@
     8.4    monom :: "['a, nat] => 'p"
     8.5    coeff :: "['p, nat] => 'a"
     8.6  
     8.7 -constdefs
     8.8 -  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
     8.9 -  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound (zero R) n f)}"
    8.10 -  UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
    8.11 +constdefs (structure R)
    8.12 +  up :: "_ => (nat => 'a) set"
    8.13 +  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero> n f)}"
    8.14 +  UP :: "_ => ('a, nat => 'a) up_ring"
    8.15    "UP R == (|
    8.16      carrier = up R,
    8.17 -    mult = (%p:up R. %q:up R. %n. finsum R (%i. mult R (p i) (q (n-i))) {..n}),
    8.18 -    one = (%i. if i=0 then one R else zero R),
    8.19 -    zero = (%i. zero R),
    8.20 -    add = (%p:up R. %q:up R. %i. add R (p i) (q i)),
    8.21 -    smult = (%a:carrier R. %p:up R. %i. mult R a (p i)),
    8.22 -    monom = (%a:carrier R. %n i. if i=n then a else zero R),
    8.23 +    mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)),
    8.24 +    one = (%i. if i=0 then \<one> else \<zero>),
    8.25 +    zero = (%i. \<zero>),
    8.26 +    add = (%p:up R. %q:up R. %i. p i \<oplus> q i),
    8.27 +    smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i),
    8.28 +    monom = (%a:carrier R. %n i. if i=n then a else \<zero>),
    8.29      coeff = (%p:up R. %n. p n) |)"
    8.30  
    8.31  text {*
    8.32 @@ -179,9 +179,8 @@
    8.33  locale UP_domain = UP_cring + "domain" R
    8.34  
    8.35  text {*
    8.36 -  Temporarily declare UP.P\_def as simp rule.
    8.37 -*}
    8.38 -(* TODO: use antiquotation once text (in locale) is supported. *)
    8.39 +  Temporarily declare @{text UP.P_def} as simp rule.
    8.40 +*}  (* TODO: use antiquotation once text (in locale) is supported. *)
    8.41  
    8.42  declare (in UP) P_def [simp]
    8.43  
    8.44 @@ -785,9 +784,9 @@
    8.45  
    8.46  subsection {* The degree function *}
    8.47  
    8.48 -constdefs
    8.49 -  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
    8.50 -  "deg R p == LEAST n. bound (zero R) n (coeff (UP R) p)"
    8.51 +constdefs (structure R)
    8.52 +  deg :: "[_, nat => 'a] => nat"
    8.53 +  "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
    8.54  
    8.55  lemma (in UP_cring) deg_aboveI:
    8.56    "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n" 
    8.57 @@ -1248,11 +1247,10 @@
    8.58    "(%a. monom P a 0) \<in> ring_hom R P"
    8.59    by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
    8.60  
    8.61 -constdefs
    8.62 -  eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
    8.63 -          'a => 'b, 'b, nat => 'a] => 'b"
    8.64 -  "eval R S phi s == (\<lambda>p \<in> carrier (UP R).
    8.65 -    finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p})"
    8.66 +constdefs (structure S)
    8.67 +  eval :: "[_, _, 'a => 'b, 'b, nat => 'a] => 'b"
    8.68 +  "eval R S phi s == \<lambda>p \<in> carrier (UP R).
    8.69 +    \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> pow S s i"
    8.70  (*
    8.71    "eval R S phi s p == if p \<in> carrier (UP R)
    8.72    then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
    8.73 @@ -1566,5 +1564,4 @@
    8.74  
    8.75  -- {* Calculates @{term "x = 500"} *}
    8.76  
    8.77 -
    8.78  end