eliminated old constdefs;
authorwenzelm
Sun Mar 21 15:57:40 2010 +0100 (2010-03-21)
changeset 3584719f1f7066917
parent 35846 2ae4b7585501
child 35848 5443079512ea
eliminated old constdefs;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/Ring.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 06:59:23 2010 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 15:57:40 2010 +0100
     1.3 @@ -17,26 +17,29 @@
     1.4  
     1.5  no_notation Plus (infixr "<+>" 65)
     1.6  
     1.7 -constdefs (structure G)
     1.8 +definition
     1.9    a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
    1.10 -  "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.11 +  where "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.12  
    1.13 +definition
    1.14    a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
    1.15 -  "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.16 +  where "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.17  
    1.18 +definition
    1.19    A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _" [81] 80)
    1.20 -  "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.21 +  where "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.22  
    1.23 +definition
    1.24    set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
    1.25 -  "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.26 +  where "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.27  
    1.28 +definition
    1.29    A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _" [81] 80)
    1.30 -  "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.31 +  where "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.32  
    1.33 -constdefs (structure G)
    1.34 -  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"
    1.35 -                  ("racong\<index> _")
    1.36 -   "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.37 +definition
    1.38 +  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
    1.39 +  where "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.40  
    1.41  definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) where
    1.42      --{*Actually defined for groups rather than monoids*}
     2.1 --- a/src/HOL/Algebra/Congruence.thy	Sun Mar 21 06:59:23 2010 +0100
     2.2 +++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 21 15:57:40 2010 +0100
     2.3 @@ -19,21 +19,25 @@
     2.4  record 'a eq_object = "'a partial_object" +
     2.5    eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
     2.6  
     2.7 -constdefs (structure S)
     2.8 +definition
     2.9    elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
    2.10 -  "x .\<in> A \<equiv> (\<exists>y \<in> A. x .= y)"
    2.11 +  where "x .\<in>\<^bsub>S\<^esub> A \<equiv> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
    2.12  
    2.13 +definition
    2.14    set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
    2.15 -  "A {.=} B == ((\<forall>x \<in> A. x .\<in> B) \<and> (\<forall>x \<in> B. x .\<in> A))"
    2.16 +  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))"
    2.17  
    2.18 +definition
    2.19    eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
    2.20 -  "class_of x == {y \<in> carrier S. x .= y}"
    2.21 +  where "class_of\<^bsub>S\<^esub> x == {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
    2.22  
    2.23 +definition
    2.24    eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
    2.25 -  "closure_of A == {y \<in> carrier S. y .\<in> A}"
    2.26 +  where "closure_of\<^bsub>S\<^esub> A == {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
    2.27  
    2.28 +definition
    2.29    eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
    2.30 -  "is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
    2.31 +  where "is_closed\<^bsub>S\<^esub> A == (A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A)"
    2.32  
    2.33  abbreviation
    2.34    not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
     3.1 --- a/src/HOL/Algebra/Coset.thy	Sun Mar 21 06:59:23 2010 +0100
     3.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Mar 21 15:57:40 2010 +0100
     3.3 @@ -8,21 +8,25 @@
     3.4  
     3.5  section {*Cosets and Quotient Groups*}
     3.6  
     3.7 -constdefs (structure G)
     3.8 +definition
     3.9    r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
    3.10 -  "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
    3.11 +  where "H #>\<^bsub>G\<^esub> a \<equiv> \<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a}"
    3.12  
    3.13 +definition
    3.14    l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
    3.15 -  "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
    3.16 +  where "a <#\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h}"
    3.17  
    3.18 +definition
    3.19    RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
    3.20 -  "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
    3.21 +  where "rcosets\<^bsub>G\<^esub> H \<equiv> \<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a}"
    3.22  
    3.23 +definition
    3.24    set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
    3.25 -  "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
    3.26 +  where "H <#>\<^bsub>G\<^esub> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k}"
    3.27  
    3.28 +definition
    3.29    SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
    3.30 -  "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
    3.31 +  where "set_inv\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
    3.32  
    3.33  
    3.34  locale normal = subgroup + group +
    3.35 @@ -589,10 +593,9 @@
    3.36  
    3.37  subsubsection{*An Equivalence Relation*}
    3.38  
    3.39 -constdefs (structure G)
    3.40 -  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
    3.41 -                  ("rcong\<index> _")
    3.42 -   "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
    3.43 +definition
    3.44 +  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
    3.45 +  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}"
    3.46  
    3.47  
    3.48  lemma (in subgroup) equiv_rcong:
     4.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 06:59:23 2010 +0100
     4.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 15:57:40 2010 +0100
     4.3 @@ -160,30 +160,30 @@
     4.4  
     4.5  subsubsection {* Function definitions *}
     4.6  
     4.7 -constdefs (structure G)
     4.8 +definition
     4.9    factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
    4.10 -  "a divides b == \<exists>c\<in>carrier G. b = a \<otimes> c"
    4.11 -
    4.12 -constdefs (structure G)
    4.13 +  where "a divides\<^bsub>G\<^esub> b == \<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c"
    4.14 +
    4.15 +definition
    4.16    associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
    4.17 -  "a \<sim> b == a divides b \<and> b divides a"
    4.18 +  where "a \<sim>\<^bsub>G\<^esub> b == a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
    4.19  
    4.20  abbreviation
    4.21    "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
    4.22  
    4.23 -constdefs (structure G)
    4.24 +definition
    4.25    properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
    4.26 -  "properfactor G a b == a divides b \<and> \<not>(b divides a)"
    4.27 -
    4.28 -constdefs (structure G)
    4.29 +  where "properfactor G a b == a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
    4.30 +
    4.31 +definition
    4.32    irreducible :: "[_, 'a] \<Rightarrow> bool"
    4.33 -  "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
    4.34 -
    4.35 -constdefs (structure G)
    4.36 -  prime :: "[_, 'a] \<Rightarrow> bool"
    4.37 -  "prime G p == p \<notin> Units G \<and> 
    4.38 -                (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides (a \<otimes> b) \<longrightarrow> p divides a \<or> p divides b)"
    4.39 -
    4.40 +  where "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
    4.41 +
    4.42 +definition
    4.43 +  prime :: "[_, 'a] \<Rightarrow> bool" where
    4.44 +  "prime G p ==
    4.45 +    p \<notin> Units G \<and> 
    4.46 +    (\<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)"
    4.47  
    4.48  
    4.49  subsubsection {* Divisibility *}
    4.50 @@ -1041,20 +1041,21 @@
    4.51  
    4.52  subsubsection {* Function definitions *}
    4.53  
    4.54 -constdefs (structure G)
    4.55 +definition
    4.56    factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
    4.57 -  "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> = a"
    4.58 -
    4.59 +  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"
    4.60 +
    4.61 +definition
    4.62    wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
    4.63 -  "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> \<sim> a"
    4.64 +  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"
    4.65  
    4.66  abbreviation
    4.67 -  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) where
    4.68 -  "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
    4.69 -
    4.70 -constdefs (structure G)
    4.71 +  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
    4.72 +  where "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
    4.73 +
    4.74 +definition
    4.75    essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
    4.76 -  "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>] fs2)"
    4.77 +  where "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
    4.78  
    4.79  
    4.80  locale factorial_monoid = comm_monoid_cancel +
    4.81 @@ -1901,7 +1902,7 @@
    4.82  abbreviation
    4.83    "assocs G x == eq_closure_of (division_rel G) {x}"
    4.84  
    4.85 -constdefs (structure G)
    4.86 +definition
    4.87    "fmset G as \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
    4.88  
    4.89  
    4.90 @@ -2615,23 +2616,25 @@
    4.91  
    4.92  subsubsection {* Definitions *}
    4.93  
    4.94 -constdefs (structure G)
    4.95 +definition
    4.96    isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
    4.97 -  "x gcdof a b \<equiv> x divides a \<and> x divides b \<and> 
    4.98 -                 (\<forall>y\<in>carrier G. (y divides a \<and> y divides b \<longrightarrow> y divides x))"
    4.99 -
   4.100 +  where "x gcdof\<^bsub>G\<^esub> a b \<equiv> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and> 
   4.101 +    (\<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))"
   4.102 +
   4.103 +definition
   4.104    islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
   4.105 -  "x lcmof a b \<equiv> a divides x \<and> b divides x \<and> 
   4.106 -                 (\<forall>y\<in>carrier G. (a divides y \<and> b divides y \<longrightarrow> x divides y))"
   4.107 -
   4.108 -constdefs (structure G)
   4.109 +  where "x lcmof\<^bsub>G\<^esub> a b \<equiv> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and> 
   4.110 +    (\<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))"
   4.111 +
   4.112 +definition
   4.113    somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   4.114 -  "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof a b"
   4.115 -
   4.116 +  where "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b"
   4.117 +
   4.118 +definition
   4.119    somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   4.120 -  "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
   4.121 -
   4.122 -constdefs (structure G)
   4.123 +  where "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b"
   4.124 +
   4.125 +definition
   4.126    "SomeGcd G A == inf (division_rel G) A"
   4.127  
   4.128  
     5.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 06:59:23 2010 +0100
     5.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 15:57:40 2010 +0100
     5.3 @@ -285,11 +285,12 @@
     5.4  
     5.5  subsubsection {* Products over Finite Sets *}
     5.6  
     5.7 -constdefs (structure G)
     5.8 -  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
     5.9 -  "finprod G f A == if finite A
    5.10 -      then foldD (carrier G) (mult G o f) \<one> A
    5.11 -      else undefined"
    5.12 +definition
    5.13 +  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" where
    5.14 +  "finprod G f A ==
    5.15 +    if finite A
    5.16 +    then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
    5.17 +    else undefined"
    5.18  
    5.19  syntax
    5.20    "_finprod" :: "index => idt => 'a set => 'b => 'b"
     6.1 --- a/src/HOL/Algebra/Group.thy	Sun Mar 21 06:59:23 2010 +0100
     6.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 15:57:40 2010 +0100
     6.3 @@ -22,13 +22,14 @@
     6.4    mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
     6.5    one     :: 'a ("\<one>\<index>")
     6.6  
     6.7 -constdefs (structure G)
     6.8 +definition
     6.9    m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
    6.10 -  "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
    6.11 +  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>)"
    6.12  
    6.13 +definition
    6.14    Units :: "_ => 'a set"
    6.15    --{*The set of invertible elements*}
    6.16 -  "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    6.17 +  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>)}"
    6.18  
    6.19  consts
    6.20    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    6.21 @@ -534,8 +535,8 @@
    6.22  
    6.23  subsection {* Homomorphisms and Isomorphisms *}
    6.24  
    6.25 -constdefs (structure G and H)
    6.26 -  hom :: "_ => _ => ('a => 'b) set"
    6.27 +definition
    6.28 +  hom :: "_ => _ => ('a => 'b) set" where
    6.29    "hom G H ==
    6.30      {h. h \<in> carrier G -> carrier H &
    6.31        (\<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)}"
     7.1 --- a/src/HOL/Algebra/Ideal.thy	Sun Mar 21 06:59:23 2010 +0100
     7.2 +++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 21 15:57:40 2010 +0100
     7.3 @@ -47,9 +47,9 @@
     7.4  
     7.5  subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
     7.6  
     7.7 -constdefs (structure R)
     7.8 +definition
     7.9    genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
    7.10 -  "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
    7.11 +  where "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
    7.12  
    7.13  
    7.14  subsubsection {* Principal Ideals *}
    7.15 @@ -451,9 +451,9 @@
    7.16  
    7.17  text {* Generation of Principal Ideals in Commutative Rings *}
    7.18  
    7.19 -constdefs (structure R)
    7.20 +definition
    7.21    cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
    7.22 -  "cgenideal R a \<equiv> { x \<otimes> a | x. x \<in> carrier R }"
    7.23 +  where "cgenideal R a \<equiv> {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
    7.24  
    7.25  text {* genhideal (?) really generates an ideal *}
    7.26  lemma (in cring) cgenideal_ideal:
     8.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Mar 21 06:59:23 2010 +0100
     8.2 +++ b/src/HOL/Algebra/Lattice.thy	Sun Mar 21 15:57:40 2010 +0100
     8.3 @@ -25,9 +25,9 @@
     8.4      and le_cong:
     8.5        "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
     8.6  
     8.7 -constdefs (structure L)
     8.8 +definition
     8.9    lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    8.10 -  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
    8.11 +  where "x \<sqsubset>\<^bsub>L\<^esub> y == x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
    8.12  
    8.13  
    8.14  subsubsection {* The order relation *}
    8.15 @@ -102,12 +102,13 @@
    8.16  
    8.17  subsubsection {* Upper and lower bounds of a set *}
    8.18  
    8.19 -constdefs (structure L)
    8.20 +definition
    8.21    Upper :: "[_, 'a set] => 'a set"
    8.22 -  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
    8.23 +  where "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
    8.24  
    8.25 +definition
    8.26    Lower :: "[_, 'a set] => 'a set"
    8.27 -  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
    8.28 +  where "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
    8.29  
    8.30  lemma Upper_closed [intro!, simp]:
    8.31    "Upper L A \<subseteq> carrier L"
    8.32 @@ -275,12 +276,13 @@
    8.33  
    8.34  subsubsection {* Least and greatest, as predicate *}
    8.35  
    8.36 -constdefs (structure L)
    8.37 +definition
    8.38    least :: "[_, 'a, 'a set] => bool"
    8.39 -  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
    8.40 +  where "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
    8.41  
    8.42 +definition
    8.43    greatest :: "[_, 'a, 'a set] => bool"
    8.44 -  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
    8.45 +  where "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
    8.46  
    8.47  text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
    8.48    .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
    8.49 @@ -400,18 +402,21 @@
    8.50  
    8.51  text {* Supremum and infimum *}
    8.52  
    8.53 -constdefs (structure L)
    8.54 +definition
    8.55    sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
    8.56 -  "\<Squnion>A == SOME x. least L x (Upper L A)"
    8.57 +  where "\<Squnion>\<^bsub>L\<^esub>A == SOME x. least L x (Upper L A)"
    8.58  
    8.59 +definition
    8.60    inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
    8.61 -  "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
    8.62 +  where "\<Sqinter>\<^bsub>L\<^esub>A == SOME x. greatest L x (Lower L A)"
    8.63  
    8.64 +definition
    8.65    join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
    8.66 -  "x \<squnion> y == \<Squnion> {x, y}"
    8.67 +  where "x \<squnion>\<^bsub>L\<^esub> y == \<Squnion>\<^bsub>L\<^esub>{x, y}"
    8.68  
    8.69 +definition
    8.70    meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
    8.71 -  "x \<sqinter> y == \<Sqinter> {x, y}"
    8.72 +  where "x \<sqinter>\<^bsub>L\<^esub> y == \<Sqinter>\<^bsub>L\<^esub>{x, y}"
    8.73  
    8.74  
    8.75  subsection {* Lattices *}
    8.76 @@ -981,12 +986,13 @@
    8.77    shows "weak_complete_lattice L"
    8.78    proof qed (auto intro: sup_exists inf_exists)
    8.79  
    8.80 -constdefs (structure L)
    8.81 +definition
    8.82    top :: "_ => 'a" ("\<top>\<index>")
    8.83 -  "\<top> == sup L (carrier L)"
    8.84 +  where "\<top>\<^bsub>L\<^esub> == sup L (carrier L)"
    8.85  
    8.86 +definition
    8.87    bottom :: "_ => 'a" ("\<bottom>\<index>")
    8.88 -  "\<bottom> == inf L (carrier L)"
    8.89 +  where "\<bottom>\<^bsub>L\<^esub> == inf L (carrier L)"
    8.90  
    8.91  
    8.92  lemma (in weak_complete_lattice) supI:
     9.1 --- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 06:59:23 2010 +0100
     9.2 +++ b/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 15:57:40 2010 +0100
     9.3 @@ -11,10 +11,10 @@
     9.4  
     9.5  subsection {* Multiplication on Cosets *}
     9.6  
     9.7 -constdefs (structure R)
     9.8 +definition
     9.9    rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
    9.10      ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
    9.11 -  "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)"
    9.12 +  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)"
    9.13  
    9.14  
    9.15  text {* @{const "rcoset_mult"} fulfils the properties required by
    9.16 @@ -89,11 +89,10 @@
    9.17  
    9.18  subsection {* Quotient Ring Definition *}
    9.19  
    9.20 -constdefs (structure R)
    9.21 -  FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
    9.22 -     (infixl "Quot" 65)
    9.23 -  "FactRing R I \<equiv>
    9.24 -    \<lparr>carrier = a_rcosets I, mult = rcoset_mult R I, one = (I +> \<one>), zero = I, add = set_add R\<rparr>"
    9.25 +definition
    9.26 +  FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"  (infixl "Quot" 65)
    9.27 +  where "FactRing R I \<equiv>
    9.28 +    \<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>"
    9.29  
    9.30  
    9.31  subsection {* Factorization over General Ideals *}
    10.1 --- a/src/HOL/Algebra/Ring.thy	Sun Mar 21 06:59:23 2010 +0100
    10.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Mar 21 15:57:40 2010 +0100
    10.3 @@ -6,7 +6,8 @@
    10.4  
    10.5  theory Ring
    10.6  imports FiniteProduct
    10.7 -uses ("ringsimp.ML") begin
    10.8 +uses ("ringsimp.ML")
    10.9 +begin
   10.10  
   10.11  
   10.12  section {* The Algebraic Hierarchy of Rings *}
   10.13 @@ -19,12 +20,13 @@
   10.14  
   10.15  text {* Derived operations. *}
   10.16  
   10.17 -constdefs (structure R)
   10.18 +definition
   10.19    a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
   10.20 -  "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
   10.21 +  where "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
   10.22  
   10.23 +definition
   10.24    a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
   10.25 -  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
   10.26 +  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)"
   10.27  
   10.28  locale abelian_monoid =
   10.29    fixes G (structure)
   10.30 @@ -728,12 +730,13 @@
   10.31  
   10.32  subsection {* Morphisms *}
   10.33  
   10.34 -constdefs (structure R S)
   10.35 +definition
   10.36    ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
   10.37 -  "ring_hom R S == {h. h \<in> carrier R -> carrier S &
   10.38 +  where "ring_hom R S ==
   10.39 +    {h. h \<in> carrier R -> carrier S &
   10.40        (ALL x y. x \<in> carrier R & y \<in> carrier R -->
   10.41 -        h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
   10.42 -      h \<one> = \<one>\<^bsub>S\<^esub>}"
   10.43 +        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) &
   10.44 +      h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
   10.45  
   10.46  lemma ring_hom_memI:
   10.47    fixes R (structure) and S (structure)