# HG changeset patch # User huffman # Date 1166130566 -3600 # Node ID 74909ecaf20acbab248cee3348f69438ac55fa04 # Parent 42e9fd3ec1a385ff4f5c2c04e7cb607df51a3661 remove ultra tactic and redundant FreeUltrafilterNat lemmas diff -r 42e9fd3ec1a3 -r 74909ecaf20a src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Thu Dec 14 22:08:35 2006 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Thu Dec 14 22:09:26 2006 +0100 @@ -102,7 +102,7 @@ text{*Also, proof of various properties of @{term FreeUltrafilterNat}: an arbitrary free ultrafilter*} - +(* lemma FreeUltrafilterNat_Ex: "\U::nat set set. freeultrafilter U" by (rule nat_infinite [THEN freeultrafilter_Ex]) @@ -190,11 +190,12 @@ text{*One further property of our free ultrafilter*} + lemma FreeUltrafilterNat_Un: "X Un Y \ FreeUltrafilterNat ==> X \ FreeUltrafilterNat | Y \ FreeUltrafilterNat" by (auto, ultra) - +*) subsection{*Properties of @{term starrel}*} @@ -301,7 +302,7 @@ apply (simp add: omega_def) apply (simp add: star_of_def star_n_eq_iff) apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] - lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) + lemma_finite_omega_set [THEN FreeUltrafilterNat.finite]) done lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \ omega" @@ -320,7 +321,7 @@ lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\x. hypreal_of_real x = epsilon)" by (auto simp add: epsilon_def star_of_def star_n_eq_iff - lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite]) + lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite]) lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \ epsilon" by (insert not_ex_hypreal_of_real_eq_epsilon, auto) diff -r 42e9fd3ec1a3 -r 74909ecaf20a src/HOL/Hyperreal/HyperNat.thy --- a/src/HOL/Hyperreal/HyperNat.thy Thu Dec 14 22:08:35 2006 +0100 +++ b/src/HOL/Hyperreal/HyperNat.thy Thu Dec 14 22:09:26 2006 +0100 @@ -271,12 +271,10 @@ hypnat_omega_def: "whn = star_n (%n::nat. n)" lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \ whn" -by (simp add: hypnat_omega_def star_of_def star_n_eq_iff - FreeUltrafilterNat.finite) +by (simp add: hypnat_omega_def star_of_def star_n_eq_iff) lemma whn_neq_hypnat_of_nat: "whn \ hypnat_of_nat n" -by (simp add: hypnat_omega_def star_of_def star_n_eq_iff - FreeUltrafilterNat.finite) +by (simp add: hypnat_omega_def star_of_def star_n_eq_iff) lemma whn_not_Nats [simp]: "whn \ Nats" by (simp add: Nats_def image_def whn_neq_hypnat_of_nat) @@ -297,9 +295,10 @@ lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \ FreeUltrafilterNat" apply (insert finite_atMost [of m]) -apply (simp add: atMost_def) -apply (drule FreeUltrafilterNat_finite) -apply (drule FreeUltrafilterNat_Compl_mem, ultra) +apply (simp add: atMost_def) +apply (drule FreeUltrafilterNat.finite) +apply (drule FreeUltrafilterNat.not_memD) +apply (simp add: Collect_neg_eq [symmetric] linorder_not_le) done lemma Compl_Collect_le: "- {n::nat. N \ n} = {n. n < N}" @@ -341,16 +340,14 @@ ==> {n. N < f n} \ FreeUltrafilterNat" apply (induct_tac N) apply (drule_tac x = 0 in spec) -apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp) -apply (drule_tac x = "Suc n" in spec, ultra) +apply (rule ccontr, drule FreeUltrafilterNat.not_memD, drule FreeUltrafilterNat.Int, assumption, simp) +apply (drule_tac x = "Suc n" in spec) +apply (elim ultra, auto) done lemma HNatInfinite_iff: "HNatInfinite = {N. \n \ Nats. n < N}" -apply (auto simp add: HNatInfinite_def SHNat_eq hypnat_of_nat_eq) -apply (rule_tac x = x in star_cases) -apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma - simp add: star_n_less FreeUltrafilterNat_Compl_iff1 - star_n_eq_iff Collect_neg_eq [symmetric]) +apply (safe intro!: Nats_less_HNatInfinite) +apply (auto simp add: HNatInfinite_def) done diff -r 42e9fd3ec1a3 -r 74909ecaf20a src/HOL/Hyperreal/NSA.thy --- a/src/HOL/Hyperreal/NSA.thy Thu Dec 14 22:08:35 2006 +0100 +++ b/src/HOL/Hyperreal/NSA.thy Thu Dec 14 22:09:26 2006 +0100 @@ -1972,7 +1972,7 @@ apply (drule HInfinite_HFinite_iff [THEN iffD1]) apply (simp add: HFinite_FreeUltrafilterNat_iff) apply (rule allI, drule_tac x="u + 1" in spec) -apply (drule FreeUltrafilterNat_Compl_mem) +apply (drule FreeUltrafilterNat.not_memD) apply (simp add: Collect_neg_eq [symmetric] linorder_not_less) apply (erule ultra, simp) done @@ -1989,7 +1989,9 @@ apply (rule HInfinite_HFinite_iff [THEN iffD2]) apply (safe, drule HFinite_FreeUltrafilterNat, safe) apply (drule_tac x = u in spec) -apply ultra +apply (drule (1) FreeUltrafilterNat.Int) +apply (simp add: Collect_conj_eq [symmetric]) +apply (subgoal_tac "\n. \ (norm (X n) < u \ u < norm (X n))", auto) done lemma HInfinite_FreeUltrafilterNat_iff: @@ -2090,13 +2092,13 @@ lemma rabs_real_of_nat_le_real_FreeUltrafilterNat: "{n. abs(real n) \ u} \ FreeUltrafilterNat" -by (blast intro!: FreeUltrafilterNat_finite finite_rabs_real_of_nat_le_real) +by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real) lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \ FreeUltrafilterNat" -apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem) +apply (rule ccontr, drule FreeUltrafilterNat.not_memD) apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \ u}") prefer 2 apply force -apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat_finite]) +apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat.finite]) done (*-------------------------------------------------------------- @@ -2112,7 +2114,7 @@ lemma FreeUltrafilterNat_omega: "{n. u < real n} \ FreeUltrafilterNat" apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat) -apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_real_le_eq) +apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_real_le_eq) done theorem HInfinite_omega [simp]: "omega \ HInfinite" @@ -2187,7 +2189,7 @@ lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat: "0 < u ==> {n. u \ inverse(real(Suc n))} \ FreeUltrafilterNat" -by (blast intro!: FreeUltrafilterNat_finite finite_inverse_real_of_posnat_ge_real) +by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real) (*-------------------------------------------------------------- The complement of {n. u \ inverse(real(Suc n))} = @@ -2204,7 +2206,7 @@ "0 < u ==> {n. inverse(real(Suc n)) < u} \ FreeUltrafilterNat" apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat) -apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_le_inverse_eq) +apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_le_inverse_eq) done text{* Example where we get a hyperreal from a real sequence @@ -2220,7 +2222,7 @@ lemma real_seq_to_hypreal_Infinitesimal: "\n. norm(X n - x) < inverse(real(Suc n)) ==> star_n X - star_of x \ Infinitesimal" -apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse) +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 lemma real_seq_to_hypreal_approx: @@ -2244,8 +2246,8 @@ ==> star_n X - star_n Y \ Infinitesimal" by (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat - FreeUltrafilterNat_all FreeUltrafilterNat_Int - intro: order_less_trans FreeUltrafilterNat_subset + FreeUltrafilterNat.Int + intro: order_less_trans FreeUltrafilterNat.subset simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff star_n_inverse)