1693 qed |
1694 qed |
1694 |
1695 |
1695 |
1696 |
1696 text\<open>Subtraction laws, mostly by Clemens Ballarin\<close> |
1697 text\<open>Subtraction laws, mostly by Clemens Ballarin\<close> |
1697 |
1698 |
1698 lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c" |
1699 lemma diff_less_mono: |
1699 by arith |
1700 fixes a b c :: nat |
1700 |
1701 assumes "a < b" and "c \<le> a" |
1701 lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))" |
1702 shows "a - c < b - c" |
1702 by arith |
1703 proof - |
|
1704 from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0" |
|
1705 by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps) |
|
1706 then show ?thesis by simp |
|
1707 qed |
|
1708 |
|
1709 lemma less_diff_conv: |
|
1710 fixes i j k :: nat |
|
1711 shows "i < j - k \<longleftrightarrow> i + k < j" (is "?P \<longleftrightarrow> ?Q") |
|
1712 by (cases "k \<le> j") |
|
1713 (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex) |
1703 |
1714 |
1704 lemma less_diff_conv2: |
1715 lemma less_diff_conv2: |
1705 fixes j k i :: nat |
1716 fixes j k i :: nat |
1706 assumes "k \<le> j" |
1717 assumes "k \<le> j" |
1707 shows "j - k < i \<longleftrightarrow> j < i + k" |
1718 shows "j - k < i \<longleftrightarrow> j < i + k" (is "?P \<longleftrightarrow> ?Q") |
1708 using assms by arith |
1719 using assms by (auto dest: le_Suc_ex) |
1709 |
1720 |
1710 lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)" |
1721 lemma le_diff_conv: |
1711 by arith |
1722 fixes j k i :: nat |
1712 |
1723 shows "j - k \<le> i \<longleftrightarrow> j \<le> i + k" |
1713 lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i" |
1724 by (cases "k \<le> j") |
1714 by arith |
1725 (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex) |
1715 |
1726 |
1716 (*Replaces the previous diff_less and le_diff_less, which had the stronger |
1727 lemma diff_diff_cancel [simp]: |
1717 second premise n\<le>m*) |
1728 fixes i n :: nat |
1718 lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m" |
1729 shows "i \<le> n \<Longrightarrow> n - (n - i) = i" |
1719 by arith |
1730 by (auto dest: le_Suc_ex) |
|
1731 |
|
1732 lemma diff_less [simp]: |
|
1733 fixes i n :: nat |
|
1734 shows "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m" |
|
1735 by (auto dest: less_imp_Suc_add) |
1720 |
1736 |
1721 text \<open>Simplification of relational expressions involving subtraction\<close> |
1737 text \<open>Simplification of relational expressions involving subtraction\<close> |
1722 |
1738 |
1723 lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)" |
1739 lemma diff_diff_eq: |
1724 by (simp split add: nat_diff_split) |
1740 fixes m n k :: nat |
|
1741 shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n" |
|
1742 by (auto dest!: le_Suc_ex) |
1725 |
1743 |
1726 hide_fact (open) diff_diff_eq |
1744 hide_fact (open) diff_diff_eq |
1727 |
1745 |
1728 lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)" |
1746 lemma eq_diff_iff: |
1729 by (auto split add: nat_diff_split) |
1747 fixes m n k :: nat |
1730 |
1748 shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n" |
1731 lemma less_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)" |
1749 by (auto dest: le_Suc_ex) |
1732 by (auto split add: nat_diff_split) |
1750 |
1733 |
1751 lemma less_diff_iff: |
1734 lemma le_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)" |
1752 fixes m n k :: nat |
1735 by (auto split add: nat_diff_split) |
1753 shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n" |
|
1754 by (auto dest!: le_Suc_ex) |
|
1755 |
|
1756 lemma le_diff_iff: |
|
1757 fixes m n k :: nat |
|
1758 shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n" |
|
1759 by (auto dest!: le_Suc_ex) |
1736 |
1760 |
1737 text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close> |
1761 text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close> |
1738 |
1762 |
1739 (* Monotonicity of subtraction in first argument *) |
1763 lemma diff_le_mono: |
1740 lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)" |
1764 fixes m n l :: nat |
1741 by (simp split add: nat_diff_split) |
1765 shows "m \<le> n \<Longrightarrow> m - l \<le> n - l" |
1742 |
1766 by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split) |
1743 lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)" |
1767 |
1744 by (simp split add: nat_diff_split) |
1768 lemma diff_le_mono2: |
1745 |
1769 fixes m n l :: nat |
1746 lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)" |
1770 shows "m \<le> n \<Longrightarrow> l - n \<le> l - m" |
1747 by (simp split add: nat_diff_split) |
1771 by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split) |
1748 |
1772 |
1749 lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n" |
1773 lemma diff_less_mono2: |
1750 by (simp split add: nat_diff_split) |
1774 fixes m n l :: nat |
1751 |
1775 shows "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m" |
1752 lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i" |
1776 by (auto dest: less_imp_Suc_add split add: nat_diff_split) |
1753 by auto |
1777 |
|
1778 lemma diffs0_imp_equal: |
|
1779 fixes m n :: nat |
|
1780 shows "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n" |
|
1781 by (simp split add: nat_diff_split) |
|
1782 |
|
1783 lemma min_diff: |
|
1784 fixes m n i :: nat |
|
1785 shows "min (m - i) (n - i) = min m n - i" (is "?lhs = ?rhs") |
|
1786 by (cases m n rule: le_cases) |
|
1787 (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono) |
1754 |
1788 |
1755 lemma inj_on_diff_nat: |
1789 lemma inj_on_diff_nat: |
1756 assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)" |
1790 assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)" |
1757 shows "inj_on (\<lambda>n. n - k) N" |
1791 shows "inj_on (\<lambda>n. n - k) N" |
1758 proof (rule inj_onI) |
1792 proof (rule inj_onI) |
1759 fix x y |
1793 fix x y |
1760 assume a: "x \<in> N" "y \<in> N" "x - k = y - k" |
1794 assume a: "x \<in> N" "y \<in> N" "x - k = y - k" |
1761 with k_le_n have "x - k + k = y - k + k" by auto |
1795 with k_le_n have "x - k + k = y - k + k" by auto |
1762 with a k_le_n show "x = y" by auto |
1796 with a k_le_n show "x = y" by (auto simp add: eq_diff_iff) |
1763 qed |
1797 qed |
1764 |
1798 |
1765 text\<open>Rewriting to pull differences out\<close> |
1799 text\<open>Rewriting to pull differences out\<close> |
1766 |
1800 |
1767 lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j" |
1801 lemma diff_diff_right [simp]: |
1768 by arith |
1802 fixes i j k :: nat |
1769 |
1803 shows "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j" |
1770 lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j" |
1804 by (fact diff_diff_right) |
1771 by arith |
1805 |
1772 |
1806 lemma diff_Suc_diff_eq1 [simp]: |
1773 lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)" |
1807 assumes "k \<le> j" |
1774 by arith |
1808 shows "i - Suc (j - k) = i + k - Suc j" |
1775 |
1809 proof - |
1776 lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n" |
1810 from assms have *: "Suc (j - k) = Suc j - k" |
1777 by simp |
1811 by (simp add: Suc_diff_le) |
1778 |
1812 from assms have "k \<le> Suc j" |
1779 (*The others are |
1813 by (rule order_trans) simp |
1780 i - j - k = i - (j + k), |
1814 with diff_diff_right [of k "Suc j" i] * show ?thesis |
1781 k \<le> j ==> j - k + i = j + i - k, |
1815 by simp |
1782 k \<le> j ==> i + (j - k) = i + j - k *) |
1816 qed |
1783 lemmas add_diff_assoc = diff_add_assoc [symmetric] |
1817 |
1784 lemmas add_diff_assoc2 = diff_add_assoc2[symmetric] |
1818 lemma diff_Suc_diff_eq2 [simp]: |
1785 declare add_diff_assoc [simp] add_diff_assoc2[simp] |
1819 assumes "k \<le> j" |
1786 |
1820 shows "Suc (j - k) - i = Suc j - (k + i)" |
1787 text\<open>At present we prove no analogue of \<open>not_less_Least\<close> or \<open>Least_Suc\<close>, since there appears to be no need.\<close> |
1821 proof - |
1788 |
1822 from assms obtain n where "j = k + n" |
1789 text\<open>Lemmas for ex/Factorization\<close> |
1823 by (auto dest: le_Suc_ex) |
1790 |
1824 moreover have "Suc n - i = (k + Suc n) - (k + i)" |
1791 lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n" |
1825 using add_diff_cancel_left [of k "Suc n" i] by simp |
1792 by (cases m) auto |
1826 ultimately show ?thesis by simp |
1793 |
1827 qed |
1794 lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n" |
1828 |
1795 by (cases m) auto |
1829 lemma Suc_diff_Suc: |
1796 |
1830 assumes "n < m" |
1797 lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m" |
1831 shows "Suc (m - Suc n) = m - n" |
1798 by (cases m) auto |
1832 proof - |
|
1833 from assms obtain q where "m = n + Suc q" |
|
1834 by (auto dest: less_imp_Suc_add) |
|
1835 moreover def r \<equiv> "Suc q" |
|
1836 ultimately have "Suc (m - Suc n) = r" and "m = n + r" |
|
1837 by simp_all |
|
1838 then show ?thesis by simp |
|
1839 qed |
|
1840 |
|
1841 lemma one_less_mult: |
|
1842 "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n" |
|
1843 using less_1_mult [of n m] by (simp add: ac_simps) |
|
1844 |
|
1845 lemma n_less_m_mult_n: |
|
1846 "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n" |
|
1847 using mult_strict_right_mono [of 1 m n] by simp |
|
1848 |
|
1849 lemma n_less_n_mult_m: |
|
1850 "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m" |
|
1851 using mult_strict_left_mono [of 1 m n] by simp |
1799 |
1852 |
1800 text \<open>Specialized induction principles that work "backwards":\<close> |
1853 text \<open>Specialized induction principles that work "backwards":\<close> |
1801 |
1854 |
1802 lemma inc_induct[consumes 1, case_names base step]: |
1855 lemma inc_induct [consumes 1, case_names base step]: |
1803 assumes less: "i \<le> j" |
1856 assumes less: "i \<le> j" |
1804 assumes base: "P j" |
1857 assumes base: "P j" |
1805 assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n" |
1858 assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n" |
1806 shows "P i" |
1859 shows "P i" |
1807 using less step |
1860 using less step |
1808 proof (induct d\<equiv>"j - i" arbitrary: i) |
1861 proof (induct "j - i" arbitrary: i) |
1809 case (0 i) |
1862 case (0 i) |
1810 hence "i = j" by simp |
1863 then have "i = j" by simp |
1811 with base show ?case by simp |
1864 with base show ?case by simp |
1812 next |
1865 next |
1813 case (Suc d n) |
1866 case (Suc d n) |
1814 hence "n \<le> n" "n < j" "P (Suc n)" |
1867 from Suc.hyps have "n \<noteq> j" by auto |
1815 by simp_all |
1868 with Suc have "n < j" by (simp add: less_le) |
1816 then show "P n" by fact |
1869 from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp |
1817 qed |
1870 then have "d + 1 - 1 = j - n - 1" by simp |
1818 |
1871 then have "d = j - n - 1" by simp |
1819 lemma strict_inc_induct[consumes 1, case_names base step]: |
1872 then have "d = j - (n + 1)" |
|
1873 by (simp add: diff_diff_eq) |
|
1874 then have "d = j - Suc n" |
|
1875 by simp |
|
1876 moreover from \<open>n < j\<close> have "Suc n \<le> j" |
|
1877 by (simp add: Suc_le_eq) |
|
1878 ultimately have "P (Suc n)" |
|
1879 thm Suc.hyps TrueI Suc.prems |
|
1880 proof (rule Suc.hyps) |
|
1881 fix q |
|
1882 assume "Suc n \<le> q" |
|
1883 then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le) |
|
1884 moreover assume "q < j" |
|
1885 moreover assume "P (Suc q)" |
|
1886 ultimately show "P q" |
|
1887 by (rule Suc.prems) |
|
1888 qed |
|
1889 with order_refl \<open>n < j\<close> show "P n" |
|
1890 by (rule Suc.prems) |
|
1891 qed |
|
1892 |
|
1893 lemma strict_inc_induct [consumes 1, case_names base step]: |
1820 assumes less: "i < j" |
1894 assumes less: "i < j" |
1821 assumes base: "!!i. j = Suc i ==> P i" |
1895 assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i" |
1822 assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i" |
1896 assumes step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i" |
1823 shows "P i" |
1897 shows "P i" |
1824 using less |
1898 using less proof (induct "j - i - 1" arbitrary: i) |
1825 proof (induct d=="j - i - 1" arbitrary: i) |
|
1826 case (0 i) |
1899 case (0 i) |
1827 with \<open>i < j\<close> have "j = Suc i" by simp |
1900 from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0" |
|
1901 by (auto dest!: less_imp_Suc_add) |
|
1902 with 0 have "j = Suc i" |
|
1903 by (auto intro: order_antisym simp add: Suc_le_eq) |
1828 with base show ?case by simp |
1904 with base show ?case by simp |
1829 next |
1905 next |
1830 case (Suc d i) |
1906 case (Suc d i) |
1831 hence "i < j" "P (Suc i)" |
1907 from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i" |
1832 by simp_all |
1908 by (simp add: diff_diff_add) |
1833 thus "P i" by (rule step) |
1909 then have "Suc d - 1 = j - Suc i - 1" |
|
1910 by simp |
|
1911 then have "d = j - Suc i - 1" |
|
1912 by simp |
|
1913 moreover from * have "j - Suc i \<noteq> 0" |
|
1914 by auto |
|
1915 then have "Suc i < j" |
|
1916 by (simp add: not_le) |
|
1917 ultimately have "P (Suc i)" |
|
1918 by (rule Suc.hyps) |
|
1919 with \<open>i < j\<close> show "P i" by (rule step) |
1834 qed |
1920 qed |
1835 |
1921 |
1836 lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)" |
1922 lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)" |
1837 using inc_induct[of "k - i" k P, simplified] by blast |
1923 using inc_induct[of "k - i" k P, simplified] by blast |
1838 |
1924 |
1839 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" |
1925 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" |
1840 using inc_induct[of 0 k P] by blast |
1926 using inc_induct[of 0 k P] by blast |
1841 |
1927 |
1842 text \<open>Further induction rule similar to @{thm inc_induct}\<close> |
1928 text \<open>Further induction rule similar to @{thm inc_induct}\<close> |
1843 |
1929 |
1844 lemma dec_induct[consumes 1, case_names base step]: |
1930 lemma dec_induct [consumes 1, case_names base step]: |
1845 "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j" |
1931 "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j" |
1846 by (induct j arbitrary: i) (auto simp: le_Suc_eq) |
1932 proof (induct j arbitrary: i) |
|
1933 case 0 then show ?case by simp |
|
1934 next |
|
1935 case (Suc j) |
|
1936 from Suc.prems have "i \<le> j \<or> i = Suc j" |
|
1937 by (simp add: le_Suc_eq) |
|
1938 then show ?case proof |
|
1939 assume "i \<le> j" |
|
1940 moreover have "j < Suc j" by simp |
|
1941 moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close> |
|
1942 proof (rule Suc.hyps) |
|
1943 fix q |
|
1944 assume "i \<le> q" |
|
1945 moreover assume "q < j" then have "q < Suc j" |
|
1946 by (simp add: less_Suc_eq) |
|
1947 moreover assume "P q" |
|
1948 ultimately show "P (Suc q)" |
|
1949 by (rule Suc.prems) |
|
1950 qed |
|
1951 ultimately show "P (Suc j)" |
|
1952 by (rule Suc.prems) |
|
1953 next |
|
1954 assume "i = Suc j" |
|
1955 with \<open>P i\<close> show "P (Suc j)" by simp |
|
1956 qed |
|
1957 qed |
|
1958 |
1847 |
1959 |
1848 subsection \<open> Monotonicity of funpow \<close> |
1960 subsection \<open> Monotonicity of funpow \<close> |
1849 |
1961 |
1850 lemma funpow_increasing: |
1962 lemma funpow_increasing: |
1851 fixes f :: "'a \<Rightarrow> ('a::{lattice, order_top})" |
1963 fixes f :: "'a \<Rightarrow> ('a::{lattice, order_top})" |