new simprocs for numerals of type "nat"
authorpaulson
Tue Apr 18 15:51:59 2000 +0200 (2000-04-18)
changeset 87360bfd6678a5fa
parent 8735 bb2250ac9557
child 8737 f9733879ff25
new simprocs for numerals of type "nat"
NEWS
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/fold_Suc.ML
src/Provers/Arith/inverse_fold.ML
     1.1 --- a/NEWS	Tue Apr 18 14:57:18 2000 +0200
     1.2 +++ b/NEWS	Tue Apr 18 15:51:59 2000 +0200
     1.3 @@ -110,6 +110,9 @@
     1.4  basically a generalized version of de-Bruijn representation; very
     1.5  useful in avoiding lifting all operations;
     1.6  
     1.7 +* greatly improved simplification involving numerals of type "nat", e.g. in
     1.8 +   (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k;
     1.9 +
    1.10  * new version of "case_tac" subsumes both boolean case split and
    1.11  "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
    1.12  exists, may define val exhaust_tac = case_tac for ad-hoc portability;
     2.1 --- a/src/HOL/IsaMakefile	Tue Apr 18 14:57:18 2000 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Apr 18 15:51:59 2000 +0200
     2.3 @@ -35,6 +35,9 @@
     2.4    $(SRC)/Provers/Arith/cancel_sums.ML		\
     2.5    $(SRC)/Provers/Arith/assoc_fold.ML		\
     2.6    $(SRC)/Provers/Arith/combine_coeff.ML		\
     2.7 +  $(SRC)/Provers/Arith/inverse_fold.ML		\
     2.8 +  $(SRC)/Provers/Arith/fold_Suc.ML		\
     2.9 +  $(SRC)/Provers/Arith/cancel_numerals.ML		\
    2.10    $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    2.11    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    2.12    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
     3.1 --- a/src/HOL/ROOT.ML	Tue Apr 18 14:57:18 2000 +0200
     3.2 +++ b/src/HOL/ROOT.ML	Tue Apr 18 15:51:59 2000 +0200
     3.3 @@ -31,6 +31,9 @@
     3.4  use "~~/src/Provers/Arith/assoc_fold.ML";
     3.5  use "~~/src/Provers/quantifier1.ML";
     3.6  use "~~/src/Provers/Arith/combine_coeff.ML";
     3.7 +use "~~/src/Provers/Arith/inverse_fold.ML";
     3.8 +use "~~/src/Provers/Arith/cancel_numerals.ML";
     3.9 +use "~~/src/Provers/Arith/fold_Suc.ML";
    3.10  
    3.11  with_path "Integ" use_thy "Main";
    3.12  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Tue Apr 18 15:51:59 2000 +0200
     4.3 @@ -0,0 +1,61 @@
     4.4 +(*  Title:      Provers/Arith/cancel_sums.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   2000  University of Cambridge
     4.8 +
     4.9 +Cancel common literals in balanced expressions:
    4.10 +
    4.11 +     i + #m + j ~~ i' + #m' + j'  ==  #(m-m') + i + j ~~ i' + j'
    4.12 +
    4.13 +where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).
    4.14 +*)
    4.15 +
    4.16 +signature CANCEL_NUMERALS_DATA =
    4.17 +sig
    4.18 +  (*abstract syntax*)
    4.19 +  val mk_numeral: int -> term
    4.20 +  val find_first_numeral: term list -> int * term * term list
    4.21 +  val mk_sum: term list -> term
    4.22 +  val dest_sum: term -> term list
    4.23 +  val mk_bal: term * term -> term
    4.24 +  val dest_bal: term -> term * term
    4.25 +  (*proof tools*)
    4.26 +  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    4.27 +  val subst_tac: term -> tactic
    4.28 +  val all_simp_tac: tactic
    4.29 +end;
    4.30 +
    4.31 +signature CANCEL_NUMERALS =
    4.32 +sig
    4.33 +  val proc: Sign.sg -> thm list -> term -> thm option
    4.34 +end;
    4.35 +
    4.36 +
    4.37 +functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
    4.38 +struct
    4.39 +
    4.40 +(*predicting the outputs of other simprocs given a term of the form
    4.41 +   (i + ... #m + ... j) - #n   *)
    4.42 +fun cancelled m n terms =
    4.43 +    if m = n then (*cancel_sums: sort the terms*)
    4.44 +	sort Term.term_ord terms 
    4.45 +    else          (*inverse_fold: subtract, keeping original term order*)
    4.46 +	Data.mk_numeral (m - n) :: terms;
    4.47 +
    4.48 +(*the simplification procedure*)
    4.49 +fun proc sg _ t =
    4.50 +  let val (t1,t2) = Data.dest_bal t 
    4.51 +      val (n1, lit1, terms1) = Data.find_first_numeral (Data.dest_sum t1)
    4.52 +      and (n2, lit2, terms2) = Data.find_first_numeral (Data.dest_sum t2)
    4.53 +      val lit_n = if n1<n2 then lit1 else lit2
    4.54 +      and n     = BasisLibrary.Int.min (n1,n2)
    4.55 +          (*having both the literals and their integer values makes it
    4.56 +            more robust against negative natural number literals*)
    4.57 +  in
    4.58 +      Data.prove_conv [Data.subst_tac lit_n, Data.all_simp_tac] sg
    4.59 +	 (t, Data.mk_bal (Data.mk_sum (cancelled n1 n terms1),
    4.60 +			  Data.mk_sum (cancelled n2 n terms2)))
    4.61 +  end
    4.62 +  handle _ => None;
    4.63 +
    4.64 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Provers/Arith/fold_Suc.ML	Tue Apr 18 15:51:59 2000 +0200
     5.3 @@ -0,0 +1,48 @@
     5.4 +(*  Title:      Provers/Arith/fold_Suc.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   2000  University of Cambridge
     5.8 +
     5.9 +Simplifies  Suc (i + ... #m + ... j) == #(m+1) + i + ... j
    5.10 +*)
    5.11 +
    5.12 +
    5.13 +signature FOLD_SUC_DATA =
    5.14 +sig
    5.15 +  (*abstract syntax*)
    5.16 +  val mk_numeral: int -> term
    5.17 +  val find_first_numeral: term list -> int * term * term list
    5.18 +  val mk_sum: term list -> term
    5.19 +  val dest_sum: term -> term list
    5.20 +  val dest_Suc: term -> term
    5.21 +  (*proof tools*)
    5.22 +  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    5.23 +  val add_norm_tac: tactic
    5.24 +  val numeral_simp_tac: thm list -> tactic
    5.25 +end;
    5.26 +
    5.27 +
    5.28 +functor FoldSucFun(Data: FOLD_SUC_DATA):
    5.29 +		sig
    5.30 +		  val proc: Sign.sg -> thm list -> term -> thm option
    5.31 +		end
    5.32 +=
    5.33 +struct
    5.34 +
    5.35 +fun proc sg _ t =
    5.36 +  let val sum = Data.dest_Suc t 
    5.37 +      val terms = Data.dest_sum sum
    5.38 +      val (m, lit_m, terms') = Data.find_first_numeral terms
    5.39 +      val assocs =  (*If needed, rewrite the literal m to the front:
    5.40 +		     i + #m + j + k == #m + i + (j + k) *)
    5.41 +	  [the (Data.prove_conv [Data.add_norm_tac] sg
    5.42 +		(sum, Data.mk_sum (lit_m::terms')))]
    5.43 +	  handle _ => []
    5.44 +  in
    5.45 +      Data.prove_conv 
    5.46 +        [Data.numeral_simp_tac assocs] sg
    5.47 +	(t, Data.mk_sum (Data.mk_numeral (m+1) :: terms'))
    5.48 +  end
    5.49 +  handle _ => None;
    5.50 +
    5.51 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Provers/Arith/inverse_fold.ML	Tue Apr 18 15:51:59 2000 +0200
     6.3 @@ -0,0 +1,65 @@
     6.4 +(*  Title:      Provers/Arith/inverse_fold.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   2000  University of Cambridge
     6.8 +
     6.9 +For things like  (i + #m + j) - #n   == #(m-n) + i + j    (n<m)
    6.10 +                                     == i + j - #(n-m)    (m<n)
    6.11 +
    6.12 +and maybe        (i * #m * j) div #n == #(m div n) * i * j   (n divides m)
    6.13 +
    6.14 +This simproc is needed for cancel_numerals.ML
    6.15 +*)
    6.16 +
    6.17 +
    6.18 +signature INVERSE_FOLD_DATA =
    6.19 +sig
    6.20 +  (*abstract syntax*)
    6.21 +  val mk_numeral: int -> term
    6.22 +  val dest_numeral: term -> int
    6.23 +  val find_first_numeral: term list -> int * term * term list
    6.24 +  val mk_sum: term list -> term
    6.25 +  val dest_sum: term -> term list
    6.26 +  val mk_diff: term * term -> term
    6.27 +  val dest_diff: term -> term * term
    6.28 +  (*rules*)
    6.29 +  val double_diff_eq: thm
    6.30 +  val move_diff_eq: thm
    6.31 +  (*proof tools*)
    6.32 +  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    6.33 +  val add_norm_tac: tactic
    6.34 +  val numeral_simp_tac: thm list -> tactic
    6.35 +end;
    6.36 +
    6.37 +
    6.38 +functor InverseFoldFun(Data: INVERSE_FOLD_DATA): 
    6.39 +		sig
    6.40 +		  val proc: Sign.sg -> thm list -> term -> thm option
    6.41 +		end
    6.42 +=
    6.43 +struct
    6.44 +
    6.45 +fun proc sg _ t =
    6.46 +  let val (sum,lit_n) = Data.dest_diff t 
    6.47 +      val terms = Data.dest_sum sum
    6.48 +      val (m, lit_m, terms') = Data.find_first_numeral terms
    6.49 +      val n = Data.dest_numeral lit_n
    6.50 +      and sum' = Data.mk_sum terms'
    6.51 +      val assocs =  (*If needed, rewrite the literal m to the front:
    6.52 +		      i + #m + j + k == #m + i + (j + k) *)
    6.53 +	    [the (Data.prove_conv [Data.add_norm_tac] sg 
    6.54 +		  (sum, Data.mk_sum [lit_m, sum']))]
    6.55 +            handle _ => []
    6.56 +  in
    6.57 +      if m < n then
    6.58 +	    Data.prove_conv 
    6.59 +	     [Data.numeral_simp_tac (Data.double_diff_eq::assocs)] sg
    6.60 +	     (t, Data.mk_diff (sum', Data.mk_numeral (n-m)))
    6.61 +      else (*n < m, since equality would have been cancelled*)
    6.62 +	    Data.prove_conv 
    6.63 +	     [Data.numeral_simp_tac (Data.move_diff_eq::assocs)] sg
    6.64 +	     (t, Data.mk_sum [Data.mk_numeral (m-n), sum'])
    6.65 +  end
    6.66 +  handle _ => None;
    6.67 +
    6.68 +end;