Move good_dimindex to miscTheory

good_dimindex is needed here and there. It seems silly to pollute
the dependency graph with imports of labProps just for that.

Fixes issue #818.

compiler/backend/ag32/proofs/ag32_memoryProofScript.sml

@@ -25,14 +25,14 @@ Theorem get_byte_word_of_bytes:
 Proof
   strip_tac
   \\ `∃k. dimindex(:'a) DIV 8 = 2 ** k` by(
-    fs[labPropsTheory.good_dimindex_def]
+    fs[good_dimindex_def]
     \\ TRY(qexists_tac`2` \\ EVAL_TAC \\ NO_TAC)
     \\ TRY(qexists_tac`3` \\ EVAL_TAC \\ NO_TAC) )
   \\ strip_tac
   \\ Q.ISPECL_THEN[`be`,`0w`,`ls`,`2 ** k`]mp_tac word_of_bytes_bytes_to_word
   \\ impl_keep_tac >- (
     rfs[bytes_in_word_def, dimword_def]
-    \\ fs[labPropsTheory.good_dimindex_def] \\ rfs[])
+    \\ fs[good_dimindex_def] \\ rfs[])
   \\ rw[]
   \\ DEP_REWRITE_TAC[data_to_word_memoryProofTheory.get_byte_bytes_to_word]
   \\ rw[]
@@ -50,7 +50,7 @@ Proof
   \\ rw[words_of_bytes_def]
   \\ qmatch_goalsub_abbrev_tac`MAX 1 bw`
   \\ `0 < bw` by (
-     fs[Abbr`bw`,labPropsTheory.good_dimindex_def]
+     fs[Abbr`bw`,good_dimindex_def]
      \\ EVAL_TAC \\ fs[dimword_def] )
   \\ `MAX 1 bw = bw` by rw[MAX_DEF] \\ fs[]
   \\ Cases_on`i < bw` \\ fs[]
@@ -59,7 +59,7 @@ Proof
     by(
       simp[alignmentTheory.byte_align_def]
       \\ irule lt_align_eq_0
-      \\ fs[labPropsTheory.good_dimindex_def,Abbr`bw`]
+      \\ fs[good_dimindex_def,Abbr`bw`]
       \\ rfs[bytes_in_word_def,dimword_def] )
     \\ simp[ZERO_DIV]
     \\ DEP_REWRITE_TAC[UNDISCH get_byte_word_of_bytes]
