--- a/src/ZF/Bin.thy Wed Mar 18 21:40:21 2015 +0100
+++ b/src/ZF/Bin.thy Thu Mar 19 11:13:54 2015 +0100
@@ -695,4 +695,62 @@
ML_file "int_arith.ML"
+subsection {* examples: *}
+
+text {* @{text combine_numerals_prod} (products of separate literals) *}
+lemma "#5 $* x $* #3 = y" apply simp oops
+
+schematic_lemma "y2 $+ ?x42 = y $+ y2" apply simp oops
+
+lemma "oo : int ==> l $+ (l $+ #2) $+ oo = oo" apply simp oops
+
+lemma "#9$*x $+ y = x$*#23 $+ z" apply simp oops
+lemma "y $+ x = x $+ z" apply simp oops
+
+lemma "x : int ==> x $+ y $+ z = x $+ z" apply simp oops
+lemma "x : int ==> y $+ (z $+ x) = z $+ x" apply simp oops
+lemma "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)" apply simp oops
+lemma "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)" apply simp oops
+
+lemma "#-3 $* x $+ y $<= x $* #2 $+ 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 "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu" apply simp oops
+lemma "u : int ==> #2 $* u = u" apply simp oops
+lemma "(i $+ j $+ #12 $+ k) $- #15 = y" apply simp oops
+lemma "(i $+ j $+ #12 $+ k) $- #5 = y" apply simp oops
+
+lemma "y $- b $< b" apply simp oops
+lemma "y $- (#3 $* b $+ c) $< b $- #2 $* c" apply simp oops
+
+lemma "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w" apply simp oops
+lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w" apply simp oops
+lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w" apply simp oops
+lemma "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w" apply simp oops
+
+lemma "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y" apply simp oops
+lemma "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y" apply simp oops
+
+lemma "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv" apply simp oops
+
+lemma "a $+ $-(b$+c) $+ b = d" apply simp oops
+lemma "a $+ $-(b$+c) $- b = d" apply simp oops
+
+text {* negative numerals *}
+lemma "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz" apply simp oops
+lemma "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y" apply simp oops
+lemma "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y" apply simp oops
+lemma "(i $+ j $+ #-12 $+ k) $- #15 = y" apply simp oops
+lemma "(i $+ j $+ #12 $+ k) $- #-15 = y" apply simp oops
+lemma "(i $+ j $+ #-12 $+ k) $- #-15 = y" apply simp oops
+
+text {* Multiplying separated numerals *}
+lemma "#6 $* ($# x $* #2) = uu" apply simp oops
+lemma "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu" apply simp oops
+
end
--- a/src/ZF/int_arith.ML Wed Mar 18 21:40:21 2015 +0100
+++ b/src/ZF/int_arith.ML Thu Mar 19 11:13:54 2015 +0100
@@ -325,72 +325,3 @@
(Int_Numeral_Simprocs.cancel_numerals @
[Int_Numeral_Simprocs.combine_numerals,
Int_Numeral_Simprocs.combine_numerals_prod])));
-
-
-(*examples:*)
-(*
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s; by (Asm_simp_tac 1));
-val sg = #sign (rep_thm (topthm()));
-val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
-val (t,_) = FOLogic.dest_eq t;
-
-(*combine_numerals_prod (products of separate literals) *)
-test "#5 $* x $* #3 = y";
-
-test "y2 $+ ?x42 = y $+ y2";
-
-test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
-
-test "#9$*x $+ y = x$*#23 $+ z";
-test "y $+ x = x $+ z";
-
-test "x : int ==> x $+ y $+ z = x $+ z";
-test "x : int ==> y $+ (z $+ x) = z $+ x";
-test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
-test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
-
-test "#-3 $* x $+ y $<= x $* #2 $+ 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 "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
-test "u : int ==> #2 $* u = u";
-test "(i $+ j $+ #12 $+ k) $- #15 = y";
-test "(i $+ j $+ #12 $+ k) $- #5 = y";
-
-test "y $- b $< b";
-test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
-
-test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
-test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
-test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
-test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
-
-test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
-test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
-
-test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv";
-
-test "a $+ $-(b$+c) $+ b = d";
-test "a $+ $-(b$+c) $- b = d";
-
-(*negative numerals*)
-test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
-test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
-test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
-test "(i $+ j $+ #-12 $+ k) $- #15 = y";
-test "(i $+ j $+ #12 $+ k) $- #-15 = y";
-test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
-
-(*Multiplying separated numerals*)
-Goal "#6 $* ($# x $* #2) = uu";
-Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu";
-*)
-