author huffman Wed, 13 Dec 2006 19:05:45 +0100 changeset 21830 e38f0226e956 parent 21829 016eff9c5699 child 21831 1897fe3d72d5
SComplex abbreviates Standard
 src/HOL/Complex/CStar.thy file | annotate | diff | comparison | revisions src/HOL/Complex/NSCA.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Complex/CStar.thy	Wed Dec 13 16:33:11 2006 +0100
+++ b/src/HOL/Complex/CStar.thy	Wed Dec 13 19:05:45 2006 +0100
@@ -14,7 +14,7 @@

lemma STARC_hcomplex_of_complex_Int:
"*s* X Int SComplex = hcomplex_of_complex ` X"

lemma lemma_not_hcomplexA:
"x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"```
```--- a/src/HOL/Complex/NSCA.thy	Wed Dec 13 16:33:11 2006 +0100
+++ b/src/HOL/Complex/NSCA.thy	Wed Dec 13 19:05:45 2006 +0100
@@ -9,10 +9,10 @@
imports NSComplex
begin

-definition
+abbreviation
(* standard complex numbers reagarded as an embedded subset of NS complex *)
SComplex  :: "hcomplex set" where
-   "SComplex = {x. \<exists>r. x = hcomplex_of_complex r}"
+   "SComplex \<equiv> Standard"

definition
stc :: "hcomplex => hcomplex" where
@@ -23,36 +23,27 @@
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}

lemma SComplex_add: "[| x \<in> SComplex; y \<in> SComplex |] ==> x + y \<in> SComplex"
-apply (rule_tac x = "r + ra" in exI, simp)
-done

lemma SComplex_mult: "[| x \<in> SComplex; y \<in> SComplex |] ==> x * y \<in> SComplex"
-apply (rule_tac x = "r * ra" in exI, simp)
-done
+by (rule Standard_mult)

lemma SComplex_inverse: "x \<in> SComplex ==> inverse x \<in> SComplex"
-apply (blast intro: star_of_inverse [symmetric])
-done
+by (rule Standard_inverse)

lemma SComplex_divide: "[| x \<in> SComplex;  y \<in> SComplex |] ==> x/y \<in> SComplex"
-by (simp add: SComplex_mult SComplex_inverse divide_inverse)
+by (rule Standard_divide)

lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
-apply (blast intro: star_of_minus [symmetric])
-done
+by (rule Standard_minus)

lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
apply auto
-apply (erule_tac [2] SComplex_minus)
apply (drule SComplex_minus, auto)
done

lemma SComplex_diff: "[| x \<in> SComplex; y \<in> SComplex |] ==> x - y \<in> SComplex"
+by (rule Standard_diff)

"[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"
@@ -60,7 +51,7 @@

lemma SReal_hcmod_hcomplex_of_complex [simp]:
"hcmod (hcomplex_of_complex r) \<in> Reals"
-by (auto simp add: hcmod SReal_def star_of_def)

lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals"
apply (subst star_of_number_of [symmetric])
@@ -68,41 +59,37 @@
done

lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
-
-lemma SComplex_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> SComplex"

-lemma SComplex_number_of [simp]: "(number_of w ::hcomplex) \<in> SComplex"
-apply (subst star_of_number_of [symmetric])
-apply (rule SComplex_hcomplex_of_complex)
-done
+lemma SComplex_hcomplex_of_complex: "hcomplex_of_complex x \<in> SComplex"
+by (rule Standard_star_of)
+
+lemma SComplex_number_of: "(number_of w ::hcomplex) \<in> SComplex"
+by (rule Standard_number_of)

lemma SComplex_divide_number_of:
"r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
-apply (simp only: divide_inverse)
-apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
-done
+by simp

lemma SComplex_UNIV_complex:
"{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
+by simp

lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"

lemma hcomplex_of_complex_image:
"hcomplex_of_complex `(UNIV::complex set) = SComplex"

lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
+apply (auto simp add: Standard_def image_def)
apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast)
done

lemma SComplex_hcomplex_of_complex_image:
"[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q"
done

lemma SComplex_SReal_dense:
@@ -113,13 +100,13 @@

lemma SComplex_hcmod_SReal:
"z \<in> SComplex ==> hcmod z \<in> Reals"

-lemma SComplex_zero [simp]: "0 \<in> SComplex"
+lemma SComplex_zero: "0 \<in> SComplex"
+by (rule Standard_zero)

-lemma SComplex_one [simp]: "1 \<in> SComplex"
+lemma SComplex_one: "1 \<in> SComplex"
+by (rule Standard_one)

(*
Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> SComplex"
@@ -132,7 +119,7 @@
subsection{*The Finite Elements form a Subring*}

lemma SComplex_subset_HFinite [simp]: "SComplex \<le> HFinite"

lemma HFinite_hcmod_hcomplex_of_complex [simp]:
"hcmod (hcomplex_of_complex r) \<in> HFinite"
@@ -274,7 +261,7 @@
by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff)

lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}"
-by (auto simp add: SComplex_def Infinitesimal_hcmod_iff)
+by (auto simp add: Standard_def Infinitesimal_hcmod_iff)

lemma SComplex_Infinitesimal_zero:
"[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0"
@@ -303,7 +290,7 @@

lemma SComplex_approx_iff:
"[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)"

lemma number_of_Infinitesimal_iff [simp]:
"((number_of w :: hcomplex) \<in> Infinitesimal) =
@@ -441,22 +428,22 @@
lemma SComplex_Re_SReal:
"star_n X \<in> SComplex
==> star_n (%n. Re(X n)) \<in> Reals"
-apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff)
-apply (rule_tac x = "Re r" in exI, ultra)
+apply (auto simp add: Standard_def SReal_def star_of_def star_n_eq_iff)
+apply (rule_tac x = "Re x" in exI, ultra)
done

lemma SComplex_Im_SReal:
"star_n X \<in> SComplex
==> star_n (%n. Im(X n)) \<in> Reals"
-apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff)
-apply (rule_tac x = "Im r" in exI, ultra)
+apply (auto simp add: Standard_def SReal_def star_of_def star_n_eq_iff)
+apply (rule_tac x = "Im x" in exI, ultra)
done

lemma Reals_Re_Im_SComplex:
"[| star_n (%n. Re(X n)) \<in> Reals;
star_n (%n. Im(X n)) \<in> Reals
|] ==> star_n X \<in> SComplex"
-apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff)
+apply (auto simp add: Standard_def image_def SReal_def star_of_def star_n_eq_iff)
apply (rule_tac x = "Complex r ra" in exI, ultra)
done
```