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