# HG changeset patch # User paulson # Date 1114088724 -7200 # Node ID 4cb16144c81b113177236284f1878afa57e8c489 # Parent ebcbffebdf973430c1beaf9f42f2c3acb85587b5 added hearder lines and deleted some redundant material diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,4 +1,5 @@ (* Title: SpassCommunication.ml + ID: $Id$ Author: Claire Quigley Copyright 2004 University of Cambridge *) diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/VampireCommunication.ML --- a/src/HOL/Tools/ATP/VampireCommunication.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/VampireCommunication.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,4 +1,5 @@ (* Title: VampireCommunication.ml + ID: $Id$ Author: Claire Quigley Copyright 2004 University of Cambridge *) diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/modUnix.ML --- a/src/HOL/Tools/ATP/modUnix.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/modUnix.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,3 +1,7 @@ +(* ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) (****************************************************************) (****** Slightly modified version of sml Unix structure *********) @@ -21,10 +25,10 @@ end fun fdReader (name : string, fd : Posix.IO.file_desc) = - Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd }; + Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; fun fdWriter (name, fd) = - Posix.IO.mkWriter { + Posix.IO.mkTextWriter { appendMode = false, initBlkMode = true, name = name, diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/recon_order_clauses.ML --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,3 +1,8 @@ +(* ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) + (*----------------------------------------------*) (* Reorder clauses for use in binary resolution *) (*----------------------------------------------*) diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,3 +1,8 @@ +(* ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) + (*use "Translate_Proof";*) (* Parsing functions *) diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/recon_prelim.ML --- a/src/HOL/Tools/ATP/recon_prelim.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_prelim.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,13 +1,7 @@ - - -Goal "A -->A"; -by Auto_tac; -qed "foo"; - - -val Mainsign = #sign (rep_thm foo); - - +(* ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) val gcounter = ref 0; @@ -35,19 +29,6 @@ fun getstring (Var (v,T)) = fst v |getstring (Free (v,T))= v; - - -fun alltrue [] = true - |alltrue (true::xs) = true andalso (alltrue xs) - |alltrue (false::xs) = false; - -fun allfalse [] = true - |allfalse (false::xs) = true andalso (allfalse xs) - |allfalse (true::xs) = false; - -fun not_empty [] = false - | not_empty _ = true; - fun twoisvar (a,b) = is_Var b; fun twoisfree (a,b) = is_Free b; fun twoiscomb (a,b) = iscomb b; @@ -86,7 +67,7 @@ true else let val (f, args) = strip_comb t in - if ((is_Free f) orelse (is_Var f)) andalso (alltrue (map is_hol_tm args)) then + if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then true (* should be is_const *) else false @@ -115,7 +96,7 @@ end else if (iscomb f) then let val (P, args) = strip_comb f in - ((is_hol_tm P)) andalso (alltrue (map is_hol_fm args)) + ((is_hol_tm P)) andalso (forall is_hol_fm args) end else is_hol_tm f; (* should be is_const, nee @@ -195,31 +176,9 @@ fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]); -exception powerError; -fun power (x, n) = if x = 0 andalso n = 0 - then raise powerError - else if n = 0 - then 1 - else x * power (x, n-1); - - -fun get_tens n = power(10, (n-1)) - - -fun digits_to_int [] posn n = n -| digits_to_int (x::xs) posn n = let - val digit_val = ((ord x) - 48)*(get_tens posn) - in - digits_to_int xs (posn -1 )(n + digit_val) - end; - -fun int_of_string str = let - val digits = explode str - val posn = length digits - in - digits_to_int digits posn 0 - end - - +fun int_of_string str = valOf (Int.fromString str) + handle Option => error ("int_of_string: " ^ str); + + exception ASSERTION of string; diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,3 +1,8 @@ +(* ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) + (******************) (* complete later *) (******************) @@ -23,15 +28,6 @@ end -fun thm_of_string str = let val _ = set show_sorts - val term = read str - val propterm = HOLogic.mk_Trueprop term - val cterm = cterm_of Mainsign propterm - val _ = reset show_sorts - in - assume cterm - end - (* check separate args in the watcher program for separating strings with a * or ; or something *) fun clause_strs_to_string [] str = str diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,4 +1,7 @@ - +(* ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) fun add_in_order (x:string) [] = [x] | add_in_order (x:string) ((y:string)::ys) = if (x < y) diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,3 +1,8 @@ +(* ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge +*) + (* Get claset rules *) diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Thu Apr 21 15:05:24 2005 +0200 @@ -1,7 +1,7 @@ - - (* Title: Watcher.ML - Author: Claire Quigley - Copyright 2004 University of Cambridge +(* Title: Watcher.ML + ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge *) (***************************************************************************) diff -r ebcbffebdf97 -r 4cb16144c81b src/HOL/Tools/ATP/watcher.sig --- a/src/HOL/Tools/ATP/watcher.sig Thu Apr 21 13:15:25 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.sig Thu Apr 21 15:05:24 2005 +0200 @@ -1,5 +1,4 @@ - -(* Title: Watcher.ML +(* ID: $Id$ Author: Claire Quigley Copyright 2004 University of Cambridge *) @@ -14,7 +13,7 @@ signature WATCHER = - sig +sig (*****************************************************************************************) (* Send request to Watcher for multiple spasses to be called for filenames in arg *)