fixing nat_combine_numerals simprocs (again)
authorpaulson
Thu Feb 28 17:46:46 2002 +0100 (2002-02-28)
changeset 12975d796a2fd6c69
parent 12974 7acfab8361d1
child 12976 5cfe2941a5db
fixing nat_combine_numerals simprocs (again)

Theorem eq_cong2 moved from Integ/int_arith1.ML to simpdata.ML, where it will
be available in all theories.

Function simplify_meta_eq now makes the meta-equality first so that eq_cong2
will work properly.
src/HOL/Integ/int_arith1.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Feb 28 17:21:48 2002 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Feb 28 17:46:46 2002 +0100
     1.3 @@ -70,11 +70,6 @@
     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 @@ -206,8 +201,8 @@
    1.16    | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
    1.17  
    1.18  fun simplify_meta_eq rules =
    1.19 -    mk_meta_eq o
    1.20      simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
    1.21 +    o mk_meta_eq;
    1.22  
    1.23  structure CancelNumeralsCommon =
    1.24    struct
     2.1 --- a/src/HOL/simpdata.ML	Thu Feb 28 17:21:48 2002 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Thu Feb 28 17:46:46 2002 +0100
     2.3 @@ -277,6 +277,11 @@
     2.4  by (etac arg_cong 1);
     2.5  qed "let_weak_cong";
     2.6  
     2.7 +(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
     2.8 +Goal "u = u' ==> (t==u) == (t==u')";
     2.9 +by (asm_simp_tac HOL_ss 1);
    2.10 +qed "eq_cong2";
    2.11 +
    2.12  Goal "f(if c then x else y) = (if c then f x else f y)";
    2.13  by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
    2.14  qed "if_distrib";