--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/patches/patch1 Sat Jan 18 22:29:47 2025 +0100
@@ -0,0 +1,25 @@
+--- hol-light/statements.ml 1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/statements.ml 2025-01-18 11:12:11.185279392 +0100
+@@ -0,0 +1,15 @@
++let name2pairs acc (name, th) =
++ let acc =
++ if is_conj (concl th) then
++ let fold_fun (no, acc) th = (no + 1, (name ^ "_conjunct" ^ (string_of_int no), th) :: acc) in
++ snd (List.fold_left fold_fun (0, acc) (CONJUNCTS th))
++ else acc
++ in (name, th) :: acc
++;;
++let dump_theorems () =
++ let oc = open_out "theorems" in
++ let all_thms = List.fold_left name2pairs [] !theorems in
++ output_value oc (map (fun (a,b) -> (a, dest_thm b)) all_thms);
++ close_out oc
++;;
++dump_theorems ();;
+--- hol-light/stage1.ml 1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/stage1.ml 2025-01-18 11:12:11.185279392 +0100
+@@ -0,0 +1,4 @@
++#use "hol.ml";;
++#use "update_database.ml";;
++#use "statements.ml";;
++exit 0;;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/patches/patch2 Sat Jan 18 22:29:47 2025 +0100
@@ -0,0 +1,374 @@
+--- 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;;
+
+--- hol-light/stage1.ml 2025-01-18 11:12:11.373276465 +0100
++++ hol-light-patched/stage1.ml 1970-01-01 01:00:00.000000000 +0100
+@@ -1,4 +0,0 @@
+-#use "hol.ml";;
+-#use "update_database.ml";;
+-#use "statements.ml";;
+-exit 0;;
+--- hol-light/stage2.ml 1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/stage2.ml 2025-01-18 11:12:11.384276293 +0100
+@@ -0,0 +1,3 @@
++#use "hol.ml";;
++stop_recording ();;
++exit 0;;
--- a/src/HOL/Import/patches/stage1.patch Sat Jan 18 22:25:47 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
---- hol-light/statements.ml 1970-01-01 01:00:00.000000000 +0100
-+++ hol-light-patched/statements.ml 2025-01-18 11:12:11.185279392 +0100
-@@ -0,0 +1,15 @@
-+let name2pairs acc (name, th) =
-+ let acc =
-+ if is_conj (concl th) then
-+ let fold_fun (no, acc) th = (no + 1, (name ^ "_conjunct" ^ (string_of_int no), th) :: acc) in
-+ snd (List.fold_left fold_fun (0, acc) (CONJUNCTS th))
-+ else acc
-+ in (name, th) :: acc
-+;;
-+let dump_theorems () =
-+ let oc = open_out "theorems" in
-+ let all_thms = List.fold_left name2pairs [] !theorems in
-+ output_value oc (map (fun (a,b) -> (a, dest_thm b)) all_thms);
-+ close_out oc
-+;;
-+dump_theorems ();;
---- hol-light/stage1.ml 1970-01-01 01:00:00.000000000 +0100
-+++ hol-light-patched/stage1.ml 2025-01-18 11:12:11.185279392 +0100
-@@ -0,0 +1,4 @@
-+#use "hol.ml";;
-+#use "update_database.ml";;
-+#use "statements.ml";;
-+exit 0;;
--- a/src/HOL/Import/patches/stage2.patch Sat Jan 18 22:25:47 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,374 +0,0 @@
---- 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;;
-
---- hol-light/stage1.ml 2025-01-18 11:12:11.373276465 +0100
-+++ hol-light-patched/stage1.ml 1970-01-01 01:00:00.000000000 +0100
-@@ -1,4 +0,0 @@
--#use "hol.ml";;
--#use "update_database.ml";;
--#use "statements.ml";;
--exit 0;;
---- hol-light/stage2.ml 1970-01-01 01:00:00.000000000 +0100
-+++ hol-light-patched/stage2.ml 2025-01-18 11:12:11.384276293 +0100
-@@ -0,0 +1,3 @@
-+#use "hol.ml";;
-+stop_recording ();;
-+exit 0;;
--- a/src/Pure/Admin/component_hol_light.scala Sat Jan 18 22:25:47 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala Sat Jan 18 22:29:47 2025 +0100
@@ -15,8 +15,6 @@
val default_hol_light_rev = "Release-3.0.0"
val hol_import_dir: Path = Path.explode("~~/src/HOL/Import")
- def patch1: Path = hol_import_dir + Path.explode("patches/stage1.patch")
- def patch2: Path = hol_import_dir + Path.explode("patches/stage2.patch")
def build_hol_light_import(
only_offline: Boolean = false,
@@ -66,15 +64,15 @@
This is an export of primitive proofs from HOL Light """ + hol_light_rev + """.
The original repository """ + hol_light_url + """
-has been patched in 2 stages. The overall export process works like this:
+has been patched in 2 phases. The overall export process works like this:
cd hol-light
make
- patch -p1 < """ + patch1 + """
+ patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch1"
./ocaml-hol -I +compiler-libs stage1.ml
- patch -p1 < """ + patch2 + """
+ patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch2"
export MAXTMS=10000
./ocaml-hol -I +compiler-libs stage2.ml
@@ -116,20 +114,33 @@
File.set_executable(platform_dir + offline_exe)
- /* export */
+ if (!only_offline) {
+ /* clone repository */
- if (!only_offline) {
val hol_light_dir = tmp_dir + Path.basic("hol-light")
Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
progress = progress)
+
+ /* patches */
+
+ Isabelle_System.make_directory(component_dir.path + Path.basic("patches"))
+
+ def patch(n: Int, source: Boolean = false): Path =
+ (if (source) hol_import_dir else component_dir.path) + Path.explode("patches/patch" + n)
+
+ for (n <- List(1, 2)) Isabelle_System.copy_file(patch(n, source = true), patch(n))
+
+
+ /* export stages */
+
def run(n: Int, lines: String*): Unit = {
val title = "stage " + n
if (n > 0) progress.echo("Running " + title + " ...")
val start = Time.now()
progress.bash(cat_lines("set -e" :: opam_env :: lines.toList),
- cwd = hol_light_dir, echo = progress.verbose).check
+ cwd = hol_light_dir, echo = progress.verbose).check.timing
val elapsed = Time.now() - start
if (n > 0) {
@@ -139,10 +150,10 @@
run(0, "make")
run(1,
- "patch -p1 < " + File.bash_path(patch1),
+ "patch -p1 < " + File.bash_path(patch(1)),
"./ocaml-hol -I +compiler-libs stage1.ml")
run(2,
- "patch -p1 < " + File.bash_path(patch2),
+ "patch -p1 < " + File.bash_path(patch(2)),
"export MAXTMS=10000",
"./ocaml-hol -I +compiler-libs stage2.ml")
run(3,