Fix another proof broken by automatic {DIV,MOD}_0

HOL-Theorem-Prover · Jul 3, 2023 · 39d587c · 39d587c
1 parent 3e3b690
commit 39d587c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/examples/machine-code/multiword/multiwordScript.sml b/examples/machine-code/multiword/multiwordScript.sml
@@ -1917,7 +1917,7 @@ Theorem mw_div_range2:
     dimword(:'a) DIV 2 <= w2n v1 ==>
     MIN ((w2n u1 * dimword(:'a) + w2n u2) DIV w2n v1) (dimword(:'a)-1)
     <= mw2n (REVERSE (u1::u2::us)) DIV mw2n (REVERSE (v1::vs)) + 2
-Proof
+Proof[exclude_simps = DIV_0 MOD_0]
 
     REPEAT GEN_TAC >>
     Q.PAT_ABBREV_TAC`V = mw2n (REVERSE (v1::vs))` >>
@@ -1966,7 +1966,7 @@ Proof
                                        `q' * (a * l) <= (w2n u1 * b + w2n u2) * l` by METIS_TAC[MULT_ASSOC,Abbr`a`,DIV_thm3,LESS_EQ_TRANS,LESS_MONO_MULT,Abbr`q'`] >>
                                        `U = (w2n u1 * b + w2n u2) * l + mw2n (REVERSE us)` by lrw[Abbr`U`,Abbr`b`,Abbr`l`,mw2n_msf,dimwords_dimword,EXP,GSYM ADD1] >>
                                        `q' * (a * l) <= U` by METIS_TAC[Abbr`a`,LESS_EQ_ADD,LESS_EQ_TRANS,Abbr`q'`] >>
-                                       Cases_on `U = 0` THEN1 full_simp_tac (srw_ss())[ENC] >>
+                                       Cases_on `U = 0` THEN1 gvs[ENC] >>
                                        `q' * X < U` by( Cases_on `0 < q'`
                                               THEN1( `V = a * l + mw2n(REVERSE vs)` by lrw[Abbr`V`,Abbr`l`,Abbr`a`,mw2n_msf,dimwords_dimword] >>
                                                      `V < a * l + l` by (full_simp_tac (srw_ss())[Abbr`l`,Abbr`b`,Abbr`a`] >> METIS_TAC[mw2n_lt,LENGTH_REVERSE,dimwords_dimword]) >>