# HG changeset patch
# User huffman
# Date 1158426774 -7200
# Node ID 055d9a1bbddf8cd874a048c8f2f61984c90a92a1
# Parent  c433e78d4203a880581c24b6ef025af2edaa9d16
add instances for real_vector and real_algebra

diff -r c433e78d4203 -r 055d9a1bbddf src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Sat Sep 16 19:12:03 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Sat Sep 16 19:12:54 2006 +0200
@@ -34,6 +34,44 @@
   epsilon  ("\<epsilon>")
 
 
+subsection {* Real vector class instances *}
+
+instance star :: (scaleR) scaleR ..
+
+defs (overloaded)
+  star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
+
+instance star :: (real_vector) real_vector
+proof
+  fix a b :: real
+  show "\<And>x y::'a star. a *# (x + y) = a *# x + a *# y"
+    by transfer (rule scaleR_right_distrib)
+  show "\<And>x::'a star. (a + b) *# x = a *# x + b *# x"
+    by transfer (rule scaleR_left_distrib)
+  show "\<And>x::'a star. (a * b) *# x = a *# b *# x"
+    by transfer (rule scaleR_assoc)
+  show "\<And>x::'a star. 1 *# x = x"
+    by transfer (rule scaleR_one)
+qed
+
+instance star :: (real_algebra) real_algebra
+proof
+  fix a :: real
+  show "\<And>x y::'a star. a *# x * y = a *# (x * y)"
+    by transfer (rule mult_scaleR_left)
+  show "\<And>x y::'a star. x * a *# y = a *# (x * y)"
+    by transfer (rule mult_scaleR_right)
+qed
+
+instance star :: (real_algebra_1) real_algebra_1 ..
+
+lemma star_of_real_def [transfer_unfold]: "of_real r \<equiv> star_of (of_real r)"
+by (rule eq_reflection, unfold of_real_def, transfer, rule refl)
+
+lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r"
+by transfer (rule refl)
+
+
 subsection{*Existence of Free Ultrafilter over the Naturals*}
 
 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: