wip

CHANGES.md

@@ -19,6 +19,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
   (an stp file contains the starting position of the corresponding proof)
 - command theorem to generate the lp files corresponding to a named theorem
 - Makefile to generate and check lp and coq files generated with split
+- fusion.ml: do not generate new theorems for empty instantiations
 
 ### Modified
 

Makefile

@@ -14,7 +14,8 @@ stp:
 
 .PHONY: clean-stp
 clean-stp:
-	find . -name '*.stp' -exec rm -f {} `basename {}`.pos `basename {}`.use \;
+	find . -maxdepth 1 -name '*.stp' -exec rm -f {} `basename {}`.pos `basename {}`.use \;
+	rm -f $(BASE).thp
 
 BASE_FILES := $(BASE)_types $(BASE)_terms $(BASE)_axioms
 

README.md

@@ -409,9 +409,9 @@ Dumping of `hol.ml`:
 | comb       | 20 |
 | term_subst | 17 |
 | refl       | 16 |
-| eqmp       | 11 |
+| eqmp       | 12 |
 | trans      |  9 |
-| conjunct1  |  5 |
+| conjunct1  |  6 |
 | abs        |  3 |
 | beta       |  3 |
 | mp         |  3 |

fusion.ml

@@ -685,11 +685,11 @@ module Hol : Hol_kernel = struct
 (* Type and term instantiation.                                              *)
 (* ------------------------------------------------------------------------- *)
 
-  let INST_TYPE theta (Sequent(asl,c,k)) =
+  let INST_TYPE theta (Sequent(asl,c,k) as th) = if theta = [] then th else
     let inst_fn = inst theta in
     new_theorem (term_image inst_fn asl) (inst_fn c) (Pinstt(k,theta))
 
-  let INST theta (Sequent(asl,c,k)) =
+  let INST theta (Sequent(asl,c,k) as th) = if theta = [] then th else
     let inst_fun = vsubst theta in
     new_theorem (term_image inst_fun asl) (inst_fun c) (Pinst(k,theta))