src/HOL/Import/patches/patch2

clarified patches: avoid duplication;

--- hol-light/fusion.ml	2025-01-18 11:11:28.417955236 +0100
+++ hol-light-patched/fusion.ml	2025-01-18 11:12:11.384276293 +0100
@@ -9,6 +9,18 @@
 
 needs "lib.ml";;
 
+#load "unix.cma";;
+let poutc = Unix.open_process_out "buffer | gzip -c > proofs.gz";;
+let foutc = open_out "facts.lst";;
+let stop_recording () = close_out poutc; close_out foutc;;
+
+let rec outl = function
+  [] -> ()
+| (h :: t) -> try
+    output_string poutc h; List.fold_left
+      (fun () e -> output_char poutc ' '; output_string poutc e) () t
+    with Sys_error _ -> ();;
+
 module type Hol_kernel =
   sig
       type hol_type = private
@@ -101,7 +113,165 @@
             | Comb of term * term
             | Abs of term * term
 
-  type thm = Sequent of (term list * term)
+  type thm = Sequent of (term list * term * int)
+(* PROOFRECORDING BEGIN *)
+let thms = Hashtbl.create 20000;;
+
+let inc = open_in "theorems";;
+let l = ((input_value inc) : ((string * (term list * term)) list));;
+close_in inc;;
+List.iter (fun (n,t) -> Hashtbl.replace thms t (n, 0)) l;;
+print_endline ("Read in: " ^ string_of_int (Hashtbl.length thms));;
+
+module Fm = Map.Make(struct type t = float let compare = compare end);;
+module Tys = Map.Make(struct type t = hol_type let compare = compare end);;
+module Tms = Map.Make(struct type t = term let compare = compare end);;
+module Ps = Map.Make(struct type t = (term list * term) let compare = compare end);;
+
+let ty_no = ref 0;;
+let tys = ref Tys.empty;;
+
+let rec out_type ty =
+  try
+    Tys.find ty !tys
+  with Not_found ->
+    match ty with
+      Tyvar t ->
+        incr ty_no; tys := Tys.add ty !ty_no !tys;
+        output_char poutc 't'; output_string poutc t; output_char poutc '\n';
+        !ty_no
+    | Tyapp (id, tl) ->
+        let tln = map out_type tl in
+        incr ty_no; tys := Tys.add ty !ty_no !tys;
+        output_char poutc 'a'; output_string poutc id; output_char poutc ' ';
+          outl (map string_of_int tln); output_char poutc '\n';
+        !ty_no;;
+
+let tm_no = ref 0;;
+let tms = ref Tms.empty;;
+let tms_prio = ref Fm.empty;;
+let tms_size = ref 0;;
+let tms_maxsize = ref (int_of_string (Sys.getenv "MAXTMS"));;
+let tm_lookup tm =
+  let (ret, oldtime) = Tms.find tm !tms in
+  let newtime = Unix.gettimeofday () in
+  tms := Tms.add tm (ret, newtime) !tms;
+  tms_prio := Fm.add newtime tm (Fm.remove oldtime !tms_prio);
+  ret;;
+
+let tm_delete () =
+  let (time, tm) = Fm.min_binding !tms_prio in
+  tms := Tms.remove tm !tms;
+  tms_prio := Fm.remove time !tms_prio;
+  decr tms_size; ();;
+
+let tm_add tm no =
+  while (!tms_size > !tms_maxsize) do tm_delete (); done;
+  let newtime = Unix.gettimeofday () in
+  tms := Tms.add tm (no, newtime) (!tms);
+  tms_prio := Fm.add newtime tm (!tms_prio);
+  incr tms_size; ();;
+
+let rec out_term tm =
+  try
+    tm_lookup tm
+  with Not_found ->
+    let outc = output_char poutc and out = output_string poutc in
+    match tm with
+      Var (name, ty) ->
+        let ty = out_type ty in
+        incr tm_no; tm_add tm !tm_no;
+        outc 'v'; out name; outc ' '; out (string_of_int ty); outc '\n';
+        !tm_no
+    | Const (name, ty) ->
+        let ty = out_type ty in
+        incr tm_no; tm_add tm !tm_no;
+        outc 'c'; out name; outc ' '; out (string_of_int ty); outc '\n';
+        !tm_no
+    | Comb (f, a) ->
+        let f = out_term f and a = out_term a in
+        incr tm_no; tm_add tm !tm_no;
+        outc 'f'; out (string_of_int f); outc ' '; out (string_of_int a); outc '\n';
+        !tm_no
+    | Abs (x, a) ->
+        let x = out_term x and a = out_term a in
+        incr tm_no; tm_add tm !tm_no;
+        outc 'l'; out (string_of_int x); outc ' '; out (string_of_int a); outc '\n';
+        !tm_no
+;;
+
+let prf_no = ref 0;;
+let outt tag ss tys tms pfs =
+  let tys = map out_type tys and
+      tms = map out_term tms in
+  try
+    output_char poutc tag;
+    outl (ss @ (map string_of_int tys)
+           @ (map string_of_int tms)
+           @ (map string_of_int pfs));
+    output_char poutc '\n'
+  with Sys_error _ -> ()
+;;
+
+let ps = ref Ps.empty;;
+
+let p_lookup p = Ps.find p !ps;;
+let p_add p no = ps := Ps.singleton p no;;
+
+let mk_prff f = incr prf_no; f (); !prf_no;;
+
+let chk_mk_prff f th =
+  try p_lookup th
+  with Not_found ->
+  try
+    let (name, i) = Hashtbl.find thms th in
+    if i > 0 then i else
+    let i = mk_prff f in
+    (ps := Ps.empty;
+    Hashtbl.replace thms th (name, i);
+    (try output_string foutc (name ^ " " ^ string_of_int i ^ "\n"); flush foutc with Sys_error _ -> ());
+    i)
+  with Not_found ->
+    mk_prff (fun () -> f (); p_add th !prf_no);;
+
+
+let mk_prf t l1 l2 l3 l4 _ = mk_prff (fun () -> outt t l1 l2 l3 l4);;
+let chk_mk_prf t l1 l2 l3 l4 th = chk_mk_prff (fun () -> outt t l1 l2 l3 l4) th;;
+let proof_REFL t th = chk_mk_prf 'R' [] [] [t] [] th;;
+let proof_TRANS (p, q) th = chk_mk_prf 'T' [] [] [] [p; q] th;;
+let proof_MK_COMB (p, q) th = chk_mk_prf 'C' [] [] [] [p; q] th;;
+let proof_ABS x p th = chk_mk_prf 'L' [] [] [x] [p] th;;
+let proof_BETA t th = chk_mk_prf 'B' [] [] [t] [] th;;
+let proof_ASSUME t th = chk_mk_prf 'H' [] [] [t] [] th;;
+let proof_EQ_MP p q th = chk_mk_prf 'E' [] [] [] [p; q] th;;
+let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) th =
+  chk_mk_prf 'D' [] [] [] [p1; p2] th;;
+let rec explode_subst = function
+  [] -> []
+| ((y,x)::rest) -> x::y::(explode_subst rest);;
+let proof_INST_TYPE s p th = chk_mk_prf 'Q' [] (explode_subst s) [] [p] th;;
+let proof_INST s p th = chk_mk_prf 'S' [] [] (explode_subst s) [p] th;;
+
+let global_ax_counter = ref 0;;
+let new_axiom_name n = incr global_ax_counter; ("ax_" ^ n ^ "_" ^ string_of_int(!global_ax_counter));;
+let proof_new_axiom axname t th = chk_mk_prf 'A' [axname] [] [t] [] th;;
+let proof_new_definition cname t th =
+  chk_mk_prf 'F' [cname] [] [t] [] th;;
+let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) p th =
+  chk_mk_prf 'Y' [tyname; absname; repname] [] [pt; tt] [p] th;;
+let proof_CONJUNCT1 p th = chk_mk_prf '1' [] [] [] [p] th;;
+let proof_CONJUNCT2 p th = chk_mk_prf '2' [] [] [] [p] th;;
+
+let clean_ts_at_saved = ((try Sys.getenv "CLEANTMS" with _ -> "") = "YES");;
+
+let save_proof name p th =
+  Hashtbl.replace thms th (name, p);
+  ps := Ps.empty;
+  if clean_ts_at_saved then (
+    tms := Tms.empty; tms_prio := Fm.empty; tms_size := 0;
+   );
+  (try output_string foutc (name ^ " " ^ string_of_int p ^ "\n"); flush foutc with Sys_error _ -> ());;
+(* PROOFRECORDING END *)
 
 (* ------------------------------------------------------------------------- *)
 (* List of current type constants with their arities.                        *)
