paulson@14352: (* Title: HOL/Real/real_arith0.ML wenzelm@9436: ID: $Id$ wenzelm@9436: Author: Tobias Nipkow, TU Muenchen paulson@14352: Copyright 1999 TU Muenchen wenzelm@9436: paulson@14352: Simprocs for common factor cancellation & Rational coefficient handling paulson@14352: paulson@14352: Instantiation of the generic linear arithmetic package for type real. wenzelm@9436: *) wenzelm@9436: paulson@14365: (*FIXME DELETE*) paulson@14365: val real_mult_left_mono = paulson@14365: read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono; paulson@14365: paulson@14387: val real_abs_def = thm "real_abs_def"; paulson@14365: paulson@14387: val real_le_def = thm "real_le_def"; paulson@14387: val real_diff_def = thm "real_diff_def"; paulson@14387: val real_divide_def = thm "real_divide_def"; paulson@14365: paulson@14387: val realrel_iff = thm"realrel_iff"; paulson@14387: val realrel_refl = thm"realrel_refl"; paulson@14387: val equiv_realrel = thm"equiv_realrel"; paulson@14387: val equiv_realrel_iff = thm"equiv_realrel_iff"; paulson@14387: val realrel_in_real = thm"realrel_in_real"; paulson@14387: val inj_on_Abs_REAL = thm"inj_on_Abs_REAL"; paulson@14387: val eq_realrelD = thm"eq_realrelD"; paulson@14387: val inj_Rep_REAL = thm"inj_Rep_REAL"; paulson@14387: val inj_real_of_preal = thm"inj_real_of_preal"; paulson@14387: val eq_Abs_REAL = thm"eq_Abs_REAL"; paulson@14387: val real_minus_congruent = thm"real_minus_congruent"; paulson@14387: val real_minus = thm"real_minus"; paulson@14387: val real_add = thm"real_add"; paulson@14387: val real_add_commute = thm"real_add_commute"; paulson@14387: val real_add_assoc = thm"real_add_assoc"; paulson@14387: val real_add_zero_left = thm"real_add_zero_left"; paulson@14387: val real_add_zero_right = thm"real_add_zero_right"; paulson@14365: paulson@14387: val real_mult = thm"real_mult"; paulson@14387: val real_mult_commute = thm"real_mult_commute"; paulson@14387: val real_mult_assoc = thm"real_mult_assoc"; paulson@14387: val real_mult_1 = thm"real_mult_1"; paulson@14387: val real_mult_1_right = thm"real_mult_1_right"; paulson@14387: val preal_le_linear = thm"preal_le_linear"; paulson@14387: val real_mult_inverse_left = thm"real_mult_inverse_left"; paulson@14387: val real_not_refl2 = thm"real_not_refl2"; paulson@14387: val real_of_preal_add = thm"real_of_preal_add"; paulson@14387: val real_of_preal_mult = thm"real_of_preal_mult"; paulson@14387: val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; paulson@14387: val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; paulson@14387: val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; paulson@14387: val real_of_preal_zero_less = thm"real_of_preal_zero_less"; paulson@14387: val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; paulson@14387: val real_le_refl = thm"real_le_refl"; paulson@14387: val real_le_linear = thm"real_le_linear"; paulson@14387: val real_le_trans = thm"real_le_trans"; paulson@14387: val real_le_anti_sym = thm"real_le_anti_sym"; paulson@14387: val real_less_le = thm"real_less_le"; paulson@14387: val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; paulson@14387: val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex"; paulson@14387: val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex"; paulson@14387: val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex"; paulson@14387: val real_less_all_preal = thm "real_less_all_preal"; paulson@14387: val real_less_all_real2 = thm "real_less_all_real2"; paulson@14387: val real_of_preal_le_iff = thm "real_of_preal_le_iff"; paulson@14387: val real_mult_order = thm "real_mult_order"; paulson@14387: val real_zero_less_one = thm "real_zero_less_one"; paulson@14387: val real_add_less_le_mono = thm "real_add_less_le_mono"; paulson@14387: val real_add_le_less_mono = thm "real_add_le_less_mono"; paulson@14387: val real_add_order = thm "real_add_order"; paulson@14387: val real_le_add_order = thm "real_le_add_order"; paulson@14387: val real_le_square = thm "real_le_square"; paulson@14387: val real_mult_less_mono2 = thm "real_mult_less_mono2"; paulson@14289: paulson@14387: val real_mult_less_iff1 = thm "real_mult_less_iff1"; paulson@14387: val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; paulson@14387: val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; paulson@14387: val real_mult_less_mono = thm "real_mult_less_mono"; paulson@14387: val real_mult_less_mono' = thm "real_mult_less_mono'"; paulson@14387: val real_sum_squares_cancel = thm "real_sum_squares_cancel"; paulson@14387: val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; paulson@14289: paulson@14387: val real_mult_left_cancel = thm"real_mult_left_cancel"; paulson@14387: val real_mult_right_cancel = thm"real_mult_right_cancel"; paulson@14387: val real_inverse_unique = thm "real_inverse_unique"; paulson@14387: val real_inverse_gt_one = thm "real_inverse_gt_one"; paulson@14289: paulson@14387: val real_of_int_zero = thm"real_of_int_zero"; paulson@14387: val real_of_one = thm"real_of_one"; paulson@14387: val real_of_int_add = thm"real_of_int_add"; paulson@14387: val real_of_int_minus = thm"real_of_int_minus"; paulson@14387: val real_of_int_diff = thm"real_of_int_diff"; paulson@14387: val real_of_int_mult = thm"real_of_int_mult"; paulson@14387: val real_of_int_real_of_nat = thm"real_of_int_real_of_nat"; paulson@14387: val real_of_int_inject = thm"real_of_int_inject"; paulson@14387: val real_of_int_less_iff = thm"real_of_int_less_iff"; paulson@14387: val real_of_int_le_iff = thm"real_of_int_le_iff"; paulson@14387: val real_of_nat_zero = thm "real_of_nat_zero"; paulson@14387: val real_of_nat_one = thm "real_of_nat_one"; paulson@14387: val real_of_nat_add = thm "real_of_nat_add"; paulson@14387: val real_of_nat_Suc = thm "real_of_nat_Suc"; paulson@14387: val real_of_nat_less_iff = thm "real_of_nat_less_iff"; paulson@14387: val real_of_nat_le_iff = thm "real_of_nat_le_iff"; paulson@14387: val real_of_nat_ge_zero = thm "real_of_nat_ge_zero"; paulson@14387: val real_of_nat_Suc_gt_zero = thm "real_of_nat_Suc_gt_zero"; paulson@14387: val real_of_nat_mult = thm "real_of_nat_mult"; paulson@14387: val real_of_nat_inject = thm "real_of_nat_inject"; paulson@14387: val real_of_nat_diff = thm "real_of_nat_diff"; paulson@14387: val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; paulson@14387: val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff"; paulson@14387: val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff"; paulson@14387: val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero"; paulson@14387: val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff"; paulson@14352: paulson@14352: paulson@14352: (****Instantiation of the generic linear arithmetic package****) paulson@14352: paulson@14289: local paulson@14289: nipkow@10693: fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; nipkow@10693: nipkow@10693: val real_mult_mono_thms = nipkow@10693: [(rotate_prems 1 real_mult_less_mono2, nipkow@10693: cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))), paulson@14334: (real_mult_left_mono, paulson@14334: cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] nipkow@10693: paulson@14369: val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, paulson@14369: real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym, paulson@14369: real_of_int_minus RS sym, real_of_int_diff RS sym, paulson@14387: real_of_int_mult RS sym]; nipkow@14355: nipkow@14355: val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2, nipkow@14355: real_of_int_inject RS iffD2]; nipkow@14355: nipkow@14355: val nat_inj_thms = [real_of_nat_le_iff RS iffD2, real_of_nat_less_iff RS iffD2, nipkow@14355: real_of_nat_inject RS iffD2]; paulson@14352: wenzelm@9436: in wenzelm@9436: paulson@14387: val fast_real_arith_simproc = paulson@14387: Simplifier.simproc (Theory.sign_of (the_context ())) paulson@14352: "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] paulson@14352: Fast_Arith.lin_arith_prover; paulson@14352: wenzelm@9436: val real_arith_setup = nipkow@10693: [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => paulson@14368: {add_mono_thms = add_mono_thms, nipkow@10693: mult_mono_thms = mult_mono_thms @ real_mult_mono_thms, nipkow@14355: inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, paulson@14365: lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*) paulson@14387: simpset = simpset addsimps simps}), nipkow@14355: arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT), nipkow@14355: arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT), paulson@14352: arith_discrete ("RealDef.real",false), paulson@14352: Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]]; paulson@14352: paulson@14352: (* some thms for injection nat => real: paulson@14352: real_of_nat_zero paulson@14352: real_of_nat_add paulson@14352: *) wenzelm@9436: wenzelm@9436: end; wenzelm@9436: paulson@14352: paulson@14352: (* Some test data [omitting examples that assume the ordering to be discrete!] paulson@14352: Goal "!!a::real. [| a <= b; c <= d; x+y a+c <= b+d"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; paulson@14352: by (arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ paulson@14352: \ ==> a <= l"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ paulson@14352: \ ==> a+a+a+a <= l+l+l+l"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ paulson@14352: \ ==> a+a+a+a+a <= l+l+l+l+i"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ paulson@14352: \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ paulson@14352: \ ==> 6*a <= 5*l+i"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "a<=b ==> a < b+(1::real)"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "a<=b ==> a-(3::real) < b"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: paulson@14352: Goal "a<=b ==> a-(1::real) < b"; paulson@14352: by (fast_arith_tac 1); paulson@14352: qed ""; paulson@14352: wenzelm@9436: *) paulson@14352: paulson@14352: paulson@14352: