--- a/src/HOL/Integ/IntArith.ML Tue May 02 18:40:16 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML Tue May 02 18:42:48 2000 +0200
@@ -159,9 +159,15 @@
(*To let us treat subtraction as addition*)
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
+val def_trans = def_imp_eq RS trans;
+
+(*Apply the given rewrite (if present) just once*)
+fun subst_tac None = all_tac
+ | subst_tac (Some th) = ALLGOALS (rtac (th RS def_trans));
+
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
-fun prove_conv tacs sg (t, u) =
+fun prove_conv name tacs sg (t, u) =
if t aconv u then None
else
Some
@@ -169,7 +175,8 @@
(K tacs))
handle ERROR => error
("The error(s) above occurred while trying to prove " ^
- (string_of_cterm (cterm_of sg (mk_eqv (t, u))))));
+ string_of_cterm (cterm_of sg (mk_eqv (t, u))) ^
+ "\nInternal failure of simproc " ^ name));
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);
@@ -182,48 +189,50 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- val prove_conv = prove_conv
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@zadd_ac))
+ val subst_tac = subst_tac
+ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+ zadd_ac))
THEN ALLGOALS
- (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@bin_simps@zmult_ac))
+ (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))
end;
-(* int eq *)
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
+ val bal_add1 = eq_add_iff1 RS trans
+ val bal_add2 = eq_add_iff2 RS trans
);
-(* int less *)
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
+ val bal_add1 = less_add_iff1 RS trans
+ val bal_add2 = less_add_iff2 RS trans
);
-(* int le *)
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 bal_add1 = le_add_iff1 RS trans
+ val bal_add2 = le_add_iff2 RS trans
);
-(* int diff *)
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
+ val prove_conv = prove_conv "intdiff_cancel_numerals"
val mk_bal = HOLogic.mk_binop "op -"
val dest_bal = HOLogic.dest_bin "op -" HOLogic.intT
- val bal_add1 = diff_add_eq1 RS trans
- val bal_add2 = diff_add_eq2 RS trans
+ val bal_add1 = diff_add_eq1 RS trans
+ val bal_add2 = diff_add_eq2 RS trans
);
@@ -287,42 +296,6 @@
*)
-
-(****************************************************************************************************************************************************************************************************************************************************************
-
-
-structure Int_CC_Data : COMBINE_COEFF_DATA =
-struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
- val thy = Bin.thy
- val T = HOLogic.intT
-
- val trans = trans
- val add_ac = zadd_ac
- val diff_def = zdiff_def
- val minus_add_distrib = zminus_zadd_distrib
- val minus_minus = zminus_zminus
- val mult_commute = zmult_commute
- val mult_1_right = zmult_1_right
- val add_mult_distrib = zadd_zmult_distrib2
- val diff_mult_distrib = zdiff_zmult_distrib2
- val mult_minus_right = zmult_zminus_right
-
- val rel_iff_rel_0_rls = [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
- zle_iff_zdiff_zle_0]
- fun dest_eqI th =
- #1 (HOLogic.dest_bin "op =" HOLogic.boolT
- (HOLogic.dest_Trueprop (concl_of th)))
-
-end;
-
-structure Int_CC = Combine_Coeff (Int_CC_Data);
-
-Addsimprocs [Int_CC.sum_conv, Int_CC.rel_conv];
-****************************************************************)
-
-
(** Constant folding for integer plus and times **)
(*We do not need
--- a/src/HOL/Integ/NatBin.ML Tue May 02 18:40:16 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML Tue May 02 18:42:48 2000 +0200
@@ -303,12 +303,19 @@
(** Arith **)
-Addsimps (map (rename_numerals thy)
- [diff_0, diff_0_eq_0, add_0, add_0_right, add_pred,
- diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
- mult_0, mult_0_right, mult_1, mult_1_right,
- mult_is_0, zero_is_mult, zero_less_mult_iff,
- mult_eq_1_iff]);
+(*Identity laws for + - * *)
+val basic_renamed_arith_simps =
+ map (rename_numerals thy)
+ [diff_0, diff_0_eq_0, add_0, add_0_right,
+ mult_0, mult_0_right, mult_1, mult_1_right];
+
+(*Non-trivial simplifications*)
+val other_renamed_arith_simps =
+ map (rename_numerals thy)
+ [add_pred, diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
+ mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
+
+Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);
@@ -350,9 +357,7 @@
(** Divides **)
-Addsimps (map (rename_numerals thy)
- [mod_1, mod_0, div_1, div_0, mod2_gr_0, mod2_add_self_eq_0,
- mod2_add_self]);
+Addsimps (map (rename_numerals thy) [mod_1, mod_0, div_1, div_0]);
AddIffs (map (rename_numerals thy)
[dvd_1_left, dvd_0_right]);
@@ -465,4 +470,3 @@
(* Push int(.) inwards: *)
Addsimps [int_Suc,zadd_int RS sym];
-
--- a/src/HOL/Integ/NatSimprocs.ML Tue May 02 18:40:16 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML Tue May 02 18:42:48 2000 +0200
@@ -14,6 +14,13 @@
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)";
@@ -56,6 +63,7 @@
addsimps [add_mult_distrib]));
qed "nat_le_add_iff2";
+
structure Nat_Numeral_Simprocs =
struct
@@ -68,8 +76,9 @@
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)
- | dest_numeral t = raise TERM("dest_numeral", [t]);
+ (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
+ handle Match => raise TERM("dest_numeral:1", [w]))
+ | dest_numeral t = raise TERM("dest_numeral:2", [t]);
fun find_first_numeral past (t::terms) =
((dest_numeral t, t, rev past @ terms)
@@ -84,6 +93,10 @@
| 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*)
@@ -98,60 +111,21 @@
fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
-val mk_diff = HOLogic.mk_binop "op -";
-val dest_diff = HOLogic.dest_bin "op -" HOLogic.natT;
-
-val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+val subst_tac = Int_Numeral_Simprocs.subst_tac;
-fun prove_conv tacs sg (t, u) =
- if t aconv u then None
- else
- Some
- (mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
- (K tacs))
- handle ERROR => error
- ("The error(s) above occurred while trying to prove " ^
- (string_of_cterm (cterm_of sg (mk_eqv (t, u))))));
+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;
-val add_norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_ac));
-
-
-(****combine_coeffs will make this obsolete****)
-structure FoldSucData =
- struct
- val mk_numeral = mk_numeral
- val dest_numeral = dest_numeral
- val find_first_numeral = find_first_numeral []
- val mk_sum = mk_sum
- val dest_sum = dest_Sucs_sum
- val mk_diff = HOLogic.mk_binop "op -"
- val dest_diff = HOLogic.dest_bin "op -" HOLogic.natT
- val dest_Suc = HOLogic.dest_Suc
- val double_diff_eq = diff_add_assoc_diff
- val move_diff_eq = diff_add_assoc2
- val prove_conv = prove_conv
- val numeral_simp_tac = ALLGOALS
- (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@bin_simps))
- val add_norm_tac = ALLGOALS (simp_tac (simpset() addsimps Suc_eq_add_numeral_1::add_ac))
- end;
-
-structure FoldSuc = FoldSucFun (FoldSucData);
-
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;
-val fold_Suc =
- prep_simproc ("fold_Suc",
- [prep_pat "Suc (i + j)"],
- FoldSuc.proc);
-(*** Now for CancelNumerals ***)
+(*** CancelNumerals simprocs ***)
val one = mk_numeral 1;
val mk_times = HOLogic.mk_binop "op *";
@@ -199,50 +173,50 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val prove_conv = prove_conv
+ val subst_tac = subst_tac
val norm_tac = ALLGOALS
(simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@
- [Suc_eq_add_numeral_1]@add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
+ [add_0, Suc_eq_add_numeral_1]@add_ac))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac@add_ac))
val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
end;
-(* nat eq *)
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
+ val bal_add1 = nat_eq_add_iff1 RS trans
+ val bal_add2 = nat_eq_add_iff2 RS trans
);
-(* nat less *)
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
+ val bal_add1 = nat_less_add_iff1 RS trans
+ val bal_add2 = nat_less_add_iff2 RS trans
);
-(* nat le *)
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
+ val bal_add1 = nat_le_add_iff1 RS trans
+ val bal_add2 = nat_le_add_iff2 RS trans
);
-(* nat diff *)
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 bal_add1 = nat_diff_add_eq1 RS trans
+ val bal_add2 = nat_diff_add_eq2 RS trans
);
@@ -270,11 +244,37 @@
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 subst_tac = subst_tac
+ val norm_tac = ALLGOALS
+ (simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@
+ [add_0, Suc_eq_add_numeral_1]@add_ac))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac@add_ac))
+ val numeral_simp_tac = ALLGOALS
+ (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
+ end;
+
+structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
+
+val combine_numerals =
+ prep_simproc ("nat_combine_numerals",
+ prep_pats ["(i::nat) + (j+k)", "(i::nat) + (j*k)",
+ "(j+k) + (i::nat)", "(j*k) + (i::nat)",
+ "Suc (i + j)"],
+ CombineNumerals.proc);
+
end;
-(**Addsimprocs [Nat_Numeral_Simprocs.fold_Suc];**)
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
+Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
(*examples:
print_depth 22;
@@ -315,6 +315,7 @@
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";
@@ -323,9 +324,14 @@
test "(i + j + #12 + (k::nat)) - #-15 = y";
test "(i + j + #-12 + (k::nat)) - #-15 = y";
-(*fold_Suc*)
+(*combine_numerals*)
+test "k + #3*k = (u::nat)";
+test "Suc (i + #3) = u";
test "Suc (i + j + #3 + k) = u";
-(*negative numerals*)
+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";
*)
@@ -344,13 +350,18 @@
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_Plus_Assoc.conv,Nat_Times_Assoc.conv];
+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
- addsimprocs simprocs
+LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
+ addsimps basic_renamed_arith_simps
+ addsimprocs simprocs
end;
+Delsimprocs [Nat_Plus_Assoc.conv]; (*combine_numerals makes it redundant*)
+
(** For simplifying Suc m - #n **)
@@ -390,3 +401,27 @@
qed "diff_Suc_eq_diff_pred";
Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];
+
+
+(** Evens and Odds, for Mutilated Chess Board **)
+
+(*Case analysis on b<#2*)
+Goal "(n::nat) < #2 ==> n = #0 | n = #1";
+by (arith_tac 1);
+qed "less_2_cases";
+
+Goal "Suc(Suc(m)) mod #2 = m mod #2";
+by (subgoal_tac "m mod #2 < #2" 1);
+by (Asm_simp_tac 2);
+be (less_2_cases RS disjE) 1;
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
+qed "mod2_Suc_Suc";
+Addsimps [mod2_Suc_Suc];
+
+Goal "(0 < m mod #2) = (m mod #2 = #1)";
+by (subgoal_tac "m mod #2 < #2" 1);
+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];
+