@@ -485,43 +655,48 @@
 (* Basic theorem destructors.                                                *)
 (* ------------------------------------------------------------------------- *)
 
-  let dest_thm (Sequent(asl,c)) = (asl,c)
+  let dest_thm (Sequent(asl,c,_)) = (asl,c)
 
-  let hyp (Sequent(asl,c)) = asl
+  let hyp (Sequent(asl,c,_)) = asl
 
-  let concl (Sequent(asl,c)) = c
+  let concl (Sequent(asl,c,_)) = c
 
 (* ------------------------------------------------------------------------- *)
 (* Basic equality properties; TRANS is derivable but included for efficiency *)
 (* ------------------------------------------------------------------------- *)
 
   let REFL tm =
-    Sequent([],safe_mk_eq tm tm)
+    let eq = safe_mk_eq tm tm in
+    Sequent([],eq,proof_REFL tm ([], eq))
 
-  let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
+  let TRANS (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
     match (c1,c2) with
       Comb((Comb(Const("=",_),_) as eql),m1),Comb(Comb(Const("=",_),m2),r)
-        when alphaorder m1 m2 = 0 -> Sequent(term_union asl1 asl2,Comb(eql,r))
+        when alphaorder m1 m2 = 0 ->
+          let (a, g) = (term_union asl1 asl2,Comb(eql,r)) in
+          Sequent (a, g, proof_TRANS (p1, p2) (a, g))
     | _ -> failwith "TRANS"
 
 (* ------------------------------------------------------------------------- *)
 (* Congruence properties of equality.                                        *)
 (* ------------------------------------------------------------------------- *)
 
-  let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) =
+  let MK_COMB(Sequent(asl1,c1,p1),Sequent(asl2,c2,p2)) =
      match (c1,c2) with
        Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2) ->
         (match type_of r1 with
            Tyapp("fun",[ty;_]) when compare ty (type_of r2) = 0
-             -> Sequent(term_union asl1 asl2,
-                        safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2)))
+             -> let (a, g) = (term_union asl1 asl2,
+                        safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2))) in
+                Sequent (a, g, proof_MK_COMB (p1, p2) (a,g))
          | _ -> failwith "MK_COMB: types do not agree")
      | _ -> failwith "MK_COMB: not both equations"
 
