src/HOL/Algebra/Divisibility.thy
 changeset 35847 19f1f7066917 parent 35416 d8d7d1b785af child 35848 5443079512ea
```     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 06:59:23 2010 +0100
1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 15:57:40 2010 +0100
1.3 @@ -160,30 +160,30 @@
1.4
1.5  subsubsection {* Function definitions *}
1.6
1.7 -constdefs (structure G)
1.8 +definition
1.9    factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
1.10 -  "a divides b == \<exists>c\<in>carrier G. b = a \<otimes> c"
1.11 -
1.12 -constdefs (structure G)
1.13 +  where "a divides\<^bsub>G\<^esub> b == \<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c"
1.14 +
1.15 +definition
1.16    associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
1.17 -  "a \<sim> b == a divides b \<and> b divides a"
1.18 +  where "a \<sim>\<^bsub>G\<^esub> b == a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
1.19
1.20  abbreviation
1.21    "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
1.22
1.23 -constdefs (structure G)
1.24 +definition
1.25    properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
1.26 -  "properfactor G a b == a divides b \<and> \<not>(b divides a)"
1.27 -
1.28 -constdefs (structure G)
1.29 +  where "properfactor G a b == a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
1.30 +
1.31 +definition
1.32    irreducible :: "[_, 'a] \<Rightarrow> bool"
1.33 -  "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
1.34 -
1.35 -constdefs (structure G)
1.36 -  prime :: "[_, 'a] \<Rightarrow> bool"
1.37 -  "prime G p == p \<notin> Units G \<and>
1.38 -                (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides (a \<otimes> b) \<longrightarrow> p divides a \<or> p divides b)"
1.39 -
1.40 +  where "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
1.41 +
1.42 +definition
1.43 +  prime :: "[_, 'a] \<Rightarrow> bool" where
1.44 +  "prime G p ==
1.45 +    p \<notin> Units G \<and>
1.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)"
1.47
1.48
1.49  subsubsection {* Divisibility *}
1.50 @@ -1041,20 +1041,21 @@
1.51
1.52  subsubsection {* Function definitions *}
1.53
1.54 -constdefs (structure G)
1.55 +definition
1.56    factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
1.57 -  "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> = a"
1.58 -
1.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"
1.60 +
1.61 +definition
1.62    wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
1.63 -  "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> \<sim> a"
1.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"
1.65
1.66  abbreviation
1.67 -  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) where
1.68 -  "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
1.69 -
1.70 -constdefs (structure G)
1.71 +  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
1.72 +  where "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
1.73 +
1.74 +definition
1.75    essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
1.76 -  "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>] fs2)"
1.77 +  where "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
1.78
1.79
1.80  locale factorial_monoid = comm_monoid_cancel +
1.81 @@ -1901,7 +1902,7 @@
1.82  abbreviation
1.83    "assocs G x == eq_closure_of (division_rel G) {x}"
1.84
1.85 -constdefs (structure G)
1.86 +definition
1.87    "fmset G as \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
1.88
1.89
1.90 @@ -2615,23 +2616,25 @@
1.91
1.92  subsubsection {* Definitions *}
1.93
1.94 -constdefs (structure G)
1.95 +definition
1.96    isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
1.97 -  "x gcdof a b \<equiv> x divides a \<and> x divides b \<and>
1.98 -                 (\<forall>y\<in>carrier G. (y divides a \<and> y divides b \<longrightarrow> y divides x))"
1.99 -
1.100 +  where "x gcdof\<^bsub>G\<^esub> a b \<equiv> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
1.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))"
1.102 +
1.103 +definition
1.104    islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
1.105 -  "x lcmof a b \<equiv> a divides x \<and> b divides x \<and>
1.106 -                 (\<forall>y\<in>carrier G. (a divides y \<and> b divides y \<longrightarrow> x divides y))"
1.107 -
1.108 -constdefs (structure G)
1.109 +  where "x lcmof\<^bsub>G\<^esub> a b \<equiv> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
1.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))"
1.111 +
1.112 +definition
1.113    somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.114 -  "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof a b"
1.115 -
1.116 +  where "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b"
1.117 +
1.118 +definition
1.119    somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.120 -  "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
1.121 -
1.122 -constdefs (structure G)
1.123 +  where "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b"
1.124 +
1.125 +definition
1.126    "SomeGcd G A == inf (division_rel G) A"
1.127
1.128
```