# HG changeset patch # User paulson # Date 957541794 -7200 # Node ID 89e9deef4bcb250a56c98c2fddedfdc2587f92f7 # Parent d289a68e74ea3eafc1752c22887472f3b30980d2 simprocs now simplify the RHS of their result diff -r d289a68e74ea -r 89e9deef4bcb src/HOL/Integ/IntArith.ML --- a/src/HOL/Integ/IntArith.ML Fri May 05 17:49:34 2000 +0200 +++ b/src/HOL/Integ/IntArith.ML Fri May 05 17:49:54 2000 +0200 @@ -76,6 +76,11 @@ @zadd_ac@rel_iff_rel_0_rls) 1); qed "le_add_iff2"; +(*To tidy up the result of a simproc. Only the RHS will be simplified.*) +Goal "u = u' ==> (t=u) = (t=u')"; +by Auto_tac; +qed "eq_cong2"; + structure Int_Numeral_Simprocs = struct @@ -178,24 +183,24 @@ (*To let us treat subtraction as addition*) val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; -val def_trans = def_imp_eq RS trans; - (*Apply the given rewrite (if present) just once*) -fun subst_tac None = all_tac - | subst_tac (Some th) = ALLGOALS (rtac (th RS def_trans)); - -val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; +fun trans_tac None = all_tac + | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); fun prove_conv name tacs sg (t, u) = if t aconv u then None else - Some - (mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u))) - (K tacs)) + let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) + in Some + (prove_goalw_cterm [] ct (K tacs) handle ERROR => error ("The error(s) above occurred while trying to prove " ^ - string_of_cterm (cterm_of sg (mk_eqv (t, u))) ^ - "\nInternal failure of simproc " ^ name)); + string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) + end; + +fun simplify_meta_eq rules = + mk_meta_eq o + simplify (HOL_basic_ss addcongs[eq_cong2] addsimps rules) fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT); @@ -208,13 +213,14 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val find_first_coeff = find_first_coeff [] - val subst_tac = subst_tac + val trans_tac = trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ zminus_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)) + val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) end; @@ -272,7 +278,7 @@ 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 trans_tac = trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ zminus_simps@zadd_ac)) @@ -281,6 +287,7 @@ bin_simps@zadd_ac@zmult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) + val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); diff -r d289a68e74ea -r 89e9deef4bcb src/HOL/Integ/NatSimprocs.ML --- a/src/HOL/Integ/NatSimprocs.ML Fri May 05 17:49:34 2000 +0200 +++ b/src/HOL/Integ/NatSimprocs.ML Fri May 05 17:49:54 2000 +0200 @@ -111,10 +111,12 @@ fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t)); -val subst_tac = Int_Numeral_Simprocs.subst_tac; +val trans_tac = Int_Numeral_Simprocs.trans_tac; val prove_conv = Int_Numeral_Simprocs.prove_conv; +val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq; + val bin_simps = [add_nat_number_of, nat_number_of_add_left, diff_nat_number_of, le_nat_number_of_eq_not_less, less_nat_number_of, Let_number_of, nat_number_of] @ @@ -173,7 +175,7 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff val find_first_coeff = find_first_coeff [] - val subst_tac = subst_tac + val trans_tac = trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@ [add_0, Suc_eq_add_numeral_1]@add_ac)) @@ -181,6 +183,7 @@ (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)) + val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) end; @@ -253,7 +256,7 @@ val dest_coeff = dest_coeff val left_distrib = left_add_mult_distrib RS trans val prove_conv = prove_conv "nat_combine_numerals" - val subst_tac = subst_tac + val trans_tac = trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@ [add_0, Suc_eq_add_numeral_1]@add_ac)) @@ -261,6 +264,7 @@ (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)) + val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); diff -r d289a68e74ea -r 89e9deef4bcb src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Fri May 05 17:49:34 2000 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Fri May 05 17:49:54 2000 +0200 @@ -37,9 +37,10 @@ val bal_add2: thm (*proof tools*) val prove_conv: tactic list -> Sign.sg -> term * term -> thm option - val subst_tac: thm option -> tactic - val norm_tac: tactic - val numeral_simp_tac: tactic + val trans_tac: thm option -> tactic (*applies the initial lemma*) + val norm_tac: tactic (*proves the initial lemma*) + val numeral_simp_tac: tactic (*proves the final theorem*) + val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) end; @@ -85,16 +86,17 @@ newshape(n2,terms2'))) in - if n2<=n1 then - Data.prove_conv - [Data.subst_tac reshape, rtac Data.bal_add1 1, - Data.numeral_simp_tac] sg - (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2')) - else - Data.prove_conv - [Data.subst_tac reshape, rtac Data.bal_add2 1, - Data.numeral_simp_tac] sg - (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2'))) + apsome Data.simplify_meta_eq + (if n2<=n1 then + Data.prove_conv + [Data.trans_tac reshape, rtac Data.bal_add1 1, + Data.numeral_simp_tac] sg + (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2')) + else + Data.prove_conv + [Data.trans_tac reshape, rtac Data.bal_add2 1, + Data.numeral_simp_tac] sg + (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2')))) end handle TERM _ => None | TYPE _ => None; (*Typically (if thy doesn't include Numeral) diff -r d289a68e74ea -r 89e9deef4bcb src/Provers/Arith/combine_numerals.ML --- a/src/Provers/Arith/combine_numerals.ML Fri May 05 17:49:34 2000 +0200 +++ b/src/Provers/Arith/combine_numerals.ML Fri May 05 17:49:54 2000 +0200 @@ -27,9 +27,10 @@ val left_distrib: thm (*proof tools*) val prove_conv: tactic list -> Sign.sg -> term * term -> thm option - val subst_tac: thm option -> tactic - val norm_tac: tactic - val numeral_simp_tac: tactic + val trans_tac: thm option -> tactic (*applies the initial lemma*) + val norm_tac: tactic (*proves the initial lemma*) + val numeral_simp_tac: tactic (*proves the final theorem*) + val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) end; @@ -76,10 +77,11 @@ Data.mk_sum ([Data.mk_coeff(m,u), Data.mk_coeff(n,u)] @ terms)) in - Data.prove_conv - [Data.subst_tac reshape, rtac Data.left_distrib 1, - Data.numeral_simp_tac] sg - (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)) + apsome Data.simplify_meta_eq + (Data.prove_conv + [Data.trans_tac reshape, rtac Data.left_distrib 1, + Data.numeral_simp_tac] sg + (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms))) end handle TERM _ => None | TYPE _ => None; (*Typically (if thy doesn't include Numeral)