src/HOL/Nat.thy
changeset 46350 a49c89df7c92
parent 46028 9f113cdf3d66
child 46351 4a1f743c05b2
equal deleted inserted replaced
46349:b159ca4e268b 46350:a49c89df7c92
  1614 by arith
  1614 by arith
  1615 
  1615 
  1616 lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
  1616 lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
  1617 by simp
  1617 by simp
  1618 
  1618 
       
  1619 (*The others are
       
  1620       i - j - k = i - (j + k),
       
  1621       k \<le> j ==> j - k + i = j + i - k,
       
  1622       k \<le> j ==> i + (j - k) = i + j - k *)
       
  1623 lemmas add_diff_assoc = diff_add_assoc [symmetric]
       
  1624 lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
       
  1625 declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
       
  1626 
       
  1627 text{*At present we prove no analogue of @{text not_less_Least} or @{text
       
  1628 Least_Suc}, since there appears to be no need.*}
       
  1629 
  1619 text{*Lemmas for ex/Factorization*}
  1630 text{*Lemmas for ex/Factorization*}
  1620 
  1631 
  1621 lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
  1632 lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
  1622 by (cases m) auto
  1633 by (cases m) auto
  1623 
  1634 
  1667   using inc_induct[of "k - i" k P, simplified] by blast
  1678   using inc_induct[of "k - i" k P, simplified] by blast
  1668 
  1679 
  1669 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
  1680 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
  1670   using inc_induct[of 0 k P] by blast
  1681   using inc_induct[of 0 k P] by blast
  1671 
  1682 
  1672 (*The others are
       
  1673       i - j - k = i - (j + k),
       
  1674       k \<le> j ==> j - k + i = j + i - k,
       
  1675       k \<le> j ==> i + (j - k) = i + j - k *)
       
  1676 lemmas add_diff_assoc = diff_add_assoc [symmetric]
       
  1677 lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
       
  1678 declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
       
  1679 
       
  1680 text{*At present we prove no analogue of @{text not_less_Least} or @{text
       
  1681 Least_Suc}, since there appears to be no need.*}
       
  1682 
       
  1683 
  1683 
  1684 subsection {* The divides relation on @{typ nat} *}
  1684 subsection {* The divides relation on @{typ nat} *}
  1685 
  1685 
  1686 lemma dvd_1_left [iff]: "Suc 0 dvd k"
  1686 lemma dvd_1_left [iff]: "Suc 0 dvd k"
  1687 unfolding dvd_def by simp
  1687 unfolding dvd_def by simp