-  let ABS v (Sequent(asl,c)) =
+  let ABS v (Sequent(asl,c,p)) =
     match (v,c) with
       Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl)
-         -> Sequent(asl,safe_mk_eq (Abs(v,l)) (Abs(v,r)))
+         -> let eq = safe_mk_eq (Abs(v,l)) (Abs(v,r)) in
+            Sequent (asl,eq,proof_ABS v p (asl,eq))
     | _ -> failwith "ABS";;
 
 (* ------------------------------------------------------------------------- *)
@@ -531,7 +706,8 @@
   let BETA tm =
     match tm with
       Comb(Abs(v,bod),arg) when compare arg v = 0
-        -> Sequent([],safe_mk_eq tm bod)
+        -> let eq = safe_mk_eq tm bod in
+           Sequent([],eq,proof_BETA tm ([], eq))
     | _ -> failwith "BETA: not a trivial beta-redex"
 
 (* ------------------------------------------------------------------------- *)
@@ -539,30 +715,35 @@
 (* ------------------------------------------------------------------------- *)
 
   let ASSUME tm =
-    if compare (type_of tm) bool_ty = 0 then Sequent([tm],tm)
+    if compare (type_of tm) bool_ty = 0 then
+      Sequent([tm],tm,proof_ASSUME tm ([tm], tm))
     else failwith "ASSUME: not a proposition"
 
-  let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
+  let EQ_MP (Sequent(asl1,eq,p1)) (Sequent(asl2,c,p2)) =
     match eq with
       Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0
-        -> Sequent(term_union asl1 asl2,r)
+        -> let t = term_union asl1 asl2 in
+           Sequent(t,r,proof_EQ_MP p1 p2 (t,r))
     | _ -> failwith "EQ_MP"
 
-  let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
+  let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
     let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
