moving declarations back to the section they seem to belong to (cf. afffe1f72143)
authorbulwahn
Sat Jan 28 10:22:46 2012 +0100 (2012-01-28)
changeset 46350a49c89df7c92
parent 46349 b159ca4e268b
child 46351 4a1f743c05b2
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Sat Jan 28 06:13:03 2012 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sat Jan 28 10:22:46 2012 +0100
     1.3 @@ -1616,6 +1616,17 @@
     1.4  lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
     1.5  by simp
     1.6  
     1.7 +(*The others are
     1.8 +      i - j - k = i - (j + k),
     1.9 +      k \<le> j ==> j - k + i = j + i - k,
    1.10 +      k \<le> j ==> i + (j - k) = i + j - k *)
    1.11 +lemmas add_diff_assoc = diff_add_assoc [symmetric]
    1.12 +lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
    1.13 +declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
    1.14 +
    1.15 +text{*At present we prove no analogue of @{text not_less_Least} or @{text
    1.16 +Least_Suc}, since there appears to be no need.*}
    1.17 +
    1.18  text{*Lemmas for ex/Factorization*}
    1.19  
    1.20  lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
    1.21 @@ -1669,17 +1680,6 @@
    1.22  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
    1.23    using inc_induct[of 0 k P] by blast
    1.24  
    1.25 -(*The others are
    1.26 -      i - j - k = i - (j + k),
    1.27 -      k \<le> j ==> j - k + i = j + i - k,
    1.28 -      k \<le> j ==> i + (j - k) = i + j - k *)
    1.29 -lemmas add_diff_assoc = diff_add_assoc [symmetric]
    1.30 -lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
    1.31 -declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
    1.32 -
    1.33 -text{*At present we prove no analogue of @{text not_less_Least} or @{text
    1.34 -Least_Suc}, since there appears to be no need.*}
    1.35 -
    1.36  
    1.37  subsection {* The divides relation on @{typ nat} *}
    1.38