1982 by auto |
1982 by auto |
1983 |
1983 |
1984 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard] |
1984 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard] |
1985 |
1985 |
1986 |
1986 |
|
1987 subsection {* The divides relation *} |
|
1988 |
|
1989 lemma zdvd_anti_sym: |
|
1990 "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" |
|
1991 apply (simp add: dvd_def, auto) |
|
1992 apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) |
|
1993 done |
|
1994 |
|
1995 lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" |
|
1996 shows "\<bar>a\<bar> = \<bar>b\<bar>" |
|
1997 proof- |
|
1998 from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast |
|
1999 from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast |
|
2000 from k k' have "a = a*k*k'" by simp |
|
2001 with mult_cancel_left1[where c="a" and b="k*k'"] |
|
2002 have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc) |
|
2003 hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff) |
|
2004 thus ?thesis using k k' by auto |
|
2005 qed |
|
2006 |
|
2007 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" |
|
2008 apply (subgoal_tac "m = n + (m - n)") |
|
2009 apply (erule ssubst) |
|
2010 apply (blast intro: dvd_add, simp) |
|
2011 done |
|
2012 |
|
2013 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" |
|
2014 apply (rule iffI) |
|
2015 apply (erule_tac [2] dvd_add) |
|
2016 apply (subgoal_tac "n = (n + k * m) - k * m") |
|
2017 apply (erule ssubst) |
|
2018 apply (erule dvd_diff) |
|
2019 apply(simp_all) |
|
2020 done |
|
2021 |
|
2022 lemma dvd_imp_le_int: |
|
2023 fixes d i :: int |
|
2024 assumes "i \<noteq> 0" and "d dvd i" |
|
2025 shows "\<bar>d\<bar> \<le> \<bar>i\<bar>" |
|
2026 proof - |
|
2027 from `d dvd i` obtain k where "i = d * k" .. |
|
2028 with `i \<noteq> 0` have "k \<noteq> 0" by auto |
|
2029 then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto |
|
2030 then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono) |
|
2031 with `i = d * k` show ?thesis by (simp add: abs_mult) |
|
2032 qed |
|
2033 |
|
2034 lemma zdvd_not_zless: |
|
2035 fixes m n :: int |
|
2036 assumes "0 < m" and "m < n" |
|
2037 shows "\<not> n dvd m" |
|
2038 proof |
|
2039 from assms have "0 < n" by auto |
|
2040 assume "n dvd m" then obtain k where k: "m = n * k" .. |
|
2041 with `0 < m` have "0 < n * k" by auto |
|
2042 with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff) |
|
2043 with k `0 < n` `m < n` have "n * k < n * 1" by simp |
|
2044 with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto |
|
2045 qed |
|
2046 |
|
2047 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)" |
|
2048 shows "m dvd n" |
|
2049 proof- |
|
2050 from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast |
|
2051 {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp |
|
2052 with h have False by (simp add: mult_assoc)} |
|
2053 hence "n = m * h" by blast |
|
2054 thus ?thesis by simp |
|
2055 qed |
|
2056 |
|
2057 theorem zdvd_int: "(x dvd y) = (int x dvd int y)" |
|
2058 proof - |
|
2059 have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y" |
|
2060 proof - |
|
2061 fix k |
|
2062 assume A: "int y = int x * k" |
|
2063 then show "x dvd y" proof (cases k) |
|
2064 case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) |
|
2065 then show ?thesis .. |
|
2066 next |
|
2067 case (2 n) with A have "int y = int x * (- int (Suc n))" by simp |
|
2068 also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right) |
|
2069 also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) |
|
2070 finally have "- int (x * Suc n) = int y" .. |
|
2071 then show ?thesis by (simp only: negative_eq_positive) auto |
|
2072 qed |
|
2073 qed |
|
2074 then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) |
|
2075 qed |
|
2076 |
|
2077 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" |
|
2078 proof |
|
2079 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp |
|
2080 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) |
|
2081 hence "nat \<bar>x\<bar> = 1" by simp |
|
2082 thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto) |
|
2083 next |
|
2084 assume "\<bar>x\<bar>=1" |
|
2085 then have "x = 1 \<or> x = -1" by auto |
|
2086 then show "x dvd 1" by (auto intro: dvdI) |
|
2087 qed |
|
2088 |
|
2089 lemma zdvd_mult_cancel1: |
|
2090 assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" |
|
2091 proof |
|
2092 assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" |
|
2093 by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff) |
|
2094 next |
|
2095 assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp |
|
2096 from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) |
|
2097 qed |
|
2098 |
|
2099 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" |
|
2100 unfolding zdvd_int by (cases "z \<ge> 0") simp_all |
|
2101 |
|
2102 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" |
|
2103 unfolding zdvd_int by (cases "z \<ge> 0") simp_all |
|
2104 |
|
2105 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" |
|
2106 by (auto simp add: dvd_int_iff) |
|
2107 |
|
2108 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)" |
|
2109 apply (rule_tac z=n in int_cases) |
|
2110 apply (auto simp add: dvd_int_iff) |
|
2111 apply (rule_tac z=z in int_cases) |
|
2112 apply (auto simp add: dvd_imp_le) |
|
2113 done |
|
2114 |
|
2115 |
1987 subsection {* Configuration of the code generator *} |
2116 subsection {* Configuration of the code generator *} |
1988 |
2117 |
1989 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int" |
2118 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int" |
1990 |
2119 |
1991 lemmas pred_succ_numeral_code [code] = |
2120 lemmas pred_succ_numeral_code [code] = |