# HG changeset patch
# User huffman
# Date 1126291020 -7200
# Node ID 14c6e073252fefdfb29cb7b7f05d0f0a5db2233f
# Parent  bc1c75855f3d46b20ecfc1c5b143d410f149c609
updated to work with new HOL-Complex version

diff -r bc1c75855f3d -r 14c6e073252f src/HOL/Complex/ex/NSPrimes.thy
--- a/src/HOL/Complex/ex/NSPrimes.thy	Fri Sep 09 19:34:22 2005 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy	Fri Sep 09 20:37:00 2005 +0200
@@ -16,13 +16,15 @@
 
 constdefs
   hdvd  :: "[hypnat, hypnat] => bool"       (infixl "hdvd" 50)
+   "(M::hypnat) hdvd N == ( *p2* (op dvd)) M N"
+(*
    "(M::hypnat) hdvd N ==
 	           \<exists>X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) &
                                {n::nat. X n dvd Y n} : FreeUltrafilterNat"
-
+*)
 constdefs
   starprime :: "hypnat set"
-  "starprime == ( *sNat* {p. prime p})"
+  "starprime == ( *s* {p. prime p})"
 
 constdefs
   choicefun :: "'a set => 'a"
@@ -78,23 +80,20 @@
 
 lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard]
 
-lemma lemma_hypnat_P_EX: "(\<exists>(x::hypnat). P x) = (\<exists>f. P (Abs_hypnat(hypnatrel `` {f})))"
+lemma lemma_hypnat_P_EX: "(\<exists>(x::hypnat). P x) = (\<exists>f. P (star_n f))"
 apply auto
-apply (rule_tac z = x in eq_Abs_hypnat, auto)
+apply (rule_tac x = x in star_cases, auto)
 done
 
-lemma lemma_hypnat_P_ALL: "(\<forall>(x::hypnat). P x) = (\<forall>f. P (Abs_hypnat(hypnatrel `` {f})))"
+lemma lemma_hypnat_P_ALL: "(\<forall>(x::hypnat). P x) = (\<forall>f. P (star_n f))"
 apply auto
-apply (rule_tac z = x in eq_Abs_hypnat, auto)
+apply (rule_tac x = x in star_cases, auto)
 done
 
 lemma hdvd:
-      "(Abs_hypnat(hypnatrel``{%n. X n}) hdvd
-            Abs_hypnat(hypnatrel``{%n. Y n})) =
+      "(star_n X hdvd star_n Y) =
        ({n. X n dvd Y n} : FreeUltrafilterNat)"
-apply (unfold hdvd_def)
-apply (auto, ultra)
-done
+by (simp add: hdvd_def starP2)
 
 lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
 by (subst hypnat_of_nat_zero [symmetric], auto)
@@ -103,18 +102,7 @@
 
 (* Goldblatt: Exercise 5.11(2) - p. 57 *)
 lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)"
-apply safe
-apply (rule_tac z = M in eq_Abs_hypnat)
-apply (auto simp add: lemma_hypnat_P_EX lemma_hypnat_P_ALL
-              hypnat_zero_def hypnat_le hypnat_less hdvd)
-apply (cut_tac dvd_by_all)
-apply (subgoal_tac " \<forall>(n::nat) . \<exists>N. 0 < N & (\<forall>m. 0 < (m::nat) & m <= (x n) --> m dvd N)")
- prefer 2 apply blast
-apply (erule thin_rl)
-apply (drule choice, safe)
-apply (rule_tac x = f in exI, auto, ultra)
-apply auto
-done
+by (unfold hdvd_def, transfer, rule dvd_by_all)
 
 lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
 
@@ -136,17 +124,7 @@
 lemma starprime:
   "starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}"
 apply (unfold starprime_def prime_def)
-apply (auto simp add: Collect_conj_eq NatStar_Int)
-apply (rule_tac [!] z = x in eq_Abs_hypnat)
-apply (rule_tac [2] z = m in eq_Abs_hypnat)
-apply (auto simp add: hdvd hypnat_one_def hypnat_less lemma_hypnat_P_ALL starsetNat_def)
-apply (drule bspec, drule_tac [2] bspec, auto)
-apply (ultra, ultra)
-apply (rule ccontr)
-apply (drule FreeUltrafilterNat_Compl_mem)
-apply (auto simp add: Collect_neg_eq [symmetric])
-apply (drule UF_choice, auto)
-apply (drule_tac x = f in spec, auto, ultra+)
+apply (unfold hdvd_def, transfer, rule refl)
 done
 
 lemma prime_two:  "prime 2"
