--- 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] \<Rightarrow> 'a set" (infixl "+>\<index>" 60)
- where "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
definition
a_l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<+\<index>" 60)
- where "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
definition
A_RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("a'_rcosets\<index> _" [81] 80)
- where "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
definition
set_add :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
- where "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
definition
A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("a'_set'_inv\<index> _" [81] 80)
- where "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
definition
a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set" ("racong\<index> _")
- where "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) where
+definition
+ A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
--{*Actually defined for groups rather than monoids*}
- "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
-definition a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>
- ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where
+definition
+ a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
--{*the kernel of a homomorphism (additive)*}
- "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
- \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
+ where "a_kernel G H h =
+ kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
+ \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> 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 \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
+ "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
--- 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 \<Rightarrow> ('a \<Rightarrow> 'a) set" where
+definition
+ Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
--{*Only extensional functions, since otherwise we get too many.*}
- "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
+ where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
-definition BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
- "BijGroup S \<equiv>
+definition
+ BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+ where "BijGroup S =
\<lparr>carrier = Bij S,
mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
one = \<lambda>x \<in> S. x\<rparr>"
@@ -69,11 +71,13 @@
done
-definition auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set" where
- "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
+definition
+ auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
+ where "auto G = hom G G \<inter> Bij (carrier G)"
-definition AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
- "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
+definition
+ AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+ where "AutoGroup G = BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
--- 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 :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
- where "x .\<in>\<^bsub>S\<^esub> A \<equiv> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
+ where "x .\<in>\<^bsub>S\<^esub> A \<longleftrightarrow> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
definition
set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
- 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))"
+ 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))"
definition
eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
- where "class_of\<^bsub>S\<^esub> x == {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
+ where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
definition
eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
- where "closure_of\<^bsub>S\<^esub> A == {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
+ where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
definition
eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
- where "is_closed\<^bsub>S\<^esub> A == (A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A)"
+ where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
abbreviation
not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
--- 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] \<Rightarrow> 'a set" (infixl "#>\<index>" 60)
- where "H #>\<^bsub>G\<^esub> a \<equiv> \<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a}"
+ where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
definition
l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<#\<index>" 60)
- where "a <#\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h}"
+ where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
definition
RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("rcosets\<index> _" [81] 80)
- where "rcosets\<^bsub>G\<^esub> H \<equiv> \<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a}"
+ where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
definition
set_mult :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
- where "H <#>\<^bsub>G\<^esub> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k}"
+ where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
definition
SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("set'_inv\<index> _" [81] 80)
- where "set_inv\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
+ where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
locale normal = subgroup + group +
@@ -595,7 +595,7 @@
definition
r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set" ("rcong\<index> _")
- 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}"
+ 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}"
lemma (in subgroup) equiv_rcong:
@@ -754,8 +754,9 @@
subsection {*Order of a Group and Lagrange's Theorem*}
-definition order :: "('a, 'b) monoid_scheme \<Rightarrow> nat" where
- "order S \<equiv> card (carrier S)"
+definition
+ order :: "('a, 'b) monoid_scheme \<Rightarrow> 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] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65) where
+definition
+ FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
--{*Actually defined for groups rather than monoids*}
- "FactGroup G H \<equiv>
- \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
+ where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
lemma (in normal) setmult_closed:
"\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> 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 \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>
- ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where
+definition
+ kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
--{*the kernel of a homomorphism*}
- "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
+ where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
apply (rule subgroup.intro)
--- 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] \<Rightarrow> bool" (infix "divides\<index>" 65)
- where "a divides\<^bsub>G\<^esub> b == \<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c"
+ where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)"
definition
associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
- where "a \<sim>\<^bsub>G\<^esub> b == a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
+ where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
abbreviation
"division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
definition
properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
- where "properfactor G a b == a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
+ where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
definition
irreducible :: "[_, 'a] \<Rightarrow> bool"
- where "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
+ where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
definition
prime :: "[_, 'a] \<Rightarrow> bool" where
- "prime G p ==
+ "prime G p \<longleftrightarrow>
p \<notin> Units G \<and>
(\<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)"
@@ -1043,11 +1043,11 @@
definition
factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
- 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"
+ 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"
definition
wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
- 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"
+ 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"
abbreviation
list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
@@ -1055,7 +1055,7 @@
definition
essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
- where "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
+ where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^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 \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
+ "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"
text {* Helper lemmas *}
@@ -2618,24 +2618,24 @@
definition
isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80)
- where "x gcdof\<^bsub>G\<^esub> a b \<equiv> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
+ where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
(\<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))"
definition
islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80)
- where "x lcmof\<^bsub>G\<^esub> a b \<equiv> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
+ where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
(\<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))"
definition
somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- where "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b"
+ where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"
definition
somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- where "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b"
+ where "somelcm G a b = (SOME x. x \<in> carrier G \<and> 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 :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
- "factorcount G a == THE c. (ALL as. set as \<subseteq> carrier G \<and>
- wfactors G as a \<longrightarrow> c = length as)"
+definition
+ factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
+ "factorcount G a =
+ (THE c. (ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as))"
lemma (in monoid) ee_length:
assumes ee: "essentially_equal G as bs"
--- 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*}
--- 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) \<in> 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) \<in> 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) \<in> foldSetD D f e)"
lemma foldSetD_closed:
"[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> 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) \<one>\<^bsub>G\<^esub> A
- else undefined"
+ else undefined)"
syntax
"_finprod" :: "index => idt => 'a set => 'b => 'b"
--- a/src/HOL/Algebra/Group.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/Group.thy Sun Mar 21 16:51:37 2010 +0100
@@ -24,12 +24,12 @@
definition
m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
- 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>)"
+ 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>)"
definition
Units :: "_ => 'a set"
--{*The set of invertible elements*}
- 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>)}"
+ 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>)}"
consts
pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
@@ -479,10 +479,12 @@
subsection {* Direct Products *}
-definition DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
- "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
- mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
- one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
+definition
+ DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
+ "G \<times>\<times> H =
+ \<lparr>carrier = carrier G \<times> carrier H,
+ mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
+ one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
lemma DirProd_monoid:
assumes "monoid G" and "monoid H"
@@ -537,7 +539,7 @@
definition
hom :: "_ => _ => ('a => 'b) set" where
- "hom G H ==
+ "hom G H =
{h. h \<in> carrier G -> carrier H &
(\<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)}"
@@ -545,8 +547,9 @@
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
by (fastsimp simp add: hom_def compose_def)
-definition iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) where
- "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
+definition
+ iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
+ where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
lemma iso_refl: "(%x. x) \<in> G \<cong> G"
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
--- a/src/HOL/Algebra/Ideal.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/Ideal.thy Sun Mar 21 16:51:37 2010 +0100
@@ -49,7 +49,7 @@
definition
genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
- where "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
+ where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
subsubsection {* Principal Ideals *}
@@ -453,7 +453,7 @@
definition
cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
- where "cgenideal R a \<equiv> {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
+ where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
text {* genhideal (?) really generates an ideal *}
lemma (in cring) cgenideal_ideal:
--- a/src/HOL/Algebra/IntRing.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/IntRing.thy Sun Mar 21 16:51:37 2010 +0100
@@ -22,8 +22,9 @@
subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
-definition int_ring :: "int ring" ("\<Z>") where
- "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+definition
+ int_ring :: "int ring" ("\<Z>") where
+ "int_ring = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
lemma int_Zcarr [intro!, simp]:
"k \<in> carrier \<Z>"
@@ -323,8 +324,9 @@
subsection {* Ideals and the Modulus *}
-definition ZMod :: "int => int => int set" where
- "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
+definition
+ ZMod :: "int => int => int set"
+ where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
lemmas ZMod_defs =
ZMod_def genideal_def
@@ -405,8 +407,9 @@
subsection {* Factorization *}
-definition ZFact :: "int \<Rightarrow> int set ring" where
- "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
+definition
+ ZFact :: "int \<Rightarrow> int set ring"
+ where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
lemmas ZFact_defs = ZFact_def FactRing_def
--- a/src/HOL/Algebra/Lattice.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/Lattice.thy Sun Mar 21 16:51:37 2010 +0100
@@ -27,7 +27,7 @@
definition
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
- where "x \<sqsubset>\<^bsub>L\<^esub> y == x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
+ where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
subsubsection {* The order relation *}
@@ -104,11 +104,11 @@
definition
Upper :: "[_, 'a set] => 'a set"
- where "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
+ where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
definition
Lower :: "[_, 'a set] => 'a set"
- where "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
+ where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
lemma Upper_closed [intro!, simp]:
"Upper L A \<subseteq> carrier L"
@@ -278,11 +278,11 @@
definition
least :: "[_, 'a, 'a set] => bool"
- where "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
+ where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
definition
greatest :: "[_, 'a, 'a set] => bool"
- where "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
+ where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
.\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
@@ -404,19 +404,19 @@
definition
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
- where "\<Squnion>\<^bsub>L\<^esub>A == SOME x. least L x (Upper L A)"
+ where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
definition
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
- where "\<Sqinter>\<^bsub>L\<^esub>A == SOME x. greatest L x (Lower L A)"
+ where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
definition
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
- where "x \<squnion>\<^bsub>L\<^esub> y == \<Squnion>\<^bsub>L\<^esub>{x, y}"
+ where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
definition
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
- where "x \<sqinter>\<^bsub>L\<^esub> y == \<Sqinter>\<^bsub>L\<^esub>{x, y}"
+ where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
subsection {* Lattices *}
@@ -988,11 +988,11 @@
definition
top :: "_ => 'a" ("\<top>\<index>")
- where "\<top>\<^bsub>L\<^esub> == sup L (carrier L)"
+ where "\<top>\<^bsub>L\<^esub> = sup L (carrier L)"
definition
bottom :: "_ => 'a" ("\<bottom>\<index>")
- where "\<bottom>\<^bsub>L\<^esub> == inf L (carrier L)"
+ where "\<bottom>\<^bsub>L\<^esub> = inf L (carrier L)"
lemma (in weak_complete_lattice) supI:
--- a/src/HOL/Algebra/QuotRing.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Sun Mar 21 16:51:37 2010 +0100
@@ -14,7 +14,7 @@
definition
rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
- 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)"
+ 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))"
text {* @{const "rcoset_mult"} fulfils the properties required by
@@ -91,7 +91,7 @@
definition
FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring" (infixl "Quot" 65)
- where "FactRing R I \<equiv>
+ where "FactRing R I =
\<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>"
--- a/src/HOL/Algebra/Ring.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/Ring.thy Sun Mar 21 16:51:37 2010 +0100
@@ -22,11 +22,11 @@
definition
a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
- where "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+ where "a_inv R = m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
definition
a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
- 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)"
+ 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)"
locale abelian_monoid =
fixes G (structure)
@@ -200,9 +200,9 @@
This definition makes it easy to lift lemmas from @{term finprod}.
*}
-definition finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
- "finsum G f A == finprod (| carrier = carrier G,
- mult = add G, one = zero G |) f A"
+definition
+ finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
+ "finsum G f A = finprod (| carrier = carrier G, mult = add G, one = zero G |) f A"
syntax
"_finsum" :: "index => idt => 'a set => 'b => 'b"
@@ -732,7 +732,7 @@
definition
ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
- where "ring_hom R S ==
+ where "ring_hom R S =
{h. h \<in> carrier R -> carrier S &
(ALL x y. x \<in> carrier R & y \<in> carrier R -->
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) &
--- a/src/HOL/Algebra/UnivPoly.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Sun Mar 21 16:51:37 2010 +0100
@@ -54,11 +54,12 @@
monom :: "['a, nat] => 'p"
coeff :: "['p, nat] => 'a"
-definition up :: "('a, 'm) ring_scheme => (nat => 'a) set"
- where up_def: "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
+definition
+ up :: "('a, 'm) ring_scheme => (nat => 'a) set"
+ where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
- where UP_def: "UP R == (|
+ where "UP R = (|
carrier = up R,
mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
@@ -711,8 +712,9 @@
subsection {* The Degree Function *}
-definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
- where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)"
+definition
+ deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
+ where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
context UP_ring
begin
@@ -1173,8 +1175,8 @@
definition
eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
'a => 'b, 'b, nat => 'a] => 'b"
- where "eval R S phi s == \<lambda>p \<in> carrier (UP R).
- \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i"
+ where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
+ \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
context UP
begin
@@ -1854,11 +1856,11 @@
by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
ring_hom_cring_axioms.intro UP_cring.intro)
-definition INTEG :: "int ring"
- where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+definition
+ INTEG :: "int ring"
+ where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
-lemma INTEG_cring:
- "cring INTEG"
+lemma INTEG_cring: "cring INTEG"
by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
zadd_zminus_inverse2 zadd_zmult_distrib)
--- a/src/HOL/Algebra/abstract/Ring2.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sun Mar 21 16:51:37 2010 +0100
@@ -30,16 +30,17 @@
and divide_def: "a / b = a * inverse b"
begin
-definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where
- assoc_def: "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
+definition
+ assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50)
+ where "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
-definition irred :: "'a \<Rightarrow> bool" where
- irred_def: "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1
- & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
+definition
+ irred :: "'a \<Rightarrow> bool" where
+ "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
-definition prime :: "'a \<Rightarrow> bool" where
- prime_def: "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1
- & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
+definition
+ prime :: "'a \<Rightarrow> bool" where
+ "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
end
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Sun Mar 21 16:51:37 2010 +0100
@@ -47,16 +47,16 @@
section {* Constants *}
definition
- coeff :: "['a up, nat] => ('a::zero)" where
- "coeff p n = Rep_UP p n"
+ coeff :: "['a up, nat] => ('a::zero)"
+ where "coeff p n = Rep_UP p n"
definition
- monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) where
- "monom a n = Abs_UP (%i. if i=n then a else 0)"
+ monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70)
+ where "monom a n = Abs_UP (%i. if i=n then a else 0)"
definition
- smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70) where
- "a *s p = Abs_UP (%i. a * Rep_UP p i)"
+ smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70)
+ where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
lemma coeff_bound_ex: "EX n. bound n (coeff p)"
proof -
@@ -132,7 +132,7 @@
begin
definition
- up_mult_def: "p * q = Abs_UP (%n::nat. setsum
+ up_mult_def: "p * q = Abs_UP (%n::nat. setsum
(%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
instance ..
@@ -149,7 +149,7 @@
THE x. a * x = 1 else 0)"
definition
- up_divide_def: "(a :: 'a up) / b = a * inverse b"
+ up_divide_def: "(a :: 'a up) / b = a * inverse b"
instance ..
@@ -482,8 +482,8 @@
section {* The degree function *}
definition
- deg :: "('a::zero) up => nat" where
- "deg p = (LEAST n. bound n (coeff p))"
+ deg :: "('a::zero) up => nat"
+ where "deg p = (LEAST n. bound n (coeff p))"
lemma deg_aboveI:
"(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"