original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/offline/README	Sat Jan 18 16:26:43 2025 +0100
@@ -0,0 +1,12 @@
+* Compile and run "offline/offline.ml" (warning, this uses a lot of memory)
+
+  ocamlopt offline.ml -o offline
+  > maps.lst
+  ./offline
+
+* Format of maps.lst:
+
+  - THM1 THM2   map HOL Light THM1 to Isabelle/HOL THM2 and forget its deps
+  - THM -       do not record THM and make sure it is not used (its deps must be mapped)
+  - THM         the definition of constant/type is mapped in Isabelle/HOL, so forget
+                its deps and look its map up when defining (may fail at import time)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/offline/maps.lst	Sat Jan 18 16:26:43 2025 +0100
@@ -0,0 +1,230 @@
+T_DEF
+AND_DEF
+IMP_DEF
+FORALL_DEF
+EXISTS_DEF
+OR_DEF
+F_DEF
+NOT_DEF
+EXISTS_UNIQUE_DEF
+_FALSITY_
+ETA_AX        hl_ax1
+SELECT_AX     hl_ax2
+COND_DEF
+DEF_o
+I_DEF
+TYDEF_1
+one_DEF
+DEF_mk_pair
+TYDEF_prod
+DEF_,
+DEF_FST
+DEF_SND
+DEF_CURRY     -
+CURRY_DEF     CURRY_DEF
+DEF_ONE_ONE
+DEF_ONTO
+INFINITY_AX   hl_ax3
+TYDEF_num     -
+ZERO_DEF      -
+DEF_SUC       -
+SUC_DEF       -
+NOT_SUC       NOT_SUC
+SUC_INJ       SUC_INJ
+num_INDUCTION num_INDUCTION
+DEF_NUMERAL
+num_Axiom     num_Axiom
+DEF_BIT0
+DEF_BIT1
+DEF_PRE       -
+PRE           PRE
+DEF_+         -
+ADD           ADD
+DEF_*         -
+MULT          MULT
+DEF_EXP       -
+EXP           EXP
+DEF_<=        -
+LE            LE
+DEF_<         -
+LT            LT
+DEF_>=
+DEF_>
+DEF_MAX
+DEF_MIN
+DEF_EVEN      -
+EVEN          EVEN
+DEF_-         -
+SUB           SUB
+DEF_FACT      -
+FACT          FACT
+DEF_DIV       -
+DEF_MOD       -
+DIVISION_0    DIVISION_0
+TYDEF_sum     -
+DEF_INL       -
+DEF_INR       -
+sum_RECURSION sum_RECURSION
+sum_INDUCT    sum_INDUCT
+DEF_OUTL      -
+OUTL          OUTL
+DEF_OUTR      -
+OUTR          OUTR
+TYDEF_list    -
+DEF_NIL       -
+DEF_CONS      -
+list_RECURSION list_RECURSION
+list_INDUCT   list_INDUCT
+DEF_HD        -
+HD            HD
+DEF_TL        -
+TL            TL
+DEF_APPEND    -
+APPEND        APPEND
+DEF_REVERSE   -
+REVERSE_conjunct0 REVERSE(0)
+REVERSE_conjunct1 REVERSE(1)
+DEF_LENGTH    -
+LENGTH        LENGTH
+DEF_MAP       -
+MAP           MAP
+DEF_LAST      -
+LAST          LAST
+DEF_BUTLAST   -
+BUTLAST_conjunct0 BUTLAST(0)
+BUTLAST_conjunct1 BUTLAST(1)
+DEF_REPLICATE -
+REPLICATE_conjunct0 REPLICATE(0)
+REPLICATE_conjunct1 REPLICATE(1)
+DEF_NULL      -
+NULL_conjunct0 NULL(0)
+NULL_conjunct1 NULL(1)
+DEF_ALL       -
+ALL_conjunct0 ALL(0)
+ALL_conjunct1 ALL(1)
+DEF_EX        -
+EX_conjunct0  EX(0)
+EX_conjunct1  EX(1)
+DEF_ITLIST    -
+ITLIST_conjunct0 ITLIST(0)
+ITLIST_conjunct1 ITLIST(1)
+DEF_ALL2      -
+ALL2_DEF_conjunct0 ALL2_DEF(0)
+ALL2_DEF_conjunct1 ALL2_DEF(1)
+DEF_FILTER    -
+FILTER_conjunct0 FILTER(0)
+FILTER_conjunct1 FILTER(1)
+DEF_ZIP       -
+ZIP_DEF_conjunct0 -
+ZIP_DEF_conjunct1 -
+ZIP_DEF       -
+ZIP_conjunct0 ZIP(0)
+ZIP_conjunct1 ZIP(1)
+TYDEF_real -
+DEF_real_of_num -
+real_of_num -
+real_of_num_th -
+DEF_real_neg -
+real_neg -
+real_neg_th -
+DEF_real_add -
+real_add -
+real_add_th -
+DEF_real_mul -
+real_mul -
+real_mul_th -
+DEF_real_le -
+real_le -
+real_le_th -
+DEF_real_inv -
+real_inv -
+real_inv_th -
+REAL_ADD_SYM REAL_ADD_SYM
+REAL_ADD_ASSOC REAL_ADD_ASSOC
+REAL_ADD_LID REAL_ADD_LID
+REAL_ADD_LINV REAL_ADD_LINV
+REAL_MUL_SYM REAL_MUL_SYM
+REAL_MUL_ASSOC REAL_MUL_ASSOC
+REAL_MUL_LID REAL_MUL_LID
+REAL_ADD_LDISTRIB REAL_ADD_LDISTRIB
+REAL_LE_REFL REAL_LE_REFL
+REAL_LE_ANTISYM REAL_LE_ANTISYM
+REAL_LE_TRANS REAL_LE_TRANS
+REAL_LE_TOTAL REAL_LE_TOTAL
+REAL_LE_LADD_IMP REAL_LE_LADD_IMP
+REAL_LE_MUL REAL_LE_MUL
+REAL_OF_NUM_LE REAL_OF_NUM_LE
+DEF_real_sub -
+real_sub real_sub
+DEF_real_lt -
+real_lt real_lt
+DEF_real_ge -
+real_ge real_ge
+DEF_real_gt -
+real_gt real_gt
+DEF_real_abs -
+real_abs real_abs
+DEF_real_pow -
+REAL_POLY_CLAUSES_conjunct9 REAL_POLY_CLAUSES_conjunct9
+REAL_POLY_CLAUSES_conjunct8 REAL_POLY_CLAUSES_conjunct8
+DEF_real_div -
+real_div real_div
+DEF_real_max -
+real_max real_max
+DEF_real_min -
+real_min real_min
+DEF_real_sgn -
+real_sgn real_sgn
+REAL_HREAL_LEMMA1 -
+REAL_HREAL_LEMMA2 -
+REAL_COMPLETE_SOMEPOS REAL_COMPLETE_SOMEPOS
+REAL_OF_NUM_MUL REAL_OF_NUM_MUL
+REAL_OF_NUM_ADD REAL_OF_NUM_ADD
+REAL_OF_NUM_EQ REAL_OF_NUM_EQ
+REAL_INV_0 REAL_INV_0
+REAL_MUL_LINV REAL_MUL_LINV
+TYDEF_int -
+DEF_integer -
+integer integer
+int_rep int_rep
+int_abstr int_abstr
+dest_int_rep dest_int_rep
+int_eq int_eq
+DEF_int_le -
+int_le     int_le
+DEF_int_ge -
+int_ge     int_ge
+DEF_int_lt -
+int_lt     int_lt
+DEF_int_gt -
+int_gt     int_gt
+DEF_int_of_num -
+int_of_num int_of_num
+int_of_num_th int_of_num_th
+int_neg    -
+int_neg_th int_neg_th
+DEF_int_add -
+int_add    -
+int_add_th int_add_th
+DEF_int_sub -
+int_sub    -
+int_sub_th int_sub_th
+DEF_int_mul -
+int_mul    -
+int_mul_th int_mul_th
+DEF_int_abs -
+int_abs    -
+int_abs_th int_abs_th
+DEF_int_sgn -
+int_sgn    -
+int_sgn_th int_sgn_th
+DEF_int_max -
+int_max    -
+int_max_th int_max_th
+DEF_int_min -
+int_min    -
+int_min_th int_min_th
+DEF_int_pow -
+int_pow    -
+int_pow_th int_pow_th
+INT_IMAGE INT_IMAGE

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/offline/offline.ml	Sat Jan 18 16:26:43 2025 +0100
@@ -0,0 +1,298 @@
+let output_int oc i = output_string oc (string_of_int i);;
+let string_list_of_string str sep =
+  let rec slos_aux str ans =
+    if str = "" then ans else
+    try
+      let first_space = String.index str sep in
+      if first_space = 0 then
+        slos_aux (String.sub str 1 (String.length str - 1)) ans
+      else
+        slos_aux
+          (String.sub str (first_space + 1)(String.length str - 1 - first_space))
+          ((String.sub str 0 (first_space)) :: ans)
+    with
+      Not_found ->
+        List.rev (str :: ans)
+  in slos_aux str []
+;;
+
+module SM = Map.Make(struct type t = string let compare = compare end);;
+module IM = Map.Make(struct type t = int let compare = compare end);;
+let facts = ref SM.empty;;
+let maps = ref IM.empty;;
+let facts_rev = ref IM.empty;;
+
+let rec addfact s n =
+  if SM.mem s (!facts) then failwith ("addfact:" ^ s) else
+  if IM.mem n (!facts_rev) then () else (
+  facts := SM.add s n (!facts);
+  facts_rev := IM.add n s (!facts_rev));;
+
+let read_facts () =
+  let inc = open_in "facts.lst" in
+  (try
+    while true do
+      let l = (string_list_of_string (input_line inc) ' ') in
+      let no = int_of_string (List.nth l 1) in
+      addfact (List.hd l) no
+    done
+  with End_of_file -> close_in inc);
+  (let inc = open_in "maps.lst" in
+  try
+    while true do
+      let (hl_name :: t) = (string_list_of_string (input_line inc) ' ') in
+      let no = try SM.find hl_name (!facts) with Not_found -> failwith ("read facts: " ^ hl_name) in
+      facts := SM.remove hl_name (!facts);
+      let isa_name = if t = [] then "" else List.hd t in
+      maps := IM.add no isa_name (!maps);
+    done
+  with End_of_file -> close_in inc);;
+
+let tyno = ref 0;;
+let tmno = ref 0;;
+let thno = ref 0;;
+let ios s = abs(int_of_string s);;
+
+let process thth thtm tmtm thty tmty tyty = function
+  ('R', [t]) -> incr thno; thtm (ios t)
+| ('B', [t]) -> incr thno; thtm (ios t)
+| ('T', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('C', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('L', [t; p]) -> incr thno; thth (ios p); thtm (ios t)
+| ('H', [t]) -> incr thno; thtm (ios t)
+| ('E', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('D', [p; q]) -> incr thno; thth (ios p); thth (ios q)
+| ('Q', ((h :: t) as l)) -> incr thno; thth (ios (List.hd (List.rev l)));
+    List.iter thty (List.map ios (List.tl (List.rev l)))
+| ('S', ((h :: t) as l)) -> incr thno; thth (ios (List.hd (List.rev l)));
+    List.iter thtm (List.map ios (List.tl (List.rev l)))
+| ('A', [_; t]) -> incr thno; thtm (ios t)
+| ('F', [_; t]) -> incr thno; thtm (ios t)
+| ('Y', [_; _; _; t; s; p]) -> incr thno; thth (ios p); thtm (ios t); thtm (ios s)
+| ('1', [p]) -> incr thno; thth (ios p)
+| ('2', [p]) -> incr thno; thth (ios p)
+| ('t', [_]) -> incr tyno
+| ('a', (h :: t)) -> incr tyno; List.iter tyty (List.map ios t)
+| ('v', [_; ty]) -> incr tmno; tmty (ios ty)
+| ('c', [_; ty]) -> incr tmno; tmty (ios ty)
+| ('f', [t; s]) -> incr tmno; tmtm (ios t); tmtm (ios s)
+| ('l', [t; s]) -> incr tmno; tmtm (ios t); tmtm (ios s)
+| (c, l) -> failwith ((String.make 1 c) ^ (String.concat " " l))
+;;
+
+let thth = Array.create 155097624 [];;
+let tmth = Array.create 55000000 [];;
+let tmtm = Array.create 55000000 [];;
+let tyth = Array.create 200000 [];;
+let tytm = Array.create 200000 [];;
+let tyty = Array.create 200000 [];;
+
+let needth no = not (IM.mem no !maps);;
+
+let addthth s = if needth !thno then thth.(s) <- !thno :: thth.(s);;
+let addtmth s = if needth !thno then tmth.(s) <- !thno :: tmth.(s);;
+let addtyth s = if needth !thno then tyth.(s) <- !thno :: tyth.(s);;
+let addtmtm s = tmtm.(s) <- !tmno :: tmtm.(s);;
+let addtytm s = tytm.(s) <- !tmno :: tytm.(s);;
+let addtyty s = tyty.(s) <- !tyno :: tyty.(s);;
+
+let add_facts_deps () =
+  thth.(0) <- 0 :: thth.(0);
+  SM.iter (fun _ n -> thth.(n) <- 0 :: thth.(n)) !facts
+;;
+
+let process_all thth thtm tmtm thty tmty tyty =
+  tyno := 0; tmno := 0; thno := 0;
+  let inc = open_in "proofs" in
+  try while true do
+      let c = input_char inc in
+      let s = input_line inc in
+      process thth thtm tmtm thty tmty tyty (c, (string_list_of_string s ' '))
+    done
+  with End_of_file -> close_in inc;;
+
+let count_nonnil l =
+  Array.fold_left (fun n l -> if l = [] then n else n + 1) 0 l;;
+
+let clean tab filter =
+  for i = Array.length tab - 1 downto 1 do
+    tab.(i) <- List.filter filter tab.(i)
+  done;;
+
+let clean_all () =
+  clean thth (fun j -> not (thth.(j) = []));
+  clean tmth (fun j -> not (thth.(j) = []));
+  clean tmtm (fun j -> not (tmth.(j) = [] && tmtm.(j) = []));
+  clean tyth (fun j -> not (thth.(j) = []));
+  clean tytm (fun j -> not (tmth.(j) = [] && tmtm.(j) = []));
+  clean tyty (fun j -> not (tyth.(j) = [] && tytm.(j) = [] && tyty.(j) = []))
+;;
+
+read_facts ();;
+let facts_rev = !facts_rev;;
+add_facts_deps ();;
+process_all addthth addtmth addtmtm addtyth addtytm addtyty;;
+
+print_string "thms: "; print_int !thno;
+print_string " tms: "; print_int !tmno;
+print_string " tys: "; print_int !tyno; print_newline (); flush stdout;;
+print_string "Direct uses: th->th th->tm tm->tm th->ty tm->ty ty->ty: \n";
+print_int (count_nonnil thth); print_char ' ';
+print_int (count_nonnil tmth); print_char ' ';
+print_int (count_nonnil tmtm); print_char ' ';
+print_int (count_nonnil tyth); print_char ' ';
+print_int (count_nonnil tytm); print_char ' ';
+print_int (count_nonnil tyty); print_newline (); flush stdout;;
+clean_all ();;
+
+print_string "After removing:\n";
+print_string "Depends: th->th th->tm tm->tm th->ty tm->ty ty->ty: \n";
+print_int (count_nonnil thth); print_char ' ';
+print_int (count_nonnil tmth); print_char ' ';
+print_int (count_nonnil tmtm); print_char ' ';
+print_int (count_nonnil tyth); print_char ' ';
+print_int (count_nonnil tytm); print_char ' ';
+print_int (count_nonnil tyty); print_newline (); flush stdout;;
+
+let rev_tables () =
+  let rev_tab t =
+    for i = 0 to Array.length t - 1 do
+      t.(i) <- List.rev (t.(i));
+    done
+  in
+  rev_tab thth; rev_tab tmth; rev_tab tyth;
+  rev_tab tmtm; rev_tab tytm; rev_tab tyty
+;;
+print_char 'c'; flush stdout;;
+rev_tables ();;
+print_char 'C'; flush stdout;;
+
+let othnth = Array.create 155300000 0;;
+let otmntm = Array.create 55000000 0;;
+let otynty = Array.create 200000 0;;
+
+let outl oc tag ss is =
+  let ss = ss @ (List.map string_of_int is) in
+  output_char oc tag; output_string oc (String.concat " " ss); output_char oc '\n'
+;;
+let ntyno = ref 0;; let ntmno = ref 0;; let nthno = ref 0;;
+let ty t i = (*!ntyno -*)
+  t.(i) <- List.tl t.(i);
+  if tyth.(i) = [] && tytm.(i) = [] && tyty.(i) = [] then (- otynty.(i)) else otynty.(i);;
+let tm t i = (*!ntmno -*)
+  t.(i) <- List.tl t.(i);
+  if tmth.(i) = [] && tmtm.(i) = [] then (- otmntm.(i)) else otmntm.(i);;
+let th i = (*!nthno -*)
+(*  (if List.hd thth.(i) = 0 then (print_int !thno));*)
+  thth.(i) <- List.tl thth.(i);
+  if thth.(i) = [] then (- othnth.(i)) else othnth.(i);;
+
+let rec itlist f l b =
+  match l with
+    [] -> b
+  | (h::t) -> f h (itlist f t b);;
+
+let insert x l =
+  if List.mem x l then l else x::l;;
+
+let union l1 l2 = itlist insert l1 l2;;
+
+let rec neededby l acc =
+  match l with [] -> acc
+  | h :: t ->
+      try if List.length acc > 10 then acc else
+        neededby t (insert (IM.find h facts_rev) acc)
+      with Not_found -> neededby (union thth.(h) t) acc
+;;
+let neededby l = String.concat " " (neededby l [])
+
+let outt oc tag ss tys tms ths =
+  if thth.(!thno) = [] then () else
+  begin
+    incr nthno;
+    othnth.(!thno) <- !nthno;
+    begin
+      try
+        let s = IM.find (!thno) (!maps) in
+        if s = "-" then failwith ("removed thm:" ^ IM.find !thno facts_rev ^ " around:" ^ neededby (thth.(!thno)))
+        else if s = "" then outl oc tag ss []
+        else outl oc 'M' [s] []
+      with Not_found ->
+        outl oc tag ss
+          (List.map (fun i -> ty tyth (ios i)) tys @ List.map
+          (fun i -> tm tmth (ios i)) tms @ List.map (fun i -> th (ios i)) ths)
+    end;
+    try outl oc '+' [IM.find (!thno) facts_rev] []
+    with Not_found -> ()
+  end
+;;
+
+let outtm oc tag ss tys tms =
+  if tmth.(!tmno) = [] && tmtm.(!tmno) = [] then () else
+  (incr ntmno; otmntm.(!tmno) <- !ntmno; outl oc tag ss (List.map (fun i -> ty tytm (ios i)) tys @ List.map (fun i -> tm tmtm (ios i)) tms))
+;;
+
+let outty oc tag ss tys =
+  if tyth.(!tyno) = [] && tytm.(!tyno) = [] && tyty.(!tyno) = [] then () else
+  (incr ntyno; otynty.(!tyno) <- !ntyno; outl oc tag ss (List.map (fun i -> ty tyty (ios i)) tys))
+;;
+
+let printer oc = function
+  ('R', [t]) -> incr thno; outt oc 'R' [] [] [t] []
+| ('B', [t]) -> incr thno; outt oc 'B' [] [] [t] []
+| ('T', [p; q]) -> incr thno; outt oc 'T' [] [] [] [p; q]
+| ('C', [p; q]) -> incr thno; outt oc 'C' [] [] [] [p; q]
+| ('L', [t; p]) -> incr thno; outt oc 'L' [] [] [t] [p]
+| ('H', [t]) -> incr thno; outt oc 'H' [] [] [t] []
+| ('E', [p; q]) -> incr thno; outt oc 'E' [] [] [] [p; q]
+| ('D', [p; q]) -> incr thno; outt oc 'D' [] [] [] [p; q]
+| ('Q', ((h :: t) as l)) -> incr thno;
+    let (th, tys) = (List.hd (List.rev l), List.rev (List.tl (List.rev l))) in
+    outt oc 'Q' [] tys [] [th]
+| ('S', ((h :: t) as l)) -> incr thno;
+    let (th, tms) = (List.hd (List.rev l), List.rev (List.tl (List.rev l))) in
+    outt oc 'S' [] [] tms [th]
+| ('A', [n; t]) -> incr thno; outt oc 'A' [n] [] [t] []
+| ('F', [n; t]) -> incr thno; outt oc 'F' [n] [] [t] []
+| ('Y', [n1; n2; n3; t; s; p]) -> incr thno; outt oc 'Y' [n1; n2; n3] [] [t; s] [p]
+| ('1', [p]) -> incr thno; outt oc '1' [] [] [] [p]
+| ('2', [p]) -> incr thno; outt oc '2' [] [] [] [p]
+| ('t', [n]) -> incr tyno; outty oc 't' [n] []
+| ('a', (h :: t)) -> incr tyno; outty oc 'a' [h] t
+| ('v', [n; ty]) -> incr tmno; outtm oc 'v' [n] [ty] []
+| ('c', [n; ty]) -> incr tmno; outtm oc 'c' [n] [ty] []
+| ('f', [t; s]) -> incr tmno; outtm oc 'f' [] [] [t; s]
+| ('l', [t; s]) -> incr tmno; outtm oc 'l' [] [] [t; s]
+| (c, l) -> failwith ((String.make 1 c) ^ (String.concat " " l))
+;;
+
+let print_all () =
+  tyno := 0; tmno := 0; thno := 0;
+  let inc = open_in "proofs" in
+  let oc = open_out "proofsN" in
+  try while true do
+      let c = input_char inc in
+      let s = input_line inc in
+      printer oc (c, string_list_of_string s ' ')
+    done
+  with End_of_file -> (close_in inc; close_out oc);;
+
+print_all ();;
+
+print_string "thms: "; print_int !nthno;
+print_string " tms: "; print_int !ntmno;
+print_string " tys: "; print_int !ntyno; print_newline (); flush stdout;;
+
+let inc = open_in "facts.lst" in
+let oc = open_out "facts.lstN" in
+try
+  while true do
+    let [name; no] = string_list_of_string (input_line inc) ' ' in
+    let no = int_of_string no in
+    try if IM.find no facts_rev = name then (
+    output_string oc name; output_char oc ' ';
+    output_int oc othnth.(no); output_char oc '\n'
+    ) else ()
+    with Not_found -> ()
+  done
+  with End_of_file -> (close_in inc; close_out oc);;