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