# HG changeset patch
# User huffman
# Date 1165906000 -3600
# Node ID 9edd495b6330dcee712c7c58bab04c89b5b11129
# Parent  66da6af2b0c9d00e781a3c6e232b23d3b1c861ef
consistent naming for FreeUltrafilterNat lemmas; cleaned up

diff -r 66da6af2b0c9 -r 9edd495b6330 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Dec 12 07:13:06 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Dec 12 07:46:40 2006 +0100
@@ -19,12 +19,14 @@
   "hypreal_of_real == star_of"
 
 definition
-  omega :: hypreal where   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
-  "omega = star_n (%n. real (Suc n))"
+  omega :: hypreal where
+   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
+  "omega = star_n (\<lambda>n. real (Suc n))"
 
 definition
-  epsilon :: hypreal where   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
-  "epsilon = star_n (%n. inverse (real (Suc n)))"
+  epsilon :: hypreal where
+   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
+  "epsilon = star_n (\<lambda>n. inverse (real (Suc n)))"
 
 notation (xsymbols)
   omega  ("\<omega>") and
@@ -42,31 +44,31 @@
 defs (overloaded)
   star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
 
-lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> r *# x \<in> Standard"
+lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard"
 by (simp add: star_scaleR_def)
 
-lemma star_of_scaleR [simp]: "star_of (r *# x) = r *# star_of x"
+lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)"
 by transfer (rule refl)
 
 instance star :: (real_vector) real_vector
 proof
   fix a b :: real
-  show "\<And>x y::'a star. a *# (x + y) = a *# x + a *# y"
+  show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y"
     by transfer (rule scaleR_right_distrib)
-  show "\<And>x::'a star. (a + b) *# x = a *# x + b *# x"
+  show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x"
     by transfer (rule scaleR_left_distrib)
-  show "\<And>x::'a star. a *# b *# x = (a * b) *# x"
+  show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x"
     by transfer (rule scaleR_scaleR)
-  show "\<And>x::'a star. 1 *# x = x"
+  show "\<And>x::'a star. scaleR 1 x = x"
     by transfer (rule scaleR_one)
 qed
 
 instance star :: (real_algebra) real_algebra
 proof
   fix a :: real
-  show "\<And>x y::'a star. a *# x * y = a *# (x * y)"
+  show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)"
     by transfer (rule mult_scaleR_left)
-  show "\<And>x y::'a star. x * a *# y = a *# (x * y)"
+  show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)"
     by transfer (rule mult_scaleR_right)
 qed
 
@@ -117,52 +119,47 @@
 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.filter])
 
 lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat"
-by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite])
+by (rule FreeUltrafilterNat.finite)
 
 lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x"
-thm FreeUltrafilterNat_mem
-thm freeultrafilter.infinite
-thm FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]
-by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite])
+by (rule FreeUltrafilterNat.infinite)
 
-lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.empty])
+lemma FreeUltrafilterNat_empty: "{} \<notin> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.empty)
 
 lemma FreeUltrafilterNat_Int:
      "[| X \<in> FreeUltrafilterNat;  Y \<in> FreeUltrafilterNat |]   
       ==> X Int Y \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.Int])
+by (rule FreeUltrafilterNat.Int)
 
 lemma FreeUltrafilterNat_subset:
      "[| X \<in> FreeUltrafilterNat;  X \<subseteq> Y |]  
       ==> Y \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.subset])
+by (rule FreeUltrafilterNat.subset)
 
 lemma FreeUltrafilterNat_Compl:
      "X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
-apply (erule contrapos_pn)
-apply (erule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD2])
-done
+by (rule FreeUltrafilterNat.memD)
 
 lemma FreeUltrafilterNat_Compl_mem:
-     "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
-by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD1])
+     "X \<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.not_memD)
 
 lemma FreeUltrafilterNat_Compl_iff1:
      "(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)"
-by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff])
+by (rule FreeUltrafilterNat.not_mem_iff)
 
 lemma FreeUltrafilterNat_Compl_iff2:
      "(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
 
 lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
-apply (drule FreeUltrafilterNat_finite)  
-apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
+apply (drule FreeUltrafilterNat.finite)
+apply (simp add: FreeUltrafilterNat.not_mem_iff)
 done
 
-lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.UNIV])
+lemma FreeUltrafilterNat_UNIV: "UNIV \<in> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.UNIV)
 
 lemma FreeUltrafilterNat_Nat_set_refl [intro]:
      "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
@@ -202,7 +199,7 @@
 subsection{*Properties of @{term starrel}*}
 
 text{*Proving that @{term starrel} is an equivalence relation*}
-
+(*
 lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
 by (rule StarDef.starrel_iff)
 
@@ -219,21 +216,11 @@
 lemma equiv_starrel: "equiv UNIV starrel"
 by (rule StarDef.equiv_starrel)
 
-(* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
 lemmas equiv_starrel_iff =
     eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] 
 
-lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
-by (simp add: star_def starrel_def quotient_def, blast)
-
-declare Abs_star_inject [simp] Abs_star_inverse [simp]
-declare equiv_starrel [THEN eq_equiv_class_iff, simp]
-
 lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
 
-lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
-by (simp add: starrel_def)
-
 lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
 apply (simp add: star_def)
 apply (auto elim!: quotientE equalityCE)
@@ -241,6 +228,16 @@
 
 lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
 by (insert Rep_star [of x], auto)
+*)
+
+lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
+by (simp add: starrel_def)
+
+lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
+by (simp add: star_def starrel_def quotient_def, blast)
+
+declare Abs_star_inject [simp] Abs_star_inverse [simp]
+declare equiv_starrel [THEN eq_equiv_class_iff, simp]
 
 subsection{*@{term hypreal_of_real}: 
             the Injection from @{typ real} to @{typ hypreal}*}
