remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
authorhuffman
Wed Jun 20 17:28:55 2007 +0200 (2007-06-20)
changeset 23438dd824e86fa8a
parent 23437 4a44fcc9dba9
child 23439 8c7da8649f2f
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
src/HOL/IntDef.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/Parity.thy
src/HOL/Nat.thy
src/HOL/Presburger.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/IntDef.thy	Wed Jun 20 17:02:57 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Wed Jun 20 17:28:55 2007 +0200
     1.3 @@ -554,7 +554,8 @@
     1.4  qed
     1.5  
     1.6  lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
     1.7 -by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
     1.8 +by (cases z rule: eq_Abs_Integ)
     1.9 +   (simp add: nat le of_int Zero_int_def of_nat_diff)
    1.10  
    1.11  
    1.12  subsection{*The Set of Integers*}
     2.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Jun 20 17:02:57 2007 +0200
     2.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Jun 20 17:28:55 2007 +0200
     2.3 @@ -105,7 +105,7 @@
     2.4  lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
     2.5    by (simp add: eq_nat_of_int int'_add)
     2.6  lemma [code, code inline]: "m - n = nat (int' m - int' n)"
     2.7 -  by (simp add: int'_def nat_eq_iff2)
     2.8 +  by (simp add: int'_def nat_eq_iff2 of_nat_diff)
     2.9  lemma [code]: "m * n = nat (int' m * int' n)"
    2.10    unfolding int'_def
    2.11    by (simp add: of_nat_mult [symmetric] del: of_nat_mult)
     3.1 --- a/src/HOL/Library/Parity.thy	Wed Jun 20 17:02:57 2007 +0200
     3.2 +++ b/src/HOL/Library/Parity.thy	Wed Jun 20 17:28:55 2007 +0200
     3.3 @@ -143,9 +143,9 @@
     3.4  
     3.5  lemma even_nat_difference:
     3.6      "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
     3.7 -  apply (auto simp add: even_nat_def)
     3.8 -  apply (case_tac "x < y", auto)
     3.9 -  apply (case_tac "x < y", auto)
    3.10 +  apply (auto simp add: even_nat_def zdiff_int [symmetric])
    3.11 +  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
    3.12 +  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
    3.13    done
    3.14  
    3.15  lemma even_nat_Suc: "even (Suc x) = odd x"
     4.1 --- a/src/HOL/Nat.thy	Wed Jun 20 17:02:57 2007 +0200
     4.2 +++ b/src/HOL/Nat.thy	Wed Jun 20 17:28:55 2007 +0200
     4.3 @@ -1372,7 +1372,7 @@
     4.4  lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
     4.5    by (simp add: inj_on_def)
     4.6  
     4.7 -lemma of_nat_diff [simp]:
     4.8 +lemma of_nat_diff:
     4.9      "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
    4.10    by (simp del: of_nat_add
    4.11      add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
     5.1 --- a/src/HOL/Presburger.thy	Wed Jun 20 17:02:57 2007 +0200
     5.2 +++ b/src/HOL/Presburger.thy	Wed Jun 20 17:28:55 2007 +0200
     5.3 @@ -389,7 +389,7 @@
     5.4  
     5.5  lemma zdiff_int_split: "P (int (x - y)) =
     5.6    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
     5.7 -  by (case_tac "y \<le> x", simp_all)
     5.8 +  by (case_tac "y \<le> x", simp_all add: zdiff_int)
     5.9  
    5.10  lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
    5.11  lemma number_of2: "(0::int) <= Numeral0" by simp
     6.1 --- a/src/HOL/Real/RealDef.thy	Wed Jun 20 17:02:57 2007 +0200
     6.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jun 20 17:28:55 2007 +0200
     6.3 @@ -739,7 +739,7 @@
     6.4  by (simp add: real_of_nat_def)
     6.5  
     6.6  lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
     6.7 -by (simp add: add: real_of_nat_def) 
     6.8 +by (simp add: add: real_of_nat_def of_nat_diff)
     6.9  
    6.10  lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
    6.11  by (simp add: add: real_of_nat_def)