eliminated old numerals;
authorwenzelm
Tue Oct 23 22:58:15 2001 +0200 (2001-10-23)
changeset 11914bca734def300
parent 11913 673d7bc6b9db
child 11915 df030220a2a8
eliminated old numerals;
src/HOL/Library/Ring_and_Field.thy
src/HOL/Library/Ring_and_Field_Example.thy
src/HOL/Library/While_Combinator.thy
     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.78    by (simp add: divide_inverse)
    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