--- a/src/ZF/ArithSimp.thy Tue Oct 17 15:10:14 2023 +0200
+++ b/src/ZF/ArithSimp.thy Tue Oct 17 15:51:28 2023 +0200
@@ -9,10 +9,78 @@
imports Arith
begin
+subsection \<open>Arithmetic simplification\<close>
+
ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
ML_file \<open>arith_data.ML\<close>
+simproc_setup nateq_cancel_numerals
+ ("l #+ m = n" | "l = m #+ n" | "l #* m = n" | "l = m #* n" | "succ(m) = n" | "m = succ(n)") =
+ \<open>K ArithData.nateq_cancel_numerals_proc\<close>
+
+simproc_setup natless_cancel_numerals
+ ("l #+ m < n" | "l < m #+ n" | "l #* m < n" | "l < m #* n" | "succ(m) < n" | "m < succ(n)") =
+ \<open>K ArithData.natless_cancel_numerals_proc\<close>
+
+simproc_setup natdiff_cancel_numerals
+ ("(l #+ m) #- n" | "l #- (m #+ n)" | "(l #* m) #- n" | "l #- (m #* n)" |
+ "succ(m) #- n" | "m #- succ(n)") =
+ \<open>K ArithData.natdiff_cancel_numerals_proc\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+lemma "x #+ y = x #+ z" apply simp oops
+lemma "y #+ x = x #+ z" apply simp oops
+lemma "x #+ y #+ z = x #+ z" apply simp oops
+lemma "y #+ (z #+ x) = z #+ x" apply simp oops
+lemma "x #+ y #+ z = (z #+ y) #+ (x #+ w)" apply simp oops
+lemma "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)" apply simp oops
+
+lemma "x #+ succ(y) = x #+ z" apply simp oops
+lemma "x #+ succ(y) = succ(z #+ x)" apply simp oops
+lemma "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)" apply simp oops
+
+lemma "(x #+ y) #- (x #+ z) = w" apply simp oops
+lemma "(y #+ x) #- (x #+ z) = dd" apply simp oops
+lemma "(x #+ y #+ z) #- (x #+ z) = dd" apply simp oops
+lemma "(y #+ (z #+ x)) #- (z #+ x) = dd" apply simp oops
+lemma "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd" apply simp oops
+lemma "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd" apply simp oops
+
+(*BAD occurrence of natify*)
+lemma "(x #+ succ(y)) #- (x #+ z) = dd" apply simp oops
+
+lemma "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2" apply simp oops
+
+lemma "(x #+ succ(y)) #- (succ(z #+ x)) = dd" apply simp oops
+lemma "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd" apply simp oops
+
+(*use of typing information*)
+lemma "x : nat ==> x #+ y = x" apply simp oops
+lemma "x : nat --> x #+ y = x" apply simp oops
+lemma "x : nat ==> x #+ y < x" apply simp oops
+lemma "x : nat ==> x < y#+x" apply simp oops
+lemma "x : nat ==> x \<le> succ(x)" apply simp oops
+
+(*fails: no typing information isn't visible*)
+lemma "x #+ y = x" apply simp? oops
+
+lemma "x #+ y < x #+ z" apply simp oops
+lemma "y #+ x < x #+ z" apply simp oops
+lemma "x #+ y #+ z < x #+ z" apply simp oops
+lemma "y #+ z #+ x < x #+ z" apply simp oops
+lemma "y #+ (z #+ x) < z #+ x" apply simp oops
+lemma "x #+ y #+ z < (z #+ y) #+ (x #+ w)" apply simp oops
+lemma "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)" apply simp oops
+
+lemma "x #+ succ(y) < x #+ z" apply simp oops
+lemma "x #+ succ(y) < succ(z #+ x)" apply simp oops
+lemma "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)" apply simp oops
+
+lemma "x #+ succ(y) \<le> succ(z #+ x)" apply simp oops
+
subsection\<open>Difference\<close>
--- a/src/ZF/Bin.thy Tue Oct 17 15:10:14 2023 +0200
+++ b/src/ZF/Bin.thy Tue Oct 17 15:51:28 2023 +0200
@@ -702,7 +702,26 @@
ML_file \<open>int_arith.ML\<close>
-subsection \<open>examples:\<close>
+simproc_setup inteq_cancel_numerals
+ ("l $+ m = n" | "l = m $+ n" | "l $- m = n" | "l = m $- n" | "l $* m = n" | "l = m $* n") =
+ \<open>K Int_Numeral_Simprocs.inteq_cancel_numerals_proc\<close>
+
+simproc_setup intless_cancel_numerals
+ ("l $+ m $< n" | "l $< m $+ n" | "l $- m $< n" | "l $< m $- n" | "l $* m $< n" | "l $< m $* n") =
+ \<open>K Int_Numeral_Simprocs.intless_cancel_numerals_proc\<close>
+
+simproc_setup intle_cancel_numerals
+ ("l $+ m $\<le> n" | "l $\<le> m $+ n" | "l $- m $\<le> n" | "l $\<le> m $- n" | "l $* m $\<le> n" | "l $\<le> m $* n") =
+ \<open>K Int_Numeral_Simprocs.intle_cancel_numerals_proc\<close>
+
+simproc_setup int_combine_numerals ("i $+ j" | "i $- j") =
+ \<open>K Int_Numeral_Simprocs.int_combine_numerals_proc\<close>
+
+simproc_setup int_combine_numerals_prod ("i $* j") =
+ \<open>K Int_Numeral_Simprocs.int_combine_numerals_prod_proc\<close>
+
+
+subsubsection \<open>Examples\<close>
text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close>
lemma "#5 $* x $* #3 = y" apply simp oops
--- a/src/ZF/arith_data.ML Tue Oct 17 15:10:14 2023 +0200
+++ b/src/ZF/arith_data.ML Tue Oct 17 15:51:28 2023 +0200
@@ -7,7 +7,9 @@
signature ARITH_DATA =
sig
(*the main outcome*)
- val nat_cancel: simproc list
+ val nateq_cancel_numerals_proc: Proof.context -> cterm -> thm option
+ val natless_cancel_numerals_proc: Proof.context -> cterm -> thm option
+ val natdiff_cancel_numerals_proc: Proof.context -> cterm -> thm option
(*tools for use in similar applications*)
val gen_trans_tac: Proof.context -> thm -> thm option -> tactic
val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
@@ -184,87 +186,8 @@
structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
-
-val nat_cancel =
- [Simplifier.make_simproc \<^context> "nateq_cancel_numerals"
- {lhss =
- [\<^term>\<open>l #+ m = n\<close>, \<^term>\<open>l = m #+ n\<close>,
- \<^term>\<open>l #* m = n\<close>, \<^term>\<open>l = m #* n\<close>,
- \<^term>\<open>succ(m) = n\<close>, \<^term>\<open>m = succ(n)\<close>],
- proc = K EqCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "natless_cancel_numerals"
- {lhss =
- [\<^term>\<open>l #+ m < n\<close>, \<^term>\<open>l < m #+ n\<close>,
- \<^term>\<open>l #* m < n\<close>, \<^term>\<open>l < m #* n\<close>,
- \<^term>\<open>succ(m) < n\<close>, \<^term>\<open>m < succ(n)\<close>],
- proc = K LessCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "natdiff_cancel_numerals"
- {lhss =
- [\<^term>\<open>(l #+ m) #- n\<close>, \<^term>\<open>l #- (m #+ n)\<close>,
- \<^term>\<open>(l #* m) #- n\<close>, \<^term>\<open>l #- (m #* n)\<close>,
- \<^term>\<open>succ(m) #- n\<close>, \<^term>\<open>m #- succ(n)\<close>],
- proc = K DiffCancelNumerals.proc}];
+val nateq_cancel_numerals_proc = EqCancelNumerals.proc;
+val natless_cancel_numerals_proc = LessCancelNumerals.proc;
+val natdiff_cancel_numerals_proc = DiffCancelNumerals.proc;
end;
-
-val _ =
- Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
- ctxt addsimprocs ArithData.nat_cancel));
-
-
-(*examples:
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s; by (Asm_simp_tac 1));
-
-test "x #+ y = x #+ z";
-test "y #+ x = x #+ z";
-test "x #+ y #+ z = x #+ z";
-test "y #+ (z #+ x) = z #+ x";
-test "x #+ y #+ z = (z #+ y) #+ (x #+ w)";
-test "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)";
-
-test "x #+ succ(y) = x #+ z";
-test "x #+ succ(y) = succ(z #+ x)";
-test "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)";
-
-test "(x #+ y) #- (x #+ z) = w";
-test "(y #+ x) #- (x #+ z) = dd";
-test "(x #+ y #+ z) #- (x #+ z) = dd";
-test "(y #+ (z #+ x)) #- (z #+ x) = dd";
-test "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd";
-test "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd";
-
-(*BAD occurrence of natify*)
-test "(x #+ succ(y)) #- (x #+ z) = dd";
-
-test "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2";
-
-test "(x #+ succ(y)) #- (succ(z #+ x)) = dd";
-test "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd";
-
-(*use of typing information*)
-test "x : nat ==> x #+ y = x";
-test "x : nat --> x #+ y = x";
-test "x : nat ==> x #+ y < x";
-test "x : nat ==> x < y#+x";
-test "x : nat ==> x le succ(x)";
-
-(*fails: no typing information isn't visible*)
-test "x #+ y = x";
-
-test "x #+ y < x #+ z";
-test "y #+ x < x #+ z";
-test "x #+ y #+ z < x #+ z";
-test "y #+ z #+ x < x #+ z";
-test "y #+ (z #+ x) < z #+ x";
-test "x #+ y #+ z < (z #+ y) #+ (x #+ w)";
-test "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)";
-
-test "x #+ succ(y) < x #+ z";
-test "x #+ succ(y) < succ(z #+ x)";
-test "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)";
-
-test "x #+ succ(y) le succ(z #+ x)";
-*)
--- a/src/ZF/int_arith.ML Tue Oct 17 15:10:14 2023 +0200
+++ b/src/ZF/int_arith.ML Tue Oct 17 15:51:28 2023 +0200
@@ -6,9 +6,11 @@
signature INT_NUMERAL_SIMPROCS =
sig
- val cancel_numerals: simproc list
- val combine_numerals: simproc
- val combine_numerals_prod: simproc
+ val inteq_cancel_numerals_proc: Proof.context -> cterm -> thm option
+ val intless_cancel_numerals_proc: Proof.context -> cterm -> thm option
+ val intle_cancel_numerals_proc: Proof.context -> cterm -> thm option
+ val int_combine_numerals_proc: Proof.context -> cterm -> thm option
+ val int_combine_numerals_prod_proc: Proof.context -> cterm -> thm option
end
structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =
@@ -50,7 +52,7 @@
fun find_first_numeral past (t::terms) =
((dest_numeral t, rev past @ terms)
handle TERM _ => find_first_numeral (t::past) terms)
- | find_first_numeral past [] = raise TERM("find_first_numeral", []);
+ | find_first_numeral _ [] = raise TERM("find_first_numeral", []);
val zero = mk_numeral 0;
fun mk_plus (t, u) = \<^Const>\<open>zadd for t u\<close>;
@@ -99,7 +101,7 @@
in (sign*n, mk_prod ts') end;
(*Find first coefficient-term THAT MATCHES u*)
-fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", [])
| find_first_coeff past u (t::terms) =
let val (n,u') = dest_coeff 1 t
in if u aconv u' then (n, rev past @ terms)
@@ -204,25 +206,9 @@
val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
);
-val cancel_numerals =
- [Simplifier.make_simproc \<^context> "inteq_cancel_numerals"
- {lhss =
- [\<^term>\<open>l $+ m = n\<close>, \<^term>\<open>l = m $+ n\<close>,
- \<^term>\<open>l $- m = n\<close>, \<^term>\<open>l = m $- n\<close>,
- \<^term>\<open>l $* m = n\<close>, \<^term>\<open>l = m $* n\<close>],
- proc = K EqCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "intless_cancel_numerals"
- {lhss =
- [\<^term>\<open>l $+ m $< n\<close>, \<^term>\<open>l $< m $+ n\<close>,
- \<^term>\<open>l $- m $< n\<close>, \<^term>\<open>l $< m $- n\<close>,
- \<^term>\<open>l $* m $< n\<close>, \<^term>\<open>l $< m $* n\<close>],
- proc = K LessCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "intle_cancel_numerals"
- {lhss =
- [\<^term>\<open>l $+ m $\<le> n\<close>, \<^term>\<open>l $\<le> m $+ n\<close>,
- \<^term>\<open>l $- m $\<le> n\<close>, \<^term>\<open>l $\<le> m $- n\<close>,
- \<^term>\<open>l $* m $\<le> n\<close>, \<^term>\<open>l $\<le> m $* n\<close>],
- proc = K LeCancelNumerals.proc}];
+val inteq_cancel_numerals_proc = EqCancelNumerals.proc;
+val intless_cancel_numerals_proc = LessCancelNumerals.proc;
+val intle_cancel_numerals_proc = LeCancelNumerals.proc;
(*version without the hyps argument*)
@@ -263,11 +249,7 @@
end;
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
-
-val combine_numerals =
- Simplifier.make_simproc \<^context> "int_combine_numerals"
- {lhss = [\<^term>\<open>i $+ j\<close>, \<^term>\<open>i $- j\<close>],
- proc = K CombineNumerals.proc};
+val int_combine_numerals_proc = CombineNumerals.proc
@@ -310,16 +292,6 @@
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
-
-val combine_numerals_prod =
- Simplifier.make_simproc \<^context> "int_combine_numerals_prod"
- {lhss = [\<^term>\<open>i $* j\<close>], proc = K CombineNumeralsProd.proc};
+val int_combine_numerals_prod_proc = CombineNumeralsProd.proc;
end;
-
-val _ =
- Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
- ctxt addsimprocs
- (Int_Numeral_Simprocs.cancel_numerals @
- [Int_Numeral_Simprocs.combine_numerals,
- Int_Numeral_Simprocs.combine_numerals_prod])));