author wenzelm Tue Oct 23 22:58:15 2001 +0200 (2001-10-23) changeset 11914 bca734def300 parent 11913 673d7bc6b9db child 11915 df030220a2a8
eliminated old numerals;
```     1.1 --- a/src/HOL/Library/Ring_and_Field.thy	Tue Oct 23 22:57:52 2001 +0200
1.2 +++ b/src/HOL/Library/Ring_and_Field.thy	Tue Oct 23 22:58:15 2001 +0200
1.3 @@ -13,17 +13,16 @@
1.4
1.5  subsection {* Abstract algebraic structures *}
1.6
1.7 -axclass ring \<subseteq> zero, plus, minus, times, number
1.8 +axclass ring \<subseteq> zero, one, plus, minus, times
1.9    add_assoc: "(a + b) + c = a + (b + c)"
1.10    add_commute: "a + b = b + a"
1.11    left_zero [simp]: "0 + a = a"
1.12    left_minus [simp]: "- a + a = 0"
1.13    diff_minus: "a - b = a + (-b)"
1.14 -  zero_number: "0 = Numeral0"
1.15
1.16    mult_assoc: "(a * b) * c = a * (b * c)"
1.17    mult_commute: "a * b = b * a"
1.18 -  left_one [simp]: "Numeral1 * a = a"
1.19 +  left_one [simp]: "1 * a = a"
1.20
1.21    left_distrib: "(a + b) * c = a * c + b * c"
1.22
1.23 @@ -33,7 +32,7 @@
1.24    abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
1.25
1.26  axclass field \<subseteq> ring, inverse
1.27 -  left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = Numeral1"
1.28 +  left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
1.29    divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
1.30
1.31  axclass ordered_field \<subseteq> ordered_ring, field
1.32 @@ -87,10 +86,10 @@
1.33
1.34  subsubsection {* Derived rules for multiplication *}
1.35
1.36 -lemma right_one [simp]: "a = a * (Numeral1::'a::field)"
1.37 +lemma right_one [simp]: "a = a * (1::'a::field)"
1.38  proof -
1.39 -  have "a = Numeral1 * a" by simp
1.40 -  also have "... = a * Numeral1" by (simp add: mult_commute)
1.41 +  have "a = 1 * a" by simp
1.42 +  also have "... = a * 1" by (simp add: mult_commute)
1.43    finally show ?thesis .
1.44  qed
1.45
1.46 @@ -103,28 +102,28 @@
1.47
1.48  theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute
1.49
1.50 -lemma right_inverse [simp]: "a \<noteq> 0 ==>  a * inverse (a::'a::field) = Numeral1"
1.51 +lemma right_inverse [simp]: "a \<noteq> 0 ==>  a * inverse (a::'a::field) = 1"
1.52  proof -
1.53    have "a * inverse a = inverse a * a" by (simp add: ring_mult_ac)
1.54    also assume "a \<noteq> 0"
1.55 -  hence "inverse a * a = Numeral1" by simp
1.56 +  hence "inverse a * a = 1" by simp
1.57    finally show ?thesis .
1.58  qed
1.59
1.60 -lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = Numeral1) = (a = (b::'a::field))"
1.61 +lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
1.62  proof
1.63    assume neq: "b \<noteq> 0"
1.64    {
1.65      hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac)
1.66 -    also assume "a / b = Numeral1"
1.67 +    also assume "a / b = 1"
1.68      finally show "a = b" by simp
1.69    next
1.70      assume "a = b"
1.71 -    with neq show "a / b = Numeral1" by (simp add: divide_inverse)
1.72 +    with neq show "a / b = 1" by (simp add: divide_inverse)
1.73    }
1.74  qed
1.75
1.76 -lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = Numeral1"
1.77 +lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
1.79
1.80
```
```     2.1 --- a/src/HOL/Library/Ring_and_Field_Example.thy	Tue Oct 23 22:57:52 2001 +0200
2.2 +++ b/src/HOL/Library/Ring_and_Field_Example.thy	Tue Oct 23 22:58:15 2001 +0200
2.3 @@ -13,8 +13,7 @@
2.4    show "i - j = i + (-j)" by simp
2.5    show "(i * j) * k = i * (j * k)" by simp
2.6    show "i * j = j * i" by simp
2.7 -  show "Numeral1 * i = i" by simp
2.8 -  show "0 = (Numeral0::int)" by simp
2.9 +  show "1 * i = i" by simp
2.10    show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
2.11    show "i \<le> j ==> k + i \<le> k + j" by simp
2.12    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
```
```     3.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Oct 23 22:57:52 2001 +0200
3.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Oct 23 22:58:15 2001 +0200
3.3 @@ -135,14 +135,13 @@
3.4   theory.}
3.5  *}
3.6
3.7 -theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
3.8 -    P {Numeral0, 4, 2}"
3.9 +theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}"
3.10  proof -
3.11    have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
3.12      apply blast
3.13      done
3.14    show ?thesis
3.15 -    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
3.16 +    apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"])
3.17         apply (rule monoI)
3.18        apply blast
3.19       apply simp
```