simprocs now simplify the RHS of their result
authorpaulson
Fri May 05 17:49:54 2000 +0200 (2000-05-05)
changeset 879989e9deef4bcb
parent 8798 d289a68e74ea
child 8800 e3688ef49f12
simprocs now simplify the RHS of their result
src/HOL/Integ/IntArith.ML
src/HOL/Integ/NatSimprocs.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
     1.1 --- a/src/HOL/Integ/IntArith.ML	Fri May 05 17:49:34 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.ML	Fri May 05 17:49:54 2000 +0200
     1.3 @@ -76,6 +76,11 @@
     1.4                                       @zadd_ac@rel_iff_rel_0_rls) 1);
     1.5  qed "le_add_iff2";
     1.6  
     1.7 +(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
     1.8 +Goal "u = u' ==> (t=u) = (t=u')";
     1.9 +by Auto_tac;
    1.10 +qed "eq_cong2";
    1.11 +
    1.12  
    1.13  structure Int_Numeral_Simprocs =
    1.14  struct
    1.15 @@ -178,24 +183,24 @@
    1.16  (*To let us treat subtraction as addition*)
    1.17  val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
    1.18  
    1.19 -val def_trans = def_imp_eq RS trans;
    1.20 -
    1.21  (*Apply the given rewrite (if present) just once*)
    1.22 -fun subst_tac None      = all_tac
    1.23 -  | subst_tac (Some th) = ALLGOALS (rtac (th RS def_trans));
    1.24 -
    1.25 -val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    1.26 +fun trans_tac None      = all_tac
    1.27 +  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
    1.28  
    1.29  fun prove_conv name tacs sg (t, u) =
    1.30    if t aconv u then None
    1.31    else
    1.32 -  Some
    1.33 -     (mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
    1.34 -	(K tacs))
    1.35 +  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
    1.36 +  in Some
    1.37 +     (prove_goalw_cterm [] ct (K tacs)
    1.38        handle ERROR => error 
    1.39  	  ("The error(s) above occurred while trying to prove " ^
    1.40 -	   string_of_cterm (cterm_of sg (mk_eqv (t, u))) ^ 
    1.41 -	   "\nInternal failure of simproc " ^ name));
    1.42 +	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
    1.43 +  end;
    1.44 +
    1.45 +fun simplify_meta_eq rules =
    1.46 +    mk_meta_eq o
    1.47 +    simplify (HOL_basic_ss addcongs[eq_cong2] addsimps rules)
    1.48  
    1.49  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    1.50  fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT);
    1.51 @@ -208,13 +213,14 @@
    1.52    val mk_coeff		= mk_coeff
    1.53    val dest_coeff	= dest_coeff 1
    1.54    val find_first_coeff	= find_first_coeff []
    1.55 -  val subst_tac         = subst_tac
    1.56 +  val trans_tac         = trans_tac
    1.57    val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    1.58                                                       zminus_simps@zadd_ac))
    1.59                   THEN ALLGOALS
    1.60                      (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    1.61                                                 bin_simps@zadd_ac@zmult_ac))
    1.62    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    1.63 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
    1.64    end;
    1.65  
    1.66  
    1.67 @@ -272,7 +278,7 @@
    1.68    val dest_coeff	= dest_coeff 1
    1.69    val left_distrib	= left_zadd_zmult_distrib RS trans
    1.70    val prove_conv	= prove_conv "int_combine_numerals"
    1.71 -  val subst_tac          = subst_tac
    1.72 +  val trans_tac          = trans_tac
    1.73    val norm_tac = ALLGOALS
    1.74                     (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    1.75                                                zminus_simps@zadd_ac))
    1.76 @@ -281,6 +287,7 @@
    1.77                                                 bin_simps@zadd_ac@zmult_ac))
    1.78    val numeral_simp_tac	= ALLGOALS 
    1.79                      (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    1.80 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
    1.81    end;
    1.82  
    1.83  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
     2.1 --- a/src/HOL/Integ/NatSimprocs.ML	Fri May 05 17:49:34 2000 +0200
     2.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Fri May 05 17:49:54 2000 +0200
     2.3 @@ -111,10 +111,12 @@
     2.4  
     2.5  fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
     2.6  
     2.7 -val subst_tac = Int_Numeral_Simprocs.subst_tac;
     2.8 +val trans_tac = Int_Numeral_Simprocs.trans_tac;
     2.9  
    2.10  val prove_conv = Int_Numeral_Simprocs.prove_conv;
    2.11  
    2.12 +val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq;
    2.13 +
    2.14  val bin_simps = [add_nat_number_of, nat_number_of_add_left,
    2.15  		 diff_nat_number_of, le_nat_number_of_eq_not_less, 
    2.16  		 less_nat_number_of, Let_number_of, nat_number_of] @ 
    2.17 @@ -173,7 +175,7 @@
    2.18    val mk_coeff		= mk_coeff
    2.19    val dest_coeff	= dest_coeff
    2.20    val find_first_coeff	= find_first_coeff []
    2.21 -  val subst_tac          = subst_tac
    2.22 +  val trans_tac          = trans_tac
    2.23    val norm_tac = ALLGOALS
    2.24                     (simp_tac (HOL_ss addsimps add_0s@mult_1s@
    2.25                                         [add_0, Suc_eq_add_numeral_1]@add_ac))
    2.26 @@ -181,6 +183,7 @@
    2.27  				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
    2.28    val numeral_simp_tac	= ALLGOALS
    2.29                  (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
    2.30 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
    2.31    end;
    2.32  
    2.33  
    2.34 @@ -253,7 +256,7 @@
    2.35    val dest_coeff	= dest_coeff
    2.36    val left_distrib	= left_add_mult_distrib RS trans
    2.37    val prove_conv	= prove_conv "nat_combine_numerals"
    2.38 -  val subst_tac          = subst_tac
    2.39 +  val trans_tac          = trans_tac
    2.40    val norm_tac = ALLGOALS
    2.41                     (simp_tac (HOL_ss addsimps add_0s@mult_1s@
    2.42                                         [add_0, Suc_eq_add_numeral_1]@add_ac))
    2.43 @@ -261,6 +264,7 @@
    2.44  				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
    2.45    val numeral_simp_tac	= ALLGOALS
    2.46                  (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
    2.47 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
    2.48    end;
    2.49  
    2.50  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
     3.1 --- a/src/Provers/Arith/cancel_numerals.ML	Fri May 05 17:49:34 2000 +0200
     3.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Fri May 05 17:49:54 2000 +0200
     3.3 @@ -37,9 +37,10 @@
     3.4    val bal_add2: thm
     3.5    (*proof tools*)
     3.6    val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
     3.7 -  val subst_tac: thm option -> tactic
     3.8 -  val norm_tac: tactic
     3.9 -  val numeral_simp_tac: tactic
    3.10 +  val trans_tac: thm option -> tactic (*applies the initial lemma*)
    3.11 +  val norm_tac: tactic                (*proves the initial lemma*)
    3.12 +  val numeral_simp_tac: tactic        (*proves the final theorem*)
    3.13 +  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
    3.14  end;
    3.15  
    3.16  
    3.17 @@ -85,16 +86,17 @@
    3.18  				      newshape(n2,terms2')))
    3.19    in
    3.20  
    3.21 -      if n2<=n1 then 
    3.22 -	  Data.prove_conv 
    3.23 -	     [Data.subst_tac reshape, rtac Data.bal_add1 1,
    3.24 -	      Data.numeral_simp_tac] sg
    3.25 -	     (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
    3.26 -      else
    3.27 -	  Data.prove_conv 
    3.28 -	     [Data.subst_tac reshape, rtac Data.bal_add2 1,
    3.29 -	      Data.numeral_simp_tac] sg
    3.30 -	     (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2')))
    3.31 +      apsome Data.simplify_meta_eq
    3.32 +       (if n2<=n1 then 
    3.33 +	    Data.prove_conv 
    3.34 +	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
    3.35 +		Data.numeral_simp_tac] sg
    3.36 +	       (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
    3.37 +	else
    3.38 +	    Data.prove_conv 
    3.39 +	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
    3.40 +		Data.numeral_simp_tac] sg
    3.41 +	       (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2'))))
    3.42    end
    3.43    handle TERM _ => None
    3.44         | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
     4.1 --- a/src/Provers/Arith/combine_numerals.ML	Fri May 05 17:49:34 2000 +0200
     4.2 +++ b/src/Provers/Arith/combine_numerals.ML	Fri May 05 17:49:54 2000 +0200
     4.3 @@ -27,9 +27,10 @@
     4.4    val left_distrib: thm
     4.5    (*proof tools*)
     4.6    val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
     4.7 -  val subst_tac: thm option -> tactic
     4.8 -  val norm_tac: tactic
     4.9 -  val numeral_simp_tac: tactic
    4.10 +  val trans_tac: thm option -> tactic (*applies the initial lemma*)
    4.11 +  val norm_tac: tactic                (*proves the initial lemma*)
    4.12 +  val numeral_simp_tac: tactic        (*proves the final theorem*)
    4.13 +  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
    4.14  end;
    4.15  
    4.16  
    4.17 @@ -76,10 +77,11 @@
    4.18  			 Data.mk_sum ([Data.mk_coeff(m,u),
    4.19  				       Data.mk_coeff(n,u)] @ terms))
    4.20    in
    4.21 -      Data.prove_conv 
    4.22 -        [Data.subst_tac reshape, rtac Data.left_distrib 1,
    4.23 -	 Data.numeral_simp_tac] sg
    4.24 -	(t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms))
    4.25 +      apsome Data.simplify_meta_eq
    4.26 +	 (Data.prove_conv 
    4.27 +	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    4.28 +	     Data.numeral_simp_tac] sg
    4.29 +	    (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
    4.30    end
    4.31    handle TERM _ => None
    4.32         | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)