added hearder lines and deleted some redundant material
authorpaulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 157894cb16144c81b
parent 15788 ebcbffebdf97
child 15790 e68dab670fc5
added hearder lines and deleted some redundant material
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/VampireCommunication.ML
src/HOL/Tools/ATP/modUnix.ML
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_prelim.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/ATP/watcher.sig
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Apr 21 13:15:25 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Apr 21 15:05:24 2005 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4  (*  Title:      SpassCommunication.ml
     1.5 +    ID:         $Id$
     1.6      Author:     Claire Quigley
     1.7      Copyright   2004  University of Cambridge
     1.8  *)
     2.1 --- a/src/HOL/Tools/ATP/VampireCommunication.ML	Thu Apr 21 13:15:25 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/VampireCommunication.ML	Thu Apr 21 15:05:24 2005 +0200
     2.3 @@ -1,4 +1,5 @@
     2.4  (*  Title:      VampireCommunication.ml
     2.5 +    ID:         $Id$
     2.6      Author:     Claire Quigley
     2.7      Copyright   2004  University of Cambridge
     2.8  *)
     3.1 --- a/src/HOL/Tools/ATP/modUnix.ML	Thu Apr 21 13:15:25 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/modUnix.ML	Thu Apr 21 15:05:24 2005 +0200
     3.3 @@ -1,3 +1,7 @@
     3.4 +(*  ID:         $Id$
     3.5 +    Author:     Claire Quigley
     3.6 +    Copyright   2004  University of Cambridge
     3.7 +*)
     3.8  
     3.9  (****************************************************************)
    3.10  (****** Slightly modified version of sml Unix structure *********)
    3.11 @@ -21,10 +25,10 @@
    3.12  	end
    3.13  
    3.14  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    3.15 -	  Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
    3.16 +	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    3.17  
    3.18  fun fdWriter (name, fd) =
    3.19 -          Posix.IO.mkWriter {
    3.20 +          Posix.IO.mkTextWriter {
    3.21  	      appendMode = false,
    3.22                initBlkMode = true,
    3.23                name = name,  
     4.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Thu Apr 21 13:15:25 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Thu Apr 21 15:05:24 2005 +0200
     4.3 @@ -1,3 +1,8 @@
     4.4 +(*  ID:         $Id$
     4.5 +    Author:     Claire Quigley
     4.6 +    Copyright   2004  University of Cambridge
     4.7 +*)
     4.8 +
     4.9  (*----------------------------------------------*)
    4.10  (* Reorder clauses for use in binary resolution *)
    4.11  (*----------------------------------------------*)
     5.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Apr 21 13:15:25 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Apr 21 15:05:24 2005 +0200
     5.3 @@ -1,3 +1,8 @@
     5.4 +(*  ID:         $Id$
     5.5 +    Author:     Claire Quigley
     5.6 +    Copyright   2004  University of Cambridge
     5.7 +*)
     5.8 +
     5.9  (*use "Translate_Proof";*)
    5.10  (* Parsing functions *)
    5.11  
     6.1 --- a/src/HOL/Tools/ATP/recon_prelim.ML	Thu Apr 21 13:15:25 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/recon_prelim.ML	Thu Apr 21 15:05:24 2005 +0200
     6.3 @@ -1,13 +1,7 @@
     6.4 -
     6.5 -
     6.6 -Goal "A -->A";
     6.7 -by Auto_tac;
     6.8 -qed "foo";
     6.9 -
    6.10 -
    6.11 -val Mainsign = #sign (rep_thm foo);
    6.12 -
    6.13 -
    6.14 +(*  ID:         $Id$
    6.15 +    Author:     Claire Quigley
    6.16 +    Copyright   2004  University of Cambridge
    6.17 +*)
    6.18  
    6.19  val gcounter = ref 0; 
    6.20  
    6.21 @@ -35,19 +29,6 @@
    6.22  fun getstring (Var (v,T)) = fst v
    6.23     |getstring (Free (v,T))= v;
    6.24  
    6.25 -
    6.26 -
    6.27 -fun alltrue [] = true
    6.28 -   |alltrue (true::xs) = true andalso (alltrue xs)
    6.29 -   |alltrue (false::xs) = false;
    6.30 -
    6.31 -fun allfalse [] = true
    6.32 -   |allfalse (false::xs) = true andalso (allfalse xs)
    6.33 -   |allfalse (true::xs) = false;
    6.34 -
    6.35 -fun not_empty [] = false 
    6.36 -    | not_empty _ = true;
    6.37 -
    6.38  fun twoisvar (a,b) = is_Var b;
    6.39  fun twoisfree (a,b) = is_Free b;
    6.40  fun twoiscomb (a,b) = iscomb b;
    6.41 @@ -86,7 +67,7 @@
    6.42                          true
    6.43                  else 
    6.44                          let val (f, args) = strip_comb t in
    6.45 -                            if ((is_Free f) orelse (is_Var f)) andalso (alltrue (map is_hol_tm args)) then 
    6.46 +                            if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then 
    6.47                                  true            (* should be is_const *)
    6.48                              else 
    6.49                                  false
    6.50 @@ -115,7 +96,7 @@
    6.51                          end
    6.52                 else if (iscomb f) then
    6.53                          let val (P, args) = strip_comb f in
    6.54 -                            ((is_hol_tm P)) andalso (alltrue (map is_hol_fm args))
    6.55 +                            ((is_hol_tm P)) andalso (forall is_hol_fm args)
    6.56                          end
    6.57                  else
    6.58                          is_hol_tm f;                              (* should be is_const, nee
    6.59 @@ -195,31 +176,9 @@
    6.60  fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
    6.61  
    6.62  
    6.63 -exception  powerError;
    6.64  
    6.65 -fun power (x, n) =  if x = 0 andalso n = 0 
    6.66 -                    then raise powerError
    6.67 -                    else  if n = 0 
    6.68 -                          then 1
    6.69 -                          else x * power (x, n-1);
    6.70 -
    6.71 -
    6.72 -fun get_tens n = power(10, (n-1))
    6.73 -
    6.74 -
    6.75 -fun digits_to_int [] posn  n = n
    6.76 -|   digits_to_int (x::xs) posn  n = let 
    6.77 -				        val digit_val = ((ord x) - 48)*(get_tens posn)
    6.78 -          		            in
    6.79 -                                        digits_to_int xs (posn -1 )(n + digit_val) 
    6.80 -         		            end;
    6.81 -
    6.82 -fun int_of_string str = let 
    6.83 -			   val digits = explode str
    6.84 -                           val posn   = length digits
    6.85 -                        in 
    6.86 -		            digits_to_int digits posn 0
    6.87 -                        end
    6.88 -                	
    6.89 - 
    6.90 +fun int_of_string str = valOf (Int.fromString str)
    6.91 +                        handle Option => error ("int_of_string: " ^ str);
    6.92 +    
    6.93 +                	 
    6.94  exception ASSERTION of string;
     7.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Apr 21 13:15:25 2005 +0200
     7.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Apr 21 15:05:24 2005 +0200
     7.3 @@ -1,3 +1,8 @@
     7.4 +(*  ID:         $Id$
     7.5 +    Author:     Claire Quigley
     7.6 +    Copyright   2004  University of Cambridge
     7.7 +*)
     7.8 +
     7.9  (******************)
    7.10  (* complete later *)
    7.11  (******************)
    7.12 @@ -23,15 +28,6 @@
    7.13                              end
    7.14  
    7.15  
    7.16 -fun thm_of_string str = let val _ = set show_sorts
    7.17 -                                val term = read str
    7.18 -                                val propterm = HOLogic.mk_Trueprop term
    7.19 -                                val cterm = cterm_of Mainsign propterm
    7.20 -                                val _ = reset show_sorts
    7.21 -                            in
    7.22 -                                assume cterm
    7.23 -                            end
    7.24 -
    7.25  (* check separate args in the watcher program for separating strings with a * or ; or something *)
    7.26  
    7.27  fun clause_strs_to_string [] str = str
     8.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Apr 21 13:15:25 2005 +0200
     8.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Apr 21 15:05:24 2005 +0200
     8.3 @@ -1,4 +1,7 @@
     8.4 -
     8.5 +(*  ID:         $Id$
     8.6 +    Author:     Claire Quigley
     8.7 +    Copyright   2004  University of Cambridge
     8.8 +*)
     8.9  
    8.10  fun add_in_order (x:string) [] = [x]
    8.11  |   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
     9.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 21 13:15:25 2005 +0200
     9.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 21 15:05:24 2005 +0200
     9.3 @@ -1,3 +1,8 @@
     9.4 +(*  ID:         $Id$
     9.5 +    Author:     Claire Quigley
     9.6 +    Copyright   2004  University of Cambridge
     9.7 +*)
     9.8 +
     9.9  (* Get claset rules *)
    9.10  
    9.11  
    10.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Apr 21 13:15:25 2005 +0200
    10.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Apr 21 15:05:24 2005 +0200
    10.3 @@ -1,7 +1,7 @@
    10.4 -
    10.5 - (*  Title:      Watcher.ML
    10.6 -     Author:     Claire Quigley
    10.7 -     Copyright   2004  University of Cambridge
    10.8 +(*  Title:      Watcher.ML
    10.9 +    ID:         $Id$
   10.10 +    Author:     Claire Quigley
   10.11 +    Copyright   2004  University of Cambridge
   10.12   *)
   10.13  
   10.14   (***************************************************************************)
    11.1 --- a/src/HOL/Tools/ATP/watcher.sig	Thu Apr 21 13:15:25 2005 +0200
    11.2 +++ b/src/HOL/Tools/ATP/watcher.sig	Thu Apr 21 15:05:24 2005 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4 -
    11.5 -(*  Title:      Watcher.ML
    11.6 +(*  ID:         $Id$
    11.7      Author:     Claire Quigley
    11.8      Copyright   2004  University of Cambridge
    11.9  *)
   11.10 @@ -14,7 +13,7 @@
   11.11  
   11.12  
   11.13  signature WATCHER =
   11.14 -  sig
   11.15 +sig
   11.16  
   11.17  (*****************************************************************************************)
   11.18  (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)