# HG changeset patch # User huffman # Date 1333115772 -7200 # Node ID ea712316fc871b424b4a1cf530d7c90042a4eed0 # Parent 65031898155705705409ebfbe7b8cbb770701e81 set up numeral reorient simproc in Num.thy diff -r 650318981557 -r ea712316fc87 src/HOL/Int.thy --- a/src/HOL/Int.thy Fri Mar 30 15:43:30 2012 +0200 +++ b/src/HOL/Int.thy Fri Mar 30 15:56:12 2012 +0200 @@ -844,16 +844,6 @@ "(m::'a::linordered_idom) = n") = {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} -setup {* - Reorient_Proc.add - (fn Const (@{const_name numeral}, _) $ _ => true - | Const (@{const_name neg_numeral}, _) $ _ => true - | _ => false) -*} - -simproc_setup reorient_numeral - ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc - subsection{*Lemmas About Small Numerals*} diff -r 650318981557 -r ea712316fc87 src/HOL/Num.thy --- a/src/HOL/Num.thy Fri Mar 30 15:43:30 2012 +0200 +++ b/src/HOL/Num.thy Fri Mar 30 15:56:12 2012 +0200 @@ -975,10 +975,6 @@ subsection {* Setting up simprocs *} -lemma numeral_reorient: - "(numeral w = x) = (x = numeral w)" - by auto - lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)" by simp @@ -999,6 +995,16 @@ mult_numeral_1 mult_numeral_1_right mult_minus1 mult_minus1_right +setup {* + Reorient_Proc.add + (fn Const (@{const_name numeral}, _) $ _ => true + | Const (@{const_name neg_numeral}, _) $ _ => true + | _ => false) +*} + +simproc_setup reorient_numeral + ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc + subsubsection {* Simplification of arithmetic operations on integer constants. *}