# HG changeset patch
# User wenzelm
# Date 1003870695 -7200
# Node ID bca734def300a0df278028a2cee6c0a7ba858444
# Parent  673d7bc6b9db5d8d953acef7875f058acbad3d2a
eliminated old numerals;

diff -r 673d7bc6b9db -r bca734def300 src/HOL/Library/Ring_and_Field.thy
--- a/src/HOL/Library/Ring_and_Field.thy	Tue Oct 23 22:57:52 2001 +0200
+++ b/src/HOL/Library/Ring_and_Field.thy	Tue Oct 23 22:58:15 2001 +0200
@@ -13,17 +13,16 @@
 
 subsection {* Abstract algebraic structures *}
 
-axclass ring \<subseteq> zero, plus, minus, times, number
+axclass ring \<subseteq> zero, one, plus, minus, times
   add_assoc: "(a + b) + c = a + (b + c)"
   add_commute: "a + b = b + a"
   left_zero [simp]: "0 + a = a"
   left_minus [simp]: "- a + a = 0"
   diff_minus: "a - b = a + (-b)"
-  zero_number: "0 = Numeral0"
 
   mult_assoc: "(a * b) * c = a * (b * c)"
   mult_commute: "a * b = b * a"
-  left_one [simp]: "Numeral1 * a = a"
+  left_one [simp]: "1 * a = a"
 
   left_distrib: "(a + b) * c = a * c + b * c"
 
@@ -33,7 +32,7 @@
   abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
 
 axclass field \<subseteq> ring, inverse
-  left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = Numeral1"
+  left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
   divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
 
 axclass ordered_field \<subseteq> ordered_ring, field
@@ -87,10 +86,10 @@
 
 subsubsection {* Derived rules for multiplication *}
 
-lemma right_one [simp]: "a = a * (Numeral1::'a::field)"
+lemma right_one [simp]: "a = a * (1::'a::field)"
 proof -
-  have "a = Numeral1 * a" by simp
-  also have "... = a * Numeral1" by (simp add: mult_commute)
+  have "a = 1 * a" by simp
+  also have "... = a * 1" by (simp add: mult_commute)
   finally show ?thesis .
 qed
 
@@ -103,28 +102,28 @@
 
 theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute
 
-lemma right_inverse [simp]: "a \<noteq> 0 ==>  a * inverse (a::'a::field) = Numeral1" 
+lemma right_inverse [simp]: "a \<noteq> 0 ==>  a * inverse (a::'a::field) = 1" 
 proof -
   have "a * inverse a = inverse a * a" by (simp add: ring_mult_ac)
   also assume "a \<noteq> 0"
-  hence "inverse a * a = Numeral1" by simp
+  hence "inverse a * a = 1" by simp
   finally show ?thesis .
 qed
 
-lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = Numeral1) = (a = (b::'a::field))"
+lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
 proof 
   assume neq: "b \<noteq> 0"
   {
     hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac)
-    also assume "a / b = Numeral1"
+    also assume "a / b = 1"
     finally show "a = b" by simp
   next
     assume "a = b"
-    with neq show "a / b = Numeral1" by (simp add: divide_inverse)
+    with neq show "a / b = 1" by (simp add: divide_inverse)
   }
 qed
 
-lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = Numeral1"
+lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   by (simp add: divide_inverse)
 
 
diff -r 673d7bc6b9db -r bca734def300 src/HOL/Library/Ring_and_Field_Example.thy
--- a/src/HOL/Library/Ring_and_Field_Example.thy	Tue Oct 23 22:57:52 2001 +0200
+++ b/src/HOL/Library/Ring_and_Field_Example.thy	Tue Oct 23 22:58:15 2001 +0200
@@ -13,8 +13,7 @@
   show "i - j = i + (-j)" by simp
   show "(i * j) * k = i * (j * k)" by simp
   show "i * j = j * i" by simp
-  show "Numeral1 * i = i" by simp
-  show "0 = (Numeral0::int)" by simp
+  show "1 * i = i" by simp
   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
   show "i \<le> j ==> k + i \<le> k + j" by simp
   show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
diff -r 673d7bc6b9db -r bca734def300 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Oct 23 22:57:52 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Tue Oct 23 22:58:15 2001 +0200
@@ -135,14 +135,13 @@
  theory.}
 *}
 
-theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
-    P {Numeral0, 4, 2}"
+theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}"
 proof -
   have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
     apply blast
     done
   show ?thesis
-    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
+    apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"])
        apply (rule monoI)
       apply blast
      apply simp