# HG changeset patch # User wenzelm # Date 1269186697 -3600 # Node ID 5443079512eaf3be28c8d4213b64a9cb5c549ac6 # Parent 19f1f7066917d5c6ca7893dd07fd3965e8e9087c slightly more uniform definitions -- eliminated old-style meta-equality; diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/AbelCoset.thy Sun Mar 21 16:51:37 2010 +0100 @@ -19,37 +19,39 @@ definition a_r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "+>\" 60) - where "a_r_coset G \ r_coset \carrier = carrier G, mult = add G, one = zero G\" + where "a_r_coset G = r_coset \carrier = carrier G, mult = add G, one = zero G\" definition a_l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<+\" 60) - where "a_l_coset G \ l_coset \carrier = carrier G, mult = add G, one = zero G\" + where "a_l_coset G = l_coset \carrier = carrier G, mult = add G, one = zero G\" definition A_RCOSETS :: "[_, 'a set] \ ('a set)set" ("a'_rcosets\ _" [81] 80) - where "A_RCOSETS G H \ RCOSETS \carrier = carrier G, mult = add G, one = zero G\ H" + where "A_RCOSETS G H = RCOSETS \carrier = carrier G, mult = add G, one = zero G\ H" definition set_add :: "[_, 'a set ,'a set] \ 'a set" (infixl "<+>\" 60) - where "set_add G \ set_mult \carrier = carrier G, mult = add G, one = zero G\" + where "set_add G = set_mult \carrier = carrier G, mult = add G, one = zero G\" definition A_SET_INV :: "[_,'a set] \ 'a set" ("a'_set'_inv\ _" [81] 80) - where "A_SET_INV G H \ SET_INV \carrier = carrier G, mult = add G, one = zero G\ H" + where "A_SET_INV G H = SET_INV \carrier = carrier G, mult = add G, one = zero G\ H" definition a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \ ('a*'a)set" ("racong\ _") - where "a_r_congruent G \ r_congruent \carrier = carrier G, mult = add G, one = zero G\" + where "a_r_congruent G = r_congruent \carrier = carrier G, mult = add G, one = zero G\" -definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \ ('a set) monoid" (infixl "A'_Mod" 65) where +definition + A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \ ('a set) monoid" (infixl "A'_Mod" 65) --{*Actually defined for groups rather than monoids*} - "A_FactGroup G H \ FactGroup \carrier = carrier G, mult = add G, one = zero G\ H" + where "A_FactGroup G H = FactGroup \carrier = carrier G, mult = add G, one = zero G\ H" -definition a_kernel :: "('a, 'm) ring_scheme \ ('b, 'n) ring_scheme \ - ('a \ 'b) \ 'a set" where +definition + a_kernel :: "('a, 'm) ring_scheme \ ('b, 'n) ring_scheme \ ('a \ 'b) \ 'a set" --{*the kernel of a homomorphism (additive)*} - "a_kernel G H h \ kernel \carrier = carrier G, mult = add G, one = zero G\ - \carrier = carrier H, mult = add H, one = zero H\ h" + where "a_kernel G H h = + kernel \carrier = carrier G, mult = add G, one = zero G\ + \carrier = carrier H, mult = add H, one = zero H\ h" locale abelian_group_hom = G: abelian_group G + H: abelian_group H for G (structure) and H (structure) + @@ -527,7 +529,7 @@ a_kernel_def kernel_def lemma a_kernel_def': - "a_kernel R S h \ {x \ carrier R. h x = \\<^bsub>S\<^esub>}" + "a_kernel R S h = {x \ carrier R. h x = \\<^bsub>S\<^esub>}" by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps]) diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/Bij.thy --- a/src/HOL/Algebra/Bij.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/Bij.thy Sun Mar 21 16:51:37 2010 +0100 @@ -7,12 +7,14 @@ section {* Bijections of a Set, Permutation and Automorphism Groups *} -definition Bij :: "'a set \ ('a \ 'a) set" where +definition + Bij :: "'a set \ ('a \ 'a) set" --{*Only extensional functions, since otherwise we get too many.*} - "Bij S \ extensional S \ {f. bij_betw f S S}" + where "Bij S = extensional S \ {f. bij_betw f S S}" -definition BijGroup :: "'a set \ ('a \ 'a) monoid" where - "BijGroup S \ +definition + BijGroup :: "'a set \ ('a \ 'a) monoid" + where "BijGroup S = \carrier = Bij S, mult = \g \ Bij S. \f \ Bij S. compose S g f, one = \x \ S. x\" @@ -69,11 +71,13 @@ done -definition auto :: "('a, 'b) monoid_scheme \ ('a \ 'a) set" where - "auto G \ hom G G \ Bij (carrier G)" +definition + auto :: "('a, 'b) monoid_scheme \ ('a \ 'a) set" + where "auto G = hom G G \ Bij (carrier G)" -definition AutoGroup :: "('a, 'c) monoid_scheme \ ('a \ 'a) monoid" where - "AutoGroup G \ BijGroup (carrier G) \carrier := auto G\" +definition + AutoGroup :: "('a, 'c) monoid_scheme \ ('a \ 'a) monoid" + where "AutoGroup G = BijGroup (carrier G) \carrier := auto G\" lemma (in group) id_in_auto: "(\x \ carrier G. x) \ auto G" by (simp add: auto_def hom_def restrictI group.axioms id_Bij) diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/Congruence.thy Sun Mar 21 16:51:37 2010 +0100 @@ -21,23 +21,23 @@ definition elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) - where "x .\\<^bsub>S\<^esub> A \ (\y \ A. x .=\<^bsub>S\<^esub> y)" + where "x .\\<^bsub>S\<^esub> A \ (\y \ A. x .=\<^bsub>S\<^esub> y)" definition set_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.=}\" 50) - where "A {.=}\<^bsub>S\<^esub> B == ((\x \ A. x .\\<^bsub>S\<^esub> B) \ (\x \ B. x .\\<^bsub>S\<^esub> A))" + where "A {.=}\<^bsub>S\<^esub> B \ ((\x \ A. x .\\<^bsub>S\<^esub> B) \ (\x \ B. x .\\<^bsub>S\<^esub> A))" definition eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\ _") - where "class_of\<^bsub>S\<^esub> x == {y \ carrier S. x .=\<^bsub>S\<^esub> y}" + where "class_of\<^bsub>S\<^esub> x = {y \ carrier S. x .=\<^bsub>S\<^esub> y}" definition eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\ _") - where "closure_of\<^bsub>S\<^esub> A == {y \ carrier S. y .\\<^bsub>S\<^esub> A}" + where "closure_of\<^bsub>S\<^esub> A = {y \ carrier S. y .\\<^bsub>S\<^esub> A}" definition eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\ _") - where "is_closed\<^bsub>S\<^esub> A == (A \ carrier S \ closure_of\<^bsub>S\<^esub> A = A)" + where "is_closed\<^bsub>S\<^esub> A \ A \ carrier S \ closure_of\<^bsub>S\<^esub> A = A" abbreviation not_eq :: "_ \ 'a \ 'a \ bool" (infixl ".\\" 50) diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/Coset.thy Sun Mar 21 16:51:37 2010 +0100 @@ -10,23 +10,23 @@ definition r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "#>\" 60) - where "H #>\<^bsub>G\<^esub> a \ \h\H. {h \\<^bsub>G\<^esub> a}" + where "H #>\<^bsub>G\<^esub> a = (\h\H. {h \\<^bsub>G\<^esub> a})" definition l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<#\" 60) - where "a <#\<^bsub>G\<^esub> H \ \h\H. {a \\<^bsub>G\<^esub> h}" + where "a <#\<^bsub>G\<^esub> H = (\h\H. {a \\<^bsub>G\<^esub> h})" definition RCOSETS :: "[_, 'a set] \ ('a set)set" ("rcosets\ _" [81] 80) - where "rcosets\<^bsub>G\<^esub> H \ \a\carrier G. {H #>\<^bsub>G\<^esub> a}" + where "rcosets\<^bsub>G\<^esub> H = (\a\carrier G. {H #>\<^bsub>G\<^esub> a})" definition set_mult :: "[_, 'a set ,'a set] \ 'a set" (infixl "<#>\" 60) - where "H <#>\<^bsub>G\<^esub> K \ \h\H. \k\K. {h \\<^bsub>G\<^esub> k}" + where "H <#>\<^bsub>G\<^esub> K = (\h\H. \k\K. {h \\<^bsub>G\<^esub> k})" definition SET_INV :: "[_,'a set] \ 'a set" ("set'_inv\ _" [81] 80) - where "set_inv\<^bsub>G\<^esub> H \ \h\H. {inv\<^bsub>G\<^esub> h}" + where "set_inv\<^bsub>G\<^esub> H = (\h\H. {inv\<^bsub>G\<^esub> h})" locale normal = subgroup + group + @@ -595,7 +595,7 @@ definition r_congruent :: "[('a,'b)monoid_scheme, 'a set] \ ('a*'a)set" ("rcong\ _") - where "rcong\<^bsub>G\<^esub> H \ {(x,y). x \ carrier G & y \ carrier G & inv\<^bsub>G\<^esub> x \\<^bsub>G\<^esub> y \ H}" + where "rcong\<^bsub>G\<^esub> H = {(x,y). x \ carrier G & y \ carrier G & inv\<^bsub>G\<^esub> x \\<^bsub>G\<^esub> y \ H}" lemma (in subgroup) equiv_rcong: @@ -754,8 +754,9 @@ subsection {*Order of a Group and Lagrange's Theorem*} -definition order :: "('a, 'b) monoid_scheme \ nat" where - "order S \ card (carrier S)" +definition + order :: "('a, 'b) monoid_scheme \ nat" + where "order S = card (carrier S)" lemma (in group) rcosets_part_G: assumes "subgroup H G" @@ -824,10 +825,10 @@ subsection {*Quotient Groups: Factorization of a Group*} -definition FactGroup :: "[('a,'b) monoid_scheme, 'a set] \ ('a set) monoid" (infixl "Mod" 65) where +definition + FactGroup :: "[('a,'b) monoid_scheme, 'a set] \ ('a set) monoid" (infixl "Mod" 65) --{*Actually defined for groups rather than monoids*} - "FactGroup G H \ - \carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\" + where "FactGroup G H = \carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\" lemma (in normal) setmult_closed: "\K1 \ rcosets H; K2 \ rcosets H\ \ K1 <#> K2 \ rcosets H" @@ -890,10 +891,10 @@ text{*The quotient by the kernel of a homomorphism is isomorphic to the range of that homomorphism.*} -definition kernel :: "('a, 'm) monoid_scheme \ ('b, 'n) monoid_scheme \ - ('a \ 'b) \ 'a set" where +definition + kernel :: "('a, 'm) monoid_scheme \ ('b, 'n) monoid_scheme \ ('a \ 'b) \ 'a set" --{*the kernel of a homomorphism*} - "kernel G H h \ {x. x \ carrier G & h x = \\<^bsub>H\<^esub>}" + where "kernel G H h = {x. x \ carrier G & h x = \\<^bsub>H\<^esub>}" lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G" apply (rule subgroup.intro) diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Sun Mar 21 16:51:37 2010 +0100 @@ -162,26 +162,26 @@ definition factor :: "[_, 'a, 'a] \ bool" (infix "divides\" 65) - where "a divides\<^bsub>G\<^esub> b == \c\carrier G. b = a \\<^bsub>G\<^esub> c" + where "a divides\<^bsub>G\<^esub> b \ (\c\carrier G. b = a \\<^bsub>G\<^esub> c)" definition associated :: "[_, 'a, 'a] => bool" (infix "\\" 55) - where "a \\<^bsub>G\<^esub> b == a divides\<^bsub>G\<^esub> b \ b divides\<^bsub>G\<^esub> a" + where "a \\<^bsub>G\<^esub> b \ a divides\<^bsub>G\<^esub> b \ b divides\<^bsub>G\<^esub> a" abbreviation "division_rel G == \carrier = carrier G, eq = op \\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\" definition properfactor :: "[_, 'a, 'a] \ bool" - where "properfactor G a b == a divides\<^bsub>G\<^esub> b \ \(b divides\<^bsub>G\<^esub> a)" + where "properfactor G a b \ a divides\<^bsub>G\<^esub> b \ \(b divides\<^bsub>G\<^esub> a)" definition irreducible :: "[_, 'a] \ bool" - where "irreducible G a == a \ Units G \ (\b\carrier G. properfactor G b a \ b \ Units G)" + where "irreducible G a \ a \ Units G \ (\b\carrier G. properfactor G b a \ b \ Units G)" definition prime :: "[_, 'a] \ bool" where - "prime G p == + "prime G p \ p \ Units G \ (\a\carrier G. \b\carrier G. p divides\<^bsub>G\<^esub> (a \\<^bsub>G\<^esub> b) \ p divides\<^bsub>G\<^esub> a \ p divides\<^bsub>G\<^esub> b)" @@ -1043,11 +1043,11 @@ definition factors :: "[_, 'a list, 'a] \ bool" - where "factors G fs a == (\x \ (set fs). irreducible G x) \ foldr (op \\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> = a" + where "factors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (op \\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> = a" definition wfactors ::"[_, 'a list, 'a] \ bool" - where "wfactors G fs a == (\x \ (set fs). irreducible G x) \ foldr (op \\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> \\<^bsub>G\<^esub> a" + where "wfactors G fs a \ (\x \ (set fs). irreducible G x) \ foldr (op \\<^bsub>G\<^esub>) fs \\<^bsub>G\<^esub> \\<^bsub>G\<^esub> a" abbreviation list_assoc :: "('a,_) monoid_scheme \ 'a list \ 'a list \ bool" (infix "[\]\" 44) @@ -1055,7 +1055,7 @@ definition essentially_equal :: "[_, 'a list, 'a list] \ bool" - where "essentially_equal G fs1 fs2 == (\fs1'. fs1 <~~> fs1' \ fs1' [\]\<^bsub>G\<^esub> fs2)" + where "essentially_equal G fs1 fs2 \ (\fs1'. fs1 <~~> fs1' \ fs1' [\]\<^bsub>G\<^esub> fs2)" locale factorial_monoid = comm_monoid_cancel + @@ -1903,7 +1903,7 @@ "assocs G x == eq_closure_of (division_rel G) {x}" definition - "fmset G as \ multiset_of (map (\a. assocs G a) as)" + "fmset G as = multiset_of (map (\a. assocs G a) as)" text {* Helper lemmas *} @@ -2618,24 +2618,24 @@ definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \ bool" ("(_ gcdof\ _ _)" [81,81,81] 80) - where "x gcdof\<^bsub>G\<^esub> a b \ x divides\<^bsub>G\<^esub> a \ x divides\<^bsub>G\<^esub> b \ + where "x gcdof\<^bsub>G\<^esub> a b \ x divides\<^bsub>G\<^esub> a \ x divides\<^bsub>G\<^esub> b \ (\y\carrier G. (y divides\<^bsub>G\<^esub> a \ y divides\<^bsub>G\<^esub> b \ y divides\<^bsub>G\<^esub> x))" definition islcm :: "[_, 'a, 'a, 'a] \ bool" ("(_ lcmof\ _ _)" [81,81,81] 80) - where "x lcmof\<^bsub>G\<^esub> a b \ a divides\<^bsub>G\<^esub> x \ b divides\<^bsub>G\<^esub> x \ + where "x lcmof\<^bsub>G\<^esub> a b \ a divides\<^bsub>G\<^esub> x \ b divides\<^bsub>G\<^esub> x \ (\y\carrier G. (a divides\<^bsub>G\<^esub> y \ b divides\<^bsub>G\<^esub> y \ x divides\<^bsub>G\<^esub> y))" definition somegcd :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" - where "somegcd G a b == SOME x. x \ carrier G \ x gcdof\<^bsub>G\<^esub> a b" + where "somegcd G a b = (SOME x. x \ carrier G \ x gcdof\<^bsub>G\<^esub> a b)" definition somelcm :: "('a,_) monoid_scheme \ 'a \ 'a \ 'a" - where "somelcm G a b == SOME x. x \ carrier G \ x lcmof\<^bsub>G\<^esub> a b" + where "somelcm G a b = (SOME x. x \ carrier G \ x lcmof\<^bsub>G\<^esub> a b)" definition - "SomeGcd G A == inf (division_rel G) A" + "SomeGcd G A = inf (division_rel G) A" locale gcd_condition_monoid = comm_monoid_cancel + @@ -3633,9 +3633,10 @@ text {* Number of factors for wellfoundedness *} -definition factorcount :: "_ \ 'a \ nat" where - "factorcount G a == THE c. (ALL as. set as \ carrier G \ - wfactors G as a \ c = length as)" +definition + factorcount :: "_ \ 'a \ nat" where + "factorcount G a = + (THE c. (ALL as. set as \ carrier G \ wfactors G as a \ c = length as))" lemma (in monoid) ee_length: assumes ee: "essentially_equal G as bs" diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/Exponent.thy Sun Mar 21 16:51:37 2010 +0100 @@ -12,8 +12,9 @@ subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} -definition exponent :: "nat => nat => nat" where -"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" +definition + exponent :: "nat => nat => nat" + where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)" text{*Prime Theorems*} diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/FiniteProduct.thy Sun Mar 21 16:51:37 2010 +0100 @@ -26,8 +26,9 @@ inductive_cases empty_foldSetDE [elim!]: "({}, x) \ foldSetD D f e" -definition foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" where - "foldD D f e A == THE x. (A, x) \ foldSetD D f e" +definition + foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" + where "foldD D f e A = (THE x. (A, x) \ foldSetD D f e)" lemma foldSetD_closed: "[| (A, z) \ foldSetD D f e ; e \ D; !!x y. [| x \ A; y \ D |] ==> f x y \ D @@ -286,11 +287,11 @@ subsubsection {* Products over Finite Sets *} definition - finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" where - "finprod G f A == - if finite A + finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" + where "finprod G f A = + (if finite A then foldD (carrier G) (mult G o f) \