Quelle patch2 Sprache: SML

--- 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 = open_out "proofs";;
+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;;

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.