2177 with `d = a * k` show "a dvd (x + t)" by simp |
2177 with `d = a * k` show "a dvd (x + t)" by simp |
2178 qed |
2178 qed |
2179 qed |
2179 qed |
2180 |
2180 |
2181 |
2181 |
|
2182 subsection {* Finiteness of intervals *} |
|
2183 |
|
2184 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}" |
|
2185 proof (cases "a <= b") |
|
2186 case True |
|
2187 from this show ?thesis |
|
2188 proof (induct b rule: int_ge_induct) |
|
2189 case base |
|
2190 have "{i. a <= i & i <= a} = {a}" by auto |
|
2191 from this show ?case by simp |
|
2192 next |
|
2193 case (step b) |
|
2194 from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto |
|
2195 from this step show ?case by simp |
|
2196 qed |
|
2197 next |
|
2198 case False from this show ?thesis |
|
2199 by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans) |
|
2200 qed |
|
2201 |
|
2202 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}" |
|
2203 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto |
|
2204 |
|
2205 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}" |
|
2206 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto |
|
2207 |
|
2208 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}" |
|
2209 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto |
|
2210 |
|
2211 |
2182 subsection {* Configuration of the code generator *} |
2212 subsection {* Configuration of the code generator *} |
2183 |
2213 |
2184 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int" |
2214 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int" |
2185 |
2215 |
2186 lemmas pred_succ_numeral_code [code] = |
2216 lemmas pred_succ_numeral_code [code] = |