author | huffman |
Wed, 27 Sep 2006 18:34:26 +0200 | |
changeset 20732 | 275f9bd2ead9 |
parent 20559 | 2116b7a371c7 |
child 21830 | e38f0226e956 |
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" |
20732 | 17 |
by (auto simp add: SComplex_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 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
25 |
lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
26 |
apply (cases Z) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
27 |
apply (simp add: hcpow starfun hypnat_of_nat_eq) |
14407 | 28 |
done |
29 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
30 |
lemma starfunCR_cmod: "*f* cmod = hcmod" |
14407 | 31 |
apply (rule ext) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
32 |
apply (rule_tac x = x in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
33 |
apply (simp add: starfun hcmod) |
14407 | 34 |
done |
35 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
36 |
subsection{*Internal Functions - Some Redundancy With *f* Now*} |
14407 | 37 |
|
38 |
(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **) |
|
13957 | 39 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
40 |
lemma starfun_n_diff: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
41 |
"( *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
|
42 |
apply (cases z) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
43 |
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
|
44 |
done |
14407 | 45 |
|
46 |
(** composition: ( *fn) o ( *gn) = *(fn o gn) **) |
|
47 |
||
48 |
lemma starfunC_eq_Re_Im_iff: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
49 |
"(( *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
|
50 |
(( *f* (%x. Im(f x))) x = hIm (z)))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
51 |
apply (cases x, cases z) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
52 |
apply (auto simp add: starfun hIm hRe complex_Re_Im_cancel_iff star_n_eq_iff, ultra+) |
14407 | 53 |
done |
54 |
||
55 |
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
|
56 |
"(( *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
|
57 |
(( *f* (%x. Im(f x))) x @= hIm (z)))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
58 |
apply (cases x, cases z) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
19765
diff
changeset
|
59 |
apply (simp add: starfun hIm hRe approx_approx_iff) |
14407 | 60 |
done |
61 |
||
62 |
end |