--- 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);
--- 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);
--- 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)
--- 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)