# HG changeset patch # User haftmann # Date 1237790467 -3600 # Node ID a400b06d03cbfc6546fc35d5340b7170b599844d # Parent 94b74365ceb92446e8cdc83613d878700073d06f# Parent 79e2d95649fe68a5e6a6bf06bdea0dc0557d6a92 merged diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Arith_Tools.thy --- a/src/HOL/Arith_Tools.thy Sun Mar 22 21:48:14 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,388 +0,0 @@ -(* Title: HOL/Arith_Tools.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Amine Chaieb, TU Muenchen -*) - -header {* Setup of arithmetic tools *} - -theory Arith_Tools -imports NatBin -uses - "~~/src/Provers/Arith/cancel_numeral_factor.ML" - "~~/src/Provers/Arith/extract_common_term.ML" - "Tools/int_factor_simprocs.ML" - "Tools/nat_simprocs.ML" - "Tools/Qelim/qelim.ML" -begin - -subsection {* Simprocs for the Naturals *} - -declaration {* K nat_simprocs_setup *} - -subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} - -text{*Where K above is a literal*} - -lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)" -by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) - -text {*Now just instantiating @{text n} to @{text "number_of v"} does - the right simplification, but with some redundant inequality - tests.*} -lemma neg_number_of_pred_iff_0: - "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))" -apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ") -apply (simp only: less_Suc_eq_le le_0_eq) -apply (subst less_number_of_Suc, simp) -done - -text{*No longer required as a simprule because of the @{text inverse_fold} - simproc*} -lemma Suc_diff_number_of: - "Int.Pls < v ==> - Suc m - (number_of v) = m - (number_of (Int.pred v))" -apply (subst Suc_diff_eq_diff_pred) -apply simp -apply (simp del: nat_numeral_1_eq_1) -apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] - neg_number_of_pred_iff_0) -done - -lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" -by (simp add: numerals split add: nat_diff_split) - - -subsubsection{*For @{term nat_case} and @{term nat_rec}*} - -lemma nat_case_number_of [simp]: - "nat_case a f (number_of v) = - (let pv = number_of (Int.pred v) in - if neg pv then a else f (nat pv))" -by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0) - -lemma nat_case_add_eq_if [simp]: - "nat_case a f ((number_of v) + n) = - (let pv = number_of (Int.pred v) in - if neg pv then nat_case a f n else f (nat pv + n))" -apply (subst add_eq_if) -apply (simp split add: nat.split - del: nat_numeral_1_eq_1 - add: nat_numeral_1_eq_1 [symmetric] - numeral_1_eq_Suc_0 [symmetric] - neg_number_of_pred_iff_0) -done - -lemma nat_rec_number_of [simp]: - "nat_rec a f (number_of v) = - (let pv = number_of (Int.pred v) in - if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" -apply (case_tac " (number_of v) ::nat") -apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0) -apply (simp split add: split_if_asm) -done - -lemma nat_rec_add_eq_if [simp]: - "nat_rec a f (number_of v + n) = - (let pv = number_of (Int.pred v) in - if neg pv then nat_rec a f n - else f (nat pv + n) (nat_rec a f (nat pv + n)))" -apply (subst add_eq_if) -apply (simp split add: nat.split - del: nat_numeral_1_eq_1 - add: nat_numeral_1_eq_1 [symmetric] - numeral_1_eq_Suc_0 [symmetric] - neg_number_of_pred_iff_0) -done - - -subsubsection{*Various Other Lemmas*} - -text {*Evens and Odds, for Mutilated Chess Board*} - -text{*Lemmas for specialist use, NOT as default simprules*} -lemma nat_mult_2: "2 * z = (z+z::nat)" -proof - - have "2*z = (1 + 1)*z" by simp - also have "... = z+z" by (simp add: left_distrib) - finally show ?thesis . -qed - -lemma nat_mult_2_right: "z * 2 = (z+z::nat)" -by (subst mult_commute, rule nat_mult_2) - -text{*Case analysis on @{term "n<2"}*} -lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" -by arith - -lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)" -by arith - -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" -by (simp add: nat_mult_2 [symmetric]) - -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" -apply (subgoal_tac "m mod 2 < 2") -apply (erule less_2_cases [THEN disjE]) -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) -done - -lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)" -apply (subgoal_tac "m mod 2 < 2") -apply (force simp del: mod_less_divisor, simp) -done - -text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} - -lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" -by simp - -lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" -by simp - -text{*Can be used to eliminate long strings of Sucs, but not by default*} -lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" -by simp - - -text{*These lemmas collapse some needless occurrences of Suc: - at least three Sucs, since two and fewer are rewritten back to Suc again! - We already have some rules to simplify operands smaller than 3.*} - -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" -by (simp add: Suc3_eq_add_3) - -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" -by (simp add: Suc3_eq_add_3) - -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" -by (simp add: Suc3_eq_add_3) - -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" -by (simp add: Suc3_eq_add_3) - -lemmas Suc_div_eq_add3_div_number_of = - Suc_div_eq_add3_div [of _ "number_of v", standard] -declare Suc_div_eq_add3_div_number_of [simp] - -lemmas Suc_mod_eq_add3_mod_number_of = - Suc_mod_eq_add3_mod [of _ "number_of v", standard] -declare Suc_mod_eq_add3_mod_number_of [simp] - - -subsubsection{*Special Simplification for Constants*} - -text{*These belong here, late in the development of HOL, to prevent their -interfering with proofs of abstract properties of instances of the function -@{term number_of}*} - -text{*These distributive laws move literals inside sums and differences.*} -lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard] -declare left_distrib_number_of [simp] - -lemmas right_distrib_number_of = right_distrib [of "number_of v", standard] -declare right_distrib_number_of [simp] - - -lemmas left_diff_distrib_number_of = - left_diff_distrib [of _ _ "number_of v", standard] -declare left_diff_distrib_number_of [simp] - -lemmas right_diff_distrib_number_of = - right_diff_distrib [of "number_of v", standard] -declare right_diff_distrib_number_of [simp] - - -text{*These are actually for fields, like real: but where else to put them?*} -lemmas zero_less_divide_iff_number_of = - zero_less_divide_iff [of "number_of w", standard] -declare zero_less_divide_iff_number_of [simp,noatp] - -lemmas divide_less_0_iff_number_of = - divide_less_0_iff [of "number_of w", standard] -declare divide_less_0_iff_number_of [simp,noatp] - -lemmas zero_le_divide_iff_number_of = - zero_le_divide_iff [of "number_of w", standard] -declare zero_le_divide_iff_number_of [simp,noatp] - -lemmas divide_le_0_iff_number_of = - divide_le_0_iff [of "number_of w", standard] -declare divide_le_0_iff_number_of [simp,noatp] - - -(**** -IF times_divide_eq_right and times_divide_eq_left are removed as simprules, -then these special-case declarations may be useful. - -text{*These simprules move numerals into numerators and denominators.*} -lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)" -by (simp add: times_divide_eq) - -lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)" -by (simp add: times_divide_eq) - -lemmas times_divide_eq_right_number_of = - times_divide_eq_right [of "number_of w", standard] -declare times_divide_eq_right_number_of [simp] - -lemmas times_divide_eq_right_number_of = - times_divide_eq_right [of _ _ "number_of w", standard] -declare times_divide_eq_right_number_of [simp] - -lemmas times_divide_eq_left_number_of = - times_divide_eq_left [of _ "number_of w", standard] -declare times_divide_eq_left_number_of [simp] - -lemmas times_divide_eq_left_number_of = - times_divide_eq_left [of _ _ "number_of w", standard] -declare times_divide_eq_left_number_of [simp] - -****) - -text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks - strange, but then other simprocs simplify the quotient.*} - -lemmas inverse_eq_divide_number_of = - inverse_eq_divide [of "number_of w", standard] -declare inverse_eq_divide_number_of [simp] - - -text {*These laws simplify inequalities, moving unary minus from a term -into the literal.*} -lemmas less_minus_iff_number_of = - less_minus_iff [of "number_of v", standard] -declare less_minus_iff_number_of [simp,noatp] - -lemmas le_minus_iff_number_of = - le_minus_iff [of "number_of v", standard] -declare le_minus_iff_number_of [simp,noatp] - -lemmas equation_minus_iff_number_of = - equation_minus_iff [of "number_of v", standard] -declare equation_minus_iff_number_of [simp,noatp] - - -lemmas minus_less_iff_number_of = - minus_less_iff [of _ "number_of v", standard] -declare minus_less_iff_number_of [simp,noatp] - -lemmas minus_le_iff_number_of = - minus_le_iff [of _ "number_of v", standard] -declare minus_le_iff_number_of [simp,noatp] - -lemmas minus_equation_iff_number_of = - minus_equation_iff [of _ "number_of v", standard] -declare minus_equation_iff_number_of [simp,noatp] - - -text{*To Simplify Inequalities Where One Side is the Constant 1*} - -lemma less_minus_iff_1 [simp,noatp]: - fixes b::"'b::{ordered_idom,number_ring}" - shows "(1 < - b) = (b < -1)" -by auto - -lemma le_minus_iff_1 [simp,noatp]: - fixes b::"'b::{ordered_idom,number_ring}" - shows "(1 \ - b) = (b \ -1)" -by auto - -lemma equation_minus_iff_1 [simp,noatp]: - fixes b::"'b::number_ring" - shows "(1 = - b) = (b = -1)" -by (subst equation_minus_iff, auto) - -lemma minus_less_iff_1 [simp,noatp]: - fixes a::"'b::{ordered_idom,number_ring}" - shows "(- a < 1) = (-1 < a)" -by auto - -lemma minus_le_iff_1 [simp,noatp]: - fixes a::"'b::{ordered_idom,number_ring}" - shows "(- a \ 1) = (-1 \ a)" -by auto - -lemma minus_equation_iff_1 [simp,noatp]: - fixes a::"'b::number_ring" - shows "(- a = 1) = (a = -1)" -by (subst minus_equation_iff, auto) - - -text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\"}) *} - -lemmas mult_less_cancel_left_number_of = - mult_less_cancel_left [of "number_of v", standard] -declare mult_less_cancel_left_number_of [simp,noatp] - -lemmas mult_less_cancel_right_number_of = - mult_less_cancel_right [of _ "number_of v", standard] -declare mult_less_cancel_right_number_of [simp,noatp] - -lemmas mult_le_cancel_left_number_of = - mult_le_cancel_left [of "number_of v", standard] -declare mult_le_cancel_left_number_of [simp,noatp] - -lemmas mult_le_cancel_right_number_of = - mult_le_cancel_right [of _ "number_of v", standard] -declare mult_le_cancel_right_number_of [simp,noatp] - - -text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\"} and @{text "="}) *} - -lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard] -lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard] -lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard] -lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard] -lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard] -lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard] - - -subsubsection{*Optional Simplification Rules Involving Constants*} - -text{*Simplify quotients that are compared with a literal constant.*} - -lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] -lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] -lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] -lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] -lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] -lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] - - -text{*Not good as automatic simprules because they cause case splits.*} -lemmas divide_const_simps = - le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of - divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of - le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 - -text{*Division By @{text "-1"}*} - -lemma divide_minus1 [simp]: - "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" -by simp - -lemma minus1_divide [simp]: - "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" -by (simp add: divide_inverse inverse_minus_eq) - -lemma half_gt_zero_iff: - "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" -by auto - -lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard] -declare half_gt_zero [simp] - -(* The following lemma should appear in Divides.thy, but there the proof - doesn't work. *) - -lemma nat_dvd_not_less: - "[| 0 < m; m < n |] ==> \ n dvd (m::nat)" - by (unfold dvd_def) auto - -ML {* -val divide_minus1 = @{thm divide_minus1}; -val minus1_divide = @{thm minus1_divide}; -*} - -end diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 23 07:41:07 2009 +0100 @@ -299,7 +299,7 @@ *} "Langford's algorithm for quantifier elimination in dense linear orders" -section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} +section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields *} text {* Linear order without upper bounds *} diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Divides.thy Mon Mar 23 07:41:07 2009 +0100 @@ -1148,4 +1148,9 @@ with j show ?thesis by blast qed +lemma nat_dvd_not_less: + fixes m n :: nat + shows "0 < m \ m < n \ \ n dvd m" +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) + end diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Mon Mar 23 07:41:07 2009 +0100 @@ -5,7 +5,7 @@ header {* Semiring normalization and Groebner Bases *} theory Groebner_Basis -imports Arith_Tools +imports NatBin uses "Tools/Groebner_Basis/misc.ML" "Tools/Groebner_Basis/normalizer_data.ML" diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Int.thy --- a/src/HOL/Int.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Int.thy Mon Mar 23 07:41:07 2009 +0100 @@ -1256,14 +1256,14 @@ by (simp add: algebra_simps diff_number_of_eq [symmetric]) + + subsection {* The Set of Integers *} context ring_1 begin -definition - Ints :: "'a set" -where +definition Ints :: "'a set" where [code del]: "Ints = range of_int" end @@ -1854,7 +1854,7 @@ qed -subsection{*Integer Powers*} +subsection {* Integer Powers *} instantiation int :: recpower begin @@ -1896,6 +1896,161 @@ lemmas zpower_int = int_power [symmetric] + +subsection {* Further theorems on numerals *} + +subsubsection{*Special Simplification for Constants*} + +text{*These distributive laws move literals inside sums and differences.*} + +lemmas left_distrib_number_of [simp] = + left_distrib [of _ _ "number_of v", standard] + +lemmas right_distrib_number_of [simp] = + right_distrib [of "number_of v", standard] + +lemmas left_diff_distrib_number_of [simp] = + left_diff_distrib [of _ _ "number_of v", standard] + +lemmas right_diff_distrib_number_of [simp] = + right_diff_distrib [of "number_of v", standard] + +text{*These are actually for fields, like real: but where else to put them?*} + +lemmas zero_less_divide_iff_number_of [simp, noatp] = + zero_less_divide_iff [of "number_of w", standard] + +lemmas divide_less_0_iff_number_of [simp, noatp] = + divide_less_0_iff [of "number_of w", standard] + +lemmas zero_le_divide_iff_number_of [simp, noatp] = + zero_le_divide_iff [of "number_of w", standard] + +lemmas divide_le_0_iff_number_of [simp, noatp] = + divide_le_0_iff [of "number_of w", standard] + + +text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks + strange, but then other simprocs simplify the quotient.*} + +lemmas inverse_eq_divide_number_of [simp] = + inverse_eq_divide [of "number_of w", standard] + +text {*These laws simplify inequalities, moving unary minus from a term +into the literal.*} + +lemmas less_minus_iff_number_of [simp, noatp] = + less_minus_iff [of "number_of v", standard] + +lemmas le_minus_iff_number_of [simp, noatp] = + le_minus_iff [of "number_of v", standard] + +lemmas equation_minus_iff_number_of [simp, noatp] = + equation_minus_iff [of "number_of v", standard] + +lemmas minus_less_iff_number_of [simp, noatp] = + minus_less_iff [of _ "number_of v", standard] + +lemmas minus_le_iff_number_of [simp, noatp] = + minus_le_iff [of _ "number_of v", standard] + +lemmas minus_equation_iff_number_of [simp, noatp] = + minus_equation_iff [of _ "number_of v", standard] + + +text{*To Simplify Inequalities Where One Side is the Constant 1*} + +lemma less_minus_iff_1 [simp,noatp]: + fixes b::"'b::{ordered_idom,number_ring}" + shows "(1 < - b) = (b < -1)" +by auto + +lemma le_minus_iff_1 [simp,noatp]: + fixes b::"'b::{ordered_idom,number_ring}" + shows "(1 \ - b) = (b \ -1)" +by auto + +lemma equation_minus_iff_1 [simp,noatp]: + fixes b::"'b::number_ring" + shows "(1 = - b) = (b = -1)" +by (subst equation_minus_iff, auto) + +lemma minus_less_iff_1 [simp,noatp]: + fixes a::"'b::{ordered_idom,number_ring}" + shows "(- a < 1) = (-1 < a)" +by auto + +lemma minus_le_iff_1 [simp,noatp]: + fixes a::"'b::{ordered_idom,number_ring}" + shows "(- a \ 1) = (-1 \ a)" +by auto + +lemma minus_equation_iff_1 [simp,noatp]: + fixes a::"'b::number_ring" + shows "(- a = 1) = (a = -1)" +by (subst minus_equation_iff, auto) + + +text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\"}) *} + +lemmas mult_less_cancel_left_number_of [simp, noatp] = + mult_less_cancel_left [of "number_of v", standard] + +lemmas mult_less_cancel_right_number_of [simp, noatp] = + mult_less_cancel_right [of _ "number_of v", standard] + +lemmas mult_le_cancel_left_number_of [simp, noatp] = + mult_le_cancel_left [of "number_of v", standard] + +lemmas mult_le_cancel_right_number_of [simp, noatp] = + mult_le_cancel_right [of _ "number_of v", standard] + + +text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\"} and @{text "="}) *} + +lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard] +lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard] +lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard] +lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard] +lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard] +lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard] + + +subsubsection{*Optional Simplification Rules Involving Constants*} + +text{*Simplify quotients that are compared with a literal constant.*} + +lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] +lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] +lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] +lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] +lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] +lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] + + +text{*Not good as automatic simprules because they cause case splits.*} +lemmas divide_const_simps = + le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of + divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of + le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 + +text{*Division By @{text "-1"}*} + +lemma divide_minus1 [simp]: + "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" +by simp + +lemma minus1_divide [simp]: + "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" +by (simp add: divide_inverse inverse_minus_eq) + +lemma half_gt_zero_iff: + "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" +by auto + +lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard] + + subsection {* Configuration of the code generator *} code_datatype Pls Min Bit0 Bit1 "number_of \ int \ int" diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/IntDiv.thy Mon Mar 23 07:41:07 2009 +0100 @@ -8,6 +8,10 @@ theory IntDiv imports Int Divides FunDef +uses + "~~/src/Provers/Arith/cancel_numeral_factor.ML" + "~~/src/Provers/Arith/extract_common_term.ML" + ("Tools/int_factor_simprocs.ML") begin definition divmod_rel :: "int \ int \ int \ int \ bool" where @@ -920,9 +924,10 @@ next assume "a\0" and le_a: "0\a" hence a_pos: "1 \ a" by arith - hence one_less_a2: "1 < 2*a" by arith + hence one_less_a2: "1 < 2 * a" by arith hence le_2a: "2 * (1 + b mod a) \ 2 * a" - by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq) + unfolding mult_le_cancel_left + by (simp add: add1_zle_eq add_commute [of 1]) with a_pos have "0 \ b mod a" by simp hence le_addm: "0 \ 1 mod (2*a) + 2*(b mod a)" by (simp add: mod_pos_pos_trivial one_less_a2) @@ -1357,6 +1362,11 @@ qed +subsection {* Simproc setup *} + +use "Tools/int_factor_simprocs.ML" + + subsection {* Code generation *} definition pdivmod :: "int \ int \ int \ int" where diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/IsaMakefile Mon Mar 23 07:41:07 2009 +0100 @@ -204,7 +204,6 @@ @$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ - Arith_Tools.thy \ ATP_Linkup.thy \ Code_Eval.thy \ Code_Message.thy \ diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Mon Mar 23 07:41:07 2009 +0100 @@ -5,10 +5,10 @@ header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} theory Euclidean_Space - imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main +imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type Inner_Product - uses ("normarith.ML") +uses ("normarith.ML") begin text{* Some common special cases.*} diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 23 07:41:07 2009 +0100 @@ -6,10 +6,9 @@ header {* Elementary topology in Euclidean space. *} theory Topology_Euclidean_Space - imports SEQ Euclidean_Space +imports SEQ Euclidean_Space begin - declare fstcart_pastecart[simp] sndcart_pastecart[simp] subsection{* General notion of a topology *} @@ -474,7 +473,7 @@ have th0: "\d x y z. (d x z :: real) <= d x y + d y z \ d y z = d z y ==> ~(d x y * 2 < d x z \ d z y * 2 < d x z)" by arith have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym] - by (auto simp add: dist_refl expand_set_eq Arith_Tools.less_divide_eq_number_of1) + by (auto simp add: dist_refl expand_set_eq less_divide_eq_number_of1) then show ?thesis by blast qed @@ -662,7 +661,7 @@ have "?k/2 \ 0" using kp by simp then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist) from iT[unfolded expand_set_eq mem_interior] - have "\ ball w (?k/4) \ T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1) + have "\ ball w (?k/4) \ T" using kp by (auto simp add: less_divide_eq_number_of1) then obtain z where z: "dist w z < ?k/4" "z \ T" by (auto simp add: subset_eq) have "z \ T \ z\ y \ dist z y < d \ dist x z < e" using z apply simp using w e(1) d apply (auto simp only: dist_sym) @@ -1323,7 +1322,7 @@ assume "e>0" hence *:"eventually (\x. dist (f x) l < e/2) net" "eventually (\x. dist (g x) m < e/2) net" using as - by (auto intro: tendstoD simp del: Arith_Tools.less_divide_eq_number_of1) + by (auto intro: tendstoD simp del: less_divide_eq_number_of1) hence "eventually (\x. dist (f x + g x) (l + m) < e) net" proof(cases "trivial_limit net") case True @@ -3956,7 +3955,7 @@ hence fx0:"f x \ 0" using `l \ 0` by auto hence fxl0: "(f x) * l \ 0" using `l \ 0` by auto from * have **:"\f x - l\ < l\ * e / 2" by auto - have "\f x\ * 2 \ \l\" using * by (auto simp del: Arith_Tools.less_divide_eq_number_of1) + have "\f x\ * 2 \ \l\" using * by (auto simp del: less_divide_eq_number_of1) hence "\f x\ * 2 * \l\ \ \l\ * \l\" unfolding mult_le_cancel_right by auto hence "\f x * l\ * 2 \ \l\^2" unfolding real_mult_commute and power2_eq_square by auto hence ***:"inverse \f x * l\ \ inverse (l\ / 2)" using fxl0 @@ -4318,7 +4317,7 @@ have "a$i < b$i" using as[THEN spec[where x=i]] by auto hence "a$i < ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i < b$i" unfolding vector_smult_component and vector_add_component - by (auto simp add: Arith_Tools.less_divide_eq_number_of1) } + by (auto simp add: less_divide_eq_number_of1) } hence "{a <..< b} \ {}" using mem_interval(1)[of "?x" a b] by auto } ultimately show ?th1 by blast @@ -4333,7 +4332,7 @@ have "a$i \ b$i" using as[THEN spec[where x=i]] by auto hence "a$i \ ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i \ b$i" unfolding vector_smult_component and vector_add_component - by (auto simp add: Arith_Tools.less_divide_eq_number_of1) } + by (auto simp add: less_divide_eq_number_of1) } hence "{a .. b} \ {}" using mem_interval(2)[of "?x" a b] by auto } ultimately show ?th2 by blast qed @@ -4397,13 +4396,13 @@ { fix j have "c $ j < ?x $ j \ ?x $ j < d $ j" unfolding Cart_lambda_beta apply(cases "j=i") using as(2)[THEN spec[where x=j]] - by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) } + by (auto simp add: less_divide_eq_number_of1 as2) } hence "?x\{c<..{a .. b}" unfolding mem_interval apply auto apply(rule_tac x=i in exI) using as(2)[THEN spec[where x=i]] and as2 - by (auto simp add: Arith_Tools.less_divide_eq_number_of1) + by (auto simp add: less_divide_eq_number_of1) ultimately have False using as by auto } hence "a$i \ c$i" by(rule ccontr)auto moreover @@ -4412,13 +4411,13 @@ { fix j have "d $ j > ?x $ j \ ?x $ j > c $ j" unfolding Cart_lambda_beta apply(cases "j=i") using as(2)[THEN spec[where x=j]] - by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) } + by (auto simp add: less_divide_eq_number_of1 as2) } hence "?x\{c<..{a .. b}" unfolding mem_interval apply auto apply(rule_tac x=i in exI) using as(2)[THEN spec[where x=i]] and as2 - by (auto simp add: Arith_Tools.less_divide_eq_number_of1) + by (auto simp add: less_divide_eq_number_of1) ultimately have False using as by auto } hence "b$i \ d$i" by(rule ccontr)auto ultimately @@ -4449,7 +4448,7 @@ lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows "{a .. b} \ {c .. d} = {(\ i. max (a$i) (c$i)) .. (\ i. min (b$i) (d$i))}" unfolding expand_set_eq and Int_iff and mem_interval - by (auto simp add: Arith_Tools.less_divide_eq_number_of1 intro!: bexI) + by (auto simp add: less_divide_eq_number_of1 intro!: bexI) (* Moved interval_open_subset_closed a bit upwards *) @@ -4564,7 +4563,7 @@ have "a $ i < ((1 / 2) *s (a + b)) $ i \ ((1 / 2) *s (a + b)) $ i < b $ i" using assms[unfolded interval_ne_empty, THEN spec[where x=i]] unfolding vector_smult_component and vector_add_component - by(auto simp add: Arith_Tools.less_divide_eq_number_of1) } + by(auto simp add: less_divide_eq_number_of1) } thus ?thesis unfolding mem_interval by auto qed @@ -5632,7 +5631,7 @@ { assume as:"dist a b > dist (f n x) (f n y)" then obtain Na Nb where "\m\Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2" and "\m\Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2" - using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: Arith_Tools.less_divide_eq_number_of1) + using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1) hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)" apply(erule_tac x="Na+Nb+n" in allE) apply(erule_tac x="Na+Nb+n" in allE) apply simp diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/NatBin.thy Mon Mar 23 07:41:07 2009 +0100 @@ -7,6 +7,7 @@ theory NatBin imports IntDiv +uses ("Tools/nat_simprocs.ML") begin text {* @@ -40,9 +41,7 @@ subsection {* Predicate for negative binary numbers *} -definition - neg :: "int \ bool" -where +definition neg :: "int \ bool" where "neg Z \ Z < 0" lemma not_neg_int [simp]: "~ neg (of_nat n)" @@ -818,4 +817,159 @@ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" by (simp add: nat_mult_div_cancel1) + +subsection {* Simprocs for the Naturals *} + +use "Tools/nat_simprocs.ML" +declaration {* K nat_simprocs_setup *} + +subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} + +text{*Where K above is a literal*} + +lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)" +by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) + +text {*Now just instantiating @{text n} to @{text "number_of v"} does + the right simplification, but with some redundant inequality + tests.*} +lemma neg_number_of_pred_iff_0: + "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))" +apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ") +apply (simp only: less_Suc_eq_le le_0_eq) +apply (subst less_number_of_Suc, simp) +done + +text{*No longer required as a simprule because of the @{text inverse_fold} + simproc*} +lemma Suc_diff_number_of: + "Int.Pls < v ==> + Suc m - (number_of v) = m - (number_of (Int.pred v))" +apply (subst Suc_diff_eq_diff_pred) +apply simp +apply (simp del: nat_numeral_1_eq_1) +apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] + neg_number_of_pred_iff_0) +done + +lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" +by (simp add: numerals split add: nat_diff_split) + + +subsubsection{*For @{term nat_case} and @{term nat_rec}*} + +lemma nat_case_number_of [simp]: + "nat_case a f (number_of v) = + (let pv = number_of (Int.pred v) in + if neg pv then a else f (nat pv))" +by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0) + +lemma nat_case_add_eq_if [simp]: + "nat_case a f ((number_of v) + n) = + (let pv = number_of (Int.pred v) in + if neg pv then nat_case a f n else f (nat pv + n))" +apply (subst add_eq_if) +apply (simp split add: nat.split + del: nat_numeral_1_eq_1 + add: nat_numeral_1_eq_1 [symmetric] + numeral_1_eq_Suc_0 [symmetric] + neg_number_of_pred_iff_0) +done + +lemma nat_rec_number_of [simp]: + "nat_rec a f (number_of v) = + (let pv = number_of (Int.pred v) in + if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" +apply (case_tac " (number_of v) ::nat") +apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0) +apply (simp split add: split_if_asm) +done + +lemma nat_rec_add_eq_if [simp]: + "nat_rec a f (number_of v + n) = + (let pv = number_of (Int.pred v) in + if neg pv then nat_rec a f n + else f (nat pv + n) (nat_rec a f (nat pv + n)))" +apply (subst add_eq_if) +apply (simp split add: nat.split + del: nat_numeral_1_eq_1 + add: nat_numeral_1_eq_1 [symmetric] + numeral_1_eq_Suc_0 [symmetric] + neg_number_of_pred_iff_0) +done + + +subsubsection{*Various Other Lemmas*} + +text {*Evens and Odds, for Mutilated Chess Board*} + +text{*Lemmas for specialist use, NOT as default simprules*} +lemma nat_mult_2: "2 * z = (z+z::nat)" +proof - + have "2*z = (1 + 1)*z" by simp + also have "... = z+z" by (simp add: left_distrib) + finally show ?thesis . +qed + +lemma nat_mult_2_right: "z * 2 = (z+z::nat)" +by (subst mult_commute, rule nat_mult_2) + +text{*Case analysis on @{term "n<2"}*} +lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" +by arith + +lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)" +by arith + +lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" +by (simp add: nat_mult_2 [symmetric]) + +lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" +apply (subgoal_tac "m mod 2 < 2") +apply (erule less_2_cases [THEN disjE]) +apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) +done + +lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)" +apply (subgoal_tac "m mod 2 < 2") +apply (force simp del: mod_less_divisor, simp) +done + +text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} + +lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" +by simp + +lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" +by simp + +text{*Can be used to eliminate long strings of Sucs, but not by default*} +lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" +by simp + + +text{*These lemmas collapse some needless occurrences of Suc: + at least three Sucs, since two and fewer are rewritten back to Suc again! + We already have some rules to simplify operands smaller than 3.*} + +lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" +by (simp add: Suc3_eq_add_3) + +lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" +by (simp add: Suc3_eq_add_3) + +lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" +by (simp add: Suc3_eq_add_3) + +lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" +by (simp add: Suc3_eq_add_3) + +lemmas Suc_div_eq_add3_div_number_of = + Suc_div_eq_add3_div [of _ "number_of v", standard] +declare Suc_div_eq_add3_div_number_of [simp] + +lemmas Suc_mod_eq_add3_mod_number_of = + Suc_mod_eq_add3_mod [of _ "number_of v", standard] +declare Suc_mod_eq_add3_mod_number_of [simp] + end diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Presburger.thy Mon Mar 23 07:41:07 2009 +0100 @@ -7,6 +7,7 @@ theory Presburger imports Groebner_Basis SetInterval uses + "Tools/Qelim/qelim.ML" "Tools/Qelim/cooper_data.ML" "Tools/Qelim/generated_cooper.ML" ("Tools/Qelim/cooper.ML") diff -r 94b74365ceb9 -r a400b06d03cb src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Sun Mar 22 21:48:14 2009 +0100 +++ b/src/HOL/Tools/Qelim/qelim.ML Mon Mar 23 07:41:07 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/Qelim/qelim.ML - ID: $Id$ Author: Amine Chaieb, TU Muenchen Generic quantifier elimination conversions for HOL formulae. @@ -26,11 +25,12 @@ case (term_of p) of Const(s,T)$_$_ => if domain_type T = HOLogic.boolT - andalso s mem ["op &","op |","op -->","op ="] + andalso member (op =) [@{const_name "op &"}, @{const_name "op |"}, + @{const_name "op -->"}, @{const_name "op ="}] s then binop_conv (conv env) p else atcv env p - | Const("Not",_)$_ => arg_conv (conv env) p - | Const("Ex",_)$Abs(s,_,_) => + | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p + | Const(@{const_name "Ex"},_)$Abs(s,_,_) => let val (e,p0) = Thm.dest_comb p val (x,p') = Thm.dest_abs (SOME s) p0 @@ -41,8 +41,8 @@ val (l,r) = Thm.dest_equals (cprop_of th') in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th)) else Thm.transitive (Thm.transitive th th') (conv env r) end - | Const("Ex",_)$ _ => (Thm.eta_long_conversion then_conv conv env) p - | Const("All",_)$_ => + | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p + | Const(@{const_name "All"},_)$_ => let val p = Thm.dest_arg p val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)