1795 |
1795 |
1796 lemmas zpower_int = int_power [symmetric] |
1796 lemmas zpower_int = int_power [symmetric] |
1797 |
1797 |
1798 subsection {* Configuration of the code generator *} |
1798 subsection {* Configuration of the code generator *} |
1799 |
1799 |
1800 instance int :: eq .. |
|
1801 |
|
1802 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int" |
1800 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int" |
|
1801 |
|
1802 lemmas pred_succ_numeral_code [code func] = |
|
1803 pred_bin_simps succ_bin_simps |
|
1804 |
|
1805 lemmas plus_numeral_code [code func] = |
|
1806 add_bin_simps |
|
1807 arith_extra_simps(1) [where 'a = int] |
|
1808 |
|
1809 lemmas minus_numeral_code [code func] = |
|
1810 minus_bin_simps |
|
1811 arith_extra_simps(2) [where 'a = int] |
|
1812 arith_extra_simps(5) [where 'a = int] |
|
1813 |
|
1814 lemmas times_numeral_code [code func] = |
|
1815 mult_bin_simps |
|
1816 arith_extra_simps(4) [where 'a = int] |
|
1817 |
|
1818 instantiation int :: eq |
|
1819 begin |
|
1820 |
|
1821 definition [code func del]: "eq k l \<longleftrightarrow> k - l = (0\<Colon>int)" |
|
1822 |
|
1823 instance by default (simp add: eq_int_def) |
|
1824 |
|
1825 end |
|
1826 |
|
1827 lemma eq_number_of_int_code [code func]: |
|
1828 "eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq k l" |
|
1829 unfolding eq_int_def number_of_is_id .. |
|
1830 |
|
1831 lemma eq_int_code [code func]: |
|
1832 "eq Int.Pls Int.Pls \<longleftrightarrow> True" |
|
1833 "eq Int.Pls Int.Min \<longleftrightarrow> False" |
|
1834 "eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq Int.Pls k2" |
|
1835 "eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False" |
|
1836 "eq Int.Min Int.Pls \<longleftrightarrow> False" |
|
1837 "eq Int.Min Int.Min \<longleftrightarrow> True" |
|
1838 "eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False" |
|
1839 "eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq Int.Min k2" |
|
1840 "eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq Int.Pls k1" |
|
1841 "eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False" |
|
1842 "eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False" |
|
1843 "eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq Int.Min k1" |
|
1844 "eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq k1 k2" |
|
1845 "eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False" |
|
1846 "eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False" |
|
1847 "eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq k1 k2" |
|
1848 unfolding eq_number_of_int_code [symmetric, of Int.Pls] |
|
1849 eq_number_of_int_code [symmetric, of Int.Min] |
|
1850 eq_number_of_int_code [symmetric, of "Int.Bit0 k1"] |
|
1851 eq_number_of_int_code [symmetric, of "Int.Bit1 k1"] |
|
1852 eq_number_of_int_code [symmetric, of "Int.Bit0 k2"] |
|
1853 eq_number_of_int_code [symmetric, of "Int.Bit1 k2"] |
|
1854 by (simp_all add: eq Pls_def, |
|
1855 simp_all only: Min_def succ_def pred_def number_of_is_id) |
|
1856 (auto simp add: iszero_def) |
|
1857 |
|
1858 lemma less_eq_number_of_int_code [code func]: |
|
1859 "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l" |
|
1860 unfolding number_of_is_id .. |
|
1861 |
|
1862 lemma less_eq_int_code [code func]: |
|
1863 "Int.Pls \<le> Int.Pls \<longleftrightarrow> True" |
|
1864 "Int.Pls \<le> Int.Min \<longleftrightarrow> False" |
|
1865 "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k" |
|
1866 "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k" |
|
1867 "Int.Min \<le> Int.Pls \<longleftrightarrow> True" |
|
1868 "Int.Min \<le> Int.Min \<longleftrightarrow> True" |
|
1869 "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k" |
|
1870 "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k" |
|
1871 "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls" |
|
1872 "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls" |
|
1873 "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min" |
|
1874 "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min" |
|
1875 "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2" |
|
1876 "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2" |
|
1877 "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2" |
|
1878 "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2" |
|
1879 unfolding less_eq_number_of_int_code [symmetric, of Int.Pls] |
|
1880 less_eq_number_of_int_code [symmetric, of Int.Min] |
|
1881 less_eq_number_of_int_code [symmetric, of "Int.Bit0 k1"] |
|
1882 less_eq_number_of_int_code [symmetric, of "Int.Bit1 k1"] |
|
1883 less_eq_number_of_int_code [symmetric, of "Int.Bit0 k2"] |
|
1884 less_eq_number_of_int_code [symmetric, of "Int.Bit1 k2"] |
|
1885 by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id) |
|
1886 (auto simp add: neg_def linorder_not_less group_simps |
|
1887 zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def) |
|
1888 |
|
1889 lemma less_number_of_int_code [code func]: |
|
1890 "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l" |
|
1891 unfolding number_of_is_id .. |
|
1892 |
|
1893 lemma less_int_code [code func]: |
|
1894 "Int.Pls < Int.Pls \<longleftrightarrow> False" |
|
1895 "Int.Pls < Int.Min \<longleftrightarrow> False" |
|
1896 "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k" |
|
1897 "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k" |
|
1898 "Int.Min < Int.Pls \<longleftrightarrow> True" |
|
1899 "Int.Min < Int.Min \<longleftrightarrow> False" |
|
1900 "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k" |
|
1901 "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k" |
|
1902 "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls" |
|
1903 "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls" |
|
1904 "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min" |
|
1905 "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min" |
|
1906 "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2" |
|
1907 "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2" |
|
1908 "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2" |
|
1909 "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2" |
|
1910 unfolding less_number_of_int_code [symmetric, of Int.Pls] |
|
1911 less_number_of_int_code [symmetric, of Int.Min] |
|
1912 less_number_of_int_code [symmetric, of "Int.Bit0 k1"] |
|
1913 less_number_of_int_code [symmetric, of "Int.Bit1 k1"] |
|
1914 less_number_of_int_code [symmetric, of "Int.Bit0 k2"] |
|
1915 less_number_of_int_code [symmetric, of "Int.Bit1 k2"] |
|
1916 by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id) |
|
1917 (auto simp add: neg_def group_simps zle_add1_eq_le [symmetric] del: iffI, |
|
1918 auto simp only: Bit0_def Bit1_def) |
1803 |
1919 |
1804 definition |
1920 definition |
1805 int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where |
1921 int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where |
1806 [code func del]: "int_aux = of_nat_aux" |
1922 [code func del]: "int_aux = of_nat_aux" |
1807 |
1923 |