# HG changeset patch
# User huffman
# Date 1162942455 -3600
# Node ID c46bc715bdfd9e86cb939232bc0239114b4b9ef4
# Parent  b803f9870e97a581c801343fd7f3d69bca8d5aaf
generalized types of of_nat and of_int to work with non-commutative types

diff -r b803f9870e97 -r c46bc715bdfd src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Nov 07 22:06:32 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Wed Nov 08 00:34:15 2006 +0100
@@ -564,7 +564,7 @@
 subsection{*The Set of Natural Numbers*}
 
 constdefs
-  Nats  :: "'a::comm_semiring_1_cancel set"
+  Nats  :: "'a::semiring_1_cancel set"
   "Nats == range of_nat"
 
 notation (xsymbols)
@@ -611,11 +611,11 @@
 qed
 
 
-subsection{*Embedding of the Integers into any @{text comm_ring_1}:
+subsection{*Embedding of the Integers into any @{text ring_1}:
 @{term of_int}*}
 
 constdefs
-   of_int :: "int => 'a::comm_ring_1"
+   of_int :: "int => 'a::ring_1"
    "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 
 
@@ -673,7 +673,7 @@
 declare of_int_0_less_iff [simp]
 declare of_int_less_0_iff [simp]
 
-text{*The ordering on the @{text comm_ring_1} is necessary.
+text{*The ordering on the @{text ring_1} is necessary.
  See @{text of_nat_eq_iff} above.*}
 lemma of_int_eq_iff [simp]:
      "(of_int w = (of_int z::'a::ordered_idom)) = (w = z)"
@@ -697,7 +697,7 @@
 subsection{*The Set of Integers*}
 
 constdefs
-  Ints  :: "'a::comm_ring_1 set"
+  Ints  :: "'a::ring_1 set"
   "Ints == range of_int"
 
 notation (xsymbols)
diff -r b803f9870e97 -r c46bc715bdfd src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Tue Nov 07 22:06:32 2006 +0100
+++ b/src/HOL/NatArith.thy	Wed Nov 08 00:34:15 2006 +0100
@@ -164,9 +164,9 @@
 *}
 
 subsection{*Embedding of the Naturals into any @{text
-comm_semiring_1_cancel}: @{term of_nat}*}
+semiring_1_cancel}: @{term of_nat}*}
 
-consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
+consts of_nat :: "nat => 'a::semiring_1_cancel"
 
 primrec
   of_nat_0:   "of_nat 0 = 0"
@@ -182,7 +182,7 @@
 
 lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
 apply (induct m)
-apply (simp_all add: mult_ac add_ac right_distrib)
+apply (simp_all add: add_ac left_distrib)
 done
 
 lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
@@ -224,7 +224,7 @@
 declare of_nat_0_le_iff [simp]
 declare of_nat_le_0_iff [simp]
 
-text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
+text{*The ordering on the @{text semiring_1_cancel} is necessary
 to exclude the possibility of a finite field, which indeed wraps back to
 zero.*}
 lemma of_nat_eq_iff [simp]:
@@ -238,7 +238,7 @@
 declare of_nat_eq_0_iff [simp]
 
 lemma of_nat_diff [simp]:
-     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
+     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
 by (simp del: of_nat_add
 	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)