# HG changeset patch # User wenzelm # Date 1737214003 -3600 # Node ID b520eb5c82232059895c0fe94fd79c322431a419 # Parent 5b9aca9b073be19cb74ed1da3cb222d62748bb53 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); diff -r 5b9aca9b073b -r b520eb5c8223 src/HOL/Import/offline/README --- /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) diff -r 5b9aca9b073b -r b520eb5c8223 src/HOL/Import/offline/maps.lst --- /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 diff -r 5b9aca9b073b -r b520eb5c8223 src/HOL/Import/offline/offline.ml --- /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);;