# HG changeset patch
# User huffman
# Date 1126914601 -7200
# Node ID f503dccdff2783213f9871097db0e32743286aab
# Parent  c0f0b92c198c47d70fda9457b8a2418b5e0b4ddc
use interpretation command

diff -r c0f0b92c198c -r f503dccdff27 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Fri Sep 16 23:55:23 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Sat Sep 17 01:50:01 2005 +0200
@@ -11,9 +11,12 @@
 imports HyperPow
 begin
 
+lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"
+by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
+
 lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
-apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
+apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
+apply (rule_tac x=whn in spec, transfer, simp)
 done
 
 lemma InternalSets_Un:
@@ -23,8 +26,8 @@
 
 lemma starset_n_Int:
       "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
-apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n filter.Collect_conj [OF filter_FUFNat])
+apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
+apply (rule_tac x=whn in spec, transfer, simp)
 done
 
 lemma InternalSets_Int:
@@ -33,17 +36,16 @@
 by (auto simp add: InternalSets_def starset_n_Int [symmetric])
 
 lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
-apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n ultrafilter.Collect_not [OF ultrafilter_FUFNat])
+apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_def)
+apply (rule_tac x=whn in spec, transfer, simp)
 done
 
 lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
 by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
 
 lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
-apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n  filter.Collect_conj [OF filter_FUFNat]
-                 ultrafilter.Collect_not [OF ultrafilter_FUFNat])
+apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_def)
+apply (rule_tac x=whn in spec, transfer, simp)
 done
 
 lemma InternalSets_diff:
diff -r c0f0b92c198c -r f503dccdff27 src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Fri Sep 16 23:55:23 2005 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy	Sat Sep 17 01:50:01 2005 +0200
@@ -23,25 +23,14 @@
  apply (rule nat_infinite)
 done
 
-lemmas ultrafilter_FUFNat =
-  freeultrafilter_FUFNat [THEN freeultrafilter.ultrafilter]
-
-lemmas filter_FUFNat =
-  freeultrafilter_FUFNat [THEN freeultrafilter.filter]
-
-lemmas FUFNat_empty [iff] =
-  filter_FUFNat [THEN filter.empty]
-
-lemmas FUFNat_UNIV [iff] =
-  filter_FUFNat [THEN filter.UNIV]
+interpretation FUFNat: freeultrafilter [FreeUltrafilterNat]
+by (cut_tac [!] freeultrafilter_FUFNat, simp_all add: freeultrafilter_def)
 
 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
-    ultrafilter_FUFNat [THEN ultrafilter.Un_iff]
-    ultrafilter_FUFNat [THEN ultrafilter.Compl_iff])
+by (simp add: Collect_imp_eq FUFNat.F.Un_iff FUFNat.F.Compl_iff)
 
 
 subsection {* Definition of @{text star} type constructor *}
@@ -105,26 +94,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 filter.Collect_ex [OF filter_FUFNat])
+by (simp only: ex_star_eq FUFNat.F.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 ultrafilter.Collect_all [OF ultrafilter_FUFNat])
+by (simp only: all_star_eq FUFNat.F.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: ultrafilter.Collect_not [OF ultrafilter_FUFNat])
+by (simp only: FUFNat.F.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: filter.Collect_conj [OF filter_FUFNat])
+by (simp only: FUFNat.F.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: ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
+by (simp only: FUFNat.F.Collect_disj)
 
 lemma transfer_imp [transfer_intro]:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>