# HG changeset patch
# User huffman
# Date 1159374866 -7200
# Node ID 275f9bd2ead91c759158f93480b2ae21dfb63f60
# Parent  2ef8b7332b4f00963cbd929109a4862847a2214c
remove redundant lemmas

diff -r 2ef8b7332b4f -r 275f9bd2ead9 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Wed Sep 27 16:33:08 2006 +0200
+++ b/src/HOL/Complex/CLim.thy	Wed Sep 27 18:34:26 2006 +0200
@@ -985,6 +985,6 @@
 lemma CARAT_CDERIVD:
      "(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l
       ==> NSCDERIV f x :> l"
-by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq); 
+by (auto simp add: NSCDERIV_iff2 isNSContc_def starfun_if_eq); 
 
 end
diff -r 2ef8b7332b4f -r 275f9bd2ead9 src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Wed Sep 27 16:33:08 2006 +0200
+++ b/src/HOL/Complex/CStar.thy	Wed Sep 27 18:34:26 2006 +0200
@@ -12,12 +12,9 @@
 
 subsection{*Properties of the *-Transform Applied to Sets of Reals*}
 
-lemma STARC_SComplex_subset: "SComplex \<subseteq> *s* (UNIV:: complex set)"
-by simp
-
 lemma STARC_hcomplex_of_complex_Int:
      "*s* X Int SComplex = hcomplex_of_complex ` X"
-by (auto simp add: SComplex_def STAR_mem_iff)
+by (auto simp add: SComplex_def)
 
 lemma lemma_not_hcomplexA:
      "x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
@@ -25,13 +22,6 @@
 
 subsection{*Theorems about Nonstandard Extensions of Functions*}
 
-lemma cstarfun_if_eq:
-     "w \<noteq> hcomplex_of_complex x
-       ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w"
-apply (cases w)
-apply (simp add: star_of_def starfun star_n_eq_iff, ultra)
-done
-
 lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
 apply (cases Z)
 apply (simp add: hcpow starfun hypnat_of_nat_eq)
@@ -69,8 +59,4 @@
 apply (simp add: starfun hIm hRe approx_approx_iff)
 done
 
-lemma starfunC_Idfun_approx:
-    "x @= hcomplex_of_complex a ==> ( *f* (%x. x)) x @= hcomplex_of_complex  a"
-by simp
-
 end
diff -r 2ef8b7332b4f -r 275f9bd2ead9 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Wed Sep 27 16:33:08 2006 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Wed Sep 27 18:34:26 2006 +0200
@@ -58,7 +58,7 @@
 
 lemma NatStar_hypreal_of_real_Int:
      "*s* X Int Nats = hypnat_of_nat ` X"
-by (auto simp add: SHNat_eq STAR_mem_iff)
+by (auto simp add: SHNat_eq)
 
 lemma starset_starset_n_eq: "*s* X = *sn* (%n. X)"
 by (simp add: starset_n_starset)
diff -r 2ef8b7332b4f -r 275f9bd2ead9 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Wed Sep 27 16:33:08 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Wed Sep 27 18:34:26 2006 +0200
@@ -45,41 +45,11 @@
 
 subsection{*Properties of the Star-transform Applied to Sets of Reals*}
 
-lemma STAR_UNIV_set: "*s*(UNIV::'a set) = (UNIV::'a star set)"
-by (transfer UNIV_def, rule refl)
-
-lemma STAR_empty_set: "*s* {} = {}"
-by (transfer empty_def, rule refl)
-
-lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
-by (transfer Un_def, rule refl)
-
-lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
-by (transfer Int_def, rule refl)
-
-lemma STAR_Compl: "*s* -A = -( *s* A)"
-by (transfer Compl_def, rule refl)
-
-lemma STAR_mem_Compl: "!!x. x \<notin> *s* F ==> x : *s* (- F)"
-by (transfer Compl_def, simp)
-
-lemma STAR_diff: "*s* (A - B) = *s* A - *s* B"
-by (transfer set_diff_def, rule refl)
-
-lemma STAR_subset: "A <= B ==> *s* A <= *s* B"
-by (transfer subset_def, simp)
-
-lemma STAR_mem: "a \<in> A ==> star_of a : *s* A"
-by transfer
-
-lemma STAR_mem_iff: "(star_of x \<in> *s* A) = (x \<in> A)"
-by (transfer, rule refl)
-
 lemma STAR_star_of_image_subset: "star_of ` A <= *s* A"
-by (auto simp add: STAR_mem)
+by auto
 
 lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
-by (auto simp add: SReal_def STAR_mem_iff)
+by (auto simp add: SReal_def)
 
 lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> \<forall>y \<in> A. x \<noteq> hypreal_of_real y"
 by auto
@@ -100,7 +70,7 @@
 by transfer
 
 lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
-by (blast dest: STAR_subset)
+by (erule rev_subsetD, simp)
 
 text{*Nonstandard extension of a set (defined using a constant
    sequence) as a special case of an internal set*}
@@ -150,7 +120,7 @@
 
 lemma starfun:
       "( *f* f) (star_n X) = star_n (%n. f (X n))"
-by (simp add: starfun_def star_of_def Ifun_star_n)
+by (rule starfun_star_n)
 
 lemma starfun_if_eq:
      "!!w. w \<noteq> star_of x