-    Sequent(term_union asl1' asl2',safe_mk_eq c1 c2)
+    let (a,g) = (term_union asl1' asl2',safe_mk_eq c1 c2) in
+    Sequent (a, g, proof_DEDUCT_ANTISYM_RULE (p1,c1) (p2,c2) (a, g))
 
 (* ------------------------------------------------------------------------- *)
 (* Type and term instantiation.                                              *)
 (* ------------------------------------------------------------------------- *)
 
-  let INST_TYPE theta (Sequent(asl,c)) =
+  let INST_TYPE theta (Sequent(asl,c,p)) =
     let inst_fn = inst theta in
-    Sequent(term_image inst_fn asl,inst_fn c)
+    let (a, g) = (term_image inst_fn asl,inst_fn c) in
+    Sequent(a,g, proof_INST_TYPE theta p (a,g))
 
-  let INST theta (Sequent(asl,c)) =
+  let INST theta (Sequent(asl,c,p)) =
     let inst_fun = vsubst theta in
-    Sequent(term_image inst_fun asl,inst_fun c)
+    let (a, g) = (term_image inst_fun asl,inst_fun c) in
+    Sequent(a, g, proof_INST theta p (a,g))
 
 (* ------------------------------------------------------------------------- *)
 (* Handling of axioms.                                                       *)
@@ -574,8 +755,11 @@
 
   let new_axiom tm =
     if compare (type_of tm) bool_ty = 0 then
-      let th = Sequent([],tm) in
-       (the_axioms := th::(!the_axioms); th)
+      let axname = new_axiom_name "" in
+      let p = proof_new_axiom axname tm ([], tm) in
+      let th = Sequent([],tm,p) in
+       (the_axioms := th::(!the_axioms);
+        save_proof axname p ([], tm); th)
     else failwith "new_axiom: Not a proposition"
 
 (* ------------------------------------------------------------------------- *)
@@ -595,7 +779,10 @@
         else if not (subset (type_vars_in_term r) (tyvars ty))
         then failwith "new_definition: Type variables not reflected in constant"
         else let c = new_constant(cname,ty); Const(cname,ty) in
-             let dth = Sequent([],safe_mk_eq c r) in
+             let concl = safe_mk_eq c r in
+             let p = proof_new_definition cname r ([], concl) in
+             let dth = Sequent([],concl, p) in
+             save_proof ("DEF_"^cname) p ([], concl);
              the_definitions := dth::(!the_definitions); dth
     | Comb(Comb(Const("=",_),Const(cname,ty)),r) ->
       failwith ("new_basic_definition: '" ^ cname ^ "' is already defined")
@@ -614,7 +801,7 @@
 (* Where "abs" and "rep" are new constants with the nominated names.         *)
 (* ------------------------------------------------------------------------- *)
 
-  let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) =
+  let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c,p)) =
     if exists (can get_const_type) [absname; repname] then
       failwith "new_basic_type_definition: Constant(s) already in use" else
     if not (asl = []) then
@@ -634,9 +821,19 @@
     let abs = (new_constant(absname,absty); Const(absname,absty))
     and rep = (new_constant(repname,repty); Const(repname,repty)) in
     let a = Var("a",aty) and r = Var("r",rty) in
-    Sequent([],safe_mk_eq (Comb(abs,mk_comb(rep,a))) a),
-    Sequent([],safe_mk_eq (Comb(P,r))
-                          (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r))
+    let ax1 = safe_mk_eq (Comb(abs,mk_comb(rep,a))) a
+    and ax2 = safe_mk_eq (Comb(P,r)) (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r) in
+    let mk_binary s =
+      let c = mk_const(s,[]) in
+      fun (l,r) -> try mk_comb(mk_comb(c,l),r)
+                   with Failure _ -> failwith "tydef_mk_binary"
+    in
+    let axc = mk_binary "/\\" (ax1, ax2) in
+    let tp = proof_new_basic_type_definition tyname (absname, repname) (P,x) p ([], axc) in
+    let p1 = proof_CONJUNCT1 tp ([], ax1) in
+    let p2 = proof_CONJUNCT2 tp ([], ax2) in
+    save_proof ("TYDEF_" ^ tyname) tp ([], axc);
+    (Sequent([],ax1,p1), Sequent([],ax2,p2));;
 
 end;;