1197 by auto |
1194 by auto |
1198 |
1195 |
1199 |
1196 |
1200 subsubsection {* Simplification of arithmetic operations on integer constants. *} |
1197 subsubsection {* Simplification of arithmetic operations on integer constants. *} |
1201 |
1198 |
1202 lemmas arith_extra_simps [standard, simp] = |
1199 lemmas arith_extra_simps [simp] = |
1203 number_of_add [symmetric] |
1200 number_of_add [symmetric] |
1204 number_of_minus [symmetric] |
1201 number_of_minus [symmetric] |
1205 numeral_m1_eq_minus_1 [symmetric] |
1202 numeral_m1_eq_minus_1 [symmetric] |
1206 number_of_mult [symmetric] |
1203 number_of_mult [symmetric] |
1207 diff_number_of_eq abs_number_of |
1204 diff_number_of_eq abs_number_of |
1208 |
1205 |
1209 text {* |
1206 text {* |
1210 For making a minimal simpset, one must include these default simprules. |
1207 For making a minimal simpset, one must include these default simprules. |
1211 Also include @{text simp_thms}. |
1208 Also include @{text simp_thms}. |
1212 *} |
1209 *} |
1463 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)" |
1460 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)" |
1464 by (rule semiring_one_add_one_is_two) |
1461 by (rule semiring_one_add_one_is_two) |
1465 |
1462 |
1466 lemmas add_special = |
1463 lemmas add_special = |
1467 one_add_one_is_two |
1464 one_add_one_is_two |
1468 binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard] |
1465 binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl] |
1469 binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard] |
1466 binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1] |
1470 |
1467 |
1471 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*} |
1468 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*} |
1472 lemmas diff_special = |
1469 lemmas diff_special = |
1473 binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard] |
1470 binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl] |
1474 binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard] |
1471 binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1] |
1475 |
1472 |
1476 text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
1473 text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
1477 lemmas eq_special = |
1474 lemmas eq_special = |
1478 binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard] |
1475 binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl] |
1479 binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard] |
1476 binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl] |
1480 binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard] |
1477 binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0] |
1481 binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard] |
1478 binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1] |
1482 |
1479 |
1483 text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
1480 text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
1484 lemmas less_special = |
1481 lemmas less_special = |
1485 binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard] |
1482 binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl] |
1486 binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard] |
1483 binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl] |
1487 binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard] |
1484 binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0] |
1488 binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard] |
1485 binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1] |
1489 |
1486 |
1490 text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
1487 text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
1491 lemmas le_special = |
1488 lemmas le_special = |
1492 binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard] |
1489 binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl] |
1493 binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard] |
1490 binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl] |
1494 binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard] |
1491 binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0] |
1495 binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard] |
1492 binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1] |
1496 |
1493 |
1497 lemmas arith_special[simp] = |
1494 lemmas arith_special[simp] = |
1498 add_special diff_special eq_special less_special le_special |
1495 add_special diff_special eq_special less_special le_special |
1499 |
1496 |
1500 |
1497 |
1893 |
1890 |
1894 subsubsection{*Special Simplification for Constants*} |
1891 subsubsection{*Special Simplification for Constants*} |
1895 |
1892 |
1896 text{*These distributive laws move literals inside sums and differences.*} |
1893 text{*These distributive laws move literals inside sums and differences.*} |
1897 |
1894 |
1898 lemmas left_distrib_number_of [simp] = |
1895 lemmas left_distrib_number_of [simp] = left_distrib [of _ _ "number_of v"] for v |
1899 left_distrib [of _ _ "number_of v", standard] |
1896 lemmas right_distrib_number_of [simp] = right_distrib [of "number_of v"] for v |
1900 |
1897 lemmas left_diff_distrib_number_of [simp] = left_diff_distrib [of _ _ "number_of v"] for v |
1901 lemmas right_distrib_number_of [simp] = |
1898 lemmas right_diff_distrib_number_of [simp] = right_diff_distrib [of "number_of v"] for v |
1902 right_distrib [of "number_of v", standard] |
|
1903 |
|
1904 lemmas left_diff_distrib_number_of [simp] = |
|
1905 left_diff_distrib [of _ _ "number_of v", standard] |
|
1906 |
|
1907 lemmas right_diff_distrib_number_of [simp] = |
|
1908 right_diff_distrib [of "number_of v", standard] |
|
1909 |
1899 |
1910 text{*These are actually for fields, like real: but where else to put them?*} |
1900 text{*These are actually for fields, like real: but where else to put them?*} |
1911 |
1901 |
1912 lemmas zero_less_divide_iff_number_of [simp, no_atp] = |
1902 lemmas zero_less_divide_iff_number_of [simp, no_atp] = zero_less_divide_iff [of "number_of w"] for w |
1913 zero_less_divide_iff [of "number_of w", standard] |
1903 lemmas divide_less_0_iff_number_of [simp, no_atp] = divide_less_0_iff [of "number_of w"] for w |
1914 |
1904 lemmas zero_le_divide_iff_number_of [simp, no_atp] = zero_le_divide_iff [of "number_of w"] for w |
1915 lemmas divide_less_0_iff_number_of [simp, no_atp] = |
1905 lemmas divide_le_0_iff_number_of [simp, no_atp] = divide_le_0_iff [of "number_of w"] for w |
1916 divide_less_0_iff [of "number_of w", standard] |
|
1917 |
|
1918 lemmas zero_le_divide_iff_number_of [simp, no_atp] = |
|
1919 zero_le_divide_iff [of "number_of w", standard] |
|
1920 |
|
1921 lemmas divide_le_0_iff_number_of [simp, no_atp] = |
|
1922 divide_le_0_iff [of "number_of w", standard] |
|
1923 |
1906 |
1924 |
1907 |
1925 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks |
1908 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks |
1926 strange, but then other simprocs simplify the quotient.*} |
1909 strange, but then other simprocs simplify the quotient.*} |
1927 |
1910 |
1928 lemmas inverse_eq_divide_number_of [simp] = |
1911 lemmas inverse_eq_divide_number_of [simp] = inverse_eq_divide [of "number_of w"] for w |
1929 inverse_eq_divide [of "number_of w", standard] |
|
1930 |
1912 |
1931 text {*These laws simplify inequalities, moving unary minus from a term |
1913 text {*These laws simplify inequalities, moving unary minus from a term |
1932 into the literal.*} |
1914 into the literal.*} |
1933 |
1915 |
1934 lemmas less_minus_iff_number_of [simp, no_atp] = |
1916 lemmas less_minus_iff_number_of [simp, no_atp] = less_minus_iff [of "number_of v"] for v |
1935 less_minus_iff [of "number_of v", standard] |
1917 lemmas le_minus_iff_number_of [simp, no_atp] = le_minus_iff [of "number_of v"] for v |
1936 |
1918 lemmas equation_minus_iff_number_of [simp, no_atp] = equation_minus_iff [of "number_of v"] for v |
1937 lemmas le_minus_iff_number_of [simp, no_atp] = |
1919 lemmas minus_less_iff_number_of [simp, no_atp] = minus_less_iff [of _ "number_of v"] for v |
1938 le_minus_iff [of "number_of v", standard] |
1920 lemmas minus_le_iff_number_of [simp, no_atp] = minus_le_iff [of _ "number_of v"] for v |
1939 |
1921 lemmas minus_equation_iff_number_of [simp, no_atp] = minus_equation_iff [of _ "number_of v"] for v |
1940 lemmas equation_minus_iff_number_of [simp, no_atp] = |
|
1941 equation_minus_iff [of "number_of v", standard] |
|
1942 |
|
1943 lemmas minus_less_iff_number_of [simp, no_atp] = |
|
1944 minus_less_iff [of _ "number_of v", standard] |
|
1945 |
|
1946 lemmas minus_le_iff_number_of [simp, no_atp] = |
|
1947 minus_le_iff [of _ "number_of v", standard] |
|
1948 |
|
1949 lemmas minus_equation_iff_number_of [simp, no_atp] = |
|
1950 minus_equation_iff [of _ "number_of v", standard] |
|
1951 |
|
1952 |
1922 |
1953 text{*To Simplify Inequalities Where One Side is the Constant 1*} |
1923 text{*To Simplify Inequalities Where One Side is the Constant 1*} |
1954 |
1924 |
1955 lemma less_minus_iff_1 [simp,no_atp]: |
1925 lemma less_minus_iff_1 [simp,no_atp]: |
1956 fixes b::"'b::{linordered_idom,number_ring}" |
1926 fixes b::"'b::{linordered_idom,number_ring}" |
1983 by (subst minus_equation_iff, auto) |
1953 by (subst minus_equation_iff, auto) |
1984 |
1954 |
1985 |
1955 |
1986 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *} |
1956 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *} |
1987 |
1957 |
1988 lemmas mult_less_cancel_left_number_of [simp, no_atp] = |
1958 lemmas mult_less_cancel_left_number_of [simp, no_atp] = mult_less_cancel_left [of "number_of v"] for v |
1989 mult_less_cancel_left [of "number_of v", standard] |
1959 lemmas mult_less_cancel_right_number_of [simp, no_atp] = mult_less_cancel_right [of _ "number_of v"] for v |
1990 |
1960 lemmas mult_le_cancel_left_number_of [simp, no_atp] = mult_le_cancel_left [of "number_of v"] for v |
1991 lemmas mult_less_cancel_right_number_of [simp, no_atp] = |
1961 lemmas mult_le_cancel_right_number_of [simp, no_atp] = mult_le_cancel_right [of _ "number_of v"] for v |
1992 mult_less_cancel_right [of _ "number_of v", standard] |
|
1993 |
|
1994 lemmas mult_le_cancel_left_number_of [simp, no_atp] = |
|
1995 mult_le_cancel_left [of "number_of v", standard] |
|
1996 |
|
1997 lemmas mult_le_cancel_right_number_of [simp, no_atp] = |
|
1998 mult_le_cancel_right [of _ "number_of v", standard] |
|
1999 |
1962 |
2000 |
1963 |
2001 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *} |
1964 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *} |
2002 |
1965 |
2003 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard] |
1966 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w"] for w |
2004 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard] |
1967 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w"] for w |
2005 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard] |
1968 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w"] for w |
2006 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard] |
1969 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w"] for w |
2007 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard] |
1970 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w"] for w |
2008 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard] |
1971 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w"] for w |
2009 |
1972 |
2010 |
1973 |
2011 subsubsection{*Optional Simplification Rules Involving Constants*} |
1974 subsubsection{*Optional Simplification Rules Involving Constants*} |
2012 |
1975 |
2013 text{*Simplify quotients that are compared with a literal constant.*} |
1976 text{*Simplify quotients that are compared with a literal constant.*} |
2014 |
1977 |
2015 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] |
1978 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w"] for w |
2016 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] |
1979 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w"] for w |
2017 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] |
1980 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w"] for w |
2018 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] |
1981 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w"] for w |
2019 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] |
1982 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w"] for w |
2020 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] |
1983 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w"] for w |
2021 |
1984 |
2022 |
1985 |
2023 text{*Not good as automatic simprules because they cause case splits.*} |
1986 text{*Not good as automatic simprules because they cause case splits.*} |
2024 lemmas divide_const_simps = |
1987 lemmas divide_const_simps = |
2025 le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of |
1988 le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of |
2357 |
2320 |
2358 lemmas inj_int = inj_of_nat [where 'a=int] |
2321 lemmas inj_int = inj_of_nat [where 'a=int] |
2359 lemmas zadd_int = of_nat_add [where 'a=int, symmetric] |
2322 lemmas zadd_int = of_nat_add [where 'a=int, symmetric] |
2360 lemmas int_mult = of_nat_mult [where 'a=int] |
2323 lemmas int_mult = of_nat_mult [where 'a=int] |
2361 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric] |
2324 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric] |
2362 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard] |
2325 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n |
2363 lemmas zless_int = of_nat_less_iff [where 'a=int] |
2326 lemmas zless_int = of_nat_less_iff [where 'a=int] |
2364 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard] |
2327 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k |
2365 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int] |
2328 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int] |
2366 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int] |
2329 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int] |
2367 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard] |
2330 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n |
2368 lemmas int_0 = of_nat_0 [where 'a=int] |
2331 lemmas int_0 = of_nat_0 [where 'a=int] |
2369 lemmas int_1 = of_nat_1 [where 'a=int] |
2332 lemmas int_1 = of_nat_1 [where 'a=int] |
2370 lemmas int_Suc = of_nat_Suc [where 'a=int] |
2333 lemmas int_Suc = of_nat_Suc [where 'a=int] |
2371 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard] |
2334 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m |
2372 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int] |
2335 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int] |
2373 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric] |
2336 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric] |
2374 |
2337 |
2375 lemma zpower_zpower: |
2338 lemma zpower_zpower: |
2376 "(x ^ y) ^ z = (x ^ (y * z)::int)" |
2339 "(x ^ y) ^ z = (x ^ (y * z)::int)" |