diff -r 66da6af2b0c9 -r 9edd495b6330 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Dec 12 07:13:06 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Tue Dec 12 07:46:40 2006 +0100
@@ -258,10 +258,12 @@
   hypnat_omega_def: "whn = star_n (%n::nat. n)"
 
 lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff FUFNat.finite)
+by (simp add: hypnat_omega_def star_of_def star_n_eq_iff
+              FreeUltrafilterNat.finite)
 
 lemma whn_neq_hypnat_of_nat: "whn \<noteq> hypnat_of_nat n"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff FUFNat.finite)
+by (simp add: hypnat_omega_def star_of_def star_n_eq_iff
+              FreeUltrafilterNat.finite)
 
 lemma whn_not_Nats [simp]: "whn \<notin> Nats"
 by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)
@@ -373,32 +375,32 @@
 
 lemma hypreal_of_hypnat_inject [simp]:
      "!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-by (transfer, simp)
+by transfer (rule real_of_nat_inject)
 
 lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
-by (simp add: star_n_zero_num hypreal_of_hypnat)
+by transfer (rule real_of_nat_zero)
 
 lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
-by (simp add: star_n_one_num hypreal_of_hypnat)
+by transfer simp
 
 lemma hypreal_of_hypnat_add [simp]:
      "!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-by (transfer, rule real_of_nat_add)
+by transfer (rule real_of_nat_add)
 
 lemma hypreal_of_hypnat_mult [simp]:
      "!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-by (transfer, rule real_of_nat_mult)
+by transfer (rule real_of_nat_mult)
 
 lemma hypreal_of_hypnat_less_iff [simp]:
      "!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-by (transfer, simp)
+by transfer (rule real_of_nat_less_iff)
 
 lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
 by (simp add: hypreal_of_hypnat_zero [symmetric])
 declare hypreal_of_hypnat_eq_zero_iff [simp]
 
 lemma hypreal_of_hypnat_ge_zero [simp]: "!!n. 0 \<le> hypreal_of_hypnat n"
-by (transfer, simp)
+by transfer (rule real_of_nat_ge_zero)
 
 lemma HNatInfinite_inverse_Infinitesimal [simp]:
      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
diff -r 66da6af2b0c9 -r 9edd495b6330 src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Tue Dec 12 07:13:06 2006 +0100
+++ b/src/HOL/Hyperreal/StarDef.thy	Tue Dec 12 07:46:40 2006 +0100
@@ -16,21 +16,22 @@
   FreeUltrafilterNat :: "nat set set"  ("\<U>") where
   "\<U> = (SOME U. freeultrafilter U)"
 
-lemma freeultrafilter_FUFNat: "freeultrafilter \<U>"
- apply (unfold FreeUltrafilterNat_def)
- apply (rule someI_ex)
- apply (rule freeultrafilter_Ex)
- apply (rule nat_infinite)
- done
+lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
+apply (unfold FreeUltrafilterNat_def)
+apply (rule someI_ex)
+apply (rule freeultrafilter_Ex)
+apply (rule nat_infinite)
+done
 
-interpretation FUFNat: freeultrafilter [FreeUltrafilterNat]
-  using freeultrafilter_FUFNat by (simp_all add: freeultrafilter_def)
+interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat]
+by (rule freeultrafilter_FreeUltrafilterNat)
 
 text {* This rule takes the place of the old ultra tactic *}
 
 lemma ultra:
   "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
-by (simp add: Collect_imp_eq FUFNat.F.Un_iff FUFNat.F.Compl_iff)
+by (simp add: Collect_imp_eq
+    FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff)
 
 
 subsection {* Definition of @{text star} type constructor *}
@@ -94,26 +95,26 @@
 lemma transfer_ex [transfer_intro]:
   "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
     \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
-by (simp only: ex_star_eq FUFNat.F.Collect_ex)
+by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
 
 lemma transfer_all [transfer_intro]:
   "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
     \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
-by (simp only: all_star_eq FUFNat.F.Collect_all)
+by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
 
 lemma transfer_not [transfer_intro]:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
-by (simp only: FUFNat.F.Collect_not)
+by (simp only: FreeUltrafilterNat.Collect_not)
 
 lemma transfer_conj [transfer_intro]:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
     \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
-by (simp only: FUFNat.F.Collect_conj)
+by (simp only: FreeUltrafilterNat.Collect_conj)
 
 lemma transfer_disj [transfer_intro]:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
     \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
-by (simp only: FUFNat.F.Collect_disj)
+by (simp only: FreeUltrafilterNat.Collect_disj)
 
 lemma transfer_imp [transfer_intro]:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>