lib: move Distinct_Prop out of Word_Lib

lib/Distinct_Prop.thy

@@ -12,7 +12,7 @@ chapter "Distinct Proposition"
 
 theory Distinct_Prop
 imports
-  HOL_Lemmas
+  "Word_Lib/HOL_Lemmas"
   "~~/src/HOL/Library/Prefix_Order"
 begin
 

lib/HaskellLib_H.thy

@@ -16,8 +16,8 @@
 theory HaskellLib_H
 imports
   Lib
+  WordSetup
   "Monad_WP/NonDetMonadVCG"
-  "Word_Lib/Word_Enum"
 begin
 
 abbreviation (input) "flip \<equiv> swp"

lib/WordSetup.thy

@@ -8,10 +8,37 @@
  * @TAG(NICTA_BSD)
  *)
 
-theory WordSetup           
-imports "Word_Lib/Word_Lemmas_32"
+
+theory WordSetup
+imports
+  Distinct_Prop
+  "Word_Lib/Word_Lemmas_32"
 begin
 
-(* select 32 bits *)
+(* Distinct_Prop lemmas that need word lemmas: *)
+
+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
+
+lemma distinct_prop_enum_step:
+  "\<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>
+     \<Longrightarrow> distinct_prop P [0, step .e. stop]"
+  apply (simp add: upto_enum_step_def distinct_prop_map)
+  apply (rule distinct_prop_enum)
+  apply simp
+  done
 
 end

lib/Word_Lib/Word_Lemmas.thy

@@ -11,7 +11,6 @@
 theory Word_Lemmas
 imports
   Aligned
-  Distinct_Prop
   Word_Enum
 begin
 
@@ -1783,33 +1782,6 @@ proof -
   qed
 qed
 
-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
-
-lemma distinct_prop_enum_step:
-  "\<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>
-     \<Longrightarrow> distinct_prop P [0, step .e. stop]"
-  apply (simp add: upto_enum_step_def distinct_prop_map)
-  apply (rule distinct_prop_enum)
-  apply simp
-  done
-
 lemma upto_enum_step_shift:
   "\<lbrakk> is_aligned p n \<rbrakk> \<Longrightarrow>
   ([p , p + 2 ^ m .e. p + 2 ^ n - 1])