--- 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) = (0<m | 0<n)";
-by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
-qed "add_gr_0";
-AddIffs [add_gr_0];
-
-(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
-Goal "!!m::nat. 0<n ==> 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<n --> (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<n) = (EX k. n=Suc(m+k))";
-by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
-qed "less_iff_Suc_add";
-
-
-(*"i <= j ==> 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<k";
-by (induct_tac "j" 1);
-by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addDs [Suc_lessD]) 1);
-qed_spec_mp "add_lessD1";
-
-Goal "~ (i+j < (i::nat))";
-by (rtac notI 1);
-by (etac (add_lessD1 RS less_irrefl) 1);
-qed "not_add_less1";
-
-Goal "~ (j+i < (i::nat))";
-by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
-qed "not_add_less2";
-AddIffs [not_add_less1, not_add_less2];
-
-Goal "m+k<=n --> 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<l; m+l = k+n |] ==> m<n";
-by (force_tac (claset(),
- simpset() delsimps [add_Suc_right]
- addsimps [less_iff_Suc_add,
- add_Suc_right RS sym] @ add_ac) 1);
-qed "less_add_eq_less";
-
-
-(*** Monotonicity of Addition ***)
-
-(*strict, in 1st argument*)
-Goal "i < j ==> 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<j ==> 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 --> 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<k ==> 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 ==> 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<n-m) = (m<n)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "zero_less_diff";
-Addsimps [zero_less_diff];
-
-Goal "i < j ==> EX k::nat. 0<k & i+k = j";
-by (res_inst_tac [("x","j - i")] exI 1);
-by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
-qed "less_imp_add_positive";
-
-Goal "P(k) --> (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<j; 0<k |] ==> 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<j; 0<k |] ==> 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 & 0<n)";
-by (induct_tac "m" 1);
-by (case_tac "n" 2);
-by (ALLGOALS Asm_simp_tac);
-qed "zero_less_mult_iff";
-Addsimps [zero_less_mult_iff];
-
-Goal "(1 <= m*n) = (1<=m & 1<=n)";
-by (induct_tac "m" 1);
-by (case_tac "n" 2);
-by (ALLGOALS Asm_simp_tac);
-qed "one_le_mult_iff";
-Addsimps [one_le_mult_iff];
-
-Goal "(m*n = 1) = (m=1 & n=1)";
-by (induct_tac "m" 1);
-by (Simp_tac 1);
-by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed "mult_eq_1_iff";
-Addsimps [mult_eq_1_iff];
-
-Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
-by (safe_tac (claset() addSIs [mult_less_mono1]));
-by (cut_facts_tac [less_linear] 1);
-by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
-qed "mult_less_cancel2";
-
-Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
-by (dtac mult_less_cancel2 1);
-by (etac subst 1);
-by (simp_tac (simpset() addsimps [mult_commute]) 1);
-qed "mult_less_cancel1";
-Addsimps [mult_less_cancel1, mult_less_cancel2];
-
-Goal "!!m::nat. 0<k ==> (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 ==> (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<b --> 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);
--- 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<b --> 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
--- 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];
--- 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
--- 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<z |] ==> 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<b; i<j |] \
-\ ==> 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<z)";
-by (case_tac "neg z" 1);
-by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
-by (auto_tac (claset() addIs [zless_trans],
- simpset() addsimps [neg_eq_less_0, zle_def]));
-qed "nat_less_eq_zless";
-
-Goal "#0 < w | #0 <= z ==> (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";
-
--- 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
--- 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 **)
--- 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
--- /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<z |] ==> 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<b; i<j |] \
+\ ==> 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);
+*)
--- /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<z)";
+by (case_tac "neg z" 1);
+by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
+by (auto_tac (claset() addIs [zless_trans],
+ simpset() addsimps [neg_eq_less_0, zle_def]));
+qed "nat_less_eq_zless";
+
+Goal "#0 < w | #0 <= z ==> (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 ...*)
--- /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;
--- 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
--- 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) = (0<m | 0<n)";
+by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
+qed "add_gr_0";
+AddIffs [add_gr_0];
+
+(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
+Goal "!!m::nat. 0<n ==> 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<n --> (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<n) = (EX k. n=Suc(m+k))";
+by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
+qed "less_iff_Suc_add";
+
+
+(*"i <= j ==> 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<k";
+by (induct_tac "j" 1);
+by (ALLGOALS Asm_simp_tac);
+by (blast_tac (claset() addDs [Suc_lessD]) 1);
+qed_spec_mp "add_lessD1";
+
+Goal "~ (i+j < (i::nat))";
+by (rtac notI 1);
+by (etac (add_lessD1 RS less_irrefl) 1);
+qed "not_add_less1";
+
+Goal "~ (j+i < (i::nat))";
+by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
+qed "not_add_less2";
+AddIffs [not_add_less1, not_add_less2];
+
+Goal "m+k<=n --> 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<l; m+l = k+n |] ==> m<n";
+by (force_tac (claset(),
+ simpset() delsimps [add_Suc_right]
+ addsimps [less_iff_Suc_add,
+ add_Suc_right RS sym] @ add_ac) 1);
+qed "less_add_eq_less";
+
+
+(*** Monotonicity of Addition ***)
+
+(*strict, in 1st argument*)
+Goal "i < j ==> 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<j ==> 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 --> 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<k ==> 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 ==> 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<n-m) = (m<n)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "zero_less_diff";
+Addsimps [zero_less_diff];
+
+Goal "i < j ==> EX k::nat. 0<k & i+k = j";
+by (res_inst_tac [("x","j - i")] exI 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
+qed "less_imp_add_positive";
+
+Goal "P(k) --> (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<j; 0<k |] ==> 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<j; 0<k |] ==> 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 & 0<n)";
+by (induct_tac "m" 1);
+by (case_tac "n" 2);
+by (ALLGOALS Asm_simp_tac);
+qed "zero_less_mult_iff";
+Addsimps [zero_less_mult_iff];
+
+Goal "(1 <= m*n) = (1<=m & 1<=n)";
+by (induct_tac "m" 1);
+by (case_tac "n" 2);
+by (ALLGOALS Asm_simp_tac);
+qed "one_le_mult_iff";
+Addsimps [one_le_mult_iff];
+
+Goal "(m*n = 1) = (m=1 & n=1)";
+by (induct_tac "m" 1);
+by (Simp_tac 1);
+by (induct_tac "n" 1);
+by (Simp_tac 1);
+by (fast_tac (claset() addss simpset()) 1);
+qed "mult_eq_1_iff";
+Addsimps [mult_eq_1_iff];
+
+Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
+by (safe_tac (claset() addSIs [mult_less_mono1]));
+by (cut_facts_tac [less_linear] 1);
+by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
+qed "mult_less_cancel2";
+
+Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
+by (dtac mult_less_cancel2 1);
+by (etac subst 1);
+by (simp_tac (simpset() addsimps [mult_commute]) 1);
+qed "mult_less_cancel1";
+Addsimps [mult_less_cancel1, mult_less_cancel2];
+
+Goal "!!m::nat. 0<k ==> (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 ==> (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";
--- 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
--- /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];
--- /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
--- /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<z |] ==> 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 "";
+*)
--- 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 **)
--- /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")]];