1.1 --- a/src/HOL/Complex/NSComplexBin.ML Sat Feb 14 02:06:12 2004 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,595 +0,0 @@
1.4 -(* Title: NSComplexBin.ML
1.5 - Author: Jacques D. Fleuriot
1.6 - Copyright: 2001 University of Edinburgh
1.7 - Descrition: Binary arithmetic for the nonstandard complex numbers
1.8 -*)
1.9 -
1.10 -(** hcomplex_of_complex (coercion from complex to nonstandard complex) **)
1.11 -
1.12 -Goal "hcomplex_of_complex (number_of w) = number_of w";
1.13 -by (simp_tac (simpset() addsimps [hcomplex_number_of_def]) 1);
1.14 -qed "hcomplex_number_of";
1.15 -Addsimps [hcomplex_number_of];
1.16 -
1.17 -Goalw [hypreal_of_real_def]
1.18 - "hcomplex_of_hypreal (hypreal_of_real x) = \
1.19 -\ hcomplex_of_complex(complex_of_real x)";
1.20 -by (simp_tac (simpset() addsimps [hcomplex_of_hypreal,
1.21 - hcomplex_of_complex_def,complex_of_real_def]) 1);
1.22 -qed "hcomplex_of_hypreal_eq_hcomplex_of_complex";
1.23 -
1.24 -Goalw [complex_number_of_def,hypreal_number_of_def]
1.25 - "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)";
1.26 -by (rtac (hcomplex_of_hypreal_eq_hcomplex_of_complex RS sym) 1);
1.27 -qed "hcomplex_hypreal_number_of";
1.28 -
1.29 -Goalw [hcomplex_number_of_def] "Numeral0 = (0::hcomplex)";
1.30 -by(Simp_tac 1);
1.31 -qed "hcomplex_numeral_0_eq_0";
1.32 -
1.33 -Goalw [hcomplex_number_of_def] "Numeral1 = (1::hcomplex)";
1.34 -by(Simp_tac 1);
1.35 -qed "hcomplex_numeral_1_eq_1";
1.36 -
1.37 -(*
1.38 -Goal "z + hcnj z = \
1.39 -\ hcomplex_of_hypreal (2 * hRe(z))";
1.40 -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
1.41 -by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
1.42 - hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
1.43 -qed "hcomplex_add_hcnj";
1.44 -
1.45 -Goal "z - hcnj z = \
1.46 -\ hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii";
1.47 -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
1.48 -by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
1.49 - hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
1.50 - complex_diff_cnj,iii_def,hcomplex_mult]));
1.51 -qed "hcomplex_diff_hcnj";
1.52 -*)
1.53 -
1.54 -(** Addition **)
1.55 -
1.56 -Goal "(number_of v :: hcomplex) + number_of v' = number_of (bin_add v v')";
1.57 -by (simp_tac
1.58 - (HOL_ss addsimps [hcomplex_number_of_def,
1.59 - hcomplex_of_complex_add RS sym, add_complex_number_of]) 1);
1.60 -qed "add_hcomplex_number_of";
1.61 -Addsimps [add_hcomplex_number_of];
1.62 -
1.63 -
1.64 -(** Subtraction **)
1.65 -
1.66 -Goalw [hcomplex_number_of_def]
1.67 - "- (number_of w :: hcomplex) = number_of (bin_minus w)";
1.68 -by (simp_tac
1.69 - (HOL_ss addsimps [minus_complex_number_of, hcomplex_of_complex_minus RS sym]) 1);
1.70 -qed "minus_hcomplex_number_of";
1.71 -Addsimps [minus_hcomplex_number_of];
1.72 -
1.73 -Goalw [hcomplex_number_of_def, hcomplex_diff_def]
1.74 - "(number_of v :: hcomplex) - number_of w = \
1.75 -\ number_of (bin_add v (bin_minus w))";
1.76 -by (Simp_tac 1);
1.77 -qed "diff_hcomplex_number_of";
1.78 -Addsimps [diff_hcomplex_number_of];
1.79 -
1.80 -
1.81 -(** Multiplication **)
1.82 -
1.83 -Goal "(number_of v :: hcomplex) * number_of v' = number_of (bin_mult v v')";
1.84 -by (simp_tac
1.85 - (HOL_ss addsimps [hcomplex_number_of_def,
1.86 - hcomplex_of_complex_mult RS sym, mult_complex_number_of]) 1);
1.87 -qed "mult_hcomplex_number_of";
1.88 -Addsimps [mult_hcomplex_number_of];
1.89 -
1.90 -Goal "(2::hcomplex) = 1 + 1";
1.91 -by (simp_tac (simpset() addsimps [hcomplex_numeral_1_eq_1 RS sym]) 1);
1.92 -val lemma = result();
1.93 -
1.94 -(*For specialist use: NOT as default simprules*)
1.95 -Goal "2 * z = (z+z::hcomplex)";
1.96 -by (simp_tac (simpset() addsimps [lemma, hcomplex_add_mult_distrib]) 1);
1.97 -qed "hcomplex_mult_2";
1.98 -
1.99 -Goal "z * 2 = (z+z::hcomplex)";
1.100 -by (stac hcomplex_mult_commute 1 THEN rtac hcomplex_mult_2 1);
1.101 -qed "hcomplex_mult_2_right";
1.102 -
1.103 -(** Equals (=) **)
1.104 -
1.105 -Goal "((number_of v :: hcomplex) = number_of v') = \
1.106 -\ iszero (number_of (bin_add v (bin_minus v')) :: int)";
1.107 -by (simp_tac
1.108 - (HOL_ss addsimps [hcomplex_number_of_def,
1.109 - hcomplex_of_complex_eq_iff, eq_complex_number_of]) 1);
1.110 -qed "eq_hcomplex_number_of";
1.111 -Addsimps [eq_hcomplex_number_of];
1.112 -
1.113 -(*** New versions of existing theorems involving 0, 1hc ***)
1.114 -
1.115 -Goal "- 1 = (-1::hcomplex)";
1.116 -by (simp_tac (simpset() addsimps [hcomplex_numeral_1_eq_1 RS sym]) 1);
1.117 -qed "hcomplex_minus_1_eq_m1";
1.118 -
1.119 -Goal "-1 * z = -(z::hcomplex)";
1.120 -by (simp_tac (simpset() addsimps [hcomplex_minus_1_eq_m1 RS sym]) 1);
1.121 -qed "hcomplex_mult_minus1";
1.122 -
1.123 -Goal "z * -1 = -(z::hcomplex)";
1.124 -by (stac hcomplex_mult_commute 1 THEN rtac hcomplex_mult_minus1 1);
1.125 -qed "hcomplex_mult_minus1_right";
1.126 -
1.127 -Addsimps [hcomplex_mult_minus1,hcomplex_mult_minus1_right];
1.128 -
1.129 -(*Maps 0 to Numeral0 and 1 to Numeral1 and -Numeral1 to -1*)
1.130 -val hcomplex_numeral_ss =
1.131 - complex_numeral_ss addsimps [hcomplex_numeral_0_eq_0 RS sym, hcomplex_numeral_1_eq_1 RS sym,
1.132 - hcomplex_minus_1_eq_m1];
1.133 -
1.134 -fun rename_numerals th =
1.135 - asm_full_simplify hcomplex_numeral_ss (Thm.transfer (the_context ()) th);
1.136 -
1.137 -
1.138 -(*Now insert some identities previously stated for 0 and 1hc*)
1.139 -
1.140 -
1.141 -Addsimps [hcomplex_numeral_0_eq_0,hcomplex_numeral_1_eq_1];
1.142 -
1.143 -Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hcomplex)";
1.144 -by (auto_tac (claset(),simpset() addsimps [hcomplex_add_assoc RS sym]));
1.145 -qed "hcomplex_add_number_of_left";
1.146 -
1.147 -Goal "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::hcomplex)";
1.148 -by (simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym]) 1);
1.149 -qed "hcomplex_mult_number_of_left";
1.150 -
1.151 -Goalw [hcomplex_diff_def]
1.152 - "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::hcomplex)";
1.153 -by (rtac hcomplex_add_number_of_left 1);
1.154 -qed "hcomplex_add_number_of_diff1";
1.155 -
1.156 -Goal "number_of v + (c - number_of w) = \
1.157 -\ number_of (bin_add v (bin_minus w)) + (c::hcomplex)";
1.158 -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]@ add_ac));
1.159 -qed "hcomplex_add_number_of_diff2";
1.160 -
1.161 -Addsimps [hcomplex_add_number_of_left, hcomplex_mult_number_of_left,
1.162 - hcomplex_add_number_of_diff1, hcomplex_add_number_of_diff2];
1.163 -
1.164 -
1.165 -(**** Simprocs for numeric literals ****)
1.166 -
1.167 -structure HComplex_Numeral_Simprocs =
1.168 -struct
1.169 -
1.170 -(*Utilities*)
1.171 -
1.172 -val hcomplexT = Type("NSComplex.hcomplex",[]);
1.173 -
1.174 -fun mk_numeral n = HOLogic.number_of_const hcomplexT $ HOLogic.mk_bin n;
1.175 -
1.176 -val dest_numeral = Complex_Numeral_Simprocs.dest_numeral;
1.177 -
1.178 -val find_first_numeral = Complex_Numeral_Simprocs.find_first_numeral;
1.179 -
1.180 -val zero = mk_numeral 0;
1.181 -val mk_plus = HOLogic.mk_binop "op +";
1.182 -
1.183 -val uminus_const = Const ("uminus", hcomplexT --> hcomplexT);
1.184 -
1.185 -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
1.186 -fun mk_sum [] = zero
1.187 - | mk_sum [t,u] = mk_plus (t, u)
1.188 - | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
1.189 -
1.190 -(*this version ALWAYS includes a trailing zero*)
1.191 -fun long_mk_sum [] = zero
1.192 - | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
1.193 -
1.194 -val dest_plus = HOLogic.dest_bin "op +" hcomplexT;
1.195 -
1.196 -(*decompose additions AND subtractions as a sum*)
1.197 -fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
1.198 - dest_summing (pos, t, dest_summing (pos, u, ts))
1.199 - | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
1.200 - dest_summing (pos, t, dest_summing (not pos, u, ts))
1.201 - | dest_summing (pos, t, ts) =
1.202 - if pos then t::ts else uminus_const$t :: ts;
1.203 -
1.204 -fun dest_sum t = dest_summing (true, t, []);
1.205 -
1.206 -val mk_diff = HOLogic.mk_binop "op -";
1.207 -val dest_diff = HOLogic.dest_bin "op -" hcomplexT;
1.208 -
1.209 -val one = mk_numeral 1;
1.210 -val mk_times = HOLogic.mk_binop "op *";
1.211 -
1.212 -fun mk_prod [] = one
1.213 - | mk_prod [t] = t
1.214 - | mk_prod (t :: ts) = if t = one then mk_prod ts
1.215 - else mk_times (t, mk_prod ts);
1.216 -
1.217 -val dest_times = HOLogic.dest_bin "op *" hcomplexT;
1.218 -
1.219 -fun dest_prod t =
1.220 - let val (t,u) = dest_times t
1.221 - in dest_prod t @ dest_prod u end
1.222 - handle TERM _ => [t];
1.223 -
1.224 -(*DON'T do the obvious simplifications; that would create special cases*)
1.225 -fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
1.226 -
1.227 -(*Express t as a product of (possibly) a numeral with other sorted terms*)
1.228 -fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
1.229 - | dest_coeff sign t =
1.230 - let val ts = sort Term.term_ord (dest_prod t)
1.231 - val (n, ts') = find_first_numeral [] ts
1.232 - handle TERM _ => (1, ts)
1.233 - in (sign*n, mk_prod ts') end;
1.234 -
1.235 -(*Find first coefficient-term THAT MATCHES u*)
1.236 -fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
1.237 - | find_first_coeff past u (t::terms) =
1.238 - let val (n,u') = dest_coeff 1 t
1.239 - in if u aconv u' then (n, rev past @ terms)
1.240 - else find_first_coeff (t::past) u terms
1.241 - end
1.242 - handle TERM _ => find_first_coeff (t::past) u terms;
1.243 -
1.244 -
1.245 -
1.246 -(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
1.247 -val add_0s = map rename_numerals [hcomplex_add_zero_left, hcomplex_add_zero_right];
1.248 -val mult_plus_1s = map rename_numerals [hcomplex_mult_one_left, hcomplex_mult_one_right];
1.249 -val mult_minus_1s = map rename_numerals [hcomplex_mult_minus1, hcomplex_mult_minus1_right];
1.250 -val mult_1s = mult_plus_1s @ mult_minus_1s;
1.251 -
1.252 -(*To perform binary arithmetic*)
1.253 -val bin_simps =
1.254 - [hcomplex_numeral_0_eq_0 RS sym, hcomplex_numeral_1_eq_1 RS sym,
1.255 - add_hcomplex_number_of, hcomplex_add_number_of_left,
1.256 - minus_hcomplex_number_of, diff_hcomplex_number_of, mult_hcomplex_number_of,
1.257 - hcomplex_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
1.258 -
1.259 -(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
1.260 - during re-arrangement*)
1.261 -val non_add_bin_simps =
1.262 - bin_simps \\ [hcomplex_add_number_of_left, add_hcomplex_number_of];
1.263 -
1.264 -(*To evaluate binary negations of coefficients*)
1.265 -val hcomplex_minus_simps = NCons_simps @
1.266 - [hcomplex_minus_1_eq_m1,minus_hcomplex_number_of,
1.267 - bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
1.268 - bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
1.269 -
1.270 -
1.271 -(*To let us treat subtraction as addition*)
1.272 -val diff_simps = [hcomplex_diff_def, minus_add_distrib, minus_minus];
1.273 -
1.274 -(*push the unary minus down: - x * y = x * - y *)
1.275 -val hcomplex_minus_mult_eq_1_to_2 =
1.276 - [minus_mult_left RS sym, minus_mult_right] MRS trans
1.277 - |> standard;
1.278 -
1.279 -(*to extract again any uncancelled minuses*)
1.280 -val hcomplex_minus_from_mult_simps =
1.281 - [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
1.282 -
1.283 -(*combine unary minus with numeric literals, however nested within a product*)
1.284 -val hcomplex_mult_minus_simps =
1.285 - [hcomplex_mult_assoc, minus_mult_left, hcomplex_minus_mult_eq_1_to_2];
1.286 -
1.287 -(*Final simplification: cancel + and * *)
1.288 -val simplify_meta_eq =
1.289 - Int_Numeral_Simprocs.simplify_meta_eq
1.290 - [add_zero_left, add_zero_right,
1.291 - mult_zero_left, mult_zero_right, mult_1, mult_1_right];
1.292 -
1.293 -val prep_simproc = Complex_Numeral_Simprocs.prep_simproc;
1.294 -
1.295 -
1.296 -structure CancelNumeralsCommon =
1.297 - struct
1.298 - val mk_sum = mk_sum
1.299 - val dest_sum = dest_sum
1.300 - val mk_coeff = mk_coeff
1.301 - val dest_coeff = dest_coeff 1
1.302 - val find_first_coeff = find_first_coeff []
1.303 - val trans_tac = Real_Numeral_Simprocs.trans_tac
1.304 - val norm_tac =
1.305 - ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
1.306 - hcomplex_minus_simps@add_ac))
1.307 - THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
1.308 - THEN ALLGOALS
1.309 - (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
1.310 - add_ac@mult_ac))
1.311 - val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
1.312 - val simplify_meta_eq = simplify_meta_eq
1.313 - end;
1.314 -
1.315 -
1.316 -structure EqCancelNumerals = CancelNumeralsFun
1.317 - (open CancelNumeralsCommon
1.318 - val prove_conv = Bin_Simprocs.prove_conv
1.319 - val mk_bal = HOLogic.mk_eq
1.320 - val dest_bal = HOLogic.dest_bin "op =" hcomplexT
1.321 - val bal_add1 = eq_add_iff1 RS trans
1.322 - val bal_add2 = eq_add_iff2 RS trans
1.323 -);
1.324 -
1.325 -
1.326 -val cancel_numerals =
1.327 - map prep_simproc
1.328 - [("hcomplexeq_cancel_numerals",
1.329 - ["(l::hcomplex) + m = n", "(l::hcomplex) = m + n",
1.330 - "(l::hcomplex) - m = n", "(l::hcomplex) = m - n",
1.331 - "(l::hcomplex) * m = n", "(l::hcomplex) = m * n"],
1.332 - EqCancelNumerals.proc)];
1.333 -
1.334 -structure CombineNumeralsData =
1.335 - struct
1.336 - val add = op + : int*int -> int
1.337 - val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *)
1.338 - val dest_sum = dest_sum
1.339 - val mk_coeff = mk_coeff
1.340 - val dest_coeff = dest_coeff 1
1.341 - val left_distrib = combine_common_factor RS trans
1.342 - val prove_conv = Bin_Simprocs.prove_conv_nohyps
1.343 - val trans_tac = Real_Numeral_Simprocs.trans_tac
1.344 - val norm_tac =
1.345 - ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
1.346 - hcomplex_minus_simps@add_ac))
1.347 - THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
1.348 - THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
1.349 - add_ac@mult_ac))
1.350 - val numeral_simp_tac = ALLGOALS
1.351 - (simp_tac (HOL_ss addsimps add_0s@bin_simps))
1.352 - val simplify_meta_eq = simplify_meta_eq
1.353 - end;
1.354 -
1.355 -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
1.356 -
1.357 -val combine_numerals =
1.358 - prep_simproc ("hcomplex_combine_numerals",
1.359 - ["(i::hcomplex) + j", "(i::hcomplex) - j"],
1.360 - CombineNumerals.proc);
1.361 -
1.362 -(** Declarations for ExtractCommonTerm **)
1.363 -
1.364 -(*this version ALWAYS includes a trailing one*)
1.365 -fun long_mk_prod [] = one
1.366 - | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
1.367 -
1.368 -(*Find first term that matches u*)
1.369 -fun find_first past u [] = raise TERM("find_first", [])
1.370 - | find_first past u (t::terms) =
1.371 - if u aconv t then (rev past @ terms)
1.372 - else find_first (t::past) u terms
1.373 - handle TERM _ => find_first (t::past) u terms;
1.374 -
1.375 -(*Final simplification: cancel + and * *)
1.376 -fun cancel_simplify_meta_eq cancel_th th =
1.377 - Int_Numeral_Simprocs.simplify_meta_eq
1.378 - [hcomplex_mult_one_left, hcomplex_mult_one_right]
1.379 - (([th, cancel_th]) MRS trans);
1.380 -
1.381 -(*** Making constant folding work for 0 and 1 too ***)
1.382 -
1.383 -structure HComplexAbstractNumeralsData =
1.384 - struct
1.385 - val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
1.386 - val is_numeral = Bin_Simprocs.is_numeral
1.387 - val numeral_0_eq_0 = hcomplex_numeral_0_eq_0
1.388 - val numeral_1_eq_1 = hcomplex_numeral_1_eq_1
1.389 - val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars
1.390 - fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
1.391 - val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
1.392 - end
1.393 -
1.394 -structure HComplexAbstractNumerals = AbstractNumeralsFun (HComplexAbstractNumeralsData)
1.395 -
1.396 -(*For addition, we already have rules for the operand 0.
1.397 - Multiplication is omitted because there are already special rules for
1.398 - both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1.
1.399 - For the others, having three patterns is a compromise between just having
1.400 - one (many spurious calls) and having nine (just too many!) *)
1.401 -val eval_numerals =
1.402 - map prep_simproc
1.403 - [("hcomplex_add_eval_numerals",
1.404 - ["(m::hcomplex) + 1", "(m::hcomplex) + number_of v"],
1.405 - HComplexAbstractNumerals.proc add_hcomplex_number_of),
1.406 - ("hcomplex_diff_eval_numerals",
1.407 - ["(m::hcomplex) - 1", "(m::hcomplex) - number_of v"],
1.408 - HComplexAbstractNumerals.proc diff_hcomplex_number_of),
1.409 - ("hcomplex_eq_eval_numerals",
1.410 - ["(m::hcomplex) = 0", "(m::hcomplex) = 1", "(m::hcomplex) = number_of v"],
1.411 - HComplexAbstractNumerals.proc eq_hcomplex_number_of)]
1.412 -
1.413 -end;
1.414 -
1.415 -Addsimprocs HComplex_Numeral_Simprocs.eval_numerals;
1.416 -Addsimprocs HComplex_Numeral_Simprocs.cancel_numerals;
1.417 -Addsimprocs [HComplex_Numeral_Simprocs.combine_numerals];
1.418 -
1.419 -
1.420 -(*examples:
1.421 -print_depth 22;
1.422 -set timing;
1.423 -set trace_simp;
1.424 -fun test s = (Goal s, by (Simp_tac 1));
1.425 -
1.426 -test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hcomplex)";
1.427 -test " 2*u = (u::hcomplex)";
1.428 -test "(i + j + 12 + (k::hcomplex)) - 15 = y";
1.429 -test "(i + j + 12 + (k::hcomplex)) - 5 = y";
1.430 -
1.431 -test "( 2*x - (u*v) + y) - v* 3*u = (w::hcomplex)";
1.432 -test "( 2*x*u*v + (u*v)* 4 + y) - v*u* 4 = (w::hcomplex)";
1.433 -test "( 2*x*u*v + (u*v)* 4 + y) - v*u = (w::hcomplex)";
1.434 -test "u*v - (x*u*v + (u*v)* 4 + y) = (w::hcomplex)";
1.435 -
1.436 -test "(i + j + 12 + (k::hcomplex)) = u + 15 + y";
1.437 -test "(i + j* 2 + 12 + (k::hcomplex)) = j + 5 + y";
1.438 -
1.439 -test " 2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::hcomplex)";
1.440 -
1.441 -test "a + -(b+c) + b = (d::hcomplex)";
1.442 -test "a + -(b+c) - b = (d::hcomplex)";
1.443 -
1.444 -(*negative numerals*)
1.445 -test "(i + j + -2 + (k::hcomplex)) - (u + 5 + y) = zz";
1.446 -
1.447 -test "(i + j + -12 + (k::hcomplex)) - 15 = y";
1.448 -test "(i + j + 12 + (k::hcomplex)) - -15 = y";
1.449 -test "(i + j + -12 + (k::hcomplex)) - -15 = y";
1.450 -*)
1.451 -
1.452 -(** Constant folding for hcomplex plus and times **)
1.453 -
1.454 -structure HComplex_Times_Assoc_Data : ASSOC_FOLD_DATA =
1.455 -struct
1.456 - val ss = HOL_ss
1.457 - val eq_reflection = eq_reflection
1.458 - val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
1.459 - val T = HComplex_Numeral_Simprocs.hcomplexT
1.460 - val plus = Const ("op *", [T,T] ---> T)
1.461 - val add_ac = mult_ac
1.462 -end;
1.463 -
1.464 -structure HComplex_Times_Assoc = Assoc_Fold (HComplex_Times_Assoc_Data);
1.465 -
1.466 -Addsimprocs [HComplex_Times_Assoc.conv];
1.467 -
1.468 -Addsimps [hcomplex_of_complex_zero_iff];
1.469 -
1.470 -
1.471 -(** extra thms **)
1.472 -
1.473 -Goal "(hcnj z = 0) = (z = 0)";
1.474 -by (auto_tac (claset(),simpset() addsimps [hcomplex_hcnj_zero_iff]));
1.475 -qed "hcomplex_hcnj_num_zero_iff";
1.476 -Addsimps [hcomplex_hcnj_num_zero_iff];
1.477 -
1.478 -Goal "0 = Abs_hcomplex (hcomplexrel `` {%n. 0})";
1.479 -by (simp_tac (simpset() addsimps [hcomplex_zero_def RS meta_eq_to_obj_eq RS sym]) 1);
1.480 -qed "hcomplex_zero_num";
1.481 -
1.482 -Goal "1 = Abs_hcomplex (hcomplexrel `` {%n. 1})";
1.483 -by (simp_tac (simpset() addsimps [hcomplex_one_def RS meta_eq_to_obj_eq RS sym]) 1);
1.484 -qed "hcomplex_one_num";
1.485 -
1.486 -(*** Real and imaginary stuff ***)
1.487 -
1.488 -(*Convert???
1.489 -Goalw [hcomplex_number_of_def]
1.490 - "((number_of xa :: hcomplex) + iii * number_of ya = \
1.491 -\ number_of xb + iii * number_of yb) = \
1.492 -\ (((number_of xa :: hcomplex) = number_of xb) & \
1.493 -\ ((number_of ya :: hcomplex) = number_of yb))";
1.494 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff,
1.495 - hcomplex_hypreal_number_of]));
1.496 -qed "hcomplex_number_of_eq_cancel_iff";
1.497 -Addsimps [hcomplex_number_of_eq_cancel_iff];
1.498 -
1.499 -Goalw [hcomplex_number_of_def]
1.500 - "((number_of xa :: hcomplex) + number_of ya * iii = \
1.501 -\ number_of xb + number_of yb * iii) = \
1.502 -\ (((number_of xa :: hcomplex) = number_of xb) & \
1.503 -\ ((number_of ya :: hcomplex) = number_of yb))";
1.504 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA,
1.505 - hcomplex_hypreal_number_of]));
1.506 -qed "hcomplex_number_of_eq_cancel_iffA";
1.507 -Addsimps [hcomplex_number_of_eq_cancel_iffA];
1.508 -
1.509 -Goalw [hcomplex_number_of_def]
1.510 - "((number_of xa :: hcomplex) + number_of ya * iii = \
1.511 -\ number_of xb + iii * number_of yb) = \
1.512 -\ (((number_of xa :: hcomplex) = number_of xb) & \
1.513 -\ ((number_of ya :: hcomplex) = number_of yb))";
1.514 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB,
1.515 - hcomplex_hypreal_number_of]));
1.516 -qed "hcomplex_number_of_eq_cancel_iffB";
1.517 -Addsimps [hcomplex_number_of_eq_cancel_iffB];
1.518 -
1.519 -Goalw [hcomplex_number_of_def]
1.520 - "((number_of xa :: hcomplex) + iii * number_of ya = \
1.521 -\ number_of xb + number_of yb * iii) = \
1.522 -\ (((number_of xa :: hcomplex) = number_of xb) & \
1.523 -\ ((number_of ya :: hcomplex) = number_of yb))";
1.524 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC,
1.525 - hcomplex_hypreal_number_of]));
1.526 -qed "hcomplex_number_of_eq_cancel_iffC";
1.527 -Addsimps [hcomplex_number_of_eq_cancel_iffC];
1.528 -
1.529 -Goalw [hcomplex_number_of_def]
1.530 - "((number_of xa :: hcomplex) + iii * number_of ya = \
1.531 -\ number_of xb) = \
1.532 -\ (((number_of xa :: hcomplex) = number_of xb) & \
1.533 -\ ((number_of ya :: hcomplex) = 0))";
1.534 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2,
1.535 - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
1.536 -qed "hcomplex_number_of_eq_cancel_iff2";
1.537 -Addsimps [hcomplex_number_of_eq_cancel_iff2];
1.538 -
1.539 -Goalw [hcomplex_number_of_def]
1.540 - "((number_of xa :: hcomplex) + number_of ya * iii = \
1.541 -\ number_of xb) = \
1.542 -\ (((number_of xa :: hcomplex) = number_of xb) & \
1.543 -\ ((number_of ya :: hcomplex) = 0))";
1.544 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a,
1.545 - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
1.546 -qed "hcomplex_number_of_eq_cancel_iff2a";
1.547 -Addsimps [hcomplex_number_of_eq_cancel_iff2a];
1.548 -
1.549 -Goalw [hcomplex_number_of_def]
1.550 - "((number_of xa :: hcomplex) + iii * number_of ya = \
1.551 -\ iii * number_of yb) = \
1.552 -\ (((number_of xa :: hcomplex) = 0) & \
1.553 -\ ((number_of ya :: hcomplex) = number_of yb))";
1.554 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3,
1.555 - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
1.556 -qed "hcomplex_number_of_eq_cancel_iff3";
1.557 -Addsimps [hcomplex_number_of_eq_cancel_iff3];
1.558 -
1.559 -Goalw [hcomplex_number_of_def]
1.560 - "((number_of xa :: hcomplex) + number_of ya * iii= \
1.561 -\ iii * number_of yb) = \
1.562 -\ (((number_of xa :: hcomplex) = 0) & \
1.563 -\ ((number_of ya :: hcomplex) = number_of yb))";
1.564 -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a,
1.565 - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
1.566 -qed "hcomplex_number_of_eq_cancel_iff3a";
1.567 -Addsimps [hcomplex_number_of_eq_cancel_iff3a];
1.568 -*)
1.569 -
1.570 -Goalw [hcomplex_number_of_def] "hcnj (number_of v :: hcomplex) = number_of v";
1.571 -by (rtac (hcomplex_hypreal_number_of RS ssubst) 1);
1.572 -by (rtac hcomplex_hcnj_hcomplex_of_hypreal 1);
1.573 -qed "hcomplex_number_of_hcnj";
1.574 -Addsimps [hcomplex_number_of_hcnj];
1.575 -
1.576 -Goalw [hcomplex_number_of_def]
1.577 - "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)";
1.578 -by (rtac (hcomplex_hypreal_number_of RS ssubst) 1);
1.579 -by (auto_tac (claset(), HOL_ss addsimps [hcmod_hcomplex_of_hypreal]));
1.580 -qed "hcomplex_number_of_hcmod";
1.581 -Addsimps [hcomplex_number_of_hcmod];
1.582 -
1.583 -Goalw [hcomplex_number_of_def]
1.584 - "hRe(number_of v :: hcomplex) = number_of v";
1.585 -by (rtac (hcomplex_hypreal_number_of RS ssubst) 1);
1.586 -by (auto_tac (claset(), HOL_ss addsimps [hRe_hcomplex_of_hypreal]));
1.587 -qed "hcomplex_number_of_hRe";
1.588 -Addsimps [hcomplex_number_of_hRe];
1.589 -
1.590 -Goalw [hcomplex_number_of_def]
1.591 - "hIm(number_of v :: hcomplex) = 0";
1.592 -by (rtac (hcomplex_hypreal_number_of RS ssubst) 1);
1.593 -by (auto_tac (claset(), HOL_ss addsimps [hIm_hcomplex_of_hypreal]));
1.594 -qed "hcomplex_number_of_hIm";
1.595 -Addsimps [hcomplex_number_of_hIm];
1.596 -
1.597 -
1.598 -