# HG changeset patch
# User huffman
# Date 1321513674 -3600
# Node ID 4849dbe6e3100c7311784a9253f573ccdd303125
# Parent  934866fc776c384bcffbff4f200a16fdc6ecb6c7
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'

diff -r 934866fc776c -r 4849dbe6e310 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Thu Nov 17 07:55:09 2011 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Thu Nov 17 08:07:54 2011 +0100
@@ -471,8 +471,8 @@
 by transfer (rule power_one_right)
 
 lemma hyperpow_two:
-  "\<And>r. (r::'a::monoid_mult star) pow ((1::hypnat) + (1::hypnat)) = r * r"
-by transfer simp
+  "\<And>r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r"
+by transfer (rule power2_eq_square)
 
 lemma hyperpow_gt_zero:
   "\<And>r n. (0::'a::{linordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
@@ -501,16 +501,16 @@
 by transfer (rule power_mult_distrib)
 
 lemma hyperpow_two_le [simp]:
-  "(0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow (1 + 1)"
+  "\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2"
 by (auto simp add: hyperpow_two zero_le_mult_iff)
 
 lemma hrabs_hyperpow_two [simp]:
-  "abs(x pow (1 + 1)) =
-   (x::'a::{monoid_mult,linordered_ring_strict} star) pow (1 + 1)"
+  "abs(x pow 2) =
+   (x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
 by (simp only: abs_of_nonneg hyperpow_two_le)
 
 lemma hyperpow_two_hrabs [simp]:
-  "abs(x::'a::{linordered_idom} star) pow (1 + 1)  = x pow (1 + 1)"
+  "abs(x::'a::{linordered_idom} star) pow 2 = x pow 2"
 by (simp add: hyperpow_hrabs)
 
 text{*The precondition could be weakened to @{term "0\<le>x"}*}
@@ -519,12 +519,12 @@
  by (simp add: mult_strict_mono order_less_imp_le)
 
 lemma hyperpow_two_gt_one:
-  "\<And>r::'a::{linordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
-by transfer (simp add: power_gt1 del: power_Suc)
+  "\<And>r::'a::{linordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow 2"
+by transfer simp
 
 lemma hyperpow_two_ge_one:
-  "\<And>r::'a::{linordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
-by transfer (simp add: one_le_power del: power_Suc)
+  "\<And>r::'a::{linordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow 2"
+by transfer (rule one_le_power)
 
 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
 apply (rule_tac y = "1 pow n" in order_trans)
@@ -532,8 +532,8 @@
 done
 
 lemma hyperpow_minus_one2 [simp]:
-     "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
-by transfer (subst power_mult, simp)
+     "\<And>n. -1 pow (2*n) = (1::hypreal)"
+by transfer (rule power_m1_even)
 
 lemma hyperpow_less_le:
      "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
diff -r 934866fc776c -r 4849dbe6e310 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Thu Nov 17 07:55:09 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy	Thu Nov 17 08:07:54 2011 +0100
@@ -1008,6 +1008,9 @@
 
 instance star :: (ring_char_0) ring_char_0 ..
 
+instance star :: (number_semiring) number_semiring
+by (intro_classes, simp only: star_number_def star_of_nat_def number_of_int)
+
 instance star :: (number_ring) number_ring
 by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)