@@ -169,28 +147,17 @@
 done
 
 (* Goldblatt Exercise 5.11(3b) - p 57  *)
-lemma hyperprime_factor_exists [rule_format]: "1 < n ==> (\<exists>k \<in> starprime. k hdvd n)"
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (auto simp add: hypnat_one_def hypnat_less starprime_def
-    lemma_hypnat_P_EX lemma_hypnat_P_ALL hdvd starsetNat_def Ball_def UF_if)
-apply (rule_tac x = "%n. @y. prime y & y dvd x n" in exI, auto, ultra)
-apply (drule sym, simp (no_asm_simp))
- prefer 2 apply ultra
-apply (rule_tac [!] someI2_ex)
-apply (auto dest!: prime_factor_exists)
-done
-
-(* behaves as expected! *)
-lemma NatStar_insert: "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)"
-apply (auto simp add: starsetNat_def hypnat_of_nat_eq)
-apply (rule_tac [!] z = xa in eq_Abs_hypnat, auto)
-apply (drule_tac [!] bspec asm_rl, auto, ultra+)
+lemma hyperprime_factor_exists [rule_format]:
+  "!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)"
+apply (unfold starprime_def hdvd_def)
+apply (transfer prime_def)
+apply (simp add: prime_factor_exists)
 done
 
 (* Goldblatt Exercise 3.10(1) - p. 29 *)
-lemma NatStar_hypnat_of_nat: "finite A ==> *sNat* A = hypnat_of_nat ` A"
-apply (rule_tac P = "%x. *sNat* x = hypnat_of_nat ` x" in finite_induct)
-apply (auto simp add: NatStar_insert)
+lemma NatStar_hypnat_of_nat: "finite A ==> *s* A = hypnat_of_nat ` A"
+apply (rule_tac P = "%x. *s* x = hypnat_of_nat ` x" in finite_induct)
+apply auto
 done
 
 (* proved elsewhere? *)
@@ -239,8 +206,8 @@
 apply auto
 done
 
-lemma inj_fun_not_hypnat_in_SHNat: "inj f ==> Abs_hypnat(hypnatrel `` {f}) \<notin> Nats"
-apply (auto simp add: SHNat_eq hypnat_of_nat_eq)
+lemma inj_fun_not_hypnat_in_SHNat: "inj (f::nat=>nat) ==> star_n f \<notin> Nats"
+apply (auto simp add: SHNat_eq hypnat_of_nat_eq star_n_eq_iff)
 apply (subgoal_tac "\<forall>m n. m \<noteq> n --> f n \<noteq> f m", auto)
 apply (drule_tac [2] injD)
 prefer 2 apply assumption
@@ -248,10 +215,9 @@
 done
 
 lemma range_subset_mem_starsetNat:
-   "range f <= A ==> Abs_hypnat(hypnatrel `` {f}) \<in> *sNat* A"
-apply (unfold starsetNat_def, auto, ultra)
-apply (drule_tac c = "f x" in subsetD)
-apply (rule rangeI, auto)
+   "range f <= A ==> star_n f \<in> *s* A"
+apply (simp add: Iset_of_def star_of_def Iset_star_n)
+apply (subgoal_tac "\<forall>n. f n \<in> A", auto)
 done
 
 (*--------------------------------------------------------------------------------*)
@@ -315,10 +281,10 @@
 text{*Only need the existence of an injective function from N to A for proof*}
 
 lemma hypnat_infinite_has_nonstandard:
-     "~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)"
+     "~ finite A ==> hypnat_of_nat ` A < ( *s* A)"
 apply auto
 apply (rule subsetD)
-apply (rule NatStar_hypreal_of_real_image_subset, auto)
+apply (rule STAR_star_of_image_subset, auto)
 apply (subgoal_tac "A \<noteq> {}")
 prefer 2 apply force
 apply (drule infinite_set_has_order_preserving_inj)
@@ -328,15 +294,15 @@
 apply (auto simp add: SHNat_eq)
 done
 
-lemma starsetNat_eq_hypnat_of_nat_image_finite: "*sNat* A =  hypnat_of_nat ` A ==> finite A"
+lemma starsetNat_eq_hypnat_of_nat_image_finite: "*s* A =  hypnat_of_nat ` A ==> finite A"
 apply (rule ccontr)
 apply (auto dest: hypnat_infinite_has_nonstandard)
 done
 
