author huffman Sat, 16 Sep 2006 19:12:54 +0200 changeset 20555 055d9a1bbddf parent 20554 c433e78d4203 child 20556 2e8227b81bf1
add instances for real_vector and real_algebra
```--- 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 ..
+
+  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}: ```