# HG changeset patch
# User haftmann
# Date 1216646843 -7200
# Node ID 55676111ed692fe9701b19d2f1d6a65b6d815ab2
# Parent  cb0021d56e119b53110f987e438e7cc19eaaae61
(re-)added simp rules for (_ + _) div/mod _

diff -r cb0021d56e11 -r 55676111ed69 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Jul 21 15:26:26 2008 +0200
+++ b/src/HOL/Divides.thy	Mon Jul 21 15:27:23 2008 +0200
@@ -98,21 +98,21 @@
 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
   using div_mult_self2_is_id [of _ 1] by simp
 
-lemma div_add_self1:
+lemma div_add_self1 [simp]:
   assumes "b \<noteq> 0"
   shows "(b + a) div b = a div b + 1"
   using assms div_mult_self1 [of b a 1] by (simp add: add_commute)
 
-lemma div_add_self2:
+lemma div_add_self2 [simp]:
   assumes "b \<noteq> 0"
   shows "(a + b) div b = a div b + 1"
   using assms div_add_self1 [of b a] by (simp add: add_commute)
 
-lemma mod_add_self1:
+lemma mod_add_self1 [simp]:
   "(b + a) mod b = a mod b"
   using mod_mult_self1 [of a 1 b] by (simp add: add_commute)
 
-lemma mod_add_self2:
+lemma mod_add_self2 [simp]:
   "(a + b) mod b = a mod b"
   using mod_mult_self1 [of a 1 b] by simp
 
diff -r cb0021d56e11 -r 55676111ed69 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Jul 21 15:26:26 2008 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon Jul 21 15:27:23 2008 +0200
@@ -293,7 +293,7 @@
     apply force
    apply force
   apply(rule Basic)
-     apply (simp add: mod_add_self2)
+     apply simp
      apply clarify
      apply simp
      apply (case_tac "X x (j mod n) \<le> j")
@@ -346,7 +346,7 @@
   apply(rule Basic)
      apply simp
      apply clarify
-     apply (simp add: mod_add_self2)
+     apply simp
      apply(rule allI)
      apply(rule impI)+
      apply(case_tac "X x ! i\<le> j")
diff -r cb0021d56e11 -r 55676111ed69 src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Mon Jul 21 15:26:26 2008 +0200
+++ b/src/HOL/Library/GCD.thy	Mon Jul 21 15:27:23 2008 +0200
@@ -163,11 +163,8 @@
 
 text {* \medskip Addition laws *}
 
-lemma gcd_add1 [simp,algebra]: "gcd (m + n) n = gcd m n"
-  apply (case_tac "n = 0")
-   apply (simp_all add: gcd_non_0)
-  apply (simp add: mod_add_self2)
-  done
+lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
+  by (cases "n = 0") (auto simp add: gcd_non_0)
 
 lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
 proof -