author wenzelm Wed, 20 Sep 2006 00:24:24 +0200 changeset 20633 e98f59806244 parent 20632 40abbc7c86df child 20634 45fe31e72391
renamed axclass_xxxx axclasses;
 src/HOL/Hyperreal/NSA.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/StarClasses.thy file | annotate | diff | comparison | revisions src/HOL/Matrix/Matrix.thy file | annotate | diff | comparison | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hyperreal/NSA.thy	Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Sep 20 00:24:24 2006 +0200
@@ -954,7 +954,7 @@

(*again: 1 is a special case, but not 0 this time*)
lemma one_not_Infinitesimal [simp]:
-  "(1::'a::{real_normed_vector,axclass_0_neq_1} star) \<notin> Infinitesimal"
+  "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal"
apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
apply simp
done
@@ -1032,8 +1032,8 @@
(number_of w = (1::'b))"
"((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
(number_of w = (1::'b))"
-  "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
-  "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
+  "~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))"
+  "~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))"
apply (unfold star_number_def star_zero_def star_one_def)
apply (unfold star_of_approx_iff)
by (auto intro: sym)```
```--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Wed Sep 20 00:24:24 2006 +0200
@@ -283,13 +283,13 @@
instance star :: (comm_semiring_0) comm_semiring_0 ..
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..

-instance star :: (axclass_0_neq_1) axclass_0_neq_1
+instance star :: (zero_neq_one) zero_neq_one
by (intro_classes, transfer, rule zero_neq_one)

instance star :: (semiring_1) semiring_1 ..
instance star :: (comm_semiring_1) comm_semiring_1 ..

-instance star :: (axclass_no_zero_divisors) axclass_no_zero_divisors
+instance star :: (no_zero_divisors) no_zero_divisors
by (intro_classes, transfer, rule no_zero_divisors)

instance star :: (semiring_1_cancel) semiring_1_cancel ..
@@ -340,7 +340,7 @@
instance star :: (pordered_ring) pordered_ring ..
instance star :: (lordered_ring) lordered_ring ..

-instance star :: (axclass_abs_if) axclass_abs_if
+instance star :: (abs_if) abs_if
by (intro_classes, transfer, rule abs_if)

instance star :: (ordered_ring_strict) ordered_ring_strict ..```
```--- a/src/HOL/Matrix/Matrix.thy	Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Wed Sep 20 00:24:24 2006 +0200
@@ -132,14 +132,14 @@
apply (rule exI[of _ n], simp add: split_if)+

-lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
+lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
proof -
have "?r <= n" by (simp add: nrows_le)
moreover have "n <= ?r" by (simp add:le_nrows, arith)
ultimately show "?r = n" by simp
qed

-lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
+lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
proof -
have "?r <= n" by (simp add: ncols_le)
moreover have "n <= ?r" by (simp add: le_ncols, arith)```
```--- a/src/HOL/Ring_and_Field.thy	Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Ring_and_Field.thy	Wed Sep 20 00:24:24 2006 +0200
@@ -241,10 +241,10 @@

instance lordered_ring \<subseteq> lordered_ab_group_join ..

-axclass axclass_abs_if \<subseteq> minus, ord, zero
+axclass abs_if \<subseteq> minus, ord, zero
abs_if: "abs a = (if (a < 0) then (-a) else a)"

-axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, axclass_abs_if
+axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, abs_if

instance ordered_ring_strict \<subseteq> lordered_ab_group ..

@@ -256,7 +256,7 @@
axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)
zero_less_one [simp]: "0 < 1"

-axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, axclass_abs_if (* previously ordered_ring *)
+axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, abs_if (* previously ordered_ring *)

instance ordered_idom \<subseteq> ordered_ring_strict ..
```