-lemma finite_starsetNat_iff: "( *sNat* A = hypnat_of_nat ` A) = (finite A)"
+lemma finite_starsetNat_iff: "( *s* A = hypnat_of_nat ` A) = (finite A)"
 by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat)
 
-lemma hypnat_infinite_has_nonstandard_iff: "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)"
+lemma hypnat_infinite_has_nonstandard_iff: "(~ finite A) = (hypnat_of_nat ` A < *s* A)"
 apply (rule iffI)
 apply (blast intro!: hypnat_infinite_has_nonstandard)
 apply (auto simp add: finite_starsetNat_iff [symmetric])
@@ -347,7 +313,7 @@
 lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)"
 apply auto
 apply (rule_tac x = 2 in bexI)
-apply (auto simp add: hypnat_of_nat_eq hypnat_one_def hdvd dvd_def)
+apply (unfold hdvd_def, transfer, auto)
 done
 declare lemma_not_dvd_hypnat_one [simp]
 
@@ -359,18 +325,12 @@
 
 (* not needed here *)
 lemma hypnat_gt_zero_gt_one:
-  "[| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N"
-apply (unfold hypnat_zero_def hypnat_one_def)
-apply (rule_tac z = N in eq_Abs_hypnat)
-apply (auto simp add: hypnat_less, ultra)
-done
+  "!!N. [| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N"
+by (transfer, simp)
 
 lemma hypnat_add_one_gt_one:
-    "0 < N ==> 1 < (N::hypnat) + 1"
-apply (unfold hypnat_zero_def hypnat_one_def)
-apply (rule_tac z = N in eq_Abs_hypnat)
-apply (auto simp add: hypnat_less hypnat_add)
-done
+    "!!N. 0 < N ==> 1 < (N::hypnat) + 1"
+by (transfer, simp)
 
 lemma zero_not_prime: "\<not> prime 0"
 apply safe
@@ -379,14 +339,12 @@
 declare zero_not_prime [simp]
 
 lemma hypnat_of_nat_zero_not_prime: "hypnat_of_nat 0 \<notin> starprime"
-by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq)
+by (unfold starprime_def, transfer prime_def, simp)
 declare hypnat_of_nat_zero_not_prime [simp]
 
 lemma hypnat_zero_not_prime:
    "0 \<notin> starprime"
-apply (unfold starprime_def starsetNat_def hypnat_zero_def)
-apply (auto intro!: bexI)
-done
+by (cut_tac hypnat_of_nat_zero_not_prime, simp)
 declare hypnat_zero_not_prime [simp]
 
 lemma one_not_prime: "\<not> prime 1"
@@ -402,31 +360,21 @@
 declare one_not_prime2 [simp]
 
 lemma hypnat_of_nat_one_not_prime: "hypnat_of_nat 1 \<notin> starprime"
-by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq)
+by (unfold starprime_def, transfer prime_def, simp)
 declare hypnat_of_nat_one_not_prime [simp]
 
 lemma hypnat_one_not_prime: "1 \<notin> starprime"
-apply (unfold starprime_def starsetNat_def hypnat_one_def)
-apply (auto intro!: bexI)
-done
+by (cut_tac hypnat_of_nat_one_not_prime, simp)
 declare hypnat_one_not_prime [simp]
 
-lemma hdvd_diff: "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)"
-apply (rule_tac z = k in eq_Abs_hypnat)
-apply (rule_tac z = m in eq_Abs_hypnat)
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (auto simp add: hdvd hypnat_minus, ultra)
-apply (blast intro: dvd_diff)
-done
+lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)"
+by (unfold hdvd_def, transfer, rule dvd_diff)
 
 lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1"
 by (unfold dvd_def, auto)
 
-lemma hdvd_one_eq_one: "x hdvd 1 ==> x = 1"
-apply (unfold hypnat_one_def)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (auto simp add: hdvd)
-done
+lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1"
+by (unfold hdvd_def, transfer, rule dvd_one_eq_one)
 
 theorem not_finite_prime: "~ finite {p. prime p}"
 apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
@@ -436,7 +384,7 @@
 apply (subgoal_tac "1 < N + 1")
 prefer 2 apply (blast intro: hypnat_add_one_gt_one)
 apply (drule hyperprime_factor_exists)
-apply (auto intro: NatStar_mem)
+apply (auto intro: STAR_mem)
 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
 apply (force simp add: starprime_def, safe)
 apply (drule_tac x = x in bspec)