1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory More_Numeral_Type 8 imports "Word_Lib.WordSetup" 9begin 10 11(* This theory provides additional setup for numeral types, which should probably go into 12 Numeral_Type in the distribution at some point. *) 13 14text \<open> 15 The function package uses @{const size} for guessing termination measures. 16 Using @{const size} also provides a convenient cast to natural numbers. 17\<close> 18 19instantiation num1 :: size 20begin 21 definition size_num1 where [simp, code]: "size (n::num1) = 0" 22 instance .. 23end 24 25instantiation bit0 and bit1 :: (finite) size 26begin 27 definition size_bit0 where [code]: "size n = nat (Rep_bit0 n)" 28 definition size_bit1 where [code]: "size n = nat (Rep_bit1 n)" 29 instance .. 30end 31 32(* As in the parent theory Numeral_Type, we first prove everything abstractly to avoid duplication, 33 and then instantiate bit0 and bit1. *) 34locale mod_size_order = mod_ring n Rep Abs 35 for n :: int 36 and Rep :: "'a::{comm_ring_1,size,linorder} \<Rightarrow> int" 37 and Abs :: "int \<Rightarrow> 'a::{comm_ring_1,size,linorder}" + 38 assumes size_def: "size x = nat (Rep x)" 39 assumes less_def: "(a < b) = (Rep a < Rep b)" 40 assumes less_eq_def: "(a \<le> b) = (Rep a \<le> Rep b)" 41begin 42 43text \<open> 44 Automatic simplification of concrete @{term "(<)"} and @{term "(<=)"} goals on numeral types. 45\<close> 46lemmas order_numeral[simp] = 47 less_def[of "numeral a" "numeral b" for a b] 48 less_eq_def[of "numeral a" "numeral b" for a b] 49 less_def[of "0" "numeral b" for b] 50 less_def[of "1" "numeral b" for b] 51 less_eq_def[of "0" "numeral b" for b] 52 less_eq_def[of "1" "numeral b" for b] 53 less_def[of "numeral a" "0" for a] 54 less_def[of "numeral a" "1" for a] 55 less_eq_def[of "numeral a" "0" for a] 56 less_eq_def[of "numeral a" "1" for a] 57 58text \<open> Simplifying size numerals. \<close> 59lemmas [simp] = Rep_numeral 60lemmas size_numerals[simp] = size_def[of "numeral m" for m] 61 62text \<open> Simplifying representatives of 0 and 1 \<close> 63lemmas [simp] = Rep_0 Rep_1 64 65lemmas definitions = definitions less_def less_eq_def size_def 66 67lemmas Rep = type_definition.Rep[OF type] 68lemmas Abs_cases = type_definition.Abs_cases[OF type] 69 70lemma of_nat_size[simp]: 71 "of_nat (size x) = (x::'a)" 72 by (cases x rule: Abs_cases) (clarsimp simp: Abs_inverse of_int_eq size_def) 73 74lemma size_of_nat[simp]: 75 "size (of_nat x :: 'a) = x mod n" 76 by (simp add: Rep_Abs_mod of_nat_eq size0 size_def) 77 78lemma zero_less_eq[simp]: 79 "0 \<le> (x :: 'a)" 80 using Rep by (simp add: less_eq_def) 81 82lemma zero_less_one[simp,intro!]: 83 "0 < (1::'a)" 84 by (simp add: less_def) 85 86lemma zero_least[simp,intro]: 87 "(x::'a) < y \<Longrightarrow> 0 < y" 88 by (simp add: le_less_trans) 89 90lemma not_less_zero_bit0[simp]: 91 "\<not> (x::'a) < 0" 92 by (simp add: not_less) 93 94lemmas not_less_zeroE[elim!] = notE[OF not_less_zero] 95 96lemma one_leq[simp]: 97 "(1 \<le> x) = (0 < (x::'a))" 98 using less_def less_eq_def by auto 99 100lemma less_eq_0[simp]: 101 "(x \<le> 0) = (x = (0::'a))" 102 by (simp add: antisym) 103 104lemma size_less[simp]: 105 "(size (x::'a) < size y) = (x < y)" 106 by (cases x rule: Abs_cases, cases y rule: Abs_cases) (auto simp: Abs_inverse definitions) 107 108lemma size_inj[simp]: 109 "(size (x::'a) = size y) = (x = y)" 110 by (metis of_nat_size) 111 112lemma size_less_eq[simp]: 113 "(size (x::'a) \<le> size y) = (x \<le> y)" 114 by (auto simp: le_eq_less_or_eq) 115 116lemma size_0[simp]: 117 "size (0::'a) = 0" 118 by (simp add: size_def) 119 120lemma size_1[simp]: 121 "size (1::'a) = 1" 122 by (simp add: size_def) 123 124lemma size_eq_0[simp]: 125 "(size x = 0) = ((x::'a) = 0)" 126 using size_inj by fastforce 127 128lemma minus_less: 129 "\<lbrakk> y \<le> x; 0 < y \<rbrakk> \<Longrightarrow> x - y < (x::'a)" 130 unfolding definitions 131 by (cases x rule: Abs_cases, cases y rule: Abs_cases) (simp add: Abs_inverse) 132 133lemma pred[simp,intro!]: 134 "0 < (x::'a) \<Longrightarrow> x - 1 < x" 135 by (auto intro!: minus_less) 136 137lemma minus1_leq: 138 "\<lbrakk> x - 1 \<le> y; y < x \<rbrakk> \<Longrightarrow> (y::'a) = x-1" 139 by (smt Rep_1 Rep_Abs_mod Rep_less_n less_def diff_def int_mod_ge le_neq_trans) 140 141lemma max_bound_leq[simp,intro!]: 142 "(x::'a) \<le> -1" 143 by (smt Rep_1 Rep_Abs_mod Rep_less_n less_eq_def int_mod_ge' minus_def) 144 145lemma leq_minus1_less: 146 "0 < y \<Longrightarrow> (x \<le> y - 1) = (x < (y::'a))" 147 by (metis le_less less_trans minus1_leq not_less pred) 148 149lemma max_bound_neq_conv[simp]: 150 "(x \<noteq> -1) = ((x::'a) < -1)" 151 using le_neq_trans by auto 152 153lemma max_bound_leq_conv[simp]: 154 "(- 1 \<le> (x::'a)) = (x = - 1)" 155 by (simp add: eq_iff) 156 157lemma max_bound_not_less[simp]: 158 "\<not> -1 < (x::'a)" 159 using minus1_leq by fastforce 160 161lemma minus_1_eq: 162 "(-1::'a) = of_nat (nat n - 1)" 163 unfolding definitions using Rep_Abs_1 of_nat_eq size1 by auto 164 165lemma n_not_less_Rep[simp]: 166 "\<not> n < Rep x" 167 using Rep[of x] by (simp add: not_less) 168 169lemma size_plus: 170 "(x::'a) < x + y \<Longrightarrow> size (x + y) = size x + size y" 171 unfolding definitions Rep_Abs_mod 172 using Rep size0 173 by (simp flip: nat_add_distrib add: eq_nat_nat_iff pos_mod_sign mod_add_if_z split: if_split_asm) 174 175lemma Suc_size[simp]: 176 "(x::'a) < x + 1 \<Longrightarrow> size (x + 1) = Suc (size x)" 177 by (simp add: size_plus) 178 179lemma no_overflow_eq_max_bound: 180 "((x::'a) < x + 1) = (x < -1)" 181 unfolding definitions 182 by (smt Rep_Abs_mod Rep_Abs_1 Rep_less_n int_mod_ge int_mod_ge' size0) 183 184lemma plus_one_leq: 185 "x < y \<Longrightarrow> x + 1 \<le> (y::'a)" 186 by (metis add_diff_cancel_right' leq_minus1_less not_le zero_least) 187 188lemma less_uminus: 189 "\<lbrakk> - x < y; x \<noteq> 0 \<rbrakk> \<Longrightarrow> - y < (x::'a)" 190 unfolding definitions 191 by (smt Rep_inverse Rep_mod Rep_Abs_mod size0 zmod_zminus1_eq_if) 192 193lemma of_nat_cases[case_names of_nat]: 194 "(\<And>m. \<lbrakk> (x::'a) = of_nat m; m < nat n \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P" 195 by (metis mod_type.Rep_less_n mod_type_axioms nat_mono_iff of_nat_size size0 size_def) 196 197lemma minus_induct[case_names 0 minus]: 198 assumes "P (0::'a)" 199 assumes suc: "\<And>x. \<lbrakk> P (x - 1); 0 < x \<rbrakk> \<Longrightarrow> P x" 200 shows "P x" 201proof (cases x rule: of_nat_cases) 202 case (of_nat m) 203 have "P (of_nat m)" 204 proof (induct m) 205 case 0 206 then show ?case using `P 0` by simp 207 next 208 case (Suc m) 209 show ?case 210 proof (cases "1 + of_nat m = (0::'a)") 211 case True 212 then show ?thesis using `P 0` by simp 213 next 214 case False 215 with Suc suc show ?thesis by (metis add_diff_cancel_left' less_eq_0 not_less of_nat_Suc) 216 qed 217 qed 218 with of_nat show ?thesis by simp 219qed 220 221lemma plus_induct[case_names 0 plus]: 222 assumes "P (0::'a)" 223 assumes suc: "\<And>x. \<lbrakk> P x; x < x + 1 \<rbrakk> \<Longrightarrow> P (x + 1)" 224 shows "P x" 225proof (cases x rule: of_nat_cases) 226 case (of_nat m) 227 have "P (of_nat m)" 228 proof (induct m) 229 case 0 230 then show ?case using `P 0` by simp 231 next 232 case (Suc m) 233 with `P 0` suc show ?case by (metis diff_add_cancel minus_induct pred) 234 qed 235 with of_nat show ?thesis by simp 236qed 237 238lemma from_top_induct[case_names top step]: 239 assumes top: "\<And>x. y \<le> x \<Longrightarrow> P (x::'a)" 240 assumes step: "\<And>x. \<lbrakk>P x; 0 < x; x \<le> y\<rbrakk> \<Longrightarrow> P (x - 1)" 241 shows "P x" 242proof - 243 obtain z where x: "x = y - z" 244 by (metis diff_eq_diff_eq diff_right_commute) 245 moreover 246 have "P (y - z)" 247 proof (induct z rule: plus_induct) 248 case 0 249 then show ?case by (simp add: top) 250 next 251 case (plus x) 252 then have [simp]: "y - (x + 1) = (y - x) - 1" by simp 253 show ?case 254 proof (cases "x < y") 255 case True 256 with plus show ?thesis 257 by simp (metis diff_add_cancel eq_iff_diff_eq_0 le_neq_trans step plus_one_leq not_le 258 top zero_less_eq) 259 next 260 case False 261 with plus show ?thesis 262 by (smt top Rep_Abs_mod Rep_le_n less_def less_eq_def diff_def int_mod_ge' size0) 263 qed 264 qed 265 ultimately show ?thesis by simp 266qed 267 268lemma tranclp_greater: "(>)\<^sup>+\<^sup>+ = ((>) :: 'a \<Rightarrow> 'a \<Rightarrow> bool)" 269 by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct) 270 271lemma card_n: 272 "CARD('a) = nat n" 273 using type by (simp add: type_definition.card) 274 275lemma finite_UNIV[intro!,simp]: 276 "finite (UNIV::'a set)" 277 by (rule card_ge_0_finite) (simp add: card_n size0) 278 279lemma finite_greater[simp]: 280 "finite {(x, y). y < (x::'a)}" 281 by (rule finite_subset[of _ "UNIV \<times> UNIV"], simp) 282 (rule finite_cartesian_product; rule finite_UNIV) 283 284lemma wf_greater[intro!,simp]: 285 "wf {(x,y). x > (y::'a)}" 286 by (auto simp: trancl_def tranclp_greater intro!: finite_acyclic_wf acyclicI) 287 288(* less_induct already instantiated in class well_order *) 289lemma greater_induct[case_names greater]: 290 "(\<And>x. (\<And>z. x < z \<Longrightarrow> P z) \<Longrightarrow> P x) \<Longrightarrow> P (x::'a)" 291 by (rule wf_induct_rule, rule wf_greater) fastforce 292 293lemma from_top_full_induct[case_names top step]: 294 assumes top: "\<And>x. y \<le> x \<Longrightarrow> P (x::'a)" 295 assumes step: "\<And>x. \<lbrakk>\<forall>z > x. P z; x < y\<rbrakk> \<Longrightarrow> P x" 296 shows "P x" 297proof (induct x rule: greater_induct) 298 case (greater x) 299 show ?case 300 proof (cases "x < y") 301 case True 302 then show ?thesis by (blast intro: step greater) 303 next 304 case False 305 then show ?thesis by (auto simp: not_less intro: top) 306 qed 307qed 308 309interpretation greater_wellorder: wellorder "(\<ge>) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "(>) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" 310 by unfold_locales (auto intro: greater_induct) 311 312lemma greater_least_fold[simp]: "greater_wellorder.Least = Greatest" 313 by (auto simp: greater_wellorder.Least_def Greatest_def) 314 315lemmas GreatestI = greater_wellorder.LeastI[simplified greater_least_fold] 316lemmas Greatest_le = greater_wellorder.Least_le[simplified greater_least_fold] 317lemmas exists_greatest_iff = greater_wellorder.exists_least_iff 318lemmas GreatestI2_wellorder = greater_wellorder.LeastI2_wellorder[simplified greater_least_fold] 319 320lemma neq_0_conv: 321 "((x::'a) \<noteq> 0) = (0 < x)" 322 by (meson neqE not_less_zero_bit0) 323 324lemma minus_leq_less: "\<lbrakk> (x::'a) \<le> y; 0 < z; z \<le> x \<rbrakk> \<Longrightarrow> x - z < y" 325 by (metis le_less less_trans minus_less) 326 327lemma minus_one_leq_less: "\<lbrakk> (x::'a) \<le> y; 0 < x \<rbrakk> \<Longrightarrow> x - 1 < y" 328 using pred by fastforce 329 330lemma size_minus: 331 "y \<le> (x::'a) \<Longrightarrow> size (x - y) = size x - size y" 332 unfolding definitions Rep_Abs_mod 333 using Rep size0 334 by (simp flip: nat_diff_distrib add: eq_nat_nat_iff pos_mod_sign mod_sub_if_z split: if_split_asm) 335 336lemma size_minus_one: 337 "0 < (x::'a) \<Longrightarrow> size (x - 1) = size x - Suc 0" 338 by (simp add: size_minus) 339 340end 341 342interpretation bit0: 343 mod_size_order "int CARD('a::finite bit0)" 344 "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" 345 "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" 346 by unfold_locales (auto simp: size_bit0_def less_bit0_def less_eq_bit0_def) 347 348interpretation bit1: 349 mod_size_order "int CARD('a::finite bit1)" 350 "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" 351 "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" 352 by unfold_locales (auto simp: size_bit1_def less_bit1_def less_eq_bit1_def) 353 354declare bit0.minus_induct[induct type] 355declare bit1.minus_induct[induct type] 356 357section \<open>Further enumeration instances.\<close> 358 359instantiation bit0 and bit1 :: (finite) enumeration_both 360begin 361 362definition enum_alt_bit0 where "enum_alt \<equiv> alt_from_ord (enum :: 'a :: finite bit0 list)" 363definition enum_alt_bit1 where "enum_alt \<equiv> alt_from_ord (enum :: 'a :: finite bit1 list)" 364 365instance by intro_classes (auto simp: enum_alt_bit0_def enum_alt_bit1_def) 366 367end 368 369subsection \<open>Relating @{const enum} and @{const size}\<close> 370 371lemma fromEnum_size_bit0[simp]: 372 "fromEnum (x::'a::finite bit0) = size x" 373proof - 374 have "enum ! the_index enum x = x" by (auto intro: nth_the_index) 375 moreover 376 have "the_index enum x < length (enum::'a bit0 list)" by (auto intro: the_index_bounded) 377 moreover 378 { fix y 379 assume "Abs_bit0' (int y) = x" 380 moreover 381 assume "y < 2 * CARD('a)" 382 ultimately 383 have "y = nat (Rep_bit0 x)" 384 by (smt Abs_bit0'_code card_bit0 mod_pos_pos_trivial nat_int of_nat_less_0_iff 385 zless_nat_eq_int_zless) 386 } 387 ultimately 388 show ?thesis by (simp add: fromEnum_def enum_bit0_def size_bit0_def) 389qed 390 391lemma fromEnum_size_bitq[simp]: 392 "fromEnum (x::'a::finite bit1) = size x" 393proof - 394 have "enum ! the_index enum x = x" by (auto intro: nth_the_index) 395 moreover 396 have "the_index enum x < length (enum::'a bit1 list)" by (auto intro: the_index_bounded) 397 moreover 398 { fix y 399 assume "Abs_bit1' (int y) = x" 400 moreover 401 assume "y < Suc (2 * CARD('a))" 402 ultimately 403 have "y = nat (Rep_bit1 x)" 404 by (smt Abs_bit1'_code card_bit1 mod_pos_pos_trivial nat_int of_nat_less_0_iff 405 zless_nat_eq_int_zless) 406 } 407 ultimately 408 show ?thesis by (simp add: fromEnum_def enum_bit1_def size_bit1_def del: upt_Suc) 409qed 410 411lemma minBound_size_bit0[simp]: 412 "(minBound::'a::finite bit0) = 0" 413 by (simp add: minBound_def hd_map enum_bit0_def Abs_bit0'_def zero_bit0_def) 414 415lemma minBound_size_bit1[simp]: 416 "(minBound::'a::finite bit1) = 0" 417 by (simp add: minBound_def hd_map enum_bit1_def Abs_bit1'_def zero_bit1_def) 418 419lemma maxBound_size_bit0: 420 "(maxBound::'a::finite bit0) = of_nat (2 * CARD('a) - 1)" 421 by (simp add: maxBound_def enum_bit0_def last_map Abs_bit0'_def bit0.of_nat_eq) 422 423lemma maxBound_size_bit1: 424 "(maxBound::'a::finite bit1) = of_nat (2 * CARD('a))" 425 by (simp add: maxBound_def enum_bit1_def last_map Abs_bit1'_def bit1.of_nat_eq) 426 427lemma maxBound_minus_one_bit0: 428 "maxBound = (-1 ::'a::finite bit0)" 429 by (simp add: bit0.definitions bit0.of_nat_eq bit0.Rep_Abs_1 maxBound_size_bit0) 430 431lemma maxBound_minus_one_bit1: 432 "maxBound = (-1 ::'a::finite bit1)" 433 by (simp add: bit1.definitions bit1.of_nat_eq bit1.Rep_Abs_1 zmod_minus1 maxBound_size_bit1) 434 435lemmas maxBound_size_bit = maxBound_size_bit0 maxBound_size_bit1 436lemmas maxBound_minus_one_bit[simp] = maxBound_minus_one_bit1 maxBound_minus_one_bit0 437 438end