# HG changeset patch # User wenzelm # Date 964476406 -7200 # Node ID 62bb04ab4b01edf6945feacae0747e8a0b544abc # Parent c3a13a7d442435d3f1a81150e070558588c66111 rearranged setup of arithmetic procedures, avoiding global reference values; diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Arith.ML Tue Jul 25 00:06:46 2000 +0200 @@ -3,1030 +3,13 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Proofs about elementary arithmetic: addition, multiplication, etc. -Some from the Hoare example from Norbert Galm +Further proofs about elementary arithmetic, using the arithmetic proof +procedures. *) -(*** Basic rewrite rules for the arithmetic operators ***) - - -(** Difference **) - -Goal "0 - n = (0::nat)"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_0_eq_0"; - -(*Must simplify BEFORE the induction! (Else we get a critical pair) - Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *) -Goal "Suc(m) - Suc(n) = m - n"; -by (Simp_tac 1); -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_Suc_Suc"; - -Addsimps [diff_0_eq_0, diff_Suc_Suc]; - -(* Could be (and is, below) generalized in various ways; - However, none of the generalizations are currently in the simpset, - and I dread to think what happens if I put them in *) -Goal "0 < n ==> Suc(n-1) = n"; -by (asm_simp_tac (simpset() addsplits [nat.split]) 1); -qed "Suc_pred"; -Addsimps [Suc_pred]; - -Delsimps [diff_Suc]; - - -(**** Inductive properties of the operators ****) - -(*** Addition ***) - -Goal "m + 0 = (m::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "add_0_right"; - -Goal "m + Suc(n) = Suc(m+n)"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "add_Suc_right"; - -Addsimps [add_0_right,add_Suc_right]; - - -(*Associative law for addition*) -Goal "(m + n) + k = m + ((n + k)::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "add_assoc"; - -(*Commutative law for addition*) -Goal "m + n = n + (m::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "add_commute"; - -Goal "x+(y+z)=y+((x+z)::nat)"; -by (rtac (add_commute RS trans) 1); -by (rtac (add_assoc RS trans) 1); -by (rtac (add_commute RS arg_cong) 1); -qed "add_left_commute"; - -(*Addition is an AC-operator*) -bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]); - -Goal "(k + m = k + n) = (m=(n::nat))"; -by (induct_tac "k" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_left_cancel"; - -Goal "(m + k = n + k) = (m=(n::nat))"; -by (induct_tac "k" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_right_cancel"; - -Goal "(k + m <= k + n) = (m<=(n::nat))"; -by (induct_tac "k" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_left_cancel_le"; - -Goal "(k + m < k + n) = (m<(n::nat))"; -by (induct_tac "k" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_left_cancel_less"; - -Addsimps [add_left_cancel, add_right_cancel, - add_left_cancel_le, add_left_cancel_less]; - -(** Reasoning about m+0=0, etc. **) - -Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)"; -by (case_tac "m" 1); -by (Auto_tac); -qed "add_is_0"; -AddIffs [add_is_0]; - -Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)"; -by (case_tac "m" 1); -by (Auto_tac); -qed "zero_is_add"; -AddIffs [zero_is_add]; - -Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)"; -by (case_tac "m" 1); -by (Auto_tac); -qed "add_is_1"; - -Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)"; -by (case_tac "m" 1); -by (Auto_tac); -qed "one_is_add"; - -Goal "!!m::nat. (0 m+(n-(Suc k)) = (m+n)-(Suc k)" *) -Goal "!!m::nat. 0 m + (n-1) = (m+n)-1"; -by (case_tac "m" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n] - addsplits [nat.split]))); -qed "add_pred"; -Addsimps [add_pred]; - -Goal "!!m::nat. m + n = m ==> n = 0"; -by (dtac (add_0_right RS ssubst) 1); -by (asm_full_simp_tac (simpset() addsimps [add_assoc] - delsimps [add_0_right]) 1); -qed "add_eq_self_zero"; - - -(**** Additional theorems about "less than" ****) - -(*Deleted less_natE; instead use less_eq_Suc_add RS exE*) -Goal "m (EX k. n=Suc(m+k))"; -by (induct_tac "n" 1); -by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less]))); -by (blast_tac (claset() addSEs [less_SucE] - addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); -qed_spec_mp "less_eq_Suc_add"; - -Goal "n <= ((m + n)::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS Simp_tac); -by (etac le_SucI 1); -qed "le_add2"; - -Goal "n <= ((n + m)::nat)"; -by (simp_tac (simpset() addsimps add_ac) 1); -by (rtac le_add2 1); -qed "le_add1"; - -bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); -bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); - -Goal "(m i <= j+m"*) -bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); - -(*"i <= j ==> i <= m+j"*) -bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans)); - -(*"i < j ==> i < j+m"*) -bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans)); - -(*"i < j ==> i < m+j"*) -bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans)); - -Goal "i+j < (k::nat) --> i m<=(n::nat)"; -by (induct_tac "k" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps))); -qed_spec_mp "add_leD1"; - -Goal "m+k<=n ==> k<=(n::nat)"; -by (full_simp_tac (simpset() addsimps [add_commute]) 1); -by (etac add_leD1 1); -qed_spec_mp "add_leD2"; - -Goal "m+k<=n ==> m<=n & k<=(n::nat)"; -by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1); -bind_thm ("add_leE", result() RS conjE); - -(*needs !!k for add_ac to work*) -Goal "!!k:: nat. [| k m i + k < j + (k::nat)"; -by (induct_tac "k" 1); -by (ALLGOALS Asm_simp_tac); -qed "add_less_mono1"; - -(*strict, in both arguments*) -Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)"; -by (rtac (add_less_mono1 RS less_trans) 1); -by (REPEAT (assume_tac 1)); -by (induct_tac "j" 1); -by (ALLGOALS Asm_simp_tac); -qed "add_less_mono"; - -(*A [clumsy] way of lifting < monotonicity to <= monotonicity *) -val [lt_mono,le] = Goal - "[| !!i j::nat. i f(i) < f(j); \ -\ i <= j \ -\ |] ==> f(i) <= (f(j)::nat)"; -by (cut_facts_tac [le] 1); -by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1); -by (blast_tac (claset() addSIs [lt_mono]) 1); -qed "less_mono_imp_le_mono"; - -(*non-strict, in 1st argument*) -Goal "i<=j ==> i + k <= j + (k::nat)"; -by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1); -by (etac add_less_mono1 1); -by (assume_tac 1); -qed "add_le_mono1"; - -(*non-strict, in both arguments*) -Goal "[|i<=j; k<=l |] ==> i + k <= j + (l::nat)"; -by (etac (add_le_mono1 RS le_trans) 1); -by (simp_tac (simpset() addsimps [add_commute]) 1); -qed "add_le_mono"; - - -(*** Multiplication ***) - -(*right annihilation in product*) -Goal "!!m::nat. m * 0 = 0"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "mult_0_right"; - -(*right successor law for multiplication*) -Goal "m * Suc(n) = m + (m * n)"; -by (induct_tac "m" 1); -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); -qed "mult_Suc_right"; - -Addsimps [mult_0_right, mult_Suc_right]; - -Goal "1 * n = n"; -by (Asm_simp_tac 1); -qed "mult_1"; - -Goal "n * 1 = n"; -by (Asm_simp_tac 1); -qed "mult_1_right"; - -(*Commutative law for multiplication*) -Goal "m * n = n * (m::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "mult_commute"; - -(*addition distributes over multiplication*) -Goal "(m + n)*k = (m*k) + ((n*k)::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); -qed "add_mult_distrib"; - -Goal "k*(m + n) = (k*m) + ((k*n)::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); -qed "add_mult_distrib2"; - -(*Associative law for multiplication*) -Goal "(m * n) * k = m * ((n * k)::nat)"; -by (induct_tac "m" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))); -qed "mult_assoc"; - -Goal "x*(y*z) = y*((x*z)::nat)"; -by (rtac trans 1); -by (rtac mult_commute 1); -by (rtac trans 1); -by (rtac mult_assoc 1); -by (rtac (mult_commute RS arg_cong) 1); -qed "mult_left_commute"; - -bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]); - -Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)"; -by (induct_tac "m" 1); -by (induct_tac "n" 2); -by (ALLGOALS Asm_simp_tac); -qed "mult_is_0"; - -Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)"; -by (stac eq_commute 1 THEN stac mult_is_0 1); -by Auto_tac; -qed "zero_is_mult"; - -Addsimps [mult_is_0, zero_is_mult]; - - -(*** Difference ***) - -Goal "!!m::nat. m - m = 0"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_self_eq_0"; - -Addsimps [diff_self_eq_0]; - -(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) -Goal "~ m n+(m-n) = (m::nat)"; -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "add_diff_inverse"; - -Goal "n<=m ==> n+(m-n) = (m::nat)"; -by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1); -qed "le_add_diff_inverse"; - -Goal "n<=m ==> (m-n)+n = (m::nat)"; -by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1); -qed "le_add_diff_inverse2"; - -Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; - - -(*** More results about difference ***) - -Goal "n <= m ==> Suc(m)-n = Suc(m-n)"; -by (etac rev_mp 1); -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS Asm_simp_tac); -qed "Suc_diff_le"; - -Goal "m - n < Suc(m)"; -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (etac less_SucE 3); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); -qed "diff_less_Suc"; - -Goal "m - n <= (m::nat)"; -by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI]))); -qed "diff_le_self"; -Addsimps [diff_le_self]; - -(* j j-n < k *) -bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans); - -Goal "!!i::nat. i-j-k = i - (j+k)"; -by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_diff_left"; - -Goal "(Suc m - n) - Suc k = m - n - k"; -by (simp_tac (simpset() addsimps [diff_diff_left]) 1); -qed "Suc_diff_diff"; -Addsimps [Suc_diff_diff]; - -Goal "0 n - Suc i < n"; -by (case_tac "n" 1); -by Safe_tac; -by (asm_simp_tac (simpset() addsimps le_simps) 1); -qed "diff_Suc_less"; -Addsimps [diff_Suc_less]; - -(*This and the next few suggested by Florian Kammueller*) -Goal "!!i::nat. i-j-k = i-k-j"; -by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1); -qed "diff_commute"; - -Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)"; -by (res_inst_tac [("m","j"),("n","k")] diff_induct 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "diff_add_assoc"; - -Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i"; -by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1); -qed_spec_mp "diff_add_assoc2"; - -Goal "(n+m) - n = (m::nat)"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_add_inverse"; - -Goal "(m+n) - n = (m::nat)"; -by (simp_tac (simpset() addsimps [diff_add_assoc]) 1); -qed "diff_add_inverse2"; - -Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)"; -by Safe_tac; -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2]))); -qed "le_imp_diff_is_add"; - -Goal "!!m::nat. (m-n = 0) = (m <= n)"; -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_is_0_eq"; - -Goal "!!m::nat. (0 = m-n) = (m <= n)"; -by (stac (diff_is_0_eq RS sym) 1); -by (rtac eq_sym_conv 1); -qed "zero_is_diff_eq"; -Addsimps [diff_is_0_eq, zero_is_diff_eq]; - -Goal "!!m::nat. (0 EX k::nat. 0 (ALL n. P(Suc(n))--> P(n)) --> P(k-i)"; -by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); -by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac)); -qed "zero_induct_lemma"; - -val prems = Goal "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)"; -by (rtac (diff_self_eq_0 RS subst) 1); -by (rtac (zero_induct_lemma RS mp RS mp) 1); -by (REPEAT (ares_tac ([impI,allI]@prems) 1)); -qed "zero_induct"; - -Goal "(k+m) - (k+n) = m - (n::nat)"; -by (induct_tac "k" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_cancel"; - -Goal "(m+k) - (n+k) = m - (n::nat)"; -by (asm_simp_tac - (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1); -qed "diff_cancel2"; - -Goal "n - (n+m) = (0::nat)"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_add_0"; - - -(** Difference distributes over multiplication **) - -Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)"; -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel]))); -qed "diff_mult_distrib" ; - -Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)"; -val mult_commute_k = read_instantiate [("m","k")] mult_commute; -by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1); -qed "diff_mult_distrib2" ; -(*NOT added as rewrites, since sometimes they are used from right-to-left*) - - -(*** Monotonicity of Multiplication ***) - -Goal "i <= (j::nat) ==> i*k<=j*k"; -by (induct_tac "k" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); -qed "mult_le_mono1"; - -Goal "i <= (j::nat) ==> k*i <= k*j"; -by (dtac mult_le_mono1 1); -by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); -qed "mult_le_mono2"; - -(* <= monotonicity, BOTH arguments*) -Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l"; -by (etac (mult_le_mono1 RS le_trans) 1); -by (etac mult_le_mono2 1); -qed "mult_le_mono"; +(*legacy ...*) +structure Arith = struct val thy = the_context () end; -(*strict, in 1st argument; proof is by induction on k>0*) -Goal "!!i::nat. [| i k*i < k*j"; -by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1); -by (Asm_simp_tac 1); -by (induct_tac "x" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); -qed "mult_less_mono2"; - -Goal "!!i::nat. [| i i*k < j*k"; -by (dtac mult_less_mono2 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute]))); -qed "mult_less_mono1"; - -Goal "!!m::nat. (0 < m*n) = (0 (m*k < n*k) = (m (k*m < k*n) = (m (m*k <= n*k) = (m<=n)"; -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -qed "mult_le_cancel2"; - -Goal "!!m::nat. 0 (k*m <= k*n) = (m<=n)"; -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -qed "mult_le_cancel1"; -Addsimps [mult_le_cancel1, mult_le_cancel2]; - -Goal "(Suc k * m < Suc k * n) = (m < n)"; -by (rtac mult_less_cancel1 1); -by (Simp_tac 1); -qed "Suc_mult_less_cancel1"; - -Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)"; -by (simp_tac (simpset_of HOL.thy) 1); -by (rtac Suc_mult_less_cancel1 1); -qed "Suc_mult_le_cancel1"; - -Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)"; -by (cut_facts_tac [less_linear] 1); -by Safe_tac; -by (assume_tac 2); -by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac)); -by (ALLGOALS Asm_full_simp_tac); -qed "mult_cancel2"; - -Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)"; -by (dtac mult_cancel2 1); -by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); -qed "mult_cancel1"; -Addsimps [mult_cancel1, mult_cancel2]; - -Goal "(Suc k * m = Suc k * n) = (m = n)"; -by (rtac mult_cancel1 1); -by (Simp_tac 1); -qed "Suc_mult_cancel1"; - - -(*Lemma for gcd*) -Goal "!!m::nat. m = m*n ==> n=1 | m=0"; -by (dtac sym 1); -by (rtac disjCI 1); -by (rtac nat_less_cases 1 THEN assume_tac 2); -by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1); -by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1); -qed "mult_eq_self_implies_10"; - - - - -(*---------------------------------------------------------------------------*) -(* Various arithmetic proof procedures *) -(*---------------------------------------------------------------------------*) - -(*---------------------------------------------------------------------------*) -(* 1. Cancellation of common terms *) -(*---------------------------------------------------------------------------*) - -(* Title: HOL/arith_data.ML - ID: $Id$ - Author: Markus Wenzel and Stefan Berghofer, TU Muenchen - -Setup various arithmetic proof procedures. -*) - -signature ARITH_DATA = -sig - val nat_cancel_sums_add: simproc list - val nat_cancel_sums: simproc list - val nat_cancel_factor: simproc list - val nat_cancel: simproc list -end; - -structure ArithData: ARITH_DATA = -struct - - -(** abstract syntax of structure nat: 0, Suc, + **) - -(* mk_sum, mk_norm_sum *) - -val one = HOLogic.mk_nat 1; -val mk_plus = HOLogic.mk_binop "op +"; - -fun mk_sum [] = HOLogic.zero - | mk_sum [t] = t - | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) -fun mk_norm_sum ts = - let val (ones, sums) = partition (equal one) ts in - funpow (length ones) HOLogic.mk_Suc (mk_sum sums) - end; - - -(* dest_sum *) - -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; - -fun dest_sum tm = - if HOLogic.is_zero tm then [] - else - (case try HOLogic.dest_Suc tm of - Some t => one :: dest_sum t - | None => - (case try dest_plus tm of - Some (t, u) => dest_sum t @ dest_sum u - | None => [tm])); - - -(** generic proof tools **) - -(* prove conversions *) - -val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; - -fun prove_conv expand_tac norm_tac sg (t, u) = - mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u))) - (K [expand_tac, norm_tac])) - handle ERROR => error ("The error(s) above occurred while trying to prove " ^ - (string_of_cterm (cterm_of sg (mk_eqv (t, u))))); - -val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s" - (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); - - -(* rewriting *) - -fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules)); - -val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; -val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; - - - -(** cancel common summands **) - -structure Sum = -struct - val mk_sum = mk_norm_sum; - val dest_sum = dest_sum; - val prove_conv = prove_conv; - val norm_tac = simp_all add_rules THEN simp_all add_ac; -end; - -fun gen_uncancel_tac rule ct = - rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1; - - -(* nat eq *) - -structure EqCancelSums = CancelSumsFun -(struct - open Sum; - val mk_bal = HOLogic.mk_eq; - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; - val uncancel_tac = gen_uncancel_tac add_left_cancel; -end); - - -(* nat less *) - -structure LessCancelSums = CancelSumsFun -(struct - open Sum; - val mk_bal = HOLogic.mk_binrel "op <"; - val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; - val uncancel_tac = gen_uncancel_tac add_left_cancel_less; -end); - - -(* nat le *) - -structure LeCancelSums = CancelSumsFun -(struct - open Sum; - val mk_bal = HOLogic.mk_binrel "op <="; - val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; - val uncancel_tac = gen_uncancel_tac add_left_cancel_le; -end); - - -(* nat diff *) - -structure DiffCancelSums = CancelSumsFun -(struct - open Sum; - val mk_bal = HOLogic.mk_binop "op -"; - val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT; - val uncancel_tac = gen_uncancel_tac diff_cancel; -end); - - - -(** cancel common factor **) - -structure Factor = -struct - val mk_sum = mk_norm_sum; - val dest_sum = dest_sum; - val prove_conv = prove_conv; - val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac; -end; - -fun mk_cnat n = cterm_of (Theory.sign_of Nat.thy) (HOLogic.mk_nat n); - -fun gen_multiply_tac rule k = - if k > 0 then - rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1 - else no_tac; - - -(* nat eq *) - -structure EqCancelFactor = CancelFactorFun -(struct - open Factor; - val mk_bal = HOLogic.mk_eq; - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; - val multiply_tac = gen_multiply_tac Suc_mult_cancel1; -end); - - -(* nat less *) - -structure LessCancelFactor = CancelFactorFun -(struct - open Factor; - val mk_bal = HOLogic.mk_binrel "op <"; - val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; - val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1; -end); - - -(* nat le *) - -structure LeCancelFactor = CancelFactorFun -(struct - open Factor; - val mk_bal = HOLogic.mk_binrel "op <="; - val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; - val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1; -end); - - - -(** prepare nat_cancel simprocs **) - -fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT); -val prep_pats = map prep_pat; - -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; - -val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]; -val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]; -val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]; -val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]; - -val nat_cancel_sums_add = map prep_simproc - [("nateq_cancel_sums", eq_pats, EqCancelSums.proc), - ("natless_cancel_sums", less_pats, LessCancelSums.proc), - ("natle_cancel_sums", le_pats, LeCancelSums.proc)]; - -val nat_cancel_sums = nat_cancel_sums_add @ - [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)]; - -val nat_cancel_factor = map prep_simproc - [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc), - ("natless_cancel_factor", less_pats, LessCancelFactor.proc), - ("natle_cancel_factor", le_pats, LeCancelFactor.proc)]; - -val nat_cancel = nat_cancel_factor @ nat_cancel_sums; - - -end; - -open ArithData; - -Addsimprocs nat_cancel; - -(*---------------------------------------------------------------------------*) -(* 2. Linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(* Parameters data for general linear arithmetic functor *) - -structure LA_Logic: LIN_ARITH_LOGIC = -struct -val ccontr = ccontr; -val conjI = conjI; -val neqE = linorder_neqE; -val notI = notI; -val sym = sym; -val not_lessD = linorder_not_less RS iffD1; -val not_leD = linorder_not_le RS iffD1; - - -fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); - -val mk_Trueprop = HOLogic.mk_Trueprop; - -fun neg_prop(TP$(Const("Not",_)$t)) = TP$t - | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t); - -fun is_False thm = - let val _ $ t = #prop(rep_thm thm) - in t = Const("False",HOLogic.boolT) end; - -fun is_nat(t) = fastype_of1 t = HOLogic.natT; - -fun mk_nat_thm sg t = - let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) - in instantiate ([],[(cn,ct)]) le0 end; - -end; - -signature LIN_ARITH_DATA2 = -sig - include LIN_ARITH_DATA - val discrete: (string * bool)list ref -end; - -structure LA_Data_Ref: LIN_ARITH_DATA2 = -struct - val add_mono_thms = ref ([]:thm list); - val lessD = ref ([]:thm list); - val ss_ref = ref HOL_basic_ss; - val discrete = ref ([]:(string*bool)list); - -(* Decomposition of terms *) - -fun nT (Type("fun",[N,_])) = N = HOLogic.natT - | nT _ = false; - -fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) - | Some n => (overwrite(p,(t,n+m:int)), i)); - -(* Turn term into list of summand * multiplicity plus a constant *) -fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) - | poly(all as Const("op -",T) $ s $ t, m, pi) = - if nT T then add_atom(all,m,pi) - else poly(s,m,poly(t,~1*m,pi)) - | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) - | poly(Const("0",_), _, pi) = pi - | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m)) - | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)= - (poly(t,m*HOLogic.dest_binum c,pi) - handle TERM _ => add_atom(all,m,pi)) - | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)= - (poly(t,m*HOLogic.dest_binum c,pi) - handle TERM _ => add_atom(all,m,pi)) - | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) = - ((p,i + m*HOLogic.dest_binum t) - handle TERM _ => add_atom(all,m,(p,i))) - | poly x = add_atom x; - -fun decomp2(rel,lhs,rhs) = - let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) - in case rel of - "op <" => Some(p,i,"<",q,j) - | "op <=" => Some(p,i,"<=",q,j) - | "op =" => Some(p,i,"=",q,j) - | _ => None - end; - -fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d) - | negate None = None; - -fun decomp1 (T,xxx) = - (case T of - Type("fun",[Type(D,[]),_]) => - (case assoc(!discrete,D) of - None => None - | Some d => (case decomp2 xxx of - None => None - | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d))) - | _ => None); - -fun decomp (_$(Const(rel,T)$lhs$rhs)) = decomp1 (T,(rel,lhs,rhs)) - | decomp (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = - negate(decomp1 (T,(rel,lhs,rhs))) - | decomp _ = None -end; - -let - -(* reduce contradictory <= to False. - Most of the work is done by the cancel tactics. -*) -val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq]; - -val add_mono_thms = map (fn s => prove_goal Arith.thy s - (fn prems => [cut_facts_tac prems 1, - blast_tac (claset() addIs [add_le_mono]) 1])) -["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)", - "(i = j) & (k <= l) ==> i + k <= j + (l::nat)", - "(i <= j) & (k = l) ==> i + k <= j + (l::nat)", - "(i = j) & (k = l) ==> i + k = j + (l::nat)" -]; - -in -LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms; -LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [Suc_leI]; -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules - addsimprocs nat_cancel_sums_add; -LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("nat",true)] -end; - -structure Fast_Arith = - Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); - -val fast_arith_tac = Fast_Arith.lin_arith_tac -and trace_arith = Fast_Arith.trace; - -let -val nat_arith_simproc_pats = - map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT)) - ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]; - -val fast_nat_arith_simproc = mk_simproc - "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover; -in -Addsimprocs [fast_nat_arith_simproc] -end; - -(* Because of fast_nat_arith_simproc, the arithmetic solver is really only -useful to detect inconsistencies among the premises for subgoals which are -*not* themselves (in)equalities, because the latter activate -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the -solver all the time rather than add the additional check. *) - -simpset_ref () := (simpset() addSolver - (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac)); - -(*Elimination of `-' on nat*) -Goal "P(a - b::nat) = (ALL d. (a P 0) & (a = b + d --> P d))"; -by (case_tac "a < b" 1); -by (auto_tac (claset(), simpset() addsimps [diff_is_0_eq RS iffD2])); -qed "nat_diff_split"; - -(* FIXME: K true should be replaced by a sensible test to speed things up - in case there are lots of irrelevant terms involved; - elimination of min/max can be optimized: - (max m n + k <= r) = (m+k <= r & n+k <= r) - (l <= min m n + k) = (l <= m+k & l <= n+k) -*) -val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max]; -fun arith_tac i = - refute_tac (K true) (REPEAT o split_tac (!arith_tac_split_thms)) - ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i; - - -(* proof method setup *) - -fun arith_method prems = - Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); - -val arith_setup = - [Method.add_methods - [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts , "decide linear arithmethic")]]; - -(*---------------------------------------------------------------------------*) -(* End of proof procedures. Now go and USE them! *) -(*---------------------------------------------------------------------------*) Goal "m <= m*(m::nat)"; by (induct_tac "m" 1); diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Arith.thy --- a/src/HOL/Arith.thy Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Arith.thy Tue Jul 25 00:06:46 2000 +0200 @@ -1,29 +1,21 @@ (* Title: HOL/Arith.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -Arithmetic operators + - and * (for div, mod and dvd, see Divides) +Setup arithmetic proof procedures. *) -Arith = Nat + +theory Arith = Nat +files "arith_data.ML": -instance - nat :: {plus, minus, times, power} - -(* size of a datatype value; overloaded *) -consts size :: 'a => nat +setup arith_setup -primrec - add_0 "0 + n = n" - add_Suc "Suc m + n = Suc(m + n)" +(*elimination of `-' on nat*) +lemma nat_diff_split: + "P(a - b::nat) = (ALL d. (a P 0) & (a = b + d --> P d))" + by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [RS iffD2]) -primrec - diff_0 "m - 0 = m" - diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" +ML {* val nat_diff_split = thm "nat_diff_split" *} -primrec - mult_0 "0 * n = 0" - mult_Suc "Suc m * n = n + (m * n)" +lemmas [arith_split] = nat_diff_split split_min split_max end diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Integ/Bin.ML Tue Jul 25 00:06:46 2000 +0200 @@ -258,7 +258,7 @@ (*Negation of a coefficient*) Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)"; -by (simp_tac (simpset_of Int.thy addsimps [number_of_minus, zmult_zminus]) 1); +by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1); qed "zminus_number_of_zmult"; Addsimps [zminus_number_of_zmult]; diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/Int.ML --- a/src/HOL/Integ/Int.ML Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Integ/Int.ML Tue Jul 25 00:06:46 2000 +0200 @@ -34,7 +34,7 @@ val ss = HOL_ss val eq_reflection = eq_reflection - val thy = IntDef.thy + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) val T = HOLogic.intT val zero = Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero val restrict_to_left = restrict_to_left diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/IntArith.ML --- a/src/HOL/Integ/IntArith.ML Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Integ/IntArith.ML Tue Jul 25 00:06:46 2000 +0200 @@ -1,575 +1,8 @@ -(* Title: HOL/Integ/IntArith.thy +(* Title: HOL/Integ/IntArith.ML ID: $Id$ Authors: Larry Paulson and Tobias Nipkow - -Simprocs and decision procedure for linear arithmetic. *) -(*** Simprocs for numeric literals ***) - -(** Combining of literal coefficients in sums of products **) - -Goal "(x < y) = (x-y < (#0::int))"; -by (simp_tac (simpset() addsimps zcompare_rls) 1); -qed "zless_iff_zdiff_zless_0"; - -Goal "(x = y) = (x-y = (#0::int))"; -by (simp_tac (simpset() addsimps zcompare_rls) 1); -qed "eq_iff_zdiff_eq_0"; - -Goal "(x <= y) = (x-y <= (#0::int))"; -by (simp_tac (simpset() addsimps zcompare_rls) 1); -qed "zle_iff_zdiff_zle_0"; - - -(** For combine_numerals **) - -Goal "i*u + (j*u + k) = (i+j)*u + (k::int)"; -by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); -qed "left_zadd_zmult_distrib"; - - -(** For cancel_numerals **) - -val rel_iff_rel_0_rls = map (inst "y" "?u+?v") - [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, - zle_iff_zdiff_zle_0] @ - map (inst "y" "n") - [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, - zle_iff_zdiff_zle_0]; - -Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "eq_add_iff1"; - -Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "eq_add_iff2"; - -Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "less_add_iff1"; - -Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "less_add_iff2"; - -Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "le_add_iff1"; - -Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib] - @zadd_ac@rel_iff_rel_0_rls) 1); -qed "le_add_iff2"; - -(*To tidy up the result of a simproc. Only the RHS will be simplified.*) -Goal "u = u' ==> (t==u) == (t==u')"; -by Auto_tac; -qed "eq_cong2"; - - -structure Int_Numeral_Simprocs = -struct - -(*Utilities*) - -fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ - NumeralSyntax.mk_bin n; - -(*Decodes a binary INTEGER*) -fun dest_numeral (Const("Numeral.number_of", _) $ w) = - (NumeralSyntax.dest_bin w - handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) - | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); - -fun find_first_numeral past (t::terms) = - ((dest_numeral t, rev past @ terms) - handle TERM _ => find_first_numeral (t::past) terms) - | find_first_numeral past [] = raise TERM("find_first_numeral", []); - -val zero = mk_numeral 0; -val mk_plus = HOLogic.mk_binop "op +"; - -val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT); - -(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) -fun mk_sum [] = zero - | mk_sum [t,u] = mk_plus (t, u) - | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -(*this version ALWAYS includes a trailing zero*) -fun long_mk_sum [] = zero - | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT; - -(*decompose additions AND subtractions as a sum*) -fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (pos, u, ts)) - | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (not pos, u, ts)) - | dest_summing (pos, t, ts) = - if pos then t::ts else uminus_const$t :: ts; - -fun dest_sum t = dest_summing (true, t, []); - -val mk_diff = HOLogic.mk_binop "op -"; -val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT; - -val one = mk_numeral 1; -val mk_times = HOLogic.mk_binop "op *"; - -fun mk_prod [] = one - | mk_prod [t] = t - | mk_prod (t :: ts) = if t = one then mk_prod ts - else mk_times (t, mk_prod ts); - -val dest_times = HOLogic.dest_bin "op *" HOLogic.intT; - -fun dest_prod t = - let val (t,u) = dest_times t - in dest_prod t @ dest_prod u end - handle TERM _ => [t]; - -(*DON'T do the obvious simplifications; that would create special cases*) -fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); - -(*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t - | dest_coeff sign t = - let val ts = sort Term.term_ord (dest_prod t) - val (n, ts') = find_first_numeral [] ts - handle TERM _ => (1, ts) - in (sign*n, mk_prod ts') end; - -(*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) - | find_first_coeff past u (t::terms) = - let val (n,u') = dest_coeff 1 t - in if u aconv u' then (n, rev past @ terms) - else find_first_coeff (t::past) u terms - end - handle TERM _ => find_first_coeff (t::past) u terms; - - -(*Simplify #1*n and n*#1 to n*) -val add_0s = [zadd_0, zadd_0_right]; -val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right]; - -(*To perform binary arithmetic*) -val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps; - -(*To evaluate binary negations of coefficients*) -val zminus_simps = NCons_simps @ - [number_of_minus RS sym, - bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, - bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; - -(*To let us treat subtraction as addition*) -val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; - -(*Apply the given rewrite (if present) just once*) -fun trans_tac None = all_tac - | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); - -fun prove_conv name tacs sg (t, u) = - if t aconv u then None - else - let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) - in Some - (prove_goalw_cterm [] ct (K tacs) - handle ERROR => error - ("The error(s) above occurred while trying to prove " ^ - string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) - end; - -fun simplify_meta_eq rules = - mk_meta_eq o - simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) - -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; -fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT); -val prep_pats = map prep_pat; - -structure CancelNumeralsCommon = - struct - val mk_sum = mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val find_first_coeff = find_first_coeff [] - val trans_tac = trans_tac - val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - zminus_simps@zadd_ac)) - THEN ALLGOALS - (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ - bin_simps@zadd_ac@zmult_ac)) - val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) - val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) - end; - - -structure EqCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = prove_conv "inteq_cancel_numerals" - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT - val bal_add1 = eq_add_iff1 RS trans - val bal_add2 = eq_add_iff2 RS trans -); - -structure LessCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = prove_conv "intless_cancel_numerals" - val mk_bal = HOLogic.mk_binrel "op <" - val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT - val bal_add1 = less_add_iff1 RS trans - val bal_add2 = less_add_iff2 RS trans -); - -structure LeCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = prove_conv "intle_cancel_numerals" - val mk_bal = HOLogic.mk_binrel "op <=" - val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT - val bal_add1 = le_add_iff1 RS trans - val bal_add2 = le_add_iff2 RS trans -); - -val cancel_numerals = - map prep_simproc - [("inteq_cancel_numerals", - prep_pats ["(l::int) + m = n", "(l::int) = m + n", - "(l::int) - m = n", "(l::int) = m - n", - "(l::int) * m = n", "(l::int) = m * n"], - EqCancelNumerals.proc), - ("intless_cancel_numerals", - prep_pats ["(l::int) + m < n", "(l::int) < m + n", - "(l::int) - m < n", "(l::int) < m - n", - "(l::int) * m < n", "(l::int) < m * n"], - LessCancelNumerals.proc), - ("intle_cancel_numerals", - prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", - "(l::int) - m <= n", "(l::int) <= m - n", - "(l::int) * m <= n", "(l::int) <= m * n"], - LeCancelNumerals.proc)]; - - -structure CombineNumeralsData = - struct - val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val left_distrib = left_zadd_zmult_distrib RS trans - val prove_conv = prove_conv "int_combine_numerals" - val trans_tac = trans_tac - val norm_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - zminus_simps@zadd_ac)) - THEN ALLGOALS - (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ - bin_simps@zadd_ac@zmult_ac)) - val numeral_simp_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@bin_simps)) - val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) - end; - -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); - -val combine_numerals = - prep_simproc ("int_combine_numerals", - prep_pats ["(i::int) + j", "(i::int) - j"], - CombineNumerals.proc); - -end; - - -Addsimprocs Int_Numeral_Simprocs.cancel_numerals; -Addsimprocs [Int_Numeral_Simprocs.combine_numerals]; - -(*The Abel_Cancel simprocs are now obsolete*) -Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); - -test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)"; - -test "#2*u = (u::int)"; -test "(i + j + #12 + (k::int)) - #15 = y"; -test "(i + j + #12 + (k::int)) - #5 = y"; - -test "y - b < (b::int)"; -test "y - (#3*b + c) < (b::int) - #2*c"; - -test "(#2*x - (u*v) + y) - v*#3*u = (w::int)"; -test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)"; -test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)"; -test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)"; - -test "(i + j + #12 + (k::int)) = u + #15 + y"; -test "(i + j*#2 + #12 + (k::int)) = j + #5 + y"; - -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::int)"; - -test "a + -(b+c) + b = (d::int)"; -test "a + -(b+c) - b = (d::int)"; - -(*negative numerals*) -test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz"; -test "(i + j + #-3 + (k::int)) < u + #5 + y"; -test "(i + j + #3 + (k::int)) < u + #-6 + y"; -test "(i + j + #-12 + (k::int)) - #15 = y"; -test "(i + j + #12 + (k::int)) - #-15 = y"; -test "(i + j + #-12 + (k::int)) - #-15 = y"; -*) - - -(** Constant folding for integer plus and times **) - -(*We do not need - structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data); - structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data); - because combine_numerals does the same thing*) - -structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA = -struct - val ss = HOL_ss - val eq_reflection = eq_reflection - val thy = Bin.thy - val T = HOLogic.intT - val plus = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT); - val add_ac = zmult_ac -end; - -structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data); - -Addsimprocs [Int_Times_Assoc.conv]; - - -(** The same for the naturals **) - -structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA = -struct - val ss = HOL_ss - val eq_reflection = eq_reflection - val thy = Bin.thy - val T = HOLogic.natT - val plus = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT); - val add_ac = mult_ac -end; - -structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data); - -Addsimprocs [Nat_Times_Assoc.conv]; - - - -(*** decision procedure for linear arithmetic ***) - -(*---------------------------------------------------------------------------*) -(* Linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(* -Instantiation of the generic linear arithmetic package for int. -*) - -(* Update parameters of arithmetic prover *) -let - -(* reduce contradictory <= to False *) -val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ - [int_0, zadd_0, zadd_0_right, zdiff_def, - zadd_zminus_inverse, zadd_zminus_inverse2, - zmult_0, zmult_0_right, - zmult_1, zmult_1_right, - zmult_minus1, zmult_minus1_right, - zminus_zadd_distrib, zminus_zminus]; - -val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ - Int_Numeral_Simprocs.cancel_numerals; - -val add_mono_thms = - map (fn s => prove_goal Int.thy s - (fn prems => [cut_facts_tac prems 1, - asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) - ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", - "(i = j) & (k <= l) ==> i + k <= j + (l::int)", - "(i <= j) & (k = l) ==> i + k <= j + (l::int)", - "(i = j) & (k = l) ==> i + k = j + (l::int)" - ]; - -in -LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms; -LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2]; -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules - addsimprocs simprocs - addcongs [if_weak_cong]; -LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)] -end; - -let -val int_arith_simproc_pats = - map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT)) - ["(m::int) < n","(m::int) <= n", "(m::int) = n"]; - -val fast_int_arith_simproc = mk_simproc - "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover; -in -Addsimprocs [fast_int_arith_simproc] -end; - -(* Some test data -Goal "!!a::int. [| a <= b; c <= d; x+y a+c <= b+d"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ -\ ==> a+a <= j+j"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a+b < i+j; a a+a - - #-1 < j+j - #3"; -by (fast_arith_tac 1); -Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; -by (arith_tac 1); -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a <= l"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a+a+a+a <= l+l+l+l"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a+a+a+a+a <= l+l+l+l+i"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; -by (fast_arith_tac 1); -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> #6*a <= #5*l+i"; -by (fast_arith_tac 1); -*) - -(*---------------------------------------------------------------------------*) -(* End of linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(** Simplification of inequalities involving numerical constants **) - -Goal "(w <= z - (#1::int)) = (w<(z::int))"; -by (arith_tac 1); -qed "zle_diff1_eq"; -Addsimps [zle_diff1_eq]; - -Goal "(w < z + #1) = (w<=(z::int))"; -by (arith_tac 1); -qed "zle_add1_eq_le"; -Addsimps [zle_add1_eq_le]; - -Goal "(z = z + w) = (w = (#0::int))"; -by (arith_tac 1); -qed "zadd_left_cancel0"; -Addsimps [zadd_left_cancel0]; - - -(* nat *) - -Goal "#0 <= z ==> int (nat z) = z"; -by (asm_full_simp_tac - (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); -qed "nat_0_le"; - -Goal "z <= #0 ==> nat z = 0"; -by (case_tac "z = #0" 1); -by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); -by (asm_full_simp_tac - (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); -qed "nat_le_0"; - -Addsimps [nat_0_le, nat_le_0]; - -val [major,minor] = Goal "[| #0 <= z; !!m. z = int m ==> P |] ==> P"; -by (rtac (major RS nat_0_le RS sym RS minor) 1); -qed "nonneg_eq_int"; - -Goal "#0 <= w ==> (nat w = m) = (w = int m)"; -by Auto_tac; -qed "nat_eq_iff"; - -Goal "#0 <= w ==> (m = nat w) = (w = int m)"; -by Auto_tac; -qed "nat_eq_iff2"; - -Goal "#0 <= w ==> (nat w < m) = (w < int m)"; -by (rtac iffI 1); -by (asm_full_simp_tac - (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); -by (etac (nat_0_le RS subst) 1); -by (Simp_tac 1); -qed "nat_less_iff"; - - -(*Users don't want to see (int 0), int(Suc 0) or w + - z*) -Addsimps [int_0, int_Suc, symmetric zdiff_def]; - -Goal "nat #0 = 0"; -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); -qed "nat_0"; - -Goal "nat #1 = 1"; -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); -qed "nat_1"; - -Goal "nat #2 = 2"; -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); -qed "nat_2"; - -Goal "#0 <= w ==> (nat w < nat z) = (w (nat w <= nat z) = (w<=z)"; -by (auto_tac (claset(), - simpset() addsimps [linorder_not_less RS sym, - zless_nat_conj])); -qed "nat_le_eq_zle"; - -(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*) -Goal "n<=m --> int m - int n = int (m-n)"; -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by Auto_tac; -qed_spec_mp "zdiff_int"; - - -(*** abs: absolute value, as an integer ****) - -(* Simpler: use zabs_def as rewrite rule; - but arith_tac is not parameterized by such simp rules -*) -Goalw [zabs_def] - "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))"; -by(Simp_tac 1); -qed "zabs_split"; - -arith_tac_split_thms := !arith_tac_split_thms @ [zabs_split]; - Goal "abs(abs(x::int)) = abs(x)"; by(arith_tac 1); qed "abs_abs"; @@ -634,4 +67,3 @@ simpset() addsimps [int_0_less_mult_iff, linorder_not_less RS sym])); qed "zmult_le_0_iff"; - diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Integ/IntArith.thy Tue Jul 25 00:06:46 2000 +0200 @@ -1,2 +1,8 @@ -theory IntArith = Bin: + +theory IntArith = Bin +files ("int_arith1.ML") ("int_arith2.ML"): + +use "int_arith1.ML" setup int_arith_setup +use "int_arith2.ML" lemmas [arith_split] = zabs_split + end diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/NatSimprocs.ML --- a/src/HOL/Integ/NatSimprocs.ML Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Integ/NatSimprocs.ML Tue Jul 25 00:06:46 2000 +0200 @@ -3,374 +3,9 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2000 University of Cambridge -Simprocs for nat numerals +Simprocs for nat numerals (see also nat_simprocs.ML). *) -Goal "number_of v + (number_of v' + (k::nat)) = \ -\ (if neg (number_of v) then number_of v' + k \ -\ else if neg (number_of v') then number_of v + k \ -\ else number_of (bin_add v v') + k)"; -by (Simp_tac 1); -qed "nat_number_of_add_left"; - - -(** For combine_numerals **) - -Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)"; -by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1); -qed "left_add_mult_distrib"; - - -(** For cancel_numerals **) - -Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"; -by (asm_simp_tac (simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib]) 1); -qed "nat_diff_add_eq1"; - -Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"; -by (asm_simp_tac (simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib]) 1); -qed "nat_diff_add_eq2"; - -Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"; -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib])); -qed "nat_eq_add_iff1"; - -Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"; -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib])); -qed "nat_eq_add_iff2"; - -Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"; -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib])); -qed "nat_less_add_iff1"; - -Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"; -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib])); -qed "nat_less_add_iff2"; - -Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib])); -qed "nat_le_add_iff1"; - -Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] - addsimps [add_mult_distrib])); -qed "nat_le_add_iff2"; - - -structure Nat_Numeral_Simprocs = -struct - -(*Utilities*) - -fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ - NumeralSyntax.mk_bin n; - -(*Decodes a unary or binary numeral to a NATURAL NUMBER*) -fun dest_numeral (Const ("0", _)) = 0 - | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t - | dest_numeral (Const("Numeral.number_of", _) $ w) = - (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w) - handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w])) - | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]); - -fun find_first_numeral past (t::terms) = - ((dest_numeral t, t, rev past @ terms) - handle TERM _ => find_first_numeral (t::past) terms) - | find_first_numeral past [] = raise TERM("find_first_numeral", []); - -val zero = mk_numeral 0; -val mk_plus = HOLogic.mk_binop "op +"; - -(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) -fun mk_sum [] = zero - | mk_sum [t,u] = mk_plus (t, u) - | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -(*this version ALWAYS includes a trailing zero*) -fun long_mk_sum [] = zero - | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; - -(*extract the outer Sucs from a term and convert them to a binary numeral*) -fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t) - | dest_Sucs (0, t) = t - | dest_Sucs (k, t) = mk_plus (mk_numeral k, t); - -fun dest_sum t = - let val (t,u) = dest_plus t - in dest_sum t @ dest_sum u end - handle TERM _ => [t]; - -fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t)); - -val trans_tac = Int_Numeral_Simprocs.trans_tac; - -val prove_conv = Int_Numeral_Simprocs.prove_conv; - -val bin_simps = [add_nat_number_of, nat_number_of_add_left, - diff_nat_number_of, le_nat_number_of_eq_not_less, - less_nat_number_of, Let_number_of, nat_number_of] @ - bin_arith_simps @ bin_rel_simps; - -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; -fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT); -val prep_pats = map prep_pat; - - -(*** CancelNumerals simprocs ***) - -val one = mk_numeral 1; -val mk_times = HOLogic.mk_binop "op *"; - -fun mk_prod [] = one - | mk_prod [t] = t - | mk_prod (t :: ts) = if t = one then mk_prod ts - else mk_times (t, mk_prod ts); - -val dest_times = HOLogic.dest_bin "op *" HOLogic.natT; - -fun dest_prod t = - let val (t,u) = dest_times t - in dest_prod t @ dest_prod u end - handle TERM _ => [t]; - -(*DON'T do the obvious simplifications; that would create special cases*) -fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); - -(*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff t = - let val ts = sort Term.term_ord (dest_prod t) - val (n, _, ts') = find_first_numeral [] ts - handle TERM _ => (1, one, ts) - in (n, mk_prod ts') end; - -(*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) - | find_first_coeff past u (t::terms) = - let val (n,u') = dest_coeff t - in if u aconv u' then (n, rev past @ terms) - else find_first_coeff (t::past) u terms - end - handle TERM _ => find_first_coeff (t::past) u terms; - - -(*Simplify #1*n and n*#1 to n*) -val add_0s = map (rename_numerals NatBin.thy) [add_0, add_0_right]; -val mult_1s = map (rename_numerals NatBin.thy) [mult_1, mult_1_right]; - -(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*) -val simplify_meta_eq = - Int_Numeral_Simprocs.simplify_meta_eq - [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right, - mult_0, mult_0_right, mult_1, mult_1_right]; - -structure CancelNumeralsCommon = - struct - val mk_sum = mk_sum - val dest_sum = dest_Sucs_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first_coeff = find_first_coeff [] - val trans_tac = trans_tac - val norm_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@mult_1s@ - [add_0, Suc_eq_add_numeral_1]@add_ac)) - THEN ALLGOALS (simp_tac - (HOL_ss addsimps bin_simps@add_ac@mult_ac)) - val numeral_simp_tac = ALLGOALS - (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) - val simplify_meta_eq = simplify_meta_eq - end; - - -structure EqCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = prove_conv "nateq_cancel_numerals" - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val bal_add1 = nat_eq_add_iff1 RS trans - val bal_add2 = nat_eq_add_iff2 RS trans -); - -structure LessCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = prove_conv "natless_cancel_numerals" - val mk_bal = HOLogic.mk_binrel "op <" - val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT - val bal_add1 = nat_less_add_iff1 RS trans - val bal_add2 = nat_less_add_iff2 RS trans -); - -structure LeCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = prove_conv "natle_cancel_numerals" - val mk_bal = HOLogic.mk_binrel "op <=" - val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT - val bal_add1 = nat_le_add_iff1 RS trans - val bal_add2 = nat_le_add_iff2 RS trans -); - -structure DiffCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = prove_conv "natdiff_cancel_numerals" - val mk_bal = HOLogic.mk_binop "op -" - val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT - val bal_add1 = nat_diff_add_eq1 RS trans - val bal_add2 = nat_diff_add_eq2 RS trans -); - - -val cancel_numerals = - map prep_simproc - [("nateq_cancel_numerals", - prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", - "(l::nat) * m = n", "(l::nat) = m * n", - "Suc m = n", "m = Suc n"], - EqCancelNumerals.proc), - ("natless_cancel_numerals", - prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", - "(l::nat) * m < n", "(l::nat) < m * n", - "Suc m < n", "m < Suc n"], - LessCancelNumerals.proc), - ("natle_cancel_numerals", - prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", - "(l::nat) * m <= n", "(l::nat) <= m * n", - "Suc m <= n", "m <= Suc n"], - LeCancelNumerals.proc), - ("natdiff_cancel_numerals", - prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", - "(l::nat) * m - n", "(l::nat) - m * n", - "Suc m - n", "m - Suc n"], - DiffCancelNumerals.proc)]; - - -structure CombineNumeralsData = - struct - val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) - val dest_sum = dest_Sucs_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val left_distrib = left_add_mult_distrib RS trans - val prove_conv = prove_conv "nat_combine_numerals" - val trans_tac = trans_tac - val norm_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@mult_1s@ - [add_0, Suc_eq_add_numeral_1]@add_ac)) - THEN ALLGOALS (simp_tac - (HOL_ss addsimps bin_simps@add_ac@mult_ac)) - val numeral_simp_tac = ALLGOALS - (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) - val simplify_meta_eq = simplify_meta_eq - end; - -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); - -val combine_numerals = - prep_simproc ("nat_combine_numerals", - prep_pats ["(i::nat) + j", "Suc (i + j)"], - CombineNumerals.proc); - -end; - - -Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; -Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; - - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); - -(*cancel_numerals*) -test "l +( #2) + (#2) + #2 + (l + #2) + (oo + #2) = (uu::nat)"; -test "(#2*length xs < #2*length xs + j)"; -test "(#2*length xs < length xs * #2 + j)"; -test "#2*u = (u::nat)"; -test "#2*u = Suc (u)"; -test "(i + j + #12 + (k::nat)) - #15 = y"; -test "(i + j + #12 + (k::nat)) - #5 = y"; -test "Suc u - #2 = y"; -test "Suc (Suc (Suc u)) - #2 = y"; -test "(i + j + #2 + (k::nat)) - 1 = y"; -test "(i + j + #1 + (k::nat)) - 2 = y"; - -test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)"; -test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)"; -test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)"; -test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w"; -test "Suc ((u*v)*#4) - v*#3*u = w"; -test "Suc (Suc ((u*v)*#3)) - v*#3*u = w"; - -test "(i + j + #12 + (k::nat)) = u + #15 + y"; -test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz"; -test "(i + j + #12 + (k::nat)) = u + #5 + y"; -(*Suc*) -test "(i + j + #12 + k) = Suc (u + y)"; -test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)"; -test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; -test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v"; -test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; -test "#2*y + #3*z + #2*u = Suc (u)"; -test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)"; -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::nat)"; -test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)"; -test "(#2*n*m) < (#3*(m*n)) + (u::nat)"; - -(*negative numerals: FAIL*) -test "(i + j + #-23 + (k::nat)) < u + #15 + y"; -test "(i + j + #3 + (k::nat)) < u + #-15 + y"; -test "(i + j + #-12 + (k::nat)) - #15 = y"; -test "(i + j + #12 + (k::nat)) - #-15 = y"; -test "(i + j + #-12 + (k::nat)) - #-15 = y"; - -(*combine_numerals*) -test "k + #3*k = (u::nat)"; -test "Suc (i + #3) = u"; -test "Suc (i + j + #3 + k) = u"; -test "k + j + #3*k + j = (u::nat)"; -test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)"; -test "(#2*n*m) + (#3*(m*n)) = (u::nat)"; -(*negative numerals: FAIL*) -test "Suc (i + j + #-3 + k) = u"; -*) - - -(*** Prepare linear arithmetic for nat numerals ***) - -let - -(* reduce contradictory <= to False *) -val add_rules = - [add_nat_number_of, diff_nat_number_of, mult_nat_number_of, - eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, - le_Suc_number_of,le_number_of_Suc, - less_Suc_number_of,less_number_of_Suc, - Suc_eq_number_of,eq_number_of_Suc, - eq_number_of_0, eq_0_number_of, less_0_number_of, - nat_number_of, Let_number_of, if_True, if_False]; - -val simprocs = [Nat_Times_Assoc.conv, - Nat_Numeral_Simprocs.combine_numerals]@ - Nat_Numeral_Simprocs.cancel_numerals; - -in -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules - addsimps basic_renamed_arith_simps - addsimprocs simprocs -end; - - - (** For simplifying Suc m - #n **) Goal "#0 < n ==> Suc m - n = m - (n - #1)"; @@ -393,8 +28,8 @@ by (Simp_tac 1); by (Simp_tac 1); by (asm_full_simp_tac - (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, - neg_number_of_bin_pred_iff_0]) 1); + (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, + neg_number_of_bin_pred_iff_0]) 1); qed "Suc_diff_number_of"; (* now redundant because of the inverse_fold simproc @@ -405,8 +40,8 @@ \ if neg pv then a else f (nat pv))"; by (simp_tac (simpset() addsplits [nat.split] - addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1); -qed "nat_case_number_of"; + addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1); +qed "nat_case_number_of"; Goal "nat_case a f ((number_of v) + n) = \ \ (let pv = number_of (bin_pred v) in \ @@ -414,8 +49,8 @@ by (stac add_eq_if 1); by (asm_simp_tac (simpset() addsplits [nat.split] - addsimps [Let_def, neg_imp_number_of_eq_0, - neg_number_of_bin_pred_iff_0]) 1); + addsimps [Let_def, neg_imp_number_of_eq_0, + neg_number_of_bin_pred_iff_0]) 1); qed "nat_case_add_eq_if"; Addsimps [nat_case_number_of, nat_case_add_eq_if]; @@ -426,9 +61,9 @@ \ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"; by (case_tac "(number_of v)::nat" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0]))); + (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0]))); by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1); -qed "nat_rec_number_of"; +qed "nat_rec_number_of"; Goal "nat_rec a f (number_of v + n) = \ \ (let pv = number_of (bin_pred v) in \ @@ -437,9 +72,9 @@ by (stac add_eq_if 1); by (asm_simp_tac (simpset() addsplits [nat.split] - addsimps [Let_def, neg_imp_number_of_eq_0, - neg_number_of_bin_pred_iff_0]) 1); -qed "nat_rec_add_eq_if"; + addsimps [Let_def, neg_imp_number_of_eq_0, + neg_number_of_bin_pred_iff_0]) 1); +qed "nat_rec_add_eq_if"; Addsimps [nat_rec_number_of, nat_rec_add_eq_if]; @@ -476,7 +111,7 @@ by (Asm_simp_tac 2); by (auto_tac (claset(), simpset() delsimps [mod_less_divisor])); qed "mod2_gr_0"; -Addsimps [mod2_gr_0, rename_numerals thy mod2_gr_0]; +Addsimps [mod2_gr_0, rename_numerals mod2_gr_0]; (** Removal of small numerals: #0, #1 and (in additive positions) #2 **) diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/NatSimprocs.thy --- a/src/HOL/Integ/NatSimprocs.thy Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Integ/NatSimprocs.thy Tue Jul 25 00:06:46 2000 +0200 @@ -1,2 +1,7 @@ -theory NatSimprocs = NatBin: + +theory NatSimprocs = NatBin +files "nat_simprocs.ML": + +setup nat_simprocs_setup + end diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/int_arith1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Integ/int_arith1.ML Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,467 @@ +(* Title: HOL/Integ/int_arith1.ML + ID: $Id$ + Authors: Larry Paulson and Tobias Nipkow + +Simprocs and decision procedure for linear arithmetic. +*) + +(*** Simprocs for numeric literals ***) + +(** Combining of literal coefficients in sums of products **) + +Goal "(x < y) = (x-y < (#0::int))"; +by (simp_tac (simpset() addsimps zcompare_rls) 1); +qed "zless_iff_zdiff_zless_0"; + +Goal "(x = y) = (x-y = (#0::int))"; +by (simp_tac (simpset() addsimps zcompare_rls) 1); +qed "eq_iff_zdiff_eq_0"; + +Goal "(x <= y) = (x-y <= (#0::int))"; +by (simp_tac (simpset() addsimps zcompare_rls) 1); +qed "zle_iff_zdiff_zle_0"; + + +(** For combine_numerals **) + +Goal "i*u + (j*u + k) = (i+j)*u + (k::int)"; +by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); +qed "left_zadd_zmult_distrib"; + + +(** For cancel_numerals **) + +val rel_iff_rel_0_rls = map (inst "y" "?u+?v") + [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, + zle_iff_zdiff_zle_0] @ + map (inst "y" "n") + [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, + zle_iff_zdiff_zle_0]; + +Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ + zadd_ac@rel_iff_rel_0_rls) 1); +qed "eq_add_iff1"; + +Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ + zadd_ac@rel_iff_rel_0_rls) 1); +qed "eq_add_iff2"; + +Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ + zadd_ac@rel_iff_rel_0_rls) 1); +qed "less_add_iff1"; + +Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ + zadd_ac@rel_iff_rel_0_rls) 1); +qed "less_add_iff2"; + +Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ + zadd_ac@rel_iff_rel_0_rls) 1); +qed "le_add_iff1"; + +Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib] + @zadd_ac@rel_iff_rel_0_rls) 1); +qed "le_add_iff2"; + +(*To tidy up the result of a simproc. Only the RHS will be simplified.*) +Goal "u = u' ==> (t==u) == (t==u')"; +by Auto_tac; +qed "eq_cong2"; + + +structure Int_Numeral_Simprocs = +struct + +(*Utilities*) + +fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ + NumeralSyntax.mk_bin n; + +(*Decodes a binary INTEGER*) +fun dest_numeral (Const("Numeral.number_of", _) $ w) = + (NumeralSyntax.dest_bin w + handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) + | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); + +fun find_first_numeral past (t::terms) = + ((dest_numeral t, rev past @ terms) + handle TERM _ => find_first_numeral (t::past) terms) + | find_first_numeral past [] = raise TERM("find_first_numeral", []); + +val zero = mk_numeral 0; +val mk_plus = HOLogic.mk_binop "op +"; + +val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT); + +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) +fun mk_sum [] = zero + | mk_sum [t,u] = mk_plus (t, u) + | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +(*this version ALWAYS includes a trailing zero*) +fun long_mk_sum [] = zero + | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT; + +(*decompose additions AND subtractions as a sum*) +fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (pos, u, ts)) + | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (not pos, u, ts)) + | dest_summing (pos, t, ts) = + if pos then t::ts else uminus_const$t :: ts; + +fun dest_sum t = dest_summing (true, t, []); + +val mk_diff = HOLogic.mk_binop "op -"; +val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT; + +val one = mk_numeral 1; +val mk_times = HOLogic.mk_binop "op *"; + +fun mk_prod [] = one + | mk_prod [t] = t + | mk_prod (t :: ts) = if t = one then mk_prod ts + else mk_times (t, mk_prod ts); + +val dest_times = HOLogic.dest_bin "op *" HOLogic.intT; + +fun dest_prod t = + let val (t,u) = dest_times t + in dest_prod t @ dest_prod u end + handle TERM _ => [t]; + +(*DON'T do the obvious simplifications; that would create special cases*) +fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); + +(*Express t as a product of (possibly) a numeral with other sorted terms*) +fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t + | dest_coeff sign t = + let val ts = sort Term.term_ord (dest_prod t) + val (n, ts') = find_first_numeral [] ts + handle TERM _ => (1, ts) + in (sign*n, mk_prod ts') end; + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff 1 t + in if u aconv u' then (n, rev past @ terms) + else find_first_coeff (t::past) u terms + end + handle TERM _ => find_first_coeff (t::past) u terms; + + +(*Simplify #1*n and n*#1 to n*) +val add_0s = [zadd_0, zadd_0_right]; +val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right]; + +(*To perform binary arithmetic*) +val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps; + +(*To evaluate binary negations of coefficients*) +val zminus_simps = NCons_simps @ + [number_of_minus RS sym, + bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, + bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; + +(*To let us treat subtraction as addition*) +val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; + +(*Apply the given rewrite (if present) just once*) +fun trans_tac None = all_tac + | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); + +fun prove_conv name tacs sg (t, u) = + if t aconv u then None + else + let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) + in Some + (prove_goalw_cterm [] ct (K tacs) + handle ERROR => error + ("The error(s) above occurred while trying to prove " ^ + string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) + end; + +fun simplify_meta_eq rules = + mk_meta_eq o + simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) + +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT); +val prep_pats = map prep_pat; + +structure CancelNumeralsCommon = + struct + val mk_sum = mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val find_first_coeff = find_first_coeff [] + val trans_tac = trans_tac + val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ + zminus_simps@zadd_ac)) + THEN ALLGOALS + (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ + bin_simps@zadd_ac@zmult_ac)) + val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) + val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) + end; + + +structure EqCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = prove_conv "inteq_cancel_numerals" + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT + val bal_add1 = eq_add_iff1 RS trans + val bal_add2 = eq_add_iff2 RS trans +); + +structure LessCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = prove_conv "intless_cancel_numerals" + val mk_bal = HOLogic.mk_binrel "op <" + val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT + val bal_add1 = less_add_iff1 RS trans + val bal_add2 = less_add_iff2 RS trans +); + +structure LeCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = prove_conv "intle_cancel_numerals" + val mk_bal = HOLogic.mk_binrel "op <=" + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT + val bal_add1 = le_add_iff1 RS trans + val bal_add2 = le_add_iff2 RS trans +); + +val cancel_numerals = + map prep_simproc + [("inteq_cancel_numerals", + prep_pats ["(l::int) + m = n", "(l::int) = m + n", + "(l::int) - m = n", "(l::int) = m - n", + "(l::int) * m = n", "(l::int) = m * n"], + EqCancelNumerals.proc), + ("intless_cancel_numerals", + prep_pats ["(l::int) + m < n", "(l::int) < m + n", + "(l::int) - m < n", "(l::int) < m - n", + "(l::int) * m < n", "(l::int) < m * n"], + LessCancelNumerals.proc), + ("intle_cancel_numerals", + prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", + "(l::int) - m <= n", "(l::int) <= m - n", + "(l::int) * m <= n", "(l::int) <= m * n"], + LeCancelNumerals.proc)]; + + +structure CombineNumeralsData = + struct + val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val left_distrib = left_zadd_zmult_distrib RS trans + val prove_conv = prove_conv "int_combine_numerals" + val trans_tac = trans_tac + val norm_tac = ALLGOALS + (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ + zminus_simps@zadd_ac)) + THEN ALLGOALS + (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ + bin_simps@zadd_ac@zmult_ac)) + val numeral_simp_tac = ALLGOALS + (simp_tac (HOL_ss addsimps add_0s@bin_simps)) + val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) + end; + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); + +val combine_numerals = + prep_simproc ("int_combine_numerals", + prep_pats ["(i::int) + j", "(i::int) - j"], + CombineNumerals.proc); + +end; + +Addsimprocs Int_Numeral_Simprocs.cancel_numerals; +Addsimprocs [Int_Numeral_Simprocs.combine_numerals]; + +(*The Abel_Cancel simprocs are now obsolete*) +Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)"; + +test "#2*u = (u::int)"; +test "(i + j + #12 + (k::int)) - #15 = y"; +test "(i + j + #12 + (k::int)) - #5 = y"; + +test "y - b < (b::int)"; +test "y - (#3*b + c) < (b::int) - #2*c"; + +test "(#2*x - (u*v) + y) - v*#3*u = (w::int)"; +test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)"; +test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)"; +test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)"; + +test "(i + j + #12 + (k::int)) = u + #15 + y"; +test "(i + j*#2 + #12 + (k::int)) = j + #5 + y"; + +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::int)"; + +test "a + -(b+c) + b = (d::int)"; +test "a + -(b+c) - b = (d::int)"; + +(*negative numerals*) +test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz"; +test "(i + j + #-3 + (k::int)) < u + #5 + y"; +test "(i + j + #3 + (k::int)) < u + #-6 + y"; +test "(i + j + #-12 + (k::int)) - #15 = y"; +test "(i + j + #12 + (k::int)) - #-15 = y"; +test "(i + j + #-12 + (k::int)) - #-15 = y"; +*) + + +(** Constant folding for integer plus and times **) + +(*We do not need + structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data); + structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data); + because combine_numerals does the same thing*) + +structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA = +struct + val ss = HOL_ss + val eq_reflection = eq_reflection + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) + val T = HOLogic.intT + val plus = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT); + val add_ac = zmult_ac +end; + +structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data); + +Addsimprocs [Int_Times_Assoc.conv]; + + +(** The same for the naturals **) + +structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA = +struct + val ss = HOL_ss + val eq_reflection = eq_reflection + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) + val T = HOLogic.natT + val plus = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT); + val add_ac = mult_ac +end; + +structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data); + +Addsimprocs [Nat_Times_Assoc.conv]; + + +(*** decision procedure for linear arithmetic ***) + +(*---------------------------------------------------------------------------*) +(* Linear arithmetic *) +(*---------------------------------------------------------------------------*) + +(* +Instantiation of the generic linear arithmetic package for int. +*) + +(* Update parameters of arithmetic prover *) +local + +(* reduce contradictory <= to False *) +val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ + [int_0, zadd_0, zadd_0_right, zdiff_def, + zadd_zminus_inverse, zadd_zminus_inverse2, + zmult_0, zmult_0_right, + zmult_1, zmult_1_right, + zmult_minus1, zmult_minus1_right, + zminus_zadd_distrib, zminus_zminus]; + +val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ + Int_Numeral_Simprocs.cancel_numerals; + +val add_mono_thms_int = + map (fn s => prove_goal (the_context ()) s + (fn prems => [cut_facts_tac prems 1, + asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) + ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", + "(i = j) & (k <= l) ==> i + k <= j + (l::int)", + "(i <= j) & (k = l) ==> i + k <= j + (l::int)", + "(i = j) & (k = l) ==> i + k = j + (l::int)" + ]; + +in + +val int_arith_setup = + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} => + {add_mono_thms = add_mono_thms @ add_mono_thms_int, + lessD = lessD @ [add1_zle_eq RS iffD2], + simpset = simpset addsimps add_rules + addsimprocs simprocs + addcongs [if_weak_cong]}), + arith_discrete ("IntDef.int", true)]; + +end; + +let +val int_arith_simproc_pats = + map (fn s => Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.boolT)) + ["(m::int) < n","(m::int) <= n", "(m::int) = n"]; + +val fast_int_arith_simproc = mk_simproc + "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover; +in +Addsimprocs [fast_int_arith_simproc] +end; + +(* Some test data +Goal "!!a::int. [| a <= b; c <= d; x+y a+c <= b+d"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ +\ ==> a+a <= j+j"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a+b < i+j; a a+a - - #-1 < j+j - #3"; +by (fast_arith_tac 1); +Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; +by (arith_tac 1); +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a <= l"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a+a+a+a <= l+l+l+l"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a+a+a+a+a <= l+l+l+l+i"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; +by (fast_arith_tac 1); +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> #6*a <= #5*l+i"; +by (fast_arith_tac 1); +*) diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/int_arith2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Integ/int_arith2.ML Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,107 @@ +(* Title: HOL/Integ/int_arith2.ML + ID: $Id$ + Authors: Larry Paulson and Tobias Nipkow +*) + +(** Simplification of inequalities involving numerical constants **) + +Goal "(w <= z - (#1::int)) = (w<(z::int))"; +by (arith_tac 1); +qed "zle_diff1_eq"; +Addsimps [zle_diff1_eq]; + +Goal "(w < z + #1) = (w<=(z::int))"; +by (arith_tac 1); +qed "zle_add1_eq_le"; +Addsimps [zle_add1_eq_le]; + +Goal "(z = z + w) = (w = (#0::int))"; +by (arith_tac 1); +qed "zadd_left_cancel0"; +Addsimps [zadd_left_cancel0]; + + +(* nat *) + +Goal "#0 <= z ==> int (nat z) = z"; +by (asm_full_simp_tac + (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); +qed "nat_0_le"; + +Goal "z <= #0 ==> nat z = 0"; +by (case_tac "z = #0" 1); +by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); +by (asm_full_simp_tac + (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); +qed "nat_le_0"; + +Addsimps [nat_0_le, nat_le_0]; + +val [major,minor] = Goal "[| #0 <= z; !!m. z = int m ==> P |] ==> P"; +by (rtac (major RS nat_0_le RS sym RS minor) 1); +qed "nonneg_eq_int"; + +Goal "#0 <= w ==> (nat w = m) = (w = int m)"; +by Auto_tac; +qed "nat_eq_iff"; + +Goal "#0 <= w ==> (m = nat w) = (w = int m)"; +by Auto_tac; +qed "nat_eq_iff2"; + +Goal "#0 <= w ==> (nat w < m) = (w < int m)"; +by (rtac iffI 1); +by (asm_full_simp_tac + (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); +by (etac (nat_0_le RS subst) 1); +by (Simp_tac 1); +qed "nat_less_iff"; + + +(*Users don't want to see (int 0), int(Suc 0) or w + - z*) +Addsimps [int_0, int_Suc, symmetric zdiff_def]; + +Goal "nat #0 = 0"; +by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); +qed "nat_0"; + +Goal "nat #1 = 1"; +by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); +qed "nat_1"; + +Goal "nat #2 = 2"; +by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); +qed "nat_2"; + +Goal "#0 <= w ==> (nat w < nat z) = (w (nat w <= nat z) = (w<=z)"; +by (auto_tac (claset(), + simpset() addsimps [linorder_not_less RS sym, + zless_nat_conj])); +qed "nat_le_eq_zle"; + +(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*) +Goal "n<=m --> int m - int n = int (m-n)"; +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); +by Auto_tac; +qed_spec_mp "zdiff_int"; + + +(*** abs: absolute value, as an integer ****) + +(* Simpler: use zabs_def as rewrite rule; + but arith_tac is not parameterized by such simp rules +*) + +Goalw [zabs_def] + "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))"; +by(Simp_tac 1); +qed "zabs_split"; + +(*continued in IntArith.ML ...*) diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/nat_simprocs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Integ/nat_simprocs.ML Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,375 @@ +(* Title: HOL/nat_simprocs.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2000 University of Cambridge + +Simprocs for nat numerals. +*) + +Goal "number_of v + (number_of v' + (k::nat)) = \ +\ (if neg (number_of v) then number_of v' + k \ +\ else if neg (number_of v') then number_of v + k \ +\ else number_of (bin_add v v') + k)"; +by (Simp_tac 1); +qed "nat_number_of_add_left"; + + +(** For combine_numerals **) + +Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)"; +by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1); +qed "left_add_mult_distrib"; + + +(** For cancel_numerals **) + +Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"; +by (asm_simp_tac (simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib]) 1); +qed "nat_diff_add_eq1"; + +Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"; +by (asm_simp_tac (simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib]) 1); +qed "nat_diff_add_eq2"; + +Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"; +by (auto_tac (claset(), simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib])); +qed "nat_eq_add_iff1"; + +Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"; +by (auto_tac (claset(), simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib])); +qed "nat_eq_add_iff2"; + +Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"; +by (auto_tac (claset(), simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib])); +qed "nat_less_add_iff1"; + +Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"; +by (auto_tac (claset(), simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib])); +qed "nat_less_add_iff2"; + +Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; +by (auto_tac (claset(), simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib])); +qed "nat_le_add_iff1"; + +Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; +by (auto_tac (claset(), simpset() addsplits [nat_diff_split] + addsimps [add_mult_distrib])); +qed "nat_le_add_iff2"; + + +structure Nat_Numeral_Simprocs = +struct + +(*Utilities*) + +fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ + NumeralSyntax.mk_bin n; + +(*Decodes a unary or binary numeral to a NATURAL NUMBER*) +fun dest_numeral (Const ("0", _)) = 0 + | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t + | dest_numeral (Const("Numeral.number_of", _) $ w) = + (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w) + handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w])) + | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]); + +fun find_first_numeral past (t::terms) = + ((dest_numeral t, t, rev past @ terms) + handle TERM _ => find_first_numeral (t::past) terms) + | find_first_numeral past [] = raise TERM("find_first_numeral", []); + +val zero = mk_numeral 0; +val mk_plus = HOLogic.mk_binop "op +"; + +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) +fun mk_sum [] = zero + | mk_sum [t,u] = mk_plus (t, u) + | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +(*this version ALWAYS includes a trailing zero*) +fun long_mk_sum [] = zero + | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; + +(*extract the outer Sucs from a term and convert them to a binary numeral*) +fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t) + | dest_Sucs (0, t) = t + | dest_Sucs (k, t) = mk_plus (mk_numeral k, t); + +fun dest_sum t = + let val (t,u) = dest_plus t + in dest_sum t @ dest_sum u end + handle TERM _ => [t]; + +fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t)); + +val trans_tac = Int_Numeral_Simprocs.trans_tac; + +val prove_conv = Int_Numeral_Simprocs.prove_conv; + +val bin_simps = [add_nat_number_of, nat_number_of_add_left, + diff_nat_number_of, le_nat_number_of_eq_not_less, + less_nat_number_of, Let_number_of, nat_number_of] @ + bin_arith_simps @ bin_rel_simps; + +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT); +val prep_pats = map prep_pat; + + +(*** CancelNumerals simprocs ***) + +val one = mk_numeral 1; +val mk_times = HOLogic.mk_binop "op *"; + +fun mk_prod [] = one + | mk_prod [t] = t + | mk_prod (t :: ts) = if t = one then mk_prod ts + else mk_times (t, mk_prod ts); + +val dest_times = HOLogic.dest_bin "op *" HOLogic.natT; + +fun dest_prod t = + let val (t,u) = dest_times t + in dest_prod t @ dest_prod u end + handle TERM _ => [t]; + +(*DON'T do the obvious simplifications; that would create special cases*) +fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); + +(*Express t as a product of (possibly) a numeral with other sorted terms*) +fun dest_coeff t = + let val ts = sort Term.term_ord (dest_prod t) + val (n, _, ts') = find_first_numeral [] ts + handle TERM _ => (1, one, ts) + in (n, mk_prod ts') end; + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff t + in if u aconv u' then (n, rev past @ terms) + else find_first_coeff (t::past) u terms + end + handle TERM _ => find_first_coeff (t::past) u terms; + + +(*Simplify #1*n and n*#1 to n*) +val add_0s = map rename_numerals [add_0, add_0_right]; +val mult_1s = map rename_numerals [mult_1, mult_1_right]; + +(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*) +val simplify_meta_eq = + Int_Numeral_Simprocs.simplify_meta_eq + [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right, + mult_0, mult_0_right, mult_1, mult_1_right]; + +structure CancelNumeralsCommon = + struct + val mk_sum = mk_sum + val dest_sum = dest_Sucs_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first_coeff = find_first_coeff [] + val trans_tac = trans_tac + val norm_tac = ALLGOALS + (simp_tac (HOL_ss addsimps add_0s@mult_1s@ + [add_0, Suc_eq_add_numeral_1]@add_ac)) + THEN ALLGOALS (simp_tac + (HOL_ss addsimps bin_simps@add_ac@mult_ac)) + val numeral_simp_tac = ALLGOALS + (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) + val simplify_meta_eq = simplify_meta_eq + end; + + +structure EqCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = prove_conv "nateq_cancel_numerals" + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val bal_add1 = nat_eq_add_iff1 RS trans + val bal_add2 = nat_eq_add_iff2 RS trans +); + +structure LessCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = prove_conv "natless_cancel_numerals" + val mk_bal = HOLogic.mk_binrel "op <" + val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT + val bal_add1 = nat_less_add_iff1 RS trans + val bal_add2 = nat_less_add_iff2 RS trans +); + +structure LeCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = prove_conv "natle_cancel_numerals" + val mk_bal = HOLogic.mk_binrel "op <=" + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT + val bal_add1 = nat_le_add_iff1 RS trans + val bal_add2 = nat_le_add_iff2 RS trans +); + +structure DiffCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = prove_conv "natdiff_cancel_numerals" + val mk_bal = HOLogic.mk_binop "op -" + val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT + val bal_add1 = nat_diff_add_eq1 RS trans + val bal_add2 = nat_diff_add_eq2 RS trans +); + + +val cancel_numerals = + map prep_simproc + [("nateq_cancel_numerals", + prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", + "(l::nat) * m = n", "(l::nat) = m * n", + "Suc m = n", "m = Suc n"], + EqCancelNumerals.proc), + ("natless_cancel_numerals", + prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", + "(l::nat) * m < n", "(l::nat) < m * n", + "Suc m < n", "m < Suc n"], + LessCancelNumerals.proc), + ("natle_cancel_numerals", + prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", + "(l::nat) * m <= n", "(l::nat) <= m * n", + "Suc m <= n", "m <= Suc n"], + LeCancelNumerals.proc), + ("natdiff_cancel_numerals", + prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", + "(l::nat) * m - n", "(l::nat) - m * n", + "Suc m - n", "m - Suc n"], + DiffCancelNumerals.proc)]; + + +structure CombineNumeralsData = + struct + val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) + val dest_sum = dest_Sucs_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val left_distrib = left_add_mult_distrib RS trans + val prove_conv = prove_conv "nat_combine_numerals" + val trans_tac = trans_tac + val norm_tac = ALLGOALS + (simp_tac (HOL_ss addsimps add_0s@mult_1s@ + [add_0, Suc_eq_add_numeral_1]@add_ac)) + THEN ALLGOALS (simp_tac + (HOL_ss addsimps bin_simps@add_ac@mult_ac)) + val numeral_simp_tac = ALLGOALS + (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) + val simplify_meta_eq = simplify_meta_eq + end; + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); + +val combine_numerals = + prep_simproc ("nat_combine_numerals", + prep_pats ["(i::nat) + j", "Suc (i + j)"], + CombineNumerals.proc); + +end; + + +Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; +Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; + + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +(*cancel_numerals*) +test "l +( #2) + (#2) + #2 + (l + #2) + (oo + #2) = (uu::nat)"; +test "(#2*length xs < #2*length xs + j)"; +test "(#2*length xs < length xs * #2 + j)"; +test "#2*u = (u::nat)"; +test "#2*u = Suc (u)"; +test "(i + j + #12 + (k::nat)) - #15 = y"; +test "(i + j + #12 + (k::nat)) - #5 = y"; +test "Suc u - #2 = y"; +test "Suc (Suc (Suc u)) - #2 = y"; +test "(i + j + #2 + (k::nat)) - 1 = y"; +test "(i + j + #1 + (k::nat)) - 2 = y"; + +test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)"; +test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)"; +test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)"; +test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w"; +test "Suc ((u*v)*#4) - v*#3*u = w"; +test "Suc (Suc ((u*v)*#3)) - v*#3*u = w"; + +test "(i + j + #12 + (k::nat)) = u + #15 + y"; +test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz"; +test "(i + j + #12 + (k::nat)) = u + #5 + y"; +(*Suc*) +test "(i + j + #12 + k) = Suc (u + y)"; +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)"; +test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v"; +test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; +test "#2*y + #3*z + #2*u = Suc (u)"; +test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)"; +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::nat)"; +test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)"; +test "(#2*n*m) < (#3*(m*n)) + (u::nat)"; + +(*negative numerals: FAIL*) +test "(i + j + #-23 + (k::nat)) < u + #15 + y"; +test "(i + j + #3 + (k::nat)) < u + #-15 + y"; +test "(i + j + #-12 + (k::nat)) - #15 = y"; +test "(i + j + #12 + (k::nat)) - #-15 = y"; +test "(i + j + #-12 + (k::nat)) - #-15 = y"; + +(*combine_numerals*) +test "k + #3*k = (u::nat)"; +test "Suc (i + #3) = u"; +test "Suc (i + j + #3 + k) = u"; +test "k + j + #3*k + j = (u::nat)"; +test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)"; +test "(#2*n*m) + (#3*(m*n)) = (u::nat)"; +(*negative numerals: FAIL*) +test "Suc (i + j + #-3 + k) = u"; +*) + + +(*** Prepare linear arithmetic for nat numerals ***) + +local + +(* reduce contradictory <= to False *) +val add_rules = + [add_nat_number_of, diff_nat_number_of, mult_nat_number_of, + eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, + le_Suc_number_of,le_number_of_Suc, + less_Suc_number_of,less_number_of_Suc, + Suc_eq_number_of,eq_number_of_Suc, + eq_number_of_0, eq_0_number_of, less_0_number_of, + nat_number_of, Let_number_of, if_True, if_False]; + +val simprocs = [Nat_Times_Assoc.conv, + Nat_Numeral_Simprocs.combine_numerals]@ + Nat_Numeral_Simprocs.cancel_numerals; + +in + +val nat_simprocs_setup = + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} => + {add_mono_thms = add_mono_thms, lessD = lessD, + simpset = simpset addsimps add_rules + addsimps basic_renamed_arith_simps + addsimprocs simprocs})]; + +end; diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/IsaMakefile Tue Jul 25 00:06:46 2000 +0200 @@ -8,10 +8,11 @@ default: HOL images: HOL HOL-Real TLA -test: HOL-Subst HOL-Induct HOL-IMP HOL-IMPP HOL-Hoare HOL-Lex HOL-Algebra \ - HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML \ - HOL-BCV HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \ - HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \ +test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \ + HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth HOL-UNITY HOL-Modelcheck \ + HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \ + HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \ + HOL-AxClasses-Tutorial HOL-Quot HOL-Real-ex \ HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory all: images test @@ -31,44 +32,43 @@ Pure: @cd $(SRC)/Pure; $(ISATOOL) make Pure -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \ - $(SRC)/Provers/Arith/cancel_sums.ML \ - $(SRC)/Provers/Arith/assoc_fold.ML \ - $(SRC)/Provers/Arith/combine_numerals.ML \ - $(SRC)/Provers/Arith/cancel_numerals.ML \ - $(SRC)/Provers/Arith/fast_lin_arith.ML \ - $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \ - $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ - $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \ - $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \ - $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \ - $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \ - $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \ - $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \ - $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \ - Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \ - Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \ - HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \ - Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \ - Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \ - Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \ - Integ/NatSimprocs.thy Integ/NatSimprocs.ML \ - Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \ - Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \ - Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \ - Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \ - Relation.ML Relation.thy Set.ML Set.thy SetInterval.ML SetInterval.thy \ - String.thy SVC_Oracle.ML \ - SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \ - Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \ - Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \ - Tools/induct_method.ML Tools/inductive_package.ML \ - Tools/numeral_syntax.ML Tools/primrec_package.ML \ - Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \ - Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \ - Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \ - cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \ - simpdata.ML subset.ML subset.thy thy_syntax.ML +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \ + $(SRC)/Provers/Arith/cancel_sums.ML \ + $(SRC)/Provers/Arith/assoc_fold.ML \ + $(SRC)/Provers/Arith/combine_numerals.ML \ + $(SRC)/Provers/Arith/cancel_numerals.ML \ + $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \ + $(SRC)/Provers/make_elim.ML $(SRC)/Provers/clasimp.ML \ + $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \ + $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML \ + $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \ + $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig \ + $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \ + $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \ + $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \ + Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML \ + Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \ + HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \ + Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \ + Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \ + Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \ + Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML \ + Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML \ + Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \ + Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML \ + Ord.thy Power.ML Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML \ + Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML Relation.thy \ + Set.ML Set.thy SetInterval.ML SetInterval.thy String.thy \ + SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \ + Tools/datatype_abs_proofs.ML Tools/datatype_package.ML Tools/datatype_prop.ML \ + Tools/datatype_rep_proofs.ML Tools/induct_method.ML \ + Tools/inductive_package.ML Tools/numeral_syntax.ML \ + Tools/primrec_package.ML Tools/recdef_package.ML \ + Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \ + Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \ + WF.thy WF_Rel.ML WF_Rel.thy arith_data.ML blastdata.ML cladata.ML \ + equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \ + subset.ML subset.thy thy_syntax.ML @$(ISATOOL) usedir -b $(OUT)/Pure HOL @@ -76,16 +76,17 @@ HOL-Real: HOL $(OUT)/HOL-Real -$(OUT)/HOL-Real: $(OUT)/HOL Real/Lubs.ML Real/Lubs.thy Real/PNat.ML \ - Real/PNat.thy Real/PRat.ML Real/PRat.thy Real/PReal.ML \ - Real/PReal.thy Real/RComplete.ML Real/RComplete.thy Real/Real.thy \ - Real/RealDef.ML Real/RealDef.thy Real/RealOrd.ML Real/RealOrd.thy \ - Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \ - Real/RealBin.ML Real/RealBin.thy Real/RealInt.ML Real/RealInt.thy \ - Real/RealPow.ML Real/RealPow.thy Real/Hyperreal/Filter.ML \ - Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \ - Real/Hyperreal/HyperDef.ML Real/Hyperreal/HyperDef.thy \ - Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy +$(OUT)/HOL-Real: $(OUT)/HOL Real/Hyperreal/Filter.ML \ + Real/Hyperreal/Filter.thy Real/Hyperreal/HyperDef.ML \ + Real/Hyperreal/HyperDef.thy Real/Hyperreal/Zorn.ML \ + Real/Hyperreal/Zorn.thy Real/Hyperreal/fuf.ML Real/Lubs.ML \ + Real/Lubs.thy Real/PNat.ML Real/PNat.thy Real/PRat.ML Real/PRat.thy \ + Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \ + Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy \ + Real/RealArith.ML Real/RealArith.thy Real/RealBin.ML \ + Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \ + Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML \ + Real/RealPow.thy Real/real_arith.ML @cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Nat.ML Tue Jul 25 00:06:46 2000 +0200 @@ -1,7 +1,9 @@ (* Title: HOL/Nat.ML ID: $Id$ - Author: Tobias Nipkow - Copyright 1997 TU Muenchen + Author: Lawrence C Paulson and Tobias Nipkow + +Proofs about natural numbers and elementary arithmetic: addition, +multiplication, etc. Some from the Hoare example from Norbert Galm. *) (** conversion rules for nat_rec **) @@ -128,3 +130,606 @@ qed "max_Suc_Suc"; Addsimps [max_0L,max_0R,max_Suc_Suc]; + + +(*** Basic rewrite rules for the arithmetic operators ***) + +(** Difference **) + +Goal "0 - n = (0::nat)"; +by (induct_tac "n" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_0_eq_0"; + +(*Must simplify BEFORE the induction! (Else we get a critical pair) + Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *) +Goal "Suc(m) - Suc(n) = m - n"; +by (Simp_tac 1); +by (induct_tac "n" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_Suc_Suc"; + +Addsimps [diff_0_eq_0, diff_Suc_Suc]; + +(* Could be (and is, below) generalized in various ways; + However, none of the generalizations are currently in the simpset, + and I dread to think what happens if I put them in *) +Goal "0 < n ==> Suc(n-1) = n"; +by (asm_simp_tac (simpset() addsplits [nat.split]) 1); +qed "Suc_pred"; +Addsimps [Suc_pred]; + +Delsimps [diff_Suc]; + + +(**** Inductive properties of the operators ****) + +(*** Addition ***) + +Goal "m + 0 = (m::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_0_right"; + +Goal "m + Suc(n) = Suc(m+n)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_Suc_right"; + +Addsimps [add_0_right,add_Suc_right]; + + +(*Associative law for addition*) +Goal "(m + n) + k = m + ((n + k)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_assoc"; + +(*Commutative law for addition*) +Goal "m + n = n + (m::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_commute"; + +Goal "x+(y+z)=y+((x+z)::nat)"; +by (rtac (add_commute RS trans) 1); +by (rtac (add_assoc RS trans) 1); +by (rtac (add_commute RS arg_cong) 1); +qed "add_left_commute"; + +(*Addition is an AC-operator*) +bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]); + +Goal "(k + m = k + n) = (m=(n::nat))"; +by (induct_tac "k" 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +qed "add_left_cancel"; + +Goal "(m + k = n + k) = (m=(n::nat))"; +by (induct_tac "k" 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +qed "add_right_cancel"; + +Goal "(k + m <= k + n) = (m<=(n::nat))"; +by (induct_tac "k" 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +qed "add_left_cancel_le"; + +Goal "(k + m < k + n) = (m<(n::nat))"; +by (induct_tac "k" 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +qed "add_left_cancel_less"; + +Addsimps [add_left_cancel, add_right_cancel, + add_left_cancel_le, add_left_cancel_less]; + +(** Reasoning about m+0=0, etc. **) + +Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)"; +by (case_tac "m" 1); +by (Auto_tac); +qed "add_is_0"; +AddIffs [add_is_0]; + +Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)"; +by (case_tac "m" 1); +by (Auto_tac); +qed "zero_is_add"; +AddIffs [zero_is_add]; + +Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)"; +by (case_tac "m" 1); +by (Auto_tac); +qed "add_is_1"; + +Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)"; +by (case_tac "m" 1); +by (Auto_tac); +qed "one_is_add"; + +Goal "!!m::nat. (0 m+(n-(Suc k)) = (m+n)-(Suc k)" *) +Goal "!!m::nat. 0 m + (n-1) = (m+n)-1"; +by (case_tac "m" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n] + addsplits [nat.split]))); +qed "add_pred"; +Addsimps [add_pred]; + +Goal "!!m::nat. m + n = m ==> n = 0"; +by (dtac (add_0_right RS ssubst) 1); +by (asm_full_simp_tac (simpset() addsimps [add_assoc] + delsimps [add_0_right]) 1); +qed "add_eq_self_zero"; + + +(**** Additional theorems about "less than" ****) + +(*Deleted less_natE; instead use less_eq_Suc_add RS exE*) +Goal "m (EX k. n=Suc(m+k))"; +by (induct_tac "n" 1); +by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less]))); +by (blast_tac (claset() addSEs [less_SucE] + addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); +qed_spec_mp "less_eq_Suc_add"; + +Goal "n <= ((m + n)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Simp_tac); +by (etac le_SucI 1); +qed "le_add2"; + +Goal "n <= ((n + m)::nat)"; +by (simp_tac (simpset() addsimps add_ac) 1); +by (rtac le_add2 1); +qed "le_add1"; + +bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); +bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); + +Goal "(m i <= j+m"*) +bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); + +(*"i <= j ==> i <= m+j"*) +bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans)); + +(*"i < j ==> i < j+m"*) +bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans)); + +(*"i < j ==> i < m+j"*) +bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans)); + +Goal "i+j < (k::nat) --> i m<=(n::nat)"; +by (induct_tac "k" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps))); +qed_spec_mp "add_leD1"; + +Goal "m+k<=n ==> k<=(n::nat)"; +by (full_simp_tac (simpset() addsimps [add_commute]) 1); +by (etac add_leD1 1); +qed_spec_mp "add_leD2"; + +Goal "m+k<=n ==> m<=n & k<=(n::nat)"; +by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1); +bind_thm ("add_leE", result() RS conjE); + +(*needs !!k for add_ac to work*) +Goal "!!k:: nat. [| k m i + k < j + (k::nat)"; +by (induct_tac "k" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_less_mono1"; + +(*strict, in both arguments*) +Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)"; +by (rtac (add_less_mono1 RS less_trans) 1); +by (REPEAT (assume_tac 1)); +by (induct_tac "j" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_less_mono"; + +(*A [clumsy] way of lifting < monotonicity to <= monotonicity *) +val [lt_mono,le] = Goal + "[| !!i j::nat. i f(i) < f(j); \ +\ i <= j \ +\ |] ==> f(i) <= (f(j)::nat)"; +by (cut_facts_tac [le] 1); +by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1); +by (blast_tac (claset() addSIs [lt_mono]) 1); +qed "less_mono_imp_le_mono"; + +(*non-strict, in 1st argument*) +Goal "i<=j ==> i + k <= j + (k::nat)"; +by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1); +by (etac add_less_mono1 1); +by (assume_tac 1); +qed "add_le_mono1"; + +(*non-strict, in both arguments*) +Goal "[|i<=j; k<=l |] ==> i + k <= j + (l::nat)"; +by (etac (add_le_mono1 RS le_trans) 1); +by (simp_tac (simpset() addsimps [add_commute]) 1); +qed "add_le_mono"; + + +(*** Multiplication ***) + +(*right annihilation in product*) +Goal "!!m::nat. m * 0 = 0"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "mult_0_right"; + +(*right successor law for multiplication*) +Goal "m * Suc(n) = m + (m * n)"; +by (induct_tac "m" 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); +qed "mult_Suc_right"; + +Addsimps [mult_0_right, mult_Suc_right]; + +Goal "1 * n = n"; +by (Asm_simp_tac 1); +qed "mult_1"; + +Goal "n * 1 = n"; +by (Asm_simp_tac 1); +qed "mult_1_right"; + +(*Commutative law for multiplication*) +Goal "m * n = n * (m::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "mult_commute"; + +(*addition distributes over multiplication*) +Goal "(m + n)*k = (m*k) + ((n*k)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); +qed "add_mult_distrib"; + +Goal "k*(m + n) = (k*m) + ((k*n)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); +qed "add_mult_distrib2"; + +(*Associative law for multiplication*) +Goal "(m * n) * k = m * ((n * k)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))); +qed "mult_assoc"; + +Goal "x*(y*z) = y*((x*z)::nat)"; +by (rtac trans 1); +by (rtac mult_commute 1); +by (rtac trans 1); +by (rtac mult_assoc 1); +by (rtac (mult_commute RS arg_cong) 1); +qed "mult_left_commute"; + +bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]); + +Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)"; +by (induct_tac "m" 1); +by (induct_tac "n" 2); +by (ALLGOALS Asm_simp_tac); +qed "mult_is_0"; + +Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)"; +by (stac eq_commute 1 THEN stac mult_is_0 1); +by Auto_tac; +qed "zero_is_mult"; + +Addsimps [mult_is_0, zero_is_mult]; + + +(*** Difference ***) + +Goal "!!m::nat. m - m = 0"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_self_eq_0"; + +Addsimps [diff_self_eq_0]; + +(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) +Goal "~ m n+(m-n) = (m::nat)"; +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); +by (ALLGOALS Asm_simp_tac); +qed_spec_mp "add_diff_inverse"; + +Goal "n<=m ==> n+(m-n) = (m::nat)"; +by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1); +qed "le_add_diff_inverse"; + +Goal "n<=m ==> (m-n)+n = (m::nat)"; +by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1); +qed "le_add_diff_inverse2"; + +Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; + + +(*** More results about difference ***) + +Goal "n <= m ==> Suc(m)-n = Suc(m-n)"; +by (etac rev_mp 1); +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); +by (ALLGOALS Asm_simp_tac); +qed "Suc_diff_le"; + +Goal "m - n < Suc(m)"; +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); +by (etac less_SucE 3); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); +qed "diff_less_Suc"; + +Goal "m - n <= (m::nat)"; +by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI]))); +qed "diff_le_self"; +Addsimps [diff_le_self]; + +(* j j-n < k *) +bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans); + +Goal "!!i::nat. i-j-k = i - (j+k)"; +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_diff_left"; + +Goal "(Suc m - n) - Suc k = m - n - k"; +by (simp_tac (simpset() addsimps [diff_diff_left]) 1); +qed "Suc_diff_diff"; +Addsimps [Suc_diff_diff]; + +Goal "0 n - Suc i < n"; +by (case_tac "n" 1); +by Safe_tac; +by (asm_simp_tac (simpset() addsimps le_simps) 1); +qed "diff_Suc_less"; +Addsimps [diff_Suc_less]; + +(*This and the next few suggested by Florian Kammueller*) +Goal "!!i::nat. i-j-k = i-k-j"; +by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1); +qed "diff_commute"; + +Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)"; +by (res_inst_tac [("m","j"),("n","k")] diff_induct 1); +by (ALLGOALS Asm_simp_tac); +qed_spec_mp "diff_add_assoc"; + +Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i"; +by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1); +qed_spec_mp "diff_add_assoc2"; + +Goal "(n+m) - n = (m::nat)"; +by (induct_tac "n" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_add_inverse"; + +Goal "(m+n) - n = (m::nat)"; +by (simp_tac (simpset() addsimps [diff_add_assoc]) 1); +qed "diff_add_inverse2"; + +Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)"; +by Safe_tac; +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2]))); +qed "le_imp_diff_is_add"; + +Goal "!!m::nat. (m-n = 0) = (m <= n)"; +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_is_0_eq"; + +Goal "!!m::nat. (0 = m-n) = (m <= n)"; +by (stac (diff_is_0_eq RS sym) 1); +by (rtac eq_sym_conv 1); +qed "zero_is_diff_eq"; +Addsimps [diff_is_0_eq, zero_is_diff_eq]; + +Goal "!!m::nat. (0 EX k::nat. 0 (ALL n. P(Suc(n))--> P(n)) --> P(k-i)"; +by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); +by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac)); +qed "zero_induct_lemma"; + +val prems = Goal "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)"; +by (rtac (diff_self_eq_0 RS subst) 1); +by (rtac (zero_induct_lemma RS mp RS mp) 1); +by (REPEAT (ares_tac ([impI,allI]@prems) 1)); +qed "zero_induct"; + +Goal "(k+m) - (k+n) = m - (n::nat)"; +by (induct_tac "k" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_cancel"; + +Goal "(m+k) - (n+k) = m - (n::nat)"; +by (asm_simp_tac + (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1); +qed "diff_cancel2"; + +Goal "n - (n+m) = (0::nat)"; +by (induct_tac "n" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_add_0"; + + +(** Difference distributes over multiplication **) + +Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)"; +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel]))); +qed "diff_mult_distrib" ; + +Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)"; +val mult_commute_k = read_instantiate [("m","k")] mult_commute; +by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1); +qed "diff_mult_distrib2" ; +(*NOT added as rewrites, since sometimes they are used from right-to-left*) + + +(*** Monotonicity of Multiplication ***) + +Goal "i <= (j::nat) ==> i*k<=j*k"; +by (induct_tac "k" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); +qed "mult_le_mono1"; + +Goal "i <= (j::nat) ==> k*i <= k*j"; +by (dtac mult_le_mono1 1); +by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); +qed "mult_le_mono2"; + +(* <= monotonicity, BOTH arguments*) +Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l"; +by (etac (mult_le_mono1 RS le_trans) 1); +by (etac mult_le_mono2 1); +qed "mult_le_mono"; + +(*strict, in 1st argument; proof is by induction on k>0*) +Goal "!!i::nat. [| i k*i < k*j"; +by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1); +by (Asm_simp_tac 1); +by (induct_tac "x" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); +qed "mult_less_mono2"; + +Goal "!!i::nat. [| i i*k < j*k"; +by (dtac mult_less_mono2 1); +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute]))); +qed "mult_less_mono1"; + +Goal "!!m::nat. (0 < m*n) = (0 (m*k < n*k) = (m (k*m < k*n) = (m (m*k <= n*k) = (m<=n)"; +by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); +qed "mult_le_cancel2"; + +Goal "!!m::nat. 0 (k*m <= k*n) = (m<=n)"; +by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); +qed "mult_le_cancel1"; +Addsimps [mult_le_cancel1, mult_le_cancel2]; + +Goal "(Suc k * m < Suc k * n) = (m < n)"; +by (rtac mult_less_cancel1 1); +by (Simp_tac 1); +qed "Suc_mult_less_cancel1"; + +Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)"; +by (simp_tac (simpset_of HOL.thy) 1); +by (rtac Suc_mult_less_cancel1 1); +qed "Suc_mult_le_cancel1"; + +Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)"; +by (cut_facts_tac [less_linear] 1); +by Safe_tac; +by (assume_tac 2); +by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac)); +by (ALLGOALS Asm_full_simp_tac); +qed "mult_cancel2"; + +Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)"; +by (dtac mult_cancel2 1); +by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); +qed "mult_cancel1"; +Addsimps [mult_cancel1, mult_cancel2]; + +Goal "(Suc k * m = Suc k * n) = (m = n)"; +by (rtac mult_cancel1 1); +by (Simp_tac 1); +qed "Suc_mult_cancel1"; + + +(*Lemma for gcd*) +Goal "!!m::nat. m = m*n ==> n=1 | m=0"; +by (dtac sym 1); +by (rtac disjCI 1); +by (rtac nat_less_cases 1 THEN assume_tac 2); +by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1); +by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1); +qed "mult_eq_self_implies_10"; diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Nat.thy Tue Jul 25 00:06:46 2000 +0200 @@ -1,13 +1,15 @@ (* Title: HOL/Nat.thy ID: $Id$ - Author: Tobias Nipkow - Copyright 1997 TU Muenchen + Author: Tobias Nipkow and Lawrence C Paulson -Type "nat" is a linear order, and a datatype +Type "nat" is a linear order, and a datatype; arithmetic operators + - +and * (for div, mod and dvd, see theory Divides). *) Nat = NatDef + Inductive + +(* type "nat" is a linear order, and a datatype *) + rep_datatype nat distinct Suc_not_Zero, Zero_not_Suc inject Suc_Suc_eq @@ -19,4 +21,25 @@ consts "^" :: ['a::power,nat] => 'a (infixr 80) + +(* arithmetic operators + - and * *) + +instance + nat :: {plus, minus, times, power} + +(* size of a datatype value; overloaded *) +consts size :: 'a => nat + +primrec + add_0 "0 + n = n" + add_Suc "Suc m + n = Suc(m + n)" + +primrec + diff_0 "m - 0 = m" + diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" + +primrec + mult_0 "0 * n = 0" + mult_Suc "Suc m * n = n + (m * n)" + end diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Real/RealArith.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealArith.ML Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,6 @@ + +(*useful??*) +Goal "(z = z + w) = (w = (#0::real))"; +by Auto_tac; +qed "real_add_left_cancel0"; +Addsimps [real_add_left_cancel0]; diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Real/RealArith.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealArith.thy Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,7 @@ + +theory RealArith = RealBin +files "real_arith.ML": + +setup real_arith_setup + +end diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Real/real_arith.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/real_arith.ML Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,109 @@ +(* Title: HOL/Real/real_arith.ML + ID: $Id$ + Author: Tobias Nipkow, TU Muenchen + Copyright 1999 TU Muenchen + +Instantiation of the generic linear arithmetic package for type real. +*) + +local + +(* reduce contradictory <= to False *) +val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1, + add_real_number_of, minus_real_number_of, diff_real_number_of, + mult_real_number_of, eq_real_number_of, less_real_number_of, + le_real_number_of_eq_not_less, real_diff_def, + real_minus_add_distrib, real_minus_minus]; + +val add_rules = + map rename_numerals + [real_add_zero_left, real_add_zero_right, + real_add_minus, real_add_minus_left, + real_mult_0, real_mult_0_right, + real_mult_1, real_mult_1_right, + real_mult_minus_1, real_mult_minus_1_right]; + +val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ + Real_Numeral_Simprocs.cancel_numerals; + +val mono_ss = simpset() addsimps + [real_add_le_mono,real_add_less_mono, + real_add_less_le_mono,real_add_le_less_mono]; + +val add_mono_thms_real = + map (fn s => prove_goal (the_context ()) s + (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) + ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)", + "(i = j) & (k <= l) ==> i + k <= j + (l::real)", + "(i <= j) & (k = l) ==> i + k <= j + (l::real)", + "(i = j) & (k = l) ==> i + k = j + (l::real)", + "(i < j) & (k = l) ==> i + k < j + (l::real)", + "(i = j) & (k < l) ==> i + k < j + (l::real)", + "(i < j) & (k <= l) ==> i + k < j + (l::real)", + "(i <= j) & (k < l) ==> i + k < j + (l::real)", + "(i < j) & (k < l) ==> i + k < j + (l::real)"]; + +val real_arith_simproc_pats = + map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT)) + ["(m::real) < n","(m::real) <= n", "(m::real) = n"]; + +in + +val fast_real_arith_simproc = mk_simproc + "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover; + +val real_arith_setup = + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} => + {add_mono_thms = add_mono_thms @ add_mono_thms_real, + lessD = lessD, (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*) + simpset = simpset addsimps simps@add_rules + addsimprocs simprocs + addcongs [if_weak_cong]}), + arith_discrete ("RealDef.real",false), + Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]]; + +end; + + +(* Some test data [omitting examples that assume the ordering to be discrete!] +Goal "!!a::real. [| a <= b; c <= d; x+y a+c <= b+d"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; +by (arith_tac 1); +qed ""; + +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a <= l"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a+a+a+a <= l+l+l+l"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a+a+a+a+a <= l+l+l+l+i"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; +by (fast_arith_tac 1); +qed ""; + +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ +\ ==> #6*a <= #5*l+i"; +by (fast_arith_tac 1); +qed ""; +*) diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Univ.thy --- a/src/HOL/Univ.thy Tue Jul 25 00:03:39 2000 +0200 +++ b/src/HOL/Univ.thy Tue Jul 25 00:06:46 2000 +0200 @@ -11,8 +11,6 @@ Univ = Arith + Sum + -setup arith_setup - (** lists, trees will be sets of nodes **) diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/arith_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/arith_data.ML Tue Jul 25 00:06:46 2000 +0200 @@ -0,0 +1,429 @@ +(* Title: HOL/arith_data.ML + ID: $Id$ + Author: Markus Wenzel, Stefan Berghofer and Tobias Nipkow + +Various arithmetic proof procedures. +*) + +(*---------------------------------------------------------------------------*) +(* 1. Cancellation of common terms *) +(*---------------------------------------------------------------------------*) + +signature ARITH_DATA = +sig + val nat_cancel_sums_add: simproc list + val nat_cancel_sums: simproc list + val nat_cancel_factor: simproc list + val nat_cancel: simproc list +end; + +structure ArithData: ARITH_DATA = +struct + + +(** abstract syntax of structure nat: 0, Suc, + **) + +(* mk_sum, mk_norm_sum *) + +val one = HOLogic.mk_nat 1; +val mk_plus = HOLogic.mk_binop "op +"; + +fun mk_sum [] = HOLogic.zero + | mk_sum [t] = t + | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) +fun mk_norm_sum ts = + let val (ones, sums) = partition (equal one) ts in + funpow (length ones) HOLogic.mk_Suc (mk_sum sums) + end; + + +(* dest_sum *) + +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; + +fun dest_sum tm = + if HOLogic.is_zero tm then [] + else + (case try HOLogic.dest_Suc tm of + Some t => one :: dest_sum t + | None => + (case try dest_plus tm of + Some (t, u) => dest_sum t @ dest_sum u + | None => [tm])); + + +(** generic proof tools **) + +(* prove conversions *) + +val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; + +fun prove_conv expand_tac norm_tac sg (t, u) = + mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u))) + (K [expand_tac, norm_tac])) + handle ERROR => error ("The error(s) above occurred while trying to prove " ^ + (string_of_cterm (cterm_of sg (mk_eqv (t, u))))); + +val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s" + (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); + + +(* rewriting *) + +fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules)); + +val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; +val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; + + + +(** cancel common summands **) + +structure Sum = +struct + val mk_sum = mk_norm_sum; + val dest_sum = dest_sum; + val prove_conv = prove_conv; + val norm_tac = simp_all add_rules THEN simp_all add_ac; +end; + +fun gen_uncancel_tac rule ct = + rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1; + + +(* nat eq *) + +structure EqCancelSums = CancelSumsFun +(struct + open Sum; + val mk_bal = HOLogic.mk_eq; + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; + val uncancel_tac = gen_uncancel_tac add_left_cancel; +end); + + +(* nat less *) + +structure LessCancelSums = CancelSumsFun +(struct + open Sum; + val mk_bal = HOLogic.mk_binrel "op <"; + val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; + val uncancel_tac = gen_uncancel_tac add_left_cancel_less; +end); + + +(* nat le *) + +structure LeCancelSums = CancelSumsFun +(struct + open Sum; + val mk_bal = HOLogic.mk_binrel "op <="; + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; + val uncancel_tac = gen_uncancel_tac add_left_cancel_le; +end); + + +(* nat diff *) + +structure DiffCancelSums = CancelSumsFun +(struct + open Sum; + val mk_bal = HOLogic.mk_binop "op -"; + val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT; + val uncancel_tac = gen_uncancel_tac diff_cancel; +end); + + + +(** cancel common factor **) + +structure Factor = +struct + val mk_sum = mk_norm_sum; + val dest_sum = dest_sum; + val prove_conv = prove_conv; + val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac; +end; + +fun mk_cnat n = cterm_of (Theory.sign_of (the_context ())) (HOLogic.mk_nat n); + +fun gen_multiply_tac rule k = + if k > 0 then + rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1 + else no_tac; + + +(* nat eq *) + +structure EqCancelFactor = CancelFactorFun +(struct + open Factor; + val mk_bal = HOLogic.mk_eq; + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; + val multiply_tac = gen_multiply_tac Suc_mult_cancel1; +end); + + +(* nat less *) + +structure LessCancelFactor = CancelFactorFun +(struct + open Factor; + val mk_bal = HOLogic.mk_binrel "op <"; + val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; + val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1; +end); + + +(* nat le *) + +structure LeCancelFactor = CancelFactorFun +(struct + open Factor; + val mk_bal = HOLogic.mk_binrel "op <="; + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; + val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1; +end); + + + +(** prepare nat_cancel simprocs **) + +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT); +val prep_pats = map prep_pat; + +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; + +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]; +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]; +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]; +val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]; + +val nat_cancel_sums_add = map prep_simproc + [("nateq_cancel_sums", eq_pats, EqCancelSums.proc), + ("natless_cancel_sums", less_pats, LessCancelSums.proc), + ("natle_cancel_sums", le_pats, LeCancelSums.proc)]; + +val nat_cancel_sums = nat_cancel_sums_add @ + [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)]; + +val nat_cancel_factor = map prep_simproc + [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc), + ("natless_cancel_factor", less_pats, LessCancelFactor.proc), + ("natle_cancel_factor", le_pats, LeCancelFactor.proc)]; + +val nat_cancel = nat_cancel_factor @ nat_cancel_sums; + + +end; + +open ArithData; + + +(*---------------------------------------------------------------------------*) +(* 2. Linear arithmetic *) +(*---------------------------------------------------------------------------*) + +(* Parameters data for general linear arithmetic functor *) + +structure LA_Logic: LIN_ARITH_LOGIC = +struct +val ccontr = ccontr; +val conjI = conjI; +val neqE = linorder_neqE; +val notI = notI; +val sym = sym; +val not_lessD = linorder_not_less RS iffD1; +val not_leD = linorder_not_le RS iffD1; + + +fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); + +val mk_Trueprop = HOLogic.mk_Trueprop; + +fun neg_prop(TP$(Const("Not",_)$t)) = TP$t + | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t); + +fun is_False thm = + let val _ $ t = #prop(rep_thm thm) + in t = Const("False",HOLogic.boolT) end; + +fun is_nat(t) = fastype_of1 t = HOLogic.natT; + +fun mk_nat_thm sg t = + let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) + in instantiate ([],[(cn,ct)]) le0 end; + +end; + + +(* arith theory data *) + +structure ArithDataArgs = +struct + val name = "HOL/arith"; + type T = {splits: thm list, discrete: (string * bool) list}; + + val empty = {splits = [], discrete = []}; + val copy = I; + val prep_ext = I; + fun merge ({splits = splits1, discrete = discrete1}, {splits = splits2, discrete = discrete2}) = + {splits = Drule.merge_rules (splits1, splits2), + discrete = merge_alists discrete1 discrete2}; + fun print _ _ = (); +end; + +structure ArithData = TheoryDataFun(ArithDataArgs); + +fun arith_split_add (thy, thm) = (ArithData.map (fn {splits, discrete} => + {splits = thm :: splits, discrete = discrete}) thy, thm); + +fun arith_discrete d = ArithData.map (fn {splits, discrete} => + {splits = splits, discrete = d :: discrete}); + + +structure LA_Data_Ref: LIN_ARITH_DATA = +struct + +(* Decomposition of terms *) + +fun nT (Type("fun",[N,_])) = N = HOLogic.natT + | nT _ = false; + +fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) + | Some n => (overwrite(p,(t,n+m:int)), i)); + +(* Turn term into list of summand * multiplicity plus a constant *) +fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) + | poly(all as Const("op -",T) $ s $ t, m, pi) = + if nT T then add_atom(all,m,pi) + else poly(s,m,poly(t,~1*m,pi)) + | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) + | poly(Const("0",_), _, pi) = pi + | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m)) + | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)= + (poly(t,m*HOLogic.dest_binum c,pi) + handle TERM _ => add_atom(all,m,pi)) + | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)= + (poly(t,m*HOLogic.dest_binum c,pi) + handle TERM _ => add_atom(all,m,pi)) + | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) = + ((p,i + m*HOLogic.dest_binum t) + handle TERM _ => add_atom(all,m,(p,i))) + | poly x = add_atom x; + +fun decomp2(rel,lhs,rhs) = + let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) + in case rel of + "op <" => Some(p,i,"<",q,j) + | "op <=" => Some(p,i,"<=",q,j) + | "op =" => Some(p,i,"=",q,j) + | _ => None + end; + +fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d) + | negate None = None; + +fun decomp1 discrete (T,xxx) = + (case T of + Type("fun",[Type(D,[]),_]) => + (case assoc(discrete,D) of + None => None + | Some d => (case decomp2 xxx of + None => None + | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d))) + | _ => None); + +fun decomp2 discrete (_$(Const(rel,T)$lhs$rhs)) = decomp1 discrete (T,(rel,lhs,rhs)) + | decomp2 discrete (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = + negate(decomp1 discrete (T,(rel,lhs,rhs))) + | decomp2 discrete _ = None + +val decomp = decomp2 o #discrete o ArithData.get_sg; + +end; + + +structure Fast_Arith = + Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); + +val fast_arith_tac = Fast_Arith.lin_arith_tac +and trace_arith = Fast_Arith.trace; + +local + +(* reduce contradictory <= to False. + Most of the work is done by the cancel tactics. +*) +val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq]; + +val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s + (fn prems => [cut_facts_tac prems 1, + blast_tac (claset() addIs [add_le_mono]) 1])) +["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)", + "(i = j) & (k <= l) ==> i + k <= j + (l::nat)", + "(i <= j) & (k = l) ==> i + k <= j + (l::nat)", + "(i = j) & (k = l) ==> i + k = j + (l::nat)" +]; + +in + +val init_lin_arith_data = + Fast_Arith.setup @ + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset = _} => + {add_mono_thms = add_mono_thms @ add_mono_thms_nat, + lessD = lessD @ [Suc_leI], + simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}), + ArithData.init, arith_discrete ("nat", true)]; + +end; + + +local +val nat_arith_simproc_pats = + map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT)) + ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]; +in +val fast_nat_arith_simproc = mk_simproc + "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover; +end; + +(* Because of fast_nat_arith_simproc, the arithmetic solver is really only +useful to detect inconsistencies among the premises for subgoals which are +*not* themselves (in)equalities, because the latter activate +fast_nat_arith_simproc anyway. However, it seems cheaper to activate the +solver all the time rather than add the additional check. *) + + +(* arith proof method *) + +(* FIXME: K true should be replaced by a sensible test to speed things up + in case there are lots of irrelevant terms involved; + elimination of min/max can be optimized: + (max m n + k <= r) = (m+k <= r & n+k <= r) + (l <= min m n + k) = (l <= m+k & l <= n+k) +*) +fun arith_tac i st = + refute_tac (K true) (REPEAT o split_tac (#splits (ArithData.get_sg (Thm.sign_of_thm st)))) + ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st; + +fun arith_method prems = + Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); + + +(* theory setup *) + +val arith_setup = + [Simplifier.change_simpset_of (op addsimprocs) nat_cancel] @ + init_lin_arith_data @ + [Simplifier.change_simpset_of (op addSolver) + (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac), + Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc], + Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts, + "decide linear arithmethic")], + Attrib.add_attributes [("arith_split", + (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute), + "declare split rules for arithmetic procedure")]];