32 const_syntax (HTML output) |
32 const_syntax (HTML output) |
33 omega ("\<omega>") |
33 omega ("\<omega>") |
34 epsilon ("\<epsilon>") |
34 epsilon ("\<epsilon>") |
35 |
35 |
36 |
36 |
|
37 subsection {* Real vector class instances *} |
|
38 |
|
39 instance star :: (scaleR) scaleR .. |
|
40 |
|
41 defs (overloaded) |
|
42 star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)" |
|
43 |
|
44 instance star :: (real_vector) real_vector |
|
45 proof |
|
46 fix a b :: real |
|
47 show "\<And>x y::'a star. a *# (x + y) = a *# x + a *# y" |
|
48 by transfer (rule scaleR_right_distrib) |
|
49 show "\<And>x::'a star. (a + b) *# x = a *# x + b *# x" |
|
50 by transfer (rule scaleR_left_distrib) |
|
51 show "\<And>x::'a star. (a * b) *# x = a *# b *# x" |
|
52 by transfer (rule scaleR_assoc) |
|
53 show "\<And>x::'a star. 1 *# x = x" |
|
54 by transfer (rule scaleR_one) |
|
55 qed |
|
56 |
|
57 instance star :: (real_algebra) real_algebra |
|
58 proof |
|
59 fix a :: real |
|
60 show "\<And>x y::'a star. a *# x * y = a *# (x * y)" |
|
61 by transfer (rule mult_scaleR_left) |
|
62 show "\<And>x y::'a star. x * a *# y = a *# (x * y)" |
|
63 by transfer (rule mult_scaleR_right) |
|
64 qed |
|
65 |
|
66 instance star :: (real_algebra_1) real_algebra_1 .. |
|
67 |
|
68 lemma star_of_real_def [transfer_unfold]: "of_real r \<equiv> star_of (of_real r)" |
|
69 by (rule eq_reflection, unfold of_real_def, transfer, rule refl) |
|
70 |
|
71 lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" |
|
72 by transfer (rule refl) |
|
73 |
|
74 |
37 subsection{*Existence of Free Ultrafilter over the Naturals*} |
75 subsection{*Existence of Free Ultrafilter over the Naturals*} |
38 |
76 |
39 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
77 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
40 an arbitrary free ultrafilter*} |
78 an arbitrary free ultrafilter*} |
41 |
79 |