1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7
8theory WordSetup (* part of non-AFP Word_Lib *)
9imports
10  Distinct_Prop
11  Word_Lemmas_64_Internal
12begin
13
14(* Distinct_Prop lemmas that need word lemmas: *)
15
16lemma distinct_prop_enum:
17  "\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop; y \<le> stop; x \<noteq> y \<rbrakk> \<Longrightarrow> P x y \<rbrakk>
18     \<Longrightarrow> distinct_prop P [0 :: 'a :: len word .e. stop]"
19  apply (simp add: upto_enum_def distinct_prop_map del: upt.simps)
20  apply (rule distinct_prop_distinct)
21   apply simp
22  apply (simp add: less_Suc_eq_le del: upt.simps)
23  apply (erule_tac x="of_nat x" in meta_allE)
24  apply (erule_tac x="of_nat y" in meta_allE)
25  apply (frule_tac y=x in unat_le)
26  apply (frule_tac y=y in unat_le)
27  apply (erule word_unat.Rep_cases)+
28  apply (simp add: toEnum_of_nat[OF unat_lt2p]
29                   word_le_nat_alt)
30  done
31
32lemma distinct_prop_enum_step:
33  "\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop div step; y \<le> stop div step; x \<noteq> y \<rbrakk> \<Longrightarrow> P (x * step) (y * step) \<rbrakk>
34     \<Longrightarrow> distinct_prop P [0, step .e. stop]"
35  apply (simp add: upto_enum_step_def distinct_prop_map)
36  apply (rule distinct_prop_enum)
37  apply simp
38  done
39
40end
41