src/HOL/Complex/NSComplex.thy
changeset 14387 e96d5c42c4b0
parent 14377 f454b3004f8f
child 14421 ee97b6463cb4
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -1368,8 +1368,10 @@
     1.4  lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0"
     1.5  by (simp add: hcomplex_of_complex_def hcomplex_zero_def)
     1.6  
     1.7 -lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)"
     1.8 -by (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
     1.9 +lemma hcomplex_of_complex_zero_iff [simp]:
    1.10 +     "(hcomplex_of_complex r = 0) = (r = 0)"
    1.11 +by (auto intro: FreeUltrafilterNat_P 
    1.12 +         simp add: hcomplex_of_complex_def hcomplex_zero_def)
    1.13  
    1.14  lemma hcomplex_of_complex_inverse [simp]:
    1.15       "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
    1.16 @@ -1398,6 +1400,199 @@
    1.17       "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
    1.18  by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
    1.19  
    1.20 +
    1.21 +subsection{*Numerals and Arithmetic*}
    1.22 +
    1.23 +instance hcomplex :: number ..
    1.24 +
    1.25 +primrec (*the type constraint is essential!*)
    1.26 +  number_of_Pls: "number_of bin.Pls = 0"
    1.27 +  number_of_Min: "number_of bin.Min = - (1::hcomplex)"
    1.28 +  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
    1.29 +	                               (number_of w) + (number_of w)"
    1.30 +
    1.31 +declare number_of_Pls [simp del]
    1.32 +        number_of_Min [simp del]
    1.33 +        number_of_BIT [simp del]
    1.34 +
    1.35 +instance hcomplex :: number_ring
    1.36 +proof
    1.37 +  show "Numeral0 = (0::hcomplex)" by (rule number_of_Pls)
    1.38 +  show "-1 = - (1::hcomplex)" by (rule number_of_Min)
    1.39 +  fix w :: bin and x :: bool
    1.40 +  show "(number_of (w BIT x) :: hcomplex) =
    1.41 +        (if x then 1 else 0) + number_of w + number_of w"
    1.42 +    by (rule number_of_BIT)
    1.43 +qed
    1.44 +
    1.45 +
    1.46 +text{*Collapse applications of @{term hcomplex_of_complex} to @{term number_of}*}
    1.47 +lemma hcomplex_number_of [simp]:
    1.48 +     "hcomplex_of_complex (number_of w) = number_of w"
    1.49 +apply (induct w) 
    1.50 +apply (simp_all only: number_of hcomplex_of_complex_add 
    1.51 +                      hcomplex_of_complex_minus, simp_all) 
    1.52 +done
    1.53 +
    1.54 +lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
    1.55 +     "hcomplex_of_hypreal (hypreal_of_real x) =  
    1.56 +      hcomplex_of_complex(complex_of_real x)"
    1.57 +by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def 
    1.58 +              complex_of_real_def)
    1.59 +
    1.60 +lemma hcomplex_hypreal_number_of: 
    1.61 +  "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
    1.62 +by (simp only: complex_number_of [symmetric] hypreal_number_of [symmetric] 
    1.63 +               hcomplex_of_hypreal_eq_hcomplex_of_complex)
    1.64 +
    1.65 +text{*This theorem is necessary because theorems such as
    1.66 +   @{text iszero_number_of_0} only hold for ordered rings. They cannot
    1.67 +   be generalized to fields in general because they fail for finite fields.
    1.68 +   They work for type complex because the reals can be embedded in them.*}
    1.69 +lemma iszero_hcomplex_number_of [simp]:
    1.70 +     "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)"
    1.71 +apply (simp only: iszero_complex_number_of [symmetric])  
    1.72 +apply (simp only: hcomplex_of_complex_zero_iff hcomplex_number_of [symmetric] 
    1.73 +                  iszero_def)  
    1.74 +done
    1.75 +
    1.76 +
    1.77 +(*
    1.78 +Goal "z + hcnj z =  
    1.79 +      hcomplex_of_hypreal (2 * hRe(z))"
    1.80 +by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
    1.81 +by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
    1.82 +    hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
    1.83 +qed "hcomplex_add_hcnj";
    1.84 +
    1.85 +Goal "z - hcnj z = \
    1.86 +\     hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii";
    1.87 +by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
    1.88 +by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
    1.89 +    hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
    1.90 +    complex_diff_cnj,iii_def,hcomplex_mult]));
    1.91 +qed "hcomplex_diff_hcnj";
    1.92 +*)
    1.93 +
    1.94 +
    1.95 +lemma hcomplex_hcnj_num_zero_iff: "(hcnj z = 0) = (z = 0)"
    1.96 +apply (auto simp add: hcomplex_hcnj_zero_iff)
    1.97 +done
    1.98 +declare hcomplex_hcnj_num_zero_iff [simp]
    1.99 +
   1.100 +lemma hcomplex_zero_num: "0 = Abs_hcomplex (hcomplexrel `` {%n. 0})"
   1.101 +apply (simp add: hcomplex_zero_def)
   1.102 +done
   1.103 +
   1.104 +lemma hcomplex_one_num: "1 =  Abs_hcomplex (hcomplexrel `` {%n. 1})"
   1.105 +apply (simp add: hcomplex_one_def)
   1.106 +done
   1.107 +
   1.108 +(*** Real and imaginary stuff ***)
   1.109 +
   1.110 +(*Convert???
   1.111 +Goalw [hcomplex_number_of_def] 
   1.112 +  "((number_of xa :: hcomplex) + iii * number_of ya =  
   1.113 +        number_of xb + iii * number_of yb) =  
   1.114 +   (((number_of xa :: hcomplex) = number_of xb) &  
   1.115 +    ((number_of ya :: hcomplex) = number_of yb))"
   1.116 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff,
   1.117 +     hcomplex_hypreal_number_of]));
   1.118 +qed "hcomplex_number_of_eq_cancel_iff";
   1.119 +Addsimps [hcomplex_number_of_eq_cancel_iff];
   1.120 +
   1.121 +Goalw [hcomplex_number_of_def] 
   1.122 +  "((number_of xa :: hcomplex) + number_of ya * iii = \
   1.123 +\       number_of xb + number_of yb * iii) = \
   1.124 +\  (((number_of xa :: hcomplex) = number_of xb) & \
   1.125 +\   ((number_of ya :: hcomplex) = number_of yb))";
   1.126 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA,
   1.127 +    hcomplex_hypreal_number_of]));
   1.128 +qed "hcomplex_number_of_eq_cancel_iffA";
   1.129 +Addsimps [hcomplex_number_of_eq_cancel_iffA];
   1.130 +
   1.131 +Goalw [hcomplex_number_of_def] 
   1.132 +  "((number_of xa :: hcomplex) + number_of ya * iii = \
   1.133 +\       number_of xb + iii * number_of yb) = \
   1.134 +\  (((number_of xa :: hcomplex) = number_of xb) & \
   1.135 +\   ((number_of ya :: hcomplex) = number_of yb))";
   1.136 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB,
   1.137 +    hcomplex_hypreal_number_of]));
   1.138 +qed "hcomplex_number_of_eq_cancel_iffB";
   1.139 +Addsimps [hcomplex_number_of_eq_cancel_iffB];
   1.140 +
   1.141 +Goalw [hcomplex_number_of_def] 
   1.142 +  "((number_of xa :: hcomplex) + iii * number_of ya = \
   1.143 +\       number_of xb + number_of yb * iii) = \
   1.144 +\  (((number_of xa :: hcomplex) = number_of xb) & \
   1.145 +\   ((number_of ya :: hcomplex) = number_of yb))";
   1.146 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC,
   1.147 +     hcomplex_hypreal_number_of]));
   1.148 +qed "hcomplex_number_of_eq_cancel_iffC";
   1.149 +Addsimps [hcomplex_number_of_eq_cancel_iffC];
   1.150 +
   1.151 +Goalw [hcomplex_number_of_def] 
   1.152 +  "((number_of xa :: hcomplex) + iii * number_of ya = \
   1.153 +\       number_of xb) = \
   1.154 +\  (((number_of xa :: hcomplex) = number_of xb) & \
   1.155 +\   ((number_of ya :: hcomplex) = 0))";
   1.156 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2,
   1.157 +    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
   1.158 +qed "hcomplex_number_of_eq_cancel_iff2";
   1.159 +Addsimps [hcomplex_number_of_eq_cancel_iff2];
   1.160 +
   1.161 +Goalw [hcomplex_number_of_def] 
   1.162 +  "((number_of xa :: hcomplex) + number_of ya * iii = \
   1.163 +\       number_of xb) = \
   1.164 +\  (((number_of xa :: hcomplex) = number_of xb) & \
   1.165 +\   ((number_of ya :: hcomplex) = 0))";
   1.166 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a,
   1.167 +    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
   1.168 +qed "hcomplex_number_of_eq_cancel_iff2a";
   1.169 +Addsimps [hcomplex_number_of_eq_cancel_iff2a];
   1.170 +
   1.171 +Goalw [hcomplex_number_of_def] 
   1.172 +  "((number_of xa :: hcomplex) + iii * number_of ya = \
   1.173 +\    iii * number_of yb) = \
   1.174 +\  (((number_of xa :: hcomplex) = 0) & \
   1.175 +\   ((number_of ya :: hcomplex) = number_of yb))";
   1.176 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3,
   1.177 +    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
   1.178 +qed "hcomplex_number_of_eq_cancel_iff3";
   1.179 +Addsimps [hcomplex_number_of_eq_cancel_iff3];
   1.180 +
   1.181 +Goalw [hcomplex_number_of_def] 
   1.182 +  "((number_of xa :: hcomplex) + number_of ya * iii= \
   1.183 +\    iii * number_of yb) = \
   1.184 +\  (((number_of xa :: hcomplex) = 0) & \
   1.185 +\   ((number_of ya :: hcomplex) = number_of yb))";
   1.186 +by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a,
   1.187 +    hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
   1.188 +qed "hcomplex_number_of_eq_cancel_iff3a";
   1.189 +Addsimps [hcomplex_number_of_eq_cancel_iff3a];
   1.190 +*)
   1.191 +
   1.192 +lemma hcomplex_number_of_hcnj [simp]:
   1.193 +     "hcnj (number_of v :: hcomplex) = number_of v"
   1.194 +by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
   1.195 +               hcomplex_hcnj_hcomplex_of_hypreal)
   1.196 +
   1.197 +lemma hcomplex_number_of_hcmod [simp]: 
   1.198 +      "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
   1.199 +by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
   1.200 +               hcmod_hcomplex_of_hypreal)
   1.201 +
   1.202 +lemma hcomplex_number_of_hRe [simp]: 
   1.203 +      "hRe(number_of v :: hcomplex) = number_of v"
   1.204 +by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
   1.205 +               hRe_hcomplex_of_hypreal)
   1.206 +
   1.207 +lemma hcomplex_number_of_hIm [simp]: 
   1.208 +      "hIm(number_of v :: hcomplex) = 0"
   1.209 +by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
   1.210 +               hIm_hcomplex_of_hypreal)
   1.211 +
   1.212 +
   1.213  ML
   1.214  {*
   1.215  val hcomplex_zero_def = thm"hcomplex_zero_def";