author | huffman |
Thu, 14 Dec 2006 19:15:16 +0100 | |
changeset 21848 | b35faf14a89f |
parent 21839 | 54018ed3b99d |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title : CStar.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001 University of Edinburgh |
|
4 |
*) |
|
5 |
||
14407 | 6 |
header{*Star-transforms in NSA, Extending Sets of Complex Numbers |
7 |
and Complex Functions*} |
|
8 |
||
15131 | 9 |
theory CStar |
15140 | 10 |
imports NSCA |
15131 | 11 |
begin |
13957 | 12 |
|
14407 | 13 |
subsection{*Properties of the *-Transform Applied to Sets of Reals*} |
14 |
||
15 |
lemma STARC_hcomplex_of_complex_Int: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
16 |
"*s* X Int SComplex = hcomplex_of_complex ` X" |
21830 | 17 |
by (auto simp add: Standard_def) |
14407 | 18 |
|
19 |
lemma lemma_not_hcomplexA: |
|
20 |
"x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y" |
|
21 |
by auto |
|
22 |
||
23 |
subsection{*Theorems about Nonstandard Extensions of Functions*} |
|
24 |
||
21848 | 25 |
lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
26 |
by transfer (rule refl) |
14407 | 27 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
28 |
lemma starfunCR_cmod: "*f* cmod = hcmod" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
29 |
by transfer (rule refl) |
14407 | 30 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
31 |
subsection{*Internal Functions - Some Redundancy With *f* Now*} |
14407 | 32 |
|
33 |
(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **) |
|
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
34 |
(* |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
35 |
lemma starfun_n_diff: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
36 |
"( *fn* f) z - ( *fn* g) z = ( *fn* (%i x. f i x - g i x)) z" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
37 |
apply (cases z) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
38 |
apply (simp add: starfun_n star_n_diff) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
39 |
done |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
40 |
*) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
41 |
(** composition: ( *fn) o ( *gn) = *(fn o gn) **) |
14407 | 42 |
|
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
43 |
lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
44 |
by transfer (rule refl) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
45 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
46 |
lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
47 |
by transfer (rule refl) |
14407 | 48 |
|
49 |
lemma starfunC_eq_Re_Im_iff: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
50 |
"(( *f* f) x = z) = ((( *f* (%x. Re(f x))) x = hRe (z)) & |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
51 |
(( *f* (%x. Im(f x))) x = hIm (z)))" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
52 |
by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im) |
14407 | 53 |
|
54 |
lemma starfunC_approx_Re_Im_iff: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
19765
diff
changeset
|
55 |
"(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) & |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
56 |
(( *f* (%x. Im(f x))) x @= hIm (z)))" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
57 |
by (simp add: hcomplex_approx_iff starfun_Re starfun_Im) |
14407 | 58 |
|
59 |
end |