src/HOL/NSA/NSComplex.thy
changeset 47108 2a1953f0d20d
parent 44846 e9d1fcbc7d20
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/NSA/NSComplex.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/NSA/NSComplex.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -626,32 +626,38 @@
     1.4  
     1.5  subsection{*Numerals and Arithmetic*}
     1.6  
     1.7 -lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w"
     1.8 -by transfer (rule number_of_eq [THEN eq_reflection])
     1.9 -
    1.10  lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
    1.11       "hcomplex_of_hypreal (hypreal_of_real x) =  
    1.12        hcomplex_of_complex (complex_of_real x)"
    1.13  by transfer (rule refl)
    1.14  
    1.15 -lemma hcomplex_hypreal_number_of: 
    1.16 -  "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
    1.17 -by transfer (rule of_real_number_of_eq [symmetric])
    1.18 +lemma hcomplex_hypreal_numeral:
    1.19 +  "hcomplex_of_complex (numeral w) = hcomplex_of_hypreal(numeral w)"
    1.20 +by transfer (rule of_real_numeral [symmetric])
    1.21  
    1.22 -lemma hcomplex_number_of_hcnj [simp]:
    1.23 -     "hcnj (number_of v :: hcomplex) = number_of v"
    1.24 -by transfer (rule complex_cnj_number_of)
    1.25 +lemma hcomplex_hypreal_neg_numeral:
    1.26 +  "hcomplex_of_complex (neg_numeral w) = hcomplex_of_hypreal(neg_numeral w)"
    1.27 +by transfer (rule of_real_neg_numeral [symmetric])
    1.28 +
    1.29 +lemma hcomplex_numeral_hcnj [simp]:
    1.30 +     "hcnj (numeral v :: hcomplex) = numeral v"
    1.31 +by transfer (rule complex_cnj_numeral)
    1.32  
    1.33 -lemma hcomplex_number_of_hcmod [simp]: 
    1.34 -      "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
    1.35 -by transfer (rule norm_number_of)
    1.36 +lemma hcomplex_numeral_hcmod [simp]:
    1.37 +      "hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)"
    1.38 +by transfer (rule norm_numeral)
    1.39 +
    1.40 +lemma hcomplex_neg_numeral_hcmod [simp]: 
    1.41 +      "hcmod(neg_numeral v :: hcomplex) = (numeral v :: hypreal)"
    1.42 +by transfer (rule norm_neg_numeral)
    1.43  
    1.44 -lemma hcomplex_number_of_hRe [simp]: 
    1.45 -      "hRe(number_of v :: hcomplex) = number_of v"
    1.46 -by transfer (rule complex_Re_number_of)
    1.47 +lemma hcomplex_numeral_hRe [simp]: 
    1.48 +      "hRe(numeral v :: hcomplex) = numeral v"
    1.49 +by transfer (rule complex_Re_numeral)
    1.50  
    1.51 -lemma hcomplex_number_of_hIm [simp]: 
    1.52 -      "hIm(number_of v :: hcomplex) = 0"
    1.53 -by transfer (rule complex_Im_number_of)
    1.54 +lemma hcomplex_numeral_hIm [simp]: 
    1.55 +      "hIm(numeral v :: hcomplex) = 0"
    1.56 +by transfer (rule complex_Im_numeral)
    1.57  
    1.58 +(* TODO: add neg_numeral rules above *)
    1.59  end