Fix some broken proofs

CakeML · May 20, 2019 · 1694ad3 · 1694ad3
1 parent c0c4142
commit 1694ad3
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/basis/fsFFIPropsScript.sml b/basis/fsFFIPropsScript.sml
@@ -81,14 +81,17 @@ Proof
     fs[bumpFD_def]
 QED
 
-Theorem bumpFD_inode_tbl[simp]
+Theorem bumpFD_inode_tbl[simp]:
-  `(bumpFD fd fs n).inode_tbl = fs.inode_tbl`
+  (bumpFD fd fs n).inode_tbl = fs.inode_tbl
+Proof
+  EVAL_TAC
+QED
 
 Theorem bumpFD_files[simp]:
    (bumpFD fd fs n).files = fs.files
 Proof
   EVAL_TAC
-QED (EVAL_TAC);
+QED
 
 Theorem bumpFD_o:
   !fs fd n1 n2.

diff --git a/compiler/bootstrap/translation/to_closProgScript.sml b/compiler/bootstrap/translation/to_closProgScript.sml
@@ -256,8 +256,7 @@ val clos_annotate_shift_side = Q.prove(`
   ho_match_mp_tac clos_annotateTheory.shift_ind>>
   `∀a b c d. shift [a] b c d ≠ []` by
     (CCONTR_TAC>>fs[]>>
-    imp_res_tac clos_annotateTheory.shift_SING>>
+    metis_tac[clos_annotateTheory.shift_SING,list_distinct])>>
-    fs[])>>
   rw[]>>
   simp[Once (fetch "-" "clos_annotate_shift_side_def")]>>
   rw[]>> metis_tac[]) |> update_precondition;