@@ -83,19 +83,19 @@ Proof
   >- (
     simp[Abbr`bw`]
     \\ reverse conj_tac >- (
-      fs[labPropsTheory.good_dimindex_def,
+      fs[good_dimindex_def,
          bytes_in_word_def]
       \\ EVAL_TAC \\ fs[] \\ EVAL_TAC )
     \\ simp[alignmentTheory.byte_align_def]
     \\ DEP_REWRITE_TAC[word_msb_align]
-    \\ conj_tac >- ( fs[labPropsTheory.good_dimindex_def])
+    \\ conj_tac >- ( fs[good_dimindex_def])
     \\ simp[word_msb_n2w]
     \\ qmatch_assum_abbrev_tac`bw * r ≤ dimword _`
     \\ `r ≤ dimword (:'a) DIV bw` by fs[X_LE_DIV]
     \\ `p < dimword(:'a) DIV bw` by fs[]
     \\ match_mp_tac bitTheory.NOT_BIT_GT_TWOEXP
     \\ fs[dimword_def, bytes_in_word_def]
-    \\ fs[Abbr`bw`, labPropsTheory.good_dimindex_def]
+    \\ fs[Abbr`bw`, good_dimindex_def]
     \\ rfs[] )
   \\ `bw < dimword(:'a)` by fs[Abbr`bw`, bytes_in_word_def]
   \\ simp[]
@@ -106,7 +106,7 @@ Proof
   \\ `n2w bw = byte_align (n2w bw)`
   by(
     fs[Abbr`bw`,bytes_in_word_def,alignmentTheory.byte_align_def]
-    \\ fs[labPropsTheory.good_dimindex_def]
+    \\ fs[good_dimindex_def]
     \\ EVAL_TAC \\ fs[dimword_def] \\ EVAL_TAC )
   \\ pop_assum SUBST1_TAC
   \\ once_rewrite_tac[WORD_ADD_COMM]

compiler/backend/proofs/backendProofScript.sml

@@ -28,7 +28,6 @@ val _ = set_trace "BasicProvers.var_eq_old" 1
 val _ = Parse.set_grammar_ancestry
   [ "backend", "backend_common", "backendProps",
     "primSemEnv", "semanticsProps",
-    "labProps", (* for good_dimindex *)
     "source_evalProof" (* for compiler instance structure *)
   ];
 
@@ -38,7 +37,7 @@ Theorem byte_aligned_mult:
    good_dimindex (:'a) ==>
     byte_aligned (a + bytes_in_word * n2w i) = byte_aligned (a:'a word)
 Proof
-  fs [alignmentTheory.byte_aligned_def,labPropsTheory.good_dimindex_def]
+  fs [alignmentTheory.byte_aligned_def,good_dimindex_def]
   \\ rw [] \\ fs [bytes_in_word_def,word_mul_n2w]
   \\ once_rewrite_tac [MULT_COMM]
   \\ rewrite_tac [GSYM (EVAL ``2n**2``),GSYM (EVAL ``2n**3``), aligned_add_pow]
@@ -51,7 +50,7 @@ Theorem byte_aligned_MOD:
 Proof
   rw[IN_DEF]>>
   fs [aligned_w2n, alignmentTheory.byte_aligned_def]>>
-  rfs[labPropsTheory.good_dimindex_def] \\ rfs []
+  rfs[good_dimindex_def] \\ rfs []
 QED
 
 (* -- *)
@@ -2029,7 +2028,7 @@ Proof
     \\ reverse conj_tac >- (
       first_x_assum irule
       \\ fs[mc_conf_ok_def]
-      \\ fs[WORD_LE,labPropsTheory.good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w]
+      \\ fs[WORD_LE,good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w]
     )
     \\ simp[Abbr`ppg`]
     \\ irule stack_namesProofTheory.stack_names_stack_asm_ok
@@ -2084,7 +2083,7 @@ Proof
       \\ fsrw_tac[DNF_ss][]
       \\ conj_tac \\ first_x_assum irule
       \\ fs[mc_conf_ok_def]
-      \\ fs[WORD_LE,labPropsTheory.good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w] )
+      \\ fs[WORD_LE,good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w] )
     \\ simp[EVERY_MEM, FORALL_PROD] \\ fs[]
     \\ disch_then drule
     \\ simp[]
@@ -2185,7 +2184,7 @@ Proof
     \\ fsrw_tac[DNF_ss][]
     \\ conj_tac \\ first_x_assum irule
     \\ fs[mc_conf_ok_def]
-    \\ fs[WORD_LE,labPropsTheory.good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w])
+    \\ fs[WORD_LE,good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w])
   \\ simp[]
   \\ strip_tac
   \\ simp[EVERY_MAP]
@@ -3372,7 +3371,7 @@ Proof
     unabbrev_all_tac >>
     fs[EVERY_MEM,MEM_MAP,PULL_EXISTS,FORALL_PROD]>>rfs[]>>
     `-8w ≤ 0w:'a word ∧ 0w:'a word ≤ 8w` by
