# HG changeset patch
# User berghofe
# Date 1064239371 -7200
# Node ID 30e41f63712e09232d287724799b0b30cb683f9c
# Parent  d6cb80cc1d2052646b4073469b785ec4f0fd626d
Improved efficiency of code generated for + and -

diff -r d6cb80cc1d20 -r 30e41f63712e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Sep 22 16:01:36 2003 +0200
+++ b/src/HOL/Nat.thy	Mon Sep 22 16:02:51 2003 +0200
@@ -627,10 +627,10 @@
 
 text {* Difference *}
 
-lemma diff_0_eq_0 [simp]: "0 - n = (0::nat)"
+lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
   by (induct_tac n) simp_all
 
-lemma diff_Suc_Suc [simp]: "Suc(m) - Suc(n) = m - n"
+lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
   by (induct_tac n) simp_all
 
 
@@ -642,7 +642,7 @@
 lemma Suc_pred [simp]: "0 < n ==> Suc (n - Suc 0) = n"
   by (simp split add: nat.split)
 
-declare diff_Suc [simp del]
+declare diff_Suc [simp del, code del]
 
 
 subsection {* Addition *}
@@ -653,6 +653,8 @@
 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   by (induct m) simp_all
 
+lemma [code]: "Suc m + n = m + Suc n" by simp
+
 
 text {* Associative law for addition *}
 lemma add_assoc: "(m + n) + k = m + ((n + k)::nat)"