(* Title: HOL/Hyperreal/HyperRealArith0.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
Assorted facts that need binary literals and the arithmetic decision procedure
Also, common factor cancellation
*)
local
open Hyperreal_Numeral_Simprocs
in
val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of,
le_hypreal_number_of_eq_not_less];
structure CancelNumeralFactorCommon =
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val trans_tac = Real_Numeral_Simprocs.trans_tac
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps @ mult_1s))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_mult_ac))
val numeral_simp_tac =
ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps))
val simplify_meta_eq = simplify_meta_eq
end
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
val cancel = mult_divide_cancel_left RS trans
val neg_exchanges = false
)
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" hyprealT
val cancel = mult_cancel_left RS trans
val neg_exchanges = false
)
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" hyprealT
val cancel = mult_less_cancel_left RS trans
val neg_exchanges = true
)
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" hyprealT
val cancel = mult_le_cancel_left RS trans
val neg_exchanges = true
)
val hypreal_cancel_numeral_factors_relations =
map prep_simproc
[("hyprealeq_cancel_numeral_factor",
["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
EqCancelNumeralFactor.proc),
("hyprealless_cancel_numeral_factor",
["(l::hypreal) * m < n", "(l::hypreal) < m * n"],
LessCancelNumeralFactor.proc),
("hyprealle_cancel_numeral_factor",
["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
LeCancelNumeralFactor.proc)];
val hypreal_cancel_numeral_factors_divide = prep_simproc
("hyprealdiv_cancel_numeral_factor",
["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)",
"((number_of v)::hypreal) / (number_of w)"],
DivCancelNumeralFactor.proc);
val hypreal_cancel_numeral_factors =
hypreal_cancel_numeral_factors_relations @
[hypreal_cancel_numeral_factors_divide];
end;
Addsimprocs hypreal_cancel_numeral_factors;
(*examples:
print_depth 22;
set timing;
set trace_simp;
fun test s = (Goal s; by (Simp_tac 1));
test "0 <= (y::hypreal) * -2";
test "9*x = 12 * (y::hypreal)";
test "(9*x) / (12 * (y::hypreal)) = z";
test "9*x < 12 * (y::hypreal)";
test "9*x <= 12 * (y::hypreal)";
test "-99*x = 123 * (y::hypreal)";
test "(-99*x) / (123 * (y::hypreal)) = z";
test "-99*x < 123 * (y::hypreal)";
test "-99*x <= 123 * (y::hypreal)";
test "999*x = -396 * (y::hypreal)";
test "(999*x) / (-396 * (y::hypreal)) = z";
test "999*x < -396 * (y::hypreal)";
test "999*x <= -396 * (y::hypreal)";
test "-99*x = -81 * (y::hypreal)";
test "(-99*x) / (-81 * (y::hypreal)) = z";
test "-99*x <= -81 * (y::hypreal)";
test "-99*x < -81 * (y::hypreal)";
test "-2 * x = -1 * (y::hypreal)";
test "-2 * x = -(y::hypreal)";
test "(-2 * x) / (-1 * (y::hypreal)) = z";
test "-2 * x < -(y::hypreal)";
test "-2 * x <= -1 * (y::hypreal)";
test "-x < -23 * (y::hypreal)";
test "-x <= -23 * (y::hypreal)";
*)
(** Declarations for ExtractCommonTerm **)
local
open Hyperreal_Numeral_Simprocs
in
structure CancelFactorCommon =
struct
val mk_sum = long_mk_prod
val dest_sum = dest_prod
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first []
val trans_tac = Real_Numeral_Simprocs.trans_tac
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hypreal_mult_ac))
end;
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" hyprealT
val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
);
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
);
val hypreal_cancel_factor =
map prep_simproc
[("hypreal_eq_cancel_factor", ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
EqCancelFactor.proc),
("hypreal_divide_cancel_factor", ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"],
DivideCancelFactor.proc)];
end;
Addsimprocs hypreal_cancel_factor;
(*examples:
print_depth 22;
set timing;
set trace_simp;
fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::hypreal)";
test "k = k*(y::hypreal)";
test "a*(b*c) = (b::hypreal)";
test "a*(b*c) = d*(b::hypreal)*(x*a)";
test "(x*k) / (k*(y::hypreal)) = (uu::hypreal)";
test "(k) / (k*(y::hypreal)) = (uu::hypreal)";
test "(a*(b*c)) / ((b::hypreal)) = (uu::hypreal)";
test "(a*(b*c)) / (d*(b::hypreal)*(x*a)) = (uu::hypreal)";
(*FIXME: what do we do about this?*)
test "a*(b*c)/(y*z) = d*(b::hypreal)*(x*a)/z";
*)
(** Division by 1, -1 **)
Goal "x/-1 = -(x::hypreal)";
by (Simp_tac 1);
qed "hypreal_divide_minus1";
Addsimps [hypreal_divide_minus1];
Goal "-1/(x::hypreal) = - (1/x)";
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
qed "hypreal_minus1_divide";
Addsimps [hypreal_minus1_divide];
(*** General rewrites to improve automation, like those for type "int" ***)
(** The next several equations can make the simplifier loop! **)
Goal "(x < - y) = (y < - (x::hypreal))";
by Auto_tac;
qed "hypreal_less_minus";
Goal "(- x < y) = (- y < (x::hypreal))";
by Auto_tac;
qed "hypreal_minus_less";
Goal "(x <= - y) = (y <= - (x::hypreal))";
by Auto_tac;
qed "hypreal_le_minus";
Goal "(- x <= y) = (- y <= (x::hypreal))";
by Auto_tac;
qed "hypreal_minus_le";
Goal "(x = - y) = (y = - (x::hypreal))";
by Auto_tac;
qed "hypreal_equation_minus";
Goal "(- x = y) = (- (y::hypreal) = x)";
by Auto_tac;
qed "hypreal_minus_equation";
Goal "(x + - a = (0::hypreal)) = (x=a)";
by (arith_tac 1);
qed "hypreal_add_minus_iff";
Addsimps [hypreal_add_minus_iff];
Goal "(-b = -a) = (b = (a::hypreal))";
by (arith_tac 1);
qed "hypreal_minus_eq_cancel";
Addsimps [hypreal_minus_eq_cancel];
Goal "(-s <= -r) = ((r::hypreal) <= s)";
by (stac hypreal_minus_le 1);
by (Simp_tac 1);
qed "hypreal_le_minus_iff";
Addsimps [hypreal_le_minus_iff];
(*** Simprules combining x+y and 0 ***)
Goal "(x+y = (0::hypreal)) = (y = -x)";
by Auto_tac;
qed "hypreal_add_eq_0_iff";
AddIffs [hypreal_add_eq_0_iff];
Goal "(x+y < (0::hypreal)) = (y < -x)";
by Auto_tac;
qed "hypreal_add_less_0_iff";
AddIffs [hypreal_add_less_0_iff];
Goal "((0::hypreal) < x+y) = (-x < y)";
by Auto_tac;
qed "hypreal_0_less_add_iff";
AddIffs [hypreal_0_less_add_iff];
Goal "(x+y <= (0::hypreal)) = (y <= -x)";
by Auto_tac;
qed "hypreal_add_le_0_iff";
AddIffs [hypreal_add_le_0_iff];
Goal "((0::hypreal) <= x+y) = (-x <= y)";
by Auto_tac;
qed "hypreal_0_le_add_iff";
AddIffs [hypreal_0_le_add_iff];
(** Simprules combining x-y and 0; see also hypreal_less_iff_diff_less_0 etc
in HyperBin
**)
Goal "((0::hypreal) < x-y) = (y < x)";
by Auto_tac;
qed "hypreal_0_less_diff_iff";
AddIffs [hypreal_0_less_diff_iff];
Goal "((0::hypreal) <= x-y) = (y <= x)";
by Auto_tac;
qed "hypreal_0_le_diff_iff";
AddIffs [hypreal_0_le_diff_iff];
(*
FIXME: we should have this, as for type int, but many proofs would break.
It replaces x+-y by x-y.
Addsimps [symmetric hypreal_diff_def];
*)
Goal "-(x-y) = y - (x::hypreal)";
by (arith_tac 1);
qed "hypreal_minus_diff_eq";
Addsimps [hypreal_minus_diff_eq];