slightly more uniform definitions -- eliminated old-style meta-equality;
authorwenzelm
Sun Mar 21 16:51:37 2010 +0100 (2010-03-21)
changeset 358485443079512ea
parent 35847 19f1f7066917
child 35849 b5522b51cb1e
slightly more uniform definitions -- eliminated old-style meta-equality;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/UnivPoly2.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 15:57:40 2010 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 16:51:37 2010 +0100
     1.3 @@ -19,37 +19,39 @@
     1.4  
     1.5  definition
     1.6    a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
     1.7 -  where "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
     1.8 +  where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
     1.9  
    1.10  definition
    1.11    a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
    1.12 -  where "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.13 +  where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.14  
    1.15  definition
    1.16    A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _" [81] 80)
    1.17 -  where "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.18 +  where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.19  
    1.20  definition
    1.21    set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
    1.22 -  where "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.23 +  where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.24  
    1.25  definition
    1.26    A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _" [81] 80)
    1.27 -  where "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.28 +  where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.29  
    1.30  definition
    1.31    a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
    1.32 -  where "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.33 +  where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.34  
    1.35 -definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) where
    1.36 +definition
    1.37 +  A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
    1.38      --{*Actually defined for groups rather than monoids*}
    1.39 -  "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.40 +  where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.41  
    1.42 -definition a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> 
    1.43 -             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where 
    1.44 +definition
    1.45 +  a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
    1.46      --{*the kernel of a homomorphism (additive)*}
    1.47 -  "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
    1.48 -                              \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
    1.49 +  where "a_kernel G H h =
    1.50 +    kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
    1.51 +      \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
    1.52  
    1.53  locale abelian_group_hom = G: abelian_group G + H: abelian_group H
    1.54      for G (structure) and H (structure) +
    1.55 @@ -527,7 +529,7 @@
    1.56    a_kernel_def kernel_def
    1.57  
    1.58  lemma a_kernel_def':
    1.59 -  "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
    1.60 +  "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
    1.61  by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
    1.62  
    1.63  
     2.1 --- a/src/HOL/Algebra/Bij.thy	Sun Mar 21 15:57:40 2010 +0100
     2.2 +++ b/src/HOL/Algebra/Bij.thy	Sun Mar 21 16:51:37 2010 +0100
     2.3 @@ -7,12 +7,14 @@
     2.4  
     2.5  section {* Bijections of a Set, Permutation and Automorphism Groups *}
     2.6  
     2.7 -definition Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" where
     2.8 +definition
     2.9 +  Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
    2.10      --{*Only extensional functions, since otherwise we get too many.*}
    2.11 -  "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
    2.12 +   where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
    2.13  
    2.14 -definition BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
    2.15 -  "BijGroup S \<equiv>
    2.16 +definition
    2.17 +  BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
    2.18 +  where "BijGroup S =
    2.19      \<lparr>carrier = Bij S,
    2.20       mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
    2.21       one = \<lambda>x \<in> S. x\<rparr>"
    2.22 @@ -69,11 +71,13 @@
    2.23  done
    2.24  
    2.25  
    2.26 -definition auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set" where
    2.27 -  "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
    2.28 +definition
    2.29 +  auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
    2.30 +  where "auto G = hom G G \<inter> Bij (carrier G)"
    2.31  
    2.32 -definition AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
    2.33 -  "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
    2.34 +definition
    2.35 +  AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
    2.36 +  where "AutoGroup G = BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
    2.37  
    2.38  lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
    2.39    by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
     3.1 --- a/src/HOL/Algebra/Congruence.thy	Sun Mar 21 15:57:40 2010 +0100
     3.2 +++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 21 16:51:37 2010 +0100
     3.3 @@ -21,23 +21,23 @@
     3.4  
     3.5  definition
     3.6    elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
     3.7 -  where "x .\<in>\<^bsub>S\<^esub> A \<equiv> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
     3.8 +  where "x .\<in>\<^bsub>S\<^esub> A \<longleftrightarrow> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
     3.9  
    3.10  definition
    3.11    set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
    3.12 -  where "A {.=}\<^bsub>S\<^esub> B == ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
    3.13 +  where "A {.=}\<^bsub>S\<^esub> B \<longleftrightarrow> ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
    3.14  
    3.15  definition
    3.16    eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
    3.17 -  where "class_of\<^bsub>S\<^esub> x == {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
    3.18 +  where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
    3.19  
    3.20  definition
    3.21    eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
    3.22 -  where "closure_of\<^bsub>S\<^esub> A == {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
    3.23 +  where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
    3.24  
    3.25  definition
    3.26    eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
    3.27 -  where "is_closed\<^bsub>S\<^esub> A == (A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A)"
    3.28 +  where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
    3.29  
    3.30  abbreviation
    3.31    not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
     4.1 --- a/src/HOL/Algebra/Coset.thy	Sun Mar 21 15:57:40 2010 +0100
     4.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Mar 21 16:51:37 2010 +0100
     4.3 @@ -10,23 +10,23 @@
     4.4  
     4.5  definition
     4.6    r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
     4.7 -  where "H #>\<^bsub>G\<^esub> a \<equiv> \<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a}"
     4.8 +  where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
     4.9  
    4.10  definition
    4.11    l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
    4.12 -  where "a <#\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h}"
    4.13 +  where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
    4.14  
    4.15  definition
    4.16    RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
    4.17 -  where "rcosets\<^bsub>G\<^esub> H \<equiv> \<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a}"
    4.18 +  where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
    4.19  
    4.20  definition
    4.21    set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
    4.22 -  where "H <#>\<^bsub>G\<^esub> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k}"
    4.23 +  where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
    4.24  
    4.25  definition
    4.26    SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
    4.27 -  where "set_inv\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
    4.28 +  where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
    4.29  
    4.30  
    4.31  locale normal = subgroup + group +
    4.32 @@ -595,7 +595,7 @@
    4.33  
    4.34  definition
    4.35    r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
    4.36 -  where "rcong\<^bsub>G\<^esub> H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
    4.37 +  where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
    4.38  
    4.39  
    4.40  lemma (in subgroup) equiv_rcong:
    4.41 @@ -754,8 +754,9 @@
    4.42  
    4.43  subsection {*Order of a Group and Lagrange's Theorem*}
    4.44  
    4.45 -definition order :: "('a, 'b) monoid_scheme \<Rightarrow> nat" where
    4.46 -  "order S \<equiv> card (carrier S)"
    4.47 +definition
    4.48 +  order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
    4.49 +  where "order S = card (carrier S)"
    4.50  
    4.51  lemma (in group) rcosets_part_G:
    4.52    assumes "subgroup H G"
    4.53 @@ -824,10 +825,10 @@
    4.54  
    4.55  subsection {*Quotient Groups: Factorization of a Group*}
    4.56  
    4.57 -definition FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65) where
    4.58 +definition
    4.59 +  FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
    4.60      --{*Actually defined for groups rather than monoids*}
    4.61 -  "FactGroup G H \<equiv>
    4.62 -    \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
    4.63 +   where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
    4.64  
    4.65  lemma (in normal) setmult_closed:
    4.66       "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
    4.67 @@ -890,10 +891,10 @@
    4.68  text{*The quotient by the kernel of a homomorphism is isomorphic to the 
    4.69    range of that homomorphism.*}
    4.70  
    4.71 -definition kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> 
    4.72 -             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where 
    4.73 +definition
    4.74 +  kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
    4.75      --{*the kernel of a homomorphism*}
    4.76 -  "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
    4.77 +  where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
    4.78  
    4.79  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
    4.80  apply (rule subgroup.intro) 
     5.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 15:57:40 2010 +0100
     5.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 16:51:37 2010 +0100
     5.3 @@ -162,26 +162,26 @@
     5.4  
     5.5  definition
     5.6    factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
     5.7 -  where "a divides\<^bsub>G\<^esub> b == \<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c"
     5.8 +  where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)"
     5.9  
    5.10  definition
    5.11    associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
    5.12 -  where "a \<sim>\<^bsub>G\<^esub> b == a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
    5.13 +  where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
    5.14  
    5.15  abbreviation
    5.16    "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
    5.17  
    5.18  definition
    5.19    properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
    5.20 -  where "properfactor G a b == a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
    5.21 +  where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
    5.22  
    5.23  definition
    5.24    irreducible :: "[_, 'a] \<Rightarrow> bool"
    5.25 -  where "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
    5.26 +  where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
    5.27  
    5.28  definition
    5.29    prime :: "[_, 'a] \<Rightarrow> bool" where
    5.30 -  "prime G p ==
    5.31 +  "prime G p \<longleftrightarrow>
    5.32      p \<notin> Units G \<and> 
    5.33      (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"
    5.34  
    5.35 @@ -1043,11 +1043,11 @@
    5.36  
    5.37  definition
    5.38    factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
    5.39 -  where "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
    5.40 +  where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
    5.41  
    5.42  definition
    5.43    wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
    5.44 -  where "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
    5.45 +  where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
    5.46  
    5.47  abbreviation
    5.48    list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
    5.49 @@ -1055,7 +1055,7 @@
    5.50  
    5.51  definition
    5.52    essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
    5.53 -  where "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
    5.54 +  where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
    5.55  
    5.56  
    5.57  locale factorial_monoid = comm_monoid_cancel +
    5.58 @@ -1903,7 +1903,7 @@
    5.59    "assocs G x == eq_closure_of (division_rel G) {x}"
    5.60  
    5.61  definition
    5.62 -  "fmset G as \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
    5.63 +  "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"
    5.64  
    5.65  
    5.66  text {* Helper lemmas *}
    5.67 @@ -2618,24 +2618,24 @@
    5.68  
    5.69  definition
    5.70    isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
    5.71 -  where "x gcdof\<^bsub>G\<^esub> a b \<equiv> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and> 
    5.72 +  where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
    5.73      (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"
    5.74  
    5.75  definition
    5.76    islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
    5.77 -  where "x lcmof\<^bsub>G\<^esub> a b \<equiv> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and> 
    5.78 +  where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
    5.79      (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"
    5.80  
    5.81  definition
    5.82    somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    5.83 -  where "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b"
    5.84 +  where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"
    5.85  
    5.86  definition
    5.87    somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    5.88 -  where "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b"
    5.89 +  where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"
    5.90  
    5.91  definition
    5.92 -  "SomeGcd G A == inf (division_rel G) A"
    5.93 +  "SomeGcd G A = inf (division_rel G) A"
    5.94  
    5.95  
    5.96  locale gcd_condition_monoid = comm_monoid_cancel +
    5.97 @@ -3633,9 +3633,10 @@
    5.98  
    5.99  text {* Number of factors for wellfoundedness *}
   5.100  
   5.101 -definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
   5.102 -  "factorcount G a == THE c. (ALL as. set as \<subseteq> carrier G \<and> 
   5.103 -                                      wfactors G as a \<longrightarrow> c = length as)"
   5.104 +definition
   5.105 +  factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
   5.106 +  "factorcount G a =
   5.107 +    (THE c. (ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as))"
   5.108  
   5.109  lemma (in monoid) ee_length:
   5.110    assumes ee: "essentially_equal G as bs"
     6.1 --- a/src/HOL/Algebra/Exponent.thy	Sun Mar 21 15:57:40 2010 +0100
     6.2 +++ b/src/HOL/Algebra/Exponent.thy	Sun Mar 21 16:51:37 2010 +0100
     6.3 @@ -12,8 +12,9 @@
     6.4  
     6.5  subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
     6.6  
     6.7 -definition exponent :: "nat => nat => nat" where
     6.8 -"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
     6.9 +definition
    6.10 +  exponent :: "nat => nat => nat"
    6.11 +  where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
    6.12  
    6.13  
    6.14  text{*Prime Theorems*}
     7.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 15:57:40 2010 +0100
     7.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 16:51:37 2010 +0100
     7.3 @@ -26,8 +26,9 @@
     7.4  
     7.5  inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
     7.6  
     7.7 -definition foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" where
     7.8 -  "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
     7.9 +definition
    7.10 +  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
    7.11 +  where "foldD D f e A = (THE x. (A, x) \<in> foldSetD D f e)"
    7.12  
    7.13  lemma foldSetD_closed:
    7.14    "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
    7.15 @@ -286,11 +287,11 @@
    7.16  subsubsection {* Products over Finite Sets *}
    7.17  
    7.18  definition
    7.19 -  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" where
    7.20 -  "finprod G f A ==
    7.21 -    if finite A
    7.22 +  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
    7.23 +  where "finprod G f A =
    7.24 +   (if finite A
    7.25      then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
    7.26 -    else undefined"
    7.27 +    else undefined)"
    7.28  
    7.29  syntax
    7.30    "_finprod" :: "index => idt => 'a set => 'b => 'b"
     8.1 --- a/src/HOL/Algebra/Group.thy	Sun Mar 21 15:57:40 2010 +0100
     8.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 16:51:37 2010 +0100
     8.3 @@ -24,12 +24,12 @@
     8.4  
     8.5  definition
     8.6    m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
     8.7 -  where "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier G & x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
     8.8 +  where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G & x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
     8.9  
    8.10  definition
    8.11    Units :: "_ => 'a set"
    8.12    --{*The set of invertible elements*}
    8.13 -  where "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
    8.14 +  where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
    8.15  
    8.16  consts
    8.17    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    8.18 @@ -479,10 +479,12 @@
    8.19  
    8.20  subsection {* Direct Products *}
    8.21  
    8.22 -definition DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
    8.23 -  "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
    8.24 -                mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
    8.25 -                one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
    8.26 +definition
    8.27 +  DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
    8.28 +  "G \<times>\<times> H =
    8.29 +    \<lparr>carrier = carrier G \<times> carrier H,
    8.30 +     mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
    8.31 +     one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
    8.32  
    8.33  lemma DirProd_monoid:
    8.34    assumes "monoid G" and "monoid H"
    8.35 @@ -537,7 +539,7 @@
    8.36  
    8.37  definition
    8.38    hom :: "_ => _ => ('a => 'b) set" where
    8.39 -  "hom G H ==
    8.40 +  "hom G H =
    8.41      {h. h \<in> carrier G -> carrier H &
    8.42        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
    8.43  
    8.44 @@ -545,8 +547,9 @@
    8.45    "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
    8.46  by (fastsimp simp add: hom_def compose_def)
    8.47  
    8.48 -definition iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) where
    8.49 -  "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    8.50 +definition
    8.51 +  iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
    8.52 +  where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    8.53  
    8.54  lemma iso_refl: "(%x. x) \<in> G \<cong> G"
    8.55  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
     9.1 --- a/src/HOL/Algebra/Ideal.thy	Sun Mar 21 15:57:40 2010 +0100
     9.2 +++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 21 16:51:37 2010 +0100
     9.3 @@ -49,7 +49,7 @@
     9.4  
     9.5  definition
     9.6    genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
     9.7 -  where "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
     9.8 +  where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
     9.9  
    9.10  
    9.11  subsubsection {* Principal Ideals *}
    9.12 @@ -453,7 +453,7 @@
    9.13  
    9.14  definition
    9.15    cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
    9.16 -  where "cgenideal R a \<equiv> {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
    9.17 +  where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
    9.18  
    9.19  text {* genhideal (?) really generates an ideal *}
    9.20  lemma (in cring) cgenideal_ideal:
    10.1 --- a/src/HOL/Algebra/IntRing.thy	Sun Mar 21 15:57:40 2010 +0100
    10.2 +++ b/src/HOL/Algebra/IntRing.thy	Sun Mar 21 16:51:37 2010 +0100
    10.3 @@ -22,8 +22,9 @@
    10.4  
    10.5  subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
    10.6  
    10.7 -definition int_ring :: "int ring" ("\<Z>") where
    10.8 -  "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
    10.9 +definition
   10.10 +  int_ring :: "int ring" ("\<Z>") where
   10.11 +  "int_ring = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
   10.12  
   10.13  lemma int_Zcarr [intro!, simp]:
   10.14    "k \<in> carrier \<Z>"
   10.15 @@ -323,8 +324,9 @@
   10.16  
   10.17  subsection {* Ideals and the Modulus *}
   10.18  
   10.19 -definition ZMod :: "int => int => int set" where
   10.20 -  "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
   10.21 +definition
   10.22 +  ZMod :: "int => int => int set"
   10.23 +  where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
   10.24  
   10.25  lemmas ZMod_defs =
   10.26    ZMod_def genideal_def
   10.27 @@ -405,8 +407,9 @@
   10.28  
   10.29  subsection {* Factorization *}
   10.30  
   10.31 -definition ZFact :: "int \<Rightarrow> int set ring" where
   10.32 -  "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
   10.33 +definition
   10.34 +  ZFact :: "int \<Rightarrow> int set ring"
   10.35 +  where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
   10.36  
   10.37  lemmas ZFact_defs = ZFact_def FactRing_def
   10.38  
    11.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Mar 21 15:57:40 2010 +0100
    11.2 +++ b/src/HOL/Algebra/Lattice.thy	Sun Mar 21 16:51:37 2010 +0100
    11.3 @@ -27,7 +27,7 @@
    11.4  
    11.5  definition
    11.6    lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    11.7 -  where "x \<sqsubset>\<^bsub>L\<^esub> y == x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
    11.8 +  where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
    11.9  
   11.10  
   11.11  subsubsection {* The order relation *}
   11.12 @@ -104,11 +104,11 @@
   11.13  
   11.14  definition
   11.15    Upper :: "[_, 'a set] => 'a set"
   11.16 -  where "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
   11.17 +  where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
   11.18  
   11.19  definition
   11.20    Lower :: "[_, 'a set] => 'a set"
   11.21 -  where "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
   11.22 +  where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
   11.23  
   11.24  lemma Upper_closed [intro!, simp]:
   11.25    "Upper L A \<subseteq> carrier L"
   11.26 @@ -278,11 +278,11 @@
   11.27  
   11.28  definition
   11.29    least :: "[_, 'a, 'a set] => bool"
   11.30 -  where "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
   11.31 +  where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
   11.32  
   11.33  definition
   11.34    greatest :: "[_, 'a, 'a set] => bool"
   11.35 -  where "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
   11.36 +  where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
   11.37  
   11.38  text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
   11.39    .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
   11.40 @@ -404,19 +404,19 @@
   11.41  
   11.42  definition
   11.43    sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   11.44 -  where "\<Squnion>\<^bsub>L\<^esub>A == SOME x. least L x (Upper L A)"
   11.45 +  where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
   11.46  
   11.47  definition
   11.48    inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   11.49 -  where "\<Sqinter>\<^bsub>L\<^esub>A == SOME x. greatest L x (Lower L A)"
   11.50 +  where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
   11.51  
   11.52  definition
   11.53    join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   11.54 -  where "x \<squnion>\<^bsub>L\<^esub> y == \<Squnion>\<^bsub>L\<^esub>{x, y}"
   11.55 +  where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
   11.56  
   11.57  definition
   11.58    meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   11.59 -  where "x \<sqinter>\<^bsub>L\<^esub> y == \<Sqinter>\<^bsub>L\<^esub>{x, y}"
   11.60 +  where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
   11.61  
   11.62  
   11.63  subsection {* Lattices *}
   11.64 @@ -988,11 +988,11 @@
   11.65  
   11.66  definition
   11.67    top :: "_ => 'a" ("\<top>\<index>")
   11.68 -  where "\<top>\<^bsub>L\<^esub> == sup L (carrier L)"
   11.69 +  where "\<top>\<^bsub>L\<^esub> = sup L (carrier L)"
   11.70  
   11.71  definition
   11.72    bottom :: "_ => 'a" ("\<bottom>\<index>")
   11.73 -  where "\<bottom>\<^bsub>L\<^esub> == inf L (carrier L)"
   11.74 +  where "\<bottom>\<^bsub>L\<^esub> = inf L (carrier L)"
   11.75  
   11.76  
   11.77  lemma (in weak_complete_lattice) supI:
    12.1 --- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 15:57:40 2010 +0100
    12.2 +++ b/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 16:51:37 2010 +0100
    12.3 @@ -14,7 +14,7 @@
    12.4  definition
    12.5    rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
    12.6      ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
    12.7 -  where "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b)"
    12.8 +  where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
    12.9  
   12.10  
   12.11  text {* @{const "rcoset_mult"} fulfils the properties required by
   12.12 @@ -91,7 +91,7 @@
   12.13  
   12.14  definition
   12.15    FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"  (infixl "Quot" 65)
   12.16 -  where "FactRing R I \<equiv>
   12.17 +  where "FactRing R I =
   12.18      \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
   12.19  
   12.20  
    13.1 --- a/src/HOL/Algebra/Ring.thy	Sun Mar 21 15:57:40 2010 +0100
    13.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Mar 21 16:51:37 2010 +0100
    13.3 @@ -22,11 +22,11 @@
    13.4  
    13.5  definition
    13.6    a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
    13.7 -  where "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
    13.8 +  where "a_inv R = m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
    13.9  
   13.10  definition
   13.11    a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
   13.12 -  where "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus>\<^bsub>R\<^esub> y == x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
   13.13 +  where "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
   13.14  
   13.15  locale abelian_monoid =
   13.16    fixes G (structure)
   13.17 @@ -200,9 +200,9 @@
   13.18    This definition makes it easy to lift lemmas from @{term finprod}.
   13.19  *}
   13.20  
   13.21 -definition finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
   13.22 -  "finsum G f A == finprod (| carrier = carrier G,
   13.23 -     mult = add G, one = zero G |) f A"
   13.24 +definition
   13.25 +  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
   13.26 +  "finsum G f A = finprod (| carrier = carrier G, mult = add G, one = zero G |) f A"
   13.27  
   13.28  syntax
   13.29    "_finsum" :: "index => idt => 'a set => 'b => 'b"
   13.30 @@ -732,7 +732,7 @@
   13.31  
   13.32  definition
   13.33    ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
   13.34 -  where "ring_hom R S ==
   13.35 +  where "ring_hom R S =
   13.36      {h. h \<in> carrier R -> carrier S &
   13.37        (ALL x y. x \<in> carrier R & y \<in> carrier R -->
   13.38          h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
    14.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 15:57:40 2010 +0100
    14.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 16:51:37 2010 +0100
    14.3 @@ -54,11 +54,12 @@
    14.4    monom :: "['a, nat] => 'p"
    14.5    coeff :: "['p, nat] => 'a"
    14.6  
    14.7 -definition up :: "('a, 'm) ring_scheme => (nat => 'a) set"
    14.8 -  where up_def: "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
    14.9 +definition
   14.10 +  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
   14.11 +  where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
   14.12  
   14.13  definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
   14.14 -  where UP_def: "UP R == (|
   14.15 +  where "UP R = (|
   14.16     carrier = up R,
   14.17     mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
   14.18     one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
   14.19 @@ -711,8 +712,9 @@
   14.20  
   14.21  subsection {* The Degree Function *}
   14.22  
   14.23 -definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
   14.24 -  where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)"
   14.25 +definition
   14.26 +  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
   14.27 +  where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
   14.28  
   14.29  context UP_ring
   14.30  begin
   14.31 @@ -1173,8 +1175,8 @@
   14.32  definition
   14.33    eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
   14.34             'a => 'b, 'b, nat => 'a] => 'b"
   14.35 -  where "eval R S phi s == \<lambda>p \<in> carrier (UP R).
   14.36 -    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i"
   14.37 +  where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
   14.38 +    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
   14.39  
   14.40  context UP
   14.41  begin
   14.42 @@ -1854,11 +1856,11 @@
   14.43    by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
   14.44      ring_hom_cring_axioms.intro UP_cring.intro)
   14.45  
   14.46 -definition  INTEG :: "int ring"
   14.47 -  where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
   14.48 +definition
   14.49 +  INTEG :: "int ring"
   14.50 +  where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
   14.51  
   14.52 -lemma INTEG_cring:
   14.53 -  "cring INTEG"
   14.54 +lemma INTEG_cring: "cring INTEG"
   14.55    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
   14.56      zadd_zminus_inverse2 zadd_zmult_distrib)
   14.57  
    15.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sun Mar 21 15:57:40 2010 +0100
    15.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Sun Mar 21 16:51:37 2010 +0100
    15.3 @@ -30,16 +30,17 @@
    15.4    and divide_def:       "a / b = a * inverse b"
    15.5  begin
    15.6  
    15.7 -definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where
    15.8 -  assoc_def: "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
    15.9 +definition
   15.10 +  assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50)
   15.11 +  where "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
   15.12  
   15.13 -definition irred :: "'a \<Rightarrow> bool" where
   15.14 -  irred_def: "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1
   15.15 -                          & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
   15.16 +definition
   15.17 +  irred :: "'a \<Rightarrow> bool" where
   15.18 +  "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
   15.19  
   15.20 -definition prime :: "'a \<Rightarrow> bool" where
   15.21 -  prime_def: "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1
   15.22 -                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
   15.23 +definition
   15.24 +  prime :: "'a \<Rightarrow> bool" where
   15.25 +  "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
   15.26  
   15.27  end
   15.28  
    16.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 15:57:40 2010 +0100
    16.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 16:51:37 2010 +0100
    16.3 @@ -47,16 +47,16 @@
    16.4  section {* Constants *}
    16.5  
    16.6  definition
    16.7 -  coeff :: "['a up, nat] => ('a::zero)" where
    16.8 -  "coeff p n = Rep_UP p n"
    16.9 +  coeff :: "['a up, nat] => ('a::zero)"
   16.10 +  where "coeff p n = Rep_UP p n"
   16.11  
   16.12  definition
   16.13 -  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70) where
   16.14 -  "monom a n = Abs_UP (%i. if i=n then a else 0)"
   16.15 +  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70)
   16.16 +  where "monom a n = Abs_UP (%i. if i=n then a else 0)"
   16.17  
   16.18  definition
   16.19 -  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70) where
   16.20 -  "a *s p = Abs_UP (%i. a * Rep_UP p i)"
   16.21 +  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70)
   16.22 +  where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
   16.23  
   16.24  lemma coeff_bound_ex: "EX n. bound n (coeff p)"
   16.25  proof -
   16.26 @@ -132,7 +132,7 @@
   16.27  begin
   16.28  
   16.29  definition
   16.30 -  up_mult_def:  "p * q = Abs_UP (%n::nat. setsum
   16.31 +  up_mult_def: "p * q = Abs_UP (%n::nat. setsum
   16.32                       (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
   16.33  
   16.34  instance ..
   16.35 @@ -149,7 +149,7 @@
   16.36                       THE x. a * x = 1 else 0)"
   16.37  
   16.38  definition
   16.39 -  up_divide_def:  "(a :: 'a up) / b = a * inverse b"
   16.40 +  up_divide_def: "(a :: 'a up) / b = a * inverse b"
   16.41  
   16.42  instance ..
   16.43  
   16.44 @@ -482,8 +482,8 @@
   16.45  section {* The degree function *}
   16.46  
   16.47  definition
   16.48 -  deg :: "('a::zero) up => nat" where
   16.49 -  "deg p = (LEAST n. bound n (coeff p))"
   16.50 +  deg :: "('a::zero) up => nat"
   16.51 +  where "deg p = (LEAST n. bound n (coeff p))"
   16.52  
   16.53  lemma deg_aboveI:
   16.54    "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"