Replaced Suc_remove by Suc_eq_plus1
authornipkow
Wed Jun 24 17:50:49 2009 +0200 (2009-06-24)
changeset 31792d5a6096b94ad
parent 31791 c9a1caf218c8
child 31793 7c10b13d49fe
child 31798 fe9a3043d36c
Replaced Suc_remove by Suc_eq_plus1
src/HOL/NewNumberTheory/Cong.thy
src/HOL/NewNumberTheory/Fib.thy
     1.1 --- a/src/HOL/NewNumberTheory/Cong.thy	Wed Jun 24 15:51:07 2009 +0200
     1.2 +++ b/src/HOL/NewNumberTheory/Cong.thy	Wed Jun 24 17:50:49 2009 +0200
     1.3 @@ -60,9 +60,7 @@
     1.4  lemma nat_1' [simp]: "nat 1 = 1"
     1.5  by simp
     1.6  
     1.7 -(* For those annoying moments where Suc reappears *)
     1.8 -lemma Suc_remove: "Suc n = n + 1"
     1.9 -by simp
    1.10 +(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
    1.11  
    1.12  declare nat_1 [simp del]
    1.13  declare add_2_eq_Suc [simp del] 
     2.1 --- a/src/HOL/NewNumberTheory/Fib.thy	Wed Jun 24 15:51:07 2009 +0200
     2.2 +++ b/src/HOL/NewNumberTheory/Fib.thy	Wed Jun 24 17:50:49 2009 +0200
     2.3 @@ -145,7 +145,7 @@
     2.4    apply (subst nat_fib_reduce)
     2.5    apply (auto simp add: ring_simps)
     2.6    apply (subst (1 3 5) nat_fib_reduce)
     2.7 -  apply (auto simp add: ring_simps Suc_remove)
     2.8 +  apply (auto simp add: ring_simps Suc_eq_plus1)
     2.9  (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
    2.10    apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
    2.11    apply (erule ssubst) back back
    2.12 @@ -220,7 +220,7 @@
    2.13    apply (induct n rule: nat_fib_induct)
    2.14    apply auto
    2.15    apply (subst (2) nat_fib_reduce)
    2.16 -  apply (auto simp add: Suc_remove) (* again, natdiff_cancel *)
    2.17 +  apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
    2.18    apply (subst add_commute, auto)
    2.19    apply (subst nat_gcd_commute, auto simp add: ring_simps)
    2.20  done