src/HOL/Complex/NSCA.thy
 changeset 20724 a1a8ba09e0ea parent 20686 e3d2b881ed0f child 21404 eb85850d3eb7
```--- a/src/HOL/Complex/NSCA.thy	Wed Sep 27 02:07:34 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy	Wed Sep 27 03:04:35 2006 +0200
@@ -536,11 +536,17 @@
lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite"
by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]])

-lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
+lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y"
+apply (frule SComplex_subset_HFinite [THEN subsetD])
+apply (drule (1) approx_HFinite)
+apply (unfold stc_def)
apply (rule some_equality)
-apply (auto intro: SComplex_subset_HFinite [THEN subsetD])
-apply (blast dest: SComplex_approx_iff [THEN iffD1])
+apply (auto intro: approx_unique_complex)
+done
+
+lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
+apply (erule stc_unique)
+apply (rule approx_refl)
done

lemma stc_hcomplex_of_complex:
@@ -562,19 +568,14 @@

"[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x"
-apply (frule stc_SComplex_eq [THEN subst])
-prefer 2 apply assumption
-apply (frule SComplex_subset_HFinite [THEN subsetD])
-apply (frule Infinitesimal_subset_HFinite [THEN subsetD])
-apply (drule stc_SComplex_eq)
-apply (rule approx_stc_eq)
+apply (erule stc_unique)
done

"[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x"
+apply (erule stc_unique)
done

@@ -583,18 +584,7 @@

"[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)"
-apply (frule_tac x = y in HFinite_stc_Infinitesimal_add, safe)
-apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))")
-apply (drule_tac [2] sym, drule_tac [2] sym)
- prefer 2 apply simp
-apply (drule stc_SComplex)+
-done

lemma stc_number_of [simp]: "stc (number_of w) = number_of w"
by (rule SComplex_number_of [THEN stc_SComplex_eq])
@@ -606,46 +596,19 @@
by simp

lemma stc_minus: "y \<in> HFinite ==> stc(-y) = -stc(y)"
-apply (frule HFinite_minus_iff [THEN iffD2])
-done
+by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus)

lemma stc_diff:
"[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x-y) = stc(x) - stc(y)"
-apply (frule_tac y1 = y in stc_minus [symmetric])
-apply (drule_tac x1 = y in HFinite_minus_iff [THEN iffD2])
-done
+by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff SComplex_diff)

lemma stc_mult:
"[| x \<in> HFinite; y \<in> HFinite |]
==> stc (x * y) = stc(x) * stc(y)"
-apply (frule_tac x = y in HFinite_stc_Infinitesimal_add, safe)
-apply (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))")
-apply (drule_tac [2] sym, drule_tac [2] sym)
- prefer 2 apply simp
-apply (erule_tac V = "x = stc x + e" in thin_rl)
-apply (erule_tac V = "y = stc y + ea" in thin_rl)
-apply (drule stc_SComplex)+
-apply (blast intro!: SComplex_mult)
-apply (drule SComplex_subset_HFinite [THEN subsetD])+
-apply (blast intro!: lemma_st_mult)
-done
+by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite SComplex_mult)

lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0"
-apply (rule stc_zero [THEN subst])
-apply (rule approx_stc_eq)
-apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
-done

lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
by (fast intro: stc_Infinitesimal)
@@ -653,9 +616,8 @@
lemma stc_inverse:
"[| x \<in> HFinite; stc x \<noteq> 0 |]
==> stc(inverse x) = inverse (stc x)"
-apply (rule_tac c1 = "stc x" in hcomplex_mult_left_cancel [THEN iffD1])
-apply (auto simp add: stc_mult [symmetric] stc_not_Infinitesimal HFinite_inverse)
-apply (subst right_inverse, auto)
+apply (drule stc_not_Infinitesimal)
+apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse SComplex_inverse)
done

lemma stc_divide [simp]:
@@ -674,19 +636,15 @@

lemma SComplex_SReal_hcomplex_of_hypreal:
"x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
-by (auto simp add: SReal_def SComplex_def hcomplex_of_hypreal_def
+by (auto simp add: SReal_def Standard_def hcomplex_of_hypreal_def
simp del: star_of_of_real)

lemma stc_hcomplex_of_hypreal:
"z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
-apply (frule st_part_Ex, safe)
-apply (rule someI2)
-apply (auto intro: approx_sym)
-apply (drule HFinite_HFinite_hcomplex_of_hypreal)
-apply (frule stc_part_Ex, safe)
-apply (rule someI2)
-apply (auto intro: approx_sym intro!: approx_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal)
+apply (rule stc_unique)
+apply (rule SComplex_SReal_hcomplex_of_hypreal)
+apply (erule st_SReal)