-      fs[WORD_LE,labPropsTheory.good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w]>>
+      fs[WORD_LE,good_dimindex_def,word_2comp_n2w,dimword_def,word_msb_n2w]>>
     metis_tac[])>>
   `stack_to_labProof$labels_ok p7` by
     (fs[Abbr`p7`]>>
@@ -3555,7 +3554,7 @@ Proof
     conj_tac >- (
       rfs[memory_assumption_def,Abbr`dm`] \\
       `(w2n:'a word -> num) bytes_in_word = dimindex (:α) DIV 8` by
-       rfs [labPropsTheory.good_dimindex_def,bytes_in_word_def,dimword_def]>>
+       rfs [good_dimindex_def,bytes_in_word_def,dimword_def]>>
       fs [attach_bitmaps_def] \\
       once_rewrite_tac[INTER_COMM] \\
       rewrite_tac[UNION_OVER_INTER] \\
@@ -3571,18 +3570,18 @@ Proof
         fs [stack_removeProofTheory.addresses_thm]>>
         fs[mc_conf_ok_def]>>
         `0 < dimindex (:α) DIV 8` by
-          rfs [labPropsTheory.good_dimindex_def]>>
+          rfs [good_dimindex_def]>>
         reverse conj_tac >-
          (fs [] \\ match_mp_tac IMP_MULT_DIV_LESS \\ fs [w2n_lt]
-          \\ rfs [labPropsTheory.good_dimindex_def])
+          \\ rfs [good_dimindex_def])
         \\ qabbrev_tac `a = tar_st.regs mc.len_reg`
         \\ qabbrev_tac `b = tar_st.regs mc.len2_reg`
         \\ qpat_x_assum `a <=+ b` assume_tac
         \\ old_drule WORD_LS_IMP \\ strip_tac \\ fs [EXTENSION]
         \\ fs [IN_DEF,PULL_EXISTS,bytes_in_word_def,word_mul_n2w]
         \\ rw [] \\ reverse eq_tac THEN1
          (rw [] \\ fs [] \\ qexists_tac `i * (dimindex (:α) DIV 8)` \\ fs []
-          \\ `0 < dimindex (:α) DIV 8` by rfs [labPropsTheory.good_dimindex_def]
+          \\ `0 < dimindex (:α) DIV 8` by rfs [good_dimindex_def]
           \\ old_drule X_LT_DIV \\ disch_then (fn th => fs [th])
           \\ fs [RIGHT_ADD_DISTRIB]
           \\ fs [GSYM word_mul_n2w,GSYM bytes_in_word_def]
@@ -3596,7 +3595,7 @@ Proof
         \\ old_drule DIVISION
         \\ disch_then (qspec_then `i` (strip_assume_tac o GSYM))
         \\ `2 ** LOG2 (dimindex (:α) DIV 8) = dimindex (:α) DIV 8` by
-             (fs [labPropsTheory.good_dimindex_def] \\ NO_TAC)
+             (fs [good_dimindex_def] \\ NO_TAC)
         \\ fs [] \\ rfs [] \\ `-1w * a + b = b - a` by fs []
         \\ full_simp_tac std_ss []
         \\ Cases_on `a` \\ Cases_on `b`
@@ -3695,7 +3694,7 @@ Proof
       (fs [lab_to_targetProofTheory.mc_conf_ok_def]
        \\ qpat_x_assum `good_dimindex _` mp_tac
        \\ rpt (pop_assum kall_tac)
-       \\ rw [labPropsTheory.good_dimindex_def] \\ simp [])
+       \\ rw [good_dimindex_def] \\ simp [])
      \\ rewrite_tac[CONJ_ASSOC]
      \\ simp [MULT_DIV,FST_SND_EQ]
      \\ qpat_x_assum `_ = (_,_)` (assume_tac o GSYM) \\ simp []

compiler/backend/proofs/data_to_wordProofScript.sml

@@ -5,7 +5,7 @@ open preamble dataSemTheory dataPropsTheory
      copying_gcTheory int_bitwiseTheory finite_mapTheory
      data_to_word_memoryProofTheory data_to_word_gcProofTheory
      data_to_word_bignumProofTheory data_to_word_assignProofTheory
-     data_to_wordTheory wordPropsTheory labPropsTheory whileTheory
+     data_to_wordTheory wordPropsTheory whileTheory
      set_sepTheory semanticsPropsTheory word_to_wordProofTheory
      helperLib alignmentTheory blastLib word_bignumTheory
      wordLangTheory word_bignumProofTheory gen_gc_partialTheory