renamed axclass_xxxx axclasses;
authorwenzelm
Wed Sep 20 00:24:24 2006 +0200 (2006-09-20 ago)
changeset 20633e98f59806244
parent 20632 40abbc7c86df
child 20634 45fe31e72391
renamed axclass_xxxx axclasses;
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Hyperreal/NSA.thy	Tue Sep 19 23:18:41 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Sep 20 00:24:24 2006 +0200
     1.3 @@ -954,7 +954,7 @@
     1.4  
     1.5  (*again: 1 is a special case, but not 0 this time*)
     1.6  lemma one_not_Infinitesimal [simp]:
     1.7 -  "(1::'a::{real_normed_vector,axclass_0_neq_1} star) \<notin> Infinitesimal"
     1.8 +  "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal"
     1.9  apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
    1.10  apply simp
    1.11  done
    1.12 @@ -1032,8 +1032,8 @@
    1.13     (number_of w = (1::'b))"
    1.14    "((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
    1.15     (number_of w = (1::'b))"
    1.16 -  "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
    1.17 -  "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
    1.18 +  "~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))"
    1.19 +  "~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))"
    1.20  apply (unfold star_number_def star_zero_def star_one_def)
    1.21  apply (unfold star_of_approx_iff)
    1.22  by (auto intro: sym)
     2.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Tue Sep 19 23:18:41 2006 +0200
     2.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Wed Sep 20 00:24:24 2006 +0200
     2.3 @@ -283,13 +283,13 @@
     2.4  instance star :: (comm_semiring_0) comm_semiring_0 ..
     2.5  instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
     2.6  
     2.7 -instance star :: (axclass_0_neq_1) axclass_0_neq_1
     2.8 +instance star :: (zero_neq_one) zero_neq_one
     2.9  by (intro_classes, transfer, rule zero_neq_one)
    2.10  
    2.11  instance star :: (semiring_1) semiring_1 ..
    2.12  instance star :: (comm_semiring_1) comm_semiring_1 ..
    2.13  
    2.14 -instance star :: (axclass_no_zero_divisors) axclass_no_zero_divisors
    2.15 +instance star :: (no_zero_divisors) no_zero_divisors
    2.16  by (intro_classes, transfer, rule no_zero_divisors)
    2.17  
    2.18  instance star :: (semiring_1_cancel) semiring_1_cancel ..
    2.19 @@ -340,7 +340,7 @@
    2.20  instance star :: (pordered_ring) pordered_ring ..
    2.21  instance star :: (lordered_ring) lordered_ring ..
    2.22  
    2.23 -instance star :: (axclass_abs_if) axclass_abs_if
    2.24 +instance star :: (abs_if) abs_if
    2.25  by (intro_classes, transfer, rule abs_if)
    2.26  
    2.27  instance star :: (ordered_ring_strict) ordered_ring_strict ..
     3.1 --- a/src/HOL/Matrix/Matrix.thy	Tue Sep 19 23:18:41 2006 +0200
     3.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Sep 20 00:24:24 2006 +0200
     3.3 @@ -132,14 +132,14 @@
     3.4  apply (rule exI[of _ n], simp add: split_if)+
     3.5  by (simp add: split_if)
     3.6  
     3.7 -lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
     3.8 +lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
     3.9  proof -
    3.10    have "?r <= n" by (simp add: nrows_le)
    3.11    moreover have "n <= ?r" by (simp add:le_nrows, arith)
    3.12    ultimately show "?r = n" by simp
    3.13  qed
    3.14  
    3.15 -lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
    3.16 +lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
    3.17  proof -
    3.18    have "?r <= n" by (simp add: ncols_le)
    3.19    moreover have "n <= ?r" by (simp add: le_ncols, arith)
     4.1 --- a/src/HOL/Ring_and_Field.thy	Tue Sep 19 23:18:41 2006 +0200
     4.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Sep 20 00:24:24 2006 +0200
     4.3 @@ -241,10 +241,10 @@
     4.4  
     4.5  instance lordered_ring \<subseteq> lordered_ab_group_join ..
     4.6  
     4.7 -axclass axclass_abs_if \<subseteq> minus, ord, zero
     4.8 +axclass abs_if \<subseteq> minus, ord, zero
     4.9    abs_if: "abs a = (if (a < 0) then (-a) else a)"
    4.10  
    4.11 -axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, axclass_abs_if
    4.12 +axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, abs_if
    4.13  
    4.14  instance ordered_ring_strict \<subseteq> lordered_ab_group ..
    4.15  
    4.16 @@ -256,7 +256,7 @@
    4.17  axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)
    4.18    zero_less_one [simp]: "0 < 1"
    4.19  
    4.20 -axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, axclass_abs_if (* previously ordered_ring *)
    4.21 +axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, abs_if (* previously ordered_ring *)
    4.22  
    4.23  instance ordered_idom \<subseteq> ordered_ring_strict ..
    4.24