use simproc_setup for more nat_numeral simprocs; add simproc tests
authorhuffman
Fri Nov 11 11:11:03 2011 +0100 (2011-11-11)
changeset 45462aba629d6cee5
parent 45451 74515e8e6046
child 45463 9a588a835c1e
use simproc_setup for more nat_numeral simprocs; add simproc tests
src/HOL/Numeral_Simprocs.thy
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 08:32:48 2011 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 11:11:03 2011 +0100
     1.3 @@ -202,6 +202,10 @@
     1.4  
     1.5  use "Tools/nat_numeral_simprocs.ML"
     1.6  
     1.7 +simproc_setup nat_combine_numerals
     1.8 +  ("(i::nat) + j" | "Suc (i + j)") =
     1.9 +  {* fn phi => Nat_Numeral_Simprocs.combine_numerals *}
    1.10 +
    1.11  simproc_setup nateq_cancel_numerals
    1.12    ("(l::nat) + m = n" | "(l::nat) = m + n" |
    1.13     "(l::nat) * m = n" | "(l::nat) = m * n" |
    1.14 @@ -226,6 +230,26 @@
    1.15     "Suc m - n" | "m - Suc n") =
    1.16    {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
    1.17  
    1.18 +simproc_setup nat_eq_cancel_factor
    1.19 +  ("(l::nat) * m = n" | "(l::nat) = m * n") =
    1.20 +  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
    1.21 +
    1.22 +simproc_setup nat_less_cancel_factor
    1.23 +  ("(l::nat) * m < n" | "(l::nat) < m * n") =
    1.24 +  {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *}
    1.25 +
    1.26 +simproc_setup nat_le_cancel_factor
    1.27 +  ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
    1.28 +  {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
    1.29 +
    1.30 +simproc_setup nat_divide_cancel_factor
    1.31 +  ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
    1.32 +  {* fn phi => Nat_Numeral_Simprocs.divide_cancel_factor *}
    1.33 +
    1.34 +simproc_setup nat_dvd_cancel_factor
    1.35 +  ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
    1.36 +  {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
    1.37 +
    1.38  declaration {* 
    1.39    K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    1.40    #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
    1.41 @@ -247,7 +271,7 @@
    1.42         @{simproc intless_cancel_numerals},
    1.43         @{simproc intle_cancel_numerals}]
    1.44    #> Lin_Arith.add_simprocs
    1.45 -      [Nat_Numeral_Simprocs.combine_numerals,
    1.46 +      [@{simproc nat_combine_numerals},
    1.47         @{simproc nateq_cancel_numerals},
    1.48         @{simproc natless_cancel_numerals},
    1.49         @{simproc natle_cancel_numerals},
     2.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 08:32:48 2011 +0100
     2.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 11:11:03 2011 +0100
     2.3 @@ -5,16 +5,20 @@
     2.4  
     2.5  signature NAT_NUMERAL_SIMPROCS =
     2.6  sig
     2.7 -  val combine_numerals: simproc
     2.8 +  val combine_numerals: simpset -> cterm -> thm option
     2.9    val eq_cancel_numerals: simpset -> cterm -> thm option
    2.10    val less_cancel_numerals: simpset -> cterm -> thm option
    2.11    val le_cancel_numerals: simpset -> cterm -> thm option
    2.12    val diff_cancel_numerals: simpset -> cterm -> thm option
    2.13 -  val cancel_factors: simproc list
    2.14 +  val eq_cancel_factor: simpset -> cterm -> thm option
    2.15 +  val less_cancel_factor: simpset -> cterm -> thm option
    2.16 +  val le_cancel_factor: simpset -> cterm -> thm option
    2.17 +  val divide_cancel_factor: simpset -> cterm -> thm option
    2.18 +  val dvd_cancel_factor: simpset -> cterm -> thm option
    2.19    val cancel_numeral_factors: simproc list
    2.20  end;
    2.21  
    2.22 -structure Nat_Numeral_Simprocs =
    2.23 +structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
    2.24  struct
    2.25  
    2.26  (*Maps n to #n for n = 0, 1, 2*)
    2.27 @@ -232,9 +236,7 @@
    2.28  
    2.29  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
    2.30  
    2.31 -val combine_numerals =
    2.32 -  Numeral_Simprocs.prep_simproc @{theory}
    2.33 -    ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
    2.34 +fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct)
    2.35  
    2.36  
    2.37  (*** Applying CancelNumeralFactorFun ***)
    2.38 @@ -387,30 +389,16 @@
    2.39    fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
    2.40  );
    2.41  
    2.42 -val cancel_factor =
    2.43 -  map (Numeral_Simprocs.prep_simproc @{theory})
    2.44 -   [("nat_eq_cancel_factor",
    2.45 -     ["(l::nat) * m = n", "(l::nat) = m * n"],
    2.46 -     K EqCancelFactor.proc),
    2.47 -    ("nat_less_cancel_factor",
    2.48 -     ["(l::nat) * m < n", "(l::nat) < m * n"],
    2.49 -     K LessCancelFactor.proc),
    2.50 -    ("nat_le_cancel_factor",
    2.51 -     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
    2.52 -     K LeCancelFactor.proc),
    2.53 -    ("nat_divide_cancel_factor",
    2.54 -     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
    2.55 -     K DivideCancelFactor.proc),
    2.56 -    ("nat_dvd_cancel_factor",
    2.57 -     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
    2.58 -     K DvdCancelFactor.proc)];
    2.59 +fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
    2.60 +fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
    2.61 +fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
    2.62 +fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
    2.63 +fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
    2.64  
    2.65  end;
    2.66  
    2.67  
    2.68 -Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
    2.69  Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
    2.70 -Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
    2.71  
    2.72  
    2.73  (*examples:
    2.74 @@ -419,40 +407,10 @@
    2.75  set simp_trace;
    2.76  fun test s = (Goal s; by (Simp_tac 1));
    2.77  
    2.78 -(*combine_numerals*)
    2.79 -test "k + 3*k = (u::nat)";
    2.80 -test "Suc (i + 3) = u";
    2.81 -test "Suc (i + j + 3 + k) = u";
    2.82 -test "k + j + 3*k + j = (u::nat)";
    2.83 -test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
    2.84 -test "(2*n*m) + (3*(m*n)) = (u::nat)";
    2.85 -(*negative numerals: FAIL*)
    2.86 -test "Suc (i + j + -3 + k) = u";
    2.87 -
    2.88  (*cancel_numeral_factors*)
    2.89  test "9*x = 12 * (y::nat)";
    2.90  test "(9*x) div (12 * (y::nat)) = z";
    2.91  test "9*x < 12 * (y::nat)";
    2.92  test "9*x <= 12 * (y::nat)";
    2.93  
    2.94 -(*cancel_factor*)
    2.95 -test "x*k = k*(y::nat)";
    2.96 -test "k = k*(y::nat)";
    2.97 -test "a*(b*c) = (b::nat)";
    2.98 -test "a*(b*c) = d*(b::nat)*(x*a)";
    2.99 -
   2.100 -test "x*k < k*(y::nat)";
   2.101 -test "k < k*(y::nat)";
   2.102 -test "a*(b*c) < (b::nat)";
   2.103 -test "a*(b*c) < d*(b::nat)*(x*a)";
   2.104 -
   2.105 -test "x*k <= k*(y::nat)";
   2.106 -test "k <= k*(y::nat)";
   2.107 -test "a*(b*c) <= (b::nat)";
   2.108 -test "a*(b*c) <= d*(b::nat)*(x*a)";
   2.109 -
   2.110 -test "(x*k) div (k*(y::nat)) = (uu::nat)";
   2.111 -test "(k) div (k*(y::nat)) = (uu::nat)";
   2.112 -test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
   2.113 -test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
   2.114  *)
     3.1 --- a/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 08:32:48 2011 +0100
     3.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 11:11:03 2011 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Testing of arithmetic simprocs *}
     3.5  
     3.6  theory Simproc_Tests
     3.7 -imports Rat
     3.8 +imports Main
     3.9  begin
    3.10  
    3.11  text {*
    3.12 @@ -324,10 +324,11 @@
    3.13    }
    3.14  end
    3.15  
    3.16 -lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
    3.17 +lemma
    3.18 +  fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
    3.19 +  shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
    3.20  oops -- "FIXME: need simproc to cover this case"
    3.21  
    3.22 -
    3.23  subsection {* @{text linordered_ring_less_cancel_factor} *}
    3.24  
    3.25  notepad begin
    3.26 @@ -384,16 +385,49 @@
    3.27    }
    3.28  end
    3.29  
    3.30 -lemma "2/3 * (x::rat) + x / 3 = uu"
    3.31 +lemma
    3.32 +  fixes x :: "'a::{linordered_field_inverse_zero,number_ring}"
    3.33 +  shows "2/3 * x + x / 3 = uu"
    3.34  apply (tactic {* test [@{simproc field_combine_numerals}] *})?
    3.35  oops -- "FIXME: test fails"
    3.36  
    3.37 +subsection {* @{text nat_combine_numerals} *}
    3.38 +
    3.39 +notepad begin
    3.40 +  fix i j k m n u :: nat
    3.41 +  {
    3.42 +    assume "4*k = u" have "k + 3*k = u"
    3.43 +      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    3.44 +  next
    3.45 +    assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
    3.46 +      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    3.47 +  next
    3.48 +    assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
    3.49 +      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    3.50 +  next
    3.51 +    assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u"
    3.52 +      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    3.53 +  next
    3.54 +    assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u"
    3.55 +    have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u"
    3.56 +      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    3.57 +  next
    3.58 +    assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u"
    3.59 +      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    3.60 +  }
    3.61 +end
    3.62 +
    3.63 +(*negative numerals: FAIL*)
    3.64 +lemma "Suc (i + j + -3 + k) = u"
    3.65 +apply (tactic {* test [@{simproc nat_combine_numerals}] *})?
    3.66 +oops
    3.67 +
    3.68  subsection {* @{text nateq_cancel_numerals} *}
    3.69  
    3.70  notepad begin
    3.71    fix i j k l oo u uu vv w y z w' y' z' :: "nat"
    3.72    {
    3.73 -    assume "Suc 0 * u = 0" have "2*u = (u::nat)"
    3.74 +    assume "Suc 0 * u = 0" have "2*u = u"
    3.75        by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
    3.76    next
    3.77      assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
    3.78 @@ -560,4 +594,79 @@
    3.79    }
    3.80  end
    3.81  
    3.82 +subsection {* Factor-cancellation simprocs for type @{typ nat} *}
    3.83 +
    3.84 +text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
    3.85 +@{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
    3.86 +@{text nat_dvd_cancel_factor}. *}
    3.87 +
    3.88 +notepad begin
    3.89 +  fix a b c d k x y uu :: nat
    3.90 +  {
    3.91 +    assume "k = 0 \<or> x = y" have "x*k = k*y"
    3.92 +      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
    3.93 +  next
    3.94 +    assume "k = 0 \<or> Suc 0 = y" have "k = k*y"
    3.95 +      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
    3.96 +  next
    3.97 +    assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b"
    3.98 +      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
    3.99 +  next
   3.100 +    assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)"
   3.101 +      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
   3.102 +  next
   3.103 +    assume "0 < k \<and> x < y" have "x*k < k*y"
   3.104 +      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
   3.105 +  next
   3.106 +    assume "0 < k \<and> Suc 0 < y" have "k < k*y"
   3.107 +      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
   3.108 +  next
   3.109 +    assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b"
   3.110 +      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
   3.111 +  next
   3.112 +    assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)"
   3.113 +      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
   3.114 +  next
   3.115 +    assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y"
   3.116 +      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
   3.117 +  next
   3.118 +    assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y"
   3.119 +      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
   3.120 +  next
   3.121 +    assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b"
   3.122 +      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
   3.123 +  next
   3.124 +    assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)"
   3.125 +      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
   3.126 +  next
   3.127 +    assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
   3.128 +      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
   3.129 +  next
   3.130 +    assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
   3.131 +      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
   3.132 +  next
   3.133 +    assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
   3.134 +      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
   3.135 +  next
   3.136 +    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
   3.137 +    have "(a*(b*c)) div (d*b*(x*a)) = uu"
   3.138 +      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
   3.139 +  next
   3.140 +    assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
   3.141 +      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
   3.142 +  next
   3.143 +    assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"
   3.144 +      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
   3.145 +  next
   3.146 +    assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)"
   3.147 +      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
   3.148 +  next
   3.149 +    assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))"
   3.150 +      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
   3.151 +  next
   3.152 +    assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"
   3.153 +      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
   3.154 +  }
   3.155  end
   3.156 +
   3.157 +end