From b53822e18dcfb4bf9d4267afa9a310614bf5b940 Mon Sep 17 00:00:00 2001 From: Hrutvik Kanabar Date: Tue, 26 Mar 2024 14:12:37 +0000 Subject: [PATCH] Some fixes - Unicode violations - Missing `INCLUDES` in `Holmakefile` - Update a `README` --- examples/cv_compute/Holmakefile | 3 ++- examples/cv_compute/README | 9 +++++---- src/finite_maps/sptreeScript.sml | 2 +- src/n-bit/bitstringScript.sml | 4 ++-- 4 files changed, 10 insertions(+), 8 deletions(-) diff --git a/examples/cv_compute/Holmakefile b/examples/cv_compute/Holmakefile index 57d87459c2..c5316d2c1a 100644 --- a/examples/cv_compute/Holmakefile +++ b/examples/cv_compute/Holmakefile @@ -1 +1,2 @@ -INCLUDES = $(HOLDIR)/examples/bootstrap +INCLUDES = $(HOLDIR)/src/num/theories/cv_compute/automation/ \ + $(HOLDIR)/examples/bootstrap diff --git a/examples/cv_compute/README b/examples/cv_compute/README index 1bee61f05b..e2a26c5cee 100644 --- a/examples/cv_compute/README +++ b/examples/cv_compute/README @@ -5,8 +5,9 @@ Examples on using the cv_computeLib library examplesScript.sml Two examples of how to define functions in the :cv type, for use with cv_computeLib.compute. - cv_numsLib.{sig,sml} An example building a conversion for natural number - arithmetic using cv_computeLib. - cv_numsScript.sml Support theorems and definitions for cv_numsLib. - cv_numsTestScript.sml Examples using cv_numsLib. + cv_golScript.sml An example which uses cv_transLib to evaluate + Conway's Game of Life symbolically. + + cv_bootScript.sml An example which applies cv_transLib to the compiler + from HOL/examples/bootstrap. diff --git a/src/finite_maps/sptreeScript.sml b/src/finite_maps/sptreeScript.sml index e28c213b5c..7553a851e5 100644 --- a/src/finite_maps/sptreeScript.sml +++ b/src/finite_maps/sptreeScript.sml @@ -426,7 +426,7 @@ Proof QED Theorem lrnext_eq: - ∀n. sptree$lrnext n = 2 ** (LOG 2 (n + 1)) + !n. sptree$lrnext n = 2 ** (LOG 2 (n + 1)) Proof strip_tac >> completeInduct_on `n` >> rw[] >> rw[Once lrnext_def] >> diff --git a/src/n-bit/bitstringScript.sml b/src/n-bit/bitstringScript.sml index b25b3c13cf..95362c9283 100644 --- a/src/n-bit/bitstringScript.sml +++ b/src/n-bit/bitstringScript.sml @@ -833,13 +833,13 @@ Proof simp[word_lsl_v2w, word_lsr_v2w, rotate_def, word_or_v2w] >> simp[Once v2w_11] >> simp[field_def, arithmeticTheory.ADD1] >> `shiftr v 0 = v` by simp[shiftr_def] >> simp[] >> - `¬ (LENGTH v < r MOD LENGTH v)` by ( + `~(LENGTH v < r MOD LENGTH v)` by ( simp[arithmeticTheory.NOT_LESS] >> irule arithmeticTheory.LESS_IMP_LESS_OR_EQ >> simp[arithmeticTheory.MOD_LESS]) >> rewrite_tac[fixwidth] >> simp[length_shiftr] >> qmatch_goalsub_abbrev_tac `bor a b` >> - `¬ (LENGTH (bor a b) < LENGTH v)` by ( + `~(LENGTH (bor a b) < LENGTH v)` by ( unabbrev_all_tac >> rewrite_tac[bor_def, bitwise_def] >> simp[length_shiftr, shiftl_def, length_fixwidth, length_pad_right]) >> unabbrev_all_tac >>