# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1395319428 0
# Node ID 00112abe9b256c9343ac82fa76cea7275cd78b05
# Parent  18378a709991b1e33781a04fc32752805e88c789
fixing messy proofs

diff -r 18378a709991 -r 00112abe9b25 src/HOL/NSA/HLog.thy
--- a/src/HOL/NSA/HLog.thy	Thu Mar 20 09:47:43 2014 +0100
+++ b/src/HOL/NSA/HLog.thy	Thu Mar 20 12:43:48 2014 +0000
@@ -40,7 +40,7 @@
 by (transfer, simp)
 
 lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
-by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
+by (metis less_numeral_extra(3) powhr_gt_zero)
 
 lemma powhr_divide:
   "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
@@ -122,7 +122,7 @@
 apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
             HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
         simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
-          hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse)
+          hlog_as_starfun divide_inverse)
 done
 
 lemma hlog_HInfinite_as_starfun:
diff -r 18378a709991 -r 00112abe9b25 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Thu Mar 20 09:47:43 2014 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Thu Mar 20 12:43:48 2014 +0000
@@ -225,14 +225,6 @@
      "abs (star_n X) = star_n (%n. abs (X n))"
 by (simp only: star_abs_def starfun_star_n)
 
-subsection{*Misc Others*}
-
-lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
-by (auto)
-
-lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
-by auto
-
 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
 by (simp add: omega_def star_n_zero_num star_n_less)
 
diff -r 18378a709991 -r 00112abe9b25 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Thu Mar 20 09:47:43 2014 +0100
+++ b/src/HOL/NSA/NSA.thy	Thu Mar 20 12:43:48 2014 +0000
@@ -1084,13 +1084,8 @@
 lemma hypreal_of_real_isLub2:
       "isLub (UNIV :: real set) Q Y
        ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)"
-apply (simp add: isLub_def leastP_def)
-apply (auto simp add: hypreal_of_real_isUb_iff setge_def)
-apply (frule_tac x2 = x in isUbD2a [THEN SReal_iff [THEN iffD1], THEN exE])
- prefer 2 apply assumption
-apply (drule_tac x = xa in spec)
-apply (auto simp add: hypreal_of_real_isUb_iff)
-done
+apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
+by (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le)
 
 lemma hypreal_of_real_isLub_iff:
      "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
@@ -1119,12 +1114,6 @@
 done
 
 (* lemma about lubs *)
-lemma hypreal_isLub_unique:
-     "[| isLub R S x; isLub R S y |] ==> x = (y::hypreal)"
-apply (frule isLub_isUb)
-apply (frule_tac x = y in isLub_isUb)
-apply (blast intro!: order_antisym dest!: isLub_le_isUb)
-done
 
 lemma lemma_st_part_ub:
      "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
@@ -1141,19 +1130,9 @@
 apply (auto simp add: abs_less_iff)
 done
 
-lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} \<subseteq> Reals"
-by auto
-
 lemma lemma_st_part_lub:
      "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
-by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset)
-
-lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r \<le> t) = (r \<le> 0)"
-apply safe
-apply (drule_tac c = "-t" in add_left_mono)
-apply (drule_tac [2] c = t in add_left_mono)
-apply (auto simp add: add_assoc [symmetric])
-done
+by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict)
 
 lemma lemma_st_part_le1:
      "[| (x::hypreal) \<in> HFinite;  isLub Reals {s. s \<in> Reals & s < x} t;
@@ -1244,7 +1223,7 @@
 apply (frule isLubD1a [THEN Reals_minus])
 using Reals_add_cancel [of x "- t"] apply simp
 apply (drule_tac x = x in lemma_SReal_lub)
-apply (drule hypreal_isLub_unique, assumption, auto)
+apply (drule isLub_unique, assumption, auto)
 done
 
 lemma lemma_st_part_not_eq2:
@@ -1256,7 +1235,7 @@
 apply (frule isLubD1a)
 using Reals_add_cancel [of "- x" t] apply simp
 apply (drule_tac x = x in lemma_SReal_lub)
-apply (drule hypreal_isLub_unique, assumption, auto)
+apply (drule isLub_unique, assumption, auto)
 done
 
 lemma lemma_st_part_major:
@@ -1360,7 +1339,7 @@
   shows "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal"
 apply (auto intro: Infinitesimal_inverse_HFinite)
 apply (drule Infinitesimal_HFinite_mult2, assumption)
-apply (simp add: not_Infinitesimal_not_zero right_inverse)
+apply (simp add: not_Infinitesimal_not_zero)
 done
 
 lemma approx_inverse:
@@ -1802,9 +1781,7 @@
 done
 
 lemma st_SReal_eq: "x \<in> Reals ==> st x = x"
-apply (erule st_unique)
-apply (rule approx_refl)
-done
+  by (metis approx_refl st_unique) 
 
 lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
 by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
@@ -1912,13 +1889,7 @@
 done
 
 lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x \<le> y |] ==> st(x) \<le> st(y)"
