Add check_axioms()

This patch adds `check_axioms()` which checks whether there are only three axioms,
`SELECT_AX` and `ETA_AX` in `class.ml` and `INFINITY_AX` in `nums.ml`, at the point of call.

This function is useful when one wants to check whether a proof did not introduce any new axiom. :)

This is backported from s2n-bignum (https://github.com/awslabs/s2n-bignum/blob/main/common/misc.ml#L17-L26).

hol_lib.ml

@@ -100,3 +100,15 @@ loads "sets.ml";;       (* Basic set theory                                  *)
 loads "iterate.ml";;    (* Iterated operations                               *)
 loads "cart.ml";;       (* Finite Cartesian products                         *)
 loads "define.ml";;     (* Support for general recursive definitions         *)
+
+
+(* ------------------------------------------------------------------------- *)
+(* Checks that no axiom other than those allowed by core libs are introduced *)
+(* ------------------------------------------------------------------------- *)
+
+let check_axioms () =
+  let basic_axioms = [INFINITY_AX; SELECT_AX; ETA_AX] in
+  let l = filter (fun th -> not (mem th basic_axioms)) (axioms()) in
+  if l <> [] then
+    let msg = "[" ^ (String.concat ", " (map string_of_thm l)) ^ "]" in
+    failwith ("check_axioms: " ^ msg);;

unit_tests.ml

@@ -26,4 +26,15 @@ assert (rhs (concl (NUM_COMPUTE_CONV `(\x. x + (1 + 2)) (3 + 4)`))
         = `10`);;
 (* Arguments are reduced when the fn is a constant. *)
 assert (rhs (concl (NUM_COMPUTE_CONV `(unknown_fn:num->num) (1+2)`))
-        = `(unknown_fn:num->num) 3`);;
+        = `(unknown_fn:num->num) 3`);;
+
+
+(* ------------------------------------------------------------------------- *)
+(* Test check_axioms.                                                        *)
+(* ------------------------------------------------------------------------- *)
+
+new_axiom `k = 1`;;
+try
+  check_axioms (); (* check_axioms must raise Failure *)
+  assert false;
+with Failure _ -> () | Assert_failure _ as e -> raise e;;