theory WordSetup

lemma distinct_prop_enum:
  "\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop; y \<le> stop; x \<noteq> y \<rbrakk> \<Longrightarrow> P x y \<rbrakk>
     \<Longrightarrow> distinct_prop P [0 :: 'a :: len word .e. stop]" apply (simp add: upto_enum_def distinct_prop_map del: upt.simps) apply (rule distinct_prop_distinct) apply simp apply (simp add: less_Suc_eq_le del: upt.simps) apply (erule_tac x="of_nat x" in meta_allE) apply (erule_tac x="of_nat y" in meta_allE) apply (frule_tac y=x in unat_le) apply (frule_tac y=y in unat_le) apply (erule word_unat.Rep_cases)+ apply (simp add: toEnum_of_nat[OF unat_lt2p]
                   word_le_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<le> stop; y \<le> stop; x \<noteq> y\<rbrakk> \<Longrightarrow> P x y) \<Longrightarrow> distinct_prop P [0 .e. stop] proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<le> stop; y \<le> stop; x \<noteq> y\<rbrakk> \<Longrightarrow> P x y) \<Longrightarrow> distinct_prop (\<lambda>x y. P (toEnum x) (toEnum y)) [0..<Suc (unat stop)] proof (prove)
goal (2 subgoals):
 1. (\<And>x y. \<lbrakk>x \<le> stop; y \<le> stop; x \<noteq> y\<rbrakk> \<Longrightarrow> P x y) \<Longrightarrow> distinct [0..<Suc (unat stop)]
 2. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<le> stop; y \<le> stop; x \<noteq> y\<rbrakk> \<Longrightarrow> P x y; x \<in> set [0..<Suc (unat stop)]; y \<in> set [0..<Suc (unat stop)]; x \<noteq> y\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<le> stop; y \<le> stop; x \<noteq> y\<rbrakk> \<Longrightarrow> P x y; x \<in> set [0..<Suc (unat stop)]; y \<in> set [0..<Suc (unat stop)]; x \<noteq> y\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<le> stop; y \<le> stop; x \<noteq> y\<rbrakk> \<Longrightarrow> P x y; x \<le> unat stop; y \<le> unat stop; x \<noteq> y\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> unat stop; y \<le> unat stop; x \<noteq> y; \<And>y. \<lbrakk>word_of_nat x \<le> stop; y \<le> stop; word_of_nat x \<noteq> y\<rbrakk> \<Longrightarrow> P (word_of_nat x) y\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> unat stop; y \<le> unat stop; x \<noteq> y; \<lbrakk>word_of_nat x \<le> stop; word_of_nat y \<le> stop; word_of_nat x \<noteq> word_of_nat y\<rbrakk> \<Longrightarrow> P (word_of_nat x) (word_of_nat y)\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> unat stop; y \<le> unat stop; x \<noteq> y; \<lbrakk>word_of_nat x \<le> stop; word_of_nat y \<le> stop; word_of_nat x \<noteq> word_of_nat y\<rbrakk> \<Longrightarrow> P (word_of_nat x) (word_of_nat y); x \<in> unats LENGTH('a)\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> unat stop; y \<le> unat stop; x \<noteq> y; \<lbrakk>word_of_nat x \<le> stop; word_of_nat y \<le> stop; word_of_nat x \<noteq> word_of_nat y\<rbrakk> \<Longrightarrow> P (word_of_nat x) (word_of_nat y); x \<in> unats LENGTH('a); y \<in> unats LENGTH('a)\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal (1 subgoal):
 1. \<And>x y xa xb. \<lbrakk>x \<le> unat stop; y \<le> unat stop; x \<noteq> y; \<lbrakk>word_of_nat x \<le> stop; word_of_nat y \<le> stop; word_of_nat x \<noteq> word_of_nat y\<rbrakk> \<Longrightarrow> P (word_of_nat x) (word_of_nat y); x = unat xa; y = unat xb\<rbrakk> \<Longrightarrow> P (toEnum x) (toEnum y) proof (prove)
goal:
No subgoals!