# HG changeset patch
# User wenzelm
# Date 1697550688 -7200
# Node ID 4f7dce5c1a81e89ed02639c1f7f3f80ecad8f788
# Parent  8f4424187193549a50f0994bac575cd2bdfc61d4
more standard simproc_setup in Isar;
recovered examples from dead comments;

diff -r 8f4424187193 -r 4f7dce5c1a81 src/ZF/ArithSimp.thy
--- 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>
 
diff -r 8f4424187193 -r 4f7dce5c1a81 src/ZF/Bin.thy
--- 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
diff -r 8f4424187193 -r 4f7dce5c1a81 src/ZF/arith_data.ML
--- 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)";
-*)
diff -r 8f4424187193 -r 4f7dce5c1a81 src/ZF/int_arith.ML
--- 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])));