-apply (frule HFinite_st_Infinitesimal_add)
-apply (rotate_tac 1)
-apply (frule HFinite_st_Infinitesimal_add, safe)
-apply (rule Infinitesimal_add_st_le_cancel)
-apply (rule_tac [3] x = ea and y = e in Infinitesimal_diff)
-apply (auto simp add: add_assoc [symmetric])
-done
+by (metis approx_le_bound approx_sym linear st_SReal st_approx_self st_part_Ex1)
 
 lemma st_zero_le: "[| 0 \<le> x;  x \<in> HFinite |] ==> 0 \<le> st x"
 apply (subst st_0 [symmetric])
@@ -1967,19 +1938,18 @@
 
 subsubsection {* @{term HInfinite} *}
 
-lemma lemma_Compl_eq: "- {n. u < norm (xa n)} = {n. norm (xa n) \<le> u}"
+lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}"
 by auto
 
-lemma lemma_Compl_eq2: "- {n. norm (xa n) < u} = {n. u \<le> norm (xa n)}"
+lemma lemma_Compl_eq2: "- {n. norm (f n) < u} = {n. u \<le> norm (f n)}"
 by auto
 
 lemma lemma_Int_eq1:
-     "{n. norm (xa n) \<le> u} Int {n. u \<le> norm (xa n)}
-          = {n. norm(xa n) = u}"
+     "{n. norm (f n) \<le> u} Int {n. u \<le> norm (f n)} = {n. norm(f n) = u}"
 by auto
 
 lemma lemma_FreeUltrafilterNat_one:
-     "{n. norm (xa n) = u} \<le> {n. norm (xa n) < u + (1::real)}"
+     "{n. norm (f n) = u} \<le> {n. norm (f n) < u + (1::real)}"
 by auto
 
 (*-------------------------------------
@@ -2146,7 +2116,7 @@
 theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
 apply (simp add: omega_def)
 apply (rule FreeUltrafilterNat_HInfinite)
-apply (simp (no_asm) add: real_norm_def real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
+apply (simp add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
 done
 
 (*-----------------------------------------------
@@ -2190,19 +2160,9 @@
 apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
 done
 
-lemma real_of_nat_inverse_eq_iff:
-     "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
-by (auto simp add: real_of_nat_Suc_gt_zero less_imp_neq [THEN not_sym])
-
-lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"
-apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff)
-apply (cut_tac x = "inverse u - 1" in lemma_finite_omega_set)
-apply (simp add: real_of_nat_Suc diff_eq_eq [symmetric] eq_commute)
-done
-
 lemma finite_inverse_real_of_posnat_ge_real:
      "0 < u ==> finite {n. u \<le> inverse(real(Suc n))}"
-by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_omega_set2 finite_inverse_real_of_posnat_gt_real)
+by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real)
 
 lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
      "0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
@@ -2214,17 +2174,14 @@
     by property of (free) ultrafilters
  --------------------------------------------------------------*)
 lemma Compl_le_inverse_eq:
-     "- {n. u \<le> inverse(real(Suc n))} =
-      {n. inverse(real(Suc n)) < u}"
-apply (auto dest!: order_le_less_trans simp add: linorder_not_le)
-done
+     "- {n. u \<le> inverse(real(Suc n))} = {n. inverse(real(Suc n)) < u}"
+by (auto dest!: order_le_less_trans simp add: linorder_not_le)
+
 
 lemma FreeUltrafilterNat_inverse_real_of_posnat:
      "0 < u ==>
       {n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
-apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
-apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_le_inverse_eq)
-done
+by (metis Compl_le_inverse_eq FreeUltrafilterNat.ultra inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
 
 text{* Example of an hypersequence (i.e. an extended standard sequence)
    whose term with an hypernatural suffix is an infinitesimal i.e.
@@ -2250,33 +2207,25 @@
 lemma real_seq_to_hypreal_Infinitesimal:
      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
      ==> star_n X - star_of x \<in> Infinitesimal"
-apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int intro: order_less_trans FreeUltrafilterNat.subset simp add: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)
-done
+unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
+by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int 
+         intro: order_less_trans FreeUltrafilterNat.subset)
 
 lemma real_seq_to_hypreal_approx:
      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
       ==> star_n X @= star_of x"
-apply (subst approx_minus_iff)
-apply (rule mem_infmal_iff [THEN subst])
-apply (erule real_seq_to_hypreal_Infinitesimal)
-done
+by (metis bex_Infinitesimal_iff real_seq_to_hypreal_Infinitesimal)
 
 lemma real_seq_to_hypreal_approx2:
      "\<forall>n. norm(x - X n) < inverse(real(Suc n))
                ==> star_n X @= star_of x"
-apply (rule real_seq_to_hypreal_approx)
-apply (subst norm_minus_cancel [symmetric])
-apply (simp del: norm_minus_cancel)
-done
+by (metis norm_minus_commute real_seq_to_hypreal_approx)
 
 lemma real_seq_to_hypreal_Infinitesimal2:
      "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
       ==> star_n X - star_n Y \<in> Infinitesimal"
-by (auto intro!: bexI
-         dest: FreeUltrafilterNat_inverse_real_of_posnat
-               FreeUltrafilterNat.Int
-         intro: order_less_trans FreeUltrafilterNat.subset
-         simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff
-                   star_n_inverse)
+unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
+by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat
+         intro: order_less_trans FreeUltrafilterNat.subset)
 
 end