1.1 --- a/src/HOL/NSA/Examples/NSPrimes.thy	Wed May 19 16:08:41 2010 -0700
     1.2 +++ b/src/HOL/NSA/Examples/NSPrimes.thy	Wed May 19 16:28:24 2010 -0700
     1.3 @@ -13,9 +13,7 @@
     1.4  text{*These can be used to derive an alternative proof of the infinitude of
     1.5  primes by considering a property of nonstandard sets.*}
     1.6  
     1.7 -definition
     1.8 -  hdvd  :: "[hypnat, hypnat] => bool"       (infixl "hdvd" 50) where
     1.9 -  [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
    1.10 +declare dvd_def [transfer_refold]
    1.11  
    1.12  definition
    1.13    starprime :: "hypnat set" where
    1.14 @@ -49,14 +47,14 @@
    1.15  
    1.16  
    1.17  (* Goldblatt: Exercise 5.11(2) - p. 57 *)
    1.18 -lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)"
    1.19 +lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
    1.20  by (transfer, rule dvd_by_all)
    1.21  
    1.22  lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
    1.23  
    1.24  (* Goldblatt: Exercise 5.11(2) - p. 57 *)
    1.25  lemma hypnat_dvd_all_hypnat_of_nat:
    1.26 -     "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) hdvd N)"
    1.27 +     "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) dvd N)"
    1.28  apply (cut_tac hdvd_by_all)
    1.29  apply (drule_tac x = whn in spec, auto)
    1.30  apply (rule exI, auto)
    1.31 @@ -70,7 +68,7 @@
    1.32  
    1.33  (* Goldblatt: Exercise 5.11(3a) - p 57  *)
    1.34  lemma starprime:
    1.35 -  "starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}"
    1.36 +  "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
    1.37  by (transfer, auto simp add: prime_def)
    1.38  
    1.39  lemma prime_two:  "prime 2"
    1.40 @@ -88,13 +86,11 @@
    1.41  apply (rule_tac x = n in exI, auto)
    1.42  apply (drule conjI [THEN not_prime_ex_mk], auto)
    1.43  apply (drule_tac x = m in spec, auto)
    1.44 -apply (rule_tac x = ka in exI)
    1.45 -apply (auto intro: dvd_mult2)
    1.46  done
    1.47  
    1.48  (* Goldblatt Exercise 5.11(3b) - p 57  *)
    1.49  lemma hyperprime_factor_exists [rule_format]:
    1.50 -  "!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)"
    1.51 +  "!!n. 1 < n ==> (\<exists>k \<in> starprime. k dvd n)"
    1.52  by (transfer, simp add: prime_factor_exists)
    1.53  
    1.54  (* Goldblatt Exercise 3.10(1) - p. 29 *)
    1.55 @@ -257,14 +253,14 @@
    1.56  
    1.57  subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*}
    1.58  
    1.59 -lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)"
    1.60 +lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)"
    1.61  apply auto
    1.62  apply (rule_tac x = 2 in bexI)
    1.63  apply (transfer, auto)
    1.64  done
    1.65  declare lemma_not_dvd_hypnat_one [simp]
    1.66  
    1.67 -lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n hdvd 1"
    1.68 +lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n dvd 1"
    1.69  apply (cut_tac lemma_not_dvd_hypnat_one)
    1.70  apply (auto simp del: lemma_not_dvd_hypnat_one)
    1.71  done
    1.72 @@ -314,13 +310,13 @@
    1.73  by (cut_tac hypnat_of_nat_one_not_prime, simp)
    1.74  declare hypnat_one_not_prime [simp]
    1.75  
    1.76 -lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)"
    1.77 -by (transfer, rule dvd_diff)
    1.78 +lemma hdvd_diff: "!!k m n :: hypnat. [| k dvd m; k dvd n |] ==> k dvd (m - n)"
    1.79 +by (transfer, rule dvd_diff_nat)
    1.80  
    1.81  lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1"
    1.82  by (unfold dvd_def, auto)
    1.83  
    1.84 -lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1"
    1.85 +lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1"
    1.86  by (transfer, rule dvd_one_eq_one)
    1.87  
    1.88  theorem not_finite_prime: "~ finite {p. prime p}"