# HG changeset patch # User paulson # Date 957371608 -7200 # Node ID 00cff9d083df7fa3a3626a1031c5d24ca66c83c7 # Parent 0e216a0eeda0112d35b755420463d652746a009f Installation of CombineNumerals for the integers Many bug fixes Removal of AssocFold for addition (nat and int) diff -r 0e216a0eeda0 -r 00cff9d083df src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Wed May 03 18:30:29 2000 +0200 +++ b/src/HOL/Integ/Bin.ML Wed May 03 18:33:28 2000 +0200 @@ -265,6 +265,13 @@ by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); qed "zmult_2_right"; +(*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); +qed "zminus_number_of_zmult"; + +Addsimps [zminus_number_of_zmult]; + (** Inequality reasoning **) diff -r 0e216a0eeda0 -r 00cff9d083df src/HOL/Integ/Int.ML --- a/src/HOL/Integ/Int.ML Wed May 03 18:30:29 2000 +0200 +++ b/src/HOL/Integ/Int.ML Wed May 03 18:33:28 2000 +0200 @@ -69,6 +69,11 @@ (*** misc ***) +Goal "- (z - y) = y - (z::int)"; +by (Simp_tac 1); +qed "zminus_zdiff_eq"; +Addsimps [zminus_zdiff_eq]; + Goal "(w 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) @@ -97,6 +106,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.intT; (*decompose additions AND subtractions as a sum*) @@ -259,10 +272,42 @@ "(l::int) * m - n", "(l::int) - m * 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_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 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@zadd_ac@zmult_ac)) + val numeral_simp_tac = ALLGOALS + (simp_tac (HOL_ss addsimps add_0s@bin_simps)) + end; + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); + +val combine_numerals = + prep_simproc ("int_combine_numerals", + prep_pats ["(i::int) + (j+k)", "(i::int) + (j*k)", + "(j+k) + (i::int)", "(j*k) + (i::int)"], + 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; @@ -270,6 +315,8 @@ 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"; @@ -277,15 +324,19 @@ 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) + 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"; @@ -299,8 +350,9 @@ (** 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 cancel_coeffs does the same thing*) + because combine_numerals does the same thing*) structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA = struct @@ -319,18 +371,6 @@ (** The same for the naturals **) -structure Nat_Plus_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 = add_ac -end; - -structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data); - structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA = struct val ss = HOL_ss @@ -343,7 +383,7 @@ structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data); -Addsimprocs [Nat_Plus_Assoc.conv, Nat_Times_Assoc.conv]; +Addsimprocs [Nat_Times_Assoc.conv]; @@ -362,11 +402,14 @@ (* reduce contradictory <= to False *) val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ - [int_0,zmult_0,zmult_0_right]; + [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]; -val simprocs = Int_Numeral_Simprocs.cancel_numerals@ - [Int_Cancel.sum_conv, Int_Cancel.rel_conv (*****, - Int_CC.sum_conv, Int_CC.rel_conv***)]; +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 diff -r 0e216a0eeda0 -r 00cff9d083df src/HOL/Integ/IntDiv.ML --- a/src/HOL/Integ/IntDiv.ML Wed May 03 18:30:29 2000 +0200 +++ b/src/HOL/Integ/IntDiv.ML Wed May 03 18:33:28 2000 +0200 @@ -198,8 +198,7 @@ Addsimps [negateSnd_eq]; Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)"; -by (auto_tac (claset(), - simpset() addsimps split_ifs@[zmult_zminus, quorem_def])); +by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def])); qed "quorem_neg"; Goal "b ~= #0 ==> quorem ((a,b), divAlg(a,b))"; @@ -804,7 +803,7 @@ by (subgoal_tac "#1 <= a" 1); by (arith_tac 2); by (subgoal_tac "#1 < a * #2" 1); - by (dres_inst_tac [("i","#1"), ("k", "#2")] zmult_zle_mono1 2); + by (arith_tac 2); by (subgoal_tac "#2*(#1 + b mod a) <= #2*a" 1); by (rtac zmult_zle_mono2 2); by (auto_tac (claset(), @@ -819,6 +818,9 @@ pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); by (auto_tac (claset(), simpset() addsimps [mod_pos_pos_trivial])); +by (subgoal_tac "#0 <= b mod a" 1); + by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); +by (arith_tac 1); qed "pos_zdiv_times_2"; @@ -863,7 +865,7 @@ by (subgoal_tac "#1 <= a" 1); by (arith_tac 2); by (subgoal_tac "#1 < a * #2" 1); - by (dres_inst_tac [("i","#1"), ("k", "#2")] zmult_zle_mono1 2); + by (arith_tac 2); by (subgoal_tac "#2*(#1 + b mod a) <= #2*a" 1); by (rtac zmult_zle_mono2 2); by (auto_tac (claset(), @@ -878,6 +880,9 @@ pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); by (auto_tac (claset(), simpset() addsimps [mod_pos_pos_trivial])); +by (subgoal_tac "#0 <= b mod a" 1); + by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); +by (arith_tac 1); qed "pos_zmod_times_2"; diff -r 0e216a0eeda0 -r 00cff9d083df src/HOL/Integ/NatSimprocs.ML --- a/src/HOL/Integ/NatSimprocs.ML Wed May 03 18:30:29 2000 +0200 +++ b/src/HOL/Integ/NatSimprocs.ML Wed May 03 18:33:28 2000 +0200 @@ -76,9 +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) - handle Match => raise TERM("dest_numeral:1", [w])) - | dest_numeral t = raise TERM("dest_numeral:2", [t]); + (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) @@ -175,9 +175,10 @@ val find_first_coeff = find_first_coeff [] val subst_tac = subst_tac val norm_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@ + (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 mult_ac@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)) end; @@ -254,9 +255,10 @@ 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@ + (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 mult_ac@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)) end; @@ -360,8 +362,6 @@ addsimprocs simprocs end; -Delsimprocs [Nat_Plus_Assoc.conv]; (*combine_numerals makes it redundant*) - (** For simplifying Suc m - #n **)