src/HOL/Hyperreal/NSA.thy
changeset 14468 6be497cacab5
parent 14430 5cb24165a2e1
child 14477 cc61fd03e589
equal deleted inserted replaced
14467:bbfa6b01a55f 14468:6be497cacab5
  1846 by (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
  1846 by (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
  1847 
  1847 
  1848 lemma HFinite_FreeUltrafilterNat:
  1848 lemma HFinite_FreeUltrafilterNat:
  1849     "x \<in> HFinite 
  1849     "x \<in> HFinite 
  1850      ==> \<exists>X \<in> Rep_hypreal x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
  1850      ==> \<exists>X \<in> Rep_hypreal x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
  1851 apply (rule eq_Abs_hypreal [of x])
  1851 apply (cases x)
  1852 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] 
  1852 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] 
  1853               hypreal_less SReal_iff hypreal_minus hypreal_of_real_def)
  1853               hypreal_less SReal_iff hypreal_minus hypreal_of_real_def)
  1854 apply (rule_tac x=x in bexI) 
  1854 apply (rule_tac x=x in bexI) 
  1855 apply (rule_tac x=y in exI, auto, ultra)
  1855 apply (rule_tac x=y in exI, auto, ultra)
  1856 done
  1856 done
  1857 
  1857 
  1858 lemma FreeUltrafilterNat_HFinite:
  1858 lemma FreeUltrafilterNat_HFinite:
  1859      "\<exists>X \<in> Rep_hypreal x.
  1859      "\<exists>X \<in> Rep_hypreal x.
  1860        \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
  1860        \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
  1861        ==>  x \<in> HFinite"
  1861        ==>  x \<in> HFinite"
  1862 apply (rule eq_Abs_hypreal [of x])
  1862 apply (cases x)
  1863 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
  1863 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
  1864 apply (rule_tac x = "hypreal_of_real u" in bexI)
  1864 apply (rule_tac x = "hypreal_of_real u" in bexI)
  1865 apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
  1865 apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
  1866 done
  1866 done
  1867 
  1867 
  1952 lemma Infinitesimal_FreeUltrafilterNat:
  1952 lemma Infinitesimal_FreeUltrafilterNat:
  1953           "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_hypreal x.
  1953           "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_hypreal x.
  1954            \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
  1954            \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
  1955 apply (simp add: Infinitesimal_def)
  1955 apply (simp add: Infinitesimal_def)
  1956 apply (auto simp add: abs_less_iff minus_less_iff [of x])
  1956 apply (auto simp add: abs_less_iff minus_less_iff [of x])
  1957 apply (rule eq_Abs_hypreal [of x])
  1957 apply (cases x)
  1958 apply (auto, rule bexI [OF _ lemma_hyprel_refl], safe)
  1958 apply (auto, rule bexI [OF _ lemma_hyprel_refl], safe)
  1959 apply (drule hypreal_of_real_less_iff [THEN iffD2])
  1959 apply (drule hypreal_of_real_less_iff [THEN iffD2])
  1960 apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
  1960 apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
  1961 apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra)
  1961 apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra)
  1962 done
  1962 done
  1964 lemma FreeUltrafilterNat_Infinitesimal:
  1964 lemma FreeUltrafilterNat_Infinitesimal:
  1965      "\<exists>X \<in> Rep_hypreal x.
  1965      "\<exists>X \<in> Rep_hypreal x.
  1966             \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
  1966             \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
  1967       ==> x \<in> Infinitesimal"
  1967       ==> x \<in> Infinitesimal"
  1968 apply (simp add: Infinitesimal_def)
  1968 apply (simp add: Infinitesimal_def)
  1969 apply (rule eq_Abs_hypreal [of x])
  1969 apply (cases x)
  1970 apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
  1970 apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
  1971 apply (auto simp add: SReal_iff)
  1971 apply (auto simp add: SReal_iff)
  1972 apply (drule_tac [!] x=y in spec) 
  1972 apply (drule_tac [!] x=y in spec) 
  1973 apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra+)
  1973 apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra+)
  1974 done
  1974 done