src/HOL/Nat.thy
 changeset 46350 a49c89df7c92 parent 46028 9f113cdf3d66 child 46351 4a1f743c05b2
equal 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 `
`  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`